src/HOLCF/Porder.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 5192 704dd3a6d47d
child 8935 548901d05a0e
permissions -rw-r--r--
tidying
slotosch@2640
     1
(*  Title:      HOLCF/Porder.thy
nipkow@243
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Franz Regensburger
nipkow@243
     4
    Copyright   1993 Technische Universitaet Muenchen
nipkow@243
     5
slotosch@2640
     6
Lemmas for theory Porder.thy 
nipkow@243
     7
*)
nipkow@243
     8
nipkow@243
     9
open Porder;
nipkow@243
    10
nipkow@625
    11
(* ------------------------------------------------------------------------ *)
nipkow@243
    12
(* lubs are unique                                                          *)
nipkow@243
    13
(* ------------------------------------------------------------------------ *)
nipkow@243
    14
wenzelm@4031
    15
qed_goalw "unique_lub" thy [is_lub, is_ub] 
clasohm@1461
    16
        "[| S <<| x ; S <<| y |] ==> x=y"
nipkow@243
    17
( fn prems =>
clasohm@1461
    18
        [
clasohm@1461
    19
        (cut_facts_tac prems 1),
clasohm@1461
    20
        (etac conjE 1),
clasohm@1461
    21
        (etac conjE 1),
clasohm@1461
    22
        (rtac antisym_less 1),
clasohm@1461
    23
        (rtac mp 1),((etac allE 1) THEN (atac 1) THEN (atac 1)),
clasohm@1461
    24
        (rtac mp 1),((etac allE 1) THEN (atac 1) THEN (atac 1))
clasohm@1461
    25
        ]);
nipkow@243
    26
nipkow@243
    27
(* ------------------------------------------------------------------------ *)
nipkow@243
    28
(* chains are monotone functions                                            *)
nipkow@243
    29
(* ------------------------------------------------------------------------ *)
nipkow@243
    30
oheimb@4721
    31
qed_goalw "chain_mono" thy [chain] "chain F ==> x<y --> F x<<F y"
nipkow@243
    32
( fn prems =>
clasohm@1461
    33
        [
clasohm@1461
    34
        (cut_facts_tac prems 1),
berghofe@5192
    35
        (induct_tac "y" 1),
clasohm@1461
    36
        (rtac impI 1),
clasohm@1461
    37
        (etac less_zeroE 1),
paulson@2033
    38
        (stac less_Suc_eq 1),
clasohm@1461
    39
        (strip_tac 1),
clasohm@1461
    40
        (etac disjE 1),
clasohm@1461
    41
        (rtac trans_less 1),
clasohm@1461
    42
        (etac allE 2),
clasohm@1461
    43
        (atac 2),
clasohm@1461
    44
        (fast_tac HOL_cs 1),
clasohm@1461
    45
        (hyp_subst_tac 1),
clasohm@1461
    46
        (etac allE 1),
clasohm@1461
    47
        (atac 1)
clasohm@1461
    48
        ]);
nipkow@243
    49
oheimb@4721
    50
qed_goal "chain_mono3" thy "[| chain F; x <= y |] ==> F x << F y"
nipkow@243
    51
 (fn prems =>
clasohm@1461
    52
        [
clasohm@1461
    53
        (cut_facts_tac prems 1),
clasohm@1461
    54
        (rtac (le_imp_less_or_eq RS disjE) 1),
clasohm@1461
    55
        (atac 1),
clasohm@1461
    56
        (etac (chain_mono RS mp) 1),
clasohm@1461
    57
        (atac 1),
clasohm@1461
    58
        (hyp_subst_tac 1),
clasohm@1461
    59
        (rtac refl_less 1)
clasohm@1461
    60
        ]);
nipkow@243
    61
nipkow@243
    62
nipkow@243
    63
(* ------------------------------------------------------------------------ *)
nipkow@243
    64
(* The range of a chain is a totaly ordered     <<                           *)
nipkow@243
    65
(* ------------------------------------------------------------------------ *)
nipkow@243
    66
oheimb@4721
    67
qed_goalw "chain_tord" thy [tord] 
oheimb@4721
    68
"!!F. chain(F) ==> tord(range(F))"
paulson@1886
    69
 (fn _ =>
clasohm@1461
    70
        [
paulson@3724
    71
        Safe_tac,
clasohm@1461
    72
        (rtac nat_less_cases 1),
wenzelm@4098
    73
        (ALLGOALS (fast_tac (claset() addIs [refl_less, chain_mono RS mp])))]);
