author krauss Tue, 07 Nov 2006 22:06:32 +0100 changeset 21237 b803f9870e97 parent 21236 890fafbcf8b0 child 21238 c46bc715bdfd
untabified
```--- a/src/HOL/Tools/function_package/context_tree.ML	Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/context_tree.ML	Tue Nov 07 22:06:32 2006 +0100
@@ -55,7 +55,7 @@
(*** Dependency analysis for congruence rules ***)

fun branch_vars t =
-    let
+    let
val t' = snd (dest_all_all t)
val assumes = Logic.strip_imp_prems t'
val concl = Logic.strip_imp_concl t'
@@ -64,13 +64,13 @@

fun cong_deps crule =
let
-	val branches = map branch_vars (prems_of crule)
-	val num_branches = (1 upto (length branches)) ~~ branches
+  val branches = map branch_vars (prems_of crule)
+  val num_branches = (1 upto (length branches)) ~~ branches
in
-	IntGraph.empty
-	    |> fold (fn (i,_)=> IntGraph.new_node (i,i)) num_branches
-	    |> fold (fn ((i,(c1,_)),(j,(_, t2))) => if i = j orelse null (c1 inter t2) then I else IntGraph.add_edge_acyclic (i,j))
-	    (product num_branches num_branches)
+  IntGraph.empty
+      |> fold (fn (i,_)=> IntGraph.new_node (i,i)) num_branches
+      |> fold (fn ((i,(c1,_)),(j,(_, t2))) => if i = j orelse null (c1 inter t2) then I else IntGraph.add_edge_acyclic (i,j))
+      (product num_branches num_branches)
end

val add_congs = map (fn c => c RS eq_reflection) [cong, ext]
@@ -80,7 +80,7 @@
(* Called on the INSTANTIATED branches of the congruence rule *)
fun mk_branch ctx t =
let
-	val (ctx', fixes, impl) = dest_all_all_ctx ctx t
+  val (ctx', fixes, impl) = dest_all_all_ctx ctx t
in
(ctx', fixes, Logic.strip_imp_prems impl, rhs_of (Logic.strip_imp_concl impl))
end
@@ -96,7 +96,7 @@
val branches = map (mk_branch ctx o Envir.beta_norm o Envir.subst_vars subst) subs
val inst = map (fn v => (cterm_of thy (Var v), cterm_of thy (Envir.subst_vars subst (Var v)))) (Term.add_vars c [])
in
-	 (cterm_instantiate inst r, dep, branches)
+   (cterm_instantiate inst r, dep, branches)
end
handle Pattern.MATCH => find_cong_rule ctx fvar h rs t)
| find_cong_rule _ _ _ [] _ = sys_error "function_package/context_tree.ML: No cong rule found!"
@@ -111,13 +111,13 @@
| NONE =>
if not (exists_subterm (fn Free v => v = fvar | _ => false) t) then Leaf t
else
-	let val (r, dep, branches) = find_cong_rule ctx fvar h congs t in
-	  Cong (t, r, dep,
+  let val (r, dep, branches) = find_cong_rule ctx fvar h congs t in
+    Cong (t, r, dep,
map (fn (ctx', fixes, assumes, st) =>
-			(fixes, map (assume o cterm_of (ProofContext.theory_of ctx)) assumes,
+      (fixes, map (assume o cterm_of (ProofContext.theory_of ctx)) assumes,
mk_tree congs fvar h ctx' st)) branches)
-	end
-
+  end
+

fun inst_tree thy fvar f tr =
let
@@ -142,7 +142,7 @@

-(* FIXME: remove *)
+(* FIXME: remove *)
fun add_context_varnames (Leaf _) = I
| add_context_varnames (Cong (_, _, _, sub)) = fold (fn (fs, _, st) => fold (insert (op =) o fst) fs o add_context_varnames st) sub
@@ -164,30 +164,30 @@

fun assume_in_ctxt thy (fixes, athms) prop =
let
-	val global_assum = export_term (fixes, map prop_of athms) prop
+  val global_assum = export_term (fixes, map prop_of athms) prop
in
-	(global_assum,
-	 assume (cterm_of thy global_assum) |> import_thm thy (fixes, athms))
+  (global_assum,
+   assume (cterm_of thy global_assum) |> import_thm thy (fixes, athms))
end

(* folds in the order of the dependencies of a graph. *)
fun fold_deps G f x =
let
-	fun fill_table i (T, x) =
-	    case Inttab.lookup T i of
-		SOME _ => (T, x)
-	      | NONE =>
-		let
-		    val (T', x') = fold fill_table (IntGraph.imm_succs G i) (T, x)
-		    val (v, x'') = f (the o Inttab.lookup T') i x
-		in
-		    (Inttab.update (i, v) T', x'')
-		end
+  fun fill_table i (T, x) =
+      case Inttab.lookup T i of
+    SOME _ => (T, x)
+        | NONE =>
+    let
+        val (T', x') = fold fill_table (IntGraph.imm_succs G i) (T, x)
+        val (v, x'') = f (the o Inttab.lookup T') i x
+    in
+        (Inttab.update (i, v) T', x'')
+    end

-	val (T, x) = fold fill_table (IntGraph.keys G) (Inttab.empty, x)
+  val (T, x) = fold fill_table (IntGraph.keys G) (Inttab.empty, x)
in
-	(Inttab.fold (cons o snd) T [], x)
+  (Inttab.fold (cons o snd) T [], x)
end

@@ -195,26 +195,26 @@

fun traverse_tree rcOp tr x =
let
-	fun traverse_help ctx (Leaf _) u x = ([], x)
-	  | traverse_help ctx (RCall (t, st)) u x =
-	    rcOp ctx t u (traverse_help ctx st u x)
-	  | traverse_help ctx (Cong (t, crule, deps, branches)) u x =
-	    let
-		fun sub_step lu i x =
-		    let
-			val (fixes, assumes, subtree) = nth branches (i - 1)
-			val used = fold_rev (append o lu) (IntGraph.imm_succs deps i) u
-			val (subs, x') = traverse_help (compose ctx (fixes, assumes)) subtree used x
-			val exported_subs = map (apfst (compose (fixes, assumes))) subs
-		    in
-			(exported_subs, x')
-		    end
-	    in
-		fold_deps deps sub_step x
-			  |> apfst flatten
-	    end
+  fun traverse_help ctx (Leaf _) u x = ([], x)
+    | traverse_help ctx (RCall (t, st)) u x =
+      rcOp ctx t u (traverse_help ctx st u x)
+    | traverse_help ctx (Cong (t, crule, deps, branches)) u x =
+      let
+    fun sub_step lu i x =
+        let
+      val (fixes, assumes, subtree) = nth branches (i - 1)
+      val used = fold_rev (append o lu) (IntGraph.imm_succs deps i) u
+      val (subs, x') = traverse_help (compose ctx (fixes, assumes)) subtree used x
+      val exported_subs = map (apfst (compose (fixes, assumes))) subs
+        in
+      (exported_subs, x')
+        end
+      in
+    fold_deps deps sub_step x
+        |> apfst flatten
+      end
in
-	snd (traverse_help ([], []) tr [] x)
+  snd (traverse_help ([], []) tr [] x)
end

@@ -222,48 +222,47 @@

fun rewrite_by_tree thy h ih x tr =
let
-	fun rewrite_help fix f_as h_as x (Leaf t) = (reflexive (cterm_of thy t), x)
-	  | rewrite_help fix f_as h_as x (RCall (_ \$ arg, st)) =
-	    let
-		val (inner, (lRi,ha)::x') = rewrite_help fix f_as h_as x st
-
-					   (* Need not use the simplifier here. Can use primitive steps! *)
-		val rew_ha = if is_refl inner then I else simplify (HOL_basic_ss addsimps [inner])
-
-		val h_a_eq_h_a' = combination (reflexive (cterm_of thy h)) inner
-		val iha = import_thm thy (fix, h_as) ha (* (a', h a') : G *)
-				     |> rew_ha
-
-		val inst_ih = instantiate' [] [SOME (cterm_of thy arg)] ih
-		val eq = implies_elim (implies_elim inst_ih lRi) iha
-
-		val h_a'_eq_f_a' = eq RS eq_reflection
-		val result = transitive h_a_eq_h_a' h_a'_eq_f_a'
-	    in
-		(result, x')
-	    end
-	  | rewrite_help fix f_as h_as x (Cong (t, crule, deps, branches)) =
-	    let
-		fun sub_step lu i x =
-		    let
-			val (fixes, assumes, st) = nth branches (i - 1)
-			val used = fold_rev (cons o lu) (IntGraph.imm_succs deps i) []
-			val used_rev = map (fn u_eq => (u_eq RS sym) RS eq_reflection) used
-			val assumes' = map (simplify (HOL_basic_ss addsimps (filter_out is_refl used_rev))) assumes
-
-			val (subeq, x') = rewrite_help (fix @ fixes) (f_as @ assumes) (h_as @ assumes') x st
-			val subeq_exp = export_thm thy (fixes, map prop_of assumes) (subeq RS meta_eq_to_obj_eq)
-		    in
-			(subeq_exp, x')
-		    end
-
-		val (subthms, x') = fold_deps deps sub_step x
-	    in
-		(fold_rev (curry op COMP) subthms crule, x')
-	    end
-
+      fun rewrite_help fix f_as h_as x (Leaf t) = (reflexive (cterm_of thy t), x)
+        | rewrite_help fix f_as h_as x (RCall (_ \$ arg, st)) =
+          let
+            val (inner, (lRi,ha)::x') = rewrite_help fix f_as h_as x st
+
+             (* Need not use the simplifier here. Can use primitive steps! *)
+            val rew_ha = if is_refl inner then I else simplify (HOL_basic_ss addsimps [inner])
+
+            val h_a_eq_h_a' = combination (reflexive (cterm_of thy h)) inner
+            val iha = import_thm thy (fix, h_as) ha (* (a', h a') : G *)
+                                 |> rew_ha
+
+            val inst_ih = instantiate' [] [SOME (cterm_of thy arg)] ih
+            val eq = implies_elim (implies_elim inst_ih lRi) iha
+
+            val h_a'_eq_f_a' = eq RS eq_reflection
+            val result = transitive h_a_eq_h_a' h_a'_eq_f_a'
+          in
+            (result, x')
+          end
+        | rewrite_help fix f_as h_as x (Cong (t, crule, deps, branches)) =
+          let
+            fun sub_step lu i x =
+                let
+                  val (fixes, assumes, st) = nth branches (i - 1)
+                  val used = fold_rev (cons o lu) (IntGraph.imm_succs deps i) []
+                  val used_rev = map (fn u_eq => (u_eq RS sym) RS eq_reflection) used
+                  val assumes' = map (simplify (HOL_basic_ss addsimps (filter_out is_refl used_rev))) assumes
+
+                  val (subeq, x') = rewrite_help (fix @ fixes) (f_as @ assumes) (h_as @ assumes') x st
+                  val subeq_exp = export_thm thy (fixes, map prop_of assumes) (subeq RS meta_eq_to_obj_eq)
+                in
+                  (subeq_exp, x')
+                end
+
+            val (subthms, x') = fold_deps deps sub_step x
+          in
+            (fold_rev (curry op COMP) subthms crule, x')
+          end
in
-	rewrite_help [] [] [] x tr
+      rewrite_help [] [] [] x tr
end
-
+
end```
```--- a/src/HOL/Tools/function_package/fundef_common.ML	Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Tue Nov 07 22:06:32 2006 +0100
@@ -97,35 +97,35 @@

datatype mutual_part =
MutualPart of
-	 {
-          fvar : string * typ,
-	  cargTs: typ list,
-	  pthA: SumTools.sum_path,
-	  pthR: SumTools.sum_path,
-	  f_def: term,
+   {
+    fvar : string * typ,
+    cargTs: typ list,
+    pthA: SumTools.sum_path,
+    pthR: SumTools.sum_path,
+    f_def: term,

-	  f: term option,
-          f_defthm : thm option
-	 }
-
+    f: term option,
+    f_defthm : thm option
+   }
+

datatype mutual_info =
Mutual of
-	 {
-	  defname: string,
-          fsum_var : string * typ,
+   {
+    defname: string,
+    fsum_var : string * typ,

-	  ST: typ,
-	  RST: typ,
-	  streeA: SumTools.sum_tree,
-	  streeR: SumTools.sum_tree,
+    ST: typ,
+    RST: typ,
+    streeA: SumTools.sum_tree,
+    streeR: SumTools.sum_tree,

-	  parts: mutual_part list,
-	  fqgars: qgar list,
-	  qglrs: ((string * typ) list * term list * term * term) list,
+    parts: mutual_part list,
+    fqgars: qgar list,
+    qglrs: ((string * typ) list * term list * term * term) list,

-          fsum : term option
-	 }
+    fsum : term option
+   }

datatype prep_result =
@@ -299,12 +299,12 @@
(* with explicit types: Needed with loose bounds *)
fun mk_relmemT xT yT (x,y) R =
let
-	val pT = HOLogic.mk_prodT (xT, yT)
-	val RT = HOLogic.mk_setT pT
+  val pT = HOLogic.mk_prodT (xT, yT)
+  val RT = HOLogic.mk_setT pT
in
-	Const ("op :", [pT, RT] ---> boolT)
-	      \$ (HOLogic.pair_const xT yT \$ x \$ y)
-	      \$ R
+  Const ("op :", [pT, RT] ---> boolT)
+        \$ (HOLogic.pair_const xT yT \$ x \$ y)
+        \$ R
end

fun free_to_var (Free (v,T)) = Var ((v,0),T)```
```--- a/src/HOL/Tools/function_package/fundef_lib.ML	Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_lib.ML	Tue Nov 07 22:06:32 2006 +0100
@@ -17,18 +17,18 @@
(* Constructs a tupled abstraction from an arbitrarily nested tuple of variables and a term. *)
fun tupled_lambda vars t =
case vars of
-	    (Free v) => lambda (Free v) t
+      (Free v) => lambda (Free v) t
| (Var v) => lambda (Var v) t
| (Const ("Pair", Type ("fun", [Ta, Type ("fun", [Tb, _])]))) \$ us \$ vs =>
-	    (HOLogic.split_const (Ta,Tb, fastype_of t)) \$ (tupled_lambda us (tupled_lambda vs t))
+      (HOLogic.split_const (Ta,Tb, fastype_of t)) \$ (tupled_lambda us (tupled_lambda vs t))
| _ => raise Match

fun dest_all (Const ("all", _) \$ Abs (a as (_,T,_))) =
let
-	    val (n, body) = Term.dest_abs a
+      val (n, body) = Term.dest_abs a
in
-	    (Free (n, T), body)
+      (Free (n, T), body)
end
| dest_all _ = raise Match

@@ -36,10 +36,10 @@
(* Removes all quantifiers from a term, replacing bound variables by frees. *)
fun dest_all_all (t as (Const ("all",_) \$ _)) =
let
-	val (v,b) = dest_all t
-	val (vs, b') = dest_all_all b
+  val (v,b) = dest_all t
+  val (vs, b') = dest_all_all b
in
-	(v :: vs, b')
+  (v :: vs, b')
end
| dest_all_all t = ([],t)

@@ -54,7 +54,7 @@

val (ctx'', vs, bd) = dest_all_all_ctx ctx' body
in
-	(ctx'', (n', T) :: vs, bd)
+      (ctx'', (n', T) :: vs, bd)
end
| dest_all_all_ctx ctx t =
(ctx, [], t)```
```--- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Nov 07 22:06:32 2006 +0100
@@ -146,7 +146,7 @@
in
lthy
|> ProofContext.note_thmss_i [(("termination",
-                                 [ContextRules.intro_query NONE]), [(ProofContext.standard lthy [termination], [])])] |> snd
+                                        [ContextRules.intro_query NONE]), [(ProofContext.standard lthy [termination], [])])] |> snd
|> Proof.theorem_i PureThy.internalK NONE
(total_termination_afterqed name data) NONE ("", [])
[(("", []), [(goal, [])])]```
```--- a/src/HOL/Tools/function_package/fundef_prep.ML	Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_prep.ML	Tue Nov 07 22:06:32 2006 +0100
@@ -465,8 +465,7 @@

fun inst_RC thy fvar f (rcfix, rcassm, rcarg) =
let
-      fun inst_term t =
-          subst_bound(f, abstract_over (fvar, t))
+      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```
```--- a/src/HOL/Tools/function_package/fundef_proof.ML	Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_proof.ML	Tue Nov 07 22:06:32 2006 +0100
@@ -11,7 +11,7 @@
sig

val mk_partial_rules : theory -> FundefCommon.prep_result
-			   -> thm -> FundefCommon.fundef_result
+         -> thm -> FundefCommon.fundef_result
end

@@ -43,128 +43,128 @@

fun mk_psimp thy globals R f_iff graph_is_function clause valthm =
let
-	val Globals {domT, z, ...} = globals
+  val Globals {domT, z, ...} = globals

-	val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {qs, cqs, gs, lhs, rhs, ags, ...}, ...} = clause
-	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" *)
+  val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {qs, cqs, gs, lhs, rhs, ags, ...}, ...} = clause
+  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)
+      ((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

fun mk_partial_induct_rule thy globals R complete_thm clauses =
let
-	val Globals {domT, x, z, a, P, D, ...} = globals
+  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 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_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
+  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
+  (* 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

-	fun prove_case clause =
-	    let
-		val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, gs, lhs, rhs, 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 aihyp = assume ihyp

-                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_rev 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)
+  fun prove_case clause =
+      let
+    val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, gs, lhs, rhs, 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_rev 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 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 (cases, steps) = split_list (map prove_case clauses)

-	val subset_induct_all = fold_rev (forall_intr o cterm_of thy) [P, a, D] subset_induct_rule
+  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 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)
+  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)
+      (subset_induct_all, simple_induct_rule)
end

@@ -172,19 +172,19 @@
(* Does this work with Guards??? *)
fun mk_domain_intro thy globals R R_cases clause =
let
-	val Globals {z, domT, ...} = globals
-	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
+      val Globals {z, domT, ...} = globals
+      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)
+      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

@@ -192,145 +192,145 @@

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 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 = 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 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 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
+            val sub' = sub @ [(([],[]), acc)]
+          in
+            (sub', (hyp :: hyps, ethm :: thms))
+          end
+        | step _ _ _ _ = raise Match
in
-	FundefCtxTree.traverse_tree step tree
+      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 ("FunDef.in_rel", mk_relT (domT, domT) --> fastype_of R) \$ Rrel
-
-	val wfR' = cterm_of thy (Trueprop (Const ("FunDef.wfP", (domT --> domT --> boolT) --> boolT) \$ R')) (* "wf R'" *)
+      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 ("FunDef.in_rel", mk_relT (domT, domT) --> fastype_of R) \$ Rrel
+
+      val wfR' = cterm_of thy (Trueprop (Const ("FunDef.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

-	(* 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 ([],[])
+      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')
-	    |> 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)
+      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')
+        |> 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
-
+

fun mk_partial_rules thy data provedgoal =
let
-	val Prep {globals, G, f, R, clauses, values, R_cases, ex1_iff, ...} = data
-
-        val _ = print "Closing Derivation"
-
-	val provedgoal = Drule.close_derivation provedgoal
-
-        val _ = print "Getting gif"
-
-        val graph_is_function = (provedgoal COMP conjunctionD1)
-                                  |> forall_elim_vars 0
-
-        val _ = print "Getting cases"
-
-        val complete_thm = provedgoal COMP conjunctionD2
-
-        val _ = print "making f_iff"
-
-	val f_iff = (graph_is_function RS ex1_iff)
-
-	val _ = Output.debug "Proving simplification rules"
-	val psimps  = map2 (mk_psimp thy globals R f_iff graph_is_function) clauses values
-
-	val _ = Output.debug "Proving partial induction rule"
-	val (subset_pinduct, simple_pinduct) = mk_partial_induct_rule thy globals R complete_thm clauses
-
-	val _ = Output.debug "Proving nested termination rule"
-	val total_intro = mk_nest_term_rule thy globals R R_cases clauses
-
-	val _ = Output.debug "Proving domain introduction rules"
-	val dom_intros = map (mk_domain_intro thy globals R R_cases) clauses
+      val Prep {globals, G, f, R, clauses, values, R_cases, ex1_iff, ...} = data
+
+      val _ = Output.debug "Closing Derivation"
+
+      val provedgoal = Drule.close_derivation provedgoal
+
+      val _ = Output.debug "Getting function theorem"
+
+      val graph_is_function = (provedgoal COMP conjunctionD1)
+                                |> forall_elim_vars 0
+
+      val _ = Output.debug "Getting cases"
+
+      val complete_thm = provedgoal COMP conjunctionD2
+
+      val _ = Output.debug "Making f_iff"
+
+      val f_iff = (graph_is_function RS ex1_iff)
+
+      val _ = Output.debug "Proving simplification rules"
+      val psimps  = map2 (mk_psimp thy globals R f_iff graph_is_function) clauses values
+
+      val _ = Output.debug "Proving partial induction rule"
+      val (subset_pinduct, simple_pinduct) = mk_partial_induct_rule thy globals R complete_thm clauses
+
+      val _ = Output.debug "Proving nested termination rule"
+      val total_intro = mk_nest_term_rule thy globals R R_cases clauses
+
+      val _ = Output.debug "Proving domain introduction rules"
+      val dom_intros = map (mk_domain_intro thy globals R R_cases) clauses
in
-	FundefResult {f=f, G=G, R=R, completeness=complete_thm,
-	 psimps=psimps, subset_pinduct=subset_pinduct, simple_pinduct=simple_pinduct, total_intro=total_intro,
-	 dom_intros=dom_intros}
+      FundefResult {f=f, G=G, R=R, completeness=complete_thm,
+                    psimps=psimps, subset_pinduct=subset_pinduct, simple_pinduct=simple_pinduct, total_intro=total_intro,
+                    dom_intros=dom_intros}
end
-
-
+
+
end

```
```--- a/src/HOL/Tools/function_package/inductive_wrap.ML	Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/inductive_wrap.ML	Tue Nov 07 22:06:32 2006 +0100
@@ -3,21 +3,8 @@
Author:     Alexander Krauss, TU Muenchen

-This is a wrapper around the inductive package which corrects some of its
-slightly annoying behaviours and makes the whole business more controllable.
-
-Specifically:
-
-- Following newer Isar conventions, declaration and definition are done in one step
-
-- The specification is expected in fully quantified form. This allows the client to
-  control the variable order. The variables will appear in the result in the same order.
-  This is especially relevant for the elimination rule, where the order usually *does* matter.
-
-
-All this will probably become obsolete in the near future, when the new "predicate" package
-is in place.
-
+A wrapper around the inductive package, restoring the quantifiers in
+the introduction and elimination rules.
*)

signature FUNDEF_INDUCTIVE_WRAP =
@@ -36,7 +23,7 @@
let
val thy = theory_of_thm thm
val frees = frees_in_term ctxt t
-                                  |> remove (op =) lfix
+                  |> remove (op =) lfix
val vars = Term.add_vars (prop_of thm) [] |> rev

val varmap = frees ~~ vars```
```--- a/src/HOL/Tools/function_package/lexicographic_order.ML	Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Tue Nov 07 22:06:32 2006 +0100
@@ -7,8 +7,8 @@

signature LEXICOGRAPHIC_ORDER =
sig
-    val lexicographic_order : Method.method
-    val setup: theory -> theory
+  val lexicographic_order : Method.method
+  val setup: theory -> theory
end

structure LexicographicOrder : LEXICOGRAPHIC_ORDER =
@@ -19,222 +19,222 @@
val wf_measures = thm "wf_measures"
val measures_less = thm "measures_less"
val measures_lesseq = thm "measures_lesseq"
-
+
fun del_index (n, []) = []
| del_index (n, x :: xs) =
-      if n>0 then x :: del_index (n - 1, xs) else xs
+    if n>0 then x :: del_index (n - 1, xs) else xs

fun transpose ([]::_) = []
| transpose xss = map hd xss :: transpose (map tl xss)

fun mk_sum_case (f1, f2) =
case (fastype_of f1, fastype_of f2) of
-	(Type("fun", [A, B]), Type("fun", [C, D])) =>
-	if (B = D) then
-            Const("Datatype.sum.sum_case", (A --> B) --> (C --> D) --> Type("+", [A,C]) --> B) \$ f1 \$ f2
-	else raise TERM ("mk_sum_case: range type mismatch", [f1, f2])
-      | _ => raise TERM ("mk_sum_case", [f1, f2])
-
+      (Type("fun", [A, B]), Type("fun", [C, D])) =>
+      if (B = D) then
+        Const("Datatype.sum.sum_case", (A --> B) --> (C --> D) --> Type("+", [A,C]) --> B) \$ f1 \$ f2
+      else raise TERM ("mk_sum_case: range type mismatch", [f1, f2])
+    | _ => raise TERM ("mk_sum_case", [f1, f2])
+
fun dest_wf (Const ("Wellfounded_Recursion.wf", _) \$ t) = t
| dest_wf t = raise TERM ("dest_wf", [t])
-
+
datatype cell = Less of thm | LessEq of thm | None of thm | False of thm;
-
+
fun is_Less cell = case cell of (Less _) => true | _ => false
-
+
fun is_LessEq cell = case cell of (LessEq _) => true | _ => false
-
+
fun thm_of_cell cell =
case cell of
-	Less thm => thm
-      | LessEq thm => thm
-      | False thm => thm
-      | None thm => thm
-
+      Less thm => thm
+    | LessEq thm => thm
+    | False thm => thm
+    | None thm => thm
+
fun mk_base_fun_bodys (t : term) (tt : typ) =
case tt of
-	Type("*", [ft, st]) => (mk_base_fun_bodys (Const("fst", tt --> ft) \$ t) ft) @ (mk_base_fun_bodys (Const("snd", tt --> st) \$ t) st)
-      | _ => [(t, tt)]
-
+      Type("*", [ft, st]) => (mk_base_fun_bodys (Const("fst", tt --> ft) \$ t) ft) @ (mk_base_fun_bodys (Const("snd", tt --> st) \$ t) st)
+    | _ => [(t, tt)]
+
fun mk_base_fun_header fulltyp (t, typ) =
if typ = HOLogic.natT then
-	Abs ("x", fulltyp, t)
+      Abs ("x", fulltyp, t)
else Abs ("x", fulltyp, Const("Nat.size", typ --> HOLogic.natT) \$ t)
-
+
fun mk_base_funs (tt: typ) =
mk_base_fun_bodys (Bound 0) tt |>
-
+
fun mk_ext_base_funs (tt : typ) =
case tt of
-	Type("+", [ft, st]) =>
-	product (mk_ext_base_funs ft) (mk_ext_base_funs st)
-        |> map mk_sum_case
-      | _ => mk_base_funs tt
-
+      Type("+", [ft, st]) =>
+      product (mk_ext_base_funs ft) (mk_ext_base_funs st)
+              |> map mk_sum_case
+    | _ => mk_base_funs tt
+
fun dest_term (t : term) =
let
-	val (vars, prop) = (FundefLib.dest_all_all t)
-	val prems = Logic.strip_imp_prems prop
-	val (tuple, rel) = Logic.strip_imp_concl prop
-                           |> HOLogic.dest_Trueprop
-                           |> HOLogic.dest_mem
-	val (lhs, rhs) = HOLogic.dest_prod tuple
+      val (vars, prop) = (FundefLib.dest_all_all t)
+      val prems = Logic.strip_imp_prems prop
+      val (tuple, rel) = Logic.strip_imp_concl prop
+                         |> HOLogic.dest_Trueprop
+                         |> HOLogic.dest_mem
+      val (lhs, rhs) = HOLogic.dest_prod tuple
in
-	(vars, prems, lhs, rhs, rel)
+      (vars, prems, lhs, rhs, rel)
end
-
+
fun mk_goal (vars, prems, lhs, rhs) rel =
let
-	val concl = HOLogic.mk_binrel rel (lhs, rhs) |> HOLogic.mk_Trueprop
-    in
-	Logic.list_implies (prems, concl) |>
-	fold_rev FundefLib.mk_forall vars
+      val concl = HOLogic.mk_binrel rel (lhs, rhs) |> HOLogic.mk_Trueprop
+    in
+      Logic.list_implies (prems, concl) |>
+                         fold_rev FundefLib.mk_forall vars
end
-
+
fun prove (thy: theory) (t: term) =
cterm_of thy t |> Goal.init
|> SINGLE (CLASIMPSET auto_tac) |> the
-
+
fun mk_cell (thy : theory) (vars, prems) (lhs, rhs) =
-    let
-	val goals = mk_goal (vars, prems, lhs, rhs)
-	val less_thm = goals "Orderings.less" |> prove thy
+    let
+      val goals = mk_goal (vars, prems, lhs, rhs)
+      val less_thm = goals "Orderings.less" |> prove thy
in
-	if Thm.no_prems less_thm then
-	    Less (Goal.finish less_thm)
-	else
-	    let
-		val lesseq_thm = goals "Orderings.less_eq" |> prove thy
-	    in
-		if Thm.no_prems lesseq_thm then
-		    LessEq (Goal.finish lesseq_thm)
-		else
-		    if prems_of lesseq_thm = [HOLogic.Trueprop \$ HOLogic.false_const] then False lesseq_thm
-		    else None lesseq_thm
-	    end
+      if Thm.no_prems less_thm then
+        Less (Goal.finish less_thm)
+      else
+        let
+          val lesseq_thm = goals "Orderings.less_eq" |> prove thy
+        in
+          if Thm.no_prems lesseq_thm then
+            LessEq (Goal.finish lesseq_thm)
+          else
+            if prems_of lesseq_thm = [HOLogic.Trueprop \$ HOLogic.false_const] then False lesseq_thm
+            else None lesseq_thm
+        end
end
-
+
fun mk_row (thy: theory) base_funs (t : term) =
let
-	val (vars, prems, lhs, rhs, _) = dest_term t
-	val lhs_list = map (fn x => x \$ lhs) base_funs
-	val rhs_list = map (fn x => x \$ rhs) base_funs
+      val (vars, prems, lhs, rhs, _) = dest_term t
+      val lhs_list = map (fn x => x \$ lhs) base_funs
+      val rhs_list = map (fn x => x \$ rhs) base_funs
in
-	map (mk_cell thy (vars, prems)) (lhs_list ~~ rhs_list)
+      map (mk_cell thy (vars, prems)) (lhs_list ~~ rhs_list)
end
-
+
(* simple depth-first search algorithm for the table *)
fun search_table table =
case table of
-	[] => SOME []
-      | _ =>
-	let
-	    val check_col = forall (fn c => is_Less c orelse is_LessEq c)
-            val col = find_index (check_col) (transpose table)
-	in case col of
-	       ~1 => NONE
-             | _ =>
-               let
-		   val order_opt = table |> filter_out (fn x => is_Less (nth x col)) |> map (curry del_index col) |> search_table
-		   val transform_order = (fn col => map (fn x => if x>=col then x+1 else x))
-               in case order_opt of
-		      NONE => NONE
-		    | SOME order =>SOME (col::(transform_order col order))
-	       end
-	end
-
+      [] => SOME []
+    | _ =>
+      let
+        val check_col = forall (fn c => is_Less c orelse is_LessEq c)
+        val col = find_index (check_col) (transpose table)
+      in case col of
+           ~1 => NONE
+         | _ =>
+           let
+             val order_opt = table |> filter_out (fn x => is_Less (nth x col)) |> map (curry del_index col) |> search_table
+             val transform_order = (fn col => map (fn x => if x>=col then x+1 else x))
+           in case order_opt of
+                NONE => NONE
+              | SOME order =>SOME (col::(transform_order col order))
+           end
+      end
+
fun prove_row row (st : thm) =
case row of
-        [] => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun prove_row (row is empty)"
-      | cell::tail =>
-	case cell of
-	    Less less_thm =>
-	    let
-		val next_thm = st |> SINGLE (rtac measures_less 1) |> the
-	    in
-		implies_elim next_thm less_thm
-	    end
-	  | LessEq lesseq_thm =>
-	    let
-		val next_thm = st |> SINGLE (rtac measures_lesseq 1) |> the
-	    in
-		implies_elim next_thm lesseq_thm |>
-                prove_row tail
-	    end
-          | _ => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun prove_row (Only expecting Less or LessEq)"
-
+      [] => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun prove_row (row is empty)"
+    | cell::tail =>
+      case cell of
+        Less less_thm =>
+        let
+          val next_thm = st |> SINGLE (rtac measures_less 1) |> the
+        in
+          implies_elim next_thm less_thm
+        end
+      | LessEq lesseq_thm =>
+        let
+          val next_thm = st |> SINGLE (rtac measures_lesseq 1) |> the
+        in
+          implies_elim next_thm lesseq_thm
+          |> prove_row tail
+        end
+      | _ => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun prove_row (Only expecting Less or LessEq)"
+
fun pr_unprovable_subgoals table =
filter (fn x => not (is_Less x) andalso not (is_LessEq x)) (flat table)
-	   |> map ((fn th => Pretty.string_of (Pretty.chunks (Display.pretty_goals (Thm.nprems_of th) th))) o thm_of_cell)
-
+    |> map ((fn th => Pretty.string_of (Pretty.chunks (Display.pretty_goals (Thm.nprems_of th) th))) o thm_of_cell)
+
fun pr_goal thy t i =
let
-	val (_, prems, lhs, rhs, _) = dest_term t
-	val prterm = string_of_cterm o (cterm_of thy)
+      val (_, prems, lhs, rhs, _) = dest_term t
+      val prterm = string_of_cterm o (cterm_of thy)
in
-	(* also show prems? *)
+      (* also show prems? *)
i ^ ") " ^ (prterm lhs) ^ " '<' " ^ (prterm rhs)
end
-
+
fun pr_fun thy t i =
(string_of_int i) ^ ") " ^ (string_of_cterm (cterm_of thy t))
-
+
fun pr_cell cell = case cell of Less _ => " <  "
-				| LessEq _ => " <= "
-				| None _ => " N  "
-				| False _ => " F  "
-
+                              | LessEq _ => " <= "
+                              | None _ => " N  "
+                              | False _ => " F  "
+
(* fun pr_err: prints the table if tactic failed *)
fun pr_err table thy tl base_funs =
let
-	val gc = map (fn i => chr (i + 96)) (1 upto (length table))
-	val mc = 1 upto (length base_funs)
-	val tstr = ("   " ^ (concat (map (fn i => " " ^ (string_of_int i) ^ "  ") mc))) ::
-		   (map2 (fn r => fn i => i ^ ": " ^ (concat (map pr_cell r))) table gc)
-	val gstr = ("Goals:"::(map2 (pr_goal thy) tl gc))
-	val mstr = ("Measures:"::(map2 (pr_fun thy) base_funs mc))
-	val ustr = ("Unfinished subgoals:"::(pr_unprovable_subgoals table))
+      val gc = map (fn i => chr (i + 96)) (1 upto (length table))
+      val mc = 1 upto (length base_funs)
+      val tstr = ("   " ^ (concat (map (fn i => " " ^ (string_of_int i) ^ "  ") mc))) ::
+                 (map2 (fn r => fn i => i ^ ": " ^ (concat (map pr_cell r))) table gc)
+      val gstr = ("Goals:"::(map2 (pr_goal thy) tl gc))
+      val mstr = ("Measures:"::(map2 (pr_fun thy) base_funs mc))
+      val ustr = ("Unfinished subgoals:"::(pr_unprovable_subgoals table))
in
-	tstr @ gstr @ mstr @ ustr
+      tstr @ gstr @ mstr @ ustr
end
-
+
(* the main function: create table, search table, create relation,
and prove the subgoals *)
fun lexicographic_order_tac (st: thm) =
let
-	val thy = theory_of_thm st
-        val termination_thm = ProofContext.get_thm (Variable.thm_context st) (Name "termination")
-	val next_st = SINGLE (rtac termination_thm 1) st |> the
-        val premlist = prems_of next_st
+      val thy = theory_of_thm st
+      val termination_thm = ProofContext.get_thm (Variable.thm_context st) (Name "termination")
+      val next_st = SINGLE (rtac termination_thm 1) st |> the
+      val premlist = prems_of next_st
in
-        case premlist of
+      case premlist of
[] => error "invalid number of subgoals for this tactic - expecting at least 1 subgoal"
| (wf::tl) => let
-		val (var, prop) = FundefLib.dest_all wf
-		val rel = HOLogic.dest_Trueprop prop |> dest_wf |> head_of
-		val crel = cterm_of thy rel
-		val base_funs = mk_ext_base_funs (fastype_of var)
-		val _ = writeln "Creating table"
-		val table = map (mk_row thy base_funs) tl
-		val _ = writeln "Searching for lexicographic order"
-		val possible_order = search_table table
-	    in
-		case possible_order of
-		    NONE => error (cat_lines ("Could not prove it by lexicographic order:"::(pr_err table thy tl base_funs)))
-		  | SOME order  => let
-			val clean_table = map (fn x => map (nth x) order) table
-			val funs = map (nth base_funs) order
-			val list = HOLogic.mk_list (fn x => x) (fastype_of var --> HOLogic.natT) funs
-			val relterm = Abs ("x", fastype_of var, Const(measures, (fastype_of list) --> (range_type (fastype_of rel))) \$ list)
-			val crelterm = cterm_of thy relterm
-			val _ = writeln ("Instantiating R with " ^ (string_of_cterm crelterm))
-			val _ = writeln "Proving subgoals"
-		    in
-			next_st |> cterm_instantiate [(crel, crelterm)]
-				|> SINGLE (rtac wf_measures 1) |> the
-				|> fold prove_row clean_table
-				|> Seq.single
+    val (var, prop) = FundefLib.dest_all wf
+    val rel = HOLogic.dest_Trueprop prop |> dest_wf |> head_of
+    val crel = cterm_of thy rel
+    val base_funs = mk_ext_base_funs (fastype_of var)
+    val _ = writeln "Creating table"
+    val table = map (mk_row thy base_funs) tl
+    val _ = writeln "Searching for lexicographic order"
+    val possible_order = search_table table
+      in
+    case possible_order of
+        NONE => error (cat_lines ("Could not prove it by lexicographic order:"::(pr_err table thy tl base_funs)))
+      | SOME order  => let
+      val clean_table = map (fn x => map (nth x) order) table
+      val funs = map (nth base_funs) order
+      val list = HOLogic.mk_list (fn x => x) (fastype_of var --> HOLogic.natT) funs
+      val relterm = Abs ("x", fastype_of var, Const(measures, (fastype_of list) --> (range_type (fastype_of rel))) \$ list)
+      val crelterm = cterm_of thy relterm
+      val _ = writeln ("Instantiating R with " ^ (string_of_cterm crelterm))
+      val _ = writeln "Proving subgoals"
+        in
+      next_st |> cterm_instantiate [(crel, crelterm)]
+        |> SINGLE (rtac wf_measures 1) |> the
+        |> fold prove_row clean_table
+        |> Seq.single
end
end
end```
```--- a/src/HOL/Tools/function_package/mutual.ML	Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/mutual.ML	Tue Nov 07 22:06:32 2006 +0100
@@ -50,7 +50,7 @@
fun split_def ctxt fnames geq arities =
let
fun input_error msg = error (cat_lines [msg, ProofContext.string_of_term ctxt geq])
-
+
val (qs, imp) = open_all_all geq

val gs = Logic.strip_imp_prems imp
@@ -69,7 +69,7 @@
|> map (fst o nth (rev qs))
-
+
val _ = if null rvs then ()
else input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:")
@@ -83,17 +83,17 @@
val k = length args

val arities' = case Symtab.lookup arities fname of
-                   NONE => Symtab.update (fname, k) arities
-                 | SOME i => if (i <> k)
-                             then input_error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations")
-                             else arities
+                       NONE => Symtab.update (fname, k) arities
+                     | SOME i => if (i <> k)
+                                 then input_error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations")
+                                 else arities
in
-        ((fname, qs, gs, args, rhs), arities')
+      ((fname, qs, gs, args, rhs), arities')
end
-
+
fun get_part fname =
the o find_first (fn (MutualPart {fvar=(n,_), ...}) => n = fname)
-
+
(* FIXME *)
fun mk_prod_abs e (t1, t2) =
let
@@ -141,7 +141,7 @@
in
(MutualPart {fvar=fvar,cargTs=caTs,pthA=pthA,pthR=pthR,f_def=def,f=NONE,f_defthm=NONE}, rew)
end
-
+
val (parts, rews) = split_list (map4 define fs caTss pthsA pthsR)

fun convert_eqs (f, qs, gs, args, rhs) =
@@ -171,10 +171,10 @@
lthy
in
(MutualPart {fvar=(fname, fT), cargTs=cargTs, pthA=pthA, pthR=pthR, f_def=f_def,
-                        f=SOME f, f_defthm=SOME f_defthm },
+                         f=SOME f, f_defthm=SOME f_defthm },
lthy')
end
-
+
val Mutual { defname, fsum_var, ST, RST, streeA, streeR, parts, fqgars, qglrs, ... } = mutual
val (parts', lthy') = fold_map def (parts ~~ fixes) lthy
in
@@ -186,39 +186,39 @@

fun prepare_fundef_mutual fixes eqss default lthy =
let
-        val mutual = analyze_eqs lthy (map fst fixes) eqss
-        val Mutual {defname, fsum_var=(n, T), qglrs, ...} = mutual
-
-        val (prep_result, fsum, lthy') =
-            FundefPrep.prepare_fundef defname (n, T, NoSyn) qglrs default lthy
-
-        val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
+      val mutual = analyze_eqs lthy (map fst fixes) eqss
+      val Mutual {defname, fsum_var=(n, T), qglrs, ...} = mutual
+
+      val (prep_result, fsum, lthy') =
+          FundefPrep.prepare_fundef defname (n, T, NoSyn) qglrs default lthy
+
+      val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
in
((mutual', defname, prep_result), lthy'')
end
-
+

(* Beta-reduce both sides of a meta-equality *)
fun beta_norm_eq thm =
let
-        val (lhs, rhs) = dest_equals (cprop_of thm)
-        val lhs_conv = beta_conversion false lhs
-        val rhs_conv = beta_conversion false rhs
+      val (lhs, rhs) = dest_equals (cprop_of thm)
+      val lhs_conv = beta_conversion false lhs
+      val rhs_conv = beta_conversion false rhs
in
-        transitive (symmetric lhs_conv) (transitive thm rhs_conv)
+      transitive (symmetric lhs_conv) (transitive thm rhs_conv)
end
-
+
fun beta_reduce thm = Thm.equal_elim (Thm.beta_conversion true (cprop_of thm)) thm
-
-
+
+
fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F =
let
val thy = ProofContext.theory_of ctxt
-
+
val oqnames = map fst pre_qs
val (qs, ctxt') = Variable.variant_fixes oqnames ctxt
-                                           |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
-
+                        |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
+
fun inst t = subst_bounds (rev qs, t)
val gs = map inst pre_gs
val args = map inst pre_args
@@ -240,7 +240,7 @@
fun recover_mutual_psimp thy RST streeR all_f_defs parts (f, _, _, args, _) import (export : thm -> thm) sum_psimp_eq =
let
val (MutualPart {f_defthm=SOME f_def, pthR, ...}) = get_part f parts
-
+
val psimp = import sum_psimp_eq
val (simp, restore_cond) = case cprems_of psimp of
[] => (psimp, I)
@@ -275,46 +275,46 @@
|> fold_rev forall_intr xs
|> forall_elim_vars 0
end
-
+

fun mutual_induct_rules thy induct all_f_defs (Mutual {RST, parts, streeA, ...}) =
let
val newPs = map2 (fn Pname => fn MutualPart {cargTs, ...} =>
-                                   Free (Pname, cargTs ---> HOLogic.boolT))
+                                       Free (Pname, cargTs ---> HOLogic.boolT))
(mutual_induct_Pnames (length parts))
parts
-
-        fun mk_P (MutualPart {cargTs, ...}) P =
-            let
-                val avars = map_index (fn (i,T) => Var (("a", i), T)) cargTs
-                val atup = foldr1 HOLogic.mk_prod avars
-            in
-                tupled_lambda atup (list_comb (P, avars))
-            end
-
-        val Ps = map2 mk_P parts newPs
-        val case_exp = SumTools.mk_sumcases streeA HOLogic.boolT Ps
-
-        val induct_inst =
-            forall_elim (cterm_of thy case_exp) induct
-                        |> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules))
-                        |> full_simplify (HOL_basic_ss addsimps all_f_defs)
-
-        fun mk_proj rule (MutualPart {cargTs, pthA, ...}) =
-            let
-                val afs = map_index (fn (i,T) => Free ("a" ^ string_of_int i, T)) cargTs
-                val inj = SumTools.mk_inj streeA pthA (foldr1 HOLogic.mk_prod afs)
-            in
-                rule
-                    |> forall_elim (cterm_of thy inj)
-                    |> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules))
-                    |> fold_rev (forall_intr o cterm_of thy) (afs @ newPs)
-            end
-
+
+      fun mk_P (MutualPart {cargTs, ...}) P =
+          let
+            val avars = map_index (fn (i,T) => Var (("a", i), T)) cargTs
+            val atup = foldr1 HOLogic.mk_prod avars
+          in
+            tupled_lambda atup (list_comb (P, avars))
+          end
+
+      val Ps = map2 mk_P parts newPs
+      val case_exp = SumTools.mk_sumcases streeA HOLogic.boolT Ps
+
+      val induct_inst =
+          forall_elim (cterm_of thy case_exp) induct
+                      |> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules))
+                      |> full_simplify (HOL_basic_ss addsimps all_f_defs)
+
+      fun mk_proj rule (MutualPart {cargTs, pthA, ...}) =
+          let
+            val afs = map_index (fn (i,T) => Free ("a" ^ string_of_int i, T)) cargTs
+            val inj = SumTools.mk_inj streeA pthA (foldr1 HOLogic.mk_prod afs)
+          in
+            rule
+              |> forall_elim (cterm_of thy inj)
+              |> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules))
+              |> fold_rev (forall_intr o cterm_of thy) (afs @ newPs)
+          end
+
in
map (mk_proj induct_inst) parts
end
-
+

@@ -322,44 +322,44 @@
fun mk_partial_rules_mutual lthy (m as Mutual {RST, parts, streeR, fqgars, ...}) data prep_result =
let
val thy = ProofContext.theory_of lthy
-
+
(* FIXME !? *)
-      val expand = Assumption.export false lthy (LocalTheory.target_of lthy);
-      val expand_term = Drule.term_rule thy expand;
-
+      val expand = Assumption.export false lthy (LocalTheory.target_of lthy)
+      val expand_term = Drule.term_rule thy expand
+
val result = FundefProof.mk_partial_rules thy data prep_result
val FundefResult {f, G, R, completeness, psimps, subset_pinduct,simple_pinduct,total_intro,dom_intros} = result
-
+
val all_f_defs = map (fn MutualPart {f_defthm = SOME f_def, cargTs, ...} =>
mk_applied_form lthy cargTs (symmetric (Thm.freezeT f_def)))
parts
-
+
fun mk_mpsimp fqgar sum_psimp =
in_context lthy fqgar (recover_mutual_psimp thy RST streeR all_f_defs parts) sum_psimp
-
+
val mpsimps = map2 mk_mpsimp fqgars psimps
-
+
val minducts = mutual_induct_rules thy simple_pinduct all_f_defs m
val termination = full_simplify (HOL_basic_ss addsimps all_f_defs) total_intro
in
FundefMResult { f=expand_term f, G=expand_term G, R=expand_term R,
-                                  psimps=map expand mpsimps, subset_pinducts=[expand subset_pinduct], simple_pinducts=map expand minducts,
-                                  cases=expand completeness, termination=expand termination,
+                      psimps=map expand mpsimps, subset_pinducts=[expand subset_pinduct], simple_pinducts=map expand minducts,
+                      cases=expand completeness, termination=expand termination,
domintros=map expand dom_intros }
end
-
-
-
+
+
+
(* puts an object in the "right bucket" *)
fun store_grouped P x [] = []
| store_grouped P x ((l, xs)::bs) =
if P (x, l) then ((l, x::xs)::bs) else ((l, xs)::store_grouped P x bs)
-
+
fun sort_by_function (Mutual {fqgars, ...}) names xs =
-      fold_rev (store_grouped (eq_str o apfst fst))  (* fill *)
-               (map name_of_fqgar fqgars ~~ xs)      (* the name-thm pairs *)
-               (map (rpair []) names)                (* in the empty buckets labeled with names *)
-
-         |> map (snd #> map snd)                     (* and remove the labels afterwards *)
-
+    fold_rev (store_grouped (eq_str o apfst fst))  (* fill *)
+             (map name_of_fqgar fqgars ~~ xs)      (* the name-thm pairs *)
+             (map (rpair []) names)                (* in the empty buckets labeled with names *)
+
+             |> map (snd #> map snd)                     (* and remove the labels afterwards *)
+
end```
```--- a/src/HOL/Tools/function_package/pattern_split.ML	Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/pattern_split.ML	Tue Nov 07 22:06:32 2006 +0100
@@ -12,10 +12,10 @@
signature FUNDEF_SPLIT =
sig
val split_some_equations :
-    Proof.context -> (bool * term) list -> term list list
+      Proof.context -> (bool * term) list -> term list list

val split_all_equations :
-    Proof.context -> term list -> term list list
+      Proof.context -> term list -> term list list
end

structure FundefSplit : FUNDEF_SPLIT =
@@ -36,16 +36,16 @@
fun saturate ctx vs t =
fold (fn T => fn (vs, t) => new_var ctx vs T |> apsnd (curry op \$ t))
(binder_types (fastype_of t)) (vs, t)
-
-
+
+
(* This is copied from "fundef_datatype.ML" *)
fun inst_constrs_of thy (T as Type (name, _)) =
-        map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
-            (the (DatatypePackage.get_datatype_constrs thy name))
+    map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
+        (the (DatatypePackage.get_datatype_constrs thy name))
| inst_constrs_of thy t = (print t; sys_error "inst_constrs_of")
-
-
-
+
+
+

fun join ((vs1,sub1), (vs2,sub2)) = (merge (op aconv) (vs1,vs2), sub1 @ sub2)
fun join_product (xs, ys) = map join (product xs ys)
@@ -91,12 +91,12 @@
fun pattern_subtract ctx eq2 eq1 =
let
val thy = ProofContext.theory_of ctx
-
+
val (vs, feq1 as (_ \$ (_ \$ lhs1 \$ _))) = dest_all_all eq1
val (_,  _ \$ (_ \$ lhs2 \$ _)) = dest_all_all eq2
-
+
val substs = pattern_subtract_subst ctx vs lhs1 lhs2
-
+
fun instantiate (vs', sigma) =
let
val t = Pattern.rewrite_term thy sigma [] feq1
@@ -106,7 +106,7 @@
in
map instantiate substs
end
-
+

(* ps - p' *)
fun pattern_subtract_from_many ctx p'=
@@ -128,7 +128,7 @@
in
split_aux [] eqns
end
-
+
fun split_all_equations ctx =
split_some_equations ctx o map (pair true)
```
```--- a/src/HOL/Tools/function_package/sum_tools.ML	Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/sum_tools.ML	Tue Nov 07 22:06:32 2006 +0100
@@ -46,30 +46,30 @@
| Branch of (typ * (typ * sum_tree) * (typ * sum_tree))

type sum_path = bool list (* true: left, false: right *)
-
+
fun sum_type_of (Leaf T) = T
| sum_type_of (Branch (ST,(LT,_),(RT,_))) = ST
-
-
+
+
fun mk_tree Ts =
let
-	fun mk_tree' 1 [T] = (T, Leaf T, [[]])
-	  | mk_tree' n Ts =
-	    let
-		val n2 = n div 2
-		val (lTs, rTs) = chop n2 Ts
-		val (TL, ltree, lpaths) = mk_tree' n2 lTs
-		val (TR, rtree, rpaths) = mk_tree' (n - n2) rTs
-		val T = mk_sumT TL TR
-		val pths = map (cons true) lpaths @ map (cons false) rpaths
-	    in
-		(T, Branch (T, (TL, ltree), (TR, rtree)), pths)
-	    end
+      fun mk_tree' 1 [T] = (T, Leaf T, [[]])
+        | mk_tree' n Ts =
+          let
+            val n2 = n div 2
+            val (lTs, rTs) = chop n2 Ts
+            val (TL, ltree, lpaths) = mk_tree' n2 lTs
+            val (TR, rtree, rpaths) = mk_tree' (n - n2) rTs
+            val T = mk_sumT TL TR
+            val pths = map (cons true) lpaths @ map (cons false) rpaths
+          in
+            (T, Branch (T, (TL, ltree), (TR, rtree)), pths)
+          end
in
-	mk_tree' (length Ts) Ts
+      mk_tree' (length Ts) Ts
end
-
-
+
+
fun mk_tree_distinct Ts =
let
fun insert_once T Ts =
@@ -78,9 +78,9 @@
in
if i = ~1 then (length Ts, Ts @ [T]) else (i, Ts)
end
-
+
val (idxs, dist_Ts) = fold_map insert_once Ts []
-
+
val (ST, tree, pths) = mk_tree dist_Ts
in
(ST, tree, map (nth pths) idxs)
@@ -104,19 +104,19 @@

fun mk_sumcases tree T ts =
let
-	fun mk_sumcases' (Leaf _) (t::ts) = (t,ts)
-	  | mk_sumcases' (Branch (ST, (LT, ltr), (RT, rtr))) ts =
-	    let
-		val (lcase, ts') = mk_sumcases' ltr ts
-		val (rcase, ts'') = mk_sumcases' rtr ts'
-	    in
-		(mk_sumcase LT RT T lcase rcase, ts'')
-	    end
-	  | mk_sumcases' _ [] = sys_error "mk_sumcases"
+      fun mk_sumcases' (Leaf _) (t::ts) = (t,ts)
+        | mk_sumcases' (Branch (ST, (LT, ltr), (RT, rtr))) ts =
+          let
+            val (lcase, ts') = mk_sumcases' ltr ts
+            val (rcase, ts'') = mk_sumcases' rtr ts'
+          in
+            (mk_sumcase LT RT T lcase rcase, ts'')
+          end
+        | mk_sumcases' _ [] = sys_error "mk_sumcases"
in
-	fst (mk_sumcases' tree ts)
+      fst (mk_sumcases' tree ts)
end
-
+
end

```
```--- a/src/HOL/Tools/function_package/termination.ML	Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/termination.ML	Tue Nov 07 22:06:32 2006 +0100
@@ -9,8 +9,8 @@

signature FUNDEF_TERMINATION =
sig
-    val mk_total_termination_goal : FundefCommon.result_with_names -> term
-    val mk_partial_termination_goal : theory -> FundefCommon.result_with_names -> string -> term * term
+  val mk_total_termination_goal : FundefCommon.result_with_names -> term
+  val mk_partial_termination_goal : theory -> FundefCommon.result_with_names -> string -> term * term
end

structure FundefTermination : FUNDEF_TERMINATION =
@@ -20,41 +20,40 @@
open FundefLib
open FundefCommon
open FundefAbbrev
-
+
fun mk_total_termination_goal (FundefMResult {R, f, ... }, _, _) =
let
-	val domT = domain_type (fastype_of f)
-	val x = Free ("x", domT)
+      val domT = domain_type (fastype_of f)
+      val x = Free ("x", domT)
in
mk_forall x (Trueprop (mk_acc domT R \$ x))
end
-
+
fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _) dom =
let
-	val domT = domain_type (fastype_of f)
-	val D = Sign.simple_read_term thy (Logic.varifyT (HOLogic.mk_setT domT)) dom
-	val DT = type_of D
-	val idomT = HOLogic.dest_setT DT
-
-	val x = Free ("x", idomT)
-	val z = Free ("z", idomT)
-	val Rname = fst (dest_Const R)
-	val iRT = mk_relT (idomT, idomT)
-	val iR = Const (Rname, iRT)
-
+      val domT = domain_type (fastype_of f)
+      val D = Sign.simple_read_term thy (Logic.varifyT (HOLogic.mk_setT domT)) dom
+      val DT = type_of D
+      val idomT = HOLogic.dest_setT DT
+
+      val x = Free ("x", idomT)
+      val z = Free ("z", idomT)
+      val Rname = fst (dest_Const R)
+      val iRT = mk_relT (idomT, idomT)
+      val iR = Const (Rname, iRT)
+
+      val subs = HOLogic.mk_Trueprop
+                   (Const ("Orderings.less_eq", DT --> DT --> boolT) \$ D \$
+                          (Const (acc_const_name, iRT --> DT) \$ iR))
+                   |> Type.freeze

-	val subs = HOLogic.mk_Trueprop
-			 (Const ("Orderings.less_eq", DT --> DT --> boolT) \$ D \$
-				(Const (acc_const_name, iRT --> DT) \$ iR))
-			 |> Type.freeze
-
-	val dcl = mk_forall x
-			    (mk_forall z (Logic.mk_implies (Trueprop (HOLogic.mk_mem (x, D)),
-							    Logic.mk_implies (mk_relmem (z, x) iR,
-									      Trueprop (mk_mem (z, D))))))
-			    |> Type.freeze
+      val dcl = mk_forall x
+                (mk_forall z (Logic.mk_implies (Trueprop (HOLogic.mk_mem (x, D)),
+                                                Logic.mk_implies (mk_relmem (z, x) iR,
+                                                                  Trueprop (mk_mem (z, D))))))
+                |> Type.freeze
in
-	(subs, dcl)
+      (subs, dcl)
end

end```