diff -r a4abccde0929 -r af871d13e320 src/HOL/ex/LocaleTest2.thy
--- a/src/HOL/ex/LocaleTest2.thy	Mon Jul 23 13:47:48 2007 +0200
+++ b/src/HOL/ex/LocaleTest2.thy	Mon Jul 23 13:48:30 2007 +0200
@@ -5,26 +5,635 @@
 
 More regression tests for locales.
 Definitions are less natural in FOL, since there is no selection operator.
-Hence we do them in HOL, not in the main test suite for locales:
-FOL/ex/LocaleTest.thy
+Hence we do them here in HOL, not in the main test suite for locales,
+which is FOL/ex/LocaleTest.thy
 *)
 
 header {* Test of Locale Interpretation *}
 
 theory LocaleTest2
-imports Main
+imports GCD
 begin
 
-ML {* set quick_and_dirty *}    (* allow for thm command in batch mode *)
-ML {* set show_hyps *}
-ML {* set show_sorts *}
-
-
-subsection {* Interpretation of Defined Concepts *}
+section {* Interpretation of Defined Concepts *}
 
 text {* Naming convention for global objects: prefixes D and d *}
 
-(* Group example with defined operation inv *)
+
+subsection {* Lattices *}
+
+text {* Much of the lattice proofs are from HOL/Lattice. *}
+
+
+subsubsection {* Definitions *}
+
+locale dpo =
+  fixes le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>" 50)
+  assumes refl [intro, simp]: "x \<sqsubseteq> x"
+    and anti_sym [intro]: "[| x \<sqsubseteq> y; y \<sqsubseteq> x |] ==> x = y"
+    and trans [trans]: "[| x \<sqsubseteq> y; y \<sqsubseteq> z |] ==> x \<sqsubseteq> z"
+
+begin
+
+theorem circular:
+  "[| x \<sqsubseteq> y; y \<sqsubseteq> z; z \<sqsubseteq> x |] ==> x = y & y = z"
+  by (blast intro: trans)
+
+definition
+  less :: "['a, 'a] => bool" (infixl "\<sqsubset>" 50)
+  where "(x \<sqsubset> y) = (x \<sqsubseteq> y & x ~= y)"
+
+theorem abs_test:
+  "op \<sqsubset> = (%x y. x \<sqsubset> y)"
+  by simp
+
+definition
+  is_inf :: "['a, 'a, 'a] => bool"
+  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))"
+
+definition
+  is_sup :: "['a, 'a, 'a] => bool"
+  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))"
+
+end
+
+locale dlat = dpo +
+  assumes ex_inf: "EX inf. dpo.is_inf le x y inf"
+    and ex_sup: "EX sup. dpo.is_sup le x y sup"
+
+begin
+
+definition
+  meet :: "['a, 'a] => 'a" (infixl "\<sqinter>" 70)
+  where "x \<sqinter> y = (THE inf. is_inf x y inf)"
+
+definition
+  join :: "['a, 'a] => 'a" (infixl "\<squnion>" 65)
+  where "x \<squnion> y = (THE sup. is_sup x y sup)"
+
+lemma is_infI [intro?]: "i \<sqsubseteq> x \<Longrightarrow> i \<sqsubseteq> y \<Longrightarrow>
+    (\<And>z. z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> i) \<Longrightarrow> is_inf x y i"
+  by (unfold is_inf_def) blast
+
+lemma is_inf_lower [elim?]:
+  "is_inf x y i \<Longrightarrow> (i \<sqsubseteq> x \<Longrightarrow> i \<sqsubseteq> y \<Longrightarrow> C) \<Longrightarrow> C"
+  by (unfold is_inf_def) blast
+
+lemma is_inf_greatest [elim?]:
+    "is_inf x y i \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> i"
+  by (unfold is_inf_def) blast
+
+theorem is_inf_uniq: "is_inf x y i \<Longrightarrow> is_inf x y i' \<Longrightarrow> i = i'"
+proof -
+  assume inf: "is_inf x y i"
+  assume inf': "is_inf x y i'"
+  show ?thesis
+  proof (rule anti_sym)
+    from inf' show "i \<sqsubseteq> i'"
+    proof (rule is_inf_greatest)
+      from inf show "i \<sqsubseteq> x" ..
+      from inf show "i \<sqsubseteq> y" ..
+    qed
+    from inf show "i' \<sqsubseteq> i"
+    proof (rule is_inf_greatest)
+      from inf' show "i' \<sqsubseteq> x" ..
+      from inf' show "i' \<sqsubseteq> y" ..
+    qed
+  qed
+qed
+
+theorem is_inf_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> is_inf x y x"
+proof -
+  assume "x \<sqsubseteq> y"
+  show ?thesis
+  proof
+    show "x \<sqsubseteq> x" ..
+    show "x \<sqsubseteq> y" by fact
+    fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" show "z \<sqsubseteq> x" by fact
+  qed
+qed
+
+lemma meet_equality [elim?]: "is_inf x y i \<Longrightarrow> x \<sqinter> y = i"
+proof (unfold meet_def)
+  assume "is_inf x y i"
+  then show "(THE i. is_inf x y i) = i"
+    by (rule the_equality) (rule is_inf_uniq [OF _ `is_inf x y i`])
+qed
+
+lemma meetI [intro?]:
+    "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"
+  by (rule meet_equality, rule is_infI) blast+
+
+lemma is_inf_meet [intro?]: "is_inf x y (x \<sqinter> y)"
+proof (unfold meet_def)
+  from ex_inf obtain i where "is_inf x y i" ..
+  then show "is_inf x y (THE i. is_inf x y i)"
+    by (rule theI) (rule is_inf_uniq [OF _ `is_inf x y i`])
+qed
+
+lemma meet_left [intro?]:
+  "x \<sqinter> y \<sqsubseteq> x"
+  by (rule is_inf_lower) (rule is_inf_meet)
+
+lemma meet_right [intro?]:
+  "x \<sqinter> y \<sqsubseteq> y"
+  by (rule is_inf_lower) (rule is_inf_meet)
+
+lemma meet_le [intro?]:
+  "[| z \<sqsubseteq> x; z \<sqsubseteq> y |] ==> z \<sqsubseteq> x \<sqinter> y"
+  by (rule is_inf_greatest) (rule is_inf_meet)
+
+lemma is_supI [intro?]: "x \<sqsubseteq> s \<Longrightarrow> y \<sqsubseteq> s \<Longrightarrow>
+    (\<And>z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> s \<sqsubseteq> z) \<Longrightarrow> is_sup x y s"
+  by (unfold is_sup_def) blast
+
+lemma is_sup_least [elim?]:
+    "is_sup x y s \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> s \<sqsubseteq> z"
+  by (unfold is_sup_def) blast
+
+lemma is_sup_upper [elim?]:
+    "is_sup x y s \<Longrightarrow> (x \<sqsubseteq> s \<Longrightarrow> y \<sqsubseteq> s \<Longrightarrow> C) \<Longrightarrow> C"
+  by (unfold is_sup_def) blast
+
+theorem is_sup_uniq: "is_sup x y s \<Longrightarrow> is_sup x y s' \<Longrightarrow> s = s'"
+proof -
+  assume sup: "is_sup x y s"
+  assume sup': "is_sup x y s'"
+  show ?thesis
+  proof (rule anti_sym)
+    from sup show "s \<sqsubseteq> s'"
+    proof (rule is_sup_least)
+      from sup' show "x \<sqsubseteq> s'" ..
+      from sup' show "y \<sqsubseteq> s'" ..
+    qed
+    from sup' show "s' \<sqsubseteq> s"
+    proof (rule is_sup_least)
+      from sup show "x \<sqsubseteq> s" ..
+      from sup show "y \<sqsubseteq> s" ..
+    qed
+  qed
+qed
+
+theorem is_sup_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> is_sup x y y"
+proof -
+  assume "x \<sqsubseteq> y"
+  show ?thesis
+  proof
+    show "x \<sqsubseteq> y" by fact
+    show "y \<sqsubseteq> y" ..
+    fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z"
+    show "y \<sqsubseteq> z" by fact
+  qed
+qed
+
+lemma join_equality [elim?]: "is_sup x y s \<Longrightarrow> x \<squnion> y = s"
+proof (unfold join_def)
+  assume "is_sup x y s"
+  then show "(THE s. is_sup x y s) = s"
+    by (rule the_equality) (rule is_sup_uniq [OF _ `is_sup x y s`])
+qed
+
+lemma joinI [intro?]: "x \<sqsubseteq> s \<Longrightarrow> y \<sqsubseteq> s \<Longrightarrow>
+    (\<And>z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> s \<sqsubseteq> z) \<Longrightarrow> x \<squnion> y = s"
+  by (rule join_equality, rule is_supI) blast+
+
+lemma is_sup_join [intro?]: "is_sup x y (x \<squnion> y)"
+proof (unfold join_def)
+  from ex_sup obtain s where "is_sup x y s" ..
+  then show "is_sup x y (THE s. is_sup x y s)"
+    by (rule theI) (rule is_sup_uniq [OF _ `is_sup x y s`])
+qed
+
+lemma join_left [intro?]:
+  "x \<sqsubseteq> x \<squnion> y"
+  by (rule is_sup_upper) (rule is_sup_join)
+
+lemma join_right [intro?]:
+  "y \<sqsubseteq> x \<squnion> y"
+  by (rule is_sup_upper) (rule is_sup_join)
+
+lemma join_le [intro?]:
+  "[| x \<sqsubseteq> z; y \<sqsubseteq> z |] ==> x \<squnion> y \<sqsubseteq> z"
+  by (rule is_sup_least) (rule is_sup_join)
+
+theorem meet_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
+proof (rule meetI)
+  show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x \<sqinter> y"
+  proof
+    show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x" ..
+    show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y"
+    proof -
+      have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" ..
+      also have "\<dots> \<sqsubseteq> y" ..
+      finally show ?thesis .
+    qed
+  qed
+  show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> z"
+  proof -
+    have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" ..
+    also have "\<dots> \<sqsubseteq> z" ..
+    finally show ?thesis .
+  qed
+  fix w assume "w \<sqsubseteq> x \<sqinter> y" and "w \<sqsubseteq> z"
+  show "w \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
+  proof
+    show "w \<sqsubseteq> x"
+    proof -
+      have "w \<sqsubseteq> x \<sqinter> y" by fact
+      also have "\<dots> \<sqsubseteq> x" ..
+      finally show ?thesis .
+    qed
+    show "w \<sqsubseteq> y \<sqinter> z"
+    proof
+      show "w \<sqsubseteq> y"
+      proof -
+        have "w \<sqsubseteq> x \<sqinter> y" by fact
+        also have "\<dots> \<sqsubseteq> y" ..
+        finally show ?thesis .
+      qed
+      show "w \<sqsubseteq> z" by fact
+    qed
+  qed
+qed
+
+theorem meet_commute: "x \<sqinter> y = y \<sqinter> x"
+proof (rule meetI)
+  show "y \<sqinter> x \<sqsubseteq> x" ..
+  show "y \<sqinter> x \<sqsubseteq> y" ..
+  fix z assume "z \<sqsubseteq> y" and "z \<sqsubseteq> x"
+  then show "z \<sqsubseteq> y \<sqinter> x" ..
+qed
+
+theorem meet_join_absorb: "x \<sqinter> (x \<squnion> y) = x"
+proof (rule meetI)
+  show "x \<sqsubseteq> x" ..
+  show "x \<sqsubseteq> x \<squnion> y" ..
+  fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> x \<squnion> y"
+  show "z \<sqsubseteq> x" by fact
+qed
+
+theorem join_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
+proof (rule joinI)
+  show "x \<squnion> y \<sqsubseteq> x \<squnion> (y \<squnion> z)"
+  proof
+    show "x \<sqsubseteq> x \<squnion> (y \<squnion> z)" ..
+    show "y \<sqsubseteq> x \<squnion> (y \<squnion> z)"
+    proof -
+      have "y \<sqsubseteq> y \<squnion> z" ..
+      also have "... \<sqsubseteq> x \<squnion> (y \<squnion> z)" ..
+      finally show ?thesis .
+    qed
+  qed
+  show "z \<sqsubseteq> x \<squnion> (y \<squnion> z)"
+  proof -
+    have "z \<sqsubseteq> y \<squnion> z"  ..
+    also have "... \<sqsubseteq> x \<squnion> (y \<squnion> z)" ..
+    finally show ?thesis .
+  qed
+  fix w assume "x \<squnion> y \<sqsubseteq> w" and "z \<sqsubseteq> w"
+  show "x \<squnion> (y \<squnion> z) \<sqsubseteq> w"
+  proof
+    show "x \<sqsubseteq> w"
+    proof -
+      have "x \<sqsubseteq> x \<squnion> y" ..
+      also have "\<dots> \<sqsubseteq> w" by fact
+      finally show ?thesis .
+    qed
+    show "y \<squnion> z \<sqsubseteq> w"
+    proof
+      show "y \<sqsubseteq> w"
+      proof -
+	have "y \<sqsubseteq> x \<squnion> y" ..
+	also have "... \<sqsubseteq> w" by fact
+        finally show ?thesis .
+      qed
+      show "z \<sqsubseteq> w" by fact
+    qed
+  qed
+qed
+
+theorem join_commute: "x \<squnion> y = y \<squnion> x"
+proof (rule joinI)
+  show "x \<sqsubseteq> y \<squnion> x" ..
+  show "y \<sqsubseteq> y \<squnion> x" ..
+  fix z assume "y \<sqsubseteq> z" and "x \<sqsubseteq> z"
+  then show "y \<squnion> x \<sqsubseteq> z" ..
+qed
+
+theorem join_meet_absorb: "x \<squnion> (x \<sqinter> y) = x"
+proof (rule joinI)
+  show "x \<sqsubseteq> x" ..
+  show "x \<sqinter> y \<sqsubseteq> x" ..
+  fix z assume "x \<sqsubseteq> z" and "x \<sqinter> y \<sqsubseteq> z"
+  show "x \<sqsubseteq> z" by fact
+qed
+
+theorem meet_idem: "x \<sqinter> x = x"
+proof -
+  have "x \<sqinter> (x \<squnion> (x \<sqinter> x)) = x" by (rule meet_join_absorb)
+  also have "x \<squnion> (x \<sqinter> x) = x" by (rule join_meet_absorb)
+  finally show ?thesis .
+qed
+
+theorem meet_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
+proof (rule meetI)
+  assume "x \<sqsubseteq> y"
+  show "x \<sqsubseteq> x" ..
+  show "x \<sqsubseteq> y" by fact
+  fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y"
+  show "z \<sqsubseteq> x" by fact
+qed
+
+theorem meet_related2 [elim?]: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
+  by (drule meet_related) (simp add: meet_commute)
+
+theorem join_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
+proof (rule joinI)
+  assume "x \<sqsubseteq> y"
+  show "y \<sqsubseteq> y" ..
+  show "x \<sqsubseteq> y" by fact
+  fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z"
+  show "y \<sqsubseteq> z" by fact
+qed
+
+theorem join_related2 [elim?]: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
+  by (drule join_related) (simp add: join_commute)
+
+
+text {* Additional theorems *}
+
+theorem meet_connection: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)"
+proof
+  assume "x \<sqsubseteq> y"
+  then have "is_inf x y x" ..
+  then show "x \<sqinter> y = x" ..
+next
+  have "x \<sqinter> y \<sqsubseteq> y" ..
+  also assume "x \<sqinter> y = x"
+  finally show "x \<sqsubseteq> y" .
+qed
+
+theorem meet_connection2: "(x \<sqsubseteq> y) = (y \<sqinter> x = x)"
+  using meet_commute meet_connection by simp
+
+theorem join_connection: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"
+proof
+  assume "x \<sqsubseteq> y"
+  then have "is_sup x y y" ..
+  then show "x \<squnion> y = y" ..
+next
+  have "x \<sqsubseteq> x \<squnion> y" ..
+  also assume "x \<squnion> y = y"
+  finally show "x \<sqsubseteq> y" .
+qed
+
+theorem join_connection2: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"
+  using join_commute join_connection by simp
+
+
+text {* Naming according to Jacobson I, p.\ 459. *}
+
+lemmas L1 = join_commute meet_commute
+lemmas L2 = join_assoc meet_assoc
+(*lemmas L3 = join_idem meet_idem*)
+lemmas L4 = join_meet_absorb meet_join_absorb
+
+end
+
+locale ddlat = dlat +
+  assumes meet_distr:
+    "dlat.meet le x (dlat.join le y z) =
+    dlat.join le (dlat.meet le x y) (dlat.meet le x z)"
+
+begin
+
+lemma join_distr:
+  "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
+  txt {* Jacobson I, p.\ 462 *}
+proof -
+  have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by (simp add: L4)
+  also have "... = x \<squnion> ((x \<sqinter> z) \<squnion> (y \<sqinter> z))" by (simp add: L2)
+  also have "... = x \<squnion> ((x \<squnion> y) \<sqinter> z)" by (simp add: L1 meet_distr)
+  also have "... = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)" by (simp add: L1 L4)
+  also have "... = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by (simp add: meet_distr)
+  finally show ?thesis .
+qed
+
+end
+
+locale dlo = dpo +
+  assumes total: "x \<sqsubseteq> y | y \<sqsubseteq> x"
+
+begin
+
+lemma less_total: "x \<sqsubset> y | x = y | y \<sqsubset> x"
+  using total
+  by (unfold less_def) blast
+
+end
+
+
+interpretation dlo < dlat
+(* TODO: definition syntax is unavailable *)
+proof unfold_locales
+  fix x y
+  from total have "is_inf x y (if x \<sqsubseteq> y then x else y)" by (auto simp: is_inf_def)
+  then show "EX inf. is_inf x y inf" by blast
+next
+  fix x y
+  from total have "is_sup x y (if x \<sqsubseteq> y then y else x)" by (auto simp: is_sup_def)
+  then show "EX sup. is_sup x y sup" by blast
+qed
+
+interpretation dlo < ddlat
+proof unfold_locales
+  fix x y z
+  show "x \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> z" (is "?l = ?r")
+    txt {* Jacobson I, p.\ 462 *}
+  proof -
+    { assume c: "y \<sqsubseteq> x" "z \<sqsubseteq> x"
+      from c have "?l = y \<squnion> z"
+	by (metis c (*join_commute*) join_connection2 join_related2 (*meet_commute*) meet_connection meet_related2 total)
+      also from c have "... = ?r" by (metis (*c*) (*join_commute*) meet_related2)
+      finally have "?l = ?r" . }
+    moreover
+    { assume c: "x \<sqsubseteq> y | x \<sqsubseteq> z"
+      from c have "?l = x"
+	by (metis (*anti_sym*) (*c*) (*circular*) (*join_assoc*)(* join_commute *) join_connection2 (*join_left*) join_related2 meet_connection(* meet_related2*) total trans)
+      also from c have "... = ?r"
+	by (metis join_commute join_related2 meet_connection meet_related2 total)
+      finally have "?l = ?r" . }
+    moreover note total
+    ultimately show ?thesis by blast
+  qed
+qed
+
+subsubsection {* Total order @{text "<="} on @{typ int} *}
+
+interpretation int: dpo ["op <= :: [int, int] => bool"]
+  where "(dpo.less (op <=) (x::int) y) = (x < y)"
+  txt {* We give interpretation for less, but not is\_inf and is\_sub. *}
+proof -
+  show "dpo (op <= :: [int, int] => bool)"
+    by unfold_locales auto
+  then interpret int: dpo ["op <= :: [int, int] => bool"] .
+    txt {* Gives interpreted version of less\_def (without condition). *}
+  show "(dpo.less (op <=) (x::int) y) = (x < y)"
+    by (unfold int.less_def) auto
+qed
+
+thm int.circular
+lemma "\<lbrakk> (x::int) \<le> y; y \<le> z; z \<le> x\<rbrakk> \<Longrightarrow> x = y \<and> y = z"
+  apply (rule int.circular) apply assumption apply assumption apply assumption done
+thm int.abs_test
+lemma "(op < :: [int, int] => bool) = op <"
+  apply (rule int.abs_test) done
+
+interpretation int: dlat ["op <= :: [int, int] => bool"]
+  where "dlat.meet (op <=) (x::int) y = min x y"
+    and "dlat.join (op <=) (x::int) y = max x y"
+proof -
+  show "dlat (op <= :: [int, int] => bool)"
+    apply unfold_locales
+    apply (unfold int.is_inf_def int.is_sup_def)
+    apply arith+
+    done
+  then interpret int: dlat ["op <= :: [int, int] => bool"] .
+  txt {* Interpretation to ease use of definitions, which are
+    conditional in general but unconditional after interpretation. *}
+  show "dlat.meet (op <=) (x::int) y = min x y"
+    apply (unfold int.meet_def)
+    apply (rule the_equality)
+    apply (unfold int.is_inf_def)
+    by auto
+  show "dlat.join (op <=) (x::int) y = max x y"
+    apply (unfold int.join_def)
+    apply (rule the_equality)
+    apply (unfold int.is_sup_def)
+    by auto
+qed
+
+interpretation int: dlo ["op <= :: [int, int] => bool"]
+  by unfold_locales arith
+
+text {* Interpreted theorems from the locales, involving defined terms. *}
+
+thm int.less_def text {* from dpo *}
+thm int.meet_left text {* from dlat *}
+thm int.meet_distr text {* from ddlat *}
+thm int.less_total text {* from dlo *}
+
+
+subsubsection {* Total order @{text "<="} on @{typ nat} *}
+
+interpretation nat: dpo ["op <= :: [nat, nat] => bool"]
+  where "dpo.less (op <=) (x::nat) y = (x < y)"
+  txt {* We give interpretation for less, but not is\_inf and is\_sub. *}
+proof -
+  show "dpo (op <= :: [nat, nat] => bool)"
+    by unfold_locales auto
+  then interpret nat: dpo ["op <= :: [nat, nat] => bool"] .
+    txt {* Gives interpreted version of less\_def (without condition). *}
+  show "dpo.less (op <=) (x::nat) y = (x < y)"
+    apply (unfold nat.less_def)
+    apply auto
+    done
+qed
+
+interpretation nat: dlat ["op <= :: [nat, nat] => bool"]
+  where "dlat.meet (op <=) (x::nat) y = min x y"
+    and "dlat.join (op <=) (x::nat) y = max x y"
+proof -
+  show "dlat (op <= :: [nat, nat] => bool)"
+    apply unfold_locales
+    apply (unfold nat.is_inf_def nat.is_sup_def)
+    apply arith+
+    done
+  then interpret nat: dlat ["op <= :: [nat, nat] => bool"] .
+  txt {* Interpretation to ease use of definitions, which are
+    conditional in general but unconditional after interpretation. *}
+  show "dlat.meet (op <=) (x::nat) y = min x y"
+    apply (unfold nat.meet_def)
+    apply (rule the_equality)
+    apply (unfold nat.is_inf_def)
+    by auto
+  show "dlat.join (op <=) (x::nat) y = max x y"
+    apply (unfold nat.join_def)
+    apply (rule the_equality)
+    apply (unfold nat.is_sup_def)
+    by auto
+qed
+
+interpretation nat: dlo ["op <= :: [nat, nat] => bool"]
+  by unfold_locales arith
+
+text {* Interpreted theorems from the locales, involving defined terms. *}
+
+thm nat.less_def text {* from dpo *}
+thm nat.meet_left text {* from dlat *}
+thm nat.meet_distr text {* from ddlat *}
+thm nat.less_total text {* from ldo *}
+
+
+subsubsection {* Lattice @{text "dvd"} on @{typ nat} *}
+
+interpretation nat_dvd: dpo ["op dvd :: [nat, nat] => bool"]
+  where "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)"
+  txt {* We give interpretation for less, but not is\_inf and is\_sub. *}
+proof -
+  show "dpo (op dvd :: [nat, nat] => bool)"
+    by unfold_locales (auto simp: dvd_def)
+  then interpret nat_dvd: dpo ["op dvd :: [nat, nat] => bool"] .
+    txt {* Gives interpreted version of less\_def (without condition). *}
+  show "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)"
+    apply (unfold nat_dvd.less_def)
+    apply auto
+    done
+qed
+
+interpretation nat_dvd: dlat ["op dvd :: [nat, nat] => bool"]
+  where "dlat.meet (op dvd) (x::nat) y = gcd (x, y)"
+    and "dlat.join (op dvd) (x::nat) y = lcm (x, y)"
+proof -
+  show "dlat (op dvd :: [nat, nat] => bool)"
+    apply unfold_locales
+    apply (unfold nat_dvd.is_inf_def nat_dvd.is_sup_def)
+    apply (rule_tac x = "gcd (x, y)" in exI)
+    apply auto [1]
+    apply (rule_tac x = "lcm (x, y)" in exI)
+    apply (auto intro: lcm_dvd1 lcm_dvd2 lcm_lowest)
+    done
+  then interpret nat_dvd: dlat ["op dvd :: [nat, nat] => bool"] .
+  txt {* Interpretation to ease use of definitions, which are
+    conditional in general but unconditional after interpretation. *}
+  show "dlat.meet (op dvd) (x::nat) y = gcd (x, y)"
+    apply (unfold nat_dvd.meet_def)
+    apply (rule the_equality)
+    apply (unfold nat_dvd.is_inf_def)
+    by auto
+  show "dlat.join (op dvd) (x::nat) y = lcm (x, y)"
+    apply (unfold nat_dvd.join_def)
+    apply (rule the_equality)
+    apply (unfold nat_dvd.is_sup_def)
+    by (auto intro: lcm_dvd1 lcm_dvd2 lcm_lowest)
+qed
+
+text {* Interpreted theorems from the locales, involving defined terms. *}
+
+thm nat_dvd.less_def text {* from dpo *}
+lemma "((x::nat) dvd y & x ~= y) = (x dvd y & x ~= y)"
+  apply (rule nat_dvd.less_def) done
+thm nat_dvd.meet_left text {* from dlat *}
+lemma "gcd (x, y) dvd x"
+  apply (rule nat_dvd.meet_left) done
+
+print_interps dpo
+print_interps dlat
+
+
+subsection {* Group example with defined operations @{text inv} and @{text unit} *}
+
+subsubsection {* Locale declarations and lemmas *}
 
 locale Dsemi =
   fixes prod (infixl "**" 65)
