src/FOL/ex/LocaleTest.thy
author ballarin
Thu Mar 24 17:03:37 2005 +0100 (2005-03-24 ago)
changeset 15624 484178635bd8
parent 15598 4ab52355bb53
child 15696 1da4ce092c0b
permissions -rw-r--r--
Further work on interpretation commands. New command `interpret' for
interpretation in proof contexts.
ballarin@15596
     1
(*  Title:      FOL/ex/LocaleTest.thy
ballarin@15596
     2
    ID:         $Id$
ballarin@15596
     3
    Author:     Clemens Ballarin
ballarin@15596
     4
    Copyright (c) 2005 by Clemens Ballarin
ballarin@15596
     5
ballarin@15596
     6
Collection of regression tests for locales.
ballarin@15596
     7
*)
ballarin@15596
     8
ballarin@15596
     9
header {* Test of Locale instantiation *}
ballarin@15596
    10
ballarin@15596
    11
theory LocaleTest = FOL:
ballarin@15596
    12
ballarin@15598
    13
(* interpretation input syntax *)
ballarin@15596
    14
ballarin@15596
    15
locale L
ballarin@15596
    16
locale M = fixes a and b and c
ballarin@15596
    17
ballarin@15598
    18
interpretation test [simp]: L + M a b c [x y z] .
ballarin@15596
    19
ballarin@15598
    20
print_interps L
ballarin@15598
    21
print_interps M
ballarin@15596
    22
ballarin@15624
    23
interpretation test [simp]: L print_interps M .
ballarin@15596
    24
ballarin@15598
    25
interpretation L .
ballarin@15596
    26
ballarin@15596
    27
(* processing of locale expression *)
ballarin@15596
    28
ballarin@15596
    29
ML {* reset show_hyps *}
ballarin@15596
    30
ballarin@15596
    31
locale A = fixes a assumes asm_A: "a = a"
ballarin@15596
    32
ballarin@15596
    33
locale (open) B = fixes b assumes asm_B [simp]: "b = b"
ballarin@15596
    34
ballarin@15596
    35
locale C = A + B + assumes asm_C: "c = c"
ballarin@15596
    36
  (* TODO: independent type var in c, prohibit locale declaration *)
ballarin@15596
    37
ballarin@15596
    38
locale D = A + B + fixes d defines def_D: "d == (a = b)"
ballarin@15596
    39
ballarin@15596
    40
ML {* set show_sorts *}
ballarin@15596
    41
ballarin@15596
    42
typedecl i
ballarin@15596
    43
arities i :: "term"
ballarin@15596
    44
ballarin@15596
    45
ML {* set Toplevel.debug *}
ballarin@15596
    46
ballarin@15598
    47
ML {* set show_hyps *}
ballarin@15598
    48
ballarin@15598
    49
interpretation p1: C ["X::'b" "Y::'b"] by (auto intro: A.intro C_axioms.intro)
ballarin@15596
    50
  (* both X and Y get type 'b since 'b is the internal type of parameter b,
ballarin@15596
    51
     not wanted, but put up with for now. *)
ballarin@15596
    52
ballarin@15598
    53
print_interps A
ballarin@15596
    54
ballarin@15624
    55
(* possible accesses
ballarin@15624
    56
thm p1.a.asm_A thm LocaleTest.p1.a.asm_A
ballarin@15624
    57
thm LocaleTest.asm_A thm p1.asm_A
ballarin@15624
    58
*)
ballarin@15624
    59
ballarin@15624
    60
(* without prefix *)
ballarin@15624
    61
ballarin@15624
    62
interpretation C ["W::'b" "Z::'b"] by (auto intro: A.intro C_axioms.intro)
ballarin@15624
    63
ballarin@15624
    64
print_interps A
ballarin@15624
    65
ballarin@15624
    66
(* possible accesses
ballarin@15624
    67
thm a.asm_A thm asm_A thm LocaleTest.a.asm_A thm LocaleTest.asm_A
ballarin@15598
    68
*)
ballarin@15598
    69
ballarin@15598
    70
interpretation p2: D [X Y "Y = X"] by (auto intro: A.intro simp: eq_commute)
ballarin@15596
    71
ballarin@15598
    72
print_interps D
ballarin@15598
    73
ballarin@15598
    74
(*
ballarin@15598
    75
thm p2.a.asm_A
ballarin@15596
    76
*)
ballarin@15596
    77
ballarin@15624
    78
interpretation p3: D [X Y] .
ballarin@15598
    79
ballarin@15598
    80
(* duplicate: not registered *)
ballarin@15598
    81
(*
ballarin@15598
    82
thm p3.a.asm_A
ballarin@15598
    83
*)
ballarin@15596
    84
ballarin@15598
    85
print_interps A
ballarin@15598
    86
print_interps B
ballarin@15598
    87
print_interps C
ballarin@15598
    88
print_interps D
ballarin@15596
    89
ballarin@15598
    90
(* not permitted *)
ballarin@15598
    91
(*
ballarin@15598
    92
interpretation p4: A ["x::?'a1"] apply (rule A.intro) apply rule done
ballarin@15598
    93
*)
ballarin@15598
    94
print_interps A
ballarin@15596
    95
ballarin@15598
    96
(* without a prefix *)
ballarin@15598
    97
(* TODO!!!
ballarin@15598
    98
interpretation A [Z] apply - apply (auto intro: A.intro) done
ballarin@15596
    99
*)
ballarin@15596
   100
ballarin@15624
   101
theorem True
ballarin@15624
   102
proof -
ballarin@15624
   103
  fix alpha::i and beta::i and gamma::i
ballarin@15624
   104
  assume "A(alpha)"
ballarin@15624
   105
  then interpret p5: A [alpha] .
ballarin@15624
   106
  print_interps A
ballarin@15624
   107
  interpret p6: C [alpha beta] by (auto intro: C_axioms.intro)
ballarin@15624
   108
  print_interps A   (* p6 not added! *)
ballarin@15624
   109
  print_interps C
ballarin@15624
   110
qed rule
ballarin@15624
   111
ballarin@15624
   112
(* lemma "bla.bla": True by rule *)
ballarin@15624
   113
ballarin@15624
   114
ballarin@15596
   115
end