# HG changeset patch # User paulson # Date 1003744895 -7200 # Node ID 181bd2050cf4c21bb4f9ba4f4f2ed960a8ebe3dc # Parent 66d4f20eb3fce9908ce5fdf8812df34c737706cc Numerals now work for the integers: the binary numerals for 0 and 1 rewrite to their abstract counterparts, while other binary numerals work correctly. diff -r 66d4f20eb3fc -r 181bd2050cf4 doc-src/TutorialI/Inductive/AB.thy --- a/doc-src/TutorialI/Inductive/AB.thy Mon Oct 22 11:55:35 2001 +0200 +++ b/doc-src/TutorialI/Inductive/AB.thy Mon Oct 22 12:01:35 2001 +0200 @@ -117,7 +117,7 @@ lemma step1: "\i < size w. \(int(size[x\take (i+1) w. P x])-int(size[x\take (i+1) w. \P x])) - - (int(size[x\take i w. P x])-int(size[x\take i w. \P x]))\ \ Numeral1" + - (int(size[x\take i w. P x])-int(size[x\take i w. \P x]))\ \ 1" txt{*\noindent The lemma is a bit hard to read because of the coercion function @@ -150,7 +150,7 @@ @{thm[source]step1}: *} -apply(insert nat0_intermed_int_val[OF step1, of "P" "w" "Numeral1"]) +apply(insert nat0_intermed_int_val[OF step1, of "P" "w" "1"]) by force text{*\noindent diff -r 66d4f20eb3fc -r 181bd2050cf4 doc-src/TutorialI/Inductive/document/AB.tex --- a/doc-src/TutorialI/Inductive/document/AB.tex Mon Oct 22 11:55:35 2001 +0200 +++ b/doc-src/TutorialI/Inductive/document/AB.tex Mon Oct 22 12:01:35 2001 +0200 @@ -110,7 +110,7 @@ 1 on our way from 0 to 2. Formally, we appeal to the following discrete intermediate value theorem \isa{nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val} \begin{isabelle}% -\ \ \ \ \ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ i\ {\isacharless}\ n\ {\isasymlongrightarrow}\ {\isasymbar}f\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharminus}\ f\ i{\isasymbar}\ {\isasymle}\ Numeral{\isadigit{1}}{\isacharsemicolon}\ f\ {\isadigit{0}}\ {\isasymle}\ k{\isacharsemicolon}\ k\ {\isasymle}\ f\ n{\isasymrbrakk}\isanewline +\ \ \ \ \ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ i\ {\isacharless}\ n\ {\isasymlongrightarrow}\ {\isasymbar}f\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharminus}\ f\ i{\isasymbar}\ {\isasymle}\ {\isadigit{1}}{\isacharsemicolon}\ f\ {\isadigit{0}}\ {\isasymle}\ k{\isacharsemicolon}\ k\ {\isasymle}\ f\ n{\isasymrbrakk}\isanewline \isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ i\ {\isasymle}\ n\ {\isasymand}\ f\ i\ {\isacharequal}\ k% \end{isabelle} where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers, @@ -128,7 +128,7 @@ \isamarkuptrue% \isacommand{lemma}\ step{\isadigit{1}}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i\ {\isacharless}\ size\ w{\isachardot}\isanewline \ \ {\isasymbar}{\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline -\ \ \ {\isacharminus}\ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isasymbar}\ {\isasymle}\ Numeral{\isadigit{1}}{\isachardoublequote}\isamarkupfalse% +\ \ \ {\isacharminus}\ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isasymbar}\ {\isasymle}\ {\isadigit{1}}{\isachardoublequote}\isamarkupfalse% % \begin{isamarkuptxt}% \noindent @@ -165,7 +165,7 @@ \isa{step{\isadigit{1}}}:% \end{isamarkuptxt}% \isamarkuptrue% -\isacommand{apply}{\isacharparenleft}insert\ nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val{\isacharbrackleft}OF\ step{\isadigit{1}}{\isacharcomma}\ of\ {\isachardoublequote}P{\isachardoublequote}\ {\isachardoublequote}w{\isachardoublequote}\ {\isachardoublequote}Numeral{\isadigit{1}}{\isachardoublequote}{\isacharbrackright}{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}insert\ nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val{\isacharbrackleft}OF\ step{\isadigit{1}}{\isacharcomma}\ of\ {\isachardoublequote}P{\isachardoublequote}\ {\isachardoublequote}w{\isachardoublequote}\ {\isachardoublequote}{\isadigit{1}}{\isachardoublequote}{\isacharbrackright}{\isacharparenright}\isanewline \isamarkupfalse% \isacommand{by}\ force\isamarkupfalse% % diff -r 66d4f20eb3fc -r 181bd2050cf4 doc-src/TutorialI/Types/document/Numbers.tex --- a/doc-src/TutorialI/Types/document/Numbers.tex Mon Oct 22 11:55:35 2001 +0200 +++ b/doc-src/TutorialI/Types/document/Numbers.tex Mon Oct 22 12:01:35 2001 +0200 @@ -208,22 +208,22 @@ \begin{isabelle}% -Numeral{\isadigit{0}}\ {\isacharless}\ b\ {\isasymLongrightarrow}\ Numeral{\isadigit{0}}\ {\isasymle}\ a\ mod\ b% +{\isadigit{0}}\ {\isacharless}\ b\ {\isasymLongrightarrow}\ {\isadigit{0}}\ {\isasymle}\ a\ mod\ b% \end{isabelle} \rulename{pos_mod_sign} \begin{isabelle}% -Numeral{\isadigit{0}}\ {\isacharless}\ b\ {\isasymLongrightarrow}\ a\ mod\ b\ {\isacharless}\ b% +{\isadigit{0}}\ {\isacharless}\ b\ {\isasymLongrightarrow}\ a\ mod\ b\ {\isacharless}\ b% \end{isabelle} \rulename{pos_mod_bound} \begin{isabelle}% -b\ {\isacharless}\ Numeral{\isadigit{0}}\ {\isasymLongrightarrow}\ a\ mod\ b\ {\isasymle}\ Numeral{\isadigit{0}}% +b\ {\isacharless}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ a\ mod\ b\ {\isasymle}\ {\isadigit{0}}% \end{isabelle} \rulename{neg_mod_sign} \begin{isabelle}% -b\ {\isacharless}\ Numeral{\isadigit{0}}\ {\isasymLongrightarrow}\ b\ {\isacharless}\ a\ mod\ b% +b\ {\isacharless}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ b\ {\isacharless}\ a\ mod\ b% \end{isabelle} \rulename{neg_mod_bound} @@ -248,12 +248,12 @@ \rulename{zmod_zmult1_eq} \begin{isabelle}% -Numeral{\isadigit{0}}\ {\isacharless}\ c\ {\isasymLongrightarrow}\ a\ div\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ a\ div\ b\ div\ c% +{\isadigit{0}}\ {\isacharless}\ c\ {\isasymLongrightarrow}\ a\ div\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ a\ div\ b\ div\ c% \end{isabelle} \rulename{zdiv_zmult2_eq} \begin{isabelle}% -Numeral{\isadigit{0}}\ {\isacharless}\ c\ {\isasymLongrightarrow}\ a\ mod\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ b\ {\isacharasterisk}\ {\isacharparenleft}a\ div\ b\ mod\ c{\isacharparenright}\ {\isacharplus}\ a\ mod\ b% +{\isadigit{0}}\ {\isacharless}\ c\ {\isasymLongrightarrow}\ a\ mod\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ b\ {\isacharasterisk}\ {\isacharparenleft}a\ div\ b\ mod\ c{\isacharparenright}\ {\isacharplus}\ a\ mod\ b% \end{isabelle} \rulename{zmod_zmult2_eq}