src/LCF/simpdata.ML
changeset 190 4ae10fc91cba
parent 65 08d3c007ae7c
child 1461 6bcb44e4d6e5
equal deleted inserted replaced
189:831a9a7ab9f3 190:4ae10fc91cba
     4     Copyright   1993  University of Cambridge
     4     Copyright   1993  University of Cambridge
     5 
     5 
     6 Simplification data for LCF
     6 Simplification data for LCF
     7 *)
     7 *)
     8 
     8 
     9 
     9 val LCF_ss = FOL_ss addsimps
    10 fun mk_rew_rules r =
    10         [minimal,
    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,
    11 	 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,
    12 	 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,
    13 	 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,
    14 	 not_FF_eq_UU,not_FF_eq_TT,
    24 	 COND_UU,COND_TT,COND_FF,
    15 	 COND_UU,COND_TT,COND_FF,
    25 	 surj_pairing,FST,SND];
    16 	 surj_pairing,FST,SND];
    26 
       
    27 val LCF_ss = FOL_ss setmksimps mk_rew_rules
       
    28                     addsimps LCF_rews;