--- a/src/HOL/Tools/Lifting/lifting_setup.ML Mon Sep 16 11:54:57 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Mon Sep 16 15:30:17 2013 +0200
@@ -11,7 +11,9 @@
val setup_by_quotient: bool -> thm -> thm option -> thm option -> local_theory -> local_theory
val setup_by_typedef_thm: bool -> thm -> local_theory -> local_theory
-end;
+
+ val lifting_restore: Lifting_Info.quotient -> Context.generic -> Context.generic
+end
structure Lifting_Setup: LIFTING_SETUP =
struct
@@ -164,8 +166,24 @@
else
lthy
+local
+ exception QUOT_ERROR of Pretty.T list
+in
fun quot_thm_sanity_check ctxt quot_thm =
let
+ val _ =
+ if (nprems_of quot_thm > 0) then
+ raise QUOT_ERROR [Pretty.block
+ [Pretty.str "The Quotient theorem has extra assumptions:",
+ Pretty.brk 1,
+ Display.pretty_thm ctxt quot_thm]]
+ else ()
+ val _ = quot_thm |> concl_of |> HOLogic.dest_Trueprop |> dest_Quotient
+ handle TERM _ => raise QUOT_ERROR
+ [Pretty.block
+ [Pretty.str "The Quotient theorem is not of the right form:",
+ Pretty.brk 1,
+ Display.pretty_thm ctxt quot_thm]]
val ((_, [quot_thm_fixed]), ctxt') = Variable.importT [quot_thm] ctxt
val (rty, qty) = quot_thm_rty_qty quot_thm_fixed
val rty_tfreesT = Term.add_tfree_namesT rty []
@@ -186,8 +204,31 @@
Pretty.str "is not a type constructor."]]
val errs = extra_rty_tfrees @ not_type_constr
in
- if null errs then () else error (cat_lines (["Sanity check of the quotient theorem failed:",""]
- @ (map Pretty.string_of errs)))
+ if null errs then () else raise QUOT_ERROR errs
+ end
+ handle QUOT_ERROR errs => error (cat_lines (["Sanity check of the quotient theorem failed:"]
+ @ (map (Pretty.string_of o Pretty.item o single) errs)))
+end
+
+fun lifting_bundle qty_full_name qinfo lthy =
+ let
+ fun qualify suffix defname = Binding.qualified true suffix defname
+ val binding = qty_full_name |> Long_Name.base_name |> Binding.name |> qualify "lifting"
+ val morphed_binding = Morphism.binding (Local_Theory.target_morphism lthy) binding
+ val bundle_name = Name_Space.full_name (Name_Space.naming_of
+ (Context.Theory (Proof_Context.theory_of lthy))) morphed_binding
+ fun phi_qinfo phi = Lifting_Info.transform_quotient phi qinfo
+
+ val thy = Proof_Context.theory_of lthy
+ val dummy_thm = Thm.transfer thy Drule.dummy_thm
+ val pointer = Outer_Syntax.scan Position.none bundle_name
+ val restore_lifting_att =
+ ([dummy_thm], [Args.src (("Lifting.lifting_restore_internal", pointer), Position.none)])
+ in
+ lthy
+ |> Local_Theory.declaration {syntax = false, pervasive = true}
+ (fn phi => Lifting_Info.init_restore_data bundle_name (phi_qinfo phi))
+ |> Bundle.bundle ((binding, [restore_lifting_att])) []
end
fun setup_lifting_infr gen_code quot_thm opt_reflp_thm lthy =
@@ -221,23 +262,24 @@
lthy
|> Local_Theory.declaration {syntax = false, pervasive = true}
(fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi))
+ |> lifting_bundle qty_full_name quotients
end
local
fun importT_inst_exclude exclude ts ctxt =
let
- val tvars = rev (subtract op= exclude (fold Term.add_tvars ts []));
- val (tfrees, ctxt') = Variable.invent_types (map #2 tvars) ctxt;
+ val tvars = rev (subtract op= exclude (fold Term.add_tvars ts []))
+ val (tfrees, ctxt') = Variable.invent_types (map #2 tvars) ctxt
in (tvars ~~ map TFree tfrees, ctxt') end
fun import_inst_exclude exclude ts ctxt =
let
val excludeT = fold (Term.add_tvarsT o snd) exclude []
- val (instT, ctxt') = importT_inst_exclude excludeT ts ctxt;
+ val (instT, ctxt') = importT_inst_exclude excludeT ts ctxt
val vars = map (apsnd (Term_Subst.instantiateT instT))
- (rev (subtract op= exclude (fold Term.add_vars ts [])));
- val (xs, ctxt'') = Variable.variant_fixes (map (#1 o #1) vars) ctxt';
- val inst = vars ~~ map Free (xs ~~ map #2 vars);
+ (rev (subtract op= exclude (fold Term.add_vars ts [])))
+ val (xs, ctxt'') = Variable.variant_fixes (map (#1 o #1) vars) ctxt'
+ val inst = vars ~~ map Free (xs ~~ map #2 vars)
in ((instT, inst), ctxt'') end
fun import_terms_exclude exclude ts ctxt =
@@ -328,16 +370,16 @@
val orig_lthy = lthy
(* it doesn't raise an exception because it would have already raised it in define_pcrel *)
val (quot_thm, _, lthy) = Lifting_Term.prove_param_quot_thm lthy rty
- val parametrized_relator = singleton (Variable.export_terms lthy orig_lthy) (quot_thm_crel quot_thm);
+ val parametrized_relator = singleton (Variable.export_terms lthy orig_lthy) (quot_thm_crel quot_thm)
val lthy = orig_lthy
val id_transfer =
@{thm id_transfer}
|> Thm.incr_indexes (Term.maxidx_of_term parametrized_relator + 1)
|> Conv.fconv_rule(HOLogic.Trueprop_conv (Conv.arg_conv id_unfold then_conv Conv.arg1_conv id_unfold))
- val var = Var (hd (Term.add_vars (prop_of id_transfer) []));
- val thy = Proof_Context.theory_of lthy;
+ val var = Var (hd (Term.add_vars (prop_of id_transfer) []))
+ val thy = Proof_Context.theory_of lthy
val inst = [(cterm_of thy var, cterm_of thy parametrized_relator)]
- val id_par_thm = Drule.cterm_instantiate inst id_transfer;
+ val id_par_thm = Drule.cterm_instantiate inst id_transfer
in
Lifting_Def.generate_parametric_transfer_rule lthy id_transfer_rule id_par_thm
end
@@ -362,7 +404,7 @@
val ct = thm |> cprop_of |> Drule.strip_imp_concl |> Thm.dest_arg |> Thm.dest_arg1 |> Thm.dest_arg
val pcrel_def = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) pcrel_def
val thm = Thm.instantiate (Thm.match (ct, Thm.rhs_of pcrel_def)) thm
- handle Pattern.MATCH => raise CTERM ("fold_Domainp_pcrel", [ct, Thm.rhs_of pcrel_def]);
+ handle Pattern.MATCH => raise CTERM ("fold_Domainp_pcrel", [ct, Thm.rhs_of pcrel_def])
in
rewrite_first_Domainp_arg (Thm.symmetric pcrel_def) thm
end
@@ -734,4 +776,243 @@
-- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse_Spec.xthm) >>
(fn (((gen_code, xthm), opt_reflp_xthm), opt_par_xthm) =>
setup_lifting_cmd gen_code xthm opt_reflp_xthm opt_par_xthm))
-end;
+
+(* restoring lifting infrastructure *)
+
+local
+ exception PCR_ERROR of Pretty.T list
+in
+
+fun lifting_restore_sanity_check ctxt (qinfo:Lifting_Info.quotient) =
+ let
+ val quot_thm = (#quot_thm qinfo)
+ val _ = quot_thm_sanity_check ctxt quot_thm
+ val pcr_info_err =
+ (case #pcr_info qinfo of
+ SOME pcr =>
+ let
+ val pcrel_def = #pcrel_def pcr
+ val pcr_cr_eq = #pcr_cr_eq pcr
+ val (def_lhs, _) = Logic.dest_equals (prop_of pcrel_def)
+ handle TERM _ => raise PCR_ERROR [Pretty.block
+ [Pretty.str "The pcr definiton theorem is not a plain meta equation:",
+ Pretty.brk 1,
+ Display.pretty_thm ctxt pcrel_def]]
+ val pcr_const_def = head_of def_lhs
+ val (eq_lhs, eq_rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of pcr_cr_eq))
+ handle TERM _ => raise PCR_ERROR [Pretty.block
+ [Pretty.str "The pcr_cr equation theorem is not a plain equation:",
+ Pretty.brk 1,
+ Display.pretty_thm ctxt pcr_cr_eq]]
+ val (pcr_const_eq, eqs) = strip_comb eq_lhs
+ fun is_eq (Const ("HOL.eq", _)) = true
+ | is_eq _ = false
+ fun eq_Const (Const (name1, _)) (Const (name2, _)) = (name1 = name2)
+ | eq_Const _ _ = false
+ val all_eqs = if not (forall is_eq eqs) then
+ [Pretty.block
+ [Pretty.str "Arguments of the lhs of the pcr_cr equation theorem are not only equalities:",
+ Pretty.brk 1,
+ Display.pretty_thm ctxt pcr_cr_eq]]
+ else []
+ val pcr_consts_not_equal = if not (eq_Const pcr_const_def pcr_const_eq) then
+ [Pretty.block
+ [Pretty.str "Parametrized correspondence relation constants in pcr_def and pcr_cr_eq are not equal:",
+ Pretty.brk 1,
+ Syntax.pretty_term ctxt pcr_const_def,
+ Pretty.brk 1,
+ Pretty.str "vs.",
+ Pretty.brk 1,
+ Syntax.pretty_term ctxt pcr_const_eq]]
+ else []
+ val crel = quot_thm_crel quot_thm
+ val cr_consts_not_equal = if not (eq_Const crel eq_rhs) then
+ [Pretty.block
+ [Pretty.str "Correspondence relation constants in the Quotient theorem and pcr_cr_eq are not equal:",
+ Pretty.brk 1,
+ Syntax.pretty_term ctxt crel,
+ Pretty.brk 1,
+ Pretty.str "vs.",
+ Pretty.brk 1,
+ Syntax.pretty_term ctxt eq_rhs]]
+ else []
+ in
+ all_eqs @ pcr_consts_not_equal @ cr_consts_not_equal
+ end
+ | NONE => [])
+ val errs = pcr_info_err
+ in
+ if null errs then () else raise PCR_ERROR errs
+ end
+ handle PCR_ERROR errs => error (cat_lines (["Sanity check failed:"]
+ @ (map (Pretty.string_of o Pretty.item o single) errs)))
+end
+
+fun lifting_restore qinfo ctxt =
+ let
+ val _ = lifting_restore_sanity_check (Context.proof_of ctxt) qinfo
+ val (_, qty) = quot_thm_rty_qty (#quot_thm qinfo)
+ val qty_full_name = (fst o dest_Type) qty
+ val stored_qinfo = Lifting_Info.lookup_quotients (Context.proof_of ctxt) qty_full_name
+ in
+ if is_some (stored_qinfo) andalso not (Lifting_Info.quotient_eq (qinfo, (the stored_qinfo)))
+ then error (Pretty.string_of
+ (Pretty.block
+ [Pretty.str "Lifting is already setup for the type",
+ Pretty.brk 1,
+ Pretty.quote (Syntax.pretty_typ (Context.proof_of ctxt) qty)]))
+ else Lifting_Info.update_quotients qty_full_name qinfo ctxt
+ end
+
+val parse_opt_pcr =
+ Scan.optional (Attrib.thm -- Attrib.thm >>
+ (fn (pcrel_def, pcr_cr_eq) => SOME {pcrel_def = pcrel_def, pcr_cr_eq = pcr_cr_eq})) NONE
+
+val lifting_restore_attribute_setup =
+ Attrib.setup @{binding lifting_restore}
+ ((Attrib.thm -- parse_opt_pcr) >>
+ (fn (quot_thm, opt_pcr) =>
+ let val qinfo = { quot_thm = quot_thm, pcr_info = opt_pcr}
+ in Thm.declaration_attribute (K (lifting_restore qinfo)) end))
+ "restoring lifting infrastructure"
+
+val _ = Theory.setup lifting_restore_attribute_setup
+
+fun lifting_restore_internal bundle_name ctxt =
+ let
+ val restore_info = Lifting_Info.lookup_restore_data (Context.proof_of ctxt) bundle_name
+ in
+ case restore_info of
+ SOME restore_info =>
+ ctxt
+ |> lifting_restore (#quotient restore_info)
+ |> fold_rev Transfer.transfer_raw_add (Item_Net.content (#transfer_rules restore_info))
+ | NONE => ctxt
+ end
+
+val lifting_restore_internal_attribute_setup =
+ Attrib.setup @{binding lifting_restore_internal}
+ (Scan.lift Args.name >> (fn name => Thm.declaration_attribute (K (lifting_restore_internal name))))
+ "restoring lifting infrastructure; internal attribute; not meant to be used directly by regular users"
+
+val _ = Theory.setup lifting_restore_internal_attribute_setup
+
+(* lifting_forget *)
+
+val monotonicity_names = [@{const_name right_unique}, @{const_name left_unique}, @{const_name right_total},
+ @{const_name left_total}, @{const_name bi_unique}, @{const_name bi_total}]
+
+fun fold_transfer_rel f (Const (@{const_name "Transfer.Rel"}, _) $ rel $ _ $ _) = f rel
+ | fold_transfer_rel f (Const (@{const_name "HOL.eq"}, _) $
+ (Const (@{const_name Domainp}, _) $ rel) $ _) = f rel
+ | fold_transfer_rel f (Const (name, _) $ rel) =
+ if member op= monotonicity_names name then f rel else f @{term undefined}
+ | fold_transfer_rel f _ = f @{term undefined}
+
+fun filter_transfer_rules_by_rel transfer_rel transfer_rules =
+ let
+ val transfer_rel_name = transfer_rel |> dest_Const |> fst;
+ fun has_transfer_rel thm =
+ let
+ val concl = thm |> concl_of |> HOLogic.dest_Trueprop
+ in
+ member op= (fold_transfer_rel (fn tm => Term.add_const_names tm []) concl) transfer_rel_name
+ end
+ handle TERM _ => false
+ in
+ filter has_transfer_rel transfer_rules
+ end
+
+type restore_data = {quotient : Lifting_Info.quotient, transfer_rules: thm Item_Net.T}
+
+fun get_transfer_rel qinfo =
+ let
+ fun get_pcrel pcr_def = pcr_def |> concl_of |> Logic.dest_equals |> fst |> head_of
+ in
+ if is_some (#pcr_info qinfo)
+ then get_pcrel (#pcrel_def (the (#pcr_info qinfo)))
+ else quot_thm_crel (#quot_thm qinfo)
+ end
+
+fun pointer_of_bundle_name bundle_name ctxt =
+ let
+ val bundle_name = Bundle.check ctxt bundle_name
+ val bundle = Bundle.the_bundle ctxt bundle_name
+ in
+ case bundle of
+ [(_, [arg_src])] =>
+ (let
+ val ((_, tokens), _) = Args.dest_src arg_src
+ in
+ (fst (Args.name tokens))
+ handle _ => error "The provided bundle is not a lifting bundle."
+ end)
+ | _ => error "The provided bundle is not a lifting bundle."
+ end
+
+fun lifting_forget pointer lthy =
+ let
+ fun get_transfer_rules_to_delete qinfo ctxt =
+ let
+ fun get_pcrel pcr_def = pcr_def |> concl_of |> Logic.dest_equals |> fst |> head_of
+ val transfer_rel = if is_some (#pcr_info qinfo)
+ then get_pcrel (#pcrel_def (the (#pcr_info qinfo)))
+ else quot_thm_crel (#quot_thm qinfo)
+ in
+ filter_transfer_rules_by_rel transfer_rel (Transfer.get_transfer_raw ctxt)
+ end
+ in
+ case Lifting_Info.lookup_restore_data lthy pointer of
+ SOME restore_info =>
+ let
+ val qinfo = #quotient restore_info
+ val quot_thm = #quot_thm qinfo
+ val transfer_rules = get_transfer_rules_to_delete qinfo lthy
+ in
+ Local_Theory.declaration {syntax = false, pervasive = true}
+ (K (fold (Transfer.transfer_raw_del) transfer_rules #> Lifting_Info.delete_quotients quot_thm))
+ lthy
+ end
+ | NONE => error "The lifting bundle refers to non-existent restore data."
+ end
+
+
+fun lifting_forget_cmd bundle_name lthy =
+ lifting_forget (pointer_of_bundle_name bundle_name lthy) lthy
+
+
+val _ =
+ Outer_Syntax.local_theory @{command_spec "lifting_forget"}
+ "unsetup Lifting and Transfer for the given lifting bundle"
+ (Parse.position Parse.xname >> (lifting_forget_cmd))
+
+(* lifting_update *)
+
+fun update_transfer_rules pointer lthy =
+ let
+ fun new_transfer_rules { quotient = qinfo, ... } lthy =
+ let
+ val transfer_rel = get_transfer_rel qinfo
+ val transfer_rules = filter_transfer_rules_by_rel transfer_rel (Transfer.get_transfer_raw lthy)
+ in
+ fn phi => fold_rev
+ (Item_Net.update o Morphism.thm phi) transfer_rules Thm.full_rules
+ end
+ in
+ case Lifting_Info.lookup_restore_data lthy pointer of
+ SOME refresh_data =>
+ Local_Theory.declaration {syntax = false, pervasive = true}
+ (fn phi => Lifting_Info.add_transfer_rules_in_restore_data pointer
+ (new_transfer_rules refresh_data lthy phi)) lthy
+ | NONE => error "The lifting bundle refers to non-existent restore data."
+ end
+
+fun lifting_update_cmd bundle_name lthy =
+ update_transfer_rules (pointer_of_bundle_name bundle_name lthy) lthy
+
+val _ =
+ Outer_Syntax.local_theory @{command_spec "lifting_update"}
+ "add newly introduced transfer rules to a bundle storing the state of Lifting and Transfer"
+ (Parse.position Parse.xname >> lifting_update_cmd)
+
+end