src/FOL/ex/Locale_Test/Locale_Test1.thy
author nipkow
Sat Jan 06 17:34:41 2018 +0100 (17 months ago)
changeset 67347 bf269672c203
parent 67119 acb0807ddb56
child 67399 eab6ce8368fa
permissions -rw-r--r--
tuned op
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
wenzelm@55380
    11
typedecl int
wenzelm@55380
    12
instance int :: "term" ..
wenzelm@55380
    13
ballarin@37134
    14
consts plus :: "int => int => int" (infixl "+" 60)
ballarin@37134
    15
  zero :: int ("0")
ballarin@37134
    16
  minus :: "int => int" ("- _")
ballarin@37134
    17
wenzelm@41779
    18
axiomatization where
wenzelm@41779
    19
  int_assoc: "(x + y::int) + z = x + (y + z)" and
wenzelm@41779
    20
  int_zero: "0 + x = x" and
wenzelm@41779
    21
  int_minus: "(-x) + x = 0" and
ballarin@37134
    22
  int_minus2: "-(-x) = x"
ballarin@37134
    23
wenzelm@60770
    24
section \<open>Inference of parameter types\<close>
ballarin@37134
    25
ballarin@37134
    26
locale param1 = fixes p
ballarin@37134
    27
print_locale! param1
ballarin@37134
    28
ballarin@37134
    29
locale param2 = fixes p :: 'b
ballarin@37134
    30
print_locale! param2
ballarin@37134
    31
ballarin@37134
    32
(*
ballarin@37134
    33
locale param_top = param2 r for r :: "'b :: {}"
ballarin@37134
    34
  Fails, cannot generalise parameter.
ballarin@37134
    35
*)
ballarin@37134
    36
ballarin@37134
    37
locale param3 = fixes p (infix ".." 50)
ballarin@37134
    38
print_locale! param3
ballarin@37134
    39
ballarin@37134
    40
locale param4 = fixes p :: "'a => 'a => 'a" (infix ".." 50)
ballarin@37134
    41
print_locale! param4
ballarin@37134
    42
ballarin@37134
    43
wenzelm@60770
    44
subsection \<open>Incremental type constraints\<close>
ballarin@37134
    45
ballarin@37134
    46
locale constraint1 =
ballarin@37134
    47
  fixes  prod (infixl "**" 65)
ballarin@37134
    48
  assumes l_id: "x ** y = x"
ballarin@37134
    49
  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
ballarin@37134
    50
print_locale! constraint1
ballarin@37134
    51
ballarin@37134
    52
locale constraint2 =
ballarin@37134
    53
  fixes p and q
ballarin@37134
    54
  assumes "p = q"
ballarin@37134
    55
print_locale! constraint2
ballarin@37134
    56
ballarin@37134
    57
wenzelm@60770
    58
section \<open>Inheritance\<close>
ballarin@37134
    59
ballarin@37134
    60
locale semi =
ballarin@37134
    61
  fixes prod (infixl "**" 65)
ballarin@37134
    62
  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
ballarin@37134
    63
print_locale! semi thm semi_def
ballarin@37134
    64
ballarin@37134
    65
locale lgrp = semi +
ballarin@37134
    66
  fixes one and inv
ballarin@37134
    67
  assumes lone: "one ** x = x"
ballarin@37134
    68
    and linv: "inv(x) ** x = one"
ballarin@37134
    69
print_locale! lgrp thm lgrp_def lgrp_axioms_def
ballarin@37134
    70
ballarin@37134
    71
locale add_lgrp = semi "op ++" for sum (infixl "++" 60) +
ballarin@37134
    72
  fixes zero and neg
ballarin@37134
    73
  assumes lzero: "zero ++ x = x"
ballarin@37134
    74
    and lneg: "neg(x) ++ x = zero"
ballarin@37134
    75
print_locale! add_lgrp thm add_lgrp_def add_lgrp_axioms_def
ballarin@37134
    76
ballarin@37134
    77
locale rev_lgrp = semi "%x y. y ++ x" for sum (infixl "++" 60)
ballarin@37134
    78
print_locale! rev_lgrp thm rev_lgrp_def
ballarin@37134
    79
ballarin@37134
    80
locale hom = f: semi f + g: semi g for f and g
ballarin@37134
    81
print_locale! hom thm hom_def
ballarin@37134
    82
ballarin@37134
    83
locale perturbation = semi + d: semi "%x y. delta(x) ** delta(y)" for delta
ballarin@37134
    84
print_locale! perturbation thm perturbation_def
ballarin@37134
    85
ballarin@37134
    86
locale pert_hom = d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2
ballarin@37134
    87
print_locale! pert_hom thm pert_hom_def
ballarin@37134
    88
wenzelm@62020
    89
text \<open>Alternative expression, obtaining nicer names in \<open>semi f\<close>.\<close>
ballarin@37134
    90
locale pert_hom' = semi f + d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2
ballarin@37134
    91
print_locale! pert_hom' thm pert_hom'_def
ballarin@37134
    92
ballarin@37134
    93
wenzelm@60770
    94
section \<open>Syntax declarations\<close>
ballarin@37134
    95
ballarin@37134
    96
locale logic =
ballarin@37134
    97
  fixes land (infixl "&&" 55)
ballarin@37134
    98
    and lnot ("-- _" [60] 60)
ballarin@37134
    99
  assumes assoc: "(x && y) && z = x && (y && z)"
ballarin@37134
   100
    and notnot: "-- (-- x) = x"
ballarin@37134
   101
begin
ballarin@37134
   102
ballarin@37134
   103
definition lor (infixl "||" 50) where
ballarin@37134
   104
  "x || y = --(-- x && -- y)"
ballarin@37134
   105
ballarin@37134
   106
end
ballarin@37134
   107
print_locale! logic
ballarin@37134
   108
wenzelm@49756
   109
locale use_decl = l: logic + semi "op ||"
ballarin@37134
   110
print_locale! use_decl thm use_decl_def
ballarin@37134
   111
