src/FOL/ex/Locale_Test/Locale_Test1.thy
author wenzelm
Wed Oct 10 15:39:01 2012 +0200 (2012-10-10)
changeset 49756 28e37eab4e6f
parent 43543 eb8b4851b039
child 51515 c3eb0b517ced
permissions -rw-r--r--
added some ad-hoc namespace prefixes to avoid duplicate facts;
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
wenzelm@41779
    16
axiomatization where
wenzelm@41779
    17
  int_assoc: "(x + y::int) + z = x + (y + z)" and
wenzelm@41779
    18
  int_zero: "0 + x = x" and
wenzelm@41779
    19
  int_minus: "(-x) + x = 0" and
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
wenzelm@49756
   107
locale use_decl = l: 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
wenzelm@37146
   151
      val obtained = Print_Mode.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
wenzelm@41305
   159
declare [[show_hyps]]
ballarin@41271
   160
ballarin@37134
   161
ML {*
ballarin@37134
   162
  check_syntax @{context} @{thm d1_def} "d1(?x) <-> ~ p2(p1(?x))";
ballarin@37134
   163
  check_syntax @{context} @{thm d2_def} "d2(?x) <-> ~ p2(?x)";
ballarin@37134
   164
*}
ballarin@37134
   165
ballarin@37134
   166
end
ballarin@37134
   167
ballarin@37134
   168
locale syntax'' = "syntax" p3 p2 for p3 :: "'a => 'b" and p2 :: "'b => o"
ballarin@37134
   169
begin
ballarin@37134
   170
ballarin@37134
   171
thm d1_def d2_def
ballarin@37134
   172
  (* should print as "syntax.d1(p3, p2, ?x) <-> ..." and "d2(?x) <-> ..." *)
ballarin@37134
   173
ballarin@37134
   174
ML {*
ballarin@37134
   175
  check_syntax @{context} @{thm d1_def} "syntax.d1(p3, p2, ?x) <-> ~ p2(p3(?x))";
ballarin@37134
   176
  check_syntax @{context} @{thm d2_def} "d2(?x) <-> ~ p2(?x)";
ballarin@37134
   177
*}
ballarin@37134
   178
ballarin@37134
   179
end
ballarin@37134
   180
ballarin@37134
   181
ballarin@37134
   182
section {* Foundational versions of theorems *}
ballarin@37134
   183
ballarin@37134
   184
thm logic.assoc
ballarin@37134
   185
thm logic.lor_def
ballarin@37134
   186
ballarin@37134
   187
ballarin@37134
   188
section {* Defines *}
ballarin@37134
   189
ballarin@37134
   190
locale logic_def =
ballarin@37134
   191
  fixes land (infixl "&&" 55)
ballarin@37134
   192
    and lor (infixl "||" 50)
ballarin@37134
   193
    and lnot ("-- _" [60] 60)
ballarin@37134
   194
  assumes assoc: "(x && y) && z = x && (y && z)"
ballarin@37134
   195
    and notnot: "-- (-- x) = x"
ballarin@37134
   196
  defines "x || y == --(-- x && -- y)"
ballarin@37134
   197
begin
ballarin@37134
   198
ballarin@37134
   199
thm lor_def
ballarin@37134
   200
ballarin@37134
   201
lemma "x || y = --(-- x && --y)"
ballarin@37134
   202
  by (unfold lor_def) (rule refl)
ballarin@37134
   203
ballarin@37134
   204
end
ballarin@37134
   205
ballarin@37134
   206
(* Inheritance of defines *)
ballarin@37134
   207
ballarin@37134
   208
locale logic_def2 = logic_def
ballarin@37134
   209
begin
ballarin@37134
   210
ballarin@37134
   211
lemma "x || y = --(-- x && --y)"
ballarin@37134
   212
  by (unfold lor_def) (rule refl)
ballarin@37134
   213
ballarin@37134
   214
end
ballarin@37134
   215
ballarin@37134
   216
ballarin@37134
   217
section {* Notes *}
ballarin@37134
   218
ballarin@37134
   219
(* A somewhat arcane homomorphism example *)
ballarin@37134
   220
ballarin@37134
   221
definition semi_hom where
ballarin@37134
   222
  "semi_hom(prod, sum, h) <-> (ALL x y. h(prod(x, y)) = sum(h(x), h(y)))"
ballarin@37134
   223
ballarin@37134
   224
lemma semi_hom_mult:
ballarin@37134
   225
  "semi_hom(prod, sum, h) ==> h(prod(x, y)) = sum(h(x), h(y))"
ballarin@37134
   226
  by (simp add: semi_hom_def)
ballarin@37134
   227
ballarin@37134
   228
