src/HOLCF/Cont.ML

-(*  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;
 
 (* ------------------------------------------------------------------------ *)
 (* 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 =>
         [
         (cut_facts_tac prems 1),
         (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 =>
         [
         (cut_facts_tac prems 1),
         (atac 1)
         ]);
 
 
-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 =>
         [
         (cut_facts_tac prems 1),
         (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 =>
         [
         (cut_facts_tac prems 1),
         (atac 1)
         ]);
 
 
-qed_goalw "monofunI" Cont.thy [monofun]
+qed_goalw "monofunI" thy [monofun]
         "! x y. x << y --> f(x) << f(y) ==> monofun(f)"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
         (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 =>
         [
         (cut_facts_tac prems 1),
         (atac 1)

 
 (* ------------------------------------------------------------------------ *)
 (* 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 =>
         [
         (cut_facts_tac prems 1),
         (rtac is_chainI 1),

 
 (* ------------------------------------------------------------------------ *)
 (* 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 =>
         [
         (cut_facts_tac prems 1),
         (rtac ub_rangeI 1),

 
 (* ------------------------------------------------------------------------ *)
 (* 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 =>
         [
         (cut_facts_tac prems 1),
         (strip_tac 1),

 
 (* ------------------------------------------------------------------------ *)
 (* 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 => 
         [
         (cut_facts_tac prems 1),
         (rtac subst 1), 

 (* ------------------------------------------------------------------------ *)
 (* right to left: cont(f) ==> monofun(f) & contlub(f)                      *)
 (* part1:         cont(f) ==> monofun(f                                    *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goalw "cont2mono" Cont.thy [monofun]
+qed_goalw "cont2mono" thy [monofun]
         "cont(f) ==> monofun(f)"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
         (strip_tac 1),

 (* ------------------------------------------------------------------------ *)
 (* right to left: cont(f) ==> monofun(f) & contlub(f)                      *)
 (* part2:         cont(f) ==>              contlub(f)                      *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goalw "cont2contlub" Cont.thy [contlub]
+qed_goalw "cont2contlub" thy [contlub]
         "cont(f) ==> contlub(f)"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
         (strip_tac 1),

 
 (* ------------------------------------------------------------------------ *)
 (* 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 => 
 	[
 	cut_facts_tac prems 1,
 	safe_tac HOL_cs,

 (* ------------------------------------------------------------------------ *)
 (* The following results are about a curried function that is monotone      *)
 (* 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 =>
         [
         (cut_facts_tac prems 1),
         (etac (ch2ch_monofun RS ch2ch_fun) 1),
         (atac 1)
         ]);
 
 
-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 =>
         [
         (cut_facts_tac prems 1),
         (etac ch2ch_monofun 1),
         (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 =>
         [
         (cut_facts_tac prems 1),

         ((rtac (monofunE RS spec RS spec RS mp) 1) THEN (etac spec 1)),
         (etac (is_chainE RS spec) 1)
         ]);
 
 
-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)|] ==> \
 \       is_chain(%j. lub(range(%i. MF2 (F j) (Y i))))"
 (fn prems =>

         (etac ch2ch_MF2L 1),
         (atac 1)
         ]);
 
 
-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)|] ==> \
 \       is_chain(%i. lub(range(%j. MF2 (F j) (Y i))))"
 (fn prems =>

         ((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
         (atac 1)
         ]);
 
 
-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)|] ==> \
 \       monofun(% x.lub(range(% j.MF2 (F j) (x))))"
 (fn prems =>

         (strip_tac 1),
         ((rtac (monofunE RS spec RS spec RS mp) 1) THEN (etac spec 1)),
         (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)|] ==> \
 \               lub(range(%j. lub(range(%i. MF2(F j) (Y i))))) =\
 \               lub(range(%i. lub(range(%j. MF2(F j) (Y i)))))"

         ((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
         (atac 1)
         ]);
 
 
-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)|] ==>\
 \ lub(range(%i. lub(range(%j. MF2(FY(j))(TY(i)))))) =\
 \ lub(range(%i. MF2(FY(i))(TY(i))))"

         (rtac is_ub_thelub 1),
         (etac ch2ch_MF2L 1),
         (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)|] ==>\
 \ lub(range(%j. lub(range(%i. MF2(FY(j))(TY(i)))))) =\
 \ lub(range(%i. MF2(FY(i))(TY(i))))"

 (* ------------------------------------------------------------------------ *)
 (* The following results are about a curried function that is continuous    *)
 (* 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 =>
         [
         (cut_facts_tac prems 1),

 
 (* ------------------------------------------------------------------------ *)
 (* 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 =>
         [
         (cut_facts_tac prems 1),
         (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 =>
         [
         (cut_facts_tac prems 1),
         (etac (monofunE RS spec RS spec RS mp) 1),
         (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 =>
         [
         (cut_facts_tac prems 1),
         (rtac trans_less 1),

 (* ------------------------------------------------------------------------ *)
 (* The following results are about the propagation of monotonicity and      *)
 (* continuity                                                               *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goal "mono2mono_MF1L" Cont.thy 
+qed_goal "mono2mono_MF1L" thy 
         "[|monofun(c1)|] ==> monofun(%x. c1 x y)"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
         (rtac monofunI 1),
         (strip_tac 1),
         (etac (monofun_fun_arg RS monofun_fun_fun) 1),
         (atac 1)
         ]);
 
-qed_goal "cont2cont_CF1L" Cont.thy 
+qed_goal "cont2cont_CF1L" thy 
         "[|cont(c1)|] ==> cont(%x. c1 x y)"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
         (rtac monocontlub2cont 1),

         (rtac refl 1)
         ]);
 
 (*********  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 =>
         [
         (cut_facts_tac prems 1),
         (rtac monofunI 1),

         (strip_tac 1),
         (rtac ((hd prems) RS spec RS monofunE RS spec RS spec RS mp) 1),
         (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 =>
         [
         (cut_facts_tac prems 1),
         (rtac monocontlub2cont 1),

 (* ------------------------------------------------------------------------ *)
 (* What D.A.Schmidt calls continuity of abstraction                         *)
 (* 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 =>
         [
         (cut_facts_tac prems 1),

         (etac spec 1),
         (atac 1)
         ]);
 
 
-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 =>
         [
         (cut_facts_tac prems 1),

         (etac (monofunE RS spec RS spec RS mp) 1),
         (atac 1)
         ]);
 
 
-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 =>
         [
         (cut_facts_tac prems 1),
         (rtac contlubI 1),

         (etac (cont2mono RS ch2ch_monofun) 1),
         (atac 1)
         ]);
 
 
-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 =>
         [
         (rtac monocontlub2cont 1),

 
 (* ------------------------------------------------------------------------ *)
 (* 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),
         (strip_tac 1),
         (etac thelubE 1),
         (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),
         (rtac is_lubI 1),
         (rtac conjI 1),

         (dtac ub_rangeE 1),
         (etac spec 1)
         ]);
 
 
-qed_goal "cont2cont_app3" Cont.thy 
+qed_goal "cont2cont_app3" thy 
  "[|cont(f);cont(t) |] ==> cont(%x. f(t(x)))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (rtac cont2cont_app2 1),
         (rtac cont_const 1),
         (atac 1),
         (atac 1)
         ]);
 
+(* ------------------------------------------------------------------------ *)
+(* A non-emptyness result for Cfun                                          *)
+(* ------------------------------------------------------------------------ *)
+
+qed_goal "CfunI" thy "?x:Collect cont"
+ (fn prems =>
+        [
+        (rtac CollectI 1),
+        (rtac cont_const 1)
+        ]);