src/FOL/ex/NewLocaleTest.thy
author ballarin
Fri Dec 05 16:41:36 2008 +0100 (2008-12-05)
changeset 29018 17538bdef546
parent 28993 829e684b02ef
child 29019 8e7d6f959bd7
permissions -rw-r--r--
Interpretation in proof contexts.
ballarin@28873
     1
(*  Title:      FOL/ex/NewLocaleTest.thy
ballarin@28873
     2
    Author:     Clemens Ballarin, TU Muenchen
ballarin@28873
     3
ballarin@28873
     4
Testing environment for locale expressions --- experimental.
ballarin@28873
     5
*)
ballarin@28873
     6
ballarin@28873
     7
theory NewLocaleTest
ballarin@28873
     8
imports NewLocaleSetup
ballarin@28873
     9
begin
ballarin@28873
    10
ballarin@28873
    11
ML_val {* set new_locales *}
ballarin@28873
    12
ML_val {* set Toplevel.debug *}
ballarin@28873
    13
ML_val {* set show_hyps *}
ballarin@28873
    14
ballarin@28873
    15
ballarin@28873
    16
typedecl int arities int :: "term"
ballarin@28873
    17
consts plus :: "int => int => int" (infixl "+" 60)
ballarin@28873
    18
  zero :: int ("0")
ballarin@28873
    19
  minus :: "int => int" ("- _")
ballarin@28873
    20
ballarin@28993
    21
axioms
ballarin@28993
    22
  int_assoc: "(x + y::int) + z = x + (y + z)"
ballarin@28993
    23
  int_zero: "0 + x = x"
ballarin@28993
    24
  int_minus: "(-x) + x = 0"
ballarin@28993
    25
  int_minus2: "-(-x) = x"
ballarin@28873
    26
ballarin@28873
    27
text {* Inference of parameter types *}
ballarin@28873
    28
ballarin@28873
    29
locale param1 = fixes p
ballarin@28873
    30
print_locale! param1
ballarin@28873
    31
ballarin@28881
    32
locale param2 = fixes p :: 'b
ballarin@28873
    33
print_locale! param2
ballarin@28873
    34
ballarin@28873
    35
(*
ballarin@28873
    36
locale param_top = param2 r for r :: "'b :: {}"
ballarin@28993
    37
  Fails, cannot generalise parameter.
ballarin@28873
    38
*)
ballarin@28873
    39
ballarin@28873
    40
locale param3 = fixes p (infix ".." 50)
ballarin@28873
    41
print_locale! param3
ballarin@28873
    42
ballarin@28873
    43
locale param4 = fixes p :: "'a => 'a => 'a" (infix ".." 50)
ballarin@28873
    44
print_locale! param4
ballarin@28873
    45
ballarin@28873
    46
ballarin@28873
    47
text {* Incremental type constraints *}
ballarin@28873
    48
ballarin@28873
    49
locale constraint1 =
ballarin@28873
    50
  fixes  prod (infixl "**" 65)
ballarin@28873
    51
  assumes l_id: "x ** y = x"
ballarin@28873
    52
  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
ballarin@28873
    53
print_locale! constraint1
ballarin@28873
    54
ballarin@28873
    55
locale constraint2 =
ballarin@28873
    56
  fixes p and q
ballarin@28873
    57
  assumes "p = q"
ballarin@28873
    58
print_locale! constraint2
ballarin@28873
    59
ballarin@28873
    60
ballarin@28881
    61
text {* Inheritance *}
ballarin@28873
    62
ballarin@28873
    63
locale semi =
ballarin@28873
    64
  fixes prod (infixl "**" 65)
ballarin@28873
    65
  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
ballarin@28873
    66
print_locale! semi thm semi_def
ballarin@28873
    67
ballarin@28873
    68
locale lgrp = semi +
ballarin@28873
    69
  fixes one and inv
ballarin@28873
    70
  assumes lone: "one ** x = x"
ballarin@28873
    71
    and linv: "inv(x) ** x = one"
