src/HOL/Library/While_Combinator.thy
changeset 10997 e14029f92770
parent 10984 8f49dcbec859
child 11047 10c51288b00d
equal deleted inserted replaced
10996:74e970389def 10997:e14029f92770
    92 
    92 
    93 theorem while_rule:
    93 theorem while_rule:
    94   "[| P s;
    94   "[| P s;
    95       !!s. [| P s; b s  |] ==> P (c s);
    95       !!s. [| P s; b s  |] ==> P (c s);
    96       !!s. [| P s; \<not> b s  |] ==> Q s;
    96       !!s. [| P s; \<not> b s  |] ==> Q s;
    97       wf r; 
    97       wf r;
    98       !!s. [| P s; b s  |] ==> (c s, s) \<in> r |] ==>
    98       !!s. [| P s; b s  |] ==> (c s, s) \<in> r |] ==>
    99    Q (while b c s)"
    99    Q (while b c s)"
   100 apply (rule while_rule_lemma)
   100 apply (rule while_rule_lemma)
   101 prefer 4 apply assumption
   101 prefer 4 apply assumption
   102 apply blast
   102 apply blast
   128 apply (clarsimp simp add: inv_image_def finite_psubset_def order_less_le)
   128 apply (clarsimp simp add: inv_image_def finite_psubset_def order_less_le)
   129 apply (blast intro!: finite_Diff dest: monoD)
   129 apply (blast intro!: finite_Diff dest: monoD)
   130 done
   130 done
   131 
   131 
   132 
   132 
   133 (*
       
   134 text {*
   133 text {*
   135  An example of using the @{term while} combinator.
   134  An example of using the @{term while} combinator.\footnote{It is safe
       
   135  to keep the example here, since there is no effect on the current
       
   136  theory.}
   136 *}
   137 *}
   137 
       
   138 lemma aux: "{f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}"
       
   139   apply blast
       
   140   done
       
   141 
   138 
   142 theorem "P (lfp (\<lambda>N::int set. {#0} \<union> {(n + #2) mod #6 | n. n \<in> N})) =
   139 theorem "P (lfp (\<lambda>N::int set. {#0} \<union> {(n + #2) mod #6 | n. n \<in> N})) =
   143     P {#0, #4, #2}"
   140     P {#0, #4, #2}"
   144   apply (subst lfp_conv_while [where ?U = "{#0, #1, #2, #3, #4, #5}"])
   141 proof -
   145      apply (rule monoI)
   142   have aux: "!!f A B. {f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}"
   146     apply blast
   143     apply blast
   147    apply simp
   144     done
   148   apply (simp add: aux set_eq_subset)
   145   show ?thesis
   149   txt {* The fixpoint computation is performed purely by rewriting: *}
   146     apply (subst lfp_conv_while [where ?U = "{#0, #1, #2, #3, #4, #5}"])
   150   apply (simp add: while_unfold aux set_eq_subset del: subset_empty)
   147        apply (rule monoI)
   151   done
   148       apply blast
   152 *)
   149      apply simp
       
   150     apply (simp add: aux set_eq_subset)
       
   151     txt {* The fixpoint computation is performed purely by rewriting: *}
       
   152     apply (simp add: while_unfold aux set_eq_subset del: subset_empty)
       
   153     done
       
   154 qed
   153 
   155 
   154 end
   156 end