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