@@ -32,128 +641,279 @@
 
 locale Dmonoid = Dsemi +
   fixes one
-  assumes lone: "one ** x = x"
-    and rone: "x ** one = x"
+  assumes l_one [simp]: "one ** x = x"
+    and r_one [simp]: "x ** one = x"
+
+begin
 
-definition (in Dmonoid)
-  inv where "inv(x) == THE y. x ** y = one & y ** x = one"
+definition
+  inv where "inv x = (THE y. x ** y = one & y ** x = one)"
+definition
+  unit where "unit x = (EX y. x ** y = one  & y ** x = one)"
 
-lemma (in Dmonoid) inv_unique:
+lemma inv_unique:
   assumes eq: "y ** x = one" "x ** y' = one"
   shows "y = y'"
 proof -
-  from eq have "y = y ** (x ** y')" by (simp add: rone)
+  from eq have "y = y ** (x ** y')" by (simp add: r_one)
   also have "... = (y ** x) ** y'" by (simp add: assoc)
-  also from eq have "... = y'" by (simp add: lone)
+  also from eq have "... = y'" by (simp add: l_one)
   finally show ?thesis .
 qed
 
-locale Dgrp = Dmonoid +
-  assumes linv_ex: "EX y. y ** x = one"
-    and rinv_ex: "EX y. x ** y = one"
+lemma unit_one [intro, simp]:
+  "unit one"
+  by (unfold unit_def) auto
+
+lemma unit_l_inv_ex:
+  "unit x ==> \<exists>y. y ** x = one"
+  by (unfold unit_def) auto
+
+lemma unit_r_inv_ex:
+  "unit x ==> \<exists>y. x ** y = one"
+  by (unfold unit_def) auto
+
+lemma unit_l_inv:
+  "unit x ==> inv x ** x = one"
+  apply (simp add: unit_def inv_def) apply (erule exE)
+  apply (rule theI2, fast)
+  apply (rule inv_unique)
+  apply fast+
+  done
 
