43 Evala.mk_cases Aexp.con_defs "<Op2(f,a1,a2),sigma> -a-> i" |
43 Evala.mk_cases Aexp.con_defs "<Op2(f,a1,a2),sigma> -a-> i" |
44 ]; |
44 ]; |
45 |
45 |
46 |
46 |
47 val prems = goal Equiv.thy "[| a: aexp; sigma: loc -> nat |] ==> \ |
47 val prems = goal Equiv.thy "[| a: aexp; sigma: loc -> nat |] ==> \ |
48 \ <a,sigma> -a-> n <-> n = A(a,sigma) "; |
48 \ <a,sigma> -a-> n <-> A(a,sigma) = n"; |
49 |
49 |
50 by (res_inst_tac [("x","n")] spec 1); (* quantify n *) |
50 by (res_inst_tac [("x","n")] spec 1); (* quantify n *) |
51 by (res_inst_tac [("x","a")] Aexp.induct 1); (* struct. ind. *) |
51 by (res_inst_tac [("x","a")] Aexp.induct 1); (* struct. ind. *) |
52 by (resolve_tac prems 1); (* type prem. *) |
52 by (resolve_tac prems 1); (* type prem. *) |
53 by (safe_tac ZF_cs); (* allI,-->,<-- *) |
|
54 by (rewrite_goals_tac A_rewrite_rules); (* rewr. Den. *) |
53 by (rewrite_goals_tac A_rewrite_rules); (* rewr. Den. *) |
55 by (TRYALL (fast_tac (ZF_cs addSIs (Evala.intrs@prems)) )); (* <== *) |
54 by (ALLGOALS (fast_tac (ZF_cs addSIs (Evala.intrs@prems) |
56 by (TRYALL (fast_tac (ZF_cs addSEs Aexp_elim_cases))); (* ==> *) |
55 addSEs Aexp_elim_cases))); |
57 |
56 |
58 val aexp_iff = result(); |
57 val aexp_iff = result(); |
59 |
58 |
60 |
59 val aexp1 = prove_goal Equiv.thy (* destr. rule *) |
61 val Aexp_rew_rules_cs = ZF_cs addIs op_type_intrs@[aexp_iff RS iffD1 RS sym]; |
60 "[| <a,sigma> -a-> n; a: aexp; sigma: loc -> nat |] ==> A(a,sigma) = n" |
62 |
61 (fn prems => [fast_tac (ZF_cs addSIs ((aexp_iff RS iffD1)::prems)) 1]); |
63 val aexp1 = prove_goal Equiv.thy (* elim the prems *) |
|
64 "<a,sigma> -a-> n ==> A(a,sigma) = n" (* destruction rule *) |
|
65 (fn prems => [(fast_tac (Aexp_rew_rules_cs addSIs prems) 1)]); |
|
66 |
62 |
67 val aexp2 = aexp_iff RS iffD2; |
63 val aexp2 = aexp_iff RS iffD2; |
68 |
64 |
69 |
65 |
70 val Bexp_elim_cases = |
66 val Bexp_elim_cases = |
77 Evalb.mk_cases Bexp.con_defs "<b0 ori b1,sigma> -b-> x" |
73 Evalb.mk_cases Bexp.con_defs "<b0 ori b1,sigma> -b-> x" |
78 ]; |
74 ]; |
79 |
75 |
80 |
76 |
81 val prems = goal Equiv.thy "[| b: bexp; sigma: loc -> nat |] ==> \ |
77 val prems = goal Equiv.thy "[| b: bexp; sigma: loc -> nat |] ==> \ |
82 \ <b,sigma> -b-> w <-> w = B(b,sigma) "; |
78 \ <b,sigma> -b-> w <-> B(b,sigma) = w"; |
83 |
79 |
84 by (res_inst_tac [("x","w")] spec 1); (* quantify w *) |
80 by (res_inst_tac [("x","w")] spec 1); (* quantify w *) |
85 by (res_inst_tac [("x","b")] Bexp.induct 1); (* struct. ind. *) |
81 by (res_inst_tac [("x","b")] Bexp.induct 1); (* struct. ind. *) |
86 by (resolve_tac prems 1); (* type prem. *) |
82 by (resolve_tac prems 1); (* type prem. *) |
87 by (safe_tac ZF_cs); (* allI,-->,<-- *) |
83 by (rewrite_goals_tac B_rewrite_rules); (* rewr. Den. *) |
88 by (rewrite_goals_tac B_rewrite_rules); (* rewr. Den. *) |
84 by (ALLGOALS (fast_tac (ZF_cs addSIs (Evalb.intrs@prems@[aexp2]) |
89 by (TRYALL (fast_tac (* <== *) |
85 addSEs Bexp_elim_cases addSDs [aexp1]))); |
90 (ZF_cs addSIs (Evalb.intrs@prems@[aexp2])) )); |
|
91 by (TRYALL (fast_tac ((ZF_cs addSDs [aexp1]) addSEs Bexp_elim_cases))); |
|
92 (* ==> *) |
|
93 |
86 |
94 val bexp_iff = result(); |
87 val bexp_iff = result(); |
95 |
88 |
96 |
89 |
97 val Bexp_rew_rules_cs = ZF_cs addIs op_type_intrs@[bexp_iff RS iffD1 RS sym]; |
90 val bexp1 = prove_goal Equiv.thy |
|
91 "[| <b,sigma> -b-> w; b : bexp; sigma : loc -> nat |] ==> B(b,sigma) = w" |
|
92 (fn prems => [fast_tac (ZF_cs addIs ((bexp_iff RS iffD1)::prems)) 1]); |
98 |
93 |
99 val bexp1 = prove_goal Equiv.thy |
94 val bexp2 = bexp_iff RS iffD2; |
100 "<b,sigma> -b-> w ==> B(b,sigma) = w" |
|
101 (fn prems => [(fast_tac (Bexp_rew_rules_cs addSIs prems) 1)]); |
|
102 |
95 |
103 val bexp2 = prove_goal Equiv.thy |
96 goal Equiv.thy "!!c. <c,sigma> -c-> sigma' ==> <sigma,sigma'> : C(c)"; |
104 "[| B(b,sigma) = w; b : bexp; sigma : loc -> nat |] ==> <b,sigma> -b-> w" |
|
105 (fn prems => |
|
106 [(cut_facts_tac prems 1), |
|
107 (fast_tac (ZF_cs addIs ([bexp_iff RS iffD2])) 1)]); |
|
108 |
|
109 |
|
110 |
|
111 val prems = goal Equiv.thy |
|
112 "<c,sigma> -c-> sigma' ==> <sigma,sigma'> : C(c)"; |
|
113 by (cut_facts_tac prems 1); |
|
114 |
97 |
115 (* start with rule induction *) |
98 (* start with rule induction *) |
116 be (Evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1; |
99 be (Evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1; |
117 |
100 |
118 by (rewrite_tac (Gamma_def::C_rewrite_rules)); |
101 by (rewrite_tac (Gamma_def::C_rewrite_rules)); |
128 (* if *) |
111 (* if *) |
129 by (fast_tac (ZF_cs addSIs [bexp1] addIs [(fst_conv RS ssubst)]) 1); |
112 by (fast_tac (ZF_cs addSIs [bexp1] addIs [(fst_conv RS ssubst)]) 1); |
130 by (fast_tac (ZF_cs addSIs [bexp1] addIs [(fst_conv RS ssubst)]) 1); |
113 by (fast_tac (ZF_cs addSIs [bexp1] addIs [(fst_conv RS ssubst)]) 1); |
131 |
114 |
132 (* while *) |
115 (* while *) |
133 by (etac (rewrite_rule [Gamma_def] (Gamma_bnd_mono RS lfp_Tarski RS ssubst)) 1); |
116 by (etac (rewrite_rule [Gamma_def] (Gamma_bnd_mono RS lfp_Tarski RS ssubst))1); |
134 by (fast_tac (comp_cs addSIs [bexp1,idI]@Evalb_type_intrs |
117 by (fast_tac (comp_cs addSIs [bexp1,idI]@Evalb_type_intrs |
135 addIs [(fst_conv RS ssubst)]) 1); |
118 addIs [(fst_conv RS ssubst)]) 1); |
136 |
119 |
137 by (etac (rewrite_rule [Gamma_def] (Gamma_bnd_mono RS lfp_Tarski RS ssubst)) 1); |
120 by (etac (rewrite_rule [Gamma_def] (Gamma_bnd_mono RS lfp_Tarski RS ssubst))1); |
138 by (fast_tac (comp_cs addSIs [bexp1,compI]@Evalb_type_intrs |
121 by (fast_tac (comp_cs addSIs [bexp1,compI]@Evalb_type_intrs |
139 addIs [(fst_conv RS ssubst)]) 1); |
122 addIs [(fst_conv RS ssubst)]) 1); |
140 |
123 |
141 val com1 = result(); |
124 val com1 = result(); |
142 |
125 |
144 val com_cs = ZF_cs addSIs [aexp2,bexp2,B_type,A_type] |
127 val com_cs = ZF_cs addSIs [aexp2,bexp2,B_type,A_type] |
145 addIs Evalc.intrs |
128 addIs Evalc.intrs |
146 addSEs [idE,compE] |
129 addSEs [idE,compE] |
147 addEs [C_type,C_type_fst]; |
130 addEs [C_type,C_type_fst]; |
148 |
131 |
149 val [prem] = goal Equiv.thy "c : com ==> ALL x. x:C(c) \ |
132 goal Equiv.thy "!!c. c : com ==> ALL io:C(c). <c,fst(io)> -c-> snd(io)"; |
150 \ --> <c,fst(x)> -c-> snd(x)"; |
|
151 |
133 |
152 br (prem RS Com.induct) 1; |
134 be Com.induct 1; |
153 by (rewrite_tac C_rewrite_rules); |
135 by (rewrite_tac C_rewrite_rules); |
154 by (safe_tac com_cs); |
136 by (safe_tac com_cs); |
155 by (ALLGOALS (asm_full_simp_tac ZF_ss)); |
137 by (ALLGOALS (asm_full_simp_tac ZF_ss)); |
156 |
138 |
157 (* skip *) |
139 (* skip *) |
159 |
141 |
160 (* assign *) |
142 (* assign *) |
161 by (fast_tac com_cs 1); |
143 by (fast_tac com_cs 1); |
162 |
144 |
163 (* comp *) |
145 (* comp *) |
164 by (REPEAT (EVERY [(etac allE 1),(etac impE 1),(atac 1)])); |
146 by (REPEAT (EVERY [dtac bspec 1, atac 1])); |
165 by (asm_full_simp_tac ZF_ss 1); |
147 by (asm_full_simp_tac ZF_ss 1); |
166 by (fast_tac com_cs 1); |
148 by (fast_tac com_cs 1); |
167 |
149 |
168 (* while *) |
150 (* while *) |
169 by (EVERY [(forward_tac [Gamma_bnd_mono] 1),(etac induct 1),(atac 1)]); |
151 by (EVERY [forward_tac [Gamma_bnd_mono] 1, etac induct 1,(atac 1)]); |
170 by (rewrite_goals_tac [Gamma_def]); |
152 by (rewrite_goals_tac [Gamma_def]); |
171 by (safe_tac com_cs); |
153 by (safe_tac com_cs); |
172 by (EVERY [(etac allE 1),(etac impE 1),(atac 1)]); |
154 by (EVERY [dtac bspec 1, atac 1]); |
173 by (ALLGOALS (asm_full_simp_tac ZF_ss)); |
155 by (ALLGOALS (asm_full_simp_tac ZF_ss)); |
174 |
156 |
175 (* while und if *) |
157 (* while und if *) |
176 by (ALLGOALS (fast_tac com_cs)); |
158 by (ALLGOALS (fast_tac com_cs)); |
177 val com2 = result(); |
159 val com2 = result(); |
178 |
160 |
179 |
161 |
180 (**** Beweis der Aequivalenz ****) |
162 (**** Beweis der Aequivalenz ****) |
181 |
163 |
182 val com_iff_cs = ZF_cs addIs [C_subset RS subsetD] |
164 val com_iff_cs = ZF_cs addIs [C_subset RS subsetD] |
183 addEs [com2 RS spec RS impE] |
165 addEs [com2 RS bspec] |
184 addDs [com1]; |
166 addDs [com1]; |
185 |
167 |
186 goal Equiv.thy "ALL c:com.\ |
168 goal Equiv.thy "ALL c:com.\ |
187 \ C(c) = {io:(loc->nat)*(loc->nat). <c,fst(io)> -c-> snd(io)}"; |
169 \ C(c) = {io:(loc->nat)*(loc->nat). <c,fst(io)> -c-> snd(io)}"; |
188 by (rtac ballI 1); |
170 by (rtac ballI 1); |