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