src/HOLCF/Cont.thy
author huffman
Tue, 11 Oct 2005 23:19:50 +0200
changeset 17831 4a8c3f8b0a92
parent 16737 f0fd06dc93e3
child 18088 e5b23b85e932
permissions -rw-r--r--
cleaned up; renamed less_fun to expand_fun_less
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
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
    21
subsection {* Definitions *}
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    22
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
    23
constdefs
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
    24
  monofun :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"  -- "monotonicity"
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
    25
  "monofun f \<equiv> \<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    26
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
    27
  contlub :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool"  -- "first cont. def"
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
    28
  "contlub f \<equiv> \<forall>Y. chain Y \<longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    29
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
    30
  cont    :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool"  -- "secnd cont. def"
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
    31
  "cont f    \<equiv> \<forall>Y. chain Y \<longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)"
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    32
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    33
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
    34
  "\<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
    35
by (simp add: contlub_def)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    36
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    37
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
    38
  "\<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
    39
by (simp add: contlub_def)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    40
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
    41
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
    42
  "\<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
    43
by (simp add: cont_def)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    44
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
    45
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
    46
  "\<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
    47
by (simp add: cont_def)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    48
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    49
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
    50
  "\<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
    51
by (simp add: monofun_def)
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 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
    54
  "\<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
    55
by (simp add: monofun_def)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    56
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
    57
text {*
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
    58
  The following results are about application for functions in @{typ "'a=>'b"}
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
    59
*}
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
    60
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
    61
lemma monofun_fun_fun: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
    62
by (simp add: less_fun_def)
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
    63
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
    64
lemma monofun_fun_arg: "\<lbrakk>monofun f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y"
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
    65
by (rule monofunE)
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
    66
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
    67
lemma monofun_fun: "\<lbrakk>monofun f; monofun g; f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> g y"
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
    68
by (rule trans_less [OF monofun_fun_arg monofun_fun_fun])
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
    69
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
    70
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
    71
