# HG changeset patch
# User huffman
# Date 1109721312 -3600
# Node ID f649b9a2cfb2c4e784d36aa5017efbeaf9c7df5f
# Parent  9d4dbd18ff2d68d280b17495102955aef74cb3b0
merged into Discrete.thy

diff -r 9d4dbd18ff2d -r f649b9a2cfb2 src/HOLCF/Discrete.ML
--- a/src/HOLCF/Discrete.ML	Wed Mar 02 00:54:06 2005 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(*  Title:      HOLCF/Discrete.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow
-*)
-
-Goalw [undiscr_def] "undiscr(Discr x) = x";
-by (Simp_tac 1);
-qed "undiscr_Discr";
-Addsimps [undiscr_Discr];
-
-Goal
- "!!S::nat=>('a::type)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}";
-by (fast_tac (claset() addDs [discr_chain0] addEs [arg_cong]) 1);
-qed "discr_chain_f_range0";
-
-Goalw [cont,is_lub_def,is_ub_def] "cont(%x::('a::type)discr. f x)";
-by (simp_tac (simpset() addsimps [discr_chain_f_range0]) 1);
-qed "cont_discr";
-AddIffs [cont_discr];
diff -r 9d4dbd18ff2d -r f649b9a2cfb2 src/HOLCF/Discrete0.ML
--- a/src/HOLCF/Discrete0.ML	Wed Mar 02 00:54:06 2005 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-(*  Title:      HOLCF/Discrete0.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow
-
-Proves that 'a discr is a po
-*)
-
-Goalw [less_discr_def] "(x::('a::type)discr) << x";
-by (rtac refl 1);
-qed "less_discr_refl";
-
-Goalw [less_discr_def]
-  "!!x. [| (x::('a::type)discr) << y; y << z |] ==> x <<  z";
-by (etac trans 1);
-by (assume_tac 1);
-qed "less_discr_trans";
-
-Goalw [less_discr_def]
-  "!!x. [| (x::('a::type)discr) << y; y << x |] ==> x=y";
-by (assume_tac 1);
-qed "less_discr_antisym";
diff -r 9d4dbd18ff2d -r f649b9a2cfb2 src/HOLCF/Discrete0.thy
--- a/src/HOLCF/Discrete0.thy	Wed Mar 02 00:54:06 2005 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-(*  Title:      HOLCF/Discrete0.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow
-
-Discrete CPOs.
-*)
-
-Discrete0 = Cont + Datatype +
-
-datatype 'a discr = Discr "'a :: type"
-
-instance discr :: (type) sq_ord
-
-defs
-less_discr_def "((op <<)::('a::type)discr=>'a discr=>bool)  ==  op ="
-
-end
diff -r 9d4dbd18ff2d -r f649b9a2cfb2 src/HOLCF/Discrete1.ML
--- a/src/HOLCF/Discrete1.ML	Wed Mar 02 00:54:06 2005 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-(*  Title:      HOLCF/Discrete1.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow
-
-Proves that 'a discr is a cpo
-*)
-
-Goalw [less_discr_def] "((x::('a::type)discr) << y) = (x=y)";
-by (rtac refl 1);
-qed "discr_less_eq";
-AddIffs [discr_less_eq];
-
-Goalw [chain_def]
- "!!S::nat=>('a::type)discr. chain S ==> S i = S 0";
-by (induct_tac "i" 1);
-by (rtac refl 1);
-by (etac subst 1);
-by (rtac sym 1);
-by (Fast_tac 1);
-qed "discr_chain0";
-
-Goal
- "!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}";
-by (fast_tac (claset() addEs [discr_chain0]) 1);
-qed "discr_chain_range0";
-Addsimps [discr_chain_range0];
-
-Goalw [is_lub_def,is_ub_def]
- "!!S. chain S ==> ? x::('a::type)discr. range(S) <<| x";
-by (Asm_simp_tac 1);
-qed "discr_cpo";
diff -r 9d4dbd18ff2d -r f649b9a2cfb2 src/HOLCF/Discrete1.thy
--- a/src/HOLCF/Discrete1.thy	Wed Mar 02 00:54:06 2005 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-(*  Title:      HOLCF/Discrete1.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow
-
-Discrete CPOs.
-*)
-
-Discrete1 = Discrete0 +
-
-instance discr :: (type) po
-  (less_discr_refl,less_discr_trans,less_discr_antisym)
-
-end