22   \ldots

    22   \ldots

    23   \end{tabular}

    23   \end{tabular}

    24   \end{center}

    24   \end{center}

    25 *}

    25 *}

    26 

    26 

    28 

    28 

    29 text {*

    29 text {*

    30   The easiest and quickest way to include code in a theory is

    30   The easiest and quickest way to include code in a theory is

    31   by using the \isacommand{ML} command. For example

    31   by using the \isacommand{ML} command. For example

    32 *}

    32 *}

   290 *}

   290 *}

   291 

   291 

   292 text {*

   292 text {*

   293 

   293 

   294   The reason is that one cannot pass the arguments @{term P}, @{term Q} and 

   294   The reason is that one cannot pass the arguments @{term P}, @{term Q} and 

   296 *}

   296 *}

   297 

   297 

   298 ML {*

   298 ML {*

   299   fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"} 

   299   fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"} 

   300 *}

   300 *}

   320 *}

   320 *}

   321  

   321  

   322 text {*

   322 text {*

   323 

   323 

   324   (FIXME: Is it useful to explain @{text "@{const_syntax}"}?)

   324   (FIXME: Is it useful to explain @{text "@{const_syntax}"}?)

   325 

   327 

   326   \begin{readmore}

   328   \begin{readmore}

   327   There are many functions in @{ML_file "Pure/logic.ML"} and

   329   There are many functions in @{ML_file "Pure/logic.ML"} and

   328   @{ML_file "HOL/hologic.ML"} that make such manual constructions of terms 

   330   @{ML_file "HOL/hologic.ML"} that make such manual constructions of terms 

   329   easier.\end{readmore}

   331   easier.\end{readmore}

   360   term is well-formed, or type checks, relative to a theory.

   362   term is well-formed, or type checks, relative to a theory.

   361   Type checking is done via the function @{ML cterm_of}, which turns 

   363   Type checking is done via the function @{ML cterm_of}, which turns 

   362   a @{ML_type term} into a  @{ML_type cterm}, a \emph{certified} term. 

   364   a @{ML_type term} into a  @{ML_type cterm}, a \emph{certified} term. 

   363   Unlike @{ML_type term}s, which are just trees, @{ML_type

   365   Unlike @{ML_type term}s, which are just trees, @{ML_type

   364   "cterm"}s are abstract objects that are guaranteed to be

   366   "cterm"}s are abstract objects that are guaranteed to be

   366   interfaces.

   368   interfaces.

   367 

   369 

   368   Type checking is always relative to a theory context. For now we can use

   370   Type checking is always relative to a theory context. For now we can use

   369   the @{ML "@{theory}"} antiquotation to get hold of the current theory.

   371   the @{ML "@{theory}"} antiquotation to get hold of the current theory.

   370   For example we can write:

   372   For example we can write:

   371 *}

   373 *}

   372 

   374 

   373 ML {* cterm_of @{theory} @{term "(a::nat) + b = c"} *}

   375 ML {* cterm_of @{theory} @{term "(a::nat) + b = c"} *}

   374 

   378 

   375 ML {*

   379 ML {*

   376   let

   380   let

   377     val natT = @{typ "nat"}

   381     val natT = @{typ "nat"}

   378     val zero = @{term "0::nat"}

   382     val zero = @{term "0::nat"}

   457   convention is an implication of the form:

   461   convention is an implication of the form:

   458 

   462 

   459   @{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> #(C)"}

   463   @{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> #(C)"}

   460 

   464 

   461   where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are the open subgoals. 

   465   where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are the open subgoals. 

   463   Since the goal @{term C} can potentially be an implication, there is a

   466   Since the goal @{term C} can potentially be an implication, there is a

   464   @{text "#"} wrapped around it, which prevents that premises are 

   467   @{text "#"} wrapped around it, which prevents that premises are 

   465   misinterpreted as open subgoals. The protection @{text "# :: prop \<Rightarrow>

   468   misinterpreted as open subgoals. The protection @{text "# :: prop \<Rightarrow>

   466   prop"} is just the identity function and used as a syntactic marker. 

   469   prop"} is just the identity function and used as a syntactic marker. 

   467   

   470   

   538     THEN' resolve_tac [disjI1] 

   541     THEN' resolve_tac [disjI1] 

   539     THEN' assume_tac) 1)

   542     THEN' assume_tac) 1)

   540 end

   543 end

   541 *}

   544 *}

   542 

   545 

   544 

   551 

   545 end

   552 end