ballarin@37134
   112
locale extra_type =
ballarin@37134
   113
  fixes a :: 'a
ballarin@37134
   114
    and P :: "'a => 'b => o"
ballarin@37134
   115
begin
ballarin@37134
   116
wenzelm@61489
   117
definition test :: "'a => o"
wenzelm@61489
   118
  where "test(x) \<longleftrightarrow> (\<forall>b. P(x, b))"
ballarin@37134
   119
ballarin@37134
   120
end
ballarin@37134
   121
ballarin@37134
   122
term extra_type.test thm extra_type.test_def
ballarin@37134
   123
ballarin@37134
   124
interpretation var?: extra_type "0" "%x y. x = 0" .
ballarin@37134
   125
ballarin@37134
   126
thm var.test_def
ballarin@37134
   127
ballarin@37134
   128
ballarin@61701
   129
text \<open>Under which circumstances notation remains active.\<close>
ballarin@37134
   130
wenzelm@60770
   131
ML \<open>
ballarin@37134
   132
  fun check_syntax ctxt thm expected =
ballarin@37134
   133
    let
wenzelm@56036
   134
      val obtained =
wenzelm@61268
   135
        Print_Mode.setmp [] (Thm.string_of_thm (Config.put show_markup false ctxt)) thm;
ballarin@37134
   136
    in
ballarin@37134
   137
      if obtained <> expected
ballarin@37134
   138
      then error ("Theorem syntax '" ^ obtained ^ "' obtained, but '" ^ expected ^ "' expected.")
ballarin@37134
   139
      else ()
ballarin@37134
   140
    end;
wenzelm@60770
   141
\<close>
ballarin@37134
   142
wenzelm@41305
   143
declare [[show_hyps]]
ballarin@41271
   144
ballarin@61701
   145
locale "syntax" =
ballarin@61701
   146
  fixes p1 :: "'a => 'b"
ballarin@61701
   147
    and p2 :: "'b => o"
ballarin@61701
   148
begin
ballarin@61701
   149
ballarin@61701
   150
definition d1 :: "'a => o" ("D1'(_')") where "d1(x) \<longleftrightarrow> \<not> p2(p1(x))"
ballarin@61701
   151
definition d2 :: "'b => o" ("D2'(_')") where "d2(x) \<longleftrightarrow> \<not> p2(x)"
ballarin@61701
   152
ballarin@61701
   153
thm d1_def d2_def
ballarin@61701
   154
ballarin@61701
   155
end
ballarin@61701
   156
ballarin@61701
   157
thm syntax.d1_def syntax.d2_def
ballarin@61701
   158
ballarin@61701
   159
locale syntax' = "syntax" p1 p2 for p1 :: "'a => 'a" and p2 :: "'a => o"
ballarin@61701
   160
begin
ballarin@61701
   161
ballarin@61701
   162
thm d1_def d2_def  (* should print as "D1(?x) <-> ..." and "D2(?x) <-> ..." *)
ballarin@61701
   163
wenzelm@60770
   164
ML \<open>
ballarin@61701
   165
  check_syntax @{context} @{thm d1_def} "D1(?x) \<longleftrightarrow> \<not> p2(p1(?x))";
ballarin@61701
   166
  check_syntax @{context} @{thm d2_def} "D2(?x) \<longleftrightarrow> \<not> p2(?x)";
wenzelm@60770
   167
\<close>
ballarin@37134
   168
ballarin@37134
   169
end
ballarin@37134
   170
ballarin@37134
   171
locale syntax'' = "syntax" p3 p2 for p3 :: "'a => 'b" and p2 :: "'b => o"
ballarin@37134
   172
begin
ballarin@37134
   173
ballarin@37134
   174
thm d1_def d2_def
ballarin@61701
   175
  (* should print as "d1(?x) <-> ..." and "D2(?x) <-> ..." *)
ballarin@37134
   176
wenzelm@60770
   177
ML \<open>
ballarin@61701
   178
  check_syntax @{context} @{thm d1_def} "d1(?x) \<longleftrightarrow> \<not> p2(p3(?x))";
ballarin@61701
   179
  check_syntax @{context} @{thm d2_def} "D2(?x) \<longleftrightarrow> \<not> p2(?x)";
wenzelm@60770
   180
\<close>
ballarin@37134
   181
ballarin@37134
   182
end
ballarin@37134
   183
ballarin@37134
   184
wenzelm@60770
   185
section \<open>Foundational versions of theorems\<close>
ballarin@37134
   186
ballarin@37134
   187
thm logic.assoc
ballarin@37134
   188
thm logic.lor_def
ballarin@37134
   189
ballarin@37134
   190
wenzelm@60770
   191
section \<open>Defines\<close>
ballarin@37134
   192
ballarin@37134
   193
locale logic_def =
ballarin@37134
   194
  fixes land (infixl "&&" 55)
ballarin@37134
   195
    and lor (infixl "||" 50)
ballarin@37134
   196
    and lnot ("-- _" [60] 60)
ballarin@37134
   197
  assumes assoc: "(x && y) && z = x && (y && z)"
ballarin@37134
   198
    and notnot: "-- (-- x) = x"
ballarin@37134
   199
  defines "x || y == --(-- x && -- y)"
ballarin@37134
   200
begin
ballarin@37134
   201
ballarin@37134
   202
thm lor_def
ballarin@37134
   203
ballarin@37134
   204
lemma "x || y = --(-- x && --y)"
ballarin@37134
   205
  by (unfold lor_def) (rule refl)
ballarin@37134
   206
ballarin@37134
   207
end
ballarin@37134
   208
ballarin@37134
   209
(* Inheritance of defines *)
ballarin@37134
   210
ballarin@37134
   211
locale logic_def2 = logic_def
ballarin@37134
   212
begin
ballarin@37134
   213
ballarin@37134
   214
lemma "x || y = --(-- x && --y)"
ballarin@37134
   215
  by (unfold lor_def) (rule refl)
ballarin@37134
   216
