# HG changeset patch
# User huffman
# Date 1288823484 25200
# Node ID 483a4876e428d2004fb5c039992a2da533ad4c39
# Parent  5f37c39648665152554583c6382c72182d18c53f
move a few admissibility lemmas into FOCUS/Stream_adm.thy

diff -r 5f37c3964866 -r 483a4876e428 src/HOLCF/Adm.thy
--- a/src/HOLCF/Adm.thy	Wed Nov 03 15:03:16 2010 -0700
+++ b/src/HOLCF/Adm.thy	Wed Nov 03 15:31:24 2010 -0700
@@ -29,16 +29,6 @@
 lemma triv_admI: "\<forall>x. P x \<Longrightarrow> adm P"
 by (rule admI, erule spec)
 
-text {* improved admissibility introduction *}
-
-lemma admI2:
-  "(\<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i); \<forall>i. \<exists>j>i. Y i \<noteq> Y j \<and> Y i \<sqsubseteq> Y j\<rbrakk> 
-    \<Longrightarrow> P (\<Squnion>i. Y i)) \<Longrightarrow> adm P"
-apply (rule admI)
-apply (erule (1) increasing_chain_adm_lemma)
-apply fast
-done
-
 subsection {* Admissibility on chain-finite types *}
 
 text {* for chain-finite (easy) types every formula is admissible *}
diff -r 5f37c3964866 -r 483a4876e428 src/HOLCF/FOCUS/Stream_adm.thy
--- a/src/HOLCF/FOCUS/Stream_adm.thy	Wed Nov 03 15:03:16 2010 -0700
+++ b/src/HOLCF/FOCUS/Stream_adm.thy	Wed Nov 03 15:31:24 2010 -0700
@@ -29,6 +29,31 @@
 
 section "admissibility"
 
+lemma infinite_chain_adm_lemma:
+  "\<lbrakk>Porder.chain Y; \<forall>i. P (Y i);  
+    \<And>Y. \<lbrakk>Porder.chain Y; \<forall>i. P (Y i); \<not> finite_chain Y\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)\<rbrakk>
+      \<Longrightarrow> P (\<Squnion>i. Y i)"
+apply (case_tac "finite_chain Y")
+prefer 2 apply fast
+apply (unfold finite_chain_def)
+apply safe
+apply (erule lub_finch1 [THEN thelubI, THEN ssubst])
+apply assumption
+apply (erule spec)
+done
+
+lemma increasing_chain_adm_lemma:
+  "\<lbrakk>Porder.chain Y;  \<forall>i. P (Y i); \<And>Y. \<lbrakk>Porder.chain Y; \<forall>i. P (Y i);
+    \<forall>i. \<exists>j>i. Y i \<noteq> Y j \<and> Y i \<sqsubseteq> Y j\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)\<rbrakk>
+      \<Longrightarrow> P (\<Squnion>i. Y i)"
+apply (erule infinite_chain_adm_lemma)
+apply assumption
+apply (erule thin_rl)
+apply (unfold finite_chain_def)
+apply (unfold max_in_chain_def)
+apply (fast dest: le_imp_less_or_eq elim: chain_mono_less)
+done
+
 lemma flatstream_adm_lemma:
   assumes 1: "Porder.chain Y"
   assumes 2: "!i. P (Y i)"
diff -r 5f37c3964866 -r 483a4876e428 src/HOLCF/Porder.thy
--- a/src/HOLCF/Porder.thy	Wed Nov 03 15:03:16 2010 -0700
+++ b/src/HOLCF/Porder.thy	Wed Nov 03 15:31:24 2010 -0700
@@ -344,33 +344,6 @@
 lemma lub_chain_maxelem: "\<lbrakk>Y i = c; \<forall>i. Y i \<sqsubseteq> c\<rbrakk> \<Longrightarrow> lub (range Y) = c"
   by (blast dest: ub_rangeD intro: thelubI is_lubI ub_rangeI)
 
-text {* lemmata for improved admissibility introdution rule *}
-
-lemma infinite_chain_adm_lemma:
-  "\<lbrakk>chain Y; \<forall>i. P (Y i);  
-    \<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i); \<not> finite_chain Y\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)\<rbrakk>
-      \<Longrightarrow> P (\<Squnion>i. Y i)"
-apply (case_tac "finite_chain Y")
-prefer 2 apply fast
-apply (unfold finite_chain_def)
-apply safe
-apply (erule lub_finch1 [THEN thelubI, THEN ssubst])
-apply assumption
-apply (erule spec)
-done
-
-lemma increasing_chain_adm_lemma:
-  "\<lbrakk>chain Y;  \<forall>i. P (Y i); \<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i);
-    \<forall>i. \<exists>j>i. Y i \<noteq> Y j \<and> Y i \<sqsubseteq> Y j\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)\<rbrakk>
-      \<Longrightarrow> P (\<Squnion>i. Y i)"
-apply (erule infinite_chain_adm_lemma)
-apply assumption
-apply (erule thin_rl)
-apply (unfold finite_chain_def)
-apply (unfold max_in_chain_def)
-apply (fast dest: le_imp_less_or_eq elim: chain_mono_less)
-done
-
 end
 
 end