1.1 --- a/NEWS Thu Apr 16 17:29:56 2009 +0200
1.2 +++ b/NEWS Fri Apr 17 08:36:18 2009 +0200
1.3 @@ -1,6 +1,14 @@
1.4 Isabelle NEWS -- history user-relevant changes
1.5 ==============================================
1.6
1.7 +*** HOL ***
1.8 +
1.9 +* Class semiring_div now requires no_zero_divisors and proof of div_mult_mult1;
1.10 +theorems div_mult_mult1, div_mult_mult2, div_mult_mult1_if, div_mult_mult1 and
1.11 +div_mult_mult2 have been generalized to class semiring_div, subsuming former
1.12 +theorems zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and zdiv_zmult_zmult2.
1.13 +div_mult_mult1 is now [simp] by default. INCOMPATIBILITY.
1.14 +
1.15 New in Isabelle2009 (April 2009)
1.16 --------------------------------
1.17
2.1 --- a/doc-src/Codegen/Thy/Program.thy Thu Apr 16 17:29:56 2009 +0200
2.2 +++ b/doc-src/Codegen/Thy/Program.thy Fri Apr 17 08:36:18 2009 +0200
2.3 @@ -323,7 +323,7 @@
2.4 *}
2.5
2.6
2.7 -subsection {* Equality and wellsortedness *}
2.8 +subsection {* Equality *}
2.9
2.10 text {*
2.11 Surely you have already noticed how equality is treated
2.12 @@ -358,60 +358,7 @@
2.13 manually like any other type class.
2.14
2.15 Though this @{text eq} class is designed to get rarely in
2.16 - the way, a subtlety
2.17 - enters the stage when definitions of overloaded constants
2.18 - are dependent on operational equality. For example, let
2.19 - us define a lexicographic ordering on tuples
2.20 - (also see theory @{theory Product_ord}):
2.21 -*}
2.22 -
2.23 -instantiation %quote "*" :: (order, order) order
2.24 -begin
2.25 -
2.26 -definition %quote [code del]:
2.27 - "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x \<le> snd y"
2.28 -
2.29 -definition %quote [code del]:
2.30 - "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"
2.31 -
2.32 -instance %quote proof
2.33 -qed (auto simp: less_eq_prod_def less_prod_def intro: order_less_trans)
2.34 -
2.35 -end %quote
2.36 -
2.37 -lemma %quote order_prod [code]:
2.38 - "(x1 \<Colon> 'a\<Colon>order, y1 \<Colon> 'b\<Colon>order) < (x2, y2) \<longleftrightarrow>
2.39 - x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
2.40 - "(x1 \<Colon> 'a\<Colon>order, y1 \<Colon> 'b\<Colon>order) \<le> (x2, y2) \<longleftrightarrow>
2.41 - x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
2.42 - by (simp_all add: less_prod_def less_eq_prod_def)
2.43 -
2.44 -text {*
2.45 - \noindent Then code generation will fail. Why? The definition
2.46 - of @{term "op \<le>"} depends on equality on both arguments,
2.47 - which are polymorphic and impose an additional @{class eq}
2.48 - class constraint, which the preprocessor does not propagate
2.49 - (for technical reasons).
2.50 -
2.51 - The solution is to add @{class eq} explicitly to the first sort arguments in the
2.52 - code theorems:
2.53 -*}
2.54 -
2.55 -lemma %quote order_prod_code [code]:
2.56 - "(x1 \<Colon> 'a\<Colon>{order, eq}, y1 \<Colon> 'b\<Colon>order) < (x2, y2) \<longleftrightarrow>
2.57 - x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
2.58 - "(x1 \<Colon> 'a\<Colon>{order, eq}, y1 \<Colon> 'b\<Colon>order) \<le> (x2, y2) \<longleftrightarrow>
2.59 - x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
2.60 - by (simp_all add: less_prod_def less_eq_prod_def)
2.61 -
2.62 -text {*
2.63 - \noindent Then code generation succeeds:
2.64 -*}
2.65 -
2.66 -text %quote {*@{code_stmts "op \<le> \<Colon> _ \<times> _ \<Rightarrow> _ \<times> _ \<Rightarrow> bool" (SML)}*}
2.67 -
2.68 -text {*
2.69 - In some cases, the automatically derived code equations
2.70 + the way, in some cases the automatically derived code equations
2.71 for equality on a particular type may not be appropriate.
2.72 As example, watch the following datatype representing
2.73 monomorphic parametric types (where type constructors
3.1 --- a/doc-src/Codegen/Thy/document/Program.tex Thu Apr 16 17:29:56 2009 +0200
3.2 +++ b/doc-src/Codegen/Thy/document/Program.tex Fri Apr 17 08:36:18 2009 +0200
3.3 @@ -714,7 +714,7 @@
3.4 \end{isamarkuptext}%
3.5 \isamarkuptrue%
3.6 %
3.7 -\isamarkupsubsection{Equality and wellsortedness%
3.8 +\isamarkupsubsection{Equality%
3.9 }
3.10 \isamarkuptrue%
3.11 %
3.12 @@ -801,141 +801,7 @@
3.13 manually like any other type class.
3.14
3.15 Though this \isa{eq} class is designed to get rarely in
3.16 - the way, a subtlety
3.17 - enters the stage when definitions of overloaded constants
3.18 - are dependent on operational equality. For example, let
3.19 - us define a lexicographic ordering on tuples
3.20 - (also see theory \hyperlink{theory.Product-ord}{\mbox{\isa{Product{\isacharunderscore}ord}}}):%
3.21 -\end{isamarkuptext}%
3.22 -\isamarkuptrue%
3.23 -%
3.24 -\isadelimquote
3.25 -%
3.26 -\endisadelimquote
3.27 -%
3.28 -\isatagquote
3.29 -\isacommand{instantiation}\isamarkupfalse%
3.30 -\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}order{\isacharcomma}\ order{\isacharparenright}\ order\isanewline
3.31 -\isakeyword{begin}\isanewline
3.32 -\isanewline
3.33 -\isacommand{definition}\isamarkupfalse%
3.34 -\ {\isacharbrackleft}code\ del{\isacharbrackright}{\isacharcolon}\isanewline
3.35 -\ \ {\isachardoublequoteopen}x\ {\isasymle}\ y\ {\isasymlongleftrightarrow}\ fst\ x\ {\isacharless}\ fst\ y\ {\isasymor}\ fst\ x\ {\isacharequal}\ fst\ y\ {\isasymand}\ snd\ x\ {\isasymle}\ snd\ y{\isachardoublequoteclose}\isanewline
3.36 -\isanewline
3.37 -\isacommand{definition}\isamarkupfalse%
3.38 -\ {\isacharbrackleft}code\ del{\isacharbrackright}{\isacharcolon}\isanewline
3.39 -\ \ {\isachardoublequoteopen}x\ {\isacharless}\ y\ {\isasymlongleftrightarrow}\ fst\ x\ {\isacharless}\ fst\ y\ {\isasymor}\ fst\ x\ {\isacharequal}\ fst\ y\ {\isasymand}\ snd\ x\ {\isacharless}\ snd\ y{\isachardoublequoteclose}\isanewline
3.40 -\isanewline
3.41 -\isacommand{instance}\isamarkupfalse%
3.42 -\ \isacommand{proof}\isamarkupfalse%
3.43 -\isanewline
3.44 -\isacommand{qed}\isamarkupfalse%
3.45 -\ {\isacharparenleft}auto\ simp{\isacharcolon}\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}prod{\isacharunderscore}def\ intro{\isacharcolon}\ order{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}\isanewline
3.46 -\isanewline
3.47 -\isacommand{end}\isamarkupfalse%
3.48 -\isanewline
3.49 -\isanewline
3.50 -\isacommand{lemma}\isamarkupfalse%
3.51 -\ order{\isacharunderscore}prod\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
3.52 -\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}order{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
3.53 -\ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline
3.54 -\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}order{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
3.55 -\ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline
3.56 -\ \ \isacommand{by}\isamarkupfalse%
3.57 -\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}%
3.58 -\endisatagquote
3.59 -{\isafoldquote}%
3.60 -%
3.61 -\isadelimquote
3.62 -%
3.63 -\endisadelimquote
3.64 -%
3.65 -\begin{isamarkuptext}%
3.66 -\noindent Then code generation will fail. Why? The definition
3.67 - of \isa{op\ {\isasymle}} depends on equality on both arguments,
3.68 - which are polymorphic and impose an additional \isa{eq}
3.69 - class constraint, which the preprocessor does not propagate
3.70 - (for technical reasons).
3.71 -
3.72 - The solution is to add \isa{eq} explicitly to the first sort arguments in the
3.73 - code theorems:%
3.74 -\end{isamarkuptext}%
3.75 -\isamarkuptrue%
3.76 -%
3.77 -\isadelimquote
3.78 -%
3.79 -\endisadelimquote
3.80 -%
3.81 -\isatagquote
3.82 -\isacommand{lemma}\isamarkupfalse%
3.83 -\ order{\isacharunderscore}prod{\isacharunderscore}code\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
3.84 -\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}order{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
3.85 -\ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline
3.86 -\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}order{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
3.87 -\ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline
3.88 -\ \ \isacommand{by}\isamarkupfalse%
3.89 -\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}%
3.90 -\endisatagquote
3.91 -{\isafoldquote}%
3.92 -%
3.93 -\isadelimquote
3.94 -%
3.95 -\endisadelimquote
3.96 -%
3.97 -\begin{isamarkuptext}%
3.98 -\noindent Then code generation succeeds:%
3.99 -\end{isamarkuptext}%
3.100 -\isamarkuptrue%
3.101 -%
3.102 -\isadelimquote
3.103 -%
3.104 -\endisadelimquote
3.105 -%
3.106 -\isatagquote
3.107 -%
3.108 -\begin{isamarkuptext}%
3.109 -\isatypewriter%
3.110 -\noindent%
3.111 -\hspace*{0pt}structure Example = \\
3.112 -\hspace*{0pt}struct\\
3.113 -\hspace*{0pt}\\
3.114 -\hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\
3.115 -\hspace*{0pt}fun eq (A{\char95}:'a eq) = {\char35}eq A{\char95};\\
3.116 -\hspace*{0pt}\\
3.117 -\hspace*{0pt}type 'a ord = {\char123}less{\char95}eq :~'a -> 'a -> bool,~less :~'a -> 'a -> bool{\char125};\\
3.118 -\hspace*{0pt}fun less{\char95}eq (A{\char95}:'a ord) = {\char35}less{\char95}eq A{\char95};\\
3.119 -\hspace*{0pt}fun less (A{\char95}:'a ord) = {\char35}less A{\char95};\\
3.120 -\hspace*{0pt}\\
3.121 -\hspace*{0pt}fun eqop A{\char95}~a b = eq A{\char95}~a b;\\
3.122 -\hspace*{0pt}\\
3.123 -\hspace*{0pt}type 'a preorder = {\char123}Orderings{\char95}{\char95}ord{\char95}preorder :~'a ord{\char125};\\
3.124 -\hspace*{0pt}fun ord{\char95}preorder (A{\char95}:'a preorder) = {\char35}Orderings{\char95}{\char95}ord{\char95}preorder A{\char95};\\
3.125 -\hspace*{0pt}\\
3.126 -\hspace*{0pt}type 'a order = {\char123}Orderings{\char95}{\char95}preorder{\char95}order :~'a preorder{\char125};\\
3.127 -\hspace*{0pt}fun preorder{\char95}order (A{\char95}:'a order) = {\char35}Orderings{\char95}{\char95}preorder{\char95}order A{\char95};\\
3.128 -\hspace*{0pt}\\
3.129 -\hspace*{0pt}fun less{\char95}eqa (A1{\char95},~A2{\char95}) B{\char95}~(x1,~y1) (x2,~y2) =\\
3.130 -\hspace*{0pt} ~less ((ord{\char95}preorder o preorder{\char95}order) A2{\char95}) x1 x2 orelse\\
3.131 -\hspace*{0pt} ~~~eqop A1{\char95}~x1 x2 andalso\\
3.132 -\hspace*{0pt} ~~~~~less{\char95}eq ((ord{\char95}preorder o preorder{\char95}order) B{\char95}) y1 y2\\
3.133 -\hspace*{0pt} ~| less{\char95}eqa (A1{\char95},~A2{\char95}) B{\char95}~(x1,~y1) (x2,~y2) =\\
3.134 -\hspace*{0pt} ~~~less ((ord{\char95}preorder o preorder{\char95}order) A2{\char95}) x1 x2 orelse\\
3.135 -\hspace*{0pt} ~~~~~eqop A1{\char95}~x1 x2 andalso\\
3.136 -\hspace*{0pt} ~~~~~~~less{\char95}eq ((ord{\char95}preorder o preorder{\char95}order) B{\char95}) y1 y2;\\
3.137 -\hspace*{0pt}\\
3.138 -\hspace*{0pt}end;~(*struct Example*)%
3.139 -\end{isamarkuptext}%
3.140 -\isamarkuptrue%
3.141 -%
3.142 -\endisatagquote
3.143 -{\isafoldquote}%
3.144 -%
3.145 -\isadelimquote
3.146 -%
3.147 -\endisadelimquote
3.148 -%
3.149 -\begin{isamarkuptext}%
3.150 -In some cases, the automatically derived code equations
3.151 + the way, in some cases the automatically derived code equations
3.152 for equality on a particular type may not be appropriate.
3.153 As example, watch the following datatype representing
3.154 monomorphic parametric types (where type constructors
4.1 --- a/src/HOL/Code_Setup.thy Thu Apr 16 17:29:56 2009 +0200
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,253 +0,0 @@
4.4 -(* Title: HOL/Code_Setup.thy
4.5 - ID: $Id$
4.6 - Author: Florian Haftmann
4.7 -*)
4.8 -
4.9 -header {* Setup of code generators and related tools *}
4.10 -
4.11 -theory Code_Setup
4.12 -imports HOL
4.13 -begin
4.14 -
4.15 -subsection {* Generic code generator foundation *}
4.16 -
4.17 -text {* Datatypes *}
4.18 -
4.19 -code_datatype True False
4.20 -
4.21 -code_datatype "TYPE('a\<Colon>{})"
4.22 -
4.23 -code_datatype Trueprop "prop"
4.24 -
4.25 -text {* Code equations *}
4.26 -
4.27 -lemma [code]:
4.28 - shows "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
4.29 - and "(False \<Longrightarrow> Q) \<equiv> Trueprop True"
4.30 - and "(PROP P \<Longrightarrow> True) \<equiv> Trueprop True"
4.31 - and "(Q \<Longrightarrow> False) \<equiv> Trueprop (\<not> Q)" by (auto intro!: equal_intr_rule)
4.32 -
4.33 -lemma [code]:
4.34 - shows "False \<and> x \<longleftrightarrow> False"
4.35 - and "True \<and> x \<longleftrightarrow> x"
4.36 - and "x \<and> False \<longleftrightarrow> False"
4.37 - and "x \<and> True \<longleftrightarrow> x" by simp_all
4.38 -
4.39 -lemma [code]:
4.40 - shows "False \<or> x \<longleftrightarrow> x"
4.41 - and "True \<or> x \<longleftrightarrow> True"
4.42 - and "x \<or> False \<longleftrightarrow> x"
4.43 - and "x \<or> True \<longleftrightarrow> True" by simp_all
4.44 -
4.45 -lemma [code]:
4.46 - shows "\<not> True \<longleftrightarrow> False"
4.47 - and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+
4.48 -
4.49 -lemmas [code] = Let_def if_True if_False
4.50 -
4.51 -lemmas [code, code unfold, symmetric, code post] = imp_conv_disj
4.52 -
4.53 -text {* Equality *}
4.54 -
4.55 -context eq
4.56 -begin
4.57 -
4.58 -lemma equals_eq [code inline, code]: "op = \<equiv> eq"
4.59 - by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
4.60 -
4.61 -declare eq [code unfold, code inline del]
4.62 -
4.63 -declare equals_eq [symmetric, code post]
4.64 -
4.65 -end
4.66 -
4.67 -declare simp_thms(6) [code nbe]
4.68 -
4.69 -hide (open) const eq
4.70 -hide const eq
4.71 -
4.72 -setup {*
4.73 - Code_Unit.add_const_alias @{thm equals_eq}
4.74 -*}
4.75 -
4.76 -text {* Cases *}
4.77 -
4.78 -lemma Let_case_cert:
4.79 - assumes "CASE \<equiv> (\<lambda>x. Let x f)"
4.80 - shows "CASE x \<equiv> f x"
4.81 - using assms by simp_all
4.82 -
4.83 -lemma If_case_cert:
4.84 - assumes "CASE \<equiv> (\<lambda>b. If b f g)"
4.85 - shows "(CASE True \<equiv> f) &&& (CASE False \<equiv> g)"
4.86 - using assms by simp_all
4.87 -
4.88 -setup {*
4.89 - Code.add_case @{thm Let_case_cert}
4.90 - #> Code.add_case @{thm If_case_cert}
4.91 - #> Code.add_undefined @{const_name undefined}
4.92 -*}
4.93 -
4.94 -code_abort undefined
4.95 -
4.96 -
4.97 -subsection {* Generic code generator preprocessor *}
4.98 -
4.99 -setup {*
4.100 - Code.map_pre (K HOL_basic_ss)
4.101 - #> Code.map_post (K HOL_basic_ss)
4.102 -*}
4.103 -
4.104 -
4.105 -subsection {* Generic code generator target languages *}
4.106 -
4.107 -text {* type bool *}
4.108 -
4.109 -code_type bool
4.110 - (SML "bool")
4.111 - (OCaml "bool")
4.112 - (Haskell "Bool")
4.113 -
4.114 -code_const True and False and Not and "op &" and "op |" and If
4.115 - (SML "true" and "false" and "not"
4.116 - and infixl 1 "andalso" and infixl 0 "orelse"
4.117 - and "!(if (_)/ then (_)/ else (_))")
4.118 - (OCaml "true" and "false" and "not"
4.119 - and infixl 4 "&&" and infixl 2 "||"
4.120 - and "!(if (_)/ then (_)/ else (_))")
4.121 - (Haskell "True" and "False" and "not"
4.122 - and infixl 3 "&&" and infixl 2 "||"
4.123 - and "!(if (_)/ then (_)/ else (_))")
4.124 -
4.125 -code_reserved SML
4.126 - bool true false not
4.127 -
4.128 -code_reserved OCaml
4.129 - bool not
4.130 -
4.131 -text {* using built-in Haskell equality *}
4.132 -
4.133 -code_class eq
4.134 - (Haskell "Eq")
4.135 -
4.136 -code_const "eq_class.eq"
4.137 - (Haskell infixl 4 "==")
4.138 -
4.139 -code_const "op ="
4.140 - (Haskell infixl 4 "==")
4.141 -
4.142 -text {* undefined *}
4.143 -
4.144 -code_const undefined
4.145 - (SML "!(raise/ Fail/ \"undefined\")")
4.146 - (OCaml "failwith/ \"undefined\"")
4.147 - (Haskell "error/ \"undefined\"")
4.148 -
4.149 -
4.150 -subsection {* SML code generator setup *}
4.151 -
4.152 -types_code
4.153 - "bool" ("bool")
4.154 -attach (term_of) {*
4.155 -fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
4.156 -*}
4.157 -attach (test) {*
4.158 -fun gen_bool i =
4.159 - let val b = one_of [false, true]
4.160 - in (b, fn () => term_of_bool b) end;
4.161 -*}
4.162 - "prop" ("bool")
4.163 -attach (term_of) {*
4.164 -fun term_of_prop b =
4.165 - HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);
4.166 -*}
4.167 -
4.168 -consts_code
4.169 - "Trueprop" ("(_)")
4.170 - "True" ("true")
4.171 - "False" ("false")
4.172 - "Not" ("Bool.not")
4.173 - "op |" ("(_ orelse/ _)")
4.174 - "op &" ("(_ andalso/ _)")
4.175 - "If" ("(if _/ then _/ else _)")
4.176 -
4.177 -setup {*
4.178 -let
4.179 -
4.180 -fun eq_codegen thy defs dep thyname b t gr =
4.181 - (case strip_comb t of
4.182 - (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
4.183 - | (Const ("op =", _), [t, u]) =>
4.184 - let
4.185 - val (pt, gr') = Codegen.invoke_codegen thy defs dep thyname false t gr;
4.186 - val (pu, gr'') = Codegen.invoke_codegen thy defs dep thyname false u gr';
4.187 - val (_, gr''') = Codegen.invoke_tycodegen thy defs dep thyname false HOLogic.boolT gr'';
4.188 - in
4.189 - SOME (Codegen.parens
4.190 - (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]), gr''')
4.191 - end
4.192 - | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
4.193 - thy defs dep thyname b (Codegen.eta_expand t ts 2) gr)
4.194 - | _ => NONE);
4.195 -
4.196 -in
4.197 - Codegen.add_codegen "eq_codegen" eq_codegen
4.198 -end
4.199 -*}
4.200 -
4.201 -
4.202 -subsection {* Evaluation and normalization by evaluation *}
4.203 -
4.204 -setup {*
4.205 - Value.add_evaluator ("SML", Codegen.eval_term o ProofContext.theory_of)
4.206 -*}
4.207 -
4.208 -ML {*
4.209 -structure Eval_Method =
4.210 -struct
4.211 -
4.212 -val eval_ref : (unit -> bool) option ref = ref NONE;
4.213 -
4.214 -end;
4.215 -*}
4.216 -
4.217 -oracle eval_oracle = {* fn ct =>
4.218 - let
4.219 - val thy = Thm.theory_of_cterm ct;
4.220 - val t = Thm.term_of ct;
4.221 - val dummy = @{cprop True};
4.222 - in case try HOLogic.dest_Trueprop t
4.223 - of SOME t' => if Code_ML.eval_term
4.224 - ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy t' []
4.225 - then Thm.capply (Thm.capply @{cterm "op \<equiv> \<Colon> prop \<Rightarrow> prop \<Rightarrow> prop"} ct) dummy
4.226 - else dummy
4.227 - | NONE => dummy
4.228 - end
4.229 -*}
4.230 -
4.231 -ML {*
4.232 -fun gen_eval_method conv ctxt = SIMPLE_METHOD'
4.233 - (CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt)
4.234 - THEN' rtac TrueI)
4.235 -*}
4.236 -
4.237 -method_setup eval = {* Scan.succeed (gen_eval_method eval_oracle) *}
4.238 - "solve goal by evaluation"
4.239 -
4.240 -method_setup evaluation = {* Scan.succeed (gen_eval_method Codegen.evaluation_conv) *}
4.241 - "solve goal by evaluation"
4.242 -
4.243 -method_setup normalization = {*
4.244 - Scan.succeed (K (SIMPLE_METHOD' (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))))
4.245 -*} "solve goal by normalization"
4.246 -
4.247 -
4.248 -subsection {* Quickcheck *}
4.249 -
4.250 -setup {*
4.251 - Quickcheck.add_generator ("SML", Codegen.test_term)
4.252 -*}
4.253 -
4.254 -quickcheck_params [size = 5, iterations = 50]
4.255 -
4.256 -end
5.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML Thu Apr 16 17:29:56 2009 +0200
5.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Fri Apr 17 08:36:18 2009 +0200
5.3 @@ -76,7 +76,7 @@
5.4 @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
5.5 Suc_plus1]
5.6 addsimps @{thms add_ac}
5.7 - addsimprocs [cancel_div_mod_proc]
5.8 + addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
5.9 val simpset0 = HOL_basic_ss
5.10 addsimps [mod_div_equality', Suc_plus1]
5.11 addsimps comp_arith
6.1 --- a/src/HOL/Decision_Procs/mir_tac.ML Thu Apr 16 17:29:56 2009 +0200
6.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML Fri Apr 17 08:36:18 2009 +0200
6.3 @@ -99,7 +99,7 @@
6.4 @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
6.5 @{thm "Suc_plus1"}]
6.6 addsimps @{thms add_ac}
6.7 - addsimprocs [cancel_div_mod_proc]
6.8 + addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
6.9 val simpset0 = HOL_basic_ss
6.10 addsimps [mod_div_equality', Suc_plus1]
6.11 addsimps comp_ths
7.1 --- a/src/HOL/Divides.thy Thu Apr 16 17:29:56 2009 +0200
7.2 +++ b/src/HOL/Divides.thy Fri Apr 17 08:36:18 2009 +0200
7.3 @@ -1,5 +1,4 @@
7.4 (* Title: HOL/Divides.thy
7.5 - ID: $Id$
7.6 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
7.7 Copyright 1999 University of Cambridge
7.8 *)
7.9 @@ -20,11 +19,12 @@
7.10
7.11 subsection {* Abstract division in commutative semirings. *}
7.12
7.13 -class semiring_div = comm_semiring_1_cancel + div +
7.14 +class semiring_div = comm_semiring_1_cancel + no_zero_divisors + div +
7.15 assumes mod_div_equality: "a div b * b + a mod b = a"
7.16 and div_by_0 [simp]: "a div 0 = 0"
7.17 and div_0 [simp]: "0 div a = 0"
7.18 and div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
7.19 + and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
7.20 begin
7.21
7.22 text {* @{const div} and @{const mod} *}
7.23 @@ -38,16 +38,16 @@
7.24 by (simp only: add_ac)
7.25
7.26 lemma div_mod_equality: "((a div b) * b + a mod b) + c = a + c"
7.27 -by (simp add: mod_div_equality)
7.28 + by (simp add: mod_div_equality)
7.29
7.30 lemma div_mod_equality2: "(b * (a div b) + a mod b) + c = a + c"
7.31 -by (simp add: mod_div_equality2)
7.32 + by (simp add: mod_div_equality2)
7.33
7.34 lemma mod_by_0 [simp]: "a mod 0 = a"
7.35 -using mod_div_equality [of a zero] by simp
7.36 + using mod_div_equality [of a zero] by simp
7.37
7.38 lemma mod_0 [simp]: "0 mod a = 0"
7.39 -using mod_div_equality [of zero a] div_0 by simp
7.40 + using mod_div_equality [of zero a] div_0 by simp
7.41
7.42 lemma div_mult_self2 [simp]:
7.43 assumes "b \<noteq> 0"
7.44 @@ -72,7 +72,7 @@
7.45 qed
7.46
7.47 lemma mod_mult_self2 [simp]: "(a + b * c) mod b = a mod b"
7.48 -by (simp add: mult_commute [of b])
7.49 + by (simp add: mult_commute [of b])
7.50
7.51 lemma div_mult_self1_is_id [simp]: "b \<noteq> 0 \<Longrightarrow> b * a div b = a"
7.52 using div_mult_self2 [of b 0 a] by simp
7.53 @@ -238,9 +238,9 @@
7.54 by (simp only: mod_add_eq [symmetric])
7.55 qed
7.56
7.57 -lemma div_add[simp]: "z dvd x \<Longrightarrow> z dvd y
7.58 +lemma div_add [simp]: "z dvd x \<Longrightarrow> z dvd y
7.59 \<Longrightarrow> (x + y) div z = x div z + y div z"
7.60 -by(cases "z=0", simp, unfold dvd_def, auto simp add: algebra_simps)
7.61 +by (cases "z = 0", simp, unfold dvd_def, auto simp add: algebra_simps)
7.62
7.63 text {* Multiplication respects modular equivalence. *}
7.64
7.65 @@ -297,21 +297,41 @@
7.66 finally show ?thesis .
7.67 qed
7.68
7.69 -end
7.70 -
7.71 -lemma div_mult_div_if_dvd: "(y::'a::{semiring_div,no_zero_divisors}) dvd x \<Longrightarrow>
7.72 - z dvd w \<Longrightarrow> (x div y) * (w div z) = (x * w) div (y * z)"
7.73 -unfolding dvd_def
7.74 - apply clarify
7.75 - apply (case_tac "y = 0")
7.76 - apply simp
7.77 - apply (case_tac "z = 0")
7.78 - apply simp
7.79 - apply (simp add: algebra_simps)
7.80 +lemma div_mult_div_if_dvd:
7.81 + "y dvd x \<Longrightarrow> z dvd w \<Longrightarrow> (x div y) * (w div z) = (x * w) div (y * z)"
7.82 + apply (cases "y = 0", simp)
7.83 + apply (cases "z = 0", simp)
7.84 + apply (auto elim!: dvdE simp add: algebra_simps)
7.85 apply (subst mult_assoc [symmetric])
7.86 apply (simp add: no_zero_divisors)
7.87 -done
7.88 + done
7.89
7.90 +lemma div_mult_mult2 [simp]:
7.91 + "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"
7.92 + by (drule div_mult_mult1) (simp add: mult_commute)
7.93 +
7.94 +lemma div_mult_mult1_if [simp]:
7.95 + "(c * a) div (c * b) = (if c = 0 then 0 else a div b)"
7.96 + by simp_all
7.97 +
7.98 +lemma mod_mult_mult1:
7.99 + "(c * a) mod (c * b) = c * (a mod b)"
7.100 +proof (cases "c = 0")
7.101 + case True then show ?thesis by simp
7.102 +next
7.103 + case False
7.104 + from mod_div_equality
7.105 + have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" .
7.106 + with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b)
7.107 + = c * a + c * (a mod b)" by (simp add: algebra_simps)
7.108 + with mod_div_equality show ?thesis by simp
7.109 +qed
7.110 +
7.111 +lemma mod_mult_mult2:
7.112 + "(a * c) mod (b * c) = (a mod b) * c"
7.113 + using mod_mult_mult1 [of c a b] by (simp add: mult_commute)
7.114 +
7.115 +end
7.116
7.117 lemma div_power: "(y::'a::{semiring_div,no_zero_divisors,recpower}) dvd x \<Longrightarrow>
7.118 (x div y)^n = x^n div y^n"
7.119 @@ -398,15 +418,17 @@
7.120 @{term "q\<Colon>nat"}(uotient) and @{term "r\<Colon>nat"}(emainder).
7.121 *}
7.122
7.123 -definition divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
7.124 - "divmod_rel m n q r \<longleftrightarrow> m = q * n + r \<and> (if n > 0 then 0 \<le> r \<and> r < n else q = 0)"
7.125 +definition divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat \<Rightarrow> bool" where
7.126 + "divmod_rel m n qr \<longleftrightarrow>
7.127 + m = fst qr * n + snd qr \<and>
7.128 + (if n = 0 then fst qr = 0 else if n > 0 then 0 \<le> snd qr \<and> snd qr < n else n < snd qr \<and> snd qr \<le> 0)"
7.129
7.130 text {* @{const divmod_rel} is total: *}
7.131
7.132 lemma divmod_rel_ex:
7.133 - obtains q r where "divmod_rel m n q r"
7.134 + obtains q r where "divmod_rel m n (q, r)"
7.135 proof (cases "n = 0")
7.136 - case True with that show thesis
7.137 + case True with that show thesis
7.138 by (auto simp add: divmod_rel_def)
7.139 next
7.140 case False
7.141 @@ -436,13 +458,14 @@
7.142
7.143 text {* @{const divmod_rel} is injective: *}
7.144
7.145 -lemma divmod_rel_unique_div:
7.146 - assumes "divmod_rel m n q r"
7.147 - and "divmod_rel m n q' r'"
7.148 - shows "q = q'"
7.149 +lemma divmod_rel_unique:
7.150 + assumes "divmod_rel m n qr"
7.151 + and "divmod_rel m n qr'"
7.152 + shows "qr = qr'"
7.153 proof (cases "n = 0")
7.154 case True with assms show ?thesis
7.155 - by (simp add: divmod_rel_def)
7.156 + by (cases qr, cases qr')
7.157 + (simp add: divmod_rel_def)
7.158 next
7.159 case False
7.160 have aux: "\<And>q r q' r'. q' * n + r' = q * n + r \<Longrightarrow> r < n \<Longrightarrow> q' \<le> (q\<Colon>nat)"
7.161 @@ -450,18 +473,11 @@
7.162 apply (subst less_iff_Suc_add)
7.163 apply (auto simp add: add_mult_distrib)
7.164 done
7.165 - from `n \<noteq> 0` assms show ?thesis
7.166 - by (auto simp add: divmod_rel_def
7.167 - intro: order_antisym dest: aux sym)
7.168 -qed
7.169 -
7.170 -lemma divmod_rel_unique_mod:
7.171 - assumes "divmod_rel m n q r"
7.172 - and "divmod_rel m n q' r'"
7.173 - shows "r = r'"
7.174 -proof -
7.175 - from assms have "q = q'" by (rule divmod_rel_unique_div)
7.176 - with assms show ?thesis by (simp add: divmod_rel_def)
7.177 + from `n \<noteq> 0` assms have "fst qr = fst qr'"
7.178 + by (auto simp add: divmod_rel_def intro: order_antisym dest: aux sym)
7.179 + moreover from this assms have "snd qr = snd qr'"
7.180 + by (simp add: divmod_rel_def)
7.181 + ultimately show ?thesis by (cases qr, cases qr') simp
7.182 qed
7.183
7.184 text {*
7.185 @@ -473,7 +489,21 @@
7.186 begin
7.187
7.188 definition divmod :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
7.189 - [code del]: "divmod m n = (THE (q, r). divmod_rel m n q r)"
7.190 + [code del]: "divmod m n = (THE qr. divmod_rel m n qr)"
7.191 +
7.192 +lemma divmod_rel_divmod:
7.193 + "divmod_rel m n (divmod m n)"
7.194 +proof -
7.195 + from divmod_rel_ex
7.196 + obtain qr where rel: "divmod_rel m n qr" .
7.197 + then show ?thesis
7.198 + by (auto simp add: divmod_def intro: theI elim: divmod_rel_unique)
7.199 +qed
7.200 +
7.201 +lemma divmod_eq:
7.202 + assumes "divmod_rel m n qr"
7.203 + shows "divmod m n = qr"
7.204 + using assms by (auto intro: divmod_rel_unique divmod_rel_divmod)
7.205
7.206 definition div_nat where
7.207 "m div n = fst (divmod m n)"
7.208 @@ -485,30 +515,18 @@
7.209 "divmod m n = (m div n, m mod n)"
7.210 unfolding div_nat_def mod_nat_def by simp
7.211
7.212 -lemma divmod_eq:
7.213 - assumes "divmod_rel m n q r"
7.214 - shows "divmod m n = (q, r)"
7.215 - using assms by (auto simp add: divmod_def
7.216 - dest: divmod_rel_unique_div divmod_rel_unique_mod)
7.217 -
7.218 lemma div_eq:
7.219 - assumes "divmod_rel m n q r"
7.220 + assumes "divmod_rel m n (q, r)"
7.221 shows "m div n = q"
7.222 - using assms by (auto dest: divmod_eq simp add: div_nat_def)
7.223 + using assms by (auto dest: divmod_eq simp add: divmod_div_mod)
7.224
7.225 lemma mod_eq:
7.226 - assumes "divmod_rel m n q r"
7.227 + assumes "divmod_rel m n (q, r)"
7.228 shows "m mod n = r"
7.229 - using assms by (auto dest: divmod_eq simp add: mod_nat_def)
7.230 + using assms by (auto dest: divmod_eq simp add: divmod_div_mod)
7.231
7.232 -lemma divmod_rel: "divmod_rel m n (m div n) (m mod n)"
7.233 -proof -
7.234 - from divmod_rel_ex
7.235 - obtain q r where rel: "divmod_rel m n q r" .
7.236 - moreover with div_eq mod_eq have "m div n = q" and "m mod n = r"
7.237 - by simp_all
7.238 - ultimately show ?thesis by simp
7.239 -qed
7.240 +lemma divmod_rel: "divmod_rel m n (m div n, m mod n)"
7.241 + by (simp add: div_nat_def mod_nat_def divmod_rel_divmod)
7.242
7.243 lemma divmod_zero:
7.244 "divmod m 0 = (0, m)"
7.245 @@ -531,10 +549,10 @@
7.246 assumes "0 < n" and "n \<le> m"
7.247 shows "divmod m n = (Suc ((m - n) div n), (m - n) mod n)"
7.248 proof -
7.249 - from divmod_rel have divmod_m_n: "divmod_rel m n (m div n) (m mod n)" .
7.250 + from divmod_rel have divmod_m_n: "divmod_rel m n (m div n, m mod n)" .
7.251 with assms have m_div_n: "m div n \<ge> 1"
7.252 by (cases "m div n") (auto simp add: divmod_rel_def)
7.253 - from assms divmod_m_n have "divmod_rel (m - n) n (m div n - Suc 0) (m mod n)"
7.254 + from assms divmod_m_n have "divmod_rel (m - n) n (m div n - Suc 0, m mod n)"
7.255 by (cases "m div n") (auto simp add: divmod_rel_def)
7.256 with divmod_eq have "divmod (m - n) n = (m div n - Suc 0, m mod n)" by simp
7.257 moreover from divmod_div_mod have "divmod (m - n) n = ((m - n) div n, (m - n) mod n)" .
7.258 @@ -569,55 +587,74 @@
7.259 shows "m mod n = (m - n) mod n"
7.260 using assms divmod_step divmod_div_mod by (cases "n = 0") simp_all
7.261
7.262 -instance proof
7.263 - fix m n :: nat show "m div n * n + m mod n = m"
7.264 - using divmod_rel [of m n] by (simp add: divmod_rel_def)
7.265 -next
7.266 - fix n :: nat show "n div 0 = 0"
7.267 - using divmod_zero divmod_div_mod [of n 0] by simp
7.268 -next
7.269 - fix n :: nat show "0 div n = 0"
7.270 - using divmod_rel [of 0 n] by (cases n) (simp_all add: divmod_rel_def)
7.271 -next
7.272 - fix m n q :: nat assume "n \<noteq> 0" then show "(q + m * n) div n = m + q div n"
7.273 - by (induct m) (simp_all add: le_div_geq)
7.274 +instance proof -
7.275 + have [simp]: "\<And>n::nat. n div 0 = 0"
7.276 + by (simp add: div_nat_def divmod_zero)
7.277 + have [simp]: "\<And>n::nat. 0 div n = 0"
7.278 + proof -
7.279 + fix n :: nat
7.280 + show "0 div n = 0"
7.281 + by (cases "n = 0") simp_all
7.282 + qed
7.283 + show "OFCLASS(nat, semiring_div_class)" proof
7.284 + fix m n :: nat
7.285 + show "m div n * n + m mod n = m"
7.286 + using divmod_rel [of m n] by (simp add: divmod_rel_def)
7.287 + next
7.288 + fix m n q :: nat
7.289 + assume "n \<noteq> 0"
7.290 + then show "(q + m * n) div n = m + q div n"
7.291 + by (induct m) (simp_all add: le_div_geq)
7.292 + next
7.293 + fix m n q :: nat
7.294 + assume "m \<noteq> 0"
7.295 + then show "(m * n) div (m * q) = n div q"
7.296 + proof (cases "n \<noteq> 0 \<and> q \<noteq> 0")
7.297 + case False then show ?thesis by auto
7.298 + next
7.299 + case True with `m \<noteq> 0`
7.300 + have "m > 0" and "n > 0" and "q > 0" by auto
7.301 + then have "\<And>a b. divmod_rel n q (a, b) \<Longrightarrow> divmod_rel (m * n) (m * q) (a, m * b)"
7.302 + by (auto simp add: divmod_rel_def) (simp_all add: algebra_simps)
7.303 + moreover from divmod_rel have "divmod_rel n q (n div q, n mod q)" .
7.304 + ultimately have "divmod_rel (m * n) (m * q) (n div q, m * (n mod q))" .
7.305 + then show ?thesis by (simp add: div_eq)
7.306 + qed
7.307 + qed simp_all
7.308 qed
7.309
7.310 end
7.311
7.312 text {* Simproc for cancelling @{const div} and @{const mod} *}
7.313
7.314 -(*lemmas mod_div_equality_nat = semiring_div_class.times_div_mod_plus_zero_one.mod_div_equality [of "m\<Colon>nat" n, standard]
7.315 -lemmas mod_div_equality2_nat = mod_div_equality2 [of "n\<Colon>nat" m, standard*)
7.316 +ML {*
7.317 +local
7.318
7.319 -ML {*
7.320 -structure CancelDivModData =
7.321 -struct
7.322 +structure CancelDivMod = CancelDivModFun(struct
7.323
7.324 -val div_name = @{const_name div};
7.325 -val mod_name = @{const_name mod};
7.326 -val mk_binop = HOLogic.mk_binop;
7.327 -val mk_sum = Nat_Arith.mk_sum;
7.328 -val dest_sum = Nat_Arith.dest_sum;
7.329 + val div_name = @{const_name div};
7.330 + val mod_name = @{const_name mod};
7.331 + val mk_binop = HOLogic.mk_binop;
7.332 + val mk_sum = Nat_Arith.mk_sum;
7.333 + val dest_sum = Nat_Arith.dest_sum;
7.334
7.335 -(*logic*)
7.336 + val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
7.337
7.338 -val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}]
7.339 + val trans = trans;
7.340
7.341 -val trans = trans
7.342 + val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
7.343 + (@{thm monoid_add_class.add_0_left} :: @{thm monoid_add_class.add_0_right} :: @{thms add_ac}))
7.344
7.345 -val prove_eq_sums =
7.346 - let val simps = @{thm add_0} :: @{thm add_0_right} :: @{thms add_ac}
7.347 - in Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac simps) end;
7.348 +end)
7.349
7.350 -end;
7.351 +in
7.352
7.353 -structure CancelDivMod = CancelDivModFun(CancelDivModData);
7.354 -
7.355 -val cancel_div_mod_proc = Simplifier.simproc (the_context ())
7.356 +val cancel_div_mod_nat_proc = Simplifier.simproc (the_context ())
7.357 "cancel_div_mod" ["(m::nat) + n"] (K CancelDivMod.proc);
7.358
7.359 -Addsimprocs[cancel_div_mod_proc];
7.360 +val _ = Addsimprocs [cancel_div_mod_nat_proc];
7.361 +
7.362 +end
7.363 *}
7.364
7.365 text {* code generator setup *}
7.366 @@ -658,7 +695,7 @@
7.367 fixes m n :: nat
7.368 assumes "n > 0"
7.369 shows "m mod n < (n::nat)"
7.370 - using assms divmod_rel unfolding divmod_rel_def by auto
7.371 + using assms divmod_rel [of m n] unfolding divmod_rel_def by auto
7.372
7.373 lemma mod_less_eq_dividend [simp]:
7.374 fixes m n :: nat
7.375 @@ -700,18 +737,19 @@
7.376 subsubsection {* Quotient and Remainder *}
7.377
7.378 lemma divmod_rel_mult1_eq:
7.379 - "[| divmod_rel b c q r; c > 0 |]
7.380 - ==> divmod_rel (a*b) c (a*q + a*r div c) (a*r mod c)"
7.381 + "divmod_rel b c (q, r) \<Longrightarrow> c > 0
7.382 + \<Longrightarrow> divmod_rel (a * b) c (a * q + a * r div c, a * r mod c)"
7.383 by (auto simp add: split_ifs divmod_rel_def algebra_simps)
7.384
7.385 -lemma div_mult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)"
7.386 +lemma div_mult1_eq:
7.387 + "(a * b) div c = a * (b div c) + a * (b mod c) div (c::nat)"
7.388 apply (cases "c = 0", simp)
7.389 apply (blast intro: divmod_rel [THEN divmod_rel_mult1_eq, THEN div_eq])
7.390 done
7.391
7.392 lemma divmod_rel_add1_eq:
7.393 - "[| divmod_rel a c aq ar; divmod_rel b c bq br; c > 0 |]
7.394 - ==> divmod_rel (a + b) c (aq + bq + (ar+br) div c) ((ar + br) mod c)"
7.395 + "divmod_rel a c (aq, ar) \<Longrightarrow> divmod_rel b c (bq, br) \<Longrightarrow> c > 0
7.396 + \<Longrightarrow> divmod_rel (a + b) c (aq + bq + (ar + br) div c, (ar + br) mod c)"
7.397 by (auto simp add: split_ifs divmod_rel_def algebra_simps)
7.398
7.399 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
7.400 @@ -728,8 +766,9 @@
7.401 apply (simp add: add_mult_distrib2)
7.402 done
7.403
7.404 -lemma divmod_rel_mult2_eq: "[| divmod_rel a b q r; 0 < b; 0 < c |]
7.405 - ==> divmod_rel a (b*c) (q div c) (b*(q mod c) + r)"
7.406 +lemma divmod_rel_mult2_eq:
7.407 + "divmod_rel a b (q, r) \<Longrightarrow> 0 < b \<Longrightarrow> 0 < c
7.408 + \<Longrightarrow> divmod_rel a (b * c) (q div c, b *(q mod c) + r)"
7.409 by (auto simp add: mult_ac divmod_rel_def add_mult_distrib2 [symmetric] mod_lemma)
7.410
7.411 lemma div_mult2_eq: "a div (b*c) = (a div b) div (c::nat)"
7.412 @@ -745,23 +784,6 @@
7.413 done
7.414
7.415
7.416 -subsubsection{*Cancellation of Common Factors in Division*}
7.417 -
7.418 -lemma div_mult_mult_lemma:
7.419 - "[| (0::nat) < b; 0 < c |] ==> (c*a) div (c*b) = a div b"
7.420 -by (auto simp add: div_mult2_eq)
7.421 -
7.422 -lemma div_mult_mult1 [simp]: "(0::nat) < c ==> (c*a) div (c*b) = a div b"
7.423 - apply (cases "b = 0")
7.424 - apply (auto simp add: linorder_neq_iff [of b] div_mult_mult_lemma)
7.425 - done
7.426 -
7.427 -lemma div_mult_mult2 [simp]: "(0::nat) < c ==> (a*c) div (b*c) = a div b"
7.428 - apply (drule div_mult_mult1)
7.429 - apply (auto simp add: mult_commute)
7.430 - done
7.431 -
7.432 -
7.433 subsubsection{*Further Facts about Quotient and Remainder*}
7.434
7.435 lemma div_1 [simp]: "m div Suc 0 = m"
7.436 @@ -769,7 +791,7 @@
7.437
7.438
7.439 (* Monotonicity of div in first argument *)
7.440 -lemma div_le_mono [rule_format]:
7.441 +lemma div_le_mono [rule_format (no_asm)]:
7.442 "\<forall>m::nat. m \<le> n --> (m div k) \<le> (n div k)"
7.443 apply (case_tac "k=0", simp)
7.444 apply (induct "n" rule: nat_less_induct, clarify)
7.445 @@ -824,12 +846,6 @@
7.446 apply (simp_all)
7.447 done
7.448
7.449 -lemma nat_div_eq_0 [simp]: "(n::nat) > 0 ==> ((m div n) = 0) = (m < n)"
7.450 -by(auto, subst mod_div_equality [of m n, symmetric], auto)
7.451 -
7.452 -lemma nat_div_gt_0 [simp]: "(n::nat) > 0 ==> ((m div n) > 0) = (m >= n)"
7.453 -by (subst neq0_conv [symmetric], auto)
7.454 -
7.455 declare div_less_dividend [simp]
7.456
7.457 text{*A fact for the mutilated chess board*}
7.458 @@ -915,16 +931,10 @@
7.459 done
7.460
7.461 lemma dvd_imp_le: "[| k dvd n; 0 < n |] ==> k \<le> (n::nat)"
7.462 -by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
7.463 -
7.464 -lemma nat_dvd_not_less: "(0::nat) < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
7.465 -by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
7.466 + by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
7.467
7.468 lemma dvd_mult_div_cancel: "n dvd m ==> n * (m div n) = (m::nat)"
7.469 - apply (subgoal_tac "m mod n = 0")
7.470 - apply (simp add: mult_div_cancel)
7.471 - apply (simp only: dvd_eq_mod_eq_0)
7.472 - done
7.473 + by (simp add: dvd_eq_mod_eq_0 mult_div_cancel)
7.474
7.475 lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
7.476 by (induct n) auto
7.477 @@ -1001,9 +1011,11 @@
7.478 from A B show ?lhs ..
7.479 next
7.480 assume P: ?lhs
7.481 - then have "divmod_rel m n q (m - n * q)"
7.482 + then have "divmod_rel m n (q, m - n * q)"
7.483 unfolding divmod_rel_def by (auto simp add: mult_ac)
7.484 - then show ?rhs using divmod_rel by (rule divmod_rel_unique_div)
7.485 + with divmod_rel_unique divmod_rel [of m n]
7.486 + have "(q, m - n * q) = (m div n, m mod n)" by auto
7.487 + then show ?rhs by simp
7.488 qed
7.489
7.490 theorem split_div':
7.491 @@ -1155,4 +1167,9 @@
7.492 with j show ?thesis by blast
7.493 qed
7.494
7.495 +lemma nat_dvd_not_less:
7.496 + fixes m n :: nat
7.497 + shows "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
7.498 +by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
7.499 +
7.500 end
8.1 --- a/src/HOL/Groebner_Basis.thy Thu Apr 16 17:29:56 2009 +0200
8.2 +++ b/src/HOL/Groebner_Basis.thy Fri Apr 17 08:36:18 2009 +0200
8.3 @@ -5,7 +5,7 @@
8.4 header {* Semiring normalization and Groebner Bases *}
8.5
8.6 theory Groebner_Basis
8.7 -imports NatBin
8.8 +imports Nat_Numeral
8.9 uses
8.10 "Tools/Groebner_Basis/misc.ML"
8.11 "Tools/Groebner_Basis/normalizer_data.ML"
9.1 --- a/src/HOL/HOL.thy Thu Apr 16 17:29:56 2009 +0200
9.2 +++ b/src/HOL/HOL.thy Fri Apr 17 08:36:18 2009 +0200
9.3 @@ -5,7 +5,7 @@
9.4 header {* The basis of Higher-Order Logic *}
9.5
9.6 theory HOL
9.7 -imports Pure
9.8 +imports Pure "~~/src/Tools/Code_Generator"
9.9 uses
9.10 ("Tools/hologic.ML")
9.11 "~~/src/Tools/IsaPlanner/zipper.ML"
9.12 @@ -27,16 +27,6 @@
9.13 "~~/src/Tools/atomize_elim.ML"
9.14 "~~/src/Tools/induct.ML"
9.15 ("~~/src/Tools/induct_tacs.ML")
9.16 - "~~/src/Tools/value.ML"
9.17 - "~~/src/Tools/code/code_name.ML"
9.18 - "~~/src/Tools/code/code_funcgr.ML" (*formal dependency*)
9.19 - "~~/src/Tools/code/code_wellsorted.ML"
9.20 - "~~/src/Tools/code/code_thingol.ML"
9.21 - "~~/src/Tools/code/code_printer.ML"
9.22 - "~~/src/Tools/code/code_target.ML"
9.23 - "~~/src/Tools/code/code_ml.ML"
9.24 - "~~/src/Tools/code/code_haskell.ML"
9.25 - "~~/src/Tools/nbe.ML"
9.26 ("Tools/recfun_codegen.ML")
9.27 begin
9.28
9.29 @@ -1674,35 +1664,259 @@
9.30 *}
9.31
9.32
9.33 -subsection {* Code generator basics -- see further theory @{text "Code_Setup"} *}
9.34 +subsection {* Code generator setup *}
9.35
9.36 -text {* Equality *}
9.37 +subsubsection {* SML code generator setup *}
9.38 +
9.39 +use "Tools/recfun_codegen.ML"
9.40 +
9.41 +setup {*
9.42 + Codegen.setup
9.43 + #> RecfunCodegen.setup
9.44 +*}
9.45 +
9.46 +types_code
9.47 + "bool" ("bool")
9.48 +attach (term_of) {*
9.49 +fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
9.50 +*}
9.51 +attach (test) {*
9.52 +fun gen_bool i =
9.53 + let val b = one_of [false, true]
9.54 + in (b, fn () => term_of_bool b) end;
9.55 +*}
9.56 + "prop" ("bool")
9.57 +attach (term_of) {*
9.58 +fun term_of_prop b =
9.59 + HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);
9.60 +*}
9.61 +
9.62 +consts_code
9.63 + "Trueprop" ("(_)")
9.64 + "True" ("true")
9.65 + "False" ("false")
9.66 + "Not" ("Bool.not")
9.67 + "op |" ("(_ orelse/ _)")
9.68 + "op &" ("(_ andalso/ _)")
9.69 + "If" ("(if _/ then _/ else _)")
9.70 +
9.71 +setup {*
9.72 +let
9.73 +
9.74 +fun eq_codegen thy defs dep thyname b t gr =
9.75 + (case strip_comb t of
9.76 + (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
9.77 + | (Const ("op =", _), [t, u]) =>
9.78 + let
9.79 + val (pt, gr') = Codegen.invoke_codegen thy defs dep thyname false t gr;
9.80 + val (pu, gr'') = Codegen.invoke_codegen thy defs dep thyname false u gr';
9.81 + val (_, gr''') = Codegen.invoke_tycodegen thy defs dep thyname false HOLogic.boolT gr'';
9.82 + in
9.83 + SOME (Codegen.parens
9.84 + (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]), gr''')
9.85 + end
9.86 + | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
9.87 + thy defs dep thyname b (Codegen.eta_expand t ts 2) gr)
9.88 + | _ => NONE);
9.89 +
9.90 +in
9.91 + Codegen.add_codegen "eq_codegen" eq_codegen
9.92 +end
9.93 +*}
9.94 +
9.95 +subsubsection {* Equality *}
9.96
9.97 class eq =
9.98 fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
9.99 assumes eq_equals: "eq x y \<longleftrightarrow> x = y"
9.100 begin
9.101
9.102 -lemma eq: "eq = (op =)"
9.103 +lemma eq [code unfold, code inline del]: "eq = (op =)"
9.104 by (rule ext eq_equals)+
9.105
9.106 lemma eq_refl: "eq x x \<longleftrightarrow> True"
9.107 unfolding eq by rule+
9.108
9.109 +lemma equals_eq [code inline, code]: "(op =) \<equiv> eq"
9.110 + by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
9.111 +
9.112 +declare equals_eq [symmetric, code post]
9.113 +
9.114 end
9.115
9.116 -text {* Module setup *}
9.117 +subsubsection {* Generic code generator foundation *}
9.118
9.119 -use "Tools/recfun_codegen.ML"
9.120 +text {* Datatypes *}
9.121 +
9.122 +code_datatype True False
9.123 +
9.124 +code_datatype "TYPE('a\<Colon>{})"
9.125 +
9.126 +code_datatype Trueprop "prop"
9.127 +
9.128 +text {* Code equations *}
9.129 +
9.130 +lemma [code]:
9.131 + shows "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
9.132 + and "(False \<Longrightarrow> Q) \<equiv> Trueprop True"
9.133 + and "(PROP P \<Longrightarrow> True) \<equiv> Trueprop True"
9.134 + and "(Q \<Longrightarrow> False) \<equiv> Trueprop (\<not> Q)" by (auto intro!: equal_intr_rule)
9.135 +
9.136 +lemma [code]:
9.137 + shows "False \<and> x \<longleftrightarrow> False"
9.138 + and "True \<and> x \<longleftrightarrow> x"
9.139 + and "x \<and> False \<longleftrightarrow> False"
9.140 + and "x \<and> True \<longleftrightarrow> x" by simp_all
9.141 +
9.142 +lemma [code]:
9.143 + shows "False \<or> x \<longleftrightarrow> x"
9.144 + and "True \<or> x \<longleftrightarrow> True"
9.145 + and "x \<or> False \<longleftrightarrow> x"
9.146 + and "x \<or> True \<longleftrightarrow> True" by simp_all
9.147 +
9.148 +lemma [code]:
9.149 + shows "\<not> True \<longleftrightarrow> False"
9.150 + and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+
9.151 +
9.152 +lemmas [code] = Let_def if_True if_False
9.153 +
9.154 +lemmas [code, code unfold, symmetric, code post] = imp_conv_disj
9.155 +
9.156 +text {* Equality *}
9.157 +
9.158 +declare simp_thms(6) [code nbe]
9.159 +
9.160 +hide (open) const eq
9.161 +hide const eq
9.162
9.163 setup {*
9.164 - Code_ML.setup
9.165 - #> Code_Haskell.setup
9.166 - #> Nbe.setup
9.167 - #> Codegen.setup
9.168 - #> RecfunCodegen.setup
9.169 + Code_Unit.add_const_alias @{thm equals_eq}
9.170 *}
9.171
9.172 +text {* Cases *}
9.173 +
9.174 +lemma Let_case_cert:
9.175 + assumes "CASE \<equiv> (\<lambda>x. Let x f)"
9.176 + shows "CASE x \<equiv> f x"
9.177 + using assms by simp_all
9.178 +
9.179 +lemma If_case_cert:
9.180 + assumes "CASE \<equiv> (\<lambda>b. If b f g)"
9.181 + shows "(CASE True \<equiv> f) &&& (CASE False \<equiv> g)"
9.182 + using assms by simp_all
9.183 +
9.184 +setup {*
9.185 + Code.add_case @{thm Let_case_cert}
9.186 + #> Code.add_case @{thm If_case_cert}
9.187 + #> Code.add_undefined @{const_name undefined}
9.188 +*}
9.189 +
9.190 +code_abort undefined
9.191 +
9.192 +subsubsection {* Generic code generator preprocessor *}
9.193 +
9.194 +setup {*
9.195 + Code.map_pre (K HOL_basic_ss)
9.196 + #> Code.map_post (K HOL_basic_ss)
9.197 +*}
9.198 +
9.199 +subsubsection {* Generic code generator target languages *}
9.200 +
9.201 +text {* type bool *}
9.202 +
9.203 +code_type bool
9.204 + (SML "bool")
9.205 + (OCaml "bool")
9.206 + (Haskell "Bool")
9.207 +
9.208 +code_const True and False and Not and "op &" and "op |" and If
9.209 + (SML "true" and "false" and "not"
9.210 + and infixl 1 "andalso" and infixl 0 "orelse"
9.211 + and "!(if (_)/ then (_)/ else (_))")
9.212 + (OCaml "true" and "false" and "not"
9.213 + and infixl 4 "&&" and infixl 2 "||"
9.214 + and "!(if (_)/ then (_)/ else (_))")
9.215 + (Haskell "True" and "False" and "not"
9.216 + and infixl 3 "&&" and infixl 2 "||"
9.217 + and "!(if (_)/ then (_)/ else (_))")
9.218 +
9.219 +code_reserved SML
9.220 + bool true false not
9.221 +
9.222 +code_reserved OCaml
9.223 + bool not
9.224 +
9.225 +text {* using built-in Haskell equality *}
9.226 +
9.227 +code_class eq
9.228 + (Haskell "Eq")
9.229 +
9.230 +code_const "eq_class.eq"
9.231 + (Haskell infixl 4 "==")
9.232 +
9.233 +code_const "op ="
9.234 + (Haskell infixl 4 "==")
9.235 +
9.236 +text {* undefined *}
9.237 +
9.238 +code_const undefined
9.239 + (SML "!(raise/ Fail/ \"undefined\")")
9.240 + (OCaml "failwith/ \"undefined\"")
9.241 + (Haskell "error/ \"undefined\"")
9.242 +
9.243 +subsubsection {* Evaluation and normalization by evaluation *}
9.244 +
9.245 +setup {*
9.246 + Value.add_evaluator ("SML", Codegen.eval_term o ProofContext.theory_of)
9.247 +*}
9.248 +
9.249 +ML {*
9.250 +structure Eval_Method =
9.251 +struct
9.252 +
9.253 +val eval_ref : (unit -> bool) option ref = ref NONE;
9.254 +
9.255 +end;
9.256 +*}
9.257 +
9.258 +oracle eval_oracle = {* fn ct =>
9.259 + let
9.260 + val thy = Thm.theory_of_cterm ct;
9.261 + val t = Thm.term_of ct;
9.262 + val dummy = @{cprop True};
9.263 + in case try HOLogic.dest_Trueprop t
9.264 + of SOME t' => if Code_ML.eval_term
9.265 + ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy t' []
9.266 + then Thm.capply (Thm.capply @{cterm "op \<equiv> \<Colon> prop \<Rightarrow> prop \<Rightarrow> prop"} ct) dummy
9.267 + else dummy
9.268 + | NONE => dummy
9.269 + end
9.270 +*}
9.271 +
9.272 +ML {*
9.273 +fun gen_eval_method conv ctxt = SIMPLE_METHOD'
9.274 + (CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt)
9.275 + THEN' rtac TrueI)
9.276 +*}
9.277 +
9.278 +method_setup eval = {* Scan.succeed (gen_eval_method eval_oracle) *}
9.279 + "solve goal by evaluation"
9.280 +
9.281 +method_setup evaluation = {* Scan.succeed (gen_eval_method Codegen.evaluation_conv) *}
9.282 + "solve goal by evaluation"
9.283 +
9.284 +method_setup normalization = {*
9.285 + Scan.succeed (K (SIMPLE_METHOD' (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))))
9.286 +*} "solve goal by normalization"
9.287 +
9.288 +subsubsection {* Quickcheck *}
9.289 +
9.290 +setup {*
9.291 + Quickcheck.add_generator ("SML", Codegen.test_term)
9.292 +*}
9.293 +
9.294 +quickcheck_params [size = 5, iterations = 50]
9.295 +
9.296
9.297 subsection {* Nitpick hooks *}
9.298
10.1 --- a/src/HOL/Import/HOL/arithmetic.imp Thu Apr 16 17:29:56 2009 +0200
10.2 +++ b/src/HOL/Import/HOL/arithmetic.imp Fri Apr 17 08:36:18 2009 +0200
10.3 @@ -43,7 +43,7 @@
10.4 "TWO" > "HOL4Base.arithmetic.TWO"
10.5 "TIMES2" > "NatSimprocs.nat_mult_2"
10.6 "SUC_SUB1" > "HOL4Base.arithmetic.SUC_SUB1"
10.7 - "SUC_ONE_ADD" > "NatBin.Suc_eq_add_numeral_1_left"
10.8 + "SUC_ONE_ADD" > "Nat_Numeral.Suc_eq_add_numeral_1_left"
10.9 "SUC_NOT" > "Nat.nat.simps_2"
10.10 "SUC_ELIM_THM" > "HOL4Base.arithmetic.SUC_ELIM_THM"
10.11 "SUC_ADD_SYM" > "HOL4Base.arithmetic.SUC_ADD_SYM"
10.12 @@ -233,7 +233,7 @@
10.13 "EVEN_AND_ODD" > "HOL4Base.arithmetic.EVEN_AND_ODD"
10.14 "EVEN_ADD" > "HOL4Base.arithmetic.EVEN_ADD"
10.15 "EVEN" > "HOL4Base.arithmetic.EVEN"
10.16 - "EQ_MULT_LCANCEL" > "NatBin.nat_mult_eq_cancel_disj"
10.17 + "EQ_MULT_LCANCEL" > "Nat_Numeral.nat_mult_eq_cancel_disj"
10.18 "EQ_MONO_ADD_EQ" > "Nat.nat_add_right_cancel"
10.19 "EQ_LESS_EQ" > "Orderings.order_eq_iff"
10.20 "EQ_ADD_RCANCEL" > "Nat.nat_add_right_cancel"
11.1 --- a/src/HOL/Import/HOL/real.imp Thu Apr 16 17:29:56 2009 +0200
11.2 +++ b/src/HOL/Import/HOL/real.imp Fri Apr 17 08:36:18 2009 +0200
11.3 @@ -99,7 +99,7 @@
11.4 "REAL_POW_INV" > "Power.power_inverse"
11.5 "REAL_POW_DIV" > "Power.power_divide"
11.6 "REAL_POW_ADD" > "Power.power_add"
11.7 - "REAL_POW2_ABS" > "NatBin.power2_abs"
11.8 + "REAL_POW2_ABS" > "Nat_Numeral.power2_abs"
11.9 "REAL_POS_NZ" > "HOL4Real.real.REAL_POS_NZ"
11.10 "REAL_POS" > "RealDef.real_of_nat_ge_zero"
11.11 "REAL_POASQ" > "HOL4Real.real.REAL_POASQ"
11.12 @@ -210,7 +210,7 @@
11.13 "REAL_LE_RDIV_EQ" > "Ring_and_Field.pos_le_divide_eq"
11.14 "REAL_LE_RDIV" > "Ring_and_Field.mult_imp_le_div_pos"
11.15 "REAL_LE_RADD" > "OrderedGroup.add_le_cancel_right"
11.16 - "REAL_LE_POW2" > "NatBin.zero_compare_simps_12"
11.17 + "REAL_LE_POW2" > "Nat_Numeral.zero_compare_simps_12"
11.18 "REAL_LE_NEGTOTAL" > "HOL4Real.real.REAL_LE_NEGTOTAL"
11.19 "REAL_LE_NEGR" > "OrderedGroup.le_minus_self_iff"
11.20 "REAL_LE_NEGL" > "OrderedGroup.minus_le_self_iff"
11.21 @@ -313,7 +313,7 @@
11.22 "POW_ONE" > "Power.power_one"
11.23 "POW_NZ" > "Power.field_power_not_zero"
11.24 "POW_MUL" > "Power.power_mult_distrib"
11.25 - "POW_MINUS1" > "NatBin.power_minus1_even"
11.26 + "POW_MINUS1" > "Nat_Numeral.power_minus1_even"
11.27 "POW_M1" > "HOL4Real.real.POW_M1"
11.28 "POW_LT" > "HOL4Real.real.POW_LT"
11.29 "POW_LE" > "Power.power_mono"
11.30 @@ -323,7 +323,7 @@
11.31 "POW_ABS" > "Power.power_abs"
11.32 "POW_2_LT" > "RealPow.two_realpow_gt"
11.33 "POW_2_LE1" > "RealPow.two_realpow_ge_one"
11.34 - "POW_2" > "NatBin.power2_eq_square"
11.35 + "POW_2" > "Nat_Numeral.power2_eq_square"
11.36 "POW_1" > "Power.power_one_right"
11.37 "POW_0" > "Power.power_0_Suc"
11.38 "ABS_ZERO" > "OrderedGroup.abs_eq_0"
11.39 @@ -335,7 +335,7 @@
11.40 "ABS_SIGN2" > "HOL4Real.real.ABS_SIGN2"
11.41 "ABS_SIGN" > "HOL4Real.real.ABS_SIGN"
11.42 "ABS_REFL" > "HOL4Real.real.ABS_REFL"
11.43 - "ABS_POW2" > "NatBin.abs_power2"
11.44 + "ABS_POW2" > "Nat_Numeral.abs_power2"
11.45 "ABS_POS" > "OrderedGroup.abs_ge_zero"
11.46 "ABS_NZ" > "OrderedGroup.zero_less_abs_iff"
11.47 "ABS_NEG" > "OrderedGroup.abs_minus_cancel"
12.1 --- a/src/HOL/Import/HOLLight/hollight.imp Thu Apr 16 17:29:56 2009 +0200
12.2 +++ b/src/HOL/Import/HOLLight/hollight.imp Fri Apr 17 08:36:18 2009 +0200
12.3 @@ -1515,7 +1515,7 @@
12.4 "EQ_REFL_T" > "HOL.simp_thms_6"
12.5 "EQ_REFL" > "Presburger.fm_modd_pinf"
12.6 "EQ_MULT_RCANCEL" > "Nat.mult_cancel2"
12.7 - "EQ_MULT_LCANCEL" > "NatBin.nat_mult_eq_cancel_disj"
12.8 + "EQ_MULT_LCANCEL" > "Nat_Numeral.nat_mult_eq_cancel_disj"
12.9 "EQ_IMP_LE" > "HOLLight.hollight.EQ_IMP_LE"
12.10 "EQ_EXT" > "HOL.meta_eq_to_obj_eq"
12.11 "EQ_CLAUSES" > "HOLLight.hollight.EQ_CLAUSES"
13.1 --- a/src/HOL/IntDiv.thy Thu Apr 16 17:29:56 2009 +0200
13.2 +++ b/src/HOL/IntDiv.thy Fri Apr 17 08:36:18 2009 +0200
13.3 @@ -249,33 +249,33 @@
13.4 text {* Tool setup *}
13.5
13.6 ML {*
13.7 -local
13.8 +local
13.9
13.10 -structure CancelDivMod = CancelDivModFun(
13.11 -struct
13.12 - val div_name = @{const_name Divides.div};
13.13 - val mod_name = @{const_name Divides.mod};
13.14 +structure CancelDivMod = CancelDivModFun(struct
13.15 +
13.16 + val div_name = @{const_name div};
13.17 + val mod_name = @{const_name mod};
13.18 val mk_binop = HOLogic.mk_binop;
13.19 val mk_sum = Int_Numeral_Simprocs.mk_sum HOLogic.intT;
13.20 val dest_sum = Int_Numeral_Simprocs.dest_sum;
13.21 - val div_mod_eqs =
13.22 - map mk_meta_eq [@{thm zdiv_zmod_equality},
13.23 - @{thm zdiv_zmod_equality2}];
13.24 +
13.25 + val div_mod_eqs = map mk_meta_eq [@{thm zdiv_zmod_equality}, @{thm zdiv_zmod_equality2}];
13.26 +
13.27 val trans = trans;
13.28 - val prove_eq_sums =
13.29 - let
13.30 - val simps = @{thm diff_int_def} :: Int_Numeral_Simprocs.add_0s @ @{thms zadd_ac}
13.31 - in Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac simps) end;
13.32 +
13.33 + val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
13.34 + (@{thm diff_minus} :: @{thms add_0s} @ @{thms add_ac}))
13.35 +
13.36 end)
13.37
13.38 in
13.39
13.40 -val cancel_zdiv_zmod_proc = Simplifier.simproc (the_context ())
13.41 - "cancel_zdiv_zmod" ["(m::int) + n"] (K CancelDivMod.proc)
13.42 +val cancel_div_mod_int_proc = Simplifier.simproc (the_context ())
13.43 + "cancel_zdiv_zmod" ["(k::int) + l"] (K CancelDivMod.proc);
13.44
13.45 -end;
13.46 +val _ = Addsimprocs [cancel_div_mod_int_proc];
13.47
13.48 -Addsimprocs [cancel_zdiv_zmod_proc]
13.49 +end
13.50 *}
13.51
13.52 lemma pos_mod_conj : "(0::int) < b ==> 0 \<le> a mod b & a mod b < b"
13.53 @@ -711,6 +711,26 @@
13.54 show "(a + c * b) div b = c + a div b"
13.55 unfolding zdiv_zadd1_eq [of a "c * b"] using not0
13.56 by (simp add: zmod_zmult1_eq zmod_zdiv_trivial zdiv_zmult1_eq)
13.57 +next
13.58 + fix a b c :: int
13.59 + assume "a \<noteq> 0"
13.60 + then show "(a * b) div (a * c) = b div c"
13.61 + proof (cases "b \<noteq> 0 \<and> c \<noteq> 0")
13.62 + case False then show ?thesis by auto
13.63 + next
13.64 + case True then have "b \<noteq> 0" and "c \<noteq> 0" by auto
13.65 + with `a \<noteq> 0`
13.66 + have "\<And>q r. divmod_rel b c (q, r) \<Longrightarrow> divmod_rel (a * b) (a * c) (q, a * r)"
13.67 + apply (auto simp add: divmod_rel_def)
13.68 + apply (auto simp add: algebra_simps)
13.69 + apply (auto simp add: zero_less_mult_iff zero_le_mult_iff mult_le_0_iff)
13.70 + apply (simp_all add: mult_less_cancel_left_disj mult_commute [of _ a])
13.71 + done
13.72 + moreover with `c \<noteq> 0` divmod_rel_div_mod have "divmod_rel b c (b div c, b mod c)" by auto
13.73 + ultimately have "divmod_rel (a * b) (a * c) (b div c, a * (b mod c))" .
13.74 + moreover from `a \<noteq> 0` `c \<noteq> 0` have "a * c \<noteq> 0" by simp
13.75 + ultimately show ?thesis by (rule divmod_rel_div)
13.76 + qed
13.77 qed auto
13.78
13.79 lemma posDivAlg_div_mod:
13.80 @@ -808,52 +828,6 @@
13.81 done
13.82
13.83
13.84 -subsection{*Cancellation of Common Factors in div*}
13.85 -
13.86 -lemma zdiv_zmult_zmult1_aux1:
13.87 - "[| (0::int) < b; c \<noteq> 0 |] ==> (c*a) div (c*b) = a div b"
13.88 -by (subst zdiv_zmult2_eq, auto)
13.89 -
13.90 -lemma zdiv_zmult_zmult1_aux2:
13.91 - "[| b < (0::int); c \<noteq> 0 |] ==> (c*a) div (c*b) = a div b"
13.92 -apply (subgoal_tac " (c * (-a)) div (c * (-b)) = (-a) div (-b) ")
13.93 -apply (rule_tac [2] zdiv_zmult_zmult1_aux1, auto)
13.94 -done
13.95 -
13.96 -lemma zdiv_zmult_zmult1: "c \<noteq> (0::int) ==> (c*a) div (c*b) = a div b"
13.97 -apply (case_tac "b = 0", simp)
13.98 -apply (auto simp add: linorder_neq_iff zdiv_zmult_zmult1_aux1 zdiv_zmult_zmult1_aux2)
13.99 -done
13.100 -
13.101 -lemma zdiv_zmult_zmult1_if[simp]:
13.102 - "(k*m) div (k*n) = (if k = (0::int) then 0 else m div n)"
13.103 -by (simp add:zdiv_zmult_zmult1)
13.104 -
13.105 -
13.106 -subsection{*Distribution of Factors over mod*}
13.107 -
13.108 -lemma zmod_zmult_zmult1_aux1:
13.109 - "[| (0::int) < b; c \<noteq> 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"
13.110 -by (subst zmod_zmult2_eq, auto)
13.111 -
13.112 -lemma zmod_zmult_zmult1_aux2:
13.113 - "[| b < (0::int); c \<noteq> 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"
13.114 -apply (subgoal_tac " (c * (-a)) mod (c * (-b)) = c * ((-a) mod (-b))")
13.115 -apply (rule_tac [2] zmod_zmult_zmult1_aux1, auto)
13.116 -done
13.117 -
13.118 -lemma zmod_zmult_zmult1: "(c*a) mod (c*b) = (c::int) * (a mod b)"
13.119 -apply (case_tac "b = 0", simp)
13.120 -apply (case_tac "c = 0", simp)
13.121 -apply (auto simp add: linorder_neq_iff zmod_zmult_zmult1_aux1 zmod_zmult_zmult1_aux2)
13.122 -done
13.123 -
13.124 -lemma zmod_zmult_zmult2: "(a*c) mod (b*c) = (a mod b) * (c::int)"
13.125 -apply (cut_tac c = c in zmod_zmult_zmult1)
13.126 -apply (auto simp add: mult_commute)
13.127 -done
13.128 -
13.129 -
13.130 subsection {*Splitting Rules for div and mod*}
13.131
13.132 text{*The proofs of the two lemmas below are essentially identical*}
13.133 @@ -937,7 +911,7 @@
13.134 right_distrib)
13.135 thus ?thesis
13.136 by (subst zdiv_zadd1_eq,
13.137 - simp add: zdiv_zmult_zmult1 zmod_zmult_zmult1 one_less_a2
13.138 + simp add: mod_mult_mult1 one_less_a2
13.139 div_pos_pos_trivial)
13.140 qed
13.141
13.142 @@ -961,7 +935,7 @@
13.143 then number_of v div (number_of w)
13.144 else (number_of v + (1::int)) div (number_of w))"
13.145 apply (simp only: number_of_eq numeral_simps UNIV_I split: split_if)
13.146 -apply (simp add: zdiv_zmult_zmult1 pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac)
13.147 +apply (simp add: pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac)
13.148 done
13.149
13.150
13.151 @@ -977,7 +951,7 @@
13.152 apply (auto simp add: add_commute [of 1] mult_commute add1_zle_eq
13.153 pos_mod_bound)
13.154 apply (subst mod_add_eq)
13.155 -apply (simp add: zmod_zmult_zmult2 mod_pos_pos_trivial)
13.156 +apply (simp add: mod_mult_mult2 mod_pos_pos_trivial)
13.157 apply (rule mod_pos_pos_trivial)
13.158 apply (auto simp add: mod_pos_pos_trivial ring_distribs)
13.159 apply (subgoal_tac "0 \<le> b mod a", arith, simp)
13.160 @@ -998,7 +972,7 @@
13.161 "number_of (Int.Bit0 v) mod number_of (Int.Bit0 w) =
13.162 (2::int) * (number_of v mod number_of w)"
13.163 apply (simp only: number_of_eq numeral_simps)
13.164 -apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2
13.165 +apply (simp add: mod_mult_mult1 pos_zmod_mult_2
13.166 neg_zmod_mult_2 add_ac)
13.167 done
13.168
13.169 @@ -1008,7 +982,7 @@
13.170 then 2 * (number_of v mod number_of w) + 1
13.171 else 2 * ((number_of v + (1::int)) mod number_of w) - 1)"
13.172 apply (simp only: number_of_eq numeral_simps)
13.173 -apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2
13.174 +apply (simp add: mod_mult_mult1 pos_zmod_mult_2
13.175 neg_zmod_mult_2 add_ac)
13.176 done
13.177
13.178 @@ -1090,9 +1064,7 @@
13.179 done
13.180
13.181 lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
13.182 - apply (simp add: dvd_def)
13.183 - apply (auto simp add: zmod_zmult_zmult1)
13.184 - done
13.185 + by (auto elim!: dvdE simp add: mod_mult_mult1)
13.186
13.187 lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
13.188 apply (subgoal_tac "k dvd n * (m div n) + m mod n")
13.189 @@ -1247,9 +1219,9 @@
13.190 lemmas zmod_simps =
13.191 mod_add_left_eq [symmetric]
13.192 mod_add_right_eq [symmetric]
13.193 - IntDiv.zmod_zmult1_eq [symmetric]
13.194 - mod_mult_left_eq [symmetric]
13.195 - IntDiv.zpower_zmod
13.196 + zmod_zmult1_eq [symmetric]
13.197 + mod_mult_left_eq [symmetric]
13.198 + zpower_zmod
13.199 zminus_zmod zdiff_zmod_left zdiff_zmod_right
13.200
13.201 text {* Distributive laws for function @{text nat}. *}
14.1 --- a/src/HOL/IsaMakefile Thu Apr 16 17:29:56 2009 +0200
14.2 +++ b/src/HOL/IsaMakefile Fri Apr 17 08:36:18 2009 +0200
14.3 @@ -89,7 +89,6 @@
14.4 $(SRC)/Tools/IsaPlanner/rw_tools.ML \
14.5 $(SRC)/Tools/IsaPlanner/zipper.ML \
14.6 $(SRC)/Tools/atomize_elim.ML \
14.7 - $(SRC)/Tools/code/code_funcgr.ML \
14.8 $(SRC)/Tools/code/code_haskell.ML \
14.9 $(SRC)/Tools/code/code_ml.ML \
14.10 $(SRC)/Tools/code/code_name.ML \
14.11 @@ -106,7 +105,7 @@
14.12 $(SRC)/Tools/project_rule.ML \
14.13 $(SRC)/Tools/random_word.ML \
14.14 $(SRC)/Tools/value.ML \
14.15 - Code_Setup.thy \
14.16 + $(SRC)/Tools/Code_Generator.thy \
14.17 HOL.thy \
14.18 Tools/hologic.ML \
14.19 Tools/recfun_codegen.ML \
14.20 @@ -216,7 +215,7 @@
14.21 List.thy \
14.22 Main.thy \
14.23 Map.thy \
14.24 - NatBin.thy \
14.25 + Nat_Numeral.thy \
14.26 Presburger.thy \
14.27 Recdef.thy \
14.28 Relation_Power.thy \
15.1 --- a/src/HOL/Library/Code_Index.thy Thu Apr 16 17:29:56 2009 +0200
15.2 +++ b/src/HOL/Library/Code_Index.thy Fri Apr 17 08:36:18 2009 +0200
15.3 @@ -144,7 +144,7 @@
15.4
15.5 subsection {* Basic arithmetic *}
15.6
15.7 -instantiation index :: "{minus, ordered_semidom, Divides.div, linorder}"
15.8 +instantiation index :: "{minus, ordered_semidom, semiring_div, linorder}"
15.9 begin
15.10
15.11 definition [simp, code del]:
15.12 @@ -172,7 +172,7 @@
15.13 "n < m \<longleftrightarrow> nat_of n < nat_of m"
15.14
15.15 instance proof
15.16 -qed (auto simp add: left_distrib)
15.17 +qed (auto simp add: index left_distrib div_mult_self1)
15.18
15.19 end
15.20
16.1 --- a/src/HOL/Library/Polynomial.thy Thu Apr 16 17:29:56 2009 +0200
16.2 +++ b/src/HOL/Library/Polynomial.thy Fri Apr 17 08:36:18 2009 +0200
16.3 @@ -987,6 +987,30 @@
16.4 by (simp add: pdivmod_rel_def left_distrib)
16.5 thus "(x + z * y) div y = z + x div y"
16.6 by (rule div_poly_eq)
16.7 +next
16.8 + fix x y z :: "'a poly"
16.9 + assume "x \<noteq> 0"
16.10 + show "(x * y) div (x * z) = y div z"
16.11 + proof (cases "y \<noteq> 0 \<and> z \<noteq> 0")
16.12 + have "\<And>x::'a poly. pdivmod_rel x 0 0 x"
16.13 + by (rule pdivmod_rel_by_0)
16.14 + then have [simp]: "\<And>x::'a poly. x div 0 = 0"
16.15 + by (rule div_poly_eq)
16.16 + have "\<And>x::'a poly. pdivmod_rel 0 x 0 0"
16.17 + by (rule pdivmod_rel_0)
16.18 + then have [simp]: "\<And>x::'a poly. 0 div x = 0"
16.19 + by (rule div_poly_eq)
16.20 + case False then show ?thesis by auto
16.21 + next
16.22 + case True then have "y \<noteq> 0" and "z \<noteq> 0" by auto
16.23 + with `x \<noteq> 0`
16.24 + have "\<And>q r. pdivmod_rel y z q r \<Longrightarrow> pdivmod_rel (x * y) (x * z) q (x * r)"
16.25 + by (auto simp add: pdivmod_rel_def algebra_simps)
16.26 + (rule classical, simp add: degree_mult_eq)
16.27 + moreover from pdivmod_rel have "pdivmod_rel y z (y div z) (y mod z)" .
16.28 + ultimately have "pdivmod_rel (x * y) (x * z) (y div z) (x * (y mod z))" .
16.29 + then show ?thesis by (simp add: div_poly_eq)
16.30 + qed
16.31 qed
16.32
16.33 end
17.1 --- a/src/HOL/Map.thy Thu Apr 16 17:29:56 2009 +0200
17.2 +++ b/src/HOL/Map.thy Fri Apr 17 08:36:18 2009 +0200
17.3 @@ -11,7 +11,7 @@
17.4 imports List
17.5 begin
17.6
17.7 -types ('a,'b) "~=>" = "'a => 'b option" (infixr 0)
17.8 +types ('a,'b) "~=>" = "'a => 'b option" (infixr "~=>" 0)
17.9 translations (type) "a ~=> b " <= (type) "a => b option"
17.10
17.11 syntax (xsymbols)
18.1 --- a/src/HOL/NatBin.thy Thu Apr 16 17:29:56 2009 +0200
18.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
18.3 @@ -1,975 +0,0 @@
18.4 -(* Title: HOL/NatBin.thy
18.5 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
18.6 - Copyright 1999 University of Cambridge
18.7 -*)
18.8 -
18.9 -header {* Binary arithmetic for the natural numbers *}
18.10 -
18.11 -theory NatBin
18.12 -imports IntDiv
18.13 -uses ("Tools/nat_simprocs.ML")
18.14 -begin
18.15 -
18.16 -text {*
18.17 - Arithmetic for naturals is reduced to that for the non-negative integers.
18.18 -*}
18.19 -
18.20 -instantiation nat :: number
18.21 -begin
18.22 -
18.23 -definition
18.24 - nat_number_of_def [code inline, code del]: "number_of v = nat (number_of v)"
18.25 -
18.26 -instance ..
18.27 -
18.28 -end
18.29 -
18.30 -lemma [code post]:
18.31 - "nat (number_of v) = number_of v"
18.32 - unfolding nat_number_of_def ..
18.33 -
18.34 -abbreviation (xsymbols)
18.35 - power2 :: "'a::power => 'a" ("(_\<twosuperior>)" [1000] 999) where
18.36 - "x\<twosuperior> == x^2"
18.37 -
18.38 -notation (latex output)
18.39 - power2 ("(_\<twosuperior>)" [1000] 999)
18.40 -
18.41 -notation (HTML output)
18.42 - power2 ("(_\<twosuperior>)" [1000] 999)
18.43 -
18.44 -
18.45 -subsection {* Predicate for negative binary numbers *}
18.46 -
18.47 -definition neg :: "int \<Rightarrow> bool" where
18.48 - "neg Z \<longleftrightarrow> Z < 0"
18.49 -
18.50 -lemma not_neg_int [simp]: "~ neg (of_nat n)"
18.51 -by (simp add: neg_def)
18.52 -
18.53 -lemma neg_zminus_int [simp]: "neg (- (of_nat (Suc n)))"
18.54 -by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc)
18.55 -
18.56 -lemmas neg_eq_less_0 = neg_def
18.57 -
18.58 -lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)"
18.59 -by (simp add: neg_def linorder_not_less)
18.60 -
18.61 -text{*To simplify inequalities when Numeral1 can get simplified to 1*}
18.62 -
18.63 -lemma not_neg_0: "~ neg 0"
18.64 -by (simp add: One_int_def neg_def)
18.65 -
18.66 -lemma not_neg_1: "~ neg 1"
18.67 -by (simp add: neg_def linorder_not_less zero_le_one)
18.68 -
18.69 -lemma neg_nat: "neg z ==> nat z = 0"
18.70 -by (simp add: neg_def order_less_imp_le)
18.71 -
18.72 -lemma not_neg_nat: "~ neg z ==> of_nat (nat z) = z"
18.73 -by (simp add: linorder_not_less neg_def)
18.74 -
18.75 -text {*
18.76 - If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
18.77 - @{term Numeral0} IS @{term "number_of Pls"}
18.78 -*}
18.79 -
18.80 -lemma not_neg_number_of_Pls: "~ neg (number_of Int.Pls)"
18.81 - by (simp add: neg_def)
18.82 -
18.83 -lemma neg_number_of_Min: "neg (number_of Int.Min)"
18.84 - by (simp add: neg_def)
18.85 -
18.86 -lemma neg_number_of_Bit0:
18.87 - "neg (number_of (Int.Bit0 w)) = neg (number_of w)"
18.88 - by (simp add: neg_def)
18.89 -
18.90 -lemma neg_number_of_Bit1:
18.91 - "neg (number_of (Int.Bit1 w)) = neg (number_of w)"
18.92 - by (simp add: neg_def)
18.93 -
18.94 -lemmas neg_simps [simp] =
18.95 - not_neg_0 not_neg_1
18.96 - not_neg_number_of_Pls neg_number_of_Min
18.97 - neg_number_of_Bit0 neg_number_of_Bit1
18.98 -
18.99 -
18.100 -subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*}
18.101 -
18.102 -declare nat_0 [simp] nat_1 [simp]
18.103 -
18.104 -lemma nat_number_of [simp]: "nat (number_of w) = number_of w"
18.105 -by (simp add: nat_number_of_def)
18.106 -
18.107 -lemma nat_numeral_0_eq_0 [simp]: "Numeral0 = (0::nat)"
18.108 -by (simp add: nat_number_of_def)
18.109 -
18.110 -lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)"
18.111 -by (simp add: nat_1 nat_number_of_def)
18.112 -
18.113 -lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
18.114 -by (simp add: nat_numeral_1_eq_1)
18.115 -
18.116 -lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
18.117 -apply (unfold nat_number_of_def)
18.118 -apply (rule nat_2)
18.119 -done
18.120 -
18.121 -
18.122 -subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
18.123 -
18.124 -lemma int_nat_number_of [simp]:
18.125 - "int (number_of v) =
18.126 - (if neg (number_of v :: int) then 0
18.127 - else (number_of v :: int))"
18.128 - unfolding nat_number_of_def number_of_is_id neg_def
18.129 - by simp
18.130 -
18.131 -
18.132 -subsubsection{*Successor *}
18.133 -
18.134 -lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
18.135 -apply (rule sym)
18.136 -apply (simp add: nat_eq_iff int_Suc)
18.137 -done
18.138 -
18.139 -lemma Suc_nat_number_of_add:
18.140 - "Suc (number_of v + n) =
18.141 - (if neg (number_of v :: int) then 1+n else number_of (Int.succ v) + n)"
18.142 - unfolding nat_number_of_def number_of_is_id neg_def numeral_simps
18.143 - by (simp add: Suc_nat_eq_nat_zadd1 add_ac)
18.144 -
18.145 -lemma Suc_nat_number_of [simp]:
18.146 - "Suc (number_of v) =
18.147 - (if neg (number_of v :: int) then 1 else number_of (Int.succ v))"
18.148 -apply (cut_tac n = 0 in Suc_nat_number_of_add)
18.149 -apply (simp cong del: if_weak_cong)
18.150 -done
18.151 -
18.152 -
18.153 -subsubsection{*Addition *}
18.154 -
18.155 -lemma add_nat_number_of [simp]:
18.156 - "(number_of v :: nat) + number_of v' =
18.157 - (if v < Int.Pls then number_of v'
18.158 - else if v' < Int.Pls then number_of v
18.159 - else number_of (v + v'))"
18.160 - unfolding nat_number_of_def number_of_is_id numeral_simps
18.161 - by (simp add: nat_add_distrib)
18.162 -
18.163 -lemma nat_number_of_add_1 [simp]:
18.164 - "number_of v + (1::nat) =
18.165 - (if v < Int.Pls then 1 else number_of (Int.succ v))"
18.166 - unfolding nat_number_of_def number_of_is_id numeral_simps
18.167 - by (simp add: nat_add_distrib)
18.168 -
18.169 -lemma nat_1_add_number_of [simp]:
18.170 - "(1::nat) + number_of v =
18.171 - (if v < Int.Pls then 1 else number_of (Int.succ v))"
18.172 - unfolding nat_number_of_def number_of_is_id numeral_simps
18.173 - by (simp add: nat_add_distrib)
18.174 -
18.175 -lemma nat_1_add_1 [simp]: "1 + 1 = (2::nat)"
18.176 - by (rule int_int_eq [THEN iffD1]) simp
18.177 -
18.178 -
18.179 -subsubsection{*Subtraction *}
18.180 -
18.181 -lemma diff_nat_eq_if:
18.182 - "nat z - nat z' =
18.183 - (if neg z' then nat z
18.184 - else let d = z-z' in
18.185 - if neg d then 0 else nat d)"
18.186 -by (simp add: Let_def nat_diff_distrib [symmetric] neg_eq_less_0 not_neg_eq_ge_0)
18.187 -
18.188 -
18.189 -lemma diff_nat_number_of [simp]:
18.190 - "(number_of v :: nat) - number_of v' =
18.191 - (if v' < Int.Pls then number_of v
18.192 - else let d = number_of (v + uminus v') in
18.193 - if neg d then 0 else nat d)"
18.194 - unfolding nat_number_of_def number_of_is_id numeral_simps neg_def
18.195 - by auto
18.196 -
18.197 -lemma nat_number_of_diff_1 [simp]:
18.198 - "number_of v - (1::nat) =
18.199 - (if v \<le> Int.Pls then 0 else number_of (Int.pred v))"
18.200 - unfolding nat_number_of_def number_of_is_id numeral_simps
18.201 - by auto
18.202 -
18.203 -
18.204 -subsubsection{*Multiplication *}
18.205 -
18.206 -lemma mult_nat_number_of [simp]:
18.207 - "(number_of v :: nat) * number_of v' =
18.208 - (if v < Int.Pls then 0 else number_of (v * v'))"
18.209 - unfolding nat_number_of_def number_of_is_id numeral_simps
18.210 - by (simp add: nat_mult_distrib)
18.211 -
18.212 -
18.213 -subsubsection{*Quotient *}
18.214 -
18.215 -lemma div_nat_number_of [simp]:
18.216 - "(number_of v :: nat) div number_of v' =
18.217 - (if neg (number_of v :: int) then 0
18.218 - else nat (number_of v div number_of v'))"
18.219 - unfolding nat_number_of_def number_of_is_id neg_def
18.220 - by (simp add: nat_div_distrib)
18.221 -
18.222 -lemma one_div_nat_number_of [simp]:
18.223 - "Suc 0 div number_of v' = nat (1 div number_of v')"
18.224 -by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric])
18.225 -
18.226 -
18.227 -subsubsection{*Remainder *}
18.228 -
18.229 -lemma mod_nat_number_of [simp]:
18.230 - "(number_of v :: nat) mod number_of v' =
18.231 - (if neg (number_of v :: int) then 0
18.232 - else if neg (number_of v' :: int) then number_of v
18.233 - else nat (number_of v mod number_of v'))"
18.234 - unfolding nat_number_of_def number_of_is_id neg_def
18.235 - by (simp add: nat_mod_distrib)
18.236 -
18.237 -lemma one_mod_nat_number_of [simp]:
18.238 - "Suc 0 mod number_of v' =
18.239 - (if neg (number_of v' :: int) then Suc 0
18.240 - else nat (1 mod number_of v'))"
18.241 -by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric])
18.242 -
18.243 -
18.244 -subsubsection{* Divisibility *}
18.245 -
18.246 -lemmas dvd_eq_mod_eq_0_number_of =
18.247 - dvd_eq_mod_eq_0 [of "number_of x" "number_of y", standard]
18.248 -
18.249 -declare dvd_eq_mod_eq_0_number_of [simp]
18.250 -
18.251 -ML
18.252 -{*
18.253 -val nat_number_of_def = thm"nat_number_of_def";
18.254 -
18.255 -val nat_number_of = thm"nat_number_of";
18.256 -val nat_numeral_0_eq_0 = thm"nat_numeral_0_eq_0";
18.257 -val nat_numeral_1_eq_1 = thm"nat_numeral_1_eq_1";
18.258 -val numeral_1_eq_Suc_0 = thm"numeral_1_eq_Suc_0";
18.259 -val numeral_2_eq_2 = thm"numeral_2_eq_2";
18.260 -val nat_div_distrib = thm"nat_div_distrib";
18.261 -val nat_mod_distrib = thm"nat_mod_distrib";
18.262 -val int_nat_number_of = thm"int_nat_number_of";
18.263 -val Suc_nat_eq_nat_zadd1 = thm"Suc_nat_eq_nat_zadd1";
18.264 -val Suc_nat_number_of_add = thm"Suc_nat_number_of_add";
18.265 -val Suc_nat_number_of = thm"Suc_nat_number_of";
18.266 -val add_nat_number_of = thm"add_nat_number_of";
18.267 -val diff_nat_eq_if = thm"diff_nat_eq_if";
18.268 -val diff_nat_number_of = thm"diff_nat_number_of";
18.269 -val mult_nat_number_of = thm"mult_nat_number_of";
18.270 -val div_nat_number_of = thm"div_nat_number_of";
18.271 -val mod_nat_number_of = thm"mod_nat_number_of";
18.272 -*}
18.273 -
18.274 -
18.275 -subsection{*Comparisons*}
18.276 -
18.277 -subsubsection{*Equals (=) *}
18.278 -
18.279 -lemma eq_nat_nat_iff:
18.280 - "[| (0::int) <= z; 0 <= z' |] ==> (nat z = nat z') = (z=z')"
18.281 -by (auto elim!: nonneg_eq_int)
18.282 -
18.283 -lemma eq_nat_number_of [simp]:
18.284 - "((number_of v :: nat) = number_of v') =
18.285 - (if neg (number_of v :: int) then (number_of v' :: int) \<le> 0
18.286 - else if neg (number_of v' :: int) then (number_of v :: int) = 0
18.287 - else v = v')"
18.288 - unfolding nat_number_of_def number_of_is_id neg_def
18.289 - by auto
18.290 -
18.291 -
18.292 -subsubsection{*Less-than (<) *}
18.293 -
18.294 -lemma less_nat_number_of [simp]:
18.295 - "(number_of v :: nat) < number_of v' \<longleftrightarrow>
18.296 - (if v < v' then Int.Pls < v' else False)"
18.297 - unfolding nat_number_of_def number_of_is_id numeral_simps
18.298 - by auto
18.299 -
18.300 -
18.301 -subsubsection{*Less-than-or-equal *}
18.302 -
18.303 -lemma le_nat_number_of [simp]:
18.304 - "(number_of v :: nat) \<le> number_of v' \<longleftrightarrow>
18.305 - (if v \<le> v' then True else v \<le> Int.Pls)"
18.306 - unfolding nat_number_of_def number_of_is_id numeral_simps
18.307 - by auto
18.308 -
18.309 -(*Maps #n to n for n = 0, 1, 2*)
18.310 -lemmas numerals = nat_numeral_0_eq_0 nat_numeral_1_eq_1 numeral_2_eq_2
18.311 -
18.312 -
18.313 -subsection{*Powers with Numeric Exponents*}
18.314 -
18.315 -text{*We cannot refer to the number @{term 2} in @{text Ring_and_Field.thy}.
18.316 -We cannot prove general results about the numeral @{term "-1"}, so we have to
18.317 -use @{term "- 1"} instead.*}
18.318 -
18.319 -lemma power2_eq_square: "(a::'a::recpower)\<twosuperior> = a * a"
18.320 - by (simp add: numeral_2_eq_2 Power.power_Suc)
18.321 -
18.322 -lemma zero_power2 [simp]: "(0::'a::{semiring_1,recpower})\<twosuperior> = 0"
18.323 - by (simp add: power2_eq_square)
18.324 -
18.325 -lemma one_power2 [simp]: "(1::'a::{semiring_1,recpower})\<twosuperior> = 1"
18.326 - by (simp add: power2_eq_square)
18.327 -
18.328 -lemma power3_eq_cube: "(x::'a::recpower) ^ 3 = x * x * x"
18.329 - apply (subgoal_tac "3 = Suc (Suc (Suc 0))")
18.330 - apply (erule ssubst)
18.331 - apply (simp add: power_Suc mult_ac)
18.332 - apply (unfold nat_number_of_def)
18.333 - apply (subst nat_eq_iff)
18.334 - apply simp
18.335 -done
18.336 -
18.337 -text{*Squares of literal numerals will be evaluated.*}
18.338 -lemmas power2_eq_square_number_of =
18.339 - power2_eq_square [of "number_of w", standard]
18.340 -declare power2_eq_square_number_of [simp]
18.341 -
18.342 -
18.343 -lemma zero_le_power2[simp]: "0 \<le> (a\<twosuperior>::'a::{ordered_idom,recpower})"
18.344 - by (simp add: power2_eq_square)
18.345 -
18.346 -lemma zero_less_power2[simp]:
18.347 - "(0 < a\<twosuperior>) = (a \<noteq> (0::'a::{ordered_idom,recpower}))"
18.348 - by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
18.349 -
18.350 -lemma power2_less_0[simp]:
18.351 - fixes a :: "'a::{ordered_idom,recpower}"
18.352 - shows "~ (a\<twosuperior> < 0)"
18.353 -by (force simp add: power2_eq_square mult_less_0_iff)
18.354 -
18.355 -lemma zero_eq_power2[simp]:
18.356 - "(a\<twosuperior> = 0) = (a = (0::'a::{ordered_idom,recpower}))"
18.357 - by (force simp add: power2_eq_square mult_eq_0_iff)
18.358 -
18.359 -lemma abs_power2[simp]:
18.360 - "abs(a\<twosuperior>) = (a\<twosuperior>::'a::{ordered_idom,recpower})"
18.361 - by (simp add: power2_eq_square abs_mult abs_mult_self)
18.362 -
18.363 -lemma power2_abs[simp]:
18.364 - "(abs a)\<twosuperior> = (a\<twosuperior>::'a::{ordered_idom,recpower})"
18.365 - by (simp add: power2_eq_square abs_mult_self)
18.366 -
18.367 -lemma power2_minus[simp]:
18.368 - "(- a)\<twosuperior> = (a\<twosuperior>::'a::{comm_ring_1,recpower})"
18.369 - by (simp add: power2_eq_square)
18.370 -
18.371 -lemma power2_le_imp_le:
18.372 - fixes x y :: "'a::{ordered_semidom,recpower}"
18.373 - shows "\<lbrakk>x\<twosuperior> \<le> y\<twosuperior>; 0 \<le> y\<rbrakk> \<Longrightarrow> x \<le> y"
18.374 -unfolding numeral_2_eq_2 by (rule power_le_imp_le_base)
18.375 -
18.376 -lemma power2_less_imp_less:
18.377 - fixes x y :: "'a::{ordered_semidom,recpower}"
18.378 - shows "\<lbrakk>x\<twosuperior> < y\<twosuperior>; 0 \<le> y\<rbrakk> \<Longrightarrow> x < y"
18.379 -by (rule power_less_imp_less_base)
18.380 -
18.381 -lemma power2_eq_imp_eq:
18.382 - fixes x y :: "'a::{ordered_semidom,recpower}"
18.383 - shows "\<lbrakk>x\<twosuperior> = y\<twosuperior>; 0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> x = y"
18.384 -unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base, simp)
18.385 -
18.386 -lemma power_minus1_even[simp]: "(- 1) ^ (2*n) = (1::'a::{comm_ring_1,recpower})"
18.387 -proof (induct n)
18.388 - case 0 show ?case by simp
18.389 -next
18.390 - case (Suc n) then show ?case by (simp add: power_Suc power_add)
18.391 -qed
18.392 -
18.393 -lemma power_minus1_odd: "(- 1) ^ Suc(2*n) = -(1::'a::{comm_ring_1,recpower})"
18.394 - by (simp add: power_Suc)
18.395 -
18.396 -lemma power_even_eq: "(a::'a::recpower) ^ (2*n) = (a^n)^2"
18.397 -by (subst mult_commute) (simp add: power_mult)
18.398 -
18.399 -lemma power_odd_eq: "(a::int) ^ Suc(2*n) = a * (a^n)^2"
18.400 -by (simp add: power_even_eq)
18.401 -
18.402 -lemma power_minus_even [simp]:
18.403 - "(-a) ^ (2*n) = (a::'a::{comm_ring_1,recpower}) ^ (2*n)"
18.404 -by (simp add: power_minus1_even power_minus [of a])
18.405 -
18.406 -lemma zero_le_even_power'[simp]:
18.407 - "0 \<le> (a::'a::{ordered_idom,recpower}) ^ (2*n)"
18.408 -proof (induct "n")
18.409 - case 0
18.410 - show ?case by (simp add: zero_le_one)
18.411 -next
18.412 - case (Suc n)
18.413 - have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)"
18.414 - by (simp add: mult_ac power_add power2_eq_square)
18.415 - thus ?case
18.416 - by (simp add: prems zero_le_mult_iff)
18.417 -qed
18.418 -
18.419 -lemma odd_power_less_zero:
18.420 - "(a::'a::{ordered_idom,recpower}) < 0 ==> a ^ Suc(2*n) < 0"
18.421 -proof (induct "n")
18.422 - case 0
18.423 - then show ?case by simp
18.424 -next
18.425 - case (Suc n)
18.426 - have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)"
18.427 - by (simp add: mult_ac power_add power2_eq_square)
18.428 - thus ?case
18.429 - by (simp del: power_Suc add: prems mult_less_0_iff mult_neg_neg)
18.430 -qed
18.431 -
18.432 -lemma odd_0_le_power_imp_0_le:
18.433 - "0 \<le> a ^ Suc(2*n) ==> 0 \<le> (a::'a::{ordered_idom,recpower})"
18.434 -apply (insert odd_power_less_zero [of a n])
18.435 -apply (force simp add: linorder_not_less [symmetric])
18.436 -done
18.437 -
18.438 -text{*Simprules for comparisons where common factors can be cancelled.*}
18.439 -lemmas zero_compare_simps =
18.440 - add_strict_increasing add_strict_increasing2 add_increasing
18.441 - zero_le_mult_iff zero_le_divide_iff
18.442 - zero_less_mult_iff zero_less_divide_iff
18.443 - mult_le_0_iff divide_le_0_iff
18.444 - mult_less_0_iff divide_less_0_iff
18.445 - zero_le_power2 power2_less_0
18.446 -
18.447 -subsubsection{*Nat *}
18.448 -
18.449 -lemma Suc_pred': "0 < n ==> n = Suc(n - 1)"
18.450 -by (simp add: numerals)
18.451 -
18.452 -(*Expresses a natural number constant as the Suc of another one.
18.453 - NOT suitable for rewriting because n recurs in the condition.*)
18.454 -lemmas expand_Suc = Suc_pred' [of "number_of v", standard]
18.455 -
18.456 -subsubsection{*Arith *}
18.457 -
18.458 -lemma Suc_eq_add_numeral_1: "Suc n = n + 1"
18.459 -by (simp add: numerals)
18.460 -
18.461 -lemma Suc_eq_add_numeral_1_left: "Suc n = 1 + n"
18.462 -by (simp add: numerals)
18.463 -
18.464 -(* These two can be useful when m = number_of... *)
18.465 -
18.466 -lemma add_eq_if: "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))"
18.467 - unfolding One_nat_def by (cases m) simp_all
18.468 -
18.469 -lemma mult_eq_if: "(m::nat) * n = (if m=0 then 0 else n + ((m - 1) * n))"
18.470 - unfolding One_nat_def by (cases m) simp_all
18.471 -
18.472 -lemma power_eq_if: "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m - 1)))"
18.473 - unfolding One_nat_def by (cases m) simp_all
18.474 -
18.475 -
18.476 -subsection{*Comparisons involving (0::nat) *}
18.477 -
18.478 -text{*Simplification already does @{term "n<0"}, @{term "n\<le>0"} and @{term "0\<le>n"}.*}
18.479 -
18.480 -lemma eq_number_of_0 [simp]:
18.481 - "number_of v = (0::nat) \<longleftrightarrow> v \<le> Int.Pls"
18.482 - unfolding nat_number_of_def number_of_is_id numeral_simps
18.483 - by auto
18.484 -
18.485 -lemma eq_0_number_of [simp]:
18.486 - "(0::nat) = number_of v \<longleftrightarrow> v \<le> Int.Pls"
18.487 -by (rule trans [OF eq_sym_conv eq_number_of_0])
18.488 -
18.489 -lemma less_0_number_of [simp]:
18.490 - "(0::nat) < number_of v \<longleftrightarrow> Int.Pls < v"
18.491 - unfolding nat_number_of_def number_of_is_id numeral_simps
18.492 - by simp
18.493 -
18.494 -lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)"
18.495 -by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
18.496 -
18.497 -
18.498 -
18.499 -subsection{*Comparisons involving @{term Suc} *}
18.500 -
18.501 -lemma eq_number_of_Suc [simp]:
18.502 - "(number_of v = Suc n) =
18.503 - (let pv = number_of (Int.pred v) in
18.504 - if neg pv then False else nat pv = n)"
18.505 -apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less
18.506 - number_of_pred nat_number_of_def
18.507 - split add: split_if)
18.508 -apply (rule_tac x = "number_of v" in spec)
18.509 -apply (auto simp add: nat_eq_iff)
18.510 -done
18.511 -
18.512 -lemma Suc_eq_number_of [simp]:
18.513 - "(Suc n = number_of v) =
18.514 - (let pv = number_of (Int.pred v) in
18.515 - if neg pv then False else nat pv = n)"
18.516 -by (rule trans [OF eq_sym_conv eq_number_of_Suc])
18.517 -
18.518 -lemma less_number_of_Suc [simp]:
18.519 - "(number_of v < Suc n) =
18.520 - (let pv = number_of (Int.pred v) in
18.521 - if neg pv then True else nat pv < n)"
18.522 -apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less
18.523 - number_of_pred nat_number_of_def
18.524 - split add: split_if)
18.525 -apply (rule_tac x = "number_of v" in spec)
18.526 -apply (auto simp add: nat_less_iff)
18.527 -done
18.528 -
18.529 -lemma less_Suc_number_of [simp]:
18.530 - "(Suc n < number_of v) =
18.531 - (let pv = number_of (Int.pred v) in
18.532 - if neg pv then False else n < nat pv)"
18.533 -apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less
18.534 - number_of_pred nat_number_of_def
18.535 - split add: split_if)
18.536 -apply (rule_tac x = "number_of v" in spec)
18.537 -apply (auto simp add: zless_nat_eq_int_zless)
18.538 -done
18.539 -
18.540 -lemma le_number_of_Suc [simp]:
18.541 - "(number_of v <= Suc n) =
18.542 - (let pv = number_of (Int.pred v) in
18.543 - if neg pv then True else nat pv <= n)"
18.544 -by (simp add: Let_def less_Suc_number_of linorder_not_less [symmetric])
18.545 -
18.546 -lemma le_Suc_number_of [simp]:
18.547 - "(Suc n <= number_of v) =
18.548 - (let pv = number_of (Int.pred v) in
18.549 - if neg pv then False else n <= nat pv)"
18.550 -by (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric])
18.551 -
18.552 -
18.553 -lemma eq_number_of_Pls_Min: "(Numeral0 ::int) ~= number_of Int.Min"
18.554 -by auto
18.555 -
18.556 -
18.557 -
18.558 -subsection{*Max and Min Combined with @{term Suc} *}
18.559 -
18.560 -lemma max_number_of_Suc [simp]:
18.561 - "max (Suc n) (number_of v) =
18.562 - (let pv = number_of (Int.pred v) in
18.563 - if neg pv then Suc n else Suc(max n (nat pv)))"
18.564 -apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def
18.565 - split add: split_if nat.split)
18.566 -apply (rule_tac x = "number_of v" in spec)
18.567 -apply auto
18.568 -done
18.569 -
18.570 -lemma max_Suc_number_of [simp]:
18.571 - "max (number_of v) (Suc n) =
18.572 - (let pv = number_of (Int.pred v) in
18.573 - if neg pv then Suc n else Suc(max (nat pv) n))"
18.574 -apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def
18.575 - split add: split_if nat.split)
18.576 -apply (rule_tac x = "number_of v" in spec)
18.577 -apply auto
18.578 -done
18.579 -
18.580 -lemma min_number_of_Suc [simp]:
18.581 - "min (Suc n) (number_of v) =
18.582 - (let pv = number_of (Int.pred v) in
18.583 - if neg pv then 0 else Suc(min n (nat pv)))"
18.584 -apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def
18.585 - split add: split_if nat.split)
18.586 -apply (rule_tac x = "number_of v" in spec)
18.587 -apply auto
18.588 -done
18.589 -
18.590 -lemma min_Suc_number_of [simp]:
18.591 - "min (number_of v) (Suc n) =
18.592 - (let pv = number_of (Int.pred v) in
18.593 - if neg pv then 0 else Suc(min (nat pv) n))"
18.594 -apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def
18.595 - split add: split_if nat.split)
18.596 -apply (rule_tac x = "number_of v" in spec)
18.597 -apply auto
18.598 -done
18.599 -
18.600 -subsection{*Literal arithmetic involving powers*}
18.601 -
18.602 -lemma nat_power_eq: "(0::int) <= z ==> nat (z^n) = nat z ^ n"
18.603 -apply (induct "n")
18.604 -apply (simp_all (no_asm_simp) add: nat_mult_distrib)
18.605 -done
18.606 -
18.607 -lemma power_nat_number_of:
18.608 - "(number_of v :: nat) ^ n =
18.609 - (if neg (number_of v :: int) then 0^n else nat ((number_of v :: int) ^ n))"
18.610 -by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def nat_power_eq
18.611 - split add: split_if cong: imp_cong)
18.612 -
18.613 -
18.614 -lemmas power_nat_number_of_number_of = power_nat_number_of [of _ "number_of w", standard]
18.615 -declare power_nat_number_of_number_of [simp]
18.616 -
18.617 -
18.618 -
18.619 -text{*For arbitrary rings*}
18.620 -
18.621 -lemma power_number_of_even:
18.622 - fixes z :: "'a::{number_ring,recpower}"
18.623 - shows "z ^ number_of (Int.Bit0 w) = (let w = z ^ (number_of w) in w * w)"
18.624 -unfolding Let_def nat_number_of_def number_of_Bit0
18.625 -apply (rule_tac x = "number_of w" in spec, clarify)
18.626 -apply (case_tac " (0::int) <= x")
18.627 -apply (auto simp add: nat_mult_distrib power_even_eq power2_eq_square)
18.628 -done
18.629 -
18.630 -lemma power_number_of_odd:
18.631 - fixes z :: "'a::{number_ring,recpower}"
18.632 - shows "z ^ number_of (Int.Bit1 w) = (if (0::int) <= number_of w
18.633 - then (let w = z ^ (number_of w) in z * w * w) else 1)"
18.634 -unfolding Let_def nat_number_of_def number_of_Bit1
18.635 -apply (rule_tac x = "number_of w" in spec, auto)
18.636 -apply (simp only: nat_add_distrib nat_mult_distrib)
18.637 -apply simp
18.638 -apply (auto simp add: nat_add_distrib nat_mult_distrib power_even_eq power2_eq_square neg_nat power_Suc)
18.639 -done
18.640 -
18.641 -lemmas zpower_number_of_even = power_number_of_even [where 'a=int]
18.642 -lemmas zpower_number_of_odd = power_number_of_odd [where 'a=int]
18.643 -
18.644 -lemmas power_number_of_even_number_of [simp] =
18.645 - power_number_of_even [of "number_of v", standard]
18.646 -
18.647 -lemmas power_number_of_odd_number_of [simp] =
18.648 - power_number_of_odd [of "number_of v", standard]
18.649 -
18.650 -
18.651 -
18.652 -ML
18.653 -{*
18.654 -val numeral_ss = @{simpset} addsimps @{thms numerals};
18.655 -
18.656 -val nat_bin_arith_setup =
18.657 - Lin_Arith.map_data
18.658 - (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
18.659 - {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
18.660 - inj_thms = inj_thms,
18.661 - lessD = lessD, neqE = neqE,
18.662 - simpset = simpset addsimps @{thms neg_simps} @
18.663 - [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}]})
18.664 -*}
18.665 -
18.666 -declaration {* K nat_bin_arith_setup *}
18.667 -
18.668 -(* Enable arith to deal with div/mod k where k is a numeral: *)
18.669 -declare split_div[of _ _ "number_of k", standard, arith_split]
18.670 -declare split_mod[of _ _ "number_of k", standard, arith_split]
18.671 -
18.672 -lemma nat_number_of_Pls: "Numeral0 = (0::nat)"
18.673 - by (simp add: number_of_Pls nat_number_of_def)
18.674 -
18.675 -lemma nat_number_of_Min: "number_of Int.Min = (0::nat)"
18.676 - apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
18.677 - done
18.678 -
18.679 -lemma nat_number_of_Bit0:
18.680 - "number_of (Int.Bit0 w) = (let n::nat = number_of w in n + n)"
18.681 - unfolding nat_number_of_def number_of_is_id numeral_simps Let_def
18.682 - by auto
18.683 -
18.684 -lemma nat_number_of_Bit1:
18.685 - "number_of (Int.Bit1 w) =
18.686 - (if neg (number_of w :: int) then 0
18.687 - else let n = number_of w in Suc (n + n))"
18.688 - unfolding nat_number_of_def number_of_is_id numeral_simps neg_def Let_def
18.689 - by auto
18.690 -
18.691 -lemmas nat_number =
18.692 - nat_number_of_Pls nat_number_of_Min
18.693 - nat_number_of_Bit0 nat_number_of_Bit1
18.694 -
18.695 -lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
18.696 - by (simp add: Let_def)
18.697 -
18.698 -lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::{number_ring,recpower})"
18.699 -by (simp add: power_mult power_Suc);
18.700 -
18.701 -lemma power_m1_odd: "(-1) ^ Suc(2*n) = (-1::'a::{number_ring,recpower})"
18.702 -by (simp add: power_mult power_Suc);
18.703 -
18.704 -
18.705 -subsection{*Literal arithmetic and @{term of_nat}*}
18.706 -
18.707 -lemma of_nat_double:
18.708 - "0 \<le> x ==> of_nat (nat (2 * x)) = of_nat (nat x) + of_nat (nat x)"
18.709 -by (simp only: mult_2 nat_add_distrib of_nat_add)
18.710 -
18.711 -lemma nat_numeral_m1_eq_0: "-1 = (0::nat)"
18.712 -by (simp only: nat_number_of_def)
18.713 -
18.714 -lemma of_nat_number_of_lemma:
18.715 - "of_nat (number_of v :: nat) =
18.716 - (if 0 \<le> (number_of v :: int)
18.717 - then (number_of v :: 'a :: number_ring)
18.718 - else 0)"
18.719 -by (simp add: int_number_of_def nat_number_of_def number_of_eq of_nat_nat);
18.720 -
18.721 -lemma of_nat_number_of_eq [simp]:
18.722 - "of_nat (number_of v :: nat) =
18.723 - (if neg (number_of v :: int) then 0
18.724 - else (number_of v :: 'a :: number_ring))"
18.725 -by (simp only: of_nat_number_of_lemma neg_def, simp)
18.726 -
18.727 -
18.728 -subsection {*Lemmas for the Combination and Cancellation Simprocs*}
18.729 -
18.730 -lemma nat_number_of_add_left:
18.731 - "number_of v + (number_of v' + (k::nat)) =
18.732 - (if neg (number_of v :: int) then number_of v' + k
18.733 - else if neg (number_of v' :: int) then number_of v + k
18.734 - else number_of (v + v') + k)"
18.735 - unfolding nat_number_of_def number_of_is_id neg_def
18.736 - by auto
18.737 -
18.738 -lemma nat_number_of_mult_left:
18.739 - "number_of v * (number_of v' * (k::nat)) =
18.740 - (if v < Int.Pls then 0
18.741 - else number_of (v * v') * k)"
18.742 -by simp
18.743 -
18.744 -
18.745 -subsubsection{*For @{text combine_numerals}*}
18.746 -
18.747 -lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)"
18.748 -by (simp add: add_mult_distrib)
18.749 -
18.750 -
18.751 -subsubsection{*For @{text cancel_numerals}*}
18.752 -
18.753 -lemma nat_diff_add_eq1:
18.754 - "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"
18.755 -by (simp split add: nat_diff_split add: add_mult_distrib)
18.756 -
18.757 -lemma nat_diff_add_eq2:
18.758 - "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))"
18.759 -by (simp split add: nat_diff_split add: add_mult_distrib)
18.760 -
18.761 -lemma nat_eq_add_iff1:
18.762 - "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)"
18.763 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
18.764 -
18.765 -lemma nat_eq_add_iff2:
18.766 - "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)"
18.767 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
18.768 -
18.769 -lemma nat_less_add_iff1:
18.770 - "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)"
18.771 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
18.772 -
18.773 -lemma nat_less_add_iff2:
18.774 - "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)"
18.775 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
18.776 -
18.777 -lemma nat_le_add_iff1:
18.778 - "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"
18.779 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
18.780 -
18.781 -lemma nat_le_add_iff2:
18.782 - "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"
18.783 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
18.784 -
18.785 -
18.786 -subsubsection{*For @{text cancel_numeral_factors} *}
18.787 -
18.788 -lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)"
18.789 -by auto
18.790 -
18.791 -lemma nat_mult_less_cancel1: "(0::nat) < k ==> (k*m < k*n) = (m<n)"
18.792 -by auto
18.793 -
18.794 -lemma nat_mult_eq_cancel1: "(0::nat) < k ==> (k*m = k*n) = (m=n)"
18.795 -by auto
18.796 -
18.797 -lemma nat_mult_div_cancel1: "(0::nat) < k ==> (k*m) div (k*n) = (m div n)"
18.798 -by auto
18.799 -
18.800 -lemma nat_mult_dvd_cancel_disj[simp]:
18.801 - "(k*m) dvd (k*n) = (k=0 | m dvd (n::nat))"
18.802 -by(auto simp: dvd_eq_mod_eq_0 mod_mult_distrib2[symmetric])
18.803 -
18.804 -lemma nat_mult_dvd_cancel1: "0 < k \<Longrightarrow> (k*m) dvd (k*n::nat) = (m dvd n)"
18.805 -by(auto)
18.806 -
18.807 -
18.808 -subsubsection{*For @{text cancel_factor} *}
18.809 -
18.810 -lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)"
18.811 -by auto
18.812 -
18.813 -lemma nat_mult_less_cancel_disj: "(k*m < k*n) = ((0::nat) < k & m<n)"
18.814 -by auto
18.815 -
18.816 -lemma nat_mult_eq_cancel_disj: "(k*m = k*n) = (k = (0::nat) | m=n)"
18.817 -by auto
18.818 -
18.819 -lemma nat_mult_div_cancel_disj[simp]:
18.820 - "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
18.821 -by (simp add: nat_mult_div_cancel1)
18.822 -
18.823 -
18.824 -subsection {* Simprocs for the Naturals *}
18.825 -
18.826 -use "Tools/nat_simprocs.ML"
18.827 -declaration {* K nat_simprocs_setup *}
18.828 -
18.829 -subsubsection{*For simplifying @{term "Suc m - K"} and @{term "K - Suc m"}*}
18.830 -
18.831 -text{*Where K above is a literal*}
18.832 -
18.833 -lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)"
18.834 -by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split)
18.835 -
18.836 -text {*Now just instantiating @{text n} to @{text "number_of v"} does
18.837 - the right simplification, but with some redundant inequality
18.838 - tests.*}
18.839 -lemma neg_number_of_pred_iff_0:
18.840 - "neg (number_of (Int.pred v)::int) = (number_of v = (0::nat))"
18.841 -apply (subgoal_tac "neg (number_of (Int.pred v)) = (number_of v < Suc 0) ")
18.842 -apply (simp only: less_Suc_eq_le le_0_eq)
18.843 -apply (subst less_number_of_Suc, simp)
18.844 -done
18.845 -
18.846 -text{*No longer required as a simprule because of the @{text inverse_fold}
18.847 - simproc*}
18.848 -lemma Suc_diff_number_of:
18.849 - "Int.Pls < v ==>
18.850 - Suc m - (number_of v) = m - (number_of (Int.pred v))"
18.851 -apply (subst Suc_diff_eq_diff_pred)
18.852 -apply simp
18.853 -apply (simp del: nat_numeral_1_eq_1)
18.854 -apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric]
18.855 - neg_number_of_pred_iff_0)
18.856 -done
18.857 -
18.858 -lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
18.859 -by (simp add: numerals split add: nat_diff_split)
18.860 -
18.861 -
18.862 -subsubsection{*For @{term nat_case} and @{term nat_rec}*}
18.863 -
18.864 -lemma nat_case_number_of [simp]:
18.865 - "nat_case a f (number_of v) =
18.866 - (let pv = number_of (Int.pred v) in
18.867 - if neg pv then a else f (nat pv))"
18.868 -by (simp split add: nat.split add: Let_def neg_number_of_pred_iff_0)
18.869 -
18.870 -lemma nat_case_add_eq_if [simp]:
18.871 - "nat_case a f ((number_of v) + n) =
18.872 - (let pv = number_of (Int.pred v) in
18.873 - if neg pv then nat_case a f n else f (nat pv + n))"
18.874 -apply (subst add_eq_if)
18.875 -apply (simp split add: nat.split
18.876 - del: nat_numeral_1_eq_1
18.877 - add: nat_numeral_1_eq_1 [symmetric]
18.878 - numeral_1_eq_Suc_0 [symmetric]
18.879 - neg_number_of_pred_iff_0)
18.880 -done
18.881 -
18.882 -lemma nat_rec_number_of [simp]:
18.883 - "nat_rec a f (number_of v) =
18.884 - (let pv = number_of (Int.pred v) in
18.885 - if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))"
18.886 -apply (case_tac " (number_of v) ::nat")
18.887 -apply (simp_all (no_asm_simp) add: Let_def neg_number_of_pred_iff_0)
18.888 -apply (simp split add: split_if_asm)
18.889 -done
18.890 -
18.891 -lemma nat_rec_add_eq_if [simp]:
18.892 - "nat_rec a f (number_of v + n) =
18.893 - (let pv = number_of (Int.pred v) in
18.894 - if neg pv then nat_rec a f n
18.895 - else f (nat pv + n) (nat_rec a f (nat pv + n)))"
18.896 -apply (subst add_eq_if)
18.897 -apply (simp split add: nat.split
18.898 - del: nat_numeral_1_eq_1
18.899 - add: nat_numeral_1_eq_1 [symmetric]
18.900 - numeral_1_eq_Suc_0 [symmetric]
18.901 - neg_number_of_pred_iff_0)
18.902 -done
18.903 -
18.904 -
18.905 -subsubsection{*Various Other Lemmas*}
18.906 -
18.907 -text {*Evens and Odds, for Mutilated Chess Board*}
18.908 -
18.909 -text{*Lemmas for specialist use, NOT as default simprules*}
18.910 -lemma nat_mult_2: "2 * z = (z+z::nat)"
18.911 -proof -
18.912 - have "2*z = (1 + 1)*z" by simp
18.913 - also have "... = z+z" by (simp add: left_distrib)
18.914 - finally show ?thesis .
18.915 -qed
18.916 -
18.917 -lemma nat_mult_2_right: "z * 2 = (z+z::nat)"
18.918 -by (subst mult_commute, rule nat_mult_2)
18.919 -
18.920 -text{*Case analysis on @{term "n<2"}*}
18.921 -lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0"
18.922 -by arith
18.923 -
18.924 -lemma div2_Suc_Suc [simp]: "Suc(Suc m) div 2 = Suc (m div 2)"
18.925 -by arith
18.926 -
18.927 -lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
18.928 -by (simp add: nat_mult_2 [symmetric])
18.929 -
18.930 -lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2"
18.931 -apply (subgoal_tac "m mod 2 < 2")
18.932 -apply (erule less_2_cases [THEN disjE])
18.933 -apply (simp_all (no_asm_simp) add: Let_def mod_Suc nat_1)
18.934 -done
18.935 -
18.936 -lemma mod2_gr_0 [simp]: "!!m::nat. (0 < m mod 2) = (m mod 2 = 1)"
18.937 -apply (subgoal_tac "m mod 2 < 2")
18.938 -apply (force simp del: mod_less_divisor, simp)
18.939 -done
18.940 -
18.941 -text{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*}
18.942 -
18.943 -lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)"
18.944 -by simp
18.945 -
18.946 -lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)"
18.947 -by simp
18.948 -
18.949 -text{*Can be used to eliminate long strings of Sucs, but not by default*}
18.950 -lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n"
18.951 -by simp
18.952 -
18.953 -
18.954 -text{*These lemmas collapse some needless occurrences of Suc:
18.955 - at least three Sucs, since two and fewer are rewritten back to Suc again!
18.956 - We already have some rules to simplify operands smaller than 3.*}
18.957 -
18.958 -lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
18.959 -by (simp add: Suc3_eq_add_3)
18.960 -
18.961 -lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
18.962 -by (simp add: Suc3_eq_add_3)
18.963 -
18.964 -lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
18.965 -by (simp add: Suc3_eq_add_3)
18.966 -
18.967 -lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
18.968 -by (simp add: Suc3_eq_add_3)
18.969 -
18.970 -lemmas Suc_div_eq_add3_div_number_of =
18.971 - Suc_div_eq_add3_div [of _ "number_of v", standard]
18.972 -declare Suc_div_eq_add3_div_number_of [simp]
18.973 -
18.974 -lemmas Suc_mod_eq_add3_mod_number_of =
18.975 - Suc_mod_eq_add3_mod [of _ "number_of v", standard]
18.976 -declare Suc_mod_eq_add3_mod_number_of [simp]
18.977 -
18.978 -end
19.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
19.2 +++ b/src/HOL/Nat_Numeral.thy Fri Apr 17 08:36:18 2009 +0200
19.3 @@ -0,0 +1,975 @@
19.4 +(* Title: HOL/Nat_Numeral.thy
19.5 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
19.6 + Copyright 1999 University of Cambridge
19.7 +*)
19.8 +
19.9 +header {* Binary numerals for the natural numbers *}
19.10 +
19.11 +theory Nat_Numeral
19.12 +imports IntDiv
19.13 +uses ("Tools/nat_simprocs.ML")
19.14 +begin
19.15 +
19.16 +text {*
19.17 + Arithmetic for naturals is reduced to that for the non-negative integers.
19.18 +*}
19.19 +
19.20 +instantiation nat :: number
19.21 +begin
19.22 +
19.23 +definition
19.24 + nat_number_of_def [code inline, code del]: "number_of v = nat (number_of v)"
19.25 +
19.26 +instance ..
19.27 +
19.28 +end
19.29 +
19.30 +lemma [code post]:
19.31 + "nat (number_of v) = number_of v"
19.32 + unfolding nat_number_of_def ..
19.33 +
19.34 +abbreviation (xsymbols)
19.35 + power2 :: "'a::power => 'a" ("(_\<twosuperior>)" [1000] 999) where
19.36 + "x\<twosuperior> == x^2"
19.37 +
19.38 +notation (latex output)
19.39 + power2 ("(_\<twosuperior>)" [1000] 999)
19.40 +
19.41 +notation (HTML output)
19.42 + power2 ("(_\<twosuperior>)" [1000] 999)
19.43 +
19.44 +
19.45 +subsection {* Predicate for negative binary numbers *}
19.46 +
19.47 +definition neg :: "int \<Rightarrow> bool" where
19.48 + "neg Z \<longleftrightarrow> Z < 0"
19.49 +
19.50 +lemma not_neg_int [simp]: "~ neg (of_nat n)"
19.51 +by (simp add: neg_def)
19.52 +
19.53 +lemma neg_zminus_int [simp]: "neg (- (of_nat (Suc n)))"
19.54 +by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc)
19.55 +
19.56 +lemmas neg_eq_less_0 = neg_def
19.57 +
19.58 +lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)"
19.59 +by (simp add: neg_def linorder_not_less)
19.60 +
19.61 +text{*To simplify inequalities when Numeral1 can get simplified to 1*}
19.62 +
19.63 +lemma not_neg_0: "~ neg 0"
19.64 +by (simp add: One_int_def neg_def)
19.65 +
19.66 +lemma not_neg_1: "~ neg 1"
19.67 +by (simp add: neg_def linorder_not_less zero_le_one)
19.68 +
19.69 +lemma neg_nat: "neg z ==> nat z = 0"
19.70 +by (simp add: neg_def order_less_imp_le)
19.71 +
19.72 +lemma not_neg_nat: "~ neg z ==> of_nat (nat z) = z"
19.73 +by (simp add: linorder_not_less neg_def)
19.74 +
19.75 +text {*
19.76 + If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
19.77 + @{term Numeral0} IS @{term "number_of Pls"}
19.78 +*}
19.79 +
19.80 +lemma not_neg_number_of_Pls: "~ neg (number_of Int.Pls)"
19.81 + by (simp add: neg_def)
19.82 +
19.83 +lemma neg_number_of_Min: "neg (number_of Int.Min)"
19.84 + by (simp add: neg_def)
19.85 +
19.86 +lemma neg_number_of_Bit0:
19.87 + "neg (number_of (Int.Bit0 w)) = neg (number_of w)"
19.88 + by (simp add: neg_def)
19.89 +
19.90 +lemma neg_number_of_Bit1:
19.91 + "neg (number_of (Int.Bit1 w)) = neg (number_of w)"
19.92 + by (simp add: neg_def)
19.93 +
19.94 +lemmas neg_simps [simp] =
19.95 + not_neg_0 not_neg_1
19.96 + not_neg_number_of_Pls neg_number_of_Min
19.97 + neg_number_of_Bit0 neg_number_of_Bit1
19.98 +
19.99 +
19.100 +subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*}
19.101 +
19.102 +declare nat_0 [simp] nat_1 [simp]
19.103 +
19.104 +lemma nat_number_of [simp]: "nat (number_of w) = number_of w"
19.105 +by (simp add: nat_number_of_def)
19.106 +
19.107 +lemma nat_numeral_0_eq_0 [simp]: "Numeral0 = (0::nat)"
19.108 +by (simp add: nat_number_of_def)
19.109 +
19.110 +lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)"
19.111 +by (simp add: nat_1 nat_number_of_def)
19.112 +
19.113 +lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
19.114 +by (simp add: nat_numeral_1_eq_1)
19.115 +
19.116 +lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
19.117 +apply (unfold nat_number_of_def)
19.118 +apply (rule nat_2)
19.119 +done
19.120 +
19.121 +
19.122 +subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
19.123 +
19.124 +lemma int_nat_number_of [simp]:
19.125 + "int (number_of v) =
19.126 + (if neg (number_of v :: int) then 0
19.127 + else (number_of v :: int))"
19.128 + unfolding nat_number_of_def number_of_is_id neg_def
19.129 + by simp
19.130 +
19.131 +
19.132 +subsubsection{*Successor *}
19.133 +
19.134 +lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
19.135 +apply (rule sym)
19.136 +apply (simp add: nat_eq_iff int_Suc)
19.137 +done
19.138 +
19.139 +lemma Suc_nat_number_of_add:
19.140 + "Suc (number_of v + n) =
19.141 + (if neg (number_of v :: int) then 1+n else number_of (Int.succ v) + n)"
19.142 + unfolding nat_number_of_def number_of_is_id neg_def numeral_simps
19.143 + by (simp add: Suc_nat_eq_nat_zadd1 add_ac)
19.144 +
19.145 +lemma Suc_nat_number_of [simp]:
19.146 + "Suc (number_of v) =
19.147 + (if neg (number_of v :: int) then 1 else number_of (Int.succ v))"
19.148 +apply (cut_tac n = 0 in Suc_nat_number_of_add)
19.149 +apply (simp cong del: if_weak_cong)
19.150 +done
19.151 +
19.152 +
19.153 +subsubsection{*Addition *}
19.154 +
19.155 +lemma add_nat_number_of [simp]:
19.156 + "(number_of v :: nat) + number_of v' =
19.157 + (if v < Int.Pls then number_of v'
19.158 + else if v' < Int.Pls then number_of v
19.159 + else number_of (v + v'))"
19.160 + unfolding nat_number_of_def number_of_is_id numeral_simps
19.161 + by (simp add: nat_add_distrib)
19.162 +
19.163 +lemma nat_number_of_add_1 [simp]:
19.164 + "number_of v + (1::nat) =
19.165 + (if v < Int.Pls then 1 else number_of (Int.succ v))"
19.166 + unfolding nat_number_of_def number_of_is_id numeral_simps
19.167 + by (simp add: nat_add_distrib)
19.168 +
19.169 +lemma nat_1_add_number_of [simp]:
19.170 + "(1::nat) + number_of v =
19.171 + (if v < Int.Pls then 1 else number_of (Int.succ v))"
19.172 + unfolding nat_number_of_def number_of_is_id numeral_simps
19.173 + by (simp add: nat_add_distrib)
19.174 +
19.175 +lemma nat_1_add_1 [simp]: "1 + 1 = (2::nat)"
19.176 + by (rule int_int_eq [THEN iffD1]) simp
19.177 +
19.178 +
19.179 +subsubsection{*Subtraction *}
19.180 +
19.181 +lemma diff_nat_eq_if:
19.182 + "nat z - nat z' =
19.183 + (if neg z' then nat z
19.184 + else let d = z-z' in
19.185 + if neg d then 0 else nat d)"
19.186 +by (simp add: Let_def nat_diff_distrib [symmetric] neg_eq_less_0 not_neg_eq_ge_0)
19.187 +
19.188 +
19.189 +lemma diff_nat_number_of [simp]:
19.190 + "(number_of v :: nat) - number_of v' =
19.191 + (if v' < Int.Pls then number_of v
19.192 + else let d = number_of (v + uminus v') in
19.193 + if neg d then 0 else nat d)"
19.194 + unfolding nat_number_of_def number_of_is_id numeral_simps neg_def
19.195 + by auto
19.196 +
19.197 +lemma nat_number_of_diff_1 [simp]:
19.198 + "number_of v - (1::nat) =
19.199 + (if v \<le> Int.Pls then 0 else number_of (Int.pred v))"
19.200 + unfolding nat_number_of_def number_of_is_id numeral_simps
19.201 + by auto
19.202 +
19.203 +
19.204 +subsubsection{*Multiplication *}
19.205 +
19.206 +lemma mult_nat_number_of [simp]:
19.207 + "(number_of v :: nat) * number_of v' =
19.208 + (if v < Int.Pls then 0 else number_of (v * v'))"
19.209 + unfolding nat_number_of_def number_of_is_id numeral_simps
19.210 + by (simp add: nat_mult_distrib)
19.211 +
19.212 +
19.213 +subsubsection{*Quotient *}
19.214 +
19.215 +lemma div_nat_number_of [simp]:
19.216 + "(number_of v :: nat) div number_of v' =
19.217 + (if neg (number_of v :: int) then 0
19.218 + else nat (number_of v div number_of v'))"
19.219 + unfolding nat_number_of_def number_of_is_id neg_def
19.220 + by (simp add: nat_div_distrib)
19.221 +
19.222 +lemma one_div_nat_number_of [simp]:
19.223 + "Suc 0 div number_of v' = nat (1 div number_of v')"
19.224 +by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric])
19.225 +
19.226 +
19.227 +subsubsection{*Remainder *}
19.228 +
19.229 +lemma mod_nat_number_of [simp]:
19.230 + "(number_of v :: nat) mod number_of v' =
19.231 + (if neg (number_of v :: int) then 0
19.232 + else if neg (number_of v' :: int) then number_of v
19.233 + else nat (number_of v mod number_of v'))"
19.234 + unfolding nat_number_of_def number_of_is_id neg_def
19.235 + by (simp add: nat_mod_distrib)
19.236 +
19.237 +lemma one_mod_nat_number_of [simp]:
19.238 + "Suc 0 mod number_of v' =
19.239 + (if neg (number_of v' :: int) then Suc 0
19.240 + else nat (1 mod number_of v'))"
19.241 +by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric])
19.242 +
19.243 +
19.244 +subsubsection{* Divisibility *}
19.245 +
19.246 +lemmas dvd_eq_mod_eq_0_number_of =
19.247 + dvd_eq_mod_eq_0 [of "number_of x" "number_of y", standard]
19.248 +
19.249 +declare dvd_eq_mod_eq_0_number_of [simp]
19.250 +
19.251 +ML
19.252 +{*
19.253 +val nat_number_of_def = thm"nat_number_of_def";
19.254 +
19.255 +val nat_number_of = thm"nat_number_of";
19.256 +val nat_numeral_0_eq_0 = thm"nat_numeral_0_eq_0";
19.257 +val nat_numeral_1_eq_1 = thm"nat_numeral_1_eq_1";
19.258 +val numeral_1_eq_Suc_0 = thm"numeral_1_eq_Suc_0";
19.259 +val numeral_2_eq_2 = thm"numeral_2_eq_2";
19.260 +val nat_div_distrib = thm"nat_div_distrib";
19.261 +val nat_mod_distrib = thm"nat_mod_distrib";
19.262 +val int_nat_number_of = thm"int_nat_number_of";
19.263 +val Suc_nat_eq_nat_zadd1 = thm"Suc_nat_eq_nat_zadd1";
19.264 +val Suc_nat_number_of_add = thm"Suc_nat_number_of_add";
19.265 +val Suc_nat_number_of = thm"Suc_nat_number_of";
19.266 +val add_nat_number_of = thm"add_nat_number_of";
19.267 +val diff_nat_eq_if = thm"diff_nat_eq_if";
19.268 +val diff_nat_number_of = thm"diff_nat_number_of";
19.269 +val mult_nat_number_of = thm"mult_nat_number_of";
19.270 +val div_nat_number_of = thm"div_nat_number_of";
19.271 +val mod_nat_number_of = thm"mod_nat_number_of";
19.272 +*}
19.273 +
19.274 +
19.275 +subsection{*Comparisons*}
19.276 +
19.277 +subsubsection{*Equals (=) *}
19.278 +
19.279 +lemma eq_nat_nat_iff:
19.280 + "[| (0::int) <= z; 0 <= z' |] ==> (nat z = nat z') = (z=z')"
19.281 +by (auto elim!: nonneg_eq_int)
19.282 +
19.283 +lemma eq_nat_number_of [simp]:
19.284 + "((number_of v :: nat) = number_of v') =
19.285 + (if neg (number_of v :: int) then (number_of v' :: int) \<le> 0
19.286 + else if neg (number_of v' :: int) then (number_of v :: int) = 0
19.287 + else v = v')"
19.288 + unfolding nat_number_of_def number_of_is_id neg_def
19.289 + by auto
19.290 +
19.291 +
19.292 +subsubsection{*Less-than (<) *}
19.293 +
19.294 +lemma less_nat_number_of [simp]:
19.295 + "(number_of v :: nat) < number_of v' \<longleftrightarrow>
19.296 + (if v < v' then Int.Pls < v' else False)"
19.297 + unfolding nat_number_of_def number_of_is_id numeral_simps
19.298 + by auto
19.299 +
19.300 +
19.301 +subsubsection{*Less-than-or-equal *}
19.302 +
19.303 +lemma le_nat_number_of [simp]:
19.304 + "(number_of v :: nat) \<le> number_of v' \<longleftrightarrow>
19.305 + (if v \<le> v' then True else v \<le> Int.Pls)"
19.306 + unfolding nat_number_of_def number_of_is_id numeral_simps
19.307 + by auto
19.308 +
19.309 +(*Maps #n to n for n = 0, 1, 2*)
19.310 +lemmas numerals = nat_numeral_0_eq_0 nat_numeral_1_eq_1 numeral_2_eq_2
19.311 +
19.312 +
19.313 +subsection{*Powers with Numeric Exponents*}
19.314 +
19.315 +text{*We cannot refer to the number @{term 2} in @{text Ring_and_Field.thy}.
19.316 +We cannot prove general results about the numeral @{term "-1"}, so we have to
19.317 +use @{term "- 1"} instead.*}
19.318 +
19.319 +lemma power2_eq_square: "(a::'a::recpower)\<twosuperior> = a * a"
19.320 + by (simp add: numeral_2_eq_2 Power.power_Suc)
19.321 +
19.322 +lemma zero_power2 [simp]: "(0::'a::{semiring_1,recpower})\<twosuperior> = 0"
19.323 + by (simp add: power2_eq_square)
19.324 +
19.325 +lemma one_power2 [simp]: "(1::'a::{semiring_1,recpower})\<twosuperior> = 1"
19.326 + by (simp add: power2_eq_square)
19.327 +
19.328 +lemma power3_eq_cube: "(x::'a::recpower) ^ 3 = x * x * x"
19.329 + apply (subgoal_tac "3 = Suc (Suc (Suc 0))")
19.330 + apply (erule ssubst)
19.331 + apply (simp add: power_Suc mult_ac)
19.332 + apply (unfold nat_number_of_def)
19.333 + apply (subst nat_eq_iff)
19.334 + apply simp
19.335 +done
19.336 +
19.337 +text{*Squares of literal numerals will be evaluated.*}
19.338 +lemmas power2_eq_square_number_of =
19.339 + power2_eq_square [of "number_of w", standard]
19.340 +declare power2_eq_square_number_of [simp]
19.341 +
19.342 +
19.343 +lemma zero_le_power2[simp]: "0 \<le> (a\<twosuperior>::'a::{ordered_idom,recpower})"
19.344 + by (simp add: power2_eq_square)
19.345 +
19.346 +lemma zero_less_power2[simp]:
19.347 + "(0 < a\<twosuperior>) = (a \<noteq> (0::'a::{ordered_idom,recpower}))"
19.348 + by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
19.349 +
19.350 +lemma power2_less_0[simp]:
19.351 + fixes a :: "'a::{ordered_idom,recpower}"
19.352 + shows "~ (a\<twosuperior> < 0)"
19.353 +by (force simp add: power2_eq_square mult_less_0_iff)
19.354 +
19.355 +lemma zero_eq_power2[simp]:
19.356 + "(a\<twosuperior> = 0) = (a = (0::'a::{ordered_idom,recpower}))"
19.357 + by (force simp add: power2_eq_square mult_eq_0_iff)
19.358 +
19.359 +lemma abs_power2[simp]:
19.360 + "abs(a\<twosuperior>) = (a\<twosuperior>::'a::{ordered_idom,recpower})"
19.361 + by (simp add: power2_eq_square abs_mult abs_mult_self)
19.362 +
19.363 +lemma power2_abs[simp]:
19.364 + "(abs a)\<twosuperior> = (a\<twosuperior>::'a::{ordered_idom,recpower})"
19.365 + by (simp add: power2_eq_square abs_mult_self)
19.366 +
19.367 +lemma power2_minus[simp]:
19.368 + "(- a)\<twosuperior> = (a\<twosuperior>::'a::{comm_ring_1,recpower})"
19.369 + by (simp add: power2_eq_square)
19.370 +
19.371 +lemma power2_le_imp_le:
19.372 + fixes x y :: "'a::{ordered_semidom,recpower}"
19.373 + shows "\<lbrakk>x\<twosuperior> \<le> y\<twosuperior>; 0 \<le> y\<rbrakk> \<Longrightarrow> x \<le> y"
19.374 +unfolding numeral_2_eq_2 by (rule power_le_imp_le_base)
19.375 +
19.376 +lemma power2_less_imp_less:
19.377 + fixes x y :: "'a::{ordered_semidom,recpower}"
19.378 + shows "\<lbrakk>x\<twosuperior> < y\<twosuperior>; 0 \<le> y\<rbrakk> \<Longrightarrow> x < y"
19.379 +by (rule power_less_imp_less_base)
19.380 +
19.381 +lemma power2_eq_imp_eq:
19.382 + fixes x y :: "'a::{ordered_semidom,recpower}"
19.383 + shows "\<lbrakk>x\<twosuperior> = y\<twosuperior>; 0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> x = y"
19.384 +unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base, simp)
19.385 +
19.386 +lemma power_minus1_even[simp]: "(- 1) ^ (2*n) = (1::'a::{comm_ring_1,recpower})"
19.387 +proof (induct n)
19.388 + case 0 show ?case by simp
19.389 +next
19.390 + case (Suc n) then show ?case by (simp add: power_Suc power_add)
19.391 +qed
19.392 +
19.393 +lemma power_minus1_odd: "(- 1) ^ Suc(2*n) = -(1::'a::{comm_ring_1,recpower})"
19.394 + by (simp add: power_Suc)
19.395 +
19.396 +lemma power_even_eq: "(a::'a::recpower) ^ (2*n) = (a^n)^2"
19.397 +by (subst mult_commute) (simp add: power_mult)
19.398 +
19.399 +lemma power_odd_eq: "(a::int) ^ Suc(2*n) = a * (a^n)^2"
19.400 +by (simp add: power_even_eq)
19.401 +
19.402 +lemma power_minus_even [simp]:
19.403 + "(-a) ^ (2*n) = (a::'a::{comm_ring_1,recpower}) ^ (2*n)"
19.404 +by (simp add: power_minus1_even power_minus [of a])
19.405 +
19.406 +lemma zero_le_even_power'[simp]:
19.407 + "0 \<le> (a::'a::{ordered_idom,recpower}) ^ (2*n)"
19.408 +proof (induct "n")
19.409 + case 0
19.410 + show ?case by (simp add: zero_le_one)
19.411 +next
19.412 + case (Suc n)
19.413 + have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)"
19.414 + by (simp add: mult_ac power_add power2_eq_square)
19.415 + thus ?case
19.416 + by (simp add: prems zero_le_mult_iff)
19.417 +qed
19.418 +
19.419 +lemma odd_power_less_zero:
19.420 + "(a::'a::{ordered_idom,recpower}) < 0 ==> a ^ Suc(2*n) < 0"
19.421 +proof (induct "n")
19.422 + case 0
19.423 + then show ?case by simp
19.424 +next
19.425 + case (Suc n)
19.426 + have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)"
19.427 + by (simp add: mult_ac power_add power2_eq_square)
19.428 + thus ?case
19.429 + by (simp del: power_Suc add: prems mult_less_0_iff mult_neg_neg)
19.430 +qed
19.431 +
19.432 +lemma odd_0_le_power_imp_0_le:
19.433 + "0 \<le> a ^ Suc(2*n) ==> 0 \<le> (a::'a::{ordered_idom,recpower})"
19.434 +apply (insert odd_power_less_zero [of a n])
19.435 +apply (force simp add: linorder_not_less [symmetric])
19.436 +done
19.437 +
19.438 +text{*Simprules for comparisons where common factors can be cancelled.*}
19.439 +lemmas zero_compare_simps =
19.440 + add_strict_increasing add_strict_increasing2 add_increasing
19.441 + zero_le_mult_iff zero_le_divide_iff
19.442 + zero_less_mult_iff zero_less_divide_iff
19.443 + mult_le_0_iff divide_le_0_iff
19.444 + mult_less_0_iff divide_less_0_iff
19.445 + zero_le_power2 power2_less_0
19.446 +
19.447 +subsubsection{*Nat *}
19.448 +
19.449 +lemma Suc_pred': "0 < n ==> n = Suc(n - 1)"
19.450 +by (simp add: numerals)
19.451 +
19.452 +(*Expresses a natural number constant as the Suc of another one.
19.453 + NOT suitable for rewriting because n recurs in the condition.*)
19.454 +lemmas expand_Suc = Suc_pred' [of "number_of v", standard]
19.455 +
19.456 +subsubsection{*Arith *}
19.457 +
19.458 +lemma Suc_eq_add_numeral_1: "Suc n = n + 1"
19.459 +by (simp add: numerals)
19.460 +
19.461 +lemma Suc_eq_add_numeral_1_left: "Suc n = 1 + n"
19.462 +by (simp add: numerals)
19.463 +
19.464 +(* These two can be useful when m = number_of... *)
19.465 +
19.466 +lemma add_eq_if: "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))"
19.467 + unfolding One_nat_def by (cases m) simp_all
19.468 +
19.469 +lemma mult_eq_if: "(m::nat) * n = (if m=0 then 0 else n + ((m - 1) * n))"
19.470 + unfolding One_nat_def by (cases m) simp_all
19.471 +
19.472 +lemma power_eq_if: "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m - 1)))"
19.473 + unfolding One_nat_def by (cases m) simp_all
19.474 +
19.475 +
19.476 +subsection{*Comparisons involving (0::nat) *}
19.477 +
19.478 +text{*Simplification already does @{term "n<0"}, @{term "n\<le>0"} and @{term "0\<le>n"}.*}
19.479 +
19.480 +lemma eq_number_of_0 [simp]:
19.481 + "number_of v = (0::nat) \<longleftrightarrow> v \<le> Int.Pls"
19.482 + unfolding nat_number_of_def number_of_is_id numeral_simps
19.483 + by auto
19.484 +
19.485 +lemma eq_0_number_of [simp]:
19.486 + "(0::nat) = number_of v \<longleftrightarrow> v \<le> Int.Pls"
19.487 +by (rule trans [OF eq_sym_conv eq_number_of_0])
19.488 +
19.489 +lemma less_0_number_of [simp]:
19.490 + "(0::nat) < number_of v \<longleftrightarrow> Int.Pls < v"
19.491 + unfolding nat_number_of_def number_of_is_id numeral_simps
19.492 + by simp
19.493 +
19.494 +lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)"
19.495 +by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
19.496 +
19.497 +
19.498 +
19.499 +subsection{*Comparisons involving @{term Suc} *}
19.500 +
19.501 +lemma eq_number_of_Suc [simp]:
19.502 + "(number_of v = Suc n) =
19.503 + (let pv = number_of (Int.pred v) in
19.504 + if neg pv then False else nat pv = n)"
19.505 +apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less
19.506 + number_of_pred nat_number_of_def
19.507 + split add: split_if)
19.508 +apply (rule_tac x = "number_of v" in spec)
19.509 +apply (auto simp add: nat_eq_iff)
19.510 +done
19.511 +
19.512 +lemma Suc_eq_number_of [simp]:
19.513 + "(Suc n = number_of v) =
19.514 + (let pv = number_of (Int.pred v) in
19.515 + if neg pv then False else nat pv = n)"
19.516 +by (rule trans [OF eq_sym_conv eq_number_of_Suc])
19.517 +
19.518 +lemma less_number_of_Suc [simp]:
19.519 + "(number_of v < Suc n) =
19.520 + (let pv = number_of (Int.pred v) in
19.521 + if neg pv then True else nat pv < n)"
19.522 +apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less
19.523 + number_of_pred nat_number_of_def
19.524 + split add: split_if)
19.525 +apply (rule_tac x = "number_of v" in spec)
19.526 +apply (auto simp add: nat_less_iff)
19.527 +done
19.528 +
19.529 +lemma less_Suc_number_of [simp]:
19.530 + "(Suc n < number_of v) =
19.531 + (let pv = number_of (Int.pred v) in
19.532 + if neg pv then False else n < nat pv)"
19.533 +apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less
19.534 + number_of_pred nat_number_of_def
19.535 + split add: split_if)
19.536 +apply (rule_tac x = "number_of v" in spec)
19.537 +apply (auto simp add: zless_nat_eq_int_zless)
19.538 +done
19.539 +
19.540 +lemma le_number_of_Suc [simp]:
19.541 + "(number_of v <= Suc n) =
19.542 + (let pv = number_of (Int.pred v) in
19.543 + if neg pv then True else nat pv <= n)"
19.544 +by (simp add: Let_def less_Suc_number_of linorder_not_less [symmetric])
19.545 +
19.546 +lemma le_Suc_number_of [simp]:
19.547 + "(Suc n <= number_of v) =
19.548 + (let pv = number_of (Int.pred v) in
19.549 + if neg pv then False else n <= nat pv)"
19.550 +by (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric])
19.551 +
19.552 +
19.553 +lemma eq_number_of_Pls_Min: "(Numeral0 ::int) ~= number_of Int.Min"
19.554 +by auto
19.555 +
19.556 +
19.557 +
19.558 +subsection{*Max and Min Combined with @{term Suc} *}
19.559 +
19.560 +lemma max_number_of_Suc [simp]:
19.561 + "max (Suc n) (number_of v) =
19.562 + (let pv = number_of (Int.pred v) in
19.563 + if neg pv then Suc n else Suc(max n (nat pv)))"
19.564 +apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def
19.565 + split add: split_if nat.split)
19.566 +apply (rule_tac x = "number_of v" in spec)
19.567 +apply auto
19.568 +done
19.569 +
19.570 +lemma max_Suc_number_of [simp]:
19.571 + "max (number_of v) (Suc n) =
19.572 + (let pv = number_of (Int.pred v) in
19.573 + if neg pv then Suc n else Suc(max (nat pv) n))"
19.574 +apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def
19.575 + split add: split_if nat.split)
19.576 +apply (rule_tac x = "number_of v" in spec)
19.577 +apply auto
19.578 +done
19.579 +
19.580 +lemma min_number_of_Suc [simp]:
19.581 + "min (Suc n) (number_of v) =
19.582 + (let pv = number_of (Int.pred v) in
19.583 + if neg pv then 0 else Suc(min n (nat pv)))"
19.584 +apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def
19.585 + split add: split_if nat.split)
19.586 +apply (rule_tac x = "number_of v" in spec)
19.587 +apply auto
19.588 +done
19.589 +
19.590 +lemma min_Suc_number_of [simp]:
19.591 + "min (number_of v) (Suc n) =
19.592 + (let pv = number_of (Int.pred v) in
19.593 + if neg pv then 0 else Suc(min (nat pv) n))"
19.594 +apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def
19.595 + split add: split_if nat.split)
19.596 +apply (rule_tac x = "number_of v" in spec)
19.597 +apply auto
19.598 +done
19.599 +
19.600 +subsection{*Literal arithmetic involving powers*}
19.601 +
19.602 +lemma nat_power_eq: "(0::int) <= z ==> nat (z^n) = nat z ^ n"
19.603 +apply (induct "n")
19.604 +apply (simp_all (no_asm_simp) add: nat_mult_distrib)
19.605 +done
19.606 +
19.607 +lemma power_nat_number_of:
19.608 + "(number_of v :: nat) ^ n =
19.609 + (if neg (number_of v :: int) then 0^n else nat ((number_of v :: int) ^ n))"
19.610 +by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def nat_power_eq
19.611 + split add: split_if cong: imp_cong)
19.612 +
19.613 +
19.614 +lemmas power_nat_number_of_number_of = power_nat_number_of [of _ "number_of w", standard]
19.615 +declare power_nat_number_of_number_of [simp]
19.616 +
19.617 +
19.618 +
19.619 +text{*For arbitrary rings*}
19.620 +
19.621 +lemma power_number_of_even:
19.622 + fixes z :: "'a::{number_ring,recpower}"
19.623 + shows "z ^ number_of (Int.Bit0 w) = (let w = z ^ (number_of w) in w * w)"
19.624 +unfolding Let_def nat_number_of_def number_of_Bit0
19.625 +apply (rule_tac x = "number_of w" in spec, clarify)
19.626 +apply (case_tac " (0::int) <= x")
19.627 +apply (auto simp add: nat_mult_distrib power_even_eq power2_eq_square)
19.628 +done
19.629 +
19.630 +lemma power_number_of_odd:
19.631 + fixes z :: "'a::{number_ring,recpower}"
19.632 + shows "z ^ number_of (Int.Bit1 w) = (if (0::int) <= number_of w
19.633 + then (let w = z ^ (number_of w) in z * w * w) else 1)"
19.634 +unfolding Let_def nat_number_of_def number_of_Bit1
19.635 +apply (rule_tac x = "number_of w" in spec, auto)
19.636 +apply (simp only: nat_add_distrib nat_mult_distrib)
19.637 +apply simp
19.638 +apply (auto simp add: nat_add_distrib nat_mult_distrib power_even_eq power2_eq_square neg_nat power_Suc)
19.639 +done
19.640 +
19.641 +lemmas zpower_number_of_even = power_number_of_even [where 'a=int]
19.642 +lemmas zpower_number_of_odd = power_number_of_odd [where 'a=int]
19.643 +
19.644 +lemmas power_number_of_even_number_of [simp] =
19.645 + power_number_of_even [of "number_of v", standard]
19.646 +
19.647 +lemmas power_number_of_odd_number_of [simp] =
19.648 + power_number_of_odd [of "number_of v", standard]
19.649 +
19.650 +
19.651 +
19.652 +ML
19.653 +{*
19.654 +val numeral_ss = @{simpset} addsimps @{thms numerals};
19.655 +
19.656 +val nat_bin_arith_setup =
19.657 + Lin_Arith.map_data
19.658 + (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
19.659 + {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
19.660 + inj_thms = inj_thms,
19.661 + lessD = lessD, neqE = neqE,
19.662 + simpset = simpset addsimps @{thms neg_simps} @
19.663 + [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}]})
19.664 +*}
19.665 +
19.666 +declaration {* K nat_bin_arith_setup *}
19.667 +
19.668 +(* Enable arith to deal with div/mod k where k is a numeral: *)
19.669 +declare split_div[of _ _ "number_of k", standard, arith_split]
19.670 +declare split_mod[of _ _ "number_of k", standard, arith_split]
19.671 +
19.672 +lemma nat_number_of_Pls: "Numeral0 = (0::nat)"
19.673 + by (simp add: number_of_Pls nat_number_of_def)
19.674 +
19.675 +lemma nat_number_of_Min: "number_of Int.Min = (0::nat)"
19.676 + apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
19.677 + done
19.678 +
19.679 +lemma nat_number_of_Bit0:
19.680 + "number_of (Int.Bit0 w) = (let n::nat = number_of w in n + n)"
19.681 + unfolding nat_number_of_def number_of_is_id numeral_simps Let_def
19.682 + by auto
19.683 +
19.684 +lemma nat_number_of_Bit1:
19.685 + "number_of (Int.Bit1 w) =
19.686 + (if neg (number_of w :: int) then 0
19.687 + else let n = number_of w in Suc (n + n))"
19.688 + unfolding nat_number_of_def number_of_is_id numeral_simps neg_def Let_def
19.689 + by auto
19.690 +
19.691 +lemmas nat_number =
19.692 + nat_number_of_Pls nat_number_of_Min
19.693 + nat_number_of_Bit0 nat_number_of_Bit1
19.694 +
19.695 +lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
19.696 + by (simp add: Let_def)
19.697 +
19.698 +lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::{number_ring,recpower})"
19.699 +by (simp add: power_mult power_Suc);
19.700 +
19.701 +lemma power_m1_odd: "(-1) ^ Suc(2*n) = (-1::'a::{number_ring,recpower})"
19.702 +by (simp add: power_mult power_Suc);
19.703 +
19.704 +
19.705 +subsection{*Literal arithmetic and @{term of_nat}*}
19.706 +
19.707 +lemma of_nat_double:
19.708 + "0 \<le> x ==> of_nat (nat (2 * x)) = of_nat (nat x) + of_nat (nat x)"
19.709 +by (simp only: mult_2 nat_add_distrib of_nat_add)
19.710 +
19.711 +lemma nat_numeral_m1_eq_0: "-1 = (0::nat)"
19.712 +by (simp only: nat_number_of_def)
19.713 +
19.714 +lemma of_nat_number_of_lemma:
19.715 + "of_nat (number_of v :: nat) =
19.716 + (if 0 \<le> (number_of v :: int)
19.717 + then (number_of v :: 'a :: number_ring)
19.718 + else 0)"
19.719 +by (simp add: int_number_of_def nat_number_of_def number_of_eq of_nat_nat);
19.720 +
19.721 +lemma of_nat_number_of_eq [simp]:
19.722 + "of_nat (number_of v :: nat) =
19.723 + (if neg (number_of v :: int) then 0
19.724 + else (number_of v :: 'a :: number_ring))"
19.725 +by (simp only: of_nat_number_of_lemma neg_def, simp)
19.726 +
19.727 +
19.728 +subsection {*Lemmas for the Combination and Cancellation Simprocs*}
19.729 +
19.730 +lemma nat_number_of_add_left:
19.731 + "number_of v + (number_of v' + (k::nat)) =
19.732 + (if neg (number_of v :: int) then number_of v' + k
19.733 + else if neg (number_of v' :: int) then number_of v + k
19.734 + else number_of (v + v') + k)"
19.735 + unfolding nat_number_of_def number_of_is_id neg_def
19.736 + by auto
19.737 +
19.738 +lemma nat_number_of_mult_left:
19.739 + "number_of v * (number_of v' * (k::nat)) =
19.740 + (if v < Int.Pls then 0
19.741 + else number_of (v * v') * k)"
19.742 +by simp
19.743 +
19.744 +
19.745 +subsubsection{*For @{text combine_numerals}*}
19.746 +
19.747 +lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)"
19.748 +by (simp add: add_mult_distrib)
19.749 +
19.750 +
19.751 +subsubsection{*For @{text cancel_numerals}*}
19.752 +
19.753 +lemma nat_diff_add_eq1:
19.754 + "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"
19.755 +by (simp split add: nat_diff_split add: add_mult_distrib)
19.756 +
19.757 +lemma nat_diff_add_eq2:
19.758 + "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))"
19.759 +by (simp split add: nat_diff_split add: add_mult_distrib)
19.760 +
19.761 +lemma nat_eq_add_iff1:
19.762 + "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)"
19.763 +by (auto split add: nat_diff_split simp add: add_mult_distrib)
19.764 +
19.765 +lemma nat_eq_add_iff2:
19.766 + "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)"
19.767 +by (auto split add: nat_diff_split simp add: add_mult_distrib)
19.768 +
19.769 +lemma nat_less_add_iff1:
19.770 + "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)"
19.771 +by (auto split add: nat_diff_split simp add: add_mult_distrib)
19.772 +
19.773 +lemma nat_less_add_iff2:
19.774 + "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)"
19.775 +by (auto split add: nat_diff_split simp add: add_mult_distrib)
19.776 +
19.777 +lemma nat_le_add_iff1:
19.778 + "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"
19.779 +by (auto split add: nat_diff_split simp add: add_mult_distrib)
19.780 +
19.781 +lemma nat_le_add_iff2:
19.782 + "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"
19.783 +by (auto split add: nat_diff_split simp add: add_mult_distrib)
19.784 +
19.785 +
19.786 +subsubsection{*For @{text cancel_numeral_factors} *}
19.787 +
19.788 +lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)"
19.789 +by auto
19.790 +
19.791 +lemma nat_mult_less_cancel1: "(0::nat) < k ==> (k*m < k*n) = (m<n)"
19.792 +by auto
19.793 +
19.794 +lemma nat_mult_eq_cancel1: "(0::nat) < k ==> (k*m = k*n) = (m=n)"
19.795 +by auto
19.796 +
19.797 +lemma nat_mult_div_cancel1: "(0::nat) < k ==> (k*m) div (k*n) = (m div n)"
19.798 +by auto
19.799 +
19.800 +lemma nat_mult_dvd_cancel_disj[simp]:
19.801 + "(k*m) dvd (k*n) = (k=0 | m dvd (n::nat))"
19.802 +by(auto simp: dvd_eq_mod_eq_0 mod_mult_distrib2[symmetric])
19.803 +
19.804 +lemma nat_mult_dvd_cancel1: "0 < k \<Longrightarrow> (k*m) dvd (k*n::nat) = (m dvd n)"
19.805 +by(auto)
19.806 +
19.807 +
19.808 +subsubsection{*For @{text cancel_factor} *}
19.809 +
19.810 +lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)"
19.811 +by auto
19.812 +
19.813 +lemma nat_mult_less_cancel_disj: "(k*m < k*n) = ((0::nat) < k & m<n)"
19.814 +by auto
19.815 +
19.816 +lemma nat_mult_eq_cancel_disj: "(k*m = k*n) = (k = (0::nat) | m=n)"
19.817 +by auto
19.818 +
19.819 +lemma nat_mult_div_cancel_disj[simp]:
19.820 + "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
19.821 +by (simp add: nat_mult_div_cancel1)
19.822 +
19.823 +
19.824 +subsection {* Simprocs for the Naturals *}
19.825 +
19.826 +use "Tools/nat_simprocs.ML"
19.827 +declaration {* K nat_simprocs_setup *}
19.828 +
19.829 +subsubsection{*For simplifying @{term "Suc m - K"} and @{term "K - Suc m"}*}
19.830 +
19.831 +text{*Where K above is a literal*}
19.832 +
19.833 +lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)"
19.834 +by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split)
19.835 +
19.836 +text {*Now just instantiating @{text n} to @{text "number_of v"} does
19.837 + the right simplification, but with some redundant inequality
19.838 + tests.*}
19.839 +lemma neg_number_of_pred_iff_0:
19.840 + "neg (number_of (Int.pred v)::int) = (number_of v = (0::nat))"
19.841 +apply (subgoal_tac "neg (number_of (Int.pred v)) = (number_of v < Suc 0) ")
19.842 +apply (simp only: less_Suc_eq_le le_0_eq)
19.843 +apply (subst less_number_of_Suc, simp)
19.844 +done
19.845 +
19.846 +text{*No longer required as a simprule because of the @{text inverse_fold}
19.847 + simproc*}
19.848 +lemma Suc_diff_number_of:
19.849 + "Int.Pls < v ==>
19.850 + Suc m - (number_of v) = m - (number_of (Int.pred v))"
19.851 +apply (subst Suc_diff_eq_diff_pred)
19.852 +apply simp
19.853 +apply (simp del: nat_numeral_1_eq_1)
19.854 +apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric]
19.855 + neg_number_of_pred_iff_0)
19.856 +done
19.857 +
19.858 +lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
19.859 +by (simp add: numerals split add: nat_diff_split)
19.860 +
19.861 +
19.862 +subsubsection{*For @{term nat_case} and @{term nat_rec}*}
19.863 +
19.864 +lemma nat_case_number_of [simp]:
19.865 + "nat_case a f (number_of v) =
19.866 + (let pv = number_of (Int.pred v) in
19.867 + if neg pv then a else f (nat pv))"
19.868 +by (simp split add: nat.split add: Let_def neg_number_of_pred_iff_0)
19.869 +
19.870 +lemma nat_case_add_eq_if [simp]:
19.871 + "nat_case a f ((number_of v) + n) =
19.872 + (let pv = number_of (Int.pred v) in
19.873 + if neg pv then nat_case a f n else f (nat pv + n))"
19.874 +apply (subst add_eq_if)
19.875 +apply (simp split add: nat.split
19.876 + del: nat_numeral_1_eq_1
19.877 + add: nat_numeral_1_eq_1 [symmetric]
19.878 + numeral_1_eq_Suc_0 [symmetric]
19.879 + neg_number_of_pred_iff_0)
19.880 +done
19.881 +
19.882 +lemma nat_rec_number_of [simp]:
19.883 + "nat_rec a f (number_of v) =
19.884 + (let pv = number_of (Int.pred v) in
19.885 + if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))"
19.886 +apply (case_tac " (number_of v) ::nat")
19.887 +apply (simp_all (no_asm_simp) add: Let_def neg_number_of_pred_iff_0)
19.888 +apply (simp split add: split_if_asm)
19.889 +done
19.890 +
19.891 +lemma nat_rec_add_eq_if [simp]:
19.892 + "nat_rec a f (number_of v + n) =
19.893 + (let pv = number_of (Int.pred v) in
19.894 + if neg pv then nat_rec a f n
19.895 + else f (nat pv + n) (nat_rec a f (nat pv + n)))"
19.896 +apply (subst add_eq_if)
19.897 +apply (simp split add: nat.split
19.898 + del: nat_numeral_1_eq_1
19.899 + add: nat_numeral_1_eq_1 [symmetric]
19.900 + numeral_1_eq_Suc_0 [symmetric]
19.901 + neg_number_of_pred_iff_0)
19.902 +done
19.903 +
19.904 +
19.905 +subsubsection{*Various Other Lemmas*}
19.906 +
19.907 +text {*Evens and Odds, for Mutilated Chess Board*}
19.908 +
19.909 +text{*Lemmas for specialist use, NOT as default simprules*}
19.910 +lemma nat_mult_2: "2 * z = (z+z::nat)"
19.911 +proof -
19.912 + have "2*z = (1 + 1)*z" by simp
19.913 + also have "... = z+z" by (simp add: left_distrib)
19.914 + finally show ?thesis .
19.915 +qed
19.916 +
19.917 +lemma nat_mult_2_right: "z * 2 = (z+z::nat)"
19.918 +by (subst mult_commute, rule nat_mult_2)
19.919 +
19.920 +text{*Case analysis on @{term "n<2"}*}
19.921 +lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0"
19.922 +by arith
19.923 +
19.924 +lemma div2_Suc_Suc [simp]: "Suc(Suc m) div 2 = Suc (m div 2)"
19.925 +by arith
19.926 +
19.927 +lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
19.928 +by (simp add: nat_mult_2 [symmetric])
19.929 +
19.930 +lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2"
19.931 +apply (subgoal_tac "m mod 2 < 2")
19.932 +apply (erule less_2_cases [THEN disjE])
19.933 +apply (simp_all (no_asm_simp) add: Let_def mod_Suc nat_1)
19.934 +done
19.935 +
19.936 +lemma mod2_gr_0 [simp]: "!!m::nat. (0 < m mod 2) = (m mod 2 = 1)"
19.937 +apply (subgoal_tac "m mod 2 < 2")
19.938 +apply (force simp del: mod_less_divisor, simp)
19.939 +done
19.940 +
19.941 +text{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*}
19.942 +
19.943 +lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)"
19.944 +by simp
19.945 +
19.946 +lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)"
19.947 +by simp
19.948 +
19.949 +text{*Can be used to eliminate long strings of Sucs, but not by default*}
19.950 +lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n"
19.951 +by simp
19.952 +
19.953 +
19.954 +text{*These lemmas collapse some needless occurrences of Suc:
19.955 + at least three Sucs, since two and fewer are rewritten back to Suc again!
19.956 + We already have some rules to simplify operands smaller than 3.*}
19.957 +
19.958 +lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
19.959 +by (simp add: Suc3_eq_add_3)
19.960 +
19.961 +lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
19.962 +by (simp add: Suc3_eq_add_3)
19.963 +
19.964 +lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
19.965 +by (simp add: Suc3_eq_add_3)
19.966 +
19.967 +lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
19.968 +by (simp add: Suc3_eq_add_3)
19.969 +
19.970 +lemmas Suc_div_eq_add3_div_number_of =
19.971 + Suc_div_eq_add3_div [of _ "number_of v", standard]
19.972 +declare Suc_div_eq_add3_div_number_of [simp]
19.973 +
19.974 +lemmas Suc_mod_eq_add3_mod_number_of =
19.975 + Suc_mod_eq_add3_mod [of _ "number_of v", standard]
19.976 +declare Suc_mod_eq_add3_mod_number_of [simp]
19.977 +
19.978 +end
20.1 --- a/src/HOL/Orderings.thy Thu Apr 16 17:29:56 2009 +0200
20.2 +++ b/src/HOL/Orderings.thy Fri Apr 17 08:36:18 2009 +0200
20.3 @@ -5,7 +5,7 @@
20.4 header {* Abstract orderings *}
20.5
20.6 theory Orderings
20.7 -imports Code_Setup
20.8 +imports HOL
20.9 uses "~~/src/Provers/order.ML"
20.10 begin
20.11
21.1 --- a/src/HOL/Product_Type.thy Thu Apr 16 17:29:56 2009 +0200
21.2 +++ b/src/HOL/Product_Type.thy Fri Apr 17 08:36:18 2009 +0200
21.3 @@ -84,6 +84,14 @@
21.4 lemma unit_abs_eta_conv [simp,noatp]: "(%u::unit. f ()) = f"
21.5 by (rule ext) simp
21.6
21.7 +instantiation unit :: default
21.8 +begin
21.9 +
21.10 +definition "default = ()"
21.11 +
21.12 +instance ..
21.13 +
21.14 +end
21.15
21.16 text {* code generator setup *}
21.17
22.1 --- a/src/HOL/Tools/Qelim/presburger.ML Thu Apr 16 17:29:56 2009 +0200
22.2 +++ b/src/HOL/Tools/Qelim/presburger.ML Fri Apr 17 08:36:18 2009 +0200
22.3 @@ -131,7 +131,7 @@
22.4 @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"},
22.5 @{thm "mod_1"}, @{thm "Suc_plus1"}]
22.6 @ @{thms add_ac}
22.7 - addsimprocs [cancel_div_mod_proc]
22.8 + addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
22.9 val splits_ss = comp_ss addsimps [@{thm "mod_div_equality'"}] addsplits
22.10 [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"},
22.11 @{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}]
23.1 --- a/src/HOL/Tools/int_factor_simprocs.ML Thu Apr 16 17:29:56 2009 +0200
23.2 +++ b/src/HOL/Tools/int_factor_simprocs.ML Fri Apr 17 08:36:18 2009 +0200
23.3 @@ -1,5 +1,4 @@
23.4 (* Title: HOL/int_factor_simprocs.ML
23.5 - ID: $Id$
23.6 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
23.7 Copyright 2000 University of Cambridge
23.8
23.9 @@ -46,13 +45,13 @@
23.10 @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right}];
23.11 end
23.12
23.13 -(*Version for integer division*)
23.14 -structure IntDivCancelNumeralFactor = CancelNumeralFactorFun
23.15 +(*Version for semiring_div*)
23.16 +structure DivCancelNumeralFactor = CancelNumeralFactorFun
23.17 (open CancelNumeralFactorCommon
23.18 val prove_conv = Arith_Data.prove_conv
23.19 val mk_bal = HOLogic.mk_binop @{const_name Divides.div}
23.20 - val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT
23.21 - val cancel = @{thm zdiv_zmult_zmult1} RS trans
23.22 + val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT
23.23 + val cancel = @{thm div_mult_mult1} RS trans
23.24 val neg_exchanges = false
23.25 )
23.26
23.27 @@ -108,8 +107,9 @@
23.28 "(l::'a::{ordered_idom,number_ring}) <= m * n"],
23.29 K LeCancelNumeralFactor.proc),
23.30 ("int_div_cancel_numeral_factors",
23.31 - ["((l::int) * m) div n", "(l::int) div (m * n)"],
23.32 - K IntDivCancelNumeralFactor.proc),
23.33 + ["((l::'a::{semiring_div,number_ring}) * m) div n",
23.34 + "(l::'a::{semiring_div,number_ring}) div (m * n)"],
23.35 + K DivCancelNumeralFactor.proc),
23.36 ("divide_cancel_numeral_factor",
23.37 ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
23.38 "(l::'a::{division_by_zero,field,number_ring}) / (m * n)",
23.39 @@ -284,24 +284,25 @@
23.40 @{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg}
23.41 );
23.42
23.43 -(*zdiv_zmult_zmult1_if is for integer division (div).*)
23.44 -structure IntDivCancelFactor = ExtractCommonTermFun
23.45 +(*for semirings with division*)
23.46 +structure DivCancelFactor = ExtractCommonTermFun
23.47 (open CancelFactorCommon
23.48 val prove_conv = Arith_Data.prove_conv
23.49 val mk_bal = HOLogic.mk_binop @{const_name Divides.div}
23.50 - val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT
23.51 - val simp_conv = K (K (SOME @{thm zdiv_zmult_zmult1_if}))
23.52 + val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT
23.53 + val simp_conv = K (K (SOME @{thm div_mult_mult1_if}))
23.54 );
23.55
23.56 -structure IntModCancelFactor = ExtractCommonTermFun
23.57 +structure ModCancelFactor = ExtractCommonTermFun
23.58 (open CancelFactorCommon
23.59 val prove_conv = Arith_Data.prove_conv
23.60 val mk_bal = HOLogic.mk_binop @{const_name Divides.mod}
23.61 val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} HOLogic.intT
23.62 - val simp_conv = K (K (SOME @{thm zmod_zmult_zmult1}))
23.63 + val simp_conv = K (K (SOME @{thm mod_mult_mult1}))
23.64 );
23.65
23.66 -structure IntDvdCancelFactor = ExtractCommonTermFun
23.67 +(*for idoms*)
23.68 +structure DvdCancelFactor = ExtractCommonTermFun
23.69 (open CancelFactorCommon
23.70 val prove_conv = Arith_Data.prove_conv
23.71 val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
23.72 @@ -321,8 +322,8 @@
23.73 val cancel_factors =
23.74 map Arith_Data.prep_simproc
23.75 [("ring_eq_cancel_factor",
23.76 - ["(l::'a::{idom}) * m = n",
23.77 - "(l::'a::{idom}) = m * n"],
23.78 + ["(l::'a::idom) * m = n",
23.79 + "(l::'a::idom) = m * n"],
23.80 K EqCancelFactor.proc),
23.81 ("ordered_ring_le_cancel_factor",
23.82 ["(l::'a::ordered_ring) * m <= n",
23.83 @@ -333,14 +334,14 @@
23.84 "(l::'a::ordered_ring) < m * n"],
23.85 K LessCancelFactor.proc),
23.86 ("int_div_cancel_factor",
23.87 - ["((l::int) * m) div n", "(l::int) div (m * n)"],
23.88 - K IntDivCancelFactor.proc),
23.89 + ["((l::'a::semiring_div) * m) div n", "(l::'a::semiring_div) div (m * n)"],
23.90 + K DivCancelFactor.proc),
23.91 ("int_mod_cancel_factor",
23.92 - ["((l::int) * m) mod n", "(l::int) mod (m * n)"],
23.93 - K IntModCancelFactor.proc),
23.94 + ["((l::'a::semiring_div) * m) mod n", "(l::'a::semiring_div) mod (m * n)"],
23.95 + K ModCancelFactor.proc),
23.96 ("dvd_cancel_factor",
23.97 ["((l::'a::idom) * m) dvd n", "(l::'a::idom) dvd (m * n)"],
23.98 - K IntDvdCancelFactor.proc),
23.99 + K DvdCancelFactor.proc),
23.100 ("divide_cancel_factor",
23.101 ["((l::'a::{division_by_zero,field}) * m) / n",
23.102 "(l::'a::{division_by_zero,field}) / (m * n)"],
24.1 --- a/src/HOL/Word/BinGeneral.thy Thu Apr 16 17:29:56 2009 +0200
24.2 +++ b/src/HOL/Word/BinGeneral.thy Fri Apr 17 08:36:18 2009 +0200
24.3 @@ -439,7 +439,7 @@
24.4 apply clarsimp
24.5 apply (simp add: bin_last_mod bin_rest_div Bit_def
24.6 cong: number_of_False_cong)
24.7 - apply (clarsimp simp: zmod_zmult_zmult1 [symmetric]
24.8 + apply (clarsimp simp: mod_mult_mult1 [symmetric]
24.9 zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]])
24.10 apply (rule trans [symmetric, OF _ emep1])
24.11 apply auto
25.1 --- a/src/HOL/Word/BinOperations.thy Thu Apr 16 17:29:56 2009 +0200
25.2 +++ b/src/HOL/Word/BinOperations.thy Fri Apr 17 08:36:18 2009 +0200
25.3 @@ -641,7 +641,7 @@
25.4 apply (simp add: bin_rest_div zdiv_zmult2_eq)
25.5 apply (case_tac b rule: bin_exhaust)
25.6 apply simp
25.7 - apply (simp add: Bit_def zmod_zmult_zmult1 p1mod22k
25.8 + apply (simp add: Bit_def mod_mult_mult1 p1mod22k
25.9 split: bit.split
25.10 cong: number_of_False_cong)
25.11 done
26.1 --- a/src/HOL/Word/Num_Lemmas.thy Thu Apr 16 17:29:56 2009 +0200
26.2 +++ b/src/HOL/Word/Num_Lemmas.thy Fri Apr 17 08:36:18 2009 +0200
26.3 @@ -66,7 +66,7 @@
26.4 apply (safe dest!: even_equiv_def [THEN iffD1])
26.5 apply (subst pos_zmod_mult_2)
26.6 apply arith
26.7 - apply (simp add: zmod_zmult_zmult1)
26.8 + apply (simp add: mod_mult_mult1)
26.9 done
26.10
26.11 lemmas eme1p = emep1 [simplified add_commute]
27.1 --- a/src/HOL/base.ML Thu Apr 16 17:29:56 2009 +0200
27.2 +++ b/src/HOL/base.ML Fri Apr 17 08:36:18 2009 +0200
27.3 @@ -1,2 +1,2 @@
27.4 (*side-entry for HOL-Base*)
27.5 -use_thy "Code_Setup";
27.6 +use_thy "HOL";
28.1 --- a/src/Provers/Arith/cancel_div_mod.ML Thu Apr 16 17:29:56 2009 +0200
28.2 +++ b/src/Provers/Arith/cancel_div_mod.ML Fri Apr 17 08:36:18 2009 +0200
28.3 @@ -69,7 +69,7 @@
28.4
28.5 fun cancel ss t pq =
28.6 let val teqt' = Data.prove_eq_sums ss (t, rearrange t pq)
28.7 - in hd(Data.div_mod_eqs RL [teqt' RS transitive_thm]) end;
28.8 + in hd (Data.div_mod_eqs RL [teqt' RS transitive_thm]) end;
28.9
28.10 fun proc ss t =
28.11 let val (divs,mods) = coll_div_mod t ([],[])
29.1 --- a/src/Pure/Isar/code.ML Thu Apr 16 17:29:56 2009 +0200
29.2 +++ b/src/Pure/Isar/code.ML Fri Apr 17 08:36:18 2009 +0200
29.3 @@ -29,8 +29,6 @@
29.4 val add_undefined: string -> theory -> theory
29.5 val purge_data: theory -> theory
29.6
29.7 - val coregular_algebra: theory -> Sorts.algebra
29.8 - val operational_algebra: theory -> (sort -> sort) * Sorts.algebra
29.9 val these_eqns: theory -> string -> (thm * bool) list
29.10 val these_raw_eqns: theory -> string -> (thm * bool) list
29.11 val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
29.12 @@ -469,39 +467,6 @@
29.13 fun mk_default_eqn thy = Code_Unit.try_thm (check_linear o Code_Unit.mk_eqn thy);
29.14
29.15
29.16 -(** operational sort algebra and class discipline **)
29.17 -
29.18 -local
29.19 -
29.20 -fun arity_constraints thy algebra (class, tyco) =
29.21 - let
29.22 - val base_constraints = Sorts.mg_domain algebra tyco [class];
29.23 - val classparam_constraints = Sorts.complete_sort algebra [class]
29.24 - |> maps (map fst o these o try (#params o AxClass.get_info thy))
29.25 - |> map_filter (fn c => try (AxClass.param_of_inst thy) (c, tyco))
29.26 - |> maps (map fst o get_eqns thy)
29.27 - |> map (map (snd o dest_TVar) o Sign.const_typargs thy o Code_Unit.const_typ_eqn);
29.28 - val inter_sorts = map2 (curry (Sorts.inter_sort algebra));
29.29 - in fold inter_sorts classparam_constraints base_constraints end;
29.30 -
29.31 -fun retrieve_algebra thy operational =
29.32 - Sorts.subalgebra (Syntax.pp_global thy) operational
29.33 - (SOME o arity_constraints thy (Sign.classes_of thy))
29.34 - (Sign.classes_of thy);
29.35 -
29.36 -in
29.37 -
29.38 -fun coregular_algebra thy = retrieve_algebra thy (K true) |> snd;
29.39 -fun operational_algebra thy =
29.40 - let
29.41 - fun add_iff_operational class =
29.42 - can (AxClass.get_info thy) class ? cons class;
29.43 - val operational_classes = fold add_iff_operational (Sign.all_classes thy) []
29.44 - in retrieve_algebra thy (member (op =) operational_classes) end;
29.45 -
29.46 -end; (*local*)
29.47 -
29.48 -
29.49 (** interfaces and attributes **)
29.50
29.51 fun delete_force msg key xs =
30.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
30.2 +++ b/src/Tools/Code_Generator.thy Fri Apr 17 08:36:18 2009 +0200
30.3 @@ -0,0 +1,27 @@
30.4 +(* Title: Tools/Code_Generator.thy
30.5 + Author: Florian Haftmann, TU Muenchen
30.6 +*)
30.7 +
30.8 +header {* Loading the code generator modules *}
30.9 +
30.10 +theory Code_Generator
30.11 +imports Pure
30.12 +uses
30.13 + "~~/src/Tools/value.ML"
30.14 + "~~/src/Tools/code/code_name.ML"
30.15 + "~~/src/Tools/code/code_wellsorted.ML"
30.16 + "~~/src/Tools/code/code_thingol.ML"
30.17 + "~~/src/Tools/code/code_printer.ML"
30.18 + "~~/src/Tools/code/code_target.ML"
30.19 + "~~/src/Tools/code/code_ml.ML"
30.20 + "~~/src/Tools/code/code_haskell.ML"
30.21 + "~~/src/Tools/nbe.ML"
30.22 +begin
30.23 +
30.24 +setup {*
30.25 + Code_ML.setup
30.26 + #> Code_Haskell.setup
30.27 + #> Nbe.setup
30.28 +*}
30.29 +
30.30 +end
30.31 \ No newline at end of file
31.1 --- a/src/Tools/code/code_funcgr.ML Thu Apr 16 17:29:56 2009 +0200
31.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
31.3 @@ -1,335 +0,0 @@
31.4 -(* Title: Tools/code/code_funcgr.ML
31.5 - Author: Florian Haftmann, TU Muenchen
31.6 -
31.7 -Retrieving, normalizing and structuring code equations in graph
31.8 -with explicit dependencies.
31.9 -
31.10 -Legacy. To be replaced by Tools/code/code_wellsorted.ML
31.11 -*)
31.12 -
31.13 -signature CODE_WELLSORTED =
31.14 -sig
31.15 - type T
31.16 - val eqns: T -> string -> (thm * bool) list
31.17 - val typ: T -> string -> (string * sort) list * typ
31.18 - val all: T -> string list
31.19 - val pretty: theory -> T -> Pretty.T
31.20 - val make: theory -> string list
31.21 - -> ((sort -> sort) * Sorts.algebra) * T
31.22 - val eval_conv: theory
31.23 - -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> thm)) -> cterm -> thm
31.24 - val eval_term: theory
31.25 - -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> 'a)) -> term -> 'a
31.26 - val timing: bool ref
31.27 -end
31.28 -
31.29 -structure Code_Wellsorted : CODE_WELLSORTED =
31.30 -struct
31.31 -
31.32 -(** the graph type **)
31.33 -
31.34 -type T = (((string * sort) list * typ) * (thm * bool) list) Graph.T;
31.35 -
31.36 -fun eqns funcgr =
31.37 - these o Option.map snd o try (Graph.get_node funcgr);
31.38 -
31.39 -fun typ funcgr =
31.40 - fst o Graph.get_node funcgr;
31.41 -
31.42 -fun all funcgr = Graph.keys funcgr;
31.43 -
31.44 -fun pretty thy funcgr =
31.45 - AList.make (snd o Graph.get_node funcgr) (Graph.keys funcgr)
31.46 - |> (map o apfst) (Code_Unit.string_of_const thy)
31.47 - |> sort (string_ord o pairself fst)
31.48 - |> map (fn (s, thms) =>
31.49 - (Pretty.block o Pretty.fbreaks) (
31.50 - Pretty.str s
31.51 - :: map (Display.pretty_thm o fst) thms
31.52 - ))
31.53 - |> Pretty.chunks;
31.54 -
31.55 -
31.56 -(** generic combinators **)
31.57 -
31.58 -fun fold_consts f thms =
31.59 - thms
31.60 - |> maps (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of)
31.61 - |> (fold o fold_aterms) (fn Const c => f c | _ => I);
31.62 -
31.63 -fun consts_of (const, []) = []
31.64 - | consts_of (const, thms as _ :: _) =
31.65 - let
31.66 - fun the_const (c, _) = if c = const then I else insert (op =) c
31.67 - in fold_consts the_const (map fst thms) [] end;
31.68 -
31.69 -fun insts_of thy algebra tys sorts =
31.70 - let
31.71 - fun class_relation (x, _) _ = x;
31.72 - fun type_constructor tyco xs class =
31.73 - (tyco, class) :: (maps o maps) fst xs;
31.74 - fun type_variable (TVar (_, sort)) = map (pair []) sort
31.75 - | type_variable (TFree (_, sort)) = map (pair []) sort;
31.76 - fun of_sort_deriv ty sort =
31.77 - Sorts.of_sort_derivation (Syntax.pp_global thy) algebra
31.78 - { class_relation = class_relation, type_constructor = type_constructor,
31.79 - type_variable = type_variable }
31.80 - (ty, sort) handle Sorts.CLASS_ERROR _ => [] (*permissive!*)
31.81 - in (flat o flat) (map2 of_sort_deriv tys sorts) end;
31.82 -
31.83 -fun meets_of thy algebra =
31.84 - let
31.85 - fun meet_of ty sort tab =
31.86 - Sorts.meet_sort algebra (ty, sort) tab
31.87 - handle Sorts.CLASS_ERROR _ => tab (*permissive!*);
31.88 - in fold2 meet_of end;
31.89 -
31.90 -
31.91 -(** graph algorithm **)
31.92 -
31.93 -val timing = ref false;
31.94 -
31.95 -local
31.96 -
31.97 -fun resort_thms thy algebra typ_of thms =
31.98 - let
31.99 - val cs = fold_consts (insert (op =)) thms [];
31.100 - fun meets (c, ty) = case typ_of c
31.101 - of SOME (vs, _) =>
31.102 - meets_of thy algebra (Sign.const_typargs thy (c, ty)) (map snd vs)
31.103 - | NONE => I;
31.104 - val tab = fold meets cs Vartab.empty;
31.105 - in map (Code_Unit.inst_thm thy tab) thms end;
31.106 -
31.107 -fun resort_eqnss thy algebra funcgr =
31.108 - let
31.109 - val typ_funcgr = try (fst o Graph.get_node funcgr);
31.110 - val resort_dep = (apsnd o burrow_fst) (resort_thms thy algebra typ_funcgr);
31.111 - fun resort_rec typ_of (c, []) = (true, (c, []))
31.112 - | resort_rec typ_of (c, thms as (thm, _) :: _) = if is_some (AxClass.inst_of_param thy c)
31.113 - then (true, (c, thms))
31.114 - else let
31.115 - val (_, (vs, ty)) = Code_Unit.head_eqn thy thm;
31.116 - val thms' as (thm', _) :: _ = burrow_fst (resort_thms thy algebra typ_of) thms
31.117 - val (_, (vs', ty')) = Code_Unit.head_eqn thy thm'; (*FIXME simplify check*)
31.118 - in (Sign.typ_equiv thy (ty, ty'), (c, thms')) end;
31.119 - fun resort_recs eqnss =
31.120 - let
31.121 - fun typ_of c = case these (AList.lookup (op =) eqnss c)
31.122 - of (thm, _) :: _ => (SOME o snd o Code_Unit.head_eqn thy) thm
31.123 - | [] => NONE;
31.124 - val (unchangeds, eqnss') = split_list (map (resort_rec typ_of) eqnss);
31.125 - val unchanged = fold (fn x => fn y => x andalso y) unchangeds true;
31.126 - in (unchanged, eqnss') end;
31.127 - fun resort_rec_until eqnss =
31.128 - let
31.129 - val (unchanged, eqnss') = resort_recs eqnss;
31.130 - in if unchanged then eqnss' else resort_rec_until eqnss' end;
31.131 - in map resort_dep #> resort_rec_until end;
31.132 -
31.133 -fun instances_of thy algebra insts =
31.134 - let
31.135 - val thy_classes = (#classes o Sorts.rep_algebra o Sign.classes_of) thy;
31.136 - fun all_classparams tyco class =
31.137 - these (try (#params o AxClass.get_info thy) class)
31.138 - |> map_filter (fn (c, _) => try (AxClass.param_of_inst thy) (c, tyco))
31.139 - in
31.140 - Symtab.empty
31.141 - |> fold (fn (tyco, class) =>
31.142 - Symtab.map_default (tyco, []) (insert (op =) class)) insts
31.143 - |> (fn tab => Symtab.fold (fn (tyco, classes) => append (maps (all_classparams tyco)
31.144 - (Graph.all_succs thy_classes classes))) tab [])
31.145 - end;
31.146 -
31.147 -fun instances_of_consts thy algebra funcgr consts =
31.148 - let
31.149 - fun inst (cexpr as (c, ty)) = insts_of thy algebra
31.150 - (Sign.const_typargs thy (c, ty)) ((map snd o fst) (typ funcgr c));
31.151 - in
31.152 - []
31.153 - |> fold (fold (insert (op =)) o inst) consts
31.154 - |> instances_of thy algebra
31.155 - end;
31.156 -
31.157 -fun ensure_const' thy algebra funcgr const auxgr =
31.158 - if can (Graph.get_node funcgr) const
31.159 - then (NONE, auxgr)
31.160 - else if can (Graph.get_node auxgr) const
31.161 - then (SOME const, auxgr)
31.162 - else if is_some (Code.get_datatype_of_constr thy const) then
31.163 - auxgr
31.164 - |> Graph.new_node (const, [])
31.165 - |> pair (SOME const)
31.166 - else let
31.167 - val thms = Code.these_eqns thy const
31.168 - |> burrow_fst (Code_Unit.norm_args thy)
31.169 - |> burrow_fst (Code_Unit.norm_varnames thy Code_Name.purify_tvar Code_Name.purify_var);
31.170 - val rhs = consts_of (const, thms);
31.171 - in
31.172 - auxgr
31.173 - |> Graph.new_node (const, thms)
31.174 - |> fold_map (ensure_const thy algebra funcgr) rhs
31.175 - |-> (fn rhs' => fold (fn SOME const' => Graph.add_edge (const, const')
31.176 - | NONE => I) rhs')
31.177 - |> pair (SOME const)
31.178 - end
31.179 -and ensure_const thy algebra funcgr const =
31.180 - let
31.181 - val timeap = if !timing
31.182 - then Output.timeap_msg ("time for " ^ Code_Unit.string_of_const thy const)
31.183 - else I;
31.184 - in timeap (ensure_const' thy algebra funcgr const) end;
31.185 -
31.186 -fun merge_eqnss thy algebra raw_eqnss funcgr =
31.187 - let
31.188 - val eqnss = raw_eqnss
31.189 - |> resort_eqnss thy algebra funcgr
31.190 - |> filter_out (can (Graph.get_node funcgr) o fst);
31.191 - fun typ_eqn c [] = Code.default_typscheme thy c
31.192 - | typ_eqn c (thms as (thm, _) :: _) = (snd o Code_Unit.head_eqn thy) thm;
31.193 - fun add_eqns (const, thms) =
31.194 - Graph.new_node (const, (typ_eqn const thms, thms));
31.195 - fun add_deps (eqns as (const, thms)) funcgr =
31.196 - let
31.197 - val deps = consts_of eqns;
31.198 - val insts = instances_of_consts thy algebra funcgr
31.199 - (fold_consts (insert (op =)) (map fst thms) []);
31.200 - in
31.201 - funcgr
31.202 - |> ensure_consts thy algebra insts
31.203 - |> fold (curry Graph.add_edge const) deps
31.204 - |> fold (curry Graph.add_edge const) insts
31.205 - end;
31.206 - in
31.207 - funcgr
31.208 - |> fold add_eqns eqnss
31.209 - |> fold add_deps eqnss
31.210 - end
31.211 -and ensure_consts thy algebra cs funcgr =
31.212 - let
31.213 - val auxgr = Graph.empty
31.214 - |> fold (snd oo ensure_const thy algebra funcgr) cs;
31.215 - in
31.216 - funcgr
31.217 - |> fold (merge_eqnss thy algebra)
31.218 - (map (AList.make (Graph.get_node auxgr))
31.219 - (rev (Graph.strong_conn auxgr)))
31.220 - end;
31.221 -
31.222 -in
31.223 -
31.224 -(** retrieval interfaces **)
31.225 -
31.226 -val ensure_consts = ensure_consts;
31.227 -
31.228 -fun proto_eval thy cterm_of evaluator_lift evaluator proto_ct funcgr =
31.229 - let
31.230 - val ct = cterm_of proto_ct;
31.231 - val _ = Sign.no_vars (Syntax.pp_global thy) (Thm.term_of ct);
31.232 - val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) ();
31.233 - fun consts_of t =
31.234 - fold_aterms (fn Const c_ty => cons c_ty | _ => I) t [];
31.235 - val algebra = Code.coregular_algebra thy;
31.236 - val thm = Code.preprocess_conv thy ct;
31.237 - val ct' = Thm.rhs_of thm;
31.238 - val t' = Thm.term_of ct';
31.239 - val consts = map fst (consts_of t');
31.240 - val funcgr' = ensure_consts thy algebra consts funcgr;
31.241 - val (t'', evaluator_funcgr) = evaluator t';
31.242 - val consts' = consts_of t'';
31.243 - val dicts = instances_of_consts thy algebra funcgr' consts';
31.244 - val funcgr'' = ensure_consts thy algebra dicts funcgr';
31.245 - in (evaluator_lift (evaluator_funcgr (Code.operational_algebra thy)) thm funcgr'', funcgr'') end;
31.246 -
31.247 -fun proto_eval_conv thy =
31.248 - let
31.249 - fun evaluator_lift evaluator thm1 funcgr =
31.250 - let
31.251 - val thm2 = evaluator funcgr;
31.252 - val thm3 = Code.postprocess_conv thy (Thm.rhs_of thm2);
31.253 - in
31.254 - Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
31.255 - error ("could not construct evaluation proof:\n"
31.256 - ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3])
31.257 - end;
31.258 - in proto_eval thy I evaluator_lift end;
31.259 -
31.260 -fun proto_eval_term thy =
31.261 - let
31.262 - fun evaluator_lift evaluator _ funcgr = evaluator funcgr;
31.263 - in proto_eval thy (Thm.cterm_of thy) evaluator_lift end;
31.264 -
31.265 -end; (*local*)
31.266 -
31.267 -structure Funcgr = CodeDataFun
31.268 -(
31.269 - type T = T;
31.270 - val empty = Graph.empty;
31.271 - fun purge _ cs funcgr =
31.272 - Graph.del_nodes ((Graph.all_preds funcgr
31.273 - o filter (can (Graph.get_node funcgr))) cs) funcgr;
31.274 -);
31.275 -
31.276 -fun make thy =
31.277 - pair (Code.operational_algebra thy)
31.278 - o Funcgr.change thy o ensure_consts thy (Code.coregular_algebra thy);
31.279 -
31.280 -fun eval_conv thy f =
31.281 - fst o Funcgr.change_yield thy o proto_eval_conv thy f;
31.282 -
31.283 -fun eval_term thy f =
31.284 - fst o Funcgr.change_yield thy o proto_eval_term thy f;
31.285 -
31.286 -
31.287 -(** diagnostic commands **)
31.288 -
31.289 -fun code_depgr thy consts =
31.290 - let
31.291 - val (_, gr) = make thy consts;
31.292 - val select = Graph.all_succs gr consts;
31.293 - in
31.294 - gr
31.295 - |> not (null consts) ? Graph.subgraph (member (op =) select)
31.296 - |> Graph.map_nodes ((apsnd o map o apfst) (AxClass.overload thy))
31.297 - end;
31.298 -
31.299 -fun code_thms thy = Pretty.writeln o pretty thy o code_depgr thy;
31.300 -
31.301 -fun code_deps thy consts =
31.302 - let
31.303 - val gr = code_depgr thy consts;
31.304 - fun mk_entry (const, (_, (_, parents))) =
31.305 - let
31.306 - val name = Code_Unit.string_of_const thy const;
31.307 - val nameparents = map (Code_Unit.string_of_const thy) parents;
31.308 - in { name = name, ID = name, dir = "", unfold = true,
31.309 - path = "", parents = nameparents }
31.310 - end;
31.311 - val prgr = Graph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) gr [];
31.312 - in Present.display_graph prgr end;
31.313 -
31.314 -local
31.315 -
31.316 -structure P = OuterParse
31.317 -and K = OuterKeyword
31.318 -
31.319 -fun code_thms_cmd thy = code_thms thy o op @ o Code_Name.read_const_exprs thy;
31.320 -fun code_deps_cmd thy = code_deps thy o op @ o Code_Name.read_const_exprs thy;
31.321 -
31.322 -in
31.323 -
31.324 -val _ =
31.325 - OuterSyntax.improper_command "code_thms" "print system of code equations for code" OuterKeyword.diag
31.326 - (Scan.repeat P.term_group
31.327 - >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
31.328 - o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
31.329 -
31.330 -val _ =
31.331 - OuterSyntax.improper_command "code_deps" "visualize dependencies of code equations for code" OuterKeyword.diag
31.332 - (Scan.repeat P.term_group
31.333 - >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
31.334 - o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
31.335 -
31.336 -end;
31.337 -
31.338 -end; (*struct*)
32.1 --- a/src/Tools/code/code_ml.ML Thu Apr 16 17:29:56 2009 +0200
32.2 +++ b/src/Tools/code/code_ml.ML Fri Apr 17 08:36:18 2009 +0200
32.3 @@ -951,13 +951,13 @@
32.4
32.5 (* evaluation *)
32.6
32.7 -fun eval eval'' term_of reff thy ct args =
32.8 +fun eval_term reff thy t args =
32.9 let
32.10 val ctxt = ProofContext.init thy;
32.11 - val _ = if null (Term.add_frees (term_of ct) []) then () else error ("Term "
32.12 - ^ quote (Syntax.string_of_term_global thy (term_of ct))
32.13 + val _ = if null (Term.add_frees t []) then () else error ("Term "
32.14 + ^ quote (Syntax.string_of_term_global thy t)
32.15 ^ " to be evaluated contains free variables");
32.16 - fun eval' naming program ((vs, ty), t) deps =
32.17 + fun evaluator _ naming program ((_, ty), t) deps =
32.18 let
32.19 val _ = if Code_Thingol.contains_dictvar t then
32.20 error "Term to be evaluated contains free dictionaries" else ();
32.21 @@ -970,9 +970,7 @@
32.22 val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
32.23 ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
32.24 in ML_Context.evaluate ctxt false reff sml_code end;
32.25 - in eval'' thy (rpair eval') ct end;
32.26 -
32.27 -fun eval_term reff = eval Code_Thingol.eval_term I reff;
32.28 + in Code_Thingol.eval_term thy I evaluator t end;
32.29
32.30
32.31 (* instrumentalization by antiquotation *)
33.1 --- a/src/Tools/code/code_thingol.ML Thu Apr 16 17:29:56 2009 +0200
33.2 +++ b/src/Tools/code/code_thingol.ML Fri Apr 17 08:36:18 2009 +0200
33.3 @@ -84,10 +84,10 @@
33.4 val consts_program: theory -> string list -> string list * (naming * program)
33.5 val cached_program: theory -> naming * program
33.6 val eval_conv: theory
33.7 - -> (term -> term * (naming -> program -> typscheme * iterm -> string list -> thm))
33.8 + -> (term -> term) -> (term -> naming -> program -> typscheme * iterm -> string list -> thm)
33.9 -> cterm -> thm
33.10 val eval_term: theory
33.11 - -> (term -> term * (naming -> program -> typscheme * iterm -> string list -> 'a))
33.12 + -> (term -> term) -> (term -> naming -> program -> typscheme * iterm -> string list -> 'a)
33.13 -> term -> 'a
33.14 end;
33.15
33.16 @@ -459,7 +459,45 @@
33.17
33.18 (* translation *)
33.19
33.20 -fun ensure_class thy (algbr as (_, algebra)) funcgr class =
33.21 +fun ensure_tyco thy algbr funcgr tyco =
33.22 + let
33.23 + val stmt_datatype =
33.24 + let
33.25 + val (vs, cos) = Code.get_datatype thy tyco;
33.26 + in
33.27 + fold_map (translate_tyvar_sort thy algbr funcgr) vs
33.28 + ##>> fold_map (fn (c, tys) =>
33.29 + ensure_const thy algbr funcgr c
33.30 + ##>> fold_map (translate_typ thy algbr funcgr) tys) cos
33.31 + #>> (fn info => Datatype (tyco, info))
33.32 + end;
33.33 + in ensure_stmt lookup_tyco (declare_tyco thy) stmt_datatype tyco end
33.34 +and ensure_const thy algbr funcgr c =
33.35 + let
33.36 + fun stmt_datatypecons tyco =
33.37 + ensure_tyco thy algbr funcgr tyco
33.38 + #>> (fn tyco => Datatypecons (c, tyco));
33.39 + fun stmt_classparam class =
33.40 + ensure_class thy algbr funcgr class
33.41 + #>> (fn class => Classparam (c, class));
33.42 + fun stmt_fun ((vs, ty), raw_thms) =
33.43 + let
33.44 + val thms = if null (Term.add_tfreesT ty []) orelse (null o fst o strip_type) ty
33.45 + then raw_thms
33.46 + else (map o apfst) (Code_Unit.expand_eta thy 1) raw_thms;
33.47 + in
33.48 + fold_map (translate_tyvar_sort thy algbr funcgr) vs
33.49 + ##>> translate_typ thy algbr funcgr ty
33.50 + ##>> fold_map (translate_eq thy algbr funcgr) thms
33.51 + #>> (fn info => Fun (c, info))
33.52 + end;
33.53 + val stmt_const = case Code.get_datatype_of_constr thy c
33.54 + of SOME tyco => stmt_datatypecons tyco
33.55 + | NONE => (case AxClass.class_of_param thy c
33.56 + of SOME class => stmt_classparam class
33.57 + | NONE => stmt_fun (Code_Wellsorted.typ funcgr c, Code_Wellsorted.eqns funcgr c))
33.58 + in ensure_stmt lookup_const (declare_const thy) stmt_const c end
33.59 +and ensure_class thy (algbr as (_, algebra)) funcgr class =
33.60 let
33.61 val superclasses = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
33.62 val cs = #params (AxClass.get_info thy class);
33.63 @@ -477,65 +515,6 @@
33.64 ##>> ensure_class thy algbr funcgr superclass
33.65 #>> Classrel;
33.66 in ensure_stmt lookup_classrel (declare_classrel thy) stmt_classrel (subclass, superclass) end
33.67 -and ensure_tyco thy algbr funcgr tyco =
33.68 - let
33.69 - val stmt_datatype =
33.70 - let
33.71 - val (vs, cos) = Code.get_datatype thy tyco;
33.72 - in
33.73 - fold_map (translate_tyvar_sort thy algbr funcgr) vs
33.74 - ##>> fold_map (fn (c, tys) =>
33.75 - ensure_const thy algbr funcgr c
33.76 - ##>> fold_map (translate_typ thy algbr funcgr) tys) cos
33.77 - #>> (fn info => Datatype (tyco, info))
33.78 - end;
33.79 - in ensure_stmt lookup_tyco (declare_tyco thy) stmt_datatype tyco end
33.80 -and translate_tyvar_sort thy (algbr as (proj_sort, _)) funcgr (v, sort) =
33.81 - fold_map (ensure_class thy algbr funcgr) (proj_sort sort)
33.82 - #>> (fn sort => (unprefix "'" v, sort))
33.83 -and translate_typ thy algbr funcgr (TFree (v, _)) =
33.84 - pair (ITyVar (unprefix "'" v))
33.85 - | translate_typ thy algbr funcgr (Type (tyco, tys)) =
33.86 - ensure_tyco thy algbr funcgr tyco
33.87 - ##>> fold_map (translate_typ thy algbr funcgr) tys
33.88 - #>> (fn (tyco, tys) => tyco `%% tys)
33.89 -and translate_dicts thy (algbr as (proj_sort, algebra)) funcgr thm (ty, sort) =
33.90 - let
33.91 - val pp = Syntax.pp_global thy;
33.92 - datatype typarg =
33.93 - Global of (class * string) * typarg list list
33.94 - | Local of (class * class) list * (string * (int * sort));
33.95 - fun class_relation (Global ((_, tyco), yss), _) class =
33.96 - Global ((class, tyco), yss)
33.97 - | class_relation (Local (classrels, v), subclass) superclass =
33.98 - Local ((subclass, superclass) :: classrels, v);
33.99 - fun type_constructor tyco yss class =
33.100 - Global ((class, tyco), (map o map) fst yss);
33.101 - fun type_variable (TFree (v, sort)) =
33.102 - let
33.103 - val sort' = proj_sort sort;
33.104 - in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
33.105 - val typargs = Sorts.of_sort_derivation pp algebra
33.106 - {class_relation = class_relation, type_constructor = type_constructor,
33.107 - type_variable = type_variable} (ty, proj_sort sort)
33.108 - handle Sorts.CLASS_ERROR e => not_wellsorted thy thm ty sort e;
33.109 - fun mk_dict (Global (inst, yss)) =
33.110 - ensure_inst thy algbr funcgr inst
33.111 - ##>> (fold_map o fold_map) mk_dict yss
33.112 - #>> (fn (inst, dss) => DictConst (inst, dss))
33.113 - | mk_dict (Local (classrels, (v, (k, sort)))) =
33.114 - fold_map (ensure_classrel thy algbr funcgr) classrels
33.115 - #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort))))
33.116 - in fold_map mk_dict typargs end
33.117 -and translate_eq thy algbr funcgr (thm, linear) =
33.118 - let
33.119 - val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
33.120 - o Logic.unvarify o prop_of) thm;
33.121 - in
33.122 - fold_map (translate_term thy algbr funcgr (SOME thm)) args
33.123 - ##>> translate_term thy algbr funcgr (SOME thm) rhs
33.124 - #>> rpair (thm, linear)
33.125 - end
33.126 and ensure_inst thy (algbr as (_, algebra)) funcgr (class, tyco) =
33.127 let
33.128 val superclasses = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
33.129 @@ -572,31 +551,12 @@
33.130 #>> (fn ((((class, tyco), arity), superarities), classparams) =>
33.131 Classinst ((class, (tyco, arity)), (superarities, classparams)));
33.132 in ensure_stmt lookup_instance (declare_instance thy) stmt_inst (class, tyco) end
33.133 -and ensure_const thy algbr funcgr c =
33.134 - let
33.135 - fun stmt_datatypecons tyco =
33.136 +and translate_typ thy algbr funcgr (TFree (v, _)) =
33.137 + pair (ITyVar (unprefix "'" v))
33.138 + | translate_typ thy algbr funcgr (Type (tyco, tys)) =
33.139 ensure_tyco thy algbr funcgr tyco
33.140 - #>> (fn tyco => Datatypecons (c, tyco));
33.141 - fun stmt_classparam class =
33.142 - ensure_class thy algbr funcgr class
33.143 - #>> (fn class => Classparam (c, class));
33.144 - fun stmt_fun ((vs, ty), raw_thms) =
33.145 - let
33.146 - val thms = if null (Term.add_tfreesT ty []) orelse (null o fst o strip_type) ty
33.147 - then raw_thms
33.148 - else (map o apfst) (Code_Unit.expand_eta thy 1) raw_thms;
33.149 - in
33.150 - fold_map (translate_tyvar_sort thy algbr funcgr) vs
33.151 - ##>> translate_typ thy algbr funcgr ty
33.152 - ##>> fold_map (translate_eq thy algbr funcgr) thms
33.153 - #>> (fn info => Fun (c, info))
33.154 - end;
33.155 - val stmt_const = case Code.get_datatype_of_constr thy c
33.156 - of SOME tyco => stmt_datatypecons tyco
33.157 - | NONE => (case AxClass.class_of_param thy c
33.158 - of SOME class => stmt_classparam class
33.159 - | NONE => stmt_fun (Code_Wellsorted.typ funcgr c, Code_Wellsorted.eqns funcgr c))
33.160 - in ensure_stmt lookup_const (declare_const thy) stmt_const c end
33.161 + ##>> fold_map (translate_typ thy algbr funcgr) tys
33.162 + #>> (fn (tyco, tys) => tyco `%% tys)
33.163 and translate_term thy algbr funcgr thm (Const (c, ty)) =
33.164 translate_app thy algbr funcgr thm ((c, ty), [])
33.165 | translate_term thy algbr funcgr thm (Free (v, _)) =
33.166 @@ -617,6 +577,15 @@
33.167 translate_term thy algbr funcgr thm t'
33.168 ##>> fold_map (translate_term thy algbr funcgr thm) ts
33.169 #>> (fn (t, ts) => t `$$ ts)
33.170 +and translate_eq thy algbr funcgr (thm, linear) =
33.171 + let
33.172 + val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
33.173 + o Logic.unvarify o prop_of) thm;
33.174 + in
33.175 + fold_map (translate_term thy algbr funcgr (SOME thm)) args
33.176 + ##>> translate_term thy algbr funcgr (SOME thm) rhs
33.177 + #>> rpair (thm, linear)
33.178 + end
33.179 and translate_const thy algbr funcgr thm (c, ty) =
33.180 let
33.181 val tys = Sign.const_typargs thy (c, ty);
33.182 @@ -695,7 +664,38 @@
33.183 and translate_app thy algbr funcgr thm (c_ty_ts as ((c, _), _)) =
33.184 case Code.get_case_scheme thy c
33.185 of SOME case_scheme => translate_app_case thy algbr funcgr thm case_scheme c_ty_ts
33.186 - | NONE => translate_app_const thy algbr funcgr thm c_ty_ts;
33.187 + | NONE => translate_app_const thy algbr funcgr thm c_ty_ts
33.188 +and translate_tyvar_sort thy (algbr as (proj_sort, _)) funcgr (v, sort) =
33.189 + fold_map (ensure_class thy algbr funcgr) (proj_sort sort)
33.190 + #>> (fn sort => (unprefix "'" v, sort))
33.191 +and translate_dicts thy (algbr as (proj_sort, algebra)) funcgr thm (ty, sort) =
33.192 + let
33.193 + val pp = Syntax.pp_global thy;
33.194 + datatype typarg =
33.195 + Global of (class * string) * typarg list list
33.196 + | Local of (class * class) list * (string * (int * sort));
33.197 + fun class_relation (Global ((_, tyco), yss), _) class =
33.198 + Global ((class, tyco), yss)
33.199 + | class_relation (Local (classrels, v), subclass) superclass =
33.200 + Local ((subclass, superclass) :: classrels, v);
33.201 + fun type_constructor tyco yss class =
33.202 + Global ((class, tyco), (map o map) fst yss);
33.203 + fun type_variable (TFree (v, sort)) =
33.204 + let
33.205 + val sort' = proj_sort sort;
33.206 + in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
33.207 + val typargs = Sorts.of_sort_derivation pp algebra
33.208 + {class_relation = class_relation, type_constructor = type_constructor,
33.209 + type_variable = type_variable} (ty, proj_sort sort)
33.210 + handle Sorts.CLASS_ERROR e => not_wellsorted thy thm ty sort e;
33.211 + fun mk_dict (Global (inst, yss)) =
33.212 + ensure_inst thy algbr funcgr inst
33.213 + ##>> (fold_map o fold_map) mk_dict yss
33.214 + #>> (fn (inst, dss) => DictConst (inst, dss))
33.215 + | mk_dict (Local (classrels, (v, (k, sort)))) =
33.216 + fold_map (ensure_classrel thy algbr funcgr) classrels
33.217 + #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort))))
33.218 + in fold_map mk_dict typargs end;
33.219
33.220
33.221 (* store *)
33.222 @@ -733,14 +733,14 @@
33.223 fun generate_consts thy algebra funcgr =
33.224 fold_map (ensure_const thy algebra funcgr);
33.225 in
33.226 - invoke_generation thy (Code_Wellsorted.make thy cs) generate_consts cs
33.227 + invoke_generation thy (Code_Wellsorted.obtain thy cs []) generate_consts cs
33.228 |-> project_consts
33.229 end;
33.230
33.231
33.232 (* value evaluation *)
33.233
33.234 -fun ensure_value thy algbr funcgr t =
33.235 +fun ensure_value thy algbr funcgr t =
33.236 let
33.237 val ty = fastype_of t;
33.238 val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
33.239 @@ -766,18 +766,72 @@
33.240 #> term_value
33.241 end;
33.242
33.243 -fun eval thy evaluator t =
33.244 +fun eval thy evaluator raw_t algebra funcgr t =
33.245 let
33.246 - val (t', evaluator'') = evaluator t;
33.247 - fun evaluator' algebra funcgr =
33.248 - let
33.249 - val (((naming, program), (vs_ty_t, deps)), _) =
33.250 - invoke_generation thy (algebra, funcgr) ensure_value t';
33.251 - in evaluator'' naming program vs_ty_t deps end;
33.252 - in (t', evaluator') end
33.253 + val (((naming, program), (vs_ty_t, deps)), _) =
33.254 + invoke_generation thy (algebra, funcgr) ensure_value t;
33.255 + in evaluator raw_t naming program vs_ty_t deps end;
33.256
33.257 -fun eval_conv thy = Code_Wellsorted.eval_conv thy o eval thy;
33.258 -fun eval_term thy = Code_Wellsorted.eval_term thy o eval thy;
33.259 +fun eval_conv thy preproc = Code_Wellsorted.eval_conv thy preproc o eval thy;
33.260 +fun eval_term thy preproc = Code_Wellsorted.eval_term thy preproc o eval thy;
33.261 +
33.262 +
33.263 +(** diagnostic commands **)
33.264 +
33.265 +fun code_depgr thy consts =
33.266 + let
33.267 + val (_, eqngr) = Code_Wellsorted.obtain thy consts [];
33.268 + val select = Graph.all_succs eqngr consts;
33.269 + in
33.270 + eqngr
33.271 + |> not (null consts) ? Graph.subgraph (member (op =) select)
33.272 + |> Graph.map_nodes ((apsnd o map o apfst) (AxClass.overload thy))
33.273 + end;
33.274 +
33.275 +fun code_thms thy = Pretty.writeln o Code_Wellsorted.pretty thy o code_depgr thy;
33.276 +
33.277 +fun code_deps thy consts =
33.278 + let
33.279 + val eqngr = code_depgr thy consts;
33.280 + val constss = Graph.strong_conn eqngr;
33.281 + val mapping = Symtab.empty |> fold (fn consts => fold (fn const =>
33.282 + Symtab.update (const, consts)) consts) constss;
33.283 + fun succs consts = consts
33.284 + |> maps (Graph.imm_succs eqngr)
33.285 + |> subtract (op =) consts
33.286 + |> map (the o Symtab.lookup mapping)
33.287 + |> distinct (op =);
33.288 + val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss;
33.289 + fun namify consts = map (Code_Unit.string_of_const thy) consts
33.290 + |> commas;
33.291 + val prgr = map (fn (consts, constss) =>
33.292 + { name = namify consts, ID = namify consts, dir = "", unfold = true,
33.293 + path = "", parents = map namify constss }) conn;
33.294 + in Present.display_graph prgr end;
33.295 +
33.296 +local
33.297 +
33.298 +structure P = OuterParse
33.299 +and K = OuterKeyword
33.300 +
33.301 +fun code_thms_cmd thy = code_thms thy o op @ o Code_Name.read_const_exprs thy;
33.302 +fun code_deps_cmd thy = code_deps thy o op @ o Code_Name.read_const_exprs thy;
33.303 +
33.304 +in
33.305 +
33.306 +val _ =
33.307 + OuterSyntax.improper_command "code_thms" "print system of code equations for code" OuterKeyword.diag
33.308 + (Scan.repeat P.term_group
33.309 + >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
33.310 + o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
33.311 +
33.312 +val _ =
33.313 + OuterSyntax.improper_command "code_deps" "visualize dependencies of code equations for code" OuterKeyword.diag
33.314 + (Scan.repeat P.term_group
33.315 + >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
33.316 + o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
33.317 +
33.318 +end;
33.319
33.320 end; (*struct*)
33.321
34.1 --- a/src/Tools/code/code_wellsorted.ML Thu Apr 16 17:29:56 2009 +0200
34.2 +++ b/src/Tools/code/code_wellsorted.ML Fri Apr 17 08:36:18 2009 +0200
34.3 @@ -12,12 +12,13 @@
34.4 val typ: T -> string -> (string * sort) list * typ
34.5 val all: T -> string list
34.6 val pretty: theory -> T -> Pretty.T
34.7 - val make: theory -> string list
34.8 - -> ((sort -> sort) * Sorts.algebra) * T
34.9 + val obtain: theory -> string list -> term list -> ((sort -> sort) * Sorts.algebra) * T
34.10 + val preprocess: theory -> cterm list -> (cterm * (thm -> thm)) list
34.11 + val preprocess_term: theory -> term list -> (term * (term -> term)) list
34.12 val eval_conv: theory
34.13 - -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> thm)) -> cterm -> thm
34.14 + -> (term -> term) -> (term -> (sort -> sort) * Sorts.algebra -> T -> term -> thm) -> cterm -> thm
34.15 val eval_term: theory
34.16 - -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> 'a)) -> term -> 'a
34.17 + -> (term -> term) -> (term -> (sort -> sort) * Sorts.algebra -> T -> term -> 'a) -> term -> 'a
34.18 end
34.19
34.20 structure Code_Wellsorted : CODE_WELLSORTED =
34.21 @@ -47,8 +48,10 @@
34.22
34.23 (* auxiliary *)
34.24
34.25 +fun is_proper_class thy = can (AxClass.get_info thy);
34.26 +
34.27 fun complete_proper_sort thy =
34.28 - Sign.complete_sort thy #> filter (can (AxClass.get_info thy));
34.29 + Sign.complete_sort thy #> filter (is_proper_class thy);
34.30
34.31 fun inst_params thy tyco =
34.32 map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
34.33 @@ -232,8 +235,7 @@
34.34 ((class, tyco), map (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k))
34.35 (0 upto Sign.arity_number thy tyco - 1));
34.36
34.37 -fun add_eqs thy (proj_sort, algebra) vardeps
34.38 - (c, (proto_lhs, proto_eqns)) (rhss, eqngr) =
34.39 +fun add_eqs thy vardeps (c, (proto_lhs, proto_eqns)) (rhss, eqngr) =
34.40 if can (Graph.get_node eqngr) c then (rhss, eqngr)
34.41 else let
34.42 val lhs = map_index (fn (k, (v, _)) =>
34.43 @@ -246,68 +248,26 @@
34.44 val eqngr' = Graph.new_node (c, (tyscm, eqns)) eqngr;
34.45 in (map (pair c) rhss' @ rhss, eqngr') end;
34.46
34.47 -fun extend_arities_eqngr thy cs cs_rhss (arities, eqngr) =
34.48 +fun extend_arities_eqngr thy cs ts (arities, eqngr) =
34.49 let
34.50 - val cs_rhss' = (map o apsnd o map) (styp_of NONE) cs_rhss;
34.51 + val cs_rhss = (fold o fold_aterms) (fn Const (c_ty as (c, _)) =>
34.52 + insert (op =) (c, (map (styp_of NONE) o Sign.const_typargs thy) c_ty) | _ => I) ts [];
34.53 val (vardeps, (eqntab, insts)) = empty_vardeps_data
34.54 |> fold (assert_fun thy arities eqngr) cs
34.55 - |> fold (assert_rhs thy arities eqngr) cs_rhss';
34.56 + |> fold (assert_rhs thy arities eqngr) cs_rhss;
34.57 val arities' = fold (add_arity thy vardeps) insts arities;
34.58 val pp = Syntax.pp_global thy;
34.59 - val is_proper_class = can (AxClass.get_info thy);
34.60 - val (proj_sort, algebra) = Sorts.subalgebra pp is_proper_class
34.61 + val algebra = Sorts.subalgebra pp (is_proper_class thy)
34.62 (AList.lookup (op =) arities') (Sign.classes_of thy);
34.63 - val (rhss, eqngr') = Symtab.fold
34.64 - (add_eqs thy (proj_sort, algebra) vardeps) eqntab ([], eqngr);
34.65 - fun deps_of (c, rhs) = c ::
34.66 - maps (dicts_of thy (proj_sort, algebra))
34.67 - (rhs ~~ (map snd o fst o fst o Graph.get_node eqngr') c);
34.68 + val (rhss, eqngr') = Symtab.fold (add_eqs thy vardeps) eqntab ([], eqngr);
34.69 + fun deps_of (c, rhs) = c :: maps (dicts_of thy algebra)
34.70 + (rhs ~~ (map snd o fst o fst o Graph.get_node eqngr') c);
34.71 val eqngr'' = fold (fn (c, rhs) => fold
34.72 (curry Graph.add_edge c) (deps_of rhs)) rhss eqngr';
34.73 - in ((proj_sort, algebra), (arities', eqngr'')) end;
34.74 + in (algebra, (arities', eqngr'')) end;
34.75
34.76
34.77 -(** retrieval interfaces **)
34.78 -
34.79 -fun proto_eval thy cterm_of evaluator_lift evaluator proto_ct arities_eqngr =
34.80 - let
34.81 - val ct = cterm_of proto_ct;
34.82 - val _ = Sign.no_vars (Syntax.pp_global thy) (Thm.term_of ct);
34.83 - val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) ();
34.84 - fun consts_of t =
34.85 - fold_aterms (fn Const c_ty => cons c_ty | _ => I) t [];
34.86 - val thm = Code.preprocess_conv thy ct;
34.87 - val ct' = Thm.rhs_of thm;
34.88 - val t' = Thm.term_of ct';
34.89 - val (t'', evaluator_eqngr) = evaluator t';
34.90 - val consts = map fst (consts_of t');
34.91 - val consts' = consts_of t'';
34.92 - val const_matches' = fold (fn (c, ty) =>
34.93 - insert (op =) (c, Sign.const_typargs thy (c, ty))) consts' [];
34.94 - val (algebra', arities_eqngr') =
34.95 - extend_arities_eqngr thy consts const_matches' arities_eqngr;
34.96 - in
34.97 - (evaluator_lift (evaluator_eqngr algebra') thm (snd arities_eqngr'),
34.98 - arities_eqngr')
34.99 - end;
34.100 -
34.101 -fun proto_eval_conv thy =
34.102 - let
34.103 - fun evaluator_lift evaluator thm1 eqngr =
34.104 - let
34.105 - val thm2 = evaluator eqngr;
34.106 - val thm3 = Code.postprocess_conv thy (Thm.rhs_of thm2);
34.107 - in
34.108 - Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
34.109 - error ("could not construct evaluation proof:\n"
34.110 - ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3])
34.111 - end;
34.112 - in proto_eval thy I evaluator_lift end;
34.113 -
34.114 -fun proto_eval_term thy =
34.115 - let
34.116 - fun evaluator_lift evaluator _ eqngr = evaluator eqngr;
34.117 - in proto_eval thy (Thm.cterm_of thy) evaluator_lift end;
34.118 +(** store **)
34.119
34.120 structure Wellsorted = CodeDataFun
34.121 (
34.122 @@ -327,71 +287,62 @@
34.123 in (arities', eqngr') end;
34.124 );
34.125
34.126 -fun make thy cs = apsnd snd
34.127 - (Wellsorted.change_yield thy (extend_arities_eqngr thy cs []));
34.128
34.129 -fun eval_conv thy f =
34.130 - fst o Wellsorted.change_yield thy o proto_eval_conv thy f;
34.131 +(** retrieval interfaces **)
34.132
34.133 -fun eval_term thy f =
34.134 - fst o Wellsorted.change_yield thy o proto_eval_term thy f;
34.135 +fun obtain thy cs ts = apsnd snd
34.136 + (Wellsorted.change_yield thy (extend_arities_eqngr thy cs ts));
34.137
34.138 +fun preprocess thy cts =
34.139 + let
34.140 + val ts = map Thm.term_of cts;
34.141 + val _ = map
34.142 + (Sign.no_vars (Syntax.pp_global thy) o Term.map_types Type.no_tvars) ts;
34.143 + fun make thm1 = (Thm.rhs_of thm1, fn thm2 =>
34.144 + let
34.145 + val thm3 = Code.postprocess_conv thy (Thm.rhs_of thm2);
34.146 + in
34.147 + Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
34.148 + error ("could not construct evaluation proof:\n"
34.149 + ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3])
34.150 + end);
34.151 + in map (make o Code.preprocess_conv thy) cts end;
34.152
34.153 -(** diagnostic commands **)
34.154 +fun preprocess_term thy ts =
34.155 + let
34.156 + val cts = map (Thm.cterm_of thy) ts;
34.157 + val postprocess = Code.postprocess_term thy;
34.158 + in map (fn (ct, _) => (Thm.term_of ct, postprocess)) (preprocess thy cts) end;
34.159
34.160 -fun code_depgr thy consts =
34.161 +(*FIXME rearrange here*)
34.162 +
34.163 +fun proto_eval thy cterm_of evaluator_lift preproc evaluator proto_ct =
34.164 let
34.165 - val (_, eqngr) = make thy consts;
34.166 - val select = Graph.all_succs eqngr consts;
34.167 - in
34.168 - eqngr
34.169 - |> not (null consts) ? Graph.subgraph (member (op =) select)
34.170 - |> Graph.map_nodes ((apsnd o map o apfst) (AxClass.overload thy))
34.171 - end;
34.172 + val ct = cterm_of proto_ct;
34.173 + val _ = Sign.no_vars (Syntax.pp_global thy) (Thm.term_of ct);
34.174 + val _ = Term.map_types Type.no_tvars (Thm.term_of ct);
34.175 + fun consts_of t =
34.176 + fold_aterms (fn Const c_ty => cons c_ty | _ => I) t [];
34.177 + val thm = Code.preprocess_conv thy ct;
34.178 + val ct' = Thm.rhs_of thm;
34.179 + val t' = Thm.term_of ct';
34.180 + val consts = map fst (consts_of t');
34.181 + val t'' = preproc t';
34.182 + val (algebra', eqngr') = obtain thy consts [t''];
34.183 + in evaluator_lift (evaluator t' algebra' eqngr' t'') thm end;
34.184
34.185 -fun code_thms thy = Pretty.writeln o pretty thy o code_depgr thy;
34.186 +fun eval_conv thy =
34.187 + let
34.188 + fun evaluator_lift thm2 thm1 =
34.189 + let
34.190 + val thm3 = Code.postprocess_conv thy (Thm.rhs_of thm2);
34.191 + in
34.192 + Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
34.193 + error ("could not construct evaluation proof:\n"
34.194 + ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3])
34.195 + end;
34.196 + in proto_eval thy I evaluator_lift end;
34.197
34.198 -fun code_deps thy consts =
34.199 - let
34.200 - val eqngr = code_depgr thy consts;
34.201 - val constss = Graph.strong_conn eqngr;
34.202 - val mapping = Symtab.empty |> fold (fn consts => fold (fn const =>
34.203 - Symtab.update (const, consts)) consts) constss;
34.204 - fun succs consts = consts
34.205 - |> maps (Graph.imm_succs eqngr)
34.206 - |> subtract (op =) consts
34.207 - |> map (the o Symtab.lookup mapping)
34.208 - |> distinct (op =);
34.209 - val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss;
34.210 - fun namify consts = map (Code_Unit.string_of_const thy) consts
34.211 - |> commas;
34.212 - val prgr = map (fn (consts, constss) =>
34.213 - { name = namify consts, ID = namify consts, dir = "", unfold = true,
34.214 - path = "", parents = map namify constss }) conn;
34.215 - in Present.display_graph prgr end;
34.216 -
34.217 -local
34.218 -
34.219 -structure P = OuterParse
34.220 -and K = OuterKeyword
34.221 -
34.222 -fun code_thms_cmd thy = code_thms thy o op @ o Code_Name.read_const_exprs thy;
34.223 -fun code_deps_cmd thy = code_deps thy o op @ o Code_Name.read_const_exprs thy;
34.224 -
34.225 -in
34.226 -
34.227 -val _ =
34.228 - OuterSyntax.improper_command "code_thms" "print system of code equations for code" OuterKeyword.diag
34.229 - (Scan.repeat P.term_group
34.230 - >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
34.231 - o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
34.232 -
34.233 -val _ =
34.234 - OuterSyntax.improper_command "code_deps" "visualize dependencies of code equations for code" OuterKeyword.diag
34.235 - (Scan.repeat P.term_group
34.236 - >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
34.237 - o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
34.238 -
34.239 -end;
34.240 +fun eval_term thy = proto_eval thy (Thm.cterm_of thy) (fn t => K t);
34.241
34.242 end; (*struct*)
35.1 --- a/src/Tools/nbe.ML Thu Apr 16 17:29:56 2009 +0200
35.2 +++ b/src/Tools/nbe.ML Fri Apr 17 08:36:18 2009 +0200
35.3 @@ -431,7 +431,7 @@
35.4
35.5 (* evaluation with type reconstruction *)
35.6
35.7 -fun eval thy t naming program vs_ty_t deps =
35.8 +fun norm thy t naming program vs_ty_t deps =
35.9 let
35.10 fun subst_const f = map_aterms (fn t as Term.Const (c, ty) => Term.Const (f c, ty)
35.11 | t => t);
35.12 @@ -463,10 +463,6 @@
35.13
35.14 (* evaluation oracle *)
35.15
35.16 -val (_, norm_oracle) = Context.>>> (Context.map_theory_result
35.17 - (Thm.add_oracle (Binding.name "norm", fn (thy, t, naming, program, vs_ty_t, deps) =>
35.18 - Thm.cterm_of thy (Logic.mk_equals (t, eval thy t naming program vs_ty_t deps)))));
35.19 -
35.20 fun add_triv_classes thy =
35.21 let
35.22 val inters = curry (Sorts.inter_sort (Sign.classes_of thy))
35.23 @@ -476,19 +472,20 @@
35.24 | TFree (v, sort) => TFree (v, f sort));
35.25 in map_sorts inters end;
35.26
35.27 +val (_, raw_norm_oracle) = Context.>>> (Context.map_theory_result
35.28 + (Thm.add_oracle (Binding.name "norm", fn (thy, t, naming, program, vs_ty_t, deps) =>
35.29 + Thm.cterm_of thy (Logic.mk_equals (t, norm thy t naming program vs_ty_t deps)))));
35.30 +
35.31 +fun norm_oracle thy t naming program vs_ty_t deps =
35.32 + raw_norm_oracle (thy, t, naming, program, vs_ty_t, deps);
35.33 +
35.34 fun norm_conv ct =
35.35 let
35.36 val thy = Thm.theory_of_cterm ct;
35.37 - fun evaluator' t naming program vs_ty_t deps =
35.38 - norm_oracle (thy, t, naming, program, vs_ty_t, deps);
35.39 - fun evaluator t = (add_triv_classes thy t, evaluator' t);
35.40 - in Code_Thingol.eval_conv thy evaluator ct end;
35.41 + in Code_Thingol.eval_conv thy (add_triv_classes thy) (norm_oracle thy) ct end;
35.42
35.43 -fun norm_term thy t =
35.44 - let
35.45 - fun evaluator' t naming program vs_ty_t deps = eval thy t naming program vs_ty_t deps;
35.46 - fun evaluator t = (add_triv_classes thy t, evaluator' t);
35.47 - in (Code.postprocess_term thy o Code_Thingol.eval_term thy evaluator) t end;
35.48 +fun norm_term thy = Code.postprocess_term thy
35.49 + o Code_Thingol.eval_term thy (add_triv_classes thy) (norm thy);
35.50
35.51 (* evaluation command *)
35.52