src/FOL/ex/LocaleTest.thy
author ballarin
Tue Jun 20 15:53:44 2006 +0200 (2006-06-20)
changeset 19931 fb32b43e7f80
parent 19783 82f365a14960
child 19984 29bb4659f80a
permissions -rw-r--r--
Restructured locales with predicates: import is now an interpretation.
New method intro_locales.
ballarin@15596
     1
(*  Title:      FOL/ex/LocaleTest.thy
ballarin@15596
     2
    ID:         $Id$
ballarin@15596
     3
    Author:     Clemens Ballarin
ballarin@15596
     4
    Copyright (c) 2005 by Clemens Ballarin
ballarin@15596
     5
ballarin@15596
     6
Collection of regression tests for locales.
ballarin@15596
     7
*)
ballarin@15596
     8
ballarin@16102
     9
header {* Test of Locale Interpretation *}
ballarin@15596
    10
ballarin@16102
    11
theory LocaleTest
ballarin@16102
    12
imports FOL
ballarin@16102
    13
begin
ballarin@15596
    14
ballarin@15696
    15
ML {* set quick_and_dirty *}    (* allow for thm command in batch mode *)
ballarin@16168
    16
ML {* set Toplevel.debug *}
ballarin@15696
    17
ML {* set show_hyps *}
ballarin@15696
    18
ML {* set show_sorts *}
ballarin@15696
    19
ballarin@17139
    20
ML {*
ballarin@17139
    21
  fun check_thm name = let
ballarin@17139
    22
    val thy = the_context ();
ballarin@17139
    23
    val thm = get_thm thy (Name name);
ballarin@17139
    24
    val {prop, hyps, ...} = rep_thm thm;
ballarin@17139
    25
    val prems = Logic.strip_imp_prems prop;
ballarin@17139
    26
    val _ = if null hyps then ()
ballarin@17139
    27
        else error ("Theorem " ^ quote name ^ " has meta hyps.\n" ^
ballarin@17139
    28
          "Consistency check of locales package failed.");
ballarin@17139
    29
    val _ = if null prems then ()
ballarin@17139
    30
        else error ("Theorem " ^ quote name ^ " has premises.\n" ^
ballarin@17139
    31
          "Consistency check of locales package failed.");
ballarin@17139
    32
  in () end;
ballarin@17139
    33
*}
ballarin@17000
    34
ballarin@17000
    35
section {* Context Elements and Locale Expressions *}
ballarin@16102
    36
ballarin@17000
    37
text {* Naming convention for global objects: prefixes L and l *}
ballarin@16168
    38
ballarin@17000
    39
subsection {* Renaming with Syntax *}
ballarin@17000
    40
ballarin@17000
    41
locale (open) LS = var mult +
ballarin@16102
    42
  assumes "mult(x, y) = mult(y, x)"
ballarin@16102
    43
ballarin@17000
    44
print_locale LS
ballarin@16168
    45
ballarin@17000
    46
locale LS' = LS mult (infixl "**" 60)
ballarin@16102
    47
ballarin@17000
    48
print_locale LS'
ballarin@16102
    49
ballarin@17000
    50
locale LT = var mult (infixl "**" 60) +
ballarin@16102
    51
  assumes "x ** y = y ** x"
ballarin@16102
    52
ballarin@17000
    53
locale LU = LT mult (infixl "**" 60) + LT add (infixl "++" 55) + var h +
ballarin@16102
    54
  assumes hom: "h(x ** y) = h(x) ++ h(y)"
ballarin@16102
    55
ballarin@19783
    56
(*
ballarin@19783
    57
Graceful handling of type errors?
ballarin@19783
    58
locale LY = LT mult (infixl "**" 60) + LT add (binder "++" 55) + var h +
ballarin@19783
    59
  assumes "mult(x) == add"
ballarin@19783
    60
*)
ballarin@19783
    61
ballarin@17000
    62
locale LV = LU _ add
ballarin@16102
    63
ballarin@19783
    64
locale LW = LU _ mult (infixl "**" 60)
ballarin@19783
    65
ballarin@16168
    66
ballarin@17000
    67
subsection {* Constrains *}
ballarin@16102
    68
ballarin@17000
    69
locale LZ = fixes a (structure)
ballarin@17000
    70
locale LZ' = LZ +
ballarin@16168
    71
  constrains a :: "'a => 'b"
ballarin@16168
    72
  assumes "a (x :: 'a) = a (y)"
ballarin@17000
    73
print_locale LZ'
ballarin@16102
    74
ballarin@16102
    75
ballarin@16102
    76
section {* Interpretation *}
ballarin@15696
    77
ballarin@17000
    78
text {* Naming convention for global objects: prefixes I and i *}
ballarin@15596
    79
ballarin@17000
    80
text {* interpretation input syntax *}
ballarin@15596
    81
ballarin@17000
    82
locale IL
ballarin@17000
    83
locale IM = fixes a and b and c
ballarin@15596
    84
ballarin@17000
    85
interpretation test [simp]: IL + IM a b c [x y z] .
ballarin@17000
    86
ballarin@17000
    87
print_interps IL    (* output: test *)
ballarin@17000
    88
print_interps IM    (* output: test *)
ballarin@15596
    89
ballarin@17000
    90
interpretation test [simp]: IL print_interps IM .
ballarin@15596
    91
ballarin@17000
    92
interpretation IL .
ballarin@15596
    93
ballarin@17000
    94
text {* Processing of locale expression *}
ballarin@15596
    95
ballarin@17000
    96
locale IA = fixes a assumes asm_A: "a = a"
ballarin@15596
    97