nipkow@243
    74
nipkow@243
    75
(* ------------------------------------------------------------------------ *)
nipkow@625
    76
(* technical lemmas about lub and is_lub                                    *)
nipkow@243
    77
(* ------------------------------------------------------------------------ *)
slotosch@2640
    78
bind_thm("lub",lub_def RS meta_eq_to_obj_eq);
nipkow@243
    79
slotosch@2640
    80
qed_goal "lubI" thy "? x. M <<| x ==> M <<| lub(M)"
nipkow@243
    81
(fn prems =>
clasohm@1461
    82
        [
clasohm@1461
    83
        (cut_facts_tac prems 1),
paulson@2033
    84
        (stac lub 1),
oheimb@1675
    85
        (etac (select_eq_Ex RS iffD2) 1)
clasohm@1461
    86
        ]);
nipkow@243
    87
slotosch@2640
    88
qed_goal "lubE" thy "M <<| lub(M) ==> ? x. M <<| x"
nipkow@243
    89
(fn prems =>
clasohm@1461
    90
        [
clasohm@1461
    91
        (cut_facts_tac prems 1),
clasohm@1461
    92
        (etac exI 1)
clasohm@1461
    93
        ]);
nipkow@243
    94
slotosch@2640
    95
qed_goal "lub_eq" thy "(? x. M <<| x)  = M <<| lub(M)"
nipkow@243
    96
(fn prems => 
clasohm@1461
    97
        [
paulson@2033
    98
        (stac lub 1),
clasohm@1461
    99
        (rtac (select_eq_Ex RS subst) 1),
clasohm@1461
   100
        (rtac refl 1)
clasohm@1461
   101
        ]);
nipkow@243
   102
nipkow@243
   103
slotosch@2640
   104
qed_goal "thelubI" thy "M <<| l ==> lub(M) = l"
nipkow@243
   105
(fn prems =>
clasohm@1461
   106
        [
clasohm@1461
   107
        (cut_facts_tac prems 1), 
clasohm@1461
   108
        (rtac unique_lub 1),
paulson@2033
   109
        (stac lub 1),
clasohm@1461
   110
        (etac selectI 1),
clasohm@1461
   111
        (atac 1)
clasohm@1461
   112
        ]);
nipkow@243
   113
nipkow@243
   114
wenzelm@5068
   115
Goal "lub{x} = x";
paulson@3018
   116
by (rtac thelubI 1);
wenzelm@4098
   117
by (simp_tac (simpset() addsimps [is_lub,is_ub]) 1);
nipkow@2841
   118
qed "lub_singleton";
nipkow@2841
   119
Addsimps [lub_singleton];
nipkow@2841
   120
nipkow@243
   121
(* ------------------------------------------------------------------------ *)
nipkow@243
   122
(* access to some definition as inference rule                              *)
nipkow@243
   123
(* ------------------------------------------------------------------------ *)
nipkow@243
   124
slotosch@2640
   125
qed_goalw "is_lubE" thy [is_lub]
clasohm@1461
   126
        "S <<| x  ==> S <| x & (! u. S <| u  --> x << u)"
nipkow@243
   127
(fn prems =>
clasohm@1461
   128
        [
clasohm@1461
   129
        (cut_facts_tac prems 1),
clasohm@1461
   130
        (atac 1)
clasohm@1461
   131
        ]);
nipkow@243
   132
slotosch@2640
   133
qed_goalw "is_lubI" thy [is_lub]
clasohm@1461
   134
        "S <| x & (! u. S <| u  --> x << u) ==> S <<| x"
nipkow@243
   135
(fn prems =>
clasohm@1461
   136
        [
clasohm@1461
   137
        (cut_facts_tac prems 1),
clasohm@1461
   138
        (atac 1)
clasohm@1461
   139
        ]);
nipkow@243
   140
oheimb@4721
   141
qed_goalw "chainE" thy [chain] "chain F ==> !i. F(i) << F(Suc(i))"
nipkow@243
   142
(fn prems =>
clasohm@1461
   143
        [
clasohm@1461
   144
        (cut_facts_tac prems 1),
clasohm@1461
   145
        (atac 1)]);
nipkow@243
   146
oheimb@4721
   147
qed_goalw "chainI" thy [chain] "!i. F i << F(Suc i) ==> chain F"
nipkow@243
   148
