author  paulson 
Thu, 02 Jul 1998 17:56:06 +0200  
changeset 5115  caf39b7b7a12 
parent 4930  89271bc4e7ed 
child 5219  924359415f09 
permissions  rwrr 
1459  1 
(* Title: FOL/simpdata 
0  2 
ID: $Id$ 
1459  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
282  4 
Copyright 1994 University of Cambridge 
0  5 

6 
Simplification data for FOL 

7 
*) 

8 

9 
(*** Rewrite rules ***) 

10 

11 
fun int_prove_fun s = 

282  12 
(writeln s; 
13 
prove_goal IFOL.thy s 

14 
(fn prems => [ (cut_facts_tac prems 1), 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2469
diff
changeset

15 
(IntPr.fast_tac 1) ])); 
0  16 

1953  17 
val conj_simps = map int_prove_fun 
1459  18 
["P & True <> P", "True & P <> P", 
0  19 
"P & False <> False", "False & P <> False", 
2801  20 
"P & P <> P", "P & P & Q <> P & Q", 
1459  21 
"P & ~P <> False", "~P & P <> False", 
0  22 
"(P & Q) & R <> P & (Q & R)"]; 
23 

1953  24 
val disj_simps = map int_prove_fun 
1459  25 
["P  True <> True", "True  P <> True", 
26 
"P  False <> P", "False  P <> P", 

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

1953  30 
val not_simps = map int_prove_fun 
282  31 
["~(PQ) <> ~P & ~Q", 
1459  32 
"~ False <> True", "~ True <> False"]; 
0  33 

1953  34 
val imp_simps = map int_prove_fun 
1459  35 
["(P > False) <> ~P", "(P > True) <> True", 
36 
"(False > P) <> True", "(True > P) <> P", 

37 
"(P > P) <> True", "(P > ~P) <> ~P"]; 

0  38 

1953  39 
val iff_simps = map int_prove_fun 
1459  40 
["(True <> P) <> P", "(P <> True) <> P", 
0  41 
"(P <> P) <> True", 
1459  42 
"(False <> P) <> ~P", "(P <> False) <> ~P"]; 
0  43 

4349
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

44 
(*The x=t versions are needed for the simplification procedures*) 
1953  45 
val quant_simps = map int_prove_fun 
4349
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

46 
["(ALL x. P) <> P", 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

47 
"(ALL x. x=t > P(x)) <> P(t)", 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

48 
"(ALL x. t=x > P(x)) <> P(t)", 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

49 
"(EX x. P) <> P", 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

50 
"(EX x. x=t & P(x)) <> P(t)", 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

51 
"(EX x. t=x & P(x)) <> P(t)"]; 
0  52 

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

1953  54 
val distrib_simps = map int_prove_fun 
282  55 
["P & (Q  R) <> P&Q  P&R", 
56 
"(Q  R) & P <> Q&P  R&P", 

0  57 
"(P  Q > R) <> (P > R) & (Q > R)"]; 
58 

282  59 
(** Conversion into rewrite rules **) 
0  60 

53  61 
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th; 
62 

282  63 
(*Make atomic rewrite rules*) 
429
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset

64 
fun atomize r = 
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset

65 
case concl_of r of 
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset

66 
Const("Trueprop",_) $ p => 
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset

67 
(case p of 
1459  68 
Const("op >",_)$_$_ => atomize(r RS mp) 
429
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset

69 
 Const("op &",_)$_$_ => atomize(r RS conjunct1) @ 
1459  70 
atomize(r RS conjunct2) 
429
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset

71 
 Const("All",_)$_ => atomize(r RS spec) 
1459  72 
 Const("True",_) => [] (*True is DELETED*) 
73 
 Const("False",_) => [] (*should False do something?*) 

429
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset

74 
 _ => [r]) 
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset

75 
 _ => [r]; 
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset

76 

282  77 

78 
val P_iff_F = int_prove_fun "~P ==> (P <> False)"; 

79 
val iff_reflection_F = P_iff_F RS iff_reflection; 

80 

81 
val P_iff_T = int_prove_fun "P ==> (P <> True)"; 

82 
val iff_reflection_T = P_iff_T RS iff_reflection; 

83 

84 
(*Make metaequalities. The operator below is Trueprop*) 

85 
fun mk_meta_eq th = case concl_of th of 

394
432bb9995893
Modified mk_meta_eq to leave metaequlities on unchanged.
nipkow
parents:
371
diff
changeset

86 
Const("==",_)$_$_ => th 
432bb9995893
Modified mk_meta_eq to leave metaequlities on unchanged.
nipkow
parents:
371
diff
changeset

87 
 _ $ (Const("op =",_)$_$_) => th RS eq_reflection 
282  88 
 _ $ (Const("op <>",_)$_$_) => th RS iff_reflection 
89 
 _ $ (Const("Not",_)$_) => th RS iff_reflection_F 

90 
 _ => th RS iff_reflection_T; 

0  91 

981  92 

2074
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

93 
(*** Classical laws ***) 
282  94 

0  95 
fun prove_fun s = 
282  96 
(writeln s; 
97 
prove_goal FOL.thy s 

98 
(fn prems => [ (cut_facts_tac prems 1), 

1459  99 
(Cla.fast_tac FOL_cs 1) ])); 
745  100 

1953  101 
(*Avoids duplication of subgoals after expand_if, when the true and false 
102 
cases boil down to the same thing.*) 

103 
val cases_simp = prove_fun "(P > Q) & (~P > Q) <> Q"; 

104 

4349
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

105 

50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

106 
(*** Miniscoping: pushing quantifiers in 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

107 
We do NOT distribute of ALL over &, or dually that of EX over  
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

108 
Baaz and Leitsch, On Skolemization and Proof Complexity (1994) 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

109 
show that this step can increase proof length! 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

110 
***) 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

111 

50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

112 
(*existential miniscoping*) 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

113 
val int_ex_simps = map int_prove_fun 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

114 
["(EX x. P(x) & Q) <> (EX x. P(x)) & Q", 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

115 
"(EX x. P & Q(x)) <> P & (EX x. Q(x))", 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

116 
"(EX x. P(x)  Q) <> (EX x. P(x))  Q", 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

117 
"(EX x. P  Q(x)) <> P  (EX x. Q(x))"]; 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

118 

50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

119 
(*classical rules*) 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

120 
val cla_ex_simps = map prove_fun 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

121 
["(EX x. P(x) > Q) <> (ALL x. P(x)) > Q", 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

122 
"(EX x. P > Q(x)) <> P > (EX x. Q(x))"]; 
0  123 

4349
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

124 
val ex_simps = int_ex_simps @ cla_ex_simps; 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

125 

50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

126 
(*universal miniscoping*) 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

127 
val int_all_simps = map int_prove_fun 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

128 
["(ALL x. P(x) & Q) <> (ALL x. P(x)) & Q", 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

129 
"(ALL x. P & Q(x)) <> P & (ALL x. Q(x))", 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

130 
"(ALL x. P(x) > Q) <> (EX x. P(x)) > Q", 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

131 
"(ALL x. P > Q(x)) <> P > (ALL x. Q(x))"]; 
1953  132 

4349
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

133 
(*classical rules*) 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

134 
val cla_all_simps = map prove_fun 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

135 
["(ALL x. P(x)  Q) <> (ALL x. P(x))  Q", 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

136 
"(ALL x. P  Q(x)) <> P  (ALL x. Q(x))"]; 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

137 

50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

138 
val all_simps = int_all_simps @ cla_all_simps; 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

139 

50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

140 

50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

141 
(*** Named rewrite rules proved for IFOL ***) 
1953  142 

1914  143 
fun int_prove nm thm = qed_goal nm IFOL.thy thm 
144 
(fn prems => [ (cut_facts_tac prems 1), 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2469
diff
changeset

145 
(IntPr.fast_tac 1) ]); 
1914  146 

3910  147 
fun prove nm thm = qed_goal nm FOL.thy thm (fn _ => [Blast_tac 1]); 
1914  148 

149 
int_prove "conj_commute" "P&Q <> Q&P"; 

150 
int_prove "conj_left_commute" "P&(Q&R) <> Q&(P&R)"; 

151 
val conj_comms = [conj_commute, conj_left_commute]; 

152 

153 
int_prove "disj_commute" "PQ <> QP"; 

154 
int_prove "disj_left_commute" "P(QR) <> Q(PR)"; 

155 
val disj_comms = [disj_commute, disj_left_commute]; 

156 

157 
int_prove "conj_disj_distribL" "P&(QR) <> (P&Q  P&R)"; 

158 
int_prove "conj_disj_distribR" "(PQ)&R <> (P&R  Q&R)"; 

159 

160 
int_prove "disj_conj_distribL" "P(Q&R) <> (PQ) & (PR)"; 

161 
int_prove "disj_conj_distribR" "(P&Q)R <> (PR) & (QR)"; 

162 

163 
int_prove "imp_conj_distrib" "(P > (Q&R)) <> (P>Q) & (P>R)"; 

164 
int_prove "imp_conj" "((P&Q)>R) <> (P > (Q > R))"; 

165 
int_prove "imp_disj" "(PQ > R) <> (P>R) & (Q>R)"; 

166 

3910  167 
prove "imp_disj1" "(P>Q)  R <> (P>Q  R)"; 
168 
prove "imp_disj2" "Q  (P>R) <> (P>Q  R)"; 

169 

1914  170 
int_prove "de_Morgan_disj" "(~(P  Q)) <> (~P & ~Q)"; 
171 
prove "de_Morgan_conj" "(~(P & Q)) <> (~P  ~Q)"; 

172 

173 
prove "not_iff" "~(P <> Q) <> (P <> ~Q)"; 

174 

3835  175 
prove "not_all" "(~ (ALL x. P(x))) <> (EX x.~P(x))"; 
176 
prove "imp_all" "((ALL x. P(x)) > Q) <> (EX x. P(x) > Q)"; 

177 
int_prove "not_ex" "(~ (EX x. P(x))) <> (ALL x.~P(x))"; 

1914  178 
int_prove "imp_ex" "((EX x. P(x)) > Q) <> (ALL x. P(x) > Q)"; 
179 

180 
int_prove "ex_disj_distrib" 

181 
"(EX x. P(x)  Q(x)) <> ((EX x. P(x))  (EX x. Q(x)))"; 

182 
int_prove "all_conj_distrib" 

183 
"(ALL x. P(x) & Q(x)) <> ((ALL x. P(x)) & (ALL x. Q(x)))"; 

184 

185 

1088
fc4fb6e8a636
Imported meta_eq_to_obj_eq from HOL for use with 'split'.
lcp
parents:
981
diff
changeset

186 
(*Used in ZF, perhaps elsewhere?*) 
fc4fb6e8a636
Imported meta_eq_to_obj_eq from HOL for use with 'split'.
lcp
parents:
981
diff
changeset

187 
val meta_eq_to_obj_eq = prove_goal IFOL.thy "x==y ==> x=y" 
fc4fb6e8a636
Imported meta_eq_to_obj_eq from HOL for use with 'split'.
lcp
parents:
981
diff
changeset

188 
(fn [prem] => [rewtac prem, rtac refl 1]); 
fc4fb6e8a636
Imported meta_eq_to_obj_eq from HOL for use with 'split'.
lcp
parents:
981
diff
changeset

189 

4349
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

190 

50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

191 
(** make simplification procedures for quantifier elimination **) 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

192 
structure Quantifier1 = Quantifier1Fun( 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

193 
struct 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

194 
(*abstract syntax*) 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

195 
fun dest_eq((c as Const("op =",_)) $ s $ t) = Some(c,s,t) 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

196 
 dest_eq _ = None; 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

197 
fun dest_conj((c as Const("op &",_)) $ s $ t) = Some(c,s,t) 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

198 
 dest_conj _ = None; 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

199 
val conj = FOLogic.conj 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

200 
val imp = FOLogic.imp 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

201 
(*rules*) 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

202 
val iff_reflection = iff_reflection 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

203 
val iffI = iffI 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

204 
val sym = sym 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

205 
val conjI= conjI 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

206 
val conjE= conjE 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

207 
val impI = impI 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

208 
val impE = impE 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

209 
val mp = mp 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

210 
val exI = exI 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

211 
val exE = exE 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

212 
val allI = allI 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

213 
val allE = allE 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

214 
end); 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

215 

50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

216 
local 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

217 
val ex_pattern = 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

218 
read_cterm (sign_of FOL.thy) ("EX x. P(x) & Q(x)", FOLogic.oT) 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

219 

50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

220 
val all_pattern = 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

221 
read_cterm (sign_of FOL.thy) ("ALL x. P(x) & P'(x) > Q(x)", FOLogic.oT) 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

222 

50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

223 
in 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

224 
val defEX_regroup = 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

225 
mk_simproc "defined EX" [ex_pattern] Quantifier1.rearrange_ex; 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

226 
val defALL_regroup = 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

227 
mk_simproc "defined ALL" [all_pattern] Quantifier1.rearrange_all; 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

228 
end; 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

229 

50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

230 

50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

231 
(*** Case splitting ***) 
0  232 

1088
fc4fb6e8a636
Imported meta_eq_to_obj_eq from HOL for use with 'split'.
lcp
parents:
981
diff
changeset

233 
qed_goal "meta_iffD" IFOL.thy "[ P==Q; Q ] ==> P" 
756  234 
(fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]); 
282  235 

