src/FOL/ex/Locale_Test/Locale_Test1.thy
author ballarin
Mon Mar 25 19:53:44 2013 +0100 (2013-03-25)
changeset 51515 c3eb0b517ced
parent 49756 28e37eab4e6f
child 53366 c8c548d83862
permissions -rw-r--r--
Fix issue related to mixins in roundup.
Previously, mixins were only applied one level down the DFS tree while they should also be applied at the level of declaration. Makes the algorithm consistent with the version presented in the upcoming JAR paper.
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@51515
   760
text {* Roundup applies mixins at declaration level in DFS tree *}
ballarin@51515
   761
ballarin@51515
   762
locale roundup = fixes x assumes true: "x <-> True"
ballarin@51515
   763
ballarin@51515
   764
sublocale roundup \<subseteq> sub: roundup x where "x <-> True & True"
ballarin@51515
   765
  apply unfold_locales apply (simp add: true) done
ballarin@51515
   766
lemma (in roundup) "True & True <-> True" by (rule sub.true)
ballarin@51515
   767
ballarin@41272
   768
ballarin@41272
   769
section {* Interpretation in proofs *}
ballarin@37134
   770
ballarin@37134
   771
lemma True
ballarin@37134
   772
proof
ballarin@37134
   773
  interpret "local": lgrp "op +" "0" "minus"
ballarin@37134
   774
    by unfold_locales  (* subsumed *)
ballarin@37134
   775
  {
ballarin@37134
   776
    fix zero :: int
ballarin@37134
   777
    assume "!!x. zero + x = x" "!!x. (-x) + x = zero"
ballarin@37134
   778
    then interpret local_fixed: lgrp "op +" zero "minus"
ballarin@37134
   779
      by unfold_locales
ballarin@37134
   780
    thm local_fixed.lone
ballarin@41435
   781
    print_dependencies! lgrp "op +" 0 minus + lgrp "op +" zero minus
ballarin@37134
   782
  }
ballarin@37134
   783
  assume "!!x zero. zero + x = x" "!!x zero. (-x) + x = zero"
ballarin@37134
   784
  then interpret local_free: lgrp "op +" zero "minus" for zero
ballarin@37134
   785
    by unfold_locales
ballarin@37134
   786
  thm local_free.lone [where ?zero = 0]
ballarin@37134
   787
qed
ballarin@37134
   788
ballarin@38108
   789
lemma True
ballarin@38108
   790
proof
ballarin@38108
   791
  {
ballarin@38108
   792
    fix pand and pnot and por
ballarin@38108
   793
    assume passoc: "!!x y z. pand(pand(x, y), z) <-> pand(x, pand(y, z))"
ballarin@38108
   794
      and pnotnot: "!!x. pnot(pnot(x)) <-> x"
ballarin@38108
   795
      and por_def: "!!x y. por(x, y) <-> pnot(pand(pnot(x), pnot(y)))"
ballarin@38108
   796
    interpret loc: logic_o pand pnot
ballarin@38108
   797
      where por_eq: "!!x y. logic_o.lor_o(pand, pnot, x, y) <-> por(x, y)"  (* FIXME *)
ballarin@38108
   798
    proof -
ballarin@38108
   799
      show logic_o: "PROP logic_o(pand, pnot)" using passoc pnotnot by unfold_locales
ballarin@38108
   800
      fix x y
ballarin@38108
   801
      show "logic_o.lor_o(pand, pnot, x, y) <-> por(x, y)"
ballarin@38108
   802
        by (unfold logic_o.lor_o_def [OF logic_o]) (rule por_def [symmetric])
ballarin@38108
   803
    qed
ballarin@38109
   804
    print_interps logic_o
ballarin@38108
   805
    have "!!x y. por(x, y) <-> pnot(pand(pnot(x), pnot(y)))" by (rule loc.lor_o_def)
ballarin@38108
   806
  }
ballarin@38108
   807
qed
ballarin@38108
   808
ballarin@37134
   809
end