--- 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
--- 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) =
--- 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
--- 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 *)