# HG changeset patch # User panny # Date 1379342888 -7200 # Node ID aeb3cf02c678e6a3c199c5ea1d8744894485c524 # Parent 8b9ea4420f817633d0f1393f9f6b967ceb867433# Parent a792a504ff2262fb9ffe7e16e584ea994bd6870b merge diff -r 8b9ea4420f81 -r aeb3cf02c678 etc/isar-keywords.el --- a/etc/isar-keywords.el Mon Sep 16 15:03:23 2013 +0200 +++ b/etc/isar-keywords.el Mon Sep 16 16:48:08 2013 +0200 @@ -135,6 +135,8 @@ "lemmas" "let" "lift_definition" + "lifting_forget" + "lifting_update" "linear_undo" "local_setup" "locale" @@ -539,6 +541,8 @@ "instantiation" "judgment" "lemmas" + "lifting_forget" + "lifting_update" "local_setup" "locale" "method_setup" diff -r 8b9ea4420f81 -r aeb3cf02c678 src/HOL/Int.thy --- a/src/HOL/Int.thy Mon Sep 16 15:03:23 2013 +0200 +++ b/src/HOL/Int.thy Mon Sep 16 16:48:08 2013 +0200 @@ -1660,12 +1660,7 @@ text {* De-register @{text "int"} as a quotient type: *} -lemmas [transfer_rule del] = - int.id_abs_transfer int.rel_eq_transfer zero_int.transfer one_int.transfer - plus_int.transfer uminus_int.transfer minus_int.transfer times_int.transfer - int_transfer less_eq_int.transfer less_int.transfer of_int.transfer - nat.transfer int.right_unique int.right_total int.bi_total - -declare Quotient_int [quot_del] +lifting_update int.lifting +lifting_forget int.lifting end diff -r 8b9ea4420f81 -r aeb3cf02c678 src/HOL/Lifting.thy --- a/src/HOL/Lifting.thy Mon Sep 16 15:03:23 2013 +0200 +++ b/src/HOL/Lifting.thy Mon Sep 16 16:48:08 2013 +0200 @@ -11,7 +11,7 @@ "parametric" and "print_quot_maps" "print_quotients" :: diag and "lift_definition" :: thy_goal and - "setup_lifting" :: thy_decl + "setup_lifting" "lifting_forget" "lifting_update" :: thy_decl begin subsection {* Function map *} diff -r 8b9ea4420f81 -r aeb3cf02c678 src/HOL/Quotient_Examples/Int_Pow.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Quotient_Examples/Int_Pow.thy Mon Sep 16 16:48:08 2013 +0200 @@ -0,0 +1,146 @@ +(* Title: HOL/Quotient_Examples/Int_Pow.thy + Author: Ondrej Kuncar + Author: Lars Noschinski +*) + +theory Int_Pow +imports Main "~~/src/HOL/Algebra/Group" +begin + +(* + This file demonstrates how to restore Lifting/Transfer enviromenent. + + We want to define int_pow (a power with an integer exponent) by directly accessing + the representation type "nat * nat" that was used to define integers. +*) + +context monoid +begin + +(* first some additional lemmas that are missing in monoid *) + +lemma Units_nat_pow_Units [intro, simp]: + "a \ Units G \ a (^) (c :: nat) \ Units G" by (induct c) auto + +lemma Units_r_cancel [simp]: + "[| z \ Units G; x \ carrier G; y \ carrier G |] ==> + (x \ z = y \ z) = (x = y)" +proof + assume eq: "x \ z = y \ z" + and G: "z \ Units G" "x \ carrier G" "y \ carrier G" + then have "x \ (z \ inv z) = y \ (z \ inv z)" + by (simp add: m_assoc[symmetric] Units_closed del: Units_r_inv) + with G show "x = y" by simp +next + assume eq: "x = y" + and G: "z \ Units G" "x \ carrier G" "y \ carrier G" + then show "x \ z = y \ z" by simp +qed + +lemma inv_mult_units: + "[| x \ Units G; y \ Units G |] ==> inv (x \ y) = inv y \ inv x" +proof - + assume G: "x \ Units G" "y \ Units G" + moreover then have "x \ carrier G" "y \ carrier G" by auto + ultimately have "inv (x \ y) \ (x \ y) = (inv y \ inv x) \ (x \ y)" + by (simp add: m_assoc) (simp add: m_assoc [symmetric]) + with G show ?thesis by (simp del: Units_l_inv) +qed + +lemma mult_same_comm: + assumes [simp, intro]: "a \ Units G" + shows "a (^) (m::nat) \ inv (a (^) (n::nat)) = inv (a (^) n) \ a (^) m" +proof (cases "m\n") + have [simp]: "a \ carrier G" using `a \ _` by (rule Units_closed) + case True + then obtain k where *:"m = k + n" and **:"m = n + k" by (metis Nat.le_iff_add nat_add_commute) + have "a (^) (m::nat) \ inv (a (^) (n::nat)) = a (^) k" + using * by (auto simp add: nat_pow_mult[symmetric] m_assoc) + also have "\ = inv (a (^) n) \ a (^) m" + using ** by (auto simp add: nat_pow_mult[symmetric] m_assoc[symmetric]) + finally show ?thesis . +next + have [simp]: "a \ carrier G" using `a \ _` by (rule Units_closed) + case False + then obtain k where *:"n = k + m" and **:"n = m + k" + by (metis Nat.le_iff_add nat_add_commute nat_le_linear) + have "a (^) (m::nat) \ inv (a (^) (n::nat)) = inv(a (^) k)" + using * by (auto simp add: nat_pow_mult[symmetric] m_assoc[symmetric] inv_mult_units) + also have "\ = inv (a (^) n) \ a (^) m" + using ** by (auto simp add: nat_pow_mult[symmetric] m_assoc inv_mult_units) + finally show ?thesis . +qed + +lemma mult_inv_same_comm: + "a \ Units G \ inv (a (^) (m::nat)) \ inv (a (^) (n::nat)) = inv (a (^) n) \ inv (a (^) m)" +by (simp add: inv_mult_units[symmetric] nat_pow_mult ac_simps Units_closed) + +context +includes int.lifting (* restores Lifting/Transfer for integers *) +begin + +lemma int_pow_rsp: + assumes eq: "(b::nat) + e = d + c" + assumes a_in_G [simp, intro]: "a \ Units G" + shows "a (^) b \ inv (a (^) c) = a (^) d \ inv (a (^) e)" +proof(cases "b\c") + have [simp]: "a \ carrier G" using `a \ _` by (rule Units_closed) + case True + then obtain n where "b = n + c" by (metis Nat.le_iff_add nat_add_commute) + then have "d = n + e" using eq by arith + from `b = _` have "a (^) b \ inv (a (^) c) = a (^) n" + by (auto simp add: nat_pow_mult[symmetric] m_assoc) + also from `d = _` have "\ = a (^) d \ inv (a (^) e)" + by (auto simp add: nat_pow_mult[symmetric] m_assoc) + finally show ?thesis . +next + have [simp]: "a \ carrier G" using `a \ _` by (rule Units_closed) + case False + then obtain n where "c = n + b" by (metis Nat.le_iff_add nat_add_commute nat_le_linear) + then have "e = n + d" using eq by arith + from `c = _` have "a (^) b \ inv (a (^) c) = inv (a (^) n)" + by (auto simp add: nat_pow_mult[symmetric] m_assoc[symmetric] inv_mult_units) + also from `e = _` have "\ = a (^) d \ inv (a (^) e)" + by (auto simp add: nat_pow_mult[symmetric] m_assoc[symmetric] inv_mult_units) + finally show ?thesis . +qed + +(* + This definition is more convinient than the definition in HOL/Algebra/Group because + it doesn't contain a test z < 0 when a (^) z is being defined. +*) + +lift_definition int_pow :: "('a, 'm) monoid_scheme \ 'a \ int \ 'a" is + "\G a (n1, n2). if a \ Units G \ monoid G then (a (^)\<^bsub>G\<^esub> n1) \\<^bsub>G\<^esub> (inv\<^bsub>G\<^esub> (a (^)\<^bsub>G\<^esub> n2)) else \\<^bsub>G\<^esub>" +unfolding intrel_def by (auto intro: monoid.int_pow_rsp) + +(* + Thus, for example, the proof of distributivity of int_pow and addition + doesn't require a substantial number of case distinctions. +*) + +lemma int_pow_dist: + assumes [simp]: "a \ Units G" + shows "int_pow G a ((n::int) + m) = int_pow G a n \\<^bsub>G\<^esub> int_pow G a m" +proof - + { + fix k l m :: nat + have "a (^) l \ (inv (a (^) m) \ inv (a (^) k)) = (a (^) l \ inv (a (^) k)) \ inv (a (^) m)" + (is "?lhs = _") + by (simp add: mult_inv_same_comm m_assoc Units_closed) + also have "\ = (inv (a (^) k) \ a (^) l) \ inv (a (^) m)" + by (simp add: mult_same_comm) + also have "\ = inv (a (^) k) \ (a (^) l \ inv (a (^) m))" (is "_ = ?rhs") + by (simp add: m_assoc Units_closed) + finally have "?lhs = ?rhs" . + } + then show ?thesis + by (transfer fixing: G) (auto simp add: nat_pow_mult[symmetric] inv_mult_units m_assoc Units_closed) +qed + +end + +lifting_update int.lifting +lifting_forget int.lifting + +end diff -r 8b9ea4420f81 -r aeb3cf02c678 src/HOL/Rat.thy --- a/src/HOL/Rat.thy Mon Sep 16 15:03:23 2013 +0200 +++ b/src/HOL/Rat.thy Mon Sep 16 16:48:08 2013 +0200 @@ -1143,20 +1143,12 @@ lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::rat)" by simp +subsection {* Hiding implementation details *} hide_const (open) normalize positive -lemmas [transfer_rule del] = - rat.rel_eq_transfer - Fract.transfer zero_rat.transfer one_rat.transfer plus_rat.transfer - uminus_rat.transfer times_rat.transfer inverse_rat.transfer - positive.transfer of_rat.transfer rat.right_unique rat.right_total - -lemmas [transfer_domain_rule del] = Domainp_cr_rat rat.domain - -text {* De-register @{text "rat"} as a quotient type: *} - -declare Quotient_rat[quot_del] +lifting_update rat.lifting +lifting_forget rat.lifting end diff -r 8b9ea4420f81 -r aeb3cf02c678 src/HOL/Real.thy --- a/src/HOL/Real.thy Mon Sep 16 15:03:23 2013 +0200 +++ b/src/HOL/Real.thy Mon Sep 16 16:48:08 2013 +0200 @@ -987,14 +987,8 @@ declare Abs_real_induct [induct del] declare Abs_real_cases [cases del] -lemmas [transfer_rule del] = - real.rel_eq_transfer - zero_real.transfer one_real.transfer plus_real.transfer uminus_real.transfer - times_real.transfer inverse_real.transfer positive.transfer real.right_unique - real.right_total - -lemmas [transfer_domain_rule del] = - real.domain real.domain_eq Domainp_pcr_real real.domain_par real.domain_par_left_total +lifting_update real.lifting +lifting_forget real.lifting subsection{*More Lemmas*} diff -r 8b9ea4420f81 -r aeb3cf02c678 src/HOL/Tools/Lifting/lifting_def.ML --- a/src/HOL/Tools/Lifting/lifting_def.ML Mon Sep 16 15:03:23 2013 +0200 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Mon Sep 16 16:48:08 2013 +0200 @@ -16,7 +16,7 @@ (binding * string option * mixfix) * string * (Facts.ref * Args.src list) option -> local_theory -> Proof.state val can_generate_code_cert: thm -> bool -end; +end structure Lifting_Def: LIFTING_DEF = struct @@ -583,4 +583,4 @@ (liftdef_parser >> lift_def_cmd_with_err_handling) -end; (* structure *) +end (* structure *) diff -r 8b9ea4420f81 -r aeb3cf02c678 src/HOL/Tools/Lifting/lifting_info.ML --- a/src/HOL/Tools/Lifting/lifting_info.ML Mon Sep 16 15:03:23 2013 +0200 +++ b/src/HOL/Tools/Lifting/lifting_info.ML Mon Sep 16 16:48:08 2013 +0200 @@ -12,11 +12,19 @@ type pcr = {pcrel_def: thm, pcr_cr_eq: thm} type quotient = {quot_thm: thm, pcr_info: pcr option} + val pcr_eq: pcr * pcr -> bool + val quotient_eq: quotient * quotient -> bool val transform_quotient: morphism -> quotient -> quotient val lookup_quotients: Proof.context -> string -> quotient option val update_quotients: string -> quotient -> Context.generic -> Context.generic + val delete_quotients: thm -> Context.generic -> Context.generic val print_quotients: Proof.context -> unit + type restore_data = {quotient : quotient, transfer_rules: thm Item_Net.T} + val lookup_restore_data: Proof.context -> string -> restore_data option + val init_restore_data: string -> quotient -> Context.generic -> Context.generic + val add_transfer_rules_in_restore_data: string -> thm Item_Net.T -> Context.generic -> Context.generic + val get_invariant_commute_rules: Proof.context -> thm list val get_reflexivity_rules: Proof.context -> thm list @@ -30,9 +38,10 @@ val get_quot_maps : Proof.context -> quot_map Symtab.table val get_quotients : Proof.context -> quotient Symtab.table val get_relator_distr_data : Proof.context -> relator_distr_data Symtab.table + val get_restore_data : Proof.context -> restore_data Symtab.table val setup: theory -> theory -end; +end structure Lifting_Info: LIFTING_INFO = struct @@ -46,6 +55,7 @@ type quotient = {quot_thm: thm, pcr_info: pcr option} type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm, pos_distr_rules: thm list, neg_distr_rules: thm list} +type restore_data = {quotient : quotient, transfer_rules: thm Item_Net.T} structure Data = Generic_Data ( @@ -53,44 +63,53 @@ { quot_maps : quot_map Symtab.table, quotients : quotient Symtab.table, reflexivity_rules : thm Item_Net.T, - relator_distr_data : relator_distr_data Symtab.table + relator_distr_data : relator_distr_data Symtab.table, + restore_data : restore_data Symtab.table } val empty = { quot_maps = Symtab.empty, quotients = Symtab.empty, reflexivity_rules = Thm.full_rules, - relator_distr_data = Symtab.empty + relator_distr_data = Symtab.empty, + restore_data = Symtab.empty } val extend = I fun merge - ( { quot_maps = qm1, quotients = q1, reflexivity_rules = rr1, relator_distr_data = rdd1 }, - { quot_maps = qm2, quotients = q2, reflexivity_rules = rr2, relator_distr_data = rdd2 } ) = + ( { quot_maps = qm1, quotients = q1, reflexivity_rules = rr1, relator_distr_data = rdd1, + restore_data = rd1 }, + { quot_maps = qm2, quotients = q2, reflexivity_rules = rr2, relator_distr_data = rdd2, + restore_data = rd2 } ) = { quot_maps = Symtab.merge (K true) (qm1, qm2), quotients = Symtab.merge (K true) (q1, q2), reflexivity_rules = Item_Net.merge (rr1, rr2), - relator_distr_data = Symtab.merge (K true) (rdd1, rdd2) } + relator_distr_data = Symtab.merge (K true) (rdd1, rdd2), + restore_data = Symtab.merge (K true) (rd1, rd2) } ) -fun map_data f1 f2 f3 f4 - { quot_maps, quotients, reflexivity_rules, relator_distr_data} = +fun map_data f1 f2 f3 f4 f5 + { quot_maps, quotients, reflexivity_rules, relator_distr_data, restore_data } = { quot_maps = f1 quot_maps, quotients = f2 quotients, reflexivity_rules = f3 reflexivity_rules, - relator_distr_data = f4 relator_distr_data } + relator_distr_data = f4 relator_distr_data, + restore_data = f5 restore_data } -fun map_quot_maps f = map_data f I I I -fun map_quotients f = map_data I f I I -fun map_reflexivity_rules f = map_data I I f I -fun map_relator_distr_data f = map_data I I I f +fun map_quot_maps f = map_data f I I I I +fun map_quotients f = map_data I f I I I +fun map_reflexivity_rules f = map_data I I f I I +fun map_relator_distr_data f = map_data I I I f I +fun map_restore_data f = map_data I I I I f val get_quot_maps' = #quot_maps o Data.get val get_quotients' = #quotients o Data.get val get_reflexivity_rules' = #reflexivity_rules o Data.get val get_relator_distr_data' = #relator_distr_data o Data.get +val get_restore_data' = #restore_data o Data.get fun get_quot_maps ctxt = get_quot_maps' (Context.Proof ctxt) fun get_quotients ctxt = get_quotients' (Context.Proof ctxt) fun get_relator_distr_data ctxt = get_relator_distr_data' (Context.Proof ctxt) +fun get_restore_data ctxt = get_restore_data' (Context.Proof ctxt) (* info about Quotient map theorems *) @@ -163,6 +182,20 @@ end (* info about quotient types *) + +fun pcr_eq ({pcrel_def = pcrel_def1, pcr_cr_eq = pcr_cr_eq1}, + {pcrel_def = pcrel_def2, pcr_cr_eq = pcr_cr_eq2}) = + Thm.eq_thm (pcrel_def1, pcrel_def2) andalso Thm.eq_thm (pcr_cr_eq1, pcr_cr_eq2) + +fun option_eq _ (NONE,NONE) = true + | option_eq _ (NONE,_) = false + | option_eq _ (_,NONE) = false + | option_eq cmp (SOME x, SOME y) = cmp (x,y); + +fun quotient_eq ({quot_thm = quot_thm1, pcr_info = pcr_info1}, + {quot_thm = quot_thm2, pcr_info = pcr_info2}) = + Thm.eq_thm (quot_thm1, quot_thm2) andalso option_eq pcr_eq (pcr_info1, pcr_info2) + fun transform_pcr_info phi {pcrel_def, pcr_cr_eq} = {pcrel_def = Morphism.thm phi pcrel_def, pcr_cr_eq = Morphism.thm phi pcr_cr_eq} @@ -208,6 +241,22 @@ Attrib.setup @{binding quot_del} (Scan.succeed (Thm.declaration_attribute delete_quotients)) "deletes the Quotient theorem" +(* data for restoring Transfer/Lifting context *) + +fun lookup_restore_data ctxt bundle_name = Symtab.lookup (get_restore_data ctxt) bundle_name + +fun update_restore_data bundle_name restore_data ctxt = + Data.map (map_restore_data (Symtab.update (bundle_name, restore_data))) ctxt + +fun init_restore_data bundle_name qinfo ctxt = + update_restore_data bundle_name { quotient = qinfo, transfer_rules = Thm.full_rules } ctxt + +fun add_transfer_rules_in_restore_data bundle_name transfer_rules ctxt = + case Symtab.lookup (get_restore_data' ctxt) bundle_name of + SOME restore_data => update_restore_data bundle_name { quotient = #quotient restore_data, + transfer_rules = Item_Net.merge ((#transfer_rules restore_data), transfer_rules) } ctxt + | NONE => error ("The restore data " ^ quote bundle_name ^ " is not defined.") + (* theorems that a relator of an invariant is an invariant of the corresponding predicate *) structure Invariant_Commute = Named_Thms @@ -468,4 +517,4 @@ Outer_Syntax.improper_command @{command_spec "print_quotients"} "print quotients" (Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of))) -end; +end diff -r 8b9ea4420f81 -r aeb3cf02c678 src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Mon Sep 16 15:03:23 2013 +0200 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Mon Sep 16 16:48:08 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 diff -r 8b9ea4420f81 -r aeb3cf02c678 src/HOL/Tools/Lifting/lifting_term.ML --- a/src/HOL/Tools/Lifting/lifting_term.ML Mon Sep 16 15:03:23 2013 +0200 +++ b/src/HOL/Tools/Lifting/lifting_term.ML Mon Sep 16 16:48:08 2013 +0200 @@ -523,4 +523,4 @@ Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.fun2_conv parametrize_relation_conv)) thm end -end; +end diff -r 8b9ea4420f81 -r aeb3cf02c678 src/HOL/Tools/Lifting/lifting_util.ML --- a/src/HOL/Tools/Lifting/lifting_util.ML Mon Sep 16 15:03:23 2013 +0200 +++ b/src/HOL/Tools/Lifting/lifting_util.ML Mon Sep 16 16:48:08 2013 +0200 @@ -28,7 +28,7 @@ val relation_types: typ -> typ * typ val mk_HOL_eq: thm -> thm val safe_HOL_meta_eq: thm -> thm -end; +end structure Lifting_Util: LIFTING_UTIL = @@ -110,4 +110,4 @@ fun safe_HOL_meta_eq r = mk_HOL_eq r handle Thm.THM _ => r -end; +end diff -r 8b9ea4420f81 -r aeb3cf02c678 src/HOL/Tools/transfer.ML --- a/src/HOL/Tools/transfer.ML Mon Sep 16 15:03:23 2013 +0200 +++ b/src/HOL/Tools/transfer.ML Mon Sep 16 16:48:08 2013 +0200 @@ -20,6 +20,8 @@ val get_compound_rhs: Proof.context -> (term * thm) Item_Net.T val transfer_add: attribute val transfer_del: attribute + val transfer_raw_add: thm -> Context.generic -> Context.generic + val transfer_raw_del: thm -> Context.generic -> Context.generic val transferred_attribute: thm list -> attribute val untransferred_attribute: thm list -> attribute val transfer_domain_add: attribute @@ -135,8 +137,6 @@ | _ => I) o map_known_frees (Term.add_frees (Thm.concl_of thm))) -fun get_args n = rev o fst o funpow_yield n (swap o dest_comb) - fun del_transfer_thm thm = Data.map (map_transfer_raw (Item_Net.remove thm) o map_compound_lhs @@ -150,6 +150,9 @@ Item_Net.remove (rhs, thm) | _ => I)) +fun transfer_raw_add thm ctxt = add_transfer_thm thm ctxt +fun transfer_raw_del thm ctxt = del_transfer_thm thm ctxt + (** Conversions **) fun bottom_rewr_conv rewrs = Conv.bottom_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context}