1.1 --- a/src/HOL/Library/Abstract_Rat.thy Thu Oct 16 22:44:22 2008 +0200
1.2 +++ b/src/HOL/Library/Abstract_Rat.thy Thu Oct 16 22:44:24 2008 +0200
1.3 @@ -404,95 +404,125 @@
1.4 finally show ?thesis by (simp add: Nle_def)
1.5 qed
1.6
1.7 -lemma Nadd_commute: "x +\<^sub>N y = y +\<^sub>N x"
1.8 +lemma Nadd_commute:
1.9 + assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
1.10 + shows "x +\<^sub>N y = y +\<^sub>N x"
1.11 proof-
1.12 have n: "isnormNum (x +\<^sub>N y)" "isnormNum (y +\<^sub>N x)" by simp_all
1.13 - have "(INum (x +\<^sub>N y)::'a :: {ring_char_0,division_by_zero,field}) = INum (y +\<^sub>N x)" by simp
1.14 + have "(INum (x +\<^sub>N y)::'a) = INum (y +\<^sub>N x)" by simp
1.15 with isnormNum_unique[OF n] show ?thesis by simp
1.16 qed
1.17
1.18 -lemma[simp]: "(0, b) +\<^sub>N y = normNum y" "(a, 0) +\<^sub>N y = normNum y"
1.19 - "x +\<^sub>N (0, b) = normNum x" "x +\<^sub>N (a, 0) = normNum x"
1.20 - apply (simp add: Nadd_def split_def, simp add: Nadd_def split_def)
1.21 - apply (subst Nadd_commute,simp add: Nadd_def split_def)
1.22 - apply (subst Nadd_commute,simp add: Nadd_def split_def)
1.23 +lemma [simp]:
1.24 + assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
1.25 + shows "(0, b) +\<^sub>N y = normNum y"
1.26 + and "(a, 0) +\<^sub>N y = normNum y"
1.27 + and "x +\<^sub>N (0, b) = normNum x"
1.28 + and "x +\<^sub>N (a, 0) = normNum x"
1.29 + apply (simp add: Nadd_def split_def)
1.30 + apply (simp add: Nadd_def split_def)
1.31 + apply (subst Nadd_commute, simp add: Nadd_def split_def)
1.32 + apply (subst Nadd_commute, simp add: Nadd_def split_def)
1.33 done
1.34
1.35 -lemma normNum_nilpotent_aux[simp]: assumes nx: "isnormNum x"
1.36 +lemma normNum_nilpotent_aux[simp]:
1.37 + assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
1.38 + assumes nx: "isnormNum x"
1.39 shows "normNum x = x"
1.40 proof-
1.41 let ?a = "normNum x"
1.42 have n: "isnormNum ?a" by simp
1.43 - have th:"INum ?a = (INum x ::'a :: {ring_char_0, division_by_zero,field})" by simp
1.44 + have th:"INum ?a = (INum x ::'a)" by simp
1.45 with isnormNum_unique[OF n nx]
1.46 show ?thesis by simp
1.47 qed
1.48
1.49 -lemma normNum_nilpotent[simp]: "normNum (normNum x) = normNum x"
1.50 +lemma normNum_nilpotent[simp]:
1.51 + assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
1.52 + shows "normNum (normNum x) = normNum x"
1.53 by simp
1.54 +
1.55 lemma normNum0[simp]: "normNum (0,b) = 0\<^sub>N" "normNum (a,0) = 0\<^sub>N"
1.56 by (simp_all add: normNum_def)
1.57 -lemma normNum_Nadd: "normNum (x +\<^sub>N y) = x +\<^sub>N y" by simp
1.58 -lemma Nadd_normNum1[simp]: "normNum x +\<^sub>N y = x +\<^sub>N y"
1.59 +
1.60 +lemma normNum_Nadd:
1.61 + assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
1.62 + shows "normNum (x +\<^sub>N y) = x +\<^sub>N y" by simp
1.63 +
1.64 +lemma Nadd_normNum1[simp]:
1.65 + assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
1.66 + shows "normNum x +\<^sub>N y = x +\<^sub>N y"
1.67 proof-
1.68 have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)" by simp_all
1.69 - have "INum (normNum x +\<^sub>N y) = INum x + (INum y :: 'a :: {ring_char_0, division_by_zero,field})" by simp
1.70 - also have "\<dots> = INum (x +\<^sub>N y)" by simp
1.71 - finally show ?thesis using isnormNum_unique[OF n] by simp
1.72 -qed
1.73 -lemma Nadd_normNum2[simp]: "x +\<^sub>N normNum y = x +\<^sub>N y"
1.74 -proof-
1.75 - have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)" by simp_all
1.76 - have "INum (x +\<^sub>N normNum y) = INum x + (INum y :: 'a :: {ring_char_0, division_by_zero,field})" by simp
1.77 + have "INum (normNum x +\<^sub>N y) = INum x + (INum y :: 'a)" by simp
1.78 also have "\<dots> = INum (x +\<^sub>N y)" by simp
1.79 finally show ?thesis using isnormNum_unique[OF n] by simp
1.80 qed
1.81
1.82 -lemma Nadd_assoc: "x +\<^sub>N y +\<^sub>N z = x +\<^sub>N (y +\<^sub>N z)"
1.83 +lemma Nadd_normNum2[simp]:
1.84 + assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
1.85 + shows "x +\<^sub>N normNum y = x +\<^sub>N y"
1.86 +proof-
1.87 + have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)" by simp_all
1.88 + have "INum (x +\<^sub>N normNum y) = INum x + (INum y :: 'a)" by simp
1.89 + also have "\<dots> = INum (x +\<^sub>N y)" by simp
1.90 + finally show ?thesis using isnormNum_unique[OF n] by simp
1.91 +qed
1.92 +
1.93 +lemma Nadd_assoc:
1.94 + assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
1.95 + shows "x +\<^sub>N y +\<^sub>N z = x +\<^sub>N (y +\<^sub>N z)"
1.96 proof-
1.97 have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))" by simp_all
1.98 - have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a :: {ring_char_0, division_by_zero,field})" by simp
1.99 + have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp
1.100 with isnormNum_unique[OF n] show ?thesis by simp
1.101 qed
1.102
1.103 lemma Nmul_commute: "isnormNum x \<Longrightarrow> isnormNum y \<Longrightarrow> x *\<^sub>N y = y *\<^sub>N x"
1.104 by (simp add: Nmul_def split_def Let_def zgcd_commute mult_commute)
1.105
1.106 -lemma Nmul_assoc: assumes nx: "isnormNum x" and ny:"isnormNum y" and nz:"isnormNum z"
1.107 +lemma Nmul_assoc:
1.108 + assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
1.109 + assumes nx: "isnormNum x" and ny:"isnormNum y" and nz:"isnormNum z"
1.110 shows "x *\<^sub>N y *\<^sub>N z = x *\<^sub>N (y *\<^sub>N z)"
1.111 proof-
1.112 from nx ny nz have n: "isnormNum (x *\<^sub>N y *\<^sub>N z)" "isnormNum (x *\<^sub>N (y *\<^sub>N z))"
1.113 by simp_all
1.114 - have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a :: {ring_char_0, division_by_zero,field})" by simp
1.115 + have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp
1.116 with isnormNum_unique[OF n] show ?thesis by simp
1.117 qed
1.118
1.119 -lemma Nsub0: assumes x: "isnormNum x" and y:"isnormNum y" shows "(x -\<^sub>N y = 0\<^sub>N) = (x = y)"
1.120 +lemma Nsub0:
1.121 + assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
1.122 + assumes x: "isnormNum x" and y:"isnormNum y" shows "(x -\<^sub>N y = 0\<^sub>N) = (x = y)"
1.123 proof-
1.124 - {fix h :: "'a :: {ring_char_0,division_by_zero,ordered_field}"
1.125 - from isnormNum_unique[where ?'a = 'a, OF Nsub_normN[OF y], where y="0\<^sub>N"]
1.126 + { fix h :: 'a
1.127 + from isnormNum_unique[where 'a = 'a, OF Nsub_normN[OF y], where y="0\<^sub>N"]
1.128 have "(x -\<^sub>N y = 0\<^sub>N) = (INum (x -\<^sub>N y) = (INum 0\<^sub>N :: 'a)) " by simp
1.129 - also have "\<dots> = (INum x = (INum y:: 'a))" by simp
1.130 + also have "\<dots> = (INum x = (INum y :: 'a))" by simp
1.131 also have "\<dots> = (x = y)" using x y by simp
1.132 - finally show ?thesis .}
1.133 + finally show ?thesis . }
1.134 qed
1.135
1.136 lemma Nmul0[simp]: "c *\<^sub>N 0\<^sub>N = 0\<^sub>N" " 0\<^sub>N *\<^sub>N c = 0\<^sub>N"
1.137 by (simp_all add: Nmul_def Let_def split_def)
1.138
1.139 -lemma Nmul_eq0[simp]: assumes nx:"isnormNum x" and ny: "isnormNum y"
1.140 +lemma Nmul_eq0[simp]:
1.141 + assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
1.142 + assumes nx:"isnormNum x" and ny: "isnormNum y"
1.143 shows "(x*\<^sub>N y = 0\<^sub>N) = (x = 0\<^sub>N \<or> y = 0\<^sub>N)"
1.144 proof-
1.145 - {fix h :: "'a :: {ring_char_0,division_by_zero,ordered_field}"
1.146 - have " \<exists> a b a' b'. x = (a,b) \<and> y= (a',b')" by auto
1.147 - then obtain a b a' b' where xy[simp]: "x = (a,b)" "y = (a',b')" by blast
1.148 - have n0: "isnormNum 0\<^sub>N" by simp
1.149 - show ?thesis using nx ny
1.150 - apply (simp only: isnormNum_unique[where ?'a = 'a, OF Nmul_normN[OF nx ny] n0, symmetric] Nmul[where ?'a = 'a])
1.151 - apply (simp add: INum_def split_def isnormNum_def fst_conv snd_conv)
1.152 - apply (cases "a=0",simp_all)
1.153 - apply (cases "a'=0",simp_all)
1.154 - done }
1.155 + { fix h :: 'a
1.156 + have " \<exists> a b a' b'. x = (a,b) \<and> y= (a',b')" by auto
1.157 + then obtain a b a' b' where xy[simp]: "x = (a,b)" "y = (a',b')" by blast
1.158 + have n0: "isnormNum 0\<^sub>N" by simp
1.159 + show ?thesis using nx ny
1.160 + apply (simp only: isnormNum_unique[where ?'a = 'a, OF Nmul_normN[OF nx ny] n0, symmetric] Nmul[where ?'a = 'a])
1.161 + apply (simp add: INum_def split_def isnormNum_def fst_conv snd_conv)
1.162 + apply (cases "a=0",simp_all)
1.163 + apply (cases "a'=0",simp_all)
1.164 + done
1.165 + }
1.166 qed
1.167 lemma Nneg_Nneg[simp]: "~\<^sub>N (~\<^sub>N c) = c"
1.168 by (simp add: Nneg_def split_def)
1.169 @@ -501,6 +531,7 @@
1.170 "isnormNum c \<Longrightarrow> 1\<^sub>N *\<^sub>N c = c"
1.171 "isnormNum c \<Longrightarrow> c *\<^sub>N 1\<^sub>N = c"
1.172 apply (simp_all add: Nmul_def Let_def split_def isnormNum_def)
1.173 - by (cases "fst c = 0", simp_all,cases c, simp_all)+
1.174 + apply (cases "fst c = 0", simp_all, cases c, simp_all)+
1.175 + done
1.176
1.177 -end
1.178 \ No newline at end of file
1.179 +end