114 (*** |
114 (*** |
115 We actually want the corollary |
115 We actually want the corollary |
116 |
116 |
117 goal I.thy |
117 goal I.thy |
118 "I e [] m id_subst = Ok(s,t,n) --> W e [] m = Ok(s, $s t, n)"; |
118 "I e [] m id_subst = Ok(s,t,n) --> W e [] m = Ok(s, $s t, n)"; |
119 by(cut_facts_tac [(read_instantiate[("x","id_subst")] |
119 by (cut_facts_tac [(read_instantiate[("x","id_subst")] |
120 (read_instantiate[("x","[]")](thm RS spec) |
120 (read_instantiate[("x","[]")](thm RS spec) |
121 RS spec RS spec))] 1); |
121 RS spec RS spec))] 1); |
122 by(Full_simp_tac 1); |
122 by (Full_simp_tac 1); |
123 by(fast_tac HOL_cs 1); |
123 by (fast_tac HOL_cs 1); |
124 qed; |
124 qed; |
125 |
125 |
126 assuming that thm is the undischarged version of I_correct_wrt_W. |
126 assuming that thm is the undischarged version of I_correct_wrt_W. |
127 |
127 |
128 Wait until simplification of thms is possible. |
128 Wait until simplification of thms is possible. |
147 by(Asm_simp_tac 1); |
147 by(Asm_simp_tac 1); |
148 by(strip_tac 1); |
148 by(strip_tac 1); |
149 be exE 1; |
149 be exE 1; |
150 by(split_all_tac 1); |
150 by(split_all_tac 1); |
151 by(Full_simp_tac 1); |
151 by(Full_simp_tac 1); |
152 by(Asm_simp_tac 1); |
152 by (Asm_simp_tac 1); |
153 by(strip_tac 1); |
153 by (strip_tac 1); |
154 be exE 1; |
154 by (etac exE 1); |
155 by(REPEAT(etac conjE 1)); |
155 by (REPEAT(etac conjE 1)); |
156 by(split_all_tac 1); |
156 by (split_all_tac 1); |
157 by(Full_simp_tac 1); |
157 by (Full_simp_tac 1); |
158 bd lemma 1; |
158 by (dtac lemma 1); |
159 by(fast_tac HOL_cs 1); |
159 by(fast_tac HOL_cs 1); |
160 be exE 1; |
160 by (etac exE 1); |
161 be conjE 1; |
161 by (etac conjE 1); |
162 by(hyp_subst_tac 1); |
162 by (hyp_subst_tac 1); |
163 by(Asm_simp_tac 1); |
163 by (Asm_simp_tac 1); |
164 br exI 1; |
164 by (rtac exI 1); |
165 br conjI 1; |
165 by (rtac conjI 1); |
166 br refl 1; |
166 br refl 1; |
167 by(Simp_tac 1); |
167 by (Simp_tac 1); |
168 be disjE 1; |
168 by (etac disjE 1); |
169 br disjI1 1; |
169 br disjI1 1; |
170 by(full_simp_tac (!simpset addsimps [o_def,subst_comp_tel]) 1); |
170 by(full_simp_tac (!simpset addsimps [o_def,subst_comp_tel]) 1); |
171 by(EVERY[etac allE 1, etac allE 1, etac allE 1, |
171 by(EVERY[etac allE 1, etac allE 1, etac allE 1, |
172 etac impE 1, etac impE 2, atac 2, atac 2]); |
172 etac impE 1, etac impE 2, atac 2, atac 2]); |
173 br conjI 1; |
173 br conjI 1; |
174 by(fast_tac (HOL_cs addIs [W_var_ge RS new_tv_list_le]) 1); |
174 by(fast_tac (HOL_cs addIs [W_var_ge RS new_tv_list_le]) 1); |
175 br new_tv_subst_comp_2 1; |
175 br new_tv_subst_comp_2 1; |
176 by(fast_tac (HOL_cs addIs [W_var_ge RS new_tv_subst_le]) 1); |
176 by(fast_tac (HOL_cs addIs [W_var_ge RS new_tv_subst_le]) 1); |
177 by(fast_tac (HOL_cs addSIs [new_tv_subst_tel]addIs[new_tv_W RS conjunct1])1); |
177 by(fast_tac (HOL_cs addSIs [new_tv_subst_tel]addIs[new_tv_W RS conjunct1])1); |
178 br disjI2 1; |
178 by (rtac disjI2 1); |
179 be exE 1; |
179 by (etac exE 1); |
180 by(split_all_tac 1); |
180 by (split_all_tac 1); |
181 be conjE 1; |
181 by (etac conjE 1); |
182 by(Full_simp_tac 1); |
182 by (Full_simp_tac 1); |
183 bd lemma 1; |
183 by (dtac lemma 1); |
184 br conjI 1; |
184 br conjI 1; |
185 by(fast_tac (HOL_cs addIs [W_var_ge RS new_tv_list_le]) 1); |
185 by(fast_tac (HOL_cs addIs [W_var_ge RS new_tv_list_le]) 1); |
186 br new_tv_subst_comp_1 1; |
186 br new_tv_subst_comp_1 1; |
187 by(fast_tac (HOL_cs addIs [W_var_ge RS new_tv_subst_le]) 1); |
187 by(fast_tac (HOL_cs addIs [W_var_ge RS new_tv_subst_le]) 1); |
188 by(fast_tac (HOL_cs addSIs [new_tv_subst_tel]addIs[new_tv_W RS conjunct1])1); |
188 by(fast_tac (HOL_cs addSIs [new_tv_subst_tel]addIs[new_tv_W RS conjunct1])1); |
189 be exE 1; |
189 by (etac exE 1); |
190 be conjE 1; |
190 by (etac conjE 1); |
191 by(hyp_subst_tac 1); |
191 by (hyp_subst_tac 1); |
192 by(asm_full_simp_tac (!simpset addsimps |
192 by (asm_full_simp_tac (!simpset addsimps |
193 [o_def,subst_comp_te RS sym,subst_comp_tel RS sym]) 1); |
193 [o_def,subst_comp_te RS sym,subst_comp_tel RS sym]) 1); |
194 by(asm_simp_tac (!simpset addcongs [conj_cong] addsimps |
194 by (asm_simp_tac (!simpset addcongs [conj_cong] addsimps |
195 [eq_sym_conv,subst_comp_te RS sym,subst_comp_tel RS sym]) 1); |
195 [eq_sym_conv,subst_comp_te RS sym,subst_comp_tel RS sym]) 1); |
196 qed_spec_mp "I_complete_wrt_W"; |
196 qed_spec_mp "I_complete_wrt_W"; |
197 |
197 |
198 (*** |
198 (*** |
199 We actually want the corollary |
199 We actually want the corollary |