src/HOL/Tools/function_package/fundef_package.ML
author wenzelm
Wed Aug 09 00:12:33 2006 +0200 (2006-08-09)
changeset 20363 f34c5dbe74d5
parent 20338 ecdfc96cf4d0
child 20523 36a59e5d0039
permissions -rw-r--r--
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
     1 
     2 (*  Title:      HOL/Tools/function_package/fundef_package.ML
     3     ID:         $Id$
     4     Author:     Alexander Krauss, TU Muenchen
     5 
     6 A package for general recursive function definitions.
     7 Isar commands.
     8 
     9 *)
    10 
    11 signature FUNDEF_PACKAGE =
    12 sig
    13     val add_fundef : ((bstring * (Attrib.src list * bool)) * string) list list -> bool -> theory -> Proof.state (* Need an _i variant *)
    14 
    15     val cong_add: attribute
    16     val cong_del: attribute
    17 
    18     val setup : theory -> theory
    19     val get_congs : theory -> thm list
    20 end
    21 
    22 
    23 structure FundefPackage : FUNDEF_PACKAGE =
    24 struct
    25 
    26 open FundefCommon
    27 
    28 
    29 fun add_simps label moreatts (MutualPart {f_name, ...}, psimps) spec_part thy =
    30     let
    31       val psimpss = Library.unflat (map snd spec_part) psimps
    32       val (names, attss) = split_list (map fst spec_part)
    33 
    34       val thy = thy |> Theory.add_path f_name
    35 
    36       val thy = thy |> Theory.add_path label
    37       val spsimpss = map (map standard) psimpss (* FIXME *)
    38       val add_list = (names ~~ spsimpss) ~~ attss
    39       val (_, thy) = PureThy.add_thmss add_list thy
    40       val thy = thy |> Theory.parent_path
    41 
    42       val (_, thy) = PureThy.add_thmss [((label, flat spsimpss), Simplifier.simp_add :: moreatts)] thy
    43       val thy = thy |> Theory.parent_path
    44     in
    45       thy
    46     end
    47 
    48 
    49 
    50 
    51 
    52 
    53 fun fundef_afterqed congs mutual_info name data spec [[result]] thy =
    54     let
    55         val fundef_data = FundefMutual.mk_partial_rules_mutual thy mutual_info data result
    56         val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
    57         val Mutual {parts, ...} = mutual_info
    58 
    59         val Prep {names = Names {acc_R=accR, ...}, ...} = data
    60         val dom_abbrev = Logic.mk_equals (Free (name ^ "_dom", fastype_of accR), accR)
    61         val (_, thy) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) thy
    62 
    63         val thy = fold2 (add_simps "psimps" []) (parts ~~ psimps) spec thy
    64 
    65         val casenames = flat (map (map (fst o fst)) spec)
    66 
    67         val thy = thy |> Theory.add_path name
    68         val (_, thy) = PureThy.add_thms [(("cases", cases), [RuleCases.case_names casenames])] thy
    69         val (_, thy) = PureThy.add_thmss [(("domintros", domintros), [])] thy
    70         val (_, thy) = PureThy.add_thms [(("termination", standard termination), [])] thy
    71         val (_,thy) = PureThy.add_thmss [(("pinduct", map standard simple_pinducts), [RuleCases.case_names casenames, InductAttrib.induct_set ""])] thy
    72         val thy = thy |> Theory.parent_path
    73     in
    74       add_fundef_data name (fundef_data, mutual_info, spec) thy
    75     end
    76 
    77 fun gen_add_fundef prep_att eqns_attss (preprocess : bool) thy =
    78     let
    79       fun prep_eqns neqs =
    80           neqs
    81             |> map (apsnd (Sign.read_prop thy))
    82             |> map (apfst (apsnd (apfst (map (prep_att thy)))))
    83             |> FundefSplit.split_some_equations (ProofContext.init thy)
    84 
    85       val spec = map prep_eqns eqns_attss
    86       val t_eqnss = map (flat o map snd) spec
    87 
    88       val congs = get_fundef_congs (Context.Theory thy)
    89 
    90       val (mutual_info, name, (data, thy)) = FundefMutual.prepare_fundef_mutual congs t_eqnss thy
    91       val Prep {goal, goalI, ...} = data
    92     in
    93       thy |> ProofContext.init
    94           |> Proof.theorem_i PureThy.internalK NONE
    95               (ProofContext.theory o fundef_afterqed congs mutual_info name data spec) NONE ("", [])
    96               [(("", []), [(goal, [])])]
    97           |> Proof.refine (Method.primitive_text (fn _ => goalI))
    98           |> Seq.hd
    99     end
   100 
   101 
   102 fun total_termination_afterqed name (Mutual {parts, ...}) thmss thy =
   103     let
   104         val totality = hd (hd thmss)
   105 
   106         val (FundefMResult {psimps, simple_pinducts, ... }, Mutual {parts, ...}, spec)
   107           = the (get_fundef_data name thy)
   108 
   109         val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
   110 
   111         val tsimps = map (map remove_domain_condition) psimps
   112         val tinduct = map remove_domain_condition simple_pinducts
   113 
   114         val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) (flat tsimps)
   115         val allatts = if has_guards then [] else [RecfunCodegen.add NONE]
   116 
   117         val thy = fold2 (add_simps "simps" allatts) (parts ~~ tsimps) spec thy
   118 
   119         val thy = Theory.add_path name thy
   120 
   121         val (_, thy) = PureThy.add_thmss [(("induct", map standard tinduct), [])] thy
   122         val thy = Theory.parent_path thy
   123     in
   124         thy
   125     end
   126 
   127 (*
   128 fun mk_partial_rules name D_name D domT idomT thmss thy =
   129     let
   130         val [subs, dcl] = (hd thmss)
   131 
   132         val {f_const, f_curried_const, G_const, R_const, G_elims, completeness, f_simps, names_attrs, subset_induct, ... }
   133           = the (Symtab.lookup (FundefData.get thy) name)
   134 
   135         val D_implies_dom = subs COMP (instantiate' [SOME (ctyp_of thy idomT)]
   136                                                     [SOME (cterm_of thy D)]
   137                                                     subsetD)
   138 
   139         val D_simps = map (curry op RS D_implies_dom) f_simps
   140 
   141         val D_induct = subset_induct
   142                            |> cterm_instantiate [(cterm_of thy (Var (("D",0), fastype_of D)) ,cterm_of thy D)]
   143                            |> curry op COMP subs
   144                            |> curry op COMP (dcl |> forall_intr (cterm_of thy (Var (("z",0), idomT)))
   145                                                  |> forall_intr (cterm_of thy (Var (("x",0), idomT))))
   146 
   147         val ([tinduct'], thy2) = PureThy.add_thms [((name ^ "_" ^ D_name ^ "_induct", D_induct), [])] thy
   148         val ([tsimps'], thy3) = PureThy.add_thmss [((name ^ "_" ^ D_name ^ "_simps", D_simps), [])] thy2
   149     in
   150         thy3
   151     end
   152 *)
   153 
   154 
   155 fun fundef_setup_termination_proof name NONE thy =
   156     let
   157         val name = if name = "" then get_last_fundef thy else name
   158         val data = the (get_fundef_data name thy)
   159                    handle Option.Option => raise ERROR ("No such function definition: " ^ name)
   160 
   161         val (res as FundefMResult {termination, ...}, mutual, _) = data
   162         val goal = FundefTermination.mk_total_termination_goal data
   163     in
   164         thy |> ProofContext.init
   165             |> ProofContext.note_thmss_i [(("termination",
   166                                             [ContextRules.intro_query NONE]), [([standard termination], [])])] |> snd
   167             |> Proof.theorem_i PureThy.internalK NONE
   168               (ProofContext.theory o total_termination_afterqed name mutual) NONE ("", [])
   169               [(("", []), [(goal, [])])]
   170     end
   171   | fundef_setup_termination_proof name (SOME (dom_name, dom)) thy =
   172     let
   173         val name = if name = "" then get_last_fundef thy else name
   174         val data = the (get_fundef_data name thy)
   175         val (subs, dcl) = FundefTermination.mk_partial_termination_goal thy data dom
   176     in
   177         thy |> ProofContext.init
   178             |> Proof.theorem_i PureThy.internalK NONE (K I) NONE ("", [])
   179             [(("", []), [(subs, []), (dcl, [])])]
   180     end
   181 
   182 
   183 val add_fundef = gen_add_fundef Attrib.attribute
   184 
   185 
   186 
   187 (* congruence rules *)
   188 
   189 val cong_add = Thm.declaration_attribute (map_fundef_congs o Drule.add_rule o safe_mk_meta_eq);
   190 val cong_del = Thm.declaration_attribute (map_fundef_congs o Drule.del_rule o safe_mk_meta_eq);
   191 
   192 
   193 (* setup *)
   194 
   195 val setup = FundefData.init #> FundefCongs.init
   196         #>  Attrib.add_attributes
   197                 [("fundef_cong", Attrib.add_del_args cong_add cong_del, "declaration of congruence rule for function definitions")]
   198 
   199 
   200 val get_congs = FundefCommon.get_fundef_congs o Context.Theory
   201 
   202 
   203 (* outer syntax *)
   204 
   205 local structure P = OuterParse and K = OuterKeyword in
   206 
   207 
   208 
   209 val star = Scan.one (fn t => (OuterLex.val_of t = "*"));
   210 
   211 
   212 val attribs_with_star = P.$$$ "[" |-- P.!!! ((P.list (star >> K NONE || P.attrib >> SOME))
   213                                                >> (fn x => (map_filter I x, exists is_none x)))
   214                               --| P.$$$ "]";
   215 
   216 val opt_attribs_with_star = Scan.optional attribs_with_star ([], false);
   217 
   218 val opt_thm_name_star =
   219   Scan.optional ((P.name -- opt_attribs_with_star || (attribs_with_star >> pair "")) --| P.$$$ ":") ("", ([], false));
   220 
   221 
   222 val function_decl =
   223     Scan.repeat1 (opt_thm_name_star -- P.prop);
   224 
   225 val functionP =
   226   OuterSyntax.command "function" "define general recursive functions" K.thy_goal
   227   (((Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "sequential" -- P.$$$ ")") >> K true) false) --
   228   P.and_list1 function_decl) >> (fn (prepr, eqnss) =>
   229                                     Toplevel.print o Toplevel.theory_to_proof (add_fundef eqnss prepr)));
   230 
   231 val terminationP =
   232   OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
   233   ((Scan.optional P.name "" -- Scan.option (P.$$$ "(" |-- Scan.optional (P.name --| P.$$$ ":") "dom" -- P.term --| P.$$$ ")"))
   234        >> (fn (name,dom) =>
   235               Toplevel.print o Toplevel.theory_to_proof (fundef_setup_termination_proof name dom)));
   236 
   237 val _ = OuterSyntax.add_keywords ["sequential", "otherwise"];
   238 
   239 val _ = OuterSyntax.add_parsers [functionP];
   240 val _ = OuterSyntax.add_parsers [terminationP];
   241 
   242 
   243 end;
   244 
   245 
   246 end