author | wenzelm |
Tue, 10 Dec 1996 14:16:11 +0100 | |
changeset 2369 | 8100f00e8950 |
parent 1770 | 608050b43bee |
child 2503 | 7590fd5ce3c7 |
permissions | -rw-r--r-- |
1243 | 1 |
(* Title: Provers/simplifier.ML |
1 | 2 |
ID: $Id$ |
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1993 TU Munich |
|
5 |
||
6 |
Generic simplifier, suitable for most logics. |
|
7 |
||
8 |
*) |
|
1260 | 9 |
|
1770 | 10 |
infix 4 addsimps addeqcongs addsolver delsimps |
983 | 11 |
setsolver setloop setmksimps setsubgoaler; |
0 | 12 |
|
13 |
signature SIMPLIFIER = |
|
14 |
sig |
|
15 |
type simpset |
|
1 | 16 |
val addeqcongs: simpset * thm list -> simpset |
0 | 17 |
val addsimps: simpset * thm list -> simpset |
1770 | 18 |
val addsolver: simpset * (thm list -> int -> tactic) -> simpset |
88 | 19 |
val delsimps: simpset * thm list -> simpset |
0 | 20 |
val asm_full_simp_tac: simpset -> int -> tactic |
1676 | 21 |
val full_simp_tac: simpset -> int -> tactic |
22 |
val asm_simp_tac: simpset -> int -> tactic |
|
0 | 23 |
val empty_ss: simpset |
24 |
val merge_ss: simpset * simpset -> simpset |
|
25 |
val prems_of_ss: simpset -> thm list |
|
26 |
val rep_ss: simpset -> {simps: thm list, congs: thm list} |
|
27 |
val setsolver: simpset * (thm list -> int -> tactic) -> simpset |
|
28 |
val setloop: simpset * (int -> tactic) -> simpset |
|
29 |
val setmksimps: simpset * (thm -> thm list) -> simpset |
|
30 |
val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset |
|
31 |
val simp_tac: simpset -> int -> tactic |
|
1243 | 32 |
|
33 |
val simpset: simpset ref |
|
34 |
val Addsimps: thm list -> unit |
|
35 |
val Delsimps: thm list -> unit |
|
36 |
val Simp_tac: int -> tactic |
|
1676 | 37 |
val Asm_simp_tac: int -> tactic |
38 |
val Full_simp_tac: int -> tactic |
|
1243 | 39 |
val Asm_full_simp_tac: int -> tactic |
0 | 40 |
end; |
41 |
||
1512 | 42 |
structure Simplifier :SIMPLIFIER = |
0 | 43 |
struct |
44 |
||
45 |
datatype simpset = |
|
1260 | 46 |
Simpset of {mss: meta_simpset, |
47 |
simps: thm list, |
|
48 |
congs: thm list, |
|
49 |
subgoal_tac: simpset -> int -> tactic, |
|
50 |
finish_tac: thm list -> int -> tactic, |
|
51 |
loop_tac: int -> tactic}; |
|
0 | 52 |
|
53 |
val empty_ss = |
|
1260 | 54 |
Simpset{mss=empty_mss, |
55 |
simps= [], |
|
56 |
congs= [], |
|
57 |
subgoal_tac= K(K no_tac), |
|
58 |
finish_tac= K(K no_tac), |
|
59 |
loop_tac= K no_tac}; |
|
0 | 60 |
|
1243 | 61 |
val simpset = ref empty_ss; |
0 | 62 |
|
1260 | 63 |
fun (Simpset{mss,simps,congs,subgoal_tac,finish_tac,...}) setloop loop_tac = |
64 |
Simpset{mss=mss, |
|
65 |
simps= simps, |
|
66 |
congs= congs, |
|
67 |
subgoal_tac= subgoal_tac, |
|
68 |
finish_tac=finish_tac, |
|
69 |
loop_tac= DETERM o loop_tac}; |
|
0 | 70 |
|
1260 | 71 |
fun (Simpset{mss,simps,congs,subgoal_tac,loop_tac,...}) setsolver finish_tac = |
72 |
Simpset{mss=mss, |
|
73 |
simps= simps, |
|
74 |
congs= congs, |
|
75 |
subgoal_tac= subgoal_tac, |
|
76 |
finish_tac=finish_tac, |
|
77 |
loop_tac=loop_tac}; |
|
0 | 78 |
|
1770 | 79 |
fun (Simpset{mss,simps,congs,subgoal_tac,loop_tac,finish_tac}) addsolver tac = |
80 |
Simpset{mss=mss, |
|
81 |
simps= simps, |
|
82 |
congs= congs, |
|
83 |
subgoal_tac= subgoal_tac, |
|
84 |
finish_tac=fn hyps => finish_tac hyps ORELSE' tac hyps, |
|
85 |
loop_tac=loop_tac}; |
|
86 |
||
1260 | 87 |
fun (Simpset{mss,simps,congs,finish_tac,loop_tac,...}) setsubgoaler |
88 |
subgoal_tac = |
|
89 |
Simpset{mss=mss, |
|
90 |
simps= simps, |
|
91 |
congs= congs, |
|
92 |
subgoal_tac= subgoal_tac, |
|
93 |
finish_tac=finish_tac, |
|
94 |
loop_tac=loop_tac}; |
|
95 |
||
96 |
fun (Simpset{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) setmksimps |
|
97 |
mk_simps = |
|
98 |
Simpset{mss=Thm.set_mk_rews(mss,mk_simps), |
|
99 |
simps= simps, |
|
100 |
congs= congs, |
|
101 |
subgoal_tac= subgoal_tac, |
|
102 |
finish_tac=finish_tac, |
|
103 |
loop_tac=loop_tac}; |
|
0 | 104 |
|
1260 | 105 |
fun (Simpset{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addsimps rews = |
88 | 106 |
let val rews' = flat(map (Thm.mk_rews_of_mss mss) rews) in |
1260 | 107 |
Simpset{mss= Thm.add_simps(mss,rews'), |
108 |
simps= rews' @ simps, |
|
109 |
congs= congs, |
|
110 |
subgoal_tac= subgoal_tac, |
|
111 |
finish_tac=finish_tac, |
|
112 |
loop_tac=loop_tac} |
|
0 | 113 |
end; |
114 |
||
1243 | 115 |
fun Addsimps rews = (simpset := !simpset addsimps rews); |
116 |
||
1260 | 117 |
fun (Simpset{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) delsimps rews = |
88 | 118 |
let val rews' = flat(map (Thm.mk_rews_of_mss mss) rews) in |
1260 | 119 |
Simpset{mss= Thm.del_simps(mss,rews'), |
120 |
simps= foldl (gen_rem eq_thm) (simps,rews'), |
|
121 |
congs= congs, |
|
122 |
subgoal_tac= subgoal_tac, |
|
123 |
finish_tac=finish_tac, |
|
124 |
loop_tac=loop_tac} |
|
88 | 125 |
end; |
126 |
||
1243 | 127 |
fun Delsimps rews = (simpset := !simpset delsimps rews); |
128 |
||
1260 | 129 |
fun (Simpset{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addeqcongs |
130 |
newcongs = |
|
131 |
Simpset{mss= Thm.add_congs(mss,newcongs), |
|
132 |
simps= simps, |
|
133 |
congs= newcongs @ congs, |
|
134 |
subgoal_tac= subgoal_tac, |
|
135 |
finish_tac=finish_tac, |
|
136 |
loop_tac=loop_tac}; |
|
137 |
||
138 |
fun merge_ss(Simpset{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}, |
|
139 |
Simpset{simps=simps2,congs=congs2,...}) = |
|
0 | 140 |
let val simps' = gen_union eq_thm (simps,simps2) |
141 |
val congs' = gen_union eq_thm (congs,congs2) |
|
142 |
val mss' = Thm.set_mk_rews(empty_mss,Thm.mk_rews_of_mss mss) |
|
143 |
val mss' = Thm.add_simps(mss',simps') |
|
144 |
val mss' = Thm.add_congs(mss',congs') |
|
1260 | 145 |
in Simpset{mss= mss', |
146 |
simps= simps', |
|
147 |
congs= congs', |
|
148 |
subgoal_tac= subgoal_tac, |
|
149 |
finish_tac= finish_tac, |
|
150 |
loop_tac= loop_tac} |
|
0 | 151 |
end; |
152 |
||
1260 | 153 |
fun prems_of_ss(Simpset{mss,...}) = prems_of_mss mss; |
0 | 154 |
|
1260 | 155 |
fun rep_ss(Simpset{simps,congs,...}) = {simps=simps,congs=congs}; |
0 | 156 |
|
1 | 157 |
fun NEWSUBGOALS tac tacf = |
158 |
STATE(fn state0 => |
|
159 |
tac THEN STATE(fn state1 => tacf(nprems_of state1 - nprems_of state0))); |
|
160 |
||
217
c972c57e7762
got rid of METAHYPS due to the change of the basic simplification routines
nipkow
parents:
146
diff
changeset
|
161 |
fun gen_simp_tac mode = |
1260 | 162 |
fn (Simpset{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) => |
0 | 163 |
let fun solve_all_tac mss = |
1260 | 164 |
let val ss = Simpset{mss=mss,simps=simps,congs=congs, |
165 |
subgoal_tac=subgoal_tac, |
|
166 |
finish_tac=finish_tac, loop_tac=loop_tac} |
|
1 | 167 |
val solve1_tac = |
168 |
NEWSUBGOALS (subgoal_tac ss 1) |
|
169 |
(fn n => if n<0 then all_tac else no_tac) |
|
170 |
in DEPTH_SOLVE(solve1_tac) end |
|
0 | 171 |
|
1512 | 172 |
fun simp_loop_tac i thm = |
173 |
(asm_rewrite_goal_tac mode solve_all_tac mss i THEN |
|
174 |
(finish_tac (prems_of_mss mss) i ORELSE looper i)) thm |
|
1 | 175 |
and allsimp i n = EVERY(map (fn j => simp_loop_tac (i+j)) (n downto 0)) |
176 |
and looper i = TRY(NEWSUBGOALS (loop_tac i) (allsimp i)) |
|
217
c972c57e7762
got rid of METAHYPS due to the change of the basic simplification routines
nipkow
parents:
146
diff
changeset
|
177 |
in simp_loop_tac end; |
0 | 178 |
|
1676 | 179 |
val asm_full_simp_tac = gen_simp_tac (true ,true ); |
180 |
val full_simp_tac = gen_simp_tac (true ,false); |
|
181 |
val asm_simp_tac = gen_simp_tac (false,true ); |
|
182 |
val simp_tac = gen_simp_tac (false,false); |
|
0 | 183 |
|
1243 | 184 |
fun Asm_full_simp_tac i = asm_full_simp_tac (!simpset) i; |
1676 | 185 |
fun Full_simp_tac i = full_simp_tac (!simpset) i; |
186 |
fun Asm_simp_tac i = asm_simp_tac (!simpset) i; |
|
187 |
fun Simp_tac i = simp_tac (!simpset) i; |
|
406 | 188 |
|
1243 | 189 |
end; |