src/FOL/ex/LocaleTest.thy
author ballarin
Mon, 01 Feb 2010 21:59:27 +0100
changeset 36089 8078d496582c
parent 33837 a406f447abef
child 36091 055934ed89b0
permissions -rw-r--r--
More mixin tests.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30749
44a16c6956f9 Comments updated.
ballarin
parents: 29513
diff changeset
     1
(*  Title:      FOL/ex/LocaleTest.thy
28873
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
     2
    Author:     Clemens Ballarin, TU Muenchen
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
     3
30749
44a16c6956f9 Comments updated.
ballarin
parents: 29513
diff changeset
     4
Test environment for the locale implementation.
28873
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
     5
*)
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
     6
29357
11956fa598b7 removed locale adaption layer
haftmann
parents: 29251
diff changeset
     7
theory LocaleTest
11956fa598b7 removed locale adaption layer
haftmann
parents: 29251
diff changeset
     8
imports FOL
28873
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
     9
begin
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    10
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    11
typedecl int arities int :: "term"
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    12
consts plus :: "int => int => int" (infixl "+" 60)
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    13
  zero :: int ("0")
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    14
  minus :: "int => int" ("- _")
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    15
28993
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
    16
axioms
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
    17
  int_assoc: "(x + y::int) + z = x + (y + z)"
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
    18
  int_zero: "0 + x = x"
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
    19
  int_minus: "(-x) + x = 0"
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
    20
  int_minus2: "-(-x) = x"
28873
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    21
29206
62dc8762ec00 Preserve idents (expression in sublocale).
ballarin
parents: 29035
diff changeset
    22
section {* Inference of parameter types *}
28873
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    23
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    24
locale param1 = fixes p
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    25
print_locale! param1
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    26
28881
df2525ad10c6 Some regression tests for theorem statements.
ballarin
parents: 28873
diff changeset
    27
locale param2 = fixes p :: 'b
28873
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    28
print_locale! param2
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    29
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    30
(*
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    31
locale param_top = param2 r for r :: "'b :: {}"
28993
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
    32
  Fails, cannot generalise parameter.
28873
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    33
*)
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    34
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    35
locale param3 = fixes p (infix ".." 50)
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    36
print_locale! param3
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    37
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    38
locale param4 = fixes p :: "'a => 'a => 'a" (infix ".." 50)
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    39
print_locale! param4
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    40
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    41
29206
62dc8762ec00 Preserve idents (expression in sublocale).
ballarin
parents: 29035
diff changeset
    42
subsection {* Incremental type constraints *}
28873
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    43
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    44
locale constraint1 =
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    45
  fixes  prod (infixl "**" 65)
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    46
  assumes l_id: "x ** y = x"
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    47
  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    48
print_locale! constraint1
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    49
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    50
locale constraint2 =
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    51
  fixes p and q
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    52
  assumes "p = q"
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    53
print_locale! constraint2
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    54
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    55
29206
62dc8762ec00 Preserve idents (expression in sublocale).
ballarin
parents: 29035
diff changeset
    56
section {* Inheritance *}
28873
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    57
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    58
locale semi =
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    59
  fixes prod (infixl "**" 65)
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    60
  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    61
print_locale! semi thm semi_def
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    62
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    63
locale lgrp = semi +
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    64
  fixes one and inv
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    65
  assumes lone: "one ** x = x"
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    66
    and linv: "inv(x) ** x = one"
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    67
print_locale! lgrp thm lgrp_def lgrp_axioms_def
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    68
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    69
locale add_lgrp = semi "op ++" for sum (infixl "++" 60) +
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    70
  fixes zero and neg
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    71
  assumes lzero: "zero ++ x = x"
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    72
    and lneg: "neg(x) ++ x = zero"
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    73
print_locale! add_lgrp thm add_lgrp_def add_lgrp_axioms_def
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    74
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    75
locale rev_lgrp = semi "%x y. y ++ x" for sum (infixl "++" 60)
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    76
print_locale! rev_lgrp thm rev_lgrp_def
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    77
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    78
locale hom = f: semi f + g: semi g for f and g
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    79
print_locale! hom thm hom_def
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    80
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    81
locale perturbation = semi + d: semi "%x y. delta(x) ** delta(y)" for delta
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    82
print_locale! perturbation thm perturbation_def
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    83
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    84
locale pert_hom = d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    85
print_locale! pert_hom thm pert_hom_def
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    86
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    87
text {* Alternative expression, obtaining nicer names in @{text "semi f"}. *}
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    88
locale pert_hom' = semi f + d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    89
print_locale! pert_hom' thm pert_hom'_def
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    90
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    91
29206
62dc8762ec00 Preserve idents (expression in sublocale).
ballarin
parents: 29035
diff changeset
    92
section {* Syntax declarations *}
28873
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    93
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    94
locale logic =
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    95
  fixes land (infixl "&&" 55)
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    96
    and lnot ("-- _" [60] 60)
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    97
  assumes assoc: "(x && y) && z = x && (y && z)"
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    98
    and notnot: "-- (-- x) = x"
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
    99
begin
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
   100
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
   101
definition lor (infixl "||" 50) where
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
   102
  "x || y = --(-- x && -- y)"
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
   103
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
   104
end
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
   105
print_locale! logic
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
   106
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
   107
locale use_decl = logic + semi "op ||"
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
   108
print_locale! use_decl thm use_decl_def
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
   109
29251
8f84a608883d Temporarily avoid type errors in parse phase.
ballarin
parents: 29249
diff changeset
   110
locale extra_type =
8f84a608883d Temporarily avoid type errors in parse phase.
ballarin
parents: 29249
diff changeset
   111
  fixes a :: 'a
8f84a608883d Temporarily avoid type errors in parse phase.
ballarin
parents: 29249
diff changeset
   112
    and P :: "'a => 'b => o"
8f84a608883d Temporarily avoid type errors in parse phase.
ballarin
parents: 29249
diff changeset
   113
begin
8f84a608883d Temporarily avoid type errors in parse phase.
ballarin
parents: 29249
diff changeset
   114
8f84a608883d Temporarily avoid type errors in parse phase.
ballarin
parents: 29249
diff changeset
   115
