--- a/Nominal/nominal_inductive.ML Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_inductive.ML Thu Jul 09 02:32:46 2015 +0100
@@ -35,7 +35,7 @@
| 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
| real_head_of (Const (@{const_name All}, _) $ Abs (_, _, t)) = real_head_of t
- | real_head_of (Const ("HOL.induct_forall", _) $ Abs (_, _, t)) = real_head_of t
+ | real_head_of (Const (@{const_name HOL.induct_forall}, _) $ Abs (_, _, t)) = real_head_of t
| real_head_of t = head_of t
@@ -81,7 +81,7 @@
end
fun induct_forall_const T =
- Const ("HOL.induct_forall", (T --> @{typ bool}) --> @{typ bool})
+ Const (@{const_name HOL.induct_forall}, (T --> @{typ bool}) --> @{typ bool})
fun mk_induct_forall (a, T) t =
induct_forall_const T $ Abs (a, T, t)
@@ -156,7 +156,7 @@
val all_elims =
let
fun spec' ct =
- Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}
+ Drule.instantiate' [SOME (Thm.ctyp_of_cterm ct)] [NONE, SOME ct] @{thm spec}
in
fold (fn ct => fn th => th RS spec' ct)
end
@@ -172,34 +172,33 @@
|> flag ? (all_elims [p])
|> flag ? (eqvt_srule context)
in
- asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps (prm' :: @{thms 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, params, prems, ...} =>
+ Subgoal.SUBPROOF (fn {context = ctxt', params, prems, ...} =>
let
- val thy = Proof_Context.theory_of context
val (prms, p, _) = split_last2 (map snd params)
- val prm_tys = map (fastype_of o term_of) prms
- val cperms = map (cterm_of thy o perm_const) prm_tys
+ 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)
|> eqvt_srule ctxt
(* for inductive-premises*)
- fun tac1 prm = helper_tac true prm p context
+ fun tac1 prm = helper_tac true prm p ctxt'
(* for non-inductive premises *)
fun tac2 prm =
EVERY' [ minus_permute_intro_tac p,
- eqvt_stac context,
- helper_tac false prm p context ]
+ 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 context,
+ EVERY1 [ eqvt_stac ctxt',
rtac prem',
RANGE (map (SUBGOAL o select) prems) ]
end) ctxt
@@ -232,9 +231,8 @@
fun binder_tac prem intr_cvars param_trms Ps user_thm avoid_trm concl_args ctxt =
Subgoal.FOCUS (fn {context = ctxt, params, prems, concl, ...} =>
let
- val thy = Proof_Context.theory_of ctxt
val (prms, p, c) = split_last2 (map snd params)
- val prm_trms = map term_of prms
+ val prm_trms = map Thm.term_of prms
val prm_tys = map fastype_of prm_trms
val avoid_trm' = subst_free (param_trms ~~ prm_trms) avoid_trm
@@ -243,7 +241,7 @@
val user_thm' = map (cterm_instantiate (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' (term_of p) (term_of c) concl_args' avoid_trm'
+ 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},
@@ -256,7 +254,7 @@
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 (cterm_of thy 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)
@@ -277,13 +275,13 @@
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' [] [] (term_of concl)
- (fn {context, ...} =>
- EVERY1 [ CONVERSION (expand_conv_bot context),
- eqvt_stac context,
+ val side_thm = Goal.prove ctxt' [] [] (Thm.term_of concl)
+ (fn {context = ctxt'', ...} =>
+ EVERY1 [ CONVERSION (expand_conv_bot ctxt''),
+ eqvt_stac ctxt'',
rtac prem',
RANGE (tac_fresh :: map (SUBGOAL o select) prems) ])
- |> singleton (Proof_Context.export ctxt' ctxt)
+ |> singleton (Proof_Context.export ctxt' ctxt)
in
rtac side_thm 1
end) ctxt
@@ -310,23 +308,22 @@
fun prove_strong_inductive pred_names rule_names avoids raw_induct intrs ctxt =
let
- val thy = Proof_Context.theory_of ctxt
val ((_, [raw_induct']), ctxt') = Variable.import true [raw_induct] ctxt
val (ind_prems, ind_concl) = raw_induct'
- |> prop_of
+ |> Thm.prop_of
|> Logic.strip_horn
|>> map strip_full_horn
val params = map (fn (x, _, _) => x) ind_prems
val param_trms = (map o map) Free params
- val intr_vars_tys = map (fn t => rev (Term.add_vars (prop_of t) [])) intrs
+ val intr_vars_tys = map (fn t => rev (Term.add_vars (Thm.prop_of t) [])) intrs
val intr_vars = (map o map) fst intr_vars_tys
val intr_vars_substs = map2 (curry (op ~~)) intr_vars param_trms
- val intr_cvars = (map o map) (cterm_of thy o Var) intr_vars_tys
+ val intr_cvars = (map o map) (Thm.cterm_of ctxt o Var) intr_vars_tys
val (intr_prems, intr_concls) = intrs
- |> map prop_of
+ |> map Thm.prop_of
|> map2 subst_Vars intr_vars_substs
|> map Logic.strip_horn
|> split_list
@@ -369,7 +366,7 @@
val strong_ind_thms = Goal.prove ctxt [] ind_prems' ind_concl'
(prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms intr_concls_args)
|> singleton (Proof_Context.export ctxt ctxt_outside)
- |> Datatype_Aux.split_conj_thm
+ |> Old_Datatype_Aux.split_conj_thm
|> map (fn thm => thm RS normalise)
|> map (asm_full_simplify (put_simpset HOL_basic_ss ctxt
addsimps @{thms permute_zero induct_rulify}))
@@ -417,7 +414,7 @@
let
(* fixme hack *)
val (((_, ctrms), _), ctxt') = Variable.import true [intr] ctxt
- val trms = map (term_of o snd) ctrms
+ val trms = map (Thm.term_of o snd) ctrms
val ctxt'' = fold Variable.declare_term trms ctxt'
in
map (Syntax.read_term ctxt'') avoid_trms
@@ -439,7 +436,7 @@
val main_parser = Parse.xname -- avoids_parser
in
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "nominal_inductive"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword nominal_inductive}
"prove strong induction theorem for inductive predicate involving nominal datatypes"
(main_parser >> prove_strong_inductive_cmd)
end