--- a/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy Thu Jul 05 16:11:33 2012 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy Thu Jul 05 16:53:29 2012 +0200
@@ -64,7 +64,10 @@
axiomatization where
finiteR_mksch:
- "Finite (mksch A B$tr$x$y) --> Finite tr"
+ "Finite (mksch A B$tr$x$y) \<Longrightarrow> Finite tr"
+
+lemma finiteR_mksch': "\<not> Finite tr \<Longrightarrow> \<not> Finite (mksch A B$tr$x$y)"
+ by (blast intro: finiteR_mksch)
declaration {* fn _ => Simplifier.map_ss (Simplifier.set_mksym (K (K NONE))) *}
@@ -507,7 +510,7 @@
apply (subgoal_tac "schA=UU")
apply (simp (no_asm_simp))
(* first side: mksch = UU *)
-apply (auto intro!: ForallQFilterPUU finiteR_mksch [THEN mp, COMP rev_contrapos] ForallBnAmksch)[1]
+apply (auto intro!: ForallQFilterPUU finiteR_mksch' ForallBnAmksch)[1]
(* schA = UU *)
apply (erule_tac A = "A" in LastActExtimplUU)
apply (simp (no_asm_simp))
@@ -726,7 +729,7 @@
apply (subgoal_tac "schB=UU")
apply (simp (no_asm_simp))
(* first side: mksch = UU *)
-apply (force intro!: ForallQFilterPUU finiteR_mksch [THEN mp, COMP rev_contrapos] ForallAnBmksch)
+apply (force intro!: ForallQFilterPUU finiteR_mksch' ForallAnBmksch)
(* schA = UU *)
apply (erule_tac A = "B" in LastActExtimplUU)
apply (simp (no_asm_simp))
--- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Thu Jul 05 16:11:33 2012 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Thu Jul 05 16:53:29 2012 +0200
@@ -651,7 +651,7 @@
(* inverse of ForallnPFilterPnil *)
-lemma FilternPnilForallP1: "!! ys . Filter P$ys = nil -->
+lemma FilternPnilForallP [rule_format]: "Filter P$ys = nil -->
(Forall (%x. ~P x) ys & Finite ys)"
apply (rule_tac x="ys" in Seq_induct)
(* adm *)
@@ -663,27 +663,32 @@
apply simp
done
-lemmas FilternPnilForallP = FilternPnilForallP1 [THEN mp]
-(* inverse of ForallnPFilterPUU. proved apply 2 lemmas because of adm problems *)
-
-lemma FilterUU_nFinite_lemma1: "Finite ys ==> Filter P$ys ~= UU"
-apply (erule Seq_Finite_ind, simp_all)
-done
-
-lemma FilterUU_nFinite_lemma2: "~ Forall (%x. ~P x) ys --> Filter P$ys ~= UU"
-apply (rule_tac x="ys" in Seq_induct)
-apply (simp add: Forall_def sforall_def)
-apply simp_all
-done
+(* inverse of ForallnPFilterPUU *)
lemma FilternPUUForallP:
- "Filter P$ys = UU ==> (Forall (%x. ~P x) ys & ~Finite ys)"
-apply (rule conjI)
-apply (cut_tac FilterUU_nFinite_lemma2 [THEN mp, COMP rev_contrapos])
-apply auto
-apply (blast dest!: FilterUU_nFinite_lemma1)
-done
+ assumes "Filter P$ys = UU"
+ shows "Forall (%x. ~P x) ys & ~Finite ys"
+proof
+ show "Forall (%x. ~P x) ys"
+ proof (rule classical)
+ assume "\<not> ?thesis"
+ then have "Filter P$ys ~= UU"
+ apply (rule rev_mp)
+ apply (induct ys rule: Seq_induct)
+ apply (simp add: Forall_def sforall_def)
+ apply simp_all
+ done
+ with assms show ?thesis by contradiction
+ qed
+ show "~ Finite ys"
+ proof
+ assume "Finite ys"
+ then have "Filter P$ys ~= UU"
+ by (rule Seq_Finite_ind) simp_all
+ with assms show False by contradiction
+ qed
+qed
lemma ForallQFilterPnil: