--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Wed Oct 28 00:23:39 2009 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Wed Oct 28 00:24:38 2009 +0100
@@ -35,7 +35,7 @@
"Itm vs bs (Add a b) = Itm vs bs a + Itm vs bs b"
"Itm vs bs (Sub a b) = Itm vs bs a - Itm vs bs b"
"Itm vs bs (Mul c a) = (Ipoly vs c) * Itm vs bs a"
- "Itm vs bs (CNP n c t) = (Ipoly vs c)*(bs!n) + Itm vs bs t"
+ "Itm vs bs (CNP n c t) = (Ipoly vs c)*(bs!n) + Itm vs bs t"
fun allpolys:: "(poly \<Rightarrow> bool) \<Rightarrow> tm \<Rightarrow> bool" where
@@ -153,14 +153,14 @@
{assume mxs: "m \<le> length (x#xs)" hence ?case using prems by (cases m, auto)}
moreover
{assume mxs: "\<not> (m \<le> length (x#xs))"
- have th: "length (removen n (x#xs)) = length xs"
- using removen_length[where n="n" and xs="x#xs"] nxs by simp
- with mxs have mxs':"m \<ge> length (removen n (x#xs))" by auto
- hence "(removen n (x#xs))!m = [] ! (m - length xs)"
- using th nth_length_exceeds[OF mxs'] by auto
- hence th: "(removen n (x#xs))!m = [] ! (m - (length (x#xs) - 1))"
- by auto
- hence ?case using nxs mln mxs by auto }
+ have th: "length (removen n (x#xs)) = length xs"
+ using removen_length[where n="n" and xs="x#xs"] nxs by simp
+ with mxs have mxs':"m \<ge> length (removen n (x#xs))" by auto
+ hence "(removen n (x#xs))!m = [] ! (m - length xs)"
+ using th nth_length_exceeds[OF mxs'] by auto
+ hence th: "(removen n (x#xs))!m = [] ! (m - (length (x#xs) - 1))"
+ by auto
+ hence ?case using nxs mln mxs by auto }
ultimately have ?case by blast
}
ultimately have ?case by blast
@@ -443,7 +443,7 @@
"fmsize (A p) = 4+ fmsize p"
"fmsize p = 1"
(* several lemmas about fmsize *)
-lemma fmsize_pos: "fmsize p > 0"
+lemma fmsize_pos: "fmsize p > 0"
by (induct p rule: fmsize.induct) simp_all
(* Semantics of formulae (fm) *)
@@ -1393,16 +1393,16 @@
using eq[OF nc(2), of vs] eq[OF nc(1), of vs] by auto}
moreover {assume cp: "?c > 0"
{fix x assume xz: "x < -?e / ?c" hence "?c * x < - ?e"
- using pos_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
+ using pos_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
hence "?c * x + ?e < 0" by simp
hence "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Eq (CNP 0 c e)))"
- using eqs tmbound0_I[OF nbe, where b="y" and b'="x" and vs=vs and bs=bs] by auto} hence ?case by auto}
+ using eqs tmbound0_I[OF nbe, where b="y" and b'="x" and vs=vs and bs=bs] by auto} hence ?case by auto}
moreover {assume cp: "?c < 0"
{fix x assume xz: "x < -?e / ?c" hence "?c * x > - ?e"
- using neg_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
+ using neg_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
hence "?c * x + ?e > 0" by simp
hence "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Eq (CNP 0 c e)))"
- using tmbound0_I[OF nbe, where b="y" and b'="x"] eqs by auto} hence ?case by auto}
+ using tmbound0_I[OF nbe, where b="y" and b'="x"] eqs by auto} hence ?case by auto}
ultimately show ?case by blast
next
case (4 c e) hence nbe: "tmbound0 e" by simp
@@ -1414,16 +1414,16 @@
moreover {assume "?c = 0" hence ?case using eqs by auto}
moreover {assume cp: "?c > 0"
{fix x assume xz: "x < -?e / ?c" hence "?c * x < - ?e"
- using pos_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
+ using pos_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
hence "?c * x + ?e < 0" by simp
hence "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (NEq (CNP 0 c e)))"
- using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto}
+ using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto}
moreover {assume cp: "?c < 0"
{fix x assume xz: "x < -?e / ?c" hence "?c * x > - ?e"
- using neg_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
+ using neg_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
hence "?c * x + ?e > 0" by simp
hence "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (NEq (CNP 0 c e)))"
- using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto}
+ using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto}
ultimately show ?case by blast
next
case (5 c e) hence nbe: "tmbound0 e" by simp
@@ -1436,16 +1436,16 @@
moreover {assume "?c = 0" hence ?case using eqs by auto}
moreover {assume cp: "?c > 0"
{fix x assume xz: "x < -?e / ?c" hence "?c * x < - ?e"
- using pos_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
+ using pos_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
hence "?c * x + ?e < 0" by simp
hence "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Lt (CNP 0 c e)))"
- using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
+ using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
moreover {assume cp: "?c < 0"
{fix x assume xz: "x < -?e / ?c" hence "?c * x > - ?e"
- using neg_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
+ using neg_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
hence "?c * x + ?e > 0" by simp
hence "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Lt (CNP 0 c e)))"
- using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] cp by auto} hence ?case by auto}
+ using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] cp by auto} hence ?case by auto}
ultimately show ?case by blast
next
case (6 c e) hence nbe: "tmbound0 e" by simp
@@ -1458,16 +1458,16 @@
moreover {assume "?c = 0" hence ?case using eqs by auto}
moreover {assume cp: "?c > 0"
{fix x assume xz: "x < -?e / ?c" hence "?c * x < - ?e"
- using pos_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
+ using pos_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
hence "?c * x + ?e < 0" by simp
hence "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Le (CNP 0 c e)))"
- using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
+ using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
moreover {assume cp: "?c < 0"
{fix x assume xz: "x < -?e / ?c" hence "?c * x > - ?e"
- using neg_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
+ using neg_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
hence "?c * x + ?e > 0" by simp
hence "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Le (CNP 0 c e)))"
- using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
+ using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
ultimately show ?case by blast
qed (auto)
@@ -1489,16 +1489,16 @@
using eq[OF nc(2), of vs] eq[OF nc(1), of vs] by auto}
moreover {assume cp: "?c > 0"
{fix x assume xz: "x > -?e / ?c" hence "?c * x > - ?e"
- using pos_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
+ using pos_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
hence "?c * x + ?e > 0" by simp
hence "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Eq (CNP 0 c e)))"
- using eqs tmbound0_I[OF nbe, where b="y" and b'="x" and vs=vs and bs=bs] by auto} hence ?case by auto}
+ using eqs tmbound0_I[OF nbe, where b="y" and b'="x" and vs=vs and bs=bs] by auto} hence ?case by auto}
moreover {assume cp: "?c < 0"
{fix x assume xz: "x > -?e / ?c" hence "?c * x < - ?e"
- using neg_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
+ using neg_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
hence "?c * x + ?e < 0" by simp
hence "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Eq (CNP 0 c e)))"
- using tmbound0_I[OF nbe, where b="y" and b'="x"] eqs by auto} hence ?case by auto}
+ using tmbound0_I[OF nbe, where b="y" and b'="x"] eqs by auto} hence ?case by auto}
ultimately show ?case by blast
next
case (4 c e) hence nbe: "tmbound0 e" by simp
@@ -1510,16 +1510,16 @@
moreover {assume "?c = 0" hence ?case using eqs by auto}
moreover {assume cp: "?c > 0"
{fix x assume xz: "x > -?e / ?c" hence "?c * x > - ?e"
- using pos_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
+ using pos_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
hence "?c * x + ?e > 0" by simp
hence "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (NEq (CNP 0 c e)))"
- using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto}
+ using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto}
moreover {assume cp: "?c < 0"
{fix x assume xz: "x > -?e / ?c" hence "?c * x < - ?e"
- using neg_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
+ using neg_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
hence "?c * x + ?e < 0" by simp
hence "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (NEq (CNP 0 c e)))"
- using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto}
+ using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto}
ultimately show ?case by blast
next
case (5 c e) hence nbe: "tmbound0 e" by simp
@@ -1532,16 +1532,16 @@
moreover {assume "?c = 0" hence ?case using eqs by auto}
moreover {assume cp: "?c > 0"
{fix x assume xz: "x > -?e / ?c" hence "?c * x > - ?e"
- using pos_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
+ using pos_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
hence "?c * x + ?e > 0" by simp
hence "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Lt (CNP 0 c e)))"
- using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
+ using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
moreover {assume cp: "?c < 0"
{fix x assume xz: "x > -?e / ?c" hence "?c * x < - ?e"
- using neg_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
+ using neg_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
hence "?c * x + ?e < 0" by simp
hence "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Lt (CNP 0 c e)))"
- using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] cp by auto} hence ?case by auto}
+ using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] cp by auto} hence ?case by auto}
ultimately show ?case by blast
next
case (6 c e) hence nbe: "tmbound0 e" by simp
@@ -1554,16 +1554,16 @@
moreover {assume "?c = 0" hence ?case using eqs by auto}
moreover {assume cp: "?c > 0"
{fix x assume xz: "x > -?e / ?c" hence "?c * x > - ?e"
- using pos_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
+ using pos_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
hence "?c * x + ?e > 0" by simp
hence "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Le (CNP 0 c e)))"
- using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
+ using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
moreover {assume cp: "?c < 0"
{fix x assume xz: "x > -?e / ?c" hence "?c * x < - ?e"
- using neg_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
+ using neg_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute)
hence "?c * x + ?e < 0" by simp
hence "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Le (CNP 0 c e)))"
- using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
+ using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto}
ultimately show ?case by blast
qed (auto)
@@ -1698,10 +1698,10 @@
{assume c: "?N c > 0"
from px pos_less_divide_eq[OF c, where a="x" and b="-?Nt x s"]
have px': "x < - ?Nt x s / ?N c"
- by (auto simp add: not_less ring_simps)
+ by (auto simp add: not_less ring_simps)
{assume y: "y < - ?Nt x s / ?N c"
hence "y * ?N c < - ?Nt x s"
- by (simp add: pos_less_divide_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
+ by (simp add: pos_less_divide_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
hence "?N c * y + ?Nt x s < 0" by (simp add: ring_simps)
hence ?case using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"] by simp}
moreover
@@ -1715,10 +1715,10 @@
{assume c: "?N c < 0"
from px neg_divide_less_eq[OF c, where a="x" and b="-?Nt x s"]
have px': "x > - ?Nt x s / ?N c"
- by (auto simp add: not_less ring_simps)
+ by (auto simp add: not_less ring_simps)
{assume y: "y > - ?Nt x s / ?N c"
hence "y * ?N c < - ?Nt x s"
- by (simp add: neg_divide_less_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
+ by (simp add: neg_divide_less_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
hence "?N c * y + ?Nt x s < 0" by (simp add: ring_simps)
hence ?case using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"] by simp}
moreover
@@ -1746,7 +1746,7 @@
have px': "x <= - ?Nt x s / ?N c" by (simp add: not_less ring_simps)
{assume y: "y < - ?Nt x s / ?N c"
hence "y * ?N c < - ?Nt x s"
- by (simp add: pos_less_divide_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
+ by (simp add: pos_less_divide_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
hence "?N c * y + ?Nt x s < 0" by (simp add: ring_simps)
hence ?case using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"] by simp}
moreover
@@ -1762,7 +1762,7 @@
have px': "x >= - ?Nt x s / ?N c" by (simp add: ring_simps)
{assume y: "y > - ?Nt x s / ?N c"
hence "y * ?N c < - ?Nt x s"
- by (simp add: neg_divide_less_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
+ by (simp add: neg_divide_less_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
hence "?N c * y + ?Nt x s < 0" by (simp add: ring_simps)
hence ?case using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"] by simp}
moreover
@@ -1899,8 +1899,8 @@
moreover{
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"
then obtain t1 and t2 where t1M: "t1 \<in> ?M" and t2M: "t2\<in> ?M"
- 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"
- by blast
+ 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"
+ by blast
from t1M have "\<exists> (t1n,t1u) \<in> ?U. t1 = - ?Nt a t1u / ?N t1n" by auto
then obtain "t1u" "t1n" where t1uU: "(t1n,t1u) \<in> ?U" and t1u: "t1 = - ?Nt a t1u / ?N t1n" by blast
from t2M have "\<exists> (t2n,t2u) \<in> ?U. t2 = - ?Nt a t2u / ?N t2n" by auto
@@ -2236,7 +2236,7 @@
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
also have "\<dots> \<longleftrightarrow> ?a*?t - (1 + 1)*?c *?r < 0"
using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c''] less_imp_neq[OF c''] c''
- by (simp add: ring_simps diff_divide_distrib del: left_distrib)
+ by (simp add: ring_simps diff_divide_distrib del: left_distrib)
finally have ?thesis using c d nc nd
apply(simp add: r[of "- (?t / ((1 + 1)*?c))"] msubstlt_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm)
apply (simp only: one_add_one_is_two[symmetric] of_int_add)
@@ -2270,7 +2270,7 @@
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
also have "\<dots> \<longleftrightarrow> ?a*?s - (1 + 1)*?d *?r < 0"
using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d''] less_imp_neq[OF d''] d''
- by (simp add: ring_simps diff_divide_distrib del: left_distrib)
+ by (simp add: ring_simps diff_divide_distrib del: left_distrib)
finally have ?thesis using c d nc nd
apply(simp add: r[of "- (?s / ((1 + 1)*?d))"] msubstlt_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm)
apply (simp only: one_add_one_is_two[symmetric] of_int_add)
@@ -2392,7 +2392,7 @@
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
also have "\<dots> \<longleftrightarrow> ?a*?t - (1 + 1)*?c *?r <= 0"
using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c''] less_imp_neq[OF c''] c''
- by (simp add: ring_simps diff_divide_distrib del: left_distrib)
+ by (simp add: ring_simps diff_divide_distrib del: left_distrib)
finally have ?thesis using c d nc nd
apply(simp add: r[of "- (?t / ((1 + 1)*?c))"] msubstle_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm)
apply (simp only: one_add_one_is_two[symmetric] of_int_add)
@@ -2426,7 +2426,7 @@
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
also have "\<dots> \<longleftrightarrow> ?a*?s - (1 + 1)*?d *?r <= 0"
using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d''] less_imp_neq[OF d''] d''
- by (simp add: ring_simps diff_divide_distrib del: left_distrib)
+ by (simp add: ring_simps diff_divide_distrib del: left_distrib)
finally have ?thesis using c d nc nd
apply(simp add: r[of "- (?s / ((1 + 1)*?d))"] msubstle_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm)
apply (simp only: one_add_one_is_two[symmetric] of_int_add)
@@ -2638,8 +2638,8 @@
moreover
{assume z: "?c \<noteq> 0" "?d \<noteq> 0"
from z have ?F using ct
- apply - apply (rule bexI[where x = "(c,t)"], simp_all)
- by (rule bexI[where x = "(d,s)"], simp_all)
+ apply - apply (rule bexI[where x = "(c,t)"], simp_all)
+ by (rule bexI[where x = "(d,s)"], simp_all)
hence ?D by blast}
ultimately have ?D by auto}
ultimately show "?D" by blast
@@ -2799,17 +2799,17 @@
from H(1) th have "isnpoly n" by blast
hence nn: "isnpoly (n *\<^sub>p (C (-2,1)))" by (simp_all add: polymul_norm n2)
have nn': "allpolys isnpoly (CP (~\<^sub>p (n *\<^sub>p C (-2, 1))))"
- by (simp add: polyneg_norm nn)
+ by (simp add: polyneg_norm nn)
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
- by (auto simp add: msubst2_def lt zero_less_mult_iff mult_less_0_iff)
+ by (auto simp add: msubst2_def lt zero_less_mult_iff mult_less_0_iff)
from msubst2[OF lp nn nn2(1), of x bs t]
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"
- using H(2) nn2 by (simp add: of_int_minus2 del: minus_add_distrib)}
+ using H(2) nn2 by (simp add: of_int_minus2 del: minus_add_distrib)}
moreover
{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"
from H(1) th have "isnpoly n" by blast
hence nn: "isnpoly (n *\<^sub>p (C (-2,1)))" "\<lparr>n *\<^sub>p(C (-2,1)) \<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
- using H(2) by (simp_all add: polymul_norm n2)
+ using H(2) by (simp_all add: polymul_norm n2)
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)}
ultimately show ?thesis by blast
qed
@@ -2820,21 +2820,21 @@
"Ifm vs (x#bs) (msubst2 p (C (-2, 1) *\<^sub>p c*\<^sub>p d) (Add (Mul d t) (Mul c s)))"
from H(1,2) th have "isnpoly c" "isnpoly d" by blast+
hence nn: "isnpoly (C (-2, 1) *\<^sub>p c*\<^sub>p d)"
- by (simp_all add: polymul_norm n2)
+ by (simp_all add: polymul_norm n2)
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)))"
- by (simp_all add: polyneg_norm nn)
+ by (simp_all add: polyneg_norm nn)
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"
- 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)
+ 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)
from msubst2[OF lp nn nn'(1), of x bs ] H(3) nn'
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"
- apply (simp add: add_divide_distrib of_int_minus2 del: minus_add_distrib)
- by (simp add: mult_commute)}
+ apply (simp add: add_divide_distrib of_int_minus2 del: minus_add_distrib)
+ by (simp add: mult_commute)}
moreover
{fix c t d s assume H: "(c,t) \<in> set (uset p)" "(d,s) \<in> set (uset p)"
"\<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"
from H(1,2) th have "isnpoly c" "isnpoly d" by blast+
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"
- using H(3,4) by (simp_all add: polymul_norm n2)
+ using H(3,4) by (simp_all add: polymul_norm n2)
from msubst2[OF lp nn, of x bs ] H(3,4,5)
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)}
ultimately show ?thesis by blast
@@ -2906,16 +2906,16 @@
proof
assume H: ?lhs
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"
- by (auto simp add: msubst2_def lt[OF stupid(3)] lt[OF stupid(1)] mult_less_0_iff zero_less_mult_iff)
+ by (auto simp add: msubst2_def lt[OF stupid(3)] lt[OF stupid(1)] mult_less_0_iff zero_less_mult_iff)
from msubst2[OF lq norm2(1) z(1), of x bs]
- msubst2[OF lq norm2(2) z(2), of x bs] H
+ msubst2[OF lq norm2(2) z(2), of x bs] H
show ?rhs by (simp add: ring_simps)
next
assume H: ?rhs
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"
- by (auto simp add: msubst2_def lt[OF stupid(4)] lt[OF stupid(2)] mult_less_0_iff zero_less_mult_iff)
+ by (auto simp add: msubst2_def lt[OF stupid(4)] lt[OF stupid(2)] mult_less_0_iff zero_less_mult_iff)
from msubst2[OF lq norm2(1) z(1), of x bs]
- msubst2[OF lq norm2(2) z(2), of x bs] H
+ msubst2[OF lq norm2(2) z(2), of x bs] H
show ?lhs by (simp add: ring_simps)
qed}
hence th0: "\<forall>x \<in> set ?U. \<forall>y \<in> set ?U. ?I (?s (x, y)) \<longleftrightarrow> ?I (?s (y, x))"
--- a/src/HOL/Decision_Procs/Polynomial_List.thy Wed Oct 28 00:23:39 2009 +0100
+++ b/src/HOL/Decision_Procs/Polynomial_List.thy Wed Oct 28 00:24:38 2009 +0100
@@ -1,8 +1,8 @@
-(* Title: HOL/Decision_Procs/Polynomial_List.thy
- Author: Amine Chaieb
+(* Title: HOL/Decision_Procs/Polynomial_List.thy
+ Author: Amine Chaieb
*)
-header{*Univariate Polynomials as Lists *}
+header {* Univariate Polynomials as Lists *}
theory Polynomial_List
imports Main
@@ -653,7 +653,7 @@
apply (simp add: divides_def fun_eq poly_mult)
apply (rule_tac x = "[]" in exI)
apply (auto dest!: order2 [where a=a]
- intro: poly_exp_divides simp del: pexp_Suc)
+ intro: poly_exp_divides simp del: pexp_Suc)
done
lemma order_decomp:
@@ -780,4 +780,5 @@
done
lemma poly_Sing: "poly [c] x = c" by simp
+
end
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Wed Oct 28 00:23:39 2009 +0100
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Wed Oct 28 00:24:38 2009 +0100
@@ -391,7 +391,7 @@
{assume nn':"\<not> n' < n" hence "n < n' \<or> n = n'" by arith
moreover {assume "n < n'" with prems have ?case by simp }
moreover {assume eq: "n = n'" hence ?case using prems
- by (cases "p +\<^sub>p p' = 0\<^sub>p", auto simp add: Let_def) }
+ by (cases "p +\<^sub>p p' = 0\<^sub>p", auto simp add: Let_def) }
ultimately have ?case by blast}
ultimately show ?case by blast
qed simp_all
@@ -413,10 +413,10 @@
by simp_all
{assume "?c = 0\<^sub>N" hence ?case by auto}
moreover {assume cnz: "?c \<noteq> 0\<^sub>N"
- from "2.hyps"(1)[rule_format,where xb="n'", OF cnz n(1) n(3)]
- "2.hyps"(2)[rule_format, where x="Suc n'"
- and xa="Suc n'" and xb = "n'", OF cnz ] cnz n have ?case
- by (auto simp add: min_def)}
+ from "2.hyps"(1)[rule_format,where xb="n'", OF cnz n(1) n(3)]
+ "2.hyps"(2)[rule_format, where x="Suc n'"
+ and xa="Suc n'" and xb = "n'", OF cnz ] cnz n have ?case
+ by (auto simp add: min_def)}
ultimately show ?case by blast
next
case (2 n0 n1) thus ?case by auto
@@ -431,10 +431,10 @@
by simp_all
{assume "?c' = 0\<^sub>N" hence ?case by auto}
moreover {assume cnz: "?c' \<noteq> 0\<^sub>N"
- from "3.hyps"(1)[rule_format,where xb="n", OF cnz n(3) n(1)]
- "3.hyps"(2)[rule_format, where x="Suc n"
- and xa="Suc n" and xb = "n", OF cnz ] cnz n have ?case
- by (auto simp add: min_def)}
+ from "3.hyps"(1)[rule_format,where xb="n", OF cnz n(3) n(1)]
+ "3.hyps"(2)[rule_format, where x="Suc n"
+ and xa="Suc n" and xb = "n", OF cnz ] cnz n have ?case
+ by (auto simp add: min_def)}
ultimately show ?case by blast
next
case (2 n0 n1) thus ?case apply auto done
@@ -446,32 +446,32 @@
{fix n0 n1
assume "isnpolyh ?cnp n0" and "isnpolyh ?cnp' n1"
hence cnp: "isnpolyh ?cnp n" and cnp': "isnpolyh ?cnp' n'"
- and np: "isnpolyh p n" and nc: "isnpolyh c (Suc n)"
- and np': "isnpolyh p' n'" and nc': "isnpolyh c' (Suc n')"
- and nn0: "n \<ge> n0" and nn1:"n' \<ge> n1"
- by simp_all
+ and np: "isnpolyh p n" and nc: "isnpolyh c (Suc n)"
+ and np': "isnpolyh p' n'" and nc': "isnpolyh c' (Suc n')"
+ and nn0: "n \<ge> n0" and nn1:"n' \<ge> n1"
+ by simp_all
have "n < n' \<or> n' < n \<or> n' = n" by auto
moreover
{assume nn': "n < n'"
- with "4.hyps"(5)[rule_format, OF nn' np cnp', where xb ="n"]
- "4.hyps"(6)[rule_format, OF nn' nc cnp', where xb="n"] nn' nn0 nn1 cnp
- have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
- by (simp add: min_def) }
+ with "4.hyps"(5)[rule_format, OF nn' np cnp', where xb ="n"]
+ "4.hyps"(6)[rule_format, OF nn' nc cnp', where xb="n"] nn' nn0 nn1 cnp
+ have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
+ by (simp add: min_def) }
moreover
{assume nn': "n > n'" hence stupid: "n' < n \<and> \<not> n < n'" by arith
- with "4.hyps"(3)[rule_format, OF stupid cnp np', where xb="n'"]
- "4.hyps"(4)[rule_format, OF stupid cnp nc', where xb="Suc n'"]
- nn' nn0 nn1 cnp'
- have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
- by (cases "Suc n' = n", simp_all add: min_def)}
+ with "4.hyps"(3)[rule_format, OF stupid cnp np', where xb="n'"]
+ "4.hyps"(4)[rule_format, OF stupid cnp nc', where xb="Suc n'"]
+ nn' nn0 nn1 cnp'
+ have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
+ by (cases "Suc n' = n", simp_all add: min_def)}
moreover
{assume nn': "n' = n" hence stupid: "\<not> n' < n \<and> \<not> n < n'" by arith
- from "4.hyps"(1)[rule_format, OF stupid cnp np', where xb="n"]
- "4.hyps"(2)[rule_format, OF stupid cnp nc', where xb="n"] nn' cnp cnp' nn1
-
- have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
- by simp (rule polyadd_normh,simp_all add: min_def isnpolyh_mono[OF nn0]) }
+ from "4.hyps"(1)[rule_format, OF stupid cnp np', where xb="n"]
+ "4.hyps"(2)[rule_format, OF stupid cnp nc', where xb="n"] nn' cnp cnp' nn1
+
+ have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
+ by simp (rule polyadd_normh,simp_all add: min_def isnpolyh_mono[OF nn0]) }
ultimately show "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)" by blast }
note th = this
{fix n0 n1 m
@@ -484,86 +484,86 @@
have "n'<n \<or> n < n' \<or> n' = n" by auto
moreover
{assume "n' < n \<or> n < n'"
- with "4.hyps" np np' m
- have ?eq apply (cases "n' < n", simp_all)
- apply (erule allE[where x="n"],erule allE[where x="n"],auto)
- done }
+ with "4.hyps" np np' m
+ have ?eq apply (cases "n' < n", simp_all)
+ apply (erule allE[where x="n"],erule allE[where x="n"],auto)
+ done }
moreover
{assume nn': "n' = n" hence nn:"\<not> n' < n \<and> \<not> n < n'" by arith
- from "4.hyps"(1)[rule_format, OF nn, where x="n" and xa ="n'" and xb="n"]
- "4.hyps"(2)[rule_format, OF nn, where x="n" and xa ="Suc n'" and xb="n"]
- np np' nn'
- have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"
- "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
- "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)"
- "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p" by (auto simp add: min_def)
- {assume mn: "m = n"
- from "4.hyps"(1)[rule_format, OF nn norm(1,4), where xb="n"]
- "4.hyps"(2)[rule_format, OF nn norm(1,2), where xb="n"] norm nn' mn
- have degs: "degreen (?cnp *\<^sub>p c') n =
- (if c'=0\<^sub>p then 0 else ?d1 + degreen c' n)"
- "degreen (?cnp *\<^sub>p p') n = ?d1 + degreen p' n" by (simp_all add: min_def)
- from degs norm
- have th1: "degreen(?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" by simp
- hence neq: "degreen (?cnp *\<^sub>p c') n \<noteq> degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n"
- by simp
- have nmin: "n \<le> min n n" by (simp add: min_def)
- from polyadd_different_degreen[OF norm(3,6) neq nmin] th1
- 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
- from "4.hyps"(1)[rule_format, OF nn norm(1,4), where xb="n"]
- "4.hyps"(2)[rule_format, OF nn norm(1,2), where xb="n"]
- mn norm m nn' deg
- have ?eq by simp}
- moreover
- {assume mn: "m \<noteq> n" hence mn': "m < n" using m np by auto
- from nn' m np have max1: "m \<le> max n n" by simp
- hence min1: "m \<le> min n n" by simp
- hence min2: "m \<le> min n (Suc n)" by simp
- {assume "c' = 0\<^sub>p"
- from `c' = 0\<^sub>p` have ?eq
- using "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
- "4.hyps"(2)[rule_format, OF nn norm(1,2) min2] mn nn'
- apply simp
- done}
- moreover
- {assume cnz: "c' \<noteq> 0\<^sub>p"
- from "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
- "4.hyps"(2)[rule_format, OF nn norm(1,2) min2]
- degreen_polyadd[OF norm(3,6) max1]
+ from "4.hyps"(1)[rule_format, OF nn, where x="n" and xa ="n'" and xb="n"]
+ "4.hyps"(2)[rule_format, OF nn, where x="n" and xa ="Suc n'" and xb="n"]
+ np np' nn'
+ have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"
+ "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
+ "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)"
+ "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p" by (auto simp add: min_def)
+ {assume mn: "m = n"
+ from "4.hyps"(1)[rule_format, OF nn norm(1,4), where xb="n"]
+ "4.hyps"(2)[rule_format, OF nn norm(1,2), where xb="n"] norm nn' mn
+ have degs: "degreen (?cnp *\<^sub>p c') n =
+ (if c'=0\<^sub>p then 0 else ?d1 + degreen c' n)"
+ "degreen (?cnp *\<^sub>p p') n = ?d1 + degreen p' n" by (simp_all add: min_def)
+ from degs norm
+ have th1: "degreen(?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" by simp
+ hence neq: "degreen (?cnp *\<^sub>p c') n \<noteq> degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n"
+ by simp
+ have nmin: "n \<le> min n n" by (simp add: min_def)
+ from polyadd_different_degreen[OF norm(3,6) neq nmin] th1
+ 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
+ from "4.hyps"(1)[rule_format, OF nn norm(1,4), where xb="n"]
+ "4.hyps"(2)[rule_format, OF nn norm(1,2), where xb="n"]
+ mn norm m nn' deg
+ have ?eq by simp}
+ moreover
+ {assume mn: "m \<noteq> n" hence mn': "m < n" using m np by auto
+ from nn' m np have max1: "m \<le> max n n" by simp
+ hence min1: "m \<le> min n n" by simp
+ hence min2: "m \<le> min n (Suc n)" by simp
+ {assume "c' = 0\<^sub>p"
+ from `c' = 0\<^sub>p` have ?eq
+ using "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
+ "4.hyps"(2)[rule_format, OF nn norm(1,2) min2] mn nn'
+ apply simp
+ done}
+ moreover
+ {assume cnz: "c' \<noteq> 0\<^sub>p"
+ from "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
+ "4.hyps"(2)[rule_format, OF nn norm(1,2) min2]
+ degreen_polyadd[OF norm(3,6) max1]
- have "degreen (?cnp *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (?cnp *\<^sub>p p')) m
- \<le> max (degreen (?cnp *\<^sub>p c') m) (degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) m)"
- using mn nn' cnz np np' by simp
- with "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
- "4.hyps"(2)[rule_format, OF nn norm(1,2) min2]
- degreen_0[OF norm(3) mn'] have ?eq using nn' mn cnz np np' by clarsimp}
- ultimately have ?eq by blast }
- ultimately have ?eq by blast}
+ have "degreen (?cnp *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (?cnp *\<^sub>p p')) m
+ \<le> max (degreen (?cnp *\<^sub>p c') m) (degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) m)"
+ using mn nn' cnz np np' by simp
+ with "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
+ "4.hyps"(2)[rule_format, OF nn norm(1,2) min2]
+ degreen_0[OF norm(3) mn'] have ?eq using nn' mn cnz np np' by clarsimp}
+ ultimately have ?eq by blast }
+ ultimately have ?eq by blast}
ultimately show ?eq by blast}
note degth = this
{ case (2 n0 n1)
hence np: "isnpolyh ?cnp n0" and np': "isnpolyh ?cnp' n1"
- and m: "m \<le> min n0 n1" by simp_all
+ and m: "m \<le> min n0 n1" by simp_all
hence mn: "m \<le> n" by simp
let ?c0p = "CN 0\<^sub>p n (?cnp *\<^sub>p p')"
{assume C: "?cnp *\<^sub>p c' +\<^sub>p ?c0p = 0\<^sub>p" "n' = n"
- hence nn: "\<not>n' < n \<and> \<not> n<n'" by simp
- from "4.hyps"(1) [rule_format, OF nn, where x="n" and xa = "n" and xb="n"]
- "4.hyps"(2) [rule_format, OF nn, where x="n" and xa = "Suc n" and xb="n"]
- np np' C(2) mn
- have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"
- "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
- "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)"
- "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p"
- "degreen (?cnp *\<^sub>p c') n = (if c'=0\<^sub>p then 0 else degreen ?cnp n + degreen c' n)"
- "degreen (?cnp *\<^sub>p p') n = degreen ?cnp n + degreen p' n"
- by (simp_all add: min_def)
-
- from norm have cn: "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp
- have degneq: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n"
- using norm by simp
- from polyadd_eq_const_degreen[OF norm(3) cn C(1), where m="n"] degneq
- have "False" by simp }
+ hence nn: "\<not>n' < n \<and> \<not> n<n'" by simp
+ from "4.hyps"(1) [rule_format, OF nn, where x="n" and xa = "n" and xb="n"]
+ "4.hyps"(2) [rule_format, OF nn, where x="n" and xa = "Suc n" and xb="n"]
+ np np' C(2) mn
+ have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"
+ "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
+ "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)"
+ "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p"
+ "degreen (?cnp *\<^sub>p c') n = (if c'=0\<^sub>p then 0 else degreen ?cnp n + degreen c' n)"
+ "degreen (?cnp *\<^sub>p p') n = degreen ?cnp n + degreen p' n"
+ by (simp_all add: min_def)
+
+ from norm have cn: "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp
+ have degneq: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n"
+ using norm by simp
+ from polyadd_eq_const_degreen[OF norm(3) cn C(1), where m="n"] degneq
+ have "False" by simp }
thus ?case using "4.hyps" by clarsimp}
qed auto
@@ -1022,8 +1022,8 @@
have "\<forall>x. poly (polypoly' (?ts @ xs) p) x = poly [] x" by simp
hence "poly (polypoly' (?ts @ xs) p) = poly []" by (auto intro: ext)
hence "\<forall> c \<in> set (coefficients p). Ipoly (?ts @ xs) (decrpoly c) = 0"
- thm poly_zero
- using poly_zero[where ?'a='a] by (simp add: polypoly'_def list_all_iff)
+ thm poly_zero
+ using poly_zero[where ?'a='a] by (simp add: polypoly'_def list_all_iff)
with coefficients_head[of p, symmetric]
have th0: "Ipoly (?ts @ xs) ?hd = 0" by simp
from bs have wf'': "wf_bs ?ts ?hd" unfolding wf_bs_def by simp
@@ -1272,18 +1272,18 @@
by (simp add: min_def)
{assume np: "n > 0"
with nn' head_isnpolyh_Suc'[OF np nth]
- head_isnpolyh_Suc'[OF np norm(5)] head_isnpolyh_Suc'[OF np norm(6)[simplified nn']]
+ head_isnpolyh_Suc'[OF np norm(5)] head_isnpolyh_Suc'[OF np norm(6)[simplified nn']]
have ?case by simp}
moreover
{moreover assume nz: "n = 0"
from polymul_degreen[OF norm(5,4), where m="0"]
- polymul_degreen[OF norm(5,3), where m="0"] nn' nz degree_eq_degreen0
+ polymul_degreen[OF norm(5,3), where m="0"] nn' nz degree_eq_degreen0
norm(5,6) degree_npolyhCN[OF norm(6)]
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
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
from polyadd_head[OF ncnpc'[simplified nz] ncnpp0'[simplified nz] dth'] dth
have ?case using norm prems(2)[rule_format, OF stupid norm(5,3)]
- prems(3)[rule_format, OF stupid norm(5,4)] nn' nz by simp }
+ prems(3)[rule_format, OF stupid norm(5,4)] nn' nz by simp }
ultimately have ?case by (cases n) auto}
ultimately show ?case by blast
qed simp_all
@@ -1399,182 +1399,182 @@
moreover
{assume dn': "\<not> d < n" hence dn: "d \<ge> n" by arith
have degsp': "degree s = degree ?p'"
- using ds dn ndp funpow_shift1_degree[where k = "d - n" and p="p"] by simp
+ using ds dn ndp funpow_shift1_degree[where k = "d - n" and p="p"] by simp
{assume ba: "?b = a"
- hence headsp': "head s = head ?p'" using ap headp' by simp
- have nr: "isnpolyh (s -\<^sub>p ?p') 0" using polysub_normh[OF ns np'] by simp
- from ds degree_polysub_samehead[OF ns np' headsp' degsp']
- have "degree (s -\<^sub>p ?p') < d \<or> s -\<^sub>p ?p' = 0\<^sub>p" by simp
- moreover
- {assume deglt:"degree (s -\<^sub>p ?p') < d"
- from H[rule_format, OF deglt nr,simplified]
- have domsp: "?D (a, n, p, k, s -\<^sub>p ?p')" by blast
- have dom: ?dths apply (rule polydivide_aux_real_domintros)
- using ba ds dn' domsp by simp_all
- from polydivide_aux.psimps[OF dom] sz dn' ba ds
- have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')"
- by (simp add: Let_def)
- {assume h1: "polydivide_aux (a, n, p, k, s) = (k', r)"
- from H[rule_format, OF deglt nr, where xa = "k" and xb="k'" and xc="r", simplified]
- trans[OF eq[symmetric] h1]
- have kk': "k \<le> k'" and nr:"\<exists>nr. isnpolyh r nr" and dr: "degree r = 0 \<or> degree r < degree p"
- 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
- from q1 obtain q n1 where nq: "isnpolyh q n1"
- and asp:"a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p') = p *\<^sub>p q +\<^sub>p r" by blast
- from nr obtain nr where nr': "isnpolyh r nr" by blast
- from polymul_normh[OF nakk' ns] have nakks': "isnpolyh (a ^\<^sub>p (k' - k) *\<^sub>p s) 0" by simp
- from polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]
- have nq': "isnpolyh (?akk' *\<^sub>p ?xdn +\<^sub>p q) 0" by simp
- from polyadd_normh[OF polymul_normh[OF np
- polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]] nr']
- have nqr': "isnpolyh (p *\<^sub>p (?akk' *\<^sub>p ?xdn +\<^sub>p q) +\<^sub>p r) 0" by simp
- 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')) =
- Ipoly bs (p *\<^sub>p q +\<^sub>p r)" by simp
- hence " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) =
- Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r"
- by (simp add: ring_simps)
- hence " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
- Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (d - n) shift1 1\<^sub>p *\<^sub>p p)
- + Ipoly bs p * Ipoly bs q + Ipoly bs r"
- by (auto simp only: funpow_shift1_1)
- hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
- Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (d - n) shift1 1\<^sub>p)
- + Ipoly bs q) + Ipoly bs r" by (simp add: ring_simps)
- hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
- 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
- with isnpolyh_unique[OF nakks' nqr']
- have "a ^\<^sub>p (k' - k) *\<^sub>p s =
- 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
- hence ?qths using nq'
- apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (d - n) shift1 1\<^sub>p) +\<^sub>p q" in exI)
- apply (rule_tac x="0" in exI) by simp
- 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"
- by blast } hence ?qrths by blast
- with dom have ?ths by blast}
- moreover
- {assume spz:"s -\<^sub>p ?p' = 0\<^sub>p"
- hence domsp: "?D (a, n, p, k, s -\<^sub>p ?p')"
- apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
- have dom: ?dths apply (rule polydivide_aux_real_domintros)
- using ba ds dn' domsp by simp_all
- 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}"]
- have " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs s = Ipoly bs ?p'" by simp
- 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
- by (simp only: funpow_shift1_1) simp
- hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] by blast
- {assume h1: "polydivide_aux (a,n,p,k,s) = (k',r)"
- from polydivide_aux.psimps[OF dom] sz dn' ba ds
- have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')"
- by (simp add: Let_def)
- also have "\<dots> = (k,0\<^sub>p)" using polydivide_aux.psimps[OF domsp] spz by simp
- finally have "(k',r) = (k,0\<^sub>p)" using h1 by simp
- with sp' ns np nxdn polyadd_0(1)[OF polymul_normh[OF np nxdn]]
- polyadd_0(2)[OF polymul_normh[OF np nxdn]] have ?qrths
- apply auto
- apply (rule exI[where x="?xdn"])
- apply auto
- apply (rule polymul_commute)
- apply simp_all
- done}
- with dom have ?ths by blast}
- ultimately have ?ths by blast }
+ hence headsp': "head s = head ?p'" using ap headp' by simp
+ have nr: "isnpolyh (s -\<^sub>p ?p') 0" using polysub_normh[OF ns np'] by simp
+ from ds degree_polysub_samehead[OF ns np' headsp' degsp']
+ have "degree (s -\<^sub>p ?p') < d \<or> s -\<^sub>p ?p' = 0\<^sub>p" by simp
+ moreover
+ {assume deglt:"degree (s -\<^sub>p ?p') < d"
+ from H[rule_format, OF deglt nr,simplified]
+ have domsp: "?D (a, n, p, k, s -\<^sub>p ?p')" by blast
+ have dom: ?dths apply (rule polydivide_aux_real_domintros)
+ using ba ds dn' domsp by simp_all
+ from polydivide_aux.psimps[OF dom] sz dn' ba ds
+ have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')"
+ by (simp add: Let_def)
+ {assume h1: "polydivide_aux (a, n, p, k, s) = (k', r)"
+ from H[rule_format, OF deglt nr, where xa = "k" and xb="k'" and xc="r", simplified]
+ trans[OF eq[symmetric] h1]
+ have kk': "k \<le> k'" and nr:"\<exists>nr. isnpolyh r nr" and dr: "degree r = 0 \<or> degree r < degree p"
+ 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
+ from q1 obtain q n1 where nq: "isnpolyh q n1"
+ and asp:"a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p') = p *\<^sub>p q +\<^sub>p r" by blast
+ from nr obtain nr where nr': "isnpolyh r nr" by blast
+ from polymul_normh[OF nakk' ns] have nakks': "isnpolyh (a ^\<^sub>p (k' - k) *\<^sub>p s) 0" by simp
+ from polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]
+ have nq': "isnpolyh (?akk' *\<^sub>p ?xdn +\<^sub>p q) 0" by simp
+ from polyadd_normh[OF polymul_normh[OF np
+ polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]] nr']
+ have nqr': "isnpolyh (p *\<^sub>p (?akk' *\<^sub>p ?xdn +\<^sub>p q) +\<^sub>p r) 0" by simp
+ 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')) =
+ Ipoly bs (p *\<^sub>p q +\<^sub>p r)" by simp
+ hence " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) =
+ Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r"
+ by (simp add: ring_simps)
+ hence " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
+ Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (d - n) shift1 1\<^sub>p *\<^sub>p p)
+ + Ipoly bs p * Ipoly bs q + Ipoly bs r"
+ by (auto simp only: funpow_shift1_1)
+ hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
+ Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (d - n) shift1 1\<^sub>p)
+ + Ipoly bs q) + Ipoly bs r" by (simp add: ring_simps)
+ hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
+ 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
+ with isnpolyh_unique[OF nakks' nqr']
+ have "a ^\<^sub>p (k' - k) *\<^sub>p s =
+ 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
+ hence ?qths using nq'
+ apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (d - n) shift1 1\<^sub>p) +\<^sub>p q" in exI)
+ apply (rule_tac x="0" in exI) by simp
+ 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"
+ by blast } hence ?qrths by blast
+ with dom have ?ths by blast}
+ moreover
+ {assume spz:"s -\<^sub>p ?p' = 0\<^sub>p"
+ hence domsp: "?D (a, n, p, k, s -\<^sub>p ?p')"
+ apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
+ have dom: ?dths apply (rule polydivide_aux_real_domintros)
+ using ba ds dn' domsp by simp_all
+ 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}"]
+ have " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs s = Ipoly bs ?p'" by simp
+ 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
+ by (simp only: funpow_shift1_1) simp
+ hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] by blast
+ {assume h1: "polydivide_aux (a,n,p,k,s) = (k',r)"
+ from polydivide_aux.psimps[OF dom] sz dn' ba ds
+ have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')"
+ by (simp add: Let_def)
+ also have "\<dots> = (k,0\<^sub>p)" using polydivide_aux.psimps[OF domsp] spz by simp
+ finally have "(k',r) = (k,0\<^sub>p)" using h1 by simp
+ with sp' ns np nxdn polyadd_0(1)[OF polymul_normh[OF np nxdn]]
+ polyadd_0(2)[OF polymul_normh[OF np nxdn]] have ?qrths
+ apply auto
+ apply (rule exI[where x="?xdn"])
+ apply auto
+ apply (rule polymul_commute)
+ apply simp_all
+ done}
+ with dom have ?ths by blast}
+ ultimately have ?ths by blast }
moreover
{assume ba: "?b \<noteq> a"
- from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np0, simplified ap] ns]
- polymul_normh[OF head_isnpolyh[OF ns] np']]
- have nth: "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" by(simp add: min_def)
- have nzths: "a *\<^sub>p s \<noteq> 0\<^sub>p" "?b *\<^sub>p ?p' \<noteq> 0\<^sub>p"
- using polymul_eq0_iff[OF head_isnpolyh[OF np0, simplified ap] ns]
- polymul_eq0_iff[OF head_isnpolyh[OF ns] np']head_nz[OF np0] ap pnz sz head_nz[OF ns]
- funpow_shift1_nz[OF pnz] by simp_all
- from polymul_head_polyeq[OF head_isnpolyh[OF np] ns] head_nz[OF np] sz ap head_head[OF np] pnz
- polymul_head_polyeq[OF head_isnpolyh[OF ns] np'] head_nz [OF ns] sz funpow_shift1_nz[OF pnz, where n="d - n"]
- have hdth: "head (a *\<^sub>p s) = head (?b *\<^sub>p ?p')"
- using head_head[OF ns] funpow_shift1_head[OF np pnz]
- polymul_commute[OF head_isnpolyh[OF np] head_isnpolyh[OF ns]]
- by (simp add: ap)
- from polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"]
- head_nz[OF np] pnz sz ap[symmetric]
- funpow_shift1_nz[OF pnz, where n="d - n"]
- polymul_degreen[OF head_isnpolyh[OF ns] np', where m="0"] head_nz[OF ns]
- ndp ds[symmetric] dn
- have degth: "degree (a *\<^sub>p s) = degree (?b *\<^sub>p ?p') "
- by (simp add: degree_eq_degreen0[symmetric] funpow_shift1_degree)
- {assume dth: "degree ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) < d"
- have th: "?D (a, n, p, Suc k, (a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))"
- using H[rule_format, OF dth nth, simplified] by blast
- have dom: ?dths
- using ba ds dn' th apply simp apply (rule polydivide_aux_real_domintros)
- using ba ds dn' by simp_all
- from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np] ns] polymul_normh[OF head_isnpolyh[OF ns]np']]
- ap have nasbp': "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" by simp
- {assume h1:"polydivide_aux (a,n,p,k,s) = (k', r)"
- from h1 polydivide_aux.psimps[OF dom] sz dn' ba ds
- have eq:"polydivide_aux (a,n,p,Suc k,(a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = (k',r)"
- by (simp add: Let_def)
- with H[rule_format, OF dth nasbp', simplified, where xa="Suc k" and xb="k'" and xc="r"]
- obtain q nq nr where kk': "Suc k \<le> k'" and nr: "isnpolyh r nr" and nq: "isnpolyh q nq"
- and dr: "degree r = 0 \<or> degree r < degree p"
- 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
- from kk' have kk'':"Suc (k' - Suc k) = k' - k" by arith
- {fix bs:: "'a::{ring_char_0,division_by_zero,field} list"
-
- from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric]
- 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
- 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"
- by (simp add: ring_simps power_Suc)
- 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"
- by (simp add:kk'' funpow_shift1_1[where n="d - n" and p="p"])
- 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"
- by (simp add: ring_simps)}
- hence ieq:"\<forall>(bs :: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
- 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
- let ?q = "q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)"
- 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]]
- have nqw: "isnpolyh ?q 0" by simp
- 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]]
- 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
- from dr kk' nr h1 asth nqw have ?qrths apply simp
- apply (rule conjI)
- apply (rule exI[where x="nr"], simp)
- apply (rule exI[where x="(q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn))"], simp)
- apply (rule exI[where x="0"], simp)
- done}
- hence ?qrths by blast
- with dom have ?ths by blast}
- moreover
- {assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p"
- hence domsp: "?D (a, n, p, Suc k, a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p'))"
- apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
- have dom: ?dths using sz ba dn' ds domsp
- by - (rule polydivide_aux_real_domintros, simp_all)
- {fix bs :: "'a::{ring_char_0,division_by_zero,field} list"
- from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz
- have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'" by simp
- hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (?b *\<^sub>p ?xdn) * Ipoly bs p"
- by (simp add: funpow_shift1_1[where n="d - n" and p="p"])
- hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" by simp
- }
- 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))" ..
- from hth
- have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)"
- using isnpolyh_unique[where ?'a = "'a::{ring_char_0,division_by_zero,field}", OF polymul_normh[OF head_isnpolyh[OF np] ns]
+ from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np0, simplified ap] ns]
+ polymul_normh[OF head_isnpolyh[OF ns] np']]
+ have nth: "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" by(simp add: min_def)
+ have nzths: "a *\<^sub>p s \<noteq> 0\<^sub>p" "?b *\<^sub>p ?p' \<noteq> 0\<^sub>p"
+ using polymul_eq0_iff[OF head_isnpolyh[OF np0, simplified ap] ns]
+ polymul_eq0_iff[OF head_isnpolyh[OF ns] np']head_nz[OF np0] ap pnz sz head_nz[OF ns]
+ funpow_shift1_nz[OF pnz] by simp_all
+ from polymul_head_polyeq[OF head_isnpolyh[OF np] ns] head_nz[OF np] sz ap head_head[OF np] pnz
+ polymul_head_polyeq[OF head_isnpolyh[OF ns] np'] head_nz [OF ns] sz funpow_shift1_nz[OF pnz, where n="d - n"]
+ have hdth: "head (a *\<^sub>p s) = head (?b *\<^sub>p ?p')"
+ using head_head[OF ns] funpow_shift1_head[OF np pnz]
+ polymul_commute[OF head_isnpolyh[OF np] head_isnpolyh[OF ns]]
+ by (simp add: ap)
+ from polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"]
+ head_nz[OF np] pnz sz ap[symmetric]
+ funpow_shift1_nz[OF pnz, where n="d - n"]
+ polymul_degreen[OF head_isnpolyh[OF ns] np', where m="0"] head_nz[OF ns]
+ ndp ds[symmetric] dn
+ have degth: "degree (a *\<^sub>p s) = degree (?b *\<^sub>p ?p') "
+ by (simp add: degree_eq_degreen0[symmetric] funpow_shift1_degree)
+ {assume dth: "degree ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) < d"
+ have th: "?D (a, n, p, Suc k, (a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))"
+ using H[rule_format, OF dth nth, simplified] by blast
+ have dom: ?dths
+ using ba ds dn' th apply simp apply (rule polydivide_aux_real_domintros)
+ using ba ds dn' by simp_all
+ from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np] ns] polymul_normh[OF head_isnpolyh[OF ns]np']]
+ ap have nasbp': "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" by simp
+ {assume h1:"polydivide_aux (a,n,p,k,s) = (k', r)"
+ from h1 polydivide_aux.psimps[OF dom] sz dn' ba ds
+ have eq:"polydivide_aux (a,n,p,Suc k,(a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = (k',r)"
+ by (simp add: Let_def)
+ with H[rule_format, OF dth nasbp', simplified, where xa="Suc k" and xb="k'" and xc="r"]
+ obtain q nq nr where kk': "Suc k \<le> k'" and nr: "isnpolyh r nr" and nq: "isnpolyh q nq"
+ and dr: "degree r = 0 \<or> degree r < degree p"
+ 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
+ from kk' have kk'':"Suc (k' - Suc k) = k' - k" by arith
+ {fix bs:: "'a::{ring_char_0,division_by_zero,field} list"
+
+ from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric]
+ 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
+ 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"
+ by (simp add: ring_simps power_Suc)
+ 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"
+ by (simp add:kk'' funpow_shift1_1[where n="d - n" and p="p"])
+ 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"
+ by (simp add: ring_simps)}
+ hence ieq:"\<forall>(bs :: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
+ 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
+ let ?q = "q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)"
+ 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]]
+ have nqw: "isnpolyh ?q 0" by simp
+ 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]]
+ 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
+ from dr kk' nr h1 asth nqw have ?qrths apply simp
+ apply (rule conjI)
+ apply (rule exI[where x="nr"], simp)
+ apply (rule exI[where x="(q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn))"], simp)
+ apply (rule exI[where x="0"], simp)
+ done}
+ hence ?qrths by blast
+ with dom have ?ths by blast}
+ moreover
+ {assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p"
+ hence domsp: "?D (a, n, p, Suc k, a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p'))"
+ apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
+ have dom: ?dths using sz ba dn' ds domsp
+ by - (rule polydivide_aux_real_domintros, simp_all)
+ {fix bs :: "'a::{ring_char_0,division_by_zero,field} list"
+ from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz
+ have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'" by simp
+ hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (?b *\<^sub>p ?xdn) * Ipoly bs p"
+ by (simp add: funpow_shift1_1[where n="d - n" and p="p"])
+ hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" by simp
+ }
+ 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))" ..
+ from hth
+ have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)"
+ using isnpolyh_unique[where ?'a = "'a::{ring_char_0,division_by_zero,field}", OF polymul_normh[OF head_isnpolyh[OF np] ns]
polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]],
- simplified ap] by simp
- {assume h1: "polydivide_aux (a,n,p,k,s) = (k', r)"
- from h1 sz ds ba dn' spz polydivide_aux.psimps[OF dom] polydivide_aux.psimps[OF domsp]
- have "(k',r) = (Suc k, 0\<^sub>p)" by (simp add: Let_def)
- with h1 np head_isnpolyh[OF np, simplified ap] ns polymul_normh[OF head_isnpolyh[OF ns] nxdn]
- polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]] asq
- have ?qrths apply (clarsimp simp add: Let_def)
- apply (rule exI[where x="?b *\<^sub>p ?xdn"]) apply simp
- apply (rule exI[where x="0"], simp)
- done}
- hence ?qrths by blast
- with dom have ?ths by blast}
- 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"]
- head_nz[OF np] pnz sz ap[symmetric] ds[symmetric]
- by (simp add: degree_eq_degreen0[symmetric]) blast }
+ simplified ap] by simp
+ {assume h1: "polydivide_aux (a,n,p,k,s) = (k', r)"
+ from h1 sz ds ba dn' spz polydivide_aux.psimps[OF dom] polydivide_aux.psimps[OF domsp]
+ have "(k',r) = (Suc k, 0\<^sub>p)" by (simp add: Let_def)
+ with h1 np head_isnpolyh[OF np, simplified ap] ns polymul_normh[OF head_isnpolyh[OF ns] nxdn]
+ polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]] asq
+ have ?qrths apply (clarsimp simp add: Let_def)
+ apply (rule exI[where x="?b *\<^sub>p ?xdn"]) apply simp
+ apply (rule exI[where x="0"], simp)
+ done}
+ hence ?qrths by blast
+ with dom have ?ths by blast}
+ 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"]
+ head_nz[OF np] pnz sz ap[symmetric] ds[symmetric]
+ by (simp add: degree_eq_degreen0[symmetric]) blast }
ultimately have ?ths by blast
}
ultimately have ?ths by blast}
@@ -1732,7 +1732,7 @@
recdef isweaknpoly "measure size"
"isweaknpoly (C c) = True"
"isweaknpoly (CN c n p) \<longleftrightarrow> isweaknpoly c \<and> isweaknpoly p"
- "isweaknpoly p = False"
+ "isweaknpoly p = False"
lemma isnpolyh_isweaknpoly: "isnpolyh p n0 \<Longrightarrow> isweaknpoly p"
by (induct p arbitrary: n0, auto)
--- a/src/HOL/Nominal/Examples/Pattern.thy Wed Oct 28 00:23:39 2009 +0100
+++ b/src/HOL/Nominal/Examples/Pattern.thy Wed Oct 28 00:24:38 2009 +0100
@@ -669,17 +669,17 @@
proof
assume "x = x' \<and> t = u"
with PVar PVar' have "PVar x T = ([]::name prm) \<bullet> q \<and>
- t = ([]::name prm) \<bullet> u \<and>
- set ([]::name prm) \<subseteq> (supp (PVar x T) \<union> supp q) \<times>
+ t = ([]::name prm) \<bullet> u \<and>
+ set ([]::name prm) \<subseteq> (supp (PVar x T) \<union> supp q) \<times>
(supp (PVar x T) \<union> supp q)" by simp
then show ?thesis ..
next
assume "x \<noteq> x' \<and> t = [(x, x')] \<bullet> u \<and> x \<sharp> u"
with PVar PVar' have "PVar x T = [(x, x')] \<bullet> q \<and>
- t = [(x, x')] \<bullet> u \<and>
- set [(x, x')] \<subseteq> (supp (PVar x T) \<union> supp q) \<times>
+ t = [(x, x')] \<bullet> u \<and>
+ set [(x, x')] \<subseteq> (supp (PVar x T) \<union> supp q) \<times>
(supp (PVar x T) \<union> supp q)"
- by (simp add: perm_swap swap_simps supp_atm perm_type)
+ by (simp add: perm_swap swap_simps supp_atm perm_type)
then show ?thesis ..
qed
next
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Oct 28 00:23:39 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Oct 28 00:24:38 2009 +0100
@@ -1140,51 +1140,51 @@
fun mk_Eval_of additional_arguments ((x, T), NONE) names = (x, names)
| mk_Eval_of additional_arguments ((x, T), SOME mode) names =
- let
+ let
val Ts = binder_types T
(*val argnames = Name.variant_list names
(map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
val args = map Free (argnames ~~ Ts)
val (inargs, outargs) = split_smode mode args*)
- fun mk_split_lambda [] t = lambda (Free (Name.variant names "x", HOLogic.unitT)) t
- | mk_split_lambda [x] t = lambda x t
- | mk_split_lambda xs t =
- let
- fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t))
- | mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t))
- in
- mk_split_lambda' xs t
- end;
- fun mk_arg (i, T) =
- let
- val vname = Name.variant names ("x" ^ string_of_int i)
- val default = Free (vname, T)
- in
- case AList.lookup (op =) mode i of
- NONE => (([], [default]), [default])
- | SOME NONE => (([default], []), [default])
- | SOME (SOME pis) =>
- case HOLogic.strip_tupleT T of
- [] => error "pair mode but unit tuple" (*(([default], []), [default])*)
- | [_] => error "pair mode but not a tuple" (*(([default], []), [default])*)
- | Ts =>
- let
- val vnames = Name.variant_list names
- (map (fn j => "x" ^ string_of_int i ^ "p" ^ string_of_int j)
- (1 upto length Ts))
- val args = map Free (vnames ~~ Ts)
- fun split_args (i, arg) (ins, outs) =
- if member (op =) pis i then
- (arg::ins, outs)
- else
- (ins, arg::outs)
- val (inargs, outargs) = fold_rev split_args ((1 upto length Ts) ~~ args) ([], [])
- fun tuple args = if null args then [] else [HOLogic.mk_tuple args]
- in ((tuple inargs, tuple outargs), args) end
- end
- val (inoutargs, args) = split_list (map mk_arg (1 upto (length Ts) ~~ Ts))
+ fun mk_split_lambda [] t = lambda (Free (Name.variant names "x", HOLogic.unitT)) t
+ | mk_split_lambda [x] t = lambda x t
+ | mk_split_lambda xs t =
+ let
+ fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t))
+ | mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t))
+ in
+ mk_split_lambda' xs t
+ end;
+ fun mk_arg (i, T) =
+ let
+ val vname = Name.variant names ("x" ^ string_of_int i)
+ val default = Free (vname, T)
+ in
+ case AList.lookup (op =) mode i of
+ NONE => (([], [default]), [default])
+ | SOME NONE => (([default], []), [default])
+ | SOME (SOME pis) =>
+ case HOLogic.strip_tupleT T of
+ [] => error "pair mode but unit tuple" (*(([default], []), [default])*)
+ | [_] => error "pair mode but not a tuple" (*(([default], []), [default])*)
+ | Ts =>
+ let
+ val vnames = Name.variant_list names
+ (map (fn j => "x" ^ string_of_int i ^ "p" ^ string_of_int j)
+ (1 upto length Ts))
+ val args = map Free (vnames ~~ Ts)
+ fun split_args (i, arg) (ins, outs) =
+ if member (op =) pis i then
+ (arg::ins, outs)
+ else
+ (ins, arg::outs)
+ val (inargs, outargs) = fold_rev split_args ((1 upto length Ts) ~~ args) ([], [])
+ fun tuple args = if null args then [] else [HOLogic.mk_tuple args]
+ in ((tuple inargs, tuple outargs), args) end
+ end
+ val (inoutargs, args) = split_list (map mk_arg (1 upto (length Ts) ~~ Ts))
val (inargs, outargs) = pairself flat (split_list inoutargs)
- val r = PredicateCompFuns.mk_Eval
+ val r = PredicateCompFuns.mk_Eval
(list_comb (x, inargs @ additional_arguments), HOLogic.mk_tuple outargs)
val t = fold_rev mk_split_lambda args r
in
@@ -1353,22 +1353,22 @@
fun compile_pred compilation_modifiers compfuns thy all_vs param_vs s T mode moded_cls =
let
- val (Ts1, Ts2) = chop (length (fst mode)) (binder_types T)
+ val (Ts1, Ts2) = chop (length (fst mode)) (binder_types T)
val (Us1, Us2) = split_smodeT (snd mode) Ts2
val Ts1' =
map2 (fn NONE => I | SOME is => #funT_of compilation_modifiers compfuns ([], is)) (fst mode) Ts1
fun mk_input_term (i, NONE) =
- [Free (Name.variant (all_vs @ param_vs) ("x" ^ string_of_int i), nth Ts2 (i - 1))]
- | mk_input_term (i, SOME pis) = case HOLogic.strip_tupleT (nth Ts2 (i - 1)) of
- [] => error "strange unit input"
- | [T] => [Free (Name.variant (all_vs @ param_vs) ("x" ^ string_of_int i), nth Ts2 (i - 1))]
- | Ts => let
- val vnames = Name.variant_list (all_vs @ param_vs)
- (map (fn j => "x" ^ string_of_int i ^ "p" ^ string_of_int j)
- pis)
- in if null pis then []
- else [HOLogic.mk_tuple (map Free (vnames ~~ map (fn j => nth Ts (j - 1)) pis))] end
- val in_ts = maps mk_input_term (snd mode)
+ [Free (Name.variant (all_vs @ param_vs) ("x" ^ string_of_int i), nth Ts2 (i - 1))]
+ | mk_input_term (i, SOME pis) = case HOLogic.strip_tupleT (nth Ts2 (i - 1)) of
+ [] => error "strange unit input"
+ | [T] => [Free (Name.variant (all_vs @ param_vs) ("x" ^ string_of_int i), nth Ts2 (i - 1))]
+ | Ts => let
+ val vnames = Name.variant_list (all_vs @ param_vs)
+ (map (fn j => "x" ^ string_of_int i ^ "p" ^ string_of_int j)
+ pis)
+ in if null pis then []
+ else [HOLogic.mk_tuple (map Free (vnames ~~ map (fn j => nth Ts (j - 1)) pis))] end
+ val in_ts = maps mk_input_term (snd mode)
val params = map2 (fn s => fn T => Free (s, T)) param_vs Ts1'
val additional_arguments = #additional_arguments compilation_modifiers (all_vs @ param_vs)
val cl_ts =
@@ -1389,7 +1389,7 @@
(* special setup for simpset *)
val HOL_basic_ss' = HOL_basic_ss addsimps (@{thms "HOL.simp_thms"} @ [@{thm Pair_eq}])
setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
- setSolver (mk_solver "True_solver" (fn _ => rtac @{thm TrueI}))
+ setSolver (mk_solver "True_solver" (fn _ => rtac @{thm TrueI}))
(* Definition of executable functions and their intro and elim rules *)
@@ -1405,29 +1405,29 @@
val funtrm = Const (mode_id, funT)
val (Ts1, Ts2) = chop (length iss) Ts;
val Ts1' = map2 (fn NONE => I | SOME is => funT_of (PredicateCompFuns.compfuns) ([], is)) iss Ts1
- val param_names = Name.variant_list []
+ val param_names = Name.variant_list []
(map (fn i => "x" ^ string_of_int i) (1 upto (length Ts1)));
val params = map Free (param_names ~~ Ts1')
- fun mk_args (i, T) argnames =
+ fun mk_args (i, T) argnames =
let
- val vname = Name.variant (param_names @ argnames) ("x" ^ string_of_int (length Ts1' + i))
- val default = (Free (vname, T), vname :: argnames)
- in
- case AList.lookup (op =) is i of
- NONE => default
- | SOME NONE => default
- | SOME (SOME pis) =>
- case HOLogic.strip_tupleT T of
- [] => default
- | [_] => default
- | Ts =>
- let
- val vnames = Name.variant_list (param_names @ argnames)
- (map (fn j => "x" ^ string_of_int (length Ts1' + i) ^ "p" ^ string_of_int j)
- (1 upto (length Ts)))
- in (HOLogic.mk_tuple (map Free (vnames ~~ Ts)), vnames @ argnames) end
- end
- val (args, argnames) = fold_map mk_args (1 upto (length Ts2) ~~ Ts2) []
+ val vname = Name.variant (param_names @ argnames) ("x" ^ string_of_int (length Ts1' + i))
+ val default = (Free (vname, T), vname :: argnames)
+ in
+ case AList.lookup (op =) is i of
+ NONE => default
+ | SOME NONE => default
+ | SOME (SOME pis) =>
+ case HOLogic.strip_tupleT T of
+ [] => default
+ | [_] => default
+ | Ts =>
+ let
+ val vnames = Name.variant_list (param_names @ argnames)
+ (map (fn j => "x" ^ string_of_int (length Ts1' + i) ^ "p" ^ string_of_int j)
+ (1 upto (length Ts)))
+ in (HOLogic.mk_tuple (map Free (vnames ~~ Ts)), vnames @ argnames) end
+ end
+ val (args, argnames) = fold_map mk_args (1 upto (length Ts2) ~~ Ts2) []
val (inargs, outargs) = split_smode is args
val param_names' = Name.variant_list (param_names @ argnames)
(map (fn i => "p" ^ string_of_int i) (1 upto (length iss)))
@@ -1443,7 +1443,7 @@
HOLogic.mk_tuple outargs))
val introtrm = Logic.list_implies (predpropI :: param_eqs, funpropI)
val simprules = [defthm, @{thm eval_pred},
- @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]
+ @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]
val unfolddef_tac = Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps simprules) 1
val introthm = Goal.prove (ProofContext.init thy) (argnames @ param_names @ param_names' @ ["y"]) [] introtrm (fn {...} => unfolddef_tac)
val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT));
@@ -1466,30 +1466,30 @@
end;
fun split_tupleT is T =
- let
- fun split_tuple' _ _ [] = ([], [])
- | split_tuple' is i (T::Ts) =
- (if i mem is then apfst else apsnd) (cons T)
- (split_tuple' is (i+1) Ts)
- in
- split_tuple' is 1 (HOLogic.strip_tupleT T)
+ let
+ fun split_tuple' _ _ [] = ([], [])
+ | split_tuple' is i (T::Ts) =
+ (if i mem is then apfst else apsnd) (cons T)
+ (split_tuple' is (i+1) Ts)
+ in
+ split_tuple' is 1 (HOLogic.strip_tupleT T)
end
-
+
fun mk_arg xin xout pis T =
let
- val n = length (HOLogic.strip_tupleT T)
- val ni = length pis
- fun mk_proj i j t =
- (if i = j then I else HOLogic.mk_fst)
- (funpow (i - 1) HOLogic.mk_snd t)
- fun mk_arg' i (si, so) = if i mem pis then
- (mk_proj si ni xin, (si+1, so))
- else
- (mk_proj so (n - ni) xout, (si, so+1))
- val (args, _) = fold_map mk_arg' (1 upto n) (1, 1)
- in
- HOLogic.mk_tuple args
- end
+ val n = length (HOLogic.strip_tupleT T)
+ val ni = length pis
+ fun mk_proj i j t =
+ (if i = j then I else HOLogic.mk_fst)
+ (funpow (i - 1) HOLogic.mk_snd t)
+ fun mk_arg' i (si, so) = if i mem pis then
+ (mk_proj si ni xin, (si+1, so))
+ else
+ (mk_proj so (n - ni) xout, (si, so+1))
+ val (args, _) = fold_map mk_arg' (1 upto n) (1, 1)
+ in
+ HOLogic.mk_tuple args
+ end
fun create_definitions preds (name, modes) thy =
let
@@ -1505,37 +1505,37 @@
val funT = (Ts1' @ Us1) ---> (mk_predT compfuns (HOLogic.mk_tupleT Us2))
val names = Name.variant_list []
(map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
- (* old *)
- (*
- val xs = map Free (names ~~ (Ts1' @ Ts2))
+ (* old *)
+ (*
+ val xs = map Free (names ~~ (Ts1' @ Ts2))
val (xparams, xargs) = chop (length iss) xs
val (xins, xouts) = split_smode is xargs
- *)
- (* new *)
- val param_names = Name.variant_list []
- (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts1')))
- val xparams = map Free (param_names ~~ Ts1')
+ *)
+ (* new *)
+ val param_names = Name.variant_list []
+ (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts1')))
+ val xparams = map Free (param_names ~~ Ts1')
fun mk_vars (i, T) names =
- let
- val vname = Name.variant names ("x" ^ string_of_int (length Ts1' + i))
- in
- case AList.lookup (op =) is i of
- NONE => ((([], [Free (vname, T)]), Free (vname, T)), vname :: names)
- | SOME NONE => ((([Free (vname, T)], []), Free (vname, T)), vname :: names)
- | SOME (SOME pis) =>
- let
- val (Tins, Touts) = split_tupleT pis T
- val name_in = Name.variant names ("x" ^ string_of_int (length Ts1' + i) ^ "in")
- val name_out = Name.variant names ("x" ^ string_of_int (length Ts1' + i) ^ "out")
- val xin = Free (name_in, HOLogic.mk_tupleT Tins)
- val xout = Free (name_out, HOLogic.mk_tupleT Touts)
- val xarg = mk_arg xin xout pis T
- in (((if null Tins then [] else [xin], if null Touts then [] else [xout]), xarg), name_in :: name_out :: names) end
- end
- val (xinoutargs, names) = fold_map mk_vars ((1 upto (length Ts2)) ~~ Ts2) param_names
+ let
+ val vname = Name.variant names ("x" ^ string_of_int (length Ts1' + i))
+ in
+ case AList.lookup (op =) is i of
+ NONE => ((([], [Free (vname, T)]), Free (vname, T)), vname :: names)
+ | SOME NONE => ((([Free (vname, T)], []), Free (vname, T)), vname :: names)
+ | SOME (SOME pis) =>
+ let
+ val (Tins, Touts) = split_tupleT pis T
+ val name_in = Name.variant names ("x" ^ string_of_int (length Ts1' + i) ^ "in")
+ val name_out = Name.variant names ("x" ^ string_of_int (length Ts1' + i) ^ "out")
+ val xin = Free (name_in, HOLogic.mk_tupleT Tins)
+ val xout = Free (name_out, HOLogic.mk_tupleT Touts)
+ val xarg = mk_arg xin xout pis T
+ in (((if null Tins then [] else [xin], if null Touts then [] else [xout]), xarg), name_in :: name_out :: names) end
+ end
+ val (xinoutargs, names) = fold_map mk_vars ((1 upto (length Ts2)) ~~ Ts2) param_names
val (xinout, xargs) = split_list xinoutargs
- val (xins, xouts) = pairself flat (split_list xinout)
- val (xparams', names') = fold_map (mk_Eval_of []) ((xparams ~~ Ts1) ~~ iss) names
+ val (xins, xouts) = pairself flat (split_list xinout)
+ val (xparams', names') = fold_map (mk_Eval_of []) ((xparams ~~ Ts1) ~~ iss) names
fun mk_split_lambda [] t = lambda (Free (Name.variant names' "x", HOLogic.unitT)) t
| mk_split_lambda [x] t = lambda x t
| mk_split_lambda xs t =
@@ -1555,7 +1555,7 @@
val (intro, elim) =
create_intro_elim_rule mode definition mode_cname funT (Const (name, T)) thy'
in thy'
- |> add_predfun name mode (mode_cname, definition, intro, elim)
+ |> add_predfun name mode (mode_cname, definition, intro, elim)
|> PureThy.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd
|> PureThy.store_thm (Binding.name (mode_cbasename ^ "E"), elim) |> snd
|> Theory.checkpoint
@@ -1635,7 +1635,7 @@
Const (name, T) => simp_tac (HOL_basic_ss addsimps
([@{thm eval_pred}, (predfun_definition_of thy name mode),
@{thm "split_eta"}, @{thm "split_beta"}, @{thm "fst_conv"},
- @{thm "snd_conv"}, @{thm pair_collapse}, @{thm "Product_Type.split_conv"}])) 1
+ @{thm "snd_conv"}, @{thm pair_collapse}, @{thm "Product_Type.split_conv"}])) 1
| Free _ => TRY (rtac @{thm refl} 1)
| Abs _ => error "prove_param: No valid parameter term"
in
@@ -1669,12 +1669,12 @@
THEN (REPEAT_DETERM (atac 1))
end
| _ => rtac @{thm bindI} 1
- THEN asm_full_simp_tac
- (HOL_basic_ss' addsimps [@{thm "split_eta"}, @{thm "split_beta"}, @{thm "fst_conv"},
- @{thm "snd_conv"}, @{thm pair_collapse}]) 1
- THEN (atac 1)
- THEN print_tac "after prove parameter call"
-
+ THEN asm_full_simp_tac
+ (HOL_basic_ss' addsimps [@{thm "split_eta"}, @{thm "split_beta"}, @{thm "fst_conv"},
+ @{thm "snd_conv"}, @{thm pair_collapse}]) 1
+ THEN (atac 1)
+ THEN print_tac "after prove parameter call"
+
fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st;
@@ -1725,9 +1725,9 @@
val (in_ts, clause_out_ts) = split_smode is ts;
fun prove_prems out_ts [] =
(prove_match thy out_ts)
- THEN print_tac "before simplifying assumptions"
+ THEN print_tac "before simplifying assumptions"
THEN asm_full_simp_tac HOL_basic_ss' 1
- THEN print_tac "before single intro rule"
+ THEN print_tac "before single intro rule"
THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
| prove_prems out_ts ((p, mode as Mode ((iss, is), _, param_modes)) :: ps) =
let
@@ -1793,7 +1793,7 @@
val pred_case_rule = the_elim_of thy pred
in
REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"}))
- THEN print_tac' options "before applying elim rule"
+ THEN print_tac' options "before applying elim rule"
THEN etac (predfun_elim_of thy pred mode) 1
THEN etac pred_case_rule 1
THEN (EVERY (map
@@ -1911,7 +1911,7 @@
THEN (print_tac "state before assumption matching")
THEN (REPEAT (atac 1 ORELSE
(CHANGED (asm_full_simp_tac (HOL_basic_ss' addsimps
- [@{thm split_eta}, @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]) 1)
+ [@{thm split_eta}, @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]) 1)
THEN print_tac "state after simp_tac:"))))
| prove_prems2 out_ts ((p, mode as Mode ((iss, is), _, param_modes)) :: ps) =
let
@@ -1987,7 +1987,7 @@
(if not (skip_proof options) then
(fn _ =>
rtac @{thm pred_iffI} 1
- THEN print_tac' options "after pred_iffI"
+ THEN print_tac' options "after pred_iffI"
THEN prove_one_direction options thy clauses preds modes pred mode moded_clauses
THEN print_tac' options "proved one direction"
THEN prove_other_direction options thy modes pred mode moded_clauses