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