10251

1 


2 
header {* \title{} *}


3 


4 
theory While_Combinator_Example = While_Combinator:


5 


6 
text {*


7 
An example of using the @{term while} combinator.


8 
*}


9 


10 
lemma aux: "{f n n. A n \<or> B n} = {f n n. A n} \<union> {f n n. B n}"


11 
apply blast


12 
done


13 


14 
theorem "P (lfp (\<lambda>N::int set. {#0} \<union> {(n + #2) mod #6 n. n \<in> N})) =


15 
P {#0, #4, #2}"


16 
apply (subst lfp_conv_while [where ?U = "{#0, #1, #2, #3, #4, #5}"])


17 
apply (rule monoI)


18 
apply blast


19 
apply simp


20 
apply (simp add: aux set_eq_subset)


21 
txt {* The fixpoint computation is performed purely by rewriting: *}


22 
apply (simp add: while_unfold aux set_eq_subset del: subset_empty)


23 
done


24 


25 
end
