1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML Sat Oct 07 01:31:04 2006 +0200
1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML Sat Oct 07 01:31:05 2006 +0200
1.3 @@ -9,16 +9,16 @@
1.4
1.5 signature FUNDEF_PACKAGE =
1.6 sig
1.7 - val add_fundef : (string * string option * mixfix) list
1.8 + val add_fundef : (string * string option * mixfix) list
1.9 -> ((bstring * Attrib.src list) * string list) list list
1.10 - -> FundefCommon.fundef_config
1.11 - -> local_theory
1.12 + -> FundefCommon.fundef_config
1.13 + -> local_theory
1.14 -> Proof.state
1.15
1.16 - val add_fundef_i: (string * typ option * mixfix) list
1.17 + val add_fundef_i: (string * typ option * mixfix) list
1.18 -> ((bstring * Attrib.src list) * term list) list list
1.19 - -> bool
1.20 - -> local_theory
1.21 + -> bool
1.22 + -> local_theory
1.23 -> Proof.state
1.24
1.25 val cong_add: attribute
1.26 @@ -43,24 +43,13 @@
1.27 fun restore_spec_structure reps spec =
1.28 (burrow o burrow_snd o burrow o K) reps spec
1.29
1.30 -fun with_local_path path f lthy =
1.31 - let
1.32 - val restore = Theory.restore_naming (ProofContext.theory_of lthy)
1.33 - in
1.34 - lthy
1.35 - |> LocalTheory.theory (Theory.add_path path)
1.36 - |> f
1.37 - |> LocalTheory.theory restore
1.38 - end
1.39 -
1.40 fun add_simps label moreatts mutual_info fixes psimps spec lthy =
1.41 let
1.42 val fnames = map (fst o fst) fixes
1.43 val psimps_by_f = FundefMutual.sort_by_function mutual_info fnames psimps
1.44
1.45 fun add_for_f fname psimps =
1.46 - with_local_path fname
1.47 - (LocalTheory.note ((label, Attrib.internal Simplifier.simp_add :: moreatts), psimps) #> snd)
1.48 + LocalTheory.note ((NameSpace.append fname label, Attrib.internal Simplifier.simp_add :: moreatts), psimps) #> snd
1.49 in
1.50 lthy
1.51 |> fold_map (fold_map LocalTheory.note) (restore_spec_structure psimps spec) |> snd
1.52 @@ -72,15 +61,15 @@
1.53 let
1.54 val fundef_data = FundefMutual.mk_partial_rules_mutual lthy mutual_info data result
1.55 val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
1.56 + val qualify = NameSpace.append defname;
1.57 in
1.58 lthy
1.59 |> add_simps "psimps" [] mutual_info fixes psimps spec
1.60 - |> with_local_path defname
1.61 - (LocalTheory.note (("domintros", []), domintros) #> snd
1.62 - #> LocalTheory.note (("termination", []), [termination]) #> snd
1.63 - #> LocalTheory.note (("cases", []), [cases]) #> snd
1.64 - #> LocalTheory.note (("pinduct", [Attrib.internal (InductAttrib.induct_set "")]), simple_pinducts) #> snd)
1.65 - |> LocalTheory.theory (Context.theory_map (add_fundef_data defname (fundef_data, mutual_info, (fixes,spec))))
1.66 + |> LocalTheory.note ((qualify "domintros", []), domintros) |> snd
1.67 + |> LocalTheory.note ((qualify "termination", []), [termination]) |> snd
1.68 + |> LocalTheory.note ((qualify "cases", []), [cases]) |> snd
1.69 + |> LocalTheory.note ((qualify "pinduct", [Attrib.internal (InductAttrib.induct_set "")]), simple_pinducts) |> snd
1.70 + |> LocalTheory.declaration (add_fundef_data defname (fundef_data, mutual_info, (fixes,spec)))
1.71 end (* FIXME: Add cases for induct and cases thm *)
1.72
1.73
1.74 @@ -94,7 +83,7 @@
1.75 val spec = map (fn eqns => snd (fst (prep [] eqns ctxt'))) eqnss
1.76 |> map (map (apsnd (map (fn t => fold_rev (mk_forall o Free) (frees_in_term ctxt' t) t)))) (* Add quantifiers *)
1.77 |> map2 (map2 (fn fs => fn (r, thms) => (r, fs ~~ thms))) flags
1.78 - |> (burrow o burrow_snd o burrow)
1.79 + |> (burrow o burrow_snd o burrow)
1.80 (FundefSplit.split_some_equations lthy)
1.81 |> map (map (apsnd flat))
1.82 in
1.83 @@ -110,7 +99,7 @@
1.84 val t_eqns = spec
1.85 |> flat |> map snd |> flat (* flatten external structure *)
1.86
1.87 - val ((mutual_info, name, prep_result as Prep {goal, goalI, ...}), lthy) =
1.88 + val ((mutual_info, name, prep_result as Prep {goal, goalI, ...}), lthy) =
1.89 FundefMutual.prepare_fundef_mutual fixes t_eqns default lthy
1.90
1.91 val afterqed = fundef_afterqed fixes spec mutual_info name prep_result
1.92 @@ -130,15 +119,15 @@
1.93 val tsimps = map remove_domain_condition psimps
1.94 val tinduct = map remove_domain_condition simple_pinducts
1.95
1.96 - (* FIXME: How to generate code from (possibly) local contexts
1.97 + (* FIXME: How to generate code from (possibly) local contexts
1.98 val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
1.99 val allatts = if has_guards then [] else [Attrib.internal (RecfunCodegen.add NONE)]
1.100 *)
1.101 + val qualify = NameSpace.append defname;
1.102 in
1.103 lthy
1.104 |> add_simps "simps" [] mutual_info fixes tsimps stmts
1.105 - |> with_local_path defname
1.106 - (LocalTheory.note (("induct", []), tinduct) #> snd)
1.107 + |> LocalTheory.note ((qualify "induct", []), tinduct) |> snd
1.108 end
1.109
1.110
1.111 @@ -151,9 +140,9 @@
1.112 val (res as FundefMResult {termination, ...}, _, _) = data
1.113 val goal = FundefTermination.mk_total_termination_goal data
1.114 in
1.115 - lthy
1.116 + lthy
1.117 |> ProofContext.note_thmss_i [(("termination",
1.118 - [ContextRules.intro_query NONE]), [(ProofContext.export_standard lthy lthy [termination], [])])] |> snd
1.119 + [ContextRules.intro_query NONE]), [(ProofContext.standard lthy [termination], [])])] |> snd
1.120 |> Proof.theorem_i PureThy.internalK NONE
1.121 (total_termination_afterqed name data) NONE ("", [])
1.122 [(("", []), [(goal, [])])]
1.123 @@ -196,8 +185,8 @@
1.124 val statements_ow = or_list1 statement_ow
1.125
1.126
1.127 -fun local_theory_to_proof f =
1.128 - Toplevel.theory_to_proof (f o LocalTheory.init NONE)
1.129 +fun local_theory_to_proof f =
1.130 + Toplevel.theory_to_proof (f o TheoryTarget.init NONE)
1.131
1.132 val functionP =
1.133 OuterSyntax.command "function" "define general recursive functions" K.thy_goal
1.134 @@ -208,7 +197,7 @@
1.135
1.136 val terminationP =
1.137 OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
1.138 - (Scan.option P.name
1.139 + (Scan.option P.name
1.140 >> (fn name => Toplevel.print o local_theory_to_proof (fundef_setup_termination_proof name)));
1.141
1.142