author  wenzelm 
Sun, 08 Jul 2007 19:51:58 +0200  
changeset 23655  d2d1138e0ddc 
parent 22822  c1a6a2159e69 
child 26288  89b9f7c18631 
permissions  rwrr 
9889  1 
(* Title: FOL/simpdata.ML 
0  2 
ID: $Id$ 
1459  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
282  4 
Copyright 1994 University of Cambridge 
0  5 

9889  6 
Simplification data for FOL. 
0  7 
*) 
8 

9 
(*** Rewrite rules ***) 

10 

10431  11 
fun int_prove_fun s = 
12 
(writeln s; 

21539  13 
prove_goal (theory "IFOL") s 
10431  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 

12038  17 
bind_thms ("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", 
12038  22 
"(P & Q) & R <> P & (Q & R)"]); 
0  23 

12038  24 
bind_thms ("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", 
12038  28 
"(P  Q)  R <> P  (Q  R)"]); 
0  29 

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

12038  34 
bind_thms ("imp_simps", map int_prove_fun 
1459  35 
["(P > False) <> ~P", "(P > True) <> True", 
10431  36 
"(False > P) <> True", "(True > P) <> P", 
12038  37 
"(P > P) <> True", "(P > ~P) <> ~P"]); 
0  38 

12038  39 
bind_thms ("iff_simps", map int_prove_fun 
1459  40 
["(True <> P) <> P", "(P <> True) <> P", 
0  41 
"(P <> P) <> True", 
12038  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*) 
12038  45 
bind_thms ("quant_simps", map int_prove_fun 
10431  46 
["(ALL x. P) <> P", 
4349
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", 
13149
773657d466cb
better simplification of trivial existential equalities
paulson
parents:
12825
diff
changeset

50 
"EX x. x=t", "EX x. t=x", 
10431  51 
"(EX x. x=t & P(x)) <> P(t)", 
12038  52 
"(EX x. t=x & P(x)) <> P(t)"]); 
0  53 

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

12038  55 
bind_thms ("distrib_simps", map int_prove_fun 
10431  56 
["P & (Q  R) <> P&Q  P&R", 
282  57 
"(Q  R) & P <> Q&P  R&P", 
12038  58 
"(P  Q > R) <> (P > R) & (Q > R)"]); 
0  59 

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

12038  62 
bind_thm ("P_iff_F", int_prove_fun "~P ==> (P <> False)"); 
63 
bind_thm ("iff_reflection_F", P_iff_F RS iff_reflection); 

282  64 

12038  65 
bind_thm ("P_iff_T", int_prove_fun "P ==> (P <> True)"); 
66 
bind_thm ("iff_reflection_T", P_iff_T RS iff_reflection); 

282  67 

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

5555  69 

282  70 
fun mk_meta_eq th = case concl_of th of 
5555  71 
_ $ (Const("op =",_)$_$_) => th RS eq_reflection 
72 
 _ $ (Const("op <>",_)$_$_) => th RS iff_reflection 

10431  73 
 _ => 
5555  74 
error("conclusion must be a =equality or <>");; 
75 

76 
fun mk_eq th = case concl_of th of 

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

77 
Const("==",_)$_$_ => th 
5555  78 
 _ $ (Const("op =",_)$_$_) => mk_meta_eq th 
79 
 _ $ (Const("op <>",_)$_$_) => mk_meta_eq th 

282  80 
 _ $ (Const("Not",_)$_) => th RS iff_reflection_F 
81 
 _ => th RS iff_reflection_T; 

0  82 

6114
45958e54d72e
congruence rules finally use == instead of = and <>
paulson
parents:
5555
diff
changeset

83 
(*Replace premises x=y, X<>Y by X==Y*) 
10431  84 
val mk_meta_prems = 
85 
rule_by_tactic 

21539  86 
(REPEAT_FIRST (resolve_tac [meta_eq_to_obj_eq, thm "def_imp_iff"])); 
6114
45958e54d72e
congruence rules finally use == instead of = and <>
paulson
parents:
5555
diff
changeset

87 

9713  88 
(*Congruence rules for = or <> (instead of ==)*) 
6114
45958e54d72e
congruence rules finally use == instead of = and <>
paulson
parents:
5555
diff
changeset

89 
fun mk_meta_cong rl = 
45958e54d72e
congruence rules finally use == instead of = and <>
paulson
parents:
5555
diff
changeset

90 
standard(mk_meta_eq (mk_meta_prems rl)) 
45958e54d72e
congruence rules finally use == instead of = and <>
paulson
parents:
5555
diff
changeset

91 
handle THM _ => 
45958e54d72e
congruence rules finally use == instead of = and <>
paulson
parents:
5555
diff
changeset

92 
error("Premises and conclusion of congruence rules must use =equality or <>"); 
5555  93 

5304  94 
val mksimps_pairs = 
95 
[("op >", [mp]), ("op &", [conjunct1,conjunct2]), 

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

97 

16019  98 
(* ###FIXME: move to simplifier.ML 
5304  99 
val mk_atomize: (string * thm list) list > thm > thm list 
100 
*) 

16019  101 
(* ###FIXME: move to simplifier.ML *) 
5304  102 
fun mk_atomize pairs = 
103 
let fun atoms th = 

104 
(case concl_of th of 

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

106 
(case head_of p of 

107 
Const(a,_) => 

17325  108 
(case AList.lookup (op =) pairs a of 
15570  109 
SOME(rls) => List.concat (map atoms ([th] RL rls)) 
15531  110 
 NONE => [th]) 
5304  111 
 _ => [th]) 
112 
 _ => [th]) 

113 
in atoms end; 

114 

12725  115 
fun mksimps pairs = (map mk_eq o mk_atomize pairs o gen_all); 
981  116 

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

117 
(*** Classical laws ***) 
282  118 

10431  119 
fun prove_fun s = 
120 
(writeln s; 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6391
diff
changeset

121 
prove_goal (the_context ()) s 
10431  122 
(fn prems => [ (cut_facts_tac prems 1), 
1459  123 
(Cla.fast_tac FOL_cs 1) ])); 
745  124 

10431  125 
(*Avoids duplication of subgoals after expand_if, when the true and false 
126 
cases boil down to the same thing.*) 

12038  127 
bind_thm ("cases_simp", prove_fun "(P > Q) & (~P > Q) <> Q"); 
1953  128 

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

129 

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

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

131 
We do NOT distribute of ALL over &, or dually that of EX over  
10431  132 
Baaz and Leitsch, On Skolemization and Proof Complexity (1994) 
4349
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

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

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

135 

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

136 
(*existential miniscoping*) 
12038  137 
bind_thms ("int_ex_simps", map int_prove_fun 
138 
["(EX x. P(x) & Q) <> (EX x. P(x)) & Q", 

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

140 
"(EX x. P(x)  Q) <> (EX x. P(x))  Q", 

141 
"(EX x. P  Q(x)) <> P  (EX x. Q(x))"]); 

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

142 

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

143 
(*classical rules*) 
12038  144 
bind_thms ("cla_ex_simps", map prove_fun 
145 
["(EX x. P(x) > Q) <> (ALL x. P(x)) > Q", 

146 
"(EX x. P > Q(x)) <> P > (EX x. Q(x))"]); 

0  147 

12038  148 
bind_thms ("ex_simps", int_ex_simps @ cla_ex_simps); 
4349
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

149 

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

150 
(*universal miniscoping*) 
12038  151 
bind_thms ("int_all_simps", map int_prove_fun 
152 
["(ALL x. P(x) & Q) <> (ALL x. P(x)) & Q", 

153 
"(ALL x. P & Q(x)) <> P & (ALL x. Q(x))", 

154 
"(ALL x. P(x) > Q) <> (EX x. P(x)) > Q", 

155 
"(ALL x. P > Q(x)) <> P > (ALL x. Q(x))"]); 

1953  156 

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

157 
(*classical rules*) 
12038  158 
bind_thms ("cla_all_simps", map prove_fun 
159 
["(ALL x. P(x)  Q) <> (ALL x. P(x))  Q", 

160 
"(ALL x. P  Q(x)) <> P  (ALL x. Q(x))"]); 

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

161 

12038  162 
bind_thms ("all_simps", int_all_simps @ cla_all_simps); 
4349
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

163 

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

164 

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

165 
(*** Named rewrite rules proved for IFOL ***) 
1953  166 

21539  167 
fun int_prove nm thm = qed_goal nm (theory "IFOL") thm 
10431  168 
(fn prems => [ (cut_facts_tac prems 1), 
2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2469
diff
changeset

169 
(IntPr.fast_tac 1) ]); 
1914  170 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6391
diff
changeset

171 
fun prove nm thm = qed_goal nm (the_context ()) thm (fn _ => [Blast_tac 1]); 
1914  172 

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

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

12038  175 
bind_thms ("conj_comms", [conj_commute, conj_left_commute]); 
1914  176 

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

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

12038  179 
bind_thms ("disj_comms", [disj_commute, disj_left_commute]); 
1914  180 

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

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

183 

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

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

186 

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

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

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

190 

3910  191 
prove "imp_disj1" "(P>Q)  R <> (P>Q  R)"; 
192 
prove "imp_disj2" "Q  (P>R) <> (P>Q  R)"; 

193 

1914  194 
int_prove "de_Morgan_disj" "(~(P  Q)) <> (~P & ~Q)"; 
195 
prove "de_Morgan_conj" "(~(P & Q)) <> (~P  ~Q)"; 

196 

12765  197 
prove "not_imp" "~(P > Q) <> (P & ~Q)"; 
1914  198 
prove "not_iff" "~(P <> Q) <> (P <> ~Q)"; 
199 

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

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

1914  203 
int_prove "imp_ex" "((EX x. P(x)) > Q) <> (ALL x. P(x) > Q)"; 
204 

205 
int_prove "ex_disj_distrib" 

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

207 
int_prove "all_conj_distrib" 

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

209 

210 

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

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

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

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

214 
(*abstract syntax*) 
15531  215 
fun dest_eq((c as Const("op =",_)) $ s $ t) = SOME(c,s,t) 
216 
 dest_eq _ = NONE; 

217 
fun dest_conj((c as Const("op &",_)) $ s $ t) = SOME(c,s,t) 

218 
 dest_conj _ = NONE; 

219 
fun dest_imp((c as Const("op >",_)) $ s $ t) = SOME(c,s,t) 

220 
 dest_imp _ = NONE; 

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

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

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

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

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

225 
val iffI = iffI 
12526
1b9db2581fe2
mods due to changed 1point simprocs (quantifier1).
nipkow
parents:
12038
diff
changeset

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

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

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

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

230 
val mp = mp 
21539  231 
val uncurry = thm "uncurry" 
4349
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

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

233 
val exE = exE 
21539  234 
val iff_allI = thm "iff_allI" 
235 
val iff_exI = thm "iff_exI" 

236 
val all_comm = thm "all_comm" 

237 
val ex_comm = thm "ex_comm" 

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

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

239 

13462  240 
val defEX_regroup = 
17002  241 
Simplifier.simproc (the_context ()) 
13462  242 
"defined EX" ["EX x. P(x)"] Quantifier1.rearrange_ex; 
4349
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

243 

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

244 
val defALL_regroup = 
17002  245 
Simplifier.simproc (the_context ()) 
13462  246 
"defined ALL" ["ALL x. P(x)"] Quantifier1.rearrange_all; 
4349
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset

247 

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

248 

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

249 
(*** Case splitting ***) 
0  250 

5304  251 
structure SplitterData = 
252 
struct 

253 
structure Simplifier = Simplifier 

5555  254 
val mk_eq = mk_eq 
5304  255 
val meta_eq_to_iff = meta_eq_to_iff 
256 
val iffD = iffD2 

257 
val disjE = disjE 

258 
val conjE = conjE 

259 
val exE = exE 

21539  260 
val contrapos = thm "contrapos" 
261 
val contrapos2 = thm "contrapos2" 

262 
val notnotD = thm "notnotD" 

5304  263 
end; 
1722  264 

5304  265 
structure Splitter = SplitterFun(SplitterData); 
1722  266 

5304  267 
val split_tac = Splitter.split_tac; 
268 
val split_inside_tac = Splitter.split_inside_tac; 

269 
val split_asm_tac = Splitter.split_asm_tac; 

5307  270 
val op addsplits = Splitter.addsplits; 
271 
val op delsplits = Splitter.delsplits; 

5304  272 
val Addsplits = Splitter.Addsplits; 
273 
val Delsplits = Splitter.Delsplits; 

4325  274 

275 

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

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

277 

12038  278 
bind_thms ("meta_simps", 
279 
[triv_forall_equality, (* prunes params *) 

21539  280 
thm "True_implies_equals"]); (* prune asms `True' *) 
5496  281 

12038  282 
bind_thms ("IFOL_simps", 
283 
[refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 

284 
imp_simps @ iff_simps @ quant_simps); 

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

285 

12038  286 
bind_thm ("notFalseI", int_prove_fun "~False"); 
21539  287 
bind_thms ("triv_rls", 
288 
[TrueI, refl, reflexive_thm, iff_refl, thm "notFalseI"]); 

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

289 

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

290 
fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls@prems), 
9713  291 
atac, etac FalseE]; 
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

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

293 
fun safe_solver prems = FIRST'[match_tac (triv_rls@prems), 
9713  294 
eq_assume_tac, ematch_tac [FalseE]]; 
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

295 

3910  296 
(*No simprules, but basic infastructure for simplification*) 
17892  297 
val FOL_basic_ss = 
298 
Simplifier.theory_context (the_context ()) empty_ss 

10431  299 
setsubgoaler asm_simp_tac 
300 
setSSolver (mk_solver "FOL safe" safe_solver) 

301 
setSolver (mk_solver "FOL unsafe" unsafe_solver) 

302 
setmksimps (mksimps mksimps_pairs) 

303 
setmkcong mk_meta_cong; 

5304  304 

18324  305 
fun unfold_tac ths = 
306 
let val ss0 = Simplifier.clear_ss FOL_basic_ss addsimps ths 

307 
in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end; 

17002  308 

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

309 

3910  310 
(*intuitionistic simprules only*) 
21539  311 
val IFOL_ss = 
312 
FOL_basic_ss 

10431  313 
addsimps (meta_simps @ IFOL_simps @ int_ex_simps @ int_all_simps) 
314 
addsimprocs [defALL_regroup, defEX_regroup] 

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

316 

12038  317 
bind_thms ("cla_simps", 
318 
[de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, 

12825  319 
not_imp, not_all, not_ex, cases_simp] @ 
12038  320 
map prove_fun 
321 
["~(P&Q) <> ~P  ~Q", 

322 
"P  ~P", "~P  P", 

323 
"~ ~ P <> P", "(~P > P) <> P", 

324 
"(~P <> ~Q) <> (P<>Q)"]); 

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

325 

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

327 
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

328 

18708  329 
val simpsetup = (fn thy => (change_simpset_of thy (fn _ => FOL_ss); thy)); 
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

330 

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

331 

5219  332 
(*** integration of simplifier with classical reasoner ***) 
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

333 

5219  334 
structure Clasimp = ClasimpFun 
8472  335 
(structure Simplifier = Simplifier and Splitter = Splitter 
9851  336 
and Classical = Cla and Blast = Blast 
18529  337 
val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE); 
4652
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
4649
diff
changeset

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

339 

22128  340 
ML_Context.value_antiq "clasimpset" 
341 
(Scan.succeed ("clasimpset", "Clasimp.local_clasimpset_of (ML_Context.the_local_context ())")); 

342 

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

343 
val FOL_css = (FOL_cs, FOL_ss); 