1 (* Title: state_space.ML |
1 (* Title: state_space.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Norbert Schirmer, TU Muenchen |
3 Author: Norbert Schirmer, TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 structure StateSpace = |
6 signature STATE_SPACE = |
|
7 sig |
|
8 val KN : string |
|
9 val distinct_compsN : string |
|
10 val getN : string |
|
11 val putN : string |
|
12 val injectN : string |
|
13 val namespaceN : string |
|
14 val projectN : string |
|
15 val valuetypesN : string |
|
16 |
|
17 val quiet_mode : bool ref |
|
18 |
|
19 val namespace_definition : |
|
20 bstring -> |
|
21 Term.typ -> |
|
22 Locale.expr -> |
|
23 string list -> string list -> Context.theory -> Context.theory |
|
24 |
|
25 val define_statespace : |
|
26 string list -> |
|
27 string -> |
|
28 (string list * bstring * (string * string) list) list -> |
|
29 (string * string) list -> Context.theory -> Context.theory |
|
30 val define_statespace_i : |
|
31 string option -> |
|
32 string list -> |
|
33 string -> |
|
34 (Term.typ list * bstring * (string * string) list) list -> |
|
35 (string * Term.typ) list -> Context.theory -> Context.theory |
|
36 |
|
37 val statespace_decl : |
|
38 OuterParse.token list -> |
|
39 ((string list * bstring) * |
|
40 ((string list * xstring * (bstring * bstring) list) list * |
|
41 (bstring * string) list)) * OuterParse.token list |
|
42 |
|
43 |
|
44 val neq_x_y : Context.proof -> Term.term -> Term.term -> Thm.thm option |
|
45 val distinctNameSolver : MetaSimplifier.solver |
|
46 val distinctTree_tac : |
|
47 Context.proof -> Term.term * int -> Tactical.tactic |
|
48 val distinct_simproc : MetaSimplifier.simproc |
|
49 |
|
50 |
|
51 val change_simpset : (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> |
|
52 Context.generic -> Context.generic |
|
53 |
|
54 val get_comp : Context.generic -> string -> (Term.typ * string) Option.option |
|
55 val get_silent : Context.generic -> bool |
|
56 val set_silent : bool -> Context.generic -> Context.generic |
|
57 |
|
58 val read_typ : |
|
59 Context.theory -> |
|
60 string -> |
|
61 (string * Term.sort) list -> Term.typ * (string * Term.sort) list |
|
62 |
|
63 val gen_lookup_tr : Context.proof -> Term.term -> string -> Term.term |
|
64 val lookup_swap_tr : Context.proof -> Term.term list -> Term.term |
|
65 val lookup_tr : Context.proof -> Term.term list -> Term.term |
|
66 val lookup_tr' : Context.proof -> Term.term list -> Term.term |
|
67 |
|
68 val gen_update_tr : |
|
69 bool -> Context.proof -> string -> Term.term -> Term.term -> Term.term |
|
70 val update_tr : Context.proof -> Term.term list -> Term.term |
|
71 val update_tr' : Context.proof -> Term.term list -> Term.term |
|
72 end; |
|
73 |
|
74 |
|
75 structure StateSpace: STATE_SPACE = |
7 struct |
76 struct |
8 |
77 |
9 (* Theorems *) |
78 (* Theorems *) |
10 |
79 |
11 (* Names *) |
80 (* Names *) |