1.1 --- a/etc/isar-keywords.el Mon Sep 16 11:54:57 2013 +0200
1.2 +++ b/etc/isar-keywords.el Mon Sep 16 15:30:17 2013 +0200
1.3 @@ -135,6 +135,8 @@
1.4 "lemmas"
1.5 "let"
1.6 "lift_definition"
1.7 + "lifting_forget"
1.8 + "lifting_update"
1.9 "linear_undo"
1.10 "local_setup"
1.11 "locale"
1.12 @@ -539,6 +541,8 @@
1.13 "instantiation"
1.14 "judgment"
1.15 "lemmas"
1.16 + "lifting_forget"
1.17 + "lifting_update"
1.18 "local_setup"
1.19 "locale"
1.20 "method_setup"
2.1 --- a/src/HOL/Lifting.thy Mon Sep 16 11:54:57 2013 +0200
2.2 +++ b/src/HOL/Lifting.thy Mon Sep 16 15:30:17 2013 +0200
2.3 @@ -11,7 +11,7 @@
2.4 "parametric" and
2.5 "print_quot_maps" "print_quotients" :: diag and
2.6 "lift_definition" :: thy_goal and
2.7 - "setup_lifting" :: thy_decl
2.8 + "setup_lifting" "lifting_forget" "lifting_update" :: thy_decl
2.9 begin
2.10
2.11 subsection {* Function map *}
3.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML Mon Sep 16 11:54:57 2013 +0200
3.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Mon Sep 16 15:30:17 2013 +0200
3.3 @@ -16,7 +16,7 @@
3.4 (binding * string option * mixfix) * string * (Facts.ref * Args.src list) option -> local_theory -> Proof.state
3.5
3.6 val can_generate_code_cert: thm -> bool
3.7 -end;
3.8 +end
3.9
3.10 structure Lifting_Def: LIFTING_DEF =
3.11 struct
3.12 @@ -583,4 +583,4 @@
3.13 (liftdef_parser >> lift_def_cmd_with_err_handling)
3.14
3.15
3.16 -end; (* structure *)
3.17 +end (* structure *)
4.1 --- a/src/HOL/Tools/Lifting/lifting_info.ML Mon Sep 16 11:54:57 2013 +0200
4.2 +++ b/src/HOL/Tools/Lifting/lifting_info.ML Mon Sep 16 15:30:17 2013 +0200
4.3 @@ -12,12 +12,19 @@
4.4
4.5 type pcr = {pcrel_def: thm, pcr_cr_eq: thm}
4.6 type quotient = {quot_thm: thm, pcr_info: pcr option}
4.7 + val pcr_eq: pcr * pcr -> bool
4.8 + val quotient_eq: quotient * quotient -> bool
4.9 val transform_quotient: morphism -> quotient -> quotient
4.10 val lookup_quotients: Proof.context -> string -> quotient option
4.11 val update_quotients: string -> quotient -> Context.generic -> Context.generic
4.12 val delete_quotients: thm -> Context.generic -> Context.generic
4.13 val print_quotients: Proof.context -> unit
4.14
4.15 + type restore_data = {quotient : quotient, transfer_rules: thm Item_Net.T}
4.16 + val lookup_restore_data: Proof.context -> string -> restore_data option
4.17 + val init_restore_data: string -> quotient -> Context.generic -> Context.generic
4.18 + val add_transfer_rules_in_restore_data: string -> thm Item_Net.T -> Context.generic -> Context.generic
4.19 +
4.20 val get_invariant_commute_rules: Proof.context -> thm list
4.21
4.22 val get_reflexivity_rules: Proof.context -> thm list
4.23 @@ -31,9 +38,10 @@
4.24 val get_quot_maps : Proof.context -> quot_map Symtab.table
4.25 val get_quotients : Proof.context -> quotient Symtab.table
4.26 val get_relator_distr_data : Proof.context -> relator_distr_data Symtab.table
4.27 + val get_restore_data : Proof.context -> restore_data Symtab.table
4.28
4.29 val setup: theory -> theory
4.30 -end;
4.31 +end
4.32
4.33 structure Lifting_Info: LIFTING_INFO =
4.34 struct
4.35 @@ -47,6 +55,7 @@
4.36 type quotient = {quot_thm: thm, pcr_info: pcr option}
4.37 type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm,
4.38 pos_distr_rules: thm list, neg_distr_rules: thm list}
4.39 +type restore_data = {quotient : quotient, transfer_rules: thm Item_Net.T}
4.40
4.41 structure Data = Generic_Data
4.42 (
4.43 @@ -54,44 +63,53 @@
4.44 { quot_maps : quot_map Symtab.table,
4.45 quotients : quotient Symtab.table,
4.46 reflexivity_rules : thm Item_Net.T,
4.47 - relator_distr_data : relator_distr_data Symtab.table
4.48 + relator_distr_data : relator_distr_data Symtab.table,
4.49 + restore_data : restore_data Symtab.table
4.50 }
4.51 val empty =
4.52 { quot_maps = Symtab.empty,
4.53 quotients = Symtab.empty,
4.54 reflexivity_rules = Thm.full_rules,
4.55 - relator_distr_data = Symtab.empty
4.56 + relator_distr_data = Symtab.empty,
4.57 + restore_data = Symtab.empty
4.58 }
4.59 val extend = I
4.60 fun merge
4.61 - ( { quot_maps = qm1, quotients = q1, reflexivity_rules = rr1, relator_distr_data = rdd1 },
4.62 - { quot_maps = qm2, quotients = q2, reflexivity_rules = rr2, relator_distr_data = rdd2 } ) =
4.63 + ( { quot_maps = qm1, quotients = q1, reflexivity_rules = rr1, relator_distr_data = rdd1,
4.64 + restore_data = rd1 },
4.65 + { quot_maps = qm2, quotients = q2, reflexivity_rules = rr2, relator_distr_data = rdd2,
4.66 + restore_data = rd2 } ) =
4.67 { quot_maps = Symtab.merge (K true) (qm1, qm2),
4.68 quotients = Symtab.merge (K true) (q1, q2),
4.69 reflexivity_rules = Item_Net.merge (rr1, rr2),
4.70 - relator_distr_data = Symtab.merge (K true) (rdd1, rdd2) }
4.71 + relator_distr_data = Symtab.merge (K true) (rdd1, rdd2),
4.72 + restore_data = Symtab.merge (K true) (rd1, rd2) }
4.73 )
4.74
4.75 -fun map_data f1 f2 f3 f4
4.76 - { quot_maps, quotients, reflexivity_rules, relator_distr_data} =
4.77 +fun map_data f1 f2 f3 f4 f5
4.78 + { quot_maps, quotients, reflexivity_rules, relator_distr_data, restore_data } =
4.79 { quot_maps = f1 quot_maps,
4.80 quotients = f2 quotients,
4.81 reflexivity_rules = f3 reflexivity_rules,
4.82 - relator_distr_data = f4 relator_distr_data }
4.83 + relator_distr_data = f4 relator_distr_data,
4.84 + restore_data = f5 restore_data }
4.85
4.86 -fun map_quot_maps f = map_data f I I I
4.87 -fun map_quotients f = map_data I f I I
4.88 -fun map_reflexivity_rules f = map_data I I f I
4.89 -fun map_relator_distr_data f = map_data I I I f
4.90 +fun map_quot_maps f = map_data f I I I I
4.91 +fun map_quotients f = map_data I f I I I
4.92 +fun map_reflexivity_rules f = map_data I I f I I
4.93 +fun map_relator_distr_data f = map_data I I I f I
4.94 +fun map_restore_data f = map_data I I I I f
4.95
4.96 val get_quot_maps' = #quot_maps o Data.get
4.97 val get_quotients' = #quotients o Data.get
4.98 val get_reflexivity_rules' = #reflexivity_rules o Data.get
4.99 val get_relator_distr_data' = #relator_distr_data o Data.get
4.100 +val get_restore_data' = #restore_data o Data.get
4.101
4.102 fun get_quot_maps ctxt = get_quot_maps' (Context.Proof ctxt)
4.103 fun get_quotients ctxt = get_quotients' (Context.Proof ctxt)
4.104 fun get_relator_distr_data ctxt = get_relator_distr_data' (Context.Proof ctxt)
4.105 +fun get_restore_data ctxt = get_restore_data' (Context.Proof ctxt)
4.106
4.107 (* info about Quotient map theorems *)
4.108
4.109 @@ -164,6 +182,20 @@
4.110 end
4.111
4.112 (* info about quotient types *)
4.113 +
4.114 +fun pcr_eq ({pcrel_def = pcrel_def1, pcr_cr_eq = pcr_cr_eq1},
4.115 + {pcrel_def = pcrel_def2, pcr_cr_eq = pcr_cr_eq2}) =
4.116 + Thm.eq_thm (pcrel_def1, pcrel_def2) andalso Thm.eq_thm (pcr_cr_eq1, pcr_cr_eq2)
4.117 +
4.118 +fun option_eq _ (NONE,NONE) = true
4.119 + | option_eq _ (NONE,_) = false
4.120 + | option_eq _ (_,NONE) = false
4.121 + | option_eq cmp (SOME x, SOME y) = cmp (x,y);
4.122 +
4.123 +fun quotient_eq ({quot_thm = quot_thm1, pcr_info = pcr_info1},
4.124 + {quot_thm = quot_thm2, pcr_info = pcr_info2}) =
4.125 + Thm.eq_thm (quot_thm1, quot_thm2) andalso option_eq pcr_eq (pcr_info1, pcr_info2)
4.126 +
4.127 fun transform_pcr_info phi {pcrel_def, pcr_cr_eq} =
4.128 {pcrel_def = Morphism.thm phi pcrel_def, pcr_cr_eq = Morphism.thm phi pcr_cr_eq}
4.129
4.130 @@ -209,6 +241,22 @@
4.131 Attrib.setup @{binding quot_del} (Scan.succeed (Thm.declaration_attribute delete_quotients))
4.132 "deletes the Quotient theorem"
4.133
4.134 +(* data for restoring Transfer/Lifting context *)
4.135 +
4.136 +fun lookup_restore_data ctxt bundle_name = Symtab.lookup (get_restore_data ctxt) bundle_name
4.137 +
4.138 +fun update_restore_data bundle_name restore_data ctxt =
4.139 + Data.map (map_restore_data (Symtab.update (bundle_name, restore_data))) ctxt
4.140 +
4.141 +fun init_restore_data bundle_name qinfo ctxt =
4.142 + update_restore_data bundle_name { quotient = qinfo, transfer_rules = Thm.full_rules } ctxt
4.143 +
4.144 +fun add_transfer_rules_in_restore_data bundle_name transfer_rules ctxt =
4.145 + case Symtab.lookup (get_restore_data' ctxt) bundle_name of
4.146 + SOME restore_data => update_restore_data bundle_name { quotient = #quotient restore_data,
4.147 + transfer_rules = Item_Net.merge ((#transfer_rules restore_data), transfer_rules) } ctxt
4.148 + | NONE => error ("The restore data " ^ quote bundle_name ^ " is not defined.")
4.149 +
4.150 (* theorems that a relator of an invariant is an invariant of the corresponding predicate *)
4.151
4.152 structure Invariant_Commute = Named_Thms
4.153 @@ -469,4 +517,4 @@
4.154 Outer_Syntax.improper_command @{command_spec "print_quotients"} "print quotients"
4.155 (Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
4.156
4.157 -end;
4.158 +end
5.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML Mon Sep 16 11:54:57 2013 +0200
5.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Mon Sep 16 15:30:17 2013 +0200
5.3 @@ -11,7 +11,9 @@
5.4 val setup_by_quotient: bool -> thm -> thm option -> thm option -> local_theory -> local_theory
5.5
5.6 val setup_by_typedef_thm: bool -> thm -> local_theory -> local_theory
5.7 -end;
5.8 +
5.9 + val lifting_restore: Lifting_Info.quotient -> Context.generic -> Context.generic
5.10 +end
5.11
5.12 structure Lifting_Setup: LIFTING_SETUP =
5.13 struct
5.14 @@ -164,8 +166,24 @@
5.15 else
5.16 lthy
5.17
5.18 +local
5.19 + exception QUOT_ERROR of Pretty.T list
5.20 +in
5.21 fun quot_thm_sanity_check ctxt quot_thm =
5.22 let
5.23 + val _ =
5.24 + if (nprems_of quot_thm > 0) then
5.25 + raise QUOT_ERROR [Pretty.block
5.26 + [Pretty.str "The Quotient theorem has extra assumptions:",
5.27 + Pretty.brk 1,
5.28 + Display.pretty_thm ctxt quot_thm]]
5.29 + else ()
5.30 + val _ = quot_thm |> concl_of |> HOLogic.dest_Trueprop |> dest_Quotient
5.31 + handle TERM _ => raise QUOT_ERROR
5.32 + [Pretty.block
5.33 + [Pretty.str "The Quotient theorem is not of the right form:",
5.34 + Pretty.brk 1,
5.35 + Display.pretty_thm ctxt quot_thm]]
5.36 val ((_, [quot_thm_fixed]), ctxt') = Variable.importT [quot_thm] ctxt
5.37 val (rty, qty) = quot_thm_rty_qty quot_thm_fixed
5.38 val rty_tfreesT = Term.add_tfree_namesT rty []
5.39 @@ -186,8 +204,31 @@
5.40 Pretty.str "is not a type constructor."]]
5.41 val errs = extra_rty_tfrees @ not_type_constr
5.42 in
5.43 - if null errs then () else error (cat_lines (["Sanity check of the quotient theorem failed:",""]
5.44 - @ (map Pretty.string_of errs)))
5.45 + if null errs then () else raise QUOT_ERROR errs
5.46 + end
5.47 + handle QUOT_ERROR errs => error (cat_lines (["Sanity check of the quotient theorem failed:"]
5.48 + @ (map (Pretty.string_of o Pretty.item o single) errs)))
5.49 +end
5.50 +
5.51 +fun lifting_bundle qty_full_name qinfo lthy =
5.52 + let
5.53 + fun qualify suffix defname = Binding.qualified true suffix defname
5.54 + val binding = qty_full_name |> Long_Name.base_name |> Binding.name |> qualify "lifting"
5.55 + val morphed_binding = Morphism.binding (Local_Theory.target_morphism lthy) binding
5.56 + val bundle_name = Name_Space.full_name (Name_Space.naming_of
5.57 + (Context.Theory (Proof_Context.theory_of lthy))) morphed_binding
5.58 + fun phi_qinfo phi = Lifting_Info.transform_quotient phi qinfo
5.59 +
5.60 + val thy = Proof_Context.theory_of lthy
5.61 + val dummy_thm = Thm.transfer thy Drule.dummy_thm
5.62 + val pointer = Outer_Syntax.scan Position.none bundle_name
5.63 + val restore_lifting_att =
5.64 + ([dummy_thm], [Args.src (("Lifting.lifting_restore_internal", pointer), Position.none)])
5.65 + in
5.66 + lthy
5.67 + |> Local_Theory.declaration {syntax = false, pervasive = true}
5.68 + (fn phi => Lifting_Info.init_restore_data bundle_name (phi_qinfo phi))
5.69 + |> Bundle.bundle ((binding, [restore_lifting_att])) []
5.70 end
5.71
5.72 fun setup_lifting_infr gen_code quot_thm opt_reflp_thm lthy =
5.73 @@ -221,23 +262,24 @@
5.74 lthy
5.75 |> Local_Theory.declaration {syntax = false, pervasive = true}
5.76 (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi))
5.77 + |> lifting_bundle qty_full_name quotients
5.78 end
5.79
5.80 local
5.81 fun importT_inst_exclude exclude ts ctxt =
5.82 let
5.83 - val tvars = rev (subtract op= exclude (fold Term.add_tvars ts []));
5.84 - val (tfrees, ctxt') = Variable.invent_types (map #2 tvars) ctxt;
5.85 + val tvars = rev (subtract op= exclude (fold Term.add_tvars ts []))
5.86 + val (tfrees, ctxt') = Variable.invent_types (map #2 tvars) ctxt
5.87 in (tvars ~~ map TFree tfrees, ctxt') end
5.88
5.89 fun import_inst_exclude exclude ts ctxt =
5.90 let
5.91 val excludeT = fold (Term.add_tvarsT o snd) exclude []
5.92 - val (instT, ctxt') = importT_inst_exclude excludeT ts ctxt;
5.93 + val (instT, ctxt') = importT_inst_exclude excludeT ts ctxt
5.94 val vars = map (apsnd (Term_Subst.instantiateT instT))
5.95 - (rev (subtract op= exclude (fold Term.add_vars ts [])));
5.96 - val (xs, ctxt'') = Variable.variant_fixes (map (#1 o #1) vars) ctxt';
5.97 - val inst = vars ~~ map Free (xs ~~ map #2 vars);
5.98 + (rev (subtract op= exclude (fold Term.add_vars ts [])))
5.99 + val (xs, ctxt'') = Variable.variant_fixes (map (#1 o #1) vars) ctxt'
5.100 + val inst = vars ~~ map Free (xs ~~ map #2 vars)
5.101 in ((instT, inst), ctxt'') end
5.102
5.103 fun import_terms_exclude exclude ts ctxt =
5.104 @@ -328,16 +370,16 @@
5.105 val orig_lthy = lthy
5.106 (* it doesn't raise an exception because it would have already raised it in define_pcrel *)
5.107 val (quot_thm, _, lthy) = Lifting_Term.prove_param_quot_thm lthy rty
5.108 - val parametrized_relator = singleton (Variable.export_terms lthy orig_lthy) (quot_thm_crel quot_thm);
5.109 + val parametrized_relator = singleton (Variable.export_terms lthy orig_lthy) (quot_thm_crel quot_thm)
5.110 val lthy = orig_lthy
5.111 val id_transfer =
5.112 @{thm id_transfer}
5.113 |> Thm.incr_indexes (Term.maxidx_of_term parametrized_relator + 1)
5.114 |> Conv.fconv_rule(HOLogic.Trueprop_conv (Conv.arg_conv id_unfold then_conv Conv.arg1_conv id_unfold))
5.115 - val var = Var (hd (Term.add_vars (prop_of id_transfer) []));
5.116 - val thy = Proof_Context.theory_of lthy;
5.117 + val var = Var (hd (Term.add_vars (prop_of id_transfer) []))
5.118 + val thy = Proof_Context.theory_of lthy
5.119 val inst = [(cterm_of thy var, cterm_of thy parametrized_relator)]
5.120 - val id_par_thm = Drule.cterm_instantiate inst id_transfer;
5.121 + val id_par_thm = Drule.cterm_instantiate inst id_transfer
5.122 in
5.123 Lifting_Def.generate_parametric_transfer_rule lthy id_transfer_rule id_par_thm
5.124 end
5.125 @@ -362,7 +404,7 @@
5.126 val ct = thm |> cprop_of |> Drule.strip_imp_concl |> Thm.dest_arg |> Thm.dest_arg1 |> Thm.dest_arg
5.127 val pcrel_def = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) pcrel_def
5.128 val thm = Thm.instantiate (Thm.match (ct, Thm.rhs_of pcrel_def)) thm
5.129 - handle Pattern.MATCH => raise CTERM ("fold_Domainp_pcrel", [ct, Thm.rhs_of pcrel_def]);
5.130 + handle Pattern.MATCH => raise CTERM ("fold_Domainp_pcrel", [ct, Thm.rhs_of pcrel_def])
5.131 in
5.132 rewrite_first_Domainp_arg (Thm.symmetric pcrel_def) thm
5.133 end
5.134 @@ -734,4 +776,243 @@
5.135 -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse_Spec.xthm) >>
5.136 (fn (((gen_code, xthm), opt_reflp_xthm), opt_par_xthm) =>
5.137 setup_lifting_cmd gen_code xthm opt_reflp_xthm opt_par_xthm))
5.138 -end;
5.139 +
5.140 +(* restoring lifting infrastructure *)
5.141 +
5.142 +local
5.143 + exception PCR_ERROR of Pretty.T list
5.144 +in
5.145 +
5.146 +fun lifting_restore_sanity_check ctxt (qinfo:Lifting_Info.quotient) =
5.147 + let
5.148 + val quot_thm = (#quot_thm qinfo)
5.149 + val _ = quot_thm_sanity_check ctxt quot_thm
5.150 + val pcr_info_err =
5.151 + (case #pcr_info qinfo of
5.152 + SOME pcr =>
5.153 + let
5.154 + val pcrel_def = #pcrel_def pcr
5.155 + val pcr_cr_eq = #pcr_cr_eq pcr
5.156 + val (def_lhs, _) = Logic.dest_equals (prop_of pcrel_def)
5.157 + handle TERM _ => raise PCR_ERROR [Pretty.block
5.158 + [Pretty.str "The pcr definiton theorem is not a plain meta equation:",
5.159 + Pretty.brk 1,
5.160 + Display.pretty_thm ctxt pcrel_def]]
5.161 + val pcr_const_def = head_of def_lhs
5.162 + val (eq_lhs, eq_rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of pcr_cr_eq))
5.163 + handle TERM _ => raise PCR_ERROR [Pretty.block
5.164 + [Pretty.str "The pcr_cr equation theorem is not a plain equation:",
5.165 + Pretty.brk 1,
5.166 + Display.pretty_thm ctxt pcr_cr_eq]]
5.167 + val (pcr_const_eq, eqs) = strip_comb eq_lhs
5.168 + fun is_eq (Const ("HOL.eq", _)) = true
5.169 + | is_eq _ = false
5.170 + fun eq_Const (Const (name1, _)) (Const (name2, _)) = (name1 = name2)
5.171 + | eq_Const _ _ = false
5.172 + val all_eqs = if not (forall is_eq eqs) then
5.173 + [Pretty.block
5.174 + [Pretty.str "Arguments of the lhs of the pcr_cr equation theorem are not only equalities:",
5.175 + Pretty.brk 1,
5.176 + Display.pretty_thm ctxt pcr_cr_eq]]
5.177 + else []
5.178 + val pcr_consts_not_equal = if not (eq_Const pcr_const_def pcr_const_eq) then
5.179 + [Pretty.block
5.180 + [Pretty.str "Parametrized correspondence relation constants in pcr_def and pcr_cr_eq are not equal:",
5.181 + Pretty.brk 1,
5.182 + Syntax.pretty_term ctxt pcr_const_def,
5.183 + Pretty.brk 1,
5.184 + Pretty.str "vs.",
5.185 + Pretty.brk 1,
5.186 + Syntax.pretty_term ctxt pcr_const_eq]]
5.187 + else []
5.188 + val crel = quot_thm_crel quot_thm
5.189 + val cr_consts_not_equal = if not (eq_Const crel eq_rhs) then
5.190 + [Pretty.block
5.191 + [Pretty.str "Correspondence relation constants in the Quotient theorem and pcr_cr_eq are not equal:",
5.192 + Pretty.brk 1,
5.193 + Syntax.pretty_term ctxt crel,
5.194 + Pretty.brk 1,
5.195 + Pretty.str "vs.",
5.196 + Pretty.brk 1,
5.197 + Syntax.pretty_term ctxt eq_rhs]]
5.198 + else []
5.199 + in
5.200 + all_eqs @ pcr_consts_not_equal @ cr_consts_not_equal
5.201 + end
5.202 + | NONE => [])
5.203 + val errs = pcr_info_err
5.204 + in
5.205 + if null errs then () else raise PCR_ERROR errs
5.206 + end
5.207 + handle PCR_ERROR errs => error (cat_lines (["Sanity check failed:"]
5.208 + @ (map (Pretty.string_of o Pretty.item o single) errs)))
5.209 +end
5.210 +
5.211 +fun lifting_restore qinfo ctxt =
5.212 + let
5.213 + val _ = lifting_restore_sanity_check (Context.proof_of ctxt) qinfo
5.214 + val (_, qty) = quot_thm_rty_qty (#quot_thm qinfo)
5.215 + val qty_full_name = (fst o dest_Type) qty
5.216 + val stored_qinfo = Lifting_Info.lookup_quotients (Context.proof_of ctxt) qty_full_name
5.217 + in
5.218 + if is_some (stored_qinfo) andalso not (Lifting_Info.quotient_eq (qinfo, (the stored_qinfo)))
5.219 + then error (Pretty.string_of
5.220 + (Pretty.block
5.221 + [Pretty.str "Lifting is already setup for the type",
5.222 + Pretty.brk 1,
5.223 + Pretty.quote (Syntax.pretty_typ (Context.proof_of ctxt) qty)]))
5.224 + else Lifting_Info.update_quotients qty_full_name qinfo ctxt
5.225 + end
5.226 +
5.227 +val parse_opt_pcr =
5.228 + Scan.optional (Attrib.thm -- Attrib.thm >>
5.229 + (fn (pcrel_def, pcr_cr_eq) => SOME {pcrel_def = pcrel_def, pcr_cr_eq = pcr_cr_eq})) NONE
5.230 +
5.231 +val lifting_restore_attribute_setup =
5.232 + Attrib.setup @{binding lifting_restore}
5.233 + ((Attrib.thm -- parse_opt_pcr) >>
5.234 + (fn (quot_thm, opt_pcr) =>
5.235 + let val qinfo = { quot_thm = quot_thm, pcr_info = opt_pcr}
5.236 + in Thm.declaration_attribute (K (lifting_restore qinfo)) end))
5.237 + "restoring lifting infrastructure"
5.238 +
5.239 +val _ = Theory.setup lifting_restore_attribute_setup
5.240 +
5.241 +fun lifting_restore_internal bundle_name ctxt =
5.242 + let
5.243 + val restore_info = Lifting_Info.lookup_restore_data (Context.proof_of ctxt) bundle_name
5.244 + in
5.245 + case restore_info of
5.246 + SOME restore_info =>
5.247 + ctxt
5.248 + |> lifting_restore (#quotient restore_info)
5.249 + |> fold_rev Transfer.transfer_raw_add (Item_Net.content (#transfer_rules restore_info))
5.250 + | NONE => ctxt
5.251 + end
5.252 +
5.253 +val lifting_restore_internal_attribute_setup =
5.254 + Attrib.setup @{binding lifting_restore_internal}
5.255 + (Scan.lift Args.name >> (fn name => Thm.declaration_attribute (K (lifting_restore_internal name))))
5.256 + "restoring lifting infrastructure; internal attribute; not meant to be used directly by regular users"
5.257 +
5.258 +val _ = Theory.setup lifting_restore_internal_attribute_setup
5.259 +
5.260 +(* lifting_forget *)
5.261 +
5.262 +val monotonicity_names = [@{const_name right_unique}, @{const_name left_unique}, @{const_name right_total},
5.263 + @{const_name left_total}, @{const_name bi_unique}, @{const_name bi_total}]
5.264 +
5.265 +fun fold_transfer_rel f (Const (@{const_name "Transfer.Rel"}, _) $ rel $ _ $ _) = f rel
5.266 + | fold_transfer_rel f (Const (@{const_name "HOL.eq"}, _) $
5.267 + (Const (@{const_name Domainp}, _) $ rel) $ _) = f rel
5.268 + | fold_transfer_rel f (Const (name, _) $ rel) =
5.269 + if member op= monotonicity_names name then f rel else f @{term undefined}
5.270 + | fold_transfer_rel f _ = f @{term undefined}
5.271 +
5.272 +fun filter_transfer_rules_by_rel transfer_rel transfer_rules =
5.273 + let
5.274 + val transfer_rel_name = transfer_rel |> dest_Const |> fst;
5.275 + fun has_transfer_rel thm =
5.276 + let
5.277 + val concl = thm |> concl_of |> HOLogic.dest_Trueprop
5.278 + in
5.279 + member op= (fold_transfer_rel (fn tm => Term.add_const_names tm []) concl) transfer_rel_name
5.280 + end
5.281 + handle TERM _ => false
5.282 + in
5.283 + filter has_transfer_rel transfer_rules
5.284 + end
5.285 +
5.286 +type restore_data = {quotient : Lifting_Info.quotient, transfer_rules: thm Item_Net.T}
5.287 +
5.288 +fun get_transfer_rel qinfo =
5.289 + let
5.290 + fun get_pcrel pcr_def = pcr_def |> concl_of |> Logic.dest_equals |> fst |> head_of
5.291 + in
5.292 + if is_some (#pcr_info qinfo)
5.293 + then get_pcrel (#pcrel_def (the (#pcr_info qinfo)))
5.294 + else quot_thm_crel (#quot_thm qinfo)
5.295 + end
5.296 +
5.297 +fun pointer_of_bundle_name bundle_name ctxt =
5.298 + let
5.299 + val bundle_name = Bundle.check ctxt bundle_name
5.300 + val bundle = Bundle.the_bundle ctxt bundle_name
5.301 + in
5.302 + case bundle of
5.303 + [(_, [arg_src])] =>
5.304 + (let
5.305 + val ((_, tokens), _) = Args.dest_src arg_src
5.306 + in
5.307 + (fst (Args.name tokens))
5.308 + handle _ => error "The provided bundle is not a lifting bundle."
5.309 + end)
5.310 + | _ => error "The provided bundle is not a lifting bundle."
5.311 + end
5.312 +
5.313 +fun lifting_forget pointer lthy =
5.314 + let
5.315 + fun get_transfer_rules_to_delete qinfo ctxt =
5.316 + let
5.317 + fun get_pcrel pcr_def = pcr_def |> concl_of |> Logic.dest_equals |> fst |> head_of
5.318 + val transfer_rel = if is_some (#pcr_info qinfo)
5.319 + then get_pcrel (#pcrel_def (the (#pcr_info qinfo)))
5.320 + else quot_thm_crel (#quot_thm qinfo)
5.321 + in
5.322 + filter_transfer_rules_by_rel transfer_rel (Transfer.get_transfer_raw ctxt)
5.323 + end
5.324 + in
5.325 + case Lifting_Info.lookup_restore_data lthy pointer of
5.326 + SOME restore_info =>
5.327 + let
5.328 + val qinfo = #quotient restore_info
5.329 + val quot_thm = #quot_thm qinfo
5.330 + val transfer_rules = get_transfer_rules_to_delete qinfo lthy
5.331 + in
5.332 + Local_Theory.declaration {syntax = false, pervasive = true}
5.333 + (K (fold (Transfer.transfer_raw_del) transfer_rules #> Lifting_Info.delete_quotients quot_thm))
5.334 + lthy
5.335 + end
5.336 + | NONE => error "The lifting bundle refers to non-existent restore data."
5.337 + end
5.338 +
5.339 +
5.340 +fun lifting_forget_cmd bundle_name lthy =
5.341 + lifting_forget (pointer_of_bundle_name bundle_name lthy) lthy
5.342 +
5.343 +
5.344 +val _ =
5.345 + Outer_Syntax.local_theory @{command_spec "lifting_forget"}
5.346 + "unsetup Lifting and Transfer for the given lifting bundle"
5.347 + (Parse.position Parse.xname >> (lifting_forget_cmd))
5.348 +
5.349 +(* lifting_update *)
5.350 +
5.351 +fun update_transfer_rules pointer lthy =
5.352 + let
5.353 + fun new_transfer_rules { quotient = qinfo, ... } lthy =
5.354 + let
5.355 + val transfer_rel = get_transfer_rel qinfo
5.356 + val transfer_rules = filter_transfer_rules_by_rel transfer_rel (Transfer.get_transfer_raw lthy)
5.357 + in
5.358 + fn phi => fold_rev
5.359 + (Item_Net.update o Morphism.thm phi) transfer_rules Thm.full_rules
5.360 + end
5.361 + in
5.362 + case Lifting_Info.lookup_restore_data lthy pointer of
5.363 + SOME refresh_data =>
5.364 + Local_Theory.declaration {syntax = false, pervasive = true}
5.365 + (fn phi => Lifting_Info.add_transfer_rules_in_restore_data pointer
5.366 + (new_transfer_rules refresh_data lthy phi)) lthy
5.367 + | NONE => error "The lifting bundle refers to non-existent restore data."
5.368 + end
5.369 +
5.370 +fun lifting_update_cmd bundle_name lthy =
5.371 + update_transfer_rules (pointer_of_bundle_name bundle_name lthy) lthy
5.372 +
5.373 +val _ =
5.374 + Outer_Syntax.local_theory @{command_spec "lifting_update"}
5.375 + "add newly introduced transfer rules to a bundle storing the state of Lifting and Transfer"
5.376 + (Parse.position Parse.xname >> lifting_update_cmd)
5.377 +
5.378 +end
6.1 --- a/src/HOL/Tools/Lifting/lifting_term.ML Mon Sep 16 11:54:57 2013 +0200
6.2 +++ b/src/HOL/Tools/Lifting/lifting_term.ML Mon Sep 16 15:30:17 2013 +0200
6.3 @@ -523,4 +523,4 @@
6.4 Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.fun2_conv parametrize_relation_conv)) thm
6.5 end
6.6
6.7 -end;
6.8 +end
7.1 --- a/src/HOL/Tools/Lifting/lifting_util.ML Mon Sep 16 11:54:57 2013 +0200
7.2 +++ b/src/HOL/Tools/Lifting/lifting_util.ML Mon Sep 16 15:30:17 2013 +0200
7.3 @@ -28,7 +28,7 @@
7.4 val relation_types: typ -> typ * typ
7.5 val mk_HOL_eq: thm -> thm
7.6 val safe_HOL_meta_eq: thm -> thm
7.7 -end;
7.8 +end
7.9
7.10
7.11 structure Lifting_Util: LIFTING_UTIL =
7.12 @@ -110,4 +110,4 @@
7.13
7.14 fun safe_HOL_meta_eq r = mk_HOL_eq r handle Thm.THM _ => r
7.15
7.16 -end;
7.17 +end