327 

   327 

   328 *}

   328 *}

   329 

   329 

   330 section {* Type Checking *}

   330 section {* Type Checking *}

   331 

   331 

   334 text {* 

   332 text {* 

   335   

   333   

   336   We can freely construct and manipulate terms, since they are just

   334   We can freely construct and manipulate terms, since they are just

   337   arbitrary unchecked trees. However, we eventually want to see if a

   335   arbitrary unchecked trees. However, we eventually want to see if a

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

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

   407 in

   405 in

   408 

   406 

   409   Qt 

   407   Qt 

   410   |> implies_intr assm2

   408   |> implies_intr assm2

   411   |> implies_intr assm1

   409   |> implies_intr assm1

   413 

   411 

   414   This code-snippet constructs the following proof:

   412   This code-snippet constructs the following proof:

   415 

   413 

   416   \[

   414   \[

   417   \infer[(@{text "\<Longrightarrow>"}$-$intro)]{\vdash @{prop "(\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> P t \<Longrightarrow> Q t"}}

   415   \infer[(@{text "\<Longrightarrow>"}$-$intro)]{\vdash @{prop "(\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> P t \<Longrightarrow> Q t"}}

   487  apply assumption

   485  apply assumption

   488 apply (rule disjI1)

   486 apply (rule disjI1)

   489 apply assumption

   487 apply assumption

   490 done

   488 done

   491 

   489 

   493 text {*

   490 text {*

   494   To start the proof, the function  @{ML "Goal.prove"}~@{text "ctxt xs As C tac"} sets 

   491   To start the proof, the function  @{ML "Goal.prove"}~@{text "ctxt xs As C tac"} sets 

   495   up a goal state for proving the goal @{text C} under the assumptions @{text As} 

   492   up a goal state for proving the goal @{text C} under the assumptions @{text As} 

   496   (empty in the proof at hand) 

   493   (empty in the proof at hand) 

   497   with the variables @{text xs} that will be generalised once the

   494   with the variables @{text xs} that will be generalised once the

   507     eresolve_tac [disjE] 1

   504     eresolve_tac [disjE] 1

   508     THEN resolve_tac [disjI2] 1

   505     THEN resolve_tac [disjI2] 1

   509     THEN assume_tac 1

   506     THEN assume_tac 1

   510     THEN resolve_tac [disjI1] 1

   507     THEN resolve_tac [disjI1] 1

   511     THEN assume_tac 1)

   508     THEN assume_tac 1)

   513 

   510 

   514   \begin{readmore}

   511   \begin{readmore}

   515   To learn more about the function @{ML Goal.prove} see \isccite{sec:results}.

   512   To learn more about the function @{ML Goal.prove} see \isccite{sec:results}.

   516   \end{readmore}

   513   \end{readmore}

   517 

   514 

   527     (eresolve_tac [disjE] 

   524     (eresolve_tac [disjE] 

   528     THEN' resolve_tac [disjI2] 

   525     THEN' resolve_tac [disjI2] 

   529     THEN' assume_tac 

   526     THEN' assume_tac 

   530     THEN' resolve_tac [disjI1] 

   527     THEN' resolve_tac [disjI1] 

   531     THEN' assume_tac) 1)

   528     THEN' assume_tac) 1)

   533 

   530 

   534   (FIXME: are there any advantages/disadvantages about this way?) 

   531   (FIXME: are there any advantages/disadvantages about this way?) 

   535 *}

   532 *}

   536 

   533 

   537 section {* Storing Theorems *}

   534 section {* Storing Theorems *}