0
|
1 |
infix addsimps addcongs
|
|
2 |
setsolver setloop setmksimps setsubgoaler;
|
|
3 |
|
|
4 |
signature SIMPLIFIER =
|
|
5 |
sig
|
|
6 |
type simpset
|
|
7 |
val addcongs: simpset * thm list -> simpset
|
|
8 |
val addsimps: simpset * thm list -> simpset
|
|
9 |
val asm_full_simp_tac: simpset -> int -> tactic
|
|
10 |
val asm_simp_tac: simpset -> int -> tactic
|
|
11 |
val empty_ss: simpset
|
|
12 |
val merge_ss: simpset * simpset -> simpset
|
|
13 |
val prems_of_ss: simpset -> thm list
|
|
14 |
val rep_ss: simpset -> {simps: thm list, congs: thm list}
|
|
15 |
val setsolver: simpset * (thm list -> int -> tactic) -> simpset
|
|
16 |
val setloop: simpset * (int -> tactic) -> simpset
|
|
17 |
val setmksimps: simpset * (thm -> thm list) -> simpset
|
|
18 |
val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset
|
|
19 |
val simp_tac: simpset -> int -> tactic
|
|
20 |
end;
|
|
21 |
|
|
22 |
structure Simplifier:SIMPLIFIER =
|
|
23 |
struct
|
|
24 |
|
|
25 |
datatype simpset =
|
|
26 |
SS of {mss: meta_simpset,
|
|
27 |
simps: thm list,
|
|
28 |
congs: thm list,
|
|
29 |
subgoal_tac: simpset -> int -> tactic,
|
|
30 |
finish_tac: thm list -> int -> tactic,
|
|
31 |
loop_tac: int -> tactic};
|
|
32 |
|
|
33 |
val empty_ss =
|
|
34 |
SS{mss=empty_mss,
|
|
35 |
simps= [],
|
|
36 |
congs= [],
|
|
37 |
subgoal_tac= K(K no_tac),
|
|
38 |
finish_tac= K(K no_tac),
|
|
39 |
loop_tac= K no_tac};
|
|
40 |
|
|
41 |
|
|
42 |
fun (SS{mss,simps,congs,subgoal_tac,finish_tac,...}) setloop loop_tac =
|
|
43 |
SS{mss=mss,
|
|
44 |
simps= simps,
|
|
45 |
congs= congs,
|
|
46 |
subgoal_tac= subgoal_tac,
|
|
47 |
finish_tac=finish_tac,
|
|
48 |
loop_tac=loop_tac};
|
|
49 |
|
|
50 |
fun (SS{mss,simps,congs,subgoal_tac,loop_tac,...}) setsolver finish_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,finish_tac,loop_tac,...}) setsubgoaler subgoal_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,subgoal_tac,finish_tac,loop_tac}) setmksimps mk_simps =
|
|
67 |
SS{mss=Thm.set_mk_rews(mss,mk_simps),
|
|
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}) addsimps rews =
|
|
75 |
let val rews' = flat(map (Thm.mk_rews_of_mss mss) rews)
|
|
76 |
in
|
|
77 |
SS{mss= Thm.add_simps(mss,rews'),
|
|
78 |
simps= rews' @ simps,
|
|
79 |
congs= congs,
|
|
80 |
subgoal_tac= subgoal_tac,
|
|
81 |
finish_tac=finish_tac,
|
|
82 |
loop_tac=loop_tac}
|
|
83 |
end;
|
|
84 |
|
|
85 |
fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addcongs newcongs =
|
|
86 |
SS{mss= Thm.add_congs(mss,newcongs),
|
|
87 |
simps= simps,
|
|
88 |
congs= newcongs @ congs,
|
|
89 |
subgoal_tac= subgoal_tac,
|
|
90 |
finish_tac=finish_tac,
|
|
91 |
loop_tac=loop_tac};
|
|
92 |
|
|
93 |
fun merge_ss(SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac},
|
|
94 |
SS{simps=simps2,congs=congs2,...}) =
|
|
95 |
let val simps' = gen_union eq_thm (simps,simps2)
|
|
96 |
val congs' = gen_union eq_thm (congs,congs2)
|
|
97 |
val mss' = Thm.set_mk_rews(empty_mss,Thm.mk_rews_of_mss mss)
|
|
98 |
val mss' = Thm.add_simps(mss',simps')
|
|
99 |
val mss' = Thm.add_congs(mss',congs')
|
|
100 |
in SS{mss= mss',
|
|
101 |
simps= simps,
|
|
102 |
congs= congs',
|
|
103 |
subgoal_tac= subgoal_tac,
|
|
104 |
finish_tac= finish_tac,
|
|
105 |
loop_tac= loop_tac}
|
|
106 |
end;
|
|
107 |
|
|
108 |
fun prems_of_ss(SS{mss,...}) = prems_of_mss mss;
|
|
109 |
|
|
110 |
fun rep_ss(SS{simps,congs,...}) = {simps=simps,congs=congs};
|
|
111 |
|
|
112 |
fun add_asms (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) prems =
|
|
113 |
let val rews = flat(map (mk_rews_of_mss mss) prems)
|
|
114 |
in SS{mss= add_prems(add_simps(mss,rews),prems), simps=simps, congs=congs,
|
|
115 |
subgoal_tac=subgoal_tac,finish_tac=finish_tac,
|
|
116 |
loop_tac=loop_tac}
|
|
117 |
end;
|
|
118 |
|
|
119 |
fun asm_full_simp_tac(SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) =
|
|
120 |
let fun solve_all_tac mss =
|
|
121 |
let val ss = SS{mss=mss,simps=simps,congs=congs,
|
|
122 |
subgoal_tac=subgoal_tac,
|
|
123 |
finish_tac=finish_tac, loop_tac=loop_tac}
|
|
124 |
fun solve1 thm = tapply(
|
|
125 |
STATE(fn state => let val n = nprems_of state
|
|
126 |
in if n=0 then all_tac
|
|
127 |
else subgoal_tac ss 1 THEN
|
|
128 |
COND (has_fewer_prems n) (Tactic solve1) no_tac
|
|
129 |
end),
|
|
130 |
thm)
|
|
131 |
in DEPTH_SOLVE(Tactic solve1) end
|
|
132 |
|
|
133 |
fun simp_loop i thm =
|
|
134 |
tapply(asm_rewrite_goal_tac solve_all_tac mss i THEN
|
|
135 |
(finish_tac (prems_of_mss mss) i ORELSE STATE(looper i)),
|
|
136 |
thm)
|
|
137 |
and allsimp i m state =
|
|
138 |
let val n = nprems_of state
|
|
139 |
in EVERY(map (fn j => simp_loop_tac (i+j)) ((n-m) downto 0)) end
|
|
140 |
and looper i state =
|
|
141 |
TRY(loop_tac i THEN STATE(allsimp i (nprems_of state)))
|
|
142 |
and simp_loop_tac i = Tactic(simp_loop i)
|
|
143 |
|
|
144 |
in simp_loop_tac end;
|
|
145 |
|
|
146 |
fun asm_simp_tac ss =
|
|
147 |
METAHYPS(fn prems => asm_full_simp_tac (add_asms ss prems) 1);
|
|
148 |
|
|
149 |
fun simp_tac ss = METAHYPS(fn _ => asm_full_simp_tac ss 1);
|
|
150 |
|
|
151 |
end;
|