equal
deleted
inserted
replaced
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 |