ballarin@17000
    98
locale (open) IB = fixes b assumes asm_B [simp]: "b = b"
ballarin@15596
    99
ballarin@17000
   100
locale IC = IA + IB + assumes asm_C: "c = c"
ballarin@15596
   101
  (* TODO: independent type var in c, prohibit locale declaration *)
ballarin@15596
   102
ballarin@17000
   103
locale ID = IA + IB + fixes d defines def_D: "d == (a = b)"
ballarin@15596
   104
ballarin@17000
   105
theorem (in IA)
ballarin@17000
   106
  includes ID
ballarin@19931
   107
  shows True
ballarin@19931
   108
  print_interps! IA
ballarin@19931
   109
  print_interps! ID
ballarin@19931
   110
  ..
ballarin@15696
   111
ballarin@17000
   112
theorem (in ID) True ..
ballarin@15596
   113
ballarin@15596
   114
typedecl i
ballarin@15596
   115
arities i :: "term"
ballarin@15596
   116
ballarin@15598
   117
ballarin@19931
   118
interpretation i1: IC ["X::i" "Y::i"] by (intro_locales) auto
ballarin@15596
   119
ballarin@17000
   120
print_interps IA  (* output: i1 *)
ballarin@15596
   121
ballarin@15696
   122
(* possible accesses *)
ballarin@17000
   123
thm i1.a.asm_A thm LocaleTest.i1.a.asm_A
ballarin@17000
   124
thm i1.asm_A thm LocaleTest.i1.asm_A
ballarin@15696
   125
ballarin@17139
   126
ML {* check_thm "i1.a.asm_A" *}
ballarin@15624
   127
ballarin@15624
   128
(* without prefix *)
ballarin@15624
   129
ballarin@17000
   130
interpretation IC ["W::i" "Z::i"] .  (* subsumed by i1: IC *)
ballarin@19931
   131
interpretation IC ["W::'a" "Z::i"] by intro_locales auto
ballarin@17000
   132
  (* subsumes i1: IA and i1: IC *)
ballarin@15696
   133
ballarin@17000
   134
print_interps IA  (* output: <no prefix>, i1 *)
ballarin@15596
   135
ballarin@15837
   136
(* possible accesses *)
ballarin@15837
   137
thm asm_C thm a_b.asm_C thm LocaleTest.a_b.asm_C thm LocaleTest.a_b.asm_C
ballarin@15696
   138
ballarin@17139
   139
ML {* check_thm "asm_C" *}
ballarin@15596
   140
ballarin@19931
   141
interpretation i2: ID [X "Y::i" "Y = X"]
ballarin@19931
   142
  by (simp add: eq_commute) intro_locales
ballarin@15837
   143
ballarin@17000
   144
print_interps IA  (* output: <no prefix>, i1 *)
ballarin@17000
   145
print_interps ID  (* output: i2 *)
ballarin@15837
   146
ballarin@15837
   147
ballarin@19931
   148
interpretation i3: ID [X "Y::i"] by simp intro_locales
ballarin@15598
   149
ballarin@17436
   150
(* duplicate: thm not added *)
ballarin@15696
   151
ballarin@17000
   152
(* thm i3.a.asm_A *)
ballarin@15696
   153
ballarin@15596
   154
ballarin@17000
   155
print_interps IA  (* output: <no prefix>, i1 *)
ballarin@17000
   156
print_interps IB  (* output: i1 *)
ballarin@17000
   157
print_interps IC  (* output: <no prefix, i1 *)
ballarin@17000
   158
print_interps ID  (* output: i2, i3 *)
ballarin@15596
   159
ballarin@15837
   160
(* schematic vars in instantiation not permitted *)
ballarin@15837
   161
(*
ballarin@17000
   162
interpretation i4: IA ["?x::?'a1"] apply (rule IA.intro) apply rule done
ballarin@17000
   163
print_interps IA
ballarin@15696
   164
*)
ballarin@15596
   165
ballarin@17000
   166
interpretation i10: ID + ID a' b' d' [X "Y::i" _ u "v::i" _] .
ballarin@15696
   167
ballarin@17000
   168
corollary (in ID) th_x: True ..
ballarin@15696
   169
ballarin@15696
   170
(* possible accesses: for each registration *)
ballarin@15696
   171
ballarin@17000
   172
thm i2.th_x thm i3.th_x
ballarin@15696
   173
ballarin@17139
   174
ML {* check_thm "i2.th_x"; check_thm "i3.th_x" *}
ballarin@17139
   175
ballarin@17000
   176
lemma (in ID) th_y: "d == (a = b)" .
ballarin@15696
   177
ballarin@17000
   178
thm i2.th_y thm i3.th_y
ballarin@15696
   179
ballarin@17139
   180
ML {* check_thm "i2.th_y"; check_thm "i3.th_y" *}
ballarin@17139
   181
ballarin@17000
   182
lemmas (in ID) th_z = th_y
ballarin@15696
   183
ballarin@17000
   184
thm i2.th_z
ballarin@15696
   185
ballarin@17139
   186
ML {* check_thm "i2.th_z" *}
ballarin@17139
   187
ballarin@15596
   188
ballarin@17000
   189
subsection {* Interpretation in Proof Contexts *}
ballarin@17000
   190
ballarin@17000
   191
locale IF = fixes f assumes asm_F: "f & f --> f"
ballarin@16102
   192
ballarin@15624
   193
theorem True
ballarin@15624
   194
proof -
ballarin@16102
   195
  fix alpha::i and beta::'a and gamma::o
ballarin@17000
   196
  (* FIXME: omitting type of beta leads to error later at interpret i6 *)
