src/HOL/Tools/function_package/fundef_package.ML
changeset 22166 0a50d4db234a
parent 22102 a89ef7144729
child 22170 5682eeaefaf4
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Mon Jan 22 16:53:33 2007 +0100
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Mon Jan 22 17:29:43 2007 +0100
     1.3 @@ -40,6 +40,8 @@
     1.4  
     1.5  val note_theorem = LocalTheory.note Thm.theoremK
     1.6  
     1.7 +fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" 
     1.8 +
     1.9  fun burrow_snd f ps = (* ('a list -> 'b list) -> ('c * 'a) list -> ('c * 'b) list *)
    1.10      let val (xs, ys) = split_list ps
    1.11      in xs ~~ f ys end
    1.12 @@ -47,49 +49,46 @@
    1.13  fun restore_spec_structure reps spec =
    1.14      (burrow o burrow_snd o burrow o K) reps spec
    1.15  
    1.16 -fun add_simps label moreatts mutual_info fixes psimps spec lthy =
    1.17 +fun add_simps fixes spec sort label moreatts simps lthy =
    1.18      let
    1.19        val fnames = map (fst o fst) fixes
    1.20  
    1.21 -      val (saved_spec_psimps, lthy) =
    1.22 -        fold_map (fold_map note_theorem) (restore_spec_structure psimps spec) lthy
    1.23 -      val saved_psimps = flat (map snd (flat saved_spec_psimps))
    1.24 +      val (saved_spec_simps, lthy) =
    1.25 +        fold_map (fold_map note_theorem) (restore_spec_structure simps spec) lthy
    1.26 +      val saved_simps = flat (map snd (flat saved_spec_simps))
    1.27  
    1.28 -      val psimps_by_f = FundefMutual.sort_by_function mutual_info fnames saved_psimps
    1.29 +      val simps_by_f = sort saved_simps
    1.30  
    1.31 -      fun add_for_f fname psimps =
    1.32 +      fun add_for_f fname simps =
    1.33          note_theorem
    1.34            ((NameSpace.qualified fname label, Attrib.internal (K Simplifier.simp_add) :: moreatts),
    1.35 -            psimps) #> snd
    1.36 +            simps) #> snd
    1.37      in
    1.38 -      (saved_psimps,
    1.39 -       fold2 add_for_f fnames psimps_by_f lthy)
    1.40 +      (saved_simps,
    1.41 +       fold2 add_for_f fnames simps_by_f lthy)
    1.42      end
    1.43  
    1.44  
    1.45 -fun fundef_afterqed config fixes spec mutual_info defname data [[result]] lthy =
    1.46 +fun fundef_afterqed config fixes spec defname cont sort_cont [[proof]] lthy =
    1.47      let
    1.48 -      val FundefConfig { domintros, ...} = config
    1.49 -      val Prep {f, R, ...} = data
    1.50 -      val fundef_data = FundefMutual.mk_partial_rules_mutual lthy mutual_info data result
    1.51 -      val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
    1.52 +      val FundefResult {f, R, psimps, trsimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = 
    1.53 +          cont (Goal.close_result proof)
    1.54 +
    1.55        val qualify = NameSpace.qualified defname
    1.56 +      val addsimps = add_simps fixes spec sort_cont
    1.57  
    1.58        val (((psimps', pinducts'), (_, [termination'])), lthy) =
    1.59            lthy
    1.60 -            |> PROFILE "adding_psimps" (add_simps "psimps" [] mutual_info fixes psimps spec)
    1.61 -            ||>> PROFILE "adding pinduct"
    1.62 -              (note_theorem ((qualify "pinduct",
    1.63 -                [Attrib.internal (K (InductAttrib.induct_set ""))]), simple_pinducts))
    1.64 -            ||>> PROFILE "adding termination"
    1.65 -              (note_theorem ((qualify "termination", []), [termination]))
    1.66 -            ||> (snd o PROFILE "adding cases" (note_theorem ((qualify "cases", []), [cases])))
    1.67 -            ||> (snd o PROFILE "adding domintros" (note_theorem ((qualify "domintros", []), domintros)))
    1.68 +            |> addsimps "psimps" [] psimps
    1.69 +            ||> fold_option (snd oo addsimps "simps" []) trsimps
    1.70 +            ||>> note_theorem ((qualify "pinduct",
    1.71 +                                [Attrib.internal (K (InductAttrib.induct_set ""))]), simple_pinducts)
    1.72 +            ||>> note_theorem ((qualify "termination", []), [termination])
    1.73 +            ||> (snd o note_theorem ((qualify "cases", []), [cases]))
    1.74 +            ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros
    1.75  
    1.76 -      val cdata = FundefCtxData { fixes=fixes, spec=spec, mutual=mutual_info, psimps=psimps',
    1.77 +      val cdata = FundefCtxData { add_simps=addsimps, psimps=psimps',
    1.78                                    pinducts=snd pinducts', termination=termination', f=f, R=R }
    1.79 -
    1.80 -
    1.81      in
    1.82        lthy  (* FIXME proper handling of morphism *)
    1.83          |> LocalTheory.declaration (fn phi => add_fundef_data defname cdata) (* save in target *)
    1.84 @@ -117,33 +116,36 @@
    1.85  
    1.86  fun gen_add_fundef prep_spec fixspec eqnss_flags config lthy =
    1.87      let
    1.88 -      val FundefConfig {sequential, default, ...} = config
    1.89 +      val FundefConfig {sequential, default, tailrec, ...} = config
    1.90  
    1.91        val ((fixes, spec), ctxt') = prep_with_flags prep_spec fixspec eqnss_flags sequential lthy
    1.92 +
    1.93 +      val defname = mk_defname fixes
    1.94 +
    1.95        val t_eqns = spec
    1.96                       |> flat |> map snd |> flat (* flatten external structure *)
    1.97  
    1.98 -      val ((mutual_info, name, prep_result as Prep {goal, goalI, ...}), lthy) =
    1.99 -          FundefMutual.prepare_fundef_mutual fixes t_eqns default lthy
   1.100 +      val ((goalstate, cont, sort_cont), lthy) =
   1.101 +          FundefMutual.prepare_fundef_mutual config defname fixes t_eqns default lthy
   1.102  
   1.103 -      val afterqed = fundef_afterqed config fixes spec mutual_info name prep_result
   1.104 +      val afterqed = fundef_afterqed config fixes spec defname cont sort_cont
   1.105      in
   1.106 -      (name, lthy
   1.107 -         |> Proof.theorem_i NONE afterqed [[(goal, [])]]
   1.108 -         |> Proof.refine (Method.primitive_text (fn _ => goalI)) |> Seq.hd)
   1.109 +      (defname, lthy
   1.110 +         |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
   1.111 +         |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd)
   1.112      end
   1.113  
   1.114  
   1.115  fun total_termination_afterqed defname data [[totality]] lthy =
   1.116      let
   1.117 -      val FundefCtxData { fixes, spec, mutual, psimps, pinducts, ... } = data
   1.118 +      val FundefCtxData { add_simps, psimps, pinducts, ... } = data
   1.119  
   1.120 -      val totality = PROFILE "closing" Goal.close_result totality
   1.121 +      val totality = Goal.close_result totality
   1.122  
   1.123        val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
   1.124  
   1.125 -      val tsimps = PROFILE "making tsimps" (map remove_domain_condition) psimps
   1.126 -      val tinduct = PROFILE "making tinduct" (map remove_domain_condition) pinducts
   1.127 +      val tsimps = map remove_domain_condition psimps
   1.128 +      val tinduct = map remove_domain_condition pinducts
   1.129  
   1.130          (* FIXME: How to generate code from (possibly) local contexts*)
   1.131        val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
   1.132 @@ -152,26 +154,26 @@
   1.133        val qualify = NameSpace.qualified defname;
   1.134      in
   1.135        lthy
   1.136 -        |> PROFILE "adding tsimps" (add_simps "simps" allatts mutual fixes tsimps spec) |> snd
   1.137 -        |> PROFILE "adding tinduct" (note_theorem ((qualify "induct", []), tinduct)) |> snd
   1.138 +        |> add_simps "simps" allatts tsimps |> snd
   1.139 +        |> note_theorem ((qualify "induct", []), tinduct) |> snd
   1.140      end
   1.141  
   1.142  
   1.143  fun setup_termination_proof name_opt lthy =
   1.144      let
   1.145 -        val name = the_default (get_last_fundef (Context.Proof lthy)) name_opt
   1.146 -        val data = the (get_fundef_data name (Context.Proof lthy))
   1.147 -                   handle Option.Option => raise ERROR ("No such function definition: " ^ name)
   1.148 +        val defname = the_default (get_last_fundef (Context.Proof lthy)) name_opt
   1.149 +        val data = the (get_fundef_data defname (Context.Proof lthy))
   1.150 +                   handle Option.Option => raise ERROR ("No such function definition: " ^ defname)
   1.151  
   1.152 -        val FundefCtxData {termination, f, R, ...} = data
   1.153 -        val goal = FundefTermination.mk_total_termination_goal f R
   1.154 +        val FundefCtxData {termination, R, ...} = data
   1.155 +        val goal = FundefTermination.mk_total_termination_goal R
   1.156      in
   1.157        lthy
   1.158          |> ProofContext.note_thmss_i ""
   1.159            [(("termination", [ContextRules.intro_query NONE]),
   1.160              [([Goal.norm_result termination], [])])] |> snd
   1.161          |> set_termination_rule termination
   1.162 -        |> Proof.theorem_i NONE (total_termination_afterqed name data) [[(goal, [])]]
   1.163 +        |> Proof.theorem_i NONE (total_termination_afterqed defname data) [[(goal, [])]]
   1.164      end
   1.165  
   1.166