locale semi_hom_loc = prod: semi prod + sum: semi sum
ballarin@37134
   229
  for prod and sum and h +
ballarin@37134
   230
  assumes semi_homh: "semi_hom(prod, sum, h)"
ballarin@37134
   231
  notes semi_hom_mult = semi_hom_mult [OF semi_homh]
ballarin@37134
   232
ballarin@37134
   233
thm semi_hom_loc.semi_hom_mult
ballarin@37134
   234
(* unspecified, attribute not applied in backgroud theory !!! *)
ballarin@37134
   235
ballarin@37134
   236
lemma (in semi_hom_loc) "h(prod(x, y)) = sum(h(x), h(y))"
ballarin@37134
   237
  by (rule semi_hom_mult)
ballarin@37134
   238
ballarin@37134
   239
(* Referring to facts from within a context specification *)
ballarin@37134
   240
ballarin@37134
   241
lemma
ballarin@37134
   242
  assumes x: "P <-> P"
ballarin@37134
   243
  notes y = x
ballarin@37134
   244
  shows True ..
ballarin@37134
   245
ballarin@37134
   246
ballarin@37134
   247
section {* Theorem statements *}
ballarin@37134
   248
ballarin@37134
   249
lemma (in lgrp) lcancel:
ballarin@37134
   250
  "x ** y = x ** z <-> y = z"
ballarin@37134
   251
proof
ballarin@37134
   252
  assume "x ** y = x ** z"
ballarin@37134
   253
  then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
ballarin@37134
   254
  then show "y = z" by (simp add: lone linv)
ballarin@37134
   255
qed simp
ballarin@37134
   256
print_locale! lgrp
ballarin@37134
   257
ballarin@37134
   258
ballarin@37134
   259
locale rgrp = semi +
ballarin@37134
   260
  fixes one and inv
ballarin@37134
   261
  assumes rone: "x ** one = x"
ballarin@37134
   262
    and rinv: "x ** inv(x) = one"
ballarin@37134
   263
begin
ballarin@37134
   264
ballarin@37134
   265
lemma rcancel:
ballarin@37134
   266
  "y ** x = z ** x <-> y = z"
ballarin@37134
   267
proof
ballarin@37134
   268
  assume "y ** x = z ** x"
ballarin@37134
   269
  then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
ballarin@37134
   270
    by (simp add: assoc [symmetric])
ballarin@37134
   271
  then show "y = z" by (simp add: rone rinv)
ballarin@37134
   272
qed simp
ballarin@37134
   273
ballarin@37134
   274
end
ballarin@37134
   275
print_locale! rgrp
ballarin@37134
   276
ballarin@37134
   277
ballarin@37134
   278
subsection {* Patterns *}
ballarin@37134
   279
ballarin@37134
   280
lemma (in rgrp)
ballarin@37134
   281
  assumes "y ** x = z ** x" (is ?a)
ballarin@37134
   282
  shows "y = z" (is ?t)
ballarin@37134
   283
proof -
ballarin@37134
   284
  txt {* Weird proof involving patterns from context element and conclusion. *}
ballarin@37134
   285
  {
ballarin@37134
   286
    assume ?a
ballarin@37134
   287
    then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
ballarin@37134
   288
      by (simp add: assoc [symmetric])
ballarin@37134
   289
    then have ?t by (simp add: rone rinv)
ballarin@37134
   290
  }
ballarin@37134
   291
  note x = this
ballarin@37134
   292
  show ?t by (rule x [OF `?a`])
ballarin@37134
   293
qed
ballarin@37134
   294
ballarin@37134
   295
ballarin@37134
   296
section {* Interpretation between locales: sublocales *}
ballarin@37134
   297
ballarin@37134
   298
sublocale lgrp < right: rgrp
ballarin@37134
   299
print_facts
ballarin@37134
   300
proof unfold_locales
ballarin@37134
   301
  {
ballarin@37134
   302
    fix x
ballarin@37134
   303
    have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
ballarin@37134
   304
    then show "x ** one = x" by (simp add: assoc lcancel)
ballarin@37134
   305
  }
ballarin@37134
   306
  note rone = this
ballarin@37134
   307
  {
ballarin@37134
   308
    fix x
ballarin@37134
   309
    have "inv(x) ** x ** inv(x) = inv(x) ** one"
ballarin@37134
   310
      by (simp add: linv lone rone)
ballarin@37134
   311
    then show "x ** inv(x) = one" by (simp add: assoc lcancel)
ballarin@37134
   312
  }
ballarin@37134
   313
qed
ballarin@37134
   314
ballarin@37134
   315
(* effect on printed locale *)
ballarin@37134
   316
ballarin@37134
   317
print_locale! lgrp
ballarin@37134
   318
ballarin@37134
   319
