src/HOLCF/porder.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 297 5ef75ff3baeb
permissions -rw-r--r--
tidying
     1 (*  Title: 	HOLCF/porder.thy
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Lemmas for theory porder.thy 
     7 *)
     8 
     9 open Porder0;
    10 open Porder;
    11 
    12 val box_less = prove_goal Porder.thy 
    13 "[| a << b; c << a; b << d|] ==> c << d"
    14  (fn prems =>
    15 	[
    16 	(cut_facts_tac prems 1),
    17 	(etac trans_less 1),
    18 	(etac trans_less 1),
    19 	(atac 1)
    20 	]);
    21 
    22 (* ------------------------------------------------------------------------ *)
    23 (* lubs are unique                                                          *)
    24 (* ------------------------------------------------------------------------ *)
    25 
    26 val unique_lub  = prove_goalw Porder.thy [is_lub, is_ub] 
    27 	"[| S <<| x ; S <<| y |] ==> x=y"
    28 ( fn prems =>
    29 	[
    30 	(cut_facts_tac prems 1),
    31 	(etac conjE 1),
    32 	(etac conjE 1),
    33 	(rtac antisym_less 1),
    34 	(rtac mp 1),((etac allE 1) THEN (atac 1) THEN (atac 1)),
    35 	(rtac mp 1),((etac allE 1) THEN (atac 1) THEN (atac 1))
    36 	]);
    37 
    38 (* ------------------------------------------------------------------------ *)
    39 (* chains are monotone functions                                            *)
    40 (* ------------------------------------------------------------------------ *)
    41 
    42 val chain_mono = prove_goalw Porder.thy [is_chain]
    43 	" is_chain(F) ==> x<y --> F(x)<<F(y)"
    44 ( fn prems =>
    45 	[
    46 	(cut_facts_tac prems 1),
    47 	(nat_ind_tac "y" 1),
    48 	(rtac impI 1),
    49 	(etac less_zeroE 1),
    50 	(rtac (less_Suc_eq RS ssubst) 1),
    51 	(strip_tac 1),
    52 	(etac disjE 1),
    53 	(rtac trans_less 1),
    54 	(etac allE 2),
    55 	(atac 2),
    56 	(fast_tac HOL_cs 1),
    57 	(hyp_subst_tac 1),
    58 	(etac allE 1),
    59 	(atac 1)
    60 	]);
    61 
    62 val chain_mono3 = prove_goal  Porder.thy 
    63 	"[| is_chain(F); x <= y |] ==> F(x) << F(y)"
    64  (fn prems =>
    65 	[
    66 	(cut_facts_tac prems 1),
    67 	(rtac (le_imp_less_or_eq RS disjE) 1),
    68 	(atac 1),
    69 	(etac (chain_mono RS mp) 1),
    70 	(atac 1),
    71 	(hyp_subst_tac 1),
    72 	(rtac refl_less 1)
    73 	]);
    74 
    75 (* ------------------------------------------------------------------------ *)
    76 (* Lemma for reasoning by cases on the natural numbers                      *)
    77 (* ------------------------------------------------------------------------ *)
    78 
    79 val nat_less_cases = prove_goal Porder.thy 
    80 	"[| m::nat < n ==> P(n,m); m=n ==> P(n,m);n < m ==> P(n,m)|]==>P(n,m)"
    81 ( fn prems =>
    82 	[
    83 	(res_inst_tac [("m1","n"),("n1","m")] (less_linear RS disjE) 1),
    84 	(etac disjE 2),
    85 	(etac (hd (tl (tl prems))) 1),
    86 	(etac (sym RS hd (tl prems)) 1),
    87 	(etac (hd prems) 1)
    88 	]);
    89 
    90 (* ------------------------------------------------------------------------ *)
    91 (* The range of a chain is a totaly ordered     <<                           *)
    92 (* ------------------------------------------------------------------------ *)
    93 
    94 val chain_is_tord = prove_goalw Porder.thy [is_tord]
    95 	"is_chain(F) ==> is_tord(range(F))"
    96 ( fn prems =>
    97 	[
    98 	(cut_facts_tac prems 1),
    99 	(rewrite_goals_tac [range_def]),
   100 	(rtac allI 1 ),
   101 	(rtac allI 1 ),
   102 	(rtac (mem_Collect_eq RS ssubst) 1),
   103 	(rtac (mem_Collect_eq RS ssubst) 1),
   104 	(strip_tac 1),
   105 	(etac conjE 1),
   106 	(etac exE 1),
   107 	(etac exE 1),
   108 	(hyp_subst_tac 1),
   109 	(hyp_subst_tac 1),
   110 	(res_inst_tac [("m","xa"),("n","xb")] (nat_less_cases) 1),
   111 	(rtac disjI1 1),
   112 	(rtac (chain_mono RS mp) 1),
   113 	(atac 1),
   114 	(atac 1),
   115 	(rtac disjI1 1),
   116 	(hyp_subst_tac 1),
   117 	(rtac refl_less 1),
   118 	(rtac disjI2 1),
   119 	(rtac (chain_mono RS mp) 1),
   120 	(atac 1),
   121 	(atac 1)
   122 	]);
   123 
   124 
   125 (* ------------------------------------------------------------------------ *)
   126 (* technical lemmas about lub and is_lub, use above results about @         *)
   127 (* ------------------------------------------------------------------------ *)
   128 
   129 val lubI = prove_goal Porder.thy "(? x. M <<| x) ==> M <<| lub(M)"
   130 (fn prems =>
   131 	[
   132 	(cut_facts_tac prems 1),
   133 	(rtac (lub RS ssubst) 1),
   134 	(etac selectI2 1)
   135 	]);
   136 
   137 val lubE = prove_goal Porder.thy " M <<| lub(M) ==>  ? x. M <<| x"
   138 (fn prems =>
   139 	[
   140 	(cut_facts_tac prems 1),
   141 	(etac exI 1)
   142 	]);
   143 
   144 val lub_eq = prove_goal Porder.thy 
   145 	"(? x. M <<| x)  = M <<| lub(M)"
   146 (fn prems => 
   147 	[
   148 	(rtac (lub RS ssubst) 1),
   149 	(rtac (select_eq_Ex RS subst) 1),
   150 	(rtac refl 1)
   151 	]);
   152 
   153 
   154 val thelubI = prove_goal  Porder.thy " M <<| l ==> lub(M) = l"
   155 (fn prems =>
   156 	[
   157 	(cut_facts_tac prems 1), 
   158 	(rtac unique_lub 1),
   159 	(rtac (lub RS ssubst) 1),
   160 	(etac selectI 1),
   161 	(atac 1)
   162 	]);
   163 
   164 
   165 (* ------------------------------------------------------------------------ *)
   166 (* access to some definition as inference rule                              *)
   167 (* ------------------------------------------------------------------------ *)
   168 
   169 val is_lubE = prove_goalw  Porder.thy [is_lub]
   170 	"S <<| x  ==> S <| x & (! u. S <| u  --> x << u)"
   171 (fn prems =>
   172 	[
   173 	(cut_facts_tac prems 1),
   174 	(atac 1)
   175 	]);
   176 
   177 val is_lubI = prove_goalw  Porder.thy [is_lub]
   178 	"S <| x & (! u. S <| u  --> x << u) ==> S <<| x"
   179 (fn prems =>
   180 	[
   181 	(cut_facts_tac prems 1),
   182 	(atac 1)
   183 	]);
   184 
   185 val is_chainE = prove_goalw Porder.thy [is_chain] 
   186  "is_chain(F) ==> ! i. F(i) << F(Suc(i))"
   187 (fn prems =>
   188 	[
   189 	(cut_facts_tac prems 1),
   190 	(atac 1)]);
   191 
   192 val is_chainI = prove_goalw Porder.thy [is_chain] 
   193  "! i. F(i) << F(Suc(i)) ==> is_chain(F) "
   194 (fn prems =>
   195 	[
   196 	(cut_facts_tac prems 1),
   197 	(atac 1)]);
   198 
   199 (* ------------------------------------------------------------------------ *)
   200 (* technical lemmas about (least) upper bounds of chains                    *)
   201 (* ------------------------------------------------------------------------ *)
   202 
   203 val ub_rangeE = prove_goalw  Porder.thy [is_ub]
   204 	"range(S) <| x  ==> ! i. S(i) << x"
   205 (fn prems =>
   206 	[
   207 	(cut_facts_tac prems 1),
   208 	(strip_tac 1),
   209 	(rtac mp 1),
   210 	(etac spec 1),
   211 	(rtac rangeI 1)
   212 	]);
   213 
   214 val ub_rangeI = prove_goalw Porder.thy [is_ub]
   215 	"! i. S(i) << x  ==> range(S) <| x"
   216 (fn prems =>
   217 	[
   218 	(cut_facts_tac prems 1),
   219 	(strip_tac 1),
   220 	(etac rangeE 1),
   221 	(hyp_subst_tac 1),
   222 	(etac spec 1)
   223 	]);
   224 
   225 val is_ub_lub = (is_lubE RS conjunct1 RS ub_rangeE RS spec);
   226 (* range(?S1) <<| ?x1 ==> ?S1(?x) << ?x1                                    *)
   227 
   228 val is_lub_lub = (is_lubE RS conjunct2 RS spec RS mp);
   229 (* [| ?S3 <<| ?x3; ?S3 <| ?x1 |] ==> ?x3 << ?x1                             *)
   230 
   231 (* ------------------------------------------------------------------------ *)
   232 (* Prototype lemmas for class pcpo                                          *)
   233 (* ------------------------------------------------------------------------ *)
   234 
   235 (* ------------------------------------------------------------------------ *)
   236 (* a technical argument about << on void                                    *)
   237 (* ------------------------------------------------------------------------ *)
   238 
   239 val less_void = prove_goal Porder.thy "(u1::void << u2) = (u1 = u2)"
   240 (fn prems =>
   241 	[
   242 	(rtac (inst_void_po RS ssubst) 1),
   243 	(rewrite_goals_tac [less_void_def]),
   244 	(rtac iffI 1),
   245 	(rtac injD 1),
   246 	(atac 2),
   247 	(rtac inj_inverseI 1),
   248 	(rtac Rep_Void_inverse 1),
   249 	(etac arg_cong 1)
   250 	]);
   251 
   252 (* ------------------------------------------------------------------------ *)
   253 (* void is pointed. The least element is UU_void                            *)
   254 (* ------------------------------------------------------------------------ *)
   255 
   256 val minimal_void = prove_goal Porder.thy  	"UU_void << x"
   257 (fn prems =>
   258 	[
   259 	(rtac (inst_void_po RS ssubst) 1),
   260 	(rewrite_goals_tac [less_void_def]),
   261 	(simp_tac (HOL_ss addsimps [unique_void]) 1)
   262 	]);
   263 
   264 (* ------------------------------------------------------------------------ *)
   265 (* UU_void is the trivial lub of all chains in void                         *)
   266 (* ------------------------------------------------------------------------ *)
   267 
   268 val lub_void = prove_goalw  Porder.thy [is_lub] "M <<| UU_void"
   269 (fn prems =>
   270 	[
   271 	(rtac conjI 1),
   272 	(rewrite_goals_tac [is_ub]),
   273 	(strip_tac 1),
   274 	(rtac (inst_void_po RS ssubst) 1),
   275 	(rewrite_goals_tac [less_void_def]),
   276 	(simp_tac (HOL_ss addsimps [unique_void]) 1),
   277 	(strip_tac 1),
   278 	(rtac minimal_void 1)
   279 	]);
   280 
   281 (* ------------------------------------------------------------------------ *)
   282 (* lub(?M) = UU_void                                                        *)
   283 (* ------------------------------------------------------------------------ *)
   284 
   285 val thelub_void = (lub_void RS thelubI);
   286 
   287 (* ------------------------------------------------------------------------ *)
   288 (* void is a cpo wrt. countable chains                                      *)
   289 (* ------------------------------------------------------------------------ *)
   290 
   291 val cpo_void = prove_goal Porder.thy
   292 	"is_chain(S::nat=>void) ==> ? x. range(S) <<| x "
   293 (fn prems =>
   294 	[
   295 	(cut_facts_tac prems 1),
   296 	(res_inst_tac [("x","UU_void")] exI 1),
   297 	(rtac lub_void 1)
   298 	]);
   299 
   300 (* ------------------------------------------------------------------------ *)
   301 (* end of prototype lemmas for class pcpo                                   *)
   302 (* ------------------------------------------------------------------------ *)
   303 
   304 
   305 (* ------------------------------------------------------------------------ *)
   306 (* the reverse law of anti--symmetrie of <<                                 *)
   307 (* ------------------------------------------------------------------------ *)
   308 
   309 val antisym_less_inverse = prove_goal Porder.thy "x=y ==> x << y & y << x"
   310 (fn prems =>
   311 	[
   312 	(cut_facts_tac prems 1),
   313 	(rtac conjI 1),
   314 	((rtac subst 1) THEN (rtac refl_less 2) THEN (atac 1)),
   315 	((rtac subst 1) THEN (rtac refl_less 2) THEN (etac sym 1))
   316 	]);
   317 
   318 (* ------------------------------------------------------------------------ *)
   319 (* results about finite chains                                              *)
   320 (* ------------------------------------------------------------------------ *)
   321 
   322 val lub_finch1 = prove_goalw Porder.thy [max_in_chain_def]
   323 	"[| is_chain(C) ; max_in_chain(i,C)|] ==> range(C) <<| C(i)"
   324 (fn prems =>
   325 	[
   326 	(cut_facts_tac prems 1),
   327 	(rtac is_lubI 1),
   328 	(rtac conjI 1),
   329 	(rtac ub_rangeI 1),
   330 	(rtac allI 1),
   331 	(res_inst_tac [("m","i")] nat_less_cases 1),
   332 	(rtac (antisym_less_inverse RS conjunct2) 1),
   333 	(etac (disjI1 RS less_or_eq_imp_le RS rev_mp) 1),
   334 	(etac spec 1),
   335 	(rtac (antisym_less_inverse RS conjunct2) 1),
   336 	(etac (disjI2 RS less_or_eq_imp_le RS rev_mp) 1),
   337 	(etac spec 1),
   338 	(etac (chain_mono RS mp) 1),
   339 	(atac 1),
   340 	(strip_tac 1),
   341 	(etac (ub_rangeE RS spec) 1)
   342 	]);	
   343 
   344 val lub_finch2 = prove_goalw Porder.thy [finite_chain_def]
   345 	"finite_chain(C) ==> range(C) <<| C(@ i. max_in_chain(i,C))"
   346  (fn prems=>
   347 	[
   348 	(cut_facts_tac prems 1),
   349 	(rtac lub_finch1 1),
   350 	(etac conjunct1 1),
   351 	(rtac selectI2 1),
   352 	(etac conjunct2 1)
   353 	]);
   354 
   355 
   356 val bin_chain = prove_goal Porder.thy "x<<y ==> is_chain(%i. if(i=0,x,y))"
   357  (fn prems =>
   358 	[
   359 	(cut_facts_tac prems 1),
   360 	(rtac is_chainI 1),
   361 	(rtac allI 1),
   362 	(nat_ind_tac "i" 1),
   363 	(asm_simp_tac nat_ss 1),
   364 	(asm_simp_tac nat_ss 1),
   365 	(rtac refl_less 1)
   366 	]);
   367 
   368 val bin_chainmax = prove_goalw Porder.thy [max_in_chain_def,le_def]
   369 	"x<<y ==> max_in_chain(Suc(0),%i. if(i=0,x,y))"
   370 (fn prems =>
   371 	[
   372 	(cut_facts_tac prems 1),
   373 	(rtac allI 1),
   374 	(nat_ind_tac "j" 1),
   375 	(asm_simp_tac nat_ss 1),
   376 	(asm_simp_tac nat_ss 1)
   377 	]);
   378 
   379 val lub_bin_chain = prove_goal Porder.thy 
   380 	"x << y ==> range(%i. if(i = 0,x,y)) <<| y"
   381 (fn prems=>
   382 	[ (cut_facts_tac prems 1),
   383 	(res_inst_tac [("s","if(Suc(0) = 0,x,y)")] subst 1),
   384 	(rtac lub_finch1 2),
   385 	(etac bin_chain 2),
   386 	(etac bin_chainmax 2),
   387 	(simp_tac nat_ss  1)
   388 	]);
   389 
   390 (* ------------------------------------------------------------------------ *)
   391 (* the maximal element in a chain is its lub                                *)
   392 (* ------------------------------------------------------------------------ *)
   393 
   394 val lub_chain_maxelem = prove_goal Porder.thy
   395 "[|is_chain(Y);? i.Y(i)=c;!i.Y(i)<<c|] ==> lub(range(Y)) = c"
   396 (fn prems =>
   397 	[
   398 	(cut_facts_tac prems 1),
   399 	(rtac thelubI 1),
   400 	(rtac is_lubI 1),
   401 	(rtac conjI 1),
   402 	(etac ub_rangeI 1),
   403 	(strip_tac 1),
   404 	(res_inst_tac [("P","%i.Y(i)=c")] exE 1),
   405 	(atac 1),
   406 	(hyp_subst_tac 1),
   407 	(etac (ub_rangeE RS spec) 1)
   408 	]);
   409 
   410 (* ------------------------------------------------------------------------ *)
   411 (* the lub of a constant chain is the constant                              *)
   412 (* ------------------------------------------------------------------------ *)
   413 
   414 val lub_const = prove_goal Porder.thy "range(%x.c) <<| c"
   415  (fn prems =>
   416 	[
   417 	(rtac is_lubI 1),
   418 	(rtac conjI 1),
   419 	(rtac ub_rangeI 1),
   420 	(strip_tac 1),
   421 	(rtac refl_less 1),
   422 	(strip_tac 1),
   423 	(etac (ub_rangeE RS spec) 1)
   424 	]);
   425 
   426 
   427