src/HOL/ex/LocaleTest2.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 33657 a4179bf442d1
child 58889 5b7a9633cfa8
permissions -rw-r--r--
specialized specification: avoid trivial instances
ballarin@22657
     1
(*  Title:      HOL/ex/LocaleTest2.thy
ballarin@22657
     2
    Author:     Clemens Ballarin
ballarin@22657
     3
    Copyright (c) 2007 by Clemens Ballarin
ballarin@22657
     4
ballarin@22657
     5
More regression tests for locales.
ballarin@22657
     6
Definitions are less natural in FOL, since there is no selection operator.
ballarin@23919
     7
Hence we do them here in HOL, not in the main test suite for locales,
ballarin@23919
     8
which is FOL/ex/LocaleTest.thy
ballarin@22657
     9
*)
ballarin@22657
    10
ballarin@22657
    11
header {* Test of Locale Interpretation *}
ballarin@22657
    12
ballarin@22657
    13
theory LocaleTest2
haftmann@25592
    14
imports Main GCD
ballarin@22657
    15
begin
ballarin@22657
    16
ballarin@23919
    17
section {* Interpretation of Defined Concepts *}
ballarin@22657
    18
ballarin@22657
    19
text {* Naming convention for global objects: prefixes D and d *}
ballarin@22657
    20
ballarin@23919
    21
ballarin@23919
    22
subsection {* Lattices *}
ballarin@23919
    23
ballarin@23919
    24
text {* Much of the lattice proofs are from HOL/Lattice. *}
ballarin@23919
    25
ballarin@23919
    26
ballarin@23919
    27
subsubsection {* Definitions *}
ballarin@23919
    28
ballarin@23919
    29
locale dpo =
ballarin@23919
    30
  fixes le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>" 50)
ballarin@23919
    31
  assumes refl [intro, simp]: "x \<sqsubseteq> x"
nipkow@33657
    32
    and antisym [intro]: "[| x \<sqsubseteq> y; y \<sqsubseteq> x |] ==> x = y"
ballarin@23919
    33
    and trans [trans]: "[| x \<sqsubseteq> y; y \<sqsubseteq> z |] ==> x \<sqsubseteq> z"
ballarin@23919
    34
ballarin@23919
    35
begin
ballarin@23919
    36
ballarin@23919
    37
theorem circular:
ballarin@23919
    38
  "[| x \<sqsubseteq> y; y \<sqsubseteq> z; z \<sqsubseteq> x |] ==> x = y & y = z"
ballarin@23919
    39
  by (blast intro: trans)
ballarin@23919
    40
ballarin@23919
    41
definition
ballarin@23919
    42
  less :: "['a, 'a] => bool" (infixl "\<sqsubset>" 50)
ballarin@23919
    43
  where "(x \<sqsubset> y) = (x \<sqsubseteq> y & x ~= y)"
ballarin@23919
    44
ballarin@23919
    45
theorem abs_test:
ballarin@23919
    46
  "op \<sqsubset> = (%x y. x \<sqsubset> y)"
ballarin@23919
    47
  by simp
ballarin@23919
    48
ballarin@23919
    49
definition
ballarin@23919
    50
  is_inf :: "['a, 'a, 'a] => bool"
ballarin@23919
    51
  where "is_inf x y i = (i \<sqsubseteq> x \<and> i \<sqsubseteq> y \<and> (\<forall>z. z \<sqsubseteq> x \<and> z \<sqsubseteq> y \<longrightarrow> z \<sqsubseteq> i))"
ballarin@23919
    52
ballarin@23919
    53
definition
ballarin@23919
    54
  is_sup :: "['a, 'a, 'a] => bool"
ballarin@23919
    55
  where "is_sup x y s = (x \<sqsubseteq> s \<and> y \<sqsubseteq> s \<and> (\<forall>z. x \<sqsubseteq> z \<and> y \<sqsubseteq> z \<longrightarrow> s \<sqsubseteq> z))"
ballarin@23919
    56
ballarin@23919
    57
end
ballarin@23919
    58
ballarin@23919
    59
locale dlat = dpo +
ballarin@23919
    60
  assumes ex_inf: "EX inf. dpo.is_inf le x y inf"
ballarin@23919
    61
    and ex_sup: "EX sup. dpo.is_sup le x y sup"
ballarin@23919
    62
ballarin@23919
    63
begin
ballarin@23919
    64
ballarin@23919
    65
definition
ballarin@23919
    66
  meet :: "['a, 'a] => 'a" (infixl "\<sqinter>" 70)
ballarin@23919
    67
  where "x \<sqinter> y = (THE inf. is_inf x y inf)"
ballarin@23919
    68
ballarin@23919
    69
definition
ballarin@23919
    70
  join :: "['a, 'a] => 'a" (infixl "\<squnion>" 65)
ballarin@23919
    71
  where "x \<squnion> y = (THE sup. is_sup x y sup)"
ballarin@23919
    72
ballarin@23919
    73
lemma is_infI [intro?]: "i \<sqsubseteq> x \<Longrightarrow> i \<sqsubseteq> y \<Longrightarrow>
ballarin@23919
    74
    (\<And>z. z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> i) \<Longrightarrow> is_inf x y i"
ballarin@23919
    75
  by (unfold is_inf_def) blast
ballarin@23919
    76
ballarin@23919
    77
lemma is_inf_lower [elim?]:
ballarin@23919
    78
  "is_inf x y i \<Longrightarrow> (i \<sqsubseteq> x \<Longrightarrow> i \<sqsubseteq> y \<Longrightarrow> C) \<Longrightarrow> C"
ballarin@23919
    79
  by (unfold is_inf_def) blast
ballarin@23919
    80
ballarin@23919
    81
lemma is_inf_greatest [elim?]:
ballarin@23919
    82
    "is_inf x y i \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> i"
ballarin@23919
    83
  by (unfold is_inf_def) blast
ballarin@23919
    84
ballarin@23919
    85
theorem is_inf_uniq: "is_inf x y i \<Longrightarrow> is_inf x y i' \<Longrightarrow> i = i'"
ballarin@23919
    86
proof -
ballarin@23919
    87
  assume inf: "is_inf x y i"
ballarin@23919
    88
  assume inf': "is_inf x y i'"
ballarin@23919
    89
  show ?thesis
nipkow@33657
    90
  proof (rule antisym)
ballarin@23919
    91
    from inf' show "i \<sqsubseteq> i'"
ballarin@23919
    92
    proof (rule is_inf_greatest)
ballarin@23919
    93
      from inf show "i \<sqsubseteq> x" ..
ballarin@23919
    94
      from inf show "i \<sqsubseteq> y" ..
ballarin@23919
    95
    qed
ballarin@23919
    96
    from inf show "i' \<sqsubseteq> i"
ballarin@23919
    97
    proof (rule is_inf_greatest)
ballarin@23919
    98
      from inf' show "i' \<sqsubseteq> x" ..
ballarin@23919
    99
      from inf' show "i' \<sqsubseteq> y" ..
ballarin@23919
   100
    qed
ballarin@23919
   101
  qed
ballarin@23919
   102
qed
ballarin@23919
   103
ballarin@23919
   104
theorem is_inf_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> is_inf x y x"
ballarin@23919
   105
proof -
ballarin@23919
   106
  assume "x \<sqsubseteq> y"
