src/HOLCF/Porder.ML
author paulson
Wed Jul 25 13:33:08 2001 +0200 (2001-07-25)
changeset 11452 f3fbbaeb4fb8
parent 11347 4e41f71179ed
child 12030 46d57d0290a2
permissions -rw-r--r--
removed reference to Ex_def
paulson@9245
     1
(*  Title:      HOLCF/Porder
nipkow@243
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Franz Regensburger
nipkow@243
     4
    Copyright   1993 Technische Universitaet Muenchen
nipkow@243
     5
paulson@9245
     6
Conservative extension of theory Porder0 by constant definitions 
nipkow@243
     7
*)
nipkow@243
     8
nipkow@625
     9
(* ------------------------------------------------------------------------ *)
nipkow@243
    10
(* lubs are unique                                                          *)
nipkow@243
    11
(* ------------------------------------------------------------------------ *)
nipkow@243
    12
paulson@9245
    13
oheimb@11347
    14
Goalw [is_lub_def, is_ub_def] 
paulson@9245
    15
        "[| S <<| x ; S <<| y |] ==> x=y";
paulson@9248
    16
by (blast_tac (claset() addIs [antisym_less]) 1);
paulson@9245
    17
qed "unique_lub";
nipkow@243
    18
nipkow@243
    19
(* ------------------------------------------------------------------------ *)
nipkow@243
    20
(* chains are monotone functions                                            *)
nipkow@243
    21
(* ------------------------------------------------------------------------ *)
nipkow@243
    22
oheimb@11347
    23
Goalw [chain_def] "chain F ==> x<y --> F x<<F y";
paulson@9245
    24
by (induct_tac "y" 1);
paulson@9248
    25
by Auto_tac;  
paulson@9248
    26
by (blast_tac (claset() addIs [trans_less]) 2);
paulson@9248
    27
by (blast_tac (claset() addSEs [less_SucE]) 1);
paulson@9248
    28
qed_spec_mp "chain_mono";
nipkow@243
    29
paulson@9169
    30
Goal "[| chain F; x <= y |] ==> F x << F y";
paulson@9248
    31
by (dtac le_imp_less_or_eq 1);
paulson@9248
    32
by (blast_tac (claset() addIs [chain_mono]) 1);
paulson@9169
    33
qed "chain_mono3";
nipkow@243
    34
nipkow@243
    35
nipkow@243
    36
(* ------------------------------------------------------------------------ *)
paulson@9245
    37
(* The range of a chain is a totally ordered     <<                         *)
nipkow@243
    38
(* ------------------------------------------------------------------------ *)
nipkow@243
    39
oheimb@11347
    40
Goalw [tord_def] "chain(F) ==> tord(range(F))";
paulson@9245
    41
by (Safe_tac);
paulson@9245
    42
by (rtac nat_less_cases 1);
paulson@9248
    43
by (ALLGOALS (fast_tac (claset() addIs [chain_mono])));
paulson@9245
    44
qed "chain_tord";
paulson@9245
    45
nipkow@243
    46
nipkow@243
    47
(* ------------------------------------------------------------------------ *)
nipkow@625
    48
(* technical lemmas about lub and is_lub                                    *)
nipkow@243
    49
(* ------------------------------------------------------------------------ *)
slotosch@2640
    50
bind_thm("lub",lub_def RS meta_eq_to_obj_eq);
nipkow@243
    51
paulson@9248
    52
Goal "EX x. M <<| x ==> M <<| lub(M)";
paulson@11452
    53
by (asm_full_simp_tac (simpset() addsimps [lub, some_eq_ex]) 1);
paulson@9248
    54
bind_thm ("lubI", exI RS result());
nipkow@243
    55
paulson@9169
    56
Goal "M <<| l ==> lub(M) = l";
paulson@9169
    57
by (rtac unique_lub 1);
paulson@9169
    58
by (stac lub 1);
paulson@9970
    59
by (etac someI 1);
paulson@9169
    60
