src/HOL/Tools/Function/function_core.ML
author wenzelm
Fri Nov 13 21:11:15 2009 +0100 (2009-11-13)
changeset 33671 4b0f2599ed48
parent 33669 ae9a2ea9a989
child 33766 c679f05600cd
permissions -rw-r--r--
modernized structure Local_Theory;
krauss@33099
     1
(*  Title:      HOL/Tools/Function/function_core.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
Main functionality.
krauss@33099
     6
*)
krauss@33099
     7
krauss@33099
     8
signature FUNCTION_CORE =
krauss@33099
     9
sig
krauss@33099
    10
    val trace: bool Unsynchronized.ref
krauss@33099
    11
krauss@33099
    12
    val prepare_function : Function_Common.function_config
krauss@33099
    13
                         -> string (* defname *)
krauss@33099
    14
                         -> ((bstring * typ) * mixfix) list (* defined symbol *)
krauss@33099
    15
                         -> ((bstring * typ) list * term list * term * term) list (* specification *)
krauss@33099
    16
                         -> local_theory
krauss@33099
    17
krauss@33099
    18
                         -> (term   (* f *)
krauss@33099
    19
                             * thm  (* goalstate *)
krauss@33099
    20
                             * (thm -> Function_Common.function_result) (* continuation *)
krauss@33099
    21
                            ) * local_theory
krauss@33099
    22
krauss@33099
    23
end
krauss@33099
    24
krauss@33099
    25
structure Function_Core : FUNCTION_CORE =
krauss@33099
    26
struct
krauss@33099
    27
krauss@33099
    28
val trace = Unsynchronized.ref false;
krauss@33099
    29
fun trace_msg msg = if ! trace then tracing (msg ()) else ();
krauss@33099
    30
krauss@33099
    31
val boolT = HOLogic.boolT
krauss@33099
    32
val mk_eq = HOLogic.mk_eq
krauss@33099
    33
krauss@33099
    34
open Function_Lib
krauss@33099
    35
open Function_Common
krauss@33099
    36
krauss@33099
    37
datatype globals =
krauss@33099
    38
   Globals of {
krauss@33099
    39
         fvar: term,
krauss@33099
    40
         domT: typ,
krauss@33099
    41
         ranT: typ,
krauss@33099
    42
         h: term,
krauss@33099
    43
         y: term,
krauss@33099
    44
         x: term,
krauss@33099
    45
         z: term,
krauss@33099
    46
         a: term,
krauss@33099
    47
         P: term,
krauss@33099
    48
         D: term,
krauss@33099
    49
         Pbool:term
krauss@33099
    50
}
krauss@33099
    51
krauss@33099
    52
krauss@33099
    53
datatype rec_call_info =
krauss@33099
    54
  RCInfo of
krauss@33099
    55
  {
krauss@33099
    56
   RIvs: (string * typ) list,  (* Call context: fixes and assumes *)
krauss@33099
    57
   CCas: thm list,
krauss@33099
    58
   rcarg: term,                 (* The recursive argument *)
krauss@33099
    59
krauss@33099
    60
   llRI: thm,
krauss@33099
    61
   h_assum: term
krauss@33099
    62
  }
krauss@33099
    63
krauss@33099
    64
krauss@33099
    65
datatype clause_context =
krauss@33099
    66
  ClauseContext of
krauss@33099
    67
  {
krauss@33099
    68
    ctxt : Proof.context,
krauss@33099
    69
krauss@33099
    70
    qs : term list,
krauss@33099
    71
    gs : term list,
krauss@33099
    72
    lhs: term,
krauss@33099
    73
    rhs: term,
krauss@33099
    74
krauss@33099
    75
    cqs: cterm list,
krauss@33099
    76
    ags: thm list,
krauss@33099
    77
    case_hyp : thm
krauss@33099
    78
  }
krauss@33099
    79
krauss@33099
    80
krauss@33099
    81
fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) =
krauss@33099
    82
    ClauseContext { ctxt = ProofContext.transfer thy ctxt,
krauss@33099
    83
                    qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp }
krauss@33099
    84
krauss@33099
    85
krauss@33099
    86
datatype clause_info =
krauss@33099
    87
  ClauseInfo of
krauss@33099
    88
     {
krauss@33099
    89
      no: int,
krauss@33099
    90
      qglr : ((string * typ) list * term list * term * term),
krauss@33099
    91
      cdata : clause_context,
krauss@33099
    92
krauss@33099
    93
      tree: Function_Ctx_Tree.ctx_tree,
krauss@33099
    94
      lGI: thm,
krauss@33099
    95
      RCs: rec_call_info list
krauss@33099
    96
     }
krauss@33099
    97
krauss@33099
    98
krauss@33099
    99
(* Theory dependencies. *)
krauss@33099
   100
val Pair_inject = @{thm Product_Type.Pair_inject};
krauss@33099
   101
krauss@33099
   102
val acc_induct_rule = @{thm accp_induct_rule};
krauss@33099
   103
krauss@33099
   104
val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence};
krauss@33099
   105
val ex1_implies_un = @{thm FunDef.fundef_ex1_uniqueness};
krauss@33099
   106
val ex1_implies_iff = @{thm FunDef.fundef_ex1_iff};
krauss@33099
   107
krauss@33099
   108
val acc_downward = @{thm accp_downward};
krauss@33099
   109
val accI = @{thm accp.accI};
krauss@33099
   110
val case_split = @{thm HOL.case_split};
krauss@33099
   111
val fundef_default_value = @{thm FunDef.fundef_default_value};
krauss@33099
   112
val not_acc_down = @{thm not_accp_down};
krauss@33099
   113
krauss@33099
   114
krauss@33099
   115
krauss@33099
   116
fun find_calls tree =
krauss@33099
   117
    let
krauss@33099
   118
      fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) = ([], (fixes, assumes, arg) :: xs)
krauss@33099
   119
        | add_Ri _ _ _ _ = raise Match
krauss@33099
   120
    in
krauss@33099
   121
      rev (Function_Ctx_Tree.traverse_tree add_Ri tree [])
krauss@33099
   122
    end
krauss@33099
   123
krauss@33099
   124
krauss@33099
   125
(** building proof obligations *)
krauss@33099
   126
krauss@33099
   127
fun mk_compat_proof_obligations domT ranT fvar f glrs =
krauss@33099
   128
    let
krauss@33099
   129
      fun mk_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
krauss@33099
   130
          let
