# HG changeset patch
# User wenzelm
# Date 1256685878 -3600
# Node ID 02de0317f66fb7509c0e48b5c99f4175a3ed9df6
# Parent  8fb01a2f94069bb3a22fd95ff266a04dd1ea3619
eliminated hard tabulators, guessing at each author's individual tab-width;

diff -r 8fb01a2f9406 -r 02de0317f66f src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Oct 28 00:23:39 2009 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Oct 28 00:24:38 2009 +0100
@@ -35,7 +35,7 @@
   "Itm vs bs (Add a b) = Itm vs bs a + Itm vs bs b"
   "Itm vs bs (Sub a b) = Itm vs bs a - Itm vs bs b"
   "Itm vs bs (Mul c a) = (Ipoly vs c) * Itm vs bs a"
-  "Itm vs bs (CNP n c t) = (Ipoly vs c)*(bs!n) + Itm vs bs t"	
+  "Itm vs bs (CNP n c t) = (Ipoly vs c)*(bs!n) + Itm vs bs t"   
 
 
 fun allpolys:: "(poly \<Rightarrow> bool) \<Rightarrow> tm \<Rightarrow> bool"  where
@@ -153,14 +153,14 @@
       {assume mxs: "m \<le> length (x#xs)" hence ?case using prems by (cases m, auto)}
       moreover
       {assume mxs: "\<not> (m \<le> length (x#xs))" 
-	have th: "length (removen n (x#xs)) = length xs" 
-	  using removen_length[where n="n" and xs="x#xs"] nxs by simp
-	with mxs have mxs':"m \<ge> length (removen n (x#xs))" by auto
-	hence "(removen n (x#xs))!m = [] ! (m - length xs)" 
-	  using th nth_length_exceeds[OF mxs'] by auto
-	hence th: "(removen n (x#xs))!m = [] ! (m - (length (x#xs) - 1))" 
-	  by auto
-	hence ?case using nxs mln mxs by auto }
+        have th: "length (removen n (x#xs)) = length xs" 
+          using removen_length[where n="n" and xs="x#xs"] nxs by simp
+        with mxs have mxs':"m \<ge> length (removen n (x#xs))" by auto
+        hence "(removen n (x#xs))!m = [] ! (m - length xs)" 
+          using th nth_length_exceeds[OF mxs'] by auto
+        hence th: "(removen n (x#xs))!m = [] ! (m - (length (x#xs) - 1))" 
+          by auto
+        hence ?case using nxs mln mxs by auto }
       ultimately have ?case by blast
     }
     ultimately have ?case by blast
@@ -443,7 +443,7 @@
   "fmsize (A p) = 4+ fmsize p"
   "fmsize p = 1"
   (* several lemmas about fmsize *)
-lemma fmsize_pos: "fmsize p > 0"	
+lemma fmsize_pos: "fmsize p > 0"        
 by (induct p rule: fmsize.induct) simp_all
 
   (* Semantics of formulae (fm) *)
