--- a/Nominal/nominal_inductive.ML Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_inductive.ML Sat Mar 19 21:06:48 2016 +0000
@@ -24,11 +24,11 @@
fun mk_cminus p =
Thm.apply @{cterm "uminus :: perm => perm"} p
-fun minus_permute_intro_tac p =
- rtac (Drule.instantiate' [] [SOME (mk_cminus p)] @{thm permute_boolE})
+fun minus_permute_intro_tac ctxt p =
+ resolve_tac ctxt [Thm.instantiate' [] [SOME (mk_cminus p)] @{thm permute_boolE}]
fun minus_permute_elim p thm =
- thm RS (Drule.instantiate' [] [NONE, SOME (mk_cminus p)] @{thm permute_boolI})
+ thm RS (Thm.instantiate' [] [NONE, SOME (mk_cminus p)] @{thm permute_boolI})
(* fixme: move to nominal_library *)
fun real_head_of (@{term Trueprop} $ t) = real_head_of t
@@ -156,23 +156,23 @@
val all_elims =
let
fun spec' ct =
- Drule.instantiate' [SOME (Thm.ctyp_of_cterm ct)] [NONE, SOME ct] @{thm spec}
+ Thm.instantiate' [SOME (Thm.ctyp_of_cterm ct)] [NONE, SOME ct] @{thm spec}
in
fold (fn ct => fn th => th RS spec' ct)
end
fun helper_tac flag prm p ctxt =
- Subgoal.SUBPROOF (fn {context, prems, ...} =>
+ Subgoal.SUBPROOF (fn {context = ctxt', prems, ...} =>
let
val prems' = prems
|> map (minus_permute_elim p)
- |> map (eqvt_srule context)
+ |> map (eqvt_srule ctxt')
val prm' = (prems' MRS prm)
|> flag ? (all_elims [p])
- |> flag ? (eqvt_srule context)
+ |> flag ? (eqvt_srule ctxt')
in
- asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps (prm' :: @{thms HOL.induct_forall_def})) 1
+ asm_full_simp_tac (put_simpset HOL_ss ctxt' addsimps (prm' :: @{thms HOL.induct_forall_def})) 1
end) ctxt
fun non_binder_tac prem intr_cvars Ps ctxt =
@@ -183,15 +183,15 @@
val cperms = map (Thm.cterm_of ctxt' o perm_const) prm_tys
val p_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 p ct2) cperms prms
val prem' = prem
- |> cterm_instantiate (intr_cvars ~~ p_prms)
- |> eqvt_srule ctxt
+ |> infer_instantiate ctxt' (map (#1 o dest_Var o Thm.term_of) intr_cvars ~~ p_prms)
+ |> eqvt_srule ctxt'
(* for inductive-premises*)
fun tac1 prm = helper_tac true prm p ctxt'
(* for non-inductive premises *)
fun tac2 prm =
- EVERY' [ minus_permute_intro_tac p,
+ EVERY' [ minus_permute_intro_tac ctxt' p,
eqvt_stac ctxt',
helper_tac false prm p ctxt' ]
@@ -199,7 +199,7 @@
(if member same_name Ps (real_head_of t) then tac1 prm else tac2 prm) i
in
EVERY1 [ eqvt_stac ctxt',
- rtac prem',
+ resolve_tac ctxt' [prem'],
RANGE (map (SUBGOAL o select) prems) ]
end) ctxt
@@ -217,8 +217,9 @@
val simp = asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps ss)
in
Goal.prove ctxt [] [] fresh_goal
- (K (HEADGOAL (rtac @{thm at_set_avoiding2}
- THEN_ALL_NEW EVERY' [cut_facts_tac user_thm, REPEAT o etac @{thm conjE}, simp])))
+ (K (HEADGOAL (resolve_tac ctxt @{thms at_set_avoiding2}
+ THEN_ALL_NEW EVERY' [cut_facts_tac user_thm, REPEAT o
+ eresolve_tac ctxt @{thms conjE}, simp])))
end
val supp_perm_eq' = @{lemma "fresh_star (supp (permute p x)) q ==> permute p x == permute (q + p) x"
@@ -238,27 +239,27 @@
val avoid_trm' = subst_free (param_trms ~~ prm_trms) avoid_trm
val concl_args' = map (subst_free (param_trms ~~ prm_trms)) concl_args
- val user_thm' = map (cterm_instantiate (intr_cvars ~~ prms)) user_thm
+ val user_thm' = map (infer_instantiate ctxt (map (#1 o dest_Var o Thm.term_of) intr_cvars ~~ prms)) user_thm
|> map (full_simplify (put_simpset HOL_ss ctxt addsimps (@{thm fresh_star_Pair}::prems)))
val fthm = fresh_thm ctxt user_thm' (Thm.term_of p) (Thm.term_of c) concl_args' avoid_trm'
val (([(_, q)], fprop :: fresh_eqs), ctxt') = Obtain.result
- (K (EVERY1 [etac @{thm exE},
+ (K (EVERY1 [eresolve_tac ctxt @{thms exE},
full_simp_tac (put_simpset HOL_basic_ss ctxt
addsimps @{thms supp_Pair fresh_star_Un}),
- REPEAT o etac @{thm conjE},
- dtac fresh_star_plus,
- REPEAT o dtac supp_perm_eq'])) [fthm] ctxt
+ REPEAT o eresolve_tac ctxt @{thms conjE},
+ dresolve_tac ctxt [fresh_star_plus],
+ REPEAT o dresolve_tac ctxt [supp_perm_eq']])) [fthm] ctxt
val expand_conv = Conv.try_conv (Conv.rewrs_conv fresh_eqs)
fun expand_conv_bot ctxt = Conv.bottom_conv (K expand_conv) ctxt
- val cperms = map (Thm.cterm_of ctxt o perm_const) prm_tys
+ val cperms = map (Thm.cterm_of ctxt' o perm_const) prm_tys
val qp_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 (mk_cplus q p) ct2) cperms prms
val prem' = prem
- |> cterm_instantiate (intr_cvars ~~ qp_prms)
- |> eqvt_srule ctxt
+ |> infer_instantiate ctxt' (map (#1 o dest_Var o Thm.term_of) intr_cvars ~~ qp_prms)
+ |> eqvt_srule ctxt'
val fprop' = eqvt_srule ctxt' fprop
val tac_fresh = simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [fprop'])
@@ -268,8 +269,8 @@
(* for non-inductive premises *)
fun tac2 prm =
- EVERY' [ minus_permute_intro_tac (mk_cplus q p),
- eqvt_stac ctxt,
+ EVERY' [ minus_permute_intro_tac ctxt' (mk_cplus q p),
+ eqvt_stac ctxt',
helper_tac false prm (mk_cplus q p) ctxt' ]
fun select prm (t, i) =
@@ -279,11 +280,11 @@
(fn {context = ctxt'', ...} =>
EVERY1 [ CONVERSION (expand_conv_bot ctxt''),
eqvt_stac ctxt'',
- rtac prem',
+ resolve_tac ctxt'' [prem'],
RANGE (tac_fresh :: map (SUBGOAL o select) prems) ])
|> singleton (Proof_Context.export ctxt' ctxt)
in
- rtac side_thm 1
+ resolve_tac ctxt [side_thm] 1
end) ctxt
fun case_tac ctxt Ps avoid avoid_trm intr_cvars param_trms prem user_thm concl_args =
@@ -291,17 +292,17 @@
val tac1 = non_binder_tac prem intr_cvars Ps ctxt
val tac2 = binder_tac prem intr_cvars param_trms Ps user_thm avoid_trm concl_args ctxt
in
- EVERY' [ rtac @{thm allI}, rtac @{thm allI},
+ EVERY' [ resolve_tac ctxt @{thms allI}, resolve_tac ctxt @{thms allI},
if null avoid then tac1 else tac2 ]
end
fun prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms concl_args
- {prems, context} =
+ {prems, context = ctxt} =
let
val cases_tac =
- map7 (case_tac context Ps) avoids avoid_trms intr_cvars param_trms prems user_thms concl_args
+ map7 (case_tac ctxt Ps) avoids avoid_trms intr_cvars param_trms prems user_thms concl_args
in
- EVERY1 [ DETERM o rtac raw_induct, RANGE cases_tac ]
+ EVERY1 [ DETERM o resolve_tac ctxt [raw_induct], RANGE cases_tac ]
end
val normalise = @{lemma "(Q --> (!p c. P p c)) ==> (!!c. Q ==> P (0::perm) c)" by simp}