krauss@33099
   131
            val shift = incr_boundvars (length qs')
krauss@33099
   132
          in
krauss@33099
   133
            Logic.mk_implies
krauss@33099
   134
              (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'),
krauss@33099
   135
                HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs'))
krauss@33099
   136
              |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
krauss@33099
   137
              |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs')
krauss@33099
   138
              |> curry abstract_over fvar
krauss@33099
   139
              |> curry subst_bound f
krauss@33099
   140
          end
krauss@33099
   141
    in
krauss@33099
   142
      map mk_impl (unordered_pairs glrs)
krauss@33099
   143
    end
krauss@33099
   144
krauss@33099
   145
krauss@33099
   146
fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs =
krauss@33099
   147
    let
krauss@33099
   148
        fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) =
krauss@33099
   149
            HOLogic.mk_Trueprop Pbool
krauss@33099
   150
                     |> curry Logic.mk_implies (HOLogic.mk_Trueprop (mk_eq (x, lhs)))
krauss@33099
   151
                     |> fold_rev (curry Logic.mk_implies) gs
krauss@33099
   152
                     |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
krauss@33099
   153
    in
krauss@33099
   154
        HOLogic.mk_Trueprop Pbool
krauss@33099
   155
                 |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs)
krauss@33099
   156
                 |> mk_forall_rename ("x", x)
krauss@33099
   157
                 |> mk_forall_rename ("P", Pbool)
krauss@33099
   158
    end
krauss@33099
   159
krauss@33099
   160
(** making a context with it's own local bindings **)
krauss@33099
   161
krauss@33099
   162
fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) =
krauss@33099
   163
    let
krauss@33099
   164
      val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt
krauss@33099
   165
                                           |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
krauss@33099
   166
krauss@33099
   167
      val thy = ProofContext.theory_of ctxt'
krauss@33099
   168
krauss@33099
   169
      fun inst t = subst_bounds (rev qs, t)
krauss@33099
   170
      val gs = map inst pre_gs
krauss@33099
   171
      val lhs = inst pre_lhs
krauss@33099
   172
      val rhs = inst pre_rhs
krauss@33099
   173
krauss@33099
   174
      val cqs = map (cterm_of thy) qs
krauss@33099
   175
      val ags = map (assume o cterm_of thy) gs
krauss@33099
   176
krauss@33099
   177
      val case_hyp = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
krauss@33099
   178
    in
krauss@33099
   179
      ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
krauss@33099
   180
                      cqs = cqs, ags = ags, case_hyp = case_hyp }
krauss@33099
   181
    end
krauss@33099
   182
krauss@33099
   183
krauss@33099
   184
(* lowlevel term function. FIXME: remove *)
krauss@33099
   185
fun abstract_over_list vs body =
krauss@33099
   186
  let
krauss@33099
   187
    fun abs lev v tm =
krauss@33099
   188
      if v aconv tm then Bound lev
krauss@33099
   189
      else
krauss@33099
   190
        (case tm of
krauss@33099
   191
          Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t)
krauss@33099
   192
        | t $ u => abs lev v t $ abs lev v u
krauss@33099
   193
        | t => t);
krauss@33099
   194
  in
krauss@33099
   195
    fold_index (fn (i, v) => fn t => abs i v t) vs body
krauss@33099
   196
  end
krauss@33099
   197
krauss@33099
   198
krauss@33099
   199
krauss@33099
   200
fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms =
krauss@33099
   201
    let
krauss@33099
   202
        val Globals {h, fvar, x, ...} = globals
krauss@33099
   203
krauss@33099
   204
        val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
krauss@33099
   205
        val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
krauss@33099
   206
krauss@33099
   207
        (* Instantiate the GIntro thm with "f" and import into the clause context. *)
krauss@33099
   208
        val lGI = GIntro_thm
krauss@33099
   209
                    |> forall_elim (cert f)
krauss@33099
   210
                    |> fold forall_elim cqs
krauss@33099
   211
                    |> fold Thm.elim_implies ags
krauss@33099
   212
krauss@33099
   213
        fun mk_call_info (rcfix, rcassm, rcarg) RI =
krauss@33099
   214
            let
krauss@33099
   215
                val llRI = RI
krauss@33099
   216
                             |> fold forall_elim cqs
krauss@33099
   217
                             |> fold (forall_elim o cert o Free) rcfix
krauss@33099
   218
                             |> fold Thm.elim_implies ags
krauss@33099
   219
                             |> fold Thm.elim_implies rcassm
krauss@33099
   220
krauss@33099
   221
                val h_assum =
krauss@33099
   222
                    HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg))
krauss@33099
   223
                              |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
krauss@33099
   224
                              |> fold_rev (Logic.all o Free) rcfix
krauss@33099
   225
                              |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] []
krauss@33099
   226
                              |> abstract_over_list (rev qs)
krauss@33099
   227
            in
krauss@33099
   228
                RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum}
krauss@33099
   229
            end
krauss@33099
   230
krauss@33099
   231
        val RC_infos = map2 mk_call_info RCs RIntro_thms
krauss@33099
   232
    in
krauss@33099
   233
        ClauseInfo
krauss@33099
   234
            {
krauss@33099
   235
             no=no,
krauss@33099
   236
             cdata=cdata,
krauss@33099
   237
             qglr=qglr,
krauss@33099
   238
krauss@33099
   239
             lGI=lGI,
krauss@33099
   240
             RCs=RC_infos,
krauss@33099
   241
             tree=tree
krauss@33099
   242
            }
krauss@33099
   243
    end
krauss@33099
   244
krauss@33099
   245
krauss@33099
   246
krauss@33099
   247
krauss@33099
   248
krauss@33099
   249
krauss@33099
   250
krauss@33099
   251
(* replace this by a table later*)
krauss@33099
   252
fun store_compat_thms 0 thms = []
krauss@33099
   253
  | store_compat_thms n thms =
krauss@33099
   254
    let
krauss@33099
   255
        val (thms1, thms2) = chop n thms
krauss@33099
   256
    in
krauss@33099
   257
        (thms1 :: store_compat_thms (n - 1) thms2)
krauss@33099
   258
    end
krauss@33099
   259
krauss@33099
   260
(* expects i <= j *)
krauss@33099
   261
fun lookup_compat_thm i j cts =
krauss@33099
   262
    nth (nth cts (i - 1)) (j - i)
krauss@33099
   263
krauss@33099
   264
(* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *)
krauss@33099
   265
(* if j < i, then turn around *)
krauss@33099
   266
fun get_compat_thm thy cts i j ctxi ctxj =
krauss@33099
   267
    let
krauss@33099
   268
      val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
krauss@33099
   269
      val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
krauss@33099
   270
krauss@33099
   271
      val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))
krauss@33099
   272
    in if j < i then
krauss@33099
   273
         let
krauss@33099
   274
           val compat = lookup_compat_thm j i cts
krauss@33099
   275
         in
