equal
deleted
inserted
replaced
181 let |
181 let |
182 val ss_thms = @{thms "permute_minus_cancel" "permute_prod.simps" "split_paired_all"} |
182 val ss_thms = @{thms "permute_minus_cancel" "permute_prod.simps" "split_paired_all"} |
183 in |
183 in |
184 REPEAT o FIRST' |
184 REPEAT o FIRST' |
185 [CHANGED o simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss_thms), |
185 [CHANGED o simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss_thms), |
186 rtac (thm RS @{thm "trans"}), |
186 resolve_tac ctxt [thm RS @{thm trans}], |
187 rtac @{thm "trans"[OF "permute_fun_def"]} THEN' rtac @{thm "ext"}] |
187 resolve_tac ctxt @{thms trans[OF "permute_fun_def"]} THEN' |
|
188 resolve_tac ctxt @{thms ext}] |
188 end |
189 end |
189 |
190 |
190 in |
191 in |
191 |
192 |
192 fun thm_4_of_1 ctxt thm = |
193 fun thm_4_of_1 ctxt thm = |
211 |
212 |
212 fun tac ctxt thm thm' = |
213 fun tac ctxt thm thm' = |
213 let |
214 let |
214 val ss_thms = @{thms "permute_minus_cancel"(2)} |
215 val ss_thms = @{thms "permute_minus_cancel"(2)} |
215 in |
216 in |
216 EVERY' [rtac @{thm "iffI"}, dtac @{thm "permute_boolE"}, rtac thm, assume_tac ctxt, |
217 EVERY' [resolve_tac ctxt @{thms iffI}, |
217 rtac @{thm "permute_boolI"}, dtac thm', |
218 dresolve_tac ctxt @{thms permute_boolE}, |
|
219 resolve_tac ctxt [thm], |
|
220 assume_tac ctxt, |
|
221 resolve_tac ctxt @{thms permute_boolI}, |
|
222 dresolve_tac ctxt [thm'], |
218 full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss_thms)] |
223 full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss_thms)] |
219 end |
224 end |
220 |
225 |
221 in |
226 in |
222 |
227 |
230 | find_perm (Abs (_, _, body)) = find_perm body |
235 | find_perm (Abs (_, _, body)) = find_perm body |
231 | find_perm _ = raise THM ("thm_3_of_2", 0, [thm]) |
236 | find_perm _ = raise THM ("thm_3_of_2", 0, [thm]) |
232 val p = concl |> dest_comb |> snd |> find_perm |
237 val p = concl |> dest_comb |> snd |> find_perm |
233 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p prem, concl)) |
238 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p prem, concl)) |
234 val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt |
239 val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt |
235 val thm' = Drule.cterm_instantiate [apply2 (Thm.cterm_of ctxt') (p, mk_minus p')] thm |
240 val thm' = infer_instantiate ctxt' [(#1 (dest_Var p), Thm.cterm_of ctxt' (mk_minus p'))] thm |
236 in |
241 in |
237 Goal.prove ctxt' [] [] goal' (fn {context = ctxt'', ...} => tac ctxt'' thm thm' 1) |
242 Goal.prove ctxt' [] [] goal' (fn {context = ctxt'', ...} => tac ctxt'' thm thm' 1) |
238 |> singleton (Proof_Context.export ctxt' ctxt) |
243 |> singleton (Proof_Context.export ctxt' ctxt) |
239 end |
244 end |
240 handle TERM _ => |
245 handle TERM _ => |