src/HOL/Statespace/state_fun.ML
changeset 25408 156f6f7082b8
parent 25171 4a9c25bffc9b
child 26496 49ae9456eba9
     1.1 --- a/src/HOL/Statespace/state_fun.ML	Sun Nov 11 20:29:07 2007 +0100
     1.2 +++ b/src/HOL/Statespace/state_fun.ML	Mon Nov 12 11:07:22 2007 +0100
     1.3 @@ -3,31 +3,31 @@
     1.4      Author:     Norbert Schirmer, TU Muenchen
     1.5  *)
     1.6  
     1.7 +signature STATE_FUN =
     1.8 +sig
     1.9 +  val lookupN : string
    1.10 +  val updateN : string
    1.11  
    1.12 -structure StateFun =
    1.13 +  val mk_constr : Context.theory -> Term.typ -> Term.term
    1.14 +  val mk_destr : Context.theory -> Term.typ -> Term.term
    1.15 +
    1.16 +  val lookup_simproc : MetaSimplifier.simproc
    1.17 +  val update_simproc : MetaSimplifier.simproc
    1.18 +  val ex_lookup_eq_simproc : MetaSimplifier.simproc
    1.19 +  val ex_lookup_ss : MetaSimplifier.simpset
    1.20 +  val lazy_conj_simproc : MetaSimplifier.simproc
    1.21 +  val string_eq_simp_tac : int -> Tactical.tactic
    1.22 +
    1.23 +  val setup : Context.theory -> Context.theory
    1.24 +end;
    1.25 +
    1.26 +structure StateFun: STATE_FUN = 
    1.27  struct
    1.28  
    1.29  val lookupN = "StateFun.lookup";
    1.30  val updateN = "StateFun.update";
    1.31  
    1.32 -
    1.33 -fun dest_nib c =
    1.34 -     let val h = List.last (String.explode c) 
    1.35 -     in if #"0" <= h andalso h <= #"9" then Char.ord h - Char.ord #"0"
    1.36 -        else if #"A" <= h andalso h <= #"F" then Char.ord h - Char.ord #"A" + 10
    1.37 -        else raise Match
    1.38 -     end;
    1.39 -
    1.40 -fun dest_chr (Const ("List.char.Char",_)$Const (c1,_)$(Const (c2,_))) = 
    1.41 -    let val c = Char.chr (dest_nib c1 * 16 + dest_nib c2)
    1.42 -    in if Char.isPrint c then c else raise Match end
    1.43 -  | dest_chr _ = raise Match;
    1.44 -
    1.45 -fun dest_string (Const ("List.list.Nil",_)) = []
    1.46 -  | dest_string (Const ("List.list.Cons",_)$c$cs) = dest_chr c::dest_string cs
    1.47 -  | dest_string _ = raise TERM ("dest_string",[]);
    1.48 -
    1.49 -fun sel_name n = String.implode (dest_string n);
    1.50 +val sel_name = HOLogic.dest_string;
    1.51  
    1.52  fun mk_name i t =
    1.53    (case try sel_name t of