removed with_local_path -- LocalTheory.note admits qualified names;
authorwenzelm
Sat Oct 07 01:31:05 2006 +0200 (2006-10-07)
changeset 20877368b997ad67e
parent 20876 bc2669d5744d
child 20878 384c5bb713b2
removed with_local_path -- LocalTheory.note admits qualified names;
TheoryTarget.init;
src/HOL/Tools/function_package/fundef_package.ML
     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