isabelle-cookbook: comparison ProgTutorial/General.thy

equal deleted inserted replaced

-:0fea8b7a14a1
+:01e71cddf6a3
 ["theory General", "imports Base FirstSteps", "begin"]
 *}
 (*>*)
-chapter {* Isabelle in More Detail \mbox{or, the Good, the Bad and the Ugly} *}
+chapter {* Isabelle in More Detail *}
 text {*
 Isabelle is build around a few central ideas. One central idea is the
 LCF-approach to theorem proving where there is a small trusted core and
 everything else is build on top of this trusted core. The fundamental data
 "let
 val natT = @{typ \"nat\"}
 val zero = @{term \"0::nat\"}
 in
 cterm_of @{theory}
-(Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero)
+(Const (@{const_name plus}, [natT, natT] ---> natT) $ zero $ zero)
 end" "0 + 0"}
 In Isabelle not just terms need to be certified, but also types. For example,
 you obtain the certified type for the Isabelle type @{typ "nat \<Rightarrow> bool"} on
 the ML-level as follows:
 text {*
 If we print out the value of @{ML my_thm} then we see only the
 final statement of the theorem.
 @{ML_response_fake [display, gray]
-"string_of_thm @{context} my_thm |> tracing"
+"string_of_thm @{context} my_thm
+|> tracing"
 "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
 However, internally the code-snippet constructs the following
 proof.
 ((@{binding "my_thm"}, []), [my_thm]) #> snd *}
 text {*
 The first argument @{ML_ind theoremK in Thm} is a kind indicator, which
 classifies the theorem. For a theorem arising from a definition we should
-state @{ML_ind definitionK in Thm}, instead. The second argument is the
+use @{ML_ind definitionK in Thm}, for an axiom @{ML_ind axiomK in Thm}, for
-name under which we store the theorem or theorems. The third can contain
+``normal'' theorems the kinds @{ML_ind theoremK in Thm} or @{ML_ind lemmaK
-a list of (theorem) attributes. Above it is empty, but if we want to store
+in Thm}.  The second argument is the name under which we store the theorem
-the theorem and at the same time add it to the simpset we have to declare:
+or theorems. The third can contain a list of (theorem) attributes. We will
+explain them in detail in Section~\ref{sec:attributes}. Below we
+use such an attribute in order add the theorem to the simpset.
+have to declare:
 *}
 local_setup %gray {*
 LocalTheory.note Thm.theoremK
 ((@{binding "my_thm_simp"},
-[Attrib.internal (K Simplifier.simp_add)]),
+[Attrib.internal (K Simplifier.simp_add)]), [my_thm]) #> snd *}
-[my_thm]) #> snd *}
 text {*
 Note that we have to use another name for the theorem, since Isabelle does
-not allow to add another theorem under the same name.  The attribute can be
+not allow to store another theorem under the same name. The attribute needs to
-given @{ML_ind internal in Attrib}. If we use the function @{ML
+be wrapped inside the function @{ML_ind internal in Attrib}. If we use the
-get_thm_names_from_ss} from the previous chapter, we can check whether the
+function @{ML get_thm_names_from_ss} from the previous chapter, we can check
-theorem has been added.
+whether the theorem has actually been added.
 @{ML_response [display,gray]
 "let
 fun pred s = match_string \"my_thm_simp\" s
 in
 exists pred (get_thm_names_from_ss @{simpset})
 end"
 "true"}
-Now the theorems @{thm [source] my_thm} and @{thm [source] my_thm_simp} can
+The main point of storing the theorems @{thm [source] my_thm} and @{thm
-also be referenced  with the \isacommand{thm}-command on the user-level of
+[source] my_thm_simp} is that they can now also be referenced with the
-Isabelle
+\isacommand{thm}-command on the user-level of Isabelle
 \begin{isabelle}
 \isacommand{thm}~@{text "my_thm"}\isanewline
 @{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
 \end{isabelle}
-or with the @{text "@{thm \<dots>}"}-antiquotation on the ML-level. Note that the
+or with the @{text "@{thm \<dots>}"}-antiquotation on the ML-level. As can be seen
-theorem does not have any meta-variables that would be present if we proved
+the theorem does not have any meta-variables that would be present if we proved
-this theorem on the user-level. As we shall see later on, we have to construct
+this theorem on the user-level. We will see later on, we have to construct
-meta-variables explicitly.
+meta-variables in a theorem explicitly.
+*}
+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
 facts.
 *}
 For the functions @{text "assume"}, @{text "forall_elim"} etc
 see \isccite{sec:thms}. The basic functions for theorems are defined in
 @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and @{ML_file "Pure/drule.ML"}.
 \end{readmore}
+The simplifier can be used to unfold definition in theorms. To show
+this we build the theorem @{term "True \<equiv> True"} (Line 1) and then
+unfold the constant according to its definition (Line 2).
+@{ML_response_fake [display,gray,linenos]
+"Thm.reflexive @{cterm \"True\"}
+|> Simplifier.rewrite_rule [@{thm True_def}]
+|> string_of_thm @{context}
+|> tracing"
+"(\<lambda>x. x) = (\<lambda>x. x) \<equiv> (\<lambda>x. x) = (\<lambda>x. x)"}
 Often it is necessary to transform theorems to and from the object
 logic.  For example, the function @{ML_ind rulify in ObjectLogic}
 replaces all @{text "\<longrightarrow>"} and @{text "\<forall>"} into the equivalents of the
 meta logic. For example
 end"
 "?A \<longrightarrow> ?B \<longrightarrow> ?C"}
 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 function @{ML_ind rewrite_rule in MetaSimplifier}
+into the object logic. The result is the theorem with object logic
-unfolds this meta-equation in the given theorem. The result is
+connectives. However, in order to completely transform a theorem
-the theorem with object logic connectives.
+such as @{thm [source] list.induct}
-x
+@{thm [display] list.induct}
+we have to first abstract over the 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 =
+let
+val thm' = forall_intr_vars thm
+val thm'' = ObjectLogic.atomize (cprop_of thm')
+in
+MetaSimplifier.rewrite_rule [thm''] thm'
+end*}
+text {*
+For @{thm [source] list.induct} it 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
 @{ML_response_fake [display,gray]

changeset 347	01e71cddf6a3
parent 346	0fea8b7a14a1
child 348	2f2018927f2a