equal
deleted
inserted
replaced
132 | "fold1 f g z (a # A) = |
132 | "fold1 f g z (a # A) = |
133 (if rsp_fold f |
133 (if rsp_fold f |
134 then ( |
134 then ( |
135 if (a memb A) then (fold1 f g z A) else (f (g a) (fold1 f g z A)) |
135 if (a memb A) then (fold1 f g z A) else (f (g a) (fold1 f g z A)) |
136 ) else z)" |
136 ) else z)" |
137 |
|
138 (* fold1_def is not usable, but: *) |
|
139 thm fold1.simps |
|
140 |
137 |
141 lemma fs1_strong_cases: |
138 lemma fs1_strong_cases: |
142 fixes X :: "'a list" |
139 fixes X :: "'a list" |
143 shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a memb Y) \<and> (X \<approx> a # Y)))" |
140 shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a memb Y) \<and> (X \<approx> a # Y)))" |
144 apply (induct X) |
141 apply (induct X) |
432 INSERT2 :: "'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2" |
429 INSERT2 :: "'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2" |
433 where |
430 where |
434 "INSERT2 \<equiv> op #" |
431 "INSERT2 \<equiv> op #" |
435 |
432 |
436 ML {* val quot = @{thms QUOTIENT_fset QUOTIENT_fset2} *} |
433 ML {* val quot = @{thms QUOTIENT_fset QUOTIENT_fset2} *} |
437 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy quot [rel_refl] [trans2] *} |
434 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *} |
438 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] quot *} |
435 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *} |
439 |
436 |
440 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" |
437 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" |
441 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) |
438 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) |
442 done |
439 done |
443 |
440 |
467 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case" |
464 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case" |
468 apply (auto simp add: FUN_REL_EQ) |
465 apply (auto simp add: FUN_REL_EQ) |
469 sorry |
466 sorry |
470 |
467 |
471 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *} |
468 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *} |
472 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] quot *} |
469 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *} |
473 |
470 |
474 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)" |
471 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)" |
475 apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *}) |
472 apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *}) |
476 done |
473 done |
477 |
474 |