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