ballarin@23919
   107
  show ?thesis
ballarin@23919
   108
  proof
ballarin@23919
   109
    show "x \<sqsubseteq> x" ..
ballarin@23919
   110
    show "x \<sqsubseteq> y" by fact
ballarin@23919
   111
    fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" show "z \<sqsubseteq> x" by fact
ballarin@23919
   112
  qed
ballarin@23919
   113
qed
ballarin@23919
   114
ballarin@23919
   115
lemma meet_equality [elim?]: "is_inf x y i \<Longrightarrow> x \<sqinter> y = i"
ballarin@23919
   116
proof (unfold meet_def)
ballarin@23919
   117
  assume "is_inf x y i"
ballarin@23919
   118
  then show "(THE i. is_inf x y i) = i"
ballarin@23919
   119
    by (rule the_equality) (rule is_inf_uniq [OF _ `is_inf x y i`])
ballarin@23919
   120
qed
ballarin@23919
   121
ballarin@23919
   122
lemma meetI [intro?]:
ballarin@23919
   123
    "i \<sqsubseteq> x \<Longrightarrow> i \<sqsubseteq> y \<Longrightarrow> (\<And>z. z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> i) \<Longrightarrow> x \<sqinter> y = i"
ballarin@23919
   124
  by (rule meet_equality, rule is_infI) blast+
ballarin@23919
   125
ballarin@23919
   126
lemma is_inf_meet [intro?]: "is_inf x y (x \<sqinter> y)"
ballarin@23919
   127
proof (unfold meet_def)
ballarin@23919
   128
  from ex_inf obtain i where "is_inf x y i" ..
ballarin@23919
   129
  then show "is_inf x y (THE i. is_inf x y i)"
ballarin@23919
   130
    by (rule theI) (rule is_inf_uniq [OF _ `is_inf x y i`])
ballarin@23919
   131
qed
ballarin@23919
   132
ballarin@23919
   133
lemma meet_left [intro?]:
ballarin@23919
   134
  "x \<sqinter> y \<sqsubseteq> x"
ballarin@23919
   135
  by (rule is_inf_lower) (rule is_inf_meet)
ballarin@23919
   136
ballarin@23919
   137
lemma meet_right [intro?]:
ballarin@23919
   138
  "x \<sqinter> y \<sqsubseteq> y"
ballarin@23919
   139
  by (rule is_inf_lower) (rule is_inf_meet)
ballarin@23919
   140
ballarin@23919
   141
lemma meet_le [intro?]:
ballarin@23919
   142
  "[| z \<sqsubseteq> x; z \<sqsubseteq> y |] ==> z \<sqsubseteq> x \<sqinter> y"
ballarin@23919
   143
  by (rule is_inf_greatest) (rule is_inf_meet)
ballarin@23919
   144
ballarin@23919
   145
lemma is_supI [intro?]: "x \<sqsubseteq> s \<Longrightarrow> y \<sqsubseteq> s \<Longrightarrow>
ballarin@23919
   146
    (\<And>z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> s \<sqsubseteq> z) \<Longrightarrow> is_sup x y s"
ballarin@23919
   147
  by (unfold is_sup_def) blast
ballarin@23919
   148
ballarin@23919
   149
lemma is_sup_least [elim?]:
ballarin@23919
   150
    "is_sup x y s \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> s \<sqsubseteq> z"
ballarin@23919
   151
  by (unfold is_sup_def) blast
ballarin@23919
   152
ballarin@23919
   153
lemma is_sup_upper [elim?]:
ballarin@23919
   154
    "is_sup x y s \<Longrightarrow> (x \<sqsubseteq> s \<Longrightarrow> y \<sqsubseteq> s \<Longrightarrow> C) \<Longrightarrow> C"
ballarin@23919
   155
  by (unfold is_sup_def) blast
ballarin@23919
   156
ballarin@23919
   157
theorem is_sup_uniq: "is_sup x y s \<Longrightarrow> is_sup x y s' \<Longrightarrow> s = s'"
ballarin@23919
   158
proof -
ballarin@23919
   159
  assume sup: "is_sup x y s"
ballarin@23919
   160
  assume sup': "is_sup x y s'"
ballarin@23919
   161
  show ?thesis
nipkow@33657
   162
  proof (rule antisym)
ballarin@23919
   163
    from sup show "s \<sqsubseteq> s'"
ballarin@23919
   164
    proof (rule is_sup_least)
ballarin@23919
   165
      from sup' show "x \<sqsubseteq> s'" ..
ballarin@23919
   166
      from sup' show "y \<sqsubseteq> s'" ..
ballarin@23919
   167
    qed
ballarin@23919
   168
    from sup' show "s' \<sqsubseteq> s"
ballarin@23919
   169
    proof (rule is_sup_least)
ballarin@23919
   170
      from sup show "x \<sqsubseteq> s" ..
ballarin@23919
   171
      from sup show "y \<sqsubseteq> s" ..
ballarin@23919
   172
    qed
ballarin@23919
   173
  qed
ballarin@23919
   174
qed
ballarin@23919
   175
ballarin@23919
   176
theorem is_sup_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> is_sup x y y"
ballarin@23919
   177
proof -
ballarin@23919
   178
  assume "x \<sqsubseteq> y"
ballarin@23919
   179
  show ?thesis
ballarin@23919
   180
  proof
ballarin@23919
   181
    show "x \<sqsubseteq> y" by fact
ballarin@23919
   182
    show "y \<sqsubseteq> y" ..
ballarin@23919
   183
    fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z"
ballarin@23919
   184
    show "y \<sqsubseteq> z" by fact
ballarin@23919
   185
  qed
ballarin@23919
   186
qed
ballarin@23919
   187
ballarin@23919
   188
lemma join_equality [elim?]: "is_sup x y s \<Longrightarrow> x \<squnion> y = s"
ballarin@23919
   189
proof (unfold join_def)
ballarin@23919
   190
  assume "is_sup x y s"
ballarin@23919
   191
  then show "(THE s. is_sup x y s) = s"
ballarin@23919
   192
    by (rule the_equality) (rule is_sup_uniq [OF _ `is_sup x y s`])
ballarin@23919
   193
qed
ballarin@23919
   194
ballarin@23919
   195
lemma joinI [intro?]: "x \<sqsubseteq> s \<Longrightarrow> y \<sqsubseteq> s \<Longrightarrow>
ballarin@23919
   196
    (\<And>z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> s \<sqsubseteq> z) \<Longrightarrow> x \<squnion> y = s"
ballarin@23919
   197
  by (rule join_equality, rule is_supI) blast+
ballarin@23919
   198
ballarin@23919
   199
lemma is_sup_join [intro?]: "is_sup x y (x \<squnion> y)"
ballarin@23919
   200
proof (unfold join_def)
ballarin@23919
   201
  from ex_sup obtain s where "is_sup x y s" ..
ballarin@23919
   202
  then show "is_sup x y (THE s. is_sup x y s)"
ballarin@23919
   203
    by (rule theI) (rule is_sup_uniq [OF _ `is_sup x y s`])
ballarin@23919
   204
qed
ballarin@23919
   205
ballarin@23919
   206
lemma join_left [intro?]:
ballarin@23919
   207
  "x \<sqsubseteq> x \<squnion> y"
ballarin@23919
   208
  by (rule is_sup_upper) (rule is_sup_join)
