# HG changeset patch # User wenzelm # Date 1155075153 -7200 # Node ID f34c5dbe74d5a758a2c75e54b0336778f8ff995c # Parent bbff23c3e2caf7ec1d16f7c0391c29d1fc4746ab global goals/qeds: after_qed operates on Proof.context (potentially local_theory); diff -r bbff23c3e2ca -r f34c5dbe74d5 src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Tue Aug 08 18:40:56 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_package.ML Wed Aug 09 00:12:33 2006 +0200 @@ -3,18 +3,18 @@ ID: $Id$ Author: Alexander Krauss, TU Muenchen -A package for general recursive function definitions. +A package for general recursive function definitions. Isar commands. *) -signature FUNDEF_PACKAGE = +signature FUNDEF_PACKAGE = sig val add_fundef : ((bstring * (Attrib.src list * bool)) * string) list list -> bool -> theory -> Proof.state (* Need an _i variant *) val cong_add: attribute val cong_del: attribute - + val setup : theory -> theory val get_congs : theory -> thm list end @@ -27,24 +27,24 @@ fun add_simps label moreatts (MutualPart {f_name, ...}, psimps) spec_part thy = - let + let val psimpss = Library.unflat (map snd spec_part) psimps - val (names, attss) = split_list (map fst spec_part) + val (names, attss) = split_list (map fst spec_part) - val thy = thy |> Theory.add_path f_name - + val thy = thy |> Theory.add_path f_name + val thy = thy |> Theory.add_path label val spsimpss = map (map standard) psimpss (* FIXME *) val add_list = (names ~~ spsimpss) ~~ attss val (_, thy) = PureThy.add_thmss add_list thy val thy = thy |> Theory.parent_path - + val (_, thy) = PureThy.add_thmss [((label, flat spsimpss), Simplifier.simp_add :: moreatts)] thy val thy = thy |> Theory.parent_path in thy end - + @@ -52,24 +52,24 @@ fun fundef_afterqed congs mutual_info name data spec [[result]] thy = let - val fundef_data = FundefMutual.mk_partial_rules_mutual thy mutual_info data result - val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data + val fundef_data = FundefMutual.mk_partial_rules_mutual thy mutual_info data result + val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data val Mutual {parts, ...} = mutual_info - val Prep {names = Names {acc_R=accR, ...}, ...} = data - val dom_abbrev = Logic.mk_equals (Free (name ^ "_dom", fastype_of accR), accR) - val (_, thy) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) thy + val Prep {names = Names {acc_R=accR, ...}, ...} = data + val dom_abbrev = Logic.mk_equals (Free (name ^ "_dom", fastype_of accR), accR) + val (_, thy) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) thy val thy = fold2 (add_simps "psimps" []) (parts ~~ psimps) spec thy val casenames = flat (map (map (fst o fst)) spec) - val thy = thy |> Theory.add_path name - val (_, thy) = PureThy.add_thms [(("cases", cases), [RuleCases.case_names casenames])] thy - val (_, thy) = PureThy.add_thmss [(("domintros", domintros), [])] thy - val (_, thy) = PureThy.add_thms [(("termination", standard termination), [])] thy - val (_,thy) = PureThy.add_thmss [(("pinduct", map standard simple_pinducts), [RuleCases.case_names casenames, InductAttrib.induct_set ""])] thy - val thy = thy |> Theory.parent_path + val thy = thy |> Theory.add_path name + val (_, thy) = PureThy.add_thms [(("cases", cases), [RuleCases.case_names casenames])] thy + val (_, thy) = PureThy.add_thmss [(("domintros", domintros), [])] thy + val (_, thy) = PureThy.add_thms [(("termination", standard termination), [])] thy + val (_,thy) = PureThy.add_thmss [(("pinduct", map standard simple_pinducts), [RuleCases.case_names casenames, InductAttrib.induct_set ""])] thy + val thy = thy |> Theory.parent_path in add_fundef_data name (fundef_data, mutual_info, spec) thy end @@ -78,10 +78,10 @@ let fun prep_eqns neqs = neqs - |> map (apsnd (Sign.read_prop thy)) + |> map (apsnd (Sign.read_prop thy)) |> map (apfst (apsnd (apfst (map (prep_att thy))))) |> FundefSplit.split_some_equations (ProofContext.init thy) - + val spec = map prep_eqns eqns_attss val t_eqnss = map (flat o map snd) spec @@ -90,92 +90,94 @@ val (mutual_info, name, (data, thy)) = FundefMutual.prepare_fundef_mutual congs t_eqnss thy val Prep {goal, goalI, ...} = data in - thy |> ProofContext.init - |> Proof.theorem_i PureThy.internalK NONE (fundef_afterqed congs mutual_info name data spec) NONE ("", []) - [(("", []), [(goal, [])])] - |> Proof.refine (Method.primitive_text (fn _ => goalI)) - |> Seq.hd + thy |> ProofContext.init + |> Proof.theorem_i PureThy.internalK NONE + (ProofContext.theory o fundef_afterqed congs mutual_info name data spec) NONE ("", []) + [(("", []), [(goal, [])])] + |> Proof.refine (Method.primitive_text (fn _ => goalI)) + |> Seq.hd end fun total_termination_afterqed name (Mutual {parts, ...}) thmss thy = let - val totality = hd (hd thmss) + val totality = hd (hd thmss) - val (FundefMResult {psimps, simple_pinducts, ... }, Mutual {parts, ...}, spec) - = the (get_fundef_data name thy) + val (FundefMResult {psimps, simple_pinducts, ... }, Mutual {parts, ...}, spec) + = the (get_fundef_data name thy) - val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals]) + val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals]) - val tsimps = map (map remove_domain_condition) psimps - val tinduct = map remove_domain_condition simple_pinducts + val tsimps = map (map remove_domain_condition) psimps + val tinduct = map remove_domain_condition simple_pinducts val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) (flat tsimps) val allatts = if has_guards then [] else [RecfunCodegen.add NONE] val thy = fold2 (add_simps "simps" allatts) (parts ~~ tsimps) spec thy - val thy = Theory.add_path name thy - - val (_, thy) = PureThy.add_thmss [(("induct", map standard tinduct), [])] thy - val thy = Theory.parent_path thy + val thy = Theory.add_path name thy + + val (_, thy) = PureThy.add_thmss [(("induct", map standard tinduct), [])] thy + val thy = Theory.parent_path thy in - thy + thy end (* fun mk_partial_rules name D_name D domT idomT thmss thy = let - val [subs, dcl] = (hd thmss) + val [subs, dcl] = (hd thmss) - val {f_const, f_curried_const, G_const, R_const, G_elims, completeness, f_simps, names_attrs, subset_induct, ... } - = the (Symtab.lookup (FundefData.get thy) name) + val {f_const, f_curried_const, G_const, R_const, G_elims, completeness, f_simps, names_attrs, subset_induct, ... } + = the (Symtab.lookup (FundefData.get thy) name) - val D_implies_dom = subs COMP (instantiate' [SOME (ctyp_of thy idomT)] - [SOME (cterm_of thy D)] - subsetD) + val D_implies_dom = subs COMP (instantiate' [SOME (ctyp_of thy idomT)] + [SOME (cterm_of thy D)] + subsetD) - val D_simps = map (curry op RS D_implies_dom) f_simps + val D_simps = map (curry op RS D_implies_dom) f_simps - val D_induct = subset_induct - |> cterm_instantiate [(cterm_of thy (Var (("D",0), fastype_of D)) ,cterm_of thy D)] - |> curry op COMP subs - |> curry op COMP (dcl |> forall_intr (cterm_of thy (Var (("z",0), idomT))) - |> forall_intr (cterm_of thy (Var (("x",0), idomT)))) + val D_induct = subset_induct + |> cterm_instantiate [(cterm_of thy (Var (("D",0), fastype_of D)) ,cterm_of thy D)] + |> curry op COMP subs + |> curry op COMP (dcl |> forall_intr (cterm_of thy (Var (("z",0), idomT))) + |> forall_intr (cterm_of thy (Var (("x",0), idomT)))) - val ([tinduct'], thy2) = PureThy.add_thms [((name ^ "_" ^ D_name ^ "_induct", D_induct), [])] thy - val ([tsimps'], thy3) = PureThy.add_thmss [((name ^ "_" ^ D_name ^ "_simps", D_simps), [])] thy2 + val ([tinduct'], thy2) = PureThy.add_thms [((name ^ "_" ^ D_name ^ "_induct", D_induct), [])] thy + val ([tsimps'], thy3) = PureThy.add_thmss [((name ^ "_" ^ D_name ^ "_simps", D_simps), [])] thy2 in - thy3 + thy3 end *) - + -fun fundef_setup_termination_proof name NONE thy = +fun fundef_setup_termination_proof name NONE thy = let - val name = if name = "" then get_last_fundef thy else name - val data = the (get_fundef_data name thy) + val name = if name = "" then get_last_fundef thy else name + val data = the (get_fundef_data name thy) handle Option.Option => raise ERROR ("No such function definition: " ^ name) - val (res as FundefMResult {termination, ...}, mutual, _) = data - val goal = FundefTermination.mk_total_termination_goal data + val (res as FundefMResult {termination, ...}, mutual, _) = data + val goal = FundefTermination.mk_total_termination_goal data in - thy |> ProofContext.init - |> ProofContext.note_thmss_i [(("termination", - [ContextRules.intro_query NONE]), [([standard termination], [])])] |> snd - |> Proof.theorem_i PureThy.internalK NONE (total_termination_afterqed name mutual) NONE ("", []) - [(("", []), [(goal, [])])] - end + thy |> ProofContext.init + |> ProofContext.note_thmss_i [(("termination", + [ContextRules.intro_query NONE]), [([standard termination], [])])] |> snd + |> Proof.theorem_i PureThy.internalK NONE + (ProofContext.theory o total_termination_afterqed name mutual) NONE ("", []) + [(("", []), [(goal, [])])] + end | fundef_setup_termination_proof name (SOME (dom_name, dom)) thy = let - val name = if name = "" then get_last_fundef thy else name - val data = the (get_fundef_data name thy) - val (subs, dcl) = FundefTermination.mk_partial_termination_goal thy data dom + val name = if name = "" then get_last_fundef thy else name + val data = the (get_fundef_data name thy) + val (subs, dcl) = FundefTermination.mk_partial_termination_goal thy data dom in - thy |> ProofContext.init - |> Proof.theorem_i PureThy.internalK NONE (K I) NONE ("", []) - [(("", []), [(subs, []), (dcl, [])])] - end + thy |> ProofContext.init + |> Proof.theorem_i PureThy.internalK NONE (K I) NONE ("", []) + [(("", []), [(subs, []), (dcl, [])])] + end val add_fundef = gen_add_fundef Attrib.attribute @@ -190,9 +192,9 @@ (* setup *) -val setup = FundefData.init #> FundefCongs.init - #> Attrib.add_attributes - [("fundef_cong", Attrib.add_del_args cong_add cong_del, "declaration of congruence rule for function definitions")] +val setup = FundefData.init #> FundefCongs.init + #> Attrib.add_attributes + [("fundef_cong", Attrib.add_del_args cong_add cong_del, "declaration of congruence rule for function definitions")] val get_congs = FundefCommon.get_fundef_congs o Context.Theory @@ -207,7 +209,7 @@ val star = Scan.one (fn t => (OuterLex.val_of t = "*")); -val attribs_with_star = P.$$$ "[" |-- P.!!! ((P.list (star >> K NONE || P.attrib >> SOME)) +val attribs_with_star = P.$$$ "[" |-- P.!!! ((P.list (star >> K NONE || P.attrib >> SOME)) >> (fn x => (map_filter I x, exists is_none x))) --| P.$$$ "]"; @@ -222,7 +224,7 @@ val functionP = OuterSyntax.command "function" "define general recursive functions" K.thy_goal - (((Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "sequential" -- P.$$$ ")") >> K true) false) -- + (((Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "sequential" -- P.$$$ ")") >> K true) false) -- P.and_list1 function_decl) >> (fn (prepr, eqnss) => Toplevel.print o Toplevel.theory_to_proof (add_fundef eqnss prepr))); @@ -230,7 +232,7 @@ OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal ((Scan.optional P.name "" -- Scan.option (P.$$$ "(" |-- Scan.optional (P.name --| P.$$$ ":") "dom" -- P.term --| P.$$$ ")")) >> (fn (name,dom) => - Toplevel.print o Toplevel.theory_to_proof (fundef_setup_termination_proof name dom))); + Toplevel.print o Toplevel.theory_to_proof (fundef_setup_termination_proof name dom))); val _ = OuterSyntax.add_keywords ["sequential", "otherwise"]; diff -r bbff23c3e2ca -r f34c5dbe74d5 src/Pure/Isar/isar_thy.ML --- a/src/Pure/Isar/isar_thy.ML Tue Aug 08 18:40:56 2006 +0200 +++ b/src/Pure/Isar/isar_thy.ML Wed Aug 09 00:12:33 2006 +0200 @@ -80,12 +80,14 @@ fun apply_theorems args = apfst (maps snd) o theorems "" [(("", []), args)]; fun apply_theorems_i args = apfst (maps snd) o theorems_i "" [(("", []), args)]; +(* FIXME local_theory *) fun smart_theorems kind NONE args thy = thy |> theorems kind args |> tap (present_theorems kind) |> (fn (_, thy) => `ProofContext.init thy) | smart_theorems kind (SOME loc) args thy = thy |> Locale.note_thmss kind loc args + ||> (fn ctxt' => (ctxt', ProofContext.theory_of ctxt')) |> tap (fn ((_, res), (_, thy')) => present_theorems kind (res, thy')) |> #2; @@ -131,7 +133,8 @@ (* global endings *) fun global_ending ending = Toplevel.proof_to_theory_context (fn int => fn state => - if can (Proof.assert_bottom true) state then ending int state + if can (Proof.assert_bottom true) state then + ending int state |> (fn ctxt' => (ctxt', ProofContext.theory_of ctxt')) else raise Toplevel.UNDEF); fun global_qed m = global_ending (K (Proof.global_qed (m, true))); diff -r bbff23c3e2ca -r f34c5dbe74d5 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Tue Aug 08 18:40:56 2006 +0200 +++ b/src/Pure/Isar/proof.ML Wed Aug 09 00:12:33 2006 +0200 @@ -94,19 +94,19 @@ val global_goal: (context -> (string * string) * (string * thm list) list -> unit) -> (theory -> 'a -> attribute) -> (context * 'b list -> context * (term list list * (context -> context))) -> - string -> Method.text option -> (thm list list -> theory -> theory) -> + string -> Method.text option -> (thm list list -> context -> context) -> string option -> string * 'a list -> ((string * 'a list) * 'b) list -> context -> state - val global_qed: Method.text option * bool -> state -> context * theory + val global_qed: Method.text option * bool -> state -> context val local_terminal_proof: Method.text * Method.text option -> state -> state Seq.seq val local_default_proof: state -> state Seq.seq val local_immediate_proof: state -> state Seq.seq val local_done_proof: state -> state Seq.seq val local_skip_proof: bool -> state -> state Seq.seq - val global_terminal_proof: Method.text * Method.text option -> state -> context * theory - val global_default_proof: state -> context * theory - val global_immediate_proof: state -> context * theory - val global_done_proof: state -> context * theory - val global_skip_proof: bool -> state -> context * theory + val global_terminal_proof: Method.text * Method.text option -> state -> context + val global_default_proof: state -> context + val global_immediate_proof: state -> context + val global_done_proof: state -> context + val global_skip_proof: bool -> state -> context val have: Method.text option -> (thm list list -> state -> state Seq.seq) -> ((string * Attrib.src list) * (string * string list) list) list -> bool -> state -> state val have_i: Method.text option -> (thm list list -> state -> state Seq.seq) -> @@ -115,10 +115,10 @@ ((string * Attrib.src list) * (string * string list) list) list -> bool -> state -> state val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) -> ((string * attribute list) * (term * term list) list) list -> bool -> state -> state - val theorem: string -> Method.text option -> (thm list list -> theory -> theory) -> + val theorem: string -> Method.text option -> (thm list list -> context -> context) -> string option -> string * Attrib.src list -> ((string * Attrib.src list) * (string * string list) list) list -> context -> state - val theorem_i: string -> Method.text option -> (thm list list -> theory -> theory) -> + val theorem_i: string -> Method.text option -> (thm list list -> context -> context) -> string option -> string * attribute list -> ((string * attribute list) * (term * term list) list) list -> context -> state end; @@ -152,7 +152,7 @@ before_qed: Method.text option, after_qed: (thm list list -> state -> state Seq.seq) * - (thm list list -> theory -> theory)}; + (thm list list -> context -> context)}; fun make_goal (statement, using, goal, before_qed, after_qed) = Goal {statement = statement, using = using, goal = goal, @@ -386,10 +386,6 @@ fun goal_cases st = RuleCases.make_common true (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st)); -fun check_theory thy state = - if subthy (thy, theory_of state) then state - else error ("Bad theory of method result: " ^ Context.str_of_thy thy); - fun apply_method current_context meth_fun state = let val (goal_ctxt, (_, {statement, using, goal, before_qed, after_qed})) = find_goal state; @@ -397,7 +393,6 @@ in Method.apply meth using goal |> Seq.map (fn (meth_cases, goal') => state - |> check_theory (Thm.theory_of_thm goal') |> map_goal (ProofContext.add_cases false (no_goal_cases goal @ goal_cases goal') #> ProofContext.add_cases true meth_cases) @@ -881,10 +876,11 @@ #> Sign.restore_naming thy; fun after_qed' results = - (case target of NONE => I - | SOME prfx => store_results (NameSpace.base prfx) - (map (ProofContext.export_standard ctxt thy_ctxt - #> map Drule.strip_shyps_warning) results)) + ProofContext.theory + (case target of NONE => I + | SOME prfx => store_results (NameSpace.base prfx) + (map (ProofContext.export_standard ctxt thy_ctxt + #> map Drule.strip_shyps_warning) results)) #> after_qed results; in init ctxt @@ -900,8 +896,7 @@ fun global_qeds txt = end_proof true txt #> Seq.map (generic_qed #> (fn (((_, after_qed), results), state) => - after_qed results (theory_of state) - |> (fn thy => (ProofContext.transfer thy (context_of state), thy)))) + after_qed results (context_of state))) |> Seq.DETERM; (*backtracking may destroy theory!*) fun global_qed txt = diff -r bbff23c3e2ca -r f34c5dbe74d5 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Tue Aug 08 18:40:56 2006 +0200 +++ b/src/Pure/Isar/toplevel.ML Wed Aug 09 00:12:33 2006 +0200 @@ -546,7 +546,8 @@ warning "Cannot skip proof of schematic goal statement" else (); if ! skip_proofs andalso not schematic then - SkipProof ((History.init (undo_limit int) 0, #2 (Proof.global_skip_proof int prf)), thy) + SkipProof ((History.init (undo_limit int) 0, + ProofContext.theory_of (Proof.global_skip_proof int prf)), thy) else Proof (ProofHistory.init (undo_limit int) prf, thy) end | _ => raise UNDEF));