# HG changeset patch
# User wenzelm
# Date 1320601335 -3600
# Node ID 208634369af2df99135a80a26111efbb64f15e50
# Parent  dc605ed5a40dcf259fee070086bfe9f14894fd7b
misc tuning and modernization;
more antiquotations;

diff -r dc605ed5a40d -r 208634369af2 src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Sun Nov 06 17:53:32 2011 +0100
+++ b/src/HOL/Statespace/state_fun.ML	Sun Nov 06 18:42:15 2011 +0100
@@ -20,22 +20,23 @@
   val setup : theory -> theory
 end;
 
-structure StateFun: STATE_FUN = 
+structure StateFun: STATE_FUN =
 struct
 
-val lookupN = "StateFun.lookup";
-val updateN = "StateFun.update";
+val lookupN = @{const_name StateFun.lookup};
+val updateN = @{const_name StateFun.update};
 
 val sel_name = HOLogic.dest_string;
 
 fun mk_name i t =
   (case try sel_name t of
-     SOME name => name
-   | NONE => (case t of 
-               Free (x,_) => x
-              |Const (x,_) => x
-              |_ => "x"^string_of_int i))
-               
+    SOME name => name
+  | NONE =>
+      (case t of
+        Free (x, _) => x
+      | Const (x, _) => x
+      | _ => "x" ^ string_of_int i));
+
 local
 
 val conj1_False = @{thm conj1_False};
@@ -43,9 +44,10 @@
 val conj_True = @{thm conj_True};
 val conj_cong = @{thm conj_cong};
 
-fun isFalse (Const (@{const_name False},_)) = true
+fun isFalse (Const (@{const_name False}, _)) = true
   | isFalse _ = false;
-fun isTrue (Const (@{const_name True},_)) = true
+
+fun isTrue (Const (@{const_name True}, _)) = true
   | isTrue _ = false;
 
 in
