summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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"