--- 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)
--- 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<count M x --> countm M P \<noteq> 0"
+lemma pos_count_imp_pos_countm [rule_format (no_asm)]: "!!P. P(x) ==> 0<count M x --> 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<count M x --> 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
--- 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
--- 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