moved example to its own file in HOL/ex
authorkrauss
Fri Jul 09 17:15:03 2010 +0200 (2010-07-09)
changeset 377608380686be5cd
parent 37759 00ff97087ab5
child 37761 decac8d1c8e7
moved example to its own file in HOL/ex
src/HOL/IsaMakefile
src/HOL/Library/While_Combinator.thy
src/HOL/ex/ROOT.ML
src/HOL/ex/While_Combinator_Example.thy
     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