ballarin@37134
   217
end
ballarin@37134
   218
ballarin@37134
   219
wenzelm@60770
   220
section \<open>Notes\<close>
ballarin@37134
   221
ballarin@37134
   222
(* A somewhat arcane homomorphism example *)
ballarin@37134
   223
ballarin@37134
   224
definition semi_hom where
wenzelm@61489
   225
  "semi_hom(prod, sum, h) \<longleftrightarrow> (\<forall>x y. h(prod(x, y)) = sum(h(x), h(y)))"
ballarin@37134
   226
ballarin@37134
   227
lemma semi_hom_mult:
wenzelm@61489
   228
  "semi_hom(prod, sum, h) \<Longrightarrow> h(prod(x, y)) = sum(h(x), h(y))"
ballarin@37134
   229
  by (simp add: semi_hom_def)
ballarin@37134
   230
ballarin@37134
   231
locale semi_hom_loc = prod: semi prod + sum: semi sum
ballarin@37134
   232
  for prod and sum and h +
ballarin@37134
   233
  assumes semi_homh: "semi_hom(prod, sum, h)"
ballarin@37134
   234
  notes semi_hom_mult = semi_hom_mult [OF semi_homh]
ballarin@37134
   235
ballarin@37134
   236
thm semi_hom_loc.semi_hom_mult
ballarin@37134
   237
(* unspecified, attribute not applied in backgroud theory !!! *)
ballarin@37134
   238
ballarin@37134
   239
lemma (in semi_hom_loc) "h(prod(x, y)) = sum(h(x), h(y))"
ballarin@37134
   240
  by (rule semi_hom_mult)
ballarin@37134
   241
ballarin@37134
   242
(* Referring to facts from within a context specification *)
ballarin@37134
   243
ballarin@37134
   244
lemma
wenzelm@61489
   245
  assumes x: "P \<longleftrightarrow> P"
ballarin@37134
   246
  notes y = x
ballarin@37134
   247
  shows True ..
ballarin@37134
   248
ballarin@37134
   249
wenzelm@60770
   250
section \<open>Theorem statements\<close>
ballarin@37134
   251
ballarin@37134
   252
lemma (in lgrp) lcancel:
wenzelm@61489
   253
  "x ** y = x ** z \<longleftrightarrow> y = z"
ballarin@37134
   254
proof
ballarin@37134
   255
  assume "x ** y = x ** z"
ballarin@37134
   256
  then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
ballarin@37134
   257
  then show "y = z" by (simp add: lone linv)
ballarin@37134
   258
qed simp
ballarin@37134
   259
print_locale! lgrp
ballarin@37134
   260
ballarin@37134
   261
ballarin@37134
   262
locale rgrp = semi +
ballarin@37134
   263
  fixes one and inv
ballarin@37134
   264
  assumes rone: "x ** one = x"
ballarin@37134
   265
    and rinv: "x ** inv(x) = one"
ballarin@37134
   266
begin
ballarin@37134
   267
ballarin@37134
   268
lemma rcancel:
wenzelm@61489
   269
  "y ** x = z ** x \<longleftrightarrow> y = z"
ballarin@37134
   270
proof
ballarin@37134
   271
  assume "y ** x = z ** x"
ballarin@37134
   272
  then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
ballarin@37134
   273
    by (simp add: assoc [symmetric])
ballarin@37134
   274
  then show "y = z" by (simp add: rone rinv)
ballarin@37134
   275
qed simp
ballarin@37134
   276
ballarin@37134
   277
end
ballarin@37134
   278
print_locale! rgrp
ballarin@37134
   279
ballarin@37134
   280
wenzelm@60770
   281
subsection \<open>Patterns\<close>
ballarin@37134
   282
ballarin@37134
   283
lemma (in rgrp)
ballarin@37134
   284
  assumes "y ** x = z ** x" (is ?a)
ballarin@37134
   285
  shows "y = z" (is ?t)
ballarin@37134
   286
proof -
wenzelm@60770
   287
  txt \<open>Weird proof involving patterns from context element and conclusion.\<close>
ballarin@37134
   288
  {
ballarin@37134
   289
    assume ?a
ballarin@37134
   290
    then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
ballarin@37134
   291
      by (simp add: assoc [symmetric])
ballarin@37134
   292
    then have ?t by (simp add: rone rinv)
ballarin@37134
   293
  }
ballarin@37134
   294
  note x = this
wenzelm@60770
   295
  show ?t by (rule x [OF \<open>?a\<close>])
ballarin@37134
   296
qed
ballarin@37134
   297
ballarin@37134
   298
wenzelm@60770
   299
section \<open>Interpretation between locales: sublocales\<close>
ballarin@37134
   300
ballarin@61565
   301
sublocale lgrp < right?: rgrp
ballarin@37134
   302
print_facts
ballarin@37134
   303
proof unfold_locales
ballarin@37134
   304
  {
ballarin@37134
   305
    fix x
ballarin@37134
   306
    have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
ballarin@37134
   307
    then show "x ** one = x" by (simp add: assoc lcancel)
ballarin@37134
   308
  }
ballarin@37134
   309
  note rone = this
ballarin@37134
   310
  {
ballarin@37134
   311
    fix x
ballarin@37134
   312
    have "inv(x) ** x ** inv(x) = inv(x) ** one"
ballarin@37134
   313
      by (simp add: linv lone rone)
ballarin@37134
   314
    then show "x ** inv(x) = one" by (simp add: assoc lcancel)
ballarin@37134
   315
  }
ballarin@37134
   316
qed
ballarin@37134
   317
ballarin@37134
   318
(* effect on printed locale *)
ballarin@37134
   319
ballarin@37134
   320
print_locale! lgrp
ballarin@37134
   321
ballarin@37134
   322
(* use of derived theorem *)
ballarin@37134
   323
ballarin@37134
   324
lemma (in lgrp)
wenzelm@61489
   325
  "y ** x = z ** x \<longleftrightarrow> y = z"
