1479
|
1 |
(* Title: HOLCF/ex/Loop.thy
|
244
|
2 |
ID: $Id$
|
1479
|
3 |
Author: Franz Regensburger
|
244
|
4 |
*)
|
|
5 |
|
17291
|
6 |
header {* Theory for a loop primitive like while *}
|
244
|
7 |
|
17291
|
8 |
theory Loop
|
|
9 |
imports HOLCF
|
|
10 |
begin
|
244
|
11 |
|
19763
|
12 |
definition
|
17291
|
13 |
step :: "('a -> tr)->('a -> 'a)->'a->'a"
|
19763
|
14 |
"step = (LAM b g x. If b$x then g$x else x fi)"
|
19742
|
15 |
|
17291
|
16 |
while :: "('a -> tr)->('a -> 'a)->'a->'a"
|
19763
|
17 |
"while = (LAM b g. fix$(LAM f x. If b$x then f$(g$x) else x fi))"
|
244
|
18 |
|
19742
|
19 |
(* ------------------------------------------------------------------------- *)
|
|
20 |
(* access to definitions *)
|
|
21 |
(* ------------------------------------------------------------------------- *)
|
|
22 |
|
|
23 |
|
|
24 |
lemma step_def2: "step$b$g$x = If b$x then g$x else x fi"
|
|
25 |
apply (unfold step_def)
|
|
26 |
apply simp
|
|
27 |
done
|
|
28 |
|
|
29 |
lemma while_def2: "while$b$g = fix$(LAM f x. If b$x then f$(g$x) else x fi)"
|
|
30 |
apply (unfold while_def)
|
|
31 |
apply simp
|
|
32 |
done
|
|
33 |
|
|
34 |
|
|
35 |
(* ------------------------------------------------------------------------- *)
|
|
36 |
(* rekursive properties of while *)
|
|
37 |
(* ------------------------------------------------------------------------- *)
|
|
38 |
|
|
39 |
lemma while_unfold: "while$b$g$x = If b$x then while$b$g$(g$x) else x fi"
|
|
40 |
apply (rule trans)
|
|
41 |
apply (rule while_def2 [THEN fix_eq5])
|
|
42 |
apply simp
|
|
43 |
done
|
|
44 |
|
|
45 |
lemma while_unfold2: "ALL x. while$b$g$x = while$b$g$(iterate k$(step$b$g)$x)"
|
|
46 |
apply (induct_tac k)
|
|
47 |
apply simp
|
|
48 |
apply (rule allI)
|
|
49 |
apply (rule trans)
|
|
50 |
apply (subst while_unfold)
|
|
51 |
apply (rule_tac [2] refl)
|
|
52 |
apply (subst iterate_Suc2)
|
|
53 |
apply (rule trans)
|
|
54 |
apply (erule_tac [2] spec)
|
|
55 |
apply (subst step_def2)
|
|
56 |
apply (rule_tac p = "b$x" in trE)
|
|
57 |
apply simp
|
|
58 |
apply (subst while_unfold)
|
|
59 |
apply (rule_tac s = "UU" and t = "b$UU" in ssubst)
|
|
60 |
apply (erule flat_codom [THEN disjE])
|
|
61 |
apply assumption
|
|
62 |
apply (erule spec)
|
|
63 |
apply simp
|
|
64 |
apply simp
|
|
65 |
apply simp
|
|
66 |
apply (subst while_unfold)
|
|
67 |
apply simp
|
|
68 |
done
|
|
69 |
|
|
70 |
lemma while_unfold3: "while$b$g$x = while$b$g$(step$b$g$x)"
|
|
71 |
apply (rule_tac s = "while$b$g$ (iterate (Suc 0) $ (step$b$g) $x) " in trans)
|
|
72 |
apply (rule while_unfold2 [THEN spec])
|
|
73 |
apply simp
|
|
74 |
done
|
|
75 |
|
|
76 |
|
|
77 |
(* ------------------------------------------------------------------------- *)
|
|
78 |
(* properties of while and iterations *)
|
|
79 |
(* ------------------------------------------------------------------------- *)
|
|
80 |
|
|
81 |
lemma loop_lemma1: "[| EX y. b$y=FF; iterate k$(step$b$g)$x = UU |]
|
|
82 |
==>iterate(Suc k)$(step$b$g)$x=UU"
|
|
83 |
apply (simp (no_asm))
|
|
84 |
apply (rule trans)
|
|
85 |
apply (rule step_def2)
|
|
86 |
apply simp
|
|
87 |
apply (erule exE)
|
|
88 |
apply (erule flat_codom [THEN disjE])
|
|
89 |
apply simp_all
|
|
90 |
done
|
|
91 |
|
|
92 |
lemma loop_lemma2: "[|EX y. b$y=FF;iterate (Suc k)$(step$b$g)$x ~=UU |]==>
|
|
93 |
iterate k$(step$b$g)$x ~=UU"
|
|
94 |
apply (blast intro: loop_lemma1)
|
|
95 |
done
|
|
96 |
|
|
97 |
lemma loop_lemma3 [rule_format (no_asm)]:
|
|
98 |
"[| ALL x. INV x & b$x=TT & g$x~=UU --> INV (g$x);
|
|
99 |
EX y. b$y=FF; INV x |]
|
|
100 |
==> iterate k$(step$b$g)$x ~=UU --> INV (iterate k$(step$b$g)$x)"
|
|
101 |
apply (induct_tac "k")
|
|
102 |
apply (simp (no_asm_simp))
|
|
103 |
apply (intro strip)
|
|
104 |
apply (simp (no_asm) add: step_def2)
|
|
105 |
apply (rule_tac p = "b$ (iterate n$ (step$b$g) $x) " in trE)
|
|
106 |
apply (erule notE)
|
|
107 |
apply (tactic {* asm_simp_tac (HOLCF_ss addsimps [thm "step_def2"]) 1 *})
|
|
108 |
apply (tactic "asm_simp_tac HOLCF_ss 1")
|
|
109 |
apply (rule mp)
|
|
110 |
apply (erule spec)
|
|
111 |
apply (tactic {* asm_simp_tac (HOLCF_ss delsimps [thm "iterate_Suc"]
|
|
112 |
addsimps [thm "loop_lemma2"]) 1 *})
|
|
113 |
apply (rule_tac s = "iterate (Suc n) $ (step$b$g) $x"
|
|
114 |
and t = "g$ (iterate n$ (step$b$g) $x) " in ssubst)
|
|
115 |
prefer 2 apply (assumption)
|
|
116 |
apply (simp add: step_def2)
|
|
117 |
apply (simp del: iterate_Suc add: loop_lemma2)
|
|
118 |
done
|
|
119 |
|
|
120 |
lemma loop_lemma4 [rule_format]:
|
|
121 |
"ALL x. b$(iterate k$(step$b$g)$x)=FF --> while$b$g$x= iterate k$(step$b$g)$x"
|
|
122 |
apply (induct_tac k)
|
|
123 |
apply (simp (no_asm))
|
|
124 |
apply (intro strip)
|
|
125 |
apply (simplesubst while_unfold)
|
|
126 |
apply simp
|
|
127 |
apply (rule allI)
|
|
128 |
apply (simplesubst iterate_Suc2)
|
|
129 |
apply (intro strip)
|
|
130 |
apply (rule trans)
|
|
131 |
apply (rule while_unfold3)
|
|
132 |
apply simp
|
|
133 |
done
|
|
134 |
|
|
135 |
lemma loop_lemma5 [rule_format (no_asm)]:
|
|
136 |
"ALL k. b$(iterate k$(step$b$g)$x) ~= FF ==>
|
|
137 |
ALL m. while$b$g$(iterate m$(step$b$g)$x)=UU"
|
|
138 |
apply (simplesubst while_def2)
|
|
139 |
apply (rule fix_ind)
|
|
140 |
apply (rule allI [THEN adm_all])
|
|
141 |
apply (rule adm_eq)
|
|
142 |
apply (tactic "cont_tacR 1")
|
|
143 |
apply (simp (no_asm))
|
|
144 |
apply (rule allI)
|
|
145 |
apply (simp (no_asm))
|
|
146 |
apply (rule_tac p = "b$ (iterate m$ (step$b$g) $x) " in trE)
|
|
147 |
apply (simp (no_asm_simp))
|
|
148 |
apply (simp (no_asm_simp))
|
|
149 |
apply (rule_tac s = "xa$ (iterate (Suc m) $ (step$b$g) $x) " in trans)
|
|
150 |
apply (erule_tac [2] spec)
|
|
151 |
apply (rule cfun_arg_cong)
|
|
152 |
apply (rule trans)
|
|
153 |
apply (rule_tac [2] iterate_Suc [symmetric])
|
|
154 |
apply (simp add: step_def2)
|
|
155 |
apply blast
|
|
156 |
done
|
|
157 |
|
|
158 |
lemma loop_lemma6: "ALL k. b$(iterate k$(step$b$g)$x) ~= FF ==> while$b$g$x=UU"
|
|
159 |
apply (rule_tac t = "x" in iterate_0 [THEN subst])
|
|
160 |
apply (erule loop_lemma5)
|
|
161 |
done
|
|
162 |
|
|
163 |
lemma loop_lemma7: "while$b$g$x ~= UU ==> EX k. b$(iterate k$(step$b$g)$x) = FF"
|
|
164 |
apply (blast intro: loop_lemma6)
|
|
165 |
done
|
|
166 |
|
|
167 |
|
|
168 |
(* ------------------------------------------------------------------------- *)
|
|
169 |
(* an invariant rule for loops *)
|
|
170 |
(* ------------------------------------------------------------------------- *)
|
|
171 |
|
|
172 |
lemma loop_inv2:
|
|
173 |
"[| (ALL y. INV y & b$y=TT & g$y ~= UU --> INV (g$y));
|
|
174 |
(ALL y. INV y & b$y=FF --> Q y);
|
|
175 |
INV x; while$b$g$x~=UU |] ==> Q (while$b$g$x)"
|
|
176 |
apply (rule_tac P = "%k. b$ (iterate k$ (step$b$g) $x) =FF" in exE)
|
|
177 |
apply (erule loop_lemma7)
|
|
178 |
apply (simplesubst loop_lemma4)
|
|
179 |
apply assumption
|
|
180 |
apply (drule spec, erule mp)
|
|
181 |
apply (rule conjI)
|
|
182 |
prefer 2 apply (assumption)
|
|
183 |
apply (rule loop_lemma3)
|
|
184 |
apply assumption
|
|
185 |
apply (blast intro: loop_lemma6)
|
|
186 |
apply assumption
|
|
187 |
apply (rotate_tac -1)
|
|
188 |
apply (simp add: loop_lemma4)
|
|
189 |
done
|
|
190 |
|
|
191 |
lemma loop_inv:
|
|
192 |
assumes premP: "P(x)"
|
|
193 |
and premI: "!!y. P y ==> INV y"
|
|
194 |
and premTT: "!!y. [| INV y; b$y=TT; g$y~=UU|] ==> INV (g$y)"
|
|
195 |
and premFF: "!!y. [| INV y; b$y=FF|] ==> Q y"
|
|
196 |
and premW: "while$b$g$x ~= UU"
|
|
197 |
shows "Q (while$b$g$x)"
|
|
198 |
apply (rule loop_inv2)
|
|
199 |
apply (rule_tac [3] premP [THEN premI])
|
|
200 |
apply (rule_tac [3] premW)
|
|
201 |
apply (blast intro: premTT)
|
|
202 |
apply (blast intro: premFF)
|
|
203 |
done
|
244
|
204 |
|
|
205 |
end
|
17291
|
206 |
|