942  236 
local val mktac = mk_case_split_tac meta_iffD 
237 
in 

238 
fun split_tac splits = mktac (map mk_meta_eq splits) 

239 
end; 

1722  240 

241 
local val mktac = mk_case_split_inside_tac meta_iffD 

242 
in 

243 
fun split_inside_tac splits = mktac (map mk_meta_eq splits) 

244 
end; 

245 

4203  246 
val split_asm_tac = mk_case_split_asm_tac split_tac 
247 
(disjE,conjE,exE,contrapos,contrapos2,notnotD); 

1722  248 

4325  249 

250 

2074
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

251 
(*** Standard simpsets ***) 
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

252 

30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

253 
structure Induction = InductionFun(struct val spec=IFOL.spec end); 
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

254 

4349
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

255 
open Induction; 
2074
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

256 

30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

257 
(*Add congruence rules for = or <> (instead of ==) *) 
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

258 
infix 4 addcongs delcongs; 
2074
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

259 
fun ss addcongs congs = 
3566  260 
ss addeqcongs (map standard (congs RL [eq_reflection,iff_reflection])); 
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

261 
fun ss delcongs congs = 
3566  262 
ss deleqcongs (map standard (congs RL [eq_reflection,iff_reflection])); 
2469  263 

4094  264 
fun Addcongs congs = (simpset_ref() := simpset() addcongs congs); 
265 
fun Delcongs congs = (simpset_ref() := simpset() delcongs congs); 

