398 |
398 |
399 val HOL_basic_ss = empty_ss setsubgoaler asm_simp_tac |
399 val HOL_basic_ss = empty_ss setsubgoaler asm_simp_tac |
400 setSSolver safe_solver |
400 setSSolver safe_solver |
401 setSolver unsafe_solver |
401 setSolver unsafe_solver |
402 setmksimps (mksimps mksimps_pairs) |
402 setmksimps (mksimps mksimps_pairs) |
403 setmkeqTrue mk_meta_eq_True |
403 setmkeqTrue mk_meta_eq_True; |
404 addsplits [expand_if]; |
|
405 |
404 |
406 val HOL_ss = |
405 val HOL_ss = |
407 HOL_basic_ss addsimps |
406 HOL_basic_ss addsimps |
408 ([triv_forall_equality, (* prunes params *) |
407 ([triv_forall_equality, (* prunes params *) |
409 True_implies_equals, (* prune asms `True' *) |
408 True_implies_equals, (* prune asms `True' *) |
411 o_apply, imp_disjL, conj_assoc, disj_assoc, |
410 o_apply, imp_disjL, conj_assoc, disj_assoc, |
412 de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp, |
411 de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp, |
413 disj_not1, not_all, not_ex, cases_simp] |
412 disj_not1, not_all, not_ex, cases_simp] |
414 @ ex_simps @ all_simps @ simp_thms) |
413 @ ex_simps @ all_simps @ simp_thms) |
415 addsimprocs [defALL_regroup,defEX_regroup] |
414 addsimprocs [defALL_regroup,defEX_regroup] |
416 addcongs [imp_cong]; |
415 addcongs [imp_cong] |
|
416 addsplits [expand_if]; |
417 |
417 |
418 qed_goal "if_distrib" HOL.thy |
418 qed_goal "if_distrib" HOL.thy |
419 "f(if c then x else y) = (if c then f x else f y)" |
419 "f(if c then x else y) = (if c then f x else f y)" |
420 (K [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]); |
420 (K [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]); |
421 |
421 |