src/HOL/ex/LocaleTest2.thy
author urbanc
Tue Jun 05 09:56:19 2007 +0200 (2007-06-05)
changeset 23243 a37d3e6e8323
parent 23219 87ad6e8a5f2c
child 23919 af871d13e320
permissions -rw-r--r--
included Class.thy in the compiling process for Nominal/Examples
ballarin@22657
     1
(*  Title:      HOL/ex/LocaleTest2.thy
ballarin@22657
     2
    ID:         $Id$
ballarin@22657
     3
    Author:     Clemens Ballarin
ballarin@22657
     4
    Copyright (c) 2007 by Clemens Ballarin
ballarin@22657
     5
ballarin@22657
     6
More regression tests for locales.
ballarin@22657
     7
Definitions are less natural in FOL, since there is no selection operator.
ballarin@22657
     8
Hence we do them in HOL, not in the main test suite for locales:
ballarin@22657
     9
FOL/ex/LocaleTest.thy
ballarin@22657
    10
*)
ballarin@22657
    11
ballarin@22657
    12
header {* Test of Locale Interpretation *}
ballarin@22657
    13
ballarin@22657
    14
theory LocaleTest2
ballarin@22657
    15
imports Main
ballarin@22657
    16
begin
ballarin@22657
    17
ballarin@22657
    18
ML {* set quick_and_dirty *}    (* allow for thm command in batch mode *)
ballarin@22657
    19
ML {* set show_hyps *}
ballarin@22657
    20
ML {* set show_sorts *}
ballarin@22657
    21
wenzelm@23219
    22
wenzelm@23219
    23
subsection {* Interpretation of Defined Concepts *}
ballarin@22657
    24
ballarin@22657
    25
text {* Naming convention for global objects: prefixes D and d *}
ballarin@22657
    26
ballarin@22657
    27
(* Group example with defined operation inv *)
ballarin@22657
    28
ballarin@22657
    29
locale Dsemi =
ballarin@22657
    30
  fixes prod (infixl "**" 65)
ballarin@22657
    31
  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
ballarin@22657
    32
ballarin@22657
    33
locale Dmonoid = Dsemi +
ballarin@22657
    34
  fixes one
ballarin@22657
    35
  assumes lone: "one ** x = x"
ballarin@22657
    36
    and rone: "x ** one = x"
ballarin@22657
    37
ballarin@22657
    38
definition (in Dmonoid)
ballarin@22657
    39
  inv where "inv(x) == THE y. x ** y = one & y ** x = one"
ballarin@22657
    40
ballarin@22657
    41
lemma (in Dmonoid) inv_unique:
ballarin@22657
    42
  assumes eq: "y ** x = one" "x ** y' = one"
ballarin@22657
    43
  shows "y = y'"
ballarin@22657
    44
proof -
ballarin@22657
    45
  from eq have "y = y ** (x ** y')" by (simp add: rone)
ballarin@22657
    46
  also have "... = (y ** x) ** y'" by (simp add: assoc)
ballarin@22657
    47
  also from eq have "... = y'" by (simp add: lone)
ballarin@22657
    48
  finally show ?thesis .
ballarin@22657
    49
qed
ballarin@22657
    50
ballarin@22657
    51
locale Dgrp = Dmonoid +
ballarin@22657
    52
  assumes linv_ex: "EX y. y ** x = one"
ballarin@22657
    53
    and rinv_ex: "EX y. x ** y = one"
ballarin@22657
    54
ballarin@22657
    55
lemma (in Dgrp) linv:
ballarin@22657
    56
  "inv x ** x = one"
ballarin@22657
    57
apply (unfold inv_def)
ballarin@22657
    58
apply (insert rinv_ex [where x = x])
ballarin@22657
    59
apply (insert linv_ex [where x = x])
ballarin@22657
    60
apply (erule exE) apply (erule exE)
ballarin@22657
    61
apply (rule theI2)
ballarin@22657
    62
apply rule apply assumption
ballarin@22657
    63
apply (frule inv_unique, assumption)
ballarin@22657
    64
apply simp
ballarin@22657
    65
apply (rule inv_unique)
ballarin@22657
    66
apply fast+
ballarin@22657
    67
done
ballarin@22657
    68
ballarin@22657
    69
lemma (in Dgrp) rinv:
ballarin@22657
    70
  "x ** inv x = one"
ballarin@22657
    71
apply (unfold inv_def)
ballarin@22657
    72
apply (insert rinv_ex [where x = x])
ballarin@22657
    73
apply (insert linv_ex [where x = x])
ballarin@22657
    74
apply (erule exE) apply (erule exE)
ballarin@22657
    75
apply (rule theI2)
ballarin@22657
    76
apply rule apply assumption
ballarin@22657
    77
apply (frule inv_unique, assumption)
ballarin@22657
    78
apply simp
ballarin@22657
    79
apply (rule inv_unique)
ballarin@22657
    80