-lemma (in Dgrp) linv:
-  "inv x ** x = one"
-apply (unfold inv_def)
-apply (insert rinv_ex [where x = x])
-apply (insert linv_ex [where x = x])
-apply (erule exE) apply (erule exE)
-apply (rule theI2)
-apply rule apply assumption
-apply (frule inv_unique, assumption)
-apply simp
-apply (rule inv_unique)
-apply fast+
-done
+lemma unit_r_inv:
+  "unit x ==> x ** inv x = one"
+  apply (simp add: unit_def inv_def) apply (erule exE)
+  apply (rule theI2, fast)
+  apply (rule inv_unique)
+  apply fast+
+  done
+
+lemma unit_inv_unit [intro, simp]:
+  "unit x ==> unit (inv x)"
+proof -
+  assume x: "unit x"
+  show "unit (inv x)"
+    by (auto simp add: unit_def
+      intro: unit_l_inv unit_r_inv x)
+qed
+
+lemma unit_l_cancel [simp]:
+  "unit x ==> (x ** y = x ** z) = (y = z)"
+proof
+  assume eq: "x ** y = x ** z"
+    and G: "unit x"
+  then have "(inv x ** x) ** y = (inv x ** x) ** z"
+    by (simp add: assoc)
+  with G show "y = z" by (simp add: unit_l_inv)
+next
+  assume eq: "y = z"
+    and G: "unit x"
+  then show "x ** y = x ** z" by simp
+qed
 
