proper Simplifier method setup;
authorwenzelm
Sat Feb 01 18:05:03 2014 +0100 (2014-02-01)
changeset 55230cb5ef74b32f9
parent 55229 08f2ebb65078
child 55231 264d34c19bf2
proper Simplifier method setup;
src/Sequents/LK.thy
src/Sequents/LK/Nat.thy
     1.1 --- a/src/Sequents/LK.thy	Sat Feb 01 18:00:28 2014 +0100
     1.2 +++ b/src/Sequents/LK.thy	Sat Feb 01 18:05:03 2014 +0100
     1.3 @@ -202,19 +202,21 @@
     1.4  
     1.5  ML_file "simpdata.ML"
     1.6  setup {* map_theory_simpset (put_simpset LK_ss) *}
     1.7 +setup {* Simplifier.method_setup [] *}
     1.8  
     1.9  
    1.10  text {* To create substition rules *}
    1.11  
    1.12  lemma eq_imp_subst: "|- a=b ==> $H, A(a), $G |- $E, A(b), $F"
    1.13 -  apply (tactic {* asm_simp_tac (put_simpset LK_basic_ss @{context}) 1 *})
    1.14 -  done
    1.15 +  by simp
    1.16  
    1.17  lemma split_if: "|- P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))"
    1.18    apply (rule_tac P = Q in cut)
    1.19 -   apply (tactic {* simp_tac (@{context} addsimps @{thms if_P}) 2 *})
    1.20 +   prefer 2
    1.21 +   apply (simp add: if_P)
    1.22    apply (rule_tac P = "~Q" in cut)
    1.23 -   apply (tactic {* simp_tac (@{context} addsimps @{thms if_not_P}) 2 *})
    1.24 +   prefer 2
    1.25 +   apply (simp add: if_not_P)
    1.26    apply fast
    1.27    done
    1.28  
     2.1 --- a/src/Sequents/LK/Nat.thy	Sat Feb 01 18:00:28 2014 +0100
     2.2 +++ b/src/Sequents/LK/Nat.thy	Sat Feb 01 18:05:03 2014 +0100
     2.3 @@ -36,7 +36,7 @@
     2.4  
     2.5  lemma Suc_n_not_n: "|- Suc(k) ~= k"
     2.6    apply (rule_tac n = k in induct)
     2.7 -  apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms Suc_neq_0}) 1 *})
     2.8 +  apply simp
     2.9    apply (fast add!: Suc_inject_rule)
    2.10    done
    2.11  
    2.12 @@ -54,26 +54,22 @@
    2.13  
    2.14  lemma add_assoc: "|- (k+m)+n = k+(m+n)"
    2.15    apply (rule_tac n = "k" in induct)
    2.16 -  apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_0}) 1 *})
    2.17 -  apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_Suc}) 1 *})
    2.18 +  apply simp_all
    2.19    done
    2.20  
    2.21  lemma add_0_right: "|- m+0 = m"
    2.22    apply (rule_tac n = "m" in induct)
    2.23 -  apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_0}) 1 *})
    2.24 -  apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_Suc}) 1 *})
    2.25 +  apply simp_all
    2.26    done
    2.27  
    2.28  lemma add_Suc_right: "|- m+Suc(n) = Suc(m+n)"
    2.29    apply (rule_tac n = "m" in induct)
    2.30 -  apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_0}) 1 *})
    2.31 -  apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_Suc}) 1 *})
    2.32 +  apply simp_all
    2.33    done
    2.34  
    2.35  lemma "(!!n. |- f(Suc(n)) = Suc(f(n))) ==> |- f(i+j) = i+f(j)"
    2.36    apply (rule_tac n = "i" in induct)
    2.37 -  apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_0}) 1 *})
    2.38 -  apply (tactic {* asm_simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_Suc}) 1 *})
    2.39 +  apply simp_all
    2.40    done
    2.41  
    2.42  end