src/HOL/Tools/function_package/fundef_core.ML

tuned proofs -- avoid implicit prems;

(*  Title:      HOL/Tools/function_package/fundef_core.ML
    ID:         $Id$
    Author:     Alexander Krauss, TU Muenchen

A package for general recursive function definitions.
Main functionality
*)

signature FUNDEF_CORE =
sig
    val prepare_fundef : FundefCommon.fundef_config
                         -> string (* defname *)
                         -> ((string * typ) * mixfix) list (* defined symbol *)
                         -> ((string * typ) list * term list * term * term) list (* specification *)
                         -> local_theory

                         -> (term   (* f *)
                             * thm  (* goalstate *)
                             * (thm -> FundefCommon.fundef_result) (* continuation *)
                            ) * local_theory

end

structure FundefCore : FUNDEF_CORE =
struct


open FundefLib
open FundefCommon
open FundefAbbrev

datatype globals =
   Globals of { 
         fvar: term, 
         domT: typ, 
         ranT: typ,
         h: term, 
         y: term, 
         x: term, 
         z: term, 
         a: term, 
         P: term, 
         D: term, 
         Pbool:term
}


datatype rec_call_info = 
  RCInfo of
  {
   RIvs: (string * typ) list,  (* Call context: fixes and assumes *)
   CCas: thm list,
   rcarg: term,                 (* The recursive argument *)

   llRI: thm,
   h_assum: term
  } 


datatype clause_context =
  ClauseContext of
  {
    ctxt : Proof.context,

    qs : term list,
    gs : term list,
    lhs: term,
    rhs: term,

    cqs: cterm list,
    ags: thm list,     
    case_hyp : thm
  }


fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) =
    ClauseContext { ctxt = ProofContext.transfer thy ctxt,
                    qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp }


datatype clause_info =
  ClauseInfo of 
     {
      no: int,
      qglr : ((string * typ) list * term list * term * term),
      cdata : clause_context,

      tree: ctx_tree,
      lGI: thm,
      RCs: rec_call_info list
     }


(* Theory dependencies. *)
val Pair_inject = thm "Product_Type.Pair_inject";

val acc_induct_rule = thm "Accessible_Part.acc_induct_rule"

val ex1_implies_ex = thm "FunDef.fundef_ex1_existence"
val ex1_implies_un = thm "FunDef.fundef_ex1_uniqueness"
val ex1_implies_iff = thm "FunDef.fundef_ex1_iff"

val acc_downward = thm "Accessible_Part.acc_downward"
val accI = thm "Accessible_Part.accI"
val case_split = thm "HOL.case_split_thm"
val fundef_default_value = thm "FunDef.fundef_default_value"
val not_acc_down = thm "Accessible_Part.not_acc_down"



fun find_calls tree =
    let
      fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) = ([], (fixes, assumes, arg) :: xs)
        | add_Ri _ _ _ _ = raise Match
    in
      rev (FundefCtxTree.traverse_tree add_Ri tree [])
    end


(** building proof obligations *)

