equal
deleted
inserted
replaced
57 *} |
57 *} |
58 |
58 |
59 term append |
59 term append |
60 term UNION |
60 term UNION |
61 thm UNION_def |
61 thm UNION_def |
62 |
|
63 |
62 |
64 thm QUOTIENT_fset |
63 thm QUOTIENT_fset |
65 |
64 |
66 thm QUOT_TYPE_I_fset.thm11 |
65 thm QUOT_TYPE_I_fset.thm11 |
67 |
66 |
158 |
157 |
159 term membship |
158 term membship |
160 term IN |
159 term IN |
161 thm IN_def |
160 thm IN_def |
162 |
161 |
|
162 local_setup {* |
|
163 make_const_def @{binding fold} @{term "fold1::('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
|
164 *} |
|
165 |
|
166 term fold1 |
|
167 term fold |
|
168 thm fold_def |
|
169 |
|
170 local_setup {* |
|
171 make_const_def @{binding fmap} @{term "map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
|
172 *} |
|
173 |
|
174 term map |
|
175 term fmap |
|
176 thm fmap_def |
|
177 |
|
178 |
163 ML {* |
179 ML {* |
164 val consts = [@{const_name "Nil"}, @{const_name "Cons"}, |
180 val consts = [@{const_name "Nil"}, @{const_name "Cons"}, |
165 @{const_name "membship"}, @{const_name "card1"}, |
181 @{const_name "membship"}, @{const_name "card1"}, |
166 @{const_name "append"}, @{const_name "fold1"}]; |
182 @{const_name "append"}, @{const_name "fold1"}, |
167 *} |
183 @{const_name "map"}]; |
168 |
184 *} |
169 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *} |
185 |
|
186 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *} |
170 ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *} |
187 ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *} |
171 |
188 |
172 lemma memb_rsp: |
189 lemma memb_rsp: |
173 fixes z |
190 fixes z |
174 assumes a: "list_eq x y" |
191 assumes a: "list_eq x y" |
218 (* Need stronger induction... *) |
235 (* Need stronger induction... *) |
219 lemma "(a @ b) \<approx> (b @ a)" |
236 lemma "(a @ b) \<approx> (b @ a)" |
220 apply(induct a) |
237 apply(induct a) |
221 sorry |
238 sorry |
222 |
239 |
223 lemma (* ho_append_rsp: *) |
240 lemma ho_append_rsp: |
224 "op \<approx> ===> op \<approx> ===> op \<approx> op @ op @" |
241 "op \<approx> ===> op \<approx> ===> op \<approx> op @ op @" |
225 sorry |
242 sorry |
|
243 |
|
244 lemma map_rsp: |
|
245 assumes a: "a \<approx> b" |
|
246 shows "map f a \<approx> map f b" |
|
247 using a |
|
248 apply (induct) |
|
249 apply(auto intro: list_eq.intros) |
|
250 done |
|
251 |
|
252 lemma ho_map_rsp: |
|
253 "op = ===> op = ===> op \<approx> ===> op \<approx> map map" |
|
254 apply (simp add: FUN_REL.simps) |
|
255 apply (rule allI) |
|
256 apply (rule allI) |
|
257 apply (rule impI) |
|
258 apply (rule allI) |
|
259 apply (rule allI) |
|
260 apply (rule impI) |
|
261 sorry (* apply (auto simp add: map_rsp[of "xa" "ya"]) *) |
|
262 |
|
263 lemma map_append : |
|
264 "(map f ((a::'a list) @ b)) \<approx> |
|
265 ((map f a) ::'a list) @ (map f b)" |
|
266 apply simp |
|
267 apply (rule list_eq_refl) |
|
268 done |
226 |
269 |
227 thm list.induct |
270 thm list.induct |
228 lemma list_induct_hol4: |
271 lemma list_induct_hol4: |
229 fixes P :: "'a list \<Rightarrow> bool" |
272 fixes P :: "'a list \<Rightarrow> bool" |
230 assumes a: "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))" |
273 assumes a: "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))" |
248 |
291 |
249 (* The all_prs and ex_prs should be proved for the instance... *) |
292 (* The all_prs and ex_prs should be proved for the instance... *) |
250 ML {* |
293 ML {* |
251 fun r_mk_comb_tac_fset ctxt = |
294 fun r_mk_comb_tac_fset ctxt = |
252 r_mk_comb_tac ctxt @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
295 r_mk_comb_tac ctxt @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
253 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp} @ @{thms ho_all_prs ho_ex_prs}) |
296 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}) |
254 *} |
297 *} |
255 |
298 |
256 |
299 |
257 ML {* val thm = @{thm list_induct_r} OF [atomize_thm @{thm list_induct_hol4}] *} |
300 ML {* val thm = @{thm list_induct_r} OF [atomize_thm @{thm list_induct_hol4}] *} |
258 ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
301 ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
399 ML {* ObjectLogic.rulify qthm *} |
442 ML {* ObjectLogic.rulify qthm *} |
400 |
443 |
401 thm fold1.simps(2) |
444 thm fold1.simps(2) |
402 thm list.recs(2) |
445 thm list.recs(2) |
403 |
446 |
404 ML {* val ind_r_a = atomize_thm @{thm list_induct_hol4} *} |
447 ML {* val ind_r_a = atomize_thm @{thm map_append} *} |
405 (* prove {* build_regularize_goal ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{context} *} |
448 (* prove {* build_regularize_goal ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{context} *} |
406 ML_prf {* fun tac ctxt = |
449 ML_prf {* fun tac ctxt = |
407 (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps |
450 (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps |
408 [(@{thm equiv_res_forall} OF [@{thm equiv_list_eq}]), |
451 [(@{thm equiv_res_forall} OF [@{thm equiv_list_eq}]), |
409 (@{thm equiv_res_exists} OF [@{thm equiv_list_eq}])])) THEN_ALL_NEW |
452 (@{thm equiv_res_exists} OF [@{thm equiv_list_eq}])])) THEN_ALL_NEW |
413 ML {* val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context} *} |
456 ML {* val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context} *} |
414 ML {* |
457 ML {* |
415 val rt = build_repabs_term @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
458 val rt = build_repabs_term @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
416 val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt); |
459 val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt); |
417 *} |
460 *} |
418 (*prove rg |
461 prove rg |
419 apply(atomize(full)) |
462 apply(atomize(full)) |
420 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})*) |
463 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
464 apply (auto) |
|
465 done |
|
466 |
421 ML {* val (g, thm, othm) = |
467 ML {* val (g, thm, othm) = |
422 Toplevel.program (fn () => |
468 Toplevel.program (fn () => |
423 repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
469 repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
424 @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
470 @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
425 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp} @ @{thms ho_all_prs ho_ex_prs}) |
471 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp} @ @{thms ho_all_prs ho_ex_prs}) |
483 ML {* lift @{thm list_eq.intros(4)} *} |
529 ML {* lift @{thm list_eq.intros(4)} *} |
484 ML {* lift @{thm list_eq.intros(5)} *} |
530 ML {* lift @{thm list_eq.intros(5)} *} |
485 ML {* lift @{thm card1_suc} *} |
531 ML {* lift @{thm card1_suc} *} |
486 (* ML {* lift @{thm append_assoc} *} *) |
532 (* ML {* lift @{thm append_assoc} *} *) |
487 |
533 |
|
534 thm |
|
535 |
|
536 |
488 (*notation ( output) "prop" ("#_" [1000] 1000) *) |
537 (*notation ( output) "prop" ("#_" [1000] 1000) *) |
489 notation ( output) "Trueprop" ("#_" [1000] 1000) |
538 notation ( output) "Trueprop" ("#_" [1000] 1000) |
490 |
539 |
491 (* |
540 (* |
492 ML {* |
541 ML {* |