src/HOL/Tools/Function/fundef_common.ML
author wenzelm
Thu Jul 02 17:34:14 2009 +0200 (2009-07-02)
changeset 31902 862ae16a799d
parent 31775 2b04504fcb69
child 32603 e08fdd615333
permissions -rw-r--r--
renamed NamedThmsFun to Named_Thms;
simplified/unified names of instances of Named_Thms;
haftmann@31775
     1
(*  Title:      HOL/Tools/Function/fundef_common.ML
krauss@19564
     2
    Author:     Alexander Krauss, TU Muenchen
krauss@19564
     3
krauss@19564
     4
A package for general recursive function definitions. 
krauss@23203
     5
Common definitions and other infrastructure.
krauss@19564
     6
*)
krauss@19564
     7
krauss@19564
     8
structure FundefCommon =
krauss@19564
     9
struct
krauss@19564
    10
wenzelm@23215
    11
local open FundefLib in
wenzelm@23215
    12
krauss@22498
    13
(* Profiling *)
krauss@21255
    14
val profile = ref false;
krauss@21255
    15
krauss@21255
    16
fun PROFILE msg = if !profile then timeap_msg msg else I
krauss@21255
    17
krauss@22498
    18
krauss@26748
    19
val acc_const_name = @{const_name "accp"}
krauss@20523
    20
fun mk_acc domT R =
krauss@22733
    21
    Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R 
krauss@19564
    22
krauss@21319
    23
val function_name = suffix "C"
krauss@21319
    24
val graph_name = suffix "_graph"
krauss@21319
    25
val rel_name = suffix "_rel"
krauss@21319
    26
val dom_name = suffix "_dom"
krauss@21319
    27
krauss@28287
    28
(* Termination rules *)
krauss@28287
    29
krauss@28287
    30
structure TerminationRule = GenericDataFun
krauss@28287
    31
(
krauss@28287
    32
  type T = thm list
krauss@28287
    33
  val empty = []
krauss@28287
    34
  val extend = I
krauss@28287
    35
  fun merge _ = Thm.merge_thms
krauss@28287
    36
);
krauss@28287
    37
krauss@28287
    38
val get_termination_rules = TerminationRule.get
krauss@28287
    39
val store_termination_rule = TerminationRule.map o cons
krauss@28287
    40
val apply_termination_rule = resolve_tac o get_termination_rules o Context.Proof
krauss@28287
    41
krauss@28287
    42
krauss@28287
    43
(* Function definition result data *)
krauss@19564
    44
krauss@19583
    45
datatype fundef_result =
krauss@19583
    46
  FundefResult of
krauss@19564
    47
     {
krauss@22733
    48
      fs: term list,
krauss@20523
    49
      G: term,
krauss@20523
    50
      R: term,
krauss@19770
    51
krauss@20523
    52
      psimps : thm list, 
krauss@22166
    53
      trsimps : thm list option, 
krauss@22166
    54
krauss@19770
    55
      simple_pinducts : thm list, 
krauss@19770
    56
      cases : thm,
krauss@19770
    57
      termination : thm,
krauss@22166
    58
      domintros : thm list option
krauss@19770
    59
     }
krauss@19770
    60
krauss@22733
    61
krauss@21255
    62
datatype fundef_context_data =
krauss@21255
    63
  FundefCtxData of
krauss@21255
    64
     {
krauss@22733
    65
      defname : string,
krauss@22733
    66
krauss@23819
    67
      (* contains no logical entities: invariant under morphisms *)
krauss@30790
    68
      add_simps : (binding -> binding) -> string -> Attrib.src list -> thm list 
krauss@26529
    69
                  -> local_theory -> thm list * local_theory,
krauss@25222
    70
      case_names : string list,
krauss@19770
    71
krauss@22733
    72
      fs : term list,
krauss@21255
    73
      R : term,
krauss@21255
    74
      
krauss@21255
    75
      psimps: thm list,
krauss@21255
    76
      pinducts: thm list,
krauss@21255
    77
      termination: thm
krauss@21255
    78
     }
krauss@21255
    79
krauss@25222
    80
fun morph_fundef_data (FundefCtxData {add_simps, case_names, fs, R, 
krauss@25222
    81
                                      psimps, pinducts, termination, defname}) phi =
krauss@22623
    82
    let
krauss@22733
    83
      val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
wenzelm@30223
    84
      val name = Binding.name_of o Morphism.binding phi o Binding.name
krauss@22623
    85
    in
krauss@25222
    86
      FundefCtxData { add_simps = add_simps, case_names = case_names,
krauss@22733
    87
                      fs = map term fs, R = term R, psimps = fact psimps, 
krauss@22733
    88
                      pinducts = fact pinducts, termination = thm termination,
krauss@22733
    89
                      defname = name defname }
