src/HOLCF/Up3.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 5291 5706f0ef1d43
child 8161 bde1391fd0a5
permissions -rw-r--r--
made tutorial first;
     1 (*  Title:      HOLCF/Up3.ML
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Lemmas for Up3.thy
     7 *)
     8 
     9 open Up3;
    10 
    11 (* for compatibility with old HOLCF-Version *)
    12 qed_goal "inst_up_pcpo" thy "UU = Abs_Up(Inl ())"
    13  (fn prems => 
    14         [
    15         (simp_tac (HOL_ss addsimps [UU_def,UU_up_def]) 1)
    16         ]);
    17 
    18 (* -------------------------------------------------------------------------*)
    19 (* some lemmas restated for class pcpo                                      *)
    20 (* ------------------------------------------------------------------------ *)
    21 
    22 qed_goal "less_up3b" thy "~ Iup(x) << UU"
    23  (fn prems =>
    24         [
    25         (stac inst_up_pcpo 1),
    26         (rtac less_up2b 1)
    27         ]);
    28 
    29 qed_goal "defined_Iup2" thy "Iup(x) ~= UU"
    30  (fn prems =>
    31         [
    32         (stac inst_up_pcpo 1),
    33         (rtac defined_Iup 1)
    34         ]);
    35 
    36 (* ------------------------------------------------------------------------ *)
    37 (* continuity for Iup                                                       *)
    38 (* ------------------------------------------------------------------------ *)
    39 
    40 qed_goal "contlub_Iup" thy "contlub(Iup)"
    41  (fn prems =>
    42         [
    43         (rtac contlubI 1),
    44         (strip_tac 1),
    45         (rtac trans 1),
    46         (rtac (thelub_up1a RS sym) 2),
    47         (fast_tac HOL_cs 3),
    48         (etac (monofun_Iup RS ch2ch_monofun) 2),
    49         (res_inst_tac [("f","Iup")] arg_cong  1),
    50         (rtac lub_equal 1),
    51         (atac 1),
    52         (rtac (monofun_Ifup2 RS ch2ch_monofun) 1),
    53         (etac (monofun_Iup RS ch2ch_monofun) 1),
    54         (asm_simp_tac Up0_ss 1)
    55         ]);
    56 
    57 qed_goal "cont_Iup" thy "cont(Iup)"
    58  (fn prems =>
    59         [
    60         (rtac monocontlub2cont 1),
    61         (rtac monofun_Iup 1),
    62         (rtac contlub_Iup 1)
    63         ]);
    64 
    65 
    66 (* ------------------------------------------------------------------------ *)
    67 (* continuity for Ifup                                                     *)
    68 (* ------------------------------------------------------------------------ *)
    69 
    70 qed_goal "contlub_Ifup1" thy "contlub(Ifup)"
    71  (fn prems =>
    72         [
    73         (rtac contlubI 1),
    74         (strip_tac 1),
    75         (rtac trans 1),
    76         (rtac (thelub_fun RS sym) 2),
    77         (etac (monofun_Ifup1 RS ch2ch_monofun) 2),
    78         (rtac ext 1),
    79         (res_inst_tac [("p","x")] upE 1),
    80         (asm_simp_tac Up0_ss 1),
    81         (rtac (lub_const RS thelubI RS sym) 1),
    82         (asm_simp_tac Up0_ss 1),
    83         (etac contlub_cfun_fun 1)
    84         ]);
    85 
    86 
    87 qed_goal "contlub_Ifup2" thy "contlub(Ifup(f))"
    88  (fn prems =>
    89         [
    90         (rtac contlubI 1),
    91         (strip_tac 1),
    92         (rtac disjE 1),
    93         (stac thelub_up1a 2),
    94         (atac 2),
    95         (atac 2),
    96         (asm_simp_tac Up0_ss 2),
    97         (stac thelub_up1b 3),
    98         (atac 3),
    99         (atac 3),
   100         (fast_tac HOL_cs 1),
   101         (asm_simp_tac Up0_ss 2),
   102         (rtac (chain_UU_I_inverse RS sym) 2),
   103         (rtac allI 2),
   104         (res_inst_tac [("p","Y(i)")] upE 2),
   105         (asm_simp_tac Up0_ss 2),
   106         (rtac notE 2),
   107         (dtac spec 2),
   108         (etac spec 2),
   109         (atac 2),
   110         (stac contlub_cfun_arg 1),
   111         (etac (monofun_Ifup2 RS ch2ch_monofun) 1),
   112         (rtac lub_equal2 1),
   113         (rtac (monofun_Rep_CFun2 RS ch2ch_monofun) 2),
   114         (etac (monofun_Ifup2 RS ch2ch_monofun) 2),
   115         (etac (monofun_Ifup2 RS ch2ch_monofun) 2),
   116         (rtac (chain_mono2 RS exE) 1),
   117         (atac 2),
   118         (etac exE 1),
   119         (etac exE 1),
   120         (rtac exI 1),
   121         (res_inst_tac [("s","Iup(x)"),("t","Y(i)")] ssubst 1),
   122         (atac 1),
   123         (rtac defined_Iup2 1),
   124         (rtac exI 1),
   125         (strip_tac 1),
   126         (res_inst_tac [("p","Y(i)")] upE 1),
   127         (asm_simp_tac Up0_ss 2),
   128         (res_inst_tac [("P","Y(i) = UU")] notE 1),
   129         (fast_tac HOL_cs 1),
   130         (stac inst_up_pcpo 1),
   131         (atac 1)
   132         ]);
   133 
   134 qed_goal "cont_Ifup1" thy "cont(Ifup)"
   135  (fn prems =>
   136         [
   137         (rtac monocontlub2cont 1),
   138         (rtac monofun_Ifup1 1),
   139         (rtac contlub_Ifup1 1)
   140         ]);
   141 
   142 qed_goal "cont_Ifup2" thy "cont(Ifup(f))"
   143  (fn prems =>
   144         [
   145         (rtac monocontlub2cont 1),
   146         (rtac monofun_Ifup2 1),
   147         (rtac contlub_Ifup2 1)
   148         ]);
   149 
   150 
   151 (* ------------------------------------------------------------------------ *)
   152 (* continuous versions of lemmas for ('a)u                                  *)
   153 (* ------------------------------------------------------------------------ *)
   154 
   155 qed_goalw "Exh_Up1" thy [up_def] "z = UU | (? x. z = up`x)"
   156  (fn prems =>
   157         [
   158         (simp_tac (Up0_ss addsimps [cont_Iup]) 1),
   159         (stac inst_up_pcpo 1),
   160         (rtac Exh_Up 1)
   161         ]);
   162 
   163 qed_goalw "inject_up" thy [up_def] "up`x=up`y ==> x=y"
   164  (fn prems =>
   165         [
   166         (cut_facts_tac prems 1),
   167         (rtac inject_Iup 1),
   168         (etac box_equals 1),
   169         (simp_tac (Up0_ss addsimps [cont_Iup]) 1),
   170         (simp_tac (Up0_ss addsimps [cont_Iup]) 1)
   171         ]);
   172 
   173 qed_goalw "defined_up" thy [up_def] " up`x ~= UU"
   174  (fn prems =>
   175         [
   176         (simp_tac (Up0_ss addsimps [cont_Iup]) 1),
   177         (rtac defined_Iup2 1)
   178         ]);
   179 
   180 qed_goalw "upE1" thy [up_def] 
   181         "[| p=UU ==> Q; !!x. p=up`x==>Q|] ==>Q"
   182  (fn prems =>
   183         [
   184         (rtac upE 1),
   185         (resolve_tac prems 1),
   186         (etac (inst_up_pcpo RS ssubst) 1),
   187         (resolve_tac (tl prems) 1),
   188         (asm_simp_tac (Up0_ss addsimps [cont_Iup]) 1)
   189         ]);
   190 
   191 val tac = (simp_tac (simpset() addsimps [cont_Iup,cont_Ifup1,
   192                 cont_Ifup2,cont2cont_CF1L]) 1);
   193 
   194 qed_goalw "fup1" thy [up_def,fup_def] "fup`f`UU=UU"
   195  (fn prems =>
   196         [
   197         (stac inst_up_pcpo 1),
   198         (stac beta_cfun 1),
   199 	tac,
   200         (stac beta_cfun 1),
   201 	tac,
   202         (simp_tac (Up0_ss addsimps [cont_Iup,cont_Ifup1,cont_Ifup2]) 1)
   203         ]);
   204 
   205 qed_goalw "fup2" thy [up_def,fup_def] "fup`f`(up`x)=f`x"
   206  (fn prems =>
   207         [
   208         (stac beta_cfun 1),
   209         (rtac cont_Iup 1),
   210         (stac beta_cfun 1),
   211 	tac,
   212         (stac beta_cfun 1),
   213         (rtac cont_Ifup2 1),
   214         (simp_tac (Up0_ss addsimps [cont_Iup,cont_Ifup1,cont_Ifup2]) 1)
   215         ]);
   216 
   217 qed_goalw "less_up4b" thy [up_def,fup_def] "~ up`x << UU"
   218  (fn prems =>
   219         [
   220         (simp_tac (Up0_ss addsimps [cont_Iup]) 1),
   221         (rtac less_up3b 1)
   222         ]);
   223 
   224 qed_goalw "less_up4c" thy [up_def,fup_def]
   225          "(up`x << up`y) = (x<<y)"
   226  (fn prems =>
   227         [
   228         (simp_tac (Up0_ss addsimps [cont_Iup]) 1),
   229         (rtac less_up2c 1)
   230         ]);
   231 
   232 qed_goalw "thelub_up2a" thy [up_def,fup_def] 
   233 "[| chain(Y); ? i x. Y(i) = up`x |] ==>\
   234 \      lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))"
   235  (fn prems =>
   236         [
   237         (cut_facts_tac prems 1),
   238         (stac beta_cfun 1),
   239 	tac,
   240         (stac beta_cfun 1),
   241 	tac,
   242         (stac (beta_cfun RS ext) 1),
   243 	tac,
   244         (rtac thelub_up1a 1),
   245         (atac 1),
   246         (etac exE 1),
   247         (etac exE 1),
   248         (rtac exI 1),
   249         (rtac exI 1),
   250         (etac box_equals 1),
   251         (rtac refl 1),
   252         (simp_tac (Up0_ss addsimps [cont_Iup]) 1)
   253         ]);
   254 
   255 
   256 
   257 qed_goalw "thelub_up2b" thy [up_def,fup_def] 
   258 "[| chain(Y); ! i x. Y(i) ~= up`x |] ==> lub(range(Y)) = UU"
   259  (fn prems =>
   260         [
   261         (cut_facts_tac prems 1),
   262         (stac inst_up_pcpo 1),
   263         (rtac thelub_up1b 1),
   264         (atac 1),
   265         (strip_tac 1),
   266         (dtac spec 1),
   267         (dtac spec 1),
   268         (rtac swap 1),
   269         (atac 1),
   270         (dtac notnotD 1),
   271         (etac box_equals 1),
   272         (rtac refl 1),
   273         (simp_tac (Up0_ss addsimps [cont_Iup]) 1)
   274         ]);
   275 
   276 
   277 qed_goal "up_lemma2" thy  " (? x. z = up`x) = (z~=UU)"
   278  (fn prems =>
   279         [
   280         (rtac iffI 1),
   281         (etac exE 1),
   282         (hyp_subst_tac 1),
   283         (rtac defined_up 1),
   284         (res_inst_tac [("p","z")] upE1 1),
   285         (etac notE 1),
   286         (atac 1),
   287         (etac exI 1)
   288         ]);
   289 
   290 
   291 qed_goal "thelub_up2a_rev" thy  
   292 "[| chain(Y); lub(range(Y)) = up`x |] ==> ? i x. Y(i) = up`x"
   293  (fn prems =>
   294         [
   295         (cut_facts_tac prems 1),
   296         (rtac exE 1),
   297         (rtac chain_UU_I_inverse2 1),
   298         (rtac (up_lemma2 RS iffD1) 1),
   299         (etac exI 1),
   300         (rtac exI 1),
   301         (rtac (up_lemma2 RS iffD2) 1),
   302         (atac 1)
   303         ]);
   304 
   305 qed_goal "thelub_up2b_rev" thy  
   306 "[| chain(Y); lub(range(Y)) = UU |] ==> ! i x.  Y(i) ~= up`x"
   307  (fn prems =>
   308         [
   309         (cut_facts_tac prems 1),
   310         (rtac allI 1),
   311         (rtac (not_ex RS iffD1) 1),
   312         (rtac contrapos 1),
   313         (etac (up_lemma2 RS iffD1) 2),
   314         (fast_tac (HOL_cs addSDs [chain_UU_I RS spec]) 1)
   315         ]);
   316 
   317 
   318 qed_goal "thelub_up3" thy  
   319 "chain(Y) ==> lub(range(Y)) = UU |\
   320 \                lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))"
   321  (fn prems =>
   322         [
   323         (cut_facts_tac prems 1),
   324         (rtac disjE 1),
   325         (rtac disjI1 2),
   326         (rtac thelub_up2b 2),
   327         (atac 2),
   328         (atac 2),
   329         (rtac disjI2 2),
   330         (rtac thelub_up2a 2),
   331         (atac 2),
   332         (atac 2),
   333         (fast_tac HOL_cs 1)
   334         ]);
   335 
   336 qed_goal "fup3" thy "fup`up`x=x"
   337  (fn prems =>
   338         [
   339         (res_inst_tac [("p","x")] upE1 1),
   340         (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [fup1,fup2]) 1),
   341         (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [fup1,fup2]) 1)
   342         ]);
   343 
   344 (* ------------------------------------------------------------------------ *)
   345 (* install simplifier for ('a)u                                             *)
   346 (* ------------------------------------------------------------------------ *)
   347 
   348 Addsimps [fup1,fup2,defined_up];