theory ex08_bonus imports "~~/src/HOL/IMP/Small_Step" "~~/src/HOL/IMP/Vars" begin (* Your tasks are marked with (**! \ *) *) (* Removes old notation, just keep this stuff ;) *) no_notation small_steps (infix "\*" 55) no_notation small_step (infix "\" 55) no_notation Assign ("_ ::= _" [1000, 61] 61) no_notation Seq ("_;;/ _" [60, 61] 60) no_notation If ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61) no_notation While ("(WHILE _/ DO _)" [0, 61] 61) datatype com = SKIP | Assign vname aexp ("_ ::= _" [1000, 61] 61) | Seq com com ("_ ;;/ _" [60, 61] 60) | Par com com ("_ ||/ _" [60, 61] 60) | If bexp com com ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61) | While bexp com ("(WHILE _/ DO _)" [0, 61] 61) text {* Start with defining the (used) variables of a command, i.e., all the variables appearing in the command. For notation convenience, you should proceed similarly to what we did for expressions in the theory @{text "Vars"}, namely, register the type of commands as an instance of the class @{text "vars"}---then you can use the name @{text "vars"} for the newly defined operation on commands. We have started the definition, you need to add the remaining clauses. *} instantiation com :: vars begin fun vars_com :: "com \ vname set" where "vars SKIP = {}" (**! Add the remaining equations here *) instance .. end (**! Extend the small step semantics with parallelism **) inductive small_step :: "com * state \ com * state \ bool" (infix "\" 55) where "undefined \ small_step x y" (**! Replace this by the correct rules! **) abbreviation small_steps :: "com * state \ com * state \ bool" (infix "\*" 55) where "x \* y == star small_step x y" (**** Automation setup ****) lemmas small_step_induct = small_step.induct[split_format(complete), induct pred] lemmas star_induct = star.induct[of small_step, split_format(complete), induct pred] declare small_step.intros[simp,intro] inductive_cases SkipE[elim!]: "(SKIP,s) \ ct" inductive_cases AssignE[elim!]: "(x::=a,s) \ ct" inductive_cases SeqE[elim]: "(c1;;c2,s) \ ct" inductive_cases ParE[elim!]: "(c1||c2,s) \ ct" inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \ ct" inductive_cases WhileE[elim]: "(WHILE b DO c, s) \ ct" (***** Adapted stuff from exercise solution ******) (**! If some of those lemmas fail: Look at the definition of your semantics! If you still think your semantics is correct, you'll have to redo the proofs. But chances are high that your semantics is odd. **) lemma [simp]: "s1 = s2 on X \ vars a \ X \ aval a s1 = aval a s2" by (metis aval_eq_if_eq_on_vars set_mp) lemma [simp]: "s1 = s2 on X \ vars b \ X \ bval b s1 = bval b s2" by (metis bval_eq_if_eq_on_vars set_mp) lemma vars_subsetD[dest]: "(c, s) \ (c', s') \ vars c' \ vars c" by (induction c s c' s' rule: small_step_induct) auto lemma small_step_confinement: "(c, s) \ (c', s') \ s = s' on UNIV - vars c" by (induction rule: small_step_induct) auto lemma small_steps_confinement: "(c, s) \* (c', s') \ s = s' on UNIV - vars c" by (induction rule: star_induct) (metis DiffD1 DiffD2 DiffI in_mono small_step_confinement vars_subsetD)+ text {* Now, we are ready to show that commands only depend on the variables they use: *} lemma small_step_indep: "(c, s) \ (c', s') \ s = t on X \ vars c \ X \ \t'. (c, t) \ (c', t') \ s' = t' on X" by (induction rule: small_step_induct) auto lemma small_steps_indep: "\(c, s) \* (c', s'); s = t on X; vars c \ X\ \ \t'. (c, t) \* (c', t') \ s' = t' on X" apply (induction arbitrary: t rule: star_induct) apply auto [] apply (frule (2) small_step_indep) apply (drule vars_subsetD) by (metis (hide_lams, no_types) dual_order.trans star.step) (* Alternative proof *) lemma "\(c, s) \* (c', s'); s = t on X; vars c \ X\ \ \t'. (c, t) \* (c', t') \ s' = t' on X" proof (induction arbitrary: t rule: star_induct) case (step c s c' s' c'' s'') with small_step_indep[of c s c' s' X t] obtain t' where "(c, t) \ (c', t')" "s' = t' on X" by blast moreover from step have "vars c' \ X" by blast ultimately obtain t'' where "(c', t') \* (c'', t'')" "s'' = t'' on X" using step.IH by blast with `(c, t) \ (c', t')` show ?case by (auto intro: star.step) qed auto lemma small_steps_SeqE: "(c1 ;; c2, s) \* (SKIP, s') \ \t. (c1, s) \* (SKIP, t) \ (c2, t) \* (SKIP, s')" by (induction "c1 ;; c2" s SKIP s' arbitrary: c1 c2 rule: star_induct) (blast intro: star.step) lemma small_steps_SeqI: "\(c1, s) \* (SKIP, s'); (c2, s') \* (SKIP, t)\ \ (c1 ;; c2, s) \* (SKIP, t)" by (induction c1 s SKIP s' rule: star_induct) (auto intro: star.step) definition equiv_com :: "com \ com \ bool" (infix "\\<^sub>s" 50) where "c1 \\<^sub>s c2 \ (\s t. (c1, s) \* (SKIP, t) \ (c2, s) \* (SKIP, t))" text {* Show that we defined an equivalence relation *} lemma ec_refl[simp]: "equiv_com c c" unfolding equiv_com_def by auto lemma ec_sym: "equiv_com c1 c2 \ equiv_com c2 c1 " unfolding equiv_com_def by auto lemma ec_trans[trans]: "equiv_com c1 c2 \ equiv_com c2 c3 \ equiv_com c1 c3" unfolding equiv_com_def by auto text {* Finally, show that commands that share no common variables can be re-ordered *} theorem Seq_equiv_Seq_reorder: assumes vars: "vars c1 \ vars c2 = {}" shows "(c1 ;; c2) \\<^sub>s (c2 ;; c1)" proof - { txt {* As the statement is symmetric, we can take a shortcut by only proving one direction: *} fix c1 c2 s t assume Seq: "(c1 ;; c2, s) \* (SKIP, t)" and vars: "vars c1 \ vars c2 = {}" have "(c2 ;; c1, s) \* (SKIP, t)" proof - obtain s' where c1: "(c1, s) \* (SKIP, s')" and c2: "(c2, s') \* (SKIP, t)" using Seq by (metis Seq small_steps_SeqE) from small_steps_confinement[OF c1] have "s' = s on UNIV - vars c1" by auto from small_steps_indep[OF c2 this] `vars c1 \ vars c2 = {}` obtain t' where t': "(c2, s) \* (SKIP, t')" and "t = t' on UNIV - vars c1" by auto from small_steps_confinement[OF this(1)] have "s = t' on UNIV - vars c2" by auto from small_steps_indep[OF c1 this] `vars c1 \ vars c2 = {}` obtain t'' where t'': "(c1, t') \* (SKIP, t'')" and "s' = t'' on UNIV - vars c2" by auto from `(c2, s) \* (SKIP, t')` `(c1, t') \* (SKIP, t'')` have "(c2 ;; c1, s) \* (SKIP, t'')" by (auto intro: small_steps_SeqI) moreover have "t'' = t" using `s' = t'' on UNIV - vars c2` small_steps_confinement[OF c2] using `t = t' on UNIV - vars c1` small_steps_confinement[OF t''] using `vars c1 \ vars c2 = {}` by (simp add: set_eq_iff) (metis DiffI ext iso_tuple_UNIV_I) ultimately show ?thesis by auto qed } with vars show ?thesis unfolding equiv_com_def by (metis Int_commute) qed (****************************************************************************) (**! As a warmup, show that parallel composition simulates sequential composition. This proof should be a few lines only. *) lemma Par_sim_Seq: "(c1 ;; c2, s) \* (SKIP, s') \ (c1 || c2, s) \* (SKIP, s')" oops (**! Then show that sequential composition simulates parallel composition, if the variables are disjoint. This proof may be a bit harder. *) lemma Seq_sim_Par: assumes "(c1 || c2, s) \* (SKIP, s')" "vars c1 \ vars c2 = {}" shows "(c1 ;; c2, s) \* (SKIP, s')" oops (**! Now combine the lemmas to show equivalence of parallel and sequential composition *) theorem Par_equiv_Seq: "vars c1 \ vars c2 = {} \ (c1 || c2) \\<^sub>s (c1 ;; c2)" oops end