theory tut09 imports "~~/src/HOL/IMP/Small_Step" "~~/src/HOL/IMP/Live_True" begin 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 -vars c" by (induction rule: small_step_induct) auto lemma small_steps_confinement: "(c,s) \* (c',s') \ s=s' on -vars c" apply (induction rule: star_induct) apply (auto simp: small_step_confinement) done 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') from small_step_indep[OF step.hyps(1) `s=t on X` `vars c \ X`] obtain th where 1: "(c,t) \ (ch,th)" and 2: "sh=th on X" by blast moreover from step.IH[OF 2] vars_subsetD[OF 1] `vars c \ X` obtain t' where "(ch, th) \* (c', t')" "s' = t' on X" by auto ultimately show ?case by (auto intro: star.step) qed auto thm star_induct lemma small_steps_seqE: "(c1;;c2,s)\*(SKIP,s') \ \t. (c1,s)\*(SKIP,t) \ (c2,t) \* (SKIP,s')" apply (induction "c1;;c2" s "SKIP" s' arbitrary: c1 c2 rule: star_induct) apply (blast intro: star.step) done lemma small_steps_seqI: "\ (c1,s)\*(SKIP,t); (c2,t) \* (SKIP,s')\ \ (c1;;c2,s) \* (SKIP,s')" apply (induction c1 s SKIP t rule: star_induct) apply (auto intro: star.step) done 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))" lemma ec_refl[simp]: "c \\<^sub>s c" unfolding equiv_com_def by auto lemma ec_sym: "c1 \\<^sub>s c2 \ c2 \\<^sub>s c1" unfolding equiv_com_def by auto lemma ec_trans[trans]: "c1 \\<^sub>s c2 \ c2 \\<^sub>s c3 \ c1 \\<^sub>s c3" unfolding equiv_com_def by auto lemma "c1\\<^sub>sc2 \ c1 \ c2" unfolding equiv_com_def by (metis big_iff_small) theorem Seq_equiv_Seq_reorder: assumes vars: "vars c1 \ vars c2 = {}" shows "c1;;c2 \\<^sub>s c2;;c1" proof - { 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 - from small_steps_seqE[OF Seq] obtain sh where c1s: "(c1,s) \* (SKIP,sh)" and c2sh: "(c2,sh) \* (SKIP,t)" by blast with small_steps_confinement have ssh_eq: "s=sh on -vars c1" and sht_eq: "sh=t on -vars c2" by auto from small_steps_indep[OF c2sh, where X="-vars c1" and t=s] ssh_eq vars obtain sh' where c2s: "(c2, s) \* (SKIP, sh')" and tsh'_eq: "t = sh' on - vars c1" by auto from small_steps_confinement[OF c2s] vars small_steps_indep[OF c1s, of "-vars c2" sh'] obtain t' where c1sh': "(c1, sh') \* (SKIP, t')" and sht'_eq: "sh = t' on - vars c2" by auto from small_steps_seqI[OF c2s c1sh'] have "(c2;; c1, s) \* (SKIP, t')" . moreover have "t'=t" apply (rule ext) by (metis Compl_iff c1sh' disjoint_iff_not_equal sht'_eq sht_eq small_steps_confinement tsh'_eq vars) ultimately show "(c2;; c1, s) \* (SKIP, t)" by simp qed } with vars show ?thesis unfolding equiv_com_def by blast qed end