fun mk_compat_proof_obligations domT ranT fvar f glrs =
    let
      fun mk_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
          let
            val shift = incr_boundvars (length qs')
          in
            (implies $ Trueprop (eq_const domT $ shift lhs $ lhs')
                     $ Trueprop (eq_const ranT $ shift rhs $ rhs'))
              |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
              |> fold_rev (fn (n,T) => fn b => all T $ Abs(n,T,b)) (qs @ qs')
              |> curry abstract_over fvar
              |> curry subst_bound f
          end
    in
      map mk_impl (unordered_pairs glrs)
    end


fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs =
    let
        fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) =
            Trueprop Pbool
                     |> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
                     |> fold_rev (curry Logic.mk_implies) gs
                     |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
    in
        Trueprop Pbool
                 |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs)
                 |> mk_forall_rename ("x", x)
                 |> mk_forall_rename ("P", Pbool)
    end

(** making a context with it's own local bindings **)

fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) =
    let
      val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt
                                           |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs

      val thy = ProofContext.theory_of ctxt'

      fun inst t = subst_bounds (rev qs, t)
      val gs = map inst pre_gs
      val lhs = inst pre_lhs
      val rhs = inst pre_rhs
                
      val cqs = map (cterm_of thy) qs
      val ags = map (assume o cterm_of thy) gs
                  
      val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
    in
      ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs, 
                      cqs = cqs, ags = ags, case_hyp = case_hyp }
    end
      

(* lowlevel term function *)
fun abstract_over_list vs body =
  let
    exception SAME;
    fun abs lev v tm =
      if v aconv tm then Bound lev
      else
        (case tm of
          Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t)
        | t $ u => (abs lev v t $ (abs lev v u handle SAME => u) handle SAME => t $ abs lev v u)
        | _ => raise SAME);
  in 
    fold_index (fn (i,v) => fn t => abs i v t handle SAME => t) vs body
  end



fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms =
    let
        val Globals {h, fvar, x, ...} = globals

        val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
        val cert = Thm.cterm_of (ProofContext.theory_of ctxt)

        (* Instantiate the GIntro thm with "f" and import into the clause context. *)
        val lGI = GIntro_thm
                    |> forall_elim (cert f)
                    |> fold forall_elim cqs
                    |> fold implies_elim_swp ags

        fun mk_call_info (rcfix, rcassm, rcarg) RI =
            let
                val llRI = RI
                             |> fold forall_elim cqs
                             |> fold (forall_elim o cert o Free) rcfix
                             |> fold implies_elim_swp ags
                             |> fold implies_elim_swp rcassm

                val h_assum =
                    Trueprop (G $ rcarg $ (h $ rcarg))
                              |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
                              |> fold_rev (mk_forall o Free) rcfix
                              |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] []
                              |> abstract_over_list (rev qs)
            in
                RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum}
            end

        val RC_infos = map2 mk_call_info RCs RIntro_thms
    in
        ClauseInfo
            {
             no=no,
             cdata=cdata,
             qglr=qglr,

             lGI=lGI, 
             RCs=RC_infos,
             tree=tree
            }
    end







(* replace this by a table later*)
fun store_compat_thms 0 thms = []
  | store_compat_thms n thms =
    let
        val (thms1, thms2) = chop n thms
    in
        (thms1 :: store_compat_thms (n - 1) thms2)
    end

(* expects i <= j *)
fun lookup_compat_thm i j cts =
    nth (nth cts (i - 1)) (j - i)

(* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *)
(* if j < i, then turn around *)
fun get_compat_thm thy cts i j ctxi ctxj = 
    let
      val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
      val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
          
      val lhsi_eq_lhsj = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj)))
    in if j < i then
         let
           val compat = lookup_compat_thm j i cts
         in
           compat         (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
                |> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
                |> fold implies_elim_swp agsj
                |> fold implies_elim_swp agsi
                |> implies_elim_swp ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
         end
       else
         let
           val compat = lookup_compat_thm i j cts
         in
               compat        (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
                 |> fold forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
                 |> fold implies_elim_swp agsi
                 |> fold implies_elim_swp agsj
                 |> implies_elim_swp (assume lhsi_eq_lhsj)
                 |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
         end
    end




(* Generates the replacement lemma in fully quantified form. *)
fun mk_replacement_lemma thy h ih_elim clause =
    let
        val ClauseInfo {cdata=ClauseContext {qs, lhs, rhs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause

        val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_elim

        val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
        val h_assums = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs

        val ih_elim_case_inst = instantiate' [] [NONE, SOME (cterm_of thy h)] ih_elim_case (* Should be done globally *)

        val (eql, _) = FundefCtxTree.rewrite_by_tree thy h ih_elim_case_inst (Ris ~~ h_assums) tree

        val replace_lemma = (eql RS meta_eq_to_obj_eq)
                                |> implies_intr (cprop_of case_hyp)
                                |> fold_rev (implies_intr o cprop_of) h_assums
                                |> fold_rev (implies_intr o cprop_of) ags
                                |> fold_rev forall_intr cqs
                                |> Goal.close_result
    in
      replace_lemma
    end


fun mk_uniqueness_clause thy globals f compat_store clausei clausej RLj =
    let
        val Globals {h, y, x, fvar, ...} = globals
        val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei
        val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej

        val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...} 
            = mk_clause_context x ctxti cdescj

        val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
        val compat = get_compat_thm thy compat_store i j cctxi cctxj
        val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj

        val RLj_import = 
            RLj |> fold forall_elim cqsj'
                |> fold implies_elim_swp agsj'
                |> fold implies_elim_swp Ghsj'

        val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h))))
        val lhsi_eq_lhsj' = assume (cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
    in
        (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
        |> implies_elim RLj_import (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
        |> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
        |> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
        |> fold_rev (implies_intr o cprop_of) Ghsj'
        |> fold_rev (implies_intr o cprop_of) agsj' (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)
        |> implies_intr (cprop_of y_eq_rhsj'h)
        |> implies_intr (cprop_of lhsi_eq_lhsj')
        |> fold_rev forall_intr (cterm_of thy h :: cqsj')
    end



fun mk_uniqueness_case ctxt thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
    let
        val Globals {x, y, ranT, fvar, ...} = globals
        val ClauseInfo {cdata = ClauseContext {lhs, rhs, qs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
        val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs

        val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro

        fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
                                                            |> fold_rev (implies_intr o cprop_of) CCas
                                                            |> fold_rev (forall_intr o cterm_of thy o Free) RIvs

        val existence = fold (curry op COMP o prep_RC) RCs lGI

        val P = cterm_of thy (mk_eq (y, rhsC))
        val G_lhs_y = assume (cterm_of thy (Trueprop (G $ lhs $ y)))

        val unique_clauses = map2 (mk_uniqueness_clause thy globals f compat_store clausei) clauses rep_lemmas

        val uniqueness = G_cases
                           |> forall_elim (cterm_of thy lhs)
                           |> forall_elim (cterm_of thy y)
                           |> forall_elim P
                           |> implies_elim_swp G_lhs_y
                           |> fold implies_elim_swp unique_clauses
                           |> implies_intr (cprop_of G_lhs_y)
                           |> forall_intr (cterm_of thy y)

        val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)

        val exactly_one =
            ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
                 |> curry (op COMP) existence
                 |> curry (op COMP) uniqueness
                 |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
                 |> implies_intr (cprop_of case_hyp)
                 |> fold_rev (implies_intr o cprop_of) ags
                 |> fold_rev forall_intr cqs

        val function_value =
            existence
              |> implies_intr ihyp
              |> implies_intr (cprop_of case_hyp)
              |> forall_intr (cterm_of thy x)
              |> forall_elim (cterm_of thy lhs)
              |> curry (op RS) refl
    in
        (exactly_one, function_value)
    end




fun prove_stuff ctxt congs globals G f R clauses complete compat compat_store G_elim f_def =
    let
        val Globals {h, domT, ranT, x, ...} = globals
        val thy = ProofContext.theory_of ctxt

        (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
        val ihyp = all domT $ Abs ("z", domT,
                                   implies $ Trueprop (R $ Bound 0 $ x)
                                           $ Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
                                                             Abs ("y", ranT, G $ Bound 1 $ Bound 0)))
                       |> cterm_of thy

        val ihyp_thm = assume ihyp |> forall_elim_vars 0
        val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
        val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)

        val _ = Output.debug (K "Proving Replacement lemmas...")
        val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses

        val _ = Output.debug (K "Proving cases for unique existence...")
        val (ex1s, values) = 
            split_list (map (mk_uniqueness_case ctxt thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)

        val _ = Output.debug (K "Proving: Graph is a function")
        val graph_is_function = complete
                                  |> forall_elim_vars 0
                                  |> fold (curry op COMP) ex1s
                                  |> implies_intr (ihyp)
                                  |> implies_intr (cterm_of thy (Trueprop (mk_acc domT R $ x)))
                                  |> forall_intr (cterm_of thy x)
                                  |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
                                  |> (fn it => fold (forall_intr o cterm_of thy) (term_vars (prop_of it)) it)

        val goalstate =  Conjunction.intr graph_is_function complete
                          |> Goal.close_result
                          |> Goal.protect
                          |> fold_rev (implies_intr o cprop_of) compat
                          |> implies_intr (cprop_of complete)
    in
      (goalstate, values)
    end


fun define_graph Gname fvar domT ranT clauses RCss lthy =
    let
      val GT = domT --> ranT --> boolT
      val Gvar = Free (the_single (Variable.variant_frees lthy [] [(Gname, GT)]))

      fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs =
          let
            fun mk_h_assm (rcfix, rcassm, rcarg) =
                Trueprop (Gvar $ rcarg $ (fvar $ rcarg))
                          |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
                          |> fold_rev (mk_forall o Free) rcfix
          in
            Trueprop (Gvar $ lhs $ rhs)
                      |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs
                      |> fold_rev (curry Logic.mk_implies) gs
                      |> fold_rev mk_forall (fvar :: qs)
          end
          
      val G_intros = map2 mk_GIntro clauses RCss
                     
      val (GIntro_thms, (G, G_elim, G_induct, lthy)) = 
          FundefInductiveWrap.inductive_def G_intros ((dest_Free Gvar, NoSyn), lthy)
    in
      ((G, GIntro_thms, G_elim, G_induct), lthy)
    end



fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
    let
      val f_def = 
          Abs ("x", domT, Const ("FunDef.THE_default", ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $
                                Abs ("y", ranT, G $ Bound 1 $ Bound 0))
              |> ProofContext.cert_term lthy

      val ((f, (_, f_defthm)), lthy) =
        LocalTheory.def Thm.internalK ((function_name fname, mixfix), ((fdefname, []), f_def)) lthy
    in
      ((f, f_defthm), lthy)
    end


fun define_recursion_relation Rname domT ranT fvar f qglrs clauses RCss lthy =
    let

      val RT = domT --> domT --> boolT
      val Rvar = Free (the_single (Variable.variant_frees lthy [] [(Rname, RT)]))

      fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =
          Trueprop (Rvar $ rcarg $ lhs)
                    |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
                    |> fold_rev (curry Logic.mk_implies) gs
                    |> fold_rev (mk_forall o Free) rcfix
                    |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
                    (* "!!qs xs. CS ==> G => (r, lhs) : R" *)

      val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss

      val (RIntro_thmss, (R, R_elim, _, lthy)) = 
          fold_burrow FundefInductiveWrap.inductive_def R_intross ((dest_Free Rvar, NoSyn), lthy)
    in
      ((R, RIntro_thmss, R_elim), lthy)
    end


fun fix_globals domT ranT fvar ctxt =
    let
      val ([h, y, x, z, a, D, P, Pbool],ctxt') = 
          Variable.variant_fixes ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt
    in
      (Globals {h = Free (h, domT --> ranT),
                y = Free (y, ranT),
                x = Free (x, domT),
                z = Free (z, domT),
                a = Free (a, domT),
                D = Free (D, domT --> boolT),
                P = Free (P, domT --> boolT),
                Pbool = Free (Pbool, boolT),
                fvar = fvar,
                domT = domT,
                ranT = ranT
               },
       ctxt')
    end



fun inst_RC thy fvar f (rcfix, rcassm, rcarg) =
    let
      fun inst_term t = subst_bound(f, abstract_over (fvar, t))
    in
      (rcfix, map (assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)
    end



(**********************************************************
 *                   PROVING THE RULES 
 **********************************************************)

fun mk_psimps thy globals R clauses valthms f_iff graph_is_function =
    let
      val Globals {domT, z, ...} = globals
  
      fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm =
          let
            val lhs_acc = cterm_of thy (Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
            val z_smaller = cterm_of thy (Trueprop (R $ z $ lhs)) (* "R z lhs" *)
          in
            ((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
              |> (fn it => it COMP graph_is_function)
              |> implies_intr z_smaller
              |> forall_intr (cterm_of thy z)
              |> (fn it => it COMP valthm)
              |> implies_intr lhs_acc 
              |> asm_simplify (HOL_basic_ss addsimps [f_iff])
              |> fold_rev (implies_intr o cprop_of) ags
              |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
          end
    in
      map2 mk_psimp clauses valthms
    end


(** Induction rule **)


val acc_subset_induct = thm "Fun.predicate1I" RS
  thm "Accessible_Part.acc_subset_induct"

fun mk_partial_induct_rule thy globals R complete_thm clauses =
    let
      val Globals {domT, x, z, a, P, D, ...} = globals
      val acc_R = mk_acc domT R
                  
      val x_D = assume (cterm_of thy (Trueprop (D $ x)))
      val a_D = cterm_of thy (Trueprop (D $ a))
                
      val D_subset = cterm_of thy (mk_forall x (implies $ Trueprop (D $ x) $ Trueprop (acc_R $ x)))
                     
      val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
                    mk_forall x
                    (mk_forall z (Logic.mk_implies (Trueprop (D $ x),
                                                    Logic.mk_implies (Trueprop (R $ z $ x),
                                                                      Trueprop (D $ z)))))
                    |> cterm_of thy
                    
                    
  (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
      val ihyp = all domT $ Abs ("z", domT, 
               implies $ Trueprop (R $ Bound 0 $ x)
             $ Trueprop (P $ Bound 0))
           |> cterm_of thy

      val aihyp = assume ihyp

  fun prove_case clause =
      let
    val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, gs, lhs, case_hyp, ...}, RCs, 
                    qglr = (oqs, _, _, _), ...} = clause
                       
    val replace_x_ss = HOL_basic_ss addsimps [case_hyp]
    val lhs_D = simplify replace_x_ss x_D (* lhs : D *)
    val sih = full_simplify replace_x_ss aihyp
          
    fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
        sih |> forall_elim (cterm_of thy rcarg)
            |> implies_elim_swp llRI
            |> fold_rev (implies_intr o cprop_of) CCas
            |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
        
    val P_recs = map mk_Prec RCs   (*  [P rec1, P rec2, ... ]  *)
                 
    val step = Trueprop (P $ lhs)
            |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
            |> fold_rev (curry Logic.mk_implies) gs
            |> curry Logic.mk_implies (Trueprop (D $ lhs))
            |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
            |> cterm_of thy
         
    val P_lhs = assume step
           |> fold forall_elim cqs
           |> implies_elim_swp lhs_D 
           |> fold implies_elim_swp ags
           |> fold implies_elim_swp P_recs
          
    val res = cterm_of thy (Trueprop (P $ x))
           |> Simplifier.rewrite replace_x_ss
           |> symmetric (* P lhs == P x *)
           |> (fn eql => equal_elim eql P_lhs) (* "P x" *)
           |> implies_intr (cprop_of case_hyp)
           |> fold_rev (implies_intr o cprop_of) ags
           |> fold_rev forall_intr cqs
      in
        (res, step)
      end
      
  val (cases, steps) = split_list (map prove_case clauses)
                       
  val istep = complete_thm
                |> forall_elim_vars 0
                |> fold (curry op COMP) cases (*  P x  *)
                |> implies_intr ihyp
                |> implies_intr (cprop_of x_D)
                |> forall_intr (cterm_of thy x)
         
  val subset_induct_rule = 
      acc_subset_induct
        |> (curry op COMP) (assume D_subset)
        |> (curry op COMP) (assume D_dcl)
        |> (curry op COMP) (assume a_D)
        |> (curry op COMP) istep
        |> fold_rev implies_intr steps
        |> implies_intr a_D
        |> implies_intr D_dcl
        |> implies_intr D_subset

  val subset_induct_all = fold_rev (forall_intr o cterm_of thy) [P, a, D] subset_induct_rule

  val simple_induct_rule =
      subset_induct_rule
        |> forall_intr (cterm_of thy D)
        |> forall_elim (cterm_of thy acc_R)
        |> assume_tac 1 |> Seq.hd
        |> (curry op COMP) (acc_downward
                              |> (instantiate' [SOME (ctyp_of thy domT)]
                                               (map (SOME o cterm_of thy) [R, x, z]))
                              |> forall_intr (cterm_of thy z)
                              |> forall_intr (cterm_of thy x))
        |> forall_intr (cterm_of thy a)
        |> forall_intr (cterm_of thy P)
    in
      (subset_induct_all, simple_induct_rule)
    end



(* FIXME: This should probably use fixed goals, to be more reliable and faster *)
fun mk_domain_intro thy (Globals {domT, ...}) R R_cases clause =
    let
      val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...}, 
                      qglr = (oqs, _, _, _), ...} = clause
      val goal = Trueprop (mk_acc domT R $ lhs)
                          |> fold_rev (curry Logic.mk_implies) gs
                          |> cterm_of thy
    in
      Goal.init goal 
      |> (SINGLE (resolve_tac [accI] 1)) |> the
      |> (SINGLE (eresolve_tac [forall_elim_vars 0 R_cases] 1))  |> the
      |> (SINGLE (CLASIMPSET auto_tac)) |> the
      |> Goal.conclude
      |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
    end



(** Termination rule **)

val wf_induct_rule = thm "Wellfounded_Recursion.wfP_induct_rule";
val wf_in_rel = thm "Wellfounded_Recursion.wf_implies_wfP";
val in_rel_def = thm "Predicate.member2_eq";

fun mk_nest_term_case thy globals R' ihyp clause =
    let
      val Globals {x, z, ...} = globals
      val ClauseInfo {cdata = ClauseContext {qs,cqs,ags,lhs,rhs,case_hyp,...},tree,
                      qglr=(oqs, _, _, _), ...} = clause
          
      val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
                    
      fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) = 
          let
            val used = map (fn ((f,a),thm) => FundefCtxTree.export_thm thy (f, map prop_of a) thm) (u @ sub)
                       
            val hyp = Trueprop (R' $ arg $ lhs)
                      |> fold_rev (curry Logic.mk_implies o prop_of) used
                      |> FundefCtxTree.export_term (fixes, map prop_of assumes) 
                      |> fold_rev (curry Logic.mk_implies o prop_of) ags
                      |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
                      |> cterm_of thy
                      
            val thm = assume hyp
                      |> fold forall_elim cqs
                      |> fold implies_elim_swp ags
                      |> FundefCtxTree.import_thm thy (fixes, assumes) (*  "(arg, lhs) : R'"  *)
                      |> fold implies_elim_swp used
                      
            val acc = thm COMP ih_case
                      
            val z_eq_arg = cterm_of thy (Trueprop (HOLogic.mk_eq (z, arg)))
                           
            val arg_eq_z = (assume z_eq_arg) RS sym
                           
            val z_acc = simplify (HOL_basic_ss addsimps [arg_eq_z]) acc (* fragile, slow... *)
                        |> implies_intr (cprop_of case_hyp)
                        |> implies_intr z_eq_arg

            val z_eq_arg = assume (cterm_of thy (Trueprop (mk_eq (z, arg))))
            val x_eq_lhs = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
                           
            val ethm = (z_acc OF [z_eq_arg, x_eq_lhs])
                         |> FundefCtxTree.export_thm thy (fixes, 
                                                          prop_of z_eq_arg :: prop_of x_eq_lhs :: map prop_of (ags @ assumes))
                         |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)

            val sub' = sub @ [(([],[]), acc)]
          in
            (sub', (hyp :: hyps, ethm :: thms))
          end
        | step _ _ _ _ = raise Match
    in
      FundefCtxTree.traverse_tree step tree
    end


fun mk_nest_term_rule thy globals R R_cases clauses =
    let
      val Globals { domT, x, z, ... } = globals
      val acc_R = mk_acc domT R
                  
      val R' = Free ("R", fastype_of R)
               
      val Rrel = Free ("R", mk_relT (domT, domT))
      val inrel_R = Const ("Predicate.member2", mk_relT (domT, domT) --> fastype_of R) $ Rrel
                    
      val wfR' = cterm_of thy (Trueprop (Const ("Wellfounded_Recursion.wfP", (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
                          
      (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
      val ihyp = all domT $ Abs ("z", domT, 
                                 implies $ Trueprop (R' $ Bound 0 $ x)
                                         $ Trueprop (acc_R $ Bound 0))
                     |> cterm_of thy

      val ihyp_a = assume ihyp |> forall_elim_vars 0
                   
      val R_z_x = cterm_of thy (Trueprop (R $ z $ x)) 
                  
      val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[])
    in
      R_cases
        |> forall_elim (cterm_of thy z)
        |> forall_elim (cterm_of thy x)
        |> forall_elim (cterm_of thy (acc_R $ z))
        |> curry op COMP (assume R_z_x)
        |> fold_rev (curry op COMP) cases
        |> implies_intr R_z_x
        |> forall_intr (cterm_of thy z)
        |> (fn it => it COMP accI)
        |> implies_intr ihyp
        |> forall_intr (cterm_of thy x)
        |> (fn it => Drule.compose_single(it,2,wf_induct_rule))
        |> curry op RS (assume wfR')
        |> forall_intr_vars
        |> (fn it => it COMP allI)
        |> fold implies_intr hyps
        |> implies_intr wfR'
        |> forall_intr (cterm_of thy R')
        |> forall_elim (cterm_of thy (inrel_R))
        |> curry op RS wf_in_rel
        |> full_simplify (HOL_basic_ss addsimps [in_rel_def])
        |> forall_intr (cterm_of thy Rrel)
    end
    


(* Tail recursion (probably very fragile)
 *
 * FIXME:
 * - Need to do forall_elim_vars on psimps: Unneccesary, if psimps would be taken from the same context.
 * - Must we really replace the fvar by f here?
 * - Splitting is not configured automatically: Problems with case?
 *)
fun mk_trsimps octxt globals f G R f_def R_cases G_induct clauses psimps =
    let
      val Globals {domT, ranT, fvar, ...} = globals

      val R_cases = forall_elim_vars 0 R_cases (* FIXME: Should be already in standard form. *)

      val graph_implies_dom = (* "G ?x ?y ==> dom ?x"  *)
          Goal.prove octxt ["x", "y"] [HOLogic.mk_Trueprop (G $ Free ("x", domT) $ Free ("y", ranT))]
                     (HOLogic.mk_Trueprop (mk_acc domT R $ Free ("x", domT)))
                     (fn {prems=[a], ...} => 
                         ((rtac (G_induct OF [a]))
                            THEN_ALL_NEW (rtac accI)
                            THEN_ALL_NEW (etac R_cases)
                            THEN_ALL_NEW (SIMPSET' asm_full_simp_tac)) 1)

      val default_thm = (forall_intr_vars graph_implies_dom) COMP (f_def COMP fundef_default_value)

      fun mk_trsimp clause psimp =
          let
            val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {ctxt, cqs, qs, gs, lhs, rhs, ...}, ...} = clause
            val thy = ProofContext.theory_of ctxt
            val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs
                        
            val trsimp = Logic.list_implies(gs, HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *)
            val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *)
          in
            Goal.prove ctxt [] [] trsimp
                       (fn _ =>  
                           rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
                                THEN (rtac (forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
                                THEN (SIMPSET (fn ss => asm_full_simp_tac (ss addsimps [default_thm]) 1))
                                THEN (etac not_acc_down 1)
                                THEN ((etac R_cases) THEN_ALL_NEW (SIMPSET' (fn ss => asm_full_simp_tac (ss addsimps [default_thm])))) 1)
              |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
          end
    in
      map2 mk_trsimp clauses psimps
    end


fun prepare_fundef config defname [((fname, fT), mixfix)] abstract_qglrs lthy =
    let
      val FundefConfig {domintros, tailrec, default=default_str, ...} = config 
                                                         
      val fvar = Free (fname, fT)
      val domT = domain_type fT
      val ranT = range_type fT
                            
      val default = singleton (ProofContext.read_termTs lthy) (default_str, fT)

      val congs = get_fundef_congs (Context.Proof lthy)
      val (globals, ctxt') = fix_globals domT ranT fvar lthy

      val Globals { x, h, ... } = globals

      val clauses = map (mk_clause_context x ctxt') abstract_qglrs 

      val n = length abstract_qglrs

      val congs_deps = map (fn c => (c, FundefCtxTree.cong_deps c)) (congs @ FundefCtxTree.add_congs) (* FIXME: Save in theory *)
              
      fun build_tree (ClauseContext { ctxt, rhs, ...}) = 
            FundefCtxTree.mk_tree congs_deps (fname, fT) h ctxt rhs

      val trees = map build_tree clauses
      val RCss = map find_calls trees

      val ((G, GIntro_thms, G_elim, G_induct), lthy) = 
          PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy

      val ((f, f_defthm), lthy) = 
          PROFILE "def_fun" (define_function (defname ^ "_sum_def") (fname, mixfix) domT ranT G default) lthy

      val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
      val trees = map (FundefCtxTree.inst_tree (ProofContext.theory_of lthy) fvar f) trees

      val ((R, RIntro_thmss, R_elim), lthy) = 
          PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy

      val (_, lthy) = 
          LocalTheory.abbrev Syntax.default_mode ((dom_name defname, NoSyn), mk_acc domT R) lthy

      val newthy = ProofContext.theory_of lthy
      val clauses = map (transfer_clause_ctx newthy) clauses

      val cert = cterm_of (ProofContext.theory_of lthy)

      val xclauses = PROFILE "xclauses" (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees RCss GIntro_thms) RIntro_thmss

      val complete = mk_completeness globals clauses abstract_qglrs |> cert |> assume
      val compat = mk_compat_proof_obligations domT ranT fvar f abstract_qglrs |> map (cert #> assume)

      val compat_store = store_compat_thms n compat

      val (goalstate, values) = PROFILE "prove_stuff" (prove_stuff lthy congs globals G f R xclauses complete compat compat_store G_elim) f_defthm

      val mk_trsimps = mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses

      fun mk_partial_rules provedgoal =
          let
            val newthy = theory_of_thm provedgoal (*FIXME*) 

            val (graph_is_function, complete_thm) = 
                provedgoal
                  |> Conjunction.elim
                  |> apfst (forall_elim_vars 0)
                
            val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)
                        
            val psimps = PROFILE "Proving simplification rules" (mk_psimps newthy globals R xclauses values f_iff) graph_is_function
                         
            val (subset_pinduct, simple_pinduct) = PROFILE "Proving partial induction rule" 
                                                           (mk_partial_induct_rule newthy globals R complete_thm) xclauses
                                                   
                                                   
            val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule newthy globals R R_elim) xclauses
                              
            val dom_intros = if domintros 
                             then SOME (PROFILE "Proving domain introduction rules" (map (mk_domain_intro newthy globals R R_elim)) xclauses)
                             else NONE
            val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE
                                                                        
          in 
            FundefResult {fs=[f], G=G, R=R, cases=complete_thm, 
                          psimps=psimps, subset_pinducts=[subset_pinduct], simple_pinducts=[simple_pinduct], 
                          termination=total_intro, trsimps=trsimps,
                          domintros=dom_intros}
          end
    in
      ((f, goalstate, mk_partial_rules), lthy)
    end




end