Theory Drinks_Machine_2

section‹An Observationally Equivalent Model›
text‹This theory defines a second formalisation of the drinks machine example which produces
identical output to the first model. This property is called \emph{observational equivalence} and is
discussed in more detail in cite"foster2018".›
theory Drinks_Machine_2
imports Drinks_Machine
begin

(* Only imports Drinks_Machine_LTL so I can easily open all three at once for testing *)

definition vend_nothing ::  where
"vend_nothing
Label = (STR ''vend''),
Arity = 0,
Guards = [],
Outputs =  [],
Updates = [(1, V (R 1)), (2, V (R 2))]
"

lemmas transitions = Drinks_Machine.transitions vend_nothing_def

definition drinks2 :: transition_matrix where
"drinks2 = {|
((0,1), select),
((1,1), vend_nothing),
((1,2), coin),
((2,2), coin),
((2,2), vend_fail),
((2,3), vend)
|}"

lemma possible_steps_0:
"length i = 1
possible_steps drinks2 0 r ((STR ''select'')) i = {|(1, select)|}"
apply (simp add: possible_steps_def drinks2_def transitions)
by force

lemma possible_steps_1:
"length i = 1
possible_steps drinks2 1 r ((STR ''coin'')) i = {|(2, coin)|}"
apply (simp add: possible_steps_def drinks2_def transitions)
by force

lemma possible_steps_2_coin:
"length i = 1
possible_steps drinks2 2 r ((STR ''coin'')) i = {|(2, coin)|}"
apply (simp add: possible_steps_def drinks2_def transitions)
by force

lemma possible_steps_2_vend:
"r $2 = Some (Num n) n 100 possible_steps drinks2 2 r ((STR ''vend'')) [] = {|(3, vend)|}" apply (simp add: possible_steps_singleton drinks2_def) apply safe by (simp_all add: transitions apply_guards_def value_gt_def join_ir_def connectives) lemma recognises_first_select: "recognises_execution drinks 0 r ((aa, b) # as) aa = STR ''select'' length b = 1" using recognises_must_be_possible_step[of drinks 0 r "(aa, b)" as] apply simp apply clarify by (metis first_step_select recognises_possible_steps_not_empty drinks_0_rejects fst_conv snd_conv) lemma drinks2_vend_insufficient: "possible_steps drinks2 1 r ((STR ''vend'')) [] = {|(1, vend_nothing)|}" apply (simp add: possible_steps_def drinks2_def transitions) by force lemma drinks2_vend_insufficient2: "r$ 2 = Some (Num x1)
x1 < 100
possible_steps drinks2 2 r ((STR ''vend'')) [] = {|(2, vend_fail)|}"
apply safe
by (simp_all add: transitions apply_guards_def value_gt_def join_ir_def connectives)

lemma drinks2_vend_sufficient: "r $2 = Some (Num x1) ¬ x1 < 100 possible_steps drinks2 2 r ((STR ''vend'')) [] = {|(3, vend)|}" apply (simp add: possible_steps_singleton drinks2_def) apply safe by (simp_all add: transitions apply_guards_def value_gt_def join_ir_def connectives) lemma recognises_1_2: proof(induct t arbitrary: r) case (Cons a as) then show ?case apply (cases a) apply (simp add: recognises_step_equiv) apply (case_tac "a=(STR ''vend'', [])") apply (case_tac "n. r$2 = Some (Num n)")
apply clarify
apply (case_tac "n < 100")
apply (metis recognises_prim recognises_prim.elims(3) drinks_rejects_future)
using drinks_vend_invalid apply blast
apply (case_tac "i. a=(STR ''coin'', [i])")
apply clarify
by (metis recognises_execution.simps drinks_1_rejects_trace)
qed auto

lemma drinks_reject_0_2:
"i. a = (STR ''select'', [i])
possible_steps drinks 0 r (fst a) (snd a) = {||}"
apply (rule drinks_0_rejects)
by (cases a, case_tac "snd a", auto)

