src/HOL/ex/Locales.thy

more explanations on advanced syntax;

(*  Title:      HOL/ex/Locales.thy
    ID:         $Id$
    Author:     Markus Wenzel, LMU Muenchen
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
*)

header {* Basic use of locales in Isabelle/Isar *}

theory Locales = Main:

text {*
  Locales provide a mechanism for encapsulating local contexts.  While
  the original version by Florian Kamm\"uller refers to the raw
  meta-logic, the present one of Isabelle/Isar builds on top of the
  rich infrastructure of Isar proof contexts.  Subsequently, we
  demonstrate basic use of locales to model mathematical structures
  (by the inevitable group theory example).
*}

text_raw {*
  \newcommand{\isasyminv}{\isasyminverse}
  \newcommand{\isasymone}{\isamath{1}}
  \newcommand{\isasymIN}{\isatext{\isakeyword{in}}}
*}


subsection {* Local contexts as mathematical structures *}

text {*
  The following definitions of @{text group} and @{text abelian_group}
  simply encapsulate local parameters (with private syntax) and
  assumptions; local definitions may be given as well, but are not
  shown here.
*}

locale group =
  fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<cdot>" 70)
    and inv :: "'a \<Rightarrow> 'a"    ("(_\<inv>)" [1000] 999)
    and one :: 'a    ("\<one>")
  assumes assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
    and left_inv: "x\<inv> \<cdot> x = \<one>"
    and left_one: "\<one> \<cdot> x = x"

locale abelian_group = group +
  assumes commute: "x \<cdot> y = y \<cdot> x"

text {*
  \medskip We may now prove theorems within a local context, just by
  including a directive ``@{text "(\<IN> name)"}'' in the goal
  specification.  The final result will be stored within the named
  locale; a second copy is exported to the enclosing theory context.
*}

theorem (in group)
  right_inv: "x \<cdot> x\<inv> = \<one>"
proof -
  have "x \<cdot> x\<inv> = \<one> \<cdot> (x \<cdot> x\<inv>)" by (simp only: left_one)
  also have "\<dots> = \<one> \<cdot> x \<cdot> x\<inv>" by (simp only: assoc)
  also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv> \<cdot> x \<cdot> x\<inv>" by (simp only: left_inv)
  also have "\<dots> = (x\<inv>)\<inv> \<cdot> (x\<inv> \<cdot> x) \<cdot> x\<inv>" by (simp only: assoc)
  also have "\<dots> = (x\<inv>)\<inv> \<cdot> \<one> \<cdot> x\<inv>" by (simp only: left_inv)
  also have "\<dots> = (x\<inv>)\<inv> \<cdot> (\<one> \<cdot> x\<inv>)" by (simp only: assoc)
  also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv>" by (simp only: left_one)
  also have "\<dots> = \<one>" by (simp only: left_inv)
  finally show ?thesis .
qed

theorem (in group)
  right_one: "x \<cdot> \<one> = x"
proof -
  have "x \<cdot> \<one> = x \<cdot> (x\<inv> \<cdot> x)" by (simp only: left_inv)
  also have "\<dots> = x \<cdot> x\<inv> \<cdot> x" by (simp only: assoc)
  also have "\<dots> = \<one> \<cdot> x" by (simp only: right_inv)
  also have "\<dots> = x" by (simp only: left_one)
  finally show ?thesis .
qed

text {*
  \medskip Apart from the named locale context we may also refer to
  further ad-hoc elements (parameters, assumptions, etc.); these are
  discharged when the proof is finished.
*}

theorem (in group)
  (assumes eq: "e \<cdot> x = x")
  one_equality: "\<one> = e"
proof -
  have "\<one> = x \<cdot> x\<inv>" by (simp only: right_inv)
  also have "\<dots> = (e \<cdot> x) \<cdot> x\<inv>" by (simp only: eq)
  also have "\<dots> = e \<cdot> (x \<cdot> x\<inv>)" by (simp only: assoc)
  also have "\<dots> = e \<cdot> \<one>" by (simp only: right_inv)
  also have "\<dots> = e" by (simp only: right_one)
  finally show ?thesis .
qed

theorem (in group)
  (assumes eq: "x' \<cdot> x = \<one>")
  inv_equality: "x\<inv> = x'"
proof -
  have "x\<inv> = \<one> \<cdot> x\<inv>" by (simp only: left_one)
  also have "\<dots> = (x' \<cdot> x) \<cdot> x\<inv>" by (simp only: eq)
  also have "\<dots> = x' \<cdot> (x \<cdot> x\<inv>)" by (simp only: assoc)
  also have "\<dots> = x' \<cdot> \<one>" by (simp only: right_inv)
  also have "\<dots> = x'" by (simp only: right_one)
  finally show ?thesis .
