author  ballarin 
Sat, 21 Nov 2009 17:39:54 +0100  
changeset 33837  a406f447abef 
parent 33836  da3e88ea6c72 
child 36089  8078d496582c 
permissions  rwrr 
30749  1 
(* Title: FOL/ex/LocaleTest.thy 
28873  2 
Author: Clemens Ballarin, TU Muenchen 
3 

30749  4 
Test environment for the locale implementation. 
28873  5 
*) 
6 

29357  7 
theory LocaleTest 
8 
imports FOL 

28873  9 
begin 
10 

11 
typedecl int arities int :: "term" 

12 
consts plus :: "int => int => int" (infixl "+" 60) 

13 
zero :: int ("0") 

14 
minus :: "int => int" (" _") 

15 

28993
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

16 
axioms 
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

17 
int_assoc: "(x + y::int) + z = x + (y + z)" 
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

18 
int_zero: "0 + x = x" 
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

19 
int_minus: "(x) + x = 0" 
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

20 
int_minus2: "(x) = x" 
28873  21 

29206  22 
section {* Inference of parameter types *} 
28873  23 

24 
locale param1 = fixes p 

25 
print_locale! param1 

26 

28881  27 
locale param2 = fixes p :: 'b 
28873  28 
print_locale! param2 
29 

30 
(* 

31 
locale param_top = param2 r for r :: "'b :: {}" 

28993
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

32 
Fails, cannot generalise parameter. 
28873  33 
*) 
34 

35 
locale param3 = fixes p (infix ".." 50) 

36 
print_locale! param3 

37 

38 
locale param4 = fixes p :: "'a => 'a => 'a" (infix ".." 50) 

39 
print_locale! param4 

40 

41 

29206  42 
subsection {* Incremental type constraints *} 
28873  43 

44 
locale constraint1 = 

45 
fixes prod (infixl "**" 65) 

46 
assumes l_id: "x ** y = x" 

47 
assumes assoc: "(x ** y) ** z = x ** (y ** z)" 

48 
print_locale! constraint1 

49 

50 
locale constraint2 = 

51 
fixes p and q 

52 
assumes "p = q" 

53 
print_locale! constraint2 

54 

55 

29206  56 
section {* Inheritance *} 
28873  57 

58 
locale semi = 

59 
fixes prod (infixl "**" 65) 

60 
assumes assoc: "(x ** y) ** z = x ** (y ** z)" 

61 
print_locale! semi thm semi_def 

62 

63 
locale lgrp = semi + 

64 
fixes one and inv 

65 
assumes lone: "one ** x = x" 

66 
and linv: "inv(x) ** x = one" 

67 
print_locale! lgrp thm lgrp_def lgrp_axioms_def 

68 

69 
locale add_lgrp = semi "op ++" for sum (infixl "++" 60) + 

70 
fixes zero and neg 

71 
assumes lzero: "zero ++ x = x" 

72 
and lneg: "neg(x) ++ x = zero" 

73 
print_locale! add_lgrp thm add_lgrp_def add_lgrp_axioms_def 

74 

75 
locale rev_lgrp = semi "%x y. y ++ x" for sum (infixl "++" 60) 

76 
print_locale! rev_lgrp thm rev_lgrp_def 

77 

78 
locale hom = f: semi f + g: semi g for f and g 

79 
print_locale! hom thm hom_def 

80 

81 
locale perturbation = semi + d: semi "%x y. delta(x) ** delta(y)" for delta 

82 
print_locale! perturbation thm perturbation_def 

83 

84 
locale pert_hom = d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2 

85 
print_locale! pert_hom thm pert_hom_def 

86 

87 
text {* Alternative expression, obtaining nicer names in @{text "semi f"}. *} 

88 
locale pert_hom' = semi f + d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2 

89 
print_locale! pert_hom' thm pert_hom'_def 

90 

91 

29206  92 
section {* Syntax declarations *} 
28873  93 

94 
locale logic = 

95 
fixes land (infixl "&&" 55) 

96 
and lnot (" _" [60] 60) 

97 
assumes assoc: "(x && y) && z = x && (y && z)" 

98 
and notnot: " ( x) = x" 

99 
begin 

100 

101 
definition lor (infixl "" 50) where 

102 
"x  y = ( x &&  y)" 

103 

104 
end 

105 
print_locale! logic 

106 

107 
locale use_decl = logic + semi "op " 

108 
print_locale! use_decl thm use_decl_def 

109 

29251  110 
locale extra_type = 
111 
fixes a :: 'a 

112 
and P :: "'a => 'b => o" 

113 
begin 

114 

