isabelle-cookbook: comparison ProgTutorial/General.thy

equal deleted inserted replaced

-:d8b6d5003823
+:0019ebf76e10
 \]
 While we obtained a theorem as result, this theorem is not
 yet stored in Isabelle's theorem database. Consequently, it cannot be
 referenced on the user level. One way to store it in the theorem database is
-by using the function @{ML_ind note in LocalTheory}.\footnote{\bf FIXME: make sure a pointer
+by using the function @{ML_ind note in Local_Theory}.\footnote{\bf FIXME: make sure a pointer
 to the section about local-setup is given earlier.}
 *}
 local_setup %gray {*
-LocalTheory.note Thm.theoremK
+Local_Theory.note ((@{binding "my_thm"}, []), [my_thm]) #> snd *}
-((@{binding "my_thm"}, []), [my_thm]) #> snd *}
+text {*
-text {*
+The fourth argument of @{ML note in Local_Theory} is the list of theorems we
-The fourth argument of @{ML note in LocalTheory} is the list of theorems we
 want to store under a name. We can store more than one under a single name.
 The first argument @{ML_ind theoremK in Thm} is
 a kind indicator, which classifies the theorem. There are several such kind
 indicators: for a theorem arising from a definition you should use @{ML_ind
-definitionK in Thm}, for an axiom @{ML_ind axiomK in Thm}, and for
+definitionK in Thm}, and for
 ``normal'' theorems the kinds @{ML_ind theoremK in Thm} or @{ML_ind lemmaK
-in Thm}.  The second argument of @{ML note in LocalTheory} is the name under
+in Thm}.  The second argument of @{ML note in Local_Theory} is the name under
 which we store the theorem or theorems. The third argument can contain a
 list of theorem attributes, which we will explain in detail in
 Section~\ref{sec:attributes}. Below we just use one such attribute for
 adding the theorem to the simpset:
 *}
 local_setup %gray {*
-LocalTheory.note Thm.theoremK
+Local_Theory.note ((@{binding "my_thm_simp"},
-((@{binding "my_thm_simp"},
 [Attrib.internal (K Simplifier.simp_add)]), [my_thm]) #> snd *}
 text {*
 Note that we have to use another name under which the theorem is stored,
-since Isabelle does not allow us to call  @{ML_ind note in LocalTheory} twice
+since Isabelle does not allow us to call  @{ML_ind note in Local_Theory} twice
 with the same name. The attribute needs to be wrapped inside the function @{ML_ind
 internal in Attrib} from the structure @{ML_struct Attrib}. If we use the function
 @{ML get_thm_names_from_ss} from
 the previous chapter, we can check whether the theorem has actually been
 added.
 \end{isabelle}
 or with the @{text "@{thm \<dots>}"}-antiquotation on the ML-level. Otherwise the
 user has no access to these theorems.
-Recall that Isabelle does not let you call @{ML note in LocalTheory} twice
+Recall that Isabelle does not let you call @{ML note in Local_Theory} twice
 with the same theorem name. In effect, once a theorem is stored under a name,
 this association is fixed. While this is a ``safety-net'' to make sure a
 theorem name refers to a particular theorem or collection of theorems, it is
 also a bit too restrictive in cases where a theorem name should refer to a
 dynamically expanding list of theorems (like a simpset). Therefore Isabelle
 ML{*structure MyThmList = Generic_Data
 (type T = thm list
 val empty = []
 val extend = I
-val merge = op @)
+val merge = merge Thm.eq_thm_prop)
-fun update thm = Context.theory_map (MyThmList.map (fn thms => thm::thms))*}
+fun update thm = Context.theory_map (MyThmList.map (Thm.add_thm thm))*}
 text {*
 The function @{ML update} allows us to update the theorem list, for example
 by adding the theorem @{thm [source] TrueI}.
 *}
 two premises of the lemma.  This can be done with the function @{ML_ind name in Rule_Cases}
 from the structure @{ML_struct Rule_Cases}.
 *}
 local_setup %gray {*
-LocalTheory.note Thm.lemmaK
+Local_Theory.note ((@{binding "foo_data'"}, []),
-((@{binding "foo_data'"}, []),
+[(Rule_Cases.name ["foo_case_one", "foo_case_two"]
-[(Rule_Cases.name ["foo_case_one", "foo_case_two"]
+@{thm foo_data})]) #> snd *}
-@{thm foo_data})]) #> snd *}
 text {*
 The data of the theorem @{thm [source] foo_data'} is then as follows:
 @{ML_response_fake [display,gray]
 section {* Contexts (TBD) *}
 section {* Local Theories (TBD) *}
+text {*
+@{ML_ind "Local_Theory.declaration"}
+*}
 (*
 setup {*
 Sign.add_consts_i [(Binding"bar", @{typ "nat"},NoSyn)]
 *}
 ML {* Pretty.mark Markup.hilite (Pretty.str "foo") |> Pretty.string_of  |> tracing *}
 ML {* (Pretty.str "bar") |> Pretty.string_of |> tracing *}
 *)
+section {* Morphisms (TBD) *}
+text {*
+Morphisms are arbitrary transformations over terms, types, theorems and bindings.
+They can be constructed using the function @{ML_ind morphism in Morphism},
+which expects a record with functions of type
+\begin{isabelle}
+\begin{tabular}{rl}
+@{text "binding:"} & @{text "binding -> binding"}\\
+@{text "typ:"}     & @{text "typ -> typ"}\\
+@{text "term:"}    & @{text "term -> term"}\\
+@{text "fact:"}    & @{text "thm list -> thm list"}
+\end{tabular}
+\end{isabelle}
+The simplest morphism is the  @{ML_ind identity in Morphism}-morphism defined as
+*}
+ML{*val identity = Morphism.morphism {binding = I, typ = I, term = I, fact = I}*}
+text {*
+Morphisms can be composed with the function @{ML_ind "$>" in Morphism}
+*}
+ML{*fun trm_phi (Free (x, T)) = Var ((x, 0), T)
+| trm_phi (Abs (x, T, t)) = Abs (x, T, trm_phi t)
+| trm_phi (t $ s) = (trm_phi t) $ (trm_phi s)
+| trm_phi t = t*}
+ML{*val phi = Morphism.term_morphism trm_phi*}
+ML{*Morphism.term phi @{term "P x y"}*}
+text {*
+@{ML_ind term_morphism in Morphism}
+@{ML_ind term in Morphism},
+@{ML_ind thm in Morphism}
+\begin{readmore}
+Morphisms are implemented in the file @{ML_file "Pure/morphism.ML"}.
+\end{readmore}
+*}
 section {* Misc (TBD) *}
 ML {*Datatype.get_info @{theory} "List.list"*}
 text {*
 @{ML_ind "Binding.str_of"} returns the string with markup;
 @{ML_ind "Binding.name_of"} returns the string without markup
+@{ML_ind "Binding.conceal"}
 *}
 section {* Concurrency (TBD) *}
 text {*

changeset 394	0019ebf76e10
parent 393	d8b6d5003823