qed

theorem (in group)
  inv_prod: "(x \<cdot> y)\<inv> = y\<inv> \<cdot> x\<inv>"
proof (rule inv_equality)
  show "(y\<inv> \<cdot> x\<inv>) \<cdot> (x \<cdot> y) = \<one>"
  proof -
    have "(y\<inv> \<cdot> x\<inv>) \<cdot> (x \<cdot> y) = (y\<inv> \<cdot> (x\<inv> \<cdot> x)) \<cdot> y" by (simp only: assoc)
    also have "\<dots> = (y\<inv> \<cdot> \<one>) \<cdot> y" by (simp only: left_inv)
    also have "\<dots> = y\<inv> \<cdot> y" by (simp only: right_one)
    also have "\<dots> = \<one>" by (simp only: left_inv)
    finally show ?thesis .
  qed
qed

text {*
  \medskip Results are automatically propagated through the hierarchy
  of locales.  Below we establish a trivial fact of commutative
  groups, while referring both to theorems of @{text group} and the
  characteristic assumption of @{text abelian_group}.
*}

theorem (in abelian_group)
  inv_prod': "(x \<cdot> y)\<inv> = x\<inv> \<cdot> y\<inv>"
proof -
  have "(x \<cdot> y)\<inv> = y\<inv> \<cdot> x\<inv>" by (rule inv_prod)
  also have "\<dots> = x\<inv> \<cdot> y\<inv>" by (rule commute)
  finally show ?thesis .
qed

text {*
  \medskip Some further facts of general group theory follow.
*}

theorem (in group)
  inv_inv: "(x\<inv>)\<inv> = x"
proof (rule inv_equality)
  show "x \<cdot> x\<inv> = \<one>" by (simp only: right_inv)
qed

theorem (in group)
  (assumes eq: "x\<inv> = y\<inv>")
  inv_inject: "x = y"
proof -
  have "x = x \<cdot> \<one>" by (simp only: right_one)
  also have "\<dots> = x \<cdot> (y\<inv> \<cdot> y)" by (simp only: left_inv)
  also have "\<dots> = x \<cdot> (x\<inv> \<cdot> y)" by (simp only: eq)
  also have "\<dots> = (x \<cdot> x\<inv>) \<cdot> y" by (simp only: assoc)
  also have "\<dots> = \<one> \<cdot> y" by (simp only: right_inv)
  also have "\<dots> = y" by (simp only: left_one)
  finally show ?thesis .
qed

text {*
  \bigskip We see that this representation of structures as local
  contexts is rather light-weight and convenient to use for abstract
  reasoning.  Here the ``components'' (the group operations) have been
  exhibited directly as context parameters; logically this corresponds
  to a curried predicate definition.  Occasionally, this
  ``externalized'' version of the informal idea of classes of tuple
  structures may cause some inconveniences, especially in
  meta-theoretical studies (involving functors from groups to groups,
  for example).

  Another drawback of the naive approach above is that concrete syntax
  will get lost on any kind of operation on the locale itself (such as
  renaming, copying, or instantiation).  Whenever the particular
  terminology of local parameters is affected the associated syntax
  would have to be changed as well, which is hard to achieve formally.
*}


subsection {* Referencing explicit structures implicitly *}

text {*
  The issue of multiple parameters raised above may be easily
  addressed by stating properties over a record of group operations,
  instead of the individual constituents.
*}

record 'a group =
  prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
  inv :: "'a \<Rightarrow> 'a"
  one :: 'a

