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.275        apply (simp only: one_add_one_is_two[symmetric] of_int_add)
   1.276 @@ -2270,7 +2270,7 @@
   1.277        using d order_less_not_sym[OF d''] less_imp_neq[OF d''] d'' mult_less_cancel_left_disj[of "(1 + 1) * ?d" 0 "?a* (- ?s / ((1 + 1)*?d))+ ?r"] by simp
   1.278      also have "\<dots> \<longleftrightarrow> ?a*?s -  (1 + 1)*?d *?r < 0" 
   1.279        using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d''] less_imp_neq[OF d''] d''
   1.280 -	by (simp add: ring_simps diff_divide_distrib del:  left_distrib)
   1.281 +        by (simp add: ring_simps diff_divide_distrib del:  left_distrib)
   1.282      finally have ?thesis using c d nc nd 
   1.283        apply(simp add: r[of "- (?s / ((1 + 1)*?d))"] msubstlt_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm)
   1.284        apply (simp only: one_add_one_is_two[symmetric] of_int_add)
   1.285 @@ -2392,7 +2392,7 @@
   1.286        using c order_less_not_sym[OF c''] less_imp_neq[OF c''] c'' mult_le_cancel_left[of "(1 + 1) * ?c" 0 "?a* (- ?t / ((1 + 1)*?c))+ ?r"] by simp
   1.287      also have "\<dots> \<longleftrightarrow> ?a*?t -  (1 + 1)*?c *?r <= 0" 
   1.288        using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c''] less_imp_neq[OF c''] c''
   1.289 -	by (simp add: ring_simps diff_divide_distrib del:  left_distrib)
   1.290 +        by (simp add: ring_simps diff_divide_distrib del:  left_distrib)
   1.291      finally have ?thesis using c d nc nd 
   1.292        apply(simp add: r[of "- (?t / ((1 + 1)*?c))"] msubstle_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm)
   1.293        apply (simp only: one_add_one_is_two[symmetric] of_int_add)
   1.294 @@ -2426,7 +2426,7 @@
   1.295        using d order_less_not_sym[OF d''] less_imp_neq[OF d''] d'' mult_le_cancel_left[of "(1 + 1) * ?d" 0 "?a* (- ?s / ((1 + 1)*?d))+ ?r"] by simp
   1.296      also have "\<dots> \<longleftrightarrow> ?a*?s -  (1 + 1)*?d *?r <= 0" 
   1.297        using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d''] less_imp_neq[OF d''] d''
   1.298 -	by (simp add: ring_simps diff_divide_distrib del:  left_distrib)
   1.299 +        by (simp add: ring_simps diff_divide_distrib del:  left_distrib)
   1.300      finally have ?thesis using c d nc nd 
   1.301        apply(simp add: r[of "- (?s / ((1 + 1)*?d))"] msubstle_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm)
   1.302        apply (simp only: one_add_one_is_two[symmetric] of_int_add)
   1.303 @@ -2638,8 +2638,8 @@
   1.304      moreover
   1.305      {assume z: "?c \<noteq> 0" "?d \<noteq> 0"
   1.306        from z have ?F using ct
   1.307 -	apply - apply (rule bexI[where x = "(c,t)"], simp_all)
   1.308 -	by (rule bexI[where x = "(d,s)"], simp_all)
   1.309 +        apply - apply (rule bexI[where x = "(c,t)"], simp_all)
   1.310 +        by (rule bexI[where x = "(d,s)"], simp_all)
   1.311        hence ?D by blast}
   1.312      ultimately have ?D by auto}
   1.313    ultimately show "?D" by blast
   1.314 @@ -2799,17 +2799,17 @@
   1.315        from H(1) th have "isnpoly n" by blast
   1.316        hence nn: "isnpoly (n *\<^sub>p (C (-2,1)))" by (simp_all add: polymul_norm n2)
   1.317        have nn': "allpolys isnpoly (CP (~\<^sub>p (n *\<^sub>p C (-2, 1))))"
   1.318 -	by (simp add: polyneg_norm nn)
   1.319 +        by (simp add: polyneg_norm nn)
   1.320        hence nn2: "\<lparr>n *\<^sub>p(C (-2,1)) \<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>n \<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" using H(2) nn' nn 
   1.321 -	by (auto simp add: msubst2_def lt zero_less_mult_iff mult_less_0_iff)
   1.322 +        by (auto simp add: msubst2_def lt zero_less_mult_iff mult_less_0_iff)
   1.323        from msubst2[OF lp nn nn2(1), of x bs t]
   1.324        have "\<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and> Ifm vs (- Itm vs (x # bs) t / (\<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> * (1 + 1)) # bs) p"
   1.325 -	using H(2) nn2 by (simp add: of_int_minus2 del: minus_add_distrib)}
   1.326 +        using H(2) nn2 by (simp add: of_int_minus2 del: minus_add_distrib)}
   1.327      moreover
   1.328      {fix n t assume H: "(n, t)\<in>set (uset p)" "\<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "Ifm vs (- Itm vs (x # bs) t / (\<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> * (1 + 1)) # bs) p"
   1.329        from H(1) th have "isnpoly n" by blast
   1.330        hence nn: "isnpoly (n *\<^sub>p (C (-2,1)))" "\<lparr>n *\<^sub>p(C (-2,1)) \<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
   1.331 -	using H(2) by (simp_all add: polymul_norm n2)
   1.332 +        using H(2) by (simp_all add: polymul_norm n2)
   1.333        from msubst2[OF lp nn, of x bs t] have "?I (msubst2 p (n *\<^sub>p (C (-2,1))) t)" using H(2,3) by (simp add: of_int_minus2 del: minus_add_distrib)}
   1.334      ultimately show ?thesis by blast
   1.335    qed
   1.336 @@ -2820,21 +2820,21 @@
   1.337       "Ifm vs (x#bs) (msubst2 p (C (-2, 1) *\<^sub>p c*\<^sub>p d) (Add (Mul d t) (Mul c s)))"
   1.338        from H(1,2) th have "isnpoly c" "isnpoly d" by blast+
   1.339        hence nn: "isnpoly (C (-2, 1) *\<^sub>p c*\<^sub>p d)" 
   1.340 -	by (simp_all add: polymul_norm n2)
   1.341 +        by (simp_all add: polymul_norm n2)
   1.342        have stupid: "allpolys isnpoly (CP (~\<^sub>p (C (-2, 1) *\<^sub>p c *\<^sub>p d)))" "allpolys isnpoly (CP ((C (-2, 1) *\<^sub>p c *\<^sub>p d)))"
   1.343 -	by (simp_all add: polyneg_norm nn)
   1.344 +        by (simp_all add: polyneg_norm nn)
   1.345        have nn': "\<lparr>(C (-2, 1) *\<^sub>p c*\<^sub>p d)\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
   1.346 -	using H(3) by (auto simp add: msubst2_def lt[OF stupid(1)]  lt[OF stupid(2)] zero_less_mult_iff mult_less_0_iff)
   1.347 +        using H(3) by (auto simp add: msubst2_def lt[OF stupid(1)]  lt[OF stupid(2)] zero_less_mult_iff mult_less_0_iff)
   1.348        from msubst2[OF lp nn nn'(1), of x bs ] H(3) nn'
   1.349        have "\<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and> \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and> Ifm vs ((- Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>) / (1 + 1) # bs) p" 
   1.350 -	apply (simp add: add_divide_distrib of_int_minus2 del: minus_add_distrib)
   1.351 -	by (simp add: mult_commute)}
   1.352 +        apply (simp add: add_divide_distrib of_int_minus2 del: minus_add_distrib)
   1.353 +        by (simp add: mult_commute)}
   1.354      moreover
   1.355      {fix c t d s assume H: "(c,t) \<in> set (uset p)" "(d,s) \<in> set (uset p)" 
   1.356        "\<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "Ifm vs ((- Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>) / (1 + 1) # bs) p"
   1.357       from H(1,2) th have "isnpoly c" "isnpoly d" by blast+
   1.358        hence nn: "isnpoly (C (-2, 1) *\<^sub>p c*\<^sub>p d)" "\<lparr>(C (-2, 1) *\<^sub>p c*\<^sub>p d)\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
   1.359 -	using H(3,4) by (simp_all add: polymul_norm n2)
   1.360 +        using H(3,4) by (simp_all add: polymul_norm n2)
   1.361        from msubst2[OF lp nn, of x bs ] H(3,4,5) 
   1.362        have "Ifm vs (x#bs) (msubst2 p (C (-2, 1) *\<^sub>p c*\<^sub>p d) (Add (Mul d t) (Mul c s)))" apply (simp add: add_divide_distrib of_int_minus2 del: minus_add_distrib)by (simp add: mult_commute)}
   1.363      ultimately show ?thesis by blast
   1.364 @@ -2906,16 +2906,16 @@
   1.365      proof
   1.366        assume H: ?lhs
   1.367        hence z: "\<lparr>C (-2, 1) *\<^sub>p b *\<^sub>p d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>C (-2, 1) *\<^sub>p d *\<^sub>p b\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" 
   1.368 -	by (auto simp add: msubst2_def lt[OF stupid(3)] lt[OF stupid(1)] mult_less_0_iff zero_less_mult_iff)
   1.369 +        by (auto simp add: msubst2_def lt[OF stupid(3)] lt[OF stupid(1)] mult_less_0_iff zero_less_mult_iff)
   1.370        from msubst2[OF lq norm2(1) z(1), of x bs] 
   1.371 -	msubst2[OF lq norm2(2) z(2), of x bs] H 
   1.372 +        msubst2[OF lq norm2(2) z(2), of x bs] H 
   1.373        show ?rhs by (simp add: ring_simps)
   1.374      next
   1.375        assume H: ?rhs
   1.376        hence z: "\<lparr>C (-2, 1) *\<^sub>p b *\<^sub>p d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>C (-2, 1) *\<^sub>p d *\<^sub>p b\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" 
   1.377 -	by (auto simp add: msubst2_def lt[OF stupid(4)] lt[OF stupid(2)] mult_less_0_iff zero_less_mult_iff)
   1.378 +        by (auto simp add: msubst2_def lt[OF stupid(4)] lt[OF stupid(2)] mult_less_0_iff zero_less_mult_iff)
   1.379        from msubst2[OF lq norm2(1) z(1), of x bs] 
   1.380 -	msubst2[OF lq norm2(2) z(2), of x bs] H 
   1.381 +        msubst2[OF lq norm2(2) z(2), of x bs] H 
   1.382        show ?lhs by (simp add: ring_simps)
   1.383      qed}
   1.384    hence th0: "\<forall>x \<in> set ?U. \<forall>y \<in> set ?U. ?I (?s (x, y)) \<longleftrightarrow> ?I (?s (y, x))"