author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 18092  2c5d5da79a1e 
child 25131  2c8caac48ade 
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) 
18088  95 
apply (erule (1) ch2ch_monofun) 
96 
apply (erule (1) contlubE [symmetric]) 

15565  97 
done 
98 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

99 
text {* first a lemma about binary chains *} 
15565  100 

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

101 
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

102 
"\<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

103 
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

104 
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

105 
apply (erule contE) 
15565  106 
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

107 
apply (rule_tac f=f in arg_cong) 
15565  108 
apply (erule lub_bin_chain [THEN thelubI]) 
109 
done 

110 

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

111 
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

112 
text {* part1: @{prop "cont f \<Longrightarrow> monofun f"} *} 
15565  113 

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

114 
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

115 
apply (rule monofunI) 
18088  116 
apply (drule (1) binchain_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

117 
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

118 
apply simp 
15565  119 
done 
120 

16737  121 
lemmas ch2ch_cont = cont2mono [THEN ch2ch_monofun] 
122 

16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset

123 
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

124 
text {* part2: @{prop "cont f \<Longrightarrow> contlub f"} *} 
15565  125 

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

126 
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

127 
apply (rule contlubI) 
15565  128 
apply (rule thelubI [symmetric]) 
18088  129 
apply (erule (1) contE) 
15565  130 
done 
131 

16737  132 
lemmas cont2contlubE = cont2contlub [THEN contlubE] 
133 

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

134 
subsection {* Continuity of basic functions *} 
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

135 

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

136 
text {* The identity function is continuous *} 
15565  137 

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

138 
lemma cont_id: "cont (\<lambda>x. x)" 
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

139 
apply (rule contI) 
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

140 
apply (erule thelubE) 
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

141 
apply (rule refl) 
15565  142 
done 
143 

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

144 
text {* constant functions are continuous *} 
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

145 

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

146 
lemma cont_const: "cont (\<lambda>x. c)" 
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

147 
apply (rule contI) 
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

148 
apply (rule lub_const) 
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

149 
done 
15565  150 

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

151 
text {* ifthenelse is continuous *} 
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

152 

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

153 
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

154 
by (induct b) simp_all 
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 
subsection {* Propagation of monotonicity and continuity *} 
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

157 

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

158 
text {* the lub of a chain of monotone functions is monotone *} 
15565  159 

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

160 
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

161 
"\<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

162 
\<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

163 
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

164 
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

165 
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

166 
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

167 
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

168 
apply (simp add: monofunE) 
15565  169 
done 
170 

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

171 
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

172 

5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset

173 
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

174 

5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset

175 
lemma 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

176 
"\<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

177 
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

178 
apply (simp add: thelub_fun) 
16737  179 
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

180 
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

181 
apply (erule ch2ch_fun) 
16737  182 
apply (simp add: ch2ch_cont) 
15565  183 
done 
184 

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

185 
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

186 
"\<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

187 
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

188 
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

189 
apply (simp add: cont2mono) 
18088  190 
apply (erule (1) contlub_lub_fun) 
15565  191 
done 
192 

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

193 
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

194 
"\<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

195 
by (simp add: thelub_fun [symmetric] cont_lub_fun) 
15565  196 

18092
2c5d5da79a1e
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
huffman
parents:
18088
diff
changeset

197 
lemma mono2mono_fun: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)" 
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

198 
apply (rule monofunI) 
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

199 
apply (erule (1) monofun_fun_arg [THEN monofun_fun_fun]) 
15565  200 
done 
201 

18092
2c5d5da79a1e
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
huffman
parents:
18088
diff
changeset

202 
lemma cont2cont_fun: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)" 
15565  203 
apply (rule monocontlub2cont) 
18092
2c5d5da79a1e
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
huffman
parents:
18088
diff
changeset