krauss@22623
    90
    end
krauss@22623
    91
krauss@20523
    92
structure FundefData = GenericDataFun
wenzelm@22846
    93
(
wenzelm@30560
    94
  type T = (term * fundef_context_data) Item_Net.T;
wenzelm@30560
    95
  val empty = Item_Net.init
haftmann@22760
    96
    (op aconv o pairself fst : (term * fundef_context_data) * (term * fundef_context_data) -> bool)
haftmann@22760
    97
    fst;
krauss@19564
    98
  val copy = I;
krauss@19564
    99
  val extend = I;
wenzelm@30560
   100
  fun merge _ (tab1, tab2) = Item_Net.merge (tab1, tab2)
wenzelm@22846
   101
);
krauss@19564
   102
wenzelm@30492
   103
val get_fundef = FundefData.get o Context.Proof;
wenzelm@30492
   104
krauss@19564
   105
krauss@22733
   106
(* Generally useful?? *)
krauss@22733
   107
fun lift_morphism thy f = 
krauss@22733
   108
    let 
krauss@22733
   109
      val term = Drule.term_rule thy f
krauss@22733
   110
    in
krauss@28883
   111
      Morphism.thm_morphism f $> Morphism.term_morphism term 
krauss@28883
   112
       $> Morphism.typ_morphism (Logic.type_map term)
krauss@22733
   113
    end
krauss@22733
   114
krauss@22733
   115
fun import_fundef_data t ctxt =
krauss@22733
   116
    let
wenzelm@30492
   117
      val thy = ProofContext.theory_of ctxt
krauss@22733
   118
      val ct = cterm_of thy t
krauss@22733
   119
      val inst_morph = lift_morphism thy o Thm.instantiate 
krauss@19564
   120
krauss@25201
   121
      fun match (trm, data) = 
krauss@25201
   122
          SOME (morph_fundef_data data (inst_morph (Thm.match (cterm_of thy trm, ct))))
krauss@22733
   123
          handle Pattern.MATCH => NONE
krauss@22733
   124
    in 
wenzelm@30560
   125
      get_first match (Item_Net.retrieve (get_fundef ctxt) t)
krauss@22733
   126
    end
krauss@19564
   127
krauss@22733
   128
fun import_last_fundef ctxt =
wenzelm@30560
   129
    case Item_Net.content (get_fundef ctxt) of
krauss@22733
   130
      [] => NONE
krauss@22733
   131
    | (t, data) :: _ =>
krauss@22733
   132
      let 
