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