diff -r 20f0b148cfe2 -r 3da18bf6886c FSet.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/FSet.thy Fri Oct 23 16:34:20 2009 +0200 @@ -0,0 +1,713 @@ +theory FSet +imports QuotMain +begin + +inductive + list_eq (infix "\" 50) +where + "a#b#xs \ b#a#xs" +| "[] \ []" +| "xs \ ys \ ys \ xs" +| "a#a#xs \ a#xs" +| "xs \ ys \ a#xs \ a#ys" +| "\xs1 \ xs2; xs2 \ xs3\ \ xs1 \ xs3" + +lemma list_eq_refl: + shows "xs \ xs" + apply (induct xs) + apply (auto intro: list_eq.intros) + done + +lemma equiv_list_eq: + shows "EQUIV list_eq" + unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def + apply(auto intro: list_eq.intros list_eq_refl) + done + +quotient fset = "'a list" / "list_eq" + apply(rule equiv_list_eq) + done + +print_theorems + +typ "'a fset" +thm "Rep_fset" +thm "ABS_fset_def" + +ML {* @{term "Abs_fset"} *} +local_setup {* + make_const_def @{binding EMPTY} @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd +*} + +term Nil +term EMPTY +thm EMPTY_def + + +local_setup {* + make_const_def @{binding INSERT} @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd +*} + +term Cons +term INSERT +thm INSERT_def + +local_setup {* + make_const_def @{binding UNION} @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd +*} + +term append +term UNION +thm UNION_def + + +thm QUOTIENT_fset + +thm QUOT_TYPE_I_fset.thm11 + + +fun + membship :: "'a \ 'a list \ bool" (infix "memb" 100) +where + m1: "(x memb []) = False" +| m2: "(x memb (y#xs)) = ((x=y) \ (x memb xs))" + +fun + card1 :: "'a list \ nat" +where + card1_nil: "(card1 []) = 0" +| card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))" + +local_setup {* + make_const_def @{binding card} @{term "card1"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd +*} + +term card1 +term card +thm card_def + +(* text {* + Maybe make_const_def should require a theorem that says that the particular lifted function + respects the relation. With it such a definition would be impossible: + make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd +*}*) + +lemma card1_0: + fixes a :: "'a list" + shows "(card1 a = 0) = (a = [])" + apply (induct a) + apply (simp) + apply (simp_all) + apply meson + apply (simp_all) + done + +lemma not_mem_card1: + fixes x :: "'a" + fixes xs :: "'a list" + shows "~(x memb xs) \ card1 (x # xs) = Suc (card1 xs)" + by simp + + +lemma mem_cons: + fixes x :: "'a" + fixes xs :: "'a list" + assumes a : "x memb xs" + shows "x # xs \ xs" + using a + apply (induct xs) + apply (auto intro: list_eq.intros) + done + +lemma card1_suc: + fixes xs :: "'a list" + fixes n :: "nat" + assumes c: "card1 xs = Suc n" + shows "\a ys. ~(a memb ys) \ xs \ (a # ys)" + using c +apply(induct xs) +apply (metis Suc_neq_Zero card1_0) +apply (metis QUOT_TYPE_I_fset.R_trans card1_cons list_eq_refl mem_cons) +done + +primrec + fold1 +where + "fold1 f (g :: 'a \ 'b) (z :: 'b) [] = z" +| "fold1 f g z (a # A) = + (if ((!u v. (f u v = f v u)) + \ (!u v w. ((f u (f v w) = f (f u v) w)))) + then ( + if (a memb A) then (fold1 f g z A) else (f (g a) (fold1 f g z A)) + ) else z)" + +(* fold1_def is not usable, but: *) +thm fold1.simps + +lemma fs1_strong_cases: + fixes X :: "'a list" + shows "(X = []) \ (\a. \ Y. (~(a memb Y) \ (X \ a # Y)))" + apply (induct X) + apply (simp) + apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons m1) + done + +local_setup {* + make_const_def @{binding IN} @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd +*} + +term membship +term IN +thm IN_def + +ML {* + val consts = [@{const_name "Nil"}, @{const_name "Cons"}, + @{const_name "membship"}, @{const_name "card1"}, + @{const_name "append"}, @{const_name "fold1"}]; +*} + +ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *} +ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *} + +thm fun_map.simps +text {* Respectfullness *} + +lemma mem_respects: + fixes z + assumes a: "list_eq x y" + shows "(z memb x) = (z memb y)" + using a by induct auto + +lemma card1_rsp: + fixes a b :: "'a list" + assumes e: "a \ b" + shows "card1 a = card1 b" + using e apply induct + apply (simp_all add:mem_respects) + done + +lemma cons_preserves: + fixes z + assumes a: "xs \ ys" + shows "(z # xs) \ (z # ys)" + using a by (rule list_eq.intros(5)) + +lemma append_respects_fst: + assumes a : "list_eq l1 l2" + shows "list_eq (l1 @ s) (l2 @ s)" + using a + apply(induct) + apply(auto intro: list_eq.intros) + apply(simp add: list_eq_refl) +done + +thm list.induct +lemma list_induct_hol4: + fixes P :: "'a list \ bool" + assumes "((P []) \ (\t. (P t) \ (\h. (P (h # t)))))" + shows "(\l. (P l))" + sorry + +ML {* atomize_thm @{thm list_induct_hol4} *} + +prove list_induct_r: {* + build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a List.list"} @{term "op \"} @{context} *} + apply (simp only: equiv_res_forall[OF equiv_list_eq]) + thm RIGHT_RES_FORALL_REGULAR + apply (rule RIGHT_RES_FORALL_REGULAR) + prefer 2 + apply (assumption) + apply (metis) + done + +ML {* +fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} => +let + val pat = Drule.strip_imp_concl (cprop_of thm) + val insts = Thm.match (pat, concl) +in + rtac (Drule.instantiate insts thm) 1 +end +handle _ => no_tac +) +*} + +ML {* +fun res_forall_rsp_tac ctxt = + (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) + THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} + THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN' + (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) +*} + + +ML {* +fun quotient_tac quot_thm = + REPEAT_ALL_NEW (FIRST' [ + rtac @{thm FUN_QUOTIENT}, + rtac quot_thm, + rtac @{thm IDENTITY_QUOTIENT} + ]) +*} + +ML {* +fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm = + (FIRST' [ + rtac @{thm FUN_QUOTIENT}, + rtac quot_thm, + rtac @{thm IDENTITY_QUOTIENT}, + rtac @{thm ext}, + rtac trans_thm, + res_forall_rsp_tac ctxt, + (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), + (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), + rtac reflex_thm, + atac, + ( + (simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps})) + THEN_ALL_NEW (fn _ => no_tac) + ) + ]) +*} + +ML {* +fun r_mk_comb_tac_fset ctxt = + r_mk_comb_tac ctxt @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} +*} + + +ML {* val thm = @{thm list_induct_r} OF [atomize_thm @{thm list_induct_hol4}] *} +ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} +ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} + +prove list_induct_tr: trm_r +apply (atomize(full)) +(* APPLY_RSP_TAC *) +apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) +(* LAMBDA_RES_TAC *) +apply (simp only: FUN_REL.simps) +apply (rule allI) +apply (rule allI) +apply (rule impI) +(* MK_COMB_TAC *) +apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) +(* MK_COMB_TAC *) +apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) +(* REFL_TAC *) +apply (simp) +(* MK_COMB_TAC *) +apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) +(* MK_COMB_TAC *) +apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) +(* REFL_TAC *) +apply (simp) +(* APPLY_RSP_TAC *) +apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) +apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) +apply (simp only: FUN_REL.simps) +apply (rule allI) +apply (rule allI) +apply (rule impI) +(* MK_COMB_TAC *) +apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) +(* MK_COMB_TAC *) +apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) +(* REFL_TAC *) +apply (simp) +(* APPLY_RSP *) +apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) +(* MK_COMB_TAC *) +apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) +(* REFL_TAC *) +apply (simp) +(* W(C (curry op THEN) (G... *) +apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) +(* CONS respects *) +apply (simp add: FUN_REL.simps) +apply (rule allI) +apply (rule allI) +apply (rule allI) +apply (rule impI) +apply (rule cons_preserves) +apply (assumption) +apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) +apply (simp only: FUN_REL.simps) +apply (rule allI) +apply (rule allI) +apply (rule impI) +apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) +done + +prove list_induct_t: trm +apply (simp only: list_induct_tr[symmetric]) +apply (tactic {* rtac thm 1 *}) +done + +ML {* val nthm = MetaSimplifier.rewrite_rule fset_defs_sym (snd (no_vars (Context.Theory @{theory}, @{thm list_induct_t}))) *} + +thm list.recs(2) +thm m2 +ML {* atomize_thm @{thm m2} *} + +prove m2_r_p: {* + build_regularize_goal (atomize_thm @{thm m2}) @{typ "'a List.list"} @{term "op \"} @{context} *} + apply (simp add: equiv_res_forall[OF equiv_list_eq]) +done + +ML {* val m2_r = @{thm m2_r_p} OF [atomize_thm @{thm m2}] *} +ML {* val m2_t_g = build_repabs_goal @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *} +ML {* val m2_t = build_repabs_term @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *} +prove m2_t_p: m2_t_g +apply (atomize(full)) +apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) +apply (simp add: FUN_REL.simps) +prefer 2 +apply (simp only: FUN_REL.simps) +apply (rule allI) +apply (rule allI) +apply (rule impI) +apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) +prefer 2 +apply (simp only: FUN_REL.simps) +apply (rule allI) +apply (rule allI) +apply (rule impI) +apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) +apply (simp only: FUN_REL.simps) +apply (rule allI) +apply (rule allI) +apply (rule impI) +apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) +apply (simp only: FUN_REL.simps) +apply (rule allI) +apply (rule allI) +apply (rule impI) +apply (rule allI) +apply (rule allI) +apply (rule impI) +apply (simp add:mem_respects) +apply (simp only: FUN_REL.simps) +apply (rule allI) +apply (rule allI) +apply (rule impI) +apply (rule allI) +apply (rule allI) +apply (rule impI) +apply (simp add:cons_preserves) +apply (simp only: FUN_REL.simps) +apply (rule allI) +apply (rule allI) +apply (rule impI) +apply (rule allI) +apply (rule allI) +apply (rule impI) +apply (simp add:mem_respects) +apply (auto) +done + +prove m2_t: m2_t +apply (simp only: m2_t_p[symmetric]) +apply (tactic {* rtac m2_r 1 *}) +done + +lemma id_apply2 [simp]: "id x \ x" + by (simp add: id_def) + + +thm LAMBDA_PRS +ML {* + val t = prop_of @{thm LAMBDA_PRS} + val tt = Drule.instantiate' [SOME @{ctyp "'a list"}, SOME @{ctyp "'a fset"}] [] @{thm LAMBDA_PRS} + val ttt = @{thm LAMBDA_PRS} OF [@{thm QUOTIENT_fset}, @{thm IDENTITY_QUOTIENT}] + val tttt = @{thm "HOL.sym"} OF [ttt] +*} +ML {* + val ttttt = MetaSimplifier.rewrite_rule [@{thm id_apply2}] tttt + val zzz = @{thm m2_t} +*} + +ML {* +fun eqsubst_thm ctxt thms thm = + let + val goalstate = Goal.init (Thm.cprop_of thm) + val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of + NONE => error "eqsubst_thm" + | SOME th => cprem_of th 1 + val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1 + val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a')) + val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac)); + in + Simplifier.rewrite_rule [rt] thm + end +*} +ML {* val m2_t' = eqsubst_thm @{context} [ttttt] @{thm m2_t} *} +ML {* val rwr = @{thm FORALL_PRS[OF QUOTIENT_fset]} *} +ML {* val rwrs = @{thm "HOL.sym"} OF [ObjectLogic.rulify rwr] *} +ML {* rwrs; m2_t' *} +ML {* eqsubst_thm @{context} [rwrs] m2_t' *} +thm INSERT_def + + +ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *} + +prove card1_suc_r: {* + Logic.mk_implies + ((prop_of card1_suc_f), + (regularise (prop_of card1_suc_f) @{typ "'a List.list"} @{term "op \"} @{context})) *} + apply (simp add: equiv_res_forall[OF equiv_list_eq] equiv_res_exists[OF equiv_list_eq]) + done + +ML {* @{thm card1_suc_r} OF [card1_suc_f] *} + +ML {* val li = Thm.freezeT (atomize_thm @{thm fold1.simps(2)}) *} +prove fold1_def_2_r: {* + Logic.mk_implies + ((prop_of li), + (regularise (prop_of li) @{typ "'a List.list"} @{term "op \"} @{context})) *} + apply (simp add: equiv_res_forall[OF equiv_list_eq]) + done + +ML {* @{thm fold1_def_2_r} OF [li] *} + + +lemma yy: + shows "(False = x memb []) = (False = IN (x::nat) EMPTY)" +unfolding IN_def EMPTY_def +apply(rule_tac f="(op =) False" in arg_cong) +apply(rule mem_respects) +apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) +apply(rule list_eq.intros) +done + +lemma + shows "IN (x::nat) EMPTY = False" +using m1 +apply - +apply(rule yy[THEN iffD1, symmetric]) +apply(simp) +done + +lemma + shows "((x=y) \ (IN x xs) = (IN (x::nat) (INSERT y xs))) = + ((x=y) \ x memb REP_fset xs = x memb (y # REP_fset xs))" +unfolding IN_def INSERT_def +apply(rule_tac f="(op \) (x=y)" in arg_cong) +apply(rule_tac f="(op =) (x memb REP_fset xs)" in arg_cong) +apply(rule mem_respects) +apply(rule list_eq.intros(3)) +apply(unfold REP_fset_def ABS_fset_def) +apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset]) +apply(rule list_eq_refl) +done + +lemma yyy: + shows " + ( + (UNION EMPTY s = s) & + ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2))) + ) = ( + ((ABS_fset ([] @ REP_fset s)) = s) & + ((ABS_fset ((e # (REP_fset s1)) @ REP_fset s2)) = ABS_fset (e # (REP_fset s1 @ REP_fset s2))) + )" + unfolding UNION_def EMPTY_def INSERT_def + apply(rule_tac f="(op &)" in arg_cong2) + apply(rule_tac f="(op =)" in arg_cong2) + apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric]) + apply(rule append_respects_fst) + apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) + apply(rule list_eq_refl) + apply(simp) + apply(rule_tac f="(op =)" in arg_cong2) + apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric]) + apply(rule append_respects_fst) + apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) + apply(rule list_eq_refl) + apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric]) + apply(rule list_eq.intros(5)) + apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) + apply(rule list_eq_refl) +done + +lemma + shows " + (UNION EMPTY s = s) & + ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))" + apply (simp add: yyy) + apply (simp add: QUOT_TYPE_I_fset.thm10) + done + +ML {* + val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2})) +*} + +ML {* +cterm_of @{theory} (prop_of m1_novars); +cterm_of @{theory} (build_repabs_term @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}); +*} + + +(* Has all the theorems about fset plugged in. These should be parameters to the tactic *) +ML {* + fun transconv_fset_tac' ctxt = + (LocalDefs.unfold_tac @{context} fset_defs) THEN + ObjectLogic.full_atomize_tac 1 THEN + REPEAT_ALL_NEW (FIRST' [ + rtac @{thm list_eq_refl}, + rtac @{thm cons_preserves}, + rtac @{thm mem_respects}, + rtac @{thm card1_rsp}, + rtac @{thm QUOT_TYPE_I_fset.R_trans2}, + CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})), + Cong_Tac.cong_tac @{thm cong}, + rtac @{thm ext} + ]) 1 +*} + +ML {* + val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1})) + val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} + val cgoal = cterm_of @{theory} goal + val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) +*} + +(*notation ( output) "prop" ("#_" [1000] 1000) *) +notation ( output) "Trueprop" ("#_" [1000] 1000) + + +prove {* (Thm.term_of cgoal2) *} + apply (tactic {* transconv_fset_tac' @{context} *}) + done + +thm length_append (* Not true but worth checking that the goal is correct *) +ML {* + val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm length_append})) + val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} + val cgoal = cterm_of @{theory} goal + val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) +*} +prove {* Thm.term_of cgoal2 *} + apply (tactic {* transconv_fset_tac' @{context} *}) + sorry + +thm m2 +ML {* + val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2})) + val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} + val cgoal = cterm_of @{theory} goal + val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) +*} +prove {* Thm.term_of cgoal2 *} + apply (tactic {* transconv_fset_tac' @{context} *}) + done + +thm list_eq.intros(4) +ML {* + val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(4)})) + val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} + val cgoal = cterm_of @{theory} goal + val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) + val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2) +*} + +(* It is the same, but we need a name for it. *) +prove zzz : {* Thm.term_of cgoal3 *} + apply (tactic {* transconv_fset_tac' @{context} *}) + done + +(*lemma zzz' : + "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \ REP_fset (INSERT a (ABS_fset xs)))" + using list_eq.intros(4) by (simp only: zzz) + +thm QUOT_TYPE_I_fset.REPS_same +ML {* val zzz'' = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *} +*) + +thm list_eq.intros(5) +(* prove {* build_repabs_goal @{context} (atomize_thm @{thm list_eq.intros(5)}) consts @{typ "'a list"} @{typ "'a fset"} *} *) +ML {* + val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)})) + val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} + val cgoal = cterm_of @{theory} goal + val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) +*} +prove {* Thm.term_of cgoal2 *} + apply (tactic {* transconv_fset_tac' @{context} *}) + done + +ML {* + fun lift_theorem_fset_aux thm lthy = + let + val ((_, [novars]), lthy2) = Variable.import true [thm] lthy; + val goal = build_repabs_goal @{context} novars consts @{typ "'a list"} @{typ "'a fset"}; + val cgoal = cterm_of @{theory} goal; + val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal); + val tac = transconv_fset_tac' @{context}; + val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac); + val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm))) + val nthm2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same QUOT_TYPE_I_fset.thm10} nthm; + val [nthm3] = ProofContext.export lthy2 lthy [nthm2] + in + nthm3 + end +*} + +ML {* lift_theorem_fset_aux @{thm m1} @{context} *} + +ML {* + fun lift_theorem_fset name thm lthy = + let + val lifted_thm = lift_theorem_fset_aux thm lthy; + val (_, lthy2) = note (name, lifted_thm) lthy; + in + lthy2 + end; +*} + +(* These do not work without proper definitions to rewrite back *) +local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *} +local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *} +local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *} +local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *} +thm m1_lift +thm leqi4_lift +thm leqi5_lift +thm m2_lift +ML {* @{thm card1_suc_r} OF [card1_suc_f] *} +(*ML {* Toplevel.program (fn () => lift_theorem_fset @{binding "card_suc"} + (@{thm card1_suc_r} OF [card1_suc_f]) @{context}) *}*) +(*local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}*) + +thm leqi4_lift +ML {* + val (nam, typ) = hd (Term.add_vars (prop_of @{thm leqi4_lift}) []) + val (_, l) = dest_Type typ + val t = Type ("FSet.fset", l) + val v = Var (nam, t) + val cv = cterm_of @{theory} ((term_of @{cpat "REP_fset"}) $ v) +*} + +ML {* + Toplevel.program (fn () => + MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} ( + Drule.instantiate' [] [NONE, SOME (cv)] @{thm leqi4_lift} + ) + ) +*} + + + +(*prove aaa: {* (Thm.term_of cgoal2) *} + apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) + apply (atomize(full)) + apply (tactic {* transconv_fset_tac' @{context} 1 *}) + done*) + +(* +datatype obj1 = + OVAR1 "string" +| OBJ1 "(string * (string \ obj1)) list" +| INVOKE1 "obj1 \ string" +| UPDATE1 "obj1 \ string \ (string \ obj1)" +*) + +end