--- a/src/Sequents/LK/Hard_Quantifiers.thy Wed May 09 19:37:20 2007 +0200
+++ b/src/Sequents/LK/Hard_Quantifiers.thy Wed May 09 19:37:21 2007 +0200
@@ -216,7 +216,7 @@
text "Problem 48"
lemma "|- (a=b | c=d) & (a=c | b=d) --> a=d | b=c"
- by (tactic {* fast_tac (LK_pack add_safes [thm "subst"]) 1 *})
+ by (tactic {* fast_tac (LK_pack add_safes @{thms subst}) 1 *})
text "Problem 50"
lemma "|- (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))"
@@ -225,16 +225,16 @@
text "Problem 51"
lemma "|- (EX z w. ALL x y. P(x,y) <-> (x=z & y=w)) -->
(EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)"
- by (tactic {* fast_tac (LK_pack add_safes [thm "subst"]) 1 *})
+ by (tactic {* fast_tac (LK_pack add_safes @{thms subst}) 1 *})
text "Problem 52" (*Almost the same as 51. *)
lemma "|- (EX z w. ALL x y. P(x,y) <-> (x=z & y=w)) -->
(EX w. ALL y. EX z. (ALL x. P(x,y) <-> x=z) <-> y=w)"
- by (tactic {* fast_tac (LK_pack add_safes [thm "subst"]) 1 *})
+ by (tactic {* fast_tac (LK_pack add_safes @{thms subst}) 1 *})
text "Problem 56"
lemma "|- (ALL x.(EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"
- by (tactic {* best_tac (LK_pack add_unsafes [thm "symL", thm "subst"]) 1 *})
+ by (tactic {* best_tac (LK_pack add_unsafes [@{thm symL}, @{thm subst}]) 1 *})
(*requires tricker to orient the equality properly*)
text "Problem 57"
@@ -244,7 +244,7 @@
text "Problem 58!"
lemma "|- (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))"
- by (tactic {* fast_tac (LK_pack add_safes [thm "subst"]) 1 *})
+ by (tactic {* fast_tac (LK_pack add_safes @{thms subst}) 1 *})
text "Problem 59"
(*Unification works poorly here -- the abstraction %sobj prevents efficient
--- a/src/Sequents/LK/Nat.thy Wed May 09 19:37:20 2007 +0200
+++ b/src/Sequents/LK/Nat.thy Wed May 09 19:37:21 2007 +0200
@@ -15,7 +15,7 @@
consts "0" :: nat ("0")
Suc :: "nat=>nat"
rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
- "+" :: "[nat, nat] => nat" (infixl 60)
+ add :: "[nat, nat] => nat" (infixl "+" 60)
axioms
induct: "[| $H |- $E, P(0), $F;
@@ -35,8 +35,8 @@
lemma Suc_n_not_n: "|- Suc(k) ~= k"
apply (rule_tac n = k in induct)
- apply (tactic {* simp_tac (LK_ss addsimps [thm "Suc_neq_0"]) 1 *})
- apply (tactic {* fast_tac (LK_pack add_safes [thm "Suc_inject_rule"]) 1 *})
+ apply (tactic {* simp_tac (LK_ss addsimps @{thms Suc_neq_0}) 1 *})
+ apply (tactic {* fast_tac (LK_pack add_safes @{thms Suc_inject_rule}) 1 *})
done
lemma add_0: "|- 0+n = n"
@@ -53,26 +53,26 @@
lemma add_assoc: "|- (k+m)+n = k+(m+n)"
apply (rule_tac n = "k" in induct)
- apply (tactic {* simp_tac (LK_ss addsimps [thm "add_0"]) 1 *})
- apply (tactic {* simp_tac (LK_ss addsimps [thm "add_Suc"]) 1 *})
+ apply (tactic {* simp_tac (LK_ss addsimps @{thms add_0}) 1 *})
+ apply (tactic {* simp_tac (LK_ss addsimps @{thms add_Suc}) 1 *})
done
lemma add_0_right: "|- m+0 = m"
apply (rule_tac n = "m" in induct)
- apply (tactic {* simp_tac (LK_ss addsimps [thm "add_0"]) 1 *})
- apply (tactic {* simp_tac (LK_ss addsimps [thm "add_Suc"]) 1 *})
+ apply (tactic {* simp_tac (LK_ss addsimps @{thms add_0}) 1 *})
+ apply (tactic {* simp_tac (LK_ss addsimps @{thms add_Suc}) 1 *})
done
lemma add_Suc_right: "|- m+Suc(n) = Suc(m+n)"
apply (rule_tac n = "m" in induct)
- apply (tactic {* simp_tac (LK_ss addsimps [thm "add_0"]) 1 *})
- apply (tactic {* simp_tac (LK_ss addsimps [thm "add_Suc"]) 1 *})
+ apply (tactic {* simp_tac (LK_ss addsimps @{thms add_0}) 1 *})
+ apply (tactic {* simp_tac (LK_ss addsimps @{thms add_Suc}) 1 *})
done
lemma "(!!n. |- f(Suc(n)) = Suc(f(n))) ==> |- f(i+j) = i+f(j)"
apply (rule_tac n = "i" in induct)
- apply (tactic {* simp_tac (LK_ss addsimps [thm "add_0"]) 1 *})
- apply (tactic {* asm_simp_tac (LK_ss addsimps [thm "add_Suc"]) 1 *})
+ apply (tactic {* simp_tac (LK_ss addsimps @{thms add_0}) 1 *})
+ apply (tactic {* asm_simp_tac (LK_ss addsimps @{thms add_Suc}) 1 *})
done
end
--- a/src/Sequents/simpdata.ML Wed May 09 19:37:20 2007 +0200
+++ b/src/Sequents/simpdata.ML Wed May 09 19:37:21 2007 +0200
@@ -10,16 +10,11 @@
(*** Rewrite rules ***)
-local
- val subst = thm "subst"
-in
-
fun prove_fun s =
(writeln s;
prove_goal (the_context ()) s
(fn prems => [ (cut_facts_tac prems 1),
- (fast_tac (LK_pack add_safes [subst]) 1) ]));
-end;
+ (fast_tac (LK_pack add_safes @{thms subst}) 1) ]));
val conj_simps = map prove_fun
["|- P & True <-> P", "|- True & P <-> P",
@@ -88,12 +83,6 @@
(** Conversion into rewrite rules **)
-local
- val mp_R = thm "mp_R";
- val conjunct1 = thm "conjunct1";
- val conjunct2 = thm "conjunct2";
- val spec = thm "spec";
-in
(*Make atomic rewrite rules*)
fun atomize r =
case concl_of r of
@@ -101,35 +90,30 @@
(case (forms_of_seq a, forms_of_seq c) of
([], [p]) =>
(case p of
- Const("op -->",_)$_$_ => atomize(r RS mp_R)
- | Const("op &",_)$_$_ => atomize(r RS conjunct1) @
- atomize(r RS conjunct2)
- | Const("All",_)$_ => atomize(r RS spec)
+ Const("imp",_)$_$_ => atomize(r RS @{thm mp_R})
+ | Const("conj",_)$_$_ => atomize(r RS @{thm conjunct1}) @
+ atomize(r RS @{thm conjunct2})
+ | Const("All",_)$_ => atomize(r RS @{thm spec})
| Const("True",_) => [] (*True is DELETED*)
| Const("False",_) => [] (*should False do something?*)
| _ => [r])
| _ => []) (*ignore theorem unless it has precisely one conclusion*)
| _ => [r];
-end;
Goal "|- ~P ==> |- (P <-> False)";
-by (etac (thm "thinR" RS (thm "cut")) 1);
+by (etac (@{thm thinR} RS @{thm cut}) 1);
by (fast_tac LK_pack 1);
qed "P_iff_F";
-bind_thm ("iff_reflection_F", thm "P_iff_F" RS thm "iff_reflection");
+bind_thm ("iff_reflection_F", P_iff_F RS @{thm iff_reflection});
Goal "|- P ==> |- (P <-> True)";
-by (etac (thm "thinR" RS (thm "cut")) 1);
+by (etac (@{thm thinR} RS @{thm cut}) 1);
by (fast_tac LK_pack 1);
qed "P_iff_T";
-bind_thm ("iff_reflection_T", thm "P_iff_T" RS thm "iff_reflection");
+bind_thm ("iff_reflection_T", P_iff_T RS @{thm iff_reflection});
-local
- val eq_reflection = thm "eq_reflection"
- val iff_reflection = thm "iff_reflection"
-in
(*Make meta-equalities.*)
fun mk_meta_eq th = case concl_of th of
Const("==",_)$_$_ => th
@@ -137,18 +121,17 @@
(case (forms_of_seq a, forms_of_seq c) of
([], [p]) =>
(case p of
- (Const("op =",_)$_$_) => th RS eq_reflection
- | (Const("op <->",_)$_$_) => th RS iff_reflection
+ (Const("equal",_)$_$_) => th RS @{thm eq_reflection}
+ | (Const("iff",_)$_$_) => th RS @{thm iff_reflection}
| (Const("Not",_)$_) => th RS iff_reflection_F
| _ => th RS iff_reflection_T)
| _ => error ("addsimps: unable to use theorem\n" ^
string_of_thm th));
-end;
(*Replace premises x=y, X<->Y by X==Y*)
val mk_meta_prems =
rule_by_tactic
- (REPEAT_FIRST (resolve_tac [thm "meta_eq_to_obj_eq", thm "def_imp_iff"]));
+ (REPEAT_FIRST (resolve_tac [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}]));
(*Congruence rules for = or <-> (instead of ==)*)
fun mk_meta_cong rl =
@@ -194,9 +177,9 @@
"[| |- P <-> P'; |- P' ==> |- Q <-> Q' |] ==> |- (P-->Q) <-> (P'-->Q')";
by (lemma_tac p1 1);
by (safe_tac LK_pack 1);
-by (REPEAT (rtac (thm "cut") 1
+by (REPEAT (rtac @{thm cut} 1
THEN
- DEPTH_SOLVE_1 (resolve_tac [thm "thinL", thm "thinR", p2 COMP thm "monotonic"] 1)
+ DEPTH_SOLVE_1 (resolve_tac [@{thm thinL}, @{thm thinR}, p2 COMP @{thm monotonic}] 1)
THEN
safe_tac LK_pack 1));
qed "imp_cong";
@@ -205,15 +188,15 @@
"[| |- P <-> P'; |- P' ==> |- Q <-> Q' |] ==> |- (P&Q) <-> (P'&Q')";
by (lemma_tac p1 1);
by (safe_tac LK_pack 1);
-by (REPEAT (rtac (thm "cut") 1
+by (REPEAT (rtac @{thm cut} 1
THEN
- DEPTH_SOLVE_1 (resolve_tac [thm "thinL", thm "thinR", p2 COMP thm "monotonic"] 1)
+ DEPTH_SOLVE_1 (resolve_tac [@{thm thinL}, @{thm thinR}, p2 COMP @{thm monotonic}] 1)
THEN
safe_tac LK_pack 1));
qed "conj_cong";
Goal "|- (x=y) <-> (y=x)";
-by (fast_tac (LK_pack add_safes [thm "subst"]) 1);
+by (fast_tac (LK_pack add_safes @{thms subst}) 1);
qed "eq_sym_conv";
@@ -240,7 +223,7 @@
val LK_simps =
[triv_forall_equality, (* prunes params *)
- thm "refl" RS P_iff_T] @
+ @{thm refl} RS P_iff_T] @
conj_simps @ disj_simps @ not_simps @
imp_simps @ iff_simps @quant_simps @ all_simps @ ex_simps @
[de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2] @