krauss@33099
   276
           compat         (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
krauss@33099
   277
                |> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
krauss@33099
   278
                |> fold Thm.elim_implies agsj
krauss@33099
   279
                |> fold Thm.elim_implies agsi
krauss@33099
   280
                |> Thm.elim_implies ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
krauss@33099
   281
         end
krauss@33099
   282
       else
krauss@33099
   283
         let
krauss@33099
   284
           val compat = lookup_compat_thm i j cts
krauss@33099
   285
         in
krauss@33099
   286
               compat        (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
krauss@33099
   287
                 |> fold forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
krauss@33099
   288
                 |> fold Thm.elim_implies agsi
krauss@33099
   289
                 |> fold Thm.elim_implies agsj
krauss@33099
   290
                 |> Thm.elim_implies (assume lhsi_eq_lhsj)
krauss@33099
   291
                 |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
krauss@33099
   292
         end
krauss@33099
   293
    end
krauss@33099
   294
krauss@33099
   295
krauss@33099
   296
krauss@33099
   297
krauss@33099
   298
(* Generates the replacement lemma in fully quantified form. *)
krauss@33099
   299
fun mk_replacement_lemma thy h ih_elim clause =
krauss@33099
   300
    let
krauss@33099
   301
        val ClauseInfo {cdata=ClauseContext {qs, lhs, rhs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause
krauss@33099
   302
        local open Conv in
krauss@33099
   303
        val ih_conv = arg1_conv o arg_conv o arg_conv
krauss@33099
   304
        end
krauss@33099
   305
krauss@33099
   306
        val ih_elim_case = Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_elim
krauss@33099
   307
krauss@33099
   308
        val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
krauss@33099
   309
        val h_assums = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
krauss@33099
   310
krauss@33099
   311
        val (eql, _) = Function_Ctx_Tree.rewrite_by_tree thy h ih_elim_case (Ris ~~ h_assums) tree
krauss@33099
   312
krauss@33099
   313
        val replace_lemma = (eql RS meta_eq_to_obj_eq)
krauss@33099
   314
                                |> implies_intr (cprop_of case_hyp)
krauss@33099
   315
                                |> fold_rev (implies_intr o cprop_of) h_assums
krauss@33099
   316
                                |> fold_rev (implies_intr o cprop_of) ags
krauss@33099
   317
                                |> fold_rev forall_intr cqs
krauss@33099
   318
                                |> Thm.close_derivation
krauss@33099
   319
    in
krauss@33099
   320
      replace_lemma
krauss@33099
   321
    end
krauss@33099
   322
krauss@33099
   323
krauss@33099
   324
fun mk_uniqueness_clause thy globals f compat_store clausei clausej RLj =
krauss@33099
   325
    let
krauss@33099
   326
        val Globals {h, y, x, fvar, ...} = globals
krauss@33099
   327
        val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei
krauss@33099
   328
        val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej
krauss@33099
   329
krauss@33099
   330
        val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...}
krauss@33099
   331
            = mk_clause_context x ctxti cdescj
krauss@33099
   332
krauss@33099
   333
        val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
krauss@33099
   334
        val compat = get_compat_thm thy compat_store i j cctxi cctxj
krauss@33099
   335
        val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
krauss@33099
   336
krauss@33099
   337
        val RLj_import =
krauss@33099
   338
            RLj |> fold forall_elim cqsj'
krauss@33099
   339
                |> fold Thm.elim_implies agsj'
krauss@33099
   340
                |> fold Thm.elim_implies Ghsj'
krauss@33099
   341
krauss@33099
   342
        val y_eq_rhsj'h = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
krauss@33099
   343
        val lhsi_eq_lhsj' = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
krauss@33099
   344
    in
krauss@33099
   345
        (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
krauss@33099
   346
        |> implies_elim RLj_import (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
krauss@33099
   347
        |> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
krauss@33099
   348
        |> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
krauss@33099
   349
        |> fold_rev (implies_intr o cprop_of) Ghsj'
krauss@33099
   350
        |> fold_rev (implies_intr o cprop_of) agsj' (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)
krauss@33099
   351
        |> implies_intr (cprop_of y_eq_rhsj'h)
krauss@33099
   352
        |> implies_intr (cprop_of lhsi_eq_lhsj')
krauss@33099
   353
        |> fold_rev forall_intr (cterm_of thy h :: cqsj')
krauss@33099
   354
    end
krauss@33099
   355
krauss@33099
   356
krauss@33099
   357
krauss@33099
   358
fun mk_uniqueness_case ctxt thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
krauss@33099
   359
    let
krauss@33099
   360
        val Globals {x, y, ranT, fvar, ...} = globals
krauss@33099
   361
        val ClauseInfo {cdata = ClauseContext {lhs, rhs, qs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
krauss@33099
   362
        val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
krauss@33099
   363
krauss@33099
   364
        val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
krauss@33099
   365
krauss@33099
   366
        fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
krauss@33099
   367
                                                            |> fold_rev (implies_intr o cprop_of) CCas
krauss@33099
   368
                                                            |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
krauss@33099
   369
krauss@33099
   370
        val existence = fold (curry op COMP o prep_RC) RCs lGI
krauss@33099
   371
krauss@33099
   372
        val P = cterm_of thy (mk_eq (y, rhsC))
krauss@33099
   373
        val G_lhs_y = assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
krauss@33099
   374
krauss@33099
   375
        val unique_clauses = map2 (mk_uniqueness_clause thy globals f compat_store clausei) clauses rep_lemmas
krauss@33099
   376
krauss@33099
   377
        val uniqueness = G_cases
krauss@33099
   378
                           |> forall_elim (cterm_of thy lhs)
krauss@33099
   379
                           |> forall_elim (cterm_of thy y)
krauss@33099
   380
                           |> forall_elim P
krauss@33099
   381
                           |> Thm.elim_implies G_lhs_y
krauss@33099
   382
                           |> fold Thm.elim_implies unique_clauses
krauss@33099
   383
                           |> implies_intr (cprop_of G_lhs_y)
krauss@33099
   384
                           |> forall_intr (cterm_of thy y)
krauss@33099
   385
krauss@33099
   386
        val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
krauss@33099
   387
krauss@33099
   388
        val exactly_one =
krauss@33099
   389
            ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
krauss@33099
   390
                 |> curry (op COMP) existence
krauss@33099
   391
                 |> curry (op COMP) uniqueness
krauss@33099
   392
                 |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
krauss@33099
   393
                 |> implies_intr (cprop_of case_hyp)
krauss@33099
   394
                 |> fold_rev (implies_intr o cprop_of) ags
krauss@33099
   395
                 |> fold_rev forall_intr cqs
krauss@33099
   396
krauss@33099
   397
        val function_value =
krauss@33099
   398
            existence
krauss@33099
   399
              |> implies_intr ihyp
krauss@33099
   400
              |> implies_intr (cprop_of case_hyp)
krauss@33099
   401
              |> forall_intr (cterm_of thy x)
krauss@33099
   402
              |> forall_elim (cterm_of thy lhs)
krauss@33099
   403
              |> curry (op RS) refl
krauss@33099
   404
    in
krauss@33099
   405
        (exactly_one, function_value)
krauss@33099
   406
    end
krauss@33099
   407
krauss@33099
   408
krauss@33099
   409
krauss@33099
   410
krauss@33099
   411
fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim f_def =
krauss@33099
   412
    let
krauss@33099
   413
        val Globals {h, domT, ranT, x, ...} = globals
krauss@33099
   414
        val thy = ProofContext.theory_of ctxt
krauss@33099
   415
krauss@33099
   416
        (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
krauss@33099
   417
        val ihyp = Term.all domT $ Abs ("z", domT,
krauss@33099
   418
                                   Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
krauss@33099
   419
                                     HOLogic.mk_Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
krauss@33099
   420
                                                             Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
krauss@33099
   421
                       |> cterm_of thy
krauss@33099
   422
krauss@33099
   423
        val ihyp_thm = assume ihyp |> Thm.forall_elim_vars 0
krauss@33099
   424
        val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
krauss@33099
   425
        val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
krauss@33099
   426
                        |> instantiate' [] [NONE, SOME (cterm_of thy h)]
krauss@33099
   427
krauss@33099
   428
        val _ = trace_msg (K "Proving Replacement lemmas...")
krauss@33099
   429
        val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
krauss@33099
   430
krauss@33099
   431
        val _ = trace_msg (K "Proving cases for unique existence...")
krauss@33099
   432
        val (ex1s, values) =
krauss@33099
   433
            split_list (map (mk_uniqueness_case ctxt thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
krauss@33099
   434
krauss@33099
   435
        val _ = trace_msg (K "Proving: Graph is a function")
krauss@33099
   436
        val graph_is_function = complete
krauss@33099
   437
                                  |> Thm.forall_elim_vars 0
krauss@33099
   438
                                  |> fold (curry op COMP) ex1s
krauss@33099
   439
                                  |> implies_intr (ihyp)
krauss@33099
   440
                                  |> implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
krauss@33099
   441
                                  |> forall_intr (cterm_of thy x)
krauss@33099
   442
                                  |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
krauss@33099
   443
                                  |> (fn it => fold (forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)
krauss@33099
   444
krauss@33099
   445
        val goalstate =  Conjunction.intr graph_is_function complete
krauss@33099
   446
                          |> Thm.close_derivation
krauss@33099
   447
                          |> Goal.protect
krauss@33099
   448
                          |> fold_rev (implies_intr o cprop_of) compat
krauss@33099
   449
                          |> implies_intr (cprop_of complete)
krauss@33099
   450
    in
krauss@33099
   451
      (goalstate, values)
krauss@33099
   452
    end
krauss@33099
   453
krauss@33348
   454
(* wrapper -- restores quantifiers in rule specifications *)
krauss@33348
   455
fun inductive_def (binding as ((R, T), _)) intrs lthy =
krauss@33348
   456
  let
krauss@33348
   457
    val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) =
krauss@33348
   458
      lthy
wenzelm@33671
   459
      |> Local_Theory.conceal
krauss@33348
   460
      |> Inductive.add_inductive_i
krauss@33350
   461
          {quiet_mode = true,
krauss@33350
   462
            verbose = ! trace,
krauss@33348
   463
            alt_name = Binding.empty,
krauss@33348
   464
            coind = false,
krauss@33348
   465
            no_elim = false,
krauss@33348
   466
            no_ind = false,
krauss@33348
   467
            skip_mono = true,
krauss@33348
   468
            fork_mono = false}
krauss@33348
   469
          [binding] (* relation *)
krauss@33348
   470
          [] (* no parameters *)
krauss@33348
   471
          (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)
krauss@33348
   472
          [] (* no special monos *)
wenzelm@33671
   473
      ||> Local_Theory.restore_naming lthy
krauss@33348
   474
krauss@33348
   475
    val cert = cterm_of (ProofContext.theory_of lthy)
krauss@33348
   476
    fun requantify orig_intro thm =
krauss@33348
   477
      let
krauss@33348
   478
        val (qs, t) = dest_all_all orig_intro
krauss@33348
   479
        val frees = frees_in_term lthy t |> remove (op =) (Binding.name_of R, T)
krauss@33348
   480
        val vars = Term.add_vars (prop_of thm) [] |> rev
krauss@33348
   481
        val varmap = AList.lookup (op =) (frees ~~ map fst vars)
krauss@33348
   482
          #> the_default ("",0)
krauss@33348
   483
      in
krauss@33348
   484
        fold_rev (fn Free (n, T) =>
krauss@33348
   485
          forall_intr_rename (n, cert (Var (varmap (n, T), T)))) qs thm
krauss@33348
   486
      end
krauss@33348
   487
  in
krauss@33349
   488
      ((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct), lthy)
krauss@33348
   489
  end
krauss@33348
   490
krauss@33099
   491
fun define_graph Gname fvar domT ranT clauses RCss lthy =
krauss@33349
   492
  let
krauss@33349
   493
    val GT = domT --> ranT --> boolT
krauss@33349
   494
    val (Gvar as (n, T)) = singleton (Variable.variant_frees lthy []) (Gname, GT)
krauss@33099
   495
krauss@33349
   496
    fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs =
krauss@33349
   497
      let
krauss@33349
   498
        fun mk_h_assm (rcfix, rcassm, rcarg) =
krauss@33349
   499
          HOLogic.mk_Trueprop (Free Gvar $ rcarg $ (fvar $ rcarg))
krauss@33349
   500
          |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
krauss@33349
   501
          |> fold_rev (Logic.all o Free) rcfix
krauss@33349
   502
      in
krauss@33349
   503
        HOLogic.mk_Trueprop (Free Gvar $ lhs $ rhs)
krauss@33349
   504
        |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs
krauss@33349
   505
        |> fold_rev (curry Logic.mk_implies) gs
krauss@33349
   506
        |> fold_rev Logic.all (fvar :: qs)
krauss@33349
   507
      end
krauss@33099
   508
krauss@33349
   509
    val G_intros = map2 mk_GIntro clauses RCss
krauss@33349
   510
  in
krauss@33349
   511
    inductive_def ((Binding.name n, T), NoSyn) G_intros lthy
krauss@33349
   512
  end
krauss@33099
   513
krauss@33099
   514
fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
krauss@33349
   515
  let
krauss@33349
   516
    val f_def =
krauss@33349
   517
      Abs ("x", domT, Const (@{const_name FunDef.THE_default}, ranT --> (ranT --> boolT) --> ranT) 
krauss@33349
   518
        $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0))
krauss@33349
   519
      |> Syntax.check_term lthy
krauss@33349
   520
  in
wenzelm@33671
   521
    Local_Theory.define ""
krauss@33349
   522
      ((Binding.name (function_name fname), mixfix),
krauss@33349
   523
        ((Binding.conceal (Binding.name fdefname), []), f_def)) lthy
krauss@33349
   524
  end
krauss@33099
   525
krauss@33099
   526
fun define_recursion_relation Rname domT ranT fvar f qglrs clauses RCss lthy =
krauss@33349
   527
  let
krauss@33349
   528
    val RT = domT --> domT --> boolT
krauss@33349
   529
    val (Rvar as (n, T)) = singleton (Variable.variant_frees lthy []) (Rname, RT)
krauss@33099
   530
krauss@33349
   531
    fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =
krauss@33349
   532
      HOLogic.mk_Trueprop (Free Rvar $ rcarg $ lhs)
krauss@33349
   533
      |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
krauss@33349
   534
      |> fold_rev (curry Logic.mk_implies) gs
krauss@33349
   535
      |> fold_rev (Logic.all o Free) rcfix
krauss@33349
   536
      |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
krauss@33349
   537
      (* "!!qs xs. CS ==> G => (r, lhs) : R" *)
krauss@33099
   538
krauss@33349
   539
    val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss
krauss@33099
   540
krauss@33349
   541
    val ((R, RIntro_thms, R_elim, _), lthy) =
krauss@33349
   542
      inductive_def ((Binding.name n, T), NoSyn) (flat R_intross) lthy
krauss@33349
   543
  in
krauss@33349
   544
    ((R, Library.unflat R_intross RIntro_thms, R_elim), lthy)
krauss@33349
   545
  end
krauss@33099
   546
krauss@33099
   547
krauss@33099
   548
fun fix_globals domT ranT fvar ctxt =
krauss@33099
   549
    let
krauss@33099
   550
      val ([h, y, x, z, a, D, P, Pbool],ctxt') =
krauss@33099
   551
          Variable.variant_fixes ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt
krauss@33099
   552
    in
krauss@33099
   553
      (Globals {h = Free (h, domT --> ranT),
krauss@33099
   554
                y = Free (y, ranT),
krauss@33099
   555
                x = Free (x, domT),
krauss@33099
   556
                z = Free (z, domT),
krauss@33099
   557
                a = Free (a, domT),
krauss@33099
   558
                D = Free (D, domT --> boolT),
krauss@33099
   559
                P = Free (P, domT --> boolT),
krauss@33099
   560
                Pbool = Free (Pbool, boolT),
krauss@33099
   561
                fvar = fvar,
krauss@33099
   562
                domT = domT,
krauss@33099
   563
                ranT = ranT
krauss@33099
   564
               },
krauss@33099
   565
       ctxt')
krauss@33099
   566
    end
krauss@33099
   567
krauss@33099
   568
krauss@33099
   569
krauss@33099
   570
fun inst_RC thy fvar f (rcfix, rcassm, rcarg) =
krauss@33099
   571
    let
krauss@33099
   572
      fun inst_term t = subst_bound(f, abstract_over (fvar, t))
krauss@33099
   573
    in
krauss@33099
   574
      (rcfix, map (assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)
krauss@33099
   575
    end
krauss@33099
   576
krauss@33099
   577
krauss@33099
   578
krauss@33099
   579
(**********************************************************
krauss@33099
   580
 *                   PROVING THE RULES
krauss@33099
   581
 **********************************************************)
krauss@33099
   582
krauss@33099
   583
fun mk_psimps thy globals R clauses valthms f_iff graph_is_function =
krauss@33099
   584
    let
krauss@33099
   585
      val Globals {domT, z, ...} = globals
krauss@33099
   586
krauss@33099
   587
      fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm =
krauss@33099
   588
          let
krauss@33099
   589
            val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
krauss@33099
   590
            val z_smaller = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *)
krauss@33099
   591
          in
krauss@33099
   592
            ((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
krauss@33099
   593
              |> (fn it => it COMP graph_is_function)
krauss@33099
   594
              |> implies_intr z_smaller
krauss@33099
   595
              |> forall_intr (cterm_of thy z)
krauss@33099
   596
              |> (fn it => it COMP valthm)
krauss@33099
   597
              |> implies_intr lhs_acc
krauss@33099
   598
              |> asm_simplify (HOL_basic_ss addsimps [f_iff])
krauss@33099
   599
              |> fold_rev (implies_intr o cprop_of) ags
krauss@33099
   600
              |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
krauss@33099
   601
          end
krauss@33099
   602
    in
krauss@33099
   603
      map2 mk_psimp clauses valthms
krauss@33099
   604
    end
krauss@33099
   605
krauss@33099
   606
krauss@33099
   607
(** Induction rule **)
krauss@33099
   608
krauss@33099
   609
krauss@33099
   610
val acc_subset_induct = @{thm Orderings.predicate1I} RS @{thm accp_subset_induct}
krauss@33099
   611
krauss@33099
   612
krauss@33099
   613
fun mk_partial_induct_rule thy globals R complete_thm clauses =
krauss@33099
   614
    let
krauss@33099
   615
      val Globals {domT, x, z, a, P, D, ...} = globals
krauss@33099
   616
      val acc_R = mk_acc domT R
krauss@33099
   617
krauss@33099
   618
      val x_D = assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x)))
krauss@33099
   619
      val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a))
krauss@33099
   620
krauss@33099
   621
      val D_subset = cterm_of thy (Logic.all x
krauss@33099
   622
        (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x))))
krauss@33099
   623
krauss@33099
   624
      val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
krauss@33099
   625
                    Logic.all x
krauss@33099
   626
                    (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x),
krauss@33099
   627
                                                    Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x),
krauss@33099
   628
                                                                      HOLogic.mk_Trueprop (D $ z)))))
krauss@33099
   629
                    |> cterm_of thy
krauss@33099
   630
krauss@33099
   631
krauss@33099
   632
  (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
krauss@33099
   633
      val ihyp = Term.all domT $ Abs ("z", domT,
krauss@33099
   634
               Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
krauss@33099
   635
                 HOLogic.mk_Trueprop (P $ Bound 0)))
krauss@33099
   636
           |> cterm_of thy
krauss@33099
   637
krauss@33099
   638
      val aihyp = assume ihyp
krauss@33099
   639
krauss@33099
   640
  fun prove_case clause =
krauss@33099
   641
      let
krauss@33099
   642
    val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...}, RCs,
krauss@33099
   643
                    qglr = (oqs, _, _, _), ...} = clause
krauss@33099
   644
krauss@33099
   645
    val case_hyp_conv = K (case_hyp RS eq_reflection)
krauss@33099
   646
    local open Conv in
krauss@33099
   647
    val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
krauss@33099
   648
    val sih = fconv_rule (More_Conv.binder_conv (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp
krauss@33099
   649
    end
krauss@33099
   650
krauss@33099
   651
    fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
krauss@33099
   652
        sih |> forall_elim (cterm_of thy rcarg)
krauss@33099
   653
            |> Thm.elim_implies llRI
krauss@33099
   654
            |> fold_rev (implies_intr o cprop_of) CCas
krauss@33099
   655
            |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
krauss@33099
   656
krauss@33099
   657
    val P_recs = map mk_Prec RCs   (*  [P rec1, P rec2, ... ]  *)
krauss@33099
   658
krauss@33099
   659
    val step = HOLogic.mk_Trueprop (P $ lhs)
krauss@33099
   660
            |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
krauss@33099
   661
            |> fold_rev (curry Logic.mk_implies) gs
krauss@33099
   662
            |> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs))
krauss@33099
   663
            |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
krauss@33099
   664
            |> cterm_of thy
krauss@33099
   665
krauss@33099
   666
    val P_lhs = assume step
krauss@33099
   667
           |> fold forall_elim cqs
krauss@33099
   668
           |> Thm.elim_implies lhs_D
krauss@33099
   669
           |> fold Thm.elim_implies ags
krauss@33099
   670
           |> fold Thm.elim_implies P_recs
krauss@33099
   671
krauss@33099
   672
    val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x))
krauss@33099
   673
           |> Conv.arg_conv (Conv.arg_conv case_hyp_conv)
krauss@33099
   674
           |> symmetric (* P lhs == P x *)
krauss@33099
   675
           |> (fn eql => equal_elim eql P_lhs) (* "P x" *)
krauss@33099
   676
           |> implies_intr (cprop_of case_hyp)
krauss@33099
   677
           |> fold_rev (implies_intr o cprop_of) ags
krauss@33099
   678
           |> fold_rev forall_intr cqs
krauss@33099
   679
      in
krauss@33099
   680
        (res, step)
krauss@33099
   681
      end
krauss@33099
   682
krauss@33099
   683
  val (cases, steps) = split_list (map prove_case clauses)
krauss@33099
   684
krauss@33099
   685
  val istep = complete_thm
krauss@33099
   686
                |> Thm.forall_elim_vars 0
krauss@33099
   687
                |> fold (curry op COMP) cases (*  P x  *)
krauss@33099
   688
                |> implies_intr ihyp
krauss@33099
   689
                |> implies_intr (cprop_of x_D)
krauss@33099
   690
                |> forall_intr (cterm_of thy x)
krauss@33099
   691
krauss@33099
   692
  val subset_induct_rule =
krauss@33099
   693
      acc_subset_induct
krauss@33099
   694
        |> (curry op COMP) (assume D_subset)
krauss@33099
   695
        |> (curry op COMP) (assume D_dcl)
krauss@33099
   696
        |> (curry op COMP) (assume a_D)
krauss@33099
   697
        |> (curry op COMP) istep
krauss@33099
   698
        |> fold_rev implies_intr steps
krauss@33099
   699
        |> implies_intr a_D
krauss@33099
   700
        |> implies_intr D_dcl
krauss@33099
   701
        |> implies_intr D_subset
krauss@33099
   702
krauss@33099
   703
  val subset_induct_all = fold_rev (forall_intr o cterm_of thy) [P, a, D] subset_induct_rule
krauss@33099
   704
krauss@33099
   705
  val simple_induct_rule =
krauss@33099
   706
      subset_induct_rule
krauss@33099
   707
        |> forall_intr (cterm_of thy D)
krauss@33099
   708
        |> forall_elim (cterm_of thy acc_R)
krauss@33099
   709
        |> assume_tac 1 |> Seq.hd
krauss@33099
   710
        |> (curry op COMP) (acc_downward
krauss@33099
   711
                              |> (instantiate' [SOME (ctyp_of thy domT)]
krauss@33099
   712
                                               (map (SOME o cterm_of thy) [R, x, z]))
krauss@33099
   713
                              |> forall_intr (cterm_of thy z)
krauss@33099
   714
                              |> forall_intr (cterm_of thy x))
krauss@33099
   715
        |> forall_intr (cterm_of thy a)
krauss@33099
   716
        |> forall_intr (cterm_of thy P)
krauss@33099
   717
    in
krauss@33099
   718
      simple_induct_rule
krauss@33099
   719
    end
krauss@33099
   720
krauss@33099
   721
krauss@33099
   722
krauss@33099
   723
(* FIXME: This should probably use fixed goals, to be more reliable and faster *)
krauss@33099
   724
fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause =
krauss@33099
   725
    let
krauss@33099
   726
      val thy = ProofContext.theory_of ctxt
krauss@33099
   727
      val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...},