by (atac 1);
paulson@9169
    61
qed "thelubI";
nipkow@243
    62
nipkow@243
    63
wenzelm@5068
    64
Goal "lub{x} = x";
oheimb@11347
    65
by (simp_tac (simpset() addsimps [thelubI,is_lub_def,is_ub_def]) 1);
nipkow@2841
    66
qed "lub_singleton";
nipkow@2841
    67
Addsimps [lub_singleton];
nipkow@2841
    68
nipkow@243
    69
(* ------------------------------------------------------------------------ *)
nipkow@243
    70
(* access to some definition as inference rule                              *)
nipkow@243
    71
(* ------------------------------------------------------------------------ *)
nipkow@243
    72
oheimb@11347
    73
Goalw [is_lub_def] "S <<| x ==> S <| x";
paulson@9248
    74
by Auto_tac;
paulson@9248
    75
qed "is_lubD1";
nipkow@243
    76
oheimb@11347
    77
Goalw [is_lub_def] "[| S <<| x; S <| u |] ==> x << u";
paulson@9248
    78
by Auto_tac;
paulson@9248
    79
qed "is_lub_lub";
paulson@9248
    80
oheimb@11347
    81
val prems = Goalw [is_lub_def]
paulson@9248
    82
        "[| S <| x; !!u. S <| u ==> x << u |] ==> S <<| x";
paulson@9248
    83
by (blast_tac (claset() addIs prems) 1);
paulson@9245
    84
qed "is_lubI";
nipkow@243
    85
oheimb@11347
    86
Goalw [chain_def] "chain F ==> F(i) << F(Suc(i))";
paulson@9248
    87
by Auto_tac;
paulson@9245
    88
qed "chainE";
nipkow@243
    89
oheimb@11347
    90
val prems = Goalw [chain_def] "(!!i. F i << F(Suc i)) ==> chain F";
paulson@9248
    91
by (blast_tac (claset() addIs prems) 1);
paulson@9245
    92
qed "chainI";
nipkow@243
    93
oheimb@11347
    94
Goal "chain Y ==> chain (%i. Y (i + j))";
oheimb@11347
    95
br chainI 1;
oheimb@11347
    96
by (Clarsimp_tac 1);
oheimb@11347
    97
be chainE 1;
oheimb@11347
    98
qed "chain_shift";
oheimb@11347
    99
nipkow@243
   100
(* ------------------------------------------------------------------------ *)
nipkow@243
   101
(* technical lemmas about (least) upper bounds of chains                    *)
nipkow@243
   102
(* ------------------------------------------------------------------------ *)
nipkow@243
   103
oheimb@11347
   104
Goalw [is_ub_def] "range S <| x  ==> S(i) << x";
paulson@9248
   105
by (Blast_tac 1);
paulson@9248
   106
qed "ub_rangeD";
nipkow@243
   107
oheimb@11347
   108
val prems = Goalw [is_ub_def] "(!!i. S i << x) ==> range S <| x";
paulson@9248
   109
by (blast_tac (claset() addIs prems) 1);
paulson@9245
   110
qed "ub_rangeI";
nipkow@243
   111
paulson@9248
   112
bind_thm ("is_ub_lub", is_lubD1 RS ub_rangeD);
nipkow@243
   113
(* range(?S1) <<| ?x1 ==> ?S1(?x) << ?x1                                    *)
nipkow@243
   114
nipkow@243
   115
nipkow@243
   116
(* ------------------------------------------------------------------------ *)
nipkow@243
   117
(* results about finite chains                                              *)
nipkow@243
   118
(* ------------------------------------------------------------------------ *)
nipkow@243
   119
paulson@9248
   120
Goalw [max_in_chain_def]
paulson@9245
   121
        "[| chain C; max_in_chain i C|] ==> range C <<| C i";
paulson@9245
   122
by (rtac is_lubI 1);
paulson@9245
   123