-lemma (in Dgrp) rinv:
+lemma unit_inv_inv [simp]:
+  "unit x ==> inv (inv x) = x"
+proof -
+  assume x: "unit x"
+  then have "inv x ** inv (inv x) = inv x ** x"
+    by (simp add: unit_l_inv unit_r_inv)
+  with x show ?thesis by simp
+qed
+
+lemma inv_inj_on_unit:
+  "inj_on inv {x. unit x}"
+proof (rule inj_onI, simp)
+  fix x y
+  assume G: "unit x"  "unit y" and eq: "inv x = inv y"
+  then have "inv (inv x) = inv (inv y)" by simp
+  with G show "x = y" by simp
+qed
+
+lemma unit_inv_comm:
+  assumes inv: "x ** y = one"
+    and G: "unit x"  "unit y"
+  shows "y ** x = one"
+proof -
+  from G have "x ** y ** x = x ** one" by (auto simp add: inv)
+  with G show ?thesis by (simp del: r_one add: assoc)
+qed
+
+end
+
+
+locale Dgrp = Dmonoid +
+  assumes unit [intro, simp]: "Dmonoid.unit (op **) one x"
+
+begin
+
+lemma l_inv_ex [simp]:
+  "\<exists>y. y ** x = one"
+  using unit_l_inv_ex by simp
+
+lemma r_inv_ex [simp]:
+  "\<exists>y. x ** y = one"
+  using unit_r_inv_ex by simp
+
+lemma l_inv [simp]:
+  "inv x ** x = one"
+  using unit_l_inv by simp
+
+lemma l_cancel [simp]:
+  "(x ** y = x ** z) = (y = z)"
+  using unit_l_inv by simp
+
+lemma r_inv [simp]:
   "x ** inv x = one"