definition test :: "'a => o" where
8f84a608883d Temporarily avoid type errors in parse phase.
ballarin
parents: 29249
diff changeset
   116
  "test(x) <-> (ALL b. P(x, b))"
8f84a608883d Temporarily avoid type errors in parse phase.
ballarin
parents: 29249
diff changeset
   117
8f84a608883d Temporarily avoid type errors in parse phase.
ballarin
parents: 29249
diff changeset
   118
end
8f84a608883d Temporarily avoid type errors in parse phase.
ballarin
parents: 29249
diff changeset
   119
8f84a608883d Temporarily avoid type errors in parse phase.
ballarin
parents: 29249
diff changeset
   120
term extra_type.test thm extra_type.test_def
8f84a608883d Temporarily avoid type errors in parse phase.
ballarin
parents: 29249
diff changeset
   121
30729
461ee3e49ad3 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 29513
diff changeset
   122
interpretation var?: extra_type "0" "%x y. x = 0" .
29251
8f84a608883d Temporarily avoid type errors in parse phase.
ballarin
parents: 29249
diff changeset
   123
8f84a608883d Temporarily avoid type errors in parse phase.
ballarin
parents: 29249
diff changeset
   124
thm var.test_def
8f84a608883d Temporarily avoid type errors in parse phase.
ballarin
parents: 29249
diff changeset
   125
28881
df2525ad10c6 Some regression tests for theorem statements.
ballarin
parents: 28873
diff changeset
   126
33460
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   127
text {* Under which circumstances term syntax remains active. *}
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   128
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   129
locale "syntax" =
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   130
  fixes p1 :: "'a => 'b"
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   131
    and p2 :: "'b => o"
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   132
begin
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   133
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   134
definition d1 :: "'a => o" where "d1(x) <-> ~ p2(p1(x))"
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   135
definition d2 :: "'b => o" where "d2(x) <-> ~ p2(x)"
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   136
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   137
thm d1_def d2_def
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   138
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   139
end
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   140
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   141
thm syntax.d1_def syntax.d2_def
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   142
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   143
locale syntax' = "syntax" p1 p2 for p1 :: "'a => 'a" and p2 :: "'a => o"
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   144
begin
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   145
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   146
thm d1_def d2_def  (* should print as "d1(?x) <-> ..." and "d2(?x) <-> ..." *)
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   147
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   148
ML {*
33462
ddcf2004e215 Use PrintMode.setmp to make thread-safe; avoid code clones.
ballarin
parents: 33461
diff changeset
   149
  fun check_syntax ctxt thm expected =
ddcf2004e215 Use PrintMode.setmp to make thread-safe; avoid code clones.
ballarin
parents: 33461
diff changeset
   150
    let
ddcf2004e215 Use PrintMode.setmp to make thread-safe; avoid code clones.
ballarin
parents: 33461
diff changeset
   151
      val obtained = PrintMode.setmp [] (Display.string_of_thm ctxt) thm;
ddcf2004e215 Use PrintMode.setmp to make thread-safe; avoid code clones.
ballarin
parents: 33461
diff changeset
   152
    in
ddcf2004e215 Use PrintMode.setmp to make thread-safe; avoid code clones.
ballarin
parents: 33461
diff changeset
   153
      if obtained <> expected
ddcf2004e215 Use PrintMode.setmp to make thread-safe; avoid code clones.
ballarin
parents: 33461
diff changeset
   154
      then error ("Theorem syntax '" ^ obtained ^ "' obtained, but '" ^ expected ^ "' expected.")
ddcf2004e215 Use PrintMode.setmp to make thread-safe; avoid code clones.
ballarin
parents: 33461
diff changeset
   155
      else ()
ddcf2004e215 Use PrintMode.setmp to make thread-safe; avoid code clones.
ballarin
parents: 33461
diff changeset
   156
    end;
ddcf2004e215 Use PrintMode.setmp to make thread-safe; avoid code clones.
ballarin
parents: 33461
diff changeset
   157
*}
ddcf2004e215 Use PrintMode.setmp to make thread-safe; avoid code clones.
ballarin
parents: 33461
diff changeset
   158
ddcf2004e215 Use PrintMode.setmp to make thread-safe; avoid code clones.
ballarin
parents: 33461
diff changeset
   159
ML {*
ddcf2004e215 Use PrintMode.setmp to make thread-safe; avoid code clones.
ballarin
parents: 33461
diff changeset
   160
  check_syntax @{context} @{thm d1_def} "d1(?x) <-> ~ p2(p1(?x))";
ddcf2004e215 Use PrintMode.setmp to make thread-safe; avoid code clones.
ballarin
parents: 33461
diff changeset
   161
  check_syntax @{context} @{thm d2_def} "d2(?x) <-> ~ p2(?x)";
33460
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   162
*}
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   163
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   164
end
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   165
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   166
locale syntax'' = "syntax" p3 p2 for p3 :: "'a => 'b" and p2 :: "'b => o"
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   167
begin
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   168
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   169
thm d1_def d2_def
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   170
  (* should print as "syntax.d1(p3, p2, ?x) <-> ..." and "d2(?x) <-> ..." *)
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   171
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   172
ML {*
33462
ddcf2004e215 Use PrintMode.setmp to make thread-safe; avoid code clones.
ballarin
parents: 33461
diff changeset
   173
  check_syntax @{context} @{thm d1_def} "syntax.d1(p3, p2, ?x) <-> ~ p2(p3(?x))";
ddcf2004e215 Use PrintMode.setmp to make thread-safe; avoid code clones.
ballarin
parents: 33461
diff changeset
   174
  check_syntax @{context} @{thm d2_def} "d2(?x) <-> ~ p2(?x)";
33460
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   175
*}
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   176
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   177
end
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   178
6c273b0e0e26 Relax on type agreement with original context when applying term syntax.
ballarin
parents: 32802
diff changeset
   179
29206
62dc8762ec00 Preserve idents (expression in sublocale).
ballarin
parents: 29035
diff changeset
   180
section {* Foundational versions of theorems *}
29028
b5dad96c755a When adding locales, delay notes until local theory is built.
ballarin
parents: 29022
diff changeset
   181