2074
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

266 

5115  267 
(** FIXME: this is a PATCH until similar code in Provers/splitter is 
268 
generalized **) 

269 

270 
fun split_format_err() = error("Wrong format for split rule"); 

271 

272 
fun split_thm_info thm = 

273 
(case concl_of thm of 

274 
Const("Trueprop",_) $ (Const("op <>", _)$(Var _$t)$c) => 

275 
(case strip_comb t of 

276 
(Const(a,_),_) => (a,case c of (Const("Not",_)$_)=> true _=> false) 

277 
 _ => split_format_err()) 

278 
 _ => split_format_err()); 

279 

4930
89271bc4e7ed
extended addsplits and delsplits to handle also split rules for assumptions
oheimb
parents:
4794
diff
changeset

280 
infix 4 addsplits delsplits; 
4669  281 
fun ss addsplits splits = 
4930
89271bc4e7ed
extended addsplits and delsplits to handle also split rules for assumptions
oheimb
parents:
4794
diff
changeset

282 
let fun addsplit (ss,split) = 
89271bc4e7ed
extended addsplits and delsplits to handle also split rules for assumptions
oheimb
parents:
4794
diff
changeset

283 
let val (name,asm) = split_thm_info split 
5115  284 
in ss addloop ("split "^ name ^ (if asm then " asm" else ""), 
4930
89271bc4e7ed
extended addsplits and delsplits to handle also split rules for assumptions
oheimb
parents:
4794
diff
changeset

285 
(if asm then split_asm_tac else split_tac) [split]) end 
4669  286 
in foldl addsplit (ss,splits) end; 
4325  287 