ballarin@23919
   209
ballarin@23919
   210
lemma join_right [intro?]:
ballarin@23919
   211
  "y \<sqsubseteq> x \<squnion> y"
ballarin@23919
   212
  by (rule is_sup_upper) (rule is_sup_join)
ballarin@23919
   213
ballarin@23919
   214
lemma join_le [intro?]:
ballarin@23919
   215
  "[| x \<sqsubseteq> z; y \<sqsubseteq> z |] ==> x \<squnion> y \<sqsubseteq> z"
ballarin@23919
   216
  by (rule is_sup_least) (rule is_sup_join)
ballarin@23919
   217
ballarin@23919
   218
theorem meet_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
ballarin@23919
   219
proof (rule meetI)
ballarin@23919
   220
  show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x \<sqinter> y"
ballarin@23919
   221
  proof
ballarin@23919
   222
    show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x" ..
ballarin@23919
   223
    show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y"
ballarin@23919
   224
    proof -
ballarin@23919
   225
      have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" ..
ballarin@23919
   226
      also have "\<dots> \<sqsubseteq> y" ..
ballarin@23919
   227
      finally show ?thesis .
ballarin@23919
   228
    qed
ballarin@23919
   229
  qed
ballarin@23919
   230
  show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> z"
ballarin@23919
   231
  proof -
ballarin@23919
   232
    have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" ..
ballarin@23919
   233
    also have "\<dots> \<sqsubseteq> z" ..
ballarin@23919
   234
    finally show ?thesis .
ballarin@23919
   235
  qed
ballarin@23919
   236
  fix w assume "w \<sqsubseteq> x \<sqinter> y" and "w \<sqsubseteq> z"
ballarin@23919
   237
  show "w \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
ballarin@23919
   238
  proof
ballarin@23919
   239
    show "w \<sqsubseteq> x"
ballarin@23919
   240
    proof -
ballarin@23919
   241
      have "w \<sqsubseteq> x \<sqinter> y" by fact
ballarin@23919
   242
      also have "\<dots> \<sqsubseteq> x" ..
ballarin@23919
   243
      finally show ?thesis .
ballarin@23919
   244
    qed
ballarin@23919
   245
    show "w \<sqsubseteq> y \<sqinter> z"
ballarin@23919
   246
    proof
ballarin@23919
   247
      show "w \<sqsubseteq> y"
ballarin@23919
   248
      proof -
ballarin@23919
   249
        have "w \<sqsubseteq> x \<sqinter> y" by fact
ballarin@23919
   250
        also have "\<dots> \<sqsubseteq> y" ..
ballarin@23919
   251
        finally show ?thesis .
ballarin@23919
   252
      qed
ballarin@23919
   253
      show "w \<sqsubseteq> z" by fact
ballarin@23919
   254
    qed
ballarin@23919
   255
  qed
ballarin@23919
   256
qed
ballarin@23919
   257
ballarin@23919
   258
theorem meet_commute: "x \<sqinter> y = y \<sqinter> x"
ballarin@23919
   259
proof (rule meetI)
ballarin@23919
   260
  show "y \<sqinter> x \<sqsubseteq> x" ..
ballarin@23919
   261
  show "y \<sqinter> x \<sqsubseteq> y" ..
ballarin@23919
   262
  fix z assume "z \<sqsubseteq> y" and "z \<sqsubseteq> x"
ballarin@23919
   263
  then show "z \<sqsubseteq> y \<sqinter> x" ..
ballarin@23919
   264
qed
ballarin@23919
   265
ballarin@23919
   266
theorem meet_join_absorb: "x \<sqinter> (x \<squnion> y) = x"
ballarin@23919
   267
proof (rule meetI)
ballarin@23919
   268
  show "x \<sqsubseteq> x" ..
ballarin@23919
   269
  show "x \<sqsubseteq> x \<squnion> y" ..
ballarin@23919
   270
  fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> x \<squnion> y"
ballarin@23919
   271
  show "z \<sqsubseteq> x" by fact
ballarin@23919
   272
qed
ballarin@23919
   273
ballarin@23919
   274
theorem join_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
ballarin@23919
   275
proof (rule joinI)
ballarin@23919
   276
  show "x \<squnion> y \<sqsubseteq> x \<squnion> (y \<squnion> z)"
ballarin@23919
   277
  proof
ballarin@23919
   278
    show "x \<sqsubseteq> x \<squnion> (y \<squnion> z)" ..
ballarin@23919
   279
    show "y \<sqsubseteq> x \<squnion> (y \<squnion> z)"
ballarin@23919
   280
    proof -
ballarin@23919
   281
      have "y \<sqsubseteq> y \<squnion> z" ..
ballarin@23919
   282
      also have "... \<sqsubseteq> x \<squnion> (y \<squnion> z)" ..
ballarin@23919
   283
      finally show ?thesis .
ballarin@23919
   284
    qed
ballarin@23919
   285
  qed
ballarin@23919
   286
  show "z \<sqsubseteq> x \<squnion> (y \<squnion> z)"
ballarin@23919
   287
  proof -
ballarin@23919
   288
    have "z \<sqsubseteq> y \<squnion> z"  ..
ballarin@23919
   289
    also have "... \<sqsubseteq> x \<squnion> (y \<squnion> z)" ..
ballarin@23919
   290
    finally show ?thesis .
ballarin@23919
   291
  qed
ballarin@23919
   292
  fix w assume "x \<squnion> y \<sqsubseteq> w" and "z \<sqsubseteq> w"
ballarin@23919
   293
  show "x \<squnion> (y \<squnion> z) \<sqsubseteq> w"
ballarin@23919
   294
  proof
ballarin@23919
   295
    show "x \<sqsubseteq> w"
ballarin@23919
   296
    proof -
ballarin@23919
   297
      have "x \<sqsubseteq> x \<squnion> y" ..
ballarin@23919
   298
      also have "\<dots> \<sqsubseteq> w" by fact
ballarin@23919
   299
      finally show ?thesis .
ballarin@23919
   300
    qed
ballarin@23919
   301
    show "y \<squnion> z \<sqsubseteq> w"
ballarin@23919
   302
    proof
ballarin@23919
   303
      show "y \<sqsubseteq> w"
ballarin@23919
   304
      proof -
wenzelm@32960
   305
        have "y \<sqsubseteq> x \<squnion> y" ..
wenzelm@32960
   306
        also have "... \<sqsubseteq> w" by fact
ballarin@23919
   307
        finally show ?thesis .
ballarin@23919
   308
      qed
ballarin@23919
   309
      show "z \<sqsubseteq> w" by fact
ballarin@23919
   310
    qed
ballarin@23919
   311
  qed
ballarin@23919
   312
qed
ballarin@23919
   313
ballarin@23919
   314
theorem join_commute: "x \<squnion> y = y \<squnion> x"
ballarin@23919
   315
proof (rule joinI)
ballarin@23919
   316
  show "x \<sqsubseteq> y \<squnion> x" ..
ballarin@23919
   317
  show "y \<sqsubseteq> y \<squnion> x" ..
ballarin@23919
   318
  fix z assume "y \<sqsubseteq> z" and "x \<sqsubseteq> z"
ballarin@23919
   319
  then show "y \<squnion> x \<sqsubseteq> z" ..
ballarin@23919
   320
qed
ballarin@23919
   321
