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