115 
definition test :: "'a => o" where 

116 
"test(x) <> (ALL b. P(x, b))" 

117 

118 
end 

119 

120 
term extra_type.test thm extra_type.test_def 

121 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29513
diff
changeset

122 
interpretation var?: extra_type "0" "%x y. x = 0" . 
29251  123 

124 
thm var.test_def 

125 

28881  126 

33460
6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

127 
text {* Under which circumstances term syntax remains active. *} 
6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

128 

6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

129 
locale "syntax" = 
6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

130 
fixes p1 :: "'a => 'b" 
6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

131 
and p2 :: "'b => o" 
6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

132 
begin 
6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

133 

6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

134 
definition d1 :: "'a => o" where "d1(x) <> ~ p2(p1(x))" 
6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

135 
definition d2 :: "'b => o" where "d2(x) <> ~ p2(x)" 
6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

136 

6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

137 
thm d1_def d2_def 
6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

138 

6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

139 
end 
6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

140 

6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

141 
thm syntax.d1_def syntax.d2_def 
6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

142 

6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

143 
locale syntax' = "syntax" p1 p2 for p1 :: "'a => 'a" and p2 :: "'a => o" 
6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

144 
begin 
6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

145 

6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

146 
thm d1_def d2_def (* should print as "d1(?x) <> ..." and "d2(?x) <> ..." *) 
6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

147 

6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

148 
ML {* 
33462
ddcf2004e215
Use PrintMode.setmp to make threadsafe; avoid code clones.
ballarin
parents:
33461
diff
changeset

149 
fun check_syntax ctxt thm expected = 
ddcf2004e215
Use PrintMode.setmp to make threadsafe; avoid code clones.
ballarin
parents:
33461
diff
changeset

150 
let 
ddcf2004e215
Use PrintMode.setmp to make threadsafe; avoid code clones.
ballarin
parents:
33461
diff
changeset

151 
val obtained = PrintMode.setmp [] (Display.string_of_thm ctxt) thm; 
ddcf2004e215
Use PrintMode.setmp to make threadsafe; avoid code clones.
ballarin
parents:
33461
diff
changeset

152 
in 
ddcf2004e215
Use PrintMode.setmp to make threadsafe; avoid code clones.
ballarin
parents:
33461
diff
changeset

153 
if obtained <> expected 
ddcf2004e215
Use PrintMode.setmp to make threadsafe; avoid code clones.
ballarin
parents:
33461
diff
changeset

154 
then error ("Theorem syntax '" ^ obtained ^ "' obtained, but '" ^ expected ^ "' expected.") 
ddcf2004e215
Use PrintMode.setmp to make threadsafe; avoid code clones.
ballarin
parents:
33461
diff
changeset

155 
else () 
ddcf2004e215
Use PrintMode.setmp to make threadsafe; avoid code clones.
ballarin
parents:
33461
diff
changeset

156 
end; 
ddcf2004e215
Use PrintMode.setmp to make threadsafe; avoid code clones.
ballarin
parents:
33461
diff
changeset

157 
*} 
ddcf2004e215
Use PrintMode.setmp to make threadsafe; avoid code clones.
ballarin
parents:
33461
diff
changeset

158 

ddcf2004e215
Use PrintMode.setmp to make threadsafe; avoid code clones.
ballarin
parents:
33461
diff
changeset

159 
ML {* 
ddcf2004e215
Use PrintMode.setmp to make threadsafe; avoid code clones.
ballarin
parents:
33461
diff
changeset

160 
check_syntax @{context} @{thm d1_def} "d1(?x) <> ~ p2(p1(?x))"; 
ddcf2004e215
Use PrintMode.setmp to make threadsafe; avoid code clones.
ballarin
parents:
33461
diff
changeset

161 
check_syntax @{context} @{thm d2_def} "d2(?x) <> ~ p2(?x)"; 
33460
6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

162 
*} 
6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

163 

6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

164 
end 
6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

165 

6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

166 
locale syntax'' = "syntax" p3 p2 for p3 :: "'a => 'b" and p2 :: "'b => o" 
6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

167 
begin 
6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

168 

6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

169 
thm d1_def d2_def 
6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

170 
(* should print as "syntax.d1(p3, p2, ?x) <> ..." and "d2(?x) <> ..." *) 
6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

171 

6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

