|
1 (* Title: FOL/ex/LocaleInst.thy |
|
2 ID: $Id$ |
|
3 Author: Clemens Ballarin |
|
4 Copyright (c) 2004 by Clemens Ballarin |
|
5 |
|
6 Test of locale instantiation mechanism, also provides a few examples. |
|
7 *) |
|
8 |
|
9 header {* Test of Locale instantiation *} |
|
10 |
|
11 theory LocaleInst = FOL: |
|
12 |
|
13 ML {* set show_hyps *} |
|
14 |
|
15 section {* Locale without assumptions *} |
|
16 |
|
17 locale L1 = notes rev_conjI [intro] = conjI [THEN iffD1 [OF conj_commute]] |
|
18 |
|
19 lemma "[| A; B |] ==> A & B" |
|
20 proof - |
|
21 instantiate my: L1 txt {* No chained fact required. *} |
|
22 assume B and A txt {* order reversed *} |
|
23 then show "A & B" .. |
|
24 txt {* Applies @{thm my.rev_conjI}. *} |
|
25 qed |
|
26 |
|
27 section {* Simple locale with assumptions *} |
|
28 |
|
29 typedecl i |
|
30 arities i :: "term" |
|
31 |
|
32 consts bin :: "[i, i] => i" (infixl "#" 60) |
|
33 |
|
34 axioms i_assoc: "(x # y) # z = x # (y # z)" |
|
35 i_comm: "x # y = y # x" |
|
36 |
|
37 locale L2 = |
|
38 fixes OP (infixl "+" 60) |
|
39 assumes assoc: "(x + y) + z = x + (y + z)" |
|
40 and comm: "x + y = y + x" |
|
41 |
|
42 lemma (in L2) lcomm: "x + (y + z) = y + (x + z)" |
|
43 proof - |
|
44 have "x + (y + z) = (x + y) + z" by (simp add: assoc) |
|
45 also have "... = (y + x) + z" by (simp add: comm) |
|
46 also have "... = y + (x + z)" by (simp add: assoc) |
|
47 finally show ?thesis . |
|
48 qed |
|
49 |
|
50 lemmas (in L2) AC = comm assoc lcomm |
|
51 |
|
52 lemma "(x::i) # y # z # w = y # x # w # z" |
|
53 proof - |
|
54 have "L2 (op #)" by (rule L2.intro [of "op #", OF i_assoc i_comm]) |
|
55 then instantiate my: L2 |
|
56 txt {* Chained fact required to discharge assumptions of @{text L2} |
|
57 and instantiate parameters. *} |
|
58 show ?thesis by (simp only: my.OP.AC) (* or simply AC *) |
|
59 qed |
|
60 |
|
61 section {* Nested locale with assumptions *} |
|
62 |
|
63 locale L3 = |
|
64 fixes OP (infixl "+" 60) |
|
65 assumes assoc: "(x + y) + z = x + (y + z)" |
|
66 |
|
67 locale L4 = L3 + |
|
68 assumes comm: "x + y = y + x" |
|
69 |
|
70 lemma (in L4) lcomm: "x + (y + z) = y + (x + z)" |
|
71 proof - |
|
72 have "x + (y + z) = (x + y) + z" by (simp add: assoc) |
|
73 also have "... = (y + x) + z" by (simp add: comm) |
|
74 also have "... = y + (x + z)" by (simp add: assoc) |
|
75 finally show ?thesis . |
|
76 qed |
|
77 |
|
78 lemmas (in L4) AC = comm assoc lcomm |
|
79 |
|
80 text {* Conceptually difficult locale: |
|
81 2nd context fragment contains facts with differing metahyps. *} |
|
82 |
|
83 lemma L4_intro: |
|
84 fixes OP (infixl "+" 60) |
|
85 assumes assoc: "!!x y z. (x + y) + z = x + (y + z)" |
|
86 and comm: "!!x y. x + y = y + x" |
|
87 shows "L4 (op+)" |
|
88 by (blast intro: L4.intro L3.intro assoc L4_axioms.intro comm) |
|
89 |
|
90 lemma "(x::i) # y # z # w = y # x # w # z" |
|
91 proof - |
|
92 have "L4 (op #)" by (rule L4_intro [of "op #", OF i_assoc i_comm]) |
|
93 then instantiate my: L4 |
|
94 show ?thesis by (simp only: my.OP.AC) (* or simply AC *) |
|
95 qed |
|
96 |
|
97 section {* Locale with definition *} |
|
98 |
|
99 text {* This example is admittedly not very creative :-) *} |
|
100 |
|
101 locale L5 = L4 + var A + |
|
102 defines A_def: "A == True" |
|
103 |
|
104 lemma (in L5) lem: A |
|
105 by (unfold A_def) rule |
|
106 |
|
107 lemma "L5(op #) ==> True" |
|
108 proof - |
|
109 assume "L5(op #)" |
|
110 then instantiate my: L5 |
|
111 show ?thesis by (rule lem) (* lem instantiated to True *) |
|
112 qed |
|
113 |
|
114 end |