src/FOL/ex/Locale_Test/Locale_Test1.thy
author ballarin
Wed May 26 21:20:18 2010 +0200 (2010-05-26)
changeset 37134 29bd6c2ffba8
child 37146 f652333bbf8e
permissions -rw-r--r--
Revise locale test theory layout.
ballarin@37134
     1
(*  Title:      FOL/ex/Locale_Test/Locale_Test1.thy
ballarin@37134
     2
    Author:     Clemens Ballarin, TU Muenchen
ballarin@37134
     3
ballarin@37134
     4
Test environment for the locale implementation.
ballarin@37134
     5
*)
ballarin@37134
     6
ballarin@37134
     7
theory Locale_Test1
ballarin@37134
     8
imports FOL
ballarin@37134
     9
begin
ballarin@37134
    10
ballarin@37134
    11
typedecl int arities int :: "term"
ballarin@37134
    12
consts plus :: "int => int => int" (infixl "+" 60)
ballarin@37134
    13
  zero :: int ("0")
ballarin@37134
    14
  minus :: "int => int" ("- _")
ballarin@37134
    15
ballarin@37134
    16
axioms
ballarin@37134
    17
  int_assoc: "(x + y::int) + z = x + (y + z)"
ballarin@37134
    18
  int_zero: "0 + x = x"
ballarin@37134
    19
  int_minus: "(-x) + x = 0"
ballarin@37134
    20
  int_minus2: "-(-x) = x"
ballarin@37134
    21
ballarin@37134
    22
section {* Inference of parameter types *}
ballarin@37134
    23
ballarin@37134
    24
locale param1 = fixes p
ballarin@37134
    25
print_locale! param1
ballarin@37134
    26
ballarin@37134
    27
locale param2 = fixes p :: 'b
ballarin@37134
    28
print_locale! param2
ballarin@37134
    29
ballarin@37134
    30
(*
ballarin@37134
    31
locale param_top = param2 r for r :: "'b :: {}"
ballarin@37134
    32
  Fails, cannot generalise parameter.
ballarin@37134
    33
*)
ballarin@37134
    34
ballarin@37134
    35
locale param3 = fixes p (infix ".." 50)
ballarin@37134
    36
print_locale! param3
ballarin@37134
    37
ballarin@37134
    38
locale param4 = fixes p :: "'a => 'a => 'a" (infix ".." 50)
ballarin@37134
    39
print_locale! param4
ballarin@37134
    40
ballarin@37134
    41
ballarin@37134
    42
subsection {* Incremental type constraints *}
ballarin@37134
    43
ballarin@37134
    44
locale constraint1 =
ballarin@37134
    45
  fixes  prod (infixl "**" 65)
ballarin@37134
    46
  assumes l_id: "x ** y = x"
ballarin@37134
    47
  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
ballarin@37134
    48
print_locale! constraint1
ballarin@37134
    49
ballarin@37134
    50
locale constraint2 =
ballarin@37134
    51
  fixes p and q
ballarin@37134
    52
  assumes "p = q"
ballarin@37134
    53
print_locale! constraint2
ballarin@37134
    54
ballarin@37134
    55
ballarin@37134
    56
section {* Inheritance *}
ballarin@37134
    57
ballarin@37134
    58
locale semi =
ballarin@37134
    59
  fixes prod (infixl "**" 65)
ballarin@37134
    60
  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
ballarin@37134
    61
print_locale! semi thm semi_def
ballarin@37134
    62
ballarin@37134
    63
locale lgrp = semi +
ballarin@37134
    64
  fixes one and inv
ballarin@37134
    65
  assumes lone: "one ** x = x"
ballarin@37134
    66
    and linv: "inv(x) ** x = one"
ballarin@37134
    67
print_locale! lgrp thm lgrp_def lgrp_axioms_def
ballarin@37134
    68
ballarin@37134
    69
locale add_lgrp = semi "op ++" for sum (infixl "++" 60) +
ballarin@37134
    70
  fixes zero and neg
ballarin@37134
    71
  assumes lzero: "zero ++ x = x"
ballarin@37134
    72
    and lneg: "neg(x) ++ x = zero"
ballarin@37134
    73
print_locale! add_lgrp thm add_lgrp_def add_lgrp_axioms_def
ballarin@37134
    74
ballarin@37134
    75
locale rev_lgrp = semi "%x y. y ++ x" for sum (infixl "++" 60)
ballarin@37134
    76
print_locale! rev_lgrp thm rev_lgrp_def
ballarin@37134
    77
ballarin@37134
    78
locale hom = f: semi f + g: semi g for f and g
ballarin@37134
    79
print_locale! hom thm hom_def
ballarin@37134
    80
ballarin@37134
    81
locale perturbation = semi + d: semi "%x y. delta(x) ** delta(y)" for delta
ballarin@37134
    82
print_locale! perturbation thm perturbation_def
ballarin@37134
    83
ballarin@37134
    84
locale pert_hom = d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2
ballarin@37134
    85
print_locale! pert_hom thm pert_hom_def
ballarin@37134
    86
