src/HOL/Tools/Function/function_common.ML
author wenzelm
Sun Aug 21 20:42:26 2011 +0200 (2011-08-21)
changeset 44357 5f5649ac8235
parent 42361 23f352990944
child 45290 f599ac41e7f5
permissions -rw-r--r--
tuned Parse.group: delayed failure message;
krauss@34232
     1
(*  Title:      HOL/Tools/Function/function_common.ML
krauss@33099
     2
    Author:     Alexander Krauss, TU Muenchen
krauss@33099
     3
krauss@41114
     4
Common definitions and other infrastructure for the function package.
krauss@33099
     5
*)
krauss@33099
     6
krauss@34230
     7
signature FUNCTION_DATA =
krauss@34230
     8
sig
krauss@34230
     9
krauss@34230
    10
type info =
krauss@34230
    11
 {is_partial : bool,
krauss@34230
    12
  defname : string,
krauss@34230
    13
    (* contains no logical entities: invariant under morphisms: *)
krauss@34230
    14
  add_simps : (binding -> binding) -> string -> (binding -> binding) ->
krauss@34230
    15
    Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
krauss@34230
    16
  case_names : string list,
krauss@34230
    17
  fs : term list,
krauss@34230
    18
  R : term,
krauss@34230
    19
  psimps: thm list,
krauss@34230
    20
  pinducts: thm list,
krauss@34231
    21
  simps : thm list option,
krauss@34231
    22
  inducts : thm list option,
krauss@34232
    23
  termination: thm}
krauss@34230
    24
krauss@34230
    25
end
krauss@34230
    26
krauss@34230
    27
structure Function_Data : FUNCTION_DATA =
krauss@34230
    28
struct
krauss@34230
    29
krauss@34230
    30
type info =
krauss@34230
    31
 {is_partial : bool,
krauss@34230
    32
  defname : string,
krauss@34230
    33
    (* contains no logical entities: invariant under morphisms: *)
krauss@34230
    34
  add_simps : (binding -> binding) -> string -> (binding -> binding) ->
krauss@34230
    35
    Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
krauss@34230
    36
  case_names : string list,
krauss@34230
    37
  fs : term list,
krauss@34230
    38
  R : term,
krauss@34230
    39
  psimps: thm list,
krauss@34230
    40
  pinducts: thm list,
krauss@34231
    41
  simps : thm list option,
krauss@34231
    42
  inducts : thm list option,
krauss@34232
    43
  termination: thm}
krauss@34230
    44
krauss@34230
    45
end
krauss@34230
    46
krauss@33099
    47
structure Function_Common =
krauss@33099
    48
struct
krauss@33099
    49
krauss@34230
    50
open Function_Data
krauss@34230
    51
krauss@33099
    52
local open Function_Lib in
krauss@33099
    53
krauss@33099
    54
(* Profiling *)
krauss@33099
    55
val profile = Unsynchronized.ref false;
krauss@33099
    56
krauss@33099
    57
fun PROFILE msg = if !profile then timeap_msg msg else I
krauss@33099
    58
krauss@33099
    59
krauss@33099
    60
val acc_const_name = @{const_name accp}
krauss@33099
    61
fun mk_acc domT R =
krauss@34232
    62
  Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R 
krauss@33099
    63
krauss@33099
    64
val function_name = suffix "C"
krauss@33099
    65
val graph_name = suffix "_graph"
krauss@33099
    66
val rel_name = suffix "_rel"
krauss@33099
    67
val dom_name = suffix "_dom"
krauss@33099
    68
krauss@33099
    69
(* Termination rules *)
krauss@33099
    70
wenzelm@33519
    71
structure TerminationRule = Generic_Data
krauss@33099
    72
(
krauss@33099
    73
  type T = thm list
krauss@33099
    74
  val empty = []
krauss@33099
    75
  val extend = I
wenzelm@33519
    76
  val merge = Thm.merge_thms
krauss@33099
    77
);
krauss@33099
    78
krauss@33099
    79
val get_termination_rules = TerminationRule.get
krauss@33099
    80
val store_termination_rule = TerminationRule.map o cons
krauss@33099
    81
val apply_termination_rule = resolve_tac o get_termination_rules o Context.Proof
krauss@33099
    82
krauss@33099
    83
krauss@33099
    84
(* Function definition result data *)
krauss@33099
    85
krauss@34232
    86
datatype function_result = FunctionResult of
krauss@34232
    87
 {fs: term list,
krauss@34232
    88
  G: term,
krauss@34232
    89
  R: term,
krauss@34232
    90
  psimps : thm list,
krauss@34232
    91
  simple_pinducts : thm list,
krauss@34232
    92
  cases : thm,
krauss@34232
    93
  termination : thm,
krauss@34232
    94
  domintros : thm list option}
krauss@33099
    95
