# HG changeset patch
# User blanchet
# Date 1286379861 -7200
# Node ID 626b1d360d426b9e4b201ddee175406912062b12
# Parent  a62e01e9b22c50b31f3a099fc601bc68a76d651f# Parent  d42ddd7407ca4efd0bff1b3e378ae34983fb9f75
merged

diff -r d42ddd7407ca -r 626b1d360d42 NEWS
--- a/NEWS	Wed Oct 06 17:44:07 2010 +0200
+++ b/NEWS	Wed Oct 06 17:44:21 2010 +0200
@@ -74,6 +74,10 @@
 
 *** HOL ***
 
+* Predicates `distinct` and `sorted` now defined inductively, with nice
+induction rules.  INCOMPATIBILITY: former distinct.simps and sorted.simps
+now named distinct_simps and sorted_simps.
+
 * Constant `contents` renamed to `the_elem`, to free the generic name
 contents for other uses.  INCOMPATIBILITY.
 
diff -r d42ddd7407ca -r 626b1d360d42 src/HOL/Library/AssocList.thy
--- a/src/HOL/Library/AssocList.thy	Wed Oct 06 17:44:07 2010 +0200
+++ b/src/HOL/Library/AssocList.thy	Wed Oct 06 17:44:21 2010 +0200
@@ -96,7 +96,7 @@
 proof -
   have "map_of \<circ> More_List.fold (prod_case update) (zip ks vs) =
     More_List.fold (\<lambda>(k, v) f. f(k \<mapsto> v)) (zip ks vs) \<circ> map_of"
-    by (rule fold_apply) (auto simp add: fun_eq_iff update_conv')
+    by (rule fold_commute) (auto simp add: fun_eq_iff update_conv')
   then show ?thesis by (auto simp add: updates_def fun_eq_iff map_upds_fold_map_upd foldl_fold split_def)
 qed
 
@@ -113,7 +113,7 @@
     by (rule fold_invariant [of "zip ks vs" "\<lambda>_. True"]) (auto intro: assms)
   moreover have "map fst \<circ> More_List.fold (prod_case update) (zip ks vs) =
     More_List.fold (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k]) (zip ks vs) \<circ> map fst"
-    by (rule fold_apply) (simp add: update_keys split_def prod_case_beta comp_def)
+    by (rule fold_commute) (simp add: update_keys split_def prod_case_beta comp_def)
   ultimately show ?thesis by (simp add: updates_def fun_eq_iff)
 qed
 
@@ -341,7 +341,7 @@
 proof -
   have "clearjunk \<circ> More_List.fold (prod_case update) (zip ks vs) =
     More_List.fold (prod_case update) (zip ks vs) \<circ> clearjunk"
-    by (rule fold_apply) (simp add: clearjunk_update prod_case_beta o_def)
+    by (rule fold_commute) (simp add: clearjunk_update prod_case_beta o_def)
   then show ?thesis by (simp add: updates_def fun_eq_iff)
 qed
 
@@ -446,7 +446,7 @@
 proof -
   have "map_of \<circ> More_List.fold (prod_case update) (rev ys) =
     More_List.fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> map_of"
-    by (rule fold_apply) (simp add: update_conv' prod_case_beta split_def fun_eq_iff)
+    by (rule fold_commute) (simp add: update_conv' prod_case_beta split_def fun_eq_iff)
   then show ?thesis
     by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev fun_eq_iff)
 qed
diff -r d42ddd7407ca -r 626b1d360d42 src/HOL/Library/Dlist.thy
--- a/src/HOL/Library/Dlist.thy	Wed Oct 06 17:44:07 2010 +0200
+++ b/src/HOL/Library/Dlist.thy	Wed Oct 06 17:44:21 2010 +0200
@@ -140,7 +140,7 @@
   case (Abs_dlist xs)
   then have "distinct xs" and dxs: "dxs = Dlist xs" by (simp_all add: Dlist_def distinct_remdups_id)
   from `distinct xs` have "P (Dlist xs)"
-  proof (induct xs rule: distinct_induct)
+  proof (induct xs)
     case Nil from empty show ?case by (simp add: empty_def)
   next
     case (insert x xs)
diff -r d42ddd7407ca -r 626b1d360d42 src/HOL/Library/Fset.thy
--- a/src/HOL/Library/Fset.thy	Wed Oct 06 17:44:07 2010 +0200
+++ b/src/HOL/Library/Fset.thy	Wed Oct 06 17:44:21 2010 +0200
@@ -1,7 +1,7 @@
 
 (* Author: Florian Haftmann, TU Muenchen *)
 
-header {* Executable finite sets *}
+header {* A set type which is executable on its finite part *}
 
 theory Fset
 imports More_Set More_List
@@ -257,7 +257,7 @@
     by (simp add: fun_eq_iff)
   have "member \<circ> fold (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member) xs =
     fold More_Set.remove xs \<circ> member"
-    by (rule fold_apply) (simp add: fun_eq_iff)
+    by (rule fold_commute) (simp add: fun_eq_iff)
   then have "fold More_Set.remove xs (member A) = 
     member (fold (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member) xs A)"
     by (simp add: fun_eq_iff)
@@ -282,7 +282,7 @@
     by (simp add: fun_eq_iff)
   have "member \<circ> fold (\<lambda>x. Fset \<circ> Set.insert x \<circ> member) xs =
     fold Set.insert xs \<circ> member"
-    by (rule fold_apply) (simp add: fun_eq_iff)
+    by (rule fold_commute) (simp add: fun_eq_iff)
   then have "fold Set.insert xs (member A) =
     member (fold (\<lambda>x. Fset \<circ> Set.insert x \<circ> member) xs A)"
     by (simp add: fun_eq_iff)
diff -r d42ddd7407ca -r 626b1d360d42 src/HOL/Library/More_List.thy
--- a/src/HOL/Library/More_List.thy	Wed Oct 06 17:44:07 2010 +0200
+++ b/src/HOL/Library/More_List.thy	Wed Oct 06 17:44:21 2010 +0200
@@ -45,11 +45,19 @@
   shows "fold f xs = id"
   using assms by (induct xs) simp_all
 
-lemma fold_apply:
+lemma fold_commute:
   assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
   shows "h \<circ> fold g xs = fold f xs \<circ> h"
   using assms by (induct xs) (simp_all add: fun_eq_iff)
 
+lemma fold_commute_apply:
+  assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
+  shows "h (fold g xs s) = fold f xs (h s)"
+proof -
+  from assms have "h \<circ> fold g xs = fold f xs \<circ> h" by (rule fold_commute)
+  then show ?thesis by (simp add: fun_eq_iff)
+qed
+
 lemma fold_invariant: 
   assumes "\<And>x. x \<in> set xs \<Longrightarrow> Q x" and "P s"
     and "\<And>x s. Q x \<Longrightarrow> P s \<Longrightarrow> P (f x s)"
@@ -73,7 +81,7 @@
 lemma fold_rev:
   assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
   shows "fold f (rev xs) = fold f xs"
-  using assms by (induct xs) (simp_all del: o_apply add: fold_apply)
+  using assms by (induct xs) (simp_all del: o_apply add: fold_commute)
 
 lemma foldr_fold:
   assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
diff -r d42ddd7407ca -r 626b1d360d42 src/HOL/Library/Permutation.thy
--- a/src/HOL/Library/Permutation.thy	Wed Oct 06 17:44:07 2010 +0200
+++ b/src/HOL/Library/Permutation.thy	Wed Oct 06 17:44:21 2010 +0200
@@ -168,7 +168,7 @@
     apply simp
     apply (subgoal_tac "a#list <~~> a#ysa@zs")
      apply (metis Cons_eq_appendI perm_append_Cons trans)
-    apply (metis Cons Cons_eq_appendI distinct.simps(2)
+    apply (metis Cons Cons_eq_appendI distinct_simps(2)
       distinct_remdups distinct_remdups_id perm_append_swap perm_distinct_iff)
    apply (subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)")
     apply (fastsimp simp add: insert_ident)
diff -r d42ddd7407ca -r 626b1d360d42 src/HOL/Library/positivstellensatz.ML
--- a/src/HOL/Library/positivstellensatz.ML	Wed Oct 06 17:44:07 2010 +0200
+++ b/src/HOL/Library/positivstellensatz.ML	Wed Oct 06 17:44:21 2010 +0200
@@ -270,7 +270,7 @@
   by (atomize (full)) (cases "x <= y", auto simp add: min_def)};
 
 
-         (* Miscalineous *)
+         (* Miscellaneous *)
 fun literals_conv bops uops cv = 
  let fun h t =
   case (term_of t) of 
diff -r d42ddd7407ca -r 626b1d360d42 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Oct 06 17:44:07 2010 +0200
+++ b/src/HOL/List.thy	Wed Oct 06 17:44:21 2010 +0200
@@ -157,16 +157,6 @@
     upt_0: "[i..<0] = []"
   | upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])"
 
