explicit SORT_CONSTRAINT for proofs depending implicitly on certain sorts;
authorwenzelm
Thu Oct 16 22:44:24 2008 +0200 (2008-10-16)
changeset 286154c8fa015ec7f
parent 28614 1f301440c97b
child 28616 ac1da69fbc5a
explicit SORT_CONSTRAINT for proofs depending implicitly on certain sorts;
src/HOL/Library/Abstract_Rat.thy
     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