text {*
  Now concrete syntax essentially needs refer to record selections;
  this is possible by giving defined operations with private syntax
  within the locale (e.g.\ see appropriate examples by Kamm\"uller).

  In the subsequent formulation of group structures we go one step
  further by using \emph{implicit} references to the underlying
  abstract entity.  To this end we define global syntax, which is
  translated to refer to the ``current'' structure at hand, denoted by
  the dummy item ``@{text \<struct>}'' according to the builtin syntax
  mechanism for locales.
*}

syntax
  "_prod" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<cdot>" 70)
  "_inv" :: "'a \<Rightarrow> 'a"    ("(_\<inv>)" [1000] 999)
  "_one" :: 'a    ("\<one>")
translations
  "x \<cdot> y"  \<rightleftharpoons>  "prod \<struct> x y"
  "x\<inv>"  \<rightleftharpoons>  "inv \<struct> x"
  "\<one>"  \<rightleftharpoons>  "one \<struct>"

text {*
  The following locale definition introduces a single parameter, which
  is declared as ``\isakeyword{structure}''.
*}

locale group_struct =
  fixes G :: "'a group"    (structure)
  assumes assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
    and left_inv: "x\<inv> \<cdot> x = \<one>"
    and left_one: "\<one> \<cdot> x = x"

text {*
  In its context the dummy ``@{text \<struct>}'' refers to this very
  parameter, independently of the present naming.  We may now proceed
  to prove results within @{text group_struct} just as before for
  @{text group}.  Proper treatment of ``@{text \<struct>}'' is hidden in
  concrete syntax, so the proof text is exactly the same as for @{text
  group} given before.
*}

theorem (in group_struct)
  right_inv: "x \<cdot> x\<inv> = \<one>"
proof -
  have "x \<cdot> x\<inv> = \<one> \<cdot> (x \<cdot> x\<inv>)" by (simp only: left_one)
  also have "\<dots> = \<one> \<cdot> x \<cdot> x\<inv>" by (simp only: assoc)
  also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv> \<cdot> x \<cdot> x\<inv>" by (simp only: left_inv)
  also have "\<dots> = (x\<inv>)\<inv> \<cdot> (x\<inv> \<cdot> x) \<cdot> x\<inv>" by (simp only: assoc)
  also have "\<dots> = (x\<inv>)\<inv> \<cdot> \<one> \<cdot> x\<inv>" by (simp only: left_inv)
  also have "\<dots> = (x\<inv>)\<inv> \<cdot> (\<one> \<cdot> x\<inv>)" by (simp only: assoc)
  also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv>" by (simp only: left_one)
  also have "\<dots> = \<one>" by (simp only: left_inv)
  finally show ?thesis .
qed

theorem (in group_struct)
  right_one: "x \<cdot> \<one> = x"
proof -
  have "x \<cdot> \<one> = x \<cdot> (x\<inv> \<cdot> x)" by (simp only: left_inv)
  also have "\<dots> = x \<cdot> x\<inv> \<cdot> x" by (simp only: assoc)
  also have "\<dots> = \<one> \<cdot> x" by (simp only: right_inv)
  also have "\<dots> = x" by (simp only: left_one)
  finally show ?thesis .
qed

text {*
  \medskip Several implicit structures may be active at the same time
  (say up to 3 in practice).  The concrete syntax facility for locales
  actually maintains indexed dummies @{text "\<struct>\<^sub>1"}, @{text
  "\<struct>\<^sub>2"}, @{text "\<struct>\<^sub>3"}, \dots (@{text \<struct>} is the same as
  @{text "\<struct>\<^sub>1"}).  So we are able to provide concrete syntax to
  cover the 2nd and 3rd group structure as well.
*}

syntax
  "_prod'" :: "'a \<Rightarrow> index \<Rightarrow> 'a \<Rightarrow> 'a"    ("(_ \<cdot>_/ _)" [70, 1000, 71] 70)
  "_inv'" :: "'a \<Rightarrow> index \<Rightarrow> 'a"    ("(_\<inv>_)" [1000] 999)
  "_one'" :: "index \<Rightarrow> 'a"    ("\<one>_")
translations
  "x \<cdot>\<^sub>2 y"  \<rightleftharpoons>  "prod \<struct>\<^sub>2 x y"
  "x \<cdot>\<^sub>3 y"  \<rightleftharpoons>  "prod \<struct>\<^sub>3 x y"
  "x\<inv>\<^sub>2"  \<rightleftharpoons>  "inv \<struct>\<^sub>2 x"
  "x\<inv>\<^sub>3"  \<rightleftharpoons>  "inv \<struct>\<^sub>3 x"
  "\<one>\<^sub>2"  \<rightleftharpoons>  "one \<struct>\<^sub>2"
  "\<one>\<^sub>3"  \<rightleftharpoons>  "one \<struct>\<^sub>3"

text {*
  \medskip The following synthetic example demonstrates how to refer
  to several structures of type @{text group} succinctly; one might
  also think of working with renamed versions of the @{text
  group_struct} locale above.
*}

lemma
  (fixes G :: "'a group" (structure)
    and H :: "'a group" (structure))
  True
proof
  have "x \<cdot> y \<cdot> \<one> = prod G (prod G x y) (one G)" ..
  have "x \<cdot>\<^sub>2 y \<cdot>\<^sub>2 \<one>\<^sub>2 = prod H (prod H x y) (one H)" ..
  have "x \<cdot> \<one>\<^sub>2 = prod G x (one H)" ..
qed

text {*
  \medskip As a minor drawback of this advanced technique we require
  slightly more work to setup abstract and concrete syntax properly
  (but only once in the beginning).  The resulting casual mode of
  writing @{text "x \<cdot> y"} for @{text "prod G x y"} etc.\ mimics common
  practice of informal mathematics quite nicely, while using a simple
  and robust formal representation.
*}

end