-primrec
-  distinct :: "'a list \<Rightarrow> bool" where
-    "distinct [] \<longleftrightarrow> True"
-  | "distinct (x # xs) \<longleftrightarrow> x \<notin> set xs \<and> distinct xs"
-
-primrec
-  remdups :: "'a list \<Rightarrow> 'a list" where
-    "remdups [] = []"
-  | "remdups (x # xs) = (if x \<in> set xs then remdups xs else x # remdups xs)"
-
 definition
   insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   "insert x xs = (if x \<in> set xs then xs else x # xs)"
@@ -184,6 +174,21 @@
     "removeAll x [] = []"
   | "removeAll x (y # xs) = (if x = y then removeAll x xs else y # removeAll x xs)"
 
+inductive
+  distinct :: "'a list \<Rightarrow> bool" where
+    Nil: "distinct []"
+  | insert: "x \<notin> set xs \<Longrightarrow> distinct xs \<Longrightarrow> distinct (x # xs)"
+
+lemma distinct_simps [simp, code]:
+  "distinct [] \<longleftrightarrow> True"
+  "distinct (x # xs) \<longleftrightarrow> x \<notin> set xs \<and> distinct xs"
+  by (auto intro: distinct.intros elim: distinct.cases)
+
+primrec
+  remdups :: "'a list \<Rightarrow> 'a list" where
+    "remdups [] = []"
+  | "remdups (x # xs) = (if x \<in> set xs then remdups xs else x # remdups xs)"
+
 primrec
   replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
     replicate_0: "replicate 0 x = []"
@@ -275,10 +280,26 @@
 context linorder
 begin
 
-fun sorted :: "'a list \<Rightarrow> bool" where
-"sorted [] \<longleftrightarrow> True" |
-"sorted [x] \<longleftrightarrow> True" |
-"sorted (x#y#zs) \<longleftrightarrow> x <= y \<and> sorted (y#zs)"
+inductive sorted :: "'a list \<Rightarrow> bool" where
+  Nil [iff]: "sorted []"
+| Cons: "\<forall>y\<in>set xs. x \<le> y \<Longrightarrow> sorted xs \<Longrightarrow> sorted (x # xs)"
+
+lemma sorted_single [iff]:
+  "sorted [x]"
+  by (rule sorted.Cons) auto
+
+lemma sorted_many:
+  "x \<le> y \<Longrightarrow> sorted (y # zs) \<Longrightarrow> sorted (x # y # zs)"
+  by (rule sorted.Cons) (cases "y # zs" rule: sorted.cases, auto)
+
+lemma sorted_many_eq [simp, code]:
+  "sorted (x # y # zs) \<longleftrightarrow> x \<le> y \<and> sorted (y # zs)"
+  by (auto intro: sorted_many elim: sorted.cases)
+
+lemma [code]:
+  "sorted [] \<longleftrightarrow> True"
+  "sorted [x] \<longleftrightarrow> True"
+  by simp_all
 
 primrec insort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
 "insort_key f x [] = [x]" |
@@ -2118,36 +2139,6 @@
   "length xs = length ys \<Longrightarrow> zip xs ys = zs \<longleftrightarrow> map fst zs = xs \<and> map snd zs = ys"
   by (auto simp add: zip_map_fst_snd)
 
