author  huffman 
Sat, 04 Jun 2005 00:22:08 +0200  
changeset 16221  879400e029bf 
parent 16214  e3816a7db016 
child 16388  1ff571813848 
permissions  rwrr 
2640  1 
(* Title: HOLCF/Fix.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:
16056
diff
changeset

5 
Definitions for fixed point operator and admissibility. 
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 {* Fixed point operator and admissibility *} 
9 

10 
theory Fix 

16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
16006
diff
changeset

11 
imports Cfun Cprod Adm 
15577  12 
begin 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

13 

16082  14 
defaultsort pcpo 
15 

16005  16 
subsection {* Definitions *} 
17 

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

18 
consts 
16214  19 
iterate :: "nat \<Rightarrow> ('a \<rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" 
20 
Ifix :: "('a \<rightarrow> 'a) \<Rightarrow> 'a" 

21 
"fix" :: "('a \<rightarrow> 'a) \<rightarrow> 'a" 

22 
admw :: "('a \<Rightarrow> bool) \<Rightarrow> bool" 

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

23 

5192  24 
primrec 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

25 
iterate_0: "iterate 0 F x = x" 
16214  26 
iterate_Suc: "iterate (Suc n) F x = F\<cdot>(iterate n F x)" 
5192  27 

1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1150
diff
changeset

28 
defs 
16214  29 
Ifix_def: "Ifix \<equiv> \<lambda>F. \<Squnion>i. iterate i F \<bottom>" 
30 
fix_def: "fix \<equiv> \<Lambda> F. Ifix F" 

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

31 

16214  32 
admw_def: "admw P == !F. (!n. P (iterate n F UU)) > 
1479  33 
P (lub(range (%i. iterate i F UU)))" 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

34 

16005  35 
subsection {* Binder syntax for @{term fix} *} 
15857  36 

37 
syntax 

38 
"@FIX" :: "('a => 'a) => 'a" (binder "FIX " 10) 

39 
"@FIXP" :: "[patterns, 'a] => 'a" ("(3FIX <_>./ _)" [0, 10] 10) 

40 

41 
syntax (xsymbols) 

42 
"FIX " :: "[idt, 'a] => 'a" ("(3\<mu>_./ _)" [0, 10] 10) 

43 
"@FIXP" :: "[patterns, 'a] => 'a" ("(3\<mu>()<_>./ _)" [0, 10] 10) 

44 

45 
translations 

46 
"FIX x. LAM y. t" == "fix\<cdot>(LAM x y. t)" 

47 
"FIX x. t" == "fix\<cdot>(LAM x. t)" 

48 
"FIX <xs>. t" == "fix\<cdot>(LAM <xs>. t)" 

49 

16005  50 
subsection {* Properties of @{term iterate} and @{term fix} *} 
51 

15637
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset

52 
text {* derive inductive properties of iterate from primitive recursion *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

53 

16214  54 
lemma iterate_Suc2: "iterate (Suc n) F x = iterate n F (F\<cdot>x)" 
55 
by (induct_tac n, auto) 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

56 

15637
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset

57 
text {* 
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset

58 
The sequence of function iterations is a chain. 
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset

59 
This property is essential since monotonicity of iterate makes no sense. 
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset

60 
*} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

61 

16214  62 
lemma chain_iterate2: "x \<sqsubseteq> F\<cdot>x \<Longrightarrow> chain (\<lambda>i. iterate i F x)" 
63 
by (rule chainI, induct_tac i, auto elim: monofun_cfun_arg) 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

64 

16214  65 
lemma chain_iterate: "chain (\<lambda>i. iterate i F \<bottom>)" 
16005  66 
by (rule chain_iterate2 [OF minimal]) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

67 

15637
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset

68 
text {* 
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset

69 
Kleene's fixed point theorems for continuous functions in pointed 
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset

70 
omega cpo's 
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset

71 
*} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

72 

16214  73 
lemma Ifix_eq: "Ifix F = F\<cdot>(Ifix F)" 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

74 
apply (unfold Ifix_def) 
16005  75 
apply (subst lub_range_shift [of _ 1, symmetric]) 
76 
apply (rule chain_iterate) 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

77 
apply (subst contlub_cfun_arg) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

78 
apply (rule chain_iterate) 
16005  79 
apply simp 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

80 
done 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

81 

16214  82 
lemma Ifix_least: "F\<cdot>x = x \<Longrightarrow> Ifix F \<sqsubseteq> x" 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

83 
apply (unfold Ifix_def) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

84 
apply (rule is_lub_thelub) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

85 
apply (rule chain_iterate) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

86 
apply (rule ub_rangeI) 
16005  87 
apply (induct_tac i) 
88 
apply simp 

89 
apply simp 

16214  90 
apply (erule subst) 
91 
apply (erule monofun_cfun_arg) 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

92 
done 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

93 

16214  94 
text {* continuity of @{term iterate} *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

95 

16214  96 
lemma cont_iterate1: "cont (\<lambda>F. iterate n F x)" 
97 
by (induct_tac n, simp_all) 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

98 

16214  99 
lemma cont_iterate2: "cont (\<lambda>x. iterate n F x)" 
100 
by (induct_tac n, simp_all) 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

101 

16214  102 
lemma cont_iterate: "cont (iterate n)" 
103 
by (rule cont_iterate1 [THEN cont2cont_CF1L_rev2]) 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

104 

16214  105 
lemmas monofun_iterate2 = cont_iterate2 [THEN cont2mono, standard] 
106 
lemmas contlub_iterate2 = cont_iterate2 [THEN cont2contlub, standard] 

107 

108 
text {* continuity of @{term Ifix} *} 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

109 

16214  110 
lemma cont_Ifix: "cont Ifix" 
111 
apply (unfold Ifix_def) 

112 
apply (rule cont2cont_lub) 

113 
apply (rule ch2ch_fun_rev) 

16005  114 
apply (rule chain_iterate) 
16214  115 
apply (rule cont_iterate1) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

116 
done 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

117 

15637
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset

118 
text {* propagate properties of @{term Ifix} to its continuous counterpart *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

119 

16214  120 
lemma fix_eq: "fix\<cdot>F = F\<cdot>(fix\<cdot>F)" 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

121 
apply (unfold fix_def) 
15637
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset

122 
apply (simp add: cont_Ifix) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

123 
apply (rule Ifix_eq) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

124 
done 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

125 

16214  126 
lemma fix_least: "F\<cdot>x = x \<Longrightarrow> fix\<cdot>F \<sqsubseteq> x" 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

127 
apply (unfold fix_def) 
15637
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset

128 
apply (simp add: cont_Ifix) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

129 
apply (erule Ifix_least) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

130 
done 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

131 

16214  132 
lemma fix_eqI: "\<lbrakk>F\<cdot>x = x; \<forall>z. F\<cdot>z = z \<longrightarrow> x \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x = fix\<cdot>F" 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

133 
apply (rule antisym_less) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

134 
apply (erule allE) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

135 
apply (erule mp) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

136 
apply (rule fix_eq [symmetric]) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

137 
apply (erule fix_least) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

138 
done 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

139 

16214  140 
lemma fix_eq2: "f \<equiv> fix\<cdot>F \<Longrightarrow> f = F\<cdot>f" 
15637
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset

141 
by (simp add: fix_eq [symmetric]) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

142 

16214  143 
lemma fix_eq3: "f \<equiv> fix\<cdot>F \<Longrightarrow> f\<cdot>x = F\<cdot>f\<cdot>x" 
15637
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset

144 
by (erule fix_eq2 [THEN cfun_fun_cong]) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

145 

16214  146 
lemma fix_eq4: "f = fix\<cdot>F \<Longrightarrow> f = F\<cdot>f" 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

147 
apply (erule ssubst) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

148 
apply (rule fix_eq) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

149 
done 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

150 

16214  151 
lemma fix_eq5: "f = fix\<cdot>F \<Longrightarrow> f\<cdot>x = F\<cdot>f\<cdot>x" 
152 
by (erule fix_eq4 [THEN cfun_fun_cong]) 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

153 

15637
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset

154 
text {* direct connection between @{term fix} and iteration without @{term Ifix} *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

155 

16214  156 
lemma fix_def2: "fix\<cdot>F = (\<Squnion>i. iterate i F \<bottom>)" 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

157 
apply (unfold fix_def) 
16214  158 
apply (simp add: cont_Ifix) 
159 
apply (simp add: Ifix_def) 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

160 
done 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

161 

16005  162 
subsection {* Admissibility and fixed point induction *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

163 

15637
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset

164 
text {* an admissible formula is also weak admissible *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

165 

16214  166 
lemma adm_impl_admw: "adm P \<Longrightarrow> admw P" 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

167 
apply (unfold admw_def) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

168 
apply (intro strip) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

169 
apply (erule admD) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

170 
apply (rule chain_iterate) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

171 
apply assumption 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

172 
done 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

173 

16079
757e1c4a8081
moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
huffman
parents:
16070
diff
changeset

174 
text {* some lemmata for functions with flat/chfin domain/range types *} 
757e1c4a8081
moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
huffman
parents:
16070
diff
changeset

175 

16214  176 
lemma adm_chfindom: "adm (\<lambda>(u::'a::cpo \<rightarrow> 'b::chfin). P(u\<cdot>s))" 
16079
757e1c4a8081
moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
huffman
parents:
16070
diff
changeset

177 
apply (unfold adm_def) 
757e1c4a8081
moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
huffman
parents:
16070
diff
changeset

178 
apply (intro strip) 
757e1c4a8081
moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
huffman
parents:
16070
diff
changeset

179 
apply (drule chfin_Rep_CFunR) 
757e1c4a8081
moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
huffman
parents:
16070
diff
changeset

180 
apply (erule_tac x = "s" in allE) 
757e1c4a8081
moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
huffman
parents:
16070
diff
changeset

181 
apply clarsimp 
757e1c4a8081
moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
huffman
parents:
16070
diff
changeset

182 
done 
757e1c4a8081
moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
huffman
parents:
16070
diff
changeset

183 

757e1c4a8081
moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
huffman
parents:
16070
diff
changeset

184 
(* adm_flat not needed any more, since it is a special case of adm_chfindom *) 
757e1c4a8081
moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
huffman
parents:
16070
diff
changeset

185 

15637
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset

186 
text {* fixed point induction *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

187 

16214  188 
lemma fix_ind: "\<lbrakk>adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P (fix\<cdot>F)" 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

189 
apply (subst fix_def2) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

190 
apply (erule admD) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

191 
apply (rule chain_iterate) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

192 
apply (rule allI) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

193 
apply (induct_tac "i") 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

194 
apply simp 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

195 
apply simp 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

196 
done 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

197 

16214  198 
lemma def_fix_ind: 
199 
"\<lbrakk>f \<equiv> fix\<cdot>F; adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P f" 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

200 
apply simp 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

201 
apply (erule fix_ind) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

202 
apply assumption 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

203 
apply fast 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

204 
done 
15637
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset

205 

d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset

206 
text {* computational induction for weak admissible formulae *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

207 

16214  208 
lemma wfix_ind: "\<lbrakk>admw P; \<forall>n. P (iterate n F UU)\<rbrakk> \<Longrightarrow> P (fix\<cdot>F)" 
209 
by (simp add: fix_def2 admw_def) 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

210 

16214  211 
lemma def_wfix_ind: 
212 
"\<lbrakk>f \<equiv> fix\<cdot>F; admw P; \<forall>n. P (iterate n F \<bottom>)\<rbrakk> \<Longrightarrow> P f" 

213 
by (simp, rule wfix_ind) 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

214 

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

215 
end 