wenzelm@9889
|
1 |
(* Title: FOL/simpdata.ML
|
clasohm@1459
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
lcp@282
|
3 |
Copyright 1994 University of Cambridge
|
clasohm@0
|
4 |
|
wenzelm@9889
|
5 |
Simplification data for FOL.
|
clasohm@0
|
6 |
*)
|
clasohm@0
|
7 |
|
lcp@282
|
8 |
(*Make meta-equalities. The operator below is Trueprop*)
|
oheimb@5555
|
9 |
|
lcp@282
|
10 |
fun mk_meta_eq th = case concl_of th of
|
wenzelm@41558
|
11 |
_ $ (Const(@{const_name eq},_)$_$_) => th RS @{thm eq_reflection}
|
wenzelm@41558
|
12 |
| _ $ (Const(@{const_name iff},_)$_$_) => th RS @{thm iff_reflection}
|
wenzelm@10431
|
13 |
| _ =>
|
oheimb@5555
|
14 |
error("conclusion must be a =-equality or <->");;
|
oheimb@5555
|
15 |
|
oheimb@5555
|
16 |
fun mk_eq th = case concl_of th of
|
nipkow@394
|
17 |
Const("==",_)$_$_ => th
|
wenzelm@41558
|
18 |
| _ $ (Const(@{const_name eq},_)$_$_) => mk_meta_eq th
|
wenzelm@41558
|
19 |
| _ $ (Const(@{const_name iff},_)$_$_) => mk_meta_eq th
|
haftmann@38725
|
20 |
| _ $ (Const(@{const_name Not},_)$_) => th RS @{thm iff_reflection_F}
|
wenzelm@26288
|
21 |
| _ => th RS @{thm iff_reflection_T};
|
clasohm@0
|
22 |
|
paulson@6114
|
23 |
(*Replace premises x=y, X<->Y by X==Y*)
|
wenzelm@36578
|
24 |
fun mk_meta_prems ctxt =
|
wenzelm@36578
|
25 |
rule_by_tactic ctxt
|
wenzelm@26288
|
26 |
(REPEAT_FIRST (resolve_tac [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}]));
|
paulson@6114
|
27 |
|
wenzelm@9713
|
28 |
(*Congruence rules for = or <-> (instead of ==)*)
|
wenzelm@36578
|
29 |
fun mk_meta_cong ss rl =
|
wenzelm@36578
|
30 |
Drule.export_without_context (mk_meta_eq (mk_meta_prems (Simplifier.the_context ss) rl))
|
wenzelm@35021
|
31 |
handle THM _ =>
|
wenzelm@35021
|
32 |
error("Premises and conclusion of congruence rules must use =-equality or <->");
|
oheimb@5555
|
33 |
|
oheimb@5304
|
34 |
val mksimps_pairs =
|
wenzelm@41558
|
35 |
[(@{const_name imp}, [@{thm mp}]), (@{const_name conj}, [@{thm conjunct1}, @{thm conjunct2}]),
|
haftmann@38725
|
36 |
(@{const_name All}, [@{thm spec}]), (@{const_name True}, []), (@{const_name False}, [])];
|
oheimb@5304
|
37 |
|
oheimb@5304
|
38 |
fun mk_atomize pairs =
|
oheimb@5304
|
39 |
let fun atoms th =
|
oheimb@5304
|
40 |
(case concl_of th of
|
haftmann@38725
|
41 |
Const(@{const_name Trueprop},_) $ p =>
|
oheimb@5304
|
42 |
(case head_of p of
|
oheimb@5304
|
43 |
Const(a,_) =>
|
haftmann@17325
|
44 |
(case AList.lookup (op =) pairs a of
|
wenzelm@32952
|
45 |
SOME(rls) => maps atoms ([th] RL rls)
|
skalberg@15531
|
46 |
| NONE => [th])
|
oheimb@5304
|
47 |
| _ => [th])
|
oheimb@5304
|
48 |
| _ => [th])
|
oheimb@5304
|
49 |
in atoms end;
|
oheimb@5304
|
50 |
|
wenzelm@36543
|
51 |
fun mksimps pairs (_: simpset) = map mk_eq o mk_atomize pairs o gen_all;
|
clasohm@0
|
52 |
|
paulson@1914
|
53 |
|
paulson@4349
|
54 |
(** make simplification procedures for quantifier elimination **)
|
wenzelm@43329
|
55 |
structure Quantifier1 = Quantifier1
|
wenzelm@43329
|
56 |
(
|
paulson@4349
|
57 |
(*abstract syntax*)
|
wenzelm@43331
|
58 |
fun dest_eq (Const (@{const_name eq}, _) $ s $ t) = SOME (s, t)
|
wenzelm@43331
|
59 |
| dest_eq _ = NONE
|
wenzelm@43331
|
60 |
fun dest_conj (Const (@{const_name conj}, _) $ s $ t) = SOME (s, t)
|
wenzelm@43331
|
61 |
| dest_conj _ = NONE
|
wenzelm@43331
|
62 |
fun dest_imp (Const (@{const_name imp}, _) $ s $ t) = SOME (s, t)
|
wenzelm@43331
|
63 |
| dest_imp _ = NONE
|
paulson@4349
|
64 |
val conj = FOLogic.conj
|
paulson@4349
|
65 |
val imp = FOLogic.imp
|
paulson@4349
|
66 |
(*rules*)
|
wenzelm@26288
|
67 |
val iff_reflection = @{thm iff_reflection}
|
wenzelm@26288
|
68 |
val iffI = @{thm iffI}
|
wenzelm@26288
|
69 |
val iff_trans = @{thm iff_trans}
|
wenzelm@26288
|
70 |
val conjI= @{thm conjI}
|
wenzelm@26288
|
71 |
val conjE= @{thm conjE}
|
wenzelm@26288
|
72 |
val impI = @{thm impI}
|
wenzelm@26288
|
73 |
val mp = @{thm mp}
|
wenzelm@26288
|
74 |
val uncurry = @{thm uncurry}
|
wenzelm@26288
|
75 |
val exI = @{thm exI}
|
wenzelm@26288
|
76 |
val exE = @{thm exE}
|
wenzelm@26288
|
77 |
val iff_allI = @{thm iff_allI}
|
wenzelm@26288
|
78 |
val iff_exI = @{thm iff_exI}
|
wenzelm@26288
|
79 |
val all_comm = @{thm all_comm}
|
wenzelm@26288
|
80 |
val ex_comm = @{thm ex_comm}
|
wenzelm@43329
|
81 |
);
|
paulson@4349
|
82 |
|
paulson@4349
|
83 |
|
paulson@4349
|
84 |
(*** Case splitting ***)
|
clasohm@0
|
85 |
|
wenzelm@32177
|
86 |
structure Splitter = Splitter
|
wenzelm@32177
|
87 |
(
|
wenzelm@32177
|
88 |
val thy = @{theory}
|
wenzelm@32177
|
89 |
val mk_eq = mk_eq
|
wenzelm@26288
|
90 |
val meta_eq_to_iff = @{thm meta_eq_to_iff}
|
wenzelm@32177
|
91 |
val iffD = @{thm iffD2}
|
wenzelm@32177
|
92 |
val disjE = @{thm disjE}
|
wenzelm@32177
|
93 |
val conjE = @{thm conjE}
|
wenzelm@32177
|
94 |
val exE = @{thm exE}
|
wenzelm@32177
|
95 |
val contrapos = @{thm contrapos}
|
wenzelm@32177
|
96 |
val contrapos2 = @{thm contrapos2}
|
wenzelm@32177
|
97 |
val notnotD = @{thm notnotD}
|
wenzelm@32177
|
98 |
);
|
berghofe@1722
|
99 |
|
wenzelm@32177
|
100 |
val split_tac = Splitter.split_tac;
|
oheimb@5304
|
101 |
val split_inside_tac = Splitter.split_inside_tac;
|
wenzelm@32177
|
102 |
val split_asm_tac = Splitter.split_asm_tac;
|
wenzelm@32177
|
103 |
val op addsplits = Splitter.addsplits;
|
wenzelm@32177
|
104 |
val op delsplits = Splitter.delsplits;
|
paulson@4325
|
105 |
|
paulson@4325
|
106 |
|
paulson@2074
|
107 |
(*** Standard simpsets ***)
|
paulson@2074
|
108 |
|
wenzelm@26288
|
109 |
val triv_rls = [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl}, @{thm notFalseI}];
|
paulson@5496
|
110 |
|
wenzelm@44469
|
111 |
fun unsafe_solver ss = FIRST'[resolve_tac (triv_rls @ prems_of_ss ss),
|
wenzelm@26288
|
112 |
atac, etac @{thm FalseE}];
|
oheimb@2633
|
113 |
(*No premature instantiation of variables during simplification*)
|
wenzelm@44469
|
114 |
fun safe_solver ss = FIRST'[match_tac (triv_rls @ prems_of_ss ss),
|
wenzelm@26288
|
115 |
eq_assume_tac, ematch_tac [@{thm FalseE}]];
|
oheimb@2633
|
116 |
|
paulson@3910
|
117 |
(*No simprules, but basic infastructure for simplification*)
|
wenzelm@17892
|
118 |
val FOL_basic_ss =
|
wenzelm@35232
|
119 |
Simplifier.global_context @{theory} empty_ss
|
wenzelm@10431
|
120 |
setsubgoaler asm_simp_tac
|
wenzelm@10431
|
121 |
setSSolver (mk_solver "FOL safe" safe_solver)
|
wenzelm@10431
|
122 |
setSolver (mk_solver "FOL unsafe" unsafe_solver)
|
wenzelm@10431
|
123 |
setmksimps (mksimps mksimps_pairs)
|
wenzelm@10431
|
124 |
setmkcong mk_meta_cong;
|
oheimb@5304
|
125 |
|
wenzelm@18324
|
126 |
fun unfold_tac ths =
|
wenzelm@18324
|
127 |
let val ss0 = Simplifier.clear_ss FOL_basic_ss addsimps ths
|
wenzelm@18324
|
128 |
in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
|
wenzelm@17002
|
129 |
|
oheimb@2633
|
130 |
|
wenzelm@5219
|
131 |
(*** integration of simplifier with classical reasoner ***)
|
oheimb@2633
|
132 |
|
wenzelm@43349
|
133 |
structure Clasimp = Clasimp
|
wenzelm@43349
|
134 |
(
|
wenzelm@43349
|
135 |
structure Simplifier = Simplifier
|
wenzelm@43349
|
136 |
and Splitter = Splitter
|
wenzelm@43349
|
137 |
and Classical = Cla
|
wenzelm@43349
|
138 |
and Blast = Blast
|
wenzelm@43349
|
139 |
val iffD1 = @{thm iffD1}
|
wenzelm@43349
|
140 |
val iffD2 = @{thm iffD2}
|
wenzelm@43349
|
141 |
val notE = @{thm notE}
|
wenzelm@43349
|
142 |
);
|
oheimb@4652
|
143 |
open Clasimp;
|
oheimb@2633
|
144 |
|