0
|
1 |
(* Title: LCF/simpdata
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow, Cambridge University Computer Laboratory
|
65
|
4 |
Copyright 1993 University of Cambridge
|
0
|
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
|
65
|
13 |
_$(_$t$_) => (case fastype_of t of
|
0
|
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;
|