author  ballarin 
Wed, 11 Nov 2009 21:53:58 +0100  
changeset 33617  bfee47887ca3 
parent 33462  ddcf2004e215 
child 33671  4b0f2599ed48 
child 33835  d6134fb5a49f 
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 
(* Can we get rid the the additional hypothesis, caused by LocalTheory.notes? *) 
e74341997a48
Pass on defines in inheritance; reject illicit defines created by instantiation.
ballarin
parents:
29028
diff
changeset

199 

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

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

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

202 

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

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

204 

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

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

206 

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

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

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

209 

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

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

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

212 

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

213 
end 
29019  214 

29035  215 

29206  216 
section {* Notes *} 
29035  217 

218 
(* A somewhat arcane homomorphism example *) 

219 

220 
definition semi_hom where 

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

222 

223 
lemma semi_hom_mult: 

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

225 
by (simp add: semi_hom_def) 

226 

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

228 
for prod and sum and h + 

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

230 
notes semi_hom_mult = semi_hom_mult [OF semi_homh] 

231 

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

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

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

234 

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

237 

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

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

239 

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

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

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

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

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

244 

29035  245 

29206  246 
section {* Theorem statements *} 
28881  247 

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

250 
proof 

251 
assume "x ** y = x ** z" 

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

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

254 
qed simp 

28881  255 
print_locale! lgrp 
256 

28873  257 

258 
locale rgrp = semi + 

259 
fixes one and inv 

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

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

28881  262 
begin 
28873  263 

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

267 
assume "y ** x = z ** x" 

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

269 
by (simp add: assoc [symmetric]) 

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

271 
qed simp 

272 

273 
end 

28881  274 
print_locale! rgrp 
275 

28886  276 

29206  277 
subsection {* Patterns *} 
28886  278 

279 
lemma (in rgrp) 

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

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

282 
proof  

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

284 
{ 

285 
assume ?a 

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

287 
by (simp add: assoc [symmetric]) 

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

289 
} 

290 
note x = this 

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

292 
qed 

293 

28896  294 

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

297 
sublocale lgrp < right: rgrp 

298 
print_facts 

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

299 
proof unfold_locales 
28896  300 
{ 
301 
fix x 

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

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

304 
} 

305 
note rone = this 

306 
{ 

307 
fix x 

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

309 
by (simp add: linv lone rone) 

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

311 
} 

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

312 
qed 
28896  313 

314 
(* effect on printed locale *) 

315 

316 
print_locale! lgrp 

317 

318 
(* use of derived theorem *) 

319 

320 
lemma (in lgrp) 

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

322 
apply (rule rcancel) 

323 
done 

324 

325 
(* circular interpretation *) 

326 

327 
sublocale rgrp < left: lgrp 

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

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

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

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

331 
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

332 
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

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

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

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

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

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

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

339 
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

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

341 
qed 
28896  342 

343 
(* effect on printed locale *) 

344 

345 
print_locale! rgrp 

346 
print_locale! lgrp 

347 

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

348 

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

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

350 

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

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

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

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

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

355 

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

356 
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

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

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

359 

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

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

361 

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

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

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

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

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

366 

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

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

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

369 

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

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

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

372 

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

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

374 

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

375 
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

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

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

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

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

380 

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

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

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

383 

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

384 

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

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

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

387 

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

388 

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

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

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

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

392 

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

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

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

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

396 

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

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

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

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

400 

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

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

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

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

404 

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

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

406 

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

407 
print_locale! A5 
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 

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

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

411 

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

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

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

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

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

416 

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

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

418 

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

420 

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

421 
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

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

423 

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

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

425 

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

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

427 

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

428 
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

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

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

431 

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

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

433 

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

434 

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

436 

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

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

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

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

440 

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

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

442 

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

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

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

445 

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

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

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

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

449 

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

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

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

452 

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

453 

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

455 

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

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

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

458 

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

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

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

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

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

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

464 
begin 
29206  465 

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

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

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

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

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

470 

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

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

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

473 

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

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

475 

29018  476 

29206  477 
subsection {* Declarations and sublocale *} 
478 

479 
locale logic_a = logic 

480 
locale logic_b = logic 

481 

482 
sublocale logic_a < logic_b 

483 
by unfold_locales 

484 

485 

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

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

487 

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

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

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

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

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

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

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

494 

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

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

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

497 

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

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

499 

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

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

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

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

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

506 
qed 

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

507 

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

509 

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

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

512 
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

513 

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

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

516 

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

517 

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

518 
subsection {* Interpretation in proofs *} 
29018  519 

520 
lemma True 

521 
proof 

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

523 
by unfold_locales (* subsumed *) 

524 
{ 

525 
fix zero :: int 

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

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

528 
by unfold_locales 

529 
thm local_fixed.lone 

530 
} 

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

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

533 
by unfold_locales 

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

535 
qed 

536 

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

537 
end 