# HG changeset patch
# User huffman
# Date 1199374313 -3600
# Node ID 230c9c87d739fff873776d0a9a6c5e0d2451575b
# Parent  8aea40e25aa88b1e1fec796973f9a8c6dd29b98d
generalized and simplified proof of adm_Finite

diff -r 8aea40e25aa8 -r 230c9c87d739 src/HOLCF/IOA/meta_theory/Seq.thy
--- a/src/HOLCF/IOA/meta_theory/Seq.thy	Thu Jan 03 16:29:37 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy	Thu Jan 03 16:31:53 2008 +0100
@@ -458,6 +458,16 @@
 apply simp
 done
 
+lemma Finite_upward: "\<lbrakk>Finite x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> Finite y"
+apply (induct arbitrary: y set: Finite)
+apply (rule_tac x=y in seq.casedist, simp, simp, simp)
+apply (rule_tac x=y in seq.casedist, simp, simp)
+apply (simp add: seq.inverts)
+done
+
+lemma adm_Finite [simp]: "adm Finite"
+by (rule adm_upward, rule Finite_upward)
+
 
 subsection "induction"
 
diff -r 8aea40e25aa8 -r 230c9c87d739 src/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Thu Jan 03 16:29:37 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Thu Jan 03 16:31:53 2008 +0100
@@ -455,43 +455,6 @@
 
 (* ----------------------------------------------------------------------------------- *)
 
-
-subsection "admissibility"
-
-(* Finite x is proven to be adm: Finite_flat shows that there are only chains of length one.
-   Then the assumption that an _infinite_ chain exists (from admI2) is set to a contradiction
-   to Finite_flat *)
-
-lemma Finite_flat [rule_format]:
-"!! (x:: 'a Seq). Finite x ==> !y. Finite (y:: 'a Seq) & x<<y --> x=y"
-apply (erule Seq_Finite_ind)
-apply (intro strip)
-apply (erule conjE)
-apply (erule nil_less_is_nil)
-(* main case *)
-apply auto
-apply (rule_tac x="y" in Seq_cases)
-apply auto
-done
-
-
-lemma adm_Finite [simp]: "adm(%(x:: 'a Seq).Finite x)"
-apply (rule admI2)
-apply (erule_tac x="0" in allE)
-back
-apply (erule exE)
-apply (erule conjE)+
-apply (rule_tac x="0" in allE)
-apply assumption
-apply (erule_tac x="j" in allE)
-apply (cut_tac x="Y 0" and y="Y j" in Finite_flat)
-(* Generates a contradiction in subgoal 3 *)
-apply auto
-done
-
-
-(* ------------------------------------------------------------------------------------ *)
-
 subsection "Conc"
 
 lemma Conc_cong: "!! x::'a Seq. Finite x ==> ((x @@ y) = (x @@ z)) = (y = z)"