doc-src/Locales/Locales/Examples3.thy
author ballarin
Mon, 19 Jan 2009 20:37:08 +0100
changeset 29566 937baa077df2
parent 27595 3ac9e3cd1fa3
child 29567 286c01be90cb
permissions -rw-r--r--
Fixed tutorial to compile with new locales; grammar of new locale commands.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27081
6d2a458be1b6 replaced (*<*)(*>*) by invisibility tags;
wenzelm
parents: 27077
diff changeset
     1
(* $Id$ *)
6d2a458be1b6 replaced (*<*)(*>*) by invisibility tags;
wenzelm
parents: 27077
diff changeset
     2
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     3
theory Examples3
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     4
imports Examples
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     5
begin
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     6
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     7
subsection {* Third Version: Local Interpretation *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     8
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     9
text {* In the above example, the fact that @{text \<le>} is a partial
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    10
  order for the natural numbers was used in the proof of the
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    11
  second goal.  In general, proofs of the equations may involve
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    12
  theorems implied by the fact the assumptions of the instantiated
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    13
  locale hold for the instantiating structure.  If these theorems have
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    14
  been shown abstractly in the locale they can be made available
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    15
  conveniently in the context through an auxiliary local interpretation (keyword
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    16
  \isakeyword{interpret}).  This interpretation is inside the proof of the global
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    17
  interpretation.  The third revision of the example illustrates this.  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    18
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
    19
interpretation %visible nat: partial_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    20
  where "partial_order.less (op \<le>) (x::nat) y = (x < y)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    21
proof -
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    22
  show "partial_order (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    23
    by unfold_locales auto
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
    24
  then interpret nat: partial_order "op \<le> :: [nat, nat] \<Rightarrow> bool" .
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    25
  show "partial_order.less (op \<le>) (x::nat) y = (x < y)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    26
    unfolding nat.less_def by auto
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    27
qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    28
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    29
text {* The inner interpretation does not require an
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    30
  elaborate new proof, it is immediate from the preceeding fact and
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    31
  proved with ``.''.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    32
  This interpretation enriches the local proof context by
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    33
  the very theorems also obtained in the interpretation from
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    34
  Section~\ref{sec:po-first}, and @{text nat.less_def} may directly be
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    35
  used to unfold the definition.  Theorems from the local
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    36
  interpretation disappear after leaving the proof context --- that
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    37
  is, after the closing \isakeyword{qed} --- and are
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    38
  then replaced by those with the desired substitutions of the strict
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    39
  order. *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    40
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    41
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    42
subsection {* Further Interpretations *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    43
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    44
text {* Further interpretations are necessary to reuse theorems from
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    45
  the other locales.  In @{text lattice} the operations @{text \<sqinter>} and
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    46
  @{text \<squnion>} are substituted by @{term "min :: nat \<Rightarrow> nat \<Rightarrow> nat"} and
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    47
  @{term "max :: nat \<Rightarrow> nat \<Rightarrow> nat"}.  The entire proof for the
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    48
  interpretation is reproduced in order to give an example of a more
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    49
  elaborate interpretation proof.  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    50
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
    51
interpretation %visible nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    52
  where "lattice.meet op \<le> (x::nat) y = min x y"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    53
    and "lattice.join op \<le> (x::nat) y = max x y"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    54
proof -
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    55
  show "lattice (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    56
    txt {* We have already shown that this is a partial order, *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    57
    apply unfold_locales
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    58
    txt {* hence only the lattice axioms remain to be shown: @{subgoals
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    59
      [display]}  After unfolding @{text is_inf} and @{text is_sup}, *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    60
    apply (unfold nat.is_inf_def nat.is_sup_def)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    61
    txt {* the goals become @{subgoals [display]} which can be solved
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    62
      by Presburger arithmetic. *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    63
    by arith+
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    64
  txt {* In order to show the equations, we put ourselves in a
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    65
    situation where the lattice theorems can be used in a convenient way. *}
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
    66
  then interpret nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool" .
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    67
  show "lattice.meet op \<le> (x::nat) y = min x y"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    68
    by (bestsimp simp: nat.meet_def nat.is_inf_def)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    69
  show "lattice.join op \<le> (x::nat) y = max x y"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    70
    by (bestsimp simp: nat.join_def nat.is_sup_def)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    71
qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    72
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    73
text {* That the relation @{text \<le>} is a total order completes this
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    74
  sequence of interpretations. *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    75
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
    76
interpretation %visible nat: total_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    77
  by unfold_locales arith
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    78
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    79
text {* Theorems that are available in the theory at this point are shown in
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    80
  Table~\ref{tab:nat-lattice}.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    81
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    82
\begin{table}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    83
\hrule
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    84
\vspace{2ex}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    85
\begin{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    86
\begin{tabular}{l}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    87
  @{thm [source] nat.less_def} from locale @{text partial_order}: \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    88
  \quad @{thm nat.less_def} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    89
  @{thm [source] nat.meet_left} from locale @{text lattice}: \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    90
  \quad @{thm nat.meet_left} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    91
  @{thm [source] nat.join_distr} from locale @{text distrib_lattice}: \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    92
  \quad @{thm nat.join_distr} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    93
  @{thm [source] nat.less_total} from locale @{text total_order}: \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    94
  \quad @{thm nat.less_total}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    95
\end{tabular}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    96
\end{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    97
\hrule
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    98
\caption{Interpreted theorems for @{text \<le>} on the natural numbers.}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    99
\label{tab:nat-lattice}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   100
\end{table}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   101
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   102
  Note that since the locale hierarchy reflects that total orders are
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   103
  distributive lattices, an explicit interpretation of distributive
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   104
  lattices for the order relation on natural numbers is not neccessary.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   105
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   106
  Why not push this idea further and just give the last interpretation
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   107
  as a single interpretation instead of the sequence of three?  The
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   108
  reasons for this are twofold:
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   109
\begin{itemize}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   110
\item
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   111
  Often it is easier to work in an incremental fashion, because later
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   112
  interpretations require theorems provided by earlier
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   113
  interpretations.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   114
\item
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   115
  Assume that a definition is made in some locale $l_1$, and that $l_2$
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   116
  imports $l_1$.  Let an equation for the definition be
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   117
  proved in an interpretation of $l_2$.  The equation will be unfolded
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   118
  in interpretations of theorems added to $l_2$ or below in the import
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   119
  hierarchy, but not for theorems added above $l_2$.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   120
  Hence, an equation interpreting a definition should always be given in
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   121
  an interpretation of the locale where the definition is made, not in
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   122
  an interpretation of a locale further down the hierarchy.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   123
\end{itemize}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   124
  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   125
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   126
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   127
subsection {* Lattice @{text "dvd"} on @{typ nat} *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   128
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   129
text {* Divisibility on the natural numbers is a distributive lattice
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   130
  but not a total order.  Interpretation again proceeds
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   131
  incrementally. *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   132
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   133
interpretation nat_dvd: partial_order "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   134
  where "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   135
proof -
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   136
  show "partial_order (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   137
    by unfold_locales (auto simp: dvd_def)
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   138
  then interpret nat_dvd: partial_order "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" .
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   139
  show "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   140
    apply (unfold nat_dvd.less_def)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   141
    apply auto
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   142
    done
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   143
qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   144
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   145
text {* Note that there is no symbol for strict divisibility.  Instead,
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   146
  interpretation substitutes @{term "x dvd y \<and> x \<noteq> y"}.   *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   147
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   148
interpretation nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   149
  where nat_dvd_meet_eq:
27595
3ac9e3cd1fa3 curried gcd
haftmann
parents: 27503
diff changeset
   150
      "lattice.meet op dvd = gcd"
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   151
    and nat_dvd_join_eq:
27595
3ac9e3cd1fa3 curried gcd
haftmann
parents: 27503
diff changeset
   152
      "lattice.join op dvd = lcm"
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   153
proof -
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   154
  show "lattice (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   155
    apply unfold_locales
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   156
    apply (unfold nat_dvd.is_inf_def nat_dvd.is_sup_def)
27595
3ac9e3cd1fa3 curried gcd
haftmann
parents: 27503
diff changeset
   157
    apply (rule_tac x = "gcd x y" in exI)
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   158
    apply auto [1]
27595
3ac9e3cd1fa3 curried gcd
haftmann
parents: 27503
diff changeset
   159
    apply (rule_tac x = "lcm x y" in exI)
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   160
    apply (auto intro: lcm_dvd1 lcm_dvd2 lcm_least)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   161
    done
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   162
  then interpret nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" .
27595
3ac9e3cd1fa3 curried gcd
haftmann
parents: 27503
diff changeset
   163
  show "lattice.meet op dvd = gcd"
3ac9e3cd1fa3 curried gcd
haftmann
parents: 27503
diff changeset
   164
    apply (auto simp add: expand_fun_eq)
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   165
    apply (unfold nat_dvd.meet_def)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   166
    apply (rule the_equality)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   167
    apply (unfold nat_dvd.is_inf_def)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   168
    by auto
27595
3ac9e3cd1fa3 curried gcd
haftmann
parents: 27503
diff changeset
   169
  show "lattice.join op dvd = lcm"
3ac9e3cd1fa3 curried gcd
haftmann
parents: 27503
diff changeset
   170
    apply (auto simp add: expand_fun_eq)
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   171
    apply (unfold nat_dvd.join_def)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   172
    apply (rule the_equality)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   173
    apply (unfold nat_dvd.is_sup_def)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   174
    by (auto intro: lcm_dvd1 lcm_dvd2 lcm_least)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   175
qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   176
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   177
text {* Equations @{thm [source] nat_dvd_meet_eq} and @{thm [source]
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   178
  nat_dvd_join_eq} are named since they are handy in the proof of
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   179
  the subsequent interpretation. *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   180
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   181
ML %invisible {* set quick_and_dirty *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   182
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   183
(*
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   184
definition
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   185
  is_lcm :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   186
  "is_lcm p m n \<longleftrightarrow> m dvd p \<and> n dvd p \<and>
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   187
    (\<forall>d. m dvd d \<longrightarrow> n dvd d \<longrightarrow> p dvd d)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   188
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   189
lemma is_gcd: "is_lcm (lcm (m, n)) m n"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   190
  by (simp add: is_lcm_def lcm_least)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   191
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   192
lemma gcd_lcm_distr_lemma:
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   193
  "[| is_gcd g1 x l1; is_lcm l1 y z; is_gcd g2 x y; is_gcd g3 x z |] ==> is_lcm g1 g2 g3"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   194
apply (unfold is_gcd_def is_lcm_def dvd_def)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   195
apply (clarsimp simp: mult_ac)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   196
apply (blast intro: mult_is_0)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   197
thm mult_is_0 [THEN iffD1]
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   198
*)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   199
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   200
lemma %invisible gcd_lcm_distr:
27595
3ac9e3cd1fa3 curried gcd
haftmann
parents: 27503
diff changeset
   201
  "gcd x (lcm y z) = lcm (gcd x y) (gcd x z)" sorry
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   202
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   203
ML %invisible {* reset quick_and_dirty *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   204
  
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   205
interpretation %visible nat_dvd:
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   206
  distrib_lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   207
  apply unfold_locales
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   208
  txt {* @{subgoals [display]} *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   209
  apply (unfold nat_dvd_meet_eq nat_dvd_join_eq)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   210
  txt {* @{subgoals [display]} *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   211
  apply (rule gcd_lcm_distr) done
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   212
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   213
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   214
text {* Theorems that are available in the theory after these
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   215
  interpretations are shown in Table~\ref{tab:nat-dvd-lattice}.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   216
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   217
\begin{table}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   218
\hrule
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   219
\vspace{2ex}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   220
\begin{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   221
\begin{tabular}{l}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   222
  @{thm [source] nat_dvd.less_def} from locale @{text partial_order}: \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   223
  \quad @{thm nat_dvd.less_def} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   224
  @{thm [source] nat_dvd.meet_left} from locale @{text lattice}: \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   225
  \quad @{thm nat_dvd.meet_left} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   226
  @{thm [source] nat_dvd.join_distr} from locale @{text distrib_lattice}: \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   227
  \quad @{thm nat_dvd.join_distr} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   228
\end{tabular}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   229
\end{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   230
\hrule
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   231
\caption{Interpreted theorems for @{text dvd} on the natural numbers.}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   232
\label{tab:nat-dvd-lattice}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   233
\end{table}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   234
  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   235
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   236
text {*
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   237
  The full syntax of the interpretation commands is shown in
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   238
  Table~\ref{tab:commands}.  The grammar refers to
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   239
  \textit{expr}, which stands for a \emph{locale} expression.  Locale
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   240
  expressions are discussed in Section~\ref{sec:expressions}.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   241
  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   242
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   243
27077
f64166dd92f0 moved labels into actual sections;
wenzelm
parents: 27075
diff changeset
   244
section {* Locale Expressions \label{sec:expressions} *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   245
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   246
text {*
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   247
  A map @{term \<phi>} between partial orders @{text \<sqsubseteq>} and @{text \<preceq>}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   248
  is called order preserving if @{text "x \<sqsubseteq> y"} implies @{text "\<phi> x \<preceq>
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   249
  \<phi> y"}.  This situation is more complex than those encountered so
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   250
  far: it involves two partial orders, and it is desirable to use the
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   251
  existing locale for both.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   252
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   253
  Inspecting the grammar of locale commands in
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   254
  Table~\ref{tab:commands} reveals that the import of a locale can be
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   255
  more than just a single locale.  In general, the import is a
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   256
  \emph{locale expression}.  Locale expressions enable to combine locales
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   257
  and rename parameters.  A locale name is a locale expression.  If
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   258
  $e_1$ and $e_2$ are locale expressions then $e_1 + e_2$ is their
27075
34005fa42128 renamed expression: plain ~ (space) instead of \colon;
wenzelm
parents: 27073
diff changeset
   259
  \emph{merge}.  If $e$ is an expression, then $e~q_1 \ldots q_n$ is
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   260
  a \emph{renamed expression} where the parameters in $e$ are renamed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   261
  to $q_1 \ldots q_n$.  Using a locale expression, a locale for order
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   262
  preserving maps can be declared in the following way.  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   263
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   264
  locale order_preserving =
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   265
    le: partial_order + le': partial_order le' for le' (infixl "\<preceq>" 50) +
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   266
    fixes \<phi> :: "'a \<Rightarrow> 'b"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   267
    assumes hom_le: "x \<sqsubseteq> y \<Longrightarrow> \<phi> x \<preceq> \<phi> y"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   268
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   269
text {* The second line contains the expression, which is the
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   270
  merge of two partial order locales.  The parameter of the second one
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   271
  is @{text le'} with new infix syntax @{text \<preceq>}.  The
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   272
  parameters of the entire locale are @{text le}, @{text le'} and
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   273
  @{text \<phi>}.  This is their \emph{canonical order},
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   274
  which is obtained by a left-to-right traversal of the expression,
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   275
  where only the new parameters are appended to the end of the list.  The
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   276
  parameters introduced in the locale elements of the declaration
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   277
  follow.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   278
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   279
  In renamings parameters are referred to by position in the canonical
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   280
  order; an underscore is used to skip a parameter position, which is
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   281
  then not renamed.  Renaming deletes the syntax of a parameter unless
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   282
  a new mixfix annotation is given.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   283
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   284
  Parameter renamings are morphisms between locales.  These can be
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   285
  lifted to terms and theorems and thus be applied to assumptions and
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   286
  conclusions.  The assumption of a merge is the conjunction of the
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   287
  assumptions of the merged locale.  The conclusions of a merge are
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   288
  obtained by appending the conclusions of the left locale and of the
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   289
  right locale.  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   290
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   291
text {* The locale @{text order_preserving} contains theorems for both
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   292
  orders @{text \<sqsubseteq>} and @{text \<preceq>}.  How can one refer to a theorem for
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   293
  a particular order, @{text \<sqsubseteq>} or @{text \<preceq>}?  Names in locales are
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   294
  qualified by the locale parameters.  More precisely, a name is
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   295
  qualified by the parameters of the locale in which its declaration
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   296
  occurs.  Here are examples: *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   297
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   298
context %invisible order_preserving begin
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   299
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   300
text {*
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   301
  @{thm [source] le.less_le_trans}: @{thm le.less_le_trans}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   302
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   303
  @{thm [source] hom_le}: @{thm hom_le}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   304
  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   305
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   306
text {* When renaming a locale, the morphism is also applied
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   307
  to the qualifiers.  Hence theorems for the partial order @{text \<preceq>}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   308
  are qualified by @{text le'}.  For example, @{thm [source]
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   309
  le'.less_le_trans}: @{thm [display, indent=2] le'.less_le_trans} *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   310
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   311
end %invisible
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   312
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   313
text {* This example reveals that there is no infix syntax for the strict
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   314
  version of @{text \<preceq>}!  This can, of course, not be introduced
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   315
  automatically, but it can be declared manually through an abbreviation.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   316
  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   317
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   318
  abbreviation (in order_preserving)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   319
    less' (infixl "\<prec>" 50) where "less' \<equiv> partial_order.less le'"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   320
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   321
text {* Now the theorem is displayed nicely as
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   322
  @{thm [locale=order_preserving] le'.less_le_trans}.  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   323
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   324
text {* Not only names of theorems are qualified.  In fact, all names
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   325
  are qualified, in particular names introduced by definitions and
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   326
  abbreviations.  The name of the strict order of @{text \<sqsubseteq>} is @{text
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   327
  le.less} and therefore @{text le'.less} is the name of the strict
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   328
  order of @{text \<preceq>}.  Hence, the equation in the above abbreviation
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   329
  could have been written as @{text "less' \<equiv> le'.less"}. *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   330
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   331
text {* Two more locales illustrate working with locale expressions.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   332
  A map @{text \<phi>} is a lattice homomorphism if it preserves meet and join. *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   333
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   334
  locale lattice_hom = le: lattice + le': lattice le' for le' (infixl "\<preceq>" 50) +
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   335
    fixes \<phi>
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   336
    assumes hom_meet:
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   337
	"\<phi> (lattice.meet le x y) = lattice.meet le' (\<phi> x) (\<phi> y)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   338
      and hom_join:
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   339
	"\<phi> (lattice.join le x y) = lattice.join le' (\<phi> x) (\<phi> y)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   340
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   341
  abbreviation (in lattice_hom)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   342
    meet' (infixl "\<sqinter>''" 50) where "meet' \<equiv> le'.meet"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   343
  abbreviation (in lattice_hom)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   344
    join' (infixl "\<squnion>''" 50) where "join' \<equiv> le'.join"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   345
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   346
text {* A homomorphism is an endomorphism if both orders coincide. *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   347
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   348
  locale lattice_end =
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   349
    lattice_hom le le for le (infixl "\<sqsubseteq>" 50)
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   350
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   351
text {* The inheritance diagram of the situation we have now is shown
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   352
  in Figure~\ref{fig:hom}, where the dashed line depicts an
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   353
  interpretation which is introduced below.  Renamings are
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   354
  indicated by $\sqsubseteq \mapsto \preceq$ etc.  The expression
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   355
  imported by @{text lattice_end} identifies the first and second
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   356
  parameter of @{text lattice_hom}.  By looking at the inheritance diagram it would seem
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   357
  that two identical copies of each of the locales @{text
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   358
  partial_order} and @{text lattice} are imported.  This is not the
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   359
  case!  Inheritance paths with identical morphisms are detected and
27503
a019d6568a3c fix typo
huffman
parents: 27081
diff changeset
   360
  the conclusions of the respective locales appear only once.
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   361
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   362
\begin{figure}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   363
\hrule \vspace{2ex}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   364
\begin{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   365
\begin{tikzpicture}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   366
  \node (o) at (0,0) {@{text partial_order}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   367
  \node (oh) at (1.5,-2) {@{text order_preserving}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   368
  \node (oh1) at (1.5,-0.7) {$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   369
  \node (oh2) at (0,-1.3) {$\scriptscriptstyle \sqsubseteq \mapsto \preceq$};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   370
  \node (l) at (-1.5,-2) {@{text lattice}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   371
  \node (lh) at (0,-4) {@{text lattice_hom}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   372
  \node (lh1) at (0,-2.7) {$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   373
  \node (lh2) at (-1.5,-3.3) {$\scriptscriptstyle \sqsubseteq \mapsto \preceq$};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   374
  \node (le) at (0,-6) {@{text lattice_end}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   375
  \node (le1) at (0,-4.8)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   376
    [anchor=west]{$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   377
  \node (le2) at (0,-5.2)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   378
    [anchor=west]{$\scriptscriptstyle \preceq \mapsto \sqsubseteq$};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   379
  \draw (o) -- (l);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   380
  \draw[dashed] (oh) -- (lh);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   381
  \draw (lh) -- (le);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   382
  \draw (o) .. controls (oh1.south west) .. (oh);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   383
  \draw (o) .. controls (oh2.north east) .. (oh);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   384
  \draw (l) .. controls (lh1.south west) .. (lh);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   385
  \draw (l) .. controls (lh2.north east) .. (lh);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   386
\end{tikzpicture}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   387
\end{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   388
\hrule
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   389
\caption{Hierarchy of Homomorphism Locales.}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   390
\label{fig:hom}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   391
\end{figure}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   392
  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   393
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   394
text {* It can be shown easily that a lattice homomorphism is order
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   395
  preserving.  As the final example of this section, a locale
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   396
  interpretation is used to assert this. *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   397
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   398
  sublocale lattice_hom \<subseteq> order_preserving proof unfold_locales
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   399
    fix x y
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   400
    assume "x \<sqsubseteq> y"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   401
    then have "y = (x \<squnion> y)" by (simp add: le.join_connection)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   402
    then have "\<phi> y = (\<phi> x \<squnion>' \<phi> y)" by (simp add: hom_join [symmetric])
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   403
    then show "\<phi> x \<preceq> \<phi> y" by (simp add: le'.join_connection)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   404
  qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   405
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   406
text {* Theorems and other declarations --- syntax, in particular ---
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   407
  from the locale @{text order_preserving} are now active in @{text
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   408
  lattice_hom}, for example
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   409
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   410
  @{thm [locale=lattice_hom, source] le'.less_le_trans}:
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   411
  @{thm [locale=lattice_hom] le'.less_le_trans}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   412
  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   413
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   414
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   415
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   416
section {* Further Reading *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   417
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   418
text {* More information on locales and their interpretation is
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   419
  available.  For the locale hierarchy of import and interpretation
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   420
  dependencies see \cite{Ballarin2006a}; interpretations in theories
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   421
  and proofs are covered in \cite{Ballarin2006b}.  In the latter, we
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   422
  show how interpretation in proofs enables to reason about families
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   423
  of algebraic structures, which cannot be expressed with locales
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   424
  directly.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   425
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   426
  Haftmann and Wenzel \cite{HaftmannWenzel2007} overcome a restriction
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   427
  of axiomatic type classes through a combination with locale
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   428
  interpretation.  The result is a Haskell-style class system with a
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   429
  facility to generate Haskell code.  Classes are sufficient for
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   430
  simple specifications with a single type parameter.  The locales for
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   431
  orders and lattices presented in this tutorial fall into this
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   432
  category.  Order preserving maps, homomorphisms and vector spaces,
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   433
  on the other hand, do not.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   434
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   435
  The original work of Kamm\"uller on locales \cite{KammullerEtAl1999}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   436
  may be of interest from a historical perspective.  The mathematical
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   437
  background on orders and lattices is taken from Jacobson's textbook
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   438
  on algebra \cite[Chapter~8]{Jacobson1985}.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   439
  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   440
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   441
text {*
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   442
\begin{table}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   443
\hrule
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   444
\vspace{2ex}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   445
\begin{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   446
\begin{tabular}{l>$c<$l}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   447
  \multicolumn{3}{l}{Miscellaneous} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   448
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   449
  \textit{attr-name} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   450
  & \textit{name} $|$ \textit{attribute} $|$
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   451
    \textit{name} \textit{attribute} \\
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   452
  \textit{qualifier} & ::=
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   453
  & \textit{name} [``\textbf{!}''] \\[2ex]
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   454
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   455
  \multicolumn{3}{l}{Context Elements} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   456
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   457
  \textit{fixes} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   458
  & \textit{name} [ ``\textbf{::}'' \textit{type} ]
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   459
    [ ``\textbf{(}'' \textbf{structure} ``\textbf{)}'' $|$
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   460
    \textit{mixfix} ] \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   461
\begin{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   462
  \textit{constrains} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   463
  & \textit{name} ``\textbf{::}'' \textit{type} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   464
\end{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   465
  \textit{assumes} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   466
  & [ \textit{attr-name} ``\textbf{:}'' ] \textit{proposition} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   467
\begin{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   468
  \textit{defines} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   469
  & [ \textit{attr-name} ``\textbf{:}'' ] \textit{proposition} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   470
  \textit{notes} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   471
  & [ \textit{attr-name} ``\textbf{=}'' ]
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   472
    ( \textit{qualified-name} [ \textit{attribute} ] )$^+$ \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   473
\end{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   474
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   475
  \textit{element} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   476
  & \textbf{fixes} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   477
\begin{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   478
  & |
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   479
  & \textbf{constrains} \textit{constrains}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   480
    ( \textbf{and} \textit{constrains} )$^*$ \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   481
\end{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   482
  & |
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   483
  & \textbf{assumes} \textit{assumes} ( \textbf{and} \textit{assumes} )$^*$ \\[2ex]
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   484
%\begin{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   485
%  & |
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   486
%  & \textbf{defines} \textit{defines} ( \textbf{and} \textit{defines} )$^*$ \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   487
%  & |
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   488
%  & \textbf{notes} \textit{notes} ( \textbf{and} \textit{notes} )$^*$ \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   489
%\end{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   490
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   491
  \multicolumn{3}{l}{Locale Expressions} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   492
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   493
  \textit{pos-insts} & ::=
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   494
  & ( \textit{term} $|$ ``\textbf{\_}'' )$^*$ \\
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   495
  \textit{named-insts} & ::=
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   496
  & \textbf{where} \textit{name} ``\textbf{=}'' \textit{term}
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   497
  ( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   498
  \textit{instance} & ::=
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   499
  & [ \textit{qualifier} \textbf{:} ]
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   500
    \textit{qualified-name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   501
  \textit{expression}  & ::= 
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   502
  & \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   503
    [ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex]
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   504
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   505
  \multicolumn{3}{l}{Declaration of Locales} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   506
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   507
  \textit{locale} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   508
  & \textit{element}$^+$ \\
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   509
  & | & \textit{expression} [ ``\textbf{+}'' \textit{element}$^+$ ] \\
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   510
  \textit{toplevel} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   511
  & \textbf{locale} \textit{name} [ ``\textbf{=}''
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   512
    \textit{locale} ] \\[2ex]
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   513
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   514
  \multicolumn{3}{l}{Interpretation} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   515
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   516
  \textit{equation} & ::= & [ \textit{attr-name} ``\textbf{:}'' ]
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   517
    \textit{prop} \\
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   518
  \textit{equations} & ::= &  \textbf{where} \textit{equation} ( \textbf{and}
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   519
    \textit{equation} )$^*$  \\
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   520
  \textit{toplevel} & ::=
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   521
  & \textbf{sublocale} \textit{name} ( ``$<$'' $|$
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   522
    ``$\subseteq$'' ) \textit{expression} \textit{proof} \\
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   523
  & |
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   524
  & \textbf{interpretation}
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   525
    \textit{expression} [ \textit{equations} ] \textit{proof} \\
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   526
  & |
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   527
  & \textbf{interpret}
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   528
    \textit{expression} \textit{proof} \\[2ex]
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   529
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   530
  \multicolumn{3}{l}{Diagnostics} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   531
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   532
  \textit{toplevel} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   533
  & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{locale} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   534
  & | & \textbf{print\_locales} 
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   535
\end{tabular}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   536
\end{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   537
\hrule
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   538
\caption{Syntax of Locale Commands (abrigded).}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   539
\label{tab:commands}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   540
\end{table}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   541
  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   542
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   543
text {* \textbf{Acknowledgements.}  Alexander Krauss, Tobias Nipkow,
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   544
  Christian Sternagel and Makarius Wenzel have made useful comments on
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   545
  a draft of this document. *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   546
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   547
end