ballarin@23919
   322
theorem join_meet_absorb: "x \<squnion> (x \<sqinter> y) = x"
ballarin@23919
   323
proof (rule joinI)
ballarin@23919
   324
  show "x \<sqsubseteq> x" ..
ballarin@23919
   325
  show "x \<sqinter> y \<sqsubseteq> x" ..
ballarin@23919
   326
  fix z assume "x \<sqsubseteq> z" and "x \<sqinter> y \<sqsubseteq> z"
ballarin@23919
   327
  show "x \<sqsubseteq> z" by fact
ballarin@23919
   328
qed
ballarin@23919
   329
ballarin@23919
   330
theorem meet_idem: "x \<sqinter> x = x"
ballarin@23919
   331
proof -
ballarin@23919
   332
  have "x \<sqinter> (x \<squnion> (x \<sqinter> x)) = x" by (rule meet_join_absorb)
ballarin@23919
   333
  also have "x \<squnion> (x \<sqinter> x) = x" by (rule join_meet_absorb)
ballarin@23919
   334
  finally show ?thesis .
ballarin@23919
   335
qed
ballarin@23919
   336
ballarin@23919
   337
theorem meet_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
ballarin@23919
   338
proof (rule meetI)
ballarin@23919
   339
  assume "x \<sqsubseteq> y"
ballarin@23919
   340
  show "x \<sqsubseteq> x" ..
ballarin@23919
   341
  show "x \<sqsubseteq> y" by fact
ballarin@23919
   342
  fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y"
ballarin@23919
   343
  show "z \<sqsubseteq> x" by fact
ballarin@23919
   344
qed
ballarin@23919
   345
ballarin@23919
   346
theorem meet_related2 [elim?]: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
ballarin@23919
   347
  by (drule meet_related) (simp add: meet_commute)
ballarin@23919
   348
ballarin@23919
   349
theorem join_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
ballarin@23919
   350
proof (rule joinI)
ballarin@23919
   351
  assume "x \<sqsubseteq> y"
ballarin@23919
   352
  show "y \<sqsubseteq> y" ..
ballarin@23919
   353
  show "x \<sqsubseteq> y" by fact
ballarin@23919
   354
  fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z"
ballarin@23919
   355
  show "y \<sqsubseteq> z" by fact
ballarin@23919
   356
qed
ballarin@23919
   357
ballarin@23919
   358
theorem join_related2 [elim?]: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
ballarin@23919
   359
  by (drule join_related) (simp add: join_commute)
ballarin@23919
   360
ballarin@23919
   361
ballarin@23919
   362
text {* Additional theorems *}
ballarin@23919
   363
ballarin@23919
   364
theorem meet_connection: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)"
ballarin@23919
   365
proof
ballarin@23919
   366
  assume "x \<sqsubseteq> y"
ballarin@23919
   367
  then have "is_inf x y x" ..
ballarin@23919
   368
  then show "x \<sqinter> y = x" ..
ballarin@23919
   369
next
ballarin@23919
   370
  have "x \<sqinter> y \<sqsubseteq> y" ..
ballarin@23919
   371
  also assume "x \<sqinter> y = x"
ballarin@23919
   372
  finally show "x \<sqsubseteq> y" .
ballarin@23919
   373
qed
ballarin@23919
   374
ballarin@23919
   375
theorem meet_connection2: "(x \<sqsubseteq> y) = (y \<sqinter> x = x)"
ballarin@23919
   376
  using meet_commute meet_connection by simp
ballarin@23919
   377
ballarin@23919
   378
theorem join_connection: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"
ballarin@23919
   379
proof
ballarin@23919
   380
  assume "x \<sqsubseteq> y"
ballarin@23919
   381
  then have "is_sup x y y" ..
ballarin@23919
   382
  then show "x \<squnion> y = y" ..
ballarin@23919
   383
next
ballarin@23919
   384
  have "x \<sqsubseteq> x \<squnion> y" ..
ballarin@23919
   385
  also assume "x \<squnion> y = y"
ballarin@23919
   386
  finally show "x \<sqsubseteq> y" .
ballarin@23919
   387
qed
ballarin@23919
   388
ballarin@23919
   389
theorem join_connection2: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"
ballarin@23919
   390
  using join_commute join_connection by simp
ballarin@23919
   391
ballarin@23919
   392
ballarin@23919
   393
text {* Naming according to Jacobson I, p.\ 459. *}
ballarin@23919
   394
ballarin@23919
   395
lemmas L1 = join_commute meet_commute
ballarin@23919
   396
lemmas L2 = join_assoc meet_assoc
ballarin@23919
   397
(*lemmas L3 = join_idem meet_idem*)
ballarin@23919
   398
lemmas L4 = join_meet_absorb meet_join_absorb
ballarin@23919
   399
ballarin@23919
   400
end
ballarin@23919
   401
ballarin@23919
   402
locale ddlat = dlat +
ballarin@23919
   403
  assumes meet_distr:
ballarin@23919
   404
    "dlat.meet le x (dlat.join le y z) =
ballarin@23919
   405
    dlat.join le (dlat.meet le x y) (dlat.meet le x z)"
ballarin@23919
   406
ballarin@23919
   407
begin
ballarin@23919
   408
ballarin@23919
   409
lemma join_distr:
ballarin@23919
   410
  "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
ballarin@23919
   411
  txt {* Jacobson I, p.\ 462 *}
ballarin@23919
   412
proof -
ballarin@23919
   413
  have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by (simp add: L4)
ballarin@23919
   414
  also have "... = x \<squnion> ((x \<sqinter> z) \<squnion> (y \<sqinter> z))" by (simp add: L2)
ballarin@23919
   415
  also have "... = x \<squnion> ((x \<squnion> y) \<sqinter> z)" by (simp add: L1 meet_distr)
ballarin@23919
   416
  also have "... = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)" by (simp add: L1 L4)
ballarin@23919
   417
  also have "... = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by (simp add: meet_distr)
ballarin@23919
   418
  finally show ?thesis .
ballarin@23919
   419
qed
ballarin@23919
   420
ballarin@23919
   421
end
ballarin@23919
   422
ballarin@23919
   423
locale dlo = dpo +
ballarin@23919
   424
  assumes total: "x \<sqsubseteq> y | y \<sqsubseteq> x"
ballarin@23919
   425
ballarin@23919
   426
begin
ballarin@23919
   427
ballarin@23919
   428
lemma less_total: "x \<sqsubset> y | x = y | y \<sqsubset> x"
ballarin@23919
   429
  using total
ballarin@23919
   430
  by (unfold less_def) blast
ballarin@23919
   431
ballarin@23919
   432
end
ballarin@23919
   433
ballarin@23919
   434
ballarin@29223
   435
sublocale dlo < dlat
haftmann@28823
   436
proof
ballarin@23919
   437
  fix x y
ballarin@23919
   438
  from total have "is_inf x y (if x \<sqsubseteq> y then x else y)" by (auto simp: is_inf_def)
ballarin@23919
   439
  then show "EX inf. is_inf x y inf" by blast
ballarin@23919
   440
next
ballarin@23919
   441
  fix x y
ballarin@23919
   442
  from total have "is_sup x y (if x \<sqsubseteq> y then y else x)" by (auto simp: is_sup_def)
ballarin@23919
   443
  then show "EX sup. is_sup x y sup" by blast