-lemma distinct_zipI1:
-  "distinct xs \<Longrightarrow> distinct (zip xs ys)"
-proof (induct xs arbitrary: ys)
-  case (Cons x xs)
-  show ?case
-  proof (cases ys)
-    case (Cons y ys')
-    have "(x, y) \<notin> set (zip xs ys')"
-      using Cons.prems by (auto simp: set_zip)
-    thus ?thesis
-      unfolding Cons zip_Cons_Cons distinct.simps
-      using Cons.hyps Cons.prems by simp
-  qed simp
-qed simp
-
-lemma distinct_zipI2:
-  "distinct xs \<Longrightarrow> distinct (zip xs ys)"
-proof (induct xs arbitrary: ys)
-  case (Cons x xs)
-  show ?case
-  proof (cases ys)
-    case (Cons y ys')
-     have "(x, y) \<notin> set (zip xs ys')"
-      using Cons.prems by (auto simp: set_zip)
-    thus ?thesis
-      unfolding Cons zip_Cons_Cons distinct.simps
-      using Cons.hyps Cons.prems by simp
-  qed simp
-qed simp
-
 
 subsubsection {* @{text list_all2} *}
 
@@ -2868,6 +2859,30 @@
   "remdups (map f (remdups xs)) = remdups (map f xs)"
   by (induct xs) simp_all
 
+lemma distinct_zipI1:
+  assumes "distinct xs"
+  shows "distinct (zip xs ys)"
+proof (rule zip_obtain_same_length)
+  fix xs' :: "'a list" and ys' :: "'b list" and n
+  assume "length xs' = length ys'"
+  assume "xs' = take n xs"
+  with assms have "distinct xs'" by simp
+  with `length xs' = length ys'` show "distinct (zip xs' ys')"
+    by (induct xs' ys' rule: list_induct2) (auto elim: in_set_zipE)
+qed
+
+lemma distinct_zipI2:
+  assumes "distinct ys"
+  shows "distinct (zip xs ys)"
+proof (rule zip_obtain_same_length)
+  fix xs' :: "'b list" and ys' :: "'a list" and n
+  assume "length xs' = length ys'"
+  assume "ys' = take n ys"
+  with assms have "distinct ys'" by simp
+  with `length xs' = length ys'` show "distinct (zip xs' ys')"
+    by (induct xs' ys' rule: list_induct2) (auto elim: in_set_zipE)
+qed
+
 
 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
 
@@ -3023,21 +3038,6 @@
   "List.insert x (remdups xs) = remdups (List.insert x xs)"
   by (simp add: List.insert_def)
 
-lemma distinct_induct [consumes 1, case_names Nil insert]:
-  assumes "distinct xs"
-  assumes "P []"
-  assumes insert: "\<And>x xs. distinct xs \<Longrightarrow> x \<notin> set xs
-    \<Longrightarrow> P xs \<Longrightarrow> P (List.insert x xs)"
-  shows "P xs"
-using `distinct xs` proof (induct xs)
-  case Nil from `P []` show ?case .
-next
-  case (Cons x xs)
-  then have "distinct xs" and "x \<notin> set xs" and "P xs" by simp_all
-  with insert have "P (List.insert x xs)" .
-  with `x \<notin> set xs` show ?case by simp
-qed
-
 
 subsubsection {* @{text remove1} *}
 
@@ -3822,39 +3822,21 @@
 apply (auto simp: sorted_distinct_set_unique)
 done
 
-lemma sorted_take:
-  "sorted xs \<Longrightarrow> sorted (take n xs)"
-proof (induct xs arbitrary: n rule: sorted.induct)
-  case 1 show ?case by simp
-next
-  case 2 show ?case by (cases n) simp_all
-next
-  case (3 x y xs)
-  then have "x \<le> y" by simp
-  show ?case proof (cases n)
-    case 0 then show ?thesis by simp
-  next
-    case (Suc m) 
-    with 3 have "sorted (take m (y # xs))" by simp
-    with Suc  `x \<le> y` show ?thesis by (cases m) simp_all
-  qed
-qed
-
-lemma sorted_drop:
-  "sorted xs \<Longrightarrow> sorted (drop n xs)"
-proof (induct xs arbitrary: n rule: sorted.induct)
-  case 1 show ?case by simp
-next
-  case 2 show ?case by (cases n) simp_all
-next
-  case 3 then show ?case by (cases n) simp_all
+lemma
+  assumes "sorted xs"
+  shows sorted_take: "sorted (take n xs)"
+  and sorted_drop: "sorted (drop n xs)"
+proof -
+  from assms have "sorted (take n xs @ drop n xs)" by simp
+  then show "sorted (take n xs)" and "sorted (drop n xs)"
+    unfolding sorted_append by simp_all
 qed
 
 lemma sorted_dropWhile: "sorted xs \<Longrightarrow> sorted (dropWhile P xs)"
-  unfolding dropWhile_eq_drop by (rule sorted_drop)
+  by (auto dest: sorted_drop simp add: dropWhile_eq_drop)
 
 lemma sorted_takeWhile: "sorted xs \<Longrightarrow> sorted (takeWhile P xs)"
-  apply (subst takeWhile_eq_take) by (rule sorted_take)
+  by (subst takeWhile_eq_take) (auto dest: sorted_take)
 
 lemma sorted_filter:
   "sorted (map f xs) \<Longrightarrow> sorted (map f (filter P xs))"
@@ -4153,7 +4135,6 @@
   by (rule sorted_distinct_set_unique) simp_all
 
 
-
 subsubsection {* @{text lists}: the list-forming operator over sets *}
 
 inductive_set
diff -r d42ddd7407ca -r 626b1d360d42 src/HOL/MicroJava/Comp/AuxLemmas.thy
--- a/src/HOL/MicroJava/Comp/AuxLemmas.thy	Wed Oct 06 17:44:07 2010 +0200
+++ b/src/HOL/MicroJava/Comp/AuxLemmas.thy	Wed Oct 06 17:44:21 2010 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/MicroJava/Comp/AuxLemmas.thy
-    ID:         $Id$
     Author:     Martin Strecker
 *)
 
@@ -78,30 +77,24 @@
   "y \<notin> set xs \<Longrightarrow> map (the \<circ> f(y\<mapsto>v)) xs = map (the \<circ> f) xs"
 by (simp add: the_map_upd)
 
-lemma map_map_upds [rule_format (no_asm), simp]: 
-"\<forall> f vs. (\<forall>y\<in>set ys. y \<notin> set xs) \<longrightarrow> map (the \<circ> f(ys[\<mapsto>]vs)) xs = map (the \<circ> f) xs"
-apply (induct xs)
+lemma map_map_upds [simp]: 
+  "(\<forall>y\<in>set ys. y \<notin> set xs) \<Longrightarrow> map (the \<circ> f(ys[\<mapsto>]vs)) xs = map (the \<circ> f) xs"
+apply (induct xs arbitrary: f vs)
  apply simp
 apply fastsimp
 done
 
-lemma map_upds_distinct [rule_format (no_asm), simp]: 
-  "\<forall> f vs. length ys = length vs \<longrightarrow> distinct ys \<longrightarrow> map (the \<circ> f(ys[\<mapsto>]vs)) ys = vs"
-apply (induct ys)
+lemma map_upds_distinct [simp]: 
+  "distinct ys \<Longrightarrow> length ys = length vs \<Longrightarrow> map (the \<circ> f(ys[\<mapsto>]vs)) ys = vs"
+apply (induct ys arbitrary: f vs rule: distinct.induct)
 apply simp
-apply (intro strip)
 apply (case_tac vs)
-apply simp
-apply (simp only: map_upds_Cons distinct.simps hd.simps tl.simps map.simps)
-apply clarify
-apply (simp del: o_apply)
-apply simp
+apply simp_all
 done
 
-
-lemma map_of_map_as_map_upd [rule_format (no_asm)]: "distinct (map f zs) \<longrightarrow> 
-map_of (map (\<lambda> p. (f p, g p)) zs) = empty (map f zs [\<mapsto>] map g zs)"
-by (induct zs, auto)
+lemma map_of_map_as_map_upd:
+  "distinct (map f zs) \<Longrightarrow> map_of (map (\<lambda> p. (f p, g p)) zs) = empty (map f zs [\<mapsto>] map g zs)"
+  by (induct zs) auto
 
 (* In analogy to Map.map_of_SomeD *)
 lemma map_upds_SomeD [rule_format (no_asm)]: 
diff -r d42ddd7407ca -r 626b1d360d42 src/HOL/MicroJava/MicroJava.thy
--- a/src/HOL/MicroJava/MicroJava.thy	Wed Oct 06 17:44:07 2010 +0200
+++ b/src/HOL/MicroJava/MicroJava.thy	Wed Oct 06 17:44:21 2010 +0200
@@ -12,4 +12,4 @@
   "Comp/CorrCompTp"
 begin
 
-end
\ No newline at end of file
+end
diff -r d42ddd7407ca -r 626b1d360d42 src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Wed Oct 06 17:44:07 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Wed Oct 06 17:44:21 2010 +0200
@@ -4,7 +4,7 @@
 
 section {* Specialisation Examples *}
 
-fun nth_el'
+primrec nth_el'
 where
   "nth_el' [] i = None"
 | "nth_el' (x # xs) i = (case i of 0 => Some x | Suc j => nth_el' xs j)"
@@ -48,7 +48,27 @@
 
 subsection {* Sorts *}
 
-code_pred [inductify] sorted .
+declare sorted.Nil [code_pred_intro]
+  sorted_single [code_pred_intro]
+  sorted_many [code_pred_intro]
+
+code_pred sorted proof -
+  assume "sorted xa"
+  assume 1: "xa = [] \<Longrightarrow> thesis"
+  assume 2: "\<And>x. xa = [x] \<Longrightarrow> thesis"
+  assume 3: "\<And>x y zs. xa = x # y # zs \<Longrightarrow> x \<le> y \<Longrightarrow> sorted (y # zs) \<Longrightarrow> thesis"
+  show thesis proof (cases xa)
+    case Nil with 1 show ?thesis .
+  next
+    case (Cons x xs) show ?thesis proof (cases xs)
+      case Nil with Cons 2 show ?thesis by simp
+    next
+      case (Cons y zs) with `xa = x # xs` have "xa = x # y # zs" by simp
+      moreover with `sorted xa` have "x \<le> y" and "sorted (y # zs)" by simp_all
+      ultimately show ?thesis by (rule 3)
+    qed
+  qed
+qed
 thm sorted.equation
 
 section {* Specialisation in POPLmark theory *}
@@ -212,10 +232,10 @@
 where
   T_Var: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> \<Longrightarrow> \<Gamma>\<langle>i\<rangle> = \<lfloor>VarB U\<rfloor> \<Longrightarrow> T = \<up>\<^isub>\<tau> (Suc i) 0 U \<Longrightarrow> \<Gamma> \<turnstile> Var i : T"
 | T_Abs: "VarB T\<^isub>1 \<Colon> \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2 \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda>:T\<^isub>1. t\<^isub>2) : T\<^isub>1 \<rightarrow> \<down>\<^isub>\<tau> 1 0 T\<^isub>2"
-| T_App: "\<Gamma> \<turnstile> t\<^isub>1 : T\<^isub>1\<^isub>1 \<rightarrow> T\<^isub>1\<^isub>2 \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>1\<^isub>1 \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>1 \<bullet> t\<^isub>2 : T\<^isub>1\<^isub>2"
+| T_App: "\<Gamma> \<turnstile> t\<^isub>1 : T\<^isub>11 \<rightarrow> T\<^isub>12 \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>11 \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>1 \<bullet> t\<^isub>2 : T\<^isub>12"
 | T_TAbs: "TVarB T\<^isub>1 \<Colon> \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2 \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda><:T\<^isub>1. t\<^isub>2) : (\<forall><:T\<^isub>1. T\<^isub>2)"
-| T_TApp: "\<Gamma> \<turnstile> t\<^isub>1 : (\<forall><:T\<^isub>1\<^isub>1. T\<^isub>1\<^isub>2) \<Longrightarrow> \<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>1\<^isub>1 \<Longrightarrow>
-    \<Gamma> \<turnstile> t\<^isub>1 \<bullet>\<^isub>\<tau> T\<^isub>2 : T\<^isub>1\<^isub>2[0 \<mapsto>\<^isub>\<tau> T\<^isub>2]\<^isub>\<tau>"
+| T_TApp: "\<Gamma> \<turnstile> t\<^isub>1 : (\<forall><:T\<^isub>11. T\<^isub>12) \<Longrightarrow> \<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>11 \<Longrightarrow>
+    \<Gamma> \<turnstile> t\<^isub>1 \<bullet>\<^isub>\<tau> T\<^isub>2 : T\<^isub>12[0 \<mapsto>\<^isub>\<tau> T\<^isub>2]\<^isub>\<tau>"
 | T_Sub: "\<Gamma> \<turnstile> t : S \<Longrightarrow> \<Gamma> \<turnstile> S <: T \<Longrightarrow> \<Gamma> \<turnstile> t : T"
 
 code_pred [inductify, skip_proof, specialise] typing .
diff -r d42ddd7407ca -r 626b1d360d42 src/HOL/Tools/Function/lexicographic_order.ML
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Wed Oct 06 17:44:07 2010 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Wed Oct 06 17:44:21 2010 +0200
@@ -1,7 +1,8 @@
 (*  Title:       HOL/Tools/Function/lexicographic_order.ML
     Author:      Lukas Bulwahn, TU Muenchen
+    Author:      Alexander Krauss, TU Muenchen
 
-Method for termination proofs with lexicographic orderings.
+Termination proofs with lexicographic orders.
 *)
 
 signature LEXICOGRAPHIC_ORDER =
@@ -41,23 +42,15 @@
 (** Matrix cell datatype **)
 
 datatype cell =
-  Less of thm| LessEq of (thm * thm) | None of (thm * thm) | False of thm;
-
-fun is_Less (Less _) = true
-  | is_Less _ = false
+  Less of thm | LessEq of (thm * thm) | None of (thm * thm) | False of thm;
 
-fun is_LessEq (LessEq _) = true
-  | is_LessEq _ = false
-
-fun pr_cell (Less _ ) = " < "
-  | pr_cell (LessEq _) = " <="
-  | pr_cell (None _) = " ? "
-  | pr_cell (False _) = " F "
+fun is_Less lcell = case Lazy.force lcell of Less _ => true | _ => false;
+fun is_LessEq lcell = case Lazy.force lcell of LessEq _ => true | _ => false;
 
 
 (** Proof attempts to build the matrix **)
 
-fun dest_term (t : term) =
+fun dest_term t =
   let
     val (vars, prop) = Function_Lib.dest_all_all t
     val (prems, concl) = Logic.strip_horn prop
@@ -76,7 +69,7 @@
     fold_rev Logic.all vars (Logic.list_implies (prems, concl))
   end
 
-fun mk_cell (thy : theory) solve_tac (vars, prems, lhs, rhs) mfun =
+fun mk_cell thy solve_tac (vars, prems, lhs, rhs) mfun = Lazy.lazy (fn _ =>
   let
     val goals = cterm_of thy o mk_goal (vars, prems, mfun $ lhs, mfun $ rhs)
   in
@@ -90,46 +83,42 @@
          else None (thm2, thm)
        | _ => raise Match) (* FIXME *)
     | _ => raise Match
-  end
+  end);
 
 
 (** Search algorithms **)
 