by (rtac ub_rangeI 1);
paulson@9245
   124
by (res_inst_tac [("m","i")] nat_less_cases 1);
paulson@9245
   125
by (rtac (antisym_less_inverse RS conjunct2) 1);
paulson@9245
   126
by (etac (disjI1 RS less_or_eq_imp_le RS rev_mp) 1);
paulson@9245
   127
by (etac spec 1);
paulson@9245
   128
by (rtac (antisym_less_inverse RS conjunct2) 1);
paulson@9245
   129
by (etac (disjI2 RS less_or_eq_imp_le RS rev_mp) 1);
paulson@9245
   130
by (etac spec 1);
paulson@9248
   131
by (etac chain_mono 1);
paulson@9245
   132
by (atac 1);
paulson@9248
   133
by (etac (ub_rangeD) 1);
paulson@9245
   134
qed "lub_finch1";     
nipkow@243
   135
paulson@9248
   136
Goalw [finite_chain_def]
paulson@9245
   137
        "finite_chain(C) ==> range(C) <<| C(@ i. max_in_chain i C)";
paulson@9245
   138
by (rtac lub_finch1 1);
paulson@9970
   139
by (best_tac (claset() addIs [someI]) 2);
paulson@9248
   140
by (Blast_tac 1);
paulson@9245
   141
qed "lub_finch2";
nipkow@243
   142
nipkow@243
   143
paulson@9169
   144
Goal "x<<y ==> chain (%i. if i=0 then x else y)";
paulson@9169
   145
by (rtac chainI 1);
paulson@9169
   146
by (induct_tac "i" 1);
paulson@9248
   147
by Auto_tac;  
paulson@9169
   148
qed "bin_chain";
nipkow@243
   149
paulson@9248
   150
Goalw [max_in_chain_def,le_def]
paulson@9245
   151
        "x<<y ==> max_in_chain (Suc 0) (%i. if (i=0) then x else y)";
paulson@9245
   152
by (rtac allI 1);
paulson@9245
   153
by (induct_tac "j" 1);
paulson@9248
   154
by Auto_tac; 
paulson@9245
   155
qed "bin_chainmax";
nipkow@243
   156
paulson@9169
   157
Goal "x << y ==> range(%i::nat. if (i=0) then x else y) <<| y";
paulson@9169
   158
by (res_inst_tac [("s","if (Suc 0) = 0 then x else y")] subst 1
paulson@9169
   159
    THEN rtac lub_finch1 2);
paulson@9169
   160
by (etac bin_chain 2);
paulson@9169
   161
by (etac bin_chainmax 2);
paulson@9248
   162
by (Simp_tac 1);
paulson@9169
   163
qed "lub_bin_chain";
nipkow@243
   164
nipkow@243
   165
(* ------------------------------------------------------------------------ *)
nipkow@243
   166
(* the maximal element in a chain is its lub                                *)
nipkow@243
   167
(* ------------------------------------------------------------------------ *)
nipkow@243
   168
paulson@9248
   169
Goal "[| Y i = c;  ALL i. Y i<<c |] ==> lub(range Y) = c";
paulson@9248
   170
by (blast_tac (claset()  addDs [ub_rangeD] 
paulson@9248
   171
                         addIs [thelubI, is_lubI, ub_rangeI]) 1);
paulson@9169
   172
qed "lub_chain_maxelem";
nipkow@243
   173
nipkow@243
   174
(* ------------------------------------------------------------------------ *)
nipkow@243
   175
(* the lub of a constant chain is the constant                              *)
nipkow@243
   176
(* ------------------------------------------------------------------------ *)
nipkow@243
   177
paulson@9169
   178
Goal "range(%x. c) <<| c";
paulson@9248
   179
by (blast_tac (claset()  addDs [ub_rangeD] addIs [is_lubI, ub_rangeI]) 1);
paulson@9169
   180
qed "lub_const";
nipkow@243
   181
nipkow@243
   182
nipkow@243
   183