equal
deleted
inserted
replaced
137 local |
137 local |
138 open Nominal_Permeq |
138 open Nominal_Permeq |
139 in |
139 in |
140 (* by default eqvt_strict_config contains unwanted @{thm permute_pure} *) |
140 (* by default eqvt_strict_config contains unwanted @{thm permute_pure} *) |
141 |
141 |
142 val eqvt_sconfig = (delposts eqvt_strict_config) addpres @{thms permute_minus_cancel} |
142 val eqvt_sconfig = eqvt_strict_config addpres @{thms permute_minus_cancel} |
143 |
143 |
144 fun eqvt_stac ctxt = eqvt_tac ctxt eqvt_sconfig |
144 fun eqvt_stac ctxt = eqvt_tac ctxt eqvt_sconfig |
145 fun eqvt_srule ctxt = eqvt_rule ctxt eqvt_sconfig |
145 fun eqvt_srule ctxt = eqvt_rule ctxt eqvt_sconfig |
146 |
146 |
147 end |
147 end |
148 |
148 |
149 val all_elims = |
149 val all_elims = |
150 let |
150 let |
173 val thy = ProofContext.theory_of context |
173 val thy = ProofContext.theory_of context |
174 val (prms, p, _) = split_last2 (map snd params) |
174 val (prms, p, _) = split_last2 (map snd params) |
175 val prm_tys = map (fastype_of o term_of) prms |
175 val prm_tys = map (fastype_of o term_of) prms |
176 val cperms = map (cterm_of thy o perm_const) prm_tys |
176 val cperms = map (cterm_of thy o perm_const) prm_tys |
177 val p_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 p ct2) cperms prms |
177 val p_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 p ct2) cperms prms |
178 val prem' = cterm_instantiate (intr_cvars ~~ p_prms) prem |
178 val prem' = prem |
|
179 |> cterm_instantiate (intr_cvars ~~ p_prms) |
|
180 |> eqvt_srule ctxt |
179 |
181 |
180 (* for inductive-premises*) |
182 (* for inductive-premises*) |
181 fun tac1 prm = helper_tac true prm p context |
183 fun tac1 prm = helper_tac true prm p context |
182 |
184 |
183 (* for non-inductive premises *) |
185 (* for non-inductive premises *) |
187 helper_tac false prm p context ] |
189 helper_tac false prm p context ] |
188 |
190 |
189 fun select prm (t, i) = |
191 fun select prm (t, i) = |
190 (if member same_name Ps (real_head_of t) then tac1 prm else tac2 prm) i |
192 (if member same_name Ps (real_head_of t) then tac1 prm else tac2 prm) i |
191 in |
193 in |
192 EVERY1 [eqvt_stac ctxt, rtac prem', RANGE (map (SUBGOAL o select) prems) ] |
194 EVERY1 [ eqvt_stac context, |
|
195 rtac prem', |
|
196 RANGE (map (SUBGOAL o select) prems) ] |
193 end) ctxt |
197 end) ctxt |
194 |
198 |
195 fun fresh_thm ctxt user_thm p c concl_args avoid_trm = |
199 fun fresh_thm ctxt user_thm p c concl_args avoid_trm = |
196 let |
200 let |
197 val conj1 = |
201 val conj1 = |
242 val expand_conv = Conv.try_conv (Conv.rewrs_conv fresh_eqs) |
246 val expand_conv = Conv.try_conv (Conv.rewrs_conv fresh_eqs) |
243 fun expand_conv_bot ctxt = Conv.bottom_conv (K expand_conv) ctxt |
247 fun expand_conv_bot ctxt = Conv.bottom_conv (K expand_conv) ctxt |
244 |
248 |
245 val cperms = map (cterm_of thy o perm_const) prm_tys |
249 val cperms = map (cterm_of thy o perm_const) prm_tys |
246 val qp_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 (mk_cplus q p) ct2) cperms prms |
250 val qp_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 (mk_cplus q p) ct2) cperms prms |
247 val prem' = cterm_instantiate (intr_cvars ~~ qp_prms) prem |
251 val prem' = prem |
|
252 |> cterm_instantiate (intr_cvars ~~ qp_prms) |
|
253 |> eqvt_srule ctxt |
248 |
254 |
249 val fprop' = eqvt_srule ctxt' fprop |
255 val fprop' = eqvt_srule ctxt' fprop |
250 val tac_fresh = simp_tac (HOL_basic_ss addsimps [fprop']) |
256 val tac_fresh = simp_tac (HOL_basic_ss addsimps [fprop']) |
251 |
257 |
252 (* for inductive-premises*) |
258 (* for inductive-premises*) |
275 fun case_tac ctxt Ps avoid avoid_trm intr_cvars param_trms prem user_thm concl_args = |
281 fun case_tac ctxt Ps avoid avoid_trm intr_cvars param_trms prem user_thm concl_args = |
276 let |
282 let |
277 val tac1 = non_binder_tac prem intr_cvars Ps ctxt |
283 val tac1 = non_binder_tac prem intr_cvars Ps ctxt |
278 val tac2 = binder_tac prem intr_cvars param_trms Ps user_thm avoid_trm concl_args ctxt |
284 val tac2 = binder_tac prem intr_cvars param_trms Ps user_thm avoid_trm concl_args ctxt |
279 in |
285 in |
280 EVERY' [ rtac @{thm allI}, rtac @{thm allI}, if null avoid then tac1 else tac2 ] |
286 EVERY' [ rtac @{thm allI}, rtac @{thm allI}, |
|
287 if null avoid then tac1 else tac2 ] |
281 end |
288 end |
282 |
289 |
283 fun prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms concl_args |
290 fun prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms concl_args |
284 {prems, context} = |
291 {prems, context} = |
285 let |
292 let |