-fun check_col ls = forall (fn c => is_Less c orelse is_LessEq c) ls andalso not (forall (is_LessEq) ls)
+fun check_col ls = forall (fn c => is_Less c orelse is_LessEq c) ls andalso not (forall is_LessEq ls)
 
 fun transform_table table col = table |> filter_out (fn x => is_Less (nth x col)) |> map (del_index col)
 
 fun transform_order col order = map (fn x => if x >= col then x + 1 else x) order
 
 (* simple depth-first search algorithm for the table *)
-fun search_table table =
-  case table of
-    [] => SOME []
-  | _ =>
-    let
-      val col = find_index (check_col) (transpose table)
-    in case col of
-         ~1 => NONE
-       | _ =>
-         let
-           val order_opt = (table, col) |-> transform_table |> search_table
-         in case order_opt of
-              NONE => NONE
-            | SOME order =>SOME (col :: transform_order col order)
-         end
-    end
+fun search_table [] = SOME []
+  | search_table table =
+    case find_index check_col (transpose table) of
+       ~1 => NONE
+     | col =>
+         (case (table, col) |-> transform_table |> search_table of
+            NONE => NONE
+          | SOME order => SOME (col :: transform_order col order))
+
 
 (** Proof Reconstruction **)
 
 (* prove row :: cell list -> tactic *)
