src/HOL/Library/Abstract_Rat.thy
changeset 31952 40501bb2d57c
parent 31706 1db0c8f235fb
child 31967 81dbc693143b
     1.1 --- a/src/HOL/Library/Abstract_Rat.thy	Tue Jul 07 07:56:24 2009 +0200
     1.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Tue Jul 07 17:39:51 2009 +0200
     1.3 @@ -30,8 +30,8 @@
     1.4    (let g = gcd a b 
     1.5     in if b > 0 then (a div g, b div g) else (- (a div g), - (b div g)))))"
     1.6  
     1.7 -declare int_gcd_dvd1[presburger]
     1.8 -declare int_gcd_dvd2[presburger]
     1.9 +declare gcd_dvd1_int[presburger]
    1.10 +declare gcd_dvd2_int[presburger]
    1.11  lemma normNum_isnormNum [simp]: "isnormNum (normNum x)"
    1.12  proof -
    1.13    have " \<exists> a b. x = (a,b)" by auto
    1.14 @@ -43,7 +43,7 @@
    1.15      let ?a' = "a div ?g"
    1.16      let ?b' = "b div ?g"
    1.17      let ?g' = "gcd ?a' ?b'"
    1.18 -    from anz bnz have "?g \<noteq> 0" by simp  with int_gcd_ge_0[of a b] 
    1.19 +    from anz bnz have "?g \<noteq> 0" by simp  with gcd_ge_0_int[of a b] 
    1.20      have gpos: "?g > 0"  by arith
    1.21      have gdvd: "?g dvd a" "?g dvd b" by arith+ 
    1.22      from zdvd_mult_div_cancel[OF gdvd(1)] zdvd_mult_div_cancel[OF gdvd(2)]
    1.23 @@ -51,7 +51,7 @@
    1.24      have nz':"?a' \<noteq> 0" "?b' \<noteq> 0"
    1.25        by - (rule notI, simp)+
    1.26      from anz bnz have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith 
    1.27 -    from int_div_gcd_coprime[OF stupid] have gp1: "?g' = 1" .
    1.28 +    from div_gcd_coprime_int[OF stupid] have gp1: "?g' = 1" .
    1.29      from bnz have "b < 0 \<or> b > 0" by arith
    1.30      moreover
    1.31      {assume b: "b > 0"
    1.32 @@ -137,7 +137,7 @@
    1.33  
    1.34  lemma Ninv_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (Ninv x)"
    1.35    by (simp add: Ninv_def isnormNum_def split_def)
    1.36 -    (cases "fst x = 0", auto simp add: int_gcd_commute)
    1.37 +    (cases "fst x = 0", auto simp add: gcd_commute_int)
    1.38  
    1.39  lemma isnormNum_int[simp]: 
    1.40    "isnormNum 0\<^sub>N" "isnormNum (1::int)\<^sub>N" "i \<noteq> 0 \<Longrightarrow> isnormNum i\<^sub>N"
    1.41 @@ -203,7 +203,7 @@
    1.42      from prems have eq:"a * b' = a'*b" 
    1.43        by (simp add: INum_def  eq_divide_eq divide_eq_eq of_int_mult[symmetric] del: of_int_mult)
    1.44      from prems have gcd1: "gcd a b = 1" "gcd b a = 1" "gcd a' b' = 1" "gcd b' a' = 1"       
    1.45 -      by (simp_all add: isnormNum_def add: int_gcd_commute)
    1.46 +      by (simp_all add: isnormNum_def add: gcd_commute_int)
    1.47      from eq have raw_dvd: "a dvd a'*b" "b dvd b'*a" "a' dvd a*b'" "b' dvd b*a'"
    1.48        apply - 
    1.49        apply algebra
    1.50 @@ -211,8 +211,8 @@
    1.51        apply simp
    1.52        apply algebra
    1.53        done
    1.54 -    from zdvd_dvd_eq[OF bz int_coprime_dvd_mult[OF gcd1(2) raw_dvd(2)]
    1.55 -      int_coprime_dvd_mult[OF gcd1(4) raw_dvd(4)]]
    1.56 +    from zdvd_dvd_eq[OF bz coprime_dvd_mult_int[OF gcd1(2) raw_dvd(2)]
    1.57 +      coprime_dvd_mult_int[OF gcd1(4) raw_dvd(4)]]
    1.58        have eq1: "b = b'" using pos by arith  
    1.59        with eq have "a = a'" using pos by simp
    1.60        with eq1 have ?rhs by simp}
    1.61 @@ -297,8 +297,8 @@
    1.62        let ?g = "gcd (a * b' + b * a') (b*b')"
    1.63        have gz: "?g \<noteq> 0" using z by simp
    1.64        have ?thesis using aa' bb' z gz
    1.65 -	of_int_div[where ?'a = 'a, OF gz int_gcd_dvd1[where x="a * b' + b * a'" and y="b*b'"]]	of_int_div[where ?'a = 'a,
    1.66 -	OF gz int_gcd_dvd2[where x="a * b' + b * a'" and y="b*b'"]]
    1.67 +	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.68 +	OF gz gcd_dvd2_int[where x="a * b' + b * a'" and y="b*b'"]]
    1.69  	by (simp add: x y Nadd_def INum_def normNum_def Let_def add_divide_distrib)}
    1.70      ultimately have ?thesis using aa' bb' 
    1.71        by (simp add: Nadd_def INum_def normNum_def x y Let_def) }
    1.72 @@ -319,8 +319,8 @@
    1.73    {assume z: "a \<noteq> 0" "a' \<noteq> 0" "b \<noteq> 0" "b' \<noteq> 0"
    1.74      let ?g="gcd (a*a') (b*b')"
    1.75      have gz: "?g \<noteq> 0" using z by simp
    1.76 -    from z of_int_div[where ?'a = 'a, OF gz int_gcd_dvd1[where x="a*a'" and y="b*b'"]] 
    1.77 -      of_int_div[where ?'a = 'a , OF gz int_gcd_dvd2[where x="a*a'" and y="b*b'"]] 
    1.78 +    from z of_int_div[where ?'a = 'a, OF gz gcd_dvd1_int[where x="a*a'" and y="b*b'"]] 
    1.79 +      of_int_div[where ?'a = 'a , OF gz gcd_dvd2_int[where x="a*a'" and y="b*b'"]] 
    1.80      have ?thesis by (simp add: Nmul_def x y Let_def INum_def)}
    1.81    ultimately show ?thesis by blast
    1.82  qed
    1.83 @@ -478,7 +478,7 @@
    1.84  qed
    1.85  
    1.86  lemma Nmul_commute: "isnormNum x \<Longrightarrow> isnormNum y \<Longrightarrow> x *\<^sub>N y = y *\<^sub>N x"
    1.87 -  by (simp add: Nmul_def split_def Let_def int_gcd_commute mult_commute)
    1.88 +  by (simp add: Nmul_def split_def Let_def gcd_commute_int mult_commute)
    1.89  
    1.90  lemma Nmul_assoc:
    1.91    assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"