After_qed takes result argument.
authorballarin
Mon Aug 08 22:14:04 2005 +0200 (2005-08-08 ago)
changeset 17034b4d9b87c102e
parent 17033 f4c1ce91aa3c
child 17035 415e897405da
After_qed takes result argument.
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	Mon Aug 08 22:11:31 2005 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Mon Aug 08 22:14:04 2005 +0200
     1.3 @@ -58,24 +58,31 @@
     1.4      -> bool -> theory -> ProofHistory.T
     1.5    val theorem_i: string -> (bstring * theory attribute list) *
     1.6      (term * (term list * term list)) -> bool -> theory -> ProofHistory.T
     1.7 -  val multi_theorem: string -> (theory -> theory) ->
     1.8 +  val multi_theorem: string -> (thm list * thm list -> theory -> theory) ->
     1.9      (cterm list -> Proof.context -> Proof.context -> thm -> thm) ->
    1.10      bstring * Attrib.src list -> Locale.element Locale.elem_expr list ->
    1.11      ((bstring * Attrib.src list) * (string * (string list * string list)) list) list
    1.12      -> bool -> theory -> ProofHistory.T
    1.13 -  val multi_theorem_i: string -> (theory -> theory) ->
    1.14 +  val multi_theorem_i: string -> (thm list * thm list -> theory -> theory) ->
    1.15 +    (cterm list -> Proof.context -> Proof.context -> thm -> thm) ->
    1.16 +    bstring * theory attribute list ->
    1.17 +    Locale.element_i Locale.elem_expr list ->
    1.18 +    ((bstring * theory attribute list) * (term * (term list * term list)) list) list ->
    1.19 +    bool -> theory -> ProofHistory.T
    1.20 +  val locale_multi_theorem:
    1.21 +    string -> (thm list * thm list -> theory -> theory) ->
    1.22      (cterm list -> Proof.context -> Proof.context -> thm -> thm) ->
    1.23 -    bstring * theory attribute list -> Locale.element_i Locale.elem_expr list
    1.24 -    -> ((bstring * theory attribute list) * (term * (term list * term list)) list) list
    1.25 -    -> bool -> theory -> ProofHistory.T
    1.26 -  val locale_multi_theorem: string -> xstring
    1.27 -    -> bstring * Attrib.src list -> Locale.element Locale.elem_expr list
    1.28 -    -> ((bstring * Attrib.src list) * (string * (string list * string list)) list) list
    1.29 -    -> bool -> theory -> ProofHistory.T
    1.30 -  val locale_multi_theorem_i: string -> string -> bstring * Attrib.src list
    1.31 -    -> Locale.element_i Locale.elem_expr list
    1.32 -    -> ((bstring * Attrib.src list) * (term * (term list * term list)) list) list
    1.33 -    -> bool -> theory -> ProofHistory.T
    1.34 +    xstring ->
    1.35 +    bstring * Attrib.src list -> Locale.element Locale.elem_expr list ->
    1.36 +    ((bstring * Attrib.src list) * (string * (string list * string list)) list) list ->
    1.37 +    bool -> theory -> ProofHistory.T
    1.38 +  val locale_multi_theorem_i:
    1.39 +    string -> (thm list * thm list -> theory -> theory) ->
    1.40 +    (cterm list -> Proof.context -> Proof.context -> thm -> thm) ->
    1.41 +    string ->
    1.42 +    bstring * Attrib.src list -> Locale.element_i Locale.elem_expr list ->
    1.43 +    ((bstring * Attrib.src list) * (term * (term list * term list)) list) list ->
    1.44 +    bool -> theory -> ProofHistory.T
    1.45    val smart_multi_theorem: string -> xstring option
    1.46      -> bstring * Attrib.src list -> Locale.element Locale.elem_expr list
    1.47      -> ((bstring * Attrib.src list) * (string * (string list * string list)) list) list
    1.48 @@ -386,8 +393,8 @@
    1.49  fun multi_theorem_i k after_qed export a =
    1.50    global_statement_i o Proof.multi_theorem_i k after_qed export NONE a;
    1.51  
    1.52 -fun locale_multi_theorem k locale (name, atts) elems concl int thy =
    1.53 -  global_statement (Proof.multi_theorem k I  ProofContext.export_standard
    1.54 +fun locale_multi_theorem k after_qed export locale (name, atts) elems concl int thy =
    1.55 +  global_statement (Proof.multi_theorem k after_qed export
    1.56        (SOME (locale,
    1.57          (map (Attrib.intern_src thy) atts,
    1.58           map (map (Attrib.intern_src thy) o snd o fst) concl)))
    1.59 @@ -395,34 +402,34 @@
    1.60        (map (Locale.intern_attrib_elem_expr thy) elems))
    1.61      (map (apfst (apsnd (K []))) concl) int thy;
    1.62  
    1.63 -fun locale_multi_theorem_i k locale (name, atts) elems concl =
    1.64 -  global_statement_i (Proof.multi_theorem_i k I ProofContext.export_standard
    1.65 +fun locale_multi_theorem_i k after_qed export locale (name, atts) elems concl =
    1.66 +  global_statement_i (Proof.multi_theorem_i k after_qed export
    1.67        (SOME (locale, (atts, map (snd o fst) concl)))
    1.68        (name, []) elems) (map (apfst (apsnd (K []))) concl);
    1.69  
    1.70  fun theorem k (a, t) =
    1.71 -  multi_theorem k I ProofContext.export_standard a [] [(("", []), [t])];
    1.72 +  multi_theorem k (K I) ProofContext.export_standard a [] [(("", []), [t])];
    1.73  
    1.74  fun theorem_i k (a, t) =
    1.75 -  multi_theorem_i k I ProofContext.export_standard a [] [(("", []), [t])];
    1.76 +  multi_theorem_i k (K I) ProofContext.export_standard a [] [(("", []), [t])];
    1.77  
    1.78  fun smart_multi_theorem k NONE a elems =
    1.79 -      multi_theorem k I ProofContext.export_standard a elems
    1.80 +      multi_theorem k (K I) ProofContext.export_standard a elems
    1.81    | smart_multi_theorem k (SOME locale) a elems =
    1.82 -      locale_multi_theorem k locale a elems;
    1.83 +      locale_multi_theorem k (K I) ProofContext.export_standard locale a elems;
    1.84  
    1.85  val assume      = local_statement Proof.assume I;
    1.86  val assume_i    = local_statement_i Proof.assume_i I;
    1.87  val presume     = local_statement Proof.presume I;
    1.88  val presume_i   = local_statement_i Proof.presume_i I;
    1.89 -val have        = local_statement (Proof.have Seq.single true) I;
    1.90 -val have_i      = local_statement_i (Proof.have_i Seq.single true) I;
    1.91 -val hence       = local_statement (Proof.have Seq.single true) Proof.chain;
    1.92 -val hence_i     = local_statement_i (Proof.have_i Seq.single true) Proof.chain;
    1.93 -val show        = local_statement' (Proof.show check_goal Seq.single true) I;
    1.94 -val show_i      = local_statement_i' (Proof.show_i check_goal Seq.single true) I;
    1.95 -val thus        = local_statement' (Proof.show check_goal Seq.single true) Proof.chain;
    1.96 -val thus_i      = local_statement_i' (Proof.show_i check_goal Seq.single true) Proof.chain;
    1.97 +val have        = local_statement (Proof.have (K Seq.single) true) I;
    1.98 +val have_i      = local_statement_i (Proof.have_i (K Seq.single) true) I;
    1.99 +val hence       = local_statement (Proof.have (K Seq.single) true) Proof.chain;
   1.100 +val hence_i     = local_statement_i (Proof.have_i (K Seq.single) true) Proof.chain;
   1.101 +val show        = local_statement' (Proof.show check_goal (K Seq.single) true) I;
   1.102 +val show_i      = local_statement_i' (Proof.show_i check_goal (K Seq.single) true) I;
   1.103 +val thus        = local_statement' (Proof.show check_goal (K Seq.single) true) Proof.chain;
   1.104 +val thus_i      = local_statement_i' (Proof.show_i check_goal (K Seq.single) true) Proof.chain;
   1.105  
   1.106  fun gen_def f ((name, srcs), def) = ProofHistory.apply (fn state =>
   1.107    f name (map (Attrib.local_attribute (Proof.theory_of state)) srcs) def state);
   1.108 @@ -641,59 +648,42 @@
   1.109  
   1.110  fun register_globally (((prfx, atts), expr), insts) int thy =
   1.111    let
   1.112 -    val (thy', propss, activate) =
   1.113 +    val (propss, after_qed) =
   1.114        Locale.prep_global_registration (prfx, atts) expr insts thy;
   1.115 -    fun witness id (thy, thm) = let
   1.116 -        val thm' = Drule.freeze_all thm;
   1.117 -      in
   1.118 -        (Locale.add_global_witness id thm' thy, thm')
   1.119 -      end;
   1.120    in
   1.121 -    multi_theorem_i Drule.internalK activate ProofContext.export_plain
   1.122 +    multi_theorem_i Drule.internalK (fst #> after_qed) ProofContext.export_plain
   1.123        ("", []) []
   1.124 -      (map (fn ((n, ps), props) =>
   1.125 -          ((NameSpace.base n, [witness (n, map Logic.varify ps)]),
   1.126 -        map (fn prop => (prop, ([], []))) props)) propss) int thy'
   1.127 -  end;
   1.128 -
   1.129 -fun register_in_locale (target, expr) int thy =
   1.130 -  let
   1.131 -    val target = Locale.intern thy target;
   1.132 -    val (target_expr, thy', propss, activate) =
   1.133 -        Locale.prep_registration_in_locale target expr thy;
   1.134 -    fun witness id (thy, thm) = let
   1.135 -        (* push outer quantifiers inside implications *)
   1.136 -        val {prop, sign, ...} = rep_thm thm;
   1.137 -        val frees = map (cterm_of sign o Free) (strip_all_vars prop);
   1.138 -            (* are hopefully distinct *)
   1.139 -        val prems = Logic.strip_imp_prems (strip_all_body prop);
   1.140 -        val cprems = map (cterm_of sign) prems;
   1.141 -        val thm' = thm |> forall_elim_list frees
   1.142 -                       |> (fn th => implies_elim_list th (map Thm.assume cprems))
   1.143 -                       |> forall_intr_list frees;
   1.144 -      in (Locale.add_witness_in_locale target id thm' thy, thm') end;
   1.145 -  in
   1.146 -    multi_theorem_i Drule.internalK activate ProofContext.export_plain
   1.147 -      ("",[]) [Locale.Expr target_expr]
   1.148 -      (map (fn (id as (n, _), props) => ((NameSpace.base n, [witness id]),
   1.149 -        map (fn prop => (prop, ([], []))) props)) propss) int thy'
   1.150 +      (map (fn ((n, _), props) => ((NameSpace.base n, []),
   1.151 +        map (fn prop => (prop, ([], []))) props)) propss) int thy
   1.152    end;
   1.153  
   1.154  fun register_locally (((prfx, atts), expr), insts) =
   1.155    ProofHistory.apply (fn state =>
   1.156      let
   1.157        val ctxt = Proof.context_of state;
   1.158 -      val (ctxt', propss, activate) =
   1.159 +      val (propss, after_qed) =
   1.160          Locale.prep_local_registration (prfx, atts) expr insts ctxt;
   1.161 -      fun witness id (ctxt, thm) = (Locale.add_local_witness id thm ctxt, thm);
   1.162      in
   1.163        state
   1.164 -      |> Proof.map_context (fn _ => ctxt')
   1.165 -      |> Proof.have_i (Seq.single o Proof.map_context activate) true
   1.166 -        (map (fn (id as (n, _), props) => ((NameSpace.base n, [witness id]),
   1.167 +      |> Proof.map_context (fn _ => ctxt)
   1.168 +      |> Proof.have_i (fn result => Seq.single o Proof.map_context (after_qed result)) true
   1.169 +        (map (fn ((n, _), props) => ((NameSpace.base n, []),
   1.170            map (fn prop => (prop, ([], []))) props)) propss)
   1.171      end);
   1.172  
   1.173 +fun register_in_locale (target, expr) int thy =
   1.174 +  let
   1.175 +    val target = Locale.intern thy target;
   1.176 +    val (propss, after_qed) =
   1.177 +        Locale.prep_registration_in_locale target expr thy;
   1.178 +  in
   1.179 +    locale_multi_theorem_i Drule.internalK (fst #> after_qed)
   1.180 +      ProofContext.export_plain
   1.181 +      target ("",[]) []
   1.182 +      (map (fn ((n, _), props) => ((NameSpace.base n, []),
   1.183 +        map (fn prop => (prop, ([], []))) props)) propss) int thy
   1.184 +  end;
   1.185 +
   1.186  
   1.187  (* theory init and exit *)
   1.188  
     2.1 --- a/src/Pure/Isar/obtain.ML	Mon Aug 08 22:11:31 2005 +0200
     2.2 +++ b/src/Pure/Isar/obtain.ML	Mon Aug 08 22:14:04 2005 +0200
     2.3 @@ -106,7 +106,7 @@
     2.4        Logic.list_rename_params ([AutoBind.thesisN],
     2.5          Term.list_all_free ([bound_thesis_var], Logic.mk_implies (that_prop, bound_thesis)));
     2.6  
     2.7 -    fun after_qed st = st
     2.8 +    fun after_qed _ st = st
     2.9        |> Method.local_qed false NONE print
    2.10        |> Seq.map (fn st' => st'
    2.11          |> Proof.fix_i vars
    2.12 @@ -114,7 +114,7 @@
    2.13    in
    2.14      state
    2.15      |> Proof.enter_forward
    2.16 -    |> Proof.have_i Seq.single true [(("", []), [(obtain_prop, ([], []))])]
    2.17 +    |> Proof.have_i (K Seq.single) true [(("", []), [(obtain_prop, ([], []))])]
    2.18      |> Method.proof (SOME (Method.Basic (K Method.succeed))) |> Seq.hd
    2.19      |> Proof.fix_i [([thesisN], NONE)]
    2.20      |> Proof.assume_i [((thatN, [ContextRules.intro_query_local NONE]), [(that_prop, ([], []))])]
     3.1 --- a/src/Pure/Isar/proof.ML	Mon Aug 08 22:11:31 2005 +0200
     3.2 +++ b/src/Pure/Isar/proof.ML	Mon Aug 08 22:14:04 2005 +0200
     3.3 @@ -85,13 +85,13 @@
     3.4    val def: string -> context attribute list -> string *  (string * string list) -> state -> state
     3.5    val def_i: string -> context attribute list -> string * (term * term list) -> state -> state
     3.6    val invoke_case: string * string option list * context attribute list -> state -> state
     3.7 -  val multi_theorem: string -> (theory -> theory) ->
     3.8 +  val multi_theorem: string -> (thm list * thm list -> theory -> theory) ->
     3.9      (cterm list -> context -> context -> thm -> thm) ->
    3.10      (xstring * (Attrib.src list * Attrib.src list list)) option ->
    3.11      bstring * theory attribute list -> Locale.element Locale.elem_expr list
    3.12      -> ((bstring * theory attribute list) * (string * (string list * string list)) list) list
    3.13      -> theory -> state
    3.14 -  val multi_theorem_i: string -> (theory -> theory) ->
    3.15 +  val multi_theorem_i: string -> (thm list * thm list -> theory -> theory) ->
    3.16      (cterm list -> context -> context -> thm -> thm) ->
    3.17      (string * (Attrib.src list * Attrib.src list list)) option
    3.18      -> bstring * theory attribute list
    3.19 @@ -100,16 +100,16 @@
    3.20      -> theory -> state
    3.21    val chain: state -> state
    3.22    val from_facts: thm list -> state -> state
    3.23 -  val show: (bool -> state -> state) -> (state -> state Seq.seq) -> bool
    3.24 +  val show: (bool -> state -> state) -> (thm list -> state -> state Seq.seq) -> bool
    3.25      -> ((string * context attribute list) * (string * (string list * string list)) list) list
    3.26      -> bool -> state -> state
    3.27 -  val show_i: (bool -> state -> state) -> (state -> state Seq.seq) -> bool
    3.28 +  val show_i: (bool -> state -> state) -> (thm list -> state -> state Seq.seq) -> bool
    3.29      -> ((string * context attribute list) * (term * (term list * term list)) list) list
    3.30      -> bool -> state -> state
    3.31 -  val have: (state -> state Seq.seq) -> bool
    3.32 +  val have: (thm list -> state -> state Seq.seq) -> bool
    3.33      -> ((string * context attribute list) * (string * (string list * string list)) list) list
    3.34      -> state -> state
    3.35 -  val have_i: (state -> state Seq.seq) -> bool
    3.36 +  val have_i: (thm list -> state -> state Seq.seq) -> bool
    3.37      -> ((string * context attribute list) * (term * (term list * term list)) list) list
    3.38      -> state -> state
    3.39    val at_bottom: state -> bool
    3.40 @@ -178,7 +178,9 @@
    3.41      node *              (*current*)
    3.42      node list           (*parents wrt. block structure*)
    3.43  and after_qed =
    3.44 -  AfterQed of (state -> state Seq.seq) * (theory -> theory);
    3.45 +  AfterQed of
    3.46 +   (thm list -> state -> state Seq.seq) *
    3.47 +   (thm list * thm list -> theory -> theory);
    3.48  
    3.49  fun make_node (context, facts, mode, goal) =
    3.50    Node {context = context, facts = facts, mode = mode, goal = goal};
    3.51 @@ -708,7 +710,7 @@
    3.52      val thy' = theory_of state';
    3.53  
    3.54      val AfterQed (after_local, after_global) = after_qed;
    3.55 -    val after_qed' = AfterQed (after_local o map_context gen_binds, after_global);
    3.56 +    val after_qed' = AfterQed (fn results => after_local results o map_context gen_binds, after_global);
    3.57  
    3.58      val props = List.concat propss;
    3.59      val cprop = Thm.cterm_of thy' (Logic.mk_conjunction_list props);
    3.60 @@ -753,14 +755,14 @@
    3.61          locale_spec = (case raw_locale of NONE => NONE | SOME (_, x) => SOME (the opt_name, x)),
    3.62          view = view,
    3.63          export = export})
    3.64 -      (AfterQed (Seq.single, after_global))
    3.65 +      (AfterQed (K Seq.single, after_global))
    3.66        true (map (fst o fst) concl) propp
    3.67    end;
    3.68  
    3.69  fun local_goal' prepp kind (check: bool -> state -> state) after_local pr args int state =
    3.70    state
    3.71    |> setup_goal open_block prepp (K I) (kind (map (snd o fst) args))
    3.72 -    (AfterQed (after_local, I)) pr (map (fst o fst) args) (map snd args)
    3.73 +    (AfterQed (after_local, K I)) pr (map (fst o fst) args) (map snd args)
    3.74    |> warn_extra_tfrees state
    3.75    |> check int;
    3.76  
    3.77 @@ -839,7 +841,7 @@
    3.78      |> (fn st => Seq.map (fn res =>
    3.79        note_thmss_i ((names ~~ attss) ~~ map (single o Thm.no_attributes) res) st) resultq)
    3.80      |> (Seq.flat o Seq.map opt_solve)
    3.81 -    |> (Seq.flat o Seq.map after_local)
    3.82 +    |> (Seq.flat o Seq.map (after_local results))
    3.83    end;
    3.84  
    3.85  fun local_qed finalize print state =
    3.86 @@ -886,7 +888,7 @@
    3.87        |> (fn (thy, res) => (thy, res)
    3.88            |>> (#1 o Locale.smart_note_thmss k locale_name
    3.89              [((name, atts), [(List.concat (map #2 res), [])])]));
    3.90 -  in (after_global theory', ((k, name), results')) end;
    3.91 +  in (after_global (locale_results, results) theory', ((k, name), results')) end;
    3.92  
    3.93  
    3.94  (*note: clients should inspect first result only, as backtracking may destroy theory*)
     4.1 --- a/src/Pure/axclass.ML	Mon Aug 08 22:11:31 2005 +0200
     4.2 +++ b/src/Pure/axclass.ML	Mon Aug 08 22:14:04 2005 +0200
     4.3 @@ -319,7 +319,7 @@
     4.4  
     4.5  fun inst_proof mk_prop add_thms inst int theory =
     4.6    theory
     4.7 -  |> IsarThy.multi_theorem_i Drule.internalK I ProofContext.export_standard
     4.8 +  |> IsarThy.multi_theorem_i Drule.internalK (K I) ProofContext.export_standard
     4.9      ("", [fn (thy, th) => (add_thms [th] thy, th)]) []
    4.10      (map (fn t => (("", []), [(t, ([], []))])) (mk_prop theory inst)) int;
    4.11