fix proofs involving ile_def
authorhuffman
Wed Feb 20 18:28:16 2008 +0100 (2008-02-20)
changeset 261022ae572207783
parent 26101 a657683e902a
child 26103 b9fc7ac04c8b
fix proofs involving ile_def
src/HOLCF/FOCUS/Stream_adm.thy
src/HOLCF/ex/Stream.thy
     1.1 --- a/src/HOLCF/FOCUS/Stream_adm.thy	Wed Feb 20 14:52:38 2008 +0100
     1.2 +++ b/src/HOLCF/FOCUS/Stream_adm.thy	Wed Feb 20 18:28:16 2008 +0100
     1.3 @@ -54,7 +54,7 @@
     1.4  apply (subst slen_infinite)
     1.5  apply (erule thin_rl)
     1.6  apply (drule spec)
     1.7 -apply (fold ile_def)
     1.8 +apply (unfold linorder_not_less)
     1.9  apply (erule ile_iless_trans [THEN Infty_eq [THEN iffD1]])
    1.10  apply (simp)
    1.11  done
    1.12 @@ -142,7 +142,7 @@
    1.13  apply (erule conjE)
    1.14  apply (case_tac "#x < Fin i")
    1.15  apply ( fast)
    1.16 -apply (fold ile_def)
    1.17 +apply (unfold linorder_not_less)
    1.18  apply (drule (1) mp)
    1.19  apply (erule all_dupE, drule mp, rule refl_less)
    1.20  apply (erule ssubst)
     2.1 --- a/src/HOLCF/ex/Stream.thy	Wed Feb 20 14:52:38 2008 +0100
     2.2 +++ b/src/HOLCF/ex/Stream.thy	Wed Feb 20 18:28:16 2008 +0100
     2.3 @@ -433,7 +433,7 @@
     2.4  by (simp add: inat_defs split:inat_splits)
     2.5  
     2.6  lemma slen_take_eq_rev: "(#x <= Fin n) = (stream_take n\<cdot>x = x)"
     2.7 -by (simp add: ile_def slen_take_eq)
     2.8 +by (simp add: linorder_not_less [symmetric] slen_take_eq)
     2.9  
    2.10  lemma slen_take_lemma1: "#x = Fin n ==> stream_take n\<cdot>x = x"
    2.11  by (rule slen_take_eq_rev [THEN iffD1], auto)