(fn prems =>
clasohm@1461
   149
        [
clasohm@1461
   150
        (cut_facts_tac prems 1),
clasohm@1461
   151
        (atac 1)]);
nipkow@243
   152
nipkow@243
   153
(* ------------------------------------------------------------------------ *)
nipkow@243
   154
(* technical lemmas about (least) upper bounds of chains                    *)
nipkow@243
   155
(* ------------------------------------------------------------------------ *)
nipkow@243
   156
slotosch@2640
   157
qed_goalw "ub_rangeE" thy [is_ub] "range S <| x  ==> !i. S(i) << x"
nipkow@243
   158
(fn prems =>
clasohm@1461
   159
        [
clasohm@1461
   160
        (cut_facts_tac prems 1),
clasohm@1461
   161
        (strip_tac 1),
clasohm@1461
   162
        (rtac mp 1),
clasohm@1461
   163
        (etac spec 1),
clasohm@1461
   164
        (rtac rangeI 1)
clasohm@1461
   165
        ]);
nipkow@243
   166
slotosch@2640
   167
qed_goalw "ub_rangeI" thy [is_ub] "!i. S i << x  ==> range S <| x"
nipkow@243
   168
(fn prems =>
clasohm@1461
   169
        [
clasohm@1461
   170
        (cut_facts_tac prems 1),
clasohm@1461
   171
        (strip_tac 1),
clasohm@1461
   172
        (etac rangeE 1),
clasohm@1461
   173
        (hyp_subst_tac 1),
clasohm@1461
   174
        (etac spec 1)
clasohm@1461
   175
        ]);
nipkow@243
   176
oheimb@1779
   177
bind_thm ("is_ub_lub", is_lubE RS conjunct1 RS ub_rangeE RS spec);
nipkow@243
   178
(* range(?S1) <<| ?x1 ==> ?S1(?x) << ?x1                                    *)
nipkow@243
   179
oheimb@1779
   180
bind_thm ("is_lub_lub", is_lubE RS conjunct2 RS spec RS mp);
nipkow@243
   181
(* [| ?S3 <<| ?x3; ?S3 <| ?x1 |] ==> ?x3 << ?x1                             *)
nipkow@243
   182
nipkow@243
   183
(* ------------------------------------------------------------------------ *)
nipkow@243
   184
(* results about finite chains                                              *)
nipkow@243
   185
(* ------------------------------------------------------------------------ *)
nipkow@243
   186
slotosch@2640
   187
qed_goalw "lub_finch1" thy [max_in_chain_def]
oheimb@4721
   188
        "[| chain C; max_in_chain i C|] ==> range C <<| C i"
nipkow@243
   189
(fn prems =>
clasohm@1461
   190
        [
clasohm@1461
   191
        (cut_facts_tac prems 1),
clasohm@1461
   192
        (rtac is_lubI 1),
clasohm@1461
   193
        (rtac conjI 1),
clasohm@1461
   194
        (rtac ub_rangeI 1),
clasohm@1461
   195
        (rtac allI 1),
clasohm@1461
   196
        (res_inst_tac [("m","i")] nat_less_cases 1),
clasohm@1461
   197
        (rtac (antisym_less_inverse RS conjunct2) 1),
clasohm@1461
   198
        (etac (disjI1 RS less_or_eq_imp_le RS rev_mp) 1),
clasohm@1461
   199
        (etac spec 1),
clasohm@1461
   200
        (rtac (antisym_less_inverse RS conjunct2) 1),
clasohm@1461
   201
        (etac (disjI2 RS less_or_eq_imp_le RS rev_mp) 1),
clasohm@1461
   202
        (etac spec 1),
clasohm@1461
   203
        (etac (chain_mono RS mp) 1),
clasohm@1461
   204
        (atac 1),
clasohm@1461
   205
        (strip_tac 1),
clasohm@1461
   206
        (etac (ub_rangeE RS spec) 1)
clasohm@1461
   207
        ]);     
nipkow@243
   208
slotosch@2640
   209
qed_goalw "lub_finch2" thy [finite_chain_def]
clasohm@1461
   210
        "finite_chain(C) ==> range(C) <<| C(@ i. max_in_chain i C)"
nipkow@243
   211
 (fn prems=>
clasohm@1461
   212
        [
clasohm@1461
   213
        (cut_facts_tac prems 1),
clasohm@1461
   214
        (rtac lub_finch1 1),
clasohm@1461
   215
        (etac conjunct1 1),
oheimb@1675
   216
        (rtac (select_eq_Ex RS iffD2) 1),
clasohm@1461
   217
        (etac conjunct2 1)
clasohm@1461
   218
        ]);
