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