ballarin@37134
    87
text {* Alternative expression, obtaining nicer names in @{text "semi f"}. *}
ballarin@37134
    88
locale pert_hom' = semi f + d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2
ballarin@37134
    89
print_locale! pert_hom' thm pert_hom'_def
ballarin@37134
    90
ballarin@37134
    91
ballarin@37134
    92
section {* Syntax declarations *}
ballarin@37134
    93
ballarin@37134
    94
locale logic =
ballarin@37134
    95
  fixes land (infixl "&&" 55)
ballarin@37134
    96
    and lnot ("-- _" [60] 60)
ballarin@37134
    97
  assumes assoc: "(x && y) && z = x && (y && z)"
ballarin@37134
    98
    and notnot: "-- (-- x) = x"
ballarin@37134
    99
begin
ballarin@37134
   100
ballarin@37134
   101
definition lor (infixl "||" 50) where
ballarin@37134
   102
  "x || y = --(-- x && -- y)"
ballarin@37134
   103
ballarin@37134
   104
end
ballarin@37134
   105
print_locale! logic
ballarin@37134
   106
ballarin@37134
   107
locale use_decl = logic + semi "op ||"
ballarin@37134
   108
print_locale! use_decl thm use_decl_def
ballarin@37134
   109
ballarin@37134
   110
locale extra_type =
ballarin@37134
   111
  fixes a :: 'a
ballarin@37134
   112
    and P :: "'a => 'b => o"
ballarin@37134
   113
begin
ballarin@37134
   114
ballarin@37134
   115
definition test :: "'a => o" where
ballarin@37134
   116
  "test(x) <-> (ALL b. P(x, b))"
ballarin@37134
   117
ballarin@37134
   118
end
ballarin@37134
   119
ballarin@37134
   120
term extra_type.test thm extra_type.test_def
ballarin@37134
   121
ballarin@37134
   122
interpretation var?: extra_type "0" "%x y. x = 0" .
ballarin@37134
   123
ballarin@37134
   124
thm var.test_def
ballarin@37134
   125
ballarin@37134
   126
ballarin@37134
   127
text {* Under which circumstances term syntax remains active. *}
ballarin@37134
   128
ballarin@37134
   129
locale "syntax" =
ballarin@37134
   130
  fixes p1 :: "'a => 'b"
ballarin@37134
   131
    and p2 :: "'b => o"
ballarin@37134
   132
begin
ballarin@37134
   133
ballarin@37134
   134
definition d1 :: "'a => o" where "d1(x) <-> ~ p2(p1(x))"
ballarin@37134
   135
definition d2 :: "'b => o" where "d2(x) <-> ~ p2(x)"
ballarin@37134
   136
ballarin@37134
   137
thm d1_def d2_def
ballarin@37134
   138
ballarin@37134
   139
end
ballarin@37134
   140
ballarin@37134
   141
thm syntax.d1_def syntax.d2_def
ballarin@37134
   142
ballarin@37134
   143
locale syntax' = "syntax" p1 p2 for p1 :: "'a => 'a" and p2 :: "'a => o"
ballarin@37134
   144
begin
ballarin@37134
   145
ballarin@37134
   146
thm d1_def d2_def  (* should print as "d1(?x) <-> ..." and "d2(?x) <-> ..." *)
ballarin@37134
   147
ballarin@37134
   148
ML {*
ballarin@37134
   149
  fun check_syntax ctxt thm expected =
ballarin@37134
   150
    let
ballarin@37134
   151
      val obtained = PrintMode.setmp [] (Display.string_of_thm ctxt) thm;
ballarin@37134
   152
    in
ballarin@37134
   153
      if obtained <> expected
ballarin@37134
   154
      then error ("Theorem syntax '" ^ obtained ^ "' obtained, but '" ^ expected ^ "' expected.")
ballarin@37134
   155
      else ()
ballarin@37134
   156
    end;
ballarin@37134
   157
*}
ballarin@37134
   158
ballarin@37134
   159
ML {*
ballarin@37134
   160
  check_syntax @{context} @{thm d1_def} "d1(?x) <-> ~ p2(p1(?x))";
ballarin@37134
   161
  check_syntax @{context} @{thm d2_def} "d2(?x) <-> ~ p2(?x)";
ballarin@37134
   162
*}
ballarin@37134
   163
ballarin@37134
   164
end
ballarin@37134
   165
ballarin@37134
   166
locale syntax'' = "syntax" p3 p2 for p3 :: "'a => 'b" and p2 :: "'b => o"
ballarin@37134
   167
begin
ballarin@37134
   168
ballarin@37134
   169
thm d1_def d2_def
ballarin@37134
   170
  (* should print as "syntax.d1(p3, p2, ?x) <-> ..." and "d2(?x) <-> ..." *)
ballarin@37134
   171
ballarin@37134
   172
