5 section \<open>Equivalence\<close> |
5 section \<open>Equivalence\<close> |
6 |
6 |
7 theory Equiv imports Denotation Com begin |
7 theory Equiv imports Denotation Com begin |
8 |
8 |
9 lemma aexp_iff [rule_format]: |
9 lemma aexp_iff [rule_format]: |
10 "[| a \<in> aexp; sigma: loc -> nat |] |
10 "\<lbrakk>a \<in> aexp; sigma: loc -> nat\<rbrakk> |
11 ==> \<forall>n. <a,sigma> -a-> n \<longleftrightarrow> A(a,sigma) = n" |
11 \<Longrightarrow> \<forall>n. <a,sigma> -a-> n \<longleftrightarrow> A(a,sigma) = n" |
12 apply (erule aexp.induct) |
12 apply (erule aexp.induct) |
13 apply (force intro!: evala.intros)+ |
13 apply (force intro!: evala.intros)+ |
14 done |
14 done |
15 |
15 |
16 declare aexp_iff [THEN iffD1, simp] |
16 declare aexp_iff [THEN iffD1, simp] |
24 "<b0 andi b1,sigma> -b-> x" |
24 "<b0 andi b1,sigma> -b-> x" |
25 "<b0 ori b1,sigma> -b-> x" |
25 "<b0 ori b1,sigma> -b-> x" |
26 |
26 |
27 |
27 |
28 lemma bexp_iff [rule_format]: |
28 lemma bexp_iff [rule_format]: |
29 "[| b \<in> bexp; sigma: loc -> nat |] |
29 "\<lbrakk>b \<in> bexp; sigma: loc -> nat\<rbrakk> |
30 ==> \<forall>w. <b,sigma> -b-> w \<longleftrightarrow> B(b,sigma) = w" |
30 \<Longrightarrow> \<forall>w. <b,sigma> -b-> w \<longleftrightarrow> B(b,sigma) = w" |
31 apply (erule bexp.induct) |
31 apply (erule bexp.induct) |
32 apply (auto intro!: evalb.intros) |
32 apply (auto intro!: evalb.intros) |
33 done |
33 done |
34 |
34 |
35 declare bexp_iff [THEN iffD1, simp] |
35 declare bexp_iff [THEN iffD1, simp] |
36 bexp_iff [THEN iffD2, intro!] |
36 bexp_iff [THEN iffD2, intro!] |
37 |
37 |
38 lemma com1: "<c,sigma> -c-> sigma' ==> <sigma,sigma'> \<in> C(c)" |
38 lemma com1: "<c,sigma> -c-> sigma' \<Longrightarrow> <sigma,sigma'> \<in> C(c)" |
39 apply (erule evalc.induct) |
39 apply (erule evalc.induct) |
40 apply (simp_all (no_asm_simp)) |
40 apply (simp_all (no_asm_simp)) |
41 txt \<open>\<open>assign\<close>\<close> |
41 txt \<open>\<open>assign\<close>\<close> |
42 apply (simp add: update_type) |
42 apply (simp add: update_type) |
43 txt \<open>\<open>comp\<close>\<close> |
43 txt \<open>\<open>comp\<close>\<close> |
52 |
52 |
53 declare B_type [intro!] A_type [intro!] |
53 declare B_type [intro!] A_type [intro!] |
54 declare evalc.intros [intro] |
54 declare evalc.intros [intro] |
55 |
55 |
56 |
56 |
57 lemma com2 [rule_format]: "c \<in> com ==> \<forall>x \<in> C(c). <c,fst(x)> -c-> snd(x)" |
57 lemma com2 [rule_format]: "c \<in> com \<Longrightarrow> \<forall>x \<in> C(c). <c,fst(x)> -c-> snd(x)" |
58 apply (erule com.induct) |
58 apply (erule com.induct) |
59 txt \<open>\<open>skip\<close>\<close> |
59 txt \<open>\<open>skip\<close>\<close> |
60 apply force |
60 apply force |
61 txt \<open>\<open>assign\<close>\<close> |
61 txt \<open>\<open>assign\<close>\<close> |
62 apply force |
62 apply force |
74 |
74 |
75 |
75 |
76 subsection \<open>Main theorem\<close> |
76 subsection \<open>Main theorem\<close> |
77 |
77 |
78 theorem com_equivalence: |
78 theorem com_equivalence: |
79 "c \<in> com ==> C(c) = {io \<in> (loc->nat) \<times> (loc->nat). <c,fst(io)> -c-> snd(io)}" |
79 "c \<in> com \<Longrightarrow> 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) |
80 by (force intro: C_subset [THEN subsetD] elim: com2 dest: com1) |
81 |
81 |
82 end |
82 end |
83 |
83 |