# HG changeset patch # User wenzelm # Date 1530280481 -7200 # Node ID 000a0e062529b3de3a6c0dff0e0ddce60c847fa9 # Parent 6740e3611a869cebaac5d98d2915ea5122e9c632 disallow pending hyps; disallow pending shyps, with option to override the check; tuned message; diff -r 6740e3611a86 -r 000a0e062529 NEWS --- a/NEWS Fri Jun 29 14:19:52 2018 +0200 +++ b/NEWS Fri Jun 29 15:54:41 2018 +0200 @@ -19,6 +19,11 @@ FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK". +* Global facts need to be closed: no free variables, no hypotheses, no +pending sort hypotheses. Rare INCOMPATIBILITY: sort hypotheses can be +allowed via "declare [[pending_shyps]]" in the global theory context, +but it should be reset to false afterwards. + * Marginal comments need to be written exclusively in the new-style form "\ \text\", old ASCII variants like "-- {* ... *}" are no longer supported. INCOMPATIBILITY, use the command-line tool "isabelle diff -r 6740e3611a86 -r 000a0e062529 src/Doc/Implementation/Logic.thy --- a/src/Doc/Implementation/Logic.thy Fri Jun 29 14:19:52 2018 +0200 +++ b/src/Doc/Implementation/Logic.thy Fri Jun 29 15:54:41 2018 +0200 @@ -862,9 +862,13 @@ class empty = assumes bad: "\(x::'a) y. x \ y" +declare [[pending_shyps]] + theorem (in empty) false: False using bad by blast +declare [[pending_shyps = false]] + ML_val \@{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])\ text \ diff -r 6740e3611a86 -r 000a0e062529 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Fri Jun 29 14:19:52 2018 +0200 +++ b/src/Pure/Isar/attrib.ML Fri Jun 29 15:54:41 2018 +0200 @@ -591,6 +591,7 @@ register_config ML_Options.exception_trace_raw #> register_config ML_Options.exception_debugger_raw #> register_config ML_Options.debugger_raw #> + register_config Global_Theory.pending_shyps_raw #> register_config Proof_Context.show_abbrevs_raw #> register_config Goal_Display.goals_limit_raw #> register_config Goal_Display.show_main_goal_raw #> diff -r 6740e3611a86 -r 000a0e062529 src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Fri Jun 29 14:19:52 2018 +0200 +++ b/src/Pure/global_theory.ML Fri Jun 29 15:54:41 2018 +0200 @@ -24,6 +24,8 @@ val name_thm: bool -> bool -> string -> thm -> thm val name_thms: bool -> bool -> string -> thm list -> thm list val name_thmss: bool -> string -> (thm list * 'a) list -> (thm list * 'a) list + val pending_shyps_raw: Config.raw + val pending_shyps: bool Config.T val add_thms_lazy: string -> (binding * thm list lazy) -> theory -> theory val store_thm: binding * thm -> theory -> thm * theory val store_thm_open: binding * thm -> theory -> thm * theory @@ -128,16 +130,35 @@ fun register_proofs thms thy = (thms, Thm.register_proofs (Lazy.value thms) thy); +val pending_shyps_raw = Config.declare ("pending_shyps", \<^here>) (K (Config.Bool false)); +val pending_shyps = Config.bool pending_shyps_raw; + fun add_facts (b, fact) thy = let val full_name = Sign.full_name thy b; val pos = Binding.pos_of b; - fun err msg = - error ("Malformed global fact " ^ quote full_name ^ Position.here pos ^ "\n" ^ msg); - fun check thm = - ignore (Logic.unvarify_global (Term_Subst.zero_var_indexes (Thm.full_prop_of thm))) - handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg; - val arg = (b, Lazy.map_finished (tap (List.app check)) fact); + fun check fact = + fact |> map_index (fn (i, thm) => + let + fun err msg = + error ("Malformed global fact " ^ + quote (full_name ^ + (if length fact = 1 then "" else "(" ^ string_of_int (i + 1) ^ ")")) ^ + Position.here pos ^ "\n" ^ msg); + val prop = Thm.plain_prop_of thm + handle THM _ => + thm + |> not (Config.get_global thy pending_shyps) ? + Thm.check_shyps (Proof_Context.init_global thy) + |> Thm.check_hyps (Context.Theory thy) + |> Thm.full_prop_of; + in + ignore (Logic.unvarify_global (Term_Subst.zero_var_indexes prop)) + handle TYPE (msg, _, _) => err msg + | TERM (msg, _) => err msg + | ERROR msg => err msg + end); + val arg = (b, Lazy.map_finished (tap check) fact); in thy |> Data.map (Facts.add_static (Context.Theory thy) {strict = true, index = false} arg #> #2) end;