# HG changeset patch
# User wenzelm
# Date 1178732241 -7200
# Node ID 1c2abcabea612e203277ad28481666064696d810
# Parent  adc529c89281e3c971b5ff8d90c6e57873648cd2
tuned ML setup;

diff -r adc529c89281 -r 1c2abcabea61 src/Sequents/LK/Hard_Quantifiers.thy
--- 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
diff -r adc529c89281 -r 1c2abcabea61 src/Sequents/LK/Nat.thy
--- 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
diff -r adc529c89281 -r 1c2abcabea61 src/Sequents/simpdata.ML
--- 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] @