|
1 theory FSet |
|
2 imports QuotMain |
|
3 begin |
|
4 |
|
5 inductive |
|
6 list_eq (infix "\<approx>" 50) |
|
7 where |
|
8 "a#b#xs \<approx> b#a#xs" |
|
9 | "[] \<approx> []" |
|
10 | "xs \<approx> ys \<Longrightarrow> ys \<approx> xs" |
|
11 | "a#a#xs \<approx> a#xs" |
|
12 | "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys" |
|
13 | "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3" |
|
14 |
|
15 lemma list_eq_refl: |
|
16 shows "xs \<approx> xs" |
|
17 apply (induct xs) |
|
18 apply (auto intro: list_eq.intros) |
|
19 done |
|
20 |
|
21 lemma equiv_list_eq: |
|
22 shows "EQUIV list_eq" |
|
23 unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def |
|
24 apply(auto intro: list_eq.intros list_eq_refl) |
|
25 done |
|
26 |
|
27 quotient fset = "'a list" / "list_eq" |
|
28 apply(rule equiv_list_eq) |
|
29 done |
|
30 |
|
31 print_theorems |
|
32 |
|
33 typ "'a fset" |
|
34 thm "Rep_fset" |
|
35 thm "ABS_fset_def" |
|
36 |
|
37 ML {* @{term "Abs_fset"} *} |
|
38 local_setup {* |
|
39 make_const_def @{binding EMPTY} @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
|
40 *} |
|
41 |
|
42 term Nil |
|
43 term EMPTY |
|
44 thm EMPTY_def |
|
45 |
|
46 |
|
47 local_setup {* |
|
48 make_const_def @{binding INSERT} @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
|
49 *} |
|
50 |
|
51 term Cons |
|
52 term INSERT |
|
53 thm INSERT_def |
|
54 |
|
55 local_setup {* |
|
56 make_const_def @{binding UNION} @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
|
57 *} |
|
58 |
|
59 term append |
|
60 term UNION |
|
61 thm UNION_def |
|
62 |
|
63 |
|
64 thm QUOTIENT_fset |
|
65 |
|
66 thm QUOT_TYPE_I_fset.thm11 |
|
67 |
|
68 |
|
69 fun |
|
70 membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infix "memb" 100) |
|
71 where |
|
72 m1: "(x memb []) = False" |
|
73 | m2: "(x memb (y#xs)) = ((x=y) \<or> (x memb xs))" |
|
74 |
|
75 fun |
|
76 card1 :: "'a list \<Rightarrow> nat" |
|
77 where |
|
78 card1_nil: "(card1 []) = 0" |
|
79 | card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))" |
|
80 |
|
81 local_setup {* |
|
82 make_const_def @{binding card} @{term "card1"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
|
83 *} |
|
84 |
|
85 term card1 |
|
86 term card |
|
87 thm card_def |
|
88 |
|
89 (* text {* |
|
90 Maybe make_const_def should require a theorem that says that the particular lifted function |
|
91 respects the relation. With it such a definition would be impossible: |
|
92 make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
|
93 *}*) |
|
94 |
|
95 lemma card1_0: |
|
96 fixes a :: "'a list" |
|
97 shows "(card1 a = 0) = (a = [])" |
|
98 apply (induct a) |
|
99 apply (simp) |
|
100 apply (simp_all) |
|
101 apply meson |
|
102 apply (simp_all) |
|
103 done |
|
104 |
|
105 lemma not_mem_card1: |
|
106 fixes x :: "'a" |
|
107 fixes xs :: "'a list" |
|
108 shows "~(x memb xs) \<Longrightarrow> card1 (x # xs) = Suc (card1 xs)" |
|
109 by simp |
|
110 |
|
111 |
|
112 lemma mem_cons: |
|
113 fixes x :: "'a" |
|
114 fixes xs :: "'a list" |
|
115 assumes a : "x memb xs" |
|
116 shows "x # xs \<approx> xs" |
|
117 using a |
|
118 apply (induct xs) |
|
119 apply (auto intro: list_eq.intros) |
|
120 done |
|
121 |
|
122 lemma card1_suc: |
|
123 fixes xs :: "'a list" |
|
124 fixes n :: "nat" |
|
125 assumes c: "card1 xs = Suc n" |
|
126 shows "\<exists>a ys. ~(a memb ys) \<and> xs \<approx> (a # ys)" |
|
127 using c |
|
128 apply(induct xs) |
|
129 apply (metis Suc_neq_Zero card1_0) |
|
130 apply (metis QUOT_TYPE_I_fset.R_trans card1_cons list_eq_refl mem_cons) |
|
131 done |
|
132 |
|
133 primrec |
|
134 fold1 |
|
135 where |
|
136 "fold1 f (g :: 'a \<Rightarrow> 'b) (z :: 'b) [] = z" |
|
137 | "fold1 f g z (a # A) = |
|
138 (if ((!u v. (f u v = f v u)) |
|
139 \<and> (!u v w. ((f u (f v w) = f (f u v) w)))) |
|
140 then ( |
|
141 if (a memb A) then (fold1 f g z A) else (f (g a) (fold1 f g z A)) |
|
142 ) else z)" |
|
143 |
|
144 (* fold1_def is not usable, but: *) |
|
145 thm fold1.simps |
|
146 |
|
147 lemma fs1_strong_cases: |
|
148 fixes X :: "'a list" |
|
149 shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a memb Y) \<and> (X \<approx> a # Y)))" |
|
150 apply (induct X) |
|
151 apply (simp) |
|
152 apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons m1) |
|
153 done |
|
154 |
|
155 local_setup {* |
|
156 make_const_def @{binding IN} @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
|
157 *} |
|
158 |
|
159 term membship |
|
160 term IN |
|
161 thm IN_def |
|
162 |
|
163 ML {* |
|
164 val consts = [@{const_name "Nil"}, @{const_name "Cons"}, |
|
165 @{const_name "membship"}, @{const_name "card1"}, |
|
166 @{const_name "append"}, @{const_name "fold1"}]; |
|
167 *} |
|
168 |
|
169 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *} |
|
170 ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *} |
|
171 |
|
172 thm fun_map.simps |
|
173 text {* Respectfullness *} |
|
174 |
|
175 lemma mem_respects: |
|
176 fixes z |
|
177 assumes a: "list_eq x y" |
|
178 shows "(z memb x) = (z memb y)" |
|
179 using a by induct auto |
|
180 |
|
181 lemma card1_rsp: |
|
182 fixes a b :: "'a list" |
|
183 assumes e: "a \<approx> b" |
|
184 shows "card1 a = card1 b" |
|
185 using e apply induct |
|
186 apply (simp_all add:mem_respects) |
|
187 done |
|
188 |
|
189 lemma cons_preserves: |
|
190 fixes z |
|
191 assumes a: "xs \<approx> ys" |
|
192 shows "(z # xs) \<approx> (z # ys)" |
|
193 using a by (rule list_eq.intros(5)) |
|
194 |
|
195 lemma append_respects_fst: |
|
196 assumes a : "list_eq l1 l2" |
|
197 shows "list_eq (l1 @ s) (l2 @ s)" |
|
198 using a |
|
199 apply(induct) |
|
200 apply(auto intro: list_eq.intros) |
|
201 apply(simp add: list_eq_refl) |
|
202 done |
|
203 |
|
204 thm list.induct |
|
205 lemma list_induct_hol4: |
|
206 fixes P :: "'a list \<Rightarrow> bool" |
|
207 assumes "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))" |
|
208 shows "(\<forall>l. (P l))" |
|
209 sorry |
|
210 |
|
211 ML {* atomize_thm @{thm list_induct_hol4} *} |
|
212 |
|
213 prove list_induct_r: {* |
|
214 build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *} |
|
215 apply (simp only: equiv_res_forall[OF equiv_list_eq]) |
|
216 thm RIGHT_RES_FORALL_REGULAR |
|
217 apply (rule RIGHT_RES_FORALL_REGULAR) |
|
218 prefer 2 |
|
219 apply (assumption) |
|
220 apply (metis) |
|
221 done |
|
222 |
|
223 ML {* |
|
224 fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} => |
|
225 let |
|
226 val pat = Drule.strip_imp_concl (cprop_of thm) |
|
227 val insts = Thm.match (pat, concl) |
|
228 in |
|
229 rtac (Drule.instantiate insts thm) 1 |
|
230 end |
|
231 handle _ => no_tac |
|
232 ) |
|
233 *} |
|
234 |
|
235 ML {* |
|
236 fun res_forall_rsp_tac ctxt = |
|
237 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
|
238 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
|
239 THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN' |
|
240 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
|
241 *} |
|
242 |
|
243 |
|
244 ML {* |
|
245 fun quotient_tac quot_thm = |
|
246 REPEAT_ALL_NEW (FIRST' [ |
|
247 rtac @{thm FUN_QUOTIENT}, |
|
248 rtac quot_thm, |
|
249 rtac @{thm IDENTITY_QUOTIENT} |
|
250 ]) |
|
251 *} |
|
252 |
|
253 ML {* |
|
254 fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm = |
|
255 (FIRST' [ |
|
256 rtac @{thm FUN_QUOTIENT}, |
|
257 rtac quot_thm, |
|
258 rtac @{thm IDENTITY_QUOTIENT}, |
|
259 rtac @{thm ext}, |
|
260 rtac trans_thm, |
|
261 res_forall_rsp_tac ctxt, |
|
262 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), |
|
263 (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), |
|
264 rtac reflex_thm, |
|
265 atac, |
|
266 ( |
|
267 (simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps})) |
|
268 THEN_ALL_NEW (fn _ => no_tac) |
|
269 ) |
|
270 ]) |
|
271 *} |
|
272 |
|
273 ML {* |
|
274 fun r_mk_comb_tac_fset ctxt = |
|
275 r_mk_comb_tac ctxt @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
|
276 *} |
|
277 |
|
278 |
|
279 ML {* val thm = @{thm list_induct_r} OF [atomize_thm @{thm list_induct_hol4}] *} |
|
280 ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
|
281 ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
|
282 |
|
283 prove list_induct_tr: trm_r |
|
284 apply (atomize(full)) |
|
285 (* APPLY_RSP_TAC *) |
|
286 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
287 (* LAMBDA_RES_TAC *) |
|
288 apply (simp only: FUN_REL.simps) |
|
289 apply (rule allI) |
|
290 apply (rule allI) |
|
291 apply (rule impI) |
|
292 (* MK_COMB_TAC *) |
|
293 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
|
294 (* MK_COMB_TAC *) |
|
295 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
|
296 (* REFL_TAC *) |
|
297 apply (simp) |
|
298 (* MK_COMB_TAC *) |
|
299 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
|
300 (* MK_COMB_TAC *) |
|
301 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
|
302 (* REFL_TAC *) |
|
303 apply (simp) |
|
304 (* APPLY_RSP_TAC *) |
|
305 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
306 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
307 apply (simp only: FUN_REL.simps) |
|
308 apply (rule allI) |
|
309 apply (rule allI) |
|
310 apply (rule impI) |
|
311 (* MK_COMB_TAC *) |
|
312 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
|
313 (* MK_COMB_TAC *) |
|
314 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
|
315 (* REFL_TAC *) |
|
316 apply (simp) |
|
317 (* APPLY_RSP *) |
|
318 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
319 (* MK_COMB_TAC *) |
|
320 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
|
321 (* REFL_TAC *) |
|
322 apply (simp) |
|
323 (* W(C (curry op THEN) (G... *) |
|
324 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
325 (* CONS respects *) |
|
326 apply (simp add: FUN_REL.simps) |
|
327 apply (rule allI) |
|
328 apply (rule allI) |
|
329 apply (rule allI) |
|
330 apply (rule impI) |
|
331 apply (rule cons_preserves) |
|
332 apply (assumption) |
|
333 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
334 apply (simp only: FUN_REL.simps) |
|
335 apply (rule allI) |
|
336 apply (rule allI) |
|
337 apply (rule impI) |
|
338 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
339 done |
|
340 |
|
341 prove list_induct_t: trm |
|
342 apply (simp only: list_induct_tr[symmetric]) |
|
343 apply (tactic {* rtac thm 1 *}) |
|
344 done |
|
345 |
|
346 ML {* val nthm = MetaSimplifier.rewrite_rule fset_defs_sym (snd (no_vars (Context.Theory @{theory}, @{thm list_induct_t}))) *} |
|
347 |
|
348 thm list.recs(2) |
|
349 thm m2 |
|
350 ML {* atomize_thm @{thm m2} *} |
|
351 |
|
352 prove m2_r_p: {* |
|
353 build_regularize_goal (atomize_thm @{thm m2}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *} |
|
354 apply (simp add: equiv_res_forall[OF equiv_list_eq]) |
|
355 done |
|
356 |
|
357 ML {* val m2_r = @{thm m2_r_p} OF [atomize_thm @{thm m2}] *} |
|
358 ML {* val m2_t_g = build_repabs_goal @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *} |
|
359 ML {* val m2_t = build_repabs_term @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *} |
|
360 prove m2_t_p: m2_t_g |
|
361 apply (atomize(full)) |
|
362 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
363 apply (simp add: FUN_REL.simps) |
|
364 prefer 2 |
|
365 apply (simp only: FUN_REL.simps) |
|
366 apply (rule allI) |
|
367 apply (rule allI) |
|
368 apply (rule impI) |
|
369 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
370 prefer 2 |
|
371 apply (simp only: FUN_REL.simps) |
|
372 apply (rule allI) |
|
373 apply (rule allI) |
|
374 apply (rule impI) |
|
375 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
376 apply (simp only: FUN_REL.simps) |
|
377 apply (rule allI) |
|
378 apply (rule allI) |
|
379 apply (rule impI) |
|
380 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
381 apply (simp only: FUN_REL.simps) |
|
382 apply (rule allI) |
|
383 apply (rule allI) |
|
384 apply (rule impI) |
|
385 apply (rule allI) |
|
386 apply (rule allI) |
|
387 apply (rule impI) |
|
388 apply (simp add:mem_respects) |
|
389 apply (simp only: FUN_REL.simps) |
|
390 apply (rule allI) |
|
391 apply (rule allI) |
|
392 apply (rule impI) |
|
393 apply (rule allI) |
|
394 apply (rule allI) |
|
395 apply (rule impI) |
|
396 apply (simp add:cons_preserves) |
|
397 apply (simp only: FUN_REL.simps) |
|
398 apply (rule allI) |
|
399 apply (rule allI) |
|
400 apply (rule impI) |
|
401 apply (rule allI) |
|
402 apply (rule allI) |
|
403 apply (rule impI) |
|
404 apply (simp add:mem_respects) |
|
405 apply (auto) |
|
406 done |
|
407 |
|
408 prove m2_t: m2_t |
|
409 apply (simp only: m2_t_p[symmetric]) |
|
410 apply (tactic {* rtac m2_r 1 *}) |
|
411 done |
|
412 |
|
413 lemma id_apply2 [simp]: "id x \<equiv> x" |
|
414 by (simp add: id_def) |
|
415 |
|
416 |
|
417 thm LAMBDA_PRS |
|
418 ML {* |
|
419 val t = prop_of @{thm LAMBDA_PRS} |
|
420 val tt = Drule.instantiate' [SOME @{ctyp "'a list"}, SOME @{ctyp "'a fset"}] [] @{thm LAMBDA_PRS} |
|
421 val ttt = @{thm LAMBDA_PRS} OF [@{thm QUOTIENT_fset}, @{thm IDENTITY_QUOTIENT}] |
|
422 val tttt = @{thm "HOL.sym"} OF [ttt] |
|
423 *} |
|
424 ML {* |
|
425 val ttttt = MetaSimplifier.rewrite_rule [@{thm id_apply2}] tttt |
|
426 val zzz = @{thm m2_t} |
|
427 *} |
|
428 |
|
429 ML {* |
|
430 fun eqsubst_thm ctxt thms thm = |
|
431 let |
|
432 val goalstate = Goal.init (Thm.cprop_of thm) |
|
433 val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of |
|
434 NONE => error "eqsubst_thm" |
|
435 | SOME th => cprem_of th 1 |
|
436 val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1 |
|
437 val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a')) |
|
438 val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac)); |
|
439 in |
|
440 Simplifier.rewrite_rule [rt] thm |
|
441 end |
|
442 *} |
|
443 ML {* val m2_t' = eqsubst_thm @{context} [ttttt] @{thm m2_t} *} |
|
444 ML {* val rwr = @{thm FORALL_PRS[OF QUOTIENT_fset]} *} |
|
445 ML {* val rwrs = @{thm "HOL.sym"} OF [ObjectLogic.rulify rwr] *} |
|
446 ML {* rwrs; m2_t' *} |
|
447 ML {* eqsubst_thm @{context} [rwrs] m2_t' *} |
|
448 thm INSERT_def |
|
449 |
|
450 |
|
451 ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *} |
|
452 |
|
453 prove card1_suc_r: {* |
|
454 Logic.mk_implies |
|
455 ((prop_of card1_suc_f), |
|
456 (regularise (prop_of card1_suc_f) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *} |
|
457 apply (simp add: equiv_res_forall[OF equiv_list_eq] equiv_res_exists[OF equiv_list_eq]) |
|
458 done |
|
459 |
|
460 ML {* @{thm card1_suc_r} OF [card1_suc_f] *} |
|
461 |
|
462 ML {* val li = Thm.freezeT (atomize_thm @{thm fold1.simps(2)}) *} |
|
463 prove fold1_def_2_r: {* |
|
464 Logic.mk_implies |
|
465 ((prop_of li), |
|
466 (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *} |
|
467 apply (simp add: equiv_res_forall[OF equiv_list_eq]) |
|
468 done |
|
469 |
|
470 ML {* @{thm fold1_def_2_r} OF [li] *} |
|
471 |
|
472 |
|
473 lemma yy: |
|
474 shows "(False = x memb []) = (False = IN (x::nat) EMPTY)" |
|
475 unfolding IN_def EMPTY_def |
|
476 apply(rule_tac f="(op =) False" in arg_cong) |
|
477 apply(rule mem_respects) |
|
478 apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) |
|
479 apply(rule list_eq.intros) |
|
480 done |
|
481 |
|
482 lemma |
|
483 shows "IN (x::nat) EMPTY = False" |
|
484 using m1 |
|
485 apply - |
|
486 apply(rule yy[THEN iffD1, symmetric]) |
|
487 apply(simp) |
|
488 done |
|
489 |
|
490 lemma |
|
491 shows "((x=y) \<or> (IN x xs) = (IN (x::nat) (INSERT y xs))) = |
|
492 ((x=y) \<or> x memb REP_fset xs = x memb (y # REP_fset xs))" |
|
493 unfolding IN_def INSERT_def |
|
494 apply(rule_tac f="(op \<or>) (x=y)" in arg_cong) |
|
495 apply(rule_tac f="(op =) (x memb REP_fset xs)" in arg_cong) |
|
496 apply(rule mem_respects) |
|
497 apply(rule list_eq.intros(3)) |
|
498 apply(unfold REP_fset_def ABS_fset_def) |
|
499 apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset]) |
|
500 apply(rule list_eq_refl) |
|
501 done |
|
502 |
|
503 lemma yyy: |
|
504 shows " |
|
505 ( |
|
506 (UNION EMPTY s = s) & |
|
507 ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2))) |
|
508 ) = ( |
|
509 ((ABS_fset ([] @ REP_fset s)) = s) & |
|
510 ((ABS_fset ((e # (REP_fset s1)) @ REP_fset s2)) = ABS_fset (e # (REP_fset s1 @ REP_fset s2))) |
|
511 )" |
|
512 unfolding UNION_def EMPTY_def INSERT_def |
|
513 apply(rule_tac f="(op &)" in arg_cong2) |
|
514 apply(rule_tac f="(op =)" in arg_cong2) |
|
515 apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric]) |
|
516 apply(rule append_respects_fst) |
|
517 apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) |
|
518 apply(rule list_eq_refl) |
|
519 apply(simp) |
|
520 apply(rule_tac f="(op =)" in arg_cong2) |
|
521 apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric]) |
|
522 apply(rule append_respects_fst) |
|
523 apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) |
|
524 apply(rule list_eq_refl) |
|
525 apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric]) |
|
526 apply(rule list_eq.intros(5)) |
|
527 apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) |
|
528 apply(rule list_eq_refl) |
|
529 done |
|
530 |
|
531 lemma |
|
532 shows " |
|
533 (UNION EMPTY s = s) & |
|
534 ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))" |
|
535 apply (simp add: yyy) |
|
536 apply (simp add: QUOT_TYPE_I_fset.thm10) |
|
537 done |
|
538 |
|
539 ML {* |
|
540 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2})) |
|
541 *} |
|
542 |
|
543 ML {* |
|
544 cterm_of @{theory} (prop_of m1_novars); |
|
545 cterm_of @{theory} (build_repabs_term @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}); |
|
546 *} |
|
547 |
|
548 |
|
549 (* Has all the theorems about fset plugged in. These should be parameters to the tactic *) |
|
550 ML {* |
|
551 fun transconv_fset_tac' ctxt = |
|
552 (LocalDefs.unfold_tac @{context} fset_defs) THEN |
|
553 ObjectLogic.full_atomize_tac 1 THEN |
|
554 REPEAT_ALL_NEW (FIRST' [ |
|
555 rtac @{thm list_eq_refl}, |
|
556 rtac @{thm cons_preserves}, |
|
557 rtac @{thm mem_respects}, |
|
558 rtac @{thm card1_rsp}, |
|
559 rtac @{thm QUOT_TYPE_I_fset.R_trans2}, |
|
560 CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})), |
|
561 Cong_Tac.cong_tac @{thm cong}, |
|
562 rtac @{thm ext} |
|
563 ]) 1 |
|
564 *} |
|
565 |
|
566 ML {* |
|
567 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1})) |
|
568 val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} |
|
569 val cgoal = cterm_of @{theory} goal |
|
570 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
|
571 *} |
|
572 |
|
573 (*notation ( output) "prop" ("#_" [1000] 1000) *) |
|
574 notation ( output) "Trueprop" ("#_" [1000] 1000) |
|
575 |
|
576 |
|
577 prove {* (Thm.term_of cgoal2) *} |
|
578 apply (tactic {* transconv_fset_tac' @{context} *}) |
|
579 done |
|
580 |
|
581 thm length_append (* Not true but worth checking that the goal is correct *) |
|
582 ML {* |
|
583 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm length_append})) |
|
584 val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} |
|
585 val cgoal = cterm_of @{theory} goal |
|
586 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
|
587 *} |
|
588 prove {* Thm.term_of cgoal2 *} |
|
589 apply (tactic {* transconv_fset_tac' @{context} *}) |
|
590 sorry |
|
591 |
|
592 thm m2 |
|
593 ML {* |
|
594 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2})) |
|
595 val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} |
|
596 val cgoal = cterm_of @{theory} goal |
|
597 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
|
598 *} |
|
599 prove {* Thm.term_of cgoal2 *} |
|
600 apply (tactic {* transconv_fset_tac' @{context} *}) |
|
601 done |
|
602 |
|
603 thm list_eq.intros(4) |
|
604 ML {* |
|
605 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(4)})) |
|
606 val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} |
|
607 val cgoal = cterm_of @{theory} goal |
|
608 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
|
609 val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2) |
|
610 *} |
|
611 |
|
612 (* It is the same, but we need a name for it. *) |
|
613 prove zzz : {* Thm.term_of cgoal3 *} |
|
614 apply (tactic {* transconv_fset_tac' @{context} *}) |
|
615 done |
|
616 |
|
617 (*lemma zzz' : |
|
618 "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))" |
|
619 using list_eq.intros(4) by (simp only: zzz) |
|
620 |
|
621 thm QUOT_TYPE_I_fset.REPS_same |
|
622 ML {* val zzz'' = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *} |
|
623 *) |
|
624 |
|
625 thm list_eq.intros(5) |
|
626 (* prove {* build_repabs_goal @{context} (atomize_thm @{thm list_eq.intros(5)}) consts @{typ "'a list"} @{typ "'a fset"} *} *) |
|
627 ML {* |
|
628 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)})) |
|
629 val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} |
|
630 val cgoal = cterm_of @{theory} goal |
|
631 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
|
632 *} |
|
633 prove {* Thm.term_of cgoal2 *} |
|
634 apply (tactic {* transconv_fset_tac' @{context} *}) |
|
635 done |
|
636 |
|
637 ML {* |
|
638 fun lift_theorem_fset_aux thm lthy = |
|
639 let |
|
640 val ((_, [novars]), lthy2) = Variable.import true [thm] lthy; |
|
641 val goal = build_repabs_goal @{context} novars consts @{typ "'a list"} @{typ "'a fset"}; |
|
642 val cgoal = cterm_of @{theory} goal; |
|
643 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal); |
|
644 val tac = transconv_fset_tac' @{context}; |
|
645 val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac); |
|
646 val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm))) |
|
647 val nthm2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same QUOT_TYPE_I_fset.thm10} nthm; |
|
648 val [nthm3] = ProofContext.export lthy2 lthy [nthm2] |
|
649 in |
|
650 nthm3 |
|
651 end |
|
652 *} |
|
653 |
|
654 ML {* lift_theorem_fset_aux @{thm m1} @{context} *} |
|
655 |
|
656 ML {* |
|
657 fun lift_theorem_fset name thm lthy = |
|
658 let |
|
659 val lifted_thm = lift_theorem_fset_aux thm lthy; |
|
660 val (_, lthy2) = note (name, lifted_thm) lthy; |
|
661 in |
|
662 lthy2 |
|
663 end; |
|
664 *} |
|
665 |
|
666 (* These do not work without proper definitions to rewrite back *) |
|
667 local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *} |
|
668 local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *} |
|
669 local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *} |
|
670 local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *} |
|
671 thm m1_lift |
|
672 thm leqi4_lift |
|
673 thm leqi5_lift |
|
674 thm m2_lift |
|
675 ML {* @{thm card1_suc_r} OF [card1_suc_f] *} |
|
676 (*ML {* Toplevel.program (fn () => lift_theorem_fset @{binding "card_suc"} |
|
677 (@{thm card1_suc_r} OF [card1_suc_f]) @{context}) *}*) |
|
678 (*local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}*) |
|
679 |
|
680 thm leqi4_lift |
|
681 ML {* |
|
682 val (nam, typ) = hd (Term.add_vars (prop_of @{thm leqi4_lift}) []) |
|
683 val (_, l) = dest_Type typ |
|
684 val t = Type ("FSet.fset", l) |
|
685 val v = Var (nam, t) |
|
686 val cv = cterm_of @{theory} ((term_of @{cpat "REP_fset"}) $ v) |
|
687 *} |
|
688 |
|
689 ML {* |
|
690 Toplevel.program (fn () => |
|
691 MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} ( |
|
692 Drule.instantiate' [] [NONE, SOME (cv)] @{thm leqi4_lift} |
|
693 ) |
|
694 ) |
|
695 *} |
|
696 |
|
697 |
|
698 |
|
699 (*prove aaa: {* (Thm.term_of cgoal2) *} |
|
700 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
|
701 apply (atomize(full)) |
|
702 apply (tactic {* transconv_fset_tac' @{context} 1 *}) |
|
703 done*) |
|
704 |
|
705 (* |
|
706 datatype obj1 = |
|
707 OVAR1 "string" |
|
708 | OBJ1 "(string * (string \<Rightarrow> obj1)) list" |
|
709 | INVOKE1 "obj1 \<Rightarrow> string" |
|
710 | UPDATE1 "obj1 \<Rightarrow> string \<Rightarrow> (string \<Rightarrow> obj1)" |
|
711 *) |
|
712 |
|
713 end |