# HG changeset patch
# User nipkow
# Date 859395528 -3600
# Node ID c2508f4ab739dff52386b92167b80511cea67490
# Parent  7e03e61612b0d5fa78ee9debccdca3fac66d2821
Added "discrete" CPOs and modified IMP to use those rather than "lift"

diff -r 7e03e61612b0 -r c2508f4ab739 src/HOLCF/Cfun3.ML
--- a/src/HOLCF/Cfun3.ML	Wed Mar 26 13:44:05 1997 +0100
+++ b/src/HOLCF/Cfun3.ML	Wed Mar 26 17:58:48 1997 +0100
@@ -214,7 +214,7 @@
 (* function application _[_]  is strict in its first arguments              *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goal "strict_fapp1" thy "(UU::'a->'b)`x = (UU::'b)"
+qed_goal "strict_fapp1" thy "(UU::'a::cpo->'b)`x = (UU::'b)"
  (fn prems =>
         [
         (stac inst_cfun_pcpo 1),
diff -r 7e03e61612b0 -r c2508f4ab739 src/HOLCF/Discrete.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Discrete.ML	Wed Mar 26 17:58:48 1997 +0100
@@ -0,0 +1,20 @@
+(*  Title:      HOLCF/Discrete.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1997 TUM
+*)
+
+goalw thy [undiscr_def] "undiscr(Discr x) = x";
+by(Simp_tac 1);
+qed "undiscr_Discr";
+Addsimps [undiscr_Discr];
+
+goal thy
+ "!!S::nat=>('a::term)discr. is_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 thy [cont,is_lub,is_ub] "cont(%x::('a::term)discr.f x)";
+by(simp_tac (!simpset addsimps [discr_chain_f_range0]) 1);
+qed "cont_discr";
+AddIffs [cont_discr];
diff -r 7e03e61612b0 -r c2508f4ab739 src/HOLCF/Discrete.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Discrete.thy	Wed Mar 26 17:58:48 1997 +0100
@@ -0,0 +1,17 @@
+(*  Title:      HOLCF/Discrete.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1997 TUM
+
+Discrete CPOs
+*)
+
+Discrete = Discrete1 +
+
+instance discr :: (term)cpo   (discr_cpo)
+
+constdefs
+   undiscr :: ('a::term)discr => 'a
+  "undiscr x == (case x of Discr y => y)"
+
+end
diff -r 7e03e61612b0 -r c2508f4ab739 src/HOLCF/Discrete0.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Discrete0.ML	Wed Mar 26 17:58:48 1997 +0100
@@ -0,0 +1,22 @@
+(*  Title:      HOLCF/Discrete0.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1997 TUM
+
+Proves that 'a discr is a po
+*)
+
+goalw thy [less_discr_def] "less (x::('a::term)discr) x";
+br refl 1;
+qed "less_discr_refl";
+
+goalw thy [less_discr_def]
+  "!!x. [| less (x::('a::term)discr) y; less y z |] ==> less x z";
+be trans 1;
+ba 1;
+qed "less_discr_trans";
+
+goalw thy [less_discr_def]
+  "!!x. [| less (x::('a::term)discr) y; less y x |] ==> x=y";
+ba 1;
+qed "less_discr_antisym";
diff -r 7e03e61612b0 -r c2508f4ab739 src/HOLCF/Discrete0.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Discrete0.thy	Wed Mar 26 17:58:48 1997 +0100
@@ -0,0 +1,16 @@
+(*  Title:      HOLCF/Discrete0.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1997 TUM
+
+Discrete CPOs
+*)
+
+Discrete0 = Cont +
+
+datatype 'a discr = Discr 'a
+
+defs
+less_discr_def "(less::('a::term)discr=>'a discr=>bool)  ==  op ="
+
+end
diff -r 7e03e61612b0 -r c2508f4ab739 src/HOLCF/Discrete1.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Discrete1.ML	Wed Mar 26 17:58:48 1997 +0100
@@ -0,0 +1,32 @@
+(*  Title:      HOLCF/Discrete1.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1997 TUM
+
+Proves that 'a discr is a cpo
+*)
+
+goalw thy [po_def,less_discr_def] "((x::('a::term)discr) << y) = (x=y)";
+br refl 1;
+qed "discr_less_eq";
+AddIffs [discr_less_eq];
+
+goalw thy [is_chain]
+ "!!S::nat=>('a::term)discr. is_chain S ==> S i = S 0";
+by(nat_ind_tac "i" 1);
+ br refl 1;
+be subst 1;
+br sym 1;
+by(Fast_tac 1);
+qed "discr_chain0";
+
+goal thy
+ "!!S::nat=>('a::term)discr. is_chain(S) ==> range(S) = {S 0}";
+by(fast_tac (!claset addEs [discr_chain0]) 1);
+qed "discr_chain_range0";
+Addsimps [discr_chain_range0];
+
+goalw thy [is_lub,is_ub]
+ "!!S. is_chain S ==> ? x::('a::term)discr. range(S) <<| x";
+by(Asm_simp_tac 1);
+qed "discr_cpo";
diff -r 7e03e61612b0 -r c2508f4ab739 src/HOLCF/Discrete1.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Discrete1.thy	Wed Mar 26 17:58:48 1997 +0100
@@ -0,0 +1,14 @@
+(*  Title:      HOLCF/Discrete1.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1997 TUM
+
+Discrete CPOs
+*)
+
+Discrete1 = Discrete0 +
+
+instance discr :: (term)po
+  (less_discr_refl,less_discr_trans,less_discr_antisym)
+
+end
diff -r 7e03e61612b0 -r c2508f4ab739 src/HOLCF/Fix.ML
--- a/src/HOLCF/Fix.ML	Wed Mar 26 13:44:05 1997 +0100
+++ b/src/HOLCF/Fix.ML	Wed Mar 26 17:58:48 1997 +0100
@@ -690,7 +690,7 @@
 	]);
 
 qed_goal "chfin_fappR" thy 
-    "[| is_chain (Y::nat => 'a->'b); chain_finite(x::'b) |] ==> \
+    "[| is_chain (Y::nat => 'a::cpo->'b); chain_finite(x::'b) |] ==> \
 \    !s. ? n. lub(range(Y))`s = Y n`s" 
 (fn prems => 
 	[
@@ -702,7 +702,8 @@
 	]);
 
 qed_goalw "adm_chfindom" thy [adm_def]
-	    "chain_finite (x::'b) ==> adm (%(u::'a->'b). P(u`s))" (fn prems => [
+    "chain_finite (x::'b) ==> adm (%(u::'a::cpo->'b). P(u`s))"
+    (fn prems => [
 	cut_facts_tac prems 1,
 	strip_tac 1,
 	dtac chfin_fappR 1,
@@ -1095,7 +1096,7 @@
         ]);
 
   val adm_disj_lemma5 = prove_goal thy
-  "!!Y::nat=>'a. [| is_chain(Y); ! j. i < j --> Q(Y(j)) |] ==>\
+  "!!Y::nat=>'a::cpo. [| is_chain(Y); ! j. i < j --> Q(Y(j)) |] ==>\
   \       lub(range(Y)) = lub(range(%m. if m< Suc(i) then Y(Suc(i)) else Y m))"
  (fn prems =>
         [
@@ -1108,7 +1109,7 @@
         ]);
 
   val adm_disj_lemma6 = prove_goal thy
-  "[| is_chain(Y::nat=>'a); ? i. ! j. i < j --> Q(Y(j)) |] ==>\
+  "[| is_chain(Y::nat=>'a::cpo); ? i. ! j. i < j --> Q(Y(j)) |] ==>\
   \         ? X. is_chain(X) & (! n. Q(X(n))) & lub(range(Y)) = lub(range(X))"
  (fn prems =>
         [
@@ -1127,7 +1128,7 @@
         ]);
 
   val adm_disj_lemma7 = prove_goal thy 
-  "[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j))  |] ==>\
+  "[| is_chain(Y::nat=>'a::cpo); ! i. ? j. i < j & P(Y(j))  |] ==>\
   \         is_chain(%m. Y(Least(%j. m<j & P(Y(j)))))"
  (fn prems =>
         [
@@ -1161,7 +1162,7 @@
         ]);
 
   val adm_disj_lemma9 = prove_goal thy
-  "[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\
+  "[| is_chain(Y::nat=>'a::cpo); ! i. ? j. i < j & P(Y(j)) |] ==>\
   \         lub(range(Y)) = lub(range(%m. Y(Least(%j. m<j & P(Y(j))))))"
  (fn prems =>
         [
@@ -1192,7 +1193,7 @@
         ]);
 
   val adm_disj_lemma10 = prove_goal thy
-  "[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\
+  "[| is_chain(Y::nat=>'a::cpo); ! i. ? j. i < j & P(Y(j)) |] ==>\
   \         ? X. is_chain(X) & (! n. P(X(n))) & lub(range(Y)) = lub(range(X))"
  (fn prems =>
         [
diff -r 7e03e61612b0 -r c2508f4ab739 src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Wed Mar 26 13:44:05 1997 +0100
+++ b/src/HOLCF/Fix.thy	Wed Mar 26 17:58:48 1997 +0100
@@ -15,10 +15,10 @@
 iterate	:: "nat=>('a->'a)=>'a=>'a"
 Ifix	:: "('a->'a)=>'a"
 fix	:: "('a->'a)->'a"
-adm		:: "('a=>bool)=>bool"
+adm		:: "('a::cpo=>bool)=>bool"
 admw		:: "('a=>bool)=>bool"
-chain_finite	:: "'a=>bool"
-flat		:: "'a=>bool" (* should be called flat, for consistency *)
+chain_finite	:: "'a::cpo=>bool"
+flat		:: "'a=>bool"
 
 defs
 
@@ -32,8 +32,8 @@
 admw_def      "admw P == !F. (!n.P (iterate n F UU)) -->
                             P (lub(range (%i. iterate i F UU)))" 
 
-chain_finite_def  "chain_finite (x::'a)==
-                        !Y. is_chain (Y::nat=>'a) --> (? n.max_in_chain n Y)"
+chain_finite_def  "chain_finite (x::'a::cpo)==
+                   !Y. is_chain (Y::nat=>'a::cpo) --> (? n.max_in_chain n Y)"
 
 flat_def	  "flat (x::'a) == ! x y. (x::'a) << y --> (x = UU) | (x=y)"
 
diff -r 7e03e61612b0 -r c2508f4ab739 src/HOLCF/HOLCF.thy
--- a/src/HOLCF/HOLCF.thy	Wed Mar 26 13:44:05 1997 +0100
+++ b/src/HOLCF/HOLCF.thy	Wed Mar 26 17:58:48 1997 +0100
@@ -8,5 +8,4 @@
 
 *)
 
-HOLCF = One + Tr
-
+HOLCF = Discrete + One + Tr
diff -r 7e03e61612b0 -r c2508f4ab739 src/HOLCF/IMP/Denotational.ML
--- a/src/HOLCF/IMP/Denotational.ML	Wed Mar 26 13:44:05 1997 +0100
+++ b/src/HOLCF/IMP/Denotational.ML	Wed Mar 26 17:58:48 1997 +0100
@@ -6,76 +6,57 @@
 Equivalence of Denotational Semantics in HOLCF and Evaluation Semantics in HOL
 *)
 
-Addsimps [flift1_def];
+goalw thy [dlift_def] "dlift f`(Def x) = f`(Discr x)";
+by(Simp_tac 1);
+qed "dlift_Def";
+Addsimps [dlift_Def];
 
-val prems = goal Lift.thy "[| f`UU = UU; f`x = Def b |] ==> EX a. x = Def a";
-by (cut_facts_tac prems 1);
-by (res_inst_tac [("x","x")] Lift_cases 1);
- by (fast_tac (HOL_cs addSEs [DefE2]) 1);
-by (fast_tac HOL_cs 1);
-qed "strict_Def";
+goalw thy [dlift_def] "cont(%f. dlift f)";
+by(Simp_tac 1);
+qed "cont_dlift";
+AddIffs [cont_dlift];
+
+goalw thy [dlift_def] "dlift f`l = Def y --> (? x. l = Def x)";
+by(simp_tac (!simpset setloop (split_tac[expand_lift_case])) 1);
+qed_spec_mp "dlift_DefD";
 
 
-goal thy "D(WHILE b DO c) = D(IF b THEN c;WHILE b DO c ELSE SKIP)";
-by(Simp_tac 1);
-by(EVERY[stac fix_eq 1, Simp_tac 1, IF_UNSOLVED	no_tac]);
-qed "D_While_If";
-
-
-goal thy "D c`UU =UU";
-by (com.induct_tac "c" 1);
-    by (ALLGOALS Asm_simp_tac);
-by (stac fix_eq 1);
-by (Asm_simp_tac 1);
-qed "D_strict";
-
-
-goal thy "!!c. <c,s> -c-> t ==> D c`(Def s) = (Def t)";
+goal thy "!!c. <c,s> -c-> t ==> D c`(Discr s) = (Def t)";
 be evalc.induct 1;
       by (ALLGOALS Asm_simp_tac);
  by (ALLGOALS (rtac (fix_eq RS ssubst) THEN' Asm_full_simp_tac));
 qed_spec_mp "eval_implies_D";
 
-goal thy "!s t. D c`(Def s) = (Def t) --> <c,s> -c-> t";
+goal thy "!s t. D c`(Discr s) = (Def t) --> <c,s> -c-> t";
 by (com.induct_tac "c" 1);
     by (fast_tac ((HOL_cs addSIs evalc.intrs) addss !simpset) 1);
    by (fast_tac ((HOL_cs addSIs evalc.intrs) addss !simpset) 1);
   by (Simp_tac 1);
   by (strip_tac 1);
-  by (forward_tac [D_strict RS strict_Def] 1);
+  by (forward_tac [dlift_DefD] 1);
   be exE 1;
   by (rotate_tac ~1 1);
   by (Asm_full_simp_tac 1);
   by (fast_tac (HOL_cs addSIs evalc.intrs) 1);
- by (REPEAT (rtac allI 1));
- by (case_tac "bexp s" 1);
-  by (fast_tac ((HOL_cs addSIs evalc.intrs) unsafe_addss !simpset) 1);
+ by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
  by (fast_tac ((HOL_cs addIs evalc.intrs) unsafe_addss !simpset) 1);
-by(res_inst_tac [("Q","D (WHILE bexp DO com)`UU = UU")] conjunct1 1);
 by (Simp_tac 1);
 br fix_ind 1;
   by(fast_tac (HOL_cs addSIs (adm_lemmas@[adm_flatdom,flat_lift])) 1);
  by (Simp_tac 1);
-br conjI 1;
- by (REPEAT (rtac allI 1));
- by (case_tac "bexp s" 1);
+by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
+by (safe_tac HOL_cs);
   (* case bexp s *)
-  by (Asm_simp_tac 1);
-  by (strip_tac 1);
-  be conjE 1;
-  bd strict_Def 1;
-   ba 1;
+  by (forward_tac [dlift_DefD] 1);
   be exE 1;
   by (rotate_tac ~1 1);
   by (Asm_full_simp_tac 1);
   by (fast_tac (HOL_cs addIs evalc.intrs) 1);
  (* case ~bexp s *)
  by (fast_tac ((HOL_cs addSIs evalc.intrs) unsafe_addss !simpset) 1);
-(* induction step for strictness *)
-by (Asm_full_simp_tac 1);
 qed_spec_mp "D_implies_eval";
 
 
-goal thy "(D c`(Def s) = (Def t)) = (<c,s> -c-> t)";
+goal thy "(D c`(Discr s) = (Def t)) = (<c,s> -c-> t)";
 by (fast_tac (HOL_cs addSEs [D_implies_eval,eval_implies_D]) 1);
 qed "D_is_eval";
diff -r 7e03e61612b0 -r c2508f4ab739 src/HOLCF/IMP/Denotational.thy
--- a/src/HOLCF/IMP/Denotational.thy	Wed Mar 26 13:44:05 1997 +0100
+++ b/src/HOLCF/IMP/Denotational.thy	Wed Mar 26 17:58:48 1997 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/IMP/Den2.ML
+(*  Title:      HOLCF/IMP/Denotational.thy
     ID:         $Id$
     Author:     Tobias Nipkow & Robert Sandner, TUM
     Copyright   1996 TUM
@@ -8,15 +8,20 @@
 
 Denotational = HOLCF + Natural +
 
-consts D :: "com => state lift -> state lift"
+constdefs
+   dlift :: "(('a::term) discr -> 'b::pcpo) => ('a lift -> 'b)"
+  "dlift f == (LAM x.case x of Undef => UU | Def(y) => f`(Discr y))"
+
+consts D :: "com => state discr -> state lift"
 
 primrec D com
-  "D(SKIP) = (LAM s. s)"
-  "D(X := a) = flift1(%s. Def(s[a(s)/X]))"
-  "D(c0 ; c1) = ((D c1) oo (D c0))"
+  "D(SKIP) = (LAM s. Def(undiscr s))"
+  "D(X := a) = (LAM s. Def((undiscr s)[a(undiscr s)/X]))"
+  "D(c0 ; c1) = (dlift(D c1) oo (D c0))"
   "D(IF b THEN c1 ELSE c2) =
-	flift1(%s . if b s then (D c1)`(Def s) else (D c2)`(Def s))"
+	(LAM s. if b(undiscr s) then (D c1)`s else (D c2)`s)"
   "D(WHILE b DO c) =
-	fix`(LAM w. flift1(%s. if b s then w`((D c)`(Def s)) else Def s))"
+	fix`(LAM w s. if b(undiscr s) then (dlift w)`((D c)`s)
+                      else Def(undiscr s))"
 
 end
diff -r 7e03e61612b0 -r c2508f4ab739 src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Wed Mar 26 13:44:05 1997 +0100
+++ b/src/HOLCF/IsaMakefile	Wed Mar 26 17:58:48 1997 +0100
@@ -16,6 +16,7 @@
        Ssum0.thy Ssum1.thy Ssum2.thy Ssum3.thy \
        Up1.thy Up2.thy Up3.thy Fix.thy ccc1.thy \
        One.thy Tr.thy\
+       Discrete0.thy Discrete1.thy Discrete.thy\
        Lift1.thy Lift2.thy Lift3.thy HOLCF.thy 
 
 ONLYTHYS = Lift.thy
diff -r 7e03e61612b0 -r c2508f4ab739 src/HOLCF/Lift3.ML
--- a/src/HOLCF/Lift3.ML	Wed Mar 26 13:44:05 1997 +0100
+++ b/src/HOLCF/Lift3.ML	Wed Mar 26 17:58:48 1997 +0100
@@ -7,8 +7,6 @@
 *)
 
 
-open Lift3;
-
 (* for compatibility with old HOLCF-Version *)
 qed_goal "inst_lift_pcpo" thy "UU = Undef"
  (fn prems => 
@@ -104,6 +102,12 @@
 by (fast_tac (HOL_cs addSEs prems) 1);
 qed"Lift_cases";
 
+goal thy
+  "P(lift_case a b x) = ((x=UU --> P a) & (!y. x = Def y --> P(b y)))";
+by(lift.induct_tac "x" 1);
+by(ALLGOALS Asm_simp_tac);
+qed "expand_lift_case";
+
 goal Lift3.thy "(x~=UU)=(? y.x=Def y)";
 br iffI 1;
  br Lift_cases 1;
diff -r 7e03e61612b0 -r c2508f4ab739 src/HOLCF/Porder.ML
--- a/src/HOLCF/Porder.ML	Wed Mar 26 13:44:05 1997 +0100
+++ b/src/HOLCF/Porder.ML	Wed Mar 26 17:58:48 1997 +0100
@@ -136,6 +136,12 @@
         ]);
 
 
+goal thy "lub{x} = x";
+br thelubI 1;
+by(simp_tac (!simpset addsimps [is_lub,is_ub]) 1);
+qed "lub_singleton";
+Addsimps [lub_singleton];
+
 (* ------------------------------------------------------------------------ *)
 (* access to some definition as inference rule                              *)
 (* ------------------------------------------------------------------------ *)
@@ -244,8 +250,7 @@
         (rtac allI 1),
         (nat_ind_tac "i" 1),
         (Asm_simp_tac 1),
-        (Asm_simp_tac 1),
-        (rtac refl_less 1)
+        (Asm_simp_tac 1)
         ]);
 
 qed_goalw "bin_chainmax" thy [max_in_chain_def,le_def]
diff -r 7e03e61612b0 -r c2508f4ab739 src/HOLCF/Porder0.ML
--- a/src/HOLCF/Porder0.ML	Wed Mar 26 13:44:05 1997 +0100
+++ b/src/HOLCF/Porder0.ML	Wed Mar 26 17:58:48 1997 +0100
@@ -13,6 +13,8 @@
         (fast_tac (HOL_cs addSIs [ax_refl_less]) 1)
         ]);
 
+AddIffs [refl_less];
+
 qed_goalw "antisym_less" thy [ po_def ] "[| x << y; y << x |] ==> x = y"
 (fn prems =>
         [
diff -r 7e03e61612b0 -r c2508f4ab739 src/HOLCF/ccc1.thy
--- a/src/HOLCF/ccc1.thy	Wed Mar 26 13:44:05 1997 +0100
+++ b/src/HOLCF/ccc1.thy	Wed Mar 26 17:58:48 1997 +0100
@@ -12,8 +12,8 @@
 instance flat<chfin (flat_subclass_chfin)
 
 consts
-        ID      :: "'a -> 'a"
-        cfcomp  :: "('b->'c)->('a->'b)->'a->'c"
+        ID      :: "('a::cpo) -> 'a"
+        cfcomp  :: "('b->'c)->(('a::cpo)->('b::cpo))->'a->('c::cpo)"
 
 syntax  "@oo"   :: "('b->'c)=>('a->'b)=>'a->'c" ("_ oo _" [101,100] 100)