Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/Cont.ML
changeset 9245 428385c4bc50
parent 8935 548901d05a0e
child 9248 e1dee89de037
equal deleted inserted replaced
9244:7edd3e5f26d4 9245:428385c4bc50 
     8 
     8 
     9 (* ------------------------------------------------------------------------ *)
 
     9 (* ------------------------------------------------------------------------ *)
 
    10 (* access to definition                                                     *)
 
    10 (* access to definition                                                     *)
 
    11 (* ------------------------------------------------------------------------ *)
 
    11 (* ------------------------------------------------------------------------ *)
 
    12 
    12 
    13 qed_goalw "contlubI" thy [contlub]
 
    13 val prems = goalw thy [contlub]
 
    14         "! Y. chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))==>\
 
    14         "! Y. chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))==>\
 
    15 \        contlub(f)"
 
    15 \        contlub(f)";
 
    16 (fn prems =>
 
    16 by (cut_facts_tac prems 1);
 
    17         [
 
    17 by (atac 1);
 
    18         (cut_facts_tac prems 1),
 
    18 qed "contlubI";
 
    19         (atac 1)
 
    19 
    20         ]);
 
    20 val prems = goalw thy [contlub]
 
    21 
       
    22 qed_goalw "contlubE" thy [contlub]
 
       
    23         " contlub(f)==>\
 
    21         " contlub(f)==>\
 
    24 \         ! Y. chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))"
 
    22 \         ! Y. chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))";
 
    25 (fn prems =>
 
    23 by (cut_facts_tac prems 1);
 
    26         [
 
    24 by (atac 1);
 
    27         (cut_facts_tac prems 1),
 
    25 qed "contlubE";
 
    28         (atac 1)
 
    26 
    29         ]);
 
    27 
    30 
    28 val prems = goalw thy [cont]
 
    31 
    29  "! Y. chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y))) ==> cont(f)";
 
    32 qed_goalw "contI" thy [cont]
 
    30 by (cut_facts_tac prems 1);
 
    33  "! Y. chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y))) ==> cont(f)"
 
    31 by (atac 1);
 
    34 (fn prems =>
 
    32 qed "contI";
 
    35         [
 
    33 
    36         (cut_facts_tac prems 1),
 
    34 val prems = goalw thy [cont]
 
    37         (atac 1)
 
    35  "cont(f) ==> ! Y. chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y)))";
 
    38         ]);
 
    36 by (cut_facts_tac prems 1);
 
    39 
    37 by (atac 1);
 
    40 qed_goalw "contE" thy [cont]
 
    38 qed "contE";
 
    41  "cont(f) ==> ! Y. chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y)))"
 
    39 
    42 (fn prems =>
 
    40 
    43         [
 
    41 val prems = goalw thy [monofun]
 
    44         (cut_facts_tac prems 1),
 
    42         "! x y. x << y --> f(x) << f(y) ==> monofun(f)";
 
    45         (atac 1)
 
    43 by (cut_facts_tac prems 1);
 
    46         ]);
 
    44 by (atac 1);
 
    47 
    45 qed "monofunI";
 
    48 
    46 
    49 qed_goalw "monofunI" thy [monofun]
 
    47 val prems = goalw thy [monofun]
 
    50         "! x y. x << y --> f(x) << f(y) ==> monofun(f)"
 
    48         "monofun(f) ==> ! x y. x << y --> f(x) << f(y)";
 
    51 (fn prems =>
 
    49 by (cut_facts_tac prems 1);
 
    52         [
 
    50 by (atac 1);
 
    53         (cut_facts_tac prems 1),
 
    51 qed "monofunE";
 
    54         (atac 1)
 
       
    55         ]);
 
       
    56 
       
    57 qed_goalw "monofunE" thy [monofun]
 
       
    58         "monofun(f) ==> ! x y. x << y --> f(x) << f(y)"
 
       
    59 (fn prems =>
 
       
    60         [
 
       
    61         (cut_facts_tac prems 1),
 
       
    62         (atac 1)
 
       
    63         ]);
 
       
    64 
    52 
    65 (* ------------------------------------------------------------------------ *)
 
    53 (* ------------------------------------------------------------------------ *)
 
    66 (* the main purpose of cont.thy is to show:                                 *)
 
    54 (* the main purpose of cont.thy is to show:                                 *)
 
    67 (*              monofun(f) & contlub(f)  <==> cont(f)                      *)
 
    55 (*              monofun(f) & contlub(f)  <==> cont(f)                      *)
 
    68 (* ------------------------------------------------------------------------ *)
 
    56 (* ------------------------------------------------------------------------ *)
 
    69 
    57 
    70 (* ------------------------------------------------------------------------ *)
 
    58 (* ------------------------------------------------------------------------ *)
 
    71 (* monotone functions map chains to chains                                  *)
 
    59 (* monotone functions map chains to chains                                  *)
 
    72 (* ------------------------------------------------------------------------ *)
 
    60 (* ------------------------------------------------------------------------ *)
 
    73 
    61 
    74 qed_goal "ch2ch_monofun" thy 
    62 val prems = goal thy 
    75         "[| monofun(f); chain(Y) |] ==> chain(%i. f(Y(i)))"
 
    63         "[| monofun(f); chain(Y) |] ==> chain(%i. f(Y(i)))";
 
    76 (fn prems =>
 
    64 by (cut_facts_tac prems 1);
 
    77         [
 
    65 by (rtac chainI 1);
 
    78         (cut_facts_tac prems 1),
 
    66 by (rtac allI 1);
 
    79         (rtac chainI 1),
 
    67 by (etac (monofunE RS spec RS spec RS mp) 1);
 
    80         (rtac allI 1),
 
    68 by (etac (chainE RS spec) 1);
 
    81         (etac (monofunE RS spec RS spec RS mp) 1),
 
    69 qed "ch2ch_monofun";
 
    82         (etac (chainE RS spec) 1)
 
       
    83         ]);
 
       
    84 
    70 
    85 (* ------------------------------------------------------------------------ *)
 
    71 (* ------------------------------------------------------------------------ *)
 
    86 (* monotone functions map upper bound to upper bounds                       *)
 
    72 (* monotone functions map upper bound to upper bounds                       *)
 
    87 (* ------------------------------------------------------------------------ *)
 
    73 (* ------------------------------------------------------------------------ *)
 
    88 
    74 
    89 qed_goal "ub2ub_monofun" thy 
    75 val prems = goal thy 
    90  "[| monofun(f); range(Y) <| u|]  ==> range(%i. f(Y(i))) <| f(u)"
 
    76  "[| monofun(f); range(Y) <| u|]  ==> range(%i. f(Y(i))) <| f(u)";
 
    91 (fn prems =>
 
    77 by (cut_facts_tac prems 1);
 
    92         [
 
    78 by (rtac ub_rangeI 1);
 
    93         (cut_facts_tac prems 1),
 
    79 by (rtac allI 1);
 
    94         (rtac ub_rangeI 1),
 
    80 by (etac (monofunE RS spec RS spec RS mp) 1);
 
    95         (rtac allI 1),
 
    81 by (etac (ub_rangeE RS spec) 1);
 
    96         (etac (monofunE RS spec RS spec RS mp) 1),
 
    82 qed "ub2ub_monofun";
 
    97         (etac (ub_rangeE RS spec) 1)
 
       
    98         ]);
 
       
    99 
    83 
   100 (* ------------------------------------------------------------------------ *)
 
    84 (* ------------------------------------------------------------------------ *)
 
   101 (* left to right: monofun(f) & contlub(f)  ==> cont(f)                     *)
 
    85 (* left to right: monofun(f) & contlub(f)  ==> cont(f)                     *)
 
   102 (* ------------------------------------------------------------------------ *)
 
    86 (* ------------------------------------------------------------------------ *)
 
   103 
    87 
   104 qed_goalw "monocontlub2cont" thy [cont]
 
    88 val prems = goalw thy [cont]
 
   105         "[|monofun(f);contlub(f)|] ==> cont(f)"
 
    89         "[|monofun(f);contlub(f)|] ==> cont(f)";
 
   106 (fn prems =>
 
    90 by (cut_facts_tac prems 1);
 
   107         [
 
    91 by (strip_tac 1);
 
   108         (cut_facts_tac prems 1),
 
    92 by (rtac thelubE 1);
 
   109         (strip_tac 1),
 
    93 by (etac ch2ch_monofun 1);
 
   110         (rtac thelubE 1),
 
    94 by (atac 1);
 
   111         (etac ch2ch_monofun 1),
 
    95 by (etac (contlubE RS spec RS mp RS sym) 1);
 
   112         (atac 1),
 
    96 by (atac 1);
 
   113         (etac (contlubE RS spec RS mp RS sym) 1),
 
    97 qed "monocontlub2cont";
 
   114         (atac 1)
 
       
   115         ]);
 
       
   116 
    98 
   117 (* ------------------------------------------------------------------------ *)
 
    99 (* ------------------------------------------------------------------------ *)
 
   118 (* first a lemma about binary chains                                        *)
 
   100 (* first a lemma about binary chains                                        *)
 
   119 (* ------------------------------------------------------------------------ *)
 
   101 (* ------------------------------------------------------------------------ *)
 
   120 
   102 
   121 qed_goal "binchain_cont" thy
 
   103 Goal "[| cont(f); x << y |]  \
 
   122 "[| cont(f); x << y |]  ==> range(%i::nat. f(if i = 0 then x else y)) <<| f(y)"
 
   104 \     ==> range(%i::nat. f(if i = 0 then x else y)) <<| f(y)";
 
   123 (fn prems => 
   105 by (rtac subst 1);
 
   124         [
 
   106 by (etac (contE RS spec RS mp) 2);
 
   125         (cut_facts_tac prems 1),
 
   107 by (etac bin_chain 2);
 
   126         (rtac subst 1), 
   108 by (res_inst_tac [("y","y")] arg_cong 1);
 
   127         (etac (contE RS spec RS mp) 2),
 
   109 by (etac (lub_bin_chain RS thelubI) 1);
 
   128         (etac bin_chain 2),
 
   110 qed "binchain_cont";
 
   129         (res_inst_tac [("y","y")] arg_cong 1),
 
       
   130         (etac (lub_bin_chain RS thelubI) 1)
 
       
   131         ]);
 
       
   132 
   111 
   133 (* ------------------------------------------------------------------------ *)
 
   112 (* ------------------------------------------------------------------------ *)
 
   134 (* right to left: cont(f) ==> monofun(f) & contlub(f)                      *)
 
   113 (* right to left: cont(f) ==> monofun(f) & contlub(f)                      *)
 
   135 (* part1:         cont(f) ==> monofun(f                                    *)
 
   114 (* part1:         cont(f) ==> monofun(f                                    *)
 
   136 (* ------------------------------------------------------------------------ *)
 
   115 (* ------------------------------------------------------------------------ *)
 
   137 
   116 
   138 qed_goalw "cont2mono" thy [monofun]
 
   117 Goalw [monofun] "cont(f) ==> monofun(f)";
 
   139         "cont(f) ==> monofun(f)"
 
   118 by (strip_tac 1);
 
   140 (fn prems =>
 
   119 by (dtac (binchain_cont RS is_ub_lub) 1);
 
   141         [
 
   120 by (auto_tac (claset(), simpset() addsplits [split_if_asm]));
 
   142         (cut_facts_tac prems 1),
 
   121 qed "cont2mono";
 
   143         (strip_tac 1),
 
       
   144         (res_inst_tac [("s","if 0 = 0 then x else y")] subst 1),
 
       
   145         (rtac (binchain_cont RS is_ub_lub) 2),
 
       
   146         (atac 2),
 
       
   147         (atac 2),
 
       
   148         (Simp_tac 1)
 
       
   149         ]);
 
       
   150 
   122 
   151 (* ------------------------------------------------------------------------ *)
 
   123 (* ------------------------------------------------------------------------ *)
 
   152 (* right to left: cont(f) ==> monofun(f) & contlub(f)                      *)
 
   124 (* right to left: cont(f) ==> monofun(f) & contlub(f)                      *)
 
   153 (* part2:         cont(f) ==>              contlub(f)                      *)
 
   125 (* part2:         cont(f) ==>              contlub(f)                      *)
 
   154 (* ------------------------------------------------------------------------ *)
 
   126 (* ------------------------------------------------------------------------ *)
 
   155 
   127 
   156 qed_goalw "cont2contlub" thy [contlub]
 
   128 Goalw [contlub] "cont(f) ==> contlub(f)";
 
   157         "cont(f) ==> contlub(f)"
 
   129 by (strip_tac 1);
 
   158 (fn prems =>
 
   130 by (rtac (thelubI RS sym) 1);
 
   159         [
 
   131 by (etac (contE RS spec RS mp) 1);
 
   160         (cut_facts_tac prems 1),
 
   132 by (atac 1);
 
   161         (strip_tac 1),
 
   133 qed "cont2contlub";
 
   162         (rtac (thelubI RS sym) 1),
 
   134 
   163         (etac (contE RS spec RS mp) 1),
 
   135 (* ------------------------------------------------------------------------ *)
 
   164         (atac 1)
 
   136 (* monotone functions map finite chains to finite chains                    *)
 
   165         ]);
 
   137 (* ------------------------------------------------------------------------ *)
 
   166 
   138 
   167 (* ------------------------------------------------------------------------ *)
 
   139 Goalw [finite_chain_def]
 
   168 (* monotone functions map finite chains to finite chains              	    *)
 
   140   "[| monofun f; finite_chain Y |] ==> finite_chain (%n. f (Y n))";
 
   169 (* ------------------------------------------------------------------------ *)
 
   141 by (force_tac (claset()  addSEs [ch2ch_monofun],
 
   170 
   142 	       simpset() addsimps [max_in_chain_def]) 1);
 
   171 qed_goalw "monofun_finch2finch" thy [finite_chain_def]
 
   143 qed "monofun_finch2finch";
 
   172   "[| monofun f; finite_chain Y |] ==> finite_chain (%n. f (Y n))" 
   144 
   173 (fn prems => 
   145 (* ------------------------------------------------------------------------ *)
 
   174 	[
 
   146 (* The same holds for continuous functions                                  *)
 
   175 	cut_facts_tac prems 1,
 
       
   176 	safe_tac HOL_cs,
 
       
   177 	fast_tac (HOL_cs addSEs [ch2ch_monofun]) 1,
 
       
   178 	fast_tac (HOL_cs addss (HOL_ss addsimps [max_in_chain_def])) 1
 
       
   179 	]);
 
       
   180 
       
   181 (* ------------------------------------------------------------------------ *)
 
       
   182 (* The same holds for continuous functions				    *)
 
       
   183 (* ------------------------------------------------------------------------ *)
 
   147 (* ------------------------------------------------------------------------ *)
 
   184 
   148 
   185 bind_thm ("cont_finch2finch", cont2mono RS monofun_finch2finch);
 
   149 bind_thm ("cont_finch2finch", cont2mono RS monofun_finch2finch);
 
   186 (* [| cont ?f; finite_chain ?Y |] ==> finite_chain (%n. ?f (?Y n)) *)
 
   150 (* [| cont ?f; finite_chain ?Y |] ==> finite_chain (%n. ?f (?Y n)) *)
 
   187 
   151 
   189 (* ------------------------------------------------------------------------ *)
 
   153 (* ------------------------------------------------------------------------ *)
 
   190 (* The following results are about a curried function that is monotone      *)
 
   154 (* The following results are about a curried function that is monotone      *)
 
   191 (* in both arguments                                                        *)
 
   155 (* in both arguments                                                        *)
 
   192 (* ------------------------------------------------------------------------ *)
 
   156 (* ------------------------------------------------------------------------ *)
 
   193 
   157 
   194 qed_goal "ch2ch_MF2L" thy 
   158 val prems = goal thy 
   195 "[|monofun(MF2); chain(F)|] ==> chain(%i. MF2 (F i) x)"
 
   159 "[|monofun(MF2); chain(F)|] ==> chain(%i. MF2 (F i) x)";
 
   196 (fn prems =>
 
   160 by (cut_facts_tac prems 1);
 
   197         [
 
   161 by (etac (ch2ch_monofun RS ch2ch_fun) 1);
 
   198         (cut_facts_tac prems 1),
 
   162 by (atac 1);
 
   199         (etac (ch2ch_monofun RS ch2ch_fun) 1),
 
   163 qed "ch2ch_MF2L";
 
   200         (atac 1)
 
   164 
   201         ]);
 
   165 
   202 
   166 val prems = goal thy 
   203 
   167 "[|monofun(MF2(f)); chain(Y)|] ==> chain(%i. MF2 f (Y i))";
 
   204 qed_goal "ch2ch_MF2R" thy 
   168 by (cut_facts_tac prems 1);
 
   205 "[|monofun(MF2(f)); chain(Y)|] ==> chain(%i. MF2 f (Y i))"
 
   169 by (etac ch2ch_monofun 1);
 
   206 (fn prems =>
 
   170 by (atac 1);
 
   207         [
 
   171 qed "ch2ch_MF2R";
 
   208         (cut_facts_tac prems 1),
 
   172 
   209         (etac ch2ch_monofun 1),
 
   173 val prems = goal thy 
   210         (atac 1)
 
       
   211         ]);
 
       
   212 
       
   213 qed_goal "ch2ch_MF2LR" thy 
       
   214 "[|monofun(MF2); !f. monofun(MF2(f)); chain(F); chain(Y)|] ==> \
 
   174 "[|monofun(MF2); !f. monofun(MF2(f)); chain(F); chain(Y)|] ==> \
 
   215 \  chain(%i. MF2(F(i))(Y(i)))"
 
   175 \  chain(%i. MF2(F(i))(Y(i)))";
 
   216  (fn prems =>
 
   176 by (cut_facts_tac prems 1);
 
   217         [
 
   177 by (rtac chainI 1);
 
   218         (cut_facts_tac prems 1),
 
   178 by (strip_tac 1 );
 
   219         (rtac chainI 1),
 
   179 by (rtac trans_less 1);
 
   220         (strip_tac 1 ),
 
   180 by (etac (ch2ch_MF2L RS chainE RS spec) 1);
 
   221         (rtac trans_less 1),
 
   181 by (atac 1);
 
   222         (etac (ch2ch_MF2L RS chainE RS spec) 1),
 
   182 by ((rtac (monofunE RS spec RS spec RS mp) 1) THEN (etac spec 1));
 
   223         (atac 1),
 
   183 by (etac (chainE RS spec) 1);
 
   224         ((rtac (monofunE RS spec RS spec RS mp) 1) THEN (etac spec 1)),
 
   184 qed "ch2ch_MF2LR";
 
   225         (etac (chainE RS spec) 1)
 
   185 
   226         ]);
 
   186 
   227 
   187 val prems = goal thy 
   228 
       
   229 qed_goal "ch2ch_lubMF2R" thy 
       
   230 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
 
   188 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
 
   231 \  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
 
   189 \  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
 
   232 \       chain(F);chain(Y)|] ==> \
 
   190 \       chain(F);chain(Y)|] ==> \
 
   233 \       chain(%j. lub(range(%i. MF2 (F j) (Y i))))"
 
   191 \       chain(%j. lub(range(%i. MF2 (F j) (Y i))))";
 
   234 (fn prems =>
 
   192 by (cut_facts_tac prems 1);
 
   235         [
 
   193 by (rtac (lub_mono RS allI RS chainI) 1);
 
   236         (cut_facts_tac prems 1),
 
   194 by ((rtac ch2ch_MF2R 1) THEN (etac spec 1));
 
   237         (rtac (lub_mono RS allI RS chainI) 1),
 
   195 by (atac 1);
 
   238         ((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
 
   196 by ((rtac ch2ch_MF2R 1) THEN (etac spec 1));
 
   239         (atac 1),
 
   197 by (atac 1);
 
   240         ((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
 
   198 by (strip_tac 1);
 
   241         (atac 1),
 
   199 by (rtac (chainE RS spec) 1);
 
   242         (strip_tac 1),
 
   200 by (etac ch2ch_MF2L 1);
 
   243         (rtac (chainE RS spec) 1),
 
   201 by (atac 1);
 
   244         (etac ch2ch_MF2L 1),
 
   202 qed "ch2ch_lubMF2R";
 
   245         (atac 1)
 
   203 
   246         ]);
 
   204 
   247 
   205 val prems = goal thy 
   248 
       
   249 qed_goal "ch2ch_lubMF2L" thy 
       
   250 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
 
   206 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
 
   251 \  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
 
   207 \  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
 
   252 \       chain(F);chain(Y)|] ==> \
 
   208 \       chain(F);chain(Y)|] ==> \
 
   253 \       chain(%i. lub(range(%j. MF2 (F j) (Y i))))"
 
   209 \       chain(%i. lub(range(%j. MF2 (F j) (Y i))))";
 
   254 (fn prems =>
 
   210 by (cut_facts_tac prems 1);
 
   255         [
 
   211 by (rtac (lub_mono RS allI RS chainI) 1);
 
   256         (cut_facts_tac prems 1),
 
   212 by (etac ch2ch_MF2L 1);
 
   257         (rtac (lub_mono RS allI RS chainI) 1),
 
   213 by (atac 1);
 
   258         (etac ch2ch_MF2L 1),
 
   214 by (etac ch2ch_MF2L 1);
 
   259         (atac 1),
 
   215 by (atac 1);
 
   260         (etac ch2ch_MF2L 1),
 
   216 by (strip_tac 1);
 
   261         (atac 1),
 
   217 by (rtac (chainE RS spec) 1);
 
   262         (strip_tac 1),
 
   218 by ((rtac ch2ch_MF2R 1) THEN (etac spec 1));
 
   263         (rtac (chainE RS spec) 1),
 
   219 by (atac 1);
 
   264         ((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
 
   220 qed "ch2ch_lubMF2L";
 
   265         (atac 1)
 
   221 
   266         ]);
 
   222 
   267 
   223 val prems = goal thy 
   268 
       
   269 qed_goal "lub_MF2_mono" thy 
       
   270 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
 
   224 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
 
   271 \  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
 
   225 \  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
 
   272 \       chain(F)|] ==> \
 
   226 \       chain(F)|] ==> \
 
   273 \       monofun(% x. lub(range(% j. MF2 (F j) (x))))"
 
   227 \       monofun(% x. lub(range(% j. MF2 (F j) (x))))";
 
   274 (fn prems =>
 
   228 by (cut_facts_tac prems 1);
 
   275         [
 
   229 by (rtac monofunI 1);
 
   276         (cut_facts_tac prems 1),
 
   230 by (strip_tac 1);
 
   277         (rtac monofunI 1),
 
   231 by (rtac lub_mono 1);
 
   278         (strip_tac 1),
 
   232 by (etac ch2ch_MF2L 1);
 
   279         (rtac lub_mono 1),
 
   233 by (atac 1);
 
   280         (etac ch2ch_MF2L 1),
 
   234 by (etac ch2ch_MF2L 1);
 
   281         (atac 1),
 
   235 by (atac 1);
 
   282         (etac ch2ch_MF2L 1),
 
   236 by (strip_tac 1);
 
   283         (atac 1),
 
   237 by ((rtac (monofunE RS spec RS spec RS mp) 1) THEN (etac spec 1));
 
   284         (strip_tac 1),
 
   238 by (atac 1);
 
   285         ((rtac (monofunE RS spec RS spec RS mp) 1) THEN (etac spec 1)),
 
   239 qed "lub_MF2_mono";
 
   286         (atac 1)
 
   240 
   287         ]);
 
   241 val prems = goal thy 
   288 
       
   289 qed_goal "ex_lubMF2" thy 
       
   290 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
 
   242 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
 
   291 \  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
 
   243 \  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
 
   292 \       chain(F); chain(Y)|] ==> \
 
   244 \       chain(F); chain(Y)|] ==> \
 
   293 \               lub(range(%j. lub(range(%i. MF2(F j) (Y i))))) =\
 
   245 \               lub(range(%j. lub(range(%i. MF2(F j) (Y i))))) =\
 
   294 \               lub(range(%i. lub(range(%j. MF2(F j) (Y i)))))"
 
   246 \               lub(range(%i. lub(range(%j. MF2(F j) (Y i)))))";
 
   295  (fn prems =>
 
   247 by (cut_facts_tac prems 1);
 
   296         [
 
   248 by (rtac antisym_less 1);
 
   297         (cut_facts_tac prems 1),
 
   249 by (rtac (ub_rangeI RSN (2,is_lub_thelub)) 1);
 
   298         (rtac antisym_less 1),
 
   250 by (etac ch2ch_lubMF2R 1);
 
   299         (rtac (ub_rangeI RSN (2,is_lub_thelub)) 1),
 
   251 by (REPEAT (atac 1));
 
   300         (etac ch2ch_lubMF2R 1),
 
   252 by (strip_tac 1);
 
   301         (REPEAT (atac 1)),
 
   253 by (rtac lub_mono 1);
 
   302         (strip_tac 1),
 
   254 by ((rtac ch2ch_MF2R 1) THEN (etac spec 1));
 
   303         (rtac lub_mono 1),
 
   255 by (atac 1);
 
   304         ((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
 
   256 by (etac ch2ch_lubMF2L 1);
 
   305         (atac 1),
 
   257 by (REPEAT (atac 1));
 
   306         (etac ch2ch_lubMF2L 1),
 
   258 by (strip_tac 1);
 
   307         (REPEAT (atac 1)),
 
   259 by (rtac is_ub_thelub 1);
 
   308         (strip_tac 1),
 
   260 by (etac ch2ch_MF2L 1);
 
   309         (rtac is_ub_thelub 1),
 
   261 by (atac 1);
 
   310         (etac ch2ch_MF2L 1),
 
   262 by (rtac (ub_rangeI RSN (2,is_lub_thelub)) 1);
 
   311         (atac 1),
 
   263 by (etac ch2ch_lubMF2L 1);
 
   312         (rtac (ub_rangeI RSN (2,is_lub_thelub)) 1),
 
   264 by (REPEAT (atac 1));
 
   313         (etac ch2ch_lubMF2L 1),
 
   265 by (strip_tac 1);
 
   314         (REPEAT (atac 1)),
 
   266 by (rtac lub_mono 1);
 
   315         (strip_tac 1),
 
   267 by (etac ch2ch_MF2L 1);
 
   316         (rtac lub_mono 1),
 
   268 by (atac 1);
 
   317         (etac ch2ch_MF2L 1),
 
   269 by (etac ch2ch_lubMF2R 1);
 
   318         (atac 1),
 
   270 by (REPEAT (atac 1));
 
   319         (etac ch2ch_lubMF2R 1),
 
   271 by (strip_tac 1);
 
   320         (REPEAT (atac 1)),
 
   272 by (rtac is_ub_thelub 1);
 
   321         (strip_tac 1),
 
   273 by ((rtac ch2ch_MF2R 1) THEN (etac spec 1));
 
   322         (rtac is_ub_thelub 1),
 
   274 by (atac 1);
 
   323         ((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
 
   275 qed "ex_lubMF2";
 
   324         (atac 1)
 
   276 
   325         ]);
 
   277 
   326 
   278 val prems = goal thy 
   327 
       
   328 qed_goal "diag_lubMF2_1" thy 
       
   329 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
 
   279 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
 
   330 \  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
 
   280 \  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
 
   331 \  chain(FY);chain(TY)|] ==>\
 
   281 \  chain(FY);chain(TY)|] ==>\
 
   332 \ lub(range(%i. lub(range(%j. MF2(FY(j))(TY(i)))))) =\
 
   282 \ lub(range(%i. lub(range(%j. MF2(FY(j))(TY(i)))))) =\
 
   333 \ lub(range(%i. MF2(FY(i))(TY(i))))"
 
   283 \ lub(range(%i. MF2(FY(i))(TY(i))))";
 
   334  (fn prems =>
 
   284 by (cut_facts_tac prems 1);
 
   335         [
 
   285 by (rtac antisym_less 1);
 
   336         (cut_facts_tac prems 1),
 
   286 by (rtac (ub_rangeI RSN (2,is_lub_thelub)) 1);
 
   337         (rtac antisym_less 1),
 
   287 by (etac ch2ch_lubMF2L 1);
 
   338         (rtac (ub_rangeI RSN (2,is_lub_thelub)) 1),
 
   288 by (REPEAT (atac 1));
 
   339         (etac ch2ch_lubMF2L 1),
 
   289 by (strip_tac 1 );
 
   340         (REPEAT (atac 1)),
 
   290 by (rtac lub_mono3 1);
 
   341         (strip_tac 1 ),
 
   291 by (etac ch2ch_MF2L 1);
 
   342         (rtac lub_mono3 1),
 
   292 by (REPEAT (atac 1));
 
   343         (etac ch2ch_MF2L 1),
 
   293 by (etac ch2ch_MF2LR 1);
 
   344         (REPEAT (atac 1)),
 
   294 by (REPEAT (atac 1));
 
   345         (etac ch2ch_MF2LR 1),
 
   295 by (rtac allI 1);
 
   346         (REPEAT (atac 1)),
 
   296 by (res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1);
 
   347         (rtac allI 1),
 
   297 by (res_inst_tac [("x","ia")] exI 1);
 
   348         (res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1),
 
   298 by (rtac (chain_mono RS mp) 1);
 
   349         (res_inst_tac [("x","ia")] exI 1),
 
   299 by (etac allE 1);
 
   350         (rtac (chain_mono RS mp) 1),
 
   300 by (etac ch2ch_MF2R 1);
 
   351         (etac allE 1),
 
   301 by (REPEAT (atac 1));
 
   352         (etac ch2ch_MF2R 1),
 
   302 by (hyp_subst_tac 1);
 
   353         (REPEAT (atac 1)),
 
   303 by (res_inst_tac [("x","ia")] exI 1);
 
   354         (hyp_subst_tac 1),
 
   304 by (rtac refl_less 1);
 
   355         (res_inst_tac [("x","ia")] exI 1),
 
   305 by (res_inst_tac [("x","i")] exI 1);
 
   356         (rtac refl_less 1),
 
   306 by (rtac (chain_mono RS mp) 1);
 
   357         (res_inst_tac [("x","i")] exI 1),
 
   307 by (etac ch2ch_MF2L 1);
 
   358         (rtac (chain_mono RS mp) 1),
 
   308 by (REPEAT (atac 1));
 
   359         (etac ch2ch_MF2L 1),
 
   309 by (rtac lub_mono 1);
 
   360         (REPEAT (atac 1)),
 
   310 by (etac ch2ch_MF2LR 1);
 
   361         (rtac lub_mono 1),
 
   311 by (REPEAT(atac 1));
 
   362         (etac ch2ch_MF2LR 1),
 
   312 by (etac ch2ch_lubMF2L 1);
 
   363         (REPEAT(atac 1)),
 
   313 by (REPEAT (atac 1));
 
   364         (etac ch2ch_lubMF2L 1),
 
   314 by (strip_tac 1 );
 
   365         (REPEAT (atac 1)),
 
   315 by (rtac is_ub_thelub 1);
 
   366         (strip_tac 1 ),
 
   316 by (etac ch2ch_MF2L 1);
 
   367         (rtac is_ub_thelub 1),
 
   317 by (atac 1);
 
   368         (etac ch2ch_MF2L 1),
 
   318 qed "diag_lubMF2_1";
 
   369         (atac 1)
 
   319 
   370         ]);
 
   320 val prems = goal thy 
   371 
       
   372 qed_goal "diag_lubMF2_2" thy 
       
   373 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
 
   321 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
 
   374 \  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
 
   322 \  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
 
   375 \  chain(FY);chain(TY)|] ==>\
 
   323 \  chain(FY);chain(TY)|] ==>\
 
   376 \ lub(range(%j. lub(range(%i. MF2(FY(j))(TY(i)))))) =\
 
   324 \ lub(range(%j. lub(range(%i. MF2(FY(j))(TY(i)))))) =\
 
   377 \ lub(range(%i. MF2(FY(i))(TY(i))))"
 
   325 \ lub(range(%i. MF2(FY(i))(TY(i))))";
 
   378  (fn prems =>
 
   326 by (cut_facts_tac prems 1);
 
   379         [
 
   327 by (rtac trans 1);
 
   380         (cut_facts_tac prems 1),
 
   328 by (rtac ex_lubMF2 1);
 
   381         (rtac trans 1),
 
   329 by (REPEAT (atac 1));
 
   382         (rtac ex_lubMF2 1),
 
   330 by (etac diag_lubMF2_1 1);
 
   383         (REPEAT (atac 1)),
 
   331 by (REPEAT (atac 1));
 
   384         (etac diag_lubMF2_1 1),
 
   332 qed "diag_lubMF2_2";
 
   385         (REPEAT (atac 1))
 
       
   386         ]);
 
       
   387 
   333 
   388 
   334 
   389 (* ------------------------------------------------------------------------ *)
 
   335 (* ------------------------------------------------------------------------ *)
 
   390 (* The following results are about a curried function that is continuous    *)
 
   336 (* The following results are about a curried function that is continuous    *)
 
   391 (* in both arguments                                                        *)
 
   337 (* in both arguments                                                        *)
 
   392 (* ------------------------------------------------------------------------ *)
 
   338 (* ------------------------------------------------------------------------ *)
 
   393 
   339 
   394 qed_goal "contlub_CF2" thy 
   340 val prems = goal thy 
   395 "[|cont(CF2);!f. cont(CF2(f));chain(FY);chain(TY)|] ==>\
 
   341 "[|cont(CF2);!f. cont(CF2(f));chain(FY);chain(TY)|] ==>\
 
   396 \ CF2(lub(range(FY)))(lub(range(TY))) = lub(range(%i. CF2(FY(i))(TY(i))))"
 
   342 \ CF2(lub(range(FY)))(lub(range(TY))) = lub(range(%i. CF2(FY(i))(TY(i))))";
 
   397  (fn prems =>
 
   343 by (cut_facts_tac prems 1);
 
   398         [
 
   344 by (stac ((hd prems) RS cont2contlub RS contlubE RS spec RS mp) 1);
 
   399         (cut_facts_tac prems 1),
 
   345 by (atac 1);
 
   400         (stac ((hd prems) RS cont2contlub RS contlubE RS spec RS mp) 1),
 
   346 by (stac thelub_fun 1);
 
   401         (atac 1),
 
   347 by (rtac ((hd prems) RS cont2mono RS ch2ch_monofun) 1);
 
   402         (stac thelub_fun 1),
 
   348 by (atac 1);
 
   403         (rtac ((hd prems) RS cont2mono RS ch2ch_monofun) 1),
 
   349 by (rtac trans 1);
 
   404         (atac 1),
 
   350 by (rtac (((hd (tl prems)) RS spec RS cont2contlub) RS contlubE RS                spec RS mp RS ext RS arg_cong RS arg_cong) 1);
 
   405         (rtac trans 1),
 
   351 by (atac 1);
 
   406         (rtac (((hd (tl prems)) RS spec RS cont2contlub) RS contlubE RS                spec RS mp RS ext RS arg_cong RS arg_cong) 1),
 
   352 by (rtac diag_lubMF2_2 1);
 
   407         (atac 1),
 
   353 by (etac cont2mono 1);
 
   408         (rtac diag_lubMF2_2 1),
 
   354 by (rtac allI 1);
 
   409         (etac cont2mono 1),
 
   355 by (etac allE 1);
 
   410         (rtac allI 1),
 
   356 by (etac cont2mono 1);
 
   411         (etac allE 1),
 
   357 by (REPEAT (atac 1));
 
   412         (etac cont2mono 1),
 
   358 qed "contlub_CF2";
 
   413         (REPEAT (atac 1))
 
       
   414         ]);
 
       
   415 
   359 
   416 (* ------------------------------------------------------------------------ *)
 
   360 (* ------------------------------------------------------------------------ *)
 
   417 (* The following results are about application for functions in 'a=>'b      *)
 
   361 (* The following results are about application for functions in 'a=>'b      *)
 
   418 (* ------------------------------------------------------------------------ *)
 
   362 (* ------------------------------------------------------------------------ *)
 
   419 
   363 
   420 qed_goal "monofun_fun_fun" thy 
   364 val prems = goal thy 
   421         "f1 << f2 ==> f1(x) << f2(x)"
 
   365         "f1 << f2 ==> f1(x) << f2(x)";
 
   422 (fn prems =>
 
   366 by (cut_facts_tac prems 1);
 
   423         [
 
   367 by (etac (less_fun RS iffD1 RS spec) 1);
 
   424         (cut_facts_tac prems 1),
 
   368 qed "monofun_fun_fun";
 
   425         (etac (less_fun RS iffD1 RS spec) 1)
 
   369 
   426         ]);
 
   370 val prems = goal thy 
   427 
   371         "[|monofun(f); x1 << x2|] ==> f(x1) << f(x2)";
 
   428 qed_goal "monofun_fun_arg" thy 
   372 by (cut_facts_tac prems 1);
 
   429         "[|monofun(f); x1 << x2|] ==> f(x1) << f(x2)"
 
   373 by (etac (monofunE RS spec RS spec RS mp) 1);
 
   430 (fn prems =>
 
   374 by (atac 1);
 
   431         [
 
   375 qed "monofun_fun_arg";
 
   432         (cut_facts_tac prems 1),
 
   376 
   433         (etac (monofunE RS spec RS spec RS mp) 1),
 
   377 val prems = goal thy 
   434         (atac 1)
 
   378 "[|monofun(f1); monofun(f2); f1 << f2; x1 << x2|] ==> f1(x1) << f2(x2)";
 
   435         ]);
 
   379 by (cut_facts_tac prems 1);
 
   436 
   380 by (rtac trans_less 1);
 
   437 qed_goal "monofun_fun" thy 
   381 by (etac monofun_fun_arg 1);
 
   438 "[|monofun(f1); monofun(f2); f1 << f2; x1 << x2|] ==> f1(x1) << f2(x2)"
 
   382 by (atac 1);
 
   439 (fn prems =>
 
   383 by (etac monofun_fun_fun 1);
 
   440         [
 
   384 qed "monofun_fun";
 
   441         (cut_facts_tac prems 1),
 
       
   442         (rtac trans_less 1),
 
       
   443         (etac monofun_fun_arg 1),
 
       
   444         (atac 1),
 
       
   445         (etac monofun_fun_fun 1)
 
       
   446         ]);
 
       
   447 
   385 
   448 
   386 
   449 (* ------------------------------------------------------------------------ *)
 
   387 (* ------------------------------------------------------------------------ *)
 
   450 (* The following results are about the propagation of monotonicity and      *)
 
   388 (* The following results are about the propagation of monotonicity and      *)
 
   451 (* continuity                                                               *)
 
   389 (* continuity                                                               *)
 
   452 (* ------------------------------------------------------------------------ *)
 
   390 (* ------------------------------------------------------------------------ *)
 
   453 
   391 
   454 qed_goal "mono2mono_MF1L" thy 
   392 val prems = goal thy 
   455         "[|monofun(c1)|] ==> monofun(%x. c1 x y)"
 
   393         "[|monofun(c1)|] ==> monofun(%x. c1 x y)";
 
   456 (fn prems =>
 
   394 by (cut_facts_tac prems 1);
 
   457         [
 
   395 by (rtac monofunI 1);
 
   458         (cut_facts_tac prems 1),
 
   396 by (strip_tac 1);
 
   459         (rtac monofunI 1),
 
   397 by (etac (monofun_fun_arg RS monofun_fun_fun) 1);
 
   460         (strip_tac 1),
 
   398 by (atac 1);
 
   461         (etac (monofun_fun_arg RS monofun_fun_fun) 1),
 
   399 qed "mono2mono_MF1L";
 
   462         (atac 1)
 
   400 
   463         ]);
 
   401 val prems = goal thy 
   464 
   402         "[|cont(c1)|] ==> cont(%x. c1 x y)";
 
   465 qed_goal "cont2cont_CF1L" thy 
   403 by (cut_facts_tac prems 1);
 
   466         "[|cont(c1)|] ==> cont(%x. c1 x y)"
 
   404 by (rtac monocontlub2cont 1);
 
   467 (fn prems =>
 
   405 by (etac (cont2mono RS mono2mono_MF1L) 1);
 
   468         [
 
   406 by (rtac contlubI 1);
 
   469         (cut_facts_tac prems 1),
 
   407 by (strip_tac 1);
 
   470         (rtac monocontlub2cont 1),
 
   408 by (rtac ((hd prems) RS cont2contlub RS contlubE RS spec RS mp RS ssubst) 1);
 
   471         (etac (cont2mono RS mono2mono_MF1L) 1),
 
   409 by (atac 1);
 
   472         (rtac contlubI 1),
 
   410 by (stac thelub_fun 1);
 
   473         (strip_tac 1),
 
   411 by (rtac ch2ch_monofun 1);
 
   474         (rtac ((hd prems) RS cont2contlub RS 
   412 by (etac cont2mono 1);
 
   475                 contlubE RS spec RS mp RS ssubst) 1),
 
   413 by (atac 1);
 
   476         (atac 1),
 
   414 by (rtac refl 1);
 
   477         (stac thelub_fun 1),
 
   415 qed "cont2cont_CF1L";
 
   478         (rtac ch2ch_monofun 1),
 
       
   479         (etac cont2mono 1),
 
       
   480         (atac 1),
 
       
   481         (rtac refl 1)
 
       
   482         ]);
 
       
   483 
   416 
   484 (*********  Note "(%x.%y.c1 x y) = c1" ***********)
 
   417 (*********  Note "(%x.%y.c1 x y) = c1" ***********)
 
   485 
   418 
   486 qed_goal "mono2mono_MF1L_rev" thy
 
   419 val prems = goal thy
 
   487         "!y. monofun(%x. c1 x y) ==> monofun(c1)"
 
   420         "!y. monofun(%x. c1 x y) ==> monofun(c1)";
 
   488 (fn prems =>
 
   421 by (cut_facts_tac prems 1);
 
   489         [
 
   422 by (rtac monofunI 1);
 
   490         (cut_facts_tac prems 1),
 
   423 by (strip_tac 1);
 
   491         (rtac monofunI 1),
 
   424 by (rtac (less_fun RS iffD2) 1);
 
   492         (strip_tac 1),
 
   425 by (strip_tac 1);
 
   493         (rtac (less_fun RS iffD2) 1),
 
   426 by (rtac ((hd prems) RS spec RS monofunE RS spec RS spec RS mp) 1);
 
   494         (strip_tac 1),
 
   427 by (atac 1);
 
   495         (rtac ((hd prems) RS spec RS monofunE RS spec RS spec RS mp) 1),
 
   428 qed "mono2mono_MF1L_rev";
 
   496         (atac 1)
 
   429 
   497         ]);
 
   430 val prems = goal thy
 
   498 
   431         "!y. cont(%x. c1 x y) ==> cont(c1)";
 
   499 qed_goal "cont2cont_CF1L_rev" thy
 
   432 by (cut_facts_tac prems 1);
 
   500         "!y. cont(%x. c1 x y) ==> cont(c1)"
 
   433 by (rtac monocontlub2cont 1);
 
   501 (fn prems =>
 
   434 by (rtac (cont2mono RS allI RS mono2mono_MF1L_rev ) 1);
 
   502         [
 
   435 by (etac spec 1);
 
   503         (cut_facts_tac prems 1),
 
   436 by (rtac contlubI 1);
 
   504         (rtac monocontlub2cont 1),
 
   437 by (strip_tac 1);
 
   505         (rtac (cont2mono RS allI RS mono2mono_MF1L_rev ) 1),
 
   438 by (rtac ext 1);
 
   506         (etac spec 1),
 
   439 by (stac thelub_fun 1);
 
   507         (rtac contlubI 1),
 
   440 by (rtac (cont2mono RS allI RS mono2mono_MF1L_rev RS ch2ch_monofun) 1);
 
   508         (strip_tac 1),
 
   441 by (etac spec 1);
 
   509         (rtac ext 1),
 
   442 by (atac 1);
 
   510         (stac thelub_fun 1),
 
   443 by (rtac ((hd prems) RS spec RS cont2contlub RS contlubE RS spec RS mp) 1);
 
   511         (rtac (cont2mono RS allI RS mono2mono_MF1L_rev RS ch2ch_monofun) 1),
 
   444 by (atac 1);
 
   512         (etac spec 1),
 
   445 qed "cont2cont_CF1L_rev";
 
   513         (atac 1),
 
       
   514         (rtac 
       
   515         ((hd prems) RS spec RS cont2contlub RS contlubE RS spec RS mp) 1),
 
       
   516         (atac 1)
 
       
   517         ]);
 
       
   518 
   446 
   519 (* ------------------------------------------------------------------------ *)
 
   447 (* ------------------------------------------------------------------------ *)
 
   520 (* What D.A.Schmidt calls continuity of abstraction                         *)
 
   448 (* What D.A.Schmidt calls continuity of abstraction                         *)
 
   521 (* never used here                                                          *)
 
   449 (* never used here                                                          *)
 
   522 (* ------------------------------------------------------------------------ *)
 
   450 (* ------------------------------------------------------------------------ *)
 
   523 
   451 
   524 qed_goal "contlub_abstraction" thy
 
   452 val prems = goal thy
 
   525 "[|chain(Y::nat=>'a);!y. cont(%x.(c::'a::cpo=>'b::cpo=>'c::cpo) x y)|] ==>\
 
   453 "[|chain(Y::nat=>'a);!y. cont(%x.(c::'a::cpo=>'b::cpo=>'c::cpo) x y)|] ==>\
 
   526 \ (%y. lub(range(%i. c (Y i) y))) = (lub(range(%i.%y. c (Y i) y)))"
 
   454 \ (%y. lub(range(%i. c (Y i) y))) = (lub(range(%i.%y. c (Y i) y)))";
 
   527  (fn prems =>
 
   455 by (cut_facts_tac prems 1);
 
   528         [
 
   456 by (rtac trans 1);
 
   529         (cut_facts_tac prems 1),
 
   457 by (rtac (cont2contlub RS contlubE RS spec RS mp) 2);
 
   530         (rtac trans 1),
 
   458 by (atac 3);
 
   531         (rtac (cont2contlub RS contlubE RS spec RS mp) 2),
 
   459 by (etac cont2cont_CF1L_rev 2);
 
   532         (atac 3),
 
   460 by (rtac ext 1);
 
   533         (etac cont2cont_CF1L_rev 2),
 
   461 by (rtac (cont2contlub RS contlubE RS spec RS mp RS sym) 1);
 
   534         (rtac ext 1), 
   462 by (etac spec 1);
 
   535         (rtac (cont2contlub RS contlubE RS spec RS mp RS sym) 1),
 
   463 by (atac 1);
 
   536         (etac spec 1),
 
   464 qed "contlub_abstraction";
 
   537         (atac 1)
 
   465 
   538         ]);
 
   466 val prems = goal thy 
   539 
       
   540 qed_goal "mono2mono_app" thy 
       
   541 "[|monofun(ft);!x. monofun(ft(x));monofun(tt)|] ==>\
 
   467 "[|monofun(ft);!x. monofun(ft(x));monofun(tt)|] ==>\
 
   542 \        monofun(%x.(ft(x))(tt(x)))"
 
   468 \        monofun(%x.(ft(x))(tt(x)))";
 
   543  (fn prems =>
 
   469 by (cut_facts_tac prems 1);
 
   544         [
 
   470 by (rtac monofunI 1);
 
   545         (cut_facts_tac prems 1),
 
   471 by (strip_tac 1);
 
   546         (rtac monofunI 1),
 
   472 by (res_inst_tac [("f1.0","ft(x)"),("f2.0","ft(y)")] monofun_fun 1);
 
   547         (strip_tac 1),
 
   473 by (etac spec 1);
 
   548         (res_inst_tac [("f1.0","ft(x)"),("f2.0","ft(y)")] monofun_fun 1),
 
   474 by (etac spec 1);
 
   549         (etac spec 1),
 
   475 by (etac (monofunE RS spec RS spec RS mp) 1);
 
   550         (etac spec 1),
 
   476 by (atac 1);
 
   551         (etac (monofunE RS spec RS spec RS mp) 1),
 
   477 by (etac (monofunE RS spec RS spec RS mp) 1);
 
   552         (atac 1),
 
   478 by (atac 1);
 
   553         (etac (monofunE RS spec RS spec RS mp) 1),
 
   479 qed "mono2mono_app";
 
   554         (atac 1)
 
   480 
   555         ]);
 
   481 
   556 
   482 val prems = goal thy 
   557 
   483 "[|cont(ft);!x. cont(ft(x));cont(tt)|] ==> contlub(%x.(ft(x))(tt(x)))";
 
   558 qed_goal "cont2contlub_app" thy 
   484 by (cut_facts_tac prems 1);
 
   559 "[|cont(ft);!x. cont(ft(x));cont(tt)|] ==> contlub(%x.(ft(x))(tt(x)))"
 
   485 by (rtac contlubI 1);
 
   560  (fn prems =>
 
   486 by (strip_tac 1);
 
   561         [
 
   487 by (res_inst_tac [("f3","tt")] (contlubE RS spec RS mp RS ssubst) 1);
 
   562         (cut_facts_tac prems 1),
 
   488 by (etac cont2contlub 1);
 
   563         (rtac contlubI 1),
 
   489 by (atac 1);
 
   564         (strip_tac 1),
 
   490 by (rtac contlub_CF2 1);
 
   565         (res_inst_tac [("f3","tt")] (contlubE RS spec RS mp RS ssubst) 1),
 
   491 by (REPEAT (atac 1));
 
   566         (etac cont2contlub 1),
 
   492 by (etac (cont2mono RS ch2ch_monofun) 1);
 
   567         (atac 1),
 
   493 by (atac 1);
 
   568         (rtac contlub_CF2 1),
 
   494 qed "cont2contlub_app";
 
   569         (REPEAT (atac 1)),
 
   495 
   570         (etac (cont2mono RS ch2ch_monofun) 1),
 
   496 
   571         (atac 1)
 
   497 Goal "[|cont(ft); !x. cont(ft(x)); cont(tt)|] ==> cont(%x.(ft(x))(tt(x)))";
 
   572         ]);
 
   498 by (blast_tac (claset() addIs [monocontlub2cont, mono2mono_app, cont2mono,
 
   573 
   499 			       cont2contlub_app]) 1);
 
   574 
   500 qed "cont2cont_app";
 
   575 qed_goal "cont2cont_app" thy 
       
   576 "[|cont(ft);!x. cont(ft(x));cont(tt)|] ==>\
 
       
   577 \        cont(%x.(ft(x))(tt(x)))"
 
       
   578  (fn prems =>
 
       
   579         [
 
       
   580         (rtac monocontlub2cont 1),
 
       
   581         (rtac mono2mono_app 1),
 
       
   582         (rtac cont2mono 1),
 
       
   583         (resolve_tac prems 1),
 
       
   584         (strip_tac 1),
 
       
   585         (rtac cont2mono 1),
 
       
   586         (cut_facts_tac prems 1),
 
       
   587         (etac spec 1),
 
       
   588         (rtac cont2mono 1),
 
       
   589         (resolve_tac prems 1),
 
       
   590         (rtac cont2contlub_app 1),
 
       
   591         (resolve_tac prems 1),
 
       
   592         (resolve_tac prems 1),
 
       
   593         (resolve_tac prems 1)
 
       
   594         ]);
 
       
   595 
   501 
   596 
   502 
   597 bind_thm ("cont2cont_app2", allI RSN (2,cont2cont_app));
 
   503 bind_thm ("cont2cont_app2", allI RSN (2,cont2cont_app));
 
   598 (*  [| cont ?ft; !!x. cont (?ft x); cont ?tt |] ==> *)
 
   504 (*  [| cont ?ft; !!x. cont (?ft x); cont ?tt |] ==> *)
 
   599 (*        cont (%x. ?ft x (?tt x))                    *)
 
   505 (*        cont (%x. ?ft x (?tt x))                    *)
 
   601 
   507 
   602 (* ------------------------------------------------------------------------ *)
 
   508 (* ------------------------------------------------------------------------ *)
 
   603 (* The identity function is continuous                                      *)
 
   509 (* The identity function is continuous                                      *)
 
   604 (* ------------------------------------------------------------------------ *)
 
   510 (* ------------------------------------------------------------------------ *)
 
   605 
   511 
   606 qed_goal "cont_id" thy "cont(% x. x)"
 
   512 val prems = goal thy "cont(% x. x)";
 
   607  (fn prems =>
 
   513 by (rtac contI 1);
 
   608         [
 
   514 by (strip_tac 1);
 
   609         (rtac contI 1),
 
   515 by (etac thelubE 1);
 
   610         (strip_tac 1),
 
   516 by (rtac refl 1);
 
   611         (etac thelubE 1),
 
   517 qed "cont_id";
 
   612         (rtac refl 1)
 
       
   613         ]);
 
       
   614 
   518 
   615 (* ------------------------------------------------------------------------ *)
 
   519 (* ------------------------------------------------------------------------ *)
 
   616 (* constant functions are continuous                                        *)
 
   520 (* constant functions are continuous                                        *)
 
   617 (* ------------------------------------------------------------------------ *)
 
   521 (* ------------------------------------------------------------------------ *)
 
   618 
   522 
   619 qed_goalw "cont_const" thy [cont] "cont(%x. c)"
 
   523 val prems = goalw thy [cont] "cont(%x. c)";
 
   620  (fn prems =>
 
   524 by (strip_tac 1);
 
   621         [
 
   525 by (rtac is_lubI 1);
 
   622         (strip_tac 1),
 
   526 by (rtac conjI 1);
 
   623         (rtac is_lubI 1),
 
   527 by (rtac ub_rangeI 1);
 
   624         (rtac conjI 1),
 
   528 by (strip_tac 1);
 
   625         (rtac ub_rangeI 1),
 
   529 by (rtac refl_less 1);
 
   626         (strip_tac 1),
 
   530 by (strip_tac 1);
 
   627         (rtac refl_less 1),
 
   531 by (dtac ub_rangeE 1);
 
   628         (strip_tac 1),
 
   532 by (etac spec 1);
 
   629         (dtac ub_rangeE 1),
 
   533 qed "cont_const";
 
   630         (etac spec 1)
 
   534 
   631         ]);
 
   535 
   632 
   536 Goal "[|cont(f); cont(t) |] ==> cont(%x. f(t(x)))";
 
   633 
   537 by (best_tac (claset() addIs [ cont2cont_app2, cont_const]) 1);
 
   634 qed_goal "cont2cont_app3" thy 
   538 qed "cont2cont_app3";
 
   635  "[|cont(f);cont(t) |] ==> cont(%x. f(t(x)))"
 
       
   636  (fn prems =>
 
       
   637         [
 
       
   638         (cut_facts_tac prems 1),
 
       
   639         (rtac cont2cont_app2 1),
 
       
   640         (rtac cont_const 1),
 
       
   641         (atac 1),
 
       
   642         (atac 1)
 
       
   643         ]);
 
       
   644 
   539 
   645 (* ------------------------------------------------------------------------ *)
 
   540 (* ------------------------------------------------------------------------ *)
 
   646 (* A non-emptyness result for Cfun                                          *)
 
   541 (* A non-emptyness result for Cfun                                          *)
 
   647 (* ------------------------------------------------------------------------ *)
 
   542 (* ------------------------------------------------------------------------ *)
 
   648 
   543 
   649 qed_goal "CfunI" thy "?x:Collect cont"
 
   544 val prems = goal thy "?x:Collect cont";
 
   650  (fn prems =>
 
   545 by (rtac CollectI 1);
 
   651         [
 
   546 by (rtac cont_const 1);
 
   652         (rtac CollectI 1),
 
   547 qed "CfunI";
 
   653         (rtac cont_const 1)
 
   548 
   654         ]);
 
   549 (* ------------------------------------------------------------------------ *)
 
   655 
   550 (* some properties of flat                                                  *)
 
   656 (* ------------------------------------------------------------------------ *)
 
   551 (* ------------------------------------------------------------------------ *)
 
   657 (* some properties of flat			 			    *)
 
   552 
   658 (* ------------------------------------------------------------------------ *)
 
   553 val prems = goalw thy [monofun]
 
   659 
   554   "f UU = UU ==> monofun (f::'a::flat=>'b::pcpo)";
 
   660 qed_goalw "flatdom2monofun" thy [monofun]
 
   555 by (cut_facts_tac prems 1);
 
   661   "f UU = UU ==> monofun (f::'a::flat=>'b::pcpo)" 
   556 by (strip_tac 1);
 
   662 (fn prems => 
   557 by (dtac (ax_flat RS spec RS spec RS mp) 1);
 
   663 	[
 
   558 by (fast_tac ((HOL_cs addss (simpset() addsimps [minimal]))) 1);
 
   664 	cut_facts_tac prems 1,
 
   559 qed "flatdom2monofun";
 
   665 	strip_tac 1,
 
       
   666 	dtac (ax_flat RS spec RS spec RS mp) 1,
 
       
   667 	fast_tac ((HOL_cs addss (simpset() addsimps [minimal]))) 1
 
       
   668 	]);
 
       
   669 
   560 
   670 
   561 
   671 Goal "monofun f ==> cont(f::'a::chfin=>'b::pcpo)";
 
   562 Goal "monofun f ==> cont(f::'a::chfin=>'b::pcpo)";
 
   672 by (rtac monocontlub2cont 1);
 
   563 by (rtac monocontlub2cont 1);
 
   673 by ( atac 1);
 
   564 by ( atac 1);
isabelle