(* use of derived theorem *)
ballarin@37134
   320
ballarin@37134
   321
lemma (in lgrp)
ballarin@37134
   322
  "y ** x = z ** x <-> y = z"
ballarin@37134
   323
  apply (rule rcancel)
ballarin@37134
   324
  done
ballarin@37134
   325
ballarin@37134
   326
(* circular interpretation *)
ballarin@37134
   327
ballarin@37134
   328
sublocale rgrp < left: lgrp
ballarin@37134
   329
proof unfold_locales
ballarin@37134
   330
  {
ballarin@37134
   331
    fix x
ballarin@37134
   332
    have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone)
ballarin@37134
   333
    then show "one ** x = x" by (simp add: assoc [symmetric] rcancel)
ballarin@37134
   334
  }
ballarin@37134
   335
  note lone = this
ballarin@37134
   336
  {
ballarin@37134
   337
    fix x
ballarin@37134
   338
    have "inv(x) ** (x ** inv(x)) = one ** inv(x)"
ballarin@37134
   339
      by (simp add: rinv lone rone)
ballarin@37134
   340
    then show "inv(x) ** x = one" by (simp add: assoc [symmetric] rcancel)
ballarin@37134
   341
  }
ballarin@37134
   342
qed
ballarin@37134
   343
ballarin@37134
   344
(* effect on printed locale *)
ballarin@37134
   345
ballarin@37134
   346
print_locale! rgrp
ballarin@37134
   347
print_locale! lgrp
ballarin@37134
   348
ballarin@37134
   349
ballarin@37134
   350
(* Duality *)
ballarin@37134
   351
ballarin@37134
   352
locale order =
ballarin@37134
   353
  fixes less :: "'a => 'a => o" (infix "<<" 50)
ballarin@37134
   354
  assumes refl: "x << x"
ballarin@37134
   355
    and trans: "[| x << y; y << z |] ==> x << z"
ballarin@37134
   356
ballarin@37134
   357
sublocale order < dual: order "%x y. y << x"
ballarin@37134
   358
  apply unfold_locales apply (rule refl) apply (blast intro: trans)
ballarin@37134
   359
  done
ballarin@37134
   360
ballarin@37134
   361
print_locale! order  (* Only two instances of order. *)
ballarin@37134
   362
ballarin@37134
   363
locale order' =
ballarin@37134
   364
  fixes less :: "'a => 'a => o" (infix "<<" 50)
ballarin@37134
   365
  assumes refl: "x << x"
ballarin@37134
   366
    and trans: "[| x << y; y << z |] ==> x << z"
ballarin@37134
   367
ballarin@37134
   368
locale order_with_def = order'
ballarin@37134
   369
begin
ballarin@37134
   370
ballarin@37134
   371
definition greater :: "'a => 'a => o" (infix ">>" 50) where
ballarin@37134
   372
  "x >> y <-> y << x"
ballarin@37134
   373
ballarin@37134
   374
end
ballarin@37134
   375
ballarin@37134
   376
sublocale order_with_def < dual: order' "op >>"
ballarin@37134
   377
  apply unfold_locales
ballarin@37134
   378
  unfolding greater_def
ballarin@37134
   379
  apply (rule refl) apply (blast intro: trans)
ballarin@37134
   380
  done
ballarin@37134
   381
ballarin@37134
   382
print_locale! order_with_def
ballarin@37134
   383
(* Note that decls come after theorems that make use of them. *)
ballarin@37134
   384
ballarin@37134
   385
ballarin@37134
   386
(* locale with many parameters ---
ballarin@37134
   387
   interpretations generate alternating group A5 *)
ballarin@37134
   388
ballarin@37134
   389
ballarin@37134
   390
locale A5 =
ballarin@37134
   391
  fixes A and B and C and D and E
ballarin@37134
   392
  assumes eq: "A <-> B <-> C <-> D <-> E"
ballarin@37134
   393
ballarin@37134
   394
sublocale A5 < 1: A5 _ _ D E C
ballarin@37134
   395
print_facts
ballarin@37134
   396
  using eq apply (blast intro: A5.intro) done
ballarin@37134
   397
ballarin@37134
   398
sublocale A5 < 2: A5 C _ E _ A
ballarin@37134
   399
print_facts
ballarin@37134
   400
  using eq apply (blast intro: A5.intro) done
ballarin@37134
   401
ballarin@37134
   402
sublocale A5 < 3: A5 B C A _ _
ballarin@37134
   403
print_facts
ballarin@37134
   404
  using eq apply (blast intro: A5.intro) done
ballarin@37134
   405
ballarin@37134
   406
(* Any even permutation of parameters is subsumed by the above. *)
ballarin@37134
   407
ballarin@37134
   408