krauss@33099
   728
                      qglr = (oqs, _, _, _), ...} = clause
krauss@33099
   729
      val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs)
krauss@33099
   730
                          |> fold_rev (curry Logic.mk_implies) gs
krauss@33099
   731
                          |> cterm_of thy
krauss@33099
   732
    in
krauss@33099
   733
      Goal.init goal
krauss@33099
   734
      |> (SINGLE (resolve_tac [accI] 1)) |> the
krauss@33099
   735
      |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1))  |> the
krauss@33099
   736
      |> (SINGLE (auto_tac (clasimpset_of ctxt))) |> the
krauss@33099
   737
      |> Goal.conclude
krauss@33099
   738
      |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
krauss@33099
   739
    end
krauss@33099
   740
krauss@33099
   741
krauss@33099
   742
krauss@33099
   743
(** Termination rule **)
krauss@33099
   744
krauss@33099
   745
val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule};
krauss@33099
   746
val wf_in_rel = @{thm FunDef.wf_in_rel};
krauss@33099
   747
val in_rel_def = @{thm FunDef.in_rel_def};
krauss@33099
   748
krauss@33099
   749
fun mk_nest_term_case thy globals R' ihyp clause =
krauss@33099
   750
    let
krauss@33099
   751
      val Globals {x, z, ...} = globals