172 
ML {* 
33462
ddcf2004e215
Use PrintMode.setmp to make threadsafe; avoid code clones.
ballarin
parents:
33461
diff
changeset

173 
check_syntax @{context} @{thm d1_def} "syntax.d1(p3, p2, ?x) <> ~ p2(p3(?x))"; 
ddcf2004e215
Use PrintMode.setmp to make threadsafe; avoid code clones.
ballarin
parents:
33461
diff
changeset

174 
check_syntax @{context} @{thm d2_def} "d2(?x) <> ~ p2(?x)"; 
33460
6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

175 
*} 
6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

176 

6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

177 
end 
6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

178 

6c273b0e0e26
Relax on type agreement with original context when applying term syntax.
ballarin
parents:
32802
diff
changeset

179 

29206  180 
section {* Foundational versions of theorems *} 
29028
b5dad96c755a
When adding locales, delay notes until local theory is built.
ballarin
parents:
29022
diff
changeset

181 

b5dad96c755a
When adding locales, delay notes until local theory is built.
ballarin
parents:
29022
diff
changeset

182 
thm logic.assoc 
b5dad96c755a
When adding locales, delay notes until local theory is built.
ballarin
parents:
29022
diff
changeset

183 
thm logic.lor_def 
b5dad96c755a
When adding locales, delay notes until local theory is built.
ballarin
parents:
29022
diff
changeset

184 

b5dad96c755a
When adding locales, delay notes until local theory is built.
ballarin
parents:
29022
diff
changeset

185 

29206  186 
section {* Defines *} 
29019  187 

188 
locale logic_def = 

189 
fixes land (infixl "&&" 55) 

190 
and lor (infixl "" 50) 

191 
and lnot (" _" [60] 60) 

192 
assumes assoc: "(x && y) && z = x && (y && z)" 

193 
and notnot: " ( x) = x" 

29022  194 
defines "x  y == ( x &&  y)" 
29021
ce100fbc3c8e
Proper shape of assumptions generated from Defines elements.
ballarin
parents:
29019
diff
changeset

195 
begin 
29019  196 

29031
e74341997a48
Pass on defines in inheritance; reject illicit defines created by instantiation.
ballarin
parents:
29028
diff
changeset

197 
thm lor_def 
e74341997a48
Pass on defines in inheritance; reject illicit defines created by instantiation.
ballarin
parents:
29028
diff
changeset

198 

29021
ce100fbc3c8e
Proper shape of assumptions generated from Defines elements.
ballarin
parents:
29019
diff
changeset

199 
lemma "x  y = ( x && y)" 
ce100fbc3c8e
Proper shape of assumptions generated from Defines elements.
ballarin
parents:
29019
diff
changeset

200 
by (unfold lor_def) (rule refl) 
ce100fbc3c8e
Proper shape of assumptions generated from Defines elements.
ballarin
parents:
29019
diff
changeset

201 

ce100fbc3c8e
Proper shape of assumptions generated from Defines elements.
ballarin
parents:
29019
diff
changeset

202 
end 
ce100fbc3c8e
Proper shape of assumptions generated from Defines elements.
ballarin
parents:
29019
diff
changeset

203 

29031
e74341997a48
Pass on defines in inheritance; reject illicit defines created by instantiation.
ballarin
parents:
29028
diff
changeset

204 
(* Inheritance of defines *) 
e74341997a48
Pass on defines in inheritance; reject illicit defines created by instantiation.
ballarin
parents:
29028
diff
changeset

205 

e74341997a48
Pass on defines in inheritance; reject illicit defines created by instantiation.
ballarin
parents:
29028
diff
changeset

206 
locale logic_def2 = logic_def 
e74341997a48
Pass on defines in inheritance; reject illicit defines created by instantiation.
ballarin
parents:
29028
diff
changeset

207 
begin 
e74341997a48
Pass on defines in inheritance; reject illicit defines created by instantiation.
ballarin
parents:
29028
diff
changeset

208 

e74341997a48
Pass on defines in inheritance; reject illicit defines created by instantiation.
ballarin
parents:
29028
diff
changeset

209 
lemma "x  y = ( x && y)" 
e74341997a48
Pass on defines in inheritance; reject illicit defines created by instantiation.
ballarin
parents:
29028
diff
changeset

210 
by (unfold lor_def) (rule refl) 
e74341997a48
Pass on defines in inheritance; reject illicit defines created by instantiation.
ballarin
parents:
29028
diff
changeset

211 

e74341997a48
Pass on defines in inheritance; reject illicit defines created by instantiation.
ballarin
parents:
29028
diff
changeset

212 
end 
29019  213 

29035  214 

29206  215 
section {* Notes *} 
29035  216 

217 
(* A somewhat arcane homomorphism example *) 

218 

219 
definition semi_hom where 

220 
"semi_hom(prod, sum, h) <> (ALL x y. h(prod(x, y)) = sum(h(x), h(y)))" 