print_locale! A5
ballarin@37134
   409
ballarin@37134
   410
ballarin@37134
   411
(* Free arguments of instance *)
ballarin@37134
   412
ballarin@37134
   413
locale trivial =
ballarin@37134
   414
  fixes P and Q :: o
ballarin@37134
   415
  assumes Q: "P <-> P <-> Q"
ballarin@37134
   416
begin
ballarin@37134
   417
ballarin@37134
   418
lemma Q_triv: "Q" using Q by fast
ballarin@37134
   419
ballarin@37134
   420
end
ballarin@37134
   421
ballarin@37134
   422
sublocale trivial < x: trivial x _
ballarin@37134
   423
  apply unfold_locales using Q by fast
ballarin@37134
   424
ballarin@37134
   425
print_locale! trivial
ballarin@37134
   426
ballarin@37134
   427
context trivial begin thm x.Q [where ?x = True] end
ballarin@37134
   428
ballarin@37134
   429
sublocale trivial < y: trivial Q Q
ballarin@37134
   430
  by unfold_locales
ballarin@37134
   431
  (* Succeeds since previous interpretation is more general. *)
ballarin@37134
   432
ballarin@37134
   433
print_locale! trivial  (* No instance for y created (subsumed). *)
ballarin@37134
   434
ballarin@37134
   435
ballarin@37134
   436
subsection {* Sublocale, then interpretation in theory *}
ballarin@37134
   437
ballarin@37134
   438
interpretation int?: lgrp "op +" "0" "minus"
ballarin@37134
   439
proof unfold_locales
ballarin@37134
   440
qed (rule int_assoc int_zero int_minus)+
ballarin@37134
   441
ballarin@37134
   442
thm int.assoc int.semi_axioms
ballarin@37134
   443
ballarin@37134
   444
interpretation int2?: semi "op +"
ballarin@37134
   445
  by unfold_locales  (* subsumed, thm int2.assoc not generated *)
ballarin@37134
   446
wenzelm@39557
   447
ML {* (Global_Theory.get_thms @{theory} "int2.assoc";
ballarin@37134
   448
    error "thm int2.assoc was generated")
ballarin@37134
   449
  handle ERROR "Unknown fact \"int2.assoc\"" => ([]:thm list); *}
ballarin@37134
   450
ballarin@37134
   451
thm int.lone int.right.rone
ballarin@37134
   452
  (* the latter comes through the sublocale relation *)
ballarin@37134
   453
ballarin@37134
   454
ballarin@37134
   455
subsection {* Interpretation in theory, then sublocale *}
ballarin@37134
   456
ballarin@37134
   457
interpretation fol: logic "op +" "minus"
ballarin@37134
   458
  by unfold_locales (rule int_assoc int_minus2)+
ballarin@37134
   459
ballarin@37134
   460
locale logic2 =
ballarin@37134
   461
  fixes land (infixl "&&" 55)
ballarin@37134
   462
    and lnot ("-- _" [60] 60)
ballarin@37134
   463
  assumes assoc: "(x && y) && z = x && (y && z)"
ballarin@37134
   464
    and notnot: "-- (-- x) = x"
ballarin@37134
   465
begin
ballarin@37134
   466
ballarin@37134
   467
definition lor (infixl "||" 50) where
ballarin@37134
   468
  "x || y = --(-- x && -- y)"
ballarin@37134
   469
ballarin@37134
   470
end
ballarin@37134
   471
ballarin@37134
   472
sublocale logic < two: logic2
ballarin@37134
   473
  by unfold_locales (rule assoc notnot)+
ballarin@37134
   474
ballarin@37134
   475
thm fol.two.assoc
ballarin@37134
   476
ballarin@37134
   477
ballarin@37134
   478
subsection {* Declarations and sublocale *}
ballarin@37134
   479
ballarin@37134
   480
locale logic_a = logic
ballarin@37134
   481
locale logic_b = logic
ballarin@37134
   482
ballarin@37134
   483
sublocale logic_a < logic_b
ballarin@37134
   484
  by unfold_locales
ballarin@37134
   485
ballarin@37134
   486
ballarin@37134
   487
subsection {* Equations *}
ballarin@37134
   488
ballarin@37134
   489
locale logic_o =
ballarin@37134
   490
  fixes land (infixl "&&" 55)
ballarin@37134
   491
    and lnot ("-- _" [60] 60)
ballarin@37134
   492
  assumes assoc_o: "(x && y) && z <-> x && (y && z)"
ballarin@37134
   493
    and notnot_o: "-- (-- x) <-> x"
ballarin@37134
   494
begin
ballarin@37134
   495
ballarin@37134
   496
definition lor_o (infixl "||" 50) where
ballarin@37134
   497
  "x || y <-> --(-- x && -- y)"
