src/FOL/ex/LocaleTest.thy
author ballarin
Wed, 17 Aug 2005 17:04:15 +0200
changeset 17096 8327b71282ce
parent 17033 f4c1ce91aa3c
child 17139 165c97f9bb63
permissions -rw-r--r--
Improved generation of witnesses in interpretation.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
     1
(*  Title:      FOL/ex/LocaleTest.thy
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
     2
    ID:         $Id$
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
     3
    Author:     Clemens Ballarin
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
     4
    Copyright (c) 2005 by Clemens Ballarin
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
     5
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
     6
Collection of regression tests for locales.
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
     7
*)
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
     8
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 15837
diff changeset
     9
header {* Test of Locale Interpretation *}
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    10
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 15837
diff changeset
    11
theory LocaleTest
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 15837
diff changeset
    12
imports FOL
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 15837
diff changeset
    13
begin
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    14
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
    15
ML {* set quick_and_dirty *}    (* allow for thm command in batch mode *)
16168
adb83939177f Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16102
diff changeset
    16
ML {* set Toplevel.debug *}
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
    17
ML {* set show_hyps *}
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
    18
ML {* set show_sorts *}
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
    19
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    20
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    21
section {* Context Elements and Locale Expressions *}
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 15837
diff changeset
    22
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    23
text {* Naming convention for global objects: prefixes L and l *}
16168
adb83939177f Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16102
diff changeset
    24
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    25
subsection {* Renaming with Syntax *}
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    26
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    27
locale (open) LS = var mult +
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 15837
diff changeset
    28
  assumes "mult(x, y) = mult(y, x)"
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 15837
diff changeset
    29
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    30
print_locale LS
16168
adb83939177f Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16102
diff changeset
    31
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    32
locale LS' = LS mult (infixl "**" 60)
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 15837
diff changeset
    33
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    34
print_locale LS'
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 15837
diff changeset
    35
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    36
locale LT = var mult (infixl "**" 60) +
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 15837
diff changeset
    37
  assumes "x ** y = y ** x"
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 15837
diff changeset
    38
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    39
locale LU = LT mult (infixl "**" 60) + LT add (infixl "++" 55) + var h +
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 15837
diff changeset
    40
  assumes hom: "h(x ** y) = h(x) ++ h(y)"
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 15837
diff changeset
    41
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    42
locale LV = LU _ add
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 15837
diff changeset
    43
16168
adb83939177f Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16102
diff changeset
    44
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    45
subsection {* Constrains *}
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 15837
diff changeset
    46
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    47
locale LZ = fixes a (structure)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    48
locale LZ' = LZ +
16168
adb83939177f Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16102
diff changeset
    49
  constrains a :: "'a => 'b"
adb83939177f Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16102
diff changeset
    50
  assumes "a (x :: 'a) = a (y)"
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    51
print_locale LZ'
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 15837
diff changeset
    52
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 15837
diff changeset
    53
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 15837
diff changeset
    54
