disallow pending hyps;
authorwenzelm
Fri Jun 29 15:54:41 2018 +0200 (17 months ago ago)
changeset 68540000a0e062529
parent 68539 6740e3611a86
child 68541 12b4b3bc585d
disallow pending hyps;
disallow pending shyps, with option to override the check;
tuned message;
NEWS
src/Doc/Implementation/Logic.thy
src/Pure/Isar/attrib.ML
src/Pure/global_theory.ML
     1.1 --- a/NEWS	Fri Jun 29 14:19:52 2018 +0200
     1.2 +++ b/NEWS	Fri Jun 29 15:54:41 2018 +0200
     1.3 @@ -19,6 +19,11 @@
     1.4  FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for
     1.5  formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK".
     1.6  
     1.7 +* Global facts need to be closed: no free variables, no hypotheses, no
     1.8 +pending sort hypotheses. Rare INCOMPATIBILITY: sort hypotheses can be
     1.9 +allowed via "declare [[pending_shyps]]" in the global theory context,
    1.10 +but it should be reset to false afterwards.
    1.11 +
    1.12  * Marginal comments need to be written exclusively in the new-style form
    1.13  "\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer
    1.14  supported. INCOMPATIBILITY, use the command-line tool "isabelle
     2.1 --- a/src/Doc/Implementation/Logic.thy	Fri Jun 29 14:19:52 2018 +0200
     2.2 +++ b/src/Doc/Implementation/Logic.thy	Fri Jun 29 15:54:41 2018 +0200
     2.3 @@ -862,9 +862,13 @@
     2.4  class empty =
     2.5    assumes bad: "\<And>(x::'a) y. x \<noteq> y"
     2.6  
     2.7 +declare [[pending_shyps]]
     2.8 +
     2.9  theorem (in empty) false: False
    2.10    using bad by blast
    2.11  
    2.12 +declare [[pending_shyps = false]]
    2.13 +
    2.14  ML_val \<open>@{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])\<close>
    2.15  
    2.16  text \<open>
     3.1 --- a/src/Pure/Isar/attrib.ML	Fri Jun 29 14:19:52 2018 +0200
     3.2 +++ b/src/Pure/Isar/attrib.ML	Fri Jun 29 15:54:41 2018 +0200
     3.3 @@ -591,6 +591,7 @@
     3.4    register_config ML_Options.exception_trace_raw #>
     3.5    register_config ML_Options.exception_debugger_raw #>
     3.6    register_config ML_Options.debugger_raw #>
     3.7 +  register_config Global_Theory.pending_shyps_raw #>
     3.8    register_config Proof_Context.show_abbrevs_raw #>
     3.9    register_config Goal_Display.goals_limit_raw #>
    3.10    register_config Goal_Display.show_main_goal_raw #>
     4.1 --- a/src/Pure/global_theory.ML	Fri Jun 29 14:19:52 2018 +0200
     4.2 +++ b/src/Pure/global_theory.ML	Fri Jun 29 15:54:41 2018 +0200
     4.3 @@ -24,6 +24,8 @@
     4.4    val name_thm: bool -> bool -> string -> thm -> thm
     4.5    val name_thms: bool -> bool -> string -> thm list -> thm list
     4.6    val name_thmss: bool -> string -> (thm list * 'a) list -> (thm list * 'a) list
     4.7 +  val pending_shyps_raw: Config.raw
     4.8 +  val pending_shyps: bool Config.T
     4.9    val add_thms_lazy: string -> (binding * thm list lazy) -> theory -> theory
    4.10    val store_thm: binding * thm -> theory -> thm * theory
    4.11    val store_thm_open: binding * thm -> theory -> thm * theory
    4.12 @@ -128,16 +130,35 @@
    4.13  
    4.14  fun register_proofs thms thy = (thms, Thm.register_proofs (Lazy.value thms) thy);
    4.15  
    4.16 +val pending_shyps_raw = Config.declare ("pending_shyps", \<^here>) (K (Config.Bool false));
    4.17 +val pending_shyps = Config.bool pending_shyps_raw;
    4.18 +
    4.19  fun add_facts (b, fact) thy =
    4.20    let
    4.21      val full_name = Sign.full_name thy b;
    4.22      val pos = Binding.pos_of b;
    4.23 -    fun err msg =
    4.24 -      error ("Malformed global fact " ^ quote full_name ^ Position.here pos ^ "\n" ^ msg);
    4.25 -    fun check thm =
    4.26 -      ignore (Logic.unvarify_global (Term_Subst.zero_var_indexes (Thm.full_prop_of thm)))
    4.27 -        handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;
    4.28 -    val arg = (b, Lazy.map_finished (tap (List.app check)) fact);
    4.29 +    fun check fact =
    4.30 +      fact |> map_index (fn (i, thm) =>
    4.31 +        let
    4.32 +          fun err msg =
    4.33 +            error ("Malformed global fact " ^
    4.34 +              quote (full_name ^
    4.35 +                (if length fact = 1 then "" else "(" ^ string_of_int (i + 1) ^ ")")) ^
    4.36 +              Position.here pos ^ "\n" ^ msg);
    4.37 +          val prop = Thm.plain_prop_of thm
    4.38 +            handle THM _ =>
    4.39 +              thm
    4.40 +              |> not (Config.get_global thy pending_shyps) ?
    4.41 +                  Thm.check_shyps (Proof_Context.init_global thy)
    4.42 +              |> Thm.check_hyps (Context.Theory thy)
    4.43 +              |> Thm.full_prop_of;
    4.44 +        in
    4.45 +          ignore (Logic.unvarify_global (Term_Subst.zero_var_indexes prop))
    4.46 +            handle TYPE (msg, _, _) => err msg
    4.47 +              | TERM (msg, _) => err msg
    4.48 +              | ERROR msg => err msg
    4.49 +        end);
    4.50 +    val arg = (b, Lazy.map_finished (tap check) fact);
    4.51    in
    4.52      thy |> Data.map (Facts.add_static (Context.Theory thy) {strict = true, index = false} arg #> #2)
    4.53    end;