krauss@34230
    96
fun morph_function_data ({add_simps, case_names, fs, R, psimps, pinducts,
krauss@34231
    97
  simps, inducts, termination, defname, is_partial} : info) phi =
krauss@33099
    98
    let
krauss@33099
    99
      val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
krauss@33099
   100
      val name = Binding.name_of o Morphism.binding phi o Binding.name
krauss@33099
   101
    in
krauss@34230
   102
      { add_simps = add_simps, case_names = case_names,
krauss@34232
   103
        fs = map term fs, R = term R, psimps = fact psimps,
krauss@34231
   104
        pinducts = fact pinducts, simps = Option.map fact simps,
krauss@34231
   105
        inducts = Option.map fact inducts, termination = thm termination,
krauss@34230
   106
        defname = name defname, is_partial=is_partial }
krauss@33099
   107
    end
krauss@33099
   108
wenzelm@33519
   109
structure FunctionData = Generic_Data
krauss@33099
   110
(
krauss@34230
   111
  type T = (term * info) Item_Net.T;
wenzelm@33373
   112
  val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
krauss@33099
   113
  val extend = I;
wenzelm@33519
   114
  fun merge tabs : T = Item_Net.merge tabs;
krauss@34232
   115
)
krauss@33099
   116
krauss@33099
   117
val get_function = FunctionData.get o Context.Proof;
krauss@33099
   118
krauss@33099
   119
krauss@34232
   120
fun lift_morphism thy f =
krauss@34232
   121
  let
krauss@34232
   122
    val term = Drule.term_rule thy f
krauss@34232
   123
  in
krauss@34232
   124
    Morphism.thm_morphism f $> Morphism.term_morphism term
krauss@34232
   125
    $> Morphism.typ_morphism (Logic.type_map term)
krauss@34232
   126
  end
krauss@33099
   127
krauss@33099
   128
fun import_function_data t ctxt =
krauss@34232
   129
  let
wenzelm@42361
   130
    val thy = Proof_Context.theory_of ctxt
krauss@34232
   131
    val ct = cterm_of thy t
krauss@34232
   132
    val inst_morph = lift_morphism thy o Thm.instantiate
krauss@33099
   133
krauss@34232
   134
    fun match (trm, data) =
krauss@34232
   135
      SOME (morph_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct))))
krauss@34232
   136
      handle Pattern.MATCH => NONE
krauss@34232
   137
  in
krauss@34232
   138
    get_first match (Item_Net.retrieve (get_function ctxt) t)
krauss@34232
   139
  end
krauss@33099
   140
krauss@33099
   141
fun import_last_function ctxt =
krauss@34232
   142
  case Item_Net.content (get_function ctxt) of
krauss@34232
   143
    [] => NONE
krauss@34232
   144
  | (t, data) :: _ =>
krauss@34232
   145
    let
