1(* Title: Sequents/simpdata.ML 2 Author: Lawrence C Paulson 3 Copyright 1999 University of Cambridge 4 5Instantiation of the generic simplifier for LK. 6 7Borrows from the DC simplifier of Soren Heilmann. 8*) 9 10 11(** Conversion into rewrite rules **) 12 13(*Make atomic rewrite rules*) 14fun atomize r = 15 case Thm.concl_of r of 16 Const(\<^const_name>\<open>Trueprop\<close>,_) $ Abs(_,_,a) $ Abs(_,_,c) => 17 (case (Cla.forms_of_seq a, Cla.forms_of_seq c) of 18 ([], [p]) => 19 (case p of 20 Const(\<^const_name>\<open>imp\<close>,_)$_$_ => atomize(r RS @{thm mp_R}) 21 | Const(\<^const_name>\<open>conj\<close>,_)$_$_ => atomize(r RS @{thm conjunct1}) @ 22 atomize(r RS @{thm conjunct2}) 23 | Const(\<^const_name>\<open>All\<close>,_)$_ => atomize(r RS @{thm spec}) 24 | Const(\<^const_name>\<open>True\<close>,_) => [] (*True is DELETED*) 25 | Const(\<^const_name>\<open>False\<close>,_) => [] (*should False do something?*) 26 | _ => [r]) 27 | _ => []) (*ignore theorem unless it has precisely one conclusion*) 28 | _ => [r]; 29 30(*Make meta-equalities.*) 31fun mk_meta_eq ctxt th = case Thm.concl_of th of 32 Const(\<^const_name>\<open>Pure.eq\<close>,_)$_$_ => th 33 | Const(\<^const_name>\<open>Trueprop\<close>,_) $ Abs(_,_,a) $ Abs(_,_,c) => 34 (case (Cla.forms_of_seq a, Cla.forms_of_seq c) of 35 ([], [p]) => 36 (case p of 37 (Const(\<^const_name>\<open>equal\<close>,_)$_$_) => th RS @{thm eq_reflection} 38 | (Const(\<^const_name>\<open>iff\<close>,_)$_$_) => th RS @{thm iff_reflection} 39 | (Const(\<^const_name>\<open>Not\<close>,_)$_) => th RS @{thm iff_reflection_F} 40 | _ => th RS @{thm iff_reflection_T}) 41 | _ => error ("addsimps: unable to use theorem\n" ^ Thm.string_of_thm ctxt th)); 42 43(*Replace premises x=y, X<->Y by X==Y*) 44fun mk_meta_prems ctxt = 45 rule_by_tactic ctxt 46 (REPEAT_FIRST (resolve_tac ctxt [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}])); 47 48(*Congruence rules for = or <-> (instead of ==)*) 49fun mk_meta_cong ctxt rl = 50 Drule.zero_var_indexes (mk_meta_eq ctxt (mk_meta_prems ctxt rl)) 51 handle THM _ => 52 error("Premises and conclusion of congruence rules must use =-equality or <->"); 53 54 55(*** Standard simpsets ***) 56 57val triv_rls = [@{thm FalseL}, @{thm TrueR}, @{thm basic}, @{thm refl}, 58 @{thm iff_refl}, reflexive_thm]; 59 60fun unsafe_solver ctxt = 61 FIRST' [resolve_tac ctxt (triv_rls @ Simplifier.prems_of ctxt), assume_tac ctxt]; 62 63(*No premature instantiation of variables during simplification*) 64fun safe_solver ctxt = 65 FIRST' [fn i => DETERM (match_tac ctxt (triv_rls @ Simplifier.prems_of ctxt) i), 66 eq_assume_tac]; 67 68(*No simprules, but basic infrastructure for simplification*) 69val LK_basic_ss = 70 empty_simpset \<^context> 71 setSSolver (mk_solver "safe" safe_solver) 72 setSolver (mk_solver "unsafe" unsafe_solver) 73 |> Simplifier.set_subgoaler asm_simp_tac 74 |> Simplifier.set_mksimps (fn ctxt => map (mk_meta_eq ctxt) o atomize o Variable.gen_all ctxt) 75 |> Simplifier.set_mkcong mk_meta_cong 76 |> simpset_of; 77 78val LK_simps = 79 [@{thm triv_forall_equality}, (* prunes params *) 80 @{thm refl} RS @{thm P_iff_T}] @ 81 @{thms conj_simps} @ @{thms disj_simps} @ @{thms not_simps} @ 82 @{thms imp_simps} @ @{thms iff_simps} @ @{thms quant_simps} @ 83 @{thms all_simps} @ @{thms ex_simps} @ 84 [@{thm de_Morgan_conj}, @{thm de_Morgan_disj}, @{thm imp_disj1}, @{thm imp_disj2}] @ 85 @{thms LK_extra_simps}; 86 87val LK_ss = 88 put_simpset LK_basic_ss \<^context> addsimps LK_simps 89 |> Simplifier.add_eqcong @{thm left_cong} 90 |> Simplifier.add_cong @{thm imp_cong} 91 |> simpset_of; 92 93