interpretation: equations are propositions not pairs of terms;
authorballarin
Mon Jul 23 13:48:30 2007 +0200 (2007-07-23)
changeset 23919af871d13e320
parent 23918 a4abccde0929
child 23920 4288dc7dc248
interpretation: equations are propositions not pairs of terms;
src/FOL/ex/LocaleTest.thy
src/HOL/ex/LocaleTest2.thy
src/Pure/Isar/spec_parse.ML
src/Pure/Tools/class_package.ML
     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 +begin
   2.659  
   2.660 -definition (in Dmonoid)
   2.661 -  inv where "inv(x) == THE y. x ** y = one & y ** x = one"
   2.662 +definition
   2.663 +  inv where "inv x = (THE y. x ** y = one & y ** x = one)"
   2.664 +definition
   2.665 +  unit where "unit x = (EX y. x ** y = one  & y ** x = one)"
   2.666  
   2.667 -lemma (in Dmonoid) inv_unique:
   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 -locale Dgrp = Dmonoid +
   2.681 -  assumes linv_ex: "EX y. y ** x = one"
   2.682 -    and rinv_ex: "EX y. x ** y = one"
   2.683 +lemma unit_one [intro, simp]:
   2.684 +  "unit one"
   2.685 +  by (unfold unit_def) auto
   2.686 +
   2.687 +lemma unit_l_inv_ex:
   2.688 +  "unit x ==> \<exists>y. y ** x = one"
   2.689 +  by (unfold unit_def) auto
   2.690 +
   2.691 +lemma unit_r_inv_ex:
   2.692 +  "unit x ==> \<exists>y. x ** y = one"
   2.693 +  by (unfold unit_def) auto
   2.694 +
   2.695 +lemma unit_l_inv:
   2.696 +  "unit x ==> inv x ** x = one"
   2.697 +  apply (simp add: unit_def inv_def) apply (erule exE)
   2.698 +  apply (rule theI2, fast)
   2.699 +  apply (rule inv_unique)
   2.700 +  apply fast+
   2.701 +  done
   2.702  
   2.703 -lemma (in Dgrp) linv:
   2.704 -  "inv x ** x = one"
   2.705 -apply (unfold inv_def)
   2.706 -apply (insert rinv_ex [where x = x])
   2.707 -apply (insert linv_ex [where x = x])
   2.708 -apply (erule exE) apply (erule exE)
   2.709 -apply (rule theI2)
   2.710 -apply rule apply assumption
   2.711 -apply (frule inv_unique, assumption)
   2.712 -apply simp
   2.713 -apply (rule inv_unique)
   2.714 -apply fast+
   2.715 -done
   2.716 +lemma unit_r_inv:
   2.717 +  "unit x ==> x ** inv x = one"
   2.718 +  apply (simp add: unit_def inv_def) apply (erule exE)
   2.719 +  apply (rule theI2, fast)
   2.720 +  apply (rule inv_unique)
   2.721 +  apply fast+
   2.722 +  done
   2.723 +
   2.724 +lemma unit_inv_unit [intro, simp]:
   2.725 +  "unit x ==> unit (inv x)"
   2.726 +proof -
   2.727 +  assume x: "unit x"
   2.728 +  show "unit (inv x)"
   2.729 +    by (auto simp add: unit_def
   2.730 +      intro: unit_l_inv unit_r_inv x)
   2.731 +qed
   2.732 +
   2.733 +lemma unit_l_cancel [simp]:
   2.734 +  "unit x ==> (x ** y = x ** z) = (y = z)"
   2.735 +proof
   2.736 +  assume eq: "x ** y = x ** z"
   2.737 +    and G: "unit x"
   2.738 +  then have "(inv x ** x) ** y = (inv x ** x) ** z"
   2.739 +    by (simp add: assoc)
   2.740 +  with G show "y = z" by (simp add: unit_l_inv)
   2.741 +next
   2.742 +  assume eq: "y = z"
   2.743 +    and G: "unit x"
   2.744 +  then show "x ** y = x ** z" by simp
   2.745 +qed
   2.746  
   2.747 -lemma (in Dgrp) rinv:
   2.748 +lemma unit_inv_inv [simp]:
   2.749 +  "unit x ==> inv (inv x) = x"
   2.750 +proof -
   2.751 +  assume x: "unit x"
   2.752 +  then have "inv x ** inv (inv x) = inv x ** x"
   2.753 +    by (simp add: unit_l_inv unit_r_inv)
   2.754 +  with x show ?thesis by simp
   2.755 +qed
   2.756 +
   2.757 +lemma inv_inj_on_unit:
   2.758 +  "inj_on inv {x. unit x}"
   2.759 +proof (rule inj_onI, simp)
   2.760 +  fix x y
   2.761 +  assume G: "unit x"  "unit y" and eq: "inv x = inv y"
   2.762 +  then have "inv (inv x) = inv (inv y)" by simp
   2.763 +  with G show "x = y" by simp
   2.764 +qed
   2.765 +
   2.766 +lemma unit_inv_comm:
   2.767 +  assumes inv: "x ** y = one"
   2.768 +    and G: "unit x"  "unit y"
   2.769 +  shows "y ** x = one"
   2.770 +proof -
   2.771 +  from G have "x ** y ** x = x ** one" by (auto simp add: inv)
   2.772 +  with G show ?thesis by (simp del: r_one add: assoc)
   2.773 +qed
   2.774 +
   2.775 +end
   2.776 +
   2.777 +
   2.778 +locale Dgrp = Dmonoid +
   2.779 +  assumes unit [intro, simp]: "Dmonoid.unit (op **) one x"
   2.780 +
   2.781 +begin
   2.782 +
   2.783 +lemma l_inv_ex [simp]:
   2.784 +  "\<exists>y. y ** x = one"
   2.785 +  using unit_l_inv_ex by simp
   2.786 +
   2.787 +lemma r_inv_ex [simp]:
   2.788 +  "\<exists>y. x ** y = one"
   2.789 +  using unit_r_inv_ex by simp
   2.790 +
   2.791 +lemma l_inv [simp]:
   2.792 +  "inv x ** x = one"
   2.793 +  using unit_l_inv by simp
   2.794 +
   2.795 +lemma l_cancel [simp]:
   2.796 +  "(x ** y = x ** z) = (y = z)"
   2.797 +  using unit_l_inv by simp
   2.798 +
   2.799 +lemma r_inv [simp]:
   2.800    "x ** inv x = one"
   2.801 -apply (unfold inv_def)
   2.802 -apply (insert rinv_ex [where x = x])
   2.803 -apply (insert linv_ex [where x = x])
   2.804 -apply (erule exE) apply (erule exE)
   2.805 -apply (rule theI2)
   2.806 -apply rule apply assumption
   2.807 -apply (frule inv_unique, assumption)
   2.808 -apply simp
   2.809 -apply (rule inv_unique)
   2.810 -apply fast+
   2.811 -done
   2.812 +proof -
   2.813 +  have "inv x ** (x ** inv x) = inv x ** one"
   2.814 +    by (simp add: assoc [symmetric] l_inv)
   2.815 +  then show ?thesis by (simp del: r_one)
   2.816 +qed
   2.817  
   2.818 -lemma (in Dgrp) lcancel:
   2.819 -  "x ** y = x ** z <-> y = z"
   2.820 +lemma r_cancel [simp]:
   2.821 +  "(y ** x = z ** x) = (y = z)"
   2.822  proof
   2.823 -  assume "x ** y = x ** z"
   2.824 -  then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
   2.825 -  then show "y = z" by (simp add: lone linv)
   2.826 +  assume eq: "y ** x = z ** x"
   2.827 +  then have "y ** (x ** inv x) = z ** (x ** inv x)"
   2.828 +    by (simp add: assoc [symmetric] del: r_inv)
   2.829 +  then show "y = z" by simp
   2.830  qed simp
   2.831  
   2.832 -interpretation Dint: Dmonoid ["op +" "0::int"]
   2.833 -  where "Dmonoid.inv (op +) (0::int)" = "uminus"
   2.834 +lemma inv_one [simp]:
   2.835 +  "inv one = one"
   2.836  proof -
   2.837 -  show "Dmonoid (op +) (0::int)" by unfold_locales auto
   2.838 -  note Dint = this (* should have this as an assumption in further goals *)
   2.839 -  {
   2.840 -    fix x
   2.841 -    have "Dmonoid.inv (op +) (0::int) x = - x"
   2.842 -      by (auto simp: Dmonoid.inv_def [OF Dint])
   2.843 -  }
   2.844 -  then show "Dmonoid.inv (op +) (0::int) == uminus"
   2.845 -    by (rule_tac eq_reflection) (fast intro: ext)
   2.846 +  have "inv one = one ** (inv one)" by (simp del: r_inv)
   2.847 +  moreover have "... = one" by simp
   2.848 +  finally show ?thesis .
   2.849  qed
   2.850  
   2.851 -thm Dmonoid.inv_def Dint.inv_def
   2.852 +lemma inv_inv [simp]:
   2.853 +  "inv (inv x) = x"
   2.854 +  using unit_inv_inv by simp
   2.855  
   2.856 -lemma "- x \<equiv> THE y. x + y = 0 \<and> y + x = (0::int)"
   2.857 -  apply (rule Dint.inv_def) done
   2.858 +lemma inv_inj:
   2.859 +  "inj_on inv UNIV"
   2.860 +  using inv_inj_on_unit by simp
   2.861  
   2.862 -interpretation Dclass: Dmonoid ["op +" "0::'a::ab_group_add"]
   2.863 -  where "Dmonoid.inv (op +) (0::'a::ab_group_add)" = "uminus"
   2.864 +lemma inv_mult_group:
   2.865 +  "inv (x ** y) = inv y ** inv x"
   2.866  proof -
   2.867 -  show "Dmonoid (op +) (0::'a::ab_group_add)" by unfold_locales auto
   2.868 -  note Dclass = this (* should have this as an assumption in further goals *)
   2.869 -  {
   2.870 -    fix x
   2.871 -    have "Dmonoid.inv (op +) (0::'a::ab_group_add) x = - x"
   2.872 -      by (auto simp: Dmonoid.inv_def [OF Dclass] equals_zero_I [symmetric])
   2.873 -  }
   2.874 -  then show "Dmonoid.inv (op +) (0::'a::ab_group_add) == uminus"
   2.875 -    by (rule_tac eq_reflection) (fast intro: ext)
   2.876 +  have "inv (x ** y) ** (x ** y) = (inv y ** inv x) ** (x ** y)"
   2.877 +    by (simp add: assoc l_inv) (simp add: assoc [symmetric])
   2.878 +  then show ?thesis by (simp del: l_inv)
   2.879 +qed
   2.880 +
   2.881 +lemma inv_comm:
   2.882 +  "x ** y = one ==> y ** x = one"
   2.883 +  by (rule unit_inv_comm) auto
   2.884 +
   2.885 +lemma inv_equality:
   2.886 +     "y ** x = one ==> inv x = y"
   2.887 +  apply (simp add: inv_def)
   2.888 +  apply (rule the_equality)
   2.889 +   apply (simp add: inv_comm [of y x])
   2.890 +  apply (rule r_cancel [THEN iffD1], auto)
   2.891 +  done
   2.892 +
   2.893 +end
   2.894 +
   2.895 +
   2.896 +locale Dhom = Dgrp prod (infixl "**" 65) one + Dgrp sum (infixl "+++" 60) zero +
   2.897 +  fixes hom
   2.898 +  assumes hom_mult [simp]: "hom (x ** y) = hom x +++ hom y"
   2.899 +
   2.900 +begin
   2.901 +
   2.902 +lemma hom_one [simp]:
   2.903 +  "hom one = zero"
   2.904 +proof -
   2.905 +  have "hom one +++ zero = hom one +++ hom one"
   2.906 +    by (simp add: hom_mult [symmetric] del: hom_mult)
   2.907 +  then show ?thesis by (simp del: r_one)
   2.908  qed
   2.909  
   2.910 -interpretation Dclass: Dgrp ["op +" "0::'a::ring"]
   2.911 -apply unfold_locales
   2.912 -apply (rule_tac x="-x" in exI) apply simp
   2.913 -apply (rule_tac x="-x" in exI) apply simp
   2.914 -done
   2.915 +end
   2.916  
   2.917 -(* Equation for inverse from Dclass: Dmonoid effective. *)
   2.918  
   2.919 -thm Dclass.linv
   2.920 -lemma "-x + x = (0::'a::ring)" apply (rule Dclass.linv) done
   2.921 -
   2.922 -(* Equations have effect in "subscriptions" *)
   2.923 -
   2.924 -(* In the same module *)
   2.925 +subsubsection {* Interpretation of Functions *}
   2.926  
   2.927 -lemma (in Dmonoid) trivial:
   2.928 -  "inv one = inv one"
   2.929 -  by rule
   2.930 -
   2.931 -thm Dclass.trivial
   2.932 -
   2.933 -(* Inherited: interpretation *)
   2.934 -
   2.935 -lemma (in Dgrp) inv_inv:
   2.936 -  "inv (inv x) = x"
   2.937 +interpretation Dfun: Dmonoid ["op o" "id :: 'a => 'a"]
   2.938 +  where "Dmonoid.unit (op o) id f = bij (f::'a => 'a)"
   2.939 +(*    and "Dmonoid.inv (op o) id" = "inv :: ('a => 'a) => ('a => 'a)" *)
   2.940  proof -
   2.941 -  have "inv x ** inv (inv x) = inv x ** x"
   2.942 -    by (simp add: linv rinv)
   2.943 -  then show ?thesis by (simp add: lcancel)
   2.944 +  show "Dmonoid op o (id :: 'a => 'a)" by unfold_locales (simp_all add: o_assoc)
   2.945 +  note Dmonoid = this
   2.946 +(*
   2.947 +  from this interpret Dmonoid ["op o" "id :: 'a => 'a"] .
   2.948 +*)
   2.949 +  show "Dmonoid.unit (op o) (id :: 'a => 'a) f = bij f"
   2.950 +    apply (unfold Dmonoid.unit_def [OF Dmonoid])
   2.951 +    apply rule apply clarify
   2.952 +  proof -
   2.953 +    fix f g
   2.954 +    assume id1: "f o g = id" and id2: "g o f = id"
   2.955 +    show "bij f"
   2.956 +    proof (rule bijI)
   2.957 +      show "inj f"
   2.958 +      proof (rule inj_onI)
   2.959 +        fix x y
   2.960 +        assume "f x = f y"
   2.961 +	then have "(g o f) x = (g o f) y" by simp
   2.962 +	with id2 show "x = y" by simp
   2.963 +      qed
   2.964 +    next
   2.965 +      show "surj f"
   2.966 +      proof (rule surjI)
   2.967 +	fix x
   2.968 +        from id1 have "(f o g) x = x" by simp
   2.969 +	then show "f (g x) = x" by simp
   2.970 +      qed
   2.971 +    qed
   2.972 +  next
   2.973 +    fix f
   2.974 +    assume bij: "bij f"
   2.975 +    then
   2.976 +    have inv: "f o Hilbert_Choice.inv f = id & Hilbert_Choice.inv f o f = id"
   2.977 +      by (simp add: bij_def surj_iff inj_iff)
   2.978 +    show "EX g. f o g = id & g o f = id" by rule (rule inv)
   2.979 +  qed
   2.980  qed
   2.981  
   2.982 -thm Dclass.inv_inv
   2.983 -lemma "- (- x) = (x::'a::ring)"
   2.984 -  apply (rule Dclass.inv_inv) done
   2.985 +thm Dmonoid.unit_def Dfun.unit_def
   2.986 +
   2.987 +thm Dmonoid.inv_inj_on_unit Dfun.inv_inj_on_unit
   2.988 +
   2.989 +lemma unit_id:
   2.990 +  "(f :: unit => unit) = id"
   2.991 +  by rule simp
   2.992 +
   2.993 +interpretation Dfun: Dgrp ["op o" "id :: unit => unit"]
   2.994 +  where "Dmonoid.inv (op o) id f = inv (f :: unit => unit)"
   2.995 +proof -
   2.996 +  have "Dmonoid op o (id :: 'a => 'a)" by unfold_locales (simp_all add: o_assoc)
   2.997 +  note Dmonoid = this
   2.998 +
   2.999 +  show "Dgrp (op o) (id :: unit => unit)"
  2.1000 +apply unfold_locales
  2.1001 +apply (unfold Dmonoid.unit_def [OF Dmonoid])
  2.1002 +apply (insert unit_id)
  2.1003 +apply simp
  2.1004 +done
  2.1005 +  show "Dmonoid.inv (op o) id f = inv (f :: unit => unit)"
  2.1006 +apply (unfold Dmonoid.inv_def [OF Dmonoid] inv_def)
  2.1007 +apply (insert unit_id)
  2.1008 +apply simp
  2.1009 +apply (rule the_equality)
  2.1010 +apply rule
  2.1011 +apply rule
  2.1012 +apply simp
  2.1013 +done
  2.1014 +qed
  2.1015 +
  2.1016 +thm Dfun.unit_l_inv Dfun.l_inv
  2.1017 +
  2.1018 +thm Dfun.inv_equality
  2.1019 +thm Dfun.inv_equality
  2.1020  
  2.1021  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)