author | nipkow |
Fri, 01 Oct 1993 13:26:22 +0100 | |
changeset 17 | b35851cafd3e |
parent 1 | c6a6e3db5353 |
child 88 | 9df4dfedee01 |
permissions | -rw-r--r-- |
1 | 1 |
(* Title: Provers/simplifier |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1993 TU Munich |
|
5 |
||
6 |
Generic simplifier, suitable for most logics. |
|
7 |
||
8 |
*) |
|
9 |
infix addsimps addeqcongs |
|
0 | 10 |
setsolver setloop setmksimps setsubgoaler; |
11 |
||
12 |
signature SIMPLIFIER = |
|
13 |
sig |
|
14 |
type simpset |
|
1 | 15 |
val addeqcongs: simpset * thm list -> simpset |
0 | 16 |
val addsimps: simpset * thm list -> simpset |
17 |
val asm_full_simp_tac: simpset -> int -> tactic |
|
18 |
val asm_simp_tac: simpset -> int -> tactic |
|
19 |
val empty_ss: simpset |
|
20 |
val merge_ss: simpset * simpset -> simpset |
|
21 |
val prems_of_ss: simpset -> thm list |
|
22 |
val rep_ss: simpset -> {simps: thm list, congs: thm list} |
|
23 |
val setsolver: simpset * (thm list -> int -> tactic) -> simpset |
|
24 |
val setloop: simpset * (int -> tactic) -> simpset |
|
25 |
val setmksimps: simpset * (thm -> thm list) -> simpset |
|
26 |
val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset |
|
27 |
val simp_tac: simpset -> int -> tactic |
|
28 |
end; |
|
29 |
||
30 |
structure Simplifier:SIMPLIFIER = |
|
31 |
struct |
|
32 |
||
33 |
datatype simpset = |
|
34 |
SS of {mss: meta_simpset, |
|
35 |
simps: thm list, |
|
36 |
congs: thm list, |
|
37 |
subgoal_tac: simpset -> int -> tactic, |
|
38 |
finish_tac: thm list -> int -> tactic, |
|
39 |
loop_tac: int -> tactic}; |
|
40 |
||
41 |
val empty_ss = |
|
42 |
SS{mss=empty_mss, |
|
43 |
simps= [], |
|
44 |
congs= [], |
|
45 |
subgoal_tac= K(K no_tac), |
|
46 |
finish_tac= K(K no_tac), |
|
47 |
loop_tac= K no_tac}; |
|
48 |
||
49 |
||
50 |
fun (SS{mss,simps,congs,subgoal_tac,finish_tac,...}) setloop loop_tac = |
|
51 |
SS{mss=mss, |
|
52 |
simps= simps, |
|
53 |
congs= congs, |
|
54 |
subgoal_tac= subgoal_tac, |
|
55 |
finish_tac=finish_tac, |
|
56 |
loop_tac=loop_tac}; |
|
57 |
||
58 |
fun (SS{mss,simps,congs,subgoal_tac,loop_tac,...}) setsolver finish_tac = |
|
59 |
SS{mss=mss, |
|
60 |
simps= simps, |
|
61 |
congs= congs, |
|
62 |
subgoal_tac= subgoal_tac, |
|
63 |
finish_tac=finish_tac, |
|
64 |
loop_tac=loop_tac}; |
|
65 |
||
66 |
fun (SS{mss,simps,congs,finish_tac,loop_tac,...}) setsubgoaler subgoal_tac = |
|
67 |
SS{mss=mss, |
|
68 |
simps= simps, |
|
69 |
congs= congs, |
|
70 |
subgoal_tac= subgoal_tac, |
|
71 |
finish_tac=finish_tac, |
|
72 |
loop_tac=loop_tac}; |
|
73 |
||
74 |
fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) setmksimps mk_simps = |
|
75 |
SS{mss=Thm.set_mk_rews(mss,mk_simps), |
|
76 |
simps= simps, |
|
77 |
congs= congs, |
|
78 |
subgoal_tac= subgoal_tac, |
|
79 |
finish_tac=finish_tac, |
|
80 |
loop_tac=loop_tac}; |
|
81 |
||
82 |
fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addsimps rews = |
|
83 |
let val rews' = flat(map (Thm.mk_rews_of_mss mss) rews) |
|
84 |
in |
|
85 |
SS{mss= Thm.add_simps(mss,rews'), |
|
86 |
simps= rews' @ simps, |
|
87 |
congs= congs, |
|
88 |
subgoal_tac= subgoal_tac, |
|
89 |
finish_tac=finish_tac, |
|
90 |
loop_tac=loop_tac} |
|
91 |
end; |
|
92 |
||
1 | 93 |
fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addeqcongs newcongs = |
0 | 94 |
SS{mss= Thm.add_congs(mss,newcongs), |
95 |
simps= simps, |
|
96 |
congs= newcongs @ congs, |
|
97 |
subgoal_tac= subgoal_tac, |
|
98 |
finish_tac=finish_tac, |
|
99 |
loop_tac=loop_tac}; |
|
100 |
||
101 |
fun merge_ss(SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}, |
|
102 |
SS{simps=simps2,congs=congs2,...}) = |
|
103 |
let val simps' = gen_union eq_thm (simps,simps2) |
|
104 |
val congs' = gen_union eq_thm (congs,congs2) |
|
105 |
val mss' = Thm.set_mk_rews(empty_mss,Thm.mk_rews_of_mss mss) |
|
106 |
val mss' = Thm.add_simps(mss',simps') |
|
107 |
val mss' = Thm.add_congs(mss',congs') |
|
108 |
in SS{mss= mss', |
|
109 |
simps= simps, |
|
110 |
congs= congs', |
|
111 |
subgoal_tac= subgoal_tac, |
|
112 |
finish_tac= finish_tac, |
|
113 |
loop_tac= loop_tac} |
|
114 |
end; |
|
115 |
||
116 |
fun prems_of_ss(SS{mss,...}) = prems_of_mss mss; |
|
117 |
||
118 |
fun rep_ss(SS{simps,congs,...}) = {simps=simps,congs=congs}; |
|
119 |
||
120 |
fun add_asms (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) prems = |
|
121 |
let val rews = flat(map (mk_rews_of_mss mss) prems) |
|
122 |
in SS{mss= add_prems(add_simps(mss,rews),prems), simps=simps, congs=congs, |
|
123 |
subgoal_tac=subgoal_tac,finish_tac=finish_tac, |
|
124 |
loop_tac=loop_tac} |
|
125 |
end; |
|
126 |
||
1 | 127 |
fun NEWSUBGOALS tac tacf = |
128 |
STATE(fn state0 => |
|
129 |
tac THEN STATE(fn state1 => tacf(nprems_of state1 - nprems_of state0))); |
|
130 |
||
0 | 131 |
fun asm_full_simp_tac(SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) = |
132 |
let fun solve_all_tac mss = |
|
133 |
let val ss = SS{mss=mss,simps=simps,congs=congs, |
|
134 |
subgoal_tac=subgoal_tac, |
|
135 |
finish_tac=finish_tac, loop_tac=loop_tac} |
|
1 | 136 |
val solve1_tac = |
137 |
NEWSUBGOALS (subgoal_tac ss 1) |
|
138 |
(fn n => if n<0 then all_tac else no_tac) |
|
139 |
in DEPTH_SOLVE(solve1_tac) end |
|
0 | 140 |
|
141 |
fun simp_loop i thm = |
|
142 |
tapply(asm_rewrite_goal_tac solve_all_tac mss i THEN |
|
1 | 143 |
(finish_tac (prems_of_mss mss) i ORELSE looper i), |
0 | 144 |
thm) |
1 | 145 |
and allsimp i n = EVERY(map (fn j => simp_loop_tac (i+j)) (n downto 0)) |
146 |
and looper i = TRY(NEWSUBGOALS (loop_tac i) (allsimp i)) |
|
0 | 147 |
and simp_loop_tac i = Tactic(simp_loop i) |
148 |
||
17
b35851cafd3e
asm_full_simp_tac now fails when applied to a state w/o subgoals.
nipkow
parents:
1
diff
changeset
|
149 |
in fn i => COND (has_fewer_prems 0) no_tac (simp_loop_tac i) end; |
0 | 150 |
|
151 |
fun asm_simp_tac ss = |
|
152 |
METAHYPS(fn prems => asm_full_simp_tac (add_asms ss prems) 1); |
|
153 |
||
154 |
fun simp_tac ss = METAHYPS(fn _ => asm_full_simp_tac ss 1); |
|
155 |
||
156 |
end; |