--- a/src/HOL/Tools/Quotient/quotient_def.ML Fri Jan 07 20:42:25 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Fri Jan 07 21:26:49 2011 +0100
@@ -19,9 +19,6 @@
structure Quotient_Def: QUOTIENT_DEF =
struct
-open Quotient_Info;
-open Quotient_Term;
-
(** Interface and Syntax Setup **)
(* The ML-interface for a quotient definition takes
@@ -60,7 +57,7 @@
val _ = sanity_test optbind lhs_str
val qconst_bname = Binding.name lhs_str
- val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
+ val absrep_trm = Quotient_Term.absrep_fun Quotient_Term.AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
val (_, prop') = Local_Defs.cert_def lthy prop
val (_, newrhs) = Local_Defs.abs_def prop'
@@ -70,10 +67,11 @@
(* data storage *)
val qconst_data = {qconst = trm, rconst = rhs, def = thm}
- fun qcinfo phi = transform_qconsts phi qconst_data
+ fun qcinfo phi = Quotient_Info.transform_qconsts phi qconst_data
fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)
- val lthy'' = Local_Theory.declaration true
- (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy'
+ val lthy'' =
+ Local_Theory.declaration true
+ (fn phi => Quotient_Info.qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy'
in
(qconst_data, lthy'')
end
@@ -92,7 +90,7 @@
fun lift_raw_const qtys (qconst_name, rconst, mx) ctxt =
let
val rty = fastype_of rconst
- val qty = derive_qtyp ctxt qtys rty
+ val qty = Quotient_Term.derive_qtyp ctxt qtys rty
val lhs = Free (qconst_name, qty)
in
quotient_def ((NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt
--- a/src/HOL/Tools/Quotient/quotient_info.ML Fri Jan 07 20:42:25 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Fri Jan 07 21:26:49 2011 +0100
@@ -4,6 +4,8 @@
Data slots for the quotient package.
*)
+(* FIXME odd names/signatures of data access operations *)
+
signature QUOTIENT_INFO =
sig
exception NotFound (* FIXME complicates signatures unnecessarily *)
@@ -44,7 +46,6 @@
val quotient_rules_add: attribute
end;
-
structure Quotient_Info: QUOTIENT_INFO =
struct
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Fri Jan 07 20:42:25 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Fri Jan 07 21:26:49 2011 +0100
@@ -25,10 +25,6 @@
structure Quotient_Tacs: QUOTIENT_TACS =
struct
-open Quotient_Info;
-open Quotient_Term;
-
-
(** various helper fuctions **)
(* Since HOL_basic_ss is too "big" for us, we *)
@@ -56,7 +52,7 @@
(** solvers for equivp and quotient assumptions **)
fun equiv_tac ctxt =
- REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt))
+ REPEAT_ALL_NEW (resolve_tac (Quotient_Info.equiv_rules_get ctxt))
fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
@@ -64,7 +60,7 @@
fun quotient_tac ctxt =
(REPEAT_ALL_NEW (FIRST'
[rtac @{thm identity_quotient},
- resolve_tac (quotient_rules_get ctxt)]))
+ resolve_tac (Quotient_Info.quotient_rules_get ctxt)]))
fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
val quotient_solver =
@@ -152,11 +148,11 @@
fun reflp_get ctxt =
map_filter (fn th => if prems_of th = [] then SOME (OF1 @{thm equivp_reflp} th) else NONE
- handle THM _ => NONE) (equiv_rules_get ctxt)
+ handle THM _ => NONE) (Quotient_Info.equiv_rules_get ctxt)
val eq_imp_rel = @{lemma "equivp R ==> a = b --> R a b" by (simp add: equivp_reflp)}
-fun eq_imp_rel_get ctxt = map (OF1 eq_imp_rel) (equiv_rules_get ctxt)
+fun eq_imp_rel_get ctxt = map (OF1 eq_imp_rel) (Quotient_Info.equiv_rules_get ctxt)
fun regularize_tac ctxt =
let
@@ -379,7 +375,7 @@
(* respectfulness of constants; in particular of a simple relation *)
| _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *)
- => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
+ => resolve_tac (Quotient_Info.rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
(* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
(* observe map_fun *)
@@ -527,18 +523,19 @@
*)
fun clean_tac lthy =
let
- val defs = map (Thm.symmetric o #def) (qconsts_dest lthy)
- val prs = prs_rules_get lthy
- val ids = id_simps_get lthy
+ val defs = map (Thm.symmetric o #def) (Quotient_Info.qconsts_dest lthy)
+ val prs = Quotient_Info.prs_rules_get lthy
+ val ids = Quotient_Info.id_simps_get lthy
val thms =
@{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs
val ss = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
in
- EVERY' [map_fun_tac lthy,
- lambda_prs_tac lthy,
- simp_tac ss,
- TRY o rtac refl]
+ EVERY' [
+ map_fun_tac lthy,
+ lambda_prs_tac lthy,
+ simp_tac ss,
+ TRY o rtac refl]
end
@@ -606,10 +603,10 @@
val thy = ProofContext.theory_of ctxt
val rtrm' = HOLogic.dest_Trueprop rtrm
val qtrm' = HOLogic.dest_Trueprop qtrm
- val reg_goal = regularize_trm_chk ctxt (rtrm', qtrm')
- handle LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
- val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm')
- handle LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
+ val reg_goal = Quotient_Term.regularize_trm_chk ctxt (rtrm', qtrm')
+ handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
+ val inj_goal = Quotient_Term.inj_repabs_trm_chk ctxt (reg_goal, qtrm')
+ handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
in
Drule.instantiate' []
[SOME (cterm_of thy rtrm'),
@@ -638,7 +635,7 @@
THEN' SUBGOAL (fn (goal, i) =>
let
val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
- val rtrm = derive_rtrm ctxt qtys goal
+ val rtrm = Quotient_Term.derive_rtrm ctxt qtys goal
val rule = procedure_inst ctxt rtrm goal
in
rtac rule i
@@ -703,7 +700,7 @@
fun lifted ctxt qtys simps rthm =
let
val ((_, [rthm']), ctxt') = Variable.import true [rthm] ctxt
- val goal = derive_qtrm ctxt' qtys (prop_of rthm')
+ val goal = Quotient_Term.derive_qtrm ctxt' qtys (prop_of rthm')
in
Goal.prove ctxt' [] [] goal
(K (HEADGOAL (lift_single_tac ctxt' simps rthm')))
--- a/src/HOL/Tools/Quotient/quotient_term.ML Fri Jan 07 20:42:25 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Fri Jan 07 21:26:49 2011 +0100
@@ -35,8 +35,6 @@
structure Quotient_Term: QUOTIENT_TERM =
struct
-open Quotient_Info;
-
exception LIFT_MATCH of string
@@ -67,7 +65,7 @@
fun get_mapfun ctxt s =
let
val thy = ProofContext.theory_of ctxt
- val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound =>
+ val mapfun = #mapfun (Quotient_Info.maps_lookup thy s) handle Quotient_Info.NotFound =>
raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
in
Const (mapfun, dummyT)
@@ -104,7 +102,7 @@
fun get_rty_qty ctxt s =
let
val thy = ProofContext.theory_of ctxt
- val qdata = quotdata_lookup thy s handle Quotient_Info.NotFound =>
+ val qdata = Quotient_Info.quotdata_lookup thy s handle Quotient_Info.NotFound =>
raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
in
(#rtyp qdata, #qtyp qdata)
@@ -276,7 +274,7 @@
fun get_relmap ctxt s =
let
val thy = ProofContext.theory_of ctxt
- val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound =>
+ val relmap = #relmap (Quotient_Info.maps_lookup thy s) handle Quotient_Info.NotFound =>
raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
in
Const (relmap, dummyT)
@@ -300,7 +298,7 @@
let
val thy = ProofContext.theory_of ctxt
in
- #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound =>
+ #equiv_rel (Quotient_Info.quotdata_lookup thy s) handle Quotient_Info.NotFound =>
raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
end
@@ -437,7 +435,7 @@
if length rtys <> length qtys then false
else forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys)
else
- (case quotdata_lookup_raw thy qs of
+ (case Quotient_Info.quotdata_lookup_raw thy qs of
SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
| NONE => false)
| _ => false)
@@ -563,7 +561,7 @@
if same_const rtrm qtrm then rtrm
else
let
- val rtrm' = #rconst (qconsts_lookup thy qtrm)
+ val rtrm' = #rconst (Quotient_Info.qconsts_lookup thy qtrm)
handle Quotient_Info.NotFound =>
term_mismatch "regularize (constant not found)" ctxt rtrm qtrm
in
@@ -753,7 +751,7 @@
let
val thy = ProofContext.theory_of ctxt
in
- quotdata_dest ctxt
+ Quotient_Info.quotdata_dest ctxt
|> map (fn x => (#rtyp x, #qtyp x))
|> filter (fn (_, qty) => member (Sign.typ_instance thy o swap) qtys qty)
|> map (if direction then swap else I)
@@ -765,12 +763,12 @@
fun proper (t1, t2) = subst_typ' (fastype_of t1) = fastype_of t2
val const_substs =
- qconsts_dest ctxt
+ Quotient_Info.qconsts_dest ctxt
|> map (fn x => (#rconst x, #qconst x))
|> map (if direction then swap else I)
val rel_substs =
- quotdata_dest ctxt
+ Quotient_Info.quotdata_dest ctxt
|> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x)))
|> map (if direction then swap else I)
in
--- a/src/HOL/Tools/Quotient/quotient_typ.ML Fri Jan 07 20:42:25 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML Fri Jan 07 21:26:49 2011 +0100
@@ -20,9 +20,8 @@
structure Quotient_Type: QUOTIENT_TYPE =
struct
-open Quotient_Info;
+(* wrappers for define, note, Attrib.internal and theorem_i *) (* FIXME !? *)
-(* wrappers for define, note, Attrib.internal and theorem_i *)
fun define (name, mx, rhs) lthy =
let
val ((rhs, (_ , thm)), lthy') =
@@ -160,12 +159,15 @@
(* storing the quotdata *)
val quotdata = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm}
- fun qinfo phi = transform_quotdata phi quotdata
+ fun qinfo phi = Quotient_Info.transform_quotdata phi quotdata
val lthy4 = lthy3
- |> Local_Theory.declaration true (fn phi => quotdata_update_gen qty_full_name (qinfo phi))
- |> note (equiv_thm_name, equiv_thm, if partial then [] else [intern_attr equiv_rules_add])
- |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add])
+ |> Local_Theory.declaration true
+ (fn phi => Quotient_Info.quotdata_update_gen qty_full_name (qinfo phi))
+ |> note
+ (equiv_thm_name, equiv_thm,
+ if partial then [] else [intern_attr Quotient_Info.equiv_rules_add])
+ |> note (quotient_thm_name, quotient_thm, [intern_attr Quotient_Info.quotient_rules_add])
in
(quotdata, lthy4)
end
@@ -218,7 +220,7 @@
fun map_check_aux rty warns =
case rty of
Type (_, []) => warns
- | Type (s, _) => if maps_defined thy s then warns else s::warns
+ | Type (s, _) => if Quotient_Info.maps_defined thy s then warns else s::warns
| _ => warns
val warns = map_check_aux rty []