--- a/src/CCL/CCL.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/CCL/CCL.thy Mon Sep 06 19:13:10 2010 +0200
@@ -238,9 +238,9 @@
fun mk_thm_str thy a b = "~ " ^ (saturate thy a "a") ^ " = " ^ (saturate thy b "b")
- val lemma = thm "lem";
- val eq_lemma = thm "eq_lemma";
- val distinctness = thm "distinctness";
+ val lemma = @{thm lem};
+ 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, @{thm sym} RS (distinctness RS notE)]
in
--- a/src/CCL/Type.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/CCL/Type.thy Mon Sep 06 19:13:10 2010 +0200
@@ -99,7 +99,7 @@
unfolding simp_type_defs by blast+
ML {*
-bind_thms ("case_rls", XH_to_Es (thms "XHs"));
+bind_thms ("case_rls", XH_to_Es @{thms XHs});
*}
@@ -260,7 +260,7 @@
lemmas iXHs = NatXH ListXH
-ML {* bind_thms ("icase_rls", XH_to_Es (thms "iXHs")) *}
+ML {* bind_thms ("icase_rls", XH_to_Es @{thms iXHs}) *}
subsection {* Type Rules *}
--- a/src/CCL/ex/Stream.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/CCL/ex/Stream.thy Mon Sep 06 19:13:10 2010 +0200
@@ -88,7 +88,7 @@
apply (tactic "EQgen_tac @{context} [] 1")
prefer 2
apply blast
- apply (tactic {* DEPTH_SOLVE (etac (XH_to_E (thm "ListsXH")) 1
+ apply (tactic {* DEPTH_SOLVE (etac (XH_to_E @{thm ListsXH}) 1
THEN EQgen_tac @{context} [] 1) *})
done
@@ -135,7 +135,7 @@
apply (tactic {* eq_coinduct3_tac @{context}
"{p. EX x y. p=<x,y> & (EX n:Nat. x=iter1 (f,f^n`a) & y=map (f) ^n`iter2 (f,a))}" 1*})
apply (fast intro!: napplyBzero [symmetric] napplyBzero [symmetric, THEN arg_cong])
- apply (tactic {* EQgen_tac @{context} [thm "iter1B", thm "iter2Blemma"] 1 *})
+ apply (tactic {* EQgen_tac @{context} [@{thm iter1B}, @{thm iter2Blemma}] 1 *})
apply (subst napply_f, assumption)
apply (rule_tac f1 = f in napplyBsucc [THEN subst])
apply blast
--- a/src/CTT/Arith.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/CTT/Arith.thy Mon Sep 06 19:13:10 2010 +0200
@@ -82,12 +82,12 @@
lemma mult_typing: "[| a:N; b:N |] ==> a #* b : N"
apply (unfold arith_defs)
-apply (tactic {* typechk_tac [thm "add_typing"] *})
+apply (tactic {* typechk_tac [@{thm add_typing}] *})
done
lemma mult_typingL: "[| a=c:N; b=d:N |] ==> a #* b = c #* d : N"
apply (unfold arith_defs)
-apply (tactic {* equal_tac [thm "add_typingL"] *})
+apply (tactic {* equal_tac [@{thm add_typingL}] *})
done
(*computation for mult: 0 and successor cases*)
@@ -159,19 +159,19 @@
structure Arith_simp_data: TSIMP_DATA =
struct
- val refl = thm "refl_elem"
- val sym = thm "sym_elem"
- val trans = thm "trans_elem"
- val refl_red = thm "refl_red"
- val trans_red = thm "trans_red"
- val red_if_equal = thm "red_if_equal"
- val default_rls = thms "arithC_rls" @ thms "comp_rls"
- val routine_tac = routine_tac (thms "arith_typing_rls" @ thms "routine_rls")
+ val refl = @{thm refl_elem}
+ val sym = @{thm sym_elem}
+ val trans = @{thm trans_elem}
+ val refl_red = @{thm refl_red}
+ val trans_red = @{thm trans_red}
+ val red_if_equal = @{thm red_if_equal}
+ val default_rls = @{thms arithC_rls} @ @{thms comp_rls}
+ val routine_tac = routine_tac (@{thms arith_typing_rls} @ @{thms routine_rls})
end
structure Arith_simp = TSimpFun (Arith_simp_data)
-local val congr_rls = thms "congr_rls" in
+local val congr_rls = @{thms congr_rls} in
fun arith_rew_tac prems = make_rew_tac
(Arith_simp.norm_tac(congr_rls, prems))
@@ -271,7 +271,7 @@
(*Solves first 0 goal, simplifies others. Two sugbgoals remain.
Both follow by rewriting, (2) using quantified induction hyp*)
apply (tactic "intr_tac []") (*strips remaining PRODs*)
-apply (tactic {* hyp_arith_rew_tac [thm "add_0_right"] *})
+apply (tactic {* hyp_arith_rew_tac [@{thm add_0_right}] *})
apply assumption
done
@@ -303,7 +303,7 @@
lemma absdiff_self_eq_0: "a:N ==> a |-| a = 0 : N"
apply (unfold absdiff_def)
-apply (tactic {* arith_rew_tac [thm "diff_self_eq_0"] *})
+apply (tactic {* arith_rew_tac [@{thm diff_self_eq_0}] *})
done
lemma absdiffC0: "a:N ==> 0 |-| a = a : N"
@@ -321,7 +321,7 @@
lemma absdiff_commute: "[| a:N; b:N |] ==> a |-| b = b |-| a : N"
apply (unfold absdiff_def)
apply (rule add_commute)
-apply (tactic {* typechk_tac [thm "diff_typing"] *})
+apply (tactic {* typechk_tac [@{thm diff_typing}] *})
done
(*If a+b=0 then a=0. Surprisingly tedious*)
@@ -332,7 +332,7 @@
apply (tactic "intr_tac []") (*strips remaining PRODs*)
apply (rule_tac [2] zero_ne_succ [THEN FE])
apply (erule_tac [3] EqE [THEN sym_elem])
-apply (tactic {* typechk_tac [thm "add_typing"] *})
+apply (tactic {* typechk_tac [@{thm add_typing}] *})
done
(*Version of above with the premise a+b=0.
@@ -354,7 +354,7 @@
apply (rule_tac [2] add_eq0)
apply (rule add_eq0)
apply (rule_tac [6] add_commute [THEN trans_elem])
-apply (tactic {* typechk_tac [thm "diff_typing"] *})
+apply (tactic {* typechk_tac [@{thm diff_typing}] *})
done
(*if a |-| b = 0 then a = b
@@ -366,7 +366,7 @@
apply (tactic eqintr_tac)
apply (rule add_diff_inverse [THEN sym_elem, THEN trans_elem])
apply (rule_tac [3] EqE, tactic "assume_tac 3")
-apply (tactic {* hyp_arith_rew_tac [thm "add_0_right"] *})
+apply (tactic {* hyp_arith_rew_tac [@{thm add_0_right}] *})
done
@@ -376,12 +376,12 @@
lemma mod_typing: "[| a:N; b:N |] ==> a mod b : N"
apply (unfold mod_def)
-apply (tactic {* typechk_tac [thm "absdiff_typing"] *})
+apply (tactic {* typechk_tac [@{thm absdiff_typing}] *})
done
lemma mod_typingL: "[| a=c:N; b=d:N |] ==> a mod b = c mod d : N"
apply (unfold mod_def)
-apply (tactic {* equal_tac [thm "absdiff_typingL"] *})
+apply (tactic {* equal_tac [@{thm absdiff_typingL}] *})
done
@@ -389,13 +389,13 @@
lemma modC0: "b:N ==> 0 mod b = 0 : N"
apply (unfold mod_def)
-apply (tactic {* rew_tac [thm "absdiff_typing"] *})
+apply (tactic {* rew_tac [@{thm absdiff_typing}] *})
done
lemma modC_succ:
"[| a:N; b:N |] ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y. succ(a mod b)) : N"
apply (unfold mod_def)
-apply (tactic {* rew_tac [thm "absdiff_typing"] *})
+apply (tactic {* rew_tac [@{thm absdiff_typing}] *})
done
@@ -403,12 +403,12 @@
lemma div_typing: "[| a:N; b:N |] ==> a div b : N"
apply (unfold div_def)
-apply (tactic {* typechk_tac [thm "absdiff_typing", thm "mod_typing"] *})
+apply (tactic {* typechk_tac [@{thm absdiff_typing}, @{thm mod_typing}] *})
done
lemma div_typingL: "[| a=c:N; b=d:N |] ==> a div b = c div d : N"
apply (unfold div_def)
-apply (tactic {* equal_tac [thm "absdiff_typingL", thm "mod_typingL"] *})
+apply (tactic {* equal_tac [@{thm absdiff_typingL}, @{thm mod_typingL}] *})
done
lemmas div_typing_rls = mod_typing div_typing absdiff_typing
@@ -418,14 +418,14 @@
lemma divC0: "b:N ==> 0 div b = 0 : N"
apply (unfold div_def)
-apply (tactic {* rew_tac [thm "mod_typing", thm "absdiff_typing"] *})
+apply (tactic {* rew_tac [@{thm mod_typing}, @{thm absdiff_typing}] *})
done
lemma divC_succ:
"[| a:N; b:N |] ==> succ(a) div b =
rec(succ(a) mod b, succ(a div b), %x y. a div b) : N"
apply (unfold div_def)
-apply (tactic {* rew_tac [thm "mod_typing"] *})
+apply (tactic {* rew_tac [@{thm mod_typing}] *})
done
@@ -433,9 +433,9 @@
lemma divC_succ2: "[| a:N; b:N |] ==>
succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), %x y. a div b) : N"
apply (rule divC_succ [THEN trans_elem])
-apply (tactic {* rew_tac (thms "div_typing_rls" @ [thm "modC_succ"]) *})
+apply (tactic {* rew_tac (@{thms div_typing_rls} @ [@{thm modC_succ}]) *})
apply (tactic {* NE_tac @{context} "succ (a mod b) |-|b" 1 *})
-apply (tactic {* rew_tac [thm "mod_typing", thm "div_typing", thm "absdiff_typing"] *})
+apply (tactic {* rew_tac [@{thm mod_typing}, @{thm div_typing}, @{thm absdiff_typing}] *})
done
(*for case analysis on whether a number is 0 or a successor*)
@@ -451,19 +451,19 @@
(*Main Result. Holds when b is 0 since a mod 0 = a and a div 0 = 0 *)
lemma mod_div_equality: "[| a:N; b:N |] ==> a mod b #+ (a div b) #* b = a : N"
apply (tactic {* NE_tac @{context} "a" 1 *})
-apply (tactic {* arith_rew_tac (thms "div_typing_rls" @
- [thm "modC0", thm "modC_succ", thm "divC0", thm "divC_succ2"]) *})
+apply (tactic {* arith_rew_tac (@{thms div_typing_rls} @
+ [@{thm modC0}, @{thm modC_succ}, @{thm divC0}, @{thm divC_succ2}]) *})
apply (rule EqE)
(*case analysis on succ(u mod b)|-|b *)
apply (rule_tac a1 = "succ (u mod b) |-| b" in iszero_decidable [THEN PlusE])
apply (erule_tac [3] SumE)
-apply (tactic {* hyp_arith_rew_tac (thms "div_typing_rls" @
- [thm "modC0", thm "modC_succ", thm "divC0", thm "divC_succ2"]) *})
+apply (tactic {* hyp_arith_rew_tac (@{thms div_typing_rls} @
+ [@{thm modC0}, @{thm modC_succ}, @{thm divC0}, @{thm divC_succ2}]) *})
(*Replace one occurence of b by succ(u mod b). Clumsy!*)
apply (rule add_typingL [THEN trans_elem])
apply (erule EqE [THEN absdiff_eq0, THEN sym_elem])
apply (rule_tac [3] refl_elem)
-apply (tactic {* hyp_arith_rew_tac (thms "div_typing_rls") *})
+apply (tactic {* hyp_arith_rew_tac @{thms div_typing_rls} *})
done
end
--- a/src/CTT/ex/Elimination.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/CTT/ex/Elimination.thy Mon Sep 06 19:13:10 2010 +0200
@@ -53,7 +53,7 @@
and "!!x. x:A ==> B(x) type"
and "!!x. x:A ==> C(x) type"
shows "?a : (SUM x:A. B(x) + C(x)) --> (SUM x:A. B(x)) + (SUM x:A. C(x))"
-apply (tactic {* pc_tac (thms "prems") 1 *})
+apply (tactic {* pc_tac @{thms assms} 1 *})
done
text "Construction of the currying functional"
@@ -68,7 +68,7 @@
and "!!z. z: (SUM x:A. B(x)) ==> C(z) type"
shows "?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)).
(PROD x:A . PROD y:B(x) . C(<x,y>))"
-apply (tactic {* pc_tac (thms "prems") 1 *})
+apply (tactic {* pc_tac @{thms assms} 1 *})
done
text "Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)"
@@ -83,7 +83,7 @@
and "!!z. z: (SUM x:A . B(x)) ==> C(z) type"
shows "?a : (PROD x:A . PROD y:B(x) . C(<x,y>))
--> (PROD z : (SUM x:A . B(x)) . C(z))"
-apply (tactic {* pc_tac (thms "prems") 1 *})
+apply (tactic {* pc_tac @{thms assms} 1 *})
done
text "Function application"
@@ -99,7 +99,7 @@
shows
"?a : (SUM y:B . PROD x:A . C(x,y))
--> (PROD x:A . SUM y:B . C(x,y))"
-apply (tactic {* pc_tac (thms "prems") 1 *})
+apply (tactic {* pc_tac @{thms assms} 1 *})
done
text "Martin-Lof (1984) pages 36-7: the combinator S"
@@ -109,7 +109,7 @@
and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type"
shows "?a : (PROD x:A. PROD y:B(x). C(x,y))
--> (PROD f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
-apply (tactic {* pc_tac (thms "prems") 1 *})
+apply (tactic {* pc_tac @{thms assms} 1 *})
done
text "Martin-Lof (1984) page 58: the axiom of disjunction elimination"
@@ -119,7 +119,7 @@
and "!!z. z: A+B ==> C(z) type"
shows "?a : (PROD x:A. C(inl(x))) --> (PROD y:B. C(inr(y)))
--> (PROD z: A+B. C(z))"
-apply (tactic {* pc_tac (thms "prems") 1 *})
+apply (tactic {* pc_tac @{thms assms} 1 *})
done
(*towards AXIOM OF CHOICE*)
@@ -137,7 +137,7 @@
and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type"
shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).
(SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
-apply (tactic {* intr_tac (thms "prems") *})
+apply (tactic {* intr_tac @{thms assms} *})
apply (tactic "add_mp_tac 2")
apply (tactic "add_mp_tac 1")
apply (erule SumE_fst)
@@ -145,7 +145,7 @@
apply (rule subst_eqtyparg)
apply (rule comp_rls)
apply (rule_tac [4] SumE_snd)
-apply (tactic {* typechk_tac (thm "SumE_fst" :: thms "prems") *})
+apply (tactic {* typechk_tac (@{thm SumE_fst} :: @{thms prems}) *})
done
text "Axiom of choice. Proof without fst, snd. Harder still!"
@@ -155,7 +155,7 @@
and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type"
shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).
(SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
-apply (tactic {* intr_tac (thms "prems") *})
+apply (tactic {* intr_tac @{thms assms} *})
(*Must not use add_mp_tac as subst_prodE hides the construction.*)
apply (rule ProdE [THEN SumE], assumption)
apply (tactic "TRYALL assume_tac")
@@ -163,11 +163,11 @@
apply (rule subst_eqtyparg)
apply (rule comp_rls)
apply (erule_tac [4] ProdE [THEN SumE])
-apply (tactic {* typechk_tac (thms "prems") *})
+apply (tactic {* typechk_tac @{thms assms} *})
apply (rule replace_type)
apply (rule subst_eqtyparg)
apply (rule comp_rls)
-apply (tactic {* typechk_tac (thms "prems") *})
+apply (tactic {* typechk_tac @{thms assms} *})
apply assumption
done
@@ -183,11 +183,11 @@
apply (tactic {* biresolve_tac safe_brls 2 *})
(*Now must convert assumption C(z) into antecedent C(<kd,ke>) *)
apply (rule_tac [2] a = "y" in ProdE)
-apply (tactic {* typechk_tac (thms "prems") *})
+apply (tactic {* typechk_tac @{thms assms} *})
apply (rule SumE, assumption)
apply (tactic "intr_tac []")
apply (tactic "TRYALL assume_tac")
-apply (tactic {* typechk_tac (thms "prems") *})
+apply (tactic {* typechk_tac @{thms assms} *})
done
end
--- a/src/CTT/ex/Typechecking.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/CTT/ex/Typechecking.thy Mon Sep 06 19:13:10 2010 +0200
@@ -66,7 +66,7 @@
(*Proofs involving arbitrary types.
For concreteness, every type variable left over is forced to be N*)
-ML {* val N_tac = TRYALL (rtac (thm "NF")) *}
+ML {* val N_tac = TRYALL (rtac @{thm NF}) *}
schematic_lemma "lam w. <w,w> : ?A"
apply (tactic "typechk_tac []")
--- a/src/CTT/rew.ML Mon Sep 06 19:11:01 2010 +0200
+++ b/src/CTT/rew.ML Mon Sep 06 19:13:10 2010 +0200
@@ -8,7 +8,7 @@
(*Make list of ProdE RS ProdE ... RS ProdE RS EqE
for using assumptions as rewrite rules*)
fun peEs 0 = []
- | peEs n = thm "EqE" :: map (curry (op RS) (thm "ProdE")) (peEs (n-1));
+ | peEs n = @{thm EqE} :: map (curry (op RS) @{thm ProdE}) (peEs (n-1));
(*Tactic used for proving conditions for the cond_rls*)
val prove_cond_tac = eresolve_tac (peEs 5);
@@ -16,19 +16,19 @@
structure TSimp_data: TSIMP_DATA =
struct
- val refl = thm "refl_elem"
- val sym = thm "sym_elem"
- val trans = thm "trans_elem"
- val refl_red = thm "refl_red"
- val trans_red = thm "trans_red"
- val red_if_equal = thm "red_if_equal"
- val default_rls = thms "comp_rls"
- val routine_tac = routine_tac (thms "routine_rls")
+ val refl = @{thm refl_elem}
+ val sym = @{thm sym_elem}
+ val trans = @{thm trans_elem}
+ val refl_red = @{thm refl_red}
+ val trans_red = @{thm trans_red}
+ val red_if_equal = @{thm red_if_equal}
+ val default_rls = @{thms comp_rls}
+ val routine_tac = routine_tac (@{thms routine_rls})
end;
structure TSimp = TSimpFun (TSimp_data);
-val standard_congr_rls = thms "intrL2_rls" @ thms "elimL_rls";
+val standard_congr_rls = @{thms intrL2_rls} @ @{thms elimL_rls};
(*Make a rewriting tactic from a normalization tactic*)
fun make_rew_tac ntac =
--- a/src/FOL/IFOL.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/FOL/IFOL.thy Mon Sep 06 19:13:10 2010 +0200
@@ -340,7 +340,7 @@
shows "(P&Q) <-> (P'&Q')"
apply (insert assms)
apply (assumption | rule iffI conjI | erule iffE conjE mp |
- tactic {* iff_tac (thms "assms") 1 *})+
+ tactic {* iff_tac @{thms assms} 1 *})+
done
(*Reversed congruence rule! Used in ZF/Order*)
@@ -350,7 +350,7 @@
shows "(Q&P) <-> (Q'&P')"
apply (insert assms)
apply (assumption | rule iffI conjI | erule iffE conjE mp |
- tactic {* iff_tac (thms "assms") 1 *})+
+ tactic {* iff_tac @{thms assms} 1 *})+
done
lemma disj_cong:
@@ -366,7 +366,7 @@
shows "(P-->Q) <-> (P'-->Q')"
apply (insert assms)
apply (assumption | rule iffI impI | erule iffE | erule (1) notE impE |
- tactic {* iff_tac (thms "assms") 1 *})+
+ tactic {* iff_tac @{thms assms} 1 *})+
done
lemma iff_cong: "[| P <-> P'; Q <-> Q' |] ==> (P<->Q) <-> (P'<->Q')"
@@ -381,21 +381,21 @@
assumes "!!x. P(x) <-> Q(x)"
shows "(ALL x. P(x)) <-> (ALL x. Q(x))"
apply (assumption | rule iffI allI | erule (1) notE impE | erule allE |
- tactic {* iff_tac (thms "assms") 1 *})+
+ tactic {* iff_tac @{thms assms} 1 *})+
done
lemma ex_cong:
assumes "!!x. P(x) <-> Q(x)"
shows "(EX x. P(x)) <-> (EX x. Q(x))"
apply (erule exE | assumption | rule iffI exI | erule (1) notE impE |
- tactic {* iff_tac (thms "assms") 1 *})+
+ tactic {* iff_tac @{thms assms} 1 *})+
done
lemma ex1_cong:
assumes "!!x. P(x) <-> Q(x)"
shows "(EX! x. P(x)) <-> (EX! x. Q(x))"
apply (erule ex1E spec [THEN mp] | assumption | rule iffI ex1I | erule (1) notE impE |
- tactic {* iff_tac (thms "assms") 1 *})+
+ tactic {* iff_tac @{thms assms} 1 *})+
done
(*** Equality rules ***)
--- a/src/FOL/hypsubstdata.ML Mon Sep 06 19:11:01 2010 +0200
+++ b/src/FOL/hypsubstdata.ML Mon Sep 06 19:13:10 2010 +0200
@@ -6,13 +6,13 @@
val dest_eq = FOLogic.dest_eq
val dest_Trueprop = FOLogic.dest_Trueprop
val dest_imp = FOLogic.dest_imp
- val eq_reflection = thm "eq_reflection"
- val rev_eq_reflection = thm "meta_eq_to_obj_eq"
- val imp_intr = thm "impI"
- val rev_mp = thm "rev_mp"
- val subst = thm "subst"
- val sym = thm "sym"
- val thin_refl = thm "thin_refl"
+ val eq_reflection = @{thm eq_reflection}
+ val rev_eq_reflection = @{thm meta_eq_to_obj_eq}
+ val imp_intr = @{thm impI}
+ val rev_mp = @{thm rev_mp}
+ val subst = @{thm subst}
+ val sym = @{thm sym}
+ val thin_refl = @{thm thin_refl}
val prop_subst = @{lemma "PROP P(t) ==> PROP prop (x = t ==> PROP P(x))"
by (unfold prop_def) (drule eq_reflection, unfold)}
end;
--- a/src/HOL/Algebra/abstract/Ring2.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/Algebra/abstract/Ring2.thy Mon Sep 06 19:13:10 2010 +0200
@@ -211,11 +211,11 @@
fun termless_ring (a, b) = (Term_Ord.term_lpo ring_ord (a, b) = LESS);
val ring_ss = HOL_basic_ss settermless termless_ring addsimps
- [thm "a_assoc", thm "l_zero", thm "l_neg", thm "a_comm", thm "m_assoc",
- thm "l_one", thm "l_distr", thm "m_comm", thm "minus_def",
- thm "r_zero", thm "r_neg", thm "r_neg2", thm "r_neg1", thm "minus_add",
- thm "minus_minus", thm "minus0", thm "a_lcomm", thm "m_lcomm", (*thm "r_one",*)
- thm "r_distr", thm "l_null", thm "r_null", thm "l_minus", thm "r_minus"];
+ [@{thm a_assoc}, @{thm l_zero}, @{thm l_neg}, @{thm a_comm}, @{thm m_assoc},
+ @{thm l_one}, @{thm l_distr}, @{thm m_comm}, @{thm minus_def},
+ @{thm r_zero}, @{thm r_neg}, @{thm r_neg2}, @{thm r_neg1}, @{thm minus_add},
+ @{thm minus_minus}, @{thm minus0}, @{thm a_lcomm}, @{thm m_lcomm}, (*@{thm r_one},*)
+ @{thm r_distr}, @{thm l_null}, @{thm r_null}, @{thm l_minus}, @{thm r_minus}];
*} (* Note: r_one is not necessary in ring_ss *)
method_setup ring =
--- a/src/HOL/Algebra/poly/LongDiv.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/Algebra/poly/LongDiv.thy Mon Sep 06 19:13:10 2010 +0200
@@ -133,8 +133,8 @@
apply (tactic {* simp_tac (@{simpset} addsimps [@{thm l_distr}, @{thm a_assoc}]
delsimprocs [ring_simproc]) 1 *})
apply (tactic {* asm_simp_tac (@{simpset} delsimprocs [ring_simproc]) 1 *})
- apply (tactic {* simp_tac (@{simpset} addsimps [thm "minus_def", thm "smult_r_distr",
- thm "smult_r_minus", thm "monom_mult_smult", thm "smult_assoc2"]
+ apply (tactic {* simp_tac (@{simpset} addsimps [@{thm minus_def}, @{thm smult_r_distr},
+ @{thm smult_r_minus}, @{thm monom_mult_smult}, @{thm smult_assoc2}]
delsimprocs [ring_simproc]) 1 *})
apply (simp add: smult_assoc1 [symmetric])
done
@@ -169,7 +169,7 @@
apply (rule conjI)
apply (drule sym)
apply (tactic {* asm_simp_tac
- (@{simpset} addsimps [thm "smult_r_distr" RS sym, thm "smult_assoc2"]
+ (@{simpset} addsimps [@{thm smult_r_distr} RS sym, @{thm smult_assoc2}]
delsimprocs [ring_simproc]) 1 *})
apply (simp (no_asm_simp) add: l_inverse_ring unit_power smult_assoc1 [symmetric])
(* degree property *)
@@ -216,21 +216,21 @@
apply (erule disjE)
(* r2 = 0 *)
apply (tactic {* asm_full_simp_tac (@{simpset}
- addsimps [thm "integral_iff", thm "minus_def", thm "l_zero", thm "uminus_zero"]
+ addsimps [@{thm integral_iff}, @{thm minus_def}, @{thm l_zero}, @{thm uminus_zero}]
delsimprocs [ring_simproc]) 1 *})
(* r2 ~= 0 *)
apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong)
apply (tactic {* asm_full_simp_tac (@{simpset} addsimps
- [thm "minus_def", thm "l_zero", thm "uminus_zero"] delsimprocs [ring_simproc]) 1 *})
+ [@{thm minus_def}, @{thm l_zero}, @{thm uminus_zero}] delsimprocs [ring_simproc]) 1 *})
(* r1 ~=0 *)
apply (erule disjE)
(* r2 = 0 *)
apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong)
apply (tactic {* asm_full_simp_tac (@{simpset} addsimps
- [thm "minus_def", thm "l_zero", thm "uminus_zero"] delsimprocs [ring_simproc]) 1 *})
+ [@{thm minus_def}, @{thm l_zero}, @{thm uminus_zero}] delsimprocs [ring_simproc]) 1 *})
(* r2 ~= 0 *)
apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong)
- apply (tactic {* asm_full_simp_tac (@{simpset} addsimps [thm "minus_def"]
+ apply (tactic {* asm_full_simp_tac (@{simpset} addsimps [@{thm minus_def}]
delsimprocs [ring_simproc]) 1 *})
apply (drule order_eq_refl [THEN add_leD2])
apply (drule leD)
--- a/src/HOL/Bali/AxCompl.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/Bali/AxCompl.thy Mon Sep 06 19:13:10 2010 +0200
@@ -1392,7 +1392,7 @@
apply -
apply (induct_tac "n")
apply (tactic "ALLGOALS (clarsimp_tac @{clasimpset})")
-apply (tactic {* dtac (Thm.permute_prems 0 1 (thm "card_seteq")) 1 *})
+apply (tactic {* dtac (Thm.permute_prems 0 1 @{thm card_seteq}) 1 *})
apply simp
apply (erule finite_imageI)
apply (simp add: MGF_asm ax_derivs_asm)
--- a/src/HOL/Bali/AxSem.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/Bali/AxSem.thy Mon Sep 06 19:13:10 2010 +0200
@@ -671,7 +671,7 @@
(* 37 subgoals *)
prefer 18 (* Methd *)
apply (rule ax_derivs.Methd, drule spec, erule mp, fast)
-apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros"))) *})
+apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) @{thms ax_derivs.intros})) *})
apply auto
done
@@ -691,8 +691,8 @@
apply (erule ax_derivs.induct)
(*42 subgoals*)
apply (tactic "ALLGOALS strip_tac")
-apply (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac (thm "subset_singletonD"),
- etac disjE, fast_tac (@{claset} addSIs [thm "ax_derivs.empty"])]))*})
+apply (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac @{thm subset_singletonD},
+ etac disjE, fast_tac (@{claset} addSIs @{thms ax_derivs.empty})]))*})
apply (tactic "TRYALL hyp_subst_tac")
apply (simp, rule ax_derivs.empty)
apply (drule subset_insertD)
@@ -702,7 +702,7 @@
apply (fast intro: ax_derivs.weaken)
apply (rule ax_derivs.conseq, clarify, tactic "smp_tac 3 1", blast(* unused *))
(*37 subgoals*)
-apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros"))
+apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) @{thms ax_derivs.intros})
THEN_ALL_NEW fast_tac @{claset}) *})
(*1 subgoal*)
apply (clarsimp simp add: subset_mtriples_iff)
--- a/src/HOL/Bali/Eval.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/Bali/Eval.thy Mon Sep 06 19:13:10 2010 +0200
@@ -1168,7 +1168,7 @@
"G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w, s') \<Longrightarrow> (\<forall>w' s''. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w', s'') \<longrightarrow> w' = w \<and> s'' = s')"
apply (erule eval_induct)
apply (tactic {* ALLGOALS (EVERY'
- [strip_tac, rotate_tac ~1, eresolve_tac (thms "eval_elim_cases")]) *})
+ [strip_tac, rotate_tac ~1, eresolve_tac @{thms eval_elim_cases}]) *})
(* 31 subgoals *)
prefer 28 (* Try *)
apply (simp (no_asm_use) only: split add: split_if_asm)
--- a/src/HOL/Bali/Evaln.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/Bali/Evaln.thy Mon Sep 06 19:13:10 2010 +0200
@@ -449,9 +449,9 @@
lemma evaln_nonstrict [rule_format (no_asm), elim]:
"G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w, s') \<Longrightarrow> \<forall>m. n\<le>m \<longrightarrow> G\<turnstile>s \<midarrow>t\<succ>\<midarrow>m\<rightarrow> (w, s')"
apply (erule evaln.induct)
-apply (tactic {* ALLGOALS (EVERY'[strip_tac, TRY o etac (thm "Suc_le_D_lemma"),
+apply (tactic {* ALLGOALS (EVERY'[strip_tac, TRY o etac @{thm Suc_le_D_lemma},
REPEAT o smp_tac 1,
- resolve_tac (thms "evaln.intros") THEN_ALL_NEW TRY o atac]) *})
+ resolve_tac @{thms evaln.intros} THEN_ALL_NEW TRY o atac]) *})
(* 3 subgoals *)
apply (auto split del: split_if)
done
--- a/src/HOL/Decision_Procs/mir_tac.ML Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML Mon Sep 06 19:13:10 2010 +0200
@@ -16,18 +16,18 @@
fun trace_msg s = if !trace then tracing s else ();
val mir_ss =
-let val ths = map thm ["real_of_int_inject", "real_of_int_less_iff", "real_of_int_le_iff"]
+let val ths = [@{thm "real_of_int_inject"}, @{thm "real_of_int_less_iff"}, @{thm "real_of_int_le_iff"}]
in @{simpset} delsimps ths addsimps (map (fn th => th RS sym) ths)
end;
val nT = HOLogic.natT;
- val nat_arith = map thm ["add_nat_number_of", "diff_nat_number_of",
- "mult_nat_number_of", "eq_nat_number_of", "less_nat_number_of"];
+ val nat_arith = [@{thm "add_nat_number_of"}, @{thm "diff_nat_number_of"},
+ @{thm "mult_nat_number_of"}, @{thm "eq_nat_number_of"}, @{thm "less_nat_number_of"}];
- val comp_arith = (map thm ["Let_def", "if_False", "if_True", "add_0",
- "add_Suc", "add_number_of_left", "mult_number_of_left",
- "Suc_eq_plus1"])@
- (map (fn s => thm s RS sym) ["numeral_1_eq_1", "numeral_0_eq_0"])
+ val comp_arith = [@{thm "Let_def"}, @{thm "if_False"}, @{thm "if_True"}, @{thm "add_0"},
+ @{thm "add_Suc"}, @{thm "add_number_of_left"}, @{thm "mult_number_of_left"},
+ @{thm "Suc_eq_plus1"}] @
+ (map (fn th => th RS sym) [@{thm "numeral_1_eq_1"}, @{thm "numeral_0_eq_0"}])
@ @{thms arith_simps} @ nat_arith @ @{thms rel_simps}
val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
@{thm "real_of_nat_number_of"},
--- a/src/HOL/HOL.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/HOL.thy Mon Sep 06 19:13:10 2010 +0200
@@ -2089,47 +2089,47 @@
fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
end;
-val all_conj_distrib = thm "all_conj_distrib";
-val all_simps = thms "all_simps";
-val atomize_not = thm "atomize_not";
-val case_split = thm "case_split";
-val cases_simp = thm "cases_simp";
-val choice_eq = thm "choice_eq"
-val cong = thm "cong"
-val conj_comms = thms "conj_comms";
-val conj_cong = thm "conj_cong";
-val de_Morgan_conj = thm "de_Morgan_conj";
-val de_Morgan_disj = thm "de_Morgan_disj";
-val disj_assoc = thm "disj_assoc";
-val disj_comms = thms "disj_comms";
-val disj_cong = thm "disj_cong";
-val eq_ac = thms "eq_ac";
-val eq_cong2 = thm "eq_cong2"
-val Eq_FalseI = thm "Eq_FalseI";
-val Eq_TrueI = thm "Eq_TrueI";
-val Ex1_def = thm "Ex1_def"
-val ex_disj_distrib = thm "ex_disj_distrib";
-val ex_simps = thms "ex_simps";
-val if_cancel = thm "if_cancel";
-val if_eq_cancel = thm "if_eq_cancel";
-val if_False = thm "if_False";
-val iff_conv_conj_imp = thm "iff_conv_conj_imp";
-val iff = thm "iff"
-val if_splits = thms "if_splits";
-val if_True = thm "if_True";
-val if_weak_cong = thm "if_weak_cong"
-val imp_all = thm "imp_all";
-val imp_cong = thm "imp_cong";
-val imp_conjL = thm "imp_conjL";
-val imp_conjR = thm "imp_conjR";
-val imp_conv_disj = thm "imp_conv_disj";
-val simp_implies_def = thm "simp_implies_def";
-val simp_thms = thms "simp_thms";
-val split_if = thm "split_if";
-val the1_equality = thm "the1_equality"
-val theI = thm "theI"
-val theI' = thm "theI'"
-val True_implies_equals = thm "True_implies_equals";
+val all_conj_distrib = @{thm all_conj_distrib};
+val all_simps = @{thms all_simps};
+val atomize_not = @{thm atomize_not};
+val case_split = @{thm case_split};
+val cases_simp = @{thm cases_simp};
+val choice_eq = @{thm choice_eq};
+val cong = @{thm cong};
+val conj_comms = @{thms conj_comms};
+val conj_cong = @{thm conj_cong};
+val de_Morgan_conj = @{thm de_Morgan_conj};
+val de_Morgan_disj = @{thm de_Morgan_disj};
+val disj_assoc = @{thm disj_assoc};
+val disj_comms = @{thms disj_comms};
+val disj_cong = @{thm disj_cong};
+val eq_ac = @{thms eq_ac};
+val eq_cong2 = @{thm eq_cong2}
+val Eq_FalseI = @{thm Eq_FalseI};
+val Eq_TrueI = @{thm Eq_TrueI};
+val Ex1_def = @{thm Ex1_def};
+val ex_disj_distrib = @{thm ex_disj_distrib};
+val ex_simps = @{thms ex_simps};
+val if_cancel = @{thm if_cancel};
+val if_eq_cancel = @{thm if_eq_cancel};
+val if_False = @{thm if_False};
+val iff_conv_conj_imp = @{thm iff_conv_conj_imp};
+val iff = @{thm iff};
+val if_splits = @{thms if_splits};
+val if_True = @{thm if_True};
+val if_weak_cong = @{thm if_weak_cong};
+val imp_all = @{thm imp_all};
+val imp_cong = @{thm imp_cong};
+val imp_conjL = @{thm imp_conjL};
+val imp_conjR = @{thm imp_conjR};
+val imp_conv_disj = @{thm imp_conv_disj};
+val simp_implies_def = @{thm simp_implies_def};
+val simp_thms = @{thms simp_thms};
+val split_if = @{thm split_if};
+val the1_equality = @{thm the1_equality};
+val theI = @{thm theI};
+val theI' = @{thm theI'};
+val True_implies_equals = @{thm True_implies_equals};
val nnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps simp_thms @ @{thms "nnf_simps"})
*}
--- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Mon Sep 06 19:13:10 2010 +0200
@@ -1199,15 +1199,15 @@
apply(case_tac [!] "M x!(T (Muts x ! j))=Black")
apply(simp_all add:Graph10)
--{* 47 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *})
+apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans}, etac @{thm Graph11},force_tac @{clasimpset}]) *})
--{* 41 subgoals left *}
apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac @{thm le_trans}, force_tac (@{claset},@{simpset} addsimps [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}])]) *})
--{* 35 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "psubset_subset_trans"),rtac (thm "Graph9"),force_tac @{clasimpset}]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{clasimpset}]) *})
--{* 31 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{clasimpset}]) *})
--{* 29 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *})
+apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans},etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{clasimpset}]) *})
--{* 25 subgoals left *}
apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac @{thm le_trans}, force_tac (@{claset},@{simpset} addsimps [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}])]) *})
--{* 10 subgoals left *}
--- a/src/HOL/Hoare_Parallel/OG_Tactics.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Tactics.thy Mon Sep 06 19:13:10 2010 +0200
@@ -273,11 +273,11 @@
lemmas ParallelConseq_list = INTER_def Collect_conj_eq length_map length_upt length_append list_length
ML {*
-val before_interfree_simp_tac = (simp_tac (HOL_basic_ss addsimps [thm "com.simps", thm "post.simps"]))
+val before_interfree_simp_tac = simp_tac (HOL_basic_ss addsimps [@{thm com.simps}, @{thm post.simps}])
-val interfree_simp_tac = (asm_simp_tac (HOL_ss addsimps [@{thm split}, thm "ball_Un", thm "ball_empty"]@(thms "my_simp_list")))
+val interfree_simp_tac = asm_simp_tac (HOL_ss addsimps [@{thm split}, @{thm ball_Un}, @{thm ball_empty}] @ @{thms my_simp_list})
-val ParallelConseq = (simp_tac (HOL_basic_ss addsimps (thms "ParallelConseq_list")@(thms "my_simp_list")))
+val ParallelConseq = simp_tac (HOL_basic_ss addsimps @{thms ParallelConseq_list} @ @{thms my_simp_list})
*}
text {* The following tactic applies @{text tac} to each conjunct in a
--- a/src/HOL/IMPP/Hoare.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/IMPP/Hoare.thy Mon Sep 06 19:13:10 2010 +0200
@@ -218,7 +218,7 @@
apply (rule hoare_derivs.conseq, intro strip, tactic "smp_tac 2 1", clarify, tactic "smp_tac 1 1",rule exI, rule exI, erule (1) conjI)
prefer 7
apply (rule_tac hoare_derivs.Body, drule_tac spec, erule_tac mp, fast)
-apply (tactic {* ALLGOALS (resolve_tac ((funpow 5 tl) (thms "hoare_derivs.intros")) THEN_ALL_NEW (fast_tac @{claset})) *})
+apply (tactic {* ALLGOALS (resolve_tac ((funpow 5 tl) @{thms hoare_derivs.intros}) THEN_ALL_NEW (fast_tac @{claset})) *})
done
lemma weak_Body: "G|-{P}. the (body pn) .{Q} ==> G|-{P}. BODY pn .{Q}"
@@ -278,7 +278,7 @@
lemma hoare_sound: "G||-ts ==> G||=ts"
apply (erule hoare_derivs.induct)
-apply (tactic {* TRYALL (eresolve_tac [thm "Loop_sound_lemma", thm "Body_sound_lemma"] THEN_ALL_NEW atac) *})
+apply (tactic {* TRYALL (eresolve_tac [@{thm Loop_sound_lemma}, @{thm Body_sound_lemma}] THEN_ALL_NEW atac) *})
apply (unfold hoare_valids_def)
apply blast
apply blast
@@ -349,7 +349,7 @@
rule_tac [3] P1 = "%Z' s. s= (Z[Loc loc::=fun Z])" in hoare_derivs.Local [THEN conseq1],
erule_tac [3] conseq12)
apply (erule_tac [5] hoare_derivs.Comp, erule_tac [5] conseq12)
-apply (tactic {* (rtac (thm "hoare_derivs.If") THEN_ALL_NEW etac (thm "conseq12")) 6 *})
+apply (tactic {* (rtac @{thm hoare_derivs.If} THEN_ALL_NEW etac @{thm conseq12}) 6 *})
apply (rule_tac [8] hoare_derivs.Loop [THEN conseq2], erule_tac [8] conseq12)
apply auto
done
--- a/src/HOL/IMPP/Natural.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/IMPP/Natural.thy Mon Sep 06 19:13:10 2010 +0200
@@ -114,7 +114,7 @@
lemma evaln_evalc: "<c,s> -n-> t ==> <c,s> -c-> t"
apply (erule evaln.induct)
-apply (tactic {* ALLGOALS (resolve_tac (thms "evalc.intros") THEN_ALL_NEW atac) *})
+apply (tactic {* ALLGOALS (resolve_tac @{thms evalc.intros} THEN_ALL_NEW atac) *})
done
lemma Suc_le_D_lemma: "[| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'"
@@ -124,8 +124,8 @@
lemma evaln_nonstrict [rule_format]: "<c,s> -n-> t ==> !m. n<=m --> <c,s> -m-> t"
apply (erule evaln.induct)
-apply (tactic {* ALLGOALS (EVERY'[strip_tac,TRY o etac (thm "Suc_le_D_lemma"), REPEAT o smp_tac 1]) *})
-apply (tactic {* ALLGOALS (resolve_tac (thms "evaln.intros") THEN_ALL_NEW atac) *})
+apply (tactic {* ALLGOALS (EVERY'[strip_tac,TRY o etac @{thm Suc_le_D_lemma}, REPEAT o smp_tac 1]) *})
+apply (tactic {* ALLGOALS (resolve_tac @{thms evaln.intros} THEN_ALL_NEW atac) *})
done
lemma evaln_Suc: "<c,s> -n-> s' ==> <c,s> -Suc n-> s'"
@@ -142,8 +142,8 @@
lemma evalc_evaln: "<c,s> -c-> t ==> ? n. <c,s> -n-> t"
apply (erule evalc.induct)
apply (tactic {* ALLGOALS (REPEAT o etac exE) *})
-apply (tactic {* TRYALL (EVERY'[datac (thm "evaln_max2") 1, REPEAT o eresolve_tac [exE, conjE]]) *})
-apply (tactic {* ALLGOALS (rtac exI THEN' resolve_tac (thms "evaln.intros") THEN_ALL_NEW atac) *})
+apply (tactic {* TRYALL (EVERY' [datac @{thm evaln_max2} 1, REPEAT o eresolve_tac [exE, conjE]]) *})
+apply (tactic {* ALLGOALS (rtac exI THEN' resolve_tac @{thms evaln.intros} THEN_ALL_NEW atac) *})
done
lemma eval_eq: "<c,s> -c-> t = (? n. <c,s> -n-> t)"
--- a/src/HOL/IOA/Solve.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/IOA/Solve.thy Mon Sep 06 19:13:10 2010 +0200
@@ -146,7 +146,7 @@
apply (simp (no_asm) add: conj_disj_distribR cong add: conj_cong split add: split_if)
apply (tactic {*
REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
- asm_full_simp_tac(@{simpset} addsimps[thm "comp1_reachable", thm "comp2_reachable"]) 1) *})
+ asm_full_simp_tac(@{simpset} addsimps [@{thm comp1_reachable}, @{thm comp2_reachable}]) 1) *})
done
--- a/src/HOL/Import/hol4rews.ML Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/Import/hol4rews.ML Mon Sep 06 19:13:10 2010 +0200
@@ -156,13 +156,10 @@
val hol4_debug = Unsynchronized.ref false
fun message s = if !hol4_debug then writeln s else ()
-local
- val eq_reflection = thm "eq_reflection"
-in
fun add_hol4_rewrite (Context.Theory thy, th) =
let
val _ = message "Adding HOL4 rewrite"
- val th1 = th RS eq_reflection
+ val th1 = th RS @{thm eq_reflection}
val current_rews = HOL4Rewrites.get thy
val new_rews = insert Thm.eq_thm th1 current_rews
val updated_thy = HOL4Rewrites.put new_rews thy
@@ -170,7 +167,6 @@
(Context.Theory updated_thy,th1)
end
| add_hol4_rewrite (context, th) = (context, th RS eq_reflection);
-end
fun ignore_hol4 bthy bthm thy =
let
--- a/src/HOL/Import/proof_kernel.ML Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML Mon Sep 06 19:13:10 2010 +0200
@@ -977,28 +977,28 @@
| NONE => raise ERR "uniq_compose" "No result"
end
-val reflexivity_thm = thm "refl"
-val substitution_thm = thm "subst"
-val mp_thm = thm "mp"
-val imp_antisym_thm = thm "light_imp_as"
-val disch_thm = thm "impI"
-val ccontr_thm = thm "ccontr"
+val reflexivity_thm = @{thm refl}
+val substitution_thm = @{thm subst}
+val mp_thm = @{thm mp}
+val imp_antisym_thm = @{thm light_imp_as}
+val disch_thm = @{thm impI}
+val ccontr_thm = @{thm ccontr}
-val meta_eq_to_obj_eq_thm = thm "meta_eq_to_obj_eq"
+val meta_eq_to_obj_eq_thm = @{thm meta_eq_to_obj_eq}
-val gen_thm = thm "HOLallI"
-val choose_thm = thm "exE"
-val exists_thm = thm "exI"
-val conj_thm = thm "conjI"
-val conjunct1_thm = thm "conjunct1"
-val conjunct2_thm = thm "conjunct2"
-val spec_thm = thm "spec"
-val disj_cases_thm = thm "disjE"
-val disj1_thm = thm "disjI1"
-val disj2_thm = thm "disjI2"
+val gen_thm = @{thm HOLallI}
+val choose_thm = @{thm exE}
+val exists_thm = @{thm exI}
+val conj_thm = @{thm conjI}
+val conjunct1_thm = @{thm conjunct1}
+val conjunct2_thm = @{thm conjunct2}
+val spec_thm = @{thm spec}
+val disj_cases_thm = @{thm disjE}
+val disj1_thm = @{thm disjI1}
+val disj2_thm = @{thm disjI2}
local
- val th = thm "not_def"
+ val th = @{thm not_def}
val thy = theory_of_thm th
val pp = Thm.reflexive (cterm_of thy (Const(@{const_name Trueprop},HOLogic.boolT-->propT)))
in
@@ -1006,13 +1006,13 @@
end
val not_intro_thm = Thm.symmetric not_elim_thm
-val abs_thm = thm "ext"
-val trans_thm = thm "trans"
-val symmetry_thm = thm "sym"
-val transitivity_thm = thm "trans"
-val eqmp_thm = thm "iffD1"
-val eqimp_thm = thm "HOL4Setup.eq_imp"
-val comb_thm = thm "cong"
+val abs_thm = @{thm ext}
+val trans_thm = @{thm trans}
+val symmetry_thm = @{thm sym}
+val transitivity_thm = @{thm trans}
+val eqmp_thm = @{thm iffD1}
+val eqimp_thm = @{thm HOL4Setup.eq_imp}
+val comb_thm = @{thm cong}
(* Beta-eta normalizes a theorem (only the conclusion, not the *
hypotheses!) *)
@@ -1971,9 +1971,6 @@
(thy22',hth)
end
-local
- val helper = thm "termspec_help"
-in
fun new_specification thyname thmname names hth thy =
case HOL4DefThy.get thy of
Replaying _ => (thy,hth)
@@ -2054,8 +2051,6 @@
intern_store_thm false thyname thmname hth thy''
end
-end
-
fun new_axiom name tm thy = raise ERR "new_axiom" ("Oh, no you don't! (" ^ name ^ ")")
fun to_isa_thm (hth as HOLThm(_,th)) =
@@ -2068,10 +2063,10 @@
fun to_isa_term tm = tm
local
- val light_nonempty = thm "light_ex_imp_nonempty"
- val ex_imp_nonempty = thm "ex_imp_nonempty"
- val typedef_hol2hol4 = thm "typedef_hol2hol4"
- val typedef_hol2hollight = thm "typedef_hol2hollight"
+ val light_nonempty = @{thm light_ex_imp_nonempty}
+ val ex_imp_nonempty = @{thm ex_imp_nonempty}
+ val typedef_hol2hol4 = @{thm typedef_hol2hol4}
+ val typedef_hol2hollight = @{thm typedef_hol2hollight}
in
fun new_type_definition thyname thmname tycname hth thy =
case HOL4DefThy.get thy of
--- a/src/HOL/Import/shuffler.ML Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/Import/shuffler.ML Mon Sep 06 19:13:10 2010 +0200
@@ -346,7 +346,7 @@
fun beta_fun thy assume t =
SOME (Thm.beta_conversion true (cterm_of thy t))
-val meta_sym_rew = thm "refl"
+val meta_sym_rew = @{thm refl}
fun equals_fun thy assume t =
case t of
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Mon Sep 06 19:13:10 2010 +0200
@@ -201,7 +201,7 @@
-- "several simplifications, XcptE, XcptEs, XcptS, Skip, Nil??"
apply( simp_all)
apply( tactic "ALLGOALS strip_tac")
-apply( tactic {* ALLGOALS (eresolve_tac [thm "ty_expr.cases", thm "ty_exprs.cases", thm "wt_stmt.cases"]
+apply( tactic {* ALLGOALS (eresolve_tac [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}]
THEN_ALL_NEW (full_simp_tac (global_simpset_of @{theory Conform}))) *})
apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])")
@@ -241,7 +241,7 @@
apply( fast elim: conforms_localD [THEN lconfD])
-- "for FAss"
-apply( tactic {* EVERY'[eresolve_tac [thm "ty_expr.cases", thm "ty_exprs.cases", thm "wt_stmt.cases"]
+apply( tactic {* EVERY'[eresolve_tac [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}]
THEN_ALL_NEW (full_simp_tac @{simpset}), REPEAT o (etac conjE), hyp_subst_tac] 3*})
-- "for if"
@@ -277,7 +277,7 @@
-- "7 LAss"
apply (fold fun_upd_def)
-apply( tactic {* (eresolve_tac [thm "ty_expr.cases", thm "ty_exprs.cases", thm "wt_stmt.cases"]
+apply( tactic {* (eresolve_tac [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}]
THEN_ALL_NEW (full_simp_tac @{simpset})) 1 *})
apply (intro strip)
apply (case_tac E)
--- a/src/HOL/NSA/NSA.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/NSA/NSA.thy Mon Sep 06 19:13:10 2010 +0200
@@ -663,9 +663,9 @@
***)
(*reorientation simprules using ==, for the following simproc*)
-val meta_zero_approx_reorient = thm "zero_approx_reorient" RS eq_reflection;
-val meta_one_approx_reorient = thm "one_approx_reorient" RS eq_reflection;
-val meta_number_of_approx_reorient = thm "number_of_approx_reorient" RS eq_reflection
+val meta_zero_approx_reorient = @{thm zero_approx_reorient} RS eq_reflection;
+val meta_one_approx_reorient = @{thm one_approx_reorient} RS eq_reflection;
+val meta_number_of_approx_reorient = @{thm number_of_approx_reorient} RS eq_reflection
(*reorientation simplification procedure: reorients (polymorphic)
0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
--- a/src/HOL/Nominal/nominal_datatype.ML Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Mon Sep 06 19:13:10 2010 +0200
@@ -24,18 +24,18 @@
structure NominalDatatype : NOMINAL_DATATYPE =
struct
-val finite_emptyI = thm "finite.emptyI";
-val finite_Diff = thm "finite_Diff";
-val finite_Un = thm "finite_Un";
-val Un_iff = thm "Un_iff";
-val In0_eq = thm "In0_eq";
-val In1_eq = thm "In1_eq";
-val In0_not_In1 = thm "In0_not_In1";
-val In1_not_In0 = thm "In1_not_In0";
-val Un_assoc = thm "Un_assoc";
-val Collect_disj_eq = thm "Collect_disj_eq";
+val finite_emptyI = @{thm finite.emptyI};
+val finite_Diff = @{thm finite_Diff};
+val finite_Un = @{thm finite_Un};
+val Un_iff = @{thm Un_iff};
+val In0_eq = @{thm In0_eq};
+val In1_eq = @{thm In1_eq};
+val In0_not_In1 = @{thm In0_not_In1};
+val In1_not_In0 = @{thm In1_not_In0};
+val Un_assoc = @{thm Un_assoc};
+val Collect_disj_eq = @{thm Collect_disj_eq};
val Collect_False_empty = @{thm empty_def [THEN sym, THEN eq_reflection]};
-val empty_iff = thm "empty_iff";
+val empty_iff = @{thm empty_iff};
open Datatype_Aux;
open NominalAtoms;
@@ -119,7 +119,7 @@
(** simplification procedure for sorting permutations **)
-val dj_cp = thm "dj_cp";
+val dj_cp = @{thm dj_cp};
fun dest_permT (Type ("fun", [Type ("List.list", [Type (@{type_name Product_Type.prod}, [T, _])]),
Type ("fun", [_, U])])) = (T, U);
@@ -148,23 +148,21 @@
val perm_simproc =
Simplifier.simproc_global @{theory} "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc';
-val meta_spec = thm "meta_spec";
-
fun projections rule =
Project_Rule.projections (ProofContext.init_global (Thm.theory_of_thm rule)) rule
|> map (Drule.export_without_context #> Rule_Cases.save rule);
-val supp_prod = thm "supp_prod";
-val fresh_prod = thm "fresh_prod";
-val supports_fresh = thm "supports_fresh";
-val supports_def = thm "Nominal.supports_def";
-val fresh_def = thm "fresh_def";
-val supp_def = thm "supp_def";
-val rev_simps = thms "rev.simps";
-val app_simps = thms "append.simps";
-val at_fin_set_supp = thm "at_fin_set_supp";
-val at_fin_set_fresh = thm "at_fin_set_fresh";
-val abs_fun_eq1 = thm "abs_fun_eq1";
+val supp_prod = @{thm supp_prod};
+val fresh_prod = @{thm fresh_prod};
+val supports_fresh = @{thm supports_fresh};
+val supports_def = @{thm Nominal.supports_def};
+val fresh_def = @{thm fresh_def};
+val supp_def = @{thm supp_def};
+val rev_simps = @{thms rev.simps};
+val app_simps = @{thms append.simps};
+val at_fin_set_supp = @{thm at_fin_set_supp};
+val at_fin_set_fresh = @{thm at_fin_set_fresh};
+val abs_fun_eq1 = @{thm abs_fun_eq1};
val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
@@ -1406,7 +1404,7 @@
[rtac induct_aux' 1,
REPEAT (resolve_tac fs_atoms 1),
REPEAT ((resolve_tac prems THEN_ALL_NEW
- (etac meta_spec ORELSE' full_simp_tac (HOL_basic_ss addsimps [fresh_def]))) 1)])
+ (etac @{thm meta_spec} ORELSE' full_simp_tac (HOL_basic_ss addsimps [fresh_def]))) 1)])
val (_, thy10) = thy9 |>
Sign.add_path big_name |>
--- a/src/HOL/Nominal/nominal_inductive.ML Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Mon Sep 06 19:13:10 2010 +0200
@@ -30,10 +30,10 @@
fun preds_of ps t = inter (op = o apfst dest_Free) (Term.add_frees t []) ps;
-val fresh_prod = thm "fresh_prod";
+val fresh_prod = @{thm fresh_prod};
-val perm_bool = mk_meta_eq (thm "perm_bool");
-val perm_boolI = thm "perm_boolI";
+val perm_bool = mk_meta_eq @{thm perm_bool};
+val perm_boolI = @{thm perm_boolI};
val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb
(Drule.strip_imp_concl (cprop_of perm_boolI))));
--- a/src/HOL/Nominal/nominal_inductive2.ML Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Mon Sep 06 19:13:10 2010 +0200
@@ -36,8 +36,8 @@
fun preds_of ps t = inter (op = o apfst dest_Free) (Term.add_frees t []) ps;
-val perm_bool = mk_meta_eq (thm "perm_bool");
-val perm_boolI = thm "perm_boolI";
+val perm_bool = mk_meta_eq @{thm perm_bool};
+val perm_boolI = @{thm perm_boolI};
val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb
(Drule.strip_imp_concl (cprop_of perm_boolI))));
--- a/src/HOL/Old_Number_Theory/Chinese.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Chinese.thy Mon Sep 06 19:13:10 2010 +0200
@@ -169,11 +169,11 @@
"0 < n ==> i \<le> n ==> m_cond n mf ==> km_cond n kf mf
==> \<exists>!x. 0 \<le> x \<and> x < mf i \<and> [kf i * mhf mf n i * x = bf i] (mod mf i)"
apply (rule zcong_lineq_unique)
- apply (tactic {* stac (thm "zgcd_zmult_cancel") 2 *})
+ apply (tactic {* stac @{thm zgcd_zmult_cancel} 2 *})
apply (unfold m_cond_def km_cond_def mhf_def)
apply (simp_all (no_asm_simp))
apply safe
- apply (tactic {* stac (thm "zgcd_zmult_cancel") 3 *})
+ apply (tactic {* stac @{thm zgcd_zmult_cancel} 3 *})
apply (rule_tac [!] funprod_zgcd)
apply safe
apply simp_all
@@ -231,12 +231,12 @@
apply (rule_tac x = "x_sol n kf bf mf mod funprod mf 0 n" in exI)
apply (unfold lincong_sol_def)
apply safe
- apply (tactic {* stac (thm "zcong_zmod") 3 *})
- apply (tactic {* stac (thm "mod_mult_eq") 3 *})
- apply (tactic {* stac (thm "mod_mod_cancel") 3 *})
- apply (tactic {* stac (thm "x_sol_lin") 4 *})
- apply (tactic {* stac (thm "mod_mult_eq" RS sym) 6 *})
- apply (tactic {* stac (thm "zcong_zmod" RS sym) 6 *})
+ apply (tactic {* stac @{thm zcong_zmod} 3 *})
+ apply (tactic {* stac @{thm mod_mult_eq} 3 *})
+ apply (tactic {* stac @{thm mod_mod_cancel} 3 *})
+ apply (tactic {* stac @{thm x_sol_lin} 4 *})
+ apply (tactic {* stac (@{thm mod_mult_eq} RS sym) 6 *})
+ apply (tactic {* stac (@{thm zcong_zmod} RS sym) 6 *})
apply (subgoal_tac [6]
"0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i
\<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)")
--- a/src/HOL/Old_Number_Theory/IntPrimes.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/Old_Number_Theory/IntPrimes.thy Mon Sep 06 19:13:10 2010 +0200
@@ -399,7 +399,7 @@
zgcd a n = 1 ==> \<exists>!x. 0 \<le> x \<and> x < n \<and> [a * x = b] (mod n)"
apply auto
apply (rule_tac [2] zcong_zless_imp_eq)
- apply (tactic {* stac (thm "zcong_cancel2" RS sym) 6 *})
+ apply (tactic {* stac (@{thm zcong_cancel2} RS sym) 6 *})
apply (rule_tac [8] zcong_trans)
apply (simp_all (no_asm_simp))
prefer 2
--- a/src/HOL/Old_Number_Theory/WilsonBij.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/Old_Number_Theory/WilsonBij.thy Mon Sep 06 19:13:10 2010 +0200
@@ -145,9 +145,9 @@
apply (unfold inj_on_def)
apply auto
apply (rule zcong_zless_imp_eq)
- apply (tactic {* stac (thm "zcong_cancel" RS sym) 5 *})
+ apply (tactic {* stac (@{thm zcong_cancel} RS sym) 5 *})
apply (rule_tac [7] zcong_trans)
- apply (tactic {* stac (thm "zcong_sym") 8 *})
+ apply (tactic {* stac @{thm zcong_sym} 8 *})
apply (erule_tac [7] inv_is_inv)
apply (tactic "asm_simp_tac @{simpset} 9")
apply (erule_tac [9] inv_is_inv)
@@ -198,15 +198,15 @@
apply (unfold reciR_def uniqP_def)
apply auto
apply (rule zcong_zless_imp_eq)
- apply (tactic {* stac (thm "zcong_cancel2" RS sym) 5 *})
+ apply (tactic {* stac (@{thm zcong_cancel2} RS sym) 5 *})
apply (rule_tac [7] zcong_trans)
- apply (tactic {* stac (thm "zcong_sym") 8 *})
+ apply (tactic {* stac @{thm zcong_sym} 8 *})
apply (rule_tac [6] zless_zprime_imp_zrelprime)
apply auto
apply (rule zcong_zless_imp_eq)
- apply (tactic {* stac (thm "zcong_cancel" RS sym) 5 *})
+ apply (tactic {* stac (@{thm zcong_cancel} RS sym) 5 *})
apply (rule_tac [7] zcong_trans)
- apply (tactic {* stac (thm "zcong_sym") 8 *})
+ apply (tactic {* stac @{thm zcong_sym} 8 *})
apply (rule_tac [6] zless_zprime_imp_zrelprime)
apply auto
done
--- a/src/HOL/Old_Number_Theory/WilsonRuss.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy Mon Sep 06 19:13:10 2010 +0200
@@ -257,7 +257,7 @@
apply (subst wset.simps)
apply (auto, unfold Let_def, auto)
apply (subst setprod_insert)
- apply (tactic {* stac (thm "setprod_insert") 3 *})
+ apply (tactic {* stac @{thm setprod_insert} 3 *})
apply (subgoal_tac [5]
"zcong (a * inv p a * (\<Prod>x\<in>wset (a - 1) p. x)) (1 * 1) p")
prefer 5
--- a/src/HOL/Option.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/Option.thy Mon Sep 06 19:13:10 2010 +0200
@@ -47,7 +47,7 @@
by simp
declaration {* fn _ =>
- Classical.map_cs (fn cs => cs addSD2 ("ospec", thm "ospec"))
+ Classical.map_cs (fn cs => cs addSD2 ("ospec", @{thm ospec}))
*}
lemma elem_set [iff]: "(x : set xo) = (xo = Some x)"
--- a/src/HOL/Proofs/Lambda/Commutation.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/Proofs/Lambda/Commutation.thy Mon Sep 06 19:13:10 2010 +0200
@@ -130,9 +130,9 @@
apply (tactic {* safe_tac HOL_cs *})
apply (tactic {*
blast_tac (HOL_cs addIs
- [thm "sup_ge2" RS thm "rtranclp_mono" RS thm "predicate2D" RS thm "rtranclp_trans",
- thm "rtranclp_converseI", thm "conversepI",
- thm "sup_ge1" RS thm "rtranclp_mono" RS thm "predicate2D"]) 1 *})
+ [@{thm sup_ge2} RS @{thm rtranclp_mono} RS @{thm predicate2D} RS @{thm rtranclp_trans},
+ @{thm rtranclp_converseI}, @{thm conversepI},
+ @{thm sup_ge1} RS @{thm rtranclp_mono} RS @{thm predicate2D}]) 1 *})
apply (erule rtranclp_induct)
apply blast
apply (blast del: rtranclp.rtrancl_refl intro: rtranclp_trans)
--- a/src/HOL/Statespace/distinct_tree_prover.ML Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/Statespace/distinct_tree_prover.ML Mon Sep 06 19:13:10 2010 +0200
@@ -23,18 +23,19 @@
structure DistinctTreeProver : DISTINCT_TREE_PROVER =
struct
-val all_distinct_left = thm "DistinctTreeProver.all_distinct_left";
-val all_distinct_right = thm "DistinctTreeProver.all_distinct_right";
+
+val all_distinct_left = @{thm DistinctTreeProver.all_distinct_left};
+val all_distinct_right = @{thm DistinctTreeProver.all_distinct_right};
-val distinct_left = thm "DistinctTreeProver.distinct_left";
-val distinct_right = thm "DistinctTreeProver.distinct_right";
-val distinct_left_right = thm "DistinctTreeProver.distinct_left_right";
-val in_set_root = thm "DistinctTreeProver.in_set_root";
-val in_set_left = thm "DistinctTreeProver.in_set_left";
-val in_set_right = thm "DistinctTreeProver.in_set_right";
+val distinct_left = @{thm DistinctTreeProver.distinct_left};
+val distinct_right = @{thm DistinctTreeProver.distinct_right};
+val distinct_left_right = @{thm DistinctTreeProver.distinct_left_right};
+val in_set_root = @{thm DistinctTreeProver.in_set_root};
+val in_set_left = @{thm DistinctTreeProver.in_set_left};
+val in_set_right = @{thm DistinctTreeProver.in_set_right};
-val swap_neq = thm "DistinctTreeProver.swap_neq";
-val neq_to_eq_False = thm "DistinctTreeProver.neq_to_eq_False"
+val swap_neq = @{thm DistinctTreeProver.swap_neq};
+val neq_to_eq_False = @{thm DistinctTreeProver.neq_to_eq_False};
datatype Direction = Left | Right
@@ -273,9 +274,9 @@
end
-val delete_root = thm "DistinctTreeProver.delete_root";
-val delete_left = thm "DistinctTreeProver.delete_left";
-val delete_right = thm "DistinctTreeProver.delete_right";
+val delete_root = @{thm DistinctTreeProver.delete_root};
+val delete_left = @{thm DistinctTreeProver.delete_left};
+val delete_right = @{thm DistinctTreeProver.delete_right};
fun deleteProver dist_thm [] = delete_root OF [dist_thm]
| deleteProver dist_thm (p::ps) =
@@ -286,10 +287,10 @@
val del = deleteProver dist_thm' ps;
in discharge [dist_thm, del] del_rule end;
-val subtract_Tip = thm "DistinctTreeProver.subtract_Tip";
-val subtract_Node = thm "DistinctTreeProver.subtract_Node";
-val delete_Some_all_distinct = thm "DistinctTreeProver.delete_Some_all_distinct";
-val subtract_Some_all_distinct_res = thm "DistinctTreeProver.subtract_Some_all_distinct_res";
+val subtract_Tip = @{thm DistinctTreeProver.subtract_Tip};
+val subtract_Node = @{thm DistinctTreeProver.subtract_Node};
+val delete_Some_all_distinct = @{thm DistinctTreeProver.delete_Some_all_distinct};
+val subtract_Some_all_distinct_res = @{thm DistinctTreeProver.subtract_Some_all_distinct_res};
local
val (alpha,v) =
@@ -320,7 +321,7 @@
in discharge [del_tree, sub_l, sub_r] subtract_Node end
end
-val subtract_Some_all_distinct = thm "DistinctTreeProver.subtract_Some_all_distinct";
+val subtract_Some_all_distinct = @{thm DistinctTreeProver.subtract_Some_all_distinct};
fun distinct_implProver dist_thm ct =
let
val ctree = ct |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
--- a/src/HOL/Statespace/state_fun.ML Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/Statespace/state_fun.ML Mon Sep 06 19:13:10 2010 +0200
@@ -38,10 +38,10 @@
local
-val conj1_False = thm "conj1_False";
-val conj2_False = thm "conj2_False";
-val conj_True = thm "conj_True";
-val conj_cong = thm "conj_cong";
+val conj1_False = @{thm conj1_False};
+val conj2_False = @{thm conj2_False};
+val conj_True = @{thm conj_True};
+val conj_cong = @{thm conj_cong};
fun isFalse (Const (@{const_name False},_)) = true
| isFalse _ = false;
@@ -255,7 +255,7 @@
local
-val swap_ex_eq = thm "StateFun.swap_ex_eq";
+val swap_ex_eq = @{thm StateFun.swap_ex_eq};
fun is_selector thy T sel =
let
val (flds,more) = Record.get_recT_fields thy T
--- a/src/HOL/TLA/Memory/Memory.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/TLA/Memory/Memory.thy Mon Sep 06 19:13:10 2010 +0200
@@ -181,10 +181,10 @@
|- Calling ch p & (rs!p ~= #NotAResult)
--> Enabled (<MemReturn ch rs p>_(rtrner ch ! p, rs!p))"
apply (tactic
- {* action_simp_tac @{simpset} [thm "MemReturn_change" RSN (2, thm "enabled_mono") ] [] 1 *})
+ {* action_simp_tac @{simpset} [@{thm MemReturn_change} RSN (2, @{thm enabled_mono}) ] [] 1 *})
apply (tactic
- {* action_simp_tac (@{simpset} addsimps [thm "MemReturn_def", thm "Return_def",
- thm "rtrner_def"]) [exI] [thm "base_enabled", thm "Pair_inject"] 1 *})
+ {* action_simp_tac (@{simpset} addsimps [@{thm MemReturn_def}, @{thm Return_def},
+ @{thm rtrner_def}]) [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
done
lemma ReadInner_enabled: "!!p. basevars (rtrner ch ! p, rs!p) ==>
@@ -227,13 +227,13 @@
--> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))"
apply (auto simp: enabled_disj [try_rewrite] intro!: RWRNext_enabled [temp_use])
apply (case_tac "arg (ch w p)")
- apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "Read_def",
- temp_rewrite (thm "enabled_ex")]) [thm "ReadInner_enabled", exI] [] 1 *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm Read_def},
+ temp_rewrite @{thm enabled_ex}]) [@{thm ReadInner_enabled}, exI] [] 1 *})
apply (force dest: base_pair [temp_use])
apply (erule contrapos_np)
- apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "Write_def",
- temp_rewrite (thm "enabled_ex")])
- [thm "WriteInner_enabled", exI] [] 1 *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm Write_def},
+ temp_rewrite @{thm enabled_ex}])
+ [@{thm WriteInner_enabled}, exI] [] 1 *})
done
end
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Mon Sep 06 19:13:10 2010 +0200
@@ -255,10 +255,10 @@
apply (rule historyI)
apply assumption+
apply (rule MI_base)
- apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "HInit_def"]) [] [] 1 *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HInit_def}]) [] [] 1 *})
apply (erule fun_cong)
- apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def"])
- [thm "busy_squareI"] [] 1 *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HNext_def}])
+ [@{thm busy_squareI}] [] 1 *})
apply (erule fun_cong)
done
@@ -346,22 +346,22 @@
caller_def rtrner_def MVNROKBA_def S_def S1_def S2_def Calling_def)
lemma S1ClerkUnch: "|- [MClkNext memCh crCh cst p]_(c p) & $(S1 rmhist p) --> unchanged (c p)"
- by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use (thm "MClkidle")]
- addsimps2 [thm "S_def", thm "S1_def"]) *})
+ by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use @{thm MClkidle}]
+ addsimps2 [@{thm S_def}, @{thm S1_def}]) *})
lemma S1RPCUnch: "|- [RPCNext crCh rmCh rst p]_(r p) & $(S1 rmhist p) --> unchanged (r p)"
- by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use (thm "RPCidle")]
- addsimps2 [thm "S_def", thm "S1_def"]) *})
+ by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use @{thm RPCidle}]
+ addsimps2 [@{thm S_def}, @{thm S1_def}]) *})
lemma S1MemUnch: "|- [RNext rmCh mm ires p]_(m p) & $(S1 rmhist p) --> unchanged (m p)"
- by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use (thm "Memoryidle")]
- addsimps2 [thm "S_def", thm "S1_def"]) *})
+ by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use @{thm Memoryidle}]
+ addsimps2 [@{thm S_def}, @{thm S1_def}]) *})
lemma S1Hist: "|- [HNext rmhist p]_(c p,r p,m p,rmhist!p) & $(S1 rmhist p)
--> unchanged (rmhist!p)"
- by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def", thm "S_def",
- thm "S1_def", thm "MemReturn_def", thm "RPCFail_def", thm "MClkReply_def",
- thm "Return_def"]) [] [temp_use (thm "squareE")] 1 *})
+ by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HNext_def}, @{thm S_def},
+ @{thm S1_def}, @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm MClkReply_def},
+ @{thm Return_def}]) [] [temp_use @{thm squareE}] 1 *})
(* ------------------------------ State S2 ---------------------------------------- *)
@@ -375,9 +375,9 @@
lemma S2Forward: "|- $(S2 rmhist p) & MClkFwd memCh crCh cst p
& unchanged (e p, r p, m p, rmhist!p)
--> (S3 rmhist p)$"
- by (tactic {* action_simp_tac (@{simpset} addsimps [thm "MClkFwd_def",
- thm "Call_def", thm "e_def", thm "r_def", thm "m_def", thm "caller_def",
- thm "rtrner_def", thm "S_def", thm "S2_def", thm "S3_def", thm "Calling_def"]) [] [] 1 *})
+ by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm MClkFwd_def},
+ @{thm Call_def}, @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def},
+ @{thm rtrner_def}, @{thm S_def}, @{thm S2_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1 *})
lemma S2RPCUnch: "|- [RPCNext crCh rmCh rst p]_(r p) & $(S2 rmhist p) --> unchanged (r p)"
by (auto simp: S_def S2_def dest!: RPCidle [temp_use])
@@ -387,8 +387,8 @@
lemma S2Hist: "|- [HNext rmhist p]_(c p,r p,m p,rmhist!p) & $(S2 rmhist p)
--> unchanged (rmhist!p)"
- by (tactic {* auto_tac (MI_fast_css addsimps2 [thm "HNext_def", thm "MemReturn_def",
- thm "RPCFail_def", thm "MClkReply_def", thm "Return_def", thm "S_def", thm "S2_def"]) *})
+ by (tactic {* auto_tac (MI_fast_css addsimps2 [@{thm HNext_def}, @{thm MemReturn_def},
+ @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm S_def}, @{thm S2_def}]) *})
(* ------------------------------ State S3 ---------------------------------------- *)
@@ -411,19 +411,19 @@
lemma S3Forward: "|- RPCFwd crCh rmCh rst p & HNext rmhist p & $(S3 rmhist p)
& unchanged (e p, c p, m p)
--> (S4 rmhist p)$ & unchanged (rmhist!p)"
- by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCFwd_def",
- thm "HNext_def", thm "MemReturn_def", thm "RPCFail_def",
- thm "MClkReply_def", thm "Return_def", thm "Call_def", thm "e_def",
- thm "c_def", thm "m_def", thm "caller_def", thm "rtrner_def", thm "S_def",
- thm "S3_def", thm "S4_def", thm "Calling_def"]) [] [] 1 *})
+ by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm RPCFwd_def},
+ @{thm HNext_def}, @{thm MemReturn_def}, @{thm RPCFail_def},
+ @{thm MClkReply_def}, @{thm Return_def}, @{thm Call_def}, @{thm e_def},
+ @{thm c_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def},
+ @{thm S3_def}, @{thm S4_def}, @{thm Calling_def}]) [] [] 1 *})
lemma S3Fail: "|- RPCFail crCh rmCh rst p & $(S3 rmhist p) & HNext rmhist p
& unchanged (e p, c p, m p)
--> (S6 rmhist p)$"
- by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def",
- thm "RPCFail_def", thm "Return_def", thm "e_def", thm "c_def",
- thm "m_def", thm "caller_def", thm "rtrner_def", thm "MVOKBARF_def",
- thm "S_def", thm "S3_def", thm "S6_def", thm "Calling_def"]) [] [] 1 *})
+ by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HNext_def},
+ @{thm RPCFail_def}, @{thm Return_def}, @{thm e_def}, @{thm c_def},
+ @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm MVOKBARF_def},
+ @{thm S_def}, @{thm S3_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1 *})
lemma S3MemUnch: "|- [RNext rmCh mm ires p]_(m p) & $(S3 rmhist p) --> unchanged (m p)"
by (auto simp: S_def S3_def dest!: Memoryidle [temp_use])
@@ -441,18 +441,18 @@
by (auto simp: S_def S4_def dest!: MClkbusy [temp_use])
lemma S4RPCUnch: "|- [RPCNext crCh rmCh rst p]_(r p) & $(S4 rmhist p) --> unchanged (r p)"
- by (tactic {* auto_tac (MI_fast_css addsimps2 [thm "S_def", thm "S4_def"]
- addSDs2 [temp_use (thm "RPCbusy")]) *})
+ by (tactic {* auto_tac (MI_fast_css addsimps2 [@{thm S_def}, @{thm S4_def}]
+ addSDs2 [temp_use @{thm RPCbusy}]) *})
lemma S4ReadInner: "|- ReadInner rmCh mm ires p l & $(S4 rmhist p) & unchanged (e p, c p, r p)
& HNext rmhist p & $(MemInv mm l)
--> (S4 rmhist p)$ & unchanged (rmhist!p)"
- by (tactic {* action_simp_tac (@{simpset} addsimps [thm "ReadInner_def",
- thm "GoodRead_def", thm "BadRead_def", thm "HNext_def", thm "MemReturn_def",
- thm "RPCFail_def", thm "MClkReply_def", thm "Return_def", thm "e_def",
- thm "c_def", thm "r_def", thm "rtrner_def", thm "caller_def",
- thm "MVNROKBA_def", thm "S_def", thm "S4_def", thm "RdRequest_def",
- thm "Calling_def", thm "MemInv_def"]) [] [] 1 *})
+ by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ReadInner_def},
+ @{thm GoodRead_def}, @{thm BadRead_def}, @{thm HNext_def}, @{thm MemReturn_def},
+ @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm e_def},
+ @{thm c_def}, @{thm r_def}, @{thm rtrner_def}, @{thm caller_def},
+ @{thm MVNROKBA_def}, @{thm S_def}, @{thm S4_def}, @{thm RdRequest_def},
+ @{thm Calling_def}, @{thm MemInv_def}]) [] [] 1 *})
lemma S4Read: "|- Read rmCh mm ires p & $(S4 rmhist p) & unchanged (e p, c p, r p)
& HNext rmhist p & (!l. $MemInv mm l)
@@ -461,11 +461,11 @@
lemma S4WriteInner: "|- WriteInner rmCh mm ires p l v & $(S4 rmhist p) & unchanged (e p, c p, r p) & HNext rmhist p
--> (S4 rmhist p)$ & unchanged (rmhist!p)"
- by (tactic {* action_simp_tac (@{simpset} addsimps [thm "WriteInner_def",
- thm "GoodWrite_def", thm "BadWrite_def", thm "HNext_def", thm "MemReturn_def",
- thm "RPCFail_def", thm "MClkReply_def", thm "Return_def", thm "e_def",
- thm "c_def", thm "r_def", thm "rtrner_def", thm "caller_def", thm "MVNROKBA_def",
- thm "S_def", thm "S4_def", thm "WrRequest_def", thm "Calling_def"]) [] [] 1 *})
+ by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm WriteInner_def},
+ @{thm GoodWrite_def}, @{thm BadWrite_def}, @{thm HNext_def}, @{thm MemReturn_def},
+ @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm e_def},
+ @{thm c_def}, @{thm r_def}, @{thm rtrner_def}, @{thm caller_def}, @{thm MVNROKBA_def},
+ @{thm S_def}, @{thm S4_def}, @{thm WrRequest_def}, @{thm Calling_def}]) [] [] 1 *})
lemma S4Write: "|- Write rmCh mm ires p l & $(S4 rmhist p) & unchanged (e p, c p, r p)
& (HNext rmhist p)
@@ -500,26 +500,26 @@
lemma S5Reply: "|- RPCReply crCh rmCh rst p & $(S5 rmhist p) & unchanged (e p, c p, m p,rmhist!p)
--> (S6 rmhist p)$"
- by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCReply_def",
- thm "Return_def", thm "e_def", thm "c_def", thm "m_def", thm "MVOKBA_def",
- thm "MVOKBARF_def", thm "caller_def", thm "rtrner_def", thm "S_def",
- thm "S5_def", thm "S6_def", thm "Calling_def"]) [] [] 1 *})
+ by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm RPCReply_def},
+ @{thm Return_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}, @{thm MVOKBA_def},
+ @{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def},
+ @{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1 *})
lemma S5Fail: "|- RPCFail crCh rmCh rst p & $(S5 rmhist p) & unchanged (e p, c p, m p,rmhist!p)
--> (S6 rmhist p)$"
- by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCFail_def",
- thm "Return_def", thm "e_def", thm "c_def", thm "m_def",
- thm "MVOKBARF_def", thm "caller_def", thm "rtrner_def",
- thm "S_def", thm "S5_def", thm "S6_def", thm "Calling_def"]) [] [] 1 *})
+ by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm RPCFail_def},
+ @{thm Return_def}, @{thm e_def}, @{thm c_def}, @{thm m_def},
+ @{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def},
+ @{thm S_def}, @{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1 *})
lemma S5MemUnch: "|- [RNext rmCh mm ires p]_(m p) & $(S5 rmhist p) --> unchanged (m p)"
by (auto simp: S_def S5_def dest!: Memoryidle [temp_use])
lemma S5Hist: "|- [HNext rmhist p]_(c p, r p, m p, rmhist!p) & $(S5 rmhist p)
--> (rmhist!p)$ = $(rmhist!p)"
- by (tactic {* auto_tac (MI_fast_css addsimps2 [thm "HNext_def",
- thm "MemReturn_def", thm "RPCFail_def", thm "MClkReply_def", thm "Return_def",
- thm "S_def", thm "S5_def"]) *})
+ by (tactic {* auto_tac (MI_fast_css addsimps2 [@{thm HNext_def},
+ @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def},
+ @{thm S_def}, @{thm S5_def}]) *})
(* ------------------------------ State S6 ---------------------------------------- *)
@@ -533,18 +533,18 @@
lemma S6Retry: "|- MClkRetry memCh crCh cst p & HNext rmhist p & $S6 rmhist p
& unchanged (e p,r p,m p)
--> (S3 rmhist p)$ & unchanged (rmhist!p)"
- by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def",
- thm "MClkReply_def", thm "MClkRetry_def", thm "Call_def", thm "Return_def",
- thm "e_def", thm "r_def", thm "m_def", thm "caller_def", thm "rtrner_def",
- thm "S_def", thm "S6_def", thm "S3_def", thm "Calling_def"]) [] [] 1 *})
+ by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HNext_def},
+ @{thm MClkReply_def}, @{thm MClkRetry_def}, @{thm Call_def}, @{thm Return_def},
+ @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def},
+ @{thm S_def}, @{thm S6_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1 *})
lemma S6Reply: "|- MClkReply memCh crCh cst p & HNext rmhist p & $S6 rmhist p
& unchanged (e p,r p,m p)
--> (S1 rmhist p)$"
- by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def",
- thm "MemReturn_def", thm "RPCFail_def", thm "Return_def", thm "MClkReply_def",
- thm "e_def", thm "r_def", thm "m_def", thm "caller_def", thm "rtrner_def",
- thm "S_def", thm "S6_def", thm "S1_def", thm "Calling_def"]) [] [] 1 *})
+ by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HNext_def},
+ @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm Return_def}, @{thm MClkReply_def},
+ @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def},
+ @{thm S_def}, @{thm S6_def}, @{thm S1_def}, @{thm Calling_def}]) [] [] 1 *})
lemma S6RPCUnch: "|- [RPCNext crCh rmCh rst p]_(r p) & $S6 rmhist p --> unchanged (r p)"
by (auto simp: S_def S6_def dest!: RPCidle [temp_use])
@@ -563,9 +563,9 @@
(* The implementation's initial condition implies the state predicate S1 *)
lemma Step1_1: "|- ImpInit p & HInit rmhist p --> S1 rmhist p"
- by (tactic {* auto_tac (MI_fast_css addsimps2 [thm "MVNROKBA_def",
- thm "MClkInit_def", thm "RPCInit_def", thm "PInit_def", thm "HInit_def",
- thm "ImpInit_def", thm "S_def", thm "S1_def"]) *})
+ by (tactic {* auto_tac (MI_fast_css addsimps2 [@{thm MVNROKBA_def},
+ @{thm MClkInit_def}, @{thm RPCInit_def}, @{thm PInit_def}, @{thm HInit_def},
+ @{thm ImpInit_def}, @{thm S_def}, @{thm S1_def}]) *})
(* ========== Step 1.2 ================================================== *)
(* Figure 16 is a predicate-action diagram for the implementation. *)
@@ -573,29 +573,29 @@
lemma Step1_2_1: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
& ~unchanged (e p, c p, r p, m p, rmhist!p) & $S1 rmhist p
--> (S2 rmhist p)$ & ENext p & unchanged (c p, r p, m p)"
- apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
- (map temp_elim [thm "S1ClerkUnch", thm "S1RPCUnch", thm "S1MemUnch", thm "S1Hist"]) 1 *})
- apply (tactic {* auto_tac (MI_fast_css addSIs2 [temp_use (thm "S1Env")]) *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) []
+ (map temp_elim [@{thm S1ClerkUnch}, @{thm S1RPCUnch}, @{thm S1MemUnch}, @{thm S1Hist}]) 1 *})
+ apply (tactic {* auto_tac (MI_fast_css addSIs2 [temp_use @{thm S1Env}]) *})
done
lemma Step1_2_2: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
& ~unchanged (e p, c p, r p, m p, rmhist!p) & $S2 rmhist p
--> (S3 rmhist p)$ & MClkFwd memCh crCh cst p
& unchanged (e p, r p, m p, rmhist!p)"
- apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
- (map temp_elim [thm "S2EnvUnch", thm "S2RPCUnch", thm "S2MemUnch", thm "S2Hist"]) 1 *})
- apply (tactic {* auto_tac (MI_fast_css addSIs2 [temp_use (thm "S2Clerk"),
- temp_use (thm "S2Forward")]) *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) []
+ (map temp_elim [@{thm S2EnvUnch}, @{thm S2RPCUnch}, @{thm S2MemUnch}, @{thm S2Hist}]) 1 *})
+ apply (tactic {* auto_tac (MI_fast_css addSIs2 [temp_use @{thm S2Clerk},
+ temp_use @{thm S2Forward}]) *})
done
lemma Step1_2_3: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
& ~unchanged (e p, c p, r p, m p, rmhist!p) & $S3 rmhist p
--> ((S4 rmhist p)$ & RPCFwd crCh rmCh rst p & unchanged (e p, c p, m p, rmhist!p))
| ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
- apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
- (map temp_elim [thm "S3EnvUnch", thm "S3ClerkUnch", thm "S3MemUnch"]) 1 *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) []
+ (map temp_elim [@{thm S3EnvUnch}, @{thm S3ClerkUnch}, @{thm S3MemUnch}]) 1 *})
apply (tactic {* action_simp_tac @{simpset} []
- (thm "squareE" :: map temp_elim [thm "S3RPC", thm "S3Forward", thm "S3Fail"]) 1 *})
+ (@{thm squareE} :: map temp_elim [@{thm S3RPC}, @{thm S3Forward}, @{thm S3Fail}]) 1 *})
apply (auto dest!: S3Hist [temp_use])
done
@@ -605,10 +605,10 @@
--> ((S4 rmhist p)$ & Read rmCh mm ires p & unchanged (e p, c p, r p, rmhist!p))
| ((S4 rmhist p)$ & (? l. Write rmCh mm ires p l) & unchanged (e p, c p, r p, rmhist!p))
| ((S5 rmhist p)$ & MemReturn rmCh ires p & unchanged (e p, c p, r p))"
- apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
- (map temp_elim [thm "S4EnvUnch", thm "S4ClerkUnch", thm "S4RPCUnch"]) 1 *})
- apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "RNext_def"]) []
- (thm "squareE" :: map temp_elim [thm "S4Read", thm "S4Write", thm "S4Return"]) 1 *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) []
+ (map temp_elim [@{thm S4EnvUnch}, @{thm S4ClerkUnch}, @{thm S4RPCUnch}]) 1 *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm RNext_def}]) []
+ (@{thm squareE} :: map temp_elim [@{thm S4Read}, @{thm S4Write}, @{thm S4Return}]) 1 *})
apply (auto dest!: S4Hist [temp_use])
done
@@ -616,21 +616,21 @@
& ~unchanged (e p, c p, r p, m p, rmhist!p) & $S5 rmhist p
--> ((S6 rmhist p)$ & RPCReply crCh rmCh rst p & unchanged (e p, c p, m p))
| ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
- apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
- (map temp_elim [thm "S5EnvUnch", thm "S5ClerkUnch", thm "S5MemUnch", thm "S5Hist"]) 1 *})
- apply (tactic {* action_simp_tac @{simpset} [] [thm "squareE", temp_elim (thm "S5RPC")] 1 *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) []
+ (map temp_elim [@{thm S5EnvUnch}, @{thm S5ClerkUnch}, @{thm S5MemUnch}, @{thm S5Hist}]) 1 *})
+ apply (tactic {* action_simp_tac @{simpset} [] [@{thm squareE}, temp_elim @{thm S5RPC}] 1 *})
apply (tactic {* auto_tac (MI_fast_css addSDs2
- [temp_use (thm "S5Reply"), temp_use (thm "S5Fail")]) *})
+ [temp_use @{thm S5Reply}, temp_use @{thm S5Fail}]) *})
done
lemma Step1_2_6: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
& ~unchanged (e p, c p, r p, m p, rmhist!p) & $S6 rmhist p
--> ((S1 rmhist p)$ & MClkReply memCh crCh cst p & unchanged (e p, r p, m p))
| ((S3 rmhist p)$ & MClkRetry memCh crCh cst p & unchanged (e p,r p,m p,rmhist!p))"
- apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
- (map temp_elim [thm "S6EnvUnch", thm "S6RPCUnch", thm "S6MemUnch"]) 1 *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) []
+ (map temp_elim [@{thm S6EnvUnch}, @{thm S6RPCUnch}, @{thm S6MemUnch}]) 1 *})
apply (tactic {* action_simp_tac @{simpset} []
- (thm "squareE" :: map temp_elim [thm "S6Clerk", thm "S6Retry", thm "S6Reply"]) 1 *})
+ (@{thm squareE} :: map temp_elim [@{thm S6Clerk}, @{thm S6Retry}, @{thm S6Reply}]) 1 *})
apply (auto dest: S6Hist [temp_use])
done
@@ -641,8 +641,8 @@
section "Initialization (Step 1.3)"
lemma Step1_3: "|- S1 rmhist p --> PInit (resbar rmhist) p"
- by (tactic {* action_simp_tac (@{simpset} addsimps [thm "resbar_def",
- thm "PInit_def", thm "S_def", thm "S1_def"]) [] [] 1 *})
+ by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm resbar_def},
+ @{thm PInit_def}, @{thm S_def}, @{thm S1_def}]) [] [] 1 *})
(* ----------------------------------------------------------------------
Step 1.4: Implementation's next-state relation simulates specification's
@@ -653,23 +653,23 @@
lemma Step1_4_1: "|- ENext p & $S1 rmhist p & (S2 rmhist p)$ & unchanged (c p, r p, m p)
--> unchanged (rtrner memCh!p, resbar rmhist!p)"
- by (tactic {* auto_tac (MI_fast_css addsimps2 [thm "c_def", thm "r_def",
- thm "m_def", thm "resbar_def"]) *})
+ by (tactic {* auto_tac (MI_fast_css addsimps2 [@{thm c_def}, @{thm r_def},
+ @{thm m_def}, @{thm resbar_def}]) *})
lemma Step1_4_2: "|- MClkFwd memCh crCh cst p & $S2 rmhist p & (S3 rmhist p)$
& unchanged (e p, r p, m p, rmhist!p)
--> unchanged (rtrner memCh!p, resbar rmhist!p)"
by (tactic {* action_simp_tac
- (@{simpset} addsimps [thm "MClkFwd_def", thm "e_def", thm "r_def", thm "m_def",
- thm "resbar_def", thm "S_def", thm "S2_def", thm "S3_def"]) [] [] 1 *})
+ (@{simpset} addsimps [@{thm MClkFwd_def}, @{thm e_def}, @{thm r_def}, @{thm m_def},
+ @{thm resbar_def}, @{thm S_def}, @{thm S2_def}, @{thm S3_def}]) [] [] 1 *})
lemma Step1_4_3a: "|- RPCFwd crCh rmCh rst p & $S3 rmhist p & (S4 rmhist p)$
& unchanged (e p, c p, m p, rmhist!p)
--> unchanged (rtrner memCh!p, resbar rmhist!p)"
apply clarsimp
apply (drule S3_excl [temp_use] S4_excl [temp_use])+
- apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def",
- thm "c_def", thm "m_def", thm "resbar_def", thm "S_def", thm "S3_def"]) [] [] 1 *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm e_def},
+ @{thm c_def}, @{thm m_def}, @{thm resbar_def}, @{thm S_def}, @{thm S3_def}]) [] [] 1 *})
done
lemma Step1_4_3b: "|- RPCFail crCh rmCh rst p & $S3 rmhist p & (S6 rmhist p)$
@@ -687,13 +687,13 @@
--> ReadInner memCh mm (resbar rmhist) p l"
apply clarsimp
apply (drule S4_excl [temp_use])+
- apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ReadInner_def",
- thm "GoodRead_def", thm "BadRead_def", thm "e_def", thm "c_def", thm "m_def"]) [] [] 1 *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ReadInner_def},
+ @{thm GoodRead_def}, @{thm BadRead_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}]) [] [] 1 *})
apply (auto simp: resbar_def)
apply (tactic {* ALLGOALS (action_simp_tac
- (@{simpset} addsimps [thm "RPCRelayArg_def", thm "MClkRelayArg_def",
- thm "S_def", thm "S4_def", thm "RdRequest_def", thm "MemInv_def"])
- [] [thm "impE", thm "MemValNotAResultE"]) *})
+ (@{simpset} addsimps [@{thm RPCRelayArg_def}, @{thm MClkRelayArg_def},
+ @{thm S_def}, @{thm S4_def}, @{thm RdRequest_def}, @{thm MemInv_def}])
+ [] [@{thm impE}, @{thm MemValNotAResultE}]) *})
done
lemma Step1_4_4a: "|- Read rmCh mm ires p & $S4 rmhist p & (S4 rmhist p)$
@@ -707,12 +707,12 @@
apply clarsimp
apply (drule S4_excl [temp_use])+
apply (tactic {* action_simp_tac (@{simpset} addsimps
- [thm "WriteInner_def", thm "GoodWrite_def", thm "BadWrite_def", thm "e_def",
- thm "c_def", thm "m_def"]) [] [] 1 *})
+ [@{thm WriteInner_def}, @{thm GoodWrite_def}, @{thm BadWrite_def}, @{thm e_def},
+ @{thm c_def}, @{thm m_def}]) [] [] 1 *})
apply (auto simp: resbar_def)
apply (tactic {* ALLGOALS (action_simp_tac (@{simpset} addsimps
- [thm "RPCRelayArg_def", thm "MClkRelayArg_def", thm "S_def",
- thm "S4_def", thm "WrRequest_def"]) [] []) *})
+ [@{thm RPCRelayArg_def}, @{thm MClkRelayArg_def}, @{thm S_def},
+ @{thm S4_def}, @{thm WrRequest_def}]) [] []) *})
done
lemma Step1_4_4b: "|- Write rmCh mm ires p l & $S4 rmhist p & (S4 rmhist p)$
@@ -723,10 +723,10 @@
lemma Step1_4_4c: "|- MemReturn rmCh ires p & $S4 rmhist p & (S5 rmhist p)$
& unchanged (e p, c p, r p)
--> unchanged (rtrner memCh!p, resbar rmhist!p)"
- apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def",
- thm "c_def", thm "r_def", thm "resbar_def"]) [] [] 1 *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm e_def},
+ @{thm c_def}, @{thm r_def}, @{thm resbar_def}]) [] [] 1 *})
apply (drule S4_excl [temp_use] S5_excl [temp_use])+
- apply (tactic {* auto_tac (MI_fast_css addsimps2 [thm "MemReturn_def", thm "Return_def"]) *})
+ apply (tactic {* auto_tac (MI_fast_css addsimps2 [@{thm MemReturn_def}, @{thm Return_def}]) *})
done
lemma Step1_4_5a: "|- RPCReply crCh rmCh rst p & $S5 rmhist p & (S6 rmhist p)$
@@ -752,12 +752,12 @@
--> MemReturn memCh (resbar rmhist) p"
apply clarsimp
apply (drule S6_excl [temp_use])+
- apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def",
- thm "r_def", thm "m_def", thm "MClkReply_def", thm "MemReturn_def",
- thm "Return_def", thm "resbar_def"]) [] [] 1 *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm e_def},
+ @{thm r_def}, @{thm m_def}, @{thm MClkReply_def}, @{thm MemReturn_def},
+ @{thm Return_def}, @{thm resbar_def}]) [] [] 1 *})
apply simp_all (* simplify if-then-else *)
apply (tactic {* ALLGOALS (action_simp_tac (@{simpset} addsimps
- [thm "MClkReplyVal_def", thm "S6_def", thm "S_def"]) [] [thm "MVOKBARFnotNR"]) *})
+ [@{thm MClkReplyVal_def}, @{thm S6_def}, @{thm S_def}]) [] [@{thm MVOKBARFnotNR}]) *})
done
lemma Step1_4_6b: "|- MClkRetry memCh crCh cst p & $S6 rmhist p & (S3 rmhist p)$
@@ -765,8 +765,8 @@
--> MemFail memCh (resbar rmhist) p"
apply clarsimp
apply (drule S3_excl [temp_use])+
- apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def", thm "r_def",
- thm "m_def", thm "MClkRetry_def", thm "MemFail_def", thm "resbar_def"]) [] [] 1 *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm e_def}, @{thm r_def},
+ @{thm m_def}, @{thm MClkRetry_def}, @{thm MemFail_def}, @{thm resbar_def}]) [] [] 1 *})
apply (auto simp: S6_def S_def)
done
@@ -816,7 +816,7 @@
lemma unchanged_safe: "|- (~unchanged (e p, c p, r p, m p, rmhist!p)
--> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p))
--> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
- apply (tactic {* split_idle_tac @{context} [thm "square_def"] 1 *})
+ apply (tactic {* split_idle_tac @{context} [@{thm square_def}] 1 *})
apply force
done
(* turn into (unsafe, looping!) introduction rule *)
@@ -898,15 +898,15 @@
lemma S1_RNextdisabled: "|- S1 rmhist p -->
~Enabled (<RNext memCh mm (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
- apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "angle_def",
- thm "S_def", thm "S1_def"]) [notI] [thm "enabledE", temp_elim (thm "Memoryidle")] 1 *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm angle_def},
+ @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}, temp_elim @{thm Memoryidle}] 1 *})
apply force
done
lemma S1_Returndisabled: "|- S1 rmhist p -->
~Enabled (<MemReturn memCh (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
- by (tactic {* action_simp_tac (@{simpset} addsimps [thm "angle_def", thm "MemReturn_def",
- thm "Return_def", thm "S_def", thm "S1_def"]) [notI] [thm "enabledE"] 1 *})
+ by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm angle_def}, @{thm MemReturn_def},
+ @{thm Return_def}, @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}] 1 *})
lemma RNext_fair: "|- []<>S1 rmhist p
--> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
@@ -986,7 +986,7 @@
& ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (ALL l. $MemInv mm l)
--> (S4 rmhist p & ires!p = #NotAResult)$
| ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)$"
- apply (tactic {* split_idle_tac @{context} [thm "m_def"] 1 *})
+ apply (tactic {* split_idle_tac @{context} [@{thm m_def}] 1 *})
apply (auto dest!: Step1_2_4 [temp_use])
done
@@ -1017,7 +1017,7 @@
lemma S4b_successors: "|- $(S4 rmhist p & ires!p ~= #NotAResult)
& ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (ALL l. $MemInv mm l)
--> (S4 rmhist p & ires!p ~= #NotAResult)$ | (S5 rmhist p)$"
- apply (tactic {* split_idle_tac @{context} [thm "m_def"] 1 *})
+ apply (tactic {* split_idle_tac @{context} [@{thm m_def}] 1 *})
apply (auto dest!: WriteResult [temp_use] Step1_2_4 [temp_use] ReadResult [temp_use])
done
@@ -1084,16 +1084,16 @@
lemma MClkReplyS6:
"|- $ImpInv rmhist p & <MClkReply memCh crCh cst p>_(c p) --> $S6 rmhist p"
- by (tactic {* action_simp_tac (@{simpset} addsimps [thm "angle_def",
- thm "MClkReply_def", thm "Return_def", thm "ImpInv_def", thm "S_def",
- thm "S1_def", thm "S2_def", thm "S3_def", thm "S4_def", thm "S5_def"]) [] [] 1 *})
+ by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm angle_def},
+ @{thm MClkReply_def}, @{thm Return_def}, @{thm ImpInv_def}, @{thm S_def},
+ @{thm S1_def}, @{thm S2_def}, @{thm S3_def}, @{thm S4_def}, @{thm S5_def}]) [] [] 1 *})
lemma S6MClkReply_enabled: "|- S6 rmhist p --> Enabled (<MClkReply memCh crCh cst p>_(c p))"
apply (auto simp: c_def intro!: MClkReply_enabled [temp_use])
apply (cut_tac MI_base)
apply (blast dest: base_pair)
apply (tactic {* ALLGOALS (action_simp_tac (@{simpset}
- addsimps [thm "S_def", thm "S6_def"]) [] []) *})
+ addsimps [@{thm S_def}, @{thm S6_def}]) [] []) *})
done
lemma S6_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & $(ImpInv rmhist p))
@@ -1104,7 +1104,7 @@
apply (erule InfiniteEnsures)
apply assumption
apply (tactic {* action_simp_tac @{simpset} []
- (map temp_elim [thm "MClkReplyS6", thm "S6MClkReply_successors"]) 1 *})
+ (map temp_elim [@{thm MClkReplyS6}, @{thm S6MClkReply_successors}]) 1 *})
apply (auto simp: SF_def)
apply (erule contrapos_np)
apply (auto intro!: S6MClkReply_enabled [temp_use] elim!: STL4E [temp_use] DmdImplE [temp_use])
@@ -1191,7 +1191,7 @@
==> sigma |= []<>S1 rmhist p"
apply (rule classical)
apply (tactic {* asm_lr_simp_tac (@{simpset} addsimps
- [temp_use (thm "NotBox"), temp_rewrite (thm "NotDmd")]) 1 *})
+ [temp_use @{thm NotBox}, temp_rewrite @{thm NotDmd}]) 1 *})
apply (auto elim!: leadsto_infinite [temp_use] mp dest!: DBImplBD [temp_use])
done
--- a/src/HOL/TLA/Memory/RPC.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/TLA/Memory/RPC.thy Mon Sep 06 19:13:10 2010 +0200
@@ -103,15 +103,15 @@
(* Enabledness of some actions *)
lemma RPCFail_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, rst!p) ==>
|- ~Calling rcv p & Calling send p --> Enabled (RPCFail send rcv rst p)"
- by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCFail_def",
- thm "Return_def", thm "caller_def", thm "rtrner_def"]) [exI]
- [thm "base_enabled", thm "Pair_inject"] 1 *})
+ by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm RPCFail_def},
+ @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
+ [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
lemma RPCReply_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, rst!p) ==>
|- ~Calling rcv p & Calling send p & rst!p = #rpcB
--> Enabled (RPCReply send rcv rst p)"
- by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCReply_def",
- thm "Return_def", thm "caller_def", thm "rtrner_def"]) [exI]
- [thm "base_enabled", thm "Pair_inject"] 1 *})
+ by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm RPCReply_def},
+ @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
+ [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
end
--- a/src/HOL/Tools/Qelim/cooper.ML Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Mon Sep 06 19:13:10 2010 +0200
@@ -423,7 +423,7 @@
val emptyIS = @{cterm "{}::int set"};
val insert_tm = @{cterm "insert :: int => _"};
fun mkISet cts = fold_rev (Thm.capply insert_tm #> Thm.capply) cts emptyIS;
-val eqelem_imp_imp = (thm"eqelem_imp_iff") RS iffD1;
+val eqelem_imp_imp = @{thm eqelem_imp_iff} RS iffD1;
val [A_tm,B_tm] = map (fn th => cprop_of th |> funpow 2 Thm.dest_arg |> Thm.dest_abs NONE |> snd |> Thm.dest_arg1 |> Thm.dest_arg
|> Thm.dest_abs NONE |> snd |> Thm.dest_fun |> Thm.dest_arg)
[asetP,bsetP];
--- a/src/HOL/Tools/TFL/casesplit.ML Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/Tools/TFL/casesplit.ML Mon Sep 06 19:13:10 2010 +0200
@@ -32,9 +32,9 @@
val dest_Trueprop = HOLogic.dest_Trueprop;
val mk_Trueprop = HOLogic.mk_Trueprop;
-val atomize = thms "induct_atomize";
-val rulify = thms "induct_rulify";
-val rulify_fallback = thms "induct_rulify_fallback";
+val atomize = @{thms induct_atomize};
+val rulify = @{thms induct_rulify};
+val rulify_fallback = @{thms induct_rulify_fallback};
end;
--- a/src/HOL/Tools/TFL/thms.ML Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/Tools/TFL/thms.ML Mon Sep 06 19:13:10 2010 +0200
@@ -1,20 +1,19 @@
(* Title: HOL/Tools/TFL/thms.ML
- ID: $Id$
Author: Konrad Slind, Cambridge University Computer Laboratory
Copyright 1997 University of Cambridge
*)
structure Thms =
struct
- val WFREC_COROLLARY = thm "tfl_wfrec";
- val WF_INDUCTION_THM = thm "tfl_wf_induct";
- val CUT_DEF = thm "cut_def";
- val eqT = thm "tfl_eq_True";
- val rev_eq_mp = thm "tfl_rev_eq_mp";
- val simp_thm = thm "tfl_simp_thm";
- val P_imp_P_iff_True = thm "tfl_P_imp_P_iff_True";
- val imp_trans = thm "tfl_imp_trans";
- val disj_assoc = thm "tfl_disj_assoc";
- val tfl_disjE = thm "tfl_disjE";
- val choose_thm = thm "tfl_exE";
+ val WFREC_COROLLARY = @{thm tfl_wfrec};
+ val WF_INDUCTION_THM = @{thm tfl_wf_induct};
+ val CUT_DEF = @{thm cut_def};
+ val eqT = @{thm tfl_eq_True};
+ val rev_eq_mp = @{thm tfl_rev_eq_mp};
+ val simp_thm = @{thm tfl_simp_thm};
+ val P_imp_P_iff_True = @{thm tfl_P_imp_P_iff_True};
+ val imp_trans = @{thm tfl_imp_trans};
+ val disj_assoc = @{thm tfl_disj_assoc};
+ val tfl_disjE = @{thm tfl_disjE};
+ val choose_thm = @{thm tfl_exE};
end;
--- a/src/HOL/Tools/meson.ML Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/Tools/meson.ML Mon Sep 06 19:13:10 2010 +0200
@@ -68,24 +68,24 @@
val ex_forward = @{thm ex_forward};
val choice = @{thm choice};
-val not_conjD = thm "meson_not_conjD";
-val not_disjD = thm "meson_not_disjD";
-val not_notD = thm "meson_not_notD";
-val not_allD = thm "meson_not_allD";
-val not_exD = thm "meson_not_exD";
-val imp_to_disjD = thm "meson_imp_to_disjD";
-val not_impD = thm "meson_not_impD";
-val iff_to_disjD = thm "meson_iff_to_disjD";
-val not_iffD = thm "meson_not_iffD";
-val conj_exD1 = thm "meson_conj_exD1";
-val conj_exD2 = thm "meson_conj_exD2";
-val disj_exD = thm "meson_disj_exD";
-val disj_exD1 = thm "meson_disj_exD1";
-val disj_exD2 = thm "meson_disj_exD2";
-val disj_assoc = thm "meson_disj_assoc";
-val disj_comm = thm "meson_disj_comm";
-val disj_FalseD1 = thm "meson_disj_FalseD1";
-val disj_FalseD2 = thm "meson_disj_FalseD2";
+val not_conjD = @{thm meson_not_conjD};
+val not_disjD = @{thm meson_not_disjD};
+val not_notD = @{thm meson_not_notD};
+val not_allD = @{thm meson_not_allD};
+val not_exD = @{thm meson_not_exD};
+val imp_to_disjD = @{thm meson_imp_to_disjD};
+val not_impD = @{thm meson_not_impD};
+val iff_to_disjD = @{thm meson_iff_to_disjD};
+val not_iffD = @{thm meson_not_iffD};
+val conj_exD1 = @{thm meson_conj_exD1};
+val conj_exD2 = @{thm meson_conj_exD2};
+val disj_exD = @{thm meson_disj_exD};
+val disj_exD1 = @{thm meson_disj_exD1};
+val disj_exD2 = @{thm meson_disj_exD2};
+val disj_assoc = @{thm meson_disj_assoc};
+val disj_comm = @{thm meson_disj_comm};
+val disj_FalseD1 = @{thm meson_disj_FalseD1};
+val disj_FalseD2 = @{thm meson_disj_FalseD2};
(**** Operators for forward proof ****)
@@ -203,7 +203,7 @@
(*They are typically functional reflexivity axioms and are the converses of
injectivity equivalences*)
-val not_refl_disj_D = thm"meson_not_refl_disj_D";
+val not_refl_disj_D = @{thm meson_not_refl_disj_D};
(*Is either term a Var that does not properly occur in the other term?*)
fun eliminable (t as Var _, u) = t aconv u orelse not (Logic.occs(t,u))
--- a/src/HOL/UNITY/Comp/Alloc.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/UNITY/Comp/Alloc.thy Mon Sep 06 19:13:10 2010 +0200
@@ -426,7 +426,7 @@
apply (rule fst_o_funPair)
done
-ML {* bind_thms ("fst_o_client_map'", make_o_equivs (thm "fst_o_client_map")) *}
+ML {* bind_thms ("fst_o_client_map'", make_o_equivs @{thm fst_o_client_map}) *}
declare fst_o_client_map' [simp]
lemma snd_o_client_map: "snd o client_map = clientState_d.dummy"
@@ -434,7 +434,7 @@
apply (rule snd_o_funPair)
done
-ML {* bind_thms ("snd_o_client_map'", make_o_equivs (thm "snd_o_client_map")) *}
+ML {* bind_thms ("snd_o_client_map'", make_o_equivs @{thm snd_o_client_map}) *}
declare snd_o_client_map' [simp]
@@ -444,28 +444,28 @@
apply record_auto
done
-ML {* bind_thms ("client_o_sysOfAlloc'", make_o_equivs (thm "client_o_sysOfAlloc")) *}
+ML {* bind_thms ("client_o_sysOfAlloc'", make_o_equivs @{thm client_o_sysOfAlloc}) *}
declare client_o_sysOfAlloc' [simp]
lemma allocGiv_o_sysOfAlloc_eq: "allocGiv o sysOfAlloc = allocGiv"
apply record_auto
done
-ML {* bind_thms ("allocGiv_o_sysOfAlloc_eq'", make_o_equivs (thm "allocGiv_o_sysOfAlloc_eq")) *}
+ML {* bind_thms ("allocGiv_o_sysOfAlloc_eq'", make_o_equivs @{thm allocGiv_o_sysOfAlloc_eq}) *}
declare allocGiv_o_sysOfAlloc_eq' [simp]
lemma allocAsk_o_sysOfAlloc_eq: "allocAsk o sysOfAlloc = allocAsk"
apply record_auto
done
-ML {* bind_thms ("allocAsk_o_sysOfAlloc_eq'", make_o_equivs (thm "allocAsk_o_sysOfAlloc_eq")) *}
+ML {* bind_thms ("allocAsk_o_sysOfAlloc_eq'", make_o_equivs @{thm allocAsk_o_sysOfAlloc_eq}) *}
declare allocAsk_o_sysOfAlloc_eq' [simp]
lemma allocRel_o_sysOfAlloc_eq: "allocRel o sysOfAlloc = allocRel"
apply record_auto
done
-ML {* bind_thms ("allocRel_o_sysOfAlloc_eq'", make_o_equivs (thm "allocRel_o_sysOfAlloc_eq")) *}
+ML {* bind_thms ("allocRel_o_sysOfAlloc_eq'", make_o_equivs @{thm allocRel_o_sysOfAlloc_eq}) *}
declare allocRel_o_sysOfAlloc_eq' [simp]
@@ -475,49 +475,49 @@
apply record_auto
done
-ML {* bind_thms ("client_o_sysOfClient'", make_o_equivs (thm "client_o_sysOfClient")) *}
+ML {* bind_thms ("client_o_sysOfClient'", make_o_equivs @{thm client_o_sysOfClient}) *}
declare client_o_sysOfClient' [simp]
lemma allocGiv_o_sysOfClient_eq: "allocGiv o sysOfClient = allocGiv o snd "
apply record_auto
done
-ML {* bind_thms ("allocGiv_o_sysOfClient_eq'", make_o_equivs (thm "allocGiv_o_sysOfClient_eq")) *}
+ML {* bind_thms ("allocGiv_o_sysOfClient_eq'", make_o_equivs @{thm allocGiv_o_sysOfClient_eq}) *}
declare allocGiv_o_sysOfClient_eq' [simp]
lemma allocAsk_o_sysOfClient_eq: "allocAsk o sysOfClient = allocAsk o snd "
apply record_auto
done
-ML {* bind_thms ("allocAsk_o_sysOfClient_eq'", make_o_equivs (thm "allocAsk_o_sysOfClient_eq")) *}
+ML {* bind_thms ("allocAsk_o_sysOfClient_eq'", make_o_equivs @{thm allocAsk_o_sysOfClient_eq}) *}
declare allocAsk_o_sysOfClient_eq' [simp]
lemma allocRel_o_sysOfClient_eq: "allocRel o sysOfClient = allocRel o snd "
apply record_auto
done
-ML {* bind_thms ("allocRel_o_sysOfClient_eq'", make_o_equivs (thm "allocRel_o_sysOfClient_eq")) *}
+ML {* bind_thms ("allocRel_o_sysOfClient_eq'", make_o_equivs @{thm allocRel_o_sysOfClient_eq}) *}
declare allocRel_o_sysOfClient_eq' [simp]
lemma allocGiv_o_inv_sysOfAlloc_eq: "allocGiv o inv sysOfAlloc = allocGiv"
apply (simp add: o_def)
done
-ML {* bind_thms ("allocGiv_o_inv_sysOfAlloc_eq'", make_o_equivs (thm "allocGiv_o_inv_sysOfAlloc_eq")) *}
+ML {* bind_thms ("allocGiv_o_inv_sysOfAlloc_eq'", make_o_equivs @{thm allocGiv_o_inv_sysOfAlloc_eq}) *}
declare allocGiv_o_inv_sysOfAlloc_eq' [simp]
lemma allocAsk_o_inv_sysOfAlloc_eq: "allocAsk o inv sysOfAlloc = allocAsk"
apply (simp add: o_def)
done
-ML {* bind_thms ("allocAsk_o_inv_sysOfAlloc_eq'", make_o_equivs (thm "allocAsk_o_inv_sysOfAlloc_eq")) *}
+ML {* bind_thms ("allocAsk_o_inv_sysOfAlloc_eq'", make_o_equivs @{thm allocAsk_o_inv_sysOfAlloc_eq}) *}
declare allocAsk_o_inv_sysOfAlloc_eq' [simp]
lemma allocRel_o_inv_sysOfAlloc_eq: "allocRel o inv sysOfAlloc = allocRel"
apply (simp add: o_def)
done
-ML {* bind_thms ("allocRel_o_inv_sysOfAlloc_eq'", make_o_equivs (thm "allocRel_o_inv_sysOfAlloc_eq")) *}
+ML {* bind_thms ("allocRel_o_inv_sysOfAlloc_eq'", make_o_equivs @{thm allocRel_o_inv_sysOfAlloc_eq}) *}
declare allocRel_o_inv_sysOfAlloc_eq' [simp]
lemma rel_inv_client_map_drop_map: "(rel o inv client_map o drop_map i o inv sysOfClient) =
@@ -525,7 +525,7 @@
apply (simp add: o_def drop_map_def)
done
-ML {* bind_thms ("rel_inv_client_map_drop_map'", make_o_equivs (thm "rel_inv_client_map_drop_map")) *}
+ML {* bind_thms ("rel_inv_client_map_drop_map'", make_o_equivs @{thm rel_inv_client_map_drop_map}) *}
declare rel_inv_client_map_drop_map [simp]
lemma ask_inv_client_map_drop_map: "(ask o inv client_map o drop_map i o inv sysOfClient) =
@@ -533,7 +533,7 @@
apply (simp add: o_def drop_map_def)
done
-ML {* bind_thms ("ask_inv_client_map_drop_map'", make_o_equivs (thm "ask_inv_client_map_drop_map")) *}
+ML {* bind_thms ("ask_inv_client_map_drop_map'", make_o_equivs @{thm ask_inv_client_map_drop_map}) *}
declare ask_inv_client_map_drop_map [simp]
@@ -812,7 +812,7 @@
ML {*
-bind_thms ("System_Increasing'", list_of_Int (thm "System_Increasing"))
+bind_thms ("System_Increasing'", list_of_Int @{thm System_Increasing})
*}
declare System_Increasing' [intro!]
@@ -903,9 +903,9 @@
text{*safety (1), step 4 (final result!) *}
theorem System_safety: "System : system_safety"
apply (unfold system_safety_def)
- apply (tactic {* rtac (Always_Int_rule [thm "System_sum_bounded",
- thm "Always_tokens_giv_le_allocGiv", thm "Always_tokens_allocRel_le_rel"] RS
- thm "Always_weaken") 1 *})
+ apply (tactic {* rtac (Always_Int_rule [@{thm System_sum_bounded},
+ @{thm Always_tokens_giv_le_allocGiv}, @{thm Always_tokens_allocRel_le_rel}] RS
+ @{thm Always_weaken}) 1 *})
apply auto
apply (rule setsum_fun_mono [THEN order_trans])
apply (drule_tac [2] order_trans)
@@ -946,8 +946,8 @@
lemma System_Bounded_allocAsk: "System : Always {s. ALL i<Nclients.
ALL elt : set ((sub i o allocAsk) s). elt \<le> NbT}"
apply (auto simp add: Collect_all_imp_eq)
- apply (tactic {* rtac (Always_Int_rule [thm "Always_allocAsk_le_ask",
- thm "System_Bounded_ask"] RS thm "Always_weaken") 1 *})
+ apply (tactic {* rtac (Always_Int_rule [@{thm Always_allocAsk_le_ask},
+ @{thm System_Bounded_ask}] RS @{thm Always_weaken}) 1 *})
apply (auto dest: set_mono)
done
--- a/src/HOLCF/FOCUS/Fstream.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOLCF/FOCUS/Fstream.thy Mon Sep 06 19:13:10 2010 +0200
@@ -156,12 +156,12 @@
lemma slen_fscons_eq_rev:
"(#x < Fin (Suc (Suc n))) = (!a y. x ~= a~> y | #y < Fin (Suc n))"
apply (simp add: fscons_def2 slen_scons_eq_rev)
-apply (tactic {* step_tac (HOL_cs addSEs [thm "DefE"]) 1 *})
-apply (tactic {* step_tac (HOL_cs addSEs [thm "DefE"]) 1 *})
-apply (tactic {* step_tac (HOL_cs addSEs [thm "DefE"]) 1 *})
-apply (tactic {* step_tac (HOL_cs addSEs [thm "DefE"]) 1 *})
-apply (tactic {* step_tac (HOL_cs addSEs [thm "DefE"]) 1 *})
-apply (tactic {* step_tac (HOL_cs addSEs [thm "DefE"]) 1 *})
+apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
+apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
+apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
+apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
+apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
+apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
apply (erule contrapos_np)
apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE)
done
--- a/src/HOLCF/IOA/ABP/Correctness.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOLCF/IOA/ABP/Correctness.thy Mon Sep 06 19:13:10 2010 +0200
@@ -164,16 +164,16 @@
lemma sender_abstraction: "is_weak_ref_map reduce srch_ioa srch_fin_ioa"
apply (tactic {*
- simp_tac (HOL_ss addsimps [thm "srch_fin_ioa_def", thm "rsch_fin_ioa_def",
- thm "srch_ioa_def", thm "rsch_ioa_def", thm "rename_through_pmap",
- thm "channel_abstraction"]) 1 *})
+ simp_tac (HOL_ss addsimps [@{thm srch_fin_ioa_def}, @{thm rsch_fin_ioa_def},
+ @{thm srch_ioa_def}, @{thm rsch_ioa_def}, @{thm rename_through_pmap},
+ @{thm channel_abstraction}]) 1 *})
done
lemma receiver_abstraction: "is_weak_ref_map reduce rsch_ioa rsch_fin_ioa"
apply (tactic {*
- simp_tac (HOL_ss addsimps [thm "srch_fin_ioa_def", thm "rsch_fin_ioa_def",
- thm "srch_ioa_def", thm "rsch_ioa_def", thm "rename_through_pmap",
- thm "channel_abstraction"]) 1 *})
+ simp_tac (HOL_ss addsimps [@{thm srch_fin_ioa_def}, @{thm rsch_fin_ioa_def},
+ @{thm srch_ioa_def}, @{thm rsch_ioa_def}, @{thm rename_through_pmap},
+ @{thm channel_abstraction}]) 1 *})
done
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy Mon Sep 06 19:13:10 2010 +0200
@@ -289,9 +289,9 @@
ML {*
local
- val defs = [thm "Filter_def", thm "Forall_def", thm "sforall_def", thm "mkex_def",
- thm "stutter_def"]
- val asigs = [thm "asig_of_par", thm "actions_asig_comp"]
+ val defs = [@{thm Filter_def}, @{thm Forall_def}, @{thm sforall_def}, @{thm mkex_def},
+ @{thm stutter_def}]
+ val asigs = [@{thm asig_of_par}, @{thm actions_asig_comp}]
in
fun mkex_induct_tac ctxt sch exA exB =
--- a/src/HOLCF/IOA/meta_theory/SimCorrectness.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.thy Mon Sep 06 19:13:10 2010 +0200
@@ -171,7 +171,7 @@
!s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R -->
mk_trace C$ex = mk_trace A$((corresp_ex_simC A R$ex) s')"
-apply (tactic {* pair_induct_tac @{context} "ex" [thm "is_exec_frag_def"] 1 *})
+apply (tactic {* pair_induct_tac @{context} "ex" [@{thm is_exec_frag_def}] 1 *})
(* cons case *)
apply auto
apply (rename_tac ex a t s s')
--- a/src/HOLCF/ex/Focus_ex.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOLCF/ex/Focus_ex.thy Mon Sep 06 19:13:10 2010 +0200
@@ -180,7 +180,7 @@
done
lemma lemma3: "def_g(g) --> is_g(g)"
-apply (tactic {* simp_tac (HOL_ss addsimps [thm "def_g_def", thm "lemma1", thm "lemma2"]) 1 *})
+apply (tactic {* simp_tac (HOL_ss addsimps [@{thm def_g_def}, @{thm lemma1}, @{thm lemma2}]) 1 *})
apply (rule impI)
apply (erule exE)
apply (rule_tac x = "f" in exI)
@@ -205,7 +205,7 @@
lemma lemma4: "is_g(g) --> def_g(g)"
apply (tactic {* simp_tac (HOL_ss delsimps (@{thms HOL.ex_simps} @ @{thms HOL.all_simps})
- addsimps [thm "lemma1", thm "lemma2", thm "def_g_def"]) 1 *})
+ addsimps [@{thm lemma1}, @{thm lemma2}, @{thm def_g_def}]) 1 *})
apply (rule impI)
apply (erule exE)
apply (rule_tac x = "f" in exI)
--- a/src/HOLCF/ex/Loop.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOLCF/ex/Loop.thy Mon Sep 06 19:13:10 2010 +0200
@@ -104,12 +104,12 @@
apply (simp (no_asm) add: step_def2)
apply (rule_tac p = "b$ (iterate n$ (step$b$g) $x) " in trE)
apply (erule notE)
-apply (tactic {* asm_simp_tac (HOLCF_ss addsimps [thm "step_def2"]) 1 *})
+apply (tactic {* asm_simp_tac (HOLCF_ss addsimps [@{thm step_def2}]) 1 *})
apply (tactic "asm_simp_tac HOLCF_ss 1")
apply (rule mp)
apply (erule spec)
-apply (tactic {* asm_simp_tac (HOLCF_ss delsimps [thm "iterate_Suc"]
- addsimps [thm "loop_lemma2"]) 1 *})
+apply (tactic {* asm_simp_tac (HOLCF_ss delsimps [@{thm iterate_Suc}]
+ addsimps [@{thm loop_lemma2}]) 1 *})
apply (rule_tac s = "iterate (Suc n) $ (step$b$g) $x"
and t = "g$ (iterate n$ (step$b$g) $x) " in ssubst)
prefer 2 apply (assumption)
--- a/src/Provers/quasi.ML Mon Sep 06 19:11:01 2010 +0200
+++ b/src/Provers/quasi.ML Mon Sep 06 19:13:10 2010 +0200
@@ -149,7 +149,7 @@
| "~=" => if (x aconv y) then
raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE))
else [ NotEq (x, y, Asm n),
- NotEq (y, x,Thm ( [Asm n], thm "not_sym"))]
+ NotEq (y, x,Thm ( [Asm n], @{thm not_sym}))]
| _ => error ("quasi_tac: unknown relation symbol ``" ^ rel ^
"''returned by decomp_quasi."))
| NONE => [];
@@ -300,7 +300,7 @@
let
val leEdge = Le (x,y, Thm ([p], Less.less_imp_le))
val neqEdges = [ NotEq (x,y, Thm ([p], Less.less_imp_neq)),
- NotEq (y,x, Thm ( [Thm ([p], Less.less_imp_neq)], thm "not_sym"))]
+ NotEq (y,x, Thm ( [Thm ([p], Less.less_imp_neq)], @{thm not_sym}))]
in
buildGraphs (ls, addEdge(y,[],(addEdge (x,[(y,leEdge)],leG))), neqEdges@neqE)
end
@@ -459,9 +459,10 @@
let
fun findParallelNeq [] = NONE
| findParallelNeq (e::es) =
- if (x aconv (lower e) andalso y aconv (upper e)) then SOME e
- else if (y aconv (lower e) andalso x aconv (upper e)) then SOME (NotEq (x,y, (Thm ([getprf e], thm "not_sym"))))
- else findParallelNeq es ;
+ if (x aconv (lower e) andalso y aconv (upper e)) then SOME e
+ else if (y aconv (lower e) andalso x aconv (upper e))
+ then SOME (NotEq (x,y, (Thm ([getprf e], @{thm not_sym}))))
+ else findParallelNeq es;
in
(* test if there is a edge x ~= y respectivly y ~= x and *)
(* if it possible to find a path x <= y in leG, thus we can conclude x < y *)
@@ -483,7 +484,7 @@
(case (Library.find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of
(SOME (NotEq (x, y, p)), NotEq (x', y', _)) =>
if (x aconv x' andalso y aconv y') then p
- else Thm ([p], thm "not_sym")
+ else Thm ([p], @{thm not_sym})
| _ => raise Cannot
)
--- a/src/Sequents/ILL.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/Sequents/ILL.thy Mon Sep 06 19:13:10 2010 +0200
@@ -126,24 +126,16 @@
ML {*
-
val lazy_cs = empty_pack
- add_safes [thm "tensl", thm "conjr", thm "disjl", thm "promote0",
- thm "context2", thm "context3"]
- add_unsafes [thm "identity", thm "zerol", thm "conjll", thm "conjlr",
- thm "disjrl", thm "disjrr", thm "impr", thm "tensr", thm "impl",
- thm "derelict", thm "weaken", thm "promote1", thm "promote2",
- thm "context1", thm "context4a", thm "context4b"];
+ add_safes [@{thm tensl}, @{thm conjr}, @{thm disjl}, @{thm promote0},
+ @{thm context2}, @{thm context3}]
+ add_unsafes [@{thm identity}, @{thm zerol}, @{thm conjll}, @{thm conjlr},
+ @{thm disjrl}, @{thm disjrr}, @{thm impr}, @{thm tensr}, @{thm impl},
+ @{thm derelict}, @{thm weaken}, @{thm promote1}, @{thm promote2},
+ @{thm context1}, @{thm context4a}, @{thm context4b}];
-local
- val promote0 = thm "promote0"
- val promote1 = thm "promote1"
- val promote2 = thm "promote2"
-in
-
-fun prom_tac n = REPEAT (resolve_tac [promote0,promote1,promote2] n)
-
-end
+fun prom_tac n =
+ REPEAT (resolve_tac [@{thm promote0}, @{thm promote1}, @{thm promote2}] n)
*}
method_setup best_lazy =
@@ -272,13 +264,12 @@
done
ML {*
+val safe_cs = lazy_cs add_safes [@{thm conj_lemma}, @{thm ll_mp}, @{thm contrad1},
+ @{thm contrad2}, @{thm mp_rule1}, @{thm mp_rule2}, @{thm o_a_rule},
+ @{thm a_not_a_rule}]
+ add_unsafes [@{thm aux_impl}];
-val safe_cs = lazy_cs add_safes [thm "conj_lemma", thm "ll_mp", thm "contrad1",
- thm "contrad2", thm "mp_rule1", thm "mp_rule2", thm "o_a_rule",
- thm "a_not_a_rule"]
- add_unsafes [thm "aux_impl"];
-
-val power_cs = safe_cs add_unsafes [thm "impr_contr_der"];
+val power_cs = safe_cs add_unsafes [@{thm impr_contr_der}];
*}
--- a/src/Sequents/LK0.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/Sequents/LK0.thy Mon Sep 06 19:13:10 2010 +0200
@@ -210,27 +210,19 @@
ML {*
val prop_pack = empty_pack add_safes
- [thm "basic", thm "refl", thm "TrueR", thm "FalseL",
- thm "conjL", thm "conjR", thm "disjL", thm "disjR", thm "impL", thm "impR",
- thm "notL", thm "notR", thm "iffL", thm "iffR"];
+ [@{thm basic}, @{thm refl}, @{thm TrueR}, @{thm FalseL},
+ @{thm conjL}, @{thm conjR}, @{thm disjL}, @{thm disjR}, @{thm impL}, @{thm impR},
+ @{thm notL}, @{thm notR}, @{thm iffL}, @{thm iffR}];
-val LK_pack = prop_pack add_safes [thm "allR", thm "exL"]
- add_unsafes [thm "allL_thin", thm "exR_thin", thm "the_equality"];
+val LK_pack = prop_pack add_safes [@{thm allR}, @{thm exL}]
+ add_unsafes [@{thm allL_thin}, @{thm exR_thin}, @{thm the_equality}];
-val LK_dup_pack = prop_pack add_safes [thm "allR", thm "exL"]
- add_unsafes [thm "allL", thm "exR", thm "the_equality"];
+val LK_dup_pack = prop_pack add_safes [@{thm allR}, @{thm exL}]
+ add_unsafes [@{thm allL}, @{thm exR}, @{thm the_equality}];
-local
- val thinR = thm "thinR"
- val thinL = thm "thinL"
- val cut = thm "cut"
-in
-
fun lemma_tac th i =
- rtac (thinR RS cut) i THEN REPEAT (rtac thinL i) THEN rtac th i;
-
-end;
+ rtac (@{thm thinR} RS @{thm cut}) i THEN REPEAT (rtac @{thm thinL} i) THEN rtac th i;
*}
method_setup fast_prop =
@@ -321,10 +313,10 @@
(** Equality **)
lemma sym: "|- a=b --> b=a"
- by (tactic {* safe_tac (LK_pack add_safes [thm "subst"]) 1 *})
+ by (tactic {* safe_tac (LK_pack add_safes [@{thm subst}]) 1 *})
lemma trans: "|- a=b --> b=c --> a=c"
- by (tactic {* safe_tac (LK_pack add_safes [thm "subst"]) 1 *})
+ by (tactic {* safe_tac (LK_pack add_safes [@{thm subst}]) 1 *})
(* Symmetry of equality in hypotheses *)
lemmas symL = sym [THEN L_of_imp, standard]
--- a/src/Sequents/S4.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/Sequents/S4.thy Mon Sep 06 19:13:10 2010 +0200
@@ -34,12 +34,12 @@
ML {*
structure S4_Prover = Modal_ProverFun
(
- val rewrite_rls = thms "rewrite_rls"
- val safe_rls = thms "safe_rls"
- val unsafe_rls = thms "unsafe_rls" @ [thm "boxR", thm "diaL"]
- val bound_rls = thms "bound_rls" @ [thm "boxL", thm "diaR"]
- val aside_rls = [thm "lstar0", thm "lstar1", thm "lstar2", thm "rstar0",
- thm "rstar1", thm "rstar2"]
+ val rewrite_rls = @{thms rewrite_rls}
+ val safe_rls = @{thms safe_rls}
+ val unsafe_rls = @{thms unsafe_rls} @ [@{thm boxR}, @{thm diaL}]
+ val bound_rls = @{thms bound_rls} @ [@{thm boxL}, @{thm diaR}]
+ val aside_rls = [@{thm lstar0}, @{thm lstar1}, @{thm lstar2}, @{thm rstar0},
+ @{thm rstar1}, @{thm rstar2}]
)
*}
--- a/src/Sequents/S43.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/Sequents/S43.thy Mon Sep 06 19:13:10 2010 +0200
@@ -79,12 +79,12 @@
ML {*
structure S43_Prover = Modal_ProverFun
(
- val rewrite_rls = thms "rewrite_rls"
- val safe_rls = thms "safe_rls"
- val unsafe_rls = thms "unsafe_rls" @ [thm "pi1", thm "pi2"]
- val bound_rls = thms "bound_rls" @ [thm "boxL", thm "diaR"]
- val aside_rls = [thm "lstar0", thm "lstar1", thm "lstar2", thm "rstar0",
- thm "rstar1", thm "rstar2", thm "S43pi0", thm "S43pi1", thm "S43pi2"]
+ val rewrite_rls = @{thms rewrite_rls}
+ val safe_rls = @{thms safe_rls}
+ val unsafe_rls = @{thms unsafe_rls} @ [@{thm pi1}, @{thm pi2}]
+ val bound_rls = @{thms bound_rls} @ [@{thm boxL}, @{thm diaR}]
+ val aside_rls = [@{thm lstar0}, @{thm lstar1}, @{thm lstar2}, @{thm rstar0},
+ @{thm rstar1}, @{thm rstar2}, @{thm S43pi0}, @{thm S43pi1}, @{thm S43pi2}]
)
*}
--- a/src/Sequents/T.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/Sequents/T.thy Mon Sep 06 19:13:10 2010 +0200
@@ -33,12 +33,12 @@
ML {*
structure T_Prover = Modal_ProverFun
(
- val rewrite_rls = thms "rewrite_rls"
- val safe_rls = thms "safe_rls"
- val unsafe_rls = thms "unsafe_rls" @ [thm "boxR", thm "diaL"]
- val bound_rls = thms "bound_rls" @ [thm "boxL", thm "diaR"]
- val aside_rls = [thm "lstar0", thm "lstar1", thm "lstar2", thm "rstar0",
- thm "rstar1", thm "rstar2"]
+ val rewrite_rls = @{thms rewrite_rls}
+ val safe_rls = @{thms safe_rls}
+ val unsafe_rls = @{thms unsafe_rls} @ [@{thm boxR}, @{thm diaL}]
+ val bound_rls = @{thms bound_rls} @ [@{thm boxL}, @{thm diaR}]
+ val aside_rls = [@{thm lstar0}, @{thm lstar1}, @{thm lstar2}, @{thm rstar0},
+ @{thm rstar1}, @{thm rstar2}]
)
*}
--- a/src/Sequents/Washing.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/Sequents/Washing.thy Mon Sep 06 19:13:10 2010 +0200
@@ -33,27 +33,27 @@
(* "activate" definitions for use in proof *)
-ML {* bind_thms ("changeI", [thm "context1"] RL ([thm "change"] RLN (2,[thm "cut"]))) *}
-ML {* bind_thms ("load1I", [thm "context1"] RL ([thm "load1"] RLN (2,[thm "cut"]))) *}
-ML {* bind_thms ("washI", [thm "context1"] RL ([thm "wash"] RLN (2,[thm "cut"]))) *}
-ML {* bind_thms ("dryI", [thm "context1"] RL ([thm "dry"] RLN (2,[thm "cut"]))) *}
+ML {* bind_thms ("changeI", [@{thm context1}] RL ([@{thm change}] RLN (2,[@{thm cut}]))) *}
+ML {* bind_thms ("load1I", [@{thm context1}] RL ([@{thm load1}] RLN (2,[@{thm cut}]))) *}
+ML {* bind_thms ("washI", [@{thm context1}] RL ([@{thm wash}] RLN (2,[@{thm cut}]))) *}
+ML {* bind_thms ("dryI", [@{thm context1}] RL ([@{thm dry}] RLN (2,[@{thm cut}]))) *}
(* a load of dirty clothes and two dollars gives you clean clothes *)
lemma "dollar , dollar , dirty |- clean"
- apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *})
+ apply (tactic {* best_tac (lazy_cs add_safes (@{thms changeI} @ @{thms load1I} @ @{thms washI} @ @{thms dryI})) 1 *})
done
(* order of premises doesn't matter *)
lemma "dollar , dirty , dollar |- clean"
- apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *})
+ apply (tactic {* best_tac (lazy_cs add_safes (@{thms changeI} @ @{thms load1I} @ @{thms washI} @ @{thms dryI})) 1 *})
done
(* alternative formulation *)
lemma "dollar , dollar |- dirty -o clean"
- apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *})
+ apply (tactic {* best_tac (lazy_cs add_safes (@{thms changeI} @ @{thms load1I} @ @{thms washI} @ @{thms dryI})) 1 *})
done
end
--- a/src/ZF/Bool.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/ZF/Bool.thy Mon Sep 06 19:13:10 2010 +0200
@@ -172,45 +172,44 @@
ML
{*
-val bool_def = thm "bool_def";
-
-val bool_defs = thms "bool_defs";
-val singleton_0 = thm "singleton_0";
-val bool_1I = thm "bool_1I";
-val bool_0I = thm "bool_0I";
-val one_not_0 = thm "one_not_0";
-val one_neq_0 = thm "one_neq_0";
-val boolE = thm "boolE";
-val cond_1 = thm "cond_1";
-val cond_0 = thm "cond_0";
-val cond_type = thm "cond_type";
-val cond_simple_type = thm "cond_simple_type";
-val def_cond_1 = thm "def_cond_1";
-val def_cond_0 = thm "def_cond_0";
-val not_1 = thm "not_1";
-val not_0 = thm "not_0";
-val and_1 = thm "and_1";
-val and_0 = thm "and_0";
-val or_1 = thm "or_1";
-val or_0 = thm "or_0";
-val xor_1 = thm "xor_1";
-val xor_0 = thm "xor_0";
-val not_type = thm "not_type";
-val and_type = thm "and_type";
-val or_type = thm "or_type";
-val xor_type = thm "xor_type";
-val bool_typechecks = thms "bool_typechecks";
-val not_not = thm "not_not";
-val not_and = thm "not_and";
-val not_or = thm "not_or";
-val and_absorb = thm "and_absorb";
-val and_commute = thm "and_commute";
-val and_assoc = thm "and_assoc";
-val and_or_distrib = thm "and_or_distrib";
-val or_absorb = thm "or_absorb";
-val or_commute = thm "or_commute";
-val or_assoc = thm "or_assoc";
-val or_and_distrib = thm "or_and_distrib";
+val bool_def = @{thm bool_def};
+val bool_defs = @{thms bool_defs};
+val singleton_0 = @{thm singleton_0};
+val bool_1I = @{thm bool_1I};
+val bool_0I = @{thm bool_0I};
+val one_not_0 = @{thm one_not_0};
+val one_neq_0 = @{thm one_neq_0};
+val boolE = @{thm boolE};
+val cond_1 = @{thm cond_1};
+val cond_0 = @{thm cond_0};
+val cond_type = @{thm cond_type};
+val cond_simple_type = @{thm cond_simple_type};
+val def_cond_1 = @{thm def_cond_1};
+val def_cond_0 = @{thm def_cond_0};
+val not_1 = @{thm not_1};
+val not_0 = @{thm not_0};
+val and_1 = @{thm and_1};
+val and_0 = @{thm and_0};
+val or_1 = @{thm or_1};
+val or_0 = @{thm or_0};
+val xor_1 = @{thm xor_1};
+val xor_0 = @{thm xor_0};
+val not_type = @{thm not_type};
+val and_type = @{thm and_type};
+val or_type = @{thm or_type};
+val xor_type = @{thm xor_type};
+val bool_typechecks = @{thms bool_typechecks};
+val not_not = @{thm not_not};
+val not_and = @{thm not_and};
+val not_or = @{thm not_or};
+val and_absorb = @{thm and_absorb};
+val and_commute = @{thm and_commute};
+val and_assoc = @{thm and_assoc};
+val and_or_distrib = @{thm and_or_distrib};
+val or_absorb = @{thm or_absorb};
+val or_commute = @{thm or_commute};
+val or_assoc = @{thm or_assoc};
+val or_and_distrib = @{thm or_and_distrib};
*}
end
--- a/src/ZF/Cardinal.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/ZF/Cardinal.thy Mon Sep 06 19:13:10 2010 +0200
@@ -1044,134 +1044,134 @@
ML
{*
-val Least_def = thm "Least_def";
-val eqpoll_def = thm "eqpoll_def";
-val lepoll_def = thm "lepoll_def";
-val lesspoll_def = thm "lesspoll_def";
-val cardinal_def = thm "cardinal_def";
-val Finite_def = thm "Finite_def";
-val Card_def = thm "Card_def";
-val eq_imp_not_mem = thm "eq_imp_not_mem";
-val decomp_bnd_mono = thm "decomp_bnd_mono";
-val Banach_last_equation = thm "Banach_last_equation";
-val decomposition = thm "decomposition";
-val schroeder_bernstein = thm "schroeder_bernstein";
-val bij_imp_eqpoll = thm "bij_imp_eqpoll";
-val eqpoll_refl = thm "eqpoll_refl";
-val eqpoll_sym = thm "eqpoll_sym";
-val eqpoll_trans = thm "eqpoll_trans";
-val subset_imp_lepoll = thm "subset_imp_lepoll";
-val lepoll_refl = thm "lepoll_refl";
-val le_imp_lepoll = thm "le_imp_lepoll";
-val eqpoll_imp_lepoll = thm "eqpoll_imp_lepoll";
-val lepoll_trans = thm "lepoll_trans";
-val eqpollI = thm "eqpollI";
-val eqpollE = thm "eqpollE";
-val eqpoll_iff = thm "eqpoll_iff";
-val lepoll_0_is_0 = thm "lepoll_0_is_0";
-val empty_lepollI = thm "empty_lepollI";
-val lepoll_0_iff = thm "lepoll_0_iff";
-val Un_lepoll_Un = thm "Un_lepoll_Un";
-val eqpoll_0_is_0 = thm "eqpoll_0_is_0";
-val eqpoll_0_iff = thm "eqpoll_0_iff";
-val eqpoll_disjoint_Un = thm "eqpoll_disjoint_Un";
-val lesspoll_not_refl = thm "lesspoll_not_refl";
-val lesspoll_irrefl = thm "lesspoll_irrefl";
-val lesspoll_imp_lepoll = thm "lesspoll_imp_lepoll";
-val lepoll_well_ord = thm "lepoll_well_ord";
-val lepoll_iff_leqpoll = thm "lepoll_iff_leqpoll";
-val inj_not_surj_succ = thm "inj_not_surj_succ";
-val lesspoll_trans = thm "lesspoll_trans";
-val lesspoll_trans1 = thm "lesspoll_trans1";
-val lesspoll_trans2 = thm "lesspoll_trans2";
-val Least_equality = thm "Least_equality";
-val LeastI = thm "LeastI";
-val Least_le = thm "Least_le";
-val less_LeastE = thm "less_LeastE";
-val LeastI2 = thm "LeastI2";
-val Least_0 = thm "Least_0";
-val Ord_Least = thm "Ord_Least";
-val Least_cong = thm "Least_cong";
-val cardinal_cong = thm "cardinal_cong";
-val well_ord_cardinal_eqpoll = thm "well_ord_cardinal_eqpoll";
-val Ord_cardinal_eqpoll = thm "Ord_cardinal_eqpoll";
-val well_ord_cardinal_eqE = thm "well_ord_cardinal_eqE";
-val well_ord_cardinal_eqpoll_iff = thm "well_ord_cardinal_eqpoll_iff";
-val Ord_cardinal_le = thm "Ord_cardinal_le";
-val Card_cardinal_eq = thm "Card_cardinal_eq";
-val CardI = thm "CardI";
-val Card_is_Ord = thm "Card_is_Ord";
-val Card_cardinal_le = thm "Card_cardinal_le";
-val Ord_cardinal = thm "Ord_cardinal";
-val Card_iff_initial = thm "Card_iff_initial";
-val lt_Card_imp_lesspoll = thm "lt_Card_imp_lesspoll";
-val Card_0 = thm "Card_0";
-val Card_Un = thm "Card_Un";
-val Card_cardinal = thm "Card_cardinal";
-val cardinal_mono = thm "cardinal_mono";
-val cardinal_lt_imp_lt = thm "cardinal_lt_imp_lt";
-val Card_lt_imp_lt = thm "Card_lt_imp_lt";
-val Card_lt_iff = thm "Card_lt_iff";
-val Card_le_iff = thm "Card_le_iff";
-val well_ord_lepoll_imp_Card_le = thm "well_ord_lepoll_imp_Card_le";
-val lepoll_cardinal_le = thm "lepoll_cardinal_le";
-val lepoll_Ord_imp_eqpoll = thm "lepoll_Ord_imp_eqpoll";
-val lesspoll_imp_eqpoll = thm "lesspoll_imp_eqpoll";
-val cardinal_subset_Ord = thm "cardinal_subset_Ord";
-val cons_lepoll_consD = thm "cons_lepoll_consD";
-val cons_eqpoll_consD = thm "cons_eqpoll_consD";
-val succ_lepoll_succD = thm "succ_lepoll_succD";
-val nat_lepoll_imp_le = thm "nat_lepoll_imp_le";
-val nat_eqpoll_iff = thm "nat_eqpoll_iff";
-val nat_into_Card = thm "nat_into_Card";
-val cardinal_0 = thm "cardinal_0";
-val cardinal_1 = thm "cardinal_1";
-val succ_lepoll_natE = thm "succ_lepoll_natE";
-val n_lesspoll_nat = thm "n_lesspoll_nat";
-val nat_lepoll_imp_ex_eqpoll_n = thm "nat_lepoll_imp_ex_eqpoll_n";
-val lepoll_imp_lesspoll_succ = thm "lepoll_imp_lesspoll_succ";
-val lesspoll_succ_imp_lepoll = thm "lesspoll_succ_imp_lepoll";
-val lesspoll_succ_iff = thm "lesspoll_succ_iff";
-val lepoll_succ_disj = thm "lepoll_succ_disj";
-val lesspoll_cardinal_lt = thm "lesspoll_cardinal_lt";
-val lt_not_lepoll = thm "lt_not_lepoll";
-val Ord_nat_eqpoll_iff = thm "Ord_nat_eqpoll_iff";
-val Card_nat = thm "Card_nat";
-val nat_le_cardinal = thm "nat_le_cardinal";
-val cons_lepoll_cong = thm "cons_lepoll_cong";
-val cons_eqpoll_cong = thm "cons_eqpoll_cong";
-val cons_lepoll_cons_iff = thm "cons_lepoll_cons_iff";
-val cons_eqpoll_cons_iff = thm "cons_eqpoll_cons_iff";
-val singleton_eqpoll_1 = thm "singleton_eqpoll_1";
-val cardinal_singleton = thm "cardinal_singleton";
-val not_0_is_lepoll_1 = thm "not_0_is_lepoll_1";
-val succ_eqpoll_cong = thm "succ_eqpoll_cong";
-val sum_eqpoll_cong = thm "sum_eqpoll_cong";
-val prod_eqpoll_cong = thm "prod_eqpoll_cong";
-val inj_disjoint_eqpoll = thm "inj_disjoint_eqpoll";
-val Diff_sing_lepoll = thm "Diff_sing_lepoll";
-val lepoll_Diff_sing = thm "lepoll_Diff_sing";
-val Diff_sing_eqpoll = thm "Diff_sing_eqpoll";
-val lepoll_1_is_sing = thm "lepoll_1_is_sing";
-val Un_lepoll_sum = thm "Un_lepoll_sum";
-val well_ord_Un = thm "well_ord_Un";
-val disj_Un_eqpoll_sum = thm "disj_Un_eqpoll_sum";
-val Finite_0 = thm "Finite_0";
-val lepoll_nat_imp_Finite = thm "lepoll_nat_imp_Finite";
-val lesspoll_nat_is_Finite = thm "lesspoll_nat_is_Finite";
-val lepoll_Finite = thm "lepoll_Finite";
-val subset_Finite = thm "subset_Finite";
-val Finite_Diff = thm "Finite_Diff";
-val Finite_cons = thm "Finite_cons";
-val Finite_succ = thm "Finite_succ";
-val nat_le_infinite_Ord = thm "nat_le_infinite_Ord";
-val Finite_imp_well_ord = thm "Finite_imp_well_ord";
-val nat_wf_on_converse_Memrel = thm "nat_wf_on_converse_Memrel";
-val nat_well_ord_converse_Memrel = thm "nat_well_ord_converse_Memrel";
-val well_ord_converse = thm "well_ord_converse";
-val ordertype_eq_n = thm "ordertype_eq_n";
-val Finite_well_ord_converse = thm "Finite_well_ord_converse";
-val nat_into_Finite = thm "nat_into_Finite";
+val Least_def = @{thm Least_def};
+val eqpoll_def = @{thm eqpoll_def};
+val lepoll_def = @{thm lepoll_def};
+val lesspoll_def = @{thm lesspoll_def};
+val cardinal_def = @{thm cardinal_def};
+val Finite_def = @{thm Finite_def};
+val Card_def = @{thm Card_def};
+val eq_imp_not_mem = @{thm eq_imp_not_mem};
+val decomp_bnd_mono = @{thm decomp_bnd_mono};
+val Banach_last_equation = @{thm Banach_last_equation};
+val decomposition = @{thm decomposition};
+val schroeder_bernstein = @{thm schroeder_bernstein};
+val bij_imp_eqpoll = @{thm bij_imp_eqpoll};
+val eqpoll_refl = @{thm eqpoll_refl};
+val eqpoll_sym = @{thm eqpoll_sym};
+val eqpoll_trans = @{thm eqpoll_trans};
+val subset_imp_lepoll = @{thm subset_imp_lepoll};
+val lepoll_refl = @{thm lepoll_refl};
+val le_imp_lepoll = @{thm le_imp_lepoll};
+val eqpoll_imp_lepoll = @{thm eqpoll_imp_lepoll};
+val lepoll_trans = @{thm lepoll_trans};
+val eqpollI = @{thm eqpollI};
+val eqpollE = @{thm eqpollE};
+val eqpoll_iff = @{thm eqpoll_iff};
+val lepoll_0_is_0 = @{thm lepoll_0_is_0};
+val empty_lepollI = @{thm empty_lepollI};
+val lepoll_0_iff = @{thm lepoll_0_iff};
+val Un_lepoll_Un = @{thm Un_lepoll_Un};
+val eqpoll_0_is_0 = @{thm eqpoll_0_is_0};
+val eqpoll_0_iff = @{thm eqpoll_0_iff};
+val eqpoll_disjoint_Un = @{thm eqpoll_disjoint_Un};
+val lesspoll_not_refl = @{thm lesspoll_not_refl};
+val lesspoll_irrefl = @{thm lesspoll_irrefl};
+val lesspoll_imp_lepoll = @{thm lesspoll_imp_lepoll};
+val lepoll_well_ord = @{thm lepoll_well_ord};
+val lepoll_iff_leqpoll = @{thm lepoll_iff_leqpoll};
+val inj_not_surj_succ = @{thm inj_not_surj_succ};
+val lesspoll_trans = @{thm lesspoll_trans};
+val lesspoll_trans1 = @{thm lesspoll_trans1};
+val lesspoll_trans2 = @{thm lesspoll_trans2};
+val Least_equality = @{thm Least_equality};
+val LeastI = @{thm LeastI};
+val Least_le = @{thm Least_le};
+val less_LeastE = @{thm less_LeastE};
+val LeastI2 = @{thm LeastI2};
+val Least_0 = @{thm Least_0};
+val Ord_Least = @{thm Ord_Least};
+val Least_cong = @{thm Least_cong};
+val cardinal_cong = @{thm cardinal_cong};
+val well_ord_cardinal_eqpoll = @{thm well_ord_cardinal_eqpoll};
+val Ord_cardinal_eqpoll = @{thm Ord_cardinal_eqpoll};
+val well_ord_cardinal_eqE = @{thm well_ord_cardinal_eqE};
+val well_ord_cardinal_eqpoll_iff = @{thm well_ord_cardinal_eqpoll_iff};
+val Ord_cardinal_le = @{thm Ord_cardinal_le};
+val Card_cardinal_eq = @{thm Card_cardinal_eq};
+val CardI = @{thm CardI};
+val Card_is_Ord = @{thm Card_is_Ord};
+val Card_cardinal_le = @{thm Card_cardinal_le};
+val Ord_cardinal = @{thm Ord_cardinal};
+val Card_iff_initial = @{thm Card_iff_initial};
+val lt_Card_imp_lesspoll = @{thm lt_Card_imp_lesspoll};
+val Card_0 = @{thm Card_0};
+val Card_Un = @{thm Card_Un};
+val Card_cardinal = @{thm Card_cardinal};
+val cardinal_mono = @{thm cardinal_mono};
+val cardinal_lt_imp_lt = @{thm cardinal_lt_imp_lt};
+val Card_lt_imp_lt = @{thm Card_lt_imp_lt};
+val Card_lt_iff = @{thm Card_lt_iff};
+val Card_le_iff = @{thm Card_le_iff};
+val well_ord_lepoll_imp_Card_le = @{thm well_ord_lepoll_imp_Card_le};
+val lepoll_cardinal_le = @{thm lepoll_cardinal_le};
+val lepoll_Ord_imp_eqpoll = @{thm lepoll_Ord_imp_eqpoll};
+val lesspoll_imp_eqpoll = @{thm lesspoll_imp_eqpoll};
+val cardinal_subset_Ord = @{thm cardinal_subset_Ord};
+val cons_lepoll_consD = @{thm cons_lepoll_consD};
+val cons_eqpoll_consD = @{thm cons_eqpoll_consD};
+val succ_lepoll_succD = @{thm succ_lepoll_succD};
+val nat_lepoll_imp_le = @{thm nat_lepoll_imp_le};
+val nat_eqpoll_iff = @{thm nat_eqpoll_iff};
+val nat_into_Card = @{thm nat_into_Card};
+val cardinal_0 = @{thm cardinal_0};
+val cardinal_1 = @{thm cardinal_1};
+val succ_lepoll_natE = @{thm succ_lepoll_natE};
+val n_lesspoll_nat = @{thm n_lesspoll_nat};
+val nat_lepoll_imp_ex_eqpoll_n = @{thm nat_lepoll_imp_ex_eqpoll_n};
+val lepoll_imp_lesspoll_succ = @{thm lepoll_imp_lesspoll_succ};
+val lesspoll_succ_imp_lepoll = @{thm lesspoll_succ_imp_lepoll};
+val lesspoll_succ_iff = @{thm lesspoll_succ_iff};
+val lepoll_succ_disj = @{thm lepoll_succ_disj};
+val lesspoll_cardinal_lt = @{thm lesspoll_cardinal_lt};
+val lt_not_lepoll = @{thm lt_not_lepoll};
+val Ord_nat_eqpoll_iff = @{thm Ord_nat_eqpoll_iff};
+val Card_nat = @{thm Card_nat};
+val nat_le_cardinal = @{thm nat_le_cardinal};
+val cons_lepoll_cong = @{thm cons_lepoll_cong};
+val cons_eqpoll_cong = @{thm cons_eqpoll_cong};
+val cons_lepoll_cons_iff = @{thm cons_lepoll_cons_iff};
+val cons_eqpoll_cons_iff = @{thm cons_eqpoll_cons_iff};
+val singleton_eqpoll_1 = @{thm singleton_eqpoll_1};
+val cardinal_singleton = @{thm cardinal_singleton};
+val not_0_is_lepoll_1 = @{thm not_0_is_lepoll_1};
+val succ_eqpoll_cong = @{thm succ_eqpoll_cong};
+val sum_eqpoll_cong = @{thm sum_eqpoll_cong};
+val prod_eqpoll_cong = @{thm prod_eqpoll_cong};
+val inj_disjoint_eqpoll = @{thm inj_disjoint_eqpoll};
+val Diff_sing_lepoll = @{thm Diff_sing_lepoll};
+val lepoll_Diff_sing = @{thm lepoll_Diff_sing};
+val Diff_sing_eqpoll = @{thm Diff_sing_eqpoll};
+val lepoll_1_is_sing = @{thm lepoll_1_is_sing};
+val Un_lepoll_sum = @{thm Un_lepoll_sum};
+val well_ord_Un = @{thm well_ord_Un};
+val disj_Un_eqpoll_sum = @{thm disj_Un_eqpoll_sum};
+val Finite_0 = @{thm Finite_0};
+val lepoll_nat_imp_Finite = @{thm lepoll_nat_imp_Finite};
+val lesspoll_nat_is_Finite = @{thm lesspoll_nat_is_Finite};
+val lepoll_Finite = @{thm lepoll_Finite};
+val subset_Finite = @{thm subset_Finite};
+val Finite_Diff = @{thm Finite_Diff};
+val Finite_cons = @{thm Finite_cons};
+val Finite_succ = @{thm Finite_succ};
+val nat_le_infinite_Ord = @{thm nat_le_infinite_Ord};
+val Finite_imp_well_ord = @{thm Finite_imp_well_ord};
+val nat_wf_on_converse_Memrel = @{thm nat_wf_on_converse_Memrel};
+val nat_well_ord_converse_Memrel = @{thm nat_well_ord_converse_Memrel};
+val well_ord_converse = @{thm well_ord_converse};
+val ordertype_eq_n = @{thm ordertype_eq_n};
+val Finite_well_ord_converse = @{thm Finite_well_ord_converse};
+val nat_into_Finite = @{thm nat_into_Finite};
*}
end
--- a/src/ZF/CardinalArith.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/ZF/CardinalArith.thy Mon Sep 06 19:13:10 2010 +0200
@@ -911,89 +911,89 @@
ML{*
-val InfCard_def = thm "InfCard_def"
-val cmult_def = thm "cmult_def"
-val cadd_def = thm "cadd_def"
-val jump_cardinal_def = thm "jump_cardinal_def"
-val csucc_def = thm "csucc_def"
+val InfCard_def = @{thm InfCard_def};
+val cmult_def = @{thm cmult_def};
+val cadd_def = @{thm cadd_def};
+val jump_cardinal_def = @{thm jump_cardinal_def};
+val csucc_def = @{thm csucc_def};
-val sum_commute_eqpoll = thm "sum_commute_eqpoll";
-val cadd_commute = thm "cadd_commute";
-val sum_assoc_eqpoll = thm "sum_assoc_eqpoll";
-val well_ord_cadd_assoc = thm "well_ord_cadd_assoc";
-val sum_0_eqpoll = thm "sum_0_eqpoll";
-val cadd_0 = thm "cadd_0";
-val sum_lepoll_self = thm "sum_lepoll_self";
-val cadd_le_self = thm "cadd_le_self";
-val sum_lepoll_mono = thm "sum_lepoll_mono";
-val cadd_le_mono = thm "cadd_le_mono";
-val eq_imp_not_mem = thm "eq_imp_not_mem";
-val sum_succ_eqpoll = thm "sum_succ_eqpoll";
-val nat_cadd_eq_add = thm "nat_cadd_eq_add";
-val prod_commute_eqpoll = thm "prod_commute_eqpoll";
-val cmult_commute = thm "cmult_commute";
-val prod_assoc_eqpoll = thm "prod_assoc_eqpoll";
-val well_ord_cmult_assoc = thm "well_ord_cmult_assoc";
-val sum_prod_distrib_eqpoll = thm "sum_prod_distrib_eqpoll";
-val well_ord_cadd_cmult_distrib = thm "well_ord_cadd_cmult_distrib";
-val prod_0_eqpoll = thm "prod_0_eqpoll";
-val cmult_0 = thm "cmult_0";
-val prod_singleton_eqpoll = thm "prod_singleton_eqpoll";
-val cmult_1 = thm "cmult_1";
-val prod_lepoll_self = thm "prod_lepoll_self";
-val cmult_le_self = thm "cmult_le_self";
-val prod_lepoll_mono = thm "prod_lepoll_mono";
-val cmult_le_mono = thm "cmult_le_mono";
-val prod_succ_eqpoll = thm "prod_succ_eqpoll";
-val nat_cmult_eq_mult = thm "nat_cmult_eq_mult";
-val cmult_2 = thm "cmult_2";
-val sum_lepoll_prod = thm "sum_lepoll_prod";
-val lepoll_imp_sum_lepoll_prod = thm "lepoll_imp_sum_lepoll_prod";
-val nat_cons_lepoll = thm "nat_cons_lepoll";
-val nat_cons_eqpoll = thm "nat_cons_eqpoll";
-val nat_succ_eqpoll = thm "nat_succ_eqpoll";
-val InfCard_nat = thm "InfCard_nat";
-val InfCard_is_Card = thm "InfCard_is_Card";
-val InfCard_Un = thm "InfCard_Un";
-val InfCard_is_Limit = thm "InfCard_is_Limit";
-val ordermap_eqpoll_pred = thm "ordermap_eqpoll_pred";
-val ordermap_z_lt = thm "ordermap_z_lt";
-val InfCard_le_cmult_eq = thm "InfCard_le_cmult_eq";
-val InfCard_cmult_eq = thm "InfCard_cmult_eq";
-val InfCard_cdouble_eq = thm "InfCard_cdouble_eq";
-val InfCard_le_cadd_eq = thm "InfCard_le_cadd_eq";
-val InfCard_cadd_eq = thm "InfCard_cadd_eq";
-val Ord_jump_cardinal = thm "Ord_jump_cardinal";
-val jump_cardinal_iff = thm "jump_cardinal_iff";
-val K_lt_jump_cardinal = thm "K_lt_jump_cardinal";
-val Card_jump_cardinal = thm "Card_jump_cardinal";
-val csucc_basic = thm "csucc_basic";
-val Card_csucc = thm "Card_csucc";
-val lt_csucc = thm "lt_csucc";
-val Ord_0_lt_csucc = thm "Ord_0_lt_csucc";
-val csucc_le = thm "csucc_le";
-val lt_csucc_iff = thm "lt_csucc_iff";
-val Card_lt_csucc_iff = thm "Card_lt_csucc_iff";
-val InfCard_csucc = thm "InfCard_csucc";
-val Finite_into_Fin = thm "Finite_into_Fin";
-val Fin_into_Finite = thm "Fin_into_Finite";
-val Finite_Fin_iff = thm "Finite_Fin_iff";
-val Finite_Un = thm "Finite_Un";
-val Finite_Union = thm "Finite_Union";
-val Finite_induct = thm "Finite_induct";
-val Fin_imp_not_cons_lepoll = thm "Fin_imp_not_cons_lepoll";
-val Finite_imp_cardinal_cons = thm "Finite_imp_cardinal_cons";
-val Finite_imp_succ_cardinal_Diff = thm "Finite_imp_succ_cardinal_Diff";
-val Finite_imp_cardinal_Diff = thm "Finite_imp_cardinal_Diff";
-val nat_implies_well_ord = thm "nat_implies_well_ord";
-val nat_sum_eqpoll_sum = thm "nat_sum_eqpoll_sum";
-val Diff_sing_Finite = thm "Diff_sing_Finite";
-val Diff_Finite = thm "Diff_Finite";
-val Ord_subset_natD = thm "Ord_subset_natD";
-val Ord_nat_subset_into_Card = thm "Ord_nat_subset_into_Card";
-val Finite_cardinal_in_nat = thm "Finite_cardinal_in_nat";
-val Finite_Diff_sing_eq_diff_1 = thm "Finite_Diff_sing_eq_diff_1";
-val cardinal_lt_imp_Diff_not_0 = thm "cardinal_lt_imp_Diff_not_0";
+val sum_commute_eqpoll = @{thm sum_commute_eqpoll};
+val cadd_commute = @{thm cadd_commute};
+val sum_assoc_eqpoll = @{thm sum_assoc_eqpoll};
+val well_ord_cadd_assoc = @{thm well_ord_cadd_assoc};
+val sum_0_eqpoll = @{thm sum_0_eqpoll};
+val cadd_0 = @{thm cadd_0};
+val sum_lepoll_self = @{thm sum_lepoll_self};
+val cadd_le_self = @{thm cadd_le_self};
+val sum_lepoll_mono = @{thm sum_lepoll_mono};
+val cadd_le_mono = @{thm cadd_le_mono};
+val eq_imp_not_mem = @{thm eq_imp_not_mem};
+val sum_succ_eqpoll = @{thm sum_succ_eqpoll};
+val nat_cadd_eq_add = @{thm nat_cadd_eq_add};
+val prod_commute_eqpoll = @{thm prod_commute_eqpoll};
+val cmult_commute = @{thm cmult_commute};
+val prod_assoc_eqpoll = @{thm prod_assoc_eqpoll};
+val well_ord_cmult_assoc = @{thm well_ord_cmult_assoc};
+val sum_prod_distrib_eqpoll = @{thm sum_prod_distrib_eqpoll};
+val well_ord_cadd_cmult_distrib = @{thm well_ord_cadd_cmult_distrib};
+val prod_0_eqpoll = @{thm prod_0_eqpoll};
+val cmult_0 = @{thm cmult_0};
+val prod_singleton_eqpoll = @{thm prod_singleton_eqpoll};
+val cmult_1 = @{thm cmult_1};
+val prod_lepoll_self = @{thm prod_lepoll_self};
+val cmult_le_self = @{thm cmult_le_self};
+val prod_lepoll_mono = @{thm prod_lepoll_mono};
+val cmult_le_mono = @{thm cmult_le_mono};
+val prod_succ_eqpoll = @{thm prod_succ_eqpoll};
+val nat_cmult_eq_mult = @{thm nat_cmult_eq_mult};
+val cmult_2 = @{thm cmult_2};
+val sum_lepoll_prod = @{thm sum_lepoll_prod};
+val lepoll_imp_sum_lepoll_prod = @{thm lepoll_imp_sum_lepoll_prod};
+val nat_cons_lepoll = @{thm nat_cons_lepoll};
+val nat_cons_eqpoll = @{thm nat_cons_eqpoll};
+val nat_succ_eqpoll = @{thm nat_succ_eqpoll};
+val InfCard_nat = @{thm InfCard_nat};
+val InfCard_is_Card = @{thm InfCard_is_Card};
+val InfCard_Un = @{thm InfCard_Un};
+val InfCard_is_Limit = @{thm InfCard_is_Limit};
+val ordermap_eqpoll_pred = @{thm ordermap_eqpoll_pred};
+val ordermap_z_lt = @{thm ordermap_z_lt};
+val InfCard_le_cmult_eq = @{thm InfCard_le_cmult_eq};
+val InfCard_cmult_eq = @{thm InfCard_cmult_eq};
+val InfCard_cdouble_eq = @{thm InfCard_cdouble_eq};
+val InfCard_le_cadd_eq = @{thm InfCard_le_cadd_eq};
+val InfCard_cadd_eq = @{thm InfCard_cadd_eq};
+val Ord_jump_cardinal = @{thm Ord_jump_cardinal};
+val jump_cardinal_iff = @{thm jump_cardinal_iff};
+val K_lt_jump_cardinal = @{thm K_lt_jump_cardinal};
+val Card_jump_cardinal = @{thm Card_jump_cardinal};
+val csucc_basic = @{thm csucc_basic};
+val Card_csucc = @{thm Card_csucc};
+val lt_csucc = @{thm lt_csucc};
+val Ord_0_lt_csucc = @{thm Ord_0_lt_csucc};
+val csucc_le = @{thm csucc_le};
+val lt_csucc_iff = @{thm lt_csucc_iff};
+val Card_lt_csucc_iff = @{thm Card_lt_csucc_iff};
+val InfCard_csucc = @{thm InfCard_csucc};
+val Finite_into_Fin = @{thm Finite_into_Fin};
+val Fin_into_Finite = @{thm Fin_into_Finite};
+val Finite_Fin_iff = @{thm Finite_Fin_iff};
+val Finite_Un = @{thm Finite_Un};
+val Finite_Union = @{thm Finite_Union};
+val Finite_induct = @{thm Finite_induct};
+val Fin_imp_not_cons_lepoll = @{thm Fin_imp_not_cons_lepoll};
+val Finite_imp_cardinal_cons = @{thm Finite_imp_cardinal_cons};
+val Finite_imp_succ_cardinal_Diff = @{thm Finite_imp_succ_cardinal_Diff};
+val Finite_imp_cardinal_Diff = @{thm Finite_imp_cardinal_Diff};
+val nat_implies_well_ord = @{thm nat_implies_well_ord};
+val nat_sum_eqpoll_sum = @{thm nat_sum_eqpoll_sum};
+val Diff_sing_Finite = @{thm Diff_sing_Finite};
+val Diff_Finite = @{thm Diff_Finite};
+val Ord_subset_natD = @{thm Ord_subset_natD};
+val Ord_nat_subset_into_Card = @{thm Ord_nat_subset_into_Card};
+val Finite_cardinal_in_nat = @{thm Finite_cardinal_in_nat};
+val Finite_Diff_sing_eq_diff_1 = @{thm Finite_Diff_sing_eq_diff_1};
+val cardinal_lt_imp_Diff_not_0 = @{thm cardinal_lt_imp_Diff_not_0};
*}
end
--- a/src/ZF/Cardinal_AC.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/ZF/Cardinal_AC.thy Mon Sep 06 19:13:10 2010 +0200
@@ -193,8 +193,8 @@
ML
{*
-val cardinal_0_iff_0 = thm "cardinal_0_iff_0";
-val cardinal_lt_iff_lesspoll = thm "cardinal_lt_iff_lesspoll";
+val cardinal_0_iff_0 = @{thm cardinal_0_iff_0};
+val cardinal_lt_iff_lesspoll = @{thm cardinal_lt_iff_lesspoll};
*}
end
--- a/src/ZF/Epsilon.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/ZF/Epsilon.thy Mon Sep 06 19:13:10 2010 +0200
@@ -398,56 +398,56 @@
ML
{*
-val arg_subset_eclose = thm "arg_subset_eclose";
-val arg_into_eclose = thm "arg_into_eclose";
-val Transset_eclose = thm "Transset_eclose";
-val eclose_subset = thm "eclose_subset";
-val ecloseD = thm "ecloseD";
-val arg_in_eclose_sing = thm "arg_in_eclose_sing";
-val arg_into_eclose_sing = thm "arg_into_eclose_sing";
-val eclose_induct = thm "eclose_induct";
-val eps_induct = thm "eps_induct";
-val eclose_least = thm "eclose_least";
-val eclose_induct_down = thm "eclose_induct_down";
-val Transset_eclose_eq_arg = thm "Transset_eclose_eq_arg";
-val mem_eclose_trans = thm "mem_eclose_trans";
-val mem_eclose_sing_trans = thm "mem_eclose_sing_trans";
-val under_Memrel = thm "under_Memrel";
-val under_Memrel_eclose = thm "under_Memrel_eclose";
-val wfrec_ssubst = thm "wfrec_ssubst";
-val wfrec_eclose_eq = thm "wfrec_eclose_eq";
-val wfrec_eclose_eq2 = thm "wfrec_eclose_eq2";
-val transrec = thm "transrec";
-val def_transrec = thm "def_transrec";
-val transrec_type = thm "transrec_type";
-val eclose_sing_Ord = thm "eclose_sing_Ord";
-val Ord_transrec_type = thm "Ord_transrec_type";
-val rank = thm "rank";
-val Ord_rank = thm "Ord_rank";
-val rank_of_Ord = thm "rank_of_Ord";
-val rank_lt = thm "rank_lt";
-val eclose_rank_lt = thm "eclose_rank_lt";
-val rank_mono = thm "rank_mono";
-val rank_Pow = thm "rank_Pow";
-val rank_0 = thm "rank_0";
-val rank_succ = thm "rank_succ";
-val rank_Union = thm "rank_Union";
-val rank_eclose = thm "rank_eclose";
-val rank_pair1 = thm "rank_pair1";
-val rank_pair2 = thm "rank_pair2";
-val the_equality_if = thm "the_equality_if";
-val rank_apply = thm "rank_apply";
-val mem_eclose_subset = thm "mem_eclose_subset";
-val eclose_mono = thm "eclose_mono";
-val eclose_idem = thm "eclose_idem";
-val transrec2_0 = thm "transrec2_0";
-val transrec2_succ = thm "transrec2_succ";
-val transrec2_Limit = thm "transrec2_Limit";
-val recursor_0 = thm "recursor_0";
-val recursor_succ = thm "recursor_succ";
-val rec_0 = thm "rec_0";
-val rec_succ = thm "rec_succ";
-val rec_type = thm "rec_type";
+val arg_subset_eclose = @{thm arg_subset_eclose};
+val arg_into_eclose = @{thm arg_into_eclose};
+val Transset_eclose = @{thm Transset_eclose};
+val eclose_subset = @{thm eclose_subset};
+val ecloseD = @{thm ecloseD};
+val arg_in_eclose_sing = @{thm arg_in_eclose_sing};
+val arg_into_eclose_sing = @{thm arg_into_eclose_sing};
+val eclose_induct = @{thm eclose_induct};
+val eps_induct = @{thm eps_induct};
+val eclose_least = @{thm eclose_least};
+val eclose_induct_down = @{thm eclose_induct_down};
+val Transset_eclose_eq_arg = @{thm Transset_eclose_eq_arg};
+val mem_eclose_trans = @{thm mem_eclose_trans};
+val mem_eclose_sing_trans = @{thm mem_eclose_sing_trans};
+val under_Memrel = @{thm under_Memrel};
+val under_Memrel_eclose = @{thm under_Memrel_eclose};
+val wfrec_ssubst = @{thm wfrec_ssubst};
+val wfrec_eclose_eq = @{thm wfrec_eclose_eq};
+val wfrec_eclose_eq2 = @{thm wfrec_eclose_eq2};
+val transrec = @{thm transrec};
+val def_transrec = @{thm def_transrec};
+val transrec_type = @{thm transrec_type};
+val eclose_sing_Ord = @{thm eclose_sing_Ord};
+val Ord_transrec_type = @{thm Ord_transrec_type};
+val rank = @{thm rank};
+val Ord_rank = @{thm Ord_rank};
+val rank_of_Ord = @{thm rank_of_Ord};
+val rank_lt = @{thm rank_lt};
+val eclose_rank_lt = @{thm eclose_rank_lt};
+val rank_mono = @{thm rank_mono};
+val rank_Pow = @{thm rank_Pow};
+val rank_0 = @{thm rank_0};
+val rank_succ = @{thm rank_succ};
+val rank_Union = @{thm rank_Union};
+val rank_eclose = @{thm rank_eclose};
+val rank_pair1 = @{thm rank_pair1};
+val rank_pair2 = @{thm rank_pair2};
+val the_equality_if = @{thm the_equality_if};
+val rank_apply = @{thm rank_apply};
+val mem_eclose_subset = @{thm mem_eclose_subset};
+val eclose_mono = @{thm eclose_mono};
+val eclose_idem = @{thm eclose_idem};
+val transrec2_0 = @{thm transrec2_0};
+val transrec2_succ = @{thm transrec2_succ};
+val transrec2_Limit = @{thm transrec2_Limit};
+val recursor_0 = @{thm recursor_0};
+val recursor_succ = @{thm recursor_succ};
+val rec_0 = @{thm rec_0};
+val rec_succ = @{thm rec_succ};
+val rec_type = @{thm rec_type};
*}
end