-apply (unfold inv_def)
-apply (insert rinv_ex [where x = x])
-apply (insert linv_ex [where x = x])
-apply (erule exE) apply (erule exE)
-apply (rule theI2)
-apply rule apply assumption
-apply (frule inv_unique, assumption)
-apply simp
-apply (rule inv_unique)
-apply fast+
-done
+proof -
+  have "inv x ** (x ** inv x) = inv x ** one"
+    by (simp add: assoc [symmetric] l_inv)
+  then show ?thesis by (simp del: r_one)
+qed
 
-lemma (in Dgrp) lcancel:
-  "x ** y = x ** z <-> y = z"
+lemma r_cancel [simp]:
+  "(y ** x = z ** x) = (y = z)"
 proof
-  assume "x ** y = x ** z"
-  then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
-  then show "y = z" by (simp add: lone linv)
+  assume eq: "y ** x = z ** x"
+  then have "y ** (x ** inv x) = z ** (x ** inv x)"
+    by (simp add: assoc [symmetric] del: r_inv)
+  then show "y = z" by simp
 qed simp
 
-interpretation Dint: Dmonoid ["op +" "0::int"]
-  where "Dmonoid.inv (op +) (0::int)" = "uminus"
+lemma inv_one [simp]:
+  "inv one = one"
 proof -
