src/HOL/Tools/function_package/fundef_package.ML
changeset 21255 617fdb08abe9
parent 21240 8e75fb38522c
child 21319 cf814e36f788
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Nov 08 21:45:15 2006 +0100
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Nov 08 22:24:54 2006 +0100
     1.3 @@ -50,31 +50,43 @@
     1.4  fun add_simps label moreatts mutual_info fixes psimps spec lthy =
     1.5      let
     1.6        val fnames = map (fst o fst) fixes
     1.7 -      val psimps_by_f = FundefMutual.sort_by_function mutual_info fnames psimps
     1.8 +
     1.9 +      val (saved_spec_psimps, lthy) = fold_map (fold_map LocalTheory.note) (restore_spec_structure psimps spec) lthy
    1.10 +      val saved_psimps = flat (map snd (flat saved_spec_psimps))
    1.11 +
    1.12 +      val psimps_by_f = FundefMutual.sort_by_function mutual_info fnames saved_psimps
    1.13  
    1.14        fun add_for_f fname psimps =
    1.15            LocalTheory.note ((NameSpace.append fname label, Attrib.internal Simplifier.simp_add :: moreatts), psimps) #> snd
    1.16      in
    1.17 -      lthy
    1.18 -        |> fold_map (fold_map LocalTheory.note) (restore_spec_structure psimps spec) |> snd
    1.19 -        |> fold2 add_for_f fnames psimps_by_f
    1.20 +      (saved_psimps,
    1.21 +       fold2 add_for_f fnames psimps_by_f lthy)
    1.22      end
    1.23  
    1.24  
    1.25  fun fundef_afterqed fixes spec mutual_info defname data [[result]] lthy =
    1.26      let
    1.27 -        val fundef_data = FundefMutual.mk_partial_rules_mutual lthy mutual_info data result
    1.28 -        val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
    1.29 -        val qualify = NameSpace.append defname;
    1.30 +      val Prep {f, R, ...} = data
    1.31 +      val fundef_data = FundefMutual.mk_partial_rules_mutual lthy mutual_info data result
    1.32 +      val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
    1.33 +      val qualify = NameSpace.append defname
    1.34 +          
    1.35 +      val (((psimps', pinducts'), (_, [termination'])), lthy) = 
    1.36 +          lthy
    1.37 +            |> PROFILE "adding_psimps" (add_simps "psimps" [] mutual_info fixes psimps spec)
    1.38 +            ||>> PROFILE "adding pinduct" (LocalTheory.note ((qualify "pinduct", [Attrib.internal (InductAttrib.induct_set "")]), simple_pinducts))
    1.39 +            ||>> PROFILE "adding termination" (LocalTheory.note ((qualify "termination", []), [termination]))
    1.40 +            ||> (snd o PROFILE "adding cases" (LocalTheory.note ((qualify "cases", []), [cases])))
    1.41 +            ||> (snd o PROFILE "adding domintros" (LocalTheory.note ((qualify "domintros", []), domintros)))
    1.42 +
    1.43 +      val cdata = FundefCtxData { fixes=fixes, spec=spec, mutual=mutual_info, psimps=psimps',
    1.44 +                                  pinducts=snd pinducts', termination=termination', f=f, R=R }
    1.45 +
    1.46 +      
    1.47      in
    1.48        lthy
    1.49 -        |> add_simps "psimps" [] mutual_info fixes psimps spec
    1.50 -        |> LocalTheory.note ((qualify "domintros", []), domintros) |> snd
    1.51 -        |> LocalTheory.note ((qualify "termination", []), [termination]) |> snd
    1.52 -        |> LocalTheory.note ((qualify "cases", []), [cases]) |> snd
    1.53 -        |> LocalTheory.note ((qualify "pinduct", [Attrib.internal (InductAttrib.induct_set "")]), simple_pinducts) |> snd
    1.54 -        |> LocalTheory.declaration (add_fundef_data defname (fundef_data, mutual_info, (fixes,spec))) (* save in target *)
    1.55 -        |> Context.proof_map (add_fundef_data defname (fundef_data, mutual_info, (fixes,spec))) (* also save in local context *)
    1.56 +        |> LocalTheory.declaration (add_fundef_data defname cdata) (* save in target *)
    1.57 +        |> Context.proof_map (add_fundef_data defname cdata) (* also save in local context *)
    1.58      end (* FIXME: Add cases for induct and cases thm *)
    1.59  
    1.60  
    1.61 @@ -117,12 +129,14 @@
    1.62  
    1.63  fun total_termination_afterqed defname data [[totality]] lthy =
    1.64      let
    1.65 -        val (FundefMResult {psimps, simple_pinducts, ... }, mutual_info, (fixes, stmts)) = data
    1.66 +      val FundefCtxData { fixes, spec, mutual, psimps, pinducts, ... } = data
    1.67 +
    1.68 +      val totality = PROFILE "closing" Drule.close_derivation totality
    1.69  
    1.70 -        val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
    1.71 +      val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
    1.72  
    1.73 -        val tsimps = map remove_domain_condition psimps
    1.74 -        val tinduct = map remove_domain_condition simple_pinducts
    1.75 +      val tsimps = PROFILE "making tsimps" (map remove_domain_condition) psimps
    1.76 +      val tinduct = PROFILE "making tinduct" (map remove_domain_condition) pinducts
    1.77  
    1.78          (* FIXME: How to generate code from (possibly) local contexts
    1.79          val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
    1.80 @@ -131,8 +145,8 @@
    1.81          val qualify = NameSpace.append defname;
    1.82      in
    1.83          lthy
    1.84 -          |> add_simps "simps" [] mutual_info fixes tsimps stmts
    1.85 -          |> LocalTheory.note ((qualify "induct", []), tinduct) |> snd
    1.86 +          |> PROFILE "adding tsimps" (add_simps "simps" [] mutual fixes tsimps spec) |> snd
    1.87 +          |> PROFILE "adding tinduct" (LocalTheory.note ((qualify "induct", []), tinduct)) |> snd
    1.88      end
    1.89  
    1.90  
    1.91 @@ -142,8 +156,8 @@
    1.92          val data = the (get_fundef_data name (Context.Proof lthy))
    1.93                     handle Option.Option => raise ERROR ("No such function definition: " ^ name)
    1.94  
    1.95 -        val (res as FundefMResult {termination, ...}, _, _) = data
    1.96 -        val goal = FundefTermination.mk_total_termination_goal data
    1.97 +        val FundefCtxData {termination, f, R, ...} = data
    1.98 +        val goal = FundefTermination.mk_total_termination_goal f R
    1.99      in
   1.100        lthy
   1.101          |> ProofContext.note_thmss_i [(("termination",