krauss@34232
   146
      val ([t'], ctxt') = Variable.import_terms true [t] ctxt
krauss@34232
   147
    in
krauss@34232
   148
      import_function_data t' ctxt'
krauss@34232
   149
    end
krauss@33099
   150
krauss@33099
   151
val all_function_data = Item_Net.content o get_function
krauss@33099
   152
krauss@34230
   153
fun add_function_data (data : info as {fs, termination, ...}) =
krauss@34232
   154
  FunctionData.map (fold (fn f => Item_Net.update (f, data)) fs)
krauss@34232
   155
  #> store_termination_rule termination
krauss@33099
   156
krauss@33099
   157
krauss@33099
   158
(* Simp rules for termination proofs *)
krauss@33099
   159
krauss@33099
   160
structure Termination_Simps = Named_Thms
krauss@33099
   161
(
krauss@34232
   162
  val name = "termination_simp"
wenzelm@38764
   163
  val description = "simplification rules for termination proofs"
krauss@34232
   164
)
krauss@33099
   165
krauss@33099
   166
krauss@33099
   167
(* Default Termination Prover *)
krauss@33099
   168
wenzelm@33519
   169
structure TerminationProver = Generic_Data
krauss@33099
   170
(
krauss@36521
   171
  type T = Proof.context -> tactic
krauss@33099
   172
  val empty = (fn _ => error "Termination prover not configured")
krauss@33099
   173
  val extend = I
wenzelm@38761
   174
  fun merge (a, _) = a
krauss@34232
   175
)
krauss@33099
   176
krauss@33099
   177
val set_termination_prover = TerminationProver.put
krauss@33099
   178
val get_termination_prover = TerminationProver.get o Context.Proof
krauss@33099
   179
krauss@33099
   180
krauss@33099
   181
(* Configuration management *)
krauss@34232
   182
datatype function_opt
krauss@33099
   183
  = Sequential
krauss@33099
   184
  | Default of string
krauss@33099
   185
  | DomIntros
krauss@33101
   186
  | No_Partials
krauss@33099
   187
krauss@34232
   188
datatype function_config = FunctionConfig of
krauss@34232
   189
 {sequential: bool,
krauss@41417
   190
  default: string option,
krauss@34232
   191
  domintros: bool,
krauss@41846
   192
  partials: bool}
krauss@33099
   193
krauss@41846
   194
fun apply_opt Sequential (FunctionConfig {sequential, default, domintros, partials}) =
krauss@41846
   195
    FunctionConfig {sequential=true, default=default, domintros=domintros, partials=partials}
krauss@41846
   196
  | apply_opt (Default d) (FunctionConfig {sequential, default, domintros, partials}) =
krauss@41846
   197
    FunctionConfig {sequential=sequential, default=SOME d, domintros=domintros, partials=partials}
krauss@41846
   198
  | apply_opt DomIntros (FunctionConfig {sequential, default, domintros, partials}) =
krauss@41846
   199
    FunctionConfig {sequential=sequential, default=default, domintros=true, partials=partials}
krauss@41846
   200
  | apply_opt No_Partials (FunctionConfig {sequential, default, domintros, partials}) =
krauss@41846
   201
    FunctionConfig {sequential=sequential, default=default, domintros=domintros, partials=false}
krauss@33099
   202
krauss@33099
   203
val default_config =
krauss@41417
   204
  FunctionConfig { sequential=false, default=NONE,
krauss@41846
   205
    domintros=false, partials=true}
krauss@33099
   206
krauss@33099
   207
krauss@33099
   208
(* Analyzing function equations *)
krauss@33099
   209
krauss@39276
   210
fun split_def ctxt check_head geq =
krauss@34232
   211
  let
krauss@34232
   212
    fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
krauss@34232
   213
    val qs = Term.strip_qnt_vars "all" geq
krauss@34232
   214
    val imp = Term.strip_qnt_body "all" geq
krauss@34232
   215
    val (gs, eq) = Logic.strip_horn imp
krauss@33099
   216
krauss@34232
   217
    val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
krauss@34232
   218
      handle TERM _ => error (input_error "Not an equation")
krauss@33099
   219
krauss@34232
   220
    val (head, args) = strip_comb f_args
krauss@33099
   221
krauss@39276
   222
    val fname = fst (dest_Free head) handle TERM _ => ""
krauss@39276
   223
    val _ = check_head fname
krauss@34232
   224
  in
krauss@34232
   225
    (fname, qs, gs, args, rhs)
krauss@34232
   226
  end
krauss@33099
   227
krauss@33099
   228
(* Check for all sorts of errors in the input *)
krauss@33099
   229
fun check_defs ctxt fixes eqs =
krauss@34232
   230
  let
krauss@34232
   231
    val fnames = map (fst o fst) fixes
krauss@34232
   232
krauss@34232
   233
    fun check geq =
krauss@34232
   234
      let
krauss@34232
   235
        fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq])
krauss@33099
   236
krauss@39276
   237
        fun check_head fname =
krauss@39276
   238
          member (op =) fnames fname orelse
krauss@39276
   239
          input_error ("Illegal equation head. Expected " ^ commas_quote fnames)
krauss@34232
   240
krauss@39276
   241
        val (fname, qs, gs, args, rhs) = split_def ctxt check_head geq
krauss@34232
   242
krauss@34232
   243
        val _ = length args > 0 orelse input_error "Function has no arguments:"
krauss@34232
   244
krauss@34232
   245
        fun add_bvs t is = add_loose_bnos (t, 0, is)
wenzelm@42081
   246
        val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs []))
wenzelm@42081
   247
                    |> map (fst o nth (rev qs))
krauss@34232
   248
krauss@34232
   249
        val _ = null rvs orelse input_error
krauss@34232
   250
          ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs ^
krauss@34232
   251
           " occur" ^ plural "s" "" rvs ^ " on right hand side only:")
krauss@34232
   252
krauss@34232
   253
        val _ = forall (not o Term.exists_subterm
haftmann@36692
   254
          (fn Free (n, _) => member (op =) fnames n | _ => false)) (gs @ args)
krauss@34232
   255
          orelse input_error "Defined function may not occur in premises or arguments"
krauss@33099
   256
krauss@34232
   257
        val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args
krauss@34232
   258
        val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs
krauss@34232
   259
        val _ = null funvars orelse (warning (cat_lines
krauss@34232
   260
          ["Bound variable" ^ plural " " "s " funvars ^
krauss@34232
   261
          commas_quote (map fst funvars) ^ " occur" ^ plural "s" "" funvars ^
krauss@34232
   262
          " in function position.", "Misspelled constructor???"]); true)
krauss@34232
   263
      in
krauss@34232
   264
        (fname, length args)
krauss@34232
   265
      end
