1(* Title: ZF/IMP/Equiv.thy 2 Author: Heiko Loetzbeyer and Robert Sandner, TU M��nchen 3*) 4 5section \<open>Equivalence\<close> 6 7theory Equiv imports Denotation Com begin 8 9lemma aexp_iff [rule_format]: 10 "[| a \<in> aexp; sigma: loc -> nat |] 11 ==> \<forall>n. <a,sigma> -a-> n \<longleftrightarrow> A(a,sigma) = n" 12 apply (erule aexp.induct) 13 apply (force intro!: evala.intros)+ 14 done 15 16declare aexp_iff [THEN iffD1, simp] 17 aexp_iff [THEN iffD2, intro!] 18 19inductive_cases [elim!]: 20 "<true,sigma> -b-> x" 21 "<false,sigma> -b-> x" 22 "<ROp(f,a0,a1),sigma> -b-> x" 23 "<noti(b),sigma> -b-> x" 24 "<b0 andi b1,sigma> -b-> x" 25 "<b0 ori b1,sigma> -b-> x" 26 27 28lemma bexp_iff [rule_format]: 29 "[| b \<in> bexp; sigma: loc -> nat |] 30 ==> \<forall>w. <b,sigma> -b-> w \<longleftrightarrow> B(b,sigma) = w" 31 apply (erule bexp.induct) 32 apply (auto intro!: evalb.intros) 33 done 34 35declare bexp_iff [THEN iffD1, simp] 36 bexp_iff [THEN iffD2, intro!] 37 38lemma com1: "<c,sigma> -c-> sigma' ==> <sigma,sigma'> \<in> C(c)" 39 apply (erule evalc.induct) 40 apply (simp_all (no_asm_simp)) 41 txt \<open>\<open>assign\<close>\<close> 42 apply (simp add: update_type) 43 txt \<open>\<open>comp\<close>\<close> 44 apply fast 45 txt \<open>\<open>while\<close>\<close> 46 apply (erule Gamma_bnd_mono [THEN lfp_unfold, THEN ssubst, OF C_subset]) 47 apply (simp add: Gamma_def) 48 txt \<open>recursive case of \<open>while\<close>\<close> 49 apply (erule Gamma_bnd_mono [THEN lfp_unfold, THEN ssubst, OF C_subset]) 50 apply (auto simp add: Gamma_def) 51 done 52 53declare B_type [intro!] A_type [intro!] 54declare evalc.intros [intro] 55 56 57lemma com2 [rule_format]: "c \<in> com ==> \<forall>x \<in> C(c). <c,fst(x)> -c-> snd(x)" 58 apply (erule com.induct) 59 txt \<open>\<open>skip\<close>\<close> 60 apply force 61 txt \<open>\<open>assign\<close>\<close> 62 apply force 63 txt \<open>\<open>comp\<close>\<close> 64 apply force 65 txt \<open>\<open>while\<close>\<close> 66 apply safe 67 apply simp_all 68 apply (frule Gamma_bnd_mono [OF C_subset], erule Fixedpt.induct, assumption) 69 apply (unfold Gamma_def) 70 apply force 71 txt \<open>\<open>if\<close>\<close> 72 apply auto 73 done 74 75 76subsection \<open>Main theorem\<close> 77 78theorem com_equivalence: 79 "c \<in> com ==> C(c) = {io \<in> (loc->nat) \<times> (loc->nat). <c,fst(io)> -c-> snd(io)}" 80 by (force intro: C_subset [THEN subsetD] elim: com2 dest: com1) 81 82end 83 84