CookBook/FirstSteps.thy
changeset 68 e7519207c2b7
parent 66 d563f8ff6aa0
child 69 19106a9975c1
equal deleted inserted replaced
67:5fbeeac2901b 68:e7519207c2b7
   224 
   224 
   225   @{ML [display] "print_depth 50"}
   225   @{ML [display] "print_depth 50"}
   226 
   226 
   227   The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type, 
   227   The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type, 
   228   inserting the invisible @{text "Trueprop"}-coercions whenever necessary. 
   228   inserting the invisible @{text "Trueprop"}-coercions whenever necessary. 
   229   Consider for example
   229   Consider for example the pairs
   230 
   230 
   231   @{ML_response [display] "(@{term \"P x\"}, @{prop \"P x\"})" "(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),
   231   @{ML_response [display] "(@{term \"P x\"}, @{prop \"P x\"})" "(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),
   232  Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}
   232  Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}
   233  
   233  
   234   which inserts the coercion in the second component and 
   234   where an coercion is inserted in the second component and 
   235 
   235 
   236   @{ML_response [display] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})" 
   236   @{ML_response [display] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})" 
   237   "(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>, Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"}
   237   "(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>, Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"}
   238 
   238 
   239   which does not (since it is already constructed using the meta-implication). 
   239   where it is not (since it is already constructed using the meta-implication). 
   240 
   240 
   241   Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example
   241   Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example
   242 
   242 
   243   @{ML_response_fake [display] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}
   243   @{ML_response_fake [display] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}
   244 
   244 
   279 fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"} 
   279 fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"} 
   280 *}
   280 *}
   281 
   281 
   282 text {*
   282 text {*
   283   To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} 
   283   To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} 
   284   to both functions: 
   284   to both functions. With @{ML make_imp} we obtain the correct term involving 
       
   285   @{term "S"}, @{text "T"} and  @{text "@{typ nat}"} 
   285 
   286 
   286   @{ML_response [display] "make_imp @{term S} @{term T} @{typ nat}" 
   287   @{ML_response [display] "make_imp @{term S} @{term T} @{typ nat}" 
   287     "Const \<dots> $ 
   288     "Const \<dots> $ 
   288     Abs (\"x\", Type (\"nat\",[]),
   289     Abs (\"x\", Type (\"nat\",[]),
   289       Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ 
   290       Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ 
   290                   (Free (\"T\",\<dots>) $ \<dots>))"}
   291                   (Free (\"T\",\<dots>) $ \<dots>))"}
       
   292 
       
   293   With @{ML make_wrong_imp} we obtain an incorrect term involving the @{term "P"} 
       
   294   and @{text "Q"} from the antiquotation.
       
   295 
   291   @{ML_response [display] "make_wrong_imp @{term S} @{term T} @{typ nat}" 
   296   @{ML_response [display] "make_wrong_imp @{term S} @{term T} @{typ nat}" 
   292     "Const \<dots> $ 
   297     "Const \<dots> $ 
   293     Abs (\"x\", \<dots>,
   298     Abs (\"x\", \<dots>,
   294       Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ 
   299       Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ 
   295                   (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
   300                   (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
   296 
   301 
   297   As can be seen, in the first case the arguments are correctly used, while the 
   302   One tricky point in constructing terms by hand is to obtain the fully
   298   second generates a term involving the @{term "P"} and @{text "Q"} from the 
   303   qualified name for constants. For example the names for @{text "zero"} and
   299   antiquotation.
   304   @{text "+"} are more complex than one first expects, namely
   300 
   305 
   301   One tricky point in constructing terms by hand is to obtain the 
       
   302   fully qualified name for constants. For example the names for @{text "zero"} and
       
   303   @{text "+"} are more complex than one first expects, namely 
       
   304 
   306 
   305   \begin{center}
   307   \begin{center}
   306   @{text "HOL.zero_class.zero"} and @{text "HOL.plus_class.plus"}. 
   308   @{text "HOL.zero_class.zero"} and @{text "HOL.plus_class.plus"}. 
   307   \end{center}
   309   \end{center}
   308   
   310   
   309   The extra prefixes @{text zero_class} and @{text plus_class} are present because 
   311   The extra prefixes @{text zero_class} and @{text plus_class} are present
   310   these constants are defined within type classes; the prefix @{text "HOL"} indicates in 
   312   because these constants are defined within type classes; the prefix @{text
   311   which theory they are defined. Guessing such internal names can sometimes be quite hard. 
   313   "HOL"} indicates in which theory they are defined. Guessing such internal
   312   Therefore Isabelle provides the antiquotation @{text "@{const_name \<dots>}"} which does the 
   314   names can sometimes be quite hard. Therefore Isabelle provides the
   313   expansion automatically, for example:
   315   antiquotation @{text "@{const_name \<dots>}"} which does the expansion
       
   316   automatically, for example:
   314 
   317 
   315   @{ML_response_fake [display] "@{const_name \"Nil\"}" "List.list.Nil"}
   318   @{ML_response_fake [display] "@{const_name \"Nil\"}" "List.list.Nil"}
   316 
   319 
   317   (FIXME: Is it useful to explain @{text "@{const_syntax}"}?)
   320   (FIXME: Is it useful to explain @{text "@{const_syntax}"}?)
   318 
   321 
   573 section {* Storing Theorems *}
   576 section {* Storing Theorems *}
   574 
   577 
   575 section {* Theorem Attributes *}
   578 section {* Theorem Attributes *}
   576 
   579 
   577 
   580 
   578 
   581 section {* Combinators *}
       
   582 
       
   583 text {*
       
   584   @{text I}, @{text K}
       
   585   
       
   586 *}
   579 
   587 
   580 end
   588 end