b5dad96c755a When adding locales, delay notes until local theory is built.
ballarin
parents: 29022
diff changeset
   182
thm logic.assoc
b5dad96c755a When adding locales, delay notes until local theory is built.
ballarin
parents: 29022
diff changeset
   183
thm logic.lor_def
b5dad96c755a When adding locales, delay notes until local theory is built.
ballarin
parents: 29022
diff changeset
   184
b5dad96c755a When adding locales, delay notes until local theory is built.
ballarin
parents: 29022
diff changeset
   185
29206
62dc8762ec00 Preserve idents (expression in sublocale).
ballarin
parents: 29035
diff changeset
   186
section {* Defines *}
29019
8e7d6f959bd7 Explicitly close up defines.
ballarin
parents: 29018
diff changeset
   187
8e7d6f959bd7 Explicitly close up defines.
ballarin
parents: 29018
diff changeset
   188
locale logic_def =
8e7d6f959bd7 Explicitly close up defines.
ballarin
parents: 29018
diff changeset
   189
  fixes land (infixl "&&" 55)
8e7d6f959bd7 Explicitly close up defines.
ballarin
parents: 29018
diff changeset
   190
    and lor (infixl "||" 50)
8e7d6f959bd7 Explicitly close up defines.
ballarin
parents: 29018
diff changeset
   191
    and lnot ("-- _" [60] 60)
8e7d6f959bd7 Explicitly close up defines.
ballarin
parents: 29018
diff changeset
   192
  assumes assoc: "(x && y) && z = x && (y && z)"
8e7d6f959bd7 Explicitly close up defines.
ballarin
parents: 29018
diff changeset
   193
    and notnot: "-- (-- x) = x"
29022
54d3a31ca0f6 Default names for definitions.
ballarin
parents: 29021
diff changeset
   194
  defines "x || y == --(-- x && -- y)"
29021
ce100fbc3c8e Proper shape of assumptions generated from Defines elements.
ballarin
parents: 29019
diff changeset
   195
begin
29019
8e7d6f959bd7 Explicitly close up defines.
ballarin
parents: 29018
diff changeset
   196
29031
e74341997a48 Pass on defines in inheritance; reject illicit defines created by instantiation.
ballarin
parents: 29028
diff changeset
   197
thm lor_def
e74341997a48 Pass on defines in inheritance; reject illicit defines created by instantiation.
ballarin
parents: 29028
diff changeset
   198
29021
ce100fbc3c8e Proper shape of assumptions generated from Defines elements.
ballarin
parents: 29019
diff changeset
   199
lemma "x || y = --(-- x && --y)"
ce100fbc3c8e Proper shape of assumptions generated from Defines elements.
ballarin
parents: 29019
diff changeset
   200
  by (unfold lor_def) (rule refl)
ce100fbc3c8e Proper shape of assumptions generated from Defines elements.
ballarin
parents: 29019
diff changeset
   201
ce100fbc3c8e Proper shape of assumptions generated from Defines elements.
ballarin
parents: 29019
diff changeset
   202
end
ce100fbc3c8e Proper shape of assumptions generated from Defines elements.
ballarin
parents: 29019
diff changeset
   203
29031
e74341997a48 Pass on defines in inheritance; reject illicit defines created by instantiation.
ballarin
parents: 29028
diff changeset
   204
(* Inheritance of defines *)
e74341997a48 Pass on defines in inheritance; reject illicit defines created by instantiation.
ballarin
parents: 29028
diff changeset
   205
e74341997a48 Pass on defines in inheritance; reject illicit defines created by instantiation.
ballarin
parents: 29028
diff changeset
   206
locale logic_def2 = logic_def
e74341997a48 Pass on defines in inheritance; reject illicit defines created by instantiation.
ballarin
parents: 29028
diff changeset
   207
begin
e74341997a48 Pass on defines in inheritance; reject illicit defines created by instantiation.
ballarin
parents: 29028
diff changeset
   208
e74341997a48 Pass on defines in inheritance; reject illicit defines created by instantiation.
ballarin
parents: 29028
diff changeset
   209
lemma "x || y = --(-- x && --y)"
e74341997a48 Pass on defines in inheritance; reject illicit defines created by instantiation.
ballarin
parents: 29028
diff changeset
   210
  by (unfold lor_def) (rule refl)
e74341997a48 Pass on defines in inheritance; reject illicit defines created by instantiation.
ballarin
parents: 29028
diff changeset
   211
e74341997a48 Pass on defines in inheritance; reject illicit defines created by instantiation.
ballarin
parents: 29028
diff changeset
   212
end
29019
8e7d6f959bd7 Explicitly close up defines.
ballarin
parents: 29018
diff changeset
   213
29035
b0a0843dfd99 Satisfy a_axioms.
ballarin
parents: 29031
diff changeset
   214
29206
62dc8762ec00 Preserve idents (expression in sublocale).
ballarin
parents: 29035
diff changeset
   215
section {* Notes *}
29035
b0a0843dfd99 Satisfy a_axioms.
ballarin
parents: 29031
diff changeset
   216
b0a0843dfd99 Satisfy a_axioms.
ballarin
parents: 29031
diff changeset
   217
(* A somewhat arcane homomorphism example *)
b0a0843dfd99 Satisfy a_axioms.
ballarin
parents: 29031
diff changeset
   218
b0a0843dfd99 Satisfy a_axioms.
ballarin
parents: 29031
diff changeset
   219
definition semi_hom where
b0a0843dfd99 Satisfy a_axioms.
ballarin
parents: 29031
diff changeset
   220
  "semi_hom(prod, sum, h) <-> (ALL x y. h(prod(x, y)) = sum(h(x), h(y)))"
b0a0843dfd99 Satisfy a_axioms.
ballarin
parents: 29031
diff changeset
   221
b0a0843dfd99 Satisfy a_axioms.
ballarin
parents: 29031
diff changeset
   222
lemma semi_hom_mult:
b0a0843dfd99 Satisfy a_axioms.
ballarin
parents: 29031
diff changeset
   223
  "semi_hom(prod, sum, h) ==> h(prod(x, y)) = sum(h(x), h(y))"
