# HG changeset patch # User Christian Urban # Date 1260103302 -3600 # Node ID a082e2d138abdd618b0a2ecd3d4409a45a3cf21d # Parent 070161f1996a807d1b8c2704a835da73ebcd8dc6 added a theorem list for equivalence theorems diff -r 070161f1996a -r a082e2d138ab FSet.thy --- a/FSet.thy Sun Dec 06 11:39:34 2009 +0100 +++ b/FSet.thy Sun Dec 06 13:41:42 2009 +0100 @@ -298,11 +298,11 @@ ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *} -ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *} +ML {* fun lift_tac_fset lthy t = lift_tac lthy t *} lemma "IN x EMPTY = False" apply(tactic {* procedure_tac @{context} @{thm m1} 1 *}) -apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) +apply(tactic {* regularize_tac @{context} 1 *}) apply(tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) apply(tactic {* clean_tac @{context} 1*}) done @@ -345,7 +345,7 @@ lemma "\P EMPTY; \a x. P x \ P (INSERT a x)\ \ P l" apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) -apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) +apply(tactic {* regularize_tac @{context} 1 *}) defer apply(tactic {* clean_tac @{context} 1 *}) apply(tactic {* inj_repabs_tac_fset @{context} 1*})+ @@ -392,7 +392,7 @@ ML {* val quot = @{thms Quotient_fset Quotient_fset2} *} ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *} -ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *} +ML {* fun lift_tac_fset lthy t = lift_tac lthy t *} lemma "P (x :: 'a fset2) (EMPTY :: 'c fset) \ (\e t. P x t \ P x (INSERT e t)) \ P x l" apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) @@ -426,7 +426,7 @@ sorry ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *} -ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *} +ML {* fun lift_tac_fset lthy t = lift_tac lthy t *} lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)" apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *}) diff -r 070161f1996a -r a082e2d138ab IntEx.thy --- a/IntEx.thy Sun Dec 06 11:39:34 2009 +0100 +++ b/IntEx.thy Sun Dec 06 13:41:42 2009 +0100 @@ -12,6 +12,8 @@ apply(auto simp add: mem_def expand_fun_eq) done +thm quotient_equiv + thm quotient_thm thm my_int_equivp @@ -138,7 +140,7 @@ ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *} -ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] *} +ML {* fun lift_tac_intex lthy t = lift_tac lthy t *} ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [rel_refl] [trans2] *} ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [rel_refl] [trans2] *} @@ -178,11 +180,9 @@ done *) - - lemma "PLUS a b = PLUS a b" apply(tactic {* procedure_tac @{context} @{thm test1} 1 *}) -apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) +apply(tactic {* regularize_tac @{context} 1 *}) apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) apply(tactic {* clean_tac @{context} 1 *}) done @@ -214,7 +214,7 @@ lemma "PLUS a b = PLUS b a" apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) -apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) +apply(tactic {* regularize_tac @{context} 1 *}) apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) apply(tactic {* clean_tac @{context} 1 *}) done @@ -229,7 +229,7 @@ lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)" apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) -apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) +apply(tactic {* regularize_tac @{context} 1 *}) apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) apply(tactic {* clean_tac @{context} 1 *}) done @@ -240,7 +240,7 @@ lemma "foldl PLUS x [] = x" apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) -apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) +apply(tactic {* regularize_tac @{context} 1 *}) apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) apply(tactic {* clean_tac @{context} 1 *}) apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int]) @@ -251,7 +251,7 @@ lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)" apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *}) -apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) +apply(tactic {* regularize_tac @{context} 1 *}) apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) apply(tactic {* clean_tac @{context} 1 *}) apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] cons_prs[OF Quotient_my_int]) diff -r 070161f1996a -r a082e2d138ab IntEx2.thy --- a/IntEx2.thy Sun Dec 06 11:39:34 2009 +0100 +++ b/IntEx2.thy Sun Dec 06 13:41:42 2009 +0100 @@ -171,16 +171,16 @@ fix i j k :: int show "(i + j) + k = i + (j + k)" unfolding add_int_def - apply(tactic {* lift_tac @{context} @{thm plus_assoc_raw} [@{thm int_equivp}] 1 *}) + apply(tactic {* lift_tac @{context} @{thm plus_assoc_raw} 1 *}) done show "i + j = j + i" unfolding add_int_def - apply(tactic {* lift_tac @{context} @{thm plus_sym_raw} [@{thm int_equivp}] 1 *}) + apply(tactic {* lift_tac @{context} @{thm plus_sym_raw} 1 *}) done show "0 + i = (i::int)" unfolding add_int_def Zero_int_def apply(tactic {* procedure_tac @{context} @{thm plus_zero_raw} 1 *}) - apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *}) + apply(tactic {* regularize_tac @{context} 1 *}) apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) defer apply(tactic {* clean_tac @{context} 1*}) @@ -188,7 +188,7 @@ show "- i + i = 0" unfolding add_int_def minus_int_def Zero_int_def apply(tactic {* procedure_tac @{context} @{thm plus_minus_zero_raw} 1 *}) - apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *}) + apply(tactic {* regularize_tac @{context} 1 *}) apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) defer apply(tactic {* clean_tac @{context} 1*}) @@ -198,7 +198,7 @@ show "(i * j) * k = i * (j * k)" unfolding mult_int_def apply(tactic {* procedure_tac @{context} @{thm mult_assoc_raw} 1 *}) - apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *}) + apply(tactic {* regularize_tac @{context} 1 *}) apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) defer apply(tactic {* clean_tac @{context} 1*}) @@ -206,7 +206,7 @@ show "i * j = j * i" unfolding mult_int_def apply(tactic {* procedure_tac @{context} @{thm mult_sym_raw} 1 *}) - apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *}) + apply(tactic {* regularize_tac @{context} 1 *}) apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) defer apply(tactic {* clean_tac @{context} 1*}) @@ -214,7 +214,7 @@ show "1 * i = i" unfolding mult_int_def One_int_def apply(tactic {* procedure_tac @{context} @{thm mult_one_raw} 1 *}) - apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *}) + apply(tactic {* regularize_tac @{context} 1 *}) apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) defer apply(tactic {* clean_tac @{context} 1*}) @@ -222,7 +222,7 @@ show "(i + j) * k = i * k + j * k" unfolding mult_int_def add_int_def apply(tactic {* procedure_tac @{context} @{thm mult_plus_comm_raw} 1 *}) - apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *}) + apply(tactic {* regularize_tac @{context} 1 *}) apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) defer apply(tactic {* clean_tac @{context} 1*}) @@ -269,21 +269,21 @@ fix i j k :: int show antisym: "i \ j \ j \ i \ i = j" unfolding le_int_def - apply(tactic {* lift_tac @{context} @{thm le_antisym_raw} [@{thm int_equivp}] 1 *}) + apply(tactic {* lift_tac @{context} @{thm le_antisym_raw} 1 *}) done show "(i < j) = (i \ j \ \ j \ i)" by (auto simp add: less_int_def dest: antisym) show "i \ i" unfolding le_int_def - apply(tactic {* lift_tac @{context} @{thm le_refl_raw} [@{thm int_equivp}] 1 *}) + apply(tactic {* lift_tac @{context} @{thm le_refl_raw} 1 *}) done show "i \ j \ j \ k \ i \ k" unfolding le_int_def - apply(tactic {* lift_tac @{context} @{thm le_trans_raw} [@{thm int_equivp}] 1 *}) + apply(tactic {* lift_tac @{context} @{thm le_trans_raw} 1 *}) done show "i \ j \ j \ i" unfolding le_int_def - apply(tactic {* lift_tac @{context} @{thm le_cases_raw} [@{thm int_equivp}] 1 *}) + apply(tactic {* lift_tac @{context} @{thm le_cases_raw} 1 *}) done qed @@ -312,7 +312,7 @@ fix i j k :: int show "i \ j \ k + i \ k + j" unfolding le_int_def add_int_def - apply(tactic {* lift_tac @{context} @{thm le_plus_raw} [@{thm int_equivp}] 1 *}) + apply(tactic {* lift_tac @{context} @{thm le_plus_raw} 1 *}) done qed diff -r 070161f1996a -r a082e2d138ab LFex.thy --- a/LFex.thy Sun Dec 06 11:39:34 2009 +0100 +++ b/LFex.thy Sun Dec 06 13:41:42 2009 +0100 @@ -258,7 +258,7 @@ using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 apply - apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) -apply(tactic {* regularize_tac @{context} @{thms alpha_equivps} 1 *}) +apply(tactic {* regularize_tac @{context} 1 *}) apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *}) apply(fold perm_kind_def perm_ty_def perm_trm_def) apply(tactic {* clean_tac @{context} 1 *}) @@ -296,7 +296,7 @@ \trm1 trm2. \P3 trm1; P3 trm2\ \ P3 (APP trm1 trm2); \ty name trm. \P2 ty; P3 trm\ \ P3 (LAM ty name trm)\ \ P1 mkind \ P2 mty \ P3 mtrm" -apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} @{thms alpha_equivps} 1 *}) +apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} 1 *}) done print_quotients diff -r 070161f1996a -r a082e2d138ab LamEx.thy --- a/LamEx.thy Sun Dec 06 11:39:34 2009 +0100 +++ b/LamEx.thy Sun Dec 06 13:41:42 2009 +0100 @@ -80,35 +80,6 @@ where "fv \ rfv" -ML {* -local - fun pp_pair (x, y) = Pretty.list "(" ")" [x, y] - fun pp_list xs = Pretty.list "[" "]" xs - fun pp_str s = Pretty.str s - fun pp_qstr s = Pretty.quote (pp_str s) - fun pp_int i = pp_str (string_of_int i) - fun pp_sort S = pp_list (map pp_qstr S) - fun pp_constr a args = Pretty.block [pp_str a, Pretty.brk 1, args] -in -fun raw_pp_typ (TVar ((a, i), S)) = - pp_constr "TVar" (pp_pair (pp_pair (pp_qstr a, pp_int i), pp_sort S)) - | raw_pp_typ (TFree (a, S)) = - pp_constr "TFree" (pp_pair (pp_qstr a, pp_sort S)) - | raw_pp_typ (Type (a, tys)) = - pp_constr "Type" (pp_pair (pp_qstr a, pp_list (map raw_pp_typ tys))) -end *} - -ML {* -PolyML.addPrettyPrinter - (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ) - -*} - -typ "name set" -typ "name => bool" - -ML {* @{typ "name set"} *} - thm fv_def (* definition of overloaded permutation function *) @@ -203,7 +174,7 @@ ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} -ML {* fun lift_tac_lam lthy t = lift_tac lthy t [rel_eqv] *} +ML {* fun lift_tac_lam lthy t = lift_tac lthy t *} lemma pi_var: "(pi\('x \ 'x) list) \ Var a = Var (pi \ a)" apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *}) diff -r 070161f1996a -r a082e2d138ab QuotMain.thy --- a/QuotMain.thy Sun Dec 06 11:39:34 2009 +0100 +++ b/QuotMain.thy Sun Dec 06 13:41:42 2009 +0100 @@ -5,11 +5,12 @@ ("quotient_def.ML") begin + locale QUOT_TYPE = fixes R :: "'a \ 'a \ bool" and Abs :: "('a \ bool) \ 'b" and Rep :: "'b \ ('a \ bool)" - assumes equiv: "equivp R" + assumes equivp: "equivp R" and rep_prop: "\y. \x. Rep y = R x" and rep_inverse: "\x. Abs (Rep x) = x" and abs_inverse: "\x. (Rep (Abs (R x))) = (R x)" @@ -29,10 +30,10 @@ lemma lem9: shows "R (Eps (R x)) = R x" proof - - have a: "R x x" using equiv by (simp add: equivp_reflp_symp_transp reflp_def) + have a: "R x x" using equivp by (simp add: equivp_reflp_symp_transp reflp_def) then have "R x (Eps (R x))" by (rule someI) then show "R (Eps (R x)) = R x" - using equiv unfolding equivp_def by simp + using equivp unfolding equivp_def by simp qed theorem thm10: @@ -53,7 +54,7 @@ lemma REP_refl: shows "R (REP a) (REP a)" unfolding REP_def -by (simp add: equiv[simplified equivp_def]) +by (simp add: equivp[simplified equivp_def]) lemma lem7: shows "(R x = R y) = (Abs (R x) = Abs (R y))" @@ -66,7 +67,7 @@ theorem thm11: shows "R r r' = (ABS r = ABS r')" unfolding ABS_def -by (simp only: equiv[simplified equivp_def] lem7) +by (simp only: equivp[simplified equivp_def] lem7) lemma REP_ABS_rsp: @@ -80,7 +81,7 @@ apply(simp add: thm10) apply(simp add: REP_refl) apply(subst thm11[symmetric]) -apply(simp add: equiv[simplified equivp_def]) +apply(simp add: equivp[simplified equivp_def]) done lemma R_trans: @@ -88,7 +89,7 @@ and bc: "R b c" shows "R a c" proof - - have tr: "transp R" using equiv equivp_reflp_symp_transp[of R] by simp + have tr: "transp R" using equivp equivp_reflp_symp_transp[of R] by simp moreover have ab: "R a b" by fact moreover have bc: "R b c" by fact ultimately show "R a c" unfolding transp_def by blast @@ -98,7 +99,7 @@ assumes ab: "R a b" shows "R b a" proof - - have re: "symp R" using equiv equivp_reflp_symp_transp[of R] by simp + have re: "symp R" using equivp equivp_reflp_symp_transp[of R] by simp then show "R b a" using ab unfolding symp_def by blast qed @@ -128,7 +129,7 @@ then show "a = b" using rep_inverse by simp next assume ab: "a = b" - have "reflp R" using equiv equivp_reflp_symp_transp[of R] by simp + have "reflp R" using equivp equivp_reflp_symp_transp[of R] by simp then show "R (REP a) (REP b)" unfolding reflp_def using ab by auto qed then show "R (REP a) (REP b) \ (a = b)" by simp @@ -151,6 +152,11 @@ lemmas [quotient_rsp] = quot_rel_rsp nil_rsp cons_rsp foldl_rsp +(* OPTION, PRODUCTS *) +lemmas [quotient_equiv] = + identity_equivp list_equivp + + ML {* maps_lookup @{theory} "List.list" *} ML {* maps_lookup @{theory} "*" *} ML {* maps_lookup @{theory} "fun" *} @@ -164,9 +170,6 @@ (* lifting of constants *) use "quotient_def.ML" -(* TODO: Consider defining it with an "if"; sth like: - Babs p m = \x. if x \ p then m x else undefined -*) definition Babs :: "('a \ bool) \ ('a \ 'b) \ 'a \ 'b" where @@ -240,7 +243,6 @@ Seq.single thm end *} - ML {* fun DT ctxt s tac i thm = let @@ -494,19 +496,14 @@ *) -(* FIXME: OPTION_equivp, PAIR_equivp, ... *) ML {* -fun equiv_tac rel_eqvs = +fun equiv_tac ctxt = REPEAT_ALL_NEW (FIRST' - [resolve_tac rel_eqvs, - rtac @{thm identity_equivp}, - rtac @{thm list_equivp}]) + [resolve_tac (equiv_rules_get ctxt)]) *} -thm ball_reg_eqv - ML {* -fun ball_reg_eqv_simproc rel_eqvs ss redex = +fun ball_reg_eqv_simproc ss redex = let val ctxt = Simplifier.the_context ss val thy = ProofContext.theory_of ctxt @@ -517,7 +514,7 @@ (let val gl = Const (@{const_name "equivp"}, dummyT) $ R; val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); - val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); + val eqv = Goal.prove ctxt [] [] glc (fn {context,...} => equiv_tac context 1) val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv} OF [eqv]]); (* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *) in @@ -530,7 +527,7 @@ *} ML {* -fun bex_reg_eqv_simproc rel_eqvs ss redex = +fun bex_reg_eqv_simproc ss redex = let val ctxt = Simplifier.the_context ss val thy = ProofContext.theory_of ctxt @@ -541,7 +538,7 @@ (let val gl = Const (@{const_name "equivp"}, dummyT) $ R; val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); - val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); + val eqv = Goal.prove ctxt [] [] glc (fn {context,...} => equiv_tac context 1) val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv} OF [eqv]]); (* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *) in @@ -574,7 +571,7 @@ *} ML {* -fun ball_reg_eqv_range_simproc rel_eqvs ss redex = +fun ball_reg_eqv_range_simproc ss redex = let val ctxt = Simplifier.the_context ss val thy = ProofContext.theory_of ctxt @@ -586,7 +583,7 @@ val gl = Const (@{const_name "equivp"}, dummyT) $ R2; val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); (* val _ = tracing (Syntax.string_of_term ctxt glc);*) - val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); + val eqv = Goal.prove ctxt [] [] glc (fn {context,...} => equiv_tac context 1) val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv_range} OF [eqv]]); val R1c = cterm_of thy R1; val thmi = Drule.instantiate' [] [SOME R1c] thm; @@ -608,7 +605,7 @@ thm bex_reg_eqv_range ML {* -fun bex_reg_eqv_range_simproc rel_eqvs ss redex = +fun bex_reg_eqv_range_simproc ss redex = let val ctxt = Simplifier.the_context ss val thy = ProofContext.theory_of ctxt @@ -620,7 +617,7 @@ val gl = Const (@{const_name "equivp"}, dummyT) $ R2; val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); (* val _ = tracing (Syntax.string_of_term ctxt glc); *) - val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); + val eqv = Goal.prove ctxt [] [] glc (fn {context,...} => equiv_tac context 1) val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv_range} OF [eqv]]); val R1c = cterm_of thy R1; val thmi = Drule.instantiate' [] [SOME R1c] thm; @@ -642,20 +639,20 @@ by (simp add: equivp_reflp) ML {* -fun regularize_tac ctxt rel_eqvs = +fun regularize_tac ctxt = let val pat1 = [@{term "Ball (Respects R) P"}]; val pat2 = [@{term "Bex (Respects R) P"}]; val pat3 = [@{term "Ball (Respects (R1 ===> R2)) P"}]; val pat4 = [@{term "Bex (Respects (R1 ===> R2)) P"}]; val thy = ProofContext.theory_of ctxt - val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc rel_eqvs)) - val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc rel_eqvs)) - val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc rel_eqvs)) - val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc rel_eqvs)) + val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc)) + val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc)) + val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc)) + val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc)) val simp_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2, simproc3, simproc4] (* TODO: Make sure that there are no list_rel, pair_rel etc involved *) - val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) rel_eqvs + val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt) in ObjectLogic.full_atomize_tac THEN' simp_tac simp_ctxt THEN' @@ -1221,21 +1218,21 @@ ML {* (* FIXME/TODO should only get as arguments the rthm like procedure_tac *) -fun lift_tac ctxt rthm rel_eqv = +fun lift_tac ctxt rthm = ObjectLogic.full_atomize_tac THEN' gen_frees_tac ctxt THEN' CSUBGOAL (fn (gl, i) => let val rthm' = atomize_thm rthm val rule = procedure_inst ctxt (prop_of rthm') (term_of gl) - val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) rel_eqv + val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) (equiv_rules_get ctxt) val quotients = quotient_rules_get ctxt val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quotients val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb gl))] @{thm QUOT_TRUE_i} in (rtac rule THEN' RANGE [rtac rthm', - regularize_tac ctxt rel_eqv, + regularize_tac ctxt, rtac thm THEN' all_inj_repabs_tac ctxt rel_refl trans2, clean_tac ctxt]) i end) diff -r 070161f1996a -r a082e2d138ab quotient.ML --- a/quotient.ML Sun Dec 06 11:39:34 2009 +0100 +++ b/quotient.ML Sun Dec 06 13:41:42 2009 +0100 @@ -28,6 +28,8 @@ (thm', lthy') end +fun internal_attr at = Attrib.internal (K at) + fun theorem after_qed goals ctxt = let val goals' = map (rpair []) goals @@ -157,7 +159,8 @@ (* FIXME: to recalculated in for example REGULARIZE *) (* storing of the equiv_thm under a name *) - val (_, lthy4) = note (Binding.suffix_name "_equivp" qty_name, equiv_thm, []) lthy3 + val (_, lthy4) = note (Binding.suffix_name "_equivp" qty_name, equiv_thm, + [internal_attr equiv_rules_add]) lthy3 (* interpretation *) val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) @@ -179,7 +182,7 @@ in lthy6 |> note (quot_thm_name, quot_thm, []) - ||>> note (quotient_thm_name, quotient_thm, [Attrib.internal (K quotient_rules_add)]) + ||>> note (quotient_thm_name, quotient_thm, [internal_attr quotient_rules_add]) ||> Local_Theory.theory (fn thy => let val global_eqns = map exp_term [eqn2i, eqn1i]; diff -r 070161f1996a -r a082e2d138ab quotient_info.ML --- a/quotient_info.ML Sun Dec 06 11:39:34 2009 +0100 +++ b/quotient_info.ML Sun Dec 06 13:41:42 2009 +0100 @@ -23,6 +23,8 @@ val qconsts_dest: theory -> qconsts_info list val print_qconstinfo: Proof.context -> unit + val equiv_rules_get: Proof.context -> thm list + val equiv_rules_add: attribute val rsp_rules_get: Proof.context -> thm list val quotient_rules_get: Proof.context -> thm list val quotient_rules_add: attribute @@ -168,24 +170,33 @@ OuterSyntax.improper_command "print_quotconsts" "print out all quotient constants" OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of))) -(* respectfulness lemmas *) +(* equivalence relation theorems *) +structure EquivRules = Named_Thms + (val name = "quotient_equiv" + val description = "Equivalence relation theorems.") + +val equiv_rules_get = EquivRules.get +val equiv_rules_add = EquivRules.add + +(* respectfulness theorems *) structure RspRules = Named_Thms (val name = "quotient_rsp" val description = "Respectfulness theorems.") val rsp_rules_get = RspRules.get -(* quotient lemmas *) +(* quotient theorems *) structure QuotientRules = Named_Thms (val name = "quotient_thm" val description = "Quotient theorems.") val quotient_rules_get = QuotientRules.get -val quotient_rules_add = Thm.declaration_attribute QuotientRules.add_thm +val quotient_rules_add = QuotientRules.add (* setup of the theorem lists *) val _ = Context.>> (Context.map_theory - (RspRules.setup #> + (EquivRules.setup #> + RspRules.setup #> QuotientRules.setup)) end; (* structure *)