ProgTutorial/General.thy
changeset 340 4ddcf4980950
parent 339 c588e8422737
child 341 62dea749d5ed
equal deleted inserted replaced
339:c588e8422737 340:4ddcf4980950
   799 
   799 
   800 text {*
   800 text {*
   801   The first argument @{ML_ind theoremK in Thm} is a kind indicator, which
   801   The first argument @{ML_ind theoremK in Thm} is a kind indicator, which
   802   classifies the theorem. For a theorem arising from a definition we should
   802   classifies the theorem. For a theorem arising from a definition we should
   803   state @{ML_ind definitionK in Thm}, instead. The second argument is the 
   803   state @{ML_ind definitionK in Thm}, instead. The second argument is the 
   804   name under which we stroe the theorem or theorems. The third contains is 
   804   name under which we store the theorem or theorems. The third can contain 
   805   a list of (theorem) attributes. Above it is empty, but if we want to store
   805   a list of (theorem) attributes. Above it is empty, but if we want to store
   806   the therem and at the same time add it to the simpset we have to declare.
   806   the theorem and at the same time add it to the simpset we have to declare:
   807 *}
   807 *}
   808 
   808 
   809 local_setup %gray {*
   809 local_setup %gray {*
   810   LocalTheory.note Thm.theoremK
   810   LocalTheory.note Thm.theoremK
   811      ((@{binding "my_thm_simp"}, [Attrib.internal (K Simplifier.simp_add)]), [my_thm]) #> snd *}
   811      ((@{binding "my_thm_simp"}, 
   812 
   812           [Attrib.internal (K Simplifier.simp_add)]), 
   813 
   813              [my_thm]) #> snd *}
   814 
   814 
   815 text {*
   815 text {*
   816   Now @{thm [source] my_thm} can be referenced with the \isacommand{thm}-command 
   816   Note that we have to use another name for the theorem, since Isabelle does
   817   on the user-level of Isabelle
   817   not allow to add another theorem under the same name.  The attribute can be
       
   818   given @{ML_ind internal in Attrib}. If we use the function @{ML
       
   819   get_thm_names_from_ss} from the previous chapter, we can check whether the
       
   820   theorem has been added.
       
   821 
       
   822   @{ML_response [display,gray]
       
   823   "let
       
   824   fun pred s = match_string \"my_thm_simp\" s
       
   825 in
       
   826   exists pred (get_thm_names_from_ss @{simpset})
       
   827 end"
       
   828   "true"}
       
   829 
       
   830   Now the theorems @{thm [source] my_thm} and @{thm [source] my_thm_simp} can 
       
   831   also be referenced  with the \isacommand{thm}-command on the user-level of 
       
   832   Isabelle
   818 
   833 
   819   \begin{isabelle}
   834   \begin{isabelle}
   820   \isacommand{thm}~@{text "my_thm"}\isanewline
   835   \isacommand{thm}~@{text "my_thm"}\isanewline
   821    @{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
   836    @{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
   822   \end{isabelle}
   837   \end{isabelle}
   823 
   838 
   824   or with the @{text "@{thm \<dots>}"}-antiquotation on the ML-level. Note that the
   839   or with the @{text "@{thm \<dots>}"}-antiquotation on the ML-level. Note that the
   825   theorem does not have any meta-variables that would be present if we proved
   840   theorem does not have any meta-variables that would be present if we proved
   826   this theorem on the user-level. As we shall see later on, we have to provide
   841   this theorem on the user-level. As we shall see later on, we have to construct
   827   this information explicitly.
   842   meta-variables explicitly.
   828 
   843 
   829   There is a multitude of functions that manage or manipulate theorems. For example 
   844   There is a multitude of functions that manage or manipulate theorems. For example 
   830   we can test theorems for (alpha) equality. Suppose you proved the following three 
   845   we can test theorems for (alpha) equality. Suppose you proved the following three 
   831   facts.
   846   facts.
   832 *}
   847 *}
   842   @{ML_response [display,gray]
   857   @{ML_response [display,gray]
   843 "(Thm.eq_thm (@{thm thm1}, @{thm thm2}),
   858 "(Thm.eq_thm (@{thm thm1}, @{thm thm2}),
   844  Thm.eq_thm (@{thm thm2}, @{thm thm3}))"
   859  Thm.eq_thm (@{thm thm2}, @{thm thm3}))"
   845 "(true, false)"}
   860 "(true, false)"}
   846 
   861 
   847   Many functions destruct a theorem into a @{ML_type cterm}. For example
   862   Many functions destruct theorems into @{ML_type cterm}s. For example
   848   @{ML_ind lhs_of in Thm} and @{ML_ind rhs_of in Thm} return the left and
   863   the functions @{ML_ind lhs_of in Thm} and @{ML_ind rhs_of in Thm} return 
   849   righ-hand side, respectively, of a meta-equality.
   864   the left and right-hand side, respectively, of a meta-equality.
   850 
   865 
   851   @{ML_response_fake [display,gray]
   866   @{ML_response_fake [display,gray]
   852   "let
   867   "let
   853   val eq = @{thm True_def}
   868   val eq = @{thm True_def}
   854 in
   869 in
   856   |> pairself (tracing o string_of_cterm @{context})
   871   |> pairself (tracing o string_of_cterm @{context})
   857 end"
   872 end"
   858   "True
   873   "True
   859 (\<lambda>x. x) = (\<lambda>x. x)"}
   874 (\<lambda>x. x) = (\<lambda>x. x)"}
   860 
   875 
   861   Other function produce immediately a term that can be pattern-matched. 
   876   Other function produce terms that can be pattern-matched. 
   862   Suppose the following theorem.
   877   Suppose the following theorem.
   863 *}
   878 *}
   864 
   879 
   865 lemma foo_test: 
   880 lemma foo_test: 
   866   shows "A \<Longrightarrow> B \<Longrightarrow> C" sorry
   881   shows "A \<Longrightarrow> B \<Longrightarrow> C" sorry
   867 
   882 
   868 text {*
   883 text {*
       
   884   We can deconstruct it into premises and conclusion. 
       
   885 
   869  @{ML_response_fake [display,gray]
   886  @{ML_response_fake [display,gray]
   870 "let
   887 "let
   871   val thm = @{thm foo_test}
   888   val thm = @{thm foo_test}
   872 in
   889 in
   873   (Thm.prems_of thm, [Thm.concl_of thm]) 
   890   (Thm.prems_of thm, [Thm.concl_of thm]) 
   879   \begin{readmore}
   896   \begin{readmore}
   880   For the functions @{text "assume"}, @{text "forall_elim"} etc 
   897   For the functions @{text "assume"}, @{text "forall_elim"} etc 
   881   see \isccite{sec:thms}. The basic functions for theorems are defined in
   898   see \isccite{sec:thms}. The basic functions for theorems are defined in
   882   @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and @{ML_file "Pure/drule.ML"}. 
   899   @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and @{ML_file "Pure/drule.ML"}. 
   883   \end{readmore}
   900   \end{readmore}
       
   901 
       
   902   TBD below.
   884 
   903 
   885   (FIXME: handy functions working on theorems, like @{ML_ind  rulify in ObjectLogic} and so on) 
   904   (FIXME: handy functions working on theorems, like @{ML_ind  rulify in ObjectLogic} and so on) 
   886 
   905 
   887   (FIXME: @{ML_ind prove in Goal})
   906   (FIXME: @{ML_ind prove in Goal})
   888 
   907