Isabelle club meeting on February 10 2016

Audience

Frédéric Boulanger
Chantal Keller
Safouan Taha
Frédéric Tuong
Yakoub Nemouchi
Burkhart Wolff
Zeye DU
Hai Nguyen Van

Support pédagogique pour Isabelle

Frédéric B & Burkhart

Frédéric présente un petit langage de description d'automate énumérant des inputs, outputs et des rules. Une rule est une [garde] input -> output. Un exemple portant sur un contrôleur de vitesse est présenté:

cruise
inputs: on off cruise brake standby
outputs: on=false cruise=false
rules:
[] off -> on=false cruise=false
[!on] on -> on=true cruise=false
[on] cruise -> cruise=true
[cruise] brake -> cruise=false
[cruise] standby -> cruise=false

Une génération de code (automatisée via Acceleo) permet de générer un fichier Isabelle comprenant la fonction de transition qui traduit les rules:

theory Cruise
imports Machine

begin
datatype Cruise = 
  Cruise  (on: bool)  (cruise: bool) 

definition CruiseInit :: Cruise
where
  "CruiseInit ≡ Cruise False False"

abbreviation on :: nat where "on ≡ 0"
abbreviation off :: nat where "off ≡ Suc on"
abbreviation cruise :: nat where "cruise ≡ Suc off"
abbreviation brake :: nat where "brake ≡ Suc cruise"
abbreviation standby :: nat where "standby ≡ Suc brake"

instantiation Cruise :: machine
begin
  fun behavior_Cruise :: "Cruise ⇒ nat ⇒ Cruise"
  where
    "behavior_Cruise (Cruise _ _) off = Cruise False False"
  | "behavior_Cruise (Cruise False _) on = Cruise True False"
  | "behavior_Cruise (Cruise True _) cruise = Cruise True True"
  | "behavior_Cruise (Cruise isOn True) brake = Cruise isOn False"
  | "behavior_Cruise (Cruise isOn True) standby = Cruise isOn False"
  | "behavior_Cruise some_cruise _ = some_cruise"

  instance ..
end (* instantiation *)

end

La théorie générée instancie la classe Machine (théorie ad-hoc développée par Frédéric) qui regroupe un certain nombre de fonctions et de prédicats, dont la notion d'état accessible par un chemin (liste d'inputs).

theory Machine

imports Main

begin

(* 
 * A machine behaves when receiving an input (encoded as a nat)
 * and becomes a new machine.
 *)
class machine =
  fixes behavior :: "'a ⇒ nat ⇒ 'a" (infixl "→" 60)
