src/FOL/ex/LocaleTest.thy
author ballarin
Fri, 20 Apr 2007 16:55:38 +0200
changeset 22757 d3298d63b7b6
parent 22659 f792579b6e59
child 22931 11cc1ccad58e
permissions -rw-r--r--
Interpretation equations applied to attributes
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
19783
82f365a14960 Improved parameter management of locales.
ballarin
parents: 17436
diff changeset
    56
(*
20034
28fcbcf49fe5 Modified comment.
ballarin
parents: 19984
diff changeset
    57
FIXME: graceful handling of type errors?
19783
82f365a14960 Improved parameter management of locales.
ballarin
parents: 17436
diff changeset
    58
locale LY = LT mult (infixl "**" 60) + LT add (binder "++" 55) + var h +
82f365a14960 Improved parameter management of locales.
ballarin
parents: 17436
diff changeset
    59
  assumes "mult(x) == add"
82f365a14960 Improved parameter management of locales.
ballarin
parents: 17436
diff changeset
    60
*)
82f365a14960 Improved parameter management of locales.
ballarin
parents: 17436
diff changeset
    61
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    62
locale LV = LU _ add
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 15837
diff changeset
    63
19783
82f365a14960 Improved parameter management of locales.
ballarin
parents: 17436
diff changeset
    64
locale LW = LU _ mult (infixl "**" 60)
82f365a14960 Improved parameter management of locales.
ballarin
parents: 17436
diff changeset
    65
16168
adb83939177f Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16102
diff changeset
    66
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    67
subsection {* Constrains *}
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 15837
diff changeset
    68
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    69
locale LZ = fixes a (structure)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    70
locale LZ' = LZ +
16168
adb83939177f Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16102
diff changeset
    71
  constrains a :: "'a => 'b"
adb83939177f Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16102
diff changeset
    72
  assumes "a (x :: 'a) = a (y)"
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    73
print_locale LZ'
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 15837
diff changeset
    74
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 15837
diff changeset
    75
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 15837
diff changeset
    76
