|
1 (* Title: HOL/ex/LocaleTest2.thy |
|
2 ID: $Id$ |
|
3 Author: Clemens Ballarin |
|
4 Copyright (c) 2007 by Clemens Ballarin |
|
5 |
|
6 More regression tests for locales. |
|
7 Definitions are less natural in FOL, since there is no selection operator. |
|
8 Hence we do them in HOL, not in the main test suite for locales: |
|
9 FOL/ex/LocaleTest.thy |
|
10 *) |
|
11 |
|
12 header {* Test of Locale Interpretation *} |
|
13 |
|
14 theory LocaleTest2 |
|
15 imports Main |
|
16 begin |
|
17 |
|
18 ML {* set quick_and_dirty *} (* allow for thm command in batch mode *) |
|
19 ML {* set Toplevel.debug *} |
|
20 ML {* set show_hyps *} |
|
21 ML {* set show_sorts *} |
|
22 |
|
23 section {* Interpretation of Defined Concepts *} |
|
24 |
|
25 text {* Naming convention for global objects: prefixes D and d *} |
|
26 |
|
27 (* Group example with defined operation inv *) |
|
28 |
|
29 locale Dsemi = |
|
30 fixes prod (infixl "**" 65) |
|
31 assumes assoc: "(x ** y) ** z = x ** (y ** z)" |
|
32 |
|
33 locale Dmonoid = Dsemi + |
|
34 fixes one |
|
35 assumes lone: "one ** x = x" |
|
36 and rone: "x ** one = x" |
|
37 |
|
38 definition (in Dmonoid) |
|
39 inv where "inv(x) == THE y. x ** y = one & y ** x = one" |
|
40 |
|
41 lemma (in Dmonoid) inv_unique: |
|
42 assumes eq: "y ** x = one" "x ** y' = one" |
|
43 shows "y = y'" |
|
44 proof - |
|
45 from eq have "y = y ** (x ** y')" by (simp add: rone) |
|
46 also have "... = (y ** x) ** y'" by (simp add: assoc) |
|
47 also from eq have "... = y'" by (simp add: lone) |
|
48 finally show ?thesis . |
|
49 qed |
|
50 |
|
51 locale Dgrp = Dmonoid + |
|
52 assumes linv_ex: "EX y. y ** x = one" |
|
53 and rinv_ex: "EX y. x ** y = one" |
|
54 |
|
55 lemma (in Dgrp) linv: |
|
56 "inv x ** x = one" |
|
57 apply (unfold inv_def) |
|
58 apply (insert rinv_ex [where x = x]) |
|
59 apply (insert linv_ex [where x = x]) |
|
60 apply (erule exE) apply (erule exE) |
|
61 apply (rule theI2) |
|
62 apply rule apply assumption |
|
63 apply (frule inv_unique, assumption) |
|
64 apply simp |
|
65 apply (rule inv_unique) |
|
66 apply fast+ |
|
67 done |
|
68 |
|
69 lemma (in Dgrp) rinv: |
|
70 "x ** inv x = one" |
|
71 apply (unfold inv_def) |
|
72 apply (insert rinv_ex [where x = x]) |
|
73 apply (insert linv_ex [where x = x]) |
|
74 apply (erule exE) apply (erule exE) |
|
75 apply (rule theI2) |
|
76 apply rule apply assumption |
|
77 apply (frule inv_unique, assumption) |
|
78 apply simp |
|
79 apply (rule inv_unique) |
|
80 apply fast+ |
|
81 done |
|
82 |
|
83 lemma (in Dgrp) lcancel: |
|
84 "x ** y = x ** z <-> y = z" |
|
85 proof |
|
86 assume "x ** y = x ** z" |
|
87 then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc) |
|
88 then show "y = z" by (simp add: lone linv) |
|
89 qed simp |
|
90 |
|
91 interpretation Dint: Dmonoid ["op +" "0::int"] |
|
92 where "Dmonoid.inv (op +) (0::int)" = "uminus" |
|
93 proof - |
|
94 show "Dmonoid (op +) (0::int)" by unfold_locales auto |
|
95 note Dint = this (* should have this as an assumption in further goals *) |
|
96 { |
|
97 fix x |
|
98 have "Dmonoid.inv (op +) (0::int) x = - x" |
|
99 by (auto simp: Dmonoid.inv_def [OF Dint]) |
|
100 } |
|
101 then show "Dmonoid.inv (op +) (0::int) == uminus" |
|
102 by (rule_tac eq_reflection) (fast intro: ext) |
|
103 qed |
|
104 |
|
105 thm Dmonoid.inv_def Dint.inv_def |
|
106 |
|
107 lemma "- x \<equiv> THE y. x + y = 0 \<and> y + x = (0::int)" |
|
108 apply (rule Dint.inv_def) done |
|
109 |
|
110 interpretation Dclass: Dmonoid ["op +" "0::'a::ab_group_add"] |
|
111 where "Dmonoid.inv (op +) (0::'a::ab_group_add)" = "uminus" |
|
112 proof - |
|
113 show "Dmonoid (op +) (0::'b::ab_group_add)" by unfold_locales auto |
|
114 note Dclass = this (* should have this as an assumption in further goals *) |
|
115 { |
|
116 fix x |
|
117 have "Dmonoid.inv (op +) (0::'b::ab_group_add) x = - x" |
|
118 by (auto simp: Dmonoid.inv_def [OF Dclass] equals_zero_I [symmetric]) |
|
119 } |
|
120 then show "Dmonoid.inv (op +) (0::'b::ab_group_add) == uminus" |
|
121 by (rule_tac eq_reflection) (fast intro: ext) |
|
122 qed |
|
123 |
|
124 interpretation Dclass: Dgrp ["op +" "0::'a::ring"] |
|
125 apply unfold_locales |
|
126 apply (rule_tac x="-x" in exI) apply simp |
|
127 apply (rule_tac x="-x" in exI) apply simp |
|
128 done |
|
129 |
|
130 (* Equation for inverse from Dclass: Dmonoid effective. *) |
|
131 |
|
132 thm Dclass.linv |
|
133 lemma "-x + x = (0::'a::ring)" apply (rule Dclass.linv) done |
|
134 |
|
135 (* Equations have effect in "subscriptions" *) |
|
136 |
|
137 (* In the same module *) |
|
138 |
|
139 lemma (in Dmonoid) trivial: |
|
140 "inv one = inv one" |
|
141 by rule |
|
142 |
|
143 thm Dclass.trivial |
|
144 |
|
145 (* Inherited: interpretation *) |
|
146 |
|
147 lemma (in Dgrp) inv_inv: |
|
148 "inv (inv x) = x" |
|
149 proof - |
|
150 have "inv x ** inv (inv x) = inv x ** x" |
|
151 by (simp add: linv rinv) |
|
152 then show ?thesis by (simp add: lcancel) |
|
153 qed |
|
154 |
|
155 thm Dclass.inv_inv |
|
156 lemma "- (- x) = (x::'a::ring)" |
|
157 apply (rule Dclass.inv_inv) done |
|
158 |
|
159 end |