method_setup "lem";
authorwenzelm
Sat Feb 01 18:22:38 2014 +0100 (2014-02-01)
changeset 552333229614ca9c5
parent 55232 7a46672934a3
child 55234 7c6c833069d2
method_setup "lem";
src/Sequents/LK.thy
src/Sequents/LK0.thy
     1.1 --- a/src/Sequents/LK.thy	Sat Feb 01 18:17:13 2014 +0100
     1.2 +++ b/src/Sequents/LK.thy	Sat Feb 01 18:22:38 2014 +0100
     1.3 @@ -175,7 +175,7 @@
     1.4    assumes p1: "|- P <-> P'"
     1.5      and p2: "|- P' ==> |- Q <-> Q'"
     1.6    shows "|- (P-->Q) <-> (P'-->Q')"
     1.7 -  apply (tactic {* lemma_tac @{thm p1} 1 *})
     1.8 +  apply (lem p1)
     1.9    apply safe
    1.10     apply (tactic {*
    1.11       REPEAT (rtac @{thm cut} 1 THEN
    1.12 @@ -188,7 +188,7 @@
    1.13    assumes p1: "|- P <-> P'"
    1.14      and p2: "|- P' ==> |- Q <-> Q'"
    1.15    shows "|- (P&Q) <-> (P'&Q')"
    1.16 -  apply (tactic {* lemma_tac @{thm p1} 1 *})
    1.17 +  apply (lem p1)
    1.18    apply safe
    1.19     apply (tactic {*
    1.20       REPEAT (rtac @{thm cut} 1 THEN
    1.21 @@ -221,12 +221,12 @@
    1.22    done
    1.23  
    1.24  lemma if_cancel: "|- (if P then x else x) = x"
    1.25 -  apply (tactic {* lemma_tac @{thm split_if} 1 *})
    1.26 +  apply (lem split_if)
    1.27    apply fast
    1.28    done
    1.29  
    1.30  lemma if_eq_cancel: "|- (if x=y then y else x) = x"
    1.31 -  apply (tactic {* lemma_tac @{thm split_if} 1 *})
    1.32 +  apply (lem split_if)
    1.33    apply safe
    1.34    apply (rule symL)
    1.35    apply (rule basic)
     2.1 --- a/src/Sequents/LK0.thy	Sat Feb 01 18:17:13 2014 +0100
     2.2 +++ b/src/Sequents/LK0.thy	Sat Feb 01 18:22:38 2014 +0100
     2.3 @@ -232,14 +232,6 @@
     2.4      |> Cla.get_pack;
     2.5  *}
     2.6  
     2.7 -ML {*
     2.8 -  fun lemma_tac th i =
     2.9 -    rtac (@{thm thinR} RS @{thm cut}) i THEN
    2.10 -    REPEAT (rtac @{thm thinL} i) THEN
    2.11 -    rtac th i;
    2.12 -*}
    2.13 -
    2.14 -
    2.15  method_setup fast_prop =
    2.16    {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.fast_tac (Cla.put_pack prop_pack ctxt))) *}
    2.17  
    2.18 @@ -249,6 +241,14 @@
    2.19  method_setup best_dup =
    2.20    {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.best_tac (Cla.put_pack LK_dup_pack ctxt))) *}
    2.21  
    2.22 +method_setup lem = {*
    2.23 +  Attrib.thm >> (fn th => fn _ =>
    2.24 +    SIMPLE_METHOD' (fn i =>
    2.25 +      rtac (@{thm thinR} RS @{thm cut}) i THEN
    2.26 +      REPEAT (rtac @{thm thinL} i) THEN
    2.27 +      rtac th i))
    2.28 +*}
    2.29 +
    2.30  
    2.31  lemma mp_R:
    2.32    assumes major: "$H |- $E, $F, P --> Q"