author huffman Thu, 03 Jan 2008 16:31:53 +0100 changeset 25803 230c9c87d739 parent 25802 8aea40e25aa8 child 25804 cf41372cfee6
generalized and simplified proof of adm_Finite
```--- 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)
+done
+
+

subsection "induction"
```
```--- 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 @@

(* ----------------------------------------------------------------------------------- *)

-
-
-(* 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
-
-
-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)"```