section {* Interpretation *}
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
    55
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    56
text {* Naming convention for global objects: prefixes I and i *}
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    57
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    58
text {* interpretation input syntax *}
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    59
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    60
locale IL
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    61
locale IM = fixes a and b and c
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    62
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    63
interpretation test [simp]: IL + IM a b c [x y z] .
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    64
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    65
print_interps IL    (* output: test *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    66
print_interps IM    (* output: test *)
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    67
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    68
interpretation test [simp]: IL print_interps IM .
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    69
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    70
interpretation IL .
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    71
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    72
text {* Processing of locale expression *}
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    73
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    74
locale IA = fixes a assumes asm_A: "a = a"
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    75
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    76
locale (open) IB = fixes b assumes asm_B [simp]: "b = b"
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    77
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    78
locale IC = IA + IB + assumes asm_C: "c = c"
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    79
  (* TODO: independent type var in c, prohibit locale declaration *)
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    80
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    81
locale ID = IA + IB + fixes d defines def_D: "d == (a = b)"
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    82
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    83
theorem (in IA)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    84
  includes ID
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
    85
  shows True ..
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
    86
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    87
theorem (in ID) True ..
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    88
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    89
typedecl i
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    90
arities i :: "term"
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    91
15598
4ab52355bb53 Registrations of global locale interpretations: improved, better naming.
ballarin
parents: 15596
diff changeset
    92
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    93
interpretation i1: IC ["X::i" "Y::i"] by (auto intro: IA.intro IC_axioms.intro)
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    94
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    95
print_interps IA  (* output: i1 *)
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    96
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
    97
(* possible accesses *)
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    98
thm i1.a.asm_A thm LocaleTest.i1.a.asm_A
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    99
thm i1.asm_A thm LocaleTest.i1.asm_A
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   100
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15598
diff changeset
   101
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15598
diff changeset
   102
(* without prefix *)
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15598
diff changeset
   103
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   104
interpretation IC ["W::i" "Z::i"] .  (* subsumed by i1: IC *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   105
interpretation IC ["W::'a" "Z::i"] by (auto intro: IA.intro IC_axioms.intro)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   106
  (* subsumes i1: IA and i1: IC *)
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   107
15598
4ab52355bb53 Registrations of global locale interpretations: improved, better naming.
ballarin
parents: 15596
diff changeset
   108
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   109
print_interps IA  (* output: <no prefix>, i1 *)
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
   110
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15763
diff changeset
   111
(* possible accesses *)
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15763
diff changeset
   112
thm asm_C thm a_b.asm_C thm LocaleTest.a_b.asm_C thm LocaleTest.a_b.asm_C
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   113
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
   114
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   115
interpretation i2: ID [X "Y::i" "Y = X"] by (simp add: eq_commute)
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15763
diff changeset
   116
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   117
print_interps IA  (* output: <no prefix>, i1 *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   118
print_interps ID  (* output: i2 *)
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15763
diff changeset
   119
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15763
diff changeset
   120
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   121
interpretation i3: ID [X "Y::i"] .
15598
4ab52355bb53 Registrations of global locale interpretations: improved, better naming.
ballarin
parents: 15596
diff changeset
   122
4ab52355bb53 Registrations of global locale interpretations: improved, better naming.
ballarin
parents: 15596
diff changeset
   123
(* duplicate: not registered *)
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   124
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   125
(* thm i3.a.asm_A *)
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   126
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
   127
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   128
print_interps IA  (* output: <no prefix>, i1 *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   129
print_interps IB  (* output: i1 *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   130
print_interps IC  (* output: <no prefix, i1 *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   131
print_interps ID  (* output: i2, i3 *)
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
   132
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15763
diff changeset
   133
(* schematic vars in instantiation not permitted *)
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15763
diff changeset
   134
(*
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   135
interpretation i4: IA ["?x::?'a1"] apply (rule IA.intro) apply rule done
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   136
print_interps IA
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   137
*)
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
   138
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   139
interpretation i10: ID + ID a' b' d' [X "Y::i" _ u "v::i" _] .
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   140
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   141
corollary (in ID) th_x: True ..
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   142
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   143
(* possible accesses: for each registration *)
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   144
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   145
thm i2.th_x thm i3.th_x
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   146
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   147
lemma (in ID) th_y: "d == (a = b)" .
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   148
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   149
thm i2.th_y thm i3.th_y
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   150
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   151
lemmas (in ID) th_z = th_y
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   152
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   153
thm i2.th_z
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   154
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
   155
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   156
subsection {* Interpretation in Proof Contexts *}
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   157
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   158
locale IF = fixes f assumes asm_F: "f & f --> f"
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 15837
diff changeset
   159
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15598
diff changeset
   160
theorem True
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15598
diff changeset
   161
proof -
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 15837
diff changeset
   162
  fix alpha::i and beta::'a and gamma::o
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   163
  (* FIXME: omitting type of beta leads to error later at interpret i6 *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   164
  have alpha_A: "IA(alpha)" by (auto intro: IA.intro)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   165
  interpret i5: IA [alpha] .  (* subsumed *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   166
  print_interps IA  (* output: <no prefix>, i1 *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   167
  interpret i6: IC [alpha beta] by (auto intro: IC_axioms.intro)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   168
  print_interps IA   (* output: <no prefix>, i1 *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   169
  print_interps IC   (* output: <no prefix>, i1, i6 *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   170
  interpret i11: IF [gamma] by (fast intro: IF.intro)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   171
  thm i11.asm_F      (* gamma is a Free *)
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15598
diff changeset
   172
qed rule
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15598
diff changeset
   173
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   174
theorem (in IA) True
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   175
proof -
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   176
  print_interps IA
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   177
  fix beta and gamma
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   178
  interpret i9: ID [a beta _]
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   179
    (* no proof obligation for IA !!! *)
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   180
    apply - apply (rule refl) apply assumption done
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   181
qed rule
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15598
diff changeset
   182
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15598
diff changeset
   183
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   184
(* Definition involving free variable *)
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   185
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   186
ML {* reset show_sorts *}
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   187
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   188
locale IE = fixes e defines e_def: "e(x) == x & x"
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   189
  notes e_def2 = e_def
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   190
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   191
lemma (in IE) True thm e_def by fast
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   192
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   193
interpretation i7: IE ["%x. x"] by simp
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   194
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   195
thm i7.e_def2 (* has no premise *)
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   196
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   197
locale IE' = fixes e defines e_def: "e == (%x. x & x)"
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   198
  notes e_def2 = e_def
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   199
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   200
interpretation i7': IE' ["(%x. x)"] by simp
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   201
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   202
thm i7'.e_def2
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   203
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   204
(* Definition involving free variable in assm *)
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   205
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   206
locale (open) IG = fixes g assumes asm_G: "g --> x"
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 15837
diff changeset
   207
  notes asm_G2 = asm_G
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   208
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   209
interpretation i8: IG ["False"] by fast
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   210
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   211
thm i8.asm_G2
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   212
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   213
text {* Locale without assumptions *}
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   214
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   215
locale IL1 = notes rev_conjI [intro] = conjI [THEN iffD1 [OF conj_commute]]
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   216
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   217
lemma "[| P; Q |] ==> P & Q"
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   218
proof -
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   219
  interpret my: IL1 .          txt {* No chained fact required. *}
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   220
  assume Q and P               txt {* order reversed *}
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   221
  then show "P & Q" ..         txt {* Applies @{thm my.rev_conjI}. *}
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   222
qed
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   223
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   224
locale IL11 = notes rev_conjI = conjI [THEN iffD1 [OF conj_commute]]
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   225
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   226
lemma "[| P; Q |] ==> P & Q"
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   227
proof -
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   228
  interpret [intro]: IL11 .     txt {* Attribute supplied at instantiation. *}
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   229
  assume Q and P
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   230
  then show "P & Q" ..
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   231
qed
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   232
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   233
subsection {* Simple locale with assumptions *}
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   234
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   235
consts ibin :: "[i, i] => i" (infixl "#" 60)
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   236
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   237
axioms i_assoc: "(x # y) # z = x # (y # z)"
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   238
  i_comm: "x # y = y # x"
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   239
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   240
locale IL2 =
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   241
  fixes OP (infixl "+" 60)
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   242
  assumes assoc: "(x + y) + z = x + (y + z)"
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   243
    and comm: "x + y = y + x"
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   244
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   245
lemma (in IL2) lcomm: "x + (y + z) = y + (x + z)"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   246
proof -
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   247
  have "x + (y + z) = (x + y) + z" by (simp add: assoc)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   248
  also have "... = (y + x) + z" by (simp add: comm)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   249
  also have "... = y + (x + z)" by (simp add: assoc)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   250
  finally show ?thesis .
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   251
qed
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   252
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   253
lemmas (in IL2) AC = comm assoc lcomm
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   254
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   255
lemma "(x::i) # y # z # w = y # x # w # z"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   256
proof -
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   257
  interpret my: IL2 ["op #"] by (rule IL2.intro [of "op #", OF i_assoc i_comm])
17033
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   258
  show ?thesis by (simp only: my.OP.AC)  (* or my.AC *)
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   259
qed
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   260
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   261
subsection {* Nested locale with assumptions *}
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   262
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   263
locale IL3 =
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   264
  fixes OP (infixl "+" 60)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   265
  assumes assoc: "(x + y) + z = x + (y + z)"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   266
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   267
locale IL4 = IL3 +
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   268
  assumes comm: "x + y = y + x"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   269
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   270
lemma (in IL4) lcomm: "x + (y + z) = y + (x + z)"
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   271
proof -
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   272
  have "x + (y + z) = (x + y) + z" by (simp add: assoc)
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   273
  also have "... = (y + x) + z" by (simp add: comm)
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   274
  also have "... = y + (x + z)" by (simp add: assoc)
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   275
  finally show ?thesis .
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   276
qed
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   277
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   278
lemmas (in IL4) AC = comm assoc lcomm
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   279
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   280
lemma "(x::i) # y # z # w = y # x # w # z"
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   281
proof -
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   282
  interpret my: IL4 ["op #"]
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   283
    by (auto intro: IL3.intro IL4_axioms.intro i_assoc i_comm)
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   284
  show ?thesis by (simp only: my.OP.AC)  (* or simply AC *)
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   285
qed
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   286
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   287
text {* Locale with definition *}
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   288
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   289
text {* This example is admittedly not very creative :-) *}
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   290
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   291
locale IL5 = IL4 + var A +
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   292
  defines A_def: "A == True"
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   293
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   294
lemma (in IL5) lem: A
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   295
  by (unfold A_def) rule
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   296
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   297
lemma "IL5(op #) ==> True"
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   298
proof -
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   299
  assume "IL5(op #)"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   300
  then interpret IL5 ["op #"] by (auto intro: IL5.axioms)
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   301
  show ?thesis by (rule lem)  (* lem instantiated to True *)
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   302
qed
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   303
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   304
text {* Interpretation in a context with target *}
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   305
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   306
lemma (in IL4)
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   307
  fixes A (infixl "$" 60)
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   308
  assumes A: "IL4(A)"
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   309
  shows "(x::i) $ y $ z $ w = y $ x $ w $ z"
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   310
proof -
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   311
  from A interpret A: IL4 ["A"] by (auto intro: IL4.axioms)
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   312
  show ?thesis by (simp only: A.OP.AC)
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   313
qed
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   314
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   315
16736
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
   316
section {* Interpretation in Locales *}
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
   317
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   318
text {* Naming convention for global objects: prefixes R and r *}
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   319
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   320
locale (open) Rsemi = var prod (infixl "**" 65) +
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   321
  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   322
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   323
locale (open) Rlgrp = Rsemi + var one + var inv +
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   324
  assumes lone: "one ** x = x"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   325
    and linv: "inv(x) ** x = one"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   326
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   327
lemma (in Rlgrp) lcancel:
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   328
  "x ** y = x ** z <-> y = z"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   329
proof
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   330
  assume "x ** y = x ** z"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   331
  then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   332
  then show "y = z" by (simp add: lone linv)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   333
qed simp
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   334
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   335
locale (open) Rrgrp = Rsemi + var one + var inv +
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   336
  assumes rone: "x ** one = x"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   337
    and rinv: "x ** inv(x) = one"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   338
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   339
lemma (in Rrgrp) rcancel:
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   340
  "y ** x = z ** x <-> y = z"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   341
proof
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   342
  assume "y ** x = z ** x"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   343
  then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   344
    by (simp add: assoc [symmetric])
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   345
  then show "y = z" by (simp add: rone rinv)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   346
qed simp
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   347
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   348
interpretation Rlgrp < Rrgrp
17033
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   349
  proof -
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   350
    {
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   351
      fix x
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   352
      have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   353
      then show "x ** one = x" by (simp add: assoc lcancel)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   354
    }
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   355
    note rone = this
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   356
    {
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   357
      fix x
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   358
      have "inv(x) ** x ** inv(x) = inv(x) ** one"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   359
	by (simp add: linv lone rone)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   360
      then show "x ** inv(x) = one" by (simp add: assoc lcancel)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   361
    }
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   362
  qed
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   363
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   364
(* effect on printed locale *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   365
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   366
print_locale Rlgrp
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   367
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   368
(* use of derived theorem *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   369
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   370
lemma (in Rlgrp)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   371
  "y ** x = z ** x <-> y = z"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   372
  apply (rule rcancel)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   373
  print_interps Rrgrp thm lcancel rcancel
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   374
  done
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   375
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   376
(* circular interpretation *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   377
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   378
interpretation Rrgrp < Rlgrp
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   379
  proof -
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   380
    {
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   381
      fix x
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   382
      have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   383
      then show "one ** x = x" by (simp add: assoc [symmetric] rcancel)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   384
    }
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   385
    note lone = this
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   386
    {
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   387
      fix x
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   388
      have "inv(x) ** (x ** inv(x)) = one ** inv(x)"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   389
	by (simp add: rinv lone rone)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   390
      then show "inv(x) ** x = one" by (simp add: assoc [symmetric] rcancel)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   391
    }
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   392
  qed
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   393
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   394
(* effect on printed locale *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   395
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   396
print_locale Rrgrp
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   397
print_locale Rlgrp
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   398
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   399
(* locale with many parameters ---
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   400
   interpretations generate alternating group A5 *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   401
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   402
locale RA5 = var A + var B + var C + var D + var E +
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   403
  assumes eq: "A <-> B <-> C <-> D <-> E"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   404
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   405
interpretation RA5 < RA5 _ _ D E C
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   406
print_facts
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   407
print_interps RA5
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   408
  using A_B_C_D_E.eq apply (blast intro: RA5.intro) done
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   409
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   410
interpretation RA5 < RA5 C _ E _ A
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   411
print_facts
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   412
print_interps RA5
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   413
  using A_B_C_D_E.eq apply (blast intro: RA5.intro) done
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   414
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   415
interpretation RA5 < RA5 B C A _ _
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   416
print_facts
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   417
print_interps RA5
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   418
  using A_B_C_D_E.eq apply (blast intro: RA5.intro) done
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   419
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   420
lemma (in RA5) True
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   421
print_facts
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   422
print_interps RA5
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   423
  ..
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   424
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   425
interpretation RA5 < RA5 _ C D B _ .
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   426
  (* Any even permutation of parameters is subsumed by the above. *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   427
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   428
(* circle of three locales, forward direction *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   429
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   430
locale (open) RA1 = var A + var B + assumes p: "A <-> B"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   431
locale (open) RA2 = var A + var B + assumes q: "A & B | ~ A & ~ B"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   432
locale (open) RA3 = var A + var B + assumes r: "(A --> B) & (B --> A)"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   433
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   434
interpretation RA1 < RA2
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   435
  print_facts
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   436
  using p apply fast done
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   437
interpretation RA2 < RA3
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   438
  print_facts
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   439
  using q apply fast done
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   440
interpretation RA3 < RA1
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   441
  print_facts
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   442
  using r apply fast done
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   443
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   444
(* circle of three locales, backward direction *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   445
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   446
locale (open) RB1 = var A + var B + assumes p: "A <-> B"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   447
locale (open) RB2 = var A + var B + assumes q: "A & B | ~ A & ~ B"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   448
locale (open) RB3 = var A + var B + assumes r: "(A --> B) & (B --> A)"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   449
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   450
interpretation RB1 < RB2
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   451
  print_facts
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   452
  using p apply fast done
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   453
interpretation RB3 < RB1
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   454
  print_facts
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   455
  using r apply fast done
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   456
interpretation RB2 < RB3
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   457
  print_facts
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   458
  using q apply fast done
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   459
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   460
lemma (in RB1) True
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   461
  print_facts
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   462
  ..
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   463
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   464
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   465
(* Group example revisited, with predicates *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   466
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   467
locale Rpsemi = var prod (infixl "**" 65) +
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   468
  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   469
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   470
locale Rplgrp = Rpsemi + var one + var inv +
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   471
  assumes lone: "one ** x = x"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   472
    and linv: "inv(x) ** x = one"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   473
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   474
lemma (in Rplgrp) lcancel:
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   475
  "x ** y = x ** z <-> y = z"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   476
proof
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   477
  assume "x ** y = x ** z"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   478
  then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   479
  then show "y = z" by (simp add: lone linv)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   480
qed simp
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   481
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   482
locale Rprgrp = Rpsemi + var one + var inv +
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   483
  assumes rone: "x ** one = x"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   484
    and rinv: "x ** inv(x) = one"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   485
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   486
lemma (in Rprgrp) rcancel:
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   487
  "y ** x = z ** x <-> y = z"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   488
proof
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   489
  assume "y ** x = z ** x"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   490
  then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   491
    by (simp add: assoc [symmetric])
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   492
  then show "y = z" by (simp add: rone rinv)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   493
qed simp
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   494
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   495
interpretation Rplgrp < Rprgrp
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   496
  proof (rule Rprgrp_axioms.intro)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   497
    {
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   498
      fix x
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   499
      have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   500
      then show "x ** one = x" by (simp add: assoc lcancel)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   501
    }
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   502
    note rone = this
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   503
    {
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   504
      fix x
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   505
      have "inv(x) ** x ** inv(x) = inv(x) ** one"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   506
	by (simp add: linv lone rone)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   507
      then show "x ** inv(x) = one" by (simp add: assoc lcancel)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   508
    }
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   509
  qed
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   510
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   511
(* effect on printed locale *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   512
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   513
print_locale Rplgrp
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   514
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   515
(* use of derived theorem *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   516
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   517
lemma (in Rplgrp)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   518
  "y ** x = z ** x <-> y = z"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   519
  apply (rule rcancel)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   520
  print_interps Rprgrp thm lcancel rcancel
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   521
  done
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   522
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   523
(* circular interpretation *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   524
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   525
interpretation Rprgrp < Rplgrp
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   526
  proof (rule Rplgrp_axioms.intro)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   527
    {
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   528
      fix x
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   529
      have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   530
      then show "one ** x = x" by (simp add: assoc [symmetric] rcancel)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   531
    }
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   532
    note lone = this
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   533
    {
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   534
      fix x
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   535
      have "inv(x) ** (x ** inv(x)) = one ** inv(x)"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   536
	by (simp add: rinv lone rone)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   537
      then show "inv(x) ** x = one" by (simp add: assoc [symmetric] rcancel)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   538
    }
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   539
  qed
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   540
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   541
(* effect on printed locale *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   542
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   543
print_locale Rprgrp
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   544
print_locale Rplgrp
16736
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
   545
17033
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   546
subsection {* Interaction of Interpretation in Theories and Locales:
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   547
  in Locale, then in Theory *}
17033
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   548
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   549
consts
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   550
  rone :: i
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   551
  rinv :: "i => i"
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   552
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   553
axioms
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   554
  r_one : "rone # x = x"
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   555
  r_inv : "rinv(x) # x = rone"
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   556
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   557
interpretation Rbool: Rlgrp ["op #" "rone" "rinv"]
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   558
proof -
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   559
  fix x y z
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   560
  {
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   561
    show "(x # y) # z = x # (y # z)" by (rule i_assoc)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   562
  next
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   563
    show "rone # x = x" by (rule r_one)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   564
  next
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   565
    show "rinv(x) # x = rone" by (rule r_inv)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   566
  }
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   567
qed
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   568
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   569
(* derived elements *)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   570
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   571
print_interps Rrgrp
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   572
print_interps Rlgrp
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   573
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   574
lemma "y # x = z # x <-> y = z" by (rule Rbool.rcancel)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   575
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   576
(* adding lemma to derived element *)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   577
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   578
lemma (in Rrgrp) new_cancel:
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   579
  "b ** a = c ** a <-> b = c"
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   580
  by (rule rcancel)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   581
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   582
thm Rbool.new_cancel (* additional prems discharged!! *)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   583
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   584
lemma "b # a = c # a <-> b = c" by (rule Rbool.new_cancel)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   585
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   586
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   587
subsection {* Interaction of Interpretation in Theories and Locales:
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   588
  in Theory, then in Locale *}
17033
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   589
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   590
(* Another copy of the group example *)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   591
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   592
locale Rqsemi = var prod (infixl "**" 65) +
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   593
  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   594
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   595
locale Rqlgrp = Rqsemi + var one + var inv +
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   596
  assumes lone: "one ** x = x"
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   597
    and linv: "inv(x) ** x = one"
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   598
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   599
lemma (in Rqlgrp) lcancel:
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   600
  "x ** y = x ** z <-> y = z"
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   601
proof
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   602
  assume "x ** y = x ** z"
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   603
  then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   604
  then show "y = z" by (simp add: lone linv)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   605
qed simp
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   606
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   607
locale Rqrgrp = Rqsemi + var one + var inv +
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   608
  assumes rone: "x ** one = x"
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   609
    and rinv: "x ** inv(x) = one"
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   610
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   611
lemma (in Rqrgrp) rcancel:
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   612
  "y ** x = z ** x <-> y = z"
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   613
proof
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   614
  assume "y ** x = z ** x"
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   615
  then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   616
    by (simp add: assoc [symmetric])
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   617
  then show "y = z" by (simp add: rone rinv)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   618
qed simp
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   619
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   620
interpretation R2: Rqlgrp ["op #" "rone" "rinv"] 
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   621
proof -
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   622
  apply_end (rule Rqsemi.intro)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   623
  fix x y z
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   624
  {
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   625
    show "(x # y) # z = x # (y # z)" by (rule i_assoc)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   626
  next
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   627
  apply_end (rule Rqlgrp_axioms.intro)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   628
    show "rone # x = x" by (rule r_one)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   629
  next
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   630
    show "rinv(x) # x = rone" by (rule r_inv)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   631
  }
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   632
qed
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   633
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   634
print_interps Rqsemi
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   635
print_interps Rqlgrp
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   636
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   637
interpretation Rqlgrp < Rqrgrp
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   638
  proof (rule Rqrgrp_axioms.intro)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   639
    {
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   640
      fix x
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   641
      have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   642
      then show "x ** one = x" by (simp add: assoc lcancel)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   643
    }
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   644
    note rone = this
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   645
    {
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   646
      fix x
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   647
      have "inv(x) ** x ** inv(x) = inv(x) ** one"
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   648
	by (simp add: linv lone rone)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   649
      then show "x ** inv(x) = one" by (simp add: assoc lcancel)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   650
    }
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   651
  qed
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   652
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   653
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   654
subsection {* Generation of Witness Theorems for Transitive Interpretations *}
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   655
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   656
locale Rtriv = var x +
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   657
  assumes x: "x = x"
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   658
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   659
locale Rtriv2 = var x + var y +
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   660
  assumes x: "x = x" and y: "y = y"
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   661
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   662
interpretation Rtriv2 < Rtriv x
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   663
  apply (rule Rtriv.intro)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   664
  apply (rule x)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   665
  done
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   666
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   667
interpretation Rtriv2 < Rtriv y
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   668
  apply (rule Rtriv.intro)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   669
  apply (rule y)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   670
  done
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   671
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   672
print_locale Rtriv2
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   673
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   674
locale Rtriv3 = var x + var y + var z +
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   675
  assumes x: "x = x" and y: "y = y" and z: "z = z"
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   676
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   677
interpretation Rtriv3 < Rtriv2 x y
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   678
  apply (rule Rtriv2.intro)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   679
  apply (rule x)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   680
  apply (rule y)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   681
  done
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   682
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   683
print_locale Rtriv3
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   684
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   685
interpretation Rtriv3 < Rtriv2 x z
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   686
  apply (rule Rtriv2.intro)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   687
  apply (rule x_y_z.x)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   688
  apply (rule z)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   689
  done
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   690
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   691
ML {* set show_types *}
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   692
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   693
print_locale Rtriv3
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   694
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   695
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   696
subsection {* Normalisation Replaces Assumed Element by Derived Element *}
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   697
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   698
typedecl ('a, 'b) pair
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   699
arities pair :: ("term", "term") "term"
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   700
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   701
consts
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   702
  pair :: "['a, 'b] => ('a, 'b) pair"
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   703
  fst :: "('a, 'b) pair => 'a"
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   704
  snd :: "('a, 'b) pair => 'b"
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   705
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   706
axioms
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   707
  fst [simp]: "fst(pair(x, y)) = x"
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   708
  snd [simp]: "snd(pair(x, y)) = y"
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   709
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   710
locale Rpair = var prod (infixl "**" 65) + var prodP (infixl "***" 65) +
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   711
  defines P_def: "x *** y == pair(fst(x) ** fst(y), snd(x) ** snd(y))"
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   712
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   713
locale Rpair_semi = Rpair + Rpsemi
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   714
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   715
interpretation Rpair_semi < Rpsemi prodP (infixl "***" 65)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   716
proof (rule Rpsemi.intro)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   717
  fix x y z
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   718
  show "(x *** y) *** z = x *** (y *** z)"
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   719
    by (unfold P_def) (simp add: assoc)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   720
qed
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   721
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   722
locale Rsemi_rev = Rpsemi + var rprod (infixl "++" 65) +
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   723
  defines r_def: "x ++ y == y ** x"
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   724
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   725
lemma (in Rsemi_rev) r_assoc:
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   726
  "(x ++ y) ++ z = x ++ (y ++ z)"
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   727
  by (simp add: r_def assoc)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   728
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   729
lemma (in Rpair_semi)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   730
  includes Rsemi_rev prodP (infixl "***" 65) rprodP (infixl "+++" 65)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   731
  constrains prod :: "['a, 'a] => 'a"
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   732
    and rprodP :: "[('a, 'a) pair, ('a, 'a) pair] => ('a, 'a) pair"
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   733
  shows "(x +++ y) +++ z = x +++ (y +++ z)"
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   734
  apply (rule r_assoc) done
17033
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   735
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
   736
end
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   737
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   738
(* Known problems:
17033
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   739
- var vs. fixes in locale to be interpreted (interpretation in locale)
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   740
  (implicit locale expressions generated by multiple registrations)
17033
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   741
- reprocess registrations in theory (after qed)?
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   742
- current finish_global adds unwanted lemmas to theory/locale
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   743
*)