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