ballarin@23919
   444
qed
ballarin@23919
   445
ballarin@29223
   446
sublocale dlo < ddlat
haftmann@28823
   447
proof
ballarin@23919
   448
  fix x y z
ballarin@23919
   449
  show "x \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> z" (is "?l = ?r")
ballarin@23919
   450
    txt {* Jacobson I, p.\ 462 *}
ballarin@23919
   451
  proof -
ballarin@23919
   452
    { assume c: "y \<sqsubseteq> x" "z \<sqsubseteq> x"
ballarin@23919
   453
      from c have "?l = y \<squnion> z"
wenzelm@32960
   454
        by (metis c (*join_commute*) join_connection2 join_related2 (*meet_commute*) meet_connection meet_related2 total)
ballarin@23919
   455
      also from c have "... = ?r" by (metis (*c*) (*join_commute*) meet_related2)
ballarin@23919
   456
      finally have "?l = ?r" . }
ballarin@23919
   457
    moreover
ballarin@23919
   458
    { assume c: "x \<sqsubseteq> y | x \<sqsubseteq> z"
ballarin@23919
   459
      from c have "?l = x"
nipkow@33657
   460
        by (metis (*antisym*) (*c*) (*circular*) (*join_assoc*)(* join_commute *) join_connection2 (*join_left*) join_related2 meet_connection(* meet_related2*) total trans)
ballarin@23919
   461
      also from c have "... = ?r"
wenzelm@32960
   462
        by (metis join_commute join_related2 meet_connection meet_related2 total)
ballarin@23919
   463
      finally have "?l = ?r" . }
ballarin@23919
   464
    moreover note total
ballarin@23919
   465
    ultimately show ?thesis by blast
ballarin@23919
   466
  qed
ballarin@23919
   467
qed
ballarin@23919
   468
ballarin@23919
   469
subsubsection {* Total order @{text "<="} on @{typ int} *}
ballarin@23919
   470
wenzelm@30729
   471
interpretation int: dpo "op <= :: [int, int] => bool"
ballarin@23919
   472
  where "(dpo.less (op <=) (x::int) y) = (x < y)"
wenzelm@24946
   473
  txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
ballarin@23919
   474
proof -
ballarin@23919
   475
  show "dpo (op <= :: [int, int] => bool)"
haftmann@28823
   476
    proof qed auto
ballarin@29226
   477
  then interpret int: dpo "op <= :: [int, int] => bool" .
wenzelm@24946
   478
    txt {* Gives interpreted version of @{text less_def} (without condition). *}
ballarin@23919
   479
  show "(dpo.less (op <=) (x::int) y) = (x < y)"
ballarin@23919
   480
    by (unfold int.less_def) auto
ballarin@23919
   481
qed
ballarin@23919
   482
ballarin@23919
   483
thm int.circular
ballarin@23919
   484
lemma "\<lbrakk> (x::int) \<le> y; y \<le> z; z \<le> x\<rbrakk> \<Longrightarrow> x = y \<and> y = z"
ballarin@23919
   485
  apply (rule int.circular) apply assumption apply assumption apply assumption done
ballarin@23919
   486
thm int.abs_test
ballarin@23919
   487
lemma "(op < :: [int, int] => bool) = op <"
ballarin@23919
   488
  apply (rule int.abs_test) done
ballarin@23919
   489
wenzelm@30729
   490
interpretation int: dlat "op <= :: [int, int] => bool"
ballarin@25284
   491
  where meet_eq: "dlat.meet (op <=) (x::int) y = min x y"
ballarin@25284
   492
    and join_eq: "dlat.join (op <=) (x::int) y = max x y"
ballarin@23919
   493
proof -
ballarin@23919
   494
  show "dlat (op <= :: [int, int] => bool)"
ballarin@23919
   495
    apply unfold_locales
ballarin@23919
   496
    apply (unfold int.is_inf_def int.is_sup_def)
ballarin@23919
   497
    apply arith+
ballarin@23919
   498
    done
ballarin@29226
   499
  then interpret int: dlat "op <= :: [int, int] => bool" .
ballarin@23919
   500
  txt {* Interpretation to ease use of definitions, which are
ballarin@23919
   501
    conditional in general but unconditional after interpretation. *}
ballarin@23919
   502
  show "dlat.meet (op <=) (x::int) y = min x y"
ballarin@23919
   503
    apply (unfold int.meet_def)
ballarin@23919
   504
    apply (rule the_equality)
ballarin@23919
   505
    apply (unfold int.is_inf_def)
ballarin@23919
   506
    by auto
ballarin@23919
   507
  show "dlat.join (op <=) (x::int) y = max x y"
ballarin@23919
   508
    apply (unfold int.join_def)
ballarin@23919
   509
    apply (rule the_equality)
ballarin@23919
   510
    apply (unfold int.is_sup_def)
ballarin@23919
   511
    by auto
ballarin@23919
   512
qed
ballarin@23919
   513
wenzelm@30729
   514
interpretation int: dlo "op <= :: [int, int] => bool"
haftmann@28823
   515
  proof qed arith
ballarin@23919
   516
ballarin@23919
   517
text {* Interpreted theorems from the locales, involving defined terms. *}
ballarin@23919
   518
ballarin@23919
   519
thm int.less_def text {* from dpo *}
ballarin@23919
   520
thm int.meet_left text {* from dlat *}
ballarin@23919
   521
thm int.meet_distr text {* from ddlat *}
ballarin@23919
   522
thm int.less_total text {* from dlo *}
ballarin@23919
   523
ballarin@23919
   524
ballarin@23919
   525
subsubsection {* Total order @{text "<="} on @{typ nat} *}
ballarin@23919
   526
wenzelm@30729
   527
interpretation nat: dpo "op <= :: [nat, nat] => bool"
ballarin@23919
   528
  where "dpo.less (op <=) (x::nat) y = (x < y)"
wenzelm@24946
   529
  txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
ballarin@23919
   530
proof -
ballarin@23919
   531
  show "dpo (op <= :: [nat, nat] => bool)"
haftmann@28823
   532
    proof qed auto
ballarin@29226
   533
  then interpret nat: dpo "op <= :: [nat, nat] => bool" .
wenzelm@24946
   534
    txt {* Gives interpreted version of @{text less_def} (without condition). *}
ballarin@23919
   535
  show "dpo.less (op <=) (x::nat) y = (x < y)"
ballarin@23919
   536
    apply (unfold nat.less_def)
ballarin@23919
   537
    apply auto
ballarin@23919
   538
    done
ballarin@23919
   539
qed
ballarin@23919
   540
wenzelm@30729
   541
interpretation nat: dlat "op <= :: [nat, nat] => bool"
ballarin@23919
   542
  where "dlat.meet (op <=) (x::nat) y = min x y"
ballarin@23919
   543
    and "dlat.join (op <=) (x::nat) y = max x y"
ballarin@23919
   544
proof -
ballarin@23919
   545
  show "dlat (op <= :: [nat, nat] => bool)"
ballarin@23919
   546
    apply unfold_locales
ballarin@23919
   547
    apply (unfold nat.is_inf_def nat.is_sup_def)
ballarin@23919
   548
    apply arith+
ballarin@23919
   549
    done
ballarin@29226
   550
  then interpret nat: dlat "op <= :: [nat, nat] => bool" .