-  show "Dmonoid (op +) (0::int)" by unfold_locales auto
-  note Dint = this (* should have this as an assumption in further goals *)
-  {
-    fix x
-    have "Dmonoid.inv (op +) (0::int) x = - x"
-      by (auto simp: Dmonoid.inv_def [OF Dint])
-  }
-  then show "Dmonoid.inv (op +) (0::int) == uminus"
-    by (rule_tac eq_reflection) (fast intro: ext)
+  have "inv one = one ** (inv one)" by (simp del: r_inv)
+  moreover have "... = one" by simp
+  finally show ?thesis .
 qed
 
-thm Dmonoid.inv_def Dint.inv_def
+lemma inv_inv [simp]:
+  "inv (inv x) = x"
+  using unit_inv_inv by simp
 
-lemma "- x \<equiv> THE y. x + y = 0 \<and> y + x = (0::int)"
-  apply (rule Dint.inv_def) done
+lemma inv_inj:
+  "inj_on inv UNIV"
+  using inv_inj_on_unit by simp
 
-interpretation Dclass: Dmonoid ["op +" "0::'a::ab_group_add"]
-  where "Dmonoid.inv (op +) (0::'a::ab_group_add)" = "uminus"
+lemma inv_mult_group:
+  "inv (x ** y) = inv y ** inv x"
 proof -
