added signatures;
authorschirmer
Mon Nov 12 11:07:22 2007 +0100 (2007-11-12)
changeset 25408156f6f7082b8
parent 25407 2859cf34aaf0
child 25409 b87196bb57da
added signatures;
tuned
src/HOL/Statespace/StateFun.thy
src/HOL/Statespace/distinct_tree_prover.ML
src/HOL/Statespace/state_fun.ML
src/HOL/Statespace/state_space.ML
     1.1 --- a/src/HOL/Statespace/StateFun.thy	Sun Nov 11 20:29:07 2007 +0100
     1.2 +++ b/src/HOL/Statespace/StateFun.thy	Mon Nov 12 11:07:22 2007 +0100
     1.3 @@ -6,7 +6,6 @@
     1.4  header {* State Space Representation as Function \label{sec:StateFun}*}
     1.5  
     1.6  theory StateFun imports DistinctTreeProver 
     1.7 -(*uses "state_space.ML" ("state_fun.ML")*)
     1.8  begin
     1.9  
    1.10  
    1.11 @@ -109,7 +108,4 @@
    1.12    apply simp
    1.13    oops
    1.14  
    1.15 -(*use "state_fun.ML"
    1.16 -setup StateFun.setup
    1.17 -*)
    1.18  end
    1.19 \ No newline at end of file
     2.1 --- a/src/HOL/Statespace/distinct_tree_prover.ML	Sun Nov 11 20:29:07 2007 +0100
     2.2 +++ b/src/HOL/Statespace/distinct_tree_prover.ML	Mon Nov 12 11:07:22 2007 +0100
     2.3 @@ -3,7 +3,29 @@
     2.4      Author:     Norbert Schirmer, TU Muenchen
     2.5  *)
     2.6  
     2.7 -structure DistinctTreeProver =
     2.8 +signature DISTINCT_TREE_PROVER =
     2.9 +sig
    2.10 +  datatype Direction = Left | Right
    2.11 +  val mk_tree : ('a -> Term.term) -> Term.typ -> 'a list -> Term.term
    2.12 +  val dest_tree : Term.term -> Term.term list
    2.13 +  val find_tree :
    2.14 +       Term.term -> Term.term -> Direction list option 
    2.15 +
    2.16 +  val neq_to_eq_False : Thm.thm
    2.17 +  val distinctTreeProver : Thm.thm -> Direction list -> Direction list -> Thm.thm
    2.18 +  val neq_x_y :
    2.19 +       Proof.context -> Term.term -> Term.term -> string -> Thm.thm option   
    2.20 +  val distinctFieldSolver : string list -> MetaSimplifier.solver
    2.21 +  val distinctTree_tac :
    2.22 +       string list -> Proof.context -> Term.term * int -> Tactical.tactic
    2.23 +  val distinct_implProver : Thm.thm -> Thm.cterm -> Thm.thm
    2.24 +  val subtractProver : Term.term -> Thm.cterm -> Thm.thm -> Thm.thm
    2.25 +  val distinct_simproc : string list -> MetaSimplifier.simproc
    2.26 +  
    2.27 +  val discharge : Thm.thm list -> Thm.thm -> Thm.thm
    2.28 +end;
    2.29 +
    2.30 +structure DistinctTreeProver : DISTINCT_TREE_PROVER =
    2.31  struct
    2.32  val all_distinct_left = thm "DistinctTreeProver.all_distinct_left";
    2.33  val all_distinct_right = thm "DistinctTreeProver.all_distinct_right";
    2.34 @@ -18,6 +40,8 @@
    2.35  val swap_neq = thm "DistinctTreeProver.swap_neq";
    2.36  val neq_to_eq_False = thm "DistinctTreeProver.neq_to_eq_False"
    2.37  
    2.38 +datatype Direction = Left | Right 
    2.39 +
    2.40  fun treeT T = Type ("DistinctTreeProver.tree",[T]);
    2.41  fun mk_tree' e T n []     = Const ("DistinctTreeProver.tree.Tip",treeT T)
    2.42    | mk_tree' e T n xs =
    2.43 @@ -37,7 +61,7 @@
    2.44    | dest_tree (Const ("DistinctTreeProver.tree.Node",_)$l$e$_$r) = dest_tree l @ e :: dest_tree r
    2.45    | dest_tree t = raise TERM ("DistinctTreeProver.dest_tree",[t]);
    2.46  
    2.47 -datatype Direction = Left | Right 
    2.48 +
    2.49  
    2.50  fun lin_find_tree e (Const ("DistinctTreeProver.tree.Tip",_)) = NONE
    2.51    | lin_find_tree e (Const ("DistinctTreeProver.tree.Node",_) $ l$ x $ _ $ r) =
     3.1 --- a/src/HOL/Statespace/state_fun.ML	Sun Nov 11 20:29:07 2007 +0100
     3.2 +++ b/src/HOL/Statespace/state_fun.ML	Mon Nov 12 11:07:22 2007 +0100
     3.3 @@ -3,31 +3,31 @@
     3.4      Author:     Norbert Schirmer, TU Muenchen
     3.5  *)
     3.6  
     3.7 +signature STATE_FUN =
     3.8 +sig
     3.9 +  val lookupN : string
    3.10 +  val updateN : string
    3.11  
    3.12 -structure StateFun =
    3.13 +  val mk_constr : Context.theory -> Term.typ -> Term.term
    3.14 +  val mk_destr : Context.theory -> Term.typ -> Term.term
    3.15 +
    3.16 +  val lookup_simproc : MetaSimplifier.simproc
    3.17 +  val update_simproc : MetaSimplifier.simproc
    3.18 +  val ex_lookup_eq_simproc : MetaSimplifier.simproc
    3.19 +  val ex_lookup_ss : MetaSimplifier.simpset
    3.20 +  val lazy_conj_simproc : MetaSimplifier.simproc
    3.21 +  val string_eq_simp_tac : int -> Tactical.tactic
    3.22 +
    3.23 +  val setup : Context.theory -> Context.theory
    3.24 +end;
    3.25 +
    3.26 +structure StateFun: STATE_FUN = 
    3.27  struct
    3.28  
    3.29  val lookupN = "StateFun.lookup";
    3.30  val updateN = "StateFun.update";
    3.31  
    3.32 -
    3.33 -fun dest_nib c =
    3.34 -     let val h = List.last (String.explode c) 
    3.35 -     in if #"0" <= h andalso h <= #"9" then Char.ord h - Char.ord #"0"
    3.36 -        else if #"A" <= h andalso h <= #"F" then Char.ord h - Char.ord #"A" + 10
    3.37 -        else raise Match
    3.38 -     end;
    3.39 -
    3.40 -fun dest_chr (Const ("List.char.Char",_)$Const (c1,_)$(Const (c2,_))) = 
    3.41 -    let val c = Char.chr (dest_nib c1 * 16 + dest_nib c2)
    3.42 -    in if Char.isPrint c then c else raise Match end
    3.43 -  | dest_chr _ = raise Match;
    3.44 -
    3.45 -fun dest_string (Const ("List.list.Nil",_)) = []
    3.46 -  | dest_string (Const ("List.list.Cons",_)$c$cs) = dest_chr c::dest_string cs
    3.47 -  | dest_string _ = raise TERM ("dest_string",[]);
    3.48 -
    3.49 -fun sel_name n = String.implode (dest_string n);
    3.50 +val sel_name = HOLogic.dest_string;
    3.51  
    3.52  fun mk_name i t =
    3.53    (case try sel_name t of
     4.1 --- a/src/HOL/Statespace/state_space.ML	Sun Nov 11 20:29:07 2007 +0100
     4.2 +++ b/src/HOL/Statespace/state_space.ML	Mon Nov 12 11:07:22 2007 +0100
     4.3 @@ -3,7 +3,76 @@
     4.4      Author:     Norbert Schirmer, TU Muenchen
     4.5  *)
     4.6  
     4.7 -structure StateSpace =
     4.8 +signature STATE_SPACE =
     4.9 +  sig
    4.10 +    val KN : string
    4.11 +    val distinct_compsN : string
    4.12 +    val getN : string
    4.13 +    val putN : string
    4.14 +    val injectN : string
    4.15 +    val namespaceN : string
    4.16 +    val projectN : string
    4.17 +    val valuetypesN : string
    4.18 +
    4.19 +    val quiet_mode : bool ref
    4.20 +
    4.21 +    val namespace_definition :
    4.22 +       bstring ->
    4.23 +       Term.typ ->
    4.24 +       Locale.expr ->
    4.25 +       string list -> string list -> Context.theory -> Context.theory
    4.26 +
    4.27 +    val define_statespace :
    4.28 +       string list ->
    4.29 +       string ->
    4.30 +       (string list * bstring * (string * string) list) list ->
    4.31 +       (string * string) list -> Context.theory -> Context.theory
    4.32 +    val define_statespace_i :
    4.33 +       string option ->
    4.34 +       string list ->
    4.35 +       string ->
    4.36 +       (Term.typ list * bstring * (string * string) list) list ->
    4.37 +       (string * Term.typ) list -> Context.theory -> Context.theory
    4.38 +
    4.39 +    val statespace_decl :
    4.40 +       OuterParse.token list -> 
    4.41 +       ((string list * bstring) *
    4.42 +         ((string list * xstring * (bstring * bstring) list) list *
    4.43 +          (bstring * string) list)) * OuterParse.token list
    4.44 +
    4.45 +
    4.46 +    val neq_x_y : Context.proof -> Term.term -> Term.term -> Thm.thm option
    4.47 +    val distinctNameSolver : MetaSimplifier.solver
    4.48 +    val distinctTree_tac :
    4.49 +       Context.proof -> Term.term * int -> Tactical.tactic
    4.50 +    val distinct_simproc : MetaSimplifier.simproc
    4.51 +
    4.52 +
    4.53 +    val change_simpset : (MetaSimplifier.simpset -> MetaSimplifier.simpset) ->
    4.54 +       Context.generic -> Context.generic
    4.55 +
    4.56 +    val get_comp : Context.generic -> string -> (Term.typ * string) Option.option
    4.57 +    val get_silent : Context.generic -> bool
    4.58 +    val set_silent : bool -> Context.generic -> Context.generic
    4.59 +
    4.60 +    val read_typ :
    4.61 +       Context.theory ->
    4.62 +       string ->
    4.63 +       (string * Term.sort) list -> Term.typ * (string * Term.sort) list
    4.64 +
    4.65 +    val gen_lookup_tr : Context.proof -> Term.term -> string -> Term.term
    4.66 +    val lookup_swap_tr : Context.proof -> Term.term list -> Term.term
    4.67 +    val lookup_tr : Context.proof -> Term.term list -> Term.term
    4.68 +    val lookup_tr' : Context.proof -> Term.term list -> Term.term
    4.69 +
    4.70 +    val gen_update_tr :
    4.71 +       bool -> Context.proof -> string -> Term.term -> Term.term -> Term.term
    4.72 +    val update_tr : Context.proof -> Term.term list -> Term.term
    4.73 +    val update_tr' : Context.proof -> Term.term list -> Term.term
    4.74 +  end;
    4.75 +
    4.76 +
    4.77 +structure StateSpace: STATE_SPACE =
    4.78  struct
    4.79  
    4.80  (* Theorems *)