1.1 --- a/src/HOL/IsaMakefile Fri Jul 09 17:00:42 2010 +0200
1.2 +++ b/src/HOL/IsaMakefile Fri Jul 09 17:15:03 2010 +0200
1.3 @@ -1006,7 +1006,8 @@
1.4 ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \
1.5 ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Sudoku.thy \
1.6 ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy ex/Tree23.thy \
1.7 - ex/Unification.thy ex/document/root.bib ex/document/root.tex \
1.8 + ex/Unification.thy ex/While_Combinator_Example.thy ex/document/root.bib \
1.9 + ex/document/root.tex \
1.10 ex/set.thy ex/svc_funcs.ML ex/svc_test.thy
1.11 @$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
1.12
2.1 --- a/src/HOL/Library/While_Combinator.thy Fri Jul 09 17:00:42 2010 +0200
2.2 +++ b/src/HOL/Library/While_Combinator.thy Fri Jul 09 17:15:03 2010 +0200
2.3 @@ -10,7 +10,7 @@
2.4 imports Main
2.5 begin
2.6
2.7 -subsection {* Option result *}
2.8 +subsection {* Partial version *}
2.9
2.10 definition while_option :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where
2.11 "while_option b c s = (if (\<exists>k. ~ b ((c ^^ k) s))
2.12 @@ -81,7 +81,7 @@
2.13 qed
2.14
2.15
2.16 -subsection {* Totalized version *}
2.17 +subsection {* Total version *}
2.18
2.19 definition while :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
2.20 where "while b c s = the (while_option b c s)"
2.21 @@ -127,54 +127,5 @@
2.22 apply blast
2.23 done
2.24
2.25 -text {*
2.26 - \medskip An application: computation of the @{term lfp} on finite
2.27 - sets via iteration.
2.28 -*}
2.29 -
2.30 -theorem lfp_conv_while:
2.31 - "[| mono f; finite U; f U = U |] ==>
2.32 - lfp f = fst (while (\<lambda>(A, fA). A \<noteq> fA) (\<lambda>(A, fA). (fA, f fA)) ({}, f {}))"
2.33 -apply (rule_tac P = "\<lambda>(A, B). (A \<subseteq> U \<and> B = f A \<and> A \<subseteq> B \<and> B \<subseteq> lfp f)" and
2.34 - r = "((Pow U \<times> UNIV) \<times> (Pow U \<times> UNIV)) \<inter>
2.35 - inv_image finite_psubset (op - U o fst)" in while_rule)
2.36 - apply (subst lfp_unfold)
2.37 - apply assumption
2.38 - apply (simp add: monoD)
2.39 - apply (subst lfp_unfold)
2.40 - apply assumption
2.41 - apply clarsimp
2.42 - apply (blast dest: monoD)
2.43 - apply (fastsimp intro!: lfp_lowerbound)
2.44 - apply (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset])
2.45 -apply (clarsimp simp add: finite_psubset_def order_less_le)
2.46 -apply (blast intro!: finite_Diff dest: monoD)
2.47 -done
2.48 -
2.49 -
2.50 -subsection {* Example *}
2.51 -
2.52 -text{* Cannot use @{thm[source]set_eq_subset} because it leads to
2.53 -looping because the antisymmetry simproc turns the subset relationship
2.54 -back into equality. *}
2.55 -
2.56 -theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) =
2.57 - P {0, 4, 2}"
2.58 -proof -
2.59 - have seteq: "!!A B. (A = B) = ((!a : A. a:B) & (!b:B. b:A))"
2.60 - by blast
2.61 - have aux: "!!f A B. {f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}"
2.62 - apply blast
2.63 - done
2.64 - show ?thesis
2.65 - apply (subst lfp_conv_while [where ?U = "{0, 1, 2, 3, 4, 5}"])
2.66 - apply (rule monoI)
2.67 - apply blast
2.68 - apply simp
2.69 - apply (simp add: aux set_eq_subset)
2.70 - txt {* The fixpoint computation is performed purely by rewriting: *}
2.71 - apply (simp add: while_unfold aux seteq del: subset_empty)
2.72 - done
2.73 -qed
2.74
2.75 end
3.1 --- a/src/HOL/ex/ROOT.ML Fri Jul 09 17:00:42 2010 +0200
3.2 +++ b/src/HOL/ex/ROOT.ML Fri Jul 09 17:15:03 2010 +0200
3.3 @@ -23,6 +23,7 @@
3.4 "InductiveInvariant_examples",
3.5 "LocaleTest2",
3.6 "Records",
3.7 + "While_Combinator_Example",
3.8 "MonoidGroup",
3.9 "BinEx",
3.10 "Hex_Bin_Examples",
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/HOL/ex/While_Combinator_Example.thy Fri Jul 09 17:15:03 2010 +0200
4.3 @@ -0,0 +1,60 @@
4.4 +(* Title: HOL/Library/While_Combinator.thy
4.5 + Author: Tobias Nipkow
4.6 + Copyright 2000 TU Muenchen
4.7 +*)
4.8 +
4.9 +header {* An application of the While combinator *}
4.10 +
4.11 +theory While_Combinator_Example
4.12 +imports While_Combinator
4.13 +begin
4.14 +
4.15 +text {* Computation of the @{term lfp} on finite sets via
4.16 + iteration. *}
4.17 +
4.18 +theorem lfp_conv_while:
4.19 + "[| mono f; finite U; f U = U |] ==>
4.20 + lfp f = fst (while (\<lambda>(A, fA). A \<noteq> fA) (\<lambda>(A, fA). (fA, f fA)) ({}, f {}))"
4.21 +apply (rule_tac P = "\<lambda>(A, B). (A \<subseteq> U \<and> B = f A \<and> A \<subseteq> B \<and> B \<subseteq> lfp f)" and
4.22 + r = "((Pow U \<times> UNIV) \<times> (Pow U \<times> UNIV)) \<inter>
4.23 + inv_image finite_psubset (op - U o fst)" in while_rule)
4.24 + apply (subst lfp_unfold)
4.25 + apply assumption
4.26 + apply (simp add: monoD)
4.27 + apply (subst lfp_unfold)
4.28 + apply assumption
4.29 + apply clarsimp
4.30 + apply (blast dest: monoD)
4.31 + apply (fastsimp intro!: lfp_lowerbound)
4.32 + apply (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset])
4.33 +apply (clarsimp simp add: finite_psubset_def order_less_le)
4.34 +apply (blast intro!: finite_Diff dest: monoD)
4.35 +done
4.36 +
4.37 +
4.38 +subsection {* Example *}
4.39 +
4.40 +text{* Cannot use @{thm[source]set_eq_subset} because it leads to
4.41 +looping because the antisymmetry simproc turns the subset relationship
4.42 +back into equality. *}
4.43 +
4.44 +theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) =
4.45 + P {0, 4, 2}"
4.46 +proof -
4.47 + have seteq: "!!A B. (A = B) = ((!a : A. a:B) & (!b:B. b:A))"
4.48 + by blast
4.49 + have aux: "!!f A B. {f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}"
4.50 + apply blast
4.51 + done
4.52 + show ?thesis
4.53 + apply (subst lfp_conv_while [where ?U = "{0, 1, 2, 3, 4, 5}"])
4.54 + apply (rule monoI)
4.55 + apply blast
4.56 + apply simp
4.57 + apply (simp add: aux set_eq_subset)
4.58 + txt {* The fixpoint computation is performed purely by rewriting: *}
4.59 + apply (simp add: while_unfold aux seteq del: subset_empty)
4.60 + done
4.61 +qed
4.62 +
4.63 +end
4.64 \ No newline at end of file