author wenzelm Thu Oct 16 22:44:24 2008 +0200 (2008-10-16) changeset 28615 4c8fa015ec7f parent 28614 1f301440c97b child 28616 ac1da69fbc5a
explicit SORT_CONSTRAINT for proofs depending implicitly on certain sorts;
```     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.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.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.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.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.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.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.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
```