krauss@33099
   266
krauss@34232
   267
    val grouped_args = AList.group (op =) (map check eqs)
krauss@34232
   268
    val _ = grouped_args
krauss@34232
   269
      |> map (fn (fname, ars) =>
krauss@34232
   270
        length (distinct (op =) ars) = 1
krauss@34232
   271
        orelse error ("Function " ^ quote fname ^
krauss@34232
   272
          " has different numbers of arguments in different equations"))
krauss@33099
   273
krauss@34232
   274
    val not_defined = subtract (op =) (map fst grouped_args) fnames
krauss@34232
   275
    val _ = null not_defined
krauss@34232
   276
      orelse error ("No defining equations for function" ^
krauss@34232
   277
        plural " " "s " not_defined ^ commas_quote not_defined)
krauss@33751
   278
krauss@34232
   279
    fun check_sorts ((fname, fT), _) =
wenzelm@42361
   280
      Sorts.of_sort (Sign.classes_of (Proof_Context.theory_of ctxt)) (fT, HOLogic.typeS)
krauss@34232
   281
      orelse error (cat_lines
krauss@34232
   282
      ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
wenzelm@39134
   283
       Syntax.string_of_typ (Config.put show_sorts true ctxt) fT])
krauss@33099
   284
krauss@34232
   285
    val _ = map check_sorts fixes
krauss@34232
   286
  in
krauss@34232
   287
    ()
krauss@34232
   288
  end
krauss@33099
   289
krauss@33099
   290
(* Preprocessors *)
krauss@33099
   291
krauss@33099
   292
type fixes = ((string * typ) * mixfix) list
krauss@33099
   293
type 'a spec = (Attrib.binding * 'a list) list
krauss@34232
   294
type preproc = function_config -> Proof.context -> fixes -> term spec ->
krauss@34232
   295
  (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list)
krauss@33099
   296
krauss@34232
   297
val fname_of = fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o
krauss@34232
   298
  HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all
krauss@33099
   299
krauss@33099
   300
fun mk_case_names i "" k = mk_case_names i (string_of_int (i + 1)) k
krauss@33099
   301
  | mk_case_names _ n 0 = []
krauss@33099
   302
  | mk_case_names _ n 1 = [n]
krauss@33099
   303
  | mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k)
krauss@33099
   304
krauss@33099
   305
fun empty_preproc check _ ctxt fixes spec =
krauss@34232
   306
  let
krauss@34232
   307
    val (bnds, tss) = split_list spec
krauss@34232
   308
    val ts = flat tss
krauss@34232
   309
    val _ = check ctxt fixes ts
krauss@34232
   310
    val fnames = map (fst o fst) fixes
krauss@34232
   311
    val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts
krauss@33099
   312
krauss@34232
   313
    fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) 
krauss@34232
   314
      (indices ~~ xs) |> map (map snd)
krauss@33099
   315
krauss@34232
   316
    (* using theorem names for case name currently disabled *)
krauss@34232
   317
    val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat
krauss@34232
   318
  in
krauss@34232
   319
    (ts, curry op ~~ bnds o Library.unflat tss, sort, cnames)
krauss@34232
   320
  end
krauss@33099
   321
wenzelm@33519
   322
structure Preprocessor = Generic_Data
krauss@33099
   323
(
krauss@33099
   324
  type T = preproc
krauss@33099
   325
  val empty : T = empty_preproc check_defs
krauss@33099
   326
  val extend = I
wenzelm@33519
   327
  fun merge (a, _) = a
krauss@34232
   328
)
krauss@33099
   329
krauss@33099
   330
val get_preproc = Preprocessor.get o Context.Proof
krauss@33099
   331
val set_preproc = Preprocessor.map o K
krauss@33099
   332
krauss@33099
   333
krauss@33099
   334
krauss@34232
   335
local
wenzelm@44357
   336
  val option_parser = Parse.group (fn () => "option")
wenzelm@36960
   337
    ((Parse.reserved "sequential" >> K Sequential)
wenzelm@36960
   338
     || ((Parse.reserved "default" |-- Parse.term) >> Default)
wenzelm@36960
   339
     || (Parse.reserved "domintros" >> K DomIntros)
krauss@41846
   340
     || (Parse.reserved "no_partials" >> K No_Partials))
krauss@33099
   341
krauss@34232
   342
  fun config_parser default =
wenzelm@36960
   343
    (Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 option_parser) --| Parse.$$$ ")") [])
krauss@34232
   344
     >> (fn opts => fold apply_opt opts default)
krauss@33099
   345
in
krauss@34232
   346
  fun function_parser default_cfg =
wenzelm@36960
   347
      config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_alt_specs
krauss@33099
   348
end
krauss@33099
   349
krauss@33099
   350
krauss@33099
   351
end
krauss@33099
   352
end