ballarin@23919
   551
  txt {* Interpretation to ease use of definitions, which are
ballarin@23919
   552
    conditional in general but unconditional after interpretation. *}
ballarin@23919
   553
  show "dlat.meet (op <=) (x::nat) y = min x y"
ballarin@23919
   554
    apply (unfold nat.meet_def)
ballarin@23919
   555
    apply (rule the_equality)
ballarin@23919
   556
    apply (unfold nat.is_inf_def)
ballarin@23919
   557
    by auto
ballarin@23919
   558
  show "dlat.join (op <=) (x::nat) y = max x y"
ballarin@23919
   559
    apply (unfold nat.join_def)
ballarin@23919
   560
    apply (rule the_equality)
ballarin@23919
   561
    apply (unfold nat.is_sup_def)
ballarin@23919
   562
    by auto
ballarin@23919
   563
qed
ballarin@23919
   564
wenzelm@30729
   565
interpretation nat: dlo "op <= :: [nat, nat] => bool"
haftmann@28823
   566
  proof qed arith
ballarin@23919
   567
ballarin@23919
   568
text {* Interpreted theorems from the locales, involving defined terms. *}
ballarin@23919
   569
ballarin@23919
   570
thm nat.less_def text {* from dpo *}
ballarin@23919
   571
thm nat.meet_left text {* from dlat *}
ballarin@23919
   572
thm nat.meet_distr text {* from ddlat *}
ballarin@23919
   573
thm nat.less_total text {* from ldo *}
ballarin@23919
   574
ballarin@23919
   575
ballarin@23919
   576
subsubsection {* Lattice @{text "dvd"} on @{typ nat} *}
ballarin@23919
   577
wenzelm@30729
   578
interpretation nat_dvd: dpo "op dvd :: [nat, nat] => bool"
ballarin@23919
   579
  where "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)"
wenzelm@24946
   580
  txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
ballarin@23919
   581
proof -
ballarin@23919
   582
  show "dpo (op dvd :: [nat, nat] => bool)"
haftmann@28823
   583
    proof qed (auto simp: dvd_def)
ballarin@29226
   584
  then interpret nat_dvd: dpo "op dvd :: [nat, nat] => bool" .
wenzelm@24946
   585
    txt {* Gives interpreted version of @{text less_def} (without condition). *}
ballarin@23919
   586
  show "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)"
ballarin@23919
   587
    apply (unfold nat_dvd.less_def)
ballarin@23919
   588
    apply auto
ballarin@23919
   589
    done
ballarin@23919
   590
qed
ballarin@23919
   591
wenzelm@30729
   592
interpretation nat_dvd: dlat "op dvd :: [nat, nat] => bool"
haftmann@27556
   593
  where "dlat.meet (op dvd) (x::nat) y = gcd x y"
haftmann@27556
   594
    and "dlat.join (op dvd) (x::nat) y = lcm x y"
ballarin@23919
   595
proof -
ballarin@23919
   596
  show "dlat (op dvd :: [nat, nat] => bool)"
ballarin@23919
   597
    apply unfold_locales
ballarin@23919
   598
    apply (unfold nat_dvd.is_inf_def nat_dvd.is_sup_def)
haftmann@27556
   599
    apply (rule_tac x = "gcd x y" in exI)
ballarin@23919
   600
    apply auto [1]
haftmann@27556
   601
    apply (rule_tac x = "lcm x y" in exI)
nipkow@31952
   602
    apply (auto intro: lcm_dvd1_nat lcm_dvd2_nat lcm_least_nat)
ballarin@23919
   603
    done
ballarin@29226
   604
  then interpret nat_dvd: dlat "op dvd :: [nat, nat] => bool" .
ballarin@23919
   605
  txt {* Interpretation to ease use of definitions, which are
ballarin@23919
   606
    conditional in general but unconditional after interpretation. *}
haftmann@27556
   607
  show "dlat.meet (op dvd) (x::nat) y = gcd x y"
ballarin@23919
   608
    apply (unfold nat_dvd.meet_def)
ballarin@23919
   609
    apply (rule the_equality)
ballarin@23919
   610
    apply (unfold nat_dvd.is_inf_def)
ballarin@23919
   611
    by auto
haftmann@27556
   612
  show "dlat.join (op dvd) (x::nat) y = lcm x y"
ballarin@23919
   613
    apply (unfold nat_dvd.join_def)
ballarin@23919
   614
    apply (rule the_equality)
ballarin@23919
   615
    apply (unfold nat_dvd.is_sup_def)
nipkow@31952
   616
    by (auto intro: lcm_dvd1_nat lcm_dvd2_nat lcm_least_nat)
ballarin@23919
   617
qed
ballarin@23919
   618
ballarin@23919
   619
text {* Interpreted theorems from the locales, involving defined terms. *}
ballarin@23919
   620
ballarin@23919
   621
thm nat_dvd.less_def text {* from dpo *}
ballarin@23919
   622
lemma "((x::nat) dvd y & x ~= y) = (x dvd y & x ~= y)"
ballarin@23919
   623
  apply (rule nat_dvd.less_def) done
ballarin@23919
   624
thm nat_dvd.meet_left text {* from dlat *}
huffman@31711
   625
lemma "gcd x y dvd (x::nat)"
ballarin@23919
   626
  apply (rule nat_dvd.meet_left) done
ballarin@23919
   627
ballarin@23919
   628
ballarin@23919
   629
subsection {* Group example with defined operations @{text inv} and @{text unit} *}
ballarin@23919
   630
ballarin@23919
   631
subsubsection {* Locale declarations and lemmas *}
ballarin@22657
   632
ballarin@22657
   633
locale Dsemi =
ballarin@22657
   634
  fixes prod (infixl "**" 65)
ballarin@22657
   635
  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
ballarin@22657
   636
ballarin@22657
   637
locale Dmonoid = Dsemi +
ballarin@22657
   638
  fixes one
ballarin@23919
   639
  assumes l_one [simp]: "one ** x = x"
ballarin@23919
   640
    and r_one [simp]: "x ** one = x"
ballarin@23919
   641
ballarin@23919
   642
begin
ballarin@22657
   643
ballarin@23919
   644
definition
ballarin@23919
   645
  inv where "inv x = (THE y. x ** y = one & y ** x = one)"
ballarin@23919
   646
definition
ballarin@23919
   647
  unit where "unit x = (EX y. x ** y = one  & y ** x = one)"
ballarin@22657
   648
ballarin@23919
   649
lemma inv_unique:
ballarin@22657
   650
  assumes eq: "y ** x = one" "x ** y' = one"
ballarin@22657
   651
  shows "y = y'"
ballarin@22657
   652
proof -
ballarin@23919
   653
  from eq have "y = y ** (x ** y')" by (simp add: r_one)
ballarin@22657
   654
  also have "... = (y ** x) ** y'" by (simp add: assoc)
ballarin@23919
   655
  also from eq have "... = y'" by (simp add: l_one)
ballarin@22657
   656
  finally show ?thesis .
ballarin@22657
   657
qed
ballarin@22657
   658
ballarin@23919
   659
lemma unit_one [intro, simp]:
ballarin@23919
   660
  "unit one"
ballarin@23919
   661
  by (unfold unit_def) auto
ballarin@23919
   662
ballarin@23919
   663
