author  paulson 
Thu, 14 Jun 2018 14:23:48 +0100  
changeset 68446  92ddca1edc43 
parent 60774  6c28d8ed2488 
child 69593  3dda49e08b9d 
permissions  rwrr 
1463  1 
(* Title: FOLP/simpdata.ML 
1459  2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  3 
Copyright 1991 University of Cambridge 
4 

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

8 

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

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

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

0  15 

16 

17 
(* Conversion into rewrite rules *) 

18 

59582  19 
fun mk_eq th = case Thm.concl_of th of 
41310  20 
_ $ (Const (@{const_name iff}, _) $ _ $ _) $ _ => th 
21 
 _ $ (Const (@{const_name eq}, _) $ _ $ _) $ _ => th 

26322  22 
 _ $ (Const (@{const_name Not}, _) $ _) $ _ => th RS @{thm not_P_imp_P_iff_F} 
0  23 
 _ => make_iff_T th; 
24 

5304  25 

26 
val mksimps_pairs = 

41310  27 
[(@{const_name imp}, [@{thm mp}]), 
28 
(@{const_name conj}, [@{thm conjunct1}, @{thm conjunct2}]), 

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

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

0  32 

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

59582  35 
(case Thm.concl_of th of 
26322  36 
Const ("Trueprop", _) $ p => 
5304  37 
(case head_of p of 
38 
Const(a,_) => 

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

44 
in atoms end; 

45 

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

0  47 

48 
(*destruct function for analysing equations*) 

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

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

52 
structure FOLP_SimpData : SIMP_DATA = 

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

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

56 
val red1 = @{thm iffD1} 

57 
val red2 = @{thm iffD2} 

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

60 
val norm_thms = norm_thms 

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

65 
structure FOLP_Simp = SimpFun(FOLP_SimpData); 

66 

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

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

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

0  72 

73 
val IFOLP_rews = 

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

0  76 

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

77 
open FOLP_Simp; 
0  78 

60774  79 
val auto_ss = empty_ss setauto (fn ctxt => ares_tac ctxt @{thms TrueI}); 
0  80 

60644  81 
val IFOLP_ss = auto_ss addcongs FOLP_congs > fold (addrew @{context}) IFOLP_rews; 
0  82 

83 

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

60644  86 
val FOLP_ss = auto_ss addcongs FOLP_congs > fold (addrew @{context}) FOLP_rews; 