src/HOLCF/Pcpo.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 4721 c8a8482a8124
child 9169 85a47aa21f74
permissions -rw-r--r--
made tutorial first;
clasohm@1461
     1
(*  Title:      HOLCF/pcpo.ML
nipkow@243
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Franz Regensburger
nipkow@243
     4
    Copyright   1993 Technische Universitaet Muenchen
nipkow@243
     5
nipkow@243
     6
Lemmas for pcpo.thy
nipkow@243
     7
*)
nipkow@243
     8
 
nipkow@243
     9
open Pcpo;
nipkow@243
    10
slotosch@2640
    11
slotosch@2640
    12
(* ------------------------------------------------------------------------ *)
slotosch@2640
    13
(* derive the old rule minimal                                              *)
slotosch@2640
    14
(* ------------------------------------------------------------------------ *)
slotosch@2640
    15
wenzelm@3842
    16
qed_goalw "UU_least" thy [ UU_def ] "!z. UU << z"
slotosch@2640
    17
(fn prems => [ 
slotosch@2640
    18
        (rtac (select_eq_Ex RS iffD2) 1),
slotosch@2640
    19
        (rtac least 1)]);
slotosch@2640
    20
slotosch@2640
    21
bind_thm("minimal",UU_least RS spec);
slotosch@2640
    22
nipkow@243
    23
(* ------------------------------------------------------------------------ *)
slotosch@2839
    24