krauss@33099
   752
      val ClauseInfo {cdata = ClauseContext {qs,cqs,ags,lhs,rhs,case_hyp,...},tree,
krauss@33099
   753
                      qglr=(oqs, _, _, _), ...} = clause
krauss@33099
   754
krauss@33099
   755
      val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
krauss@33099
   756
krauss@33099
   757
      fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
krauss@33099
   758
          let
krauss@33099
   759
            val used = map (fn (ctx,thm) => Function_Ctx_Tree.export_thm thy ctx thm) (u @ sub)
krauss@33099
   760
krauss@33099
   761
            val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs)
krauss@33099
   762
                      |> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *)
krauss@33099
   763
                      |> Function_Ctx_Tree.export_term (fixes, assumes)
krauss@33099
   764
                      |> fold_rev (curry Logic.mk_implies o prop_of) ags
krauss@33099
   765
                      |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
krauss@33099
   766
                      |> cterm_of thy
krauss@33099
   767
krauss@33099
   768
            val thm = assume hyp
krauss@33099
   769
                      |> fold forall_elim cqs
krauss@33099
   770
                      |> fold Thm.elim_implies ags
krauss@33099
   771
                      |> Function_Ctx_Tree.import_thm thy (fixes, assumes)
krauss@33099
   772
                      |> fold Thm.elim_implies used (*  "(arg, lhs) : R'"  *)