ballarin@37134
   498
ballarin@37134
   499
end
ballarin@37134
   500
ballarin@37134
   501
interpretation x: logic_o "op &" "Not"
ballarin@43543
   502
  where bool_logic_o: "x.lor_o(x, y) <-> x | y"
ballarin@37134
   503
proof -
ballarin@37134
   504
  show bool_logic_o: "PROP logic_o(op &, Not)" by unfold_locales fast+
ballarin@37134
   505
  show "logic_o.lor_o(op &, Not, x, y) <-> x | y"
ballarin@37134
   506
    by (unfold logic_o.lor_o_def [OF bool_logic_o]) fast
ballarin@37134
   507
qed
ballarin@37134
   508
ballarin@37134
   509
thm x.lor_o_def bool_logic_o
ballarin@37134
   510
ballarin@37134
   511
lemma lor_triv: "z <-> z" ..
ballarin@37134
   512
ballarin@37134
   513
lemma (in logic_o) lor_triv: "x || y <-> x || y" by fast
ballarin@37134
   514
ballarin@37134
   515
thm lor_triv [where z = True] (* Check strict prefix. *)
ballarin@37134
   516
  x.lor_triv
ballarin@37134
   517
ballarin@37134
   518
ballarin@37134
   519
subsection {* Inheritance of mixins *}
ballarin@37134
   520
ballarin@37134
   521
locale reflexive =
ballarin@37134
   522
  fixes le :: "'a => 'a => o" (infix "\<sqsubseteq>" 50)
ballarin@37134
   523
  assumes refl: "x \<sqsubseteq> x"
ballarin@37134
   524
begin
ballarin@37134
   525
ballarin@37134
   526
definition less (infix "\<sqsubset>" 50) where "x \<sqsubset> y <-> x \<sqsubseteq> y & x ~= y"
ballarin@37134
   527
ballarin@37134
   528
end
ballarin@37134
   529
wenzelm@41779
   530
axiomatization
wenzelm@41779
   531
  gle :: "'a => 'a => o" and gless :: "'a => 'a => o" and
wenzelm@41779
   532
  gle' :: "'a => 'a => o" and gless' :: "'a => 'a => o"
wenzelm@41779
   533
where
wenzelm@41779
   534
  grefl: "gle(x, x)" and gless_def: "gless(x, y) <-> gle(x, y) & x ~= y" and
wenzelm@41779
   535
  grefl': "gle'(x, x)" and gless'_def: "gless'(x, y) <-> gle'(x, y) & x ~= y"
ballarin@37134
   536
ballarin@37134
   537
text {* Setup *}
ballarin@37134
   538
ballarin@37134
   539
locale mixin = reflexive
ballarin@37134
   540
begin
ballarin@37134
   541
lemmas less_thm = less_def
ballarin@37134
   542
end
ballarin@37134
   543
ballarin@37134
   544
interpretation le: mixin gle where "reflexive.less(gle, x, y) <-> gless(x, y)"
ballarin@37134
   545
proof -
ballarin@37134
   546
  show "mixin(gle)" by unfold_locales (rule grefl)
ballarin@37134
   547
  note reflexive = this[unfolded mixin_def]
ballarin@37134
   548
  show "reflexive.less(gle, x, y) <-> gless(x, y)"
ballarin@37134
   549
    by (simp add: reflexive.less_def[OF reflexive] gless_def)
ballarin@37134
   550
qed
ballarin@37134
   551
ballarin@37134
   552
text {* Mixin propagated along the locale hierarchy *}
ballarin@37134
   553
ballarin@37134
   554
locale mixin2 = mixin
ballarin@37134
   555
begin
ballarin@37134
   556
lemmas less_thm2 = less_def
ballarin@37134
   557
end
ballarin@37134
   558
ballarin@37134
   559
interpretation le: mixin2 gle
ballarin@37134
   560
  by unfold_locales
ballarin@37134
   561
ballarin@37134
   562
thm le.less_thm2  (* mixin applied *)
ballarin@37134
   563
lemma "gless(x, y) <-> gle(x, y) & x ~= y"
ballarin@37134
   564
  by (rule le.less_thm2)
ballarin@37134
   565
ballarin@37134
   566
text {* Mixin does not leak to a side branch. *}
ballarin@37134
   567
ballarin@37134
   568
locale mixin3 = reflexive
ballarin@37134
   569
begin
ballarin@37134
   570
lemmas less_thm3 = less_def
ballarin@37134
   571
end
ballarin@37134
   572
ballarin@37134
   573
interpretation le: mixin3 gle
ballarin@37134
   574
  by unfold_locales
ballarin@37134
   575
ballarin@37134
   576
