eliminated hard tabulators, guessing at each author's individual tab-width;
authorwenzelm
Wed Oct 28 00:24:38 2009 +0100 (2009-10-28)
changeset 3326802de0317f66f
parent 33267 8fb01a2f9406
child 33272 73a0c804840f
child 33276 f2bc8bc6e73d
child 33326 7d0288d90535
eliminated hard tabulators, guessing at each author's individual tab-width;
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Decision_Procs/Polynomial_List.thy
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
src/HOL/Nominal/Examples/Pattern.thy
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Oct 28 00:23:39 2009 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Oct 28 00:24:38 2009 +0100
     1.3 @@ -35,7 +35,7 @@
     1.4    "Itm vs bs (Add a b) = Itm vs bs a + Itm vs bs b"
     1.5    "Itm vs bs (Sub a b) = Itm vs bs a - Itm vs bs b"
     1.6    "Itm vs bs (Mul c a) = (Ipoly vs c) * Itm vs bs a"
     1.7 -  "Itm vs bs (CNP n c t) = (Ipoly vs c)*(bs!n) + Itm vs bs t"	
     1.8 +  "Itm vs bs (CNP n c t) = (Ipoly vs c)*(bs!n) + Itm vs bs t"   
     1.9  
    1.10  
    1.11  fun allpolys:: "(poly \<Rightarrow> bool) \<Rightarrow> tm \<Rightarrow> bool"  where
    1.12 @@ -153,14 +153,14 @@
    1.13        {assume mxs: "m \<le> length (x#xs)" hence ?case using prems by (cases m, auto)}
    1.14        moreover
    1.15        {assume mxs: "\<not> (m \<le> length (x#xs))" 
    1.16 -	have th: "length (removen n (x#xs)) = length xs" 
    1.17 -	  using removen_length[where n="n" and xs="x#xs"] nxs by simp
    1.18 -	with mxs have mxs':"m \<ge> length (removen n (x#xs))" by auto
    1.19 -	hence "(removen n (x#xs))!m = [] ! (m - length xs)" 
    1.20 -	  using th nth_length_exceeds[OF mxs'] by auto
    1.21 -	hence th: "(removen n (x#xs))!m = [] ! (m - (length (x#xs) - 1))" 
    1.22 -	  by auto
    1.23 -	hence ?case using nxs mln mxs by auto }
    1.24 +        have th: "length (removen n (x#xs)) = length xs" 
    1.25 +          using removen_length[where n="n" and xs="x#xs"] nxs by simp
    1.26 +        with mxs have mxs':"m \<ge> length (removen n (x#xs))" by auto
    1.27 +        hence "(removen n (x#xs))!m = [] ! (m - length xs)" 
    1.28 +          using th nth_length_exceeds[OF mxs'] by auto
    1.29 +        hence th: "(removen n (x#xs))!m = [] ! (m - (length (x#xs) - 1))" 
    1.30 +          by auto
    1.31 +        hence ?case using nxs mln mxs by auto }
    1.32        ultimately have ?case by blast
    1.33      }
    1.34      ultimately have ?case by blast
    1.35 @@ -443,7 +443,7 @@
    1.36    "fmsize (A p) = 4+ fmsize p"
    1.37    "fmsize p = 1"
    1.38    (* several lemmas about fmsize *)
    1.39 -lemma fmsize_pos: "fmsize p > 0"	
    1.40 +lemma fmsize_pos: "fmsize p > 0"        
    1.41  by (induct p rule: fmsize.induct) simp_all
    1.42  
    1.43    (* Semantics of formulae (fm) *)
    1.44 @@ -1393,16 +1393,16 @@
    1.45        using eq[OF nc(2), of vs] eq[OF nc(1), of vs] by auto}
    1.46    moreover {assume cp: "?c > 0"
    1.47      {fix x assume xz: "x < -?e / ?c" hence "?c * x < - ?e"
    1.48 -	using pos_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
    1.49 +        using pos_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
    1.50        hence "?c * x + ?e < 0" by simp
    1.51        hence "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Eq (CNP 0 c e)))"
    1.52 -	using eqs tmbound0_I[OF nbe, where b="y" and b'="x" and vs=vs and bs=bs] by auto} hence ?case by auto}
    1.53 +        using eqs tmbound0_I[OF nbe, where b="y" and b'="x" and vs=vs and bs=bs] by auto} hence ?case by auto}
    1.54    moreover {assume cp: "?c < 0"
    1.55      {fix x assume xz: "x < -?e / ?c" hence "?c * x > - ?e"
    1.56 -	using neg_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
    1.57 +        using neg_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
    1.58        hence "?c * x + ?e > 0" by simp
    1.59        hence "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Eq (CNP 0 c e)))"
    1.60 -	using tmbound0_I[OF nbe, where b="y" and b'="x"] eqs by auto} hence ?case by auto}
    1.61 +        using tmbound0_I[OF nbe, where b="y" and b'="x"] eqs by auto} hence ?case by auto}
    1.62    ultimately show ?case by blast
    1.63  next
    1.64    case (4 c e)  hence nbe: "tmbound0 e" by simp
    1.65 @@ -1414,16 +1414,16 @@
    1.66    moreover {assume "?c = 0" hence ?case using eqs by auto}
    1.67    moreover {assume cp: "?c > 0"
    1.68      {fix x assume xz: "x < -?e / ?c" hence "?c * x < - ?e"
    1.69 -	using pos_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
    1.70 +        using pos_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
    1.71        hence "?c * x + ?e < 0" by simp
    1.72        hence "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (NEq (CNP 0 c e)))"
    1.73 -	using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto}
    1.74 +        using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto}
    1.75    moreover {assume cp: "?c < 0"
    1.76      {fix x assume xz: "x < -?e / ?c" hence "?c * x > - ?e"
    1.77 -	using neg_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
    1.78 +        using neg_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
    1.79        hence "?c * x + ?e > 0" by simp
    1.80        hence "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (NEq (CNP 0 c e)))"
    1.81 -	using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto}
    1.82 +        using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto}
    1.83    ultimately show ?case by blast
    1.84  next
    1.85    case (5 c e)  hence nbe: "tmbound0 e" by simp
    1.86 @@ -1436,16 +1436,16 @@
    1.87    moreover {assume "?c = 0" hence ?case using eqs by auto}
    1.88    moreover {assume cp: "?c > 0"
    1.89      {fix x assume xz: "x < -?e / ?c" hence "?c * x < - ?e"
    1.90 -	using pos_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
    1.91 +        using pos_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
    1.92        hence "?c * x + ?e < 0" by simp
    1.93        hence "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Lt (CNP 0 c e)))"
    1.94 -	using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
    1.95 +        using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
    1.96    moreover {assume cp: "?c < 0"
    1.97      {fix x assume xz: "x < -?e / ?c" hence "?c * x > - ?e"
    1.98 -	using neg_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
    1.99 +        using neg_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
   1.100        hence "?c * x + ?e > 0" by simp
   1.101        hence "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Lt (CNP 0 c e)))"
   1.102 -	using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] cp by auto} hence ?case by auto}
   1.103 +        using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] cp by auto} hence ?case by auto}
   1.104    ultimately show ?case by blast
   1.105  next
   1.106    case (6 c e)  hence nbe: "tmbound0 e" by simp
   1.107 @@ -1458,16 +1458,16 @@
   1.108    moreover {assume "?c = 0" hence ?case using eqs by auto}
   1.109    moreover {assume cp: "?c > 0"
   1.110      {fix x assume xz: "x < -?e / ?c" hence "?c * x < - ?e"
   1.111 -	using pos_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
   1.112 +        using pos_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
   1.113        hence "?c * x + ?e < 0" by simp
   1.114        hence "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Le (CNP 0 c e)))"
   1.115 -	using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
   1.116 +        using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
   1.117    moreover {assume cp: "?c < 0"
   1.118      {fix x assume xz: "x < -?e / ?c" hence "?c * x > - ?e"
   1.119 -	using neg_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
   1.120 +        using neg_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
   1.121        hence "?c * x + ?e > 0" by simp
   1.122        hence "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Le (CNP 0 c e)))"
   1.123 -	using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
   1.124 +        using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
   1.125    ultimately show ?case by blast
   1.126  qed (auto)
   1.127  
   1.128 @@ -1489,16 +1489,16 @@
   1.129        using eq[OF nc(2), of vs] eq[OF nc(1), of vs] by auto}
   1.130    moreover {assume cp: "?c > 0"
   1.131      {fix x assume xz: "x > -?e / ?c" hence "?c * x > - ?e" 
   1.132 -	using pos_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
   1.133 +        using pos_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
   1.134        hence "?c * x + ?e > 0" by simp
   1.135        hence "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Eq (CNP 0 c e)))"
   1.136 -	using eqs tmbound0_I[OF nbe, where b="y" and b'="x" and vs=vs and bs=bs] by auto} hence ?case by auto}
   1.137 +        using eqs tmbound0_I[OF nbe, where b="y" and b'="x" and vs=vs and bs=bs] by auto} hence ?case by auto}
   1.138    moreover {assume cp: "?c < 0"
   1.139      {fix x assume xz: "x > -?e / ?c" hence "?c * x < - ?e"
   1.140 -	using neg_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
   1.141 +        using neg_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
   1.142        hence "?c * x + ?e < 0" by simp
   1.143        hence "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Eq (CNP 0 c e)))"
   1.144 -	using tmbound0_I[OF nbe, where b="y" and b'="x"] eqs by auto} hence ?case by auto}
   1.145 +        using tmbound0_I[OF nbe, where b="y" and b'="x"] eqs by auto} hence ?case by auto}
   1.146    ultimately show ?case by blast
   1.147  next
   1.148    case (4 c e)  hence nbe: "tmbound0 e" by simp
   1.149 @@ -1510,16 +1510,16 @@
   1.150    moreover {assume "?c = 0" hence ?case using eqs by auto}
   1.151    moreover {assume cp: "?c > 0"
   1.152      {fix x assume xz: "x > -?e / ?c" hence "?c * x > - ?e"
   1.153 -	using pos_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
   1.154 +        using pos_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
   1.155        hence "?c * x + ?e > 0" by simp
   1.156        hence "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (NEq (CNP 0 c e)))"
   1.157 -	using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto}
   1.158 +        using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto}
   1.159    moreover {assume cp: "?c < 0"
   1.160      {fix x assume xz: "x > -?e / ?c" hence "?c * x < - ?e"
   1.161 -	using neg_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
   1.162 +        using neg_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
   1.163        hence "?c * x + ?e < 0" by simp
   1.164        hence "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (NEq (CNP 0 c e)))"
   1.165 -	using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto}
   1.166 +        using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto}
   1.167    ultimately show ?case by blast
   1.168  next
   1.169    case (5 c e)  hence nbe: "tmbound0 e" by simp
   1.170 @@ -1532,16 +1532,16 @@
   1.171    moreover {assume "?c = 0" hence ?case using eqs by auto}
   1.172    moreover {assume cp: "?c > 0"
   1.173      {fix x assume xz: "x > -?e / ?c" hence "?c * x > - ?e"
   1.174 -	using pos_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
   1.175 +        using pos_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
   1.176        hence "?c * x + ?e > 0" by simp
   1.177        hence "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Lt (CNP 0 c e)))"
   1.178 -	using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
   1.179 +        using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
   1.180    moreover {assume cp: "?c < 0"
   1.181      {fix x assume xz: "x > -?e / ?c" hence "?c * x < - ?e"
   1.182 -	using neg_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
   1.183 +        using neg_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
   1.184        hence "?c * x + ?e < 0" by simp
   1.185        hence "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Lt (CNP 0 c e)))"
   1.186 -	using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] cp by auto} hence ?case by auto}
   1.187 +        using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] cp by auto} hence ?case by auto}
   1.188    ultimately show ?case by blast
   1.189  next
   1.190    case (6 c e)  hence nbe: "tmbound0 e" by simp
   1.191 @@ -1554,16 +1554,16 @@
   1.192    moreover {assume "?c = 0" hence ?case using eqs by auto}
   1.193    moreover {assume cp: "?c > 0"
   1.194      {fix x assume xz: "x > -?e / ?c" hence "?c * x > - ?e"
   1.195 -	using pos_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
   1.196 +        using pos_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
   1.197        hence "?c * x + ?e > 0" by simp
   1.198        hence "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Le (CNP 0 c e)))"
   1.199 -	using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
   1.200 +        using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
   1.201    moreover {assume cp: "?c < 0"
   1.202      {fix x assume xz: "x > -?e / ?c" hence "?c * x < - ?e"
   1.203 -	using neg_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
   1.204 +        using neg_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
   1.205        hence "?c * x + ?e < 0" by simp
   1.206        hence "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Le (CNP 0 c e)))"
   1.207 -	using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
   1.208 +        using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
   1.209    ultimately show ?case by blast
   1.210  qed (auto)
   1.211  
   1.212 @@ -1698,10 +1698,10 @@
   1.213    {assume c: "?N c > 0"
   1.214        from px pos_less_divide_eq[OF c, where a="x" and b="-?Nt x s"]  
   1.215        have px': "x < - ?Nt x s / ?N c" 
   1.216 -	by (auto simp add: not_less ring_simps) 
   1.217 +        by (auto simp add: not_less ring_simps) 
   1.218      {assume y: "y < - ?Nt x s / ?N c" 
   1.219        hence "y * ?N c < - ?Nt x s"
   1.220 -	by (simp add: pos_less_divide_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
   1.221 +        by (simp add: pos_less_divide_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
   1.222        hence "?N c * y + ?Nt x s < 0" by (simp add: ring_simps)
   1.223        hence ?case using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"] by simp}
   1.224      moreover
   1.225 @@ -1715,10 +1715,10 @@
   1.226    {assume c: "?N c < 0"
   1.227        from px neg_divide_less_eq[OF c, where a="x" and b="-?Nt x s"]  
   1.228        have px': "x > - ?Nt x s / ?N c" 
   1.229 -	by (auto simp add: not_less ring_simps) 
   1.230 +        by (auto simp add: not_less ring_simps) 
   1.231      {assume y: "y > - ?Nt x s / ?N c" 
   1.232        hence "y * ?N c < - ?Nt x s"
   1.233 -	by (simp add: neg_divide_less_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
   1.234 +        by (simp add: neg_divide_less_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
   1.235        hence "?N c * y + ?Nt x s < 0" by (simp add: ring_simps)
   1.236        hence ?case using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"] by simp}
   1.237      moreover
   1.238 @@ -1746,7 +1746,7 @@
   1.239        have px': "x <= - ?Nt x s / ?N c" by (simp add: not_less ring_simps) 
   1.240      {assume y: "y < - ?Nt x s / ?N c" 
   1.241        hence "y * ?N c < - ?Nt x s"
   1.242 -	by (simp add: pos_less_divide_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
   1.243 +        by (simp add: pos_less_divide_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
   1.244        hence "?N c * y + ?Nt x s < 0" by (simp add: ring_simps)
   1.245        hence ?case using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"] by simp}
   1.246      moreover
   1.247 @@ -1762,7 +1762,7 @@
   1.248        have px': "x >= - ?Nt x s / ?N c" by (simp add: ring_simps) 
   1.249      {assume y: "y > - ?Nt x s / ?N c" 
   1.250        hence "y * ?N c < - ?Nt x s"
   1.251 -	by (simp add: neg_divide_less_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
   1.252 +        by (simp add: neg_divide_less_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
   1.253        hence "?N c * y + ?Nt x s < 0" by (simp add: ring_simps)
   1.254        hence ?case using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"] by simp}
   1.255      moreover
   1.256 @@ -1899,8 +1899,8 @@
   1.257      moreover{
   1.258        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"
   1.259        then obtain t1 and t2 where t1M: "t1 \<in> ?M" and t2M: "t2\<in> ?M" 
   1.260 -	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"
   1.261 -	by blast
   1.262 +        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"
   1.263 +        by blast
   1.264        from t1M have "\<exists> (t1n,t1u) \<in> ?U. t1 = - ?Nt a t1u / ?N t1n" by auto
   1.265        then obtain "t1u" "t1n" where t1uU: "(t1n,t1u) \<in> ?U" and t1u: "t1 = - ?Nt a t1u / ?N t1n" by blast
   1.266        from t2M have "\<exists> (t2n,t2u) \<in> ?U. t2 = - ?Nt a t2u / ?N t2n" by auto
   1.267 @@ -2236,7 +2236,7 @@
   1.268        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
   1.269      also have "\<dots> \<longleftrightarrow> ?a*?t -  (1 + 1)*?c *?r < 0" 
   1.270        using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c''] less_imp_neq[OF c''] c''
   1.271 -	by (simp add: ring_simps diff_divide_distrib del:  left_distrib)
   1.272 +        by (simp add: ring_simps diff_divide_distrib del:  left_distrib)
   1.273      finally have ?thesis using c d nc nd 
   1.274        apply(simp add: r[of "- (?t / ((1 + 1)*?c))"] msubstlt_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm)
   1.275        apply (simp only: one_add_one_is_two[symmetric] of_int_add)
   1.276 @@ -2270,7 +2270,7 @@
   1.277        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
   1.278      also have "\<dots> \<longleftrightarrow> ?a*?s -  (1 + 1)*?d *?r < 0" 
   1.279        using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d''] less_imp_neq[OF d''] d''
   1.280 -	by (simp add: ring_simps diff_divide_distrib del:  left_distrib)
   1.281 +        by (simp add: ring_simps diff_divide_distrib del:  left_distrib)
   1.282      finally have ?thesis using c d nc nd 
   1.283        apply(simp add: r[of "- (?s / ((1 + 1)*?d))"] msubstlt_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm)
   1.284        apply (simp only: one_add_one_is_two[symmetric] of_int_add)
   1.285 @@ -2392,7 +2392,7 @@
   1.286        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
   1.287      also have "\<dots> \<longleftrightarrow> ?a*?t -  (1 + 1)*?c *?r <= 0" 
   1.288        using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c''] less_imp_neq[OF c''] c''
   1.289 -	by (simp add: ring_simps diff_divide_distrib del:  left_distrib)
   1.290 +        by (simp add: ring_simps diff_divide_distrib del:  left_distrib)
   1.291      finally have ?thesis using c d nc nd 
   1.292        apply(simp add: r[of "- (?t / ((1 + 1)*?c))"] msubstle_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm)
   1.293        apply (simp only: one_add_one_is_two[symmetric] of_int_add)
   1.294 @@ -2426,7 +2426,7 @@
   1.295        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
   1.296      also have "\<dots> \<longleftrightarrow> ?a*?s -  (1 + 1)*?d *?r <= 0" 
   1.297        using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d''] less_imp_neq[OF d''] d''
   1.298 -	by (simp add: ring_simps diff_divide_distrib del:  left_distrib)
   1.299 +        by (simp add: ring_simps diff_divide_distrib del:  left_distrib)
   1.300      finally have ?thesis using c d nc nd 
   1.301        apply(simp add: r[of "- (?s / ((1 + 1)*?d))"] msubstle_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm)
   1.302        apply (simp only: one_add_one_is_two[symmetric] of_int_add)
   1.303 @@ -2638,8 +2638,8 @@
   1.304      moreover
   1.305      {assume z: "?c \<noteq> 0" "?d \<noteq> 0"
   1.306        from z have ?F using ct
   1.307 -	apply - apply (rule bexI[where x = "(c,t)"], simp_all)
   1.308 -	by (rule bexI[where x = "(d,s)"], simp_all)
   1.309 +        apply - apply (rule bexI[where x = "(c,t)"], simp_all)
   1.310 +        by (rule bexI[where x = "(d,s)"], simp_all)
   1.311        hence ?D by blast}
   1.312      ultimately have ?D by auto}
   1.313    ultimately show "?D" by blast
   1.314 @@ -2799,17 +2799,17 @@
   1.315        from H(1) th have "isnpoly n" by blast
   1.316        hence nn: "isnpoly (n *\<^sub>p (C (-2,1)))" by (simp_all add: polymul_norm n2)
   1.317        have nn': "allpolys isnpoly (CP (~\<^sub>p (n *\<^sub>p C (-2, 1))))"
   1.318 -	by (simp add: polyneg_norm nn)
   1.319 +        by (simp add: polyneg_norm nn)
   1.320        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 
   1.321 -	by (auto simp add: msubst2_def lt zero_less_mult_iff mult_less_0_iff)
   1.322 +        by (auto simp add: msubst2_def lt zero_less_mult_iff mult_less_0_iff)
   1.323        from msubst2[OF lp nn nn2(1), of x bs t]
   1.324        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"
   1.325 -	using H(2) nn2 by (simp add: of_int_minus2 del: minus_add_distrib)}
   1.326 +        using H(2) nn2 by (simp add: of_int_minus2 del: minus_add_distrib)}
   1.327      moreover
   1.328      {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"
   1.329        from H(1) th have "isnpoly n" by blast
   1.330        hence nn: "isnpoly (n *\<^sub>p (C (-2,1)))" "\<lparr>n *\<^sub>p(C (-2,1)) \<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
   1.331 -	using H(2) by (simp_all add: polymul_norm n2)
   1.332 +        using H(2) by (simp_all add: polymul_norm n2)
   1.333        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)}
   1.334      ultimately show ?thesis by blast
   1.335    qed
   1.336 @@ -2820,21 +2820,21 @@
   1.337       "Ifm vs (x#bs) (msubst2 p (C (-2, 1) *\<^sub>p c*\<^sub>p d) (Add (Mul d t) (Mul c s)))"
   1.338        from H(1,2) th have "isnpoly c" "isnpoly d" by blast+
   1.339        hence nn: "isnpoly (C (-2, 1) *\<^sub>p c*\<^sub>p d)" 
   1.340 -	by (simp_all add: polymul_norm n2)
   1.341 +        by (simp_all add: polymul_norm n2)
   1.342        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)))"
   1.343 -	by (simp_all add: polyneg_norm nn)
   1.344 +        by (simp_all add: polyneg_norm nn)
   1.345        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"
   1.346 -	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)
   1.347 +        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)
   1.348        from msubst2[OF lp nn nn'(1), of x bs ] H(3) nn'
   1.349        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" 
   1.350 -	apply (simp add: add_divide_distrib of_int_minus2 del: minus_add_distrib)
   1.351 -	by (simp add: mult_commute)}
   1.352 +        apply (simp add: add_divide_distrib of_int_minus2 del: minus_add_distrib)
   1.353 +        by (simp add: mult_commute)}
   1.354      moreover
   1.355      {fix c t d s assume H: "(c,t) \<in> set (uset p)" "(d,s) \<in> set (uset p)" 
   1.356        "\<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"
   1.357       from H(1,2) th have "isnpoly c" "isnpoly d" by blast+
   1.358        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"
   1.359 -	using H(3,4) by (simp_all add: polymul_norm n2)
   1.360 +        using H(3,4) by (simp_all add: polymul_norm n2)
   1.361        from msubst2[OF lp nn, of x bs ] H(3,4,5) 
   1.362        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)}
   1.363      ultimately show ?thesis by blast
   1.364 @@ -2906,16 +2906,16 @@
   1.365      proof
   1.366        assume H: ?lhs
   1.367        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" 
   1.368 -	by (auto simp add: msubst2_def lt[OF stupid(3)] lt[OF stupid(1)] mult_less_0_iff zero_less_mult_iff)
   1.369 +        by (auto simp add: msubst2_def lt[OF stupid(3)] lt[OF stupid(1)] mult_less_0_iff zero_less_mult_iff)
   1.370        from msubst2[OF lq norm2(1) z(1), of x bs] 
   1.371 -	msubst2[OF lq norm2(2) z(2), of x bs] H 
   1.372 +        msubst2[OF lq norm2(2) z(2), of x bs] H 
   1.373        show ?rhs by (simp add: ring_simps)
   1.374      next
   1.375        assume H: ?rhs
   1.376        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" 
   1.377 -	by (auto simp add: msubst2_def lt[OF stupid(4)] lt[OF stupid(2)] mult_less_0_iff zero_less_mult_iff)
   1.378 +        by (auto simp add: msubst2_def lt[OF stupid(4)] lt[OF stupid(2)] mult_less_0_iff zero_less_mult_iff)
   1.379        from msubst2[OF lq norm2(1) z(1), of x bs] 
   1.380 -	msubst2[OF lq norm2(2) z(2), of x bs] H 
   1.381 +        msubst2[OF lq norm2(2) z(2), of x bs] H 
   1.382        show ?lhs by (simp add: ring_simps)
   1.383      qed}
   1.384    hence th0: "\<forall>x \<in> set ?U. \<forall>y \<in> set ?U. ?I (?s (x, y)) \<longleftrightarrow> ?I (?s (y, x))"
     2.1 --- a/src/HOL/Decision_Procs/Polynomial_List.thy	Wed Oct 28 00:23:39 2009 +0100
     2.2 +++ b/src/HOL/Decision_Procs/Polynomial_List.thy	Wed Oct 28 00:24:38 2009 +0100
     2.3 @@ -1,8 +1,8 @@
     2.4 -(*  Title:       HOL/Decision_Procs/Polynomial_List.thy
     2.5 -    Author:      Amine Chaieb
     2.6 +(*  Title:      HOL/Decision_Procs/Polynomial_List.thy
     2.7 +    Author:     Amine Chaieb
     2.8  *)
     2.9  
    2.10 -header{*Univariate Polynomials as Lists *}
    2.11 +header {* Univariate Polynomials as Lists *}
    2.12  
    2.13  theory Polynomial_List
    2.14  imports Main
    2.15 @@ -653,7 +653,7 @@
    2.16  apply (simp add: divides_def fun_eq poly_mult)
    2.17  apply (rule_tac x = "[]" in exI)
    2.18  apply (auto dest!: order2 [where a=a]
    2.19 -	    intro: poly_exp_divides simp del: pexp_Suc)
    2.20 +            intro: poly_exp_divides simp del: pexp_Suc)
    2.21  done
    2.22  
    2.23  lemma order_decomp:
    2.24 @@ -780,4 +780,5 @@
    2.25  done
    2.26  
    2.27  lemma poly_Sing: "poly [c] x = c" by simp
    2.28 +
    2.29  end
     3.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Wed Oct 28 00:23:39 2009 +0100
     3.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Wed Oct 28 00:24:38 2009 +0100
     3.3 @@ -391,7 +391,7 @@
     3.4    {assume nn':"\<not> n' < n" hence "n < n' \<or> n = n'" by arith
     3.5      moreover {assume "n < n'" with prems have ?case by simp }
     3.6      moreover {assume eq: "n = n'" hence ?case using prems 
     3.7 -	by (cases "p +\<^sub>p p' = 0\<^sub>p", auto simp add: Let_def) }
     3.8 +        by (cases "p +\<^sub>p p' = 0\<^sub>p", auto simp add: Let_def) }
     3.9      ultimately have ?case by blast}
    3.10    ultimately show ?case by blast
    3.11  qed simp_all
    3.12 @@ -413,10 +413,10 @@
    3.13        by simp_all
    3.14      {assume "?c = 0\<^sub>N" hence ?case by auto}
    3.15        moreover {assume cnz: "?c \<noteq> 0\<^sub>N" 
    3.16 -	from "2.hyps"(1)[rule_format,where xb="n'",  OF cnz n(1) n(3)] 
    3.17 -	  "2.hyps"(2)[rule_format, where x="Suc n'" 
    3.18 -	  and xa="Suc n'" and xb = "n'", OF cnz ] cnz n have ?case
    3.19 -	  by (auto simp add: min_def)}
    3.20 +        from "2.hyps"(1)[rule_format,where xb="n'",  OF cnz n(1) n(3)] 
    3.21 +          "2.hyps"(2)[rule_format, where x="Suc n'" 
    3.22 +          and xa="Suc n'" and xb = "n'", OF cnz ] cnz n have ?case
    3.23 +          by (auto simp add: min_def)}
    3.24        ultimately show ?case by blast
    3.25    next
    3.26      case (2 n0 n1) thus ?case by auto 
    3.27 @@ -431,10 +431,10 @@
    3.28        by simp_all
    3.29      {assume "?c' = 0\<^sub>N" hence ?case by auto}
    3.30        moreover {assume cnz: "?c' \<noteq> 0\<^sub>N"
    3.31 -	from "3.hyps"(1)[rule_format,where xb="n",  OF cnz n(3) n(1)] 
    3.32 -	  "3.hyps"(2)[rule_format, where x="Suc n" 
    3.33 -	  and xa="Suc n" and xb = "n", OF cnz ] cnz n have ?case
    3.34 -	  by (auto simp add: min_def)}
    3.35 +        from "3.hyps"(1)[rule_format,where xb="n",  OF cnz n(3) n(1)] 
    3.36 +          "3.hyps"(2)[rule_format, where x="Suc n" 
    3.37 +          and xa="Suc n" and xb = "n", OF cnz ] cnz n have ?case
    3.38 +          by (auto simp add: min_def)}
    3.39        ultimately show ?case by blast
    3.40    next
    3.41      case (2 n0 n1) thus ?case apply auto done
    3.42 @@ -446,32 +446,32 @@
    3.43      {fix n0 n1
    3.44        assume "isnpolyh ?cnp n0" and "isnpolyh ?cnp' n1"
    3.45        hence cnp: "isnpolyh ?cnp n" and cnp': "isnpolyh ?cnp' n'"
    3.46 -	and np: "isnpolyh p n" and nc: "isnpolyh c (Suc n)" 
    3.47 -	and np': "isnpolyh p' n'" and nc': "isnpolyh c' (Suc n')"
    3.48 -	and nn0: "n \<ge> n0" and nn1:"n' \<ge> n1"
    3.49 -	by simp_all
    3.50 +        and np: "isnpolyh p n" and nc: "isnpolyh c (Suc n)" 
    3.51 +        and np': "isnpolyh p' n'" and nc': "isnpolyh c' (Suc n')"
    3.52 +        and nn0: "n \<ge> n0" and nn1:"n' \<ge> n1"
    3.53 +        by simp_all
    3.54        have "n < n' \<or> n' < n \<or> n' = n" by auto
    3.55        moreover
    3.56        {assume nn': "n < n'"
    3.57 -	with "4.hyps"(5)[rule_format, OF nn' np cnp', where xb ="n"] 
    3.58 -	  "4.hyps"(6)[rule_format, OF nn' nc cnp', where xb="n"] nn' nn0 nn1 cnp
    3.59 -	have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
    3.60 -	  by (simp add: min_def) }
    3.61 +        with "4.hyps"(5)[rule_format, OF nn' np cnp', where xb ="n"] 
    3.62 +          "4.hyps"(6)[rule_format, OF nn' nc cnp', where xb="n"] nn' nn0 nn1 cnp
    3.63 +        have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
    3.64 +          by (simp add: min_def) }
    3.65        moreover
    3.66  
    3.67        {assume nn': "n > n'" hence stupid: "n' < n \<and> \<not> n < n'" by arith
    3.68 -	with "4.hyps"(3)[rule_format, OF stupid cnp np', where xb="n'"]
    3.69 -	  "4.hyps"(4)[rule_format, OF stupid cnp nc', where xb="Suc n'"] 
    3.70 -	  nn' nn0 nn1 cnp'
    3.71 -	have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
    3.72 -	  by (cases "Suc n' = n", simp_all add: min_def)}
    3.73 +        with "4.hyps"(3)[rule_format, OF stupid cnp np', where xb="n'"]
    3.74 +          "4.hyps"(4)[rule_format, OF stupid cnp nc', where xb="Suc n'"] 
    3.75 +          nn' nn0 nn1 cnp'
    3.76 +        have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
    3.77 +          by (cases "Suc n' = n", simp_all add: min_def)}
    3.78        moreover
    3.79        {assume nn': "n' = n" hence stupid: "\<not> n' < n \<and> \<not> n < n'" by arith
    3.80 -	from "4.hyps"(1)[rule_format, OF stupid cnp np', where xb="n"]
    3.81 -	  "4.hyps"(2)[rule_format, OF stupid cnp nc', where xb="n"] nn' cnp cnp' nn1
    3.82 -	
    3.83 -	have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
    3.84 -	  by simp (rule polyadd_normh,simp_all add: min_def isnpolyh_mono[OF nn0]) }
    3.85 +        from "4.hyps"(1)[rule_format, OF stupid cnp np', where xb="n"]
    3.86 +          "4.hyps"(2)[rule_format, OF stupid cnp nc', where xb="n"] nn' cnp cnp' nn1
    3.87 +        
    3.88 +        have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
    3.89 +          by simp (rule polyadd_normh,simp_all add: min_def isnpolyh_mono[OF nn0]) }
    3.90        ultimately show "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)" by blast }
    3.91      note th = this
    3.92      {fix n0 n1 m
    3.93 @@ -484,86 +484,86 @@
    3.94        have "n'<n \<or> n < n' \<or> n' = n" by auto
    3.95        moreover 
    3.96        {assume "n' < n \<or> n < n'"
    3.97 -	with "4.hyps" np np' m 
    3.98 -	have ?eq apply (cases "n' < n", simp_all)
    3.99 -	apply (erule allE[where x="n"],erule allE[where x="n"],auto) 
   3.100 -	done }
   3.101 +        with "4.hyps" np np' m 
   3.102 +        have ?eq apply (cases "n' < n", simp_all)
   3.103 +        apply (erule allE[where x="n"],erule allE[where x="n"],auto) 
   3.104 +        done }
   3.105        moreover
   3.106        {assume nn': "n' = n"  hence nn:"\<not> n' < n \<and> \<not> n < n'" by arith
   3.107 - 	from "4.hyps"(1)[rule_format, OF nn, where x="n" and xa ="n'" and xb="n"]
   3.108 -	  "4.hyps"(2)[rule_format, OF nn, where x="n" and xa ="Suc n'" and xb="n"] 
   3.109 -	  np np' nn'
   3.110 -	have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"
   3.111 -	  "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
   3.112 -	  "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)" 
   3.113 -	  "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p" by (auto simp add: min_def)
   3.114 -	{assume mn: "m = n" 
   3.115 -	  from "4.hyps"(1)[rule_format, OF nn norm(1,4), where xb="n"]
   3.116 -	    "4.hyps"(2)[rule_format, OF nn norm(1,2), where xb="n"] norm nn' mn
   3.117 -	  have degs:  "degreen (?cnp *\<^sub>p c') n = 
   3.118 -	    (if c'=0\<^sub>p then 0 else ?d1 + degreen c' n)"
   3.119 -	    "degreen (?cnp *\<^sub>p p') n = ?d1  + degreen p' n" by (simp_all add: min_def)
   3.120 -	  from degs norm
   3.121 -	  have th1: "degreen(?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" by simp
   3.122 -	  hence neq: "degreen (?cnp *\<^sub>p c') n \<noteq> degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n"
   3.123 -	    by simp
   3.124 -	  have nmin: "n \<le> min n n" by (simp add: min_def)
   3.125 -	  from polyadd_different_degreen[OF norm(3,6) neq nmin] th1
   3.126 -	  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 
   3.127 -	  from "4.hyps"(1)[rule_format, OF nn norm(1,4), where xb="n"]
   3.128 -	    "4.hyps"(2)[rule_format, OF nn norm(1,2), where xb="n"]
   3.129 -	    mn norm m nn' deg
   3.130 -	  have ?eq by simp}
   3.131 -	moreover
   3.132 -	{assume mn: "m \<noteq> n" hence mn': "m < n" using m np by auto
   3.133 -	  from nn' m np have max1: "m \<le> max n n"  by simp 
   3.134 -	  hence min1: "m \<le> min n n" by simp	
   3.135 -	  hence min2: "m \<le> min n (Suc n)" by simp
   3.136 -	  {assume "c' = 0\<^sub>p"
   3.137 -	    from `c' = 0\<^sub>p` have ?eq
   3.138 -	      using "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
   3.139 -	    "4.hyps"(2)[rule_format, OF nn norm(1,2) min2] mn nn'
   3.140 -	      apply simp
   3.141 -	      done}
   3.142 -	  moreover
   3.143 -	  {assume cnz: "c' \<noteq> 0\<^sub>p"
   3.144 -	    from "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
   3.145 -	      "4.hyps"(2)[rule_format, OF nn norm(1,2) min2]
   3.146 -	      degreen_polyadd[OF norm(3,6) max1]
   3.147 +        from "4.hyps"(1)[rule_format, OF nn, where x="n" and xa ="n'" and xb="n"]
   3.148 +          "4.hyps"(2)[rule_format, OF nn, where x="n" and xa ="Suc n'" and xb="n"] 
   3.149 +          np np' nn'
   3.150 +        have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"
   3.151 +          "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
   3.152 +          "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)" 
   3.153 +          "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p" by (auto simp add: min_def)
   3.154 +        {assume mn: "m = n" 
   3.155 +          from "4.hyps"(1)[rule_format, OF nn norm(1,4), where xb="n"]
   3.156 +            "4.hyps"(2)[rule_format, OF nn norm(1,2), where xb="n"] norm nn' mn
   3.157 +          have degs:  "degreen (?cnp *\<^sub>p c') n = 
   3.158 +            (if c'=0\<^sub>p then 0 else ?d1 + degreen c' n)"
   3.159 +            "degreen (?cnp *\<^sub>p p') n = ?d1  + degreen p' n" by (simp_all add: min_def)
   3.160 +          from degs norm
   3.161 +          have th1: "degreen(?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" by simp
   3.162 +          hence neq: "degreen (?cnp *\<^sub>p c') n \<noteq> degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n"
   3.163 +            by simp
   3.164 +          have nmin: "n \<le> min n n" by (simp add: min_def)
   3.165 +          from polyadd_different_degreen[OF norm(3,6) neq nmin] th1
   3.166 +          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 
   3.167 +          from "4.hyps"(1)[rule_format, OF nn norm(1,4), where xb="n"]
   3.168 +            "4.hyps"(2)[rule_format, OF nn norm(1,2), where xb="n"]
   3.169 +            mn norm m nn' deg
   3.170 +          have ?eq by simp}
   3.171 +        moreover
   3.172 +        {assume mn: "m \<noteq> n" hence mn': "m < n" using m np by auto
   3.173 +          from nn' m np have max1: "m \<le> max n n"  by simp 
   3.174 +          hence min1: "m \<le> min n n" by simp     
   3.175 +          hence min2: "m \<le> min n (Suc n)" by simp
   3.176 +          {assume "c' = 0\<^sub>p"
   3.177 +            from `c' = 0\<^sub>p` have ?eq
   3.178 +              using "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
   3.179 +            "4.hyps"(2)[rule_format, OF nn norm(1,2) min2] mn nn'
   3.180 +              apply simp
   3.181 +              done}
   3.182 +          moreover
   3.183 +          {assume cnz: "c' \<noteq> 0\<^sub>p"
   3.184 +            from "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
   3.185 +              "4.hyps"(2)[rule_format, OF nn norm(1,2) min2]
   3.186 +              degreen_polyadd[OF norm(3,6) max1]
   3.187  
   3.188 -	    have "degreen (?cnp *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (?cnp *\<^sub>p p')) m 
   3.189 -	      \<le> max (degreen (?cnp *\<^sub>p c') m) (degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) m)"
   3.190 -	      using mn nn' cnz np np' by simp
   3.191 -	    with "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
   3.192 -	      "4.hyps"(2)[rule_format, OF nn norm(1,2) min2]
   3.193 -	      degreen_0[OF norm(3) mn'] have ?eq using nn' mn cnz np np' by clarsimp}
   3.194 -	  ultimately have ?eq by blast }
   3.195 -	ultimately have ?eq by blast}
   3.196 +            have "degreen (?cnp *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (?cnp *\<^sub>p p')) m 
   3.197 +              \<le> max (degreen (?cnp *\<^sub>p c') m) (degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) m)"
   3.198 +              using mn nn' cnz np np' by simp
   3.199 +            with "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
   3.200 +              "4.hyps"(2)[rule_format, OF nn norm(1,2) min2]
   3.201 +              degreen_0[OF norm(3) mn'] have ?eq using nn' mn cnz np np' by clarsimp}
   3.202 +          ultimately have ?eq by blast }
   3.203 +        ultimately have ?eq by blast}
   3.204        ultimately show ?eq by blast}
   3.205      note degth = this
   3.206      { case (2 n0 n1)
   3.207        hence np: "isnpolyh ?cnp n0" and np': "isnpolyh ?cnp' n1" 
   3.208 -	and m: "m \<le> min n0 n1" by simp_all
   3.209 +        and m: "m \<le> min n0 n1" by simp_all
   3.210        hence mn: "m \<le> n" by simp
   3.211        let ?c0p = "CN 0\<^sub>p n (?cnp *\<^sub>p p')"
   3.212        {assume C: "?cnp *\<^sub>p c' +\<^sub>p ?c0p = 0\<^sub>p" "n' = n"
   3.213 -	hence nn: "\<not>n' < n \<and> \<not> n<n'" by simp
   3.214 -	from "4.hyps"(1) [rule_format, OF nn, where x="n" and xa = "n" and xb="n"] 
   3.215 -	  "4.hyps"(2) [rule_format, OF nn, where x="n" and xa = "Suc n" and xb="n"] 
   3.216 -	  np np' C(2) mn
   3.217 -	have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"
   3.218 -	  "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
   3.219 -	  "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)" 
   3.220 -	  "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p" 
   3.221 -	  "degreen (?cnp *\<^sub>p c') n = (if c'=0\<^sub>p then 0 else degreen ?cnp n + degreen c' n)"
   3.222 -	    "degreen (?cnp *\<^sub>p p') n = degreen ?cnp n + degreen p' n"
   3.223 -	  by (simp_all add: min_def)
   3.224 -	    
   3.225 -	  from norm have cn: "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp
   3.226 -	  have degneq: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" 
   3.227 -	    using norm by simp
   3.228 -	from polyadd_eq_const_degreen[OF norm(3) cn C(1), where m="n"]  degneq
   3.229 -	have "False" by simp }
   3.230 +        hence nn: "\<not>n' < n \<and> \<not> n<n'" by simp
   3.231 +        from "4.hyps"(1) [rule_format, OF nn, where x="n" and xa = "n" and xb="n"] 
   3.232 +          "4.hyps"(2) [rule_format, OF nn, where x="n" and xa = "Suc n" and xb="n"] 
   3.233 +          np np' C(2) mn
   3.234 +        have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"
   3.235 +          "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
   3.236 +          "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)" 
   3.237 +          "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p" 
   3.238 +          "degreen (?cnp *\<^sub>p c') n = (if c'=0\<^sub>p then 0 else degreen ?cnp n + degreen c' n)"
   3.239 +            "degreen (?cnp *\<^sub>p p') n = degreen ?cnp n + degreen p' n"
   3.240 +          by (simp_all add: min_def)
   3.241 +            
   3.242 +          from norm have cn: "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp
   3.243 +          have degneq: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" 
   3.244 +            using norm by simp
   3.245 +        from polyadd_eq_const_degreen[OF norm(3) cn C(1), where m="n"]  degneq
   3.246 +        have "False" by simp }
   3.247        thus ?case using "4.hyps" by clarsimp}
   3.248  qed auto
   3.249  
   3.250 @@ -1022,8 +1022,8 @@
   3.251        have "\<forall>x. poly (polypoly' (?ts @ xs) p) x = poly [] x"  by simp
   3.252        hence "poly (polypoly' (?ts @ xs) p) = poly []" by (auto intro: ext) 
   3.253        hence "\<forall> c \<in> set (coefficients p). Ipoly (?ts @ xs) (decrpoly c) = 0"
   3.254 -	thm poly_zero
   3.255 -	using poly_zero[where ?'a='a] by (simp add: polypoly'_def list_all_iff)
   3.256 +        thm poly_zero
   3.257 +        using poly_zero[where ?'a='a] by (simp add: polypoly'_def list_all_iff)
   3.258        with coefficients_head[of p, symmetric]
   3.259        have th0: "Ipoly (?ts @ xs) ?hd = 0" by simp
   3.260        from bs have wf'': "wf_bs ?ts ?hd" unfolding wf_bs_def by simp
   3.261 @@ -1272,18 +1272,18 @@
   3.262        by (simp add: min_def)
   3.263      {assume np: "n > 0"
   3.264        with nn' head_isnpolyh_Suc'[OF np nth]
   3.265 -	head_isnpolyh_Suc'[OF np norm(5)] head_isnpolyh_Suc'[OF np norm(6)[simplified nn']]
   3.266 +        head_isnpolyh_Suc'[OF np norm(5)] head_isnpolyh_Suc'[OF np norm(6)[simplified nn']]
   3.267        have ?case by simp}
   3.268      moreover
   3.269      {moreover assume nz: "n = 0"
   3.270        from polymul_degreen[OF norm(5,4), where m="0"]
   3.271 -	polymul_degreen[OF norm(5,3), where m="0"] nn' nz degree_eq_degreen0
   3.272 +        polymul_degreen[OF norm(5,3), where m="0"] nn' nz degree_eq_degreen0
   3.273        norm(5,6) degree_npolyhCN[OF norm(6)]
   3.274      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
   3.275      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
   3.276      from polyadd_head[OF ncnpc'[simplified nz] ncnpp0'[simplified nz] dth'] dth
   3.277      have ?case   using norm prems(2)[rule_format, OF stupid norm(5,3)]
   3.278 -	prems(3)[rule_format, OF stupid norm(5,4)] nn' nz by simp }
   3.279 +        prems(3)[rule_format, OF stupid norm(5,4)] nn' nz by simp }
   3.280      ultimately have ?case by (cases n) auto} 
   3.281    ultimately show ?case by blast
   3.282  qed simp_all
   3.283 @@ -1399,182 +1399,182 @@
   3.284      moreover 
   3.285      {assume dn': "\<not> d < n" hence dn: "d \<ge> n" by arith
   3.286        have degsp': "degree s = degree ?p'" 
   3.287 -	using ds dn ndp funpow_shift1_degree[where k = "d - n" and p="p"] by simp
   3.288 +        using ds dn ndp funpow_shift1_degree[where k = "d - n" and p="p"] by simp
   3.289        {assume ba: "?b = a"
   3.290 -	hence headsp': "head s = head ?p'" using ap headp' by simp
   3.291 -	have nr: "isnpolyh (s -\<^sub>p ?p') 0" using polysub_normh[OF ns np'] by simp
   3.292 -	from ds degree_polysub_samehead[OF ns np' headsp' degsp']
   3.293 -	have "degree (s -\<^sub>p ?p') < d \<or> s -\<^sub>p ?p' = 0\<^sub>p" by simp
   3.294 -	moreover 
   3.295 -	{assume deglt:"degree (s -\<^sub>p ?p') < d"
   3.296 -	  from  H[rule_format, OF deglt nr,simplified] 
   3.297 -	  have domsp: "?D (a, n, p, k, s -\<^sub>p ?p')" by blast 
   3.298 -	  have dom: ?dths apply (rule polydivide_aux_real_domintros) 
   3.299 -	    using ba ds dn' domsp by simp_all
   3.300 -	  from polydivide_aux.psimps[OF dom] sz dn' ba ds
   3.301 -	  have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')"
   3.302 -	    by (simp add: Let_def)
   3.303 -	  {assume h1: "polydivide_aux (a, n, p, k, s) = (k', r)"
   3.304 -	    from H[rule_format, OF deglt nr, where xa = "k" and xb="k'" and xc="r", simplified]
   3.305 -	      trans[OF eq[symmetric] h1]
   3.306 -	    have kk': "k \<le> k'" and nr:"\<exists>nr. isnpolyh r nr" and dr: "degree r = 0 \<or> degree r < degree p"
   3.307 -	      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
   3.308 -	    from q1 obtain q n1 where nq: "isnpolyh q n1" 
   3.309 -	      and asp:"a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p') = p *\<^sub>p q +\<^sub>p r"  by blast
   3.310 -	    from nr obtain nr where nr': "isnpolyh r nr" by blast
   3.311 -	    from polymul_normh[OF nakk' ns] have nakks': "isnpolyh (a ^\<^sub>p (k' - k) *\<^sub>p s) 0" by simp
   3.312 -	    from polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]
   3.313 -	    have nq': "isnpolyh (?akk' *\<^sub>p ?xdn +\<^sub>p q) 0" by simp
   3.314 -	    from polyadd_normh[OF polymul_normh[OF np 
   3.315 -	      polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]] nr']
   3.316 -	    have nqr': "isnpolyh (p *\<^sub>p (?akk' *\<^sub>p ?xdn +\<^sub>p q) +\<^sub>p r) 0" by simp 
   3.317 -	    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')) = 
   3.318 -	      Ipoly bs (p *\<^sub>p q +\<^sub>p r)" by simp
   3.319 -	    hence " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) = 
   3.320 -	      Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r" 
   3.321 -	      by (simp add: ring_simps)
   3.322 -	    hence " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   3.323 -	      Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (d - n) shift1 1\<^sub>p *\<^sub>p p) 
   3.324 -	      + Ipoly bs p * Ipoly bs q + Ipoly bs r"
   3.325 -	      by (auto simp only: funpow_shift1_1) 
   3.326 -	    hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   3.327 -	      Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (d - n) shift1 1\<^sub>p) 
   3.328 -	      + Ipoly bs q) + Ipoly bs r" by (simp add: ring_simps)
   3.329 -	    hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   3.330 -	      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
   3.331 -	    with isnpolyh_unique[OF nakks' nqr']
   3.332 -	    have "a ^\<^sub>p (k' - k) *\<^sub>p s = 
   3.333 -	      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
   3.334 -	    hence ?qths using nq'
   3.335 -	      apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (d - n) shift1 1\<^sub>p) +\<^sub>p q" in exI)
   3.336 -	      apply (rule_tac x="0" in exI) by simp
   3.337 -	    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"
   3.338 -	      by blast } hence ?qrths by blast
   3.339 -	  with dom have ?ths by blast} 
   3.340 -	moreover 
   3.341 -	{assume spz:"s -\<^sub>p ?p' = 0\<^sub>p"
   3.342 -	  hence domsp: "?D (a, n, p, k, s -\<^sub>p ?p')" 
   3.343 -	    apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
   3.344 -	  have dom: ?dths apply (rule polydivide_aux_real_domintros) 
   3.345 -	    using ba ds dn' domsp by simp_all
   3.346 -	  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}"]
   3.347 -	  have " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs s = Ipoly bs ?p'" by simp
   3.348 -	  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
   3.349 -	    by (simp only: funpow_shift1_1) simp
   3.350 -	  hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] by blast
   3.351 -	  {assume h1: "polydivide_aux (a,n,p,k,s) = (k',r)"
   3.352 -	    from polydivide_aux.psimps[OF dom] sz dn' ba ds
   3.353 -	    have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')"
   3.354 -	      by (simp add: Let_def)
   3.355 -	    also have "\<dots> = (k,0\<^sub>p)" using polydivide_aux.psimps[OF domsp] spz by simp
   3.356 -	    finally have "(k',r) = (k,0\<^sub>p)" using h1 by simp
   3.357 -	    with sp' ns np nxdn polyadd_0(1)[OF polymul_normh[OF np nxdn]]
   3.358 -	      polyadd_0(2)[OF polymul_normh[OF np nxdn]] have ?qrths
   3.359 -	      apply auto
   3.360 -	      apply (rule exI[where x="?xdn"]) 	      
   3.361 -	      apply auto
   3.362 -	      apply (rule polymul_commute)
   3.363 -	      apply simp_all
   3.364 -	      done}
   3.365 -	  with dom have ?ths by blast}
   3.366 -	ultimately have ?ths by blast }
   3.367 +        hence headsp': "head s = head ?p'" using ap headp' by simp
   3.368 +        have nr: "isnpolyh (s -\<^sub>p ?p') 0" using polysub_normh[OF ns np'] by simp
   3.369 +        from ds degree_polysub_samehead[OF ns np' headsp' degsp']
   3.370 +        have "degree (s -\<^sub>p ?p') < d \<or> s -\<^sub>p ?p' = 0\<^sub>p" by simp
   3.371 +        moreover 
   3.372 +        {assume deglt:"degree (s -\<^sub>p ?p') < d"
   3.373 +          from  H[rule_format, OF deglt nr,simplified] 
   3.374 +          have domsp: "?D (a, n, p, k, s -\<^sub>p ?p')" by blast 
   3.375 +          have dom: ?dths apply (rule polydivide_aux_real_domintros) 
   3.376 +            using ba ds dn' domsp by simp_all
   3.377 +          from polydivide_aux.psimps[OF dom] sz dn' ba ds
   3.378 +          have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')"
   3.379 +            by (simp add: Let_def)
   3.380 +          {assume h1: "polydivide_aux (a, n, p, k, s) = (k', r)"
   3.381 +            from H[rule_format, OF deglt nr, where xa = "k" and xb="k'" and xc="r", simplified]
   3.382 +              trans[OF eq[symmetric] h1]
   3.383 +            have kk': "k \<le> k'" and nr:"\<exists>nr. isnpolyh r nr" and dr: "degree r = 0 \<or> degree r < degree p"
   3.384 +              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
   3.385 +            from q1 obtain q n1 where nq: "isnpolyh q n1" 
   3.386 +              and asp:"a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p') = p *\<^sub>p q +\<^sub>p r"  by blast
   3.387 +            from nr obtain nr where nr': "isnpolyh r nr" by blast
   3.388 +            from polymul_normh[OF nakk' ns] have nakks': "isnpolyh (a ^\<^sub>p (k' - k) *\<^sub>p s) 0" by simp
   3.389 +            from polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]
   3.390 +            have nq': "isnpolyh (?akk' *\<^sub>p ?xdn +\<^sub>p q) 0" by simp
   3.391 +            from polyadd_normh[OF polymul_normh[OF np 
   3.392 +              polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]] nr']
   3.393 +            have nqr': "isnpolyh (p *\<^sub>p (?akk' *\<^sub>p ?xdn +\<^sub>p q) +\<^sub>p r) 0" by simp 
   3.394 +            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')) = 
   3.395 +              Ipoly bs (p *\<^sub>p q +\<^sub>p r)" by simp
   3.396 +            hence " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) = 
   3.397 +              Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r" 
   3.398 +              by (simp add: ring_simps)
   3.399 +            hence " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   3.400 +              Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (d - n) shift1 1\<^sub>p *\<^sub>p p) 
   3.401 +              + Ipoly bs p * Ipoly bs q + Ipoly bs r"
   3.402 +              by (auto simp only: funpow_shift1_1) 
   3.403 +            hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   3.404 +              Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (d - n) shift1 1\<^sub>p) 
   3.405 +              + Ipoly bs q) + Ipoly bs r" by (simp add: ring_simps)
   3.406 +            hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   3.407 +              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
   3.408 +            with isnpolyh_unique[OF nakks' nqr']
   3.409 +            have "a ^\<^sub>p (k' - k) *\<^sub>p s = 
   3.410 +              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
   3.411 +            hence ?qths using nq'
   3.412 +              apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (d - n) shift1 1\<^sub>p) +\<^sub>p q" in exI)
   3.413 +              apply (rule_tac x="0" in exI) by simp
   3.414 +            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"
   3.415 +              by blast } hence ?qrths by blast
   3.416 +          with dom have ?ths by blast} 
   3.417 +        moreover 
   3.418 +        {assume spz:"s -\<^sub>p ?p' = 0\<^sub>p"
   3.419 +          hence domsp: "?D (a, n, p, k, s -\<^sub>p ?p')" 
   3.420 +            apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
   3.421 +          have dom: ?dths apply (rule polydivide_aux_real_domintros) 
   3.422 +            using ba ds dn' domsp by simp_all
   3.423 +          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}"]
   3.424 +          have " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs s = Ipoly bs ?p'" by simp
   3.425 +          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
   3.426 +            by (simp only: funpow_shift1_1) simp
   3.427 +          hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] by blast
   3.428 +          {assume h1: "polydivide_aux (a,n,p,k,s) = (k',r)"
   3.429 +            from polydivide_aux.psimps[OF dom] sz dn' ba ds
   3.430 +            have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')"
   3.431 +              by (simp add: Let_def)
   3.432 +            also have "\<dots> = (k,0\<^sub>p)" using polydivide_aux.psimps[OF domsp] spz by simp
   3.433 +            finally have "(k',r) = (k,0\<^sub>p)" using h1 by simp
   3.434 +            with sp' ns np nxdn polyadd_0(1)[OF polymul_normh[OF np nxdn]]
   3.435 +              polyadd_0(2)[OF polymul_normh[OF np nxdn]] have ?qrths
   3.436 +              apply auto
   3.437 +              apply (rule exI[where x="?xdn"])        
   3.438 +              apply auto
   3.439 +              apply (rule polymul_commute)
   3.440 +              apply simp_all
   3.441 +              done}
   3.442 +          with dom have ?ths by blast}
   3.443 +        ultimately have ?ths by blast }
   3.444        moreover
   3.445        {assume ba: "?b \<noteq> a"
   3.446 -	from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np0, simplified ap] ns] 
   3.447 -	  polymul_normh[OF head_isnpolyh[OF ns] np']]
   3.448 -	have nth: "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" by(simp add: min_def)
   3.449 -	have nzths: "a *\<^sub>p s \<noteq> 0\<^sub>p" "?b *\<^sub>p ?p' \<noteq> 0\<^sub>p"
   3.450 -	  using polymul_eq0_iff[OF head_isnpolyh[OF np0, simplified ap] ns] 
   3.451 -	    polymul_eq0_iff[OF head_isnpolyh[OF ns] np']head_nz[OF np0] ap pnz sz head_nz[OF ns]
   3.452 -	    funpow_shift1_nz[OF pnz] by simp_all
   3.453 -	from polymul_head_polyeq[OF head_isnpolyh[OF np] ns] head_nz[OF np] sz ap head_head[OF np] pnz
   3.454 -	  polymul_head_polyeq[OF head_isnpolyh[OF ns] np'] head_nz [OF ns] sz funpow_shift1_nz[OF pnz, where n="d - n"]
   3.455 -	have hdth: "head (a *\<^sub>p s) = head (?b *\<^sub>p ?p')" 
   3.456 -	  using head_head[OF ns] funpow_shift1_head[OF np pnz]
   3.457 -	    polymul_commute[OF head_isnpolyh[OF np] head_isnpolyh[OF ns]]
   3.458 -	  by (simp add: ap)
   3.459 -	from polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"]
   3.460 -	  head_nz[OF np] pnz sz ap[symmetric]
   3.461 -	  funpow_shift1_nz[OF pnz, where n="d - n"]
   3.462 -	  polymul_degreen[OF head_isnpolyh[OF ns] np', where m="0"]  head_nz[OF ns]
   3.463 -	  ndp ds[symmetric] dn
   3.464 -	have degth: "degree (a *\<^sub>p s) = degree (?b *\<^sub>p ?p') "
   3.465 -	  by (simp add: degree_eq_degreen0[symmetric] funpow_shift1_degree)
   3.466 -	{assume dth: "degree ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) < d"
   3.467 -	  have th: "?D (a, n, p, Suc k, (a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))"
   3.468 -	    using H[rule_format, OF dth nth, simplified] by blast 
   3.469 -	  have dom: ?dths
   3.470 -	    using ba ds dn' th apply simp apply (rule polydivide_aux_real_domintros)  
   3.471 -	    using ba ds dn'  by simp_all
   3.472 -	  from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np] ns] polymul_normh[OF head_isnpolyh[OF ns]np']]
   3.473 -	  ap have nasbp': "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" by simp
   3.474 -	  {assume h1:"polydivide_aux (a,n,p,k,s) = (k', r)"
   3.475 -	    from h1  polydivide_aux.psimps[OF dom] sz dn' ba ds
   3.476 -	    have eq:"polydivide_aux (a,n,p,Suc k,(a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = (k',r)"
   3.477 -	      by (simp add: Let_def)
   3.478 -	    with H[rule_format, OF dth nasbp', simplified, where xa="Suc k" and xb="k'" and xc="r"]
   3.479 -	    obtain q nq nr where kk': "Suc k \<le> k'" and nr: "isnpolyh r nr" and nq: "isnpolyh q nq" 
   3.480 -	      and dr: "degree r = 0 \<or> degree r < degree p"
   3.481 -	      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
   3.482 -	    from kk' have kk'':"Suc (k' - Suc k) = k' - k" by arith
   3.483 -	    {fix bs:: "'a::{ring_char_0,division_by_zero,field} list"
   3.484 -	      
   3.485 -	    from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric]
   3.486 -	    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
   3.487 -	    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"
   3.488 -	      by (simp add: ring_simps power_Suc)
   3.489 -	    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"
   3.490 -	      by (simp add:kk'' funpow_shift1_1[where n="d - n" and p="p"])
   3.491 -	    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"
   3.492 -	      by (simp add: ring_simps)}
   3.493 -	    hence ieq:"\<forall>(bs :: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   3.494 -	      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 
   3.495 -	    let ?q = "q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)"
   3.496 -	    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]]
   3.497 -	    have nqw: "isnpolyh ?q 0" by simp
   3.498 -	    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]]
   3.499 -	    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
   3.500 -	    from dr kk' nr h1 asth nqw have ?qrths apply simp
   3.501 -	      apply (rule conjI)
   3.502 -	      apply (rule exI[where x="nr"], simp)
   3.503 -	      apply (rule exI[where x="(q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn))"], simp)
   3.504 -	      apply (rule exI[where x="0"], simp)
   3.505 -	      done}
   3.506 -	  hence ?qrths by blast
   3.507 -	  with dom have ?ths by blast}
   3.508 -	moreover 
   3.509 -	{assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p"
   3.510 -	  hence domsp: "?D (a, n, p, Suc k, a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p'))" 
   3.511 -	    apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
   3.512 -	  have dom: ?dths using sz ba dn' ds domsp 
   3.513 -	    by - (rule polydivide_aux_real_domintros, simp_all)
   3.514 -	  {fix bs :: "'a::{ring_char_0,division_by_zero,field} list"
   3.515 -	    from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz
   3.516 -	  have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'" by simp
   3.517 -	  hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (?b *\<^sub>p ?xdn) * Ipoly bs p" 
   3.518 -	    by (simp add: funpow_shift1_1[where n="d - n" and p="p"])
   3.519 -	  hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" by simp
   3.520 -	}
   3.521 -	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))" ..
   3.522 -	  from hth
   3.523 -	  have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)" 
   3.524 -	    using isnpolyh_unique[where ?'a = "'a::{ring_char_0,division_by_zero,field}", OF polymul_normh[OF head_isnpolyh[OF np] ns] 
   3.525 +        from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np0, simplified ap] ns] 
   3.526 +          polymul_normh[OF head_isnpolyh[OF ns] np']]
   3.527 +        have nth: "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" by(simp add: min_def)
   3.528 +        have nzths: "a *\<^sub>p s \<noteq> 0\<^sub>p" "?b *\<^sub>p ?p' \<noteq> 0\<^sub>p"
   3.529 +          using polymul_eq0_iff[OF head_isnpolyh[OF np0, simplified ap] ns] 
   3.530 +            polymul_eq0_iff[OF head_isnpolyh[OF ns] np']head_nz[OF np0] ap pnz sz head_nz[OF ns]
   3.531 +            funpow_shift1_nz[OF pnz] by simp_all
   3.532 +        from polymul_head_polyeq[OF head_isnpolyh[OF np] ns] head_nz[OF np] sz ap head_head[OF np] pnz
   3.533 +          polymul_head_polyeq[OF head_isnpolyh[OF ns] np'] head_nz [OF ns] sz funpow_shift1_nz[OF pnz, where n="d - n"]
   3.534 +        have hdth: "head (a *\<^sub>p s) = head (?b *\<^sub>p ?p')" 
   3.535 +          using head_head[OF ns] funpow_shift1_head[OF np pnz]
   3.536 +            polymul_commute[OF head_isnpolyh[OF np] head_isnpolyh[OF ns]]
   3.537 +          by (simp add: ap)
   3.538 +        from polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"]
   3.539 +          head_nz[OF np] pnz sz ap[symmetric]
   3.540 +          funpow_shift1_nz[OF pnz, where n="d - n"]
   3.541 +          polymul_degreen[OF head_isnpolyh[OF ns] np', where m="0"]  head_nz[OF ns]
   3.542 +          ndp ds[symmetric] dn
   3.543 +        have degth: "degree (a *\<^sub>p s) = degree (?b *\<^sub>p ?p') "
   3.544 +          by (simp add: degree_eq_degreen0[symmetric] funpow_shift1_degree)
   3.545 +        {assume dth: "degree ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) < d"
   3.546 +          have th: "?D (a, n, p, Suc k, (a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))"
   3.547 +            using H[rule_format, OF dth nth, simplified] by blast 
   3.548 +          have dom: ?dths
   3.549 +            using ba ds dn' th apply simp apply (rule polydivide_aux_real_domintros)  
   3.550 +            using ba ds dn'  by simp_all
   3.551 +          from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np] ns] polymul_normh[OF head_isnpolyh[OF ns]np']]
   3.552 +          ap have nasbp': "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" by simp
   3.553 +          {assume h1:"polydivide_aux (a,n,p,k,s) = (k', r)"
   3.554 +            from h1  polydivide_aux.psimps[OF dom] sz dn' ba ds
   3.555 +            have eq:"polydivide_aux (a,n,p,Suc k,(a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = (k',r)"
   3.556 +              by (simp add: Let_def)
   3.557 +            with H[rule_format, OF dth nasbp', simplified, where xa="Suc k" and xb="k'" and xc="r"]
   3.558 +            obtain q nq nr where kk': "Suc k \<le> k'" and nr: "isnpolyh r nr" and nq: "isnpolyh q nq" 
   3.559 +              and dr: "degree r = 0 \<or> degree r < degree p"
   3.560 +              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
   3.561 +            from kk' have kk'':"Suc (k' - Suc k) = k' - k" by arith
   3.562 +            {fix bs:: "'a::{ring_char_0,division_by_zero,field} list"
   3.563 +              
   3.564 +            from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric]
   3.565 +            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
   3.566 +            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"
   3.567 +              by (simp add: ring_simps power_Suc)
   3.568 +            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"
   3.569 +              by (simp add:kk'' funpow_shift1_1[where n="d - n" and p="p"])
   3.570 +            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"
   3.571 +              by (simp add: ring_simps)}
   3.572 +            hence ieq:"\<forall>(bs :: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   3.573 +              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 
   3.574 +            let ?q = "q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)"
   3.575 +            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]]
   3.576 +            have nqw: "isnpolyh ?q 0" by simp
   3.577 +            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]]
   3.578 +            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
   3.579 +            from dr kk' nr h1 asth nqw have ?qrths apply simp
   3.580 +              apply (rule conjI)
   3.581 +              apply (rule exI[where x="nr"], simp)
   3.582 +              apply (rule exI[where x="(q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn))"], simp)
   3.583 +              apply (rule exI[where x="0"], simp)
   3.584 +              done}
   3.585 +          hence ?qrths by blast
   3.586 +          with dom have ?ths by blast}
   3.587 +        moreover 
   3.588 +        {assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p"
   3.589 +          hence domsp: "?D (a, n, p, Suc k, a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p'))" 
   3.590 +            apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
   3.591 +          have dom: ?dths using sz ba dn' ds domsp 
   3.592 +            by - (rule polydivide_aux_real_domintros, simp_all)
   3.593 +          {fix bs :: "'a::{ring_char_0,division_by_zero,field} list"
   3.594 +            from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz
   3.595 +          have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'" by simp
   3.596 +          hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (?b *\<^sub>p ?xdn) * Ipoly bs p" 
   3.597 +            by (simp add: funpow_shift1_1[where n="d - n" and p="p"])
   3.598 +          hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" by simp
   3.599 +        }
   3.600 +        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))" ..
   3.601 +          from hth
   3.602 +          have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)" 
   3.603 +            using isnpolyh_unique[where ?'a = "'a::{ring_char_0,division_by_zero,field}", OF polymul_normh[OF head_isnpolyh[OF np] ns] 
   3.604                      polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]],
   3.605 -	      simplified ap] by simp
   3.606 -	  {assume h1: "polydivide_aux (a,n,p,k,s) = (k', r)"
   3.607 -	  from h1 sz ds ba dn' spz polydivide_aux.psimps[OF dom] polydivide_aux.psimps[OF domsp] 
   3.608 -	  have "(k',r) = (Suc k, 0\<^sub>p)" by (simp add: Let_def)
   3.609 -	  with h1 np head_isnpolyh[OF np, simplified ap] ns polymul_normh[OF head_isnpolyh[OF ns] nxdn]
   3.610 -	    polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]] asq
   3.611 -	  have ?qrths apply (clarsimp simp add: Let_def)
   3.612 -	    apply (rule exI[where x="?b *\<^sub>p ?xdn"]) apply simp
   3.613 -	    apply (rule exI[where x="0"], simp)
   3.614 -	    done}
   3.615 -	hence ?qrths by blast
   3.616 -	with dom have ?ths by blast}
   3.617 -	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"]
   3.618 -	  head_nz[OF np] pnz sz ap[symmetric] ds[symmetric] 
   3.619 -	  by (simp add: degree_eq_degreen0[symmetric]) blast }
   3.620 +              simplified ap] by simp
   3.621 +          {assume h1: "polydivide_aux (a,n,p,k,s) = (k', r)"
   3.622 +          from h1 sz ds ba dn' spz polydivide_aux.psimps[OF dom] polydivide_aux.psimps[OF domsp] 
   3.623 +          have "(k',r) = (Suc k, 0\<^sub>p)" by (simp add: Let_def)
   3.624 +          with h1 np head_isnpolyh[OF np, simplified ap] ns polymul_normh[OF head_isnpolyh[OF ns] nxdn]
   3.625 +            polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]] asq
   3.626 +          have ?qrths apply (clarsimp simp add: Let_def)
   3.627 +            apply (rule exI[where x="?b *\<^sub>p ?xdn"]) apply simp
   3.628 +            apply (rule exI[where x="0"], simp)
   3.629 +            done}
   3.630 +        hence ?qrths by blast
   3.631 +        with dom have ?ths by blast}
   3.632 +        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"]
   3.633 +          head_nz[OF np] pnz sz ap[symmetric] ds[symmetric] 
   3.634 +          by (simp add: degree_eq_degreen0[symmetric]) blast }
   3.635        ultimately have ?ths by blast
   3.636      }
   3.637      ultimately have ?ths by blast}
   3.638 @@ -1732,7 +1732,7 @@
   3.639  recdef isweaknpoly "measure size"
   3.640    "isweaknpoly (C c) = True"
   3.641    "isweaknpoly (CN c n p) \<longleftrightarrow> isweaknpoly c \<and> isweaknpoly p"
   3.642 -  "isweaknpoly p = False"	
   3.643 +  "isweaknpoly p = False"       
   3.644  
   3.645  lemma isnpolyh_isweaknpoly: "isnpolyh p n0 \<Longrightarrow> isweaknpoly p" 
   3.646    by (induct p arbitrary: n0, auto)
     4.1 --- a/src/HOL/Nominal/Examples/Pattern.thy	Wed Oct 28 00:23:39 2009 +0100
     4.2 +++ b/src/HOL/Nominal/Examples/Pattern.thy	Wed Oct 28 00:24:38 2009 +0100
     4.3 @@ -669,17 +669,17 @@
     4.4      proof
     4.5        assume "x = x' \<and> t = u"
     4.6        with PVar PVar' have "PVar x T = ([]::name prm) \<bullet> q \<and>
     4.7 -	t = ([]::name prm) \<bullet> u \<and>
     4.8 -	set ([]::name prm) \<subseteq> (supp (PVar x T) \<union> supp q) \<times>
     4.9 +        t = ([]::name prm) \<bullet> u \<and>
    4.10 +        set ([]::name prm) \<subseteq> (supp (PVar x T) \<union> supp q) \<times>
    4.11            (supp (PVar x T) \<union> supp q)" by simp
    4.12        then show ?thesis ..
    4.13      next
    4.14        assume "x \<noteq> x' \<and> t = [(x, x')] \<bullet> u \<and> x \<sharp> u"
    4.15        with PVar PVar' have "PVar x T = [(x, x')] \<bullet> q \<and>
    4.16 -	t = [(x, x')] \<bullet> u \<and>
    4.17 -	set [(x, x')] \<subseteq> (supp (PVar x T) \<union> supp q) \<times>
    4.18 +        t = [(x, x')] \<bullet> u \<and>
    4.19 +        set [(x, x')] \<subseteq> (supp (PVar x T) \<union> supp q) \<times>
    4.20            (supp (PVar x T) \<union> supp q)"
    4.21 -	by (simp add: perm_swap swap_simps supp_atm perm_type)
    4.22 +        by (simp add: perm_swap swap_simps supp_atm perm_type)
    4.23        then show ?thesis ..
    4.24      qed
    4.25    next
     5.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Oct 28 00:23:39 2009 +0100
     5.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Oct 28 00:24:38 2009 +0100
     5.3 @@ -1140,51 +1140,51 @@
     5.4  
     5.5  fun mk_Eval_of additional_arguments ((x, T), NONE) names = (x, names)
     5.6    | mk_Eval_of additional_arguments ((x, T), SOME mode) names =
     5.7 -	let
     5.8 +  let
     5.9      val Ts = binder_types T
    5.10      (*val argnames = Name.variant_list names
    5.11          (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
    5.12      val args = map Free (argnames ~~ Ts)
    5.13      val (inargs, outargs) = split_smode mode args*)
    5.14 -		fun mk_split_lambda [] t = lambda (Free (Name.variant names "x", HOLogic.unitT)) t
    5.15 -			| mk_split_lambda [x] t = lambda x t
    5.16 -			| mk_split_lambda xs t =
    5.17 -			let
    5.18 -				fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t))
    5.19 -					| mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t))
    5.20 -			in
    5.21 -				mk_split_lambda' xs t
    5.22 -			end;
    5.23 -  	fun mk_arg (i, T) =
    5.24 -		  let
    5.25 -	  	  val vname = Name.variant names ("x" ^ string_of_int i)
    5.26 -		    val default = Free (vname, T)
    5.27 -		  in 
    5.28 -		    case AList.lookup (op =) mode i of
    5.29 -		      NONE => (([], [default]), [default])
    5.30 -			  | SOME NONE => (([default], []), [default])
    5.31 -			  | SOME (SOME pis) =>
    5.32 -				  case HOLogic.strip_tupleT T of
    5.33 -						[] => error "pair mode but unit tuple" (*(([default], []), [default])*)
    5.34 -					| [_] => error "pair mode but not a tuple" (*(([default], []), [default])*)
    5.35 -					| Ts =>
    5.36 -					  let
    5.37 -							val vnames = Name.variant_list names
    5.38 -								(map (fn j => "x" ^ string_of_int i ^ "p" ^ string_of_int j)
    5.39 -									(1 upto length Ts))
    5.40 -							val args = map Free (vnames ~~ Ts)
    5.41 -							fun split_args (i, arg) (ins, outs) =
    5.42 -							  if member (op =) pis i then
    5.43 -							    (arg::ins, outs)
    5.44 -								else
    5.45 -								  (ins, arg::outs)
    5.46 -							val (inargs, outargs) = fold_rev split_args ((1 upto length Ts) ~~ args) ([], [])
    5.47 -							fun tuple args = if null args then [] else [HOLogic.mk_tuple args]
    5.48 -						in ((tuple inargs, tuple outargs), args) end
    5.49 -			end
    5.50 -		val (inoutargs, args) = split_list (map mk_arg (1 upto (length Ts) ~~ Ts))
    5.51 +    fun mk_split_lambda [] t = lambda (Free (Name.variant names "x", HOLogic.unitT)) t
    5.52 +      | mk_split_lambda [x] t = lambda x t
    5.53 +      | mk_split_lambda xs t =
    5.54 +      let
    5.55 +        fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t))
    5.56 +          | mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t))
    5.57 +      in
    5.58 +        mk_split_lambda' xs t
    5.59 +      end;
    5.60 +    fun mk_arg (i, T) =
    5.61 +      let
    5.62 +        val vname = Name.variant names ("x" ^ string_of_int i)
    5.63 +        val default = Free (vname, T)
    5.64 +      in 
    5.65 +        case AList.lookup (op =) mode i of
    5.66 +          NONE => (([], [default]), [default])
    5.67 +        | SOME NONE => (([default], []), [default])
    5.68 +        | SOME (SOME pis) =>
    5.69 +          case HOLogic.strip_tupleT T of
    5.70 +            [] => error "pair mode but unit tuple" (*(([default], []), [default])*)
    5.71 +          | [_] => error "pair mode but not a tuple" (*(([default], []), [default])*)
    5.72 +          | Ts =>
    5.73 +            let
    5.74 +              val vnames = Name.variant_list names
    5.75 +                (map (fn j => "x" ^ string_of_int i ^ "p" ^ string_of_int j)
    5.76 +                  (1 upto length Ts))
    5.77 +              val args = map Free (vnames ~~ Ts)
    5.78 +              fun split_args (i, arg) (ins, outs) =
    5.79 +                if member (op =) pis i then
    5.80 +                  (arg::ins, outs)
    5.81 +                else
    5.82 +                  (ins, arg::outs)
    5.83 +              val (inargs, outargs) = fold_rev split_args ((1 upto length Ts) ~~ args) ([], [])
    5.84 +              fun tuple args = if null args then [] else [HOLogic.mk_tuple args]
    5.85 +            in ((tuple inargs, tuple outargs), args) end
    5.86 +      end
    5.87 +    val (inoutargs, args) = split_list (map mk_arg (1 upto (length Ts) ~~ Ts))
    5.88      val (inargs, outargs) = pairself flat (split_list inoutargs)
    5.89 -		val r = PredicateCompFuns.mk_Eval 
    5.90 +    val r = PredicateCompFuns.mk_Eval 
    5.91        (list_comb (x, inargs @ additional_arguments), HOLogic.mk_tuple outargs)
    5.92      val t = fold_rev mk_split_lambda args r
    5.93    in
    5.94 @@ -1353,22 +1353,22 @@
    5.95  
    5.96  fun compile_pred compilation_modifiers compfuns thy all_vs param_vs s T mode moded_cls =
    5.97    let
    5.98 -	  val (Ts1, Ts2) = chop (length (fst mode)) (binder_types T)
    5.99 +    val (Ts1, Ts2) = chop (length (fst mode)) (binder_types T)
   5.100      val (Us1, Us2) = split_smodeT (snd mode) Ts2
   5.101      val Ts1' =
   5.102        map2 (fn NONE => I | SOME is => #funT_of compilation_modifiers compfuns ([], is)) (fst mode) Ts1
   5.103      fun mk_input_term (i, NONE) =
   5.104 -		    [Free (Name.variant (all_vs @ param_vs) ("x" ^ string_of_int i), nth Ts2 (i - 1))]
   5.105 -		  | mk_input_term (i, SOME pis) = case HOLogic.strip_tupleT (nth Ts2 (i - 1)) of
   5.106 -						   [] => error "strange unit input"
   5.107 -					   | [T] => [Free (Name.variant (all_vs @ param_vs) ("x" ^ string_of_int i), nth Ts2 (i - 1))]
   5.108 -						 | Ts => let
   5.109 -							 val vnames = Name.variant_list (all_vs @ param_vs)
   5.110 -								(map (fn j => "x" ^ string_of_int i ^ "p" ^ string_of_int j)
   5.111 -									pis)
   5.112 -						 in if null pis then []
   5.113 -						   else [HOLogic.mk_tuple (map Free (vnames ~~ map (fn j => nth Ts (j - 1)) pis))] end
   5.114 -		val in_ts = maps mk_input_term (snd mode)
   5.115 +        [Free (Name.variant (all_vs @ param_vs) ("x" ^ string_of_int i), nth Ts2 (i - 1))]
   5.116 +      | mk_input_term (i, SOME pis) = case HOLogic.strip_tupleT (nth Ts2 (i - 1)) of
   5.117 +               [] => error "strange unit input"
   5.118 +             | [T] => [Free (Name.variant (all_vs @ param_vs) ("x" ^ string_of_int i), nth Ts2 (i - 1))]
   5.119 +             | Ts => let
   5.120 +               val vnames = Name.variant_list (all_vs @ param_vs)
   5.121 +                (map (fn j => "x" ^ string_of_int i ^ "p" ^ string_of_int j)
   5.122 +                  pis)
   5.123 +             in if null pis then []
   5.124 +               else [HOLogic.mk_tuple (map Free (vnames ~~ map (fn j => nth Ts (j - 1)) pis))] end
   5.125 +    val in_ts = maps mk_input_term (snd mode)
   5.126      val params = map2 (fn s => fn T => Free (s, T)) param_vs Ts1'
   5.127      val additional_arguments = #additional_arguments compilation_modifiers (all_vs @ param_vs)
   5.128      val cl_ts =
   5.129 @@ -1389,7 +1389,7 @@
   5.130  (* special setup for simpset *)                  
   5.131  val HOL_basic_ss' = HOL_basic_ss addsimps (@{thms "HOL.simp_thms"} @ [@{thm Pair_eq}])
   5.132    setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
   5.133 -	setSolver (mk_solver "True_solver" (fn _ => rtac @{thm TrueI}))
   5.134 +  setSolver (mk_solver "True_solver" (fn _ => rtac @{thm TrueI}))
   5.135  
   5.136  (* Definition of executable functions and their intro and elim rules *)
   5.137  
   5.138 @@ -1405,29 +1405,29 @@
   5.139    val funtrm = Const (mode_id, funT)
   5.140    val (Ts1, Ts2) = chop (length iss) Ts;
   5.141    val Ts1' = map2 (fn NONE => I | SOME is => funT_of (PredicateCompFuns.compfuns) ([], is)) iss Ts1
   5.142 -	val param_names = Name.variant_list []
   5.143 +  val param_names = Name.variant_list []
   5.144      (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts1)));
   5.145    val params = map Free (param_names ~~ Ts1')
   5.146 -	fun mk_args (i, T) argnames =
   5.147 +  fun mk_args (i, T) argnames =
   5.148      let
   5.149 -		  val vname = Name.variant (param_names @ argnames) ("x" ^ string_of_int (length Ts1' + i))
   5.150 -		  val default = (Free (vname, T), vname :: argnames)
   5.151 -	  in
   5.152 -  	  case AList.lookup (op =) is i of
   5.153 -						 NONE => default
   5.154 -					 | SOME NONE => default
   5.155 -        	 | SOME (SOME pis) =>
   5.156 -					   case HOLogic.strip_tupleT T of
   5.157 -						   [] => default
   5.158 -					   | [_] => default
   5.159 -						 | Ts => 
   5.160 -						let
   5.161 -							val vnames = Name.variant_list (param_names @ argnames)
   5.162 -								(map (fn j => "x" ^ string_of_int (length Ts1' + i) ^ "p" ^ string_of_int j)
   5.163 -									(1 upto (length Ts)))
   5.164 -						 in (HOLogic.mk_tuple (map Free (vnames ~~ Ts)), vnames  @ argnames) end
   5.165 -		end
   5.166 -	val (args, argnames) = fold_map mk_args (1 upto (length Ts2) ~~ Ts2) []
   5.167 +      val vname = Name.variant (param_names @ argnames) ("x" ^ string_of_int (length Ts1' + i))
   5.168 +      val default = (Free (vname, T), vname :: argnames)
   5.169 +    in
   5.170 +      case AList.lookup (op =) is i of
   5.171 +             NONE => default
   5.172 +           | SOME NONE => default
   5.173 +           | SOME (SOME pis) =>
   5.174 +             case HOLogic.strip_tupleT T of
   5.175 +               [] => default
   5.176 +             | [_] => default
   5.177 +             | Ts => 
   5.178 +            let
   5.179 +              val vnames = Name.variant_list (param_names @ argnames)
   5.180 +                (map (fn j => "x" ^ string_of_int (length Ts1' + i) ^ "p" ^ string_of_int j)
   5.181 +                  (1 upto (length Ts)))
   5.182 +             in (HOLogic.mk_tuple (map Free (vnames ~~ Ts)), vnames  @ argnames) end
   5.183 +    end
   5.184 +  val (args, argnames) = fold_map mk_args (1 upto (length Ts2) ~~ Ts2) []
   5.185    val (inargs, outargs) = split_smode is args
   5.186    val param_names' = Name.variant_list (param_names @ argnames)
   5.187      (map (fn i => "p" ^ string_of_int i) (1 upto (length iss)))
   5.188 @@ -1443,7 +1443,7 @@
   5.189                     HOLogic.mk_tuple outargs))
   5.190    val introtrm = Logic.list_implies (predpropI :: param_eqs, funpropI)
   5.191    val simprules = [defthm, @{thm eval_pred},
   5.192 -	  @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]
   5.193 +    @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]
   5.194    val unfolddef_tac = Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps simprules) 1
   5.195    val introthm = Goal.prove (ProofContext.init thy) (argnames @ param_names @ param_names' @ ["y"]) [] introtrm (fn {...} => unfolddef_tac)
   5.196    val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT));
   5.197 @@ -1466,30 +1466,30 @@
   5.198    end;
   5.199  
   5.200  fun split_tupleT is T =
   5.201 -	let
   5.202 -		fun split_tuple' _ _ [] = ([], [])
   5.203 -			| split_tuple' is i (T::Ts) =
   5.204 -			(if i mem is then apfst else apsnd) (cons T)
   5.205 -				(split_tuple' is (i+1) Ts)
   5.206 -	in
   5.207 -	  split_tuple' is 1 (HOLogic.strip_tupleT T)
   5.208 +  let
   5.209 +    fun split_tuple' _ _ [] = ([], [])
   5.210 +      | split_tuple' is i (T::Ts) =
   5.211 +      (if i mem is then apfst else apsnd) (cons T)
   5.212 +        (split_tuple' is (i+1) Ts)
   5.213 +  in
   5.214 +    split_tuple' is 1 (HOLogic.strip_tupleT T)
   5.215    end
   5.216 -	
   5.217 +  
   5.218  fun mk_arg xin xout pis T =
   5.219    let
   5.220 -	  val n = length (HOLogic.strip_tupleT T)
   5.221 -		val ni = length pis
   5.222 -	  fun mk_proj i j t =
   5.223 -		  (if i = j then I else HOLogic.mk_fst)
   5.224 -			  (funpow (i - 1) HOLogic.mk_snd t)
   5.225 -	  fun mk_arg' i (si, so) = if i mem pis then
   5.226 -		    (mk_proj si ni xin, (si+1, so))
   5.227 -		  else
   5.228 -			  (mk_proj so (n - ni) xout, (si, so+1))
   5.229 -	  val (args, _) = fold_map mk_arg' (1 upto n) (1, 1)
   5.230 -	in
   5.231 -	  HOLogic.mk_tuple args
   5.232 -	end
   5.233 +    val n = length (HOLogic.strip_tupleT T)
   5.234 +    val ni = length pis
   5.235 +    fun mk_proj i j t =
   5.236 +      (if i = j then I else HOLogic.mk_fst)
   5.237 +        (funpow (i - 1) HOLogic.mk_snd t)
   5.238 +    fun mk_arg' i (si, so) = if i mem pis then
   5.239 +        (mk_proj si ni xin, (si+1, so))
   5.240 +      else
   5.241 +        (mk_proj so (n - ni) xout, (si, so+1))
   5.242 +    val (args, _) = fold_map mk_arg' (1 upto n) (1, 1)
   5.243 +  in
   5.244 +    HOLogic.mk_tuple args
   5.245 +  end
   5.246  
   5.247  fun create_definitions preds (name, modes) thy =
   5.248    let
   5.249 @@ -1505,37 +1505,37 @@
   5.250        val funT = (Ts1' @ Us1) ---> (mk_predT compfuns (HOLogic.mk_tupleT Us2))
   5.251        val names = Name.variant_list []
   5.252          (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
   5.253 -			(* old *)
   5.254 -			(*
   5.255 -		  val xs = map Free (names ~~ (Ts1' @ Ts2))
   5.256 +      (* old *)
   5.257 +      (*
   5.258 +      val xs = map Free (names ~~ (Ts1' @ Ts2))
   5.259        val (xparams, xargs) = chop (length iss) xs
   5.260        val (xins, xouts) = split_smode is xargs
   5.261 -			*)
   5.262 -			(* new *)
   5.263 -			val param_names = Name.variant_list []
   5.264 -			  (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts1')))
   5.265 -		  val xparams = map Free (param_names ~~ Ts1')
   5.266 +      *)
   5.267 +      (* new *)
   5.268 +      val param_names = Name.variant_list []
   5.269 +        (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts1')))
   5.270 +      val xparams = map Free (param_names ~~ Ts1')
   5.271        fun mk_vars (i, T) names =
   5.272 -			  let
   5.273 -				  val vname = Name.variant names ("x" ^ string_of_int (length Ts1' + i))
   5.274 -				in
   5.275 -					case AList.lookup (op =) is i of
   5.276 -						 NONE => ((([], [Free (vname, T)]), Free (vname, T)), vname :: names)
   5.277 -					 | SOME NONE => ((([Free (vname, T)], []), Free (vname, T)), vname :: names)
   5.278 -        	 | SOME (SOME pis) =>
   5.279 -					   let
   5.280 -						   val (Tins, Touts) = split_tupleT pis T
   5.281 -							 val name_in = Name.variant names ("x" ^ string_of_int (length Ts1' + i) ^ "in")
   5.282 -							 val name_out = Name.variant names ("x" ^ string_of_int (length Ts1' + i) ^ "out")
   5.283 -						   val xin = Free (name_in, HOLogic.mk_tupleT Tins)
   5.284 -							 val xout = Free (name_out, HOLogic.mk_tupleT Touts)
   5.285 -							 val xarg = mk_arg xin xout pis T
   5.286 -						 in (((if null Tins then [] else [xin], if null Touts then [] else [xout]), xarg), name_in :: name_out :: names) end
   5.287 -						 end
   5.288 -   	  val (xinoutargs, names) = fold_map mk_vars ((1 upto (length Ts2)) ~~ Ts2) param_names
   5.289 +        let
   5.290 +          val vname = Name.variant names ("x" ^ string_of_int (length Ts1' + i))
   5.291 +        in
   5.292 +          case AList.lookup (op =) is i of
   5.293 +             NONE => ((([], [Free (vname, T)]), Free (vname, T)), vname :: names)
   5.294 +           | SOME NONE => ((([Free (vname, T)], []), Free (vname, T)), vname :: names)
   5.295 +           | SOME (SOME pis) =>
   5.296 +             let
   5.297 +               val (Tins, Touts) = split_tupleT pis T
   5.298 +               val name_in = Name.variant names ("x" ^ string_of_int (length Ts1' + i) ^ "in")
   5.299 +               val name_out = Name.variant names ("x" ^ string_of_int (length Ts1' + i) ^ "out")
   5.300 +               val xin = Free (name_in, HOLogic.mk_tupleT Tins)
   5.301 +               val xout = Free (name_out, HOLogic.mk_tupleT Touts)
   5.302 +               val xarg = mk_arg xin xout pis T
   5.303 +             in (((if null Tins then [] else [xin], if null Touts then [] else [xout]), xarg), name_in :: name_out :: names) end
   5.304 +             end
   5.305 +      val (xinoutargs, names) = fold_map mk_vars ((1 upto (length Ts2)) ~~ Ts2) param_names
   5.306        val (xinout, xargs) = split_list xinoutargs
   5.307 -			val (xins, xouts) = pairself flat (split_list xinout)
   5.308 -			val (xparams', names') = fold_map (mk_Eval_of []) ((xparams ~~ Ts1) ~~ iss) names
   5.309 +      val (xins, xouts) = pairself flat (split_list xinout)
   5.310 +      val (xparams', names') = fold_map (mk_Eval_of []) ((xparams ~~ Ts1) ~~ iss) names
   5.311        fun mk_split_lambda [] t = lambda (Free (Name.variant names' "x", HOLogic.unitT)) t
   5.312          | mk_split_lambda [x] t = lambda x t
   5.313          | mk_split_lambda xs t =
   5.314 @@ -1555,7 +1555,7 @@
   5.315        val (intro, elim) =
   5.316          create_intro_elim_rule mode definition mode_cname funT (Const (name, T)) thy'
   5.317        in thy'
   5.318 -			  |> add_predfun name mode (mode_cname, definition, intro, elim)
   5.319 +        |> add_predfun name mode (mode_cname, definition, intro, elim)
   5.320          |> PureThy.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd
   5.321          |> PureThy.store_thm (Binding.name (mode_cbasename ^ "E"), elim)  |> snd
   5.322          |> Theory.checkpoint
   5.323 @@ -1635,7 +1635,7 @@
   5.324        Const (name, T) => simp_tac (HOL_basic_ss addsimps 
   5.325           ([@{thm eval_pred}, (predfun_definition_of thy name mode),
   5.326           @{thm "split_eta"}, @{thm "split_beta"}, @{thm "fst_conv"},
   5.327 -				 @{thm "snd_conv"}, @{thm pair_collapse}, @{thm "Product_Type.split_conv"}])) 1
   5.328 +         @{thm "snd_conv"}, @{thm pair_collapse}, @{thm "Product_Type.split_conv"}])) 1
   5.329      | Free _ => TRY (rtac @{thm refl} 1)
   5.330      | Abs _ => error "prove_param: No valid parameter term"
   5.331    in
   5.332 @@ -1669,12 +1669,12 @@
   5.333          THEN (REPEAT_DETERM (atac 1))
   5.334        end
   5.335    | _ => rtac @{thm bindI} 1
   5.336 -	  THEN asm_full_simp_tac
   5.337 -		  (HOL_basic_ss' addsimps [@{thm "split_eta"}, @{thm "split_beta"}, @{thm "fst_conv"},
   5.338 -				 @{thm "snd_conv"}, @{thm pair_collapse}]) 1
   5.339 -	  THEN (atac 1)
   5.340 -	  THEN print_tac "after prove parameter call"
   5.341 -		
   5.342 +    THEN asm_full_simp_tac
   5.343 +      (HOL_basic_ss' addsimps [@{thm "split_eta"}, @{thm "split_beta"}, @{thm "fst_conv"},
   5.344 +         @{thm "snd_conv"}, @{thm pair_collapse}]) 1
   5.345 +    THEN (atac 1)
   5.346 +    THEN print_tac "after prove parameter call"
   5.347 +    
   5.348  
   5.349  fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st; 
   5.350  
   5.351 @@ -1725,9 +1725,9 @@
   5.352      val (in_ts, clause_out_ts) = split_smode is ts;
   5.353      fun prove_prems out_ts [] =
   5.354        (prove_match thy out_ts)
   5.355 -			THEN print_tac "before simplifying assumptions"
   5.356 +      THEN print_tac "before simplifying assumptions"
   5.357        THEN asm_full_simp_tac HOL_basic_ss' 1
   5.358 -			THEN print_tac "before single intro rule"
   5.359 +      THEN print_tac "before single intro rule"
   5.360        THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
   5.361      | prove_prems out_ts ((p, mode as Mode ((iss, is), _, param_modes)) :: ps) =
   5.362        let
   5.363 @@ -1793,7 +1793,7 @@
   5.364      val pred_case_rule = the_elim_of thy pred
   5.365    in
   5.366      REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"}))
   5.367 -		THEN print_tac' options "before applying elim rule"
   5.368 +    THEN print_tac' options "before applying elim rule"
   5.369      THEN etac (predfun_elim_of thy pred mode) 1
   5.370      THEN etac pred_case_rule 1
   5.371      THEN (EVERY (map
   5.372 @@ -1911,7 +1911,7 @@
   5.373        THEN (print_tac "state before assumption matching")
   5.374        THEN (REPEAT (atac 1 ORELSE 
   5.375           (CHANGED (asm_full_simp_tac (HOL_basic_ss' addsimps
   5.376 -					 [@{thm split_eta}, @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]) 1)
   5.377 +           [@{thm split_eta}, @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]) 1)
   5.378            THEN print_tac "state after simp_tac:"))))
   5.379      | prove_prems2 out_ts ((p, mode as Mode ((iss, is), _, param_modes)) :: ps) =
   5.380        let
   5.381 @@ -1987,7 +1987,7 @@
   5.382        (if not (skip_proof options) then
   5.383          (fn _ =>
   5.384          rtac @{thm pred_iffI} 1
   5.385 -				THEN print_tac' options "after pred_iffI"
   5.386 +        THEN print_tac' options "after pred_iffI"
   5.387          THEN prove_one_direction options thy clauses preds modes pred mode moded_clauses
   5.388          THEN print_tac' options "proved one direction"
   5.389          THEN prove_other_direction options thy modes pred mode moded_clauses