# HG changeset patch
# User schirmer
# Date 1194862042 -3600
# Node ID 156f6f7082b8f0f073c7b439896f0b2161ab8663
# Parent  2859cf34aaf00bb6c00b82c00287bd08f619e40b
added signatures;
tuned

diff -r 2859cf34aaf0 -r 156f6f7082b8 src/HOL/Statespace/StateFun.thy
--- a/src/HOL/Statespace/StateFun.thy	Sun Nov 11 20:29:07 2007 +0100
+++ b/src/HOL/Statespace/StateFun.thy	Mon Nov 12 11:07:22 2007 +0100
@@ -6,7 +6,6 @@
 header {* State Space Representation as Function \label{sec:StateFun}*}
 
 theory StateFun imports DistinctTreeProver 
-(*uses "state_space.ML" ("state_fun.ML")*)
 begin
 
 
@@ -109,7 +108,4 @@
   apply simp
   oops
 
-(*use "state_fun.ML"
-setup StateFun.setup
-*)
 end
\ No newline at end of file
diff -r 2859cf34aaf0 -r 156f6f7082b8 src/HOL/Statespace/distinct_tree_prover.ML
--- a/src/HOL/Statespace/distinct_tree_prover.ML	Sun Nov 11 20:29:07 2007 +0100
+++ b/src/HOL/Statespace/distinct_tree_prover.ML	Mon Nov 12 11:07:22 2007 +0100
@@ -3,7 +3,29 @@
     Author:     Norbert Schirmer, TU Muenchen
 *)
 
-structure DistinctTreeProver =
+signature DISTINCT_TREE_PROVER =
+sig
+  datatype Direction = Left | Right
+  val mk_tree : ('a -> Term.term) -> Term.typ -> 'a list -> Term.term
+  val dest_tree : Term.term -> Term.term list
+  val find_tree :
+       Term.term -> Term.term -> Direction list option 
+
+  val neq_to_eq_False : Thm.thm
+  val distinctTreeProver : Thm.thm -> Direction list -> Direction list -> Thm.thm
+  val neq_x_y :
+       Proof.context -> Term.term -> Term.term -> string -> Thm.thm option   
+  val distinctFieldSolver : string list -> MetaSimplifier.solver
+  val distinctTree_tac :
+       string list -> Proof.context -> Term.term * int -> Tactical.tactic
+  val distinct_implProver : Thm.thm -> Thm.cterm -> Thm.thm
+  val subtractProver : Term.term -> Thm.cterm -> Thm.thm -> Thm.thm
+  val distinct_simproc : string list -> MetaSimplifier.simproc
+  
+  val discharge : Thm.thm list -> Thm.thm -> Thm.thm
+end;
+
+structure DistinctTreeProver : DISTINCT_TREE_PROVER =
 struct
 val all_distinct_left = thm "DistinctTreeProver.all_distinct_left";
 val all_distinct_right = thm "DistinctTreeProver.all_distinct_right";
@@ -18,6 +40,8 @@
 val swap_neq = thm "DistinctTreeProver.swap_neq";
 val neq_to_eq_False = thm "DistinctTreeProver.neq_to_eq_False"
 
+datatype Direction = Left | Right 
+
 fun treeT T = Type ("DistinctTreeProver.tree",[T]);
 fun mk_tree' e T n []     = Const ("DistinctTreeProver.tree.Tip",treeT T)
   | mk_tree' e T n xs =
@@ -37,7 +61,7 @@
   | dest_tree (Const ("DistinctTreeProver.tree.Node",_)$l$e$_$r) = dest_tree l @ e :: dest_tree r
   | dest_tree t = raise TERM ("DistinctTreeProver.dest_tree",[t]);
 
-datatype Direction = Left | Right 
+
 
 fun lin_find_tree e (Const ("DistinctTreeProver.tree.Tip",_)) = NONE
   | lin_find_tree e (Const ("DistinctTreeProver.tree.Node",_) $ l$ x $ _ $ r) =
diff -r 2859cf34aaf0 -r 156f6f7082b8 src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Sun Nov 11 20:29:07 2007 +0100
+++ b/src/HOL/Statespace/state_fun.ML	Mon Nov 12 11:07:22 2007 +0100
@@ -3,31 +3,31 @@
     Author:     Norbert Schirmer, TU Muenchen
 *)
 
+signature STATE_FUN =
+sig
+  val lookupN : string
+  val updateN : string
 
