src/HOL/HOLCF/Cont.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45294 3c5d3d286055
child 57945 cacb00a569e0
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42151
4da4fc77664b tuned headers;
wenzelm
parents: 40774
diff changeset
     1
(*  Title:      HOL/HOLCF/Cont.thy
1479
21eb5e156d91 expanded tabs
clasohm
parents: 1274
diff changeset
     2
    Author:     Franz Regensburger
35794
8cd7134275cc use headers consistently
huffman
parents: 31902
diff changeset
     3
    Author:     Brian Huffman
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     4
*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     5
15577
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
     6
header {* Continuity and monotonicity *}
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
     7
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
     8
theory Cont
25786
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25783
diff changeset
     9
imports Pcpo
15577
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
    10
begin
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    11
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    12
text {*
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    13
   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
    14
   of default class po
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    15
*}
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    16
36452
d37c6eed8117 renamed command 'defaultsort' to 'default_sort';
wenzelm
parents: 35914
diff changeset
    17
default_sort po
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    18
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
    19
subsection {* Definitions *}
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    20
25131
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 18092
diff changeset
    21
definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 18092
diff changeset
    22
  monofun :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"  -- "monotonicity"  where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 18092
diff changeset
    23
  "monofun f = (\<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
    24
25131
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 18092
diff changeset
    25
definition
35914
91a7311177c4 remove contlub predicate
huffman
parents: 35900
diff changeset
    26
  cont :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool"
91a7311177c4 remove contlub predicate
huffman
parents: 35900
diff changeset
    27
where
25131
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 18092
diff changeset
    28
  "cont f = (\<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
    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
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
    31
  "\<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
    32
by (simp add: cont_def)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    33
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
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
    35
  "\<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
    36
by (simp add: cont_def)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    37
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    38
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
    39
  "\<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
    40
by (simp add: monofun_def)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    41
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    42
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
    43
  "\<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
    44
by (simp add: monofun_def)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    45
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
    46
35900
aa5dfb03eb1e remove LaTeX hyperref warnings by avoiding antiquotations within section headings
huffman
parents: 35794
diff changeset
    47
subsection {* Equivalence of alternate definition *}
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
    48
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    49
text {* monotone functions map chains to chains *}
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 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
    52
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
    53
apply (erule monofunE)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    54
apply (erule chainE)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    55
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    56
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    57
text {* monotone functions map upper bound to upper bounds *}
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 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
    60
  "\<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
    61
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
    62
apply (erule monofunE)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    63
apply (erule ub_rangeD)
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    64
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    65
35914
91a7311177c4 remove contlub predicate
huffman
parents: 35900
diff changeset
    66
text {* a lemma about binary chains *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    67
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
    68
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
    69
  "\<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
    70
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
    71
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
    72
apply (erule contE)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    73
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
    74
apply (rule_tac f=f in arg_cong)
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40736
diff changeset
    75
apply (erule is_lub_bin_chain [THEN lub_eqI])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    76
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    77
35914
91a7311177c4 remove contlub predicate
huffman
parents: 35900
diff changeset
    78
text {* continuity implies monotonicity *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    79
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
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
    81
apply (rule monofunI)
18088
e5b23b85e932 cleaned up
huffman
parents: 17831
diff changeset
    82
apply (drule (1) binchain_cont)
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40736
diff changeset
    83
apply (drule_tac i=0 in is_lub_rangeD1)
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
apply simp
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    85
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    86
29532
59bee7985149 add lemmas cont2monofunE, cont2cont_apply
huffman
parents: 29530
diff changeset
    87
lemmas cont2monofunE = cont2mono [THEN monofunE]
59bee7985149 add lemmas cont2monofunE, cont2cont_apply
huffman
parents: 29530
diff changeset
    88
16737
f0fd06dc93e3 add lemmas ch2ch_cont and cont2contlubE
huffman
parents: 16624
diff changeset
    89
lemmas ch2ch_cont = cont2mono [THEN ch2ch_monofun]
f0fd06dc93e3 add lemmas ch2ch_cont and cont2contlubE
huffman
parents: 16624
diff changeset
    90
35914
91a7311177c4 remove contlub predicate
huffman
parents: 35900
diff changeset
    91
text {* continuity implies preservation of lubs *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    92
35914
91a7311177c4 remove contlub predicate
huffman
parents: 35900
diff changeset
    93
lemma cont2contlubE:
91a7311177c4 remove contlub predicate
huffman
parents: 35900
diff changeset
    94
  "\<lbrakk>cont f; chain Y\<rbrakk> \<Longrightarrow> f (\<Squnion> i. Y i) = (\<Squnion> i. f (Y i))"
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40736
diff changeset
    95
apply (rule lub_eqI [symmetric])
18088
e5b23b85e932 cleaned up
huffman
parents: 17831
diff changeset
    96
apply (erule (1) contE)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    97
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    98
25896
b2d2f1ae5808 add lemma contI2
huffman
parents: 25825
diff changeset
    99
lemma contI2:
40736
72857de90621 isar-style proof for lemma contI2
huffman
parents: 40010
diff changeset
   100
  fixes f :: "'a::cpo \<Rightarrow> 'b::cpo"
25896
b2d2f1ae5808 add lemma contI2
huffman
parents: 25825
diff changeset
   101
  assumes mono: "monofun f"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31041
diff changeset
   102
  assumes below: "\<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. f (Y i))\<rbrakk>
27413
3154f3765cc7 replace lub (range Y) with (LUB i. Y i)
huffman
parents: 26452
diff changeset
   103
     \<Longrightarrow> f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. f (Y i))"
25896
b2d2f1ae5808 add lemma contI2
huffman
parents: 25825
diff changeset
   104
  shows "cont f"
40736
72857de90621 isar-style proof for lemma contI2
huffman
parents: 40010
diff changeset
   105
proof (rule contI)
72857de90621 isar-style proof for lemma contI2
huffman
parents: 40010
diff changeset
   106
  fix Y :: "nat \<Rightarrow> 'a"
72857de90621 isar-style proof for lemma contI2
huffman
parents: 40010
diff changeset
   107
  assume Y: "chain Y"
72857de90621 isar-style proof for lemma contI2
huffman
parents: 40010
diff changeset
   108
  with mono have fY: "chain (\<lambda>i. f (Y i))"
72857de90621 isar-style proof for lemma contI2
huffman
parents: 40010
diff changeset
   109
    by (rule ch2ch_monofun)
72857de90621 isar-style proof for lemma contI2
huffman
parents: 40010
diff changeset
   110
  have "(\<Squnion>i. f (Y i)) = f (\<Squnion>i. Y i)"
72857de90621 isar-style proof for lemma contI2
huffman
parents: 40010
diff changeset
   111
    apply (rule below_antisym)
72857de90621 isar-style proof for lemma contI2
huffman
parents: 40010
diff changeset
   112
    apply (rule lub_below [OF fY])
72857de90621 isar-style proof for lemma contI2
huffman
parents: 40010
diff changeset
   113
    apply (rule monofunE [OF mono])
72857de90621 isar-style proof for lemma contI2
huffman
parents: 40010
diff changeset
   114
    apply (rule is_ub_thelub [OF Y])
72857de90621 isar-style proof for lemma contI2
huffman
parents: 40010
diff changeset
   115
    apply (rule below [OF Y fY])
72857de90621 isar-style proof for lemma contI2
huffman
parents: 40010
diff changeset
   116
    done
72857de90621 isar-style proof for lemma contI2
huffman
parents: 40010
diff changeset
   117
  with fY show "range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)"
72857de90621 isar-style proof for lemma contI2
huffman
parents: 40010
diff changeset
   118
    by (rule thelubE)
72857de90621 isar-style proof for lemma contI2
huffman
parents: 40010
diff changeset
   119
qed
25896
b2d2f1ae5808 add lemma contI2
huffman
parents: 25825
diff changeset
   120
37079
0cd15d8c90a0 remove cont2cont simproc; instead declare cont2cont rules as simp rules
huffman
parents: 36658
diff changeset
   121
subsection {* Collection of continuity rules *}
29530
9905b660612b change to simpler, more extensible continuity simproc
huffman
parents: 29138
diff changeset
   122
9905b660612b change to simpler, more extensible continuity simproc
huffman
parents: 29138
diff changeset
   123
ML {*
31902
862ae16a799d renamed NamedThmsFun to Named_Thms;
wenzelm
parents: 31076
diff changeset
   124
structure Cont2ContData = Named_Thms
862ae16a799d renamed NamedThmsFun to Named_Thms;
wenzelm
parents: 31076
diff changeset
   125
(
45294
3c5d3d286055 tuned Named_Thms: proper binding;
wenzelm
parents: 42151
diff changeset
   126
  val name = @{binding cont2cont}
31902
862ae16a799d renamed NamedThmsFun to Named_Thms;
wenzelm
parents: 31076
diff changeset
   127
  val description = "continuity intro rule"
862ae16a799d renamed NamedThmsFun to Named_Thms;
wenzelm
parents: 31076
diff changeset
   128
)
29530
9905b660612b change to simpler, more extensible continuity simproc
huffman
parents: 29138
diff changeset
   129
*}
9905b660612b change to simpler, more extensible continuity simproc
huffman
parents: 29138
diff changeset
   130
31030
5ee6368d622b use simproc_setup command for cont_proc
huffman
parents: 29541
diff changeset
   131
setup Cont2ContData.setup
29530
9905b660612b change to simpler, more extensible continuity simproc
huffman
parents: 29138
diff changeset
   132
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   133
subsection {* Continuity of basic functions *}
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   134
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   135
text {* The identity function is continuous *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   136
37079
0cd15d8c90a0 remove cont2cont simproc; instead declare cont2cont rules as simp rules
huffman
parents: 36658
diff changeset
   137
lemma cont_id [simp, cont2cont]: "cont (\<lambda>x. x)"
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   138
apply (rule contI)
26027
87cb69d27558 add lemma cpo_lubI
huffman
parents: 26024
diff changeset
   139
apply (erule cpo_lubI)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   140
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   141
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   142
text {* constant functions are continuous *}
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   143
37079
0cd15d8c90a0 remove cont2cont simproc; instead declare cont2cont rules as simp rules
huffman
parents: 36658
diff changeset
   144
lemma cont_const [simp, cont2cont]: "cont (\<lambda>x. c)"
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40736
diff changeset
   145
  using is_lub_const by (rule contI)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   146
29532
59bee7985149 add lemmas cont2monofunE, cont2cont_apply
huffman
parents: 29530
diff changeset
   147
text {* application of functions is continuous *}
59bee7985149 add lemmas cont2monofunE, cont2cont_apply
huffman
parents: 29530
diff changeset
   148
31041
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 31030
diff changeset
   149
lemma cont_apply:
29532
59bee7985149 add lemmas cont2monofunE, cont2cont_apply
huffman
parents: 29530
diff changeset
   150
  fixes f :: "'a::cpo \<Rightarrow> 'b::cpo \<Rightarrow> 'c::cpo" and t :: "'a \<Rightarrow> 'b"
31041
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 31030
diff changeset
   151
  assumes 1: "cont (\<lambda>x. t x)"
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 31030
diff changeset
   152
  assumes 2: "\<And>x. cont (\<lambda>y. f x y)"
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 31030
diff changeset
   153
  assumes 3: "\<And>y. cont (\<lambda>x. f x y)"
29532
59bee7985149 add lemmas cont2monofunE, cont2cont_apply
huffman
parents: 29530
diff changeset
   154
  shows "cont (\<lambda>x. (f x) (t x))"
35914
91a7311177c4 remove contlub predicate
huffman
parents: 35900
diff changeset
   155
proof (rule contI2 [OF monofunI])
29532
59bee7985149 add lemmas cont2monofunE, cont2cont_apply
huffman
parents: 29530
diff changeset
   156
  fix x y :: "'a" assume "x \<sqsubseteq> y"
59bee7985149 add lemmas cont2monofunE, cont2cont_apply
huffman
parents: 29530
diff changeset
   157
  then show "f x (t x) \<sqsubseteq> f y (t y)"
31041
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 31030
diff changeset
   158
    by (auto intro: cont2monofunE [OF 1]
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 31030
diff changeset
   159
                    cont2monofunE [OF 2]
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 31030
diff changeset
   160
                    cont2monofunE [OF 3]
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31041
diff changeset
   161
                    below_trans)
29532
59bee7985149 add lemmas cont2monofunE, cont2cont_apply
huffman
parents: 29530
diff changeset
   162
next
59bee7985149 add lemmas cont2monofunE, cont2cont_apply
huffman
parents: 29530
diff changeset
   163
  fix Y :: "nat \<Rightarrow> 'a" assume "chain Y"
35914
91a7311177c4 remove contlub predicate
huffman
parents: 35900
diff changeset
   164
  then show "f (\<Squnion>i. Y i) (t (\<Squnion>i. Y i)) \<sqsubseteq> (\<Squnion>i. f (Y i) (t (Y i)))"
31041
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 31030
diff changeset
   165
    by (simp only: cont2contlubE [OF 1] ch2ch_cont [OF 1]
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 31030
diff changeset
   166
                   cont2contlubE [OF 2] ch2ch_cont [OF 2]
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 31030
diff changeset
   167
                   cont2contlubE [OF 3] ch2ch_cont [OF 3]
35914
91a7311177c4 remove contlub predicate
huffman
parents: 35900
diff changeset
   168
                   diag_lub below_refl)
29532
59bee7985149 add lemmas cont2monofunE, cont2cont_apply
huffman
parents: 29530
diff changeset
   169
qed
59bee7985149 add lemmas cont2monofunE, cont2cont_apply
huffman
parents: 29530
diff changeset
   170
31041
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 31030
diff changeset
   171
lemma cont_compose:
29532
59bee7985149 add lemmas cont2monofunE, cont2cont_apply
huffman
parents: 29530
diff changeset
   172
  "\<lbrakk>cont c; cont (\<lambda>x. f x)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. c (f x))"
31041
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 31030
diff changeset
   173
by (rule cont_apply [OF _ _ cont_const])
29532
59bee7985149 add lemmas cont2monofunE, cont2cont_apply
huffman
parents: 29530
diff changeset
   174
40004
9f6ed6840e8d reformulate lemma cont2cont_lub and move to Cont.thy
huffman
parents: 37099
diff changeset
   175
text {* Least upper bounds preserve continuity *}
9f6ed6840e8d reformulate lemma cont2cont_lub and move to Cont.thy
huffman
parents: 37099
diff changeset
   176
9f6ed6840e8d reformulate lemma cont2cont_lub and move to Cont.thy
huffman
parents: 37099
diff changeset
   177
lemma cont2cont_lub [simp]:
9f6ed6840e8d reformulate lemma cont2cont_lub and move to Cont.thy
huffman
parents: 37099
diff changeset
   178
  assumes chain: "\<And>x. chain (\<lambda>i. F i x)" and cont: "\<And>i. cont (\<lambda>x. F i x)"
9f6ed6840e8d reformulate lemma cont2cont_lub and move to Cont.thy
huffman
parents: 37099
diff changeset
   179
  shows "cont (\<lambda>x. \<Squnion>i. F i x)"
9f6ed6840e8d reformulate lemma cont2cont_lub and move to Cont.thy
huffman
parents: 37099
diff changeset
   180
apply (rule contI2)
9f6ed6840e8d reformulate lemma cont2cont_lub and move to Cont.thy
huffman
parents: 37099
diff changeset
   181
apply (simp add: monofunI cont2monofunE [OF cont] lub_mono chain)
9f6ed6840e8d reformulate lemma cont2cont_lub and move to Cont.thy
huffman
parents: 37099
diff changeset
   182
apply (simp add: cont2contlubE [OF cont])
9f6ed6840e8d reformulate lemma cont2cont_lub and move to Cont.thy
huffman
parents: 37099
diff changeset
   183
apply (simp add: diag_lub ch2ch_cont [OF cont] chain)
9f6ed6840e8d reformulate lemma cont2cont_lub and move to Cont.thy
huffman
parents: 37099
diff changeset
   184
done
9f6ed6840e8d reformulate lemma cont2cont_lub and move to Cont.thy
huffman
parents: 37099
diff changeset
   185
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   186
text {* if-then-else is continuous *}
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   187
37099
3636b08cbf51 declare a few more cont2cont rules
huffman
parents: 37079
diff changeset
   188
lemma cont_if [simp, cont2cont]:
26452
ed657432b8b9 declare cont_lemmas_ext as simp rules individually
huffman
parents: 26027
diff changeset
   189
  "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. if b then f x else g x)"
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   190
by (induct b) simp_all
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   191
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   192
subsection {* Finite chains and flat pcpos *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   193
40010
d7fdd84b959f edit comments
huffman
parents: 40004
diff changeset
   194
text {* Monotone functions map finite chains to finite chains. *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   195
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   196
lemma monofun_finch2finch:
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   197
  "\<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
   198
apply (unfold finite_chain_def)
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   199
apply (simp add: ch2ch_monofun)
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   200
apply (force simp add: max_in_chain_def)
15565
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
40010
d7fdd84b959f edit comments
huffman
parents: 40004
diff changeset
   203
text {* The same holds for continuous functions. *}
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   204
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   205
lemma cont_finch2finch:
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   206
  "\<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
   207
by (rule cont2mono [THEN monofun_finch2finch])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   208
40010
d7fdd84b959f edit comments
huffman
parents: 40004
diff changeset
   209
text {* All monotone functions with chain-finite domain are continuous. *}
d7fdd84b959f edit comments
huffman
parents: 40004
diff changeset
   210
25825
94c075b912ff generalized chfindom_monofun2cont
huffman
parents: 25786
diff changeset
   211
lemma chfindom_monofun2cont: "monofun f \<Longrightarrow> cont (f::'a::chfin \<Rightarrow> 'b::cpo)"
35914
91a7311177c4 remove contlub predicate
huffman
parents: 35900
diff changeset
   212
apply (erule contI2)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   213
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
   214
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
   215
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
   216
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
   217
apply (force simp add: max_in_chain_def)
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   218
done
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   219
40010
d7fdd84b959f edit comments
huffman
parents: 40004
diff changeset
   220
text {* All strict functions with flat domain are continuous. *}
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   221
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   222
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
   223
apply (rule monofunI)
25920
8df5eabda5f6 change class axiom ax_flat to rule_format
huffman
parents: 25896
diff changeset
   224
apply (drule ax_flat)
16624
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   225
apply auto
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   226
done
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   227
645b9560f3fd cleaned up; reorganized and added section headings
huffman
parents: 16564
diff changeset
   228
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
   229
by (rule flatdom_strict2mono [THEN chfindom_monofun2cont])
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
   230
40010
d7fdd84b959f edit comments
huffman
parents: 40004
diff changeset
   231
text {* All functions with discrete domain are continuous. *}
26024
d5129e687290 new lemma cont_discrete_cpo
huffman
parents: 25920
diff changeset
   232
37079
0cd15d8c90a0 remove cont2cont simproc; instead declare cont2cont rules as simp rules
huffman
parents: 36658
diff changeset
   233
lemma cont_discrete_cpo [simp, cont2cont]: "cont (f::'a::discrete_cpo \<Rightarrow> 'b::cpo)"
26024
d5129e687290 new lemma cont_discrete_cpo
huffman
parents: 25920
diff changeset
   234
apply (rule contI)
d5129e687290 new lemma cont_discrete_cpo
huffman
parents: 25920
diff changeset
   235
apply (drule discrete_chain_const, clarify)
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40736
diff changeset
   236
apply (simp add: is_lub_const)
26024
d5129e687290 new lemma cont_discrete_cpo
huffman
parents: 25920
diff changeset
   237
done
d5129e687290 new lemma cont_discrete_cpo
huffman
parents: 25920
diff changeset
   238
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   239
end