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