src/HOL/Library/While_Combinator_Example.thy

A general ``while'' combinator (from main HOL);

header {* \title{} *}

theory While_Combinator_Example = While_Combinator:

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

lemma aux: "{f n| n. A n \<or> B n} = {f n| n. A n} \<union> {f n| n. B n}"
  apply blast
  done

theorem "P (lfp (\<lambda>N::int set. {#0} \<union> {(n + #2) mod #6| n. n \<in> N})) =
    P {#0, #4, #2}"
  apply (subst lfp_conv_while [where ?U = "{#0, #1, #2, #3, #4, #5}"])
     apply (rule monoI)
    apply blast
   apply simp
  apply (simp add: aux set_eq_subset)
  txt {* The fixpoint computation is performed purely by rewriting: *}
  apply (simp add: while_unfold aux set_eq_subset del: subset_empty)
  done

end