--- 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 "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> 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) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> 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 *})
--- 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])
--- 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 \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> 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 \<le> j \<and> \<not> j \<le> i)"
by (auto simp add: less_int_def dest: antisym)
show "i \<le> 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 \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> 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 \<le> j \<or> j \<le> 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 \<le> j \<Longrightarrow> k + i \<le> 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
--- 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 @@
\<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2);
\<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk>
\<Longrightarrow> P1 mkind \<and> P2 mty \<and> 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
--- 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 \<equiv> 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\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)"
apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *})
--- 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 \<Rightarrow> 'a \<Rightarrow> bool"
and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
- assumes equiv: "equivp R"
+ assumes equivp: "equivp R"
and rep_prop: "\<And>y. \<exists>x. Rep y = R x"
and rep_inverse: "\<And>x. Abs (Rep x) = x"
and abs_inverse: "\<And>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) \<equiv> (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 = \<lambda>x. if x \<in> p then m x else undefined
-*)
definition
Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> '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)
--- 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];
--- 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 *)