--- a/src/HOLCF/Cfun3.ML Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Cfun3.ML Thu Oct 06 18:40:18 1994 +0100
@@ -17,11 +17,11 @@
(strip_tac 1),
(rtac (expand_fun_eq RS iffD2) 1),
(strip_tac 1),
- (rtac (lub_cfun RS thelubI RS ssubst) 1),
+ (rtac (thelub_cfun RS ssubst) 1),
(atac 1),
(rtac (Cfunapp2 RS ssubst) 1),
(etac contX_lubcfun 1),
- (rtac (lub_fun RS thelubI RS ssubst) 1),
+ (rtac (thelub_fun RS ssubst) 1),
(etac (monofun_fapp1 RS ch2ch_monofun) 1),
(rtac refl 1)
]);
--- a/src/HOLCF/Cont.ML Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Cont.ML Thu Oct 06 18:40:18 1994 +0100
@@ -312,15 +312,12 @@
(* in both arguments *)
(* ------------------------------------------------------------------------ *)
-val diag_lubCF2_1 = prove_goal Cont.thy
+val diag_lemma1 = prove_goal Cont.thy
"[|contX(CF2);!f.contX(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
-\ lub(range(%i. lub(range(%j. CF2(FY(j))(TY(i)))))) =\
-\ lub(range(%i. CF2(FY(i))(TY(i))))"
-(fn prems =>
+\ is_chain(%i. lub(range(%j. CF2(FY(j), TY(i)))))"
+ (fn prems =>
[
(cut_facts_tac prems 1),
- (rtac antisym_less 1),
- (rtac is_lub_thelub 1),
(rtac ch2ch_lubMF2L 1),
(rtac contX2mono 1),
(atac 1),
@@ -328,109 +325,124 @@
(rtac contX2mono 1),
(etac spec 1),
(atac 1),
- (atac 1),
- (rtac ub_rangeI 1),
- (strip_tac 1 ),
- (rtac is_lub_thelub 1),
- ((rtac ch2ch_MF2L 1) THEN (rtac contX2mono 1) THEN (atac 1)),
- (atac 1),
- (rtac ub_rangeI 1),
- (strip_tac 1 ),
- (res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1),
- (rtac trans_less 1),
- (rtac is_ub_thelub 2),
- (rtac (chain_mono RS mp) 1),
- ((rtac ch2ch_MF2R 1) THEN (rtac contX2mono 1) THEN (etac spec 1)),
- (atac 1),
- (atac 1),
- ((rtac ch2ch_MF2LR 1) THEN (etac contX2mono 1)),
+ (atac 1)
+ ]);
+
+val diag_lemma2 = prove_goal Cont.thy
+"[|contX(CF2);is_chain(FY); is_chain(TY) |] ==>\
+\ is_chain(%m. CF2(FY(m), TY(n::nat)))"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (etac (contX2mono RS ch2ch_MF2L) 1),
+ (atac 1)
+ ]);
+
+val diag_lemma3 = prove_goal Cont.thy
+"[|!f.contX(CF2(f));is_chain(FY); is_chain(TY) |] ==>\
+\ is_chain(%m. CF2(FY(n), TY(m)))"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (etac allE 1),
+ (etac (contX2mono RS ch2ch_MF2R) 1),
+ (atac 1)
+ ]);
+
+val diag_lemma4 = prove_goal Cont.thy
+"[|contX(CF2);!f.contX(CF2(f));is_chain(FY); is_chain(TY) |] ==>\
+\ is_chain(%m. CF2(FY(m), TY(m)))"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (etac (contX2mono RS ch2ch_MF2LR) 1),
(rtac allI 1),
- ((rtac contX2mono 1) THEN (etac spec 1)),
- (atac 1),
- (atac 1),
- (hyp_subst_tac 1),
- (rtac is_ub_thelub 1),
- ((rtac ch2ch_MF2LR 1) THEN (etac contX2mono 1)),
- (rtac allI 1),
- ((rtac contX2mono 1) THEN (etac spec 1)),
- (atac 1),
+ (etac allE 1),
+ (etac contX2mono 1),
(atac 1),
- (rtac trans_less 1),
- (rtac is_ub_thelub 2),
- (res_inst_tac [("x1","ia")] (chain_mono RS mp) 1),
- ((rtac ch2ch_MF2L 1) THEN (etac contX2mono 1)),
- (atac 1),
- (atac 1),
- ((rtac ch2ch_MF2LR 1) THEN (etac contX2mono 1)),
- (rtac allI 1),
- ((rtac contX2mono 1) THEN (etac spec 1)),
- (atac 1),
- (atac 1),
- (rtac lub_mono 1),
- ((rtac ch2ch_MF2LR 1) THEN (etac contX2mono 1)),
- (rtac allI 1),
- ((rtac contX2mono 1) THEN (etac spec 1)),
- (atac 1),
- (atac 1),
- (rtac ch2ch_lubMF2L 1),
- (rtac contX2mono 1),
- (atac 1),
- (rtac allI 1),
- ((rtac contX2mono 1) THEN (etac spec 1)),
- (atac 1),
- (atac 1),
- (strip_tac 1 ),
- (rtac is_ub_thelub 1),
- ((rtac ch2ch_MF2L 1) THEN (etac contX2mono 1)),
(atac 1)
]);
+val diag_lubCF2_1 = prove_goal Cont.thy
+"[|contX(CF2);!f.contX(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
+\ lub(range(%i. lub(range(%j. CF2(FY(j))(TY(i)))))) =\
+\ lub(range(%i. CF2(FY(i))(TY(i))))"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (rtac antisym_less 1),
+ (rtac is_lub_thelub 1),
+ (etac diag_lemma1 1),
+ (REPEAT (atac 1)),
+ (rtac ub_rangeI 1),
+ (strip_tac 1 ),
+ (rtac lub_mono3 1),
+ (etac diag_lemma2 1),
+ (REPEAT (atac 1)),
+ (etac diag_lemma4 1),
+ (REPEAT (atac 1)),
+ (rtac allI 1),
+ (res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1),
+ (res_inst_tac [("x","ia")] exI 1),
+ (rtac (chain_mono RS mp) 1),
+ (etac diag_lemma3 1),
+ (REPEAT (atac 1)),
+ (hyp_subst_tac 1),
+ (res_inst_tac [("x","ia")] exI 1),
+ (rtac refl_less 1),
+ (res_inst_tac [("x","i")] exI 1),
+ (rtac (chain_mono RS mp) 1),
+ (etac diag_lemma2 1),
+ (REPEAT (atac 1)),
+ (rtac lub_mono 1),
+ (etac diag_lemma4 1),
+ (REPEAT (atac 1)),
+ (etac diag_lemma1 1),
+ (REPEAT (atac 1)),
+ (strip_tac 1 ),
+ (rtac is_ub_thelub 1),
+ (etac diag_lemma2 1),
+ (REPEAT (atac 1))
+ ]);
+
val diag_lubCF2_2 = prove_goal Cont.thy
"[|contX(CF2);!f.contX(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
\ lub(range(%j. lub(range(%i. CF2(FY(j))(TY(i)))))) =\
\ lub(range(%i. CF2(FY(i))(TY(i))))"
-(fn prems =>
+ (fn prems =>
[
(cut_facts_tac prems 1),
(rtac trans 1),
(rtac ex_lubMF2 1),
- (rtac ((hd prems) RS contX2mono) 1),
+ (etac contX2mono 1),
(rtac allI 1),
- (rtac (((hd (tl prems)) RS spec RS contX2mono)) 1),
- (atac 1),
- (atac 1),
+ (etac allE 1),
+ (etac contX2mono 1),
+ (REPEAT (atac 1)),
(rtac diag_lubCF2_1 1),
- (atac 1),
- (atac 1),
- (atac 1),
- (atac 1)
+ (REPEAT (atac 1))
]);
-
val contlub_CF2 = prove_goal Cont.thy
"[|contX(CF2);!f.contX(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
\ CF2(lub(range(FY)))(lub(range(TY))) = lub(range(%i.CF2(FY(i))(TY(i))))"
-(fn prems =>
+ (fn prems =>
[
(cut_facts_tac prems 1),
- (rtac ((hd prems) RS contX2contlub RS contlubE RS
- spec RS mp RS ssubst) 1),
+ (rtac ((hd prems) RS contX2contlub RS contlubE RS spec RS mp RS ssubst) 1),
(atac 1),
(rtac (thelub_fun RS ssubst) 1),
- (rtac ((hd prems) RS contX2mono RS ch2ch_monofun) 1),
+ (rtac ((hd prems) RS contX2mono RS ch2ch_monofun) 1),
(atac 1),
(rtac trans 1),
- (rtac (((hd (tl prems)) RS spec RS contX2contlub) RS
- contlubE RS spec RS mp RS ext RS arg_cong RS arg_cong) 1),
+ (rtac (((hd (tl prems)) RS spec RS contX2contlub) RS contlubE RS
+ spec RS mp RS ext RS arg_cong RS arg_cong) 1),
(atac 1),
(rtac diag_lubCF2_2 1),
- (atac 1),
- (atac 1),
- (atac 1),
- (atac 1)
+ (REPEAT (atac 1))
]);
-
+
(* ------------------------------------------------------------------------ *)
(* The following results are about application for functions in 'a=>'b *)
(* ------------------------------------------------------------------------ *)
@@ -574,24 +586,20 @@
(atac 1)
]);
+
val contX2contlub_app = prove_goal Cont.thy
-"[|contX(ft);!x.contX(ft(x));contX(tt)|] ==>\
-\ contlub(%x.(ft(x))(tt(x)))"
+"[|contX(ft);!x.contX(ft(x));contX(tt)|] ==> contlub(%x.(ft(x))(tt(x)))"
(fn prems =>
[
(cut_facts_tac prems 1),
(rtac contlubI 1),
(strip_tac 1),
(res_inst_tac [("f3","tt")] (contlubE RS spec RS mp RS ssubst) 1),
- (rtac contX2contlub 1),
- (resolve_tac prems 1),
+ (etac contX2contlub 1),
(atac 1),
(rtac contlub_CF2 1),
- (resolve_tac prems 1),
- (resolve_tac prems 1),
- (atac 1),
- (rtac (contX2mono RS ch2ch_monofun) 1),
- (resolve_tac prems 1),
+ (REPEAT (atac 1)),
+ (etac (contX2mono RS ch2ch_monofun) 1),
(atac 1)
]);
--- a/src/HOLCF/Cprod3.thy Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Cprod3.thy Thu Oct 06 18:40:18 1994 +0100
@@ -20,6 +20,8 @@
csnd :: "('a*'b)->'b"
csplit :: "('a->'b->'c)->('a*'b)->'c"
+translations "x#y" => "cpair[x][y]"
+
rules
inst_cprod_pcpo "(UU::'a*'b) = <UU,UU>"
@@ -31,13 +33,6 @@
end
-ML
-
-(* ----------------------------------------------------------------------*)
-(* parse translations for the above mixfix *)
-(* ----------------------------------------------------------------------*)
-
-val parse_translation = [("@cpair",mk_cinfixtr "@cpair")];
--- a/src/HOLCF/Dlist.thy Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Dlist.thy Thu Oct 06 18:40:18 1994 +0100
@@ -4,7 +4,19 @@
ID: $ $
Copyright 1994 Technische Universitaet Muenchen
-Theory for lists
+Theory for finite lists 'a dlist = one ++ ('a ** 'a dlist)
+
+The type is axiomatized as the least solution of the domain equation above.
+The functor term that specifies the domain equation is:
+
+ FT = <++,K_{one},<**,K_{'a},I>>
+
+For details see chapter 5 of:
+
+[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
+ Dissertation, Technische Universit"at M"unchen, 1994
+
+
*)
Dlist = Stream2 +
@@ -47,8 +59,9 @@
(* axiomatization of recursive type 'a dlist *)
(* ----------------------------------------------------------------------- *)
(* ('a dlist,dlist_abs) is the initial F-algebra where *)
-(* F is the locally continuous functor determined by domain equation *)
-(* X = one ++ 'a ** X *)
+(* F is the locally continuous functor determined by functor term FT. *)
+(* domain equation: 'a dlist = one ++ ('a ** 'a dlist) *)
+(* functor term: FT = <++,K_{one},<**,K_{'a},I>> *)
(* ----------------------------------------------------------------------- *)
(* dlist_abs is an isomorphism with inverse dlist_rep *)
(* identity is the least endomorphism on 'a dlist *)
--- a/src/HOLCF/Dnat.ML Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Dnat.ML Thu Oct 06 18:40:18 1994 +0100
@@ -12,7 +12,7 @@
(* The isomorphisms dnat_rep_iso and dnat_abs_iso are strict *)
(* ------------------------------------------------------------------------*)
-val dnat_iso_strict= dnat_rep_iso RS (dnat_abs_iso RS
+val dnat_iso_strict = dnat_rep_iso RS (dnat_abs_iso RS
(allI RSN (2,allI RS iso_strict)));
val dnat_rews = [dnat_iso_strict RS conjunct1,
@@ -530,3 +530,5 @@
+
+
--- a/src/HOLCF/Dnat.thy Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Dnat.thy Thu Oct 06 18:40:18 1994 +0100
@@ -3,7 +3,17 @@
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Theory for the domain of natural numbers
+Theory for the domain of natural numbers dnat = one ++ dnat
+
+The type is axiomatized as the least solution of the domain equation above.
+The functor term that specifies the domain equation is:
+
+ FT = <++,K_{one},I>
+
+For details see chapter 5 of:
+
+[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
+ Dissertation, Technische Universit"at M"unchen, 1994
*)
@@ -44,8 +54,9 @@
(* axiomatization of recursive type dnat *)
(* ----------------------------------------------------------------------- *)
(* (dnat,dnat_abs) is the initial F-algebra where *)
-(* F is the locally continuous functor determined by domain equation *)
-(* X = one ++ X *)
+(* F is the locally continuous functor determined by functor term FT. *)
+(* domain equation: dnat = one ++ dnat *)
+(* functor term: FT = <++,K_{one},I> *)
(* ----------------------------------------------------------------------- *)
(* dnat_abs is an isomorphism with inverse dnat_rep *)
(* identity is the least endomorphism on dnat *)
--- a/src/HOLCF/Fix.ML Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Fix.ML Thu Oct 06 18:40:18 1994 +0100
@@ -688,6 +688,43 @@
(etac cfun_arg_cong 1)
]);
+(* ------------------------------------------------------------------------- *)
+(* a result about functions with flat codomain *)
+(* ------------------------------------------------------------------------- *)
+
+val flat_codom = prove_goalw Fix.thy [flat_def]
+"[|flat(y::'b);f[x::'a]=(c::'b)|] ==> f[UU::'a]=UU::'b | (!z.f[z::'a]=c)"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (res_inst_tac [("Q","f[x::'a]=UU::'b")] classical2 1),
+ (rtac disjI1 1),
+ (rtac UU_I 1),
+ (res_inst_tac [("s","f[x]"),("t","UU::'b")] subst 1),
+ (atac 1),
+ (rtac (minimal RS monofun_cfun_arg) 1),
+ (res_inst_tac [("Q","f[UU::'a]=UU::'b")] classical2 1),
+ (etac disjI1 1),
+ (rtac disjI2 1),
+ (rtac allI 1),
+ (res_inst_tac [("s","f[x]"),("t","c")] subst 1),
+ (atac 1),
+ (res_inst_tac [("a","f[UU::'a]")] (refl RS box_equals) 1),
+ (etac allE 1),(etac allE 1),
+ (dtac mp 1),
+ (res_inst_tac [("fo5","f")] (minimal RS monofun_cfun_arg) 1),
+ (etac disjE 1),
+ (contr_tac 1),
+ (atac 1),
+ (etac allE 1),
+ (etac allE 1),
+ (dtac mp 1),
+ (res_inst_tac [("fo5","f")] (minimal RS monofun_cfun_arg) 1),
+ (etac disjE 1),
+ (contr_tac 1),
+ (atac 1)
+ ]);
+
(* ------------------------------------------------------------------------ *)
(* admissibility of special formulae and propagation *)
(* ------------------------------------------------------------------------ *)
@@ -777,6 +814,8 @@
(etac spec 1)
]);
+val adm_all2 = (allI RS adm_all);
+
val adm_subst = prove_goal Fix.thy
"[|contX(t); adm(P)|] ==> adm(%x.P(t(x)))"
(fn prems =>
@@ -1127,45 +1166,8 @@
]);
-val adm_all2 = (allI RS adm_all);
val adm_thms = [adm_impl,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less,
adm_all2,adm_not_less,adm_not_free,adm_conj,adm_less
];
-(* ------------------------------------------------------------------------- *)
-(* a result about functions with flat codomain *)
-(* ------------------------------------------------------------------------- *)
-
-val flat_codom = prove_goalw Fix.thy [flat_def]
-"[|flat(y::'b);f[x::'a]=(c::'b)|] ==> f[UU::'a]=(UU::'b) | (!z.f[z::'a]=c)"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (res_inst_tac [("Q","f[x::'a]=(UU::'b)")] classical2 1),
- (rtac disjI1 1),
- (rtac UU_I 1),
- (res_inst_tac [("s","f[x]"),("t","UU::'b")] subst 1),
- (atac 1),
- (rtac (minimal RS monofun_cfun_arg) 1),
- (res_inst_tac [("Q","f[UU::'a]=(UU::'b)")] classical2 1),
- (etac disjI1 1),
- (rtac disjI2 1),
- (rtac allI 1),
- (res_inst_tac [("s","f[x]"),("t","c")] subst 1),
- (atac 1),
- (res_inst_tac [("a","f[UU::'a]")] (refl RS box_equals) 1),
- (etac allE 1),(etac allE 1),
- (dtac mp 1),
- (res_inst_tac [("fo5","f")] (minimal RS monofun_cfun_arg) 1),
- (etac disjE 1),
- (contr_tac 1),
- (atac 1),
- (etac allE 1),
- (etac allE 1),
- (dtac mp 1),
- (res_inst_tac [("fo5","f")] (minimal RS monofun_cfun_arg) 1),
- (etac disjE 1),
- (contr_tac 1),
- (atac 1)
- ]);
--- a/src/HOLCF/Holcfb.ML Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Holcfb.ML Thu Oct 06 18:40:18 1994 +0100
@@ -9,10 +9,10 @@
open Holcfb;
(* ------------------------------------------------------------------------ *)
-(* <::nat=>nat=>bool is well-founded *)
+(* <::nat=>nat=>bool is a well-ordering *)
(* ------------------------------------------------------------------------ *)
-val well_founded_nat = prove_goal Nat.thy
+val well_ordering_nat = prove_goal Nat.thy
"!P. P(x::nat) --> (? y. P(y) & (! x. P(x) --> y <= x))"
(fn prems =>
[
@@ -45,7 +45,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (well_founded_nat RS spec RS mp RS exE) 1),
+ (rtac (well_ordering_nat RS spec RS mp RS exE) 1),
(atac 1),
(rtac selectI 1),
(atac 1)
@@ -150,3 +150,21 @@
val classical3 = (notE RS notI);
(* [| ?P ==> ~ ?P1; ?P ==> ?P1 |] ==> ~ ?P *)
+
+val nat_less_cases = prove_goal Nat.thy
+ "[| (m::nat) < n ==> P(n,m); m=n ==> P(n,m);n < m ==> P(n,m)|]==>P(n,m)"
+( fn prems =>
+ [
+ (res_inst_tac [("m1","n"),("n1","m")] (less_linear RS disjE) 1),
+ (etac disjE 2),
+ (etac (hd (tl (tl prems))) 1),
+ (etac (sym RS hd (tl prems)) 1),
+ (etac (hd prems) 1)
+ ]);
+
+
+
+
+
+
+
--- a/src/HOLCF/One.ML Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/One.ML Thu Oct 06 18:40:18 1994 +0100
@@ -68,15 +68,17 @@
(* one is flat *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw One.thy [flat_def] "flat(one)";
-by (rtac allI 1);
-by (rtac allI 1);
-by (res_inst_tac [("p","x")] oneE 1);
-by (asm_simp_tac ccc1_ss 1);
-by (res_inst_tac [("p","y")] oneE 1);
-by (asm_simp_tac (ccc1_ss addsimps dist_less_one) 1);
-by (asm_simp_tac ccc1_ss 1);
-val flat_one = result();
+val flat_one = prove_goalw One.thy [flat_def] "flat(one)"
+ (fn prems =>
+ [
+ (rtac allI 1),
+ (rtac allI 1),
+ (res_inst_tac [("p","x")] oneE 1),
+ (asm_simp_tac ccc1_ss 1),
+ (res_inst_tac [("p","y")] oneE 1),
+ (asm_simp_tac (ccc1_ss addsimps dist_less_one) 1),
+ (asm_simp_tac ccc1_ss 1)
+ ]);
(* ------------------------------------------------------------------------ *)
--- a/src/HOLCF/One.thy Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/One.thy Thu Oct 06 18:40:18 1994 +0100
@@ -3,27 +3,17 @@
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Introduve atomic type one = (void)u
+Introduce atomic type one = (void)u
-This is the first type that is introduced using a domain isomorphism.
-The type axiom
-
- arities one :: pcpo
+The type is axiomatized as the least solution of a domain equation.
+The functor term that specifies the domain equation is:
-and the continuity of the Isomorphisms are taken for granted. Since the
-type is not recursive, it could be easily introduced in a purely conservative
-style as it was used for the types sprod, ssum, lift. The definition of the
-ordering is canonical using abstraction and representation, but this would take
-again a lot of internal constants. It can easily be seen that the axioms below
-are consistent.
+ FT = <U,K_{void}>
-The partial ordering on type one is implicitly defined via the
-isomorphism axioms and the continuity of abs_one and rep_one.
+For details see chapter 5 of:
-We could also introduce the function less_one with definition
-
-less_one(x,y) = rep_one[x] << rep_one[y]
-
+[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
+ Dissertation, Technische Universit"at M"unchen, 1994
*)
--- a/src/HOLCF/Pcpo.thy Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Pcpo.thy Thu Oct 06 18:40:18 1994 +0100
@@ -1,38 +1,14 @@
-(* Title: HOLCF/pcpo.thy
- ID: $Id$
- Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
-Definition of class pcpo (pointed complete partial order)
-
-The prototype theory for this class is porder.thy
-
-*)
-
Pcpo = Porder +
-(* Introduction of new class. The witness is type void. *)
-
classes pcpo < po
-
-(* default class is still term *)
-(* void is the prototype in pcpo *)
-
arities void :: pcpo
consts
- UU :: "'a::pcpo" (* UU is the least element *)
+ UU :: "'a::pcpo"
rules
-(* class axioms: justification is theory Porder *)
-
-minimal "UU << x" (* witness is minimal_void *)
-
-cpo "is_chain(S) ==> ? x. range(S) <<| (x::('a::pcpo))"
- (* witness is cpo_void *)
- (* needs explicit type *)
-
-(* instance of UU for the prototype void *)
+minimal "UU << x"
+cpo "is_chain(S) ==> ? x. range(S) <<| x::('a::pcpo)"
inst_void_pcpo "(UU::void) = UU_void"
--- a/src/HOLCF/Porder.ML Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Porder.ML Thu Oct 06 18:40:18 1994 +0100
@@ -9,6 +9,21 @@
open Porder0;
open Porder;
+
+(* ------------------------------------------------------------------------ *)
+(* the reverse law of anti--symmetrie of << *)
+(* ------------------------------------------------------------------------ *)
+
+val antisym_less_inverse = prove_goal Porder.thy "x=y ==> x << y & y << x"
+(fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (rtac conjI 1),
+ ((rtac subst 1) THEN (rtac refl_less 2) THEN (atac 1)),
+ ((rtac subst 1) THEN (rtac refl_less 2) THEN (etac sym 1))
+ ]);
+
+
val box_less = prove_goal Porder.thy
"[| a << b; c << a; b << d|] ==> c << d"
(fn prems =>
@@ -72,20 +87,6 @@
(rtac refl_less 1)
]);
-(* ------------------------------------------------------------------------ *)
-(* Lemma for reasoning by cases on the natural numbers *)
-(* ------------------------------------------------------------------------ *)
-
-val nat_less_cases = prove_goal Porder.thy
- "[| (m::nat) < n ==> P(n,m); m=n ==> P(n,m);n < m ==> P(n,m)|]==>P(n,m)"
-( fn prems =>
- [
- (res_inst_tac [("m1","n"),("n1","m")] (less_linear RS disjE) 1),
- (etac disjE 2),
- (etac (hd (tl (tl prems))) 1),
- (etac (sym RS hd (tl prems)) 1),
- (etac (hd prems) 1)
- ]);
(* ------------------------------------------------------------------------ *)
(* The range of a chain is a totaly ordered << *)
@@ -123,7 +124,7 @@
(* ------------------------------------------------------------------------ *)
-(* technical lemmas about lub and is_lub, use above results about @ *)
+(* technical lemmas about lub and is_lub *)
(* ------------------------------------------------------------------------ *)
val lubI = prove_goal Porder.thy "(? x. M <<| x) ==> M <<| lub(M)"
@@ -303,19 +304,6 @@
(* ------------------------------------------------------------------------ *)
-(* the reverse law of anti--symmetrie of << *)
-(* ------------------------------------------------------------------------ *)
-
-val antisym_less_inverse = prove_goal Porder.thy "x=y ==> x << y & y << x"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac conjI 1),
- ((rtac subst 1) THEN (rtac refl_less 2) THEN (atac 1)),
- ((rtac subst 1) THEN (rtac refl_less 2) THEN (etac sym 1))
- ]);
-
-(* ------------------------------------------------------------------------ *)
(* results about finite chains *)
(* ------------------------------------------------------------------------ *)
--- a/src/HOLCF/ROOT.ML Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/ROOT.ML Thu Oct 06 18:40:18 1994 +0100
@@ -55,7 +55,7 @@
use_thy "One";
use_thy "Tr1";
use_thy "Tr2";
-
+
use_thy "HOLCF";
use_thy "Dnat";
@@ -64,7 +64,6 @@
use_thy "Stream2";
use_thy "Dlist";
-
use "../Pure/install_pp.ML";
print_depth 8;
--- a/src/HOLCF/Sprod3.thy Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Sprod3.thy Thu Oct 06 18:40:18 1994 +0100
@@ -18,6 +18,8 @@
ssnd :: "('a**'b)->'b"
ssplit :: "('a->'b->'c)->('a**'b)->'c"
+translations "x##y" => "spair[x][y]"
+
rules
inst_sprod_pcpo "(UU::'a**'b) = Ispair(UU,UU)"
@@ -28,12 +30,5 @@
end
-ML
-
-(* ----------------------------------------------------------------------*)
-(* parse translations for the above mixfix *)
-(* ----------------------------------------------------------------------*)
-
-val parse_translation = [("@spair",mk_cinfixtr "@spair")];
--- a/src/HOLCF/Stream.ML Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Stream.ML Thu Oct 06 18:40:18 1994 +0100
@@ -419,6 +419,30 @@
(REPEAT (atac 1))
]);
+(* prove induction using definition of admissibility
+ stream_reach rsp. stream_reach2
+ and finite induction stream_finite_ind *)
+
+val stream_ind = prove_goal Stream.thy
+"[|adm(P);\
+\ P(UU);\
+\ !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
+\ |] ==> P(s)"
+ (fn prems =>
+ [
+ (rtac (stream_reach2 RS subst) 1),
+ (rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
+ (resolve_tac prems 1),
+ (SELECT_GOAL (rewrite_goals_tac [stream_take_def]) 1),
+ (rtac ch2ch_fappL 1),
+ (rtac is_chain_iterate 1),
+ (rtac allI 1),
+ (rtac (stream_finite_ind RS spec) 1),
+ (REPEAT (resolve_tac prems 1)),
+ (REPEAT (atac 1))
+ ]);
+
+(* prove induction with usual LCF-Method using fixed point induction *)
val stream_ind = prove_goal Stream.thy
"[|adm(P);\
\ P(UU);\
@@ -440,6 +464,7 @@
(REPEAT (atac 1))
]);
+
(* ------------------------------------------------------------------------*)
(* simplify use of Co-induction *)
(* ------------------------------------------------------------------------*)
--- a/src/HOLCF/Stream.thy Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Stream.thy Thu Oct 06 18:40:18 1994 +0100
@@ -3,7 +3,18 @@
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Theory for streams without defined empty stream
+Theory for streams without defined empty stream
+ 'a stream = 'a ** ('a stream)u
+
+The type is axiomatized as the least solution of the domain equation above.
+The functor term that specifies the domain equation is:
+
+ FT = <**,K_{'a},U>
+
+For details see chapter 5 of:
+
+[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
+ Dissertation, Technische Universit"at M"unchen, 1994
*)
Stream = Dnat2 +
@@ -44,8 +55,9 @@
(* axiomatization of recursive type 'a stream *)
(* ----------------------------------------------------------------------- *)
(* ('a stream,stream_abs) is the initial F-algebra where *)
-(* F is the locally continuous functor determined by domain equation *)
-(* X = 'a ** (X)u *)
+(* F is the locally continuous functor determined by functor term FT. *)
+(* domain equation: 'a stream = 'a ** ('a stream)u *)
+(* functor term: FT = <**,K_{'a},U> *)
(* ----------------------------------------------------------------------- *)
(* stream_abs is an isomorphism with inverse stream_rep *)
(* identity is the least endomorphism on 'a stream *)
--- a/src/HOLCF/Tr1.thy Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Tr1.thy Thu Oct 06 18:40:18 1994 +0100
@@ -3,22 +3,17 @@
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Introduve the domain of truth values tr = {UU,TT,FF}
-
-This type is introduced using a domain isomorphism.
+Introduce the domain of truth values tr = one ++ one
-The type axiom
-
- arities tr :: pcpo
+The type is axiomatized as the least solution of a domain equation.
+The functor term that specifies the domain equation is:
-and the continuity of the Isomorphisms are taken for granted. Since the
-type is not recursive, it could be easily introduced in a purely conservative
-style as it was used for the types sprod, ssum, lift. The definition of the
-ordering is canonical using abstraction and representation, but this would take
-again a lot of internal constants. It can be easily seen that the axioms below
-are consistent.
+ FT = <++,K_{one},K_{one}>
-Partial Ordering is implicit in isomorphims abs_tr,rep_tr and their continuity
+For details see chapter 5 of:
+
+[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
+ Dissertation, Technische Universit"at M"unchen, 1994
*)
--- a/src/HOLCF/Tr2.thy Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Tr2.thy Thu Oct 06 18:40:18 1994 +0100
@@ -20,6 +20,10 @@
"neg" :: "tr -> tr"
+translations "x andalso y" => "trand[x][y]"
+ "x orelse y" => "tror[x][y]"
+ "If b then e1 else e2 fi" => "Icifte[b][e1][e2]"
+
rules
ifte_def "Icifte == (LAM t e1 e2.tr_when[e1][e2][t])"
@@ -29,29 +33,7 @@
end
-ML
-
-(* ----------------------------------------------------------------------*)
-(* translations for the above mixfixes *)
-(* ----------------------------------------------------------------------*)
-
-fun ciftetr ts =
- let val Cfapp = Const("fapp",dummyT) in
- Cfapp $
- (Cfapp $
- (Cfapp$Const("Icifte",dummyT)$(nth_elem (0,ts)))$
- (nth_elem (1,ts)))$
- (nth_elem (2,ts))
- end;
-
-
-val parse_translation = [("@andalso",mk_cinfixtr "@andalso"),
- ("@orelse",mk_cinfixtr "@orelse"),
- ("@cifte",ciftetr)];
-
-val print_translation = [];
-
--- a/src/HOLCF/ccc1.thy Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/ccc1.thy Thu Oct 06 18:40:18 1994 +0100
@@ -16,6 +16,7 @@
"@oo" :: "('b->'c)=>('a->'b)=>'a->'c" ("_ oo _" [101,100] 100)
"cop @oo" :: "('b->'c)->('a->'b)->'a->'c" ("cfcomp")
+translations "f1 oo f2" => "cfcomp[f1][f2]"
rules
@@ -24,15 +25,6 @@
end
-ML
-
-(* ----------------------------------------------------------------------*)
-(* parse translations for the above mixfix oo *)
-(* ----------------------------------------------------------------------*)
-
-val parse_translation = [("@oo",mk_cinfixtr "@oo")];
-val print_translation = [];
-