src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
 changeset 33268 02de0317f66f parent 33212 f3c8acbff503 child 33639 603320b93668
```     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.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))"
```