221 

222 
lemma semi_hom_mult: 

223 
"semi_hom(prod, sum, h) ==> h(prod(x, y)) = sum(h(x), h(y))" 

224 
by (simp add: semi_hom_def) 

225 

226 
locale semi_hom_loc = prod: semi prod + sum: semi sum 

227 
for prod and sum and h + 

228 
assumes semi_homh: "semi_hom(prod, sum, h)" 

229 
notes semi_hom_mult = semi_hom_mult [OF semi_homh] 

230 

29219
fa3fb943a091
Attributes not applied in foundational version of fact.
ballarin
parents:
29217
diff
changeset

231 
thm semi_hom_loc.semi_hom_mult 
fa3fb943a091
Attributes not applied in foundational version of fact.
ballarin
parents:
29217
diff
changeset

232 
(* unspecified, attribute not applied in backgroud theory !!! *) 
fa3fb943a091
Attributes not applied in foundational version of fact.
ballarin
parents:
29217
diff
changeset

233 

29035  234 
lemma (in semi_hom_loc) "h(prod(x, y)) = sum(h(x), h(y))" 
235 
by (rule semi_hom_mult) 

236 

29217
a1c992fb3184
Finergrained activation so that facts from earlier elements are available.
ballarin
parents:
29214
diff
changeset

237 
(* Referring to facts from within a context specification *) 
a1c992fb3184
Finergrained activation so that facts from earlier elements are available.
ballarin
parents:
29214
diff
changeset

238 

a1c992fb3184
Finergrained activation so that facts from earlier elements are available.
ballarin
parents:
29214
diff
changeset

239 
lemma 
a1c992fb3184
Finergrained activation so that facts from earlier elements are available.
ballarin
parents:
29214
diff
changeset

240 
assumes x: "P <> P" 
a1c992fb3184
Finergrained activation so that facts from earlier elements are available.
ballarin
parents:
29214
diff
changeset

241 
notes y = x 
a1c992fb3184
Finergrained activation so that facts from earlier elements are available.
ballarin
parents:
29214
diff
changeset

242 
shows True .. 
a1c992fb3184
Finergrained activation so that facts from earlier elements are available.
ballarin
parents:
29214
diff
changeset

243 

29035  244 

29206  245 
section {* Theorem statements *} 
28881  246 

28873  247 
lemma (in lgrp) lcancel: 
248 
"x ** y = x ** z <> y = z" 

249 
proof 

250 
assume "x ** y = x ** z" 

251 
then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc) 

252 
then show "y = z" by (simp add: lone linv) 

253 
qed simp 

28881  254 
print_locale! lgrp 
255 

28873  256 

257 
locale rgrp = semi + 

258 
fixes one and inv 

259 
assumes rone: "x ** one = x" 

260 
and rinv: "x ** inv(x) = one" 

28881  261 
begin 
28873  262 

28881  263 
lemma rcancel: 
28873  264 
"y ** x = z ** x <> y = z" 
265 
proof 

266 
assume "y ** x = z ** x" 

267 
then have "y ** (x ** inv(x)) = z ** (x ** inv(x))" 

268 
by (simp add: assoc [symmetric]) 

269 
then show "y = z" by (simp add: rone rinv) 

270 
qed simp 

271 

272 
end 

28881  273 
print_locale! rgrp 
274 

28886  275 

29206  276 
subsection {* Patterns *} 
28886  277 

278 
lemma (in rgrp) 

279 
assumes "y ** x = z ** x" (is ?a) 

280 
shows "y = z" (is ?t) 

281 
proof  

282 
txt {* Weird proof involving patterns from context element and conclusion. *} 

283 
{ 

284 
assume ?a 

285 
then have "y ** (x ** inv(x)) = z ** (x ** inv(x))" 

286 
by (simp add: assoc [symmetric]) 

287 
then have ?t by (simp add: rone rinv) 

288 
} 

289 
note x = this 

290 
show ?t by (rule x [OF `?a`]) 

291 
qed 

292 

28896  293 

29206  294 
section {* Interpretation between locales: sublocales *} 
28896  295 

296 
sublocale lgrp < right: rgrp 

297 
print_facts 

28927
7e631979922f
Methods intro_locales and unfold_locales apply to both old and new locales.
ballarin
parents:
28903
diff
changeset

298 
proof unfold_locales 
28896  299 
{ 
300 
fix x 

301 
have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone) 

302 
then show "x ** one = x" by (simp add: assoc lcancel) 

303 
} 

304 
note rone = this 