wenzelm@30492
   133
        val ([t'], ctxt') = Variable.import_terms true [t] ctxt
krauss@22733
   134
      in
wenzelm@30492
   135
        import_fundef_data t' ctxt'
krauss@22733
   136
      end
krauss@19564
   137
wenzelm@30560
   138
val all_fundef_data = Item_Net.content o get_fundef
krauss@21319
   139
krauss@28287
   140
fun add_fundef_data (data as FundefCtxData {fs, termination, ...}) =
wenzelm@30560
   141
    FundefData.map (fold (fn f => Item_Net.insert (f, data)) fs)
krauss@28287
   142
    #> store_termination_rule termination
krauss@28287
   143
krauss@28287
   144
krauss@28287
   145
(* Simp rules for termination proofs *)
krauss@28287
   146
wenzelm@31902
   147
structure Termination_Simps = Named_Thms
wenzelm@26989
   148
(
krauss@26749
   149
  val name = "termination_simp" 
krauss@26749
   150
  val description = "Simplification rule for termination proofs"
krauss@26749
   151
);
krauss@26749
   152
krauss@28287
   153
krauss@28287
   154
(* Default Termination Prover *)
krauss@28287
   155
krauss@28287
   156
structure TerminationProver = GenericDataFun
wenzelm@22846
   157
(
wenzelm@30510
   158
  type T = Proof.context -> Proof.method
krauss@28287
   159
  val empty = (fn _ => error "Termination prover not configured")
wenzelm@22846
   160
  val extend = I
krauss@28287
   161
  fun merge _ (a,b) = b (* FIXME *)
wenzelm@22846
   162
);
krauss@21319
   163
krauss@28287
   164
val set_termination_prover = TerminationProver.put
wenzelm@30492
   165
val get_termination_prover = TerminationProver.get o Context.Proof
krauss@22733
   166
krauss@21319
   167
krauss@20654
   168
(* Configuration management *)
krauss@20654
   169
datatype fundef_opt 
krauss@20654
   170
  = Sequential
krauss@20654
   171
  | Default of string
krauss@21319
   172
  | DomIntros
krauss@22166
   173
  | Tailrec
krauss@20654
   174
krauss@20654
   175
datatype fundef_config
krauss@20654
   176
  = FundefConfig of
krauss@20654
   177
   {
krauss@20654
   178
    sequential: bool,
krauss@20654
   179
    default: string,
krauss@22166
   180
    domintros: bool,
krauss@22166
   181
    tailrec: bool
krauss@20654
   182
   }
krauss@20654
   183
wenzelm@26989
   184
fun apply_opt Sequential (FundefConfig {sequential, default, domintros,tailrec}) = 
wenzelm@26989
   185
    FundefConfig {sequential=true, default=default, domintros=domintros, tailrec=tailrec}
wenzelm@26989
   186
  | apply_opt (Default d) (FundefConfig {sequential, default, domintros,tailrec}) = 
wenzelm@26989
   187
    FundefConfig {sequential=sequential, default=d, domintros=domintros, tailrec=tailrec}
wenzelm@26989
   188
  | apply_opt DomIntros (FundefConfig {sequential, default, domintros,tailrec}) =
wenzelm@26989
   189
    FundefConfig {sequential=sequential, default=default, domintros=true,tailrec=tailrec}
wenzelm@26989
   190
  | apply_opt Tailrec (FundefConfig {sequential, default, domintros,tailrec}) =
wenzelm@26989
   191
    FundefConfig {sequential=sequential, default=default, domintros=domintros,tailrec=true}
krauss@20654
   192
wenzelm@26989
   193
val default_config =
krauss@28883
   194
  FundefConfig { sequential=false, default="%x. undefined" (*FIXME dynamic scoping*), 
krauss@28883
   195
                 domintros=false, tailrec=false }
krauss@23819
   196
krauss@23819
   197
krauss@28287
   198
(* Analyzing function equations *)
krauss@23189
   199
krauss@24170
   200
fun split_def ctxt geq =
krauss@23189
   201
    let
wenzelm@24920
   202
      fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
krauss@28287
   203
      val qs = Term.strip_qnt_vars "all" geq
krauss@28287
   204
      val imp = Term.strip_qnt_body "all" geq
krauss@26529
   205
      val (gs, eq) = Logic.strip_horn imp
krauss@23189
   206
krauss@23189
   207
      val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
krauss@24170
   208
          handle TERM _ => error (input_error "Not an equation")
krauss@23189
   209
krauss@23189
   210
      val (head, args) = strip_comb f_args
krauss@23189
   211
krauss@23189
   212
      val fname = fst (dest_Free head)
krauss@24170
   213
          handle TERM _ => error (input_error "Head symbol must not be a bound variable")
krauss@23189
   214
    in
krauss@23189
   215
      (fname, qs, gs, args, rhs)
krauss@23189
   216
    end
krauss@23189
   217
krauss@23203
   218
(* Check for all sorts of errors in the input *)
krauss@23203
   219
fun check_defs ctxt fixes eqs =
krauss@23203
   220
    let
krauss@23203
   221
      val fnames = map (fst o fst) fixes
krauss@23203
   222
                                
krauss@23203
   223
      fun check geq = 
krauss@23203
   224
          let
krauss@28883
   225
            fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq])
krauss@23203
   226
                                  
krauss@24170
   227
            val fqgar as (fname, qs, gs, args, rhs) = split_def ctxt geq
krauss@23203
   228
                                 
krauss@23203
   229
            val _ = fname mem fnames 
krauss@28883
   230
                    orelse input_error 
krauss@28883
   231
                             ("Head symbol of left hand side must be " 
krauss@28883
   232
                              ^ plural "" "one out of " fnames ^ commas_quote fnames)
krauss@23203
   233
                                            
krauss@30832
   234
            val _ = length args > 0 orelse input_error "Function has no arguments:"
krauss@30832
   235
krauss@23203
   236
            fun add_bvs t is = add_loose_bnos (t, 0, is)
krauss@23203
   237
            val rvs = (add_bvs rhs [] \\ fold add_bvs args [])
krauss@23203
   238
                        |> map (fst o nth (rev qs))
krauss@23203
   239
                      
krauss@28883
   240
            val _ = null rvs orelse input_error 
krauss@28883
   241
                        ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
krauss@28883
   242
                         ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:")
krauss@23203
   243
                                    
krauss@28883
   244
            val _ = forall (not o Term.exists_subterm 
krauss@29922
   245
                             (fn Free (n, _) => n mem fnames | _ => false)) (gs @ args)
krauss@29922
   246
                    orelse input_error "Defined function may not occur in premises or arguments"
krauss@24171
   247
krauss@24171
   248
            val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args
krauss@24171
   249
            val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs
krauss@24171
   250
            val _ = null funvars
krauss@28883
   251
                    orelse (warning (cat_lines 
krauss@28883
   252
                    ["Bound variable" ^ plural " " "s " funvars 
krauss@28883
   253
                     ^ commas_quote (map fst funvars) ^  
krauss@28883
   254
                     " occur" ^ plural "s" "" funvars ^ " in function position.",  
krauss@28883
   255
                     "Misspelled constructor???"]); true)
