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