ML {*
ballarin@37134
   173
  check_syntax @{context} @{thm d1_def} "syntax.d1(p3, p2, ?x) <-> ~ p2(p3(?x))";
ballarin@37134
   174
  check_syntax @{context} @{thm d2_def} "d2(?x) <-> ~ p2(?x)";
ballarin@37134
   175
*}
ballarin@37134
   176
ballarin@37134
   177
end
ballarin@37134
   178
ballarin@37134
   179
ballarin@37134
   180
section {* Foundational versions of theorems *}
ballarin@37134
   181
ballarin@37134
   182
thm logic.assoc
ballarin@37134
   183
thm logic.lor_def
ballarin@37134
   184
ballarin@37134
   185
ballarin@37134
   186
section {* Defines *}
ballarin@37134
   187
ballarin@37134
   188
locale logic_def =
ballarin@37134
   189
  fixes land (infixl "&&" 55)
ballarin@37134
   190
    and lor (infixl "||" 50)
ballarin@37134
   191
    and lnot ("-- _" [60] 60)
ballarin@37134
   192
  assumes assoc: "(x && y) && z = x && (y && z)"
ballarin@37134
   193
    and notnot: "-- (-- x) = x"
ballarin@37134
   194
  defines "x || y == --(-- x && -- y)"
ballarin@37134
   195
begin
ballarin@37134
   196
ballarin@37134
   197
thm lor_def
ballarin@37134
   198
ballarin@37134
   199
lemma "x || y = --(-- x && --y)"
ballarin@37134
   200
  by (unfold lor_def) (rule refl)
ballarin@37134
   201
ballarin@37134
   202
end
ballarin@37134
   203
ballarin@37134
   204
(* Inheritance of defines *)
ballarin@37134
   205
ballarin@37134
   206
locale logic_def2 = logic_def
ballarin@37134
   207
begin
ballarin@37134
   208
ballarin@37134
   209
lemma "x || y = --(-- x && --y)"
ballarin@37134
   210
  by (unfold lor_def) (rule refl)
ballarin@37134
   211
ballarin@37134
   212
end
ballarin@37134
   213
ballarin@37134
   214
ballarin@37134
   215
section {* Notes *}
ballarin@37134
   216
ballarin@37134
   217
(* A somewhat arcane homomorphism example *)
ballarin@37134
   218
ballarin@37134
   219
definition semi_hom where
ballarin@37134
   220
  "semi_hom(prod, sum, h) <-> (ALL x y. h(prod(x, y)) = sum(h(x), h(y)))"
ballarin@37134
   221
ballarin@37134
   222
lemma semi_hom_mult:
ballarin@37134
   223
  "semi_hom(prod, sum, h) ==> h(prod(x, y)) = sum(h(x), h(y))"
ballarin@37134
   224
  by (simp add: semi_hom_def)
ballarin@37134
   225
ballarin@37134
   226
locale semi_hom_loc = prod: semi prod + sum: semi sum
ballarin@37134
   227
  for prod and sum and h +
ballarin@37134
   228
  assumes semi_homh: "semi_hom(prod, sum, h)"
ballarin@37134
   229
  notes semi_hom_mult = semi_hom_mult [OF semi_homh]
ballarin@37134
   230
ballarin@37134
   231
thm semi_hom_loc.semi_hom_mult
ballarin@37134
   232
(* unspecified, attribute not applied in backgroud theory !!! *)
ballarin@37134
   233
ballarin@37134
   234
lemma (in semi_hom_loc) "h(prod(x, y)) = sum(h(x), h(y))"
ballarin@37134
   235
  by (rule semi_hom_mult)
ballarin@37134
   236
ballarin@37134
   237
(* Referring to facts from within a context specification *)
ballarin@37134
   238
ballarin@37134
   239
lemma
ballarin@37134
   240
  assumes x: "P <-> P"
ballarin@37134
   241
  notes y = x
ballarin@37134
   242
  shows True ..
ballarin@37134
   243
ballarin@37134
   244
ballarin@37134
   245
section {* Theorem statements *}
ballarin@37134
   246
ballarin@37134
   247
lemma (in lgrp) lcancel:
ballarin@37134
   248
  "x ** y = x ** z <-> y = z"
ballarin@37134
   249
proof
ballarin@37134
   250
  assume "x ** y = x ** z"
ballarin@37134
   251
  then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
ballarin@37134
   252
  then show "y = z" by (simp add: lone linv)
ballarin@37134
   253
qed simp
ballarin@37134
   254
print_locale! lgrp
ballarin@37134
   255
ballarin@37134
   256
ballarin@37134
   257
locale rgrp = semi +
ballarin@37134
   258
  fixes one and inv
ballarin@37134
   259
  assumes rone: "x ** one = x"
ballarin@37134
   260
    and rinv: "x ** inv(x) = one"
ballarin@37134
   261
begin
ballarin@37134
   262
ballarin@37134
   263
lemma rcancel:
ballarin@37134
   264
  "y ** x = z ** x <-> y = z"
ballarin@37134
   265
proof
ballarin@37134
   266
  assume "y ** x = z ** x"
ballarin@37134
   267
  then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
ballarin@37134
   268
    by (simp add: assoc [symmetric])