ballarin@37134
   326
  apply (rule rcancel)
ballarin@37134
   327
  done
ballarin@37134
   328
ballarin@37134
   329
(* circular interpretation *)
ballarin@37134
   330
ballarin@37134
   331
sublocale rgrp < left: lgrp
ballarin@37134
   332
proof unfold_locales
ballarin@37134
   333
  {
ballarin@37134
   334
    fix x
ballarin@37134
   335
    have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone)
ballarin@37134
   336
    then show "one ** x = x" by (simp add: assoc [symmetric] rcancel)
ballarin@37134
   337
  }
ballarin@37134
   338
  note lone = this
ballarin@37134
   339
  {
ballarin@37134
   340
    fix x
ballarin@37134
   341
    have "inv(x) ** (x ** inv(x)) = one ** inv(x)"
ballarin@37134
   342
      by (simp add: rinv lone rone)
ballarin@37134
   343
    then show "inv(x) ** x = one" by (simp add: assoc [symmetric] rcancel)
ballarin@37134
   344
  }
ballarin@37134
   345
qed
ballarin@37134
   346
ballarin@37134
   347
(* effect on printed locale *)
ballarin@37134
   348
ballarin@37134
   349
print_locale! rgrp
ballarin@37134
   350
print_locale! lgrp
ballarin@37134
   351
ballarin@37134
   352
ballarin@37134
   353
(* Duality *)
ballarin@37134
   354
ballarin@37134
   355
locale order =
ballarin@37134
   356
  fixes less :: "'a => 'a => o" (infix "<<" 50)
ballarin@37134
   357
  assumes refl: "x << x"
ballarin@37134
   358
    and trans: "[| x << y; y << z |] ==> x << z"
ballarin@37134
   359
ballarin@37134
   360
sublocale order < dual: order "%x y. y << x"
ballarin@37134
   361
  apply unfold_locales apply (rule refl) apply (blast intro: trans)
ballarin@37134
   362
  done
ballarin@37134
   363
ballarin@37134
   364
print_locale! order  (* Only two instances of order. *)
ballarin@37134
   365
ballarin@37134
   366
locale order' =
ballarin@37134
   367
  fixes less :: "'a => 'a => o" (infix "<<" 50)
ballarin@37134
   368
  assumes refl: "x << x"
ballarin@37134
   369
    and trans: "[| x << y; y << z |] ==> x << z"
ballarin@37134
   370
ballarin@37134
   371
locale order_with_def = order'
ballarin@37134
   372
begin
ballarin@37134
   373
ballarin@37134
   374
definition greater :: "'a => 'a => o" (infix ">>" 50) where
wenzelm@61489
   375
  "x >> y \<longleftrightarrow> y << x"
ballarin@37134
   376
ballarin@37134
   377
end
ballarin@37134
   378
ballarin@37134
   379
sublocale order_with_def < dual: order' "op >>"
ballarin@37134
   380
  apply unfold_locales
ballarin@37134
   381
  unfolding greater_def
ballarin@37134
   382
  apply (rule refl) apply (blast intro: trans)
ballarin@37134
   383
  done
ballarin@37134
   384
ballarin@37134
   385
print_locale! order_with_def
ballarin@37134
   386
(* Note that decls come after theorems that make use of them. *)
ballarin@37134
   387
ballarin@37134
   388
ballarin@37134
   389
(* locale with many parameters ---
ballarin@37134
   390
   interpretations generate alternating group A5 *)
ballarin@37134
   391
ballarin@37134
   392
ballarin@37134
   393
locale A5 =
ballarin@37134
   394
  fixes A and B and C and D and E
wenzelm@61489
   395
  assumes eq: "A \<longleftrightarrow> B \<longleftrightarrow> C \<longleftrightarrow> D \<longleftrightarrow> E"
ballarin@37134
   396
ballarin@37134
   397
sublocale A5 < 1: A5 _ _ D E C
ballarin@37134
   398
print_facts
ballarin@37134
   399
  using eq apply (blast intro: A5.intro) done
ballarin@37134
   400
ballarin@37134
   401
sublocale A5 < 2: A5 C _ E _ A
ballarin@37134
   402
print_facts
ballarin@37134
   403
  using eq apply (blast intro: A5.intro) done
ballarin@37134
   404
ballarin@37134
   405
sublocale A5 < 3: A5 B C A _ _
ballarin@37134
   406
print_facts
ballarin@37134
   407
  using eq apply (blast intro: A5.intro) done
ballarin@37134
   408
ballarin@37134
   409
(* Any even permutation of parameters is subsumed by the above. *)
ballarin@37134
   410
ballarin@37134
   411
print_locale! A5
ballarin@37134
   412
ballarin@37134
   413
ballarin@37134
   414
(* Free arguments of instance *)
ballarin@37134
   415
ballarin@37134
   416
locale trivial =
ballarin@37134
   417
  fixes P and Q :: o
wenzelm@61489
   418
  assumes Q: "P \<longleftrightarrow> P \<longleftrightarrow> Q"
ballarin@37134
   419
begin
ballarin@37134
   420
ballarin@37134
   421
lemma Q_triv: "Q" using Q by fast
ballarin@37134
   422
ballarin@37134
   423
end
ballarin@37134
   424
ballarin@37134
   425
sublocale trivial < x: trivial x _
ballarin@37134
   426
  apply unfold_locales using Q by fast
ballarin@37134
   427
ballarin@37134
   428
print_locale! trivial
ballarin@37134
   429
ballarin@37134
   430
context trivial begin thm x.Q [where ?x = True] end
ballarin@37134
   431
ballarin@37134
   432
sublocale trivial < y: trivial Q Q
ballarin@37134
   433
  by unfold_locales
ballarin@37134
   434
  (* Succeeds since previous interpretation is more general. *)
ballarin@37134
   435
ballarin@37134
   436
print_locale! trivial  (* No instance for y created (subsumed). *)
ballarin@37134
   437
ballarin@37134
   438
wenzelm@60770
   439
