# HG changeset patch # User wenzelm # Date 1164128851 -3600 # Node ID 883337ea2f3bacecb1bd910a140c63292a2b4510 # Parent 944f80576be09f256374751b754b76f36490e696 LocalTheory.axioms/notes/defs: proper kind; simplified Proof.theorem(_i); diff -r 944f80576be0 -r 883337ea2f3b src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Tue Nov 21 18:07:30 2006 +0100 +++ b/src/HOL/Tools/function_package/fundef_package.ML Tue Nov 21 18:07:31 2006 +0100 @@ -38,6 +38,8 @@ open FundefLib open FundefCommon +val note_theorem = LocalTheory.note Thm.theoremK + fun burrow_snd f ps = (* ('a list -> 'b list) -> ('c * 'a) list -> ('c * 'b) list *) let val (xs, ys) = split_list ps in xs ~~ f ys end @@ -49,13 +51,16 @@ let val fnames = map (fst o fst) fixes - val (saved_spec_psimps, lthy) = fold_map (fold_map LocalTheory.note) (restore_spec_structure psimps spec) lthy + val (saved_spec_psimps, lthy) = + fold_map (fold_map note_theorem) (restore_spec_structure psimps spec) lthy val saved_psimps = flat (map snd (flat saved_spec_psimps)) val psimps_by_f = FundefMutual.sort_by_function mutual_info fnames saved_psimps fun add_for_f fname psimps = - LocalTheory.note ((NameSpace.qualified fname label, Attrib.internal Simplifier.simp_add :: moreatts), psimps) #> snd + note_theorem + ((NameSpace.qualified fname label, Attrib.internal Simplifier.simp_add :: moreatts), + psimps) #> snd in (saved_psimps, fold2 add_for_f fnames psimps_by_f lthy) @@ -73,10 +78,10 @@ val (((psimps', pinducts'), (_, [termination'])), lthy) = lthy |> PROFILE "adding_psimps" (add_simps "psimps" [] mutual_info fixes psimps spec) - ||>> PROFILE "adding pinduct" (LocalTheory.note ((qualify "pinduct", [Attrib.internal (InductAttrib.induct_set "")]), simple_pinducts)) - ||>> PROFILE "adding termination" (LocalTheory.note ((qualify "termination", []), [termination])) - ||> (snd o PROFILE "adding cases" (LocalTheory.note ((qualify "cases", []), [cases]))) - ||> (snd o PROFILE "adding domintros" (LocalTheory.note ((qualify "domintros", []), domintros))) + ||>> PROFILE "adding pinduct" (note_theorem ((qualify "pinduct", [Attrib.internal (InductAttrib.induct_set "")]), simple_pinducts)) + ||>> PROFILE "adding termination" (note_theorem ((qualify "termination", []), [termination])) + ||> (snd o PROFILE "adding cases" (note_theorem ((qualify "cases", []), [cases]))) + ||> (snd o PROFILE "adding domintros" (note_theorem ((qualify "domintros", []), domintros))) val cdata = FundefCtxData { fixes=fixes, spec=spec, mutual=mutual_info, psimps=psimps', pinducts=snd pinducts', termination=termination', f=f, R=R } @@ -121,7 +126,7 @@ val afterqed = fundef_afterqed config fixes spec mutual_info name prep_result in (name, lthy - |> Proof.theorem_i PureThy.internalK NONE afterqed [[(goal, [])]] + |> Proof.theorem_i NONE afterqed [[(goal, [])]] |> Proof.refine (Method.primitive_text (fn _ => goalI)) |> Seq.hd) end @@ -145,7 +150,7 @@ in lthy |> PROFILE "adding tsimps" (add_simps "simps" [] mutual fixes tsimps spec) |> snd - |> PROFILE "adding tinduct" (LocalTheory.note ((qualify "induct", []), tinduct)) |> snd + |> PROFILE "adding tinduct" (note_theorem ((qualify "induct", []), tinduct)) |> snd end @@ -159,11 +164,10 @@ val goal = FundefTermination.mk_total_termination_goal f R in lthy - |> ProofContext.note_thmss_i [(("termination", + |> ProofContext.note_thmss_i "" [(("termination", [ContextRules.intro_query NONE]), [(ProofContext.standard lthy [termination], [])])] |> snd |> set_termination_rule termination - |> Proof.theorem_i PureThy.internalK NONE - (total_termination_afterqed name data) [[(goal, [])]] + |> Proof.theorem_i NONE (total_termination_afterqed name data) [[(goal, [])]] end diff -r 944f80576be0 -r 883337ea2f3b src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Tue Nov 21 18:07:30 2006 +0100 +++ b/src/Pure/Isar/specification.ML Tue Nov 21 18:07:31 2006 +0100 @@ -102,7 +102,7 @@ val ((consts, axioms), lthy') = lthy |> LocalTheory.consts spec_frees vars ||> fold (fold Variable.auto_fixes o snd) specs (* FIXME !? *) - ||>> LocalTheory.axioms specs; + ||>> LocalTheory.axioms Thm.axiomK specs; (* FIXME generic target!? *) val hs = map (Term.head_of o #2 o Logic.dest_equals o Thm.prop_of o #2) consts; @@ -130,9 +130,9 @@ else error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote x')); val ((lhs, (_, th)), lthy2) = lthy1 (* |> LocalTheory.def ((x, mx), ((name ^ "_raw", []), rhs)); FIXME *) - |> LocalTheory.def ((x, mx), ((name, []), rhs)); + |> LocalTheory.def Thm.definitionK ((x, mx), ((name, []), rhs)); val ((b, [th']), lthy3) = lthy2 - |> LocalTheory.note ((name, atts), [prove lthy2 th]); + |> LocalTheory.note Thm.definitionK ((name, atts), [prove lthy2 th]); in (((x, T), (lhs, (b, th'))), LocalTheory.restore lthy3) end; val ((cs, defs), lthy') = lthy |> fold_map define args |>> split_list; @@ -185,12 +185,11 @@ fun gen_theorems prep_thms prep_att kind raw_facts lthy = let - val k = if kind = "" then [] else [Attrib.kind kind]; val attrib = prep_att (ProofContext.theory_of lthy); val facts = raw_facts |> map (fn ((name, atts), bs) => ((name, map attrib atts), - bs |> map (fn (b, more_atts) => (prep_thms lthy b, map attrib more_atts @ k)))); - val (res, lthy') = lthy |> LocalTheory.notes facts; + bs |> map (fn (b, more_atts) => (prep_thms lthy b, map attrib more_atts)))); + val (res, lthy') = lthy |> LocalTheory.notes kind facts; val _ = present_results' lthy' kind res; in (res, lthy') end; @@ -246,8 +245,8 @@ val (facts, goal_ctxt) = elems_ctxt |> (snd o ProofContext.add_fixes_i [(AutoBind.thesisN, NONE, NoSyn)]) |> fold_map assume_case (obtains ~~ propp) - |-> (fn ths => - ProofContext.note_thmss_i [((Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths); + |-> (fn ths => ProofContext.note_thmss_i Thm.assumptionK + [((Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths); in ((stmt, facts), goal_ctxt) end); fun gen_theorem prep_att prep_stmt @@ -255,7 +254,6 @@ let val _ = LocalTheory.assert lthy0; val thy = ProofContext.theory_of lthy0; - val attrib = prep_att thy; val (loc, ctxt, lthy) = (case (TheoryTarget.peek lthy0, exists (fn Locale.Expr _ => true | _ => false) raw_elems) of @@ -263,28 +261,26 @@ (SOME loc, ProofContext.init thy, LocalTheory.restore lthy0) | _ => (NONE, lthy0, lthy0)); + val attrib = prep_att thy; + val atts = map attrib raw_atts; + val elems = raw_elems |> (map o Locale.map_elem) (Element.map_ctxt {name = I, var = I, typ = I, term = I, fact = I, attrib = attrib}); val ((stmt, facts), goal_ctxt) = prep_statement attrib (prep_stmt loc) elems raw_concl ctxt; - val k = if kind = "" then [] else [Attrib.kind kind]; - val names = map (fst o fst) stmt; - val attss = map (fn ((_, atts), _) => atts @ k) stmt; - val atts = map attrib raw_atts @ k; - fun after_qed' results goal_ctxt' = let val results' = burrow (ProofContext.export_standard goal_ctxt' lthy) results in lthy - |> LocalTheory.notes ((names ~~ attss) ~~ map (fn ths => [(ths, [])]) results') + |> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results') |> (fn (res, lthy') => (present_results lthy' ((kind, name), res); - if name = "" andalso null raw_atts then lthy' - else #2 (LocalTheory.notes [((name, atts), [(maps #2 res, [])])] lthy'))) + if name = "" andalso null atts then lthy' + else #2 (LocalTheory.notes kind [((name, atts), [(maps #2 res, [])])] lthy'))) |> after_qed results' end; in goal_ctxt - |> Proof.theorem_i kind before_qed after_qed' (map snd stmt) + |> Proof.theorem_i before_qed after_qed' (map snd stmt) |> Proof.refine_insert facts end;