doc-src/Locales/Locales/Examples3.thy
author ballarin
Thu, 15 Oct 2009 22:22:08 +0200
changeset 32982 40810d98f4c9
parent 32981 0114e04a0d64
child 32983 a6914429005b
permissions -rw-r--r--
Changed part of the examples to int.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     1
theory Examples3
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
     2
imports Examples "~~/src/HOL/Number_Theory/UniqueFactorization"
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     3
begin
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
     4
hide %invisible const Lattices.lattice
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
     5
  (* imported again through Number_Theory *)
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
     6
text {* \vspace{-5ex} *}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
     7
subsection {* Third Version: Local Interpretation
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
     8
  \label{sec:local-interpretation} *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     9
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    10
text {* In the above example, the fact that @{term "op \<le>"} is a partial
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    11
  order for the integers was used in the second goal to
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    12
  discharge the premise in the definition of @{text "op \<sqsubset>"}.  In
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    13
  general, proofs of the equations not only may involve definitions
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    14
  fromthe interpreted locale but arbitrarily complex arguments in the
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    15
  context of the locale.  Therefore is would be convenient to have the
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    16
  interpreted locale conclusions temporary available in the proof.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    17
  This can be achieved by a locale interpretation in the proof body.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    18
  The command for local interpretations is \isakeyword{interpret}.  We
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    19
  repeat the example from the previous section to illustrate this. *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    20
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    21
  interpretation %visible int: partial_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    22
    where "partial_order.less op \<le> (x::int) y = (x < y)"
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    23
  proof -
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    24
    show "partial_order (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)"
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    25
      by unfold_locales auto
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    26
    then interpret int: partial_order "op \<le> :: [int, int] \<Rightarrow> bool" .
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    27
    show "partial_order.less op \<le> (x::int) y = (x < y)"
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    28
      unfolding int.less_def by auto
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    29
  qed
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    30
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    31
text {* The inner interpretation is immediate from the preceding fact
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    32
  and proved by assumption (Isar short hand ``.'').  It enriches the
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    33
  local proof context by the theorems
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
    34
  also obtained in the interpretation from Section~\ref{sec:po-first},
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    35
  and @{text int.less_def} may directly be used to unfold the
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
    36
  definition.  Theorems from the local interpretation disappear after
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    37
  leaving the proof context --- that is, after the closing a
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    38
  \isakeyword{next} or \isakeyword{qed} statement. *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    39
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    40
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    41
subsection {* Further Interpretations *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    42
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    43
text {* Further interpretations are necessary for
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    44
  the other locales.  In @{text lattice} the operations @{text \<sqinter>} and
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    45
  @{text \<squnion>} are substituted by @{term "min :: int \<Rightarrow> int \<Rightarrow> int"} and
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    46
  @{term "max :: int \<Rightarrow> int \<Rightarrow> int"}.  The entire proof for the
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    47
  interpretation is reproduced to give an example of a more
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    48
  elaborate interpretation proof.  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    49
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    50
  interpretation %visible int: lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    51
    where "lattice.meet op \<le> (x::int) y = min x y"
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    52
      and "lattice.join op \<le> (x::int) y = max x y"
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    53
  proof -
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    54
    show "lattice (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)"
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    55
      txt {* \normalsize We have already shown that this is a partial
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    56
	order, *}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    57
      apply unfold_locales
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    58
      txt {* \normalsize hence only the lattice axioms remain to be
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    59
	shown: @{subgoals [display]}  After unfolding @{text is_inf} and
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    60
	@{text is_sup}, *}
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    61
      apply (unfold int.is_inf_def int.is_sup_def)
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    62
      txt {* \normalsize the goals become @{subgoals [display]}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    63
	This can be solved by Presburger arithmetic, which is contained
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    64
	in @{text arith}. *}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    65
      by arith+
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    66
    txt {* \normalsize In order to show the equations, we put ourselves
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    67
      in a situation where the lattice theorems can be used in a
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    68
      convenient way. *}
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    69
    then interpret int: lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool" .
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    70
    show "lattice.meet op \<le> (x::int) y = min x y"
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    71
      by (bestsimp simp: int.meet_def int.is_inf_def)
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    72
    show "lattice.join op \<le> (x::int) y = max x y"
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    73
      by (bestsimp simp: int.join_def int.is_sup_def)
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    74
  qed
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    75
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    76
text {* Next follows that @{text "op \<le>"} is a total order, again for
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    77
  the integers. *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    78
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    79
  interpretation %visible int: total_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    80
    by unfold_locales arith
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    81
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    82
text {* Theorems that are available in the theory at this point are shown in
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    83
  Table~\ref{tab:int-lattice}.  Two points are worth noting:
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    84
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    85
\begin{table}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    86
\hrule
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    87
\vspace{2ex}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    88
\begin{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    89
\begin{tabular}{l}
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    90
  @{thm [source] int.less_def} from locale @{text partial_order}: \\
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    91
  \quad @{thm int.less_def} \\
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    92
  @{thm [source] int.meet_left} from locale @{text lattice}: \\
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    93
  \quad @{thm int.meet_left} \\
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    94
  @{thm [source] int.join_distr} from locale @{text distrib_lattice}: \\
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    95
  \quad @{thm int.join_distr} \\
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    96
  @{thm [source] int.less_total} from locale @{text total_order}: \\
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    97
  \quad @{thm int.less_total}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    98
\end{tabular}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    99
\end{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   100
\hrule
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
   101
\caption{Interpreted theorems for @{text \<le>} on the integers.}
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
   102
\label{tab:int-lattice}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   103
\end{table}
32804
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 31960
diff changeset
   104
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 31960
diff changeset
   105
\begin{itemize}
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 31960
diff changeset
   106
\item
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   107
  Locale @{text distrib_lattice} was also interpreted.  Since the
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   108
  locale hierarcy reflects that total orders are distributive
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   109
  lattices, the interpretation of the latter was inserted
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   110
  automatically with the interpretation of the former.  In general,
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   111
  interpretation of a locale will also interpret all locales further
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   112
  up in the hierarchy, regardless whether imported or proved via the
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   113
  \isakeyword{sublocale} command.
32804
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 31960
diff changeset
   114
\item
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
   115
  Theorem @{thm [source] int.less_total} makes use of @{term "op <"}
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   116
  although an equation for the replacement of @{text "op \<sqsubset>"} was only
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   117
  given in the interpretation of @{text partial_order}.  These
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   118
  equations are pushed downwards the hierarchy for related
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   119
  interpretations --- that is, for interpretations that share the
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   120
  instance for parameters they have in common.
32804
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 31960
diff changeset
   121
\end{itemize}
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   122
  In the next section, the divisibility relation on the natural
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   123
  numbers will be explored.
27063
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
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   127
subsection {* Interpretations for Divisibility *}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   128
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   129
text {* In this section, further examples of interpretations are
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   130
  presented.  Impatient readers may skip this section at first
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   131
  reading.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   132
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   133
  Divisibility on the natural numbers is a distributive lattice
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   134
  but not a total order.  Interpretation again proceeds
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   135
  incrementally.  In order to distinguish divisibility from the order
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   136
  relation $\le$, we use the qualifier @{text nat_dvd} for
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   137
  divisibility. *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   138
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   139
  interpretation nat_dvd: partial_order "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   140
    where "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   141
  proof -
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   142
    show "partial_order (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)"
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   143
      by unfold_locales (auto simp: dvd_def)
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   144
    then interpret nat_dvd: partial_order "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" .
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   145
    show "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   146
      apply (unfold nat_dvd.less_def)
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   147
      apply auto
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   148
      done
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   149
  qed
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   150
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   151
text {* Note that in Isabelle/HOL there is no operator for strict
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   152
  divisibility.  Instead, we substitute @{term "x dvd y \<and> x \<noteq> y"}.  *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   153
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   154
  interpretation nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   155
    where nat_dvd_meet_eq:
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   156
	"lattice.meet (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = gcd"
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   157
      and nat_dvd_join_eq:
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   158
	"lattice.join (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = lcm"
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   159
  proof -
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   160
    show "lattice (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)"
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   161
      apply unfold_locales
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   162
      apply (unfold nat_dvd.is_inf_def nat_dvd.is_sup_def)
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   163
      apply (rule_tac x = "gcd x y" in exI)
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   164
      apply auto [1]
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   165
      apply (rule_tac x = "lcm x y" in exI)
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   166
      apply (auto intro: lcm_least_nat)
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   167
      done
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   168
    then interpret nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" .
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   169
    show "lattice.meet (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = gcd"
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   170
      apply (auto simp add: expand_fun_eq)
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   171
      apply (unfold nat_dvd.meet_def)
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   172
      apply (rule the_equality)
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   173
      apply (unfold nat_dvd.is_inf_def)
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   174
      by auto
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   175
    show "lattice.join (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = lcm"
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   176
      apply (auto simp add: expand_fun_eq)
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   177
      apply (unfold nat_dvd.join_def)
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   178
      apply (rule the_equality)
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   179
      apply (unfold nat_dvd.is_sup_def)
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   180
      apply (auto intro: lcm_least_nat iff: lcm_unique_nat)
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   181
      done
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   182
  qed
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   183
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   184
text {* The replacement equations @{thm [source] nat_dvd_meet_eq} and
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   185
  @{thm [source] nat_dvd_join_eq} are theorems of current theories.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   186
  They are named so that they can be used in the main part of the
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   187
  subsequent interpretation. *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   188
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   189
  interpretation %visible nat_dvd:
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   190
    distrib_lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   191
    apply unfold_locales
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   192
    txt {* \normalsize @{subgoals [display]}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   193
      Distributivity of lattice meet and join needs to be shown.  This is
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   194
      distributivity of gcd and lcm, as becomes apparent when unfolding
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   195
      the replacement equations from the previous interpretation: *}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   196
    unfolding nat_dvd_meet_eq nat_dvd_join_eq
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   197
    txt {* \normalsize @{subgoals [display]}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   198
      This is a result of number theory: *}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   199
    by (rule UniqueFactorization.gcd_lcm_distrib_nat)
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   200
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   201
text {* Theorems that are available in the theory after these
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   202
  interpretations are shown in Table~\ref{tab:nat-dvd-lattice}.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   203
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   204
\begin{table}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   205
\hrule
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   206
\vspace{2ex}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   207
\begin{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   208
\begin{tabular}{l}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   209
  @{thm [source] nat_dvd.less_def} from locale @{text partial_order}: \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   210
  \quad @{thm nat_dvd.less_def} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   211
  @{thm [source] nat_dvd.meet_left} from locale @{text lattice}: \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   212
  \quad @{thm nat_dvd.meet_left} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   213
  @{thm [source] nat_dvd.join_distr} from locale @{text distrib_lattice}: \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   214
  \quad @{thm nat_dvd.join_distr} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   215
\end{tabular}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   216
\end{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   217
\hrule
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   218
\caption{Interpreted theorems for @{text dvd} on the natural numbers.}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   219
\label{tab:nat-dvd-lattice}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   220
\end{table}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   221
  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   222
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   223
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   224
subsection {* Inspecting Interpretations of a Locale *}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   225
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   226
text {* The interpretations for a locale $n$ within the current
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   227
  theory may be inspected with \isakeyword{print\_interps}~$n$.  This
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   228
  prints the list of instances of $n$, for which interpretations exist.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   229
  For example, \isakeyword{print\_interps} @{term partial_order}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   230
  outputs the following:
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   231
\begin{alltt}
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
   232
  int! : partial_order "op \(\le\)"
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   233
  nat_dvd! : partial_order "op dvd"
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   234
\end{alltt}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   235
  The interpretation qualifiers on the left are decorated with an
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   236
  exclamation point, which means that they are mandatory.  Qualifiers
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   237
  can either be \emph{mandatory} or \emph{optional}, designated by
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   238
  ``!'' or ``?'' respectively.  Mandatory qualifiers must occur in a
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   239
  name reference while optional ones need not.  Mandatory qualifiers
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   240
  prevent accidental hiding of names, while optional qualifers can be
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   241
  more convenient to use.  For \isakeyword{interpretation}, the
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   242
  default for qualifiers without an explicit designator is ``!''.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   243
*}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   244
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   245
27077
f64166dd92f0 moved labels into actual sections;
wenzelm
parents: 27075
diff changeset
   246
section {* Locale Expressions \label{sec:expressions} *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   247
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   248
text {*
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   249
  A map @{term \<phi>} between partial orders @{text \<sqsubseteq>} and @{text \<preceq>}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   250
  is called order preserving if @{text "x \<sqsubseteq> y"} implies @{text "\<phi> x \<preceq>
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   251
  \<phi> y"}.  This situation is more complex than those encountered so
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   252
  far: it involves two partial orders, and it is desirable to use the
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   253
  existing locale for both.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   254
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   255
  A locale for order preserving maps requires three parameters: @{text
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   256
  le} (\isakeyword{infixl}~@{text \<sqsubseteq>}), @{text le'}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   257
  (\isakeyword{infixl}~@{text \<preceq>}) for the orders and @{text \<phi>} for the
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   258
  map.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   259
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   260
  In order to reuse the existing locale for partial orders, which has
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   261
  the single parameter @{text le}, it must be imported twice, once
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   262
  mapping its parameter to @{text le} (\isakeyword{infixl}~@{text \<sqsubseteq>})
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   263
  from the new locale and once to @{text le'}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   264
  (\isakeyword{infixl}~@{text \<preceq>}).  This can be achieved with a locale
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   265
  expression.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   266
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   267
  A \emph{locale expression} is a sequence of \emph{locale instances}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   268
  separated by ``$\textbf{+}$'' and followed by a \isakeyword{for}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   269
  clause.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   270
An instance has the following format:
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   271
\begin{quote}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   272
  \textit{qualifier} \textbf{:} \textit{locale-name}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   273
  \textit{parameter-instantiation}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   274
\end{quote}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   275
  We have already seen locale instances as arguments to
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   276
  \isakeyword{interpretation} in Section~\ref{sec:interpretation}.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   277
  The qualifier serves to disambiguate the names from different
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   278
  instances of the same locale.
30750
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   279
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   280
  Since the parameters @{text le} and @{text le'} are to be partial
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   281
  orders, our locale for order preserving maps will import the these
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   282
  instances:
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   283
\begin{alltt}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   284
  le: partial_order le
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   285
  le': partial_order le'
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   286
\end{alltt}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   287
  For matter of convenience we choose the parameter names also as
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   288
  qualifiers.  This is an arbitrary decision.  Technically, qualifiers
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   289
  and parameters are unrelated.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   290
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   291
  Having determined the instances, let us turn to the \isakeyword{for}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   292
  clause.  It serves to declare locale parameters in the same way as
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   293
  the context element \isakeyword{fixes} does.  Context elements can
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   294
  only occur after the import section, and therefore the parameters
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   295
  referred to inthe instances must be declared in the \isakeyword{for}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   296
  clause.%
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   297
\footnote{Since all parameters can be declared in the \isakeyword{for}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   298
  clause, the context element \isakeyword{fixes} is not needed in
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   299
  locales.  It is provided for compatibility with the long goals
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   300
  format, where the context element also occurs.}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   301
  The \isakeyword{for} clause is also where the syntax of these
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   302
  parameters is declared.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   303
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   304
  Two context elements for the map parameter @{text \<phi>} and the
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   305
  assumptions that it is order perserving complete the locale
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   306
  declaration. *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   307
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   308
  locale order_preserving =
30750
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   309
    le: partial_order le + le': partial_order le'
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   310
      for le (infixl "\<sqsubseteq>" 50) and le' (infixl "\<preceq>" 50) +
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   311
    fixes \<phi>
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   312
    assumes hom_le: "x \<sqsubseteq> y \<Longrightarrow> \<phi> x \<preceq> \<phi> y"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   313
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   314
text (in order_preserving) {* Here are examples of theorems that are
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   315
  available in the locale:
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   316
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   317
  @{thm [source] hom_le}: @{thm hom_le}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   318
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   319
  @{thm [source] le.less_le_trans}: @{thm le.less_le_trans}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   320
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   321
  @{thm [source] le'.less_le_trans}:
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   322
  @{thm [display, indent=2] le'.less_le_trans}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   323
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   324
  While there is infix syntax for the strict operation associated to
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   325
  @{term "op \<sqsubseteq>"}, there is none for the strict version of @{term
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   326
  "op \<preceq>"}.  The abbreviation @{text less} with its infix syntax is only
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   327
  available for the original instance it was declared for.  We may
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   328
  introduce the abbreviation @{text less'} with infix syntax @{text \<prec>}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   329
  with this declaration: *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   330
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   331
  abbreviation (in order_preserving)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   332
    less' (infixl "\<prec>" 50) where "less' \<equiv> partial_order.less le'"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   333
30393
aa6f42252bf6 replaced old locale option by proper "text (in locale)";
wenzelm
parents: 29568
diff changeset
   334
text (in order_preserving) {* Now the theorem is displayed nicely as
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   335
  @{thm [source]  le'.less_le_trans}:
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   336
  @{thm [display, indent=2] le'.less_le_trans} *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   337
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   338
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   339
subsection {* Default Instantiations and Implicit Parameters *}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   340
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   341
text {* It is possible to omit parameter instantiations in a locale
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   342
  expression.  In that case, the instantiation defaults to the name of
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   343
  the parameter itself.  That is, the locale expression @{text
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   344
  partial_order} is short for @{text "partial_order le"}, since the
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   345
  locale's single parameter is @{text le}.  We took advantage of this
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   346
  short hand in the \isakeyword{sublocale} declarations of
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   347
  Section~\ref{sec:changing-the-hierarchy}. *}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   348
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   349
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   350
text {* In a locale expression that occurs within a locale
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   351
  declaration, omitted parameters additionally extend the (possibly
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   352
  empty) \isakeyword{for} clause.
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   353
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   354
  The \isakeyword{for} clause is a
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   355
  general construct of Isabelle/Isar to mark names from the preceding
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   356
  declaration as ``arbitrary but fixed''.  This is necessary for
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   357
  example, if the name is already bound in a surrounding context.  In
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   358
  a locale expression, names occurring in parameter instantiations
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   359
  should be bound by a \isakeyword{for} clause whenever these names
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   360
  are not introduced elsewhere in the context --- for example, on the
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   361
  left hand side of a \isakeyword{sublocale} declaration.
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   362
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   363
  There is an exception to this rule in locale declarations, where the
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   364
  \isakeyword{for} clause servers to declare locale parameters.  Here,
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   365
  locale parameters for which no parameter instantiation is given are
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   366
  implicitly added, with their mixfix syntax, at the beginning of the
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   367
  \isakeyword{for} clause.  For example, in a locale declaration, the
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   368
  expression @{text partial_order} is short for
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   369
\begin{alltt}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   370
  partial_order le \isakeyword{for} le (\isakeyword{infixl} "\(\sqsubseteq\)" 50)\textrm{.}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   371
\end{alltt}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   372
  This short hand was used in the locale declarations of
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   373
  Section~\ref{sec:import}.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   374
 *}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   375
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   376
text{*
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   377
  The following locale declarations provide more examples.  A map
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   378
  @{text \<phi>} is a lattice homomorphism if it preserves meet and
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   379
  join. *}
30750
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   380
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   381
  locale lattice_hom =
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   382
    le: lattice + le': lattice le' for le' (infixl "\<preceq>" 50) +
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   383
    fixes \<phi>
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   384
    assumes hom_meet: "\<phi> (x \<sqinter> y) = le'.meet (\<phi> x) (\<phi> y)"
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   385
      and hom_join: "\<phi> (x \<squnion> y) = le'.join (\<phi> x) (\<phi> y)"
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   386
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   387
text {* We omit the parameter instantiation in the first instance of
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   388
  @{term lattice}.  This causes the parameter @{text le} to be added
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   389
  to the \isakeyword{for} clause, and the locale has parameters
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   390
  @{text le} and @{text le'}.
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   391
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   392
  Before turning to the second example, we complete the locale by
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   393
  provinding infix syntax for the meet and join operations of the
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   394
  second lattice.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   395
*}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   396
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   397
  context lattice_hom begin
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   398
  abbreviation meet' (infixl "\<sqinter>''" 50) where "meet' \<equiv> le'.meet"
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   399
  abbreviation join' (infixl "\<squnion>''" 50) where "join' \<equiv> le'.join"
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   400
  end
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   401
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   402
text {* The next example pushes the short hand facilities.  A
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   403
  homomorphism is an endomorphism if both orders coincide. *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   404
30750
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   405
  locale lattice_end = lattice_hom _ le
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   406
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   407
text {* The notation @{text _} enables to omit a parameter in a
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   408
  positional instantiation.  The omitted parameter, @{text le} becomes
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   409
  the parameter of the declared locale and is, in the following
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   410
  position used to instantiate the second parameter of @{text
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   411
  lattice_hom}.  The effect is that of identifying the first in second
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   412
  parameter of the homomorphism locale. *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   413
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   414
text {* The inheritance diagram of the situation we have now is shown
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   415
  in Figure~\ref{fig:hom}, where the dashed line depicts an
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   416
  interpretation which is introduced below.  Renamings are
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   417
  indicated by $\sqsubseteq \mapsto \preceq$ etc.  By looking at the
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   418
  inheritance diagram it would seem
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   419
  that two identical copies of each of the locales @{text
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   420
  partial_order} and @{text lattice} are imported by @{text
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   421
  lattice_end}.  This is not the case!  Inheritance paths with
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   422
  identical morphisms are automatically detected and
27503
a019d6568a3c fix typo
huffman
parents: 27081
diff changeset
   423
  the conclusions of the respective locales appear only once.
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   424
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   425
\begin{figure}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   426
\hrule \vspace{2ex}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   427
\begin{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   428
\begin{tikzpicture}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   429
  \node (o) at (0,0) {@{text partial_order}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   430
  \node (oh) at (1.5,-2) {@{text order_preserving}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   431
  \node (oh1) at (1.5,-0.7) {$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   432
  \node (oh2) at (0,-1.3) {$\scriptscriptstyle \sqsubseteq \mapsto \preceq$};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   433
  \node (l) at (-1.5,-2) {@{text lattice}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   434
  \node (lh) at (0,-4) {@{text lattice_hom}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   435
  \node (lh1) at (0,-2.7) {$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   436
  \node (lh2) at (-1.5,-3.3) {$\scriptscriptstyle \sqsubseteq \mapsto \preceq$};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   437
  \node (le) at (0,-6) {@{text lattice_end}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   438
  \node (le1) at (0,-4.8)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   439
    [anchor=west]{$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   440
  \node (le2) at (0,-5.2)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   441
    [anchor=west]{$\scriptscriptstyle \preceq \mapsto \sqsubseteq$};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   442
  \draw (o) -- (l);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   443
  \draw[dashed] (oh) -- (lh);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   444
  \draw (lh) -- (le);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   445
  \draw (o) .. controls (oh1.south west) .. (oh);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   446
  \draw (o) .. controls (oh2.north east) .. (oh);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   447
  \draw (l) .. controls (lh1.south west) .. (lh);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   448
  \draw (l) .. controls (lh2.north east) .. (lh);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   449
\end{tikzpicture}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   450
\end{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   451
\hrule
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   452
\caption{Hierarchy of Homomorphism Locales.}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   453
\label{fig:hom}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   454
\end{figure}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   455
  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   456
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   457
text {* It can be shown easily that a lattice homomorphism is order
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   458
  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
   459
  interpretation is used to assert this: *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   460
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   461
  sublocale lattice_hom \<subseteq> order_preserving proof unfold_locales
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   462
    fix x y
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   463
    assume "x \<sqsubseteq> y"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   464
    then have "y = (x \<squnion> y)" by (simp add: le.join_connection)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   465
    then have "\<phi> y = (\<phi> x \<squnion>' \<phi> y)" by (simp add: hom_join [symmetric])
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   466
    then show "\<phi> x \<preceq> \<phi> y" by (simp add: le'.join_connection)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   467
  qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   468
30393
aa6f42252bf6 replaced old locale option by proper "text (in locale)";
wenzelm
parents: 29568
diff changeset
   469
text (in lattice_hom) {*
aa6f42252bf6 replaced old locale option by proper "text (in locale)";
wenzelm
parents: 29568
diff changeset
   470
  Theorems and other declarations --- syntax, in particular --- from
aa6f42252bf6 replaced old locale option by proper "text (in locale)";
wenzelm
parents: 29568
diff changeset
   471
  the locale @{text order_preserving} are now active in @{text
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   472
  lattice_hom}, for example
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   473
  @{thm [source] hom_le}:
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   474
  @{thm [display, indent=2] hom_le}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   475
  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   476
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   477
(*
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   478
section {* Conditional Interpretation *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   479
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   480
  locale non_negative =
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   481
    fixes n :: int
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   482
    assumes non_negative: "0 \<le> n"
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   483
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   484
  interpretation partial_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   485
    where "partial_order.less op \<le> (x::int) y = (x < y)"
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   486
    sorry
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   487
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   488
  sublocale non_negative \<subseteq> order_preserving "op \<le>" "op \<le>" "\<lambda>i. n * i"
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   489
    apply unfold_locales using non_negative apply - by (rule mult_left_mono)
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   490
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   491
  interpretation lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   492
    where min_eq: "lattice.meet op \<le> (x::int) y = min x y"
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   493
      and max_eq: "lattice.join op \<le> (x::int) y = max x y"
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   494
    sorry
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   495
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   496
    apply unfold_locales unfolding is_inf_def is_sup_def by arith+
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   497
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   498
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   499
  sublocale non_negative \<subseteq> lattice_end "op \<le>" "\<lambda>i. n * i"
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   500
    apply unfold_locales unfolding min_eq max_eq apply (case_tac "x \<le> y")
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   501
    unfolding min_def apply auto apply arith
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   502
    apply (rule sym)
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   503
    apply (rule the_equality)
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   504
  proof
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   505
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   506
  locale fspace_po = partial_order
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   507
  sublocale fspace_po \<subseteq> fspace: partial_order "\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x"
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   508
(* fspace needed to disambiguate less etc *)
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   509
apply unfold_locales
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   510
apply auto
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   511
apply (rule) apply auto apply (blast intro: trans) done
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   512
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   513
*)
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   514
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   515
section {* Further Reading *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   516
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   517
text {* More information on locales and their interpretation is
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   518
  available.  For the locale hierarchy of import and interpretation
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   519
  dependencies see \cite{Ballarin2006a}; interpretations in theories
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   520
  and proofs are covered in \cite{Ballarin2006b}.  In the latter, I
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   521
  show how interpretation in proofs enables to reason about families
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   522
  of algebraic structures, which cannot be expressed with locales
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   523
  directly.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   524
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   525
  Haftmann and Wenzel \cite{HaftmannWenzel2007} overcome a restriction
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   526
  of axiomatic type classes through a combination with locale
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   527
  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
   528
  facility to generate ML and Haskell code.  Classes are sufficient for
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   529
  simple specifications with a single type parameter.  The locales for
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   530
  orders and lattices presented in this tutorial fall into this
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   531
  category.  Order preserving maps, homomorphisms and vector spaces,
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   532
  on the other hand, do not.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   533
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   534
  The locales reimplementation for Isabelle 2009 provides, among other
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   535
  improvements, a clean intergration with Isabelle/Isar's local theory
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   536
  mechnisms, which are described in \cite{HaftmannWenzel2009}.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   537
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   538
  The original work of Kamm\"uller on locales \cite{KammullerEtAl1999}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   539
  may be of interest from a historical perspective.  The mathematical
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   540
  background on orders and lattices is taken from Jacobson's textbook
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   541
  on algebra \cite[Chapter~8]{Jacobson1985}.
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   542
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   543
  The sources of this tutorial, which include all proofs, are
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   544
  available with the Isabelle distribution at
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   545
  \url{http://isabelle.in.tum.de}.
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   546
  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   547
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   548
text {*
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   549
\begin{table}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   550
\hrule
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   551
\vspace{2ex}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   552
\begin{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   553
\begin{tabular}{l>$c<$l}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   554
  \multicolumn{3}{l}{Miscellaneous} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   555
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   556
  \textit{attr-name} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   557
  & \textit{name} $|$ \textit{attribute} $|$
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   558
    \textit{name} \textit{attribute} \\
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   559
  \textit{qualifier} & ::=
30751
36a255c2e428 Corrections to locale syntax.
ballarin
parents: 30750
diff changeset
   560
  & \textit{name} [``\textbf{?}'' $|$ ``\textbf{!}''] \\[2ex]
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   561
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   562
  \multicolumn{3}{l}{Context Elements} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   563
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   564
  \textit{fixes} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   565
  & \textit{name} [ ``\textbf{::}'' \textit{type} ]
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   566
    [ ``\textbf{(}'' \textbf{structure} ``\textbf{)}'' $|$
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   567
    \textit{mixfix} ] \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   568
\begin{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   569
  \textit{constrains} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   570
  & \textit{name} ``\textbf{::}'' \textit{type} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   571
\end{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   572
  \textit{assumes} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   573
  & [ \textit{attr-name} ``\textbf{:}'' ] \textit{proposition} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   574
\begin{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   575
  \textit{defines} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   576
  & [ \textit{attr-name} ``\textbf{:}'' ] \textit{proposition} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   577
  \textit{notes} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   578
  & [ \textit{attr-name} ``\textbf{=}'' ]
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   579
    ( \textit{qualified-name} [ \textit{attribute} ] )$^+$ \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   580
\end{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   581
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   582
  \textit{element} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   583
  & \textbf{fixes} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   584
\begin{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   585
  & |
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   586
  & \textbf{constrains} \textit{constrains}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   587
    ( \textbf{and} \textit{constrains} )$^*$ \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   588
\end{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   589
  & |
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   590
  & \textbf{assumes} \textit{assumes} ( \textbf{and} \textit{assumes} )$^*$ \\[2ex]
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   591
%\begin{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   592
%  & |
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   593
%  & \textbf{defines} \textit{defines} ( \textbf{and} \textit{defines} )$^*$ \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   594
%  & |
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   595
%  & \textbf{notes} \textit{notes} ( \textbf{and} \textit{notes} )$^*$ \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   596
%\end{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   597
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   598
  \multicolumn{3}{l}{Locale Expressions} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   599
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   600
  \textit{pos-insts} & ::=
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   601
  & ( \textit{term} $|$ ``\textbf{\_}'' )$^*$ \\
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   602
  \textit{named-insts} & ::=
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   603
  & \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
   604
  ( \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
   605
  \textit{instance} & ::=
30751
36a255c2e428 Corrections to locale syntax.
ballarin
parents: 30750
diff changeset
   606
  & [ \textit{qualifier} ``\textbf{:}'' ]
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   607
    \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
   608
  \textit{expression}  & ::= 
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   609
  & \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   610
    [ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex]
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   611
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   612
  \multicolumn{3}{l}{Declaration of Locales} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   613
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   614
  \textit{locale} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   615
  & \textit{element}$^+$ \\
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   616
  & | & \textit{expression} [ ``\textbf{+}'' \textit{element}$^+$ ] \\
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   617
  \textit{toplevel} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   618
  & \textbf{locale} \textit{name} [ ``\textbf{=}''
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   619
    \textit{locale} ] \\[2ex]
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   620
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   621
  \multicolumn{3}{l}{Interpretation} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   622
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   623
  \textit{equation} & ::= & [ \textit{attr-name} ``\textbf{:}'' ]
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   624
    \textit{prop} \\
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   625
  \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
   626
    \textit{equation} )$^*$  \\
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   627
  \textit{toplevel} & ::=
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   628
  & \textbf{sublocale} \textit{name} ( ``$<$'' $|$
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   629
    ``$\subseteq$'' ) \textit{expression} \textit{proof} \\
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   630
  & |
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   631
  & \textbf{interpretation}
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   632
    \textit{expression} [ \textit{equations} ] \textit{proof} \\
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   633
  & |
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   634
  & \textbf{interpret}
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   635
    \textit{expression} \textit{proof} \\[2ex]
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   636
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   637
  \multicolumn{3}{l}{Diagnostics} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   638
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   639
  \textit{toplevel} & ::=
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   640
  & \textbf{print\_locales} \\
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   641
  & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{locale} \\
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   642
  & | & \textbf{print\_interps} \textit{locale}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   643
\end{tabular}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   644
\end{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   645
\hrule
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   646
\caption{Syntax of Locale Commands.}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   647
\label{tab:commands}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   648
\end{table}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   649
  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   650
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   651
text {* \textbf{Revision History.}  For the present third revision,
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   652
  which was completed in October 2009, much of the explanatory text
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   653
  has been rewritten.  In addition, inheritance of interpretation
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   654
  equations, which was not available for Isabelle 2009, but in the
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   655
  meantime has been implemented, is illustrated.  The second revision
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   656
  accommodates changes introduced by the locales reimplementation for
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   657
  Isabelle 2009.  Most notably, in complex specifications
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   658
  (\emph{locale expressions}) renaming has been generalised to
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   659
  instantiation.  *}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   660
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   661
text {* \textbf{Acknowledgements.}  Alexander Krauss, Tobias Nipkow,
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   662
  Randy Pollack, Christian Sternagel and Makarius Wenzel have made
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   663
  useful comments on earlier versions of this document. *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   664
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   665
end