305 
{ 

306 
fix x 

307 
have "inv(x) ** x ** inv(x) = inv(x) ** one" 

308 
by (simp add: linv lone rone) 

309 
then show "x ** inv(x) = one" by (simp add: assoc lcancel) 

310 
} 

28903
b3fc3a62247a
Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents:
28899
diff
changeset

311 
qed 
28896  312 

313 
(* effect on printed locale *) 

314 

315 
print_locale! lgrp 

316 

317 
(* use of derived theorem *) 

318 

319 
lemma (in lgrp) 

320 
"y ** x = z ** x <> y = z" 

321 
apply (rule rcancel) 

322 
done 

323 

324 
(* circular interpretation *) 

325 

326 
sublocale rgrp < left: lgrp 

28927
7e631979922f
Methods intro_locales and unfold_locales apply to both old and new locales.
ballarin
parents:
28903
diff
changeset

327 
proof unfold_locales 
28903
b3fc3a62247a
Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents:
28899
diff
changeset

328 
{ 
b3fc3a62247a
Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents:
28899
diff
changeset

329 
fix x 
b3fc3a62247a
Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents:
28899
diff
changeset

330 
have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone) 
b3fc3a62247a
Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents:
28899
diff
changeset

331 
then show "one ** x = x" by (simp add: assoc [symmetric] rcancel) 
b3fc3a62247a
Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents:
28899
diff
changeset

332 
} 
b3fc3a62247a
Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents:
28899
diff
changeset

333 
note lone = this 
b3fc3a62247a
Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents:
28899
diff
changeset

334 
{ 
b3fc3a62247a
Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents:
28899
diff
changeset

335 
fix x 
b3fc3a62247a
Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents:
28899
diff
changeset

336 
have "inv(x) ** (x ** inv(x)) = one ** inv(x)" 
b3fc3a62247a
Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents:
28899
diff
changeset

337 
by (simp add: rinv lone rone) 
b3fc3a62247a
Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents:
28899
diff
changeset

338 
then show "inv(x) ** x = one" by (simp add: assoc [symmetric] rcancel) 
b3fc3a62247a
Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents:
28899
diff
changeset

339 
} 
b3fc3a62247a
Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents:
28899
diff
changeset

340 
qed 
28896  341 

342 
(* effect on printed locale *) 

343 

344 
print_locale! rgrp 

345 
print_locale! lgrp 

346 

28898
530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

347 

28899
7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

348 
(* Duality *) 
7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

349 

7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

350 
locale order = 
7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

351 
fixes less :: "'a => 'a => o" (infix "<<" 50) 
7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

352 
assumes refl: "x << x" 
7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

353 
and trans: "[ x << y; y << z ] ==> x << z" 
7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

354 

7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

355 
sublocale order < dual: order "%x y. y << x" 
28927
7e631979922f
Methods intro_locales and unfold_locales apply to both old and new locales.
ballarin
parents:
28903
diff
changeset

356 
apply unfold_locales apply (rule refl) apply (blast intro: trans) 
28899
7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

357 
done 
7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

358 

7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

359 
print_locale! order (* Only two instances of order. *) 
7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

360 

7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

361 
locale order' = 
7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

362 
fixes less :: "'a => 'a => o" (infix "<<" 50) 
7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

363 
assumes refl: "x << x" 
7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

364 
and trans: "[ x << y; y << z ] ==> x << z" 
7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

365 

7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

366 
locale order_with_def = order' 
7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

367 
begin 
7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

368 

7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

369 
definition greater :: "'a => 'a => o" (infix ">>" 50) where 
7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

370 
"x >> y <> y << x" 
7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

371 

7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

372 
end 
7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

373 

7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

374 
sublocale order_with_def < dual: order' "op >>" 
28927
7e631979922f
Methods intro_locales and unfold_locales apply to both old and new locales.
ballarin
parents:
28903
diff
changeset

375 
apply unfold_locales 
28899
7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

376 
unfolding greater_def 
7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

377 
apply (rule refl) apply (blast intro: trans) 
7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

378 
done 
7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

379 

7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

380 
print_locale! order_with_def 
29210
4025459e3f83
Interpretation in theories: first version with equations.
ballarin
parents:
29206
diff
changeset

381 
(* Note that decls come after theorems that make use of them. *) 
28899
7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

382 

7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

383 

28898
530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

384 
(* locale with many parameters  
530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

385 
interpretations generate alternating group A5 *) 
530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

386 

28899
7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

387 

28898
530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

388 
locale A5 = 
530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

389 
fixes A and B and C and D and E 
530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

390 
assumes eq: "A <> B <> C <> D <> E" 
530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