ballarin@28873
    72
print_locale! lgrp thm lgrp_def lgrp_axioms_def
ballarin@28873
    73
ballarin@28873
    74
locale add_lgrp = semi "op ++" for sum (infixl "++" 60) +
ballarin@28873
    75
  fixes zero and neg
ballarin@28873
    76
  assumes lzero: "zero ++ x = x"
ballarin@28873
    77
    and lneg: "neg(x) ++ x = zero"
ballarin@28873
    78
print_locale! add_lgrp thm add_lgrp_def add_lgrp_axioms_def
ballarin@28873
    79
ballarin@28873
    80
locale rev_lgrp = semi "%x y. y ++ x" for sum (infixl "++" 60)
ballarin@28873
    81
print_locale! rev_lgrp thm rev_lgrp_def
ballarin@28873
    82
ballarin@28873
    83
locale hom = f: semi f + g: semi g for f and g
ballarin@28873
    84
print_locale! hom thm hom_def
ballarin@28873
    85
ballarin@28873
    86
locale perturbation = semi + d: semi "%x y. delta(x) ** delta(y)" for delta
ballarin@28873
    87
print_locale! perturbation thm perturbation_def
ballarin@28873
    88
ballarin@28873
    89
locale pert_hom = d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2
ballarin@28873
    90
print_locale! pert_hom thm pert_hom_def
ballarin@28873
    91
ballarin@28873
    92
text {* Alternative expression, obtaining nicer names in @{text "semi f"}. *}
ballarin@28873
    93
locale pert_hom' = semi f + d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2
ballarin@28873
    94
print_locale! pert_hom' thm pert_hom'_def
ballarin@28873
    95
ballarin@28873
    96
ballarin@28881
    97
text {* Syntax declarations *}
ballarin@28873
    98
ballarin@28873
    99
locale logic =
ballarin@28873
   100
  fixes land (infixl "&&" 55)
ballarin@28873
   101
    and lnot ("-- _" [60] 60)
ballarin@28873
   102
  assumes assoc: "(x && y) && z = x && (y && z)"
ballarin@28873
   103
    and notnot: "-- (-- x) = x"
ballarin@28873
   104
begin
ballarin@28873
   105
ballarin@28873
   106
definition lor (infixl "||" 50) where
ballarin@28873
   107
  "x || y = --(-- x && -- y)"
ballarin@28873
   108
ballarin@28873
   109
end
ballarin@28873
   110
print_locale! logic
ballarin@28873
   111
ballarin@28873
   112
locale use_decl = logic + semi "op ||"
ballarin@28873
   113
print_locale! use_decl thm use_decl_def
ballarin@28873
   114
ballarin@28881
   115
ballarin@28881
   116
text {* Theorem statements *}
ballarin@28881
   117
ballarin@28873
   118
lemma (in lgrp) lcancel:
ballarin@28873
   119
  "x ** y = x ** z <-> y = z"
ballarin@28873
   120
proof
ballarin@28873
   121
  assume "x ** y = x ** z"
ballarin@28873
   122
  then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
ballarin@28873
   123
  then show "y = z" by (simp add: lone linv)
ballarin@28873
   124
qed simp
ballarin@28881
   125
print_locale! lgrp
ballarin@28881
   126
ballarin@28873
   127
ballarin@28873
   128
locale rgrp = semi +
ballarin@28873
   129
  fixes one and inv
ballarin@28873
   130
  assumes rone: "x ** one = x"
ballarin@28873
   131
    and rinv: "x ** inv(x) = one"
ballarin@28881
   132
begin
ballarin@28873
   133
ballarin@28881
   134
lemma rcancel:
ballarin@28873
   135
  "y ** x = z ** x <-> y = z"
ballarin@28873
   136
proof
ballarin@28873
   137
  assume "y ** x = z ** x"
ballarin@28873
   138
  then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
ballarin@28873
   139
    by (simp add: assoc [symmetric])
