200 lemma eq_sym_conv: "|- (x=y) <-> (y=x)" |
200 lemma eq_sym_conv: "|- (x=y) <-> (y=x)" |
201 by (fast add!: subst) |
201 by (fast add!: subst) |
202 |
202 |
203 ML_file "simpdata.ML" |
203 ML_file "simpdata.ML" |
204 setup {* map_theory_simpset (put_simpset LK_ss) *} |
204 setup {* map_theory_simpset (put_simpset LK_ss) *} |
|
205 setup {* Simplifier.method_setup [] *} |
205 |
206 |
206 |
207 |
207 text {* To create substition rules *} |
208 text {* To create substition rules *} |
208 |
209 |
209 lemma eq_imp_subst: "|- a=b ==> $H, A(a), $G |- $E, A(b), $F" |
210 lemma eq_imp_subst: "|- a=b ==> $H, A(a), $G |- $E, A(b), $F" |
210 apply (tactic {* asm_simp_tac (put_simpset LK_basic_ss @{context}) 1 *}) |
211 by simp |
211 done |
|
212 |
212 |
213 lemma split_if: "|- P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))" |
213 lemma split_if: "|- P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))" |
214 apply (rule_tac P = Q in cut) |
214 apply (rule_tac P = Q in cut) |
215 apply (tactic {* simp_tac (@{context} addsimps @{thms if_P}) 2 *}) |
215 prefer 2 |
|
216 apply (simp add: if_P) |
216 apply (rule_tac P = "~Q" in cut) |
217 apply (rule_tac P = "~Q" in cut) |
217 apply (tactic {* simp_tac (@{context} addsimps @{thms if_not_P}) 2 *}) |
218 prefer 2 |
|
219 apply (simp add: if_not_P) |
218 apply fast |
220 apply fast |
219 done |
221 done |
220 |
222 |
221 lemma if_cancel: "|- (if P then x else x) = x" |
223 lemma if_cancel: "|- (if P then x else x) = x" |
222 apply (tactic {* lemma_tac @{thm split_if} 1 *}) |
224 apply (tactic {* lemma_tac @{thm split_if} 1 *}) |