@@ -53,36 +55,34 @@
 val lazy_conj_simproc =
   Simplifier.simproc_global @{theory HOL} "lazy_conj_simp" ["P & Q"]
     (fn thy => fn ss => fn t =>
-      (case t of (Const (@{const_name HOL.conj},_)$P$Q) => 
-         let
-            val P_P' = Simplifier.rewrite ss (cterm_of thy P);
-            val P' = P_P' |> prop_of |> Logic.dest_equals |> #2 
-         in if isFalse P'
-            then SOME (conj1_False OF [P_P'])
-            else 
-              let
-                val Q_Q' = Simplifier.rewrite ss (cterm_of thy Q);
-                val Q' = Q_Q' |> prop_of |> Logic.dest_equals |> #2 
-              in if isFalse Q'
-                 then SOME (conj2_False OF [Q_Q'])
-                 else if isTrue P' andalso isTrue Q'
-                      then SOME (conj_True OF [P_P', Q_Q'])
-                      else if P aconv P' andalso Q aconv Q' then NONE
-                           else SOME (conj_cong OF [P_P', Q_Q'])
-              end 
+      (case t of (Const (@{const_name HOL.conj},_) $ P $ Q) =>
+        let
+          val P_P' = Simplifier.rewrite ss (cterm_of thy P);
+          val P' = P_P' |> prop_of |> Logic.dest_equals |> #2;
+        in
+          if isFalse P' then SOME (conj1_False OF [P_P'])
+          else
+            let
+              val Q_Q' = Simplifier.rewrite ss (cterm_of thy Q);
+              val Q' = Q_Q' |> prop_of |> Logic.dest_equals |> #2;
+            in
+              if isFalse Q' then SOME (conj2_False OF [Q_Q'])
+              else if isTrue P' andalso isTrue Q' then SOME (conj_True OF [P_P', Q_Q'])
+              else if P aconv P' andalso Q aconv Q' then NONE
+              else SOME (conj_cong OF [P_P', Q_Q'])
+            end
          end
-        
       | _ => NONE));
 
-val string_eq_simp_tac = simp_tac (HOL_basic_ss 
+val string_eq_simp_tac = simp_tac (HOL_basic_ss
   addsimps (@{thms list.inject} @ @{thms char.inject}
     @ @{thms list.distinct} @ @{thms char.distinct} @ @{thms simp_thms})
   addsimprocs [lazy_conj_simproc]
-  addcongs [@{thm block_conj_cong}])
+  addcongs [@{thm block_conj_cong}]);
 
 end;
 
-val lookup_ss = (HOL_basic_ss 
+val lookup_ss = (HOL_basic_ss
   addsimps (@{thms list.inject} @ @{thms char.inject}
     @ @{thms list.distinct} @ @{thms char.distinct} @ @{thms simp_thms}
     @ [@{thm StateFun.lookup_update_id_same}, @{thm StateFun.id_id_cancel},
@@ -94,235 +94,238 @@
 val ex_lookup_ss = HOL_ss addsimps @{thms StateFun.ex_id};
 
 
-structure StateFunData = Generic_Data
+structure Data = Generic_Data
 (
-  type T = simpset * simpset * bool;
-           (* lookup simpset, ex_lookup simpset, are simprocs installed *)
+  type T = simpset * simpset * bool;  (*lookup simpset, ex_lookup simpset, are simprocs installed*)
   val empty = (empty_ss, empty_ss, false);
   val extend = I;
   fun merge ((ss1, ex_ss1, b1), (ss2, ex_ss2, b2)) =
-    (merge_ss (ss1, ss2), merge_ss (ex_ss1, ex_ss2), b1 orelse b2 (* FIXME odd merge *));
+    (merge_ss (ss1, ss2), merge_ss (ex_ss1, ex_ss2), b1 orelse b2);
 );
 
 val init_state_fun_data =
-  Context.theory_map (StateFunData.put (lookup_ss,ex_lookup_ss,false));
+  Context.theory_map (Data.put (lookup_ss, ex_lookup_ss, false));
 
 val lookup_simproc =
   Simplifier.simproc_global @{theory} "lookup_simp" ["lookup d n (update d' c m v s)"]
     (fn thy => fn ss => fn t =>
-      (case t of (Const ("StateFun.lookup",lT)$destr$n$
-                   (s as Const ("StateFun.update",uT)$_$_$_$_$_)) =>
+      (case t of (Const (@{const_name StateFun.lookup}, lT) $ destr $ n $
+                   (s as Const (@{const_name StateFun.update}, uT) $ _ $ _ $ _ $ _ $ _)) =>
         (let
           val (_::_::_::_::sT::_) = binder_types uT;
           val mi = maxidx_of_term t;
-          fun mk_upds (Const ("StateFun.update",uT)$d'$c$m$v$s) =
-               let
-                 val (_::_::_::fT::_::_) = binder_types uT;
-                 val vT = domain_type fT;
-                 val (s',cnt) = mk_upds s;
-                 val (v',cnt') = 
-                      (case v of
-                        Const ("StateFun.K_statefun",KT)$v''
-                         => (case v'' of 
-                             (Const ("StateFun.lookup",_)$(d as (Const ("Fun.id",_)))$n'$_)
-                              => if d aconv c andalso n aconv m andalso m aconv n' 
-                                 then (v,cnt) (* Keep value so that 
-                                                 lookup_update_id_same can fire *)
-                                 else (Const ("StateFun.K_statefun",KT)$Var (("v",cnt),vT),
-                                       cnt+1)
-                              | _ => (Const ("StateFun.K_statefun",KT)$Var (("v",cnt),vT),
-                                       cnt+1))
-                       | _ => (v,cnt));
-               in (Const ("StateFun.update",uT)$d'$c$m$v'$s',cnt')
-               end
-            | mk_upds s = (Var (("s",mi+1),sT),mi+2);
-          
-          val ct = cterm_of thy 
-                    (Const ("StateFun.lookup",lT)$destr$n$(fst (mk_upds s)));
+          fun mk_upds (Const (@{const_name StateFun.update}, uT) $ d' $ c $ m $ v $ s) =
+                let
+                  val (_ :: _ :: _ :: fT :: _ :: _) = binder_types uT;
+                  val vT = domain_type fT;
+                  val (s', cnt) = mk_upds s;
+                  val (v', cnt') =
+                    (case v of
+                      Const (@{const_name K_statefun}, KT) $ v'' =>
+                        (case v'' of
+                          (Const (@{const_name StateFun.lookup}, _) $
+                            (d as (Const (@{const_name Fun.id}, _))) $ n' $ _) =>
+                              if d aconv c andalso n aconv m andalso m aconv n'
+                              then (v,cnt) (* Keep value so that
+                                              lookup_update_id_same can fire *)
+                              else
+                                (Const (@{const_name StateFun.K_statefun}, KT) $
+                                  Var (("v", cnt), vT), cnt + 1)
+                        | _ =>
+                          (Const (@{const_name StateFun.K_statefun}, KT) $
+                            Var (("v", cnt), vT), cnt + 1))
+                     | _ => (v, cnt));
+                in (Const (@{const_name StateFun.update}, uT) $ d' $ c $ m $ v' $ s', cnt') end
+            | mk_upds s = (Var (("s", mi + 1), sT), mi + 2);
+
+          val ct =
+            cterm_of thy (Const (@{const_name StateFun.lookup}, lT) $ destr $ n $ fst (mk_upds s));
           val ctxt = Simplifier.the_context ss;
-          val basic_ss = #1 (StateFunData.get (Context.Proof ctxt));
+          val basic_ss = #1 (Data.get (Context.Proof ctxt));
           val ss' = Simplifier.context (Config.put simp_depth_limit 100 ctxt) basic_ss;
           val thm = Simplifier.rewrite ss' ct;
-        in if (op aconv) (Logic.dest_equals (prop_of thm))
-           then NONE
-           else SOME thm
+        in
+          if (op aconv) (Logic.dest_equals (prop_of thm))
+          then NONE
+          else SOME thm
         end
         handle Option.Option => NONE)
-         
       | _ => NONE ));
 
 
 local
+
 val meta_ext = @{thm StateFun.meta_ext};
 val ss' = (HOL_ss addsimps
   (@{thm StateFun.update_apply} :: @{thm Fun.o_apply} :: @{thms list.inject} @ @{thms char.inject}
     @ @{thms list.distinct} @ @{thms char.distinct})
   addsimprocs [lazy_conj_simproc, StateSpace.distinct_simproc]
   addcongs @{thms block_conj_cong});
+
 in
+
 val update_simproc =
   Simplifier.simproc_global @{theory} "update_simp" ["update d c n v s"]
     (fn thy => fn ss => fn t =>
-      (case t of ((upd as Const ("StateFun.update", uT)) $ d $ c $ n $ v $ s) =>
-         let 
-            
-             val (_::_::_::_::sT::_) = binder_types uT;
-                (*"('v => 'a1) => ('a2 => 'v) => 'n => ('a1 => 'a2) => ('n => 'v) => ('n => 'v)"*)
-             fun init_seed s = (Bound 0,Bound 0, [("s",sT)],[], false);
+      (case t of
+        ((upd as Const ("StateFun.update", uT)) $ d $ c $ n $ v $ s) =>
+          let
+            val (_ :: _ :: _ :: _ :: sT :: _) = binder_types uT;
+              (*"('v => 'a1) => ('a2 => 'v) => 'n => ('a1 => 'a2) => ('n => 'v) => ('n => 'v)"*)
+            fun init_seed s = (Bound 0, Bound 0, [("s", sT)], [], false);
 
-             fun mk_comp f fT g gT =
-               let val T = (domain_type fT --> range_type gT) 
-               in (Const ("Fun.comp",gT --> fT --> T)$g$f,T) end
+            fun mk_comp f fT g gT =
+              let val T = domain_type fT --> range_type gT
+              in (Const (@{const_name Fun.comp}, gT --> fT --> T) $ g $ f, T) end;
 
-             fun mk_comps fs = 
-                   foldl1 (fn ((f,fT),(g,gT)) => mk_comp g gT f fT) fs;
+            fun mk_comps fs = foldl1 (fn ((f, fT), (g, gT)) => mk_comp g gT f fT) fs;
+
+            fun append n c cT f fT d dT comps =
+              (case AList.lookup (op aconv) comps n of
+                SOME gTs => AList.update (op aconv) (n, [(c, cT), (f, fT), (d, dT)] @ gTs) comps
+              | NONE => AList.update (op aconv) (n, [(c, cT), (f, fT), (d, dT)]) comps);
 
-             fun append n c cT f fT d dT comps =
-               (case AList.lookup (op aconv) comps n of
-                  SOME gTs => AList.update (op aconv) 
-                                    (n,[(c,cT),(f,fT),(d,dT)]@gTs) comps
-                | NONE => AList.update (op aconv) (n,[(c,cT),(f,fT),(d,dT)]) comps)
+            fun split_list (x :: xs) = let val (xs', y) = split_last xs in (x, xs', y) end
+              | split_list _ = error "StateFun.split_list";
 
-             fun split_list (x::xs) = let val (xs',y) = split_last xs in (x,xs',y) end
-               | split_list _ = error "StateFun.split_list";
-
-             fun merge_upds n comps =
-               let val ((c,cT),fs,(d,dT)) = split_list (the (AList.lookup (op aconv) comps n))
-               in ((c,cT),fst (mk_comps fs),(d,dT)) end;
+            fun merge_upds n comps =
+              let val ((c, cT), fs, (d, dT)) = split_list (the (AList.lookup (op aconv) comps n))
+              in ((c, cT), fst (mk_comps fs), (d, dT)) end;
 
-             (* mk_updterm returns 
-              *  - (orig-term-skeleton,simplified-term-skeleton, vars, b)
-              *     where boolean b tells if a simplification has occurred.
-                    "orig-term-skeleton = simplified-term-skeleton" is
-              *     the desired simplification rule.
-              * The algorithm first walks down the updates to the seed-state while
-              * memorising the updates in the already-table. While walking up the
-              * updates again, the optimised term is constructed.
-              *)
-             fun mk_updterm already
-                 (t as ((upd as Const ("StateFun.update", uT)) $ d $ c $ n $ v $ s)) =
-                      let
-                         fun rest already = mk_updterm already;
-                         val (dT::cT::nT::vT::sT::_) = binder_types uT;
-                          (*"('v => 'a1) => ('a2 => 'v) => 'n => ('a1 => 'a2) => 
-                                ('n => 'v) => ('n => 'v)"*)
-                      in if member (op aconv) already n
-                         then (case rest already s of
-                                 (trm,trm',vars,comps,_) =>
-                                   let
-                                     val i = length vars;
-                                     val kv = (mk_name i n,vT);
-                                     val kb = Bound i;
-                                     val comps' = append n c cT kb vT d dT comps;
-                                   in (upd$d$c$n$kb$trm, trm', kv::vars,comps',true) end)
-                         else
-                          (case rest (n::already) s of
-                             (trm,trm',vars,comps,b) =>
-                                let
-                                   val i = length vars;
-                                   val kv = (mk_name i n,vT);
-                                   val kb = Bound i;
-                                   val comps' = append n c cT kb vT d dT comps;
-                                   val ((c',c'T),f',(d',d'T)) = merge_upds n comps';
-                                   val vT' = range_type d'T --> domain_type c'T;
-                                   val upd' = Const ("StateFun.update",d'T --> c'T --> nT --> vT' --> sT --> sT);
-                                in (upd$d$c$n$kb$trm, upd'$d'$c'$n$f'$trm', kv::vars,comps',b) 
-                                end)
-                      end
-               | mk_updterm _ t = init_seed t;
+               (* mk_updterm returns
+                *  - (orig-term-skeleton,simplified-term-skeleton, vars, b)
+                *     where boolean b tells if a simplification has occurred.
+                      "orig-term-skeleton = simplified-term-skeleton" is
+                *     the desired simplification rule.
+                * The algorithm first walks down the updates to the seed-state while
+                * memorising the updates in the already-table. While walking up the
+                * updates again, the optimised term is constructed.
+                *)
+            fun mk_updterm already
+                (t as ((upd as Const ("StateFun.update", uT)) $ d $ c $ n $ v $ s)) =
+                  let
+                    fun rest already = mk_updterm already;
+                    val (dT :: cT :: nT :: vT :: sT :: _) = binder_types uT;
+                      (*"('v => 'a1) => ('a2 => 'v) => 'n => ('a1 => 'a2) =>
+                            ('n => 'v) => ('n => 'v)"*)
+                  in
+                    if member (op aconv) already n then
+                      (case rest already s of
+                        (trm, trm', vars, comps, _) =>
+                          let
+                            val i = length vars;
+                            val kv = (mk_name i n, vT);
+                            val kb = Bound i;
+                            val comps' = append n c cT kb vT d dT comps;
+                          in (upd $ d $ c $ n $ kb $ trm, trm', kv :: vars, comps',true) end)
+                    else
+                      (case rest (n :: already) s of
+                        (trm, trm', vars, comps, b) =>
+                          let
+                            val i = length vars;
+                            val kv = (mk_name i n, vT);
+                            val kb = Bound i;
+                            val comps' = append n c cT kb vT d dT comps;
+                            val ((c', c'T), f', (d', d'T)) = merge_upds n comps';
+                            val vT' = range_type d'T --> domain_type c'T;
+                            val upd' =
+                              Const (@{const_name StateFun.update},
+                                d'T --> c'T --> nT --> vT' --> sT --> sT);
+                          in
+                            (upd $ d $ c $ n $ kb $ trm, upd' $ d' $ c' $ n $ f' $ trm', kv :: vars, comps', b)
+                          end)
+                  end
+              | mk_updterm _ t = init_seed t;
 
-             val ctxt = Simplifier.the_context ss |> Config.put simp_depth_limit 100;
-             val ss1 = Simplifier.context ctxt ss';
-             val ss2 = Simplifier.context ctxt 
-                         (#1 (StateFunData.get (Context.Proof ctxt)));
-         in (case mk_updterm [] t of
-               (trm,trm',vars,_,true)
-                => let
-                     val eq1 = Goal.prove ctxt [] [] 
-                                      (list_all (vars, Logic.mk_equals (trm, trm')))
-                                      (fn _ => rtac meta_ext 1 THEN 
-                                               simp_tac ss1 1);
-                     val eq2 = Simplifier.asm_full_rewrite ss2 (Thm.dest_equals_rhs (cprop_of eq1));
-                   in SOME (Thm.transitive eq1 eq2) end
-             | _ => NONE)
-         end
-       | _ => NONE));
-end
+            val ctxt = Simplifier.the_context ss |> Config.put simp_depth_limit 100;
+            val ss1 = Simplifier.context ctxt ss';
+            val ss2 = Simplifier.context ctxt (#1 (Data.get (Context.Proof ctxt)));
+          in
+            (case mk_updterm [] t of
+              (trm, trm', vars, _, true) =>
+                let
+                  val eq1 =
+                    Goal.prove ctxt [] []
+                      (list_all (vars, Logic.mk_equals (trm, trm')))
+                      (fn _ => rtac meta_ext 1 THEN simp_tac ss1 1);
+                  val eq2 = Simplifier.asm_full_rewrite ss2 (Thm.dest_equals_rhs (cprop_of eq1));
+                in SOME (Thm.transitive eq1 eq2) end
+            | _ => NONE)
+          end
+      | _ => NONE));
 
-
+end;
 
 
 local
+
 val swap_ex_eq = @{thm StateFun.swap_ex_eq};
+
 fun is_selector thy T sel =
-     let 
-       val (flds,more) = Record.get_recT_fields thy T 
-     in member (fn (s,(n,_)) => n=s) (more::flds) sel
-     end;
+  let val (flds, more) = Record.get_recT_fields thy T
+  in member (fn (s, (n, _)) => n = s) (more :: flds) sel end;
+
 in
+
 val ex_lookup_eq_simproc =
   Simplifier.simproc_global @{theory HOL} "ex_lookup_eq_simproc" ["Ex t"]
     (fn thy => fn ss => fn t =>
-       let
-         val ctxt = Simplifier.the_context ss |> Config.put simp_depth_limit 100;
-         val ex_lookup_ss = #2 (StateFunData.get (Context.Proof ctxt));
-         val ss' = (Simplifier.context ctxt ex_lookup_ss);
-         fun prove prop =
-           Goal.prove_global thy [] [] prop 
-             (fn _ => Record.split_simp_tac [] (K ~1) 1 THEN
-                      simp_tac ss' 1);
+      let
+        val ctxt = Simplifier.the_context ss |> Config.put simp_depth_limit 100;
+        val ex_lookup_ss = #2 (Data.get (Context.Proof ctxt));
+        val ss' = Simplifier.context ctxt ex_lookup_ss;
+        fun prove prop =
+          Goal.prove_global thy [] [] prop
+            (fn _ => Record.split_simp_tac [] (K ~1) 1 THEN simp_tac ss' 1);
 
-         fun mkeq (swap,Teq,lT,lo,d,n,x,s) i =
-               let val (_::nT::_) = binder_types lT;
-                         (*  ('v => 'a) => 'n => ('n => 'v) => 'a *)
-                   val x' = if not (Term.is_dependent x)
-                            then Bound 1
-                            else raise TERM ("",[x]);
-                   val n' = if not (Term.is_dependent n)
-                            then Bound 2
-                            else raise TERM ("",[n]);
-                   val sel' = lo $ d $ n' $ s;
-                  in (Const (@{const_name HOL.eq},Teq)$sel'$x',hd (binder_types Teq),nT,swap) end;
+        fun mkeq (swap, Teq, lT, lo, d, n, x, s) i =
+          let
+            val (_ :: nT :: _) = binder_types lT;
+            (*  ('v => 'a) => 'n => ('n => 'v) => 'a *)
+            val x' = if not (Term.is_dependent x) then Bound 1 else raise TERM ("", [x]);
+            val n' = if not (Term.is_dependent n) then Bound 2 else raise TERM ("", [n]);
+            val sel' = lo $ d $ n' $ s;
+          in (Const (@{const_name HOL.eq}, Teq) $ sel' $ x', hd (binder_types Teq), nT, swap) end;
+
+        fun dest_state (s as Bound 0) = s
+          | dest_state (s as (Const (sel, sT) $ Bound 0)) =
+              if is_selector thy (domain_type sT) sel then s
+              else raise TERM ("StateFun.ex_lookup_eq_simproc: not a record slector", [s])
+          | dest_state s = raise TERM ("StateFun.ex_lookup_eq_simproc: not a record slector", [s]);
 
-         fun dest_state (s as Bound 0) = s
-           | dest_state (s as (Const (sel,sT)$Bound 0)) =
-               if is_selector thy (domain_type sT) sel
-               then s
-               else raise TERM ("StateFun.ex_lookup_eq_simproc: not a record slector",[s])
-           | dest_state s = 
-                    raise TERM ("StateFun.ex_lookup_eq_simproc: not a record slector",[s]);
-  
-         fun dest_sel_eq (Const (@{const_name HOL.eq},Teq)$
-                           ((lo as (Const ("StateFun.lookup",lT)))$d$n$s)$X) =
-                           (false,Teq,lT,lo,d,n,X,dest_state s)
-           | dest_sel_eq (Const (@{const_name HOL.eq},Teq)$X$
-                            ((lo as (Const ("StateFun.lookup",lT)))$d$n$s)) =
-                           (true,Teq,lT,lo,d,n,X,dest_state s)
-           | dest_sel_eq _ = raise TERM ("",[]);
+        fun dest_sel_eq
+              (Const (@{const_name HOL.eq}, Teq) $
+                ((lo as (Const (@{const_name StateFun.lookup}, lT))) $ d $ n $ s) $ X) =
+              (false, Teq, lT, lo, d, n, X, dest_state s)
+          | dest_sel_eq
+              (Const (@{const_name HOL.eq}, Teq) $ X $
+                ((lo as (Const (@{const_name StateFun.lookup}, lT))) $ d $ n $ s)) =
+              (true, Teq, lT, lo, d, n, X, dest_state s)
+          | dest_sel_eq _ = raise TERM ("", []);
+      in
+        (case t of
+          Const (@{const_name Ex}, Tex) $ Abs (s, T, t) =>
+            (let
+              val (eq, eT, nT, swap) = mkeq (dest_sel_eq t) 0;
+              val prop =
+                list_all ([("n", nT), ("x", eT)],
+                  Logic.mk_equals (Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), HOLogic.true_const));
+              val thm = Drule.export_without_context (prove prop);
+              val thm' = if swap then swap_ex_eq OF [thm] else thm
+            in SOME thm' end handle TERM _ => NONE)
+        | _ => NONE)
+      end handle Option.Option => NONE);
 
-       in
-         (case t of
-           (Const (@{const_name Ex},Tex)$Abs(s,T,t)) =>
-             (let val (eq,eT,nT,swap) = mkeq (dest_sel_eq t) 0;
-                  val prop = list_all ([("n",nT),("x",eT)],
-                              Logic.mk_equals (Const (@{const_name Ex},Tex)$Abs(s,T,eq),
-                                               HOLogic.true_const));
-                  val thm = Drule.export_without_context (prove prop);
-                  val thm' = if swap then swap_ex_eq OF [thm] else thm
-             in SOME thm' end
-             handle TERM _ => NONE)
-          | _ => NONE)
-        end handle Option.Option => NONE) 
 end;
 
 val val_sfx = "V";
 val val_prfx = "StateFun."
 fun deco base_prfx s = val_prfx ^ (base_prfx ^ suffix val_sfx s);
 
-fun mkUpper str = 
+fun mkUpper str =
   (case String.explode str of
     [] => ""
-   | c::cs => String.implode (Char.toUpper c::cs ))
+  | c::cs => String.implode (Char.toUpper c :: cs));
 
 fun mkName (Type (T,args)) = implode (map mkName args) ^ mkUpper (Long_Name.base_name T)
   | mkName (TFree (x,_)) = mkUpper (Long_Name.base_name x)
@@ -333,50 +336,53 @@
 fun mk_map "List.list" = Syntax.const "List.map"
   | mk_map n = Syntax.const ("StateFun.map_" ^ Long_Name.base_name n);
 
-fun gen_constr_destr comp prfx thy (Type (T,[])) = 
+fun gen_constr_destr comp prfx thy (Type (T, [])) =
       Syntax.const (deco prfx (mkUpper (Long_Name.base_name T)))
   | gen_constr_destr comp prfx thy (T as Type ("fun",_)) =
-     let val (argTs,rangeT) = strip_type T;
-     in comp 
+      let val (argTs, rangeT) = strip_type T;
+      in
+        comp
           (Syntax.const (deco prfx (implode (map mkName argTs) ^ "Fun")))
-          (fold (fn x => fn y => x$y)
-               (replicate (length argTs) (Syntax.const "StateFun.map_fun"))
-               (gen_constr_destr comp prfx thy rangeT))
-     end
-  | gen_constr_destr comp prfx thy (T' as Type (T,argTs)) = 
-     if is_datatype thy T
-     then (* datatype args are recursively embedded into val *)
-         (case argTs of
-           [argT] => comp 
-                     ((Syntax.const (deco prfx (mkUpper (Long_Name.base_name T)))))
-                     ((mk_map T $ gen_constr_destr comp prfx thy argT))
-          | _ => raise (TYPE ("StateFun.gen_constr_destr",[T'],[])))
-     else (* type args are not recursively embedded into val *)
-           Syntax.const (deco prfx (implode (map mkName argTs) ^ mkUpper (Long_Name.base_name T)))
-  | gen_constr_destr thy _ _ T = raise (TYPE ("StateFun.gen_constr_destr",[T],[]));
-                   
-val mk_constr = gen_constr_destr (fn a => fn b => Syntax.const "Fun.comp" $ a $ b) ""
-val mk_destr =  gen_constr_destr (fn a => fn b => Syntax.const "Fun.comp" $ b $ a) "the_"
+          (fold (fn x => fn y => x $ y)
+            (replicate (length argTs) (Syntax.const "StateFun.map_fun"))
+            (gen_constr_destr comp prfx thy rangeT))
+      end
+  | gen_constr_destr comp prfx thy (T' as Type (T, argTs)) =
+      if is_datatype thy T
+      then (* datatype args are recursively embedded into val *)
+        (case argTs of
+          [argT] =>
+            comp
+              ((Syntax.const (deco prfx (mkUpper (Long_Name.base_name T)))))
+              ((mk_map T $ gen_constr_destr comp prfx thy argT))
+        | _ => raise (TYPE ("StateFun.gen_constr_destr", [T'], [])))
+      else (* type args are not recursively embedded into val *)
+        Syntax.const (deco prfx (implode (map mkName argTs) ^ mkUpper (Long_Name.base_name T)))
+  | gen_constr_destr thy _ _ T = raise (TYPE ("StateFun.gen_constr_destr", [T], []));
 
-  
+val mk_constr = gen_constr_destr (fn a => fn b => Syntax.const @{const_name Fun.comp} $ a $ b) "";
+val mk_destr = gen_constr_destr (fn a => fn b => Syntax.const @{const_name Fun.comp} $ b $ a) "the_";
+
+
 val statefun_simp_attr = Thm.declaration_attribute (fn thm => fn ctxt =>
   let
-     val (lookup_ss,ex_lookup_ss,simprocs_active) = StateFunData.get ctxt;
-     val (lookup_ss', ex_lookup_ss') = 
-           (case (concl_of thm) of
-            (_$((Const (@{const_name Ex},_)$_))) => (lookup_ss, ex_lookup_ss addsimps [thm])
-            | _ => (lookup_ss addsimps [thm], ex_lookup_ss))
-     fun activate_simprocs ctxt =
-          if simprocs_active then ctxt
-          else Simplifier.map_ss (fn ss => ss addsimprocs [lookup_simproc,update_simproc]) ctxt
+    val (lookup_ss, ex_lookup_ss, simprocs_active) = Data.get ctxt;
+    val (lookup_ss', ex_lookup_ss') =
+      (case concl_of thm of
+        (_ $ ((Const (@{const_name Ex}, _) $ _))) => (lookup_ss, ex_lookup_ss addsimps [thm])
+      | _ => (lookup_ss addsimps [thm], ex_lookup_ss));
+    fun activate_simprocs ctxt =
+      if simprocs_active then ctxt
+      else Simplifier.map_ss (fn ss => ss addsimprocs [lookup_simproc, update_simproc]) ctxt;
   in
-    ctxt 
+    ctxt
     |> activate_simprocs
-    |> (StateFunData.put (lookup_ss',ex_lookup_ss',true))
+    |> Data.put (lookup_ss', ex_lookup_ss', true)
   end);
 
-val setup = 
+val setup =
   init_state_fun_data #>
   Attrib.setup @{binding statefun_simp} (Scan.succeed statefun_simp_attr)
-    "simplification in statespaces"
-end
+    "simplification in statespaces";
+
+end;