# HG changeset patch # User nipkow # Date 1193172505 -7200 # Node ID aa847439803022b7743d0e025a2fe5aa6701a679 # Parent 72fcf0832cfe7fbe6750a69897bf57966fa4e7a4 changed back from ~=0 to >0 diff -r 72fcf0832cfe -r aa8474398030 src/HOLCF/IOA/NTP/Impl.thy --- a/src/HOLCF/IOA/NTP/Impl.thy Tue Oct 23 14:00:06 2007 +0200 +++ b/src/HOLCF/IOA/NTP/Impl.thy Tue Oct 23 22:48:25 2007 +0200 @@ -168,7 +168,7 @@ apply (rule impI) apply (erule conjE)+ apply (simp add: Impl.hdr_sum_def Multiset.count_def Multiset.countm_nonempty_def - Multiset.delm_nonempty_def neq0_conv split add: split_if) + Multiset.delm_nonempty_def split add: split_if) apply (rule allI) apply (rule conjI) apply (rule impI) diff -r 72fcf0832cfe -r aa8474398030 src/HOLCF/IOA/NTP/Multiset.thy --- a/src/HOLCF/IOA/NTP/Multiset.thy Tue Oct 23 14:00:06 2007 +0200 +++ b/src/HOLCF/IOA/NTP/Multiset.thy Tue Oct 23 22:48:25 2007 +0200 @@ -75,17 +75,17 @@ done -lemma pos_count_imp_pos_countm [rule_format (no_asm)]: "!!P. P(x) ==> 0 countm M P \ 0" +lemma pos_count_imp_pos_countm [rule_format (no_asm)]: "!!P. P(x) ==> 0 countm M P > 0" apply (rule_tac M = "M" in Multiset.induction) apply (simp (no_asm) add: Multiset.delm_empty_def Multiset.count_def Multiset.countm_empty_def) - apply (simp (no_asm_simp) add: Multiset.count_def Multiset.delm_nonempty_def Multiset.countm_nonempty_def) + apply (simp add: Multiset.count_def Multiset.delm_nonempty_def Multiset.countm_nonempty_def) done lemma countm_done_delm: "!!P. P(x) ==> 0 countm (delm M x) P = countm M P - 1" apply (rule_tac M = "M" in Multiset.induction) apply (simp (no_asm) add: Multiset.delm_empty_def Multiset.countm_empty_def) - apply (simp (no_asm_simp) add: neq0_conv count_addm_simp Multiset.delm_nonempty_def Multiset.countm_nonempty_def pos_count_imp_pos_countm) + apply (simp (no_asm_simp) add: count_addm_simp Multiset.delm_nonempty_def Multiset.countm_nonempty_def pos_count_imp_pos_countm) apply auto done diff -r 72fcf0832cfe -r aa8474398030 src/HOLCF/IsaMakefile --- a/src/HOLCF/IsaMakefile Tue Oct 23 14:00:06 2007 +0200 +++ b/src/HOLCF/IsaMakefile Tue Oct 23 22:48:25 2007 +0200 @@ -34,7 +34,7 @@ Tools/domain/domain_extender.ML Tools/domain/domain_axioms.ML \ Tools/domain/domain_library.ML Tools/domain/domain_syntax.ML \ Tools/domain/domain_theorems.ML Tools/fixrec_package.ML \ - Tools/pcpodef_package.ML Tr.thy Up.thy document/root.tex ex/Stream.thy \ + Tools/pcpodef_package.ML Tr.thy Up.thy document/root.tex \ holcf_logic.ML @$(ISATOOL) usedir -b -g true -r $(OUT)/HOL HOLCF @@ -52,7 +52,7 @@ HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz -$(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF ex/Dagstuhl.thy \ +$(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF ex/Stream.thy ex/Dagstuhl.thy \ ex/Dnat.thy ex/Fix2.thy ex/Focus_ex.thy ex/Hoare.thy ex/Loop.thy \ ex/ROOT.ML ex/Fixrec_ex.thy ../HOL/Library/Nat_Infinity.thy @$(ISATOOL) usedir $(OUT)/HOLCF ex diff -r 72fcf0832cfe -r aa8474398030 src/HOLCF/ex/Stream.thy --- a/src/HOLCF/ex/Stream.thy Tue Oct 23 14:00:06 2007 +0200 +++ b/src/HOLCF/ex/Stream.thy Tue Oct 23 22:48:25 2007 +0200 @@ -693,8 +693,7 @@ lemma take_i_rt_prefix_lemma: "[| stream_take n$s1 << stream_take n$s2; i_rt n s1 << i_rt n s2 |] ==> s1 << s2" apply (case_tac "n=0",simp) -apply (insert neq0_conv [of n]) -apply (insert not0_implies_Suc [of n],auto) +apply (auto) apply (subgoal_tac "stream_take 0$s1 << stream_take 0$s2 & i_rt 0 s1 << i_rt 0 s2") defer 1