4930
89271bc4e7ed
extended addsplits and delsplits to handle also split rules for assumptions
oheimb
parents:
4794
diff
changeset

288 
fun ss delsplits splits = 
89271bc4e7ed
extended addsplits and delsplits to handle also split rules for assumptions
oheimb
parents:
4794
diff
changeset

289 
let fun delsplit(ss,split) = 
89271bc4e7ed
extended addsplits and delsplits to handle also split rules for assumptions
oheimb
parents:
4794
diff
changeset

290 
let val (name,asm) = split_thm_info split 
5115  291 
in ss delloop ("split "^ name ^ (if asm then " asm" else "")) end 
4930
89271bc4e7ed
extended addsplits and delsplits to handle also split rules for assumptions
oheimb
parents:
4794
diff
changeset

292 
in foldl delsplit (ss,splits) end; 
89271bc4e7ed
extended addsplits and delsplits to handle also split rules for assumptions
oheimb
parents:
4794
diff
changeset

293 

5115  294 
fun Addsplits splits = (simpset_ref() := simpset() addsplits splits); 
295 
fun Delsplits splits = (simpset_ref() := simpset() delsplits splits); 

296 

2074
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

297 
val IFOL_simps = 
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

298 
[refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

299 
imp_simps @ iff_simps @ quant_simps; 
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

300 

30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

301 
val notFalseI = int_prove_fun "~False"; 
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

302 
val triv_rls = [TrueI,refl,iff_refl,notFalseI]; 
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

303 

2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

304 
fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls@prems), 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

