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