author | blanchet |
Wed, 24 Sep 2014 15:45:55 +0200 | |
changeset 58425 | 246985c6b20b |
parent 42151 | 4da4fc77664b |
child 58880 | 0baae4311a9f |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/ex/Loop.thy |
1479 | 2 |
Author: Franz Regensburger |
244 | 3 |
*) |
4 |
||
17291 | 5 |
header {* Theory for a loop primitive like while *} |
244 | 6 |
|
17291 | 7 |
theory Loop |
8 |
imports HOLCF |
|
9 |
begin |
|
244 | 10 |
|
19763 | 11 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
12 |
step :: "('a -> tr)->('a -> 'a)->'a->'a" where |
40322
707eb30e8a53
make syntax of continuous if-then-else consistent with HOL if-then-else
huffman
parents:
40028
diff
changeset
|
13 |
"step = (LAM b g x. If b$x then g$x else x)" |
19742 | 14 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
15 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
16 |
while :: "('a -> tr)->('a -> 'a)->'a->'a" where |
40322
707eb30e8a53
make syntax of continuous if-then-else consistent with HOL if-then-else
huffman
parents:
40028
diff
changeset
|
17 |
"while = (LAM b g. fix$(LAM f x. If b$x then f$(g$x) else x))" |
244 | 18 |
|
19742 | 19 |
(* ------------------------------------------------------------------------- *) |
20 |
(* access to definitions *) |
|
21 |
(* ------------------------------------------------------------------------- *) |
|
22 |
||
23 |
||
40322
707eb30e8a53
make syntax of continuous if-then-else consistent with HOL if-then-else
huffman
parents:
40028
diff
changeset
|
24 |
lemma step_def2: "step$b$g$x = If b$x then g$x else x" |
19742 | 25 |
apply (unfold step_def) |
26 |
apply simp |
|
27 |
done |
|
28 |
||
40322
707eb30e8a53
make syntax of continuous if-then-else consistent with HOL if-then-else
huffman
parents:
40028
diff
changeset
|
29 |
lemma while_def2: "while$b$g = fix$(LAM f x. If b$x then f$(g$x) else x)" |
19742 | 30 |
apply (unfold while_def) |
31 |
apply simp |
|
32 |
done |
|
33 |
||
34 |
||
35 |
(* ------------------------------------------------------------------------- *) |
|
36 |
(* rekursive properties of while *) |
|
37 |
(* ------------------------------------------------------------------------- *) |
|
38 |
||
40322
707eb30e8a53
make syntax of continuous if-then-else consistent with HOL if-then-else
huffman
parents:
40028
diff
changeset
|
39 |
lemma while_unfold: "while$b$g$x = If b$x then while$b$g$(g$x) else x" |
19742 | 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) |
|
40429 | 50 |
apply (rule while_unfold) |
19742 | 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) |
|
40429 | 59 |
apply (erule strictI) |
19742 | 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) |
|
40028 | 104 |
apply (simp add: step_def2) |
105 |
apply (simp (no_asm_simp)) |
|
19742 | 106 |
apply (rule mp) |
107 |
apply (erule spec) |
|
40028 | 108 |
apply (simp (no_asm_simp) del: iterate_Suc add: loop_lemma2) |
19742 | 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) |
|
35170 | 113 |
apply (drule (1) loop_lemma2, simp) |
19742 | 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) |
|
35948 | 136 |
apply simp |
137 |
apply simp |
|
19742 | 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 |
|
244 | 198 |
|
199 |
end |
|
17291 | 200 |