51 given for a particular predicate or parameter, this means that the type should be |
51 given for a particular predicate or parameter, this means that the type should be |
52 inferred by the package. Additional \emph{mixfix syntax} may be associated with |
52 inferred by the package. Additional \emph{mixfix syntax} may be associated with |
53 the predicates and parameters as well. Note that @{ML add_inductive_i in SIP} does not |
53 the predicates and parameters as well. Note that @{ML add_inductive_i in SIP} does not |
54 allow mixfix syntax to be associated with parameters, since it can only be used |
54 allow mixfix syntax to be associated with parameters, since it can only be used |
55 for parsing. The names of the predicates, parameters and rules are represented by the |
55 for parsing. The names of the predicates, parameters and rules are represented by the |
56 type @{ML_type Binding.T}. Strings can be turned into elements of the type |
56 type @{ML_type Binding.binding}. Strings can be turned into elements of the type |
57 @{ML_type Binding.T} using the function |
57 @{ML_type Binding.binding} using the function |
58 @{ML [display] "Binding.name : string -> Binding.T"} |
58 @{ML [display] "Binding.name : string -> Binding.binding"} |
59 Each introduction rule is given as a tuple containing its name, a list of \emph{attributes} |
59 Each introduction rule is given as a tuple containing its name, a list of \emph{attributes} |
60 and a logical formula. Note that the type @{ML_type Attrib.binding} used in the list of |
60 and a logical formula. Note that the type @{ML_type Attrib.binding} used in the list of |
61 introduction rules is just a shorthand for the type @{ML_type "Binding.T * Attrib.src list"}. |
61 introduction rules is just a shorthand for the type @{ML_type "Binding.binding * Attrib.src list"}. |
62 The function @{ML add_inductive_i in SIP} expects the formula to be specified using the datatype |
62 The function @{ML add_inductive_i in SIP} expects the formula to be specified using the datatype |
63 @{ML_type term}, whereas @{ML add_inductive in SIP} expects it to be given as a string. |
63 @{ML_type term}, whereas @{ML add_inductive in SIP} expects it to be given as a string. |
64 An attribute specifies additional actions and transformations that should be applied to |
64 An attribute specifies additional actions and transformations that should be applied to |
65 a theorem, such as storing it in the rule databases used by automatic tactics |
65 a theorem, such as storing it in the rule databases used by automatic tactics |
66 like the simplifier. The code of the package, which will be described in the following |
66 like the simplifier. The code of the package, which will be described in the following |
70 of the package is quite simple. Essentially, it just parses the introduction rules |
70 of the package is quite simple. Essentially, it just parses the introduction rules |
71 and then passes them on to @{ML add_inductive_i in SIP}: |
71 and then passes them on to @{ML add_inductive_i in SIP}: |
72 @{ML_chunk [display] add_inductive} |
72 @{ML_chunk [display] add_inductive} |
73 For parsing and type checking the introduction rules, we use the function |
73 For parsing and type checking the introduction rules, we use the function |
74 @{ML [display] "Specification.read_specification: |
74 @{ML [display] "Specification.read_specification: |
75 (Binding.T * string option * mixfix) list -> (*{variables}*) |
75 (Binding.binding * string option * mixfix) list -> (*{variables}*) |
76 (Attrib.binding * string list) list list -> (*{rules}*) |
76 (Attrib.binding * string list) list list -> (*{rules}*) |
77 local_theory -> |
77 local_theory -> |
78 (((Binding.T * typ) * mixfix) list * |
78 (((Binding.binding * typ) * mixfix) list * |
79 (Attrib.binding * term list) list) * |
79 (Attrib.binding * term list) list) * |
80 local_theory"} |
80 local_theory"} |
81 *} |
81 *} |
82 |
82 |
83 text {* |
83 text {* |
125 Const (\"==>\", \<dots>) $ |
125 Const (\"==>\", \<dots>) $ |
126 (Const (\"Trueprop\", \<dots>) $ |
126 (Const (\"Trueprop\", \<dots>) $ |
127 (Free (\"trcl\", \<dots>) $ Free (\"r\", \<dots>) $ Bound 2 $ Bound 1)) $ |
127 (Free (\"trcl\", \<dots>) $ Free (\"r\", \<dots>) $ Bound 2 $ Bound 1)) $ |
128 (Const (\"==>\", \<dots>) $ \<dots> $ \<dots>))))])]), |
128 (Const (\"==>\", \<dots>) $ \<dots> $ \<dots>))))])]), |
129 \<dots>) |
129 \<dots>) |
130 : (((Binding.T * typ) * mixfix) list * |
130 : (((Binding.binding * typ) * mixfix) list * |
131 (Attrib.binding * term list) list) * local_theory"} |
131 (Attrib.binding * term list) list) * local_theory"} |
132 In the list of variables passed to @{ML read_specification in Specification}, we have |
132 In the list of variables passed to @{ML read_specification in Specification}, we have |
133 used the mixfix annotation @{ML NoSyn} to indicate that we do not want to associate any |
133 used the mixfix annotation @{ML NoSyn} to indicate that we do not want to associate any |
134 mixfix syntax with the variable. Moreover, we have only specified the type of \texttt{r}, |
134 mixfix syntax with the variable. Moreover, we have only specified the type of \texttt{r}, |
135 whereas the type of \texttt{trcl} is computed using type inference. |
135 whereas the type of \texttt{trcl} is computed using type inference. |
380 @{ML "enum1: string -> (token list -> 'a * token list) -> token list -> |
380 @{ML "enum1: string -> (token list -> 'a * token list) -> token list -> |
381 'a list * token list" in OuterParse} \\ |
381 'a list * token list" in OuterParse} \\ |
382 @{ML "prop: token list -> string * token list" in OuterParse} \\ |
382 @{ML "prop: token list -> string * token list" in OuterParse} \\ |
383 @{ML "opt_target: token list -> string option * token list" in OuterParse} \\ |
383 @{ML "opt_target: token list -> string option * token list" in OuterParse} \\ |
384 @{ML "fixes: token list -> |
384 @{ML "fixes: token list -> |
385 (Binding.T * string option * mixfix) list * token list" in OuterParse} \\ |
385 (Binding.binding * string option * mixfix) list * token list" in OuterParse} \\ |
386 @{ML "for_fixes: token list -> |
386 @{ML "for_fixes: token list -> |
387 (Binding.T * string option * mixfix) list * token list" in OuterParse} \\ |
387 (Binding.binding * string option * mixfix) list * token list" in OuterParse} \\ |
388 @{ML "!!! : (token list -> 'a) -> token list -> 'a" in OuterParse} |
388 @{ML "!!! : (token list -> 'a) -> token list -> 'a" in OuterParse} |
389 \end{table} |
389 \end{table} |
390 |
390 |
391 The parsers @{ML "$$$" in OuterParse} and @{ML "!!!" in OuterParse} are |
391 The parsers @{ML "$$$" in OuterParse} and @{ML "!!!" in OuterParse} are |
392 defined using the parsers @{ML "one" in Scan} and @{ML "!!"} from |
392 defined using the parsers @{ML "one" in Scan} and @{ML "!!"} from |