--- a/src/Sequents/LK.thy Sat Feb 01 18:00:28 2014 +0100
+++ b/src/Sequents/LK.thy Sat Feb 01 18:05:03 2014 +0100
@@ -202,19 +202,21 @@
ML_file "simpdata.ML"
setup {* map_theory_simpset (put_simpset LK_ss) *}
+setup {* Simplifier.method_setup [] *}
text {* To create substition rules *}
lemma eq_imp_subst: "|- a=b ==> $H, A(a), $G |- $E, A(b), $F"
- apply (tactic {* asm_simp_tac (put_simpset LK_basic_ss @{context}) 1 *})
- done
+ by simp
lemma split_if: "|- P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))"
apply (rule_tac P = Q in cut)
- apply (tactic {* simp_tac (@{context} addsimps @{thms if_P}) 2 *})
+ prefer 2
+ apply (simp add: if_P)
apply (rule_tac P = "~Q" in cut)
- apply (tactic {* simp_tac (@{context} addsimps @{thms if_not_P}) 2 *})
+ prefer 2
+ apply (simp add: if_not_P)
apply fast
done
--- a/src/Sequents/LK/Nat.thy Sat Feb 01 18:00:28 2014 +0100
+++ b/src/Sequents/LK/Nat.thy Sat Feb 01 18:05:03 2014 +0100
@@ -36,7 +36,7 @@
lemma Suc_n_not_n: "|- Suc(k) ~= k"
apply (rule_tac n = k in induct)
- apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms Suc_neq_0}) 1 *})
+ apply simp
apply (fast add!: Suc_inject_rule)
done
@@ -54,26 +54,22 @@
lemma add_assoc: "|- (k+m)+n = k+(m+n)"
apply (rule_tac n = "k" in induct)
- apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_0}) 1 *})
- apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_Suc}) 1 *})
+ apply simp_all
done
lemma add_0_right: "|- m+0 = m"
apply (rule_tac n = "m" in induct)
- apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_0}) 1 *})
- apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_Suc}) 1 *})
+ apply simp_all
done
lemma add_Suc_right: "|- m+Suc(n) = Suc(m+n)"
apply (rule_tac n = "m" in induct)
- apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_0}) 1 *})
- apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_Suc}) 1 *})
+ apply simp_all
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 (put_simpset LK_ss @{context} addsimps @{thms add_0}) 1 *})
- apply (tactic {* asm_simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_Suc}) 1 *})
+ apply simp_all
done
end