src/HOLCF/Cont.thy
author huffman
Sat, 04 Jun 2005 00:22:08 +0200
changeset 16221 879400e029bf
parent 16204 5dd79d3f0105
child 16388 1ff571813848
permissions -rw-r--r--
New theory with lemmas for the fixrec package
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
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
    11
imports Ffun
15577
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
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
    28
monofun_def:         "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
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
    30
contlub_def:         "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
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
    33
cont_def:            "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:
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
    44
  "\<lbrakk>\<And>Y. chain Y \<Longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i))\<rbrakk> \<Longrightarrow> contlub f"
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
    45
by (simp add: contlub_def)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    46
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    47
lemma contlubE: 
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
    48
  "\<lbrakk>contlub f; chain Y\<rbrakk> \<Longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i))" 
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
    49
by (simp add: contlub_def)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    50
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
    51
lemma contI:
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
    52
  "\<lbrakk>\<And>Y. chain Y \<Longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> cont f"
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
    53
by (simp add: cont_def)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    54
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
    55
lemma contE:
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
    56
  "\<lbrakk>cont f; chain Y\<rbrakk> \<Longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)"
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
    57
by (simp add: cont_def)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    58
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    59
lemma monofunI: 
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
    60
  "\<lbrakk>\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y\<rbrakk> \<Longrightarrow> monofun f"
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
    61
by (simp add: monofun_def)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    62
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    63
lemma monofunE: 
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
    64
  "\<lbrakk>monofun f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y"
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
    65
