theory tut08 imports "~~/src/HOL/IMP/Small_Step" "~~/src/HOL/IMP/Vars" begin term "(s::state) = (t::state) on (X::vname set)" lemma [simp]: "\s1 = s2 on X; vars a \ X\ \ aval a s1 = aval a s2" by (induction a) auto lemma [simp]: "\s1 = s2 on X; vars b \ X\ \ bval b s1 = bval b s2" by (induction b) auto lemma vars_subsetD[dest]: "(c,s) \ (c',s') \ vars c' \ vars c" by (induction 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" apply (induction rule: star_induct) apply simp apply auto by (metis DiffI UNIV_I in_mono small_step_confinement vars_subsetD) 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" proof (induction arbitrary: t rule: star_induct) case (step c s ch sh c' s') have "vars ch \ vars c" using step.hyps(1) by (blast) also note `vars c \ X` finally have "vars ch \ X" . from small_step_indep [OF step.hyps(1) `s=t on X` `vars c \ X`] obtain th where 1: "(c, t) \ (ch, th)" and "sh = th on X" by blast from step.IH[OF `sh = th on X` `vars ch \ X`] obtain t' where 2: "(ch, th) \* (c', t')" and 3: "s' = t' on X" by blast from 1 2 have "(c,t) \* (c',t')" by (rule star.step) with 3 show ?case by blast qed auto (* Alternative apply-style proof: *) lemma "\(c,s) \* (c',s'); s=t on X; vars c \ X \ \ \t'. (c,t)\*(c',t') \ s'=t' on X" (* Isar proof is more appropriate here! *) 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) text {* Two lemmas that may prove useful for the next proof.*} 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 (rule seq_comp) (* by (induction c1 s SKIP s' rule: star_induct) (auto intro: star.step) *) lemma small_steps_Seq_eq: "(c1 ;; c2, s) \* (SKIP, s') \ (\t. (c1, s) \* (SKIP, t) \ (c2, t) \* (SKIP, s'))" by (metis small_steps_SeqE small_steps_SeqI) 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" by (auto simp: equiv_com_def) lemma ec_sym: "equiv_com c1 c2 \ equiv_com c2 c1 " by (auto simp: equiv_com_def) lemma ec_trans[trans]: "equiv_com c1 c2 \ equiv_com c2 c3 \ equiv_com c1 c3" by (auto simp: equiv_com_def) text {* Note that our small-step equivalence matches the big-step equivalence *} lemma "c1\\<^sub>sc2 \ c1\c2" unfolding equiv_com_def by (metis big_iff_small) 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 end