ballarin@37134
   269
  then show "y = z" by (simp add: rone rinv)
ballarin@37134
   270
qed simp
ballarin@37134
   271
ballarin@37134
   272
end
ballarin@37134
   273
print_locale! rgrp
ballarin@37134
   274
ballarin@37134
   275
ballarin@37134
   276
subsection {* Patterns *}
ballarin@37134
   277
ballarin@37134
   278
lemma (in rgrp)
ballarin@37134
   279
  assumes "y ** x = z ** x" (is ?a)
ballarin@37134
   280
  shows "y = z" (is ?t)
ballarin@37134
   281
proof -
ballarin@37134
   282
  txt {* Weird proof involving patterns from context element and conclusion. *}
ballarin@37134
   283
  {
ballarin@37134
   284
    assume ?a
ballarin@37134
   285
    then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
ballarin@37134
   286
      by (simp add: assoc [symmetric])
ballarin@37134
   287
    then have ?t by (simp add: rone rinv)
ballarin@37134
   288
  }
ballarin@37134
   289
  note x = this
ballarin@37134
   290
  show ?t by (rule x [OF `?a`])
ballarin@37134
   291
qed
ballarin@37134
   292
ballarin@37134
   293
ballarin@37134
   294
section {* Interpretation between locales: sublocales *}
ballarin@37134
   295
ballarin@37134
   296
sublocale lgrp < right: rgrp
ballarin@37134
   297
print_facts
ballarin@37134
   298
proof unfold_locales
ballarin@37134
   299
  {
ballarin@37134
   300
    fix x
ballarin@37134
   301
    have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
ballarin@37134
   302
    then show "x ** one = x" by (simp add: assoc lcancel)
ballarin@37134
   303
  }
ballarin@37134
   304
  note rone = this
ballarin@37134
   305
  {
ballarin@37134
   306
    fix x
ballarin@37134
   307
    have "inv(x) ** x ** inv(x) = inv(x) ** one"
ballarin@37134
   308
      by (simp add: linv lone rone)
ballarin@37134
   309
    then show "x ** inv(x) = one" by (simp add: assoc lcancel)
ballarin@37134
   310
  }
ballarin@37134
   311
qed
ballarin@37134
   312
ballarin@37134
   313
(* effect on printed locale *)
ballarin@37134
   314
ballarin@37134
   315
print_locale! lgrp
ballarin@37134
   316
ballarin@37134
   317
(* use of derived theorem *)
ballarin@37134
   318
ballarin@37134
   319
lemma (in lgrp)
ballarin@37134
   320
  "y ** x = z ** x <-> y = z"
ballarin@37134
   321
  apply (rule rcancel)
ballarin@37134
   322
  done
ballarin@37134
   323
ballarin@37134
   324
(* circular interpretation *)
ballarin@37134
   325
ballarin@37134
   326
sublocale rgrp < left: lgrp
ballarin@37134
   327
proof unfold_locales
ballarin@37134
   328
  {
ballarin@37134
   329
    fix x
ballarin@37134
   330
    have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone)
ballarin@37134
   331
    then show "one ** x = x" by (simp add: assoc [symmetric] rcancel)
ballarin@37134
   332
  }
ballarin@37134
   333
  note lone = this
ballarin@37134
   334
  {
ballarin@37134
   335
    fix x
ballarin@37134
   336
    have "inv(x) ** (x ** inv(x)) = one ** inv(x)"
ballarin@37134
   337
      by (simp add: rinv lone rone)
ballarin@37134
   338
    then show "inv(x) ** x = one" by (simp add: assoc [symmetric] rcancel)
ballarin@37134
   339
  }
ballarin@37134
   340
qed
ballarin@37134
   341
ballarin@37134
   342
(* effect on printed locale *)
ballarin@37134
   343
ballarin@37134
   344
print_locale! rgrp
ballarin@37134
   345
print_locale! lgrp
ballarin@37134
   346
ballarin@37134
   347
ballarin@37134
   348
(* Duality *)
ballarin@37134
   349
ballarin@37134
   350
locale order =
ballarin@37134
   351
  fixes less :: "'a => 'a => o" (infix "<<" 50)
ballarin@37134
   352
  assumes refl: "x << x"
ballarin@37134
   353
    and trans: "[| x << y; y << z |] ==> x << z"
ballarin@37134
   354
ballarin@37134
   355
sublocale order < dual: order "%x y. y << x"
ballarin@37134
   356
  apply unfold_locales apply (rule refl) apply (blast intro: trans)
ballarin@37134
   357
  done
ballarin@37134
   358
ballarin@37134
   359
print_locale! order  (* Only two instances of order. *)
ballarin@37134
   360
ballarin@37134
   361
locale order' =
ballarin@37134
   362
  fixes less :: "'a => 'a => o" (infix "<<" 50)
ballarin@37134
   363
  assumes refl: "x << x"
ballarin@37134
   364
    and trans: "[| x << y; y << z |] ==> x << z"
ballarin@37134
   365
ballarin@37134
   366
