equal
deleted
inserted
replaced
205 by (simp add: supp_perm_eq)} |
205 by (simp add: supp_perm_eq)} |
206 val fresh_star_plus = @{lemma "fresh_star (permute q (permute p x)) c ==> fresh_star (permute (q + p) x) c" |
206 val fresh_star_plus = @{lemma "fresh_star (permute q (permute p x)) c ==> fresh_star (permute (q + p) x) c" |
207 by (simp add: permute_plus)} |
207 by (simp add: permute_plus)} |
208 |
208 |
209 |
209 |
210 fun binder_tac prem intr_cvars param_trms Ps user_thm avoid avoid_trm concl_args ctxt = |
210 fun binder_tac prem intr_cvars param_trms Ps user_thm avoid_trm concl_args ctxt = |
211 Subgoal.FOCUS (fn {context = ctxt, params, prems, concl, ...} => |
211 Subgoal.FOCUS (fn {context = ctxt, params, prems, concl, ...} => |
212 let |
212 let |
213 val thy = ProofContext.theory_of ctxt |
213 val thy = ProofContext.theory_of ctxt |
214 val (prms, p, c) = split_last2 (map snd params) |
214 val (prms, p, c) = split_last2 (map snd params) |
215 val prm_trms = map term_of prms |
215 val prm_trms = map term_of prms |
272 end) ctxt |
272 end) ctxt |
273 |
273 |
274 fun case_tac ctxt Ps avoid avoid_trm intr_cvars param_trms prem user_thm concl_args = |
274 fun case_tac ctxt Ps avoid avoid_trm intr_cvars param_trms prem user_thm concl_args = |
275 let |
275 let |
276 val tac1 = non_binder_tac prem intr_cvars Ps ctxt |
276 val tac1 = non_binder_tac prem intr_cvars Ps ctxt |
277 val tac2 = binder_tac prem intr_cvars param_trms Ps user_thm avoid avoid_trm concl_args ctxt |
277 val tac2 = binder_tac prem intr_cvars param_trms Ps user_thm avoid_trm concl_args ctxt |
278 in |
278 in |
279 EVERY' [ rtac @{thm allI}, rtac @{thm allI}, if null avoid then tac1 else tac2 ] |
279 EVERY' [ rtac @{thm allI}, rtac @{thm allI}, if null avoid then tac1 else tac2 ] |
280 end |
280 end |
281 |
281 |
282 fun prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms concl_args |
282 fun prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms concl_args |