src/FOL/ex/LocaleTest.thy
author ballarin
Wed, 09 Mar 2005 18:44:52 +0100
changeset 15596 8665d08085df
child 15598 4ab52355bb53
permissions -rw-r--r--
First version of global registration command.
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
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
     9
header {* Test of Locale instantiation *}
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    10
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    11
theory LocaleTest = FOL:
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    12
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    13
(* registration input syntax *)
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    14
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    15
locale L
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    16
locale M = fixes a and b and c
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    17
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    18
registration test [simp]: L + M a b c [x y z] .
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    19
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    20
print_registrations L
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    21
print_registrations M
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    22
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    23
registration test [simp]: L .
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    24
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    25
registration L .
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    26
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    27
(* processing of locale expression *)
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    28
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    29
ML {* reset show_hyps *}
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    30
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    31
locale A = fixes a assumes asm_A: "a = a"
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    32
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    33
locale (open) B = fixes b assumes asm_B [simp]: "b = b"
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    34
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    35
locale C = A + B + assumes asm_C: "c = c"
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    36
  (* TODO: independent type var in c, prohibit locale declaration *)
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    37
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    38
locale D = A + B + fixes d defines def_D: "d == (a = b)"
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    39
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    40
ML {* set show_sorts *}
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    41
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    42
typedecl i
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    43
arities i :: "term"
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    44
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    45
ML {* set Toplevel.debug *}
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    46
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    47
registration p1: C ["X::'b" "Y"] by (auto intro: A.intro C_axioms.intro)
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    48
  (* both X and Y get type 'b since 'b is the internal type of parameter b,
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    49
     not wanted, but put up with for now. *)
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    50
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    51
ML {* set show_hyps *}
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    52
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    53
print_registrations A
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    54
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    55
(* thm asm_A a.asm_A p1.a.asm_A *)
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    56
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    57
(*
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    58
registration p2: D [X Y Z] sorry
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    59
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    60
print_registrations D
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    61
*)
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    62
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    63
registration p3: D [X Y] by (auto intro: A.intro)
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    64
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    65
print_registrations A
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    66
print_registrations B
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    67
print_registrations C
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    68
print_registrations D
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    69
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    70
(* not permitted
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    71
registration p4: A ["?x10"] apply (rule A.intro) apply rule done
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    72
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    73
print_registrations A
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    74
*)
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    75
8665d08085df First version of global registration command.
ballarin
parents:
diff changeset
    76
end