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