merged
authorchaieb
Sat Jul 04 15:19:29 2009 +0200 (2009-07-04)
changeset 3196436156921f5e5
parent 31963 663a725dc339
child 31965 f6d9798b13f1
merged
src/HOL/Library/Abstract_Rat.thy
     1.1 --- a/src/HOL/Library/Abstract_Rat.thy	Thu Jul 02 13:48:39 2009 +0200
     1.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Sat Jul 04 15:19:29 2009 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Abstract rational numbers *}
     1.5  
     1.6  theory Abstract_Rat
     1.7 -imports GCD Complex_Main
     1.8 +imports GCD Main
     1.9  begin
    1.10  
    1.11  types Num = "int \<times> int"
    1.12 @@ -404,14 +404,16 @@
    1.13  qed
    1.14  
    1.15  lemma Nadd_commute:
    1.16 +  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
    1.17    shows "x +\<^sub>N y = y +\<^sub>N x"
    1.18  proof-
    1.19    have n: "isnormNum (x +\<^sub>N y)" "isnormNum (y +\<^sub>N x)" by simp_all
    1.20 -  have "(INum (x +\<^sub>N y)::rat) = INum (y +\<^sub>N x)" by simp
    1.21 +  have "(INum (x +\<^sub>N y)::'a) = INum (y +\<^sub>N x)" by simp
    1.22    with isnormNum_unique[OF n] show ?thesis by simp
    1.23  qed
    1.24  
    1.25  lemma [simp]:
    1.26 +  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
    1.27    shows "(0, b) +\<^sub>N y = normNum y"
    1.28      and "(a, 0) +\<^sub>N y = normNum y" 
    1.29      and "x +\<^sub>N (0, b) = normNum x"
    1.30 @@ -423,17 +425,19 @@
    1.31    done
    1.32  
    1.33  lemma normNum_nilpotent_aux[simp]:
    1.34 +  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
    1.35    assumes nx: "isnormNum x" 
    1.36    shows "normNum x = x"
    1.37  proof-
    1.38    let ?a = "normNum x"
    1.39    have n: "isnormNum ?a" by simp
    1.40 -  have th:"INum ?a = (INum x :: 'a::{ring_char_0, division_by_zero, field})" by simp
    1.41 +  have th:"INum ?a = (INum x ::'a)" by simp
    1.42    with isnormNum_unique[OF n nx]  
    1.43    show ?thesis by simp
    1.44  qed
    1.45  
    1.46  lemma normNum_nilpotent[simp]:
    1.47 +  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
    1.48    shows "normNum (normNum x) = normNum x"
    1.49    by simp
    1.50  
    1.51 @@ -441,31 +445,35 @@
    1.52    by (simp_all add: normNum_def)
    1.53  
    1.54  lemma normNum_Nadd:
    1.55 +  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
    1.56    shows "normNum (x +\<^sub>N y) = x +\<^sub>N y" by simp
    1.57  
    1.58  lemma Nadd_normNum1[simp]:
    1.59 +  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
    1.60    shows "normNum x +\<^sub>N y = x +\<^sub>N y"
    1.61  proof-
    1.62    have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)" by simp_all
    1.63 -  have "INum (normNum x +\<^sub>N y) = INum x + (INum y :: real)" by simp
    1.64 +  have "INum (normNum x +\<^sub>N y) = INum x + (INum y :: 'a)" by simp
    1.65    also have "\<dots> = INum (x +\<^sub>N y)" by simp
    1.66    finally show ?thesis using isnormNum_unique[OF n] by simp
    1.67  qed
    1.68  
    1.69  lemma Nadd_normNum2[simp]:
    1.70 +  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
    1.71    shows "x +\<^sub>N normNum y = x +\<^sub>N y"
    1.72  proof-
    1.73    have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)" by simp_all
    1.74 -  have "INum (x +\<^sub>N normNum y) = INum x + (INum y :: real)" by simp
    1.75 +  have "INum (x +\<^sub>N normNum y) = INum x + (INum y :: 'a)" by simp
    1.76    also have "\<dots> = INum (x +\<^sub>N y)" by simp
    1.77    finally show ?thesis using isnormNum_unique[OF n] by simp
    1.78  qed
    1.79  
    1.80  lemma Nadd_assoc:
    1.81 +  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
    1.82    shows "x +\<^sub>N y +\<^sub>N z = x +\<^sub>N (y +\<^sub>N z)"
    1.83  proof-
    1.84    have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))" by simp_all
    1.85 -  have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: real)" by simp
    1.86 +  have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp
    1.87    with isnormNum_unique[OF n] show ?thesis by simp
    1.88  qed
    1.89  
    1.90 @@ -473,22 +481,24 @@
    1.91    by (simp add: Nmul_def split_def Let_def int_gcd_commute mult_commute)
    1.92  
    1.93  lemma Nmul_assoc:
    1.94 +  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
    1.95    assumes nx: "isnormNum x" and ny:"isnormNum y" and nz:"isnormNum z"
    1.96    shows "x *\<^sub>N y *\<^sub>N z = x *\<^sub>N (y *\<^sub>N z)"
    1.97  proof-
    1.98    from nx ny nz have n: "isnormNum (x *\<^sub>N y *\<^sub>N z)" "isnormNum (x *\<^sub>N (y *\<^sub>N z))" 
    1.99      by simp_all
   1.100 -  have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: real)" by simp
   1.101 +  have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp
   1.102    with isnormNum_unique[OF n] show ?thesis by simp
   1.103  qed
   1.104  
   1.105  lemma Nsub0:
   1.106 +  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   1.107    assumes x: "isnormNum x" and y:"isnormNum y" shows "(x -\<^sub>N y = 0\<^sub>N) = (x = y)"
   1.108  proof-
   1.109    { fix h :: 'a
   1.110 -    from isnormNum_unique[where 'a = real, OF Nsub_normN[OF y], where y="0\<^sub>N"] 
   1.111 -    have "(x -\<^sub>N y = 0\<^sub>N) = (INum (x -\<^sub>N y) = (INum 0\<^sub>N :: real)) " by simp
   1.112 -    also have "\<dots> = (INum x = (INum y :: real))" by simp
   1.113 +    from isnormNum_unique[where 'a = 'a, OF Nsub_normN[OF y], where y="0\<^sub>N"] 
   1.114 +    have "(x -\<^sub>N y = 0\<^sub>N) = (INum (x -\<^sub>N y) = (INum 0\<^sub>N :: 'a)) " by simp
   1.115 +    also have "\<dots> = (INum x = (INum y :: 'a))" by simp
   1.116      also have "\<dots> = (x = y)" using x y by simp
   1.117      finally show ?thesis . }
   1.118  qed