src/HOL/Library/Abstract_Rat.thy
changeset 32960 69916a850301
parent 32456 341c83339aeb
child 33657 a4179bf442d1
     1.1 --- a/src/HOL/Library/Abstract_Rat.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -56,18 +56,18 @@
     1.4      moreover
     1.5      {assume b: "b > 0"
     1.6        from b have "?b' \<ge> 0" 
     1.7 -	by (presburger add: pos_imp_zdiv_nonneg_iff[OF gpos])  
     1.8 +        by (presburger add: pos_imp_zdiv_nonneg_iff[OF gpos])  
     1.9        with nz' have b': "?b' > 0" by arith 
    1.10        from b b' anz bnz nz' gp1 have ?thesis 
    1.11 -	by (simp add: isnormNum_def normNum_def Let_def split_def fst_conv snd_conv)}
    1.12 +        by (simp add: isnormNum_def normNum_def Let_def split_def fst_conv snd_conv)}
    1.13      moreover {assume b: "b < 0"
    1.14        {assume b': "?b' \<ge> 0" 
    1.15 -	from gpos have th: "?g \<ge> 0" by arith
    1.16 -	from mult_nonneg_nonneg[OF th b'] zdvd_mult_div_cancel[OF gdvd(2)]
    1.17 -	have False using b by arith }
    1.18 +        from gpos have th: "?g \<ge> 0" by arith
    1.19 +        from mult_nonneg_nonneg[OF th b'] zdvd_mult_div_cancel[OF gdvd(2)]
    1.20 +        have False using b by arith }
    1.21        hence b': "?b' < 0" by (presburger add: linorder_not_le[symmetric]) 
    1.22        from anz bnz nz' b b' gp1 have ?thesis 
    1.23 -	by (simp add: isnormNum_def normNum_def Let_def split_def)}
    1.24 +        by (simp add: isnormNum_def normNum_def Let_def split_def)}
    1.25      ultimately have ?thesis by blast
    1.26    }
    1.27    ultimately show ?thesis by blast
    1.28 @@ -287,14 +287,14 @@
    1.29        hence "of_int b' * of_int a / (of_int b * of_int b') + of_int b * of_int a' / (of_int b * of_int b') = ?z"  by (simp add:add_divide_distrib) 
    1.30        hence th: "of_int a / of_int b + of_int a' / of_int b' = ?z" using bb' aa' by simp 
    1.31        from z aa' bb' have ?thesis 
    1.32 -	by (simp add: th Nadd_def normNum_def INum_def split_def)}
    1.33 +        by (simp add: th Nadd_def normNum_def INum_def split_def)}
    1.34      moreover {assume z: "a * b' + b * a' \<noteq> 0"
    1.35        let ?g = "gcd (a * b' + b * a') (b*b')"
    1.36        have gz: "?g \<noteq> 0" using z by simp
    1.37        have ?thesis using aa' bb' z gz
    1.38 -	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.39 -	OF gz gcd_dvd2_int[where x="a * b' + b * a'" and y="b*b'"]]
    1.40 -	by (simp add: x y Nadd_def INum_def normNum_def Let_def add_divide_distrib)}
    1.41 +        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.42 +        OF gz gcd_dvd2_int[where x="a * b' + b * a'" and y="b*b'"]]
    1.43 +        by (simp add: x y Nadd_def INum_def normNum_def Let_def add_divide_distrib)}
    1.44      ultimately have ?thesis using aa' bb' 
    1.45        by (simp add: Nadd_def INum_def normNum_def x y Let_def) }
    1.46    ultimately show ?thesis by blast