-  show "Dmonoid (op +) (0::'a::ab_group_add)" by unfold_locales auto
-  note Dclass = this (* should have this as an assumption in further goals *)
-  {
-    fix x
-    have "Dmonoid.inv (op +) (0::'a::ab_group_add) x = - x"
-      by (auto simp: Dmonoid.inv_def [OF Dclass] equals_zero_I [symmetric])
-  }
-  then show "Dmonoid.inv (op +) (0::'a::ab_group_add) == uminus"
-    by (rule_tac eq_reflection) (fast intro: ext)
+  have "inv (x ** y) ** (x ** y) = (inv y ** inv x) ** (x ** y)"
+    by (simp add: assoc l_inv) (simp add: assoc [symmetric])
+  then show ?thesis by (simp del: l_inv)
+qed
+
+lemma inv_comm:
+  "x ** y = one ==> y ** x = one"
+  by (rule unit_inv_comm) auto
+
+lemma inv_equality:
+     "y ** x = one ==> inv x = y"
+  apply (simp add: inv_def)
+  apply (rule the_equality)
+   apply (simp add: inv_comm [of y x])
+  apply (rule r_cancel [THEN iffD1], auto)
+  done
+
+end
+
+
+locale Dhom = Dgrp prod (infixl "**" 65) one + Dgrp sum (infixl "+++" 60) zero +
+  fixes hom
+  assumes hom_mult [simp]: "hom (x ** y) = hom x +++ hom y"
+
+begin
+
+lemma hom_one [simp]:
+  "hom one = zero"
+proof -
+  have "hom one +++ zero = hom one +++ hom one"
+    by (simp add: hom_mult [symmetric] del: hom_mult)
+  then show ?thesis by (simp del: r_one)
 qed
 
