author  wenzelm 
Sun, 11 Jan 2009 21:49:59 +0100  
changeset 29450  ac7f67be7f1f 
parent 26322  eaf634e975fa 
child 35762  af3ff2ba4c54 
permissions  rwrr 
1463  1 
(* Title: FOLP/simpdata.ML 
0  2 
ID: $Id$ 
1459  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1991 University of Cambridge 
5 

17480  6 
Simplification data for FOLP. 
0  7 
*) 
8 

9 

26322  10 
fun make_iff_T th = th RS @{thm P_Imp_P_iff_T}; 
0  11 

26322  12 
val refl_iff_T = make_iff_T @{thm refl}; 
0  13 

26322  14 
val norm_thms = [(@{thm norm_eq} RS @{thm sym}, @{thm norm_eq}), 
15 
(@{thm NORM_iff} RS @{thm iff_sym}, @{thm NORM_iff})]; 

0  16 

17 

18 
(* Conversion into rewrite rules *) 

19 

20 
fun mk_eq th = case concl_of th of 

26322  21 
_ $ (Const (@{const_name "op <>"}, _) $ _ $ _) $ _ => th 
22 
 _ $ (Const (@{const_name "op ="}, _) $ _ $ _) $ _ => th 

23 
 _ $ (Const (@{const_name Not}, _) $ _) $ _ => th RS @{thm not_P_imp_P_iff_F} 

0  24 
 _ => make_iff_T th; 
25 

5304  26 

27 
val mksimps_pairs = 

26322  28 
[(@{const_name "op >"}, [@{thm mp}]), 
29 
(@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}]), 

30 
(@{const_name "All"}, [@{thm spec}]), 

31 
(@{const_name True}, []), 

32 
(@{const_name False}, [])]; 

0  33 

5304  34 
fun mk_atomize pairs = 
35 
let fun atoms th = 

36 
(case concl_of th of 

26322  37 
Const ("Trueprop", _) $ p => 
5304  38 
(case head_of p of 
39 
Const(a,_) => 

17325  40 
(case AList.lookup (op =) pairs a of 
26322  41 
SOME(rls) => maps atoms ([th] RL rls) 
15531  42 
 NONE => [th]) 
5304  43 
 _ => [th]) 
44 
 _ => [th]) 

45 
in atoms end; 

46 

47 
fun mk_rew_rules th = map mk_eq (mk_atomize mksimps_pairs th); 

0  48 

49 
(*destruct function for analysing equations*) 

50 
fun dest_red(_ $ (red $ lhs $ rhs) $ _) = (red,lhs,rhs) 

26322  51 
 dest_red t = raise TERM("dest_red", [t]); 
0  52 

53 
structure FOLP_SimpData : SIMP_DATA = 

26322  54 
struct 
55 
val refl_thms = [@{thm refl}, @{thm iff_refl}] 

56 
val trans_thms = [@{thm trans}, @{thm iff_trans}] 

57 
val red1 = @{thm iffD1} 

58 
val red2 = @{thm iffD2} 

1459  59 
val mk_rew_rules = mk_rew_rules 
60 
val case_splits = [] (*NO IF'S!*) 

61 
val norm_thms = norm_thms 

26322  62 
val subst_thms = [@{thm subst}]; 
1459  63 
val dest_red = dest_red 
26322  64 
end; 
0  65 

66 
structure FOLP_Simp = SimpFun(FOLP_SimpData); 

67 

68 
(*not a component of SIMP_DATA, but an argument of SIMP_TAC *) 

17480  69 
val FOLP_congs = 
26322  70 
[@{thm all_cong}, @{thm ex_cong}, @{thm eq_cong}, 
71 
@{thm conj_cong}, @{thm disj_cong}, @{thm imp_cong}, 

72 
@{thm iff_cong}, @{thm not_cong}] @ @{thms pred_congs}; 

0  73 

74 
val IFOLP_rews = 

26322  75 
[refl_iff_T] @ @{thms conj_rews} @ @{thms disj_rews} @ @{thms not_rews} @ 
76 
@{thms imp_rews} @ @{thms iff_rews} @ @{thms quant_rews}; 

0  77 

1009
eb7c50688405
No longer builds the induction structure (from ../Provers/ind.ML)
lcp
parents:
0
diff
changeset

78 
open FOLP_Simp; 
0  79 

26322  80 
val auto_ss = empty_ss setauto ares_tac [@{thm TrueI}]; 
0  81 

82 
val IFOLP_ss = auto_ss addcongs FOLP_congs addrews IFOLP_rews; 

83 

84 

26322  85 
val FOLP_rews = IFOLP_rews @ @{thms cla_rews}; 
0  86 

87 
val FOLP_ss = auto_ss addcongs FOLP_congs addrews FOLP_rews; 