--- a/src/HOL/Nominal/nominal_datatype.ML Fri Dec 02 10:31:47 2011 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Fri Dec 02 13:38:24 2011 +0100
@@ -320,7 +320,7 @@
Const ("Nominal.perm", T) $ pi $ Free (x, T2))
end)
(perm_names_types ~~ perm_indnames))))
- (fn _ => EVERY [indtac induct perm_indnames 1,
+ (fn _ => EVERY [Datatype_Aux.ind_tac induct perm_indnames 1,
ALLGOALS (asm_full_simp_tac
(global_simpset_of thy2 addsimps [perm_fun_def]))])),
length new_type_names));
@@ -341,7 +341,7 @@
Free (x, T)))
(perm_names ~~
map body_type perm_types ~~ perm_indnames)))))
- (fn _ => EVERY [indtac induct perm_indnames 1,
+ (fn _ => EVERY [Datatype_Aux.ind_tac induct perm_indnames 1,
ALLGOALS (asm_full_simp_tac (global_simpset_of thy2))])),
length new_type_names))
end)
@@ -376,7 +376,7 @@
end)
(perm_names ~~
map body_type perm_types ~~ perm_indnames)))))
- (fn _ => EVERY [indtac induct perm_indnames 1,
+ (fn _ => EVERY [Datatype_Aux.ind_tac induct perm_indnames 1,
ALLGOALS (asm_full_simp_tac (global_simpset_of thy2 addsimps [pt2', pt2_ax]))]))),
length new_type_names)
end) atoms;
@@ -412,7 +412,7 @@
end)
(perm_names ~~
map body_type perm_types ~~ perm_indnames))))))
- (fn _ => EVERY [indtac induct perm_indnames 1,
+ (fn _ => EVERY [Datatype_Aux.ind_tac induct perm_indnames 1,
ALLGOALS (asm_full_simp_tac (global_simpset_of thy2 addsimps [pt3', pt3_rev', pt3_ax]))]))),
length new_type_names)
end) atoms;
@@ -464,7 +464,7 @@
perm2 $ (perm3 $ pi1 $ pi2) $ (perm1 $ pi1 $ Free (x, T)))
end)
(perm_names ~~ Ts ~~ perm_indnames)))))
- (fn _ => EVERY [indtac induct perm_indnames 1,
+ (fn _ => EVERY [Datatype_Aux.ind_tac induct perm_indnames 1,
ALLGOALS (asm_full_simp_tac simps)]))
in
fold (fn (s, tvs) => fn thy => AxClass.prove_arity
@@ -599,7 +599,7 @@
Free ("pi", permT) $ Free (x, T)))
end) (rep_set_names'' ~~ recTs' ~~ perm_indnames')))))
(fn _ => EVERY
- [indtac rep_induct [] 1,
+ [Datatype_Aux.ind_tac rep_induct [] 1,
ALLGOALS (simp_tac (global_simpset_of thy4 addsimps
(Thm.symmetric perm_fun_def :: abs_perm))),
ALLGOALS (resolve_tac rep_intrs THEN_ALL_NEW assume_tac)])),
@@ -1071,7 +1071,7 @@
(Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
(fn {prems, ...} => EVERY
[rtac indrule_lemma' 1,
- (indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
+ (Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
EVERY (map (fn (prem, r) => (EVERY
[REPEAT (eresolve_tac Abs_inverse_thms' 1),
simp_tac (HOL_basic_ss addsimps [Thm.symmetric r]) 1,
@@ -1099,7 +1099,7 @@
Const ("Finite_Set.finite", HOLogic.mk_setT atomT --> HOLogic.boolT) $
(Const ("Nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T)))
(indnames ~~ recTs)))))
- (fn _ => indtac dt_induct indnames 1 THEN
+ (fn _ => Datatype_Aux.ind_tac dt_induct indnames 1 THEN
ALLGOALS (asm_full_simp_tac (global_simpset_of thy8 addsimps
(abs_supp @ supp_atm @
Global_Theory.get_thms thy8 ("fs_" ^ Long_Name.base_name atom ^ "1") @
@@ -1312,7 +1312,7 @@
val th = Goal.prove context [] []
(augment_sort thy9 fs_cp_sort aux_ind_concl)
(fn {context = context1, ...} =>
- EVERY (indtac dt_induct tnames 1 ::
+ EVERY (Datatype_Aux.ind_tac dt_induct tnames 1 ::
maps (fn ((_, (_, _, constrs)), (_, constrs')) =>
map (fn ((cname, cargs), is) =>
REPEAT (rtac allI 1) THEN
--- a/src/HOL/Tools/Datatype/datatype.ML Fri Dec 02 10:31:47 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Fri Dec 02 13:38:24 2011 +0100
@@ -435,7 +435,7 @@
Skip_Proof.prove_global thy5 [] []
(HOLogic.mk_Trueprop (Datatype_Aux.mk_conj ind_concl1))
(fn _ => EVERY
- [(Datatype_Aux.indtac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
+ [(Datatype_Aux.ind_tac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
REPEAT (EVERY
[rtac allI 1, rtac impI 1,
Datatype_Aux.exh_tac (exh_thm_of dt_info) 1,
@@ -461,7 +461,7 @@
Skip_Proof.prove_global thy5 [] []
(HOLogic.mk_Trueprop (Datatype_Aux.mk_conj ind_concl2))
(fn _ =>
- EVERY [(Datatype_Aux.indtac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
+ EVERY [(Datatype_Aux.ind_tac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
rewrite_goals_tac rewrites,
REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
@@ -497,7 +497,7 @@
else
drop (length newTs) (Datatype_Aux.split_conj_thm
(Skip_Proof.prove_global thy5 [] [] iso_t (fn _ => EVERY
- [(Datatype_Aux.indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
+ [(Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
REPEAT (rtac TrueI 1),
rewrite_goals_tac (mk_meta_eq @{thm choice_eq} ::
Thm.symmetric (mk_meta_eq @{thm fun_eq_iff}) :: range_eqs),
@@ -653,7 +653,7 @@
(fn {prems, ...} =>
EVERY
[rtac indrule_lemma' 1,
- (Datatype_Aux.indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
+ (Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
EVERY (map (fn (prem, r) => (EVERY
[REPEAT (eresolve_tac Abs_inverse_thms 1),
simp_tac (HOL_basic_ss addsimps (Thm.symmetric r :: Rep_inverse_thms')) 1,
--- a/src/HOL/Tools/Datatype/datatype_aux.ML Fri Dec 02 10:31:47 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Fri Dec 02 13:38:24 2011 +0100
@@ -52,7 +52,7 @@
val app_bnds : term -> int -> term
- val indtac : thm -> string list -> int -> tactic
+ val ind_tac : thm -> string list -> int -> tactic
val exh_tac : (string -> thm) -> int -> tactic
exception Datatype
@@ -127,7 +127,7 @@
(* instantiate induction rule *)
-fun indtac indrule indnames = CSUBGOAL (fn (cgoal, i) =>
+fun ind_tac indrule indnames = CSUBGOAL (fn (cgoal, i) =>
let
val cert = cterm_of (Thm.theory_of_cterm cgoal);
val goal = term_of cgoal;
--- a/src/HOL/Tools/Function/size.ML Fri Dec 02 10:31:47 2011 +0100
+++ b/src/HOL/Tools/Function/size.ML Fri Dec 02 13:38:24 2011 +0100
@@ -166,7 +166,7 @@
map (mk_unfolded_size_eq (AList.lookup op =
(new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs)
(xs ~~ recTs2 ~~ rec_combs2))))
- (fn _ => (indtac induct xs THEN_ALL_NEW asm_simp_tac simpset1) 1));
+ (fn _ => (Datatype_Aux.ind_tac induct xs THEN_ALL_NEW asm_simp_tac simpset1) 1));
val unfolded_size_eqs1 = prove_unfolded_size_eqs param_size fs;
val unfolded_size_eqs2 = prove_unfolded_size_eqs (K NONE) fs';