1.1 --- a/src/HOL/Statespace/state_fun.ML Sun Nov 06 17:53:32 2011 +0100
1.2 +++ b/src/HOL/Statespace/state_fun.ML Sun Nov 06 18:42:15 2011 +0100
1.3 @@ -20,22 +20,23 @@
1.4 val setup : theory -> theory
1.5 end;
1.6
1.7 -structure StateFun: STATE_FUN =
1.8 +structure StateFun: STATE_FUN =
1.9 struct
1.10
1.11 -val lookupN = "StateFun.lookup";
1.12 -val updateN = "StateFun.update";
1.13 +val lookupN = @{const_name StateFun.lookup};
1.14 +val updateN = @{const_name StateFun.update};
1.15
1.16 val sel_name = HOLogic.dest_string;
1.17
1.18 fun mk_name i t =
1.19 (case try sel_name t of
1.20 - SOME name => name
1.21 - | NONE => (case t of
1.22 - Free (x,_) => x
1.23 - |Const (x,_) => x
1.24 - |_ => "x"^string_of_int i))
1.25 -
1.26 + SOME name => name
1.27 + | NONE =>
1.28 + (case t of
1.29 + Free (x, _) => x
1.30 + | Const (x, _) => x
1.31 + | _ => "x" ^ string_of_int i));
1.32 +
1.33 local
1.34
1.35 val conj1_False = @{thm conj1_False};
1.36 @@ -43,9 +44,10 @@
1.37 val conj_True = @{thm conj_True};
1.38 val conj_cong = @{thm conj_cong};
1.39
1.40 -fun isFalse (Const (@{const_name False},_)) = true
1.41 +fun isFalse (Const (@{const_name False}, _)) = true
1.42 | isFalse _ = false;
1.43 -fun isTrue (Const (@{const_name True},_)) = true
1.44 +
1.45 +fun isTrue (Const (@{const_name True}, _)) = true
1.46 | isTrue _ = false;
1.47
1.48 in
1.49 @@ -53,36 +55,34 @@
1.50 val lazy_conj_simproc =
1.51 Simplifier.simproc_global @{theory HOL} "lazy_conj_simp" ["P & Q"]
1.52 (fn thy => fn ss => fn t =>
1.53 - (case t of (Const (@{const_name HOL.conj},_)$P$Q) =>
1.54 - let
1.55 - val P_P' = Simplifier.rewrite ss (cterm_of thy P);
1.56 - val P' = P_P' |> prop_of |> Logic.dest_equals |> #2
1.57 - in if isFalse P'
1.58 - then SOME (conj1_False OF [P_P'])
1.59 - else
1.60 - let
1.61 - val Q_Q' = Simplifier.rewrite ss (cterm_of thy Q);
1.62 - val Q' = Q_Q' |> prop_of |> Logic.dest_equals |> #2
1.63 - in if isFalse Q'
1.64 - then SOME (conj2_False OF [Q_Q'])
1.65 - else if isTrue P' andalso isTrue Q'
1.66 - then SOME (conj_True OF [P_P', Q_Q'])
1.67 - else if P aconv P' andalso Q aconv Q' then NONE
1.68 - else SOME (conj_cong OF [P_P', Q_Q'])
1.69 - end
1.70 + (case t of (Const (@{const_name HOL.conj},_) $ P $ Q) =>
1.71 + let
1.72 + val P_P' = Simplifier.rewrite ss (cterm_of thy P);
1.73 + val P' = P_P' |> prop_of |> Logic.dest_equals |> #2;
1.74 + in
1.75 + if isFalse P' then SOME (conj1_False OF [P_P'])
1.76 + else
1.77 + let
1.78 + val Q_Q' = Simplifier.rewrite ss (cterm_of thy Q);
1.79 + val Q' = Q_Q' |> prop_of |> Logic.dest_equals |> #2;
1.80 + in
1.81 + if isFalse Q' then SOME (conj2_False OF [Q_Q'])
1.82 + else if isTrue P' andalso isTrue Q' then SOME (conj_True OF [P_P', Q_Q'])
1.83 + else if P aconv P' andalso Q aconv Q' then NONE
1.84 + else SOME (conj_cong OF [P_P', Q_Q'])
1.85 + end
1.86 end
1.87 -
1.88 | _ => NONE));
1.89
1.90 -val string_eq_simp_tac = simp_tac (HOL_basic_ss
1.91 +val string_eq_simp_tac = simp_tac (HOL_basic_ss
1.92 addsimps (@{thms list.inject} @ @{thms char.inject}
1.93 @ @{thms list.distinct} @ @{thms char.distinct} @ @{thms simp_thms})
1.94 addsimprocs [lazy_conj_simproc]
1.95 - addcongs [@{thm block_conj_cong}])
1.96 + addcongs [@{thm block_conj_cong}]);
1.97
1.98 end;
1.99
1.100 -val lookup_ss = (HOL_basic_ss
1.101 +val lookup_ss = (HOL_basic_ss
1.102 addsimps (@{thms list.inject} @ @{thms char.inject}
1.103 @ @{thms list.distinct} @ @{thms char.distinct} @ @{thms simp_thms}
1.104 @ [@{thm StateFun.lookup_update_id_same}, @{thm StateFun.id_id_cancel},
1.105 @@ -94,235 +94,238 @@
1.106 val ex_lookup_ss = HOL_ss addsimps @{thms StateFun.ex_id};
1.107
1.108
1.109 -structure StateFunData = Generic_Data
1.110 +structure Data = Generic_Data
1.111 (
1.112 - type T = simpset * simpset * bool;
1.113 - (* lookup simpset, ex_lookup simpset, are simprocs installed *)
1.114 + type T = simpset * simpset * bool; (*lookup simpset, ex_lookup simpset, are simprocs installed*)
1.115 val empty = (empty_ss, empty_ss, false);
1.116 val extend = I;
1.117 fun merge ((ss1, ex_ss1, b1), (ss2, ex_ss2, b2)) =
1.118 - (merge_ss (ss1, ss2), merge_ss (ex_ss1, ex_ss2), b1 orelse b2 (* FIXME odd merge *));
1.119 + (merge_ss (ss1, ss2), merge_ss (ex_ss1, ex_ss2), b1 orelse b2);
1.120 );
1.121
1.122 val init_state_fun_data =
1.123 - Context.theory_map (StateFunData.put (lookup_ss,ex_lookup_ss,false));
1.124 + Context.theory_map (Data.put (lookup_ss, ex_lookup_ss, false));
1.125
1.126 val lookup_simproc =
1.127 Simplifier.simproc_global @{theory} "lookup_simp" ["lookup d n (update d' c m v s)"]
1.128 (fn thy => fn ss => fn t =>
1.129 - (case t of (Const ("StateFun.lookup",lT)$destr$n$
1.130 - (s as Const ("StateFun.update",uT)$_$_$_$_$_)) =>
1.131 + (case t of (Const (@{const_name StateFun.lookup}, lT) $ destr $ n $
1.132 + (s as Const (@{const_name StateFun.update}, uT) $ _ $ _ $ _ $ _ $ _)) =>
1.133 (let
1.134 val (_::_::_::_::sT::_) = binder_types uT;
1.135 val mi = maxidx_of_term t;
1.136 - fun mk_upds (Const ("StateFun.update",uT)$d'$c$m$v$s) =
1.137 - let
1.138 - val (_::_::_::fT::_::_) = binder_types uT;
1.139 - val vT = domain_type fT;
1.140 - val (s',cnt) = mk_upds s;
1.141 - val (v',cnt') =
1.142 - (case v of
1.143 - Const ("StateFun.K_statefun",KT)$v''
1.144 - => (case v'' of
1.145 - (Const ("StateFun.lookup",_)$(d as (Const ("Fun.id",_)))$n'$_)
1.146 - => if d aconv c andalso n aconv m andalso m aconv n'
1.147 - then (v,cnt) (* Keep value so that
1.148 - lookup_update_id_same can fire *)
1.149 - else (Const ("StateFun.K_statefun",KT)$Var (("v",cnt),vT),
1.150 - cnt+1)
1.151 - | _ => (Const ("StateFun.K_statefun",KT)$Var (("v",cnt),vT),
1.152 - cnt+1))
1.153 - | _ => (v,cnt));
1.154 - in (Const ("StateFun.update",uT)$d'$c$m$v'$s',cnt')
1.155 - end
1.156 - | mk_upds s = (Var (("s",mi+1),sT),mi+2);
1.157 -
1.158 - val ct = cterm_of thy
1.159 - (Const ("StateFun.lookup",lT)$destr$n$(fst (mk_upds s)));
1.160 + fun mk_upds (Const (@{const_name StateFun.update}, uT) $ d' $ c $ m $ v $ s) =
1.161 + let
1.162 + val (_ :: _ :: _ :: fT :: _ :: _) = binder_types uT;
1.163 + val vT = domain_type fT;
1.164 + val (s', cnt) = mk_upds s;
1.165 + val (v', cnt') =
1.166 + (case v of
1.167 + Const (@{const_name K_statefun}, KT) $ v'' =>
1.168 + (case v'' of
1.169 + (Const (@{const_name StateFun.lookup}, _) $
1.170 + (d as (Const (@{const_name Fun.id}, _))) $ n' $ _) =>
1.171 + if d aconv c andalso n aconv m andalso m aconv n'
1.172 + then (v,cnt) (* Keep value so that
1.173 + lookup_update_id_same can fire *)
1.174 + else
1.175 + (Const (@{const_name StateFun.K_statefun}, KT) $
1.176 + Var (("v", cnt), vT), cnt + 1)
1.177 + | _ =>
1.178 + (Const (@{const_name StateFun.K_statefun}, KT) $
1.179 + Var (("v", cnt), vT), cnt + 1))
1.180 + | _ => (v, cnt));
1.181 + in (Const (@{const_name StateFun.update}, uT) $ d' $ c $ m $ v' $ s', cnt') end
1.182 + | mk_upds s = (Var (("s", mi + 1), sT), mi + 2);
1.183 +
1.184 + val ct =
1.185 + cterm_of thy (Const (@{const_name StateFun.lookup}, lT) $ destr $ n $ fst (mk_upds s));
1.186 val ctxt = Simplifier.the_context ss;
1.187 - val basic_ss = #1 (StateFunData.get (Context.Proof ctxt));
1.188 + val basic_ss = #1 (Data.get (Context.Proof ctxt));
1.189 val ss' = Simplifier.context (Config.put simp_depth_limit 100 ctxt) basic_ss;
1.190 val thm = Simplifier.rewrite ss' ct;
1.191 - in if (op aconv) (Logic.dest_equals (prop_of thm))
1.192 - then NONE
1.193 - else SOME thm
1.194 + in
1.195 + if (op aconv) (Logic.dest_equals (prop_of thm))
1.196 + then NONE
1.197 + else SOME thm
1.198 end
1.199 handle Option.Option => NONE)
1.200 -
1.201 | _ => NONE ));
1.202
1.203
1.204 local
1.205 +
1.206 val meta_ext = @{thm StateFun.meta_ext};
1.207 val ss' = (HOL_ss addsimps
1.208 (@{thm StateFun.update_apply} :: @{thm Fun.o_apply} :: @{thms list.inject} @ @{thms char.inject}
1.209 @ @{thms list.distinct} @ @{thms char.distinct})
1.210 addsimprocs [lazy_conj_simproc, StateSpace.distinct_simproc]
1.211 addcongs @{thms block_conj_cong});
1.212 +
1.213 in
1.214 +
1.215 val update_simproc =
1.216 Simplifier.simproc_global @{theory} "update_simp" ["update d c n v s"]
1.217 (fn thy => fn ss => fn t =>
1.218 - (case t of ((upd as Const ("StateFun.update", uT)) $ d $ c $ n $ v $ s) =>
1.219 - let
1.220 -
1.221 - val (_::_::_::_::sT::_) = binder_types uT;
1.222 - (*"('v => 'a1) => ('a2 => 'v) => 'n => ('a1 => 'a2) => ('n => 'v) => ('n => 'v)"*)
1.223 - fun init_seed s = (Bound 0,Bound 0, [("s",sT)],[], false);
1.224 + (case t of
1.225 + ((upd as Const ("StateFun.update", uT)) $ d $ c $ n $ v $ s) =>
1.226 + let
1.227 + val (_ :: _ :: _ :: _ :: sT :: _) = binder_types uT;
1.228 + (*"('v => 'a1) => ('a2 => 'v) => 'n => ('a1 => 'a2) => ('n => 'v) => ('n => 'v)"*)
1.229 + fun init_seed s = (Bound 0, Bound 0, [("s", sT)], [], false);
1.230
1.231 - fun mk_comp f fT g gT =
1.232 - let val T = (domain_type fT --> range_type gT)
1.233 - in (Const ("Fun.comp",gT --> fT --> T)$g$f,T) end
1.234 + fun mk_comp f fT g gT =
1.235 + let val T = domain_type fT --> range_type gT
1.236 + in (Const (@{const_name Fun.comp}, gT --> fT --> T) $ g $ f, T) end;
1.237
1.238 - fun mk_comps fs =
1.239 - foldl1 (fn ((f,fT),(g,gT)) => mk_comp g gT f fT) fs;
1.240 + fun mk_comps fs = foldl1 (fn ((f, fT), (g, gT)) => mk_comp g gT f fT) fs;
1.241
1.242 - fun append n c cT f fT d dT comps =
1.243 - (case AList.lookup (op aconv) comps n of
1.244 - SOME gTs => AList.update (op aconv)
1.245 - (n,[(c,cT),(f,fT),(d,dT)]@gTs) comps
1.246 - | NONE => AList.update (op aconv) (n,[(c,cT),(f,fT),(d,dT)]) comps)
1.247 + fun append n c cT f fT d dT comps =
1.248 + (case AList.lookup (op aconv) comps n of
1.249 + SOME gTs => AList.update (op aconv) (n, [(c, cT), (f, fT), (d, dT)] @ gTs) comps
1.250 + | NONE => AList.update (op aconv) (n, [(c, cT), (f, fT), (d, dT)]) comps);
1.251
1.252 - fun split_list (x::xs) = let val (xs',y) = split_last xs in (x,xs',y) end
1.253 - | split_list _ = error "StateFun.split_list";
1.254 + fun split_list (x :: xs) = let val (xs', y) = split_last xs in (x, xs', y) end
1.255 + | split_list _ = error "StateFun.split_list";
1.256
1.257 - fun merge_upds n comps =
1.258 - let val ((c,cT),fs,(d,dT)) = split_list (the (AList.lookup (op aconv) comps n))
1.259 - in ((c,cT),fst (mk_comps fs),(d,dT)) end;
1.260 + fun merge_upds n comps =
1.261 + let val ((c, cT), fs, (d, dT)) = split_list (the (AList.lookup (op aconv) comps n))
1.262 + in ((c, cT), fst (mk_comps fs), (d, dT)) end;
1.263
1.264 - (* mk_updterm returns
1.265 - * - (orig-term-skeleton,simplified-term-skeleton, vars, b)
1.266 - * where boolean b tells if a simplification has occurred.
1.267 - "orig-term-skeleton = simplified-term-skeleton" is
1.268 - * the desired simplification rule.
1.269 - * The algorithm first walks down the updates to the seed-state while
1.270 - * memorising the updates in the already-table. While walking up the
1.271 - * updates again, the optimised term is constructed.
1.272 - *)
1.273 - fun mk_updterm already
1.274 - (t as ((upd as Const ("StateFun.update", uT)) $ d $ c $ n $ v $ s)) =
1.275 - let
1.276 - fun rest already = mk_updterm already;
1.277 - val (dT::cT::nT::vT::sT::_) = binder_types uT;
1.278 - (*"('v => 'a1) => ('a2 => 'v) => 'n => ('a1 => 'a2) =>
1.279 - ('n => 'v) => ('n => 'v)"*)
1.280 - in if member (op aconv) already n
1.281 - then (case rest already s of
1.282 - (trm,trm',vars,comps,_) =>
1.283 - let
1.284 - val i = length vars;
1.285 - val kv = (mk_name i n,vT);
1.286 - val kb = Bound i;
1.287 - val comps' = append n c cT kb vT d dT comps;
1.288 - in (upd$d$c$n$kb$trm, trm', kv::vars,comps',true) end)
1.289 - else
1.290 - (case rest (n::already) s of
1.291 - (trm,trm',vars,comps,b) =>
1.292 - let
1.293 - val i = length vars;
1.294 - val kv = (mk_name i n,vT);
1.295 - val kb = Bound i;
1.296 - val comps' = append n c cT kb vT d dT comps;
1.297 - val ((c',c'T),f',(d',d'T)) = merge_upds n comps';
1.298 - val vT' = range_type d'T --> domain_type c'T;
1.299 - val upd' = Const ("StateFun.update",d'T --> c'T --> nT --> vT' --> sT --> sT);
1.300 - in (upd$d$c$n$kb$trm, upd'$d'$c'$n$f'$trm', kv::vars,comps',b)
1.301 - end)
1.302 - end
1.303 - | mk_updterm _ t = init_seed t;
1.304 + (* mk_updterm returns
1.305 + * - (orig-term-skeleton,simplified-term-skeleton, vars, b)
1.306 + * where boolean b tells if a simplification has occurred.
1.307 + "orig-term-skeleton = simplified-term-skeleton" is
1.308 + * the desired simplification rule.
1.309 + * The algorithm first walks down the updates to the seed-state while
1.310 + * memorising the updates in the already-table. While walking up the
1.311 + * updates again, the optimised term is constructed.
1.312 + *)
1.313 + fun mk_updterm already
1.314 + (t as ((upd as Const ("StateFun.update", uT)) $ d $ c $ n $ v $ s)) =
1.315 + let
1.316 + fun rest already = mk_updterm already;
1.317 + val (dT :: cT :: nT :: vT :: sT :: _) = binder_types uT;
1.318 + (*"('v => 'a1) => ('a2 => 'v) => 'n => ('a1 => 'a2) =>
1.319 + ('n => 'v) => ('n => 'v)"*)
1.320 + in
1.321 + if member (op aconv) already n then
1.322 + (case rest already s of
1.323 + (trm, trm', vars, comps, _) =>
1.324 + let
1.325 + val i = length vars;
1.326 + val kv = (mk_name i n, vT);
1.327 + val kb = Bound i;
1.328 + val comps' = append n c cT kb vT d dT comps;
1.329 + in (upd $ d $ c $ n $ kb $ trm, trm', kv :: vars, comps',true) end)
1.330 + else
1.331 + (case rest (n :: already) s of
1.332 + (trm, trm', vars, comps, b) =>
1.333 + let
1.334 + val i = length vars;
1.335 + val kv = (mk_name i n, vT);
1.336 + val kb = Bound i;
1.337 + val comps' = append n c cT kb vT d dT comps;
1.338 + val ((c', c'T), f', (d', d'T)) = merge_upds n comps';
1.339 + val vT' = range_type d'T --> domain_type c'T;
1.340 + val upd' =
1.341 + Const (@{const_name StateFun.update},
1.342 + d'T --> c'T --> nT --> vT' --> sT --> sT);
1.343 + in
1.344 + (upd $ d $ c $ n $ kb $ trm, upd' $ d' $ c' $ n $ f' $ trm', kv :: vars, comps', b)
1.345 + end)
1.346 + end
1.347 + | mk_updterm _ t = init_seed t;
1.348
1.349 - val ctxt = Simplifier.the_context ss |> Config.put simp_depth_limit 100;
1.350 - val ss1 = Simplifier.context ctxt ss';
1.351 - val ss2 = Simplifier.context ctxt
1.352 - (#1 (StateFunData.get (Context.Proof ctxt)));
1.353 - in (case mk_updterm [] t of
1.354 - (trm,trm',vars,_,true)
1.355 - => let
1.356 - val eq1 = Goal.prove ctxt [] []
1.357 - (list_all (vars, Logic.mk_equals (trm, trm')))
1.358 - (fn _ => rtac meta_ext 1 THEN
1.359 - simp_tac ss1 1);
1.360 - val eq2 = Simplifier.asm_full_rewrite ss2 (Thm.dest_equals_rhs (cprop_of eq1));
1.361 - in SOME (Thm.transitive eq1 eq2) end
1.362 - | _ => NONE)
1.363 - end
1.364 - | _ => NONE));
1.365 -end
1.366 + val ctxt = Simplifier.the_context ss |> Config.put simp_depth_limit 100;
1.367 + val ss1 = Simplifier.context ctxt ss';
1.368 + val ss2 = Simplifier.context ctxt (#1 (Data.get (Context.Proof ctxt)));
1.369 + in
1.370 + (case mk_updterm [] t of
1.371 + (trm, trm', vars, _, true) =>
1.372 + let
1.373 + val eq1 =
1.374 + Goal.prove ctxt [] []
1.375 + (list_all (vars, Logic.mk_equals (trm, trm')))
1.376 + (fn _ => rtac meta_ext 1 THEN simp_tac ss1 1);
1.377 + val eq2 = Simplifier.asm_full_rewrite ss2 (Thm.dest_equals_rhs (cprop_of eq1));
1.378 + in SOME (Thm.transitive eq1 eq2) end
1.379 + | _ => NONE)
1.380 + end
1.381 + | _ => NONE));
1.382
1.383 -
1.384 +end;
1.385
1.386
1.387 local
1.388 +
1.389 val swap_ex_eq = @{thm StateFun.swap_ex_eq};
1.390 +
1.391 fun is_selector thy T sel =
1.392 - let
1.393 - val (flds,more) = Record.get_recT_fields thy T
1.394 - in member (fn (s,(n,_)) => n=s) (more::flds) sel
1.395 - end;
1.396 + let val (flds, more) = Record.get_recT_fields thy T
1.397 + in member (fn (s, (n, _)) => n = s) (more :: flds) sel end;
1.398 +
1.399 in
1.400 +
1.401 val ex_lookup_eq_simproc =
1.402 Simplifier.simproc_global @{theory HOL} "ex_lookup_eq_simproc" ["Ex t"]
1.403 (fn thy => fn ss => fn t =>
1.404 - let
1.405 - val ctxt = Simplifier.the_context ss |> Config.put simp_depth_limit 100;
1.406 - val ex_lookup_ss = #2 (StateFunData.get (Context.Proof ctxt));
1.407 - val ss' = (Simplifier.context ctxt ex_lookup_ss);
1.408 - fun prove prop =
1.409 - Goal.prove_global thy [] [] prop
1.410 - (fn _ => Record.split_simp_tac [] (K ~1) 1 THEN
1.411 - simp_tac ss' 1);
1.412 + let
1.413 + val ctxt = Simplifier.the_context ss |> Config.put simp_depth_limit 100;
1.414 + val ex_lookup_ss = #2 (Data.get (Context.Proof ctxt));
1.415 + val ss' = Simplifier.context ctxt ex_lookup_ss;
1.416 + fun prove prop =
1.417 + Goal.prove_global thy [] [] prop
1.418 + (fn _ => Record.split_simp_tac [] (K ~1) 1 THEN simp_tac ss' 1);
1.419
1.420 - fun mkeq (swap,Teq,lT,lo,d,n,x,s) i =
1.421 - let val (_::nT::_) = binder_types lT;
1.422 - (* ('v => 'a) => 'n => ('n => 'v) => 'a *)
1.423 - val x' = if not (Term.is_dependent x)
1.424 - then Bound 1
1.425 - else raise TERM ("",[x]);
1.426 - val n' = if not (Term.is_dependent n)
1.427 - then Bound 2
1.428 - else raise TERM ("",[n]);
1.429 - val sel' = lo $ d $ n' $ s;
1.430 - in (Const (@{const_name HOL.eq},Teq)$sel'$x',hd (binder_types Teq),nT,swap) end;
1.431 + fun mkeq (swap, Teq, lT, lo, d, n, x, s) i =
1.432 + let
1.433 + val (_ :: nT :: _) = binder_types lT;
1.434 + (* ('v => 'a) => 'n => ('n => 'v) => 'a *)
1.435 + val x' = if not (Term.is_dependent x) then Bound 1 else raise TERM ("", [x]);
1.436 + val n' = if not (Term.is_dependent n) then Bound 2 else raise TERM ("", [n]);
1.437 + val sel' = lo $ d $ n' $ s;
1.438 + in (Const (@{const_name HOL.eq}, Teq) $ sel' $ x', hd (binder_types Teq), nT, swap) end;
1.439
1.440 - fun dest_state (s as Bound 0) = s
1.441 - | dest_state (s as (Const (sel,sT)$Bound 0)) =
1.442 - if is_selector thy (domain_type sT) sel
1.443 - then s
1.444 - else raise TERM ("StateFun.ex_lookup_eq_simproc: not a record slector",[s])
1.445 - | dest_state s =
1.446 - raise TERM ("StateFun.ex_lookup_eq_simproc: not a record slector",[s]);
1.447 -
1.448 - fun dest_sel_eq (Const (@{const_name HOL.eq},Teq)$
1.449 - ((lo as (Const ("StateFun.lookup",lT)))$d$n$s)$X) =
1.450 - (false,Teq,lT,lo,d,n,X,dest_state s)
1.451 - | dest_sel_eq (Const (@{const_name HOL.eq},Teq)$X$
1.452 - ((lo as (Const ("StateFun.lookup",lT)))$d$n$s)) =
1.453 - (true,Teq,lT,lo,d,n,X,dest_state s)
1.454 - | dest_sel_eq _ = raise TERM ("",[]);
1.455 + fun dest_state (s as Bound 0) = s
1.456 + | dest_state (s as (Const (sel, sT) $ Bound 0)) =
1.457 + if is_selector thy (domain_type sT) sel then s
1.458 + else raise TERM ("StateFun.ex_lookup_eq_simproc: not a record slector", [s])
1.459 + | dest_state s = raise TERM ("StateFun.ex_lookup_eq_simproc: not a record slector", [s]);
1.460
1.461 - in
1.462 - (case t of
1.463 - (Const (@{const_name Ex},Tex)$Abs(s,T,t)) =>
1.464 - (let val (eq,eT,nT,swap) = mkeq (dest_sel_eq t) 0;
1.465 - val prop = list_all ([("n",nT),("x",eT)],
1.466 - Logic.mk_equals (Const (@{const_name Ex},Tex)$Abs(s,T,eq),
1.467 - HOLogic.true_const));
1.468 - val thm = Drule.export_without_context (prove prop);
1.469 - val thm' = if swap then swap_ex_eq OF [thm] else thm
1.470 - in SOME thm' end
1.471 - handle TERM _ => NONE)
1.472 - | _ => NONE)
1.473 - end handle Option.Option => NONE)
1.474 + fun dest_sel_eq
1.475 + (Const (@{const_name HOL.eq}, Teq) $
1.476 + ((lo as (Const (@{const_name StateFun.lookup}, lT))) $ d $ n $ s) $ X) =
1.477 + (false, Teq, lT, lo, d, n, X, dest_state s)
1.478 + | dest_sel_eq
1.479 + (Const (@{const_name HOL.eq}, Teq) $ X $
1.480 + ((lo as (Const (@{const_name StateFun.lookup}, lT))) $ d $ n $ s)) =
1.481 + (true, Teq, lT, lo, d, n, X, dest_state s)
1.482 + | dest_sel_eq _ = raise TERM ("", []);
1.483 + in
1.484 + (case t of
1.485 + Const (@{const_name Ex}, Tex) $ Abs (s, T, t) =>
1.486 + (let
1.487 + val (eq, eT, nT, swap) = mkeq (dest_sel_eq t) 0;
1.488 + val prop =
1.489 + list_all ([("n", nT), ("x", eT)],
1.490 + Logic.mk_equals (Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), HOLogic.true_const));
1.491 + val thm = Drule.export_without_context (prove prop);
1.492 + val thm' = if swap then swap_ex_eq OF [thm] else thm
1.493 + in SOME thm' end handle TERM _ => NONE)
1.494 + | _ => NONE)
1.495 + end handle Option.Option => NONE);
1.496 +
1.497 end;
1.498
1.499 val val_sfx = "V";
1.500 val val_prfx = "StateFun."
1.501 fun deco base_prfx s = val_prfx ^ (base_prfx ^ suffix val_sfx s);
1.502
1.503 -fun mkUpper str =
1.504 +fun mkUpper str =
1.505 (case String.explode str of
1.506 [] => ""
1.507 - | c::cs => String.implode (Char.toUpper c::cs ))
1.508 + | c::cs => String.implode (Char.toUpper c :: cs));
1.509
1.510 fun mkName (Type (T,args)) = implode (map mkName args) ^ mkUpper (Long_Name.base_name T)
1.511 | mkName (TFree (x,_)) = mkUpper (Long_Name.base_name x)
1.512 @@ -333,50 +336,53 @@
1.513 fun mk_map "List.list" = Syntax.const "List.map"
1.514 | mk_map n = Syntax.const ("StateFun.map_" ^ Long_Name.base_name n);
1.515
1.516 -fun gen_constr_destr comp prfx thy (Type (T,[])) =
1.517 +fun gen_constr_destr comp prfx thy (Type (T, [])) =
1.518 Syntax.const (deco prfx (mkUpper (Long_Name.base_name T)))
1.519 | gen_constr_destr comp prfx thy (T as Type ("fun",_)) =
1.520 - let val (argTs,rangeT) = strip_type T;
1.521 - in comp
1.522 + let val (argTs, rangeT) = strip_type T;
1.523 + in
1.524 + comp
1.525 (Syntax.const (deco prfx (implode (map mkName argTs) ^ "Fun")))
1.526 - (fold (fn x => fn y => x$y)
1.527 - (replicate (length argTs) (Syntax.const "StateFun.map_fun"))
1.528 - (gen_constr_destr comp prfx thy rangeT))
1.529 - end
1.530 - | gen_constr_destr comp prfx thy (T' as Type (T,argTs)) =
1.531 - if is_datatype thy T
1.532 - then (* datatype args are recursively embedded into val *)
1.533 - (case argTs of
1.534 - [argT] => comp
1.535 - ((Syntax.const (deco prfx (mkUpper (Long_Name.base_name T)))))
1.536 - ((mk_map T $ gen_constr_destr comp prfx thy argT))
1.537 - | _ => raise (TYPE ("StateFun.gen_constr_destr",[T'],[])))
1.538 - else (* type args are not recursively embedded into val *)
1.539 - Syntax.const (deco prfx (implode (map mkName argTs) ^ mkUpper (Long_Name.base_name T)))
1.540 - | gen_constr_destr thy _ _ T = raise (TYPE ("StateFun.gen_constr_destr",[T],[]));
1.541 -
1.542 -val mk_constr = gen_constr_destr (fn a => fn b => Syntax.const "Fun.comp" $ a $ b) ""
1.543 -val mk_destr = gen_constr_destr (fn a => fn b => Syntax.const "Fun.comp" $ b $ a) "the_"
1.544 + (fold (fn x => fn y => x $ y)
1.545 + (replicate (length argTs) (Syntax.const "StateFun.map_fun"))
1.546 + (gen_constr_destr comp prfx thy rangeT))
1.547 + end
1.548 + | gen_constr_destr comp prfx thy (T' as Type (T, argTs)) =
1.549 + if is_datatype thy T
1.550 + then (* datatype args are recursively embedded into val *)
1.551 + (case argTs of
1.552 + [argT] =>
1.553 + comp
1.554 + ((Syntax.const (deco prfx (mkUpper (Long_Name.base_name T)))))
1.555 + ((mk_map T $ gen_constr_destr comp prfx thy argT))
1.556 + | _ => raise (TYPE ("StateFun.gen_constr_destr", [T'], [])))
1.557 + else (* type args are not recursively embedded into val *)
1.558 + Syntax.const (deco prfx (implode (map mkName argTs) ^ mkUpper (Long_Name.base_name T)))
1.559 + | gen_constr_destr thy _ _ T = raise (TYPE ("StateFun.gen_constr_destr", [T], []));
1.560
1.561 -
1.562 +val mk_constr = gen_constr_destr (fn a => fn b => Syntax.const @{const_name Fun.comp} $ a $ b) "";
1.563 +val mk_destr = gen_constr_destr (fn a => fn b => Syntax.const @{const_name Fun.comp} $ b $ a) "the_";
1.564 +
1.565 +
1.566 val statefun_simp_attr = Thm.declaration_attribute (fn thm => fn ctxt =>
1.567 let
1.568 - val (lookup_ss,ex_lookup_ss,simprocs_active) = StateFunData.get ctxt;
1.569 - val (lookup_ss', ex_lookup_ss') =
1.570 - (case (concl_of thm) of
1.571 - (_$((Const (@{const_name Ex},_)$_))) => (lookup_ss, ex_lookup_ss addsimps [thm])
1.572 - | _ => (lookup_ss addsimps [thm], ex_lookup_ss))
1.573 - fun activate_simprocs ctxt =
1.574 - if simprocs_active then ctxt
1.575 - else Simplifier.map_ss (fn ss => ss addsimprocs [lookup_simproc,update_simproc]) ctxt
1.576 + val (lookup_ss, ex_lookup_ss, simprocs_active) = Data.get ctxt;
1.577 + val (lookup_ss', ex_lookup_ss') =
1.578 + (case concl_of thm of
1.579 + (_ $ ((Const (@{const_name Ex}, _) $ _))) => (lookup_ss, ex_lookup_ss addsimps [thm])
1.580 + | _ => (lookup_ss addsimps [thm], ex_lookup_ss));
1.581 + fun activate_simprocs ctxt =
1.582 + if simprocs_active then ctxt
1.583 + else Simplifier.map_ss (fn ss => ss addsimprocs [lookup_simproc, update_simproc]) ctxt;
1.584 in
1.585 - ctxt
1.586 + ctxt
1.587 |> activate_simprocs
1.588 - |> (StateFunData.put (lookup_ss',ex_lookup_ss',true))
1.589 + |> Data.put (lookup_ss', ex_lookup_ss', true)
1.590 end);
1.591
1.592 -val setup =
1.593 +val setup =
1.594 init_state_fun_data #>
1.595 Attrib.setup @{binding statefun_simp} (Scan.succeed statefun_simp_attr)
1.596 - "simplification in statespaces"
1.597 -end
1.598 + "simplification in statespaces";
1.599 +
1.600 +end;