src/HOLCF/Cont.thy
author huffman
Fri, 27 May 2005 01:12:15 +0200
changeset 16096 16e895296b2a
parent 16070 4a83dd540b88
child 16204 5dd79d3f0105
permissions -rw-r--r--
added lemmas monofun_lub_fun and cont_lub_fun
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15600
a59f07556a8d fixed filename in header
huffman
parents: 15588
diff changeset
     1
(*  Title:      HOLCF/Cont.thy
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     2
    ID:         $Id$
1479
21eb5e156d91 expanded tabs
clasohm
parents: 1274
diff changeset
     3
    Author:     Franz Regensburger
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     4
16070
4a83dd540b88 removed LICENCE note -- everything is subject to Isabelle licence as
wenzelm
parents: 16053
diff changeset
     5
Results about continuity and monotonicity.
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     6
*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     7
15577
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
     8
header {* Continuity and monotonicity *}
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
     9
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
    10
theory Cont
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
    11
imports FunCpo
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
    12
begin
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    13
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    14
text {*
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    15
   Now we change the default class! Form now on all untyped type variables are
3323
194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord
slotosch
parents: 2838
diff changeset
    16
   of default class po
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    17
*}
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    18
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    19
defaultsort po
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    20
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    21
consts  
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    22
        monofun :: "('a => 'b) => bool"  -- "monotonicity"
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    23
        contlub :: "('a::cpo => 'b::cpo) => bool"  -- "first cont. def"
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    24
        cont    :: "('a::cpo => 'b::cpo) => bool"  -- "secnd cont. def"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    25
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 1150
diff changeset
    26
defs 
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    27
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    28
monofun:         "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
    29
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    30
contlub:         "contlub(f) == ! Y. chain(Y) --> 
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3323
diff changeset
    31
                                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
    32
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    33
cont:            "cont(f)   == ! Y. chain(Y) --> 
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3323
diff changeset
    34
                                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
    35
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    36
text {*
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    37
  the main purpose of cont.thy is to show:
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    38
  @{prop "monofun(f) & contlub(f) == cont(f)"}
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    39
*}
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    40
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    41
text {* access to definition *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    42
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    43
lemma contlubI:
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    44
        "! Y. chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))==>
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    45
        contlub(f)"
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    46
by (unfold contlub)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    47
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    48
lemma contlubE: 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    49
        " contlub(f)==> 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    50
          ! Y. chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))"
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    51
by (unfold contlub)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    52
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    53
lemma contI: 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    54
 "! Y. chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y))) ==> cont(f)"
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    55
by (unfold cont)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    56
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    57
lemma contE: 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    58
 "cont(f) ==> ! Y. chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y)))"
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    59
by (unfold cont)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    60
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    61
lemma monofunI: 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    62
        "! x y. x << y --> f(x) << f(y) ==> monofun(f)"
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    63
by (unfold monofun)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    64
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    65
lemma monofunE: 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    66
        "monofun(f) ==> ! x y. x << y --> f(x) << f(y)"
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    67
by (unfold monofun)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    68
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    69
text {* monotone functions map chains to chains *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    70
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    71
lemma ch2ch_monofun: 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    72
        "[| monofun(f); chain(Y) |] ==> chain(%i. f(Y(i)))"
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    73
apply (rule chainI)
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    74
apply (erule monofunE [rule_format])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    75
apply (erule chainE)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    76
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    77
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    78
text {* monotone functions map upper bound to upper bounds *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    79
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    80
lemma ub2ub_monofun: 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    81
 "[| monofun(f); range(Y) <| u|]  ==> range(%i. f(Y(i))) <| f(u)"
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    82
apply (rule ub_rangeI)
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    83
apply (erule monofunE [rule_format])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    84
apply (erule ub_rangeD)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    85
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    86
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    87
text {* left to right: @{prop "monofun(f) & contlub(f) ==> cont(f)"} *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    88
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    89
lemma monocontlub2cont: 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    90
        "[|monofun(f);contlub(f)|] ==> cont(f)"
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    91
apply (rule contI [rule_format])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    92
apply (rule thelubE)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    93
apply (erule ch2ch_monofun)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    94
apply assumption
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    95
apply (erule contlubE [rule_format, symmetric])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    96
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    97
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    98
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    99
text {* first a lemma about binary chains *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   100
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   101
lemma binchain_cont: "[| cont(f); x << y |]   
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   102
      ==> range(%i::nat. f(if i = 0 then x else y)) <<| f(y)"
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   103
apply (rule subst)
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   104
prefer 2 apply (erule contE [rule_format])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   105
apply (erule bin_chain)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   106
apply (rule_tac y = "y" in arg_cong)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   107
apply (erule lub_bin_chain [THEN thelubI])
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   108
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   109
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   110
text {* right to left: @{prop "cont(f) ==> monofun(f) & contlub(f)"} *}
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   111
text {* part1: @{prop "cont(f) ==> monofun(f)"} *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   112
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   113
lemma cont2mono: "cont(f) ==> monofun(f)"
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   114
apply (rule monofunI [rule_format])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   115
apply (drule binchain_cont [THEN is_ub_lub])
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   116
apply (auto split add: split_if_asm)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   117
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   118
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   119
text {* right to left: @{prop "cont(f) ==> monofun(f) & contlub(f)"} *}
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   120
text {* part2: @{prop "cont(f) ==> contlub(f)"} *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   121
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   122
lemma cont2contlub: "cont(f) ==> contlub(f)"
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   123
apply (rule contlubI [rule_format])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   124
apply (rule thelubI [symmetric])
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   125
apply (erule contE [rule_format])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   126
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   127
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   128
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   129
text {* monotone functions map finite chains to finite chains *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   130
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   131
lemma monofun_finch2finch: 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   132
  "[| monofun f; finite_chain Y |] ==> finite_chain (%n. f (Y n))"
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   133
apply (unfold finite_chain_def)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   134
apply (force elim!: ch2ch_monofun simp add: max_in_chain_def)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   135
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   136
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   137
text {* The same holds for continuous functions *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   138
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   139
lemmas cont_finch2finch = cont2mono [THEN monofun_finch2finch, standard]
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   140
(* [| cont ?f; finite_chain ?Y |] ==> finite_chain (%n. ?f (?Y n)) *)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   141
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   142
text {*
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   143
  The following results are about a curried function that is monotone
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   144
  in both arguments
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   145
*}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   146
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   147
lemma ch2ch_MF2L: 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   148
"[|monofun(MF2); chain(F)|] ==> chain(%i. MF2 (F i) x)"
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   149
by (erule ch2ch_monofun [THEN ch2ch_fun])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   150
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   151
lemma ch2ch_MF2R: 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   152
"[|monofun(MF2(f)); chain(Y)|] ==> chain(%i. MF2 f (Y i))"
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   153
by (erule ch2ch_monofun)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   154
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   155
lemma ch2ch_MF2LR: 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   156
"[|monofun(MF2); !f. monofun(MF2(f)); chain(F); chain(Y)|] ==>  
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   157
   chain(%i. MF2(F(i))(Y(i)))"
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   158
apply (rule chainI)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   159
apply (rule trans_less)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   160
apply (erule ch2ch_MF2L [THEN chainE])
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   161
apply assumption
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   162
apply (rule monofunE [rule_format], erule spec)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   163
apply (erule chainE)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   164
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   165
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   166
lemma ch2ch_lubMF2R: 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   167
"[|monofun(MF2::('a::po=>'b::po=>'c::cpo)); 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   168
   !f. monofun(MF2(f)::('b::po=>'c::cpo)); 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   169
        chain(F);chain(Y)|] ==>  
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   170
        chain(%j. lub(range(%i. MF2 (F j) (Y i))))"
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   171
apply (rule lub_mono [THEN chainI])
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   172
apply (rule ch2ch_MF2R, erule spec)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   173
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   174
apply (rule ch2ch_MF2R, erule spec)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   175
apply assumption
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   176
apply (rule allI)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   177
apply (rule chainE)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   178
apply (erule ch2ch_MF2L)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   179
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   180
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   181
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   182
lemma ch2ch_lubMF2L: 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   183
"[|monofun(MF2::('a::po=>'b::po=>'c::cpo)); 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   184
   !f. monofun(MF2(f)::('b::po=>'c::cpo)); 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   185
        chain(F);chain(Y)|] ==>  
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   186
        chain(%i. lub(range(%j. MF2 (F j) (Y i))))"
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   187
apply (rule lub_mono [THEN chainI])
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   188
apply (erule ch2ch_MF2L)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   189
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   190
apply (erule ch2ch_MF2L)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   191
apply assumption
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   192
apply (rule allI)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   193
apply (rule chainE)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   194
apply (rule ch2ch_MF2R, erule spec)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   195
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   196
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   197
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   198
lemma lub_MF2_mono: 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   199
"[|monofun(MF2::('a::po=>'b::po=>'c::cpo)); 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   200
   !f. monofun(MF2(f)::('b::po=>'c::cpo)); 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   201
        chain(F)|] ==>  
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   202
        monofun(% x. lub(range(% j. MF2 (F j) (x))))"
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   203
apply (rule monofunI [rule_format])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   204
apply (rule lub_mono)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   205
apply (erule ch2ch_MF2L)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   206
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   207
apply (erule ch2ch_MF2L)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   208
apply assumption
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   209
apply (rule allI)
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   210
apply (rule monofunE [rule_format], erule spec)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   211
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   212
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   213
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   214
lemma ex_lubMF2: 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   215
"[|monofun(MF2::('a::po=>'b::po=>'c::cpo)); 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   216
   !f. monofun(MF2(f)::('b::po=>'c::cpo)); 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   217
        chain(F); chain(Y)|] ==>  
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   218
                lub(range(%j. lub(range(%i. MF2(F j) (Y i))))) = 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   219
                lub(range(%i. lub(range(%j. MF2(F j) (Y i)))))"
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   220
apply (rule antisym_less)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   221
apply (rule is_lub_thelub[OF _ ub_rangeI])
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   222
apply (erule ch2ch_lubMF2R)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   223
apply (assumption+)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   224
apply (rule lub_mono)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   225
apply (rule ch2ch_MF2R, erule spec)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   226
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   227
apply (erule ch2ch_lubMF2L)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   228
apply (assumption+)
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   229
apply (rule allI)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   230
apply (rule is_ub_thelub)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   231
apply (erule ch2ch_MF2L)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   232
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   233
apply (rule is_lub_thelub[OF _ ub_rangeI])
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   234
apply (erule ch2ch_lubMF2L)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   235
apply (assumption+)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   236
apply (rule lub_mono)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   237
apply (erule ch2ch_MF2L)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   238
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   239
apply (erule ch2ch_lubMF2R)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   240
apply (assumption+)
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   241
apply (rule allI)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   242
apply (rule is_ub_thelub)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   243
apply (rule ch2ch_MF2R, erule spec)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   244
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   245
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   246
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   247
lemma diag_lubMF2_1: 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   248
"[|monofun(MF2::('a::po=>'b::po=>'c::cpo)); 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   249
   !f. monofun(MF2(f)::('b::po=>'c::cpo)); 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   250
   chain(FY);chain(TY)|] ==> 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   251
  lub(range(%i. lub(range(%j. MF2(FY(j))(TY(i)))))) = 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   252
  lub(range(%i. MF2(FY(i))(TY(i))))"
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   253
apply (rule antisym_less)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   254
apply (rule is_lub_thelub[OF _ ub_rangeI])
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   255
apply (erule ch2ch_lubMF2L)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   256
apply (assumption+)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   257
apply (rule lub_mono3)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   258
apply (erule ch2ch_MF2L)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   259
apply (assumption+)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   260
apply (erule ch2ch_MF2LR)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   261
apply (assumption+)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   262
apply (rule allI)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   263
apply (rule_tac m = "i" and n = "ia" in nat_less_cases)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   264
apply (rule_tac x = "ia" in exI)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   265
apply (rule chain_mono)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   266
apply (erule allE)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   267
apply (erule ch2ch_MF2R)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   268
apply (assumption+)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   269
apply (erule ssubst)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   270
apply (rule_tac x = "ia" in exI)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   271
apply (rule refl_less)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   272
apply (rule_tac x = "i" in exI)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   273
apply (rule chain_mono)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   274
apply (erule ch2ch_MF2L)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   275
apply (assumption+)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   276
apply (rule lub_mono)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   277
apply (erule ch2ch_MF2LR)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   278
apply (assumption+)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   279
apply (erule ch2ch_lubMF2L)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   280
apply (assumption+)
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   281
apply (rule allI)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   282
apply (rule is_ub_thelub)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   283
apply (erule ch2ch_MF2L)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   284
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   285
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   286
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   287
lemma diag_lubMF2_2: 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   288
"[|monofun(MF2::('a::po=>'b::po=>'c::cpo)); 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   289
   !f. monofun(MF2(f)::('b::po=>'c::cpo)); 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   290
   chain(FY);chain(TY)|] ==> 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   291
  lub(range(%j. lub(range(%i. MF2(FY(j))(TY(i)))))) = 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   292
  lub(range(%i. MF2(FY(i))(TY(i))))"
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   293
apply (rule trans)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   294
apply (rule ex_lubMF2)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   295
apply (assumption+)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   296
apply (erule diag_lubMF2_1)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   297
apply (assumption+)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   298
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   299
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   300
text {*
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   301
  The following results are about a curried function that is continuous
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   302
  in both arguments
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   303
*}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   304
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   305
lemma contlub_CF2:
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   306
assumes prem1: "cont(CF2)"
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   307
assumes prem2: "!f. cont(CF2(f))"
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   308
assumes prem3: "chain(FY)"
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   309
assumes prem4: "chain(TY)"
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   310
shows "CF2(lub(range(FY)))(lub(range(TY))) = lub(range(%i. CF2(FY(i))(TY(i))))"
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   311
apply (subst prem1 [THEN cont2contlub, THEN contlubE, THEN spec, THEN mp])
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   312
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   313
apply (subst thelub_fun)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   314
apply (rule prem1 [THEN cont2mono [THEN ch2ch_monofun]])
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   315
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   316
apply (rule trans)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   317
apply (rule prem2 [THEN spec, THEN cont2contlub, THEN contlubE, THEN spec, THEN mp, THEN ext, THEN arg_cong, THEN arg_cong])
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   318
apply (rule prem4)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   319
apply (rule diag_lubMF2_2)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   320
apply (auto simp add: cont2mono prems)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   321
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   322
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   323
text {*
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   324
  The following results are about application for functions in @{typ "'a=>'b"}
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   325
*}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   326
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   327
lemma monofun_fun_fun: "f1 << f2 ==> f1(x) << f2(x)"
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   328
by (erule less_fun [THEN iffD1, THEN spec])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   329
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   330
lemma monofun_fun_arg: "[|monofun(f); x1 << x2|] ==> f(x1) << f(x2)"
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   331
by (erule monofunE [THEN spec, THEN spec, THEN mp])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   332
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   333
lemma monofun_fun: "[|monofun(f1); monofun(f2); f1 << f2; x1 << x2|] ==> f1(x1) << f2(x2)"
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   334
apply (rule trans_less)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   335
apply (erule monofun_fun_arg)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   336
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   337
apply (erule monofun_fun_fun)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   338
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   339
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   340
text {*
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   341
  The following results are about the propagation of monotonicity and
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   342
  continuity
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   343
*}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   344
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   345
lemma mono2mono_MF1L: "[|monofun(c1)|] ==> monofun(%x. c1 x y)"
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   346
apply (rule monofunI [rule_format])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   347
apply (erule monofun_fun_arg [THEN monofun_fun_fun])
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   348
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   349
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   350
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   351
lemma cont2cont_CF1L: "[|cont(c1)|] ==> cont(%x. c1 x y)"
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   352
apply (rule monocontlub2cont)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   353
apply (erule cont2mono [THEN mono2mono_MF1L])
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   354
apply (rule contlubI [rule_format])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   355
apply (frule asm_rl)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   356
apply (erule cont2contlub [THEN contlubE, THEN spec, THEN mp, THEN ssubst])
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   357
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   358
apply (subst thelub_fun)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   359
apply (rule ch2ch_monofun)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   360
apply (erule cont2mono)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   361
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   362
apply (rule refl)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   363
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   364
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   365
(*********  Note "(%x.%y.c1 x y) = c1" ***********)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   366
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   367
lemma mono2mono_MF1L_rev: "!y. monofun(%x. c1 x y) ==> monofun(c1)"
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   368
apply (rule monofunI [rule_format])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   369
apply (rule less_fun [THEN iffD2])
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   370
apply (blast dest: monofunE)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   371
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   372
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   373
lemma cont2cont_CF1L_rev: "!y. cont(%x. c1 x y) ==> cont(c1)"
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   374
apply (rule monocontlub2cont)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   375
apply (rule cont2mono [THEN allI, THEN mono2mono_MF1L_rev])
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   376
apply (erule spec)
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   377
apply (rule contlubI [rule_format])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   378
apply (rule ext)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   379
apply (subst thelub_fun)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   380
apply (rule cont2mono [THEN allI, THEN mono2mono_MF1L_rev, THEN ch2ch_monofun])
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   381
apply (erule spec)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   382
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   383
apply (blast dest: cont2contlub [THEN contlubE])
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   384
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   385
16053
603820cad083 moved theorem cont2cont_CF1L_rev2 to Cont.thy
huffman
parents: 15600
diff changeset
   386
lemma cont2cont_CF1L_rev2: "(!!y. cont (%x. c1 x y)) ==> cont c1"
603820cad083 moved theorem cont2cont_CF1L_rev2 to Cont.thy
huffman
parents: 15600
diff changeset
   387
apply (rule cont2cont_CF1L_rev)
603820cad083 moved theorem cont2cont_CF1L_rev2 to Cont.thy
huffman
parents: 15600
diff changeset
   388
apply simp
603820cad083 moved theorem cont2cont_CF1L_rev2 to Cont.thy
huffman
parents: 15600
diff changeset
   389
done
603820cad083 moved theorem cont2cont_CF1L_rev2 to Cont.thy
huffman
parents: 15600
diff changeset
   390
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   391
text {*
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   392
  What D.A.Schmidt calls continuity of abstraction
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   393
  never used here
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   394
*}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   395
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   396
lemma contlub_abstraction: 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   397
"[|chain(Y::nat=>'a);!y. cont(%x.(c::'a::cpo=>'b::cpo=>'c::cpo) x y)|] ==> 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   398
  (%y. lub(range(%i. c (Y i) y))) = (lub(range(%i.%y. c (Y i) y)))"
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   399
apply (rule trans)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   400
prefer 2 apply (rule cont2contlub [THEN contlubE, THEN spec, THEN mp])
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   401
prefer 2 apply (assumption)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   402
apply (erule cont2cont_CF1L_rev)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   403
apply (rule ext)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   404
apply (rule cont2contlub [THEN contlubE, THEN spec, THEN mp, symmetric])
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   405
apply (erule spec)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   406
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   407
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   408
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   409
lemma mono2mono_app: "[|monofun(ft);!x. monofun(ft(x));monofun(tt)|] ==> 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   410
         monofun(%x.(ft(x))(tt(x)))"
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   411
apply (rule monofunI [rule_format])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   412
apply (rule_tac ?f1.0 = "ft(x)" and ?f2.0 = "ft(y)" in monofun_fun)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   413
apply (erule spec)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   414
apply (erule spec)
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   415
apply (erule monofunE [rule_format])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   416
apply assumption
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   417
apply (erule monofunE [rule_format])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   418
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   419
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   420
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   421
lemma cont2contlub_app: "[|cont(ft);!x. cont(ft(x));cont(tt)|] ==> contlub(%x.(ft(x))(tt(x)))"
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   422
apply (rule contlubI [rule_format])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   423
apply (rule_tac f3 = "tt" in contlubE [THEN spec, THEN mp, THEN ssubst])
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   424
apply (erule cont2contlub)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   425
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   426
apply (rule contlub_CF2)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   427
apply (assumption+)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   428
apply (erule cont2mono [THEN ch2ch_monofun])
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   429
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   430
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   431
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   432
lemma cont2cont_app: "[|cont(ft); !x. cont(ft(x)); cont(tt)|] ==> cont(%x.(ft(x))(tt(x)))"
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   433
apply (blast intro: monocontlub2cont mono2mono_app cont2mono cont2contlub_app)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   434
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   435
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   436
lemmas cont2cont_app2 = cont2cont_app[OF _ allI]
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   437
(*  [| cont ?ft; !!x. cont (?ft x); cont ?tt |] ==> *)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   438
(*        cont (%x. ?ft x (?tt x))                    *)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   439
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   440
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   441
text {* The identity function is continuous *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   442
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   443
lemma cont_id: "cont(% x. x)"
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   444
apply (rule contI [rule_format])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   445
apply (erule thelubE)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   446
apply (rule refl)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   447
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   448
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   449
text {* constant functions are continuous *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   450
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   451
lemma cont_const: "cont(%x. c)"
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   452
apply (rule contI [rule_format])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   453
apply (blast intro: is_lubI ub_rangeI dest: ub_rangeD)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   454
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   455
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   456
lemma cont2cont_app3: "[|cont(f); cont(t) |] ==> cont(%x. f(t(x)))"
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   457
by (best intro: cont2cont_app2 cont_const)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   458
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   459
text {* A non-emptiness result for Cfun *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   460
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   461
lemma CfunI: "?x:Collect cont"
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   462
apply (rule CollectI)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   463
apply (rule cont_const)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   464
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   465
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   466
text {* some properties of flat *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   467
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   468
lemma flatdom2monofun: "f UU = UU ==> monofun (f::'a::flat=>'b::pcpo)"
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   469
apply (rule monofunI [rule_format])
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   470
apply (drule ax_flat [rule_format])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   471
apply auto
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   472
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   473
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   474
declare range_composition [simp del]
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   475
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   476
lemma chfindom_monofun2cont: "monofun f ==> cont(f::'a::chfin=>'b::pcpo)"
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   477
apply (rule monocontlub2cont)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   478
apply assumption
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   479
apply (rule contlubI [rule_format])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   480
apply (frule chfin2finch)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   481
apply (rule antisym_less)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   482
apply (clarsimp simp add: finite_chain_def maxinch_is_thelub)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   483
apply (rule is_ub_thelub)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   484
apply (erule ch2ch_monofun)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   485
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   486
apply (drule monofun_finch2finch[COMP swap_prems_rl])
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   487
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   488
apply (simp add: finite_chain_def)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   489
apply (erule conjE)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   490
apply (erule exE)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   491
apply (simp add: maxinch_is_thelub)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   492
apply (erule monofunE [THEN spec, THEN spec, THEN mp])
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   493
apply (erule is_ub_thelub)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   494
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   495
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   496
lemmas flatdom_strict2cont = flatdom2monofun [THEN chfindom_monofun2cont, standard]
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   497
(* f UU = UU ==> cont (f::'a=>'b::pcpo)" *)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   498
16096
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   499
text {* the lub of a chain of monotone functions is monotone. *}
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   500
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   501
lemma monofun_lub_fun:
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   502
  "\<lbrakk>chain (F::nat \<Rightarrow> 'a \<Rightarrow> 'b::cpo); \<forall>i. monofun (F i)\<rbrakk>
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   503
    \<Longrightarrow> monofun (\<Squnion>i. F i)"
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   504
apply (rule monofunI [rule_format])
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   505
apply (simp add: thelub_fun)
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   506
apply (rule lub_mono [rule_format])
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   507
apply (erule ch2ch_fun)
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   508
apply (erule ch2ch_fun)
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   509
apply (simp add: monofunE)
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   510
done
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   511
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   512
text {* the lub of a chain of continuous functions is continuous *}
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   513
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   514
lemma cont_lub_fun:
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   515
  "\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<Squnion>i. F i)"
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   516
 apply (rule contI [rule_format])
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   517
 apply (rule is_lubI)
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   518
  apply (rule ub_rangeI)
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   519
  apply (erule monofun_lub_fun [THEN monofunE [rule_format]])
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   520
   apply (simp add: cont2mono)
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   521
  apply (erule is_ub_thelub)
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   522
 apply (simp add: thelub_fun)
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   523
 apply (rule is_lub_thelub)
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   524
  apply (erule ch2ch_fun)
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   525
 apply (rule ub_rangeI)
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   526
 apply (drule_tac x=i in spec)
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   527
 apply (simp add: cont2contlub [THEN contlubE])
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   528
 apply (rule is_lub_thelub)
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   529
  apply (simp add: cont2mono [THEN ch2ch_monofun])
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   530
 apply (rule ub_rangeI)
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   531
 apply (rule trans_less)
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   532
  apply (erule ch2ch_fun [THEN is_ub_thelub])
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   533
 apply (erule ub_rangeD)
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   534
done
16e895296b2a added lemmas monofun_lub_fun and cont_lub_fun
huffman
parents: 16070
diff changeset
   535
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   536
end