391 

530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

392 
sublocale A5 < 1: A5 _ _ D E C 
530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

393 
print_facts 
530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

394 
using eq apply (blast intro: A5.intro) done 
530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

395 

530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

396 
sublocale A5 < 2: A5 C _ E _ A 
530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

397 
print_facts 
530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

398 
using eq apply (blast intro: A5.intro) done 
530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

399 

530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

400 
sublocale A5 < 3: A5 B C A _ _ 
530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

401 
print_facts 
530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

402 
using eq apply (blast intro: A5.intro) done 
530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

403 

530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

404 
(* Any even permutation of parameters is subsumed by the above. *) 
530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

405 

530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

406 
print_locale! A5 
530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

407 

530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

408 

530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

409 
(* Free arguments of instance *) 
530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

410 

530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

411 
locale trivial = 
530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

412 
fixes P and Q :: o 
530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

413 
assumes Q: "P <> P <> Q" 
530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

414 
begin 
530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

415 

530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

416 
lemma Q_triv: "Q" using Q by fast 
530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

417 

28881  418 
end 
28898
530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

419 

530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

420 
sublocale trivial < x: trivial x _ 
28927
7e631979922f
Methods intro_locales and unfold_locales apply to both old and new locales.
ballarin
parents:
28903
diff
changeset

421 
apply unfold_locales using Q by fast 
28898
530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

422 

530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

423 
print_locale! trivial 
530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

424 

530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

425 
context trivial begin thm x.Q [where ?x = True] end 
530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

426 

28899
7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

427 
sublocale trivial < y: trivial Q Q 
28927
7e631979922f
Methods intro_locales and unfold_locales apply to both old and new locales.
ballarin
parents:
28903
diff
changeset

428 
by unfold_locales 
28903
b3fc3a62247a
Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents:
28899
diff
changeset

429 
(* Succeeds since previous interpretation is more general. *) 
28899
7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

430 

7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

431 
print_locale! trivial (* No instance for y created (subsumed). *) 
7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

432 

28993
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

433 

29206  434 
subsection {* Sublocale, then interpretation in theory *} 
28993
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

435 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29513
diff
changeset

436 
interpretation int?: lgrp "op +" "0" "minus" 
28993
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

437 
proof unfold_locales 
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

438 
qed (rule int_assoc int_zero int_minus)+ 
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

439 

829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

440 
thm int.assoc int.semi_axioms 
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

441 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29513
diff
changeset

442 
interpretation int2?: semi "op +" 
28993
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

443 
by unfold_locales (* subsumed, thm int2.assoc not generated *) 
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

444 

32802
b52aa3bc7362
Stricter test: raise error if registration generates duplicate theorem.
ballarin
parents:
30752
diff
changeset

445 
ML {* (PureThy.get_thms @{theory} "int2.assoc"; 
b52aa3bc7362
Stricter test: raise error if registration generates duplicate theorem.
ballarin
parents:
30752
diff
changeset

446 
error "thm int2.assoc was generated") 
b52aa3bc7362
Stricter test: raise error if registration generates duplicate theorem.
ballarin
parents:
30752
diff
changeset

447 
handle ERROR "Unknown fact \"int2.assoc\"" => ([]:thm list); *} 
b52aa3bc7362
Stricter test: raise error if registration generates duplicate theorem.
ballarin
parents:
30752
diff
changeset

448 

28993
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

449 
thm int.lone int.right.rone 
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

450 
(* the latter comes through the sublocale relation *) 
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

451 

829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

452 

29206  453 
subsection {* Interpretation in theory, then sublocale *} 
28993
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

454 

33617
bfee47887ca3
Enables tests for locale functionality that is now available.
ballarin
parents:
33462
diff
changeset

455 
interpretation fol: logic "op +" "minus" 
28993
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

456 
by unfold_locales (rule int_assoc int_minus2)+ 
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

457 

829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

458 
locale logic2 = 
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

459 
fixes land (infixl "&&" 55) 
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

460 
and lnot (" _" [60] 60) 
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

461 
assumes assoc: "(x && y) && z = x && (y && z)" 
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

462 
and notnot: " ( x) = x" 
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

463 
begin 
29206  464 

28993
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

465 
definition lor (infixl "" 50) where 
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

466 
"x  y = ( x &&  y)" 
29206  467 

28898
530c7d28a962
Proper treatment of expressions with free arguments.
ballarin
parents:
28896
diff
changeset

468 
end 
28993
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

469 

829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

470 
sublocale logic < two: logic2 
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

471 
by unfold_locales (rule assoc notnot)+ 
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

472 