locale order_with_def = order'
ballarin@37134
   367
begin
ballarin@37134
   368
ballarin@37134
   369
definition greater :: "'a => 'a => o" (infix ">>" 50) where
ballarin@37134
   370
  "x >> y <-> y << x"
ballarin@37134
   371
ballarin@37134
   372
end
ballarin@37134
   373
ballarin@37134
   374
sublocale order_with_def < dual: order' "op >>"
ballarin@37134
   375
  apply unfold_locales
ballarin@37134
   376
  unfolding greater_def
ballarin@37134
   377
  apply (rule refl) apply (blast intro: trans)
ballarin@37134
   378
  done
ballarin@37134
   379
ballarin@37134
   380
print_locale! order_with_def
ballarin@37134
   381
(* Note that decls come after theorems that make use of them. *)
ballarin@37134
   382
ballarin@37134
   383
ballarin@37134
   384
(* locale with many parameters ---
ballarin@37134
   385
   interpretations generate alternating group A5 *)
ballarin@37134
   386
ballarin@37134
   387
ballarin@37134
   388
locale A5 =
ballarin@37134
   389
  fixes A and B and C and D and E
ballarin@37134
   390
  assumes eq: "A <-> B <-> C <-> D <-> E"
ballarin@37134
   391
ballarin@37134
   392
sublocale A5 < 1: A5 _ _ D E C
ballarin@37134
   393
print_facts
ballarin@37134
   394
  using eq apply (blast intro: A5.intro) done
ballarin@37134
   395
ballarin@37134
   396
sublocale A5 < 2: A5 C _ E _ A
ballarin@37134
   397
print_facts
ballarin@37134
   398
  using eq apply (blast intro: A5.intro) done
ballarin@37134
   399
ballarin@37134
   400
sublocale A5 < 3: A5 B C A _ _
ballarin@37134
   401
print_facts
ballarin@37134
   402
  using eq apply (blast intro: A5.intro) done
ballarin@37134
   403
ballarin@37134
   404
(* Any even permutation of parameters is subsumed by the above. *)
ballarin@37134
   405
ballarin@37134
   406
print_locale! A5
ballarin@37134
   407
ballarin@37134
   408
ballarin@37134
   409
(* Free arguments of instance *)
ballarin@37134
   410
ballarin@37134
   411
locale trivial =
ballarin@37134
   412
  fixes P and Q :: o
ballarin@37134
   413
  assumes Q: "P <-> P <-> Q"
ballarin@37134
   414
begin
ballarin@37134
   415
ballarin@37134
   416
lemma Q_triv: "Q" using Q by fast
ballarin@37134
   417
ballarin@37134
   418
end
ballarin@37134
   419
ballarin@37134
   420
sublocale trivial < x: trivial x _
ballarin@37134
   421
  apply unfold_locales using Q by fast
ballarin@37134
   422
ballarin@37134
   423
print_locale! trivial
ballarin@37134
   424
ballarin@37134
   425
context trivial begin thm x.Q [where ?x = True] end
ballarin@37134
   426
ballarin@37134
   427
sublocale trivial < y: trivial Q Q
ballarin@37134
   428
  by unfold_locales
ballarin@37134
   429
  (* Succeeds since previous interpretation is more general. *)
ballarin@37134
   430
ballarin@37134
   431
print_locale! trivial  (* No instance for y created (subsumed). *)
ballarin@37134
   432
ballarin@37134
   433
ballarin@37134
   434
subsection {* Sublocale, then interpretation in theory *}
ballarin@37134
   435
ballarin@37134
   436
interpretation int?: lgrp "op +" "0" "minus"
ballarin@37134
   437
proof unfold_locales
ballarin@37134
   438
qed (rule int_assoc int_zero int_minus)+
ballarin@37134
   439
ballarin@37134
   440
thm int.assoc int.semi_axioms
ballarin@37134
   441
ballarin@37134
   442
interpretation int2?: semi "op +"
ballarin@37134
   443
  by unfold_locales  (* subsumed, thm int2.assoc not generated *)
ballarin@37134
   444
ballarin@37134
   445
ML {* (PureThy.get_thms @{theory} "int2.assoc";
ballarin@37134
   446
    error "thm int2.assoc was generated")
ballarin@37134
   447
  handle ERROR "Unknown fact \"int2.assoc\"" => ([]:thm list); *}
ballarin@37134
   448
ballarin@37134
   449
thm int.lone int.right.rone
ballarin@37134
   450
  (* the latter comes through the sublocale relation *)
ballarin@37134
   451
ballarin@37134
   452
ballarin@37134
   453
subsection {* Interpretation in theory, then sublocale *}
ballarin@37134
   454
ballarin@37134
   455
interpretation fol: logic "op +" "minus"
ballarin@37134
   456
  by unfold_locales (rule int_assoc int_minus2)+
ballarin@37134
   457
ballarin@37134
   458
locale logic2 =
ballarin@37134
   459
  fixes land (infixl "&&" 55)
ballarin@37134
   460
    and lnot ("-- _" [60] 60)
