src/HOLCF/Cprod3.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 4721 c8a8482a8124
child 9245 428385c4bc50
permissions -rw-r--r--
made tutorial first;
     1 (*  Title:      HOLCF/cprod3.ML
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Lemmas for Cprod3.thy 
     7 *)
     8 
     9 open Cprod3;
    10 
    11 (* for compatibility with old HOLCF-Version *)
    12 qed_goal "inst_cprod_pcpo" thy "UU = (UU,UU)"
    13  (fn prems => 
    14         [
    15         (simp_tac (HOL_ss addsimps [UU_def,UU_cprod_def]) 1)
    16         ]);
    17 
    18 (* ------------------------------------------------------------------------ *)
    19 (* continuity of (_,_) , fst, snd                                           *)
    20 (* ------------------------------------------------------------------------ *)
    21 
    22 qed_goal "Cprod3_lemma1" Cprod3.thy 
    23 "chain(Y::(nat=>'a::cpo)) ==>\
    24 \ (lub(range(Y)),(x::'b::cpo)) =\
    25 \ (lub(range(%i. fst(Y i,x))),lub(range(%i. snd(Y i,x))))"
    26  (fn prems =>
    27         [
    28         (cut_facts_tac prems 1),
    29         (res_inst_tac [("f1","Pair")] (arg_cong RS cong) 1),
    30         (rtac lub_equal 1),
    31         (atac 1),
    32         (rtac (monofun_fst RS ch2ch_monofun) 1),
    33         (rtac ch2ch_fun 1),
    34         (rtac (monofun_pair1 RS ch2ch_monofun) 1),
    35         (atac 1),
    36         (rtac allI 1),
    37         (Simp_tac 1),
    38         (rtac sym 1),
    39         (Simp_tac 1),
    40         (rtac (lub_const RS thelubI) 1)
    41         ]);
    42 
    43 qed_goal "contlub_pair1" Cprod3.thy "contlub(Pair)"
    44  (fn prems =>
    45         [
    46         (rtac contlubI 1),
    47         (strip_tac 1),
    48         (rtac (expand_fun_eq RS iffD2) 1),
    49         (strip_tac 1),
    50         (stac (lub_fun RS thelubI) 1),
    51         (etac (monofun_pair1 RS ch2ch_monofun) 1),
    52         (rtac trans 1),
    53         (rtac (thelub_cprod RS sym) 2),
    54         (rtac ch2ch_fun 2),
    55         (etac (monofun_pair1 RS ch2ch_monofun) 2),
    56         (etac Cprod3_lemma1 1)
    57         ]);
    58 
    59 qed_goal "Cprod3_lemma2" Cprod3.thy 
    60 "chain(Y::(nat=>'a::cpo)) ==>\
    61 \ ((x::'b::cpo),lub(range Y)) =\
    62 \ (lub(range(%i. fst(x,Y i))),lub(range(%i. snd(x, Y i))))"
    63  (fn prems =>
    64         [
    65         (cut_facts_tac prems 1),
    66         (res_inst_tac [("f1","Pair")] (arg_cong RS cong) 1),
    67         (rtac sym 1),
    68         (Simp_tac 1),
    69         (rtac (lub_const RS thelubI) 1),
    70         (rtac lub_equal 1),
    71         (atac 1),
    72         (rtac (monofun_snd RS ch2ch_monofun) 1),
    73         (rtac (monofun_pair2 RS ch2ch_monofun) 1),
    74         (atac 1),
    75         (rtac allI 1),
    76         (Simp_tac 1)
    77         ]);
    78 
    79 qed_goal "contlub_pair2" Cprod3.thy "contlub(Pair(x))"
    80  (fn prems =>
    81         [
    82         (rtac contlubI 1),
    83         (strip_tac 1),
    84         (rtac trans 1),
    85         (rtac (thelub_cprod RS sym) 2),
    86         (etac (monofun_pair2 RS ch2ch_monofun) 2),
    87         (etac Cprod3_lemma2 1)
    88         ]);
    89 
    90 qed_goal "cont_pair1" Cprod3.thy "cont(Pair)"
    91 (fn prems =>
    92         [
    93         (rtac monocontlub2cont 1),
    94         (rtac monofun_pair1 1),
    95         (rtac contlub_pair1 1)
    96         ]);
    97 
    98 qed_goal "cont_pair2" Cprod3.thy "cont(Pair(x))"
    99 (fn prems =>
   100         [
   101         (rtac monocontlub2cont 1),
   102         (rtac monofun_pair2 1),
   103         (rtac contlub_pair2 1)
   104         ]);
   105 
   106 qed_goal "contlub_fst" Cprod3.thy "contlub(fst)"
   107  (fn prems =>
   108         [
   109         (rtac contlubI 1),
   110         (strip_tac 1),
   111         (stac (lub_cprod RS thelubI) 1),
   112         (atac 1),
   113         (Simp_tac 1)
   114         ]);
   115 
   116 qed_goal "contlub_snd" Cprod3.thy "contlub(snd)"
   117  (fn prems =>
   118         [
   119         (rtac contlubI 1),
   120         (strip_tac 1),
   121         (stac (lub_cprod RS thelubI) 1),
   122         (atac 1),
   123         (Simp_tac 1)
   124         ]);
   125 
   126 qed_goal "cont_fst" Cprod3.thy "cont(fst)"
   127 (fn prems =>
   128         [
   129         (rtac monocontlub2cont 1),
   130         (rtac monofun_fst 1),
   131         (rtac contlub_fst 1)
   132         ]);
   133 
   134 qed_goal "cont_snd" Cprod3.thy "cont(snd)"
   135 (fn prems =>
   136         [
   137         (rtac monocontlub2cont 1),
   138         (rtac monofun_snd 1),
   139         (rtac contlub_snd 1)
   140         ]);
   141 
   142 (* 
   143  -------------------------------------------------------------------------- 
   144  more lemmas for Cprod3.thy 
   145  
   146  -------------------------------------------------------------------------- 
   147 *)
   148 
   149 (* ------------------------------------------------------------------------ *)
   150 (* convert all lemmas to the continuous versions                            *)
   151 (* ------------------------------------------------------------------------ *)
   152 
   153 qed_goalw "beta_cfun_cprod" Cprod3.thy [cpair_def]
   154         "(LAM x y.(x,y))`a`b = (a,b)"
   155  (fn prems =>
   156         [
   157         (stac beta_cfun 1),
   158         (simp_tac (simpset() addsimps [cont_pair1,cont_pair2,cont2cont_CF1L]) 1),
   159         (stac beta_cfun 1),
   160         (rtac cont_pair2 1),
   161         (rtac refl 1)
   162         ]);
   163 
   164 qed_goalw "inject_cpair" Cprod3.thy [cpair_def]
   165         " <a,b>=<aa,ba>  ==> a=aa & b=ba"
   166  (fn prems =>
   167         [
   168         (cut_facts_tac prems 1),
   169         (dtac (beta_cfun_cprod RS subst) 1),
   170         (dtac (beta_cfun_cprod RS subst) 1),
   171         (etac Pair_inject 1),
   172         (fast_tac HOL_cs 1)
   173         ]);
   174 
   175 qed_goalw "inst_cprod_pcpo2" Cprod3.thy [cpair_def] "UU = <UU,UU>"
   176  (fn prems =>
   177         [
   178         (rtac sym 1),
   179         (rtac trans 1),
   180         (rtac beta_cfun_cprod 1),
   181         (rtac sym 1),
   182         (rtac inst_cprod_pcpo 1)
   183         ]);
   184 
   185 qed_goal "defined_cpair_rev" Cprod3.thy
   186  "<a,b> = UU ==> a = UU & b = UU"
   187  (fn prems =>
   188         [
   189         (cut_facts_tac prems 1),
   190         (dtac (inst_cprod_pcpo2 RS subst) 1),
   191         (etac inject_cpair 1)
   192         ]);
   193 
   194 qed_goalw "Exh_Cprod2" Cprod3.thy [cpair_def]
   195         "? a b. z=<a,b>"
   196  (fn prems =>
   197         [
   198         (rtac PairE 1),
   199         (rtac exI 1),
   200         (rtac exI 1),
   201         (etac (beta_cfun_cprod RS ssubst) 1)
   202         ]);
   203 
   204 qed_goalw "cprodE" Cprod3.thy [cpair_def]
   205 "[|!!x y. [|p=<x,y> |] ==> Q|] ==> Q"
   206  (fn prems =>
   207         [
   208         (rtac PairE 1),
   209         (resolve_tac prems 1),
   210         (etac (beta_cfun_cprod RS ssubst) 1)
   211         ]);
   212 
   213 qed_goalw "cfst2" Cprod3.thy [cfst_def,cpair_def] 
   214         "cfst`<x,y>=x"
   215  (fn prems =>
   216         [
   217         (cut_facts_tac prems 1),
   218         (stac beta_cfun_cprod 1),
   219         (stac beta_cfun 1),
   220         (rtac cont_fst 1),
   221         (Simp_tac  1)
   222         ]);
   223 
   224 qed_goalw "csnd2" Cprod3.thy [csnd_def,cpair_def] 
   225         "csnd`<x,y>=y"
   226  (fn prems =>
   227         [
   228         (cut_facts_tac prems 1),
   229         (stac beta_cfun_cprod 1),
   230         (stac beta_cfun 1),
   231         (rtac cont_snd 1),
   232         (Simp_tac  1)
   233         ]);
   234 
   235 qed_goal "cfst_strict" Cprod3.thy "cfst`UU = UU" (fn _ => [
   236              (simp_tac (HOL_ss addsimps [inst_cprod_pcpo2,cfst2]) 1)]);
   237 qed_goal "csnd_strict" Cprod3.thy "csnd`UU = UU" (fn _ => [
   238              (simp_tac (HOL_ss addsimps [inst_cprod_pcpo2,csnd2]) 1)]);
   239 
   240 qed_goalw "surjective_pairing_Cprod2" Cprod3.thy 
   241         [cfst_def,csnd_def,cpair_def] "<cfst`p , csnd`p> = p"
   242  (fn prems =>
   243         [
   244         (stac beta_cfun_cprod 1),
   245         (stac beta_cfun 1),
   246         (rtac cont_snd 1),
   247         (stac beta_cfun 1),
   248         (rtac cont_fst 1),
   249         (rtac (surjective_pairing RS sym) 1)
   250         ]);
   251 
   252 qed_goalw "less_cprod5c" Cprod3.thy [cfst_def,csnd_def,cpair_def]
   253  "<xa,ya> << <x,y> ==> xa<<x & ya << y"
   254  (fn prems =>
   255         [
   256         (cut_facts_tac prems 1),
   257         (rtac less_cprod4c 1),
   258         (dtac (beta_cfun_cprod RS subst) 1),
   259         (dtac (beta_cfun_cprod RS subst) 1),
   260         (atac 1)
   261         ]);
   262 
   263 qed_goalw "lub_cprod2" Cprod3.thy [cfst_def,csnd_def,cpair_def]
   264 "[|chain(S)|] ==> range(S) <<| \
   265 \ <(lub(range(%i. cfst`(S i)))) , lub(range(%i. csnd`(S i)))>"
   266  (fn prems =>
   267         [
   268         (cut_facts_tac prems 1),
   269         (stac beta_cfun_cprod 1),
   270         (stac (beta_cfun RS ext) 1),
   271         (rtac cont_snd 1),
   272         (stac (beta_cfun RS ext) 1),
   273         (rtac cont_fst 1),
   274         (rtac lub_cprod 1),
   275         (atac 1)
   276         ]);
   277 
   278 bind_thm ("thelub_cprod2", lub_cprod2 RS thelubI);
   279 (*
   280 chain ?S1 ==>
   281  lub (range ?S1) =
   282  <lub (range (%i. cfst`(?S1 i))), lub (range (%i. csnd`(?S1 i)))>" 
   283 *)
   284 qed_goalw "csplit2" Cprod3.thy [csplit_def]
   285         "csplit`f`<x,y> = f`x`y"
   286  (fn prems =>
   287         [
   288         (stac beta_cfun 1),
   289         (Simp_tac 1),
   290         (simp_tac (simpset() addsimps [cfst2,csnd2]) 1)
   291         ]);
   292 
   293 qed_goalw "csplit3" Cprod3.thy [csplit_def]
   294   "csplit`cpair`z=z"
   295  (fn prems =>
   296         [
   297         (stac beta_cfun 1),
   298         (Simp_tac 1),
   299         (simp_tac (simpset() addsimps [surjective_pairing_Cprod2]) 1)
   300         ]);
   301 
   302 (* ------------------------------------------------------------------------ *)
   303 (* install simplifier for Cprod                                             *)
   304 (* ------------------------------------------------------------------------ *)
   305 
   306 Addsimps [cfst2,csnd2,csplit2];
   307 
   308 val Cprod_rews = [cfst2,csnd2,csplit2];