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