thm le.less_thm3  (* mixin not applied *)
ballarin@37134
   577
lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y" by (rule le.less_thm3)
ballarin@37134
   578
ballarin@37134
   579
text {* Mixin only available in original context *}
ballarin@37134
   580
ballarin@37134
   581
locale mixin4_base = reflexive
ballarin@37134
   582
ballarin@37134
   583
locale mixin4_mixin = mixin4_base
ballarin@37134
   584
ballarin@37134
   585
interpretation le: mixin4_mixin gle
ballarin@37134
   586
  where "reflexive.less(gle, x, y) <-> gless(x, y)"
ballarin@37134
   587
proof -
ballarin@37134
   588
  show "mixin4_mixin(gle)" by unfold_locales (rule grefl)
ballarin@37134
   589
  note reflexive = this[unfolded mixin4_mixin_def mixin4_base_def mixin_def]
ballarin@37134
   590
  show "reflexive.less(gle, x, y) <-> gless(x, y)"
ballarin@37134
   591
    by (simp add: reflexive.less_def[OF reflexive] gless_def)
ballarin@37134
   592
qed
ballarin@37134
   593
ballarin@37134
   594
locale mixin4_copy = mixin4_base
ballarin@37134
   595
begin
ballarin@37134
   596
lemmas less_thm4 = less_def
ballarin@37134
   597
end
ballarin@37134
   598
ballarin@37134
   599
locale mixin4_combined = le1: mixin4_mixin le' + le2: mixin4_copy le for le' le
ballarin@37134
   600
begin
ballarin@37134
   601
lemmas less_thm4' = less_def
ballarin@37134
   602
end
ballarin@37134
   603
ballarin@37134
   604
