author | wenzelm |
Sat, 17 Mar 2012 17:36:10 +0100 | |
changeset 46996 | f1856425224e |
parent 45659 | 09539cdffcd7 |
child 51717 | 9e7d1c139569 |
permissions | -rw-r--r-- |
9889 | 1 |
(* Title: FOL/simpdata.ML |
1459 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
282 | 3 |
Copyright 1994 University of Cambridge |
0 | 4 |
|
9889 | 5 |
Simplification data for FOL. |
0 | 6 |
*) |
7 |
||
282 | 8 |
(*Make meta-equalities. The operator below is Trueprop*) |
5555 | 9 |
|
282 | 10 |
fun mk_meta_eq th = case concl_of th of |
41310 | 11 |
_ $ (Const(@{const_name eq},_)$_$_) => th RS @{thm eq_reflection} |
12 |
| _ $ (Const(@{const_name iff},_)$_$_) => th RS @{thm iff_reflection} |
|
10431 | 13 |
| _ => |
5555 | 14 |
error("conclusion must be a =-equality or <->");; |
15 |
||
16 |
fun mk_eq th = case concl_of th of |
|
394
432bb9995893
Modified mk_meta_eq to leave meta-equlities on unchanged.
nipkow
parents:
371
diff
changeset
|
17 |
Const("==",_)$_$_ => th |
41310 | 18 |
| _ $ (Const(@{const_name eq},_)$_$_) => mk_meta_eq th |
19 |
| _ $ (Const(@{const_name iff},_)$_$_) => mk_meta_eq th |
|
38500 | 20 |
| _ $ (Const(@{const_name Not},_)$_) => th RS @{thm iff_reflection_F} |
26288
89b9f7c18631
eliminated out-of-scope proofs (cf. theory IFOL and FOL);
wenzelm
parents:
22822
diff
changeset
|
21 |
| _ => th RS @{thm iff_reflection_T}; |
0 | 22 |
|
6114
45958e54d72e
congruence rules finally use == instead of = and <->
paulson
parents:
5555
diff
changeset
|
23 |
(*Replace premises x=y, X<->Y by X==Y*) |
36546 | 24 |
fun mk_meta_prems ctxt = |
25 |
rule_by_tactic ctxt |
|
26288
89b9f7c18631
eliminated out-of-scope proofs (cf. theory IFOL and FOL);
wenzelm
parents:
22822
diff
changeset
|
26 |
(REPEAT_FIRST (resolve_tac [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}])); |
6114
45958e54d72e
congruence rules finally use == instead of = and <->
paulson
parents:
5555
diff
changeset
|
27 |
|
9713 | 28 |
(*Congruence rules for = or <-> (instead of ==)*) |
36546 | 29 |
fun mk_meta_cong ss rl = |
45659
09539cdffcd7
avoid stepping outside of context -- plain zero_var_indexes should be sufficient;
wenzelm
parents:
45625
diff
changeset
|
30 |
Drule.zero_var_indexes (mk_meta_eq (mk_meta_prems (Simplifier.the_context ss) rl)) |
35021
c839a4c670c6
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
32957
diff
changeset
|
31 |
handle THM _ => |
c839a4c670c6
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
32957
diff
changeset
|
32 |
error("Premises and conclusion of congruence rules must use =-equality or <->"); |
5555 | 33 |
|
5304 | 34 |
val mksimps_pairs = |
41310 | 35 |
[(@{const_name imp}, [@{thm mp}]), (@{const_name conj}, [@{thm conjunct1}, @{thm conjunct2}]), |
38500 | 36 |
(@{const_name All}, [@{thm spec}]), (@{const_name True}, []), (@{const_name False}, [])]; |
5304 | 37 |
|
38 |
fun mk_atomize pairs = |
|
39 |
let fun atoms th = |
|
40 |
(case concl_of th of |
|
38500 | 41 |
Const(@{const_name Trueprop},_) $ p => |
5304 | 42 |
(case head_of p of |
43 |
Const(a,_) => |
|
17325 | 44 |
(case AList.lookup (op =) pairs a of |
32952 | 45 |
SOME(rls) => maps atoms ([th] RL rls) |
15531 | 46 |
| NONE => [th]) |
5304 | 47 |
| _ => [th]) |
48 |
| _ => [th]) |
|
49 |
in atoms end; |
|
50 |
||
36543
0e7fc5bf38de
proper context for mksimps etc. -- via simpset of the running Simplifier;
wenzelm
parents:
35232
diff
changeset
|
51 |
fun mksimps pairs (_: simpset) = map mk_eq o mk_atomize pairs o gen_all; |
981 | 52 |
|
1914 | 53 |
|
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
54 |
(** make simplification procedures for quantifier elimination **) |
42458 | 55 |
structure Quantifier1 = Quantifier1 |
56 |
( |
|
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
57 |
(*abstract syntax*) |
42460 | 58 |
fun dest_eq (Const (@{const_name eq}, _) $ s $ t) = SOME (s, t) |
59 |
| dest_eq _ = NONE |
|
60 |
fun dest_conj (Const (@{const_name conj}, _) $ s $ t) = SOME (s, t) |
|
61 |
| dest_conj _ = NONE |
|
62 |
fun dest_imp (Const (@{const_name imp}, _) $ s $ t) = SOME (s, t) |
|
63 |
| dest_imp _ = NONE |
|
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
64 |
val conj = FOLogic.conj |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
65 |
val imp = FOLogic.imp |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
66 |
(*rules*) |
26288
89b9f7c18631
eliminated out-of-scope proofs (cf. theory IFOL and FOL);
wenzelm
parents:
22822
diff
changeset
|
67 |
val iff_reflection = @{thm iff_reflection} |
89b9f7c18631
eliminated out-of-scope proofs (cf. theory IFOL and FOL);
wenzelm
parents:
22822
diff
changeset
|
68 |
val iffI = @{thm iffI} |
89b9f7c18631
eliminated out-of-scope proofs (cf. theory IFOL and FOL);
wenzelm
parents:
22822
diff
changeset
|
69 |
val iff_trans = @{thm iff_trans} |
89b9f7c18631
eliminated out-of-scope proofs (cf. theory IFOL and FOL);
wenzelm
parents:
22822
diff
changeset
|
70 |
val conjI= @{thm conjI} |
89b9f7c18631
eliminated out-of-scope proofs (cf. theory IFOL and FOL);
wenzelm
parents:
22822
diff
changeset
|
71 |
val conjE= @{thm conjE} |
89b9f7c18631
eliminated out-of-scope proofs (cf. theory IFOL and FOL);
wenzelm
parents:
22822
diff
changeset
|
72 |
val impI = @{thm impI} |
89b9f7c18631
eliminated out-of-scope proofs (cf. theory IFOL and FOL);
wenzelm
parents:
22822
diff
changeset
|
73 |
val mp = @{thm mp} |
89b9f7c18631
eliminated out-of-scope proofs (cf. theory IFOL and FOL);
wenzelm
parents:
22822
diff
changeset
|
74 |
val uncurry = @{thm uncurry} |
89b9f7c18631
eliminated out-of-scope proofs (cf. theory IFOL and FOL);
wenzelm
parents:
22822
diff
changeset
|
75 |
val exI = @{thm exI} |
89b9f7c18631
eliminated out-of-scope proofs (cf. theory IFOL and FOL);
wenzelm
parents:
22822
diff
changeset
|
76 |
val exE = @{thm exE} |
89b9f7c18631
eliminated out-of-scope proofs (cf. theory IFOL and FOL);
wenzelm
parents:
22822
diff
changeset
|
77 |
val iff_allI = @{thm iff_allI} |
89b9f7c18631
eliminated out-of-scope proofs (cf. theory IFOL and FOL);
wenzelm
parents:
22822
diff
changeset
|
78 |
val iff_exI = @{thm iff_exI} |
89b9f7c18631
eliminated out-of-scope proofs (cf. theory IFOL and FOL);
wenzelm
parents:
22822
diff
changeset
|
79 |
val all_comm = @{thm all_comm} |
89b9f7c18631
eliminated out-of-scope proofs (cf. theory IFOL and FOL);
wenzelm
parents:
22822
diff
changeset
|
80 |
val ex_comm = @{thm ex_comm} |
42458 | 81 |
); |
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
82 |
|
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
83 |
|
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4325
diff
changeset
|
84 |
(*** Case splitting ***) |
0 | 85 |
|
32177
bc02c5bfcb5b
renamed functor SplitterFun to Splitter, require explicit theory;
wenzelm
parents:
32155
diff
changeset
|
86 |
structure Splitter = Splitter |
bc02c5bfcb5b
renamed functor SplitterFun to Splitter, require explicit theory;
wenzelm
parents:
32155
diff
changeset
|
87 |
( |
bc02c5bfcb5b
renamed functor SplitterFun to Splitter, require explicit theory;
wenzelm
parents:
32155
diff
changeset
|
88 |
val thy = @{theory} |
bc02c5bfcb5b
renamed functor SplitterFun to Splitter, require explicit theory;
wenzelm
parents:
32155
diff
changeset
|
89 |
val mk_eq = mk_eq |
26288
89b9f7c18631
eliminated out-of-scope proofs (cf. theory IFOL and FOL);
wenzelm
parents:
22822
diff
changeset
|
90 |
val meta_eq_to_iff = @{thm meta_eq_to_iff} |
32177
bc02c5bfcb5b
renamed functor SplitterFun to Splitter, require explicit theory;
wenzelm
parents:
32155
diff
changeset
|
91 |
val iffD = @{thm iffD2} |
bc02c5bfcb5b
renamed functor SplitterFun to Splitter, require explicit theory;
wenzelm
parents:
32155
diff
changeset
|
92 |
val disjE = @{thm disjE} |
bc02c5bfcb5b
renamed functor SplitterFun to Splitter, require explicit theory;
wenzelm
parents:
32155
diff
changeset
|
93 |
val conjE = @{thm conjE} |
bc02c5bfcb5b
renamed functor SplitterFun to Splitter, require explicit theory;
wenzelm
parents:
32155
diff
changeset
|
94 |
val exE = @{thm exE} |
bc02c5bfcb5b
renamed functor SplitterFun to Splitter, require explicit theory;
wenzelm
parents:
32155
diff
changeset
|
95 |
val contrapos = @{thm contrapos} |
bc02c5bfcb5b
renamed functor SplitterFun to Splitter, require explicit theory;
wenzelm
parents:
32155
diff
changeset
|
96 |
val contrapos2 = @{thm contrapos2} |
bc02c5bfcb5b
renamed functor SplitterFun to Splitter, require explicit theory;
wenzelm
parents:
32155
diff
changeset
|
97 |
val notnotD = @{thm notnotD} |
bc02c5bfcb5b
renamed functor SplitterFun to Splitter, require explicit theory;
wenzelm
parents:
32155
diff
changeset
|
98 |
); |
1722 | 99 |
|
32177
bc02c5bfcb5b
renamed functor SplitterFun to Splitter, require explicit theory;
wenzelm
parents:
32155
diff
changeset
|
100 |
val split_tac = Splitter.split_tac; |
5304 | 101 |
val split_inside_tac = Splitter.split_inside_tac; |
32177
bc02c5bfcb5b
renamed functor SplitterFun to Splitter, require explicit theory;
wenzelm
parents:
32155
diff
changeset
|
102 |
val split_asm_tac = Splitter.split_asm_tac; |
4325 | 103 |
|
104 |
||
2074
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
105 |
(*** Standard simpsets ***) |
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
106 |
|
26288
89b9f7c18631
eliminated out-of-scope proofs (cf. theory IFOL and FOL);
wenzelm
parents:
22822
diff
changeset
|
107 |
val triv_rls = [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl}, @{thm notFalseI}]; |
2074
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset
|
108 |
|
43597 | 109 |
fun unsafe_solver ss = |
110 |
FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ss), atac, etac @{thm FalseE}]; |
|
111 |
||
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
112 |
(*No premature instantiation of variables during simplification*) |
43597 | 113 |
fun safe_solver ss = |
114 |
FIRST' [match_tac (triv_rls @ Simplifier.prems_of ss), eq_assume_tac, ematch_tac @{thms FalseE}]; |
|
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
115 |
|
3910 | 116 |
(*No simprules, but basic infastructure for simplification*) |
17892 | 117 |
val FOL_basic_ss = |
35232
f588e1169c8b
renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
wenzelm
parents:
35021
diff
changeset
|
118 |
Simplifier.global_context @{theory} empty_ss |
10431 | 119 |
setSSolver (mk_solver "FOL safe" safe_solver) |
120 |
setSolver (mk_solver "FOL unsafe" unsafe_solver) |
|
45625
750c5a47400b
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset
|
121 |
|> Simplifier.set_subgoaler asm_simp_tac |
750c5a47400b
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset
|
122 |
|> Simplifier.set_mksimps (mksimps mksimps_pairs) |
750c5a47400b
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset
|
123 |
|> Simplifier.set_mkcong mk_meta_cong; |
5304 | 124 |
|
18324 | 125 |
fun unfold_tac ths = |
126 |
let val ss0 = Simplifier.clear_ss FOL_basic_ss addsimps ths |
|
127 |
in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end; |
|
17002 | 128 |
|
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
129 |
|
5219 | 130 |
(*** integration of simplifier with classical reasoner ***) |
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
131 |
|
42478 | 132 |
structure Clasimp = Clasimp |
133 |
( |
|
134 |
structure Simplifier = Simplifier |
|
135 |
and Splitter = Splitter |
|
136 |
and Classical = Cla |
|
137 |
and Blast = Blast |
|
138 |
val iffD1 = @{thm iffD1} |
|
139 |
val iffD2 = @{thm iffD2} |
|
140 |
val notE = @{thm notE} |
|
141 |
); |
|
4652
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
4649
diff
changeset
|
142 |
open Clasimp; |
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset
|
143 |