src/HOLCF/Cont.ML
author oheimb
Wed, 12 Aug 1998 15:31:35 +0200
changeset 5297 410417e0fd04
parent 4721 c8a8482a8124
child 7322 d16d7ddcc842
permissions -rw-r--r--
repaired proof of chfindom_monofun2cont
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
     1
(*  Title:      HOLCF/Cont.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
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
     6
Lemmas for Cont.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
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     9
open Cont;
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    10
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
(* access to definition                                                     *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    13
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    14
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
    15
qed_goalw "contlubI" thy [contlub]
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
    16
        "! Y. chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))==>\
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    17
\        contlub(f)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    18
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    19
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    20
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    21
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    22
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    23
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
    24
qed_goalw "contlubE" thy [contlub]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    25
        " contlub(f)==>\
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
    26
\         ! Y. chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    27
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    28
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    29
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    30
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    31
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    32
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    33
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
    34
qed_goalw "contI" thy [cont]
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
    35
 "! Y. chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y))) ==> cont(f)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    36
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    37
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    38
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    39
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    40
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    41
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
    42
qed_goalw "contE" thy [cont]
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
    43
 "cont(f) ==> ! Y. chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y)))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    44
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    45
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    46
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    47
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    48
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    49
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    50
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
    51
qed_goalw "monofunI" thy [monofun]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    52
        "! x y. x << y --> f(x) << f(y) ==> monofun(f)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    53
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    54
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    55
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    56
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    57
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    58
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
    59
qed_goalw "monofunE" thy [monofun]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    60
        "monofun(f) ==> ! x y. x << y --> f(x) << f(y)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    61
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    62
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    63
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    64
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    65
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    66
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    67
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    68
(* the main purpose of cont.thy is to show:                                 *)
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 892
diff changeset
    69
(*              monofun(f) & contlub(f)  <==> cont(f)                      *)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    70
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    71
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    72
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    73
(* monotone functions map chains to chains                                  *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    74
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    75
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
    76
qed_goal "ch2ch_monofun" thy 
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
    77
        "[| monofun(f); chain(Y) |] ==> chain(%i. f(Y(i)))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    78
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    79
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    80
        (cut_facts_tac prems 1),
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
    81
        (rtac chainI 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    82
        (rtac allI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    83
        (etac (monofunE RS spec RS spec RS mp) 1),
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
    84
        (etac (chainE RS spec) 1)
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    85
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    86
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    87
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    88
(* monotone functions map upper bound to upper bounds                       *)
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
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
    91
qed_goal "ub2ub_monofun" thy 
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3326
diff changeset
    92
 "[| monofun(f); range(Y) <| u|]  ==> range(%i. f(Y(i))) <| f(u)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    93
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    94
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    95
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    96
        (rtac ub_rangeI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    97
        (rtac allI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    98
        (etac (monofunE RS spec RS spec RS mp) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    99
        (etac (ub_rangeE RS spec) 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   100
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   101
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   102
(* ------------------------------------------------------------------------ *)
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 892
diff changeset
   103
(* left to right: monofun(f) & contlub(f)  ==> cont(f)                     *)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   104
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   105
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   106
qed_goalw "monocontlub2cont" thy [cont]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   107
        "[|monofun(f);contlub(f)|] ==> cont(f)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   108
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   109
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   110
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   111
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   112
        (rtac thelubE 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   113
        (etac ch2ch_monofun 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   114
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   115
        (etac (contlubE RS spec RS mp RS sym) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   116
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   117
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   118
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   119
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   120
(* first a lemma about binary chains                                        *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   121
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   122
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   123
qed_goal "binchain_cont" thy
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 892
diff changeset
   124
"[| cont(f); x << y |]  ==> range(%i. f(if i = 0 then x else y)) <<| f(y)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   125
(fn prems => 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   126
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   127
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   128
        (rtac subst 1), 
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   129
        (etac (contE RS spec RS mp) 2),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   130
        (etac bin_chain 2),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   131
        (res_inst_tac [("y","y")] arg_cong 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   132
        (etac (lub_bin_chain RS thelubI) 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   133
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   134
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   135
(* ------------------------------------------------------------------------ *)
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 892
diff changeset
   136
(* right to left: cont(f) ==> monofun(f) & contlub(f)                      *)
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 892
diff changeset
   137
(* part1:         cont(f) ==> monofun(f                                    *)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   138
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   139
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   140
qed_goalw "cont2mono" thy [monofun]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   141
        "cont(f) ==> monofun(f)"
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
        (res_inst_tac [("s","if 0 = 0 then x else y")] subst 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   147
        (rtac (binchain_cont RS is_ub_lub) 2),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   148
        (atac 2),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   149
        (atac 2),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   150
        (Simp_tac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   151
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   152
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   153
(* ------------------------------------------------------------------------ *)
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 892
diff changeset
   154
(* right to left: cont(f) ==> monofun(f) & contlub(f)                      *)
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 892
diff changeset
   155
(* part2:         cont(f) ==>              contlub(f)                      *)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   156
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   157
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   158
qed_goalw "cont2contlub" thy [contlub]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   159
        "cont(f) ==> contlub(f)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   160
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   161
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   162
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   163
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   164
        (rtac (thelubI RS sym) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   165
        (etac (contE RS spec RS mp) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   166
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   167
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   168
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   169
(* ------------------------------------------------------------------------ *)
2354
b4a1e3306aa0 added theorems
sandnerr
parents: 2033
diff changeset
   170
(* monotone functions map finite chains to finite chains              	    *)
b4a1e3306aa0 added theorems
sandnerr
parents: 2033
diff changeset
   171
(* ------------------------------------------------------------------------ *)
b4a1e3306aa0 added theorems
sandnerr
parents: 2033
diff changeset
   172
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   173
qed_goalw "monofun_finch2finch" thy [finite_chain_def]
2354
b4a1e3306aa0 added theorems
sandnerr
parents: 2033
diff changeset
   174
  "[| monofun f; finite_chain Y |] ==> finite_chain (%n. f (Y n))" 
b4a1e3306aa0 added theorems
sandnerr
parents: 2033
diff changeset
   175
(fn prems => 
b4a1e3306aa0 added theorems
sandnerr
parents: 2033
diff changeset
   176
	[
b4a1e3306aa0 added theorems
sandnerr
parents: 2033
diff changeset
   177
	cut_facts_tac prems 1,
b4a1e3306aa0 added theorems
sandnerr
parents: 2033
diff changeset
   178
	safe_tac HOL_cs,
b4a1e3306aa0 added theorems
sandnerr
parents: 2033
diff changeset
   179
	fast_tac (HOL_cs addSEs [ch2ch_monofun]) 1,
b4a1e3306aa0 added theorems
sandnerr
parents: 2033
diff changeset
   180
	fast_tac (HOL_cs addss (HOL_ss addsimps [max_in_chain_def])) 1
b4a1e3306aa0 added theorems
sandnerr
parents: 2033
diff changeset
   181
	]);
b4a1e3306aa0 added theorems
sandnerr
parents: 2033
diff changeset
   182
b4a1e3306aa0 added theorems
sandnerr
parents: 2033
diff changeset
   183
(* ------------------------------------------------------------------------ *)
b4a1e3306aa0 added theorems
sandnerr
parents: 2033
diff changeset
   184
(* The same holds for continuous functions				    *)
b4a1e3306aa0 added theorems
sandnerr
parents: 2033
diff changeset
   185
(* ------------------------------------------------------------------------ *)
b4a1e3306aa0 added theorems
sandnerr
parents: 2033
diff changeset
   186
b4a1e3306aa0 added theorems
sandnerr
parents: 2033
diff changeset
   187
bind_thm ("cont_finch2finch", cont2mono RS monofun_finch2finch);
b4a1e3306aa0 added theorems
sandnerr
parents: 2033
diff changeset
   188
(* [| cont ?f; finite_chain ?Y |] ==> finite_chain (%n. ?f (?Y n)) *)
b4a1e3306aa0 added theorems
sandnerr
parents: 2033
diff changeset
   189
b4a1e3306aa0 added theorems
sandnerr
parents: 2033
diff changeset
   190
b4a1e3306aa0 added theorems
sandnerr
parents: 2033
diff changeset
   191
(* ------------------------------------------------------------------------ *)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   192
(* The following results are about a curried function that is monotone      *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   193
(* in both arguments                                                        *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   194
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   195
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   196
qed_goal "ch2ch_MF2L" thy 
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
   197
"[|monofun(MF2); chain(F)|] ==> chain(%i. MF2 (F i) x)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   198
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   199
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   200
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   201
        (etac (ch2ch_monofun RS ch2ch_fun) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   202
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   203
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   204
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   205
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   206
qed_goal "ch2ch_MF2R" thy 
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
   207
"[|monofun(MF2(f)); chain(Y)|] ==> chain(%i. MF2 f (Y i))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   208
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   209
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   210
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   211
        (etac ch2ch_monofun 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   212
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   213
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   214
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   215
qed_goal "ch2ch_MF2LR" thy 
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
   216
"[|monofun(MF2); !f. monofun(MF2(f)); chain(F); chain(Y)|] ==> \
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
   217
\  chain(%i. MF2(F(i))(Y(i)))"
752
b89462f9d5f1 ----------------------------------------------------------------------
regensbu
parents: 625
diff changeset
   218
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   219
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   220
        (cut_facts_tac prems 1),
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
   221
        (rtac chainI 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   222
        (strip_tac 1 ),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   223
        (rtac trans_less 1),
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
   224
        (etac (ch2ch_MF2L RS chainE RS spec) 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   225
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   226
        ((rtac (monofunE RS spec RS spec RS mp) 1) THEN (etac spec 1)),
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
   227
        (etac (chainE RS spec) 1)
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   228
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   229
752
b89462f9d5f1 ----------------------------------------------------------------------
regensbu
parents: 625
diff changeset
   230
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   231
qed_goal "ch2ch_lubMF2R" thy 
2838
2e908f29bc3d changed continuous functions from pcpo to cpo (including instances)
slotosch
parents: 2640
diff changeset
   232
"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3326
diff changeset
   233
\  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
   234
\       chain(F);chain(Y)|] ==> \
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
   235
\       chain(%j. lub(range(%i. MF2 (F j) (Y i))))"
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),
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
   239
        (rtac (lub_mono RS allI RS chainI) 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   240
        ((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   241
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   242
        ((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   243
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   244
        (strip_tac 1),
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
   245
        (rtac (chainE RS spec) 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   246
        (etac ch2ch_MF2L 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   247
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   248
        ]);
243
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
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   251
qed_goal "ch2ch_lubMF2L" thy 
2838
2e908f29bc3d changed continuous functions from pcpo to cpo (including instances)
slotosch
parents: 2640
diff changeset
   252
"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3326
diff changeset
   253
\  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
   254
\       chain(F);chain(Y)|] ==> \
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
   255
\       chain(%i. lub(range(%j. MF2 (F j) (Y i))))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   256
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   257
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   258
        (cut_facts_tac prems 1),
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
   259
        (rtac (lub_mono RS allI RS chainI) 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   260
        (etac ch2ch_MF2L 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   261
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   262
        (etac ch2ch_MF2L 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   263
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   264
        (strip_tac 1),
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
   265
        (rtac (chainE RS spec) 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   266
        ((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   267
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   268
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   269
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   270
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   271
qed_goal "lub_MF2_mono" thy 
2838
2e908f29bc3d changed continuous functions from pcpo to cpo (including instances)
slotosch
parents: 2640
diff changeset
   272
"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3326
diff changeset
   273
\  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
   274
\       chain(F)|] ==> \
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3326
diff changeset
   275
\       monofun(% x. lub(range(% j. MF2 (F j) (x))))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   276
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   277
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   278
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   279
        (rtac monofunI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   280
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   281
        (rtac lub_mono 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   282
        (etac ch2ch_MF2L 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   283
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   284
        (etac ch2ch_MF2L 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   285
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   286
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   287
        ((rtac (monofunE RS spec RS spec RS mp) 1) THEN (etac spec 1)),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   288
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   289
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   290
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   291
qed_goal "ex_lubMF2" thy 
2838
2e908f29bc3d changed continuous functions from pcpo to cpo (including instances)
slotosch
parents: 2640
diff changeset
   292
"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3326
diff changeset
   293
\  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
   294
\       chain(F); chain(Y)|] ==> \
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   295
\               lub(range(%j. lub(range(%i. MF2(F j) (Y i))))) =\
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   296
\               lub(range(%i. lub(range(%j. MF2(F j) (Y i)))))"
752
b89462f9d5f1 ----------------------------------------------------------------------
regensbu
parents: 625
diff changeset
   297
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   298
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   299
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   300
        (rtac antisym_less 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   301
        (rtac (ub_rangeI RSN (2,is_lub_thelub)) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   302
        (etac ch2ch_lubMF2R 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   303
        (REPEAT (atac 1)),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   304
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   305
        (rtac lub_mono 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   306
        ((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   307
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   308
        (etac ch2ch_lubMF2L 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   309
        (REPEAT (atac 1)),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   310
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   311
        (rtac is_ub_thelub 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   312
        (etac ch2ch_MF2L 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   313
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   314
        (rtac (ub_rangeI RSN (2,is_lub_thelub)) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   315
        (etac ch2ch_lubMF2L 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   316
        (REPEAT (atac 1)),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   317
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   318
        (rtac lub_mono 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   319
        (etac ch2ch_MF2L 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   320
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   321
        (etac ch2ch_lubMF2R 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   322
        (REPEAT (atac 1)),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   323
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   324
        (rtac is_ub_thelub 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   325
        ((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   326
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   327
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   328
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   329
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   330
qed_goal "diag_lubMF2_1" thy 
2838
2e908f29bc3d changed continuous functions from pcpo to cpo (including instances)
slotosch
parents: 2640
diff changeset
   331
"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3326
diff changeset
   332
\  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
   333
\  chain(FY);chain(TY)|] ==>\
752
b89462f9d5f1 ----------------------------------------------------------------------
regensbu
parents: 625
diff changeset
   334
\ lub(range(%i. lub(range(%j. MF2(FY(j))(TY(i)))))) =\
b89462f9d5f1 ----------------------------------------------------------------------
regensbu
parents: 625
diff changeset
   335
\ lub(range(%i. MF2(FY(i))(TY(i))))"
625
119391dd1d59 New version
nipkow
parents: 243
diff changeset
   336
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   337
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   338
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   339
        (rtac antisym_less 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   340
        (rtac (ub_rangeI RSN (2,is_lub_thelub)) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   341
        (etac ch2ch_lubMF2L 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   342
        (REPEAT (atac 1)),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   343
        (strip_tac 1 ),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   344
        (rtac lub_mono3 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   345
        (etac ch2ch_MF2L 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   346
        (REPEAT (atac 1)),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   347
        (etac ch2ch_MF2LR 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   348
        (REPEAT (atac 1)),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   349
        (rtac allI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   350
        (res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   351
        (res_inst_tac [("x","ia")] exI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   352
        (rtac (chain_mono RS mp) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   353
        (etac allE 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   354
        (etac ch2ch_MF2R 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   355
        (REPEAT (atac 1)),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   356
        (hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   357
        (res_inst_tac [("x","ia")] exI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   358
        (rtac refl_less 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   359
        (res_inst_tac [("x","i")] exI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   360
        (rtac (chain_mono RS mp) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   361
        (etac ch2ch_MF2L 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   362
        (REPEAT (atac 1)),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   363
        (rtac lub_mono 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   364
        (etac ch2ch_MF2LR 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   365
        (REPEAT(atac 1)),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   366
        (etac ch2ch_lubMF2L 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   367
        (REPEAT (atac 1)),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   368
        (strip_tac 1 ),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   369
        (rtac is_ub_thelub 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   370
        (etac ch2ch_MF2L 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   371
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   372
        ]);
625
119391dd1d59 New version
nipkow
parents: 243
diff changeset
   373
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   374
qed_goal "diag_lubMF2_2" thy 
2838
2e908f29bc3d changed continuous functions from pcpo to cpo (including instances)
slotosch
parents: 2640
diff changeset
   375
"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3326
diff changeset
   376
\  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
   377
\  chain(FY);chain(TY)|] ==>\
752
b89462f9d5f1 ----------------------------------------------------------------------
regensbu
parents: 625
diff changeset
   378
\ lub(range(%j. lub(range(%i. MF2(FY(j))(TY(i)))))) =\
b89462f9d5f1 ----------------------------------------------------------------------
regensbu
parents: 625
diff changeset
   379
\ lub(range(%i. MF2(FY(i))(TY(i))))"
625
119391dd1d59 New version
nipkow
parents: 243
diff changeset
   380
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   381
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   382
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   383
        (rtac trans 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   384
        (rtac ex_lubMF2 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   385
        (REPEAT (atac 1)),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   386
        (etac diag_lubMF2_1 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   387
        (REPEAT (atac 1))
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   388
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   389
752
b89462f9d5f1 ----------------------------------------------------------------------
regensbu
parents: 625
diff changeset
   390
b89462f9d5f1 ----------------------------------------------------------------------
regensbu
parents: 625
diff changeset
   391
(* ------------------------------------------------------------------------ *)
b89462f9d5f1 ----------------------------------------------------------------------
regensbu
parents: 625
diff changeset
   392
(* The following results are about a curried function that is continuous    *)
b89462f9d5f1 ----------------------------------------------------------------------
regensbu
parents: 625
diff changeset
   393
(* in both arguments                                                        *)
b89462f9d5f1 ----------------------------------------------------------------------
regensbu
parents: 625
diff changeset
   394
(* ------------------------------------------------------------------------ *)
b89462f9d5f1 ----------------------------------------------------------------------
regensbu
parents: 625
diff changeset
   395
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   396
qed_goal "contlub_CF2" thy 
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
   397
"[|cont(CF2);!f. cont(CF2(f));chain(FY);chain(TY)|] ==>\
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3326
diff changeset
   398
\ CF2(lub(range(FY)))(lub(range(TY))) = lub(range(%i. CF2(FY(i))(TY(i))))"
625
119391dd1d59 New version
nipkow
parents: 243
diff changeset
   399
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   400
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   401
        (cut_facts_tac prems 1),
2033
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1779
diff changeset
   402
        (stac ((hd prems) RS cont2contlub RS contlubE RS spec RS mp) 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   403
        (atac 1),
2033
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1779
diff changeset
   404
        (stac thelub_fun 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   405
        (rtac ((hd prems) RS cont2mono RS ch2ch_monofun) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   406
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   407
        (rtac trans 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   408
        (rtac (((hd (tl prems)) RS spec RS cont2contlub) RS contlubE RS                spec RS mp RS ext RS arg_cong RS arg_cong) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   409
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   410
        (rtac diag_lubMF2_2 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   411
        (etac cont2mono 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   412
        (rtac allI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   413
        (etac allE 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   414
        (etac cont2mono 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   415
        (REPEAT (atac 1))
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   416
        ]);
752
b89462f9d5f1 ----------------------------------------------------------------------
regensbu
parents: 625
diff changeset
   417
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   418
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   419
(* The following results are about application for functions in 'a=>'b      *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   420
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   421
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   422
qed_goal "monofun_fun_fun" thy 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   423
        "f1 << f2 ==> f1(x) << f2(x)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   424
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   425
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   426
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   427
        (etac (less_fun RS iffD1 RS spec) 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   428
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   429
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   430
qed_goal "monofun_fun_arg" thy 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   431
        "[|monofun(f); x1 << x2|] ==> f(x1) << f(x2)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   432
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   433
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   434
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   435
        (etac (monofunE RS spec RS spec RS mp) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   436
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   437
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   438
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   439
qed_goal "monofun_fun" thy 
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   440
"[|monofun(f1); monofun(f2); f1 << f2; x1 << x2|] ==> f1(x1) << f2(x2)"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   441
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   442
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   443
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   444
        (rtac trans_less 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   445
        (etac monofun_fun_arg 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   446
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   447
        (etac monofun_fun_fun 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   448
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   449
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   450
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   451
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   452
(* The following results are about the propagation of monotonicity and      *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   453
(* continuity                                                               *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   454
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   455
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   456
qed_goal "mono2mono_MF1L" thy 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   457
        "[|monofun(c1)|] ==> monofun(%x. c1 x y)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   458
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   459
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   460
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   461
        (rtac monofunI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   462
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   463
        (etac (monofun_fun_arg RS monofun_fun_fun) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   464
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   465
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   466
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   467
qed_goal "cont2cont_CF1L" thy 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   468
        "[|cont(c1)|] ==> cont(%x. c1 x y)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   469
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   470
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   471
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   472
        (rtac monocontlub2cont 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   473
        (etac (cont2mono RS mono2mono_MF1L) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   474
        (rtac contlubI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   475
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   476
        (rtac ((hd prems) RS cont2contlub RS 
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   477
                contlubE RS spec RS mp RS ssubst) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   478
        (atac 1),
2033
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1779
diff changeset
   479
        (stac thelub_fun 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   480
        (rtac ch2ch_monofun 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   481
        (etac cont2mono 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   482
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   483
        (rtac refl 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   484
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   485
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 892
diff changeset
   486
(*********  Note "(%x.%y.c1 x y) = c1" ***********)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   487
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   488
qed_goal "mono2mono_MF1L_rev" thy
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3326
diff changeset
   489
        "!y. monofun(%x. c1 x y) ==> monofun(c1)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   490
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   491
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   492
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   493
        (rtac monofunI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   494
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   495
        (rtac (less_fun RS iffD2) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   496
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   497
        (rtac ((hd prems) RS spec RS monofunE RS spec RS spec RS mp) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   498
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   499
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   500
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   501
qed_goal "cont2cont_CF1L_rev" thy
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3326
diff changeset
   502
        "!y. cont(%x. c1 x y) ==> cont(c1)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   503
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   504
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   505
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   506
        (rtac monocontlub2cont 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   507
        (rtac (cont2mono RS allI RS mono2mono_MF1L_rev ) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   508
        (etac spec 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   509
        (rtac contlubI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   510
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   511
        (rtac ext 1),
2033
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1779
diff changeset
   512
        (stac thelub_fun 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   513
        (rtac (cont2mono RS allI RS mono2mono_MF1L_rev RS ch2ch_monofun) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   514
        (etac spec 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   515
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   516
        (rtac 
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   517
        ((hd prems) RS spec RS cont2contlub RS contlubE RS spec RS mp) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   518
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   519
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   520
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   521
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   522
(* What D.A.Schmidt calls continuity of abstraction                         *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   523
(* never used here                                                          *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   524
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   525
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   526
qed_goal "contlub_abstraction" thy
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
   527
"[|chain(Y::nat=>'a);!y. cont(%x.(c::'a::cpo=>'b::cpo=>'c::cpo) x y)|] ==>\
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3326
diff changeset
   528
\ (%y. lub(range(%i. c (Y i) y))) = (lub(range(%i.%y. c (Y i) y)))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   529
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   530
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   531
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   532
        (rtac trans 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   533
        (rtac (cont2contlub RS contlubE RS spec RS mp) 2),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   534
        (atac 3),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   535
        (etac cont2cont_CF1L_rev 2),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   536
        (rtac ext 1), 
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   537
        (rtac (cont2contlub RS contlubE RS spec RS mp RS sym) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   538
        (etac spec 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   539
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   540
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   541
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   542
qed_goal "mono2mono_app" thy 
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3326
diff changeset
   543
"[|monofun(ft);!x. monofun(ft(x));monofun(tt)|] ==>\
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   544
\        monofun(%x.(ft(x))(tt(x)))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   545
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   546
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   547
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   548
        (rtac monofunI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   549
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   550
        (res_inst_tac [("f1.0","ft(x)"),("f2.0","ft(y)")] monofun_fun 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   551
        (etac spec 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   552
        (etac spec 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   553
        (etac (monofunE RS spec RS spec RS mp) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   554
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   555
        (etac (monofunE RS spec RS spec RS mp) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   556
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   557
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   558
625
119391dd1d59 New version
nipkow
parents: 243
diff changeset
   559
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   560
qed_goal "cont2contlub_app" thy 
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3326
diff changeset
   561
"[|cont(ft);!x. cont(ft(x));cont(tt)|] ==> contlub(%x.(ft(x))(tt(x)))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   562
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   563
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   564
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   565
        (rtac contlubI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   566
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   567
        (res_inst_tac [("f3","tt")] (contlubE RS spec RS mp RS ssubst) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   568
        (etac cont2contlub 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   569
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   570
        (rtac contlub_CF2 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   571
        (REPEAT (atac 1)),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   572
        (etac (cont2mono RS ch2ch_monofun) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   573
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   574
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   575
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   576
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   577
qed_goal "cont2cont_app" thy 
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3326
diff changeset
   578
"[|cont(ft);!x. cont(ft(x));cont(tt)|] ==>\
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   579
\        cont(%x.(ft(x))(tt(x)))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   580
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   581
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   582
        (rtac monocontlub2cont 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   583
        (rtac mono2mono_app 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   584
        (rtac cont2mono 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   585
        (resolve_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   586
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   587
        (rtac cont2mono 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   588
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   589
        (etac spec 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   590
        (rtac cont2mono 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   591
        (resolve_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   592
        (rtac cont2contlub_app 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   593
        (resolve_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   594
        (resolve_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   595
        (resolve_tac prems 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   596
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   597
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   598
1779
1155c06fa956 introduced forgotten bind_thm calls
oheimb
parents: 1461
diff changeset
   599
bind_thm ("cont2cont_app2", allI RSN (2,cont2cont_app));
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 892
diff changeset
   600
(*  [| cont ?ft; !!x. cont (?ft x); cont ?tt |] ==> *)
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 892
diff changeset
   601
(*        cont (%x. ?ft x (?tt x))                    *)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   602
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   603
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   604
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   605
(* The identity function is continuous                                      *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   606
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   607
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3326
diff changeset
   608
qed_goal "cont_id" thy "cont(% x. x)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   609
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   610
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   611
        (rtac contI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   612
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   613
        (etac thelubE 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   614
        (rtac refl 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   615
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   616
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   617
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   618
(* constant functions are continuous                                        *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   619
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   620
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3326
diff changeset
   621
qed_goalw "cont_const" thy [cont] "cont(%x. c)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   622
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   623
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   624
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   625
        (rtac is_lubI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   626
        (rtac conjI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   627
        (rtac ub_rangeI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   628
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   629
        (rtac refl_less 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   630
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   631
        (dtac ub_rangeE 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   632
        (etac spec 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   633
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   634
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   635
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   636
qed_goal "cont2cont_app3" thy 
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 892
diff changeset
   637
 "[|cont(f);cont(t) |] ==> cont(%x. f(t(x)))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   638
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   639
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   640
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   641
        (rtac cont2cont_app2 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   642
        (rtac cont_const 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   643
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   644
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   645
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   646
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   647
(* ------------------------------------------------------------------------ *)
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   648
(* A non-emptyness result for Cfun                                          *)
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   649
(* ------------------------------------------------------------------------ *)
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   650
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   651
qed_goal "CfunI" thy "?x:Collect cont"
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   652
 (fn prems =>
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   653
        [
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   654
        (rtac CollectI 1),
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   655
        (rtac cont_const 1)
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2354
diff changeset
   656
        ]);
3326
930c9bed5a09 Moved the classes flat chfin from Fix to Pcpo.
slotosch
parents: 2838
diff changeset
   657
930c9bed5a09 Moved the classes flat chfin from Fix to Pcpo.
slotosch
parents: 2838
diff changeset
   658
(* ------------------------------------------------------------------------ *)
930c9bed5a09 Moved the classes flat chfin from Fix to Pcpo.
slotosch
parents: 2838
diff changeset
   659
(* some properties of flat			 			    *)
930c9bed5a09 Moved the classes flat chfin from Fix to Pcpo.
slotosch
parents: 2838
diff changeset
   660
(* ------------------------------------------------------------------------ *)
930c9bed5a09 Moved the classes flat chfin from Fix to Pcpo.
slotosch
parents: 2838
diff changeset
   661
930c9bed5a09 Moved the classes flat chfin from Fix to Pcpo.
slotosch
parents: 2838
diff changeset
   662
qed_goalw "flatdom2monofun" thy [monofun]
930c9bed5a09 Moved the classes flat chfin from Fix to Pcpo.
slotosch
parents: 2838
diff changeset
   663
  "f UU = UU ==> monofun (f::'a::flat=>'b::pcpo)" 
930c9bed5a09 Moved the classes flat chfin from Fix to Pcpo.
slotosch
parents: 2838
diff changeset
   664
(fn prems => 
930c9bed5a09 Moved the classes flat chfin from Fix to Pcpo.
slotosch
parents: 2838
diff changeset
   665
	[
930c9bed5a09 Moved the classes flat chfin from Fix to Pcpo.
slotosch
parents: 2838
diff changeset
   666
	cut_facts_tac prems 1,
930c9bed5a09 Moved the classes flat chfin from Fix to Pcpo.
slotosch
parents: 2838
diff changeset
   667
	strip_tac 1,
930c9bed5a09 Moved the classes flat chfin from Fix to Pcpo.
slotosch
parents: 2838
diff changeset
   668
	dtac (ax_flat RS spec RS spec RS mp) 1,
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
   669
	fast_tac ((HOL_cs addss (simpset() addsimps [minimal]))) 1
3326
930c9bed5a09 Moved the classes flat chfin from Fix to Pcpo.
slotosch
parents: 2838
diff changeset
   670
	]);
930c9bed5a09 Moved the classes flat chfin from Fix to Pcpo.
slotosch
parents: 2838
diff changeset
   671
930c9bed5a09 Moved the classes flat chfin from Fix to Pcpo.
slotosch
parents: 2838
diff changeset
   672
5297
410417e0fd04 repaired proof of chfindom_monofun2cont
oheimb
parents: 4721
diff changeset
   673
Goal "monofun f ==> cont(f::'a::chfin=>'b::pcpo)";
410417e0fd04 repaired proof of chfindom_monofun2cont
oheimb
parents: 4721
diff changeset
   674
by(rtac monocontlub2cont 1);
410417e0fd04 repaired proof of chfindom_monofun2cont
oheimb
parents: 4721
diff changeset
   675
by( atac 1);
410417e0fd04 repaired proof of chfindom_monofun2cont
oheimb
parents: 4721
diff changeset
   676
by(rtac contlubI 1);
410417e0fd04 repaired proof of chfindom_monofun2cont
oheimb
parents: 4721
diff changeset
   677
by(strip_tac 1);
410417e0fd04 repaired proof of chfindom_monofun2cont
oheimb
parents: 4721
diff changeset
   678
by(forward_tac [chfin2finch] 1);
410417e0fd04 repaired proof of chfindom_monofun2cont
oheimb
parents: 4721
diff changeset
   679
by(rtac antisym_less 1);
410417e0fd04 repaired proof of chfindom_monofun2cont
oheimb
parents: 4721
diff changeset
   680
by( force_tac (HOL_cs addIs [is_ub_thelub,ch2ch_monofun],
410417e0fd04 repaired proof of chfindom_monofun2cont
oheimb
parents: 4721
diff changeset
   681
               HOL_ss addsimps [finite_chain_def,maxinch_is_thelub]) 1);
410417e0fd04 repaired proof of chfindom_monofun2cont
oheimb
parents: 4721
diff changeset
   682
by(dtac (monofun_finch2finch COMP swap_prems_rl) 1);
410417e0fd04 repaired proof of chfindom_monofun2cont
oheimb
parents: 4721
diff changeset
   683
by( atac 1);
410417e0fd04 repaired proof of chfindom_monofun2cont
oheimb
parents: 4721
diff changeset
   684
by(asm_full_simp_tac (HOL_ss addsimps [finite_chain_def]) 1);
410417e0fd04 repaired proof of chfindom_monofun2cont
oheimb
parents: 4721
diff changeset
   685
by(etac conjE 1);
410417e0fd04 repaired proof of chfindom_monofun2cont
oheimb
parents: 4721
diff changeset
   686
by(etac exE 1);
410417e0fd04 repaired proof of chfindom_monofun2cont
oheimb
parents: 4721
diff changeset
   687
by(asm_full_simp_tac (HOL_ss addsimps [maxinch_is_thelub]) 1);
410417e0fd04 repaired proof of chfindom_monofun2cont
oheimb
parents: 4721
diff changeset
   688
by(etac (monofunE RS spec RS spec RS mp) 1);
410417e0fd04 repaired proof of chfindom_monofun2cont
oheimb
parents: 4721
diff changeset
   689
by(etac is_ub_thelub 1);
410417e0fd04 repaired proof of chfindom_monofun2cont
oheimb
parents: 4721
diff changeset
   690
qed "chfindom_monofun2cont";
3326
930c9bed5a09 Moved the classes flat chfin from Fix to Pcpo.
slotosch
parents: 2838
diff changeset
   691
930c9bed5a09 Moved the classes flat chfin from Fix to Pcpo.
slotosch
parents: 2838
diff changeset
   692
bind_thm ("flatdom_strict2cont",flatdom2monofun RS chfindom_monofun2cont);
930c9bed5a09 Moved the classes flat chfin from Fix to Pcpo.
slotosch
parents: 2838
diff changeset
   693
(* f UU = UU ==> cont (f::'a=>'b::pcpo)" *)