# HG changeset patch # User Cezary Kaliszyk # Date 1256308460 -7200 # Node ID 3da18bf6886c3a87c919e312a7072030480ab9af # Parent 20f0b148cfe23f46df110bf63ca8fc6c58d52718 Split Finite Set example into separate file 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 diff -r 20f0b148cfe2 -r 3da18bf6886c QuotMain.thy --- a/QuotMain.thy Fri Oct 23 16:01:13 2009 +0200 +++ b/QuotMain.thy Fri Oct 23 16:34:20 2009 +0200 @@ -167,83 +167,13 @@ in th' end); *} -section {* various tests for quotient types*} -datatype trm = - var "nat" -| app "trm" "trm" -| lam "nat" "trm" - -axiomatization - RR :: "trm \ trm \ bool" -where - r_eq: "EQUIV RR" - -ML {* print_quotdata @{context} *} - -quotient qtrm = trm / "RR" - apply(rule r_eq) - done - -ML {* print_quotdata @{context} *} - -typ qtrm -term Rep_qtrm -term REP_qtrm -term Abs_qtrm -term ABS_qtrm -thm QUOT_TYPE_qtrm -thm QUOTIENT_qtrm -thm REP_qtrm_def - -(* Test interpretation *) -thm QUOT_TYPE_I_qtrm.thm11 -thm QUOT_TYPE.thm11 - -print_theorems - -thm Rep_qtrm - -text {* another test *} -datatype 'a trm' = - var' "'a" -| app' "'a trm'" "'a trm'" -| lam' "'a" "'a trm'" - -consts R' :: "'a trm' \ 'a trm' \ bool" -axioms r_eq': "EQUIV R'" - -quotient qtrm' = "'a trm'" / "R'" - apply(rule r_eq') - done - -print_theorems - -term ABS_qtrm' -term REP_qtrm' -thm QUOT_TYPE_qtrm' -thm QUOTIENT_qtrm' -thm Rep_qtrm' - - -text {* a test with lists of terms *} -datatype t = - vr "string" -| ap "t list" -| lm "string" "t" - -consts Rt :: "t \ t \ bool" -axioms t_eq: "EQUIV Rt" - -quotient qt = "t" / "Rt" - by (rule t_eq) - section {* lifting of constants *} ML {* (* calculates the aggregate abs and rep functions for a given type; repF is for constants' arguments; absF is for constants; function types need to be treated specially, since repF and absF - change + change *) datatype flag = absF | repF @@ -278,8 +208,8 @@ (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty)) end - fun get_const absF = (Const ("QuotMain.ABS_" ^ qty_name, rty --> qty), (rty, qty)) - | get_const repF = (Const ("QuotMain.REP_" ^ qty_name, qty --> rty), (qty, rty)) + fun get_const absF = (Const ("FSet.ABS_" ^ qty_name, rty --> qty), (rty, qty)) + | get_const repF = (Const ("FSet.REP_" ^ qty_name, qty --> rty), (qty, rty)) fun mk_identity ty = Abs ("", ty, Bound 0) @@ -297,28 +227,6 @@ end *} -ML {* - get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt \ qt) \ qt) \ qt) list) * nat"} - |> fst - |> Syntax.string_of_term @{context} - |> writeln -*} - -ML {* - get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt * nat"} - |> fst - |> Syntax.string_of_term @{context} - |> writeln -*} - -ML {* - get_fun absF @{typ t} @{typ qt} @{context} @{typ "(qt \ qt) \ qt"} - |> fst - |> Syntax.pretty_term @{context} - |> Pretty.string_of - |> writeln -*} - text {* produces the definition for a lifted constant *} ML {* @@ -365,58 +273,6 @@ end *} -(* A test whether get_fun works properly -consts bla :: "(t \ t) \ t" -local_setup {* - fn lthy => (Toplevel.program (fn () => - make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy - )) |> snd -*} -*) - -local_setup {* - make_const_def @{binding VR} @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd #> - make_const_def @{binding AP} @{term "ap"} NoSyn @{typ "t"} @{typ "qt"} #> snd #> - make_const_def @{binding LM} @{term "lm"} NoSyn @{typ "t"} @{typ "qt"} #> snd -*} - -term vr -term ap -term lm -thm VR_def AP_def LM_def -term LM -term VR -term AP - -text {* a test with functions *} -datatype 'a t' = - vr' "string" -| ap' "('a t') * ('a t')" -| lm' "'a" "string \ ('a t')" - -consts Rt' :: "('a t') \ ('a t') \ bool" -axioms t_eq': "EQUIV Rt'" - -quotient qt' = "'a t'" / "Rt'" - apply(rule t_eq') - done - -print_theorems - -local_setup {* - make_const_def @{binding VR'} @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #> - make_const_def @{binding AP'} @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #> - make_const_def @{binding LM'} @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd -*} - -term vr' -term ap' -term ap' -thm VR'_def AP'_def LM'_def -term LM' -term VR' -term AP' - section {* ATOMIZE *} text {* @@ -506,10 +362,6 @@ | _ => HOLogic.eq_const ty) *} -ML {* - cterm_of @{theory} (tyRel @{typ "trm \ bool"} @{typ "trm"} @{term "RR"} @{context}) -*} - definition Babs :: "('a \ bool) \ ('a \ 'b) \ 'a \ 'b" where @@ -621,14 +473,6 @@ *} -ML {* - cterm_of @{theory} (regularise @{term "\x :: int. x"} @{typ "trm"} @{term "RR"} @{context}); - cterm_of @{theory} (regularise @{term "\x :: trm. x"} @{typ "trm"} @{term "RR"} @{context}); - cterm_of @{theory} (regularise @{term "\x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context}); - cterm_of @{theory} (regularise @{term "\x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context}); - cterm_of @{theory} (regularise @{term "All (P :: trm \ bool)"} @{typ "trm"} @{term "RR"} @{context}); -*} - (* my version of regularise *) (****************************) @@ -685,37 +529,6 @@ | _ => trm *} -ML {* - cterm_of @{theory} (regularise @{term "\(y::trm). P (\(x::trm). y)"} @{typ "trm"} - @{term "RR"} @{context}); - cterm_of @{theory} (my_reg @{term "RR"} @{term "\(y::trm). P (\(x::trm). y)"}) -*} - -ML {* - cterm_of @{theory} (regularise @{term "\x::trm. x"} @{typ "trm"} @{term "RR"} @{context}); - cterm_of @{theory} (my_reg @{term "RR"} @{term "\x::trm. x"}) -*} - -ML {* - cterm_of @{theory} (regularise @{term "\(x::trm) (y::trm). P x y"} @{typ "trm"} @{term "RR"} @{context}); - cterm_of @{theory} (my_reg @{term "RR"} @{term "\(x::trm) (y::trm). P x y"}) -*} - -ML {* - cterm_of @{theory} (regularise @{term "\x::trm. P x"} @{typ "trm"} @{term "RR"} @{context}); - cterm_of @{theory} (my_reg @{term "RR"} @{term "\x::trm. P x"}) -*} - -ML {* - cterm_of @{theory} (regularise @{term "\x::trm. P x"} @{typ "trm"} @{term "RR"} @{context}); - cterm_of @{theory} (my_reg @{term "RR"} @{term "\x::trm. P x"}) -*} - -(* my version is not eta-expanded, but that should be OK *) -ML {* - cterm_of @{theory} (regularise @{term "All (P::trm \ bool)"} @{typ "trm"} @{term "RR"} @{context}); - cterm_of @{theory} (my_reg @{term "RR"} @{term "All (P::trm \ bool)"}) -*} (*fun prove_reg trm \ thm (we might need some facts to do this) trm == new_trm @@ -798,717 +611,4 @@ Logic.mk_equals ((Thm.prop_of thm), (build_repabs_term ctxt thm cons rty qty)) *} - -section {* finite set example *} - -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" - -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 QuotMain.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 QuotMain.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 QuotMain.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 ("QuotMain.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 - diff -r 20f0b148cfe2 -r 3da18bf6886c QuotTest.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/QuotTest.thy Fri Oct 23 16:34:20 2009 +0200 @@ -0,0 +1,189 @@ +theory QuotTest +imports QuotMain +begin + +section {* various tests for quotient types*} +datatype trm = + var "nat" +| app "trm" "trm" +| lam "nat" "trm" + +axiomatization + RR :: "trm ⇒ trm ⇒ bool" +where + r_eq: "EQUIV RR" + +ML {* print_quotdata @{context} *} + +quotient qtrm = trm / "RR" + apply(rule r_eq) + done + +ML {* print_quotdata @{context} *} + +typ qtrm +term Rep_qtrm +term REP_qtrm +term Abs_qtrm +term ABS_qtrm +thm QUOT_TYPE_qtrm +thm QUOTIENT_qtrm +thm REP_qtrm_def + +(* Test interpretation *) +thm QUOT_TYPE_I_qtrm.thm11 +thm QUOT_TYPE.thm11 + +print_theorems + +thm Rep_qtrm + +text {* another test *} +datatype 'a trm' = + var' "'a" +| app' "'a trm'" "'a trm'" +| lam' "'a" "'a trm'" + +consts R' :: "'a trm' ⇒ 'a trm' ⇒ bool" +axioms r_eq': "EQUIV R'" + +quotient qtrm' = "'a trm'" / "R'" + apply(rule r_eq') + done + +print_theorems + +term ABS_qtrm' +term REP_qtrm' +thm QUOT_TYPE_qtrm' +thm QUOTIENT_qtrm' +thm Rep_qtrm' + + +text {* a test with lists of terms *} +datatype t = + vr "string" +| ap "t list" +| lm "string" "t" + +consts Rt :: "t ⇒ t ⇒ bool" +axioms t_eq: "EQUIV Rt" + +quotient qt = "t" / "Rt" + by (rule t_eq) + + +ML {* + get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt ⇒ qt) ⇒ qt) ⇒ qt) list) * nat"} + |> fst + |> Syntax.string_of_term @{context} + |> writeln +*} + +ML {* + get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt * nat"} + |> fst + |> Syntax.string_of_term @{context} + |> writeln +*} + +ML {* + get_fun absF @{typ t} @{typ qt} @{context} @{typ "(qt ⇒ qt) ⇒ qt"} + |> fst + |> Syntax.pretty_term @{context} + |> Pretty.string_of + |> writeln +*} + +(* A test whether get_fun works properly +consts bla :: "(t ⇒ t) ⇒ t" +local_setup {* + fn lthy => (Toplevel.program (fn () => + make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy + )) |> snd +*} +*) + +local_setup {* + make_const_def @{binding VR} @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd #> + make_const_def @{binding AP} @{term "ap"} NoSyn @{typ "t"} @{typ "qt"} #> snd #> + make_const_def @{binding LM} @{term "lm"} NoSyn @{typ "t"} @{typ "qt"} #> snd +*} + +term vr +term ap +term lm +thm VR_def AP_def LM_def +term LM +term VR +term AP + +text {* a test with functions *} +datatype 'a t' = + vr' "string" +| ap' "('a t') * ('a t')" +| lm' "'a" "string ⇒ ('a t')" + +consts Rt' :: "('a t') ⇒ ('a t') ⇒ bool" +axioms t_eq': "EQUIV Rt'" + +quotient qt' = "'a t'" / "Rt'" + apply(rule t_eq') + done + +print_theorems + +local_setup {* + make_const_def @{binding VR'} @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #> + make_const_def @{binding AP'} @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #> + make_const_def @{binding LM'} @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd +*} + +term vr' +term ap' +term ap' +thm VR'_def AP'_def LM'_def +term LM' +term VR' +term AP' + +text {* Tests of regularise *} +ML {* + cterm_of @{theory} (regularise @{term "λx :: int. x"} @{typ "trm"} @{term "RR"} @{context}); + cterm_of @{theory} (regularise @{term "λx :: trm. x"} @{typ "trm"} @{term "RR"} @{context}); + cterm_of @{theory} (regularise @{term "∀x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context}); + cterm_of @{theory} (regularise @{term "∃x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context}); + cterm_of @{theory} (regularise @{term "All (P :: trm ⇒ bool)"} @{typ "trm"} @{term "RR"} @{context}); +*} + +ML {* + cterm_of @{theory} (regularise @{term "∃(y::trm). P (λ(x::trm). y)"} @{typ "trm"} + @{term "RR"} @{context}); + cterm_of @{theory} (my_reg @{term "RR"} @{term "∃(y::trm). P (λ(x::trm). y)"}) +*} + +ML {* + cterm_of @{theory} (regularise @{term "λx::trm. x"} @{typ "trm"} @{term "RR"} @{context}); + cterm_of @{theory} (my_reg @{term "RR"} @{term "λx::trm. x"}) +*} + +ML {* + cterm_of @{theory} (regularise @{term "∀(x::trm) (y::trm). P x y"} @{typ "trm"} @{term "RR"} @{context}); + cterm_of @{theory} (my_reg @{term "RR"} @{term "∀(x::trm) (y::trm). P x y"}) +*} + +ML {* + cterm_of @{theory} (regularise @{term "∀x::trm. P x"} @{typ "trm"} @{term "RR"} @{context}); + cterm_of @{theory} (my_reg @{term "RR"} @{term "∀x::trm. P x"}) +*} + +ML {* + cterm_of @{theory} (regularise @{term "∃x::trm. P x"} @{typ "trm"} @{term "RR"} @{context}); + cterm_of @{theory} (my_reg @{term "RR"} @{term "∃x::trm. P x"}) +*} + +(* my version is not eta-expanded, but that should be OK *) +ML {* + cterm_of @{theory} (regularise @{term "All (P::trm ⇒ bool)"} @{typ "trm"} @{term "RR"} @{context}); + cterm_of @{theory} (my_reg @{term "RR"} @{term "All (P::trm ⇒ bool)"}) +*}