33617
bfee47887ca3
Enables tests for locale functionality that is now available.
ballarin
parents:
33462
diff
changeset

473 
thm fol.two.assoc 
28993
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

474 

29018  475 

29206  476 
subsection {* Declarations and sublocale *} 
477 

478 
locale logic_a = logic 

479 
locale logic_b = logic 

480 

481 
sublocale logic_a < logic_b 

482 
by unfold_locales 

483 

484 

29210
4025459e3f83
Interpretation in theories: first version with equations.
ballarin
parents:
29206
diff
changeset

485 
subsection {* Equations *} 
4025459e3f83
Interpretation in theories: first version with equations.
ballarin
parents:
29206
diff
changeset

486 

4025459e3f83
Interpretation in theories: first version with equations.
ballarin
parents:
29206
diff
changeset

487 
locale logic_o = 
4025459e3f83
Interpretation in theories: first version with equations.
ballarin
parents:
29206
diff
changeset

488 
fixes land (infixl "&&" 55) 
4025459e3f83
Interpretation in theories: first version with equations.
ballarin
parents:
29206
diff
changeset

489 
and lnot (" _" [60] 60) 
4025459e3f83
Interpretation in theories: first version with equations.
ballarin
parents:
29206
diff
changeset

490 
assumes assoc_o: "(x && y) && z <> x && (y && z)" 
4025459e3f83
Interpretation in theories: first version with equations.
ballarin
parents:
29206
diff
changeset

491 
and notnot_o: " ( x) <> x" 
4025459e3f83
Interpretation in theories: first version with equations.
ballarin
parents:
29206
diff
changeset

492 
begin 
4025459e3f83
Interpretation in theories: first version with equations.
ballarin
parents:
29206
diff
changeset

493 

4025459e3f83
Interpretation in theories: first version with equations.
ballarin
parents:
29206
diff
changeset

494 
definition lor_o (infixl "" 50) where 
4025459e3f83
Interpretation in theories: first version with equations.
ballarin
parents:
29206
diff
changeset

495 
"x  y <> ( x &&  y)" 
4025459e3f83
Interpretation in theories: first version with equations.
ballarin
parents:
29206
diff
changeset

496 

4025459e3f83
Interpretation in theories: first version with equations.
ballarin
parents:
29206
diff
changeset

497 
end 
4025459e3f83
Interpretation in theories: first version with equations.
ballarin
parents:
29206
diff
changeset

498 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29513
diff
changeset

499 
interpretation x: logic_o "op &" "Not" 
29211  500 
where bool_logic_o: "logic_o.lor_o(op &, Not, x, y) <> x  y" 
501 
proof  

502 
show bool_logic_o: "PROP logic_o(op &, Not)" by unfold_locales fast+ 

503 
show "logic_o.lor_o(op &, Not, x, y) <> x  y" 

504 
by (unfold logic_o.lor_o_def [OF bool_logic_o]) fast 

505 
qed 

29210
4025459e3f83
Interpretation in theories: first version with equations.
ballarin
parents:
29206
diff
changeset

506 

29211  507 
thm x.lor_o_def bool_logic_o 
29210
4025459e3f83
Interpretation in theories: first version with equations.
ballarin
parents:
29206
diff
changeset

508 

29214  509 
lemma lor_triv: "z <> z" .. 
510 

29210
4025459e3f83
Interpretation in theories: first version with equations.
ballarin
parents:
29206
diff
changeset

511 
lemma (in logic_o) lor_triv: "x  y <> x  y" by fast 
4025459e3f83
Interpretation in theories: first version with equations.
ballarin
parents:
29206
diff
changeset

512 

29214  513 
thm lor_triv [where z = True] (* Check strict prefix. *) 
514 
x.lor_triv 

29210
4025459e3f83
Interpretation in theories: first version with equations.
ballarin
parents:
29206
diff
changeset

515 

4025459e3f83
Interpretation in theories: first version with equations.
ballarin
parents:
29206
diff
changeset

516 

33835  517 
subsection {* Inheritance of mixins *} 
518 

519 
locale reflexive = 

520 
fixes le :: "'a => 'a => o" (infix "\<sqsubseteq>" 50) 

521 
assumes refl: "x \<sqsubseteq> x" 

522 
begin 

523 

524 
definition less (infix "\<sqsubset>" 50) where "x \<sqsubset> y <> x \<sqsubseteq> y & x ~= y" 

525 

526 
end 

527 

528 
consts 

529 
gle :: "'a => 'a => o" gless :: "'a => 'a => o" 

530 
gle' :: "'a => 'a => o" gless' :: "'a => 'a => o" 

