--- a/doc-src/Locales/Locales/Examples.thy Mon Aug 27 21:04:37 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,770 +0,0 @@
-theory Examples
-imports Main
-begin
-
-pretty_setmargin %invisible 65
-
-(*
-text {* The following presentation will use notation of
- Isabelle's meta logic, hence a few sentences to explain this.
- The logical
- primitives are universal quantification (@{text "\<And>"}), entailment
- (@{text "\<Longrightarrow>"}) and equality (@{text "\<equiv>"}). Variables (not bound
- variables) are sometimes preceded by a question mark. The logic is
- typed. Type variables are denoted by~@{text "'a"},~@{text "'b"}
- etc., and~@{text "\<Rightarrow>"} is the function type. Double brackets~@{text
- "\<lbrakk>"} and~@{text "\<rbrakk>"} are used to abbreviate nested entailment.
-*}
-*)
-
-section {* Introduction *}
-
-text {*
- Locales are based on contexts. A \emph{context} can be seen as a
- formula schema
-\[
- @{text "\<And>x\<^sub>1\<dots>x\<^sub>n. \<lbrakk> A\<^sub>1; \<dots> ;A\<^sub>m \<rbrakk> \<Longrightarrow> \<dots>"}
-\]
- where the variables~@{text "x\<^sub>1"}, \ldots,~@{text "x\<^sub>n"} are called
- \emph{parameters} and the premises $@{text "A\<^sub>1"}, \ldots,~@{text
- "A\<^sub>m"}$ \emph{assumptions}. A formula~@{text "C"}
- is a \emph{theorem} in the context if it is a conclusion
-\[
- @{text "\<And>x\<^sub>1\<dots>x\<^sub>n. \<lbrakk> A\<^sub>1; \<dots> ;A\<^sub>m \<rbrakk> \<Longrightarrow> C"}.
-\]
- Isabelle/Isar's notion of context goes beyond this logical view.
- Its contexts record, in a consecutive order, proved
- conclusions along with \emph{attributes}, which can provide context
- specific configuration information for proof procedures and concrete
- syntax. From a logical perspective, locales are just contexts that
- have been made persistent. To the user, though, they provide
- powerful means for declaring and combining contexts, and for the
- reuse of theorems proved in these contexts.
- *}
-
-section {* Simple Locales *}
-
-text {*
- In its simplest form, a
- \emph{locale declaration} consists of a sequence of context elements
- declaring parameters (keyword \isakeyword{fixes}) and assumptions
- (keyword \isakeyword{assumes}). The following is the specification of
- partial orders, as locale @{text partial_order}.
- *}
-
- locale partial_order =
- fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubseteq>" 50)
- assumes refl [intro, simp]: "x \<sqsubseteq> x"
- and anti_sym [intro]: "\<lbrakk> x \<sqsubseteq> y; y \<sqsubseteq> x \<rbrakk> \<Longrightarrow> x = y"
- and trans [trans]: "\<lbrakk> x \<sqsubseteq> y; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
-
-text (in partial_order) {* The parameter of this locale is~@{text le},
- which is a binary predicate with infix syntax~@{text \<sqsubseteq>}. The
- parameter syntax is available in the subsequent
- assumptions, which are the familiar partial order axioms.
-
- Isabelle recognises unbound names as free variables. In locale
- assumptions, these are implicitly universally quantified. That is,
- @{term "\<lbrakk> x \<sqsubseteq> y; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"} in fact means
- @{term "\<And>x y z. \<lbrakk> x \<sqsubseteq> y; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"}.
-
- Two commands are provided to inspect locales:
- \isakeyword{print\_locales} lists the names of all locales of the
- current theory; \isakeyword{print\_locale}~$n$ prints the parameters
- and assumptions of locale $n$; the variation \isakeyword{print\_locale!}~$n$
- additionally outputs the conclusions that are stored in the locale.
- We may inspect the new locale
- by issuing \isakeyword{print\_locale!} @{term partial_order}. The output
- is the following list of context elements.
-\begin{small}
-\begin{alltt}
- \isakeyword{fixes} le :: "'a \(\Rightarrow\) 'a \(\Rightarrow\) bool" (\isakeyword{infixl} "\(\sqsubseteq\)" 50)
- \isakeyword{assumes} "partial_order op \(\sqsubseteq\)"
- \isakeyword{notes} assumption
- refl [intro, simp] = `?x \(\sqsubseteq\) ?x`
- \isakeyword{and}
- anti_sym [intro] = `\(\isasymlbrakk\)?x \(\sqsubseteq\) ?y; ?y \(\sqsubseteq\) ?x\(\isasymrbrakk\) \(\Longrightarrow\) ?x = ?y`
- \isakeyword{and}
- trans [trans] = `\(\isasymlbrakk\)?x \(\sqsubseteq\) ?y; ?y \(\sqsubseteq\) ?z\(\isasymrbrakk\) \(\Longrightarrow\) ?x \(\sqsubseteq\) ?z`
-\end{alltt}
-\end{small}
- The keyword \isakeyword{notes} denotes a conclusion element. There
- is one conclusion, which was added automatically. Instead, there is
- only one assumption, namely @{term "partial_order le"}. The locale
- declaration has introduced the predicate @{term
- partial_order} to the theory. This predicate is the
- \emph{locale predicate}. Its definition may be inspected by
- issuing \isakeyword{thm} @{thm [source] partial_order_def}.
- @{thm [display, indent=2] partial_order_def}
- In our example, this is a unary predicate over the parameter of the
- locale. It is equivalent to the original assumptions, which have
- been turned into conclusions and are
- available as theorems in the context of the locale. The names and
- attributes from the locale declaration are associated to these
- theorems and are effective in the context of the locale.
-
- Each conclusion has a \emph{foundational theorem} as counterpart
- in the theory. Technically, this is simply the theorem composed
- of context and conclusion. For the transitivity theorem, this is
- @{thm [source] partial_order.trans}:
- @{thm [display, indent=2] partial_order.trans}
-*}
-
-subsection {* Targets: Extending Locales *}
-
-text {*
- The specification of a locale is fixed, but its list of conclusions
- may be extended through Isar commands that take a \emph{target} argument.
- In the following, \isakeyword{definition} and
- \isakeyword{theorem} are illustrated.
- Table~\ref{tab:commands-with-target} lists Isar commands that accept
- a target. Isar provides various ways of specifying the target. A
- target for a single command may be indicated with keyword
- \isakeyword{in} in the following way:
-
-\begin{table}
-\hrule
-\vspace{2ex}
-\begin{center}
-\begin{tabular}{ll}
- \isakeyword{definition} & definition through an equation \\
- \isakeyword{inductive} & inductive definition \\
- \isakeyword{primrec} & primitive recursion \\
- \isakeyword{fun}, \isakeyword{function} & general recursion \\
- \isakeyword{abbreviation} & syntactic abbreviation \\
- \isakeyword{theorem}, etc.\ & theorem statement with proof \\
- \isakeyword{theorems}, etc.\ & redeclaration of theorems \\
- \isakeyword{text}, etc.\ & document markup
-\end{tabular}
-\end{center}
-\hrule
-\caption{Isar commands that accept a target.}
-\label{tab:commands-with-target}
-\end{table}
- *}
-
- definition (in partial_order)
- less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubset>" 50)
- where "(x \<sqsubset> y) = (x \<sqsubseteq> y \<and> x \<noteq> y)"
-
-text (in partial_order) {* The strict order @{text less} with infix
- syntax~@{text \<sqsubset>} is
- defined in terms of the locale parameter~@{text le} and the general
- equality of the object logic we work in. The definition generates a
- \emph{foundational constant}
- @{term partial_order.less} with definition @{thm [source]
- partial_order.less_def}:
- @{thm [display, indent=2] partial_order.less_def}
- At the same time, the locale is extended by syntax transformations
- hiding this construction in the context of the locale. Here, the
- abbreviation @{text less} is available for
- @{text "partial_order.less le"}, and it is printed
- and parsed as infix~@{text \<sqsubset>}. Finally, the conclusion @{thm [source]
- less_def} is added to the locale:
- @{thm [display, indent=2] less_def}
-*}
-
-text {* The treatment of theorem statements is more straightforward.
- As an example, here is the derivation of a transitivity law for the
- strict order relation. *}
-
- lemma (in partial_order) less_le_trans [trans]:
- "\<lbrakk> x \<sqsubset> y; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<sqsubset> z"
- unfolding %visible less_def by %visible (blast intro: trans)
-
-text {* In the context of the proof, conclusions of the
- locale may be used like theorems. Attributes are effective: @{text
- anti_sym} was
- declared as introduction rule, hence it is in the context's set of
- rules used by the classical reasoner by default. *}
-
-subsection {* Context Blocks *}
-
-text {* When working with locales, sequences of commands with the same
- target are frequent. A block of commands, delimited by
- \isakeyword{begin} and \isakeyword{end}, makes a theory-like style
- of working possible. All commands inside the block refer to the
- same target. A block may immediately follow a locale
- declaration, which makes that locale the target. Alternatively the
- target for a block may be given with the \isakeyword{context}
- command.
-
- This style of working is illustrated in the block below, where
- notions of infimum and supremum for partial orders are introduced,
- together with theorems about their uniqueness. *}
-
- context partial_order
- begin
-
- definition
- is_inf where "is_inf x y i =
- (i \<sqsubseteq> x \<and> i \<sqsubseteq> y \<and> (\<forall>z. z \<sqsubseteq> x \<and> z \<sqsubseteq> y \<longrightarrow> z \<sqsubseteq> i))"
-
- definition
- is_sup where "is_sup x y s =
- (x \<sqsubseteq> s \<and> y \<sqsubseteq> s \<and> (\<forall>z. x \<sqsubseteq> z \<and> y \<sqsubseteq> z \<longrightarrow> s \<sqsubseteq> z))"
-
- lemma %invisible is_infI [intro?]: "i \<sqsubseteq> x \<Longrightarrow> i \<sqsubseteq> y \<Longrightarrow>
- (\<And>z. z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> i) \<Longrightarrow> is_inf x y i"
- by (unfold is_inf_def) blast
-
- lemma %invisible is_inf_lower [elim?]:
- "is_inf x y i \<Longrightarrow> (i \<sqsubseteq> x \<Longrightarrow> i \<sqsubseteq> y \<Longrightarrow> C) \<Longrightarrow> C"
- by (unfold is_inf_def) blast
-
- lemma %invisible is_inf_greatest [elim?]:
- "is_inf x y i \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> i"
- by (unfold is_inf_def) blast
-
- theorem is_inf_uniq: "\<lbrakk>is_inf x y i; is_inf x y i'\<rbrakk> \<Longrightarrow> i = i'"
- proof -
- assume inf: "is_inf x y i"
- assume inf': "is_inf x y i'"
- show ?thesis
- proof (rule anti_sym)
- from inf' show "i \<sqsubseteq> i'"
- proof (rule is_inf_greatest)
- from inf show "i \<sqsubseteq> x" ..
- from inf show "i \<sqsubseteq> y" ..
- qed
- from inf show "i' \<sqsubseteq> i"
- proof (rule is_inf_greatest)
- from inf' show "i' \<sqsubseteq> x" ..
- from inf' show "i' \<sqsubseteq> y" ..
- qed
- qed
- qed
-
- theorem %invisible is_inf_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> is_inf x y x"
- proof -
- assume "x \<sqsubseteq> y"
- show ?thesis
- proof
- show "x \<sqsubseteq> x" ..
- show "x \<sqsubseteq> y" by fact
- fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" show "z \<sqsubseteq> x" by fact
- qed
- qed
-
- lemma %invisible is_supI [intro?]: "x \<sqsubseteq> s \<Longrightarrow> y \<sqsubseteq> s \<Longrightarrow>
- (\<And>z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> s \<sqsubseteq> z) \<Longrightarrow> is_sup x y s"
- by (unfold is_sup_def) blast
-
- lemma %invisible is_sup_least [elim?]:
- "is_sup x y s \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> s \<sqsubseteq> z"
- by (unfold is_sup_def) blast
-
- lemma %invisible is_sup_upper [elim?]:
- "is_sup x y s \<Longrightarrow> (x \<sqsubseteq> s \<Longrightarrow> y \<sqsubseteq> s \<Longrightarrow> C) \<Longrightarrow> C"
- by (unfold is_sup_def) blast
-
- theorem is_sup_uniq: "\<lbrakk>is_sup x y s; is_sup x y s'\<rbrakk> \<Longrightarrow> s = s'"
- proof -
- assume sup: "is_sup x y s"
- assume sup': "is_sup x y s'"
- show ?thesis
- proof (rule anti_sym)
- from sup show "s \<sqsubseteq> s'"
- proof (rule is_sup_least)
- from sup' show "x \<sqsubseteq> s'" ..
- from sup' show "y \<sqsubseteq> s'" ..
- qed
- from sup' show "s' \<sqsubseteq> s"
- proof (rule is_sup_least)
- from sup show "x \<sqsubseteq> s" ..
- from sup show "y \<sqsubseteq> s" ..
- qed
- qed
- qed
-
- theorem %invisible is_sup_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> is_sup x y y"
- proof -
- assume "x \<sqsubseteq> y"
- show ?thesis
- proof
- show "x \<sqsubseteq> y" by fact
- show "y \<sqsubseteq> y" ..
- fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z"
- show "y \<sqsubseteq> z" by fact
- qed
- qed
-
- end
-
-text {* The syntax of the locale commands discussed in this tutorial is
- shown in Table~\ref{tab:commands}. The grammar is complete with the
- exception of the context elements \isakeyword{constrains} and
- \isakeyword{defines}, which are provided for backward
- compatibility. See the Isabelle/Isar Reference
- Manual~\cite{IsarRef} for full documentation. *}
-
-
-section {* Import \label{sec:import} *}
-
-text {*
- Algebraic structures are commonly defined by adding operations and
- properties to existing structures. For example, partial orders
- are extended to lattices and total orders. Lattices are extended to
- distributive lattices. *}
-
-text {*
- With locales, this kind of inheritance is achieved through
- \emph{import} of locales. The import part of a locale declaration,
- if present, precedes the context elements. Here is an example,
- where partial orders are extended to lattices.
- *}
-
- locale lattice = partial_order +
- assumes ex_inf: "\<exists>inf. is_inf x y inf"
- and ex_sup: "\<exists>sup. is_sup x y sup"
- begin
-
-text {* These assumptions refer to the predicates for infimum
- and supremum defined for @{text partial_order} in the previous
- section. We now introduce the notions of meet and join. *}
-
- definition
- meet (infixl "\<sqinter>" 70) where "x \<sqinter> y = (THE inf. is_inf x y inf)"
- definition
- join (infixl "\<squnion>" 65) where "x \<squnion> y = (THE sup. is_sup x y sup)"
-
- lemma %invisible meet_equality [elim?]: "is_inf x y i \<Longrightarrow> x \<sqinter> y = i"
- proof (unfold meet_def)
- assume "is_inf x y i"
- then show "(THE i. is_inf x y i) = i"
- by (rule the_equality) (rule is_inf_uniq [OF _ `is_inf x y i`])
- qed
-
- lemma %invisible meetI [intro?]:
- "i \<sqsubseteq> x \<Longrightarrow> i \<sqsubseteq> y \<Longrightarrow> (\<And>z. z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> i) \<Longrightarrow> x \<sqinter> y = i"
- by (rule meet_equality, rule is_infI) blast+
-
- lemma %invisible is_inf_meet [intro?]: "is_inf x y (x \<sqinter> y)"
- proof (unfold meet_def)
- from ex_inf obtain i where "is_inf x y i" ..
- then show "is_inf x y (THE i. is_inf x y i)"
- by (rule theI) (rule is_inf_uniq [OF _ `is_inf x y i`])
- qed
-
- lemma %invisible meet_left [intro?]:
- "x \<sqinter> y \<sqsubseteq> x"
- by (rule is_inf_lower) (rule is_inf_meet)
-
- lemma %invisible meet_right [intro?]:
- "x \<sqinter> y \<sqsubseteq> y"
- by (rule is_inf_lower) (rule is_inf_meet)
-
- lemma %invisible meet_le [intro?]:
- "\<lbrakk> z \<sqsubseteq> x; z \<sqsubseteq> y \<rbrakk> \<Longrightarrow> z \<sqsubseteq> x \<sqinter> y"
- by (rule is_inf_greatest) (rule is_inf_meet)
-
- lemma %invisible join_equality [elim?]: "is_sup x y s \<Longrightarrow> x \<squnion> y = s"
- proof (unfold join_def)
- assume "is_sup x y s"
- then show "(THE s. is_sup x y s) = s"
- by (rule the_equality) (rule is_sup_uniq [OF _ `is_sup x y s`])
- qed
-
- lemma %invisible joinI [intro?]: "x \<sqsubseteq> s \<Longrightarrow> y \<sqsubseteq> s \<Longrightarrow>
- (\<And>z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> s \<sqsubseteq> z) \<Longrightarrow> x \<squnion> y = s"
- by (rule join_equality, rule is_supI) blast+
-
- lemma %invisible is_sup_join [intro?]: "is_sup x y (x \<squnion> y)"
- proof (unfold join_def)
- from ex_sup obtain s where "is_sup x y s" ..
- then show "is_sup x y (THE s. is_sup x y s)"
- by (rule theI) (rule is_sup_uniq [OF _ `is_sup x y s`])
- qed
-
- lemma %invisible join_left [intro?]:
- "x \<sqsubseteq> x \<squnion> y"
- by (rule is_sup_upper) (rule is_sup_join)
-
- lemma %invisible join_right [intro?]:
- "y \<sqsubseteq> x \<squnion> y"
- by (rule is_sup_upper) (rule is_sup_join)
-
- lemma %invisible join_le [intro?]:
- "\<lbrakk> x \<sqsubseteq> z; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
- by (rule is_sup_least) (rule is_sup_join)
-
- theorem %invisible meet_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
- proof (rule meetI)
- show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x \<sqinter> y"
- proof
- show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x" ..
- show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y"
- proof -
- have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" ..
- also have "\<dots> \<sqsubseteq> y" ..
- finally show ?thesis .
- qed
- qed
- show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> z"
- proof -
- have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" ..
- also have "\<dots> \<sqsubseteq> z" ..
- finally show ?thesis .
- qed
- fix w assume "w \<sqsubseteq> x \<sqinter> y" and "w \<sqsubseteq> z"
- show "w \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
- proof
- show "w \<sqsubseteq> x"
- proof -
- have "w \<sqsubseteq> x \<sqinter> y" by fact
- also have "\<dots> \<sqsubseteq> x" ..
- finally show ?thesis .
- qed
- show "w \<sqsubseteq> y \<sqinter> z"
- proof
- show "w \<sqsubseteq> y"
- proof -
- have "w \<sqsubseteq> x \<sqinter> y" by fact
- also have "\<dots> \<sqsubseteq> y" ..
- finally show ?thesis .
- qed
- show "w \<sqsubseteq> z" by fact
- qed
- qed
- qed
-
- theorem %invisible meet_commute: "x \<sqinter> y = y \<sqinter> x"
- proof (rule meetI)
- show "y \<sqinter> x \<sqsubseteq> x" ..
- show "y \<sqinter> x \<sqsubseteq> y" ..
- fix z assume "z \<sqsubseteq> y" and "z \<sqsubseteq> x"
- then show "z \<sqsubseteq> y \<sqinter> x" ..
- qed
-
- theorem %invisible meet_join_absorb: "x \<sqinter> (x \<squnion> y) = x"
- proof (rule meetI)
- show "x \<sqsubseteq> x" ..
- show "x \<sqsubseteq> x \<squnion> y" ..
- fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> x \<squnion> y"
- show "z \<sqsubseteq> x" by fact
- qed
-
- theorem %invisible join_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
- proof (rule joinI)
- show "x \<squnion> y \<sqsubseteq> x \<squnion> (y \<squnion> z)"
- proof
- show "x \<sqsubseteq> x \<squnion> (y \<squnion> z)" ..
- show "y \<sqsubseteq> x \<squnion> (y \<squnion> z)"
- proof -
- have "y \<sqsubseteq> y \<squnion> z" ..
- also have "... \<sqsubseteq> x \<squnion> (y \<squnion> z)" ..
- finally show ?thesis .
- qed
- qed
- show "z \<sqsubseteq> x \<squnion> (y \<squnion> z)"
- proof -
- have "z \<sqsubseteq> y \<squnion> z" ..
- also have "... \<sqsubseteq> x \<squnion> (y \<squnion> z)" ..
- finally show ?thesis .
- qed
- fix w assume "x \<squnion> y \<sqsubseteq> w" and "z \<sqsubseteq> w"
- show "x \<squnion> (y \<squnion> z) \<sqsubseteq> w"
- proof
- show "x \<sqsubseteq> w"
- proof -
- have "x \<sqsubseteq> x \<squnion> y" ..
- also have "\<dots> \<sqsubseteq> w" by fact
- finally show ?thesis .
- qed
- show "y \<squnion> z \<sqsubseteq> w"
- proof
- show "y \<sqsubseteq> w"
- proof -
- have "y \<sqsubseteq> x \<squnion> y" ..
- also have "... \<sqsubseteq> w" by fact
- finally show ?thesis .
- qed
- show "z \<sqsubseteq> w" by fact
- qed
- qed
- qed
-
- theorem %invisible join_commute: "x \<squnion> y = y \<squnion> x"
- proof (rule joinI)
- show "x \<sqsubseteq> y \<squnion> x" ..
- show "y \<sqsubseteq> y \<squnion> x" ..
- fix z assume "y \<sqsubseteq> z" and "x \<sqsubseteq> z"
- then show "y \<squnion> x \<sqsubseteq> z" ..
- qed
-
- theorem %invisible join_meet_absorb: "x \<squnion> (x \<sqinter> y) = x"
- proof (rule joinI)
- show "x \<sqsubseteq> x" ..
- show "x \<sqinter> y \<sqsubseteq> x" ..
- fix z assume "x \<sqsubseteq> z" and "x \<sqinter> y \<sqsubseteq> z"
- show "x \<sqsubseteq> z" by fact
- qed
-
- theorem %invisible meet_idem: "x \<sqinter> x = x"
- proof -
- have "x \<sqinter> (x \<squnion> (x \<sqinter> x)) = x" by (rule meet_join_absorb)
- also have "x \<squnion> (x \<sqinter> x) = x" by (rule join_meet_absorb)
- finally show ?thesis .
- qed
-
- theorem %invisible meet_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
- proof (rule meetI)
- assume "x \<sqsubseteq> y"
- show "x \<sqsubseteq> x" ..
- show "x \<sqsubseteq> y" by fact
- fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y"
- show "z \<sqsubseteq> x" by fact
- qed
-
- theorem %invisible meet_related2 [elim?]: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
- by (drule meet_related) (simp add: meet_commute)
-
- theorem %invisible join_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
- proof (rule joinI)
- assume "x \<sqsubseteq> y"
- show "y \<sqsubseteq> y" ..
- show "x \<sqsubseteq> y" by fact
- fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z"
- show "y \<sqsubseteq> z" by fact
- qed
-
- theorem %invisible join_related2 [elim?]: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
- by (drule join_related) (simp add: join_commute)
-
- theorem %invisible meet_connection: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)"
- proof
- assume "x \<sqsubseteq> y"
- then have "is_inf x y x" ..
- then show "x \<sqinter> y = x" ..
- next
- have "x \<sqinter> y \<sqsubseteq> y" ..
- also assume "x \<sqinter> y = x"
- finally show "x \<sqsubseteq> y" .
- qed
-
- theorem %invisible join_connection: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"
- proof
- assume "x \<sqsubseteq> y"
- then have "is_sup x y y" ..
- then show "x \<squnion> y = y" ..
- next
- have "x \<sqsubseteq> x \<squnion> y" ..
- also assume "x \<squnion> y = y"
- finally show "x \<sqsubseteq> y" .
- qed
-
- theorem %invisible meet_connection2: "(x \<sqsubseteq> y) = (y \<sqinter> x = x)"
- using meet_commute meet_connection by simp
-
- theorem %invisible join_connection2: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"
- using join_commute join_connection by simp
-
- text %invisible {* Naming according to Jacobson I, p.\ 459. *}
- lemmas %invisible L1 = join_commute meet_commute
- lemmas %invisible L2 = join_assoc meet_assoc
- (* lemmas L3 = join_idem meet_idem *)
- lemmas %invisible L4 = join_meet_absorb meet_join_absorb
-
- end
-
-text {* Locales for total orders and distributive lattices follow to
- establish a sufficiently rich landscape of locales for
- further examples in this tutorial. Each comes with an example
- theorem. *}
-
- locale total_order = partial_order +
- assumes total: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
-
- lemma (in total_order) less_total: "x \<sqsubset> y \<or> x = y \<or> y \<sqsubset> x"
- using total
- by (unfold less_def) blast
-
- locale distrib_lattice = lattice +
- assumes meet_distr: "x \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> z"
-
- lemma (in distrib_lattice) join_distr:
- "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" (* txt {* Jacobson I, p.\ 462 *} *)
- proof -
- have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by (simp add: L4)
- also have "... = x \<squnion> ((x \<sqinter> z) \<squnion> (y \<sqinter> z))" by (simp add: L2)
- also have "... = x \<squnion> ((x \<squnion> y) \<sqinter> z)" by (simp add: L1 meet_distr)
- also have "... = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)" by (simp add: L1 L4)
- also have "... = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by (simp add: meet_distr)
- finally show ?thesis .
- qed
-
-text {*
- The locale hierarchy obtained through these declarations is shown in
- Figure~\ref{fig:lattices}(a).
-
-\begin{figure}
-\hrule \vspace{2ex}
-\begin{center}
-\subfigure[Declared hierarchy]{
-\begin{tikzpicture}
- \node (po) at (0,0) {@{text partial_order}};
- \node (lat) at (-1.5,-1) {@{text lattice}};
- \node (dlat) at (-1.5,-2) {@{text distrib_lattice}};
- \node (to) at (1.5,-1) {@{text total_order}};
- \draw (po) -- (lat);
- \draw (lat) -- (dlat);
- \draw (po) -- (to);
-% \draw[->, dashed] (lat) -- (to);
-\end{tikzpicture}
-} \\
-\subfigure[Total orders are lattices]{
-\begin{tikzpicture}
- \node (po) at (0,0) {@{text partial_order}};
- \node (lat) at (0,-1) {@{text lattice}};
- \node (dlat) at (-1.5,-2) {@{text distrib_lattice}};
- \node (to) at (1.5,-2) {@{text total_order}};
- \draw (po) -- (lat);
- \draw (lat) -- (dlat);
- \draw (lat) -- (to);
-% \draw[->, dashed] (dlat) -- (to);
-\end{tikzpicture}
-} \quad
-\subfigure[Total orders are distributive lattices]{
-\begin{tikzpicture}
- \node (po) at (0,0) {@{text partial_order}};
- \node (lat) at (0,-1) {@{text lattice}};
- \node (dlat) at (0,-2) {@{text distrib_lattice}};
- \node (to) at (0,-3) {@{text total_order}};
- \draw (po) -- (lat);
- \draw (lat) -- (dlat);
- \draw (dlat) -- (to);
-\end{tikzpicture}
-}
-\end{center}
-\hrule
-\caption{Hierarchy of Lattice Locales.}
-\label{fig:lattices}
-\end{figure}
- *}
-
-section {* Changing the Locale Hierarchy
- \label{sec:changing-the-hierarchy} *}
-
-text {*
- Locales enable to prove theorems abstractly, relative to
- sets of assumptions. These theorems can then be used in other
- contexts where the assumptions themselves, or
- instances of the assumptions, are theorems. This form of theorem
- reuse is called \emph{interpretation}. Locales generalise
- interpretation from theorems to conclusions, enabling the reuse of
- definitions and other constructs that are not part of the
- specifications of the locales.
-
- The first form of interpretation we will consider in this tutorial
- is provided by the \isakeyword{sublocale} command. It enables to
- modify the import hierarchy to reflect the \emph{logical} relation
- between locales.
-
- Consider the locale hierarchy from Figure~\ref{fig:lattices}(a).
- Total orders are lattices, although this is not reflected here, and
- definitions, theorems and other conclusions
- from @{term lattice} are not available in @{term total_order}. To
- obtain the situation in Figure~\ref{fig:lattices}(b), it is
- sufficient to add the conclusions of the latter locale to the former.
- The \isakeyword{sublocale} command does exactly this.
- The declaration \isakeyword{sublocale} $l_1
- \subseteq l_2$ causes locale $l_2$ to be \emph{interpreted} in the
- context of $l_1$. This means that all conclusions of $l_2$ are made
- available in $l_1$.
-
- Of course, the change of hierarchy must be supported by a theorem
- that reflects, in our example, that total orders are indeed
- lattices. Therefore the \isakeyword{sublocale} command generates a
- goal, which must be discharged by the user. This is illustrated in
- the following paragraphs. First the sublocale relation is stated.
-*}
-
- sublocale %visible total_order \<subseteq> lattice
-
-txt {* \normalsize
- This enters the context of locale @{text total_order}, in
- which the goal @{subgoals [display]} must be shown.
- Now the
- locale predicate needs to be unfolded --- for example, using its
- definition or by introduction rules
- provided by the locale package. For automation, the locale package
- provides the methods @{text intro_locales} and @{text
- unfold_locales}. They are aware of the
- current context and dependencies between locales and automatically
- discharge goals implied by these. While @{text unfold_locales}
- always unfolds locale predicates to assumptions, @{text
- intro_locales} only unfolds definitions along the locale
- hierarchy, leaving a goal consisting of predicates defined by the
- locale package. Occasionally the latter is of advantage since the goal
- is smaller.
-
- For the current goal, we would like to get hold of
- the assumptions of @{text lattice}, which need to be shown, hence
- @{text unfold_locales} is appropriate. *}
-
- proof unfold_locales
-
-txt {* \normalsize
- Since the fact that both lattices and total orders are partial
- orders is already reflected in the locale hierarchy, the assumptions
- of @{text partial_order} are discharged automatically, and only the
- assumptions introduced in @{text lattice} remain as subgoals
- @{subgoals [display]}
- The proof for the first subgoal is obtained by constructing an
- infimum, whose existence is implied by totality. *}
-
- fix x y
- from total have "is_inf x y (if x \<sqsubseteq> y then x else y)"
- by (auto simp: is_inf_def)
- then show "\<exists>inf. is_inf x y inf" ..
-txt {* \normalsize
- The proof for the second subgoal is analogous and not
- reproduced here. *}
- next %invisible
- fix x y
- from total have "is_sup x y (if x \<sqsubseteq> y then y else x)"
- by (auto simp: is_sup_def)
- then show "\<exists>sup. is_sup x y sup" .. qed %visible
-
-text {* Similarly, we may establish that total orders are distributive
- lattices with a second \isakeyword{sublocale} statement. *}
-
- sublocale total_order \<subseteq> distrib_lattice
- proof unfold_locales
- fix %"proof" x y z
- show "x \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> z" (is "?l = ?r")
- txt {* Jacobson I, p.\ 462 *}
- proof -
- { assume c: "y \<sqsubseteq> x" "z \<sqsubseteq> x"
- from c have "?l = y \<squnion> z"
- by (metis c join_connection2 join_related2 meet_related2 total)
- also from c have "... = ?r" by (metis meet_related2)
- finally have "?l = ?r" . }
- moreover
- { assume c: "x \<sqsubseteq> y \<or> x \<sqsubseteq> z"
- from c have "?l = x"
- by (metis join_connection2 join_related2 meet_connection total trans)
- also from c have "... = ?r"
- by (metis join_commute join_related2 meet_connection meet_related2 total)
- finally have "?l = ?r" . }
- moreover note total
- ultimately show ?thesis by blast
- qed
- qed
-
-text {* The locale hierarchy is now as shown in
- Figure~\ref{fig:lattices}(c). *}
-
-text {*
- Locale interpretation is \emph{dynamic}. The statement
- \isakeyword{sublocale} $l_1 \subseteq l_2$ will not just add the
- current conclusions of $l_2$ to $l_1$. Rather the dependency is
- stored, and conclusions that will be
- added to $l_2$ in future are automatically propagated to $l_1$.
- The sublocale relation is transitive --- that is, propagation takes
- effect along chains of sublocales. Even cycles in the sublocale relation are
- supported, as long as these cycles do not lead to infinite chains.
- Details are discussed in the technical report \cite{Ballarin2006a}.
- See also Section~\ref{sec:infinite-chains} of this tutorial. *}
-
-end