equal
deleted
inserted
replaced
33 apply (rule wf_same_fst) |
33 apply (rule wf_same_fst) |
34 apply (simp add: wf_iff_no_infinite_down_chain) |
34 apply (simp add: wf_iff_no_infinite_down_chain) |
35 apply blast |
35 apply blast |
36 done |
36 done |
37 |
37 |
38 constdefs |
38 definition |
39 while :: "('a => bool) => ('a => 'a) => 'a => 'a" |
39 while :: "('a => bool) => ('a => 'a) => 'a => 'a" |
40 "while b c s == while_aux (b, c, s)" |
40 "while b c s == while_aux (b, c, s)" |
41 |
41 |
42 lemma while_aux_unfold: |
42 lemma while_aux_unfold: |
43 "while_aux (b, c, s) = |
43 "while_aux (b, c, s) = |
86 theorem while_rule_lemma: |
86 theorem while_rule_lemma: |
87 assumes invariant: "!!s. P s ==> b s ==> P (c s)" |
87 assumes invariant: "!!s. P s ==> b s ==> P (c s)" |
88 and terminate: "!!s. P s ==> \<not> b s ==> Q s" |
88 and terminate: "!!s. P s ==> \<not> b s ==> Q s" |
89 and wf: "wf {(t, s). P s \<and> b s \<and> t = c s}" |
89 and wf: "wf {(t, s). P s \<and> b s \<and> t = c s}" |
90 shows "P s \<Longrightarrow> Q (while b c s)" |
90 shows "P s \<Longrightarrow> Q (while b c s)" |
91 apply (induct s rule: wf [THEN wf_induct]) |
91 using wf |
|
92 apply (induct s) |
92 apply simp |
93 apply simp |
93 apply (subst while_unfold) |
94 apply (subst while_unfold) |
94 apply (simp add: invariant terminate) |
95 apply (simp add: invariant terminate) |
95 done |
96 done |
96 |
97 |
99 !!s. [| P s; b s |] ==> P (c s); |
100 !!s. [| P s; b s |] ==> P (c s); |
100 !!s. [| P s; \<not> b s |] ==> Q s; |
101 !!s. [| P s; \<not> b s |] ==> Q s; |
101 wf r; |
102 wf r; |
102 !!s. [| P s; b s |] ==> (c s, s) \<in> r |] ==> |
103 !!s. [| P s; b s |] ==> (c s, s) \<in> r |] ==> |
103 Q (while b c s)" |
104 Q (while b c s)" |
104 apply (rule while_rule_lemma) |
105 apply (rule while_rule_lemma) |
105 prefer 4 apply assumption |
106 prefer 4 apply assumption |
106 apply blast |
107 apply blast |
107 apply blast |
108 apply blast |
108 apply(erule wf_subset) |
109 apply (erule wf_subset) |
109 apply blast |
110 apply blast |
110 done |
111 done |
111 |
112 |
112 text {* |
113 text {* |
113 \medskip An application: computation of the @{term lfp} on finite |
114 \medskip An application: computation of the @{term lfp} on finite |
114 sets via iteration. |
115 sets via iteration. |
115 *} |
116 *} |
140 |
141 |
141 text{* Cannot use @{thm[source]set_eq_subset} because it leads to |
142 text{* Cannot use @{thm[source]set_eq_subset} because it leads to |
142 looping because the antisymmetry simproc turns the subset relationship |
143 looping because the antisymmetry simproc turns the subset relationship |
143 back into equality. *} |
144 back into equality. *} |
144 |
145 |
145 lemma seteq: "(A = B) = ((!a : A. a:B) & (!b:B. b:A))" |
|
146 by blast |
|
147 |
|
148 theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) = |
146 theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) = |
149 P {0, 4, 2}" |
147 P {0, 4, 2}" |
150 proof - |
148 proof - |
|
149 have seteq: "!!A B. (A = B) = ((!a : A. a:B) & (!b:B. b:A))" |
|
150 by blast |
151 have aux: "!!f A B. {f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}" |
151 have aux: "!!f A B. {f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}" |
152 apply blast |
152 apply blast |
153 done |
153 done |
154 show ?thesis |
154 show ?thesis |
155 apply (subst lfp_conv_while [where ?U = "{0, 1, 2, 3, 4, 5}"]) |
155 apply (subst lfp_conv_while [where ?U = "{0, 1, 2, 3, 4, 5}"]) |