begin
  (* Machine m2 is a successor of m1 if m1 can become m2 when receiving an input. *)
  definition successor :: "'a ⇒ 'a ⇒ nat set ⇒ bool"
  where
    "successor m1 m2 inp ≡ (∃i ∈ inp. m2 = m1 → i)"

  (* Machine m2 is reachable from m1 by path p if the succession 
     of behaviors triggered by the inputs in p lead from m1 to m2.
   *)
  (* Definition as a function (for computation) *)
  fun reach_by_path_f :: "'a ⇒ 'a ⇒ nat list ⇒ bool"
  where
    "reach_by_path_f m1 m2 [] = (m1 = m2)"
  | "reach_by_path_f m1 m2 [inp] = (m2 = m1 → inp)"
  | "reach_by_path_f m1 m2 (i1#i2#seq) = reach_by_path_f (m1 → i1) m2 (i2#seq)"

  (* Definition as an inductive predicate (for proofs) *)
  inductive reach_by_path :: "'a ⇒ 'a ⇒ nat list ⇒ bool"
  where
    "m1 = m2 ⟹ reach_by_path m1 m2 []"
  | "m1 → inp = m2 ⟹ reach_by_path m1 m2 [inp]"
  | "reach_by_path (m1 → inp) m2 (i#seq) ⟹ reach_by_path m1 m2 (inp#i#seq)"

  (* Generate elimination rules for proof automation *)
  inductive_cases empty_path[elim!]:"reach_by_path m1 m2 []"
  inductive_cases step_path[elim!]:"reach_by_path m1 m2 [inp]"
  inductive_cases long_path[elim]:"reach_by_path m1 m2 (inp#i#seq)"

  (* Proof that the function and the inductive predicate are the same *)
  lemma [code]:"reach_by_path m1 m2 seq = reach_by_path_f m1 m2 seq"
  proof (induction seq arbitrary: m1 m2) print_cases
    case Nil
      show ?case using reach_by_path.intros(1) by auto
  next
    case (Cons i s)
      show ?case
      proof (cases s)
        case Nil
          have "reach_by_path m1 m2 (i#[]) = reach_by_path (m1 → i) m2 []"
            using reach_by_path.simps and step_path by metis
          moreover have "reach_by_path_f m1 m2 (i#[]) = reach_by_path_f (m1 → i) m2 []"
            using reach_by_path_f.simps(2) by auto
          ultimately show "reach_by_path m1 m2 (i # s) = reach_by_path_f m1 m2 (i # s)"
            using Cons.IH and Nil by auto
      next
        case (Cons i' s')
          have "reach_by_path m1 m2 (i#i'#s') = reach_by_path (m1 → i) m2 (i'#s')"
            using reach_by_path.simps and long_path by metis
          moreover have "reach_by_path_f m1 m2 (i#i'#s') = reach_by_path_f (m1 → i) m2 (i'#s')"
            using reach_by_path_f.simps(3) by auto
          ultimately show "reach_by_path m1 m2 (i # s) = reach_by_path_f m1 m2 (i # s)"
            using Cons.IH and Cons and reach_by_path.intros(3) by auto
      qed
  qed

  (* Machine m2 is reachable from m1 with a set of inputs
     if there exists a sequence of inputs taken from the set
     that leads from m1 to m2. *)
  definition reachable :: "'a ⇒ 'a ⇒ nat set ⇒ bool"
  where
    "reachable m1 m2 inp ≡ (∃seq. (set seq) ⊆ inp ∧ reach_by_path m1 m2 seq)"

end (* class machine *)

end

Pour ceux que cela intéresse, les instructions pour créer les plug-ins Eclipse pour l'éditeur du langage et les transformations Acceleo sont données dans le sujet proposé aux élèves.

Voici un corrigé pour la grammaire Xtext du langage, la transformation vers Java et la transformation vers Isabelle.

En vu de simplifier les preuves et d'en améliorer l'automatisation, on propose d'utiliser des théories alternatives à Machine:

Burkhart présente une formalisation alternative à base de monades. la théorie Monads encode de manière naturelle les machines de Mealy. Notre fonction de transition devient une fonction d'input vers monades.

theory Cruise_Monad
imports Monads
begin
record cruise_state = 
   on     :: bool
   cruise :: bool


definition σ⇩0 where "σ⇩0 = ⦇ on = False, cruise = False⦈"


datatype inputs = on | off | cruise | brake | standby


fun      step :: "inputs ⇒ (unit, cruise_state) MON⇩S⇩E"
where   "step on      = (λσ.(if cruise_state.on σ 
                         then Some((), σ⦇on:=True, cruise:=False⦈) 
                         else Some((), σ)))"
      | "step cruise  = (λσ.(if cruise_state.on σ 
                         then Some((), σ⦇on:=True, cruise:=True⦈) 
                         else Some((), σ)))"
      | "step off     = (λσ. Some((), σ⦇on:=True, cruise:=False⦈))" 
      | "step brake   = (λσ.(if cruise_state.cruise σ 
                         then Some((), σ⦇cruise:=False⦈) 
                         else Some((), σ)))"      
      | "step standby = (λσ.(if cruise_state.cruise σ 
                         then Some((), σ⦇cruise:=False⦈) 
                         else Some((), σ)))"     

lemma    step_is_total : "step X σ ≠ None"
by(induct X, simp_all)

theorem unreacheable :
assumes  "set S ⊆ {on, off, brake, standby}"
shows    " σ⇩0 ⊨ (_ ← mbind⇩F⇩a⇩i⇩l⇩S⇩t⇩o⇩p S step ; assert⇩S⇩E(λ σ. ¬ (cruise_state.cruise σ)))"
txt{* All valid execution sequences from @{term σ⇩0} to anywhere via a sequence @{term S} 
      not containing @{term cruise} leads to a safe state. *}
