src/HOL/Tools/Function/function.ML
author krauss
Sat Jan 02 23:18:58 2010 +0100 (2010-01-02)
changeset 34232 36a2a3029fd3
parent 34231 da4d7d40f2f9
child 34950 1f5e55eb821c
permissions -rw-r--r--
new year's resolution: reindented code in function package
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@34232
    12
  val add_function: (binding * typ option * mixfix) list ->
krauss@34232
    13
    (Attrib.binding * term) list -> Function_Common.function_config ->
krauss@34232
    14
    local_theory -> Proof.state
krauss@34230
    15
krauss@34232
    16
  val add_function_cmd: (binding * string option * mixfix) list ->
krauss@34232
    17
    (Attrib.binding * string) list -> Function_Common.function_config ->
krauss@34232
    18
    local_theory -> Proof.state
krauss@33099
    19
krauss@34232
    20
  val termination_proof : term option -> local_theory -> Proof.state
krauss@34232
    21
  val termination_proof_cmd : string option -> local_theory -> Proof.state
krauss@33099
    22
krauss@34232
    23
  val setup : theory -> theory
krauss@34232
    24
  val get_congs : Proof.context -> thm list
krauss@34230
    25
krauss@34232
    26
  val get_info : Proof.context -> term -> info
krauss@33099
    27
end
krauss@33099
    28
krauss@33099
    29
krauss@33099
    30
structure Function : FUNCTION =
krauss@33099
    31
struct
krauss@33099
    32
krauss@33099
    33
open Function_Lib
krauss@33099
    34
open Function_Common
krauss@33099
    35
krauss@33099
    36
val simp_attribs = map (Attrib.internal o K)
krauss@34232
    37
  [Simplifier.simp_add,
krauss@34232
    38
   Code.add_default_eqn_attribute,
krauss@34232
    39
   Nitpick_Simps.add]
krauss@33099
    40
krauss@33099
    41
val psimp_attribs = map (Attrib.internal o K)
krauss@34232
    42
  [Simplifier.simp_add,
krauss@34232
    43
   Nitpick_Psimps.add]
krauss@33099
    44
krauss@33099
    45
fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
krauss@33099
    46
krauss@34232
    47
fun add_simps fnames post sort extra_qualify label mod_binding moreatts
krauss@34232
    48
  simps lthy =
krauss@34232
    49
  let
krauss@34232
    50
    val spec = post simps
krauss@34232
    51
      |> map (apfst (apsnd (fn ats => moreatts @ ats)))
krauss@34232
    52
      |> map (apfst (apfst extra_qualify))
krauss@33099
    53
krauss@34232
    54
    val (saved_spec_simps, lthy) =
krauss@34232
    55
      fold_map Local_Theory.note spec lthy
krauss@33099
    56
krauss@34232
    57
    val saved_simps = maps snd saved_spec_simps
krauss@34232
    58
    val simps_by_f = sort saved_simps
krauss@33099
    59
krauss@34232
    60
    fun add_for_f fname simps =
krauss@34232
    61
      Local_Theory.note
