# HG changeset patch # User haftmann # Date 1216098650 -7200 # Node ID 3ac9e3cd1fa39962f57e09a9f2785f3508f3a6e3 # Parent 86db6468145d079ea9d28632e9ad1e3103173378 curried gcd diff -r 86db6468145d -r 3ac9e3cd1fa3 doc-src/Locales/Locales/Examples3.thy --- a/doc-src/Locales/Locales/Examples3.thy Mon Jul 14 23:28:26 2008 +0200 +++ b/doc-src/Locales/Locales/Examples3.thy Tue Jul 15 07:10:50 2008 +0200 @@ -147,25 +147,27 @@ interpretation nat_dvd: lattice ["op dvd :: nat \ nat \ bool"] where nat_dvd_meet_eq: - "lattice.meet op dvd (x::nat) y = gcd (x, y)" + "lattice.meet op dvd = gcd" and nat_dvd_join_eq: - "lattice.join op dvd (x::nat) y = lcm (x, y)" + "lattice.join op dvd = lcm" proof - show "lattice (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 (rule_tac x = "gcd x y" in exI) apply auto [1] - apply (rule_tac x = "lcm (x, y)" in exI) + apply (rule_tac x = "lcm x y" in exI) apply (auto intro: lcm_dvd1 lcm_dvd2 lcm_least) done then interpret nat_dvd: lattice ["op dvd :: nat \ nat \ bool"] . - show "lattice.meet op dvd (x::nat) y = gcd (x, y)" + show "lattice.meet op dvd = 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 (x::nat) y = lcm (x, y)" + show "lattice.join op dvd = 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) @@ -196,8 +198,7 @@ *) lemma %invisible gcd_lcm_distr: - "gcd (x, lcm (y, z)) = lcm (gcd (x, y), gcd (x, z))" - sorry + "gcd x (lcm y z) = lcm (gcd x y) (gcd x z)" sorry ML %invisible {* reset quick_and_dirty *} diff -r 86db6468145d -r 3ac9e3cd1fa3 doc-src/Locales/Locales/document/Examples3.tex --- a/doc-src/Locales/Locales/document/Examples3.tex Mon Jul 14 23:28:26 2008 +0200 +++ b/doc-src/Locales/Locales/document/Examples3.tex Tue Jul 15 07:10:50 2008 +0200 @@ -287,9 +287,9 @@ \isacommand{interpretation}\isamarkupfalse% \ nat{\isacharunderscore}dvd{\isacharcolon}\ lattice\ {\isacharbrackleft}{\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\isanewline \ \ \isakeyword{where}\ nat{\isacharunderscore}dvd{\isacharunderscore}meet{\isacharunderscore}eq{\isacharcolon}\isanewline -\ \ \ \ \ \ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ gcd\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \ \ \ \ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ dvd\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline \ \ \ \ \isakeyword{and}\ nat{\isacharunderscore}dvd{\isacharunderscore}join{\isacharunderscore}eq{\isacharcolon}\isanewline -\ \ \ \ \ \ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ lcm\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \ \ \ \ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ dvd\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline % \isadelimproof % @@ -305,11 +305,11 @@ \ \ \ \ \isacommand{apply}\isamarkupfalse% \ {\isacharparenleft}unfold\ nat{\isacharunderscore}dvd{\isachardot}is{\isacharunderscore}inf{\isacharunderscore}def\ nat{\isacharunderscore}dvd{\isachardot}is{\isacharunderscore}sup{\isacharunderscore}def{\isacharparenright}\isanewline \ \ \ \ \isacommand{apply}\isamarkupfalse% -\ {\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequoteopen}gcd\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline +\ {\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequoteopen}gcd\ x\ y{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline \ \ \ \ \isacommand{apply}\isamarkupfalse% \ auto\ {\isacharbrackleft}{\isadigit{1}}{\isacharbrackright}\isanewline \ \ \ \ \isacommand{apply}\isamarkupfalse% -\ {\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequoteopen}lcm\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline +\ {\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 \ \ \ \ \isacommand{done}\isamarkupfalse% @@ -319,7 +319,9 @@ \ nat{\isacharunderscore}dvd{\isacharcolon}\ lattice\ {\isacharbrackleft}{\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\ \isacommand{{\isachardot}}\isamarkupfalse% \isanewline \ \ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ gcd\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ dvd\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline +\ \ \ \ \isacommand{apply}\isamarkupfalse% +\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ expand{\isacharunderscore}fun{\isacharunderscore}eq{\isacharparenright}\isanewline \ \ \ \ \isacommand{apply}\isamarkupfalse% \ {\isacharparenleft}unfold\ nat{\isacharunderscore}dvd{\isachardot}meet{\isacharunderscore}def{\isacharparenright}\isanewline \ \ \ \ \isacommand{apply}\isamarkupfalse% @@ -329,7 +331,9 @@ \ \ \ \ \isacommand{by}\isamarkupfalse% \ auto\isanewline \ \ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ lcm\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ dvd\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline +\ \ \ \ \isacommand{apply}\isamarkupfalse% +\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ expand{\isacharunderscore}fun{\isacharunderscore}eq{\isacharparenright}\isanewline \ \ \ \ \isacommand{apply}\isamarkupfalse% \ {\isacharparenleft}unfold\ nat{\isacharunderscore}dvd{\isachardot}join{\isacharunderscore}def{\isacharparenright}\isanewline \ \ \ \ \isacommand{apply}\isamarkupfalse% @@ -365,8 +369,7 @@ \isanewline \isacommand{lemma}\isamarkupfalse% \ gcd{\isacharunderscore}lcm{\isacharunderscore}distr{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}gcd\ {\isacharparenleft}x{\isacharcomma}\ lcm\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ lcm\ {\isacharparenleft}gcd\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isacharcomma}\ gcd\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ \isacommand{sorry}\isamarkupfalse% +\ \ {\isachardoublequoteopen}gcd\ x\ {\isacharparenleft}lcm\ y\ z{\isacharparenright}\ {\isacharequal}\ lcm\ {\isacharparenleft}gcd\ x\ y{\isacharparenright}\ {\isacharparenleft}gcd\ x\ z{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{sorry}\isamarkupfalse% \isanewline \isanewline \isacommand{ML}\isamarkupfalse% @@ -403,7 +406,7 @@ \ {\isacharparenleft}unfold\ nat{\isacharunderscore}dvd{\isacharunderscore}meet{\isacharunderscore}eq\ nat{\isacharunderscore}dvd{\isacharunderscore}join{\isacharunderscore}eq{\isacharparenright}% \begin{isamarkuptxt}% \begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ y\ z{\isachardot}\ gcd\ {\isacharparenleft}x{\isacharcomma}\ lcm\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ lcm\ {\isacharparenleft}gcd\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isacharcomma}\ gcd\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}{\isacharparenright}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ y\ z{\isachardot}\ gcd\ x\ {\isacharparenleft}lcm\ y\ z{\isacharparenright}\ {\isacharequal}\ lcm\ {\isacharparenleft}gcd\ x\ y{\isacharparenright}\ {\isacharparenleft}gcd\ x\ z{\isacharparenright}% \end{isabelle}% \end{isamarkuptxt}% \isamarkuptrue% @@ -429,9 +432,9 @@ \isa{nat{\isacharunderscore}dvd{\isachardot}less{\isacharunderscore}def} from locale \isa{partial{\isacharunderscore}order}: \\ \quad \isa{{\isacharparenleft}{\isacharquery}x\ dvd\ {\isacharquery}y\ {\isasymand}\ {\isacharquery}x\ {\isasymnoteq}\ {\isacharquery}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharquery}x\ dvd\ {\isacharquery}y\ {\isasymand}\ {\isacharquery}x\ {\isasymnoteq}\ {\isacharquery}y{\isacharparenright}} \\ \isa{nat{\isacharunderscore}dvd{\isachardot}meet{\isacharunderscore}left} from locale \isa{lattice}: \\ - \quad \isa{gcd\ {\isacharparenleft}{\isacharquery}x{\isacharcomma}\ {\isacharquery}y{\isacharparenright}\ dvd\ {\isacharquery}x} \\ + \quad \isa{gcd\ {\isacharquery}x\ {\isacharquery}y\ dvd\ {\isacharquery}x} \\ \isa{nat{\isacharunderscore}dvd{\isachardot}join{\isacharunderscore}distr} from locale \isa{distrib{\isacharunderscore}lattice}: \\ - \quad \isa{lcm\ {\isacharparenleft}{\isacharquery}x{\isacharcomma}\ gcd\ {\isacharparenleft}{\isacharquery}y{\isacharcomma}\ {\isacharquery}z{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ gcd\ {\isacharparenleft}lcm\ {\isacharparenleft}{\isacharquery}x{\isacharcomma}\ {\isacharquery}y{\isacharparenright}{\isacharcomma}\ lcm\ {\isacharparenleft}{\isacharquery}x{\isacharcomma}\ {\isacharquery}z{\isacharparenright}{\isacharparenright}} \\ + \quad \isa{lcm\ {\isacharquery}x\ {\isacharparenleft}gcd\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ gcd\ {\isacharparenleft}lcm\ {\isacharquery}x\ {\isacharquery}y{\isacharparenright}\ {\isacharparenleft}lcm\ {\isacharquery}x\ {\isacharquery}z{\isacharparenright}} \\ \end{tabular} \end{center} \hrule