subsection \<open>Sublocale, then interpretation in theory\<close>
ballarin@37134
   440
ballarin@37134
   441
interpretation int?: lgrp "op +" "0" "minus"
ballarin@37134
   442
proof unfold_locales
ballarin@37134
   443
qed (rule int_assoc int_zero int_minus)+
ballarin@37134
   444
ballarin@37134
   445
thm int.assoc int.semi_axioms
ballarin@37134
   446
ballarin@37134
   447
interpretation int2?: semi "op +"
ballarin@37134
   448
  by unfold_locales  (* subsumed, thm int2.assoc not generated *)
ballarin@37134
   449
wenzelm@60770
   450
ML \<open>(Global_Theory.get_thms @{theory} "int2.assoc";
wenzelm@56138
   451
    raise Fail "thm int2.assoc was generated")
wenzelm@60770
   452
  handle ERROR _ => ([]:thm list);\<close>
ballarin@37134
   453
ballarin@37134
   454
thm int.lone int.right.rone
ballarin@37134
   455
  (* the latter comes through the sublocale relation *)
ballarin@37134
   456
ballarin@37134
   457
wenzelm@60770
   458
subsection \<open>Interpretation in theory, then sublocale\<close>
ballarin@37134
   459
ballarin@37134
   460
interpretation fol: logic "op +" "minus"
ballarin@37134
   461
  by unfold_locales (rule int_assoc int_minus2)+
ballarin@37134
   462
ballarin@37134
   463
locale logic2 =
ballarin@37134
   464
  fixes land (infixl "&&" 55)
ballarin@37134
   465
    and lnot ("-- _" [60] 60)
ballarin@37134
   466
  assumes assoc: "(x && y) && z = x && (y && z)"
ballarin@37134
   467
    and notnot: "-- (-- x) = x"
ballarin@37134
   468
begin
ballarin@37134
   469
ballarin@37134
   470
definition lor (infixl "||" 50) where
ballarin@37134
   471
  "x || y = --(-- x && -- y)"
ballarin@37134
   472
ballarin@37134
   473
end
ballarin@37134
   474
ballarin@37134
   475
sublocale logic < two: logic2
ballarin@37134
   476
  by unfold_locales (rule assoc notnot)+
ballarin@37134
   477
ballarin@37134
   478
thm fol.two.assoc
ballarin@37134
   479
ballarin@37134
   480
wenzelm@60770
   481
subsection \<open>Declarations and sublocale\<close>
ballarin@37134
   482
ballarin@37134
   483
locale logic_a = logic
ballarin@37134
   484
locale logic_b = logic
ballarin@37134
   485
ballarin@37134
   486
sublocale logic_a < logic_b
ballarin@37134
   487
  by unfold_locales
ballarin@37134
   488
ballarin@37134
   489
wenzelm@60770
   490
subsection \<open>Interpretation\<close>
ballarin@53366
   491
wenzelm@60770
   492
subsection \<open>Rewrite morphism\<close>
ballarin@37134
   493
ballarin@37134
   494
locale logic_o =
ballarin@37134
   495
  fixes land (infixl "&&" 55)
ballarin@37134
   496
    and lnot ("-- _" [60] 60)
wenzelm@61489
   497
  assumes assoc_o: "(x && y) && z \<longleftrightarrow> x && (y && z)"
wenzelm@61489
   498
    and notnot_o: "-- (-- x) \<longleftrightarrow> x"
ballarin@37134
   499
begin
ballarin@37134
   500
ballarin@37134
   501
definition lor_o (infixl "||" 50) where
wenzelm@61489
   502
  "x || y \<longleftrightarrow> --(-- x && -- y)"
ballarin@37134
   503
ballarin@37134
   504
end
ballarin@37134
   505
wenzelm@61489
   506
interpretation x: logic_o "op \<and>" "Not"
ballarin@61566
   507
  rewrites bool_logic_o: "x.lor_o(x, y) \<longleftrightarrow> x \<or> y"
ballarin@37134
   508
proof -
wenzelm@61489
   509
  show bool_logic_o: "PROP logic_o(op \<and>, Not)" by unfold_locales fast+
wenzelm@61489
   510
  show "logic_o.lor_o(op \<and>, Not, x, y) \<longleftrightarrow> x \<or> y"
ballarin@37134
   511
    by (unfold logic_o.lor_o_def [OF bool_logic_o]) fast
ballarin@37134
   512
qed
ballarin@37134
   513
ballarin@37134
   514
thm x.lor_o_def bool_logic_o
ballarin@37134
   515
wenzelm@61489
   516
lemma lor_triv: "z \<longleftrightarrow> z" ..
ballarin@37134
   517
wenzelm@61489
   518
lemma (in logic_o) lor_triv: "x || y \<longleftrightarrow> x || y" by fast
ballarin@37134
   519
ballarin@37134
   520
thm lor_triv [where z = True] (* Check strict prefix. *)
ballarin@37134
   521
  x.lor_triv
ballarin@37134
   522
ballarin@37134
   523
wenzelm@60770
   524
subsection \<open>Inheritance of rewrite morphisms\<close>
ballarin@37134
   525
ballarin@37134
   526
locale reflexive =
ballarin@37134
   527
  fixes le :: "'a => 'a => o" (infix "\<sqsubseteq>" 50)
ballarin@37134
   528
  assumes refl: "x \<sqsubseteq> x"
ballarin@37134
   529
begin
ballarin@37134
   530
wenzelm@61489
   531
definition less (infix "\<sqsubset>" 50) where "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<noteq> y"
ballarin@37134
   532
ballarin@37134
   533
end
ballarin@37134
   534
wenzelm@41779
   535
axiomatization
wenzelm@41779
   536
  gle :: "'a => 'a => o" and gless :: "'a => 'a => o" and
wenzelm@41779
   537
  gle' :: "'a => 'a => o" and gless' :: "'a => 'a => o"
wenzelm@41779
   538
