# HG changeset patch # User wenzelm # Date 1752609906 -7200 # Node ID fa1c57d4269987f193dceaa7a8694ff9eec4ac60 # Parent 3e1521dc095df327e956f30ec23b8bf27ab9430b# Parent d19f589fe9ad46bc27ace846044a69d1df99d9e9 merged diff -r 3e1521dc095d -r fa1c57d42699 NEWS --- a/NEWS Mon Jul 14 18:41:41 2025 +0100 +++ b/NEWS Tue Jul 15 22:05:06 2025 +0200 @@ -16,6 +16,16 @@ state output (if enabled). This affects Isabelle/jEdit panels for Output vs. State in particular. +* Declarations of intro/elim/dest rules for Pure and the Classical +Reasoner (e.g. HOL) are handled more uniformly and efficiently: the +order of rule declarations is maintained accurately, regardless of +intermediate [rule del] declarations. Furthermore, [dest] is now a +proper declaration on its own account, instead of the former expansion +[elim_format, elim]. Consequently, [rule del] no longer deletes the +[elim_format] of the given rule, only the original rule. Rare +INCOMPATIBILITY: tools like "blast" and "auto" may fail in unusual +situations. + * A Prover IDE session, e.g. in Isabelle/jEdit or Isabelle/VSCode, is now able to load markup and messages from the underlying session database. Example: "isabelle jedit -l HOL src/HOL/Nat.thy" for theory diff -r 3e1521dc095d -r fa1c57d42699 src/HOL/Hahn_Banach/Function_Norm.thy --- a/src/HOL/Hahn_Banach/Function_Norm.thy Mon Jul 14 18:41:41 2025 +0100 +++ b/src/HOL/Hahn_Banach/Function_Norm.thy Tue Jul 15 22:05:06 2025 +0200 @@ -151,7 +151,7 @@ then show ?thesis unfolding fn_norm_def by (rule the_lubI_ex) qed -lemma (in normed_vectorspace_with_fn_norm) fn_norm_ub [iff?]: +lemma (in normed_vectorspace_with_fn_norm) fn_norm_ub [intro?]: assumes "continuous V f norm" assumes b: "b \ B V f" shows "b \ \f\\V" diff -r 3e1521dc095d -r fa1c57d42699 src/HOL/Hahn_Banach/Normed_Space.thy --- a/src/HOL/Hahn_Banach/Normed_Space.thy Mon Jul 14 18:41:41 2025 +0100 +++ b/src/HOL/Hahn_Banach/Normed_Space.thy Tue Jul 15 22:05:06 2025 +0200 @@ -19,9 +19,9 @@ locale seminorm = fixes V :: "'a::{minus, plus, zero, uminus} set" fixes norm :: "'a \ real" (\\_\\) - assumes ge_zero [iff?]: "x \ V \ 0 \ \x\" - and abs_homogenous [iff?]: "x \ V \ \a \ x\ = \a\ * \x\" - and subadditive [iff?]: "x \ V \ y \ V \ \x + y\ \ \x\ + \y\" + assumes ge_zero [intro?]: "x \ V \ 0 \ \x\" + and abs_homogenous [intro?]: "x \ V \ \a \ x\ = \a\ * \x\" + and subadditive [intro?]: "x \ V \ y \ V \ \x + y\ \ \x\ + \y\" declare seminorm.intro [intro?] diff -r 3e1521dc095d -r fa1c57d42699 src/Provers/clasimp.ML --- a/src/Provers/clasimp.ML Mon Jul 14 18:41:41 2025 +0100 +++ b/src/Provers/clasimp.ML Tue Jul 15 22:05:06 2025 +0200 @@ -27,7 +27,7 @@ val slow_simp_tac: Proof.context -> int -> tactic val best_simp_tac: Proof.context -> int -> tactic val iff_add: attribute - val iff_add': attribute + val iff_add_pure: attribute val iff_del: attribute val iff_modifiers: Method.modifier parser list val clasimp_modifiers: Method.modifier parser list @@ -43,65 +43,72 @@ (* simp as classical wrapper *) -(* FIXME !? *) -fun clasimp f name tac ctxt = f (ctxt, (name, fn _ => CHANGED o tac ctxt)); - -(*Add a simpset to the claset!*) (*Caution: only one simpset added can be added by each of addSss and addss*) -val addSss = clasimp Classical.addSafter "safe_asm_full_simp_tac" Simplifier.safe_asm_full_simp_tac; -val addss = clasimp Classical.addbefore "asm_full_simp_tac" Simplifier.asm_full_simp_tac; +local + fun add_wrapper f name tac ctxt = f (ctxt, (name, fn _ => CHANGED o tac ctxt)); +in + val addSss = + add_wrapper Classical.addSafter "safe_asm_full_simp_tac" Simplifier.safe_asm_full_simp_tac; + val addss = + add_wrapper Classical.addbefore "asm_full_simp_tac" Simplifier.asm_full_simp_tac; +end; (* iffs: addition of rules to simpsets and clasets simultaneously *) local +val safe_atts = + {intro = Classical.safe_intro NONE, + elim = Classical.safe_elim NONE, + dest = Classical.safe_dest NONE}; + +val unsafe_atts = + {intro = Classical.unsafe_intro NONE, + elim = Classical.unsafe_elim NONE, + dest = Classical.unsafe_dest NONE}; + +val pure_atts = + {intro = Context_Rules.intro_query NONE, + elim = Context_Rules.elim_query NONE, + dest = Context_Rules.dest_query NONE}; + +val del_atts = + {intro = Classical.rule_del, + elim = Classical.rule_del, + dest = Classical.rule_del}; + (*Takes (possibly conditional) theorems of the form A<->B to the Safe Intr rule B==>A and the Safe Destruct rule A==>B. Also ~A goes to the Safe Elim rule A ==> ?R Failing other cases, A is added as a Safe Intr rule*) -fun add_iff safe unsafe = +fun iff_decl safe unsafe = Thm.declaration_attribute (fn th => fn context => let val n = Thm.nprems_of th; - val (elim, intro) = if n = 0 then safe else unsafe; + val {intro, elim, dest} = if n = 0 then safe else unsafe; val zero_rotate = zero_var_indexes o rotate_prems n; val decls = [(intro, zero_rotate (th RS Data.iffD2)), - (elim, Tactic.make_elim (zero_rotate (th RS Data.iffD1)))] + (dest, zero_rotate (th RS Data.iffD1))] handle THM _ => [(elim, zero_rotate (th RS Data.notE))] handle THM _ => [(intro, th)]; in fold (uncurry Thm.attribute_declaration) decls context end); -fun del_iff del = Thm.declaration_attribute (fn th => fn context => - let - val zero_rotate = zero_var_indexes o rotate_prems (Thm.nprems_of th); - val rls = - [zero_rotate (th RS Data.iffD2), Tactic.make_elim (zero_rotate (th RS Data.iffD1))] - handle THM _ => [zero_rotate (th RS Data.notE)] - handle THM _ => [th]; - in fold (Thm.attribute_declaration del) rls context end); - in val iff_add = Thm.declaration_attribute (fn th => - Thm.attribute_declaration (add_iff - (Classical.safe_elim NONE, Classical.safe_intro NONE) - (Classical.unsafe_elim NONE, Classical.unsafe_intro NONE)) th - #> Thm.attribute_declaration Simplifier.simp_add th); + Thm.attribute_declaration (iff_decl safe_atts unsafe_atts) th #> + Thm.attribute_declaration Simplifier.simp_add th); -val iff_add' = - add_iff - (Context_Rules.elim_query NONE, Context_Rules.intro_query NONE) - (Context_Rules.elim_query NONE, Context_Rules.intro_query NONE); +val iff_add_pure = iff_decl pure_atts pure_atts; val iff_del = Thm.declaration_attribute (fn th => - Thm.attribute_declaration (del_iff Classical.rule_del) th #> - Thm.attribute_declaration (del_iff Context_Rules.rule_del) th #> + Thm.attribute_declaration (iff_decl del_atts del_atts) th #> Thm.attribute_declaration Simplifier.simp_del th); end; @@ -183,19 +190,19 @@ (Attrib.setup \<^binding>\iff\ (Scan.lift (Args.del >> K iff_del || - Scan.option Args.add -- Args.query >> K iff_add' || + Scan.option Args.add -- Args.query >> K iff_add_pure || Scan.option Args.add >> K iff_add)) "declaration of Simplifier / Classical rules"); (* method modifiers *) -val iffN = "iff"; +val iff_token = Args.$$$ "iff"; val iff_modifiers = - [Args.$$$ iffN -- Scan.option Args.add -- Args.colon >> K (Method.modifier iff_add \<^here>), - Args.$$$ iffN -- Scan.option Args.add -- Args.query_colon >> K (Method.modifier iff_add' \<^here>), - Args.$$$ iffN -- Args.del -- Args.colon >> K (Method.modifier iff_del \<^here>)]; + [iff_token -- Scan.option Args.add -- Args.colon >> K (Method.modifier iff_add \<^here>), + iff_token -- Scan.option Args.add -- Args.query_colon >> K (Method.modifier iff_add_pure \<^here>), + iff_token -- Args.del -- Args.colon >> K (Method.modifier iff_del \<^here>)]; val clasimp_modifiers = Simplifier.simp_modifiers @ Splitter.split_modifiers @ diff -r 3e1521dc095d -r fa1c57d42699 src/Provers/classical.ML --- a/src/Provers/classical.ML Mon Jul 14 18:41:41 2025 +0100 +++ b/src/Provers/classical.ML Tue Jul 15 22:05:06 2025 +0200 @@ -285,34 +285,33 @@ (* erros and warnings *) -fun err_thm ctxt msg th = error (msg ^ "\n" ^ Thm.string_of_thm ctxt th); +fun err_thm ctxt msg th = error (msg () ^ "\n" ^ Thm.string_of_thm ctxt th); -fun make_elim ctxt th = - if Thm.no_prems th then err_thm ctxt "Ill-formed destruction rule" th - else Tactic.make_elim th; +fun err_thm_illformed ctxt kind th = + err_thm ctxt (fn () => "Ill-formed " ^ Bires.kind_name kind) th; fun init_decl kind opt_weight info : decl = let val weight = the_default (Bires.kind_index kind) opt_weight in {kind = kind, tag = Bires.weight_tag weight, info = info} end; -fun is_declared decls th kind = - exists (fn {kind = kind', ...} => kind = kind') (Bires.get_decls decls th); - fun warn_thm ctxt msg th = if Context_Position.is_really_visible ctxt - then warning (msg () ^ Thm.string_of_thm ctxt th) else (); + then warning (msg () ^ "\n" ^ Thm.string_of_thm ctxt th) else (); -fun warn_kind ctxt decls prefix th kind = - is_declared decls th kind andalso - (warn_thm ctxt (fn () => prefix ^ Bires.kind_description kind ^ "\n") th; true); +fun warn_kind ctxt prefix th kind = + if Context_Position.is_really_visible ctxt then + warn_thm ctxt (fn () => prefix ^ " " ^ Bires.kind_description kind) th + else (); fun warn_other_kinds ctxt decls th = - let val warn = warn_kind ctxt decls "Rule already declared as " th in - warn Bires.intro_bang_kind orelse - warn Bires.elim_bang_kind orelse - warn Bires.intro_kind orelse - warn Bires.elim_kind - end; + if Context_Position.is_really_visible ctxt then + (case Bires.get_decls decls th of + [] => () + | ds => + Bires.kind_domain + |> filter (member (op =) (map #kind ds)) + |> List.app (warn_kind ctxt "Rule already declared as" th)) + else (); (* extend and merge rules *) @@ -346,15 +345,39 @@ fun trim_context_info {rl, dup_rl, plain} : info = {rl = trim_context_rl rl, dup_rl = trim_context_rl dup_rl, plain = Thm.trim_context plain}; -fun extend_rules ctxt kind opt_weight (th, info) cs = +fun ext_info ctxt kind th = + if kind = Bires.intro_bang_kind then + make_info1 (maybe_swapped_rl (flat_rule ctxt th)) th + else if kind = Bires.elim_bang_kind orelse kind = Bires.dest_bang_kind then + let + val _ = Thm.no_prems th andalso err_thm_illformed ctxt kind th; + val elim = Bires.kind_make_elim kind th; + in make_info1 (no_swapped_rl (classical_rule ctxt (flat_rule ctxt elim))) elim end + else if kind = Bires.intro_kind then + let + val th' = flat_rule ctxt th; + val dup_th' = dup_intr th' handle THM _ => err_thm_illformed ctxt kind th; + in make_info (maybe_swapped_rl th') (maybe_swapped_rl dup_th') th end + else if kind = Bires.elim_kind orelse kind = Bires.dest_kind then + let + val _ = Thm.no_prems th andalso err_thm_illformed ctxt kind th; + val elim = Bires.kind_make_elim kind th; + val th' = classical_rule ctxt (flat_rule ctxt elim); + val dup_th' = dup_elim ctxt th' handle THM _ => err_thm_illformed ctxt kind th; + in make_info (no_swapped_rl th') (no_swapped_rl dup_th') elim end + else raise Fail "Bad rule kind"; + +in + +fun extend_rules ctxt kind opt_weight th cs = let val th' = Thm.trim_context th; - val decl' = init_decl kind opt_weight (trim_context_info info); + val decl' = init_decl kind opt_weight (trim_context_info (ext_info ctxt kind th)); val CS {decls, swrappers, uwrappers, safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair} = cs; in (case Bires.extend_decls (th', decl') decls of - (NONE, _) => (warn_kind ctxt decls "Ignoring duplicate " th kind; cs) + (NONE, _) => (warn_kind ctxt "Ignoring duplicate" th kind; cs) | (SOME new_decl, decls') => let val _ = warn_other_kinds ctxt decls th; @@ -374,8 +397,6 @@ end) end; -in - fun merge_cs (cs, cs2) = if pointer_eq (cs, cs2) then cs else @@ -400,48 +421,24 @@ extra_netpair = extra_netpair'} end; -fun addSI w ctxt th cs = - extend_rules ctxt Bires.intro_bang_kind w - (th, make_info1 (maybe_swapped_rl (flat_rule ctxt th)) th) cs; - -fun addSE w ctxt th cs = - if Thm.no_prems th then err_thm ctxt "Ill-formed elimination rule" th - else - let val info = make_info1 (no_swapped_rl (classical_rule ctxt (flat_rule ctxt th))) th - in extend_rules ctxt Bires.elim_bang_kind w (th, info) cs end; - -fun addSD w ctxt th = addSE w ctxt (make_elim ctxt th); - -fun addI w ctxt th cs = - let - val th' = flat_rule ctxt th; - val dup_th' = dup_intr th' handle THM _ => err_thm ctxt "Ill-formed introduction rule" th; - val info = make_info (maybe_swapped_rl th') (maybe_swapped_rl dup_th') th; - in extend_rules ctxt Bires.intro_kind w (th, info) cs end; - -fun addE w ctxt th cs = - let - val _ = Thm.no_prems th andalso err_thm ctxt "Ill-formed elimination rule" th; - val th' = classical_rule ctxt (flat_rule ctxt th); - val dup_th' = dup_elim ctxt th' handle THM _ => err_thm ctxt "Ill-formed elimination rule" th; - val info = make_info (no_swapped_rl th') (no_swapped_rl dup_th') th; - in extend_rules ctxt Bires.elim_kind w (th, info) cs end; - -fun addD w ctxt th = addE w ctxt (make_elim ctxt th); - end; (* delete rules *) -fun delrule ctxt th cs = +fun delrule ctxt warn th cs = let - val ths = th :: the_list (try Tactic.make_elim th); val CS {decls, swrappers, uwrappers, safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair} = cs; - val (old_decls, decls') = fold_map Bires.remove_decls ths decls |>> flat; + val (old_decls, decls') = Bires.remove_decls th decls; + val _ = + if Bires.has_decls decls (Tactic.make_elim th) then + warn_thm ctxt + (fn () => "Not deleting elim format --- need to to declare proper dest rule") th + else (); in - if null old_decls then (warn_thm ctxt (fn () => "Undeclared classical rule\n") th; cs) + if null old_decls then + (if warn then warn_thm ctxt (fn () => "Undeclared classical rule") th else (); cs) else let fun del which ({tag = {index, ...}, info, ...}: decl) = delete_rl index (which info); @@ -497,17 +494,19 @@ fun put_claset cs = map_claset (K cs); -(* old-style declarations *) +(* old-style ML declarations *) -fun decl f (ctxt, ths) = map_claset (fold_rev (f ctxt) ths) ctxt; +fun ml_decl kind (ctxt, ths) = + map_claset (fold_rev (extend_rules ctxt kind NONE) ths) ctxt; -val op addSIs = decl (addSI NONE); -val op addSEs = decl (addSE NONE); -val op addSDs = decl (addSD NONE); -val op addIs = decl (addI NONE); -val op addEs = decl (addE NONE); -val op addDs = decl (addD NONE); -val op delrules = decl delrule; +val op addSIs = ml_decl Bires.intro_bang_kind; +val op addSEs = ml_decl Bires.elim_bang_kind; +val op addSDs = ml_decl Bires.dest_bang_kind; +val op addIs = ml_decl Bires.intro_kind; +val op addEs = ml_decl Bires.elim_kind; +val op addDs = ml_decl Bires.dest_kind; + +fun ctxt delrules ths = map_claset (fold_rev (delrule ctxt true) ths) ctxt; @@ -738,21 +737,21 @@ (* declarations *) -fun attrib f = +fun attrib kind w = Thm.declaration_attribute (fn th => fn context => - map_cs (f (Context.proof_of context) th) context); + map_cs (extend_rules (Context.proof_of context) kind w th) context); -val safe_elim = attrib o addSE; -val safe_intro = attrib o addSI; -val safe_dest = attrib o addSD; -val unsafe_elim = attrib o addE; -val unsafe_intro = attrib o addI; -val unsafe_dest = attrib o addD; +val safe_intro = attrib Bires.intro_bang_kind; +val safe_elim = attrib Bires.elim_bang_kind; +val safe_dest = attrib Bires.dest_bang_kind; +val unsafe_intro = attrib Bires.intro_kind; +val unsafe_elim = attrib Bires.elim_kind; +val unsafe_dest = attrib Bires.dest_kind; val rule_del = Thm.declaration_attribute (fn th => fn context => context - |> map_cs (delrule (Context.proof_of context) th) + |> map_cs (delrule (Context.proof_of context) (not (Context_Rules.declared_rule context th)) th) |> Thm.attribute_declaration Context_Rules.rule_del th); @@ -861,13 +860,10 @@ fun print_claset ctxt = let val {decls, swrappers, uwrappers, ...} = rep_claset_of ctxt; - val prt_rules = - Bires.pretty_decls ctxt - [Bires.intro_bang_kind, Bires.intro_kind, Bires.elim_bang_kind, Bires.elim_kind] decls; val prt_wrappers = [Pretty.strs ("safe wrappers:" :: map #1 swrappers), Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)]; - in Pretty.writeln (Pretty.chunks (prt_rules @ prt_wrappers)) end; + in Pretty.writeln (Pretty.chunks (Bires.pretty_decls ctxt decls @ prt_wrappers)) end; val _ = Outer_Syntax.command \<^command_keyword>\print_claset\ "print context of Classical Reasoner" diff -r 3e1521dc095d -r fa1c57d42699 src/Pure/General/pretty.ML --- a/src/Pure/General/pretty.ML Mon Jul 14 18:41:41 2025 +0100 +++ b/src/Pure/General/pretty.ML Tue Jul 15 22:05:06 2025 +0200 @@ -243,7 +243,7 @@ let val bs = out prt; val bs' = - if Bytes.size bs <= String.maxSize then bs + if Bytes.size bs + 8000 <= String.maxSize then bs else out (from_ML (ML_Pretty.no_markup (to_ML prt))); in Bytes.content bs' end; diff -r 3e1521dc095d -r fa1c57d42699 src/Pure/Isar/context_rules.ML --- a/src/Pure/Isar/context_rules.ML Mon Jul 14 18:41:41 2025 +0100 +++ b/src/Pure/Isar/context_rules.ML Tue Jul 15 22:05:06 2025 +0200 @@ -12,6 +12,7 @@ val netpair: Proof.context -> Bires.netpair val find_rules_netpair: Proof.context -> bool -> thm list -> term -> Bires.netpair -> thm list val find_rules: Proof.context -> bool -> thm list -> term -> thm list list + val declared_rule: Context.generic -> thm -> bool val print_rules: Proof.context -> unit val addSWrapper: (Proof.context -> (int -> tactic) -> int -> tactic) -> theory -> theory val addWrapper: (Proof.context -> (int -> tactic) -> int -> tactic) -> theory -> theory @@ -68,7 +69,8 @@ fun add_rule kind opt_weight th (rules as Rules {decls, netpairs, wrappers}) = let val th' = Thm.trim_context th; - val decl' = init_decl kind opt_weight th'; + val th'' = Thm.trim_context (Bires.kind_make_elim kind th); + val decl' = init_decl kind opt_weight th''; in (case Bires.extend_decls (th', decl') decls of (NONE, _) => rules @@ -77,7 +79,7 @@ in make_rules decls' netpairs' wrappers end) end; -fun del_rule0 th (rules as Rules {decls, netpairs, wrappers}) = +fun del_rule th (rules as Rules {decls, netpairs, wrappers}) = (case Bires.remove_decls th decls of ([], _) => rules | (old_decls, decls') => @@ -87,8 +89,6 @@ old_decls netpairs; in make_rules decls' netpairs' wrappers end); -fun del_rule th = - fold del_rule0 (th :: the_list (try Tactic.make_elim th)); structure Data = Generic_Data ( @@ -111,9 +111,13 @@ in make_rules decls netpairs wrappers end; ); +fun declared_rule context = + let val Rules {decls, ...} = Data.get context + in Bires.has_decls decls end; + fun print_rules ctxt = let val Rules {decls, ...} = Data.get (Context.Proof ctxt) - in Pretty.writeln (Pretty.chunks (Bires.pretty_decls ctxt Bires.kind_domain decls)) end; + in Pretty.writeln (Pretty.chunks (Bires.pretty_decls ctxt decls)) end; (* access data *) @@ -173,21 +177,20 @@ (* add and del rules *) - val rule_del = Thm.declaration_attribute (Data.map o del_rule); -fun rule_add k view opt_w = - Thm.declaration_attribute (fn th => Data.map (add_rule k opt_w (view th) o del_rule th)); +fun rule_add k opt_w = + Thm.declaration_attribute (fn th => Data.map (add_rule k opt_w th o del_rule th)); -val intro_bang = rule_add Bires.intro_bang_kind I; -val elim_bang = rule_add Bires.elim_bang_kind I; -val dest_bang = rule_add Bires.elim_bang_kind Tactic.make_elim; -val intro = rule_add Bires.intro_kind I; -val elim = rule_add Bires.elim_kind I; -val dest = rule_add Bires.elim_kind Tactic.make_elim; -val intro_query = rule_add Bires.intro_query_kind I; -val elim_query = rule_add Bires.elim_query_kind I; -val dest_query = rule_add Bires.elim_query_kind Tactic.make_elim; +val intro_bang = rule_add Bires.intro_bang_kind; +val elim_bang = rule_add Bires.elim_bang_kind; +val dest_bang = rule_add Bires.dest_bang_kind; +val intro = rule_add Bires.intro_kind; +val elim = rule_add Bires.elim_kind; +val dest = rule_add Bires.dest_kind; +val intro_query = rule_add Bires.intro_query_kind; +val elim_query = rule_add Bires.elim_query_kind; +val dest_query = rule_add Bires.dest_query_kind; val _ = Theory.setup (snd o Global_Theory.add_thms [((Binding.empty, Drule.equal_intr_rule), [intro_query NONE])]); diff -r 3e1521dc095d -r fa1c57d42699 src/Pure/bires.ML --- a/src/Pure/bires.ML Mon Jul 14 18:41:41 2025 +0100 +++ b/src/Pure/bires.ML Tue Jul 15 22:05:06 2025 +0200 @@ -23,15 +23,20 @@ eqtype kind val intro_bang_kind: kind val elim_bang_kind: kind + val dest_bang_kind: kind val intro_kind: kind val elim_kind: kind + val dest_kind: kind val intro_query_kind: kind val elim_query_kind: kind + val dest_query_kind: kind val kind_safe: kind -> bool val kind_unsafe: kind -> bool val kind_extra: kind -> bool val kind_index: kind -> int - val kind_elim: kind -> bool + val kind_is_elim: kind -> bool + val kind_make_elim: kind -> thm -> thm + val kind_name: kind -> string val kind_domain: kind list val kind_values: 'a -> 'a list val kind_map: kind -> ('a -> 'a) -> 'a list -> 'a list @@ -46,7 +51,7 @@ val has_decls: 'a decls -> thm -> bool val get_decls: 'a decls -> thm -> 'a decl list val dest_decls: 'a decls -> (thm * 'a decl -> bool) -> (thm * 'a decl) list - val pretty_decls: Proof.context -> kind list -> 'a decls -> Pretty.T list + val pretty_decls: Proof.context -> 'a decls -> Pretty.T list val merge_decls: 'a decls * 'a decls -> 'a decl list * 'a decls val extend_decls: thm * 'a decl -> 'a decls -> 'a decl option * 'a decls val remove_decls: thm -> 'a decls -> 'a decl list * 'a decls @@ -105,30 +110,48 @@ fun next_tag next ({weight, ...}: tag) = {weight = weight, index = next}; -(* kind: intro! / elim! / intro / elim / intro? / elim? *) +(* kind: intro/elim/dest *) + +datatype kind = Kind of {index: int, is_elim: bool, make_elim: bool}; -datatype kind = Kind of int * bool; +fun make_intro_kind i = Kind {index = i, is_elim = false, make_elim = false}; +fun make_elim_kind i = Kind {index = i, is_elim = true, make_elim = false}; +fun make_dest_kind i = Kind {index = i, is_elim = true, make_elim = true}; -val intro_bang_kind = Kind (0, false); -val elim_bang_kind = Kind (0, true); -val intro_kind = Kind (1, false); -val elim_kind = Kind (1, true); -val intro_query_kind = Kind (2, false); -val elim_query_kind = Kind (2, true); +val intro_bang_kind = make_intro_kind 0; +val elim_bang_kind = make_elim_kind 0; +val dest_bang_kind = make_dest_kind 0; + +val intro_kind = make_intro_kind 1; +val elim_kind = make_elim_kind 1; +val dest_kind = make_dest_kind 1; + +val intro_query_kind = make_intro_kind 2; +val elim_query_kind = make_elim_kind 2; +val dest_query_kind = make_dest_kind 2; val kind_infos = [(intro_bang_kind, ("safe introduction", "(intro!)")), (elim_bang_kind, ("safe elimination", "(elim!)")), - (intro_kind, ("introduction", "(intro)")), - (elim_kind, ("elimination", "(elim)")), + (dest_bang_kind, ("safe destruction", "(dest!)")), + (intro_kind, ("unsafe introduction", "(intro)")), + (elim_kind, ("unsafe elimination", "(elim)")), + (dest_kind, ("unsafe destruction", "(dest)")), (intro_query_kind, ("extra introduction", "(intro?)")), - (elim_query_kind, ("extra elimination", "(elim?)"))]; + (elim_query_kind, ("extra elimination", "(elim?)")), + (dest_query_kind, ("extra destruction", "(dest?)"))]; -fun kind_safe (Kind (i, _)) = i = 0; -fun kind_unsafe (Kind (i, _)) = i = 1; -fun kind_extra (Kind (i, _)) = i = 2; -fun kind_index (Kind (i, _)) = i; -fun kind_elim (Kind (_, b)) = b; +fun kind_safe (Kind {index, ...}) = index = 0; +fun kind_unsafe (Kind {index, ...}) = index = 1; +fun kind_extra (Kind {index, ...}) = index = 2; +fun kind_index (Kind {index, ...}) = index; +fun kind_is_elim (Kind {is_elim, ...}) = is_elim; +fun kind_make_elim (Kind {make_elim, ...}) = make_elim ? Tactic.make_elim; + +fun kind_name (Kind {is_elim, make_elim, ...}) = + if is_elim andalso make_elim then "destruction rule" + else if is_elim then "elimination rule" + else "introduction rule"; val kind_domain = map #1 kind_infos; @@ -136,7 +159,7 @@ replicate (length (distinct (op =) (map kind_index kind_domain))) x; fun kind_map kind f = nth_map (kind_index kind) f; -fun kind_rule kind thm : rule = (kind_elim kind, thm); +fun kind_rule kind thm : rule = (kind_is_elim kind, thm); val the_kind_info = the o AList.lookup (op =) kind_infos; @@ -185,11 +208,13 @@ build (rules |> Proptab.fold (fn (th, ds) => ds |> fold (fn d => pred (th, d) ? cons (th, d)))) |> sort (decl_ord o apply2 #2); -fun pretty_decls ctxt kinds decls = - kinds |> map (fn kind => - Pretty.big_list (kind_title kind ^ ":") - (dest_decls decls (fn (_, {kind = kind', ...}) => kind = kind') - |> map (fn (th, _) => Thm.pretty_thm_item ctxt th))); +fun pretty_decls ctxt decls = + kind_domain |> map_filter (fn kind => + (case dest_decls decls (fn (_, {kind = kind', ...}) => kind = kind') of + [] => NONE + | ds => + SOME (Pretty.big_list (kind_title kind ^ ":") + (map (Thm.pretty_thm_item ctxt o #1) ds)))); fun merge_decls (decls1, decls2) = decls1 |> fold_map add_decls (rev (dest_decls decls2 (not o dup_decls decls1)));