b0a0843dfd99 Satisfy a_axioms.
ballarin
parents: 29031
diff changeset
   224
  by (simp add: semi_hom_def)
b0a0843dfd99 Satisfy a_axioms.
ballarin
parents: 29031
diff changeset
   225
b0a0843dfd99 Satisfy a_axioms.
ballarin
parents: 29031
diff changeset
   226
locale semi_hom_loc = prod: semi prod + sum: semi sum
b0a0843dfd99 Satisfy a_axioms.
ballarin
parents: 29031
diff changeset
   227
  for prod and sum and h +
b0a0843dfd99 Satisfy a_axioms.
ballarin
parents: 29031
diff changeset
   228
  assumes semi_homh: "semi_hom(prod, sum, h)"
b0a0843dfd99 Satisfy a_axioms.
ballarin
parents: 29031
diff changeset
   229
  notes semi_hom_mult = semi_hom_mult [OF semi_homh]
b0a0843dfd99 Satisfy a_axioms.
ballarin
parents: 29031
diff changeset
   230
29219
fa3fb943a091 Attributes not applied in foundational version of fact.
ballarin
parents: 29217
diff changeset
   231
thm semi_hom_loc.semi_hom_mult
fa3fb943a091 Attributes not applied in foundational version of fact.
ballarin
parents: 29217
diff changeset
   232
(* unspecified, attribute not applied in backgroud theory !!! *)
fa3fb943a091 Attributes not applied in foundational version of fact.
ballarin
parents: 29217
diff changeset
   233
29035
b0a0843dfd99 Satisfy a_axioms.
ballarin
parents: 29031
diff changeset
   234
lemma (in semi_hom_loc) "h(prod(x, y)) = sum(h(x), h(y))"
b0a0843dfd99 Satisfy a_axioms.
ballarin
parents: 29031
diff changeset
   235
  by (rule semi_hom_mult)
b0a0843dfd99 Satisfy a_axioms.
ballarin
parents: 29031
diff changeset
   236
29217
a1c992fb3184 Finer-grained activation so that facts from earlier elements are available.
ballarin
parents: 29214
diff changeset
   237
(* Referring to facts from within a context specification *)
a1c992fb3184 Finer-grained activation so that facts from earlier elements are available.
ballarin
parents: 29214
diff changeset
   238
a1c992fb3184 Finer-grained activation so that facts from earlier elements are available.
ballarin
parents: 29214
diff changeset
   239
lemma
a1c992fb3184 Finer-grained activation so that facts from earlier elements are available.
ballarin
parents: 29214
diff changeset
   240
  assumes x: "P <-> P"
a1c992fb3184 Finer-grained activation so that facts from earlier elements are available.
ballarin
parents: 29214
diff changeset
   241
  notes y = x
a1c992fb3184 Finer-grained activation so that facts from earlier elements are available.
ballarin
parents: 29214
diff changeset
   242
  shows True ..
a1c992fb3184 Finer-grained activation so that facts from earlier elements are available.
ballarin
parents: 29214
diff changeset
   243
29035
b0a0843dfd99 Satisfy a_axioms.
ballarin
parents: 29031
diff changeset
   244
29206
62dc8762ec00 Preserve idents (expression in sublocale).
ballarin
parents: 29035
diff changeset
   245
section {* Theorem statements *}
28881
df2525ad10c6 Some regression tests for theorem statements.
ballarin
parents: 28873
diff changeset
   246
28873
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
   247
lemma (in lgrp) lcancel:
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
   248
  "x ** y = x ** z <-> y = z"
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
   249
proof
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
   250
  assume "x ** y = x ** z"
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
   251
  then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
   252
  then show "y = z" by (simp add: lone linv)
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
   253
qed simp
28881
df2525ad10c6 Some regression tests for theorem statements.
ballarin
parents: 28873
diff changeset
   254
print_locale! lgrp
df2525ad10c6 Some regression tests for theorem statements.
ballarin
parents: 28873
diff changeset
   255
28873
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
   256
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
   257
locale rgrp = semi +
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
   258
  fixes one and inv
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
   259
  assumes rone: "x ** one = x"
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
   260
    and rinv: "x ** inv(x) = one"
28881
df2525ad10c6 Some regression tests for theorem statements.
ballarin
parents: 28873
diff changeset
   261
begin
28873
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
   262
28881
df2525ad10c6 Some regression tests for theorem statements.
ballarin
parents: 28873
diff changeset
   263
lemma rcancel:
28873
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
   264
  "y ** x = z ** x <-> y = z"
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
   265
proof
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
   266
  assume "y ** x = z ** x"
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
   267
  then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
   268
    by (simp add: assoc [symmetric])
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
   269
  then show "y = z" by (simp add: rone rinv)
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
   270
qed simp
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
   271
2058a6b0eb20 Regression tests for new locale implementation.
ballarin
parents:
diff changeset
   272
end
28881
df2525ad10c6 Some regression tests for theorem statements.
ballarin
parents: 28873
diff changeset
   273
print_locale! rgrp
df2525ad10c6 Some regression tests for theorem statements.
ballarin
parents: 28873
diff changeset
   274
28886
9cb1297b6f13 Test for term patterns added.
ballarin
parents: 28881
diff changeset
   275
29206
62dc8762ec00 Preserve idents (expression in sublocale).
ballarin
parents: 29035
diff changeset
   276
subsection {* Patterns *}
28886
9cb1297b6f13 Test for term patterns added.
ballarin
parents: 28881
diff changeset
   277
9cb1297b6f13 Test for term patterns added.
ballarin
parents: 28881
diff changeset
   278
lemma (in rgrp)
9cb1297b6f13 Test for term patterns added.
ballarin
parents: 28881
diff changeset
   279
  assumes "y ** x = z ** x" (is ?a)
9cb1297b6f13 Test for term patterns added.
ballarin
parents: 28881
diff changeset
   280
  shows "y = z" (is ?t)
9cb1297b6f13 Test for term patterns added.
ballarin
parents: 28881
diff changeset
   281
proof -
9cb1297b6f13 Test for term patterns added.
ballarin
parents: 28881
diff changeset
   282
  txt {* Weird proof involving patterns from context element and conclusion. *}
