--- a/src/CCL/CCL.thy Sat Feb 27 23:13:01 2010 +0100
+++ b/src/CCL/CCL.thy Sun Feb 28 22:30:51 2010 +0100
@@ -193,7 +193,7 @@
fun mk_inj_lemmas r = [@{thm arg_cong}] RL [r RS (r RS @{thm eq_lemma})]
val inj_lemmas = maps mk_inj_lemmas rews
in
- CHANGED (REPEAT (ares_tac [iffI, allI, conjI] i ORELSE
+ CHANGED (REPEAT (ares_tac [@{thm iffI}, @{thm allI}, @{thm conjI}] i ORELSE
eresolve_tac inj_lemmas i ORELSE
asm_simp_tac (simpset_of ctxt addsimps rews) i))
end;
@@ -242,7 +242,7 @@
val eq_lemma = thm "eq_lemma";
val distinctness = thm "distinctness";
fun mk_lemma (ra,rb) = [lemma] RL [ra RS (rb RS eq_lemma)] RL
- [distinctness RS notE,sym RS (distinctness RS notE)]
+ [distinctness RS notE, @{thm sym} RS (distinctness RS notE)]
in
fun mk_lemmas rls = maps mk_lemma (mk_combs pair rls)
fun mk_dstnct_rls thy xs = mk_combs (mk_thm_str thy) xs
@@ -258,7 +258,7 @@
let
fun mk_raw_dstnct_thm rls s =
Goal.prove_global @{theory} [] [] (Syntax.read_prop_global @{theory} s)
- (fn _=> rtac notI 1 THEN eresolve_tac rls 1)
+ (fn _=> rtac @{thm notI} 1 THEN eresolve_tac rls 1)
in map (mk_raw_dstnct_thm caseB_lemmas)
(mk_dstnct_rls @{theory} ["bot","true","false","pair","lambda"]) end
@@ -406,9 +406,9 @@
"~ false [= lam x. f(x)"
"~ lam x. f(x) [= false"
by (tactic {*
- REPEAT (rtac notI 1 THEN
+ REPEAT (rtac @{thm notI} 1 THEN
dtac @{thm case_pocong} 1 THEN
- etac rev_mp 5 THEN
+ etac @{thm rev_mp} 5 THEN
ALLGOALS (simp_tac @{simpset}) THEN
REPEAT (resolve_tac [@{thm po_refl}, @{thm npo_lam_bot}] 1)) *})
--- a/src/CCL/Type.thy Sat Feb 27 23:13:01 2010 +0100
+++ b/src/CCL/Type.thy Sun Feb 28 22:30:51 2010 +0100
@@ -127,7 +127,7 @@
fun mk_ncanT_tac top_crls crls =
SUBPROOF (fn {context = ctxt, prems = major :: prems, ...} =>
resolve_tac ([major] RL top_crls) 1 THEN
- REPEAT_SOME (eresolve_tac (crls @ [exE, @{thm bexE}, conjE, disjE])) THEN
+ REPEAT_SOME (eresolve_tac (crls @ [@{thm exE}, @{thm bexE}, @{thm conjE}, @{thm disjE}])) THEN
ALLGOALS (asm_simp_tac (simpset_of ctxt)) THEN
ALLGOALS (ares_tac (prems RL [@{thm lem}]) ORELSE' etac @{thm bspec}) THEN
safe_tac (claset_of ctxt addSIs prems))
@@ -498,7 +498,7 @@
fun EQgen_tac ctxt rews i =
SELECT_GOAL
(TRY (safe_tac (claset_of ctxt)) THEN
- resolve_tac ((rews @ [refl]) RL ((rews @ [refl]) RL [@{thm ssubst_pair}])) i THEN
+ resolve_tac ((rews @ [@{thm refl}]) RL ((rews @ [@{thm refl}]) RL [@{thm ssubst_pair}])) i THEN
ALLGOALS (simp_tac (simpset_of ctxt)) THEN
ALLGOALS EQgen_raw_tac) i
*}
--- a/src/FOL/IFOL.thy Sat Feb 27 23:13:01 2010 +0100
+++ b/src/FOL/IFOL.thy Sun Feb 28 22:30:51 2010 +0100
@@ -890,45 +890,4 @@
lemma all_conj_distrib:
"(ALL x. P(x) & Q(x)) <-> ((ALL x. P(x)) & (ALL x. Q(x)))" by iprover
-
-subsection {* Legacy ML bindings *}
-
-ML {*
-val refl = @{thm refl}
-val trans = @{thm trans}
-val sym = @{thm sym}
-val subst = @{thm subst}
-val ssubst = @{thm ssubst}
-val conjI = @{thm conjI}
-val conjE = @{thm conjE}
-val conjunct1 = @{thm conjunct1}
-val conjunct2 = @{thm conjunct2}
-val disjI1 = @{thm disjI1}
-val disjI2 = @{thm disjI2}
-val disjE = @{thm disjE}
-val impI = @{thm impI}
-val impE = @{thm impE}
-val mp = @{thm mp}
-val rev_mp = @{thm rev_mp}
-val TrueI = @{thm TrueI}
-val FalseE = @{thm FalseE}
-val iff_refl = @{thm iff_refl}
-val iff_trans = @{thm iff_trans}
-val iffI = @{thm iffI}
-val iffE = @{thm iffE}
-val iffD1 = @{thm iffD1}
-val iffD2 = @{thm iffD2}
-val notI = @{thm notI}
-val notE = @{thm notE}
-val allI = @{thm allI}
-val allE = @{thm allE}
-val spec = @{thm spec}
-val exI = @{thm exI}
-val exE = @{thm exE}
-val eq_reflection = @{thm eq_reflection}
-val iff_reflection = @{thm iff_reflection}
-val meta_eq_to_obj_eq = @{thm meta_eq_to_obj_eq}
-val meta_eq_to_iff = @{thm meta_eq_to_iff}
-*}
-
end
--- a/src/ZF/Datatype_ZF.thy Sat Feb 27 23:13:01 2010 +0100
+++ b/src/ZF/Datatype_ZF.thy Sun Feb 28 22:30:51 2010 +0100
@@ -92,7 +92,7 @@
else ();
val goal = Logic.mk_equals (old, new)
val thm = Goal.prove (Simplifier.the_context ss) [] [] goal
- (fn _ => rtac iff_reflection 1 THEN
+ (fn _ => rtac @{thm iff_reflection} 1 THEN
simp_tac (Simplifier.inherit_context ss datatype_ss addsimps #free_iffs lcon_info) 1)
handle ERROR msg =>
(warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Syntax.string_of_term_global sg goal);
--- a/src/ZF/Tools/datatype_package.ML Sat Feb 27 23:13:01 2010 +0100
+++ b/src/ZF/Tools/datatype_package.ML Sun Feb 28 22:30:51 2010 +0100
@@ -281,7 +281,7 @@
list_comb (case_free, args)));
val case_trans = hd con_defs RS @{thm def_trans}
- and split_trans = Pr.split_eq RS meta_eq_to_obj_eq RS @{thm trans};
+ and split_trans = Pr.split_eq RS @{thm meta_eq_to_obj_eq} RS @{thm trans};
fun prove_case_eqn (arg, con_def) =
Goal.prove_global thy1 [] []
@@ -290,7 +290,9 @@
(fn _ => EVERY
[rewrite_goals_tac [con_def],
rtac case_trans 1,
- REPEAT (resolve_tac [refl, split_trans, Su.case_inl RS trans, Su.case_inr RS trans] 1)]);
+ REPEAT
+ (resolve_tac [@{thm refl}, split_trans,
+ Su.case_inl RS @{thm trans}, Su.case_inr RS @{thm trans}] 1)]);
val free_iffs = map Drule.export_without_context (con_defs RL [@{thm def_swap_iff}]);
@@ -321,7 +323,7 @@
args)),
subst_rec (Term.betapplys (recursor_case, args))));
- val recursor_trans = recursor_def RS @{thm def_Vrecursor} RS trans;
+ val recursor_trans = recursor_def RS @{thm def_Vrecursor} RS @{thm trans};
fun prove_recursor_eqn arg =
Goal.prove_global thy1 [] []
--- a/src/ZF/Tools/induct_tacs.ML Sat Feb 27 23:13:01 2010 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Sun Feb 28 22:30:51 2010 +0100
@@ -136,7 +136,7 @@
rec_rewrites = recursor_eqns,
case_rewrites = case_eqns,
induct = induct,
- mutual_induct = TrueI, (*No need for mutual induction*)
+ mutual_induct = @{thm TrueI}, (*No need for mutual induction*)
exhaustion = elim};
val con_info =
--- a/src/ZF/Tools/inductive_package.ML Sat Feb 27 23:13:01 2010 +0100
+++ b/src/ZF/Tools/inductive_package.ML Sun Feb 28 22:30:51 2010 +0100
@@ -222,7 +222,7 @@
rtac disjIn 2,
(*Not ares_tac, since refl must be tried before equality assumptions;
backtracking may occur if the premises have extra variables!*)
- DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 2 APPEND assume_tac 2),
+ DEPTH_SOLVE_1 (resolve_tac [@{thm refl}, @{thm exI}, @{thm conjI}] 2 APPEND assume_tac 2),
(*Now solve the equations like Tcons(a,f) = Inl(?b4)*)
rewrite_goals_tac con_defs,
REPEAT (rtac @{thm refl} 2),
@@ -310,7 +310,7 @@
Intro rules with extra Vars in premises still cause some backtracking *)
fun ind_tac [] 0 = all_tac
| ind_tac(prem::prems) i =
- DEPTH_SOLVE_1 (ares_tac [prem, refl] i) THEN ind_tac prems (i-1);
+ DEPTH_SOLVE_1 (ares_tac [prem, @{thm refl}] i) THEN ind_tac prems (i-1);
val pred = Free(pred_name, Ind_Syntax.iT --> FOLogic.oT);
@@ -332,7 +332,7 @@
setSolver (mk_solver "minimal"
(fn prems => resolve_tac (triv_rls@prems)
ORELSE' assume_tac
- ORELSE' etac FalseE));
+ ORELSE' etac @{thm FalseE}));
val quant_induct =
Goal.prove_global thy1 [] ind_prems
@@ -470,11 +470,11 @@
(mut_ss addsimps @{thms conj_simps} @ @{thms imp_simps} @ @{thms quant_simps}) 1
THEN
(*unpackage and use "prem" in the corresponding place*)
- REPEAT (rtac impI 1) THEN
+ REPEAT (rtac @{thm impI} 1) THEN
rtac (rewrite_rule all_defs prem) 1 THEN
(*prem must not be REPEATed below: could loop!*)
- DEPTH_SOLVE (FIRSTGOAL (ares_tac [impI] ORELSE'
- eresolve_tac (conjE::mp::cmonos))))
+ DEPTH_SOLVE (FIRSTGOAL (ares_tac [@{thm impI}] ORELSE'
+ eresolve_tac (@{thm conjE} :: @{thm mp} :: cmonos))))
) i)
THEN mutual_ind_tac prems (i-1);
@@ -485,7 +485,7 @@
(fn {prems, ...} => EVERY
[rtac (quant_induct RS lemma) 1,
mutual_ind_tac (rev prems) (length prems)])
- else TrueI;
+ else @{thm TrueI};
(** Uncurrying the predicate in the ordinary induction rule **)
@@ -498,7 +498,7 @@
cterm_of thy1 elem_tuple)]);
(*strip quantifier and the implication*)
- val induct0 = inst (quant_induct RS spec RSN (2, @{thm rev_mp}));
+ val induct0 = inst (quant_induct RS @{thm spec} RSN (2, @{thm rev_mp}));
val Const (@{const_name Trueprop}, _) $ (pred_var $ _) = concl_of induct0
@@ -521,7 +521,7 @@
else
(thy1
|> PureThy.add_thms [((Binding.name (co_prefix ^ "induct"), raw_induct), [])]
- |> apfst hd |> Library.swap, TrueI)
+ |> apfst hd |> Library.swap, @{thm TrueI})
and defs = big_rec_def :: part_rec_defs
--- a/src/ZF/Tools/primrec_package.ML Sat Feb 27 23:13:01 2010 +0100
+++ b/src/ZF/Tools/primrec_package.ML Sun Feb 28 22:30:51 2010 +0100
@@ -175,7 +175,7 @@
val eqn_thms =
eqn_terms |> map (fn t =>
Goal.prove_global thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t)
- (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1]));
+ (fn _ => EVERY [rewrite_goals_tac rewrites, rtac @{thm refl} 1]));
val (eqn_thms', thy2) =
thy1
--- a/src/ZF/Tools/typechk.ML Sat Feb 27 23:13:01 2010 +0100
+++ b/src/ZF/Tools/typechk.ML Sun Feb 28 22:30:51 2010 +0100
@@ -98,7 +98,7 @@
(*Instantiates variables in typing conditions.
drawback: does not simplify conjunctions*)
fun type_solver_tac ctxt hyps = SELECT_GOAL
- (DEPTH_SOLVE (etac FalseE 1
+ (DEPTH_SOLVE (etac @{thm FalseE} 1
ORELSE basic_res_tac 1
ORELSE (ares_tac hyps 1
APPEND typecheck_step_tac (tcset_of ctxt))));
--- a/src/ZF/UNITY/Constrains.thy Sat Feb 27 23:13:01 2010 +0100
+++ b/src/ZF/UNITY/Constrains.thy Sun Feb 28 22:30:51 2010 +0100
@@ -484,9 +484,9 @@
REPEAT (force_tac css 2),
full_simp_tac (ss addsimps (Program_Defs.get ctxt)) 1,
ALLGOALS (clarify_tac cs),
- REPEAT (FIRSTGOAL (etac disjE)),
+ REPEAT (FIRSTGOAL (etac @{thm disjE})),
ALLGOALS (clarify_tac cs),
- REPEAT (FIRSTGOAL (etac disjE)),
+ REPEAT (FIRSTGOAL (etac @{thm disjE})),
ALLGOALS (clarify_tac cs),
ALLGOALS (asm_full_simp_tac ss),
ALLGOALS (clarify_tac cs)])
--- a/src/ZF/UNITY/SubstAx.thy Sat Feb 27 23:13:01 2010 +0100
+++ b/src/ZF/UNITY/SubstAx.thy Sun Feb 28 22:30:51 2010 +0100
@@ -366,7 +366,7 @@
(* proving the domain part *)
clarify_tac cs 3, dtac @{thm swap} 3, force_tac css 4,
rtac @{thm ReplaceI} 3, force_tac css 3, force_tac css 4,
- asm_full_simp_tac ss 3, rtac conjI 3, simp_tac ss 4,
+ asm_full_simp_tac ss 3, rtac @{thm conjI} 3, simp_tac ss 4,
REPEAT (rtac @{thm state_update_type} 3),
constrains_tac ctxt 1,
ALLGOALS (clarify_tac cs),
--- a/src/ZF/arith_data.ML Sat Feb 27 23:13:01 2010 +0100
+++ b/src/ZF/arith_data.ML Sun Feb 28 22:30:51 2010 +0100
@@ -163,9 +163,9 @@
val prove_conv = prove_conv "nateq_cancel_numerals"
val mk_bal = FOLogic.mk_eq
val dest_bal = FOLogic.dest_eq
- val bal_add1 = @{thm eq_add_iff} RS iff_trans
- val bal_add2 = @{thm eq_add_iff} RS iff_trans
- fun trans_tac _ = gen_trans_tac iff_trans
+ val bal_add1 = @{thm eq_add_iff} RS @{thm iff_trans}
+ val bal_add2 = @{thm eq_add_iff} RS @{thm iff_trans}
+ fun trans_tac _ = gen_trans_tac @{thm iff_trans}
end;
structure EqCancelNumerals = CancelNumeralsFun(EqCancelNumeralsData);
@@ -176,9 +176,9 @@
val prove_conv = prove_conv "natless_cancel_numerals"
val mk_bal = FOLogic.mk_binrel "Ordinal.lt"
val dest_bal = FOLogic.dest_bin "Ordinal.lt" iT
- val bal_add1 = @{thm less_add_iff} RS iff_trans
- val bal_add2 = @{thm less_add_iff} RS iff_trans
- fun trans_tac _ = gen_trans_tac iff_trans
+ val bal_add1 = @{thm less_add_iff} RS @{thm iff_trans}
+ val bal_add2 = @{thm less_add_iff} RS @{thm iff_trans}
+ fun trans_tac _ = gen_trans_tac @{thm iff_trans}
end;
structure LessCancelNumerals = CancelNumeralsFun(LessCancelNumeralsData);
@@ -189,9 +189,9 @@
val prove_conv = prove_conv "natdiff_cancel_numerals"
val mk_bal = FOLogic.mk_binop "Arith.diff"
val dest_bal = FOLogic.dest_bin "Arith.diff" iT
- val bal_add1 = @{thm diff_add_eq} RS trans
- val bal_add2 = @{thm diff_add_eq} RS trans
- fun trans_tac _ = gen_trans_tac trans
+ val bal_add1 = @{thm diff_add_eq} RS @{thm trans}
+ val bal_add2 = @{thm diff_add_eq} RS @{thm trans}
+ fun trans_tac _ = gen_trans_tac @{thm trans}
end;
structure DiffCancelNumerals = CancelNumeralsFun(DiffCancelNumeralsData);
--- a/src/ZF/int_arith.ML Sat Feb 27 23:13:01 2010 +0100
+++ b/src/ZF/int_arith.ML Sun Feb 28 22:30:51 2010 +0100
@@ -128,7 +128,7 @@
(*To evaluate binary negations of coefficients*)
val zminus_simps = @{thms NCons_simps} @
- [@{thm integ_of_minus} RS sym,
+ [@{thm integ_of_minus} RS @{thm sym},
@{thm bin_minus_1}, @{thm bin_minus_0}, @{thm bin_minus_Pls}, @{thm bin_minus_Min},
@{thm bin_pred_1}, @{thm bin_pred_0}, @{thm bin_pred_Pls}, @{thm bin_pred_Min}];
@@ -144,7 +144,7 @@
(*combine unary minus with numeric literals, however nested within a product*)
val int_mult_minus_simps =
- [@{thm zmult_assoc}, @{thm zmult_zminus} RS sym, int_minus_mult_eq_1_to_2];
+ [@{thm zmult_assoc}, @{thm zmult_zminus} RS @{thm sym}, int_minus_mult_eq_1_to_2];
fun prep_simproc thy (name, pats, proc) =
Simplifier.simproc thy name pats proc;
@@ -156,7 +156,7 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff 1
val find_first_coeff = find_first_coeff []
- fun trans_tac _ = ArithData.gen_trans_tac iff_trans
+ fun trans_tac _ = ArithData.gen_trans_tac @{thm iff_trans}
val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac}
val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys
@@ -179,8 +179,8 @@
val prove_conv = ArithData.prove_conv "inteq_cancel_numerals"
val mk_bal = FOLogic.mk_eq
val dest_bal = FOLogic.dest_eq
- val bal_add1 = @{thm eq_add_iff1} RS iff_trans
- val bal_add2 = @{thm eq_add_iff2} RS iff_trans
+ val bal_add1 = @{thm eq_add_iff1} RS @{thm iff_trans}
+ val bal_add2 = @{thm eq_add_iff2} RS @{thm iff_trans}
);
structure LessCancelNumerals = CancelNumeralsFun
@@ -188,8 +188,8 @@
val prove_conv = ArithData.prove_conv "intless_cancel_numerals"
val mk_bal = FOLogic.mk_binrel @{const_name "zless"}
val dest_bal = FOLogic.dest_bin @{const_name "zless"} @{typ i}
- val bal_add1 = @{thm less_add_iff1} RS iff_trans
- val bal_add2 = @{thm less_add_iff2} RS iff_trans
+ val bal_add1 = @{thm less_add_iff1} RS @{thm iff_trans}
+ val bal_add2 = @{thm less_add_iff2} RS @{thm iff_trans}
);
structure LeCancelNumerals = CancelNumeralsFun
@@ -197,8 +197,8 @@
val prove_conv = ArithData.prove_conv "intle_cancel_numerals"
val mk_bal = FOLogic.mk_binrel @{const_name "zle"}
val dest_bal = FOLogic.dest_bin @{const_name "zle"} @{typ i}
- val bal_add1 = @{thm le_add_iff1} RS iff_trans
- val bal_add2 = @{thm le_add_iff2} RS iff_trans
+ val bal_add1 = @{thm le_add_iff1} RS @{thm iff_trans}
+ val bal_add2 = @{thm le_add_iff2} RS @{thm iff_trans}
);
val cancel_numerals =
@@ -232,9 +232,9 @@
val dest_sum = dest_sum
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff 1
- val left_distrib = @{thm left_zadd_zmult_distrib} RS trans
+ val left_distrib = @{thm left_zadd_zmult_distrib} RS @{thm trans}
val prove_conv = prove_conv_nohyps "int_combine_numerals"
- fun trans_tac _ = ArithData.gen_trans_tac trans
+ fun trans_tac _ = ArithData.gen_trans_tac @{thm trans}
val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac} @ intifys
val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys
@@ -274,14 +274,14 @@
fun mk_coeff(k,t) = if t=one then mk_numeral k
else raise TERM("mk_coeff", [])
fun dest_coeff t = (dest_numeral t, one) (*We ONLY want pure numerals.*)
- val left_distrib = @{thm zmult_assoc} RS sym RS trans
+ val left_distrib = @{thm zmult_assoc} RS @{thm sym} RS @{thm trans}
val prove_conv = prove_conv_nohyps "int_combine_numerals_prod"
- fun trans_tac _ = ArithData.gen_trans_tac trans
+ fun trans_tac _ = ArithData.gen_trans_tac @{thm trans}
val norm_ss1 = ZF_ss addsimps mult_1s @ diff_simps @ zminus_simps
- val norm_ss2 = ZF_ss addsimps [@{thm zmult_zminus_right} RS sym] @
+ val norm_ss2 = ZF_ss addsimps [@{thm zmult_zminus_right} RS @{thm sym}] @
bin_simps @ @{thms zmult_ac} @ tc_rules @ intifys
fun norm_tac ss =
ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1))
--- a/src/ZF/simpdata.ML Sat Feb 27 23:13:01 2010 +0100
+++ b/src/ZF/simpdata.ML Sun Feb 28 22:30:51 2010 +0100
@@ -32,9 +32,9 @@
(*Analyse a rigid formula*)
val ZF_conn_pairs =
[("Ball", [@{thm bspec}]),
- ("All", [spec]),
- ("op -->", [mp]),
- ("op &", [conjunct1,conjunct2])];
+ ("All", [@{thm spec}]),
+ ("op -->", [@{thm mp}]),
+ ("op &", [@{thm conjunct1}, @{thm conjunct2}])];
(*Analyse a:b, where b is rigid*)
val ZF_mem_pairs =