-fun prove_row (Less less_thm :: _) =
-    (rtac @{thm "mlex_less"} 1)
-    THEN PRIMITIVE (Thm.elim_implies less_thm)
-  | prove_row (LessEq (lesseq_thm, _) :: tail) =
-    (rtac @{thm "mlex_leq"} 1)
-    THEN PRIMITIVE (Thm.elim_implies lesseq_thm)
-    THEN prove_row tail
-  | prove_row _ = sys_error "lexicographic_order"
+fun prove_row (c :: cs) =
+  (case Lazy.force c of
+     Less thm =>
+       rtac @{thm "mlex_less"} 1
+       THEN PRIMITIVE (Thm.elim_implies thm)
+   | LessEq (thm, _) =>
+       rtac @{thm "mlex_leq"} 1
+       THEN PRIMITIVE (Thm.elim_implies thm)
+       THEN prove_row cs
+   | _ => sys_error "lexicographic_order")
+ | prove_row [] = no_tac;
 
 
 (** Error reporting **)
@@ -158,8 +147,14 @@
   |> flat
   |> map (pr_unprovable_cell ctxt)
 
-fun no_order_msg ctxt table tl measure_funs =
+fun pr_cell (Less _ ) = " < "
+  | pr_cell (LessEq _) = " <="
+  | pr_cell (None _) = " ? "
+  | pr_cell (False _) = " F "
+
+fun no_order_msg ctxt ltable tl measure_funs =
   let