9cb1297b6f13 Test for term patterns added.
ballarin
parents: 28881
diff changeset
   283
  {
9cb1297b6f13 Test for term patterns added.
ballarin
parents: 28881
diff changeset
   284
    assume ?a
9cb1297b6f13 Test for term patterns added.
ballarin
parents: 28881
diff changeset
   285
    then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
9cb1297b6f13 Test for term patterns added.
ballarin
parents: 28881
diff changeset
   286
      by (simp add: assoc [symmetric])
9cb1297b6f13 Test for term patterns added.
ballarin
parents: 28881
diff changeset
   287
    then have ?t by (simp add: rone rinv)
9cb1297b6f13 Test for term patterns added.
ballarin
parents: 28881
diff changeset
   288
  }
9cb1297b6f13 Test for term patterns added.
ballarin
parents: 28881
diff changeset
   289
  note x = this
9cb1297b6f13 Test for term patterns added.
ballarin
parents: 28881
diff changeset
   290
  show ?t by (rule x [OF `?a`])
9cb1297b6f13 Test for term patterns added.
ballarin
parents: 28881
diff changeset
   291
qed
9cb1297b6f13 Test for term patterns added.
ballarin
parents: 28881
diff changeset
   292
28896
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   293
29206
62dc8762ec00 Preserve idents (expression in sublocale).
ballarin
parents: 29035
diff changeset
   294
section {* Interpretation between locales: sublocales *}
28896
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   295
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   296
sublocale lgrp < right: rgrp
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   297
print_facts
28927
7e631979922f Methods intro_locales and unfold_locales apply to both old and new locales.
ballarin
parents: 28903
diff changeset
   298
proof unfold_locales
28896
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   299
  {
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   300
    fix x
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   301
    have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   302
    then show "x ** one = x" by (simp add: assoc lcancel)
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   303
  }
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   304
  note rone = this
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   305
  {
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   306
    fix x
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   307
    have "inv(x) ** x ** inv(x) = inv(x) ** one"
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   308
      by (simp add: linv lone rone)
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   309
    then show "x ** inv(x) = one" by (simp add: assoc lcancel)
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   310
  }
28903
b3fc3a62247a Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents: 28899
diff changeset
   311
qed
28896
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   312
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   313
(* effect on printed locale *)
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   314
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   315
print_locale! lgrp
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   316
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   317
(* use of derived theorem *)
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   318
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   319
lemma (in lgrp)
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   320
  "y ** x = z ** x <-> y = z"
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   321
  apply (rule rcancel)
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   322
  done
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   323
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   324
(* circular interpretation *)
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   325
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   326
sublocale rgrp < left: lgrp
28927
7e631979922f Methods intro_locales and unfold_locales apply to both old and new locales.
ballarin
parents: 28903
diff changeset
   327
proof unfold_locales
28903
b3fc3a62247a Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents: 28899
diff changeset
   328
  {
b3fc3a62247a Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents: 28899
diff changeset
   329
    fix x
b3fc3a62247a Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents: 28899
diff changeset
   330
    have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone)
b3fc3a62247a Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents: 28899
diff changeset
   331
    then show "one ** x = x" by (simp add: assoc [symmetric] rcancel)
b3fc3a62247a Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents: 28899
diff changeset
   332
  }
b3fc3a62247a Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents: 28899
diff changeset
   333
  note lone = this
b3fc3a62247a Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents: 28899
diff changeset
   334
  {
b3fc3a62247a Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents: 28899
diff changeset
   335
    fix x
b3fc3a62247a Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents: 28899
diff changeset
   336
    have "inv(x) ** (x ** inv(x)) = one ** inv(x)"
b3fc3a62247a Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents: 28899
diff changeset
   337
      by (simp add: rinv lone rone)
b3fc3a62247a Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents: 28899
diff changeset
   338
    then show "inv(x) ** x = one" by (simp add: assoc [symmetric] rcancel)
b3fc3a62247a Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents: 28899
diff changeset
   339
  }
b3fc3a62247a Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents: 28899
diff changeset
   340
qed
28896
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   341
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   342
(* effect on printed locale *)
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   343
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   344
print_locale! rgrp
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   345
print_locale! lgrp
f30016592375 Tests for sublocale command.
ballarin
parents: 28886
diff changeset
   346
28898
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   347
28899
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   348
(* Duality *)
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   349
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   350
locale order =
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   351
  fixes less :: "'a => 'a => o" (infix "<<" 50)
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   352
  assumes refl: "x << x"
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   353
    and trans: "[| x << y; y << z |] ==> x << z"
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   354
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   355
sublocale order < dual: order "%x y. y << x"
28927
7e631979922f Methods intro_locales and unfold_locales apply to both old and new locales.
ballarin
parents: 28903
diff changeset
   356
  apply unfold_locales apply (rule refl) apply (blast intro: trans)
28899
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   357
  done
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   358
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   359
print_locale! order  (* Only two instances of order. *)
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   360
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   361
locale order' =
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   362
  fixes less :: "'a => 'a => o" (infix "<<" 50)
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   363
  assumes refl: "x << x"
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   364
    and trans: "[| x << y; y << z |] ==> x << z"
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   365
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   366
locale order_with_def = order'
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   367
begin
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   368
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   369
definition greater :: "'a => 'a => o" (infix ">>" 50) where
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   370
  "x >> y <-> y << x"
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   371
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   372
end
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   373
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   374
sublocale order_with_def < dual: order' "op >>"
28927
7e631979922f Methods intro_locales and unfold_locales apply to both old and new locales.
ballarin
parents: 28903
diff changeset
   375
  apply unfold_locales
28899
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   376
  unfolding greater_def
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   377
  apply (rule refl) apply (blast intro: trans)
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   378
  done
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   379
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   380
print_locale! order_with_def
29210
4025459e3f83 Interpretation in theories: first version with equations.
ballarin
parents: 29206
diff changeset
   381
