src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
changeset 41816 7a55699805dc
parent 41809 6799f95479e2
parent 41807 ab5d2d81f9fb
child 41821 c118ae98dfbf
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Feb 21 23:14:36 2011 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Feb 21 23:54:53 2011 +0100
     1.3 @@ -144,11 +144,10 @@
     1.4    {assume nxs: "n \<ge> length (x#xs)" hence ?case using removen_same[OF nxs] by simp}
     1.5    moreover
     1.6    {assume nxs: "\<not> (n \<ge> length (x#xs))" 
     1.7 -    {assume mln: "m < n" hence ?case using prems by (cases m, auto)}
     1.8 +    {assume mln: "m < n" hence ?case using Cons by (cases m, auto)}
     1.9      moreover
    1.10      {assume mln: "\<not> (m < n)" 
    1.11 -      
    1.12 -      {assume mxs: "m \<le> length (x#xs)" hence ?case using prems by (cases m, auto)}
    1.13 +      {assume mxs: "m \<le> length (x#xs)" hence ?case using Cons 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 @@ -162,15 +161,13 @@
    1.18        ultimately have ?case by blast
    1.19      }
    1.20      ultimately have ?case by blast
    1.21 -    
    1.22 -  }      ultimately show ?case by blast
    1.23 +  } ultimately show ?case by blast
    1.24  qed
    1.25  
    1.26  lemma decrtm: assumes bnd: "tmboundslt (length bs) t" and nb: "tmbound m t" 
    1.27    and nle: "m \<le> length bs" 
    1.28    shows "Itm vs (removen m bs) (decrtm m t) = Itm vs bs t"
    1.29 -  using bnd nb nle
    1.30 -  by (induct t rule: tm.induct, auto simp add: removen_nth)
    1.31 +  using bnd nb nle by (induct t rule: tm.induct) (auto simp add: removen_nth)
    1.32  
    1.33  primrec tmsubst0:: "tm \<Rightarrow> tm \<Rightarrow> tm" where
    1.34    "tmsubst0 t (CP c) = CP c"
    1.35 @@ -182,10 +179,10 @@
    1.36  | "tmsubst0 t (Mul i a) = Mul i (tmsubst0 t a)"
    1.37  lemma tmsubst0:
    1.38    shows "Itm vs (x#bs) (tmsubst0 t a) = Itm vs ((Itm vs (x#bs) t)#bs) a"
    1.39 -by (induct a rule: tm.induct,auto simp add: nth_pos2)
    1.40 +  by (induct a rule: tm.induct) (auto simp add: nth_pos2)
    1.41  
    1.42  lemma tmsubst0_nb: "tmbound0 t \<Longrightarrow> tmbound0 (tmsubst0 t a)"
    1.43 -by (induct a rule: tm.induct,auto simp add: nth_pos2)
    1.44 +  by (induct a rule: tm.induct) (auto simp add: nth_pos2)
    1.45  
    1.46  primrec tmsubst:: "nat \<Rightarrow> tm \<Rightarrow> tm \<Rightarrow> tm" where
    1.47    "tmsubst n t (CP c) = CP c"
    1.48 @@ -569,13 +566,13 @@
    1.49  proof(induct p arbitrary: bs n rule: fm.induct)
    1.50    case (E p bs n) 
    1.51    {fix y
    1.52 -    from prems have bnd: "boundslt (length (y#bs)) p" 
    1.53 +    from E have bnd: "boundslt (length (y#bs)) p" 
    1.54        and nb: "bound (Suc n) p" and le: "Suc n \<le> length (y#bs)" by simp+
    1.55      from E.hyps[OF bnd nb le tmbound_I] have "Ifm vs ((y#bs)[Suc n:=x]) p = Ifm vs (y#bs) p" .   }
    1.56    thus ?case by simp 
    1.57  next
    1.58    case (A p bs n) {fix y
    1.59 -    from prems have bnd: "boundslt (length (y#bs)) p" 
    1.60 +    from A have bnd: "boundslt (length (y#bs)) p" 
    1.61        and nb: "bound (Suc n) p" and le: "Suc n \<le> length (y#bs)" by simp+
    1.62      from A.hyps[OF bnd nb le tmbound_I] have "Ifm vs ((y#bs)[Suc n:=x]) p = Ifm vs (y#bs) p" .   }
    1.63    thus ?case by simp 
    1.64 @@ -620,16 +617,16 @@
    1.65  proof(induct p arbitrary: bs m rule: fm.induct)
    1.66    case (E p bs m) 
    1.67    {fix x
    1.68 -    from prems have bnd: "boundslt (length (x#bs)) p" and nb: "bound (Suc m) p" 
    1.69 +    from E have bnd: "boundslt (length (x#bs)) p" and nb: "bound (Suc m) p" 
    1.70    and nle: "Suc m < length (x#bs)" by auto
    1.71 -    from prems(4)[OF bnd nb nle] have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p".
    1.72 +    from E(1)[OF bnd nb nle] have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p".
    1.73    } thus ?case by auto 
    1.74  next
    1.75    case (A p bs m)  
    1.76    {fix x
    1.77 -    from prems have bnd: "boundslt (length (x#bs)) p" and nb: "bound (Suc m) p" 
    1.78 +    from A have bnd: "boundslt (length (x#bs)) p" and nb: "bound (Suc m) p" 
    1.79    and nle: "Suc m < length (x#bs)" by auto
    1.80 -    from prems(4)[OF bnd nb nle] have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p".
    1.81 +    from A(1)[OF bnd nb nle] have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p".
    1.82    } thus ?case by auto
    1.83  qed (auto simp add: decrtm removen_nth)
    1.84  
    1.85 @@ -680,18 +677,18 @@
    1.86  proof (induct p arbitrary: bs n t rule: fm.induct)
    1.87    case (E p bs n) 
    1.88    {fix x 
    1.89 -    from prems have bn: "boundslt (length (x#bs)) p" by simp 
    1.90 -      from prems have nlm: "Suc n \<le> length (x#bs)" by simp
    1.91 -    from prems(3)[OF bn nlm] have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = Ifm vs ((x#bs)[Suc n:= Itm vs (x#bs) (incrtm0 t)]) p" by simp 
    1.92 +    from E have bn: "boundslt (length (x#bs)) p" by simp 
    1.93 +    from E have nlm: "Suc n \<le> length (x#bs)" by simp
    1.94 +    from E(1)[OF bn nlm] have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = Ifm vs ((x#bs)[Suc n:= Itm vs (x#bs) (incrtm0 t)]) p" by simp 
    1.95      hence "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = Ifm vs (x#bs[n:= Itm vs bs t]) p"
    1.96      by (simp add: incrtm0[where x="x" and bs="bs" and t="t"]) }  
    1.97  thus ?case by simp 
    1.98  next
    1.99    case (A p bs n)   
   1.100    {fix x 
   1.101 -    from prems have bn: "boundslt (length (x#bs)) p" by simp 
   1.102 -      from prems have nlm: "Suc n \<le> length (x#bs)" by simp
   1.103 -    from prems(3)[OF bn nlm] have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = Ifm vs ((x#bs)[Suc n:= Itm vs (x#bs) (incrtm0 t)]) p" by simp 
   1.104 +    from A have bn: "boundslt (length (x#bs)) p" by simp 
   1.105 +    from A have nlm: "Suc n \<le> length (x#bs)" by simp
   1.106 +    from A(1)[OF bn nlm] have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = Ifm vs ((x#bs)[Suc n:= Itm vs (x#bs) (incrtm0 t)]) p" by simp 
   1.107      hence "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = Ifm vs (x#bs[n:= Itm vs bs t]) p"
   1.108      by (simp add: incrtm0[where x="x" and bs="bs" and t="t"]) }  
   1.109  thus ?case by simp 
   1.110 @@ -1371,7 +1368,7 @@
   1.111    case 2 thus ?case by (auto,rule_tac x="min z za" in exI, auto)
   1.112  next
   1.113    case (3 c e) hence nbe: "tmbound0 e" by simp
   1.114 -  from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   1.115 +  from 3 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   1.116    note eqs = eq[OF nc(1), where ?'a = 'a] eq[OF nc(2), where ?'a = 'a]
   1.117    let ?c = "Ipoly vs c"
   1.118    let ?e = "Itm vs (y#bs) e"
   1.119 @@ -1393,7 +1390,7 @@
   1.120    ultimately show ?case by blast
   1.121  next
   1.122    case (4 c e)  hence nbe: "tmbound0 e" by simp
   1.123 -  from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   1.124 +  from 4 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   1.125    note eqs = eq[OF nc(1), where ?'a = 'a] eq[OF nc(2), where ?'a = 'a]
   1.126    let ?c = "Ipoly vs c"
   1.127    let ?e = "Itm vs (y#bs) e"
   1.128 @@ -1414,7 +1411,7 @@
   1.129    ultimately show ?case by blast
   1.130  next
   1.131    case (5 c e)  hence nbe: "tmbound0 e" by simp
   1.132 -  from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   1.133 +  from 5 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   1.134    hence nc': "allpolys isnpoly (CP (~\<^sub>p c))" by (simp add: polyneg_norm)
   1.135    note eqs = lt[OF nc', where ?'a = 'a] eq [OF nc(1), where ?'a = 'a] lt[OF nc(2), where ?'a = 'a]
   1.136    let ?c = "Ipoly vs c"
   1.137 @@ -1436,7 +1433,7 @@
   1.138    ultimately show ?case by blast
   1.139  next
   1.140    case (6 c e)  hence nbe: "tmbound0 e" by simp
   1.141 -  from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   1.142 +  from 6 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   1.143    hence nc': "allpolys isnpoly (CP (~\<^sub>p c))" by (simp add: polyneg_norm)
   1.144    note eqs = lt[OF nc', where ?'a = 'a] eq [OF nc(1), where ?'a = 'a] le[OF nc(2), where ?'a = 'a]
   1.145    let ?c = "Ipoly vs c"
   1.146 @@ -1467,7 +1464,7 @@
   1.147    case 2 thus ?case by (auto,rule_tac x="max z za" in exI, auto)
   1.148  next
   1.149    case (3 c e) hence nbe: "tmbound0 e" by simp
   1.150 -  from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   1.151 +  from 3 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   1.152    note eqs = eq[OF nc(1), where ?'a = 'a] eq[OF nc(2), where ?'a = 'a]
   1.153    let ?c = "Ipoly vs c"
   1.154    let ?e = "Itm vs (y#bs) e"
   1.155 @@ -1488,8 +1485,8 @@
   1.156          using tmbound0_I[OF nbe, where b="y" and b'="x"] eqs by auto} hence ?case by auto}
   1.157    ultimately show ?case by blast
   1.158  next
   1.159 -  case (4 c e)  hence nbe: "tmbound0 e" by simp
   1.160 -  from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   1.161 +  case (4 c e) hence nbe: "tmbound0 e" by simp
   1.162 +  from 4 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   1.163    note eqs = eq[OF nc(1), where ?'a = 'a] eq[OF nc(2), where ?'a = 'a]
   1.164    let ?c = "Ipoly vs c"
   1.165    let ?e = "Itm vs (y#bs) e"
   1.166 @@ -1509,8 +1506,8 @@
   1.167          using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto}
   1.168    ultimately show ?case by blast
   1.169  next
   1.170 -  case (5 c e)  hence nbe: "tmbound0 e" by simp
   1.171 -  from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   1.172 +  case (5 c e) hence nbe: "tmbound0 e" by simp
   1.173 +  from 5 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   1.174    hence nc': "allpolys isnpoly (CP (~\<^sub>p c))" by (simp add: polyneg_norm)
   1.175    note eqs = lt[OF nc(1), where ?'a = 'a] lt[OF nc', where ?'a = 'a] eq [OF nc(1), where ?'a = 'a] lt[OF nc(2), where ?'a = 'a]
   1.176    let ?c = "Ipoly vs c"
   1.177 @@ -1532,7 +1529,7 @@
   1.178    ultimately show ?case by blast
   1.179  next
   1.180    case (6 c e)  hence nbe: "tmbound0 e" by simp
   1.181 -  from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   1.182 +  from 6 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   1.183    hence nc': "allpolys isnpoly (CP (~\<^sub>p c))" by (simp add: polyneg_norm)
   1.184    note eqs = lt[OF nc(1), where ?'a = 'a] eq [OF nc(1), where ?'a = 'a] le[OF nc(2), where ?'a = 'a]
   1.185    let ?c = "Ipoly vs c"