296 ML {* val rsp_thms = |
296 ML {* val rsp_thms = |
297 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} *} |
297 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} *} |
298 |
298 |
299 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
299 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
300 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *} |
300 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *} |
301 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *} |
301 ML {* fun lift_tac_fset lthy t = lift_tac lthy t *} |
302 |
302 |
303 lemma "IN x EMPTY = False" |
303 lemma "IN x EMPTY = False" |
304 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *}) |
304 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *}) |
305 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
305 apply(tactic {* regularize_tac @{context} 1 *}) |
306 apply(tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
306 apply(tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
307 apply(tactic {* clean_tac @{context} 1*}) |
307 apply(tactic {* clean_tac @{context} 1*}) |
308 done |
308 done |
309 |
309 |
310 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)" |
310 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)" |
343 |
343 |
344 |
344 |
345 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
345 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
346 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) |
346 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) |
347 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
347 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
348 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
348 apply(tactic {* regularize_tac @{context} 1 *}) |
349 defer |
349 defer |
350 apply(tactic {* clean_tac @{context} 1 *}) |
350 apply(tactic {* clean_tac @{context} 1 *}) |
351 apply(tactic {* inj_repabs_tac_fset @{context} 1*})+ |
351 apply(tactic {* inj_repabs_tac_fset @{context} 1*})+ |
352 done |
352 done |
353 |
353 |
390 where |
390 where |
391 "INSERT2 \<equiv> op #" |
391 "INSERT2 \<equiv> op #" |
392 |
392 |
393 ML {* val quot = @{thms Quotient_fset Quotient_fset2} *} |
393 ML {* val quot = @{thms Quotient_fset Quotient_fset2} *} |
394 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *} |
394 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *} |
395 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *} |
395 ML {* fun lift_tac_fset lthy t = lift_tac lthy t *} |
396 |
396 |
397 lemma "P (x :: 'a fset2) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l" |
397 lemma "P (x :: 'a fset2) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l" |
398 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) |
398 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) |
399 done |
399 done |
400 |
400 |
424 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case" |
424 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case" |
425 apply (auto) |
425 apply (auto) |
426 sorry |
426 sorry |
427 |
427 |
428 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *} |
428 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *} |
429 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *} |
429 ML {* fun lift_tac_fset lthy t = lift_tac lthy t *} |
430 |
430 |
431 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)" |
431 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)" |
432 apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *}) |
432 apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *}) |
433 done |
433 done |
434 |
434 |