src/LCF/simpdata.ML
author lcp
Thu Oct 21 14:59:54 1993 +0100 (1993-10-21)
changeset 65 08d3c007ae7c
parent 0 a5a9c433f639
child 190 4ae10fc91cba
permissions -rw-r--r--
simpdata/basify: now calls new fastype_of
     1 (*  Title: 	LCF/simpdata
     2     ID:         $Id$
     3     Author: 	Tobias Nipkow, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Simplification data for LCF
     7 *)
     8 
     9 
    10 fun mk_rew_rules r =
    11 let fun basify thm =
    12 	  (case concl_of thm of
    13              _$(_$t$_) => (case fastype_of t of
    14 	                     Type("fun",_) => basify(thm RS ap_thm)
    15 	                   | _ => thm)
    16            | _ => thm)
    17 in map (mk_meta_eq o basify) (atomize r) end;
    18 
    19 val LCF_rews = [minimal,
    20 	 UU_app, UU_app RS ap_thm, UU_app RS ap_thm RS ap_thm,
    21 	 not_TT_less_FF,not_FF_less_TT,not_TT_less_UU,not_FF_less_UU,
    22 	 not_UU_eq_TT,not_UU_eq_FF,not_TT_eq_UU,not_TT_eq_FF,
    23 	 not_FF_eq_UU,not_FF_eq_TT,
    24 	 COND_UU,COND_TT,COND_FF,
    25 	 surj_pairing,FST,SND];
    26 
    27 val LCF_ss = FOL_ss setmksimps mk_rew_rules
    28                     addsimps LCF_rews;