# HG changeset patch # User wenzelm # Date 1322829504 -3600 # Node ID 7d7d7af647a9129ab7ec3deffd74748ad9998707 # Parent 1024dd30da42915cd9df544c6e462400f3b72704 tuned signature; diff -r 1024dd30da42 -r 7d7d7af647a9 src/HOL/Nominal/nominal_datatype.ML --- 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 diff -r 1024dd30da42 -r 7d7d7af647a9 src/HOL/Tools/Datatype/datatype.ML --- 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, diff -r 1024dd30da42 -r 7d7d7af647a9 src/HOL/Tools/Datatype/datatype_aux.ML --- 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; diff -r 1024dd30da42 -r 7d7d7af647a9 src/HOL/Tools/Function/size.ML --- 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';