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