1.1 --- a/src/FOL/ex/LocaleTest.thy Mon Jul 23 13:47:48 2007 +0200
1.2 +++ b/src/FOL/ex/LocaleTest.thy Mon Jul 23 13:48:30 2007 +0200
1.3 @@ -798,6 +798,9 @@
1.4
1.5 text {* Naming convention for global objects: prefixes D and d *}
1.6
1.7 +
1.8 +subsection {* Simple examples *}
1.9 +
1.10 locale Da = fixes a :: o
1.11 assumes true: a
1.12
1.13 @@ -807,7 +810,7 @@
1.14 apply simp apply (rule true) done
1.15
1.16 interpretation D1: Da ["True"]
1.17 - where "~ True" = "False"
1.18 + where "~ True == False"
1.19 apply -
1.20 apply unfold_locales [1] apply rule
1.21 by simp
1.22 @@ -816,7 +819,7 @@
1.23 lemma "False <-> False" apply (rule D1.not_false) done
1.24
1.25 interpretation D2: Da ["x | ~ x"]
1.26 - where "~ (x | ~ x)" = "~ x & x"
1.27 + where "~ (x | ~ x) <-> ~ x & x"
1.28 apply -
1.29 apply unfold_locales [1] apply fast
1.30 by simp
2.1 --- a/src/HOL/ex/LocaleTest2.thy Mon Jul 23 13:47:48 2007 +0200
2.2 +++ b/src/HOL/ex/LocaleTest2.thy Mon Jul 23 13:48:30 2007 +0200
2.3 @@ -5,26 +5,635 @@
2.4
2.5 More regression tests for locales.
2.6 Definitions are less natural in FOL, since there is no selection operator.
2.7 -Hence we do them in HOL, not in the main test suite for locales:
2.8 -FOL/ex/LocaleTest.thy
2.9 +Hence we do them here in HOL, not in the main test suite for locales,
2.10 +which is FOL/ex/LocaleTest.thy
2.11 *)
2.12
2.13 header {* Test of Locale Interpretation *}
2.14
2.15 theory LocaleTest2
2.16 -imports Main
2.17 +imports GCD
2.18 begin
2.19
2.20 -ML {* set quick_and_dirty *} (* allow for thm command in batch mode *)
2.21 -ML {* set show_hyps *}
2.22 -ML {* set show_sorts *}
2.23 -
2.24 -
2.25 -subsection {* Interpretation of Defined Concepts *}
2.26 +section {* Interpretation of Defined Concepts *}
2.27
2.28 text {* Naming convention for global objects: prefixes D and d *}
2.29
2.30 -(* Group example with defined operation inv *)
2.31 +
2.32 +subsection {* Lattices *}
2.33 +
2.34 +text {* Much of the lattice proofs are from HOL/Lattice. *}
2.35 +
2.36 +
2.37 +subsubsection {* Definitions *}
2.38 +
2.39 +locale dpo =
2.40 + fixes le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>" 50)
2.41 + assumes refl [intro, simp]: "x \<sqsubseteq> x"
2.42 + and anti_sym [intro]: "[| x \<sqsubseteq> y; y \<sqsubseteq> x |] ==> x = y"
2.43 + and trans [trans]: "[| x \<sqsubseteq> y; y \<sqsubseteq> z |] ==> x \<sqsubseteq> z"
2.44 +
2.45 +begin
2.46 +
2.47 +theorem circular:
2.48 + "[| x \<sqsubseteq> y; y \<sqsubseteq> z; z \<sqsubseteq> x |] ==> x = y & y = z"
2.49 + by (blast intro: trans)
2.50 +
2.51 +definition
2.52 + less :: "['a, 'a] => bool" (infixl "\<sqsubset>" 50)
2.53 + where "(x \<sqsubset> y) = (x \<sqsubseteq> y & x ~= y)"
2.54 +
2.55 +theorem abs_test:
2.56 + "op \<sqsubset> = (%x y. x \<sqsubset> y)"
2.57 + by simp
2.58 +
2.59 +definition
2.60 + is_inf :: "['a, 'a, 'a] => bool"
2.61 + where "is_inf x y i = (i \<sqsubseteq> x \<and> i \<sqsubseteq> y \<and> (\<forall>z. z \<sqsubseteq> x \<and> z \<sqsubseteq> y \<longrightarrow> z \<sqsubseteq> i))"
2.62 +
2.63 +definition
2.64 + is_sup :: "['a, 'a, 'a] => bool"
2.65 + where "is_sup x y s = (x \<sqsubseteq> s \<and> y \<sqsubseteq> s \<and> (\<forall>z. x \<sqsubseteq> z \<and> y \<sqsubseteq> z \<longrightarrow> s \<sqsubseteq> z))"
2.66 +
2.67 +end
2.68 +
2.69 +locale dlat = dpo +
2.70 + assumes ex_inf: "EX inf. dpo.is_inf le x y inf"
2.71 + and ex_sup: "EX sup. dpo.is_sup le x y sup"
2.72 +
2.73 +begin
2.74 +
2.75 +definition
2.76 + meet :: "['a, 'a] => 'a" (infixl "\<sqinter>" 70)
2.77 + where "x \<sqinter> y = (THE inf. is_inf x y inf)"
2.78 +
2.79 +definition
2.80 + join :: "['a, 'a] => 'a" (infixl "\<squnion>" 65)
2.81 + where "x \<squnion> y = (THE sup. is_sup x y sup)"
2.82 +
2.83 +lemma is_infI [intro?]: "i \<sqsubseteq> x \<Longrightarrow> i \<sqsubseteq> y \<Longrightarrow>
2.84 + (\<And>z. z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> i) \<Longrightarrow> is_inf x y i"
2.85 + by (unfold is_inf_def) blast
2.86 +
2.87 +lemma is_inf_lower [elim?]:
2.88 + "is_inf x y i \<Longrightarrow> (i \<sqsubseteq> x \<Longrightarrow> i \<sqsubseteq> y \<Longrightarrow> C) \<Longrightarrow> C"
2.89 + by (unfold is_inf_def) blast
2.90 +
2.91 +lemma is_inf_greatest [elim?]:
2.92 + "is_inf x y i \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> i"
2.93 + by (unfold is_inf_def) blast
2.94 +
2.95 +theorem is_inf_uniq: "is_inf x y i \<Longrightarrow> is_inf x y i' \<Longrightarrow> i = i'"
2.96 +proof -
2.97 + assume inf: "is_inf x y i"
2.98 + assume inf': "is_inf x y i'"
2.99 + show ?thesis
2.100 + proof (rule anti_sym)
2.101 + from inf' show "i \<sqsubseteq> i'"
2.102 + proof (rule is_inf_greatest)
2.103 + from inf show "i \<sqsubseteq> x" ..
2.104 + from inf show "i \<sqsubseteq> y" ..
2.105 + qed
2.106 + from inf show "i' \<sqsubseteq> i"
2.107 + proof (rule is_inf_greatest)
2.108 + from inf' show "i' \<sqsubseteq> x" ..
2.109 + from inf' show "i' \<sqsubseteq> y" ..
2.110 + qed
2.111 + qed
2.112 +qed
2.113 +
2.114 +theorem is_inf_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> is_inf x y x"
2.115 +proof -
2.116 + assume "x \<sqsubseteq> y"
2.117 + show ?thesis
2.118 + proof
2.119 + show "x \<sqsubseteq> x" ..
2.120 + show "x \<sqsubseteq> y" by fact
2.121 + fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" show "z \<sqsubseteq> x" by fact
2.122 + qed
2.123 +qed
2.124 +
2.125 +lemma meet_equality [elim?]: "is_inf x y i \<Longrightarrow> x \<sqinter> y = i"
2.126 +proof (unfold meet_def)
2.127 + assume "is_inf x y i"
2.128 + then show "(THE i. is_inf x y i) = i"
2.129 + by (rule the_equality) (rule is_inf_uniq [OF _ `is_inf x y i`])
2.130 +qed
2.131 +
2.132 +lemma meetI [intro?]:
2.133 + "i \<sqsubseteq> x \<Longrightarrow> i \<sqsubseteq> y \<Longrightarrow> (\<And>z. z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> i) \<Longrightarrow> x \<sqinter> y = i"
2.134 + by (rule meet_equality, rule is_infI) blast+
2.135 +
2.136 +lemma is_inf_meet [intro?]: "is_inf x y (x \<sqinter> y)"
2.137 +proof (unfold meet_def)
2.138 + from ex_inf obtain i where "is_inf x y i" ..
2.139 + then show "is_inf x y (THE i. is_inf x y i)"
2.140 + by (rule theI) (rule is_inf_uniq [OF _ `is_inf x y i`])
2.141 +qed
2.142 +
2.143 +lemma meet_left [intro?]:
2.144 + "x \<sqinter> y \<sqsubseteq> x"
2.145 + by (rule is_inf_lower) (rule is_inf_meet)
2.146 +
2.147 +lemma meet_right [intro?]:
2.148 + "x \<sqinter> y \<sqsubseteq> y"
2.149 + by (rule is_inf_lower) (rule is_inf_meet)
2.150 +
2.151 +lemma meet_le [intro?]:
2.152 + "[| z \<sqsubseteq> x; z \<sqsubseteq> y |] ==> z \<sqsubseteq> x \<sqinter> y"
2.153 + by (rule is_inf_greatest) (rule is_inf_meet)
2.154 +
2.155 +lemma is_supI [intro?]: "x \<sqsubseteq> s \<Longrightarrow> y \<sqsubseteq> s \<Longrightarrow>
2.156 + (\<And>z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> s \<sqsubseteq> z) \<Longrightarrow> is_sup x y s"
2.157 + by (unfold is_sup_def) blast
2.158 +
2.159 +lemma is_sup_least [elim?]:
2.160 + "is_sup x y s \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> s \<sqsubseteq> z"
2.161 + by (unfold is_sup_def) blast
2.162 +
2.163 +lemma is_sup_upper [elim?]:
2.164 + "is_sup x y s \<Longrightarrow> (x \<sqsubseteq> s \<Longrightarrow> y \<sqsubseteq> s \<Longrightarrow> C) \<Longrightarrow> C"
2.165 + by (unfold is_sup_def) blast
2.166 +
2.167 +theorem is_sup_uniq: "is_sup x y s \<Longrightarrow> is_sup x y s' \<Longrightarrow> s = s'"
2.168 +proof -
2.169 + assume sup: "is_sup x y s"
2.170 + assume sup': "is_sup x y s'"
2.171 + show ?thesis
2.172 + proof (rule anti_sym)
2.173 + from sup show "s \<sqsubseteq> s'"
2.174 + proof (rule is_sup_least)
2.175 + from sup' show "x \<sqsubseteq> s'" ..
2.176 + from sup' show "y \<sqsubseteq> s'" ..
2.177 + qed
2.178 + from sup' show "s' \<sqsubseteq> s"
2.179 + proof (rule is_sup_least)
2.180 + from sup show "x \<sqsubseteq> s" ..
2.181 + from sup show "y \<sqsubseteq> s" ..
2.182 + qed
2.183 + qed
2.184 +qed
2.185 +
2.186 +theorem is_sup_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> is_sup x y y"
2.187 +proof -
2.188 + assume "x \<sqsubseteq> y"
2.189 + show ?thesis
2.190 + proof
2.191 + show "x \<sqsubseteq> y" by fact
2.192 + show "y \<sqsubseteq> y" ..
2.193 + fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z"
2.194 + show "y \<sqsubseteq> z" by fact
2.195 + qed
2.196 +qed
2.197 +
2.198 +lemma join_equality [elim?]: "is_sup x y s \<Longrightarrow> x \<squnion> y = s"
2.199 +proof (unfold join_def)
2.200 + assume "is_sup x y s"
2.201 + then show "(THE s. is_sup x y s) = s"
2.202 + by (rule the_equality) (rule is_sup_uniq [OF _ `is_sup x y s`])
2.203 +qed
2.204 +
2.205 +lemma joinI [intro?]: "x \<sqsubseteq> s \<Longrightarrow> y \<sqsubseteq> s \<Longrightarrow>
2.206 + (\<And>z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> s \<sqsubseteq> z) \<Longrightarrow> x \<squnion> y = s"
2.207 + by (rule join_equality, rule is_supI) blast+
2.208 +
2.209 +lemma is_sup_join [intro?]: "is_sup x y (x \<squnion> y)"
2.210 +proof (unfold join_def)
2.211 + from ex_sup obtain s where "is_sup x y s" ..
2.212 + then show "is_sup x y (THE s. is_sup x y s)"
2.213 + by (rule theI) (rule is_sup_uniq [OF _ `is_sup x y s`])
2.214 +qed
2.215 +
2.216 +lemma join_left [intro?]:
2.217 + "x \<sqsubseteq> x \<squnion> y"
2.218 + by (rule is_sup_upper) (rule is_sup_join)
2.219 +
2.220 +lemma join_right [intro?]:
2.221 + "y \<sqsubseteq> x \<squnion> y"
2.222 + by (rule is_sup_upper) (rule is_sup_join)
2.223 +
2.224 +lemma join_le [intro?]:
2.225 + "[| x \<sqsubseteq> z; y \<sqsubseteq> z |] ==> x \<squnion> y \<sqsubseteq> z"
2.226 + by (rule is_sup_least) (rule is_sup_join)
2.227 +
2.228 +theorem meet_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
2.229 +proof (rule meetI)
2.230 + show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x \<sqinter> y"
2.231 + proof
2.232 + show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x" ..
2.233 + show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y"
2.234 + proof -
2.235 + have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" ..
2.236 + also have "\<dots> \<sqsubseteq> y" ..
2.237 + finally show ?thesis .
2.238 + qed
2.239 + qed
2.240 + show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> z"
2.241 + proof -
2.242 + have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" ..
2.243 + also have "\<dots> \<sqsubseteq> z" ..
2.244 + finally show ?thesis .
2.245 + qed
2.246 + fix w assume "w \<sqsubseteq> x \<sqinter> y" and "w \<sqsubseteq> z"
2.247 + show "w \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
2.248 + proof
2.249 + show "w \<sqsubseteq> x"
2.250 + proof -
2.251 + have "w \<sqsubseteq> x \<sqinter> y" by fact
2.252 + also have "\<dots> \<sqsubseteq> x" ..
2.253 + finally show ?thesis .
2.254 + qed
2.255 + show "w \<sqsubseteq> y \<sqinter> z"
2.256 + proof
2.257 + show "w \<sqsubseteq> y"
2.258 + proof -
2.259 + have "w \<sqsubseteq> x \<sqinter> y" by fact
2.260 + also have "\<dots> \<sqsubseteq> y" ..
2.261 + finally show ?thesis .
2.262 + qed
2.263 + show "w \<sqsubseteq> z" by fact
2.264 + qed
2.265 + qed
2.266 +qed
2.267 +
2.268 +theorem meet_commute: "x \<sqinter> y = y \<sqinter> x"
2.269 +proof (rule meetI)
2.270 + show "y \<sqinter> x \<sqsubseteq> x" ..
2.271 + show "y \<sqinter> x \<sqsubseteq> y" ..
2.272 + fix z assume "z \<sqsubseteq> y" and "z \<sqsubseteq> x"
2.273 + then show "z \<sqsubseteq> y \<sqinter> x" ..
2.274 +qed
2.275 +
2.276 +theorem meet_join_absorb: "x \<sqinter> (x \<squnion> y) = x"
2.277 +proof (rule meetI)
2.278 + show "x \<sqsubseteq> x" ..
2.279 + show "x \<sqsubseteq> x \<squnion> y" ..
2.280 + fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> x \<squnion> y"
2.281 + show "z \<sqsubseteq> x" by fact
2.282 +qed
2.283 +
2.284 +theorem join_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
2.285 +proof (rule joinI)
2.286 + show "x \<squnion> y \<sqsubseteq> x \<squnion> (y \<squnion> z)"
2.287 + proof
2.288 + show "x \<sqsubseteq> x \<squnion> (y \<squnion> z)" ..
2.289 + show "y \<sqsubseteq> x \<squnion> (y \<squnion> z)"
2.290 + proof -
2.291 + have "y \<sqsubseteq> y \<squnion> z" ..
2.292 + also have "... \<sqsubseteq> x \<squnion> (y \<squnion> z)" ..
2.293 + finally show ?thesis .
2.294 + qed
2.295 + qed
2.296 + show "z \<sqsubseteq> x \<squnion> (y \<squnion> z)"
2.297 + proof -
2.298 + have "z \<sqsubseteq> y \<squnion> z" ..
2.299 + also have "... \<sqsubseteq> x \<squnion> (y \<squnion> z)" ..
2.300 + finally show ?thesis .
2.301 + qed
2.302 + fix w assume "x \<squnion> y \<sqsubseteq> w" and "z \<sqsubseteq> w"
2.303 + show "x \<squnion> (y \<squnion> z) \<sqsubseteq> w"
2.304 + proof
2.305 + show "x \<sqsubseteq> w"
2.306 + proof -
2.307 + have "x \<sqsubseteq> x \<squnion> y" ..
2.308 + also have "\<dots> \<sqsubseteq> w" by fact
2.309 + finally show ?thesis .
2.310 + qed
2.311 + show "y \<squnion> z \<sqsubseteq> w"
2.312 + proof
2.313 + show "y \<sqsubseteq> w"
2.314 + proof -
2.315 + have "y \<sqsubseteq> x \<squnion> y" ..
2.316 + also have "... \<sqsubseteq> w" by fact
2.317 + finally show ?thesis .
2.318 + qed
2.319 + show "z \<sqsubseteq> w" by fact
2.320 + qed
2.321 + qed
2.322 +qed
2.323 +
2.324 +theorem join_commute: "x \<squnion> y = y \<squnion> x"
2.325 +proof (rule joinI)
2.326 + show "x \<sqsubseteq> y \<squnion> x" ..
2.327 + show "y \<sqsubseteq> y \<squnion> x" ..
2.328 + fix z assume "y \<sqsubseteq> z" and "x \<sqsubseteq> z"
2.329 + then show "y \<squnion> x \<sqsubseteq> z" ..
2.330 +qed
2.331 +
2.332 +theorem join_meet_absorb: "x \<squnion> (x \<sqinter> y) = x"
2.333 +proof (rule joinI)
2.334 + show "x \<sqsubseteq> x" ..
2.335 + show "x \<sqinter> y \<sqsubseteq> x" ..
2.336 + fix z assume "x \<sqsubseteq> z" and "x \<sqinter> y \<sqsubseteq> z"
2.337 + show "x \<sqsubseteq> z" by fact
2.338 +qed
2.339 +
2.340 +theorem meet_idem: "x \<sqinter> x = x"
2.341 +proof -
2.342 + have "x \<sqinter> (x \<squnion> (x \<sqinter> x)) = x" by (rule meet_join_absorb)
2.343 + also have "x \<squnion> (x \<sqinter> x) = x" by (rule join_meet_absorb)
2.344 + finally show ?thesis .
2.345 +qed
2.346 +
2.347 +theorem meet_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
2.348 +proof (rule meetI)
2.349 + assume "x \<sqsubseteq> y"
2.350 + show "x \<sqsubseteq> x" ..
2.351 + show "x \<sqsubseteq> y" by fact
2.352 + fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y"
2.353 + show "z \<sqsubseteq> x" by fact
2.354 +qed
2.355 +
2.356 +theorem meet_related2 [elim?]: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
2.357 + by (drule meet_related) (simp add: meet_commute)
2.358 +
2.359 +theorem join_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
2.360 +proof (rule joinI)
2.361 + assume "x \<sqsubseteq> y"
2.362 + show "y \<sqsubseteq> y" ..
2.363 + show "x \<sqsubseteq> y" by fact
2.364 + fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z"
2.365 + show "y \<sqsubseteq> z" by fact
2.366 +qed
2.367 +
2.368 +theorem join_related2 [elim?]: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
2.369 + by (drule join_related) (simp add: join_commute)
2.370 +
2.371 +
2.372 +text {* Additional theorems *}
2.373 +
2.374 +theorem meet_connection: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)"
2.375 +proof
2.376 + assume "x \<sqsubseteq> y"
2.377 + then have "is_inf x y x" ..
2.378 + then show "x \<sqinter> y = x" ..
2.379 +next
2.380 + have "x \<sqinter> y \<sqsubseteq> y" ..
2.381 + also assume "x \<sqinter> y = x"
2.382 + finally show "x \<sqsubseteq> y" .
2.383 +qed
2.384 +
2.385 +theorem meet_connection2: "(x \<sqsubseteq> y) = (y \<sqinter> x = x)"
2.386 + using meet_commute meet_connection by simp
2.387 +
2.388 +theorem join_connection: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"
2.389 +proof
2.390 + assume "x \<sqsubseteq> y"
2.391 + then have "is_sup x y y" ..
2.392 + then show "x \<squnion> y = y" ..
2.393 +next
2.394 + have "x \<sqsubseteq> x \<squnion> y" ..
2.395 + also assume "x \<squnion> y = y"
2.396 + finally show "x \<sqsubseteq> y" .
2.397 +qed
2.398 +
2.399 +theorem join_connection2: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"
2.400 + using join_commute join_connection by simp
2.401 +
2.402 +
2.403 +text {* Naming according to Jacobson I, p.\ 459. *}
2.404 +
2.405 +lemmas L1 = join_commute meet_commute
2.406 +lemmas L2 = join_assoc meet_assoc
2.407 +(*lemmas L3 = join_idem meet_idem*)
2.408 +lemmas L4 = join_meet_absorb meet_join_absorb
2.409 +
2.410 +end
2.411 +
2.412 +locale ddlat = dlat +
2.413 + assumes meet_distr:
2.414 + "dlat.meet le x (dlat.join le y z) =
2.415 + dlat.join le (dlat.meet le x y) (dlat.meet le x z)"
2.416 +
2.417 +begin
2.418 +
2.419 +lemma join_distr:
2.420 + "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
2.421 + txt {* Jacobson I, p.\ 462 *}
2.422 +proof -
2.423 + have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by (simp add: L4)
2.424 + also have "... = x \<squnion> ((x \<sqinter> z) \<squnion> (y \<sqinter> z))" by (simp add: L2)
2.425 + also have "... = x \<squnion> ((x \<squnion> y) \<sqinter> z)" by (simp add: L1 meet_distr)
2.426 + also have "... = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)" by (simp add: L1 L4)
2.427 + also have "... = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by (simp add: meet_distr)
2.428 + finally show ?thesis .
2.429 +qed
2.430 +
2.431 +end
2.432 +
2.433 +locale dlo = dpo +
2.434 + assumes total: "x \<sqsubseteq> y | y \<sqsubseteq> x"
2.435 +
2.436 +begin
2.437 +
2.438 +lemma less_total: "x \<sqsubset> y | x = y | y \<sqsubset> x"
2.439 + using total
2.440 + by (unfold less_def) blast
2.441 +
2.442 +end
2.443 +
2.444 +
2.445 +interpretation dlo < dlat
2.446 +(* TODO: definition syntax is unavailable *)
2.447 +proof unfold_locales
2.448 + fix x y
2.449 + from total have "is_inf x y (if x \<sqsubseteq> y then x else y)" by (auto simp: is_inf_def)
2.450 + then show "EX inf. is_inf x y inf" by blast
2.451 +next
2.452 + fix x y
2.453 + from total have "is_sup x y (if x \<sqsubseteq> y then y else x)" by (auto simp: is_sup_def)
2.454 + then show "EX sup. is_sup x y sup" by blast
2.455 +qed
2.456 +
2.457 +interpretation dlo < ddlat
2.458 +proof unfold_locales
2.459 + fix x y z
2.460 + show "x \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> z" (is "?l = ?r")
2.461 + txt {* Jacobson I, p.\ 462 *}
2.462 + proof -
2.463 + { assume c: "y \<sqsubseteq> x" "z \<sqsubseteq> x"
2.464 + from c have "?l = y \<squnion> z"
2.465 + by (metis c (*join_commute*) join_connection2 join_related2 (*meet_commute*) meet_connection meet_related2 total)
2.466 + also from c have "... = ?r" by (metis (*c*) (*join_commute*) meet_related2)
2.467 + finally have "?l = ?r" . }
2.468 + moreover
2.469 + { assume c: "x \<sqsubseteq> y | x \<sqsubseteq> z"
2.470 + from c have "?l = x"
2.471 + by (metis (*anti_sym*) (*c*) (*circular*) (*join_assoc*)(* join_commute *) join_connection2 (*join_left*) join_related2 meet_connection(* meet_related2*) total trans)
2.472 + also from c have "... = ?r"
2.473 + by (metis join_commute join_related2 meet_connection meet_related2 total)
2.474 + finally have "?l = ?r" . }
2.475 + moreover note total
2.476 + ultimately show ?thesis by blast
2.477 + qed
2.478 +qed
2.479 +
2.480 +subsubsection {* Total order @{text "<="} on @{typ int} *}
2.481 +
2.482 +interpretation int: dpo ["op <= :: [int, int] => bool"]
2.483 + where "(dpo.less (op <=) (x::int) y) = (x < y)"
2.484 + txt {* We give interpretation for less, but not is\_inf and is\_sub. *}
2.485 +proof -
2.486 + show "dpo (op <= :: [int, int] => bool)"
2.487 + by unfold_locales auto
2.488 + then interpret int: dpo ["op <= :: [int, int] => bool"] .
2.489 + txt {* Gives interpreted version of less\_def (without condition). *}
2.490 + show "(dpo.less (op <=) (x::int) y) = (x < y)"
2.491 + by (unfold int.less_def) auto
2.492 +qed
2.493 +
2.494 +thm int.circular
2.495 +lemma "\<lbrakk> (x::int) \<le> y; y \<le> z; z \<le> x\<rbrakk> \<Longrightarrow> x = y \<and> y = z"
2.496 + apply (rule int.circular) apply assumption apply assumption apply assumption done
2.497 +thm int.abs_test
2.498 +lemma "(op < :: [int, int] => bool) = op <"
2.499 + apply (rule int.abs_test) done
2.500 +
2.501 +interpretation int: dlat ["op <= :: [int, int] => bool"]
2.502 + where "dlat.meet (op <=) (x::int) y = min x y"
2.503 + and "dlat.join (op <=) (x::int) y = max x y"
2.504 +proof -
2.505 + show "dlat (op <= :: [int, int] => bool)"
2.506 + apply unfold_locales
2.507 + apply (unfold int.is_inf_def int.is_sup_def)
2.508 + apply arith+
2.509 + done
2.510 + then interpret int: dlat ["op <= :: [int, int] => bool"] .
2.511 + txt {* Interpretation to ease use of definitions, which are
2.512 + conditional in general but unconditional after interpretation. *}
2.513 + show "dlat.meet (op <=) (x::int) y = min x y"
2.514 + apply (unfold int.meet_def)
2.515 + apply (rule the_equality)
2.516 + apply (unfold int.is_inf_def)
2.517 + by auto
2.518 + show "dlat.join (op <=) (x::int) y = max x y"
2.519 + apply (unfold int.join_def)
2.520 + apply (rule the_equality)
2.521 + apply (unfold int.is_sup_def)
2.522 + by auto
2.523 +qed
2.524 +
2.525 +interpretation int: dlo ["op <= :: [int, int] => bool"]
2.526 + by unfold_locales arith
2.527 +
2.528 +text {* Interpreted theorems from the locales, involving defined terms. *}
2.529 +
2.530 +thm int.less_def text {* from dpo *}
2.531 +thm int.meet_left text {* from dlat *}
2.532 +thm int.meet_distr text {* from ddlat *}
2.533 +thm int.less_total text {* from dlo *}
2.534 +
2.535 +
2.536 +subsubsection {* Total order @{text "<="} on @{typ nat} *}
2.537 +
2.538 +interpretation nat: dpo ["op <= :: [nat, nat] => bool"]
2.539 + where "dpo.less (op <=) (x::nat) y = (x < y)"
2.540 + txt {* We give interpretation for less, but not is\_inf and is\_sub. *}
2.541 +proof -
2.542 + show "dpo (op <= :: [nat, nat] => bool)"
2.543 + by unfold_locales auto
2.544 + then interpret nat: dpo ["op <= :: [nat, nat] => bool"] .
2.545 + txt {* Gives interpreted version of less\_def (without condition). *}
2.546 + show "dpo.less (op <=) (x::nat) y = (x < y)"
2.547 + apply (unfold nat.less_def)
2.548 + apply auto
2.549 + done
2.550 +qed
2.551 +
2.552 +interpretation nat: dlat ["op <= :: [nat, nat] => bool"]
2.553 + where "dlat.meet (op <=) (x::nat) y = min x y"
2.554 + and "dlat.join (op <=) (x::nat) y = max x y"
2.555 +proof -
2.556 + show "dlat (op <= :: [nat, nat] => bool)"
2.557 + apply unfold_locales
2.558 + apply (unfold nat.is_inf_def nat.is_sup_def)
2.559 + apply arith+
2.560 + done
2.561 + then interpret nat: dlat ["op <= :: [nat, nat] => bool"] .
2.562 + txt {* Interpretation to ease use of definitions, which are
2.563 + conditional in general but unconditional after interpretation. *}
2.564 + show "dlat.meet (op <=) (x::nat) y = min x y"
2.565 + apply (unfold nat.meet_def)
2.566 + apply (rule the_equality)
2.567 + apply (unfold nat.is_inf_def)
2.568 + by auto
2.569 + show "dlat.join (op <=) (x::nat) y = max x y"
2.570 + apply (unfold nat.join_def)
2.571 + apply (rule the_equality)
2.572 + apply (unfold nat.is_sup_def)
2.573 + by auto
2.574 +qed
2.575 +
2.576 +interpretation nat: dlo ["op <= :: [nat, nat] => bool"]
2.577 + by unfold_locales arith
2.578 +
2.579 +text {* Interpreted theorems from the locales, involving defined terms. *}
2.580 +
2.581 +thm nat.less_def text {* from dpo *}
2.582 +thm nat.meet_left text {* from dlat *}
2.583 +thm nat.meet_distr text {* from ddlat *}
2.584 +thm nat.less_total text {* from ldo *}
2.585 +
2.586 +
2.587 +subsubsection {* Lattice @{text "dvd"} on @{typ nat} *}
2.588 +
2.589 +interpretation nat_dvd: dpo ["op dvd :: [nat, nat] => bool"]
2.590 + where "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)"
2.591 + txt {* We give interpretation for less, but not is\_inf and is\_sub. *}
2.592 +proof -
2.593 + show "dpo (op dvd :: [nat, nat] => bool)"
2.594 + by unfold_locales (auto simp: dvd_def)
2.595 + then interpret nat_dvd: dpo ["op dvd :: [nat, nat] => bool"] .
2.596 + txt {* Gives interpreted version of less\_def (without condition). *}
2.597 + show "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)"
2.598 + apply (unfold nat_dvd.less_def)
2.599 + apply auto
2.600 + done
2.601 +qed
2.602 +
2.603 +interpretation nat_dvd: dlat ["op dvd :: [nat, nat] => bool"]
2.604 + where "dlat.meet (op dvd) (x::nat) y = gcd (x, y)"
2.605 + and "dlat.join (op dvd) (x::nat) y = lcm (x, y)"
2.606 +proof -
2.607 + show "dlat (op dvd :: [nat, nat] => bool)"
2.608 + apply unfold_locales
2.609 + apply (unfold nat_dvd.is_inf_def nat_dvd.is_sup_def)
2.610 + apply (rule_tac x = "gcd (x, y)" in exI)
2.611 + apply auto [1]
2.612 + apply (rule_tac x = "lcm (x, y)" in exI)
2.613 + apply (auto intro: lcm_dvd1 lcm_dvd2 lcm_lowest)
2.614 + done
2.615 + then interpret nat_dvd: dlat ["op dvd :: [nat, nat] => bool"] .
2.616 + txt {* Interpretation to ease use of definitions, which are
2.617 + conditional in general but unconditional after interpretation. *}
2.618 + show "dlat.meet (op dvd) (x::nat) y = gcd (x, y)"
2.619 + apply (unfold nat_dvd.meet_def)
2.620 + apply (rule the_equality)
2.621 + apply (unfold nat_dvd.is_inf_def)
2.622 + by auto
2.623 + show "dlat.join (op dvd) (x::nat) y = lcm (x, y)"
2.624 + apply (unfold nat_dvd.join_def)
2.625 + apply (rule the_equality)
2.626 + apply (unfold nat_dvd.is_sup_def)
2.627 + by (auto intro: lcm_dvd1 lcm_dvd2 lcm_lowest)
2.628 +qed
2.629 +
2.630 +text {* Interpreted theorems from the locales, involving defined terms. *}
2.631 +
2.632 +thm nat_dvd.less_def text {* from dpo *}
2.633 +lemma "((x::nat) dvd y & x ~= y) = (x dvd y & x ~= y)"
2.634 + apply (rule nat_dvd.less_def) done
2.635 +thm nat_dvd.meet_left text {* from dlat *}
2.636 +lemma "gcd (x, y) dvd x"
2.637 + apply (rule nat_dvd.meet_left) done
2.638 +
2.639 +print_interps dpo
2.640 +print_interps dlat
2.641 +
2.642 +
2.643 +subsection {* Group example with defined operations @{text inv} and @{text unit} *}
2.644 +
2.645 +subsubsection {* Locale declarations and lemmas *}
2.646
2.647 locale Dsemi =
2.648 fixes prod (infixl "**" 65)
2.649 @@ -32,128 +641,279 @@
2.650
2.651 locale Dmonoid = Dsemi +
2.652 fixes one
2.653 - assumes lone: "one ** x = x"
2.654 - and rone: "x ** one = x"
2.655 + assumes l_one [simp]: "one ** x = x"
2.656 + and r_one [simp]: "x ** one = x"
2.657
2.658 -definition (in Dmonoid)
2.659 - inv where "inv(x) == THE y. x ** y = one & y ** x = one"
2.660 +begin
2.661
2.662 -lemma (in Dmonoid) inv_unique:
2.663 +definition
2.664 + inv where "inv x = (THE y. x ** y = one & y ** x = one)"
2.665 +definition
2.666 + unit where "unit x = (EX y. x ** y = one & y ** x = one)"
2.667 +
2.668 +lemma inv_unique:
2.669 assumes eq: "y ** x = one" "x ** y' = one"
2.670 shows "y = y'"
2.671 proof -
2.672 - from eq have "y = y ** (x ** y')" by (simp add: rone)
2.673 + from eq have "y = y ** (x ** y')" by (simp add: r_one)
2.674 also have "... = (y ** x) ** y'" by (simp add: assoc)
2.675 - also from eq have "... = y'" by (simp add: lone)
2.676 + also from eq have "... = y'" by (simp add: l_one)
2.677 finally show ?thesis .
2.678 qed
2.679
2.680 +lemma unit_one [intro, simp]:
2.681 + "unit one"
2.682 + by (unfold unit_def) auto
2.683 +
2.684 +lemma unit_l_inv_ex:
2.685 + "unit x ==> \<exists>y. y ** x = one"
2.686 + by (unfold unit_def) auto
2.687 +
2.688 +lemma unit_r_inv_ex:
2.689 + "unit x ==> \<exists>y. x ** y = one"
2.690 + by (unfold unit_def) auto
2.691 +
2.692 +lemma unit_l_inv:
2.693 + "unit x ==> inv x ** x = one"
2.694 + apply (simp add: unit_def inv_def) apply (erule exE)
2.695 + apply (rule theI2, fast)
2.696 + apply (rule inv_unique)
2.697 + apply fast+
2.698 + done
2.699 +
2.700 +lemma unit_r_inv:
2.701 + "unit x ==> x ** inv x = one"
2.702 + apply (simp add: unit_def inv_def) apply (erule exE)
2.703 + apply (rule theI2, fast)
2.704 + apply (rule inv_unique)
2.705 + apply fast+
2.706 + done
2.707 +
2.708 +lemma unit_inv_unit [intro, simp]:
2.709 + "unit x ==> unit (inv x)"
2.710 +proof -
2.711 + assume x: "unit x"
2.712 + show "unit (inv x)"
2.713 + by (auto simp add: unit_def
2.714 + intro: unit_l_inv unit_r_inv x)
2.715 +qed
2.716 +
2.717 +lemma unit_l_cancel [simp]:
2.718 + "unit x ==> (x ** y = x ** z) = (y = z)"
2.719 +proof
2.720 + assume eq: "x ** y = x ** z"
2.721 + and G: "unit x"
2.722 + then have "(inv x ** x) ** y = (inv x ** x) ** z"
2.723 + by (simp add: assoc)
2.724 + with G show "y = z" by (simp add: unit_l_inv)
2.725 +next
2.726 + assume eq: "y = z"
2.727 + and G: "unit x"
2.728 + then show "x ** y = x ** z" by simp
2.729 +qed
2.730 +
2.731 +lemma unit_inv_inv [simp]:
2.732 + "unit x ==> inv (inv x) = x"
2.733 +proof -
2.734 + assume x: "unit x"
2.735 + then have "inv x ** inv (inv x) = inv x ** x"
2.736 + by (simp add: unit_l_inv unit_r_inv)
2.737 + with x show ?thesis by simp
2.738 +qed
2.739 +
2.740 +lemma inv_inj_on_unit:
2.741 + "inj_on inv {x. unit x}"
2.742 +proof (rule inj_onI, simp)
2.743 + fix x y
2.744 + assume G: "unit x" "unit y" and eq: "inv x = inv y"
2.745 + then have "inv (inv x) = inv (inv y)" by simp
2.746 + with G show "x = y" by simp
2.747 +qed
2.748 +
2.749 +lemma unit_inv_comm:
2.750 + assumes inv: "x ** y = one"
2.751 + and G: "unit x" "unit y"
2.752 + shows "y ** x = one"
2.753 +proof -
2.754 + from G have "x ** y ** x = x ** one" by (auto simp add: inv)
2.755 + with G show ?thesis by (simp del: r_one add: assoc)
2.756 +qed
2.757 +
2.758 +end
2.759 +
2.760 +
2.761 locale Dgrp = Dmonoid +
2.762 - assumes linv_ex: "EX y. y ** x = one"
2.763 - and rinv_ex: "EX y. x ** y = one"
2.764 + assumes unit [intro, simp]: "Dmonoid.unit (op **) one x"
2.765
2.766 -lemma (in Dgrp) linv:
2.767 +begin
2.768 +
2.769 +lemma l_inv_ex [simp]:
2.770 + "\<exists>y. y ** x = one"
2.771 + using unit_l_inv_ex by simp
2.772 +
2.773 +lemma r_inv_ex [simp]:
2.774 + "\<exists>y. x ** y = one"
2.775 + using unit_r_inv_ex by simp
2.776 +
2.777 +lemma l_inv [simp]:
2.778 "inv x ** x = one"
2.779 -apply (unfold inv_def)
2.780 -apply (insert rinv_ex [where x = x])
2.781 -apply (insert linv_ex [where x = x])
2.782 -apply (erule exE) apply (erule exE)
2.783 -apply (rule theI2)
2.784 -apply rule apply assumption
2.785 -apply (frule inv_unique, assumption)
2.786 -apply simp
2.787 -apply (rule inv_unique)
2.788 -apply fast+
2.789 -done
2.790 + using unit_l_inv by simp
2.791
2.792 -lemma (in Dgrp) rinv:
2.793 +lemma l_cancel [simp]:
2.794 + "(x ** y = x ** z) = (y = z)"
2.795 + using unit_l_inv by simp
2.796 +
2.797 +lemma r_inv [simp]:
2.798 "x ** inv x = one"
2.799 -apply (unfold inv_def)
2.800 -apply (insert rinv_ex [where x = x])
2.801 -apply (insert linv_ex [where x = x])
2.802 -apply (erule exE) apply (erule exE)
2.803 -apply (rule theI2)
2.804 -apply rule apply assumption
2.805 -apply (frule inv_unique, assumption)
2.806 -apply simp
2.807 -apply (rule inv_unique)
2.808 -apply fast+
2.809 -done
2.810 +proof -
2.811 + have "inv x ** (x ** inv x) = inv x ** one"
2.812 + by (simp add: assoc [symmetric] l_inv)
2.813 + then show ?thesis by (simp del: r_one)
2.814 +qed
2.815
2.816 -lemma (in Dgrp) lcancel:
2.817 - "x ** y = x ** z <-> y = z"
2.818 +lemma r_cancel [simp]:
2.819 + "(y ** x = z ** x) = (y = z)"
2.820 proof
2.821 - assume "x ** y = x ** z"
2.822 - then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
2.823 - then show "y = z" by (simp add: lone linv)
2.824 + assume eq: "y ** x = z ** x"
2.825 + then have "y ** (x ** inv x) = z ** (x ** inv x)"
2.826 + by (simp add: assoc [symmetric] del: r_inv)
2.827 + then show "y = z" by simp
2.828 qed simp
2.829
2.830 -interpretation Dint: Dmonoid ["op +" "0::int"]
2.831 - where "Dmonoid.inv (op +) (0::int)" = "uminus"
2.832 +lemma inv_one [simp]:
2.833 + "inv one = one"
2.834 proof -
2.835 - show "Dmonoid (op +) (0::int)" by unfold_locales auto
2.836 - note Dint = this (* should have this as an assumption in further goals *)
2.837 - {
2.838 - fix x
2.839 - have "Dmonoid.inv (op +) (0::int) x = - x"
2.840 - by (auto simp: Dmonoid.inv_def [OF Dint])
2.841 - }
2.842 - then show "Dmonoid.inv (op +) (0::int) == uminus"
2.843 - by (rule_tac eq_reflection) (fast intro: ext)
2.844 + have "inv one = one ** (inv one)" by (simp del: r_inv)
2.845 + moreover have "... = one" by simp
2.846 + finally show ?thesis .
2.847 qed
2.848
2.849 -thm Dmonoid.inv_def Dint.inv_def
2.850 +lemma inv_inv [simp]:
2.851 + "inv (inv x) = x"
2.852 + using unit_inv_inv by simp
2.853
2.854 -lemma "- x \<equiv> THE y. x + y = 0 \<and> y + x = (0::int)"
2.855 - apply (rule Dint.inv_def) done
2.856 +lemma inv_inj:
2.857 + "inj_on inv UNIV"
2.858 + using inv_inj_on_unit by simp
2.859
2.860 -interpretation Dclass: Dmonoid ["op +" "0::'a::ab_group_add"]
2.861 - where "Dmonoid.inv (op +) (0::'a::ab_group_add)" = "uminus"
2.862 +lemma inv_mult_group:
2.863 + "inv (x ** y) = inv y ** inv x"
2.864 proof -
2.865 - show "Dmonoid (op +) (0::'a::ab_group_add)" by unfold_locales auto
2.866 - note Dclass = this (* should have this as an assumption in further goals *)
2.867 - {
2.868 - fix x
2.869 - have "Dmonoid.inv (op +) (0::'a::ab_group_add) x = - x"
2.870 - by (auto simp: Dmonoid.inv_def [OF Dclass] equals_zero_I [symmetric])
2.871 - }
2.872 - then show "Dmonoid.inv (op +) (0::'a::ab_group_add) == uminus"
2.873 - by (rule_tac eq_reflection) (fast intro: ext)
2.874 + have "inv (x ** y) ** (x ** y) = (inv y ** inv x) ** (x ** y)"
2.875 + by (simp add: assoc l_inv) (simp add: assoc [symmetric])
2.876 + then show ?thesis by (simp del: l_inv)
2.877 qed
2.878
2.879 -interpretation Dclass: Dgrp ["op +" "0::'a::ring"]
2.880 -apply unfold_locales
2.881 -apply (rule_tac x="-x" in exI) apply simp
2.882 -apply (rule_tac x="-x" in exI) apply simp
2.883 -done
2.884 +lemma inv_comm:
2.885 + "x ** y = one ==> y ** x = one"
2.886 + by (rule unit_inv_comm) auto
2.887
2.888 -(* Equation for inverse from Dclass: Dmonoid effective. *)
2.889 +lemma inv_equality:
2.890 + "y ** x = one ==> inv x = y"
2.891 + apply (simp add: inv_def)
2.892 + apply (rule the_equality)
2.893 + apply (simp add: inv_comm [of y x])
2.894 + apply (rule r_cancel [THEN iffD1], auto)
2.895 + done
2.896
2.897 -thm Dclass.linv
2.898 -lemma "-x + x = (0::'a::ring)" apply (rule Dclass.linv) done
2.899 +end
2.900
2.901 -(* Equations have effect in "subscriptions" *)
2.902
2.903 -(* In the same module *)
2.904 +locale Dhom = Dgrp prod (infixl "**" 65) one + Dgrp sum (infixl "+++" 60) zero +
2.905 + fixes hom
2.906 + assumes hom_mult [simp]: "hom (x ** y) = hom x +++ hom y"
2.907
2.908 -lemma (in Dmonoid) trivial:
2.909 - "inv one = inv one"
2.910 - by rule
2.911 +begin
2.912
2.913 -thm Dclass.trivial
2.914 -
2.915 -(* Inherited: interpretation *)
2.916 -
2.917 -lemma (in Dgrp) inv_inv:
2.918 - "inv (inv x) = x"
2.919 +lemma hom_one [simp]:
2.920 + "hom one = zero"
2.921 proof -
2.922 - have "inv x ** inv (inv x) = inv x ** x"
2.923 - by (simp add: linv rinv)
2.924 - then show ?thesis by (simp add: lcancel)
2.925 + have "hom one +++ zero = hom one +++ hom one"
2.926 + by (simp add: hom_mult [symmetric] del: hom_mult)
2.927 + then show ?thesis by (simp del: r_one)
2.928 qed
2.929
2.930 -thm Dclass.inv_inv
2.931 -lemma "- (- x) = (x::'a::ring)"
2.932 - apply (rule Dclass.inv_inv) done
2.933 +end
2.934 +
2.935 +
2.936 +subsubsection {* Interpretation of Functions *}
2.937 +
2.938 +interpretation Dfun: Dmonoid ["op o" "id :: 'a => 'a"]
2.939 + where "Dmonoid.unit (op o) id f = bij (f::'a => 'a)"
2.940 +(* and "Dmonoid.inv (op o) id" = "inv :: ('a => 'a) => ('a => 'a)" *)
2.941 +proof -
2.942 + show "Dmonoid op o (id :: 'a => 'a)" by unfold_locales (simp_all add: o_assoc)
2.943 + note Dmonoid = this
2.944 +(*
2.945 + from this interpret Dmonoid ["op o" "id :: 'a => 'a"] .
2.946 +*)
2.947 + show "Dmonoid.unit (op o) (id :: 'a => 'a) f = bij f"
2.948 + apply (unfold Dmonoid.unit_def [OF Dmonoid])
2.949 + apply rule apply clarify
2.950 + proof -
2.951 + fix f g
2.952 + assume id1: "f o g = id" and id2: "g o f = id"
2.953 + show "bij f"
2.954 + proof (rule bijI)
2.955 + show "inj f"
2.956 + proof (rule inj_onI)
2.957 + fix x y
2.958 + assume "f x = f y"
2.959 + then have "(g o f) x = (g o f) y" by simp
2.960 + with id2 show "x = y" by simp
2.961 + qed
2.962 + next
2.963 + show "surj f"
2.964 + proof (rule surjI)
2.965 + fix x
2.966 + from id1 have "(f o g) x = x" by simp
2.967 + then show "f (g x) = x" by simp
2.968 + qed
2.969 + qed
2.970 + next
2.971 + fix f
2.972 + assume bij: "bij f"
2.973 + then
2.974 + have inv: "f o Hilbert_Choice.inv f = id & Hilbert_Choice.inv f o f = id"
2.975 + by (simp add: bij_def surj_iff inj_iff)
2.976 + show "EX g. f o g = id & g o f = id" by rule (rule inv)
2.977 + qed
2.978 +qed
2.979 +
2.980 +thm Dmonoid.unit_def Dfun.unit_def
2.981 +
2.982 +thm Dmonoid.inv_inj_on_unit Dfun.inv_inj_on_unit
2.983 +
2.984 +lemma unit_id:
2.985 + "(f :: unit => unit) = id"
2.986 + by rule simp
2.987 +
2.988 +interpretation Dfun: Dgrp ["op o" "id :: unit => unit"]
2.989 + where "Dmonoid.inv (op o) id f = inv (f :: unit => unit)"
2.990 +proof -
2.991 + have "Dmonoid op o (id :: 'a => 'a)" by unfold_locales (simp_all add: o_assoc)
2.992 + note Dmonoid = this
2.993 +
2.994 + show "Dgrp (op o) (id :: unit => unit)"
2.995 +apply unfold_locales
2.996 +apply (unfold Dmonoid.unit_def [OF Dmonoid])
2.997 +apply (insert unit_id)
2.998 +apply simp
2.999 +done
2.1000 + show "Dmonoid.inv (op o) id f = inv (f :: unit => unit)"
2.1001 +apply (unfold Dmonoid.inv_def [OF Dmonoid] inv_def)
2.1002 +apply (insert unit_id)
2.1003 +apply simp
2.1004 +apply (rule the_equality)
2.1005 +apply rule
2.1006 +apply rule
2.1007 +apply simp
2.1008 +done
2.1009 +qed
2.1010 +
2.1011 +thm Dfun.unit_l_inv Dfun.l_inv
2.1012 +
2.1013 +thm Dfun.inv_equality
2.1014 +thm Dfun.inv_equality
2.1015
2.1016 end
3.1 --- a/src/Pure/Isar/spec_parse.ML Mon Jul 23 13:47:48 2007 +0200
3.2 +++ b/src/Pure/Isar/spec_parse.ML Mon Jul 23 13:48:30 2007 +0200
3.3 @@ -24,7 +24,7 @@
3.4 val locale_mixfix: token list -> mixfix * token list
3.5 val locale_fixes: token list -> (string * string option * mixfix) list * token list
3.6 val locale_insts: token list ->
3.7 - (string option list * (string * string) list) * token list
3.8 + (string option list * string list) * token list
3.9 val locale_expr: token list -> Locale.expr * token list
3.10 val locale_expr_unless: (token list -> 'a * token list) ->
3.11 token list -> Locale.expr * token list
3.12 @@ -88,7 +88,7 @@
3.13
3.14 val locale_insts =
3.15 Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) []
3.16 - -- Scan.optional (P.$$$ "where" |-- P.and_list1 (P.term -- (P.$$$ "=" |-- P.!!! P.term))) [];
3.17 + -- Scan.optional (P.$$$ "where" |-- P.and_list1 P.term) [];
3.18
3.19 local
3.20
4.1 --- a/src/Pure/Tools/class_package.ML Mon Jul 23 13:47:48 2007 +0200
4.2 +++ b/src/Pure/Tools/class_package.ML Mon Jul 23 13:48:30 2007 +0200
4.3 @@ -637,7 +637,7 @@
4.4 val def' = symmetric def
4.5 val tac = (ALLGOALS o ProofContext.fact_tac) [def'];
4.6 val name_locale = (#locale o the_class_data thy) class;
4.7 - val def_eq = (Logic.dest_equals o Thm.prop_of) def';
4.8 + val def_eq = Thm.prop_of def';
4.9 val (params, consts) = split_list (param_map thy [class]);
4.10 in
4.11 prove_interpretation tac ((false, prfx), []) (Locale.Locale name_locale)