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