author | wenzelm |
Mon, 21 Aug 2017 17:15:26 +0200 | |
changeset 66475 | d8e0fd64216f |
parent 61798 | 27f3c10b0b50 |
child 76213 | e44d86131648 |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: ZF/IMP/Equiv.thy |
40945 | 2 |
Author: Heiko Loetzbeyer and Robert Sandner, TU München |
482 | 3 |
*) |
4 |
||
60770 | 5 |
section \<open>Equivalence\<close> |
12610 | 6 |
|
16417 | 7 |
theory Equiv imports Denotation Com begin |
12606 | 8 |
|
9 |
lemma aexp_iff [rule_format]: |
|
12610 | 10 |
"[| a \<in> aexp; sigma: loc -> nat |] |
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
40945
diff
changeset
|
11 |
==> \<forall>n. <a,sigma> -a-> n \<longleftrightarrow> A(a,sigma) = n" |
12610 | 12 |
apply (erule aexp.induct) |
13 |
apply (force intro!: evala.intros)+ |
|
14 |
done |
|
12606 | 15 |
|
16 |
declare aexp_iff [THEN iffD1, simp] |
|
17 |
aexp_iff [THEN iffD2, intro!] |
|
18 |
||
12610 | 19 |
inductive_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" |
|
12606 | 26 |
|
27 |
||
28 |
lemma bexp_iff [rule_format]: |
|
12610 | 29 |
"[| b \<in> bexp; sigma: loc -> nat |] |
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
40945
diff
changeset
|
30 |
==> \<forall>w. <b,sigma> -b-> w \<longleftrightarrow> B(b,sigma) = w" |
12610 | 31 |
apply (erule bexp.induct) |
32 |
apply (auto intro!: evalb.intros) |
|
33 |
done |
|
12606 | 34 |
|
35 |
declare bexp_iff [THEN iffD1, simp] |
|
36 |
bexp_iff [THEN iffD2, intro!] |
|
37 |
||
38 |
lemma com1: "<c,sigma> -c-> sigma' ==> <sigma,sigma'> \<in> C(c)" |
|
12610 | 39 |
apply (erule evalc.induct) |
13612 | 40 |
apply (simp_all (no_asm_simp)) |
61798 | 41 |
txt \<open>\<open>assign\<close>\<close> |
12610 | 42 |
apply (simp add: update_type) |
61798 | 43 |
txt \<open>\<open>comp\<close>\<close> |
12610 | 44 |
apply fast |
61798 | 45 |
txt \<open>\<open>while\<close>\<close> |
12610 | 46 |
apply (erule Gamma_bnd_mono [THEN lfp_unfold, THEN ssubst, OF C_subset]) |
47 |
apply (simp add: Gamma_def) |
|
61798 | 48 |
txt \<open>recursive case of \<open>while\<close>\<close> |
12610 | 49 |
apply (erule Gamma_bnd_mono [THEN lfp_unfold, THEN ssubst, OF C_subset]) |
50 |
apply (auto simp add: Gamma_def) |
|
51 |
done |
|
12606 | 52 |
|
53 |
declare B_type [intro!] A_type [intro!] |
|
54 |
declare evalc.intros [intro] |
|
55 |
||
56 |
||
57 |
lemma com2 [rule_format]: "c \<in> com ==> \<forall>x \<in> C(c). <c,fst(x)> -c-> snd(x)" |
|
12610 | 58 |
apply (erule com.induct) |
61798 | 59 |
txt \<open>\<open>skip\<close>\<close> |
12610 | 60 |
apply force |
61798 | 61 |
txt \<open>\<open>assign\<close>\<close> |
12610 | 62 |
apply force |
61798 | 63 |
txt \<open>\<open>comp\<close>\<close> |
12610 | 64 |
apply force |
61798 | 65 |
txt \<open>\<open>while\<close>\<close> |
12610 | 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 |
|
61798 | 71 |
txt \<open>\<open>if\<close>\<close> |
12610 | 72 |
apply auto |
73 |
done |
|
12606 | 74 |
|
75 |
||
60770 | 76 |
subsection \<open>Main theorem\<close> |
12606 | 77 |
|
12610 | 78 |
theorem 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) |
|
12606 | 81 |
|
82 |
end |
|
83 |