--- a/FIXME-TODO Thu Dec 03 14:02:05 2009 +0100
+++ b/FIXME-TODO Thu Dec 03 15:03:31 2009 +0100
@@ -24,7 +24,15 @@
Lower Priority
==============
+- allow the user to provide the rsp lemmas in a more
+ natural form
+
- find clean ways how to write down the "mathematical"
procedure for a possible submission (Peter submitted
his work only to TPHOLs 2005...we would have to go
- maybe for the Journal of Formalised Mathematics)
\ No newline at end of file
+ maybe for the Journal of Formalised Mathematics)
+
+- use lower-case letters where appropriate in order
+ to make Markus happy
+
+- add tests for adding theorems to the various thm lists
\ No newline at end of file
--- a/FSet.thy Thu Dec 03 14:02:05 2009 +0100
+++ b/FSet.thy Thu Dec 03 15:03:31 2009 +0100
@@ -180,7 +180,7 @@
shows "(z memb x) = (z memb y)"
using a by induct auto
-lemma ho_memb_rsp[quot_rsp]:
+lemma ho_memb_rsp[quotient_rsp]:
"(op = ===> (op \<approx> ===> op =)) (op memb) (op memb)"
by (simp add: memb_rsp)
@@ -190,17 +190,17 @@
shows "card1 a = card1 b"
using e by induct (simp_all add:memb_rsp)
-lemma ho_card1_rsp[quot_rsp]:
+lemma ho_card1_rsp[quotient_rsp]:
"(op \<approx> ===> op =) card1 card1"
by (simp add: card1_rsp)
-lemma cons_rsp[quot_rsp]:
+lemma cons_rsp[quotient_rsp]:
fixes z
assumes a: "xs \<approx> ys"
shows "(z # xs) \<approx> (z # ys)"
using a by (rule list_eq.intros(5))
-lemma ho_cons_rsp[quot_rsp]:
+lemma ho_cons_rsp[quotient_rsp]:
"(op = ===> op \<approx> ===> op \<approx>) op # op #"
by (simp add: cons_rsp)
@@ -257,7 +257,7 @@
apply (rule append_sym_rsp)
done
-lemma ho_append_rsp[quot_rsp]:
+lemma ho_append_rsp[quotient_rsp]:
"(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
by (simp add: append_rsp)
@@ -269,7 +269,7 @@
apply(auto intro: list_eq.intros)
done
-lemma ho_map_rsp[quot_rsp]:
+lemma ho_map_rsp[quotient_rsp]:
"(op = ===> op \<approx> ===> op \<approx>) map map"
by (simp add: map_rsp)
@@ -277,7 +277,7 @@
"(map f (a @ b)) \<approx> (map f a) @ (map f b)"
by simp (rule list_eq_refl)
-lemma ho_fold_rsp[quot_rsp]:
+lemma ho_fold_rsp[quotient_rsp]:
"(op = ===> op = ===> op = ===> op \<approx> ===> op =) fold1 fold1"
apply (auto simp add: FUN_REL_EQ)
apply (case_tac "rsp_fold x")
@@ -297,13 +297,13 @@
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] [quot] *}
+ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *}
lemma "IN x EMPTY = False"
apply(tactic {* procedure_tac @{context} @{thm m1} 1 *})
apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply(tactic {* clean_tac @{context} [quot] 1*})
+apply(tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply(tactic {* clean_tac @{context} 1*})
done
lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)"
@@ -330,7 +330,7 @@
apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
done
-ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [quot] [rel_refl] [trans2] *}
+ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *})
@@ -348,7 +348,7 @@
apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
prefer 2
-apply(tactic {* clean_tac @{context} [quot] 1 *})
+apply(tactic {* clean_tac @{context} 1 *})
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
@@ -404,6 +404,9 @@
apply (assumption)
done
+ML {* quot *}
+thm quotient_thm
+
lemma "P (x :: 'a list) (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 *})
done
@@ -453,14 +456,14 @@
"fset_case \<equiv> list_case"
(* Probably not true without additional assumptions about the function *)
-lemma list_rec_rsp[quot_rsp]:
+lemma list_rec_rsp[quotient_rsp]:
"(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec"
apply (auto simp add: FUN_REL_EQ)
apply (erule_tac list_eq.induct)
apply (simp_all)
sorry
-lemma list_case_rsp[quot_rsp]:
+lemma list_case_rsp[quotient_rsp]:
"(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
apply (auto simp add: FUN_REL_EQ)
sorry
--- a/IntEx.thy Thu Dec 03 14:02:05 2009 +0100
+++ b/IntEx.thy Thu Dec 03 15:03:31 2009 +0100
@@ -13,6 +13,8 @@
apply(auto simp add: mem_def expand_fun_eq)
done
+thm quotient_thm
+
thm my_int_equiv
print_theorems
@@ -129,7 +131,7 @@
apply(auto)
done
-lemma ho_plus_rsp[quot_rsp]:
+lemma ho_plus_rsp[quotient_rsp]:
shows "(intrel ===> intrel ===> intrel) my_plus my_plus"
by (simp)
@@ -139,17 +141,17 @@
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] [quot] *}
+ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] *}
-ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [quot] [rel_refl] [trans2] *}
-ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [quot] [rel_refl] [trans2] *}
+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] *}
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 *})
prefer 2
-apply(tactic {* clean_tac @{context} [quot] 1 *})
+apply(tactic {* clean_tac @{context} 1 *})
apply(tactic {* inj_repabs_tac_intex @{context} 1*})
apply(tactic {* inj_repabs_tac_intex @{context} 1*})
apply(tactic {* inj_repabs_tac_intex @{context} 1*})
@@ -187,7 +189,7 @@
apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* clean_tac @{context} [quot] 1 *})
+apply(tactic {* clean_tac @{context} 1 *})
done
lemma ho_tst: "foldl my_plus x [] = x"
@@ -234,12 +236,12 @@
apply (induct t)
by (simp_all add: QUOTIENT_ABS_REP[OF a])
-lemma cons_rsp[quot_rsp]:
+lemma cons_rsp[quotient_rsp]:
"(op \<approx> ===> LIST_REL op \<approx> ===> LIST_REL op \<approx>) op # op #"
by simp
(* I believe it's true. *)
-lemma foldl_rsp[quot_rsp]:
+lemma foldl_rsp[quotient_rsp]:
"((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> LIST_REL op \<approx> ===> op \<approx>) foldl foldl"
apply (simp only: FUN_REL.simps)
apply (rule allI)
@@ -254,37 +256,17 @@
apply (induct_tac xb yb rule: list_induct2) (* To finish I need to give it: arbitrary:xa ya *)
sorry
-lemma nil_listrel_rsp[quot_rsp]:
+lemma nil_listrel_rsp[quotient_rsp]:
"(LIST_REL R) [] []"
by simp
-thm LAMBDA_PRS[no_vars]
-thm all_prs[no_vars]
-
-lemma test_all_prs:
- "\<lbrakk>QUOTIENT R absf repf; f = g\<rbrakk> \<Longrightarrow> Ball (Respects R) ((absf ---> id) f) = All g"
-apply(drule all_prs)
-apply(simp)
-done
-
-lemma test:
- "\<lbrakk>QUOTIENT R1 Abs1 Rep1; QUOTIENT R2 Abs2 Rep2;
- (\<lambda>x. Rep2 (f (Abs1 x))) = lhs \<rbrakk> \<Longrightarrow> (Rep1 ---> Abs2) lhs = f"
-apply -
-thm LAMBDA_PRS
-apply(drule LAMBDA_PRS)
-apply(assumption)
-apply(auto)
-done
-
-
lemma "foldl PLUS x [] = x"
apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *})
apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int])
apply(simp only: nil_prs)
-apply(tactic {* clean_tac @{context} [quot] 1 *})
+apply(tactic {* clean_tac @{context} 1 *})
done
lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)"
@@ -296,6 +278,6 @@
apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int])
apply(simp only: cons_prs[OF QUOTIENT_my_int])
-apply(tactic {* clean_tac @{context} [quot] 1 *})
+apply(tactic {* clean_tac @{context} 1 *})
done
--- a/LFex.thy Thu Dec 03 14:02:05 2009 +0100
+++ b/LFex.thy Thu Dec 03 15:03:31 2009 +0100
@@ -181,35 +181,35 @@
"perm_trm \<equiv> (perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)"
(* TODO/FIXME: Think whether these RSP theorems are true. *)
-lemma kpi_rsp[quot_rsp]:
+lemma kpi_rsp[quotient_rsp]:
"(aty ===> op = ===> akind ===> akind) KPi KPi" sorry
-lemma tconst_rsp[quot_rsp]:
+lemma tconst_rsp[quotient_rsp]:
"(op = ===> aty) TConst TConst" sorry
-lemma tapp_rsp[quot_rsp]:
+lemma tapp_rsp[quotient_rsp]:
"(aty ===> atrm ===> aty) TApp TApp" sorry
-lemma tpi_rsp[quot_rsp]:
+lemma tpi_rsp[quotient_rsp]:
"(aty ===> op = ===> aty ===> aty) TPi TPi" sorry
-lemma var_rsp[quot_rsp]:
+lemma var_rsp[quotient_rsp]:
"(op = ===> atrm) Var Var" sorry
-lemma app_rsp[quot_rsp]:
+lemma app_rsp[quotient_rsp]:
"(atrm ===> atrm ===> atrm) App App" sorry
-lemma const_rsp[quot_rsp]:
+lemma const_rsp[quotient_rsp]:
"(op = ===> atrm) Const Const" sorry
-lemma lam_rsp[quot_rsp]:
+lemma lam_rsp[quotient_rsp]:
"(aty ===> op = ===> atrm ===> atrm) Lam Lam" sorry
-lemma perm_kind_rsp[quot_rsp]:
+lemma perm_kind_rsp[quotient_rsp]:
"(op = ===> akind ===> akind) op \<bullet> op \<bullet>" sorry
-lemma perm_ty_rsp[quot_rsp]:
+lemma perm_ty_rsp[quotient_rsp]:
"(op = ===> aty ===> aty) op \<bullet> op \<bullet>" sorry
-lemma perm_trm_rsp[quot_rsp]:
+lemma perm_trm_rsp[quotient_rsp]:
"(op = ===> atrm ===> atrm) op \<bullet> op \<bullet>" sorry
-lemma fv_ty_rsp[quot_rsp]:
+lemma fv_ty_rsp[quotient_rsp]:
"(aty ===> op =) fv_ty fv_ty" sorry
-lemma fv_kind_rsp[quot_rsp]:
+lemma fv_kind_rsp[quotient_rsp]:
"(akind ===> op =) fv_kind fv_kind" sorry
-lemma fv_trm_rsp[quot_rsp]:
+lemma fv_trm_rsp[quotient_rsp]:
"(atrm ===> op =) fv_trm fv_trm" sorry
@@ -261,7 +261,7 @@
apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})
apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
prefer 2
-apply(tactic {* clean_tac @{context} quot 1 *})
+apply(tactic {* clean_tac @{context} 1 *})
(*
Profiling:
ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *}
@@ -270,7 +270,7 @@
ML_prf {* PolyML.profiling 1 *}
ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *}
*)
-apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})
done
(* Does not work:
@@ -299,8 +299,8 @@
\<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm"
apply(tactic {* procedure_tac @{context} @{thm kind_ty_trm.induct} 1 *})
apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1 *})
-apply(tactic {* clean_tac @{context} quot 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})
+apply(tactic {* clean_tac @{context} 1 *})
done
print_quotients
--- a/QuotMain.thy Thu Dec 03 14:02:05 2009 +0100
+++ b/QuotMain.thy Thu Dec 03 15:03:31 2009 +0100
@@ -155,6 +155,9 @@
declare [[map * = (prod_fun, prod_rel)]]
declare [[map "fun" = (fun_map, FUN_REL)]]
+lemmas [quotient_thm] =
+ FUN_QUOTIENT IDENTITY_QUOTIENT LIST_QUOTIENT
+
ML {* maps_lookup @{theory} "List.list" *}
ML {* maps_lookup @{theory} "*" *}
ML {* maps_lookup @{theory} "fun" *}
@@ -730,12 +733,9 @@
*}
ML {*
-fun quotient_tac ctxt quot_thms =
+fun quotient_tac ctxt =
REPEAT_ALL_NEW (FIRST'
- [rtac @{thm FUN_QUOTIENT},
- resolve_tac quot_thms,
- rtac @{thm IDENTITY_QUOTIENT},
- rtac @{thm LIST_QUOTIENT},
+ [resolve_tac (quotient_rules_get ctxt),
(* For functional identity quotients, (op = ---> op =) *)
(* TODO: think about the other way around, if we need to shorten the relation *)
CHANGED o (simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms id_simps}))])
@@ -901,7 +901,7 @@
ML {*
-fun inj_repabs_tac ctxt quot_thms rel_refl trans2 =
+fun inj_repabs_tac ctxt rel_refl trans2 =
(FIRST' [
(* "cong" rule of the of the relation / transitivity*)
(* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *)
@@ -933,11 +933,11 @@
(* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
(* observe ---> *)
NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt
- THEN' (RANGE [SOLVES' (quotient_tac ctxt quot_thms)]))),
+ THEN' (RANGE [SOLVES' (quotient_tac ctxt)]))),
(* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP provided type of t needs lifting *)
NDT ctxt "A" (APPLY_RSP_TAC ctxt THEN'
- (RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms),
+ (RANGE [SOLVES' (quotient_tac ctxt), SOLVES' (quotient_tac ctxt),
quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
(* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *)
@@ -961,8 +961,8 @@
*}
ML {*
-fun all_inj_repabs_tac ctxt quot_thms rel_refl trans2 =
- REPEAT_ALL_NEW (inj_repabs_tac ctxt quot_thms rel_refl trans2)
+fun all_inj_repabs_tac ctxt rel_refl trans2 =
+ REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2)
*}
section {* Cleaning of the theorem *}
@@ -970,8 +970,8 @@
(* TODO: This is slow *)
ML {*
-fun allex_prs_tac ctxt quot =
- (EqSubst.eqsubst_tac ctxt [0] @{thms all_prs ex_prs}) THEN' (quotient_tac ctxt quot)
+fun allex_prs_tac ctxt =
+ (EqSubst.eqsubst_tac ctxt [0] @{thms all_prs ex_prs}) THEN' (quotient_tac ctxt)
*}
ML {*
@@ -991,11 +991,11 @@
(* It proves the QUOTIENT assumptions by calling quotient_tac *)
ML {*
-fun solve_quotient_assum i quot_thms ctxt thm =
+fun solve_quotient_assum i ctxt thm =
let
val tac =
(compose_tac (false, thm, i)) THEN_ALL_NEW
- (quotient_tac ctxt quot_thms);
+ (quotient_tac ctxt);
val gc = Drule.strip_imp_concl (cprop_of thm);
in
Goal.prove_internal [] gc (fn _ => tac 1)
@@ -1004,7 +1004,7 @@
*}
ML {*
-fun lambda_allex_prs_simple_conv quot_thms ctxt ctrm =
+fun lambda_allex_prs_simple_conv ctxt ctrm =
case (term_of ctrm) of
((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>
let
@@ -1015,7 +1015,7 @@
val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_d];
val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS};
- val te = @{thm eq_reflection} OF [solve_quotient_assum 2 quot_thms ctxt lpi]
+ val te = @{thm eq_reflection} OF [solve_quotient_assum 2 ctxt lpi]
val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
val tl = Thm.lhs_of ts;
val (insp, inst) = make_inst (term_of tl) (term_of ctrm);
@@ -1032,7 +1032,7 @@
val tyinst = [SOME cty_a, SOME cty_b];
val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)];
val thm = Drule.instantiate' tyinst tinst @{thm all_prs};
- val ti = @{thm eq_reflection} OF [solve_quotient_assum 1 quot_thms ctxt thm];
+ val ti = @{thm eq_reflection} OF [solve_quotient_assum 1 ctxt thm];
in
Conv.rewr_conv ti ctrm
end
@@ -1045,7 +1045,7 @@
val tyinst = [SOME cty_a, SOME cty_b];
val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)];
val thm = Drule.instantiate' tyinst tinst @{thm ex_prs};
- val ti = @{thm eq_reflection} OF [solve_quotient_assum 1 quot_thms ctxt thm];
+ val ti = @{thm eq_reflection} OF [solve_quotient_assum 1 ctxt thm];
in
Conv.rewr_conv ti ctrm
end
@@ -1055,12 +1055,12 @@
(* quot stands for the QUOTIENT theorems: *)
(* could be potentially all of them *)
ML {*
-fun lambda_allex_prs_conv quot =
- More_Conv.top_conv (lambda_allex_prs_simple_conv quot)
+val lambda_allex_prs_conv =
+ More_Conv.top_conv lambda_allex_prs_simple_conv
*}
ML {*
-fun lambda_allex_prs_tac quot ctxt = CONVERSION (lambda_allex_prs_conv quot ctxt)
+fun lambda_allex_prs_tac ctxt = CONVERSION (lambda_allex_prs_conv ctxt)
*}
(*
@@ -1090,13 +1090,14 @@
*)
ML {*
-fun clean_tac lthy quot =
+fun clean_tac lthy =
let
val thy = ProofContext.theory_of lthy;
+ val quotients = quotient_rules_get lthy
val defs = map (Thm.varifyT o #def) (qconsts_dest thy);
- val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot
+ val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quotients
val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep;
- val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot
+ val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quotients
val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same
val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps
(@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs)
@@ -1104,7 +1105,7 @@
EVERY' [
(* (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) ----> f *)
(* \<forall>x\<in>Respects R. (abs ---> id) f ----> \<forall>x. f *)
- NDT lthy "a" (TRY o lambda_allex_prs_tac quot lthy),
+ NDT lthy "a" (TRY o lambda_allex_prs_tac lthy),
(* NewConst ----> (rep ---> abs) oldConst *)
(* Abs (Rep x) ----> x *)
@@ -1217,7 +1218,7 @@
ML {*
(* FIXME/TODO should only get as arguments the rthm like procedure_tac *)
-fun lift_tac lthy rthm rel_eqv quot =
+fun lift_tac lthy rthm rel_eqv =
ObjectLogic.full_atomize_tac
THEN' gen_frees_tac lthy
THEN' Subgoal.FOCUS (fn {context, concl, ...} =>
@@ -1232,8 +1233,8 @@
[rtac rule,
RANGE [rtac rthm',
regularize_tac lthy rel_eqv,
- rtac thm THEN' all_inj_repabs_tac lthy quot rel_refl trans2,
- clean_tac lthy quot]]
+ rtac thm THEN' all_inj_repabs_tac lthy rel_refl trans2,
+ clean_tac lthy]]
end) lthy
*}
--- a/quotient_info.ML Thu Dec 03 14:02:05 2009 +0100
+++ b/quotient_info.ML Thu Dec 03 15:03:31 2009 +0100
@@ -164,14 +164,14 @@
(* respectfulness lemmas *)
structure RspRules = Named_Thms
- (val name = "quot_rsp"
+ (val name = "quotient_rsp"
val description = "Respectfulness theorems.")
val rsp_rules_get = RspRules.get
(* quotient lemmas *)
structure QuotientRules = Named_Thms
- (val name = "quotient"
+ (val name = "quotient_thm"
val description = "Quotient theorems.")
val quotient_rules_get = QuotientRules.get