--- 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
--- 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%