section {* Interpretation *}
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
    77
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    78
text {* Naming convention for global objects: prefixes I and i *}
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    79
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    80
text {* interpretation input syntax *}
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
locale IL
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    83
locale IM = fixes a and b and c
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    84
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    85
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
    86
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    87
print_interps IL    (* output: test *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    88
print_interps IM    (* output: test *)
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
interpretation test [simp]: IL print_interps IM .
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
interpretation IL .
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    93
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    94
text {* Processing of locale expression *}
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    95
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    96
locale IA = fixes a assumes asm_A: "a = a"
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    97
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
    98
locale (open) IB = fixes b assumes asm_B [simp]: "b = b"
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    99
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   100
locale IC = IA + IB + assumes asm_C: "c = c"
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
   101
  (* TODO: independent type var in c, prohibit locale declaration *)
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
   102
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   103
locale ID = IA + IB + fixes d defines def_D: "d == (a = b)"
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
   104
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   105
theorem (in IA)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   106
  includes ID
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19783
diff changeset
   107
  shows True
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19783
diff changeset
   108
  print_interps! IA
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19783
diff changeset
   109
  print_interps! ID
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19783
diff changeset
   110
  ..
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   111
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   112
theorem (in ID) True ..
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
   113
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
   114
typedecl i
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
   115
arities i :: "term"
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
   116
15598
4ab52355bb53 Registrations of global locale interpretations: improved, better naming.
ballarin
parents: 15596
diff changeset
   117
19984
29bb4659f80a Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents: 19931
diff changeset
   118
interpretation i1: IC ["X::i" "Y::i"] by unfold_locales auto
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
   119
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   120
print_interps IA  (* output: i1 *)
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
   121
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   122
(* possible accesses *)
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   123
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
   124
thm i1.asm_A thm LocaleTest.i1.asm_A
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   125
17139
165c97f9bb63 Printing of interpretations: option to show witness theorems;
ballarin
parents: 17096
diff changeset
   126
ML {* check_thm "i1.a.asm_A" *}
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15598
diff changeset
   127
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15598
diff changeset
   128
(* without prefix *)
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15598
diff changeset
   129
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   130
interpretation IC ["W::i" "Z::i"] .  (* subsumed by i1: IC *)
19984
29bb4659f80a Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents: 19931
diff changeset
   131
interpretation IC ["W::'a" "Z::i"] by unfold_locales auto
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   132
  (* subsumes i1: IA and i1: IC *)
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   133
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   134
print_interps IA  (* output: <no prefix>, i1 *)
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
   135
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15763
diff changeset
   136
(* possible accesses *)
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15763
diff changeset
   137
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
   138
17139
165c97f9bb63 Printing of interpretations: option to show witness theorems;
ballarin
parents: 17096
diff changeset
   139
ML {* check_thm "asm_C" *}
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
   140
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19783
diff changeset
   141
interpretation i2: ID [X "Y::i" "Y = X"]
19984
29bb4659f80a Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents: 19931
diff changeset
   142
  by (simp add: eq_commute) unfold_locales
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15763
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 ID  (* output: i2 *)
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15763
diff changeset
   146
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15763
diff changeset
   147
19984
29bb4659f80a Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents: 19931
diff changeset
   148
interpretation i3: ID [X "Y::i"] by simp unfold_locales
15598
4ab52355bb53 Registrations of global locale interpretations: improved, better naming.
ballarin
parents: 15596
diff changeset
   149
17436
ballarin
parents: 17228
diff changeset
   150
(* duplicate: thm not added *)
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   151
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   152
(* thm i3.a.asm_A *)
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
print_interps IA  (* output: <no prefix>, i1 *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   156
print_interps IB  (* output: i1 *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   157
print_interps IC  (* output: <no prefix, i1 *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   158
print_interps ID  (* output: i2, i3 *)
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
   159
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15763
diff changeset
   160
(* schematic vars in instantiation not permitted *)
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15763
diff changeset
   161
(*
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   162
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
   163
print_interps IA
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   164
*)
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
   165
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   166
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
   167
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   168
corollary (in ID) th_x: True ..
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   169
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   170
(* possible accesses: for each registration *)
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   171
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   172
thm i2.th_x thm i3.th_x
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   173
17139
165c97f9bb63 Printing of interpretations: option to show witness theorems;
ballarin
parents: 17096
diff changeset
   174
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
   175
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   176
lemma (in ID) th_y: "d == (a = b)" .
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   177
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   178
thm i2.th_y thm i3.th_y
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   179
17139
165c97f9bb63 Printing of interpretations: option to show witness theorems;
ballarin
parents: 17096
diff changeset
   180
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
   181
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   182
lemmas (in ID) th_z = th_y
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   183
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   184
thm i2.th_z
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   185
17139
165c97f9bb63 Printing of interpretations: option to show witness theorems;
ballarin
parents: 17096
diff changeset
   186
ML {* check_thm "i2.th_z" *}
165c97f9bb63 Printing of interpretations: option to show witness theorems;
ballarin
parents: 17096
diff changeset
   187
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
   188
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   189
subsection {* Interpretation in Proof Contexts *}
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   190
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   191
locale IF = fixes f assumes asm_F: "f & f --> f"
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 15837
diff changeset
   192
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15598
diff changeset
   193
theorem True
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15598
diff changeset
   194
proof -
22757
d3298d63b7b6 Interpretation equations applied to attributes
ballarin
parents: 22659
diff changeset
   195
  fix alpha::i and beta and gamma::o
19984
29bb4659f80a Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents: 19931
diff changeset
   196
  have alpha_A: "IA(alpha)" by unfold_locales simp
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   197
  interpret i5: IA [alpha] .  (* subsumed *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   198
  print_interps IA  (* output: <no prefix>, i1 *)
19984
29bb4659f80a Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents: 19931
diff changeset
   199
  interpret i6: IC [alpha beta] by unfold_locales auto
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   200
  print_interps IA   (* output: <no prefix>, i1 *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   201
  print_interps IC   (* output: <no prefix>, i1, i6 *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   202
  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
   203
  thm i11.asm_F      (* gamma is a Free *)
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15598
diff changeset
   204
qed rule
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15598
diff changeset
   205
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   206
theorem (in IA) True
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   207
proof -
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19783
diff changeset
   208
  print_interps! IA
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   209
  fix beta and gamma
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   210
  interpret i9: ID [a beta _]
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19783
diff changeset
   211
    apply - apply assumption
19984
29bb4659f80a Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents: 19931
diff changeset
   212
    apply unfold_locales
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19783
diff changeset
   213
    apply (rule refl) done
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   214
qed rule
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15598
diff changeset
   215
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15598
diff changeset
   216
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   217
(* Definition involving free variable *)
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   218
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   219
ML {* reset show_sorts *}
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
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
lemma (in IE) True thm e_def by fast
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
interpretation i7: IE ["%x. x"] by simp
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   227
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   228
thm i7.e_def2 (* has no premise *)
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   229
17139
165c97f9bb63 Printing of interpretations: option to show witness theorems;
ballarin
parents: 17096
diff changeset
   230
ML {* check_thm "i7.e_def2" *}
165c97f9bb63 Printing of interpretations: option to show witness theorems;
ballarin
parents: 17096
diff changeset
   231
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   232
locale IE' = fixes e defines e_def: "e == (%x. x & x)"
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   233
  notes e_def2 = e_def
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 i7': IE' ["(%x. x)"] by simp
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 i7'.e_def2
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 "i7'.e_def2" *}
165c97f9bb63 Printing of interpretations: option to show witness theorems;
ballarin
parents: 17096
diff changeset
   240
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   241
(* Definition involving free variable in assm *)
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 (open) IG = fixes g assumes asm_G: "g --> x"
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 15837
diff changeset
   244
  notes asm_G2 = asm_G
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   245
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   246
interpretation i8: IG ["False"] by fast
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   247
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   248
thm i8.asm_G2
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   249
17139
165c97f9bb63 Printing of interpretations: option to show witness theorems;
ballarin
parents: 17096
diff changeset
   250
ML {* check_thm "i8.asm_G2" *}
165c97f9bb63 Printing of interpretations: option to show witness theorems;
ballarin
parents: 17096
diff changeset
   251
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   252
text {* Locale without assumptions *}
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   253
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   254
locale IL1 = notes rev_conjI [intro] = conjI [THEN iffD1 [OF conj_commute]]
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   255
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   256
lemma "[| P; Q |] ==> P & Q"
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   257
proof -
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   258
  interpret my: IL1 .          txt {* No chained fact required. *}
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   259
  assume Q and P               txt {* order reversed *}
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   260
  then show "P & Q" ..         txt {* Applies @{thm my.rev_conjI}. *}
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   261
qed
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
locale IL11 = notes rev_conjI = conjI [THEN iffD1 [OF conj_commute]]
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
lemma "[| P; Q |] ==> P & Q"
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   266
proof -
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   267
  interpret [intro]: IL11 .     txt {* Attribute supplied at instantiation. *}
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   268
  assume Q and P
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   269
  then show "P & Q" ..
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   270
qed
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   271
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   272
subsection {* Simple locale with assumptions *}
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   273
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   274
consts ibin :: "[i, i] => i" (infixl "#" 60)
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   275
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   276
axioms i_assoc: "(x # y) # z = x # (y # z)"
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   277
  i_comm: "x # y = y # x"
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   278
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   279
locale IL2 =
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   280
  fixes OP (infixl "+" 60)
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   281
  assumes assoc: "(x + y) + z = x + (y + z)"
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   282
    and comm: "x + y = y + x"
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   283
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   284
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
   285
proof -
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   286
  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
   287
  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
   288
  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
   289
  finally show ?thesis .
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   290
qed
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   291
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   292
lemmas (in IL2) AC = comm assoc lcomm
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   293
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   294
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
   295
proof -
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   296
  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
   297
  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
   298
qed
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   299
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   300
subsection {* Nested locale with assumptions *}
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   301
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   302
locale IL3 =
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   303
  fixes OP (infixl "+" 60)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   304
  assumes assoc: "(x + y) + z = x + (y + z)"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   305
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   306
locale IL4 = IL3 +
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   307
  assumes comm: "x + y = y + x"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   308
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   309
lemma (in IL4) lcomm: "x + (y + z) = y + (x + z)"
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   310
proof -
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   311
  have "x + (y + z) = (x + y) + z" by (simp add: assoc)
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   312
  also have "... = (y + x) + z" by (simp add: comm)
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   313
  also have "... = y + (x + z)" by (simp add: assoc)
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   314
  finally show ?thesis .
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   315
qed
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   316
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   317
lemmas (in IL4) AC = comm assoc lcomm
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   318
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   319
lemma "(x::i) # y # z # w = y # x # w # z"
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   320
proof -
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   321
  interpret my: IL4 ["op #"]
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19783
diff changeset
   322
    by (auto intro: IL4.intro IL3.intro IL4_axioms.intro i_assoc i_comm)
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   323
  show ?thesis by (simp only: my.OP.AC)  (* or simply AC *)
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   324
qed
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   325
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   326
text {* Locale with definition *}
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   327
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   328
text {* This example is admittedly not very creative :-) *}
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   329
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   330
locale IL5 = IL4 + var A +
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   331
  defines A_def: "A == True"
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   332
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   333
lemma (in IL5) lem: A
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   334
  by (unfold A_def) rule
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   335
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   336
lemma "IL5(op #) ==> True"
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   337
proof -
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   338
  assume "IL5(op #)"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   339
  then interpret IL5 ["op #"] by (auto intro: IL5.axioms)
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   340
  show ?thesis by (rule lem)  (* lem instantiated to True *)
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
text {* Interpretation in a context with target *}
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   344
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   345
lemma (in IL4)
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   346
  fixes A (infixl "$" 60)
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   347
  assumes A: "IL4(A)"
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   348
  shows "(x::i) $ y $ z $ w = y $ x $ w $ z"
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   349
proof -
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   350
  from A interpret A: IL4 ["A"] by (auto intro: IL4.axioms)
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   351
  show ?thesis by (simp only: A.OP.AC)
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   352
qed
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   353
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   354
16736
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
   355
section {* Interpretation in Locales *}
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
   356
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   357
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
   358
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   359
locale (open) Rsemi = var prod (infixl "**" 65) +
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   360
  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   361
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   362
locale (open) Rlgrp = Rsemi + var one + var inv +
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   363
  assumes lone: "one ** x = x"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   364
    and linv: "inv(x) ** x = one"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   365
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   366
lemma (in Rlgrp) lcancel:
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   367
  "x ** y = x ** z <-> y = z"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   368
proof
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   369
  assume "x ** y = x ** z"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   370
  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
   371
  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
   372
qed simp
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   373
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   374
locale (open) Rrgrp = Rsemi + var one + var inv +
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   375
  assumes rone: "x ** one = x"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   376
    and rinv: "x ** inv(x) = one"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   377
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   378
lemma (in Rrgrp) rcancel:
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   379
  "y ** x = z ** x <-> y = z"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   380
proof
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   381
  assume "y ** x = z ** x"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   382
  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
   383
    by (simp add: assoc [symmetric])
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   384
  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
   385
qed simp
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   386
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   387
interpretation Rlgrp < Rrgrp
17033
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   388
  proof -
17000
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
      fix x
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   391
      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
   392
      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
   393
    }
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   394
    note rone = this
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
      fix x
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   397
      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
   398
	by (simp add: linv lone rone)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   399
      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
   400
    }
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   401
  qed
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   402
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   403
(* effect on printed locale *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   404
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19783
diff changeset
   405
print_locale! Rlgrp
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   406
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   407
(* use of derived theorem *)
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
lemma (in Rlgrp)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   410
  "y ** x = z ** x <-> y = z"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   411
  apply (rule rcancel)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   412
  print_interps Rrgrp thm lcancel rcancel
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   413
  done
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   414
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   415
(* circular interpretation *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   416
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   417
interpretation Rrgrp < Rlgrp
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   418
  proof -
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
      fix x
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   421
      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
   422
      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
   423
    }
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   424
    note lone = this
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   425
    {
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   426
      fix x
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   427
      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
   428
	by (simp add: rinv lone rone)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   429
      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
   430
    }
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   431
  qed
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
(* effect on printed locale *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   434
17228
19b460b39dad print_locale omits facts by default
ballarin
parents: 17139
diff changeset
   435
print_locale! Rrgrp
19b460b39dad print_locale omits facts by default
ballarin
parents: 17139
diff changeset
   436
print_locale! Rlgrp
17000
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
(* locale with many parameters ---
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   439
   interpretations generate alternating group A5 *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   440
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   441
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
   442
  assumes eq: "A <-> B <-> C <-> D <-> E"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   443
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   444
interpretation RA5 < RA5 _ _ D E C
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   445
print_facts
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   446
print_interps RA5
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   447
  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
   448
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   449
interpretation RA5 < RA5 C _ E _ A
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   450
print_facts
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   451
print_interps RA5
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   452
  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
   453
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   454
interpretation RA5 < RA5 B C A _ _
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   455
print_facts
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   456
print_interps RA5
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   457
  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
   458
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   459
interpretation RA5 < RA5 _ C D B _ .
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   460
  (* 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
   461
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   462
(* circle of three locales, forward direction *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   463
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   464
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
   465
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
   466
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
   467
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   468
interpretation RA1 < RA2
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 p apply fast done
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   471
interpretation RA2 < RA3
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   472
  print_facts
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   473
  using q apply fast done
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   474
interpretation RA3 < RA1
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   475
  print_facts
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   476
  using r apply fast done
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
(* circle of three locales, backward direction *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   479
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   480
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
   481
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
   482
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
   483
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   484
interpretation RB1 < RB2
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 p apply fast done
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   487
interpretation RB3 < RB1
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   488
  print_facts
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   489
  using r apply fast done
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   490
interpretation RB2 < RB3
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   491
  print_facts
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   492
  using q apply fast done
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   493
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   494
lemma (in RB1) True
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   495
  print_facts
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   496
  ..
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
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   499
(* Group example revisited, with predicates *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   500
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   501
locale Rpsemi = var prod (infixl "**" 65) +
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   502
  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   503
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   504
locale Rplgrp = Rpsemi + var one + var inv +
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   505
  assumes lone: "one ** x = x"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   506
    and linv: "inv(x) ** x = one"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   507
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   508
lemma (in Rplgrp) lcancel:
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   509
  "x ** y = x ** z <-> y = z"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   510
proof
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   511
  assume "x ** y = x ** z"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   512
  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
   513
  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
   514
qed simp
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   515
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   516
locale Rprgrp = Rpsemi + var one + var inv +
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   517
  assumes rone: "x ** one = x"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   518
    and rinv: "x ** inv(x) = one"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   519
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   520
lemma (in Rprgrp) rcancel:
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   521
  "y ** x = z ** x <-> y = z"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   522
proof
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   523
  assume "y ** x = z ** x"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   524
  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
   525
    by (simp add: assoc [symmetric])
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   526
  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
   527
qed simp
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   528
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   529
interpretation Rplgrp < Rprgrp
19984
29bb4659f80a Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents: 19931
diff changeset
   530
  proof unfold_locales
17000
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 ** 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
   534
      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
   535
    }
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   536
    note rone = this
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   537
    {
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   538
      fix x
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   539
      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
   540
	by (simp add: linv lone rone)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   541
      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
   542
    }
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   543
  qed
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
(* effect on printed locale *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   546
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19783
diff changeset
   547
print_locale! Rplgrp
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   548
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   549
(* use of derived theorem *)
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
lemma (in Rplgrp)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   552
  "y ** x = z ** x <-> y = z"
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   553
  apply (rule rcancel)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   554
  print_interps Rprgrp thm lcancel rcancel
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   555
  done
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   556
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   557
(* circular interpretation *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   558
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   559
interpretation Rprgrp < Rplgrp
19984
29bb4659f80a Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents: 19931
diff changeset
   560
  proof unfold_locales
17000
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 "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
   564
      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
   565
    }
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   566
    note lone = this
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   567
    {
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   568
      fix x
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   569
      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
   570
	by (simp add: rinv lone rone)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   571
      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
   572
    }
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   573
  qed
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   574
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   575
(* effect on printed locale *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16736
diff changeset
   576
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19783
diff changeset
   577
print_locale! Rprgrp
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19783
diff changeset
   578
print_locale! Rplgrp
16736
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
   579
17033
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   580
subsection {* Interaction of Interpretation in Theories and Locales:
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   581
  in Locale, then in Theory *}
17033
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   582
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   583
consts
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   584
  rone :: i
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   585
  rinv :: "i => i"
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   586
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   587
axioms
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   588
  r_one : "rone # x = x"
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   589
  r_inv : "rinv(x) # x = rone"
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   590
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   591
interpretation Rbool: Rlgrp ["op #" "rone" "rinv"]
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   592
proof -
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   593
  fix x y z
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   594
  {
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   595
    show "(x # y) # z = x # (y # z)" by (rule i_assoc)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   596
  next
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   597
    show "rone # x = x" by (rule r_one)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   598
  next
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   599
    show "rinv(x) # x = rone" by (rule r_inv)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   600
  }
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   601
qed
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   602
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   603
(* derived elements *)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   604
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   605
print_interps Rrgrp
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   606
print_interps Rlgrp
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   607
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   608
lemma "y # x = z # x <-> y = z" by (rule Rbool.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
(* adding lemma to derived element *)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   611
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   612
lemma (in Rrgrp) new_cancel:
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   613
  "b ** a = c ** a <-> b = c"
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   614
  by (rule rcancel)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   615
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   616
thm Rbool.new_cancel (* additional prems discharged!! *)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   617
17139
165c97f9bb63 Printing of interpretations: option to show witness theorems;
ballarin
parents: 17096
diff changeset
   618
ML {* check_thm "Rbool.new_cancel" *}
165c97f9bb63 Printing of interpretations: option to show witness theorems;
ballarin
parents: 17096
diff changeset
   619
17033
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   620
lemma "b # a = c # a <-> b = c" by (rule Rbool.new_cancel)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   621
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   622
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   623
subsection {* Interaction of Interpretation in Theories and Locales:
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   624
  in Theory, then in Locale *}
17033
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   625
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   626
(* Another copy of the group example *)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   627
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   628
locale Rqsemi = var prod (infixl "**" 65) +
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   629
  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   630
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   631
locale Rqlgrp = Rqsemi + var one + var inv +
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   632
  assumes lone: "one ** x = x"
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   633
    and linv: "inv(x) ** x = one"
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   634
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   635
lemma (in Rqlgrp) lcancel:
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   636
  "x ** y = x ** z <-> y = z"
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   637
proof
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   638
  assume "x ** y = x ** z"
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   639
  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
   640
  then show "y = z" by (simp add: lone linv)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   641
qed simp
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   642
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   643
locale Rqrgrp = Rqsemi + var one + var inv +
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   644
  assumes rone: "x ** one = x"
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   645
    and rinv: "x ** inv(x) = one"
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   646
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   647
lemma (in Rqrgrp) rcancel:
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   648
  "y ** x = z ** x <-> y = z"
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   649
proof
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   650
  assume "y ** x = z ** x"
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   651
  then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   652
    by (simp add: assoc [symmetric])
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   653
  then show "y = z" by (simp add: rone rinv)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   654
qed simp
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   655
17139
165c97f9bb63 Printing of interpretations: option to show witness theorems;
ballarin
parents: 17096
diff changeset
   656
interpretation Rqrgrp < Rprgrp
19984
29bb4659f80a Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents: 19931
diff changeset
   657
  apply unfold_locales
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19783
diff changeset
   658
  apply (rule assoc)
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19783
diff changeset
   659
  apply (rule rone)
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19783
diff changeset
   660
  apply (rule rinv)
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19783
diff changeset
   661
  done
17139
165c97f9bb63 Printing of interpretations: option to show witness theorems;
ballarin
parents: 17096
diff changeset
   662
17033
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   663
interpretation R2: Rqlgrp ["op #" "rone" "rinv"] 
19984
29bb4659f80a Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents: 19931
diff changeset
   664
  apply unfold_locales  (* FIXME: unfold_locales is too eager and shouldn't
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19783
diff changeset
   665
                          solve this. *)
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19783
diff changeset
   666
  done
17033
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   667
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   668
print_interps Rqsemi
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   669
print_interps Rqlgrp
17139
165c97f9bb63 Printing of interpretations: option to show witness theorems;
ballarin
parents: 17096
diff changeset
   670
print_interps Rplgrp  (* no interpretations yet *)
165c97f9bb63 Printing of interpretations: option to show witness theorems;
ballarin
parents: 17096
diff changeset
   671
17033
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   672
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   673
interpretation Rqlgrp < Rqrgrp
19984
29bb4659f80a Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents: 19931
diff changeset
   674
  proof unfold_locales
17033
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   675
    {
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   676
      fix x
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   677
      have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   678
      then show "x ** one = x" by (simp add: assoc lcancel)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   679
    }
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   680
    note rone = this
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   681
    {
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   682
      fix x
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   683
      have "inv(x) ** x ** inv(x) = inv(x) ** one"
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   684
	by (simp add: linv lone rone)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   685
      then show "x ** inv(x) = one" by (simp add: assoc lcancel)
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   686
    }
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   687
  qed
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   688
17139
165c97f9bb63 Printing of interpretations: option to show witness theorems;
ballarin
parents: 17096
diff changeset
   689
print_interps! Rqrgrp
165c97f9bb63 Printing of interpretations: option to show witness theorems;
ballarin
parents: 17096
diff changeset
   690
print_interps! Rpsemi  (* witness must not have meta hyps *)
165c97f9bb63 Printing of interpretations: option to show witness theorems;
ballarin
parents: 17096
diff changeset
   691
print_interps! Rprgrp  (* witness must not have meta hyps *)
165c97f9bb63 Printing of interpretations: option to show witness theorems;
ballarin
parents: 17096
diff changeset
   692
print_interps! Rplgrp  (* witness must not have meta hyps *)
165c97f9bb63 Printing of interpretations: option to show witness theorems;
ballarin
parents: 17096
diff changeset
   693
thm R2.rcancel
165c97f9bb63 Printing of interpretations: option to show witness theorems;
ballarin
parents: 17096
diff changeset
   694
thm R2.lcancel
165c97f9bb63 Printing of interpretations: option to show witness theorems;
ballarin
parents: 17096
diff changeset
   695
165c97f9bb63 Printing of interpretations: option to show witness theorems;
ballarin
parents: 17096
diff changeset
   696
ML {* check_thm "R2.rcancel"; check_thm "R2.lcancel" *}
165c97f9bb63 Printing of interpretations: option to show witness theorems;
ballarin
parents: 17096
diff changeset
   697
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   698
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   699
subsection {* Generation of Witness Theorems for Transitive Interpretations *}
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   700
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   701
locale Rtriv = var x +
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   702
  assumes x: "x = x"
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
locale Rtriv2 = var x + var y +
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   705
  assumes x: "x = x" and y: "y = y"
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   706
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   707
interpretation Rtriv2 < Rtriv x
19984
29bb4659f80a Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents: 19931
diff changeset
   708
  apply unfold_locales
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   709
  apply (rule x)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   710
  done
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 y
19984
29bb4659f80a Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents: 19931
diff changeset
   713
  apply unfold_locales
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   714
  apply (rule y)
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
print_locale Rtriv2
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   718
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   719
locale Rtriv3 = var x + var y + var z +
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   720
  assumes x: "x = x" and y: "y = y" and z: "z = z"
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
interpretation Rtriv3 < Rtriv2 x y
19984
29bb4659f80a Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents: 19931
diff changeset
   723
  apply unfold_locales
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   724
  apply (rule x)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   725
  apply (rule y)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   726
  done
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   727
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   728
print_locale Rtriv3
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   729
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   730
interpretation Rtriv3 < Rtriv2 x z
19984
29bb4659f80a Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents: 19931
diff changeset
   731
  apply unfold_locales
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   732
  apply (rule x_y_z.x)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   733
  apply (rule z)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   734
  done
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   735
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   736
ML {* set show_types *}
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   737
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   738
print_locale Rtriv3
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   739
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
subsection {* Normalisation Replaces Assumed Element by Derived Element *}
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
typedecl ('a, 'b) pair
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   744
arities pair :: ("term", "term") "term"
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
consts
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   747
  pair :: "['a, 'b] => ('a, 'b) pair"
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   748
  fst :: "('a, 'b) pair => 'a"
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   749
  snd :: "('a, 'b) pair => 'b"
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
axioms
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   752
  fst [simp]: "fst(pair(x, y)) = x"
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   753
  snd [simp]: "snd(pair(x, y)) = y"
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   754
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   755
locale Rpair = var prod (infixl "**" 65) + var prodP (infixl "***" 65) +
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   756
  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
   757
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   758
locale Rpair_semi = Rpair + Rpsemi
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
interpretation Rpair_semi < Rpsemi prodP (infixl "***" 65)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   761
proof (rule Rpsemi.intro)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   762
  fix x y z
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   763
  show "(x *** y) *** z = x *** (y *** z)"
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19783
diff changeset
   764
    apply (simp only: P_def) apply (simp add: assoc) (* FIXME: unfold P_def fails *)
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19783
diff changeset
   765
    done
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   766
qed
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   767
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   768
locale Rsemi_rev = Rpsemi + var rprod (infixl "++" 65) +
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   769
  defines r_def: "x ++ y == y ** x"
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   770
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   771
lemma (in Rsemi_rev) r_assoc:
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   772
  "(x ++ y) ++ z = x ++ (y ++ z)"
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   773
  by (simp add: r_def assoc)
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 Rpair_semi)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   776
  includes Rsemi_rev prodP (infixl "***" 65) rprodP (infixl "+++" 65)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   777
  constrains prod :: "['a, 'a] => 'a"
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   778
    and rprodP :: "[('a, 'a) pair, ('a, 'a) pair] => ('a, 'a) pair"
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   779
  shows "(x +++ y) +++ z = x +++ (y +++ z)"
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   780
  apply (rule r_assoc) done
17033
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   781
20469
bb75c1cdf913 More locale test code.
ballarin
parents: 20034
diff changeset
   782
bb75c1cdf913 More locale test code.
ballarin
parents: 20034
diff changeset
   783
subsection {* Import of Locales with Predicates as Interpretation *}
bb75c1cdf913 More locale test code.
ballarin
parents: 20034
diff changeset
   784
bb75c1cdf913 More locale test code.
ballarin
parents: 20034
diff changeset
   785
locale Ra =
bb75c1cdf913 More locale test code.
ballarin
parents: 20034
diff changeset
   786
  assumes Ra: "True"
bb75c1cdf913 More locale test code.
ballarin
parents: 20034
diff changeset
   787
bb75c1cdf913 More locale test code.
ballarin
parents: 20034
diff changeset
   788
locale Rb = Ra +
bb75c1cdf913 More locale test code.
ballarin
parents: 20034
diff changeset
   789
  assumes Rb: "True"
bb75c1cdf913 More locale test code.
ballarin
parents: 20034
diff changeset
   790
bb75c1cdf913 More locale test code.
ballarin
parents: 20034
diff changeset
   791
locale Rc = Rb +
bb75c1cdf913 More locale test code.
ballarin
parents: 20034
diff changeset
   792
  assumes Rc: "True"
bb75c1cdf913 More locale test code.
ballarin
parents: 20034
diff changeset
   793
bb75c1cdf913 More locale test code.
ballarin
parents: 20034
diff changeset
   794
print_locale! Rc
bb75c1cdf913 More locale test code.
ballarin
parents: 20034
diff changeset
   795
22659
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   796
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   797
section {* Interpretation of Defined Concepts *}
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   798
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   799
text {* Naming convention for global objects: prefixes D and d *}
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   800
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   801
locale Da = fixes a :: o
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   802
  assumes true: a
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   803
22757
d3298d63b7b6 Interpretation equations applied to attributes
ballarin
parents: 22659
diff changeset
   804
text {* In the following examples, @{term "~ a"} is the defined concept. *}
d3298d63b7b6 Interpretation equations applied to attributes
ballarin
parents: 22659
diff changeset
   805
22659
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   806
lemma (in Da) not_false: "~ a <-> False"
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   807
  apply simp apply (rule true) done
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   808
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   809
interpretation D1: Da ["True"]
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   810
  where "~ True" = "False"
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   811
  apply -
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   812
  apply unfold_locales [1] apply rule
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   813
  by simp
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   814
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   815
thm D1.not_false
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   816
lemma "False <-> False" apply (rule D1.not_false) done
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   817
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   818
interpretation D2: Da ["x | ~ x"]
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   819
  where "~ (x | ~ x)" = "~ x & x"
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   820
  apply -
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   821
  apply unfold_locales [1] apply fast
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   822
  by simp
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   823
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   824
thm D2.not_false
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   825
lemma "~ x & x <-> False" apply (rule D2.not_false) done
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   826
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   827
print_interps! Da
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   828
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   829
(* Subscriptions of interpretations *)
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   830
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   831
lemma (in Da) not_false2: "~a <-> False"
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   832
  apply simp apply (rule true) done
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   833
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   834
thm D1.not_false2 D2.not_false2
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   835
lemma "False <-> False" apply (rule D1.not_false2) done
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   836
lemma "~x & x <-> False" apply (rule D2.not_false2) done
f792579b6e59 Experimental code for the interpretation of definitions.
ballarin
parents: 20469
diff changeset
   837
22757
d3298d63b7b6 Interpretation equations applied to attributes
ballarin
parents: 22659
diff changeset
   838
(* Unfolding in attributes *)
d3298d63b7b6 Interpretation equations applied to attributes
ballarin
parents: 22659
diff changeset
   839
d3298d63b7b6 Interpretation equations applied to attributes
ballarin
parents: 22659
diff changeset
   840
locale Db = Da +
d3298d63b7b6 Interpretation equations applied to attributes
ballarin
parents: 22659
diff changeset
   841
  fixes b :: o
d3298d63b7b6 Interpretation equations applied to attributes
ballarin
parents: 22659
diff changeset
   842
  assumes a_iff_b: "~a <-> b"
d3298d63b7b6 Interpretation equations applied to attributes
ballarin
parents: 22659
diff changeset
   843
d3298d63b7b6 Interpretation equations applied to attributes
ballarin
parents: 22659
diff changeset
   844
lemmas (in Db) not_false_b = not_false [unfolded a_iff_b]
d3298d63b7b6 Interpretation equations applied to attributes
ballarin
parents: 22659
diff changeset
   845
d3298d63b7b6 Interpretation equations applied to attributes
ballarin
parents: 22659
diff changeset
   846
interpretation D2: Db ["x | ~ x" "~ (x <-> x)"]
d3298d63b7b6 Interpretation equations applied to attributes
ballarin
parents: 22659
diff changeset
   847
  apply unfold_locales apply fast done
d3298d63b7b6 Interpretation equations applied to attributes
ballarin
parents: 22659
diff changeset
   848
d3298d63b7b6 Interpretation equations applied to attributes
ballarin
parents: 22659
diff changeset
   849
thm D2.not_false_b
d3298d63b7b6 Interpretation equations applied to attributes
ballarin
parents: 22659
diff changeset
   850
lemma "~(x <-> x) <-> False" apply (rule D2.not_false_b) done
d3298d63b7b6 Interpretation equations applied to attributes
ballarin
parents: 22659
diff changeset
   851
d3298d63b7b6 Interpretation equations applied to attributes
ballarin
parents: 22659
diff changeset
   852
(* Subscription and attributes *)
d3298d63b7b6 Interpretation equations applied to attributes
ballarin
parents: 22659
diff changeset
   853
d3298d63b7b6 Interpretation equations applied to attributes
ballarin
parents: 22659
diff changeset
   854
lemmas (in Db) not_false_b2 = not_false [unfolded a_iff_b]
d3298d63b7b6 Interpretation equations applied to attributes
ballarin
parents: 22659
diff changeset
   855
d3298d63b7b6 Interpretation equations applied to attributes
ballarin
parents: 22659
diff changeset
   856
thm D2.not_false_b2
d3298d63b7b6 Interpretation equations applied to attributes
ballarin
parents: 22659
diff changeset
   857
lemma "~(x <-> x) <-> False" apply (rule D2.not_false_b2) done
d3298d63b7b6 Interpretation equations applied to attributes
ballarin
parents: 22659
diff changeset
   858
15596
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
   859
end