equal
deleted
inserted
replaced
65 apply blast |
65 apply blast |
66 done |
66 done |
67 |
67 |
68 hide const while_aux |
68 hide const while_aux |
69 |
69 |
70 lemma def_while_unfold: assumes fdef: "f == while test do" |
70 lemma def_while_unfold: |
71 shows "f x = (if test x then f(do x) else x)" |
71 assumes fdef: "f == while test do" |
|
72 shows "f x = (if test x then f(do x) else x)" |
72 proof - |
73 proof - |
73 have "f x = while test do x" using fdef by simp |
74 have "f x = while test do x" using fdef by simp |
74 also have "\<dots> = (if test x then while test do (do x) else x)" |
75 also have "\<dots> = (if test x then while test do (do x) else x)" |
75 by(rule while_unfold) |
76 by(rule while_unfold) |
76 also have "\<dots> = (if test x then f(do x) else x)" by(simp add:fdef[symmetric]) |
77 also have "\<dots> = (if test x then f(do x) else x)" by(simp add:fdef[symmetric]) |
80 |
81 |
81 text {* |
82 text {* |
82 The proof rule for @{term while}, where @{term P} is the invariant. |
83 The proof rule for @{term while}, where @{term P} is the invariant. |
83 *} |
84 *} |
84 |
85 |
85 theorem while_rule_lemma[rule_format]: |
86 theorem while_rule_lemma: |
86 "[| !!s. P s ==> b s ==> P (c s); |
87 assumes invariant: "!!s. P s ==> b s ==> P (c s)" |
87 !!s. P s ==> \<not> b s ==> Q s; |
88 and terminate: "!!s. P s ==> \<not> b s ==> Q s" |
88 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}" |
89 P s --> Q (while b c s)" |
90 shows "P s \<Longrightarrow> Q (while b c s)" |
90 proof - |
91 apply (induct s rule: wf [THEN wf_induct]) |
91 case rule_context |
92 apply simp |
92 assume wf: "wf {(t, s). P s \<and> b s \<and> t = c s}" |
93 apply (subst while_unfold) |
93 show ?thesis |
94 apply (simp add: invariant terminate) |
94 apply (induct s rule: wf [THEN wf_induct]) |
95 done |
95 apply simp |
|
96 apply clarify |
|
97 apply (subst while_unfold) |
|
98 apply (simp add: rule_context) |
|
99 done |
|
100 qed |
|
101 |
96 |
102 theorem while_rule: |
97 theorem while_rule: |
103 "[| P s; |
98 "[| P s; |
104 !!s. [| P s; b s |] ==> P (c s); |
99 !!s. [| P s; b s |] ==> P (c s); |
105 !!s. [| P s; \<not> b s |] ==> Q s; |
100 !!s. [| P s; \<not> b s |] ==> Q s; |
146 text{* Cannot use @{thm[source]set_eq_subset} because it leads to |
141 text{* Cannot use @{thm[source]set_eq_subset} because it leads to |
147 looping because the antisymmetry simproc turns the subset relationship |
142 looping because the antisymmetry simproc turns the subset relationship |
148 back into equality. *} |
143 back into equality. *} |
149 |
144 |
150 lemma seteq: "(A = B) = ((!a : A. a:B) & (!b:B. b:A))" |
145 lemma seteq: "(A = B) = ((!a : A. a:B) & (!b:B. b:A))" |
151 by blast |
146 by blast |
152 |
147 |
153 theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) = |
148 theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) = |
154 P {0, 4, 2}" |
149 P {0, 4, 2}" |
155 proof - |
150 proof - |
156 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}" |