--- a/src/HOL/Tools/Lifting/lifting_def.ML Mon May 21 11:31:52 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Mon May 21 16:36:48 2012 +0200
@@ -118,7 +118,7 @@
*)
fun can_generate_code_cert quot_thm =
- case Lifting_Term.quot_thm_rel quot_thm of
+ case quot_thm_rel quot_thm of
Const (@{const_name HOL.eq}, _) => true
| Const (@{const_name invariant}, _) $ _ => true
| _ => false
@@ -136,7 +136,7 @@
| _ => raise CODE_CERT_GEN "relation is neither equality nor invariant"
val unfolded_def = Conv.fconv_rule (Conv.arg_conv unfold_fun_maps_beta) def_thm
val unabs_def = unabs_all_def ctxt unfolded_def
- val rep = (cterm_of thy o Lifting_Term.quot_thm_rep) quot_thm
+ val rep = (cterm_of thy o quot_thm_rep) quot_thm
val rep_refl = Thm.reflexive rep RS @{thm meta_eq_to_obj_eq}
val repped_eq = [rep_refl, unabs_def RS @{thm meta_eq_to_obj_eq}] MRSL @{thm cong}
val code_cert = [repped_eq, abs_rep_eq] MRSL @{thm trans}
@@ -195,8 +195,8 @@
val abs_eq_with_assms =
let
- val (rty, qty) = Lifting_Term.quot_thm_rty_qty quot_thm
- val rel = Lifting_Term.quot_thm_rel quot_thm
+ val (rty, qty) = quot_thm_rty_qty quot_thm
+ val rel = quot_thm_rel quot_thm
val ty_args = get_binder_types_by_rel rel (rty, qty)
val body_type = get_body_type_by_rel rel (rty, qty)
val quot_ret_thm = Lifting_Term.prove_quot_thm ctxt body_type
@@ -248,7 +248,7 @@
fun has_constr ctxt quot_thm =
let
val thy = Proof_Context.theory_of ctxt
- val abs_fun = Lifting_Term.quot_thm_abs quot_thm
+ val abs_fun = quot_thm_abs quot_thm
in
if is_Const abs_fun then
Code.is_constr thy ((fst o dest_Const) abs_fun)
@@ -259,7 +259,7 @@
fun has_abstr ctxt quot_thm =
let
val thy = Proof_Context.theory_of ctxt
- val abs_fun = Lifting_Term.quot_thm_abs quot_thm
+ val abs_fun = quot_thm_abs quot_thm
in
if is_Const abs_fun then
Code.is_abstr thy ((fst o dest_Const) abs_fun)
@@ -304,7 +304,7 @@
let
val rty = fastype_of rhs
val quot_thm = Lifting_Term.prove_quot_thm lthy (rty, qty)
- val absrep_trm = Lifting_Term.quot_thm_abs quot_thm
+ val absrep_trm = quot_thm_abs quot_thm
val rty_forced = (domain_type o fastype_of) absrep_trm
val forced_rhs = force_rty_type lthy rty_forced rhs
val lhs = Free (Binding.print (#1 var), qty)
--- a/src/HOL/Tools/Lifting/lifting_info.ML Mon May 21 11:31:52 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML Mon May 21 16:36:48 2012 +0200
@@ -99,7 +99,7 @@
Quotmaps.map (Symtab.update (relatorT_name, minfo)) ctxt
end
-val quotmaps_attribute_setup =
+val quot_map_attribute_setup =
Attrib.setup @{binding quot_map} (Scan.succeed (Thm.declaration_attribute add_quot_map))
"declaration of the Quotient map theorem"
@@ -136,6 +136,22 @@
fun update_quotients str qinfo = Quotients.map (Symtab.update (str, qinfo))
+fun delete_quotients quot_thm ctxt =
+ let
+ val (_, qtyp) = quot_thm_rty_qty quot_thm
+ val qty_full_name = (fst o dest_Type) qtyp
+ val symtab = Quotients.get ctxt
+ val maybe_stored_quot_thm = Symtab.lookup symtab qty_full_name
+ in
+ case maybe_stored_quot_thm of
+ SOME {quot_thm = stored_quot_thm} =>
+ if Thm.eq_thm_prop (stored_quot_thm, quot_thm) then
+ Quotients.map (Symtab.delete qty_full_name) ctxt
+ else
+ ctxt
+ | NONE => ctxt
+ end
+
fun dest_quotients ctxt = (* FIXME slightly expensive way to retrieve data *)
map snd (Symtab.dest (Quotients.get (Context.Proof ctxt)))
@@ -153,6 +169,10 @@
|> Pretty.writeln
end
+val quot_del_attribute_setup =
+ Attrib.setup @{binding quot_del} (Scan.succeed (Thm.declaration_attribute delete_quotients))
+ "deletes the Quotient theorem"
+
structure Invariant_Commute = Named_Thms
(
val name = @{binding invariant_commute}
@@ -174,7 +194,8 @@
(* theory setup *)
val setup =
- quotmaps_attribute_setup
+ quot_map_attribute_setup
+ #> quot_del_attribute_setup
#> Invariant_Commute.setup
#> Reflp_Preserve.setup
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Mon May 21 11:31:52 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Mon May 21 16:36:48 2012 +0200
@@ -38,7 +38,7 @@
fun define_code_constr gen_code quot_thm lthy =
let
- val abs = Lifting_Term.quot_thm_abs quot_thm
+ val abs = quot_thm_abs quot_thm
val abs_background = Morphism.term (Local_Theory.target_morphism lthy) abs
in
if gen_code andalso is_Const abs_background then
@@ -71,7 +71,7 @@
fun quot_thm_sanity_check ctxt quot_thm =
let
val ((_, [quot_thm_fixed]), ctxt') = Variable.importT [quot_thm] ctxt
- val (rty, qty) = Lifting_Term.quot_thm_rty_qty quot_thm_fixed
+ val (rty, qty) = quot_thm_rty_qty quot_thm_fixed
val rty_tfreesT = Term.add_tfree_namesT rty []
val qty_tfreesT = Term.add_tfree_namesT qty []
val extra_rty_tfrees =
@@ -97,7 +97,7 @@
fun setup_lifting_infr gen_code quot_thm maybe_reflp_thm lthy =
let
val _ = quot_thm_sanity_check lthy quot_thm
- val (_, qtyp) = Lifting_Term.quot_thm_rty_qty quot_thm
+ val (_, qtyp) = quot_thm_rty_qty quot_thm
val qty_full_name = (fst o dest_Type) qtyp
val quotients = { quot_thm = quot_thm }
fun quot_info phi = Lifting_Info.transform_quotients phi quotients
@@ -127,7 +127,7 @@
fun setup_by_quotient gen_code quot_thm maybe_reflp_thm lthy =
let
val transfer_attr = Attrib.internal (K Transfer.transfer_add)
- val (_, qty) = Lifting_Term.quot_thm_rty_qty quot_thm
+ val (_, qty) = quot_thm_rty_qty quot_thm
val induct_attr = Attrib.internal (K (Induct.induct_type (fst (dest_Type qty))))
val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty
fun qualify suffix = Binding.qualified true suffix qty_name
@@ -183,7 +183,7 @@
| _ =>
[typedef_thm, T_def] MRSL @{thm typedef_to_Quotient}
- val (_, qty) = Lifting_Term.quot_thm_rty_qty quot_thm
+ val (_, qty) = quot_thm_rty_qty quot_thm
val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty
fun qualify suffix = Binding.qualified true suffix qty_name
val simplify = Raw_Simplifier.rewrite_rule [mk_meta_eq @{thm mem_Collect_eq}]
--- a/src/HOL/Tools/Lifting/lifting_term.ML Mon May 21 11:31:52 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_term.ML Mon May 21 16:36:48 2012 +0200
@@ -14,11 +14,6 @@
val abs_fun: Proof.context -> typ * typ -> term
val equiv_relation: Proof.context -> typ * typ -> term
-
- val quot_thm_rel: thm -> term
- val quot_thm_abs: thm -> term
- val quot_thm_rep: thm -> term
- val quot_thm_rty_qty: thm -> typ * typ
end
structure Lifting_Term: LIFTING_TERM =
@@ -79,31 +74,6 @@
fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient})
-(*
- quot_thm_rel, quot_thm_abs, quot_thm_rep and quot_thm_rty_qty - simple functions
- for destructing quotient theorems (Quotient R Abs Rep T).
-*)
-
-fun quot_thm_rel quot_thm =
- case (dest_Quotient o HOLogic.dest_Trueprop o prop_of) quot_thm of
- (rel, _, _, _) => rel
-
-fun quot_thm_abs quot_thm =
- case (dest_Quotient o HOLogic.dest_Trueprop o prop_of) quot_thm of
- (_, abs, _, _) => abs
-
-fun quot_thm_rep quot_thm =
- case (dest_Quotient o HOLogic.dest_Trueprop o prop_of) quot_thm of
- (_, _, rep, _) => rep
-
-fun quot_thm_rty_qty quot_thm =
- let
- val abs = quot_thm_abs quot_thm
- val abs_type = fastype_of abs
- in
- (domain_type abs_type, range_type abs_type)
- end
-
fun check_raw_types (provided_rty_name, rty_of_qty_name) qty_name =
if provided_rty_name <> rty_of_qty_name then
raise QUOT_THM_INTERNAL (Pretty.block
--- a/src/HOL/Tools/Lifting/lifting_util.ML Mon May 21 11:31:52 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_util.ML Mon May 21 16:36:48 2012 +0200
@@ -9,6 +9,11 @@
val MRSL: thm list * thm -> thm
val Trueprop_conv: conv -> conv
val dest_Quotient: term -> term * term * term * term
+
+ val quot_thm_rel: thm -> term
+ val quot_thm_abs: thm -> term
+ val quot_thm_rep: thm -> term
+ val quot_thm_rty_qty: thm -> typ * typ
end;
@@ -28,4 +33,29 @@
= (rel, abs, rep, cr)
| dest_Quotient t = raise TERM ("dest_Quotient", [t])
+(*
+ quot_thm_rel, quot_thm_abs, quot_thm_rep and quot_thm_rty_qty - simple functions
+ for destructing quotient theorems (Quotient R Abs Rep T).
+*)
+
+fun quot_thm_rel quot_thm =
+ case (dest_Quotient o HOLogic.dest_Trueprop o prop_of) quot_thm of
+ (rel, _, _, _) => rel
+
+fun quot_thm_abs quot_thm =
+ case (dest_Quotient o HOLogic.dest_Trueprop o prop_of) quot_thm of
+ (_, abs, _, _) => abs
+
+fun quot_thm_rep quot_thm =
+ case (dest_Quotient o HOLogic.dest_Trueprop o prop_of) quot_thm of
+ (_, _, rep, _) => rep
+
+fun quot_thm_rty_qty quot_thm =
+ let
+ val abs = quot_thm_abs quot_thm
+ val abs_type = fastype_of abs
+ in
+ (domain_type abs_type, range_type abs_type)
+ end
+
end;