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 Name.binding}. Strings can be turned into elements of the type |
56 type @{ML_type Binding.T}. Strings can be turned into elements of the type |
57 @{ML_type Name.binding} using the function |
57 @{ML_type Binding.T} using the function |
58 @{ML [display] "Name.binding : string -> Name.binding"} |
58 @{ML [display] "Binding.name : string -> Binding.T"} |
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 "Name.binding * Attrib.src list"}. |
61 introduction rules is just a shorthand for the type @{ML_type "Binding.T * 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 (Name.binding * string option * mixfix) list -> (*{variables}*) |
75 (Binding.T * 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 (((Name.binding * typ) * mixfix) list * |
78 (((Binding.T * 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 {* |
106 Finally, @{ML read_specification in Specification} also returns another local theory, |
106 Finally, @{ML read_specification in Specification} also returns another local theory, |
107 but we can safely discard it. As an example, let us look at how we can use this |
107 but we can safely discard it. As an example, let us look at how we can use this |
108 function to parse the introduction rules of the @{text trcl} predicate: |
108 function to parse the introduction rules of the @{text trcl} predicate: |
109 @{ML_response [display] |
109 @{ML_response [display] |
110 "Specification.read_specification |
110 "Specification.read_specification |
111 [(Name.binding \"trcl\", NONE, NoSyn), |
111 [(Binding.name \"trcl\", NONE, NoSyn), |
112 (Name.binding \"r\", SOME \"'a \<Rightarrow> 'a \<Rightarrow> bool\", NoSyn)] |
112 (Binding.name \"r\", SOME \"'a \<Rightarrow> 'a \<Rightarrow> bool\", NoSyn)] |
113 [[((Name.binding \"base\", []), [\"trcl r x x\"])], |
113 [[((Binding.name \"base\", []), [\"trcl r x x\"])], |
114 [((Name.binding \"step\", []), [\"trcl r x y \<Longrightarrow> r y z \<Longrightarrow> trcl r x z\"])]] |
114 [((Binding.name \"step\", []), [\"trcl r x y \<Longrightarrow> r y z \<Longrightarrow> trcl r x z\"])]] |
115 @{context}" |
115 @{context}" |
116 "((\<dots>, |
116 "((\<dots>, |
117 [(\<dots>, |
117 [(\<dots>, |
118 [Const (\"all\", \<dots>) $ Abs (\"x\", TFree (\"'a\", \<dots>), |
118 [Const (\"all\", \<dots>) $ Abs (\"x\", TFree (\"'a\", \<dots>), |
119 Const (\"Trueprop\", \<dots>) $ |
119 Const (\"Trueprop\", \<dots>) $ |
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 : (((Name.binding * typ) * mixfix) list * |
130 : (((Binding.T * 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. |
247 thm rel.accpartI' |
247 thm rel.accpartI' |
248 thm rel.accpart'.induct |
248 thm rel.accpart'.induct |
249 |
249 |
250 ML {* |
250 ML {* |
251 val (result, lthy) = SimpleInductivePackage.add_inductive |
251 val (result, lthy) = SimpleInductivePackage.add_inductive |
252 [(Name.binding "trcl'", NONE, NoSyn)] [(Name.binding "r", SOME "'a \<Rightarrow> 'a \<Rightarrow> bool", NoSyn)] |
252 [(Binding.name "trcl'", NONE, NoSyn)] [(Binding.name "r", SOME "'a \<Rightarrow> 'a \<Rightarrow> bool", NoSyn)] |
253 [((Name.binding "base", []), "\<And>x. trcl' r x x"), ((Name.binding "step", []), "\<And>x y z. trcl' r x y \<Longrightarrow> r y z \<Longrightarrow> trcl' r x z")] |
253 [((Binding.name "base", []), "\<And>x. trcl' r x x"), ((Binding.name "step", []), "\<And>x y z. trcl' r x y \<Longrightarrow> r y z \<Longrightarrow> trcl' r x z")] |
254 (TheoryTarget.init NONE @{theory}) |
254 (TheoryTarget.init NONE @{theory}) |
255 *} |
255 *} |
256 (*>*) |
256 (*>*) |
257 |
257 |
258 text {* |
258 text {* |
376 @{ML "enum1: string -> (token list -> 'a * token list) -> token list -> |
376 @{ML "enum1: string -> (token list -> 'a * token list) -> token list -> |
377 'a list * token list" in OuterParse} \\ |
377 'a list * token list" in OuterParse} \\ |
378 @{ML "prop: token list -> string * token list" in OuterParse} \\ |
378 @{ML "prop: token list -> string * token list" in OuterParse} \\ |
379 @{ML "opt_target: token list -> string option * token list" in OuterParse} \\ |
379 @{ML "opt_target: token list -> string option * token list" in OuterParse} \\ |
380 @{ML "fixes: token list -> |
380 @{ML "fixes: token list -> |
381 (Name.binding * string option * mixfix) list * token list" in OuterParse} \\ |
381 (Binding.T * string option * mixfix) list * token list" in OuterParse} \\ |
382 @{ML "for_fixes: token list -> |
382 @{ML "for_fixes: token list -> |
383 (Name.binding * string option * mixfix) list * token list" in OuterParse} \\ |
383 (Binding.T * string option * mixfix) list * token list" in OuterParse} \\ |
384 @{ML "!!! : (token list -> 'a) -> token list -> 'a" in OuterParse} |
384 @{ML "!!! : (token list -> 'a) -> token list -> 'a" in OuterParse} |
385 \end{mytable} |
385 \end{mytable} |
386 The parsers @{ML "$$$" in OuterParse} and @{ML "!!!" in OuterParse} are |
386 The parsers @{ML "$$$" in OuterParse} and @{ML "!!!" in OuterParse} are |
387 defined using the parsers @{ML "one" in Scan} and @{ML "!!"} from |
387 defined using the parsers @{ML "one" in Scan} and @{ML "!!"} from |
388 @{ML_struct Scan}. |
388 @{ML_struct Scan}. |