Quelle While_Combinator_Example.thy Sprache: Isabelle

(*  Title:      HOL/ex/While_Combinator_Example.thy
    Author:     Tobias Nipkow
    Copyright   2000 TU Muenchen
*)

section \<open>An application of the While combinator\<close>

theory While_Combinator_Example
imports "HOL-Library.While_Combinator"
begin

text \<open>Computation of the \<^term>\<open>lfp\<close> on finite sets via
  iteration.\<close>

theorem lfp_conv_while:
  "[| mono f; finite U; f U = U |] ==>
    lfp f = fst (while (\<lambda>(A, fA). A \<noteq> fA) (\<lambda>(A, fA). (fA, f fA)) ({}, f {}))"
apply (rule_tac P = "\(A, B). (A \ U \ B = f A \ A \ B \ B \ lfp f)" and
                r = "((Pow U \ UNIV) \ (Pow U \ UNIV)) \
                     inv_image finite_psubset ((-) U o fst)" in while_rule)
   apply (subst lfp_unfold)
    apply assumption
   apply (simp add: monoD)
  apply (subst lfp_unfold)
   apply assumption
  apply clarsimp
  apply (blast dest: monoD)
apply (fastforce intro!: lfp_lowerbound)
apply (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset])
apply (clarsimp simp add: finite_psubset_def order_less_le)
apply (blast dest: monoD)
done

subsection \<open>Example\<close>

text\<open>Cannot use @{thm[source]set_eq_subset} because it leads to
looping because the antisymmetry simproc turns the subset relationship
back into equality.\<close>

theorem "P (lfp (\N::int set. {0} \ {(n + 2) mod 6 | n. n \ N})) =
  P {0, 4, 2}"
proof -
  have seteq: "\A B. (A = B) = ((\a \ A. a\B) \ (\b\B. b\A))"
    by blast
  have aux: "\f A B. {f n | n. A n \ B n} = {f n | n. A n} \ {f n | n. B n}"
    apply blast
    done
  show ?thesis
    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 \<open>The fixpoint computation is performed purely by rewriting:\<close>
    apply (simp add: while_unfold aux seteq del: subset_empty)
    done
qed

end

quality100%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.