--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Decision_Procs/Algebra_Aux.thy Sun Jan 29 11:59:48 2017 +0100
@@ -0,0 +1,505 @@
+(* Title: HOL/Decision_Procs/Algebra_Aux.thy
+ Author: Stefan Berghofer
+*)
+
+section \<open>Things that can be added to the Algebra library\<close>
+
+theory Algebra_Aux
+imports "~~/src/HOL/Algebra/Ring"
+begin
+
+definition of_natural :: "('a, 'm) ring_scheme \<Rightarrow> nat \<Rightarrow> 'a" ("\<guillemotleft>_\<guillemotright>\<^sub>\<nat>\<index>") where
+ "\<guillemotleft>n\<guillemotright>\<^sub>\<nat>\<^bsub>R\<^esub> = (op \<oplus>\<^bsub>R\<^esub> \<one>\<^bsub>R\<^esub> ^^ n) \<zero>\<^bsub>R\<^esub>"
+
+definition of_integer :: "('a, 'm) ring_scheme \<Rightarrow> int \<Rightarrow> 'a" ("\<guillemotleft>_\<guillemotright>\<index>") where
+ "\<guillemotleft>i\<guillemotright>\<^bsub>R\<^esub> = (if 0 \<le> i then \<guillemotleft>nat i\<guillemotright>\<^sub>\<nat>\<^bsub>R\<^esub> else \<ominus>\<^bsub>R\<^esub> \<guillemotleft>nat (- i)\<guillemotright>\<^sub>\<nat>\<^bsub>R\<^esub>)"
+
+context ring begin
+
+lemma of_nat_0 [simp]: "\<guillemotleft>0\<guillemotright>\<^sub>\<nat> = \<zero>"
+ by (simp add: of_natural_def)
+
+lemma of_nat_Suc [simp]: "\<guillemotleft>Suc n\<guillemotright>\<^sub>\<nat> = \<one> \<oplus> \<guillemotleft>n\<guillemotright>\<^sub>\<nat>"
+ by (simp add: of_natural_def)
+
+lemma of_int_0 [simp]: "\<guillemotleft>0\<guillemotright> = \<zero>"
+ by (simp add: of_integer_def)
+
+lemma of_nat_closed [simp]: "\<guillemotleft>n\<guillemotright>\<^sub>\<nat> \<in> carrier R"
+ by (induct n) simp_all
+
+lemma of_int_closed [simp]: "\<guillemotleft>i\<guillemotright> \<in> carrier R"
+ by (simp add: of_integer_def)
+
+lemma of_int_minus [simp]: "\<guillemotleft>- i\<guillemotright> = \<ominus> \<guillemotleft>i\<guillemotright>"
+ by (simp add: of_integer_def)
+
+lemma of_nat_add [simp]: "\<guillemotleft>m + n\<guillemotright>\<^sub>\<nat> = \<guillemotleft>m\<guillemotright>\<^sub>\<nat> \<oplus> \<guillemotleft>n\<guillemotright>\<^sub>\<nat>"
+ by (induct m) (simp_all add: a_ac)
+
+lemma of_nat_diff [simp]: "n \<le> m \<Longrightarrow> \<guillemotleft>m - n\<guillemotright>\<^sub>\<nat> = \<guillemotleft>m\<guillemotright>\<^sub>\<nat> \<ominus> \<guillemotleft>n\<guillemotright>\<^sub>\<nat>"
+proof (induct m arbitrary: n)
+ case (Suc m)
+ note Suc' = this
+ show ?case
+ proof (cases n)
+ case (Suc k)
+ with Suc' have "\<guillemotleft>Suc m - Suc k\<guillemotright>\<^sub>\<nat> = \<guillemotleft>m\<guillemotright>\<^sub>\<nat> \<ominus> \<guillemotleft>k\<guillemotright>\<^sub>\<nat>" by simp
+ also have "\<dots> = \<one> \<oplus> \<ominus> \<one> \<oplus> (\<guillemotleft>m\<guillemotright>\<^sub>\<nat> \<ominus> \<guillemotleft>k\<guillemotright>\<^sub>\<nat>)"
+ by (simp add: r_neg)
+ also have "\<dots> = \<guillemotleft>Suc m\<guillemotright>\<^sub>\<nat> \<ominus> \<guillemotleft>Suc k\<guillemotright>\<^sub>\<nat>"
+ by (simp add: minus_eq minus_add a_ac)
+ finally show ?thesis using Suc by simp
+ qed (simp add: minus_eq)
+qed (simp add: minus_eq)
+
+lemma of_int_add [simp]: "\<guillemotleft>i + j\<guillemotright> = \<guillemotleft>i\<guillemotright> \<oplus> \<guillemotleft>j\<guillemotright>"
+proof (cases "0 \<le> i")
+ case True
+ show ?thesis
+ proof (cases "0 \<le> j")
+ case True
+ with `0 \<le> i` show ?thesis by (simp add: of_integer_def nat_add_distrib)
+ next
+ case False
+ show ?thesis
+ proof (cases "0 \<le> i + j")
+ case True
+ then have "\<guillemotleft>i + j\<guillemotright> = \<guillemotleft>nat (i - (- j))\<guillemotright>\<^sub>\<nat>"
+ by (simp add: of_integer_def)
+ also from True `0 \<le> i` `\<not> 0 \<le> j`
+ have "nat (i - (- j)) = nat i - nat (- j)"
+ by (simp add: nat_diff_distrib)
+ finally show ?thesis using True `0 \<le> i` `\<not> 0 \<le> j`
+ by (simp add: minus_eq of_integer_def)
+ next
+ case False
+ then have "\<guillemotleft>i + j\<guillemotright> = \<ominus> \<guillemotleft>nat (- j - i)\<guillemotright>\<^sub>\<nat>"
+ by (simp add: of_integer_def) (simp only: diff_conv_add_uminus add_ac)
+ also from False `0 \<le> i` `\<not> 0 \<le> j`
+ have "nat (- j - i) = nat (- j) - nat i"
+ by (simp add: nat_diff_distrib)
+ finally show ?thesis using False `0 \<le> i` `\<not> 0 \<le> j`
+ by (simp add: minus_eq minus_add a_ac of_integer_def)
+ qed
+ qed
+next
+ case False
+ show ?thesis
+ proof (cases "0 \<le> j")
+ case True
+ show ?thesis
+ proof (cases "0 \<le> i + j")
+ case True
+ then have "\<guillemotleft>i + j\<guillemotright> = \<guillemotleft>nat (j - (- i))\<guillemotright>\<^sub>\<nat>"
+ by (simp add: of_integer_def add_ac)
+ also from True `\<not> 0 \<le> i` `0 \<le> j`
+ have "nat (j - (- i)) = nat j - nat (- i)"
+ by (simp add: nat_diff_distrib)
+ finally show ?thesis using True `\<not> 0 \<le> i` `0 \<le> j`
+ by (simp add: minus_eq minus_add a_ac of_integer_def)
+ next
+ case False
+ then have "\<guillemotleft>i + j\<guillemotright> = \<ominus> \<guillemotleft>nat (- i - j)\<guillemotright>\<^sub>\<nat>"
+ by (simp add: of_integer_def)
+ also from False `\<not> 0 \<le> i` `0 \<le> j`
+ have "nat (- i - j) = nat (- i) - nat j"
+ by (simp add: nat_diff_distrib)
+ finally show ?thesis using False `\<not> 0 \<le> i` `0 \<le> j`
+ by (simp add: minus_eq minus_add of_integer_def)
+ qed
+ next
+ case False
+ with `\<not> 0 \<le> i` show ?thesis
+ by (simp add: of_integer_def nat_add_distrib minus_add diff_conv_add_uminus
+ del: add_uminus_conv_diff uminus_add_conv_diff)
+ qed
+qed
+
+lemma of_int_diff [simp]: "\<guillemotleft>i - j\<guillemotright> = \<guillemotleft>i\<guillemotright> \<ominus> \<guillemotleft>j\<guillemotright>"
+ by (simp only: diff_conv_add_uminus of_int_add) (simp add: minus_eq)
+
+lemma of_nat_mult [simp]: "\<guillemotleft>i * j\<guillemotright>\<^sub>\<nat> = \<guillemotleft>i\<guillemotright>\<^sub>\<nat> \<otimes> \<guillemotleft>j\<guillemotright>\<^sub>\<nat>"
+ by (induct i) (simp_all add: l_distr)
+
+lemma of_int_mult [simp]: "\<guillemotleft>i * j\<guillemotright> = \<guillemotleft>i\<guillemotright> \<otimes> \<guillemotleft>j\<guillemotright>"
+proof (cases "0 \<le> i")
+ case True
+ show ?thesis
+ proof (cases "0 \<le> j")
+ case True
+ with `0 \<le> i` show ?thesis
+ by (simp add: of_integer_def nat_mult_distrib zero_le_mult_iff)
+ next
+ case False
+ with `0 \<le> i` show ?thesis
+ by (simp add: of_integer_def zero_le_mult_iff
+ minus_mult_right nat_mult_distrib r_minus
+ del: minus_mult_right [symmetric])
+ qed
+next
+ case False
+ show ?thesis
+ proof (cases "0 \<le> j")
+ case True
+ with `\<not> 0 \<le> i` show ?thesis
+ by (simp add: of_integer_def zero_le_mult_iff
+ minus_mult_left nat_mult_distrib l_minus
+ del: minus_mult_left [symmetric])
+ next
+ case False
+ with `\<not> 0 \<le> i` show ?thesis
+ by (simp add: of_integer_def zero_le_mult_iff
+ minus_mult_minus [of i j, symmetric] nat_mult_distrib
+ l_minus r_minus
+ del: minus_mult_minus
+ minus_mult_left [symmetric] minus_mult_right [symmetric])
+ qed
+qed
+
+lemma of_int_1 [simp]: "\<guillemotleft>1\<guillemotright> = \<one>"
+ by (simp add: of_integer_def)
+
+lemma of_int_2: "\<guillemotleft>2\<guillemotright> = \<one> \<oplus> \<one>"
+ by (simp add: of_integer_def numeral_2_eq_2)
+
+lemma minus_0_r [simp]: "x \<in> carrier R \<Longrightarrow> x \<ominus> \<zero> = x"
+ by (simp add: minus_eq)
+
+lemma minus_0_l [simp]: "x \<in> carrier R \<Longrightarrow> \<zero> \<ominus> x = \<ominus> x"
+ by (simp add: minus_eq)
+
+lemma eq_diff0:
+ assumes "x \<in> carrier R" "y \<in> carrier R"
+ shows "(x \<ominus> y = \<zero>) = (x = y)"
+proof
+ assume "x \<ominus> y = \<zero>"
+ with assms have "x \<oplus> (\<ominus> y \<oplus> y) = y"
+ by (simp add: minus_eq a_assoc [symmetric])
+ with assms show "x = y" by (simp add: l_neg)
+next
+ assume "x = y"
+ with assms show "x \<ominus> y = \<zero>" by (simp add: minus_eq r_neg)
+qed
+
+lemma power2_eq_square: "x \<in> carrier R \<Longrightarrow> x (^) (2::nat) = x \<otimes> x"
+ by (simp add: numeral_eq_Suc)
+
+lemma eq_neg_iff_add_eq_0:
+ assumes "x \<in> carrier R" "y \<in> carrier R"
+ shows "(x = \<ominus> y) = (x \<oplus> y = \<zero>)"
+proof
+ assume "x = \<ominus> y"
+ with assms show "x \<oplus> y = \<zero>" by (simp add: l_neg)
+next
+ assume "x \<oplus> y = \<zero>"
+ with assms have "x \<oplus> (y \<oplus> \<ominus> y) = \<zero> \<oplus> \<ominus> y"
+ by (simp add: a_assoc [symmetric])
+ with assms show "x = \<ominus> y"
+ by (simp add: r_neg)
+qed
+
+lemma neg_equal_iff_equal:
+ assumes x: "x \<in> carrier R" and y: "y \<in> carrier R"
+ shows "(\<ominus> x = \<ominus> y) = (x = y)"
+proof
+ assume "\<ominus> x = \<ominus> y"
+ then have "\<ominus> (\<ominus> x) = \<ominus> (\<ominus> y)" by simp
+ with x y show "x = y" by simp
+next
+ assume "x = y"
+ then show "\<ominus> x = \<ominus> y" by simp
+qed
+
+lemma neg_equal_swap:
+ assumes x: "x \<in> carrier R" and y: "y \<in> carrier R"
+ shows "(\<ominus> x = y) = (x = \<ominus> y)"
+ using assms neg_equal_iff_equal [of x "\<ominus> y"]
+ by simp
+
+lemma mult2: "x \<in> carrier R \<Longrightarrow> x \<oplus> x = \<guillemotleft>2\<guillemotright> \<otimes> x"
+ by (simp add: of_int_2 l_distr)
+
+end
+
+lemma (in cring) of_int_power [simp]: "\<guillemotleft>i ^ n\<guillemotright> = \<guillemotleft>i\<guillemotright> (^) n"
+ by (induct n) (simp_all add: m_ac)
+
+definition cring_class_ops :: "'a::comm_ring_1 ring" where
+ "cring_class_ops \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
+
+lemma cring_class: "cring cring_class_ops"
+ apply unfold_locales
+ apply (auto simp add: cring_class_ops_def ring_distribs Units_def)
+ apply (rule_tac x="- x" in exI)
+ apply simp
+ done
+
+lemma carrier_class: "x \<in> carrier cring_class_ops"
+ by (simp add: cring_class_ops_def)
+
+lemma zero_class: "\<zero>\<^bsub>cring_class_ops\<^esub> = 0"
+ by (simp add: cring_class_ops_def)
+
+lemma one_class: "\<one>\<^bsub>cring_class_ops\<^esub> = 1"
+ by (simp add: cring_class_ops_def)
+
+lemma plus_class: "x \<oplus>\<^bsub>cring_class_ops\<^esub> y = x + y"
+ by (simp add: cring_class_ops_def)
+
+lemma times_class: "x \<otimes>\<^bsub>cring_class_ops\<^esub> y = x * y"
+ by (simp add: cring_class_ops_def)
+
+lemma uminus_class: "\<ominus>\<^bsub>cring_class_ops\<^esub> x = - x"
+ apply (simp add: a_inv_def m_inv_def cring_class_ops_def)
+ apply (rule the_equality)
+ apply (simp_all add: eq_neg_iff_add_eq_0)
+ done
+
+lemma minus_class: "x \<ominus>\<^bsub>cring_class_ops\<^esub> y = x - y"
+ by (simp add: a_minus_def carrier_class plus_class uminus_class)
+
+lemma power_class: "x (^)\<^bsub>cring_class_ops\<^esub> n = x ^ n"
+ by (induct n) (simp_all add: one_class times_class
+ monoid.nat_pow_0 [OF comm_monoid.axioms(1) [OF cring.axioms(2) [OF cring_class]]]
+ monoid.nat_pow_Suc [OF comm_monoid.axioms(1) [OF cring.axioms(2) [OF cring_class]]])
+
+lemma of_nat_class: "\<guillemotleft>n\<guillemotright>\<^sub>\<nat>\<^bsub>cring_class_ops\<^esub> = of_nat n"
+ by (induct n) (simp_all add: cring_class_ops_def of_natural_def)
+
+lemma of_int_class: "\<guillemotleft>i\<guillemotright>\<^bsub>cring_class_ops\<^esub> = of_int i"
+ by (simp add: of_integer_def of_nat_class uminus_class)
+
+lemmas class_simps = zero_class one_class plus_class minus_class uminus_class
+ times_class power_class of_nat_class of_int_class carrier_class
+
+interpretation cring_class: cring "cring_class_ops::'a::comm_ring_1 ring"
+ rewrites
+ "(\<zero>\<^bsub>cring_class_ops\<^esub>::'a) = 0" and
+ "(\<one>\<^bsub>cring_class_ops\<^esub>::'a) = 1" and
+ "(x::'a) \<oplus>\<^bsub>cring_class_ops\<^esub> y = x + y" and
+ "(x::'a) \<otimes>\<^bsub>cring_class_ops\<^esub> y = x * y" and
+ "\<ominus>\<^bsub>cring_class_ops\<^esub> (x::'a) = - x" and
+ "(x::'a) \<ominus>\<^bsub>cring_class_ops\<^esub> y = x - y" and
+ "(x::'a) (^)\<^bsub>cring_class_ops\<^esub> n = x ^ n" and
+ "\<guillemotleft>n\<guillemotright>\<^sub>\<nat>\<^bsub>cring_class_ops\<^esub> = of_nat n" and
+ "((\<guillemotleft>i\<guillemotright>\<^bsub>cring_class_ops\<^esub>)::'a) = of_int i" and
+ "(Int.of_int (numeral m)::'a) = numeral m"
+ by (simp_all add: cring_class class_simps)
+
+lemma (in domain) nat_pow_eq_0_iff [simp]:
+ "a \<in> carrier R \<Longrightarrow> (a (^) (n::nat) = \<zero>) = (a = \<zero> \<and> n \<noteq> 0)"
+ by (induct n) (auto simp add: integral_iff)
+
+lemma (in domain) square_eq_iff:
+ assumes "x \<in> carrier R" "y \<in> carrier R"
+ shows "(x \<otimes> x = y \<otimes> y) = (x = y \<or> x = \<ominus> y)"
+proof
+ assume "x \<otimes> x = y \<otimes> y"
+ with assms have "(x \<ominus> y) \<otimes> (x \<oplus> y) = x \<otimes> y \<oplus> \<ominus> (x \<otimes> y) \<oplus> (y \<otimes> y \<oplus> \<ominus> (y \<otimes> y))"
+ by (simp add: r_distr l_distr minus_eq r_minus m_comm a_ac)
+ with assms show "x = y \<or> x = \<ominus> y"
+ by (simp add: integral_iff eq_neg_iff_add_eq_0 eq_diff0 r_neg)
+next
+ assume "x = y \<or> x = \<ominus> y"
+ with assms show "x \<otimes> x = y \<otimes> y" by (auto simp add: l_minus r_minus)
+qed
+
+definition
+ m_div :: "('a, 'b) ring_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<oslash>\<index>" 70) where
+ "x \<oslash>\<^bsub>G\<^esub> y = (if y = \<zero>\<^bsub>G\<^esub> then \<zero>\<^bsub>G\<^esub> else x \<otimes>\<^bsub>G\<^esub> inv\<^bsub>G\<^esub> y)"
+
+context field
+begin
+
+lemma inv_closed [simp]: "x \<in> carrier R \<Longrightarrow> x \<noteq> \<zero> \<Longrightarrow> inv x \<in> carrier R"
+ by (simp add: field_Units)
+
+lemma l_inv [simp]: "x \<in> carrier R \<Longrightarrow> x \<noteq> \<zero> \<Longrightarrow> inv x \<otimes> x = \<one>"
+ by (simp add: field_Units)
+
+lemma r_inv [simp]: "x \<in> carrier R \<Longrightarrow> x \<noteq> \<zero> \<Longrightarrow> x \<otimes> inv x = \<one>"
+ by (simp add: field_Units)
+
+lemma inverse_unique:
+ assumes a: "a \<in> carrier R"
+ and b: "b \<in> carrier R"
+ and ab: "a \<otimes> b = \<one>"
+ shows "inv a = b"
+proof -
+ have "a \<noteq> \<zero>" using ab b by (cases "a = \<zero>") simp_all
+ moreover with a have "inv a \<otimes> (a \<otimes> b) = inv a" by (simp add: ab)
+ ultimately show ?thesis using a b by (simp add: m_assoc [symmetric])
+qed
+
+lemma nonzero_inverse_inverse_eq:
+ "a \<in> carrier R \<Longrightarrow> a \<noteq> \<zero> \<Longrightarrow> inv (inv a) = a"
+ by (rule inverse_unique) simp_all
+
+lemma inv_1 [simp]: "inv \<one> = \<one>"
+ by (rule inverse_unique) simp_all
+
+lemma nonzero_inverse_mult_distrib:
+ assumes "a \<in> carrier R" and "b \<in> carrier R" and "a \<noteq> \<zero>" and "b \<noteq> \<zero>"
+ shows "inv (a \<otimes> b) = inv b \<otimes> inv a"
+proof -
+ have "a \<otimes> (b \<otimes> inv b) \<otimes> inv a = \<one>" using assms by simp
+ hence eq: "a \<otimes> b \<otimes> (inv b \<otimes> inv a) = \<one>" using assms
+ by (simp only: m_assoc m_closed inv_closed assms)
+ from inverse_unique [OF _ _ eq] assms
+ show ?thesis by simp
+qed
+
+lemma nonzero_imp_inverse_nonzero:
+ assumes "a \<in> carrier R" and "a \<noteq> \<zero>"
+ shows "inv a \<noteq> \<zero>"
+proof
+ assume ianz: "inv a = \<zero>"
+ from assms
+ have "\<one> = a \<otimes> inv a" by simp
+ also with assms have "... = \<zero>" by (simp add: ianz)
+ finally have "\<one> = \<zero>" .
+ thus False by (simp add: eq_commute)
+qed
+
+lemma nonzero_divide_divide_eq_left:
+ "a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> c \<in> carrier R \<Longrightarrow> b \<noteq> \<zero> \<Longrightarrow> c \<noteq> \<zero> \<Longrightarrow>
+ a \<oslash> b \<oslash> c = a \<oslash> (b \<otimes> c)"
+ by (simp add: m_div_def nonzero_inverse_mult_distrib m_ac integral_iff)
+
+lemma nonzero_times_divide_eq:
+ "a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> c \<in> carrier R \<Longrightarrow> d \<in> carrier R \<Longrightarrow>
+ b \<noteq> \<zero> \<Longrightarrow> d \<noteq> \<zero> \<Longrightarrow> (a \<oslash> b) \<otimes> (c \<oslash> d) = (a \<otimes> c) \<oslash> (b \<otimes> d)"
+ by (simp add: m_div_def nonzero_inverse_mult_distrib m_ac integral_iff)
+
+lemma nonzero_divide_divide_eq:
+ "a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> c \<in> carrier R \<Longrightarrow> d \<in> carrier R \<Longrightarrow>
+ b \<noteq> \<zero> \<Longrightarrow> c \<noteq> \<zero> \<Longrightarrow> d \<noteq> \<zero> \<Longrightarrow> (a \<oslash> b) \<oslash> (c \<oslash> d) = (a \<otimes> d) \<oslash> (b \<otimes> c)"
+ by (simp add: m_div_def nonzero_inverse_mult_distrib
+ nonzero_imp_inverse_nonzero nonzero_inverse_inverse_eq m_ac integral_iff)
+
+lemma divide_1 [simp]: "x \<in> carrier R \<Longrightarrow> x \<oslash> \<one> = x"
+ by (simp add: m_div_def)
+
+lemma add_frac_eq:
+ assumes "x \<in> carrier R" and "y \<in> carrier R" and "z \<in> carrier R" and "w \<in> carrier R"
+ and "y \<noteq> \<zero>" and "z \<noteq> \<zero>"
+ shows "x \<oslash> y \<oplus> w \<oslash> z = (x \<otimes> z \<oplus> w \<otimes> y) \<oslash> (y \<otimes> z)"
+proof -
+ from assms
+ have "x \<oslash> y \<oplus> w \<oslash> z = x \<otimes> inv y \<otimes> (z \<otimes> inv z) \<oplus> w \<otimes> inv z \<otimes> (y \<otimes> inv y)"
+ by (simp add: m_div_def)
+ also from assms have "\<dots> = (x \<otimes> z \<oplus> w \<otimes> y) \<oslash> (y \<otimes> z)"
+ by (simp add: m_div_def nonzero_inverse_mult_distrib r_distr m_ac integral_iff del: r_inv)
+ finally show ?thesis .
+qed
+
+lemma div_closed [simp]:
+ "x \<in> carrier R \<Longrightarrow> y \<in> carrier R \<Longrightarrow> y \<noteq> \<zero> \<Longrightarrow> x \<oslash> y \<in> carrier R"
+ by (simp add: m_div_def)
+
+lemma minus_divide_left [simp]:
+ "a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> b \<noteq> \<zero> \<Longrightarrow> \<ominus> (a \<oslash> b) = \<ominus> a \<oslash> b"
+ by (simp add: m_div_def l_minus)
+
+lemma diff_frac_eq:
+ assumes "x \<in> carrier R" and "y \<in> carrier R" and "z \<in> carrier R" and "w \<in> carrier R"
+ and "y \<noteq> \<zero>" and "z \<noteq> \<zero>"
+ shows "x \<oslash> y \<ominus> w \<oslash> z = (x \<otimes> z \<ominus> w \<otimes> y) \<oslash> (y \<otimes> z)"
+ using assms
+ by (simp add: minus_eq l_minus add_frac_eq)
+
+lemma nonzero_mult_divide_mult_cancel_left [simp]:
+ assumes "a \<in> carrier R" and "b \<in> carrier R" and "c \<in> carrier R"
+ and "b \<noteq> \<zero>" and "c \<noteq> \<zero>"
+ shows "(c \<otimes> a) \<oslash> (c \<otimes> b) = a \<oslash> b"
+proof -
+ from assms have "(c \<otimes> a) \<oslash> (c \<otimes> b) = c \<otimes> a \<otimes> (inv b \<otimes> inv c)"
+ by (simp add: m_div_def nonzero_inverse_mult_distrib integral_iff)
+ also from assms have "\<dots> = a \<otimes> inv b \<otimes> (inv c \<otimes> c)"
+ by (simp add: m_ac)
+ also from assms have "\<dots> = a \<otimes> inv b" by simp
+ finally show ?thesis using assms by (simp add: m_div_def)
+qed
+
+lemma times_divide_eq_left [simp]:
+ "a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> c \<in> carrier R \<Longrightarrow> c \<noteq> \<zero> \<Longrightarrow>
+ (b \<oslash> c) \<otimes> a = b \<otimes> a \<oslash> c"
+ by (simp add: m_div_def m_ac)
+
+lemma times_divide_eq_right [simp]:
+ "a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> c \<in> carrier R \<Longrightarrow> c \<noteq> \<zero> \<Longrightarrow>
+ a \<otimes> (b \<oslash> c) = a \<otimes> b \<oslash> c"
+ by (simp add: m_div_def m_ac)
+
+lemma nonzero_power_divide:
+ "a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> b \<noteq> \<zero> \<Longrightarrow>
+ (a \<oslash> b) (^) (n::nat) = a (^) n \<oslash> b (^) n"
+ by (induct n) (simp_all add: nonzero_divide_divide_eq_left)
+
+lemma r_diff_distr:
+ "x \<in> carrier R \<Longrightarrow> y \<in> carrier R \<Longrightarrow> z \<in> carrier R \<Longrightarrow>
+ z \<otimes> (x \<ominus> y) = z \<otimes> x \<ominus> z \<otimes> y"
+ by (simp add: minus_eq r_distr r_minus)
+
+lemma divide_zero_left [simp]:
+ "a \<in> carrier R \<Longrightarrow> a \<noteq> \<zero> \<Longrightarrow> \<zero> \<oslash> a = \<zero>"
+ by (simp add: m_div_def)
+
+lemma divide_self: "a \<in> carrier R \<Longrightarrow> a \<noteq> \<zero> \<Longrightarrow> a \<oslash> a = \<one>"
+ by (simp add: m_div_def)
+
+lemma divide_eq_0_iff:
+ assumes "a \<in> carrier R"
+ and "b \<in> carrier R"
+ and "b \<noteq> \<zero>"
+ shows "(a \<oslash> b = \<zero>) = (a = \<zero>)"
+proof
+ assume "a = \<zero>"
+ with assms show "a \<oslash> b = \<zero>" by simp
+next
+ assume "a \<oslash> b = \<zero>"
+ with assms have "b \<otimes> (a \<oslash> b) = b \<otimes> \<zero>" by simp
+ also from assms have "b \<otimes> (a \<oslash> b) = b \<otimes> a \<oslash> b" by simp
+ also from assms have "b \<otimes> a = a \<otimes> b" by (simp add: m_comm)
+ also from assms have "a \<otimes> b \<oslash> b = a \<otimes> (b \<oslash> b)" by simp
+ also from assms have "b \<oslash> b = \<one>" by (simp add: divide_self)
+ finally show "a = \<zero>" using assms by simp
+qed
+
+end
+
+lemma field_class: "field (cring_class_ops::'a::field ring)"
+ apply unfold_locales
+ apply (simp_all add: cring_class_ops_def)
+ apply (auto simp add: Units_def)
+ apply (rule_tac x="1 / x" in exI)
+ apply simp
+ done
+
+lemma div_class: "(x::'a::field) \<oslash>\<^bsub>cring_class_ops\<^esub> y = x / y"
+ apply (simp add: m_div_def m_inv_def class_simps)
+ apply (rule impI)
+ apply (rule ssubst [OF the_equality, of _ "1 / y"])
+ apply simp_all
+ apply (drule conjunct2)
+ apply (drule_tac f="\<lambda>x. x / y" in arg_cong)
+ apply simp
+ done
+
+interpretation field_class: field "cring_class_ops::'a::field ring"
+ rewrites
+ "(\<zero>\<^bsub>cring_class_ops\<^esub>::'a) = 0" and
+ "(\<one>\<^bsub>cring_class_ops\<^esub>::'a) = 1" and
+ "(x::'a) \<oplus>\<^bsub>cring_class_ops\<^esub> y = x + y" and
+ "(x::'a) \<otimes>\<^bsub>cring_class_ops\<^esub> y = x * y" and
+ "\<ominus>\<^bsub>cring_class_ops\<^esub> (x::'a) = - x" and
+ "(x::'a) \<ominus>\<^bsub>cring_class_ops\<^esub> y = x - y" and
+ "(x::'a) (^)\<^bsub>cring_class_ops\<^esub> n = x ^ n" and
+ "\<guillemotleft>n\<guillemotright>\<^sub>\<nat>\<^bsub>cring_class_ops\<^esub> = of_nat n" and
+ "((\<guillemotleft>i\<guillemotright>\<^bsub>cring_class_ops\<^esub>)::'a) = of_int i" and
+ "(x::'a) \<oslash>\<^bsub>cring_class_ops\<^esub> y = x / y" and
+ "(Int.of_int (numeral m)::'a) = numeral m"
+ by (simp_all add: field_class class_simps div_class)
+
+end
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy Sun Jan 29 11:49:48 2017 +0100
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy Sun Jan 29 11:59:48 2017 +0100
@@ -1,4 +1,5 @@
-(* Author: Bernhard Haeupler
+(* Title: HOL/Decision_Procs/Commutative_Ring.thy
+ Author: Bernhard Haeupler, Stefan Berghofer, and Amine Chaieb
Proving equalities in commutative rings done "right" in Isabelle/HOL.
*)
@@ -6,44 +7,91 @@
section \<open>Proving equalities in commutative rings\<close>
theory Commutative_Ring
-imports Main
+imports
+ Conversions
+ Algebra_Aux
+ "~~/src/HOL/Library/Code_Target_Numeral"
begin
text \<open>Syntax of multivariate polynomials (pol) and polynomial expressions.\<close>
-datatype 'a pol =
- Pc 'a
- | Pinj nat "'a pol"
- | PX "'a pol" nat "'a pol"
+datatype pol =
+ Pc int
+ | Pinj nat pol
+ | PX pol nat pol
-datatype 'a polex =
- Pol "'a pol"
- | Add "'a polex" "'a polex"
- | Sub "'a polex" "'a polex"
- | Mul "'a polex" "'a polex"
- | Pow "'a polex" nat
- | Neg "'a polex"
+datatype polex =
+ Var nat
+ | Const int
+ | Add polex polex
+ | Sub polex polex
+ | Mul polex polex
+ | Pow polex nat
+ | Neg polex
text \<open>Interpretation functions for the shadow syntax.\<close>
-primrec Ipol :: "'a::comm_ring_1 list \<Rightarrow> 'a pol \<Rightarrow> 'a"
+context cring begin
+
+definition in_carrier :: "'a list \<Rightarrow> bool" where
+ "in_carrier xs = (\<forall>x\<in>set xs. x \<in> carrier R)"
+
+lemma in_carrier_Nil: "in_carrier []"
+ by (simp add: in_carrier_def)
+
+lemma in_carrier_Cons: "x \<in> carrier R \<Longrightarrow> in_carrier xs \<Longrightarrow> in_carrier (x # xs)"
+ by (simp add: in_carrier_def)
+
+lemma drop_in_carrier [simp]: "in_carrier xs \<Longrightarrow> in_carrier (drop n xs)"
+ using set_drop_subset [of n xs]
+ by (auto simp add: in_carrier_def)
+
+primrec head :: "'a list \<Rightarrow> 'a"
where
- "Ipol l (Pc c) = c"
+ "head [] = \<zero>"
+ | "head (x # xs) = x"
+
+lemma head_closed [simp]: "in_carrier xs \<Longrightarrow> head xs \<in> carrier R"
+ by (cases xs) (simp_all add: in_carrier_def)
+
+primrec Ipol :: "'a list \<Rightarrow> pol \<Rightarrow> 'a"
+where
+ "Ipol l (Pc c) = \<guillemotleft>c\<guillemotright>"
| "Ipol l (Pinj i P) = Ipol (drop i l) P"
- | "Ipol l (PX P x Q) = Ipol l P * (hd l)^x + Ipol (drop 1 l) Q"
+ | "Ipol l (PX P x Q) = Ipol l P \<otimes> head l (^) x \<oplus> Ipol (drop 1 l) Q"
-primrec Ipolex :: "'a::comm_ring_1 list \<Rightarrow> 'a polex \<Rightarrow> 'a"
+lemma Ipol_Pc:
+ "Ipol l (Pc 0) = \<zero>"
+ "Ipol l (Pc 1) = \<one>"
+ "Ipol l (Pc (numeral n)) = \<guillemotleft>numeral n\<guillemotright>"
+ "Ipol l (Pc (- numeral n)) = \<ominus> \<guillemotleft>numeral n\<guillemotright>"
+ by simp_all
+
+lemma Ipol_closed [simp]:
+ "in_carrier l \<Longrightarrow> Ipol l p \<in> carrier R"
+ by (induct p arbitrary: l) simp_all
+
+primrec Ipolex :: "'a list \<Rightarrow> polex \<Rightarrow> 'a"
where
- "Ipolex l (Pol P) = Ipol l P"
- | "Ipolex l (Add P Q) = Ipolex l P + Ipolex l Q"
- | "Ipolex l (Sub P Q) = Ipolex l P - Ipolex l Q"
- | "Ipolex l (Mul P Q) = Ipolex l P * Ipolex l Q"
- | "Ipolex l (Pow p n) = Ipolex l p ^ n"
- | "Ipolex l (Neg P) = - Ipolex l P"
+ "Ipolex l (Var n) = head (drop n l)"
+ | "Ipolex l (Const i) = \<guillemotleft>i\<guillemotright>"
+ | "Ipolex l (Add P Q) = Ipolex l P \<oplus> Ipolex l Q"
+ | "Ipolex l (Sub P Q) = Ipolex l P \<ominus> Ipolex l Q"
+ | "Ipolex l (Mul P Q) = Ipolex l P \<otimes> Ipolex l Q"
+ | "Ipolex l (Pow p n) = Ipolex l p (^) n"
+ | "Ipolex l (Neg P) = \<ominus> Ipolex l P"
+
+lemma Ipolex_Const:
+ "Ipolex l (Const 0) = \<zero>"
+ "Ipolex l (Const 1) = \<one>"
+ "Ipolex l (Const (numeral n)) = \<guillemotleft>numeral n\<guillemotright>"
+ by simp_all
+
+end
text \<open>Create polynomial normalized polynomials given normalized inputs.\<close>
-definition mkPinj :: "nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol"
+definition mkPinj :: "nat \<Rightarrow> pol \<Rightarrow> pol"
where
"mkPinj x P =
(case P of
@@ -51,7 +99,7 @@
| Pinj y P \<Rightarrow> Pinj (x + y) P
| PX p1 y p2 \<Rightarrow> Pinj x P)"
-definition mkPX :: "'a::comm_ring pol \<Rightarrow> nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol"
+definition mkPX :: "pol \<Rightarrow> nat \<Rightarrow> pol \<Rightarrow> pol"
where
"mkPX P i Q =
(case P of
@@ -61,151 +109,154 @@
text \<open>Defining the basic ring operations on normalized polynomials\<close>
-lemma pol_size_nz[simp]: "size (p :: 'a pol) \<noteq> 0"
- by (cases p) simp_all
-
-function add :: "'a::comm_ring pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol" (infixl "\<oplus>" 65)
+function add :: "pol \<Rightarrow> pol \<Rightarrow> pol" (infixl "\<langle>+\<rangle>" 65)
where
- "Pc a \<oplus> Pc b = Pc (a + b)"
-| "Pc c \<oplus> Pinj i P = Pinj i (P \<oplus> Pc c)"
-| "Pinj i P \<oplus> Pc c = Pinj i (P \<oplus> Pc c)"
-| "Pc c \<oplus> PX P i Q = PX P i (Q \<oplus> Pc c)"
-| "PX P i Q \<oplus> Pc c = PX P i (Q \<oplus> Pc c)"
-| "Pinj x P \<oplus> Pinj y Q =
- (if x = y then mkPinj x (P \<oplus> Q)
- else (if x > y then mkPinj y (Pinj (x - y) P \<oplus> Q)
- else mkPinj x (Pinj (y - x) Q \<oplus> P)))"
-| "Pinj x P \<oplus> PX Q y R =
- (if x = 0 then P \<oplus> PX Q y R
- else (if x = 1 then PX Q y (R \<oplus> P)
- else PX Q y (R \<oplus> Pinj (x - 1) P)))"
-| "PX P x R \<oplus> Pinj y Q =
- (if y = 0 then PX P x R \<oplus> Q
- else (if y = 1 then PX P x (R \<oplus> Q)
- else PX P x (R \<oplus> Pinj (y - 1) Q)))"
-| "PX P1 x P2 \<oplus> PX Q1 y Q2 =
- (if x = y then mkPX (P1 \<oplus> Q1) x (P2 \<oplus> Q2)
- else (if x > y then mkPX (PX P1 (x - y) (Pc 0) \<oplus> Q1) y (P2 \<oplus> Q2)
- else mkPX (PX Q1 (y-x) (Pc 0) \<oplus> P1) x (P2 \<oplus> Q2)))"
+ "Pc a \<langle>+\<rangle> Pc b = Pc (a + b)"
+ | "Pc c \<langle>+\<rangle> Pinj i P = Pinj i (P \<langle>+\<rangle> Pc c)"
+ | "Pinj i P \<langle>+\<rangle> Pc c = Pinj i (P \<langle>+\<rangle> Pc c)"
+ | "Pc c \<langle>+\<rangle> PX P i Q = PX P i (Q \<langle>+\<rangle> Pc c)"
+ | "PX P i Q \<langle>+\<rangle> Pc c = PX P i (Q \<langle>+\<rangle> Pc c)"
+ | "Pinj x P \<langle>+\<rangle> Pinj y Q =
+ (if x = y then mkPinj x (P \<langle>+\<rangle> Q)
+ else (if x > y then mkPinj y (Pinj (x - y) P \<langle>+\<rangle> Q)
+ else mkPinj x (Pinj (y - x) Q \<langle>+\<rangle> P)))"
+ | "Pinj x P \<langle>+\<rangle> PX Q y R =
+ (if x = 0 then P \<langle>+\<rangle> PX Q y R
+ else (if x = 1 then PX Q y (R \<langle>+\<rangle> P)
+ else PX Q y (R \<langle>+\<rangle> Pinj (x - 1) P)))"
+ | "PX P x R \<langle>+\<rangle> Pinj y Q =
+ (if y = 0 then PX P x R \<langle>+\<rangle> Q
+ else (if y = 1 then PX P x (R \<langle>+\<rangle> Q)
+ else PX P x (R \<langle>+\<rangle> Pinj (y - 1) Q)))"
+ | "PX P1 x P2 \<langle>+\<rangle> PX Q1 y Q2 =
+ (if x = y then mkPX (P1 \<langle>+\<rangle> Q1) x (P2 \<langle>+\<rangle> Q2)
+ else (if x > y then mkPX (PX P1 (x - y) (Pc 0) \<langle>+\<rangle> Q1) y (P2 \<langle>+\<rangle> Q2)
+ else mkPX (PX Q1 (y - x) (Pc 0) \<langle>+\<rangle> P1) x (P2 \<langle>+\<rangle> Q2)))"
by pat_completeness auto
termination by (relation "measure (\<lambda>(x, y). size x + size y)") auto
-function mul :: "'a::comm_ring pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol" (infixl "\<otimes>" 70)
+function mul :: "pol \<Rightarrow> pol \<Rightarrow> pol" (infixl "\<langle>*\<rangle>" 70)
where
- "Pc a \<otimes> Pc b = Pc (a * b)"
-| "Pc c \<otimes> Pinj i P =
- (if c = 0 then Pc 0 else mkPinj i (P \<otimes> Pc c))"
-| "Pinj i P \<otimes> Pc c =
- (if c = 0 then Pc 0 else mkPinj i (P \<otimes> Pc c))"
-| "Pc c \<otimes> PX P i Q =
- (if c = 0 then Pc 0 else mkPX (P \<otimes> Pc c) i (Q \<otimes> Pc c))"
-| "PX P i Q \<otimes> Pc c =
- (if c = 0 then Pc 0 else mkPX (P \<otimes> Pc c) i (Q \<otimes> Pc c))"
-| "Pinj x P \<otimes> Pinj y Q =
- (if x = y then mkPinj x (P \<otimes> Q)
- else
- (if x > y then mkPinj y (Pinj (x-y) P \<otimes> Q)
- else mkPinj x (Pinj (y - x) Q \<otimes> P)))"
-| "Pinj x P \<otimes> PX Q y R =
- (if x = 0 then P \<otimes> PX Q y R
- else
- (if x = 1 then mkPX (Pinj x P \<otimes> Q) y (R \<otimes> P)
- else mkPX (Pinj x P \<otimes> Q) y (R \<otimes> Pinj (x - 1) P)))"
-| "PX P x R \<otimes> Pinj y Q =
- (if y = 0 then PX P x R \<otimes> Q
- else
- (if y = 1 then mkPX (Pinj y Q \<otimes> P) x (R \<otimes> Q)
- else mkPX (Pinj y Q \<otimes> P) x (R \<otimes> Pinj (y - 1) Q)))"
-| "PX P1 x P2 \<otimes> PX Q1 y Q2 =
- mkPX (P1 \<otimes> Q1) (x + y) (P2 \<otimes> Q2) \<oplus>
- (mkPX (P1 \<otimes> mkPinj 1 Q2) x (Pc 0) \<oplus>
- (mkPX (Q1 \<otimes> mkPinj 1 P2) y (Pc 0)))"
+ "Pc a \<langle>*\<rangle> Pc b = Pc (a * b)"
+ | "Pc c \<langle>*\<rangle> Pinj i P =
+ (if c = 0 then Pc 0 else mkPinj i (P \<langle>*\<rangle> Pc c))"
+ | "Pinj i P \<langle>*\<rangle> Pc c =
+ (if c = 0 then Pc 0 else mkPinj i (P \<langle>*\<rangle> Pc c))"
+ | "Pc c \<langle>*\<rangle> PX P i Q =
+ (if c = 0 then Pc 0 else mkPX (P \<langle>*\<rangle> Pc c) i (Q \<langle>*\<rangle> Pc c))"
+ | "PX P i Q \<langle>*\<rangle> Pc c =
+ (if c = 0 then Pc 0 else mkPX (P \<langle>*\<rangle> Pc c) i (Q \<langle>*\<rangle> Pc c))"
+ | "Pinj x P \<langle>*\<rangle> Pinj y Q =
+ (if x = y then mkPinj x (P \<langle>*\<rangle> Q)
+ else
+ (if x > y then mkPinj y (Pinj (x - y) P \<langle>*\<rangle> Q)
+ else mkPinj x (Pinj (y - x) Q \<langle>*\<rangle> P)))"
+ | "Pinj x P \<langle>*\<rangle> PX Q y R =
+ (if x = 0 then P \<langle>*\<rangle> PX Q y R
+ else
+ (if x = 1 then mkPX (Pinj x P \<langle>*\<rangle> Q) y (R \<langle>*\<rangle> P)
+ else mkPX (Pinj x P \<langle>*\<rangle> Q) y (R \<langle>*\<rangle> Pinj (x - 1) P)))"
+ | "PX P x R \<langle>*\<rangle> Pinj y Q =
+ (if y = 0 then PX P x R \<langle>*\<rangle> Q
+ else
+ (if y = 1 then mkPX (Pinj y Q \<langle>*\<rangle> P) x (R \<langle>*\<rangle> Q)
+ else mkPX (Pinj y Q \<langle>*\<rangle> P) x (R \<langle>*\<rangle> Pinj (y - 1) Q)))"
+ | "PX P1 x P2 \<langle>*\<rangle> PX Q1 y Q2 =
+ mkPX (P1 \<langle>*\<rangle> Q1) (x + y) (P2 \<langle>*\<rangle> Q2) \<langle>+\<rangle>
+ (mkPX (P1 \<langle>*\<rangle> mkPinj 1 Q2) x (Pc 0) \<langle>+\<rangle>
+ (mkPX (Q1 \<langle>*\<rangle> mkPinj 1 P2) y (Pc 0)))"
by pat_completeness auto
termination by (relation "measure (\<lambda>(x, y). size x + size y)")
(auto simp add: mkPinj_def split: pol.split)
text \<open>Negation\<close>
-primrec neg :: "'a::comm_ring pol \<Rightarrow> 'a pol"
+primrec neg :: "pol \<Rightarrow> pol"
where
- "neg (Pc c) = Pc (-c)"
-| "neg (Pinj i P) = Pinj i (neg P)"
-| "neg (PX P x Q) = PX (neg P) x (neg Q)"
+ "neg (Pc c) = Pc (- c)"
+ | "neg (Pinj i P) = Pinj i (neg P)"
+ | "neg (PX P x Q) = PX (neg P) x (neg Q)"
-text \<open>Substraction\<close>
-definition sub :: "'a::comm_ring pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol" (infixl "\<ominus>" 65)
- where "sub P Q = P \<oplus> neg Q"
+text \<open>Subtraction\<close>
+definition sub :: "pol \<Rightarrow> pol \<Rightarrow> pol" (infixl "\<langle>-\<rangle>" 65)
+where
+ "sub P Q = P \<langle>+\<rangle> neg Q"
-text \<open>Square for Fast Exponentation\<close>
-primrec sqr :: "'a::comm_ring_1 pol \<Rightarrow> 'a pol"
+text \<open>Square for Fast Exponentiation\<close>
+primrec sqr :: "pol \<Rightarrow> pol"
where
- "sqr (Pc c) = Pc (c * c)"
-| "sqr (Pinj i P) = mkPinj i (sqr P)"
-| "sqr (PX A x B) =
- mkPX (sqr A) (x + x) (sqr B) \<oplus> mkPX (Pc (1 + 1) \<otimes> A \<otimes> mkPinj 1 B) x (Pc 0)"
+ "sqr (Pc c) = Pc (c * c)"
+ | "sqr (Pinj i P) = mkPinj i (sqr P)"
+ | "sqr (PX A x B) = mkPX (sqr A) (x + x) (sqr B) \<langle>+\<rangle>
+ mkPX (Pc 2 \<langle>*\<rangle> A \<langle>*\<rangle> mkPinj 1 B) x (Pc 0)"
-text \<open>Fast Exponentation\<close>
+text \<open>Fast Exponentiation\<close>
-fun pow :: "nat \<Rightarrow> 'a::comm_ring_1 pol \<Rightarrow> 'a pol"
+fun pow :: "nat \<Rightarrow> pol \<Rightarrow> pol"
where
pow_if [simp del]: "pow n P =
(if n = 0 then Pc 1
else if even n then pow (n div 2) (sqr P)
- else P \<otimes> pow (n div 2) (sqr P))"
+ else P \<langle>*\<rangle> pow (n div 2) (sqr P))"
lemma pow_simps [simp]:
"pow 0 P = Pc 1"
"pow (2 * n) P = pow n (sqr P)"
- "pow (Suc (2 * n)) P = P \<otimes> pow n (sqr P)"
+ "pow (Suc (2 * n)) P = P \<langle>*\<rangle> pow n (sqr P)"
by (simp_all add: pow_if)
lemma even_pow: "even n \<Longrightarrow> pow n P = pow (n div 2) (sqr P)"
by (erule evenE) simp
-lemma odd_pow: "odd n \<Longrightarrow> pow n P = P \<otimes> pow (n div 2) (sqr P)"
+lemma odd_pow: "odd n \<Longrightarrow> pow n P = P \<langle>*\<rangle> pow (n div 2) (sqr P)"
by (erule oddE) simp
text \<open>Normalization of polynomial expressions\<close>
-primrec norm :: "'a::comm_ring_1 polex \<Rightarrow> 'a pol"
+primrec norm :: "polex \<Rightarrow> pol"
where
- "norm (Pol P) = P"
-| "norm (Add P Q) = norm P \<oplus> norm Q"
-| "norm (Sub P Q) = norm P \<ominus> norm Q"
-| "norm (Mul P Q) = norm P \<otimes> norm Q"
-| "norm (Pow P n) = pow n (norm P)"
-| "norm (Neg P) = neg (norm P)"
+ "norm (Var n) =
+ (if n = 0 then PX (Pc 1) 1 (Pc 0)
+ else Pinj n (PX (Pc 1) 1 (Pc 0)))"
+ | "norm (Const i) = Pc i"
+ | "norm (Add P Q) = norm P \<langle>+\<rangle> norm Q"
+ | "norm (Sub P Q) = norm P \<langle>-\<rangle> norm Q"
+ | "norm (Mul P Q) = norm P \<langle>*\<rangle> norm Q"
+ | "norm (Pow P n) = pow n (norm P)"
+ | "norm (Neg P) = neg (norm P)"
+
+context cring
+begin
text \<open>mkPinj preserve semantics\<close>
lemma mkPinj_ci: "Ipol l (mkPinj a B) = Ipol l (Pinj a B)"
by (induct B) (auto simp add: mkPinj_def algebra_simps)
text \<open>mkPX preserves semantics\<close>
-lemma mkPX_ci: "Ipol l (mkPX A b C) = Ipol l (PX A b C)"
- by (cases A) (auto simp add: mkPX_def mkPinj_ci power_add algebra_simps)
+lemma mkPX_ci: "in_carrier l \<Longrightarrow> Ipol l (mkPX A b C) = Ipol l (PX A b C)"
+ by (cases A) (auto simp add: mkPX_def mkPinj_ci nat_pow_mult [symmetric] m_ac)
text \<open>Correctness theorems for the implemented operations\<close>
text \<open>Negation\<close>
-lemma neg_ci: "Ipol l (neg P) = -(Ipol l P)"
- by (induct P arbitrary: l) auto
+lemma neg_ci: "in_carrier l \<Longrightarrow> Ipol l (neg P) = \<ominus> (Ipol l P)"
+ by (induct P arbitrary: l) (auto simp add: minus_add l_minus)
text \<open>Addition\<close>
-lemma add_ci: "Ipol l (P \<oplus> Q) = Ipol l P + Ipol l Q"
+lemma add_ci: "in_carrier l \<Longrightarrow> Ipol l (P \<langle>+\<rangle> Q) = Ipol l P \<oplus> Ipol l Q"
proof (induct P Q arbitrary: l rule: add.induct)
case (6 x P y Q)
consider "x < y" | "x = y" | "x > y" by arith
- then
- show ?case
+ then show ?case
proof cases
case 1
- with 6 show ?thesis by (simp add: mkPinj_ci algebra_simps)
+ with 6 show ?thesis by (simp add: mkPinj_ci a_ac)
next
case 2
with 6 show ?thesis by (simp add: mkPinj_ci)
next
case 3
- with 6 show ?thesis by (simp add: mkPinj_ci algebra_simps)
+ with 6 show ?thesis by (simp add: mkPinj_ci)
qed
next
case (7 x P Q y R)
@@ -216,14 +267,14 @@
with 7 show ?thesis by simp
next
case 2
- with 7 show ?thesis by (simp add: algebra_simps)
+ with 7 show ?thesis by (simp add: a_ac)
next
case 3
- from 7 show ?thesis by (cases x) simp_all
+ with 7 show ?thesis by (cases x) (simp_all add: a_ac)
qed
next
case (8 P x R y Q)
- then show ?case by simp
+ then show ?case by (simp add: a_ac)
next
case (9 P1 x P2 Q1 y Q2)
consider "x = y" | d where "d + x = y" | d where "d + y = x"
@@ -231,80 +282,696 @@
then show ?case
proof cases
case 1
- with 9 show ?thesis by (simp add: mkPX_ci algebra_simps)
+ with 9 show ?thesis by (simp add: mkPX_ci r_distr a_ac m_ac)
next
case 2
- with 9 show ?thesis by (auto simp add: mkPX_ci power_add algebra_simps)
+ with 9 show ?thesis by (auto simp add: mkPX_ci nat_pow_mult [symmetric] r_distr a_ac m_ac)
next
case 3
- with 9 show ?thesis by (auto simp add: power_add mkPX_ci algebra_simps)
+ with 9 show ?thesis by (auto simp add: nat_pow_mult [symmetric] mkPX_ci r_distr a_ac m_ac)
qed
-qed (auto simp add: algebra_simps)
+qed (auto simp add: a_ac m_ac)
text \<open>Multiplication\<close>
-lemma mul_ci: "Ipol l (P \<otimes> Q) = Ipol l P * Ipol l Q"
+lemma mul_ci: "in_carrier l \<Longrightarrow> Ipol l (P \<langle>*\<rangle> Q) = Ipol l P \<otimes> Ipol l Q"
by (induct P Q arbitrary: l rule: mul.induct)
- (simp_all add: mkPX_ci mkPinj_ci algebra_simps add_ci power_add)
+ (simp_all add: mkPX_ci mkPinj_ci a_ac m_ac r_distr add_ci nat_pow_mult [symmetric])
-text \<open>Substraction\<close>
-lemma sub_ci: "Ipol l (P \<ominus> Q) = Ipol l P - Ipol l Q"
- by (simp add: add_ci neg_ci sub_def)
+text \<open>Subtraction\<close>
+lemma sub_ci: "in_carrier l \<Longrightarrow> Ipol l (P \<langle>-\<rangle> Q) = Ipol l P \<ominus> Ipol l Q"
+ by (simp add: add_ci neg_ci sub_def minus_eq)
text \<open>Square\<close>
-lemma sqr_ci: "Ipol ls (sqr P) = Ipol ls P * Ipol ls P"
+lemma sqr_ci: "in_carrier ls \<Longrightarrow> Ipol ls (sqr P) = Ipol ls P \<otimes> Ipol ls P"
by (induct P arbitrary: ls)
- (simp_all add: add_ci mkPinj_ci mkPX_ci mul_ci algebra_simps power_add)
+ (simp_all add: add_ci mkPinj_ci mkPX_ci mul_ci l_distr r_distr
+ a_ac m_ac nat_pow_mult [symmetric] of_int_2)
text \<open>Power\<close>
-lemma pow_ci: "Ipol ls (pow n P) = Ipol ls P ^ n"
+lemma pow_ci: "in_carrier ls \<Longrightarrow> Ipol ls (pow n P) = Ipol ls P (^) n"
proof (induct n arbitrary: P rule: less_induct)
case (less k)
consider "k = 0" | "k > 0" by arith
- then
- show ?case
+ then show ?case
proof cases
case 1
then show ?thesis by simp
next
case 2
then have "k div 2 < k" by arith
- with less have *: "Ipol ls (pow (k div 2) (sqr P)) = Ipol ls (sqr P) ^ (k div 2)"
+ with less have *: "Ipol ls (pow (k div 2) (sqr P)) = Ipol ls (sqr P) (^) (k div 2)"
by simp
show ?thesis
proof (cases "even k")
case True
- with * show ?thesis
- by (simp add: even_pow sqr_ci power_mult_distrib power_add [symmetric]
+ with * \<open>in_carrier ls\<close> show ?thesis
+ by (simp add: even_pow sqr_ci nat_pow_distr nat_pow_mult
mult_2 [symmetric] even_two_times_div_two)
next
case False
- with * show ?thesis
- by (simp add: odd_pow mul_ci sqr_ci power_mult_distrib power_add [symmetric]
- mult_2 [symmetric] power_Suc [symmetric])
+ with * \<open>in_carrier ls\<close> show ?thesis
+ by (simp add: odd_pow mul_ci sqr_ci nat_pow_distr nat_pow_mult
+ mult_2 [symmetric] trans [OF nat_pow_Suc m_comm, symmetric])
qed
qed
qed
text \<open>Normalization preserves semantics\<close>
-lemma norm_ci: "Ipolex l Pe = Ipol l (norm Pe)"
+lemma norm_ci: "in_carrier l \<Longrightarrow> Ipolex l Pe = Ipol l (norm Pe)"
by (induct Pe) (simp_all add: add_ci sub_ci mul_ci neg_ci pow_ci)
text \<open>Reflection lemma: Key to the (incomplete) decision procedure\<close>
lemma norm_eq:
- assumes "norm P1 = norm P2"
+ assumes "in_carrier l"
+ and "norm P1 = norm P2"
shows "Ipolex l P1 = Ipolex l P2"
proof -
- from assms have "Ipol l (norm P1) = Ipol l (norm P2)"
+ from assms have "Ipol l (norm P1) = Ipol l (norm P2)" by simp
+ with assms show ?thesis by (simp only: norm_ci)
+qed
+
+end
+
+
+text \<open>Monomials\<close>
+
+datatype mon =
+ Mc int
+ | Minj nat mon
+ | MX nat mon
+
+primrec (in cring)
+ Imon :: "'a list \<Rightarrow> mon \<Rightarrow> 'a"
+where
+ "Imon l (Mc c) = \<guillemotleft>c\<guillemotright>"
+ | "Imon l (Minj i M) = Imon (drop i l) M"
+ | "Imon l (MX x M) = Imon (drop 1 l) M \<otimes> head l (^) x"
+
+lemma (in cring) Imon_closed [simp]:
+ "in_carrier l \<Longrightarrow> Imon l m \<in> carrier R"
+ by (induct m arbitrary: l) simp_all
+
+definition
+ mkMinj :: "nat \<Rightarrow> mon \<Rightarrow> mon" where
+ "mkMinj i M = (case M of
+ Mc c \<Rightarrow> Mc c
+ | Minj j M \<Rightarrow> Minj (i + j) M
+ | _ \<Rightarrow> Minj i M)"
+
+definition
+ Minj_pred :: "nat \<Rightarrow> mon \<Rightarrow> mon" where
+ "Minj_pred i M = (if i = 1 then M else mkMinj (i - 1) M)"
+
+primrec mkMX :: "nat \<Rightarrow> mon \<Rightarrow> mon"
+where
+ "mkMX i (Mc c) = MX i (Mc c)"
+| "mkMX i (Minj j M) = (if j = 0 then mkMX i M else MX i (Minj_pred j M))"
+| "mkMX i (MX j M) = MX (i + j) M"
+
+lemma (in cring) mkMinj_correct:
+ "Imon l (mkMinj i M) = Imon l (Minj i M)"
+ by (simp add: mkMinj_def add.commute split: mon.split)
+
+lemma (in cring) Minj_pred_correct:
+ "0 < i \<Longrightarrow> Imon (drop 1 l) (Minj_pred i M) = Imon l (Minj i M)"
+ by (simp add: Minj_pred_def mkMinj_correct)
+
+lemma (in cring) mkMX_correct:
+ "in_carrier l \<Longrightarrow> Imon l (mkMX i M) = Imon l M \<otimes> head l (^) i"
+ by (induct M) (simp_all add: Minj_pred_correct [simplified] nat_pow_mult [symmetric] m_ac split: mon.split)
+
+fun cfactor :: "pol \<Rightarrow> int \<Rightarrow> pol \<times> pol"
+where
+ "cfactor (Pc c') c = (Pc (c' mod c), Pc (c' div c))"
+| "cfactor (Pinj i P) c =
+ (let (R, S) = cfactor P c
+ in (mkPinj i R, mkPinj i S))"
+| "cfactor (PX P i Q) c =
+ (let
+ (R1, S1) = cfactor P c;
+ (R2, S2) = cfactor Q c
+ in (mkPX R1 i R2, mkPX S1 i S2))"
+
+lemma (in cring) cfactor_correct:
+ "in_carrier l \<Longrightarrow> Ipol l P = Ipol l (fst (cfactor P c)) \<oplus> \<guillemotleft>c\<guillemotright> \<otimes> Ipol l (snd (cfactor P c))"
+proof (induct P c arbitrary: l rule: cfactor.induct)
+ case (1 c' c)
+ show ?case
+ by (simp add: of_int_mult [symmetric] of_int_add [symmetric] del: of_int_mult)
+next
+ case (2 i P c)
+ then show ?case
+ by (simp add: mkPinj_ci split_beta)
+next
+ case (3 P i Q c)
+ from 3(1) 3(2) [OF refl prod.collapse] 3(3)
+ show ?case
+ by (simp add: mkPX_ci r_distr a_ac m_ac split_beta)
+qed
+
+fun mfactor :: "pol \<Rightarrow> mon \<Rightarrow> pol \<times> pol"
+where
+ "mfactor P (Mc c) = (if c = 1 then (Pc 0, P) else cfactor P c)"
+| "mfactor (Pc d) M = (Pc d, Pc 0)"
+| "mfactor (Pinj i P) (Minj j M) =
+ (if i = j then
+ let (R, S) = mfactor P M
+ in (mkPinj i R, mkPinj i S)
+ else if i < j then
+ let (R, S) = mfactor P (Minj (j - i) M)
+ in (mkPinj i R, mkPinj i S)
+ else (Pinj i P, Pc 0))"
+| "mfactor (Pinj i P) (MX j M) = (Pinj i P, Pc 0)"
+| "mfactor (PX P i Q) (Minj j M) =
+ (if j = 0 then mfactor (PX P i Q) M
+ else
+ let
+ (R1, S1) = mfactor P (Minj j M);
+ (R2, S2) = mfactor Q (Minj_pred j M)
+ in (mkPX R1 i R2, mkPX S1 i S2))"
+| "mfactor (PX P i Q) (MX j M) =
+ (if i = j then
+ let (R, S) = mfactor P (mkMinj 1 M)
+ in (mkPX R i Q, S)
+ else if i < j then
+ let (R, S) = mfactor P (MX (j - i) M)
+ in (mkPX R i Q, S)
+ else
+ let (R, S) = mfactor P (mkMinj 1 M)
+ in (mkPX R i Q, mkPX S (i - j) (Pc 0)))"
+
+lemmas mfactor_induct = mfactor.induct
+ [case_names Mc Pc_Minj Pc_MX Pinj_Minj Pinj_MX PX_Minj PX_MX]
+
+lemma (in cring) mfactor_correct:
+ "in_carrier l \<Longrightarrow>
+ Ipol l P =
+ Ipol l (fst (mfactor P M)) \<oplus>
+ Imon l M \<otimes> Ipol l (snd (mfactor P M))"
+proof (induct P M arbitrary: l rule: mfactor_induct)
+ case (Mc P c)
+ then show ?case
+ by (simp add: cfactor_correct)
+next
+ case (Pc_Minj d i M)
+ then show ?case
by simp
- then show ?thesis
- by (simp only: norm_ci)
+next
+ case (Pc_MX d i M)
+ then show ?case
+ by simp
+next
+ case (Pinj_Minj i P j M)
+ then show ?case
+ by (simp add: mkPinj_ci split_beta)
+next
+ case (Pinj_MX i P j M)
+ then show ?case
+ by simp
+next
+ case (PX_Minj P i Q j M)
+ from PX_Minj(1,2) PX_Minj(3) [OF _ refl prod.collapse] PX_Minj(4)
+ show ?case
+ by (simp add: mkPX_ci Minj_pred_correct [simplified] r_distr a_ac m_ac split_beta)
+next
+ case (PX_MX P i Q j M)
+ from \<open>in_carrier l\<close>
+ have eq1: "(Imon (drop (Suc 0) l) M \<otimes> head l (^) (j - i)) \<otimes>
+ Ipol l (snd (mfactor P (MX (j - i) M))) \<otimes> head l (^) i =
+ Imon (drop (Suc 0) l) M \<otimes>
+ Ipol l (snd (mfactor P (MX (j - i) M))) \<otimes>
+ (head l (^) (j - i) \<otimes> head l (^) i)"
+ by (simp add: m_ac)
+ from \<open>in_carrier l\<close>
+ have eq2: "(Imon (drop (Suc 0) l) M \<otimes> head l (^) j) \<otimes>
+ (Ipol l (snd (mfactor P (mkMinj (Suc 0) M))) \<otimes> head l (^) (i - j)) =
+ Imon (drop (Suc 0) l) M \<otimes>
+ Ipol l (snd (mfactor P (mkMinj (Suc 0) M))) \<otimes>
+ (head l (^) (i - j) \<otimes> head l (^) j)"
+ by (simp add: m_ac)
+ from PX_MX \<open>in_carrier l\<close> show ?case
+ by (simp add: mkPX_ci mkMinj_correct l_distr eq1 eq2 split_beta nat_pow_mult)
+ (simp add: a_ac m_ac)
qed
+primrec mon_of_pol :: "pol \<Rightarrow> mon option"
+where
+ "mon_of_pol (Pc c) = Some (Mc c)"
+| "mon_of_pol (Pinj i P) = (case mon_of_pol P of
+ None \<Rightarrow> None
+ | Some M \<Rightarrow> Some (mkMinj i M))"
+| "mon_of_pol (PX P i Q) =
+ (if Q = Pc 0 then (case mon_of_pol P of
+ None \<Rightarrow> None
+ | Some M \<Rightarrow> Some (mkMX i M))
+ else None)"
-ML_file "commutative_ring_tac.ML"
+lemma (in cring) mon_of_pol_correct:
+ assumes "in_carrier l"
+ and "mon_of_pol P = Some M"
+ shows "Ipol l P = Imon l M"
+ using assms
+proof (induct P arbitrary: M l)
+ case (PX P1 i P2)
+ from PX(1,3,4)
+ show ?case
+ by (auto simp add: mkMinj_correct mkMX_correct split: if_split_asm option.split_asm)
+qed (auto simp add: mkMinj_correct split: option.split_asm)
+
+fun (in cring) Ipolex_polex_list :: "'a list \<Rightarrow> (polex \<times> polex) list \<Rightarrow> bool"
+where
+ "Ipolex_polex_list l [] = True"
+| "Ipolex_polex_list l ((P, Q) # pps) = ((Ipolex l P = Ipolex l Q) \<and> Ipolex_polex_list l pps)"
+
+fun (in cring) Imon_pol_list :: "'a list \<Rightarrow> (mon \<times> pol) list \<Rightarrow> bool"
+where
+ "Imon_pol_list l [] = True"
+| "Imon_pol_list l ((M, P) # mps) = ((Imon l M = Ipol l P) \<and> Imon_pol_list l mps)"
+
+fun mk_monpol_list :: "(polex \<times> polex) list \<Rightarrow> (mon \<times> pol) list"
+where
+ "mk_monpol_list [] = []"
+| "mk_monpol_list ((P, Q) # pps) =
+ (case mon_of_pol (norm P) of
+ None \<Rightarrow> mk_monpol_list pps
+ | Some M \<Rightarrow> (M, norm Q) # mk_monpol_list pps)"
+
+lemma (in cring) mk_monpol_list_correct:
+ "in_carrier l \<Longrightarrow> Ipolex_polex_list l pps \<Longrightarrow> Imon_pol_list l (mk_monpol_list pps)"
+ by (induct pps rule: mk_monpol_list.induct)
+ (auto split: option.split
+ simp add: norm_ci [symmetric] mon_of_pol_correct [symmetric])
+
+definition ponesubst :: "pol \<Rightarrow> mon \<Rightarrow> pol \<Rightarrow> pol option" where
+ "ponesubst P1 M P2 =
+ (let (Q, R) = mfactor P1 M
+ in case R of
+ Pc c \<Rightarrow> if c = 0 then None else Some (add Q (mul P2 R))
+ | _ \<Rightarrow> Some (add Q (mul P2 R)))"
+
+fun pnsubst1 :: "pol \<Rightarrow> mon \<Rightarrow> pol \<Rightarrow> nat \<Rightarrow> pol"
+where
+ "pnsubst1 P1 M P2 n = (case ponesubst P1 M P2 of
+ None \<Rightarrow> P1
+ | Some P3 \<Rightarrow> if n = 0 then P3 else pnsubst1 P3 M P2 (n - 1))"
+
+lemma pnsubst1_0 [simp]: "pnsubst1 P1 M P2 0 = (case ponesubst P1 M P2 of
+ None \<Rightarrow> P1 | Some P3 \<Rightarrow> P3)"
+ by (simp split: option.split)
+
+lemma pnsubst1_Suc [simp]: "pnsubst1 P1 M P2 (Suc n) = (case ponesubst P1 M P2 of
+ None \<Rightarrow> P1 | Some P3 \<Rightarrow> pnsubst1 P3 M P2 n)"
+ by (simp split: option.split)
+
+declare pnsubst1.simps [simp del]
+
+definition pnsubst :: "pol \<Rightarrow> mon \<Rightarrow> pol \<Rightarrow> nat \<Rightarrow> pol option" where
+ "pnsubst P1 M P2 n = (case ponesubst P1 M P2 of
+ None \<Rightarrow> None
+ | Some P3 \<Rightarrow> Some (pnsubst1 P3 M P2 n))"
+
+fun psubstl1 :: "pol \<Rightarrow> (mon \<times> pol) list \<Rightarrow> nat \<Rightarrow> pol"
+where
+ "psubstl1 P1 [] n = P1"
+| "psubstl1 P1 ((M, P2) # mps) n = psubstl1 (pnsubst1 P1 M P2 n) mps n"
+
+fun psubstl :: "pol \<Rightarrow> (mon \<times> pol) list \<Rightarrow> nat \<Rightarrow> pol option"
+where
+ "psubstl P1 [] n = None"
+| "psubstl P1 ((M, P2) # mps) n = (case pnsubst P1 M P2 n of
+ None \<Rightarrow> psubstl P1 mps n
+ | Some P3 \<Rightarrow> Some (psubstl1 P3 mps n))"
+
+fun pnsubstl :: "pol \<Rightarrow> (mon \<times> pol) list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> pol"
+where
+ "pnsubstl P1 mps m n = (case psubstl P1 mps n of
+ None \<Rightarrow> P1
+ | Some P3 \<Rightarrow> if m = 0 then P3 else pnsubstl P3 mps (m - 1) n)"
+
+lemma pnsubstl_0 [simp]: "pnsubstl P1 mps 0 n = (case psubstl P1 mps n of
+ None \<Rightarrow> P1 | Some P3 \<Rightarrow> P3)"
+ by (simp split: option.split)
+
+lemma pnsubstl_Suc [simp]: "pnsubstl P1 mps (Suc m) n = (case psubstl P1 mps n of
+ None \<Rightarrow> P1 | Some P3 \<Rightarrow> pnsubstl P3 mps m n)"
+ by (simp split: option.split)
+
+declare pnsubstl.simps [simp del]
+
+lemma (in cring) ponesubst_correct:
+ "in_carrier l \<Longrightarrow> ponesubst P1 M P2 = Some P3 \<Longrightarrow> Imon l M = Ipol l P2 \<Longrightarrow> Ipol l P1 = Ipol l P3"
+ by (auto simp add: ponesubst_def split_beta mfactor_correct [of l P1 M]
+ add_ci mul_ci split: pol.split_asm if_split_asm)
+
+lemma (in cring) pnsubst1_correct:
+ "in_carrier l \<Longrightarrow> Imon l M = Ipol l P2 \<Longrightarrow> Ipol l (pnsubst1 P1 M P2 n) = Ipol l P1"
+ by (induct n arbitrary: P1)
+ (simp_all add: ponesubst_correct split: option.split)
+
+lemma (in cring) pnsubst_correct:
+ "in_carrier l \<Longrightarrow> pnsubst P1 M P2 n = Some P3 \<Longrightarrow> Imon l M = Ipol l P2 \<Longrightarrow> Ipol l P1 = Ipol l P3"
+ by (auto simp add: pnsubst_def
+ pnsubst1_correct ponesubst_correct split: option.split_asm)
+
+lemma (in cring) psubstl1_correct:
+ "in_carrier l \<Longrightarrow> Imon_pol_list l mps \<Longrightarrow> Ipol l (psubstl1 P1 mps n) = Ipol l P1"
+ by (induct P1 mps n rule: psubstl1.induct) (simp_all add: pnsubst1_correct)
+
+lemma (in cring) psubstl_correct:
+ "in_carrier l \<Longrightarrow> psubstl P1 mps n = Some P2 \<Longrightarrow> Imon_pol_list l mps \<Longrightarrow> Ipol l P1 = Ipol l P2"
+ by (induct P1 mps n rule: psubstl.induct)
+ (auto simp add: psubstl1_correct pnsubst_correct split: option.split_asm)
+
+lemma (in cring) pnsubstl_correct:
+ "in_carrier l \<Longrightarrow> Imon_pol_list l mps \<Longrightarrow> Ipol l (pnsubstl P1 mps m n) = Ipol l P1"
+ by (induct m arbitrary: P1)
+ (simp_all add: psubstl_correct split: option.split)
+
+lemma (in cring) norm_subst_correct:
+ "in_carrier l \<Longrightarrow> Ipolex_polex_list l pps \<Longrightarrow>
+ Ipolex l P = Ipol l (pnsubstl (norm P) (mk_monpol_list pps) m n)"
+ by (simp add: pnsubstl_correct mk_monpol_list_correct norm_ci)
+
+lemma in_carrier_trivial: "cring_class.in_carrier l"
+ by (induct l) (simp_all add: cring_class.in_carrier_def carrier_class)
+
+code_reflect Ring_Code
+ datatypes pol = Pc | Pinj | PX
+ and polex = Var | Const | Add | Sub | Mul | Pow | Neg
+ and nat and int
+ functions norm pnsubstl mk_monpol_list
+ Nat.zero_nat_inst.zero_nat Nat.one_nat_inst.one_nat
+ Nat.minus_nat_inst.minus_nat Nat.times_nat_inst.times_nat nat_of_integer integer_of_nat
+ Int.zero_int_inst.zero_int Int.one_int_inst.one_int
+ Int.uminus_int_inst.uminus_int
+ int_of_integer
+ term_of_pol_inst.term_of_pol
+ term_of_polex_inst.term_of_polex
+ equal_pol_inst.equal_pol
+
+definition ring_codegen_aux :: "pol itself" where
+ "ring_codegen_aux = (Code_Evaluation.TERM_OF_EQUAL::pol itself)"
+
+ML \<open>
+signature RING_TAC =
+sig
+ structure Ring_Simps:
+ sig
+ type T
+ val get: Context.generic -> T
+ val put: T -> Context.generic -> Context.generic
+ val map: (T -> T) -> Context.generic -> Context.generic
+ end
+ val insert_rules: ((term * 'a) * (term * 'a) -> bool) -> (term * 'a) ->
+ (term * 'a) Net.net -> (term * 'a) Net.net
+ val eq_ring_simps:
+ (term * (thm list * thm list * thm list * thm list * thm * thm)) *
+ (term * (thm list * thm list * thm list * thm list * thm * thm)) -> bool
+ val ring_tac: bool -> thm list -> Proof.context -> int -> tactic
+ val get_matching_rules: Proof.context -> (term * 'a) Net.net -> term -> 'a option
+ val norm: thm -> thm
+ val mk_in_carrier: Proof.context -> term -> thm list -> (string * typ) list -> thm
+ val mk_ring: typ -> term
+end
+
+structure Ring_Tac : RING_TAC =
+struct
+
+fun eq_ring_simps
+ ((t, (ths1, ths2, ths3, ths4, th5, th)),
+ (t', (ths1', ths2', ths3', ths4', th5', th'))) =
+ t aconv t' andalso
+ eq_list Thm.eq_thm (ths1, ths1') andalso
+ eq_list Thm.eq_thm (ths2, ths2') andalso
+ eq_list Thm.eq_thm (ths3, ths3') andalso
+ eq_list Thm.eq_thm (ths4, ths4') andalso
+ Thm.eq_thm (th5, th5') andalso
+ Thm.eq_thm (th, th');
+
+structure Ring_Simps = Generic_Data
+(struct
+ type T = (term * (thm list * thm list * thm list * thm list * thm * thm)) Net.net
+ val empty = Net.empty
+ val extend = I
+ val merge = Net.merge eq_ring_simps
+end);
+
+fun get_matching_rules ctxt net t = get_first
+ (fn (p, x) =>
+ if Pattern.matches (Proof_Context.theory_of ctxt) (p, t) then SOME x else NONE)
+ (Net.match_term net t);
+
+fun insert_rules eq (t, x) = Net.insert_term eq (t, (t, x));
+
+fun norm thm = thm COMP_INCR asm_rl;
-method_setup comm_ring = \<open>
- Scan.succeed (SIMPLE_METHOD' o Commutative_Ring_Tac.tac)
-\<close> "reflective decision procedure for equalities over commutative rings"
+fun get_ring_simps ctxt optcT t =
+ (case get_matching_rules ctxt (Ring_Simps.get (Context.Proof ctxt)) t of
+ SOME (ths1, ths2, ths3, ths4, th5, th) =>
+ let val tr =
+ Thm.transfer (Proof_Context.theory_of ctxt) #>
+ (case optcT of NONE => I | SOME cT => inst [cT] [] #> norm)
+ in (map tr ths1, map tr ths2, map tr ths3, map tr ths4, tr th5, tr th) end
+ | NONE => error "get_ring_simps: lookup failed");
+
+fun ring_struct (Const (@{const_name Ring.ring.add}, _) $ R $ _ $ _) = SOME R
+ | ring_struct (Const (@{const_name Ring.a_minus}, _) $ R $ _ $ _) = SOME R
+ | ring_struct (Const (@{const_name Group.monoid.mult}, _) $ R $ _ $ _) = SOME R
+ | ring_struct (Const (@{const_name Ring.a_inv}, _) $ R $ _) = SOME R
+ | ring_struct (Const (@{const_name Group.pow}, _) $ R $ _ $ _) = SOME R
+ | ring_struct (Const (@{const_name Ring.ring.zero}, _) $ R) = SOME R
+ | ring_struct (Const (@{const_name Group.monoid.one}, _) $ R) = SOME R
+ | ring_struct (Const (@{const_name Algebra_Aux.of_integer}, _) $ R $ _) = SOME R
+ | ring_struct _ = NONE;
+
+fun reif_polex vs (Const (@{const_name Ring.ring.add}, _) $ _ $ a $ b) =
+ @{const Add} $ reif_polex vs a $ reif_polex vs b
+ | reif_polex vs (Const (@{const_name Ring.a_minus}, _) $ _ $ a $ b) =
+ @{const Sub} $ reif_polex vs a $ reif_polex vs b
+ | reif_polex vs (Const (@{const_name Group.monoid.mult}, _) $ _ $ a $ b) =
+ @{const Mul} $ reif_polex vs a $ reif_polex vs b
+ | reif_polex vs (Const (@{const_name Ring.a_inv}, _) $ _ $ a) =
+ @{const Neg} $ reif_polex vs a
+ | reif_polex vs (Const (@{const_name Group.pow}, _) $ _ $ a $ n) =
+ @{const Pow} $ reif_polex vs a $ n
+ | reif_polex vs (Free x) =
+ @{const Var} $ HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)
+ | reif_polex vs (Const (@{const_name Ring.ring.zero}, _) $ _) =
+ @{term "Const 0"}
+ | reif_polex vs (Const (@{const_name Group.monoid.one}, _) $ _) =
+ @{term "Const 1"}
+ | reif_polex vs (Const (@{const_name Algebra_Aux.of_integer}, _) $ _ $ n) =
+ @{const Const} $ n
+ | reif_polex _ _ = error "reif_polex: bad expression";
+
+fun reif_polex' vs (Const (@{const_name Groups.plus}, _) $ a $ b) =
+ @{const Add} $ reif_polex' vs a $ reif_polex' vs b
+ | reif_polex' vs (Const (@{const_name Groups.minus}, _) $ a $ b) =
+ @{const Sub} $ reif_polex' vs a $ reif_polex' vs b
+ | reif_polex' vs (Const (@{const_name Groups.times}, _) $ a $ b) =
+ @{const Mul} $ reif_polex' vs a $ reif_polex' vs b
+ | reif_polex' vs (Const (@{const_name Groups.uminus}, _) $ a) =
+ @{const Neg} $ reif_polex' vs a
+ | reif_polex' vs (Const (@{const_name Power.power}, _) $ a $ n) =
+ @{const Pow} $ reif_polex' vs a $ n
+ | reif_polex' vs (Free x) =
+ @{const Var} $ HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)
+ | reif_polex' vs (Const (@{const_name numeral}, _) $ b) =
+ @{const Const} $ (@{const numeral (int)} $ b)
+ | reif_polex' vs (Const (@{const_name zero_class.zero}, _)) = @{term "Const 0"}
+ | reif_polex' vs (Const (@{const_name one_class.one}, _)) = @{term "Const 1"}
+ | reif_polex' vs t = error "reif_polex: bad expression";
+
+fun head_conv (_, _, _, _, head_simp, _) ys =
+ (case strip_app ys of
+ (@{const_name Cons}, [y, xs]) => inst [] [y, xs] head_simp);
+
+fun Ipol_conv (rls as
+ ([Ipol_simps_1, Ipol_simps_2, Ipol_simps_3,
+ Ipol_simps_4, Ipol_simps_5, Ipol_simps_6,
+ Ipol_simps_7], _, _, _, _, _)) =
+ let
+ val a = type_of_eqn Ipol_simps_1;
+ val drop_conv_a = drop_conv a;
+
+ fun conv l p = (case strip_app p of
+ (@{const_name Pc}, [c]) => (case strip_numeral c of
+ (@{const_name zero_class.zero}, _) => inst [] [l] Ipol_simps_4
+ | (@{const_name one_class.one}, _) => inst [] [l] Ipol_simps_5
+ | (@{const_name numeral}, [m]) => inst [] [l, m] Ipol_simps_6
+ | (@{const_name uminus}, [m]) => inst [] [l, m] Ipol_simps_7
+ | _ => inst [] [l, c] Ipol_simps_1)
+ | (@{const_name Pinj}, [i, P]) =>
+ transitive'
+ (inst [] [l, i, P] Ipol_simps_2)
+ (cong2' conv (args2 drop_conv_a) Thm.reflexive)
+ | (@{const_name PX}, [P, x, Q]) =>
+ transitive'
+ (inst [] [l, P, x, Q] Ipol_simps_3)
+ (cong2
+ (cong2
+ (args2 conv) (cong2 (args1 (head_conv rls)) Thm.reflexive))
+ (cong2' conv (args2 drop_conv_a) Thm.reflexive)))
+ in conv end;
+
+fun Ipolex_conv (rls as
+ (_,
+ [Ipolex_Var, Ipolex_Const, Ipolex_Add,
+ Ipolex_Sub, Ipolex_Mul, Ipolex_Pow,
+ Ipolex_Neg, Ipolex_Const_0, Ipolex_Const_1,
+ Ipolex_Const_numeral], _, _, _, _)) =
+ let
+ val a = type_of_eqn Ipolex_Var;
+ val drop_conv_a = drop_conv a;
+
+ fun conv l r = (case strip_app r of
+ (@{const_name Var}, [n]) =>
+ transitive'
+ (inst [] [l, n] Ipolex_Var)
+ (cong1' (head_conv rls) (args2 drop_conv_a))
+ | (@{const_name Const}, [i]) => (case strip_app i of
+ (@{const_name zero_class.zero}, _) => inst [] [l] Ipolex_Const_0
+ | (@{const_name one_class.one}, _) => inst [] [l] Ipolex_Const_1
+ | (@{const_name numeral}, [m]) => inst [] [l, m] Ipolex_Const_numeral
+ | _ => inst [] [l, i] Ipolex_Const)
+ | (@{const_name Add}, [P, Q]) =>
+ transitive'
+ (inst [] [l, P, Q] Ipolex_Add)
+ (cong2 (args2 conv) (args2 conv))
+ | (@{const_name Sub}, [P, Q]) =>
+ transitive'
+ (inst [] [l, P, Q] Ipolex_Sub)
+ (cong2 (args2 conv) (args2 conv))
+ | (@{const_name Mul}, [P, Q]) =>
+ transitive'
+ (inst [] [l, P, Q] Ipolex_Mul)
+ (cong2 (args2 conv) (args2 conv))
+ | (@{const_name Pow}, [P, n]) =>
+ transitive'
+ (inst [] [l, P, n] Ipolex_Pow)
+ (cong2 (args2 conv) Thm.reflexive)
+ | (@{const_name Neg}, [P]) =>
+ transitive'
+ (inst [] [l, P] Ipolex_Neg)
+ (cong1 (args2 conv)))
+ in conv end;
+
+fun Ipolex_polex_list_conv (rls as
+ (_, _,
+ [Ipolex_polex_list_Nil, Ipolex_polex_list_Cons], _, _, _)) l pps =
+ (case strip_app pps of
+ (@{const_name Nil}, []) => inst [] [l] Ipolex_polex_list_Nil
+ | (@{const_name Cons}, [p, pps']) => (case strip_app p of
+ (@{const_name Pair}, [P, Q]) =>
+ transitive'
+ (inst [] [l, P, Q, pps'] Ipolex_polex_list_Cons)
+ (cong2
+ (cong2 (args2 (Ipolex_conv rls)) (args2 (Ipolex_conv rls)))
+ (args2 (Ipolex_polex_list_conv rls)))));
+
+fun dest_conj th =
+ let
+ val th1 = th RS @{thm conjunct1};
+ val th2 = th RS @{thm conjunct2}
+ in
+ dest_conj th1 @ dest_conj th2
+ end handle THM _ => [th];
+
+fun mk_in_carrier ctxt R prems xs =
+ let
+ val (_, _, _, [in_carrier_Nil, in_carrier_Cons], _, _) =
+ get_ring_simps ctxt NONE R;
+ val props = map fst (Facts.props (Proof_Context.facts_of ctxt)) @ maps dest_conj prems;
+ val ths = map (fn p as (x, _) =>
+ (case find_first
+ ((fn Const (@{const_name Trueprop}, _) $
+ (Const (@{const_name Set.member}, _) $
+ Free (y, _) $ (Const (@{const_name carrier}, _) $ S)) =>
+ x = y andalso R aconv S
+ | _ => false) o Thm.prop_of) props of
+ SOME th => th
+ | NONE => error ("Variable " ^ Syntax.string_of_term ctxt (Free p) ^
+ " not in carrier"))) xs
+ in
+ fold_rev (fn th1 => fn th2 => [th1, th2] MRS in_carrier_Cons)
+ ths in_carrier_Nil
+ end;
+
+fun mk_ring T =
+ Const (@{const_name cring_class_ops},
+ Type (@{type_name partial_object_ext}, [T,
+ Type (@{type_name monoid_ext}, [T,
+ Type (@{type_name ring_ext}, [T, @{typ unit}])])]));
+
+val iterations = @{cterm "1000::nat"};
+val Trueprop_cong = Thm.combination (Thm.reflexive @{cterm Trueprop});
+
+val cv = Code_Evaluation.static_conv
+ {ctxt = @{context},
+ consts =
+ [@{const_name pnsubstl},
+ @{const_name norm},
+ @{const_name mk_monpol_list},
+ @{const_name ring_codegen_aux}]};
+
+fun commutative_ring_conv ctxt prems eqs ct =
+ let
+ val cT = Thm.ctyp_of_cterm ct;
+ val T = Thm.typ_of cT;
+ val eqs' = map (HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) eqs;
+ val xs = filter (equal T o snd) (rev (fold Term.add_frees
+ (map fst eqs' @ map snd eqs' @ [Thm.term_of ct]) []));
+ val (R, optcT, prem', reif) = (case ring_struct (Thm.term_of ct) of
+ SOME R => (R, NONE, mk_in_carrier ctxt R prems xs, reif_polex xs)
+ | NONE => (mk_ring T, SOME cT, @{thm in_carrier_trivial}, reif_polex' xs));
+ val rls as (_, _, _, _, _, norm_subst_correct) = get_ring_simps ctxt optcT R;
+ val cxs = Thm.cterm_of ctxt (HOLogic.mk_list T (map Free xs));
+ val ceqs = Thm.cterm_of ctxt (HOLogic.mk_list @{typ "polex * polex"}
+ (map (HOLogic.mk_prod o apply2 reif) eqs'));
+ val cp = Thm.cterm_of ctxt (reif (Thm.term_of ct));
+ val prem = Thm.equal_elim
+ (Trueprop_cong (Thm.symmetric (Ipolex_polex_list_conv rls cxs ceqs)))
+ (fold_rev (fn th1 => fn th2 => [th1, th2] MRS @{thm conjI})
+ eqs @{thm TrueI});
+ in
+ Thm.transitive
+ (Thm.symmetric (Ipolex_conv rls cxs cp))
+ (transitive'
+ ([prem', prem] MRS inst [] [cxs, ceqs, cp, iterations, iterations]
+ norm_subst_correct)
+ (cong2' (Ipol_conv rls)
+ Thm.reflexive
+ (cv ctxt)))
+ end;
+
+fun ring_tac in_prems thms ctxt =
+ tactic_of_conv (fn ct =>
+ (if in_prems then Conv.prems_conv else Conv.concl_conv)
+ (Logic.count_prems (Thm.term_of ct))
+ (Conv.arg_conv (Conv.binop_conv (commutative_ring_conv ctxt [] thms))) ct) THEN'
+ TRY o (assume_tac ctxt ORELSE' resolve_tac ctxt [@{thm refl}]);
end
+\<close>
+
+context cring begin
+
+local_setup \<open>
+Local_Theory.declaration {syntax = false, pervasive = false}
+ (fn phi => Ring_Tac.Ring_Simps.map (Ring_Tac.insert_rules Ring_Tac.eq_ring_simps
+ (Morphism.term phi @{term R},
+ (Morphism.fact phi @{thms Ipol.simps [meta] Ipol_Pc [meta]},
+ Morphism.fact phi @{thms Ipolex.simps [meta] Ipolex_Const [meta]},
+ Morphism.fact phi @{thms Ipolex_polex_list.simps [meta]},
+ Morphism.fact phi @{thms in_carrier_Nil in_carrier_Cons},
+ singleton (Morphism.fact phi) @{thm head.simps(2) [meta]},
+ singleton (Morphism.fact phi) @{thm norm_subst_correct [meta]}))))
+\<close>
+
+end
+
+method_setup ring = \<open>
+ Scan.lift (Args.mode "prems") -- Attrib.thms >> (SIMPLE_METHOD' oo uncurry Ring_Tac.ring_tac)
+\<close> "simplify equations involving rings"
+
+end
--- a/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy Sun Jan 29 11:49:48 2017 +0100
+++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy Sun Jan 29 11:59:48 2017 +0100
@@ -1,8 +1,8 @@
(* Author: Bernhard Haeupler
-This theory is about of the relative completeness of method comm-ring
-method. As long as the reified atomic polynomials of type 'a pol are
-in normal form, the cring method is complete.
+This theory is about of the relative completeness of the ring
+method. As long as the reified atomic polynomials of type pol are
+in normal form, the ring method is complete.
*)
section \<open>Proof of the relative completeness of method comm-ring\<close>
@@ -12,7 +12,7 @@
begin
text \<open>Formalization of normal form\<close>
-fun isnorm :: "'a::comm_ring pol \<Rightarrow> bool"
+fun isnorm :: "pol \<Rightarrow> bool"
where
"isnorm (Pc c) \<longleftrightarrow> True"
| "isnorm (Pinj i (Pc c)) \<longleftrightarrow> False"
@@ -130,7 +130,7 @@
qed
text \<open>add conserves normalizedness\<close>
-lemma add_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<oplus> Q)"
+lemma add_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<langle>+\<rangle> Q)"
proof (induct P Q rule: add.induct)
case 1
then show ?case by simp
@@ -219,7 +219,7 @@
case x: 2
from 7 have "isnorm R" "isnorm P2"
by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
- with 7 x have "isnorm (R \<oplus> P2)"
+ with 7 x have "isnorm (R \<langle>+\<rangle> P2)"
by simp
with 7 x show ?thesis
by (simp add: norm_PXtrans[of Q2 y _])
@@ -229,7 +229,7 @@
by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
with 7 x have "isnorm (Pinj (x - 1) P2)"
by (cases P2) auto
- with 7 x NR have "isnorm (R \<oplus> Pinj (x - 1) P2)"
+ with 7 x NR have "isnorm (R \<langle>+\<rangle> Pinj (x - 1) P2)"
by simp
with \<open>isnorm (PX Q2 y R)\<close> x show ?thesis
by (simp add: norm_PXtrans[of Q2 y _])
@@ -247,7 +247,7 @@
case x: 2
with 8 have "isnorm R" "isnorm P2"
by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
- with 8 x have "isnorm (R \<oplus> P2)"
+ with 8 x have "isnorm (R \<langle>+\<rangle> P2)"
by simp
with 8 x show ?thesis
by (simp add: norm_PXtrans[of Q2 y _])
@@ -258,7 +258,7 @@
by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
with 8 x have "isnorm (Pinj (x - 1) P2)"
by (cases P2) auto
- with 8 x NR have "isnorm (R \<oplus> Pinj (x - 1) P2)"
+ with 8 x NR have "isnorm (R \<langle>+\<rangle> Pinj (x - 1) P2)"
by simp
with \<open>isnorm (PX Q2 y R)\<close> x show ?thesis
by (simp add: norm_PXtrans[of Q2 y _])
@@ -291,13 +291,13 @@
with 9 xy x show ?thesis
by (cases d) auto
qed
- with 9 NQ1 NP1 NP2 NQ2 xy x have "isnorm (P2 \<oplus> Q2)" "isnorm (PX P1 (x - y) (Pc 0) \<oplus> Q1)"
+ with 9 NQ1 NP1 NP2 NQ2 xy x have "isnorm (P2 \<langle>+\<rangle> Q2)" "isnorm (PX P1 (x - y) (Pc 0) \<langle>+\<rangle> Q1)"
by auto
with Y0 xy x show ?thesis
by (simp add: mkPX_cn)
next
case xy: 2
- with 9 NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<oplus> Q2)" "isnorm (P1 \<oplus> Q1)"
+ with 9 NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<langle>+\<rangle> Q2)" "isnorm (P1 \<langle>+\<rangle> Q1)"
by auto
with xy Y0 show ?thesis
by (simp add: mkPX_cn)
@@ -319,7 +319,7 @@
with 9 xy y show ?thesis
by (cases d) auto
qed
- with 9 NQ1 NP1 NP2 NQ2 xy y have "isnorm (P2 \<oplus> Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \<oplus> P1)"
+ with 9 NQ1 NP1 NP2 NQ2 xy y have "isnorm (P2 \<langle>+\<rangle> Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \<langle>+\<rangle> P1)"
by auto
with X0 xy y show ?thesis
by (simp add: mkPX_cn)
@@ -327,7 +327,7 @@
qed
text \<open>mul concerves normalizedness\<close>
-lemma mul_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<otimes> Q)"
+lemma mul_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<langle>*\<rangle> Q)"
proof (induct P Q rule: mul.induct)
case 1
then show ?case by simp
@@ -426,7 +426,7 @@
case x: 2
from 7 have "isnorm R" "isnorm P2"
by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
- with 7 x have "isnorm (R \<otimes> P2)" "isnorm Q2"
+ with 7 x have "isnorm (R \<langle>*\<rangle> P2)" "isnorm Q2"
by (auto simp add: norm_PX1[of Q2 y R])
with 7 x Y0 show ?thesis
by (simp add: mkPX_cn)
@@ -436,7 +436,7 @@
by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
from 7 x have "isnorm (Pinj (x - 1) P2)"
by (cases P2) auto
- with 7 x * have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)"
+ with 7 x * have "isnorm (R \<langle>*\<rangle> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<langle>*\<rangle> Q2)"
by auto
with Y0 x show ?thesis
by (simp add: mkPX_cn)
@@ -456,7 +456,7 @@
case x: 2
from 8 have "isnorm R" "isnorm P2"
by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
- with 8 x have "isnorm (R \<otimes> P2)" "isnorm Q2"
+ with 8 x have "isnorm (R \<langle>*\<rangle> P2)" "isnorm Q2"
by (auto simp add: norm_PX1[of Q2 y R])
with 8 x Y0 show ?thesis
by (simp add: mkPX_cn)
@@ -466,7 +466,7 @@
by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
from 8 x have "isnorm (Pinj (x - 1) P2)"
by (cases P2) auto
- with 8 x * have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)"
+ with 8 x * have "isnorm (R \<langle>*\<rangle> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<langle>*\<rangle> Q2)"
by auto
with Y0 x show ?thesis
by (simp add: mkPX_cn)
@@ -479,13 +479,13 @@
by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
from 9 have "isnorm Q1" "isnorm Q2"
by (auto simp add: norm_PX1[of Q1 y Q2] norm_PX2[of Q1 y Q2])
- with 9 * have "isnorm (P1 \<otimes> Q1)" "isnorm (P2 \<otimes> Q2)"
- "isnorm (P1 \<otimes> mkPinj 1 Q2)" "isnorm (Q1 \<otimes> mkPinj 1 P2)"
+ with 9 * have "isnorm (P1 \<langle>*\<rangle> Q1)" "isnorm (P2 \<langle>*\<rangle> Q2)"
+ "isnorm (P1 \<langle>*\<rangle> mkPinj 1 Q2)" "isnorm (Q1 \<langle>*\<rangle> mkPinj 1 P2)"
by (auto simp add: mkPinj_cn)
with 9 X0 Y0 have
- "isnorm (mkPX (P1 \<otimes> Q1) (x + y) (P2 \<otimes> Q2))"
- "isnorm (mkPX (P1 \<otimes> mkPinj (Suc 0) Q2) x (Pc 0))"
- "isnorm (mkPX (Q1 \<otimes> mkPinj (Suc 0) P2) y (Pc 0))"
+ "isnorm (mkPX (P1 \<langle>*\<rangle> Q1) (x + y) (P2 \<langle>*\<rangle> Q2))"
+ "isnorm (mkPX (P1 \<langle>*\<rangle> mkPinj (Suc 0) Q2) x (Pc 0))"
+ "isnorm (mkPX (Q1 \<langle>*\<rangle> mkPinj (Suc 0) P2) y (Pc 0))"
by (auto simp add: mkPX_cn)
then show ?case
by (simp add: add_cn)
@@ -519,7 +519,7 @@
qed
text \<open>sub conserves normalizedness\<close>
-lemma sub_cn: "isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)"
+lemma sub_cn: "isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<langle>-\<rangle> q)"
by (simp add: sub_def add_cn neg_cn)
text \<open>sqr conserves normalizizedness\<close>
@@ -542,7 +542,7 @@
using PX
apply (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
done
- with PX have "isnorm (mkPX (Pc (1 + 1) \<otimes> P1 \<otimes> mkPinj (Suc 0) P2) x (Pc 0))"
+ with PX have "isnorm (mkPX (Pc (1 + 1) \<langle>*\<rangle> P1 \<langle>*\<rangle> mkPinj (Suc 0) P2) x (Pc 0))"
and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))"
by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
then show ?case
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Decision_Procs/Conversions.thy Sun Jan 29 11:59:48 2017 +0100
@@ -0,0 +1,844 @@
+(* Title: HOL/Decision_Procs/Conversions.thy
+ Author: Stefan Berghofer
+*)
+
+theory Conversions
+imports Main
+begin
+
+ML {*
+fun tactic_of_conv cv i st =
+ if i > Thm.nprems_of st then Seq.empty
+ else Seq.single (Conv.gconv_rule cv i st);
+
+fun binop_conv cv cv' = Conv.combination_conv (Conv.arg_conv cv) cv';
+*}
+
+ML {*
+fun err s ct =
+ error (s ^ ": " ^ Syntax.string_of_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct));
+*}
+
+attribute_setup meta =
+ {* Scan.succeed (fn (ctxt, th) => (NONE, SOME (mk_meta_eq th))) *}
+ {* convert equality to meta equality *}
+
+ML {*
+fun mk_obj_eq th = th RS @{thm meta_eq_to_obj_eq};
+
+fun strip_app ct = ct |> Drule.strip_comb |>> Thm.term_of |>> dest_Const |>> fst;
+
+fun inst cTs cts th =
+ Thm.instantiate' (map SOME cTs) (map SOME cts) th;
+
+fun transitive' eq eq' = Thm.transitive eq (eq' (Thm.rhs_of eq));
+
+fun type_of_eqn eqn = Thm.ctyp_of_cterm (Thm.dest_arg1 (Thm.cprop_of eqn));
+
+fun cong1 conv ct =
+ Thm.combination (Thm.reflexive (Thm.dest_fun ct)) (conv (Thm.dest_arg ct));
+
+fun cong1' conv' conv ct =
+ let val eqn = conv (Thm.dest_arg ct)
+ in
+ Thm.transitive
+ (Thm.combination (Thm.reflexive (Thm.dest_fun ct)) eqn)
+ (conv' (Thm.rhs_of eqn))
+ end;
+
+fun cong2 conv1 conv2 ct =
+ Thm.combination
+ (Thm.combination
+ (Thm.reflexive (Thm.dest_fun2 ct))
+ (conv1 (Thm.dest_arg1 ct)))
+ (conv2 (Thm.dest_arg ct));
+
+fun cong2' conv conv1 conv2 ct =
+ let
+ val eqn1 = conv1 (Thm.dest_arg1 ct);
+ val eqn2 = conv2 (Thm.dest_arg ct)
+ in
+ Thm.transitive
+ (Thm.combination
+ (Thm.combination (Thm.reflexive (Thm.dest_fun2 ct)) eqn1)
+ eqn2)
+ (conv (Thm.rhs_of eqn1) (Thm.rhs_of eqn2))
+ end;
+
+fun cong2'' conv eqn1 eqn2 =
+ let val eqn3 = conv (Thm.rhs_of eqn1) (Thm.rhs_of eqn2)
+ in
+ Thm.transitive
+ (Thm.combination
+ (Thm.combination (Thm.reflexive (Thm.dest_fun2 (Thm.lhs_of eqn3))) eqn1)
+ eqn2)
+ eqn3
+ end;
+
+fun args1 conv ct = conv (Thm.dest_arg ct);
+fun args2 conv ct = conv (Thm.dest_arg1 ct) (Thm.dest_arg ct);
+*}
+
+ML {*
+fun strip_numeral ct = (case strip_app ct of
+ (@{const_name uminus}, [n]) => (case strip_app n of
+ (@{const_name numeral}, [b]) => (@{const_name uminus}, [b])
+ | _ => ("", []))
+ | x => x);
+*}
+
+lemma nat_minus1_eq: "nat (- 1) = 0"
+ by simp
+
+ML {*
+fun nat_conv i = (case strip_app i of
+ (@{const_name zero_class.zero}, []) => @{thm nat_0 [meta]}
+ | (@{const_name one_class.one}, []) => @{thm transfer_nat_int_numerals(2) [meta, symmetric]}
+ | (@{const_name numeral}, [b]) => inst [] [b] @{thm nat_numeral [meta]}
+ | (@{const_name uminus}, [b]) => (case strip_app b of
+ (@{const_name one_class.one}, []) => @{thm nat_minus1_eq [meta]}
+ | (@{const_name numeral}, [b']) => inst [] [b'] @{thm nat_neg_numeral [meta]}));
+*}
+
+ML {*
+fun add_num_conv b b' = (case (strip_app b, strip_app b') of
+ ((@{const_name Num.One}, []), (@{const_name Num.One}, [])) =>
+ @{thm add_num_simps(1) [meta]}
+ | ((@{const_name Num.One}, []), (@{const_name Num.Bit0}, [n])) =>
+ inst [] [n] @{thm add_num_simps(2) [meta]}
+ | ((@{const_name Num.One}, []), (@{const_name Num.Bit1}, [n])) =>
+ transitive'
+ (inst [] [n] @{thm add_num_simps(3) [meta]})
+ (cong1 (args2 add_num_conv))
+ | ((@{const_name Num.Bit0}, [m]), (@{const_name Num.One}, [])) =>
+ inst [] [m] @{thm add_num_simps(4) [meta]}
+ | ((@{const_name Num.Bit0}, [m]), (@{const_name Num.Bit0}, [n])) =>
+ transitive'
+ (inst [] [m, n] @{thm add_num_simps(5) [meta]})
+ (cong1 (args2 add_num_conv))
+ | ((@{const_name Num.Bit0}, [m]), (@{const_name Num.Bit1}, [n])) =>
+ transitive'
+ (inst [] [m, n] @{thm add_num_simps(6) [meta]})
+ (cong1 (args2 add_num_conv))
+ | ((@{const_name Num.Bit1}, [m]), (@{const_name Num.One}, [])) =>
+ transitive'
+ (inst [] [m] @{thm add_num_simps(7) [meta]})
+ (cong1 (args2 add_num_conv))
+ | ((@{const_name Num.Bit1}, [m]), (@{const_name Num.Bit0}, [n])) =>
+ transitive'
+ (inst [] [m, n] @{thm add_num_simps(8) [meta]})
+ (cong1 (args2 add_num_conv))
+ | ((@{const_name Num.Bit1}, [m]), (@{const_name Num.Bit1}, [n])) =>
+ transitive'
+ (inst [] [m, n] @{thm add_num_simps(9) [meta]})
+ (cong1 (cong2' add_num_conv (args2 add_num_conv) Thm.reflexive)));
+*}
+
+ML {*
+fun BitM_conv m = (case strip_app m of
+ (@{const_name Num.One}, []) => @{thm BitM.simps(1) [meta]}
+ | (@{const_name Num.Bit0}, [n]) =>
+ transitive'
+ (inst [] [n] @{thm BitM.simps(2) [meta]})
+ (cong1 (args1 BitM_conv))
+ | (@{const_name Num.Bit1}, [n]) =>
+ inst [] [n] @{thm BitM.simps(3) [meta]});
+*}
+
+lemma dbl_neg_numeral:
+ "Num.dbl (- Num.numeral k) = - Num.numeral (Num.Bit0 k)"
+ by simp
+
+ML {*
+fun dbl_conv a =
+ let
+ val dbl_neg_numeral_a = inst [a] [] @{thm dbl_neg_numeral [meta]};
+ val dbl_0_a = inst [a] [] @{thm dbl_simps(2) [meta]};
+ val dbl_numeral_a = inst [a] [] @{thm dbl_simps(5) [meta]}
+ in
+ fn n =>
+ case strip_numeral n of
+ (@{const_name zero_class.zero}, []) => dbl_0_a
+ | (@{const_name numeral}, [k]) => inst [] [k] dbl_numeral_a
+ | (@{const_name uminus}, [k]) => inst [] [k] dbl_neg_numeral_a
+ end;
+*}
+
+lemma dbl_inc_neg_numeral:
+ "Num.dbl_inc (- Num.numeral k) = - Num.numeral (Num.BitM k)"
+ by simp
+
+ML {*
+fun dbl_inc_conv a =
+ let
+ val dbl_inc_neg_numeral_a = inst [a] [] @{thm dbl_inc_neg_numeral [meta]};
+ val dbl_inc_0_a = inst [a] [] @{thm dbl_inc_simps(2) [folded numeral_One, meta]};
+ val dbl_inc_numeral_a = inst [a] [] @{thm dbl_inc_simps(5) [meta]};
+ in
+ fn n =>
+ case strip_numeral n of
+ (@{const_name zero_class.zero}, []) => dbl_inc_0_a
+ | (@{const_name numeral}, [k]) => inst [] [k] dbl_inc_numeral_a
+ | (@{const_name uminus}, [k]) =>
+ transitive'
+ (inst [] [k] dbl_inc_neg_numeral_a)
+ (cong1 (cong1 (args1 BitM_conv)))
+ end;
+*}
+
+lemma dbl_dec_neg_numeral:
+ "Num.dbl_dec (- Num.numeral k) = - Num.numeral (Num.Bit1 k)"
+ by simp
+
+ML {*
+fun dbl_dec_conv a =
+ let
+ val dbl_dec_neg_numeral_a = inst [a] [] @{thm dbl_dec_neg_numeral [meta]};
+ val dbl_dec_0_a = inst [a] [] @{thm dbl_dec_simps(2) [folded numeral_One, meta]};
+ val dbl_dec_numeral_a = inst [a] [] @{thm dbl_dec_simps(5) [meta]};
+ in
+ fn n =>
+ case strip_numeral n of
+ (@{const_name zero_class.zero}, []) => dbl_dec_0_a
+ | (@{const_name uminus}, [k]) => inst [] [k] dbl_dec_neg_numeral_a
+ | (@{const_name numeral}, [k]) =>
+ transitive'
+ (inst [] [k] dbl_dec_numeral_a)
+ (cong1 (args1 BitM_conv))
+ end;
+*}
+
+ML {*
+fun sub_conv a =
+ let
+ val [sub_One_One, sub_One_Bit0, sub_One_Bit1,
+ sub_Bit0_One, sub_Bit1_One, sub_Bit0_Bit0,
+ sub_Bit0_Bit1, sub_Bit1_Bit0, sub_Bit1_Bit1] =
+ map (inst [a] []) @{thms sub_num_simps [meta]};
+ val dbl_conv_a = dbl_conv a;
+ val dbl_inc_conv_a = dbl_inc_conv a;
+ val dbl_dec_conv_a = dbl_dec_conv a;
+
+ fun conv m n = (case (strip_app m, strip_app n) of
+ ((@{const_name Num.One}, []), (@{const_name Num.One}, [])) =>
+ sub_One_One
+ | ((@{const_name Num.One}, []), (@{const_name Num.Bit0}, [l])) =>
+ transitive'
+ (inst [] [l] sub_One_Bit0)
+ (cong1 (cong1 (args1 BitM_conv)))
+ | ((@{const_name Num.One}, []), (@{const_name Num.Bit1}, [l])) =>
+ inst [] [l] sub_One_Bit1
+ | ((@{const_name Num.Bit0}, [k]), (@{const_name Num.One}, [])) =>
+ transitive'
+ (inst [] [k] sub_Bit0_One)
+ (cong1 (args1 BitM_conv))
+ | ((@{const_name Num.Bit1}, [k]), (@{const_name Num.One}, [])) =>
+ inst [] [k] sub_Bit1_One
+ | ((@{const_name Num.Bit0}, [k]), (@{const_name Num.Bit0}, [l])) =>
+ transitive'
+ (inst [] [k, l] sub_Bit0_Bit0)
+ (cong1' dbl_conv_a (args2 conv))
+ | ((@{const_name Num.Bit0}, [k]), (@{const_name Num.Bit1}, [l])) =>
+ transitive'
+ (inst [] [k, l] sub_Bit0_Bit1)
+ (cong1' dbl_dec_conv_a (args2 conv))
+ | ((@{const_name Num.Bit1}, [k]), (@{const_name Num.Bit0}, [l])) =>
+ transitive'
+ (inst [] [k, l] sub_Bit1_Bit0)
+ (cong1' dbl_inc_conv_a (args2 conv))
+ | ((@{const_name Num.Bit1}, [k]), (@{const_name Num.Bit1}, [l])) =>
+ transitive'
+ (inst [] [k, l] sub_Bit1_Bit1)
+ (cong1' dbl_conv_a (args2 conv)))
+ in conv end;
+*}
+
+ML {*
+fun expand1 a =
+ let val numeral_1_eq_1_a = inst [a] [] @{thm numeral_One [meta, symmetric]}
+ in
+ fn n =>
+ case Thm.term_of n of
+ Const (@{const_name one_class.one}, _) => numeral_1_eq_1_a
+ | Const (@{const_name uminus}, _) $ Const (@{const_name one_class.one}, _) =>
+ Thm.combination (Thm.reflexive (Thm.dest_fun n)) numeral_1_eq_1_a
+ | Const (@{const_name zero_class.zero}, _) => Thm.reflexive n
+ | Const (@{const_name numeral}, _) $ _ => Thm.reflexive n
+ | Const (@{const_name uminus}, _) $
+ (Const (@{const_name numeral}, _) $ _) => Thm.reflexive n
+ | _ => err "expand1" n
+ end;
+
+fun norm1_eq a =
+ let val numeral_1_eq_1_a = inst [a] [] @{thm numeral_One [meta]}
+ in
+ fn eq =>
+ case Thm.term_of (Thm.rhs_of eq) of
+ Const (@{const_name Num.numeral}, _) $ Const (@{const_name Num.One}, _) =>
+ Thm.transitive eq numeral_1_eq_1_a
+ | Const (@{const_name uminus}, _) $
+ (Const (@{const_name Num.numeral}, _) $ Const (@{const_name Num.One}, _)) =>
+ Thm.transitive eq
+ (Thm.combination (Thm.reflexive (Thm.dest_fun (Thm.rhs_of eq)))
+ numeral_1_eq_1_a)
+ | _ => eq
+ end;
+*}
+
+ML {*
+fun plus_conv f a =
+ let
+ val add_0_a = inst [a] [] @{thm add_0 [meta]};
+ val add_0_right_a = inst [a] [] @{thm add_0_right [meta]};
+ val numeral_plus_numeral_a = inst [a] [] @{thm numeral_plus_numeral [meta]};
+ val expand1_a = expand1 a;
+
+ fun conv m n = (case (strip_app m, strip_app n) of
+ ((@{const_name zero_class.zero}, []), _) => inst [] [n] add_0_a
+ | (_, (@{const_name zero_class.zero}, [])) => inst [] [m] add_0_right_a
+ | ((@{const_name numeral}, [m]), (@{const_name numeral}, [n])) =>
+ transitive'
+ (inst [] [m, n] numeral_plus_numeral_a)
+ (cong1 (args2 add_num_conv))
+ | _ => cong2'' (f conv) (expand1_a m) (expand1_a n))
+ in f conv end;
+
+val nat_plus_conv = plus_conv I @{ctyp nat};
+*}
+
+lemma neg_numeral_plus_neg_numeral:
+ "- Num.numeral m + - Num.numeral n = (- Num.numeral (m + n) ::'a::neg_numeral)"
+ by simp
+
+ML {*
+fun plus_neg_conv a =
+ let
+ val numeral_plus_neg_numeral_a =
+ inst [a] [] @{thm add_neg_numeral_simps(1) [meta]};
+ val neg_numeral_plus_numeral_a =
+ inst [a] [] @{thm add_neg_numeral_simps(2) [meta]};
+ val neg_numeral_plus_neg_numeral_a =
+ inst [a] [] @{thm neg_numeral_plus_neg_numeral [meta]};
+ val sub_conv_a = sub_conv a;
+ in
+ fn conv => fn m => fn n =>
+ case (strip_numeral m, strip_numeral n) of
+ ((@{const_name Num.numeral}, [m]), (@{const_name uminus}, [n])) =>
+ Thm.transitive
+ (inst [] [m, n] numeral_plus_neg_numeral_a)
+ (sub_conv_a m n)
+ | ((@{const_name uminus}, [m]), (@{const_name Num.numeral}, [n])) =>
+ Thm.transitive
+ (inst [] [m, n] neg_numeral_plus_numeral_a)
+ (sub_conv_a n m)
+ | ((@{const_name uminus}, [m]), (@{const_name uminus}, [n])) =>
+ transitive'
+ (inst [] [m, n] neg_numeral_plus_neg_numeral_a)
+ (cong1 (cong1 (args2 add_num_conv)))
+ | _ => conv m n
+ end;
+
+fun plus_conv' a = norm1_eq a oo plus_conv (plus_neg_conv a) a;
+
+val int_plus_conv = plus_conv' @{ctyp int};
+*}
+
+lemma minus_one: "- 1 = - 1" by simp
+lemma minus_numeral: "- numeral b = - numeral b" by simp
+
+ML {*
+fun uminus_conv a =
+ let
+ val minus_zero_a = inst [a] [] @{thm minus_zero [meta]};
+ val minus_one_a = inst [a] [] @{thm minus_one [meta]};
+ val minus_numeral_a = inst [a] [] @{thm minus_numeral [meta]};
+ val minus_minus_a = inst [a] [] @{thm minus_minus [meta]}
+ in
+ fn n =>
+ case strip_app n of
+ (@{const_name zero_class.zero}, []) => minus_zero_a
+ | (@{const_name one_class.one}, []) => minus_one_a
+ | (@{const_name Num.numeral}, [m]) => inst [] [m] minus_numeral_a
+ | (@{const_name uminus}, [m]) => inst [] [m] minus_minus_a
+ end;
+
+val int_neg_conv = uminus_conv @{ctyp int};
+*}
+
+ML {*
+fun minus_conv a =
+ let
+ val [numeral_minus_numeral_a, numeral_minus_neg_numeral_a,
+ neg_numeral_minus_numeral_a, neg_numeral_minus_neg_numeral_a] =
+ map (inst [a] []) @{thms diff_numeral_simps [meta]};
+ val diff_0_a = inst [a] [] @{thm diff_0 [meta]};
+ val diff_0_right_a = inst [a] [] @{thm diff_0_right [meta]};
+ val sub_conv_a = sub_conv a;
+ val uminus_conv_a = uminus_conv a;
+ val expand1_a = expand1 a;
+ val norm1_eq_a = norm1_eq a;
+
+ fun conv m n = (case (strip_numeral m, strip_numeral n) of
+ ((@{const_name zero_class.zero}, []), _) =>
+ Thm.transitive (inst [] [n] diff_0_a) (uminus_conv_a n)
+ | (_, (@{const_name zero_class.zero}, [])) => inst [] [m] diff_0_right_a
+ | ((@{const_name Num.numeral}, [m]), (@{const_name Num.numeral}, [n])) =>
+ Thm.transitive
+ (inst [] [m, n] numeral_minus_numeral_a)
+ (sub_conv_a m n)
+ | ((@{const_name Num.numeral}, [m]), (@{const_name uminus}, [n])) =>
+ transitive'
+ (inst [] [m, n] numeral_minus_neg_numeral_a)
+ (cong1 (args2 add_num_conv))
+ | ((@{const_name uminus}, [m]), (@{const_name Num.numeral}, [n])) =>
+ transitive'
+ (inst [] [m, n] neg_numeral_minus_numeral_a)
+ (cong1 (cong1 (args2 add_num_conv)))
+ | ((@{const_name uminus}, [m]), (@{const_name uminus}, [n])) =>
+ Thm.transitive
+ (inst [] [m, n] neg_numeral_minus_neg_numeral_a)
+ (sub_conv_a n m)
+ | _ => cong2'' conv (expand1_a m) (expand1_a n))
+ in norm1_eq_a oo conv end;
+
+val int_minus_conv = minus_conv @{ctyp int};
+*}
+
+ML {*
+val int_numeral = Thm.apply @{cterm "numeral :: num \<Rightarrow> int"};
+
+val nat_minus_refl = Thm.reflexive @{cterm "minus :: nat \<Rightarrow> nat \<Rightarrow> nat"};
+
+val expand1_nat = expand1 @{ctyp nat};
+
+fun nat_minus_conv m n = (case (strip_app m, strip_app n) of
+ ((@{const_name zero_class.zero}, []), _) =>
+ inst [] [n] @{thm diff_0_eq_0 [meta]}
+ | (_, (@{const_name zero_class.zero}, [])) =>
+ inst [] [m] @{thm minus_nat.diff_0 [meta]}
+ | ((@{const_name numeral}, [m]), (@{const_name numeral}, [n])) =>
+ transitive'
+ (inst [] [m, n] @{thm diff_nat_numeral [meta]})
+ (cong1' nat_conv (args2 int_minus_conv))
+ | _ => cong2'' nat_minus_conv (expand1_nat m) (expand1_nat n));
+*}
+
+ML {*
+fun mult_num_conv m n = (case (strip_app m, strip_app n) of
+ (_, (@{const_name Num.One}, [])) =>
+ inst [] [m] @{thm mult_num_simps(1) [meta]}
+ | ((@{const_name Num.One}, []), _) =>
+ inst [] [n] @{thm mult_num_simps(2) [meta]}
+ | ((@{const_name Num.Bit0}, [m]), (@{const_name Num.Bit0}, [n])) =>
+ transitive'
+ (inst [] [m, n] @{thm mult_num_simps(3) [meta]})
+ (cong1 (cong1 (args2 mult_num_conv)))
+ | ((@{const_name Num.Bit0}, [m]), (@{const_name Num.Bit1}, [n'])) =>
+ transitive'
+ (inst [] [m, n'] @{thm mult_num_simps(4) [meta]})
+ (cong1 (args2 mult_num_conv))
+ | ((@{const_name Num.Bit1}, [m']), (@{const_name Num.Bit0}, [n])) =>
+ transitive'
+ (inst [] [m', n] @{thm mult_num_simps(5) [meta]})
+ (cong1 (args2 mult_num_conv))
+ | ((@{const_name Num.Bit1}, [m]), (@{const_name Num.Bit1}, [n])) =>
+ transitive'
+ (inst [] [m, n] @{thm mult_num_simps(6) [meta]})
+ (cong1 (cong2' add_num_conv
+ (args2 add_num_conv)
+ (cong1 (args2 mult_num_conv)))));
+*}
+
+ML {*
+fun mult_conv f a =
+ let
+ val mult_zero_left_a = inst [a] [] @{thm mult_zero_left [meta]};
+ val mult_zero_right_a = inst [a] [] @{thm mult_zero_right [meta]};
+ val numeral_times_numeral_a = inst [a] [] @{thm numeral_times_numeral [meta]};
+ val expand1_a = expand1 a;
+ val norm1_eq_a = norm1_eq a;
+
+ fun conv m n = (case (strip_app m, strip_app n) of
+ ((@{const_name zero_class.zero}, []), _) => inst [] [n] mult_zero_left_a
+ | (_, (@{const_name zero_class.zero}, [])) => inst [] [m] mult_zero_right_a
+ | ((@{const_name numeral}, [m]), (@{const_name numeral}, [n])) =>
+ transitive'
+ (inst [] [m, n] numeral_times_numeral_a)
+ (cong1 (args2 mult_num_conv))
+ | _ => cong2'' (f conv) (expand1_a m) (expand1_a n))
+ in norm1_eq_a oo f conv end;
+
+val nat_mult_conv = mult_conv I @{ctyp nat};
+*}
+
+ML {*
+fun mult_neg_conv a =
+ let
+ val [neg_numeral_times_neg_numeral_a, neg_numeral_times_numeral_a,
+ numeral_times_neg_numeral_a] =
+ map (inst [a] []) @{thms mult_neg_numeral_simps [meta]};
+ in
+ fn conv => fn m => fn n =>
+ case (strip_numeral m, strip_numeral n) of
+ ((@{const_name uminus}, [m]), (@{const_name uminus}, [n])) =>
+ transitive'
+ (inst [] [m, n] neg_numeral_times_neg_numeral_a)
+ (cong1 (args2 mult_num_conv))
+ | ((@{const_name uminus}, [m]), (@{const_name numeral}, [n])) =>
+ transitive'
+ (inst [] [m, n] neg_numeral_times_numeral_a)
+ (cong1 (cong1 (args2 mult_num_conv)))
+ | ((@{const_name numeral}, [m]), (@{const_name uminus}, [n])) =>
+ transitive'
+ (inst [] [m, n] numeral_times_neg_numeral_a)
+ (cong1 (cong1 (args2 mult_num_conv)))
+ | _ => conv m n
+ end;
+
+fun mult_conv' a = mult_conv (mult_neg_conv a) a;
+
+val int_mult_conv = mult_conv' @{ctyp int};
+*}
+
+ML {*
+fun eq_num_conv m n = (case (strip_app m, strip_app n) of
+ ((@{const_name Num.One}, []), (@{const_name Num.One}, [])) =>
+ @{thm eq_num_simps(1) [meta]}
+ | ((@{const_name Num.One}, []), (@{const_name Num.Bit0}, [n])) =>
+ inst [] [n] @{thm eq_num_simps(2) [meta]}
+ | ((@{const_name Num.One}, []), (@{const_name Num.Bit1}, [n])) =>
+ inst [] [n] @{thm eq_num_simps(3) [meta]}
+ | ((@{const_name Num.Bit0}, [m]), (@{const_name Num.One}, [])) =>
+ inst [] [m] @{thm eq_num_simps(4) [meta]}
+ | ((@{const_name Num.Bit1}, [m]), (@{const_name Num.One}, [])) =>
+ inst [] [m] @{thm eq_num_simps(5) [meta]}
+ | ((@{const_name Num.Bit0}, [m]), (@{const_name Num.Bit0}, [n])) =>
+ Thm.transitive
+ (inst [] [m, n] @{thm eq_num_simps(6) [meta]})
+ (eq_num_conv m n)
+ | ((@{const_name Num.Bit0}, [m]), (@{const_name Num.Bit1}, [n])) =>
+ inst [] [m, n] @{thm eq_num_simps(7) [meta]}
+ | ((@{const_name Num.Bit1}, [m]), (@{const_name Num.Bit0}, [n])) =>
+ inst [] [m, n] @{thm eq_num_simps(8) [meta]}
+ | ((@{const_name Num.Bit1}, [m]), (@{const_name Num.Bit1}, [n])) =>
+ Thm.transitive
+ (inst [] [m, n] @{thm eq_num_simps(9) [meta]})
+ (eq_num_conv m n));
+*}
+
+ML {*
+fun eq_conv f a =
+ let
+ val zero_eq_zero_a = inst [a] [] @{thm refl [of 0, THEN Eq_TrueI]};
+ val zero_neq_numeral_a =
+ inst [a] [] @{thm zero_neq_numeral [THEN Eq_FalseI]};
+ val numeral_neq_zero_a =
+ inst [a] [] @{thm numeral_neq_zero [THEN Eq_FalseI]};
+ val numeral_eq_iff_a = inst [a] [] @{thm numeral_eq_iff [meta]};
+ val expand1_a = expand1 a;
+
+ fun conv m n = (case (strip_app m, strip_app n) of
+ ((@{const_name zero_class.zero}, []), (@{const_name zero_class.zero}, [])) =>
+ zero_eq_zero_a
+ | ((@{const_name zero_class.zero}, []), (@{const_name numeral}, [n])) =>
+ inst [] [n] zero_neq_numeral_a
+ | ((@{const_name numeral}, [m]), (@{const_name zero_class.zero}, [])) =>
+ inst [] [m] numeral_neq_zero_a
+ | ((@{const_name numeral}, [m]), (@{const_name numeral}, [n])) =>
+ Thm.transitive
+ (inst [] [m, n] numeral_eq_iff_a)
+ (eq_num_conv m n)
+ | _ => cong2'' (f conv) (expand1_a m) (expand1_a n))
+ in f conv end;
+
+val nat_eq_conv = eq_conv I @{ctyp nat};
+*}
+
+ML {*
+fun eq_neg_conv a =
+ let
+ val neg_numeral_neq_zero_a =
+ inst [a] [] @{thm neg_numeral_neq_zero [THEN Eq_FalseI]};
+ val zero_neq_neg_numeral_a =
+ inst [a] [] @{thm zero_neq_neg_numeral [THEN Eq_FalseI]};
+ val neg_numeral_neq_numeral_a =
+ inst [a] [] @{thm neg_numeral_neq_numeral [THEN Eq_FalseI]};
+ val numeral_neq_neg_numeral_a =
+ inst [a] [] @{thm numeral_neq_neg_numeral [THEN Eq_FalseI]};
+ val neg_numeral_eq_iff_a = inst [a] [] @{thm neg_numeral_eq_iff [meta]}
+ in
+ fn conv => fn m => fn n =>
+ case (strip_numeral m, strip_numeral n) of
+ ((@{const_name uminus}, [m]), (@{const_name zero_class.zero}, [])) =>
+ inst [] [m] neg_numeral_neq_zero_a
+ | ((@{const_name zero_class.zero}, []), (@{const_name uminus}, [n])) =>
+ inst [] [n] zero_neq_neg_numeral_a
+ | ((@{const_name Num.numeral}, [m]), (@{const_name uminus}, [n])) =>
+ inst [] [m, n] numeral_neq_neg_numeral_a
+ | ((@{const_name uminus}, [m]), (@{const_name Num.numeral}, [n])) =>
+ inst [] [m, n] neg_numeral_neq_numeral_a
+ | ((@{const_name uminus}, [m]), (@{const_name uminus}, [n])) =>
+ Thm.transitive
+ (inst [] [m, n] neg_numeral_eq_iff_a)
+ (eq_num_conv m n)
+ | _ => conv m n
+ end;
+
+fun eq_conv' a = eq_conv (eq_neg_conv a) a;
+
+val int_eq_conv = eq_conv' @{ctyp int};
+*}
+
+ML {*
+fun le_num_conv m n = (case (strip_app m, strip_app n) of
+ ((@{const_name Num.One}, []), _) =>
+ inst [] [n] @{thm le_num_simps(1) [meta]}
+ | ((@{const_name Num.Bit0}, [m]), (@{const_name Num.One}, [])) =>
+ inst [] [m] @{thm le_num_simps(2) [meta]}
+ | ((@{const_name Num.Bit1}, [m]), (@{const_name Num.One}, [])) =>
+ inst [] [m] @{thm le_num_simps(3) [meta]}
+ | ((@{const_name Num.Bit0}, [m]), (@{const_name Num.Bit0}, [n])) =>
+ Thm.transitive
+ (inst [] [m, n] @{thm le_num_simps(4) [meta]})
+ (le_num_conv m n)
+ | ((@{const_name Num.Bit0}, [m]), (@{const_name Num.Bit1}, [n])) =>
+ Thm.transitive
+ (inst [] [m, n] @{thm le_num_simps(5) [meta]})
+ (le_num_conv m n)
+ | ((@{const_name Num.Bit1}, [m]), (@{const_name Num.Bit1}, [n])) =>
+ Thm.transitive
+ (inst [] [m, n] @{thm le_num_simps(6) [meta]})
+ (le_num_conv m n)
+ | ((@{const_name Num.Bit1}, [m]), (@{const_name Num.Bit0}, [n])) =>
+ Thm.transitive
+ (inst [] [m, n] @{thm le_num_simps(7) [meta]})
+ (less_num_conv m n))
+
+and less_num_conv m n = (case (strip_app m, strip_app n) of
+ (_, (@{const_name Num.One}, [])) =>
+ inst [] [m] @{thm less_num_simps(1) [meta]}
+ | ((@{const_name Num.One}, []), (@{const_name Num.Bit0}, [n])) =>
+ inst [] [n] @{thm less_num_simps(2) [meta]}
+ | ((@{const_name Num.One}, []), (@{const_name Num.Bit1}, [n])) =>
+ inst [] [n] @{thm less_num_simps(3) [meta]}
+ | ((@{const_name Num.Bit0}, [m]), (@{const_name Num.Bit0}, [n])) =>
+ Thm.transitive
+ (inst [] [m, n] @{thm less_num_simps(4) [meta]})
+ (less_num_conv m n)
+ | ((@{const_name Num.Bit0}, [m]), (@{const_name Num.Bit1}, [n])) =>
+ Thm.transitive
+ (inst [] [m, n] @{thm less_num_simps(5) [meta]})
+ (le_num_conv m n)
+ | ((@{const_name Num.Bit1}, [m]), (@{const_name Num.Bit1}, [n])) =>
+ Thm.transitive
+ (inst [] [m, n] @{thm less_num_simps(6) [meta]})
+ (less_num_conv m n)
+ | ((@{const_name Num.Bit1}, [m]), (@{const_name Num.Bit0}, [n])) =>
+ Thm.transitive
+ (inst [] [m, n] @{thm less_num_simps(7) [meta]})
+ (less_num_conv m n));
+*}
+
+ML {*
+fun le_conv f a =
+ let
+ val zero_le_zero_a = inst [a] [] @{thm order_refl [of 0, THEN Eq_TrueI]};
+ val zero_le_numeral_a =
+ inst [a] [] @{thm zero_le_numeral [THEN Eq_TrueI]};
+ val not_numeral_le_zero_a =
+ inst [a] [] @{thm not_numeral_le_zero [THEN Eq_FalseI]};
+ val numeral_le_iff_a = inst [a] [] @{thm numeral_le_iff [meta]};
+ val expand1_a = expand1 a;
+
+ fun conv m n = (case (strip_app m, strip_app n) of
+ ((@{const_name zero_class.zero}, []), (@{const_name zero_class.zero}, [])) =>
+ zero_le_zero_a
+ | ((@{const_name zero_class.zero}, []), (@{const_name numeral}, [n])) =>
+ inst [] [n] zero_le_numeral_a
+ | ((@{const_name numeral}, [m]), (@{const_name zero_class.zero}, [])) =>
+ inst [] [m] not_numeral_le_zero_a
+ | ((@{const_name numeral}, [m]), (@{const_name numeral}, [n])) =>
+ Thm.transitive
+ (inst [] [m, n] numeral_le_iff_a)
+ (le_num_conv m n)
+ | _ => cong2'' (f conv) (expand1_a m) (expand1_a n))
+ in f conv end;
+
+val nat_le_conv = le_conv I @{ctyp nat};
+*}
+
+ML {*
+fun le_neg_conv a =
+ let
+ val neg_numeral_le_zero_a =
+ inst [a] [] @{thm neg_numeral_le_zero [THEN Eq_TrueI]};
+ val not_zero_le_neg_numeral_a =
+ inst [a] [] @{thm not_zero_le_neg_numeral [THEN Eq_FalseI]};
+ val neg_numeral_le_numeral_a =
+ inst [a] [] @{thm neg_numeral_le_numeral [THEN Eq_TrueI]};
+ val not_numeral_le_neg_numeral_a =
+ inst [a] [] @{thm not_numeral_le_neg_numeral [THEN Eq_FalseI]};
+ val neg_numeral_le_iff_a = inst [a] [] @{thm neg_numeral_le_iff [meta]}
+ in
+ fn conv => fn m => fn n =>
+ case (strip_numeral m, strip_numeral n) of
+ ((@{const_name uminus}, [m]), (@{const_name zero_class.zero}, [])) =>
+ inst [] [m] neg_numeral_le_zero_a
+ | ((@{const_name zero_class.zero}, []), (@{const_name uminus}, [n])) =>
+ inst [] [n] not_zero_le_neg_numeral_a
+ | ((@{const_name Num.numeral}, [m]), (@{const_name uminus}, [n])) =>
+ inst [] [m, n] not_numeral_le_neg_numeral_a
+ | ((@{const_name uminus}, [m]), (@{const_name Num.numeral}, [n])) =>
+ inst [] [m, n] neg_numeral_le_numeral_a
+ | ((@{const_name uminus}, [m]), (@{const_name uminus}, [n])) =>
+ Thm.transitive
+ (inst [] [m, n] neg_numeral_le_iff_a)
+ (le_num_conv n m)
+ | _ => conv m n
+ end;
+
+fun le_conv' a = le_conv (le_neg_conv a) a;
+
+val int_le_conv = le_conv' @{ctyp int};
+*}
+
+ML {*
+fun less_conv f a =
+ let
+ val not_zero_less_zero_a = inst [a] [] @{thm less_irrefl [of 0, THEN Eq_FalseI]};
+ val zero_less_numeral_a =
+ inst [a] [] @{thm zero_less_numeral [THEN Eq_TrueI]};
+ val not_numeral_less_zero_a =
+ inst [a] [] @{thm not_numeral_less_zero [THEN Eq_FalseI]};
+ val numeral_less_iff_a = inst [a] [] @{thm numeral_less_iff [meta]};
+ val expand1_a = expand1 a;
+
+ fun conv m n = (case (strip_app m, strip_app n) of
+ ((@{const_name zero_class.zero}, []), (@{const_name zero_class.zero}, [])) =>
+ not_zero_less_zero_a
+ | ((@{const_name zero_class.zero}, []), (@{const_name numeral}, [n])) =>
+ inst [] [n] zero_less_numeral_a
+ | ((@{const_name numeral}, [m]), (@{const_name zero_class.zero}, [])) =>
+ inst [] [m] not_numeral_less_zero_a
+ | ((@{const_name numeral}, [m]), (@{const_name numeral}, [n])) =>
+ Thm.transitive
+ (inst [] [m, n] numeral_less_iff_a)
+ (less_num_conv m n)
+ | _ => cong2'' (f conv) (expand1_a m) (expand1_a n))
+ in f conv end;
+
+val nat_less_conv = less_conv I @{ctyp nat};
+*}
+
+ML {*
+fun less_neg_conv a =
+ let
+ val neg_numeral_less_zero_a =
+ inst [a] [] @{thm neg_numeral_less_zero [THEN Eq_TrueI]};
+ val not_zero_less_neg_numeral_a =
+ inst [a] [] @{thm not_zero_less_neg_numeral [THEN Eq_FalseI]};
+ val neg_numeral_less_numeral_a =
+ inst [a] [] @{thm neg_numeral_less_numeral [THEN Eq_TrueI]};
+ val not_numeral_less_neg_numeral_a =
+ inst [a] [] @{thm not_numeral_less_neg_numeral [THEN Eq_FalseI]};
+ val neg_numeral_less_iff_a = inst [a] [] @{thm neg_numeral_less_iff [meta]}
+ in
+ fn conv => fn m => fn n =>
+ case (strip_numeral m, strip_numeral n) of
+ ((@{const_name uminus}, [m]), (@{const_name zero_class.zero}, [])) =>
+ inst [] [m] neg_numeral_less_zero_a
+ | ((@{const_name zero_class.zero}, []), (@{const_name uminus}, [n])) =>
+ inst [] [n] not_zero_less_neg_numeral_a
+ | ((@{const_name Num.numeral}, [m]), (@{const_name uminus}, [n])) =>
+ inst [] [m, n] not_numeral_less_neg_numeral_a
+ | ((@{const_name uminus}, [m]), (@{const_name Num.numeral}, [n])) =>
+ inst [] [m, n] neg_numeral_less_numeral_a
+ | ((@{const_name uminus}, [m]), (@{const_name uminus}, [n])) =>
+ Thm.transitive
+ (inst [] [m, n] neg_numeral_less_iff_a)
+ (less_num_conv n m)
+ | _ => conv m n
+ end;
+
+fun less_conv' a = less_conv (less_neg_conv a) a;
+
+val int_less_conv = less_conv' @{ctyp int};
+*}
+
+ML {*
+fun If_conv a =
+ let
+ val if_True = inst [a] [] @{thm if_True [meta]};
+ val if_False = inst [a] [] @{thm if_False [meta]}
+ in
+ fn p => fn x => fn y => fn ct =>
+ case strip_app ct of
+ (@{const_name If}, [cb, cx, cy]) =>
+ let
+ val p_eq = p cb
+ val eq = Thm.combination (Thm.reflexive (Thm.dest_fun (Thm.dest_fun2 ct))) p_eq
+ in
+ case Thm.term_of (Thm.rhs_of p_eq) of
+ Const (@{const_name True}, _) =>
+ let
+ val x_eq = x cx;
+ val cx = Thm.rhs_of x_eq;
+ in
+ Thm.transitive
+ (Thm.combination
+ (Thm.combination eq x_eq)
+ (Thm.reflexive cy))
+ (inst [] [cx, cy] if_True)
+ end
+ | Const (@{const_name False}, _) =>
+ let
+ val y_eq = y cy;
+ val cy = Thm.rhs_of y_eq;
+ in
+ Thm.transitive
+ (Thm.combination
+ (Thm.combination eq (Thm.reflexive cx))
+ y_eq)
+ (inst [] [cx, cy] if_False)
+ end
+ | _ => err "If_conv" (Thm.rhs_of p_eq)
+ end
+ end;
+*}
+
+ML {*
+fun drop_conv a =
+ let
+ val drop_0_a = inst [a] [] @{thm drop_0 [meta]};
+ val drop_Cons_a = inst [a] [] @{thm drop_Cons' [meta]};
+ val If_conv_a = If_conv (type_of_eqn drop_0_a);
+
+ fun conv n ys = (case Thm.term_of n of
+ Const (@{const_name zero_class.zero}, _) => inst [] [ys] drop_0_a
+ | _ => (case strip_app ys of
+ (@{const_name Cons}, [x, xs]) =>
+ transitive'
+ (inst [] [n, x, xs] drop_Cons_a)
+ (If_conv_a (args2 nat_eq_conv)
+ Thm.reflexive
+ (cong2' conv (args2 nat_minus_conv) Thm.reflexive))))
+ in conv end;
+*}
+
+ML {*
+fun nth_conv a =
+ let
+ val nth_Cons_a = inst [a] [] @{thm nth_Cons' [meta]};
+ val If_conv_a = If_conv a;
+
+ fun conv ys n = (case strip_app ys of
+ (@{const_name Cons}, [x, xs]) =>
+ transitive'
+ (inst [] [x, xs, n] nth_Cons_a)
+ (If_conv_a (args2 nat_eq_conv)
+ Thm.reflexive
+ (cong2' conv Thm.reflexive (args2 nat_minus_conv))))
+ in conv end;
+*}
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Decision_Procs/Reflective_Field.thy Sun Jan 29 11:59:48 2017 +0100
@@ -0,0 +1,941 @@
+(* Title: HOL/Decision_Procs/Reflective_Field.thy
+ Author: Stefan Berghofer
+
+Reducing equalities in fields to equalities in rings.
+*)
+
+theory Reflective_Field
+imports Commutative_Ring
+begin
+
+datatype fexpr =
+ FCnst int
+ | FVar nat
+ | FAdd fexpr fexpr
+ | FSub fexpr fexpr
+ | FMul fexpr fexpr
+ | FNeg fexpr
+ | FDiv fexpr fexpr
+ | FPow fexpr nat
+
+fun (in field) nth_el :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" where
+ "nth_el [] n = \<zero>"
+| "nth_el (x # xs) 0 = x"
+| "nth_el (x # xs) (Suc n) = nth_el xs n"
+
+lemma (in field) nth_el_Cons:
+ "nth_el (x # xs) n = (if n = 0 then x else nth_el xs (n - 1))"
+ by (cases n) simp_all
+
+lemma (in field) nth_el_closed [simp]:
+ "in_carrier xs \<Longrightarrow> nth_el xs n \<in> carrier R"
+ by (induct xs n rule: nth_el.induct) (simp_all add: in_carrier_def)
+
+primrec (in field) feval :: "'a list \<Rightarrow> fexpr \<Rightarrow> 'a"
+where
+ "feval xs (FCnst c) = \<guillemotleft>c\<guillemotright>"
+| "feval xs (FVar n) = nth_el xs n"
+| "feval xs (FAdd a b) = feval xs a \<oplus> feval xs b"
+| "feval xs (FSub a b) = feval xs a \<ominus> feval xs b"
+| "feval xs (FMul a b) = feval xs a \<otimes> feval xs b"
+| "feval xs (FNeg a) = \<ominus> feval xs a"
+| "feval xs (FDiv a b) = feval xs a \<oslash> feval xs b"
+| "feval xs (FPow a n) = feval xs a (^) n"
+
+lemma (in field) feval_Cnst:
+ "feval xs (FCnst 0) = \<zero>"
+ "feval xs (FCnst 1) = \<one>"
+ "feval xs (FCnst (numeral n)) = \<guillemotleft>numeral n\<guillemotright>"
+ by simp_all
+
+datatype pexpr =
+ PExpr1 pexpr1
+ | PExpr2 pexpr2
+and pexpr1 =
+ PCnst int
+ | PVar nat
+ | PAdd pexpr pexpr
+ | PSub pexpr pexpr
+ | PNeg pexpr
+and pexpr2 =
+ PMul pexpr pexpr
+ | PPow pexpr nat
+
+lemma pexpr_cases [case_names PCnst PVar PAdd PSub PNeg PMul PPow]:
+ assumes
+ "\<And>c. e = PExpr1 (PCnst c) \<Longrightarrow> P"
+ "\<And>n. e = PExpr1 (PVar n) \<Longrightarrow> P"
+ "\<And>e1 e2. e = PExpr1 (PAdd e1 e2) \<Longrightarrow> P"
+ "\<And>e1 e2. e = PExpr1 (PSub e1 e2) \<Longrightarrow> P"
+ "\<And>e'. e = PExpr1 (PNeg e') \<Longrightarrow> P"
+ "\<And>e1 e2. e = PExpr2 (PMul e1 e2) \<Longrightarrow> P"
+ "\<And>e' n. e = PExpr2 (PPow e' n) \<Longrightarrow> P"
+ shows P
+proof (cases e)
+ case (PExpr1 e')
+ then show ?thesis
+ apply (cases e')
+ apply simp_all
+ apply (erule assms)+
+ done
+next
+ case (PExpr2 e')
+ then show ?thesis
+ apply (cases e')
+ apply simp_all
+ apply (erule assms)+
+ done
+qed
+
+lemmas pexpr_cases2 = pexpr_cases [case_product pexpr_cases]
+
+fun (in field) peval :: "'a list \<Rightarrow> pexpr \<Rightarrow> 'a"
+where
+ "peval xs (PExpr1 (PCnst c)) = \<guillemotleft>c\<guillemotright>"
+| "peval xs (PExpr1 (PVar n)) = nth_el xs n"
+| "peval xs (PExpr1 (PAdd a b)) = peval xs a \<oplus> peval xs b"
+| "peval xs (PExpr1 (PSub a b)) = peval xs a \<ominus> peval xs b"
+| "peval xs (PExpr1 (PNeg a)) = \<ominus> peval xs a"
+| "peval xs (PExpr2 (PMul a b)) = peval xs a \<otimes> peval xs b"
+| "peval xs (PExpr2 (PPow a n)) = peval xs a (^) n"
+
+lemma (in field) peval_Cnst:
+ "peval xs (PExpr1 (PCnst 0)) = \<zero>"
+ "peval xs (PExpr1 (PCnst 1)) = \<one>"
+ "peval xs (PExpr1 (PCnst (numeral n))) = \<guillemotleft>numeral n\<guillemotright>"
+ "peval xs (PExpr1 (PCnst (- numeral n))) = \<ominus> \<guillemotleft>numeral n\<guillemotright>"
+ by simp_all
+
+lemma (in field) peval_closed [simp]:
+ "in_carrier xs \<Longrightarrow> peval xs e \<in> carrier R"
+ "in_carrier xs \<Longrightarrow> peval xs (PExpr1 e1) \<in> carrier R"
+ "in_carrier xs \<Longrightarrow> peval xs (PExpr2 e2) \<in> carrier R"
+ by (induct e and e1 and e2) simp_all
+
+definition npepow :: "pexpr \<Rightarrow> nat \<Rightarrow> pexpr"
+where
+ "npepow e n =
+ (if n = 0 then PExpr1 (PCnst 1)
+ else if n = 1 then e
+ else (case e of
+ PExpr1 (PCnst c) \<Rightarrow> PExpr1 (PCnst (c ^ n))
+ | _ \<Rightarrow> PExpr2 (PPow e n)))"
+
+lemma (in field) npepow_correct:
+ "in_carrier xs \<Longrightarrow> peval xs (npepow e n) = peval xs (PExpr2 (PPow e n))"
+ by (cases e rule: pexpr_cases)
+ (simp_all add: npepow_def)
+
+fun npemul :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr"
+where
+ "npemul x y = (case x of
+ PExpr1 (PCnst c) \<Rightarrow>
+ if c = 0 then x
+ else if c = 1 then y else
+ (case y of
+ PExpr1 (PCnst d) \<Rightarrow> PExpr1 (PCnst (c * d))
+ | _ \<Rightarrow> PExpr2 (PMul x y))
+ | PExpr2 (PPow e1 n) \<Rightarrow>
+ (case y of
+ PExpr2 (PPow e2 m) \<Rightarrow>
+ if n = m then npepow (npemul e1 e2) n
+ else PExpr2 (PMul x y)
+ | PExpr1 (PCnst d) \<Rightarrow>
+ if d = 0 then y
+ else if d = 1 then x
+ else PExpr2 (PMul x y)
+ | _ \<Rightarrow> PExpr2 (PMul x y))
+ | _ \<Rightarrow> (case y of
+ PExpr1 (PCnst d) \<Rightarrow>
+ if d = 0 then y
+ else if d = 1 then x
+ else PExpr2 (PMul x y)
+ | _ \<Rightarrow> PExpr2 (PMul x y)))"
+
+lemma (in field) npemul_correct:
+ "in_carrier xs \<Longrightarrow> peval xs (npemul e1 e2) = peval xs (PExpr2 (PMul e1 e2))"
+proof (induct e1 e2 rule: npemul.induct)
+ case (1 x y)
+ then show ?case
+ proof (cases x y rule: pexpr_cases2)
+ case (PPow_PPow e n e' m)
+ then show ?thesis
+ by (simp add: 1 npepow_correct nat_pow_distr
+ npemul.simps [of "PExpr2 (PPow e n)" "PExpr2 (PPow e' m)"]
+ del: npemul.simps)
+ qed simp_all
+qed
+
+declare npemul.simps [simp del]
+
+definition npeadd :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr"
+where
+ "npeadd x y = (case x of
+ PExpr1 (PCnst c) \<Rightarrow>
+ if c = 0 then y else
+ (case y of
+ PExpr1 (PCnst d) \<Rightarrow> PExpr1 (PCnst (c + d))
+ | _ \<Rightarrow> PExpr1 (PAdd x y))
+ | _ \<Rightarrow> (case y of
+ PExpr1 (PCnst d) \<Rightarrow>
+ if d = 0 then x
+ else PExpr1 (PAdd x y)
+ | _ \<Rightarrow> PExpr1 (PAdd x y)))"
+
+lemma (in field) npeadd_correct:
+ "in_carrier xs \<Longrightarrow> peval xs (npeadd e1 e2) = peval xs (PExpr1 (PAdd e1 e2))"
+ by (cases e1 e2 rule: pexpr_cases2) (simp_all add: npeadd_def)
+
+definition npesub :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr"
+where
+ "npesub x y = (case y of
+ PExpr1 (PCnst d) \<Rightarrow>
+ if d = 0 then x else
+ (case x of
+ PExpr1 (PCnst c) \<Rightarrow> PExpr1 (PCnst (c - d))
+ | _ \<Rightarrow> PExpr1 (PSub x y))
+ | _ \<Rightarrow> (case x of
+ PExpr1 (PCnst c) \<Rightarrow>
+ if c = 0 then PExpr1 (PNeg y)
+ else PExpr1 (PSub x y)
+ | _ \<Rightarrow> PExpr1 (PSub x y)))"
+
+lemma (in field) npesub_correct:
+ "in_carrier xs \<Longrightarrow> peval xs (npesub e1 e2) = peval xs (PExpr1 (PSub e1 e2))"
+ by (cases e1 e2 rule: pexpr_cases2) (simp_all add: npesub_def)
+
+definition npeneg :: "pexpr \<Rightarrow> pexpr"
+where
+ "npeneg e = (case e of
+ PExpr1 (PCnst c) \<Rightarrow> PExpr1 (PCnst (- c))
+ | _ \<Rightarrow> PExpr1 (PNeg e))"
+
+lemma (in field) npeneg_correct:
+ "peval xs (npeneg e) = peval xs (PExpr1 (PNeg e))"
+ by (cases e rule: pexpr_cases) (simp_all add: npeneg_def)
+
+lemma option_pair_cases [case_names None Some]:
+ assumes
+ "x = None \<Longrightarrow> P"
+ "\<And>p q. x = Some (p, q) \<Longrightarrow> P"
+ shows P
+proof (cases x)
+ case None
+ then show ?thesis by (rule assms)
+next
+ case (Some r)
+ then show ?thesis
+ apply (cases r)
+ apply simp
+ by (rule assms)
+qed
+
+fun isin :: "pexpr \<Rightarrow> nat \<Rightarrow> pexpr \<Rightarrow> nat \<Rightarrow> (nat * pexpr) option"
+where
+ "isin e n (PExpr2 (PMul e1 e2)) m =
+ (case isin e n e1 m of
+ Some (k, e3) \<Rightarrow>
+ if k = 0 then Some (0, npemul e3 (npepow e2 m))
+ else (case isin e k e2 m of
+ Some (l, e4) \<Rightarrow> Some (l, npemul e3 e4)
+ | None \<Rightarrow> Some (k, npemul e3 (npepow e2 m)))
+ | None \<Rightarrow> (case isin e n e2 m of
+ Some (k, e3) \<Rightarrow> Some (k, npemul (npepow e1 m) e3)
+ | None \<Rightarrow> None))"
+| "isin e n (PExpr2 (PPow e' k)) m =
+ (if k = 0 then None else isin e n e' (k * m))"
+| "isin (PExpr1 e) n (PExpr1 e') m =
+ (if e = e' then
+ if n >= m then Some (n - m, PExpr1 (PCnst 1))
+ else Some (0, npepow (PExpr1 e) (m - n))
+ else None)"
+| "isin (PExpr2 e) n (PExpr1 e') m = None"
+
+lemma (in field) isin_correct:
+ assumes "in_carrier xs"
+ and "isin e n e' m = Some (p, e'')"
+ shows
+ "peval xs (PExpr2 (PPow e' m)) =
+ peval xs (PExpr2 (PMul (PExpr2 (PPow e (n - p))) e''))"
+ "p \<le> n"
+ using assms
+ by (induct e n e' m arbitrary: p e'' rule: isin.induct)
+ (force
+ simp add:
+ nat_pow_distr nat_pow_pow nat_pow_mult m_ac
+ npemul_correct npepow_correct
+ split: option.split_asm prod.split_asm if_split_asm)+
+
+lemma (in field) isin_correct':
+ "in_carrier xs \<Longrightarrow> isin e n e' 1 = Some (p, e'') \<Longrightarrow>
+ peval xs e' = peval xs e (^) (n - p) \<otimes> peval xs e''"
+ "in_carrier xs \<Longrightarrow> isin e n e' 1 = Some (p, e'') \<Longrightarrow> p \<le> n"
+ using isin_correct [where m=1]
+ by simp_all
+
+fun split_aux :: "pexpr \<Rightarrow> nat \<Rightarrow> pexpr \<Rightarrow> pexpr \<times> pexpr \<times> pexpr"
+where
+ "split_aux (PExpr2 (PMul e1 e2)) n e =
+ (let
+ (left1, common1, right1) = split_aux e1 n e;
+ (left2, common2, right2) = split_aux e2 n right1
+ in (npemul left1 left2, npemul common1 common2, right2))"
+| "split_aux (PExpr2 (PPow e' m)) n e =
+ (if m = 0 then (PExpr1 (PCnst 1), PExpr1 (PCnst 1), e)
+ else split_aux e' (m * n) e)"
+| "split_aux (PExpr1 e') n e =
+ (case isin (PExpr1 e') n e 1 of
+ Some (m, e'') \<Rightarrow>
+ (if m = 0 then (PExpr1 (PCnst 1), npepow (PExpr1 e') n, e'')
+ else (npepow (PExpr1 e') m, npepow (PExpr1 e') (n - m), e''))
+ | None \<Rightarrow> (npepow (PExpr1 e') n, PExpr1 (PCnst 1), e))"
+
+hide_const Left Right
+
+abbreviation Left :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr" where
+ "Left e1 e2 \<equiv> fst (split_aux e1 (Suc 0) e2)"
+
+abbreviation Common :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr" where
+ "Common e1 e2 \<equiv> fst (snd (split_aux e1 (Suc 0) e2))"
+
+abbreviation Right :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr" where
+ "Right e1 e2 \<equiv> snd (snd (split_aux e1 (Suc 0) e2))"
+
+lemma split_aux_induct [case_names 1 2 3]:
+ assumes I1: "\<And>e1 e2 n e. P e1 n e \<Longrightarrow> P e2 n (snd (snd (split_aux e1 n e))) \<Longrightarrow>
+ P (PExpr2 (PMul e1 e2)) n e"
+ and I2: "\<And>e' m n e. (m \<noteq> 0 \<Longrightarrow> P e' (m * n) e) \<Longrightarrow> P (PExpr2 (PPow e' m)) n e"
+ and I3: "\<And>e' n e. P (PExpr1 e') n e"
+ shows "P x y z"
+proof (induct x y z rule: split_aux.induct)
+ case 1
+ from 1(1) 1(2) [OF refl prod.collapse prod.collapse]
+ show ?case by (rule I1)
+next
+ case 2
+ then show ?case by (rule I2)
+next
+ case 3
+ then show ?case by (rule I3)
+qed
+
+lemma (in field) split_aux_correct:
+ "in_carrier xs \<Longrightarrow>
+ peval xs (PExpr2 (PPow e\<^sub>1 n)) =
+ peval xs (PExpr2 (PMul (fst (split_aux e\<^sub>1 n e\<^sub>2)) (fst (snd (split_aux e\<^sub>1 n e\<^sub>2)))))"
+ "in_carrier xs \<Longrightarrow>
+ peval xs e\<^sub>2 =
+ peval xs (PExpr2 (PMul (snd (snd (split_aux e\<^sub>1 n e\<^sub>2))) (fst (snd (split_aux e\<^sub>1 n e\<^sub>2)))))"
+ by (induct e\<^sub>1 n e\<^sub>2 rule: split_aux_induct)
+ (auto simp add: split_beta
+ nat_pow_distr nat_pow_pow nat_pow_mult m_ac
+ npemul_correct npepow_correct isin_correct'
+ split: option.split)
+
+lemma (in field) split_aux_correct':
+ "in_carrier xs \<Longrightarrow>
+ peval xs e\<^sub>1 = peval xs (Left e\<^sub>1 e\<^sub>2) \<otimes> peval xs (Common e\<^sub>1 e\<^sub>2)"
+ "in_carrier xs \<Longrightarrow>
+ peval xs e\<^sub>2 = peval xs (Right e\<^sub>1 e\<^sub>2) \<otimes> peval xs (Common e\<^sub>1 e\<^sub>2)"
+ using split_aux_correct [where n=1]
+ by simp_all
+
+fun fnorm :: "fexpr \<Rightarrow> pexpr \<times> pexpr \<times> pexpr list"
+where
+ "fnorm (FCnst c) = (PExpr1 (PCnst c), PExpr1 (PCnst 1), [])"
+| "fnorm (FVar n) = (PExpr1 (PVar n), PExpr1 (PCnst 1), [])"
+| "fnorm (FAdd e1 e2) =
+ (let
+ (xn, xd, xc) = fnorm e1;
+ (yn, yd, yc) = fnorm e2;
+ (left, common, right) = split_aux xd 1 yd
+ in
+ (npeadd (npemul xn right) (npemul yn left),
+ npemul left (npemul right common),
+ List.union xc yc))"
+| "fnorm (FSub e1 e2) =
+ (let
+ (xn, xd, xc) = fnorm e1;
+ (yn, yd, yc) = fnorm e2;
+ (left, common, right) = split_aux xd 1 yd
+ in
+ (npesub (npemul xn right) (npemul yn left),
+ npemul left (npemul right common),
+ List.union xc yc))"
+| "fnorm (FMul e1 e2) =
+ (let
+ (xn, xd, xc) = fnorm e1;
+ (yn, yd, yc) = fnorm e2;
+ (left1, common1, right1) = split_aux xn 1 yd;
+ (left2, common2, right2) = split_aux yn 1 xd
+ in
+ (npemul left1 left2,
+ npemul right2 right1,
+ List.union xc yc))"
+| "fnorm (FNeg e) =
+ (let (n, d, c) = fnorm e
+ in (npeneg n, d, c))"
+| "fnorm (FDiv e1 e2) =
+ (let
+ (xn, xd, xc) = fnorm e1;
+ (yn, yd, yc) = fnorm e2;
+ (left1, common1, right1) = split_aux xn 1 yn;
+ (left2, common2, right2) = split_aux xd 1 yd
+ in
+ (npemul left1 right2,
+ npemul left2 right1,
+ List.insert yn (List.union xc yc)))"
+| "fnorm (FPow e m) =
+ (let (n, d, c) = fnorm e
+ in (npepow n m, npepow d m, c))"
+
+abbreviation Num :: "fexpr \<Rightarrow> pexpr" where
+ "Num e \<equiv> fst (fnorm e)"
+
+abbreviation Denom :: "fexpr \<Rightarrow> pexpr" where
+ "Denom e \<equiv> fst (snd (fnorm e))"
+
+abbreviation Cond :: "fexpr \<Rightarrow> pexpr list" where
+ "Cond e \<equiv> snd (snd (fnorm e))"
+
+primrec (in field) nonzero :: "'a list \<Rightarrow> pexpr list \<Rightarrow> bool"
+where
+ "nonzero xs [] = True"
+| "nonzero xs (p # ps) = (peval xs p \<noteq> \<zero> \<and> nonzero xs ps)"
+
+lemma (in field) nonzero_singleton:
+ "nonzero xs [p] = (peval xs p \<noteq> \<zero>)"
+ by simp
+
+lemma (in field) nonzero_append:
+ "nonzero xs (ps @ qs) = (nonzero xs ps \<and> nonzero xs qs)"
+ by (induct ps) simp_all
+
+lemma (in field) nonzero_idempotent:
+ "p \<in> set ps \<Longrightarrow> (peval xs p \<noteq> \<zero> \<and> nonzero xs ps) = nonzero xs ps"
+ by (induct ps) auto
+
+lemma (in field) nonzero_insert:
+ "nonzero xs (List.insert p ps) = (peval xs p \<noteq> \<zero> \<and> nonzero xs ps)"
+ by (simp add: List.insert_def nonzero_idempotent)
+
+lemma (in field) nonzero_union:
+ "nonzero xs (List.union ps qs) = (nonzero xs ps \<and> nonzero xs qs)"
+ by (induct ps rule: rev_induct)
+ (auto simp add: List.union_def nonzero_insert nonzero_append)
+
+lemma (in field) fnorm_correct:
+ assumes "in_carrier xs"
+ and "nonzero xs (Cond e)"
+ shows "feval xs e = peval xs (Num e) \<oslash> peval xs (Denom e)"
+ and "peval xs (Denom e) \<noteq> \<zero>"
+ using assms
+proof (induct e)
+ case (FCnst c) {
+ case 1
+ show ?case by simp
+ next
+ case 2
+ show ?case by simp
+ }
+next
+ case (FVar n) {
+ case 1
+ then show ?case by simp
+ next
+ case 2
+ show ?case by simp
+ }
+next
+ case (FAdd e1 e2)
+ note split = split_aux_correct' [where xs=xs and
+ e\<^sub>1="Denom e1" and e\<^sub>2="Denom e2"]
+ {
+ case 1
+ let ?left = "peval xs (Left (Denom e1) (Denom e2))"
+ let ?common = "peval xs (Common (Denom e1) (Denom e2))"
+ let ?right = "peval xs (Right (Denom e1) (Denom e2))"
+ from 1 FAdd
+ have "feval xs (FAdd e1 e2) =
+ (?common \<otimes> (peval xs (Num e1) \<otimes> ?right \<oplus> peval xs (Num e2) \<otimes> ?left)) \<oslash>
+ (?common \<otimes> (?left \<otimes> (?right \<otimes> ?common)))"
+ by (simp add: split_beta split nonzero_union
+ add_frac_eq r_distr m_ac)
+ also from 1 FAdd have "\<dots> =
+ peval xs (Num (FAdd e1 e2)) \<oslash> peval xs (Denom (FAdd e1 e2))"
+ by (simp add: split_beta split nonzero_union npeadd_correct npemul_correct integral_iff)
+ finally show ?case .
+ next
+ case 2
+ with FAdd show ?case
+ by (simp add: split_beta split nonzero_union npemul_correct integral_iff)
+ }
+next
+ case (FSub e1 e2)
+ note split = split_aux_correct' [where xs=xs and
+ e\<^sub>1="Denom e1" and e\<^sub>2="Denom e2"]
+ {
+ case 1
+ let ?left = "peval xs (Left (Denom e1) (Denom e2))"
+ let ?common = "peval xs (Common (Denom e1) (Denom e2))"
+ let ?right = "peval xs (Right (Denom e1) (Denom e2))"
+ from 1 FSub
+ have "feval xs (FSub e1 e2) =
+ (?common \<otimes> (peval xs (Num e1) \<otimes> ?right \<ominus> peval xs (Num e2) \<otimes> ?left)) \<oslash>
+ (?common \<otimes> (?left \<otimes> (?right \<otimes> ?common)))"
+ by (simp add: split_beta split nonzero_union
+ diff_frac_eq r_diff_distr m_ac)
+ also from 1 FSub have "\<dots> =
+ peval xs (Num (FSub e1 e2)) \<oslash> peval xs (Denom (FSub e1 e2))"
+ by (simp add: split_beta split nonzero_union npesub_correct npemul_correct integral_iff)
+ finally show ?case .
+ next
+ case 2
+ with FSub show ?case
+ by (simp add: split_beta split nonzero_union npemul_correct integral_iff)
+ }
+next
+ case (FMul e1 e2)
+ note split =
+ split_aux_correct' [where xs=xs and
+ e\<^sub>1="Num e1" and e\<^sub>2="Denom e2"]
+ split_aux_correct' [where xs=xs and
+ e\<^sub>1="Num e2" and e\<^sub>2="Denom e1"]
+ {
+ case 1
+ let ?left\<^sub>1 = "peval xs (Left (Num e1) (Denom e2))"
+ let ?common\<^sub>1 = "peval xs (Common (Num e1) (Denom e2))"
+ let ?right\<^sub>1 = "peval xs (Right (Num e1) (Denom e2))"
+ let ?left\<^sub>2 = "peval xs (Left (Num e2) (Denom e1))"
+ let ?common\<^sub>2 = "peval xs (Common (Num e2) (Denom e1))"
+ let ?right\<^sub>2 = "peval xs (Right (Num e2) (Denom e1))"
+ from 1 FMul
+ have "feval xs (FMul e1 e2) =
+ ((?common\<^sub>1 \<otimes> ?common\<^sub>2) \<otimes> (?left\<^sub>1 \<otimes> ?left\<^sub>2)) \<oslash>
+ ((?common\<^sub>1 \<otimes> ?common\<^sub>2) \<otimes> (?right\<^sub>2 \<otimes> ?right\<^sub>1))"
+ by (simp add: split_beta split nonzero_union
+ nonzero_divide_divide_eq_left m_ac)
+ also from 1 FMul have "\<dots> =
+ peval xs (Num (FMul e1 e2)) \<oslash> peval xs (Denom (FMul e1 e2))"
+ by (simp add: split_beta split nonzero_union npemul_correct integral_iff)
+ finally show ?case .
+ next
+ case 2
+ with FMul show ?case
+ by (simp add: split_beta split nonzero_union npemul_correct integral_iff)
+ }
+next
+ case (FNeg e)
+ {
+ case 1
+ with FNeg show ?case
+ by (simp add: split_beta npeneg_correct)
+ next
+ case 2
+ with FNeg show ?case
+ by (simp add: split_beta)
+ }
+next
+ case (FDiv e1 e2)
+ note split =
+ split_aux_correct' [where xs=xs and
+ e\<^sub>1="Num e1" and e\<^sub>2="Num e2"]
+ split_aux_correct' [where xs=xs and
+ e\<^sub>1="Denom e1" and e\<^sub>2="Denom e2"]
+ {
+ case 1
+ let ?left\<^sub>1 = "peval xs (Left (Num e1) (Num e2))"
+ let ?common\<^sub>1 = "peval xs (Common (Num e1) (Num e2))"
+ let ?right\<^sub>1 = "peval xs (Right (Num e1) (Num e2))"
+ let ?left\<^sub>2 = "peval xs (Left (Denom e1) (Denom e2))"
+ let ?common\<^sub>2 = "peval xs (Common (Denom e1) (Denom e2))"
+ let ?right\<^sub>2 = "peval xs (Right (Denom e1) (Denom e2))"
+ from 1 FDiv
+ have "feval xs (FDiv e1 e2) =
+ ((?common\<^sub>1 \<otimes> ?common\<^sub>2) \<otimes> (?left\<^sub>1 \<otimes> ?right\<^sub>2)) \<oslash>
+ ((?common\<^sub>1 \<otimes> ?common\<^sub>2) \<otimes> (?left\<^sub>2 \<otimes> ?right\<^sub>1))"
+ by (simp add: split_beta split nonzero_union nonzero_insert
+ nonzero_divide_divide_eq m_ac)
+ also from 1 FDiv have "\<dots> =
+ peval xs (Num (FDiv e1 e2)) \<oslash> peval xs (Denom (FDiv e1 e2))"
+ by (simp add: split_beta split nonzero_union nonzero_insert npemul_correct integral_iff)
+ finally show ?case .
+ next
+ case 2
+ with FDiv show ?case
+ by (simp add: split_beta split nonzero_union nonzero_insert npemul_correct integral_iff)
+ }
+next
+ case (FPow e n)
+ {
+ case 1
+ with FPow show ?case
+ by (simp add: split_beta nonzero_power_divide npepow_correct)
+ next
+ case 2
+ with FPow show ?case
+ by (simp add: split_beta npepow_correct)
+ }
+qed
+
+lemma (in field) feval_eq0:
+ assumes "in_carrier xs"
+ and "fnorm e = (n, d, c)"
+ and "nonzero xs c"
+ and "peval xs n = \<zero>"
+ shows "feval xs e = \<zero>"
+ using assms fnorm_correct [of xs e]
+ by simp
+
+lemma (in field) fexpr_in_carrier:
+ assumes "in_carrier xs"
+ and "nonzero xs (Cond e)"
+ shows "feval xs e \<in> carrier R"
+ using assms
+proof (induct e)
+ case (FDiv e1 e2)
+ then have "feval xs e1 \<in> carrier R" "feval xs e2 \<in> carrier R"
+ "peval xs (Num e2) \<noteq> \<zero>" "nonzero xs (Cond e2)"
+ by (simp_all add: nonzero_union nonzero_insert split: prod.split_asm)
+ from `in_carrier xs` `nonzero xs (Cond e2)`
+ have "feval xs e2 = peval xs (Num e2) \<oslash> peval xs (Denom e2)"
+ by (rule fnorm_correct)
+ moreover from `in_carrier xs` `nonzero xs (Cond e2)`
+ have "peval xs (Denom e2) \<noteq> \<zero>" by (rule fnorm_correct)
+ ultimately have "feval xs e2 \<noteq> \<zero>" using `peval xs (Num e2) \<noteq> \<zero>` `in_carrier xs`
+ by (simp add: divide_eq_0_iff)
+ with `feval xs e1 \<in> carrier R` `feval xs e2 \<in> carrier R`
+ show ?case by simp
+qed (simp_all add: nonzero_union split: prod.split_asm)
+
+lemma (in field) feval_eq:
+ assumes "in_carrier xs"
+ and "fnorm (FSub e e') = (n, d, c)"
+ and "nonzero xs c"
+ shows "(feval xs e = feval xs e') = (peval xs n = \<zero>)"
+proof -
+ from assms have "nonzero xs (Cond e)" "nonzero xs (Cond e')"
+ by (auto simp add: nonzero_union split: prod.split_asm)
+ with assms fnorm_correct [of xs "FSub e e'"]
+ have "feval xs e \<ominus> feval xs e' = peval xs n \<oslash> peval xs d"
+ "peval xs d \<noteq> \<zero>"
+ by simp_all
+ show ?thesis
+ proof
+ assume "feval xs e = feval xs e'"
+ with `feval xs e \<ominus> feval xs e' = peval xs n \<oslash> peval xs d`
+ `in_carrier xs` `nonzero xs (Cond e')`
+ have "peval xs n \<oslash> peval xs d = \<zero>"
+ by (simp add: fexpr_in_carrier minus_eq r_neg)
+ with `peval xs d \<noteq> \<zero>` `in_carrier xs`
+ show "peval xs n = \<zero>"
+ by (simp add: divide_eq_0_iff)
+ next
+ assume "peval xs n = \<zero>"
+ with `feval xs e \<ominus> feval xs e' = peval xs n \<oslash> peval xs d` `peval xs d \<noteq> \<zero>`
+ `nonzero xs (Cond e)` `nonzero xs (Cond e')` `in_carrier xs`
+ show "feval xs e = feval xs e'"
+ by (simp add: eq_diff0 fexpr_in_carrier)
+ qed
+qed
+
+code_reflect Field_Code
+ datatypes fexpr = FCnst | FVar | FAdd | FSub | FMul | FNeg | FDiv | FPow
+ and pexpr = PExpr1 | PExpr2
+ and pexpr1 = PCnst | PVar | PAdd | PSub | PNeg
+ and pexpr2 = PMul | PPow
+ functions fnorm
+ term_of_fexpr_inst.term_of_fexpr
+ term_of_pexpr_inst.term_of_pexpr
+ equal_pexpr_inst.equal_pexpr
+
+definition field_codegen_aux :: "(pexpr \<times> pexpr list) itself" where
+ "field_codegen_aux = (Code_Evaluation.TERM_OF_EQUAL::(pexpr \<times> pexpr list) itself)"
+
+ML {*
+signature FIELD_TAC =
+sig
+ structure Field_Simps:
+ sig
+ type T
+ val get: Context.generic -> T
+ val put: T -> Context.generic -> Context.generic
+ val map: (T -> T) -> Context.generic -> Context.generic
+ end
+ val eq_field_simps:
+ (term * (thm list * thm list * thm list * thm * thm)) *
+ (term * (thm list * thm list * thm list * thm * thm)) -> bool
+ val field_tac: bool -> Proof.context -> int -> tactic
+end
+
+structure Field_Tac : FIELD_TAC =
+struct
+
+open Ring_Tac;
+
+fun field_struct (Const (@{const_name Ring.ring.add}, _) $ R $ _ $ _) = SOME R
+ | field_struct (Const (@{const_name Ring.a_minus}, _) $ R $ _ $ _) = SOME R
+ | field_struct (Const (@{const_name Group.monoid.mult}, _) $ R $ _ $ _) = SOME R
+ | field_struct (Const (@{const_name Ring.a_inv}, _) $ R $ _) = SOME R
+ | field_struct (Const (@{const_name Group.pow}, _) $ R $ _ $ _) = SOME R
+ | field_struct (Const (@{const_name Algebra_Aux.m_div}, _) $ R $ _ $ _) = SOME R
+ | field_struct (Const (@{const_name Ring.ring.zero}, _) $ R) = SOME R
+ | field_struct (Const (@{const_name Group.monoid.one}, _) $ R) = SOME R
+ | field_struct (Const (@{const_name Algebra_Aux.of_integer}, _) $ R $ _) = SOME R
+ | field_struct _ = NONE;
+
+fun reif_fexpr vs (Const (@{const_name Ring.ring.add}, _) $ _ $ a $ b) =
+ @{const FAdd} $ reif_fexpr vs a $ reif_fexpr vs b
+ | reif_fexpr vs (Const (@{const_name Ring.a_minus}, _) $ _ $ a $ b) =
+ @{const FSub} $ reif_fexpr vs a $ reif_fexpr vs b
+ | reif_fexpr vs (Const (@{const_name Group.monoid.mult}, _) $ _ $ a $ b) =
+ @{const FMul} $ reif_fexpr vs a $ reif_fexpr vs b
+ | reif_fexpr vs (Const (@{const_name Ring.a_inv}, _) $ _ $ a) =
+ @{const FNeg} $ reif_fexpr vs a
+ | reif_fexpr vs (Const (@{const_name Group.pow}, _) $ _ $ a $ n) =
+ @{const FPow} $ reif_fexpr vs a $ n
+ | reif_fexpr vs (Const (@{const_name Algebra_Aux.m_div}, _) $ _ $ a $ b) =
+ @{const FDiv} $ reif_fexpr vs a $ reif_fexpr vs b
+ | reif_fexpr vs (Free x) =
+ @{const FVar} $ HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)
+ | reif_fexpr vs (Const (@{const_name Ring.ring.zero}, _) $ _) =
+ @{term "FCnst 0"}
+ | reif_fexpr vs (Const (@{const_name Group.monoid.one}, _) $ _) =
+ @{term "FCnst 1"}
+ | reif_fexpr vs (Const (@{const_name Algebra_Aux.of_integer}, _) $ _ $ n) =
+ @{const FCnst} $ n
+ | reif_fexpr _ _ = error "reif_fexpr: bad expression";
+
+fun reif_fexpr' vs (Const (@{const_name Groups.plus}, _) $ a $ b) =
+ @{const FAdd} $ reif_fexpr' vs a $ reif_fexpr' vs b
+ | reif_fexpr' vs (Const (@{const_name Groups.minus}, _) $ a $ b) =
+ @{const FSub} $ reif_fexpr' vs a $ reif_fexpr' vs b
+ | reif_fexpr' vs (Const (@{const_name Groups.times}, _) $ a $ b) =
+ @{const FMul} $ reif_fexpr' vs a $ reif_fexpr' vs b
+ | reif_fexpr' vs (Const (@{const_name Groups.uminus}, _) $ a) =
+ @{const FNeg} $ reif_fexpr' vs a
+ | reif_fexpr' vs (Const (@{const_name Power.power}, _) $ a $ n) =
+ @{const FPow} $ reif_fexpr' vs a $ n
+ | reif_fexpr' vs (Const (@{const_name divide}, _) $ a $ b) =
+ @{const FDiv} $ reif_fexpr' vs a $ reif_fexpr' vs b
+ | reif_fexpr' vs (Free x) =
+ @{const FVar} $ HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)
+ | reif_fexpr' vs (Const (@{const_name zero_class.zero}, _)) =
+ @{term "FCnst 0"}
+ | reif_fexpr' vs (Const (@{const_name one_class.one}, _)) =
+ @{term "FCnst 1"}
+ | reif_fexpr' vs (Const (@{const_name numeral}, _) $ b) =
+ @{const FCnst} $ (@{const numeral (int)} $ b)
+ | reif_fexpr' _ _ = error "reif_fexpr: bad expression";
+
+fun eq_field_simps
+ ((t, (ths1, ths2, ths3, th4, th)),
+ (t', (ths1', ths2', ths3', th4', th'))) =
+ t aconv t' andalso
+ eq_list Thm.eq_thm (ths1, ths1') andalso
+ eq_list Thm.eq_thm (ths2, ths2') andalso
+ eq_list Thm.eq_thm (ths3, ths3') andalso
+ Thm.eq_thm (th4, th4') andalso
+ Thm.eq_thm (th, th');
+
+structure Field_Simps = Generic_Data
+(struct
+ type T = (term * (thm list * thm list * thm list * thm * thm)) Net.net
+ val empty = Net.empty
+ val extend = I
+ val merge = Net.merge eq_field_simps
+end);
+
+fun get_field_simps ctxt optcT t =
+ (case get_matching_rules ctxt (Field_Simps.get (Context.Proof ctxt)) t of
+ SOME (ths1, ths2, ths3, th4, th) =>
+ let val tr =
+ Thm.transfer (Proof_Context.theory_of ctxt) #>
+ (case optcT of NONE => I | SOME cT => inst [cT] [] #> norm)
+ in (map tr ths1, map tr ths2, map tr ths3, tr th4, tr th) end
+ | NONE => error "get_field_simps: lookup failed");
+
+fun nth_el_conv (_, _, _, nth_el_Cons, _) =
+ let
+ val a = type_of_eqn nth_el_Cons;
+ val If_conv_a = If_conv a;
+
+ fun conv ys n = (case strip_app ys of
+ (@{const_name Cons}, [x, xs]) =>
+ transitive'
+ (inst [] [x, xs, n] nth_el_Cons)
+ (If_conv_a (args2 nat_eq_conv)
+ Thm.reflexive
+ (cong2' conv Thm.reflexive (args2 nat_minus_conv))))
+ in conv end;
+
+fun feval_conv (rls as
+ ([feval_simps_1, feval_simps_2, feval_simps_3,
+ feval_simps_4, feval_simps_5, feval_simps_6,
+ feval_simps_7, feval_simps_8, feval_simps_9,
+ feval_simps_10, feval_simps_11],
+ _, _, _, _)) =
+ let
+ val nth_el_conv' = nth_el_conv rls;
+
+ fun conv xs x = (case strip_app x of
+ (@{const_name FCnst}, [c]) => (case strip_app c of
+ (@{const_name zero_class.zero}, _) => inst [] [xs] feval_simps_9
+ | (@{const_name one_class.one}, _) => inst [] [xs] feval_simps_10
+ | (@{const_name numeral}, [n]) => inst [] [xs, n] feval_simps_11
+ | _ => inst [] [xs, c] feval_simps_1)
+ | (@{const_name FVar}, [n]) =>
+ transitive' (inst [] [xs, n] feval_simps_2) (args2 nth_el_conv')
+ | (@{const_name FAdd}, [a, b]) =>
+ transitive' (inst [] [xs, a, b] feval_simps_3)
+ (cong2 (args2 conv) (args2 conv))
+ | (@{const_name FSub}, [a, b]) =>
+ transitive' (inst [] [xs, a, b] feval_simps_4)
+ (cong2 (args2 conv) (args2 conv))
+ | (@{const_name FMul}, [a, b]) =>
+ transitive' (inst [] [xs, a, b] feval_simps_5)
+ (cong2 (args2 conv) (args2 conv))
+ | (@{const_name FNeg}, [a]) =>
+ transitive' (inst [] [xs, a] feval_simps_6)
+ (cong1 (args2 conv))
+ | (@{const_name FDiv}, [a, b]) =>
+ transitive' (inst [] [xs, a, b] feval_simps_7)
+ (cong2 (args2 conv) (args2 conv))
+ | (@{const_name FPow}, [a, n]) =>
+ transitive' (inst [] [xs, a, n] feval_simps_8)
+ (cong2 (args2 conv) Thm.reflexive))
+ in conv end;
+
+fun peval_conv (rls as
+ (_,
+ [peval_simps_1, peval_simps_2, peval_simps_3,
+ peval_simps_4, peval_simps_5, peval_simps_6,
+ peval_simps_7, peval_simps_8, peval_simps_9,
+ peval_simps_10, peval_simps_11],
+ _, _, _)) =
+ let
+ val nth_el_conv' = nth_el_conv rls;
+
+ fun conv xs x = (case strip_app x of
+ (@{const_name PExpr1}, [e]) => (case strip_app e of
+ (@{const_name PCnst}, [c]) => (case strip_numeral c of
+ (@{const_name zero_class.zero}, _) => inst [] [xs] peval_simps_8
+ | (@{const_name one_class.one}, _) => inst [] [xs] peval_simps_9
+ | (@{const_name numeral}, [n]) => inst [] [xs, n] peval_simps_10
+ | (@{const_name uminus}, [n]) => inst [] [xs, n] peval_simps_11
+ | _ => inst [] [xs, c] peval_simps_1)
+ | (@{const_name PVar}, [n]) =>
+ transitive' (inst [] [xs, n] peval_simps_2) (args2 nth_el_conv')
+ | (@{const_name PAdd}, [a, b]) =>
+ transitive' (inst [] [xs, a, b] peval_simps_3)
+ (cong2 (args2 conv) (args2 conv))
+ | (@{const_name PSub}, [a, b]) =>
+ transitive' (inst [] [xs, a, b] peval_simps_4)
+ (cong2 (args2 conv) (args2 conv))
+ | (@{const_name PNeg}, [a]) =>
+ transitive' (inst [] [xs, a] peval_simps_5)
+ (cong1 (args2 conv)))
+ | (@{const_name PExpr2}, [e]) => (case strip_app e of
+ (@{const_name PMul}, [a, b]) =>
+ transitive' (inst [] [xs, a, b] peval_simps_6)
+ (cong2 (args2 conv) (args2 conv))
+ | (@{const_name PPow}, [a, n]) =>
+ transitive' (inst [] [xs, a, n] peval_simps_7)
+ (cong2 (args2 conv) Thm.reflexive)))
+ in conv end;
+
+fun nonzero_conv (rls as
+ (_, _,
+ [nonzero_Nil, nonzero_Cons, nonzero_singleton],
+ _, _)) =
+ let
+ val peval_conv' = peval_conv rls;
+
+ fun conv xs qs = (case strip_app qs of
+ (@{const_name Nil}, []) => inst [] [xs] nonzero_Nil
+ | (@{const_name Cons}, [p, ps]) => (case Thm.term_of ps of
+ Const (@{const_name Nil}, _) =>
+ transitive' (inst [] [xs, p] nonzero_singleton)
+ (cong1 (cong2 (args2 peval_conv') Thm.reflexive))
+ | _ => transitive' (inst [] [xs, p, ps] nonzero_Cons)
+ (cong2 (cong1 (cong2 (args2 peval_conv') Thm.reflexive)) (args2 conv))))
+ in conv end;
+
+val cv = Code_Evaluation.static_conv
+ {ctxt = @{context},
+ consts =
+ [@{const_name nat_of_integer},
+ @{const_name fnorm}, @{const_name field_codegen_aux}]};
+
+fun field_tac in_prem ctxt =
+ SUBGOAL (fn (g, i) =>
+ let
+ val (prems, concl) = Logic.strip_horn g;
+ fun find_eq s = (case s of
+ (_ $ (Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t $ u)) =>
+ (case (field_struct t, field_struct u) of
+ (SOME R, _) => SOME ((t, u), R, T, NONE, mk_in_carrier ctxt R [], reif_fexpr)
+ | (_, SOME R) => SOME ((t, u), R, T, NONE, mk_in_carrier ctxt R [], reif_fexpr)
+ | _ =>
+ if Sign.of_sort (Proof_Context.theory_of ctxt) (T, @{sort field})
+ then SOME ((t, u), mk_ring T, T, SOME T, K @{thm in_carrier_trivial}, reif_fexpr')
+ else NONE)
+ | _ => NONE);
+ val ((t, u), R, T, optT, mkic, reif) =
+ (case get_first find_eq
+ (if in_prem then prems else [concl]) of
+ SOME q => q
+ | NONE => error "cannot determine field");
+ val rls as (_, _, _, _, feval_eq) =
+ get_field_simps ctxt (Option.map (Thm.ctyp_of ctxt) optT) R;
+ val xs = [] |> Term.add_frees t |> Term.add_frees u |> filter (equal T o snd);
+ val cxs = Thm.cterm_of ctxt (HOLogic.mk_list T (map Free xs));
+ val ce = Thm.cterm_of ctxt (reif xs t);
+ val ce' = Thm.cterm_of ctxt (reif xs u);
+ val fnorm = cv ctxt
+ (Thm.apply @{cterm fnorm} (Thm.apply (Thm.apply @{cterm FSub} ce) ce'));
+ val (_, [n, dc]) = strip_app (Thm.rhs_of fnorm);
+ val (_, [_, c]) = strip_app dc;
+ val th =
+ Conv.fconv_rule (Conv.concl_conv 1 (Conv.arg_conv
+ (binop_conv
+ (binop_conv
+ (K (feval_conv rls cxs ce)) (K (feval_conv rls cxs ce')))
+ (Conv.arg1_conv (K (peval_conv rls cxs n))))))
+ ([mkic xs,
+ mk_obj_eq fnorm,
+ mk_obj_eq (nonzero_conv rls cxs c) RS @{thm iffD2}] MRS
+ feval_eq);
+ val th' = Drule.rotate_prems 1
+ (th RS (if in_prem then @{thm iffD1} else @{thm iffD2}));
+ in
+ if in_prem then
+ dresolve_tac ctxt [th'] 1 THEN defer_tac 1
+ else
+ resolve_tac ctxt [th'] 1
+ end);
+
+end
+*}
+
+context field begin
+
+local_setup {*
+Local_Theory.declaration {syntax = false, pervasive = false}
+ (fn phi => Field_Tac.Field_Simps.map (Ring_Tac.insert_rules Field_Tac.eq_field_simps
+ (Morphism.term phi @{term R},
+ (Morphism.fact phi @{thms feval.simps [meta] feval_Cnst [meta]},
+ Morphism.fact phi @{thms peval.simps [meta] peval_Cnst [meta]},
+ Morphism.fact phi @{thms nonzero.simps [meta] nonzero_singleton [meta]},
+ singleton (Morphism.fact phi) @{thm nth_el_Cons [meta]},
+ singleton (Morphism.fact phi) @{thm feval_eq}))))
+*}
+
+end
+
+method_setup field = {*
+ Scan.lift (Args.mode "prems") -- Attrib.thms >> (fn (in_prem, thms) => fn ctxt =>
+ SIMPLE_METHOD' (Field_Tac.field_tac in_prem ctxt THEN' Ring_Tac.ring_tac in_prem thms ctxt))
+*} "reduce equations over fields to equations over rings"
+
+end
--- a/src/HOL/Decision_Procs/commutative_ring_tac.ML Sun Jan 29 11:49:48 2017 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,106 +0,0 @@
-(* Title: HOL/Decision_Procs/commutative_ring_tac.ML
- Author: Amine Chaieb
-
-Tactic for solving equalities over commutative rings.
-*)
-
-signature COMMUTATIVE_RING_TAC =
-sig
- val tac: Proof.context -> int -> tactic
-end
-
-structure Commutative_Ring_Tac: COMMUTATIVE_RING_TAC =
-struct
-
-(* Zero and One of the commutative ring *)
-fun cring_zero T = Const (@{const_name Groups.zero}, T);
-fun cring_one T = Const (@{const_name Groups.one}, T);
-
-(* reification functions *)
-(* add two polynom expressions *)
-fun polT t = Type (@{type_name Commutative_Ring.pol}, [t]);
-fun polexT t = Type (@{type_name Commutative_Ring.polex}, [t]);
-
-(* pol *)
-fun pol_Pc t =
- Const (@{const_name Commutative_Ring.pol.Pc}, t --> polT t);
-fun pol_Pinj t =
- Const (@{const_name Commutative_Ring.pol.Pinj}, HOLogic.natT --> polT t --> polT t);
-fun pol_PX t =
- Const (@{const_name Commutative_Ring.pol.PX}, polT t --> HOLogic.natT --> polT t --> polT t);
-
-(* polex *)
-fun polex_add t =
- Const (@{const_name Commutative_Ring.polex.Add}, polexT t --> polexT t --> polexT t);
-fun polex_sub t =
- Const (@{const_name Commutative_Ring.polex.Sub}, polexT t --> polexT t --> polexT t);
-fun polex_mul t =
- Const (@{const_name Commutative_Ring.polex.Mul}, polexT t --> polexT t --> polexT t);
-fun polex_neg t =
- Const (@{const_name Commutative_Ring.polex.Neg}, polexT t --> polexT t);
-fun polex_pol t =
- Const (@{const_name Commutative_Ring.polex.Pol}, polT t --> polexT t);
-fun polex_pow t =
- Const (@{const_name Commutative_Ring.polex.Pow}, polexT t --> HOLogic.natT --> polexT t);
-
-(* reification of polynoms : primitive cring expressions *)
-fun reif_pol T vs (t as Free _) =
- let
- val one = @{term "1::nat"};
- val i = find_index (fn t' => t' = t) vs
- in
- if i = 0 then
- pol_PX T $ (pol_Pc T $ cring_one T) $ one $ (pol_Pc T $ cring_zero T)
- else
- pol_Pinj T $ HOLogic.mk_nat i $
- (pol_PX T $ (pol_Pc T $ cring_one T) $ one $ (pol_Pc T $ cring_zero T))
- end
- | reif_pol T _ t = pol_Pc T $ t;
-
-(* reification of polynom expressions *)
-fun reif_polex T vs (Const (@{const_name Groups.plus}, _) $ a $ b) =
- polex_add T $ reif_polex T vs a $ reif_polex T vs b
- | reif_polex T vs (Const (@{const_name Groups.minus}, _) $ a $ b) =
- polex_sub T $ reif_polex T vs a $ reif_polex T vs b
- | reif_polex T vs (Const (@{const_name Groups.times}, _) $ a $ b) =
- polex_mul T $ reif_polex T vs a $ reif_polex T vs b
- | reif_polex T vs (Const (@{const_name Groups.uminus}, _) $ a) =
- polex_neg T $ reif_polex T vs a
- | reif_polex T vs (Const (@{const_name Power.power}, _) $ a $ n) =
- polex_pow T $ reif_polex T vs a $ n
- | reif_polex T vs t = polex_pol T $ reif_pol T vs t;
-
-(* reification of the equation *)
-val cr_sort = @{sort comm_ring_1};
-
-fun reif_eq ctxt (eq as Const (@{const_name HOL.eq}, Type (@{type_name fun}, [T, _])) $ lhs $ rhs) =
- if Sign.of_sort (Proof_Context.theory_of ctxt) (T, cr_sort) then
- let
- val fs = Misc_Legacy.term_frees eq;
- val cvs = Thm.cterm_of ctxt (HOLogic.mk_list T fs);
- val clhs = Thm.cterm_of ctxt (reif_polex T fs lhs);
- val crhs = Thm.cterm_of ctxt (reif_polex T fs rhs);
- val ca = Thm.ctyp_of ctxt T;
- in (ca, cvs, clhs, crhs) end
- else error ("reif_eq: not an equation over " ^ Syntax.string_of_sort ctxt cr_sort)
- | reif_eq _ _ = error "reif_eq: not an equation";
-
-(* The cring tactic *)
-(* Attention: You have to make sure that no t^0 is in the goal!! *)
-(* Use simply rewriting t^0 = 1 *)
-val cring_simps =
- @{thms mkPX_def mkPinj_def sub_def power_add even_iff_mod_2_eq_zero pow_if power_add [symmetric]};
-
-fun tac ctxt = SUBGOAL (fn (g, i) =>
- let
- val cring_ctxt = ctxt addsimps cring_simps; (*FIXME really the full simpset!?*)
- val (ca, cvs, clhs, crhs) = reif_eq ctxt (HOLogic.dest_Trueprop g);
- val norm_eq_th = (* may collapse to True *)
- simplify cring_ctxt (Thm.instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq});
- in
- cut_tac norm_eq_th i
- THEN (simp_tac cring_ctxt i)
- THEN TRY(simp_tac cring_ctxt i)
- end);
-
-end;
--- a/src/HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy Sun Jan 29 11:49:48 2017 +0100
+++ b/src/HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy Sun Jan 29 11:59:48 2017 +0100
@@ -1,49 +1,134 @@
-(* Author: Bernhard Haeupler *)
+(* Title: HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy
+ Author: Bernhard Haeupler, Stefan Berghofer
+*)
-section \<open>Some examples demonstrating the comm-ring method\<close>
+section \<open>Some examples demonstrating the ring and field methods\<close>
theory Commutative_Ring_Ex
-imports "../Commutative_Ring"
+imports "../Reflective_Field"
begin
-lemma "4*(x::int)^5*y^3*x^2*3 + x*z + 3^5 = 12*x^7*y^3 + z*x + 243"
- by comm_ring
+lemma "4 * (x::int) ^ 5 * y ^ 3 * x ^ 2 * 3 + x * z + 3 ^ 5 = 12 * x ^ 7 * y ^ 3 + z * x + 243"
+ by ring
+
+lemma (in cring)
+ assumes "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R"
+ shows "\<guillemotleft>4\<guillemotright> \<otimes> x (^) (5::nat) \<otimes> y (^) (3::nat) \<otimes> x (^) (2::nat) \<otimes> \<guillemotleft>3\<guillemotright> \<oplus> x \<otimes> z \<oplus> \<guillemotleft>3\<guillemotright> (^) (5::nat) =
+ \<guillemotleft>12\<guillemotright> \<otimes> x (^) (7::nat) \<otimes> y (^) (3::nat) \<oplus> z \<otimes> x \<oplus> \<guillemotleft>243\<guillemotright>"
+ by ring
+
+lemma "((x::int) + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y"
+ by ring
-lemma "((x::int) + y)^2 = x^2 + y^2 + 2*x*y"
- by comm_ring
+lemma (in cring)
+ assumes "x \<in> carrier R" "y \<in> carrier R"
+ shows "(x \<oplus> y) (^) (2::nat) = x (^) (2::nat) \<oplus> y (^) (2::nat) \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> x \<otimes> y"
+ by ring
+
+lemma "((x::int) + y) ^ 3 = x ^ 3 + y ^ 3 + 3 * x ^ 2 * y + 3 * y ^ 2 * x"
+ by ring
-lemma "((x::int) + y)^3 = x^3 + y^3 + 3*x^2*y + 3*y^2*x"
- by comm_ring
+lemma (in cring)
+ assumes "x \<in> carrier R" "y \<in> carrier R"
+ shows "(x \<oplus> y) (^) (3::nat) =
+ x (^) (3::nat) \<oplus> y (^) (3::nat) \<oplus> \<guillemotleft>3\<guillemotright> \<otimes> x (^) (2::nat) \<otimes> y \<oplus> \<guillemotleft>3\<guillemotright> \<otimes> y (^) (2::nat) \<otimes> x"
+ by ring
+
+lemma "((x::int) - y) ^ 3 = x ^ 3 + 3 * x * y ^ 2 + (- 3) * y * x ^ 2 - y ^ 3"
+ by ring
-lemma "((x::int) - y)^3 = x^3 + 3*x*y^2 + (-3)*y*x^2 - y^3"
- by comm_ring
+lemma (in cring)
+ assumes "x \<in> carrier R" "y \<in> carrier R"
+ shows "(x \<ominus> y) (^) (3::nat) =
+ x (^) (3::nat) \<oplus> \<guillemotleft>3\<guillemotright> \<otimes> x \<otimes> y (^) (2::nat) \<oplus> (\<ominus> \<guillemotleft>3\<guillemotright>) \<otimes> y \<otimes> x (^) (2::nat) \<ominus> y (^) (3::nat)"
+ by ring
+
+lemma "((x::int) - y) ^ 2 = x ^ 2 + y ^ 2 - 2 * x * y"
+ by ring
+
+lemma (in cring)
+ assumes "x \<in> carrier R" "y \<in> carrier R"
+ shows "(x \<ominus> y) (^) (2::nat) = x (^) (2::nat) \<oplus> y (^) (2::nat) \<ominus> \<guillemotleft>2\<guillemotright> \<otimes> x \<otimes> y"
+ by ring
-lemma "((x::int) - y)^2 = x^2 + y^2 - 2*x*y"
- by comm_ring
+lemma " ((a::int) + b + c) ^ 2 = a ^ 2 + b ^ 2 + c ^ 2 + 2 * a * b + 2 * b * c + 2 * a * c"
+ by ring
+
+lemma (in cring)
+ assumes "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R"
+ shows " (a \<oplus> b \<oplus> c) (^) (2::nat) =
+ a (^) (2::nat) \<oplus> b (^) (2::nat) \<oplus> c (^) (2::nat) \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> a \<otimes> b \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> b \<otimes> c \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> a \<otimes> c"
+ by ring
-lemma " ((a::int) + b + c)^2 = a^2 + b^2 + c^2 + 2*a*b + 2*b*c + 2*a*c"
- by comm_ring
+lemma "((a::int) - b - c) ^ 2 = a ^ 2 + b ^ 2 + c ^ 2 - 2 * a * b + 2 * b * c - 2 * a * c"
+ by ring
+
+lemma (in cring)
+ assumes "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R"
+ shows "(a \<ominus> b \<ominus> c) (^) (2::nat) =
+ a (^) (2::nat) \<oplus> b (^) (2::nat) \<oplus> c (^) (2::nat) \<ominus> \<guillemotleft>2\<guillemotright> \<otimes> a \<otimes> b \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> b \<otimes> c \<ominus> \<guillemotleft>2\<guillemotright> \<otimes> a \<otimes> c"
+ by ring
-lemma "((a::int) - b - c)^2 = a^2 + b^2 + c^2 - 2*a*b + 2*b*c - 2*a*c"
- by comm_ring
+lemma "(a::int) * b + a * c = a * (b + c)"
+ by ring
+
+lemma (in cring)
+ assumes "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R"
+ shows "a \<otimes> b \<oplus> a \<otimes> c = a \<otimes> (b \<oplus> c)"
+ by ring
+
+lemma "(a::int) ^ 2 - b ^ 2 = (a - b) * (a + b)"
+ by ring
-lemma "(a::int)*b + a*c = a*(b+c)"
- by comm_ring
+lemma (in cring)
+ assumes "a \<in> carrier R" "b \<in> carrier R"
+ shows "a (^) (2::nat) \<ominus> b (^) (2::nat) = (a \<ominus> b) \<otimes> (a \<oplus> b)"
+ by ring
+
+lemma "(a::int) ^ 3 - b ^ 3 = (a - b) * (a ^ 2 + a * b + b ^ 2)"
+ by ring
-lemma "(a::int)^2 - b^2 = (a - b) * (a + b)"
- by comm_ring
+lemma (in cring)
+ assumes "a \<in> carrier R" "b \<in> carrier R"
+ shows "a (^) (3::nat) \<ominus> b (^) (3::nat) = (a \<ominus> b) \<otimes> (a (^) (2::nat) \<oplus> a \<otimes> b \<oplus> b (^) (2::nat))"
+ by ring
+
+lemma "(a::int) ^ 3 + b ^ 3 = (a + b) * (a ^ 2 - a * b + b ^ 2)"
+ by ring
-lemma "(a::int)^3 - b^3 = (a - b) * (a^2 + a*b + b^2)"
- by comm_ring
+lemma (in cring)
+ assumes "a \<in> carrier R" "b \<in> carrier R"
+ shows "a (^) (3::nat) \<oplus> b (^) (3::nat) = (a \<oplus> b) \<otimes> (a (^) (2::nat) \<ominus> a \<otimes> b \<oplus> b (^) (2::nat))"
+ by ring
-lemma "(a::int)^3 + b^3 = (a + b) * (a^2 - a*b + b^2)"
- by comm_ring
+lemma "(a::int) ^ 4 - b ^ 4 = (a - b) * (a + b) * (a ^ 2 + b ^ 2)"
+ by ring
+
+lemma (in cring)
+ assumes "a \<in> carrier R" "b \<in> carrier R"
+ shows "a (^) (4::nat) \<ominus> b (^) (4::nat) = (a \<ominus> b) \<otimes> (a \<oplus> b) \<otimes> (a (^) (2::nat) \<oplus> b (^) (2::nat))"
+ by ring
-lemma "(a::int)^4 - b^4 = (a - b) * (a + b)*(a^2 + b^2)"
- by comm_ring
+lemma "(a::int) ^ 10 - b ^ 10 =
+ (a - b) * (a ^ 9 + a ^ 8 * b + a ^ 7 * b ^ 2 + a ^ 6 * b ^ 3 + a ^ 5 * b ^ 4 +
+ a ^ 4 * b ^ 5 + a ^ 3 * b ^ 6 + a ^ 2 * b ^ 7 + a * b ^ 8 + b ^ 9)"
+ by ring
-lemma "(a::int)^10 - b^10 =
- (a - b) * (a^9 + a^8*b + a^7*b^2 + a^6*b^3 + a^5*b^4 + a^4*b^5 + a^3*b^6 + a^2*b^7 + a*b^8 + b^9)"
- by comm_ring
+lemma (in cring)
+ assumes "a \<in> carrier R" "b \<in> carrier R"
+ shows "a (^) (10::nat) \<ominus> b (^) (10::nat) =
+ (a \<ominus> b) \<otimes> (a (^) (9::nat) \<oplus> a (^) (8::nat) \<otimes> b \<oplus> a (^) (7::nat) \<otimes> b (^) (2::nat) \<oplus>
+ a (^) (6::nat) \<otimes> b (^) (3::nat) \<oplus> a (^) (5::nat) \<otimes> b (^) (4::nat) \<oplus>
+ a (^) (4::nat) \<otimes> b (^) (5::nat) \<oplus> a (^) (3::nat) \<otimes> b (^) (6::nat) \<oplus>
+ a (^) (2::nat) \<otimes> b (^) (7::nat) \<oplus> a \<otimes> b (^) (8::nat) \<oplus> b (^) (9::nat))"
+ by ring
+
+lemma "(x::'a::field) \<noteq> 0 \<Longrightarrow> (1 - 1 / x) * x - x + 1 = 0"
+ by field
+
+lemma (in field)
+ assumes "x \<in> carrier R"
+ shows "x \<noteq> \<zero> \<Longrightarrow> (\<one> \<ominus> \<one> \<oslash> x) \<otimes> x \<ominus> x \<oplus> \<one> = \<zero>"
+ by field
end