134 assumes "p \<subseteq> i" |
134 assumes "p \<subseteq> i" |
135 and "\<And>n::nat . ValidTC (i \<inter> b \<inter> {s . v s = n}) c (A n) (i \<inter> {s . v s < n})" |
135 and "\<And>n::nat . ValidTC (i \<inter> b \<inter> {s . v s = n}) c (A n) (i \<inter> {s . v s < n})" |
136 and "i \<inter> uminus b \<subseteq> q" |
136 and "i \<inter> uminus b \<subseteq> q" |
137 shows "ValidTC p (While b c) (Awhile i v (\<lambda>n. A n)) q" |
137 shows "ValidTC p (While b c) (Awhile i v (\<lambda>n. A n)) q" |
138 proof - |
138 proof - |
139 { |
139 have "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b c) s t \<and> t \<in> q)" for s n |
140 fix s n |
140 proof (induction "n" arbitrary: s rule: less_induct) |
141 have "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b c) s t \<and> t \<in> q)" |
141 fix n :: nat |
142 proof (induction "n" arbitrary: s rule: less_induct) |
142 fix s :: 'a |
143 fix n :: nat |
143 assume 1: "\<And>(m::nat) s::'a . m < n \<Longrightarrow> s \<in> i \<and> v s = m \<longrightarrow> (\<exists>t . Sem (While b c) s t \<and> t \<in> q)" |
144 fix s :: 'a |
144 show "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b c) s t \<and> t \<in> q)" |
145 assume 1: "\<And>(m::nat) s::'a . m < n \<Longrightarrow> s \<in> i \<and> v s = m \<longrightarrow> (\<exists>t . Sem (While b c) s t \<and> t \<in> q)" |
145 proof (rule impI, cases "s \<in> b") |
146 show "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b c) s t \<and> t \<in> q)" |
146 assume 2: "s \<in> b" and "s \<in> i \<and> v s = n" |
147 proof (rule impI, cases "s \<in> b") |
147 hence "s \<in> i \<inter> b \<inter> {s . v s = n}" |
148 assume 2: "s \<in> b" and "s \<in> i \<and> v s = n" |
148 using assms(1) by auto |
149 hence "s \<in> i \<inter> b \<inter> {s . v s = n}" |
149 hence "\<exists>t . Sem c s t \<and> t \<in> i \<inter> {s . v s < n}" |
150 using assms(1) by auto |
150 by (metis assms(2) ValidTC_def) |
151 hence "\<exists>t . Sem c s t \<and> t \<in> i \<inter> {s . v s < n}" |
151 from this obtain t where 3: "Sem c s t \<and> t \<in> i \<inter> {s . v s < n}" |
152 by (metis assms(2) ValidTC_def) |
152 by auto |
153 from this obtain t where 3: "Sem c s t \<and> t \<in> i \<inter> {s . v s < n}" |
153 hence "\<exists>u . Sem (While b c) t u \<and> u \<in> q" |
154 by auto |
154 using 1 by auto |
155 hence "\<exists>u . Sem (While b c) t u \<and> u \<in> q" |
155 thus "\<exists>t . Sem (While b c) s t \<and> t \<in> q" |
156 using 1 by auto |
156 using 2 3 Sem.intros(6) by force |
157 thus "\<exists>t . Sem (While b c) s t \<and> t \<in> q" |
157 next |
158 using 2 3 Sem.intros(6) by force |
158 assume "s \<notin> b" and "s \<in> i \<and> v s = n" |
159 next |
159 thus "\<exists>t . Sem (While b c) s t \<and> t \<in> q" |
160 assume "s \<notin> b" and "s \<in> i \<and> v s = n" |
160 using Sem.intros(5) assms(3) by fastforce |
161 thus "\<exists>t . Sem (While b c) s t \<and> t \<in> q" |
|
162 using Sem.intros(5) assms(3) by fastforce |
|
163 qed |
|
164 qed |
161 qed |
165 } |
162 qed |
166 thus ?thesis |
163 thus ?thesis |
167 using assms(1) ValidTC_def by force |
164 using assms(1) ValidTC_def by force |
168 qed |
165 qed |
169 |
166 |
170 |
167 |