(* Note that decls come after theorems that make use of them. *)
28899
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   382
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   383
28898
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   384
(* locale with many parameters ---
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   385
   interpretations generate alternating group A5 *)
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   386
28899
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   387
28898
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   388
locale A5 =
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   389
  fixes A and B and C and D and E
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   390
  assumes eq: "A <-> B <-> C <-> D <-> E"
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   391
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   392
sublocale A5 < 1: A5 _ _ D E C
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   393
print_facts
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   394
  using eq apply (blast intro: A5.intro) done
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   395
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   396
sublocale A5 < 2: A5 C _ E _ A
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   397
print_facts
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   398
  using eq apply (blast intro: A5.intro) done
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   399
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   400
sublocale A5 < 3: A5 B C A _ _
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   401
print_facts
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   402
  using eq apply (blast intro: A5.intro) done
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   403
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   404
(* Any even permutation of parameters is subsumed by the above. *)
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   405
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   406
print_locale! A5
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   407
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   408
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   409
(* Free arguments of instance *)
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   410
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   411
locale trivial =
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   412
  fixes P and Q :: o
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   413
  assumes Q: "P <-> P <-> Q"
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   414
begin
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   415
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   416
lemma Q_triv: "Q" using Q by fast
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   417
28881
df2525ad10c6 Some regression tests for theorem statements.
ballarin
parents: 28873
diff changeset
   418
end
28898
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   419
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   420
sublocale trivial < x: trivial x _
28927
7e631979922f Methods intro_locales and unfold_locales apply to both old and new locales.
ballarin
parents: 28903
diff changeset
   421
  apply unfold_locales using Q by fast
28898
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   422
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   423
print_locale! trivial
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   424
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   425
context trivial begin thm x.Q [where ?x = True] end
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   426
28899
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   427
sublocale trivial < y: trivial Q Q
28927
7e631979922f Methods intro_locales and unfold_locales apply to both old and new locales.
ballarin
parents: 28903
diff changeset
   428
  by unfold_locales
28903
b3fc3a62247a Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents: 28899
diff changeset
   429
  (* Succeeds since previous interpretation is more general. *)
28899
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   430
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   431
print_locale! trivial  (* No instance for y created (subsumed). *)
7bf5d7f154b8 Perform higher-order pattern matching during round-up.
ballarin
parents: 28898
diff changeset
   432
28993
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
   433
29206
62dc8762ec00 Preserve idents (expression in sublocale).
ballarin
parents: 29035
diff changeset
   434
subsection {* Sublocale, then interpretation in theory *}
28993
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
   435
30729
461ee3e49ad3 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 29513
diff changeset
   436
interpretation int?: lgrp "op +" "0" "minus"
28993
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
   437
proof unfold_locales
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
   438
qed (rule int_assoc int_zero int_minus)+
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
   439
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
   440
thm int.assoc int.semi_axioms
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
   441
30729
461ee3e49ad3 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 29513
diff changeset
   442
interpretation int2?: semi "op +"
28993
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
   443
  by unfold_locales  (* subsumed, thm int2.assoc not generated *)
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
   444
32802
b52aa3bc7362 Stricter test: raise error if registration generates duplicate theorem.
ballarin
parents: 30752
diff changeset
   445
ML {* (PureThy.get_thms @{theory} "int2.assoc";
b52aa3bc7362 Stricter test: raise error if registration generates duplicate theorem.
ballarin
parents: 30752
diff changeset
   446
    error "thm int2.assoc was generated")
b52aa3bc7362 Stricter test: raise error if registration generates duplicate theorem.
ballarin
parents: 30752
diff changeset
   447
  handle ERROR "Unknown fact \"int2.assoc\"" => ([]:thm list); *}
b52aa3bc7362 Stricter test: raise error if registration generates duplicate theorem.
ballarin
parents: 30752
diff changeset
   448
28993
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
   449
thm int.lone int.right.rone
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
   450
  (* the latter comes through the sublocale relation *)
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
   451
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
   452
29206
62dc8762ec00 Preserve idents (expression in sublocale).
ballarin
parents: 29035
diff changeset
   453
subsection {* Interpretation in theory, then sublocale *}
28993
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
   454
33617
bfee47887ca3 Enables tests for locale functionality that is now available.
ballarin
parents: 33462
diff changeset
   455
interpretation fol: logic "op +" "minus"
28993
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
   456
  by unfold_locales (rule int_assoc int_minus2)+
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
   457
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
   458
locale logic2 =
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
   459
  fixes land (infixl "&&" 55)
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
   460
    and lnot ("-- _" [60] 60)
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
   461
  assumes assoc: "(x && y) && z = x && (y && z)"
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
   462
    and notnot: "-- (-- x) = x"
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
   463
begin
29206
62dc8762ec00 Preserve idents (expression in sublocale).
ballarin
parents: 29035
diff changeset
   464
28993
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
   465
definition lor (infixl "||" 50) where
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
   466
  "x || y = --(-- x && -- y)"
29206
62dc8762ec00 Preserve idents (expression in sublocale).
ballarin
parents: 29035
diff changeset
   467
28898
530c7d28a962 Proper treatment of expressions with free arguments.
ballarin
parents: 28896
diff changeset
   468
end
28993
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
   469
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
   470
sublocale logic < two: logic2
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
   471
  by unfold_locales (rule assoc notnot)+
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
   472
33617
bfee47887ca3 Enables tests for locale functionality that is now available.
ballarin
parents: 33462
diff changeset
   473
thm fol.two.assoc
28993
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
   474
29018
17538bdef546 Interpretation in proof contexts.
ballarin
parents: 28993
diff changeset
   475
29206
62dc8762ec00 Preserve idents (expression in sublocale).
ballarin
parents: 29035
diff changeset
   476
subsection {* Declarations and sublocale *}
62dc8762ec00 Preserve idents (expression in sublocale).
ballarin
parents: 29035
diff changeset
   477
62dc8762ec00 Preserve idents (expression in sublocale).
ballarin
parents: 29035
diff changeset
   478
locale logic_a = logic
62dc8762ec00 Preserve idents (expression in sublocale).
ballarin
parents: 29035
diff changeset
   479
locale logic_b = logic
62dc8762ec00 Preserve idents (expression in sublocale).
ballarin
parents: 29035
diff changeset
   480
62dc8762ec00 Preserve idents (expression in sublocale).
ballarin
parents: 29035
diff changeset
   481
