author  huffman 
Thu, 07 Jul 2005 18:19:20 +0200  
changeset 16737  f0fd06dc93e3 
parent 16624  645b9560f3fd 
child 17831  4a8c3f8b0a92 
permissions  rwrr 
15600  1 
(* Title: HOLCF/Cont.thy 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

2 
ID: $Id$ 
1479  3 
Author: Franz Regensburger 
243
c22b85994e17
Franz Regensburger's HigherOrder 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 HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

6 
*) 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

7 

15577  8 
header {* Continuity and monotonicity *} 
9 

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  12 
begin 
243
c22b85994e17
Franz Regensburger's HigherOrder 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 HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

18 

15565  19 
defaultsort po 
243
c22b85994e17
Franz Regensburger's HigherOrder 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 HigherOrder 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 HigherOrder 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 HigherOrder 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  32 

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  36 

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  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  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  48 

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  52 

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  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  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  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  78 
apply (erule chainE) 
79 
done 

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  82 

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  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  87 
apply (erule ub_rangeD) 
88 
done 

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  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  94 
apply (rule thelubE) 
95 
apply (erule ch2ch_monofun) 

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  98 
apply assumption 
99 
done 

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  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  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  110 
apply (erule lub_bin_chain [THEN thelubI]) 
111 
done 

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  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  121 
done 
122 

16737  123 
lemmas ch2ch_cont = cont2mono [THEN ch2ch_monofun] 
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  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  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  132 
apply assumption 
133 
done 

134 

16737  135 
lemmas cont2contlubE = cont2contlub [THEN contlubE] 
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  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  145 
done 
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  153 

16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

154 
text {* ifthenelse 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  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  172 
done 
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  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  185 
apply (simp add: ch2ch_cont) 
15565  186 
done 
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  194 
apply assumption 
195 
done 

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  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  204 
done 
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  207 
apply (rule monocontlub2cont) 
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  210 
apply (simp add: cont2contlubE) 
211 
apply (simp add: thelub_fun ch2ch_cont) 

15565  212 
done 
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  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) 
15565  218 
apply (rule less_fun [THEN iffD2]) 
219 
apply (blast dest: monofunE) 

220 
done 

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  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  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  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  231 
done 
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  234 
apply (rule cont2cont_CF1L_rev) 
235 
apply simp 

236 
done 

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  239 

16564  240 
lemma contlub_abstraction: 
241 
"\<lbrakk>chain Y; \<forall>y. cont (\<lambda>x.(c::'a::cpo\<Rightarrow>'b::type\<Rightarrow>'c::cpo) x y)\<rbrakk> \<Longrightarrow> 

242 
(\<lambda>y. \<Squnion>i. c (Y i) y) = (\<Squnion>i. (\<lambda>y. c (Y i) y))" 

243 
apply (rule thelub_fun [symmetric]) 

16737  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  246 
done 
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  252 
done 
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  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  263 
apply (erule (1) ch2ch_cont) 
264 
apply (erule (1) ch2ch_cont) 

265 
apply (erule (1) ch2ch_cont) 

15565  266 
done 
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  271 

16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

272 
lemmas cont2cont_app2 = cont2cont_app [rule_format] 
15565  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  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  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  286 
done 
287 

16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

288 
text {* The same holds for continuous functions *} 
15565  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  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  295 
apply (rule monocontlub2cont) 
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  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  303 
done 
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  315 

243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

316 
end 