ballarin@28873
   140
  then show "y = z" by (simp add: rone rinv)
ballarin@28873
   141
qed simp
ballarin@28873
   142
ballarin@28873
   143
end
ballarin@28881
   144
print_locale! rgrp
ballarin@28881
   145
ballarin@28886
   146
ballarin@28886
   147
text {* Patterns *}
ballarin@28886
   148
ballarin@28886
   149
lemma (in rgrp)
ballarin@28886
   150
  assumes "y ** x = z ** x" (is ?a)
ballarin@28886
   151
  shows "y = z" (is ?t)
ballarin@28886
   152
proof -
ballarin@28886
   153
  txt {* Weird proof involving patterns from context element and conclusion. *}
ballarin@28886
   154
  {
ballarin@28886
   155
    assume ?a
ballarin@28886
   156
    then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
ballarin@28886
   157
      by (simp add: assoc [symmetric])
ballarin@28886
   158
    then have ?t by (simp add: rone rinv)
ballarin@28886
   159
  }
ballarin@28886
   160
  note x = this
ballarin@28886
   161
  show ?t by (rule x [OF `?a`])
ballarin@28886
   162
qed
ballarin@28886
   163
ballarin@28896
   164
ballarin@28896
   165
text {* Interpretation between locales: sublocales *}
ballarin@28896
   166
ballarin@28896
   167
sublocale lgrp < right: rgrp
ballarin@28896
   168
print_facts
ballarin@28927
   169
proof unfold_locales
ballarin@28896
   170
  {
ballarin@28896
   171
    fix x
ballarin@28896
   172
    have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
ballarin@28896
   173
    then show "x ** one = x" by (simp add: assoc lcancel)
ballarin@28896
   174
  }
ballarin@28896
   175
  note rone = this
ballarin@28896
   176
  {
ballarin@28896
   177
    fix x
ballarin@28896
   178
    have "inv(x) ** x ** inv(x) = inv(x) ** one"
ballarin@28896
   179
      by (simp add: linv lone rone)
ballarin@28896
   180
    then show "x ** inv(x) = one" by (simp add: assoc lcancel)
ballarin@28896
   181
  }
ballarin@28903
   182
qed
ballarin@28896
   183
ballarin@28896
   184
(* effect on printed locale *)
ballarin@28896
   185
ballarin@28896
   186
print_locale! lgrp
ballarin@28896
   187
ballarin@28896
   188
(* use of derived theorem *)
ballarin@28896
   189
ballarin@28896
   190
lemma (in lgrp)
ballarin@28896
   191
  "y ** x = z ** x <-> y = z"
ballarin@28896
   192
  apply (rule rcancel)
ballarin@28896
   193
  done
ballarin@28896
   194
ballarin@28896
   195
(* circular interpretation *)
ballarin@28896
   196
ballarin@28896
   197
sublocale rgrp < left: lgrp
ballarin@28927
   198
proof unfold_locales
ballarin@28903
   199
  {
ballarin@28903
   200
    fix x
ballarin@28903
   201
    have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone)
ballarin@28903
   202
    then show "one ** x = x" by (simp add: assoc [symmetric] rcancel)
ballarin@28903
   203
  }
ballarin@28903
   204
  note lone = this
ballarin@28903
   205
  {
ballarin@28903
   206
    fix x
ballarin@28903
   207
    have "inv(x) ** (x ** inv(x)) = one ** inv(x)"
ballarin@28903
   208
      by (simp add: rinv lone rone)
ballarin@28903
   209
    then show "inv(x) ** x = one" by (simp add: assoc [symmetric] rcancel)
ballarin@28903
   210
  }
ballarin@28903
   211
qed
ballarin@28896
   212
ballarin@28896
   213
(* effect on printed locale *)
ballarin@28896
   214
ballarin@28896
   215
print_locale! rgrp
ballarin@28896
   216
print_locale! lgrp
ballarin@28896
   217
ballarin@28898
   218