531 

532 
axioms 

533 
grefl: "gle(x, x)" gless_def: "gless(x, y) <> gle(x, y) & x ~= y" 

534 
grefl': "gle'(x, x)" gless'_def: "gless'(x, y) <> gle'(x, y) & x ~= y" 

535 

536 
text {* Mixin not applied to locales further up the hierachy. *} 

537 

538 
locale mixin = reflexive 

539 
begin 

540 
lemmas less_thm = less_def 

541 
end 

542 

543 
interpretation le: mixin gle where "reflexive.less(gle, x, y) <> gless(x, y)" 

544 
proof  

545 
show "mixin(gle)" by unfold_locales (rule grefl) 

546 
note reflexive = this[unfolded mixin_def] 

547 
show "reflexive.less(gle, x, y) <> gless(x, y)" 

548 
by (simp add: reflexive.less_def[OF reflexive] gless_def) 

549 
qed 

550 

551 
thm le.less_def (* mixin not applied *) 

552 
lemma "reflexive.less(gle, x, y) <> gle(x, y) & x ~= y" by (rule le.less_def) 

553 
thm le.less_thm (* mixin applied *) 

554 
lemma "gless(x, y) <> gle(x, y) & x ~= y" by (rule le.less_thm) 

555 

556 
lemma "reflexive.less(gle, x, y) <> gle(x, y) & x ~= y" 

557 
by (rule le.less_def) 

558 
lemma "gless(x, y) <> gle(x, y) & x ~= y" 

559 
by (rule le.less_thm) 

560 

561 
text {* Mixin propagated along the locale hierarchy *} 

562 

563 
locale mixin2 = mixin 

564 
begin 

565 
lemmas less_thm2 = less_def 

566 
end 

567 

568 
interpretation le: mixin2 gle 

569 
by unfold_locales 

570 

571 
thm le.less_thm2 (* mixin applied *) 

572 
lemma "gless(x, y) <> gle(x, y) & x ~= y" 

573 
by (rule le.less_thm2) 

574 

575 
text {* Mixin only available in original context *} 

576 

577 
(* This section is not finished. *) 

578 

579 
locale mixin3 = mixin le' for le' :: "'a => 'a => o" (infix "\<sqsubseteq>''" 50) 

580 

581 
lemma (in mixin2) before: 

582 
"reflexive.less(gle, x, y) <> gle(x, y) & x ~= y" 

583 
proof  

584 
have "reflexive(gle)" by unfold_locales (rule grefl) 

585 
note th = reflexive.less_def[OF this] 

586 
then show ?thesis by (simp add: th) 

587 
qed 

588 

589 
interpretation le': mixin2 gle' 

590 
apply unfold_locales apply (rule grefl') done 

591 

592 
lemma (in mixin2) after: 

593 
"reflexive.less(gle, x, y) <> gle(x, y) & x ~= y" 

594 
proof  

595 
have "reflexive(gle)" by unfold_locales (rule grefl) 

596 
note th = reflexive.less_def[OF this] 

597 
then show ?thesis by (simp add: th) 

598 
qed 

599 

600 
thm le'.less_def le'.less_thm le'.less_thm2 le'.before le'.after 

601 

602 
locale combined = le: reflexive le + le': mixin le' 

603 
for le :: "'a => 'a => o" (infixl "\<sqsubseteq>" 50) and le' :: "'a => 'a => o" (infixl "\<sqsubseteq>''" 50) 

604 

605 
interpretation combined gle gle' 

606 
apply unfold_locales done 

607 

608 
thm le.less_def le.less_thm le'.less_def le'.less_thm 

609 

610 

29210
4025459e3f83
Interpretation in theories: first version with equations.
ballarin
parents:
29206
diff
changeset

611 
subsection {* Interpretation in proofs *} 
29018  612 

613 
lemma True 

614 
proof 

615 
interpret "local": lgrp "op +" "0" "minus" 

616 
by unfold_locales (* subsumed *) 

617 
{ 

618 
fix zero :: int 

619 
assume "!!x. zero + x = x" "!!x. (x) + x = zero" 

620 
then interpret local_fixed: lgrp "op +" zero "minus" 

621 
by unfold_locales 

622 
thm local_fixed.lone 

623 
} 

624 
assume "!!x zero. zero + x = x" "!!x zero. (x) + x = zero" 

625 
then interpret local_free: lgrp "op +" zero "minus" for zero 

626 
by unfold_locales 

627 
thm local_free.lone [where ?zero = 0] 

628 
qed 

629 

28993
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28936
diff
changeset

630 
end 