apply fast+
ballarin@22657
    81
done
ballarin@22657
    82
ballarin@22657
    83
lemma (in Dgrp) lcancel:
ballarin@22657
    84
  "x ** y = x ** z <-> y = z"
ballarin@22657
    85
proof
ballarin@22657
    86
  assume "x ** y = x ** z"
ballarin@22657
    87
  then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
ballarin@22657
    88
  then show "y = z" by (simp add: lone linv)
ballarin@22657
    89
qed simp
ballarin@22657
    90
ballarin@22657
    91
interpretation Dint: Dmonoid ["op +" "0::int"]
ballarin@22657
    92
  where "Dmonoid.inv (op +) (0::int)" = "uminus"
ballarin@22657
    93
proof -
ballarin@22657
    94
  show "Dmonoid (op +) (0::int)" by unfold_locales auto
ballarin@22657
    95
  note Dint = this (* should have this as an assumption in further goals *)
ballarin@22657
    96
  {
ballarin@22657
    97
    fix x
ballarin@22657
    98
    have "Dmonoid.inv (op +) (0::int) x = - x"
ballarin@22657
    99
      by (auto simp: Dmonoid.inv_def [OF Dint])
ballarin@22657
   100
  }
ballarin@22657
   101
  then show "Dmonoid.inv (op +) (0::int) == uminus"
ballarin@22657
   102
    by (rule_tac eq_reflection) (fast intro: ext)
ballarin@22657
   103
qed
ballarin@22657
   104
ballarin@22657
   105
thm Dmonoid.inv_def Dint.inv_def
ballarin@22657
   106
ballarin@22657
   107
lemma "- x \<equiv> THE y. x + y = 0 \<and> y + x = (0::int)"
ballarin@22657
   108
  apply (rule Dint.inv_def) done
ballarin@22657
   109
ballarin@22657
   110
interpretation Dclass: Dmonoid ["op +" "0::'a::ab_group_add"]
ballarin@22657
   111
  where "Dmonoid.inv (op +) (0::'a::ab_group_add)" = "uminus"
ballarin@22657
   112
proof -
ballarin@22757
   113
  show "Dmonoid (op +) (0::'a::ab_group_add)" by unfold_locales auto
ballarin@22657
   114
  note Dclass = this (* should have this as an assumption in further goals *)
ballarin@22657
   115
  {
ballarin@22657
   116
    fix x
ballarin@22757
   117
    have "Dmonoid.inv (op +) (0::'a::ab_group_add) x = - x"
ballarin@22657
   118
      by (auto simp: Dmonoid.inv_def [OF Dclass] equals_zero_I [symmetric])
ballarin@22657
   119
  }
ballarin@22757
   120
  then show "Dmonoid.inv (op +) (0::'a::ab_group_add) == uminus"
ballarin@22657
   121
    by (rule_tac eq_reflection) (fast intro: ext)
ballarin@22657
   122
qed
ballarin@22657
   123
ballarin@22657
   124
interpretation Dclass: Dgrp ["op +" "0::'a::ring"]
ballarin@22657
   125
apply unfold_locales
ballarin@22657
   126
apply (rule_tac x="-x" in exI) apply simp
ballarin@22657
   127
apply (rule_tac x="-x" in exI) apply simp
ballarin@22657
   128
done
ballarin@22657
   129
ballarin@22657
   130
(* Equation for inverse from Dclass: Dmonoid effective. *)
ballarin@22657
   131
ballarin@22657
   132
thm Dclass.linv
ballarin@22657
   133
lemma "-x + x = (0::'a::ring)" apply (rule Dclass.linv) done
ballarin@22657
   134
ballarin@22657
   135
(* Equations have effect in "subscriptions" *)
ballarin@22657
   136
ballarin@22657
   137
(* In the same module *)
ballarin@22657
   138
ballarin@22657
   139
lemma (in Dmonoid) trivial:
ballarin@22657
   140
  "inv one = inv one"
ballarin@22657
   141
  by rule
ballarin@22657
   142
ballarin@22657
   143
thm Dclass.trivial
ballarin@22657
   144
ballarin@22657
   145
(* Inherited: interpretation *)
ballarin@22657
   146
ballarin@22657
   147
lemma (in Dgrp) inv_inv:
ballarin@22657
   148
  "inv (inv x) = x"
ballarin@22657
   149
proof -
ballarin@22657
   150
  have "inv x ** inv (inv x) = inv x ** x"
ballarin@22657
   151
    by (simp add: linv rinv)
ballarin@22657
   152
  then show ?thesis by (simp add: lcancel)
ballarin@22657
   153
qed
ballarin@22657
   154
ballarin@22657
   155
thm Dclass.inv_inv
ballarin@22657
   156
lemma "- (- x) = (x::'a::ring)"
ballarin@22657
   157
  apply (rule Dclass.inv_inv) done
ballarin@22657
   158
ballarin@22657
   159
end