305 
atac, etac FalseE]; 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

306 
(*No premature instantiation of variables during simplification*) 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

307 
fun safe_solver prems = FIRST'[match_tac (triv_rls@prems), 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

308 
eq_assume_tac, ematch_tac [FalseE]]; 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

309 

3910  310 
(*No simprules, but basic infastructure for simplification*) 
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

311 
val FOL_basic_ss = empty_ss setsubgoaler asm_simp_tac 
4349
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

312 
addsimprocs [defALL_regroup,defEX_regroup] 
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

313 
setSSolver safe_solver 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

314 
setSolver unsafe_solver 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

315 
setmksimps (map mk_meta_eq o atomize o gen_all); 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

316 

3910  317 
(*intuitionistic simprules only*) 
4349
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

318 
val IFOL_ss = FOL_basic_ss addsimps (IFOL_simps @ int_ex_simps @ int_all_simps) 
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

319 
addcongs [imp_cong]; 
2074
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

320 

30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

321 
val cla_simps = 
3910  322 
[de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, 
323 
not_all, not_ex, cases_simp] @ 

2074
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

324 
map prove_fun 
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

325 
["~(P&Q) <> ~P  ~Q", 
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

326 
"P  ~P", "~P  P", 
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

327 
"~ ~ P <> P", "(~P > P) <> P", 
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

328 
"(~P <> ~Q) <> (P<>Q)"]; 
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

329 

3910  330 
(*classical simprules too*) 
4349
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

331 
val FOL_ss = IFOL_ss addsimps (cla_simps @ cla_ex_simps @ cla_all_simps); 
2074
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

332 

4094  333 
simpset_ref() := FOL_ss; 
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

334 

37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

335 

37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

336 

4652
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
4649
diff
changeset

337 

d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
4649
diff
changeset

338 

d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
4649
diff
changeset

339 

d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
4649
diff
changeset

340 

2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

341 
(*** Integration of simplifier with classical reasoner ***) 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

342 

37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

343 
(* rot_eq_tac rotates the first equality premise of subgoal i to the front, 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

344 
fails if there is no equaliy or if an equality is already at the front *) 
3537  345 
local 
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

346 
fun is_eq (Const ("Trueprop", _) $ (Const("op =" ,_) $ _ $ _)) = true 
3537  347 
 is_eq (Const ("Trueprop", _) $ (Const("op <>",_) $ _ $ _)) = true 
348 
 is_eq _ = false; 

4188
1025a27b08f9
changed libraray function find to find_index_eq, currying it
oheimb
parents:
4094
diff
changeset

349 
val find_eq = find_index is_eq; 
3537  350 
in 
351 
val rot_eq_tac = 

4188
1025a27b08f9
changed libraray function find to find_index_eq, currying it
oheimb
parents:
4094
diff
changeset

352 
SUBGOAL (fn (Bi,i) => let val n = find_eq (Logic.strip_assums_hyp Bi) in 
1025a27b08f9
changed libraray function find to find_index_eq, currying it
oheimb
parents:
4094
diff
changeset

353 
if n>0 then rotate_tac n i else no_tac end) 
3537  354 
end; 
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

355 

4652
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
4649
diff
changeset

356 
use "$ISABELLE_HOME/src/Provers/clasimp.ML"; 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
4649
diff
changeset

357 
open Clasimp; 
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

358 

37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

359 
val FOL_css = (FOL_cs, FOL_ss); 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

360 