# HG changeset patch # User wenzelm # Date 1538303791 -7200 # Node ID 43dade957d59ef8f7c37f05eb3fe5241b1a45e7a # Parent 051127c38be80afbe496da5424a02345b14ad662 tuned whitespace and sections; diff -r 051127c38be8 -r 43dade957d59 src/HOL/Tools/Lifting/lifting_info.ML --- a/src/HOL/Tools/Lifting/lifting_info.ML Sun Sep 30 12:33:42 2018 +0200 +++ b/src/HOL/Tools/Lifting/lifting_info.ML Sun Sep 30 12:36:31 2018 +0200 @@ -9,7 +9,7 @@ type quot_map = {rel_quot_thm: thm} val lookup_quot_maps: Proof.context -> string -> quot_map option val print_quot_maps: Proof.context -> unit - + type pcr = {pcrel_def: thm, pcr_cr_eq: thm} type quotient = {quot_thm: thm, pcr_info: pcr option} val pcr_eq: pcr * pcr -> bool @@ -24,14 +24,14 @@ 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 add_transfer_rules_in_restore_data: string -> thm Item_Net.T -> Context.generic -> Context.generic val get_relator_eq_onp_rules: Proof.context -> thm list - + val get_reflexivity_rules: Proof.context -> thm list val add_reflexivity_rule_attribute: attribute - type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm, + type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm, pos_distr_rules: thm list, neg_distr_rules: thm list} val lookup_relator_distr_data: Proof.context -> string -> relator_distr_data option @@ -50,17 +50,18 @@ open Lifting_Util -(** data container **) + +(* context data *) type quot_map = {rel_quot_thm: thm} type pcr = {pcrel_def: thm, pcr_cr_eq: thm} type quotient = {quot_thm: thm, pcr_info: pcr option} -type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm, +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} fun pcr_eq ({pcrel_def = pcrel_def1, pcr_cr_eq = pcr_cr_eq1}, - {pcrel_def = pcrel_def2, pcr_cr_eq = pcr_cr_eq2}) = + {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 quotient_eq ({quot_thm = quot_thm1, pcr_info = pcr_info1}, @@ -70,12 +71,12 @@ fun join_restore_data key (rd1:restore_data, rd2) = if pointer_eq (rd1, rd2) then raise Symtab.SAME else if not (quotient_eq (#quotient rd1, #quotient rd2)) then raise Symtab.DUP key else - { quotient = #quotient rd1, + { quotient = #quotient rd1, transfer_rules = Item_Net.merge (#transfer_rules rd1, #transfer_rules rd2)} structure Data = Generic_Data ( - type T = + type T = { quot_maps : quot_map Symtab.table, quotients : quotient Symtab.table, reflexivity_rules : thm Item_Net.T, @@ -93,7 +94,7 @@ } val extend = I fun merge - ( { quot_maps = qm1, quotients = q1, reflexivity_rules = rr1, relator_distr_data = rdd1, + ( { quot_maps = qm1, quotients = q1, reflexivity_rules = rr1, relator_distr_data = rdd1, restore_data = rd1, no_code_types = nct1 }, { quot_maps = qm2, quotients = q2, reflexivity_rules = rr2, relator_distr_data = rdd2, restore_data = rd2, no_code_types = nct2 } ) = @@ -122,7 +123,7 @@ fun map_relator_distr_data f = map_data I I I f I I fun map_restore_data f = map_data I I I I f I fun map_no_code_types f = map_data I 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 @@ -136,14 +137,15 @@ fun get_restore_data ctxt = get_restore_data' (Context.Proof ctxt) fun get_no_code_types ctxt = get_no_code_types' (Context.Proof ctxt) + (* info about Quotient map theorems *) val lookup_quot_maps = Symtab.lookup o get_quot_maps fun quot_map_thm_sanity_check rel_quot_thm ctxt = let - fun quot_term_absT ctxt quot_term = - let + fun quot_term_absT ctxt quot_term = + let val (_, abs, _, _) = (dest_Quotient o HOLogic.dest_Trueprop) quot_term handle TERM (_, [t]) => error (Pretty.string_of (Pretty.block [Pretty.str "The Quotient map theorem is not in the right form.", @@ -161,23 +163,23 @@ val rel_quot_thm_prems = Logic.strip_imp_prems rel_quot_thm_prop; val concl_absT = quot_term_absT ctxt' rel_quot_thm_concl val concl_tfrees = Term.add_tfree_namesT (concl_absT) [] - val prems_tfrees = fold (fn typ => fn list => Term.add_tfree_namesT (quot_term_absT ctxt' typ) list) + val prems_tfrees = fold (fn typ => fn list => Term.add_tfree_namesT (quot_term_absT ctxt' typ) list) rel_quot_thm_prems [] val extra_prem_tfrees = case subtract (op =) concl_tfrees prems_tfrees of [] => [] | extras => [Pretty.block ([Pretty.str "Extra type variables in the premises:", - Pretty.brk 1] @ + Pretty.brk 1] @ ((Pretty.commas o map (Pretty.str o quote)) extras) @ [Pretty.str "."])] - val errs = extra_prem_tfrees + val errs = extra_prem_tfrees in - if null errs then () else error (cat_lines (["Sanity check of the quotient map theorem failed:",""] + if null errs then () else error (cat_lines (["Sanity check of the quotient map theorem failed:",""] @ (map Pretty.string_of errs))) end -fun add_quot_map rel_quot_thm ctxt = +fun add_quot_map rel_quot_thm ctxt = let val _ = Context.cases (K ()) (quot_map_thm_sanity_check rel_quot_thm) ctxt val rel_quot_thm_concl = (Logic.strip_imp_concl o Thm.prop_of) rel_quot_thm @@ -186,7 +188,7 @@ val minfo = {rel_quot_thm = rel_quot_thm} in Data.map (map_quot_maps (Symtab.update (relatorT_name, minfo))) ctxt - end + end val _ = Theory.setup @@ -197,9 +199,9 @@ let fun prt_map (ty_name, {rel_quot_thm}) = Pretty.block (separate (Pretty.brk 2) - [Pretty.str "type:", + [Pretty.str "type:", Pretty.str ty_name, - Pretty.str "quot. theorem:", + Pretty.str "quot. theorem:", Syntax.pretty_term ctxt (Thm.prop_of rel_quot_thm)]) in map prt_map (Symtab.dest (get_quot_maps ctxt)) @@ -207,6 +209,7 @@ |> Pretty.writeln end + (* info about quotient types *) fun transform_pcr_info phi {pcrel_def, pcr_cr_eq} = @@ -228,7 +231,7 @@ | NONE => NONE end -fun update_quotients type_name qinfo ctxt = +fun update_quotients type_name qinfo ctxt = Data.map (map_quotients (Symtab.update (type_name, qinfo))) ctxt fun delete_quotients quot_thm ctxt = @@ -245,7 +248,7 @@ let fun prt_quot (qty_name, {quot_thm, pcr_info}: quotient) = Pretty.block (separate (Pretty.brk 2) - [Pretty.str "type:", + [Pretty.str "type:", Pretty.str qty_name, Pretty.str "quot. thm:", Syntax.pretty_term ctxt (Thm.prop_of quot_thm), @@ -268,23 +271,25 @@ fun lookup_restore_data ctxt bundle_name = Symtab.lookup (get_restore_data ctxt) bundle_name -fun update_restore_data bundle_name restore_data ctxt = +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 = +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, + 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 eq_onp is an eq_onp of the corresponding predicate *) fun get_relator_eq_onp_rules ctxt = map safe_mk_meta_eq (rev (Named_Theorems.get ctxt @{named_theorems relator_eq_onp})) + (* info about reflexivity rules *) fun get_reflexivity_rules ctxt = Item_Net.content (get_reflexivity_rules' (Context.Proof ctxt)) @@ -292,18 +297,19 @@ fun add_reflexivity_rule thm = Data.map (map_reflexivity_rules (Item_Net.update thm)) val add_reflexivity_rule_attribute = Thm.declaration_attribute add_reflexivity_rule + (* info about relator distributivity theorems *) fun map_relator_distr_data' f1 f2 f3 f4 {pos_mono_rule, neg_mono_rule, pos_distr_rules, neg_distr_rules} = - {pos_mono_rule = f1 pos_mono_rule, + {pos_mono_rule = f1 pos_mono_rule, neg_mono_rule = f2 neg_mono_rule, - pos_distr_rules = f3 pos_distr_rules, + pos_distr_rules = f3 pos_distr_rules, neg_distr_rules = f4 neg_distr_rules} fun map_pos_mono_rule f = map_relator_distr_data' f I I I fun map_neg_mono_rule f = map_relator_distr_data' I f I I -fun map_pos_distr_rules f = map_relator_distr_data' I I f I +fun map_pos_distr_rules f = map_relator_distr_data' I I f I fun map_neg_distr_rules f = map_relator_distr_data' I I I f fun introduce_polarities rule = @@ -312,40 +318,40 @@ val prems_pairs = map (dest_less_eq o HOLogic.dest_Trueprop) (Thm.prems_of rule) val equal_prems = filter op= prems_pairs val _ = - if null equal_prems then () + if null equal_prems then () else error "The rule contains reflexive assumptions." - val concl_pairs = rule + val concl_pairs = rule |> Thm.concl_of |> HOLogic.dest_Trueprop |> dest_less_eq |> apply2 (snd o strip_comb) |> op ~~ |> filter_out op = - - val _ = if has_duplicates op= concl_pairs + + val _ = if has_duplicates op= concl_pairs then error "The rule contains duplicated variables in the conlusion." else () - fun rewrite_prem prem_pair = + fun rewrite_prem prem_pair = if member op= concl_pairs prem_pair then HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm POS_def})) else if member op= concl_pairs (swap prem_pair) then HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm NEG_def})) else error "The rule contains a non-relevant assumption." - + fun rewrite_prems [] = Conv.all_conv | rewrite_prems (x::xs) = Conv.implies_conv (rewrite_prem x) (rewrite_prems xs) - + val rewrite_prems_conv = rewrite_prems prems_pairs - val rewrite_concl_conv = + val rewrite_concl_conv = Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm POS_def}))) in (Conv.fconv_rule (rewrite_prems_conv then_conv rewrite_concl_conv)) rule end - handle + handle TERM _ => error "The rule has a wrong format." | CTERM _ => error "The rule has a wrong format." -fun negate_mono_rule mono_rule = +fun negate_mono_rule mono_rule = let val rewr_conv = HOLogic.Trueprop_conv (Conv.rewrs_conv [@{thm POS_NEG}, @{thm NEG_POS}]) in @@ -359,69 +365,69 @@ val concl_rhs = (hd o get_args 1 o HOLogic.dest_Trueprop o Thm.concl_of) thm; val rules = Item_Net.retrieve (Transfer.get_relator_eq_item_net ctxt) concl_rhs; in - find_first (fn thm => Pattern.matches (Proof_Context.theory_of ctxt) (concl_rhs, + find_first (fn thm => Pattern.matches (Proof_Context.theory_of ctxt) (concl_rhs, (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.concl_of) thm)) rules end val eq_rule = find_eq_rule mono_rule (Context.proof_of ctxt); - val eq_rule = if is_some eq_rule then the eq_rule else error + val eq_rule = if is_some eq_rule then the eq_rule else error "No corresponding rule that the relator preserves equality was found." in ctxt |> add_reflexivity_rule (Drule.zero_var_indexes (@{thm ord_le_eq_trans} OF [mono_rule, eq_rule])) - |> add_reflexivity_rule + |> add_reflexivity_rule (Drule.zero_var_indexes (@{thm ord_eq_le_trans} OF [sym OF [eq_rule], mono_rule])) end -fun add_mono_rule mono_rule ctxt = +fun add_mono_rule mono_rule ctxt = let val pol_mono_rule = introduce_polarities mono_rule - val mono_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o + val mono_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o dest_Const o head_of o HOLogic.dest_Trueprop o Thm.concl_of) pol_mono_rule - val _ = if Symtab.defined (get_relator_distr_data' ctxt) mono_ruleT_name + val _ = if Symtab.defined (get_relator_distr_data' ctxt) mono_ruleT_name then error ("Monotocity rule for type " ^ quote mono_ruleT_name ^ " is already_defined.") else () val neg_mono_rule = negate_mono_rule pol_mono_rule - val relator_distr_data = {pos_mono_rule = pol_mono_rule, neg_mono_rule = neg_mono_rule, + val relator_distr_data = {pos_mono_rule = pol_mono_rule, neg_mono_rule = neg_mono_rule, pos_distr_rules = [], neg_distr_rules = []} in - ctxt + ctxt |> Data.map (map_relator_distr_data (Symtab.update (mono_ruleT_name, relator_distr_data))) |> add_reflexivity_rules mono_rule end; -local +local fun add_distr_rule update_entry distr_rule ctxt = let - val distr_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o + val distr_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o dest_Const o head_of o HOLogic.dest_Trueprop o Thm.concl_of) distr_rule in - if Symtab.defined (get_relator_distr_data' ctxt) distr_ruleT_name then - Data.map (map_relator_distr_data (Symtab.map_entry distr_ruleT_name (update_entry distr_rule))) + if Symtab.defined (get_relator_distr_data' ctxt) distr_ruleT_name then + Data.map (map_relator_distr_data (Symtab.map_entry distr_ruleT_name (update_entry distr_rule))) ctxt else error "The monoticity rule is not defined." end - fun rewrite_concl_conv thm ctm = + fun rewrite_concl_conv thm ctm = Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric thm))) ctm handle CTERM _ => error "The rule has a wrong format." in - fun add_pos_distr_rule distr_rule ctxt = + fun add_pos_distr_rule distr_rule ctxt = let val distr_rule = Conv.fconv_rule (rewrite_concl_conv @{thm POS_def}) distr_rule - fun update_entry distr_rule data = + fun update_entry distr_rule data = map_pos_distr_rules (cons (@{thm POS_trans} OF [distr_rule, #pos_mono_rule data])) data in add_distr_rule update_entry distr_rule ctxt end handle THM _ => error "Combining of the distr. rule and the monotonicity rule together has failed." - - fun add_neg_distr_rule distr_rule ctxt = + + fun add_neg_distr_rule distr_rule ctxt = let val distr_rule = Conv.fconv_rule (rewrite_concl_conv @{thm NEG_def}) distr_rule - fun update_entry distr_rule data = + fun update_entry distr_rule data = map_neg_distr_rules (cons (@{thm NEG_trans} OF [distr_rule, #neg_mono_rule data])) data in add_distr_rule update_entry distr_rule ctxt @@ -429,15 +435,15 @@ handle THM _ => error "Combining of the distr. rule and the monotonicity rule together has failed." end -local +local val eq_refl2 = sym RS @{thm eq_refl} in fun add_eq_distr_rule distr_rule ctxt = - let + let val pos_distr_rule = @{thm eq_refl} OF [distr_rule] val neg_distr_rule = eq_refl2 OF [distr_rule] in - ctxt + ctxt |> add_pos_distr_rule pos_distr_rule |> add_neg_distr_rule neg_distr_rule end @@ -457,7 +463,7 @@ | Const (@{const_name HOL.eq}, _) $ (lhs as Const (@{const_name relcompp},_) $ _ $ _) $ rhs => (lhs, rhs) | _ => error "The rule has a wrong format.") - + val lhs_vars = Term.add_vars lhs [] val rhs_vars = Term.add_vars rhs [] val assms_vars = fold Term.add_vars assms []; @@ -465,10 +471,10 @@ if has_duplicates op= lhs_vars then error "Left-hand side has variable duplicates" else () val _ = - if subset op= (rhs_vars, lhs_vars) then () + if subset op= (rhs_vars, lhs_vars) then () else error "Extra variables in the right-hand side of the rule" val _ = - if subset op= (assms_vars, lhs_vars) then () + if subset op= (assms_vars, lhs_vars) then () else error "Extra variables in the assumptions of the rule" val rhs_args = (snd o strip_comb) rhs; fun check_comp t = @@ -479,7 +485,7 @@ in () end in - fun add_distr_rule distr_rule ctxt = + fun add_distr_rule distr_rule ctxt = let val _ = sanity_check distr_rule val concl = (perhaps (try HOLogic.dest_Trueprop)) (Thm.concl_of distr_rule) @@ -494,12 +500,12 @@ end end -fun get_distr_rules_raw ctxt = Symtab.fold - (fn (_, {pos_distr_rules, neg_distr_rules, ...}) => fn rules => pos_distr_rules @ neg_distr_rules @ rules) +fun get_distr_rules_raw ctxt = Symtab.fold + (fn (_, {pos_distr_rules, neg_distr_rules, ...}) => fn rules => pos_distr_rules @ neg_distr_rules @ rules) (get_relator_distr_data' ctxt) [] -fun get_mono_rules_raw ctxt = Symtab.fold - (fn (_, {pos_mono_rule, neg_mono_rule, ...}) => fn rules => [pos_mono_rule, neg_mono_rule] @ rules) +fun get_mono_rules_raw ctxt = Symtab.fold + (fn (_, {pos_mono_rule, neg_mono_rule, ...}) => fn rules => [pos_mono_rule, neg_mono_rule] @ rules) (get_relator_distr_data' ctxt) [] val lookup_relator_distr_data = Symtab.lookup o get_relator_distr_data @@ -515,13 +521,15 @@ #> Global_Theory.add_thms_dynamic (@{binding relator_mono_raw}, get_mono_rules_raw)) + (* no_code types *) -fun add_no_code_type type_name ctxt = +fun add_no_code_type type_name ctxt = Data.map (map_no_code_types (Symtab.update (type_name, ()))) ctxt; fun is_no_code_type ctxt type_name = (Symtab.defined o get_no_code_types) ctxt type_name + (* setup fixed eq_onp rules *) val _ = Context.>> @@ -529,12 +537,14 @@ Transfer.prep_transfer_domain_thm @{context}) @{thms composed_equiv_rel_eq_onp composed_equiv_rel_eq_eq_onp}) + (* setup fixed reflexivity rules *) -val _ = Context.>> (fold add_reflexivity_rule +val _ = Context.>> (fold add_reflexivity_rule @{thms order_refl[of "(=)"] eq_onp_le_eq Quotient_composition_le_eq Quotient_composition_ge_eq bi_unique_OO bi_total_OO right_unique_OO right_total_OO left_unique_OO left_total_OO}) + (* outer syntax commands *) val _ =