ballarin@19931
   197
  have alpha_A: "IA(alpha)" by intro_locales simp
ballarin@17000
   198
  interpret i5: IA [alpha] .  (* subsumed *)
ballarin@17000
   199
  print_interps IA  (* output: <no prefix>, i1 *)
ballarin@19931
   200
  interpret i6: IC [alpha beta] by intro_locales auto
ballarin@17000
   201
  print_interps IA   (* output: <no prefix>, i1 *)
ballarin@17000
   202
  print_interps IC   (* output: <no prefix>, i1, i6 *)
ballarin@17000
   203
  interpret i11: IF [gamma] by (fast intro: IF.intro)
ballarin@17000
   204
  thm i11.asm_F      (* gamma is a Free *)
ballarin@15624
   205
qed rule
ballarin@15624
   206
ballarin@17000
   207
theorem (in IA) True
ballarin@15696
   208
proof -
ballarin@19931
   209
  print_interps! IA
ballarin@15696
   210
  fix beta and gamma
ballarin@17000
   211
  interpret i9: ID [a beta _]
ballarin@19931
   212
    apply - apply assumption
ballarin@19931
   213
    apply intro_locales
ballarin@19931
   214
    apply (rule refl) done
ballarin@15696
   215
qed rule
ballarin@15624
   216
ballarin@15624
   217
ballarin@15696
   218
(* Definition involving free variable *)
ballarin@15696
   219
ballarin@15696
   220
ML {* reset show_sorts *}
ballarin@15696
   221
ballarin@17000
   222
locale IE = fixes e defines e_def: "e(x) == x & x"
ballarin@15696
   223
  notes e_def2 = e_def
ballarin@15696
   224
ballarin@17000
   225
lemma (in IE) True thm e_def by fast
ballarin@15696
   226
ballarin@17000
   227
interpretation i7: IE ["%x. x"] by simp
ballarin@15696
   228
ballarin@17000
   229
thm i7.e_def2 (* has no premise *)
ballarin@15696
   230
ballarin@17139
   231
ML {* check_thm "i7.e_def2" *}
ballarin@17139
   232
ballarin@17000
   233
locale IE' = fixes e defines e_def: "e == (%x. x & x)"
ballarin@15696
   234
  notes e_def2 = e_def
ballarin@15696
   235
ballarin@17000
   236
interpretation i7': IE' ["(%x. x)"] by simp
ballarin@15696
   237
ballarin@17000
   238
thm i7'.e_def2
ballarin@15696
   239
ballarin@17139
   240
ML {* check_thm "i7'.e_def2" *}
ballarin@17139
   241
ballarin@15696
   242
(* Definition involving free variable in assm *)
ballarin@15696
   243
ballarin@17000
   244
locale (open) IG = fixes g assumes asm_G: "g --> x"
ballarin@16102
   245
  notes asm_G2 = asm_G
ballarin@15696
   246
ballarin@17000
   247
interpretation i8: IG ["False"] by fast
ballarin@15696
   248
ballarin@17000
   249
thm i8.asm_G2
ballarin@15696
   250
ballarin@17139
   251
ML {* check_thm "i8.asm_G2" *}
ballarin@17139
   252
ballarin@17000
   253
text {* Locale without assumptions *}
ballarin@15696
   254
ballarin@17000
   255
locale IL1 = notes rev_conjI [intro] = conjI [THEN iffD1 [OF conj_commute]]
ballarin@15696
   256
ballarin@15696
   257
lemma "[| P; Q |] ==> P & Q"
ballarin@15696
   258
proof -
ballarin@17000
   259
  interpret my: IL1 .          txt {* No chained fact required. *}
ballarin@15696
   260
  assume Q and P               txt {* order reversed *}
ballarin@15696
   261
  then show "P & Q" ..         txt {* Applies @{thm my.rev_conjI}. *}
ballarin@15696
   262
qed
ballarin@15696
   263
ballarin@17000
   264
locale IL11 = notes rev_conjI = conjI [THEN iffD1 [OF conj_commute]]
ballarin@15696
   265
ballarin@15696
   266
lemma "[| P; Q |] ==> P & Q"
ballarin@15696
   267
proof -
ballarin@17000
   268
  interpret [intro]: IL11 .     txt {* Attribute supplied at instantiation. *}
ballarin@15696
   269
  assume Q and P
ballarin@15696
   270
  then show "P & Q" ..
ballarin@15696
   271
qed
ballarin@15696
   272
ballarin@15696
   273
subsection {* Simple locale with assumptions *}
ballarin@15696
   274
ballarin@17000
   275
consts ibin :: "[i, i] => i" (infixl "#" 60)
ballarin@15696
   276
ballarin@15696
   277
axioms i_assoc: "(x # y) # z = x # (y # z)"
ballarin@15696
   278
  i_comm: "x # y = y # x"
ballarin@15696
   279
ballarin@17000
   280
locale IL2 =
ballarin@15696
   281
  fixes OP (infixl "+" 60)
ballarin@15696
   282
  assumes assoc: "(x + y) + z = x + (y + z)"
ballarin@15696
   283
    and comm: "x + y = y + x"
ballarin@15696
   284
ballarin@17000
   285
lemma (in IL2) lcomm: "x + (y + z) = y + (x + z)"
ballarin@17000
   286
proof -
ballarin@17000
   287
  have "x + (y + z) = (x + y) + z" by (simp add: assoc)
ballarin@17000
   288
  also have "... = (y + x) + z" by (simp add: comm)
ballarin@17000
   289
  also have "... = y + (x + z)" by (simp add: assoc)