proof(rule assms [THEN rev_mp], rule List.rev_induct)
   show "set [] ⊆ {inputs.on, off, brake, standby} ⟶
             (σ⇩0 ⊨ ( _ ← mbind⇩F⇩a⇩i⇩l⇩S⇩t⇩o⇩p [] step; assert⇩S⇩E (λσ. ¬ cruise_state.cruise σ)))"
        by(simp add:  Monads.assert_disch4 σ⇩0_def)
next
   fix x xs
   show "set xs ⊆ {inputs.on, off, brake, standby} ⟶
            (σ⇩0 ⊨ ( _ ← mbind⇩F⇩a⇩i⇩l⇩S⇩t⇩o⇩p xs step; assert⇩S⇩E (λσ. ¬ cruise_state.cruise σ))) ⟹
            set (xs @ [x]) ⊆ {inputs.on, off, brake, standby} ⟶
            (σ⇩0 ⊨  ( _ ← mbind⇩F⇩a⇩i⇩l⇩S⇩t⇩o⇩p (xs @ [x]) step; assert⇩S⇩E (λσ. ¬ cruise_state.cruise σ)))" 
         apply(rule impI, erule impE, simp, erule assert_suffix_inv)
         by(auto simp: valid_SE_def bind_SE_def assert_SE_def)
qed

On note ici l'usage de la règle List.rev_induct qui permet de raisonner sur un invariant d'exécution. Le théorème prouve que l'état de régulation est inatteignable sans l'occurence de l'input cruise .

Chantal propose d'utiliser les relations pour formaliser la fonction de transition. Il suffit ensuite de générer la fermeture transitive pour raisonner sur les chemins d'exécution.

definition step' :: "inputs ⇒ cruise_state rel"
where     "step' x = {(σ,σ'). step x σ = Some((), σ') }" 

definition steps' where "steps' ≡ step' inputs.on ∪ step' off ∪ step' brake ∪ step' standby "

find_theorems name:"induct" "_⇧*" 
theorem "(σ⇩0,σ) ∈ (steps')⇧* ⟹ ¬ cruise_state.cruise σ"
apply(erule rtrancl.induct)

Nouvelle version utilisant la clôture reflexive et transitive