-structure StateFun =
+  val mk_constr : Context.theory -> Term.typ -> Term.term
+  val mk_destr : Context.theory -> Term.typ -> Term.term
+
+  val lookup_simproc : MetaSimplifier.simproc
+  val update_simproc : MetaSimplifier.simproc
+  val ex_lookup_eq_simproc : MetaSimplifier.simproc
+  val ex_lookup_ss : MetaSimplifier.simpset
+  val lazy_conj_simproc : MetaSimplifier.simproc
+  val string_eq_simp_tac : int -> Tactical.tactic
+
+  val setup : Context.theory -> Context.theory
+end;
+
+structure StateFun: STATE_FUN = 
 struct
 
 val lookupN = "StateFun.lookup";
 val updateN = "StateFun.update";
 
-
-fun dest_nib c =
-     let val h = List.last (String.explode c) 
-     in if #"0" <= h andalso h <= #"9" then Char.ord h - Char.ord #"0"
-        else if #"A" <= h andalso h <= #"F" then Char.ord h - Char.ord #"A" + 10
-        else raise Match
-     end;
-
-fun dest_chr (Const ("List.char.Char",_)$Const (c1,_)$(Const (c2,_))) = 
-    let val c = Char.chr (dest_nib c1 * 16 + dest_nib c2)
-    in if Char.isPrint c then c else raise Match end
-  | dest_chr _ = raise Match;
-
-fun dest_string (Const ("List.list.Nil",_)) = []
-  | dest_string (Const ("List.list.Cons",_)$c$cs) = dest_chr c::dest_string cs
-  | dest_string _ = raise TERM ("dest_string",[]);
-
-fun sel_name n = String.implode (dest_string n);
+val sel_name = HOLogic.dest_string;
 
 fun mk_name i t =
   (case try sel_name t of
diff -r 2859cf34aaf0 -r 156f6f7082b8 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Sun Nov 11 20:29:07 2007 +0100
+++ b/src/HOL/Statespace/state_space.ML	Mon Nov 12 11:07:22 2007 +0100
@@ -3,7 +3,76 @@
     Author:     Norbert Schirmer, TU Muenchen
 *)
 
-structure StateSpace =
+signature STATE_SPACE =
+  sig
+    val KN : string
+    val distinct_compsN : string
+    val getN : string
+    val putN : string
+    val injectN : string
+    val namespaceN : string
+    val projectN : string
+    val valuetypesN : string
+
+    val quiet_mode : bool ref
+
+    val namespace_definition :
+       bstring ->
+       Term.typ ->
+       Locale.expr ->
+       string list -> string list -> Context.theory -> Context.theory
+
+    val define_statespace :
+       string list ->
+       string ->
+       (string list * bstring * (string * string) list) list ->
+       (string * string) list -> Context.theory -> Context.theory
+    val define_statespace_i :
+       string option ->
+       string list ->
+       string ->
+       (Term.typ list * bstring * (string * string) list) list ->
+       (string * Term.typ) list -> Context.theory -> Context.theory
+
+    val statespace_decl :
+       OuterParse.token list -> 
+       ((string list * bstring) *
+         ((string list * xstring * (bstring * bstring) list) list *
+          (bstring * string) list)) * OuterParse.token list
+
+
+    val neq_x_y : Context.proof -> Term.term -> Term.term -> Thm.thm option
+    val distinctNameSolver : MetaSimplifier.solver
+    val distinctTree_tac :
+       Context.proof -> Term.term * int -> Tactical.tactic
+    val distinct_simproc : MetaSimplifier.simproc
+
+
+    val change_simpset : (MetaSimplifier.simpset -> MetaSimplifier.simpset) ->
+       Context.generic -> Context.generic
+
+    val get_comp : Context.generic -> string -> (Term.typ * string) Option.option
+    val get_silent : Context.generic -> bool
+    val set_silent : bool -> Context.generic -> Context.generic
+
+    val read_typ :
+       Context.theory ->
+       string ->
+       (string * Term.sort) list -> Term.typ * (string * Term.sort) list
+
+    val gen_lookup_tr : Context.proof -> Term.term -> string -> Term.term
+    val lookup_swap_tr : Context.proof -> Term.term list -> Term.term
+    val lookup_tr : Context.proof -> Term.term list -> Term.term
+    val lookup_tr' : Context.proof -> Term.term list -> Term.term
+
+    val gen_update_tr :
+       bool -> Context.proof -> string -> Term.term -> Term.term -> Term.term
+    val update_tr : Context.proof -> Term.term list -> Term.term
+    val update_tr' : Context.proof -> Term.term list -> Term.term
+  end;
+
+
+structure StateSpace: STATE_SPACE =
 struct
 
 (* Theorems *)