src/HOL/Tools/Function/function_core.ML
changeset 34232 36a2a3029fd3
parent 34065 6f8f9835e219
child 36270 fd95c0514623
     1.1 --- a/src/HOL/Tools/Function/function_core.ML	Sat Jan 02 23:18:58 2010 +0100
     1.2 +++ b/src/HOL/Tools/Function/function_core.ML	Sat Jan 02 23:18:58 2010 +0100
     1.3 @@ -7,26 +7,25 @@
     1.4  
     1.5  signature FUNCTION_CORE =
     1.6  sig
     1.7 -    val trace: bool Unsynchronized.ref
     1.8 +  val trace: bool Unsynchronized.ref
     1.9  
    1.10 -    val prepare_function : Function_Common.function_config
    1.11 -                         -> string (* defname *)
    1.12 -                         -> ((bstring * typ) * mixfix) list (* defined symbol *)
    1.13 -                         -> ((bstring * typ) list * term list * term * term) list (* specification *)
    1.14 -                         -> local_theory
    1.15 -
    1.16 -                         -> (term   (* f *)
    1.17 -                             * thm  (* goalstate *)
    1.18 -                             * (thm -> Function_Common.function_result) (* continuation *)
    1.19 -                            ) * local_theory
    1.20 +  val prepare_function : Function_Common.function_config
    1.21 +    -> string (* defname *)
    1.22 +    -> ((bstring * typ) * mixfix) list (* defined symbol *)
    1.23 +    -> ((bstring * typ) list * term list * term * term) list (* specification *)
    1.24 +    -> local_theory
    1.25 +    -> (term   (* f *)
    1.26 +        * thm  (* goalstate *)
    1.27 +        * (thm -> Function_Common.function_result) (* continuation *)
    1.28 +       ) * local_theory
    1.29  
    1.30  end
    1.31  
    1.32  structure Function_Core : FUNCTION_CORE =
    1.33  struct
    1.34  
    1.35 -val trace = Unsynchronized.ref false;
    1.36 -fun trace_msg msg = if ! trace then tracing (msg ()) else ();
    1.37 +val trace = Unsynchronized.ref false
    1.38 +fun trace_msg msg = if ! trace then tracing (msg ()) else ()
    1.39  
    1.40  val boolT = HOLogic.boolT
    1.41  val mk_eq = HOLogic.mk_eq
    1.42 @@ -34,149 +33,134 @@
    1.43  open Function_Lib
    1.44  open Function_Common
    1.45  
    1.46 -datatype globals =
    1.47 -   Globals of {
    1.48 -         fvar: term,
    1.49 -         domT: typ,
    1.50 -         ranT: typ,
    1.51 -         h: term,
    1.52 -         y: term,
    1.53 -         x: term,
    1.54 -         z: term,
    1.55 -         a: term,
    1.56 -         P: term,
    1.57 -         D: term,
    1.58 -         Pbool:term
    1.59 -}
    1.60 +datatype globals = Globals of
    1.61 + {fvar: term,
    1.62 +  domT: typ,
    1.63 +  ranT: typ,
    1.64 +  h: term,
    1.65 +  y: term,
    1.66 +  x: term,
    1.67 +  z: term,
    1.68 +  a: term,
    1.69 +  P: term,
    1.70 +  D: term,
    1.71 +  Pbool:term}
    1.72 +
    1.73 +datatype rec_call_info = RCInfo of
    1.74 + {RIvs: (string * typ) list,  (* Call context: fixes and assumes *)
    1.75 +  CCas: thm list,
    1.76 +  rcarg: term,                 (* The recursive argument *)
    1.77 +  llRI: thm,
    1.78 +  h_assum: term}
    1.79  
    1.80  
    1.81 -datatype rec_call_info =
    1.82 -  RCInfo of
    1.83 -  {
    1.84 -   RIvs: (string * typ) list,  (* Call context: fixes and assumes *)
    1.85 -   CCas: thm list,
    1.86 -   rcarg: term,                 (* The recursive argument *)
    1.87 -
    1.88 -   llRI: thm,
    1.89 -   h_assum: term
    1.90 -  }
    1.91 -
    1.92 -
    1.93 -datatype clause_context =
    1.94 -  ClauseContext of
    1.95 -  {
    1.96 -    ctxt : Proof.context,
    1.97 -
    1.98 -    qs : term list,
    1.99 -    gs : term list,
   1.100 -    lhs: term,
   1.101 -    rhs: term,
   1.102 -
   1.103 -    cqs: cterm list,
   1.104 -    ags: thm list,
   1.105 -    case_hyp : thm
   1.106 -  }
   1.107 +datatype clause_context = ClauseContext of
   1.108 + {ctxt : Proof.context,
   1.109 +  qs : term list,
   1.110 +  gs : term list,
   1.111 +  lhs: term,
   1.112 +  rhs: term,
   1.113 +  cqs: cterm list,
   1.114 +  ags: thm list,
   1.115 +  case_hyp : thm}
   1.116  
   1.117  
   1.118  fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) =
   1.119 -    ClauseContext { ctxt = ProofContext.transfer thy ctxt,
   1.120 -                    qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp }
   1.121 +  ClauseContext { ctxt = ProofContext.transfer thy ctxt,
   1.122 +    qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp }
   1.123  
   1.124  
   1.125 -datatype clause_info =
   1.126 -  ClauseInfo of
   1.127 -     {
   1.128 -      no: int,
   1.129 -      qglr : ((string * typ) list * term list * term * term),
   1.130 -      cdata : clause_context,
   1.131 -
   1.132 -      tree: Function_Ctx_Tree.ctx_tree,
   1.133 -      lGI: thm,
   1.134 -      RCs: rec_call_info list
   1.135 -     }
   1.136 +datatype clause_info = ClauseInfo of
   1.137 + {no: int,
   1.138 +  qglr : ((string * typ) list * term list * term * term),
   1.139 +  cdata : clause_context,
   1.140 +  tree: Function_Ctx_Tree.ctx_tree,
   1.141 +  lGI: thm,
   1.142 +  RCs: rec_call_info list}
   1.143  
   1.144  
   1.145  (* Theory dependencies. *)
   1.146 -val acc_induct_rule = @{thm accp_induct_rule};
   1.147 +val acc_induct_rule = @{thm accp_induct_rule}
   1.148  
   1.149 -val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence};
   1.150 -val ex1_implies_un = @{thm FunDef.fundef_ex1_uniqueness};
   1.151 -val ex1_implies_iff = @{thm FunDef.fundef_ex1_iff};
   1.152 +val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence}
   1.153 +val ex1_implies_un = @{thm FunDef.fundef_ex1_uniqueness}
   1.154 +val ex1_implies_iff = @{thm FunDef.fundef_ex1_iff}
   1.155  
   1.156 -val acc_downward = @{thm accp_downward};
   1.157 -val accI = @{thm accp.accI};
   1.158 -val case_split = @{thm HOL.case_split};
   1.159 -val fundef_default_value = @{thm FunDef.fundef_default_value};
   1.160 -val not_acc_down = @{thm not_accp_down};
   1.161 +val acc_downward = @{thm accp_downward}
   1.162 +val accI = @{thm accp.accI}
   1.163 +val case_split = @{thm HOL.case_split}
   1.164 +val fundef_default_value = @{thm FunDef.fundef_default_value}
   1.165 +val not_acc_down = @{thm not_accp_down}
   1.166  
   1.167  
   1.168  
   1.169  fun find_calls tree =
   1.170 -    let
   1.171 -      fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) = ([], (fixes, assumes, arg) :: xs)
   1.172 -        | add_Ri _ _ _ _ = raise Match
   1.173 -    in
   1.174 -      rev (Function_Ctx_Tree.traverse_tree add_Ri tree [])
   1.175 -    end
   1.176 +  let
   1.177 +    fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) =
   1.178 +      ([], (fixes, assumes, arg) :: xs)
   1.179 +      | add_Ri _ _ _ _ = raise Match
   1.180 +  in
   1.181 +    rev (Function_Ctx_Tree.traverse_tree add_Ri tree [])
   1.182 +  end
   1.183  
   1.184  
   1.185  (** building proof obligations *)
   1.186  
   1.187  fun mk_compat_proof_obligations domT ranT fvar f glrs =
   1.188 -    let
   1.189 -      fun mk_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
   1.190 -          let
   1.191 -            val shift = incr_boundvars (length qs')
   1.192 -          in
   1.193 -            Logic.mk_implies
   1.194 -              (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'),
   1.195 -                HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs'))
   1.196 -              |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
   1.197 -              |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs')
   1.198 -              |> curry abstract_over fvar
   1.199 -              |> curry subst_bound f
   1.200 -          end
   1.201 -    in
   1.202 -      map mk_impl (unordered_pairs glrs)
   1.203 -    end
   1.204 +  let
   1.205 +    fun mk_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
   1.206 +      let
   1.207 +        val shift = incr_boundvars (length qs')
   1.208 +      in
   1.209 +        Logic.mk_implies
   1.210 +          (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'),
   1.211 +            HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs'))
   1.212 +        |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
   1.213 +        |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs')
   1.214 +        |> curry abstract_over fvar
   1.215 +        |> curry subst_bound f
   1.216 +      end
   1.217 +  in
   1.218 +    map mk_impl (unordered_pairs glrs)
   1.219 +  end
   1.220  
   1.221  
   1.222  fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs =
   1.223 -    let
   1.224 -        fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) =
   1.225 -            HOLogic.mk_Trueprop Pbool
   1.226 -                     |> curry Logic.mk_implies (HOLogic.mk_Trueprop (mk_eq (x, lhs)))
   1.227 -                     |> fold_rev (curry Logic.mk_implies) gs
   1.228 -                     |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
   1.229 -    in
   1.230 -        HOLogic.mk_Trueprop Pbool
   1.231 -                 |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs)
   1.232 -                 |> mk_forall_rename ("x", x)
   1.233 -                 |> mk_forall_rename ("P", Pbool)
   1.234 -    end
   1.235 +  let
   1.236 +    fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) =
   1.237 +      HOLogic.mk_Trueprop Pbool
   1.238 +      |> curry Logic.mk_implies (HOLogic.mk_Trueprop (mk_eq (x, lhs)))
   1.239 +      |> fold_rev (curry Logic.mk_implies) gs
   1.240 +      |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
   1.241 +  in
   1.242 +    HOLogic.mk_Trueprop Pbool
   1.243 +    |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs)
   1.244 +    |> mk_forall_rename ("x", x)
   1.245 +    |> mk_forall_rename ("P", Pbool)
   1.246 +  end
   1.247  
   1.248  (** making a context with it's own local bindings **)
   1.249  
   1.250  fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) =
   1.251 -    let
   1.252 -      val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt
   1.253 -                                           |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
   1.254 +  let
   1.255 +    val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt
   1.256 +      |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
   1.257  
   1.258 -      val thy = ProofContext.theory_of ctxt'
   1.259 +    val thy = ProofContext.theory_of ctxt'
   1.260  
   1.261 -      fun inst t = subst_bounds (rev qs, t)
   1.262 -      val gs = map inst pre_gs
   1.263 -      val lhs = inst pre_lhs
   1.264 -      val rhs = inst pre_rhs
   1.265 +    fun inst t = subst_bounds (rev qs, t)
   1.266 +    val gs = map inst pre_gs
   1.267 +    val lhs = inst pre_lhs
   1.268 +    val rhs = inst pre_rhs
   1.269  
   1.270 -      val cqs = map (cterm_of thy) qs
   1.271 -      val ags = map (assume o cterm_of thy) gs
   1.272 +    val cqs = map (cterm_of thy) qs
   1.273 +    val ags = map (assume o cterm_of thy) gs
   1.274  
   1.275 -      val case_hyp = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
   1.276 -    in
   1.277 -      ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
   1.278 -                      cqs = cqs, ags = ags, case_hyp = case_hyp }
   1.279 -    end
   1.280 +    val case_hyp = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
   1.281 +  in
   1.282 +    ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
   1.283 +      cqs = cqs, ags = ags, case_hyp = case_hyp }
   1.284 +  end
   1.285  
   1.286  
   1.287  (* lowlevel term function. FIXME: remove *)
   1.288 @@ -188,7 +172,7 @@
   1.289          (case tm of
   1.290            Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t)
   1.291          | t $ u => abs lev v t $ abs lev v u
   1.292 -        | t => t);
   1.293 +        | t => t)
   1.294    in
   1.295      fold_index (fn (i, v) => fn t => abs i v t) vs body
   1.296    end
   1.297 @@ -196,258 +180,249 @@
   1.298  
   1.299  
   1.300  fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms =
   1.301 -    let
   1.302 -        val Globals {h, ...} = globals
   1.303 +  let
   1.304 +    val Globals {h, ...} = globals
   1.305  
   1.306 -        val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
   1.307 -        val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
   1.308 +    val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
   1.309 +    val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
   1.310  
   1.311 -        (* Instantiate the GIntro thm with "f" and import into the clause context. *)
   1.312 -        val lGI = GIntro_thm
   1.313 -                    |> forall_elim (cert f)
   1.314 -                    |> fold forall_elim cqs
   1.315 -                    |> fold Thm.elim_implies ags
   1.316 -
   1.317 -        fun mk_call_info (rcfix, rcassm, rcarg) RI =
   1.318 -            let
   1.319 -                val llRI = RI
   1.320 -                             |> fold forall_elim cqs
   1.321 -                             |> fold (forall_elim o cert o Free) rcfix
   1.322 -                             |> fold Thm.elim_implies ags
   1.323 -                             |> fold Thm.elim_implies rcassm
   1.324 +    (* Instantiate the GIntro thm with "f" and import into the clause context. *)
   1.325 +    val lGI = GIntro_thm
   1.326 +      |> forall_elim (cert f)
   1.327 +      |> fold forall_elim cqs
   1.328 +      |> fold Thm.elim_implies ags
   1.329  
   1.330 -                val h_assum =
   1.331 -                    HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg))
   1.332 -                              |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
   1.333 -                              |> fold_rev (Logic.all o Free) rcfix
   1.334 -                              |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] []
   1.335 -                              |> abstract_over_list (rev qs)
   1.336 -            in
   1.337 -                RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum}
   1.338 -            end
   1.339 +    fun mk_call_info (rcfix, rcassm, rcarg) RI =
   1.340 +      let
   1.341 +        val llRI = RI
   1.342 +          |> fold forall_elim cqs
   1.343 +          |> fold (forall_elim o cert o Free) rcfix
   1.344 +          |> fold Thm.elim_implies ags
   1.345 +          |> fold Thm.elim_implies rcassm
   1.346  
   1.347 -        val RC_infos = map2 mk_call_info RCs RIntro_thms
   1.348 -    in
   1.349 -        ClauseInfo
   1.350 -            {
   1.351 -             no=no,
   1.352 -             cdata=cdata,
   1.353 -             qglr=qglr,
   1.354 +        val h_assum =
   1.355 +          HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg))
   1.356 +          |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
   1.357 +          |> fold_rev (Logic.all o Free) rcfix
   1.358 +          |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] []
   1.359 +          |> abstract_over_list (rev qs)
   1.360 +      in
   1.361 +        RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum}
   1.362 +      end
   1.363  
   1.364 -             lGI=lGI,
   1.365 -             RCs=RC_infos,
   1.366 -             tree=tree
   1.367 -            }
   1.368 -    end
   1.369 +    val RC_infos = map2 mk_call_info RCs RIntro_thms
   1.370 +  in
   1.371 +    ClauseInfo {no=no, cdata=cdata, qglr=qglr, lGI=lGI, RCs=RC_infos,
   1.372 +      tree=tree}
   1.373 +  end
   1.374  
   1.375  
   1.376 -
   1.377 -
   1.378 -
   1.379 -
   1.380 -
   1.381 -(* replace this by a table later*)
   1.382  fun store_compat_thms 0 thms = []
   1.383    | store_compat_thms n thms =
   1.384 -    let
   1.385 -        val (thms1, thms2) = chop n thms
   1.386 -    in
   1.387 -        (thms1 :: store_compat_thms (n - 1) thms2)
   1.388 -    end
   1.389 +  let
   1.390 +    val (thms1, thms2) = chop n thms
   1.391 +  in
   1.392 +    (thms1 :: store_compat_thms (n - 1) thms2)
   1.393 +  end
   1.394  
   1.395  (* expects i <= j *)
   1.396  fun lookup_compat_thm i j cts =
   1.397 -    nth (nth cts (i - 1)) (j - i)
   1.398 +  nth (nth cts (i - 1)) (j - i)
   1.399  
   1.400  (* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *)
   1.401  (* if j < i, then turn around *)
   1.402  fun get_compat_thm thy cts i j ctxi ctxj =
   1.403 -    let
   1.404 -      val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
   1.405 -      val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
   1.406 +  let
   1.407 +    val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
   1.408 +    val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
   1.409  
   1.410 -      val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))
   1.411 -    in if j < i then
   1.412 -         let
   1.413 -           val compat = lookup_compat_thm j i cts
   1.414 -         in
   1.415 -           compat         (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
   1.416 -                |> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
   1.417 -                |> fold Thm.elim_implies agsj
   1.418 -                |> fold Thm.elim_implies agsi
   1.419 -                |> Thm.elim_implies ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
   1.420 -         end
   1.421 -       else
   1.422 -         let
   1.423 -           val compat = lookup_compat_thm i j cts
   1.424 -         in
   1.425 -               compat        (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
   1.426 -                 |> fold forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
   1.427 -                 |> fold Thm.elim_implies agsi
   1.428 -                 |> fold Thm.elim_implies agsj
   1.429 -                 |> Thm.elim_implies (assume lhsi_eq_lhsj)
   1.430 -                 |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
   1.431 -         end
   1.432 +    val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))
   1.433 +  in if j < i then
   1.434 +    let
   1.435 +      val compat = lookup_compat_thm j i cts
   1.436 +    in
   1.437 +      compat         (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
   1.438 +      |> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
   1.439 +      |> fold Thm.elim_implies agsj
   1.440 +      |> fold Thm.elim_implies agsi
   1.441 +      |> Thm.elim_implies ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
   1.442      end
   1.443 -
   1.444 -
   1.445 -
   1.446 +    else
   1.447 +    let
   1.448 +      val compat = lookup_compat_thm i j cts
   1.449 +    in
   1.450 +      compat        (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
   1.451 +      |> fold forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
   1.452 +      |> fold Thm.elim_implies agsi
   1.453 +      |> fold Thm.elim_implies agsj
   1.454 +      |> Thm.elim_implies (assume lhsi_eq_lhsj)
   1.455 +      |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
   1.456 +    end
   1.457 +  end
   1.458  
   1.459  (* Generates the replacement lemma in fully quantified form. *)
   1.460  fun mk_replacement_lemma thy h ih_elim clause =
   1.461 -    let
   1.462 -        val ClauseInfo {cdata=ClauseContext {qs, lhs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause
   1.463 -        local open Conv in
   1.464 -        val ih_conv = arg1_conv o arg_conv o arg_conv
   1.465 -        end
   1.466 +  let
   1.467 +    val ClauseInfo {cdata=ClauseContext {qs, lhs, cqs, ags, case_hyp, ...},
   1.468 +      RCs, tree, ...} = clause
   1.469 +    local open Conv in
   1.470 +      val ih_conv = arg1_conv o arg_conv o arg_conv
   1.471 +    end
   1.472  
   1.473 -        val ih_elim_case = Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_elim
   1.474 -
   1.475 -        val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
   1.476 -        val h_assums = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
   1.477 +    val ih_elim_case =
   1.478 +      Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_elim
   1.479  
   1.480 -        val (eql, _) = Function_Ctx_Tree.rewrite_by_tree thy h ih_elim_case (Ris ~~ h_assums) tree
   1.481 +    val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
   1.482 +    val h_assums = map (fn RCInfo {h_assum, ...} =>
   1.483 +      assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
   1.484 +
   1.485 +    val (eql, _) =
   1.486 +      Function_Ctx_Tree.rewrite_by_tree thy h ih_elim_case (Ris ~~ h_assums) tree
   1.487  
   1.488 -        val replace_lemma = (eql RS meta_eq_to_obj_eq)
   1.489 -                                |> implies_intr (cprop_of case_hyp)
   1.490 -                                |> fold_rev (implies_intr o cprop_of) h_assums
   1.491 -                                |> fold_rev (implies_intr o cprop_of) ags
   1.492 -                                |> fold_rev forall_intr cqs
   1.493 -                                |> Thm.close_derivation
   1.494 -    in
   1.495 -      replace_lemma
   1.496 -    end
   1.497 +    val replace_lemma = (eql RS meta_eq_to_obj_eq)
   1.498 +      |> implies_intr (cprop_of case_hyp)
   1.499 +      |> fold_rev (implies_intr o cprop_of) h_assums
   1.500 +      |> fold_rev (implies_intr o cprop_of) ags
   1.501 +      |> fold_rev forall_intr cqs
   1.502 +      |> Thm.close_derivation
   1.503 +  in
   1.504 +    replace_lemma
   1.505 +  end
   1.506  
   1.507  
   1.508  fun mk_uniqueness_clause thy globals compat_store clausei clausej RLj =
   1.509 -    let
   1.510 -        val Globals {h, y, x, fvar, ...} = globals
   1.511 -        val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei
   1.512 -        val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej
   1.513 +  let
   1.514 +    val Globals {h, y, x, fvar, ...} = globals
   1.515 +    val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei
   1.516 +    val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej
   1.517 +
   1.518 +    val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...} =
   1.519 +      mk_clause_context x ctxti cdescj
   1.520  
   1.521 -        val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...}
   1.522 -            = mk_clause_context x ctxti cdescj
   1.523 +    val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
   1.524 +    val compat = get_compat_thm thy compat_store i j cctxi cctxj
   1.525 +    val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
   1.526  
   1.527 -        val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
   1.528 -        val compat = get_compat_thm thy compat_store i j cctxi cctxj
   1.529 -        val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
   1.530 +    val RLj_import = RLj
   1.531 +      |> fold forall_elim cqsj'
   1.532 +      |> fold Thm.elim_implies agsj'
   1.533 +      |> fold Thm.elim_implies Ghsj'
   1.534  
   1.535 -        val RLj_import =
   1.536 -            RLj |> fold forall_elim cqsj'
   1.537 -                |> fold Thm.elim_implies agsj'
   1.538 -                |> fold Thm.elim_implies Ghsj'
   1.539 -
   1.540 -        val y_eq_rhsj'h = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
   1.541 -        val lhsi_eq_lhsj' = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
   1.542 -    in
   1.543 -        (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
   1.544 -        |> implies_elim RLj_import (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
   1.545 -        |> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
   1.546 -        |> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
   1.547 -        |> fold_rev (implies_intr o cprop_of) Ghsj'
   1.548 -        |> fold_rev (implies_intr o cprop_of) agsj' (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)
   1.549 -        |> implies_intr (cprop_of y_eq_rhsj'h)
   1.550 -        |> implies_intr (cprop_of lhsi_eq_lhsj')
   1.551 -        |> fold_rev forall_intr (cterm_of thy h :: cqsj')
   1.552 -    end
   1.553 +    val y_eq_rhsj'h = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
   1.554 +    val lhsi_eq_lhsj' = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj'))))
   1.555 +       (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
   1.556 +  in
   1.557 +    (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
   1.558 +    |> implies_elim RLj_import
   1.559 +      (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
   1.560 +    |> (fn it => trans OF [it, compat])
   1.561 +      (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
   1.562 +    |> (fn it => trans OF [y_eq_rhsj'h, it])
   1.563 +      (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
   1.564 +    |> fold_rev (implies_intr o cprop_of) Ghsj'
   1.565 +    |> fold_rev (implies_intr o cprop_of) agsj'
   1.566 +      (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)
   1.567 +    |> implies_intr (cprop_of y_eq_rhsj'h)
   1.568 +    |> implies_intr (cprop_of lhsi_eq_lhsj')
   1.569 +    |> fold_rev forall_intr (cterm_of thy h :: cqsj')
   1.570 +  end
   1.571  
   1.572  
   1.573  
   1.574  fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
   1.575 -    let
   1.576 -        val Globals {x, y, ranT, fvar, ...} = globals
   1.577 -        val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
   1.578 -        val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
   1.579 +  let
   1.580 +    val Globals {x, y, ranT, fvar, ...} = globals
   1.581 +    val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
   1.582 +    val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
   1.583  
   1.584 -        val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
   1.585 +    val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
   1.586  
   1.587 -        fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
   1.588 -                                                            |> fold_rev (implies_intr o cprop_of) CCas
   1.589 -                                                            |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
   1.590 +    fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
   1.591 +      |> fold_rev (implies_intr o cprop_of) CCas
   1.592 +      |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
   1.593 +
   1.594 +    val existence = fold (curry op COMP o prep_RC) RCs lGI
   1.595  
   1.596 -        val existence = fold (curry op COMP o prep_RC) RCs lGI
   1.597 +    val P = cterm_of thy (mk_eq (y, rhsC))
   1.598 +    val G_lhs_y = assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
   1.599  
   1.600 -        val P = cterm_of thy (mk_eq (y, rhsC))
   1.601 -        val G_lhs_y = assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
   1.602 -
   1.603 -        val unique_clauses = map2 (mk_uniqueness_clause thy globals compat_store clausei) clauses rep_lemmas
   1.604 +    val unique_clauses =
   1.605 +      map2 (mk_uniqueness_clause thy globals compat_store clausei) clauses rep_lemmas
   1.606  
   1.607 -        val uniqueness = G_cases
   1.608 -                           |> forall_elim (cterm_of thy lhs)
   1.609 -                           |> forall_elim (cterm_of thy y)
   1.610 -                           |> forall_elim P
   1.611 -                           |> Thm.elim_implies G_lhs_y
   1.612 -                           |> fold Thm.elim_implies unique_clauses
   1.613 -                           |> implies_intr (cprop_of G_lhs_y)
   1.614 -                           |> forall_intr (cterm_of thy y)
   1.615 +    val uniqueness = G_cases
   1.616 +      |> forall_elim (cterm_of thy lhs)
   1.617 +      |> forall_elim (cterm_of thy y)
   1.618 +      |> forall_elim P
   1.619 +      |> Thm.elim_implies G_lhs_y
   1.620 +      |> fold Thm.elim_implies unique_clauses
   1.621 +      |> implies_intr (cprop_of G_lhs_y)
   1.622 +      |> forall_intr (cterm_of thy y)
   1.623  
   1.624 -        val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
   1.625 +    val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
   1.626  
   1.627 -        val exactly_one =
   1.628 -            ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
   1.629 -                 |> curry (op COMP) existence
   1.630 -                 |> curry (op COMP) uniqueness
   1.631 -                 |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
   1.632 -                 |> implies_intr (cprop_of case_hyp)
   1.633 -                 |> fold_rev (implies_intr o cprop_of) ags
   1.634 -                 |> fold_rev forall_intr cqs
   1.635 +    val exactly_one =
   1.636 +      ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
   1.637 +      |> curry (op COMP) existence
   1.638 +      |> curry (op COMP) uniqueness
   1.639 +      |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
   1.640 +      |> implies_intr (cprop_of case_hyp)
   1.641 +      |> fold_rev (implies_intr o cprop_of) ags
   1.642 +      |> fold_rev forall_intr cqs
   1.643  
   1.644 -        val function_value =
   1.645 -            existence
   1.646 -              |> implies_intr ihyp
   1.647 -              |> implies_intr (cprop_of case_hyp)
   1.648 -              |> forall_intr (cterm_of thy x)
   1.649 -              |> forall_elim (cterm_of thy lhs)
   1.650 -              |> curry (op RS) refl
   1.651 -    in
   1.652 -        (exactly_one, function_value)
   1.653 -    end
   1.654 -
   1.655 -
   1.656 +    val function_value =
   1.657 +      existence
   1.658 +      |> implies_intr ihyp
   1.659 +      |> implies_intr (cprop_of case_hyp)
   1.660 +      |> forall_intr (cterm_of thy x)
   1.661 +      |> forall_elim (cterm_of thy lhs)
   1.662 +      |> curry (op RS) refl
   1.663 +  in
   1.664 +    (exactly_one, function_value)
   1.665 +  end
   1.666  
   1.667  
   1.668  fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim f_def =
   1.669 -    let
   1.670 -        val Globals {h, domT, ranT, x, ...} = globals
   1.671 -        val thy = ProofContext.theory_of ctxt
   1.672 +  let
   1.673 +    val Globals {h, domT, ranT, x, ...} = globals
   1.674 +    val thy = ProofContext.theory_of ctxt
   1.675  
   1.676 -        (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
   1.677 -        val ihyp = Term.all domT $ Abs ("z", domT,
   1.678 -                                   Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
   1.679 -                                     HOLogic.mk_Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
   1.680 -                                                             Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
   1.681 -                       |> cterm_of thy
   1.682 +    (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
   1.683 +    val ihyp = Term.all domT $ Abs ("z", domT,
   1.684 +      Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
   1.685 +        HOLogic.mk_Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
   1.686 +          Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
   1.687 +      |> cterm_of thy
   1.688  
   1.689 -        val ihyp_thm = assume ihyp |> Thm.forall_elim_vars 0
   1.690 -        val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
   1.691 -        val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
   1.692 -                        |> instantiate' [] [NONE, SOME (cterm_of thy h)]
   1.693 +    val ihyp_thm = assume ihyp |> Thm.forall_elim_vars 0
   1.694 +    val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
   1.695 +    val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
   1.696 +      |> instantiate' [] [NONE, SOME (cterm_of thy h)]
   1.697  
   1.698 -        val _ = trace_msg (K "Proving Replacement lemmas...")
   1.699 -        val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
   1.700 +    val _ = trace_msg (K "Proving Replacement lemmas...")
   1.701 +    val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
   1.702  
   1.703 -        val _ = trace_msg (K "Proving cases for unique existence...")
   1.704 -        val (ex1s, values) =
   1.705 -            split_list (map (mk_uniqueness_case thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
   1.706 +    val _ = trace_msg (K "Proving cases for unique existence...")
   1.707 +    val (ex1s, values) =
   1.708 +      split_list (map (mk_uniqueness_case thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
   1.709  
   1.710 -        val _ = trace_msg (K "Proving: Graph is a function")
   1.711 -        val graph_is_function = complete
   1.712 -                                  |> Thm.forall_elim_vars 0
   1.713 -                                  |> fold (curry op COMP) ex1s
   1.714 -                                  |> implies_intr (ihyp)
   1.715 -                                  |> implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
   1.716 -                                  |> forall_intr (cterm_of thy x)
   1.717 -                                  |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
   1.718 -                                  |> (fn it => fold (forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)
   1.719 +    val _ = trace_msg (K "Proving: Graph is a function")
   1.720 +    val graph_is_function = complete
   1.721 +      |> Thm.forall_elim_vars 0
   1.722 +      |> fold (curry op COMP) ex1s
   1.723 +      |> implies_intr (ihyp)
   1.724 +      |> implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
   1.725 +      |> forall_intr (cterm_of thy x)
   1.726 +      |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
   1.727 +      |> (fn it => fold (forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)
   1.728  
   1.729 -        val goalstate =  Conjunction.intr graph_is_function complete
   1.730 -                          |> Thm.close_derivation
   1.731 -                          |> Goal.protect
   1.732 -                          |> fold_rev (implies_intr o cprop_of) compat
   1.733 -                          |> implies_intr (cprop_of complete)
   1.734 -    in
   1.735 -      (goalstate, values)
   1.736 -    end
   1.737 +    val goalstate =  Conjunction.intr graph_is_function complete
   1.738 +      |> Thm.close_derivation
   1.739 +      |> Goal.protect
   1.740 +      |> fold_rev (implies_intr o cprop_of) compat
   1.741 +      |> implies_intr (cprop_of complete)
   1.742 +  in
   1.743 +    (goalstate, values)
   1.744 +  end
   1.745  
   1.746  (* wrapper -- restores quantifiers in rule specifications *)
   1.747  fun inductive_def (binding as ((R, T), _)) intrs lthy =
   1.748 @@ -483,7 +458,7 @@
   1.749            forall_intr_rename (n, cert (Var (varmap (n, T), T)))) qs thm
   1.750        end
   1.751    in
   1.752 -      ((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct), lthy)
   1.753 +    ((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct), lthy)
   1.754    end
   1.755  
   1.756  fun define_graph Gname fvar domT ranT clauses RCss lthy =
   1.757 @@ -544,33 +519,30 @@
   1.758  
   1.759  
   1.760  fun fix_globals domT ranT fvar ctxt =
   1.761 -    let
   1.762 -      val ([h, y, x, z, a, D, P, Pbool],ctxt') =
   1.763 -          Variable.variant_fixes ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt
   1.764 -    in
   1.765 -      (Globals {h = Free (h, domT --> ranT),
   1.766 -                y = Free (y, ranT),
   1.767 -                x = Free (x, domT),
   1.768 -                z = Free (z, domT),
   1.769 -                a = Free (a, domT),
   1.770 -                D = Free (D, domT --> boolT),
   1.771 -                P = Free (P, domT --> boolT),
   1.772 -                Pbool = Free (Pbool, boolT),
   1.773 -                fvar = fvar,
   1.774 -                domT = domT,
   1.775 -                ranT = ranT
   1.776 -               },
   1.777 -       ctxt')
   1.778 -    end
   1.779 -
   1.780 -
   1.781 +  let
   1.782 +    val ([h, y, x, z, a, D, P, Pbool],ctxt') = Variable.variant_fixes
   1.783 +      ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt
   1.784 +  in
   1.785 +    (Globals {h = Free (h, domT --> ranT),
   1.786 +      y = Free (y, ranT),
   1.787 +      x = Free (x, domT),
   1.788 +      z = Free (z, domT),
   1.789 +      a = Free (a, domT),
   1.790 +      D = Free (D, domT --> boolT),
   1.791 +      P = Free (P, domT --> boolT),
   1.792 +      Pbool = Free (Pbool, boolT),
   1.793 +      fvar = fvar,
   1.794 +      domT = domT,
   1.795 +      ranT = ranT},
   1.796 +    ctxt')
   1.797 +  end
   1.798  
   1.799  fun inst_RC thy fvar f (rcfix, rcassm, rcarg) =
   1.800 -    let
   1.801 -      fun inst_term t = subst_bound(f, abstract_over (fvar, t))
   1.802 -    in
   1.803 -      (rcfix, map (assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)
   1.804 -    end
   1.805 +  let
   1.806 +    fun inst_term t = subst_bound(f, abstract_over (fvar, t))
   1.807 +  in
   1.808 +    (rcfix, map (assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)
   1.809 +  end
   1.810  
   1.811  
   1.812  
   1.813 @@ -579,27 +551,27 @@
   1.814   **********************************************************)
   1.815  
   1.816  fun mk_psimps thy globals R clauses valthms f_iff graph_is_function =
   1.817 -    let
   1.818 -      val Globals {domT, z, ...} = globals
   1.819 +  let
   1.820 +    val Globals {domT, z, ...} = globals
   1.821  
   1.822 -      fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm =
   1.823 -          let
   1.824 -            val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
   1.825 -            val z_smaller = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *)
   1.826 -          in
   1.827 -            ((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
   1.828 -              |> (fn it => it COMP graph_is_function)
   1.829 -              |> implies_intr z_smaller
   1.830 -              |> forall_intr (cterm_of thy z)
   1.831 -              |> (fn it => it COMP valthm)
   1.832 -              |> implies_intr lhs_acc
   1.833 -              |> asm_simplify (HOL_basic_ss addsimps [f_iff])
   1.834 -              |> fold_rev (implies_intr o cprop_of) ags
   1.835 -              |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
   1.836 -          end
   1.837 -    in
   1.838 -      map2 mk_psimp clauses valthms
   1.839 -    end
   1.840 +    fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm =
   1.841 +      let
   1.842 +        val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
   1.843 +        val z_smaller = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *)
   1.844 +      in
   1.845 +        ((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
   1.846 +        |> (fn it => it COMP graph_is_function)
   1.847 +        |> implies_intr z_smaller
   1.848 +        |> forall_intr (cterm_of thy z)
   1.849 +        |> (fn it => it COMP valthm)
   1.850 +        |> implies_intr lhs_acc
   1.851 +        |> asm_simplify (HOL_basic_ss addsimps [f_iff])
   1.852 +        |> fold_rev (implies_intr o cprop_of) ags
   1.853 +        |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
   1.854 +      end
   1.855 +  in
   1.856 +    map2 mk_psimp clauses valthms
   1.857 +  end
   1.858  
   1.859  
   1.860  (** Induction rule **)
   1.861 @@ -609,232 +581,236 @@
   1.862  
   1.863  
   1.864  fun mk_partial_induct_rule thy globals R complete_thm clauses =
   1.865 -    let
   1.866 -      val Globals {domT, x, z, a, P, D, ...} = globals
   1.867 -      val acc_R = mk_acc domT R
   1.868 +  let
   1.869 +    val Globals {domT, x, z, a, P, D, ...} = globals
   1.870 +    val acc_R = mk_acc domT R
   1.871  
   1.872 -      val x_D = assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x)))
   1.873 -      val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a))
   1.874 +    val x_D = assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x)))
   1.875 +    val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a))
   1.876  
   1.877 -      val D_subset = cterm_of thy (Logic.all x
   1.878 -        (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x))))
   1.879 +    val D_subset = cterm_of thy (Logic.all x
   1.880 +      (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x))))
   1.881  
   1.882 -      val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
   1.883 -                    Logic.all x
   1.884 -                    (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x),
   1.885 -                                                    Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x),
   1.886 -                                                                      HOLogic.mk_Trueprop (D $ z)))))
   1.887 -                    |> cterm_of thy
   1.888 -
   1.889 +    val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
   1.890 +      Logic.all x (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x),
   1.891 +        Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x),
   1.892 +          HOLogic.mk_Trueprop (D $ z)))))
   1.893 +      |> cterm_of thy
   1.894  
   1.895 -  (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
   1.896 -      val ihyp = Term.all domT $ Abs ("z", domT,
   1.897 -               Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
   1.898 -                 HOLogic.mk_Trueprop (P $ Bound 0)))
   1.899 -           |> cterm_of thy
   1.900 +    (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
   1.901 +    val ihyp = Term.all domT $ Abs ("z", domT,
   1.902 +      Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
   1.903 +        HOLogic.mk_Trueprop (P $ Bound 0)))
   1.904 +      |> cterm_of thy
   1.905  
   1.906 -      val aihyp = assume ihyp
   1.907 +    val aihyp = assume ihyp
   1.908  
   1.909 -  fun prove_case clause =
   1.910 +    fun prove_case clause =
   1.911        let
   1.912 -    val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...}, RCs,
   1.913 -                    qglr = (oqs, _, _, _), ...} = clause
   1.914 +        val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...},
   1.915 +          RCs, qglr = (oqs, _, _, _), ...} = clause
   1.916  
   1.917 -    val case_hyp_conv = K (case_hyp RS eq_reflection)
   1.918 -    local open Conv in
   1.919 -    val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
   1.920 -    val sih = fconv_rule (More_Conv.binder_conv (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp
   1.921 -    end
   1.922 +        val case_hyp_conv = K (case_hyp RS eq_reflection)
   1.923 +        local open Conv in
   1.924 +          val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
   1.925 +          val sih =
   1.926 +            fconv_rule (More_Conv.binder_conv
   1.927 +              (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp
   1.928 +        end
   1.929  
   1.930 -    fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
   1.931 -        sih |> forall_elim (cterm_of thy rcarg)
   1.932 -            |> Thm.elim_implies llRI
   1.933 -            |> fold_rev (implies_intr o cprop_of) CCas
   1.934 -            |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
   1.935 +        fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = sih
   1.936 +          |> forall_elim (cterm_of thy rcarg)
   1.937 +          |> Thm.elim_implies llRI
   1.938 +          |> fold_rev (implies_intr o cprop_of) CCas
   1.939 +          |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
   1.940  
   1.941 -    val P_recs = map mk_Prec RCs   (*  [P rec1, P rec2, ... ]  *)
   1.942 +        val P_recs = map mk_Prec RCs   (*  [P rec1, P rec2, ... ]  *)
   1.943  
   1.944 -    val step = HOLogic.mk_Trueprop (P $ lhs)
   1.945 -            |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
   1.946 -            |> fold_rev (curry Logic.mk_implies) gs
   1.947 -            |> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs))
   1.948 -            |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
   1.949 -            |> cterm_of thy
   1.950 +        val step = HOLogic.mk_Trueprop (P $ lhs)
   1.951 +          |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
   1.952 +          |> fold_rev (curry Logic.mk_implies) gs
   1.953 +          |> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs))
   1.954 +          |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
   1.955 +          |> cterm_of thy
   1.956  
   1.957 -    val P_lhs = assume step
   1.958 -           |> fold forall_elim cqs
   1.959 -           |> Thm.elim_implies lhs_D
   1.960 -           |> fold Thm.elim_implies ags
   1.961 -           |> fold Thm.elim_implies P_recs
   1.962 +        val P_lhs = assume step
   1.963 +          |> fold forall_elim cqs
   1.964 +          |> Thm.elim_implies lhs_D
   1.965 +          |> fold Thm.elim_implies ags
   1.966 +          |> fold Thm.elim_implies P_recs
   1.967  
   1.968 -    val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x))
   1.969 -           |> Conv.arg_conv (Conv.arg_conv case_hyp_conv)
   1.970 -           |> symmetric (* P lhs == P x *)
   1.971 -           |> (fn eql => equal_elim eql P_lhs) (* "P x" *)
   1.972 -           |> implies_intr (cprop_of case_hyp)
   1.973 -           |> fold_rev (implies_intr o cprop_of) ags
   1.974 -           |> fold_rev forall_intr cqs
   1.975 +        val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x))
   1.976 +          |> Conv.arg_conv (Conv.arg_conv case_hyp_conv)
   1.977 +          |> symmetric (* P lhs == P x *)
   1.978 +          |> (fn eql => equal_elim eql P_lhs) (* "P x" *)
   1.979 +          |> implies_intr (cprop_of case_hyp)
   1.980 +          |> fold_rev (implies_intr o cprop_of) ags
   1.981 +          |> fold_rev forall_intr cqs
   1.982        in
   1.983          (res, step)
   1.984        end
   1.985  
   1.986 -  val (cases, steps) = split_list (map prove_case clauses)
   1.987 +    val (cases, steps) = split_list (map prove_case clauses)
   1.988  
   1.989 -  val istep = complete_thm
   1.990 -                |> Thm.forall_elim_vars 0
   1.991 -                |> fold (curry op COMP) cases (*  P x  *)
   1.992 -                |> implies_intr ihyp
   1.993 -                |> implies_intr (cprop_of x_D)
   1.994 -                |> forall_intr (cterm_of thy x)
   1.995 +    val istep = complete_thm
   1.996 +      |> Thm.forall_elim_vars 0
   1.997 +      |> fold (curry op COMP) cases (*  P x  *)
   1.998 +      |> implies_intr ihyp
   1.999 +      |> implies_intr (cprop_of x_D)
  1.1000 +      |> forall_intr (cterm_of thy x)
  1.1001  
  1.1002 -  val subset_induct_rule =
  1.1003 +    val subset_induct_rule =
  1.1004        acc_subset_induct
  1.1005 -        |> (curry op COMP) (assume D_subset)
  1.1006 -        |> (curry op COMP) (assume D_dcl)
  1.1007 -        |> (curry op COMP) (assume a_D)
  1.1008 -        |> (curry op COMP) istep
  1.1009 -        |> fold_rev implies_intr steps
  1.1010 -        |> implies_intr a_D
  1.1011 -        |> implies_intr D_dcl
  1.1012 -        |> implies_intr D_subset
  1.1013 +      |> (curry op COMP) (assume D_subset)
  1.1014 +      |> (curry op COMP) (assume D_dcl)
  1.1015 +      |> (curry op COMP) (assume a_D)
  1.1016 +      |> (curry op COMP) istep
  1.1017 +      |> fold_rev implies_intr steps
  1.1018 +      |> implies_intr a_D
  1.1019 +      |> implies_intr D_dcl
  1.1020 +      |> implies_intr D_subset
  1.1021  
  1.1022 -  val simple_induct_rule =
  1.1023 +    val simple_induct_rule =
  1.1024        subset_induct_rule
  1.1025 -        |> forall_intr (cterm_of thy D)
  1.1026 -        |> forall_elim (cterm_of thy acc_R)
  1.1027 -        |> assume_tac 1 |> Seq.hd
  1.1028 -        |> (curry op COMP) (acc_downward
  1.1029 -                              |> (instantiate' [SOME (ctyp_of thy domT)]
  1.1030 -                                               (map (SOME o cterm_of thy) [R, x, z]))
  1.1031 -                              |> forall_intr (cterm_of thy z)
  1.1032 -                              |> forall_intr (cterm_of thy x))
  1.1033 -        |> forall_intr (cterm_of thy a)
  1.1034 -        |> forall_intr (cterm_of thy P)
  1.1035 -    in
  1.1036 -      simple_induct_rule
  1.1037 -    end
  1.1038 +      |> forall_intr (cterm_of thy D)
  1.1039 +      |> forall_elim (cterm_of thy acc_R)
  1.1040 +      |> assume_tac 1 |> Seq.hd
  1.1041 +      |> (curry op COMP) (acc_downward
  1.1042 +        |> (instantiate' [SOME (ctyp_of thy domT)]
  1.1043 +             (map (SOME o cterm_of thy) [R, x, z]))
  1.1044 +        |> forall_intr (cterm_of thy z)
  1.1045 +        |> forall_intr (cterm_of thy x))
  1.1046 +      |> forall_intr (cterm_of thy a)
  1.1047 +      |> forall_intr (cterm_of thy P)
  1.1048 +  in
  1.1049 +    simple_induct_rule
  1.1050 +  end
  1.1051  
  1.1052  
  1.1053 -
  1.1054 -(* FIXME: This should probably use fixed goals, to be more reliable and faster *)
  1.1055 +(* FIXME: broken by design *)
  1.1056  fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause =
  1.1057 -    let
  1.1058 -      val thy = ProofContext.theory_of ctxt
  1.1059 -      val ClauseInfo {cdata = ClauseContext {gs, lhs, cqs, ...},
  1.1060 -                      qglr = (oqs, _, _, _), ...} = clause
  1.1061 -      val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs)
  1.1062 -                          |> fold_rev (curry Logic.mk_implies) gs
  1.1063 -                          |> cterm_of thy
  1.1064 -    in
  1.1065 -      Goal.init goal
  1.1066 -      |> (SINGLE (resolve_tac [accI] 1)) |> the
  1.1067 -      |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1))  |> the
  1.1068 -      |> (SINGLE (auto_tac (clasimpset_of ctxt))) |> the
  1.1069 -      |> Goal.conclude
  1.1070 -      |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
  1.1071 -    end
  1.1072 +  let
  1.1073 +    val thy = ProofContext.theory_of ctxt
  1.1074 +    val ClauseInfo {cdata = ClauseContext {gs, lhs, cqs, ...},
  1.1075 +      qglr = (oqs, _, _, _), ...} = clause
  1.1076 +    val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs)
  1.1077 +      |> fold_rev (curry Logic.mk_implies) gs
  1.1078 +      |> cterm_of thy
  1.1079 +  in
  1.1080 +    Goal.init goal
  1.1081 +    |> (SINGLE (resolve_tac [accI] 1)) |> the
  1.1082 +    |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1))  |> the
  1.1083 +    |> (SINGLE (auto_tac (clasimpset_of ctxt))) |> the
  1.1084 +    |> Goal.conclude
  1.1085 +    |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
  1.1086 +  end
  1.1087  
  1.1088  
  1.1089  
  1.1090  (** Termination rule **)
  1.1091  
  1.1092 -val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule};
  1.1093 -val wf_in_rel = @{thm FunDef.wf_in_rel};
  1.1094 -val in_rel_def = @{thm FunDef.in_rel_def};
  1.1095 +val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule}
  1.1096 +val wf_in_rel = @{thm FunDef.wf_in_rel}
  1.1097 +val in_rel_def = @{thm FunDef.in_rel_def}
  1.1098  
  1.1099  fun mk_nest_term_case thy globals R' ihyp clause =
  1.1100 -    let
  1.1101 -      val Globals {z, ...} = globals
  1.1102 -      val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...},tree,
  1.1103 -                      qglr=(oqs, _, _, _), ...} = clause
  1.1104 +  let
  1.1105 +    val Globals {z, ...} = globals
  1.1106 +    val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...}, tree,
  1.1107 +      qglr=(oqs, _, _, _), ...} = clause
  1.1108  
  1.1109 -      val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
  1.1110 +    val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
  1.1111  
  1.1112 -      fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
  1.1113 -          let
  1.1114 -            val used = map (fn (ctx,thm) => Function_Ctx_Tree.export_thm thy ctx thm) (u @ sub)
  1.1115 +    fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
  1.1116 +      let
  1.1117 +        val used = (u @ sub)
  1.1118 +          |> map (fn (ctx,thm) => Function_Ctx_Tree.export_thm thy ctx thm)
  1.1119  
  1.1120 -            val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs)
  1.1121 -                      |> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *)
  1.1122 -                      |> Function_Ctx_Tree.export_term (fixes, assumes)
  1.1123 -                      |> fold_rev (curry Logic.mk_implies o prop_of) ags
  1.1124 -                      |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
  1.1125 -                      |> cterm_of thy
  1.1126 +        val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs)
  1.1127 +          |> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *)
  1.1128 +          |> Function_Ctx_Tree.export_term (fixes, assumes)
  1.1129 +          |> fold_rev (curry Logic.mk_implies o prop_of) ags
  1.1130 +          |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
  1.1131 +          |> cterm_of thy
  1.1132  
  1.1133 -            val thm = assume hyp
  1.1134 -                      |> fold forall_elim cqs
  1.1135 -                      |> fold Thm.elim_implies ags
  1.1136 -                      |> Function_Ctx_Tree.import_thm thy (fixes, assumes)
  1.1137 -                      |> fold Thm.elim_implies used (*  "(arg, lhs) : R'"  *)
  1.1138 +        val thm = assume hyp
  1.1139 +          |> fold forall_elim cqs
  1.1140 +          |> fold Thm.elim_implies ags
  1.1141 +          |> Function_Ctx_Tree.import_thm thy (fixes, assumes)
  1.1142 +          |> fold Thm.elim_implies used (*  "(arg, lhs) : R'"  *)
  1.1143  
  1.1144 -            val z_eq_arg = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (z, arg))))
  1.1145 +        val z_eq_arg = HOLogic.mk_Trueprop (mk_eq (z, arg))
  1.1146 +          |> cterm_of thy |> assume
  1.1147  
  1.1148 -            val acc = thm COMP ih_case
  1.1149 -            val z_acc_local = acc
  1.1150 -            |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (K (symmetric (z_eq_arg RS eq_reflection)))))
  1.1151 +        val acc = thm COMP ih_case
  1.1152 +        val z_acc_local = acc
  1.1153 +          |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (K (symmetric (z_eq_arg RS eq_reflection)))))
  1.1154  
  1.1155 -            val ethm = z_acc_local
  1.1156 -                         |> Function_Ctx_Tree.export_thm thy (fixes,
  1.1157 -                                                          z_eq_arg :: case_hyp :: ags @ assumes)
  1.1158 -                         |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
  1.1159 +        val ethm = z_acc_local
  1.1160 +          |> Function_Ctx_Tree.export_thm thy (fixes,
  1.1161 +               z_eq_arg :: case_hyp :: ags @ assumes)
  1.1162 +          |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
  1.1163  
  1.1164 -            val sub' = sub @ [(([],[]), acc)]
  1.1165 -          in
  1.1166 -            (sub', (hyp :: hyps, ethm :: thms))
  1.1167 -          end
  1.1168 -        | step _ _ _ _ = raise Match
  1.1169 -    in
  1.1170 -      Function_Ctx_Tree.traverse_tree step tree
  1.1171 -    end
  1.1172 +        val sub' = sub @ [(([],[]), acc)]
  1.1173 +      in
  1.1174 +        (sub', (hyp :: hyps, ethm :: thms))
  1.1175 +      end
  1.1176 +      | step _ _ _ _ = raise Match
  1.1177 +  in
  1.1178 +    Function_Ctx_Tree.traverse_tree step tree
  1.1179 +  end
  1.1180  
  1.1181  
  1.1182  fun mk_nest_term_rule thy globals R R_cases clauses =
  1.1183 -    let
  1.1184 -      val Globals { domT, x, z, ... } = globals
  1.1185 -      val acc_R = mk_acc domT R
  1.1186 +  let
  1.1187 +    val Globals { domT, x, z, ... } = globals
  1.1188 +    val acc_R = mk_acc domT R
  1.1189  
  1.1190 -      val R' = Free ("R", fastype_of R)
  1.1191 +    val R' = Free ("R", fastype_of R)
  1.1192  
  1.1193 -      val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
  1.1194 -      val inrel_R = Const (@{const_name FunDef.in_rel}, HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
  1.1195 +    val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
  1.1196 +    val inrel_R = Const (@{const_name FunDef.in_rel},
  1.1197 +      HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
  1.1198  
  1.1199 -      val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP}, (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
  1.1200 +    val wfR' = HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP},
  1.1201 +      (domT --> domT --> boolT) --> boolT) $ R')
  1.1202 +      |> cterm_of thy (* "wf R'" *)
  1.1203  
  1.1204 -      (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
  1.1205 -      val ihyp = Term.all domT $ Abs ("z", domT,
  1.1206 -                                 Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x),
  1.1207 -                                   HOLogic.mk_Trueprop (acc_R $ Bound 0)))
  1.1208 -                     |> cterm_of thy
  1.1209 +    (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
  1.1210 +    val ihyp = Term.all domT $ Abs ("z", domT,
  1.1211 +      Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x),
  1.1212 +        HOLogic.mk_Trueprop (acc_R $ Bound 0)))
  1.1213 +      |> cterm_of thy
  1.1214  
  1.1215 -      val ihyp_a = assume ihyp |> Thm.forall_elim_vars 0
  1.1216 +    val ihyp_a = assume ihyp |> Thm.forall_elim_vars 0
  1.1217  
  1.1218 -      val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x))
  1.1219 +    val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x))
  1.1220  
  1.1221 -      val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[])
  1.1222 -    in
  1.1223 -      R_cases
  1.1224 -        |> forall_elim (cterm_of thy z)
  1.1225 -        |> forall_elim (cterm_of thy x)
  1.1226 -        |> forall_elim (cterm_of thy (acc_R $ z))
  1.1227 -        |> curry op COMP (assume R_z_x)
  1.1228 -        |> fold_rev (curry op COMP) cases
  1.1229 -        |> implies_intr R_z_x
  1.1230 -        |> forall_intr (cterm_of thy z)
  1.1231 -        |> (fn it => it COMP accI)
  1.1232 -        |> implies_intr ihyp
  1.1233 -        |> forall_intr (cterm_of thy x)
  1.1234 -        |> (fn it => Drule.compose_single(it,2,wf_induct_rule))
  1.1235 -        |> curry op RS (assume wfR')
  1.1236 -        |> forall_intr_vars
  1.1237 -        |> (fn it => it COMP allI)
  1.1238 -        |> fold implies_intr hyps
  1.1239 -        |> implies_intr wfR'
  1.1240 -        |> forall_intr (cterm_of thy R')
  1.1241 -        |> forall_elim (cterm_of thy (inrel_R))
  1.1242 -        |> curry op RS wf_in_rel
  1.1243 -        |> full_simplify (HOL_basic_ss addsimps [in_rel_def])
  1.1244 -        |> forall_intr (cterm_of thy Rrel)
  1.1245 -    end
  1.1246 +    val (hyps, cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([], [])
  1.1247 +  in
  1.1248 +    R_cases
  1.1249 +    |> forall_elim (cterm_of thy z)
  1.1250 +    |> forall_elim (cterm_of thy x)
  1.1251 +    |> forall_elim (cterm_of thy (acc_R $ z))
  1.1252 +    |> curry op COMP (assume R_z_x)
  1.1253 +    |> fold_rev (curry op COMP) cases
  1.1254 +    |> implies_intr R_z_x
  1.1255 +    |> forall_intr (cterm_of thy z)
  1.1256 +    |> (fn it => it COMP accI)
  1.1257 +    |> implies_intr ihyp
  1.1258 +    |> forall_intr (cterm_of thy x)
  1.1259 +    |> (fn it => Drule.compose_single(it,2,wf_induct_rule))
  1.1260 +    |> curry op RS (assume wfR')
  1.1261 +    |> forall_intr_vars
  1.1262 +    |> (fn it => it COMP allI)
  1.1263 +    |> fold implies_intr hyps
  1.1264 +    |> implies_intr wfR'
  1.1265 +    |> forall_intr (cterm_of thy R')
  1.1266 +    |> forall_elim (cterm_of thy (inrel_R))
  1.1267 +    |> curry op RS wf_in_rel
  1.1268 +    |> full_simplify (HOL_basic_ss addsimps [in_rel_def])
  1.1269 +    |> forall_intr (cterm_of thy Rrel)
  1.1270 +  end
  1.1271  
  1.1272  
  1.1273  
  1.1274 @@ -846,135 +822,150 @@
  1.1275   * - Splitting is not configured automatically: Problems with case?
  1.1276   *)
  1.1277  fun mk_trsimps octxt globals f G R f_def R_cases G_induct clauses psimps =
  1.1278 -    let
  1.1279 -      val Globals {domT, ranT, fvar, ...} = globals
  1.1280 +  let
  1.1281 +    val Globals {domT, ranT, fvar, ...} = globals
  1.1282  
  1.1283 -      val R_cases = Thm.forall_elim_vars 0 R_cases (* FIXME: Should be already in standard form. *)
  1.1284 +    val R_cases = Thm.forall_elim_vars 0 R_cases (* FIXME: Should be already in standard form. *)
  1.1285  
  1.1286 -      val graph_implies_dom = (* "G ?x ?y ==> dom ?x"  *)
  1.1287 -          Goal.prove octxt ["x", "y"] [HOLogic.mk_Trueprop (G $ Free ("x", domT) $ Free ("y", ranT))]
  1.1288 -                     (HOLogic.mk_Trueprop (mk_acc domT R $ Free ("x", domT)))
  1.1289 -                     (fn {prems=[a], ...} =>
  1.1290 -                         ((rtac (G_induct OF [a]))
  1.1291 -                            THEN_ALL_NEW (rtac accI)
  1.1292 -                            THEN_ALL_NEW (etac R_cases)
  1.1293 -                            THEN_ALL_NEW (asm_full_simp_tac (simpset_of octxt))) 1)
  1.1294 +    val graph_implies_dom = (* "G ?x ?y ==> dom ?x"  *)
  1.1295 +      Goal.prove octxt ["x", "y"] [HOLogic.mk_Trueprop (G $ Free ("x", domT) $ Free ("y", ranT))]
  1.1296 +        (HOLogic.mk_Trueprop (mk_acc domT R $ Free ("x", domT)))
  1.1297 +        (fn {prems=[a], ...} =>
  1.1298 +          ((rtac (G_induct OF [a]))
  1.1299 +          THEN_ALL_NEW rtac accI
  1.1300 +          THEN_ALL_NEW etac R_cases
  1.1301 +          THEN_ALL_NEW asm_full_simp_tac (simpset_of octxt)) 1)
  1.1302  
  1.1303 -      val default_thm = (forall_intr_vars graph_implies_dom) COMP (f_def COMP fundef_default_value)
  1.1304 +    val default_thm =
  1.1305 +      forall_intr_vars graph_implies_dom COMP (f_def COMP fundef_default_value)
  1.1306  
  1.1307 -      fun mk_trsimp clause psimp =
  1.1308 -          let
  1.1309 -            val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {ctxt, cqs, gs, lhs, rhs, ...}, ...} = clause
  1.1310 -            val thy = ProofContext.theory_of ctxt
  1.1311 -            val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs
  1.1312 +    fun mk_trsimp clause psimp =
  1.1313 +      let
  1.1314 +        val ClauseInfo {qglr = (oqs, _, _, _), cdata =
  1.1315 +          ClauseContext {ctxt, cqs, gs, lhs, rhs, ...}, ...} = clause
  1.1316 +        val thy = ProofContext.theory_of ctxt
  1.1317 +        val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs
  1.1318  
  1.1319 -            val trsimp = Logic.list_implies(gs, HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *)
  1.1320 -            val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *)
  1.1321 -            fun simp_default_tac ss = asm_full_simp_tac (ss addsimps [default_thm, Let_def])
  1.1322 -          in
  1.1323 -            Goal.prove ctxt [] [] trsimp
  1.1324 -                       (fn _ =>
  1.1325 -                           rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
  1.1326 -                                THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
  1.1327 -                                THEN (simp_default_tac (simpset_of ctxt) 1)
  1.1328 -                                THEN (etac not_acc_down 1)
  1.1329 -                                THEN ((etac R_cases) THEN_ALL_NEW (simp_default_tac (simpset_of ctxt))) 1)
  1.1330 -              |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
  1.1331 -          end
  1.1332 -    in
  1.1333 -      map2 mk_trsimp clauses psimps
  1.1334 -    end
  1.1335 +        val trsimp = Logic.list_implies(gs,
  1.1336 +          HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *)
  1.1337 +        val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *)
  1.1338 +        fun simp_default_tac ss =
  1.1339 +          asm_full_simp_tac (ss addsimps [default_thm, Let_def])
  1.1340 +      in
  1.1341 +        Goal.prove ctxt [] [] trsimp (fn _ =>
  1.1342 +          rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
  1.1343 +          THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
  1.1344 +          THEN (simp_default_tac (simpset_of ctxt) 1)
  1.1345 +          THEN (etac not_acc_down 1)
  1.1346 +          THEN ((etac R_cases)
  1.1347 +            THEN_ALL_NEW (simp_default_tac (simpset_of ctxt))) 1)
  1.1348 +        |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
  1.1349 +      end
  1.1350 +  in
  1.1351 +    map2 mk_trsimp clauses psimps
  1.1352 +  end
  1.1353  
  1.1354  
  1.1355  fun prepare_function config defname [((fname, fT), mixfix)] abstract_qglrs lthy =
  1.1356 -    let
  1.1357 -      val FunctionConfig {domintros, tailrec, default=default_str, ...} = config
  1.1358 +  let
  1.1359 +    val FunctionConfig {domintros, tailrec, default=default_str, ...} = config
  1.1360  
  1.1361 -      val fvar = Free (fname, fT)
  1.1362 -      val domT = domain_type fT
  1.1363 -      val ranT = range_type fT
  1.1364 +    val fvar = Free (fname, fT)
  1.1365 +    val domT = domain_type fT
  1.1366 +    val ranT = range_type fT
  1.1367  
  1.1368 -      val default = Syntax.parse_term lthy default_str
  1.1369 -        |> TypeInfer.constrain fT |> Syntax.check_term lthy
  1.1370 +    val default = Syntax.parse_term lthy default_str
  1.1371 +      |> TypeInfer.constrain fT |> Syntax.check_term lthy
  1.1372 +
  1.1373 +    val (globals, ctxt') = fix_globals domT ranT fvar lthy
  1.1374  
  1.1375 -      val (globals, ctxt') = fix_globals domT ranT fvar lthy
  1.1376 +    val Globals { x, h, ... } = globals
  1.1377  
  1.1378 -      val Globals { x, h, ... } = globals
  1.1379 +    val clauses = map (mk_clause_context x ctxt') abstract_qglrs
  1.1380 +
  1.1381 +    val n = length abstract_qglrs
  1.1382  
  1.1383 -      val clauses = map (mk_clause_context x ctxt') abstract_qglrs
  1.1384 +    fun build_tree (ClauseContext { ctxt, rhs, ...}) =
  1.1385 +       Function_Ctx_Tree.mk_tree (fname, fT) h ctxt rhs
  1.1386  
  1.1387 -      val n = length abstract_qglrs
  1.1388 -
  1.1389 -      fun build_tree (ClauseContext { ctxt, rhs, ...}) =
  1.1390 -            Function_Ctx_Tree.mk_tree (fname, fT) h ctxt rhs
  1.1391 +    val trees = map build_tree clauses
  1.1392 +    val RCss = map find_calls trees
  1.1393  
  1.1394 -      val trees = map build_tree clauses
  1.1395 -      val RCss = map find_calls trees
  1.1396 +    val ((G, GIntro_thms, G_elim, G_induct), lthy) =
  1.1397 +      PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
  1.1398 +
  1.1399 +    val ((f, (_, f_defthm)), lthy) =
  1.1400 +      PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
  1.1401  
  1.1402 -      val ((G, GIntro_thms, G_elim, G_induct), lthy) =
  1.1403 -          PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
  1.1404 +    val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
  1.1405 +    val trees = map (Function_Ctx_Tree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
  1.1406  
  1.1407 -      val ((f, (_, f_defthm)), lthy) =
  1.1408 -          PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
  1.1409 +    val ((R, RIntro_thmss, R_elim), lthy) =
  1.1410 +      PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy
  1.1411  
  1.1412 -      val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
  1.1413 -      val trees = map (Function_Ctx_Tree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
  1.1414 +    val (_, lthy) =
  1.1415 +      Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
  1.1416  
  1.1417 -      val ((R, RIntro_thmss, R_elim), lthy) =
  1.1418 -          PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy
  1.1419 +    val newthy = ProofContext.theory_of lthy
  1.1420 +    val clauses = map (transfer_clause_ctx newthy) clauses
  1.1421  
  1.1422 -      val (_, lthy) =
  1.1423 -          Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
  1.1424 +    val cert = cterm_of (ProofContext.theory_of lthy)
  1.1425  
  1.1426 -      val newthy = ProofContext.theory_of lthy
  1.1427 -      val clauses = map (transfer_clause_ctx newthy) clauses
  1.1428 -
  1.1429 -      val cert = cterm_of (ProofContext.theory_of lthy)
  1.1430 +    val xclauses = PROFILE "xclauses"
  1.1431 +      (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees
  1.1432 +        RCss GIntro_thms) RIntro_thmss
  1.1433  
  1.1434 -      val xclauses = PROFILE "xclauses" (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees RCss GIntro_thms) RIntro_thmss
  1.1435 -
  1.1436 -      val complete = mk_completeness globals clauses abstract_qglrs |> cert |> assume
  1.1437 -      val compat = mk_compat_proof_obligations domT ranT fvar f abstract_qglrs |> map (cert #> assume)
  1.1438 +    val complete =
  1.1439 +      mk_completeness globals clauses abstract_qglrs |> cert |> assume
  1.1440  
  1.1441 -      val compat_store = store_compat_thms n compat
  1.1442 +    val compat =
  1.1443 +      mk_compat_proof_obligations domT ranT fvar f abstract_qglrs
  1.1444 +      |> map (cert #> assume)
  1.1445  
  1.1446 -      val (goalstate, values) = PROFILE "prove_stuff" (prove_stuff lthy globals G f R xclauses complete compat compat_store G_elim) f_defthm
  1.1447 -
  1.1448 -      val mk_trsimps = mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses
  1.1449 +    val compat_store = store_compat_thms n compat
  1.1450  
  1.1451 -      fun mk_partial_rules provedgoal =
  1.1452 -          let
  1.1453 -            val newthy = theory_of_thm provedgoal (*FIXME*)
  1.1454 +    val (goalstate, values) = PROFILE "prove_stuff"
  1.1455 +      (prove_stuff lthy globals G f R xclauses complete compat
  1.1456 +         compat_store G_elim) f_defthm
  1.1457 +
  1.1458 +    val mk_trsimps =
  1.1459 +      mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses
  1.1460  
  1.1461 -            val (graph_is_function, complete_thm) =
  1.1462 -                provedgoal
  1.1463 -                  |> Conjunction.elim
  1.1464 -                  |> apfst (Thm.forall_elim_vars 0)
  1.1465 +    fun mk_partial_rules provedgoal =
  1.1466 +      let
  1.1467 +        val newthy = theory_of_thm provedgoal (*FIXME*)
  1.1468  
  1.1469 -            val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)
  1.1470 +        val (graph_is_function, complete_thm) =
  1.1471 +          provedgoal
  1.1472 +          |> Conjunction.elim
  1.1473 +          |> apfst (Thm.forall_elim_vars 0)
  1.1474  
  1.1475 -            val psimps = PROFILE "Proving simplification rules" (mk_psimps newthy globals R xclauses values f_iff) graph_is_function
  1.1476 +        val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)
  1.1477 +
  1.1478 +        val psimps = PROFILE "Proving simplification rules"
  1.1479 +          (mk_psimps newthy globals R xclauses values f_iff) graph_is_function
  1.1480  
  1.1481 -            val simple_pinduct = PROFILE "Proving partial induction rule"
  1.1482 -                                                           (mk_partial_induct_rule newthy globals R complete_thm) xclauses
  1.1483 +        val simple_pinduct = PROFILE "Proving partial induction rule"
  1.1484 +          (mk_partial_induct_rule newthy globals R complete_thm) xclauses
  1.1485  
  1.1486 -
  1.1487 -            val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule newthy globals R R_elim) xclauses
  1.1488 +        val total_intro = PROFILE "Proving nested termination rule"
  1.1489 +          (mk_nest_term_rule newthy globals R R_elim) xclauses
  1.1490  
  1.1491 -            val dom_intros = if domintros
  1.1492 -                             then SOME (PROFILE "Proving domain introduction rules" (map (mk_domain_intro lthy globals R R_elim)) xclauses)
  1.1493 -                             else NONE
  1.1494 -            val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE
  1.1495 +        val dom_intros =
  1.1496 +          if domintros then SOME (PROFILE "Proving domain introduction rules"
  1.1497 +             (map (mk_domain_intro lthy globals R R_elim)) xclauses)
  1.1498 +           else NONE
  1.1499 +        val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE
  1.1500  
  1.1501 -          in
  1.1502 -            FunctionResult {fs=[f], G=G, R=R, cases=complete_thm,
  1.1503 -                          psimps=psimps, simple_pinducts=[simple_pinduct],
  1.1504 -                          termination=total_intro, trsimps=trsimps,
  1.1505 -                          domintros=dom_intros}
  1.1506 -          end
  1.1507 -    in
  1.1508 -      ((f, goalstate, mk_partial_rules), lthy)
  1.1509 -    end
  1.1510 +      in
  1.1511 +        FunctionResult {fs=[f], G=G, R=R, cases=complete_thm,
  1.1512 +          psimps=psimps, simple_pinducts=[simple_pinduct],
  1.1513 +          termination=total_intro, trsimps=trsimps,
  1.1514 +          domintros=dom_intros}
  1.1515 +      end
  1.1516 +  in
  1.1517 +    ((f, goalstate, mk_partial_rules), lthy)
  1.1518 +  end
  1.1519  
  1.1520  
  1.1521  end