fix more looping simp rules
authorhuffman
Wed Feb 17 10:30:36 2010 -0800 (2010-02-17)
changeset 3517561255c81da01
parent 35174 e15040ae75d7
child 35176 3b9762ad372d
fix more looping simp rules
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/Ramsey.thy
src/HOL/Library/Word.thy
src/HOL/Library/Zorn.thy
     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Wed Feb 17 10:00:22 2010 -0800
     1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Wed Feb 17 10:30:36 2010 -0800
     1.3 @@ -2864,8 +2864,8 @@
     1.4      then have nz: "pochhammer (1 + b - of_nat n) n \<noteq> 0" 
     1.5        by (auto simp add: algebra_simps)
     1.6      
     1.7 -    from nz kn have nz': "pochhammer (1 + b - of_nat n) k \<noteq> 0" 
     1.8 -      by (simp add: pochhammer_neq_0_mono)
     1.9 +    from nz kn [simplified] have nz': "pochhammer (1 + b - of_nat n) k \<noteq> 0" 
    1.10 +      by (rule pochhammer_neq_0_mono)
    1.11      {assume k0: "k = 0 \<or> n =0" 
    1.12        then have "b gchoose (n - k) = (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)" 
    1.13          using kn
     2.1 --- a/src/HOL/Library/Ramsey.thy	Wed Feb 17 10:00:22 2010 -0800
     2.2 +++ b/src/HOL/Library/Ramsey.thy	Wed Feb 17 10:30:36 2010 -0800
     2.3 @@ -111,7 +111,7 @@
     2.4          have infYx': "infinite (Yx-{yx'})" using fields px by auto
     2.5          with fields px yx' Suc.prems
     2.6          have partfx': "part r s (Yx - {yx'}) (f \<circ> insert yx')"
     2.7 -          by (simp add: o_def part_Suc_imp_part part_subset [where ?YY=YY]) 
     2.8 +          by (simp add: o_def part_Suc_imp_part part_subset [where YY=YY and Y=Yx])
     2.9          from Suc.hyps [OF infYx' partfx']
    2.10          obtain Y' and t'
    2.11          where Y': "Y' \<subseteq> Yx - {yx'}"  "infinite Y'"  "t' < s"
     3.1 --- a/src/HOL/Library/Word.thy	Wed Feb 17 10:00:22 2010 -0800
     3.2 +++ b/src/HOL/Library/Word.thy	Wed Feb 17 10:30:36 2010 -0800
     3.3 @@ -980,7 +980,8 @@
     3.4    fix xs
     3.5    assume "length (norm_signed (\<zero>#xs)) = Suc (length xs)"
     3.6    thus "norm_signed (\<zero>#xs) = \<zero>#xs"
     3.7 -    by (simp add: norm_signed_Cons norm_unsigned_equal split: split_if_asm)
     3.8 +    by (simp add: norm_signed_Cons norm_unsigned_equal [THEN eqTrueI]
     3.9 +             split: split_if_asm)
    3.10  next
    3.11    fix xs
    3.12    assume "length (norm_signed (\<one>#xs)) = Suc (length xs)"
     4.1 --- a/src/HOL/Library/Zorn.thy	Wed Feb 17 10:00:22 2010 -0800
     4.2 +++ b/src/HOL/Library/Zorn.thy	Wed Feb 17 10:30:36 2010 -0800
     4.3 @@ -333,7 +333,7 @@
     4.4  
     4.5  lemma antisym_init_seg_of:
     4.6    "r initial_segment_of s \<Longrightarrow> s initial_segment_of r \<Longrightarrow> r=s"
     4.7 -by(auto simp:init_seg_of_def)
     4.8 +unfolding init_seg_of_def by safe
     4.9  
    4.10  lemma Chain_init_seg_of_Union:
    4.11    "R \<in> Chain init_seg_of \<Longrightarrow> r\<in>R \<Longrightarrow> r initial_segment_of \<Union>R"