lemma purchase_coke:
"observe_execution drinks2 0 <> [((STR ''select''), [Str ''coke'']), ((STR ''coin''), [Num 50]), ((STR ''coin''), [Num 50]), ((STR ''vend''), [])] =
[[], [Some (Num 50)], [Some (Num 100)], [Some (Str ''coke'')]]"
possible_steps_1 coin_def apply_outputs finfun_update_twist
possible_steps_2_coin possible_steps_2_vend vend_def)

lemma drinks2_0_invalid:
"¬ (aa = (STR ''select'')  length (b) = 1)
(possible_steps drinks2 0 <> aa b) = {||}"
apply (simp add: drinks2_def possible_steps_def transitions)
by force

lemma drinks2_vend_r2_none:
"r $2 = None possible_steps drinks2 2 r ((STR ''vend'')) [] = {||}" apply (simp add: possible_steps_empty drinks2_def can_take_transition_def can_take_def transitions) by (simp add: value_gt_def) lemma drinks2_end: apply (simp add: possible_steps_def drinks2_def transitions) by force lemma drinks2_vend_r2_String: "r$ 2 = Some (value.Str x2)
possible_steps drinks2 2 r ((STR ''vend'')) [] = {||}"
apply safe
by (simp_all add: transitions can_take_transition_def can_take_def value_gt_def)

lemma drinks2_2_invalid:
"fst a = (STR ''coin'')  length (snd a)  1
a  ((STR ''vend''), [])
possible_steps drinks2 2 r (fst a) (snd a) = {||}"
apply (simp add: possible_steps_empty drinks2_def transitions can_take_transition_def can_take_def)
by (metis prod.collapse)

lemma drinks2_1_invalid:
"¬(a = (STR ''coin'')  length b = 1)
¬(a = (STR ''vend'')  b = [])
possible_steps drinks2 1 r a b = {||}"
apply safe
by (simp_all add: transitions can_take_transition_def can_take_def value_gt_def)

lemma drinks2_vend_invalid:
"n. r $2 = Some (Num n) possible_steps drinks2 2 r (STR ''vend'') [] = {||}" apply (simp add: possible_steps_empty drinks2_def) apply safe by (simp_all add: transitions can_take_transition_def can_take_def value_gt_def MaybeBoolInt_not_num_1) lemma equiv_1_2: proof(induct x arbitrary: r) case (Cons a t) then show ?case apply (cases a, clarsimp) apply (simp add: executionally_equivalent_step) apply (case_tac "fst a = STR ''coin'' length (snd a) = 1") apply (simp add: Drinks_Machine.possible_steps_1_coin possible_steps_2_coin) apply (case_tac "a = (STR ''vend'', [])") defer using drinks2_2_invalid drinks_no_possible_steps_1 apply auto[1] apply (case_tac "n. r$ 2 = Some (Num n)")
defer using drinks_vend_invalid drinks2_vend_invalid apply simp
apply clarify
subgoal for aa b n
apply (case_tac "n < 100")
apply (induct t)
apply simp
subgoal for aa t apply (case_tac aa, clarsimp)
by (simp add: executionally_equivalent_step drinks_end drinks2_end)
done
done
qed auto

lemma equiv_1_1:
proof(induct x)
case (Cons a t)
then show ?case
apply (cases a, clarsimp)
subgoal for aa b
apply (case_tac "aa = STR ''coin''  length b = 1")
apply (simp add: possible_steps_1_coin possible_steps_1 equiv_1_2)
apply (case_tac "a = (STR ''vend'', [])")
apply clarsimp
apply (metis finfun_upd_triv)
done
qed auto

(* Corresponds to Example 3 in Foster et. al. *)
lemma executional_equivalence:
proof(induct t)
case (Cons a t)
then show ?case
apply (cases a, clarify)
subgoal for aa b