-interpretation Dclass: Dgrp ["op +" "0::'a::ring"]
-apply unfold_locales
-apply (rule_tac x="-x" in exI) apply simp
-apply (rule_tac x="-x" in exI) apply simp
-done
+end
 
-(* Equation for inverse from Dclass: Dmonoid effective. *)
 
-thm Dclass.linv
-lemma "-x + x = (0::'a::ring)" apply (rule Dclass.linv) done
-
-(* Equations have effect in "subscriptions" *)
-
-(* In the same module *)
+subsubsection {* Interpretation of Functions *}
 
-lemma (in Dmonoid) trivial:
-  "inv one = inv one"
-  by rule
-
-thm Dclass.trivial
-
-(* Inherited: interpretation *)
-
-lemma (in Dgrp) inv_inv:
-  "inv (inv x) = x"
+interpretation Dfun: Dmonoid ["op o" "id :: 'a => 'a"]
+  where "Dmonoid.unit (op o) id f = bij (f::'a => 'a)"
+(*    and "Dmonoid.inv (op o) id" = "inv :: ('a => 'a) => ('a => 'a)" *)
 proof -
-  have "inv x ** inv (inv x) = inv x ** x"
-    by (simp add: linv rinv)
-  then show ?thesis by (simp add: lcancel)
+  show "Dmonoid op o (id :: 'a => 'a)" by unfold_locales (simp_all add: o_assoc)
+  note Dmonoid = this
+(*
+  from this interpret Dmonoid ["op o" "id :: 'a => 'a"] .
+*)
+  show "Dmonoid.unit (op o) (id :: 'a => 'a) f = bij f"
+    apply (unfold Dmonoid.unit_def [OF Dmonoid])
+    apply rule apply clarify
+  proof -
+    fix f g
+    assume id1: "f o g = id" and id2: "g o f = id"
+    show "bij f"
+    proof (rule bijI)
+      show "inj f"
+      proof (rule inj_onI)
+        fix x y
+        assume "f x = f y"
+	then have "(g o f) x = (g o f) y" by simp
+	with id2 show "x = y" by simp
+      qed
+    next
+      show "surj f"
+      proof (rule surjI)
+	fix x
+        from id1 have "(f o g) x = x" by simp
+	then show "f (g x) = x" by simp
+      qed
+    qed
+  next
+    fix f
+    assume bij: "bij f"
+    then
+    have inv: "f o Hilbert_Choice.inv f = id & Hilbert_Choice.inv f o f = id"
+      by (simp add: bij_def surj_iff inj_iff)
+    show "EX g. f o g = id & g o f = id" by rule (rule inv)
+  qed
 qed
 
-thm Dclass.inv_inv
-lemma "- (- x) = (x::'a::ring)"
-  apply (rule Dclass.inv_inv) done
+thm Dmonoid.unit_def Dfun.unit_def
+
+thm Dmonoid.inv_inj_on_unit Dfun.inv_inj_on_unit
+
+lemma unit_id:
+  "(f :: unit => unit) = id"
+  by rule simp
+
+interpretation Dfun: Dgrp ["op o" "id :: unit => unit"]
+  where "Dmonoid.inv (op o) id f = inv (f :: unit => unit)"
+proof -
+  have "Dmonoid op o (id :: 'a => 'a)" by unfold_locales (simp_all add: o_assoc)
+  note Dmonoid = this
+
+  show "Dgrp (op o) (id :: unit => unit)"
+apply unfold_locales
+apply (unfold Dmonoid.unit_def [OF Dmonoid])
+apply (insert unit_id)
+apply simp
+done
+  show "Dmonoid.inv (op o) id f = inv (f :: unit => unit)"
+apply (unfold Dmonoid.inv_def [OF Dmonoid] inv_def)
+apply (insert unit_id)
+apply simp
+apply (rule the_equality)
+apply rule
+apply rule
+apply simp
+done
+qed
+
+thm Dfun.unit_l_inv Dfun.l_inv
+
+thm Dfun.inv_equality
+thm Dfun.inv_equality
 
 end