interpretation le4: mixin4_combined gle' gle
ballarin@37134
   605
  by unfold_locales (rule grefl')
ballarin@37134
   606
ballarin@37134
   607
thm le4.less_thm4' (* mixin not applied *)
ballarin@37134
   608
lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
ballarin@37134
   609
  by (rule le4.less_thm4')
ballarin@37134
   610
ballarin@37134
   611
text {* Inherited mixin applied to new theorem *}
ballarin@37134
   612
ballarin@37134
   613
locale mixin5_base = reflexive
ballarin@37134
   614
ballarin@37134
   615
locale mixin5_inherited = mixin5_base
ballarin@37134
   616
ballarin@37134
   617
interpretation le5: mixin5_base gle
ballarin@37134
   618
  where "reflexive.less(gle, x, y) <-> gless(x, y)"
ballarin@37134
   619
proof -
ballarin@37134
   620
  show "mixin5_base(gle)" by unfold_locales
ballarin@37134
   621
  note reflexive = this[unfolded mixin5_base_def mixin_def]
ballarin@37134
   622
  show "reflexive.less(gle, x, y) <-> gless(x, y)"
ballarin@37134
   623
    by (simp add: reflexive.less_def[OF reflexive] gless_def)
ballarin@37134
   624
qed
ballarin@37134
   625
ballarin@37134
   626
interpretation le5: mixin5_inherited gle
ballarin@37134
   627
  by unfold_locales
ballarin@37134
   628
ballarin@37134
   629
lemmas (in mixin5_inherited) less_thm5 = less_def
ballarin@37134
   630
ballarin@37134
   631
thm le5.less_thm5  (* mixin applied *)
ballarin@37134
   632
lemma "gless(x, y) <-> gle(x, y) & x ~= y"
ballarin@37134
   633
  by (rule le5.less_thm5)
ballarin@37134
   634
ballarin@37134
   635
text {* Mixin pushed down to existing inherited locale *}
ballarin@37134
   636
ballarin@37134
   637
locale mixin6_base = reflexive
ballarin@37134
   638
ballarin@37134
   639
locale mixin6_inherited = mixin5_base
ballarin@37134
   640
ballarin@37134
   641
interpretation le6: mixin6_base gle
ballarin@37134
   642
  by unfold_locales
ballarin@37134
   643
interpretation le6: mixin6_inherited gle
ballarin@37134
   644
  by unfold_locales
ballarin@37134
   645
interpretation le6: mixin6_base gle
ballarin@37134
   646
  where "reflexive.less(gle, x, y) <-> gless(x, y)"
ballarin@37134
   647
proof -
ballarin@37134
   648
  show "mixin6_base(gle)" by unfold_locales
ballarin@37134
   649
  note reflexive = this[unfolded mixin6_base_def mixin_def]
ballarin@37134
   650
  show "reflexive.less(gle, x, y) <-> gless(x, y)"
ballarin@37134
   651
    by (simp add: reflexive.less_def[OF reflexive] gless_def)
ballarin@37134
   652
qed
ballarin@37134
   653
ballarin@37134
   654
lemmas (in mixin6_inherited) less_thm6 = less_def
ballarin@37134
   655
ballarin@37134
   656
thm le6.less_thm6  (* mixin applied *)
ballarin@37134
   657
lemma "gless(x, y) <-> gle(x, y) & x ~= y"
ballarin@37134
   658
  by (rule le6.less_thm6)
ballarin@37134
   659
ballarin@37134
   660
text {* Existing mixin inherited through sublocale relation *}
ballarin@37134
   661
ballarin@37134
   662
locale mixin7_base = reflexive
ballarin@37134
   663
ballarin@37134
   664
locale mixin7_inherited = reflexive
ballarin@37134
   665
ballarin@37134
   666
interpretation le7: mixin7_base gle
ballarin@37134
   667
  where "reflexive.less(gle, x, y) <-> gless(x, y)"
ballarin@37134
   668
proof -
ballarin@37134
   669
  show "mixin7_base(gle)" by unfold_locales
ballarin@37134
   670
  note reflexive = this[unfolded mixin7_base_def mixin_def]
ballarin@37134
   671
  show "reflexive.less(gle, x, y) <-> gless(x, y)"
ballarin@37134
   672
    by (simp add: reflexive.less_def[OF reflexive] gless_def)
ballarin@37134
   673
qed
ballarin@37134
   674
ballarin@37134
   675
interpretation le7: mixin7_inherited gle
ballarin@37134
   676
  by unfold_locales
ballarin@37134
   677
ballarin@37134
   678
lemmas (in mixin7_inherited) less_thm7 = less_def
ballarin@37134
   679
ballarin@37134
   680
thm le7.less_thm7  (* before, mixin not applied *)
ballarin@37134
   681
lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
ballarin@37134
   682
  by (rule le7.less_thm7)
ballarin@37134
   683
ballarin@37134
   684
sublocale mixin7_inherited < mixin7_base
ballarin@37134
   685
  by unfold_locales
ballarin@37134
   686
ballarin@37134
   687
lemmas (in mixin7_inherited) less_thm7b = less_def
ballarin@37134
   688
ballarin@37134
   689
thm le7.less_thm7b  (* after, mixin applied *)
ballarin@37134
   690
lemma "gless(x, y) <-> gle(x, y) & x ~= y"
ballarin@37134
   691
  by (rule le7.less_thm7b)
ballarin@37134
   692
ballarin@37134
   693
ballarin@37134
   694
text {* This locale will be interpreted in later theories. *}
ballarin@37134
   695
ballarin@37134
   696
locale mixin_thy_merge = le: reflexive le + le': reflexive le' for le le'
ballarin@37134
   697
ballarin@37134
   698
ballarin@41272
   699
subsection {* Mixins in sublocale *}
ballarin@41272
   700
ballarin@41272
   701
text {* Simulate a specification of left groups where unit and inverse are defined
ballarin@41272
   702
  rather than specified.  This is possible, but not in FOL, due to the lack of a
ballarin@41272
   703
  selection operator. *}
ballarin@41272
   704
ballarin@41272
   705
axiomatization glob_one and glob_inv
ballarin@41272
   706
  where glob_lone: "prod(glob_one(prod), x) = x"
ballarin@41272
   707
    and glob_linv: "prod(glob_inv(prod, x), x) = glob_one(prod)"
ballarin@41272
   708
ballarin@41272
   709
locale dgrp = semi
ballarin@41272
   710
begin
ballarin@41272
   711
ballarin@41272
   712
definition one where "one = glob_one(prod)"
ballarin@41272
   713
ballarin@41272
   714
lemma lone: "one ** x = x"
ballarin@41272
   715
  unfolding one_def by (rule glob_lone)
ballarin@41272
   716
ballarin@41272
   717
definition inv where "inv(x) = glob_inv(prod, x)"
ballarin@41272
   718
ballarin@41272
   719
lemma linv: "inv(x) ** x = one"
ballarin@41272
   720
  unfolding one_def inv_def by (rule glob_linv)
ballarin@41272
   721
ballarin@41272
   722
end
ballarin@41272
   723
ballarin@41272
   724
sublocale lgrp < "def": dgrp
ballarin@41272
   725
  where one_equation: "dgrp.one(prod) = one" and inv_equation: "dgrp.inv(prod, x) = inv(x)"
ballarin@41272
   726
proof -
ballarin@41272
   727
  show "dgrp(prod)" by unfold_locales
ballarin@41272
   728
  from this interpret d: dgrp .
ballarin@41272
   729
  -- Unit
ballarin@41272
   730
  have "dgrp.one(prod) = glob_one(prod)" by (rule d.one_def)
ballarin@41272
   731
  also have "... = glob_one(prod) ** one" by (simp add: rone)
ballarin@41272
   732
  also have "... = one" by (simp add: glob_lone)
ballarin@41272
   733
  finally show "dgrp.one(prod) = one" .
ballarin@41272
   734
  -- Inverse
ballarin@41272
   735
  then have "dgrp.inv(prod, x) ** x = inv(x) ** x" by (simp add: glob_linv d.linv linv)
ballarin@41272
   736
  then show "dgrp.inv(prod, x) = inv(x)" by (simp add: rcancel)
ballarin@41272
   737
qed
ballarin@41272
   738
ballarin@41272
   739
print_locale! lgrp
ballarin@41272
   740
ballarin@41272
   741
context lgrp begin
ballarin@41272
   742
ballarin@41272
   743
text {* Equations stored in target *}
ballarin@41272
   744
ballarin@41272
   745
lemma "dgrp.one(prod) = one" by (rule one_equation)
ballarin@41272
   746
lemma "dgrp.inv(prod, x) = inv(x)" by (rule inv_equation)
ballarin@41272
   747
ballarin@41272
   748
text {* Mixins applied *}
ballarin@41272
   749
ballarin@41272
   750
lemma "one = glob_one(prod)" by (rule one_def)
ballarin@41272
   751
lemma "inv(x) = glob_inv(prod, x)" by (rule inv_def)
ballarin@41272
   752
ballarin@41272
   753
end
ballarin@41272
   754
ballarin@41272
   755
text {* Interpreted versions *}
ballarin@41272
   756
ballarin@41272
   757
lemma "0 = glob_one (op +)" by (rule int.def.one_def)
ballarin@41272
   758
lemma "- x = glob_inv(op +, x)" by (rule int.def.inv_def)
ballarin@41272
   759
ballarin@41272
   760
ballarin@41272
   761
section {* Interpretation in proofs *}
ballarin@37134
   762
ballarin@37134
   763
lemma True
ballarin@37134
   764
proof
ballarin@37134
   765
  interpret "local": lgrp "op +" "0" "minus"
ballarin@37134
   766
    by unfold_locales  (* subsumed *)
ballarin@37134
   767
  {
ballarin@37134
   768
    fix zero :: int
ballarin@37134
   769
    assume "!!x. zero + x = x" "!!x. (-x) + x = zero"
ballarin@37134
   770
    then interpret local_fixed: lgrp "op +" zero "minus"
ballarin@37134
   771
      by unfold_locales
ballarin@37134
   772
    thm local_fixed.lone
ballarin@41435
   773
    print_dependencies! lgrp "op +" 0 minus + lgrp "op +" zero minus
ballarin@37134
   774
  }
ballarin@37134
   775
  assume "!!x zero. zero + x = x" "!!x zero. (-x) + x = zero"
ballarin@37134
   776
  then interpret local_free: lgrp "op +" zero "minus" for zero
ballarin@37134
   777
    by unfold_locales
ballarin@37134
   778
  thm local_free.lone [where ?zero = 0]
ballarin@37134
   779
qed
ballarin@37134
   780
ballarin@38108
   781
lemma True
ballarin@38108
   782
proof
ballarin@38108
   783
  {
ballarin@38108
   784
    fix pand and pnot and por
ballarin@38108
   785
    assume passoc: "!!x y z. pand(pand(x, y), z) <-> pand(x, pand(y, z))"
ballarin@38108
   786
      and pnotnot: "!!x. pnot(pnot(x)) <-> x"
ballarin@38108
   787
      and por_def: "!!x y. por(x, y) <-> pnot(pand(pnot(x), pnot(y)))"
ballarin@38108
   788
    interpret loc: logic_o pand pnot
ballarin@38108
   789
      where por_eq: "!!x y. logic_o.lor_o(pand, pnot, x, y) <-> por(x, y)"  (* FIXME *)
ballarin@38108
   790
    proof -
ballarin@38108
   791
      show logic_o: "PROP logic_o(pand, pnot)" using passoc pnotnot by unfold_locales
ballarin@38108
   792
      fix x y
ballarin@38108
   793
      show "logic_o.lor_o(pand, pnot, x, y) <-> por(x, y)"
ballarin@38108
   794
        by (unfold logic_o.lor_o_def [OF logic_o]) (rule por_def [symmetric])
ballarin@38108
   795
    qed
ballarin@38109
   796
    print_interps logic_o
ballarin@38108
   797
    have "!!x y. por(x, y) <-> pnot(pand(pnot(x), pnot(y)))" by (rule loc.lor_o_def)
ballarin@38108
   798
  }
ballarin@38108
   799
qed
ballarin@38108
   800
ballarin@37134
   801
end