# HG changeset patch # User wenzelm # Date 1160177465 -7200 # Node ID 368b997ad67e5702517dfc2ce30a55b48cb48955 # Parent bc2669d5744d0d2e079a3b33b506c32dcfd54114 removed with_local_path -- LocalTheory.note admits qualified names; TheoryTarget.init; diff -r bc2669d5744d -r 368b997ad67e src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Sat Oct 07 01:31:04 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_package.ML Sat Oct 07 01:31:05 2006 +0200 @@ -9,16 +9,16 @@ signature FUNDEF_PACKAGE = sig - val add_fundef : (string * string option * mixfix) list + val add_fundef : (string * string option * mixfix) list -> ((bstring * Attrib.src list) * string list) list list - -> FundefCommon.fundef_config - -> local_theory + -> FundefCommon.fundef_config + -> local_theory -> Proof.state - val add_fundef_i: (string * typ option * mixfix) list + val add_fundef_i: (string * typ option * mixfix) list -> ((bstring * Attrib.src list) * term list) list list - -> bool - -> local_theory + -> bool + -> local_theory -> Proof.state val cong_add: attribute @@ -43,24 +43,13 @@ fun restore_spec_structure reps spec = (burrow o burrow_snd o burrow o K) reps spec -fun with_local_path path f lthy = - let - val restore = Theory.restore_naming (ProofContext.theory_of lthy) - in - lthy - |> LocalTheory.theory (Theory.add_path path) - |> f - |> LocalTheory.theory restore - end - fun add_simps label moreatts mutual_info fixes psimps spec lthy = let val fnames = map (fst o fst) fixes val psimps_by_f = FundefMutual.sort_by_function mutual_info fnames psimps fun add_for_f fname psimps = - with_local_path fname - (LocalTheory.note ((label, Attrib.internal Simplifier.simp_add :: moreatts), psimps) #> snd) + LocalTheory.note ((NameSpace.append fname label, Attrib.internal Simplifier.simp_add :: moreatts), psimps) #> snd in lthy |> fold_map (fold_map LocalTheory.note) (restore_spec_structure psimps spec) |> snd @@ -72,15 +61,15 @@ let val fundef_data = FundefMutual.mk_partial_rules_mutual lthy mutual_info data result val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data + val qualify = NameSpace.append defname; in lthy |> add_simps "psimps" [] mutual_info fixes psimps spec - |> with_local_path defname - (LocalTheory.note (("domintros", []), domintros) #> snd - #> LocalTheory.note (("termination", []), [termination]) #> snd - #> LocalTheory.note (("cases", []), [cases]) #> snd - #> LocalTheory.note (("pinduct", [Attrib.internal (InductAttrib.induct_set "")]), simple_pinducts) #> snd) - |> LocalTheory.theory (Context.theory_map (add_fundef_data defname (fundef_data, mutual_info, (fixes,spec)))) + |> LocalTheory.note ((qualify "domintros", []), domintros) |> snd + |> LocalTheory.note ((qualify "termination", []), [termination]) |> snd + |> LocalTheory.note ((qualify "cases", []), [cases]) |> snd + |> LocalTheory.note ((qualify "pinduct", [Attrib.internal (InductAttrib.induct_set "")]), simple_pinducts) |> snd + |> LocalTheory.declaration (add_fundef_data defname (fundef_data, mutual_info, (fixes,spec))) end (* FIXME: Add cases for induct and cases thm *) @@ -94,7 +83,7 @@ val spec = map (fn eqns => snd (fst (prep [] eqns ctxt'))) eqnss |> map (map (apsnd (map (fn t => fold_rev (mk_forall o Free) (frees_in_term ctxt' t) t)))) (* Add quantifiers *) |> map2 (map2 (fn fs => fn (r, thms) => (r, fs ~~ thms))) flags - |> (burrow o burrow_snd o burrow) + |> (burrow o burrow_snd o burrow) (FundefSplit.split_some_equations lthy) |> map (map (apsnd flat)) in @@ -110,7 +99,7 @@ val t_eqns = spec |> flat |> map snd |> flat (* flatten external structure *) - val ((mutual_info, name, prep_result as Prep {goal, goalI, ...}), lthy) = + val ((mutual_info, name, prep_result as Prep {goal, goalI, ...}), lthy) = FundefMutual.prepare_fundef_mutual fixes t_eqns default lthy val afterqed = fundef_afterqed fixes spec mutual_info name prep_result @@ -130,15 +119,15 @@ val tsimps = map remove_domain_condition psimps val tinduct = map remove_domain_condition simple_pinducts - (* FIXME: How to generate code from (possibly) local contexts + (* FIXME: How to generate code from (possibly) local contexts val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps val allatts = if has_guards then [] else [Attrib.internal (RecfunCodegen.add NONE)] *) + val qualify = NameSpace.append defname; in lthy |> add_simps "simps" [] mutual_info fixes tsimps stmts - |> with_local_path defname - (LocalTheory.note (("induct", []), tinduct) #> snd) + |> LocalTheory.note ((qualify "induct", []), tinduct) |> snd end @@ -151,9 +140,9 @@ val (res as FundefMResult {termination, ...}, _, _) = data val goal = FundefTermination.mk_total_termination_goal data in - lthy + lthy |> ProofContext.note_thmss_i [(("termination", - [ContextRules.intro_query NONE]), [(ProofContext.export_standard lthy lthy [termination], [])])] |> snd + [ContextRules.intro_query NONE]), [(ProofContext.standard lthy [termination], [])])] |> snd |> Proof.theorem_i PureThy.internalK NONE (total_termination_afterqed name data) NONE ("", []) [(("", []), [(goal, [])])] @@ -196,8 +185,8 @@ val statements_ow = or_list1 statement_ow -fun local_theory_to_proof f = - Toplevel.theory_to_proof (f o LocalTheory.init NONE) +fun local_theory_to_proof f = + Toplevel.theory_to_proof (f o TheoryTarget.init NONE) val functionP = OuterSyntax.command "function" "define general recursive functions" K.thy_goal @@ -208,7 +197,7 @@ val terminationP = OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal - (Scan.option P.name + (Scan.option P.name >> (fn name => Toplevel.print o local_theory_to_proof (fundef_setup_termination_proof name)));