ballarin@17000
   290
  finally show ?thesis .
ballarin@17000
   291
qed
ballarin@17000
   292
ballarin@17000
   293
lemmas (in IL2) AC = comm assoc lcomm
ballarin@17000
   294
ballarin@17000
   295
lemma "(x::i) # y # z # w = y # x # w # z"
ballarin@17000
   296
proof -
ballarin@17000
   297
  interpret my: IL2 ["op #"] by (rule IL2.intro [of "op #", OF i_assoc i_comm])
ballarin@17033
   298
  show ?thesis by (simp only: my.OP.AC)  (* or my.AC *)
ballarin@17000
   299
qed
ballarin@17000
   300
ballarin@17000
   301
subsection {* Nested locale with assumptions *}
ballarin@17000
   302
ballarin@17000
   303
locale IL3 =
ballarin@17000
   304
  fixes OP (infixl "+" 60)
ballarin@17000
   305
  assumes assoc: "(x + y) + z = x + (y + z)"
ballarin@17000
   306
ballarin@17000
   307
locale IL4 = IL3 +
ballarin@17000
   308
  assumes comm: "x + y = y + x"
ballarin@17000
   309
ballarin@17000
   310
lemma (in IL4) lcomm: "x + (y + z) = y + (x + z)"
ballarin@15696
   311
proof -
ballarin@15696
   312
  have "x + (y + z) = (x + y) + z" by (simp add: assoc)
ballarin@15696
   313
  also have "... = (y + x) + z" by (simp add: comm)
ballarin@15696
   314
  also have "... = y + (x + z)" by (simp add: assoc)
ballarin@15696
   315
  finally show ?thesis .
ballarin@15696
   316
qed
ballarin@15696
   317
ballarin@17000
   318
lemmas (in IL4) AC = comm assoc lcomm
ballarin@15696
   319
ballarin@15696
   320
lemma "(x::i) # y # z # w = y # x # w # z"
ballarin@15696
   321
proof -
ballarin@17000
   322
  interpret my: IL4 ["op #"]
ballarin@19931
   323
    by (auto intro: IL4.intro IL3.intro IL4_axioms.intro i_assoc i_comm)
ballarin@15696
   324
  show ?thesis by (simp only: my.OP.AC)  (* or simply AC *)
ballarin@15696
   325
qed
ballarin@15696
   326
ballarin@17000
   327
text {* Locale with definition *}
ballarin@15696
   328
ballarin@15696
   329
text {* This example is admittedly not very creative :-) *}
ballarin@15696
   330
ballarin@17000
   331
locale IL5 = IL4 + var A +
ballarin@15696
   332
  defines A_def: "A == True"
ballarin@15696
   333
ballarin@17000
   334
lemma (in IL5) lem: A
ballarin@15696
   335
  by (unfold A_def) rule
ballarin@15696
   336
ballarin@17000
   337
lemma "IL5(op #) ==> True"
ballarin@15696
   338
proof -
ballarin@17000
   339
  assume "IL5(op #)"
ballarin@17000
   340
  then interpret IL5 ["op #"] by (auto intro: IL5.axioms)
ballarin@15696
   341
  show ?thesis by (rule lem)  (* lem instantiated to True *)
ballarin@15696
   342
qed
ballarin@15696
   343
ballarin@17000
   344
text {* Interpretation in a context with target *}
ballarin@15696
   345
ballarin@17000
   346
lemma (in IL4)
ballarin@15696
   347
  fixes A (infixl "$" 60)
ballarin@17000
   348
  assumes A: "IL4(A)"
ballarin@15696
   349
  shows "(x::i) $ y $ z $ w = y $ x $ w $ z"
ballarin@15696
   350
proof -
ballarin@17000
   351
  from A interpret A: IL4 ["A"] by (auto intro: IL4.axioms)
ballarin@15696
   352
  show ?thesis by (simp only: A.OP.AC)
ballarin@15696
   353
qed
ballarin@15696
   354
ballarin@17000
   355
ballarin@16736
   356
section {* Interpretation in Locales *}
ballarin@16736
   357
ballarin@17000
   358
text {* Naming convention for global objects: prefixes R and r *}
ballarin@17000
   359
ballarin@17000
   360
locale (open) Rsemi = var prod (infixl "**" 65) +
ballarin@17000
   361
  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
ballarin@17000
   362
ballarin@17000
   363
locale (open) Rlgrp = Rsemi + var one + var inv +
ballarin@17000
   364
  assumes lone: "one ** x = x"
ballarin@17000
   365
    and linv: "inv(x) ** x = one"
ballarin@17000
   366
ballarin@17000
   367
lemma (in Rlgrp) lcancel:
ballarin@17000
   368
  "x ** y = x ** z <-> y = z"
ballarin@17000
   369
proof
ballarin@17000
   370
  assume "x ** y = x ** z"
ballarin@17000
   371
  then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
ballarin@17000
   372
  then show "y = z" by (simp add: lone linv)
ballarin@17000
   373
qed simp
ballarin@17000
   374
ballarin@17000
   375
locale (open) Rrgrp = Rsemi + var one + var inv +
ballarin@17000
   376
  assumes rone: "x ** one = x"
ballarin@17000
   377
    and rinv: "x ** inv(x) = one"
ballarin@17000
   378
ballarin@17000
   379
lemma (in Rrgrp) rcancel:
ballarin@17000
   380
  "y ** x = z ** x <-> y = z"
ballarin@17000
   381
proof
ballarin@17000
   382
  assume "y ** x = z ** x"
ballarin@17000
   383
  then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