nipkow@243
   219
nipkow@243
   220
oheimb@4721
   221
qed_goal "bin_chain" thy "x<<y ==> chain (%i. if i=0 then x else y)"
nipkow@243
   222
 (fn prems =>
clasohm@1461
   223
        [
clasohm@1461
   224
        (cut_facts_tac prems 1),
oheimb@4721
   225
        (rtac chainI 1),
clasohm@1461
   226
        (rtac allI 1),
berghofe@5192
   227
        (induct_tac "i" 1),
clasohm@1461
   228
        (Asm_simp_tac 1),
nipkow@2841
   229
        (Asm_simp_tac 1)
clasohm@1461
   230
        ]);
nipkow@243
   231
slotosch@2640
   232
qed_goalw "bin_chainmax" thy [max_in_chain_def,le_def]
clasohm@1461
   233
        "x<<y ==> max_in_chain (Suc 0) (%i. if (i=0) then x else y)"
nipkow@243
   234
(fn prems =>
clasohm@1461
   235
        [
clasohm@1461
   236
        (cut_facts_tac prems 1),
clasohm@1461
   237
        (rtac allI 1),
berghofe@5192
   238
        (induct_tac "j" 1),
clasohm@1461
   239
        (Asm_simp_tac 1),
clasohm@1461
   240
        (Asm_simp_tac 1)
clasohm@1461
   241
        ]);
nipkow@243
   242
slotosch@2640
   243
qed_goal "lub_bin_chain" thy 
clasohm@1461
   244
        "x << y ==> range(%i. if (i=0) then x else y) <<| y"
nipkow@243
   245
(fn prems=>
clasohm@1461
   246
        [ (cut_facts_tac prems 1),
clasohm@1461
   247
        (res_inst_tac [("s","if (Suc 0) = 0 then x else y")] subst 1),
clasohm@1461
   248
        (rtac lub_finch1 2),
clasohm@1461
   249
        (etac bin_chain 2),
clasohm@1461
   250
        (etac bin_chainmax 2),
clasohm@1461
   251
        (Simp_tac  1)
clasohm@1461
   252
        ]);
nipkow@243
   253
nipkow@243
   254
(* ------------------------------------------------------------------------ *)
nipkow@243
   255
(* the maximal element in a chain is its lub                                *)
nipkow@243
   256
(* ------------------------------------------------------------------------ *)
nipkow@243
   257
slotosch@2640
   258
qed_goal "lub_chain_maxelem" thy
wenzelm@3842
   259
"[|? i. Y i=c;!i. Y i<<c|] ==> lub(range Y) = c"
regensbu@1043
   260
 (fn prems =>
clasohm@1461
   261
        [
clasohm@1461
   262
        (cut_facts_tac prems 1),
clasohm@1461
   263
        (rtac thelubI 1),
clasohm@1461
   264
        (rtac is_lubI 1),
clasohm@1461
   265
        (rtac conjI 1),
clasohm@1461
   266
        (etac ub_rangeI 1),
clasohm@1461
   267
        (strip_tac 1),
clasohm@1461
   268
        (etac exE 1),
clasohm@1461
   269
        (hyp_subst_tac 1),
clasohm@1461
   270
        (etac (ub_rangeE RS spec) 1)
clasohm@1461
   271
        ]);
nipkow@243
   272
nipkow@243
   273
(* ------------------------------------------------------------------------ *)
nipkow@243
   274
(* the lub of a constant chain is the constant                              *)
nipkow@243
   275
(* ------------------------------------------------------------------------ *)
nipkow@243
   276
wenzelm@3842
   277
qed_goal "lub_const" thy "range(%x. c) <<| c"
nipkow@243
   278
 (fn prems =>
clasohm@1461
   279
        [
clasohm@1461
   280
        (rtac is_lubI 1),
clasohm@1461
   281
        (rtac conjI 1),
clasohm@1461
   282
        (rtac ub_rangeI 1),
clasohm@1461
   283
        (strip_tac 1),
clasohm@1461
   284
        (rtac refl_less 1),
clasohm@1461
   285
        (strip_tac 1),
clasohm@1461
   286
        (etac (ub_rangeE RS spec) 1)
clasohm@1461
   287
        ]);
nipkow@243
   288
nipkow@243
   289
nipkow@243
   290