equal
deleted
inserted
replaced
242 theories @{text "HOL"} and @{text "Nat"}, respectively, they are |
242 theories @{text "HOL"} and @{text "Nat"}, respectively, they are |
243 still represented by their simple name. |
243 still represented by their simple name. |
244 |
244 |
245 @{ML_response [display,gray] |
245 @{ML_response [display,gray] |
246 "@{typ \"bool \<Rightarrow> nat\"}" |
246 "@{typ \"bool \<Rightarrow> nat\"}" |
247 "Type (\"fun\", [Type (\"bool\", []), Type (\"nat\", [])])"} |
247 "Type (\"fun\", [Type (\"bool\", []), Type (\"Nat.nat\", [])])"} |
248 |
248 |
249 We can restore the usual behaviour of Isabelle's pretty printer |
249 We can restore the usual behaviour of Isabelle's pretty printer |
250 with the code |
250 with the code |
251 *} |
251 *} |
252 |
252 |
301 to both functions. With @{ML make_imp} you obtain the intended term involving |
301 to both functions. With @{ML make_imp} you obtain the intended term involving |
302 the given arguments |
302 the given arguments |
303 |
303 |
304 @{ML_response [display,gray] "make_imp @{term S} @{term T}" |
304 @{ML_response [display,gray] "make_imp @{term S} @{term T}" |
305 "Const \<dots> $ |
305 "Const \<dots> $ |
306 Abs (\"x\", Type (\"nat\",[]), |
306 Abs (\"x\", Type (\"Nat.nat\",[]), |
307 Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ (Free (\"T\",\<dots>) $ \<dots>))"} |
307 Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ (Free (\"T\",\<dots>) $ \<dots>))"} |
308 |
308 |
309 whereas with @{ML make_wrong_imp} you obtain a term involving the @{term "P"} |
309 whereas with @{ML make_wrong_imp} you obtain a term involving the @{term "P"} |
310 and @{text "Q"} from the antiquotation. |
310 and @{text "Q"} from the antiquotation. |
311 |
311 |
339 val x_nat = @{term \"x::nat\"} |
339 val x_nat = @{term \"x::nat\"} |
340 val trm = @{term \"(P::nat \<Rightarrow> bool) x\"} |
340 val trm = @{term \"(P::nat \<Rightarrow> bool) x\"} |
341 in |
341 in |
342 lambda x_nat trm |
342 lambda x_nat trm |
343 end" |
343 end" |
344 "Abs (\"x\", \"nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Bound 0)"} |
344 "Abs (\"x\", \"Nat.nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Bound 0)"} |
345 |
345 |
346 In this example, @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound 0"}), |
346 In this example, @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound 0"}), |
347 and an abstraction, where it also records the type of the abstracted |
347 and an abstraction, where it also records the type of the abstracted |
348 variable and for printing purposes also its name. Note that because of the |
348 variable and for printing purposes also its name. Note that because of the |
349 typing annotation on @{text "P"}, the variable @{text "x"} in @{text "P x"} |
349 typing annotation on @{text "P"}, the variable @{text "x"} in @{text "P x"} |
444 "let |
444 "let |
445 val body = Bound 0 $ Free (\"x\", @{typ nat}) |
445 val body = Bound 0 $ Free (\"x\", @{typ nat}) |
446 in |
446 in |
447 Term.dest_abs (\"x\", @{typ \"nat \<Rightarrow> bool\"}, body) |
447 Term.dest_abs (\"x\", @{typ \"nat \<Rightarrow> bool\"}, body) |
448 end" |
448 end" |
449 "(\"xa\", Free (\"xa\", \"nat \<Rightarrow> bool\") $ Free (\"x\", \"nat\"))"} |
449 "(\"xa\", Free (\"xa\", \"Nat.nat \<Rightarrow> bool\") $ Free (\"x\", \"Nat.nat\"))"} |
450 |
450 |
451 There are also many convenient functions that construct specific HOL-terms |
451 There are also many convenient functions that construct specific HOL-terms |
452 in the structure @{ML_struct HOLogic}. For example @{ML_ind mk_eq in |
452 in the structure @{ML_struct HOLogic}. For example @{ML_ind mk_eq in |
453 HOLogic} constructs an equality out of two terms. The types needed in this |
453 HOLogic} constructs an equality out of two terms. The types needed in this |
454 equality are calculated from the type of the arguments. For example |
454 equality are calculated from the type of the arguments. For example |