author  nipkow 
Fri, 10 Sep 2004 20:04:14 +0200  
changeset 15197  19e735596e51 
parent 15140  322485b816ac 
child 18372  2bffdf62fe7f 
permissions  rwrr 
10251  1 
(* Title: HOL/Library/While.thy 
2 
ID: $Id$ 

3 
Author: Tobias Nipkow 

4 
Copyright 2000 TU Muenchen 

5 
*) 

6 

14706  7 
header {* A general ``while'' combinator *} 
10251  8 

15131  9 
theory While_Combinator 
15140  10 
imports Main 
15131  11 
begin 
10251  12 

13 
text {* 

14 
We define a whilecombinator @{term while} and prove: (a) an 

15 
unrestricted unfolding law (even if while diverges!) (I got this 

16 
idea from Wolfgang Goerigk), and (b) the invariant rule for reasoning 

17 
about @{term while}. 

18 
*} 

19 

20 
consts while_aux :: "('a => bool) \<times> ('a => 'a) \<times> 'a => 'a" 

11626  21 
recdef (permissive) while_aux 
10251  22 
"same_fst (\<lambda>b. True) (\<lambda>b. same_fst (\<lambda>c. True) (\<lambda>c. 
23 
{(t, s). b s \<and> c s = t \<and> 

11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11626
diff
changeset

24 
\<not> (\<exists>f. f (0::nat) = s \<and> (\<forall>i. b (f i) \<and> c (f i) = f (i + 1)))}))" 
10251  25 
"while_aux (b, c, s) = 
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11626
diff
changeset

26 
(if (\<exists>f. f (0::nat) = s \<and> (\<forall>i. b (f i) \<and> c (f i) = f (i + 1))) 
10251  27 
then arbitrary 
28 
else if b s then while_aux (b, c, c s) 

29 
else s)" 

30 

10774  31 
recdef_tc while_aux_tc: while_aux 
32 
apply (rule wf_same_fst) 

33 
apply (rule wf_same_fst) 

34 
apply (simp add: wf_iff_no_infinite_down_chain) 

35 
apply blast 

36 
done 

37 

10251  38 
constdefs 
39 
while :: "('a => bool) => ('a => 'a) => 'a => 'a" 

40 
"while b c s == while_aux (b, c, s)" 

41 

42 
lemma while_aux_unfold: 

43 
"while_aux (b, c, s) = 

11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11626
diff
changeset

44 
(if \<exists>f. f (0::nat) = s \<and> (\<forall>i. b (f i) \<and> c (f i) = f (i + 1)) 
10251  45 
then arbitrary 
46 
else if b s then while_aux (b, c, c s) 

47 
else s)" 

48 
apply (rule while_aux_tc [THEN while_aux.simps [THEN trans]]) 

49 
apply (rule refl) 

50 
done 

51 

52 
text {* 

53 
The recursion equation for @{term while}: directly executable! 

54 
*} 

55 

12791
ccc0f45ad2c4
registered directly executable version with the code generator
kleing
parents:
11914
diff
changeset

56 
theorem while_unfold [code]: 
10251  57 
"while b c s = (if b s then while b c (c s) else s)" 
58 
apply (unfold while_def) 

59 
apply (rule while_aux_unfold [THEN trans]) 

60 
apply auto 

61 
apply (subst while_aux_unfold) 

62 
apply simp 

63 
apply clarify 

64 
apply (erule_tac x = "\<lambda>i. f (Suc i)" in allE) 

65 
apply blast 

66 
done 

67 

10984  68 
hide const while_aux 
69 

14300  70 
lemma def_while_unfold: assumes fdef: "f == while test do" 
71 
shows "f x = (if test x then f(do x) else x)" 

72 
proof  

73 
have "f x = while test do x" using fdef by simp 

74 
also have "\<dots> = (if test x then while test do (do x) else x)" 

75 
by(rule while_unfold) 

76 
also have "\<dots> = (if test x then f(do x) else x)" by(simp add:fdef[symmetric]) 

77 
finally show ?thesis . 

78 
qed 

79 

80 

