equal
deleted
inserted
replaced
5 |
5 |
6 text {* |
6 text {* |
7 An example of using the @{term while} combinator. |
7 An example of using the @{term while} combinator. |
8 *} |
8 *} |
9 |
9 |
10 lemma aux: "{f n| n. A n \<or> B n} = {f n| n. A n} \<union> {f n| n. B n}" |
10 lemma aux: "{f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}" |
11 apply blast |
11 apply blast |
12 done |
12 done |
13 |
13 |
14 theorem "P (lfp (\<lambda>N::int set. {#0} \<union> {(n + #2) mod #6| n. n \<in> N})) = |
14 theorem "P (lfp (\<lambda>N::int set. {#0} \<union> {(n + #2) mod #6 | n. n \<in> N})) = |
15 P {#0, #4, #2}" |
15 P {#0, #4, #2}" |
16 apply (subst lfp_conv_while [where ?U = "{#0, #1, #2, #3, #4, #5}"]) |
16 apply (subst lfp_conv_while [where ?U = "{#0, #1, #2, #3, #4, #5}"]) |
17 apply (rule monoI) |
17 apply (rule monoI) |
18 apply blast |
18 apply blast |
19 apply simp |
19 apply simp |