by (simp add: monofun_def)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    66
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    67
text {* monotone functions map chains to chains *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    68
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
    69
lemma ch2ch_monofun: "\<lbrakk>monofun f; chain Y\<rbrakk> \<Longrightarrow> chain (\<lambda>i. f (Y i))"
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    70
apply (rule chainI)
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
    71
apply (erule monofunE)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    72
apply (erule chainE)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    73
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    74
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    75
text {* monotone functions map upper bound to upper bounds *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    76
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    77
lemma ub2ub_monofun: 
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
    78
  "\<lbrakk>monofun f; range Y <| u\<rbrakk> \<Longrightarrow> range (\<lambda>i. f (Y i)) <| f u"
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    79
apply (rule ub_rangeI)
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
    80
apply (erule monofunE)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    81
apply (erule ub_rangeD)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    82
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    83
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    84
text {* left to right: @{prop "monofun(f) & contlub(f) ==> cont(f)"} *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    85
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
    86
lemma monocontlub2cont: "\<lbrakk>monofun f; contlub f\<rbrakk> \<Longrightarrow> cont f"
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
    87
apply (rule contI)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    88
apply (rule thelubE)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    89
apply (erule ch2ch_monofun)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    90
apply assumption
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
    91
apply (erule contlubE [symmetric])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    92
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    93
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    94
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    95
text {* first a lemma about binary chains *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    96
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
    97
lemma binchain_cont:
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
    98
  "\<lbrakk>cont f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> range (\<lambda>i::nat. f (if i = 0 then x else y)) <<| f y"
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
    99
apply (subgoal_tac "f (\<Squnion>i::nat. if i = 0 then x else y) = f y")
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   100
apply (erule subst)
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   101
apply (erule contE)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   102
apply (erule bin_chain)
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   103
apply (rule_tac f=f in arg_cong)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   104
apply (erule lub_bin_chain [THEN thelubI])
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   105
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   106
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   107
text {* right to left: @{prop "cont f \<Longrightarrow> monofun f \<and> contlub f"} *}
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   108
text {* part1: @{prop "cont f \<Longrightarrow> monofun f"} *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   109
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   110
lemma cont2mono: "cont f \<Longrightarrow> monofun f"
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   111
apply (rule monofunI)
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   112
apply (drule binchain_cont, assumption)
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   113
apply (drule_tac i=0 in is_ub_lub)
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   114
apply simp
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   115
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   116
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   117
text {* right to left: @{prop "cont f \<Longrightarrow> monofun f \<and> contlub f"} *}
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   118
text {* part2: @{prop "cont f \<Longrightarrow> contlub f"} *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   119
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   120
lemma cont2contlub: "cont(f) ==> contlub(f)"
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   121
apply (rule contlubI)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   122
apply (rule thelubI [symmetric])
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   123
apply (erule contE)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   124
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   125
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   126
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   127
text {* monotone functions map finite chains to finite chains *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   128
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   129
lemma monofun_finch2finch:
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   130
  "\<lbrakk>monofun f; finite_chain Y\<rbrakk> \<Longrightarrow> finite_chain (\<lambda>n. f (Y n))"
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   131
apply (unfold finite_chain_def)
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   132
apply (simp add: ch2ch_monofun)
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   133
apply (force simp add: max_in_chain_def)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   134
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   135
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   136
text {* The same holds for continuous functions *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   137
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   138
lemmas cont_finch2finch = cont2mono [THEN monofun_finch2finch, standard]
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   139
(* [| cont ?f; finite_chain ?Y |] ==> finite_chain (%n. ?f (?Y n)) *)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   140
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   141
lemma monofun_lub_fun:
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   142
  "\<lbrakk>chain (F::nat \<Rightarrow> 'a \<Rightarrow> 'b::cpo); \<forall>i. monofun (F i)\<rbrakk>
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   143
    \<Longrightarrow> monofun (\<Squnion>i. F i)"
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   144
apply (rule monofunI)
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   145
apply (simp add: thelub_fun)
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   146
apply (rule lub_mono [rule_format])
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   147
apply (erule ch2ch_fun)
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   148
apply (erule ch2ch_fun)
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   149
apply (simp add: monofunE)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   150
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   151
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   152
text {* the lub of a chain of continuous functions is continuous *}
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   153
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   154
declare range_composition [simp del]
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   155
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   156
lemma contlub_lub_fun:
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   157
  "\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> contlub (\<Squnion>i. F i)"
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   158
apply (rule contlubI)
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   159
apply (simp add: thelub_fun)
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   160
apply (simp add: cont2contlub [THEN contlubE])
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   161
apply (rule ex_lub)
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   162
apply (erule ch2ch_fun)
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   163
apply (simp add: cont2mono [THEN ch2ch_monofun])
15565
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
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   166
lemma cont_lub_fun:
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   167
  "\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<Squnion>i. F i)"
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   168
apply (rule monocontlub2cont)
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   169
apply (erule monofun_lub_fun)
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   170
apply (simp add: cont2mono)
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   171
apply (erule contlub_lub_fun)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   172
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   173
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   174
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   175
lemma cont2cont_lub:
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   176
  "\<lbrakk>chain F; \<And>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. \<Squnion>i. F i x)"
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   177
by (simp add: thelub_fun [symmetric] cont_lub_fun)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   178
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   179
text {*
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   180
  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
   181
*}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   182
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   183
lemma monofun_fun_fun: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   184
by (simp add: less_fun_def)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   185
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   186
lemma monofun_fun_arg: "\<lbrakk>monofun f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y"
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   187
by (rule monofunE)
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   188
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   189
lemma monofun_fun: "\<lbrakk>monofun f; monofun g; f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> g y"
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   190
by (rule trans_less [OF monofun_fun_arg monofun_fun_fun])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   191
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   192
text {*
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   193
  The following results are about the propagation of monotonicity and
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   194
  continuity
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   195
*}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   196
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   197
lemma mono2mono_MF1L: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)"
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   198
apply (rule monofunI)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   199
apply (erule monofun_fun_arg [THEN monofun_fun_fun])
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   200
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   201
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   202
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   203
lemma cont2cont_CF1L: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)"
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   204
apply (rule monocontlub2cont)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   205
apply (erule cont2mono [THEN mono2mono_MF1L])
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   206
apply (rule contlubI)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   207
apply (frule asm_rl)
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   208
apply (erule cont2contlub [THEN contlubE, THEN ssubst])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   209
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   210
apply (subst thelub_fun)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   211
apply (rule ch2ch_monofun)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   212
apply (erule cont2mono)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   213
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   214
apply (rule refl)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   215
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   216
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   217
(*********  Note "(%x.%y.c1 x y) = c1" ***********)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   218
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   219
lemma mono2mono_MF1L_rev: "\<forall>y. monofun (\<lambda>x. f x y) \<Longrightarrow> monofun f"
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   220
apply (rule monofunI)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   221
apply (rule less_fun [THEN iffD2])
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   222
apply (blast dest: monofunE)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   223
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   224
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   225
lemma cont2cont_CF1L_rev: "\<forall>y. cont (\<lambda>x. f x y) \<Longrightarrow> cont f"
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   226
apply (rule monocontlub2cont)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   227
apply (rule cont2mono [THEN allI, THEN mono2mono_MF1L_rev])
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   228
apply (erule spec)
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   229
apply (rule contlubI)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   230
apply (rule ext)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   231
apply (subst thelub_fun)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   232
apply (rule cont2mono [THEN allI, THEN mono2mono_MF1L_rev, THEN ch2ch_monofun])
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   233
apply (erule spec)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   234
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   235
apply (blast dest: cont2contlub [THEN contlubE])
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   236
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   237
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   238
lemma cont2cont_CF1L_rev2: "(\<And>y. cont (\<lambda>x. f x y)) \<Longrightarrow> cont f"
16053
603820cad083 moved theorem cont2cont_CF1L_rev2 to Cont.thy
huffman
parents: 15600
diff changeset
   239
apply (rule cont2cont_CF1L_rev)
603820cad083 moved theorem cont2cont_CF1L_rev2 to Cont.thy
huffman
parents: 15600
diff changeset
   240
apply simp
603820cad083 moved theorem cont2cont_CF1L_rev2 to Cont.thy
huffman
parents: 15600
diff changeset
   241
done
603820cad083 moved theorem cont2cont_CF1L_rev2 to Cont.thy
huffman
parents: 15600
diff changeset
   242
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   243
text {*
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   244
  What D.A.Schmidt calls continuity of abstraction
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   245
  never used here
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   246
*}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   247
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   248
lemma contlub_abstraction: 
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   249
"[|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
   250
  (%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
   251
apply (rule trans)
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   252
prefer 2 apply (rule cont2contlub [THEN contlubE])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   253
prefer 2 apply (assumption)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   254
apply (erule cont2cont_CF1L_rev)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   255
apply (rule ext)
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   256
apply (rule cont2contlub [THEN contlubE, symmetric])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   257
apply (erule spec)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   258
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   259
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   260
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   261
lemma mono2mono_app:
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   262
  "\<lbrakk>monofun f; \<forall>x. monofun (f x); monofun t\<rbrakk> \<Longrightarrow> monofun (\<lambda>x. (f x) (t x))"
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   263
apply (rule monofunI)
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   264
apply (simp add: monofun_fun monofunE)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   265
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   266
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   267
lemma cont2contlub_app:
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   268
  "\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> contlub (\<lambda>x. (f x) (t x))"
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   269
apply (rule contlubI)
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   270
apply (subgoal_tac "chain (\<lambda>i. f (Y i))")
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   271
apply (subgoal_tac "chain (\<lambda>i. t (Y i))")
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   272
apply (simp add: cont2contlub [THEN contlubE] thelub_fun)
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   273
apply (rule diag_lub)
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   274
apply (erule ch2ch_fun)
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   275
apply (drule spec)
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   276
apply (erule cont2mono [THEN ch2ch_monofun], assumption)
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   277
apply (erule cont2mono [THEN ch2ch_monofun], assumption)
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   278
apply (erule cont2mono [THEN ch2ch_monofun], assumption)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   279
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   280
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   281
lemma cont2cont_app:
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   282
  "\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. (f x) (t x))"
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   283
by (blast intro: monocontlub2cont mono2mono_app cont2mono cont2contlub_app)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   284
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   285
lemmas cont2cont_app2 = cont2cont_app[OF _ allI]
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   286
(*  [| cont ?ft; !!x. cont (?ft x); cont ?tt |] ==> *)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   287
(*        cont (%x. ?ft x (?tt x))                    *)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   288
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   289
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   290
text {* The identity function is continuous *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   291
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   292
lemma cont_id: "cont (\<lambda>x. x)"
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   293
apply (rule contI)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   294
apply (erule thelubE)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   295
apply (rule refl)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   296
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   297
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   298
text {* constant functions are continuous *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   299
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   300
lemma cont_const: "cont (\<lambda>x. c)"
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   301
apply (rule contI)
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   302
apply (rule lub_const)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   303
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   304
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   305
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
   306
by (best intro: cont2cont_app2 cont_const)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   307
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   308
text {* some properties of flat *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   309
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   310
lemma flatdom2monofun: "f \<bottom> = \<bottom> \<Longrightarrow> monofun (f::'a::flat \<Rightarrow> 'b::pcpo)"
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   311
apply (rule monofunI)
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   312
apply (drule ax_flat [rule_format])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   313
apply auto
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   314
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   315
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   316
lemma chfindom_monofun2cont: "monofun f \<Longrightarrow> cont (f::'a::chfin \<Rightarrow> 'b::pcpo)"
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   317
apply (rule monocontlub2cont)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   318
apply assumption
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   319
apply (rule contlubI)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   320
apply (frule chfin2finch)
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   321
apply (clarsimp simp add: finite_chain_def)
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   322
apply (subgoal_tac "max_in_chain i (\<lambda>i. f (Y i))")
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   323
apply (simp add: maxinch_is_thelub ch2ch_monofun)
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 16096
diff changeset
   324
apply (force simp add: max_in_chain_def)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   325
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   326
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   327
lemmas flatdom_strict2cont = flatdom2monofun [THEN chfindom_monofun2cont, standard]
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   328
(* f UU = UU ==> cont (f::'a=>'b::pcpo)" *)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   329
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   330
end