# HG changeset patch # User kuncar # Date 1377693455 -7200 # Node ID ca237b9e4542ad77a6dd2e74fcaf43cbde07f917 # Parent 9ddc3bf9f5dfebc187d350674f6fdf7643902d97 use only one data slot; rename print_quotmaps to print_quot_maps; tuned diff -r 9ddc3bf9f5df -r ca237b9e4542 etc/isar-keywords.el --- a/etc/isar-keywords.el Wed Aug 28 11:15:14 2013 +0200 +++ b/etc/isar-keywords.el Wed Aug 28 14:37:35 2013 +0200 @@ -195,10 +195,10 @@ "print_methods" "print_options" "print_orders" + "print_quot_maps" "print_quotconsts" "print_quotients" "print_quotientsQ3" - "print_quotmaps" "print_quotmapsQ3" "print_rules" "print_simpset" @@ -422,10 +422,10 @@ "print_methods" "print_options" "print_orders" + "print_quot_maps" "print_quotconsts" "print_quotients" "print_quotientsQ3" - "print_quotmaps" "print_quotmapsQ3" "print_rules" "print_simpset" diff -r 9ddc3bf9f5df -r ca237b9e4542 src/Doc/IsarRef/HOL_Specific.thy --- a/src/Doc/IsarRef/HOL_Specific.thy Wed Aug 28 11:15:14 2013 +0200 +++ b/src/Doc/IsarRef/HOL_Specific.thy Wed Aug 28 14:37:35 2013 +0200 @@ -1550,7 +1550,7 @@ \begin{matharray}{rcl} @{command_def (HOL) "setup_lifting"} & : & @{text "local_theory \ local_theory"}\\ @{command_def (HOL) "lift_definition"} & : & @{text "local_theory \ proof(prove)"}\\ - @{command_def (HOL) "print_quotmaps"} & : & @{text "context \"}\\ + @{command_def (HOL) "print_quot_maps"} & : & @{text "context \"}\\ @{command_def (HOL) "print_quotients"} & : & @{text "context \"}\\ @{attribute_def (HOL) "quot_map"} & : & @{text attribute} \\ @{attribute_def (HOL) "invariant_commute"} & : & @{text attribute} \\ @@ -1626,7 +1626,7 @@ Integration with code: For total quotients, @{command (HOL) "lift_definition"} uses @{text f.abs_eq} as a code equation. - \item @{command (HOL) "print_quotmaps"} prints stored quotient map + \item @{command (HOL) "print_quot_maps"} prints stored quotient map theorems. \item @{command (HOL) "print_quotients"} prints stored quotient diff -r 9ddc3bf9f5df -r ca237b9e4542 src/HOL/Lifting.thy --- a/src/HOL/Lifting.thy Wed Aug 28 11:15:14 2013 +0200 +++ b/src/HOL/Lifting.thy Wed Aug 28 14:37:35 2013 +0200 @@ -9,7 +9,7 @@ imports Equiv_Relations Transfer keywords "parametric" and - "print_quotmaps" "print_quotients" :: diag and + "print_quot_maps" "print_quotients" :: diag and "lift_definition" :: thy_goal and "setup_lifting" :: thy_decl begin diff -r 9ddc3bf9f5df -r ca237b9e4542 src/HOL/Tools/Lifting/lifting_info.ML --- a/src/HOL/Tools/Lifting/lifting_info.ML Wed Aug 28 11:15:14 2013 +0200 +++ b/src/HOL/Tools/Lifting/lifting_info.ML Wed Aug 28 14:37:35 2013 +0200 @@ -6,18 +6,15 @@ signature LIFTING_INFO = sig - type quotmaps = {rel_quot_thm: thm} - val lookup_quotmaps: Proof.context -> string -> quotmaps option - val lookup_quotmaps_global: theory -> string -> quotmaps option - val print_quotmaps: Proof.context -> unit - - type pcrel_info = {pcrel_def: thm, pcr_cr_eq: thm} - type quotients = {quot_thm: thm, pcrel_info: pcrel_info option} - val transform_quotients: morphism -> quotients -> quotients - val lookup_quotients: Proof.context -> string -> quotients option - val lookup_quotients_global: theory -> string -> quotients option - val update_quotients: string -> quotients -> Context.generic -> Context.generic - val dest_quotients: Proof.context -> quotients list + 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 transform_quotient: morphism -> quotient -> quotient + val lookup_quotients: Proof.context -> string -> quotient option + val update_quotients: string -> quotient -> Context.generic -> Context.generic val print_quotients: Proof.context -> unit val get_invariant_commute_rules: Proof.context -> thm list @@ -29,7 +26,10 @@ 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 - val lookup_relator_distr_data_global: theory -> string -> relator_distr_data option + + 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 setup: theory -> theory end; @@ -39,23 +39,62 @@ open Lifting_Util -(** data containers **) +(** data container **) + +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, + pos_distr_rules: thm list, neg_distr_rules: thm list} + +structure Data = Generic_Data +( + type T = + { quot_maps : quot_map Symtab.table, + quotients : quotient Symtab.table, + reflexivity_rules : thm Item_Net.T, + relator_distr_data : relator_distr_data Symtab.table + } + val empty = + { quot_maps = Symtab.empty, + quotients = Symtab.empty, + reflexivity_rules = Thm.full_rules, + relator_distr_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 = 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) } +) + +fun map_data f1 f2 f3 f4 + { quot_maps, quotients, reflexivity_rules, relator_distr_data} = + { quot_maps = f1 quot_maps, + quotients = f2 quotients, + reflexivity_rules = f3 reflexivity_rules, + relator_distr_data = f4 relator_distr_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 + +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 + +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) (* info about Quotient map theorems *) -type quotmaps = {rel_quot_thm: thm} -structure Quotmaps = Generic_Data -( - type T = quotmaps Symtab.table - val empty = Symtab.empty - val extend = I - fun merge data = Symtab.merge (K true) data -) - -val lookup_quotmaps = Symtab.lookup o Quotmaps.get o Context.Proof -val lookup_quotmaps_global = Symtab.lookup o Quotmaps.get o Context.Theory - -(* FIXME export proper internal update operation!? *) +val lookup_quot_maps = Symtab.lookup o get_quot_maps fun quot_map_thm_sanity_check rel_quot_thm ctxt = let @@ -102,14 +141,14 @@ val relatorT_name = (fst o dest_Type o fst o dest_funT o fastype_of) abs val minfo = {rel_quot_thm = rel_quot_thm} in - Quotmaps.map (Symtab.update (relatorT_name, minfo)) ctxt + Data.map (map_quot_maps (Symtab.update (relatorT_name, minfo))) ctxt end val quot_map_attribute_setup = Attrib.setup @{binding quot_map} (Scan.succeed (Thm.declaration_attribute add_quot_map)) "declaration of the Quotient map theorem" -fun print_quotmaps ctxt = +fun print_quot_maps ctxt = let fun prt_map (ty_name, {rel_quot_thm}) = Pretty.block (separate (Pretty.brk 2) @@ -118,67 +157,49 @@ Pretty.str "quot. theorem:", Syntax.pretty_term ctxt (prop_of rel_quot_thm)]) in - map prt_map (Symtab.dest (Quotmaps.get (Context.Proof ctxt))) + map prt_map (Symtab.dest (get_quot_maps ctxt)) |> Pretty.big_list "maps for type constructors:" |> Pretty.writeln end (* info about quotient types *) -type pcrel_info = {pcrel_def: thm, pcr_cr_eq: thm} -type quotients = {quot_thm: thm, pcrel_info: pcrel_info option} - -structure Quotients = Generic_Data -( - type T = quotients Symtab.table - val empty = Symtab.empty - val extend = I - fun merge data = Symtab.merge (K true) data -) - -fun transform_pcrel_info phi {pcrel_def, pcr_cr_eq} = +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} -fun transform_quotients phi {quot_thm, pcrel_info} = - {quot_thm = Morphism.thm phi quot_thm, pcrel_info = Option.map (transform_pcrel_info phi) pcrel_info} +fun transform_quotient phi {quot_thm, pcr_info} = + {quot_thm = Morphism.thm phi quot_thm, pcr_info = Option.map (transform_pcr_info phi) pcr_info} -val lookup_quotients = Symtab.lookup o Quotients.get o Context.Proof -val lookup_quotients_global = Symtab.lookup o Quotients.get o Context.Theory +fun lookup_quotients ctxt type_name = Symtab.lookup (get_quotients ctxt) type_name -fun update_quotients str qinfo = Quotients.map (Symtab.update (str, qinfo)) +fun update_quotients type_name qinfo ctxt = + Data.map (map_quotients (Symtab.update (type_name, qinfo))) ctxt 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 opt_stored_quot_thm = Symtab.lookup symtab qty_full_name + val symtab = get_quotients' ctxt + fun compare_data (_, data) = Thm.eq_thm_prop (#quot_thm data, quot_thm) in - case opt_stored_quot_thm of - SOME data => - if Thm.eq_thm_prop (#quot_thm data, quot_thm) then - Quotients.map (Symtab.delete qty_full_name) ctxt - else - ctxt - | NONE => ctxt + if Symtab.member compare_data symtab (qty_full_name, quot_thm) + then Data.map (map_quotients (Symtab.delete qty_full_name)) ctxt + else ctxt end -fun dest_quotients ctxt = (* FIXME slightly expensive way to retrieve data *) - map snd (Symtab.dest (Quotients.get (Context.Proof ctxt))) - fun print_quotients ctxt = let - fun prt_quot (qty_name, {quot_thm, pcrel_info}: quotients) = + fun prt_quot (qty_name, {quot_thm, pcr_info}: quotient) = Pretty.block (separate (Pretty.brk 2) [Pretty.str "type:", Pretty.str qty_name, Pretty.str "quot. thm:", Syntax.pretty_term ctxt (prop_of quot_thm), Pretty.str "pcrel_def thm:", - option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o prop_of o #pcrel_def) pcrel_info, + option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o prop_of o #pcrel_def) pcr_info, Pretty.str "pcr_cr_eq thm:", - option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o prop_of o #pcr_cr_eq) pcrel_info]) + option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o prop_of o #pcr_cr_eq) pcr_info]) in - map prt_quot (Symtab.dest (Quotients.get (Context.Proof ctxt))) + map prt_quot (Symtab.dest (get_quotients ctxt)) |> Pretty.big_list "quotients:" |> Pretty.writeln end @@ -187,6 +208,8 @@ Attrib.setup @{binding quot_del} (Scan.succeed (Thm.declaration_attribute delete_quotients)) "deletes the Quotient theorem" +(* theorems that a relator of an invariant is an invariant of the corresponding predicate *) + structure Invariant_Commute = Named_Thms ( val name = @{binding invariant_commute} @@ -197,16 +220,8 @@ (* info about reflexivity rules *) -structure Reflexivity_Rule = Generic_Data -( - type T = thm Item_Net.T - val empty = Thm.full_rules - val extend = I - val merge = Item_Net.merge -) - -fun get_reflexivity_rules ctxt = ctxt - |> (Item_Net.content o Reflexivity_Rule.get o Context.Proof) +fun get_reflexivity_rules ctxt = Item_Net.content (get_reflexivity_rules' (Context.Proof ctxt)) + (* Conversion to create a reflp' variant of a reflexivity rule *) fun safe_reflp_conv ct = @@ -219,7 +234,7 @@ else_conv Conv.all_conv) ct -fun add_reflexivity_rule_raw thm = Reflexivity_Rule.map (Item_Net.update thm) +fun add_reflexivity_rule_raw thm = Data.map (map_reflexivity_rules (Item_Net.update thm)) val add_reflexivity_rule_raw_attribute = Thm.declaration_attribute add_reflexivity_rule_raw fun add_reflexivity_rule thm = add_reflexivity_rule_raw thm #> @@ -230,40 +245,30 @@ val relfexivity_rule_setup = let val name = @{binding reflexivity_rule} - fun del_thm_raw thm = Reflexivity_Rule.map (Item_Net.remove thm) + fun del_thm_raw thm = Data.map (map_reflexivity_rules (Item_Net.remove thm)) fun del_thm thm = del_thm_raw thm #> del_thm_raw (Conv.fconv_rule prep_reflp_conv thm) val del = Thm.declaration_attribute del_thm val text = "rules that are used to prove that a relation is reflexive" - val content = Item_Net.content o Reflexivity_Rule.get + val content = Item_Net.content o get_reflexivity_rules' in Attrib.setup name (Attrib.add_del add_reflexivity_rule_attribute del) text #> Global_Theory.add_thms_dynamic (name, content) end (* info about relator distributivity theorems *) -type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm, - pos_distr_rules: thm list, neg_distr_rules: thm list} -fun map_relator_distr_data f1 f2 f3 f4 +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, neg_mono_rule = f2 neg_mono_rule, 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_neg_distr_rules f = map_relator_distr_data I I I f - -structure Relator_Distr = Generic_Data -( - type T = relator_distr_data Symtab.table - val empty = Symtab.empty - val extend = I - fun merge data = Symtab.merge (K true) data -); +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_neg_distr_rules f = map_relator_distr_data' I I I f fun introduce_polarities rule = let @@ -315,14 +320,14 @@ val 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 dest_Const o head_of o HOLogic.dest_Trueprop o concl_of) mono_rule - val _ = if Symtab.defined (Relator_Distr.get 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 mono_rule val relator_distr_data = {pos_mono_rule = mono_rule, neg_mono_rule = neg_mono_rule, pos_distr_rules = [], neg_distr_rules = []} in - Relator_Distr.map (Symtab.update (mono_ruleT_name, relator_distr_data)) ctxt + Data.map (map_relator_distr_data (Symtab.update (mono_ruleT_name, relator_distr_data))) ctxt end; local @@ -331,8 +336,9 @@ 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 concl_of) distr_rule in - if Symtab.defined (Relator_Distr.get ctxt) distr_ruleT_name then - Relator_Distr.map (Symtab.map_entry distr_ruleT_name (update_entry distr_rule)) ctxt + 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 @@ -425,14 +431,13 @@ fun get_distr_rules_raw ctxt = Symtab.fold (fn (_, {pos_distr_rules, neg_distr_rules, ...}) => fn rules => pos_distr_rules @ neg_distr_rules @ rules) - (Relator_Distr.get ctxt) [] + (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) - (Relator_Distr.get ctxt) [] + (get_relator_distr_data' ctxt) [] -val lookup_relator_distr_data = Symtab.lookup o Relator_Distr.get o Context.Proof -val lookup_relator_distr_data_global = Symtab.lookup o Relator_Distr.get o Context.Theory +val lookup_relator_distr_data = Symtab.lookup o get_relator_distr_data val relator_distr_attribute_setup = Attrib.setup @{binding relator_mono} (Scan.succeed (Thm.declaration_attribute add_mono_rule)) @@ -456,8 +461,8 @@ (* outer syntax commands *) val _ = - Outer_Syntax.improper_command @{command_spec "print_quotmaps"} "print quotient map functions" - (Scan.succeed (Toplevel.keep (print_quotmaps o Toplevel.context_of))) + Outer_Syntax.improper_command @{command_spec "print_quot_maps"} "print quotient map functions" + (Scan.succeed (Toplevel.keep (print_quot_maps o Toplevel.context_of))) val _ = Outer_Syntax.improper_command @{command_spec "print_quotients"} "print quotients" diff -r 9ddc3bf9f5df -r ca237b9e4542 src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Wed Aug 28 11:15:14 2013 +0200 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Wed Aug 28 14:37:35 2013 +0200 @@ -201,12 +201,12 @@ val (pcr_cr_eq, lthy) = case pcrel_def of SOME pcrel_def => apfst SOME (define_pcr_cr_eq lthy pcrel_def) | NONE => (NONE, lthy) - val pcrel_info = case pcrel_def of + val pcr_info = case pcrel_def of SOME pcrel_def => SOME { pcrel_def = pcrel_def, pcr_cr_eq = the pcr_cr_eq } | NONE => NONE - val quotients = { quot_thm = quot_thm, pcrel_info = pcrel_info } + val quotients = { quot_thm = quot_thm, pcr_info = pcr_info } val qty_full_name = (fst o dest_Type) qtyp - fun quot_info phi = Lifting_Info.transform_quotients phi quotients + fun quot_info phi = Lifting_Info.transform_quotient phi quotients val reflexivity_rule_attr = Attrib.internal (K Lifting_Info.add_reflexivity_rule_attribute) val lthy = case opt_reflp_thm of SOME reflp_thm => lthy @@ -376,7 +376,7 @@ reduced_assm RS thm end in - fun parametrize_domain dom_thm (pcrel_info : Lifting_Info.pcrel_info) ctxt = + fun parametrize_domain dom_thm (pcr_info : Lifting_Info.pcr) ctxt = let fun reduce_first_assm ctxt rules thm = let @@ -386,9 +386,9 @@ reduced_assm RS thm end - val pcr_cr_met_eq = #pcr_cr_eq pcrel_info RS @{thm eq_reflection} + val pcr_cr_met_eq = #pcr_cr_eq pcr_info RS @{thm eq_reflection} val pcr_Domainp_eq = rewrite_first_Domainp_arg (Thm.symmetric pcr_cr_met_eq) dom_thm - val pcrel_def = #pcrel_def pcrel_info + val pcrel_def = #pcrel_def pcr_info val pcr_Domainp_par_left_total = (dom_thm RS @{thm pcr_Domainp_par_left_total}) |> fold_Domainp_pcrel pcrel_def @@ -422,7 +422,7 @@ end fun get_pcrel_info ctxt qty_full_name = - #pcrel_info (the (Lifting_Info.lookup_quotients ctxt qty_full_name)) + #pcr_info (the (Lifting_Info.lookup_quotients ctxt qty_full_name)) fun get_Domainp_thm quot_thm = the (get_first (try(curry op RS quot_thm)) [@{thm invariant_to_Domainp}, @{thm Quotient_to_Domainp}]) diff -r 9ddc3bf9f5df -r ca237b9e4542 src/HOL/Tools/Lifting/lifting_term.ML --- a/src/HOL/Tools/Lifting/lifting_term.ML Wed Aug 28 11:15:14 2013 +0200 +++ b/src/HOL/Tools/Lifting/lifting_term.ML Wed Aug 28 14:37:35 2013 +0200 @@ -75,8 +75,8 @@ end fun get_pcrel_info ctxt s = - case #pcrel_info (get_quot_data ctxt s) of - SOME pcrel_info => pcrel_info + case #pcr_info (get_quot_data ctxt s) of + SOME pcr_info => pcr_info | NONE => raise QUOT_THM_INTERNAL (Pretty.block [Pretty.str ("No parametrized correspondce relation for " ^ quote s), Pretty.brk 1, @@ -100,7 +100,7 @@ let val thy = Proof_Context.theory_of ctxt in - (case Lifting_Info.lookup_quotmaps ctxt s of + (case Lifting_Info.lookup_quot_maps ctxt s of SOME map_data => Thm.transfer thy (#rel_quot_thm map_data) | NONE => raise QUOT_THM_INTERNAL (Pretty.block [Pretty.str ("No relator for the type " ^ quote s),