204 
apply (erule cont2mono [THEN mono2mono_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

205 
apply (rule contlubI) 
16737  206 
apply (simp add: cont2contlubE) 
207 
apply (simp add: thelub_fun ch2ch_cont) 

15565  208 
done 
209 

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

210 
text {* Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"} *} 
15565  211 

18092
2c5d5da79a1e
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
huffman
parents:
18088
diff
changeset

212 
lemma mono2mono_lambda: "(\<And>y. monofun (\<lambda>x. f x y)) \<Longrightarrow> monofun 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

213 
apply (rule monofunI) 
17831  214 
apply (rule less_fun_ext) 
15565  215 
apply (blast dest: monofunE) 
216 
done 

217 

18092
2c5d5da79a1e
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
huffman
parents:
18088
diff
changeset

218 
lemma cont2cont_lambda: "(\<And>y. cont (\<lambda>x. f x y)) \<Longrightarrow> cont f" 
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

219 
apply (subgoal_tac "monofun f") 
15565  220 
apply (rule monocontlub2cont) 
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

221 
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

222 
apply (rule contlubI) 
15565  223 
apply (rule ext) 
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

224 
apply (simp add: thelub_fun ch2ch_monofun) 
16737  225 
apply (blast dest: cont2contlubE) 
18092
2c5d5da79a1e
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
huffman
parents:
18088
diff
changeset

226 
apply (simp add: mono2mono_lambda cont2mono) 
15565  227 
done 
228 

18092
2c5d5da79a1e
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
huffman
parents:
18088
diff
changeset

229 
text {* What D.A.Schmidt calls continuity of abstraction; never used here *} 
16053  230 

18092
2c5d5da79a1e
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
huffman
parents:
18088
diff
changeset

231 
lemma contlub_lambda: 
2c5d5da79a1e
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
huffman
parents:
18088
diff
changeset

232 
"(\<And>x::'a::type. chain (\<lambda>i. S i x::'b::cpo)) 
2c5d5da79a1e
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
huffman
parents:
18088
diff
changeset

233 
\<Longrightarrow> (\<lambda>x. \<Squnion>i. S i x) = (\<Squnion>i. (\<lambda>x. S i x))" 
2c5d5da79a1e
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
huffman
parents:
18088
diff
changeset

234 
by (simp add: thelub_fun ch2ch_lambda) 
15565  235 

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

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

239 
apply (rule thelub_fun [symmetric]) 

18092
2c5d5da79a1e
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
huffman
parents:
18088
diff
changeset

240 
apply (rule ch2ch_cont) 
2c5d5da79a1e
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
huffman
parents:
18088
diff
changeset

241 
apply (simp add: cont2cont_lambda) 
2c5d5da79a1e
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
huffman
parents:
18088
diff
changeset

242 
apply assumption 
15565  243 
done 
244 

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

245 
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

246 
"\<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

247 
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

248 
apply (simp add: monofun_fun monofunE) 
15565  249 
done 
250 

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

251 
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

252 
"\<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

253 
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

254 
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

255 
apply (subgoal_tac "chain (\<lambda>i. t (Y i))") 
16737  256 
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

257 
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

258 
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

259 
apply (drule spec) 
16737  260 
apply (erule (1) ch2ch_cont) 
261 
apply (erule (1) ch2ch_cont) 

262 
apply (erule (1) ch2ch_cont) 

15565  263 
done 
264 

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

265 
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

266 
"\<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

267 
by (blast intro: monocontlub2cont mono2mono_app cont2mono cont2contlub_app) 
15565  268 

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

269 
lemmas cont2cont_app2 = cont2cont_app [rule_format] 
15565  270 

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

271 
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

272 
by (rule cont2cont_app2 [OF cont_const]) 
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

273 

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

274 
subsection {* Finite chains and flat pcpos *} 
15565  275 

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

276 
text {* monotone functions map finite chains to finite chains *} 
15565  277 

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

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

279 
"\<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

280 
apply (unfold finite_chain_def) 
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

281 
apply (simp add: ch2ch_monofun) 
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

282 
apply (force simp add: max_in_chain_def) 
15565  283 
done 
284 

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

285 
text {* The same holds for continuous functions *} 
15565  286 

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

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

288 
"\<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

289 
by (rule cont2mono [THEN monofun_finch2finch]) 
15565  290 

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

291 
lemma chfindom_monofun2cont: "monofun f \<Longrightarrow> cont (f::'a::chfin \<Rightarrow> 'b::pcpo)" 
15565  292 
apply (rule monocontlub2cont) 
293 
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

294 
apply (rule contlubI) 
15565  295 
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

296 
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

297 
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

298 
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

299 
apply (force simp add: max_in_chain_def) 
15565  300 
done 
301 

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

302 
text {* some properties of flat *} 
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

303 

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

304 
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

305 
apply (rule monofunI) 
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

306 
apply (drule ax_flat [rule_format]) 
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

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

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

309 

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

310 
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

311 
by (rule flatdom_strict2mono [THEN chfindom_monofun2cont]) 
15565  312 

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

313 
end 