author  ballarin 
Fri, 28 Nov 2008 17:43:06 +0100  
changeset 28903  b3fc3a62247a 
parent 28899  7bf5d7f154b8 
child 28927  7e631979922f 
permissions  rwrr 
28873  1 
(* Title: FOL/ex/NewLocaleTest.thy 
2 
ID: $Id$ 

3 
Author: Clemens Ballarin, TU Muenchen 

4 

5 
Testing environment for locale expressions  experimental. 

6 
*) 

7 

8 
theory NewLocaleTest 

9 
imports NewLocaleSetup 

10 
begin 

11 

12 
ML_val {* set new_locales *} 

13 
ML_val {* set Toplevel.debug *} 

14 
ML_val {* set show_hyps *} 

15 

16 

17 
typedecl int arities int :: "term" 

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

19 
zero :: int ("0") 

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

21 

22 

23 
text {* Inference of parameter types *} 

24 

25 
locale param1 = fixes p 

26 
print_locale! param1 

27 

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

31 
(* 

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

33 
print_locale! param_top 

34 
*) 

35 

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

37 
print_locale! param3 

38 

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

40 
print_locale! param4 

41 

42 

43 
text {* Incremental type constraints *} 

44 

45 
locale constraint1 = 

46 
fixes prod (infixl "**" 65) 

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

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

49 
print_locale! constraint1 

50 

51 
locale constraint2 = 

52 
fixes p and q 

53 
assumes "p = q" 

54 
print_locale! constraint2 

55 

56 

28881  57 
text {* Inheritance *} 
28873  58 

59 
locale semi = 

60 
fixes prod (infixl "**" 65) 

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

62 
print_locale! semi thm semi_def 

63 

64 
locale lgrp = semi + 

65 
fixes one and inv 

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

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

68 
print_locale! lgrp thm lgrp_def lgrp_axioms_def 

69 

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

71 
fixes zero and neg 

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

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

74 
print_locale! add_lgrp thm add_lgrp_def add_lgrp_axioms_def 

75 

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

77 
print_locale! rev_lgrp thm rev_lgrp_def 

78 

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

80 
print_locale! hom thm hom_def 

81 

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

83 
print_locale! perturbation thm perturbation_def 

84 

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

86 
print_locale! pert_hom thm pert_hom_def 

87 

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

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

90 
print_locale! pert_hom' thm pert_hom'_def 

91 

92 

28881  93 
text {* Syntax declarations *} 
28873  94 

95 
locale logic = 

96 
fixes land (infixl "&&" 55) 

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

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

99 
and notnot: " ( x) = x" 

100 
begin 

101 

102 
definition lor (infixl "" 50) where 

103 
"x  y = ( x &&  y)" 

104 

105 
end 

106 
print_locale! logic 

107 

108 
locale use_decl = logic + semi "op " 

109 
print_locale! use_decl thm use_decl_def 

110 

28881  111 

112 
text {* Theorem statements *} 

113 

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

116 
proof 

117 
assume "x ** y = x ** z" 

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

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

120 
qed simp 

28881  121 
print_locale! lgrp 
122 

28873  123 

124 
locale rgrp = semi + 

125 
fixes one and inv 

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

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

28881  128 
begin 
28873  129 

28881  130 
lemma rcancel: 
28873  131 
"y ** x = z ** x <> y = z" 
132 
proof 

133 
assume "y ** x = z ** x" 

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

135 
by (simp add: assoc [symmetric]) 

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

137 
qed simp 

138 

139 
end 

28881  140 
print_locale! rgrp 
141 

28886  142 

143 
text {* Patterns *} 

144 

145 
lemma (in rgrp) 

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

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

148 
proof  

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

150 
{ 

151 
assume ?a 

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

153 
by (simp add: assoc [symmetric]) 

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

155 
} 

156 
note x = this 

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

158 
qed 

159 

160 
lemma 

161 
assumes "P <> P" (is "?p <> _") 

162 
shows "?p <> ?p" 

163 
. 

164 

28896  165 

166 
text {* Interpretation between locales: sublocales *} 

167 

168 
sublocale lgrp < right: rgrp 

169 
print_facts 

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

170 
proof new_unfold_locales 
28896  171 
{ 
172 
fix x 

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

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

175 
} 

176 
note rone = this 

177 
{ 

178 
fix x 

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

180 
by (simp add: linv lone rone) 

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

182 
} 

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

183 
qed 
28896  184 

185 
(* effect on printed locale *) 

186 

187 
print_locale! lgrp 

188 

189 
(* use of derived theorem *) 

190 

191 
lemma (in lgrp) 

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

193 
apply (rule rcancel) 

194 
done 

195 

196 
(* circular interpretation *) 

197 

198 
sublocale rgrp < left: lgrp 

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

199 
proof new_unfold_locales 
b3fc3a62247a
Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents:
28899
diff
changeset

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

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

202 
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

203 
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

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

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

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

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

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

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

210 
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

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

212 
qed 
28896  213 

214 
(* effect on printed locale *) 

215 

216 
print_locale! rgrp 

217 
print_locale! lgrp 

218 

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

219 

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

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

221 

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

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

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

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

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

226 

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

227 
sublocale order < dual: order "%x y. y << x" 
28903
b3fc3a62247a
Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents:
28899
diff
changeset

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

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

230 

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

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

232 

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

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

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

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

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

237 

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

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

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

240 

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

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

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

243 

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

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

245 

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

246 
sublocale order_with_def < dual: order' "op >>" 
28903
b3fc3a62247a
Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents:
28899
diff
changeset

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

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

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

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

251 

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

252 
print_locale! order_with_def 
7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

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

254 
Appears to be harmless at least in this example. *) 
7bf5d7f154b8
Perform higherorder pattern matching during roundup.
ballarin
parents:
28898
diff
changeset

255 

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

256 

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

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

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

259 

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

260 

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

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

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

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

264 

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

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

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

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

268 

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

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

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

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

272 

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

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

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

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

276 

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

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

278 

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

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

280 

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

281 

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

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

283 

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

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

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

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

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

288 

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

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

290 

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

292 

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

293 
sublocale trivial < x: trivial x _ 
28903
b3fc3a62247a
Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents:
28899
diff
changeset

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

295 

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

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

297 

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

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

299 

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

300 
sublocale trivial < y: trivial Q Q 
28903
b3fc3a62247a
Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents:
28899
diff
changeset

301 
by new_unfold_locales 
b3fc3a62247a
Intro_locales_tac to simplify goals involving locale predicates.
ballarin
parents:
28899
diff
changeset

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

303 

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

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

305 

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

306 
end 