ballarin@17000
   384
    by (simp add: assoc [symmetric])
ballarin@17000
   385
  then show "y = z" by (simp add: rone rinv)
ballarin@17000
   386
qed simp
ballarin@17000
   387
ballarin@17000
   388
interpretation Rlgrp < Rrgrp
ballarin@17033
   389
  proof -
ballarin@17000
   390
    {
ballarin@17000
   391
      fix x
ballarin@17000
   392
      have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
ballarin@17000
   393
      then show "x ** one = x" by (simp add: assoc lcancel)
ballarin@17000
   394
    }
ballarin@17000
   395
    note rone = this
ballarin@17000
   396
    {
ballarin@17000
   397
      fix x
ballarin@17000
   398
      have "inv(x) ** x ** inv(x) = inv(x) ** one"
ballarin@17000
   399
	by (simp add: linv lone rone)
ballarin@17000
   400
      then show "x ** inv(x) = one" by (simp add: assoc lcancel)
ballarin@17000
   401
    }
ballarin@17000
   402
  qed
ballarin@17000
   403
ballarin@17000
   404
(* effect on printed locale *)
ballarin@17000
   405
ballarin@19931
   406
print_locale! Rlgrp
ballarin@17000
   407
ballarin@17000
   408
(* use of derived theorem *)
ballarin@17000
   409
ballarin@17000
   410
lemma (in Rlgrp)
ballarin@17000
   411
  "y ** x = z ** x <-> y = z"
ballarin@17000
   412
  apply (rule rcancel)
ballarin@17000
   413
  print_interps Rrgrp thm lcancel rcancel
ballarin@17000
   414
  done
ballarin@17000
   415
ballarin@17000
   416
(* circular interpretation *)
ballarin@17000
   417
ballarin@17000
   418
interpretation Rrgrp < Rlgrp
ballarin@17000
   419
  proof -
ballarin@17000
   420
    {
ballarin@17000
   421
      fix x
ballarin@17000
   422
      have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone)
ballarin@17000
   423
      then show "one ** x = x" by (simp add: assoc [symmetric] rcancel)
ballarin@17000
   424
    }
ballarin@17000
   425
    note lone = this
ballarin@17000
   426
    {
ballarin@17000
   427
      fix x
ballarin@17000
   428
      have "inv(x) ** (x ** inv(x)) = one ** inv(x)"
ballarin@17000
   429
	by (simp add: rinv lone rone)
ballarin@17000
   430
      then show "inv(x) ** x = one" by (simp add: assoc [symmetric] rcancel)
ballarin@17000
   431
    }
ballarin@17000
   432
  qed
ballarin@17000
   433
ballarin@17000
   434
(* effect on printed locale *)
ballarin@17000
   435
ballarin@17228
   436
print_locale! Rrgrp
ballarin@17228
   437
print_locale! Rlgrp
ballarin@17000
   438
ballarin@17000
   439
(* locale with many parameters ---
ballarin@17000
   440
   interpretations generate alternating group A5 *)
ballarin@17000
   441
ballarin@17000
   442
locale RA5 = var A + var B + var C + var D + var E +
ballarin@17000
   443
  assumes eq: "A <-> B <-> C <-> D <-> E"
ballarin@17000
   444
ballarin@17000
   445
interpretation RA5 < RA5 _ _ D E C
ballarin@17000
   446
print_facts
ballarin@17000
   447
print_interps RA5
ballarin@17000
   448
  using A_B_C_D_E.eq apply (blast intro: RA5.intro) done
ballarin@17000
   449
ballarin@17000
   450
interpretation RA5 < RA5 C _ E _ A
ballarin@17000
   451
print_facts
ballarin@17000
   452
print_interps RA5
ballarin@17000
   453
  using A_B_C_D_E.eq apply (blast intro: RA5.intro) done
ballarin@17000
   454
ballarin@17000
   455
interpretation RA5 < RA5 B C A _ _
ballarin@17000
   456
print_facts
ballarin@17000
   457
print_interps RA5
ballarin@17000
   458
  using A_B_C_D_E.eq apply (blast intro: RA5.intro) done
ballarin@17000
   459
ballarin@17000
   460
interpretation RA5 < RA5 _ C D B _ .
ballarin@17000
   461
  (* Any even permutation of parameters is subsumed by the above. *)
ballarin@17000
   462
ballarin@17000
   463
(* circle of three locales, forward direction *)
ballarin@17000
   464
ballarin@17000
   465
locale (open) RA1 = var A + var B + assumes p: "A <-> B"
ballarin@17000
   466
locale (open) RA2 = var A + var B + assumes q: "A & B | ~ A & ~ B"
ballarin@17000
   467
locale (open) RA3 = var A + var B + assumes r: "(A --> B) & (B --> A)"
ballarin@17000
   468
ballarin@17000
   469
interpretation RA1 < RA2
ballarin@17000
   470
  print_facts
ballarin@17000
   471
  using p apply fast done
ballarin@17000
   472
interpretation RA2 < RA3
ballarin@17000
   473
  print_facts
ballarin@17000
   474
  using q apply fast done
ballarin@17000
   475
interpretation RA3 < RA1
ballarin@17000
   476
  print_facts
ballarin@17000
   477
  using r apply fast done
ballarin@17000
   478
ballarin@17000
   479
(* circle of three locales, backward direction *)
ballarin@17000
   480
ballarin@17000
   481
locale (open) RB1 = var A + var B + assumes p: "A <-> B"
ballarin@17000
   482
locale (open) RB2 = var A + var B + assumes q: "A & B | ~ A & ~ B"
ballarin@17000
   483
