author  wenzelm 
Sat, 01 Jul 2000 19:55:22 +0200  
changeset 9230  17ae63f82ad8 
parent 8643  331f0c75e3dc 
child 9300  ee5c9672d208 
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 

5496  9 
(* Elimination of True from asumptions: *) 
10 

11 
val True_implies_equals = prove_goal IFOL.thy 

12 
"(True ==> PROP P) == PROP P" 

13 
(K [rtac equal_intr_rule 1, atac 2, 

14 
METAHYPS (fn prems => resolve_tac prems 1) 1, 

15 
rtac TrueI 1]); 

16 

17 

0  18 
(*** Rewrite rules ***) 
19 

20 
fun int_prove_fun s = 

282  21 
(writeln s; 
22 
prove_goal IFOL.thy s 

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

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

24 
(IntPr.fast_tac 1) ])); 
0  25 

1953  26 
val conj_simps = map int_prove_fun 
1459  27 
["P & True <> P", "True & P <> P", 
0  28 
"P & False <> False", "False & P <> False", 
2801  29 
"P & P <> P", "P & P & Q <> P & Q", 
1459  30 
"P & ~P <> False", "~P & P <> False", 
0  31 
"(P & Q) & R <> P & (Q & R)"]; 
32 

1953  33 
val disj_simps = map int_prove_fun 
1459  34 
["P  True <> True", "True  P <> True", 
35 
"P  False <> P", "False  P <> P", 

2801  36 
"P  P <> P", "P  P  Q <> P  Q", 
0  37 
"(P  Q)  R <> P  (Q  R)"]; 
38 

1953  39 
val not_simps = map int_prove_fun 
282  40 
["~(PQ) <> ~P & ~Q", 
1459  41 
"~ False <> True", "~ True <> False"]; 
0  42 

1953  43 
val imp_simps = map int_prove_fun 
1459  44 
["(P > False) <> ~P", "(P > True) <> True", 
45 
"(False > P) <> True", "(True > P) <> P", 

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

0  47 

1953  48 
val iff_simps = map int_prove_fun 
1459  49 
["(True <> P) <> P", "(P <> True) <> P", 
0  50 
"(P <> P) <> True", 
1459  51 
"(False <> P) <> ~P", "(P <> False) <> ~P"]; 
0  52 

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

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

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

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

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

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

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

60 
"(EX x. t=x & P(x)) <> P(t)"]; 
0  61 

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

1953  63 
val distrib_simps = map int_prove_fun 
282  64 
["P & (Q  R) <> P&Q  P&R", 
65 
"(Q  R) & P <> Q&P  R&P", 

0  66 
"(P  Q > R) <> (P > R) & (Q > R)"]; 
67 

282  68 
(** Conversion into rewrite rules **) 
0  69 

53  70 
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th; 
71 

282  72 
val P_iff_F = int_prove_fun "~P ==> (P <> False)"; 
73 
val iff_reflection_F = P_iff_F RS iff_reflection; 

74 

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

76 
val iff_reflection_T = P_iff_T RS iff_reflection; 

77 

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

5555  79 

282  80 
fun mk_meta_eq th = case concl_of th of 
5555  81 
_ $ (Const("op =",_)$_$_) => th RS eq_reflection 
82 
 _ $ (Const("op <>",_)$_$_) => th RS iff_reflection 

83 
 _ => 

84 
error("conclusion must be a =equality or <>");; 

85 

86 
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

87 
Const("==",_)$_$_ => th 
5555  88 
 _ $ (Const("op =",_)$_$_) => mk_meta_eq th 
89 
 _ $ (Const("op <>",_)$_$_) => mk_meta_eq th 

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

0  92 

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

93 
(*Replace premises x=y, X<>Y by X==Y*) 
45958e54d72e
congruence rules finally use == instead of = and <>
paulson
parents:
5555
diff
changeset

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

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

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

97 

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

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

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

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

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

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

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

106 

5555  107 
(* ###FIXME: move to Provers/simplifier.ML 
5304  108 
val mk_atomize: (string * thm list) list > thm > thm list 
109 
*) 

5555  110 
(* ###FIXME: move to Provers/simplifier.ML *) 
5304  111 
fun mk_atomize pairs = 
112 
let fun atoms th = 

113 
(case concl_of th of 

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

115 
(case head_of p of 

116 
Const(a,_) => 

117 
(case assoc(pairs,a) of 

118 
Some(rls) => flat (map atoms ([th] RL rls)) 

119 
 None => [th]) 

120 
 _ => [th]) 

121 
 _ => [th]) 

122 
in atoms end; 

123 

5555  124 
fun mksimps pairs = (map mk_eq o mk_atomize pairs o gen_all); 
981  125 

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

126 
(*** Classical laws ***) 
282  127 

0  128 
fun prove_fun s = 
282  129 
(writeln s; 
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6391
diff
changeset

130 
prove_goal (the_context ()) s 
282  131 
(fn prems => [ (cut_facts_tac prems 1), 
1459  132 
(Cla.fast_tac FOL_cs 1) ])); 
745  133 

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

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

137 

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

138 

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

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

140 
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

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

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

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

144 

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

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

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

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

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

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

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

151 

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

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

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

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

155 
"(EX x. P > Q(x)) <> P > (EX x. Q(x))"]; 
0  156 

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

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

158 

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

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

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

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

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

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

164 
"(ALL x. P > Q(x)) <> P > (ALL x. Q(x))"]; 
1953  165 

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

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

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

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

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

170 

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

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

172 

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

173 

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

174 
(*** Named rewrite rules proved for IFOL ***) 
1953  175 

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

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

178 
(IntPr.fast_tac 1) ]); 
1914  179 

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

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

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

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