where
wenzelm@61489
   539
  grefl: "gle(x, x)" and gless_def: "gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y" and
wenzelm@61489
   540
  grefl': "gle'(x, x)" and gless'_def: "gless'(x, y) \<longleftrightarrow> gle'(x, y) \<and> x \<noteq> y"
ballarin@37134
   541
wenzelm@60770
   542
text \<open>Setup\<close>
ballarin@37134
   543
ballarin@37134
   544
locale mixin = reflexive
ballarin@37134
   545
begin
ballarin@37134
   546
lemmas less_thm = less_def
ballarin@37134
   547
end
ballarin@37134
   548
ballarin@61566
   549
interpretation le: mixin gle rewrites "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
ballarin@37134
   550
proof -
ballarin@37134
   551
  show "mixin(gle)" by unfold_locales (rule grefl)
ballarin@37134
   552
  note reflexive = this[unfolded mixin_def]
wenzelm@61489
   553
  show "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
ballarin@37134
   554
    by (simp add: reflexive.less_def[OF reflexive] gless_def)
ballarin@37134
   555
qed
ballarin@37134
   556
wenzelm@60770
   557
text \<open>Rewrite morphism propagated along the locale hierarchy\<close>
ballarin@37134
   558
ballarin@37134
   559
locale mixin2 = mixin
ballarin@37134
   560
begin
ballarin@37134
   561
lemmas less_thm2 = less_def
ballarin@37134
   562
end
ballarin@37134
   563
ballarin@37134
   564
interpretation le: mixin2 gle
ballarin@37134
   565
  by unfold_locales
ballarin@37134
   566
ballarin@53366
   567
thm le.less_thm2  (* rewrite morphism applied *)
wenzelm@61489
   568
lemma "gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y"
ballarin@37134
   569
  by (rule le.less_thm2)
ballarin@37134
   570
wenzelm@60770
   571
text \<open>Rewrite morphism does not leak to a side branch.\<close>
ballarin@37134
   572
ballarin@37134
   573
locale mixin3 = reflexive
ballarin@37134
   574
begin
ballarin@37134
   575
lemmas less_thm3 = less_def
ballarin@37134
   576
end
ballarin@37134
   577
ballarin@37134
   578
interpretation le: mixin3 gle
ballarin@37134
   579
  by unfold_locales
ballarin@37134
   580
ballarin@53366
   581
thm le.less_thm3  (* rewrite morphism not applied *)
wenzelm@61489
   582
lemma "reflexive.less(gle, x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y" by (rule le.less_thm3)
ballarin@37134
   583
wenzelm@60770
   584
text \<open>Rewrite morphism only available in original context\<close>
ballarin@37134
   585
ballarin@37134
   586
locale mixin4_base = reflexive
ballarin@37134
   587
ballarin@37134
   588
locale mixin4_mixin = mixin4_base
ballarin@37134
   589
ballarin@37134
   590
interpretation le: mixin4_mixin gle
ballarin@61566
   591
  rewrites "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
ballarin@37134
   592
proof -
ballarin@37134
   593
  show "mixin4_mixin(gle)" by unfold_locales (rule grefl)
ballarin@37134
   594
  note reflexive = this[unfolded mixin4_mixin_def mixin4_base_def mixin_def]
wenzelm@61489
   595
  show "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
ballarin@37134
   596
    by (simp add: reflexive.less_def[OF reflexive] gless_def)
ballarin@37134
   597
qed
ballarin@37134
   598
ballarin@37134
   599
locale mixin4_copy = mixin4_base
ballarin@37134
   600
begin
ballarin@37134
   601
lemmas less_thm4 = less_def
ballarin@37134
   602
end
ballarin@37134
   603
ballarin@61565
   604
locale mixin4_combined = le1?: mixin4_mixin le' + le2?: mixin4_copy le for le' le
ballarin@37134
   605
begin
ballarin@37134
   606
lemmas less_thm4' = less_def
ballarin@37134
   607
end
ballarin@37134
   608
ballarin@37134
   609
