# 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 [ @@ -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 [ @@ -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-> t ==> D c`(Def s) = (Def t)"; +goal thy "!!c. -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-> t"; +goal thy "!s t. D c`(Discr s) = (Def t) --> -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-> t)"; +goal thy "(D c`(Discr s) = (Def t)) = ( -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 '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)