locale (open) RB3 = var A + var B + assumes r: "(A --> B) & (B --> A)"
ballarin@17000
   484
ballarin@17000
   485
interpretation RB1 < RB2
ballarin@17000
   486
  print_facts
ballarin@17000
   487
  using p apply fast done
ballarin@17000
   488
interpretation RB3 < RB1
ballarin@17000
   489
  print_facts
ballarin@17000
   490
  using r apply fast done
ballarin@17000
   491
interpretation RB2 < RB3
ballarin@17000
   492
  print_facts
ballarin@17000
   493
  using q apply fast done
ballarin@17000
   494
ballarin@17000
   495
lemma (in RB1) True
ballarin@17000
   496
  print_facts
ballarin@17000
   497
  ..
ballarin@17000
   498
ballarin@17000
   499
ballarin@17000
   500
(* Group example revisited, with predicates *)
ballarin@17000
   501
ballarin@17000
   502
locale Rpsemi = var prod (infixl "**" 65) +
ballarin@17000
   503
  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
ballarin@17000
   504
ballarin@17000
   505
locale Rplgrp = Rpsemi + var one + var inv +
ballarin@17000
   506
  assumes lone: "one ** x = x"
ballarin@17000
   507
    and linv: "inv(x) ** x = one"
ballarin@17000
   508
ballarin@17000
   509
lemma (in Rplgrp) lcancel:
ballarin@17000
   510
  "x ** y = x ** z <-> y = z"
ballarin@17000
   511
proof
ballarin@17000
   512
  assume "x ** y = x ** z"
ballarin@17000
   513
  then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
ballarin@17000
   514
  then show "y = z" by (simp add: lone linv)
ballarin@17000
   515
qed simp
ballarin@17000
   516
ballarin@17000
   517
locale Rprgrp = Rpsemi + var one + var inv +
ballarin@17000
   518
  assumes rone: "x ** one = x"
ballarin@17000
   519
    and rinv: "x ** inv(x) = one"
ballarin@17000
   520
ballarin@17000
   521
lemma (in Rprgrp) rcancel:
ballarin@17000
   522
  "y ** x = z ** x <-> y = z"
ballarin@17000
   523
proof
ballarin@17000
   524
  assume "y ** x = z ** x"
ballarin@17000
   525
  then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
ballarin@17000
   526
    by (simp add: assoc [symmetric])
ballarin@17000
   527
  then show "y = z" by (simp add: rone rinv)
ballarin@17000
   528
qed simp
ballarin@17000
   529
ballarin@17000
   530
interpretation Rplgrp < Rprgrp
ballarin@19931
   531
  proof intro_locales
ballarin@17000
   532
    {
ballarin@17000
   533
      fix x
ballarin@17000
   534
      have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
ballarin@17000
   535
      then show "x ** one = x" by (simp add: assoc lcancel)
ballarin@17000
   536
    }
ballarin@17000
   537
    note rone = this
ballarin@17000
   538
    {
ballarin@17000
   539
      fix x
ballarin@17000
   540
      have "inv(x) ** x ** inv(x) = inv(x) ** one"
ballarin@17000
   541
	by (simp add: linv lone rone)
ballarin@17000
   542
      then show "x ** inv(x) = one" by (simp add: assoc lcancel)
ballarin@17000
   543
    }
ballarin@17000
   544
  qed
ballarin@17000
   545
ballarin@17000
   546
(* effect on printed locale *)
ballarin@17000
   547
ballarin@19931
   548
print_locale! Rplgrp
ballarin@17000
   549
ballarin@17000
   550
(* use of derived theorem *)
ballarin@17000
   551
ballarin@17000
   552
lemma (in Rplgrp)
ballarin@17000
   553
  "y ** x = z ** x <-> y = z"
ballarin@17000
   554
  apply (rule rcancel)
ballarin@17000
   555
  print_interps Rprgrp thm lcancel rcancel
ballarin@17000
   556
  done
ballarin@17000
   557
ballarin@17000
   558
(* circular interpretation *)
ballarin@17000
   559
ballarin@17000
   560
interpretation Rprgrp < Rplgrp
ballarin@19931
   561
  proof intro_locales
ballarin@17000
   562
    {
ballarin@17000
   563
      fix x
ballarin@17000
   564
      have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone)
ballarin@17000
   565
      then show "one ** x = x" by (simp add: assoc [symmetric] rcancel)
ballarin@17000
   566
    }
ballarin@17000
   567
    note lone = this
ballarin@17000
   568
    {
ballarin@17000
   569
      fix x
ballarin@17000
   570
      have "inv(x) ** (x ** inv(x)) = one ** inv(x)"
ballarin@17000
   571
	by (simp add: rinv lone rone)
ballarin@17000
   572
      then show "inv(x) ** x = one" by (simp add: assoc [symmetric] rcancel)
ballarin@17000
   573
    }
ballarin@17000
   574
  qed
ballarin@17000
   575
ballarin@17000
   576
(* effect on printed locale *)
ballarin@17000
   577
ballarin@19931
   578
print_locale! Rprgrp
ballarin@19931
   579
print_locale! Rplgrp
ballarin@16736
   580
ballarin@17033
   581
subsection {* Interaction of Interpretation in Theories and Locales:
ballarin@17096
   582
  in Locale, then in Theory *}
ballarin@17033
   583
ballarin@17033
   584
consts
ballarin@17033
   585
  rone :: i
ballarin@17033
   586
  rinv :: "i => i"
ballarin@17033
   587
ballarin@17033
   588
axioms
ballarin@17033
   589
  r_one : "rone # x = x"
