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