interpretation le4: mixin4_combined gle' gle
ballarin@37134
   610
  by unfold_locales (rule grefl')
ballarin@37134
   611
ballarin@53366
   612
thm le4.less_thm4' (* rewrite morphism not applied *)
wenzelm@61489
   613
lemma "reflexive.less(gle, x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y"
ballarin@37134
   614
  by (rule le4.less_thm4')
ballarin@37134
   615
wenzelm@60770
   616
text \<open>Inherited rewrite morphism applied to new theorem\<close>
ballarin@37134
   617
ballarin@37134
   618
locale mixin5_base = reflexive
ballarin@37134
   619
ballarin@37134
   620
locale mixin5_inherited = mixin5_base
ballarin@37134
   621
ballarin@37134
   622
interpretation le5: mixin5_base gle
ballarin@61566
   623
  rewrites "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
ballarin@37134
   624
proof -
ballarin@37134
   625
  show "mixin5_base(gle)" by unfold_locales
ballarin@37134
   626
  note reflexive = this[unfolded mixin5_base_def mixin_def]
wenzelm@61489
   627
  show "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
ballarin@37134
   628
    by (simp add: reflexive.less_def[OF reflexive] gless_def)
ballarin@37134
   629
qed
ballarin@37134
   630
ballarin@37134
   631
interpretation le5: mixin5_inherited gle
ballarin@37134
   632
  by unfold_locales
ballarin@37134
   633
ballarin@37134
   634
lemmas (in mixin5_inherited) less_thm5 = less_def
ballarin@37134
   635
ballarin@53366
   636
thm le5.less_thm5  (* rewrite morphism applied *)
wenzelm@61489
   637
lemma "gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y"
ballarin@37134
   638
  by (rule le5.less_thm5)
ballarin@37134
   639
wenzelm@60770
   640
text \<open>Rewrite morphism pushed down to existing inherited locale\<close>
ballarin@37134
   641
ballarin@37134
   642
locale mixin6_base = reflexive
ballarin@37134
   643
ballarin@37134
   644
locale mixin6_inherited = mixin5_base
ballarin@37134
   645
ballarin@37134
   646
interpretation le6: mixin6_base gle
ballarin@37134
   647
  by unfold_locales
ballarin@37134
   648
interpretation le6: mixin6_inherited gle
ballarin@37134
   649
  by unfold_locales
ballarin@37134
   650
interpretation le6: mixin6_base gle
ballarin@61566
   651
  rewrites "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
ballarin@37134
   652
proof -
ballarin@37134
   653
  show "mixin6_base(gle)" by unfold_locales
ballarin@37134
   654
  note reflexive = this[unfolded mixin6_base_def mixin_def]
wenzelm@61489
   655
  show "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
ballarin@37134
   656
    by (simp add: reflexive.less_def[OF reflexive] gless_def)
ballarin@37134
   657
qed
ballarin@37134
   658
ballarin@37134
   659
lemmas (in mixin6_inherited) less_thm6 = less_def
ballarin@37134
   660
ballarin@37134
   661
thm le6.less_thm6  (* mixin applied *)
wenzelm@61489
   662
lemma "gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y"
ballarin@37134
   663
  by (rule le6.less_thm6)
ballarin@37134
   664
wenzelm@60770
   665
text \<open>Existing rewrite morphism inherited through sublocale relation\<close>
ballarin@37134
   666
ballarin@37134
   667
locale mixin7_base = reflexive
ballarin@37134
   668
ballarin@37134
   669
locale mixin7_inherited = reflexive
ballarin@37134
   670
ballarin@37134
   671
interpretation le7: mixin7_base gle
ballarin@61566
   672
  rewrites "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
ballarin@37134
   673
proof -
ballarin@37134
   674
  show "mixin7_base(gle)" by unfold_locales
ballarin@37134
   675
  note reflexive = this[unfolded mixin7_base_def mixin_def]
wenzelm@61489
   676
  show "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
ballarin@37134
   677
    by (simp add: reflexive.less_def[OF reflexive] gless_def)
ballarin@37134
   678
qed
ballarin@37134
   679
ballarin@37134
   680
interpretation le7: mixin7_inherited gle
ballarin@37134
   681
  by unfold_locales
ballarin@37134
   682
ballarin@37134
   683
lemmas (in mixin7_inherited) less_thm7 = less_def
ballarin@37134
   684
ballarin@53366
   685
thm le7.less_thm7  (* before, rewrite morphism not applied *)
wenzelm@61489
   686
lemma "reflexive.less(gle, x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y"
ballarin@37134
   687
  by (rule le7.less_thm7)
ballarin@37134
   688
ballarin@37134
   689
sublocale mixin7_inherited < mixin7_base
ballarin@37134
   690
  by unfold_locales
ballarin@37134
   691
ballarin@37134
   692
lemmas (in mixin7_inherited) less_thm7b = less_def
ballarin@37134
   693
ballarin@37134
   694
thm le7.less_thm7b  (* after, mixin applied *)
wenzelm@61489
   695
lemma "gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y"
ballarin@37134
   696
  by (rule le7.less_thm7b)
ballarin@37134
   697
ballarin@37134
   698
wenzelm@60770
   699
text \<open>This locale will be interpreted in later theories.\<close>
ballarin@37134
   700
ballarin@37134
   701
locale mixin_thy_merge = le: reflexive le + le': reflexive le' for le le'
ballarin@37134
   702
ballarin@37134
   703
wenzelm@60770
   704
subsection \<open>Rewrite morphisms in sublocale\<close>
ballarin@41272
   705
wenzelm@60770
   706
text \<open>Simulate a specification of left groups where unit and inverse are defined
ballarin@41272
   707
  rather than specified.  This is possible, but not in FOL, due to the lack of a
wenzelm@60770
   708
  selection operator.\<close>
ballarin@41272
   709
ballarin@41272
   710
axiomatization glob_one and glob_inv
ballarin@41272
   711
  where glob_lone: "prod(glob_one(prod), x) = x"
ballarin@41272
   712
    and glob_linv: "prod(glob_inv(prod, x), x) = glob_one(prod)"
ballarin@41272
   713
ballarin@41272
   714
locale dgrp = semi
ballarin@41272
   715
begin
ballarin@41272
   716
ballarin@41272
   717
definition one where "one = glob_one(prod)"
ballarin@41272
   718
ballarin@41272
   719
lemma lone: "one ** x = x"
ballarin@41272
   720
  unfolding one_def by (rule glob_lone)
ballarin@41272
   721
ballarin@41272
   722
definition inv where "inv(x) = glob_inv(prod, x)"
ballarin@41272
   723
ballarin@41272
   724
lemma linv: "inv(x) ** x = one"
ballarin@41272
   725
  unfolding one_def inv_def by (rule glob_linv)
ballarin@41272
   726
ballarin@41272
   727
end
ballarin@41272
   728
wenzelm@67119
   729
sublocale lgrp < def?: dgrp
ballarin@61566
   730
  rewrites one_equation: "dgrp.one(prod) = one" and inv_equation: "dgrp.inv(prod, x) = inv(x)"
ballarin@41272
   731
proof -
ballarin@41272
   732
  show "dgrp(prod)" by unfold_locales
ballarin@41272
   733
  from this interpret d: dgrp .
wenzelm@62020
   734
  \<comment> Unit
ballarin@41272
   735
  have "dgrp.one(prod) = glob_one(prod)" by (rule d.one_def)
ballarin@41272
   736
  also have "... = glob_one(prod) ** one" by (simp add: rone)
ballarin@41272
   737
  also have "... = one" by (simp add: glob_lone)
ballarin@41272
   738
  finally show "dgrp.one(prod) = one" .
wenzelm@62020
   739
  \<comment> Inverse
ballarin@41272
   740
  then have "dgrp.inv(prod, x) ** x = inv(x) ** x" by (simp add: glob_linv d.linv linv)
ballarin@41272
   741
  then show "dgrp.inv(prod, x) = inv(x)" by (simp add: rcancel)
ballarin@41272
   742
qed
ballarin@41272
   743
ballarin@41272
   744
print_locale! lgrp
ballarin@41272
   745
ballarin@41272
   746
context lgrp begin
ballarin@41272
   747
wenzelm@60770
   748
text \<open>Equations stored in target\<close>
ballarin@41272
   749
ballarin@41272
   750
lemma "dgrp.one(prod) = one" by (rule one_equation)
ballarin@41272
   751
lemma "dgrp.inv(prod, x) = inv(x)" by (rule inv_equation)
ballarin@41272
   752
wenzelm@60770
   753
text \<open>Rewrite morphisms applied\<close>
ballarin@41272
   754
ballarin@41272
   755
lemma "one = glob_one(prod)" by (rule one_def)
ballarin@41272
   756
lemma "inv(x) = glob_inv(prod, x)" by (rule inv_def)
ballarin@41272
   757
ballarin@41272
   758
end
ballarin@41272
   759
wenzelm@60770
   760
text \<open>Interpreted versions\<close>
ballarin@41272
   761
nipkow@67347
   762
lemma "0 = glob_one ((op +))" by (rule int.def.one_def)
ballarin@41272
   763
lemma "- x = glob_inv(op +, x)" by (rule int.def.inv_def)
ballarin@41272
   764
wenzelm@60770
   765
text \<open>Roundup applies rewrite morphisms at declaration level in DFS tree\<close>
ballarin@51515
   766
wenzelm@61489
   767
locale roundup = fixes x assumes true: "x \<longleftrightarrow> True"
ballarin@51515
   768
ballarin@61566
   769
sublocale roundup \<subseteq> sub: roundup x rewrites "x \<longleftrightarrow> True \<and> True"
ballarin@51515
   770
  apply unfold_locales apply (simp add: true) done
wenzelm@61489
   771
lemma (in roundup) "True \<and> True \<longleftrightarrow> True" by (rule sub.true)
ballarin@51515
   772
ballarin@41272
   773
wenzelm@60770
   774
section \<open>Interpretation in named contexts\<close>
ballarin@53367
   775
ballarin@53367
   776
locale container
ballarin@53367
   777
begin
wenzelm@61605
   778
interpretation "private": roundup True by unfold_locales rule
ballarin@53367
   779
lemmas true_copy = private.true
ballarin@53367
   780
end
ballarin@53367
   781
ballarin@53367
   782
context container begin
wenzelm@60770
   783
ML \<open>(Context.>> (fn generic => let val context = Context.proof_of generic
ballarin@53367
   784
  val _ = Proof_Context.get_thms context "private.true" in generic end);
wenzelm@56138
   785
  raise Fail "thm private.true was persisted")
wenzelm@60770
   786
  handle ERROR _ => ([]:thm list);\<close>
ballarin@53367
   787
thm true_copy
ballarin@53367
   788
end
ballarin@53367
   789
ballarin@53367
   790
wenzelm@60770
   791
section \<open>Interpretation in proofs\<close>
ballarin@37134
   792
ballarin@37134
   793
lemma True
ballarin@37134
   794
proof
ballarin@37134
   795
  interpret "local": lgrp "op +" "0" "minus"
ballarin@37134
   796
    by unfold_locales  (* subsumed *)
ballarin@37134
   797
  {
ballarin@37134
   798
    fix zero :: int
ballarin@37134
   799
    assume "!!x. zero + x = x" "!!x. (-x) + x = zero"
ballarin@37134
   800
    then interpret local_fixed: lgrp "op +" zero "minus"
ballarin@37134
   801
      by unfold_locales
ballarin@37134
   802
    thm local_fixed.lone
ballarin@41435
   803
    print_dependencies! lgrp "op +" 0 minus + lgrp "op +" zero minus
ballarin@37134
   804
  }
ballarin@37134
   805
  assume "!!x zero. zero + x = x" "!!x zero. (-x) + x = zero"
ballarin@37134
   806
  then interpret local_free: lgrp "op +" zero "minus" for zero
ballarin@37134
   807
    by unfold_locales
ballarin@37134
   808
  thm local_free.lone [where ?zero = 0]
ballarin@37134
   809
qed
ballarin@37134
   810
ballarin@38108
   811
lemma True
ballarin@38108
   812
proof
ballarin@38108
   813
  {
ballarin@38108
   814
    fix pand and pnot and por
wenzelm@61489
   815
    assume passoc: "\<And>x y z. pand(pand(x, y), z) \<longleftrightarrow> pand(x, pand(y, z))"
wenzelm@61489
   816
      and pnotnot: "\<And>x. pnot(pnot(x)) \<longleftrightarrow> x"
wenzelm@61489
   817
      and por_def: "\<And>x y. por(x, y) \<longleftrightarrow> pnot(pand(pnot(x), pnot(y)))"
ballarin@38108
   818
    interpret loc: logic_o pand pnot
ballarin@61566
   819
      rewrites por_eq: "\<And>x y. logic_o.lor_o(pand, pnot, x, y) \<longleftrightarrow> por(x, y)"  (* FIXME *)
ballarin@38108
   820
    proof -
ballarin@38108
   821
      show logic_o: "PROP logic_o(pand, pnot)" using passoc pnotnot by unfold_locales
ballarin@38108
   822
      fix x y
wenzelm@61489
   823
      show "logic_o.lor_o(pand, pnot, x, y) \<longleftrightarrow> por(x, y)"
ballarin@38108
   824
        by (unfold logic_o.lor_o_def [OF logic_o]) (rule por_def [symmetric])
ballarin@38108
   825
    qed
ballarin@38109
   826
    print_interps logic_o
wenzelm@61489
   827
    have "\<And>x y. por(x, y) \<longleftrightarrow> pnot(pand(pnot(x), pnot(y)))" by (rule loc.lor_o_def)
ballarin@38108
   828
  }
ballarin@38108
   829
qed
ballarin@38108
   830
ballarin@37134
   831
end