nominal2: comparison Nominal/nominal

equal deleted inserted replaced

-:4af8a92396ce
+:c4f31f1564b7
 Thm.apply (Thm.apply @{cterm "plus :: perm => perm => perm"} p) q
 fun mk_cminus p =
 Thm.apply @{cterm "uminus :: perm => perm"} p
-fun minus_permute_intro_tac p =
+fun minus_permute_intro_tac ctxt p =
-rtac (Drule.instantiate' [] [SOME (mk_cminus p)] @{thm permute_boolE})
+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
 | real_head_of (Const (@{const_name Pure.imp}, _) $ _ $ t) = real_head_of t
 | real_head_of (Const (@{const_name Pure.all}, _) $ Abs (_, _, t)) = real_head_of t
 end
 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 =
 Subgoal.SUBPROOF (fn {context = ctxt', params, prems, ...} =>
 let
 val (prms, p, _) = split_last2 (map snd params)
 val prm_tys = map (fastype_of o Thm.term_of) prms
 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)
+|> infer_instantiate ctxt' (map (#1 o dest_Var o Thm.term_of) intr_cvars ~~ p_prms)
-|> eqvt_srule ctxt
+|> 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' ]
 fun select prm (t, i) =
 (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
 fun fresh_thm ctxt user_thm p c concl_args avoid_trm =
 let
 val ss = @{thms finite_supp supp_Pair finite_Un permute_finite} @
 @{thms fresh_star_Pair fresh_star_permute_iff}
 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}
+(K (HEADGOAL (resolve_tac ctxt @{thms at_set_avoiding2}
-THEN_ALL_NEW EVERY' [cut_facts_tac user_thm, REPEAT o etac @{thm conjE}, simp])))
+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"
 by (simp add: supp_perm_eq)}
 val prm_tys = map fastype_of prm_trms
 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},
+REPEAT o eresolve_tac ctxt @{thms conjE},
-dtac fresh_star_plus,
+dresolve_tac ctxt [fresh_star_plus],
-REPEAT o dtac supp_perm_eq'])) [fthm] ctxt
+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)
+|> infer_instantiate ctxt' (map (#1 o dest_Var o Thm.term_of) intr_cvars ~~ qp_prms)
-|> eqvt_srule ctxt
+|> eqvt_srule ctxt'
 val fprop' = eqvt_srule ctxt' fprop
 val tac_fresh = simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [fprop'])
 (* for inductive-premises*)
 fun tac1 prm = helper_tac true prm (mk_cplus q p) ctxt'
 (* for non-inductive premises *)
 fun tac2 prm =
-EVERY' [ minus_permute_intro_tac (mk_cplus q p),
+EVERY' [ minus_permute_intro_tac ctxt' (mk_cplus q p),
-eqvt_stac ctxt,
+eqvt_stac ctxt',
 helper_tac false prm (mk_cplus q p) ctxt' ]
 fun select prm (t, i) =
 (if member same_name Ps (real_head_of t) then tac1 prm else tac2 prm) i
 val side_thm = Goal.prove ctxt' [] [] (Thm.term_of concl)
 (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 =
 let
 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}
 fun prove_strong_inductive pred_names rule_names avoids raw_induct intrs ctxt =

branch	Nominal2-Isabelle2016
changeset 3243	c4f31f1564b7
parent 3239	67370521c09c
child 3245	017e33849f4d