--- 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),
--- /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];
--- /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
--- /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";
--- /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
--- /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";
--- /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
--- 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 =>
[
--- 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)"
--- 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
--- 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";
--- 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
--- 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
--- 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;
--- 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]
--- 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 =>
[
--- 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)