krauss@33099
   773
krauss@33099
   774
            val z_eq_arg = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (z, arg))))
krauss@33099
   775
krauss@33099
   776
            val acc = thm COMP ih_case
krauss@33099
   777
            val z_acc_local = acc
krauss@33099
   778
            |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (K (symmetric (z_eq_arg RS eq_reflection)))))
krauss@33099
   779
krauss@33099
   780
            val ethm = z_acc_local
krauss@33099
   781
                         |> Function_Ctx_Tree.export_thm thy (fixes,
krauss@33099
   782
                                                          z_eq_arg :: case_hyp :: ags @ assumes)
krauss@33099
   783
                         |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
krauss@33099
   784
krauss@33099
   785
            val sub' = sub @ [(([],[]), acc)]
krauss@33099
   786
          in
krauss@33099
   787
            (sub', (hyp :: hyps, ethm :: thms))
krauss@33099
   788
          end
krauss@33099
   789
        | step _ _ _ _ = raise Match
krauss@33099
   790
    in
krauss@33099
   791
      Function_Ctx_Tree.traverse_tree step tree
krauss@33099
   792
    end
krauss@33099
   793
krauss@33099
   794
krauss@33099
   795
fun mk_nest_term_rule thy globals R R_cases clauses =
krauss@33099
   796
    let
krauss@33099
   797
      val Globals { domT, x, z, ... } = globals
krauss@33099
   798
      val acc_R = mk_acc domT R
krauss@33099
   799
krauss@33099
   800
      val R' = Free ("R", fastype_of R)
krauss@33099
   801
krauss@33099
   802
      val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
krauss@33099
   803
      val inrel_R = Const (@{const_name FunDef.in_rel}, HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
krauss@33099
   804
krauss@33099
   805
      val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP}, (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
krauss@33099
   806
krauss@33099
   807
      (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
krauss@33099
   808
      val ihyp = Term.all domT $ Abs ("z", domT,
krauss@33099
   809
                                 Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x),
krauss@33099
   810
                                   HOLogic.mk_Trueprop (acc_R $ Bound 0)))
krauss@33099
   811
                     |> cterm_of thy
krauss@33099
   812
krauss@33099
   813
      val ihyp_a = assume ihyp |> Thm.forall_elim_vars 0
krauss@33099
   814
krauss@33099
   815
      val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x))
