src/HOL/Library/Abstract_Rat.thy
 changeset 32456 341c83339aeb parent 31967 81dbc693143b child 32960 69916a850301
```     1.1 --- a/src/HOL/Library/Abstract_Rat.thy	Sat Aug 29 14:31:39 2009 +0200
1.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Mon Aug 31 14:09:42 2009 +0200
1.3 @@ -189,14 +189,9 @@
1.4    have "\<exists> a b a' b'. x = (a,b) \<and> y = (a',b')" by auto
1.5    then obtain a b a' b' where xy[simp]: "x = (a,b)" "y=(a',b')" by blast
1.6    assume H: ?lhs
1.7 -  {assume "a = 0 \<or> b = 0 \<or> a' = 0 \<or> b' = 0" hence ?rhs
1.8 -      using na nb H
1.9 -      apply (simp add: INum_def split_def isnormNum_def)
1.10 -      apply (cases "a = 0", simp_all)
1.11 -      apply (cases "b = 0", simp_all)
1.12 -      apply (cases "a' = 0", simp_all)
1.13 -      apply (cases "a' = 0", simp_all add: of_int_eq_0_iff)
1.14 -      done}
1.15 +  {assume "a = 0 \<or> b = 0 \<or> a' = 0 \<or> b' = 0"
1.16 +    hence ?rhs using na nb H
1.17 +      by (simp add: INum_def split_def isnormNum_def split: split_if_asm)}
1.18    moreover
1.19    { assume az: "a \<noteq> 0" and bz: "b \<noteq> 0" and a'z: "a'\<noteq>0" and b'z: "b'\<noteq>0"
1.20      from az bz a'z b'z na nb have pos: "b > 0" "b' > 0" by (simp_all add: isnormNum_def)
1.21 @@ -517,10 +512,7 @@
1.22      have n0: "isnormNum 0\<^sub>N" by simp
1.23      show ?thesis using nx ny
1.24        apply (simp only: isnormNum_unique[where ?'a = 'a, OF  Nmul_normN[OF nx ny] n0, symmetric] Nmul[where ?'a = 'a])
1.25 -      apply (simp add: INum_def split_def isnormNum_def fst_conv snd_conv)
1.26 -      apply (cases "a=0",simp_all)
1.27 -      apply (cases "a'=0",simp_all)
1.28 -      done
1.29 +      by (simp add: INum_def split_def isnormNum_def fst_conv snd_conv split: split_if_asm)
1.30    }
1.31  qed
1.32  lemma Nneg_Nneg[simp]: "~\<^sub>N (~\<^sub>N c) = c"
```