src/HOL/Library/While_Combinator.thy
 changeset 10984 8f49dcbec859 parent 10774 4de3a0d3ae28 child 10997 e14029f92770
```     1.1 --- a/src/HOL/Library/While_Combinator.thy	Fri Jan 26 15:50:28 2001 +0100
1.2 +++ b/src/HOL/Library/While_Combinator.thy	Fri Jan 26 15:50:52 2001 +0100
1.3 @@ -67,14 +67,16 @@
1.4    apply blast
1.5    done
1.6
1.7 +hide const while_aux
1.8 +
1.9  text {*
1.10   The proof rule for @{term while}, where @{term P} is the invariant.
1.11  *}
1.12
1.13  theorem while_rule_lemma[rule_format]:
1.14 -  "(!!s. P s ==> b s ==> P (c s)) ==>
1.15 -    (!!s. P s ==> \<not> b s ==> Q s) ==>
1.16 -    wf {(t, s). P s \<and> b s \<and> t = c s} ==>
1.17 +  "[| !!s. P s ==> b s ==> P (c s);
1.18 +      !!s. P s ==> \<not> b s ==> Q s;
1.19 +      wf {(t, s). P s \<and> b s \<and> t = c s} |] ==>
1.20      P s --> Q (while b c s)"
1.21  proof -
1.22    case antecedent
1.23 @@ -89,10 +91,12 @@
1.24  qed
1.25
1.26  theorem while_rule:
1.27 -  "[| P s; !!s. [| P s; b s  |] ==> P (c s);
1.28 -    !!s. [| P s; \<not> b s  |] ==> Q s;
1.29 -    wf r;  !!s. [| P s; b s  |] ==> (c s, s) \<in> r |] ==>
1.30 -    Q (while b c s)"
1.31 +  "[| P s;
1.32 +      !!s. [| P s; b s  |] ==> P (c s);
1.33 +      !!s. [| P s; \<not> b s  |] ==> Q s;
1.34 +      wf r;
1.35 +      !!s. [| P s; b s  |] ==> (c s, s) \<in> r |] ==>
1.36 +   Q (while b c s)"
1.37  apply (rule while_rule_lemma)
1.38  prefer 4 apply assumption
1.39  apply blast
1.40 @@ -101,6 +105,50 @@
1.41  apply blast
1.42  done
1.43
1.44 -hide const while_aux
1.45 +text {*
1.46 + \medskip An application: computation of the @{term lfp} on finite
1.47 + sets via iteration.
1.48 +*}
1.49 +
1.50 +theorem lfp_conv_while:
1.51 +  "[| mono f; finite U; f U = U |] ==>
1.52 +    lfp f = fst (while (\<lambda>(A, fA). A \<noteq> fA) (\<lambda>(A, fA). (fA, f fA)) ({}, f {}))"
1.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
1.54 +                r = "((Pow U <*> UNIV) <*> (Pow U <*> UNIV)) \<inter>
1.55 +                     inv_image finite_psubset (op - U o fst)" in while_rule)
1.56 +   apply (subst lfp_unfold)
1.57 +    apply assumption
1.58 +   apply (simp add: monoD)
1.59 +  apply (subst lfp_unfold)
1.60 +   apply assumption
1.61 +  apply clarsimp
1.62 +  apply (blast dest: monoD)
1.63 + apply (fastsimp intro!: lfp_lowerbound)
1.64 + apply (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset])
1.65 +apply (clarsimp simp add: inv_image_def finite_psubset_def order_less_le)
1.66 +apply (blast intro!: finite_Diff dest: monoD)
1.67 +done
1.68 +
1.69 +
1.70 +(*
1.71 +text {*
1.72 + An example of using the @{term while} combinator.
1.73 +*}
1.74 +
1.75 +lemma aux: "{f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}"
1.76 +  apply blast
1.77 +  done
1.78 +
1.79 +theorem "P (lfp (\<lambda>N::int set. {#0} \<union> {(n + #2) mod #6 | n. n \<in> N})) =
1.80 +    P {#0, #4, #2}"
1.81 +  apply (subst lfp_conv_while [where ?U = "{#0, #1, #2, #3, #4, #5}"])
1.82 +     apply (rule monoI)
1.83 +    apply blast
1.84 +   apply simp
1.85 +  apply (simp add: aux set_eq_subset)
1.86 +  txt {* The fixpoint computation is performed purely by rewriting: *}
1.87 +  apply (simp add: while_unfold aux set_eq_subset del: subset_empty)
1.88 +  done
1.89 +*)
1.90
1.91  end
```