ballarin@37134
   461
  assumes assoc: "(x && y) && z = x && (y && z)"
ballarin@37134
   462
    and notnot: "-- (-- x) = x"
ballarin@37134
   463
begin
ballarin@37134
   464
ballarin@37134
   465
definition lor (infixl "||" 50) where
ballarin@37134
   466
  "x || y = --(-- x && -- y)"
ballarin@37134
   467
ballarin@37134
   468
end
ballarin@37134
   469
ballarin@37134
   470
sublocale logic < two: logic2
ballarin@37134
   471
  by unfold_locales (rule assoc notnot)+
ballarin@37134
   472
ballarin@37134
   473
thm fol.two.assoc
ballarin@37134
   474
ballarin@37134
   475
ballarin@37134
   476
subsection {* Declarations and sublocale *}
ballarin@37134
   477
ballarin@37134
   478
locale logic_a = logic
ballarin@37134
   479
locale logic_b = logic
ballarin@37134
   480
ballarin@37134
   481
sublocale logic_a < logic_b
ballarin@37134
   482
  by unfold_locales
ballarin@37134
   483
ballarin@37134
   484
ballarin@37134
   485
subsection {* Equations *}
ballarin@37134
   486
ballarin@37134
   487
locale logic_o =
ballarin@37134
   488
  fixes land (infixl "&&" 55)
ballarin@37134
   489
    and lnot ("-- _" [60] 60)
ballarin@37134
   490
  assumes assoc_o: "(x && y) && z <-> x && (y && z)"
ballarin@37134
   491
    and notnot_o: "-- (-- x) <-> x"
ballarin@37134
   492
begin
ballarin@37134
   493
ballarin@37134
   494
definition lor_o (infixl "||" 50) where
ballarin@37134
   495
  "x || y <-> --(-- x && -- y)"
ballarin@37134
   496
ballarin@37134
   497
end
ballarin@37134
   498
ballarin@37134
   499
interpretation x: logic_o "op &" "Not"
ballarin@37134
   500
  where bool_logic_o: "logic_o.lor_o(op &, Not, x, y) <-> x | y"
ballarin@37134
   501
proof -
ballarin@37134
   502
  show bool_logic_o: "PROP logic_o(op &, Not)" by unfold_locales fast+
ballarin@37134
   503
  show "logic_o.lor_o(op &, Not, x, y) <-> x | y"
ballarin@37134
   504
    by (unfold logic_o.lor_o_def [OF bool_logic_o]) fast
ballarin@37134
   505
qed
ballarin@37134
   506
ballarin@37134
   507
thm x.lor_o_def bool_logic_o
ballarin@37134
   508
ballarin@37134
   509
lemma lor_triv: "z <-> z" ..
ballarin@37134
   510
ballarin@37134
   511
lemma (in logic_o) lor_triv: "x || y <-> x || y" by fast
ballarin@37134
   512
ballarin@37134
   513
thm lor_triv [where z = True] (* Check strict prefix. *)
ballarin@37134
   514
  x.lor_triv
ballarin@37134
   515
ballarin@37134
   516
ballarin@37134
   517
subsection {* Inheritance of mixins *}
ballarin@37134
   518
ballarin@37134
   519
locale reflexive =
ballarin@37134
   520
  fixes le :: "'a => 'a => o" (infix "\<sqsubseteq>" 50)
ballarin@37134
   521
  assumes refl: "x \<sqsubseteq> x"
ballarin@37134
   522
begin
ballarin@37134
   523
ballarin@37134
   524
definition less (infix "\<sqsubset>" 50) where "x \<sqsubset> y <-> x \<sqsubseteq> y & x ~= y"
ballarin@37134
   525
ballarin@37134
   526
end
ballarin@37134
   527
ballarin@37134
   528
consts
ballarin@37134
   529
  gle :: "'a => 'a => o" gless :: "'a => 'a => o"
ballarin@37134
   530
  gle' :: "'a => 'a => o" gless' :: "'a => 'a => o"
ballarin@37134
   531
ballarin@37134
   532
axioms
ballarin@37134
   533
  grefl: "gle(x, x)" gless_def: "gless(x, y) <-> gle(x, y) & x ~= y"
ballarin@37134
   534
  grefl': "gle'(x, x)" gless'_def: "gless'(x, y) <-> gle'(x, y) & x ~= y"
ballarin@37134
   535
ballarin@37134
   536
text {* Setup *}
ballarin@37134
   537
ballarin@37134
   538
locale mixin = reflexive
ballarin@37134
   539
begin
ballarin@37134
   540
lemmas less_thm = less_def
ballarin@37134
   541
end
ballarin@37134
   542
ballarin@37134
   543
interpretation le: mixin gle where "reflexive.less(gle, x, y) <-> gless(x, y)"
ballarin@37134
   544
proof -
ballarin@37134
   545
  show "mixin(gle)" by unfold_locales (rule grefl)
ballarin@37134
   546
  note reflexive = this[unfolded mixin_def]
