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