--- a/QuotMain.thy Fri Dec 04 09:08:51 2009 +0100
+++ b/QuotMain.thy Fri Dec 04 09:25:27 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,15 +733,10 @@
*}
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},
- (* 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}))])
+ [rtac @{thm IDENTITY_QUOTIENT},
+ resolve_tac (quotient_rules_get ctxt)])
*}
lemma FUN_REL_I:
@@ -901,7 +899,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 +931,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 *)
@@ -953,16 +951,17 @@
NDT ctxt "D" (resolve_tac rel_refl),
(* resolving with R x y assumptions *)
- NDT ctxt "E" (atac),
+ NDT ctxt "E" (atac)
(* (op =) ===> (op =) \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *)
(* global simplification *)
- NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))])
+ (*NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms FUN_REL_EQ LIST_REL_EQ})))*)
+ ])
*}
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)
*}
(* A faster version *)
@@ -1024,10 +1023,12 @@
(* 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 {*
fun make_inst lhs t =
@@ -1046,11 +1047,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)
@@ -1059,7 +1060,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
@@ -1070,7 +1071,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);
@@ -1087,7 +1088,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
@@ -1100,7 +1101,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
@@ -1110,12 +1111,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)
*}
(*
@@ -1145,13 +1146,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)
@@ -1159,7 +1161,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 *)
@@ -1272,7 +1274,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, ...} =>
@@ -1287,8 +1289,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
*}