krauss@33099
   816
krauss@33099
   817
      val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[])
krauss@33099
   818
    in
krauss@33099
   819
      R_cases
krauss@33099
   820
        |> forall_elim (cterm_of thy z)
krauss@33099
   821
        |> forall_elim (cterm_of thy x)
krauss@33099
   822
        |> forall_elim (cterm_of thy (acc_R $ z))
krauss@33099
   823
        |> curry op COMP (assume R_z_x)
krauss@33099
   824
        |> fold_rev (curry op COMP) cases
krauss@33099
   825
        |> implies_intr R_z_x
krauss@33099
   826
        |> forall_intr (cterm_of thy z)
krauss@33099
   827
        |> (fn it => it COMP accI)
krauss@33099
   828
        |> implies_intr ihyp
krauss@33099
   829
        |> forall_intr (cterm_of thy x)
krauss@33099
   830
        |> (fn it => Drule.compose_single(it,2,wf_induct_rule))
krauss@33099
   831
        |> curry op RS (assume wfR')
krauss@33099
   832
        |> forall_intr_vars
krauss@33099
   833
        |> (fn it => it COMP allI)
krauss@33099
   834
        |> fold implies_intr hyps
krauss@33099
   835
        |> implies_intr wfR'
krauss@33099
   836
        |> forall_intr (cterm_of thy R')
krauss@33099
   837
        |> forall_elim (cterm_of thy (inrel_R))
krauss@33099
   838
        |> curry op RS wf_in_rel
krauss@33099
   839
        |> full_simplify (HOL_basic_ss addsimps [in_rel_def])
krauss@33099
   840
        |> forall_intr (cterm_of thy Rrel)
krauss@33099
   841
    end
krauss@33099
   842
krauss@33099
   843
krauss@33099
   844
krauss@33099
   845
(* Tail recursion (probably very fragile)
krauss@33099
   846
 *
krauss@33099
   847
 * FIXME:
krauss@33099
   848
 * - Need to do forall_elim_vars on psimps: Unneccesary, if psimps would be taken from the same context.
krauss@33099
   849
 * - Must we really replace the fvar by f here?
krauss@33099
   850
 * - Splitting is not configured automatically: Problems with case?
krauss@33099
   851
 *)
krauss@33099
   852
fun mk_trsimps octxt globals f G R f_def R_cases G_induct clauses psimps =
krauss@33099
   853
    let
krauss@33099
   854
      val Globals {domT, ranT, fvar, ...} = globals
krauss@33099
   855
krauss@33099
   856
      val R_cases = Thm.forall_elim_vars 0 R_cases (* FIXME: Should be already in standard form. *)
krauss@33099
   857
krauss@33099
   858
      val graph_implies_dom = (* "G ?x ?y ==> dom ?x"  *)
krauss@33099
   859
          Goal.prove octxt ["x", "y"] [HOLogic.mk_Trueprop (G $ Free ("x", domT) $ Free ("y", ranT))]
krauss@33099
   860
                     (HOLogic.mk_Trueprop (mk_acc domT R $ Free ("x", domT)))
krauss@33099
   861
                     (fn {prems=[a], ...} =>
krauss@33099
   862
                         ((rtac (G_induct OF [a]))
krauss@33099
   863
                            THEN_ALL_NEW (rtac accI)
krauss@33099
   864
                            THEN_ALL_NEW (etac R_cases)
krauss@33099
   865
                            THEN_ALL_NEW (asm_full_simp_tac (simpset_of octxt))) 1)
krauss@33099
   866
krauss@33099
   867
      val default_thm = (forall_intr_vars graph_implies_dom) COMP (f_def COMP fundef_default_value)
krauss@33099
   868
krauss@33099
   869
      fun mk_trsimp clause psimp =
krauss@33099
   870
          let
krauss@33099
   871
            val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {ctxt, cqs, qs, gs, lhs, rhs, ...}, ...} = clause
krauss@33099
   872
            val thy = ProofContext.theory_of ctxt
krauss@33099
   873
            val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs
krauss@33099
   874
krauss@33099
   875
            val trsimp = Logic.list_implies(gs, HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *)
krauss@33099
   876
            val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *)