lemma unit_l_inv_ex:
ballarin@23919
   664
  "unit x ==> \<exists>y. y ** x = one"
ballarin@23919
   665
  by (unfold unit_def) auto
ballarin@23919
   666
ballarin@23919
   667
lemma unit_r_inv_ex:
ballarin@23919
   668
  "unit x ==> \<exists>y. x ** y = one"
ballarin@23919
   669
  by (unfold unit_def) auto
ballarin@23919
   670
ballarin@23919
   671
lemma unit_l_inv:
ballarin@23919
   672
  "unit x ==> inv x ** x = one"
ballarin@23919
   673
  apply (simp add: unit_def inv_def) apply (erule exE)
ballarin@23919
   674
  apply (rule theI2, fast)
ballarin@23919
   675
  apply (rule inv_unique)
ballarin@23919
   676
  apply fast+
ballarin@23919
   677
  done
ballarin@22657
   678
ballarin@23919
   679
lemma unit_r_inv:
ballarin@23919
   680
  "unit x ==> x ** inv x = one"
ballarin@23919
   681
  apply (simp add: unit_def inv_def) apply (erule exE)
ballarin@23919
   682
  apply (rule theI2, fast)
ballarin@23919
   683
  apply (rule inv_unique)
ballarin@23919
   684
  apply fast+
ballarin@23919
   685
  done
ballarin@23919
   686
ballarin@23919
   687
lemma unit_inv_unit [intro, simp]:
ballarin@23919
   688
  "unit x ==> unit (inv x)"
ballarin@23919
   689
proof -
ballarin@23919
   690
  assume x: "unit x"
ballarin@23919
   691
  show "unit (inv x)"
ballarin@23919
   692
    by (auto simp add: unit_def
ballarin@23919
   693
      intro: unit_l_inv unit_r_inv x)
ballarin@23919
   694
qed
ballarin@23919
   695
ballarin@23919
   696
lemma unit_l_cancel [simp]:
ballarin@23919
   697
  "unit x ==> (x ** y = x ** z) = (y = z)"
ballarin@23919
   698
proof
ballarin@23919
   699
  assume eq: "x ** y = x ** z"
ballarin@23919
   700
    and G: "unit x"
ballarin@23919
   701
  then have "(inv x ** x) ** y = (inv x ** x) ** z"
ballarin@23919
   702
    by (simp add: assoc)
ballarin@23919
   703
  with G show "y = z" by (simp add: unit_l_inv)
ballarin@23919
   704
next
ballarin@23919
   705
  assume eq: "y = z"
ballarin@23919
   706
    and G: "unit x"
ballarin@23919
   707
  then show "x ** y = x ** z" by simp
ballarin@23919
   708
qed
ballarin@22657
   709
ballarin@23919
   710
lemma unit_inv_inv [simp]:
ballarin@23919
   711
  "unit x ==> inv (inv x) = x"
ballarin@23919
   712
proof -
ballarin@23919
   713
  assume x: "unit x"
ballarin@23919
   714
  then have "inv x ** inv (inv x) = inv x ** x"
ballarin@23919
   715
    by (simp add: unit_l_inv unit_r_inv)
ballarin@23919
   716
  with x show ?thesis by simp
ballarin@23919
   717
qed
ballarin@23919
   718
ballarin@23919
   719
lemma inv_inj_on_unit:
ballarin@23919
   720
  "inj_on inv {x. unit x}"
ballarin@23919
   721
proof (rule inj_onI, simp)
ballarin@23919
   722
  fix x y
ballarin@23919
   723
  assume G: "unit x"  "unit y" and eq: "inv x = inv y"
ballarin@23919
   724
  then have "inv (inv x) = inv (inv y)" by simp
ballarin@23919
   725
  with G show "x = y" by simp
ballarin@23919
   726
qed
ballarin@23919
   727
ballarin@23919
   728
lemma unit_inv_comm:
ballarin@23919
   729
  assumes inv: "x ** y = one"
ballarin@23919
   730
    and G: "unit x"  "unit y"
ballarin@23919
   731
  shows "y ** x = one"
ballarin@23919
   732
proof -
ballarin@23919
   733
  from G have "x ** y ** x = x ** one" by (auto simp add: inv)
ballarin@23919
   734
  with G show ?thesis by (simp del: r_one add: assoc)
ballarin@23919
   735
qed
ballarin@23919
   736
ballarin@23919
   737
end
ballarin@23919
   738
ballarin@23919
   739
ballarin@23919
   740
locale Dgrp = Dmonoid +
ballarin@23919
   741
  assumes unit [intro, simp]: "Dmonoid.unit (op **) one x"
ballarin@23919
   742
ballarin@23919
   743
begin
ballarin@23919
   744
ballarin@23919
   745
lemma l_inv_ex [simp]:
ballarin@23919
   746
  "\<exists>y. y ** x = one"
ballarin@23919
   747
  using unit_l_inv_ex by simp
ballarin@23919
   748
ballarin@23919
   749
lemma r_inv_ex [simp]:
ballarin@23919
   750
  "\<exists>y. x ** y = one"
ballarin@23919
   751
  using unit_r_inv_ex by simp
ballarin@23919
   752
ballarin@23919
   753
lemma l_inv [simp]:
ballarin@23919
   754
  "inv x ** x = one"
ballarin@23919
   755
  using unit_l_inv by simp
ballarin@23919
   756
ballarin@23919
   757
lemma l_cancel [simp]:
ballarin@23919
   758
  "(x ** y = x ** z) = (y = z)"
ballarin@23919
   759
  using unit_l_inv by simp
ballarin@23919
   760
ballarin@23919
   761
lemma r_inv [simp]:
ballarin@22657
   762
  "x ** inv x = one"
ballarin@23919
   763
proof -
ballarin@23919
   764
  have "inv x ** (x ** inv x) = inv x ** one"
ballarin@23919
   765
    by (simp add: assoc [symmetric] l_inv)
ballarin@23919
   766
  then show ?thesis by (simp del: r_one)
ballarin@23919
   767
qed
ballarin@22657
   768
ballarin@23919
   769
lemma r_cancel [simp]:
ballarin@23919
   770
  "(y ** x = z ** x) = (y = z)"
ballarin@22657
   771
proof
ballarin@23919
   772
  assume eq: "y ** x = z ** x"
ballarin@23919
   773
  then have "y ** (x ** inv x) = z ** (x ** inv x)"
ballarin@23919
   774
    by (simp add: assoc [symmetric] del: r_inv)
ballarin@23919
   775
  then show "y = z" by simp
ballarin@22657
   776
qed simp
ballarin@22657
   777
ballarin@23919
   778
lemma inv_one [simp]:
ballarin@23919
   779
  "inv one = one"
ballarin@22657
   780
proof -
ballarin@23919
   781
  have "inv one = one ** (inv one)" by (simp del: r_inv)
ballarin@23919
   782
  moreover have "... = one" by simp
ballarin@23919
   783
  finally show ?thesis .
ballarin@22657
   784
qed
ballarin@22657
   785
ballarin@23919
   786
lemma inv_inv [simp]:
ballarin@23919
   787
  "inv (inv x) = x"
ballarin@23919
   788
  using unit_inv_inv by simp
ballarin@22657
   789
ballarin@23919
   790
lemma inv_inj:
ballarin@23919
   791
  "inj_on inv UNIV"
