src/HOLCF/Porder.ML
author paulson
Wed, 28 Jun 2000 10:54:21 +0200
changeset 9169 85a47aa21f74
parent 8935 548901d05a0e
child 9245 428385c4bc50
permissions -rw-r--r--
tidying and unbatchifying
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2033
diff changeset
     1
(*  Title:      HOLCF/Porder.thy
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
     3
    Author:     Franz Regensburger
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     4
    Copyright   1993 Technische Universitaet Muenchen
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     5
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2033
diff changeset
     6
Lemmas for theory Porder.thy 
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     7
*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     8
625
119391dd1d59 New version
nipkow
parents: 442
diff changeset
     9
(* ------------------------------------------------------------------------ *)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    10
(* lubs are unique                                                          *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    11
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    12
4031
42cbf6256d60 fixed spaces in qed;
wenzelm
parents: 3842
diff changeset
    13
qed_goalw "unique_lub" thy [is_lub, is_ub] 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    14
        "[| S <<| x ; S <<| y |] ==> x=y"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    15
( fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    16
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    17
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    18
        (etac conjE 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    19
        (etac conjE 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    20
        (rtac antisym_less 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    21
        (rtac mp 1),((etac allE 1) THEN (atac 1) THEN (atac 1)),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    22
        (rtac mp 1),((etac allE 1) THEN (atac 1) THEN (atac 1))
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    23
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    24
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    25
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    26
(* chains are monotone functions                                            *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    27
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    28
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
    29
qed_goalw "chain_mono" thy [chain] "chain F ==> x<y --> F x<<F y"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    30
( fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    31
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    32
        (cut_facts_tac prems 1),
5192
704dd3a6d47d Adapted to new datatype package.
berghofe
parents: 5068
diff changeset
    33
        (induct_tac "y" 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    34
        (rtac impI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    35
        (etac less_zeroE 1),
2033
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1886
diff changeset
    36
        (stac less_Suc_eq 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    37
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    38
        (etac disjE 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    39
        (rtac trans_less 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    40
        (etac allE 2),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    41
        (atac 2),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    42
        (fast_tac HOL_cs 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    43
        (hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    44
        (etac allE 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    45
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    46
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    47
9169
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
    48
Goal "[| chain F; x <= y |] ==> F x << F y";
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
    49
by (rtac (le_imp_less_or_eq RS disjE) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
    50
by (atac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
    51
by (etac (chain_mono RS mp) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
    52
by (atac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
    53
by (hyp_subst_tac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
    54
by (rtac refl_less 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
    55
qed "chain_mono3";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    56
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    57
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    58
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    59
(* The range of a chain is a totaly ordered     <<                           *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    60
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    61
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
    62
qed_goalw "chain_tord" thy [tord] 
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
    63
"!!F. chain(F) ==> tord(range(F))"
1886
0922b597b53d Redefining "range" as a macro -- new proof needed
paulson
parents: 1779
diff changeset
    64
 (fn _ =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    65
        [
3724
f33e301a89f5 Step_tac -> Safe_tac
paulson
parents: 3026
diff changeset
    66
        Safe_tac,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    67
        (rtac nat_less_cases 1),
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 4031
diff changeset
    68
        (ALLGOALS (fast_tac (claset() addIs [refl_less, chain_mono RS mp])))]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    69
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    70
(* ------------------------------------------------------------------------ *)
625
119391dd1d59 New version
nipkow
parents: 442
diff changeset
    71
(* technical lemmas about lub and is_lub                                    *)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    72
(* ------------------------------------------------------------------------ *)
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2033
diff changeset
    73
bind_thm("lub",lub_def RS meta_eq_to_obj_eq);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    74
9169
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
    75
Goal "? x. M <<| x ==> M <<| lub(M)";
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
    76
by (stac lub 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
    77
by (etac (select_eq_Ex RS iffD2) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
    78
qed "lubI";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    79
9169
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
    80
Goal "M <<| lub(M) ==> ? x. M <<| x";
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
    81
by (etac exI 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
    82
qed "lubE";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    83
9169
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
    84
Goal "(? x. M <<| x)  = M <<| lub(M)";
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
    85
by (stac lub 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
    86
by (rtac (select_eq_Ex RS subst) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
    87
by (rtac refl 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
    88
qed "lub_eq";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    89
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    90
9169
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
    91
Goal "M <<| l ==> lub(M) = l";
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
    92
by (rtac unique_lub 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
    93
by (stac lub 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
    94
by (etac selectI 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
    95
by (atac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
    96
qed "thelubI";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    97
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    98
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4721
diff changeset
    99
Goal "lub{x} = x";
3018
e65b60b28341 Ran expandshort
paulson
parents: 2841
diff changeset
   100
by (rtac thelubI 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 4031
diff changeset
   101
by (simp_tac (simpset() addsimps [is_lub,is_ub]) 1);
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents: 2640
diff changeset
   102
qed "lub_singleton";
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents: 2640
diff changeset
   103
Addsimps [lub_singleton];
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents: 2640
diff changeset
   104
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   105
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   106
(* access to some definition as inference rule                              *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   107
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   108
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2033
diff changeset
   109
qed_goalw "is_lubE" thy [is_lub]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   110
        "S <<| x  ==> S <| x & (! u. S <| u  --> x << u)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   111
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   112
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   113
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   114
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   115
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   116
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2033
diff changeset
   117
qed_goalw "is_lubI" thy [is_lub]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   118
        "S <| x & (! u. S <| u  --> x << u) ==> S <<| x"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   119
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   120
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   121
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   122
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   123
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   124
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
   125
qed_goalw "chainE" thy [chain] "chain F ==> !i. F(i) << F(Suc(i))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   126
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   127
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   128
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   129
        (atac 1)]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   130
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
   131
qed_goalw "chainI" thy [chain] "!i. F i << F(Suc i) ==> chain F"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   132
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   133
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   134
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   135
        (atac 1)]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   136
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   137
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   138
(* technical lemmas about (least) upper bounds of chains                    *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   139
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   140
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2033
diff changeset
   141
qed_goalw "ub_rangeE" thy [is_ub] "range S <| x  ==> !i. S(i) << x"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   142
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   143
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   144
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   145
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   146
        (rtac mp 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   147
        (etac spec 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   148
        (rtac rangeI 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   149
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   150
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2033
diff changeset
   151
qed_goalw "ub_rangeI" thy [is_ub] "!i. S i << x  ==> range S <| x"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   152
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   153
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   154
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   155
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   156
        (etac rangeE 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   157
        (hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   158
        (etac spec 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   159
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   160
1779
1155c06fa956 introduced forgotten bind_thm calls
oheimb
parents: 1675
diff changeset
   161
bind_thm ("is_ub_lub", is_lubE RS conjunct1 RS ub_rangeE RS spec);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   162
(* range(?S1) <<| ?x1 ==> ?S1(?x) << ?x1                                    *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   163
1779
1155c06fa956 introduced forgotten bind_thm calls
oheimb
parents: 1675
diff changeset
   164
bind_thm ("is_lub_lub", is_lubE RS conjunct2 RS spec RS mp);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   165
(* [| ?S3 <<| ?x3; ?S3 <| ?x1 |] ==> ?x3 << ?x1                             *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   166
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   167
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   168
(* results about finite chains                                              *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   169
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   170
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2033
diff changeset
   171
qed_goalw "lub_finch1" thy [max_in_chain_def]
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
   172
        "[| chain C; max_in_chain i C|] ==> range C <<| C i"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   173
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   174
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   175
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   176
        (rtac is_lubI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   177
        (rtac conjI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   178
        (rtac ub_rangeI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   179
        (rtac allI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   180
        (res_inst_tac [("m","i")] nat_less_cases 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   181
        (rtac (antisym_less_inverse RS conjunct2) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   182
        (etac (disjI1 RS less_or_eq_imp_le RS rev_mp) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   183
        (etac spec 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   184
        (rtac (antisym_less_inverse RS conjunct2) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   185
        (etac (disjI2 RS less_or_eq_imp_le RS rev_mp) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   186
        (etac spec 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   187
        (etac (chain_mono RS mp) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   188
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   189
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   190
        (etac (ub_rangeE RS spec) 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   191
        ]);     
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   192
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2033
diff changeset
   193
qed_goalw "lub_finch2" thy [finite_chain_def]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   194
        "finite_chain(C) ==> range(C) <<| C(@ i. max_in_chain i C)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   195
 (fn prems=>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   196
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   197
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   198
        (rtac lub_finch1 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   199
        (etac conjunct1 1),
1675
36ba4da350c3 adapted several proofs
oheimb
parents: 1461
diff changeset
   200
        (rtac (select_eq_Ex RS iffD2) 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   201
        (etac conjunct2 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   202
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   203
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   204
9169
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   205
Goal "x<<y ==> chain (%i. if i=0 then x else y)";
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   206
by (rtac chainI 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   207
by (rtac allI 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   208
by (induct_tac "i" 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   209
by (Asm_simp_tac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   210
by (Asm_simp_tac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   211
qed "bin_chain";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   212
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2033
diff changeset
   213
qed_goalw "bin_chainmax" thy [max_in_chain_def,le_def]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   214
        "x<<y ==> max_in_chain (Suc 0) (%i. if (i=0) then x else y)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   215
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   216
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   217
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   218
        (rtac allI 1),
5192
704dd3a6d47d Adapted to new datatype package.
berghofe
parents: 5068
diff changeset
   219
        (induct_tac "j" 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   220
        (Asm_simp_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   221
        (Asm_simp_tac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   222
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   223
9169
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   224
Goal "x << y ==> range(%i::nat. if (i=0) then x else y) <<| y";
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   225
by (res_inst_tac [("s","if (Suc 0) = 0 then x else y")] subst 1
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   226
    THEN rtac lub_finch1 2);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   227
by (etac bin_chain 2);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   228
by (etac bin_chainmax 2);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   229
by (Simp_tac  1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   230
qed "lub_bin_chain";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   231
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   232
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   233
(* the maximal element in a chain is its lub                                *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   234
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   235
9169
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   236
Goal "[|? i. Y i=c;!i. Y i<<c|] ==> lub(range Y) = c";
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   237
by (rtac thelubI 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   238
by (rtac is_lubI 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   239
by (rtac conjI 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   240
by (etac ub_rangeI 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   241
by (strip_tac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   242
by (etac exE 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   243
by (hyp_subst_tac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   244
by (etac (ub_rangeE RS spec) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   245
qed "lub_chain_maxelem";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   246
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   247
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   248
(* the lub of a constant chain is the constant                              *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   249
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   250
9169
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   251
Goal "range(%x. c) <<| c";
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   252
by (rtac is_lubI 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   253
by (rtac conjI 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   254
by (rtac ub_rangeI 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   255
by (strip_tac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   256
by (rtac refl_less 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   257
by (strip_tac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   258
by (etac (ub_rangeE RS spec) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8935
diff changeset
   259
qed "lub_const";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   260
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   261
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   262