78 |
78 |
79 lemma funpow_commute: |
79 lemma funpow_commute: |
80 "\<lbrakk>\<forall>k' < k. f (c ((c^^k') s)) = c' (f ((c^^k') s))\<rbrakk> \<Longrightarrow> f ((c^^k) s) = (c'^^k) (f s)" |
80 "\<lbrakk>\<forall>k' < k. f (c ((c^^k') s)) = c' (f ((c^^k') s))\<rbrakk> \<Longrightarrow> f ((c^^k) s) = (c'^^k) (f s)" |
81 by (induct k arbitrary: s) auto |
81 by (induct k arbitrary: s) auto |
82 |
82 |
83 lemma while_option_commute: |
83 lemma while_option_commute_invariant: |
84 assumes "\<And>s. b s = b' (f s)" "\<And>s. \<lbrakk>b s\<rbrakk> \<Longrightarrow> f (c s) = c' (f s)" |
84 assumes Invariant: "\<And>s. P s \<Longrightarrow> b s \<Longrightarrow> P (c s)" |
85 shows "Option.map f (while_option b c s) = while_option b' c' (f s)" |
85 assumes TestCommute: "\<And>s. P s \<Longrightarrow> b s = b' (f s)" |
|
86 assumes BodyCommute: "\<And>s. P s \<Longrightarrow> b s \<Longrightarrow> f (c s) = c' (f s)" |
|
87 assumes Initial: "P s" |
|
88 shows "Option.map f (while_option b c s) = while_option b' c' (f s)" |
86 unfolding while_option_def |
89 unfolding while_option_def |
87 proof (rule trans[OF if_distrib if_cong], safe, unfold option.inject) |
90 proof (rule trans[OF if_distrib if_cong], safe, unfold option.inject) |
88 fix k assume "\<not> b ((c ^^ k) s)" |
91 fix k |
89 thus "\<exists>k. \<not> b' ((c' ^^ k) (f s))" |
92 assume "\<not> b ((c ^^ k) s)" |
|
93 with Initial show "\<exists>k. \<not> b' ((c' ^^ k) (f s))" |
90 proof (induction k arbitrary: s) |
94 proof (induction k arbitrary: s) |
91 case 0 thus ?case by (auto simp: assms(1) intro: exI[of _ 0]) |
95 case 0 thus ?case by (auto simp: TestCommute intro: exI[of _ 0]) |
92 next |
96 next |
93 case (Suc k) |
97 case (Suc k) thus ?case |
94 hence "\<not> b ((c^^k) (c s))" by (auto simp: funpow_swap1) |
98 proof (cases "b s") |
95 from Suc.IH[OF this] obtain k where "\<not> b' ((c' ^^ k) (f (c s)))" .. |
99 assume "b s" |
96 with assms show ?case |
100 with Suc.IH[of "c s"] Suc.prems show ?thesis |
97 by (cases "b s") (auto simp: funpow_swap1 intro: exI[of _ "Suc k"] exI[of _ "0"]) |
101 by (metis BodyCommute Invariant comp_apply funpow.simps(2) funpow_swap1) |
|
102 next |
|
103 assume "\<not> b s" |
|
104 with Suc show ?thesis by (auto simp: TestCommute intro: exI [of _ 0]) |
|
105 qed |
98 qed |
106 qed |
99 next |
107 next |
100 fix k assume "\<not> b' ((c' ^^ k) (f s))" |
108 fix k |
101 thus "\<exists>k. \<not> b ((c ^^ k) s)" |
109 assume "\<not> b' ((c' ^^ k) (f s))" |
|
110 with Initial show "\<exists>k. \<not> b ((c ^^ k) s)" |
102 proof (induction k arbitrary: s) |
111 proof (induction k arbitrary: s) |
103 case 0 thus ?case by (auto simp: assms(1) intro: exI[of _ 0]) |
112 case 0 thus ?case by (auto simp: TestCommute intro: exI[of _ 0]) |
104 next |
113 next |
105 case (Suc k) |
114 case (Suc k) thus ?case |
106 hence *: "\<not> b' ((c'^^k) (c' (f s)))" by (auto simp: funpow_swap1) |
|
107 show ?case |
|
108 proof (cases "b s") |
115 proof (cases "b s") |
109 case True |
116 assume "b s" |
110 with assms(2) * have "\<not> b' ((c'^^k) (f (c s)))" by simp |
117 with Suc.IH[of "c s"] Suc.prems show ?thesis |
111 from Suc.IH[OF this] obtain k where "\<not> b ((c ^^ k) (c s))" .. |
118 by (metis BodyCommute Invariant comp_apply funpow.simps(2) funpow_swap1) |
112 thus ?thesis by (auto simp: funpow_swap1 intro: exI[of _ "Suc k"]) |
119 next |
113 qed (auto intro: exI[of _ "0"]) |
120 assume "\<not> b s" |
|
121 with Suc show ?thesis by (auto simp: TestCommute intro: exI [of _ 0]) |
|
122 qed |
114 qed |
123 qed |
115 next |
124 next |
116 fix k assume k: "\<not> b' ((c' ^^ k) (f s))" |
125 fix k |
117 have *: "(LEAST k. \<not> b' ((c' ^^ k) (f s))) = (LEAST k. \<not> b ((c ^^ k) s))" (is "?k' = ?k") |
126 assume k: "\<not> b' ((c' ^^ k) (f s))" |
|
127 have *: "(LEAST k. \<not> b' ((c' ^^ k) (f s))) = (LEAST k. \<not> b ((c ^^ k) s))" |
|
128 (is "?k' = ?k") |
118 proof (cases ?k') |
129 proof (cases ?k') |
119 case 0 |
130 case 0 |
120 have "\<not> b' ((c'^^0) (f s))" unfolding 0[symmetric] by (rule LeastI[of _ k]) (rule k) |
131 have "\<not> b' ((c' ^^ 0) (f s))" |
121 hence "\<not> b s" unfolding assms(1) by simp |
132 unfolding 0[symmetric] by (rule LeastI[of _ k]) (rule k) |
|
133 hence "\<not> b s" by (auto simp: TestCommute Initial) |
122 hence "?k = 0" by (intro Least_equality) auto |
134 hence "?k = 0" by (intro Least_equality) auto |
123 with 0 show ?thesis by auto |
135 with 0 show ?thesis by auto |
124 next |
136 next |
125 case (Suc k') |
137 case (Suc k') |
126 have "\<not> b' ((c'^^Suc k') (f s))" unfolding Suc[symmetric] by (rule LeastI) (rule k) |
138 have "\<not> b' ((c' ^^ Suc k') (f s))" |
|
139 unfolding Suc[symmetric] by (rule LeastI) (rule k) |
127 moreover |
140 moreover |
128 { fix k assume "k \<le> k'" |
141 { fix k assume "k \<le> k'" |
129 hence "k < ?k'" unfolding Suc by simp |
142 hence "k < ?k'" unfolding Suc by simp |
130 hence "b' ((c' ^^ k) (f s))" by (rule iffD1[OF not_not, OF not_less_Least]) |
143 hence "b' ((c' ^^ k) (f s))" by (rule iffD1[OF not_not, OF not_less_Least]) |
131 } note b' = this |
144 } |
|
145 note b' = this |
132 { fix k assume "k \<le> k'" |
146 { fix k assume "k \<le> k'" |
133 hence "f ((c ^^ k) s) = (c'^^k) (f s)" by (induct k) (auto simp: b' assms) |
147 hence "f ((c ^^ k) s) = (c' ^^ k) (f s)" |
134 with `k \<le> k'` have "b ((c^^k) s)" |
148 and "b ((c ^^ k) s) = b' ((c' ^^ k) (f s))" |
135 proof (induct k) |
149 and "P ((c ^^ k) s)" |
136 case (Suc k) thus ?case unfolding assms(1) by (simp only: b') |
150 by (induct k) (auto simp: b' assms) |
137 qed (simp add: b'[of 0, simplified] assms(1)) |
151 with `k \<le> k'` |
138 } note b = this |
152 have "b ((c ^^ k) s)" |
139 hence k': "f ((c^^k') s) = (c'^^k') (f s)" by (induct k') (auto simp: assms(2)) |
153 and "f ((c ^^ k) s) = (c' ^^ k) (f s)" |
|
154 and "P ((c ^^ k) s)" |
|
155 by (auto simp: b') |
|
156 } |
|
157 note b = this(1) and body = this(2) and inv = this(3) |
|
158 hence k': "f ((c ^^ k') s) = (c' ^^ k') (f s)" by auto |
140 ultimately show ?thesis unfolding Suc using b |
159 ultimately show ?thesis unfolding Suc using b |
141 by (intro sym[OF Least_equality]) |
160 proof (intro Least_equality[symmetric]) |
142 (auto simp add: assms(1) assms(2)[OF b] k' not_less_eq_eq[symmetric]) |
161 case goal1 |
|
162 hence Test: "\<not> b' (f ((c ^^ Suc k') s))" |
|
163 by (auto simp: BodyCommute inv b) |
|
164 have "P ((c ^^ Suc k') s)" by (auto simp: Invariant inv b) |
|
165 with Test show ?case by (auto simp: TestCommute) |
|
166 next |
|
167 case goal2 thus ?case by (metis not_less_eq_eq) |
|
168 qed |
143 qed |
169 qed |
144 have "f ((c ^^ ?k) s) = (c' ^^ ?k') (f s)" unfolding * |
170 have "f ((c ^^ ?k) s) = (c' ^^ ?k') (f s)" unfolding * |
145 by (auto intro: funpow_commute assms(2) dest: not_less_Least) |
171 proof (rule funpow_commute, clarify) |
|
172 fix k assume "k < ?k" |
|
173 hence TestTrue: "b ((c ^^ k) s)" by (auto dest: not_less_Least) |
|
174 from `k < ?k` have "P ((c ^^ k) s)" |
|
175 proof (induct k) |
|
176 case 0 thus ?case by (auto simp: assms) |
|
177 next |
|
178 case (Suc h) |
|
179 hence "P ((c ^^ h) s)" by auto |
|
180 with Suc show ?case |
|
181 by (auto, metis (lifting, no_types) Invariant Suc_lessD not_less_Least) |
|
182 qed |
|
183 with TestTrue show "f (c ((c ^^ k) s)) = c' (f ((c ^^ k) s))" |
|
184 by (metis BodyCommute) |
|
185 qed |
146 thus "\<exists>z. (c ^^ ?k) s = z \<and> f z = (c' ^^ ?k') (f s)" by blast |
186 thus "\<exists>z. (c ^^ ?k) s = z \<and> f z = (c' ^^ ?k') (f s)" by blast |
147 qed |
187 qed |
|
188 |
|
189 lemma while_option_commute: |
|
190 assumes "\<And>s. b s = b' (f s)" "\<And>s. \<lbrakk>b s\<rbrakk> \<Longrightarrow> f (c s) = c' (f s)" |
|
191 shows "Option.map f (while_option b c s) = while_option b' c' (f s)" |
|
192 by(rule while_option_commute_invariant[where P = "\<lambda>_. True"]) |
|
193 (auto simp add: assms) |
148 |
194 |
149 subsection {* Total version *} |
195 subsection {* Total version *} |
150 |
196 |
151 definition while :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" |
197 definition while :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" |
152 where "while b c s = the (while_option b c s)" |
198 where "while b c s = the (while_option b c s)" |
197 theorem wf_while_option_Some: |
243 theorem wf_while_option_Some: |
198 assumes "wf {(t, s). (P s \<and> b s) \<and> t = c s}" |
244 assumes "wf {(t, s). (P s \<and> b s) \<and> t = c s}" |
199 and "!!s. P s \<Longrightarrow> b s \<Longrightarrow> P(c s)" and "P s" |
245 and "!!s. P s \<Longrightarrow> b s \<Longrightarrow> P(c s)" and "P s" |
200 shows "EX t. while_option b c s = Some t" |
246 shows "EX t. while_option b c s = Some t" |
201 using assms(1,3) |
247 using assms(1,3) |
202 apply (induct s) |
248 proof (induction s) |
203 using assms(2) |
249 case less thus ?case using assms(2) |
204 apply (subst while_option_unfold) |
250 by (subst while_option_unfold) simp |
205 apply simp |
251 qed |
206 done |
252 |
|
253 lemma wf_rel_while_option_Some: |
|
254 assumes wf: "wf R" |
|
255 assumes smaller: "\<And>s. P s \<and> b s \<Longrightarrow> (c s, s) \<in> R" |
|
256 assumes inv: "\<And>s. P s \<and> b s \<Longrightarrow> P(c s)" |
|
257 assumes init: "P s" |
|
258 shows "\<exists>t. while_option b c s = Some t" |
|
259 proof - |
|
260 from smaller have "{(t,s). P s \<and> b s \<and> t = c s} \<subseteq> R" by auto |
|
261 with wf have "wf {(t,s). P s \<and> b s \<and> t = c s}" by (auto simp: wf_subset) |
|
262 with inv init show ?thesis by (auto simp: wf_while_option_Some) |
|
263 qed |
207 |
264 |
208 theorem measure_while_option_Some: fixes f :: "'s \<Rightarrow> nat" |
265 theorem measure_while_option_Some: fixes f :: "'s \<Rightarrow> nat" |
209 shows "(!!s. P s \<Longrightarrow> b s \<Longrightarrow> P(c s) \<and> f(c s) < f s) |
266 shows "(!!s. P s \<Longrightarrow> b s \<Longrightarrow> P(c s) \<and> f(c s) < f s) |
210 \<Longrightarrow> P s \<Longrightarrow> EX t. while_option b c s = Some t" |
267 \<Longrightarrow> P s \<Longrightarrow> EX t. while_option b c s = Some t" |
211 by(blast intro: wf_while_option_Some[OF wf_if_measure, of P b f]) |
268 by(blast intro: wf_while_option_Some[OF wf_if_measure, of P b f]) |