+    val table = map (map Lazy.force) ltable
     val prterm = Syntax.string_of_term ctxt
     fun pr_fun t i = string_of_int i ^ ") " ^ prterm t
 
@@ -195,7 +190,7 @@
       MeasureFunctions.get_measure_functions ctxt domT
 
     val table = (* 2: create table *)
-      Par_List.map (fn t => Par_List.map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl
+      map (fn t => map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl
   in
     case search_table table of
       NONE => if quiet then no_tac st else error (no_order_msg ctxt table tl measure_funs)
diff -r d42ddd7407ca -r 626b1d360d42 src/HOL/Tools/Function/scnp_reconstruct.ML
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Wed Oct 06 17:44:07 2010 +0200
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Wed Oct 06 17:44:21 2010 +0200
@@ -298,52 +298,7 @@
     end
 
 
-
-local open Termination in
-fun print_cell (SOME (Less _)) = "<"
-  | print_cell (SOME (LessEq _)) = "\<le>"
-  | print_cell (SOME (None _)) = "-"
-  | print_cell (SOME (False _)) = "-"
-  | print_cell (NONE) = "?"
-
-fun print_error ctxt D = CALLS (fn (cs, _) =>
-  let
-    val np = get_num_points D
-    val ms = map_range (get_measures D) np
-    fun index xs = (1 upto length xs) ~~ xs
-    fun outp s t f xs = map (fn (x, y) => s ^ Int.toString x ^ t ^ f y ^ "\n") xs
-    val ims = index (map index ms)
-    val _ = tracing (implode (outp "fn #" ":\n" (implode o outp "\tmeasure #" ": " (Syntax.string_of_term ctxt)) ims))
-    fun print_call (k, c) =
-      let
-        val (_, p, _, q, _, _) = dest_call D c
-        val _ = tracing ("call table for call #" ^ Int.toString k ^ ": fn " ^ 
-                                Int.toString (p + 1) ^ " ~> fn " ^ Int.toString (q + 1))
-        val caller_ms = nth ms p
-        val callee_ms = nth ms q
-        val entries = map (fn x => map (pair x) (callee_ms)) (caller_ms)
-        fun print_ln (i : int, l) = implode (Int.toString i :: "   " :: map (enclose " " " " o print_cell o (uncurry (get_descent D c))) l)
-        val _ = tracing (implode (Int.toString (p + 1) ^ "|" ^ Int.toString (q + 1) ^ 
-                                        " " :: map (enclose " " " " o Int.toString) (1 upto length callee_ms)) ^ "\n" 
-                                ^ cat_lines (map print_ln ((1 upto (length entries)) ~~ entries)))
-      in
-        true
-      end
-    fun list_call (k, c) =
-      let
-        val (_, p, _, q, _, _) = dest_call D c
-        val _ = tracing ("call #" ^ (Int.toString k) ^ ": fn " ^
-                                Int.toString (p + 1) ^ " ~> fn " ^ Int.toString (q + 1) ^ "\n" ^ 
-                                (Syntax.string_of_term ctxt c))
-      in true end
-    val _ = forall list_call ((1 upto length cs) ~~ cs)
-    val _ = forall print_call ((1 upto length cs) ~~ cs)
-  in
-    all_tac
-  end)
-end
-
-fun single_scnp_tac use_tags orders ctxt cont err_cont D = Termination.CALLS (fn (cs, i) =>
+fun single_scnp_tac use_tags orders ctxt D = Termination.CALLS (fn (cs, i) =>
   let
     val ms_configured = is_some (Multiset_Setup.get (ProofContext.theory_of ctxt))
     val orders' = if ms_configured then orders
@@ -352,56 +307,40 @@
     val certificate = generate_certificate use_tags orders' gp
   in
     case certificate
-     of NONE => err_cont D i
+     of NONE => no_tac
       | SOME cert =>
           SELECT_GOAL (reconstruct_tac ctxt D cs gp cert) i
-          THEN (rtac @{thm wf_empty} i ORELSE cont D i)
+          THEN TRY (rtac @{thm wf_empty} i)
   end)
 
-fun gen_decomp_scnp_tac orders autom_tac ctxt err_cont =
-  let
-    open Termination
-    val derive_diag = Termination.derive_diag ctxt autom_tac
-    val derive_all = Termination.derive_all ctxt autom_tac
-    val decompose = Termination.decompose_tac ctxt autom_tac
-    val scnp_no_tags = single_scnp_tac false orders ctxt
-    val scnp_full = single_scnp_tac true orders ctxt
-
-    fun first_round c e =
-        derive_diag (REPEAT scnp_no_tags c e)
-
-    val second_round =
-        REPEAT (fn c => fn e => decompose (scnp_no_tags c c) e)
+local open Termination in
 
-    val third_round =
-        derive_all oo
-        REPEAT (fn c => fn e =>
-          scnp_full (decompose c c) e)
-
-    fun Then s1 s2 c e = s1 (s2 c c) (s2 c e)
+fun gen_decomp_scnp_tac orders autom_tac ctxt =
+TERMINATION ctxt autom_tac (fn D => 
+  let
+    val decompose = decompose_tac D
+    val scnp_full = single_scnp_tac true orders ctxt D
+  in
+    REPEAT_ALL_NEW (scnp_full ORELSE' decompose)
+  end)
+end
 
-    val strategy = Then (Then first_round second_round) third_round
-
-  in
-    TERMINATION ctxt (strategy err_cont err_cont)
-  end
-
-fun gen_sizechange_tac orders autom_tac ctxt err_cont =
+fun gen_sizechange_tac orders autom_tac ctxt =
   TRY (Function_Common.apply_termination_rule ctxt 1)
   THEN TRY (Termination.wf_union_tac ctxt)
   THEN
    (rtac @{thm wf_empty} 1
-    ORELSE gen_decomp_scnp_tac orders autom_tac ctxt err_cont 1)
+    ORELSE gen_decomp_scnp_tac orders autom_tac ctxt 1)
 
 fun sizechange_tac ctxt autom_tac =
-  gen_sizechange_tac [MAX, MS, MIN] autom_tac ctxt (K (K all_tac))
+  gen_sizechange_tac [MAX, MS, MIN] autom_tac ctxt
 
 fun decomp_scnp_tac orders ctxt =
   let
     val extra_simps = Function_Common.Termination_Simps.get ctxt
     val autom_tac = auto_tac (clasimpset_of ctxt addsimps2 extra_simps)
   in
-     gen_sizechange_tac orders autom_tac ctxt (print_error ctxt)
+     gen_sizechange_tac orders autom_tac ctxt
   end
 
 
diff -r d42ddd7407ca -r 626b1d360d42 src/HOL/Tools/Function/termination.ML
--- a/src/HOL/Tools/Function/termination.ML	Wed Oct 06 17:44:07 2010 +0200
+++ b/src/HOL/Tools/Function/termination.ML	Wed Oct 06 17:44:21 2010 +0200
@@ -9,7 +9,7 @@
 sig
 
   type data
-  datatype cell = Less of thm | LessEq of (thm * thm) | None of (thm * thm) | False of thm
+  datatype cell = Less of thm | LessEq of thm * thm | None of thm * thm | False of thm
 
   val mk_sumcases : data -> typ -> term list -> term
 
@@ -17,7 +17,6 @@
   val get_types      : data -> int -> typ
   val get_measures   : data -> int -> term list
 
-  (* read from cache *)
   val get_chain      : data -> term -> term -> thm option option
   val get_descent    : data -> term -> term -> term -> cell option
 
@@ -25,23 +24,14 @@
 
   val CALLS : (term list * int -> tactic) -> int -> tactic
 
-  (* Termination tactics. Sequential composition via continuations. (2nd argument is the error continuation) *)
-  type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
+  (* Termination tactics *)
+  type ttac = data -> int -> tactic
 
-  val TERMINATION : Proof.context -> (data -> int -> tactic) -> int -> tactic
-
-  val REPEAT : ttac -> ttac
+  val TERMINATION : Proof.context -> tactic -> ttac -> int -> tactic
 
   val wf_union_tac : Proof.context -> tactic
 
-  val decompose_tac : Proof.context -> tactic -> ttac
-
-  val derive_diag : Proof.context -> tactic -> 
-    (data -> int -> tactic) -> data -> int -> tactic
-
-  val derive_all  : Proof.context -> tactic ->
-    (data -> int -> tactic) -> data -> int -> tactic
-
+  val decompose_tac : ttac
 end
 
 
@@ -119,22 +109,16 @@
 
 (** Matrix cell datatype **)
 
-datatype cell = Less of thm | LessEq of (thm * thm) | None of (thm * thm) | False of thm;
+datatype cell = Less of thm | LessEq of thm * thm | None of thm * thm | False of thm;
 
 
 type data =
   skel                            (* structure of the sum type encoding "program points" *)
   * (int -> typ)                  (* types of program points *)
   * (term list Inttab.table)      (* measures for program points *)
-  * (thm option Term2tab.table)   (* which calls form chains? *)
-  * (cell Term3tab.table)         (* local descents *)
-
+  * (term * term -> thm option)   (* which calls form chains? (cached) *)
+  * (term * (term * term) -> cell)(* local descents (cached) *)
 
-fun map_chains f (p, T, M, C, D) = (p, T, M, f C, D)
-fun map_descent f (p, T, M, C, D) = (p, T, M, C, f D)
-
-fun note_chain c1 c2 res = map_chains (Term2tab.update ((c1, c2), res))
-fun note_descent c m1 m2 res = map_descent (Term3tab.update ((c,(m1, m2)), res))
 
 (* Build case expression *)
 fun mk_sumcases (sk, _, _, _, _) T fs =
@@ -155,33 +139,21 @@
     mk_skel (fold collect_pats cs [])
   end
 
-fun create ctxt T rel =
+fun prove_chain thy chain_tac (c1, c2) =
   let
-    val sk = mk_sum_skel rel
-    val Ts = node_types sk T
-    val M = Inttab.make (map_index (apsnd (MeasureFunctions.get_measure_functions ctxt)) Ts)
+    val goal =
+      HOLogic.mk_eq (HOLogic.mk_binop @{const_name Relation.rel_comp} (c1, c2),
+        Const (@{const_abbrev Set.empty}, fastype_of c1))
+      |> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *)
   in
-    (sk, nth Ts, M, Term2tab.empty, Term3tab.empty)
+    case Function_Lib.try_proof (cterm_of thy goal) chain_tac of
+      Function_Lib.Solved thm => SOME thm
+    | _ => NONE
   end
 
-fun get_num_points (sk, _, _, _, _) =
+
+fun dest_call' sk (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
   let
-    fun num (SLeaf i) = i + 1
-      | num (SBranch (s, t)) = num t
-  in num sk end
-
-fun get_types (_, T, _, _, _) = T
-fun get_measures (_, _, M, _, _) = Inttab.lookup_list M
-
-fun get_chain (_, _, _, C, _) c1 c2 =
-  Term2tab.lookup C (c1, c2)
-
-fun get_descent (_, _, _, _, D) c m1 m2 =
-  Term3tab.lookup D (c, (m1, m2))
-
-fun dest_call D (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
-  let
-    val (sk, _, _, _, _) = D
     val vs = Term.strip_qnt_vars @{const_name Ex} c
 
     (* FIXME: throw error "dest_call" for malformed terms *)
@@ -192,8 +164,9 @@
   in
     (vs, p, l', q, r', Gam)
   end
-  | dest_call D t = error "dest_call"
+  | dest_call' _ _ = error "dest_call"
 
+fun dest_call (sk, _, _, _, _) = dest_call' sk
 
 fun mk_desc thy tac vs Gam l r m1 m2 =
   let
@@ -216,15 +189,41 @@
      | _ => raise Match
 end
 
-fun derive_descent thy tac c m1 m2 D =
-  case get_descent D c m1 m2 of
-    SOME _ => D
-  | NONE => 
-    let
-      val (vs, _, l, _, r, Gam) = dest_call D c
-    in 
-      note_descent c m1 m2 (mk_desc thy tac vs Gam l r m1 m2) D
-    end
+fun prove_descent thy tac sk (c, (m1, m2)) =
+  let
+    val (vs, _, l, _, r, Gam) = dest_call' sk c
+  in 
+    mk_desc thy tac vs Gam l r m1 m2
+  end
+
+fun create ctxt chain_tac descent_tac T rel =
+  let
+    val thy = ProofContext.theory_of ctxt
+    val sk = mk_sum_skel rel
+    val Ts = node_types sk T
+    val M = Inttab.make (map_index (apsnd (MeasureFunctions.get_measure_functions ctxt)) Ts)
+    val chain_cache = Cache.create Term2tab.empty Term2tab.lookup Term2tab.update
+      (prove_chain thy chain_tac)
+    val descent_cache = Cache.create Term3tab.empty Term3tab.lookup Term3tab.update
+      (prove_descent thy descent_tac sk)
+  in
+    (sk, nth Ts, M, chain_cache, descent_cache)
+  end
+
+fun get_num_points (sk, _, _, _, _) =
+  let
+    fun num (SLeaf i) = i + 1
+      | num (SBranch (s, t)) = num t
+  in num sk end
+
+fun get_types (_, T, _, _, _) = T
+fun get_measures (_, _, M, _, _) = Inttab.lookup_list M
+
+fun get_chain (_, _, _, C, _) c1 c2 =
+  SOME (C (c1, c2))
+
+fun get_descent (_, _, _, _, D) c m1 m2 =
+  SOME (D (c, (m1, m2)))
 
 fun CALLS tac i st =
   if Thm.no_prems st then all_tac st
@@ -232,14 +231,14 @@
     (_ $ (_ $ rel)) => tac (Function_Lib.dest_binop_list @{const_name Lattices.sup} rel, i) st
   |_ => no_tac st
 
-type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
+type ttac = data -> int -> tactic
 
-fun TERMINATION ctxt tac =
+fun TERMINATION ctxt atac tac =
   SUBGOAL (fn (_ $ (Const (@{const_name wf}, wfT) $ rel), i) =>
   let
     val (T, _) = HOLogic.dest_prodT (HOLogic.dest_setT (domain_type wfT))
   in
-    tac (create ctxt T rel) i
+    tac (create ctxt atac atac T rel) i
   end)
 
 
@@ -309,36 +308,9 @@
 end
 
 
-(* continuation passing repeat combinator *)
-fun REPEAT ttac cont err_cont =
-    ttac (fn D => fn i => (REPEAT ttac cont cont D i)) err_cont
 
 (*** DEPENDENCY GRAPHS ***)
 
-fun prove_chain thy chain_tac c1 c2 =
-  let
-    val goal =
-      HOLogic.mk_eq (HOLogic.mk_binop @{const_name Relation.rel_comp} (c1, c2),
-        Const (@{const_abbrev Set.empty}, fastype_of c1))
-      |> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *)
-  in
-    case Function_Lib.try_proof (cterm_of thy goal) chain_tac of
-      Function_Lib.Solved thm => SOME thm
-    | _ => NONE
-  end
-
-fun derive_chains ctxt chain_tac cont D = CALLS (fn (cs, i) =>
-  let
-    val thy = ProofContext.theory_of ctxt
-
-    fun derive_chain c1 c2 D =
-      if is_some (get_chain D c1 c2) then D else
-      note_chain c1 c2 (prove_chain thy chain_tac c1 c2) D
-  in
-    cont (fold_product derive_chain cs cs D) i
-  end)
-
-
 fun mk_dgraph D cs =
   Term_Graph.empty
   |> fold (fn c => Term_Graph.new_node (c, ())) cs
@@ -368,50 +340,23 @@
    | _ => no_tac)
   | _ => no_tac)
 
