isabelle-cookbook: comparison CookBook/FirstSteps.thy

equal deleted inserted replaced

-:5ae6a1bb91c9
+:2356e5c70d98
 function is called. Operationally speaking,  @{text "@{theory}"} is
 \emph{not} replaced with code that will look up the current theory in
 some data structure and return it. Instead, it is literally
 replaced with the value representing the theory name.
-In a similar way you can use antiquotations to refer to theorems:
+In a similar way you can use antiquotations to refer to theorems or simpsets:
 *}
 ML {* @{thm allI} *}
+ML {* @{simpset} *}
 text {*
 In the course of this introduction, we will learn more about
 these antiquotations: they greatly simplify Isabelle programming since one
 can directly access all kinds of logical elements from ML.
 assumes assm\<^isub>1: "\<And>(x::nat). P x \<Longrightarrow> Q x"
 and     assm\<^isub>2: "P t"
 shows "Q t" (*<*)oops(*>*)
 text {*
-on the ML level:\footnote{Note that @{text "|>"} is just reverse
+on the ML level:\footnote{Note that @{text "|>"} is reverse
 application. This combinator, and several variants are defined in
 @{ML_file "Pure/General/basics.ML"}.}
 *}
 |> implies_intr assm1
 end
 *}
 text {*
+This code-snippet constructs the following proof:
+\[
+\infer[(@{text "\<Longrightarrow>"}$-$intro)]{\vdash @{prop "(\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> P t \<Longrightarrow> Q t"}}
+{\infer[(@{text "\<Longrightarrow>"}$-$intro)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "P t \<Longrightarrow> Q t"}}
+{\infer[(@{text "\<Longrightarrow>"}$-$elim)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"}, @{prop "P t"} \vdash @{prop "Q t"}}
+{\infer[(@{text "\<And>"}$-$elim)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "P t \<Longrightarrow> Q t"}}
+{\infer[(assume)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "\<And>x. P x \<Longrightarrow> Q x"}}{}}
+&
+\infer[(assume)]{@{prop "P t"} \vdash @{prop "P t"}}{}
+}
+}
+}
+\]
 \begin{readmore}
 For how the functions @{text "assume"}, @{text "forall_elim"} etc work
 see \isccite{sec:thms}. The basic functions for theorems are defined in
 @{ML_file "Pure/thm.ML"}.
 Since the goal @{term C} can potentially be an implication, there is a
 @{text "#"} wrapped around it, which prevents that premises are
 misinterpreted as open subgoals. The protection @{text "# :: prop \<Rightarrow>
 prop"} is just the identity function and used as a syntactic marker.
+(FIXME: maybe show how this is printed on the screen)
 \begin{readmore}
 For more on goals see \isccite{sec:tactical-goals}.
 \end{readmore}
 Tactics are functions that map a goal state to a (lazy)
 apply assumption
 done
 text {*
+To start the proof, the function  @{ML "Goal.prove"}~@{text "ctxt xs As C tac"} sets
-To start the proof, the function  @{ML "Goal.prove"}~@{text "ctxt params assms goal tac"}
+up a goal state for proving the goal @{text C} under the assumptions @{text As}
-sets up a goal state for proving @{text goal} under the assumptions @{text assms} with
+(empty in the proof at hand)
-the variables @{text params} that will be generalised once the
+with the variables @{text xs} that will be generalised once the
-goal is proved; @{text "tac"} is a function that returns a tactic having some funny
+goal is proved. The @{text "tac"} is the tactic which proves the goal and which
-input parameters (FIXME by possibly having an explanation in the implementation-manual).
+can make use of the local assumptions.
 *}
 ML {*
 THEN resolve_tac [disjI1] 1
 THEN assume_tac 1)
 end
 *}
+text {*
+\begin{readmore}
+To learn more about the function @{ML Goal.prove} see \isccite{sec:results}.
+\end{readmore}
+*}
 text {* An alternative way to transcribe this proof is as follows *}
 ML {*
 let
 val ctxt = @{context}
 THEN' resolve_tac [disjI1]
 THEN' assume_tac) 1)
 end
 *}
+text {* (FIXME: are there any advantages/disadvantages about this way?) *}
 section {* Storing Theorems *}
 section {* Theorem Attributes *}
-text {* Was changing theorems. *}
 end

changeset 21	2356e5c70d98
parent 20	5ae6a1bb91c9
child 25	e2f9f94b26d4