src/HOL/Tools/Function/function.ML
author wenzelm
Thu May 27 17:41:27 2010 +0200 (2010-05-27)
changeset 37145 01aa36932739
parent 36960 01594f816e3a
child 37744 3daaf23b9ab4
permissions -rw-r--r--
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
krauss@33099
     1
(*  Title:      HOL/Tools/Function/fundef.ML
krauss@33099
     2
    Author:     Alexander Krauss, TU Muenchen
krauss@33099
     3
krauss@33099
     4
A package for general recursive function definitions.
krauss@33099
     5
Isar commands.
krauss@33099
     6
*)
krauss@33099
     7
krauss@33099
     8
signature FUNCTION =
krauss@33099
     9
sig
krauss@34232
    10
  include FUNCTION_DATA
krauss@34232
    11
krauss@36520
    12
  val add_function: (binding * typ option * mixfix) list ->
krauss@36520
    13
    (Attrib.binding * term) list -> Function_Common.function_config ->
krauss@36522
    14
    (Proof.context -> tactic) -> local_theory -> info * local_theory
krauss@36520
    15
krauss@36520
    16
  val add_function_cmd: (binding * string option * mixfix) list ->
krauss@36520
    17
    (Attrib.binding * string) list -> Function_Common.function_config ->
krauss@36522
    18
    (Proof.context -> tactic) -> local_theory -> info * local_theory
krauss@36520
    19
krauss@36519
    20
  val function: (binding * typ option * mixfix) list ->
krauss@34232
    21
    (Attrib.binding * term) list -> Function_Common.function_config ->
krauss@34232
    22
    local_theory -> Proof.state
krauss@34230
    23
krauss@36519
    24
  val function_cmd: (binding * string option * mixfix) list ->
krauss@34232
    25
    (Attrib.binding * string) list -> Function_Common.function_config ->
krauss@34232
    26
    local_theory -> Proof.state
krauss@33099
    27
krauss@36547
    28
  val prove_termination: term option -> tactic -> local_theory -> 
krauss@36547
    29
    info * local_theory
krauss@36547
    30
  val prove_termination_cmd: string option -> tactic -> local_theory ->
krauss@36547
    31
    info * local_theory
krauss@36520
    32
krauss@36519
    33
  val termination : term option -> local_theory -> Proof.state
krauss@36519
    34
  val termination_cmd : string option -> local_theory -> Proof.state
krauss@33099
    35
krauss@34232
    36
  val setup : theory -> theory
krauss@34232
    37
  val get_congs : Proof.context -> thm list
krauss@34230
    38
krauss@34232
    39
  val get_info : Proof.context -> term -> info
krauss@33099
    40
end
krauss@33099
    41
krauss@33099
    42
krauss@33099
    43
structure Function : FUNCTION =
krauss@33099
    44
struct
krauss@33099
    45
krauss@33099
    46
open Function_Lib
krauss@33099
    47
open Function_Common
krauss@33099
    48
krauss@33099
    49
val simp_attribs = map (Attrib.internal o K)
krauss@34232
    50
  [Simplifier.simp_add,
krauss@34232
    51
   Code.add_default_eqn_attribute,
krauss@34232
    52
   Nitpick_Simps.add]
krauss@33099
    53
krauss@33099
    54
val psimp_attribs = map (Attrib.internal o K)
krauss@34232
    55
  [Simplifier.simp_add,
krauss@34232
    56
   Nitpick_Psimps.add]
krauss@33099
    57
krauss@33099
    58
fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
krauss@33099
    59
krauss@34232
    60
fun add_simps fnames post sort extra_qualify label mod_binding moreatts
krauss@34232
    61
  simps lthy =
krauss@34232
    62
  let
krauss@34232
    63
    val spec = post simps
krauss@34232
    64
      |> map (apfst (apsnd (fn ats => moreatts @ ats)))
krauss@34232
    65
      |> map (apfst (apfst extra_qualify))
krauss@33099
    66
krauss@34232
    67
    val (saved_spec_simps, lthy) =
krauss@34232
    68
      fold_map Local_Theory.note spec lthy
krauss@33099
    69
krauss@34232
    70
    val saved_simps = maps snd saved_spec_simps
krauss@34232
    71
    val simps_by_f = sort saved_simps
krauss@33099
    72
krauss@34232
    73
    fun add_for_f fname simps =
