(* Title: FOLP/simpdata.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
Simplification data for FOLP.
*)
fun make_iff_T th = th RS @{thm P_Imp_P_iff_T};
val refl_iff_T = make_iff_T @{thm refl};
val norm_thms = [(@{thm norm_eq} RS @{thm sym}, @{thm norm_eq}),
(@{thm NORM_iff} RS @{thm iff_sym}, @{thm NORM_iff})];
(* Conversion into rewrite rules *)
fun mk_eq th = case concl_of th of
_ $ (Const (@{const_name "op <->"}, _) $ _ $ _) $ _ => th
| _ $ (Const (@{const_name "op ="}, _) $ _ $ _) $ _ => th
| _ $ (Const (@{const_name Not}, _) $ _) $ _ => th RS @{thm not_P_imp_P_iff_F}
| _ => make_iff_T th;
val mksimps_pairs =
[(@{const_name "op -->"}, [@{thm mp}]),
(@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}]),
(@{const_name "All"}, [@{thm spec}]),
(@{const_name True}, []),
(@{const_name False}, [])];
fun mk_atomize pairs =
let fun atoms th =
(case concl_of th of
Const ("Trueprop", _) $ p =>
(case head_of p of
Const(a,_) =>
(case AList.lookup (op =) pairs a of
SOME(rls) => maps atoms ([th] RL rls)
| NONE => [th])
| _ => [th])
| _ => [th])
in atoms end;
fun mk_rew_rules th = map mk_eq (mk_atomize mksimps_pairs th);
(*destruct function for analysing equations*)
fun dest_red(_ $ (red $ lhs $ rhs) $ _) = (red,lhs,rhs)
| dest_red t = raise TERM("dest_red", [t]);
structure FOLP_SimpData : SIMP_DATA =
struct
val refl_thms = [@{thm refl}, @{thm iff_refl}]
val trans_thms = [@{thm trans}, @{thm iff_trans}]
val red1 = @{thm iffD1}
val red2 = @{thm iffD2}
val mk_rew_rules = mk_rew_rules
val case_splits = [] (*NO IF'S!*)
val norm_thms = norm_thms
val subst_thms = [@{thm subst}];
val dest_red = dest_red
end;
structure FOLP_Simp = SimpFun(FOLP_SimpData);
(*not a component of SIMP_DATA, but an argument of SIMP_TAC *)
val FOLP_congs =
[@{thm all_cong}, @{thm ex_cong}, @{thm eq_cong},
@{thm conj_cong}, @{thm disj_cong}, @{thm imp_cong},
@{thm iff_cong}, @{thm not_cong}] @ @{thms pred_congs};
val IFOLP_rews =
[refl_iff_T] @ @{thms conj_rews} @ @{thms disj_rews} @ @{thms not_rews} @
@{thms imp_rews} @ @{thms iff_rews} @ @{thms quant_rews};
open FOLP_Simp;
val auto_ss = empty_ss setauto ares_tac [@{thm TrueI}];
val IFOLP_ss = auto_ss addcongs FOLP_congs addrews IFOLP_rews;
val FOLP_rews = IFOLP_rews @ @{thms cla_rews};
val FOLP_ss = auto_ss addcongs FOLP_congs addrews FOLP_rews;