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