author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 44066  d74182c93f04 
child 58880  0baae4311a9f 
permissions  rwrr 
42151  1 
(* Title: HOL/HOLCF/Fix.thy 
1479  2 
Author: Franz Regensburger 
35794  3 
Author: Brian Huffman 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

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

5 

15577  6 
header {* Fixed point operator and admissibility *} 
7 

8 
theory Fix 

35939  9 
imports Cfun 
15577  10 
begin 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

11 

36452  12 
default_sort pcpo 
16082  13 

18093
587692219f69
put iterate and fix in separate sections; added Letrec
huffman
parents:
18092
diff
changeset

14 
subsection {* Iteration *} 
16005  15 

34941  16 
primrec iterate :: "nat \<Rightarrow> ('a::cpo \<rightarrow> 'a) \<rightarrow> ('a \<rightarrow> 'a)" where 
17 
"iterate 0 = (\<Lambda> F x. x)" 

18 
 "iterate (Suc n) = (\<Lambda> F x. F\<cdot>(iterate n\<cdot>F\<cdot>x))" 

5192  19 

18093
587692219f69
put iterate and fix in separate sections; added Letrec
huffman
parents:
18092
diff
changeset

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

21 

18074
a92b7c5133de
reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents:
17816
diff
changeset

22 
lemma iterate_0 [simp]: "iterate 0\<cdot>F\<cdot>x = x" 
a92b7c5133de
reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents:
17816
diff
changeset

23 
by simp 
a92b7c5133de
reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents:
17816
diff
changeset

24 

a92b7c5133de
reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents:
17816
diff
changeset

25 
lemma iterate_Suc [simp]: "iterate (Suc n)\<cdot>F\<cdot>x = F\<cdot>(iterate n\<cdot>F\<cdot>x)" 
a92b7c5133de
reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents:
17816
diff
changeset

26 
by simp 
a92b7c5133de
reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents:
17816
diff
changeset

27 

a92b7c5133de
reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents:
17816
diff
changeset

28 
declare iterate.simps [simp del] 
a92b7c5133de
reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents:
17816
diff
changeset

29 

a92b7c5133de
reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents:
17816
diff
changeset

30 
lemma iterate_Suc2: "iterate (Suc n)\<cdot>F\<cdot>x = iterate n\<cdot>F\<cdot>(F\<cdot>x)" 
27270  31 
by (induct n) simp_all 
32 

33 
lemma iterate_iterate: 

34 
"iterate m\<cdot>F\<cdot>(iterate n\<cdot>F\<cdot>x) = iterate (m + n)\<cdot>F\<cdot>x" 

35 
by (induct m) simp_all 

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

36 

36075
2e0370c03066
tuned proof (no induction needed); removed unused lemma and fuzzy comment
krauss
parents:
35939
diff
changeset

37 
text {* The sequence of function iterations is a chain. *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

38 

18074
a92b7c5133de
reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents:
17816
diff
changeset

39 
lemma chain_iterate [simp]: "chain (\<lambda>i. iterate i\<cdot>F\<cdot>\<bottom>)" 
36075
2e0370c03066
tuned proof (no induction needed); removed unused lemma and fuzzy comment
krauss
parents:
35939
diff
changeset

40 
by (rule chainI, unfold iterate_Suc2, rule monofun_cfun_arg, rule minimal) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

41 

18093
587692219f69
put iterate and fix in separate sections; added Letrec
huffman
parents:
18092
diff
changeset

42 

587692219f69
put iterate and fix in separate sections; added Letrec
huffman
parents:
18092
diff
changeset

43 
subsection {* Least fixed point operator *} 
587692219f69
put iterate and fix in separate sections; added Letrec
huffman
parents:
18092
diff
changeset

44 

25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18095
diff
changeset

45 
definition 
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18095
diff
changeset

46 
"fix" :: "('a \<rightarrow> 'a) \<rightarrow> 'a" where 
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18095
diff
changeset

47 
"fix = (\<Lambda> F. \<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>)" 
18093
587692219f69
put iterate and fix in separate sections; added Letrec
huffman
parents:
18092
diff
changeset

48 

587692219f69
put iterate and fix in separate sections; added Letrec
huffman
parents:
18092
diff
changeset

49 
text {* Binder syntax for @{term fix} *} 
587692219f69
put iterate and fix in separate sections; added Letrec
huffman
parents:
18092
diff
changeset

50 

27316
9e74019041d4
use newstyle abbreviation/notation for fix syntax
huffman
parents:
27270
diff
changeset

51 
abbreviation 
9e74019041d4
use newstyle abbreviation/notation for fix syntax
huffman
parents:
27270
diff
changeset

52 
fix_syn :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" (binder "FIX " 10) where 
9e74019041d4
use newstyle abbreviation/notation for fix syntax
huffman
parents:
27270
diff
changeset

53 
"fix_syn (\<lambda>x. f x) \<equiv> fix\<cdot>(\<Lambda> x. f x)" 
18093
587692219f69
put iterate and fix in separate sections; added Letrec
huffman
parents:
18092
diff
changeset

54 

27316
9e74019041d4
use newstyle abbreviation/notation for fix syntax
huffman
parents:
27270
diff
changeset

55 
notation (xsymbols) 
9e74019041d4
use newstyle abbreviation/notation for fix syntax
huffman
parents:
27270
diff
changeset

56 
fix_syn (binder "\<mu> " 10) 
18093
587692219f69
put iterate and fix in separate sections; added Letrec
huffman
parents:
18092
diff
changeset

57 

587692219f69
put iterate and fix in separate sections; added Letrec
huffman
parents:
18092
diff
changeset

58 
text {* Properties of @{term fix} *} 
18074
a92b7c5133de
reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents:
17816
diff
changeset

59 

18090
9d5cfd71f510
moved adm_chfindom from Fix.thy to Cfun.thy; moved admwrelated stuff to its own section
huffman
parents:
18078
diff
changeset

60 
text {* direct connection between @{term fix} and iteration *} 
18074
a92b7c5133de
reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents:
17816
diff
changeset

61 

a92b7c5133de
reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents:
17816
diff
changeset

62 
lemma fix_def2: "fix\<cdot>F = (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>)" 
40004
9f6ed6840e8d
reformulate lemma cont2cont_lub and move to Cont.thy
huffman
parents:
36452
diff
changeset

63 
unfolding fix_def by simp 
18074
a92b7c5133de
reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents:
17816
diff
changeset

64 

35055  65 
lemma iterate_below_fix: "iterate n\<cdot>f\<cdot>\<bottom> \<sqsubseteq> fix\<cdot>f" 
66 
unfolding fix_def2 

67 
using chain_iterate by (rule is_ub_thelub) 

68 

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

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

70 
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

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

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

73 

18074
a92b7c5133de
reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents:
17816
diff
changeset

74 
lemma fix_eq: "fix\<cdot>F = F\<cdot>(fix\<cdot>F)" 
a92b7c5133de
reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents:
17816
diff
changeset

75 
apply (simp add: fix_def2) 
16005  76 
apply (subst lub_range_shift [of _ 1, symmetric]) 
77 
apply (rule chain_iterate) 

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

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

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

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

82 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

83 
lemma fix_least_below: "F\<cdot>x \<sqsubseteq> x \<Longrightarrow> fix\<cdot>F \<sqsubseteq> x" 
18074
a92b7c5133de
reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents:
17816
diff
changeset

84 
apply (simp add: fix_def2) 
40500
ee9c8d36318e
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents:
40321
diff
changeset

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

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

89 
apply simp 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

90 
apply (erule rev_below_trans) 
16214  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 
lemma fix_least: "F\<cdot>x = x \<Longrightarrow> fix\<cdot>F \<sqsubseteq> x" 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

95 
by (rule fix_least_below, simp) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
14981
diff
changeset

96 

27185
0407630909ef
change orientation of fix_eqI and convert to rule_format;
huffman
parents:
25927
diff
changeset

97 
lemma fix_eqI: 
0407630909ef
change orientation of fix_eqI and convert to rule_format;
huffman
parents:
25927
diff
changeset

98 
assumes fixed: "F\<cdot>x = x" and least: "\<And>z. F\<cdot>z = z \<Longrightarrow> x \<sqsubseteq> z" 
0407630909ef
change orientation of fix_eqI and convert to rule_format;
huffman
parents:
25927
diff
changeset

99 
shows "fix\<cdot>F = x" 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

100 
apply (rule below_antisym) 
27185
0407630909ef
change orientation of fix_eqI and convert to rule_format;
huffman
parents:
25927
diff
changeset

101 
apply (rule fix_least [OF fixed]) 
0407630909ef
change orientation of fix_eqI and convert to rule_format;
huffman
parents:
25927
diff
changeset

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

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

104 

16214  105 
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

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

107 

16214  108 
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

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

110 

16214  111 
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

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

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

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

115 

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

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

118 

16556
a0c8d0499b5f
added theorems fix_strict, fix_defined, fix_id, fix_const
huffman
parents:
16388
diff
changeset

119 
text {* strictness of @{term fix} *} 
a0c8d0499b5f
added theorems fix_strict, fix_defined, fix_id, fix_const
huffman
parents:
16388
diff
changeset

120 

40321
d065b195ec89
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents:
40004
diff
changeset

121 
lemma fix_bottom_iff: "(fix\<cdot>F = \<bottom>) = (F\<cdot>\<bottom> = \<bottom>)" 
16917  122 
apply (rule iffI) 
123 
apply (erule subst) 

124 
apply (rule fix_eq [symmetric]) 

41430
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41324
diff
changeset

125 
apply (erule fix_least [THEN bottomI]) 
16917  126 
done 
127 

16556
a0c8d0499b5f
added theorems fix_strict, fix_defined, fix_id, fix_const
huffman
parents:
16388
diff
changeset

128 
lemma fix_strict: "F\<cdot>\<bottom> = \<bottom> \<Longrightarrow> fix\<cdot>F = \<bottom>" 
40321
d065b195ec89
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents:
40004
diff
changeset

129 
by (simp add: fix_bottom_iff) 
16556
a0c8d0499b5f
added theorems fix_strict, fix_defined, fix_id, fix_const
huffman
parents:
16388
diff
changeset

130 

a0c8d0499b5f
added theorems fix_strict, fix_defined, fix_id, fix_const
huffman
parents:
16388
diff
changeset

131 
lemma fix_defined: "F\<cdot>\<bottom> \<noteq> \<bottom> \<Longrightarrow> fix\<cdot>F \<noteq> \<bottom>" 
40321
d065b195ec89
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents:
40004
diff
changeset

132 
by (simp add: fix_bottom_iff) 
16556
a0c8d0499b5f
added theorems fix_strict, fix_defined, fix_id, fix_const
huffman
parents:
16388
diff
changeset

133 

a0c8d0499b5f
added theorems fix_strict, fix_defined, fix_id, fix_const
huffman
parents:
16388
diff
changeset

134 
text {* @{term fix} applied to identity and constant functions *} 
a0c8d0499b5f
added theorems fix_strict, fix_defined, fix_id, fix_const
huffman
parents:
16388
diff
changeset

135 

a0c8d0499b5f
added theorems fix_strict, fix_defined, fix_id, fix_const
huffman
parents:
16388
diff
changeset

136 
lemma fix_id: "(\<mu> x. x) = \<bottom>" 
a0c8d0499b5f
added theorems fix_strict, fix_defined, fix_id, fix_const
huffman
parents:
16388
diff
changeset

137 
by (simp add: fix_strict) 
a0c8d0499b5f
added theorems fix_strict, fix_defined, fix_id, fix_const
huffman
parents:
16388
diff
changeset

138 

a0c8d0499b5f
added theorems fix_strict, fix_defined, fix_id, fix_const
huffman
parents:
16388
diff
changeset

139 
lemma fix_const: "(\<mu> x. c) = c" 
18074
a92b7c5133de
reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents:
17816
diff
changeset

140 
by (subst fix_eq, simp) 
16556
a0c8d0499b5f
added theorems fix_strict, fix_defined, fix_id, fix_const
huffman
parents:
16388
diff
changeset

141 

18090
9d5cfd71f510
moved adm_chfindom from Fix.thy to Cfun.thy; moved admwrelated stuff to its own section
huffman
parents:
18078
diff
changeset

142 
subsection {* Fixed point induction *} 
9d5cfd71f510
moved adm_chfindom from Fix.thy to Cfun.thy; moved admwrelated stuff to its own section
huffman
parents:
18078
diff
changeset

143 

9d5cfd71f510
moved adm_chfindom from Fix.thy to Cfun.thy; moved admwrelated stuff to its own section
huffman
parents:
18078
diff
changeset

144 
lemma fix_ind: "\<lbrakk>adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P (fix\<cdot>F)" 
27185
0407630909ef
change orientation of fix_eqI and convert to rule_format;
huffman
parents:
25927
diff
changeset

145 
unfolding fix_def2 
25925  146 
apply (erule admD) 
18090
9d5cfd71f510
moved adm_chfindom from Fix.thy to Cfun.thy; moved admwrelated stuff to its own section
huffman
parents:
18078
diff
changeset

147 
apply (rule chain_iterate) 
27185
0407630909ef
change orientation of fix_eqI and convert to rule_format;
huffman
parents:
25927
diff
changeset

148 
apply (rule nat_induct, simp_all) 
18090
9d5cfd71f510
moved adm_chfindom from Fix.thy to Cfun.thy; moved admwrelated stuff to its own section
huffman
parents:
18078
diff
changeset

149 
done 
9d5cfd71f510
moved adm_chfindom from Fix.thy to Cfun.thy; moved admwrelated stuff to its own section
huffman
parents:
18078
diff
changeset

150 

41324
1383653efec3
make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for betareduction
huffman
parents:
40774
diff
changeset

151 
lemma cont_fix_ind: 
1383653efec3
make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for betareduction
huffman
parents:
40774
diff
changeset

152 
"\<lbrakk>cont F; adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F x)\<rbrakk> \<Longrightarrow> P (fix\<cdot>(Abs_cfun F))" 
1383653efec3
make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for betareduction
huffman
parents:
40774
diff
changeset

153 
by (simp add: fix_ind) 
1383653efec3
make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for betareduction
huffman
parents:
40774
diff
changeset

154 

18090
9d5cfd71f510
moved adm_chfindom from Fix.thy to Cfun.thy; moved admwrelated stuff to its own section
huffman
parents:
18078
diff
changeset

155 
lemma def_fix_ind: 
9d5cfd71f510
moved adm_chfindom from Fix.thy to Cfun.thy; moved admwrelated stuff to its own section
huffman
parents:
18078
diff
changeset

156 
"\<lbrakk>f \<equiv> fix\<cdot>F; adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P f" 
9d5cfd71f510
moved adm_chfindom from Fix.thy to Cfun.thy; moved admwrelated stuff to its own section
huffman
parents:
18078
diff
changeset

157 
by (simp add: fix_ind) 
9d5cfd71f510
moved adm_chfindom from Fix.thy to Cfun.thy; moved admwrelated stuff to its own section
huffman
parents:
18078
diff
changeset

158 

27185
0407630909ef
change orientation of fix_eqI and convert to rule_format;
huffman
parents:
25927
diff
changeset

159 
lemma fix_ind2: 
0407630909ef
change orientation of fix_eqI and convert to rule_format;
huffman
parents:
25927
diff
changeset

160 
assumes adm: "adm P" 
0407630909ef
change orientation of fix_eqI and convert to rule_format;
huffman
parents:
25927
diff
changeset

161 
assumes 0: "P \<bottom>" and 1: "P (F\<cdot>\<bottom>)" 
0407630909ef
change orientation of fix_eqI and convert to rule_format;
huffman
parents:
25927
diff
changeset

162 
assumes step: "\<And>x. \<lbrakk>P x; P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P (F\<cdot>(F\<cdot>x))" 
0407630909ef
change orientation of fix_eqI and convert to rule_format;
huffman
parents:
25927
diff
changeset

163 
shows "P (fix\<cdot>F)" 
0407630909ef
change orientation of fix_eqI and convert to rule_format;
huffman
parents:
25927
diff
changeset

164 
unfolding fix_def2 
0407630909ef
change orientation of fix_eqI and convert to rule_format;
huffman
parents:
25927
diff
changeset

165 
apply (rule admD [OF adm chain_iterate]) 
0407630909ef
change orientation of fix_eqI and convert to rule_format;
huffman
parents:
25927
diff
changeset

166 
apply (rule nat_less_induct) 
0407630909ef
change orientation of fix_eqI and convert to rule_format;
huffman
parents:
25927
diff
changeset

167 
apply (case_tac n) 
0407630909ef
change orientation of fix_eqI and convert to rule_format;
huffman
parents:
25927
diff
changeset

168 
apply (simp add: 0) 
0407630909ef
change orientation of fix_eqI and convert to rule_format;
huffman
parents:
25927
diff
changeset

169 
apply (case_tac nat) 
0407630909ef
change orientation of fix_eqI and convert to rule_format;
huffman
parents:
25927
diff
changeset

170 
apply (simp add: 1) 
0407630909ef
change orientation of fix_eqI and convert to rule_format;
huffman
parents:
25927
diff
changeset

171 
apply (frule_tac x=nat in spec) 
0407630909ef
change orientation of fix_eqI and convert to rule_format;
huffman
parents:
25927
diff
changeset

172 
apply (simp add: step) 
0407630909ef
change orientation of fix_eqI and convert to rule_format;
huffman
parents:
25927
diff
changeset

173 
done 
0407630909ef
change orientation of fix_eqI and convert to rule_format;
huffman
parents:
25927
diff
changeset

174 

33590  175 
lemma parallel_fix_ind: 
176 
assumes adm: "adm (\<lambda>x. P (fst x) (snd x))" 

177 
assumes base: "P \<bottom> \<bottom>" 

178 
assumes step: "\<And>x y. P x y \<Longrightarrow> P (F\<cdot>x) (G\<cdot>y)" 

179 
shows "P (fix\<cdot>F) (fix\<cdot>G)" 

180 
proof  

181 
from adm have adm': "adm (split P)" 

182 
unfolding split_def . 

183 
have "\<And>i. P (iterate i\<cdot>F\<cdot>\<bottom>) (iterate i\<cdot>G\<cdot>\<bottom>)" 

184 
by (induct_tac i, simp add: base, simp add: step) 

185 
hence "\<And>i. split P (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>)" 

186 
by simp 

187 
hence "split P (\<Squnion>i. (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>))" 

188 
by  (rule admD [OF adm'], simp, assumption) 

189 
hence "split P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>, \<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)" 

40771  190 
by (simp add: lub_Pair) 
33590  191 
hence "P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>) (\<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)" 
192 
by simp 

193 
thus "P (fix\<cdot>F) (fix\<cdot>G)" 

194 
by (simp add: fix_def2) 

195 
qed 

196 

41324
1383653efec3
make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for betareduction
huffman
parents:
40774
diff
changeset

197 
lemma cont_parallel_fix_ind: 
1383653efec3
make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for betareduction
huffman
parents:
40774
diff
changeset

198 
assumes "cont F" and "cont G" 
1383653efec3
make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for betareduction
huffman
parents:
40774
diff
changeset

199 
assumes "adm (\<lambda>x. P (fst x) (snd x))" 
1383653efec3
make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for betareduction
huffman
parents:
40774
diff
changeset

200 
assumes "P \<bottom> \<bottom>" 
1383653efec3
make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for betareduction
huffman
parents:
40774
diff
changeset

201 
assumes "\<And>x y. P x y \<Longrightarrow> P (F x) (G y)" 
1383653efec3
make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for betareduction
huffman
parents:
40774
diff
changeset

202 
shows "P (fix\<cdot>(Abs_cfun F)) (fix\<cdot>(Abs_cfun G))" 
1383653efec3
make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for betareduction
huffman
parents:
40774
diff
changeset

203 
by (rule parallel_fix_ind, simp_all add: assms) 
1383653efec3
make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for betareduction
huffman
parents:
40774
diff
changeset

204 

35932
86559356502d
move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents:
35923
diff
changeset

205 
subsection {* Fixedpoints on product types *} 
18093
587692219f69
put iterate and fix in separate sections; added Letrec
huffman
parents:
18092
diff
changeset

206 

18095  207 
text {* 
208 
Bekic's Theorem: Simultaneous fixed points over pairs 

209 
can be written in terms of separate fixed points. 

210 
*} 

211 

212 
lemma fix_cprod: 

213 
"fix\<cdot>(F::'a \<times> 'b \<rightarrow> 'a \<times> 'b) = 

35921  214 
(\<mu> x. fst (F\<cdot>(x, \<mu> y. snd (F\<cdot>(x, y)))), 
215 
\<mu> y. snd (F\<cdot>(\<mu> x. fst (F\<cdot>(x, \<mu> y. snd (F\<cdot>(x, y)))), y)))" 

216 
(is "fix\<cdot>F = (?x, ?y)") 

27185
0407630909ef
change orientation of fix_eqI and convert to rule_format;
huffman
parents:
25927
diff
changeset

217 
proof (rule fix_eqI) 
35921  218 
have 1: "fst (F\<cdot>(?x, ?y)) = ?x" 
18095  219 
by (rule trans [symmetric, OF fix_eq], simp) 
35921  220 
have 2: "snd (F\<cdot>(?x, ?y)) = ?y" 
18095  221 
by (rule trans [symmetric, OF fix_eq], simp) 
44066
d74182c93f04
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
huffman
parents:
42151
diff
changeset

222 
from 1 2 show "F\<cdot>(?x, ?y) = (?x, ?y)" by (simp add: prod_eq_iff) 
18095  223 
next 
224 
fix z assume F_z: "F\<cdot>z = z" 

35921  225 
obtain x y where z: "z = (x,y)" by (rule prod.exhaust) 
226 
from F_z z have F_x: "fst (F\<cdot>(x, y)) = x" by simp 

227 
from F_z z have F_y: "snd (F\<cdot>(x, y)) = y" by simp 

228 
let ?y1 = "\<mu> y. snd (F\<cdot>(x, y))" 

18095  229 
have "?y1 \<sqsubseteq> y" by (rule fix_least, simp add: F_y) 
35921  230 
hence "fst (F\<cdot>(x, ?y1)) \<sqsubseteq> fst (F\<cdot>(x, y))" 
231 
by (simp add: fst_monofun monofun_cfun) 

232 
hence "fst (F\<cdot>(x, ?y1)) \<sqsubseteq> x" using F_x by simp 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

233 
hence 1: "?x \<sqsubseteq> x" by (simp add: fix_least_below) 
35921  234 
hence "snd (F\<cdot>(?x, y)) \<sqsubseteq> snd (F\<cdot>(x, y))" 
235 
by (simp add: snd_monofun monofun_cfun) 

236 
hence "snd (F\<cdot>(?x, y)) \<sqsubseteq> y" using F_y by simp 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

237 
hence 2: "?y \<sqsubseteq> y" by (simp add: fix_least_below) 
35921  238 
show "(?x, ?y) \<sqsubseteq> z" using z 1 2 by simp 
18095  239 
qed 
240 

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

241 
end 