src/Doc/Locales/Examples.thy
author wenzelm
Sat, 05 Apr 2014 15:03:40 +0200
changeset 56421 1ffd7eaa778b
parent 51799 8fcf6e32544e
child 58620 7435b6a3f72e
permissions -rw-r--r--
updated to jedit_build-20140405: Code2HTML.jar, CommonControls.jar, Console.jar, kappalayout.jar, Navigator.jar, SideKick.jar, doc with jEdit manuals (ant dist-manuals);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     1
theory Examples
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
     2
imports Main
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     3
begin
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     4
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     5
(*
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     6
text {* The following presentation will use notation of
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     7
  Isabelle's meta logic, hence a few sentences to explain this.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     8
  The logical
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     9
  primitives are universal quantification (@{text "\<And>"}), entailment
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    10
  (@{text "\<Longrightarrow>"}) and equality (@{text "\<equiv>"}).  Variables (not bound
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    11
  variables) are sometimes preceded by a question mark.  The logic is
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    12
  typed.  Type variables are denoted by~@{text "'a"},~@{text "'b"}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    13
  etc., and~@{text "\<Rightarrow>"} is the function type.  Double brackets~@{text
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    14
  "\<lbrakk>"} and~@{text "\<rbrakk>"} are used to abbreviate nested entailment.
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    15
*}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    16
*)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    17
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    18
section {* Introduction *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    19
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    20
text {*
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    21
  Locales are based on contexts.  A \emph{context} can be seen as a
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    22
  formula schema
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    23
\[
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    24
  @{text "\<And>x\<^sub>1\<dots>x\<^sub>n. \<lbrakk> A\<^sub>1; \<dots> ;A\<^sub>m \<rbrakk> \<Longrightarrow> \<dots>"}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    25
\]
33838
a3166a169793 Publication details and minor correction of the text.
ballarin
parents: 32984
diff changeset
    26
  where the variables~@{text "x\<^sub>1"}, \ldots,~@{text "x\<^sub>n"} are called
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    27
  \emph{parameters} and the premises $@{text "A\<^sub>1"}, \ldots,~@{text
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    28
  "A\<^sub>m"}$ \emph{assumptions}.  A formula~@{text "C"}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    29
  is a \emph{theorem} in the context if it is a conclusion
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    30
\[
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    31
  @{text "\<And>x\<^sub>1\<dots>x\<^sub>n. \<lbrakk> A\<^sub>1; \<dots> ;A\<^sub>m \<rbrakk> \<Longrightarrow> C"}.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    32
\]
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    33
  Isabelle/Isar's notion of context goes beyond this logical view.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    34
  Its contexts record, in a consecutive order, proved
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    35
  conclusions along with \emph{attributes}, which can provide context
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    36
  specific configuration information for proof procedures and concrete
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    37
  syntax.  From a logical perspective, locales are just contexts that
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    38
  have been made persistent.  To the user, though, they provide
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    39
  powerful means for declaring and combining contexts, and for the
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    40
  reuse of theorems proved in these contexts.
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    41
  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    42
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    43
section {* Simple Locales *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    44
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    45
text {*
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    46
  In its simplest form, a
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    47
  \emph{locale declaration} consists of a sequence of context elements
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    48
  declaring parameters (keyword \isakeyword{fixes}) and assumptions
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    49
  (keyword \isakeyword{assumes}).  The following is the specification of
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    50
  partial orders, as locale @{text partial_order}.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    51
  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    52
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    53
  locale partial_order =
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    54
    fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubseteq>" 50)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    55
    assumes refl [intro, simp]: "x \<sqsubseteq> x"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    56
      and anti_sym [intro]: "\<lbrakk> x \<sqsubseteq> y; y \<sqsubseteq> x \<rbrakk> \<Longrightarrow> x = y"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    57
      and trans [trans]: "\<lbrakk> x \<sqsubseteq> y; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    58
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    59
text (in partial_order) {* The parameter of this locale is~@{text le},
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    60
  which is a binary predicate with infix syntax~@{text \<sqsubseteq>}.  The
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    61
  parameter syntax is available in the subsequent
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    62
  assumptions, which are the familiar partial order axioms.
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    63
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    64
  Isabelle recognises unbound names as free variables.  In locale
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    65
  assumptions, these are implicitly universally quantified.  That is,
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    66
  @{term "\<lbrakk> x \<sqsubseteq> y; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"} in fact means
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    67
  @{term "\<And>x y z. \<lbrakk> x \<sqsubseteq> y; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"}.
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    68
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    69
  Two commands are provided to inspect locales:
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    70
  \isakeyword{print\_locales} lists the names of all locales of the
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    71
  current theory; \isakeyword{print\_locale}~$n$ prints the parameters
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    72
  and assumptions of locale $n$; the variation \isakeyword{print\_locale!}~$n$
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    73
  additionally outputs the conclusions that are stored in the locale.
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    74
  We may inspect the new locale
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    75
  by issuing \isakeyword{print\_locale!} @{term partial_order}.  The output
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    76
  is the following list of context elements.
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    77
\begin{small}
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    78
\begin{alltt}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    79
  \isakeyword{fixes} le :: "'a \(\Rightarrow\) 'a \(\Rightarrow\)  bool" (\isakeyword{infixl} "\(\sqsubseteq\)" 50)
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    80
  \isakeyword{assumes} "partial_order op \(\sqsubseteq\)"
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    81
  \isakeyword{notes} assumption
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    82
    refl [intro, simp] = `?x \(\sqsubseteq\) ?x`
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    83
    \isakeyword{and}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    84
    anti_sym [intro] = `\(\isasymlbrakk\)?x \(\sqsubseteq\) ?y; ?y \(\sqsubseteq\) ?x\(\isasymrbrakk\) \(\Longrightarrow\) ?x = ?y`
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    85
    \isakeyword{and}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    86
    trans [trans] = `\(\isasymlbrakk\)?x \(\sqsubseteq\) ?y; ?y \(\sqsubseteq\) ?z\(\isasymrbrakk\) \(\Longrightarrow\) ?x \(\sqsubseteq\) ?z`
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    87
\end{alltt}
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    88
\end{small}
51799
8fcf6e32544e Clarified confusing sentence in locales tutorial.
ballarin
parents: 48985
diff changeset
    89
8fcf6e32544e Clarified confusing sentence in locales tutorial.
ballarin
parents: 48985
diff changeset
    90
  This differs from the declaration.  The assumptions have turned into
8fcf6e32544e Clarified confusing sentence in locales tutorial.
ballarin
parents: 48985
diff changeset
    91
  conclusions, denoted by the keyword \isakeyword{notes}.  Also,
8fcf6e32544e Clarified confusing sentence in locales tutorial.
ballarin
parents: 48985
diff changeset
    92
  there is only one assumption, namely @{term "partial_order le"}.
8fcf6e32544e Clarified confusing sentence in locales tutorial.
ballarin
parents: 48985
diff changeset
    93
  The locale declaration has introduced the predicate @{term
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    94
  partial_order} to the theory.  This predicate is the
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    95
  \emph{locale predicate}.  Its definition may be inspected by
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    96
  issuing \isakeyword{thm} @{thm [source] partial_order_def}.
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    97
  @{thm [display, indent=2] partial_order_def}
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    98
  In our example, this is a unary predicate over the parameter of the
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    99
  locale.  It is equivalent to the original assumptions, which have
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   100
  been turned into conclusions and are
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   101
  available as theorems in the context of the locale.  The names and
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   102
  attributes from the locale declaration are associated to these
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   103
  theorems and are effective in the context of the locale.
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   104
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   105
  Each conclusion has a \emph{foundational theorem} as counterpart
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   106
  in the theory.  Technically, this is simply the theorem composed
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   107
  of context and conclusion.  For the transitivity theorem, this is
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   108
  @{thm [source] partial_order.trans}:
37206
7f2a6f3143ad Typo in locales tutorial.
ballarin
parents: 37094
diff changeset
   109
  @{thm [display, indent=2] partial_order.trans}
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   110
*}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   111
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   112
subsection {* Targets: Extending Locales *}
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   113
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   114
text {*
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   115
  The specification of a locale is fixed, but its list of conclusions
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   116
  may be extended through Isar commands that take a \emph{target} argument.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   117
  In the following, \isakeyword{definition} and 
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   118
  \isakeyword{theorem} are illustrated.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   119
  Table~\ref{tab:commands-with-target} lists Isar commands that accept
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   120
  a target.  Isar provides various ways of specifying the target.  A
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   121
  target for a single command may be indicated with keyword
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   122
  \isakeyword{in} in the following way:
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   123
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   124
\begin{table}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   125
\hrule
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   126
\vspace{2ex}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   127
\begin{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   128
\begin{tabular}{ll}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   129
  \isakeyword{definition} & definition through an equation \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   130
  \isakeyword{inductive} & inductive definition \\
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30780
diff changeset
   131
  \isakeyword{primrec} & primitive recursion \\
a53f4872400e Improvements to the text.
ballarin
parents: 30780
diff changeset
   132
  \isakeyword{fun}, \isakeyword{function} & general recursion \\
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   133
  \isakeyword{abbreviation} & syntactic abbreviation \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   134
  \isakeyword{theorem}, etc.\ & theorem statement with proof \\
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30780
diff changeset
   135
  \isakeyword{theorems}, etc.\ & redeclaration of theorems \\
a53f4872400e Improvements to the text.
ballarin
parents: 30780
diff changeset
   136
  \isakeyword{text}, etc.\ & document markup
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   137
\end{tabular}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   138
\end{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   139
\hrule
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   140
\caption{Isar commands that accept a target.}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   141
\label{tab:commands-with-target}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   142
\end{table}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   143
  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   144
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   145
  definition (in partial_order)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   146
    less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubset>" 50)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   147
    where "(x \<sqsubset> y) = (x \<sqsubseteq> y \<and> x \<noteq> y)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   148
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   149
text (in partial_order) {* The strict order @{text less} with infix
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   150
  syntax~@{text \<sqsubset>} is
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   151
  defined in terms of the locale parameter~@{text le} and the general
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   152
  equality of the object logic we work in.  The definition generates a
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   153
  \emph{foundational constant}
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   154
  @{term partial_order.less} with definition @{thm [source]
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   155
  partial_order.less_def}:
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   156
  @{thm [display, indent=2] partial_order.less_def}
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30780
diff changeset
   157
  At the same time, the locale is extended by syntax transformations
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   158
  hiding this construction in the context of the locale.  Here, the
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   159
  abbreviation @{text less} is available for
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   160
  @{text "partial_order.less le"}, and it is printed
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   161
  and parsed as infix~@{text \<sqsubset>}.  Finally, the conclusion @{thm [source]
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   162
  less_def} is added to the locale:
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   163
  @{thm [display, indent=2] less_def}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   164
*}
30393
aa6f42252bf6 replaced old locale option by proper "text (in locale)";
wenzelm
parents: 29567
diff changeset
   165
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   166
text {* The treatment of theorem statements is more straightforward.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   167
  As an example, here is the derivation of a transitivity law for the
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   168
  strict order relation. *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   169
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   170
  lemma (in partial_order) less_le_trans [trans]:
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   171
    "\<lbrakk> x \<sqsubset> y; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<sqsubset> z"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   172
    unfolding %visible less_def by %visible (blast intro: trans)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   173
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   174
text {* In the context of the proof, conclusions of the
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   175
  locale may be used like theorems.  Attributes are effective: @{text
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   176
  anti_sym} was
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   177
  declared as introduction rule, hence it is in the context's set of
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   178
  rules used by the classical reasoner by default.  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   179
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   180
subsection {* Context Blocks *}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   181
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   182
text {* When working with locales, sequences of commands with the same
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   183
  target are frequent.  A block of commands, delimited by
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   184
  \isakeyword{begin} and \isakeyword{end}, makes a theory-like style
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   185
  of working possible.  All commands inside the block refer to the
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   186
  same target.  A block may immediately follow a locale
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   187
  declaration, which makes that locale the target.  Alternatively the
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   188
  target for a block may be given with the \isakeyword{context}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   189
  command.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   190
30580
cc5a55d7a5be Updated chapters 1-5 to locale reimplementation.
ballarin
parents: 30393
diff changeset
   191
  This style of working is illustrated in the block below, where
cc5a55d7a5be Updated chapters 1-5 to locale reimplementation.
ballarin
parents: 30393
diff changeset
   192
  notions of infimum and supremum for partial orders are introduced,
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   193
  together with theorems about their uniqueness.  *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   194
46855
f72a2bedd7a9 more precise alignment of begin/end, proof/qed;
wenzelm
parents: 37206
diff changeset
   195
  context partial_order
f72a2bedd7a9 more precise alignment of begin/end, proof/qed;
wenzelm
parents: 37206
diff changeset
   196
  begin
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   197
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   198
  definition
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   199
    is_inf where "is_inf x y i =
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   200
      (i \<sqsubseteq> x \<and> i \<sqsubseteq> y \<and> (\<forall>z. z \<sqsubseteq> x \<and> z \<sqsubseteq> y \<longrightarrow> z \<sqsubseteq> i))"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   201
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   202
  definition
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   203
    is_sup where "is_sup x y s =
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   204
      (x \<sqsubseteq> s \<and> y \<sqsubseteq> s \<and> (\<forall>z. x \<sqsubseteq> z \<and> y \<sqsubseteq> z \<longrightarrow> s \<sqsubseteq> z))"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   205
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   206
  lemma %invisible is_infI [intro?]: "i \<sqsubseteq> x \<Longrightarrow> i \<sqsubseteq> y \<Longrightarrow>
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   207
      (\<And>z. z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> i) \<Longrightarrow> is_inf x y i"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   208
    by (unfold is_inf_def) blast
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   209
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   210
  lemma %invisible is_inf_lower [elim?]:
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   211
    "is_inf x y i \<Longrightarrow> (i \<sqsubseteq> x \<Longrightarrow> i \<sqsubseteq> y \<Longrightarrow> C) \<Longrightarrow> C"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   212
    by (unfold is_inf_def) blast
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   213
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   214
  lemma %invisible is_inf_greatest [elim?]:
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   215
      "is_inf x y i \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> i"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   216
    by (unfold is_inf_def) blast
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   217
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   218
  theorem is_inf_uniq: "\<lbrakk>is_inf x y i; is_inf x y i'\<rbrakk> \<Longrightarrow> i = i'"
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   219
    proof -
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   220
    assume inf: "is_inf x y i"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   221
    assume inf': "is_inf x y i'"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   222
    show ?thesis
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   223
    proof (rule anti_sym)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   224
      from inf' show "i \<sqsubseteq> i'"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   225
      proof (rule is_inf_greatest)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   226
        from inf show "i \<sqsubseteq> x" ..
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   227
        from inf show "i \<sqsubseteq> y" ..
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   228
      qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   229
      from inf show "i' \<sqsubseteq> i"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   230
      proof (rule is_inf_greatest)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   231
        from inf' show "i' \<sqsubseteq> x" ..
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   232
        from inf' show "i' \<sqsubseteq> y" ..
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   233
      qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   234
    qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   235
  qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   236
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   237
  theorem %invisible is_inf_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> is_inf x y x"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   238
  proof -
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   239
    assume "x \<sqsubseteq> y"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   240
    show ?thesis
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   241
    proof
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   242
      show "x \<sqsubseteq> x" ..
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   243
      show "x \<sqsubseteq> y" by fact
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   244
      fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" show "z \<sqsubseteq> x" by fact
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   245
    qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   246
  qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   247
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   248
  lemma %invisible is_supI [intro?]: "x \<sqsubseteq> s \<Longrightarrow> y \<sqsubseteq> s \<Longrightarrow>
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   249
      (\<And>z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> s \<sqsubseteq> z) \<Longrightarrow> is_sup x y s"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   250
    by (unfold is_sup_def) blast
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   251
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   252
  lemma %invisible is_sup_least [elim?]:
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   253
      "is_sup x y s \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> s \<sqsubseteq> z"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   254
    by (unfold is_sup_def) blast
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   255
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   256
  lemma %invisible is_sup_upper [elim?]:
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   257
      "is_sup x y s \<Longrightarrow> (x \<sqsubseteq> s \<Longrightarrow> y \<sqsubseteq> s \<Longrightarrow> C) \<Longrightarrow> C"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   258
    by (unfold is_sup_def) blast
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   259
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   260
  theorem is_sup_uniq: "\<lbrakk>is_sup x y s; is_sup x y s'\<rbrakk> \<Longrightarrow> s = s'"
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   261
    proof -
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   262
    assume sup: "is_sup x y s"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   263
    assume sup': "is_sup x y s'"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   264
    show ?thesis
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   265
    proof (rule anti_sym)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   266
      from sup show "s \<sqsubseteq> s'"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   267
      proof (rule is_sup_least)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   268
        from sup' show "x \<sqsubseteq> s'" ..
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   269
        from sup' show "y \<sqsubseteq> s'" ..
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   270
      qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   271
      from sup' show "s' \<sqsubseteq> s"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   272
      proof (rule is_sup_least)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   273
        from sup show "x \<sqsubseteq> s" ..
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   274
        from sup show "y \<sqsubseteq> s" ..
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   275
      qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   276
    qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   277
  qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   278
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   279
  theorem %invisible is_sup_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> is_sup x y y"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   280
  proof -
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   281
    assume "x \<sqsubseteq> y"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   282
    show ?thesis
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   283
    proof
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   284
      show "x \<sqsubseteq> y" by fact
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   285
      show "y \<sqsubseteq> y" ..
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   286
      fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   287
      show "y \<sqsubseteq> z" by fact
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   288
    qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   289
  qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   290
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   291
  end
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   292
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   293
text {* The syntax of the locale commands discussed in this tutorial is
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   294
  shown in Table~\ref{tab:commands}.  The grammar is complete with the
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   295
  exception of the context elements \isakeyword{constrains} and
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   296
  \isakeyword{defines}, which are provided for backward
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   297
  compatibility.  See the Isabelle/Isar Reference
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   298
  Manual~\cite{IsarRef} for full documentation.  *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   299
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   300
30580
cc5a55d7a5be Updated chapters 1-5 to locale reimplementation.
ballarin
parents: 30393
diff changeset
   301
section {* Import \label{sec:import} *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   302
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   303
text {* 
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   304
  Algebraic structures are commonly defined by adding operations and
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   305
  properties to existing structures.  For example, partial orders
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   306
  are extended to lattices and total orders.  Lattices are extended to
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   307
  distributive lattices. *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   308
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   309
text {*
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   310
  With locales, this kind of inheritance is achieved through
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   311
  \emph{import} of locales.  The import part of a locale declaration,
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   312
  if present, precedes the context elements.  Here is an example,
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   313
  where partial orders are extended to lattices.
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   314
  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   315
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   316
  locale lattice = partial_order +
30580
cc5a55d7a5be Updated chapters 1-5 to locale reimplementation.
ballarin
parents: 30393
diff changeset
   317
    assumes ex_inf: "\<exists>inf. is_inf x y inf"
cc5a55d7a5be Updated chapters 1-5 to locale reimplementation.
ballarin
parents: 30393
diff changeset
   318
      and ex_sup: "\<exists>sup. is_sup x y sup"
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   319
  begin
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   320
30580
cc5a55d7a5be Updated chapters 1-5 to locale reimplementation.
ballarin
parents: 30393
diff changeset
   321
text {* These assumptions refer to the predicates for infimum
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   322
  and supremum defined for @{text partial_order} in the previous
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   323
  section.  We now introduce the notions of meet and join.  *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   324
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   325
  definition
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   326
    meet (infixl "\<sqinter>" 70) where "x \<sqinter> y = (THE inf. is_inf x y inf)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   327
  definition
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   328
    join (infixl "\<squnion>" 65) where "x \<squnion> y = (THE sup. is_sup x y sup)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   329
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   330
  lemma %invisible meet_equality [elim?]: "is_inf x y i \<Longrightarrow> x \<sqinter> y = i"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   331
  proof (unfold meet_def)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   332
    assume "is_inf x y i"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   333
    then show "(THE i. is_inf x y i) = i"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   334
      by (rule the_equality) (rule is_inf_uniq [OF _ `is_inf x y i`])
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   335
  qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   336
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   337
  lemma %invisible meetI [intro?]:
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   338
      "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"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   339
    by (rule meet_equality, rule is_infI) blast+
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   340
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   341
  lemma %invisible is_inf_meet [intro?]: "is_inf x y (x \<sqinter> y)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   342
  proof (unfold meet_def)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   343
    from ex_inf obtain i where "is_inf x y i" ..
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   344
    then show "is_inf x y (THE i. is_inf x y i)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   345
      by (rule theI) (rule is_inf_uniq [OF _ `is_inf x y i`])
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   346
  qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   347
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   348
  lemma %invisible meet_left [intro?]:
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   349
    "x \<sqinter> y \<sqsubseteq> x"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   350
    by (rule is_inf_lower) (rule is_inf_meet)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   351
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   352
  lemma %invisible meet_right [intro?]:
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   353
    "x \<sqinter> y \<sqsubseteq> y"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   354
    by (rule is_inf_lower) (rule is_inf_meet)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   355
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   356
  lemma %invisible meet_le [intro?]:
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   357
    "\<lbrakk> z \<sqsubseteq> x; z \<sqsubseteq> y \<rbrakk> \<Longrightarrow> z \<sqsubseteq> x \<sqinter> y"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   358
    by (rule is_inf_greatest) (rule is_inf_meet)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   359
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   360
  lemma %invisible join_equality [elim?]: "is_sup x y s \<Longrightarrow> x \<squnion> y = s"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   361
  proof (unfold join_def)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   362
    assume "is_sup x y s"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   363
    then show "(THE s. is_sup x y s) = s"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   364
      by (rule the_equality) (rule is_sup_uniq [OF _ `is_sup x y s`])
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   365
  qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   366
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   367
  lemma %invisible joinI [intro?]: "x \<sqsubseteq> s \<Longrightarrow> y \<sqsubseteq> s \<Longrightarrow>
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   368
      (\<And>z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> s \<sqsubseteq> z) \<Longrightarrow> x \<squnion> y = s"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   369
    by (rule join_equality, rule is_supI) blast+
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   370
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   371
  lemma %invisible is_sup_join [intro?]: "is_sup x y (x \<squnion> y)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   372
  proof (unfold join_def)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   373
    from ex_sup obtain s where "is_sup x y s" ..
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   374
    then show "is_sup x y (THE s. is_sup x y s)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   375
      by (rule theI) (rule is_sup_uniq [OF _ `is_sup x y s`])
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   376
  qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   377
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   378
  lemma %invisible join_left [intro?]:
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   379
    "x \<sqsubseteq> x \<squnion> y"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   380
    by (rule is_sup_upper) (rule is_sup_join)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   381
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   382
  lemma %invisible join_right [intro?]:
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   383
    "y \<sqsubseteq> x \<squnion> y"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   384
    by (rule is_sup_upper) (rule is_sup_join)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   385
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   386
  lemma %invisible join_le [intro?]:
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   387
    "\<lbrakk> x \<sqsubseteq> z; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   388
    by (rule is_sup_least) (rule is_sup_join)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   389
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   390
  theorem %invisible meet_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   391
  proof (rule meetI)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   392
    show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x \<sqinter> y"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   393
    proof
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   394
      show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x" ..
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   395
      show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   396
      proof -
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   397
        have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" ..
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   398
        also have "\<dots> \<sqsubseteq> y" ..
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   399
        finally show ?thesis .
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   400
      qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   401
    qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   402
    show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> z"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   403
    proof -
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   404
      have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" ..
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   405
      also have "\<dots> \<sqsubseteq> z" ..
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   406
      finally show ?thesis .
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   407
    qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   408
    fix w assume "w \<sqsubseteq> x \<sqinter> y" and "w \<sqsubseteq> z"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   409
    show "w \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   410
    proof
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   411
      show "w \<sqsubseteq> x"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   412
      proof -
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   413
        have "w \<sqsubseteq> x \<sqinter> y" by fact
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   414
        also have "\<dots> \<sqsubseteq> x" ..
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   415
        finally show ?thesis .
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   416
      qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   417
      show "w \<sqsubseteq> y \<sqinter> z"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   418
      proof
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   419
        show "w \<sqsubseteq> y"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   420
        proof -
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   421
          have "w \<sqsubseteq> x \<sqinter> y" by fact
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   422
          also have "\<dots> \<sqsubseteq> y" ..
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   423
          finally show ?thesis .
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   424
        qed
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   425
        show "w \<sqsubseteq> z" by fact
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   426
      qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   427
    qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   428
  qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   429
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   430
  theorem %invisible meet_commute: "x \<sqinter> y = y \<sqinter> x"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   431
  proof (rule meetI)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   432
    show "y \<sqinter> x \<sqsubseteq> x" ..
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   433
    show "y \<sqinter> x \<sqsubseteq> y" ..
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   434
    fix z assume "z \<sqsubseteq> y" and "z \<sqsubseteq> x"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   435
    then show "z \<sqsubseteq> y \<sqinter> x" ..
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   436
  qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   437
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   438
  theorem %invisible meet_join_absorb: "x \<sqinter> (x \<squnion> y) = x"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   439
  proof (rule meetI)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   440
    show "x \<sqsubseteq> x" ..
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   441
    show "x \<sqsubseteq> x \<squnion> y" ..
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   442
    fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> x \<squnion> y"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   443
    show "z \<sqsubseteq> x" by fact
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   444
  qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   445
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   446
  theorem %invisible join_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   447
  proof (rule joinI)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   448
    show "x \<squnion> y \<sqsubseteq> x \<squnion> (y \<squnion> z)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   449
    proof
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   450
      show "x \<sqsubseteq> x \<squnion> (y \<squnion> z)" ..
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   451
      show "y \<sqsubseteq> x \<squnion> (y \<squnion> z)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   452
      proof -
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   453
        have "y \<sqsubseteq> y \<squnion> z" ..
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   454
        also have "... \<sqsubseteq> x \<squnion> (y \<squnion> z)" ..
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   455
        finally show ?thesis .
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   456
      qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   457
    qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   458
    show "z \<sqsubseteq> x \<squnion> (y \<squnion> z)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   459
    proof -
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   460
      have "z \<sqsubseteq> y \<squnion> z"  ..
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   461
      also have "... \<sqsubseteq> x \<squnion> (y \<squnion> z)" ..
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   462
      finally show ?thesis .
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   463
    qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   464
    fix w assume "x \<squnion> y \<sqsubseteq> w" and "z \<sqsubseteq> w"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   465
    show "x \<squnion> (y \<squnion> z) \<sqsubseteq> w"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   466
    proof
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   467
      show "x \<sqsubseteq> w"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   468
      proof -
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   469
        have "x \<sqsubseteq> x \<squnion> y" ..
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   470
        also have "\<dots> \<sqsubseteq> w" by fact
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   471
        finally show ?thesis .
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   472
      qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   473
      show "y \<squnion> z \<sqsubseteq> w"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   474
      proof
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   475
        show "y \<sqsubseteq> w"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   476
        proof -
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   477
          have "y \<sqsubseteq> x \<squnion> y" ..
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   478
          also have "... \<sqsubseteq> w" by fact
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   479
          finally show ?thesis .
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   480
        qed
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   481
        show "z \<sqsubseteq> w" by fact
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   482
      qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   483
    qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   484
  qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   485
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   486
  theorem %invisible join_commute: "x \<squnion> y = y \<squnion> x"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   487
  proof (rule joinI)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   488
    show "x \<sqsubseteq> y \<squnion> x" ..
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   489
    show "y \<sqsubseteq> y \<squnion> x" ..
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   490
    fix z assume "y \<sqsubseteq> z" and "x \<sqsubseteq> z"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   491
    then show "y \<squnion> x \<sqsubseteq> z" ..
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   492
  qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   493
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   494
  theorem %invisible join_meet_absorb: "x \<squnion> (x \<sqinter> y) = x"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   495
  proof (rule joinI)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   496
    show "x \<sqsubseteq> x" ..
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   497
    show "x \<sqinter> y \<sqsubseteq> x" ..
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   498
    fix z assume "x \<sqsubseteq> z" and "x \<sqinter> y \<sqsubseteq> z"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   499
    show "x \<sqsubseteq> z" by fact
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   500
  qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   501
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   502
  theorem %invisible meet_idem: "x \<sqinter> x = x"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   503
  proof -
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   504
    have "x \<sqinter> (x \<squnion> (x \<sqinter> x)) = x" by (rule meet_join_absorb)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   505
    also have "x \<squnion> (x \<sqinter> x) = x" by (rule join_meet_absorb)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   506
    finally show ?thesis .
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   507
  qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   508
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   509
  theorem %invisible meet_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   510
  proof (rule meetI)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   511
    assume "x \<sqsubseteq> y"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   512
    show "x \<sqsubseteq> x" ..
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   513
    show "x \<sqsubseteq> y" by fact
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   514
    fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   515
    show "z \<sqsubseteq> x" by fact
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   516
  qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   517
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   518
  theorem %invisible meet_related2 [elim?]: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   519
    by (drule meet_related) (simp add: meet_commute)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   520
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   521
  theorem %invisible join_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   522
  proof (rule joinI)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   523
    assume "x \<sqsubseteq> y"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   524
    show "y \<sqsubseteq> y" ..
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   525
    show "x \<sqsubseteq> y" by fact
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   526
    fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   527
    show "y \<sqsubseteq> z" by fact
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   528
  qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   529
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   530
  theorem %invisible join_related2 [elim?]: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   531
    by (drule join_related) (simp add: join_commute)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   532
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   533
  theorem %invisible meet_connection: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   534
  proof
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   535
    assume "x \<sqsubseteq> y"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   536
    then have "is_inf x y x" ..
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   537
    then show "x \<sqinter> y = x" ..
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   538
  next
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   539
    have "x \<sqinter> y \<sqsubseteq> y" ..
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   540
    also assume "x \<sqinter> y = x"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   541
    finally show "x \<sqsubseteq> y" .
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   542
  qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   543
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   544
  theorem %invisible join_connection: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   545
  proof
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   546
    assume "x \<sqsubseteq> y"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   547
    then have "is_sup x y y" ..
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   548
    then show "x \<squnion> y = y" ..
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   549
  next
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   550
    have "x \<sqsubseteq> x \<squnion> y" ..
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   551
    also assume "x \<squnion> y = y"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   552
    finally show "x \<sqsubseteq> y" .
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   553
  qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   554
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   555
  theorem %invisible meet_connection2: "(x \<sqsubseteq> y) = (y \<sqinter> x = x)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   556
    using meet_commute meet_connection by simp
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   557
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   558
  theorem %invisible join_connection2: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   559
    using join_commute join_connection by simp
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   560
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   561
  text %invisible {* Naming according to Jacobson I, p.\ 459. *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   562
  lemmas %invisible L1 = join_commute meet_commute
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   563
  lemmas %invisible L2 = join_assoc meet_assoc
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   564
  (* lemmas L3 = join_idem meet_idem *)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   565
  lemmas %invisible L4 = join_meet_absorb meet_join_absorb
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   566
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   567
  end
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   568
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   569
text {* Locales for total orders and distributive lattices follow to
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   570
  establish a sufficiently rich landscape of locales for
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   571
  further examples in this tutorial.  Each comes with an example
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   572
  theorem. *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   573
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   574
  locale total_order = partial_order +
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   575
    assumes total: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   576
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   577
  lemma (in total_order) less_total: "x \<sqsubset> y \<or> x = y \<or> y \<sqsubset> x"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   578
    using total
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   579
    by (unfold less_def) blast
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   580
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   581
  locale distrib_lattice = lattice +
30580
cc5a55d7a5be Updated chapters 1-5 to locale reimplementation.
ballarin
parents: 30393
diff changeset
   582
    assumes meet_distr: "x \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> z"
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   583
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   584
  lemma (in distrib_lattice) join_distr:
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   585
    "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"  (* txt {* Jacobson I, p.\ 462 *} *)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   586
    proof -
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   587
    have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by (simp add: L4)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   588
    also have "... = x \<squnion> ((x \<sqinter> z) \<squnion> (y \<sqinter> z))" by (simp add: L2)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   589
    also have "... = x \<squnion> ((x \<squnion> y) \<sqinter> z)" by (simp add: L1 meet_distr)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   590
    also have "... = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)" by (simp add: L1 L4)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   591
    also have "... = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by (simp add: meet_distr)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   592
    finally show ?thesis .
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   593
  qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   594
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   595
text {*
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   596
  The locale hierarchy obtained through these declarations is shown in
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   597
  Figure~\ref{fig:lattices}(a).
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   598
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   599
\begin{figure}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   600
\hrule \vspace{2ex}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   601
\begin{center}
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   602
\subfigure[Declared hierarchy]{
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   603
\begin{tikzpicture}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   604
  \node (po) at (0,0) {@{text partial_order}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   605
  \node (lat) at (-1.5,-1) {@{text lattice}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   606
  \node (dlat) at (-1.5,-2) {@{text distrib_lattice}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   607
  \node (to) at (1.5,-1) {@{text total_order}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   608
  \draw (po) -- (lat);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   609
  \draw (lat) -- (dlat);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   610
  \draw (po) -- (to);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   611
%  \draw[->, dashed] (lat) -- (to);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   612
\end{tikzpicture}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   613
} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   614
\subfigure[Total orders are lattices]{
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   615
\begin{tikzpicture}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   616
  \node (po) at (0,0) {@{text partial_order}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   617
  \node (lat) at (0,-1) {@{text lattice}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   618
  \node (dlat) at (-1.5,-2) {@{text distrib_lattice}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   619
  \node (to) at (1.5,-2) {@{text total_order}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   620
  \draw (po) -- (lat);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   621
  \draw (lat) -- (dlat);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   622
  \draw (lat) -- (to);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   623
%  \draw[->, dashed] (dlat) -- (to);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   624
\end{tikzpicture}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   625
} \quad
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   626
\subfigure[Total orders are distributive lattices]{
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   627
\begin{tikzpicture}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   628
  \node (po) at (0,0) {@{text partial_order}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   629
  \node (lat) at (0,-1) {@{text lattice}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   630
  \node (dlat) at (0,-2) {@{text distrib_lattice}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   631
  \node (to) at (0,-3) {@{text total_order}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   632
  \draw (po) -- (lat);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   633
  \draw (lat) -- (dlat);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   634
  \draw (dlat) -- (to);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   635
\end{tikzpicture}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   636
}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   637
\end{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   638
\hrule
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   639
\caption{Hierarchy of Lattice Locales.}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   640
\label{fig:lattices}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   641
\end{figure}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   642
  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   643
30580
cc5a55d7a5be Updated chapters 1-5 to locale reimplementation.
ballarin
parents: 30393
diff changeset
   644
section {* Changing the Locale Hierarchy
cc5a55d7a5be Updated chapters 1-5 to locale reimplementation.
ballarin
parents: 30393
diff changeset
   645
  \label{sec:changing-the-hierarchy} *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   646
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   647
text {*
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   648
  Locales enable to prove theorems abstractly, relative to
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   649
  sets of assumptions.  These theorems can then be used in other
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   650
  contexts where the assumptions themselves, or
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   651
  instances of the assumptions, are theorems.  This form of theorem
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   652
  reuse is called \emph{interpretation}.  Locales generalise
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   653
  interpretation from theorems to conclusions, enabling the reuse of
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   654
  definitions and other constructs that are not part of the
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   655
  specifications of the locales.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   656
37094
2e93e29a809a Typo fixed.
webertj
parents: 36691
diff changeset
   657
  The first form of interpretation we will consider in this tutorial
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   658
  is provided by the \isakeyword{sublocale} command.  It enables to
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   659
  modify the import hierarchy to reflect the \emph{logical} relation
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   660
  between locales.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   661
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   662
  Consider the locale hierarchy from Figure~\ref{fig:lattices}(a).
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   663
  Total orders are lattices, although this is not reflected here, and
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   664
  definitions, theorems and other conclusions
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   665
  from @{term lattice} are not available in @{term total_order}.  To
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   666
  obtain the situation in Figure~\ref{fig:lattices}(b), it is
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   667
  sufficient to add the conclusions of the latter locale to the former.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   668
  The \isakeyword{sublocale} command does exactly this.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   669
  The declaration \isakeyword{sublocale} $l_1
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   670
  \subseteq l_2$ causes locale $l_2$ to be \emph{interpreted} in the
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   671
  context of $l_1$.  This means that all conclusions of $l_2$ are made
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   672
  available in $l_1$.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   673
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   674
  Of course, the change of hierarchy must be supported by a theorem
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   675
  that reflects, in our example, that total orders are indeed
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   676
  lattices.  Therefore the \isakeyword{sublocale} command generates a
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   677
  goal, which must be discharged by the user.  This is illustrated in
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   678
  the following paragraphs.  First the sublocale relation is stated.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   679
*}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   680
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27375
diff changeset
   681
  sublocale %visible total_order \<subseteq> lattice
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   682
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   683
txt {* \normalsize
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   684
  This enters the context of locale @{text total_order}, in
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   685
  which the goal @{subgoals [display]} must be shown.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   686
  Now the
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   687
  locale predicate needs to be unfolded --- for example, using its
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   688
  definition or by introduction rules
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   689
  provided by the locale package.  For automation, the locale package
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   690
  provides the methods @{text intro_locales} and @{text
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   691
  unfold_locales}.  They are aware of the
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   692
  current context and dependencies between locales and automatically
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   693
  discharge goals implied by these.  While @{text unfold_locales}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   694
  always unfolds locale predicates to assumptions, @{text
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   695
  intro_locales} only unfolds definitions along the locale
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   696
  hierarchy, leaving a goal consisting of predicates defined by the
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   697
  locale package.  Occasionally the latter is of advantage since the goal
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   698
  is smaller.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   699
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   700
  For the current goal, we would like to get hold of
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   701
  the assumptions of @{text lattice}, which need to be shown, hence
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   702
  @{text unfold_locales} is appropriate. *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   703
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   704
  proof unfold_locales
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   705
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   706
txt {* \normalsize
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   707
  Since the fact that both lattices and total orders are partial
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   708
  orders is already reflected in the locale hierarchy, the assumptions
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   709
  of @{text partial_order} are discharged automatically, and only the
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   710
  assumptions introduced in @{text lattice} remain as subgoals
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   711
  @{subgoals [display]}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   712
  The proof for the first subgoal is obtained by constructing an
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   713
  infimum, whose existence is implied by totality. *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   714
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   715
    fix x y
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   716
    from total have "is_inf x y (if x \<sqsubseteq> y then x else y)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   717
      by (auto simp: is_inf_def)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   718
    then show "\<exists>inf. is_inf x y inf" ..
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   719
txt {* \normalsize
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   720
   The proof for the second subgoal is analogous and not
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   721
  reproduced here. *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   722
  next %invisible
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   723
    fix x y
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   724
    from total have "is_sup x y (if x \<sqsubseteq> y then y else x)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   725
      by (auto simp: is_sup_def)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   726
    then show "\<exists>sup. is_sup x y sup" .. qed %visible
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   727
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   728
text {* Similarly, we may establish that total orders are distributive
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   729
  lattices with a second \isakeyword{sublocale} statement. *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   730
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27375
diff changeset
   731
  sublocale total_order \<subseteq> distrib_lattice
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   732
    proof unfold_locales
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   733
    fix %"proof" x y z
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   734
    show "x \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> z" (is "?l = ?r")
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   735
      txt {* Jacobson I, p.\ 462 *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   736
    proof -
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   737
      { assume c: "y \<sqsubseteq> x" "z \<sqsubseteq> x"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   738
        from c have "?l = y \<squnion> z"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   739
          by (metis c join_connection2 join_related2 meet_related2 total)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   740
        also from c have "... = ?r" by (metis meet_related2)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   741
        finally have "?l = ?r" . }
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   742
      moreover
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   743
      { assume c: "x \<sqsubseteq> y \<or> x \<sqsubseteq> z"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   744
        from c have "?l = x"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   745
          by (metis join_connection2 join_related2 meet_connection total trans)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   746
        also from c have "... = ?r"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   747
          by (metis join_commute join_related2 meet_connection meet_related2 total)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30826
diff changeset
   748
        finally have "?l = ?r" . }
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   749
      moreover note total
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   750
      ultimately show ?thesis by blast
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   751
    qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   752
  qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   753
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   754
text {* The locale hierarchy is now as shown in
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   755
  Figure~\ref{fig:lattices}(c). *}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   756
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   757
text {*
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   758
  Locale interpretation is \emph{dynamic}.  The statement
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   759
  \isakeyword{sublocale} $l_1 \subseteq l_2$ will not just add the
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   760
  current conclusions of $l_2$ to $l_1$.  Rather the dependency is
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   761
  stored, and conclusions that will be
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   762
  added to $l_2$ in future are automatically propagated to $l_1$.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   763
  The sublocale relation is transitive --- that is, propagation takes
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   764
  effect along chains of sublocales.  Even cycles in the sublocale relation are
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
   765
  supported, as long as these cycles do not lead to infinite chains.
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   766
  Details are discussed in the technical report \cite{Ballarin2006a}.
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
   767
  See also Section~\ref{sec:infinite-chains} of this tutorial.  *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   768
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   769
end