author | berghofe |
Sun, 10 Jan 2010 18:09:11 +0100 | |
changeset 34910 | b23bd3ee4813 |
parent 33519 | e31a85f92ce9 |
child 35021 | c839a4c670c6 |
permissions | -rw-r--r-- |
28308 | 1 |
(* Title: HOL/Statespace/state_fun.ML |
25171 | 2 |
Author: Norbert Schirmer, TU Muenchen |
3 |
*) |
|
4 |
||
25408 | 5 |
signature STATE_FUN = |
6 |
sig |
|
7 |
val lookupN : string |
|
8 |
val updateN : string |
|
25171 | 9 |
|
29302 | 10 |
val mk_constr : theory -> typ -> term |
11 |
val mk_destr : theory -> typ -> term |
|
25408 | 12 |
|
29302 | 13 |
val lookup_simproc : simproc |
14 |
val update_simproc : simproc |
|
15 |
val ex_lookup_eq_simproc : simproc |
|
16 |
val ex_lookup_ss : simpset |
|
17 |
val lazy_conj_simproc : simproc |
|
18 |
val string_eq_simp_tac : int -> tactic |
|
25408 | 19 |
|
29302 | 20 |
val setup : theory -> theory |
25408 | 21 |
end; |
22 |
||
23 |
structure StateFun: STATE_FUN = |
|
25171 | 24 |
struct |
25 |
||
26 |
val lookupN = "StateFun.lookup"; |
|
27 |
val updateN = "StateFun.update"; |
|
28 |
||
25408 | 29 |
val sel_name = HOLogic.dest_string; |
25171 | 30 |
|
31 |
fun mk_name i t = |
|
32 |
(case try sel_name t of |
|
33 |
SOME name => name |
|
34 |
| NONE => (case t of |
|
35 |
Free (x,_) => x |
|
36 |
|Const (x,_) => x |
|
37 |
|_ => "x"^string_of_int i)) |
|
38 |
||
39 |
local |
|
32921 | 40 |
|
25171 | 41 |
val conj1_False = thm "conj1_False"; |
42 |
val conj2_False = thm "conj2_False"; |
|
43 |
val conj_True = thm "conj_True"; |
|
44 |
val conj_cong = thm "conj_cong"; |
|
32921 | 45 |
|
25171 | 46 |
fun isFalse (Const ("False",_)) = true |
47 |
| isFalse _ = false; |
|
48 |
fun isTrue (Const ("True",_)) = true |
|
49 |
| isTrue _ = false; |
|
50 |
||
51 |
in |
|
32921 | 52 |
|
25171 | 53 |
val lazy_conj_simproc = |
29064 | 54 |
Simplifier.simproc @{theory HOL} "lazy_conj_simp" ["P & Q"] |
25171 | 55 |
(fn thy => fn ss => fn t => |
56 |
(case t of (Const ("op &",_)$P$Q) => |
|
57 |
let |
|
58 |
val P_P' = Simplifier.rewrite ss (cterm_of thy P); |
|
59 |
val P' = P_P' |> prop_of |> Logic.dest_equals |> #2 |
|
60 |
in if isFalse P' |
|
61 |
then SOME (conj1_False OF [P_P']) |
|
62 |
else |
|
63 |
let |
|
64 |
val Q_Q' = Simplifier.rewrite ss (cterm_of thy Q); |
|
65 |
val Q' = Q_Q' |> prop_of |> Logic.dest_equals |> #2 |
|
66 |
in if isFalse Q' |
|
67 |
then SOME (conj2_False OF [Q_Q']) |
|
68 |
else if isTrue P' andalso isTrue Q' |
|
69 |
then SOME (conj_True OF [P_P', Q_Q']) |
|
70 |
else if P aconv P' andalso Q aconv Q' then NONE |
|
71 |
else SOME (conj_cong OF [P_P', Q_Q']) |
|
72 |
end |
|
73 |
end |
|
74 |
||
75 |
| _ => NONE)); |
|
76 |
||
32921 | 77 |
val string_eq_simp_tac = simp_tac (HOL_basic_ss |
78 |
addsimps (@{thms list.inject} @ @{thms char.inject} |
|
79 |
@ @{thms list.distinct} @ @{thms char.distinct} @ simp_thms) |
|
80 |
addsimprocs [lazy_conj_simproc] |
|
81 |
addcongs [@{thm block_conj_cong}]) |
|
82 |
||
25171 | 83 |
end; |
84 |
||
32921 | 85 |
val lookup_ss = (HOL_basic_ss |
86 |
addsimps (@{thms list.inject} @ @{thms char.inject} |
|
87 |
@ @{thms list.distinct} @ @{thms char.distinct} @ simp_thms |
|
88 |
@ [@{thm StateFun.lookup_update_id_same}, @{thm StateFun.id_id_cancel}, |
|
89 |
@{thm StateFun.lookup_update_same}, @{thm StateFun.lookup_update_other}]) |
|
90 |
addsimprocs [lazy_conj_simproc] |
|
91 |
addcongs @{thms block_conj_cong} |
|
92 |
addSolver StateSpace.distinctNameSolver); |
|
25171 | 93 |
|
32921 | 94 |
val ex_lookup_ss = HOL_ss addsimps @{thms StateFun.ex_id}; |
25171 | 95 |
|
33519 | 96 |
|
97 |
structure StateFunData = Generic_Data |
|
98 |
( |
|
99 |
type T = simpset * simpset * bool; |
|
25171 | 100 |
(* lookup simpset, ex_lookup simpset, are simprocs installed *) |
101 |
val empty = (empty_ss, empty_ss, false); |
|
102 |
val extend = I; |
|
33519 | 103 |
fun merge ((ss1, ex_ss1, b1), (ss2, ex_ss2, b2)) = |
104 |
(merge_ss (ss1, ss2), merge_ss (ex_ss1, ex_ss2), b1 orelse b2); |
|
105 |
); |
|
25171 | 106 |
|
107 |
val init_state_fun_data = |
|
108 |
Context.theory_map (StateFunData.put (lookup_ss,ex_lookup_ss,false)); |
|
109 |
||
110 |
val lookup_simproc = |
|
32010 | 111 |
Simplifier.simproc @{theory} "lookup_simp" ["lookup d n (update d' c m v s)"] |
25171 | 112 |
(fn thy => fn ss => fn t => |
113 |
(case t of (Const ("StateFun.lookup",lT)$destr$n$ |
|
114 |
(s as Const ("StateFun.update",uT)$_$_$_$_$_)) => |
|
115 |
(let |
|
116 |
val (_::_::_::_::sT::_) = binder_types uT; |
|
117 |
val mi = maxidx_of_term t; |
|
118 |
fun mk_upds (Const ("StateFun.update",uT)$d'$c$m$v$s) = |
|
119 |
let |
|
120 |
val (_::_::_::fT::_::_) = binder_types uT; |
|
121 |
val vT = domain_type fT; |
|
122 |
val (s',cnt) = mk_upds s; |
|
123 |
val (v',cnt') = |
|
124 |
(case v of |
|
125 |
Const ("StateFun.K_statefun",KT)$v'' |
|
126 |
=> (case v'' of |
|
127 |
(Const ("StateFun.lookup",_)$(d as (Const ("Fun.id",_)))$n'$_) |
|
128 |
=> if d aconv c andalso n aconv m andalso m aconv n' |
|
129 |
then (v,cnt) (* Keep value so that |
|
130 |
lookup_update_id_same can fire *) |
|
131 |
else (Const ("StateFun.K_statefun",KT)$Var (("v",cnt),vT), |
|
132 |
cnt+1) |
|
133 |
| _ => (Const ("StateFun.K_statefun",KT)$Var (("v",cnt),vT), |
|
134 |
cnt+1)) |
|
135 |
| _ => (v,cnt)); |
|
136 |
in (Const ("StateFun.update",uT)$d'$c$m$v'$s',cnt') |
|
137 |
end |
|
138 |
| mk_upds s = (Var (("s",mi+1),sT),mi+2); |
|
139 |
||
140 |
val ct = cterm_of thy |
|
141 |
(Const ("StateFun.lookup",lT)$destr$n$(fst (mk_upds s))); |
|
30289 | 142 |
val ctxt = Simplifier.the_context ss; |
25171 | 143 |
val basic_ss = #1 (StateFunData.get (Context.Proof ctxt)); |
144 |
val ss' = Simplifier.context |
|
145 |
(Config.map MetaSimplifier.simp_depth_limit (K 100) ctxt) basic_ss; |
|
146 |
val thm = Simplifier.rewrite ss' ct; |
|
147 |
in if (op aconv) (Logic.dest_equals (prop_of thm)) |
|
148 |
then NONE |
|
149 |
else SOME thm |
|
150 |
end |
|
151 |
handle Option => NONE) |
|
152 |
||
153 |
| _ => NONE )); |
|
154 |
||
155 |
||
156 |
local |
|
32921 | 157 |
val meta_ext = @{thm StateFun.meta_ext}; |
158 |
val ss' = (HOL_ss addsimps |
|
159 |
(@{thm StateFun.update_apply} :: @{thm Fun.o_apply} :: @{thms list.inject} @ @{thms char.inject} |
|
160 |
@ @{thms list.distinct} @ @{thms char.distinct}) |
|
161 |
addsimprocs [lazy_conj_simproc, StateSpace.distinct_simproc] |
|
162 |
addcongs @{thms block_conj_cong}); |
|
25171 | 163 |
in |
164 |
val update_simproc = |
|
32010 | 165 |
Simplifier.simproc @{theory} "update_simp" ["update d c n v s"] |
25171 | 166 |
(fn thy => fn ss => fn t => |
167 |
(case t of ((upd as Const ("StateFun.update", uT)) $ d $ c $ n $ v $ s) => |
|
168 |
let |
|
169 |
||
170 |
val (_::_::_::_::sT::_) = binder_types uT; |
|
171 |
(*"('v => 'a1) => ('a2 => 'v) => 'n => ('a1 => 'a2) => ('n => 'v) => ('n => 'v)"*) |
|
172 |
fun init_seed s = (Bound 0,Bound 0, [("s",sT)],[], false); |
|
173 |
||
174 |
fun mk_comp f fT g gT = |
|
175 |
let val T = (domain_type fT --> range_type gT) |
|
176 |
in (Const ("Fun.comp",gT --> fT --> T)$g$f,T) end |
|
177 |
||
178 |
fun mk_comps fs = |
|
33003
1c93cfa807bc
eliminated duplicate fold1 -- beware of argument order!
wenzelm
parents:
32960
diff
changeset
|
179 |
foldl1 (fn ((f,fT),(g,gT)) => mk_comp g gT f fT) fs; |
25171 | 180 |
|
181 |
fun append n c cT f fT d dT comps = |
|
182 |
(case AList.lookup (op aconv) comps n of |
|
183 |
SOME gTs => AList.update (op aconv) |
|
184 |
(n,[(c,cT),(f,fT),(d,dT)]@gTs) comps |
|
185 |
| NONE => AList.update (op aconv) (n,[(c,cT),(f,fT),(d,dT)]) comps) |
|
186 |
||
187 |
fun split_list (x::xs) = let val (xs',y) = split_last xs in (x,xs',y) end |
|
188 |
| split_list _ = error "StateFun.split_list"; |
|
189 |
||
190 |
fun merge_upds n comps = |
|
191 |
let val ((c,cT),fs,(d,dT)) = split_list (the (AList.lookup (op aconv) comps n)) |
|
192 |
in ((c,cT),fst (mk_comps fs),(d,dT)) end; |
|
193 |
||
194 |
(* mk_updterm returns |
|
195 |
* - (orig-term-skeleton,simplified-term-skeleton, vars, b) |
|
196 |
* where boolean b tells if a simplification has occured. |
|
197 |
"orig-term-skeleton = simplified-term-skeleton" is |
|
198 |
* the desired simplification rule. |
|
199 |
* The algorithm first walks down the updates to the seed-state while |
|
200 |
* memorising the updates in the already-table. While walking up the |
|
201 |
* updates again, the optimised term is constructed. |
|
202 |
*) |
|
203 |
fun mk_updterm already |
|
204 |
(t as ((upd as Const ("StateFun.update", uT)) $ d $ c $ n $ v $ s)) = |
|
205 |
let |
|
206 |
fun rest already = mk_updterm already; |
|
207 |
val (dT::cT::nT::vT::sT::_) = binder_types uT; |
|
208 |
(*"('v => 'a1) => ('a2 => 'v) => 'n => ('a1 => 'a2) => |
|
209 |
('n => 'v) => ('n => 'v)"*) |
|
210 |
in if member (op aconv) already n |
|
211 |
then (case rest already s of |
|
212 |
(trm,trm',vars,comps,_) => |
|
213 |
let |
|
214 |
val i = length vars; |
|
215 |
val kv = (mk_name i n,vT); |
|
216 |
val kb = Bound i; |
|
217 |
val comps' = append n c cT kb vT d dT comps; |
|
218 |
in (upd$d$c$n$kb$trm, trm', kv::vars,comps',true) end) |
|
219 |
else |
|
220 |
(case rest (n::already) s of |
|
221 |
(trm,trm',vars,comps,b) => |
|
222 |
let |
|
223 |
val i = length vars; |
|
224 |
val kv = (mk_name i n,vT); |
|
225 |
val kb = Bound i; |
|
226 |
val comps' = append n c cT kb vT d dT comps; |
|
227 |
val ((c',c'T),f',(d',d'T)) = merge_upds n comps'; |
|
228 |
val vT' = range_type d'T --> domain_type c'T; |
|
229 |
val upd' = Const ("StateFun.update",d'T --> c'T --> nT --> vT' --> sT --> sT); |
|
230 |
in (upd$d$c$n$kb$trm, upd'$d'$c'$n$f'$trm', kv::vars,comps',b) |
|
231 |
end) |
|
232 |
end |
|
233 |
| mk_updterm _ t = init_seed t; |
|
234 |
||
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
235 |
val ctxt = Simplifier.the_context ss |> |
25171 | 236 |
Config.map MetaSimplifier.simp_depth_limit (K 100); |
237 |
val ss1 = Simplifier.context ctxt ss'; |
|
238 |
val ss2 = Simplifier.context ctxt |
|
239 |
(#1 (StateFunData.get (Context.Proof ctxt))); |
|
240 |
in (case mk_updterm [] t of |
|
241 |
(trm,trm',vars,_,true) |
|
242 |
=> let |
|
243 |
val eq1 = Goal.prove ctxt [] [] |
|
27330 | 244 |
(list_all (vars, Logic.mk_equals (trm, trm'))) |
25171 | 245 |
(fn _ => rtac meta_ext 1 THEN |
246 |
simp_tac ss1 1); |
|
247 |
val eq2 = Simplifier.asm_full_rewrite ss2 (Thm.dest_equals_rhs (cprop_of eq1)); |
|
248 |
in SOME (transitive eq1 eq2) end |
|
249 |
| _ => NONE) |
|
250 |
end |
|
251 |
| _ => NONE)); |
|
252 |
end |
|
253 |
||
254 |
||
255 |
||
256 |
||
257 |
local |
|
258 |
val swap_ex_eq = thm "StateFun.swap_ex_eq"; |
|
259 |
fun is_selector thy T sel = |
|
260 |
let |
|
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
30528
diff
changeset
|
261 |
val (flds,more) = Record.get_recT_fields thy T |
25171 | 262 |
in member (fn (s,(n,_)) => n=s) (more::flds) sel |
263 |
end; |
|
264 |
in |
|
265 |
val ex_lookup_eq_simproc = |
|
29064 | 266 |
Simplifier.simproc @{theory HOL} "ex_lookup_eq_simproc" ["Ex t"] |
25171 | 267 |
(fn thy => fn ss => fn t => |
268 |
let |
|
269 |
val ctxt = Simplifier.the_context ss |> |
|
270 |
Config.map MetaSimplifier.simp_depth_limit (K 100) |
|
271 |
val ex_lookup_ss = #2 (StateFunData.get (Context.Proof ctxt)); |
|
272 |
val ss' = (Simplifier.context ctxt ex_lookup_ss); |
|
273 |
fun prove prop = |
|
274 |
Goal.prove_global thy [] [] prop |
|
275 |
(fn _ => record_split_simp_tac [] (K ~1) 1 THEN |
|
276 |
simp_tac ss' 1); |
|
277 |
||
278 |
fun mkeq (swap,Teq,lT,lo,d,n,x,s) i = |
|
279 |
let val (_::nT::_) = binder_types lT; |
|
280 |
(* ('v => 'a) => 'n => ('n => 'v) => 'a *) |
|
281 |
val x' = if not (loose_bvar1 (x,0)) |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
282 |
then Bound 1 |
25171 | 283 |
else raise TERM ("",[x]); |
284 |
val n' = if not (loose_bvar1 (n,0)) |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
285 |
then Bound 2 |
25171 | 286 |
else raise TERM ("",[n]); |
287 |
val sel' = lo $ d $ n' $ s; |
|
288 |
in (Const ("op =",Teq)$sel'$x',hd (binder_types Teq),nT,swap) end; |
|
289 |
||
290 |
fun dest_state (s as Bound 0) = s |
|
291 |
| dest_state (s as (Const (sel,sT)$Bound 0)) = |
|
292 |
if is_selector thy (domain_type sT) sel |
|
293 |
then s |
|
294 |
else raise TERM ("StateFun.ex_lookup_eq_simproc: not a record slector",[s]) |
|
295 |
| dest_state s = |
|
296 |
raise TERM ("StateFun.ex_lookup_eq_simproc: not a record slector",[s]); |
|
297 |
||
298 |
fun dest_sel_eq (Const ("op =",Teq)$ |
|
299 |
((lo as (Const ("StateFun.lookup",lT)))$d$n$s)$X) = |
|
300 |
(false,Teq,lT,lo,d,n,X,dest_state s) |
|
301 |
| dest_sel_eq (Const ("op =",Teq)$X$ |
|
302 |
((lo as (Const ("StateFun.lookup",lT)))$d$n$s)) = |
|
303 |
(true,Teq,lT,lo,d,n,X,dest_state s) |
|
304 |
| dest_sel_eq _ = raise TERM ("",[]); |
|
305 |
||
306 |
in |
|
307 |
(case t of |
|
308 |
(Const ("Ex",Tex)$Abs(s,T,t)) => |
|
309 |
(let val (eq,eT,nT,swap) = mkeq (dest_sel_eq t) 0; |
|
310 |
val prop = list_all ([("n",nT),("x",eT)], |
|
311 |
Logic.mk_equals (Const ("Ex",Tex)$Abs(s,T,eq), |
|
312 |
HOLogic.true_const)); |
|
32957 | 313 |
val thm = Drule.standard (prove prop); |
25171 | 314 |
val thm' = if swap then swap_ex_eq OF [thm] else thm |
315 |
in SOME thm' end |
|
316 |
handle TERM _ => NONE) |
|
317 |
| _ => NONE) |
|
318 |
end handle Option => NONE) |
|
319 |
end; |
|
320 |
||
321 |
val val_sfx = "V"; |
|
322 |
val val_prfx = "StateFun." |
|
323 |
fun deco base_prfx s = val_prfx ^ (base_prfx ^ suffix val_sfx s); |
|
324 |
||
325 |
fun mkUpper str = |
|
326 |
(case String.explode str of |
|
327 |
[] => "" |
|
328 |
| c::cs => String.implode (Char.toUpper c::cs )) |
|
329 |
||
32952 | 330 |
fun mkName (Type (T,args)) = implode (map mkName args) ^ mkUpper (Long_Name.base_name T) |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30289
diff
changeset
|
331 |
| mkName (TFree (x,_)) = mkUpper (Long_Name.base_name x) |
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30289
diff
changeset
|
332 |
| mkName (TVar ((x,_),_)) = mkUpper (Long_Name.base_name x); |
25171 | 333 |
|
31784 | 334 |
fun is_datatype thy = is_some o Datatype.get_info thy; |
25171 | 335 |
|
30280 | 336 |
fun mk_map "List.list" = Syntax.const "List.map" |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30289
diff
changeset
|
337 |
| mk_map n = Syntax.const ("StateFun.map_" ^ Long_Name.base_name n); |
25171 | 338 |
|
339 |
fun gen_constr_destr comp prfx thy (Type (T,[])) = |
|
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30289
diff
changeset
|
340 |
Syntax.const (deco prfx (mkUpper (Long_Name.base_name T))) |
25171 | 341 |
| gen_constr_destr comp prfx thy (T as Type ("fun",_)) = |
342 |
let val (argTs,rangeT) = strip_type T; |
|
343 |
in comp |
|
32952 | 344 |
(Syntax.const (deco prfx (implode (map mkName argTs) ^ "Fun"))) |
25171 | 345 |
(fold (fn x => fn y => x$y) |
346 |
(replicate (length argTs) (Syntax.const "StateFun.map_fun")) |
|
347 |
(gen_constr_destr comp prfx thy rangeT)) |
|
348 |
end |
|
349 |
| gen_constr_destr comp prfx thy (T' as Type (T,argTs)) = |
|
350 |
if is_datatype thy T |
|
351 |
then (* datatype args are recursively embedded into val *) |
|
352 |
(case argTs of |
|
353 |
[argT] => comp |
|
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30289
diff
changeset
|
354 |
((Syntax.const (deco prfx (mkUpper (Long_Name.base_name T))))) |
25171 | 355 |
((mk_map T $ gen_constr_destr comp prfx thy argT)) |
356 |
| _ => raise (TYPE ("StateFun.gen_constr_destr",[T'],[]))) |
|
357 |
else (* type args are not recursively embedded into val *) |
|
32952 | 358 |
Syntax.const (deco prfx (implode (map mkName argTs) ^ mkUpper (Long_Name.base_name T))) |
25171 | 359 |
| gen_constr_destr thy _ _ T = raise (TYPE ("StateFun.gen_constr_destr",[T],[])); |
360 |
||
361 |
val mk_constr = gen_constr_destr (fn a => fn b => Syntax.const "Fun.comp" $ a $ b) "" |
|
362 |
val mk_destr = gen_constr_destr (fn a => fn b => Syntax.const "Fun.comp" $ b $ a) "the_" |
|
363 |
||
364 |
||
30528 | 365 |
val statefun_simp_attr = Thm.declaration_attribute (fn thm => fn ctxt => |
25171 | 366 |
let |
367 |
val (lookup_ss,ex_lookup_ss,simprocs_active) = StateFunData.get ctxt; |
|
368 |
val (lookup_ss', ex_lookup_ss') = |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
369 |
(case (concl_of thm) of |
25171 | 370 |
(_$((Const ("Ex",_)$_))) => (lookup_ss, ex_lookup_ss addsimps [thm]) |
371 |
| _ => (lookup_ss addsimps [thm], ex_lookup_ss)) |
|
372 |
fun activate_simprocs ctxt = |
|
373 |
if simprocs_active then ctxt |
|
26496
49ae9456eba9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
25408
diff
changeset
|
374 |
else Simplifier.map_ss (fn ss => ss addsimprocs [lookup_simproc,update_simproc]) ctxt |
30528 | 375 |
in |
376 |
ctxt |
|
377 |
|> activate_simprocs |
|
378 |
|> (StateFunData.put (lookup_ss',ex_lookup_ss',true)) |
|
379 |
end); |
|
25171 | 380 |
|
381 |
val setup = |
|
30528 | 382 |
init_state_fun_data #> |
383 |
Attrib.setup @{binding statefun_simp} (Scan.succeed statefun_simp_attr) |
|
384 |
"simplification in statespaces" |
|
25171 | 385 |
end |