ballarin@23919
   792
  using inv_inj_on_unit by simp
ballarin@22657
   793
ballarin@23919
   794
lemma inv_mult_group:
ballarin@23919
   795
  "inv (x ** y) = inv y ** inv x"
ballarin@22657
   796
proof -
ballarin@23919
   797
  have "inv (x ** y) ** (x ** y) = (inv y ** inv x) ** (x ** y)"
ballarin@23919
   798
    by (simp add: assoc l_inv) (simp add: assoc [symmetric])
ballarin@23919
   799
  then show ?thesis by (simp del: l_inv)
ballarin@23919
   800
qed
ballarin@23919
   801
ballarin@23919
   802
lemma inv_comm:
ballarin@23919
   803
  "x ** y = one ==> y ** x = one"
ballarin@23919
   804
  by (rule unit_inv_comm) auto
ballarin@23919
   805
ballarin@23919
   806
lemma inv_equality:
ballarin@23919
   807
     "y ** x = one ==> inv x = y"
ballarin@23919
   808
  apply (simp add: inv_def)
ballarin@23919
   809
  apply (rule the_equality)
ballarin@23919
   810
   apply (simp add: inv_comm [of y x])
ballarin@23919
   811
  apply (rule r_cancel [THEN iffD1], auto)
ballarin@23919
   812
  done
ballarin@23919
   813
ballarin@23919
   814
end
ballarin@23919
   815
ballarin@23919
   816
ballarin@29226
   817
locale Dhom = prod: Dgrp prod one + sum: Dgrp sum zero
ballarin@29226
   818
    for prod (infixl "**" 65) and one and sum (infixl "+++" 60) and zero +
ballarin@23919
   819
  fixes hom
ballarin@23919
   820
  assumes hom_mult [simp]: "hom (x ** y) = hom x +++ hom y"
ballarin@23919
   821
ballarin@23919
   822
begin
ballarin@23919
   823
ballarin@23919
   824
lemma hom_one [simp]:
ballarin@23919
   825
  "hom one = zero"
ballarin@23919
   826
proof -
ballarin@23919
   827
  have "hom one +++ zero = hom one +++ hom one"
ballarin@23919
   828
    by (simp add: hom_mult [symmetric] del: hom_mult)
ballarin@23919
   829
  then show ?thesis by (simp del: r_one)
ballarin@22657
   830
qed
ballarin@22657
   831
ballarin@23919
   832
end
ballarin@22657
   833
ballarin@22657
   834
ballarin@23919
   835
subsubsection {* Interpretation of Functions *}
ballarin@22657
   836
wenzelm@30729
   837
interpretation Dfun: Dmonoid "op o" "id :: 'a => 'a"
ballarin@23919
   838
  where "Dmonoid.unit (op o) id f = bij (f::'a => 'a)"
ballarin@23919
   839
(*    and "Dmonoid.inv (op o) id" = "inv :: ('a => 'a) => ('a => 'a)" *)
ballarin@22657
   840
proof -
haftmann@28823
   841
  show "Dmonoid op o (id :: 'a => 'a)" proof qed (simp_all add: o_assoc)
ballarin@23919
   842
  note Dmonoid = this
ballarin@23919
   843
(*
ballarin@29226
   844
  from this interpret Dmonoid "op o" "id :: 'a => 'a" .
ballarin@23919
   845
*)
ballarin@23919
   846
  show "Dmonoid.unit (op o) (id :: 'a => 'a) f = bij f"
ballarin@23919
   847
    apply (unfold Dmonoid.unit_def [OF Dmonoid])
ballarin@23919
   848
    apply rule apply clarify
ballarin@23919
   849
  proof -
ballarin@23919
   850
    fix f g
ballarin@23919
   851
    assume id1: "f o g = id" and id2: "g o f = id"
ballarin@23919
   852
    show "bij f"
ballarin@23919
   853
    proof (rule bijI)
ballarin@23919
   854
      show "inj f"
ballarin@23919
   855
      proof (rule inj_onI)
ballarin@23919
   856
        fix x y
ballarin@23919
   857
        assume "f x = f y"
wenzelm@32960
   858
        then have "(g o f) x = (g o f) y" by simp
wenzelm@32960
   859
        with id2 show "x = y" by simp
ballarin@23919
   860
      qed
ballarin@23919
   861
    next
ballarin@23919
   862
      show "surj f"
ballarin@23919
   863
      proof (rule surjI)
wenzelm@32960
   864
        fix x
ballarin@23919
   865
        from id1 have "(f o g) x = x" by simp
wenzelm@32960
   866
        then show "f (g x) = x" by simp
ballarin@23919
   867
      qed
ballarin@23919
   868
    qed
ballarin@23919
   869
  next
ballarin@23919
   870
    fix f
ballarin@23919
   871
    assume bij: "bij f"
ballarin@23919
   872
    then
ballarin@23919
   873
    have inv: "f o Hilbert_Choice.inv f = id & Hilbert_Choice.inv f o f = id"
ballarin@23919
   874
      by (simp add: bij_def surj_iff inj_iff)
ballarin@23919
   875
    show "EX g. f o g = id & g o f = id" by rule (rule inv)
ballarin@23919
   876
  qed
ballarin@22657
   877
qed
ballarin@22657
   878
ballarin@23919
   879
thm Dmonoid.unit_def Dfun.unit_def
ballarin@23919
   880
ballarin@23919
   881
thm Dmonoid.inv_inj_on_unit Dfun.inv_inj_on_unit
ballarin@23919
   882
ballarin@23919
   883
lemma unit_id:
ballarin@23919
   884
  "(f :: unit => unit) = id"
ballarin@23919
   885
  by rule simp
ballarin@23919
   886
wenzelm@30729
   887
interpretation Dfun: Dgrp "op o" "id :: unit => unit"
ballarin@23919
   888
  where "Dmonoid.inv (op o) id f = inv (f :: unit => unit)"
ballarin@23919
   889
proof -
haftmann@28823
   890
  have "Dmonoid op o (id :: 'a => 'a)" ..
ballarin@23919
   891
  note Dmonoid = this
ballarin@23919
   892
ballarin@23919
   893
  show "Dgrp (op o) (id :: unit => unit)"
ballarin@23919
   894
apply unfold_locales
ballarin@23919
   895
apply (unfold Dmonoid.unit_def [OF Dmonoid])
ballarin@23919
   896
apply (insert unit_id)
ballarin@23919
   897
apply simp
ballarin@23919
   898
done
ballarin@23919
   899
  show "Dmonoid.inv (op o) id f = inv (f :: unit => unit)"
berghofe@33000
   900
apply (unfold Dmonoid.inv_def [OF Dmonoid])
ballarin@23919
   901
apply (insert unit_id)
ballarin@23919
   902
apply simp
ballarin@23919
   903
apply (rule the_equality)
ballarin@23919
   904
apply rule
ballarin@23919
   905
apply rule
ballarin@23919
   906
apply simp
ballarin@23919
   907
done
ballarin@23919
   908
qed
ballarin@23919
   909
ballarin@23919
   910
thm Dfun.unit_l_inv Dfun.l_inv
ballarin@23919
   911
ballarin@23919
   912
thm Dfun.inv_equality
ballarin@23919
   913
thm Dfun.inv_equality
ballarin@22657
   914
ballarin@22657
   915
end