src/HOLCF/Pcpo.ML
author slotosch
Sun, 25 May 1997 11:07:52 +0200
changeset 3323 194ae2e0c193
parent 2839 7ca787c6efca
child 3326 930c9bed5a09
permissions -rw-r--r--
eliminated the constant less by the introduction of the axclass sq_ord added explicit type ::'a::po in the following theorems: minimal2UU,antisym_less_inverse,box_less,not_less2not_eq,monofun_pair and dist_eqI (in domain-package) added instances instance fun :: (term,sq_ord)sq_ord instance "->" :: (term,sq_ord)sq_ord instance "**" :: (sq_ord,sq_ord)sq_ord instance "*" :: (sq_ord,sq_ord)sq_ord instance "++" :: (pcpo,pcpo)sq_ord instance u :: (sq_ord)sq_ord instance lift :: (term)sq_ord instance discr :: (term)sq_ord
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
        ]);