src/FOLP/simpdata.ML
author blanchet
Mon May 19 23:43:53 2014 +0200 (2014-05-19)
changeset 57009 8cb6a5f1ae84
parent 41310 65631ca437c9
child 59582 0fbed69ff081
permissions -rw-r--r--
added SML implementation of MaSh
clasohm@1463
     1
(*  Title:      FOLP/simpdata.ML
clasohm@1459
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     3
    Copyright   1991  University of Cambridge
clasohm@0
     4
wenzelm@17480
     5
Simplification data for FOLP.
clasohm@0
     6
*)
clasohm@0
     7
clasohm@0
     8
wenzelm@26322
     9
fun make_iff_T th = th RS @{thm P_Imp_P_iff_T};
clasohm@0
    10
wenzelm@26322
    11
val refl_iff_T = make_iff_T @{thm refl};
clasohm@0
    12
wenzelm@26322
    13
val norm_thms = [(@{thm norm_eq} RS @{thm sym}, @{thm norm_eq}),
wenzelm@26322
    14
                 (@{thm NORM_iff} RS @{thm iff_sym}, @{thm NORM_iff})];
clasohm@0
    15
clasohm@0
    16
clasohm@0
    17
(* Conversion into rewrite rules *)
clasohm@0
    18
clasohm@0
    19
fun mk_eq th = case concl_of th of
wenzelm@41310
    20
      _ $ (Const (@{const_name iff}, _) $ _ $ _) $ _ => th
wenzelm@41310
    21
    | _ $ (Const (@{const_name eq}, _) $ _ $ _) $ _ => th
wenzelm@26322
    22
    | _ $ (Const (@{const_name Not}, _) $ _) $ _ => th RS @{thm not_P_imp_P_iff_F}
clasohm@0
    23
    | _ => make_iff_T th;
clasohm@0
    24
oheimb@5304
    25
oheimb@5304
    26
val mksimps_pairs =
wenzelm@41310
    27
  [(@{const_name imp}, [@{thm mp}]),
wenzelm@41310
    28
   (@{const_name conj}, [@{thm conjunct1}, @{thm conjunct2}]),
wenzelm@26322
    29
   (@{const_name "All"}, [@{thm spec}]),
wenzelm@26322
    30
   (@{const_name True}, []),
wenzelm@26322
    31
   (@{const_name False}, [])];
clasohm@0
    32
oheimb@5304
    33
fun mk_atomize pairs =
oheimb@5304
    34
  let fun atoms th =
oheimb@5304
    35
        (case concl_of th of
wenzelm@26322
    36
           Const ("Trueprop", _) $ p =>
oheimb@5304
    37
             (case head_of p of
oheimb@5304
    38
                Const(a,_) =>
haftmann@17325
    39
                  (case AList.lookup (op =) pairs a of
wenzelm@26322
    40
                     SOME(rls) => maps atoms ([th] RL rls)
skalberg@15531
    41
                   | NONE => [th])
oheimb@5304
    42
              | _ => [th])
oheimb@5304
    43
         | _ => [th])
oheimb@5304
    44
  in atoms end;
oheimb@5304
    45
oheimb@5304
    46
fun mk_rew_rules th = map mk_eq (mk_atomize mksimps_pairs th);
clasohm@0
    47
clasohm@0
    48
(*destruct function for analysing equations*)
clasohm@0
    49
fun dest_red(_ $ (red $ lhs $ rhs) $ _) = (red,lhs,rhs)
wenzelm@26322
    50
  | dest_red t = raise TERM("dest_red", [t]);
clasohm@0
    51
clasohm@0
    52
structure FOLP_SimpData : SIMP_DATA =
wenzelm@26322
    53
struct
wenzelm@26322
    54
  val refl_thms         = [@{thm refl}, @{thm iff_refl}]
wenzelm@26322
    55
  val trans_thms        = [@{thm trans}, @{thm iff_trans}]
wenzelm@26322
    56
  val red1              = @{thm iffD1}
wenzelm@26322
    57
  val red2              = @{thm iffD2}
clasohm@1459
    58
  val mk_rew_rules      = mk_rew_rules
clasohm@1459
    59
  val case_splits       = []         (*NO IF'S!*)
clasohm@1459
    60
  val norm_thms         = norm_thms
wenzelm@26322
    61
  val subst_thms        = [@{thm subst}];
clasohm@1459
    62
  val dest_red          = dest_red
wenzelm@26322
    63
end;
clasohm@0
    64
clasohm@0
    65
structure FOLP_Simp = SimpFun(FOLP_SimpData);
clasohm@0
    66
clasohm@0
    67
(*not a component of SIMP_DATA, but an argument of SIMP_TAC *)
wenzelm@17480
    68
val FOLP_congs =
wenzelm@26322
    69
   [@{thm all_cong}, @{thm ex_cong}, @{thm eq_cong},
wenzelm@26322
    70
    @{thm conj_cong}, @{thm disj_cong}, @{thm imp_cong},
wenzelm@26322
    71
    @{thm iff_cong}, @{thm not_cong}] @ @{thms pred_congs};
clasohm@0
    72
clasohm@0
    73
val IFOLP_rews =
wenzelm@26322
    74
   [refl_iff_T] @ @{thms conj_rews} @ @{thms disj_rews} @ @{thms not_rews} @
wenzelm@26322
    75
    @{thms imp_rews} @ @{thms iff_rews} @ @{thms quant_rews};
clasohm@0
    76
lcp@1009
    77
open FOLP_Simp;
clasohm@0
    78
wenzelm@26322
    79
val auto_ss = empty_ss setauto ares_tac [@{thm TrueI}];
clasohm@0
    80
clasohm@0
    81
val IFOLP_ss = auto_ss addcongs FOLP_congs addrews IFOLP_rews;
clasohm@0
    82
clasohm@0
    83
wenzelm@26322
    84
val FOLP_rews = IFOLP_rews @ @{thms cla_rews};
clasohm@0
    85
clasohm@0
    86
val FOLP_ss = auto_ss addcongs FOLP_congs addrews FOLP_rews;