184 
val conj_comms = [conj_commute, conj_left_commute]; 

185 

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

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

188 
val disj_comms = [disj_commute, disj_left_commute]; 

189 

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

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

192 

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

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

195 

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

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

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

199 

3910  200 
prove "imp_disj1" "(P>Q)  R <> (P>Q  R)"; 
201 
prove "imp_disj2" "Q  (P>R) <> (P>Q  R)"; 

202 

1914  203 
int_prove "de_Morgan_disj" "(~(P  Q)) <> (~P & ~Q)"; 
204 
prove "de_Morgan_conj" "(~(P & Q)) <> (~P  ~Q)"; 

205 

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

207 

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

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

1914  211 
int_prove "imp_ex" "((EX x. P(x)) > Q) <> (ALL x. P(x) > Q)"; 
212 

213 
int_prove "ex_disj_distrib" 

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

215 
int_prove "all_conj_distrib" 

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

217 

218 

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

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

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

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

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

223 
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

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

225 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

242 
end); 
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 
local 
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6391
diff
changeset

245 

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

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

247 
read_cterm (Theory.sign_of (the_context ())) ("EX x. P(x) & Q(x)", FOLogic.oT) 
4349
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 
val all_pattern = 
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6391
diff
changeset

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

251 

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

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

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

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

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

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

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

258 

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

259 

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

260 
(*** Case splitting ***) 
0  261 

5304  262 
val meta_eq_to_iff = prove_goal IFOL.thy "x==y ==> x<>y" 
263 
(fn [prem] => [rewtac prem, rtac iffI 1, atac 1, atac 1]); 

1722  264 

5304  265 
structure SplitterData = 
266 
struct 

267 
structure Simplifier = Simplifier 

5555  268 
val mk_eq = mk_eq 
5304  269 
val meta_eq_to_iff = meta_eq_to_iff 
270 
val iffD = iffD2 

271 
val disjE = disjE 

272 
val conjE = conjE 

273 
val exE = exE 

274 
val contrapos = contrapos 

275 
val contrapos2 = contrapos2 

276 
val notnotD = notnotD 

277 
end; 

1722  278 

5304  279 
structure Splitter = SplitterFun(SplitterData); 
1722  280 

5304  281 
val split_tac = Splitter.split_tac; 
282 
val split_inside_tac = Splitter.split_inside_tac; 

283 
val split_asm_tac = Splitter.split_asm_tac; 

5307  284 
val op addsplits = Splitter.addsplits; 
285 
val op delsplits = Splitter.delsplits; 

5304  286 
val Addsplits = Splitter.Addsplits; 
287 
val Delsplits = Splitter.Delsplits; 

4325  288 

289 

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

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

291 

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

292 
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

293 

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

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

295 

5555  296 

297 
(* Add congruence rules for = or <> (instead of ==) *) 

298 

299 
(* ###FIXME: Move to simplifier, 

300 
taking mk_meta_cong as input, eliminating addeqcongs and deleqcongs *) 

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

301 
infix 4 addcongs delcongs; 
5555  302 
fun ss addcongs congs = ss addeqcongs (map mk_meta_cong congs); 
303 
fun ss delcongs congs = ss deleqcongs (map mk_meta_cong congs); 

4094  304 
fun Addcongs congs = (simpset_ref() := simpset() addcongs congs); 
305 
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

306 

8643  307 
val cong_add_global = Simplifier.change_global_ss (op addcongs); 
308 
val cong_del_global = Simplifier.change_global_ss (op delcongs); 

309 
val cong_add_local = Simplifier.change_local_ss (op addcongs); 

310 
val cong_del_local = Simplifier.change_local_ss (op delcongs); 

311 

312 
val cong_attrib_setup = 

313 
[Attrib.add_attributes [("cong", 

314 
(Attrib.add_del_args cong_add_global cong_del_global, 

315 
Attrib.add_del_args cong_add_local cong_del_local), 

316 
"declare Simplifier congruence rules")]]; 

317 

5115  318 

5496  319 
val meta_simps = 
320 
[triv_forall_equality, (* prunes params *) 

321 
True_implies_equals]; (* prune asms `True' *) 

322 

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

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

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

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

326 

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

327 
val notFalseI = int_prove_fun "~False"; 
6114
45958e54d72e
congruence rules finally use == instead of = and <>
paulson
parents:
5555
diff
changeset

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

329 

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

330 
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

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

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

333 
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

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

335 

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

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

338 
addsimprocs [defALL_regroup,defEX_regroup] 
7570  339 
setSSolver (mk_solver "FOL safe" safe_solver) 
340 
setSolver (mk_solver "FOL unsafe" unsafe_solver) 

5304  341 
setmksimps (mksimps mksimps_pairs); 
342 

343 

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

344 

3910  345 
(*intuitionistic simprules only*) 
5496  346 
val IFOL_ss = 
347 
FOL_basic_ss addsimps (meta_simps @ IFOL_simps @ 

348 
int_ex_simps @ int_all_simps) 

349 
addcongs [imp_cong]; 

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

350 

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

351 
val cla_simps = 
3910  352 
[de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, 
353 
not_all, not_ex, cases_simp] @ 

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

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

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

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

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

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

359 

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

361 
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

362 

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

363 
val simpsetup = [fn thy => (simpset_ref_of thy := FOL_ss; thy)]; 
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

364 

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

365 

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

367 

5219  368 
structure Clasimp = ClasimpFun 
8472  369 
(structure Simplifier = Simplifier and Splitter = Splitter 
370 
and Classical = Cla and Blast = Blast); 

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

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

372 

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

373 
val FOL_css = (FOL_cs, FOL_ss); 