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; |
|