isabelle-cookbook: comparison ProgTutorial/General.thy

equal deleted inserted replaced

-:2f2018927f2a
+:9e374cd891e1
 or with the @{text "@{thm \<dots>}"}-antiquotation on the ML-level. As can be seen
 the theorem does not have any meta-variables that would be present if we proved
 this theorem on the user-level. We will see later on that usually we have to
 construct meta-variables in theorems explicitly.
+\footnote{\bf FIXME say something about @{ML_ind add_thms_dynamic in PureThy}}
 *}
 text {*
 There is a multitude of functions that manage or manipulate theorems. For example
 we can test theorems for alpha equality. Suppose you proved the following three
 In this code the function @{ML atomize in ObjectLogic} produces
 a meta-equation between the given theorem and the theorem transformed
 into the object logic. The result is the theorem with object logic
 connectives. However, in order to completely transform a theorem
-such as @{thm [source] list.induct}
+such as @{thm [source] list.induct}, which is of the form
 @{thm [display] list.induct}
-we have to first abstract over the variables @{text "?P"} and
+we have to first abstract over the meta variables @{text "?P"} and
 @{text "?list"}. For this we can use the function
 @{ML_ind forall_intr_vars in Drule}.
 *}
 ML{*fun atomize_thm thm =
 in
 MetaSimplifier.rewrite_rule [thm''] thm'
 end*}
 text {*
-For @{thm [source] list.induct} it produces:
+For the theorem @{thm [source] list.induct}, this function produces:
 @{ML_response_fake [display, gray]
 "atomize_thm @{thm list.induct}"
 "\<forall>P list. P [] \<longrightarrow> (\<forall>a list. P list \<longrightarrow> P (a # list)) \<longrightarrow> P list"}
 Theorems can also be produced from terms by giving an explicit proof.
 One way to achive this is by using the function @{ML_ind prove in Goal}.
-For example
+For example below we prove the term @{term "P \<Longrightarrow> P"}.
 @{ML_response_fake [display,gray]
 "let
 val trm = @{term \"P \<Longrightarrow> P::bool\"}
 val tac = K (atac 1)
 end"
 "?P \<Longrightarrow> ?P"}
 This function takes as second argument a list of strings. This list specifies
 which variables should be turned into meta-variables once the term is proved.
-The proof is given in form of a tactic. We explain tactics in
+The proof is given in form of a tactic as last argument. We explain tactics in
-Chapter~\ref{chp:tactical}.
+Chapter~\ref{chp:tactical}. In the code above the tactic proved the theorem
+by assumption.
 Theorems also contain auxiliary data, such their names and kind, but also
 names for cases etc. This data is stored in a string-string list and can
 be retrieved with the function @{ML_ind get_tags in Thm}. Assume the
 following lemma.
 @{ML_response_fake [display,gray]
 "Thm.get_tags @{thm foo_data}"
 "[(\"name\", \"General.foo_data\"), (\"kind\", \"lemma\")]"}
-We can extend the data associated with this lemma by attaching case names.
+When we store lemmas in the theorem database, we can explicitly extend the data
+associated with this lemma by attaching case names.
 *}
 local_setup %gray {*
 LocalTheory.note Thm.lemmaK
 ((@{binding "foo_data'"}, []),
 [(RuleCases.name ["foo_case1", "foo_case2"]
 @{thm foo_data})]) #> snd *}
 text {*
-The date of the theorem @{thm [source] foo_data'} is as follows:
+The data of the theorem @{thm [source] foo_data'} is then as follows:
 @{ML_response_fake [display,gray]
 "Thm.get_tags @{thm foo_data'}"
 "[(\"name\", \"General.foo_data'\"), (\"kind\", \"lemma\"),
 (\"case_names\", \"foo_case1;foo_case2\")]"}
+You notice the difference when using the proof methods @{ML_text cases}
+or @{ML_text induct}. In the proof below
 *}
 lemma
 "Q \<Longrightarrow> Q \<Longrightarrow> Q"
-proof (induct rule: foo_data')
+proof (cases rule: foo_data')
+print_cases
 (*<*)oops(*>*)
 text {*
+we can proceed by analysing the cases @{ML_text "foo_case1"} and
+@{ML_text "foo_case2"}. While if the theorem has no names, then
+the cases have standard names @{ML_text 1}, @{ML_text 2} and so
+on. This can be seen in the proof below.
+*}
+lemma
+"Q \<Longrightarrow> Q \<Longrightarrow> Q"
+proof (cases rule: foo_data)
+print_cases
+(*<*)oops(*>*)
+text {*
 TBD below
+One great feature of Isabelle is its document preparation system where
+proved theorems can be quoted in the text directly from the formalisation.
 (FIXME: example for how to add theorem styles)
 *}
 ML {*
 ML {*
 strip_assums_all ([], @{term "\<And>x y. A x y"})
 *}
+(*
 setup %gray {*
 TermStyle.add_style "no_all_prem1" (style_parm_premise 1) #>
 TermStyle.add_style "no_all_prem2" (style_parm_premise 2)
 *}
+*)
 lemma
 shows "A \<Longrightarrow> B"
 and   "C \<Longrightarrow> D"
 oops
 *}
 section {* Contexts (TBD) *}
 section {* Local Theories (TBD) *}
-section {* Storing Theorems\label{sec:storing} (TBD) *}
-text {* @{ML_ind  add_thms_dynamic in PureThy} *}
-local_setup %gray {*
-LocalTheory.note Thm.theoremK
-((@{binding "allI_alt"}, []), [@{thm allI}]) #> snd *}
 (*
 setup {*
 Sign.add_consts_i [(Binding"bar", @{typ "nat"},NoSyn)]
 section {* Managing Name Spaces (TBD) *}
+section {* Summary *}
+text {*
+\begin{conventions}
+\begin{itemize}
+\item Start with a proper context and then pass it around
+through all your functions.
+\end{itemize}
+\end{conventions}
+*}
 end

changeset 349	9e374cd891e1
parent 348	2f2018927f2a
child 350	364fffa80794