src/HOL/Library/Abstract_Rat.thy
changeset 41528 276078f01ada
parent 36411 4cd87067791e
child 42463 f270e3e18be5
     1.1 --- a/src/HOL/Library/Abstract_Rat.thy	Wed Jan 12 16:41:49 2011 +0100
     1.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Wed Jan 12 17:14:27 2011 +0100
     1.3 @@ -44,7 +44,7 @@
     1.4      let ?b' = "b div ?g"
     1.5      let ?g' = "gcd ?a' ?b'"
     1.6      from anz bnz have "?g \<noteq> 0" by simp  with gcd_ge_0_int[of a b] 
     1.7 -    have gpos: "?g > 0"  by arith
     1.8 +    have gpos: "?g > 0" by arith
     1.9      have gdvd: "?g dvd a" "?g dvd b" by arith+ 
    1.10      from zdvd_mult_div_cancel[OF gdvd(1)] zdvd_mult_div_cancel[OF gdvd(2)]
    1.11      anz bnz
    1.12 @@ -140,7 +140,7 @@
    1.13      (cases "fst x = 0", auto simp add: gcd_commute_int)
    1.14  
    1.15  lemma isnormNum_int[simp]: 
    1.16 -  "isnormNum 0\<^sub>N" "isnormNum (1::int)\<^sub>N" "i \<noteq> 0 \<Longrightarrow> isnormNum i\<^sub>N"
    1.17 +  "isnormNum 0\<^sub>N" "isnormNum ((1::int)\<^sub>N)" "i \<noteq> 0 \<Longrightarrow> isnormNum (i\<^sub>N)"
    1.18    by (simp_all add: isnormNum_def)
    1.19  
    1.20  
    1.21 @@ -179,7 +179,7 @@
    1.22  definition
    1.23    "INum = (\<lambda>(a,b). of_int a / of_int b)"
    1.24  
    1.25 -lemma INum_int [simp]: "INum i\<^sub>N = ((of_int i) ::'a::field)" "INum 0\<^sub>N = (0::'a::field)"
    1.26 +lemma INum_int [simp]: "INum (i\<^sub>N) = ((of_int i) ::'a::field)" "INum 0\<^sub>N = (0::'a::field)"
    1.27    by (simp_all add: INum_def)
    1.28  
    1.29  lemma isnormNum_unique[simp]: 
    1.30 @@ -195,9 +195,9 @@
    1.31    moreover
    1.32    { assume az: "a \<noteq> 0" and bz: "b \<noteq> 0" and a'z: "a'\<noteq>0" and b'z: "b'\<noteq>0"
    1.33      from az bz a'z b'z na nb have pos: "b > 0" "b' > 0" by (simp_all add: isnormNum_def)
    1.34 -    from prems have eq:"a * b' = a'*b" 
    1.35 +    from H bz b'z have eq:"a * b' = a'*b" 
    1.36        by (simp add: INum_def  eq_divide_eq divide_eq_eq of_int_mult[symmetric] del: of_int_mult)
    1.37 -    from prems have gcd1: "gcd a b = 1" "gcd b a = 1" "gcd a' b' = 1" "gcd b' a' = 1"       
    1.38 +    from az a'z na nb have gcd1: "gcd a b = 1" "gcd b a = 1" "gcd a' b' = 1" "gcd b' a' = 1"       
    1.39        by (simp_all add: isnormNum_def add: gcd_commute_int)
    1.40      from eq have raw_dvd: "a dvd a'*b" "b dvd b'*a" "a' dvd a*b'" "b' dvd b*a'"
    1.41        apply - 
    1.42 @@ -208,7 +208,7 @@
    1.43        done
    1.44      from zdvd_antisym_abs[OF coprime_dvd_mult_int[OF gcd1(2) raw_dvd(2)]
    1.45        coprime_dvd_mult_int[OF gcd1(4) raw_dvd(4)]]
    1.46 -      have eq1: "b = b'" using pos by arith  
    1.47 +      have eq1: "b = b'" using pos by arith
    1.48        with eq have "a = a'" using pos by simp
    1.49        with eq1 have ?rhs by simp}
    1.50    ultimately show ?rhs by blast
    1.51 @@ -225,7 +225,6 @@
    1.52      of_int (x div d) + (of_int (x mod d)) / ((of_int d)::'a)"
    1.53  proof -
    1.54    assume "d ~= 0"
    1.55 -  hence dz: "of_int d \<noteq> (0::'a)" by (simp add: of_int_eq_0_iff)
    1.56    let ?t = "of_int (x div d) * ((of_int d)::'a) + of_int(x mod d)"
    1.57    let ?f = "\<lambda>x. x / of_int d"
    1.58    have "x = (x div d) * d + x mod d"
    1.59 @@ -234,7 +233,7 @@
    1.60      by (simp only: of_int_mult[symmetric] of_int_add [symmetric])
    1.61    then have "of_int x / of_int d = ?t / of_int d" 
    1.62      using cong[OF refl[of ?f] eq] by simp
    1.63 -  then show ?thesis by (simp add: add_divide_distrib algebra_simps prems)
    1.64 +  then show ?thesis by (simp add: add_divide_distrib algebra_simps `d ~= 0`)
    1.65  qed
    1.66  
    1.67  lemma of_int_div: "(d::int) ~= 0 ==> d dvd n ==>
    1.68 @@ -294,9 +293,9 @@
    1.69        have ?thesis using aa' bb' z gz
    1.70          of_int_div[where ?'a = 'a, OF gz gcd_dvd1_int[where x="a * b' + b * a'" and y="b*b'"]]  of_int_div[where ?'a = 'a,
    1.71          OF gz gcd_dvd2_int[where x="a * b' + b * a'" and y="b*b'"]]
    1.72 -        by (simp add: x y Nadd_def INum_def normNum_def Let_def add_divide_distrib)}
    1.73 +        by (simp add: Nadd_def INum_def normNum_def Let_def add_divide_distrib)}
    1.74      ultimately have ?thesis using aa' bb' 
    1.75 -      by (simp add: Nadd_def INum_def normNum_def x y Let_def) }
    1.76 +      by (simp add: Nadd_def INum_def normNum_def Let_def) }
    1.77    ultimately show ?thesis by blast
    1.78  qed
    1.79  
    1.80 @@ -512,7 +511,7 @@
    1.81      have n0: "isnormNum 0\<^sub>N" by simp
    1.82      show ?thesis using nx ny 
    1.83        apply (simp only: isnormNum_unique[where ?'a = 'a, OF  Nmul_normN[OF nx ny] n0, symmetric] Nmul[where ?'a = 'a])
    1.84 -      by (simp add: INum_def split_def isnormNum_def fst_conv snd_conv split: split_if_asm)
    1.85 +      by (simp add: INum_def split_def isnormNum_def split: split_if_asm)
    1.86    }
    1.87  qed
    1.88  lemma Nneg_Nneg[simp]: "~\<^sub>N (~\<^sub>N c) = c"
    1.89 @@ -520,7 +519,7 @@
    1.90  
    1.91  lemma Nmul1[simp]: 
    1.92    "isnormNum c \<Longrightarrow> 1\<^sub>N *\<^sub>N c = c" 
    1.93 -  "isnormNum c \<Longrightarrow> c *\<^sub>N 1\<^sub>N  = c" 
    1.94 +  "isnormNum c \<Longrightarrow> c *\<^sub>N (1\<^sub>N) = c" 
    1.95    apply (simp_all add: Nmul_def Let_def split_def isnormNum_def)
    1.96    apply (cases "fst c = 0", simp_all, cases c, simp_all)+
    1.97    done