11 (* ------------------------------------------------------------------------*) |
11 (* ------------------------------------------------------------------------*) |
12 (* The isomorphisms dnat_rep_iso and dnat_abs_iso are strict *) |
12 (* The isomorphisms dnat_rep_iso and dnat_abs_iso are strict *) |
13 (* ------------------------------------------------------------------------*) |
13 (* ------------------------------------------------------------------------*) |
14 |
14 |
15 val dnat_iso_strict = dnat_rep_iso RS (dnat_abs_iso RS |
15 val dnat_iso_strict = dnat_rep_iso RS (dnat_abs_iso RS |
16 (allI RSN (2,allI RS iso_strict))); |
16 (allI RSN (2,allI RS iso_strict))); |
17 |
17 |
18 val dnat_rews = [dnat_iso_strict RS conjunct1, |
18 val dnat_rews = [dnat_iso_strict RS conjunct1, |
19 dnat_iso_strict RS conjunct2]; |
19 dnat_iso_strict RS conjunct2]; |
20 |
20 |
21 (* ------------------------------------------------------------------------*) |
21 (* ------------------------------------------------------------------------*) |
22 (* Properties of dnat_copy *) |
22 (* Properties of dnat_copy *) |
23 (* ------------------------------------------------------------------------*) |
23 (* ------------------------------------------------------------------------*) |
24 |
24 |
25 fun prover defs thm = prove_goalw Dnat.thy defs thm |
25 fun prover defs thm = prove_goalw Dnat.thy defs thm |
26 (fn prems => |
26 (fn prems => |
27 [ |
27 [ |
28 (cut_facts_tac prems 1), |
28 (cut_facts_tac prems 1), |
29 (asm_simp_tac (!simpset addsimps |
29 (asm_simp_tac (!simpset addsimps |
30 (dnat_rews @ [dnat_abs_iso,dnat_rep_iso])) 1) |
30 (dnat_rews @ [dnat_abs_iso,dnat_rep_iso])) 1) |
31 ]); |
31 ]); |
32 |
32 |
33 val dnat_copy = |
33 val dnat_copy = |
34 [ |
34 [ |
35 prover [dnat_copy_def] "dnat_copy`f`UU=UU", |
35 prover [dnat_copy_def] "dnat_copy`f`UU=UU", |
36 prover [dnat_copy_def,dzero_def] "dnat_copy`f`dzero= dzero", |
36 prover [dnat_copy_def,dzero_def] "dnat_copy`f`dzero= dzero", |
37 prover [dnat_copy_def,dsucc_def] |
37 prover [dnat_copy_def,dsucc_def] |
38 "n~=UU ==> dnat_copy`f`(dsucc`n) = dsucc`(f`n)" |
38 "n~=UU ==> dnat_copy`f`(dsucc`n) = dsucc`(f`n)" |
39 ]; |
39 ]; |
40 |
40 |
41 val dnat_rews = dnat_copy @ dnat_rews; |
41 val dnat_rews = dnat_copy @ dnat_rews; |
42 |
42 |
43 (* ------------------------------------------------------------------------*) |
43 (* ------------------------------------------------------------------------*) |
44 (* Exhaustion and elimination for dnat *) |
44 (* Exhaustion and elimination for dnat *) |
45 (* ------------------------------------------------------------------------*) |
45 (* ------------------------------------------------------------------------*) |
46 |
46 |
47 qed_goalw "Exh_dnat" Dnat.thy [dsucc_def,dzero_def] |
47 qed_goalw "Exh_dnat" Dnat.thy [dsucc_def,dzero_def] |
48 "n = UU | n = dzero | (? x . x~=UU & n = dsucc`x)" |
48 "n = UU | n = dzero | (? x . x~=UU & n = dsucc`x)" |
49 (fn prems => |
49 (fn prems => |
50 [ |
50 [ |
51 (Simp_tac 1), |
51 (Simp_tac 1), |
52 (rtac (dnat_rep_iso RS subst) 1), |
52 (rtac (dnat_rep_iso RS subst) 1), |
53 (res_inst_tac [("p","dnat_rep`n")] ssumE 1), |
53 (res_inst_tac [("p","dnat_rep`n")] ssumE 1), |
54 (rtac disjI1 1), |
54 (rtac disjI1 1), |
55 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
55 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
56 (rtac (disjI1 RS disjI2) 1), |
56 (rtac (disjI1 RS disjI2) 1), |
57 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
57 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
58 (res_inst_tac [("p","x")] oneE 1), |
58 (res_inst_tac [("p","x")] oneE 1), |
59 (contr_tac 1), |
59 (contr_tac 1), |
60 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
60 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
61 (rtac (disjI2 RS disjI2) 1), |
61 (rtac (disjI2 RS disjI2) 1), |
62 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
62 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
63 (fast_tac HOL_cs 1) |
63 (fast_tac HOL_cs 1) |
64 ]); |
64 ]); |
65 |
65 |
66 qed_goal "dnatE" Dnat.thy |
66 qed_goal "dnatE" Dnat.thy |
67 "[| n=UU ==> Q; n=dzero ==> Q; !!x.[|n=dsucc`x;x~=UU|]==>Q|]==>Q" |
67 "[| n=UU ==> Q; n=dzero ==> Q; !!x.[|n=dsucc`x;x~=UU|]==>Q|]==>Q" |
68 (fn prems => |
68 (fn prems => |
69 [ |
69 [ |
70 (rtac (Exh_dnat RS disjE) 1), |
70 (rtac (Exh_dnat RS disjE) 1), |
71 (eresolve_tac prems 1), |
71 (eresolve_tac prems 1), |
72 (etac disjE 1), |
72 (etac disjE 1), |
73 (eresolve_tac prems 1), |
73 (eresolve_tac prems 1), |
74 (REPEAT (etac exE 1)), |
74 (REPEAT (etac exE 1)), |
75 (resolve_tac prems 1), |
75 (resolve_tac prems 1), |
76 (fast_tac HOL_cs 1), |
76 (fast_tac HOL_cs 1), |
77 (fast_tac HOL_cs 1) |
77 (fast_tac HOL_cs 1) |
78 ]); |
78 ]); |
79 |
79 |
80 (* ------------------------------------------------------------------------*) |
80 (* ------------------------------------------------------------------------*) |
81 (* Properties of dnat_when *) |
81 (* Properties of dnat_when *) |
82 (* ------------------------------------------------------------------------*) |
82 (* ------------------------------------------------------------------------*) |
83 |
83 |
84 fun prover defs thm = prove_goalw Dnat.thy defs thm |
84 fun prover defs thm = prove_goalw Dnat.thy defs thm |
85 (fn prems => |
85 (fn prems => |
86 [ |
86 [ |
87 (cut_facts_tac prems 1), |
87 (cut_facts_tac prems 1), |
88 (asm_simp_tac (!simpset addsimps |
88 (asm_simp_tac (!simpset addsimps |
89 (dnat_rews @ [dnat_abs_iso,dnat_rep_iso])) 1) |
89 (dnat_rews @ [dnat_abs_iso,dnat_rep_iso])) 1) |
90 ]); |
90 ]); |
91 |
91 |
92 |
92 |
93 val dnat_when = [ |
93 val dnat_when = [ |
94 prover [dnat_when_def] "dnat_when`c`f`UU=UU", |
94 prover [dnat_when_def] "dnat_when`c`f`UU=UU", |
95 prover [dnat_when_def,dzero_def] "dnat_when`c`f`dzero=c", |
95 prover [dnat_when_def,dzero_def] "dnat_when`c`f`dzero=c", |
96 prover [dnat_when_def,dsucc_def] |
96 prover [dnat_when_def,dsucc_def] |
97 "n~=UU ==> dnat_when`c`f`(dsucc`n)=f`n" |
97 "n~=UU ==> dnat_when`c`f`(dsucc`n)=f`n" |
98 ]; |
98 ]; |
99 |
99 |
100 val dnat_rews = dnat_when @ dnat_rews; |
100 val dnat_rews = dnat_when @ dnat_rews; |
101 |
101 |
102 (* ------------------------------------------------------------------------*) |
102 (* ------------------------------------------------------------------------*) |
103 (* Rewrites for discriminators and selectors *) |
103 (* Rewrites for discriminators and selectors *) |
104 (* ------------------------------------------------------------------------*) |
104 (* ------------------------------------------------------------------------*) |
105 |
105 |
106 fun prover defs thm = prove_goalw Dnat.thy defs thm |
106 fun prover defs thm = prove_goalw Dnat.thy defs thm |
107 (fn prems => |
107 (fn prems => |
108 [ |
108 [ |
109 (simp_tac (!simpset addsimps dnat_rews) 1) |
109 (simp_tac (!simpset addsimps dnat_rews) 1) |
110 ]); |
110 ]); |
111 |
111 |
112 val dnat_discsel = [ |
112 val dnat_discsel = [ |
113 prover [is_dzero_def] "is_dzero`UU=UU", |
113 prover [is_dzero_def] "is_dzero`UU=UU", |
114 prover [is_dsucc_def] "is_dsucc`UU=UU", |
114 prover [is_dsucc_def] "is_dsucc`UU=UU", |
115 prover [dpred_def] "dpred`UU=UU" |
115 prover [dpred_def] "dpred`UU=UU" |
116 ]; |
116 ]; |
117 |
117 |
118 |
118 |
119 fun prover defs thm = prove_goalw Dnat.thy defs thm |
119 fun prover defs thm = prove_goalw Dnat.thy defs thm |
120 (fn prems => |
120 (fn prems => |
121 [ |
121 [ |
122 (cut_facts_tac prems 1), |
122 (cut_facts_tac prems 1), |
123 (asm_simp_tac (!simpset addsimps dnat_rews) 1) |
123 (asm_simp_tac (!simpset addsimps dnat_rews) 1) |
124 ]); |
124 ]); |
125 |
125 |
126 val dnat_discsel = [ |
126 val dnat_discsel = [ |
127 prover [is_dzero_def] "is_dzero`dzero=TT", |
127 prover [is_dzero_def] "is_dzero`dzero=TT", |
128 prover [is_dzero_def] "n~=UU ==>is_dzero`(dsucc`n)=FF", |
128 prover [is_dzero_def] "n~=UU ==>is_dzero`(dsucc`n)=FF", |
129 prover [is_dsucc_def] "is_dsucc`dzero=FF", |
129 prover [is_dsucc_def] "is_dsucc`dzero=FF", |
130 prover [is_dsucc_def] "n~=UU ==> is_dsucc`(dsucc`n)=TT", |
130 prover [is_dsucc_def] "n~=UU ==> is_dsucc`(dsucc`n)=TT", |
131 prover [dpred_def] "dpred`dzero=UU", |
131 prover [dpred_def] "dpred`dzero=UU", |
132 prover [dpred_def] "n~=UU ==> dpred`(dsucc`n)=n" |
132 prover [dpred_def] "n~=UU ==> dpred`(dsucc`n)=n" |
133 ] @ dnat_discsel; |
133 ] @ dnat_discsel; |
134 |
134 |
135 val dnat_rews = dnat_discsel @ dnat_rews; |
135 val dnat_rews = dnat_discsel @ dnat_rews; |
136 |
136 |
137 (* ------------------------------------------------------------------------*) |
137 (* ------------------------------------------------------------------------*) |
138 (* Definedness and strictness *) |
138 (* Definedness and strictness *) |
139 (* ------------------------------------------------------------------------*) |
139 (* ------------------------------------------------------------------------*) |
140 |
140 |
141 fun prover contr thm = prove_goal Dnat.thy thm |
141 fun prover contr thm = prove_goal Dnat.thy thm |
142 (fn prems => |
142 (fn prems => |
143 [ |
143 [ |
144 (res_inst_tac [("P1",contr)] classical3 1), |
144 (res_inst_tac [("P1",contr)] classical3 1), |
145 (simp_tac (!simpset addsimps dnat_rews) 1), |
145 (simp_tac (!simpset addsimps dnat_rews) 1), |
146 (dtac sym 1), |
146 (dtac sym 1), |
147 (Asm_simp_tac 1), |
147 (Asm_simp_tac 1), |
148 (simp_tac (!simpset addsimps (prems @ dnat_rews)) 1) |
148 (simp_tac (!simpset addsimps (prems @ dnat_rews)) 1) |
149 ]); |
149 ]); |
150 |
150 |
151 val dnat_constrdef = [ |
151 val dnat_constrdef = [ |
152 prover "is_dzero`UU ~= UU" "dzero~=UU", |
152 prover "is_dzero`UU ~= UU" "dzero~=UU", |
153 prover "is_dsucc`UU ~= UU" "n~=UU ==> dsucc`n~=UU" |
153 prover "is_dsucc`UU ~= UU" "n~=UU ==> dsucc`n~=UU" |
154 ]; |
154 ]; |
155 |
155 |
156 |
156 |
157 fun prover defs thm = prove_goalw Dnat.thy defs thm |
157 fun prover defs thm = prove_goalw Dnat.thy defs thm |
158 (fn prems => |
158 (fn prems => |
159 [ |
159 [ |
160 (simp_tac (!simpset addsimps dnat_rews) 1) |
160 (simp_tac (!simpset addsimps dnat_rews) 1) |
161 ]); |
161 ]); |
162 |
162 |
163 val dnat_constrdef = [ |
163 val dnat_constrdef = [ |
164 prover [dsucc_def] "dsucc`UU=UU" |
164 prover [dsucc_def] "dsucc`UU=UU" |
165 ] @ dnat_constrdef; |
165 ] @ dnat_constrdef; |
166 |
166 |
167 val dnat_rews = dnat_constrdef @ dnat_rews; |
167 val dnat_rews = dnat_constrdef @ dnat_rews; |
168 |
168 |
169 |
169 |
170 (* ------------------------------------------------------------------------*) |
170 (* ------------------------------------------------------------------------*) |
171 (* Distinctness wrt. << and = *) |
171 (* Distinctness wrt. << and = *) |
172 (* ------------------------------------------------------------------------*) |
172 (* ------------------------------------------------------------------------*) |
173 |
173 |
174 val temp = prove_goal Dnat.thy "~dzero << dsucc`n" |
174 val temp = prove_goal Dnat.thy "~dzero << dsucc`n" |
175 (fn prems => |
175 (fn prems => |
176 [ |
176 [ |
177 (res_inst_tac [("P1","TT << FF")] classical3 1), |
177 (res_inst_tac [("P1","TT << FF")] classical3 1), |
178 (resolve_tac dist_less_tr 1), |
178 (resolve_tac dist_less_tr 1), |
179 (dres_inst_tac [("fo5","is_dzero")] monofun_cfun_arg 1), |
179 (dres_inst_tac [("fo5","is_dzero")] monofun_cfun_arg 1), |
180 (etac box_less 1), |
180 (etac box_less 1), |
181 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
181 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
182 (res_inst_tac [("Q","n=UU")] classical2 1), |
182 (res_inst_tac [("Q","n=UU")] classical2 1), |
183 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
183 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
184 (asm_simp_tac (!simpset addsimps dnat_rews) 1) |
184 (asm_simp_tac (!simpset addsimps dnat_rews) 1) |
185 ]); |
185 ]); |
186 |
186 |
187 val dnat_dist_less = [temp]; |
187 val dnat_dist_less = [temp]; |
188 |
188 |
189 val temp = prove_goal Dnat.thy "n~=UU ==> ~dsucc`n << dzero" |
189 val temp = prove_goal Dnat.thy "n~=UU ==> ~dsucc`n << dzero" |
190 (fn prems => |
190 (fn prems => |
191 [ |
191 [ |
192 (cut_facts_tac prems 1), |
192 (cut_facts_tac prems 1), |
193 (res_inst_tac [("P1","TT << FF")] classical3 1), |
193 (res_inst_tac [("P1","TT << FF")] classical3 1), |
194 (resolve_tac dist_less_tr 1), |
194 (resolve_tac dist_less_tr 1), |
195 (dres_inst_tac [("fo5","is_dsucc")] monofun_cfun_arg 1), |
195 (dres_inst_tac [("fo5","is_dsucc")] monofun_cfun_arg 1), |
196 (etac box_less 1), |
196 (etac box_less 1), |
197 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
197 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
198 (asm_simp_tac (!simpset addsimps dnat_rews) 1) |
198 (asm_simp_tac (!simpset addsimps dnat_rews) 1) |
199 ]); |
199 ]); |
200 |
200 |
201 val dnat_dist_less = temp::dnat_dist_less; |
201 val dnat_dist_less = temp::dnat_dist_less; |
202 |
202 |
203 val temp = prove_goal Dnat.thy "dzero ~= dsucc`n" |
203 val temp = prove_goal Dnat.thy "dzero ~= dsucc`n" |
204 (fn prems => |
204 (fn prems => |
205 [ |
205 [ |
206 (res_inst_tac [("Q","n=UU")] classical2 1), |
206 (res_inst_tac [("Q","n=UU")] classical2 1), |
207 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
207 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
208 (res_inst_tac [("P1","TT = FF")] classical3 1), |
208 (res_inst_tac [("P1","TT = FF")] classical3 1), |
209 (resolve_tac dist_eq_tr 1), |
209 (resolve_tac dist_eq_tr 1), |
210 (dres_inst_tac [("f","is_dzero")] cfun_arg_cong 1), |
210 (dres_inst_tac [("f","is_dzero")] cfun_arg_cong 1), |
211 (etac box_equals 1), |
211 (etac box_equals 1), |
212 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
212 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
213 (asm_simp_tac (!simpset addsimps dnat_rews) 1) |
213 (asm_simp_tac (!simpset addsimps dnat_rews) 1) |
214 ]); |
214 ]); |
215 |
215 |
216 val dnat_dist_eq = [temp, temp RS not_sym]; |
216 val dnat_dist_eq = [temp, temp RS not_sym]; |
217 |
217 |
218 val dnat_rews = dnat_dist_less @ dnat_dist_eq @ dnat_rews; |
218 val dnat_rews = dnat_dist_less @ dnat_dist_eq @ dnat_rews; |
219 |
219 |
220 (* ------------------------------------------------------------------------*) |
220 (* ------------------------------------------------------------------------*) |
221 (* Invertibility *) |
221 (* Invertibility *) |
222 (* ------------------------------------------------------------------------*) |
222 (* ------------------------------------------------------------------------*) |
223 |
223 |
224 val dnat_invert = |
224 val dnat_invert = |
225 [ |
225 [ |
226 prove_goal Dnat.thy |
226 prove_goal Dnat.thy |
227 "[|x1~=UU; y1~=UU; dsucc`x1 << dsucc`y1 |] ==> x1<< y1" |
227 "[|x1~=UU; y1~=UU; dsucc`x1 << dsucc`y1 |] ==> x1<< y1" |
228 (fn prems => |
228 (fn prems => |
229 [ |
229 [ |
230 (cut_facts_tac prems 1), |
230 (cut_facts_tac prems 1), |
231 (dres_inst_tac [("fo5","dnat_when`c`(LAM x.x)")] monofun_cfun_arg 1), |
231 (dres_inst_tac [("fo5","dnat_when`c`(LAM x.x)")] monofun_cfun_arg 1), |
232 (etac box_less 1), |
232 (etac box_less 1), |
233 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
233 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
234 (asm_simp_tac (!simpset addsimps dnat_rews) 1) |
234 (asm_simp_tac (!simpset addsimps dnat_rews) 1) |
235 ]) |
235 ]) |
236 ]; |
236 ]; |
237 |
237 |
238 (* ------------------------------------------------------------------------*) |
238 (* ------------------------------------------------------------------------*) |
239 (* Injectivity *) |
239 (* Injectivity *) |
240 (* ------------------------------------------------------------------------*) |
240 (* ------------------------------------------------------------------------*) |
241 |
241 |
242 val dnat_inject = |
242 val dnat_inject = |
243 [ |
243 [ |
244 prove_goal Dnat.thy |
244 prove_goal Dnat.thy |
245 "[|x1~=UU; y1~=UU; dsucc`x1 = dsucc`y1 |] ==> x1= y1" |
245 "[|x1~=UU; y1~=UU; dsucc`x1 = dsucc`y1 |] ==> x1= y1" |
246 (fn prems => |
246 (fn prems => |
247 [ |
247 [ |
248 (cut_facts_tac prems 1), |
248 (cut_facts_tac prems 1), |
249 (dres_inst_tac [("f","dnat_when`c`(LAM x.x)")] cfun_arg_cong 1), |
249 (dres_inst_tac [("f","dnat_when`c`(LAM x.x)")] cfun_arg_cong 1), |
250 (etac box_equals 1), |
250 (etac box_equals 1), |
251 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
251 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
252 (asm_simp_tac (!simpset addsimps dnat_rews) 1) |
252 (asm_simp_tac (!simpset addsimps dnat_rews) 1) |
253 ]) |
253 ]) |
254 ]; |
254 ]; |
255 |
255 |
256 (* ------------------------------------------------------------------------*) |
256 (* ------------------------------------------------------------------------*) |
257 (* definedness for discriminators and selectors *) |
257 (* definedness for discriminators and selectors *) |
258 (* ------------------------------------------------------------------------*) |
258 (* ------------------------------------------------------------------------*) |
259 |
259 |
260 |
260 |
261 fun prover thm = prove_goal Dnat.thy thm |
261 fun prover thm = prove_goal Dnat.thy thm |
262 (fn prems => |
262 (fn prems => |
263 [ |
263 [ |
264 (cut_facts_tac prems 1), |
264 (cut_facts_tac prems 1), |
265 (rtac dnatE 1), |
265 (rtac dnatE 1), |
266 (contr_tac 1), |
266 (contr_tac 1), |
267 (REPEAT (asm_simp_tac (!simpset addsimps dnat_rews) 1)) |
267 (REPEAT (asm_simp_tac (!simpset addsimps dnat_rews) 1)) |
268 ]); |
268 ]); |
269 |
269 |
270 val dnat_discsel_def = |
270 val dnat_discsel_def = |
271 [ |
271 [ |
272 prover "n~=UU ==> is_dzero`n ~= UU", |
272 prover "n~=UU ==> is_dzero`n ~= UU", |
273 prover "n~=UU ==> is_dsucc`n ~= UU" |
273 prover "n~=UU ==> is_dsucc`n ~= UU" |
274 ]; |
274 ]; |
275 |
275 |
276 val dnat_rews = dnat_discsel_def @ dnat_rews; |
276 val dnat_rews = dnat_discsel_def @ dnat_rews; |
277 |
277 |
278 |
278 |
279 (* ------------------------------------------------------------------------*) |
279 (* ------------------------------------------------------------------------*) |
280 (* Properties dnat_take *) |
280 (* Properties dnat_take *) |
281 (* ------------------------------------------------------------------------*) |
281 (* ------------------------------------------------------------------------*) |
282 val temp = prove_goalw Dnat.thy [dnat_take_def] "dnat_take n`UU = UU" |
282 val temp = prove_goalw Dnat.thy [dnat_take_def] "dnat_take n`UU = UU" |
283 (fn prems => |
283 (fn prems => |
284 [ |
284 [ |
285 (res_inst_tac [("n","n")] natE 1), |
285 (res_inst_tac [("n","n")] natE 1), |
286 (Asm_simp_tac 1), |
286 (Asm_simp_tac 1), |
287 (Asm_simp_tac 1), |
287 (Asm_simp_tac 1), |
288 (simp_tac (!simpset addsimps dnat_rews) 1) |
288 (simp_tac (!simpset addsimps dnat_rews) 1) |
289 ]); |
289 ]); |
290 |
290 |
291 val dnat_take = [temp]; |
291 val dnat_take = [temp]; |
292 |
292 |
293 val temp = prove_goalw Dnat.thy [dnat_take_def] "dnat_take 0`xs = UU" |
293 val temp = prove_goalw Dnat.thy [dnat_take_def] "dnat_take 0`xs = UU" |
294 (fn prems => |
294 (fn prems => |
295 [ |
295 [ |
296 (Asm_simp_tac 1) |
296 (Asm_simp_tac 1) |
297 ]); |
297 ]); |
298 |
298 |
299 val dnat_take = temp::dnat_take; |
299 val dnat_take = temp::dnat_take; |
300 |
300 |
301 val temp = prove_goalw Dnat.thy [dnat_take_def] |
301 val temp = prove_goalw Dnat.thy [dnat_take_def] |
302 "dnat_take (Suc n)`dzero=dzero" |
302 "dnat_take (Suc n)`dzero=dzero" |
303 (fn prems => |
303 (fn prems => |
304 [ |
304 [ |
305 (Asm_simp_tac 1), |
305 (Asm_simp_tac 1), |
306 (simp_tac (!simpset addsimps dnat_rews) 1) |
306 (simp_tac (!simpset addsimps dnat_rews) 1) |
307 ]); |
307 ]); |
308 |
308 |
309 val dnat_take = temp::dnat_take; |
309 val dnat_take = temp::dnat_take; |
310 |
310 |
311 val temp = prove_goalw Dnat.thy [dnat_take_def] |
311 val temp = prove_goalw Dnat.thy [dnat_take_def] |
312 "dnat_take (Suc n)`(dsucc`xs)=dsucc`(dnat_take n ` xs)" |
312 "dnat_take (Suc n)`(dsucc`xs)=dsucc`(dnat_take n ` xs)" |
313 (fn prems => |
313 (fn prems => |
314 [ |
314 [ |
315 (res_inst_tac [("Q","xs=UU")] classical2 1), |
315 (res_inst_tac [("Q","xs=UU")] classical2 1), |
316 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
316 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
317 (Asm_simp_tac 1), |
317 (Asm_simp_tac 1), |
318 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
318 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
319 (res_inst_tac [("n","n")] natE 1), |
319 (res_inst_tac [("n","n")] natE 1), |
320 (Asm_simp_tac 1), |
320 (Asm_simp_tac 1), |
321 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
321 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
322 (Asm_simp_tac 1), |
322 (Asm_simp_tac 1), |
323 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
323 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
324 (Asm_simp_tac 1), |
324 (Asm_simp_tac 1), |
325 (asm_simp_tac (!simpset addsimps dnat_rews) 1) |
325 (asm_simp_tac (!simpset addsimps dnat_rews) 1) |
326 ]); |
326 ]); |
327 |
327 |
328 val dnat_take = temp::dnat_take; |
328 val dnat_take = temp::dnat_take; |
329 |
329 |
330 val dnat_rews = dnat_take @ dnat_rews; |
330 val dnat_rews = dnat_take @ dnat_rews; |
331 |
331 |
334 (* take lemma for dnats *) |
334 (* take lemma for dnats *) |
335 (* ------------------------------------------------------------------------*) |
335 (* ------------------------------------------------------------------------*) |
336 |
336 |
337 fun prover reach defs thm = prove_goalw Dnat.thy defs thm |
337 fun prover reach defs thm = prove_goalw Dnat.thy defs thm |
338 (fn prems => |
338 (fn prems => |
339 [ |
339 [ |
340 (res_inst_tac [("t","s1")] (reach RS subst) 1), |
340 (res_inst_tac [("t","s1")] (reach RS subst) 1), |
341 (res_inst_tac [("t","s2")] (reach RS subst) 1), |
341 (res_inst_tac [("t","s2")] (reach RS subst) 1), |
342 (rtac (fix_def2 RS ssubst) 1), |
342 (rtac (fix_def2 RS ssubst) 1), |
343 (rtac (contlub_cfun_fun RS ssubst) 1), |
343 (rtac (contlub_cfun_fun RS ssubst) 1), |
344 (rtac is_chain_iterate 1), |
344 (rtac is_chain_iterate 1), |
345 (rtac (contlub_cfun_fun RS ssubst) 1), |
345 (rtac (contlub_cfun_fun RS ssubst) 1), |
346 (rtac is_chain_iterate 1), |
346 (rtac is_chain_iterate 1), |
347 (rtac lub_equal 1), |
347 (rtac lub_equal 1), |
348 (rtac (is_chain_iterate RS ch2ch_fappL) 1), |
348 (rtac (is_chain_iterate RS ch2ch_fappL) 1), |
349 (rtac (is_chain_iterate RS ch2ch_fappL) 1), |
349 (rtac (is_chain_iterate RS ch2ch_fappL) 1), |
350 (rtac allI 1), |
350 (rtac allI 1), |
351 (resolve_tac prems 1) |
351 (resolve_tac prems 1) |
352 ]); |
352 ]); |
353 |
353 |
354 val dnat_take_lemma = prover dnat_reach [dnat_take_def] |
354 val dnat_take_lemma = prover dnat_reach [dnat_take_def] |
355 "(!!n.dnat_take n`s1 = dnat_take n`s2) ==> s1=s2"; |
355 "(!!n.dnat_take n`s1 = dnat_take n`s2) ==> s1=s2"; |
356 |
356 |
357 |
357 |
358 (* ------------------------------------------------------------------------*) |
358 (* ------------------------------------------------------------------------*) |
359 (* Co -induction for dnats *) |
359 (* Co -induction for dnats *) |
360 (* ------------------------------------------------------------------------*) |
360 (* ------------------------------------------------------------------------*) |
361 |
361 |
362 qed_goalw "dnat_coind_lemma" Dnat.thy [dnat_bisim_def] |
362 qed_goalw "dnat_coind_lemma" Dnat.thy [dnat_bisim_def] |
363 "dnat_bisim R ==> ! p q. R p q --> dnat_take n`p = dnat_take n`q" |
363 "dnat_bisim R ==> ! p q. R p q --> dnat_take n`p = dnat_take n`q" |
364 (fn prems => |
364 (fn prems => |
365 [ |
365 [ |
366 (cut_facts_tac prems 1), |
366 (cut_facts_tac prems 1), |
367 (nat_ind_tac "n" 1), |
367 (nat_ind_tac "n" 1), |
368 (simp_tac (!simpset addsimps dnat_take) 1), |
368 (simp_tac (!simpset addsimps dnat_take) 1), |
369 (strip_tac 1), |
369 (strip_tac 1), |
370 ((etac allE 1) THEN (etac allE 1) THEN (etac (mp RS disjE) 1)), |
370 ((etac allE 1) THEN (etac allE 1) THEN (etac (mp RS disjE) 1)), |
371 (atac 1), |
371 (atac 1), |
372 (asm_simp_tac (!simpset addsimps dnat_take) 1), |
372 (asm_simp_tac (!simpset addsimps dnat_take) 1), |
373 (etac disjE 1), |
373 (etac disjE 1), |
374 (asm_simp_tac (!simpset addsimps dnat_take) 1), |
374 (asm_simp_tac (!simpset addsimps dnat_take) 1), |
375 (etac exE 1), |
375 (etac exE 1), |
376 (etac exE 1), |
376 (etac exE 1), |
377 (asm_simp_tac (!simpset addsimps dnat_take) 1), |
377 (asm_simp_tac (!simpset addsimps dnat_take) 1), |
378 (REPEAT (etac conjE 1)), |
378 (REPEAT (etac conjE 1)), |
379 (rtac cfun_arg_cong 1), |
379 (rtac cfun_arg_cong 1), |
380 (fast_tac HOL_cs 1) |
380 (fast_tac HOL_cs 1) |
381 ]); |
381 ]); |
382 |
382 |
383 qed_goal "dnat_coind" Dnat.thy "[|dnat_bisim R;R p q|] ==> p = q" |
383 qed_goal "dnat_coind" Dnat.thy "[|dnat_bisim R;R p q|] ==> p = q" |
384 (fn prems => |
384 (fn prems => |
385 [ |
385 [ |
386 (rtac dnat_take_lemma 1), |
386 (rtac dnat_take_lemma 1), |
387 (rtac (dnat_coind_lemma RS spec RS spec RS mp) 1), |
387 (rtac (dnat_coind_lemma RS spec RS spec RS mp) 1), |
388 (resolve_tac prems 1), |
388 (resolve_tac prems 1), |
389 (resolve_tac prems 1) |
389 (resolve_tac prems 1) |
390 ]); |
390 ]); |
391 |
391 |
392 |
392 |
393 (* ------------------------------------------------------------------------*) |
393 (* ------------------------------------------------------------------------*) |
394 (* structural induction for admissible predicates *) |
394 (* structural induction for admissible predicates *) |
395 (* ------------------------------------------------------------------------*) |
395 (* ------------------------------------------------------------------------*) |
399 "[| adm(P);\ |
399 "[| adm(P);\ |
400 \ P(UU);\ |
400 \ P(UU);\ |
401 \ P(dzero);\ |
401 \ P(dzero);\ |
402 \ !! s1.[|s1~=UU ; P(s1)|] ==> P(dsucc`s1)|] ==> P(s)" |
402 \ !! s1.[|s1~=UU ; P(s1)|] ==> P(dsucc`s1)|] ==> P(s)" |
403 (fn prems => |
403 (fn prems => |
404 [ |
404 [ |
405 (rtac (dnat_reach RS subst) 1), |
405 (rtac (dnat_reach RS subst) 1), |
406 (res_inst_tac [("x","s")] spec 1), |
406 (res_inst_tac [("x","s")] spec 1), |
407 (rtac fix_ind 1), |
407 (rtac fix_ind 1), |
408 (rtac adm_all2 1), |
408 (rtac adm_all2 1), |
409 (rtac adm_subst 1), |
409 (rtac adm_subst 1), |
410 (cont_tacR 1), |
410 (cont_tacR 1), |
411 (resolve_tac prems 1), |
411 (resolve_tac prems 1), |
412 (Simp_tac 1), |
412 (Simp_tac 1), |
413 (resolve_tac prems 1), |
413 (resolve_tac prems 1), |
414 (strip_tac 1), |
414 (strip_tac 1), |
415 (res_inst_tac [("n","xa")] dnatE 1), |
415 (res_inst_tac [("n","xa")] dnatE 1), |
416 (asm_simp_tac (!simpset addsimps dnat_copy) 1), |
416 (asm_simp_tac (!simpset addsimps dnat_copy) 1), |
417 (resolve_tac prems 1), |
417 (resolve_tac prems 1), |
418 (asm_simp_tac (!simpset addsimps dnat_copy) 1), |
418 (asm_simp_tac (!simpset addsimps dnat_copy) 1), |
419 (resolve_tac prems 1), |
419 (resolve_tac prems 1), |
420 (asm_simp_tac (!simpset addsimps dnat_copy) 1), |
420 (asm_simp_tac (!simpset addsimps dnat_copy) 1), |
421 (res_inst_tac [("Q","x`xb=UU")] classical2 1), |
421 (res_inst_tac [("Q","x`xb=UU")] classical2 1), |
422 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
422 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
423 (resolve_tac prems 1), |
423 (resolve_tac prems 1), |
424 (eresolve_tac prems 1), |
424 (eresolve_tac prems 1), |
425 (etac spec 1) |
425 (etac spec 1) |
426 ]); |
426 ]); |
427 *) |
427 *) |
428 |
428 |
429 qed_goal "dnat_finite_ind" Dnat.thy |
429 qed_goal "dnat_finite_ind" Dnat.thy |
430 "[|P(UU);P(dzero);\ |
430 "[|P(UU);P(dzero);\ |
431 \ !! s1.[|s1~=UU;P(s1)|] ==> P(dsucc`s1)\ |
431 \ !! s1.[|s1~=UU;P(s1)|] ==> P(dsucc`s1)\ |
432 \ |] ==> !s.P(dnat_take n`s)" |
432 \ |] ==> !s.P(dnat_take n`s)" |
433 (fn prems => |
433 (fn prems => |
434 [ |
434 [ |
435 (nat_ind_tac "n" 1), |
435 (nat_ind_tac "n" 1), |
436 (simp_tac (!simpset addsimps dnat_rews) 1), |
436 (simp_tac (!simpset addsimps dnat_rews) 1), |
437 (resolve_tac prems 1), |
437 (resolve_tac prems 1), |
438 (rtac allI 1), |
438 (rtac allI 1), |
439 (res_inst_tac [("n","s")] dnatE 1), |
439 (res_inst_tac [("n","s")] dnatE 1), |
440 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
440 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
441 (resolve_tac prems 1), |
441 (resolve_tac prems 1), |
442 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
442 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
443 (resolve_tac prems 1), |
443 (resolve_tac prems 1), |
444 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
444 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
445 (res_inst_tac [("Q","dnat_take n1`x=UU")] classical2 1), |
445 (res_inst_tac [("Q","dnat_take n1`x=UU")] classical2 1), |
446 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
446 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
447 (resolve_tac prems 1), |
447 (resolve_tac prems 1), |
448 (resolve_tac prems 1), |
448 (resolve_tac prems 1), |
449 (atac 1), |
449 (atac 1), |
450 (etac spec 1) |
450 (etac spec 1) |
451 ]); |
451 ]); |
452 |
452 |
453 qed_goal "dnat_all_finite_lemma1" Dnat.thy |
453 qed_goal "dnat_all_finite_lemma1" Dnat.thy |
454 "!s.dnat_take n`s=UU |dnat_take n`s=s" |
454 "!s.dnat_take n`s=UU |dnat_take n`s=s" |
455 (fn prems => |
455 (fn prems => |
456 [ |
456 [ |
457 (nat_ind_tac "n" 1), |
457 (nat_ind_tac "n" 1), |
458 (simp_tac (!simpset addsimps dnat_rews) 1), |
458 (simp_tac (!simpset addsimps dnat_rews) 1), |
459 (rtac allI 1), |
459 (rtac allI 1), |
460 (res_inst_tac [("n","s")] dnatE 1), |
460 (res_inst_tac [("n","s")] dnatE 1), |
461 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
461 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
462 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
462 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
463 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
463 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
464 (eres_inst_tac [("x","x")] allE 1), |
464 (eres_inst_tac [("x","x")] allE 1), |
465 (etac disjE 1), |
465 (etac disjE 1), |
466 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
466 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
467 (asm_simp_tac (!simpset addsimps dnat_rews) 1) |
467 (asm_simp_tac (!simpset addsimps dnat_rews) 1) |
468 ]); |
468 ]); |
469 |
469 |
470 qed_goal "dnat_all_finite_lemma2" Dnat.thy "? n.dnat_take n`s=s" |
470 qed_goal "dnat_all_finite_lemma2" Dnat.thy "? n.dnat_take n`s=s" |
471 (fn prems => |
471 (fn prems => |
472 [ |
472 [ |
473 (res_inst_tac [("Q","s=UU")] classical2 1), |
473 (res_inst_tac [("Q","s=UU")] classical2 1), |
474 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
474 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
475 (subgoal_tac "(!n.dnat_take(n)`s=UU) |(? n.dnat_take(n)`s=s)" 1), |
475 (subgoal_tac "(!n.dnat_take(n)`s=UU) |(? n.dnat_take(n)`s=s)" 1), |
476 (etac disjE 1), |
476 (etac disjE 1), |
477 (eres_inst_tac [("P","s=UU")] notE 1), |
477 (eres_inst_tac [("P","s=UU")] notE 1), |
478 (rtac dnat_take_lemma 1), |
478 (rtac dnat_take_lemma 1), |
479 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
479 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
480 (atac 1), |
480 (atac 1), |
481 (subgoal_tac "!n.!s.dnat_take(n)`s=UU |dnat_take(n)`s=s" 1), |
481 (subgoal_tac "!n.!s.dnat_take(n)`s=UU |dnat_take(n)`s=s" 1), |
482 (fast_tac HOL_cs 1), |
482 (fast_tac HOL_cs 1), |
483 (rtac allI 1), |
483 (rtac allI 1), |
484 (rtac dnat_all_finite_lemma1 1) |
484 (rtac dnat_all_finite_lemma1 1) |
485 ]); |
485 ]); |
486 |
486 |
487 |
487 |
488 qed_goal "dnat_ind" Dnat.thy |
488 qed_goal "dnat_ind" Dnat.thy |
489 "[|P(UU);P(dzero);\ |
489 "[|P(UU);P(dzero);\ |
490 \ !! s1.[|s1~=UU;P(s1)|] ==> P(dsucc`s1)\ |
490 \ !! s1.[|s1~=UU;P(s1)|] ==> P(dsucc`s1)\ |
491 \ |] ==> P(s)" |
491 \ |] ==> P(s)" |
492 (fn prems => |
492 (fn prems => |
493 [ |
493 [ |
494 (rtac (dnat_all_finite_lemma2 RS exE) 1), |
494 (rtac (dnat_all_finite_lemma2 RS exE) 1), |
495 (etac subst 1), |
495 (etac subst 1), |
496 (rtac (dnat_finite_ind RS spec) 1), |
496 (rtac (dnat_finite_ind RS spec) 1), |
497 (REPEAT (resolve_tac prems 1)), |
497 (REPEAT (resolve_tac prems 1)), |
498 (REPEAT (atac 1)) |
498 (REPEAT (atac 1)) |
499 ]); |
499 ]); |
500 |
500 |
501 |
501 |
502 qed_goalw "dnat_flat" Dnat.thy [is_flat_def] "is_flat(dzero)" |
502 qed_goalw "dnat_flat" Dnat.thy [is_flat_def] "is_flat(dzero)" |
503 (fn prems => |
503 (fn prems => |
504 [ |
504 [ |
505 (rtac allI 1), |
505 (rtac allI 1), |
506 (res_inst_tac [("s","x")] dnat_ind 1), |
506 (res_inst_tac [("s","x")] dnat_ind 1), |
507 (fast_tac HOL_cs 1), |
507 (fast_tac HOL_cs 1), |
508 (rtac allI 1), |
508 (rtac allI 1), |
509 (res_inst_tac [("n","y")] dnatE 1), |
509 (res_inst_tac [("n","y")] dnatE 1), |
510 (fast_tac (HOL_cs addSIs [UU_I]) 1), |
510 (fast_tac (HOL_cs addSIs [UU_I]) 1), |
511 (Asm_simp_tac 1), |
511 (Asm_simp_tac 1), |
512 (asm_simp_tac (!simpset addsimps dnat_dist_less) 1), |
512 (asm_simp_tac (!simpset addsimps dnat_dist_less) 1), |
513 (rtac allI 1), |
513 (rtac allI 1), |
514 (res_inst_tac [("n","y")] dnatE 1), |
514 (res_inst_tac [("n","y")] dnatE 1), |
515 (fast_tac (HOL_cs addSIs [UU_I]) 1), |
515 (fast_tac (HOL_cs addSIs [UU_I]) 1), |
516 (asm_simp_tac (!simpset addsimps dnat_dist_less) 1), |
516 (asm_simp_tac (!simpset addsimps dnat_dist_less) 1), |
517 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
517 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
518 (strip_tac 1), |
518 (strip_tac 1), |
519 (subgoal_tac "s1<<xa" 1), |
519 (subgoal_tac "s1<<xa" 1), |
520 (etac allE 1), |
520 (etac allE 1), |
521 (dtac mp 1), |
521 (dtac mp 1), |
522 (atac 1), |
522 (atac 1), |
523 (etac disjE 1), |
523 (etac disjE 1), |
524 (contr_tac 1), |
524 (contr_tac 1), |
525 (Asm_simp_tac 1), |
525 (Asm_simp_tac 1), |
526 (resolve_tac dnat_invert 1), |
526 (resolve_tac dnat_invert 1), |
527 (REPEAT (atac 1)) |
527 (REPEAT (atac 1)) |
528 ]); |
528 ]); |
529 |
529 |
530 |
530 |
531 |
531 |
532 |
532 |
533 |
533 |
534 |
534 |