ballarin@37134
   547
  show "reflexive.less(gle, x, y) <-> gless(x, y)"
ballarin@37134
   548
    by (simp add: reflexive.less_def[OF reflexive] gless_def)
ballarin@37134
   549
qed
ballarin@37134
   550
ballarin@37134
   551
text {* Mixin propagated along the locale hierarchy *}
ballarin@37134
   552
ballarin@37134
   553
locale mixin2 = mixin
ballarin@37134
   554
begin
ballarin@37134
   555
lemmas less_thm2 = less_def
ballarin@37134
   556
end
ballarin@37134
   557
ballarin@37134
   558
interpretation le: mixin2 gle
ballarin@37134
   559
  by unfold_locales
ballarin@37134
   560
ballarin@37134
   561
thm le.less_thm2  (* mixin applied *)
ballarin@37134
   562
lemma "gless(x, y) <-> gle(x, y) & x ~= y"
ballarin@37134
   563
  by (rule le.less_thm2)
ballarin@37134
   564
ballarin@37134
   565
text {* Mixin does not leak to a side branch. *}
ballarin@37134
   566
ballarin@37134
   567
locale mixin3 = reflexive
ballarin@37134
   568
begin
ballarin@37134
   569
lemmas less_thm3 = less_def
ballarin@37134
   570
end
ballarin@37134
   571
ballarin@37134
   572
interpretation le: mixin3 gle
ballarin@37134
   573
  by unfold_locales
ballarin@37134
   574
ballarin@37134
   575
thm le.less_thm3  (* mixin not applied *)
ballarin@37134
   576
lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y" by (rule le.less_thm3)
ballarin@37134
   577
ballarin@37134
   578
text {* Mixin only available in original context *}
ballarin@37134
   579
ballarin@37134
   580
locale mixin4_base = reflexive
ballarin@37134
   581
ballarin@37134
   582
locale mixin4_mixin = mixin4_base
ballarin@37134
   583
ballarin@37134
   584
interpretation le: mixin4_mixin gle
ballarin@37134
   585
  where "reflexive.less(gle, x, y) <-> gless(x, y)"
ballarin@37134
   586
proof -
ballarin@37134
   587
  show "mixin4_mixin(gle)" by unfold_locales (rule grefl)
ballarin@37134
   588
  note reflexive = this[unfolded mixin4_mixin_def mixin4_base_def mixin_def]
ballarin@37134
   589
  show "reflexive.less(gle, x, y) <-> gless(x, y)"
ballarin@37134
   590
    by (simp add: reflexive.less_def[OF reflexive] gless_def)
ballarin@37134
   591
qed
ballarin@37134
   592
ballarin@37134
   593
locale mixin4_copy = mixin4_base
ballarin@37134
   594
begin
ballarin@37134
   595
lemmas less_thm4 = less_def
ballarin@37134
   596
end
ballarin@37134
   597
ballarin@37134
   598
locale mixin4_combined = le1: mixin4_mixin le' + le2: mixin4_copy le for le' le
ballarin@37134
   599
begin
ballarin@37134
   600
lemmas less_thm4' = less_def
ballarin@37134
   601
end
ballarin@37134
   602
ballarin@37134
   603
