doc-src/Locales/Locales/Examples3.thy
author ballarin
Tue, 31 Mar 2009 21:25:08 +0200
changeset 30826 a53f4872400e
parent 30782 38e477e8524f
child 31748 530596c997da
permissions -rw-r--r--
Improvements to the text.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     1
theory Examples3
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     2
imports Examples
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     3
begin
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     4
subsection {* Third Version: Local Interpretation *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     5
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     6
text {* In the above example, the fact that @{text \<le>} is a partial
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     7
  order for the natural numbers was used in the proof of the
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     8
  second goal.  In general, proofs of the equations may involve
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     9
  theorems implied by the fact the assumptions of the instantiated
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    10
  locale hold for the instantiating structure.  If these theorems have
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    11
  been shown abstractly in the locale they can be made available
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    12
  conveniently in the context through an auxiliary local interpretation (keyword
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    13
  \isakeyword{interpret}).  This interpretation is inside the proof of the global
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    14
  interpretation.  The third revision of the example illustrates this.  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    15
30780
c3f1e8a9e0b5 Default mode of qualifiers in locale commands.
ballarin
parents: 30751
diff changeset
    16
interpretation %visible nat: partial_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
30782
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
    17
  where nat_less_eq: "partial_order.less op \<le> (x::nat) y = (x < y)"
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    18
proof -
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    19
  show "partial_order (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    20
    by unfold_locales auto
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
    21
  then interpret nat: partial_order "op \<le> :: [nat, nat] \<Rightarrow> bool" .
30580
cc5a55d7a5be Updated chapters 1-5 to locale reimplementation.
ballarin
parents: 30393
diff changeset
    22
  show "partial_order.less op \<le> (x::nat) y = (x < y)"
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    23
    unfolding nat.less_def by auto
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    24
qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    25
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
    26
text {* The inner interpretation does not require an elaborate new
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
    27
  proof, it is immediate from the preceding fact and proved with
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
    28
  ``.''.  It enriches the local proof context by the very theorems
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
    29
  also obtained in the interpretation from Section~\ref{sec:po-first},
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
    30
  and @{text nat.less_def} may directly be used to unfold the
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
    31
  definition.  Theorems from the local interpretation disappear after
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
    32
  leaving the proof context --- that is, after the closing
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
    33
  \isakeyword{qed} --- and are then replaced by those with the desired
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
    34
  substitutions of the strict order.  *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    35
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    36
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    37
subsection {* Further Interpretations *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    38
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    39
text {* Further interpretations are necessary to reuse theorems from
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    40
  the other locales.  In @{text lattice} the operations @{text \<sqinter>} and
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    41
  @{text \<squnion>} are substituted by @{term "min :: nat \<Rightarrow> nat \<Rightarrow> nat"} and
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    42
  @{term "max :: nat \<Rightarrow> nat \<Rightarrow> nat"}.  The entire proof for the
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    43
  interpretation is reproduced in order to give an example of a more
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    44
  elaborate interpretation proof.  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    45
30780
c3f1e8a9e0b5 Default mode of qualifiers in locale commands.
ballarin
parents: 30751
diff changeset
    46
interpretation %visible nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
30782
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
    47
  where "partial_order.less op \<le> (x::nat) y = (x < y)"
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
    48
    and nat_meet_eq: "lattice.meet op \<le> (x::nat) y = min x y"
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
    49
    and nat_join_eq: "lattice.join op \<le> (x::nat) y = max x y"
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    50
proof -
30782
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
    51
  show lattice: "lattice (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    52
    txt {* We have already shown that this is a partial order, *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    53
    apply unfold_locales
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    54
    txt {* hence only the lattice axioms remain to be shown: @{subgoals
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    55
      [display]}  After unfolding @{text is_inf} and @{text is_sup}, *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    56
    apply (unfold nat.is_inf_def nat.is_sup_def)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    57
    txt {* the goals become @{subgoals [display]} which can be solved
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    58
      by Presburger arithmetic. *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    59
    by arith+
30782
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
    60
  txt {* For the first of the equations, we refer to the theorem
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
    61
  shown in the previous interpretation. *}
30782
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
    62
  show "partial_order.less op \<le> (x::nat) y = (x < y)"
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
    63
    by (rule nat_less_eq)
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
    64
  txt {* In order to show the remaining equations, we put ourselves in a
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    65
    situation where the lattice theorems can be used in a convenient way. *}
30782
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
    66
  from lattice 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
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
    73
text {* Next follows that @{text \<le>} is a total order. *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    74
30780
c3f1e8a9e0b5 Default mode of qualifiers in locale commands.
ballarin
parents: 30751
diff changeset
    75
interpretation %visible nat: total_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
30782
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
    76
  where "partial_order.less op \<le> (x::nat) y = (x < y)"
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
    77
    and "lattice.meet op \<le> (x::nat) y = min x y"
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
    78
    and "lattice.join op \<le> (x::nat) y = max x y"
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
    79
proof -
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
    80
  show "total_order (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
    81
    by unfold_locales arith
30782
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
    82
qed (rule nat_less_eq nat_meet_eq nat_join_eq)+
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
    83
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
    84
text {* Since the locale hierarchy reflects that total
30782
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
    85
  orders are distributive lattices, an explicit interpretation of
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
    86
  distributive lattices for the order relation on natural numbers is
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
    87
  only necessary for mapping the definitions to the right operators on
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
    88
  @{typ nat}. *}
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
    89
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
    90
interpretation %visible nat: distrib_lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
    91
  where "partial_order.less op \<le> (x::nat) y = (x < y)"
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
    92
    and "lattice.meet op \<le> (x::nat) y = min x y"
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
    93
    and "lattice.join op \<le> (x::nat) y = max x y"
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
    94
  by unfold_locales [1] (rule nat_less_eq nat_meet_eq nat_join_eq)+
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    95
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    96
text {* Theorems that are available in the theory at this point are shown in
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    97
  Table~\ref{tab:nat-lattice}.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    98
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    99
\begin{table}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   100
\hrule
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   101
\vspace{2ex}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   102
\begin{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   103
\begin{tabular}{l}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   104
  @{thm [source] nat.less_def} from locale @{text partial_order}: \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   105
  \quad @{thm nat.less_def} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   106
  @{thm [source] nat.meet_left} from locale @{text lattice}: \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   107
  \quad @{thm nat.meet_left} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   108
  @{thm [source] nat.join_distr} from locale @{text distrib_lattice}: \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   109
  \quad @{thm nat.join_distr} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   110
  @{thm [source] nat.less_total} from locale @{text total_order}: \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   111
  \quad @{thm nat.less_total}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   112
\end{tabular}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   113
\end{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   114
\hrule
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   115
\caption{Interpreted theorems for @{text \<le>} on the natural numbers.}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   116
\label{tab:nat-lattice}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   117
\end{table}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   118
  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   119
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   120
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   121
subsection {* Lattice @{text "dvd"} on @{typ nat} *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   122
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   123
text {* Divisibility on the natural numbers is a distributive lattice
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   124
  but not a total order.  Interpretation again proceeds
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   125
  incrementally. *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   126
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   127
interpretation nat_dvd: partial_order "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   128
  where nat_dvd_less_eq:
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   129
    "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   130
proof -
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   131
  show "partial_order (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   132
    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
   133
  then interpret nat_dvd: partial_order "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" .
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   134
  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
   135
    apply (unfold nat_dvd.less_def)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   136
    apply auto
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   137
    done
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   138
qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   139
30580
cc5a55d7a5be Updated chapters 1-5 to locale reimplementation.
ballarin
parents: 30393
diff changeset
   140
text {* Note that in Isabelle/HOL there is no symbol for strict
cc5a55d7a5be Updated chapters 1-5 to locale reimplementation.
ballarin
parents: 30393
diff changeset
   141
  divisibility.  Instead, interpretation substitutes @{term "x dvd y \<and>
cc5a55d7a5be Updated chapters 1-5 to locale reimplementation.
ballarin
parents: 30393
diff changeset
   142
  x \<noteq> y"}.  *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   143
30780
c3f1e8a9e0b5 Default mode of qualifiers in locale commands.
ballarin
parents: 30751
diff changeset
   144
interpretation nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
30782
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
   145
  where "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
   146
    and nat_dvd_meet_eq: "lattice.meet op dvd = gcd"
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
   147
    and nat_dvd_join_eq: "lattice.join op dvd = lcm"
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   148
proof -
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   149
  show "lattice (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   150
    apply unfold_locales
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   151
    apply (unfold nat_dvd.is_inf_def nat_dvd.is_sup_def)
27595
3ac9e3cd1fa3 curried gcd
haftmann
parents: 27503
diff changeset
   152
    apply (rule_tac x = "gcd x y" in exI)
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   153
    apply auto [1]
27595
3ac9e3cd1fa3 curried gcd
haftmann
parents: 27503
diff changeset
   154
    apply (rule_tac x = "lcm x y" in exI)
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   155
    apply (auto intro: lcm_dvd1 lcm_dvd2 lcm_least)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   156
    done
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   157
  then interpret nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" .
30782
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
   158
  show "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
   159
    by (rule nat_dvd_less_eq)
27595
3ac9e3cd1fa3 curried gcd
haftmann
parents: 27503
diff changeset
   160
  show "lattice.meet op dvd = gcd"
3ac9e3cd1fa3 curried gcd
haftmann
parents: 27503
diff changeset
   161
    apply (auto simp add: expand_fun_eq)
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   162
    apply (unfold nat_dvd.meet_def)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   163
    apply (rule the_equality)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   164
    apply (unfold nat_dvd.is_inf_def)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   165
    by auto
27595
3ac9e3cd1fa3 curried gcd
haftmann
parents: 27503
diff changeset
   166
  show "lattice.join op dvd = lcm"
3ac9e3cd1fa3 curried gcd
haftmann
parents: 27503
diff changeset
   167
    apply (auto simp add: expand_fun_eq)
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   168
    apply (unfold nat_dvd.join_def)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   169
    apply (rule the_equality)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   170
    apply (unfold nat_dvd.is_sup_def)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   171
    by (auto intro: lcm_dvd1 lcm_dvd2 lcm_least)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   172
qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   173
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   174
text {* Equations @{thm [source] nat_dvd_meet_eq} and @{thm [source]
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   175
  nat_dvd_join_eq} are used in the main part the subsequent
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   176
  interpretation. *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   177
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   178
(*
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   179
definition
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   180
  is_lcm :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   181
  "is_lcm p m n \<longleftrightarrow> m dvd p \<and> n dvd p \<and>
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   182
    (\<forall>d. m dvd d \<longrightarrow> n dvd d \<longrightarrow> p dvd d)"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   183
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   184
lemma is_gcd: "is_lcm (lcm (m, n)) m n"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   185
  by (simp add: is_lcm_def lcm_least)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   186
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   187
lemma gcd_lcm_distr_lemma:
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   188
  "[| 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
   189
apply (unfold is_gcd_def is_lcm_def dvd_def)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   190
apply (clarsimp simp: mult_ac)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   191
apply (blast intro: mult_is_0)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   192
thm mult_is_0 [THEN iffD1]
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   193
*)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   194
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   195
lemma %invisible gcd_lcm_distr:
27595
3ac9e3cd1fa3 curried gcd
haftmann
parents: 27503
diff changeset
   196
  "gcd x (lcm y z) = lcm (gcd x y) (gcd x z)" sorry
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   197
30780
c3f1e8a9e0b5 Default mode of qualifiers in locale commands.
ballarin
parents: 30751
diff changeset
   198
interpretation %visible nat_dvd:
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   199
  distrib_lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
30782
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
   200
  where "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
   201
    and "lattice.meet op dvd = gcd"
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
   202
    and "lattice.join op dvd = lcm"
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
   203
proof -
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
   204
  show "distrib_lattice (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)"
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
   205
    apply unfold_locales
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
   206
    txt {* @{subgoals [display]} *}
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
   207
    apply (unfold nat_dvd_meet_eq nat_dvd_join_eq)
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
   208
    txt {* @{subgoals [display]} *}
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
   209
    apply (rule gcd_lcm_distr)
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
   210
    done
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
   211
qed (rule nat_dvd_less_eq nat_dvd_meet_eq nat_dvd_join_eq)+
27063
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 {*
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   237
  The syntax of the interpretation commands is shown in
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   238
  Table~\ref{tab:commands}.  The grammar refers to
30580
cc5a55d7a5be Updated chapters 1-5 to locale reimplementation.
ballarin
parents: 30393
diff changeset
   239
  \textit{expression}, which stands for a \emph{locale} expression.
cc5a55d7a5be Updated chapters 1-5 to locale reimplementation.
ballarin
parents: 30393
diff changeset
   240
  Locale expressions are discussed in the following section.
27063
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
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   256
  \emph{locale expression}, which enables to combine locales
30750
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   257
  and instantiate parameters.  A locale expression is a sequence of
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   258
  locale \emph{instances} followed by an optional \isakeyword{for}
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   259
  clause.  Each instance consists of a locale reference, which may be
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   260
  preceded by a qualifer and succeeded by instantiations of the
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   261
  parameters of that locale.  Instantiations may be either positional
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   262
  or through explicit mappings of parameters to arguments.
30750
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   263
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   264
  Using a locale expression, a locale for order
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   265
  preserving maps can be declared in the following way.  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   266
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   267
  locale order_preserving =
30750
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   268
    le: partial_order le + le': partial_order le'
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   269
      for le (infixl "\<sqsubseteq>" 50) and le' (infixl "\<preceq>" 50) +
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   270
    fixes \<phi> :: "'a \<Rightarrow> 'b"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   271
    assumes hom_le: "x \<sqsubseteq> y \<Longrightarrow> \<phi> x \<preceq> \<phi> y"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   272
30750
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   273
text {* The second and third line contain the expression --- two
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   274
  instances of the partial order locale where the parameter is
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   275
  instantiated to @{text le}
30750
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   276
  and @{text le'}, respectively.  The \isakeyword{for} clause consists
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   277
  of parameter declarations and is similar to the context element
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   278
  \isakeyword{fixes}.  The notable difference is that the
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   279
  \isakeyword{for} clause is part of the expression, and only
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   280
  parameters defined in the expression may occur in its instances.
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   281
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   282
  Instances define \emph{morphisms} on locales.  Their effect on the
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   283
  parameters is lifted to terms, propositions and theorems in the
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   284
  canonical way,
30750
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   285
  and thus to the assumptions and conclusions of a locale.  The
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   286
  assumption of a locale expression is the conjunction of the
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   287
  assumptions of the instances.  The conclusions of a sequence of
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   288
  instances are obtained by appending the conclusions of the
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   289
  instances in the order of the sequence.
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   290
30750
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   291
  The qualifiers in the expression are already a familiar concept from
30780
c3f1e8a9e0b5 Default mode of qualifiers in locale commands.
ballarin
parents: 30751
diff changeset
   292
  the \isakeyword{interpretation} command
c3f1e8a9e0b5 Default mode of qualifiers in locale commands.
ballarin
parents: 30751
diff changeset
   293
  (Section~\ref{sec:po-first}).  Here, they serve to distinguish names
c3f1e8a9e0b5 Default mode of qualifiers in locale commands.
ballarin
parents: 30751
diff changeset
   294
  (in particular theorem names) for the two partial orders within the
c3f1e8a9e0b5 Default mode of qualifiers in locale commands.
ballarin
parents: 30751
diff changeset
   295
  locale.  Qualifiers in the \isakeyword{locale} command (and in
c3f1e8a9e0b5 Default mode of qualifiers in locale commands.
ballarin
parents: 30751
diff changeset
   296
  \isakeyword{sublocale}) default to optional --- that is, they need
c3f1e8a9e0b5 Default mode of qualifiers in locale commands.
ballarin
parents: 30751
diff changeset
   297
  not occur in references to the qualified names.  Here are examples
c3f1e8a9e0b5 Default mode of qualifiers in locale commands.
ballarin
parents: 30751
diff changeset
   298
  of theorems in locale @{text order_preserving}: *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   299
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   300
context %invisible order_preserving begin
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   301
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   302
text {*
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   303
  @{thm [source] le.less_le_trans}: @{thm le.less_le_trans}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   304
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   305
  @{thm [source] hom_le}: @{thm hom_le}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   306
  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   307
30750
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   308
text {* The theorems for the partial order @{text \<preceq>}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   309
  are qualified by @{text le'}.  For example, @{thm [source]
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   310
  le'.less_le_trans}: @{thm [display, indent=2] le'.less_le_trans} *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   311
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   312
end %invisible
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   313
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   314
text {* This example reveals that there is no infix syntax for the
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   315
  strict operation associated with @{text \<preceq>}.  This can be declared
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   316
  through an abbreviation.  *}
27063
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
30393
aa6f42252bf6 replaced old locale option by proper "text (in locale)";
wenzelm
parents: 29568
diff changeset
   321
text (in order_preserving) {* Now the theorem is displayed nicely as
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   322
  @{thm [source]  le'.less_le_trans}:
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   323
  @{thm [display, indent=2] le'.less_le_trans} *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   324
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   325
text (in order_preserving)  {* Qualifiers not only apply to theorem names, but also to names
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   326
  introduced by definitions and abbreviations.  For example, in @{text
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   327
  partial_order} the name @{text less} abbreviates @{term
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   328
  "partial_order.less le"}.  Therefore, in @{text order_preserving}
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   329
  the qualified name @{text le.less} abbreviates @{term
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   330
  "partial_order.less le"} and @{text le'.less} abbreviates @{term
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   331
  "partial_order.less le'"}.  Hence, the equation in the abbreviation
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   332
  above could have been written more concisely as @{text "less' \<equiv>
30750
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   333
  le'.less"}. *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   334
30750
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   335
text {* Readers may find the declaration of locale @{text
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   336
  order_preserving} a little awkward, because the declaration and
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   337
  concrete syntax for @{text le} from @{text partial_order} are
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   338
  repeated in the declaration of @{text order_preserving}.  Locale
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   339
  expressions provide a convenient short hand for this.  A parameter
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   340
  in an instance is \emph{untouched} if no instantiation term is
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   341
  provided for it.  In positional instantiations, a parameter position
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   342
  may be skipped with an underscore, and it is allowed to give fewer
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   343
  instantiation terms than the instantiated locale's number of
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   344
  parameters.  In named instantiations, instantiation pairs for
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   345
  certain parameters may simply be omitted.  Untouched parameters are
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   346
  implicitly declared by the locale expression and with their concrete
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   347
  syntax.  In the sequence of parameters, they appear before the
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   348
  parameters from the \isakeyword{for} clause.
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   349
30750
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   350
  The following locales illustrate this.  A map @{text \<phi>} is a
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   351
  lattice homomorphism if it preserves meet and join. *}
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   352
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   353
  locale lattice_hom =
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   354
    le: lattice + le': lattice le' for le' (infixl "\<preceq>" 50) +
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   355
    fixes \<phi>
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   356
    assumes hom_meet: "\<phi> (x \<sqinter> y) = le'.meet (\<phi> x) (\<phi> y)"
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   357
      and hom_join: "\<phi> (x \<squnion> y) = le'.join (\<phi> x) (\<phi> y)"
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   358
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   359
  abbreviation (in lattice_hom)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   360
    meet' (infixl "\<sqinter>''" 50) where "meet' \<equiv> le'.meet"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   361
  abbreviation (in lattice_hom)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   362
    join' (infixl "\<squnion>''" 50) where "join' \<equiv> le'.join"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   363
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   364
text {* A homomorphism is an endomorphism if both orders coincide. *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   365
30750
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   366
  locale lattice_end = lattice_hom _ le
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   367
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   368
text {* In this declaration, the first parameter of @{text
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   369
  lattice_hom}, @{text le}, is untouched and is then used to instantiate
30780
c3f1e8a9e0b5 Default mode of qualifiers in locale commands.
ballarin
parents: 30751
diff changeset
   370
  the second parameter.  Its concrete syntax is preserved. *}
30750
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   371
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   372
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   373
text {* The inheritance diagram of the situation we have now is shown
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   374
  in Figure~\ref{fig:hom}, where the dashed line depicts an
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   375
  interpretation which is introduced below.  Renamings are
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   376
  indicated by $\sqsubseteq \mapsto \preceq$ etc.  The expression
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   377
  imported by @{text lattice_end} identifies the first and second
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   378
  parameter of @{text lattice_hom}.  By looking at the inheritance diagram it would seem
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   379
  that two identical copies of each of the locales @{text
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   380
  partial_order} and @{text lattice} are imported.  This is not the
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   381
  case!  Inheritance paths with identical morphisms are detected and
27503
a019d6568a3c fix typo
huffman
parents: 27081
diff changeset
   382
  the conclusions of the respective locales appear only once.
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   383
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   384
\begin{figure}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   385
\hrule \vspace{2ex}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   386
\begin{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   387
\begin{tikzpicture}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   388
  \node (o) at (0,0) {@{text partial_order}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   389
  \node (oh) at (1.5,-2) {@{text order_preserving}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   390
  \node (oh1) at (1.5,-0.7) {$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   391
  \node (oh2) at (0,-1.3) {$\scriptscriptstyle \sqsubseteq \mapsto \preceq$};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   392
  \node (l) at (-1.5,-2) {@{text lattice}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   393
  \node (lh) at (0,-4) {@{text lattice_hom}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   394
  \node (lh1) at (0,-2.7) {$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   395
  \node (lh2) at (-1.5,-3.3) {$\scriptscriptstyle \sqsubseteq \mapsto \preceq$};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   396
  \node (le) at (0,-6) {@{text lattice_end}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   397
  \node (le1) at (0,-4.8)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   398
    [anchor=west]{$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   399
  \node (le2) at (0,-5.2)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   400
    [anchor=west]{$\scriptscriptstyle \preceq \mapsto \sqsubseteq$};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   401
  \draw (o) -- (l);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   402
  \draw[dashed] (oh) -- (lh);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   403
  \draw (lh) -- (le);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   404
  \draw (o) .. controls (oh1.south west) .. (oh);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   405
  \draw (o) .. controls (oh2.north east) .. (oh);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   406
  \draw (l) .. controls (lh1.south west) .. (lh);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   407
  \draw (l) .. controls (lh2.north east) .. (lh);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   408
\end{tikzpicture}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   409
\end{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   410
\hrule
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   411
\caption{Hierarchy of Homomorphism Locales.}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   412
\label{fig:hom}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   413
\end{figure}
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
text {* It can be shown easily that a lattice homomorphism is order
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   417
  preserving.  As the final example of this section, a locale
30750
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   418
  interpretation is used to assert this: *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   419
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   420
  sublocale lattice_hom \<subseteq> order_preserving proof unfold_locales
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   421
    fix x y
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   422
    assume "x \<sqsubseteq> y"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   423
    then have "y = (x \<squnion> y)" by (simp add: le.join_connection)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   424
    then have "\<phi> y = (\<phi> x \<squnion>' \<phi> y)" by (simp add: hom_join [symmetric])
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   425
    then show "\<phi> x \<preceq> \<phi> y" by (simp add: le'.join_connection)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   426
  qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   427
30393
aa6f42252bf6 replaced old locale option by proper "text (in locale)";
wenzelm
parents: 29568
diff changeset
   428
text (in lattice_hom) {*
aa6f42252bf6 replaced old locale option by proper "text (in locale)";
wenzelm
parents: 29568
diff changeset
   429
  Theorems and other declarations --- syntax, in particular --- from
aa6f42252bf6 replaced old locale option by proper "text (in locale)";
wenzelm
parents: 29568
diff changeset
   430
  the locale @{text order_preserving} are now active in @{text
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   431
  lattice_hom}, for example
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   432
  @{thm [source] hom_le}:
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   433
  @{thm [display, indent=2] hom_le}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   434
  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   435
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   436
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   437
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   438
section {* Further Reading *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   439
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   440
text {* More information on locales and their interpretation is
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   441
  available.  For the locale hierarchy of import and interpretation
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   442
  dependencies see \cite{Ballarin2006a}; interpretations in theories
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   443
  and proofs are covered in \cite{Ballarin2006b}.  In the latter, we
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   444
  show how interpretation in proofs enables to reason about families
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   445
  of algebraic structures, which cannot be expressed with locales
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   446
  directly.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   447
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   448
  Haftmann and Wenzel \cite{HaftmannWenzel2007} overcome a restriction
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   449
  of axiomatic type classes through a combination with locale
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   450
  interpretation.  The result is a Haskell-style class system with a
30750
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   451
  facility to generate ML and Haskell code.  Classes are sufficient for
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   452
  simple specifications with a single type parameter.  The locales for
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   453
  orders and lattices presented in this tutorial fall into this
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   454
  category.  Order preserving maps, homomorphisms and vector spaces,
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   455
  on the other hand, do not.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   456
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   457
  The original work of Kamm\"uller on locales \cite{KammullerEtAl1999}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   458
  may be of interest from a historical perspective.  The mathematical
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   459
  background on orders and lattices is taken from Jacobson's textbook
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   460
  on algebra \cite[Chapter~8]{Jacobson1985}.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   461
  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   462
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   463
text {*
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   464
\begin{table}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   465
\hrule
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   466
\vspace{2ex}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   467
\begin{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   468
\begin{tabular}{l>$c<$l}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   469
  \multicolumn{3}{l}{Miscellaneous} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   470
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   471
  \textit{attr-name} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   472
  & \textit{name} $|$ \textit{attribute} $|$
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   473
    \textit{name} \textit{attribute} \\
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   474
  \textit{qualifier} & ::=
30751
36a255c2e428 Corrections to locale syntax.
ballarin
parents: 30750
diff changeset
   475
  & \textit{name} [``\textbf{?}'' $|$ ``\textbf{!}''] \\[2ex]
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   476
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   477
  \multicolumn{3}{l}{Context Elements} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   478
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   479
  \textit{fixes} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   480
  & \textit{name} [ ``\textbf{::}'' \textit{type} ]
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   481
    [ ``\textbf{(}'' \textbf{structure} ``\textbf{)}'' $|$
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   482
    \textit{mixfix} ] \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   483
\begin{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   484
  \textit{constrains} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   485
  & \textit{name} ``\textbf{::}'' \textit{type} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   486
\end{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   487
  \textit{assumes} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   488
  & [ \textit{attr-name} ``\textbf{:}'' ] \textit{proposition} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   489
\begin{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   490
  \textit{defines} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   491
  & [ \textit{attr-name} ``\textbf{:}'' ] \textit{proposition} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   492
  \textit{notes} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   493
  & [ \textit{attr-name} ``\textbf{=}'' ]
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   494
    ( \textit{qualified-name} [ \textit{attribute} ] )$^+$ \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   495
\end{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   496
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   497
  \textit{element} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   498
  & \textbf{fixes} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   499
\begin{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   500
  & |
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   501
  & \textbf{constrains} \textit{constrains}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   502
    ( \textbf{and} \textit{constrains} )$^*$ \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   503
\end{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   504
  & |
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   505
  & \textbf{assumes} \textit{assumes} ( \textbf{and} \textit{assumes} )$^*$ \\[2ex]
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   506
%\begin{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   507
%  & |
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   508
%  & \textbf{defines} \textit{defines} ( \textbf{and} \textit{defines} )$^*$ \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   509
%  & |
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   510
%  & \textbf{notes} \textit{notes} ( \textbf{and} \textit{notes} )$^*$ \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   511
%\end{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   512
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   513
  \multicolumn{3}{l}{Locale Expressions} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   514
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   515
  \textit{pos-insts} & ::=
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   516
  & ( \textit{term} $|$ ``\textbf{\_}'' )$^*$ \\
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   517
  \textit{named-insts} & ::=
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   518
  & \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
   519
  ( \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
   520
  \textit{instance} & ::=
30751
36a255c2e428 Corrections to locale syntax.
ballarin
parents: 30750
diff changeset
   521
  & [ \textit{qualifier} ``\textbf{:}'' ]
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   522
    \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
   523
  \textit{expression}  & ::= 
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   524
  & \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   525
    [ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex]
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   526
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   527
  \multicolumn{3}{l}{Declaration of Locales} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   528
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   529
  \textit{locale} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   530
  & \textit{element}$^+$ \\
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   531
  & | & \textit{expression} [ ``\textbf{+}'' \textit{element}$^+$ ] \\
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   532
  \textit{toplevel} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   533
  & \textbf{locale} \textit{name} [ ``\textbf{=}''
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   534
    \textit{locale} ] \\[2ex]
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   535
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   536
  \multicolumn{3}{l}{Interpretation} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   537
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   538
  \textit{equation} & ::= & [ \textit{attr-name} ``\textbf{:}'' ]
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   539
    \textit{prop} \\
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   540
  \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
   541
    \textit{equation} )$^*$  \\
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   542
  \textit{toplevel} & ::=
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   543
  & \textbf{sublocale} \textit{name} ( ``$<$'' $|$
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   544
    ``$\subseteq$'' ) \textit{expression} \textit{proof} \\
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   545
  & |
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   546
  & \textbf{interpretation}
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   547
    \textit{expression} [ \textit{equations} ] \textit{proof} \\
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   548
  & |
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   549
  & \textbf{interpret}
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   550
    \textit{expression} \textit{proof} \\[2ex]
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   551
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   552
  \multicolumn{3}{l}{Diagnostics} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   553
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   554
  \textit{toplevel} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   555
  & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{locale} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   556
  & | & \textbf{print\_locales} 
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   557
\end{tabular}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   558
\end{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   559
\hrule
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   560
\caption{Syntax of Locale Commands.}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   561
\label{tab:commands}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   562
\end{table}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   563
  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   564
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   565
text {* \textbf{Acknowledgements.}  Alexander Krauss, Tobias Nipkow,
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   566
  Christian Sternagel and Makarius Wenzel have made useful comments on
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   567
  a draft of this document. *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   568
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   569
end