author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 17480  fd19f77dcf60 
child 26322  eaf634e975fa 
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 
(*** Rewrite rules ***) 

10 

17480  11 
fun int_prove_fun_raw s = 
12 
(writeln s; prove_goal (the_context ()) s 

2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
1463
diff
changeset

13 
(fn prems => [ (cut_facts_tac prems 1), (IntPr.fast_tac 1) ])); 
0  14 

15 
fun int_prove_fun s = int_prove_fun_raw ("?p : "^s); 

16 

17 
val conj_rews = map int_prove_fun 

1459  18 
["P & True <> P", "True & P <> P", 
0  19 
"P & False <> False", "False & P <> False", 
20 
"P & P <> P", 

1459  21 
"P & ~P <> False", "~P & P <> False", 
0  22 
"(P & Q) & R <> P & (Q & R)"]; 
23 

24 
val disj_rews = map int_prove_fun 

1459  25 
["P  True <> True", "True  P <> True", 
26 
"P  False <> P", "False  P <> P", 

0  27 
"P  P <> P", 
28 
"(P  Q)  R <> P  (Q  R)"]; 

29 

30 
val not_rews = map int_prove_fun 

1459  31 
["~ False <> True", "~ True <> False"]; 
0  32 

33 
val imp_rews = map int_prove_fun 

1459  34 
["(P > False) <> ~P", "(P > True) <> True", 
17480  35 
"(False > P) <> True", "(True > P) <> P", 
1459  36 
"(P > P) <> True", "(P > ~P) <> ~P"]; 
0  37 

38 
val iff_rews = map int_prove_fun 

1459  39 
["(True <> P) <> P", "(P <> True) <> P", 
0  40 
"(P <> P) <> True", 
1459  41 
"(False <> P) <> ~P", "(P <> False) <> ~P"]; 
0  42 

43 
val quant_rews = map int_prove_fun 

3836  44 
["(ALL x. P) <> P", "(EX x. P) <> P"]; 
0  45 

46 
(*These are NOT supplied by default!*) 

47 
val distrib_rews = map int_prove_fun 

48 
["~(PQ) <> ~P & ~Q", 

49 
"P & (Q  R) <> P&Q  P&R", "(Q  R) & P <> Q&P  R&P", 

50 
"(P  Q > R) <> (P > R) & (Q > R)", 

3836  51 
"~(EX x. NORM(P(x))) <> (ALL x. ~NORM(P(x)))", 
52 
"((EX x. NORM(P(x))) > Q) <> (ALL x. NORM(P(x)) > Q)", 

53 
"(EX x. NORM(P(x))) & NORM(Q) <> (EX x. NORM(P(x)) & NORM(Q))", 

54 
"NORM(Q) & (EX x. NORM(P(x))) <> (EX x. NORM(Q) & NORM(P(x)))"]; 

0  55 

56 
val P_Imp_P_iff_T = int_prove_fun_raw "p:P ==> ?p:(P <> True)"; 

57 

58 
fun make_iff_T th = th RS P_Imp_P_iff_T; 

59 

60 
val refl_iff_T = make_iff_T refl; 

61 

62 
val norm_thms = [(norm_eq RS sym, norm_eq), 

1459  63 
(NORM_iff RS iff_sym, NORM_iff)]; 
0  64 

65 

66 
(* Conversion into rewrite rules *) 

67 

68 
val not_P_imp_P_iff_F = int_prove_fun_raw "p:~P ==> ?p:(P <> False)"; 

69 

70 
fun mk_eq th = case concl_of th of 

71 
_ $ (Const("op <>",_)$_$_) $ _ => th 

72 
 _ $ (Const("op =",_)$_$_) $ _ => th 

17480  73 
 _ $ (Const("Not",_)$_) $ _ => th RS not_P_imp_P_iff_F 
0  74 
 _ => make_iff_T th; 
75 

5304  76 

77 
val mksimps_pairs = 

78 
[("op >", [mp]), ("op &", [conjunct1,conjunct2]), 

79 
("All", [spec]), ("True", []), ("False", [])]; 

0  80 

5304  81 
fun mk_atomize pairs = 
82 
let fun atoms th = 

83 
(case concl_of th of 

84 
Const("Trueprop",_) $ p => 

85 
(case head_of p of 

86 
Const(a,_) => 

17325  87 
(case AList.lookup (op =) pairs a of 
15570  88 
SOME(rls) => List.concat (map atoms ([th] RL rls)) 
15531  89 
 NONE => [th]) 
5304  90 
 _ => [th]) 
91 
 _ => [th]) 

92 
in atoms end; 

93 

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

0  95 

96 
(*destruct function for analysing equations*) 

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

98 
 dest_red t = raise TERM("FOL/dest_red", [t]); 

99 

100 
structure FOLP_SimpData : SIMP_DATA = 

101 
struct 

1459  102 
val refl_thms = [refl, iff_refl] 
103 
val trans_thms = [trans, iff_trans] 

104 
val red1 = iffD1 

105 
val red2 = iffD2 

106 
val mk_rew_rules = mk_rew_rules 

107 
val case_splits = [] (*NO IF'S!*) 

108 
val norm_thms = norm_thms 

109 
val subst_thms = [subst]; 

110 
val dest_red = dest_red 

0  111 
end; 
112 

113 
structure FOLP_Simp = SimpFun(FOLP_SimpData); 

114 

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

17480  116 
val FOLP_congs = 
0  117 
[all_cong,ex_cong,eq_cong, 
118 
conj_cong,disj_cong,imp_cong,iff_cong,not_cong] @ pred_congs; 

119 

120 
val IFOLP_rews = 

17480  121 
[refl_iff_T] @ conj_rews @ disj_rews @ not_rews @ 
0  122 
imp_rews @ iff_rews @ quant_rews; 
123 

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

124 
open FOLP_Simp; 
0  125 

126 
val auto_ss = empty_ss setauto ares_tac [TrueI]; 

127 

128 
val IFOLP_ss = auto_ss addcongs FOLP_congs addrews IFOLP_rews; 

129 

130 
(*Classical version...*) 

17480  131 
fun prove_fun s = 
132 
(writeln s; prove_goal (the_context ()) s 

0  133 
(fn prems => [ (cut_facts_tac prems 1), (Cla.fast_tac FOLP_cs 1) ])); 
134 

135 
val cla_rews = map prove_fun 

1459  136 
["?p:P  ~P", "?p:~P  P", 
137 
"?p:~ ~ P <> P", "?p:(~P > P) <> P"]; 

0  138 

139 
val FOLP_rews = IFOLP_rews@cla_rews; 

140 

141 
val FOLP_ss = auto_ss addcongs FOLP_congs addrews FOLP_rews; 