27 Uncertified terms are often just called terms. One way to construct them is by |
27 Uncertified terms are often just called terms. One way to construct them is by |
28 using the antiquotation \mbox{\<open>@{term \<dots>}\<close>}. For example |
28 using the antiquotation \mbox{\<open>@{term \<dots>}\<close>}. For example |
29 |
29 |
30 @{ML_response [display,gray] |
30 @{ML_response [display,gray] |
31 "@{term \"(a::nat) + b = c\"}" |
31 "@{term \"(a::nat) + b = c\"}" |
32 "Const (\"HOL.eq\", \<dots>) $ |
32 "Const (\"HOL.eq\", _) $ |
33 (Const (\"Groups.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"} |
33 (Const (\"Groups.plus_class.plus\", _) $ _ $ _) $ _"} |
34 |
34 |
35 constructs the term @{term "(a::nat) + b = c"}. The resulting term is printed using |
35 constructs the term @{term "(a::nat) + b = c"}. The resulting term is printed using |
36 the internal representation corresponding to the datatype @{ML_type_ind "term"}, |
36 the internal representation corresponding to the datatype @{ML_type_ind "term"}, |
37 which is defined as follows: |
37 which is defined as follows: |
38 \<close> |
38 \<close> |
185 The antiquotation \<open>@{prop \<dots>}\<close> constructs terms by inserting the |
185 The antiquotation \<open>@{prop \<dots>}\<close> constructs terms by inserting the |
186 usually invisible \<open>Trueprop\<close>-coercions whenever necessary. |
186 usually invisible \<open>Trueprop\<close>-coercions whenever necessary. |
187 Consider for example the pairs |
187 Consider for example the pairs |
188 |
188 |
189 @{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" |
189 @{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" |
190 "(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>), |
190 "(Free (\"P\", _) $ Free (\"x\", _), |
191 Const (\"HOL.Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"} |
191 Const (\"HOL.Trueprop\", _) $ (Free (\"P\", _) $ Free (\"x\", _)))"} |
192 |
192 |
193 where a coercion is inserted in the second component and |
193 where a coercion is inserted in the second component and |
194 |
194 |
195 @{ML_response [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})" |
195 @{ML_response [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})" |
196 "(Const (\"Pure.imp\", \<dots>) $ \<dots> $ \<dots>, |
196 "(Const (\"Pure.imp\", _) $ _ $ _, |
197 Const (\"Pure.imp\", \<dots>) $ \<dots> $ \<dots>)"} |
197 Const (\"Pure.imp\", _) $ _ $ _)"} |
198 |
198 |
199 where it is not (since it is already constructed by a meta-implication). |
199 where it is not (since it is already constructed by a meta-implication). |
200 The purpose of the \<open>Trueprop\<close>-coercion is to embed formulae of |
200 The purpose of the \<open>Trueprop\<close>-coercion is to embed formulae of |
201 an object logic, for example HOL, into the meta-logic of Isabelle. The coercion |
201 an object logic, for example HOL, into the meta-logic of Isabelle. The coercion |
202 is needed whenever a term is constructed that will be proved as a theorem. |
202 is needed whenever a term is constructed that will be proved as a theorem. |
203 |
203 |
204 As already seen above, types can be constructed using the antiquotation |
204 As already seen above, types can be constructed using the antiquotation |
205 \<open>@{typ \<dots>}\<close>. For example: |
205 \<open>@{typ _}\<close>. For example: |
206 |
206 |
207 @{ML_response_fake [display,gray] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"} |
207 @{ML_response_fake [display,gray] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"} |
208 |
208 |
209 The corresponding datatype is |
209 The corresponding datatype is |
210 \<close> |
210 \<close> |
337 To see this, apply \<open>@{term S}\<close> and \<open>@{term T}\<close> |
337 To see this, apply \<open>@{term S}\<close> and \<open>@{term T}\<close> |
338 to both functions. With @{ML make_imp} you obtain the intended term involving |
338 to both functions. With @{ML make_imp} you obtain the intended term involving |
339 the given arguments |
339 the given arguments |
340 |
340 |
341 @{ML_response [display,gray] "make_imp @{term S} @{term T}" |
341 @{ML_response [display,gray] "make_imp @{term S} @{term T}" |
342 "Const \<dots> $ |
342 "Const _ $ |
343 Abs (\"x\", Type (\"Nat.nat\",[]), |
343 Abs (\"x\", Type (\"Nat.nat\",[]), |
344 Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ (Free (\"T\",\<dots>) $ \<dots>))"} |
344 Const _ $ (Free (\"S\",_) $ _) $ (Free (\"T\",_) $ _))"} |
345 |
345 |
346 whereas with @{ML make_wrong_imp} you obtain a term involving the @{term "P"} |
346 whereas with @{ML make_wrong_imp} you obtain a term involving the @{term "P"} |
347 and \<open>Q\<close> from the antiquotation. |
347 and \<open>Q\<close> from the antiquotation. |
348 |
348 |
349 @{ML_response [display,gray] "make_wrong_imp @{term S} @{term T}" |
349 @{ML_response [display,gray] "make_wrong_imp @{term S} @{term T}" |
350 "Const \<dots> $ |
350 "Const _ $ |
351 Abs (\"x\", \<dots>, |
351 Abs (\"x\", _, |
352 Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ |
352 Const _ $ (Const _ $ (Free (\"P\",_) $ _)) $ |
353 (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"} |
353 (Const _ $ (Free (\"Q\",_) $ _)))"} |
354 |
354 |
355 There are a number of handy functions that are frequently used for |
355 There are a number of handy functions that are frequently used for |
356 constructing terms. One is the function @{ML_ind list_comb in Term}, which |
356 constructing terms. One is the function @{ML_ind list_comb in Term}, which |
357 takes as argument a term and a list of terms, and produces as output the |
357 takes as argument a term and a list of terms, and produces as output the |
358 term list applied to the term. For example |
358 term list applied to the term. For example |
447 the body of the universal quantification. For example |
447 the body of the universal quantification. For example |
448 |
448 |
449 @{ML_response_fake [display, gray] |
449 @{ML_response_fake [display, gray] |
450 "strip_alls @{term \"\<forall>x y. x = (y::bool)\"}" |
450 "strip_alls @{term \"\<forall>x y. x = (y::bool)\"}" |
451 "([Free (\"x\", \"bool\"), Free (\"y\", \"bool\")], |
451 "([Free (\"x\", \"bool\"), Free (\"y\", \"bool\")], |
452 Const (\"op =\", \<dots>) $ Bound 1 $ Bound 0)"} |
452 Const (\"op =\", _) $ Bound 1 $ Bound 0)"} |
453 |
453 |
454 Note that we produced in the body two dangling de Bruijn indices. |
454 Note that we produced in the body two dangling de Bruijn indices. |
455 Later on we will also use the inverse function that |
455 Later on we will also use the inverse function that |
456 builds the quantification from a body and a list of (free) variables. |
456 builds the quantification from a body and a list of (free) variables. |
457 \<close> |
457 \<close> |
603 The problem is that on the ML-level the name of a constant is more |
603 The problem is that on the ML-level the name of a constant is more |
604 subtle than you might expect. The function @{ML is_all} worked correctly, |
604 subtle than you might expect. The function @{ML is_all} worked correctly, |
605 because @{term "All"} is such a fundamental constant, which can be referenced |
605 because @{term "All"} is such a fundamental constant, which can be referenced |
606 by @{ML "Const (\"All\", some_type)" for some_type}. However, if you look at |
606 by @{ML "Const (\"All\", some_type)" for some_type}. However, if you look at |
607 |
607 |
608 @{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", \<dots>)"} |
608 @{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", _)"} |
609 |
609 |
610 the name of the constant \<open>Nil\<close> depends on the theory in which the |
610 the name of the constant \<open>Nil\<close> depends on the theory in which the |
611 term constructor is defined (\<open>List\<close>) and also in which datatype |
611 term constructor is defined (\<open>List\<close>) and also in which datatype |
612 (\<open>list\<close>). Even worse, some constants have a name involving |
612 (\<open>list\<close>). Even worse, some constants have a name involving |
613 type-classes. Consider for example the constants for @{term "zero"} and |
613 type-classes. Consider for example the constants for @{term "zero"} and |
614 \mbox{@{term "times"}}: |
614 \mbox{@{term "times"}}: |
615 |
615 |
616 @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"times\"})" |
616 @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"times\"})" |
617 "(Const (\"Groups.zero_class.zero\", \<dots>), |
617 "(Const (\"Groups.zero_class.zero\", _), |
618 Const (\"Groups.times_class.times\", \<dots>))"} |
618 Const (\"Groups.times_class.times\", _))"} |
619 |
619 |
620 While you could use the complete name, for example |
620 While you could use the complete name, for example |
621 @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or |
621 @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or |
622 matching against \<open>Nil\<close>, this would make the code rather brittle. |
622 matching against \<open>Nil\<close>, this would make the code rather brittle. |
623 The reason is that the theory and the name of the datatype can easily change. |
623 The reason is that the theory and the name of the datatype can easily change. |