author  paulson 
Mon, 10 Feb 1997 12:52:11 +0100  
changeset 2603  4988dda71c0b 
parent 1463  49ca5e875691 
child 3836  f1a1817659e6 
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 

1463  6 
Simplification data for FOLP 
0  7 
*) 
8 

9 
(*** Rewrite rules ***) 

10 

11 
fun int_prove_fun_raw s = 

12 
(writeln s; prove_goal IFOLP.thy 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", 
35 
"(False > P) <> True", "(True > P) <> P", 

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 

1459  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)", 

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)))"]; 

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 

73 
 _ $ (Const("Not",_)$_) $ _ => th RS not_P_imp_P_iff_F 

74 
 _ => make_iff_T th; 

75 

76 
fun atomize th = case concl_of th of (*The operator below is "Proof $ P $ p"*) 

77 
_ $ (Const("op >",_) $ _ $ _) $ _ => atomize(th RS mp) 

78 
 _ $ (Const("op &",_) $ _ $ _) $ _ => atomize(th RS conjunct1) @ 

1459  79 
atomize(th RS conjunct2) 
0  80 
 _ $ (Const("All",_) $ _) $ _ => atomize(th RS spec) 
81 
 _ $ (Const("True",_)) $ _ => [] 

82 
 _ $ (Const("False",_)) $ _ => [] 

83 
 _ => [th]; 

84 

85 
fun mk_rew_rules th = map mk_eq (atomize th); 

86 

87 
(*destruct function for analysing equations*) 

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

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

90 

91 
structure FOLP_SimpData : SIMP_DATA = 

92 
struct 

1459  93 
val refl_thms = [refl, iff_refl] 
94 
val trans_thms = [trans, iff_trans] 

95 
val red1 = iffD1 

96 
val red2 = iffD2 

97 
val mk_rew_rules = mk_rew_rules 

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

99 
val norm_thms = norm_thms 

100 
val subst_thms = [subst]; 

101 
val dest_red = dest_red 

0  102 
end; 
103 

104 
structure FOLP_Simp = SimpFun(FOLP_SimpData); 

105 

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

107 
val FOLP_congs = 

108 
[all_cong,ex_cong,eq_cong, 

109 
conj_cong,disj_cong,imp_cong,iff_cong,not_cong] @ pred_congs; 

110 

111 
val IFOLP_rews = 

112 
[refl_iff_T] @ conj_rews @ disj_rews @ not_rews @ 

113 
imp_rews @ iff_rews @ quant_rews; 

114 

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

115 
open FOLP_Simp; 
0  116 

117 
val auto_ss = empty_ss setauto ares_tac [TrueI]; 

118 

119 
val IFOLP_ss = auto_ss addcongs FOLP_congs addrews IFOLP_rews; 

120 

121 
(*Classical version...*) 

122 
fun prove_fun s = 

123 
(writeln s; prove_goal FOLP.thy s 

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

125 

126 
val cla_rews = map prove_fun 

1459  127 
["?p:P  ~P", "?p:~P  P", 
128 
"?p:~ ~ P <> P", "?p:(~P > P) <> P"]; 

0  129 

130 
val FOLP_rews = IFOLP_rews@cla_rews; 

131 

132 
val FOLP_ss = auto_ss addcongs FOLP_congs addrews FOLP_rews; 

133 

134 