Merged Example into While_Combi
authornipkow
Fri Jan 26 15:50:52 2001 +0100 (2001-01-26)
changeset 109848f49dcbec859
parent 10983 59961d32b1ae
child 10985 65a8a0e2d55b
Merged Example into While_Combi
src/HOL/Library/Library.thy
src/HOL/Library/ROOT.ML
src/HOL/Library/While_Combinator.thy
src/HOL/Library/While_Combinator_Example.thy
     1.1 --- a/src/HOL/Library/Library.thy	Fri Jan 26 15:50:28 2001 +0100
     1.2 +++ b/src/HOL/Library/Library.thy	Fri Jan 26 15:50:52 2001 +0100
     1.3 @@ -7,6 +7,6 @@
     1.4    Nested_Environment +
     1.5    Accessible_Part +
     1.6    Multiset +
     1.7 -  While_Combinator + While_Combinator_Example:
     1.8 +  While_Combinator:
     1.9  end
    1.10  (*>*)
     2.1 --- a/src/HOL/Library/ROOT.ML	Fri Jan 26 15:50:28 2001 +0100
     2.2 +++ b/src/HOL/Library/ROOT.ML	Fri Jan 26 15:50:52 2001 +0100
     2.3 @@ -1,2 +1,1 @@
     2.4 -
     2.5  use_thy "Library";
     3.1 --- a/src/HOL/Library/While_Combinator.thy	Fri Jan 26 15:50:28 2001 +0100
     3.2 +++ b/src/HOL/Library/While_Combinator.thy	Fri Jan 26 15:50:52 2001 +0100
     3.3 @@ -67,14 +67,16 @@
     3.4    apply blast
     3.5    done
     3.6  
     3.7 +hide const while_aux
     3.8 +
     3.9  text {*
    3.10   The proof rule for @{term while}, where @{term P} is the invariant.
    3.11  *}
    3.12  
    3.13  theorem while_rule_lemma[rule_format]:
    3.14 -  "(!!s. P s ==> b s ==> P (c s)) ==>
    3.15 -    (!!s. P s ==> \<not> b s ==> Q s) ==>
    3.16 -    wf {(t, s). P s \<and> b s \<and> t = c s} ==>
    3.17 +  "[| !!s. P s ==> b s ==> P (c s);
    3.18 +      !!s. P s ==> \<not> b s ==> Q s;
    3.19 +      wf {(t, s). P s \<and> b s \<and> t = c s} |] ==>
    3.20      P s --> Q (while b c s)"
    3.21  proof -
    3.22    case antecedent
    3.23 @@ -89,10 +91,12 @@
    3.24  qed
    3.25  
    3.26  theorem while_rule:
    3.27 -  "[| P s; !!s. [| P s; b s  |] ==> P (c s);
    3.28 -    !!s. [| P s; \<not> b s  |] ==> Q s;
    3.29 -    wf r;  !!s. [| P s; b s  |] ==> (c s, s) \<in> r |] ==>
    3.30 -    Q (while b c s)"
    3.31 +  "[| P s;
    3.32 +      !!s. [| P s; b s  |] ==> P (c s);
    3.33 +      !!s. [| P s; \<not> b s  |] ==> Q s;
    3.34 +      wf r; 
    3.35 +      !!s. [| P s; b s  |] ==> (c s, s) \<in> r |] ==>
    3.36 +   Q (while b c s)"
    3.37  apply (rule while_rule_lemma)
    3.38  prefer 4 apply assumption
    3.39  apply blast
    3.40 @@ -101,6 +105,50 @@
    3.41  apply blast
    3.42  done
    3.43  
    3.44 -hide const while_aux
    3.45 +text {*
    3.46 + \medskip An application: computation of the @{term lfp} on finite
    3.47 + sets via iteration.
    3.48 +*}
    3.49 +
    3.50 +theorem lfp_conv_while:
    3.51 +  "[| mono f; finite U; f U = U |] ==>
    3.52 +    lfp f = fst (while (\<lambda>(A, fA). A \<noteq> fA) (\<lambda>(A, fA). (fA, f fA)) ({}, f {}))"
    3.53 +apply (rule_tac P = "\<lambda>(A, B). (A \<subseteq> U \<and> B = f A \<and> A \<subseteq> B \<and> B \<subseteq> lfp f)" and
    3.54 +                r = "((Pow U <*> UNIV) <*> (Pow U <*> UNIV)) \<inter>
    3.55 +                     inv_image finite_psubset (op - U o fst)" in while_rule)
    3.56 +   apply (subst lfp_unfold)
    3.57 +    apply assumption
    3.58 +   apply (simp add: monoD)
    3.59 +  apply (subst lfp_unfold)
    3.60 +   apply assumption
    3.61 +  apply clarsimp
    3.62 +  apply (blast dest: monoD)
    3.63 + apply (fastsimp intro!: lfp_lowerbound)
    3.64 + apply (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset])
    3.65 +apply (clarsimp simp add: inv_image_def finite_psubset_def order_less_le)
    3.66 +apply (blast intro!: finite_Diff dest: monoD)
    3.67 +done
    3.68 +
    3.69 +
    3.70 +(*
    3.71 +text {*
    3.72 + An example of using the @{term while} combinator.
    3.73 +*}
    3.74 +
    3.75 +lemma aux: "{f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}"
    3.76 +  apply blast
    3.77 +  done
    3.78 +
    3.79 +theorem "P (lfp (\<lambda>N::int set. {#0} \<union> {(n + #2) mod #6 | n. n \<in> N})) =
    3.80 +    P {#0, #4, #2}"
    3.81 +  apply (subst lfp_conv_while [where ?U = "{#0, #1, #2, #3, #4, #5}"])
    3.82 +     apply (rule monoI)
    3.83 +    apply blast
    3.84 +   apply simp
    3.85 +  apply (simp add: aux set_eq_subset)
    3.86 +  txt {* The fixpoint computation is performed purely by rewriting: *}
    3.87 +  apply (simp add: while_unfold aux set_eq_subset del: subset_empty)
    3.88 +  done
    3.89 +*)
    3.90  
    3.91  end
     4.1 --- a/src/HOL/Library/While_Combinator_Example.thy	Fri Jan 26 15:50:28 2001 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,49 +0,0 @@
     4.4 -
     4.5 -header {* \title{} *}
     4.6 -
     4.7 -theory While_Combinator_Example = While_Combinator:
     4.8 -
     4.9 -text {*
    4.10 - \medskip An application: computation of the @{term lfp} on finite
    4.11 - sets via iteration.
    4.12 -*}
    4.13 -
    4.14 -theorem lfp_conv_while:
    4.15 -  "mono f ==> finite U ==> f U = U ==>
    4.16 -    lfp f = fst (while (\<lambda>(A, fA). A \<noteq> fA) (\<lambda>(A, fA). (fA, f fA)) ({}, f {}))"
    4.17 -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.18 -                r = "((Pow U <*> UNIV) <*> (Pow U <*> UNIV)) \<inter>
    4.19 -                     inv_image finite_psubset (op - U o fst)" in while_rule)
    4.20 -   apply (subst lfp_unfold)
    4.21 -    apply assumption
    4.22 -   apply (simp add: monoD)
    4.23 -  apply (subst lfp_unfold)
    4.24 -   apply assumption
    4.25 -  apply clarsimp
    4.26 -  apply (blast dest: monoD)
    4.27 - apply (fastsimp intro!: lfp_lowerbound)
    4.28 - apply (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset])
    4.29 -apply (clarsimp simp add: inv_image_def finite_psubset_def order_less_le)
    4.30 -apply (blast intro!: finite_Diff dest: monoD)
    4.31 -done
    4.32 -
    4.33 -text {*
    4.34 - An example of using the @{term while} combinator.
    4.35 -*}
    4.36 -
    4.37 -lemma aux: "{f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}"
    4.38 -  apply blast
    4.39 -  done
    4.40 -
    4.41 -theorem "P (lfp (\<lambda>N::int set. {#0} \<union> {(n + #2) mod #6 | n. n \<in> N})) =
    4.42 -    P {#0, #4, #2}"
    4.43 -  apply (subst lfp_conv_while [where ?U = "{#0, #1, #2, #3, #4, #5}"])
    4.44 -     apply (rule monoI)
    4.45 -    apply blast
    4.46 -   apply simp
    4.47 -  apply (simp add: aux set_eq_subset)
    4.48 -  txt {* The fixpoint computation is performed purely by rewriting: *}
    4.49 -  apply (simp add: while_unfold aux set_eq_subset del: subset_empty)
    4.50 -  done
    4.51 -
    4.52 -end