interpretation le4: mixin4_combined gle' gle
ballarin@37134
   604
  by unfold_locales (rule grefl')
ballarin@37134
   605
ballarin@37134
   606
thm le4.less_thm4' (* mixin not applied *)
ballarin@37134
   607
lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
ballarin@37134
   608
  by (rule le4.less_thm4')
ballarin@37134
   609
ballarin@37134
   610
text {* Inherited mixin applied to new theorem *}
ballarin@37134
   611
ballarin@37134
   612
locale mixin5_base = reflexive
ballarin@37134
   613
ballarin@37134
   614
locale mixin5_inherited = mixin5_base
ballarin@37134
   615
ballarin@37134
   616
interpretation le5: mixin5_base gle
ballarin@37134
   617
  where "reflexive.less(gle, x, y) <-> gless(x, y)"
ballarin@37134
   618
proof -
ballarin@37134
   619
  show "mixin5_base(gle)" by unfold_locales
ballarin@37134
   620
  note reflexive = this[unfolded mixin5_base_def mixin_def]
ballarin@37134
   621
  show "reflexive.less(gle, x, y) <-> gless(x, y)"
ballarin@37134
   622
    by (simp add: reflexive.less_def[OF reflexive] gless_def)
ballarin@37134
   623
qed
ballarin@37134
   624
ballarin@37134
   625
interpretation le5: mixin5_inherited gle
ballarin@37134
   626
  by unfold_locales
ballarin@37134
   627
ballarin@37134
   628
lemmas (in mixin5_inherited) less_thm5 = less_def
ballarin@37134
   629
ballarin@37134
   630
thm le5.less_thm5  (* mixin applied *)
ballarin@37134
   631
lemma "gless(x, y) <-> gle(x, y) & x ~= y"
ballarin@37134
   632
  by (rule le5.less_thm5)
ballarin@37134
   633
ballarin@37134
   634
text {* Mixin pushed down to existing inherited locale *}
ballarin@37134
   635
ballarin@37134
   636
locale mixin6_base = reflexive
ballarin@37134
   637
ballarin@37134
   638
locale mixin6_inherited = mixin5_base
ballarin@37134
   639
ballarin@37134
   640
interpretation le6: mixin6_base gle
ballarin@37134
   641
  by unfold_locales
ballarin@37134
   642
interpretation le6: mixin6_inherited gle
ballarin@37134
   643
  by unfold_locales
ballarin@37134
   644
interpretation le6: mixin6_base gle
ballarin@37134
   645
  where "reflexive.less(gle, x, y) <-> gless(x, y)"
ballarin@37134
   646
proof -
ballarin@37134
   647
  show "mixin6_base(gle)" by unfold_locales
ballarin@37134
   648
  note reflexive = this[unfolded mixin6_base_def mixin_def]
ballarin@37134
   649
  show "reflexive.less(gle, x, y) <-> gless(x, y)"
ballarin@37134
   650
    by (simp add: reflexive.less_def[OF reflexive] gless_def)
ballarin@37134
   651
qed
ballarin@37134
   652
ballarin@37134
   653
lemmas (in mixin6_inherited) less_thm6 = less_def
ballarin@37134
   654
ballarin@37134
   655
thm le6.less_thm6  (* mixin applied *)
ballarin@37134
   656
lemma "gless(x, y) <-> gle(x, y) & x ~= y"
ballarin@37134
   657
  by (rule le6.less_thm6)
ballarin@37134
   658
ballarin@37134
   659
text {* Existing mixin inherited through sublocale relation *}
ballarin@37134
   660
ballarin@37134
   661
locale mixin7_base = reflexive
ballarin@37134
   662
ballarin@37134
   663
locale mixin7_inherited = reflexive
ballarin@37134
   664
ballarin@37134
   665
interpretation le7: mixin7_base gle
ballarin@37134
   666
  where "reflexive.less(gle, x, y) <-> gless(x, y)"
ballarin@37134
   667
proof -
ballarin@37134
   668
  show "mixin7_base(gle)" by unfold_locales
ballarin@37134
   669
  note reflexive = this[unfolded mixin7_base_def mixin_def]
ballarin@37134
   670
  show "reflexive.less(gle, x, y) <-> gless(x, y)"
ballarin@37134
   671
    by (simp add: reflexive.less_def[OF reflexive] gless_def)
ballarin@37134
   672
qed
ballarin@37134
   673
ballarin@37134
   674
interpretation le7: mixin7_inherited gle
ballarin@37134
   675
  by unfold_locales
ballarin@37134
   676
ballarin@37134
   677
lemmas (in mixin7_inherited) less_thm7 = less_def
ballarin@37134
   678
ballarin@37134
   679
thm le7.less_thm7  (* before, mixin not applied *)
ballarin@37134
   680
lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
ballarin@37134
   681
  by (rule le7.less_thm7)
ballarin@37134
   682
ballarin@37134
   683
sublocale mixin7_inherited < mixin7_base
ballarin@37134
   684
  by unfold_locales
ballarin@37134
   685
ballarin@37134
   686
lemmas (in mixin7_inherited) less_thm7b = less_def
ballarin@37134
   687
ballarin@37134
   688
thm le7.less_thm7b  (* after, mixin applied *)
ballarin@37134
   689
lemma "gless(x, y) <-> gle(x, y) & x ~= y"
ballarin@37134
   690
  by (rule le7.less_thm7b)
ballarin@37134
   691
ballarin@37134
   692
ballarin@37134
   693
text {* This locale will be interpreted in later theories. *}
ballarin@37134
   694
ballarin@37134
   695
locale mixin_thy_merge = le: reflexive le + le': reflexive le' for le le'
ballarin@37134
   696
ballarin@37134
   697
ballarin@37134
   698
subsection {* Interpretation in proofs *}
ballarin@37134
   699
ballarin@37134
   700
lemma True
ballarin@37134
   701
proof
ballarin@37134
   702
  interpret "local": lgrp "op +" "0" "minus"
ballarin@37134
   703
    by unfold_locales  (* subsumed *)
ballarin@37134
   704
  {
ballarin@37134
   705
    fix zero :: int
ballarin@37134
   706
    assume "!!x. zero + x = x" "!!x. (-x) + x = zero"
ballarin@37134
   707
    then interpret local_fixed: lgrp "op +" zero "minus"
ballarin@37134
   708
      by unfold_locales
ballarin@37134
   709
    thm local_fixed.lone
ballarin@37134
   710
  }
ballarin@37134
   711
  assume "!!x zero. zero + x = x" "!!x zero. (-x) + x = zero"
ballarin@37134
   712
  then interpret local_free: lgrp "op +" zero "minus" for zero
ballarin@37134
   713
    by unfold_locales
ballarin@37134
   714
  thm local_free.lone [where ?zero = 0]
ballarin@37134
   715
qed
ballarin@37134
   716
ballarin@37134
   717
end