Je regroupe la définition de la relation successors s (transitions possibles sur un alphabet d'entrée s) et de la relation reachable s (états entre lesquels il existe un chemin sur l'alphabet d'entrée s) dans une locale :

theory Machine

imports Main

begin

(* 
 * A machine behaves when receiving an input (of type 'inp) and becomes a new machine.
 *)
locale machine =
  fixes behavior :: "'inp ⇒ 'a ⇒ 'a" (infixl "→" 60)
begin
  (* Machine m2 is a successor of m1 if m1 can become m2 when receiving an input. *)
  definition successors :: "'inp set ⇒ 'a rel"
  where
    "successors s ≡ ⋃i∈s. {(σ, σ'). σ'= i → σ}"

  (* Alternate definition
  definition successors :: "CruiseInput set ⇒ Cruise rel"
  where
    "successors s ≡ {(σ, σ'). ∃i ∈ s. σ' = i → σ}"
  *)

  (* Machine m2 is reachable from m1 with a set of inputs
     if there exists a sequence of inputs taken from the set
     that leads from m1 to m2. *)
  abbreviation reachable :: "'inp set ⇒ 'a rel"
  where
    "reachable s ≡ (successors s)⇧*"

  lemma successors_sub:"successors s ⊆ successors UNIV"
  using successors_def by auto

  lemma reachable_mono: "s ⊆ s' ⟹ reachable s ⊆ reachable s'"
  unfolding successors_def by (simp add: SUP_subset_mono rtrancl_mono)

end (* locale machine *)

print_locale! machine

end

La transformation Acceleo (Trans2Isabelle.mtl) a été mise à jour pour générer une théorie qui utilise cette locale. Elle génère également quelques lemmes utiles qui sont prouvés automatiquement :

theory Cruise
imports Machine

begin
datatype Cruise = 
  Cruise  (s_on: bool)  (s_cruise: bool) 

(* Some lemmas to get an instance from a simple property on the state *)
lemma on_ex:
  assumes "s_on m  = X"
  shows   "∃ p_cruise. m = Cruise X p_cruise"
proof -
  from Cruise.nchotomy obtain p_on p_cruise
       where "m = Cruise p_on p_cruise" by blast
  with assms show ?thesis by simp
qed

lemma cruise_ex:
  assumes "s_cruise m  = X"
  shows   "∃p_on . m = Cruise p_on X"
proof -
  from Cruise.nchotomy obtain p_on p_cruise
       where "m = Cruise p_on p_cruise" by blast
  with assms show ?thesis by simp
qed


(* The initial state of a Cruise *)
abbreviation CruiseInit :: Cruise
where
  "CruiseInit ≡ Cruise False False"

(* Possible inputs for a Cruise machine *)
datatype CruiseInput = on | off | cruise | brake | standby

(* Behavior of a Cruise machine *)
fun CruiseBehavior :: "CruiseInput ⇒ Cruise ⇒ Cruise"
where
"CruiseBehavior off (Cruise _ _) = Cruise False False"
  | "CruiseBehavior on (Cruise False _) = Cruise True False"
  | "CruiseBehavior cruise (Cruise True _) = Cruise True True"
  | "CruiseBehavior brake (Cruise isOn True) = Cruise isOn False"
  | "CruiseBehavior standby (Cruise isOn True) = Cruise isOn False"
  | "CruiseBehavior _ some_cruise = some_cruise"

(* A Cruise can be interpreted as a machine *)
interpretation machine "CruiseBehavior" .

end

Il est alors possible de démontrer des propriétés sur le comportement de la machine :

theory CruiseProofs

imports Cruise

begin

(* It is possible to switch the machine on *)
lemma 1:"(CruiseInit, (Cruise True False)) ∈ successors UNIV"
proof -
  from CruiseBehavior.simps(2) have "CruiseBehavior on CruiseInit = (Cruise True False)" by simp
  hence "(CruiseInit, (Cruise True False)) ∈ successors {on}" unfolding successors_def by simp
  thus ?thesis using successors_sub ..
qed

(* It is possible to turn on cruising when the machine is on *)
lemma 2:"((Cruise True False), (Cruise True True)) ∈ successors UNIV"
proof -
  from CruiseBehavior.simps(3) have "CruiseBehavior cruise (Cruise True False) = (Cruise True True)" .
  hence "(Cruise True False, Cruise True True) ∈ successors {cruise}" unfolding successors_def by simp
  thus ?thesis using successors_sub ..
qed

(* It is possible to turn cruising on from the initial state *)
lemma "(CruiseInit, (Cruise True True)) ∈ reachable UNIV"
proof -
  from 1 and 2 show ?thesis by simp
qed

(* Without the cruise input, you cannot turn cruising on (function version) *)
lemma no_magic_cruise : 
  assumes "i ∈ {on, off, brake, standby}"
  shows   "s_cruise (CruiseBehavior i (Cruise a False)) = False"
proof (cases i) print_cases
  case cruise (* impossible case *)
    thus ?thesis using assms by simp
next
  case on print_facts
    thus ?thesis by (case_tac a, simp_all) 
qed simp_all

(* Without the cruise input, you cannot turn cruising on (relation version) *)
lemma no_magic_cruise_suc :
  "((Cruise a False), (Cruise a' True)) ∉ successors {on, off, brake, standby}" (is "(?a,?b) ∉ successors ?inpset")
proof -
  from no_magic_cruise have
    "∀i ∈ ?inpset. CruiseBehavior i ?a ≠ ?b"
    by (metis Cruise.sel(2))
    hence
      "¬(∃i ∈ ?inpset. CruiseBehavior i ?a = ?b)" by simp
  thus ?thesis unfolding successors_def by simp
qed

(* From any state with cruise off, all the reachable state without the cruise input have cruise off *)
lemma no_reach_cruise: "((Cruise a False), s) ∈ reachable {on, off, brake, standby} ⟹  ¬ s_cruise s"
proof (induction rule: rtrancl_induct)
    case base thus ?case by simp (* cruise is initially off *)
next 
    case (step y z) thus ?case   (* show that no step can switch is on *)
    proof -
      from cruise_ex step.IH obtain p where yfalse:"y = Cruise p False" by blast
      {
        assume "s_cruise z"
        with cruise_ex obtain g where "z = Cruise g True" by blast
        with yfalse and step.hyps(2) and no_magic_cruise_suc[of p g] have "False" by simp
      }
      thus ?thesis ..
    qed
qed

(* Dual version of the same theorem:
   From any state where cruise is off, if we reach a state where cruise is on, we received a cruise input *)
lemma reach_imp_cruise:"(Cruise a False, Cruise a' True) ∈ (reachable s) ⟹ cruise ∈ s" (is "?P ⟹ ?Q")
proof -
  {
    assume hyp:"¬?Q"
    hence "s ⊆ {on, off, brake, standby}" using CruiseInput.exhaust by blast
    from reachable_mono[OF this] have "reachable s ⊆ reachable {on, off, brake, standby}" .
    hence "?P ⟹ (Cruise a False, Cruise a' True) ∈ reachable {on, off, brake, standby}" by blast
    with no_reach_cruise have "¬?P" using Cruise.sel(2) by blast
  }
  thus "?P ⟹ ?Q" by blast
qed

end

Autre exemple, un peu plus complexe, avec des feux pour un passage piéton :

/*
 * A model of traffic lights for pedestrians
 * 
 * Properties to check (Promela/Spin syntax):
 *   ltl {[] !(car_green && ped_green)}   (safety)
 *   ltl {[] (car_red -> <> car_green)}   (liveness)
 *   ltl {[] (ped_red -> <> ped_green)}   (liveness)
 */
traffic
inputs: pedestrian car time
outputs: ped_green=true ped_red=false ped_waiting=false car_green=false car_orange=false car_red=true car_waiting=false
rules:
[ped_red !ped_waiting !car_waiting !car_orange]
  pedestrian -> car_green=false  car_orange=true
[car_orange]
  time       -> car_orange=false car_red=true    ped_waiting=true
[ped_waiting]
  time       -> ped_red=false    ped_green=true  ped_waiting=false
[car_red !car_waiting !ped_waiting]
  car        -> ped_green=false  ped_red=true    car_waiting=true
[car_waiting]
  time       -> car_red=false    car_green=true  car_waiting=false

Transformation Acceleo pour générer le code Promela/Spin permettant de vérifier les formules LTL : Trans2promela.mtl.

Théorie Isabelle :

theory Traffic
imports Machine

begin
datatype Traffic = 
  Traffic  (s_ped_green: bool)  (s_ped_red: bool)  (s_ped_waiting: bool)  (s_car_green: bool)  (s_car_orange: bool)  (s_car_red: bool)  (s_car_waiting: bool) 

(* Some lemmas to get an instance from a simple property on the state *)
lemma ped_green_ex:
  assumes "s_ped_green m  = X"
  shows   "∃ p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting. m = Traffic X p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting"
proof -
  from Traffic.nchotomy obtain p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting
       where "m = Traffic p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting" by blast
  with assms show ?thesis by simp
qed

lemma ped_red_ex:
  assumes "s_ped_red m  = X"
  shows   "∃p_ped_green  p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting. m = Traffic p_ped_green X p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting"
proof -
  from Traffic.nchotomy obtain p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting
       where "m = Traffic p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting" by blast
  with assms show ?thesis by simp
qed

lemma ped_waiting_ex:
  assumes "s_ped_waiting m  = X"
  shows   "∃p_ped_green p_ped_red  p_car_green p_car_orange p_car_red p_car_waiting. m = Traffic p_ped_green p_ped_red X p_car_green p_car_orange p_car_red p_car_waiting"
proof -
  from Traffic.nchotomy obtain p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting
       where "m = Traffic p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting" by blast
  with assms show ?thesis by simp
qed

lemma car_green_ex:
  assumes "s_car_green m  = X"
  shows   "∃p_ped_green p_ped_red p_ped_waiting  p_car_orange p_car_red p_car_waiting. m = Traffic p_ped_green p_ped_red p_ped_waiting X p_car_orange p_car_red p_car_waiting"
proof -
  from Traffic.nchotomy obtain p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting
       where "m = Traffic p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting" by blast
  with assms show ?thesis by simp
qed

lemma car_orange_ex:
  assumes "s_car_orange m  = X"
  shows   "∃p_ped_green p_ped_red p_ped_waiting p_car_green  p_car_red p_car_waiting. m = Traffic p_ped_green p_ped_red p_ped_waiting p_car_green X p_car_red p_car_waiting"
proof -
  from Traffic.nchotomy obtain p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting
       where "m = Traffic p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting" by blast
  with assms show ?thesis by simp
qed

lemma car_red_ex:
  assumes "s_car_red m  = X"
  shows   "∃p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange  p_car_waiting. m = Traffic p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange X p_car_waiting"
proof -
  from Traffic.nchotomy obtain p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting
       where "m = Traffic p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting" by blast
  with assms show ?thesis by simp
qed

lemma car_waiting_ex:
  assumes "s_car_waiting m  = X"
  shows   "∃p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red . m = Traffic p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red X"
proof -
  from Traffic.nchotomy obtain p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting
       where "m = Traffic p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting" by blast
  with assms show ?thesis by simp
qed


(* The initial state of a Traffic *)
abbreviation TrafficInit :: Traffic
where
  "TrafficInit ≡ Traffic True False False False False True False"

(* Possible inputs for a Traffic machine *)
datatype TrafficInput = pedestrian | car | time

(* Behavior of a Traffic machine *)
fun TrafficBehavior :: "TrafficInput ⇒ Traffic ⇒ Traffic"
where
"TrafficBehavior pedestrian (Traffic isPed_green True False _ False isCar_red False) = Traffic isPed_green True False False True isCar_red False"
  | "TrafficBehavior time (Traffic isPed_green isPed_red _ isCar_green True _ isCar_waiting) = Traffic isPed_green isPed_red True isCar_green False True isCar_waiting"
  | "TrafficBehavior time (Traffic _ _ True isCar_green isCar_orange isCar_red isCar_waiting) = Traffic True False False isCar_green isCar_orange isCar_red isCar_waiting"
  | "TrafficBehavior car (Traffic _ _ False isCar_green isCar_orange True False) = Traffic False True False isCar_green isCar_orange True True"
  | "TrafficBehavior time (Traffic isPed_green isPed_red isPed_waiting _ isCar_orange _ True) = Traffic isPed_green isPed_red isPed_waiting True isCar_orange False False"
  | "TrafficBehavior _ some_traffic = some_traffic"

(* A Traffic can be interpreted as a machine *)
interpretation machine "TrafficBehavior" .

end

Preuves :

theory TrafficProofs

imports Traffic

begin

(* definition only_one where "only_one boollist ≡ fold (λb s. if b then Suc s else s) boollist 0 = 1" *)
(*abbreviation "car_excl s ≡ only_one [s_car_green s, s_car_orange s, s_car_red s]"*)
abbreviation "car_excl s ≡ (s_car_green s ∨ s_car_orange s ∨ s_car_red s) ∧ ¬(s_car_green s ∧ s_car_orange s) ∧ ¬(s_car_orange s ∧ s_car_red s) ∧ ¬(s_car_green s ∧ s_car_red s)"
(*abbreviation "ped_excl s ≡ only_one [s_ped_green s, s_ped_red s]"*)
abbreviation "ped_excl s ≡ (s_ped_green s ∨ s_ped_red s) ∧ ¬(s_ped_green s ∧ s_ped_red s)"

(* Some invariants thet must be proven to hold together *)
abbreviation "traffic_inv s ≡
  car_excl s
∧ ped_excl s
∧ ¬(s_ped_green s ∧ s_car_green s)
∧ (s_ped_waiting s ⟶ s_ped_red s)
∧ (s_ped_waiting s ⟶ s_car_red s)
∧ (s_car_waiting s ⟶ s_car_red s)
∧ (s_car_waiting s ⟶ s_ped_red s)
∧ (s_car_orange s ⟶ s_ped_red s)
∧ ¬(s_ped_waiting s ∧ s_car_waiting s)
∧ (s_ped_red s ∧ ¬s_ped_waiting s ∧ ¬s_car_waiting s ⟶ s_car_green s ∨ s_car_orange s)"

(* Proof that the invariants are preserved for each reaction of the machine *)
lemma invariants_step:
  assumes "(s, t) ∈ successors UNIV"
  and     "traffic_inv s"
  shows   "traffic_inv t"
proof -
  from input_ex[OF assms(1)] obtain i where hyp:"t = TrafficBehavior i s" by blast
  show ?thesis
  proof (cases i)
    case pedestrian show ?thesis
      proof (cases "∀pg cg cr. s ≠ Traffic pg True False cg False cr False")
        case True
          hence "TrafficBehavior pedestrian s = s" by (metis (full_types) Traffic.collapse TrafficBehavior.simps(10,25,29,33))
          thus ?thesis using assms and hyp and pedestrian by auto
      next
        case False
          hence "∃pg cg cr. s = Traffic pg True False cg False cr False" by simp
          from this obtain pg cg cr where "s = Traffic pg True False cg False cr False" by blast
          with assms(2) have "s = Traffic False True False True False False False" by auto
          hence "t = Traffic False True False False True False False" using hyp pedestrian by simp
          thus ?thesis using hyp by auto
      qed
  next
    case car show ?thesis
      proof (cases "∀pg pr cg co. s ≠ Traffic pg pr False cg co True False")
        case True
          hence "TrafficBehavior car s = s" by (metis (full_types) Traffic.collapse TrafficBehavior.simps(7, 26, 34))
          thus ?thesis using assms and hyp and car by auto
      next
        case False
          hence "∃pg pr cg co. s = Traffic pg pr False cg co True False" by simp
          from this obtain pg pr cg co where "s = Traffic pg pr False cg co True False" by blast
          with assms(2) have "s = Traffic pg pr False False False True False" by simp
          hence "t = Traffic False True False False False True True" using hyp and car by simp
          thus ?thesis using hyp by auto
      qed
  next
    case time show ?thesis
      proof (cases "∃pg pr pw cg cr cw. s = Traffic pg pr pw cg True cr cw")
        case True
          from this obtain pg pr pw cg cr cw where "s = Traffic pg pr pw cg True cr cw" by blast
          with assms(2) have "s = Traffic False True pw False True False False" by auto
          hence "t = Traffic False True True False False True False" using hyp time by simp
          thus ?thesis using hyp assms by auto
      next
        case False
          hence "¬(∃pg pr pw cg cr cw. s = Traffic pg pr pw cg True cr cw)" by simp
          hence "s_car_orange s = False" using car_orange_ex by blast
          hence "∃pg pr pw cg cr cw. s = Traffic pg pr pw cg False cr cw" using car_orange_ex by simp
          from this obtain pg pr pw cg cr cw where sprop:"s = Traffic pg pr pw cg False cr cw" by blast
          show ?thesis
          proof (cases pw)
            case True
              hence "s = Traffic False True True False False True False" using sprop assms by auto
              hence "t = Traffic True False False False False True False" using hyp time by simp
              thus ?thesis using sprop hyp assms by auto
          next
            case False
              hence h:"s = Traffic pg pr False cg False cr cw" using sprop by simp
              show ?thesis
              proof (cases cw)
                case True
                  hence "s = Traffic False True False cg False cr True" using assms sprop h by auto
                  hence "t = Traffic False True False True False False False" using hyp time by simp
                  thus ?thesis using h hyp assms by auto
              next
                case False
                  hence "s = Traffic pg pr False cg False cr False" using sprop h by simp
                  hence "TrafficBehavior time s = s" using Traffic.collapse TrafficBehavior.simps(2,3,5,9,19,22) by simp
                  thus ?thesis using assms hyp time by auto
              qed
          qed
      qed
  qed
qed

(* Proof that the invariants hold for any reachable state from the initial state *)
lemma invariants:"(TrafficInit, t) ∈ reachable UNIV ⟹ traffic_inv t"
proof (induction rule: rtrancl_induct)
  case base thus ?case by auto
next
  case step thus ?case using invariants_step by simp
qed

(* Both lights are never green at the same time *)
lemma "(TrafficInit, t) ∈ reachable UNIV ⟹ ¬(s_ped_green t ∧ s_car_green t)"
using invariants by simp

end

Previous meeting -- Next meeting