@@ -1393,16 +1393,16 @@
       using eq[OF nc(2), of vs] eq[OF nc(1), of vs] by auto}
   moreover {assume cp: "?c > 0"
     {fix x assume xz: "x < -?e / ?c" hence "?c * x < - ?e"
-	using pos_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
+        using pos_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
       hence "?c * x + ?e < 0" by simp
       hence "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Eq (CNP 0 c e)))"
-	using eqs tmbound0_I[OF nbe, where b="y" and b'="x" and vs=vs and bs=bs] by auto} hence ?case by auto}
+        using eqs tmbound0_I[OF nbe, where b="y" and b'="x" and vs=vs and bs=bs] by auto} hence ?case by auto}
   moreover {assume cp: "?c < 0"
     {fix x assume xz: "x < -?e / ?c" hence "?c * x > - ?e"
-	using neg_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
+        using neg_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
       hence "?c * x + ?e > 0" by simp
       hence "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Eq (CNP 0 c e)))"
-	using tmbound0_I[OF nbe, where b="y" and b'="x"] eqs by auto} hence ?case by auto}
+        using tmbound0_I[OF nbe, where b="y" and b'="x"] eqs by auto} hence ?case by auto}
   ultimately show ?case by blast
 next
   case (4 c e)  hence nbe: "tmbound0 e" by simp
@@ -1414,16 +1414,16 @@
   moreover {assume "?c = 0" hence ?case using eqs by auto}
   moreover {assume cp: "?c > 0"
     {fix x assume xz: "x < -?e / ?c" hence "?c * x < - ?e"
-	using pos_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
+        using pos_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
       hence "?c * x + ?e < 0" by simp
       hence "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (NEq (CNP 0 c e)))"
-	using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto}
+        using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto}
   moreover {assume cp: "?c < 0"
     {fix x assume xz: "x < -?e / ?c" hence "?c * x > - ?e"
-	using neg_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
+        using neg_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
       hence "?c * x + ?e > 0" by simp
       hence "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (NEq (CNP 0 c e)))"
-	using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto}
+        using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto}
   ultimately show ?case by blast
 next
   case (5 c e)  hence nbe: "tmbound0 e" by simp
@@ -1436,16 +1436,16 @@
   moreover {assume "?c = 0" hence ?case using eqs by auto}
   moreover {assume cp: "?c > 0"
     {fix x assume xz: "x < -?e / ?c" hence "?c * x < - ?e"
-	using pos_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
+        using pos_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
       hence "?c * x + ?e < 0" by simp
       hence "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Lt (CNP 0 c e)))"
-	using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
+        using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
   moreover {assume cp: "?c < 0"
     {fix x assume xz: "x < -?e / ?c" hence "?c * x > - ?e"
-	using neg_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
+        using neg_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
       hence "?c * x + ?e > 0" by simp
       hence "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Lt (CNP 0 c e)))"
-	using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] cp by auto} hence ?case by auto}
+        using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] cp by auto} hence ?case by auto}
   ultimately show ?case by blast
 next
   case (6 c e)  hence nbe: "tmbound0 e" by simp
@@ -1458,16 +1458,16 @@
   moreover {assume "?c = 0" hence ?case using eqs by auto}
   moreover {assume cp: "?c > 0"
     {fix x assume xz: "x < -?e / ?c" hence "?c * x < - ?e"
-	using pos_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
+        using pos_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
       hence "?c * x + ?e < 0" by simp
       hence "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Le (CNP 0 c e)))"
-	using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
+        using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
   moreover {assume cp: "?c < 0"
     {fix x assume xz: "x < -?e / ?c" hence "?c * x > - ?e"
-	using neg_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
+        using neg_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
       hence "?c * x + ?e > 0" by simp
       hence "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Le (CNP 0 c e)))"
-	using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
+        using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
   ultimately show ?case by blast
 qed (auto)
 
@@ -1489,16 +1489,16 @@
       using eq[OF nc(2), of vs] eq[OF nc(1), of vs] by auto}
   moreover {assume cp: "?c > 0"
     {fix x assume xz: "x > -?e / ?c" hence "?c * x > - ?e" 
-	using pos_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
+        using pos_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
       hence "?c * x + ?e > 0" by simp
       hence "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Eq (CNP 0 c e)))"
-	using eqs tmbound0_I[OF nbe, where b="y" and b'="x" and vs=vs and bs=bs] by auto} hence ?case by auto}
+        using eqs tmbound0_I[OF nbe, where b="y" and b'="x" and vs=vs and bs=bs] by auto} hence ?case by auto}
   moreover {assume cp: "?c < 0"
     {fix x assume xz: "x > -?e / ?c" hence "?c * x < - ?e"
-	using neg_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
+        using neg_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
       hence "?c * x + ?e < 0" by simp
       hence "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Eq (CNP 0 c e)))"
-	using tmbound0_I[OF nbe, where b="y" and b'="x"] eqs by auto} hence ?case by auto}
+        using tmbound0_I[OF nbe, where b="y" and b'="x"] eqs by auto} hence ?case by auto}
   ultimately show ?case by blast
 next
   case (4 c e)  hence nbe: "tmbound0 e" by simp
@@ -1510,16 +1510,16 @@
   moreover {assume "?c = 0" hence ?case using eqs by auto}
   moreover {assume cp: "?c > 0"
     {fix x assume xz: "x > -?e / ?c" hence "?c * x > - ?e"
-	using pos_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
+        using pos_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
       hence "?c * x + ?e > 0" by simp
       hence "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (NEq (CNP 0 c e)))"
-	using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto}
+        using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto}
   moreover {assume cp: "?c < 0"
     {fix x assume xz: "x > -?e / ?c" hence "?c * x < - ?e"
-	using neg_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
+        using neg_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
       hence "?c * x + ?e < 0" by simp
       hence "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (NEq (CNP 0 c e)))"
-	using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto}
+        using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto}
   ultimately show ?case by blast
 next
   case (5 c e)  hence nbe: "tmbound0 e" by simp
@@ -1532,16 +1532,16 @@
   moreover {assume "?c = 0" hence ?case using eqs by auto}
   moreover {assume cp: "?c > 0"
     {fix x assume xz: "x > -?e / ?c" hence "?c * x > - ?e"
-	using pos_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
+        using pos_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
       hence "?c * x + ?e > 0" by simp
       hence "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Lt (CNP 0 c e)))"
-	using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
+        using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
   moreover {assume cp: "?c < 0"
     {fix x assume xz: "x > -?e / ?c" hence "?c * x < - ?e"
-	using neg_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
+        using neg_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
       hence "?c * x + ?e < 0" by simp
       hence "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Lt (CNP 0 c e)))"
-	using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] cp by auto} hence ?case by auto}
+        using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] cp by auto} hence ?case by auto}
   ultimately show ?case by blast
 next
   case (6 c e)  hence nbe: "tmbound0 e" by simp
@@ -1554,16 +1554,16 @@
   moreover {assume "?c = 0" hence ?case using eqs by auto}
   moreover {assume cp: "?c > 0"
     {fix x assume xz: "x > -?e / ?c" hence "?c * x > - ?e"
-	using pos_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
+        using pos_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
       hence "?c * x + ?e > 0" by simp
       hence "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Le (CNP 0 c e)))"
-	using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
+        using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
   moreover {assume cp: "?c < 0"
     {fix x assume xz: "x > -?e / ?c" hence "?c * x < - ?e"
-	using neg_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
+        using neg_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
       hence "?c * x + ?e < 0" by simp
       hence "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Le (CNP 0 c e)))"
-	using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
+        using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
   ultimately show ?case by blast
 qed (auto)
 
@@ -1698,10 +1698,10 @@
   {assume c: "?N c > 0"
       from px pos_less_divide_eq[OF c, where a="x" and b="-?Nt x s"]  
       have px': "x < - ?Nt x s / ?N c" 
-	by (auto simp add: not_less ring_simps) 
+        by (auto simp add: not_less ring_simps) 
     {assume y: "y < - ?Nt x s / ?N c" 
       hence "y * ?N c < - ?Nt x s"
-	by (simp add: pos_less_divide_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
+        by (simp add: pos_less_divide_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
       hence "?N c * y + ?Nt x s < 0" by (simp add: ring_simps)
       hence ?case using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"] by simp}
     moreover
@@ -1715,10 +1715,10 @@
   {assume c: "?N c < 0"
       from px neg_divide_less_eq[OF c, where a="x" and b="-?Nt x s"]  
       have px': "x > - ?Nt x s / ?N c" 
-	by (auto simp add: not_less ring_simps) 
+        by (auto simp add: not_less ring_simps) 
     {assume y: "y > - ?Nt x s / ?N c" 
       hence "y * ?N c < - ?Nt x s"
-	by (simp add: neg_divide_less_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
+        by (simp add: neg_divide_less_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
       hence "?N c * y + ?Nt x s < 0" by (simp add: ring_simps)
       hence ?case using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"] by simp}
     moreover
@@ -1746,7 +1746,7 @@
       have px': "x <= - ?Nt x s / ?N c" by (simp add: not_less ring_simps) 
     {assume y: "y < - ?Nt x s / ?N c" 
       hence "y * ?N c < - ?Nt x s"
-	by (simp add: pos_less_divide_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
+        by (simp add: pos_less_divide_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
       hence "?N c * y + ?Nt x s < 0" by (simp add: ring_simps)
       hence ?case using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"] by simp}
     moreover
@@ -1762,7 +1762,7 @@
       have px': "x >= - ?Nt x s / ?N c" by (simp add: ring_simps) 
     {assume y: "y > - ?Nt x s / ?N c" 
       hence "y * ?N c < - ?Nt x s"
-	by (simp add: neg_divide_less_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
+        by (simp add: neg_divide_less_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
       hence "?N c * y + ?Nt x s < 0" by (simp add: ring_simps)
       hence ?case using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"] by simp}
     moreover
@@ -1899,8 +1899,8 @@
     moreover{
       assume "\<exists> t1\<in> ?M. \<exists> t2 \<in> ?M. (\<forall> y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> ?M) \<and> t1 < a \<and> a < t2 \<and> ?I a p"
       then obtain t1 and t2 where t1M: "t1 \<in> ?M" and t2M: "t2\<in> ?M" 
-	and noM: "\<forall> y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> ?M" and t1x: "t1 < a" and xt2: "a < t2" and px: "?I a p"
-	by blast
+        and noM: "\<forall> y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> ?M" and t1x: "t1 < a" and xt2: "a < t2" and px: "?I a p"
+        by blast
       from t1M have "\<exists> (t1n,t1u) \<in> ?U. t1 = - ?Nt a t1u / ?N t1n" by auto
       then obtain "t1u" "t1n" where t1uU: "(t1n,t1u) \<in> ?U" and t1u: "t1 = - ?Nt a t1u / ?N t1n" by blast
       from t2M have "\<exists> (t2n,t2u) \<in> ?U. t2 = - ?Nt a t2u / ?N t2n" by auto
@@ -2236,7 +2236,7 @@
       using c order_less_not_sym[OF c''] less_imp_neq[OF c''] c'' mult_less_cancel_left_disj[of "(1 + 1) * ?c" 0 "?a* (- ?t / ((1 + 1)*?c))+ ?r"] by simp
     also have "\<dots> \<longleftrightarrow> ?a*?t -  (1 + 1)*?c *?r < 0" 
       using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c''] less_imp_neq[OF c''] c''
-	by (simp add: ring_simps diff_divide_distrib del:  left_distrib)
+        by (simp add: ring_simps diff_divide_distrib del:  left_distrib)
     finally have ?thesis using c d nc nd 
       apply(simp add: r[of "- (?t / ((1 + 1)*?c))"] msubstlt_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm)
       apply (simp only: one_add_one_is_two[symmetric] of_int_add)
@@ -2270,7 +2270,7 @@
       using d order_less_not_sym[OF d''] less_imp_neq[OF d''] d'' mult_less_cancel_left_disj[of "(1 + 1) * ?d" 0 "?a* (- ?s / ((1 + 1)*?d))+ ?r"] by simp
     also have "\<dots> \<longleftrightarrow> ?a*?s -  (1 + 1)*?d *?r < 0" 
       using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d''] less_imp_neq[OF d''] d''
-	by (simp add: ring_simps diff_divide_distrib del:  left_distrib)
+        by (simp add: ring_simps diff_divide_distrib del:  left_distrib)
     finally have ?thesis using c d nc nd 
       apply(simp add: r[of "- (?s / ((1 + 1)*?d))"] msubstlt_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm)
       apply (simp only: one_add_one_is_two[symmetric] of_int_add)
@@ -2392,7 +2392,7 @@
       using c order_less_not_sym[OF c''] less_imp_neq[OF c''] c'' mult_le_cancel_left[of "(1 + 1) * ?c" 0 "?a* (- ?t / ((1 + 1)*?c))+ ?r"] by simp
     also have "\<dots> \<longleftrightarrow> ?a*?t -  (1 + 1)*?c *?r <= 0" 
       using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c''] less_imp_neq[OF c''] c''
-	by (simp add: ring_simps diff_divide_distrib del:  left_distrib)
+        by (simp add: ring_simps diff_divide_distrib del:  left_distrib)
     finally have ?thesis using c d nc nd 
       apply(simp add: r[of "- (?t / ((1 + 1)*?c))"] msubstle_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm)
       apply (simp only: one_add_one_is_two[symmetric] of_int_add)
@@ -2426,7 +2426,7 @@
       using d order_less_not_sym[OF d''] less_imp_neq[OF d''] d'' mult_le_cancel_left[of "(1 + 1) * ?d" 0 "?a* (- ?s / ((1 + 1)*?d))+ ?r"] by simp
     also have "\<dots> \<longleftrightarrow> ?a*?s -  (1 + 1)*?d *?r <= 0" 
       using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d''] less_imp_neq[OF d''] d''
-	by (simp add: ring_simps diff_divide_distrib del:  left_distrib)
+        by (simp add: ring_simps diff_divide_distrib del:  left_distrib)
     finally have ?thesis using c d nc nd 
       apply(simp add: r[of "- (?s / ((1 + 1)*?d))"] msubstle_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm)
       apply (simp only: one_add_one_is_two[symmetric] of_int_add)
@@ -2638,8 +2638,8 @@
     moreover
     {assume z: "?c \<noteq> 0" "?d \<noteq> 0"
       from z have ?F using ct
-	apply - apply (rule bexI[where x = "(c,t)"], simp_all)
-	by (rule bexI[where x = "(d,s)"], simp_all)
+        apply - apply (rule bexI[where x = "(c,t)"], simp_all)
+        by (rule bexI[where x = "(d,s)"], simp_all)
       hence ?D by blast}
     ultimately have ?D by auto}
   ultimately show "?D" by blast
@@ -2799,17 +2799,17 @@
       from H(1) th have "isnpoly n" by blast
       hence nn: "isnpoly (n *\<^sub>p (C (-2,1)))" by (simp_all add: polymul_norm n2)
       have nn': "allpolys isnpoly (CP (~\<^sub>p (n *\<^sub>p C (-2, 1))))"
-	by (simp add: polyneg_norm nn)
+        by (simp add: polyneg_norm nn)
       hence nn2: "\<lparr>n *\<^sub>p(C (-2,1)) \<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>n \<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" using H(2) nn' nn 
-	by (auto simp add: msubst2_def lt zero_less_mult_iff mult_less_0_iff)
+        by (auto simp add: msubst2_def lt zero_less_mult_iff mult_less_0_iff)
       from msubst2[OF lp nn nn2(1), of x bs t]
       have "\<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and> Ifm vs (- Itm vs (x # bs) t / (\<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> * (1 + 1)) # bs) p"
-	using H(2) nn2 by (simp add: of_int_minus2 del: minus_add_distrib)}
+        using H(2) nn2 by (simp add: of_int_minus2 del: minus_add_distrib)}
     moreover
     {fix n t assume H: "(n, t)\<in>set (uset p)" "\<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "Ifm vs (- Itm vs (x # bs) t / (\<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> * (1 + 1)) # bs) p"
       from H(1) th have "isnpoly n" by blast
       hence nn: "isnpoly (n *\<^sub>p (C (-2,1)))" "\<lparr>n *\<^sub>p(C (-2,1)) \<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
-	using H(2) by (simp_all add: polymul_norm n2)
+        using H(2) by (simp_all add: polymul_norm n2)
       from msubst2[OF lp nn, of x bs t] have "?I (msubst2 p (n *\<^sub>p (C (-2,1))) t)" using H(2,3) by (simp add: of_int_minus2 del: minus_add_distrib)}
     ultimately show ?thesis by blast
   qed
@@ -2820,21 +2820,21 @@
      "Ifm vs (x#bs) (msubst2 p (C (-2, 1) *\<^sub>p c*\<^sub>p d) (Add (Mul d t) (Mul c s)))"
       from H(1,2) th have "isnpoly c" "isnpoly d" by blast+
       hence nn: "isnpoly (C (-2, 1) *\<^sub>p c*\<^sub>p d)" 
-	by (simp_all add: polymul_norm n2)
+        by (simp_all add: polymul_norm n2)
       have stupid: "allpolys isnpoly (CP (~\<^sub>p (C (-2, 1) *\<^sub>p c *\<^sub>p d)))" "allpolys isnpoly (CP ((C (-2, 1) *\<^sub>p c *\<^sub>p d)))"
-	by (simp_all add: polyneg_norm nn)
+        by (simp_all add: polyneg_norm nn)
       have nn': "\<lparr>(C (-2, 1) *\<^sub>p c*\<^sub>p d)\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
-	using H(3) by (auto simp add: msubst2_def lt[OF stupid(1)]  lt[OF stupid(2)] zero_less_mult_iff mult_less_0_iff)
+        using H(3) by (auto simp add: msubst2_def lt[OF stupid(1)]  lt[OF stupid(2)] zero_less_mult_iff mult_less_0_iff)
       from msubst2[OF lp nn nn'(1), of x bs ] H(3) nn'
       have "\<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and> \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and> Ifm vs ((- Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>) / (1 + 1) # bs) p" 
-	apply (simp add: add_divide_distrib of_int_minus2 del: minus_add_distrib)
-	by (simp add: mult_commute)}
+        apply (simp add: add_divide_distrib of_int_minus2 del: minus_add_distrib)
+        by (simp add: mult_commute)}
     moreover
     {fix c t d s assume H: "(c,t) \<in> set (uset p)" "(d,s) \<in> set (uset p)" 
       "\<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "Ifm vs ((- Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>) / (1 + 1) # bs) p"
      from H(1,2) th have "isnpoly c" "isnpoly d" by blast+
       hence nn: "isnpoly (C (-2, 1) *\<^sub>p c*\<^sub>p d)" "\<lparr>(C (-2, 1) *\<^sub>p c*\<^sub>p d)\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
-	using H(3,4) by (simp_all add: polymul_norm n2)
+        using H(3,4) by (simp_all add: polymul_norm n2)
       from msubst2[OF lp nn, of x bs ] H(3,4,5) 
       have "Ifm vs (x#bs) (msubst2 p (C (-2, 1) *\<^sub>p c*\<^sub>p d) (Add (Mul d t) (Mul c s)))" apply (simp add: add_divide_distrib of_int_minus2 del: minus_add_distrib)by (simp add: mult_commute)}
     ultimately show ?thesis by blast
@@ -2906,16 +2906,16 @@
     proof
       assume H: ?lhs
       hence z: "\<lparr>C (-2, 1) *\<^sub>p b *\<^sub>p d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>C (-2, 1) *\<^sub>p d *\<^sub>p b\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" 
-	by (auto simp add: msubst2_def lt[OF stupid(3)] lt[OF stupid(1)] mult_less_0_iff zero_less_mult_iff)
+        by (auto simp add: msubst2_def lt[OF stupid(3)] lt[OF stupid(1)] mult_less_0_iff zero_less_mult_iff)
       from msubst2[OF lq norm2(1) z(1), of x bs] 
-	msubst2[OF lq norm2(2) z(2), of x bs] H 
+        msubst2[OF lq norm2(2) z(2), of x bs] H 
       show ?rhs by (simp add: ring_simps)
     next
       assume H: ?rhs
       hence z: "\<lparr>C (-2, 1) *\<^sub>p b *\<^sub>p d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>C (-2, 1) *\<^sub>p d *\<^sub>p b\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" 
-	by (auto simp add: msubst2_def lt[OF stupid(4)] lt[OF stupid(2)] mult_less_0_iff zero_less_mult_iff)
+        by (auto simp add: msubst2_def lt[OF stupid(4)] lt[OF stupid(2)] mult_less_0_iff zero_less_mult_iff)
       from msubst2[OF lq norm2(1) z(1), of x bs] 
-	msubst2[OF lq norm2(2) z(2), of x bs] H 
+        msubst2[OF lq norm2(2) z(2), of x bs] H 
       show ?lhs by (simp add: ring_simps)
     qed}
   hence th0: "\<forall>x \<in> set ?U. \<forall>y \<in> set ?U. ?I (?s (x, y)) \<longleftrightarrow> ?I (?s (y, x))"
diff -r 8fb01a2f9406 -r 02de0317f66f src/HOL/Decision_Procs/Polynomial_List.thy
--- a/src/HOL/Decision_Procs/Polynomial_List.thy	Wed Oct 28 00:23:39 2009 +0100
+++ b/src/HOL/Decision_Procs/Polynomial_List.thy	Wed Oct 28 00:24:38 2009 +0100
@@ -1,8 +1,8 @@
-(*  Title:       HOL/Decision_Procs/Polynomial_List.thy
-    Author:      Amine Chaieb
+(*  Title:      HOL/Decision_Procs/Polynomial_List.thy
+    Author:     Amine Chaieb
 *)
 
-header{*Univariate Polynomials as Lists *}
+header {* Univariate Polynomials as Lists *}
 
 theory Polynomial_List
 imports Main
@@ -653,7 +653,7 @@
 apply (simp add: divides_def fun_eq poly_mult)
 apply (rule_tac x = "[]" in exI)
 apply (auto dest!: order2 [where a=a]
-	    intro: poly_exp_divides simp del: pexp_Suc)
+            intro: poly_exp_divides simp del: pexp_Suc)
 done
 
 lemma order_decomp:
@@ -780,4 +780,5 @@
 done
 
 lemma poly_Sing: "poly [c] x = c" by simp
+
 end
diff -r 8fb01a2f9406 -r 02de0317f66f src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Wed Oct 28 00:23:39 2009 +0100
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Wed Oct 28 00:24:38 2009 +0100
@@ -391,7 +391,7 @@
   {assume nn':"\<not> n' < n" hence "n < n' \<or> n = n'" by arith
     moreover {assume "n < n'" with prems have ?case by simp }
     moreover {assume eq: "n = n'" hence ?case using prems 
-	by (cases "p +\<^sub>p p' = 0\<^sub>p", auto simp add: Let_def) }
+        by (cases "p +\<^sub>p p' = 0\<^sub>p", auto simp add: Let_def) }
     ultimately have ?case by blast}
   ultimately show ?case by blast
 qed simp_all
@@ -413,10 +413,10 @@
       by simp_all
     {assume "?c = 0\<^sub>N" hence ?case by auto}
       moreover {assume cnz: "?c \<noteq> 0\<^sub>N" 
-	from "2.hyps"(1)[rule_format,where xb="n'",  OF cnz n(1) n(3)] 
-	  "2.hyps"(2)[rule_format, where x="Suc n'" 
-	  and xa="Suc n'" and xb = "n'", OF cnz ] cnz n have ?case
-	  by (auto simp add: min_def)}
+        from "2.hyps"(1)[rule_format,where xb="n'",  OF cnz n(1) n(3)] 
+          "2.hyps"(2)[rule_format, where x="Suc n'" 
+          and xa="Suc n'" and xb = "n'", OF cnz ] cnz n have ?case
+          by (auto simp add: min_def)}
       ultimately show ?case by blast
   next
     case (2 n0 n1) thus ?case by auto 
@@ -431,10 +431,10 @@
       by simp_all
     {assume "?c' = 0\<^sub>N" hence ?case by auto}
       moreover {assume cnz: "?c' \<noteq> 0\<^sub>N"
-	from "3.hyps"(1)[rule_format,where xb="n",  OF cnz n(3) n(1)] 
-	  "3.hyps"(2)[rule_format, where x="Suc n" 
-	  and xa="Suc n" and xb = "n", OF cnz ] cnz n have ?case
-	  by (auto simp add: min_def)}
+        from "3.hyps"(1)[rule_format,where xb="n",  OF cnz n(3) n(1)] 
+          "3.hyps"(2)[rule_format, where x="Suc n" 
+          and xa="Suc n" and xb = "n", OF cnz ] cnz n have ?case
+          by (auto simp add: min_def)}
       ultimately show ?case by blast
   next
     case (2 n0 n1) thus ?case apply auto done
@@ -446,32 +446,32 @@
     {fix n0 n1
       assume "isnpolyh ?cnp n0" and "isnpolyh ?cnp' n1"
       hence cnp: "isnpolyh ?cnp n" and cnp': "isnpolyh ?cnp' n'"
-	and np: "isnpolyh p n" and nc: "isnpolyh c (Suc n)" 
-	and np': "isnpolyh p' n'" and nc': "isnpolyh c' (Suc n')"
-	and nn0: "n \<ge> n0" and nn1:"n' \<ge> n1"
-	by simp_all
+        and np: "isnpolyh p n" and nc: "isnpolyh c (Suc n)" 
+        and np': "isnpolyh p' n'" and nc': "isnpolyh c' (Suc n')"
+        and nn0: "n \<ge> n0" and nn1:"n' \<ge> n1"
+        by simp_all
       have "n < n' \<or> n' < n \<or> n' = n" by auto
       moreover
       {assume nn': "n < n'"
-	with "4.hyps"(5)[rule_format, OF nn' np cnp', where xb ="n"] 
-	  "4.hyps"(6)[rule_format, OF nn' nc cnp', where xb="n"] nn' nn0 nn1 cnp
-	have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
-	  by (simp add: min_def) }
+        with "4.hyps"(5)[rule_format, OF nn' np cnp', where xb ="n"] 
+          "4.hyps"(6)[rule_format, OF nn' nc cnp', where xb="n"] nn' nn0 nn1 cnp
+        have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
+          by (simp add: min_def) }
       moreover
 
       {assume nn': "n > n'" hence stupid: "n' < n \<and> \<not> n < n'" by arith
-	with "4.hyps"(3)[rule_format, OF stupid cnp np', where xb="n'"]
-	  "4.hyps"(4)[rule_format, OF stupid cnp nc', where xb="Suc n'"] 
-	  nn' nn0 nn1 cnp'
-	have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
-	  by (cases "Suc n' = n", simp_all add: min_def)}
+        with "4.hyps"(3)[rule_format, OF stupid cnp np', where xb="n'"]
+          "4.hyps"(4)[rule_format, OF stupid cnp nc', where xb="Suc n'"] 
+          nn' nn0 nn1 cnp'
+        have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
+          by (cases "Suc n' = n", simp_all add: min_def)}
       moreover
       {assume nn': "n' = n" hence stupid: "\<not> n' < n \<and> \<not> n < n'" by arith
-	from "4.hyps"(1)[rule_format, OF stupid cnp np', where xb="n"]
-	  "4.hyps"(2)[rule_format, OF stupid cnp nc', where xb="n"] nn' cnp cnp' nn1
-	
-	have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
-	  by simp (rule polyadd_normh,simp_all add: min_def isnpolyh_mono[OF nn0]) }
+        from "4.hyps"(1)[rule_format, OF stupid cnp np', where xb="n"]
+          "4.hyps"(2)[rule_format, OF stupid cnp nc', where xb="n"] nn' cnp cnp' nn1
+        
+        have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
+          by simp (rule polyadd_normh,simp_all add: min_def isnpolyh_mono[OF nn0]) }
       ultimately show "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)" by blast }
     note th = this
     {fix n0 n1 m
@@ -484,86 +484,86 @@
       have "n'<n \<or> n < n' \<or> n' = n" by auto
       moreover 
       {assume "n' < n \<or> n < n'"
-	with "4.hyps" np np' m 
-	have ?eq apply (cases "n' < n", simp_all)
-	apply (erule allE[where x="n"],erule allE[where x="n"],auto) 
-	done }
+        with "4.hyps" np np' m 
+        have ?eq apply (cases "n' < n", simp_all)
+        apply (erule allE[where x="n"],erule allE[where x="n"],auto) 
+        done }
       moreover
       {assume nn': "n' = n"  hence nn:"\<not> n' < n \<and> \<not> n < n'" by arith
- 	from "4.hyps"(1)[rule_format, OF nn, where x="n" and xa ="n'" and xb="n"]
-	  "4.hyps"(2)[rule_format, OF nn, where x="n" and xa ="Suc n'" and xb="n"] 
-	  np np' nn'
-	have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"
-	  "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
-	  "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)" 
-	  "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p" by (auto simp add: min_def)
-	{assume mn: "m = n" 
-	  from "4.hyps"(1)[rule_format, OF nn norm(1,4), where xb="n"]
-	    "4.hyps"(2)[rule_format, OF nn norm(1,2), where xb="n"] norm nn' mn
-	  have degs:  "degreen (?cnp *\<^sub>p c') n = 
-	    (if c'=0\<^sub>p then 0 else ?d1 + degreen c' n)"
-	    "degreen (?cnp *\<^sub>p p') n = ?d1  + degreen p' n" by (simp_all add: min_def)
-	  from degs norm
-	  have th1: "degreen(?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" by simp
-	  hence neq: "degreen (?cnp *\<^sub>p c') n \<noteq> degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n"
-	    by simp
-	  have nmin: "n \<le> min n n" by (simp add: min_def)
-	  from polyadd_different_degreen[OF norm(3,6) neq nmin] th1
-	  have deg: "degreen (CN c n p *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n = degreen (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp 
-	  from "4.hyps"(1)[rule_format, OF nn norm(1,4), where xb="n"]
-	    "4.hyps"(2)[rule_format, OF nn norm(1,2), where xb="n"]
-	    mn norm m nn' deg
-	  have ?eq by simp}
-	moreover
-	{assume mn: "m \<noteq> n" hence mn': "m < n" using m np by auto
-	  from nn' m np have max1: "m \<le> max n n"  by simp 
-	  hence min1: "m \<le> min n n" by simp	
-	  hence min2: "m \<le> min n (Suc n)" by simp
-	  {assume "c' = 0\<^sub>p"
-	    from `c' = 0\<^sub>p` have ?eq
-	      using "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
-	    "4.hyps"(2)[rule_format, OF nn norm(1,2) min2] mn nn'
-	      apply simp
-	      done}
-	  moreover
-	  {assume cnz: "c' \<noteq> 0\<^sub>p"
-	    from "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
-	      "4.hyps"(2)[rule_format, OF nn norm(1,2) min2]
-	      degreen_polyadd[OF norm(3,6) max1]
+        from "4.hyps"(1)[rule_format, OF nn, where x="n" and xa ="n'" and xb="n"]
+          "4.hyps"(2)[rule_format, OF nn, where x="n" and xa ="Suc n'" and xb="n"] 
+          np np' nn'
+        have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"
+          "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
+          "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)" 
+          "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p" by (auto simp add: min_def)
+        {assume mn: "m = n" 
+          from "4.hyps"(1)[rule_format, OF nn norm(1,4), where xb="n"]
+            "4.hyps"(2)[rule_format, OF nn norm(1,2), where xb="n"] norm nn' mn
+          have degs:  "degreen (?cnp *\<^sub>p c') n = 
+            (if c'=0\<^sub>p then 0 else ?d1 + degreen c' n)"
+            "degreen (?cnp *\<^sub>p p') n = ?d1  + degreen p' n" by (simp_all add: min_def)
+          from degs norm
+          have th1: "degreen(?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" by simp
+          hence neq: "degreen (?cnp *\<^sub>p c') n \<noteq> degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n"
+            by simp
+          have nmin: "n \<le> min n n" by (simp add: min_def)
+          from polyadd_different_degreen[OF norm(3,6) neq nmin] th1
+          have deg: "degreen (CN c n p *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n = degreen (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp 
+          from "4.hyps"(1)[rule_format, OF nn norm(1,4), where xb="n"]
+            "4.hyps"(2)[rule_format, OF nn norm(1,2), where xb="n"]
+            mn norm m nn' deg
+          have ?eq by simp}
+        moreover
+        {assume mn: "m \<noteq> n" hence mn': "m < n" using m np by auto
+          from nn' m np have max1: "m \<le> max n n"  by simp 
+          hence min1: "m \<le> min n n" by simp     
+          hence min2: "m \<le> min n (Suc n)" by simp
+          {assume "c' = 0\<^sub>p"
+            from `c' = 0\<^sub>p` have ?eq
+              using "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
+            "4.hyps"(2)[rule_format, OF nn norm(1,2) min2] mn nn'
+              apply simp
+              done}
+          moreover
+          {assume cnz: "c' \<noteq> 0\<^sub>p"
+            from "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
+              "4.hyps"(2)[rule_format, OF nn norm(1,2) min2]
+              degreen_polyadd[OF norm(3,6) max1]
 
-	    have "degreen (?cnp *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (?cnp *\<^sub>p p')) m 
-	      \<le> max (degreen (?cnp *\<^sub>p c') m) (degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) m)"
-	      using mn nn' cnz np np' by simp
-	    with "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
-	      "4.hyps"(2)[rule_format, OF nn norm(1,2) min2]
-	      degreen_0[OF norm(3) mn'] have ?eq using nn' mn cnz np np' by clarsimp}
-	  ultimately have ?eq by blast }
-	ultimately have ?eq by blast}
+            have "degreen (?cnp *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (?cnp *\<^sub>p p')) m 
+              \<le> max (degreen (?cnp *\<^sub>p c') m) (degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) m)"
+              using mn nn' cnz np np' by simp
+            with "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
+              "4.hyps"(2)[rule_format, OF nn norm(1,2) min2]
+              degreen_0[OF norm(3) mn'] have ?eq using nn' mn cnz np np' by clarsimp}
+          ultimately have ?eq by blast }
+        ultimately have ?eq by blast}
       ultimately show ?eq by blast}
     note degth = this
     { case (2 n0 n1)
       hence np: "isnpolyh ?cnp n0" and np': "isnpolyh ?cnp' n1" 
-	and m: "m \<le> min n0 n1" by simp_all
+        and m: "m \<le> min n0 n1" by simp_all
       hence mn: "m \<le> n" by simp
       let ?c0p = "CN 0\<^sub>p n (?cnp *\<^sub>p p')"
       {assume C: "?cnp *\<^sub>p c' +\<^sub>p ?c0p = 0\<^sub>p" "n' = n"
-	hence nn: "\<not>n' < n \<and> \<not> n<n'" by simp
-	from "4.hyps"(1) [rule_format, OF nn, where x="n" and xa = "n" and xb="n"] 
-	  "4.hyps"(2) [rule_format, OF nn, where x="n" and xa = "Suc n" and xb="n"] 
-	  np np' C(2) mn
-	have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"
-	  "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
-	  "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)" 
-	  "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p" 
-	  "degreen (?cnp *\<^sub>p c') n = (if c'=0\<^sub>p then 0 else degreen ?cnp n + degreen c' n)"
-	    "degreen (?cnp *\<^sub>p p') n = degreen ?cnp n + degreen p' n"
-	  by (simp_all add: min_def)
-	    
-	  from norm have cn: "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp
-	  have degneq: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" 
-	    using norm by simp
-	from polyadd_eq_const_degreen[OF norm(3) cn C(1), where m="n"]  degneq
-	have "False" by simp }
+        hence nn: "\<not>n' < n \<and> \<not> n<n'" by simp
+        from "4.hyps"(1) [rule_format, OF nn, where x="n" and xa = "n" and xb="n"] 
+          "4.hyps"(2) [rule_format, OF nn, where x="n" and xa = "Suc n" and xb="n"] 
+          np np' C(2) mn
+        have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"
+          "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
+          "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)" 
+          "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p" 
+          "degreen (?cnp *\<^sub>p c') n = (if c'=0\<^sub>p then 0 else degreen ?cnp n + degreen c' n)"
+            "degreen (?cnp *\<^sub>p p') n = degreen ?cnp n + degreen p' n"
+          by (simp_all add: min_def)
+            
+          from norm have cn: "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp
+          have degneq: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" 
+            using norm by simp
+        from polyadd_eq_const_degreen[OF norm(3) cn C(1), where m="n"]  degneq
+        have "False" by simp }
       thus ?case using "4.hyps" by clarsimp}
 qed auto
 
@@ -1022,8 +1022,8 @@
       have "\<forall>x. poly (polypoly' (?ts @ xs) p) x = poly [] x"  by simp
       hence "poly (polypoly' (?ts @ xs) p) = poly []" by (auto intro: ext) 
       hence "\<forall> c \<in> set (coefficients p). Ipoly (?ts @ xs) (decrpoly c) = 0"
-	thm poly_zero
-	using poly_zero[where ?'a='a] by (simp add: polypoly'_def list_all_iff)
+        thm poly_zero
+        using poly_zero[where ?'a='a] by (simp add: polypoly'_def list_all_iff)
       with coefficients_head[of p, symmetric]
       have th0: "Ipoly (?ts @ xs) ?hd = 0" by simp
       from bs have wf'': "wf_bs ?ts ?hd" unfolding wf_bs_def by simp
@@ -1272,18 +1272,18 @@
       by (simp add: min_def)
     {assume np: "n > 0"
       with nn' head_isnpolyh_Suc'[OF np nth]
-	head_isnpolyh_Suc'[OF np norm(5)] head_isnpolyh_Suc'[OF np norm(6)[simplified nn']]
+        head_isnpolyh_Suc'[OF np norm(5)] head_isnpolyh_Suc'[OF np norm(6)[simplified nn']]
       have ?case by simp}
     moreover
     {moreover assume nz: "n = 0"
       from polymul_degreen[OF norm(5,4), where m="0"]
-	polymul_degreen[OF norm(5,3), where m="0"] nn' nz degree_eq_degreen0
+        polymul_degreen[OF norm(5,3), where m="0"] nn' nz degree_eq_degreen0
       norm(5,6) degree_npolyhCN[OF norm(6)]
     have dth:"degree (CN c 0 p *\<^sub>p c') < degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))" by simp
     hence dth':"degree (CN c 0 p *\<^sub>p c') \<noteq> degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))" by simp
     from polyadd_head[OF ncnpc'[simplified nz] ncnpp0'[simplified nz] dth'] dth
     have ?case   using norm prems(2)[rule_format, OF stupid norm(5,3)]
-	prems(3)[rule_format, OF stupid norm(5,4)] nn' nz by simp }
+        prems(3)[rule_format, OF stupid norm(5,4)] nn' nz by simp }
     ultimately have ?case by (cases n) auto} 
   ultimately show ?case by blast
 qed simp_all
@@ -1399,182 +1399,182 @@
     moreover 
     {assume dn': "\<not> d < n" hence dn: "d \<ge> n" by arith
       have degsp': "degree s = degree ?p'" 
-	using ds dn ndp funpow_shift1_degree[where k = "d - n" and p="p"] by simp
+        using ds dn ndp funpow_shift1_degree[where k = "d - n" and p="p"] by simp
       {assume ba: "?b = a"
-	hence headsp': "head s = head ?p'" using ap headp' by simp
-	have nr: "isnpolyh (s -\<^sub>p ?p') 0" using polysub_normh[OF ns np'] by simp
-	from ds degree_polysub_samehead[OF ns np' headsp' degsp']
-	have "degree (s -\<^sub>p ?p') < d \<or> s -\<^sub>p ?p' = 0\<^sub>p" by simp
-	moreover 
-	{assume deglt:"degree (s -\<^sub>p ?p') < d"
-	  from  H[rule_format, OF deglt nr,simplified] 
-	  have domsp: "?D (a, n, p, k, s -\<^sub>p ?p')" by blast 
-	  have dom: ?dths apply (rule polydivide_aux_real_domintros) 
-	    using ba ds dn' domsp by simp_all
-	  from polydivide_aux.psimps[OF dom] sz dn' ba ds
-	  have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')"
-	    by (simp add: Let_def)
-	  {assume h1: "polydivide_aux (a, n, p, k, s) = (k', r)"
-	    from H[rule_format, OF deglt nr, where xa = "k" and xb="k'" and xc="r", simplified]
-	      trans[OF eq[symmetric] h1]
-	    have kk': "k \<le> k'" and nr:"\<exists>nr. isnpolyh r nr" and dr: "degree r = 0 \<or> degree r < degree p"
-	      and q1:"\<exists>q nq. isnpolyh q nq \<and> (a ^\<^sub>p k' - k *\<^sub>p (s -\<^sub>p ?p') = p *\<^sub>p q +\<^sub>p r)" by auto
-	    from q1 obtain q n1 where nq: "isnpolyh q n1" 
-	      and asp:"a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p') = p *\<^sub>p q +\<^sub>p r"  by blast
-	    from nr obtain nr where nr': "isnpolyh r nr" by blast
-	    from polymul_normh[OF nakk' ns] have nakks': "isnpolyh (a ^\<^sub>p (k' - k) *\<^sub>p s) 0" by simp
-	    from polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]
-	    have nq': "isnpolyh (?akk' *\<^sub>p ?xdn +\<^sub>p q) 0" by simp
-	    from polyadd_normh[OF polymul_normh[OF np 
-	      polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]] nr']
-	    have nqr': "isnpolyh (p *\<^sub>p (?akk' *\<^sub>p ?xdn +\<^sub>p q) +\<^sub>p r) 0" by simp 
-	    from asp have "\<forall> (bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p')) = 
-	      Ipoly bs (p *\<^sub>p q +\<^sub>p r)" by simp
-	    hence " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) = 
-	      Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r" 
-	      by (simp add: ring_simps)
-	    hence " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
-	      Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (d - n) shift1 1\<^sub>p *\<^sub>p p) 
-	      + Ipoly bs p * Ipoly bs q + Ipoly bs r"
-	      by (auto simp only: funpow_shift1_1) 
-	    hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
-	      Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (d - n) shift1 1\<^sub>p) 
-	      + Ipoly bs q) + Ipoly bs r" by (simp add: ring_simps)
-	    hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
-	      Ipoly bs (p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (d - n) shift1 1\<^sub>p) +\<^sub>p q) +\<^sub>p r)" by simp
-	    with isnpolyh_unique[OF nakks' nqr']
-	    have "a ^\<^sub>p (k' - k) *\<^sub>p s = 
-	      p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (d - n) shift1 1\<^sub>p) +\<^sub>p q) +\<^sub>p r" by blast
-	    hence ?qths using nq'
-	      apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (d - n) shift1 1\<^sub>p) +\<^sub>p q" in exI)
-	      apply (rule_tac x="0" in exI) by simp
-	    with kk' nr dr have "k \<le> k' \<and> (degree r = 0 \<or> degree r < degree p) \<and> (\<exists>nr. isnpolyh r nr) \<and> ?qths"
-	      by blast } hence ?qrths by blast
-	  with dom have ?ths by blast} 
-	moreover 
-	{assume spz:"s -\<^sub>p ?p' = 0\<^sub>p"
-	  hence domsp: "?D (a, n, p, k, s -\<^sub>p ?p')" 
-	    apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
-	  have dom: ?dths apply (rule polydivide_aux_real_domintros) 
-	    using ba ds dn' domsp by simp_all
-	  from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{ring_char_0,division_by_zero,field}"]
-	  have " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs s = Ipoly bs ?p'" by simp
-	  hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)" using np nxdn apply simp
-	    by (simp only: funpow_shift1_1) simp
-	  hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] by blast
-	  {assume h1: "polydivide_aux (a,n,p,k,s) = (k',r)"
-	    from polydivide_aux.psimps[OF dom] sz dn' ba ds
-	    have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')"
-	      by (simp add: Let_def)
-	    also have "\<dots> = (k,0\<^sub>p)" using polydivide_aux.psimps[OF domsp] spz by simp
-	    finally have "(k',r) = (k,0\<^sub>p)" using h1 by simp
-	    with sp' ns np nxdn polyadd_0(1)[OF polymul_normh[OF np nxdn]]
-	      polyadd_0(2)[OF polymul_normh[OF np nxdn]] have ?qrths
-	      apply auto
-	      apply (rule exI[where x="?xdn"]) 	      
-	      apply auto
-	      apply (rule polymul_commute)
-	      apply simp_all
-	      done}
-	  with dom have ?ths by blast}
-	ultimately have ?ths by blast }
+        hence headsp': "head s = head ?p'" using ap headp' by simp
+        have nr: "isnpolyh (s -\<^sub>p ?p') 0" using polysub_normh[OF ns np'] by simp
+        from ds degree_polysub_samehead[OF ns np' headsp' degsp']
+        have "degree (s -\<^sub>p ?p') < d \<or> s -\<^sub>p ?p' = 0\<^sub>p" by simp
+        moreover 
+        {assume deglt:"degree (s -\<^sub>p ?p') < d"
+          from  H[rule_format, OF deglt nr,simplified] 
+          have domsp: "?D (a, n, p, k, s -\<^sub>p ?p')" by blast 
+          have dom: ?dths apply (rule polydivide_aux_real_domintros) 
+            using ba ds dn' domsp by simp_all
+          from polydivide_aux.psimps[OF dom] sz dn' ba ds
+          have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')"
+            by (simp add: Let_def)
+          {assume h1: "polydivide_aux (a, n, p, k, s) = (k', r)"
+            from H[rule_format, OF deglt nr, where xa = "k" and xb="k'" and xc="r", simplified]
+              trans[OF eq[symmetric] h1]
+            have kk': "k \<le> k'" and nr:"\<exists>nr. isnpolyh r nr" and dr: "degree r = 0 \<or> degree r < degree p"
+              and q1:"\<exists>q nq. isnpolyh q nq \<and> (a ^\<^sub>p k' - k *\<^sub>p (s -\<^sub>p ?p') = p *\<^sub>p q +\<^sub>p r)" by auto
+            from q1 obtain q n1 where nq: "isnpolyh q n1" 
+              and asp:"a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p') = p *\<^sub>p q +\<^sub>p r"  by blast
+            from nr obtain nr where nr': "isnpolyh r nr" by blast
+            from polymul_normh[OF nakk' ns] have nakks': "isnpolyh (a ^\<^sub>p (k' - k) *\<^sub>p s) 0" by simp
+            from polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]
+            have nq': "isnpolyh (?akk' *\<^sub>p ?xdn +\<^sub>p q) 0" by simp
+            from polyadd_normh[OF polymul_normh[OF np 
+              polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]] nr']
+            have nqr': "isnpolyh (p *\<^sub>p (?akk' *\<^sub>p ?xdn +\<^sub>p q) +\<^sub>p r) 0" by simp 
+            from asp have "\<forall> (bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p')) = 
+              Ipoly bs (p *\<^sub>p q +\<^sub>p r)" by simp
+            hence " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) = 
+              Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r" 
+              by (simp add: ring_simps)
+            hence " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
+              Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (d - n) shift1 1\<^sub>p *\<^sub>p p) 
+              + Ipoly bs p * Ipoly bs q + Ipoly bs r"
+              by (auto simp only: funpow_shift1_1) 
+            hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
+              Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (d - n) shift1 1\<^sub>p) 
+              + Ipoly bs q) + Ipoly bs r" by (simp add: ring_simps)
+            hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
+              Ipoly bs (p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (d - n) shift1 1\<^sub>p) +\<^sub>p q) +\<^sub>p r)" by simp
+            with isnpolyh_unique[OF nakks' nqr']
+            have "a ^\<^sub>p (k' - k) *\<^sub>p s = 
+              p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (d - n) shift1 1\<^sub>p) +\<^sub>p q) +\<^sub>p r" by blast
+            hence ?qths using nq'
+              apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (d - n) shift1 1\<^sub>p) +\<^sub>p q" in exI)
+              apply (rule_tac x="0" in exI) by simp
+            with kk' nr dr have "k \<le> k' \<and> (degree r = 0 \<or> degree r < degree p) \<and> (\<exists>nr. isnpolyh r nr) \<and> ?qths"
+              by blast } hence ?qrths by blast
+          with dom have ?ths by blast} 
+        moreover 
+        {assume spz:"s -\<^sub>p ?p' = 0\<^sub>p"
+          hence domsp: "?D (a, n, p, k, s -\<^sub>p ?p')" 
+            apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
+          have dom: ?dths apply (rule polydivide_aux_real_domintros) 
+            using ba ds dn' domsp by simp_all
+          from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{ring_char_0,division_by_zero,field}"]
+          have " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs s = Ipoly bs ?p'" by simp
+          hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)" using np nxdn apply simp
+            by (simp only: funpow_shift1_1) simp
+          hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] by blast
+          {assume h1: "polydivide_aux (a,n,p,k,s) = (k',r)"
+            from polydivide_aux.psimps[OF dom] sz dn' ba ds
+            have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')"
+              by (simp add: Let_def)
+            also have "\<dots> = (k,0\<^sub>p)" using polydivide_aux.psimps[OF domsp] spz by simp
+            finally have "(k',r) = (k,0\<^sub>p)" using h1 by simp
+            with sp' ns np nxdn polyadd_0(1)[OF polymul_normh[OF np nxdn]]
+              polyadd_0(2)[OF polymul_normh[OF np nxdn]] have ?qrths
+              apply auto
+              apply (rule exI[where x="?xdn"])        
+              apply auto
+              apply (rule polymul_commute)
+              apply simp_all
+              done}
+          with dom have ?ths by blast}
+        ultimately have ?ths by blast }
       moreover
       {assume ba: "?b \<noteq> a"
-	from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np0, simplified ap] ns] 
-	  polymul_normh[OF head_isnpolyh[OF ns] np']]
-	have nth: "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" by(simp add: min_def)
-	have nzths: "a *\<^sub>p s \<noteq> 0\<^sub>p" "?b *\<^sub>p ?p' \<noteq> 0\<^sub>p"
-	  using polymul_eq0_iff[OF head_isnpolyh[OF np0, simplified ap] ns] 
-	    polymul_eq0_iff[OF head_isnpolyh[OF ns] np']head_nz[OF np0] ap pnz sz head_nz[OF ns]
-	    funpow_shift1_nz[OF pnz] by simp_all
-	from polymul_head_polyeq[OF head_isnpolyh[OF np] ns] head_nz[OF np] sz ap head_head[OF np] pnz
-	  polymul_head_polyeq[OF head_isnpolyh[OF ns] np'] head_nz [OF ns] sz funpow_shift1_nz[OF pnz, where n="d - n"]
-	have hdth: "head (a *\<^sub>p s) = head (?b *\<^sub>p ?p')" 
-	  using head_head[OF ns] funpow_shift1_head[OF np pnz]
-	    polymul_commute[OF head_isnpolyh[OF np] head_isnpolyh[OF ns]]
-	  by (simp add: ap)
-	from polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"]
-	  head_nz[OF np] pnz sz ap[symmetric]
-	  funpow_shift1_nz[OF pnz, where n="d - n"]
-	  polymul_degreen[OF head_isnpolyh[OF ns] np', where m="0"]  head_nz[OF ns]
-	  ndp ds[symmetric] dn
-	have degth: "degree (a *\<^sub>p s) = degree (?b *\<^sub>p ?p') "
-	  by (simp add: degree_eq_degreen0[symmetric] funpow_shift1_degree)
-	{assume dth: "degree ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) < d"
-	  have th: "?D (a, n, p, Suc k, (a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))"
-	    using H[rule_format, OF dth nth, simplified] by blast 
-	  have dom: ?dths
-	    using ba ds dn' th apply simp apply (rule polydivide_aux_real_domintros)  
-	    using ba ds dn'  by simp_all
-	  from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np] ns] polymul_normh[OF head_isnpolyh[OF ns]np']]
-	  ap have nasbp': "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" by simp
-	  {assume h1:"polydivide_aux (a,n,p,k,s) = (k', r)"
-	    from h1  polydivide_aux.psimps[OF dom] sz dn' ba ds
-	    have eq:"polydivide_aux (a,n,p,Suc k,(a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = (k',r)"
-	      by (simp add: Let_def)
-	    with H[rule_format, OF dth nasbp', simplified, where xa="Suc k" and xb="k'" and xc="r"]
-	    obtain q nq nr where kk': "Suc k \<le> k'" and nr: "isnpolyh r nr" and nq: "isnpolyh q nq" 
-	      and dr: "degree r = 0 \<or> degree r < degree p"
-	      and qr: "a ^\<^sub>p (k' - Suc k) *\<^sub>p ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = p *\<^sub>p q +\<^sub>p r" by auto
-	    from kk' have kk'':"Suc (k' - Suc k) = k' - k" by arith
-	    {fix bs:: "'a::{ring_char_0,division_by_zero,field} list"
-	      
-	    from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric]
-	    have "Ipoly bs (a ^\<^sub>p (k' - Suc k) *\<^sub>p ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))) = Ipoly bs (p *\<^sub>p q +\<^sub>p r)" by simp
-	    hence "Ipoly bs a ^ (Suc (k' - Suc k)) * Ipoly bs s = Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?p' + Ipoly bs r"
-	      by (simp add: ring_simps power_Suc)
-	    hence "Ipoly bs a ^ (k' - k)  * Ipoly bs s = Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn * Ipoly bs p + Ipoly bs r"
-	      by (simp add:kk'' funpow_shift1_1[where n="d - n" and p="p"])
-	    hence "Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = Ipoly bs p * (Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn) + Ipoly bs r"
-	      by (simp add: ring_simps)}
-	    hence ieq:"\<forall>(bs :: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
-	      Ipoly bs (p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r)" by auto 
-	    let ?q = "q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)"
-	    from polyadd_normh[OF nq polymul_normh[OF polymul_normh[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k"] head_isnpolyh[OF ns], simplified ap ] nxdn]]
-	    have nqw: "isnpolyh ?q 0" by simp
-	    from ieq isnpolyh_unique[OF polymul_normh[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - k"] ns, simplified ap] polyadd_normh[OF polymul_normh[OF np nqw] nr]]
-	    have asth: "(a ^\<^sub>p (k' - k) *\<^sub>p s) = p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r" by blast
-	    from dr kk' nr h1 asth nqw have ?qrths apply simp
-	      apply (rule conjI)
-	      apply (rule exI[where x="nr"], simp)
-	      apply (rule exI[where x="(q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn))"], simp)
-	      apply (rule exI[where x="0"], simp)
-	      done}
-	  hence ?qrths by blast
-	  with dom have ?ths by blast}
-	moreover 
-	{assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p"
-	  hence domsp: "?D (a, n, p, Suc k, a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p'))" 
-	    apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
-	  have dom: ?dths using sz ba dn' ds domsp 
-	    by - (rule polydivide_aux_real_domintros, simp_all)
-	  {fix bs :: "'a::{ring_char_0,division_by_zero,field} list"
-	    from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz
-	  have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'" by simp
-	  hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (?b *\<^sub>p ?xdn) * Ipoly bs p" 
-	    by (simp add: funpow_shift1_1[where n="d - n" and p="p"])
-	  hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" by simp
-	}
-	hence hth: "\<forall> (bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" ..
-	  from hth
-	  have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)" 
-	    using isnpolyh_unique[where ?'a = "'a::{ring_char_0,division_by_zero,field}", OF polymul_normh[OF head_isnpolyh[OF np] ns] 
+        from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np0, simplified ap] ns] 
+          polymul_normh[OF head_isnpolyh[OF ns] np']]
+        have nth: "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" by(simp add: min_def)
+        have nzths: "a *\<^sub>p s \<noteq> 0\<^sub>p" "?b *\<^sub>p ?p' \<noteq> 0\<^sub>p"
+          using polymul_eq0_iff[OF head_isnpolyh[OF np0, simplified ap] ns] 
+            polymul_eq0_iff[OF head_isnpolyh[OF ns] np']head_nz[OF np0] ap pnz sz head_nz[OF ns]
+            funpow_shift1_nz[OF pnz] by simp_all
+        from polymul_head_polyeq[OF head_isnpolyh[OF np] ns] head_nz[OF np] sz ap head_head[OF np] pnz
+          polymul_head_polyeq[OF head_isnpolyh[OF ns] np'] head_nz [OF ns] sz funpow_shift1_nz[OF pnz, where n="d - n"]
+        have hdth: "head (a *\<^sub>p s) = head (?b *\<^sub>p ?p')" 
+          using head_head[OF ns] funpow_shift1_head[OF np pnz]
+            polymul_commute[OF head_isnpolyh[OF np] head_isnpolyh[OF ns]]
+          by (simp add: ap)
+        from polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"]
+          head_nz[OF np] pnz sz ap[symmetric]
+          funpow_shift1_nz[OF pnz, where n="d - n"]
+          polymul_degreen[OF head_isnpolyh[OF ns] np', where m="0"]  head_nz[OF ns]
+          ndp ds[symmetric] dn
+        have degth: "degree (a *\<^sub>p s) = degree (?b *\<^sub>p ?p') "
+          by (simp add: degree_eq_degreen0[symmetric] funpow_shift1_degree)
+        {assume dth: "degree ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) < d"
+          have th: "?D (a, n, p, Suc k, (a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))"
+            using H[rule_format, OF dth nth, simplified] by blast 
+          have dom: ?dths
+            using ba ds dn' th apply simp apply (rule polydivide_aux_real_domintros)  
+            using ba ds dn'  by simp_all
+          from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np] ns] polymul_normh[OF head_isnpolyh[OF ns]np']]
+          ap have nasbp': "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" by simp
+          {assume h1:"polydivide_aux (a,n,p,k,s) = (k', r)"
+            from h1  polydivide_aux.psimps[OF dom] sz dn' ba ds
+            have eq:"polydivide_aux (a,n,p,Suc k,(a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = (k',r)"
+              by (simp add: Let_def)
+            with H[rule_format, OF dth nasbp', simplified, where xa="Suc k" and xb="k'" and xc="r"]
+            obtain q nq nr where kk': "Suc k \<le> k'" and nr: "isnpolyh r nr" and nq: "isnpolyh q nq" 
+              and dr: "degree r = 0 \<or> degree r < degree p"
+              and qr: "a ^\<^sub>p (k' - Suc k) *\<^sub>p ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = p *\<^sub>p q +\<^sub>p r" by auto
+            from kk' have kk'':"Suc (k' - Suc k) = k' - k" by arith
+            {fix bs:: "'a::{ring_char_0,division_by_zero,field} list"
+              
+            from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric]
+            have "Ipoly bs (a ^\<^sub>p (k' - Suc k) *\<^sub>p ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))) = Ipoly bs (p *\<^sub>p q +\<^sub>p r)" by simp
+            hence "Ipoly bs a ^ (Suc (k' - Suc k)) * Ipoly bs s = Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?p' + Ipoly bs r"
+              by (simp add: ring_simps power_Suc)
+            hence "Ipoly bs a ^ (k' - k)  * Ipoly bs s = Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn * Ipoly bs p + Ipoly bs r"
+              by (simp add:kk'' funpow_shift1_1[where n="d - n" and p="p"])
+            hence "Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = Ipoly bs p * (Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn) + Ipoly bs r"
+              by (simp add: ring_simps)}
+            hence ieq:"\<forall>(bs :: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
+              Ipoly bs (p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r)" by auto 
+            let ?q = "q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)"
+            from polyadd_normh[OF nq polymul_normh[OF polymul_normh[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k"] head_isnpolyh[OF ns], simplified ap ] nxdn]]
+            have nqw: "isnpolyh ?q 0" by simp
+            from ieq isnpolyh_unique[OF polymul_normh[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - k"] ns, simplified ap] polyadd_normh[OF polymul_normh[OF np nqw] nr]]
+            have asth: "(a ^\<^sub>p (k' - k) *\<^sub>p s) = p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r" by blast
+            from dr kk' nr h1 asth nqw have ?qrths apply simp
+              apply (rule conjI)
+              apply (rule exI[where x="nr"], simp)
+              apply (rule exI[where x="(q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn))"], simp)
+              apply (rule exI[where x="0"], simp)
+              done}
+          hence ?qrths by blast
+          with dom have ?ths by blast}
+        moreover 
+        {assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p"
+          hence domsp: "?D (a, n, p, Suc k, a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p'))" 
+            apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
+          have dom: ?dths using sz ba dn' ds domsp 
+            by - (rule polydivide_aux_real_domintros, simp_all)
+          {fix bs :: "'a::{ring_char_0,division_by_zero,field} list"
+            from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz
+          have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'" by simp
+          hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (?b *\<^sub>p ?xdn) * Ipoly bs p" 
+            by (simp add: funpow_shift1_1[where n="d - n" and p="p"])
+          hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" by simp
+        }
+        hence hth: "\<forall> (bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" ..
+          from hth
+          have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)" 
+            using isnpolyh_unique[where ?'a = "'a::{ring_char_0,division_by_zero,field}", OF polymul_normh[OF head_isnpolyh[OF np] ns] 
                     polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]],
-	      simplified ap] by simp
-	  {assume h1: "polydivide_aux (a,n,p,k,s) = (k', r)"
-	  from h1 sz ds ba dn' spz polydivide_aux.psimps[OF dom] polydivide_aux.psimps[OF domsp] 
-	  have "(k',r) = (Suc k, 0\<^sub>p)" by (simp add: Let_def)
-	  with h1 np head_isnpolyh[OF np, simplified ap] ns polymul_normh[OF head_isnpolyh[OF ns] nxdn]
-	    polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]] asq
-	  have ?qrths apply (clarsimp simp add: Let_def)
-	    apply (rule exI[where x="?b *\<^sub>p ?xdn"]) apply simp
-	    apply (rule exI[where x="0"], simp)
-	    done}
-	hence ?qrths by blast
-	with dom have ?ths by blast}
-	ultimately have ?ths using  degree_polysub_samehead[OF polymul_normh[OF head_isnpolyh[OF np0, simplified ap] ns] polymul_normh[OF head_isnpolyh[OF ns] np'] hdth degth] polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"]
-	  head_nz[OF np] pnz sz ap[symmetric] ds[symmetric] 
-	  by (simp add: degree_eq_degreen0[symmetric]) blast }
+              simplified ap] by simp
+          {assume h1: "polydivide_aux (a,n,p,k,s) = (k', r)"
+          from h1 sz ds ba dn' spz polydivide_aux.psimps[OF dom] polydivide_aux.psimps[OF domsp] 
+          have "(k',r) = (Suc k, 0\<^sub>p)" by (simp add: Let_def)
+          with h1 np head_isnpolyh[OF np, simplified ap] ns polymul_normh[OF head_isnpolyh[OF ns] nxdn]
+            polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]] asq
+          have ?qrths apply (clarsimp simp add: Let_def)
+            apply (rule exI[where x="?b *\<^sub>p ?xdn"]) apply simp
+            apply (rule exI[where x="0"], simp)
+            done}
+        hence ?qrths by blast
+        with dom have ?ths by blast}
+        ultimately have ?ths using  degree_polysub_samehead[OF polymul_normh[OF head_isnpolyh[OF np0, simplified ap] ns] polymul_normh[OF head_isnpolyh[OF ns] np'] hdth degth] polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"]
+          head_nz[OF np] pnz sz ap[symmetric] ds[symmetric] 
+          by (simp add: degree_eq_degreen0[symmetric]) blast }
       ultimately have ?ths by blast
     }
     ultimately have ?ths by blast}
@@ -1732,7 +1732,7 @@
 recdef isweaknpoly "measure size"
   "isweaknpoly (C c) = True"
   "isweaknpoly (CN c n p) \<longleftrightarrow> isweaknpoly c \<and> isweaknpoly p"
-  "isweaknpoly p = False"	
+  "isweaknpoly p = False"       
 
 lemma isnpolyh_isweaknpoly: "isnpolyh p n0 \<Longrightarrow> isweaknpoly p" 
   by (induct p arbitrary: n0, auto)
diff -r 8fb01a2f9406 -r 02de0317f66f src/HOL/Nominal/Examples/Pattern.thy
--- a/src/HOL/Nominal/Examples/Pattern.thy	Wed Oct 28 00:23:39 2009 +0100
+++ b/src/HOL/Nominal/Examples/Pattern.thy	Wed Oct 28 00:24:38 2009 +0100
@@ -669,17 +669,17 @@
     proof
       assume "x = x' \<and> t = u"
       with PVar PVar' have "PVar x T = ([]::name prm) \<bullet> q \<and>
-	t = ([]::name prm) \<bullet> u \<and>
-	set ([]::name prm) \<subseteq> (supp (PVar x T) \<union> supp q) \<times>
+        t = ([]::name prm) \<bullet> u \<and>
+        set ([]::name prm) \<subseteq> (supp (PVar x T) \<union> supp q) \<times>
           (supp (PVar x T) \<union> supp q)" by simp
       then show ?thesis ..
     next
       assume "x \<noteq> x' \<and> t = [(x, x')] \<bullet> u \<and> x \<sharp> u"
       with PVar PVar' have "PVar x T = [(x, x')] \<bullet> q \<and>
-	t = [(x, x')] \<bullet> u \<and>
-	set [(x, x')] \<subseteq> (supp (PVar x T) \<union> supp q) \<times>
+        t = [(x, x')] \<bullet> u \<and>
+        set [(x, x')] \<subseteq> (supp (PVar x T) \<union> supp q) \<times>
           (supp (PVar x T) \<union> supp q)"
-	by (simp add: perm_swap swap_simps supp_atm perm_type)
+        by (simp add: perm_swap swap_simps supp_atm perm_type)
       then show ?thesis ..
     qed
   next
diff -r 8fb01a2f9406 -r 02de0317f66f src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Oct 28 00:23:39 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Oct 28 00:24:38 2009 +0100
@@ -1140,51 +1140,51 @@
 
 fun mk_Eval_of additional_arguments ((x, T), NONE) names = (x, names)
   | mk_Eval_of additional_arguments ((x, T), SOME mode) names =
-	let
+  let
     val Ts = binder_types T
     (*val argnames = Name.variant_list names
         (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
     val args = map Free (argnames ~~ Ts)
     val (inargs, outargs) = split_smode mode args*)
-		fun mk_split_lambda [] t = lambda (Free (Name.variant names "x", HOLogic.unitT)) t
-			| mk_split_lambda [x] t = lambda x t
-			| mk_split_lambda xs t =
-			let
-				fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t))
-					| mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t))
-			in
-				mk_split_lambda' xs t
-			end;
-  	fun mk_arg (i, T) =
-		  let
-	  	  val vname = Name.variant names ("x" ^ string_of_int i)
-		    val default = Free (vname, T)
-		  in 
-		    case AList.lookup (op =) mode i of
-		      NONE => (([], [default]), [default])
-			  | SOME NONE => (([default], []), [default])
-			  | SOME (SOME pis) =>
-				  case HOLogic.strip_tupleT T of
-						[] => error "pair mode but unit tuple" (*(([default], []), [default])*)
-					| [_] => error "pair mode but not a tuple" (*(([default], []), [default])*)
-					| Ts =>
-					  let
-							val vnames = Name.variant_list names
-								(map (fn j => "x" ^ string_of_int i ^ "p" ^ string_of_int j)
-									(1 upto length Ts))
-							val args = map Free (vnames ~~ Ts)
-							fun split_args (i, arg) (ins, outs) =
-							  if member (op =) pis i then
-							    (arg::ins, outs)
-								else
-								  (ins, arg::outs)
-							val (inargs, outargs) = fold_rev split_args ((1 upto length Ts) ~~ args) ([], [])
-							fun tuple args = if null args then [] else [HOLogic.mk_tuple args]
-						in ((tuple inargs, tuple outargs), args) end
-			end
-		val (inoutargs, args) = split_list (map mk_arg (1 upto (length Ts) ~~ Ts))
+    fun mk_split_lambda [] t = lambda (Free (Name.variant names "x", HOLogic.unitT)) t
+      | mk_split_lambda [x] t = lambda x t
+      | mk_split_lambda xs t =
+      let
+        fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t))
+          | mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t))
+      in
+        mk_split_lambda' xs t
+      end;
+    fun mk_arg (i, T) =
+      let
+        val vname = Name.variant names ("x" ^ string_of_int i)
+        val default = Free (vname, T)
+      in 
+        case AList.lookup (op =) mode i of
+          NONE => (([], [default]), [default])
+        | SOME NONE => (([default], []), [default])
+        | SOME (SOME pis) =>
+          case HOLogic.strip_tupleT T of
+            [] => error "pair mode but unit tuple" (*(([default], []), [default])*)
+          | [_] => error "pair mode but not a tuple" (*(([default], []), [default])*)
+          | Ts =>
+            let
+              val vnames = Name.variant_list names
+                (map (fn j => "x" ^ string_of_int i ^ "p" ^ string_of_int j)
+                  (1 upto length Ts))
+              val args = map Free (vnames ~~ Ts)
+              fun split_args (i, arg) (ins, outs) =
+                if member (op =) pis i then
+                  (arg::ins, outs)
+                else
+                  (ins, arg::outs)
+              val (inargs, outargs) = fold_rev split_args ((1 upto length Ts) ~~ args) ([], [])
+              fun tuple args = if null args then [] else [HOLogic.mk_tuple args]
+            in ((tuple inargs, tuple outargs), args) end
+      end
+    val (inoutargs, args) = split_list (map mk_arg (1 upto (length Ts) ~~ Ts))
     val (inargs, outargs) = pairself flat (split_list inoutargs)
-		val r = PredicateCompFuns.mk_Eval 
+    val r = PredicateCompFuns.mk_Eval 
       (list_comb (x, inargs @ additional_arguments), HOLogic.mk_tuple outargs)
     val t = fold_rev mk_split_lambda args r
   in
@@ -1353,22 +1353,22 @@
 
 fun compile_pred compilation_modifiers compfuns thy all_vs param_vs s T mode moded_cls =
   let
-	  val (Ts1, Ts2) = chop (length (fst mode)) (binder_types T)
+    val (Ts1, Ts2) = chop (length (fst mode)) (binder_types T)
     val (Us1, Us2) = split_smodeT (snd mode) Ts2
     val Ts1' =
       map2 (fn NONE => I | SOME is => #funT_of compilation_modifiers compfuns ([], is)) (fst mode) Ts1
     fun mk_input_term (i, NONE) =
-		    [Free (Name.variant (all_vs @ param_vs) ("x" ^ string_of_int i), nth Ts2 (i - 1))]
-		  | mk_input_term (i, SOME pis) = case HOLogic.strip_tupleT (nth Ts2 (i - 1)) of
-						   [] => error "strange unit input"
-					   | [T] => [Free (Name.variant (all_vs @ param_vs) ("x" ^ string_of_int i), nth Ts2 (i - 1))]
-						 | Ts => let
-							 val vnames = Name.variant_list (all_vs @ param_vs)
-								(map (fn j => "x" ^ string_of_int i ^ "p" ^ string_of_int j)
-									pis)
-						 in if null pis then []
-						   else [HOLogic.mk_tuple (map Free (vnames ~~ map (fn j => nth Ts (j - 1)) pis))] end
-		val in_ts = maps mk_input_term (snd mode)
+        [Free (Name.variant (all_vs @ param_vs) ("x" ^ string_of_int i), nth Ts2 (i - 1))]
+      | mk_input_term (i, SOME pis) = case HOLogic.strip_tupleT (nth Ts2 (i - 1)) of
+               [] => error "strange unit input"
+             | [T] => [Free (Name.variant (all_vs @ param_vs) ("x" ^ string_of_int i), nth Ts2 (i - 1))]
+             | Ts => let
+               val vnames = Name.variant_list (all_vs @ param_vs)
+                (map (fn j => "x" ^ string_of_int i ^ "p" ^ string_of_int j)
+                  pis)
+             in if null pis then []
+               else [HOLogic.mk_tuple (map Free (vnames ~~ map (fn j => nth Ts (j - 1)) pis))] end
+    val in_ts = maps mk_input_term (snd mode)
     val params = map2 (fn s => fn T => Free (s, T)) param_vs Ts1'
     val additional_arguments = #additional_arguments compilation_modifiers (all_vs @ param_vs)
     val cl_ts =
@@ -1389,7 +1389,7 @@
 (* special setup for simpset *)                  
 val HOL_basic_ss' = HOL_basic_ss addsimps (@{thms "HOL.simp_thms"} @ [@{thm Pair_eq}])
   setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
-	setSolver (mk_solver "True_solver" (fn _ => rtac @{thm TrueI}))
+  setSolver (mk_solver "True_solver" (fn _ => rtac @{thm TrueI}))
 
 (* Definition of executable functions and their intro and elim rules *)
 
@@ -1405,29 +1405,29 @@
   val funtrm = Const (mode_id, funT)
   val (Ts1, Ts2) = chop (length iss) Ts;
   val Ts1' = map2 (fn NONE => I | SOME is => funT_of (PredicateCompFuns.compfuns) ([], is)) iss Ts1
-	val param_names = Name.variant_list []
+  val param_names = Name.variant_list []
     (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts1)));
   val params = map Free (param_names ~~ Ts1')
-	fun mk_args (i, T) argnames =
+  fun mk_args (i, T) argnames =
     let
-		  val vname = Name.variant (param_names @ argnames) ("x" ^ string_of_int (length Ts1' + i))
-		  val default = (Free (vname, T), vname :: argnames)
-	  in
-  	  case AList.lookup (op =) is i of
-						 NONE => default
-					 | SOME NONE => default
-        	 | SOME (SOME pis) =>
-					   case HOLogic.strip_tupleT T of
-						   [] => default
-					   | [_] => default
-						 | Ts => 
-						let
-							val vnames = Name.variant_list (param_names @ argnames)
-								(map (fn j => "x" ^ string_of_int (length Ts1' + i) ^ "p" ^ string_of_int j)
-									(1 upto (length Ts)))
-						 in (HOLogic.mk_tuple (map Free (vnames ~~ Ts)), vnames  @ argnames) end
-		end
-	val (args, argnames) = fold_map mk_args (1 upto (length Ts2) ~~ Ts2) []
+      val vname = Name.variant (param_names @ argnames) ("x" ^ string_of_int (length Ts1' + i))
+      val default = (Free (vname, T), vname :: argnames)
+    in
+      case AList.lookup (op =) is i of
+             NONE => default
+           | SOME NONE => default
+           | SOME (SOME pis) =>
+             case HOLogic.strip_tupleT T of
+               [] => default
+             | [_] => default
+             | Ts => 
+            let
+              val vnames = Name.variant_list (param_names @ argnames)
+                (map (fn j => "x" ^ string_of_int (length Ts1' + i) ^ "p" ^ string_of_int j)
+                  (1 upto (length Ts)))
+             in (HOLogic.mk_tuple (map Free (vnames ~~ Ts)), vnames  @ argnames) end
+    end
+  val (args, argnames) = fold_map mk_args (1 upto (length Ts2) ~~ Ts2) []
   val (inargs, outargs) = split_smode is args
   val param_names' = Name.variant_list (param_names @ argnames)
     (map (fn i => "p" ^ string_of_int i) (1 upto (length iss)))
@@ -1443,7 +1443,7 @@
                    HOLogic.mk_tuple outargs))
   val introtrm = Logic.list_implies (predpropI :: param_eqs, funpropI)
   val simprules = [defthm, @{thm eval_pred},
-	  @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]
+    @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]
   val unfolddef_tac = Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps simprules) 1
   val introthm = Goal.prove (ProofContext.init thy) (argnames @ param_names @ param_names' @ ["y"]) [] introtrm (fn {...} => unfolddef_tac)
   val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT));
@@ -1466,30 +1466,30 @@
   end;
 
 fun split_tupleT is T =
-	let
-		fun split_tuple' _ _ [] = ([], [])
-			| split_tuple' is i (T::Ts) =
-			(if i mem is then apfst else apsnd) (cons T)
-				(split_tuple' is (i+1) Ts)
-	in
-	  split_tuple' is 1 (HOLogic.strip_tupleT T)
+  let
+    fun split_tuple' _ _ [] = ([], [])
+      | split_tuple' is i (T::Ts) =
+      (if i mem is then apfst else apsnd) (cons T)
+        (split_tuple' is (i+1) Ts)
+  in
+    split_tuple' is 1 (HOLogic.strip_tupleT T)
   end
-	
+  
 fun mk_arg xin xout pis T =
   let
-	  val n = length (HOLogic.strip_tupleT T)
-		val ni = length pis
-	  fun mk_proj i j t =
-		  (if i = j then I else HOLogic.mk_fst)
-			  (funpow (i - 1) HOLogic.mk_snd t)
-	  fun mk_arg' i (si, so) = if i mem pis then
-		    (mk_proj si ni xin, (si+1, so))
-		  else
-			  (mk_proj so (n - ni) xout, (si, so+1))
-	  val (args, _) = fold_map mk_arg' (1 upto n) (1, 1)
-	in
-	  HOLogic.mk_tuple args
-	end
+    val n = length (HOLogic.strip_tupleT T)
+    val ni = length pis
+    fun mk_proj i j t =
+      (if i = j then I else HOLogic.mk_fst)
+        (funpow (i - 1) HOLogic.mk_snd t)
+    fun mk_arg' i (si, so) = if i mem pis then
+        (mk_proj si ni xin, (si+1, so))
+      else
+        (mk_proj so (n - ni) xout, (si, so+1))
+    val (args, _) = fold_map mk_arg' (1 upto n) (1, 1)
+  in
+    HOLogic.mk_tuple args
+  end
 
 fun create_definitions preds (name, modes) thy =
   let
@@ -1505,37 +1505,37 @@
       val funT = (Ts1' @ Us1) ---> (mk_predT compfuns (HOLogic.mk_tupleT Us2))
       val names = Name.variant_list []
         (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
-			(* old *)
-			(*
-		  val xs = map Free (names ~~ (Ts1' @ Ts2))
+      (* old *)
+      (*
+      val xs = map Free (names ~~ (Ts1' @ Ts2))
       val (xparams, xargs) = chop (length iss) xs
       val (xins, xouts) = split_smode is xargs
-			*)
-			(* new *)
-			val param_names = Name.variant_list []
-			  (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts1')))
-		  val xparams = map Free (param_names ~~ Ts1')
+      *)
+      (* new *)
+      val param_names = Name.variant_list []
+        (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts1')))
+      val xparams = map Free (param_names ~~ Ts1')
       fun mk_vars (i, T) names =
-			  let
-				  val vname = Name.variant names ("x" ^ string_of_int (length Ts1' + i))
-				in
-					case AList.lookup (op =) is i of
-						 NONE => ((([], [Free (vname, T)]), Free (vname, T)), vname :: names)
-					 | SOME NONE => ((([Free (vname, T)], []), Free (vname, T)), vname :: names)
-        	 | SOME (SOME pis) =>
-					   let
-						   val (Tins, Touts) = split_tupleT pis T
-							 val name_in = Name.variant names ("x" ^ string_of_int (length Ts1' + i) ^ "in")
-							 val name_out = Name.variant names ("x" ^ string_of_int (length Ts1' + i) ^ "out")
-						   val xin = Free (name_in, HOLogic.mk_tupleT Tins)
-							 val xout = Free (name_out, HOLogic.mk_tupleT Touts)
-							 val xarg = mk_arg xin xout pis T
-						 in (((if null Tins then [] else [xin], if null Touts then [] else [xout]), xarg), name_in :: name_out :: names) end
-						 end
-   	  val (xinoutargs, names) = fold_map mk_vars ((1 upto (length Ts2)) ~~ Ts2) param_names
+        let
+          val vname = Name.variant names ("x" ^ string_of_int (length Ts1' + i))
+        in
+          case AList.lookup (op =) is i of
+             NONE => ((([], [Free (vname, T)]), Free (vname, T)), vname :: names)
+           | SOME NONE => ((([Free (vname, T)], []), Free (vname, T)), vname :: names)
+           | SOME (SOME pis) =>
+             let
+               val (Tins, Touts) = split_tupleT pis T
+               val name_in = Name.variant names ("x" ^ string_of_int (length Ts1' + i) ^ "in")
+               val name_out = Name.variant names ("x" ^ string_of_int (length Ts1' + i) ^ "out")
+               val xin = Free (name_in, HOLogic.mk_tupleT Tins)
+               val xout = Free (name_out, HOLogic.mk_tupleT Touts)
+               val xarg = mk_arg xin xout pis T
+             in (((if null Tins then [] else [xin], if null Touts then [] else [xout]), xarg), name_in :: name_out :: names) end
+             end
+      val (xinoutargs, names) = fold_map mk_vars ((1 upto (length Ts2)) ~~ Ts2) param_names
       val (xinout, xargs) = split_list xinoutargs
-			val (xins, xouts) = pairself flat (split_list xinout)
-			val (xparams', names') = fold_map (mk_Eval_of []) ((xparams ~~ Ts1) ~~ iss) names
+      val (xins, xouts) = pairself flat (split_list xinout)
+      val (xparams', names') = fold_map (mk_Eval_of []) ((xparams ~~ Ts1) ~~ iss) names
       fun mk_split_lambda [] t = lambda (Free (Name.variant names' "x", HOLogic.unitT)) t
         | mk_split_lambda [x] t = lambda x t
         | mk_split_lambda xs t =
@@ -1555,7 +1555,7 @@
       val (intro, elim) =
         create_intro_elim_rule mode definition mode_cname funT (Const (name, T)) thy'
       in thy'
-			  |> add_predfun name mode (mode_cname, definition, intro, elim)
+        |> add_predfun name mode (mode_cname, definition, intro, elim)
         |> PureThy.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd
         |> PureThy.store_thm (Binding.name (mode_cbasename ^ "E"), elim)  |> snd
         |> Theory.checkpoint
@@ -1635,7 +1635,7 @@
       Const (name, T) => simp_tac (HOL_basic_ss addsimps 
          ([@{thm eval_pred}, (predfun_definition_of thy name mode),
          @{thm "split_eta"}, @{thm "split_beta"}, @{thm "fst_conv"},
-				 @{thm "snd_conv"}, @{thm pair_collapse}, @{thm "Product_Type.split_conv"}])) 1
+         @{thm "snd_conv"}, @{thm pair_collapse}, @{thm "Product_Type.split_conv"}])) 1
     | Free _ => TRY (rtac @{thm refl} 1)
     | Abs _ => error "prove_param: No valid parameter term"
   in
@@ -1669,12 +1669,12 @@
         THEN (REPEAT_DETERM (atac 1))
       end
   | _ => rtac @{thm bindI} 1
-	  THEN asm_full_simp_tac
-		  (HOL_basic_ss' addsimps [@{thm "split_eta"}, @{thm "split_beta"}, @{thm "fst_conv"},
-				 @{thm "snd_conv"}, @{thm pair_collapse}]) 1
-	  THEN (atac 1)
-	  THEN print_tac "after prove parameter call"
-		
+    THEN asm_full_simp_tac
+      (HOL_basic_ss' addsimps [@{thm "split_eta"}, @{thm "split_beta"}, @{thm "fst_conv"},
+         @{thm "snd_conv"}, @{thm pair_collapse}]) 1
+    THEN (atac 1)
+    THEN print_tac "after prove parameter call"
+    
 
 fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st; 
 
@@ -1725,9 +1725,9 @@
     val (in_ts, clause_out_ts) = split_smode is ts;
     fun prove_prems out_ts [] =
       (prove_match thy out_ts)
-			THEN print_tac "before simplifying assumptions"
+      THEN print_tac "before simplifying assumptions"
       THEN asm_full_simp_tac HOL_basic_ss' 1
-			THEN print_tac "before single intro rule"
+      THEN print_tac "before single intro rule"
       THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
     | prove_prems out_ts ((p, mode as Mode ((iss, is), _, param_modes)) :: ps) =
       let
@@ -1793,7 +1793,7 @@
     val pred_case_rule = the_elim_of thy pred
   in
     REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"}))
-		THEN print_tac' options "before applying elim rule"
+    THEN print_tac' options "before applying elim rule"
     THEN etac (predfun_elim_of thy pred mode) 1
     THEN etac pred_case_rule 1
     THEN (EVERY (map
@@ -1911,7 +1911,7 @@
       THEN (print_tac "state before assumption matching")
       THEN (REPEAT (atac 1 ORELSE 
          (CHANGED (asm_full_simp_tac (HOL_basic_ss' addsimps
-					 [@{thm split_eta}, @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]) 1)
+           [@{thm split_eta}, @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]) 1)
           THEN print_tac "state after simp_tac:"))))
     | prove_prems2 out_ts ((p, mode as Mode ((iss, is), _, param_modes)) :: ps) =
       let
@@ -1987,7 +1987,7 @@
       (if not (skip_proof options) then
         (fn _ =>
         rtac @{thm pred_iffI} 1
-				THEN print_tac' options "after pred_iffI"
+        THEN print_tac' options "after pred_iffI"
         THEN prove_one_direction options thy clauses preds modes pred mode moded_clauses
         THEN print_tac' options "proved one direction"
         THEN prove_other_direction options thy modes pred mode moded_clauses