312 fixes p :: "'a \<Rightarrow> bool" |
312 fixes p :: "'a \<Rightarrow> bool" |
313 and f :: "'a \<Rightarrow> 'a list" |
313 and f :: "'a \<Rightarrow> 'a list" |
314 and x :: 'a |
314 and x :: 'a |
315 begin |
315 begin |
316 |
316 |
317 fun rtrancl_while_test :: "'a list \<times> 'a set \<Rightarrow> bool" |
317 qualified fun rtrancl_while_test :: "'a list \<times> 'a set \<Rightarrow> bool" |
318 where "rtrancl_while_test (ws,_) = (ws \<noteq> [] \<and> p(hd ws))" |
318 where "rtrancl_while_test (ws,_) = (ws \<noteq> [] \<and> p(hd ws))" |
319 |
319 |
320 fun rtrancl_while_step :: "'a list \<times> 'a set \<Rightarrow> 'a list \<times> 'a set" |
320 qualified fun rtrancl_while_step :: "'a list \<times> 'a set \<Rightarrow> 'a list \<times> 'a set" |
321 where "rtrancl_while_step (ws, Z) = |
321 where "rtrancl_while_step (ws, Z) = |
322 (let x = hd ws; new = remdups (filter (\<lambda>y. y \<notin> Z) (f x)) |
322 (let x = hd ws; new = remdups (filter (\<lambda>y. y \<notin> Z) (f x)) |
323 in (new @ tl ws, set new \<union> Z))" |
323 in (new @ tl ws, set new \<union> Z))" |
324 |
324 |
325 definition rtrancl_while :: "('a list * 'a set) option" |
325 definition rtrancl_while :: "('a list * 'a set) option" |
326 where "rtrancl_while = while_option rtrancl_while_test rtrancl_while_step ([x],{x})" |
326 where "rtrancl_while = while_option rtrancl_while_test rtrancl_while_step ([x],{x})" |
327 |
327 |
328 fun rtrancl_while_invariant :: "'a list \<times> 'a set \<Rightarrow> bool" |
328 qualified fun rtrancl_while_invariant :: "'a list \<times> 'a set \<Rightarrow> bool" |
329 where "rtrancl_while_invariant (ws, Z) = |
329 where "rtrancl_while_invariant (ws, Z) = |
330 (x \<in> Z \<and> set ws \<subseteq> Z \<and> distinct ws \<and> {(x,y). y \<in> set(f x)} `` (Z - set ws) \<subseteq> Z \<and> |
330 (x \<in> Z \<and> set ws \<subseteq> Z \<and> distinct ws \<and> {(x,y). y \<in> set(f x)} `` (Z - set ws) \<subseteq> Z \<and> |
331 Z \<subseteq> {(x,y). y \<in> set(f x)}^* `` {x} \<and> (\<forall>z\<in>Z - set ws. p z))" |
331 Z \<subseteq> {(x,y). y \<in> set(f x)}^* `` {x} \<and> (\<forall>z\<in>Z - set ws. p z))" |
332 |
332 |
333 lemma rtrancl_while_invariant: |
333 qualified lemma rtrancl_while_invariant: |
334 assumes inv: "rtrancl_while_invariant st" and test: "rtrancl_while_test st" |
334 assumes inv: "rtrancl_while_invariant st" and test: "rtrancl_while_test st" |
335 shows "rtrancl_while_invariant (rtrancl_while_step st)" |
335 shows "rtrancl_while_invariant (rtrancl_while_step st)" |
336 proof (cases st) |
336 proof (cases st) |
337 fix ws Z assume st: "st = (ws, Z)" |
337 fix ws Z assume st: "st = (ws, Z)" |
338 with test obtain h t where "ws = h # t" "p h" by (cases ws) auto |
338 with test obtain h t where "ws = h # t" "p h" by (cases ws) auto |