# HG changeset patch # User ballarin # Date 1123532044 -7200 # Node ID b4d9b87c102efb4b1d23b22a00bc01d9774bbc5c # Parent f4c1ce91aa3c97aff08cc0f3c54921ee37627f87 After_qed takes result argument. diff -r f4c1ce91aa3c -r b4d9b87c102e src/Pure/Isar/isar_thy.ML --- a/src/Pure/Isar/isar_thy.ML Mon Aug 08 22:11:31 2005 +0200 +++ b/src/Pure/Isar/isar_thy.ML Mon Aug 08 22:14:04 2005 +0200 @@ -58,24 +58,31 @@ -> bool -> theory -> ProofHistory.T val theorem_i: string -> (bstring * theory attribute list) * (term * (term list * term list)) -> bool -> theory -> ProofHistory.T - val multi_theorem: string -> (theory -> theory) -> + val multi_theorem: string -> (thm list * thm list -> theory -> theory) -> (cterm list -> Proof.context -> Proof.context -> thm -> thm) -> bstring * Attrib.src list -> Locale.element Locale.elem_expr list -> ((bstring * Attrib.src list) * (string * (string list * string list)) list) list -> bool -> theory -> ProofHistory.T - val multi_theorem_i: string -> (theory -> theory) -> + val multi_theorem_i: string -> (thm list * thm list -> theory -> theory) -> + (cterm list -> Proof.context -> Proof.context -> thm -> thm) -> + bstring * theory attribute list -> + Locale.element_i Locale.elem_expr list -> + ((bstring * theory attribute list) * (term * (term list * term list)) list) list -> + bool -> theory -> ProofHistory.T + val locale_multi_theorem: + string -> (thm list * thm list -> theory -> theory) -> (cterm list -> Proof.context -> Proof.context -> thm -> thm) -> - bstring * theory attribute list -> Locale.element_i Locale.elem_expr list - -> ((bstring * theory attribute list) * (term * (term list * term list)) list) list - -> bool -> theory -> ProofHistory.T - val locale_multi_theorem: string -> xstring - -> bstring * Attrib.src list -> Locale.element Locale.elem_expr list - -> ((bstring * Attrib.src list) * (string * (string list * string list)) list) list - -> bool -> theory -> ProofHistory.T - val locale_multi_theorem_i: string -> string -> bstring * Attrib.src list - -> Locale.element_i Locale.elem_expr list - -> ((bstring * Attrib.src list) * (term * (term list * term list)) list) list - -> bool -> theory -> ProofHistory.T + xstring -> + bstring * Attrib.src list -> Locale.element Locale.elem_expr list -> + ((bstring * Attrib.src list) * (string * (string list * string list)) list) list -> + bool -> theory -> ProofHistory.T + val locale_multi_theorem_i: + string -> (thm list * thm list -> theory -> theory) -> + (cterm list -> Proof.context -> Proof.context -> thm -> thm) -> + string -> + bstring * Attrib.src list -> Locale.element_i Locale.elem_expr list -> + ((bstring * Attrib.src list) * (term * (term list * term list)) list) list -> + bool -> theory -> ProofHistory.T val smart_multi_theorem: string -> xstring option -> bstring * Attrib.src list -> Locale.element Locale.elem_expr list -> ((bstring * Attrib.src list) * (string * (string list * string list)) list) list @@ -386,8 +393,8 @@ fun multi_theorem_i k after_qed export a = global_statement_i o Proof.multi_theorem_i k after_qed export NONE a; -fun locale_multi_theorem k locale (name, atts) elems concl int thy = - global_statement (Proof.multi_theorem k I ProofContext.export_standard +fun locale_multi_theorem k after_qed export locale (name, atts) elems concl int thy = + global_statement (Proof.multi_theorem k after_qed export (SOME (locale, (map (Attrib.intern_src thy) atts, map (map (Attrib.intern_src thy) o snd o fst) concl))) @@ -395,34 +402,34 @@ (map (Locale.intern_attrib_elem_expr thy) elems)) (map (apfst (apsnd (K []))) concl) int thy; -fun locale_multi_theorem_i k locale (name, atts) elems concl = - global_statement_i (Proof.multi_theorem_i k I ProofContext.export_standard +fun locale_multi_theorem_i k after_qed export locale (name, atts) elems concl = + global_statement_i (Proof.multi_theorem_i k after_qed export (SOME (locale, (atts, map (snd o fst) concl))) (name, []) elems) (map (apfst (apsnd (K []))) concl); fun theorem k (a, t) = - multi_theorem k I ProofContext.export_standard a [] [(("", []), [t])]; + multi_theorem k (K I) ProofContext.export_standard a [] [(("", []), [t])]; fun theorem_i k (a, t) = - multi_theorem_i k I ProofContext.export_standard a [] [(("", []), [t])]; + multi_theorem_i k (K I) ProofContext.export_standard a [] [(("", []), [t])]; fun smart_multi_theorem k NONE a elems = - multi_theorem k I ProofContext.export_standard a elems + multi_theorem k (K I) ProofContext.export_standard a elems | smart_multi_theorem k (SOME locale) a elems = - locale_multi_theorem k locale a elems; + locale_multi_theorem k (K I) ProofContext.export_standard locale a elems; val assume = local_statement Proof.assume I; val assume_i = local_statement_i Proof.assume_i I; val presume = local_statement Proof.presume I; val presume_i = local_statement_i Proof.presume_i I; -val have = local_statement (Proof.have Seq.single true) I; -val have_i = local_statement_i (Proof.have_i Seq.single true) I; -val hence = local_statement (Proof.have Seq.single true) Proof.chain; -val hence_i = local_statement_i (Proof.have_i Seq.single true) Proof.chain; -val show = local_statement' (Proof.show check_goal Seq.single true) I; -val show_i = local_statement_i' (Proof.show_i check_goal Seq.single true) I; -val thus = local_statement' (Proof.show check_goal Seq.single true) Proof.chain; -val thus_i = local_statement_i' (Proof.show_i check_goal Seq.single true) Proof.chain; +val have = local_statement (Proof.have (K Seq.single) true) I; +val have_i = local_statement_i (Proof.have_i (K Seq.single) true) I; +val hence = local_statement (Proof.have (K Seq.single) true) Proof.chain; +val hence_i = local_statement_i (Proof.have_i (K Seq.single) true) Proof.chain; +val show = local_statement' (Proof.show check_goal (K Seq.single) true) I; +val show_i = local_statement_i' (Proof.show_i check_goal (K Seq.single) true) I; +val thus = local_statement' (Proof.show check_goal (K Seq.single) true) Proof.chain; +val thus_i = local_statement_i' (Proof.show_i check_goal (K Seq.single) true) Proof.chain; fun gen_def f ((name, srcs), def) = ProofHistory.apply (fn state => f name (map (Attrib.local_attribute (Proof.theory_of state)) srcs) def state); @@ -641,59 +648,42 @@ fun register_globally (((prfx, atts), expr), insts) int thy = let - val (thy', propss, activate) = + val (propss, after_qed) = Locale.prep_global_registration (prfx, atts) expr insts thy; - fun witness id (thy, thm) = let - val thm' = Drule.freeze_all thm; - in - (Locale.add_global_witness id thm' thy, thm') - end; in - multi_theorem_i Drule.internalK activate ProofContext.export_plain + multi_theorem_i Drule.internalK (fst #> after_qed) ProofContext.export_plain ("", []) [] - (map (fn ((n, ps), props) => - ((NameSpace.base n, [witness (n, map Logic.varify ps)]), - map (fn prop => (prop, ([], []))) props)) propss) int thy' - end; - -fun register_in_locale (target, expr) int thy = - let - val target = Locale.intern thy target; - val (target_expr, thy', propss, activate) = - Locale.prep_registration_in_locale target expr thy; - fun witness id (thy, thm) = let - (* push outer quantifiers inside implications *) - val {prop, sign, ...} = rep_thm thm; - val frees = map (cterm_of sign o Free) (strip_all_vars prop); - (* are hopefully distinct *) - val prems = Logic.strip_imp_prems (strip_all_body prop); - val cprems = map (cterm_of sign) prems; - val thm' = thm |> forall_elim_list frees - |> (fn th => implies_elim_list th (map Thm.assume cprems)) - |> forall_intr_list frees; - in (Locale.add_witness_in_locale target id thm' thy, thm') end; - in - multi_theorem_i Drule.internalK activate ProofContext.export_plain - ("",[]) [Locale.Expr target_expr] - (map (fn (id as (n, _), props) => ((NameSpace.base n, [witness id]), - map (fn prop => (prop, ([], []))) props)) propss) int thy' + (map (fn ((n, _), props) => ((NameSpace.base n, []), + map (fn prop => (prop, ([], []))) props)) propss) int thy end; fun register_locally (((prfx, atts), expr), insts) = ProofHistory.apply (fn state => let val ctxt = Proof.context_of state; - val (ctxt', propss, activate) = + val (propss, after_qed) = Locale.prep_local_registration (prfx, atts) expr insts ctxt; - fun witness id (ctxt, thm) = (Locale.add_local_witness id thm ctxt, thm); in state - |> Proof.map_context (fn _ => ctxt') - |> Proof.have_i (Seq.single o Proof.map_context activate) true - (map (fn (id as (n, _), props) => ((NameSpace.base n, [witness id]), + |> Proof.map_context (fn _ => ctxt) + |> Proof.have_i (fn result => Seq.single o Proof.map_context (after_qed result)) true + (map (fn ((n, _), props) => ((NameSpace.base n, []), map (fn prop => (prop, ([], []))) props)) propss) end); +fun register_in_locale (target, expr) int thy = + let + val target = Locale.intern thy target; + val (propss, after_qed) = + Locale.prep_registration_in_locale target expr thy; + in + locale_multi_theorem_i Drule.internalK (fst #> after_qed) + ProofContext.export_plain + target ("",[]) [] + (map (fn ((n, _), props) => ((NameSpace.base n, []), + map (fn prop => (prop, ([], []))) props)) propss) int thy + end; + (* theory init and exit *) diff -r f4c1ce91aa3c -r b4d9b87c102e src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Mon Aug 08 22:11:31 2005 +0200 +++ b/src/Pure/Isar/obtain.ML Mon Aug 08 22:14:04 2005 +0200 @@ -106,7 +106,7 @@ Logic.list_rename_params ([AutoBind.thesisN], Term.list_all_free ([bound_thesis_var], Logic.mk_implies (that_prop, bound_thesis))); - fun after_qed st = st + fun after_qed _ st = st |> Method.local_qed false NONE print |> Seq.map (fn st' => st' |> Proof.fix_i vars @@ -114,7 +114,7 @@ in state |> Proof.enter_forward - |> Proof.have_i Seq.single true [(("", []), [(obtain_prop, ([], []))])] + |> Proof.have_i (K Seq.single) true [(("", []), [(obtain_prop, ([], []))])] |> Method.proof (SOME (Method.Basic (K Method.succeed))) |> Seq.hd |> Proof.fix_i [([thesisN], NONE)] |> Proof.assume_i [((thatN, [ContextRules.intro_query_local NONE]), [(that_prop, ([], []))])] diff -r f4c1ce91aa3c -r b4d9b87c102e src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Mon Aug 08 22:11:31 2005 +0200 +++ b/src/Pure/Isar/proof.ML Mon Aug 08 22:14:04 2005 +0200 @@ -85,13 +85,13 @@ val def: string -> context attribute list -> string * (string * string list) -> state -> state val def_i: string -> context attribute list -> string * (term * term list) -> state -> state val invoke_case: string * string option list * context attribute list -> state -> state - val multi_theorem: string -> (theory -> theory) -> + val multi_theorem: string -> (thm list * thm list -> theory -> theory) -> (cterm list -> context -> context -> thm -> thm) -> (xstring * (Attrib.src list * Attrib.src list list)) option -> bstring * theory attribute list -> Locale.element Locale.elem_expr list -> ((bstring * theory attribute list) * (string * (string list * string list)) list) list -> theory -> state - val multi_theorem_i: string -> (theory -> theory) -> + val multi_theorem_i: string -> (thm list * thm list -> theory -> theory) -> (cterm list -> context -> context -> thm -> thm) -> (string * (Attrib.src list * Attrib.src list list)) option -> bstring * theory attribute list @@ -100,16 +100,16 @@ -> theory -> state val chain: state -> state val from_facts: thm list -> state -> state - val show: (bool -> state -> state) -> (state -> state Seq.seq) -> bool + val show: (bool -> state -> state) -> (thm list -> state -> state Seq.seq) -> bool -> ((string * context attribute list) * (string * (string list * string list)) list) list -> bool -> state -> state - val show_i: (bool -> state -> state) -> (state -> state Seq.seq) -> bool + val show_i: (bool -> state -> state) -> (thm list -> state -> state Seq.seq) -> bool -> ((string * context attribute list) * (term * (term list * term list)) list) list -> bool -> state -> state - val have: (state -> state Seq.seq) -> bool + val have: (thm list -> state -> state Seq.seq) -> bool -> ((string * context attribute list) * (string * (string list * string list)) list) list -> state -> state - val have_i: (state -> state Seq.seq) -> bool + val have_i: (thm list -> state -> state Seq.seq) -> bool -> ((string * context attribute list) * (term * (term list * term list)) list) list -> state -> state val at_bottom: state -> bool @@ -178,7 +178,9 @@ node * (*current*) node list (*parents wrt. block structure*) and after_qed = - AfterQed of (state -> state Seq.seq) * (theory -> theory); + AfterQed of + (thm list -> state -> state Seq.seq) * + (thm list * thm list -> theory -> theory); fun make_node (context, facts, mode, goal) = Node {context = context, facts = facts, mode = mode, goal = goal}; @@ -708,7 +710,7 @@ val thy' = theory_of state'; val AfterQed (after_local, after_global) = after_qed; - val after_qed' = AfterQed (after_local o map_context gen_binds, after_global); + val after_qed' = AfterQed (fn results => after_local results o map_context gen_binds, after_global); val props = List.concat propss; val cprop = Thm.cterm_of thy' (Logic.mk_conjunction_list props); @@ -753,14 +755,14 @@ locale_spec = (case raw_locale of NONE => NONE | SOME (_, x) => SOME (the opt_name, x)), view = view, export = export}) - (AfterQed (Seq.single, after_global)) + (AfterQed (K Seq.single, after_global)) true (map (fst o fst) concl) propp end; fun local_goal' prepp kind (check: bool -> state -> state) after_local pr args int state = state |> setup_goal open_block prepp (K I) (kind (map (snd o fst) args)) - (AfterQed (after_local, I)) pr (map (fst o fst) args) (map snd args) + (AfterQed (after_local, K I)) pr (map (fst o fst) args) (map snd args) |> warn_extra_tfrees state |> check int; @@ -839,7 +841,7 @@ |> (fn st => Seq.map (fn res => note_thmss_i ((names ~~ attss) ~~ map (single o Thm.no_attributes) res) st) resultq) |> (Seq.flat o Seq.map opt_solve) - |> (Seq.flat o Seq.map after_local) + |> (Seq.flat o Seq.map (after_local results)) end; fun local_qed finalize print state = @@ -886,7 +888,7 @@ |> (fn (thy, res) => (thy, res) |>> (#1 o Locale.smart_note_thmss k locale_name [((name, atts), [(List.concat (map #2 res), [])])])); - in (after_global theory', ((k, name), results')) end; + in (after_global (locale_results, results) theory', ((k, name), results')) end; (*note: clients should inspect first result only, as backtracking may destroy theory*) diff -r f4c1ce91aa3c -r b4d9b87c102e src/Pure/axclass.ML --- a/src/Pure/axclass.ML Mon Aug 08 22:11:31 2005 +0200 +++ b/src/Pure/axclass.ML Mon Aug 08 22:14:04 2005 +0200 @@ -319,7 +319,7 @@ fun inst_proof mk_prop add_thms inst int theory = theory - |> IsarThy.multi_theorem_i Drule.internalK I ProofContext.export_standard + |> IsarThy.multi_theorem_i Drule.internalK (K I) ProofContext.export_standard ("", [fn (thy, th) => (add_thms [th] thy, th)]) [] (map (fn t => (("", []), [(t, ([], []))])) (mk_prop theory inst)) int;