(* in cpo's everthing equal to THE lub has lub properties for every chain  *)
nipkow@243
    25
(* ------------------------------------------------------------------------ *)
nipkow@243
    26
slotosch@2640
    27
qed_goal "thelubE"  thy 
oheimb@4721
    28
        "[| chain(S);lub(range(S)) = (l::'a::cpo)|] ==> range(S) <<| l "
nipkow@243
    29
(fn prems =>
clasohm@1461
    30
        [
clasohm@1461
    31
        (cut_facts_tac prems 1), 
clasohm@1461
    32
        (hyp_subst_tac 1),
clasohm@1461
    33
        (rtac lubI 1),
clasohm@1461
    34
        (etac cpo 1)
clasohm@1461
    35
        ]);
nipkow@243
    36
nipkow@243
    37
(* ------------------------------------------------------------------------ *)
nipkow@243
    38
(* Properties of the lub                                                    *)
nipkow@243
    39
(* ------------------------------------------------------------------------ *)
nipkow@243
    40
nipkow@243
    41
oheimb@1779
    42
bind_thm ("is_ub_thelub", cpo RS lubI RS is_ub_lub);
oheimb@4721
    43
(* chain(?S1) ==> ?S1(?x) << lub(range(?S1))                             *)
nipkow@243
    44
oheimb@1779
    45
bind_thm ("is_lub_thelub", cpo RS lubI RS is_lub_lub);
oheimb@4721
    46
(* [| chain(?S5); range(?S5) <| ?x1 |] ==> lub(range(?S5)) << ?x1        *)
nipkow@243
    47
oheimb@4721
    48
qed_goal "maxinch_is_thelub" thy "chain Y ==> \
slotosch@2839
    49
\       max_in_chain i Y = (lub(range(Y)) = ((Y i)::'a::cpo))" 
sandnerr@2354
    50
(fn prems => 
paulson@2416
    51
        [
paulson@2416
    52
        cut_facts_tac prems 1,
paulson@2416
    53
        rtac iffI 1,
paulson@2416
    54
        fast_tac (HOL_cs addSIs [thelubI,lub_finch1]) 1,
paulson@2416
    55
        rewtac max_in_chain_def,
paulson@2416
    56
        safe_tac (HOL_cs addSIs [antisym_less]),
paulson@2416
    57
        fast_tac (HOL_cs addSEs [chain_mono3]) 1,
paulson@2416
    58
        dtac sym 1,
wenzelm@4098
    59
        fast_tac ((HOL_cs addSEs [is_ub_thelub]) addss simpset()) 1
paulson@2416
    60
        ]);
sandnerr@2354
    61
nipkow@243
    62
nipkow@243
    63
(* ------------------------------------------------------------------------ *)
nipkow@243
    64
(* the << relation between two chains is preserved by their lubs            *)
nipkow@243
    65
(* ------------------------------------------------------------------------ *)
nipkow@243
    66
slotosch@2640
    67
qed_goal "lub_mono" thy 
oheimb@4721
    68
        "[|chain(C1::(nat=>'a::cpo));chain(C2); ! k. C1(k) << C2(k)|]\
nipkow@243
    69
\           ==> lub(range(C1)) << lub(range(C2))"
nipkow@243
    70
(fn prems =>
clasohm@1461
    71
        [
clasohm@1461
    72
        (cut_facts_tac prems 1),
clasohm@1461
    73
        (etac is_lub_thelub 1),
clasohm@1461
    74
        (rtac ub_rangeI 1),
clasohm@1461
    75
        (rtac allI 1),
clasohm@1461
    76
        (rtac trans_less 1),
clasohm@1461
    77
        (etac spec 1),
clasohm@1461
    78
        (etac is_ub_thelub 1)
clasohm@1461
    79
        ]);
nipkow@243
    80
nipkow@243
    81
(* ------------------------------------------------------------------------ *)
nipkow@243
    82
(* the = relation between two chains is preserved by their lubs            *)
nipkow@243
    83
(* ------------------------------------------------------------------------ *)
nipkow@243
    84
slotosch@2640
    85
qed_goal "lub_equal" thy
oheimb@4721
    86
"[| chain(C1::(nat=>'a::cpo));chain(C2);!k. C1(k)=C2(k)|]\
clasohm@1461
    87
\       ==> lub(range(C1))=lub(range(C2))"
nipkow@243
    88
(fn prems =>
clasohm@1461
    89
        [
clasohm@1461
    90
        (cut_facts_tac prems 1),
clasohm@1461
    91
        (rtac antisym_less 1),
clasohm@1461
    92
        (rtac lub_mono 1),
clasohm@1461
    93
        (atac 1),
clasohm@1461
    94
        (atac 1),
clasohm@1461
    95
        (strip_tac 1),
clasohm@1461
    96
        (rtac (antisym_less_inverse RS conjunct1) 1),
clasohm@1461
    97
        (etac spec 1),
clasohm@1461
    98
        (rtac lub_mono 1),
clasohm@1461
    99
        (atac 1),
clasohm@1461
   100
        (atac 1),
clasohm@1461
   101
        (strip_tac 1),
clasohm@1461
   102
        (rtac (antisym_less_inverse RS conjunct2) 1),
clasohm@1461
   103
        (etac spec 1)
clasohm@1461
   104
        ]);
nipkow@243
   105
nipkow@243
   106
(* ------------------------------------------------------------------------ *)
nipkow@243
   107
(* more results about mono and = of lubs of chains                          *)
nipkow@243
   108
(* ------------------------------------------------------------------------ *)
nipkow@243
   109
slotosch@2640
   110
qed_goal "lub_mono2" thy 
oheimb@4721
   111
"[|? j.!i. j<i --> X(i::nat)=Y(i);chain(X::nat=>'a::cpo);chain(Y)|]\
nipkow@243
   112
\ ==> lub(range(X))<<lub(range(Y))"
nipkow@243
   113
 (fn prems =>
clasohm@1461
   114
        [
clasohm@1461
   115
        (rtac  exE 1),
clasohm@1461
   116
        (resolve_tac prems 1),
clasohm@1461
   117
        (rtac is_lub_thelub 1),
clasohm@1461
   118
        (resolve_tac prems 1),
clasohm@1461
   119
        (rtac ub_rangeI 1),
clasohm@1461
   120
        (strip_tac 1),
oheimb@1675
   121
        (case_tac "x<i" 1),
clasohm@1461
   122
        (res_inst_tac [("s","Y(i)"),("t","X(i)")] subst 1),
clasohm@1461
   123
        (rtac sym 1),
paulson@3726
   124
        (Fast_tac 1),
clasohm@1461
   125
        (rtac is_ub_thelub 1),
clasohm@1461
   126
        (resolve_tac prems 1),
clasohm@1461
   127
        (res_inst_tac [("y","X(Suc(x))")] trans_less 1),
clasohm@1461
   128
        (rtac (chain_mono RS mp) 1),
clasohm@1461
   129
        (resolve_tac prems 1),
clasohm@1461
   130
        (rtac (not_less_eq RS subst) 1),
clasohm@1461
   131
        (atac 1),
clasohm@1461
   132
        (res_inst_tac [("s","Y(Suc(x))"),("t","X(Suc(x))")] subst 1),
clasohm@1461
   133
        (rtac sym 1),
clasohm@1461
   134
        (Asm_simp_tac 1),
clasohm@1461
   135
        (rtac is_ub_thelub 1),
clasohm@1461
   136
        (resolve_tac prems 1)
clasohm@1461
   137
        ]);
nipkow@243
   138
slotosch@2640
   139
qed_goal "lub_equal2" thy 
oheimb@4721
   140
"[|? j.!i. j<i --> X(i)=Y(i);chain(X::nat=>'a::cpo);chain(Y)|]\
nipkow@243
   141
\ ==> lub(range(X))=lub(range(Y))"
nipkow@243
   142
 (fn prems =>
clasohm@1461
   143
        [
clasohm@1461
   144
        (rtac antisym_less 1),
clasohm@1461
   145
        (rtac lub_mono2 1),
clasohm@1461
   146
        (REPEAT (resolve_tac prems 1)),
clasohm@1461
   147
        (cut_facts_tac prems 1),
clasohm@1461
   148
        (rtac lub_mono2 1),
paulson@3726
   149
        Safe_tac,
paulson@3726
   150
        (Step_tac 1),
paulson@3726
   151
        Safe_tac,
clasohm@1461
   152
        (rtac sym 1),
paulson@3726
   153
        (Fast_tac 1)
clasohm@1461
   154
        ]);
nipkow@243
   155
oheimb@4721
   156
qed_goal "lub_mono3" thy "[|chain(Y::nat=>'a::cpo);chain(X);\
nipkow@243
   157
\! i. ? j. Y(i)<< X(j)|]==> lub(range(Y))<<lub(range(X))"
nipkow@243
   158
 (fn prems =>
clasohm@1461
   159
        [
clasohm@1461
   160
        (cut_facts_tac prems 1),
clasohm@1461
   161
        (rtac is_lub_thelub 1),
clasohm@1461
   162
        (atac 1),
clasohm@1461
   163
        (rtac ub_rangeI 1),
clasohm@1461
   164
        (strip_tac 1),
clasohm@1461
   165
        (etac allE 1),
clasohm@1461
   166
        (etac exE 1),
clasohm@1461
   167
        (rtac trans_less 1),
clasohm@1461
   168
        (rtac is_ub_thelub 2),
clasohm@1461
   169
        (atac 2),
clasohm@1461
   170
        (atac 1)
clasohm@1461
   171
        ]);
nipkow@243
   172
nipkow@243
   173
(* ------------------------------------------------------------------------ *)
nipkow@243
   174
(* usefull lemmas about UU                                                  *)
nipkow@243
   175
(* ------------------------------------------------------------------------ *)
nipkow@243
   176
slotosch@2640
   177
val eq_UU_sym = prove_goal thy "(UU = x) = (x = UU)" (fn _ => [
paulson@3726
   178
        Fast_tac 1]);
oheimb@2275
   179
slotosch@2640
   180
qed_goal "eq_UU_iff" thy "(x=UU)=(x<<UU)"
nipkow@243
   181
 (fn prems =>
clasohm@1461
   182
        [
clasohm@1461
   183
        (rtac iffI 1),
clasohm@1461
   184
        (hyp_subst_tac 1),
clasohm@1461
   185
        (rtac refl_less 1),
clasohm@1461
   186
        (rtac antisym_less 1),
clasohm@1461
   187
        (atac 1),
clasohm@1461
   188
        (rtac minimal 1)
clasohm@1461
   189
        ]);
nipkow@243
   190
slotosch@2640
   191
qed_goal "UU_I" thy "x << UU ==> x = UU"
nipkow@243
   192
 (fn prems =>
clasohm@1461
   193
        [
paulson@2033
   194
        (stac eq_UU_iff 1),
clasohm@1461
   195
        (resolve_tac prems 1)
clasohm@1461
   196
        ]);
nipkow@243
   197
slotosch@3323
   198
qed_goal "not_less2not_eq" thy "~(x::'a::po)<<y ==> ~x=y"
nipkow@243
   199
 (fn prems =>
clasohm@1461
   200
        [
clasohm@1461
   201
        (cut_facts_tac prems 1),
oheimb@2445
   202
        (rtac classical2 1),
clasohm@1461
   203
        (atac 1),
clasohm@1461
   204
        (hyp_subst_tac 1),
clasohm@1461
   205
        (rtac refl_less 1)
clasohm@1461
   206
        ]);
nipkow@243
   207
slotosch@2640
   208
qed_goal "chain_UU_I" thy
oheimb@4721
   209
        "[|chain(Y);lub(range(Y))=UU|] ==> ! i. Y(i)=UU"
regensbu@1043
   210
 (fn prems =>
clasohm@1461
   211
        [
clasohm@1461
   212
        (cut_facts_tac prems 1),
clasohm@1461
   213
        (rtac allI 1),
clasohm@1461
   214
        (rtac antisym_less 1),
clasohm@1461
   215
        (rtac minimal 2),
clasohm@1461
   216
        (etac subst 1),
clasohm@1461
   217
        (etac is_ub_thelub 1)
clasohm@1461
   218
        ]);
nipkow@243
   219
nipkow@243
   220
slotosch@2640
   221
qed_goal "chain_UU_I_inverse" thy 
wenzelm@3842
   222
        "!i. Y(i::nat)=UU ==> lub(range(Y::(nat=>'a::pcpo)))=UU"
regensbu@1043
   223
 (fn prems =>
clasohm@1461
   224
        [
clasohm@1461
   225
        (cut_facts_tac prems 1),
clasohm@1461
   226
        (rtac lub_chain_maxelem 1),
clasohm@1461
   227
        (rtac exI 1),
clasohm@1461
   228
        (etac spec 1),
clasohm@1461
   229
        (rtac allI 1),
clasohm@1461
   230
        (rtac (antisym_less_inverse RS conjunct1) 1),
clasohm@1461
   231
        (etac spec 1)
clasohm@1461
   232
        ]);
nipkow@243
   233
slotosch@2640
   234
qed_goal "chain_UU_I_inverse2" thy 
clasohm@1461
   235
        "~lub(range(Y::(nat=>'a::pcpo)))=UU ==> ? i.~ Y(i)=UU"
nipkow@243
   236
 (fn prems =>
clasohm@1461
   237
        [
clasohm@1461
   238
        (cut_facts_tac prems 1),
oheimb@1675
   239
        (rtac (not_all RS iffD1) 1),
clasohm@1461
   240
        (rtac swap 1),
clasohm@1461
   241
        (rtac chain_UU_I_inverse 2),
clasohm@1461
   242
        (etac notnotD 2),
clasohm@1461
   243
        (atac 1)
clasohm@1461
   244
        ]);
nipkow@243
   245
nipkow@243
   246
slotosch@2640
   247
qed_goal "notUU_I" thy "[| x<<y; ~x=UU |] ==> ~y=UU"
nipkow@243
   248
(fn prems =>
clasohm@1461
   249
        [
clasohm@1461
   250
        (cut_facts_tac prems 1),
clasohm@1461
   251
        (etac contrapos 1),
clasohm@1461
   252
        (rtac UU_I 1),
clasohm@1461
   253
        (hyp_subst_tac 1),
clasohm@1461
   254
        (atac 1)
clasohm@1461
   255
        ]);
nipkow@243
   256
nipkow@243
   257
slotosch@2640
   258
qed_goal "chain_mono2" thy 
oheimb@4721
   259
"[|? j.~Y(j)=UU;chain(Y::nat=>'a::pcpo)|]\
wenzelm@3842
   260
\ ==> ? j.!i. j<i-->~Y(i)=UU"
nipkow@243
   261
 (fn prems =>
clasohm@1461
   262
        [
clasohm@1461
   263
        (cut_facts_tac prems 1),
paulson@3726
   264
        Safe_tac,
paulson@3726
   265
        (Step_tac 1),
clasohm@1461
   266
        (strip_tac 1),
clasohm@1461
   267
        (rtac notUU_I 1),
clasohm@1461
   268
        (atac 2),
clasohm@1461
   269
        (etac (chain_mono RS mp) 1),
clasohm@1461
   270
        (atac 1)
clasohm@1461
   271
        ]);
slotosch@3326
   272
slotosch@3326
   273
(**************************************)
slotosch@3326
   274
(* some properties for chfin and flat *)
slotosch@3326
   275
(**************************************)
slotosch@3326
   276
slotosch@3326
   277
(* ------------------------------------------------------------------------ *)
oheimb@4721
   278
(* flat types are chfin                                              *)
slotosch@3326
   279
(* ------------------------------------------------------------------------ *)
slotosch@3326
   280
oheimb@4721
   281
qed_goalw "flat_imp_chfin" thy [max_in_chain_def]
oheimb@4721
   282
        "!Y::nat=>'a::flat. chain Y-->(? n. max_in_chain n Y)"
slotosch@3326
   283
 (fn _ =>
slotosch@3326
   284
        [
slotosch@3326
   285
        (strip_tac 1),
wenzelm@3842
   286
        (case_tac "!i. Y(i)=UU" 1),
slotosch@3326
   287
        (res_inst_tac [("x","0")] exI 1),
slotosch@3326
   288
	(Asm_simp_tac 1),
slotosch@3326
   289
 	(Asm_full_simp_tac 1),
slotosch@3326
   290
 	(etac exE 1),
slotosch@3326
   291
        (res_inst_tac [("x","i")] exI 1),
slotosch@3326
   292
        (strip_tac 1),
slotosch@3326
   293
        (dres_inst_tac [("x","i"),("y","j")] chain_mono 1),
slotosch@3326
   294
        (etac (le_imp_less_or_eq RS disjE) 1),
paulson@3726
   295
	Safe_tac,
slotosch@3326
   296
	(dtac (ax_flat RS spec RS spec RS mp) 1),
paulson@3726
   297
	(Fast_tac 1)
slotosch@3326
   298
        ]);
slotosch@3326
   299
slotosch@3326
   300
(* flat subclass of chfin --> adm_flat not needed *)
slotosch@3326
   301
slotosch@3326
   302
qed_goal "flat_eq" thy "(a::'a::flat) ~= UU ==> a << b = (a = b)" 
slotosch@3326
   303
(fn prems=>
slotosch@3326
   304
	[
slotosch@3326
   305
        cut_facts_tac prems 1,
slotosch@3326
   306
        safe_tac (HOL_cs addSIs [refl_less]),
slotosch@3326
   307
	dtac (ax_flat RS spec RS spec RS mp) 1,
slotosch@3326
   308
	fast_tac (HOL_cs addSIs [refl_less,ax_flat RS spec RS spec RS mp]) 1
slotosch@3326
   309
	]);
slotosch@3326
   310
slotosch@3326
   311
qed_goal "chfin2finch" thy 
oheimb@4721
   312
    "chain (Y::nat=>'a::chfin) ==> finite_chain Y"
slotosch@3326
   313
	(fn prems => 
slotosch@3326
   314
	[
slotosch@3326
   315
	cut_facts_tac prems 1,
slotosch@3326
   316
	fast_tac (HOL_cs addss 
wenzelm@4098
   317
		 (simpset() addsimps [chfin,finite_chain_def])) 1
slotosch@3326
   318
	]);
slotosch@3326
   319
slotosch@3326
   320
(* ------------------------------------------------------------------------ *)
slotosch@3326
   321
(* lemmata for improved admissibility introdution rule                      *)
slotosch@3326
   322
(* ------------------------------------------------------------------------ *)
slotosch@3326
   323
slotosch@3326
   324
qed_goal "infinite_chain_adm_lemma" Porder.thy 
oheimb@4721
   325
"[|chain Y; !i. P (Y i); \
oheimb@4721
   326
\  (!!Y. [| chain Y; !i. P (Y i); ~ finite_chain Y |] ==> P (lub (range Y)))\
slotosch@3326
   327
\ |] ==> P (lub (range Y))"
slotosch@3326
   328
 (fn prems => [
slotosch@3326
   329
        cut_facts_tac prems 1,
slotosch@3326
   330
        case_tac "finite_chain Y" 1,
slotosch@3326
   331
         eresolve_tac prems 2, atac 2, atac 2,
slotosch@3326
   332
        rewtac finite_chain_def,
slotosch@3326
   333
        safe_tac HOL_cs,
slotosch@3326
   334
        etac (lub_finch1 RS thelubI RS ssubst) 1, atac 1, etac spec 1]);
slotosch@3326
   335
slotosch@3326
   336
qed_goal "increasing_chain_adm_lemma" Porder.thy 
oheimb@4721
   337
"[|chain Y; !i. P (Y i); \
oheimb@4721
   338
\  (!!Y. [| chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j|]\
slotosch@3326
   339
\ ==> P (lub (range Y))) |] ==> P (lub (range Y))"
slotosch@3326
   340
 (fn prems => [
slotosch@3326
   341
        cut_facts_tac prems 1,
slotosch@3326
   342
        etac infinite_chain_adm_lemma 1, atac 1, etac thin_rl 1,
slotosch@3326
   343
        rewtac finite_chain_def,
slotosch@3326
   344
        safe_tac HOL_cs,
slotosch@3326
   345
        etac swap 1,
slotosch@3326
   346
        rewtac max_in_chain_def,
slotosch@3326
   347
        resolve_tac prems 1, atac 1, atac 1,
slotosch@3326
   348
        fast_tac (HOL_cs addDs [le_imp_less_or_eq] 
slotosch@3326
   349
                         addEs [chain_mono RS mp]) 1]);