10251  81 
text {* 
82 
The proof rule for @{term while}, where @{term P} is the invariant. 

83 
*} 

84 

10653  85 
theorem while_rule_lemma[rule_format]: 
10984  86 
"[ !!s. P s ==> b s ==> P (c s); 
87 
!!s. P s ==> \<not> b s ==> Q s; 

88 
wf {(t, s). P s \<and> b s \<and> t = c s} ] ==> 

10251  89 
P s > Q (while b c s)" 
90 
proof  

11549  91 
case rule_context 
10251  92 
assume wf: "wf {(t, s). P s \<and> b s \<and> t = c s}" 
93 
show ?thesis 

94 
apply (induct s rule: wf [THEN wf_induct]) 

95 
apply simp 

96 
apply clarify 

97 
apply (subst while_unfold) 

11549  98 
apply (simp add: rule_context) 
10251  99 
done 
100 
qed 

101 

10653  102 
theorem while_rule: 
10984  103 
"[ P s; 
104 
!!s. [ P s; b s ] ==> P (c s); 

105 
!!s. [ P s; \<not> b s ] ==> Q s; 

10997  106 
wf r; 
10984  107 
!!s. [ P s; b s ] ==> (c s, s) \<in> r ] ==> 
108 
Q (while b c s)" 

10653  109 
apply (rule while_rule_lemma) 
110 
prefer 4 apply assumption 

111 
apply blast 

112 
apply blast 

113 
apply(erule wf_subset) 

114 
apply blast 

115 
done 

116 

10984  117 
text {* 
118 
\medskip An application: computation of the @{term lfp} on finite 

119 
sets via iteration. 

120 
*} 

121 

122 
theorem lfp_conv_while: 

123 
"[ mono f; finite U; f U = U ] ==> 

124 
lfp f = fst (while (\<lambda>(A, fA). A \<noteq> fA) (\<lambda>(A, fA). (fA, f fA)) ({}, f {}))" 

125 
apply (rule_tac P = "\<lambda>(A, B). (A \<subseteq> U \<and> B = f A \<and> A \<subseteq> B \<and> B \<subseteq> lfp f)" and 

11047  126 
r = "((Pow U \<times> UNIV) \<times> (Pow U \<times> UNIV)) \<inter> 
10984  127 
inv_image finite_psubset (op  U o fst)" in while_rule) 
128 
apply (subst lfp_unfold) 

129 
apply assumption 

130 
apply (simp add: monoD) 

131 
apply (subst lfp_unfold) 

132 
apply assumption 

133 
apply clarsimp 

134 
apply (blast dest: monoD) 

135 
apply (fastsimp intro!: lfp_lowerbound) 

136 
apply (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset]) 

137 
apply (clarsimp simp add: inv_image_def finite_psubset_def order_less_le) 

138 
apply (blast intro!: finite_Diff dest: monoD) 

139 
done 

140 

141 

142 
text {* 

14589  143 
An example of using the @{term while} combinator. 
10984  144 
*} 
145 

15197  146 
text{* Cannot use @{thm[source]set_eq_subset} because it leads to 
147 
looping because the antisymmetry simproc turns the subset relationship 

148 
back into equality. *} 

149 

150 
lemma seteq: "(A = B) = ((!a : A. a:B) & (!b:B. b:A))" 

151 
by blast 

152 

14589  153 
theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6  n. n \<in> N})) = 
154 
P {0, 4, 2}" 

10997  155 
proof  
156 
have aux: "!!f A B. {f n  n. A n \<or> B n} = {f n  n. A n} \<union> {f n  n. B n}" 

10984  157 
apply blast 
10997  158 
done 
159 
show ?thesis 

11914  160 
apply (subst lfp_conv_while [where ?U = "{0, 1, 2, 3, 4, 5}"]) 
10997  161 
apply (rule monoI) 
162 
apply blast 

163 
apply simp 

164 
apply (simp add: aux set_eq_subset) 

165 
txt {* The fixpoint computation is performed purely by rewriting: *} 

15197  166 
apply (simp add: while_unfold aux seteq del: subset_empty) 
10997  167 
done 
168 
qed 

10251  169 

170 
end 