krauss@34232
    62
        ((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps)
krauss@34232
    63
      #> snd
krauss@34232
    64
  in
krauss@34232
    65
    (saved_simps, fold2 add_for_f fnames simps_by_f lthy)
krauss@34232
    66
  end
krauss@33099
    67
krauss@33099
    68
fun gen_add_function is_external prep default_constraint fixspec eqns config lthy =
krauss@34232
    69
  let
krauss@34232
    70
    val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
krauss@34232
    71
    val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
krauss@34232
    72
    val fixes = map (apfst (apfst Binding.name_of)) fixes0;
krauss@34232
    73
    val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0;
krauss@34232
    74
    val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec
krauss@33099
    75
krauss@34232
    76
    val defname = mk_defname fixes
krauss@34232
    77
    val FunctionConfig {partials, ...} = config
krauss@33099
    78
krauss@34232
    79
    val ((goalstate, cont), lthy) =
krauss@34232
    80
      Function_Mutual.prepare_function_mutual config defname fixes eqs lthy
krauss@33099
    81
krauss@34232
    82
    fun afterqed [[proof]] lthy =
krauss@34232
    83
      let
krauss@34232
    84
        val FunctionResult {fs, R, psimps, trsimps,  simple_pinducts,
krauss@34232
    85
          termination, domintros, cases, ...} =
krauss@33099
    86
          cont (Thm.close_derivation proof)
krauss@33099
    87
krauss@34232
    88
        val fnames = map (fst o fst) fixes
krauss@34232
    89
        fun qualify n = Binding.name n
krauss@34232
    90
          |> Binding.qualify true defname
krauss@34232
    91
        val conceal_partial = if partials then I else Binding.conceal
krauss@33394
    92
krauss@34232
    93
        val addsmps = add_simps fnames post sort_cont
krauss@33099
    94
krauss@34232
    95
        val (((psimps', pinducts'), (_, [termination'])), lthy) =
krauss@34232
    96
          lthy
krauss@34232
    97
          |> addsmps (conceal_partial o Binding.qualify false "partial")
krauss@34232
    98
               "psimps" conceal_partial psimp_attribs psimps
krauss@34232
    99
          ||> fold_option (snd oo addsmps I "simps" I simp_attribs) trsimps
krauss@34232
   100
          ||>> Local_Theory.note ((conceal_partial (qualify "pinduct"),
krauss@34232
   101
                 [Attrib.internal (K (Rule_Cases.case_names cnames)),
krauss@34232
   102
                  Attrib.internal (K (Rule_Cases.consumes 1)),
krauss@34232
   103
                  Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
krauss@34232
   104
          ||>> Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination])
krauss@34232
   105
          ||> (snd o Local_Theory.note ((qualify "cases",
krauss@34232
   106
                 [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases]))
krauss@34232
   107
          ||> fold_option (snd oo curry Local_Theory.note (qualify "domintros", [])) domintros
krauss@33099
   108
krauss@34232
   109
        val info = { add_simps=addsmps, case_names=cnames, psimps=psimps',
krauss@34232
   110
          pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
krauss@34232
   111
          fs=fs, R=R, defname=defname, is_partial=true }
krauss@34230
   112
krauss@34232
   113
        val _ =
krauss@34232
   114
          if not is_external then ()
krauss@34232
   115
          else Specification.print_consts lthy (K false) (map fst fixes)
krauss@34232
   116
      in
krauss@34232
   117
        lthy
krauss@34232
   118
        |> Local_Theory.declaration false (add_function_data o morph_function_data info)
krauss@34232
   119
      end
krauss@34232
   120
  in
krauss@34232
   121
    lthy
krauss@34232
   122
    |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
krauss@34232
   123
    |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
krauss@34232
   124
  end
krauss@33099
   125
krauss@34232
   126
val add_function =
krauss@34232
   127
  gen_add_function false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)
krauss@33099
   128
val add_function_cmd = gen_add_function true Specification.read_spec "_::type"
krauss@33099
   129
krauss@33099
   130
fun gen_termination_proof prep_term raw_term_opt lthy =
krauss@34232
   131
  let
krauss@34232
   132
    val term_opt = Option.map (prep_term lthy) raw_term_opt
krauss@34232
   133
    val info = the (case term_opt of
krauss@34232
   134
                      SOME t => (import_function_data t lthy
krauss@34232
   135
                        handle Option.Option =>
krauss@34232
   136
                          error ("Not a function: " ^ quote (Syntax.string_of_term lthy t)))
krauss@34232
   137
                    | NONE => (import_last_function lthy handle Option.Option => error "Not a function"))
krauss@33099
   138
krauss@34232
   139
      val { termination, fs, R, add_simps, case_names, psimps,
krauss@34232
   140
        pinducts, defname, ...} = info
krauss@34232
   141
      val domT = domain_type (fastype_of R)
krauss@34232
   142
      val goal = HOLogic.mk_Trueprop
krauss@34232
   143
                   (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
krauss@34232
   144
      fun afterqed [[totality]] lthy =
krauss@34232
   145
        let
krauss@34232
   146
          val totality = Thm.close_derivation totality
krauss@34232
   147
          val remove_domain_condition =
krauss@34232
   148
            full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
krauss@34232
   149
          val tsimps = map remove_domain_condition psimps
krauss@34232
   150
          val tinduct = map remove_domain_condition pinducts
krauss@34230
   151
krauss@34232
   152
          fun qualify n = Binding.name n
krauss@34232
   153
            |> Binding.qualify true defname
krauss@34232
   154
        in
krauss@34232
   155
          lthy
krauss@34232
   156
          |> add_simps I "simps" I simp_attribs tsimps
krauss@34232
   157
          ||>> Local_Theory.note
krauss@34232
   158
             ((qualify "induct",
krauss@34232
   159
               [Attrib.internal (K (Rule_Cases.case_names case_names))]),
krauss@34232
   160
              tinduct)
krauss@34232
   161
          |-> (fn (simps, (_, inducts)) =>
krauss@34232
   162
            let val info' = { is_partial=false, defname=defname, add_simps=add_simps,
krauss@34232
   163
              case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts,
krauss@34232
   164
              simps=SOME simps, inducts=SOME inducts, termination=termination }
krauss@34232
   165
            in
krauss@34232
   166
              Local_Theory.declaration false (add_function_data o morph_function_data info')
krauss@34232
   167
            end)
krauss@34232
   168
        end
krauss@34232
   169
  in
krauss@34232
   170
    lthy
krauss@34232
   171
    |> ProofContext.note_thmss ""
krauss@34232
   172
       [((Binding.empty, [Context_Rules.rule_del]), [([allI], [])])] |> snd
krauss@34232
   173
    |> ProofContext.note_thmss ""
krauss@34232
   174
       [((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
krauss@34232
   175
    |> ProofContext.note_thmss ""
krauss@34232
   176
       [((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]),
krauss@34232
   177
         [([Goal.norm_result termination], [])])] |> snd
krauss@34232
   178
    |> Proof.theorem_i NONE afterqed [[(goal, [])]]
krauss@34232
   179
  end
krauss@33099
   180
wenzelm@33726
   181
val termination_proof = gen_termination_proof Syntax.check_term
wenzelm@33726
   182
val termination_proof_cmd = gen_termination_proof Syntax.read_term
krauss@33099
   183
krauss@33099
   184
krauss@33099
   185
(* Datatype hook to declare datatype congs as "function_congs" *)
krauss@33099
   186
krauss@33099
   187
krauss@33099
   188
fun add_case_cong n thy =
krauss@34232
   189
  let
krauss@34232
   190
    val cong = #case_cong (Datatype.the_info thy n)
krauss@34232
   191
      |> safe_mk_meta_eq
krauss@34232
   192
  in
krauss@34232
   193
    Context.theory_map
krauss@34232
   194
      (Function_Ctx_Tree.map_function_congs (Thm.add_thm cong)) thy
krauss@34232
   195
  end
krauss@33099
   196
krauss@33099
   197
val setup_case_cong = Datatype.interpretation (K (fold add_case_cong))
krauss@33099
   198
krauss@33099
   199
krauss@33099
   200
(* setup *)
krauss@33099
   201
krauss@33099
   202
val setup =
krauss@33099
   203
  Attrib.setup @{binding fundef_cong}
krauss@33099
   204
    (Attrib.add_del Function_Ctx_Tree.cong_add Function_Ctx_Tree.cong_del)
krauss@33099
   205
    "declaration of congruence rule for function definitions"
krauss@33099
   206
  #> setup_case_cong
krauss@33099
   207
  #> Function_Relation.setup
krauss@33099
   208
  #> Function_Common.Termination_Simps.setup
krauss@33099
   209
krauss@33099
   210
val get_congs = Function_Ctx_Tree.get_function_congs
krauss@33099
   211
krauss@34230
   212
fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t
krauss@34230
   213
  |> the_single |> snd
krauss@33099
   214
krauss@33099
   215
(* outer syntax *)
krauss@33099
   216
krauss@33099
   217
local structure P = OuterParse and K = OuterKeyword in
krauss@33099
   218
krauss@33099
   219
val _ =
krauss@33099
   220
  OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal
krauss@33099
   221
  (function_parser default_config
wenzelm@33726
   222
     >> (fn ((config, fixes), statements) => add_function_cmd fixes statements config))
krauss@33099
   223
krauss@33099
   224
val _ =
krauss@33099
   225
  OuterSyntax.local_theory_to_proof "termination" "prove termination of a recursive function" K.thy_goal
wenzelm@33726
   226
  (Scan.option P.term >> termination_proof_cmd)
krauss@33099
   227
wenzelm@33726
   228
end
krauss@33099
   229
krauss@33099
   230
krauss@33099
   231
end