-fun decompose_tac' cont err_cont D = CALLS (fn (cs, i) =>
+fun decompose_tac D = CALLS (fn (cs, i) =>
   let
     val G = mk_dgraph D cs
     val sccs = Term_Graph.strong_conn G
 
-    fun split [SCC] i = (solve_trivial_tac D i ORELSE cont D i)
+    fun split [SCC] i = TRY (solve_trivial_tac D i)
       | split (SCC::rest) i =
         regroup_calls_tac SCC i
         THEN rtac @{thm wf_union_compatible} i
         THEN rtac @{thm less_by_empty} (i + 2)
         THEN ucomp_empty_tac (the o the oo get_chain D) (i + 2)
         THEN split rest (i + 1)
-        THEN (solve_trivial_tac D i ORELSE cont D i)
+        THEN TRY (solve_trivial_tac D i)
   in
     if length sccs > 1 then split sccs i
-    else solve_trivial_tac D i ORELSE err_cont D i
+    else solve_trivial_tac D i
   end)
 
-fun decompose_tac ctxt chain_tac cont err_cont =
-  derive_chains ctxt chain_tac (decompose_tac' cont err_cont)
-
-
-(*** Local Descent Proofs ***)
-
-fun gen_descent diag ctxt tac cont D = CALLS (fn (cs, i) =>
-  let
-    val thy = ProofContext.theory_of ctxt
-    val measures_of = get_measures D
-
-    fun derive c D =
-      let
-        val (_, p, _, q, _, _) = dest_call D c
-      in
-        if diag andalso p = q
-        then fold (fn m => derive_descent thy tac c m m) (measures_of p) D
-        else fold_product (derive_descent thy tac c)
-               (measures_of p) (measures_of q) D
-      end
-  in
-    cont (Function_Common.PROFILE "deriving descents" (fold derive cs) D) i
-  end)
-
-fun derive_diag ctxt = gen_descent true ctxt
-fun derive_all ctxt = gen_descent false ctxt
-
 
 end