equal
deleted
inserted
replaced
133 An example of using the @{term while} combinator.\footnote{It is safe |
133 An example of using the @{term while} combinator.\footnote{It is safe |
134 to keep the example here, since there is no effect on the current |
134 to keep the example here, since there is no effect on the current |
135 theory.} |
135 theory.} |
136 *} |
136 *} |
137 |
137 |
138 theorem "P (lfp (\<lambda>N::int set. {Numeral0} \<union> {(n + 2) mod 6 | n. n \<in> N})) = |
138 theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) = P {0, 4, 2}" |
139 P {Numeral0, 4, 2}" |
|
140 proof - |
139 proof - |
141 have aux: "!!f A B. {f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}" |
140 have aux: "!!f A B. {f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}" |
142 apply blast |
141 apply blast |
143 done |
142 done |
144 show ?thesis |
143 show ?thesis |
145 apply (subst lfp_conv_while [where ?U = "{Numeral0, Numeral1, 2, 3, 4, 5}"]) |
144 apply (subst lfp_conv_while [where ?U = "{0, 1, 2, 3, 4, 5}"]) |
146 apply (rule monoI) |
145 apply (rule monoI) |
147 apply blast |
146 apply blast |
148 apply simp |
147 apply simp |
149 apply (simp add: aux set_eq_subset) |
148 apply (simp add: aux set_eq_subset) |
150 txt {* The fixpoint computation is performed purely by rewriting: *} |
149 txt {* The fixpoint computation is performed purely by rewriting: *} |