ballarin@17033
   590
  r_inv : "rinv(x) # x = rone"
ballarin@17033
   591
ballarin@17033
   592
interpretation Rbool: Rlgrp ["op #" "rone" "rinv"]
ballarin@17033
   593
proof -
ballarin@17033
   594
  fix x y z
ballarin@17033
   595
  {
ballarin@17033
   596
    show "(x # y) # z = x # (y # z)" by (rule i_assoc)
ballarin@17033
   597
  next
ballarin@17033
   598
    show "rone # x = x" by (rule r_one)
ballarin@17033
   599
  next
ballarin@17033
   600
    show "rinv(x) # x = rone" by (rule r_inv)
ballarin@17033
   601
  }
ballarin@17033
   602
qed
ballarin@17033
   603
ballarin@17033
   604
(* derived elements *)
ballarin@17033
   605
ballarin@17033
   606
print_interps Rrgrp
ballarin@17033
   607
print_interps Rlgrp
ballarin@17033
   608
ballarin@17033
   609
lemma "y # x = z # x <-> y = z" by (rule Rbool.rcancel)
ballarin@17033
   610
ballarin@17033
   611
(* adding lemma to derived element *)
ballarin@17033
   612
ballarin@17033
   613
lemma (in Rrgrp) new_cancel:
ballarin@17033
   614
  "b ** a = c ** a <-> b = c"
ballarin@17033
   615
  by (rule rcancel)
ballarin@17033
   616
ballarin@17033
   617
thm Rbool.new_cancel (* additional prems discharged!! *)
ballarin@17033
   618
ballarin@17139
   619
ML {* check_thm "Rbool.new_cancel" *}
ballarin@17139
   620
ballarin@17033
   621
lemma "b # a = c # a <-> b = c" by (rule Rbool.new_cancel)
ballarin@17033
   622
ballarin@17033
   623
ballarin@17033
   624
subsection {* Interaction of Interpretation in Theories and Locales:
ballarin@17096
   625
  in Theory, then in Locale *}
ballarin@17033
   626
ballarin@17033
   627
(* Another copy of the group example *)
ballarin@17033
   628
ballarin@17033
   629
locale Rqsemi = var prod (infixl "**" 65) +
ballarin@17033
   630
  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
ballarin@17033
   631
ballarin@17033
   632
locale Rqlgrp = Rqsemi + var one + var inv +
ballarin@17033
   633
  assumes lone: "one ** x = x"
ballarin@17033
   634
    and linv: "inv(x) ** x = one"
ballarin@17033
   635
ballarin@17033
   636
lemma (in Rqlgrp) lcancel:
ballarin@17033
   637
  "x ** y = x ** z <-> y = z"
ballarin@17033
   638
proof
ballarin@17033
   639
  assume "x ** y = x ** z"
ballarin@17033
   640
  then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
ballarin@17033
   641
  then show "y = z" by (simp add: lone linv)
ballarin@17033
   642
qed simp
ballarin@17033
   643
ballarin@17033
   644
locale Rqrgrp = Rqsemi + var one + var inv +
ballarin@17033
   645
  assumes rone: "x ** one = x"
ballarin@17033
   646
    and rinv: "x ** inv(x) = one"
ballarin@17033
   647
ballarin@17033
   648
lemma (in Rqrgrp) rcancel:
ballarin@17033
   649
  "y ** x = z ** x <-> y = z"
ballarin@17033
   650
proof
ballarin@17033
   651
  assume "y ** x = z ** x"
ballarin@17033
   652
  then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
ballarin@17033
   653
    by (simp add: assoc [symmetric])
ballarin@17033
   654
  then show "y = z" by (simp add: rone rinv)
ballarin@17033
   655
qed simp
ballarin@17033
   656
ballarin@17139
   657
interpretation Rqrgrp < Rprgrp
ballarin@19931
   658
  apply intro_locales
ballarin@19931
   659
  apply (rule assoc)
ballarin@19931
   660
  apply (rule rone)
ballarin@19931
   661
  apply (rule rinv)
ballarin@19931
   662
  done
ballarin@17139
   663
ballarin@17033
   664
interpretation R2: Rqlgrp ["op #" "rone" "rinv"] 
ballarin@19931
   665
  apply intro_locales  (* FIXME: intro_locales is too eager and shouldn't
ballarin@19931
   666
                          solve this. *)
ballarin@19931
   667
  done
ballarin@17033
   668
ballarin@17033
   669
print_interps Rqsemi
ballarin@17033
   670
print_interps Rqlgrp
ballarin@17139
   671
print_interps Rplgrp  (* no interpretations yet *)
ballarin@17139
   672
ballarin@17033
   673
ballarin@17033
   674
interpretation Rqlgrp < Rqrgrp
ballarin@19931
   675
  proof intro_locales
ballarin@17033
   676
    {
ballarin@17033
   677
      fix x
ballarin@17033
   678
      have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
ballarin@17033
   679
      then show "x ** one = x" by (simp add: assoc lcancel)
ballarin@17033
   680
    }
ballarin@17033
   681
    note rone = this
ballarin@17033
   682
    {
ballarin@17033
   683
      fix x
ballarin@17033
   684
      have "inv(x) ** x ** inv(x) = inv(x) ** one"
ballarin@17033
   685
	by (simp add: linv lone rone)
ballarin@17033
   686
      then show "x ** inv(x) = one" by (simp add: assoc lcancel)
ballarin@17033
   687
    }
ballarin@17033
   688
  qed
ballarin@17033
   689
ballarin@17139
   690
