--- a/src/HOLCF/Cont.ML Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Cont.ML Mon Feb 17 10:57:11 1997 +0100
@@ -1,9 +1,9 @@
-(* Title: HOLCF/cont.ML
+(* Title: HOLCF/Cont.ML
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Lemmas for cont.thy
+Lemmas for Cont.thy
*)
open Cont;
@@ -12,7 +12,7 @@
(* access to definition *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "contlubI" Cont.thy [contlub]
+qed_goalw "contlubI" thy [contlub]
"! Y. is_chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))==>\
\ contlub(f)"
(fn prems =>
@@ -21,7 +21,7 @@
(atac 1)
]);
-qed_goalw "contlubE" Cont.thy [contlub]
+qed_goalw "contlubE" thy [contlub]
" contlub(f)==>\
\ ! Y. is_chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))"
(fn prems =>
@@ -31,7 +31,7 @@
]);
-qed_goalw "contI" Cont.thy [cont]
+qed_goalw "contI" thy [cont]
"! Y. is_chain(Y) --> range(% i.f(Y(i))) <<| f(lub(range(Y))) ==> cont(f)"
(fn prems =>
[
@@ -39,7 +39,7 @@
(atac 1)
]);
-qed_goalw "contE" Cont.thy [cont]
+qed_goalw "contE" thy [cont]
"cont(f) ==> ! Y. is_chain(Y) --> range(% i.f(Y(i))) <<| f(lub(range(Y)))"
(fn prems =>
[
@@ -48,7 +48,7 @@
]);
-qed_goalw "monofunI" Cont.thy [monofun]
+qed_goalw "monofunI" thy [monofun]
"! x y. x << y --> f(x) << f(y) ==> monofun(f)"
(fn prems =>
[
@@ -56,7 +56,7 @@
(atac 1)
]);
-qed_goalw "monofunE" Cont.thy [monofun]
+qed_goalw "monofunE" thy [monofun]
"monofun(f) ==> ! x y. x << y --> f(x) << f(y)"
(fn prems =>
[
@@ -73,7 +73,7 @@
(* monotone functions map chains to chains *)
(* ------------------------------------------------------------------------ *)
-qed_goal "ch2ch_monofun" Cont.thy
+qed_goal "ch2ch_monofun" thy
"[| monofun(f); is_chain(Y) |] ==> is_chain(%i. f(Y(i)))"
(fn prems =>
[
@@ -88,7 +88,7 @@
(* monotone functions map upper bound to upper bounds *)
(* ------------------------------------------------------------------------ *)
-qed_goal "ub2ub_monofun" Cont.thy
+qed_goal "ub2ub_monofun" thy
"[| monofun(f); range(Y) <| u|] ==> range(%i.f(Y(i))) <| f(u)"
(fn prems =>
[
@@ -103,7 +103,7 @@
(* left to right: monofun(f) & contlub(f) ==> cont(f) *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "monocontlub2cont" Cont.thy [cont]
+qed_goalw "monocontlub2cont" thy [cont]
"[|monofun(f);contlub(f)|] ==> cont(f)"
(fn prems =>
[
@@ -120,7 +120,7 @@
(* first a lemma about binary chains *)
(* ------------------------------------------------------------------------ *)
-qed_goal "binchain_cont" Cont.thy
+qed_goal "binchain_cont" thy
"[| cont(f); x << y |] ==> range(%i. f(if i = 0 then x else y)) <<| f(y)"
(fn prems =>
[
@@ -137,7 +137,7 @@
(* part1: cont(f) ==> monofun(f *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "cont2mono" Cont.thy [monofun]
+qed_goalw "cont2mono" thy [monofun]
"cont(f) ==> monofun(f)"
(fn prems =>
[
@@ -155,7 +155,7 @@
(* part2: cont(f) ==> contlub(f) *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "cont2contlub" Cont.thy [contlub]
+qed_goalw "cont2contlub" thy [contlub]
"cont(f) ==> contlub(f)"
(fn prems =>
[
@@ -170,7 +170,7 @@
(* monotone functions map finite chains to finite chains *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "monofun_finch2finch" Cont.thy [finite_chain_def]
+qed_goalw "monofun_finch2finch" thy [finite_chain_def]
"[| monofun f; finite_chain Y |] ==> finite_chain (%n. f (Y n))"
(fn prems =>
[
@@ -193,7 +193,7 @@
(* in both arguments *)
(* ------------------------------------------------------------------------ *)
-qed_goal "ch2ch_MF2L" Cont.thy
+qed_goal "ch2ch_MF2L" thy
"[|monofun(MF2); is_chain(F)|] ==> is_chain(%i. MF2 (F i) x)"
(fn prems =>
[
@@ -203,7 +203,7 @@
]);
-qed_goal "ch2ch_MF2R" Cont.thy
+qed_goal "ch2ch_MF2R" thy
"[|monofun(MF2(f)); is_chain(Y)|] ==> is_chain(%i. MF2 f (Y i))"
(fn prems =>
[
@@ -212,7 +212,7 @@
(atac 1)
]);
-qed_goal "ch2ch_MF2LR" Cont.thy
+qed_goal "ch2ch_MF2LR" thy
"[|monofun(MF2); !f.monofun(MF2(f)); is_chain(F); is_chain(Y)|] ==> \
\ is_chain(%i. MF2(F(i))(Y(i)))"
(fn prems =>
@@ -228,7 +228,7 @@
]);
-qed_goal "ch2ch_lubMF2R" Cont.thy
+qed_goal "ch2ch_lubMF2R" thy
"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
\ !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
\ is_chain(F);is_chain(Y)|] ==> \
@@ -248,7 +248,7 @@
]);
-qed_goal "ch2ch_lubMF2L" Cont.thy
+qed_goal "ch2ch_lubMF2L" thy
"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
\ !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
\ is_chain(F);is_chain(Y)|] ==> \
@@ -268,7 +268,7 @@
]);
-qed_goal "lub_MF2_mono" Cont.thy
+qed_goal "lub_MF2_mono" thy
"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
\ !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
\ is_chain(F)|] ==> \
@@ -288,7 +288,7 @@
(atac 1)
]);
-qed_goal "ex_lubMF2" Cont.thy
+qed_goal "ex_lubMF2" thy
"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
\ !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
\ is_chain(F); is_chain(Y)|] ==> \
@@ -327,7 +327,7 @@
]);
-qed_goal "diag_lubMF2_1" Cont.thy
+qed_goal "diag_lubMF2_1" thy
"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
\ !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
\ is_chain(FY);is_chain(TY)|] ==>\
@@ -371,7 +371,7 @@
(atac 1)
]);
-qed_goal "diag_lubMF2_2" Cont.thy
+qed_goal "diag_lubMF2_2" thy
"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
\ !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
\ is_chain(FY);is_chain(TY)|] ==>\
@@ -395,7 +395,7 @@
(* in both arguments *)
(* ------------------------------------------------------------------------ *)
-qed_goal "contlub_CF2" Cont.thy
+qed_goal "contlub_CF2" thy
"[|cont(CF2);!f.cont(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 =>
@@ -421,7 +421,7 @@
(* The following results are about application for functions in 'a=>'b *)
(* ------------------------------------------------------------------------ *)
-qed_goal "monofun_fun_fun" Cont.thy
+qed_goal "monofun_fun_fun" thy
"f1 << f2 ==> f1(x) << f2(x)"
(fn prems =>
[
@@ -429,7 +429,7 @@
(etac (less_fun RS iffD1 RS spec) 1)
]);
-qed_goal "monofun_fun_arg" Cont.thy
+qed_goal "monofun_fun_arg" thy
"[|monofun(f); x1 << x2|] ==> f(x1) << f(x2)"
(fn prems =>
[
@@ -438,7 +438,7 @@
(atac 1)
]);
-qed_goal "monofun_fun" Cont.thy
+qed_goal "monofun_fun" thy
"[|monofun(f1); monofun(f2); f1 << f2; x1 << x2|] ==> f1(x1) << f2(x2)"
(fn prems =>
[
@@ -455,7 +455,7 @@
(* continuity *)
(* ------------------------------------------------------------------------ *)
-qed_goal "mono2mono_MF1L" Cont.thy
+qed_goal "mono2mono_MF1L" thy
"[|monofun(c1)|] ==> monofun(%x. c1 x y)"
(fn prems =>
[
@@ -466,7 +466,7 @@
(atac 1)
]);
-qed_goal "cont2cont_CF1L" Cont.thy
+qed_goal "cont2cont_CF1L" thy
"[|cont(c1)|] ==> cont(%x. c1 x y)"
(fn prems =>
[
@@ -487,7 +487,7 @@
(********* Note "(%x.%y.c1 x y) = c1" ***********)
-qed_goal "mono2mono_MF1L_rev" Cont.thy
+qed_goal "mono2mono_MF1L_rev" thy
"!y.monofun(%x.c1 x y) ==> monofun(c1)"
(fn prems =>
[
@@ -500,7 +500,7 @@
(atac 1)
]);
-qed_goal "cont2cont_CF1L_rev" Cont.thy
+qed_goal "cont2cont_CF1L_rev" thy
"!y.cont(%x.c1 x y) ==> cont(c1)"
(fn prems =>
[
@@ -526,7 +526,7 @@
(* never used here *)
(* ------------------------------------------------------------------------ *)
-qed_goal "contlub_abstraction" Cont.thy
+qed_goal "contlub_abstraction" thy
"[|is_chain(Y::nat=>'a);!y.cont(%x.(c::'a=>'b=>'c) x y)|] ==>\
\ (%y.lub(range(%i.c (Y i) y))) = (lub(range(%i.%y.c (Y i) y)))"
(fn prems =>
@@ -543,7 +543,7 @@
]);
-qed_goal "mono2mono_app" Cont.thy
+qed_goal "mono2mono_app" thy
"[|monofun(ft);!x.monofun(ft(x));monofun(tt)|] ==>\
\ monofun(%x.(ft(x))(tt(x)))"
(fn prems =>
@@ -561,7 +561,7 @@
]);
-qed_goal "cont2contlub_app" Cont.thy
+qed_goal "cont2contlub_app" thy
"[|cont(ft);!x.cont(ft(x));cont(tt)|] ==> contlub(%x.(ft(x))(tt(x)))"
(fn prems =>
[
@@ -578,7 +578,7 @@
]);
-qed_goal "cont2cont_app" Cont.thy
+qed_goal "cont2cont_app" thy
"[|cont(ft);!x.cont(ft(x));cont(tt)|] ==>\
\ cont(%x.(ft(x))(tt(x)))"
(fn prems =>
@@ -609,7 +609,7 @@
(* The identity function is continuous *)
(* ------------------------------------------------------------------------ *)
-qed_goal "cont_id" Cont.thy "cont(% x.x)"
+qed_goal "cont_id" thy "cont(% x.x)"
(fn prems =>
[
(rtac contI 1),
@@ -618,13 +618,11 @@
(rtac refl 1)
]);
-
-
(* ------------------------------------------------------------------------ *)
(* constant functions are continuous *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "cont_const" Cont.thy [cont] "cont(%x.c)"
+qed_goalw "cont_const" thy [cont] "cont(%x.c)"
(fn prems =>
[
(strip_tac 1),
@@ -639,7 +637,7 @@
]);
-qed_goal "cont2cont_app3" Cont.thy
+qed_goal "cont2cont_app3" thy
"[|cont(f);cont(t) |] ==> cont(%x. f(t(x)))"
(fn prems =>
[
@@ -650,3 +648,13 @@
(atac 1)
]);
+(* ------------------------------------------------------------------------ *)
+(* A non-emptyness result for Cfun *)
+(* ------------------------------------------------------------------------ *)
+
+qed_goal "CfunI" thy "?x:Collect cont"
+ (fn prems =>
+ [
+ (rtac CollectI 1),
+ (rtac cont_const 1)
+ ]);