ballarin@28899
   219
(* Duality *)
ballarin@28899
   220
ballarin@28899
   221
locale order =
ballarin@28899
   222
  fixes less :: "'a => 'a => o" (infix "<<" 50)
ballarin@28899
   223
  assumes refl: "x << x"
ballarin@28899
   224
    and trans: "[| x << y; y << z |] ==> x << z"
ballarin@28899
   225
ballarin@28899
   226
sublocale order < dual: order "%x y. y << x"
ballarin@28927
   227
  apply unfold_locales apply (rule refl) apply (blast intro: trans)
ballarin@28899
   228
  done
ballarin@28899
   229
ballarin@28899
   230
print_locale! order  (* Only two instances of order. *)
ballarin@28899
   231
ballarin@28899
   232
locale order' =
ballarin@28899
   233
  fixes less :: "'a => 'a => o" (infix "<<" 50)
ballarin@28899
   234
  assumes refl: "x << x"
ballarin@28899
   235
    and trans: "[| x << y; y << z |] ==> x << z"
ballarin@28899
   236
ballarin@28899
   237
locale order_with_def = order'
ballarin@28899
   238
begin
ballarin@28899
   239
ballarin@28899
   240
definition greater :: "'a => 'a => o" (infix ">>" 50) where
ballarin@28899
   241
  "x >> y <-> y << x"
ballarin@28899
   242
ballarin@28899
   243
end
ballarin@28899
   244
ballarin@28899
   245
sublocale order_with_def < dual: order' "op >>"
ballarin@28927
   246
  apply unfold_locales
ballarin@28899
   247
  unfolding greater_def
ballarin@28899
   248
  apply (rule refl) apply (blast intro: trans)
ballarin@28899
   249
  done
ballarin@28899
   250
ballarin@28899
   251
print_locale! order_with_def
ballarin@28899
   252
(* Note that decls come after theorems that make use of them.
ballarin@28899
   253
  Appears to be harmless at least in this example. *)
ballarin@28899
   254
ballarin@28899
   255
ballarin@28898
   256
(* locale with many parameters ---
ballarin@28898
   257
   interpretations generate alternating group A5 *)
ballarin@28898
   258
ballarin@28899
   259
ballarin@28898
   260
locale A5 =
ballarin@28898
   261
  fixes A and B and C and D and E
ballarin@28898
   262
  assumes eq: "A <-> B <-> C <-> D <-> E"
ballarin@28898
   263
ballarin@28898
   264
sublocale A5 < 1: A5 _ _ D E C
ballarin@28898
   265
print_facts
ballarin@28898
   266
  using eq apply (blast intro: A5.intro) done
ballarin@28898
   267
ballarin@28898
   268
sublocale A5 < 2: A5 C _ E _ A
ballarin@28898
   269
print_facts
ballarin@28898
   270
  using eq apply (blast intro: A5.intro) done
ballarin@28898
   271
ballarin@28898
   272
sublocale A5 < 3: A5 B C A _ _
ballarin@28898
   273
print_facts
ballarin@28898
   274
  using eq apply (blast intro: A5.intro) done
ballarin@28898
   275
ballarin@28898
   276
(* Any even permutation of parameters is subsumed by the above. *)
ballarin@28898
   277
ballarin@28898
   278
print_locale! A5
ballarin@28898
   279
ballarin@28898
   280
ballarin@28898
   281
(* Free arguments of instance *)
ballarin@28898
   282
ballarin@28898
   283
locale trivial =
ballarin@28898
   284
  fixes P and Q :: o
ballarin@28898
   285
  assumes Q: "P <-> P <-> Q"
ballarin@28898
   286
begin
ballarin@28898
   287
ballarin@28898
   288
lemma Q_triv: "Q" using Q by fast
ballarin@28898
   289
ballarin@28881
   290
end
ballarin@28898
   291
ballarin@28898
   292
sublocale trivial < x: trivial x _
ballarin@28927
   293
  apply unfold_locales using Q by fast
