src/HOL/Statespace/state_fun.ML
changeset 25408 156f6f7082b8
parent 25171 4a9c25bffc9b
child 26496 49ae9456eba9
equal deleted inserted replaced
25407:2859cf34aaf0 25408:156f6f7082b8
     1 (*  Title:      state_fun.ML
     1 (*  Title:      state_fun.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Norbert Schirmer, TU Muenchen
     3     Author:     Norbert Schirmer, TU Muenchen
     4 *)
     4 *)
     5 
     5 
     6 
     6 signature STATE_FUN =
     7 structure StateFun =
     7 sig
       
     8   val lookupN : string
       
     9   val updateN : string
       
    10 
       
    11   val mk_constr : Context.theory -> Term.typ -> Term.term
       
    12   val mk_destr : Context.theory -> Term.typ -> Term.term
       
    13 
       
    14   val lookup_simproc : MetaSimplifier.simproc
       
    15   val update_simproc : MetaSimplifier.simproc
       
    16   val ex_lookup_eq_simproc : MetaSimplifier.simproc
       
    17   val ex_lookup_ss : MetaSimplifier.simpset
       
    18   val lazy_conj_simproc : MetaSimplifier.simproc
       
    19   val string_eq_simp_tac : int -> Tactical.tactic
       
    20 
       
    21   val setup : Context.theory -> Context.theory
       
    22 end;
       
    23 
       
    24 structure StateFun: STATE_FUN = 
     8 struct
    25 struct
     9 
    26 
    10 val lookupN = "StateFun.lookup";
    27 val lookupN = "StateFun.lookup";
    11 val updateN = "StateFun.update";
    28 val updateN = "StateFun.update";
    12 
    29 
    13 
    30 val sel_name = HOLogic.dest_string;
    14 fun dest_nib c =
       
    15      let val h = List.last (String.explode c) 
       
    16      in if #"0" <= h andalso h <= #"9" then Char.ord h - Char.ord #"0"
       
    17         else if #"A" <= h andalso h <= #"F" then Char.ord h - Char.ord #"A" + 10
       
    18         else raise Match
       
    19      end;
       
    20 
       
    21 fun dest_chr (Const ("List.char.Char",_)$Const (c1,_)$(Const (c2,_))) = 
       
    22     let val c = Char.chr (dest_nib c1 * 16 + dest_nib c2)
       
    23     in if Char.isPrint c then c else raise Match end
       
    24   | dest_chr _ = raise Match;
       
    25 
       
    26 fun dest_string (Const ("List.list.Nil",_)) = []
       
    27   | dest_string (Const ("List.list.Cons",_)$c$cs) = dest_chr c::dest_string cs
       
    28   | dest_string _ = raise TERM ("dest_string",[]);
       
    29 
       
    30 fun sel_name n = String.implode (dest_string n);
       
    31 
    31 
    32 fun mk_name i t =
    32 fun mk_name i t =
    33   (case try sel_name t of
    33   (case try sel_name t of
    34      SOME name => name
    34      SOME name => name
    35    | NONE => (case t of 
    35    | NONE => (case t of