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 "\<lbrakk>a \<in> aexp; sigma: loc -> nat\<rbrakk> |
10 "\<lbrakk>a \<in> aexp; sigma: loc -> nat\<rbrakk> |
11 \<Longrightarrow> \<forall>n. <a,sigma> -a-> n \<longleftrightarrow> A(a,sigma) = n" |
11 \<Longrightarrow> \<forall>n. \<langle>a,sigma\<rangle> -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] |
17 aexp_iff [THEN iffD2, intro!] |
17 aexp_iff [THEN iffD2, intro!] |
18 |
18 |
19 inductive_cases [elim!]: |
19 inductive_cases [elim!]: |
20 "<true,sigma> -b-> x" |
20 "\<langle>true,sigma\<rangle> -b-> x" |
21 "<false,sigma> -b-> x" |
21 "\<langle>false,sigma\<rangle> -b-> x" |
22 "<ROp(f,a0,a1),sigma> -b-> x" |
22 "<ROp(f,a0,a1),sigma> -b-> x" |
23 "<noti(b),sigma> -b-> x" |
23 "<noti(b),sigma> -b-> x" |
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 "\<lbrakk>b \<in> bexp; sigma: loc -> nat\<rbrakk> |
29 "\<lbrakk>b \<in> bexp; sigma: loc -> nat\<rbrakk> |
30 \<Longrightarrow> \<forall>w. <b,sigma> -b-> w \<longleftrightarrow> B(b,sigma) = w" |
30 \<Longrightarrow> \<forall>w. \<langle>b,sigma\<rangle> -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' \<Longrightarrow> <sigma,sigma'> \<in> C(c)" |
38 lemma com1: "\<langle>c,sigma\<rangle> -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> |