sublocale logic_a < logic_b
62dc8762ec00 Preserve idents (expression in sublocale).
ballarin
parents: 29035
diff changeset
   482
  by unfold_locales
62dc8762ec00 Preserve idents (expression in sublocale).
ballarin
parents: 29035
diff changeset
   483
62dc8762ec00 Preserve idents (expression in sublocale).
ballarin
parents: 29035
diff changeset
   484
29210
4025459e3f83 Interpretation in theories: first version with equations.
ballarin
parents: 29206
diff changeset
   485
subsection {* Equations *}
4025459e3f83 Interpretation in theories: first version with equations.
ballarin
parents: 29206
diff changeset
   486
4025459e3f83 Interpretation in theories: first version with equations.
ballarin
parents: 29206
diff changeset
   487
locale logic_o =
4025459e3f83 Interpretation in theories: first version with equations.
ballarin
parents: 29206
diff changeset
   488
  fixes land (infixl "&&" 55)
4025459e3f83 Interpretation in theories: first version with equations.
ballarin
parents: 29206
diff changeset
   489
    and lnot ("-- _" [60] 60)
4025459e3f83 Interpretation in theories: first version with equations.
ballarin
parents: 29206
diff changeset
   490
  assumes assoc_o: "(x && y) && z <-> x && (y && z)"
4025459e3f83 Interpretation in theories: first version with equations.
ballarin
parents: 29206
diff changeset
   491
    and notnot_o: "-- (-- x) <-> x"
4025459e3f83 Interpretation in theories: first version with equations.
ballarin
parents: 29206
diff changeset
   492
begin
4025459e3f83 Interpretation in theories: first version with equations.
ballarin
parents: 29206
diff changeset
   493
4025459e3f83 Interpretation in theories: first version with equations.
ballarin
parents: 29206
diff changeset
   494
definition lor_o (infixl "||" 50) where
4025459e3f83 Interpretation in theories: first version with equations.
ballarin
parents: 29206
diff changeset
   495
  "x || y <-> --(-- x && -- y)"
4025459e3f83 Interpretation in theories: first version with equations.
ballarin
parents: 29206
diff changeset
   496
4025459e3f83 Interpretation in theories: first version with equations.
ballarin
parents: 29206
diff changeset
   497
end
4025459e3f83 Interpretation in theories: first version with equations.
ballarin
parents: 29206
diff changeset
   498
30729
461ee3e49ad3 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 29513
diff changeset
   499
interpretation x: logic_o "op &" "Not"
29211
ab99da3854af Equations in interpretation as goals.
ballarin
parents: 29210
diff changeset
   500
  where bool_logic_o: "logic_o.lor_o(op &, Not, x, y) <-> x | y"
ab99da3854af Equations in interpretation as goals.
ballarin
parents: 29210
diff changeset
   501
proof -
ab99da3854af Equations in interpretation as goals.
ballarin
parents: 29210
diff changeset
   502
  show bool_logic_o: "PROP logic_o(op &, Not)" by unfold_locales fast+
ab99da3854af Equations in interpretation as goals.
ballarin
parents: 29210
diff changeset
   503
  show "logic_o.lor_o(op &, Not, x, y) <-> x | y"
ab99da3854af Equations in interpretation as goals.
ballarin
parents: 29210
diff changeset
   504
    by (unfold logic_o.lor_o_def [OF bool_logic_o]) fast
ab99da3854af Equations in interpretation as goals.
ballarin
parents: 29210
diff changeset
   505
qed
29210
4025459e3f83 Interpretation in theories: first version with equations.
ballarin
parents: 29206
diff changeset
   506
29211
ab99da3854af Equations in interpretation as goals.
ballarin
parents: 29210
diff changeset
   507
thm x.lor_o_def bool_logic_o
29210
4025459e3f83 Interpretation in theories: first version with equations.
ballarin
parents: 29206
diff changeset
   508
29214
76c7fc5ba849 Strict prefixes in locales expressions.
ballarin
parents: 29213
diff changeset
   509
lemma lor_triv: "z <-> z" ..
76c7fc5ba849 Strict prefixes in locales expressions.
ballarin
parents: 29213
diff changeset
   510
29210
4025459e3f83 Interpretation in theories: first version with equations.
ballarin
parents: 29206
diff changeset
   511
lemma (in logic_o) lor_triv: "x || y <-> x || y" by fast
4025459e3f83 Interpretation in theories: first version with equations.
ballarin
parents: 29206
diff changeset
   512
29214
76c7fc5ba849 Strict prefixes in locales expressions.
ballarin
parents: 29213
diff changeset
   513
thm lor_triv [where z = True] (* Check strict prefix. *)
76c7fc5ba849 Strict prefixes in locales expressions.
ballarin
parents: 29213
diff changeset
   514
  x.lor_triv
29210
4025459e3f83 Interpretation in theories: first version with equations.
ballarin
parents: 29206
diff changeset
   515
4025459e3f83 Interpretation in theories: first version with equations.
ballarin
parents: 29206
diff changeset
   516
