src/HOL/Tools/function_package/fundef_package.ML
author bulwahn
Sat May 16 20:17:59 2009 +0200 (2009-05-16)
changeset 31174 f1f1e9b53c81
parent 31172 74d72ba262fb
child 31177 c39994cb152a
permissions -rw-r--r--
added new kind generated_theorem for theorems which are generated by packages to distinguish between theorems from users and packages
     1 (*  Title:      HOL/Tools/function_package/fundef_package.ML
     2     Author:     Alexander Krauss, TU Muenchen
     3 
     4 A package for general recursive function definitions.
     5 Isar commands.
     6 *)
     7 
     8 signature FUNDEF_PACKAGE =
     9 sig
    10     val add_fundef :  (binding * typ option * mixfix) list
    11                        -> (Attrib.binding * term) list
    12                        -> FundefCommon.fundef_config
    13                        -> local_theory
    14                        -> Proof.state
    15     val add_fundef_cmd :  (binding * string option * mixfix) list
    16                       -> (Attrib.binding * string) list
    17                       -> FundefCommon.fundef_config
    18                       -> local_theory
    19                       -> Proof.state
    20 
    21     val termination_proof : term option -> local_theory -> Proof.state
    22     val termination_proof_cmd : string option -> local_theory -> Proof.state
    23     val termination : term option -> local_theory -> Proof.state
    24     val termination_cmd : string option -> local_theory -> Proof.state
    25 
    26     val setup : theory -> theory
    27     val get_congs : Proof.context -> thm list
    28 end
    29 
    30 
    31 structure FundefPackage : FUNDEF_PACKAGE =
    32 struct
    33 
    34 open FundefLib
    35 open FundefCommon
    36 
    37 val simp_attribs = map (Attrib.internal o K)
    38     [Simplifier.simp_add,
    39      Code.add_default_eqn_attribute,
    40      Nitpick_Const_Simp_Thms.add,
    41      Quickcheck_RecFun_Simp_Thms.add]
    42 
    43 val psimp_attribs = map (Attrib.internal o K)
    44     [Simplifier.simp_add,
    45      Nitpick_Const_Psimp_Thms.add]
    46 
    47 fun note_theorem ((name, atts), ths) =
    48   LocalTheory.note Thm.generated_theoremK ((Binding.qualified_name name, atts), ths)
    49 
    50 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
    51 
    52 fun add_simps fnames post sort extra_qualify label moreatts simps lthy =
    53     let
    54       val spec = post simps
    55                    |> map (apfst (apsnd (fn ats => moreatts @ ats)))
    56                    |> map (apfst (apfst extra_qualify))
    57 
    58       val (saved_spec_simps, lthy) =
    59         fold_map (LocalTheory.note Thm.generated_theoremK) spec lthy
    60 
    61       val saved_simps = flat (map snd saved_spec_simps)
    62       val simps_by_f = sort saved_simps
    63 
    64       fun add_for_f fname simps =
    65         note_theorem ((Long_Name.qualify fname label, []), simps) #> snd
    66     in
    67       (saved_simps,
    68        fold2 add_for_f fnames simps_by_f lthy)
    69     end
    70 
    71 fun gen_add_fundef is_external prep default_constraint fixspec eqns config lthy =
    72     let
    73       val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
    74       val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
    75       val fixes = map (apfst (apfst Binding.name_of)) fixes0;
    76       val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0;
    77       val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config ctxt' fixes spec
    78 
    79       val defname = mk_defname fixes
    80 
    81       val ((goalstate, cont), lthy) =
    82           FundefMutual.prepare_fundef_mutual config defname fixes eqs lthy
    83 
    84       fun afterqed [[proof]] lthy =
    85         let
    86           val FundefResult {fs, R, psimps, trsimps,  simple_pinducts, termination,
    87                             domintros, cases, ...} =
    88           cont (Thm.close_derivation proof)
    89 
    90           val fnames = map (fst o fst) fixes
    91           val qualify = Long_Name.qualify defname
    92           val addsmps = add_simps fnames post sort_cont
    93 
    94           val (((psimps', pinducts'), (_, [termination'])), lthy) =
    95             lthy
    96             |> addsmps (Binding.qualify false "partial") "psimps"
    97                  psimp_attribs psimps
    98             ||> fold_option (snd oo addsmps I "simps" simp_attribs) trsimps
    99             ||>> note_theorem ((qualify "pinduct",
   100                    [Attrib.internal (K (RuleCases.case_names cnames)),
   101                     Attrib.internal (K (RuleCases.consumes 1)),
   102                     Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
   103             ||>> note_theorem ((qualify "termination", []), [termination])
   104             ||> (snd o note_theorem ((qualify "cases",
   105                    [Attrib.internal (K (RuleCases.case_names cnames))]), [cases]))
   106             ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros
   107 
   108           val cdata = FundefCtxData { add_simps=addsmps, case_names=cnames, psimps=psimps',
   109                                       pinducts=snd pinducts', termination=termination',
   110                                       fs=fs, R=R, defname=defname }
   111           val _ =
   112             if not is_external then ()
   113             else Specification.print_consts lthy (K false) (map fst fixes)
   114         in
   115           lthy
   116           |> LocalTheory.declaration (add_fundef_data o morph_fundef_data cdata)
   117         end
   118     in
   119       lthy
   120         |> is_external ? LocalTheory.set_group (serial_string ())
   121         |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
   122         |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
   123     end
   124 
   125 val add_fundef = gen_add_fundef false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)
   126 val add_fundef_cmd = gen_add_fundef true Specification.read_spec "_::type"
   127 
   128 fun gen_termination_proof prep_term raw_term_opt lthy =
   129     let
   130       val term_opt = Option.map (prep_term lthy) raw_term_opt
   131       val data = the (case term_opt of
   132                         SOME t => (import_fundef_data t lthy
   133                           handle Option.Option =>
   134                             error ("Not a function: " ^ quote (Syntax.string_of_term lthy t)))
   135                       | NONE => (import_last_fundef lthy handle Option.Option => error "Not a function"))
   136 
   137         val FundefCtxData { termination, R, add_simps, case_names, psimps,
   138                             pinducts, defname, ...} = data
   139         val domT = domain_type (fastype_of R)
   140         val goal = HOLogic.mk_Trueprop
   141                      (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
   142         fun afterqed [[totality]] lthy =
   143           let
   144             val totality = Thm.close_derivation totality
   145             val remove_domain_condition =
   146               full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
   147             val tsimps = map remove_domain_condition psimps
   148             val tinduct = map remove_domain_condition pinducts
   149             val qualify = Long_Name.qualify defname;
   150           in
   151             lthy
   152             |> add_simps I "simps" simp_attribs tsimps |> snd
   153             |> note_theorem
   154                ((qualify "induct",
   155                  [Attrib.internal (K (RuleCases.case_names case_names))]),
   156                 tinduct) |> snd
   157           end
   158     in
   159       lthy
   160       |> ProofContext.note_thmss ""
   161          [((Binding.empty, [ContextRules.rule_del]), [([allI], [])])] |> snd
   162       |> ProofContext.note_thmss ""
   163          [((Binding.empty, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
   164       |> ProofContext.note_thmss ""
   165          [((Binding.name "termination", [ContextRules.intro_bang (SOME 0)]),
   166            [([Goal.norm_result termination], [])])] |> snd
   167       |> Proof.theorem_i NONE afterqed [[(goal, [])]]
   168     end
   169 
   170 val termination_proof = gen_termination_proof Syntax.check_term;
   171 val termination_proof_cmd = gen_termination_proof Syntax.read_term;
   172 
   173 fun termination term_opt lthy =
   174   lthy
   175   |> LocalTheory.set_group (serial_string ())
   176   |> termination_proof term_opt;
   177 
   178 fun termination_cmd term_opt lthy =
   179   lthy
   180   |> LocalTheory.set_group (serial_string ())
   181   |> termination_proof_cmd term_opt;
   182 
   183 
   184 (* Datatype hook to declare datatype congs as "fundef_congs" *)
   185 
   186 
   187 fun add_case_cong n thy =
   188     Context.theory_map (FundefCtxTree.map_fundef_congs (Thm.add_thm
   189                           (DatatypePackage.get_datatype thy n |> the
   190                            |> #case_cong
   191                            |> safe_mk_meta_eq)))
   192                        thy
   193 
   194 val case_cong = fold add_case_cong
   195 
   196 val setup_case_cong = DatatypePackage.interpretation case_cong
   197 
   198 
   199 (* setup *)
   200 
   201 val setup =
   202   Attrib.setup @{binding fundef_cong}
   203     (Attrib.add_del FundefCtxTree.cong_add FundefCtxTree.cong_del)
   204     "declaration of congruence rule for function definitions"
   205   #> setup_case_cong
   206   #> FundefRelation.setup
   207   #> FundefCommon.TerminationSimps.setup
   208 
   209 val get_congs = FundefCtxTree.get_fundef_congs
   210 
   211 
   212 (* outer syntax *)
   213 
   214 local structure P = OuterParse and K = OuterKeyword in
   215 
   216 val _ =
   217   OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal
   218   (fundef_parser default_config
   219      >> (fn ((config, fixes), statements) => add_fundef_cmd fixes statements config));
   220 
   221 val _ =
   222   OuterSyntax.local_theory_to_proof "termination" "prove termination of a recursive function" K.thy_goal
   223   (Scan.option P.term >> termination_cmd);
   224 
   225 end;
   226 
   227 
   228 end