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