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