33835
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   517
subsection {* Inheritance of mixins *}
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   518
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   519
locale reflexive =
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   520
  fixes le :: "'a => 'a => o" (infix "\<sqsubseteq>" 50)
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   521
  assumes refl: "x \<sqsubseteq> x"
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   522
begin
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   523
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   524
definition less (infix "\<sqsubset>" 50) where "x \<sqsubset> y <-> x \<sqsubseteq> y & x ~= y"
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   525
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   526
end
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   527
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   528
consts
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   529
  gle :: "'a => 'a => o" gless :: "'a => 'a => o"
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   530
  gle' :: "'a => 'a => o" gless' :: "'a => 'a => o"
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   531
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   532
axioms
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   533
  grefl: "gle(x, x)" gless_def: "gless(x, y) <-> gle(x, y) & x ~= y"
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   534
  grefl': "gle'(x, x)" gless'_def: "gless'(x, y) <-> gle'(x, y) & x ~= y"
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   535
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   536
text {* Mixin not applied to locales further up the hierachy. *}
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   537
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   538
locale mixin = reflexive
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   539
begin
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   540
lemmas less_thm = less_def
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   541
end
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   542
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   543
interpretation le: mixin gle where "reflexive.less(gle, x, y) <-> gless(x, y)"
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   544
proof -
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   545
  show "mixin(gle)" by unfold_locales (rule grefl)
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   546
  note reflexive = this[unfolded mixin_def]
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   547
  show "reflexive.less(gle, x, y) <-> gless(x, y)"
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   548
    by (simp add: reflexive.less_def[OF reflexive] gless_def)
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   549
qed
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   550
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   551
thm le.less_def  (* mixin not applied *)
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   552
lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y" by (rule le.less_def)
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   553
thm le.less_thm  (* mixin applied *)
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   554
lemma "gless(x, y) <-> gle(x, y) & x ~= y" by (rule le.less_thm)
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   555
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   556
lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   557
  by (rule le.less_def)
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   558
lemma "gless(x, y) <-> gle(x, y) & x ~= y"
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   559
  by (rule le.less_thm)
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   560
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   561
text {* Mixin propagated along the locale hierarchy *}
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   562
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   563
locale mixin2 = mixin
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   564
begin
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   565
lemmas less_thm2 = less_def
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   566
end
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   567
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   568
interpretation le: mixin2 gle
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   569
  by unfold_locales
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   570
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   571
thm le.less_thm2  (* mixin applied *)
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   572
lemma "gless(x, y) <-> gle(x, y) & x ~= y"
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   573
  by (rule le.less_thm2)
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   574
36089
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   575
text {* Mixin does not leak to a side branch. *}
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   576
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   577
locale mixin3 = reflexive
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   578
begin
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   579
lemmas less_thm3 = less_def
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   580
end
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   581
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   582
interpretation le: mixin3 gle
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   583
  by unfold_locales
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   584
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   585
thm le.less_thm3  (* mixin not applied *)
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   586
lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y" by (rule le.less_thm3)
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   587
33835
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   588
text {* Mixin only available in original context *}
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   589
36089
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   590
locale mixin4_base = reflexive
33835
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   591
36089
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   592
locale mixin4_mixin = mixin4_base
33835
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   593
36089
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   594
interpretation le: mixin4_mixin gle
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   595
  where "reflexive.less(gle, x, y) <-> gless(x, y)"
33835
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   596
proof -
36089
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   597
  show "mixin4_mixin(gle)" by unfold_locales (rule grefl)
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   598
  note reflexive = this[unfolded mixin4_mixin_def mixin4_base_def mixin_def]
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   599
  show "reflexive.less(gle, x, y) <-> gless(x, y)"
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   600
    by (simp add: reflexive.less_def[OF reflexive] gless_def)
33835
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   601
qed
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   602
36089
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   603
locale mixin4_copy = mixin4_base
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   604
begin
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   605
lemmas less_thm4 = less_def
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   606
end
33835
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   607
36089
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   608
locale mixin4_combined = le1: mixin4_mixin le' + le2: mixin4_copy le for le' le
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   609
begin
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   610
lemmas less_thm4' = less_def
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   611
end
33835
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   612
36089
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   613
interpretation le4: mixin4_combined gle' gle
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   614
  by unfold_locales (rule grefl')
33835
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   615
36089
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   616
thm le4.less_thm4' (* mixin not applied *)
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   617
lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
8078d496582c More mixin tests.
ballarin
parents: 33837
diff changeset
   618
  by (rule le4.less_thm4')
33835
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   619
d6134fb5a49f More tests for locale interpretation.
ballarin
parents: 33617
diff changeset
   620
29210
4025459e3f83 Interpretation in theories: first version with equations.
ballarin
parents: 29206
diff changeset
   621
subsection {* Interpretation in proofs *}
29018
17538bdef546 Interpretation in proof contexts.
ballarin
parents: 28993
diff changeset
   622
17538bdef546 Interpretation in proof contexts.
ballarin
parents: 28993
diff changeset
   623
lemma True
17538bdef546 Interpretation in proof contexts.
ballarin
parents: 28993
diff changeset
   624
proof
17538bdef546 Interpretation in proof contexts.
ballarin
parents: 28993
diff changeset
   625
  interpret "local": lgrp "op +" "0" "minus"
17538bdef546 Interpretation in proof contexts.
ballarin
parents: 28993
diff changeset
   626
    by unfold_locales  (* subsumed *)
17538bdef546 Interpretation in proof contexts.
ballarin
parents: 28993
diff changeset
   627
  {
17538bdef546 Interpretation in proof contexts.
ballarin
parents: 28993
diff changeset
   628
    fix zero :: int
17538bdef546 Interpretation in proof contexts.
ballarin
parents: 28993
diff changeset
   629
    assume "!!x. zero + x = x" "!!x. (-x) + x = zero"
17538bdef546 Interpretation in proof contexts.
ballarin
parents: 28993
diff changeset
   630
    then interpret local_fixed: lgrp "op +" zero "minus"
17538bdef546 Interpretation in proof contexts.
ballarin
parents: 28993
diff changeset
   631
      by unfold_locales
17538bdef546 Interpretation in proof contexts.
ballarin
parents: 28993
diff changeset
   632
    thm local_fixed.lone
17538bdef546 Interpretation in proof contexts.
ballarin
parents: 28993
diff changeset
   633
  }
17538bdef546 Interpretation in proof contexts.
ballarin
parents: 28993
diff changeset
   634
  assume "!!x zero. zero + x = x" "!!x zero. (-x) + x = zero"
17538bdef546 Interpretation in proof contexts.
ballarin
parents: 28993
diff changeset
   635
  then interpret local_free: lgrp "op +" zero "minus" for zero
17538bdef546 Interpretation in proof contexts.
ballarin
parents: 28993
diff changeset
   636
    by unfold_locales
17538bdef546 Interpretation in proof contexts.
ballarin
parents: 28993
diff changeset
   637
  thm local_free.lone [where ?zero = 0]
17538bdef546 Interpretation in proof contexts.
ballarin
parents: 28993
diff changeset
   638
qed
17538bdef546 Interpretation in proof contexts.
ballarin
parents: 28993
diff changeset
   639
28993
829e684b02ef Interpretation in theories including interaction with subclass relation.
ballarin
parents: 28936
diff changeset
   640
end