static relevance of proof via syntax keywords;
authorwenzelm
Tue Apr 10 21:31:05 2012 +0200 (2012-04-10 ago)
changeset 47416df8fc0567a3d
parent 47415 c486ac962b89
child 47417 9679bab23f93
static relevance of proof via syntax keywords;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Apr 10 20:42:17 2012 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Apr 10 21:31:05 2012 +0200
     1.3 @@ -464,7 +464,7 @@
     1.4        (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
     1.5  
     1.6  val _ =
     1.7 -  Outer_Syntax.command ("sublocale", Keyword.thy_goal)
     1.8 +  Outer_Syntax.command ("sublocale", Keyword.thy_schematic_goal)
     1.9      "prove sublocale relation between a locale and a locale expression"
    1.10      (Parse.position Parse.xname --| (Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") --
    1.11        parse_interpretation_arguments false
    1.12 @@ -472,7 +472,7 @@
    1.13            Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd I loc expr equations)));
    1.14  
    1.15  val _ =
    1.16 -  Outer_Syntax.command ("interpretation", Keyword.thy_goal)
    1.17 +  Outer_Syntax.command ("interpretation", Keyword.thy_schematic_goal)
    1.18      "prove interpretation of locale expression in theory"
    1.19      (parse_interpretation_arguments true
    1.20        >> (fn (expr, equations) => Toplevel.print o
     2.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue Apr 10 20:42:17 2012 +0200
     2.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Apr 10 21:31:05 2012 +0200
     2.3 @@ -296,7 +296,8 @@
     2.4      val (tr, proper_head) = read head |>> Toplevel.modify_init init;
     2.5      val proof_trs = map read proof |> filter #2 |> map #1;
     2.6    in
     2.7 -    if proper_head andalso proper_proof then [(tr, proof_trs)]
     2.8 +    if proper_head andalso proper_proof andalso
     2.9 +      not (Keyword.is_schematic_goal (Toplevel.name_of tr)) then [(tr, proof_trs)]
    2.10      else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
    2.11    end;
    2.12  
     3.1 --- a/src/Pure/Isar/proof.ML	Tue Apr 10 20:42:17 2012 +0200
     3.2 +++ b/src/Pure/Isar/proof.ML	Tue Apr 10 21:31:05 2012 +0200
     3.3 @@ -112,11 +112,8 @@
     3.4    val show_cmd: Method.text option -> (thm list list -> state -> state) ->
     3.5      (Attrib.binding * (string * string list) list) list -> bool -> state -> state
     3.6    val schematic_goal: state -> bool
     3.7 -  val is_relevant: state -> bool
     3.8 -  val local_future_proof: (state -> ('a * state) Future.future) ->
     3.9 -    state -> 'a Future.future * state
    3.10 -  val global_future_proof: (state -> ('a * Proof.context) Future.future) ->
    3.11 -    state -> 'a Future.future * context
    3.12 +  val local_future_proof: (state -> ('a * state) future) -> state -> 'a future * state
    3.13 +  val global_future_proof: (state -> ('a * Proof.context) future) -> state -> 'a future * context
    3.14    val local_future_terminal_proof: Method.text * Method.text option -> bool -> state -> state
    3.15    val global_future_terminal_proof: Method.text * Method.text option -> bool -> state -> context
    3.16  end;
     4.1 --- a/src/Pure/Isar/toplevel.ML	Tue Apr 10 20:42:17 2012 +0200
     4.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Apr 10 21:31:05 2012 +0200
     4.3 @@ -672,12 +672,7 @@
     4.4  
     4.5  fun proof_result immediate (tr, proof_trs) st =
     4.6    let val st' = command tr st in
     4.7 -    if immediate orelse
     4.8 -      null proof_trs orelse
     4.9 -      Keyword.is_schematic_goal (name_of tr) orelse
    4.10 -      exists (Keyword.is_qed_global o name_of) proof_trs orelse
    4.11 -      not (can proof_of st') orelse
    4.12 -      Proof.is_relevant (proof_of st')
    4.13 +    if immediate orelse null proof_trs orelse not (can proof_of st')
    4.14      then
    4.15        let val (states, st'') = fold_map command_result proof_trs st'
    4.16        in (Future.value ((tr, st') :: (proof_trs ~~ states)), st'') end