subsection {* @{prop "monofun f \<and> contlub f \<equiv> cont f"} *}
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
    72
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    73
text {* monotone functions map chains to chains *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    74
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
    75
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
    76
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
    77
apply (erule monofunE)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    78
apply (erule chainE)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    79
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    80
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    81
text {* monotone functions map upper bound to upper bounds *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    82
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    83
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
    84
  "\<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
    85
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
    86
apply (erule monofunE)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    87
apply (erule ub_rangeD)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    88
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    89
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
    90
text {* left to right: @{prop "monofun f \<and> contlub f \<Longrightarrow> cont f"} *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    91
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
    92
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
    93
apply (rule contI)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    94
apply (rule thelubE)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    95
apply (erule ch2ch_monofun)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    96
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
    97
apply (erule contlubE [symmetric])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    98
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    99
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   100
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   101
text {* first a lemma about binary chains *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   102
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
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
   104
  "\<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
   105
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
   106
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
   107
apply (erule contE)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   108
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
   109
apply (rule_tac f=f in arg_cong)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   110
apply (erule lub_bin_chain [THEN thelubI])
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   111
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   112
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
   113
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
   114
text {* part1: @{prop "cont f \<Longrightarrow> monofun f"} *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   115
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
   116
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
   117
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
   118
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
   119
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
   120
apply simp
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   121
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   122
16737
f0fd06dc93e3 add lemmas ch2ch_cont and cont2contlubE
huffman
parents: 16624
diff changeset
   123
lemmas ch2ch_cont = cont2mono [THEN ch2ch_monofun]
f0fd06dc93e3 add lemmas ch2ch_cont and cont2contlubE
huffman
parents: 16624
diff changeset
   124
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
   125
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
   126
text {* part2: @{prop "cont f \<Longrightarrow> contlub f"} *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   127
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   128
lemma cont2contlub: "cont f \<Longrightarrow> 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
   129
apply (rule contlubI)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   130
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
   131
apply (erule contE)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   132
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   133
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   134
16737
f0fd06dc93e3 add lemmas ch2ch_cont and cont2contlubE
huffman
parents: 16624
diff changeset
   135
lemmas cont2contlubE = cont2contlub [THEN contlubE]
f0fd06dc93e3 add lemmas ch2ch_cont and cont2contlubE
huffman
parents: 16624
diff changeset
   136
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   137
subsection {* Continuity of basic functions *}
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   138
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   139
text {* The identity function is continuous *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   140
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   141
lemma cont_id: "cont (\<lambda>x. x)"
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   142
apply (rule contI)
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   143
apply (erule thelubE)
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   144
apply (rule refl)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   145
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   146
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   147
text {* constant functions are continuous *}
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   148
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   149
lemma cont_const: "cont (\<lambda>x. c)"
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   150
apply (rule contI)
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   151
apply (rule lub_const)
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   152
done
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   153
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   154
text {* if-then-else is continuous *}
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   155
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   156
lemma cont_if: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. if b then f x else g x)"
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   157
by (induct b) simp_all
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   158
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   159
subsection {* Propagation of monotonicity and continuity *}
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   160
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   161
text {* the lub of a chain of monotone functions is monotone *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   162
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
   163
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
   164
  "\<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
   165
    \<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
   166
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
   167
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
   168
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
   169
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
   170
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
   171
apply (simp add: monofunE)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   172
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   173
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
   174
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
   175
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
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
   177
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
   178
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
   179
  "\<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
   180
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
   181
apply (simp add: thelub_fun)
16737
f0fd06dc93e3 add lemmas ch2ch_cont and cont2contlubE
huffman
parents: 16624
diff changeset
   182
apply (simp add: cont2contlubE)
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
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
   184
apply (erule ch2ch_fun)
16737
f0fd06dc93e3 add lemmas ch2ch_cont and cont2contlubE
huffman
parents: 16624
diff changeset
   185
apply (simp add: ch2ch_cont)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   186
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   187
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
   188
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
   189
  "\<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
   190
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
   191
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
   192
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
   193
apply (erule contlub_lub_fun)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   194
apply assumption
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   195
done
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 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
   198
  "\<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
   199
by (simp add: thelub_fun [symmetric] cont_lub_fun)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   200
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
   201
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
   202
apply (rule monofunI)
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   203
apply (erule (1) monofun_fun_arg [THEN monofun_fun_fun])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   204
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   205
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
lemma cont2cont_CF1L: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)"
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   207
apply (rule monocontlub2cont)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   208
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
   209
apply (rule contlubI)
16737
f0fd06dc93e3 add lemmas ch2ch_cont and cont2contlubE
huffman
parents: 16624
diff changeset
   210
apply (simp add: cont2contlubE)
f0fd06dc93e3 add lemmas ch2ch_cont and cont2contlubE
huffman
parents: 16624
diff changeset
   211
apply (simp add: thelub_fun ch2ch_cont)
15565
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
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   214
text {* Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"} *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   215
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
   216
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
   217
apply (rule monofunI)
17831
4a8c3f8b0a92 cleaned up; renamed less_fun to expand_fun_less
huffman
parents: 16737
diff changeset
   218
apply (rule less_fun_ext)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   219
apply (blast dest: monofunE)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   220
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   221
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
   222
lemma cont2cont_CF1L_rev: "\<forall>y. cont (\<lambda>x. f x y) \<Longrightarrow> cont f"
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   223
apply (subgoal_tac "monofun f")
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   224
apply (rule monocontlub2cont)
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   225
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
   226
apply (rule contlubI)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   227
apply (rule ext)
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   228
apply (simp add: thelub_fun ch2ch_monofun)
16737
f0fd06dc93e3 add lemmas ch2ch_cont and cont2contlubE
huffman
parents: 16624
diff changeset
   229
apply (blast dest: cont2contlubE)
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   230
apply (simp add: mono2mono_MF1L_rev cont2mono)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   231
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   232
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   233
lemma cont2cont_lambda: "(\<And>y. cont (\<lambda>x. f x y)) \<Longrightarrow> cont (\<lambda>x. (\<lambda>y. f x y))"
16053
603820cad083 moved theorem cont2cont_CF1L_rev2 to Cont.thy
huffman
parents: 15600
diff changeset
   234
apply (rule cont2cont_CF1L_rev)
603820cad083 moved theorem cont2cont_CF1L_rev2 to Cont.thy
huffman
parents: 15600
diff changeset
   235
apply simp
603820cad083 moved theorem cont2cont_CF1L_rev2 to Cont.thy
huffman
parents: 15600
diff changeset
   236
done
603820cad083 moved theorem cont2cont_CF1L_rev2 to Cont.thy
huffman
parents: 15600
diff changeset
   237
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   238
text {* What D.A.Schmidt calls continuity of abstraction; never used here *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   239
16564
6fc73c9dd5f4 cleaned up proof of contlub_abstraction
huffman
parents: 16388
diff changeset
   240
lemma contlub_abstraction:
6fc73c9dd5f4 cleaned up proof of contlub_abstraction
huffman
parents: 16388
diff changeset
   241
  "\<lbrakk>chain Y; \<forall>y. cont (\<lambda>x.(c::'a::cpo\<Rightarrow>'b::type\<Rightarrow>'c::cpo) x y)\<rbrakk> \<Longrightarrow>
6fc73c9dd5f4 cleaned up proof of contlub_abstraction
huffman
parents: 16388
diff changeset
   242
    (\<lambda>y. \<Squnion>i. c (Y i) y) = (\<Squnion>i. (\<lambda>y. c (Y i) y))"
6fc73c9dd5f4 cleaned up proof of contlub_abstraction
huffman
parents: 16388
diff changeset
   243
apply (rule thelub_fun [symmetric])
16737
f0fd06dc93e3 add lemmas ch2ch_cont and cont2contlubE
huffman
parents: 16624
diff changeset
   244
apply (rule ch2ch_cont)
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   245
apply (erule (1) cont2cont_CF1L_rev)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   246
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   247
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
   248
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
   249
  "\<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
   250
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
   251
apply (simp add: monofun_fun monofunE)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   252
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   253
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
   254
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
   255
  "\<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
   256
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
   257
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
   258
apply (subgoal_tac "chain (\<lambda>i. t (Y i))")
16737
f0fd06dc93e3 add lemmas ch2ch_cont and cont2contlubE
huffman
parents: 16624
diff changeset
   259
apply (simp add: cont2contlubE thelub_fun)
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
   260
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
   261
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
   262
apply (drule spec)
16737
f0fd06dc93e3 add lemmas ch2ch_cont and cont2contlubE
huffman
parents: 16624
diff changeset
   263
apply (erule (1) ch2ch_cont)
f0fd06dc93e3 add lemmas ch2ch_cont and cont2contlubE
huffman
parents: 16624
diff changeset
   264
apply (erule (1) ch2ch_cont)
f0fd06dc93e3 add lemmas ch2ch_cont and cont2contlubE
huffman
parents: 16624
diff changeset
   265
apply (erule (1) ch2ch_cont)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   266
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   267
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
   268
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
   269
  "\<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
   270
by (blast intro: monocontlub2cont mono2mono_app cont2mono cont2contlub_app)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   271
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   272
lemmas cont2cont_app2 = cont2cont_app [rule_format]
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   273
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   274
lemma cont2cont_app3: "\<lbrakk>cont f; cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. f (t x))"
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   275
by (rule cont2cont_app2 [OF cont_const])
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   276
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   277
subsection {* Finite chains and flat pcpos *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   278
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   279
text {* monotone functions map finite chains to finite chains *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   280
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   281
lemma monofun_finch2finch:
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   282
  "\<lbrakk>monofun f; finite_chain Y\<rbrakk> \<Longrightarrow> finite_chain (\<lambda>n. f (Y n))"
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   283
apply (unfold finite_chain_def)
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   284
apply (simp add: ch2ch_monofun)
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   285
apply (force simp add: max_in_chain_def)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   286
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   287
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   288
text {* The same holds for continuous functions *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   289
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   290
lemma cont_finch2finch:
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   291
  "\<lbrakk>cont f; finite_chain Y\<rbrakk> \<Longrightarrow> finite_chain (\<lambda>n. f (Y n))"
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   292
by (rule cont2mono [THEN monofun_finch2finch])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   293
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
   294
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
   295
apply (rule monocontlub2cont)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   296
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
   297
apply (rule contlubI)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   298
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
   299
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
   300
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
   301
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
   302
apply (force simp add: max_in_chain_def)
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
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   305
text {* some properties of flat *}
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   306
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   307
lemma flatdom_strict2mono: "f \<bottom> = \<bottom> \<Longrightarrow> monofun (f::'a::flat \<Rightarrow> 'b::pcpo)"
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   308
apply (rule monofunI)
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   309
apply (drule ax_flat [rule_format])
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   310
apply auto
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   311
done
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   312
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   313
lemma flatdom_strict2cont: "f \<bottom> = \<bottom> \<Longrightarrow> cont (f::'a::flat \<Rightarrow> 'b::pcpo)"
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   314
by (rule flatdom_strict2mono [THEN chfindom_monofun2cont])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   315
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   316
end