print_interps! Rqrgrp
ballarin@17139
   691
print_interps! Rpsemi  (* witness must not have meta hyps *)
ballarin@17139
   692
print_interps! Rprgrp  (* witness must not have meta hyps *)
ballarin@17139
   693
print_interps! Rplgrp  (* witness must not have meta hyps *)
ballarin@17139
   694
thm R2.rcancel
ballarin@17139
   695
thm R2.lcancel
ballarin@17139
   696
ballarin@17139
   697
ML {* check_thm "R2.rcancel"; check_thm "R2.lcancel" *}
ballarin@17139
   698
ballarin@17096
   699
ballarin@17096
   700
subsection {* Generation of Witness Theorems for Transitive Interpretations *}
ballarin@17096
   701
ballarin@17096
   702
locale Rtriv = var x +
ballarin@17096
   703
  assumes x: "x = x"
ballarin@17096
   704
ballarin@17096
   705
locale Rtriv2 = var x + var y +
ballarin@17096
   706
  assumes x: "x = x" and y: "y = y"
ballarin@17096
   707
ballarin@17096
   708
interpretation Rtriv2 < Rtriv x
ballarin@19931
   709
  apply intro_locales
ballarin@17096
   710
  apply (rule x)
ballarin@17096
   711
  done
ballarin@17096
   712
ballarin@17096
   713
interpretation Rtriv2 < Rtriv y
ballarin@19931
   714
  apply intro_locales
ballarin@17096
   715
  apply (rule y)
ballarin@17096
   716
  done
ballarin@17096
   717
ballarin@17096
   718
print_locale Rtriv2
ballarin@17096
   719
ballarin@17096
   720
locale Rtriv3 = var x + var y + var z +
ballarin@17096
   721
  assumes x: "x = x" and y: "y = y" and z: "z = z"
ballarin@17096
   722
ballarin@17096
   723
interpretation Rtriv3 < Rtriv2 x y
ballarin@19931
   724
  apply intro_locales
ballarin@17096
   725
  apply (rule x)
ballarin@17096
   726
  apply (rule y)
ballarin@17096
   727
  done
ballarin@17096
   728
ballarin@17096
   729
print_locale Rtriv3
ballarin@17096
   730
ballarin@17096
   731
interpretation Rtriv3 < Rtriv2 x z
ballarin@19931
   732
  apply intro_locales
ballarin@17096
   733
  apply (rule x_y_z.x)
ballarin@17096
   734
  apply (rule z)
ballarin@17096
   735
  done
ballarin@17096
   736
ballarin@17096
   737
ML {* set show_types *}
ballarin@17096
   738
ballarin@17096
   739
print_locale Rtriv3
ballarin@17096
   740
ballarin@17096
   741
ballarin@17096
   742
subsection {* Normalisation Replaces Assumed Element by Derived Element *}
ballarin@17096
   743
ballarin@17096
   744
typedecl ('a, 'b) pair
ballarin@17096
   745
arities pair :: ("term", "term") "term"
ballarin@17096
   746
ballarin@17096
   747
consts
ballarin@17096
   748
  pair :: "['a, 'b] => ('a, 'b) pair"
ballarin@17096
   749
  fst :: "('a, 'b) pair => 'a"
ballarin@17096
   750
  snd :: "('a, 'b) pair => 'b"
ballarin@17096
   751
ballarin@17096
   752
axioms
ballarin@17096
   753
  fst [simp]: "fst(pair(x, y)) = x"
ballarin@17096
   754
  snd [simp]: "snd(pair(x, y)) = y"
ballarin@17096
   755
ballarin@17096
   756
locale Rpair = var prod (infixl "**" 65) + var prodP (infixl "***" 65) +
ballarin@17096
   757
  defines P_def: "x *** y == pair(fst(x) ** fst(y), snd(x) ** snd(y))"
ballarin@17096
   758
ballarin@17096
   759
locale Rpair_semi = Rpair + Rpsemi
ballarin@17096
   760
ballarin@17096
   761
interpretation Rpair_semi < Rpsemi prodP (infixl "***" 65)
ballarin@17096
   762
proof (rule Rpsemi.intro)
ballarin@17096
   763
  fix x y z
ballarin@17096
   764
  show "(x *** y) *** z = x *** (y *** z)"
ballarin@19931
   765
    apply (simp only: P_def) apply (simp add: assoc) (* FIXME: unfold P_def fails *)
ballarin@19931
   766
    done
ballarin@17096
   767
qed
ballarin@17096
   768
ballarin@17096
   769
locale Rsemi_rev = Rpsemi + var rprod (infixl "++" 65) +
ballarin@17096
   770
  defines r_def: "x ++ y == y ** x"
ballarin@17096
   771
ballarin@17096
   772
lemma (in Rsemi_rev) r_assoc:
ballarin@17096
   773
  "(x ++ y) ++ z = x ++ (y ++ z)"
ballarin@17096
   774
  by (simp add: r_def assoc)
ballarin@17096
   775
ballarin@17096
   776
lemma (in Rpair_semi)
ballarin@17096
   777
  includes Rsemi_rev prodP (infixl "***" 65) rprodP (infixl "+++" 65)
ballarin@17096
   778
  constrains prod :: "['a, 'a] => 'a"
ballarin@17096
   779
    and rprodP :: "[('a, 'a) pair, ('a, 'a) pair] => ('a, 'a) pair"
ballarin@17096
   780
  shows "(x +++ y) +++ z = x +++ (y +++ z)"
ballarin@17096
   781
  apply (rule r_assoc) done
ballarin@17033
   782
ballarin@15596
   783
end