simplified after_qed;
authorwenzelm
Tue Nov 08 10:44:40 2005 +0100 (2005-11-08)
changeset 18124a310c78298f9
parent 18123 1bb572e8cee9
child 18125 50e63c68768f
simplified after_qed;
src/Pure/Isar/isar_thy.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/proof.ML
src/Pure/axclass.ML
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Tue Nov 08 10:43:15 2005 +0100
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Tue Nov 08 10:44:40 2005 +0100
     1.3 @@ -102,10 +102,10 @@
     1.4  local
     1.5  
     1.6  fun local_goal opt_chain goal stmt int =
     1.7 -  opt_chain #> goal NONE (K (K Seq.single)) stmt int;
     1.8 +  opt_chain #> goal NONE (K Seq.single) stmt int;
     1.9  
    1.10  fun global_goal goal kind a propp thy =
    1.11 -  goal kind NONE (K (K I)) (SOME "") a [(("", []), [propp])] (ProofContext.init thy);
    1.12 +  goal kind NONE (K I) (SOME "") a [(("", []), [propp])] (ProofContext.init thy);
    1.13  
    1.14  in
    1.15  
     2.1 --- a/src/Pure/Isar/obtain.ML	Tue Nov 08 10:43:15 2005 +0100
     2.2 +++ b/src/Pure/Isar/obtain.ML	Tue Nov 08 10:44:40 2005 +0100
     2.3 @@ -123,7 +123,7 @@
     2.4        Logic.list_rename_params ([AutoBind.thesisN],
     2.5          Term.list_all_free ([thesis_var], Logic.mk_implies (that_prop, thesis)));
     2.6  
     2.7 -    fun after_qed _ _ =
     2.8 +    fun after_qed _ =
     2.9        Proof.local_qed (NONE, false)
    2.10        #> Seq.map (`Proof.the_fact #-> (fn rule =>
    2.11          Proof.fix_i vars
    2.12 @@ -131,7 +131,7 @@
    2.13    in
    2.14      state
    2.15      |> Proof.enter_forward
    2.16 -    |> Proof.have_i NONE (K (K Seq.single)) [(("", []), [(obtain_prop, ([], []))])] int
    2.17 +    |> Proof.have_i NONE (K Seq.single) [(("", []), [(obtain_prop, ([], []))])] int
    2.18      |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
    2.19      |> Proof.fix_i [([thesisN], NONE)]
    2.20      |> Proof.assume_i [((thatN, [ContextRules.intro_query_local NONE]), [(that_prop, ([], []))])]
    2.21 @@ -235,7 +235,7 @@
    2.22        end;
    2.23  
    2.24      val before_qed = SOME (Method.primitive_text (Goal.conclude #> Goal.protect));
    2.25 -    fun after_qed _ [[res]] =
    2.26 +    fun after_qed [[res]] =
    2.27        (check_result res; Proof.end_block #> Seq.map (`Proof.the_fact #-> guess_context));
    2.28    in
    2.29      state
     3.1 --- a/src/Pure/Isar/proof.ML	Tue Nov 08 10:43:15 2005 +0100
     3.2 +++ b/src/Pure/Isar/proof.ML	Tue Nov 08 10:44:40 2005 +0100
     3.3 @@ -88,15 +88,13 @@
     3.4    val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
     3.5      (theory -> 'a -> context attribute) ->
     3.6      (context * 'b list -> context * (term list list * (context -> context))) ->
     3.7 -    string -> Method.text option ->
     3.8 -    (context * thm list -> thm list list -> state -> state Seq.seq) ->
     3.9 +    string -> Method.text option -> (thm list list -> state -> state Seq.seq) ->
    3.10      ((string * 'a list) * 'b) list -> state -> state
    3.11    val local_qed: Method.text option * bool -> state -> state Seq.seq
    3.12    val global_goal: (context -> (string * string) * (string * thm list) list -> unit) ->
    3.13      (theory -> 'a -> theory attribute) ->
    3.14      (context * 'b list -> context * (term list list * (context -> context))) ->
    3.15 -    string -> Method.text option ->
    3.16 -    (context * thm list -> thm list list -> theory -> theory) ->
    3.17 +    string -> Method.text option -> (thm list list -> theory -> theory) ->
    3.18      string option -> string * 'a list -> ((string * 'a list) * 'b) list -> context -> state
    3.19    val global_qed: Method.text option * bool -> state -> theory * context
    3.20    val local_terminal_proof: Method.text * Method.text option -> state -> state Seq.seq
    3.21 @@ -109,29 +107,23 @@
    3.22    val global_immediate_proof: state -> theory * context
    3.23    val global_done_proof: state -> theory * context
    3.24    val global_skip_proof: bool -> state -> theory * context
    3.25 -  val have: Method.text option ->
    3.26 -    (context * thm list -> thm list list -> state -> state Seq.seq) ->
    3.27 +  val have: Method.text option -> (thm list list -> state -> state Seq.seq) ->
    3.28      ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
    3.29      bool -> state -> state
    3.30 -  val have_i: Method.text option ->
    3.31 -    (context * thm list -> thm list list -> state -> state Seq.seq) ->
    3.32 +  val have_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
    3.33      ((string * context attribute list) * (term * (term list * term list)) list) list ->
    3.34      bool -> state -> state
    3.35 -  val show: Method.text option ->
    3.36 -    (context * thm list -> thm list list -> state -> state Seq.seq) ->
    3.37 +  val show: Method.text option -> (thm list list -> state -> state Seq.seq) ->
    3.38      ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
    3.39      bool -> state -> state
    3.40 -  val show_i: Method.text option ->
    3.41 -    (context * thm list -> thm list list -> state -> state Seq.seq) ->
    3.42 +  val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
    3.43      ((string * context attribute list) * (term * (term list * term list)) list) list ->
    3.44      bool -> state -> state
    3.45 -  val theorem: string -> Method.text option ->
    3.46 -    (context * thm list -> thm list list -> theory -> theory) ->
    3.47 +  val theorem: string -> Method.text option -> (thm list list -> theory -> theory) ->
    3.48      string option -> string * Attrib.src list ->
    3.49      ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
    3.50      context -> state
    3.51 -  val theorem_i: string -> Method.text option ->
    3.52 -    (context * thm list -> thm list list -> theory -> theory) ->
    3.53 +  val theorem_i: string -> Method.text option -> (thm list list -> theory -> theory) ->
    3.54      string option -> string * theory attribute list ->
    3.55      ((string * theory attribute list) * (term * (term list * term list)) list) list ->
    3.56      context -> state
    3.57 @@ -164,9 +156,9 @@
    3.58      using: thm list,                        (*goal facts*)
    3.59      goal: thm,                              (*subgoals ==> statement*)
    3.60      before_qed: Method.text option,
    3.61 -    after_qed:   (* FIXME results only *)
    3.62 -      (context * thm list -> thm list list -> state -> state Seq.seq) *
    3.63 -      (context * thm list -> thm list list -> theory -> theory)};
    3.64 +    after_qed:
    3.65 +      (thm list list -> state -> state Seq.seq) *
    3.66 +      (thm list list -> theory -> theory)};
    3.67  
    3.68  exception STATE of string * state;
    3.69  
    3.70 @@ -787,9 +779,8 @@
    3.71      val props = List.concat propss;
    3.72      val goal = Goal.init (Thm.cterm_of thy (Logic.mk_conjunction_list props));
    3.73  
    3.74 -    val after_qed' = after_qed |>> (fn after_local => fn raw_results => fn results =>
    3.75 -      map_context after_ctxt
    3.76 -      #> after_local raw_results results);
    3.77 +    val after_qed' = after_qed |>> (fn after_local =>
    3.78 +      fn results => map_context after_ctxt #> after_local results);
    3.79    in
    3.80      goal_state
    3.81      |> tap (check_tvars props)
    3.82 @@ -813,15 +804,15 @@
    3.83      val outer_ctxt = context_of outer_state;
    3.84  
    3.85      val raw_props = List.concat stmt;
    3.86 -    val raw_results = conclude_goal state raw_props goal;
    3.87      val props = ProofContext.generalize goal_ctxt outer_ctxt raw_props;
    3.88      val results =
    3.89 -      Seq.map_list (ProofContext.exports goal_ctxt outer_ctxt) raw_results
    3.90 +      conclude_goal state raw_props goal
    3.91 +      |> Seq.map_list (ProofContext.exports goal_ctxt outer_ctxt)
    3.92        |> Seq.map (Library.unflat stmt);
    3.93    in
    3.94      outer_state
    3.95      |> map_context (ProofContext.auto_bind_facts props)
    3.96 -    |> pair (after_qed, ((goal_ctxt, raw_results), results))
    3.97 +    |> pair (after_qed, results)
    3.98    end;
    3.99  
   3.100  
   3.101 @@ -831,21 +822,20 @@
   3.102    let
   3.103      val ((names, attss), propp) = prep_names (prep_att (theory_of state)) stmt;
   3.104  
   3.105 -    fun after_qed' raw_results results =
   3.106 +    fun after_qed' results =
   3.107        local_results ((names ~~ attss) ~~ map Thm.simple_fact results)
   3.108        #-> (fn res => tap (fn st => print_results (context_of st) ((kind, ""), res) : unit))
   3.109 -      #> after_qed raw_results results;
   3.110 +      #> after_qed results;
   3.111    in
   3.112      state
   3.113 -    |> generic_goal prepp (kind ^ goal_names NONE "" names) before_qed (after_qed', K (K I)) propp
   3.114 +    |> generic_goal prepp (kind ^ goal_names NONE "" names) before_qed (after_qed', K I) propp
   3.115      |> warn_extra_tfrees state
   3.116    end;
   3.117  
   3.118  fun local_qed txt =
   3.119    end_proof false txt
   3.120    #> Seq.map generic_qed
   3.121 -  #> Seq.maps (uncurry (fn (after_qed, (raw_results, results)) =>
   3.122 -      Seq.lifts (#1 after_qed raw_results) results));
   3.123 +  #> Seq.maps (uncurry (fn ((after_qed, _), results) => Seq.lifts after_qed results));
   3.124  
   3.125  
   3.126  (* global goals *)
   3.127 @@ -867,16 +857,16 @@
   3.128            #2 o global_results kind [((name, atts), List.concat (map #2 res'))]))
   3.129        #> Sign.restore_naming thy;
   3.130  
   3.131 -    fun after_qed' raw_results results =
   3.132 +    fun after_qed' results =
   3.133        (case target of NONE => I
   3.134        | SOME prfx => store_results (NameSpace.base prfx)
   3.135            (map (map (ProofContext.export ctxt thy_ctxt
   3.136              #> Drule.strip_shyps_warning)) results))
   3.137 -      #> after_qed raw_results results;
   3.138 +      #> after_qed results;
   3.139    in
   3.140      init ctxt
   3.141      |> generic_goal (prepp #> ProofContext.auto_fix) (kind ^ goal_names target name names)
   3.142 -      before_qed (K (K Seq.single), after_qed') propp
   3.143 +      before_qed (K Seq.single, after_qed') propp
   3.144    end;
   3.145  
   3.146  fun check_result msg state sq =
   3.147 @@ -887,8 +877,8 @@
   3.148  fun global_qeds txt =
   3.149    end_proof true txt
   3.150    #> Seq.map generic_qed
   3.151 -  #> Seq.maps (fn ((after_qed, (raw_results, results)), state) =>
   3.152 -    Seq.lift (#2 after_qed raw_results) results (theory_of state)
   3.153 +  #> Seq.maps (fn (((_, after_qed), results), state) =>
   3.154 +    Seq.lift after_qed results (theory_of state)
   3.155      |> Seq.map (rpair (context_of state)))
   3.156    |> Seq.DETERM;   (*backtracking may destroy theory!*)
   3.157  
   3.158 @@ -953,9 +943,9 @@
   3.159        |> transform_error
   3.160        |> capture;
   3.161  
   3.162 -    fun after_qed' raw_results results =
   3.163 +    fun after_qed' results =
   3.164        refine_goals print_rule (context_of state) (List.concat results)
   3.165 -      #> Seq.maps (after_qed raw_results results);
   3.166 +      #> Seq.maps (after_qed results);
   3.167    in
   3.168      state
   3.169      |> local_goal print_results prep_att prepp "show" before_qed after_qed' stmt
     4.1 --- a/src/Pure/axclass.ML	Tue Nov 08 10:43:15 2005 +0100
     4.2 +++ b/src/Pure/axclass.ML	Tue Nov 08 10:44:40 2005 +0100
     4.3 @@ -303,7 +303,7 @@
     4.4  
     4.5  fun gen_instance mk_prop add_thms inst thy = thy
     4.6    |> ProofContext.init
     4.7 -  |> Proof.theorem_i Drule.internalK NONE (K (fold add_thms)) NONE ("", [])
     4.8 +  |> Proof.theorem_i Drule.internalK NONE (fold add_thms) NONE ("", [])
     4.9      (map (fn t => (("", []), [(t, ([], []))])) (mk_prop thy inst));
    4.10  
    4.11  in