ballarin@28898
   294
ballarin@28898
   295
print_locale! trivial
ballarin@28898
   296
ballarin@28898
   297
context trivial begin thm x.Q [where ?x = True] end
ballarin@28898
   298
ballarin@28899
   299
sublocale trivial < y: trivial Q Q
ballarin@28927
   300
  by unfold_locales
ballarin@28903
   301
  (* Succeeds since previous interpretation is more general. *)
ballarin@28899
   302
ballarin@28899
   303
print_locale! trivial  (* No instance for y created (subsumed). *)
ballarin@28899
   304
ballarin@28993
   305
ballarin@28993
   306
text {* Sublocale, then interpretation in theory *}
ballarin@28993
   307
ballarin@28993
   308
interpretation int: lgrp "op +" "0" "minus"
ballarin@28993
   309
proof unfold_locales
ballarin@28993
   310
qed (rule int_assoc int_zero int_minus)+
ballarin@28993
   311
ballarin@28993
   312
thm int.assoc int.semi_axioms
ballarin@28993
   313
ballarin@28993
   314
interpretation int2: semi "op +"
ballarin@28993
   315
  by unfold_locales  (* subsumed, thm int2.assoc not generated *)
ballarin@28993
   316
ballarin@28993
   317
thm int.lone int.right.rone
ballarin@28993
   318
  (* the latter comes through the sublocale relation *)
ballarin@28993
   319
ballarin@28993
   320
ballarin@28993
   321
text {* Interpretation in theory, then sublocale *}
ballarin@28993
   322
ballarin@28993
   323
interpretation (* fol: *) logic "op +" "minus"
ballarin@28993
   324
(* FIXME declaration of qualified names *)
ballarin@28993
   325
  by unfold_locales (rule int_assoc int_minus2)+
ballarin@28993
   326
ballarin@28993
   327
locale logic2 =
ballarin@28993
   328
  fixes land (infixl "&&" 55)
ballarin@28993
   329
    and lnot ("-- _" [60] 60)
ballarin@28993
   330
  assumes assoc: "(x && y) && z = x && (y && z)"
ballarin@28993
   331
    and notnot: "-- (-- x) = x"
ballarin@28993
   332
begin
ballarin@28993
   333
(* FIXME
ballarin@28993
   334
definition lor (infixl "||" 50) where
ballarin@28993
   335
  "x || y = --(-- x && -- y)"
ballarin@28993
   336
*)
ballarin@28898
   337
end
ballarin@28993
   338
ballarin@28993
   339
sublocale logic < two: logic2
ballarin@28993
   340
  by unfold_locales (rule assoc notnot)+
ballarin@28993
   341
ballarin@28993
   342
thm two.assoc
ballarin@28993
   343
ballarin@29018
   344
ballarin@29018
   345
text {* Interpretation in proofs *}
ballarin@29018
   346
ballarin@29018
   347
lemma True
ballarin@29018
   348
proof
ballarin@29018
   349
  interpret "local": lgrp "op +" "0" "minus"
ballarin@29018
   350
    by unfold_locales  (* subsumed *)
ballarin@29018
   351
  {
ballarin@29018
   352
    fix zero :: int
ballarin@29018
   353
    assume "!!x. zero + x = x" "!!x. (-x) + x = zero"
ballarin@29018
   354
    then interpret local_fixed: lgrp "op +" zero "minus"
ballarin@29018
   355
      by unfold_locales
ballarin@29018
   356
    thm local_fixed.lone
ballarin@29018
   357
  }
ballarin@29018
   358
  assume "!!x zero. zero + x = x" "!!x zero. (-x) + x = zero"
ballarin@29018
   359
  then interpret local_free: lgrp "op +" zero "minus" for zero
ballarin@29018
   360
    by unfold_locales
ballarin@29018
   361
  thm local_free.lone [where ?zero = 0]
ballarin@29018
   362
qed
ballarin@29018
   363
ballarin@28993
   364
end