# HG changeset patch
# User wenzelm
# Date 1341500009 -7200
# Node ID 1440a3103af0907de924d355bfd24021c2b41cad
# Parent  cab79d456044d8d8a84ce8d6e9a23635e9787f90
tuned proofs -- eliminated old-fashioned COMP and rev_contrapos;

diff -r cab79d456044 -r 1440a3103af0 src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy
--- 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))
diff -r cab79d456044 -r 1440a3103af0 src/HOL/HOLCF/IOA/meta_theory/Sequence.thy
--- 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: