# HG changeset patch # User wenzelm # Date 1267392651 -3600 # Node ID 5c5bb83f2bae8b5ca34b61820f3566aa5283be6e # Parent b48ab741683b129bdf8932147ffce0eb5232e4fb more antiquotations; eliminated legacy ML bindings; diff -r b48ab741683b -r 5c5bb83f2bae src/CCL/CCL.thy --- 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)) *}) diff -r b48ab741683b -r 5c5bb83f2bae src/CCL/Type.thy --- 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 *} diff -r b48ab741683b -r 5c5bb83f2bae src/FOL/IFOL.thy --- 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 diff -r b48ab741683b -r 5c5bb83f2bae src/ZF/Datatype_ZF.thy --- 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); diff -r b48ab741683b -r 5c5bb83f2bae src/ZF/Tools/datatype_package.ML --- 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 [] [] diff -r b48ab741683b -r 5c5bb83f2bae src/ZF/Tools/induct_tacs.ML --- 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 = diff -r b48ab741683b -r 5c5bb83f2bae src/ZF/Tools/inductive_package.ML --- 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 diff -r b48ab741683b -r 5c5bb83f2bae src/ZF/Tools/primrec_package.ML --- 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 diff -r b48ab741683b -r 5c5bb83f2bae src/ZF/Tools/typechk.ML --- 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)))); diff -r b48ab741683b -r 5c5bb83f2bae src/ZF/UNITY/Constrains.thy --- 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)]) diff -r b48ab741683b -r 5c5bb83f2bae src/ZF/UNITY/SubstAx.thy --- 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), diff -r b48ab741683b -r 5c5bb83f2bae src/ZF/arith_data.ML --- 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); diff -r b48ab741683b -r 5c5bb83f2bae src/ZF/int_arith.ML --- 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)) diff -r b48ab741683b -r 5c5bb83f2bae src/ZF/simpdata.ML --- 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 =