krauss@33099
   877
            fun simp_default_tac ss = asm_full_simp_tac (ss addsimps [default_thm, Let_def])
krauss@33099
   878
          in
krauss@33099
   879
            Goal.prove ctxt [] [] trsimp
krauss@33099
   880
                       (fn _ =>
krauss@33099
   881
                           rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
krauss@33099
   882
                                THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
krauss@33099
   883
                                THEN (simp_default_tac (simpset_of ctxt) 1)
krauss@33099
   884
                                THEN (etac not_acc_down 1)
krauss@33099
   885
                                THEN ((etac R_cases) THEN_ALL_NEW (simp_default_tac (simpset_of ctxt))) 1)
krauss@33099
   886
              |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
krauss@33099
   887
          end
krauss@33099
   888
    in
krauss@33099
   889
      map2 mk_trsimp clauses psimps
krauss@33099
   890
    end
krauss@33099
   891
krauss@33099
   892
krauss@33099
   893
fun prepare_function config defname [((fname, fT), mixfix)] abstract_qglrs lthy =
krauss@33099
   894
    let
krauss@33099
   895
      val FunctionConfig {domintros, tailrec, default=default_str, ...} = config
krauss@33099
   896
krauss@33099
   897
      val fvar = Free (fname, fT)
krauss@33099
   898
      val domT = domain_type fT
krauss@33099
   899
      val ranT = range_type fT
krauss@33099
   900
krauss@33099
   901
      val default = Syntax.parse_term lthy default_str
krauss@33099
   902
        |> TypeInfer.constrain fT |> Syntax.check_term lthy
krauss@33099
   903
krauss@33099
   904
      val (globals, ctxt') = fix_globals domT ranT fvar lthy
krauss@33099
   905
krauss@33099
   906
      val Globals { x, h, ... } = globals
krauss@33099
   907
krauss@33099
   908
      val clauses = map (mk_clause_context x ctxt') abstract_qglrs
krauss@33099
   909
krauss@33099
   910
      val n = length abstract_qglrs
krauss@33099
   911
krauss@33099
   912
      fun build_tree (ClauseContext { ctxt, rhs, ...}) =
krauss@33099
   913
            Function_Ctx_Tree.mk_tree (fname, fT) h ctxt rhs
krauss@33099
   914
krauss@33099
   915
      val trees = map build_tree clauses
krauss@33099
   916
      val RCss = map find_calls trees
krauss@33099
   917
krauss@33099
   918
      val ((G, GIntro_thms, G_elim, G_induct), lthy) =
krauss@33099
   919
          PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
krauss@33099
   920
krauss@33349
   921
      val ((f, (_, f_defthm)), lthy) =
krauss@33099
   922
          PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
krauss@33099
   923
krauss@33099
   924
      val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
krauss@33099
   925
      val trees = map (Function_Ctx_Tree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
krauss@33099
   926
krauss@33099
   927
      val ((R, RIntro_thmss, R_elim), lthy) =
krauss@33099
   928
          PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
krauss@33099
   929
krauss@33099
   930
      val (_, lthy) =
wenzelm@33671
   931
          Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
krauss@33099
   932
krauss@33099
   933
      val newthy = ProofContext.theory_of lthy
krauss@33099
   934
      val clauses = map (transfer_clause_ctx newthy) clauses
krauss@33099
   935
krauss@33099
   936
      val cert = cterm_of (ProofContext.theory_of lthy)
krauss@33099
   937
krauss@33099
   938
      val xclauses = PROFILE "xclauses" (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees RCss GIntro_thms) RIntro_thmss
krauss@33099
   939
krauss@33099
   940
      val complete = mk_completeness globals clauses abstract_qglrs |> cert |> assume
krauss@33099
   941
      val compat = mk_compat_proof_obligations domT ranT fvar f abstract_qglrs |> map (cert #> assume)
krauss@33099
   942
krauss@33099
   943
      val compat_store = store_compat_thms n compat
krauss@33099
   944
krauss@33099
   945
      val (goalstate, values) = PROFILE "prove_stuff" (prove_stuff lthy globals G f R xclauses complete compat compat_store G_elim) f_defthm
krauss@33099
   946
krauss@33099
   947
      val mk_trsimps = mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses
krauss@33099
   948
krauss@33099
   949
      fun mk_partial_rules provedgoal =
krauss@33099
   950
          let
krauss@33099
   951
            val newthy = theory_of_thm provedgoal (*FIXME*)
krauss@33099
   952
krauss@33099
   953
            val (graph_is_function, complete_thm) =
krauss@33099
   954
                provedgoal
krauss@33099
   955
                  |> Conjunction.elim
krauss@33099
   956
                  |> apfst (Thm.forall_elim_vars 0)
krauss@33099
   957
krauss@33099
   958
            val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)
krauss@33099
   959
krauss@33099
   960
            val psimps = PROFILE "Proving simplification rules" (mk_psimps newthy globals R xclauses values f_iff) graph_is_function
krauss@33099
   961
krauss@33099
   962
            val simple_pinduct = PROFILE "Proving partial induction rule"
krauss@33099
   963
                                                           (mk_partial_induct_rule newthy globals R complete_thm) xclauses
krauss@33099
   964
krauss@33099
   965
krauss@33099
   966
            val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule newthy globals R R_elim) xclauses
krauss@33099
   967
krauss@33099
   968
            val dom_intros = if domintros
krauss@33099
   969
                             then SOME (PROFILE "Proving domain introduction rules" (map (mk_domain_intro lthy globals R R_elim)) xclauses)
krauss@33099
   970
                             else NONE
krauss@33099
   971
            val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE
krauss@33099
   972
krauss@33099
   973
          in
krauss@33099
   974
            FunctionResult {fs=[f], G=G, R=R, cases=complete_thm,
krauss@33099
   975
                          psimps=psimps, simple_pinducts=[simple_pinduct],
krauss@33099
   976
                          termination=total_intro, trsimps=trsimps,
krauss@33099
   977
                          domintros=dom_intros}
krauss@33099
   978
          end
krauss@33099
   979
    in
krauss@33099
   980
      ((f, goalstate, mk_partial_rules), lthy)
krauss@33099
   981
    end
krauss@33099
   982
krauss@33099
   983
krauss@33099
   984
end