author wenzelm Wed Oct 28 00:24:38 2009 +0100 (2009-10-28) changeset 33268 02de0317f66f parent 33267 8fb01a2f9406 child 33272 73a0c804840f child 33276 f2bc8bc6e73d child 33326 7d0288d90535
eliminated hard tabulators, guessing at each author's individual tab-width;
```     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.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.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.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.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.351 -	by (simp add: mult_commute)}
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.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.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.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.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
```