wenzelm@9889
|
1 |
(* Title: FOL/simpdata.ML
|
clasohm@0
|
2 |
ID: $Id$
|
clasohm@1459
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
lcp@282
|
4 |
Copyright 1994 University of Cambridge
|
clasohm@0
|
5 |
|
wenzelm@9889
|
6 |
Simplification data for FOL.
|
clasohm@0
|
7 |
*)
|
clasohm@0
|
8 |
|
lcp@282
|
9 |
(*Make meta-equalities. The operator below is Trueprop*)
|
oheimb@5555
|
10 |
|
lcp@282
|
11 |
fun mk_meta_eq th = case concl_of th of
|
wenzelm@26288
|
12 |
_ $ (Const("op =",_)$_$_) => th RS @{thm eq_reflection}
|
wenzelm@26288
|
13 |
| _ $ (Const("op <->",_)$_$_) => th RS @{thm iff_reflection}
|
wenzelm@10431
|
14 |
| _ =>
|
oheimb@5555
|
15 |
error("conclusion must be a =-equality or <->");;
|
oheimb@5555
|
16 |
|
oheimb@5555
|
17 |
fun mk_eq th = case concl_of th of
|
nipkow@394
|
18 |
Const("==",_)$_$_ => th
|
oheimb@5555
|
19 |
| _ $ (Const("op =",_)$_$_) => mk_meta_eq th
|
oheimb@5555
|
20 |
| _ $ (Const("op <->",_)$_$_) => mk_meta_eq th
|
wenzelm@26288
|
21 |
| _ $ (Const("Not",_)$_) => th RS @{thm iff_reflection_F}
|
wenzelm@26288
|
22 |
| _ => th RS @{thm iff_reflection_T};
|
clasohm@0
|
23 |
|
paulson@6114
|
24 |
(*Replace premises x=y, X<->Y by X==Y*)
|
wenzelm@10431
|
25 |
val mk_meta_prems =
|
wenzelm@10431
|
26 |
rule_by_tactic
|
wenzelm@26288
|
27 |
(REPEAT_FIRST (resolve_tac [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}]));
|
paulson@6114
|
28 |
|
wenzelm@9713
|
29 |
(*Congruence rules for = or <-> (instead of ==)*)
|
paulson@6114
|
30 |
fun mk_meta_cong rl =
|
paulson@6114
|
31 |
standard(mk_meta_eq (mk_meta_prems rl))
|
paulson@6114
|
32 |
handle THM _ =>
|
paulson@6114
|
33 |
error("Premises and conclusion of congruence rules must use =-equality or <->");
|
oheimb@5555
|
34 |
|
oheimb@5304
|
35 |
val mksimps_pairs =
|
wenzelm@26288
|
36 |
[("op -->", [@{thm mp}]), ("op &", [@{thm conjunct1}, @{thm conjunct2}]),
|
wenzelm@26288
|
37 |
("All", [@{thm spec}]), ("True", []), ("False", [])];
|
oheimb@5304
|
38 |
|
wenzelm@16019
|
39 |
(* ###FIXME: move to simplifier.ML
|
oheimb@5304
|
40 |
val mk_atomize: (string * thm list) list -> thm -> thm list
|
oheimb@5304
|
41 |
*)
|
wenzelm@16019
|
42 |
(* ###FIXME: move to simplifier.ML *)
|
oheimb@5304
|
43 |
fun mk_atomize pairs =
|
oheimb@5304
|
44 |
let fun atoms th =
|
oheimb@5304
|
45 |
(case concl_of th of
|
oheimb@5304
|
46 |
Const("Trueprop",_) $ p =>
|
oheimb@5304
|
47 |
(case head_of p of
|
oheimb@5304
|
48 |
Const(a,_) =>
|
haftmann@17325
|
49 |
(case AList.lookup (op =) pairs a of
|
skalberg@15570
|
50 |
SOME(rls) => List.concat (map atoms ([th] RL rls))
|
skalberg@15531
|
51 |
| NONE => [th])
|
oheimb@5304
|
52 |
| _ => [th])
|
oheimb@5304
|
53 |
| _ => [th])
|
oheimb@5304
|
54 |
in atoms end;
|
oheimb@5304
|
55 |
|
wenzelm@12725
|
56 |
fun mksimps pairs = (map mk_eq o mk_atomize pairs o gen_all);
|
clasohm@0
|
57 |
|
paulson@1914
|
58 |
|
paulson@4349
|
59 |
(** make simplification procedures for quantifier elimination **)
|
paulson@4349
|
60 |
structure Quantifier1 = Quantifier1Fun(
|
paulson@4349
|
61 |
struct
|
paulson@4349
|
62 |
(*abstract syntax*)
|
skalberg@15531
|
63 |
fun dest_eq((c as Const("op =",_)) $ s $ t) = SOME(c,s,t)
|
skalberg@15531
|
64 |
| dest_eq _ = NONE;
|
skalberg@15531
|
65 |
fun dest_conj((c as Const("op &",_)) $ s $ t) = SOME(c,s,t)
|
skalberg@15531
|
66 |
| dest_conj _ = NONE;
|
skalberg@15531
|
67 |
fun dest_imp((c as Const("op -->",_)) $ s $ t) = SOME(c,s,t)
|
skalberg@15531
|
68 |
| dest_imp _ = NONE;
|
paulson@4349
|
69 |
val conj = FOLogic.conj
|
paulson@4349
|
70 |
val imp = FOLogic.imp
|
paulson@4349
|
71 |
(*rules*)
|
wenzelm@26288
|
72 |
val iff_reflection = @{thm iff_reflection}
|
wenzelm@26288
|
73 |
val iffI = @{thm iffI}
|
wenzelm@26288
|
74 |
val iff_trans = @{thm iff_trans}
|
wenzelm@26288
|
75 |
val conjI= @{thm conjI}
|
wenzelm@26288
|
76 |
val conjE= @{thm conjE}
|
wenzelm@26288
|
77 |
val impI = @{thm impI}
|
wenzelm@26288
|
78 |
val mp = @{thm mp}
|
wenzelm@26288
|
79 |
val uncurry = @{thm uncurry}
|
wenzelm@26288
|
80 |
val exI = @{thm exI}
|
wenzelm@26288
|
81 |
val exE = @{thm exE}
|
wenzelm@26288
|
82 |
val iff_allI = @{thm iff_allI}
|
wenzelm@26288
|
83 |
val iff_exI = @{thm iff_exI}
|
wenzelm@26288
|
84 |
val all_comm = @{thm all_comm}
|
wenzelm@26288
|
85 |
val ex_comm = @{thm ex_comm}
|
paulson@4349
|
86 |
end);
|
paulson@4349
|
87 |
|
wenzelm@13462
|
88 |
val defEX_regroup =
|
wenzelm@17002
|
89 |
Simplifier.simproc (the_context ())
|
wenzelm@13462
|
90 |
"defined EX" ["EX x. P(x)"] Quantifier1.rearrange_ex;
|
wenzelm@7355
|
91 |
|
paulson@4349
|
92 |
val defALL_regroup =
|
wenzelm@17002
|
93 |
Simplifier.simproc (the_context ())
|
wenzelm@13462
|
94 |
"defined ALL" ["ALL x. P(x)"] Quantifier1.rearrange_all;
|
paulson@4349
|
95 |
|
paulson@4349
|
96 |
|
paulson@4349
|
97 |
(*** Case splitting ***)
|
clasohm@0
|
98 |
|
oheimb@5304
|
99 |
structure SplitterData =
|
oheimb@5304
|
100 |
struct
|
oheimb@5304
|
101 |
structure Simplifier = Simplifier
|
oheimb@5555
|
102 |
val mk_eq = mk_eq
|
wenzelm@26288
|
103 |
val meta_eq_to_iff = @{thm meta_eq_to_iff}
|
wenzelm@26288
|
104 |
val iffD = @{thm iffD2}
|
wenzelm@26288
|
105 |
val disjE = @{thm disjE}
|
wenzelm@26288
|
106 |
val conjE = @{thm conjE}
|
wenzelm@26288
|
107 |
val exE = @{thm exE}
|
wenzelm@26288
|
108 |
val contrapos = @{thm contrapos}
|
wenzelm@26288
|
109 |
val contrapos2 = @{thm contrapos2}
|
wenzelm@26288
|
110 |
val notnotD = @{thm notnotD}
|
oheimb@5304
|
111 |
end;
|
berghofe@1722
|
112 |
|
oheimb@5304
|
113 |
structure Splitter = SplitterFun(SplitterData);
|
berghofe@1722
|
114 |
|
oheimb@5304
|
115 |
val split_tac = Splitter.split_tac;
|
oheimb@5304
|
116 |
val split_inside_tac = Splitter.split_inside_tac;
|
oheimb@5304
|
117 |
val split_asm_tac = Splitter.split_asm_tac;
|
oheimb@5307
|
118 |
val op addsplits = Splitter.addsplits;
|
oheimb@5307
|
119 |
val op delsplits = Splitter.delsplits;
|
oheimb@5304
|
120 |
val Addsplits = Splitter.Addsplits;
|
oheimb@5304
|
121 |
val Delsplits = Splitter.Delsplits;
|
paulson@4325
|
122 |
|
paulson@4325
|
123 |
|
paulson@2074
|
124 |
(*** Standard simpsets ***)
|
paulson@2074
|
125 |
|
wenzelm@26288
|
126 |
val triv_rls = [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl}, @{thm notFalseI}];
|
paulson@5496
|
127 |
|
wenzelm@26288
|
128 |
fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls @ prems),
|
wenzelm@26288
|
129 |
atac, etac @{thm FalseE}];
|
oheimb@2633
|
130 |
(*No premature instantiation of variables during simplification*)
|
wenzelm@26288
|
131 |
fun safe_solver prems = FIRST'[match_tac (triv_rls @ prems),
|
wenzelm@26288
|
132 |
eq_assume_tac, ematch_tac [@{thm FalseE}]];
|
oheimb@2633
|
133 |
|
paulson@3910
|
134 |
(*No simprules, but basic infastructure for simplification*)
|
wenzelm@17892
|
135 |
val FOL_basic_ss =
|
wenzelm@26288
|
136 |
Simplifier.theory_context @{theory} empty_ss
|
wenzelm@10431
|
137 |
setsubgoaler asm_simp_tac
|
wenzelm@10431
|
138 |
setSSolver (mk_solver "FOL safe" safe_solver)
|
wenzelm@10431
|
139 |
setSolver (mk_solver "FOL unsafe" unsafe_solver)
|
wenzelm@10431
|
140 |
setmksimps (mksimps mksimps_pairs)
|
wenzelm@10431
|
141 |
setmkcong mk_meta_cong;
|
oheimb@5304
|
142 |
|
wenzelm@18324
|
143 |
fun unfold_tac ths =
|
wenzelm@18324
|
144 |
let val ss0 = Simplifier.clear_ss FOL_basic_ss addsimps ths
|
wenzelm@18324
|
145 |
in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
|
wenzelm@17002
|
146 |
|
oheimb@2633
|
147 |
|
paulson@3910
|
148 |
(*intuitionistic simprules only*)
|
wenzelm@21539
|
149 |
val IFOL_ss =
|
wenzelm@21539
|
150 |
FOL_basic_ss
|
wenzelm@26288
|
151 |
addsimps (@{thms meta_simps} @ @{thms IFOL_simps} @ @{thms int_ex_simps} @ @{thms int_all_simps})
|
wenzelm@10431
|
152 |
addsimprocs [defALL_regroup, defEX_regroup]
|
wenzelm@26288
|
153 |
addcongs [@{thm imp_cong}];
|
paulson@2074
|
154 |
|
paulson@3910
|
155 |
(*classical simprules too*)
|
wenzelm@26288
|
156 |
val FOL_ss = IFOL_ss addsimps (@{thms cla_simps} @ @{thms cla_ex_simps} @ @{thms cla_all_simps});
|
paulson@2074
|
157 |
|
wenzelm@18708
|
158 |
val simpsetup = (fn thy => (change_simpset_of thy (fn _ => FOL_ss); thy));
|
oheimb@2633
|
159 |
|
oheimb@2633
|
160 |
|
wenzelm@5219
|
161 |
(*** integration of simplifier with classical reasoner ***)
|
oheimb@2633
|
162 |
|
wenzelm@5219
|
163 |
structure Clasimp = ClasimpFun
|
wenzelm@8472
|
164 |
(structure Simplifier = Simplifier and Splitter = Splitter
|
wenzelm@9851
|
165 |
and Classical = Cla and Blast = Blast
|
wenzelm@26288
|
166 |
val iffD1 = @{thm iffD1} val iffD2 = @{thm iffD2} val notE = @{thm notE});
|
oheimb@4652
|
167 |
open Clasimp;
|
oheimb@2633
|
168 |
|
wenzelm@22128
|
169 |
ML_Context.value_antiq "clasimpset"
|
wenzelm@22128
|
170 |
(Scan.succeed ("clasimpset", "Clasimp.local_clasimpset_of (ML_Context.the_local_context ())"));
|
wenzelm@22128
|
171 |
|
oheimb@2633
|
172 |
val FOL_css = (FOL_cs, FOL_ss);
|