krauss@34232
    74
      Local_Theory.note
krauss@34232
    75
        ((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps)
krauss@34232
    76
      #> snd
krauss@34232
    77
  in
krauss@34232
    78
    (saved_simps, fold2 add_for_f fnames simps_by_f lthy)
krauss@34232
    79
  end
krauss@33099
    80
krauss@36518
    81
fun prepare_function is_external prep default_constraint fixspec eqns config lthy =
krauss@34232
    82
  let
krauss@34232
    83
    val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
krauss@34232
    84
    val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
krauss@34232
    85
    val fixes = map (apfst (apfst Binding.name_of)) fixes0;
krauss@34232
    86
    val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0;
krauss@34232
    87
    val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec
krauss@33099
    88
krauss@34232
    89
    val defname = mk_defname fixes
krauss@34232
    90
    val FunctionConfig {partials, ...} = config
krauss@33099
    91
krauss@36519
    92
    val ((goal_state, cont), lthy') =
krauss@34232
    93
      Function_Mutual.prepare_function_mutual config defname fixes eqs lthy
krauss@33099
    94
krauss@34232
    95
    fun afterqed [[proof]] lthy =
krauss@34232
    96
      let
bulwahn@35756
    97
        val FunctionResult {fs, R, psimps, trsimps, simple_pinducts,
krauss@34232
    98
          termination, domintros, cases, ...} =
krauss@33099
    99
          cont (Thm.close_derivation proof)
krauss@33099
   100
krauss@34232
   101
        val fnames = map (fst o fst) fixes
krauss@34232
   102
        fun qualify n = Binding.name n
krauss@34232
   103
          |> Binding.qualify true defname
krauss@34232
   104
        val conceal_partial = if partials then I else Binding.conceal
krauss@33394
   105
krauss@34232
   106
        val addsmps = add_simps fnames post sort_cont
krauss@33099
   107
krauss@34232
   108
        val (((psimps', pinducts'), (_, [termination'])), lthy) =
krauss@34232
   109
          lthy
krauss@34232
   110
          |> addsmps (conceal_partial o Binding.qualify false "partial")
krauss@34232
   111
               "psimps" conceal_partial psimp_attribs psimps
krauss@34232
   112
          ||> fold_option (snd oo addsmps I "simps" I simp_attribs) trsimps
bulwahn@35756
   113
          ||> fold_option (Spec_Rules.add Spec_Rules.Equational o pair fs) trsimps
krauss@34232
   114
          ||>> Local_Theory.note ((conceal_partial (qualify "pinduct"),
krauss@34232
   115
                 [Attrib.internal (K (Rule_Cases.case_names cnames)),
krauss@34232
   116
                  Attrib.internal (K (Rule_Cases.consumes 1)),
krauss@34232
   117
                  Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
krauss@34232
   118
          ||>> Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination])
krauss@34232
   119
          ||> (snd o Local_Theory.note ((qualify "cases",
krauss@34232
   120
                 [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases]))
krauss@34232
   121
          ||> fold_option (snd oo curry Local_Theory.note (qualify "domintros", [])) domintros
krauss@33099
   122
krauss@34232
   123
        val info = { add_simps=addsmps, case_names=cnames, psimps=psimps',
krauss@34232
   124
          pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
krauss@34232
   125
          fs=fs, R=R, defname=defname, is_partial=true }
krauss@34230
   126
krauss@34232
   127
        val _ =
krauss@34232
   128
          if not is_external then ()
krauss@34232
   129
          else Specification.print_consts lthy (K false) (map fst fixes)
krauss@34232
   130
      in
krauss@36522
   131
        (info, 
krauss@36522
   132
         lthy |> Local_Theory.declaration false (add_function_data o morph_function_data info))
krauss@34232
   133
      end
krauss@36520
   134
  in
krauss@36519
   135
    ((goal_state, afterqed), lthy')
krauss@36518
   136
  end
krauss@36518
   137
krauss@36520
   138
fun gen_add_function is_external prep default_constraint fixspec eqns config tac lthy =
krauss@36520
   139
  let
krauss@36520
   140
    val ((goal_state, afterqed), lthy') =
krauss@36520
   141
      prepare_function is_external prep default_constraint fixspec eqns config lthy
krauss@36520
   142
    val pattern_thm =
krauss@36520
   143
      case SINGLE (tac lthy') goal_state of
krauss@36520
   144
        NONE => error "pattern completeness and compatibility proof failed"
krauss@36520
   145
      | SOME st => Goal.finish lthy' st
krauss@36520
   146
  in
krauss@36520
   147
    lthy'
krauss@36520
   148
    |> afterqed [[pattern_thm]]
krauss@36520
   149
  end
krauss@36520
   150
krauss@36520
   151
val add_function =
wenzelm@37145
   152
  gen_add_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
krauss@36520
   153
val add_function_cmd = gen_add_function true Specification.read_spec "_::type"
krauss@36520
   154
krauss@36519
   155
fun gen_function is_external prep default_constraint fixspec eqns config lthy =
krauss@36518
   156
  let
krauss@36520
   157
    val ((goal_state, afterqed), lthy') =
krauss@36518
   158
      prepare_function is_external prep default_constraint fixspec eqns config lthy
krauss@34232
   159
  in
krauss@36518
   160
    lthy'
krauss@36522
   161
    |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (concl_of goal_state), [])]]
krauss@36519
   162
    |> Proof.refine (Method.primitive_text (K goal_state)) |> Seq.hd
krauss@34232
   163
  end
krauss@33099
   164
krauss@36519
   165
val function =
wenzelm@37145
   166
  gen_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
krauss@36519
   167
val function_cmd = gen_function true Specification.read_spec "_::type"
krauss@36520
   168
krauss@36518
   169
fun prepare_termination_proof prep_term raw_term_opt lthy =
krauss@34232
   170
  let
krauss@34232
   171
    val term_opt = Option.map (prep_term lthy) raw_term_opt
krauss@34232
   172
    val info = the (case term_opt of
krauss@34232
   173
                      SOME t => (import_function_data t lthy
krauss@34232
   174
                        handle Option.Option =>
krauss@34232
   175
                          error ("Not a function: " ^ quote (Syntax.string_of_term lthy t)))
krauss@34232
   176
                    | NONE => (import_last_function lthy handle Option.Option => error "Not a function"))
krauss@33099
   177
krauss@34232
   178
      val { termination, fs, R, add_simps, case_names, psimps,
krauss@34232
   179
        pinducts, defname, ...} = info
krauss@34232
   180
      val domT = domain_type (fastype_of R)
krauss@34232
   181
      val goal = HOLogic.mk_Trueprop
krauss@34232
   182
                   (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
krauss@34232
   183
      fun afterqed [[totality]] lthy =
krauss@34232
   184
        let
krauss@34232
   185
          val totality = Thm.close_derivation totality
krauss@34232
   186
          val remove_domain_condition =
wenzelm@35410
   187
            full_simplify (HOL_basic_ss addsimps [totality, @{thm True_implies_equals}])
krauss@34232
   188
          val tsimps = map remove_domain_condition psimps
krauss@34232
   189
          val tinduct = map remove_domain_condition pinducts
krauss@34230
   190
krauss@34232
   191
          fun qualify n = Binding.name n
krauss@34232
   192
            |> Binding.qualify true defname
krauss@34232
   193
        in
krauss@34232
   194
          lthy
krauss@34232
   195
          |> add_simps I "simps" I simp_attribs tsimps
krauss@34232
   196
          ||>> Local_Theory.note
krauss@34232
   197
             ((qualify "induct",
krauss@34232
   198
               [Attrib.internal (K (Rule_Cases.case_names case_names))]),
krauss@34232
   199
              tinduct)
krauss@36547
   200
          |-> (fn (simps, (_, inducts)) => fn lthy =>
krauss@34232
   201
            let val info' = { is_partial=false, defname=defname, add_simps=add_simps,
krauss@34232
   202
              case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts,
krauss@34232
   203
              simps=SOME simps, inducts=SOME inducts, termination=termination }
krauss@34232
   204
            in
krauss@36547
   205
              (info',
krauss@36547
   206
               lthy 
krauss@36547
   207
               |> Local_Theory.declaration false (add_function_data o morph_function_data info')
krauss@36547
   208
               |> Spec_Rules.add Spec_Rules.Equational (fs, tsimps))
krauss@34232
   209
            end)
krauss@34232
   210
        end
krauss@34232
   211
  in
krauss@36518
   212
    (goal, afterqed, termination)
krauss@36518
   213
  end
krauss@36518
   214
krauss@36520
   215
fun gen_prove_termination prep_term raw_term_opt tac lthy =
krauss@36520
   216
  let
krauss@36520
   217
    val (goal, afterqed, termination) =
krauss@36520
   218
      prepare_termination_proof prep_term raw_term_opt lthy
krauss@36520
   219
krauss@36520
   220
    val totality = Goal.prove lthy [] [] goal (K tac)
krauss@36520
   221
  in
krauss@36520
   222
    afterqed [[totality]] lthy
krauss@36520
   223
end
krauss@36520
   224
krauss@36520
   225
val prove_termination = gen_prove_termination Syntax.check_term
krauss@36520
   226
val prove_termination_cmd = gen_prove_termination Syntax.read_term
krauss@36520
   227
krauss@36519
   228
fun gen_termination prep_term raw_term_opt lthy =
krauss@36518
   229
  let
krauss@36518
   230
    val (goal, afterqed, termination) = prepare_termination_proof prep_term raw_term_opt lthy
krauss@36518
   231
  in
krauss@34232
   232
    lthy
krauss@34232
   233
    |> ProofContext.note_thmss ""
krauss@34232
   234
       [((Binding.empty, [Context_Rules.rule_del]), [([allI], [])])] |> snd
krauss@34232
   235
    |> ProofContext.note_thmss ""
krauss@34232
   236
       [((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
krauss@34232
   237
    |> ProofContext.note_thmss ""
krauss@34232
   238
       [((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]),
krauss@34232
   239
         [([Goal.norm_result termination], [])])] |> snd
krauss@36547
   240
    |> Proof.theorem NONE (snd oo afterqed) [[(goal, [])]]
krauss@34232
   241
  end
krauss@33099
   242
krauss@36519
   243
val termination = gen_termination Syntax.check_term
krauss@36519
   244
val termination_cmd = gen_termination Syntax.read_term
krauss@33099
   245
krauss@33099
   246
krauss@33099
   247
(* Datatype hook to declare datatype congs as "function_congs" *)
krauss@33099
   248
krauss@33099
   249
krauss@33099
   250
fun add_case_cong n thy =
krauss@34232
   251
  let
krauss@34232
   252
    val cong = #case_cong (Datatype.the_info thy n)
krauss@34232
   253
      |> safe_mk_meta_eq
krauss@34232
   254
  in
krauss@34232
   255
    Context.theory_map
krauss@34232
   256
      (Function_Ctx_Tree.map_function_congs (Thm.add_thm cong)) thy
krauss@34232
   257
  end
krauss@33099
   258
krauss@33099
   259
val setup_case_cong = Datatype.interpretation (K (fold add_case_cong))
krauss@33099
   260
krauss@33099
   261
krauss@33099
   262
(* setup *)
krauss@33099
   263
krauss@33099
   264
val setup =
krauss@33099
   265
  Attrib.setup @{binding fundef_cong}
krauss@33099
   266
    (Attrib.add_del Function_Ctx_Tree.cong_add Function_Ctx_Tree.cong_del)
krauss@33099
   267
    "declaration of congruence rule for function definitions"
krauss@33099
   268
  #> setup_case_cong
krauss@33099
   269
  #> Function_Relation.setup
krauss@33099
   270
  #> Function_Common.Termination_Simps.setup
krauss@33099
   271
krauss@33099
   272
val get_congs = Function_Ctx_Tree.get_function_congs
krauss@33099
   273
krauss@34230
   274
fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t
krauss@34230
   275
  |> the_single |> snd
krauss@33099
   276
wenzelm@36960
   277
krauss@33099
   278
(* outer syntax *)
krauss@33099
   279
krauss@33099
   280
val _ =
wenzelm@36960
   281
  Outer_Syntax.local_theory_to_proof "function" "define general recursive functions"
wenzelm@36960
   282
  Keyword.thy_goal
krauss@33099
   283
  (function_parser default_config
krauss@36519
   284
     >> (fn ((config, fixes), statements) => function_cmd fixes statements config))
krauss@33099
   285
krauss@33099
   286
val _ =
wenzelm@36960
   287
  Outer_Syntax.local_theory_to_proof "termination" "prove termination of a recursive function"
wenzelm@36960
   288
  Keyword.thy_goal
wenzelm@36960
   289
  (Scan.option Parse.term >> termination_cmd)
krauss@33099
   290
krauss@33099
   291
krauss@33099
   292
end