krauss@23203
   256
          in
krauss@30906
   257
            (fname, length args)
krauss@23203
   258
          end
krauss@30906
   259
krauss@30906
   260
      val _ = AList.group (op =) (map check eqs)
krauss@30906
   261
        |> map (fn (fname, ars) =>
krauss@30906
   262
             length (distinct (op =) ars) = 1
krauss@30906
   263
             orelse error ("Function " ^ quote fname ^
krauss@30906
   264
                           " has different numbers of arguments in different equations"))
krauss@28884
   265
krauss@24170
   266
      fun check_sorts ((fname, fT), _) =
krauss@24170
   267
          Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS)
krauss@28883
   268
          orelse error (cat_lines 
krauss@28883
   269
          ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
krauss@28883
   270
           setmp show_sorts true (Syntax.string_of_typ ctxt) fT])
krauss@24170
   271
krauss@24170
   272
      val _ = map check_sorts fixes
krauss@23203
   273
    in
krauss@23203
   274
      ()
krauss@23203
   275
    end
krauss@23203
   276
krauss@23203
   277
(* Preprocessors *)
krauss@23203
   278
krauss@23203
   279
type fixes = ((string * typ) * mixfix) list
krauss@30790
   280
type 'a spec = (Attrib.binding * 'a list) list
krauss@30787
   281
type preproc = fundef_config -> Proof.context -> fixes -> term spec 
krauss@25222
   282
               -> (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list)
krauss@23819
   283
krauss@28883
   284
val fname_of = fst o dest_Free o fst o strip_comb o fst 
krauss@28883
   285
 o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all
krauss@23203
   286
krauss@25222
   287
fun mk_case_names i "" k = mk_case_names i (string_of_int (i + 1)) k
krauss@25222
   288
  | mk_case_names _ n 0 = []
krauss@25222
   289
  | mk_case_names _ n 1 = [n]
krauss@25222
   290
  | mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k)
krauss@25222
   291
krauss@30787
   292
fun empty_preproc check _ ctxt fixes spec =
krauss@23203
   293
    let 
krauss@30790
   294
      val (bnds, tss) = split_list spec
krauss@23819
   295
      val ts = flat tss
krauss@25222
   296
      val _ = check ctxt fixes ts
krauss@23819
   297
      val fnames = map (fst o fst) fixes
krauss@23819
   298
      val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts
krauss@23819
   299
krauss@28883
   300
      fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) 
krauss@28883
   301
                                   (indices ~~ xs)
krauss@23819
   302
                        |> map (map snd)
krauss@25222
   303
krauss@25361
   304
      (* using theorem names for case name currently disabled *)
krauss@30790
   305
      val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat
krauss@23203
   306
    in
krauss@30790
   307
      (ts, curry op ~~ bnds o Library.unflat tss, sort, cnames)
krauss@23203
   308
    end
krauss@23203
   309
krauss@23203
   310
structure Preprocessor = GenericDataFun
krauss@23203
   311
(
krauss@23203
   312
  type T = preproc
wenzelm@23206
   313
  val empty : T = empty_preproc check_defs
krauss@23203
   314
  val extend = I
krauss@23203
   315
  fun merge _ (a, _) = a
krauss@23203
   316
);
krauss@23203
   317
krauss@23203
   318
val get_preproc = Preprocessor.get o Context.Proof
krauss@23203
   319
val set_preproc = Preprocessor.map o K
krauss@23203
   320
krauss@23203
   321
krauss@23203
   322
krauss@23203
   323
local 
haftmann@25558
   324
  structure P = OuterParse and K = OuterKeyword
krauss@23203
   325
krauss@28883
   326
  val option_parser = 
krauss@28883
   327
      P.group "option" ((P.reserved "sequential" >> K Sequential)
krauss@28883
   328
                    || ((P.reserved "default" |-- P.term) >> Default)
krauss@28883
   329
                    || (P.reserved "domintros" >> K DomIntros)
krauss@28883
   330
                    || (P.reserved "tailrec" >> K Tailrec))
krauss@23203
   331
krauss@28883
   332
  fun config_parser default = 
krauss@28883
   333
      (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 option_parser) --| P.$$$ ")") [])
krauss@28883
   334
        >> (fn opts => fold apply_opt opts default)
krauss@23203
   335
in
krauss@28883
   336
  fun fundef_parser default_cfg = 
krauss@30791
   337
      config_parser default_cfg -- P.fixes -- SpecParse.where_alt_specs
krauss@23203
   338
end
krauss@23203
   339
krauss@23203
   340
wenzelm@23215
   341
end
krauss@19564
   342
end
krauss@19564
   343