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