# HG changeset patch
# User haftmann
# Date 1245673522 -7200
# Node ID 530596c997da92bb322b204b37ba8e369ae458b8
# Parent  8361d7a517b444834fef7e174836c9c9d0daae4e
adapted to number theory switch

diff -r 8361d7a517b4 -r 530596c997da doc-src/Locales/Locales/Examples3.thy
--- a/doc-src/Locales/Locales/Examples3.thy	Mon Jun 22 08:17:52 2009 +0200
+++ b/doc-src/Locales/Locales/Examples3.thy	Mon Jun 22 14:25:22 2009 +0200
@@ -143,8 +143,8 @@
 
 interpretation nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
   where "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
-    and nat_dvd_meet_eq: "lattice.meet op dvd = gcd"
-    and nat_dvd_join_eq: "lattice.join op dvd = lcm"
+    and nat_dvd_meet_eq: "lattice.meet (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = gcd"
+    and nat_dvd_join_eq: "lattice.join (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = lcm"
 proof -
   show "lattice (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)"
     apply unfold_locales
@@ -152,23 +152,24 @@
     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_least)
+    apply (auto intro: nat_lcm_least)
     done
   then interpret nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" .
   show "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
     by (rule nat_dvd_less_eq)
-  show "lattice.meet op dvd = gcd"
+  show "lattice.meet (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = gcd"
     apply (auto simp add: expand_fun_eq)
     apply (unfold nat_dvd.meet_def)
     apply (rule the_equality)
     apply (unfold nat_dvd.is_inf_def)
     by auto
-  show "lattice.join op dvd = lcm"
+  show "lattice.join (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = lcm"
     apply (auto simp add: expand_fun_eq)
     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_least)
+    apply (auto intro: nat_lcm_least iff: nat_lcm_unique)
+    done
 qed
 
 text {* Equations @{thm [source] nat_dvd_meet_eq} and @{thm [source]
@@ -198,8 +199,8 @@
 interpretation %visible nat_dvd:
   distrib_lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
   where "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
-    and "lattice.meet op dvd = gcd"
-    and "lattice.join op dvd = lcm"
+    and "lattice.meet (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = gcd"
+    and "lattice.join (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = lcm"
 proof -
   show "distrib_lattice (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)"
     apply unfold_locales
diff -r 8361d7a517b4 -r 530596c997da doc-src/Locales/Locales/document/Examples3.tex
--- a/doc-src/Locales/Locales/document/Examples3.tex	Mon Jun 22 08:17:52 2009 +0200
+++ b/doc-src/Locales/Locales/document/Examples3.tex	Mon Jun 22 14:25:22 2009 +0200
@@ -307,8 +307,8 @@
 \isacommand{interpretation}\isamarkupfalse%
 \ nat{\isacharunderscore}dvd{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
 \ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{and}\ nat{\isacharunderscore}dvd{\isacharunderscore}meet{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ dvd\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{and}\ nat{\isacharunderscore}dvd{\isacharunderscore}join{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ dvd\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ nat{\isacharunderscore}dvd{\isacharunderscore}meet{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ nat{\isacharunderscore}dvd{\isacharunderscore}join{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}lattice{\isachardot}join\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline
 %
 \isadelimproof
 %
@@ -330,7 +330,7 @@
 \ \ \ \ \isacommand{apply}\isamarkupfalse%
 \ {\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequoteopen}lcm\ x\ y{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
 \ \ \ \ \isacommand{apply}\isamarkupfalse%
-\ {\isacharparenleft}auto\ intro{\isacharcolon}\ lcm{\isacharunderscore}dvd{\isadigit{1}}\ lcm{\isacharunderscore}dvd{\isadigit{2}}\ lcm{\isacharunderscore}least{\isacharparenright}\isanewline
+\ {\isacharparenleft}auto\ intro{\isacharcolon}\ nat{\isacharunderscore}lcm{\isacharunderscore}least{\isacharparenright}\isanewline
 \ \ \ \ \isacommand{done}\isamarkupfalse%
 \isanewline
 \ \ \isacommand{then}\isamarkupfalse%
@@ -342,7 +342,7 @@
 \ \ \ \ \isacommand{by}\isamarkupfalse%
 \ {\isacharparenleft}rule\ nat{\isacharunderscore}dvd{\isacharunderscore}less{\isacharunderscore}eq{\isacharparenright}\isanewline
 \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ dvd\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}lattice{\isachardot}meet\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isacommand{apply}\isamarkupfalse%
 \ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ expand{\isacharunderscore}fun{\isacharunderscore}eq{\isacharparenright}\isanewline
 \ \ \ \ \isacommand{apply}\isamarkupfalse%
@@ -354,7 +354,7 @@
 \ \ \ \ \isacommand{by}\isamarkupfalse%
 \ auto\isanewline
 \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ dvd\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}lattice{\isachardot}join\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isacommand{apply}\isamarkupfalse%
 \ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ expand{\isacharunderscore}fun{\isacharunderscore}eq{\isacharparenright}\isanewline
 \ \ \ \ \isacommand{apply}\isamarkupfalse%
@@ -363,8 +363,10 @@
 \ {\isacharparenleft}rule\ the{\isacharunderscore}equality{\isacharparenright}\isanewline
 \ \ \ \ \isacommand{apply}\isamarkupfalse%
 \ {\isacharparenleft}unfold\ nat{\isacharunderscore}dvd{\isachardot}is{\isacharunderscore}sup{\isacharunderscore}def{\isacharparenright}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}auto\ intro{\isacharcolon}\ lcm{\isacharunderscore}dvd{\isadigit{1}}\ lcm{\isacharunderscore}dvd{\isadigit{2}}\ lcm{\isacharunderscore}least{\isacharparenright}\isanewline
+\ \ \ \ \isacommand{apply}\isamarkupfalse%
+\ {\isacharparenleft}auto\ intro{\isacharcolon}\ nat{\isacharunderscore}lcm{\isacharunderscore}least\ iff{\isacharcolon}\ nat{\isacharunderscore}lcm{\isacharunderscore}unique{\isacharparenright}\isanewline
+\ \ \ \ \isacommand{done}\isamarkupfalse%
+\isanewline
 \isacommand{qed}\isamarkupfalse%
 %
 \endisatagproof
@@ -407,8 +409,8 @@
 \ nat{\isacharunderscore}dvd{\isacharcolon}\isanewline
 \ \ distrib{\isacharunderscore}lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
 \ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ dvd\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ dvd\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}join\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline
 \isacommand{proof}\isamarkupfalse%
 \ {\isacharminus}\isanewline
 \ \ \isacommand{show}\isamarkupfalse%