--- a/NEWS Thu Apr 16 17:29:56 2009 +0200
+++ b/NEWS Fri Apr 17 08:36:18 2009 +0200
@@ -1,6 +1,14 @@
Isabelle NEWS -- history user-relevant changes
==============================================
+*** HOL ***
+
+* Class semiring_div now requires no_zero_divisors and proof of div_mult_mult1;
+theorems div_mult_mult1, div_mult_mult2, div_mult_mult1_if, div_mult_mult1 and
+div_mult_mult2 have been generalized to class semiring_div, subsuming former
+theorems zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and zdiv_zmult_zmult2.
+div_mult_mult1 is now [simp] by default. INCOMPATIBILITY.
+
New in Isabelle2009 (April 2009)
--------------------------------
--- a/doc-src/Codegen/Thy/Program.thy Thu Apr 16 17:29:56 2009 +0200
+++ b/doc-src/Codegen/Thy/Program.thy Fri Apr 17 08:36:18 2009 +0200
@@ -323,7 +323,7 @@
*}
-subsection {* Equality and wellsortedness *}
+subsection {* Equality *}
text {*
Surely you have already noticed how equality is treated
@@ -358,60 +358,7 @@
manually like any other type class.
Though this @{text eq} class is designed to get rarely in
- the way, a subtlety
- enters the stage when definitions of overloaded constants
- are dependent on operational equality. For example, let
- us define a lexicographic ordering on tuples
- (also see theory @{theory Product_ord}):
-*}
-
-instantiation %quote "*" :: (order, order) order
-begin
-
-definition %quote [code del]:
- "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x \<le> snd y"
-
-definition %quote [code del]:
- "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"
-
-instance %quote proof
-qed (auto simp: less_eq_prod_def less_prod_def intro: order_less_trans)
-
-end %quote
-
-lemma %quote order_prod [code]:
- "(x1 \<Colon> 'a\<Colon>order, y1 \<Colon> 'b\<Colon>order) < (x2, y2) \<longleftrightarrow>
- x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
- "(x1 \<Colon> 'a\<Colon>order, y1 \<Colon> 'b\<Colon>order) \<le> (x2, y2) \<longleftrightarrow>
- x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
- by (simp_all add: less_prod_def less_eq_prod_def)
-
-text {*
- \noindent Then code generation will fail. Why? The definition
- of @{term "op \<le>"} depends on equality on both arguments,
- which are polymorphic and impose an additional @{class eq}
- class constraint, which the preprocessor does not propagate
- (for technical reasons).
-
- The solution is to add @{class eq} explicitly to the first sort arguments in the
- code theorems:
-*}
-
-lemma %quote order_prod_code [code]:
- "(x1 \<Colon> 'a\<Colon>{order, eq}, y1 \<Colon> 'b\<Colon>order) < (x2, y2) \<longleftrightarrow>
- x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
- "(x1 \<Colon> 'a\<Colon>{order, eq}, y1 \<Colon> 'b\<Colon>order) \<le> (x2, y2) \<longleftrightarrow>
- x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
- by (simp_all add: less_prod_def less_eq_prod_def)
-
-text {*
- \noindent Then code generation succeeds:
-*}
-
-text %quote {*@{code_stmts "op \<le> \<Colon> _ \<times> _ \<Rightarrow> _ \<times> _ \<Rightarrow> bool" (SML)}*}
-
-text {*
- In some cases, the automatically derived code equations
+ the way, in some cases the automatically derived code equations
for equality on a particular type may not be appropriate.
As example, watch the following datatype representing
monomorphic parametric types (where type constructors
--- a/doc-src/Codegen/Thy/document/Program.tex Thu Apr 16 17:29:56 2009 +0200
+++ b/doc-src/Codegen/Thy/document/Program.tex Fri Apr 17 08:36:18 2009 +0200
@@ -714,7 +714,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Equality and wellsortedness%
+\isamarkupsubsection{Equality%
}
\isamarkuptrue%
%
@@ -801,141 +801,7 @@
manually like any other type class.
Though this \isa{eq} class is designed to get rarely in
- the way, a subtlety
- enters the stage when definitions of overloaded constants
- are dependent on operational equality. For example, let
- us define a lexicographic ordering on tuples
- (also see theory \hyperlink{theory.Product-ord}{\mbox{\isa{Product{\isacharunderscore}ord}}}):%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{instantiation}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}order{\isacharcomma}\ order{\isacharparenright}\ order\isanewline
-\isakeyword{begin}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ {\isacharbrackleft}code\ del{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}x\ {\isasymle}\ y\ {\isasymlongleftrightarrow}\ fst\ x\ {\isacharless}\ fst\ y\ {\isasymor}\ fst\ x\ {\isacharequal}\ fst\ y\ {\isasymand}\ snd\ x\ {\isasymle}\ snd\ y{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ {\isacharbrackleft}code\ del{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}x\ {\isacharless}\ y\ {\isasymlongleftrightarrow}\ fst\ x\ {\isacharless}\ fst\ y\ {\isasymor}\ fst\ x\ {\isacharequal}\ fst\ y\ {\isasymand}\ snd\ x\ {\isacharless}\ snd\ y{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{instance}\isamarkupfalse%
-\ \isacommand{proof}\isamarkupfalse%
-\isanewline
-\isacommand{qed}\isamarkupfalse%
-\ {\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
-\isanewline
-\isacommand{end}\isamarkupfalse%
-\isanewline
-\isanewline
-\isacommand{lemma}\isamarkupfalse%
-\ order{\isacharunderscore}prod\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\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
-\ \ \ \ \ 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
-\ \ {\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
-\ \ \ \ \ 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
-\ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent Then code generation will fail. Why? The definition
- of \isa{op\ {\isasymle}} depends on equality on both arguments,
- which are polymorphic and impose an additional \isa{eq}
- class constraint, which the preprocessor does not propagate
- (for technical reasons).
-
- The solution is to add \isa{eq} explicitly to the first sort arguments in the
- code theorems:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{lemma}\isamarkupfalse%
-\ order{\isacharunderscore}prod{\isacharunderscore}code\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\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
-\ \ \ \ \ 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
-\ \ {\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
-\ \ \ \ \ 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
-\ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent Then code generation succeeds:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-%
-\begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}structure Example = \\
-\hspace*{0pt}struct\\
-\hspace*{0pt}\\
-\hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\
-\hspace*{0pt}fun eq (A{\char95}:'a eq) = {\char35}eq A{\char95};\\
-\hspace*{0pt}\\
-\hspace*{0pt}type 'a ord = {\char123}less{\char95}eq :~'a -> 'a -> bool,~less :~'a -> 'a -> bool{\char125};\\
-\hspace*{0pt}fun less{\char95}eq (A{\char95}:'a ord) = {\char35}less{\char95}eq A{\char95};\\
-\hspace*{0pt}fun less (A{\char95}:'a ord) = {\char35}less A{\char95};\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun eqop A{\char95}~a b = eq A{\char95}~a b;\\
-\hspace*{0pt}\\
-\hspace*{0pt}type 'a preorder = {\char123}Orderings{\char95}{\char95}ord{\char95}preorder :~'a ord{\char125};\\
-\hspace*{0pt}fun ord{\char95}preorder (A{\char95}:'a preorder) = {\char35}Orderings{\char95}{\char95}ord{\char95}preorder A{\char95};\\
-\hspace*{0pt}\\
-\hspace*{0pt}type 'a order = {\char123}Orderings{\char95}{\char95}preorder{\char95}order :~'a preorder{\char125};\\
-\hspace*{0pt}fun preorder{\char95}order (A{\char95}:'a order) = {\char35}Orderings{\char95}{\char95}preorder{\char95}order A{\char95};\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun less{\char95}eqa (A1{\char95},~A2{\char95}) B{\char95}~(x1,~y1) (x2,~y2) =\\
-\hspace*{0pt} ~less ((ord{\char95}preorder o preorder{\char95}order) A2{\char95}) x1 x2 orelse\\
-\hspace*{0pt} ~~~eqop A1{\char95}~x1 x2 andalso\\
-\hspace*{0pt} ~~~~~less{\char95}eq ((ord{\char95}preorder o preorder{\char95}order) B{\char95}) y1 y2\\
-\hspace*{0pt} ~| less{\char95}eqa (A1{\char95},~A2{\char95}) B{\char95}~(x1,~y1) (x2,~y2) =\\
-\hspace*{0pt} ~~~less ((ord{\char95}preorder o preorder{\char95}order) A2{\char95}) x1 x2 orelse\\
-\hspace*{0pt} ~~~~~eqop A1{\char95}~x1 x2 andalso\\
-\hspace*{0pt} ~~~~~~~less{\char95}eq ((ord{\char95}preorder o preorder{\char95}order) B{\char95}) y1 y2;\\
-\hspace*{0pt}\\
-\hspace*{0pt}end;~(*struct Example*)%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-In some cases, the automatically derived code equations
+ the way, in some cases the automatically derived code equations
for equality on a particular type may not be appropriate.
As example, watch the following datatype representing
monomorphic parametric types (where type constructors
--- a/src/HOL/Code_Setup.thy Thu Apr 16 17:29:56 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,253 +0,0 @@
-(* Title: HOL/Code_Setup.thy
- ID: $Id$
- Author: Florian Haftmann
-*)
-
-header {* Setup of code generators and related tools *}
-
-theory Code_Setup
-imports HOL
-begin
-
-subsection {* Generic code generator foundation *}
-
-text {* Datatypes *}
-
-code_datatype True False
-
-code_datatype "TYPE('a\<Colon>{})"
-
-code_datatype Trueprop "prop"
-
-text {* Code equations *}
-
-lemma [code]:
- shows "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
- and "(False \<Longrightarrow> Q) \<equiv> Trueprop True"
- and "(PROP P \<Longrightarrow> True) \<equiv> Trueprop True"
- and "(Q \<Longrightarrow> False) \<equiv> Trueprop (\<not> Q)" by (auto intro!: equal_intr_rule)
-
-lemma [code]:
- shows "False \<and> x \<longleftrightarrow> False"
- and "True \<and> x \<longleftrightarrow> x"
- and "x \<and> False \<longleftrightarrow> False"
- and "x \<and> True \<longleftrightarrow> x" by simp_all
-
-lemma [code]:
- shows "False \<or> x \<longleftrightarrow> x"
- and "True \<or> x \<longleftrightarrow> True"
- and "x \<or> False \<longleftrightarrow> x"
- and "x \<or> True \<longleftrightarrow> True" by simp_all
-
-lemma [code]:
- shows "\<not> True \<longleftrightarrow> False"
- and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+
-
-lemmas [code] = Let_def if_True if_False
-
-lemmas [code, code unfold, symmetric, code post] = imp_conv_disj
-
-text {* Equality *}
-
-context eq
-begin
-
-lemma equals_eq [code inline, code]: "op = \<equiv> eq"
- by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
-
-declare eq [code unfold, code inline del]
-
-declare equals_eq [symmetric, code post]
-
-end
-
-declare simp_thms(6) [code nbe]
-
-hide (open) const eq
-hide const eq
-
-setup {*
- Code_Unit.add_const_alias @{thm equals_eq}
-*}
-
-text {* Cases *}
-
-lemma Let_case_cert:
- assumes "CASE \<equiv> (\<lambda>x. Let x f)"
- shows "CASE x \<equiv> f x"
- using assms by simp_all
-
-lemma If_case_cert:
- assumes "CASE \<equiv> (\<lambda>b. If b f g)"
- shows "(CASE True \<equiv> f) &&& (CASE False \<equiv> g)"
- using assms by simp_all
-
-setup {*
- Code.add_case @{thm Let_case_cert}
- #> Code.add_case @{thm If_case_cert}
- #> Code.add_undefined @{const_name undefined}
-*}
-
-code_abort undefined
-
-
-subsection {* Generic code generator preprocessor *}
-
-setup {*
- Code.map_pre (K HOL_basic_ss)
- #> Code.map_post (K HOL_basic_ss)
-*}
-
-
-subsection {* Generic code generator target languages *}
-
-text {* type bool *}
-
-code_type bool
- (SML "bool")
- (OCaml "bool")
- (Haskell "Bool")
-
-code_const True and False and Not and "op &" and "op |" and If
- (SML "true" and "false" and "not"
- and infixl 1 "andalso" and infixl 0 "orelse"
- and "!(if (_)/ then (_)/ else (_))")
- (OCaml "true" and "false" and "not"
- and infixl 4 "&&" and infixl 2 "||"
- and "!(if (_)/ then (_)/ else (_))")
- (Haskell "True" and "False" and "not"
- and infixl 3 "&&" and infixl 2 "||"
- and "!(if (_)/ then (_)/ else (_))")
-
-code_reserved SML
- bool true false not
-
-code_reserved OCaml
- bool not
-
-text {* using built-in Haskell equality *}
-
-code_class eq
- (Haskell "Eq")
-
-code_const "eq_class.eq"
- (Haskell infixl 4 "==")
-
-code_const "op ="
- (Haskell infixl 4 "==")
-
-text {* undefined *}
-
-code_const undefined
- (SML "!(raise/ Fail/ \"undefined\")")
- (OCaml "failwith/ \"undefined\"")
- (Haskell "error/ \"undefined\"")
-
-
-subsection {* SML code generator setup *}
-
-types_code
- "bool" ("bool")
-attach (term_of) {*
-fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
-*}
-attach (test) {*
-fun gen_bool i =
- let val b = one_of [false, true]
- in (b, fn () => term_of_bool b) end;
-*}
- "prop" ("bool")
-attach (term_of) {*
-fun term_of_prop b =
- HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);
-*}
-
-consts_code
- "Trueprop" ("(_)")
- "True" ("true")
- "False" ("false")
- "Not" ("Bool.not")
- "op |" ("(_ orelse/ _)")
- "op &" ("(_ andalso/ _)")
- "If" ("(if _/ then _/ else _)")
-
-setup {*
-let
-
-fun eq_codegen thy defs dep thyname b t gr =
- (case strip_comb t of
- (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
- | (Const ("op =", _), [t, u]) =>
- let
- val (pt, gr') = Codegen.invoke_codegen thy defs dep thyname false t gr;
- val (pu, gr'') = Codegen.invoke_codegen thy defs dep thyname false u gr';
- val (_, gr''') = Codegen.invoke_tycodegen thy defs dep thyname false HOLogic.boolT gr'';
- in
- SOME (Codegen.parens
- (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]), gr''')
- end
- | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
- thy defs dep thyname b (Codegen.eta_expand t ts 2) gr)
- | _ => NONE);
-
-in
- Codegen.add_codegen "eq_codegen" eq_codegen
-end
-*}
-
-
-subsection {* Evaluation and normalization by evaluation *}
-
-setup {*
- Value.add_evaluator ("SML", Codegen.eval_term o ProofContext.theory_of)
-*}
-
-ML {*
-structure Eval_Method =
-struct
-
-val eval_ref : (unit -> bool) option ref = ref NONE;
-
-end;
-*}
-
-oracle eval_oracle = {* fn ct =>
- let
- val thy = Thm.theory_of_cterm ct;
- val t = Thm.term_of ct;
- val dummy = @{cprop True};
- in case try HOLogic.dest_Trueprop t
- of SOME t' => if Code_ML.eval_term
- ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy t' []
- then Thm.capply (Thm.capply @{cterm "op \<equiv> \<Colon> prop \<Rightarrow> prop \<Rightarrow> prop"} ct) dummy
- else dummy
- | NONE => dummy
- end
-*}
-
-ML {*
-fun gen_eval_method conv ctxt = SIMPLE_METHOD'
- (CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt)
- THEN' rtac TrueI)
-*}
-
-method_setup eval = {* Scan.succeed (gen_eval_method eval_oracle) *}
- "solve goal by evaluation"
-
-method_setup evaluation = {* Scan.succeed (gen_eval_method Codegen.evaluation_conv) *}
- "solve goal by evaluation"
-
-method_setup normalization = {*
- Scan.succeed (K (SIMPLE_METHOD' (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))))
-*} "solve goal by normalization"
-
-
-subsection {* Quickcheck *}
-
-setup {*
- Quickcheck.add_generator ("SML", Codegen.test_term)
-*}
-
-quickcheck_params [size = 5, iterations = 50]
-
-end
--- a/src/HOL/Decision_Procs/cooper_tac.ML Thu Apr 16 17:29:56 2009 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Fri Apr 17 08:36:18 2009 +0200
@@ -76,7 +76,7 @@
@{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
Suc_plus1]
addsimps @{thms add_ac}
- addsimprocs [cancel_div_mod_proc]
+ addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
val simpset0 = HOL_basic_ss
addsimps [mod_div_equality', Suc_plus1]
addsimps comp_arith
--- a/src/HOL/Decision_Procs/mir_tac.ML Thu Apr 16 17:29:56 2009 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML Fri Apr 17 08:36:18 2009 +0200
@@ -99,7 +99,7 @@
@{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
@{thm "Suc_plus1"}]
addsimps @{thms add_ac}
- addsimprocs [cancel_div_mod_proc]
+ addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
val simpset0 = HOL_basic_ss
addsimps [mod_div_equality', Suc_plus1]
addsimps comp_ths
--- a/src/HOL/Divides.thy Thu Apr 16 17:29:56 2009 +0200
+++ b/src/HOL/Divides.thy Fri Apr 17 08:36:18 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/Divides.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1999 University of Cambridge
*)
@@ -20,11 +19,12 @@
subsection {* Abstract division in commutative semirings. *}
-class semiring_div = comm_semiring_1_cancel + div +
+class semiring_div = comm_semiring_1_cancel + no_zero_divisors + div +
assumes mod_div_equality: "a div b * b + a mod b = a"
and div_by_0 [simp]: "a div 0 = 0"
and div_0 [simp]: "0 div a = 0"
and div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
+ and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
begin
text {* @{const div} and @{const mod} *}
@@ -38,16 +38,16 @@
by (simp only: add_ac)
lemma div_mod_equality: "((a div b) * b + a mod b) + c = a + c"
-by (simp add: mod_div_equality)
+ by (simp add: mod_div_equality)
lemma div_mod_equality2: "(b * (a div b) + a mod b) + c = a + c"
-by (simp add: mod_div_equality2)
+ by (simp add: mod_div_equality2)
lemma mod_by_0 [simp]: "a mod 0 = a"
-using mod_div_equality [of a zero] by simp
+ using mod_div_equality [of a zero] by simp
lemma mod_0 [simp]: "0 mod a = 0"
-using mod_div_equality [of zero a] div_0 by simp
+ using mod_div_equality [of zero a] div_0 by simp
lemma div_mult_self2 [simp]:
assumes "b \<noteq> 0"
@@ -72,7 +72,7 @@
qed
lemma mod_mult_self2 [simp]: "(a + b * c) mod b = a mod b"
-by (simp add: mult_commute [of b])
+ by (simp add: mult_commute [of b])
lemma div_mult_self1_is_id [simp]: "b \<noteq> 0 \<Longrightarrow> b * a div b = a"
using div_mult_self2 [of b 0 a] by simp
@@ -238,9 +238,9 @@
by (simp only: mod_add_eq [symmetric])
qed
-lemma div_add[simp]: "z dvd x \<Longrightarrow> z dvd y
+lemma div_add [simp]: "z dvd x \<Longrightarrow> z dvd y
\<Longrightarrow> (x + y) div z = x div z + y div z"
-by(cases "z=0", simp, unfold dvd_def, auto simp add: algebra_simps)
+by (cases "z = 0", simp, unfold dvd_def, auto simp add: algebra_simps)
text {* Multiplication respects modular equivalence. *}
@@ -297,21 +297,41 @@
finally show ?thesis .
qed
-end
-
-lemma div_mult_div_if_dvd: "(y::'a::{semiring_div,no_zero_divisors}) dvd x \<Longrightarrow>
- z dvd w \<Longrightarrow> (x div y) * (w div z) = (x * w) div (y * z)"
-unfolding dvd_def
- apply clarify
- apply (case_tac "y = 0")
- apply simp
- apply (case_tac "z = 0")
- apply simp
- apply (simp add: algebra_simps)
+lemma div_mult_div_if_dvd:
+ "y dvd x \<Longrightarrow> z dvd w \<Longrightarrow> (x div y) * (w div z) = (x * w) div (y * z)"
+ apply (cases "y = 0", simp)
+ apply (cases "z = 0", simp)
+ apply (auto elim!: dvdE simp add: algebra_simps)
apply (subst mult_assoc [symmetric])
apply (simp add: no_zero_divisors)
-done
+ done
+
+lemma div_mult_mult2 [simp]:
+ "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"
+ by (drule div_mult_mult1) (simp add: mult_commute)
+
+lemma div_mult_mult1_if [simp]:
+ "(c * a) div (c * b) = (if c = 0 then 0 else a div b)"
+ by simp_all
+lemma mod_mult_mult1:
+ "(c * a) mod (c * b) = c * (a mod b)"
+proof (cases "c = 0")
+ case True then show ?thesis by simp
+next
+ case False
+ from mod_div_equality
+ have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" .
+ with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b)
+ = c * a + c * (a mod b)" by (simp add: algebra_simps)
+ with mod_div_equality show ?thesis by simp
+qed
+
+lemma mod_mult_mult2:
+ "(a * c) mod (b * c) = (a mod b) * c"
+ using mod_mult_mult1 [of c a b] by (simp add: mult_commute)
+
+end
lemma div_power: "(y::'a::{semiring_div,no_zero_divisors,recpower}) dvd x \<Longrightarrow>
(x div y)^n = x^n div y^n"
@@ -398,15 +418,17 @@
@{term "q\<Colon>nat"}(uotient) and @{term "r\<Colon>nat"}(emainder).
*}
-definition divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
- "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)"
+definition divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat \<Rightarrow> bool" where
+ "divmod_rel m n qr \<longleftrightarrow>
+ m = fst qr * n + snd qr \<and>
+ (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)"
text {* @{const divmod_rel} is total: *}
lemma divmod_rel_ex:
- obtains q r where "divmod_rel m n q r"
+ obtains q r where "divmod_rel m n (q, r)"
proof (cases "n = 0")
- case True with that show thesis
+ case True with that show thesis
by (auto simp add: divmod_rel_def)
next
case False
@@ -436,13 +458,14 @@
text {* @{const divmod_rel} is injective: *}
-lemma divmod_rel_unique_div:
- assumes "divmod_rel m n q r"
- and "divmod_rel m n q' r'"
- shows "q = q'"
+lemma divmod_rel_unique:
+ assumes "divmod_rel m n qr"
+ and "divmod_rel m n qr'"
+ shows "qr = qr'"
proof (cases "n = 0")
case True with assms show ?thesis
- by (simp add: divmod_rel_def)
+ by (cases qr, cases qr')
+ (simp add: divmod_rel_def)
next
case False
have aux: "\<And>q r q' r'. q' * n + r' = q * n + r \<Longrightarrow> r < n \<Longrightarrow> q' \<le> (q\<Colon>nat)"
@@ -450,18 +473,11 @@
apply (subst less_iff_Suc_add)
apply (auto simp add: add_mult_distrib)
done
- from `n \<noteq> 0` assms show ?thesis
- by (auto simp add: divmod_rel_def
- intro: order_antisym dest: aux sym)
-qed
-
-lemma divmod_rel_unique_mod:
- assumes "divmod_rel m n q r"
- and "divmod_rel m n q' r'"
- shows "r = r'"
-proof -
- from assms have "q = q'" by (rule divmod_rel_unique_div)
- with assms show ?thesis by (simp add: divmod_rel_def)
+ from `n \<noteq> 0` assms have "fst qr = fst qr'"
+ by (auto simp add: divmod_rel_def intro: order_antisym dest: aux sym)
+ moreover from this assms have "snd qr = snd qr'"
+ by (simp add: divmod_rel_def)
+ ultimately show ?thesis by (cases qr, cases qr') simp
qed
text {*
@@ -473,7 +489,21 @@
begin
definition divmod :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
- [code del]: "divmod m n = (THE (q, r). divmod_rel m n q r)"
+ [code del]: "divmod m n = (THE qr. divmod_rel m n qr)"
+
+lemma divmod_rel_divmod:
+ "divmod_rel m n (divmod m n)"
+proof -
+ from divmod_rel_ex
+ obtain qr where rel: "divmod_rel m n qr" .
+ then show ?thesis
+ by (auto simp add: divmod_def intro: theI elim: divmod_rel_unique)
+qed
+
+lemma divmod_eq:
+ assumes "divmod_rel m n qr"
+ shows "divmod m n = qr"
+ using assms by (auto intro: divmod_rel_unique divmod_rel_divmod)
definition div_nat where
"m div n = fst (divmod m n)"
@@ -485,30 +515,18 @@
"divmod m n = (m div n, m mod n)"
unfolding div_nat_def mod_nat_def by simp
-lemma divmod_eq:
- assumes "divmod_rel m n q r"
- shows "divmod m n = (q, r)"
- using assms by (auto simp add: divmod_def
- dest: divmod_rel_unique_div divmod_rel_unique_mod)
-
lemma div_eq:
- assumes "divmod_rel m n q r"
+ assumes "divmod_rel m n (q, r)"
shows "m div n = q"
- using assms by (auto dest: divmod_eq simp add: div_nat_def)
+ using assms by (auto dest: divmod_eq simp add: divmod_div_mod)
lemma mod_eq:
- assumes "divmod_rel m n q r"
+ assumes "divmod_rel m n (q, r)"
shows "m mod n = r"
- using assms by (auto dest: divmod_eq simp add: mod_nat_def)
+ using assms by (auto dest: divmod_eq simp add: divmod_div_mod)
-lemma divmod_rel: "divmod_rel m n (m div n) (m mod n)"
-proof -
- from divmod_rel_ex
- obtain q r where rel: "divmod_rel m n q r" .
- moreover with div_eq mod_eq have "m div n = q" and "m mod n = r"
- by simp_all
- ultimately show ?thesis by simp
-qed
+lemma divmod_rel: "divmod_rel m n (m div n, m mod n)"
+ by (simp add: div_nat_def mod_nat_def divmod_rel_divmod)
lemma divmod_zero:
"divmod m 0 = (0, m)"
@@ -531,10 +549,10 @@
assumes "0 < n" and "n \<le> m"
shows "divmod m n = (Suc ((m - n) div n), (m - n) mod n)"
proof -
- from divmod_rel have divmod_m_n: "divmod_rel m n (m div n) (m mod n)" .
+ from divmod_rel have divmod_m_n: "divmod_rel m n (m div n, m mod n)" .
with assms have m_div_n: "m div n \<ge> 1"
by (cases "m div n") (auto simp add: divmod_rel_def)
- from assms divmod_m_n have "divmod_rel (m - n) n (m div n - Suc 0) (m mod n)"
+ from assms divmod_m_n have "divmod_rel (m - n) n (m div n - Suc 0, m mod n)"
by (cases "m div n") (auto simp add: divmod_rel_def)
with divmod_eq have "divmod (m - n) n = (m div n - Suc 0, m mod n)" by simp
moreover from divmod_div_mod have "divmod (m - n) n = ((m - n) div n, (m - n) mod n)" .
@@ -569,55 +587,74 @@
shows "m mod n = (m - n) mod n"
using assms divmod_step divmod_div_mod by (cases "n = 0") simp_all
-instance proof
- fix m n :: nat show "m div n * n + m mod n = m"
- using divmod_rel [of m n] by (simp add: divmod_rel_def)
-next
- fix n :: nat show "n div 0 = 0"
- using divmod_zero divmod_div_mod [of n 0] by simp
-next
- fix n :: nat show "0 div n = 0"
- using divmod_rel [of 0 n] by (cases n) (simp_all add: divmod_rel_def)
-next
- fix m n q :: nat assume "n \<noteq> 0" then show "(q + m * n) div n = m + q div n"
- by (induct m) (simp_all add: le_div_geq)
+instance proof -
+ have [simp]: "\<And>n::nat. n div 0 = 0"
+ by (simp add: div_nat_def divmod_zero)
+ have [simp]: "\<And>n::nat. 0 div n = 0"
+ proof -
+ fix n :: nat
+ show "0 div n = 0"
+ by (cases "n = 0") simp_all
+ qed
+ show "OFCLASS(nat, semiring_div_class)" proof
+ fix m n :: nat
+ show "m div n * n + m mod n = m"
+ using divmod_rel [of m n] by (simp add: divmod_rel_def)
+ next
+ fix m n q :: nat
+ assume "n \<noteq> 0"
+ then show "(q + m * n) div n = m + q div n"
+ by (induct m) (simp_all add: le_div_geq)
+ next
+ fix m n q :: nat
+ assume "m \<noteq> 0"
+ then show "(m * n) div (m * q) = n div q"
+ proof (cases "n \<noteq> 0 \<and> q \<noteq> 0")
+ case False then show ?thesis by auto
+ next
+ case True with `m \<noteq> 0`
+ have "m > 0" and "n > 0" and "q > 0" by auto
+ then have "\<And>a b. divmod_rel n q (a, b) \<Longrightarrow> divmod_rel (m * n) (m * q) (a, m * b)"
+ by (auto simp add: divmod_rel_def) (simp_all add: algebra_simps)
+ moreover from divmod_rel have "divmod_rel n q (n div q, n mod q)" .
+ ultimately have "divmod_rel (m * n) (m * q) (n div q, m * (n mod q))" .
+ then show ?thesis by (simp add: div_eq)
+ qed
+ qed simp_all
qed
end
text {* Simproc for cancelling @{const div} and @{const mod} *}
-(*lemmas mod_div_equality_nat = semiring_div_class.times_div_mod_plus_zero_one.mod_div_equality [of "m\<Colon>nat" n, standard]
-lemmas mod_div_equality2_nat = mod_div_equality2 [of "n\<Colon>nat" m, standard*)
+ML {*
+local
+
+structure CancelDivMod = CancelDivModFun(struct
-ML {*
-structure CancelDivModData =
-struct
-
-val div_name = @{const_name div};
-val mod_name = @{const_name mod};
-val mk_binop = HOLogic.mk_binop;
-val mk_sum = Nat_Arith.mk_sum;
-val dest_sum = Nat_Arith.dest_sum;
+ val div_name = @{const_name div};
+ val mod_name = @{const_name mod};
+ val mk_binop = HOLogic.mk_binop;
+ val mk_sum = Nat_Arith.mk_sum;
+ val dest_sum = Nat_Arith.dest_sum;
-(*logic*)
+ val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
-val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}]
-
-val trans = trans
+ val trans = trans;
-val prove_eq_sums =
- let val simps = @{thm add_0} :: @{thm add_0_right} :: @{thms add_ac}
- in Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac simps) end;
+ val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
+ (@{thm monoid_add_class.add_0_left} :: @{thm monoid_add_class.add_0_right} :: @{thms add_ac}))
-end;
+end)
-structure CancelDivMod = CancelDivModFun(CancelDivModData);
+in
-val cancel_div_mod_proc = Simplifier.simproc (the_context ())
+val cancel_div_mod_nat_proc = Simplifier.simproc (the_context ())
"cancel_div_mod" ["(m::nat) + n"] (K CancelDivMod.proc);
-Addsimprocs[cancel_div_mod_proc];
+val _ = Addsimprocs [cancel_div_mod_nat_proc];
+
+end
*}
text {* code generator setup *}
@@ -658,7 +695,7 @@
fixes m n :: nat
assumes "n > 0"
shows "m mod n < (n::nat)"
- using assms divmod_rel unfolding divmod_rel_def by auto
+ using assms divmod_rel [of m n] unfolding divmod_rel_def by auto
lemma mod_less_eq_dividend [simp]:
fixes m n :: nat
@@ -700,18 +737,19 @@
subsubsection {* Quotient and Remainder *}
lemma divmod_rel_mult1_eq:
- "[| divmod_rel b c q r; c > 0 |]
- ==> divmod_rel (a*b) c (a*q + a*r div c) (a*r mod c)"
+ "divmod_rel b c (q, r) \<Longrightarrow> c > 0
+ \<Longrightarrow> divmod_rel (a * b) c (a * q + a * r div c, a * r mod c)"
by (auto simp add: split_ifs divmod_rel_def algebra_simps)
-lemma div_mult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)"
+lemma div_mult1_eq:
+ "(a * b) div c = a * (b div c) + a * (b mod c) div (c::nat)"
apply (cases "c = 0", simp)
apply (blast intro: divmod_rel [THEN divmod_rel_mult1_eq, THEN div_eq])
done
lemma divmod_rel_add1_eq:
- "[| divmod_rel a c aq ar; divmod_rel b c bq br; c > 0 |]
- ==> divmod_rel (a + b) c (aq + bq + (ar+br) div c) ((ar + br) mod c)"
+ "divmod_rel a c (aq, ar) \<Longrightarrow> divmod_rel b c (bq, br) \<Longrightarrow> c > 0
+ \<Longrightarrow> divmod_rel (a + b) c (aq + bq + (ar + br) div c, (ar + br) mod c)"
by (auto simp add: split_ifs divmod_rel_def algebra_simps)
(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
@@ -728,8 +766,9 @@
apply (simp add: add_mult_distrib2)
done
-lemma divmod_rel_mult2_eq: "[| divmod_rel a b q r; 0 < b; 0 < c |]
- ==> divmod_rel a (b*c) (q div c) (b*(q mod c) + r)"
+lemma divmod_rel_mult2_eq:
+ "divmod_rel a b (q, r) \<Longrightarrow> 0 < b \<Longrightarrow> 0 < c
+ \<Longrightarrow> divmod_rel a (b * c) (q div c, b *(q mod c) + r)"
by (auto simp add: mult_ac divmod_rel_def add_mult_distrib2 [symmetric] mod_lemma)
lemma div_mult2_eq: "a div (b*c) = (a div b) div (c::nat)"
@@ -745,23 +784,6 @@
done
-subsubsection{*Cancellation of Common Factors in Division*}
-
-lemma div_mult_mult_lemma:
- "[| (0::nat) < b; 0 < c |] ==> (c*a) div (c*b) = a div b"
-by (auto simp add: div_mult2_eq)
-
-lemma div_mult_mult1 [simp]: "(0::nat) < c ==> (c*a) div (c*b) = a div b"
- apply (cases "b = 0")
- apply (auto simp add: linorder_neq_iff [of b] div_mult_mult_lemma)
- done
-
-lemma div_mult_mult2 [simp]: "(0::nat) < c ==> (a*c) div (b*c) = a div b"
- apply (drule div_mult_mult1)
- apply (auto simp add: mult_commute)
- done
-
-
subsubsection{*Further Facts about Quotient and Remainder*}
lemma div_1 [simp]: "m div Suc 0 = m"
@@ -769,7 +791,7 @@
(* Monotonicity of div in first argument *)
-lemma div_le_mono [rule_format]:
+lemma div_le_mono [rule_format (no_asm)]:
"\<forall>m::nat. m \<le> n --> (m div k) \<le> (n div k)"
apply (case_tac "k=0", simp)
apply (induct "n" rule: nat_less_induct, clarify)
@@ -824,12 +846,6 @@
apply (simp_all)
done
-lemma nat_div_eq_0 [simp]: "(n::nat) > 0 ==> ((m div n) = 0) = (m < n)"
-by(auto, subst mod_div_equality [of m n, symmetric], auto)
-
-lemma nat_div_gt_0 [simp]: "(n::nat) > 0 ==> ((m div n) > 0) = (m >= n)"
-by (subst neq0_conv [symmetric], auto)
-
declare div_less_dividend [simp]
text{*A fact for the mutilated chess board*}
@@ -915,16 +931,10 @@
done
lemma dvd_imp_le: "[| k dvd n; 0 < n |] ==> k \<le> (n::nat)"
-by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
-
-lemma nat_dvd_not_less: "(0::nat) < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
-by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
+ by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
lemma dvd_mult_div_cancel: "n dvd m ==> n * (m div n) = (m::nat)"
- apply (subgoal_tac "m mod n = 0")
- apply (simp add: mult_div_cancel)
- apply (simp only: dvd_eq_mod_eq_0)
- done
+ by (simp add: dvd_eq_mod_eq_0 mult_div_cancel)
lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
by (induct n) auto
@@ -1001,9 +1011,11 @@
from A B show ?lhs ..
next
assume P: ?lhs
- then have "divmod_rel m n q (m - n * q)"
+ then have "divmod_rel m n (q, m - n * q)"
unfolding divmod_rel_def by (auto simp add: mult_ac)
- then show ?rhs using divmod_rel by (rule divmod_rel_unique_div)
+ with divmod_rel_unique divmod_rel [of m n]
+ have "(q, m - n * q) = (m div n, m mod n)" by auto
+ then show ?rhs by simp
qed
theorem split_div':
@@ -1155,4 +1167,9 @@
with j show ?thesis by blast
qed
+lemma nat_dvd_not_less:
+ fixes m n :: nat
+ shows "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
+by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
+
end
--- a/src/HOL/Groebner_Basis.thy Thu Apr 16 17:29:56 2009 +0200
+++ b/src/HOL/Groebner_Basis.thy Fri Apr 17 08:36:18 2009 +0200
@@ -5,7 +5,7 @@
header {* Semiring normalization and Groebner Bases *}
theory Groebner_Basis
-imports NatBin
+imports Nat_Numeral
uses
"Tools/Groebner_Basis/misc.ML"
"Tools/Groebner_Basis/normalizer_data.ML"
--- a/src/HOL/HOL.thy Thu Apr 16 17:29:56 2009 +0200
+++ b/src/HOL/HOL.thy Fri Apr 17 08:36:18 2009 +0200
@@ -5,7 +5,7 @@
header {* The basis of Higher-Order Logic *}
theory HOL
-imports Pure
+imports Pure "~~/src/Tools/Code_Generator"
uses
("Tools/hologic.ML")
"~~/src/Tools/IsaPlanner/zipper.ML"
@@ -27,16 +27,6 @@
"~~/src/Tools/atomize_elim.ML"
"~~/src/Tools/induct.ML"
("~~/src/Tools/induct_tacs.ML")
- "~~/src/Tools/value.ML"
- "~~/src/Tools/code/code_name.ML"
- "~~/src/Tools/code/code_funcgr.ML" (*formal dependency*)
- "~~/src/Tools/code/code_wellsorted.ML"
- "~~/src/Tools/code/code_thingol.ML"
- "~~/src/Tools/code/code_printer.ML"
- "~~/src/Tools/code/code_target.ML"
- "~~/src/Tools/code/code_ml.ML"
- "~~/src/Tools/code/code_haskell.ML"
- "~~/src/Tools/nbe.ML"
("Tools/recfun_codegen.ML")
begin
@@ -1674,35 +1664,259 @@
*}
-subsection {* Code generator basics -- see further theory @{text "Code_Setup"} *}
+subsection {* Code generator setup *}
+
+subsubsection {* SML code generator setup *}
+
+use "Tools/recfun_codegen.ML"
+
+setup {*
+ Codegen.setup
+ #> RecfunCodegen.setup
+*}
+
+types_code
+ "bool" ("bool")
+attach (term_of) {*
+fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
+*}
+attach (test) {*
+fun gen_bool i =
+ let val b = one_of [false, true]
+ in (b, fn () => term_of_bool b) end;
+*}
+ "prop" ("bool")
+attach (term_of) {*
+fun term_of_prop b =
+ HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);
+*}
-text {* Equality *}
+consts_code
+ "Trueprop" ("(_)")
+ "True" ("true")
+ "False" ("false")
+ "Not" ("Bool.not")
+ "op |" ("(_ orelse/ _)")
+ "op &" ("(_ andalso/ _)")
+ "If" ("(if _/ then _/ else _)")
+
+setup {*
+let
+
+fun eq_codegen thy defs dep thyname b t gr =
+ (case strip_comb t of
+ (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
+ | (Const ("op =", _), [t, u]) =>
+ let
+ val (pt, gr') = Codegen.invoke_codegen thy defs dep thyname false t gr;
+ val (pu, gr'') = Codegen.invoke_codegen thy defs dep thyname false u gr';
+ val (_, gr''') = Codegen.invoke_tycodegen thy defs dep thyname false HOLogic.boolT gr'';
+ in
+ SOME (Codegen.parens
+ (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]), gr''')
+ end
+ | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
+ thy defs dep thyname b (Codegen.eta_expand t ts 2) gr)
+ | _ => NONE);
+
+in
+ Codegen.add_codegen "eq_codegen" eq_codegen
+end
+*}
+
+subsubsection {* Equality *}
class eq =
fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
assumes eq_equals: "eq x y \<longleftrightarrow> x = y"
begin
-lemma eq: "eq = (op =)"
+lemma eq [code unfold, code inline del]: "eq = (op =)"
by (rule ext eq_equals)+
lemma eq_refl: "eq x x \<longleftrightarrow> True"
unfolding eq by rule+
+lemma equals_eq [code inline, code]: "(op =) \<equiv> eq"
+ by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
+
+declare equals_eq [symmetric, code post]
+
end
-text {* Module setup *}
+subsubsection {* Generic code generator foundation *}
+
+text {* Datatypes *}
+
+code_datatype True False
+
+code_datatype "TYPE('a\<Colon>{})"
+
+code_datatype Trueprop "prop"
+
+text {* Code equations *}
+
+lemma [code]:
+ shows "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
+ and "(False \<Longrightarrow> Q) \<equiv> Trueprop True"
+ and "(PROP P \<Longrightarrow> True) \<equiv> Trueprop True"
+ and "(Q \<Longrightarrow> False) \<equiv> Trueprop (\<not> Q)" by (auto intro!: equal_intr_rule)
+
+lemma [code]:
+ shows "False \<and> x \<longleftrightarrow> False"
+ and "True \<and> x \<longleftrightarrow> x"
+ and "x \<and> False \<longleftrightarrow> False"
+ and "x \<and> True \<longleftrightarrow> x" by simp_all
+
+lemma [code]:
+ shows "False \<or> x \<longleftrightarrow> x"
+ and "True \<or> x \<longleftrightarrow> True"
+ and "x \<or> False \<longleftrightarrow> x"
+ and "x \<or> True \<longleftrightarrow> True" by simp_all
+
+lemma [code]:
+ shows "\<not> True \<longleftrightarrow> False"
+ and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+
-use "Tools/recfun_codegen.ML"
+lemmas [code] = Let_def if_True if_False
+
+lemmas [code, code unfold, symmetric, code post] = imp_conv_disj
+
+text {* Equality *}
+
+declare simp_thms(6) [code nbe]
+
+hide (open) const eq
+hide const eq
+
+setup {*
+ Code_Unit.add_const_alias @{thm equals_eq}
+*}
+
+text {* Cases *}
+
+lemma Let_case_cert:
+ assumes "CASE \<equiv> (\<lambda>x. Let x f)"
+ shows "CASE x \<equiv> f x"
+ using assms by simp_all
+
+lemma If_case_cert:
+ assumes "CASE \<equiv> (\<lambda>b. If b f g)"
+ shows "(CASE True \<equiv> f) &&& (CASE False \<equiv> g)"
+ using assms by simp_all
+
+setup {*
+ Code.add_case @{thm Let_case_cert}
+ #> Code.add_case @{thm If_case_cert}
+ #> Code.add_undefined @{const_name undefined}
+*}
+
+code_abort undefined
+
+subsubsection {* Generic code generator preprocessor *}
setup {*
- Code_ML.setup
- #> Code_Haskell.setup
- #> Nbe.setup
- #> Codegen.setup
- #> RecfunCodegen.setup
+ Code.map_pre (K HOL_basic_ss)
+ #> Code.map_post (K HOL_basic_ss)
*}
+subsubsection {* Generic code generator target languages *}
+
+text {* type bool *}
+
+code_type bool
+ (SML "bool")
+ (OCaml "bool")
+ (Haskell "Bool")
+
+code_const True and False and Not and "op &" and "op |" and If
+ (SML "true" and "false" and "not"
+ and infixl 1 "andalso" and infixl 0 "orelse"
+ and "!(if (_)/ then (_)/ else (_))")
+ (OCaml "true" and "false" and "not"
+ and infixl 4 "&&" and infixl 2 "||"
+ and "!(if (_)/ then (_)/ else (_))")
+ (Haskell "True" and "False" and "not"
+ and infixl 3 "&&" and infixl 2 "||"
+ and "!(if (_)/ then (_)/ else (_))")
+
+code_reserved SML
+ bool true false not
+
+code_reserved OCaml
+ bool not
+
+text {* using built-in Haskell equality *}
+
+code_class eq
+ (Haskell "Eq")
+
+code_const "eq_class.eq"
+ (Haskell infixl 4 "==")
+
+code_const "op ="
+ (Haskell infixl 4 "==")
+
+text {* undefined *}
+
+code_const undefined
+ (SML "!(raise/ Fail/ \"undefined\")")
+ (OCaml "failwith/ \"undefined\"")
+ (Haskell "error/ \"undefined\"")
+
+subsubsection {* Evaluation and normalization by evaluation *}
+
+setup {*
+ Value.add_evaluator ("SML", Codegen.eval_term o ProofContext.theory_of)
+*}
+
+ML {*
+structure Eval_Method =
+struct
+
+val eval_ref : (unit -> bool) option ref = ref NONE;
+
+end;
+*}
+
+oracle eval_oracle = {* fn ct =>
+ let
+ val thy = Thm.theory_of_cterm ct;
+ val t = Thm.term_of ct;
+ val dummy = @{cprop True};
+ in case try HOLogic.dest_Trueprop t
+ of SOME t' => if Code_ML.eval_term
+ ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy t' []
+ then Thm.capply (Thm.capply @{cterm "op \<equiv> \<Colon> prop \<Rightarrow> prop \<Rightarrow> prop"} ct) dummy
+ else dummy
+ | NONE => dummy
+ end
+*}
+
+ML {*
+fun gen_eval_method conv ctxt = SIMPLE_METHOD'
+ (CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt)
+ THEN' rtac TrueI)
+*}
+
+method_setup eval = {* Scan.succeed (gen_eval_method eval_oracle) *}
+ "solve goal by evaluation"
+
+method_setup evaluation = {* Scan.succeed (gen_eval_method Codegen.evaluation_conv) *}
+ "solve goal by evaluation"
+
+method_setup normalization = {*
+ Scan.succeed (K (SIMPLE_METHOD' (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))))
+*} "solve goal by normalization"
+
+subsubsection {* Quickcheck *}
+
+setup {*
+ Quickcheck.add_generator ("SML", Codegen.test_term)
+*}
+
+quickcheck_params [size = 5, iterations = 50]
+
subsection {* Nitpick hooks *}
--- a/src/HOL/Import/HOL/arithmetic.imp Thu Apr 16 17:29:56 2009 +0200
+++ b/src/HOL/Import/HOL/arithmetic.imp Fri Apr 17 08:36:18 2009 +0200
@@ -43,7 +43,7 @@
"TWO" > "HOL4Base.arithmetic.TWO"
"TIMES2" > "NatSimprocs.nat_mult_2"
"SUC_SUB1" > "HOL4Base.arithmetic.SUC_SUB1"
- "SUC_ONE_ADD" > "NatBin.Suc_eq_add_numeral_1_left"
+ "SUC_ONE_ADD" > "Nat_Numeral.Suc_eq_add_numeral_1_left"
"SUC_NOT" > "Nat.nat.simps_2"
"SUC_ELIM_THM" > "HOL4Base.arithmetic.SUC_ELIM_THM"
"SUC_ADD_SYM" > "HOL4Base.arithmetic.SUC_ADD_SYM"
@@ -233,7 +233,7 @@
"EVEN_AND_ODD" > "HOL4Base.arithmetic.EVEN_AND_ODD"
"EVEN_ADD" > "HOL4Base.arithmetic.EVEN_ADD"
"EVEN" > "HOL4Base.arithmetic.EVEN"
- "EQ_MULT_LCANCEL" > "NatBin.nat_mult_eq_cancel_disj"
+ "EQ_MULT_LCANCEL" > "Nat_Numeral.nat_mult_eq_cancel_disj"
"EQ_MONO_ADD_EQ" > "Nat.nat_add_right_cancel"
"EQ_LESS_EQ" > "Orderings.order_eq_iff"
"EQ_ADD_RCANCEL" > "Nat.nat_add_right_cancel"
--- a/src/HOL/Import/HOL/real.imp Thu Apr 16 17:29:56 2009 +0200
+++ b/src/HOL/Import/HOL/real.imp Fri Apr 17 08:36:18 2009 +0200
@@ -99,7 +99,7 @@
"REAL_POW_INV" > "Power.power_inverse"
"REAL_POW_DIV" > "Power.power_divide"
"REAL_POW_ADD" > "Power.power_add"
- "REAL_POW2_ABS" > "NatBin.power2_abs"
+ "REAL_POW2_ABS" > "Nat_Numeral.power2_abs"
"REAL_POS_NZ" > "HOL4Real.real.REAL_POS_NZ"
"REAL_POS" > "RealDef.real_of_nat_ge_zero"
"REAL_POASQ" > "HOL4Real.real.REAL_POASQ"
@@ -210,7 +210,7 @@
"REAL_LE_RDIV_EQ" > "Ring_and_Field.pos_le_divide_eq"
"REAL_LE_RDIV" > "Ring_and_Field.mult_imp_le_div_pos"
"REAL_LE_RADD" > "OrderedGroup.add_le_cancel_right"
- "REAL_LE_POW2" > "NatBin.zero_compare_simps_12"
+ "REAL_LE_POW2" > "Nat_Numeral.zero_compare_simps_12"
"REAL_LE_NEGTOTAL" > "HOL4Real.real.REAL_LE_NEGTOTAL"
"REAL_LE_NEGR" > "OrderedGroup.le_minus_self_iff"
"REAL_LE_NEGL" > "OrderedGroup.minus_le_self_iff"
@@ -313,7 +313,7 @@
"POW_ONE" > "Power.power_one"
"POW_NZ" > "Power.field_power_not_zero"
"POW_MUL" > "Power.power_mult_distrib"
- "POW_MINUS1" > "NatBin.power_minus1_even"
+ "POW_MINUS1" > "Nat_Numeral.power_minus1_even"
"POW_M1" > "HOL4Real.real.POW_M1"
"POW_LT" > "HOL4Real.real.POW_LT"
"POW_LE" > "Power.power_mono"
@@ -323,7 +323,7 @@
"POW_ABS" > "Power.power_abs"
"POW_2_LT" > "RealPow.two_realpow_gt"
"POW_2_LE1" > "RealPow.two_realpow_ge_one"
- "POW_2" > "NatBin.power2_eq_square"
+ "POW_2" > "Nat_Numeral.power2_eq_square"
"POW_1" > "Power.power_one_right"
"POW_0" > "Power.power_0_Suc"
"ABS_ZERO" > "OrderedGroup.abs_eq_0"
@@ -335,7 +335,7 @@
"ABS_SIGN2" > "HOL4Real.real.ABS_SIGN2"
"ABS_SIGN" > "HOL4Real.real.ABS_SIGN"
"ABS_REFL" > "HOL4Real.real.ABS_REFL"
- "ABS_POW2" > "NatBin.abs_power2"
+ "ABS_POW2" > "Nat_Numeral.abs_power2"
"ABS_POS" > "OrderedGroup.abs_ge_zero"
"ABS_NZ" > "OrderedGroup.zero_less_abs_iff"
"ABS_NEG" > "OrderedGroup.abs_minus_cancel"
--- a/src/HOL/Import/HOLLight/hollight.imp Thu Apr 16 17:29:56 2009 +0200
+++ b/src/HOL/Import/HOLLight/hollight.imp Fri Apr 17 08:36:18 2009 +0200
@@ -1515,7 +1515,7 @@
"EQ_REFL_T" > "HOL.simp_thms_6"
"EQ_REFL" > "Presburger.fm_modd_pinf"
"EQ_MULT_RCANCEL" > "Nat.mult_cancel2"
- "EQ_MULT_LCANCEL" > "NatBin.nat_mult_eq_cancel_disj"
+ "EQ_MULT_LCANCEL" > "Nat_Numeral.nat_mult_eq_cancel_disj"
"EQ_IMP_LE" > "HOLLight.hollight.EQ_IMP_LE"
"EQ_EXT" > "HOL.meta_eq_to_obj_eq"
"EQ_CLAUSES" > "HOLLight.hollight.EQ_CLAUSES"
--- a/src/HOL/IntDiv.thy Thu Apr 16 17:29:56 2009 +0200
+++ b/src/HOL/IntDiv.thy Fri Apr 17 08:36:18 2009 +0200
@@ -249,33 +249,33 @@
text {* Tool setup *}
ML {*
-local
+local
-structure CancelDivMod = CancelDivModFun(
-struct
- val div_name = @{const_name Divides.div};
- val mod_name = @{const_name Divides.mod};
+structure CancelDivMod = CancelDivModFun(struct
+
+ val div_name = @{const_name div};
+ val mod_name = @{const_name mod};
val mk_binop = HOLogic.mk_binop;
val mk_sum = Int_Numeral_Simprocs.mk_sum HOLogic.intT;
val dest_sum = Int_Numeral_Simprocs.dest_sum;
- val div_mod_eqs =
- map mk_meta_eq [@{thm zdiv_zmod_equality},
- @{thm zdiv_zmod_equality2}];
+
+ val div_mod_eqs = map mk_meta_eq [@{thm zdiv_zmod_equality}, @{thm zdiv_zmod_equality2}];
+
val trans = trans;
- val prove_eq_sums =
- let
- val simps = @{thm diff_int_def} :: Int_Numeral_Simprocs.add_0s @ @{thms zadd_ac}
- in Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac simps) end;
+
+ val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
+ (@{thm diff_minus} :: @{thms add_0s} @ @{thms add_ac}))
+
end)
in
-val cancel_zdiv_zmod_proc = Simplifier.simproc (the_context ())
- "cancel_zdiv_zmod" ["(m::int) + n"] (K CancelDivMod.proc)
+val cancel_div_mod_int_proc = Simplifier.simproc (the_context ())
+ "cancel_zdiv_zmod" ["(k::int) + l"] (K CancelDivMod.proc);
-end;
+val _ = Addsimprocs [cancel_div_mod_int_proc];
-Addsimprocs [cancel_zdiv_zmod_proc]
+end
*}
lemma pos_mod_conj : "(0::int) < b ==> 0 \<le> a mod b & a mod b < b"
@@ -711,6 +711,26 @@
show "(a + c * b) div b = c + a div b"
unfolding zdiv_zadd1_eq [of a "c * b"] using not0
by (simp add: zmod_zmult1_eq zmod_zdiv_trivial zdiv_zmult1_eq)
+next
+ fix a b c :: int
+ assume "a \<noteq> 0"
+ then show "(a * b) div (a * c) = b div c"
+ proof (cases "b \<noteq> 0 \<and> c \<noteq> 0")
+ case False then show ?thesis by auto
+ next
+ case True then have "b \<noteq> 0" and "c \<noteq> 0" by auto
+ with `a \<noteq> 0`
+ have "\<And>q r. divmod_rel b c (q, r) \<Longrightarrow> divmod_rel (a * b) (a * c) (q, a * r)"
+ apply (auto simp add: divmod_rel_def)
+ apply (auto simp add: algebra_simps)
+ apply (auto simp add: zero_less_mult_iff zero_le_mult_iff mult_le_0_iff)
+ apply (simp_all add: mult_less_cancel_left_disj mult_commute [of _ a])
+ done
+ moreover with `c \<noteq> 0` divmod_rel_div_mod have "divmod_rel b c (b div c, b mod c)" by auto
+ ultimately have "divmod_rel (a * b) (a * c) (b div c, a * (b mod c))" .
+ moreover from `a \<noteq> 0` `c \<noteq> 0` have "a * c \<noteq> 0" by simp
+ ultimately show ?thesis by (rule divmod_rel_div)
+ qed
qed auto
lemma posDivAlg_div_mod:
@@ -808,52 +828,6 @@
done
-subsection{*Cancellation of Common Factors in div*}
-
-lemma zdiv_zmult_zmult1_aux1:
- "[| (0::int) < b; c \<noteq> 0 |] ==> (c*a) div (c*b) = a div b"
-by (subst zdiv_zmult2_eq, auto)
-
-lemma zdiv_zmult_zmult1_aux2:
- "[| b < (0::int); c \<noteq> 0 |] ==> (c*a) div (c*b) = a div b"
-apply (subgoal_tac " (c * (-a)) div (c * (-b)) = (-a) div (-b) ")
-apply (rule_tac [2] zdiv_zmult_zmult1_aux1, auto)
-done
-
-lemma zdiv_zmult_zmult1: "c \<noteq> (0::int) ==> (c*a) div (c*b) = a div b"
-apply (case_tac "b = 0", simp)
-apply (auto simp add: linorder_neq_iff zdiv_zmult_zmult1_aux1 zdiv_zmult_zmult1_aux2)
-done
-
-lemma zdiv_zmult_zmult1_if[simp]:
- "(k*m) div (k*n) = (if k = (0::int) then 0 else m div n)"
-by (simp add:zdiv_zmult_zmult1)
-
-
-subsection{*Distribution of Factors over mod*}
-
-lemma zmod_zmult_zmult1_aux1:
- "[| (0::int) < b; c \<noteq> 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"
-by (subst zmod_zmult2_eq, auto)
-
-lemma zmod_zmult_zmult1_aux2:
- "[| b < (0::int); c \<noteq> 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"
-apply (subgoal_tac " (c * (-a)) mod (c * (-b)) = c * ((-a) mod (-b))")
-apply (rule_tac [2] zmod_zmult_zmult1_aux1, auto)
-done
-
-lemma zmod_zmult_zmult1: "(c*a) mod (c*b) = (c::int) * (a mod b)"
-apply (case_tac "b = 0", simp)
-apply (case_tac "c = 0", simp)
-apply (auto simp add: linorder_neq_iff zmod_zmult_zmult1_aux1 zmod_zmult_zmult1_aux2)
-done
-
-lemma zmod_zmult_zmult2: "(a*c) mod (b*c) = (a mod b) * (c::int)"
-apply (cut_tac c = c in zmod_zmult_zmult1)
-apply (auto simp add: mult_commute)
-done
-
-
subsection {*Splitting Rules for div and mod*}
text{*The proofs of the two lemmas below are essentially identical*}
@@ -937,7 +911,7 @@
right_distrib)
thus ?thesis
by (subst zdiv_zadd1_eq,
- simp add: zdiv_zmult_zmult1 zmod_zmult_zmult1 one_less_a2
+ simp add: mod_mult_mult1 one_less_a2
div_pos_pos_trivial)
qed
@@ -961,7 +935,7 @@
then number_of v div (number_of w)
else (number_of v + (1::int)) div (number_of w))"
apply (simp only: number_of_eq numeral_simps UNIV_I split: split_if)
-apply (simp add: zdiv_zmult_zmult1 pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac)
+apply (simp add: pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac)
done
@@ -977,7 +951,7 @@
apply (auto simp add: add_commute [of 1] mult_commute add1_zle_eq
pos_mod_bound)
apply (subst mod_add_eq)
-apply (simp add: zmod_zmult_zmult2 mod_pos_pos_trivial)
+apply (simp add: mod_mult_mult2 mod_pos_pos_trivial)
apply (rule mod_pos_pos_trivial)
apply (auto simp add: mod_pos_pos_trivial ring_distribs)
apply (subgoal_tac "0 \<le> b mod a", arith, simp)
@@ -998,7 +972,7 @@
"number_of (Int.Bit0 v) mod number_of (Int.Bit0 w) =
(2::int) * (number_of v mod number_of w)"
apply (simp only: number_of_eq numeral_simps)
-apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2
+apply (simp add: mod_mult_mult1 pos_zmod_mult_2
neg_zmod_mult_2 add_ac)
done
@@ -1008,7 +982,7 @@
then 2 * (number_of v mod number_of w) + 1
else 2 * ((number_of v + (1::int)) mod number_of w) - 1)"
apply (simp only: number_of_eq numeral_simps)
-apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2
+apply (simp add: mod_mult_mult1 pos_zmod_mult_2
neg_zmod_mult_2 add_ac)
done
@@ -1090,9 +1064,7 @@
done
lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
- apply (simp add: dvd_def)
- apply (auto simp add: zmod_zmult_zmult1)
- done
+ by (auto elim!: dvdE simp add: mod_mult_mult1)
lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
apply (subgoal_tac "k dvd n * (m div n) + m mod n")
@@ -1247,9 +1219,9 @@
lemmas zmod_simps =
mod_add_left_eq [symmetric]
mod_add_right_eq [symmetric]
- IntDiv.zmod_zmult1_eq [symmetric]
- mod_mult_left_eq [symmetric]
- IntDiv.zpower_zmod
+ zmod_zmult1_eq [symmetric]
+ mod_mult_left_eq [symmetric]
+ zpower_zmod
zminus_zmod zdiff_zmod_left zdiff_zmod_right
text {* Distributive laws for function @{text nat}. *}
--- a/src/HOL/IsaMakefile Thu Apr 16 17:29:56 2009 +0200
+++ b/src/HOL/IsaMakefile Fri Apr 17 08:36:18 2009 +0200
@@ -89,7 +89,6 @@
$(SRC)/Tools/IsaPlanner/rw_tools.ML \
$(SRC)/Tools/IsaPlanner/zipper.ML \
$(SRC)/Tools/atomize_elim.ML \
- $(SRC)/Tools/code/code_funcgr.ML \
$(SRC)/Tools/code/code_haskell.ML \
$(SRC)/Tools/code/code_ml.ML \
$(SRC)/Tools/code/code_name.ML \
@@ -106,7 +105,7 @@
$(SRC)/Tools/project_rule.ML \
$(SRC)/Tools/random_word.ML \
$(SRC)/Tools/value.ML \
- Code_Setup.thy \
+ $(SRC)/Tools/Code_Generator.thy \
HOL.thy \
Tools/hologic.ML \
Tools/recfun_codegen.ML \
@@ -216,7 +215,7 @@
List.thy \
Main.thy \
Map.thy \
- NatBin.thy \
+ Nat_Numeral.thy \
Presburger.thy \
Recdef.thy \
Relation_Power.thy \
--- a/src/HOL/Library/Code_Index.thy Thu Apr 16 17:29:56 2009 +0200
+++ b/src/HOL/Library/Code_Index.thy Fri Apr 17 08:36:18 2009 +0200
@@ -144,7 +144,7 @@
subsection {* Basic arithmetic *}
-instantiation index :: "{minus, ordered_semidom, Divides.div, linorder}"
+instantiation index :: "{minus, ordered_semidom, semiring_div, linorder}"
begin
definition [simp, code del]:
@@ -172,7 +172,7 @@
"n < m \<longleftrightarrow> nat_of n < nat_of m"
instance proof
-qed (auto simp add: left_distrib)
+qed (auto simp add: index left_distrib div_mult_self1)
end
--- a/src/HOL/Library/Polynomial.thy Thu Apr 16 17:29:56 2009 +0200
+++ b/src/HOL/Library/Polynomial.thy Fri Apr 17 08:36:18 2009 +0200
@@ -987,6 +987,30 @@
by (simp add: pdivmod_rel_def left_distrib)
thus "(x + z * y) div y = z + x div y"
by (rule div_poly_eq)
+next
+ fix x y z :: "'a poly"
+ assume "x \<noteq> 0"
+ show "(x * y) div (x * z) = y div z"
+ proof (cases "y \<noteq> 0 \<and> z \<noteq> 0")
+ have "\<And>x::'a poly. pdivmod_rel x 0 0 x"
+ by (rule pdivmod_rel_by_0)
+ then have [simp]: "\<And>x::'a poly. x div 0 = 0"
+ by (rule div_poly_eq)
+ have "\<And>x::'a poly. pdivmod_rel 0 x 0 0"
+ by (rule pdivmod_rel_0)
+ then have [simp]: "\<And>x::'a poly. 0 div x = 0"
+ by (rule div_poly_eq)
+ case False then show ?thesis by auto
+ next
+ case True then have "y \<noteq> 0" and "z \<noteq> 0" by auto
+ with `x \<noteq> 0`
+ have "\<And>q r. pdivmod_rel y z q r \<Longrightarrow> pdivmod_rel (x * y) (x * z) q (x * r)"
+ by (auto simp add: pdivmod_rel_def algebra_simps)
+ (rule classical, simp add: degree_mult_eq)
+ moreover from pdivmod_rel have "pdivmod_rel y z (y div z) (y mod z)" .
+ ultimately have "pdivmod_rel (x * y) (x * z) (y div z) (x * (y mod z))" .
+ then show ?thesis by (simp add: div_poly_eq)
+ qed
qed
end
--- a/src/HOL/Map.thy Thu Apr 16 17:29:56 2009 +0200
+++ b/src/HOL/Map.thy Fri Apr 17 08:36:18 2009 +0200
@@ -11,7 +11,7 @@
imports List
begin
-types ('a,'b) "~=>" = "'a => 'b option" (infixr 0)
+types ('a,'b) "~=>" = "'a => 'b option" (infixr "~=>" 0)
translations (type) "a ~=> b " <= (type) "a => b option"
syntax (xsymbols)
--- a/src/HOL/NatBin.thy Thu Apr 16 17:29:56 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,975 +0,0 @@
-(* Title: HOL/NatBin.thy
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1999 University of Cambridge
-*)
-
-header {* Binary arithmetic for the natural numbers *}
-
-theory NatBin
-imports IntDiv
-uses ("Tools/nat_simprocs.ML")
-begin
-
-text {*
- Arithmetic for naturals is reduced to that for the non-negative integers.
-*}
-
-instantiation nat :: number
-begin
-
-definition
- nat_number_of_def [code inline, code del]: "number_of v = nat (number_of v)"
-
-instance ..
-
-end
-
-lemma [code post]:
- "nat (number_of v) = number_of v"
- unfolding nat_number_of_def ..
-
-abbreviation (xsymbols)
- power2 :: "'a::power => 'a" ("(_\<twosuperior>)" [1000] 999) where
- "x\<twosuperior> == x^2"
-
-notation (latex output)
- power2 ("(_\<twosuperior>)" [1000] 999)
-
-notation (HTML output)
- power2 ("(_\<twosuperior>)" [1000] 999)
-
-
-subsection {* Predicate for negative binary numbers *}
-
-definition neg :: "int \<Rightarrow> bool" where
- "neg Z \<longleftrightarrow> Z < 0"
-
-lemma not_neg_int [simp]: "~ neg (of_nat n)"
-by (simp add: neg_def)
-
-lemma neg_zminus_int [simp]: "neg (- (of_nat (Suc n)))"
-by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc)
-
-lemmas neg_eq_less_0 = neg_def
-
-lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)"
-by (simp add: neg_def linorder_not_less)
-
-text{*To simplify inequalities when Numeral1 can get simplified to 1*}
-
-lemma not_neg_0: "~ neg 0"
-by (simp add: One_int_def neg_def)
-
-lemma not_neg_1: "~ neg 1"
-by (simp add: neg_def linorder_not_less zero_le_one)
-
-lemma neg_nat: "neg z ==> nat z = 0"
-by (simp add: neg_def order_less_imp_le)
-
-lemma not_neg_nat: "~ neg z ==> of_nat (nat z) = z"
-by (simp add: linorder_not_less neg_def)
-
-text {*
- If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
- @{term Numeral0} IS @{term "number_of Pls"}
-*}
-
-lemma not_neg_number_of_Pls: "~ neg (number_of Int.Pls)"
- by (simp add: neg_def)
-
-lemma neg_number_of_Min: "neg (number_of Int.Min)"
- by (simp add: neg_def)
-
-lemma neg_number_of_Bit0:
- "neg (number_of (Int.Bit0 w)) = neg (number_of w)"
- by (simp add: neg_def)
-
-lemma neg_number_of_Bit1:
- "neg (number_of (Int.Bit1 w)) = neg (number_of w)"
- by (simp add: neg_def)
-
-lemmas neg_simps [simp] =
- not_neg_0 not_neg_1
- not_neg_number_of_Pls neg_number_of_Min
- neg_number_of_Bit0 neg_number_of_Bit1
-
-
-subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*}
-
-declare nat_0 [simp] nat_1 [simp]
-
-lemma nat_number_of [simp]: "nat (number_of w) = number_of w"
-by (simp add: nat_number_of_def)
-
-lemma nat_numeral_0_eq_0 [simp]: "Numeral0 = (0::nat)"
-by (simp add: nat_number_of_def)
-
-lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)"
-by (simp add: nat_1 nat_number_of_def)
-
-lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
-by (simp add: nat_numeral_1_eq_1)
-
-lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
-apply (unfold nat_number_of_def)
-apply (rule nat_2)
-done
-
-
-subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
-
-lemma int_nat_number_of [simp]:
- "int (number_of v) =
- (if neg (number_of v :: int) then 0
- else (number_of v :: int))"
- unfolding nat_number_of_def number_of_is_id neg_def
- by simp
-
-
-subsubsection{*Successor *}
-
-lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
-apply (rule sym)
-apply (simp add: nat_eq_iff int_Suc)
-done
-
-lemma Suc_nat_number_of_add:
- "Suc (number_of v + n) =
- (if neg (number_of v :: int) then 1+n else number_of (Int.succ v) + n)"
- unfolding nat_number_of_def number_of_is_id neg_def numeral_simps
- by (simp add: Suc_nat_eq_nat_zadd1 add_ac)
-
-lemma Suc_nat_number_of [simp]:
- "Suc (number_of v) =
- (if neg (number_of v :: int) then 1 else number_of (Int.succ v))"
-apply (cut_tac n = 0 in Suc_nat_number_of_add)
-apply (simp cong del: if_weak_cong)
-done
-
-
-subsubsection{*Addition *}
-
-lemma add_nat_number_of [simp]:
- "(number_of v :: nat) + number_of v' =
- (if v < Int.Pls then number_of v'
- else if v' < Int.Pls then number_of v
- else number_of (v + v'))"
- unfolding nat_number_of_def number_of_is_id numeral_simps
- by (simp add: nat_add_distrib)
-
-lemma nat_number_of_add_1 [simp]:
- "number_of v + (1::nat) =
- (if v < Int.Pls then 1 else number_of (Int.succ v))"
- unfolding nat_number_of_def number_of_is_id numeral_simps
- by (simp add: nat_add_distrib)
-
-lemma nat_1_add_number_of [simp]:
- "(1::nat) + number_of v =
- (if v < Int.Pls then 1 else number_of (Int.succ v))"
- unfolding nat_number_of_def number_of_is_id numeral_simps
- by (simp add: nat_add_distrib)
-
-lemma nat_1_add_1 [simp]: "1 + 1 = (2::nat)"
- by (rule int_int_eq [THEN iffD1]) simp
-
-
-subsubsection{*Subtraction *}
-
-lemma diff_nat_eq_if:
- "nat z - nat z' =
- (if neg z' then nat z
- else let d = z-z' in
- if neg d then 0 else nat d)"
-by (simp add: Let_def nat_diff_distrib [symmetric] neg_eq_less_0 not_neg_eq_ge_0)
-
-
-lemma diff_nat_number_of [simp]:
- "(number_of v :: nat) - number_of v' =
- (if v' < Int.Pls then number_of v
- else let d = number_of (v + uminus v') in
- if neg d then 0 else nat d)"
- unfolding nat_number_of_def number_of_is_id numeral_simps neg_def
- by auto
-
-lemma nat_number_of_diff_1 [simp]:
- "number_of v - (1::nat) =
- (if v \<le> Int.Pls then 0 else number_of (Int.pred v))"
- unfolding nat_number_of_def number_of_is_id numeral_simps
- by auto
-
-
-subsubsection{*Multiplication *}
-
-lemma mult_nat_number_of [simp]:
- "(number_of v :: nat) * number_of v' =
- (if v < Int.Pls then 0 else number_of (v * v'))"
- unfolding nat_number_of_def number_of_is_id numeral_simps
- by (simp add: nat_mult_distrib)
-
-
-subsubsection{*Quotient *}
-
-lemma div_nat_number_of [simp]:
- "(number_of v :: nat) div number_of v' =
- (if neg (number_of v :: int) then 0
- else nat (number_of v div number_of v'))"
- unfolding nat_number_of_def number_of_is_id neg_def
- by (simp add: nat_div_distrib)
-
-lemma one_div_nat_number_of [simp]:
- "Suc 0 div number_of v' = nat (1 div number_of v')"
-by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric])
-
-
-subsubsection{*Remainder *}
-
-lemma mod_nat_number_of [simp]:
- "(number_of v :: nat) mod number_of v' =
- (if neg (number_of v :: int) then 0
- else if neg (number_of v' :: int) then number_of v
- else nat (number_of v mod number_of v'))"
- unfolding nat_number_of_def number_of_is_id neg_def
- by (simp add: nat_mod_distrib)
-
-lemma one_mod_nat_number_of [simp]:
- "Suc 0 mod number_of v' =
- (if neg (number_of v' :: int) then Suc 0
- else nat (1 mod number_of v'))"
-by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric])
-
-
-subsubsection{* Divisibility *}
-
-lemmas dvd_eq_mod_eq_0_number_of =
- dvd_eq_mod_eq_0 [of "number_of x" "number_of y", standard]
-
-declare dvd_eq_mod_eq_0_number_of [simp]
-
-ML
-{*
-val nat_number_of_def = thm"nat_number_of_def";
-
-val nat_number_of = thm"nat_number_of";
-val nat_numeral_0_eq_0 = thm"nat_numeral_0_eq_0";
-val nat_numeral_1_eq_1 = thm"nat_numeral_1_eq_1";
-val numeral_1_eq_Suc_0 = thm"numeral_1_eq_Suc_0";
-val numeral_2_eq_2 = thm"numeral_2_eq_2";
-val nat_div_distrib = thm"nat_div_distrib";
-val nat_mod_distrib = thm"nat_mod_distrib";
-val int_nat_number_of = thm"int_nat_number_of";
-val Suc_nat_eq_nat_zadd1 = thm"Suc_nat_eq_nat_zadd1";
-val Suc_nat_number_of_add = thm"Suc_nat_number_of_add";
-val Suc_nat_number_of = thm"Suc_nat_number_of";
-val add_nat_number_of = thm"add_nat_number_of";
-val diff_nat_eq_if = thm"diff_nat_eq_if";
-val diff_nat_number_of = thm"diff_nat_number_of";
-val mult_nat_number_of = thm"mult_nat_number_of";
-val div_nat_number_of = thm"div_nat_number_of";
-val mod_nat_number_of = thm"mod_nat_number_of";
-*}
-
-
-subsection{*Comparisons*}
-
-subsubsection{*Equals (=) *}
-
-lemma eq_nat_nat_iff:
- "[| (0::int) <= z; 0 <= z' |] ==> (nat z = nat z') = (z=z')"
-by (auto elim!: nonneg_eq_int)
-
-lemma eq_nat_number_of [simp]:
- "((number_of v :: nat) = number_of v') =
- (if neg (number_of v :: int) then (number_of v' :: int) \<le> 0
- else if neg (number_of v' :: int) then (number_of v :: int) = 0
- else v = v')"
- unfolding nat_number_of_def number_of_is_id neg_def
- by auto
-
-
-subsubsection{*Less-than (<) *}
-
-lemma less_nat_number_of [simp]:
- "(number_of v :: nat) < number_of v' \<longleftrightarrow>
- (if v < v' then Int.Pls < v' else False)"
- unfolding nat_number_of_def number_of_is_id numeral_simps
- by auto
-
-
-subsubsection{*Less-than-or-equal *}
-
-lemma le_nat_number_of [simp]:
- "(number_of v :: nat) \<le> number_of v' \<longleftrightarrow>
- (if v \<le> v' then True else v \<le> Int.Pls)"
- unfolding nat_number_of_def number_of_is_id numeral_simps
- by auto
-
-(*Maps #n to n for n = 0, 1, 2*)
-lemmas numerals = nat_numeral_0_eq_0 nat_numeral_1_eq_1 numeral_2_eq_2
-
-
-subsection{*Powers with Numeric Exponents*}
-
-text{*We cannot refer to the number @{term 2} in @{text Ring_and_Field.thy}.
-We cannot prove general results about the numeral @{term "-1"}, so we have to
-use @{term "- 1"} instead.*}
-
-lemma power2_eq_square: "(a::'a::recpower)\<twosuperior> = a * a"
- by (simp add: numeral_2_eq_2 Power.power_Suc)
-
-lemma zero_power2 [simp]: "(0::'a::{semiring_1,recpower})\<twosuperior> = 0"
- by (simp add: power2_eq_square)
-
-lemma one_power2 [simp]: "(1::'a::{semiring_1,recpower})\<twosuperior> = 1"
- by (simp add: power2_eq_square)
-
-lemma power3_eq_cube: "(x::'a::recpower) ^ 3 = x * x * x"
- apply (subgoal_tac "3 = Suc (Suc (Suc 0))")
- apply (erule ssubst)
- apply (simp add: power_Suc mult_ac)
- apply (unfold nat_number_of_def)
- apply (subst nat_eq_iff)
- apply simp
-done
-
-text{*Squares of literal numerals will be evaluated.*}
-lemmas power2_eq_square_number_of =
- power2_eq_square [of "number_of w", standard]
-declare power2_eq_square_number_of [simp]
-
-
-lemma zero_le_power2[simp]: "0 \<le> (a\<twosuperior>::'a::{ordered_idom,recpower})"
- by (simp add: power2_eq_square)
-
-lemma zero_less_power2[simp]:
- "(0 < a\<twosuperior>) = (a \<noteq> (0::'a::{ordered_idom,recpower}))"
- by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
-
-lemma power2_less_0[simp]:
- fixes a :: "'a::{ordered_idom,recpower}"
- shows "~ (a\<twosuperior> < 0)"
-by (force simp add: power2_eq_square mult_less_0_iff)
-
-lemma zero_eq_power2[simp]:
- "(a\<twosuperior> = 0) = (a = (0::'a::{ordered_idom,recpower}))"
- by (force simp add: power2_eq_square mult_eq_0_iff)
-
-lemma abs_power2[simp]:
- "abs(a\<twosuperior>) = (a\<twosuperior>::'a::{ordered_idom,recpower})"
- by (simp add: power2_eq_square abs_mult abs_mult_self)
-
-lemma power2_abs[simp]:
- "(abs a)\<twosuperior> = (a\<twosuperior>::'a::{ordered_idom,recpower})"
- by (simp add: power2_eq_square abs_mult_self)
-
-lemma power2_minus[simp]:
- "(- a)\<twosuperior> = (a\<twosuperior>::'a::{comm_ring_1,recpower})"
- by (simp add: power2_eq_square)
-
-lemma power2_le_imp_le:
- fixes x y :: "'a::{ordered_semidom,recpower}"
- shows "\<lbrakk>x\<twosuperior> \<le> y\<twosuperior>; 0 \<le> y\<rbrakk> \<Longrightarrow> x \<le> y"
-unfolding numeral_2_eq_2 by (rule power_le_imp_le_base)
-
-lemma power2_less_imp_less:
- fixes x y :: "'a::{ordered_semidom,recpower}"
- shows "\<lbrakk>x\<twosuperior> < y\<twosuperior>; 0 \<le> y\<rbrakk> \<Longrightarrow> x < y"
-by (rule power_less_imp_less_base)
-
-lemma power2_eq_imp_eq:
- fixes x y :: "'a::{ordered_semidom,recpower}"
- shows "\<lbrakk>x\<twosuperior> = y\<twosuperior>; 0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> x = y"
-unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base, simp)
-
-lemma power_minus1_even[simp]: "(- 1) ^ (2*n) = (1::'a::{comm_ring_1,recpower})"
-proof (induct n)
- case 0 show ?case by simp
-next
- case (Suc n) then show ?case by (simp add: power_Suc power_add)
-qed
-
-lemma power_minus1_odd: "(- 1) ^ Suc(2*n) = -(1::'a::{comm_ring_1,recpower})"
- by (simp add: power_Suc)
-
-lemma power_even_eq: "(a::'a::recpower) ^ (2*n) = (a^n)^2"
-by (subst mult_commute) (simp add: power_mult)
-
-lemma power_odd_eq: "(a::int) ^ Suc(2*n) = a * (a^n)^2"
-by (simp add: power_even_eq)
-
-lemma power_minus_even [simp]:
- "(-a) ^ (2*n) = (a::'a::{comm_ring_1,recpower}) ^ (2*n)"
-by (simp add: power_minus1_even power_minus [of a])
-
-lemma zero_le_even_power'[simp]:
- "0 \<le> (a::'a::{ordered_idom,recpower}) ^ (2*n)"
-proof (induct "n")
- case 0
- show ?case by (simp add: zero_le_one)
-next
- case (Suc n)
- have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)"
- by (simp add: mult_ac power_add power2_eq_square)
- thus ?case
- by (simp add: prems zero_le_mult_iff)
-qed
-
-lemma odd_power_less_zero:
- "(a::'a::{ordered_idom,recpower}) < 0 ==> a ^ Suc(2*n) < 0"
-proof (induct "n")
- case 0
- then show ?case by simp
-next
- case (Suc n)
- have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)"
- by (simp add: mult_ac power_add power2_eq_square)
- thus ?case
- by (simp del: power_Suc add: prems mult_less_0_iff mult_neg_neg)
-qed
-
-lemma odd_0_le_power_imp_0_le:
- "0 \<le> a ^ Suc(2*n) ==> 0 \<le> (a::'a::{ordered_idom,recpower})"
-apply (insert odd_power_less_zero [of a n])
-apply (force simp add: linorder_not_less [symmetric])
-done
-
-text{*Simprules for comparisons where common factors can be cancelled.*}
-lemmas zero_compare_simps =
- add_strict_increasing add_strict_increasing2 add_increasing
- zero_le_mult_iff zero_le_divide_iff
- zero_less_mult_iff zero_less_divide_iff
- mult_le_0_iff divide_le_0_iff
- mult_less_0_iff divide_less_0_iff
- zero_le_power2 power2_less_0
-
-subsubsection{*Nat *}
-
-lemma Suc_pred': "0 < n ==> n = Suc(n - 1)"
-by (simp add: numerals)
-
-(*Expresses a natural number constant as the Suc of another one.
- NOT suitable for rewriting because n recurs in the condition.*)
-lemmas expand_Suc = Suc_pred' [of "number_of v", standard]
-
-subsubsection{*Arith *}
-
-lemma Suc_eq_add_numeral_1: "Suc n = n + 1"
-by (simp add: numerals)
-
-lemma Suc_eq_add_numeral_1_left: "Suc n = 1 + n"
-by (simp add: numerals)
-
-(* These two can be useful when m = number_of... *)
-
-lemma add_eq_if: "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))"
- unfolding One_nat_def by (cases m) simp_all
-
-lemma mult_eq_if: "(m::nat) * n = (if m=0 then 0 else n + ((m - 1) * n))"
- unfolding One_nat_def by (cases m) simp_all
-
-lemma power_eq_if: "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m - 1)))"
- unfolding One_nat_def by (cases m) simp_all
-
-
-subsection{*Comparisons involving (0::nat) *}
-
-text{*Simplification already does @{term "n<0"}, @{term "n\<le>0"} and @{term "0\<le>n"}.*}
-
-lemma eq_number_of_0 [simp]:
- "number_of v = (0::nat) \<longleftrightarrow> v \<le> Int.Pls"
- unfolding nat_number_of_def number_of_is_id numeral_simps
- by auto
-
-lemma eq_0_number_of [simp]:
- "(0::nat) = number_of v \<longleftrightarrow> v \<le> Int.Pls"
-by (rule trans [OF eq_sym_conv eq_number_of_0])
-
-lemma less_0_number_of [simp]:
- "(0::nat) < number_of v \<longleftrightarrow> Int.Pls < v"
- unfolding nat_number_of_def number_of_is_id numeral_simps
- by simp
-
-lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)"
-by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
-
-
-
-subsection{*Comparisons involving @{term Suc} *}
-
-lemma eq_number_of_Suc [simp]:
- "(number_of v = Suc n) =
- (let pv = number_of (Int.pred v) in
- if neg pv then False else nat pv = n)"
-apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less
- number_of_pred nat_number_of_def
- split add: split_if)
-apply (rule_tac x = "number_of v" in spec)
-apply (auto simp add: nat_eq_iff)
-done
-
-lemma Suc_eq_number_of [simp]:
- "(Suc n = number_of v) =
- (let pv = number_of (Int.pred v) in
- if neg pv then False else nat pv = n)"
-by (rule trans [OF eq_sym_conv eq_number_of_Suc])
-
-lemma less_number_of_Suc [simp]:
- "(number_of v < Suc n) =
- (let pv = number_of (Int.pred v) in
- if neg pv then True else nat pv < n)"
-apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less
- number_of_pred nat_number_of_def
- split add: split_if)
-apply (rule_tac x = "number_of v" in spec)
-apply (auto simp add: nat_less_iff)
-done
-
-lemma less_Suc_number_of [simp]:
- "(Suc n < number_of v) =
- (let pv = number_of (Int.pred v) in
- if neg pv then False else n < nat pv)"
-apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less
- number_of_pred nat_number_of_def
- split add: split_if)
-apply (rule_tac x = "number_of v" in spec)
-apply (auto simp add: zless_nat_eq_int_zless)
-done
-
-lemma le_number_of_Suc [simp]:
- "(number_of v <= Suc n) =
- (let pv = number_of (Int.pred v) in
- if neg pv then True else nat pv <= n)"
-by (simp add: Let_def less_Suc_number_of linorder_not_less [symmetric])
-
-lemma le_Suc_number_of [simp]:
- "(Suc n <= number_of v) =
- (let pv = number_of (Int.pred v) in
- if neg pv then False else n <= nat pv)"
-by (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric])
-
-
-lemma eq_number_of_Pls_Min: "(Numeral0 ::int) ~= number_of Int.Min"
-by auto
-
-
-
-subsection{*Max and Min Combined with @{term Suc} *}
-
-lemma max_number_of_Suc [simp]:
- "max (Suc n) (number_of v) =
- (let pv = number_of (Int.pred v) in
- if neg pv then Suc n else Suc(max n (nat pv)))"
-apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def
- split add: split_if nat.split)
-apply (rule_tac x = "number_of v" in spec)
-apply auto
-done
-
-lemma max_Suc_number_of [simp]:
- "max (number_of v) (Suc n) =
- (let pv = number_of (Int.pred v) in
- if neg pv then Suc n else Suc(max (nat pv) n))"
-apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def
- split add: split_if nat.split)
-apply (rule_tac x = "number_of v" in spec)
-apply auto
-done
-
-lemma min_number_of_Suc [simp]:
- "min (Suc n) (number_of v) =
- (let pv = number_of (Int.pred v) in
- if neg pv then 0 else Suc(min n (nat pv)))"
-apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def
- split add: split_if nat.split)
-apply (rule_tac x = "number_of v" in spec)
-apply auto
-done
-
-lemma min_Suc_number_of [simp]:
- "min (number_of v) (Suc n) =
- (let pv = number_of (Int.pred v) in
- if neg pv then 0 else Suc(min (nat pv) n))"
-apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def
- split add: split_if nat.split)
-apply (rule_tac x = "number_of v" in spec)
-apply auto
-done
-
-subsection{*Literal arithmetic involving powers*}
-
-lemma nat_power_eq: "(0::int) <= z ==> nat (z^n) = nat z ^ n"
-apply (induct "n")
-apply (simp_all (no_asm_simp) add: nat_mult_distrib)
-done
-
-lemma power_nat_number_of:
- "(number_of v :: nat) ^ n =
- (if neg (number_of v :: int) then 0^n else nat ((number_of v :: int) ^ n))"
-by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def nat_power_eq
- split add: split_if cong: imp_cong)
-
-
-lemmas power_nat_number_of_number_of = power_nat_number_of [of _ "number_of w", standard]
-declare power_nat_number_of_number_of [simp]
-
-
-
-text{*For arbitrary rings*}
-
-lemma power_number_of_even:
- fixes z :: "'a::{number_ring,recpower}"
- shows "z ^ number_of (Int.Bit0 w) = (let w = z ^ (number_of w) in w * w)"
-unfolding Let_def nat_number_of_def number_of_Bit0
-apply (rule_tac x = "number_of w" in spec, clarify)
-apply (case_tac " (0::int) <= x")
-apply (auto simp add: nat_mult_distrib power_even_eq power2_eq_square)
-done
-
-lemma power_number_of_odd:
- fixes z :: "'a::{number_ring,recpower}"
- shows "z ^ number_of (Int.Bit1 w) = (if (0::int) <= number_of w
- then (let w = z ^ (number_of w) in z * w * w) else 1)"
-unfolding Let_def nat_number_of_def number_of_Bit1
-apply (rule_tac x = "number_of w" in spec, auto)
-apply (simp only: nat_add_distrib nat_mult_distrib)
-apply simp
-apply (auto simp add: nat_add_distrib nat_mult_distrib power_even_eq power2_eq_square neg_nat power_Suc)
-done
-
-lemmas zpower_number_of_even = power_number_of_even [where 'a=int]
-lemmas zpower_number_of_odd = power_number_of_odd [where 'a=int]
-
-lemmas power_number_of_even_number_of [simp] =
- power_number_of_even [of "number_of v", standard]
-
-lemmas power_number_of_odd_number_of [simp] =
- power_number_of_odd [of "number_of v", standard]
-
-
-
-ML
-{*
-val numeral_ss = @{simpset} addsimps @{thms numerals};
-
-val nat_bin_arith_setup =
- Lin_Arith.map_data
- (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
- {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
- inj_thms = inj_thms,
- lessD = lessD, neqE = neqE,
- simpset = simpset addsimps @{thms neg_simps} @
- [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}]})
-*}
-
-declaration {* K nat_bin_arith_setup *}
-
-(* Enable arith to deal with div/mod k where k is a numeral: *)
-declare split_div[of _ _ "number_of k", standard, arith_split]
-declare split_mod[of _ _ "number_of k", standard, arith_split]
-
-lemma nat_number_of_Pls: "Numeral0 = (0::nat)"
- by (simp add: number_of_Pls nat_number_of_def)
-
-lemma nat_number_of_Min: "number_of Int.Min = (0::nat)"
- apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
- done
-
-lemma nat_number_of_Bit0:
- "number_of (Int.Bit0 w) = (let n::nat = number_of w in n + n)"
- unfolding nat_number_of_def number_of_is_id numeral_simps Let_def
- by auto
-
-lemma nat_number_of_Bit1:
- "number_of (Int.Bit1 w) =
- (if neg (number_of w :: int) then 0
- else let n = number_of w in Suc (n + n))"
- unfolding nat_number_of_def number_of_is_id numeral_simps neg_def Let_def
- by auto
-
-lemmas nat_number =
- nat_number_of_Pls nat_number_of_Min
- nat_number_of_Bit0 nat_number_of_Bit1
-
-lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
- by (simp add: Let_def)
-
-lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::{number_ring,recpower})"
-by (simp add: power_mult power_Suc);
-
-lemma power_m1_odd: "(-1) ^ Suc(2*n) = (-1::'a::{number_ring,recpower})"
-by (simp add: power_mult power_Suc);
-
-
-subsection{*Literal arithmetic and @{term of_nat}*}
-
-lemma of_nat_double:
- "0 \<le> x ==> of_nat (nat (2 * x)) = of_nat (nat x) + of_nat (nat x)"
-by (simp only: mult_2 nat_add_distrib of_nat_add)
-
-lemma nat_numeral_m1_eq_0: "-1 = (0::nat)"
-by (simp only: nat_number_of_def)
-
-lemma of_nat_number_of_lemma:
- "of_nat (number_of v :: nat) =
- (if 0 \<le> (number_of v :: int)
- then (number_of v :: 'a :: number_ring)
- else 0)"
-by (simp add: int_number_of_def nat_number_of_def number_of_eq of_nat_nat);
-
-lemma of_nat_number_of_eq [simp]:
- "of_nat (number_of v :: nat) =
- (if neg (number_of v :: int) then 0
- else (number_of v :: 'a :: number_ring))"
-by (simp only: of_nat_number_of_lemma neg_def, simp)
-
-
-subsection {*Lemmas for the Combination and Cancellation Simprocs*}
-
-lemma nat_number_of_add_left:
- "number_of v + (number_of v' + (k::nat)) =
- (if neg (number_of v :: int) then number_of v' + k
- else if neg (number_of v' :: int) then number_of v + k
- else number_of (v + v') + k)"
- unfolding nat_number_of_def number_of_is_id neg_def
- by auto
-
-lemma nat_number_of_mult_left:
- "number_of v * (number_of v' * (k::nat)) =
- (if v < Int.Pls then 0
- else number_of (v * v') * k)"
-by simp
-
-
-subsubsection{*For @{text combine_numerals}*}
-
-lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)"
-by (simp add: add_mult_distrib)
-
-
-subsubsection{*For @{text cancel_numerals}*}
-
-lemma nat_diff_add_eq1:
- "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"
-by (simp split add: nat_diff_split add: add_mult_distrib)
-
-lemma nat_diff_add_eq2:
- "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))"
-by (simp split add: nat_diff_split add: add_mult_distrib)
-
-lemma nat_eq_add_iff1:
- "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)"
-by (auto split add: nat_diff_split simp add: add_mult_distrib)
-
-lemma nat_eq_add_iff2:
- "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)"
-by (auto split add: nat_diff_split simp add: add_mult_distrib)
-
-lemma nat_less_add_iff1:
- "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)"
-by (auto split add: nat_diff_split simp add: add_mult_distrib)
-
-lemma nat_less_add_iff2:
- "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)"
-by (auto split add: nat_diff_split simp add: add_mult_distrib)
-
-lemma nat_le_add_iff1:
- "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"
-by (auto split add: nat_diff_split simp add: add_mult_distrib)
-
-lemma nat_le_add_iff2:
- "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"
-by (auto split add: nat_diff_split simp add: add_mult_distrib)
-
-
-subsubsection{*For @{text cancel_numeral_factors} *}
-
-lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)"
-by auto
-
-lemma nat_mult_less_cancel1: "(0::nat) < k ==> (k*m < k*n) = (m<n)"
-by auto
-
-lemma nat_mult_eq_cancel1: "(0::nat) < k ==> (k*m = k*n) = (m=n)"
-by auto
-
-lemma nat_mult_div_cancel1: "(0::nat) < k ==> (k*m) div (k*n) = (m div n)"
-by auto
-
-lemma nat_mult_dvd_cancel_disj[simp]:
- "(k*m) dvd (k*n) = (k=0 | m dvd (n::nat))"
-by(auto simp: dvd_eq_mod_eq_0 mod_mult_distrib2[symmetric])
-
-lemma nat_mult_dvd_cancel1: "0 < k \<Longrightarrow> (k*m) dvd (k*n::nat) = (m dvd n)"
-by(auto)
-
-
-subsubsection{*For @{text cancel_factor} *}
-
-lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)"
-by auto
-
-lemma nat_mult_less_cancel_disj: "(k*m < k*n) = ((0::nat) < k & m<n)"
-by auto
-
-lemma nat_mult_eq_cancel_disj: "(k*m = k*n) = (k = (0::nat) | m=n)"
-by auto
-
-lemma nat_mult_div_cancel_disj[simp]:
- "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
-by (simp add: nat_mult_div_cancel1)
-
-
-subsection {* Simprocs for the Naturals *}
-
-use "Tools/nat_simprocs.ML"
-declaration {* K nat_simprocs_setup *}
-
-subsubsection{*For simplifying @{term "Suc m - K"} and @{term "K - Suc m"}*}
-
-text{*Where K above is a literal*}
-
-lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)"
-by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split)
-
-text {*Now just instantiating @{text n} to @{text "number_of v"} does
- the right simplification, but with some redundant inequality
- tests.*}
-lemma neg_number_of_pred_iff_0:
- "neg (number_of (Int.pred v)::int) = (number_of v = (0::nat))"
-apply (subgoal_tac "neg (number_of (Int.pred v)) = (number_of v < Suc 0) ")
-apply (simp only: less_Suc_eq_le le_0_eq)
-apply (subst less_number_of_Suc, simp)
-done
-
-text{*No longer required as a simprule because of the @{text inverse_fold}
- simproc*}
-lemma Suc_diff_number_of:
- "Int.Pls < v ==>
- Suc m - (number_of v) = m - (number_of (Int.pred v))"
-apply (subst Suc_diff_eq_diff_pred)
-apply simp
-apply (simp del: nat_numeral_1_eq_1)
-apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric]
- neg_number_of_pred_iff_0)
-done
-
-lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
-by (simp add: numerals split add: nat_diff_split)
-
-
-subsubsection{*For @{term nat_case} and @{term nat_rec}*}
-
-lemma nat_case_number_of [simp]:
- "nat_case a f (number_of v) =
- (let pv = number_of (Int.pred v) in
- if neg pv then a else f (nat pv))"
-by (simp split add: nat.split add: Let_def neg_number_of_pred_iff_0)
-
-lemma nat_case_add_eq_if [simp]:
- "nat_case a f ((number_of v) + n) =
- (let pv = number_of (Int.pred v) in
- if neg pv then nat_case a f n else f (nat pv + n))"
-apply (subst add_eq_if)
-apply (simp split add: nat.split
- del: nat_numeral_1_eq_1
- add: nat_numeral_1_eq_1 [symmetric]
- numeral_1_eq_Suc_0 [symmetric]
- neg_number_of_pred_iff_0)
-done
-
-lemma nat_rec_number_of [simp]:
- "nat_rec a f (number_of v) =
- (let pv = number_of (Int.pred v) in
- if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))"
-apply (case_tac " (number_of v) ::nat")
-apply (simp_all (no_asm_simp) add: Let_def neg_number_of_pred_iff_0)
-apply (simp split add: split_if_asm)
-done
-
-lemma nat_rec_add_eq_if [simp]:
- "nat_rec a f (number_of v + n) =
- (let pv = number_of (Int.pred v) in
- if neg pv then nat_rec a f n
- else f (nat pv + n) (nat_rec a f (nat pv + n)))"
-apply (subst add_eq_if)
-apply (simp split add: nat.split
- del: nat_numeral_1_eq_1
- add: nat_numeral_1_eq_1 [symmetric]
- numeral_1_eq_Suc_0 [symmetric]
- neg_number_of_pred_iff_0)
-done
-
-
-subsubsection{*Various Other Lemmas*}
-
-text {*Evens and Odds, for Mutilated Chess Board*}
-
-text{*Lemmas for specialist use, NOT as default simprules*}
-lemma nat_mult_2: "2 * z = (z+z::nat)"
-proof -
- have "2*z = (1 + 1)*z" by simp
- also have "... = z+z" by (simp add: left_distrib)
- finally show ?thesis .
-qed
-
-lemma nat_mult_2_right: "z * 2 = (z+z::nat)"
-by (subst mult_commute, rule nat_mult_2)
-
-text{*Case analysis on @{term "n<2"}*}
-lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0"
-by arith
-
-lemma div2_Suc_Suc [simp]: "Suc(Suc m) div 2 = Suc (m div 2)"
-by arith
-
-lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
-by (simp add: nat_mult_2 [symmetric])
-
-lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2"
-apply (subgoal_tac "m mod 2 < 2")
-apply (erule less_2_cases [THEN disjE])
-apply (simp_all (no_asm_simp) add: Let_def mod_Suc nat_1)
-done
-
-lemma mod2_gr_0 [simp]: "!!m::nat. (0 < m mod 2) = (m mod 2 = 1)"
-apply (subgoal_tac "m mod 2 < 2")
-apply (force simp del: mod_less_divisor, simp)
-done
-
-text{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*}
-
-lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)"
-by simp
-
-lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)"
-by simp
-
-text{*Can be used to eliminate long strings of Sucs, but not by default*}
-lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n"
-by simp
-
-
-text{*These lemmas collapse some needless occurrences of Suc:
- at least three Sucs, since two and fewer are rewritten back to Suc again!
- We already have some rules to simplify operands smaller than 3.*}
-
-lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
-by (simp add: Suc3_eq_add_3)
-
-lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
-by (simp add: Suc3_eq_add_3)
-
-lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
-by (simp add: Suc3_eq_add_3)
-
-lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
-by (simp add: Suc3_eq_add_3)
-
-lemmas Suc_div_eq_add3_div_number_of =
- Suc_div_eq_add3_div [of _ "number_of v", standard]
-declare Suc_div_eq_add3_div_number_of [simp]
-
-lemmas Suc_mod_eq_add3_mod_number_of =
- Suc_mod_eq_add3_mod [of _ "number_of v", standard]
-declare Suc_mod_eq_add3_mod_number_of [simp]
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nat_Numeral.thy Fri Apr 17 08:36:18 2009 +0200
@@ -0,0 +1,975 @@
+(* Title: HOL/Nat_Numeral.thy
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1999 University of Cambridge
+*)
+
+header {* Binary numerals for the natural numbers *}
+
+theory Nat_Numeral
+imports IntDiv
+uses ("Tools/nat_simprocs.ML")
+begin
+
+text {*
+ Arithmetic for naturals is reduced to that for the non-negative integers.
+*}
+
+instantiation nat :: number
+begin
+
+definition
+ nat_number_of_def [code inline, code del]: "number_of v = nat (number_of v)"
+
+instance ..
+
+end
+
+lemma [code post]:
+ "nat (number_of v) = number_of v"
+ unfolding nat_number_of_def ..
+
+abbreviation (xsymbols)
+ power2 :: "'a::power => 'a" ("(_\<twosuperior>)" [1000] 999) where
+ "x\<twosuperior> == x^2"
+
+notation (latex output)
+ power2 ("(_\<twosuperior>)" [1000] 999)
+
+notation (HTML output)
+ power2 ("(_\<twosuperior>)" [1000] 999)
+
+
+subsection {* Predicate for negative binary numbers *}
+
+definition neg :: "int \<Rightarrow> bool" where
+ "neg Z \<longleftrightarrow> Z < 0"
+
+lemma not_neg_int [simp]: "~ neg (of_nat n)"
+by (simp add: neg_def)
+
+lemma neg_zminus_int [simp]: "neg (- (of_nat (Suc n)))"
+by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc)
+
+lemmas neg_eq_less_0 = neg_def
+
+lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)"
+by (simp add: neg_def linorder_not_less)
+
+text{*To simplify inequalities when Numeral1 can get simplified to 1*}
+
+lemma not_neg_0: "~ neg 0"
+by (simp add: One_int_def neg_def)
+
+lemma not_neg_1: "~ neg 1"
+by (simp add: neg_def linorder_not_less zero_le_one)
+
+lemma neg_nat: "neg z ==> nat z = 0"
+by (simp add: neg_def order_less_imp_le)
+
+lemma not_neg_nat: "~ neg z ==> of_nat (nat z) = z"
+by (simp add: linorder_not_less neg_def)
+
+text {*
+ If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
+ @{term Numeral0} IS @{term "number_of Pls"}
+*}
+
+lemma not_neg_number_of_Pls: "~ neg (number_of Int.Pls)"
+ by (simp add: neg_def)
+
+lemma neg_number_of_Min: "neg (number_of Int.Min)"
+ by (simp add: neg_def)
+
+lemma neg_number_of_Bit0:
+ "neg (number_of (Int.Bit0 w)) = neg (number_of w)"
+ by (simp add: neg_def)
+
+lemma neg_number_of_Bit1:
+ "neg (number_of (Int.Bit1 w)) = neg (number_of w)"
+ by (simp add: neg_def)
+
+lemmas neg_simps [simp] =
+ not_neg_0 not_neg_1
+ not_neg_number_of_Pls neg_number_of_Min
+ neg_number_of_Bit0 neg_number_of_Bit1
+
+
+subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*}
+
+declare nat_0 [simp] nat_1 [simp]
+
+lemma nat_number_of [simp]: "nat (number_of w) = number_of w"
+by (simp add: nat_number_of_def)
+
+lemma nat_numeral_0_eq_0 [simp]: "Numeral0 = (0::nat)"
+by (simp add: nat_number_of_def)
+
+lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)"
+by (simp add: nat_1 nat_number_of_def)
+
+lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
+by (simp add: nat_numeral_1_eq_1)
+
+lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
+apply (unfold nat_number_of_def)
+apply (rule nat_2)
+done
+
+
+subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
+
+lemma int_nat_number_of [simp]:
+ "int (number_of v) =
+ (if neg (number_of v :: int) then 0
+ else (number_of v :: int))"
+ unfolding nat_number_of_def number_of_is_id neg_def
+ by simp
+
+
+subsubsection{*Successor *}
+
+lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
+apply (rule sym)
+apply (simp add: nat_eq_iff int_Suc)
+done
+
+lemma Suc_nat_number_of_add:
+ "Suc (number_of v + n) =
+ (if neg (number_of v :: int) then 1+n else number_of (Int.succ v) + n)"
+ unfolding nat_number_of_def number_of_is_id neg_def numeral_simps
+ by (simp add: Suc_nat_eq_nat_zadd1 add_ac)
+
+lemma Suc_nat_number_of [simp]:
+ "Suc (number_of v) =
+ (if neg (number_of v :: int) then 1 else number_of (Int.succ v))"
+apply (cut_tac n = 0 in Suc_nat_number_of_add)
+apply (simp cong del: if_weak_cong)
+done
+
+
+subsubsection{*Addition *}
+
+lemma add_nat_number_of [simp]:
+ "(number_of v :: nat) + number_of v' =
+ (if v < Int.Pls then number_of v'
+ else if v' < Int.Pls then number_of v
+ else number_of (v + v'))"
+ unfolding nat_number_of_def number_of_is_id numeral_simps
+ by (simp add: nat_add_distrib)
+
+lemma nat_number_of_add_1 [simp]:
+ "number_of v + (1::nat) =
+ (if v < Int.Pls then 1 else number_of (Int.succ v))"
+ unfolding nat_number_of_def number_of_is_id numeral_simps
+ by (simp add: nat_add_distrib)
+
+lemma nat_1_add_number_of [simp]:
+ "(1::nat) + number_of v =
+ (if v < Int.Pls then 1 else number_of (Int.succ v))"
+ unfolding nat_number_of_def number_of_is_id numeral_simps
+ by (simp add: nat_add_distrib)
+
+lemma nat_1_add_1 [simp]: "1 + 1 = (2::nat)"
+ by (rule int_int_eq [THEN iffD1]) simp
+
+
+subsubsection{*Subtraction *}
+
+lemma diff_nat_eq_if:
+ "nat z - nat z' =
+ (if neg z' then nat z
+ else let d = z-z' in
+ if neg d then 0 else nat d)"
+by (simp add: Let_def nat_diff_distrib [symmetric] neg_eq_less_0 not_neg_eq_ge_0)
+
+
+lemma diff_nat_number_of [simp]:
+ "(number_of v :: nat) - number_of v' =
+ (if v' < Int.Pls then number_of v
+ else let d = number_of (v + uminus v') in
+ if neg d then 0 else nat d)"
+ unfolding nat_number_of_def number_of_is_id numeral_simps neg_def
+ by auto
+
+lemma nat_number_of_diff_1 [simp]:
+ "number_of v - (1::nat) =
+ (if v \<le> Int.Pls then 0 else number_of (Int.pred v))"
+ unfolding nat_number_of_def number_of_is_id numeral_simps
+ by auto
+
+
+subsubsection{*Multiplication *}
+
+lemma mult_nat_number_of [simp]:
+ "(number_of v :: nat) * number_of v' =
+ (if v < Int.Pls then 0 else number_of (v * v'))"
+ unfolding nat_number_of_def number_of_is_id numeral_simps
+ by (simp add: nat_mult_distrib)
+
+
+subsubsection{*Quotient *}
+
+lemma div_nat_number_of [simp]:
+ "(number_of v :: nat) div number_of v' =
+ (if neg (number_of v :: int) then 0
+ else nat (number_of v div number_of v'))"
+ unfolding nat_number_of_def number_of_is_id neg_def
+ by (simp add: nat_div_distrib)
+
+lemma one_div_nat_number_of [simp]:
+ "Suc 0 div number_of v' = nat (1 div number_of v')"
+by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric])
+
+
+subsubsection{*Remainder *}
+
+lemma mod_nat_number_of [simp]:
+ "(number_of v :: nat) mod number_of v' =
+ (if neg (number_of v :: int) then 0
+ else if neg (number_of v' :: int) then number_of v
+ else nat (number_of v mod number_of v'))"
+ unfolding nat_number_of_def number_of_is_id neg_def
+ by (simp add: nat_mod_distrib)
+
+lemma one_mod_nat_number_of [simp]:
+ "Suc 0 mod number_of v' =
+ (if neg (number_of v' :: int) then Suc 0
+ else nat (1 mod number_of v'))"
+by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric])
+
+
+subsubsection{* Divisibility *}
+
+lemmas dvd_eq_mod_eq_0_number_of =
+ dvd_eq_mod_eq_0 [of "number_of x" "number_of y", standard]
+
+declare dvd_eq_mod_eq_0_number_of [simp]
+
+ML
+{*
+val nat_number_of_def = thm"nat_number_of_def";
+
+val nat_number_of = thm"nat_number_of";
+val nat_numeral_0_eq_0 = thm"nat_numeral_0_eq_0";
+val nat_numeral_1_eq_1 = thm"nat_numeral_1_eq_1";
+val numeral_1_eq_Suc_0 = thm"numeral_1_eq_Suc_0";
+val numeral_2_eq_2 = thm"numeral_2_eq_2";
+val nat_div_distrib = thm"nat_div_distrib";
+val nat_mod_distrib = thm"nat_mod_distrib";
+val int_nat_number_of = thm"int_nat_number_of";
+val Suc_nat_eq_nat_zadd1 = thm"Suc_nat_eq_nat_zadd1";
+val Suc_nat_number_of_add = thm"Suc_nat_number_of_add";
+val Suc_nat_number_of = thm"Suc_nat_number_of";
+val add_nat_number_of = thm"add_nat_number_of";
+val diff_nat_eq_if = thm"diff_nat_eq_if";
+val diff_nat_number_of = thm"diff_nat_number_of";
+val mult_nat_number_of = thm"mult_nat_number_of";
+val div_nat_number_of = thm"div_nat_number_of";
+val mod_nat_number_of = thm"mod_nat_number_of";
+*}
+
+
+subsection{*Comparisons*}
+
+subsubsection{*Equals (=) *}
+
+lemma eq_nat_nat_iff:
+ "[| (0::int) <= z; 0 <= z' |] ==> (nat z = nat z') = (z=z')"
+by (auto elim!: nonneg_eq_int)
+
+lemma eq_nat_number_of [simp]:
+ "((number_of v :: nat) = number_of v') =
+ (if neg (number_of v :: int) then (number_of v' :: int) \<le> 0
+ else if neg (number_of v' :: int) then (number_of v :: int) = 0
+ else v = v')"
+ unfolding nat_number_of_def number_of_is_id neg_def
+ by auto
+
+
+subsubsection{*Less-than (<) *}
+
+lemma less_nat_number_of [simp]:
+ "(number_of v :: nat) < number_of v' \<longleftrightarrow>
+ (if v < v' then Int.Pls < v' else False)"
+ unfolding nat_number_of_def number_of_is_id numeral_simps
+ by auto
+
+
+subsubsection{*Less-than-or-equal *}
+
+lemma le_nat_number_of [simp]:
+ "(number_of v :: nat) \<le> number_of v' \<longleftrightarrow>
+ (if v \<le> v' then True else v \<le> Int.Pls)"
+ unfolding nat_number_of_def number_of_is_id numeral_simps
+ by auto
+
+(*Maps #n to n for n = 0, 1, 2*)
+lemmas numerals = nat_numeral_0_eq_0 nat_numeral_1_eq_1 numeral_2_eq_2
+
+
+subsection{*Powers with Numeric Exponents*}
+
+text{*We cannot refer to the number @{term 2} in @{text Ring_and_Field.thy}.
+We cannot prove general results about the numeral @{term "-1"}, so we have to
+use @{term "- 1"} instead.*}
+
+lemma power2_eq_square: "(a::'a::recpower)\<twosuperior> = a * a"
+ by (simp add: numeral_2_eq_2 Power.power_Suc)
+
+lemma zero_power2 [simp]: "(0::'a::{semiring_1,recpower})\<twosuperior> = 0"
+ by (simp add: power2_eq_square)
+
+lemma one_power2 [simp]: "(1::'a::{semiring_1,recpower})\<twosuperior> = 1"
+ by (simp add: power2_eq_square)
+
+lemma power3_eq_cube: "(x::'a::recpower) ^ 3 = x * x * x"
+ apply (subgoal_tac "3 = Suc (Suc (Suc 0))")
+ apply (erule ssubst)
+ apply (simp add: power_Suc mult_ac)
+ apply (unfold nat_number_of_def)
+ apply (subst nat_eq_iff)
+ apply simp
+done
+
+text{*Squares of literal numerals will be evaluated.*}
+lemmas power2_eq_square_number_of =
+ power2_eq_square [of "number_of w", standard]
+declare power2_eq_square_number_of [simp]
+
+
+lemma zero_le_power2[simp]: "0 \<le> (a\<twosuperior>::'a::{ordered_idom,recpower})"
+ by (simp add: power2_eq_square)
+
+lemma zero_less_power2[simp]:
+ "(0 < a\<twosuperior>) = (a \<noteq> (0::'a::{ordered_idom,recpower}))"
+ by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
+
+lemma power2_less_0[simp]:
+ fixes a :: "'a::{ordered_idom,recpower}"
+ shows "~ (a\<twosuperior> < 0)"
+by (force simp add: power2_eq_square mult_less_0_iff)
+
+lemma zero_eq_power2[simp]:
+ "(a\<twosuperior> = 0) = (a = (0::'a::{ordered_idom,recpower}))"
+ by (force simp add: power2_eq_square mult_eq_0_iff)
+
+lemma abs_power2[simp]:
+ "abs(a\<twosuperior>) = (a\<twosuperior>::'a::{ordered_idom,recpower})"
+ by (simp add: power2_eq_square abs_mult abs_mult_self)
+
+lemma power2_abs[simp]:
+ "(abs a)\<twosuperior> = (a\<twosuperior>::'a::{ordered_idom,recpower})"
+ by (simp add: power2_eq_square abs_mult_self)
+
+lemma power2_minus[simp]:
+ "(- a)\<twosuperior> = (a\<twosuperior>::'a::{comm_ring_1,recpower})"
+ by (simp add: power2_eq_square)
+
+lemma power2_le_imp_le:
+ fixes x y :: "'a::{ordered_semidom,recpower}"
+ shows "\<lbrakk>x\<twosuperior> \<le> y\<twosuperior>; 0 \<le> y\<rbrakk> \<Longrightarrow> x \<le> y"
+unfolding numeral_2_eq_2 by (rule power_le_imp_le_base)
+
+lemma power2_less_imp_less:
+ fixes x y :: "'a::{ordered_semidom,recpower}"
+ shows "\<lbrakk>x\<twosuperior> < y\<twosuperior>; 0 \<le> y\<rbrakk> \<Longrightarrow> x < y"
+by (rule power_less_imp_less_base)
+
+lemma power2_eq_imp_eq:
+ fixes x y :: "'a::{ordered_semidom,recpower}"
+ shows "\<lbrakk>x\<twosuperior> = y\<twosuperior>; 0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> x = y"
+unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base, simp)
+
+lemma power_minus1_even[simp]: "(- 1) ^ (2*n) = (1::'a::{comm_ring_1,recpower})"
+proof (induct n)
+ case 0 show ?case by simp
+next
+ case (Suc n) then show ?case by (simp add: power_Suc power_add)
+qed
+
+lemma power_minus1_odd: "(- 1) ^ Suc(2*n) = -(1::'a::{comm_ring_1,recpower})"
+ by (simp add: power_Suc)
+
+lemma power_even_eq: "(a::'a::recpower) ^ (2*n) = (a^n)^2"
+by (subst mult_commute) (simp add: power_mult)
+
+lemma power_odd_eq: "(a::int) ^ Suc(2*n) = a * (a^n)^2"
+by (simp add: power_even_eq)
+
+lemma power_minus_even [simp]:
+ "(-a) ^ (2*n) = (a::'a::{comm_ring_1,recpower}) ^ (2*n)"
+by (simp add: power_minus1_even power_minus [of a])
+
+lemma zero_le_even_power'[simp]:
+ "0 \<le> (a::'a::{ordered_idom,recpower}) ^ (2*n)"
+proof (induct "n")
+ case 0
+ show ?case by (simp add: zero_le_one)
+next
+ case (Suc n)
+ have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)"
+ by (simp add: mult_ac power_add power2_eq_square)
+ thus ?case
+ by (simp add: prems zero_le_mult_iff)
+qed
+
+lemma odd_power_less_zero:
+ "(a::'a::{ordered_idom,recpower}) < 0 ==> a ^ Suc(2*n) < 0"
+proof (induct "n")
+ case 0
+ then show ?case by simp
+next
+ case (Suc n)
+ have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)"
+ by (simp add: mult_ac power_add power2_eq_square)
+ thus ?case
+ by (simp del: power_Suc add: prems mult_less_0_iff mult_neg_neg)
+qed
+
+lemma odd_0_le_power_imp_0_le:
+ "0 \<le> a ^ Suc(2*n) ==> 0 \<le> (a::'a::{ordered_idom,recpower})"
+apply (insert odd_power_less_zero [of a n])
+apply (force simp add: linorder_not_less [symmetric])
+done
+
+text{*Simprules for comparisons where common factors can be cancelled.*}
+lemmas zero_compare_simps =
+ add_strict_increasing add_strict_increasing2 add_increasing
+ zero_le_mult_iff zero_le_divide_iff
+ zero_less_mult_iff zero_less_divide_iff
+ mult_le_0_iff divide_le_0_iff
+ mult_less_0_iff divide_less_0_iff
+ zero_le_power2 power2_less_0
+
+subsubsection{*Nat *}
+
+lemma Suc_pred': "0 < n ==> n = Suc(n - 1)"
+by (simp add: numerals)
+
+(*Expresses a natural number constant as the Suc of another one.
+ NOT suitable for rewriting because n recurs in the condition.*)
+lemmas expand_Suc = Suc_pred' [of "number_of v", standard]
+
+subsubsection{*Arith *}
+
+lemma Suc_eq_add_numeral_1: "Suc n = n + 1"
+by (simp add: numerals)
+
+lemma Suc_eq_add_numeral_1_left: "Suc n = 1 + n"
+by (simp add: numerals)
+
+(* These two can be useful when m = number_of... *)
+
+lemma add_eq_if: "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))"
+ unfolding One_nat_def by (cases m) simp_all
+
+lemma mult_eq_if: "(m::nat) * n = (if m=0 then 0 else n + ((m - 1) * n))"
+ unfolding One_nat_def by (cases m) simp_all
+
+lemma power_eq_if: "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m - 1)))"
+ unfolding One_nat_def by (cases m) simp_all
+
+
+subsection{*Comparisons involving (0::nat) *}
+
+text{*Simplification already does @{term "n<0"}, @{term "n\<le>0"} and @{term "0\<le>n"}.*}
+
+lemma eq_number_of_0 [simp]:
+ "number_of v = (0::nat) \<longleftrightarrow> v \<le> Int.Pls"
+ unfolding nat_number_of_def number_of_is_id numeral_simps
+ by auto
+
+lemma eq_0_number_of [simp]:
+ "(0::nat) = number_of v \<longleftrightarrow> v \<le> Int.Pls"
+by (rule trans [OF eq_sym_conv eq_number_of_0])
+
+lemma less_0_number_of [simp]:
+ "(0::nat) < number_of v \<longleftrightarrow> Int.Pls < v"
+ unfolding nat_number_of_def number_of_is_id numeral_simps
+ by simp
+
+lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)"
+by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
+
+
+
+subsection{*Comparisons involving @{term Suc} *}
+
+lemma eq_number_of_Suc [simp]:
+ "(number_of v = Suc n) =
+ (let pv = number_of (Int.pred v) in
+ if neg pv then False else nat pv = n)"
+apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less
+ number_of_pred nat_number_of_def
+ split add: split_if)
+apply (rule_tac x = "number_of v" in spec)
+apply (auto simp add: nat_eq_iff)
+done
+
+lemma Suc_eq_number_of [simp]:
+ "(Suc n = number_of v) =
+ (let pv = number_of (Int.pred v) in
+ if neg pv then False else nat pv = n)"
+by (rule trans [OF eq_sym_conv eq_number_of_Suc])
+
+lemma less_number_of_Suc [simp]:
+ "(number_of v < Suc n) =
+ (let pv = number_of (Int.pred v) in
+ if neg pv then True else nat pv < n)"
+apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less
+ number_of_pred nat_number_of_def
+ split add: split_if)
+apply (rule_tac x = "number_of v" in spec)
+apply (auto simp add: nat_less_iff)
+done
+
+lemma less_Suc_number_of [simp]:
+ "(Suc n < number_of v) =
+ (let pv = number_of (Int.pred v) in
+ if neg pv then False else n < nat pv)"
+apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less
+ number_of_pred nat_number_of_def
+ split add: split_if)
+apply (rule_tac x = "number_of v" in spec)
+apply (auto simp add: zless_nat_eq_int_zless)
+done
+
+lemma le_number_of_Suc [simp]:
+ "(number_of v <= Suc n) =
+ (let pv = number_of (Int.pred v) in
+ if neg pv then True else nat pv <= n)"
+by (simp add: Let_def less_Suc_number_of linorder_not_less [symmetric])
+
+lemma le_Suc_number_of [simp]:
+ "(Suc n <= number_of v) =
+ (let pv = number_of (Int.pred v) in
+ if neg pv then False else n <= nat pv)"
+by (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric])
+
+
+lemma eq_number_of_Pls_Min: "(Numeral0 ::int) ~= number_of Int.Min"
+by auto
+
+
+
+subsection{*Max and Min Combined with @{term Suc} *}
+
+lemma max_number_of_Suc [simp]:
+ "max (Suc n) (number_of v) =
+ (let pv = number_of (Int.pred v) in
+ if neg pv then Suc n else Suc(max n (nat pv)))"
+apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def
+ split add: split_if nat.split)
+apply (rule_tac x = "number_of v" in spec)
+apply auto
+done
+
+lemma max_Suc_number_of [simp]:
+ "max (number_of v) (Suc n) =
+ (let pv = number_of (Int.pred v) in
+ if neg pv then Suc n else Suc(max (nat pv) n))"
+apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def
+ split add: split_if nat.split)
+apply (rule_tac x = "number_of v" in spec)
+apply auto
+done
+
+lemma min_number_of_Suc [simp]:
+ "min (Suc n) (number_of v) =
+ (let pv = number_of (Int.pred v) in
+ if neg pv then 0 else Suc(min n (nat pv)))"
+apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def
+ split add: split_if nat.split)
+apply (rule_tac x = "number_of v" in spec)
+apply auto
+done
+
+lemma min_Suc_number_of [simp]:
+ "min (number_of v) (Suc n) =
+ (let pv = number_of (Int.pred v) in
+ if neg pv then 0 else Suc(min (nat pv) n))"
+apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def
+ split add: split_if nat.split)
+apply (rule_tac x = "number_of v" in spec)
+apply auto
+done
+
+subsection{*Literal arithmetic involving powers*}
+
+lemma nat_power_eq: "(0::int) <= z ==> nat (z^n) = nat z ^ n"
+apply (induct "n")
+apply (simp_all (no_asm_simp) add: nat_mult_distrib)
+done
+
+lemma power_nat_number_of:
+ "(number_of v :: nat) ^ n =
+ (if neg (number_of v :: int) then 0^n else nat ((number_of v :: int) ^ n))"
+by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def nat_power_eq
+ split add: split_if cong: imp_cong)
+
+
+lemmas power_nat_number_of_number_of = power_nat_number_of [of _ "number_of w", standard]
+declare power_nat_number_of_number_of [simp]
+
+
+
+text{*For arbitrary rings*}
+
+lemma power_number_of_even:
+ fixes z :: "'a::{number_ring,recpower}"
+ shows "z ^ number_of (Int.Bit0 w) = (let w = z ^ (number_of w) in w * w)"
+unfolding Let_def nat_number_of_def number_of_Bit0
+apply (rule_tac x = "number_of w" in spec, clarify)
+apply (case_tac " (0::int) <= x")
+apply (auto simp add: nat_mult_distrib power_even_eq power2_eq_square)
+done
+
+lemma power_number_of_odd:
+ fixes z :: "'a::{number_ring,recpower}"
+ shows "z ^ number_of (Int.Bit1 w) = (if (0::int) <= number_of w
+ then (let w = z ^ (number_of w) in z * w * w) else 1)"
+unfolding Let_def nat_number_of_def number_of_Bit1
+apply (rule_tac x = "number_of w" in spec, auto)
+apply (simp only: nat_add_distrib nat_mult_distrib)
+apply simp
+apply (auto simp add: nat_add_distrib nat_mult_distrib power_even_eq power2_eq_square neg_nat power_Suc)
+done
+
+lemmas zpower_number_of_even = power_number_of_even [where 'a=int]
+lemmas zpower_number_of_odd = power_number_of_odd [where 'a=int]
+
+lemmas power_number_of_even_number_of [simp] =
+ power_number_of_even [of "number_of v", standard]
+
+lemmas power_number_of_odd_number_of [simp] =
+ power_number_of_odd [of "number_of v", standard]
+
+
+
+ML
+{*
+val numeral_ss = @{simpset} addsimps @{thms numerals};
+
+val nat_bin_arith_setup =
+ Lin_Arith.map_data
+ (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
+ {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
+ inj_thms = inj_thms,
+ lessD = lessD, neqE = neqE,
+ simpset = simpset addsimps @{thms neg_simps} @
+ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}]})
+*}
+
+declaration {* K nat_bin_arith_setup *}
+
+(* Enable arith to deal with div/mod k where k is a numeral: *)
+declare split_div[of _ _ "number_of k", standard, arith_split]
+declare split_mod[of _ _ "number_of k", standard, arith_split]
+
+lemma nat_number_of_Pls: "Numeral0 = (0::nat)"
+ by (simp add: number_of_Pls nat_number_of_def)
+
+lemma nat_number_of_Min: "number_of Int.Min = (0::nat)"
+ apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
+ done
+
+lemma nat_number_of_Bit0:
+ "number_of (Int.Bit0 w) = (let n::nat = number_of w in n + n)"
+ unfolding nat_number_of_def number_of_is_id numeral_simps Let_def
+ by auto
+
+lemma nat_number_of_Bit1:
+ "number_of (Int.Bit1 w) =
+ (if neg (number_of w :: int) then 0
+ else let n = number_of w in Suc (n + n))"
+ unfolding nat_number_of_def number_of_is_id numeral_simps neg_def Let_def
+ by auto
+
+lemmas nat_number =
+ nat_number_of_Pls nat_number_of_Min
+ nat_number_of_Bit0 nat_number_of_Bit1
+
+lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
+ by (simp add: Let_def)
+
+lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::{number_ring,recpower})"
+by (simp add: power_mult power_Suc);
+
+lemma power_m1_odd: "(-1) ^ Suc(2*n) = (-1::'a::{number_ring,recpower})"
+by (simp add: power_mult power_Suc);
+
+
+subsection{*Literal arithmetic and @{term of_nat}*}
+
+lemma of_nat_double:
+ "0 \<le> x ==> of_nat (nat (2 * x)) = of_nat (nat x) + of_nat (nat x)"
+by (simp only: mult_2 nat_add_distrib of_nat_add)
+
+lemma nat_numeral_m1_eq_0: "-1 = (0::nat)"
+by (simp only: nat_number_of_def)
+
+lemma of_nat_number_of_lemma:
+ "of_nat (number_of v :: nat) =
+ (if 0 \<le> (number_of v :: int)
+ then (number_of v :: 'a :: number_ring)
+ else 0)"
+by (simp add: int_number_of_def nat_number_of_def number_of_eq of_nat_nat);
+
+lemma of_nat_number_of_eq [simp]:
+ "of_nat (number_of v :: nat) =
+ (if neg (number_of v :: int) then 0
+ else (number_of v :: 'a :: number_ring))"
+by (simp only: of_nat_number_of_lemma neg_def, simp)
+
+
+subsection {*Lemmas for the Combination and Cancellation Simprocs*}
+
+lemma nat_number_of_add_left:
+ "number_of v + (number_of v' + (k::nat)) =
+ (if neg (number_of v :: int) then number_of v' + k
+ else if neg (number_of v' :: int) then number_of v + k
+ else number_of (v + v') + k)"
+ unfolding nat_number_of_def number_of_is_id neg_def
+ by auto
+
+lemma nat_number_of_mult_left:
+ "number_of v * (number_of v' * (k::nat)) =
+ (if v < Int.Pls then 0
+ else number_of (v * v') * k)"
+by simp
+
+
+subsubsection{*For @{text combine_numerals}*}
+
+lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)"
+by (simp add: add_mult_distrib)
+
+
+subsubsection{*For @{text cancel_numerals}*}
+
+lemma nat_diff_add_eq1:
+ "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"
+by (simp split add: nat_diff_split add: add_mult_distrib)
+
+lemma nat_diff_add_eq2:
+ "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))"
+by (simp split add: nat_diff_split add: add_mult_distrib)
+
+lemma nat_eq_add_iff1:
+ "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)"
+by (auto split add: nat_diff_split simp add: add_mult_distrib)
+
+lemma nat_eq_add_iff2:
+ "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)"
+by (auto split add: nat_diff_split simp add: add_mult_distrib)
+
+lemma nat_less_add_iff1:
+ "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)"
+by (auto split add: nat_diff_split simp add: add_mult_distrib)
+
+lemma nat_less_add_iff2:
+ "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)"
+by (auto split add: nat_diff_split simp add: add_mult_distrib)
+
+lemma nat_le_add_iff1:
+ "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"
+by (auto split add: nat_diff_split simp add: add_mult_distrib)
+
+lemma nat_le_add_iff2:
+ "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"
+by (auto split add: nat_diff_split simp add: add_mult_distrib)
+
+
+subsubsection{*For @{text cancel_numeral_factors} *}
+
+lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)"
+by auto
+
+lemma nat_mult_less_cancel1: "(0::nat) < k ==> (k*m < k*n) = (m<n)"
+by auto
+
+lemma nat_mult_eq_cancel1: "(0::nat) < k ==> (k*m = k*n) = (m=n)"
+by auto
+
+lemma nat_mult_div_cancel1: "(0::nat) < k ==> (k*m) div (k*n) = (m div n)"
+by auto
+
+lemma nat_mult_dvd_cancel_disj[simp]:
+ "(k*m) dvd (k*n) = (k=0 | m dvd (n::nat))"
+by(auto simp: dvd_eq_mod_eq_0 mod_mult_distrib2[symmetric])
+
+lemma nat_mult_dvd_cancel1: "0 < k \<Longrightarrow> (k*m) dvd (k*n::nat) = (m dvd n)"
+by(auto)
+
+
+subsubsection{*For @{text cancel_factor} *}
+
+lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)"
+by auto
+
+lemma nat_mult_less_cancel_disj: "(k*m < k*n) = ((0::nat) < k & m<n)"
+by auto
+
+lemma nat_mult_eq_cancel_disj: "(k*m = k*n) = (k = (0::nat) | m=n)"
+by auto
+
+lemma nat_mult_div_cancel_disj[simp]:
+ "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
+by (simp add: nat_mult_div_cancel1)
+
+
+subsection {* Simprocs for the Naturals *}
+
+use "Tools/nat_simprocs.ML"
+declaration {* K nat_simprocs_setup *}
+
+subsubsection{*For simplifying @{term "Suc m - K"} and @{term "K - Suc m"}*}
+
+text{*Where K above is a literal*}
+
+lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)"
+by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split)
+
+text {*Now just instantiating @{text n} to @{text "number_of v"} does
+ the right simplification, but with some redundant inequality
+ tests.*}
+lemma neg_number_of_pred_iff_0:
+ "neg (number_of (Int.pred v)::int) = (number_of v = (0::nat))"
+apply (subgoal_tac "neg (number_of (Int.pred v)) = (number_of v < Suc 0) ")
+apply (simp only: less_Suc_eq_le le_0_eq)
+apply (subst less_number_of_Suc, simp)
+done
+
+text{*No longer required as a simprule because of the @{text inverse_fold}
+ simproc*}
+lemma Suc_diff_number_of:
+ "Int.Pls < v ==>
+ Suc m - (number_of v) = m - (number_of (Int.pred v))"
+apply (subst Suc_diff_eq_diff_pred)
+apply simp
+apply (simp del: nat_numeral_1_eq_1)
+apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric]
+ neg_number_of_pred_iff_0)
+done
+
+lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
+by (simp add: numerals split add: nat_diff_split)
+
+
+subsubsection{*For @{term nat_case} and @{term nat_rec}*}
+
+lemma nat_case_number_of [simp]:
+ "nat_case a f (number_of v) =
+ (let pv = number_of (Int.pred v) in
+ if neg pv then a else f (nat pv))"
+by (simp split add: nat.split add: Let_def neg_number_of_pred_iff_0)
+
+lemma nat_case_add_eq_if [simp]:
+ "nat_case a f ((number_of v) + n) =
+ (let pv = number_of (Int.pred v) in
+ if neg pv then nat_case a f n else f (nat pv + n))"
+apply (subst add_eq_if)
+apply (simp split add: nat.split
+ del: nat_numeral_1_eq_1
+ add: nat_numeral_1_eq_1 [symmetric]
+ numeral_1_eq_Suc_0 [symmetric]
+ neg_number_of_pred_iff_0)
+done
+
+lemma nat_rec_number_of [simp]:
+ "nat_rec a f (number_of v) =
+ (let pv = number_of (Int.pred v) in
+ if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))"
+apply (case_tac " (number_of v) ::nat")
+apply (simp_all (no_asm_simp) add: Let_def neg_number_of_pred_iff_0)
+apply (simp split add: split_if_asm)
+done
+
+lemma nat_rec_add_eq_if [simp]:
+ "nat_rec a f (number_of v + n) =
+ (let pv = number_of (Int.pred v) in
+ if neg pv then nat_rec a f n
+ else f (nat pv + n) (nat_rec a f (nat pv + n)))"
+apply (subst add_eq_if)
+apply (simp split add: nat.split
+ del: nat_numeral_1_eq_1
+ add: nat_numeral_1_eq_1 [symmetric]
+ numeral_1_eq_Suc_0 [symmetric]
+ neg_number_of_pred_iff_0)
+done
+
+
+subsubsection{*Various Other Lemmas*}
+
+text {*Evens and Odds, for Mutilated Chess Board*}
+
+text{*Lemmas for specialist use, NOT as default simprules*}
+lemma nat_mult_2: "2 * z = (z+z::nat)"
+proof -
+ have "2*z = (1 + 1)*z" by simp
+ also have "... = z+z" by (simp add: left_distrib)
+ finally show ?thesis .
+qed
+
+lemma nat_mult_2_right: "z * 2 = (z+z::nat)"
+by (subst mult_commute, rule nat_mult_2)
+
+text{*Case analysis on @{term "n<2"}*}
+lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0"
+by arith
+
+lemma div2_Suc_Suc [simp]: "Suc(Suc m) div 2 = Suc (m div 2)"
+by arith
+
+lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
+by (simp add: nat_mult_2 [symmetric])
+
+lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2"
+apply (subgoal_tac "m mod 2 < 2")
+apply (erule less_2_cases [THEN disjE])
+apply (simp_all (no_asm_simp) add: Let_def mod_Suc nat_1)
+done
+
+lemma mod2_gr_0 [simp]: "!!m::nat. (0 < m mod 2) = (m mod 2 = 1)"
+apply (subgoal_tac "m mod 2 < 2")
+apply (force simp del: mod_less_divisor, simp)
+done
+
+text{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*}
+
+lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)"
+by simp
+
+lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)"
+by simp
+
+text{*Can be used to eliminate long strings of Sucs, but not by default*}
+lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n"
+by simp
+
+
+text{*These lemmas collapse some needless occurrences of Suc:
+ at least three Sucs, since two and fewer are rewritten back to Suc again!
+ We already have some rules to simplify operands smaller than 3.*}
+
+lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
+by (simp add: Suc3_eq_add_3)
+
+lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
+by (simp add: Suc3_eq_add_3)
+
+lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
+by (simp add: Suc3_eq_add_3)
+
+lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
+by (simp add: Suc3_eq_add_3)
+
+lemmas Suc_div_eq_add3_div_number_of =
+ Suc_div_eq_add3_div [of _ "number_of v", standard]
+declare Suc_div_eq_add3_div_number_of [simp]
+
+lemmas Suc_mod_eq_add3_mod_number_of =
+ Suc_mod_eq_add3_mod [of _ "number_of v", standard]
+declare Suc_mod_eq_add3_mod_number_of [simp]
+
+end
--- a/src/HOL/Orderings.thy Thu Apr 16 17:29:56 2009 +0200
+++ b/src/HOL/Orderings.thy Fri Apr 17 08:36:18 2009 +0200
@@ -5,7 +5,7 @@
header {* Abstract orderings *}
theory Orderings
-imports Code_Setup
+imports HOL
uses "~~/src/Provers/order.ML"
begin
--- a/src/HOL/Product_Type.thy Thu Apr 16 17:29:56 2009 +0200
+++ b/src/HOL/Product_Type.thy Fri Apr 17 08:36:18 2009 +0200
@@ -84,6 +84,14 @@
lemma unit_abs_eta_conv [simp,noatp]: "(%u::unit. f ()) = f"
by (rule ext) simp
+instantiation unit :: default
+begin
+
+definition "default = ()"
+
+instance ..
+
+end
text {* code generator setup *}
--- a/src/HOL/Tools/Qelim/presburger.ML Thu Apr 16 17:29:56 2009 +0200
+++ b/src/HOL/Tools/Qelim/presburger.ML Fri Apr 17 08:36:18 2009 +0200
@@ -131,7 +131,7 @@
@{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"},
@{thm "mod_1"}, @{thm "Suc_plus1"}]
@ @{thms add_ac}
- addsimprocs [cancel_div_mod_proc]
+ addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
val splits_ss = comp_ss addsimps [@{thm "mod_div_equality'"}] addsplits
[@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"},
@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}]
--- a/src/HOL/Tools/int_factor_simprocs.ML Thu Apr 16 17:29:56 2009 +0200
+++ b/src/HOL/Tools/int_factor_simprocs.ML Fri Apr 17 08:36:18 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/int_factor_simprocs.ML
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 2000 University of Cambridge
@@ -46,13 +45,13 @@
@{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right}];
end
-(*Version for integer division*)
-structure IntDivCancelNumeralFactor = CancelNumeralFactorFun
+(*Version for semiring_div*)
+structure DivCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binop @{const_name Divides.div}
- val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT
- val cancel = @{thm zdiv_zmult_zmult1} RS trans
+ val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT
+ val cancel = @{thm div_mult_mult1} RS trans
val neg_exchanges = false
)
@@ -108,8 +107,9 @@
"(l::'a::{ordered_idom,number_ring}) <= m * n"],
K LeCancelNumeralFactor.proc),
("int_div_cancel_numeral_factors",
- ["((l::int) * m) div n", "(l::int) div (m * n)"],
- K IntDivCancelNumeralFactor.proc),
+ ["((l::'a::{semiring_div,number_ring}) * m) div n",
+ "(l::'a::{semiring_div,number_ring}) div (m * n)"],
+ K DivCancelNumeralFactor.proc),
("divide_cancel_numeral_factor",
["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
"(l::'a::{division_by_zero,field,number_ring}) / (m * n)",
@@ -284,24 +284,25 @@
@{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg}
);
-(*zdiv_zmult_zmult1_if is for integer division (div).*)
-structure IntDivCancelFactor = ExtractCommonTermFun
+(*for semirings with division*)
+structure DivCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binop @{const_name Divides.div}
- val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT
- val simp_conv = K (K (SOME @{thm zdiv_zmult_zmult1_if}))
+ val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT
+ val simp_conv = K (K (SOME @{thm div_mult_mult1_if}))
);
-structure IntModCancelFactor = ExtractCommonTermFun
+structure ModCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binop @{const_name Divides.mod}
val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} HOLogic.intT
- val simp_conv = K (K (SOME @{thm zmod_zmult_zmult1}))
+ val simp_conv = K (K (SOME @{thm mod_mult_mult1}))
);
-structure IntDvdCancelFactor = ExtractCommonTermFun
+(*for idoms*)
+structure DvdCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
@@ -321,8 +322,8 @@
val cancel_factors =
map Arith_Data.prep_simproc
[("ring_eq_cancel_factor",
- ["(l::'a::{idom}) * m = n",
- "(l::'a::{idom}) = m * n"],
+ ["(l::'a::idom) * m = n",
+ "(l::'a::idom) = m * n"],
K EqCancelFactor.proc),
("ordered_ring_le_cancel_factor",
["(l::'a::ordered_ring) * m <= n",
@@ -333,14 +334,14 @@
"(l::'a::ordered_ring) < m * n"],
K LessCancelFactor.proc),
("int_div_cancel_factor",
- ["((l::int) * m) div n", "(l::int) div (m * n)"],
- K IntDivCancelFactor.proc),
+ ["((l::'a::semiring_div) * m) div n", "(l::'a::semiring_div) div (m * n)"],
+ K DivCancelFactor.proc),
("int_mod_cancel_factor",
- ["((l::int) * m) mod n", "(l::int) mod (m * n)"],
- K IntModCancelFactor.proc),
+ ["((l::'a::semiring_div) * m) mod n", "(l::'a::semiring_div) mod (m * n)"],
+ K ModCancelFactor.proc),
("dvd_cancel_factor",
["((l::'a::idom) * m) dvd n", "(l::'a::idom) dvd (m * n)"],
- K IntDvdCancelFactor.proc),
+ K DvdCancelFactor.proc),
("divide_cancel_factor",
["((l::'a::{division_by_zero,field}) * m) / n",
"(l::'a::{division_by_zero,field}) / (m * n)"],
--- a/src/HOL/Word/BinGeneral.thy Thu Apr 16 17:29:56 2009 +0200
+++ b/src/HOL/Word/BinGeneral.thy Fri Apr 17 08:36:18 2009 +0200
@@ -439,7 +439,7 @@
apply clarsimp
apply (simp add: bin_last_mod bin_rest_div Bit_def
cong: number_of_False_cong)
- apply (clarsimp simp: zmod_zmult_zmult1 [symmetric]
+ apply (clarsimp simp: mod_mult_mult1 [symmetric]
zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]])
apply (rule trans [symmetric, OF _ emep1])
apply auto
--- a/src/HOL/Word/BinOperations.thy Thu Apr 16 17:29:56 2009 +0200
+++ b/src/HOL/Word/BinOperations.thy Fri Apr 17 08:36:18 2009 +0200
@@ -641,7 +641,7 @@
apply (simp add: bin_rest_div zdiv_zmult2_eq)
apply (case_tac b rule: bin_exhaust)
apply simp
- apply (simp add: Bit_def zmod_zmult_zmult1 p1mod22k
+ apply (simp add: Bit_def mod_mult_mult1 p1mod22k
split: bit.split
cong: number_of_False_cong)
done
--- a/src/HOL/Word/Num_Lemmas.thy Thu Apr 16 17:29:56 2009 +0200
+++ b/src/HOL/Word/Num_Lemmas.thy Fri Apr 17 08:36:18 2009 +0200
@@ -66,7 +66,7 @@
apply (safe dest!: even_equiv_def [THEN iffD1])
apply (subst pos_zmod_mult_2)
apply arith
- apply (simp add: zmod_zmult_zmult1)
+ apply (simp add: mod_mult_mult1)
done
lemmas eme1p = emep1 [simplified add_commute]
--- a/src/HOL/base.ML Thu Apr 16 17:29:56 2009 +0200
+++ b/src/HOL/base.ML Fri Apr 17 08:36:18 2009 +0200
@@ -1,2 +1,2 @@
(*side-entry for HOL-Base*)
-use_thy "Code_Setup";
+use_thy "HOL";
--- a/src/Provers/Arith/cancel_div_mod.ML Thu Apr 16 17:29:56 2009 +0200
+++ b/src/Provers/Arith/cancel_div_mod.ML Fri Apr 17 08:36:18 2009 +0200
@@ -69,7 +69,7 @@
fun cancel ss t pq =
let val teqt' = Data.prove_eq_sums ss (t, rearrange t pq)
- in hd(Data.div_mod_eqs RL [teqt' RS transitive_thm]) end;
+ in hd (Data.div_mod_eqs RL [teqt' RS transitive_thm]) end;
fun proc ss t =
let val (divs,mods) = coll_div_mod t ([],[])
--- a/src/Pure/Isar/code.ML Thu Apr 16 17:29:56 2009 +0200
+++ b/src/Pure/Isar/code.ML Fri Apr 17 08:36:18 2009 +0200
@@ -29,8 +29,6 @@
val add_undefined: string -> theory -> theory
val purge_data: theory -> theory
- val coregular_algebra: theory -> Sorts.algebra
- val operational_algebra: theory -> (sort -> sort) * Sorts.algebra
val these_eqns: theory -> string -> (thm * bool) list
val these_raw_eqns: theory -> string -> (thm * bool) list
val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
@@ -469,39 +467,6 @@
fun mk_default_eqn thy = Code_Unit.try_thm (check_linear o Code_Unit.mk_eqn thy);
-(** operational sort algebra and class discipline **)
-
-local
-
-fun arity_constraints thy algebra (class, tyco) =
- let
- val base_constraints = Sorts.mg_domain algebra tyco [class];
- val classparam_constraints = Sorts.complete_sort algebra [class]
- |> maps (map fst o these o try (#params o AxClass.get_info thy))
- |> map_filter (fn c => try (AxClass.param_of_inst thy) (c, tyco))
- |> maps (map fst o get_eqns thy)
- |> map (map (snd o dest_TVar) o Sign.const_typargs thy o Code_Unit.const_typ_eqn);
- val inter_sorts = map2 (curry (Sorts.inter_sort algebra));
- in fold inter_sorts classparam_constraints base_constraints end;
-
-fun retrieve_algebra thy operational =
- Sorts.subalgebra (Syntax.pp_global thy) operational
- (SOME o arity_constraints thy (Sign.classes_of thy))
- (Sign.classes_of thy);
-
-in
-
-fun coregular_algebra thy = retrieve_algebra thy (K true) |> snd;
-fun operational_algebra thy =
- let
- fun add_iff_operational class =
- can (AxClass.get_info thy) class ? cons class;
- val operational_classes = fold add_iff_operational (Sign.all_classes thy) []
- in retrieve_algebra thy (member (op =) operational_classes) end;
-
-end; (*local*)
-
-
(** interfaces and attributes **)
fun delete_force msg key xs =
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Code_Generator.thy Fri Apr 17 08:36:18 2009 +0200
@@ -0,0 +1,27 @@
+(* Title: Tools/Code_Generator.thy
+ Author: Florian Haftmann, TU Muenchen
+*)
+
+header {* Loading the code generator modules *}
+
+theory Code_Generator
+imports Pure
+uses
+ "~~/src/Tools/value.ML"
+ "~~/src/Tools/code/code_name.ML"
+ "~~/src/Tools/code/code_wellsorted.ML"
+ "~~/src/Tools/code/code_thingol.ML"
+ "~~/src/Tools/code/code_printer.ML"
+ "~~/src/Tools/code/code_target.ML"
+ "~~/src/Tools/code/code_ml.ML"
+ "~~/src/Tools/code/code_haskell.ML"
+ "~~/src/Tools/nbe.ML"
+begin
+
+setup {*
+ Code_ML.setup
+ #> Code_Haskell.setup
+ #> Nbe.setup
+*}
+
+end
\ No newline at end of file
--- a/src/Tools/code/code_funcgr.ML Thu Apr 16 17:29:56 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,335 +0,0 @@
-(* Title: Tools/code/code_funcgr.ML
- Author: Florian Haftmann, TU Muenchen
-
-Retrieving, normalizing and structuring code equations in graph
-with explicit dependencies.
-
-Legacy. To be replaced by Tools/code/code_wellsorted.ML
-*)
-
-signature CODE_WELLSORTED =
-sig
- type T
- val eqns: T -> string -> (thm * bool) list
- val typ: T -> string -> (string * sort) list * typ
- val all: T -> string list
- val pretty: theory -> T -> Pretty.T
- val make: theory -> string list
- -> ((sort -> sort) * Sorts.algebra) * T
- val eval_conv: theory
- -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> thm)) -> cterm -> thm
- val eval_term: theory
- -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> 'a)) -> term -> 'a
- val timing: bool ref
-end
-
-structure Code_Wellsorted : CODE_WELLSORTED =
-struct
-
-(** the graph type **)
-
-type T = (((string * sort) list * typ) * (thm * bool) list) Graph.T;
-
-fun eqns funcgr =
- these o Option.map snd o try (Graph.get_node funcgr);
-
-fun typ funcgr =
- fst o Graph.get_node funcgr;
-
-fun all funcgr = Graph.keys funcgr;
-
-fun pretty thy funcgr =
- AList.make (snd o Graph.get_node funcgr) (Graph.keys funcgr)
- |> (map o apfst) (Code_Unit.string_of_const thy)
- |> sort (string_ord o pairself fst)
- |> map (fn (s, thms) =>
- (Pretty.block o Pretty.fbreaks) (
- Pretty.str s
- :: map (Display.pretty_thm o fst) thms
- ))
- |> Pretty.chunks;
-
-
-(** generic combinators **)
-
-fun fold_consts f thms =
- thms
- |> maps (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of)
- |> (fold o fold_aterms) (fn Const c => f c | _ => I);
-
-fun consts_of (const, []) = []
- | consts_of (const, thms as _ :: _) =
- let
- fun the_const (c, _) = if c = const then I else insert (op =) c
- in fold_consts the_const (map fst thms) [] end;
-
-fun insts_of thy algebra tys sorts =
- let
- fun class_relation (x, _) _ = x;
- fun type_constructor tyco xs class =
- (tyco, class) :: (maps o maps) fst xs;
- fun type_variable (TVar (_, sort)) = map (pair []) sort
- | type_variable (TFree (_, sort)) = map (pair []) sort;
- fun of_sort_deriv ty sort =
- Sorts.of_sort_derivation (Syntax.pp_global thy) algebra
- { class_relation = class_relation, type_constructor = type_constructor,
- type_variable = type_variable }
- (ty, sort) handle Sorts.CLASS_ERROR _ => [] (*permissive!*)
- in (flat o flat) (map2 of_sort_deriv tys sorts) end;
-
-fun meets_of thy algebra =
- let
- fun meet_of ty sort tab =
- Sorts.meet_sort algebra (ty, sort) tab
- handle Sorts.CLASS_ERROR _ => tab (*permissive!*);
- in fold2 meet_of end;
-
-
-(** graph algorithm **)
-
-val timing = ref false;
-
-local
-
-fun resort_thms thy algebra typ_of thms =
- let
- val cs = fold_consts (insert (op =)) thms [];
- fun meets (c, ty) = case typ_of c
- of SOME (vs, _) =>
- meets_of thy algebra (Sign.const_typargs thy (c, ty)) (map snd vs)
- | NONE => I;
- val tab = fold meets cs Vartab.empty;
- in map (Code_Unit.inst_thm thy tab) thms end;
-
-fun resort_eqnss thy algebra funcgr =
- let
- val typ_funcgr = try (fst o Graph.get_node funcgr);
- val resort_dep = (apsnd o burrow_fst) (resort_thms thy algebra typ_funcgr);
- fun resort_rec typ_of (c, []) = (true, (c, []))
- | resort_rec typ_of (c, thms as (thm, _) :: _) = if is_some (AxClass.inst_of_param thy c)
- then (true, (c, thms))
- else let
- val (_, (vs, ty)) = Code_Unit.head_eqn thy thm;
- val thms' as (thm', _) :: _ = burrow_fst (resort_thms thy algebra typ_of) thms
- val (_, (vs', ty')) = Code_Unit.head_eqn thy thm'; (*FIXME simplify check*)
- in (Sign.typ_equiv thy (ty, ty'), (c, thms')) end;
- fun resort_recs eqnss =
- let
- fun typ_of c = case these (AList.lookup (op =) eqnss c)
- of (thm, _) :: _ => (SOME o snd o Code_Unit.head_eqn thy) thm
- | [] => NONE;
- val (unchangeds, eqnss') = split_list (map (resort_rec typ_of) eqnss);
- val unchanged = fold (fn x => fn y => x andalso y) unchangeds true;
- in (unchanged, eqnss') end;
- fun resort_rec_until eqnss =
- let
- val (unchanged, eqnss') = resort_recs eqnss;
- in if unchanged then eqnss' else resort_rec_until eqnss' end;
- in map resort_dep #> resort_rec_until end;
-
-fun instances_of thy algebra insts =
- let
- val thy_classes = (#classes o Sorts.rep_algebra o Sign.classes_of) thy;
- fun all_classparams tyco class =
- these (try (#params o AxClass.get_info thy) class)
- |> map_filter (fn (c, _) => try (AxClass.param_of_inst thy) (c, tyco))
- in
- Symtab.empty
- |> fold (fn (tyco, class) =>
- Symtab.map_default (tyco, []) (insert (op =) class)) insts
- |> (fn tab => Symtab.fold (fn (tyco, classes) => append (maps (all_classparams tyco)
- (Graph.all_succs thy_classes classes))) tab [])
- end;
-
-fun instances_of_consts thy algebra funcgr consts =
- let
- fun inst (cexpr as (c, ty)) = insts_of thy algebra
- (Sign.const_typargs thy (c, ty)) ((map snd o fst) (typ funcgr c));
- in
- []
- |> fold (fold (insert (op =)) o inst) consts
- |> instances_of thy algebra
- end;
-
-fun ensure_const' thy algebra funcgr const auxgr =
- if can (Graph.get_node funcgr) const
- then (NONE, auxgr)
- else if can (Graph.get_node auxgr) const
- then (SOME const, auxgr)
- else if is_some (Code.get_datatype_of_constr thy const) then
- auxgr
- |> Graph.new_node (const, [])
- |> pair (SOME const)
- else let
- val thms = Code.these_eqns thy const
- |> burrow_fst (Code_Unit.norm_args thy)
- |> burrow_fst (Code_Unit.norm_varnames thy Code_Name.purify_tvar Code_Name.purify_var);
- val rhs = consts_of (const, thms);
- in
- auxgr
- |> Graph.new_node (const, thms)
- |> fold_map (ensure_const thy algebra funcgr) rhs
- |-> (fn rhs' => fold (fn SOME const' => Graph.add_edge (const, const')
- | NONE => I) rhs')
- |> pair (SOME const)
- end
-and ensure_const thy algebra funcgr const =
- let
- val timeap = if !timing
- then Output.timeap_msg ("time for " ^ Code_Unit.string_of_const thy const)
- else I;
- in timeap (ensure_const' thy algebra funcgr const) end;
-
-fun merge_eqnss thy algebra raw_eqnss funcgr =
- let
- val eqnss = raw_eqnss
- |> resort_eqnss thy algebra funcgr
- |> filter_out (can (Graph.get_node funcgr) o fst);
- fun typ_eqn c [] = Code.default_typscheme thy c
- | typ_eqn c (thms as (thm, _) :: _) = (snd o Code_Unit.head_eqn thy) thm;
- fun add_eqns (const, thms) =
- Graph.new_node (const, (typ_eqn const thms, thms));
- fun add_deps (eqns as (const, thms)) funcgr =
- let
- val deps = consts_of eqns;
- val insts = instances_of_consts thy algebra funcgr
- (fold_consts (insert (op =)) (map fst thms) []);
- in
- funcgr
- |> ensure_consts thy algebra insts
- |> fold (curry Graph.add_edge const) deps
- |> fold (curry Graph.add_edge const) insts
- end;
- in
- funcgr
- |> fold add_eqns eqnss
- |> fold add_deps eqnss
- end
-and ensure_consts thy algebra cs funcgr =
- let
- val auxgr = Graph.empty
- |> fold (snd oo ensure_const thy algebra funcgr) cs;
- in
- funcgr
- |> fold (merge_eqnss thy algebra)
- (map (AList.make (Graph.get_node auxgr))
- (rev (Graph.strong_conn auxgr)))
- end;
-
-in
-
-(** retrieval interfaces **)
-
-val ensure_consts = ensure_consts;
-
-fun proto_eval thy cterm_of evaluator_lift evaluator proto_ct funcgr =
- let
- val ct = cterm_of proto_ct;
- val _ = Sign.no_vars (Syntax.pp_global thy) (Thm.term_of ct);
- val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) ();
- fun consts_of t =
- fold_aterms (fn Const c_ty => cons c_ty | _ => I) t [];
- val algebra = Code.coregular_algebra thy;
- val thm = Code.preprocess_conv thy ct;
- val ct' = Thm.rhs_of thm;
- val t' = Thm.term_of ct';
- val consts = map fst (consts_of t');
- val funcgr' = ensure_consts thy algebra consts funcgr;
- val (t'', evaluator_funcgr) = evaluator t';
- val consts' = consts_of t'';
- val dicts = instances_of_consts thy algebra funcgr' consts';
- val funcgr'' = ensure_consts thy algebra dicts funcgr';
- in (evaluator_lift (evaluator_funcgr (Code.operational_algebra thy)) thm funcgr'', funcgr'') end;
-
-fun proto_eval_conv thy =
- let
- fun evaluator_lift evaluator thm1 funcgr =
- let
- val thm2 = evaluator funcgr;
- val thm3 = Code.postprocess_conv thy (Thm.rhs_of thm2);
- in
- Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
- error ("could not construct evaluation proof:\n"
- ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3])
- end;
- in proto_eval thy I evaluator_lift end;
-
-fun proto_eval_term thy =
- let
- fun evaluator_lift evaluator _ funcgr = evaluator funcgr;
- in proto_eval thy (Thm.cterm_of thy) evaluator_lift end;
-
-end; (*local*)
-
-structure Funcgr = CodeDataFun
-(
- type T = T;
- val empty = Graph.empty;
- fun purge _ cs funcgr =
- Graph.del_nodes ((Graph.all_preds funcgr
- o filter (can (Graph.get_node funcgr))) cs) funcgr;
-);
-
-fun make thy =
- pair (Code.operational_algebra thy)
- o Funcgr.change thy o ensure_consts thy (Code.coregular_algebra thy);
-
-fun eval_conv thy f =
- fst o Funcgr.change_yield thy o proto_eval_conv thy f;
-
-fun eval_term thy f =
- fst o Funcgr.change_yield thy o proto_eval_term thy f;
-
-
-(** diagnostic commands **)
-
-fun code_depgr thy consts =
- let
- val (_, gr) = make thy consts;
- val select = Graph.all_succs gr consts;
- in
- gr
- |> not (null consts) ? Graph.subgraph (member (op =) select)
- |> Graph.map_nodes ((apsnd o map o apfst) (AxClass.overload thy))
- end;
-
-fun code_thms thy = Pretty.writeln o pretty thy o code_depgr thy;
-
-fun code_deps thy consts =
- let
- val gr = code_depgr thy consts;
- fun mk_entry (const, (_, (_, parents))) =
- let
- val name = Code_Unit.string_of_const thy const;
- val nameparents = map (Code_Unit.string_of_const thy) parents;
- in { name = name, ID = name, dir = "", unfold = true,
- path = "", parents = nameparents }
- end;
- val prgr = Graph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) gr [];
- in Present.display_graph prgr end;
-
-local
-
-structure P = OuterParse
-and K = OuterKeyword
-
-fun code_thms_cmd thy = code_thms thy o op @ o Code_Name.read_const_exprs thy;
-fun code_deps_cmd thy = code_deps thy o op @ o Code_Name.read_const_exprs thy;
-
-in
-
-val _ =
- OuterSyntax.improper_command "code_thms" "print system of code equations for code" OuterKeyword.diag
- (Scan.repeat P.term_group
- >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
- o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
-
-val _ =
- OuterSyntax.improper_command "code_deps" "visualize dependencies of code equations for code" OuterKeyword.diag
- (Scan.repeat P.term_group
- >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
- o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
-
-end;
-
-end; (*struct*)
--- a/src/Tools/code/code_ml.ML Thu Apr 16 17:29:56 2009 +0200
+++ b/src/Tools/code/code_ml.ML Fri Apr 17 08:36:18 2009 +0200
@@ -951,13 +951,13 @@
(* evaluation *)
-fun eval eval'' term_of reff thy ct args =
+fun eval_term reff thy t args =
let
val ctxt = ProofContext.init thy;
- val _ = if null (Term.add_frees (term_of ct) []) then () else error ("Term "
- ^ quote (Syntax.string_of_term_global thy (term_of ct))
+ val _ = if null (Term.add_frees t []) then () else error ("Term "
+ ^ quote (Syntax.string_of_term_global thy t)
^ " to be evaluated contains free variables");
- fun eval' naming program ((vs, ty), t) deps =
+ fun evaluator _ naming program ((_, ty), t) deps =
let
val _ = if Code_Thingol.contains_dictvar t then
error "Term to be evaluated contains free dictionaries" else ();
@@ -970,9 +970,7 @@
val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
^ space_implode " " (map (enclose "(" ")") args) ^ " end";
in ML_Context.evaluate ctxt false reff sml_code end;
- in eval'' thy (rpair eval') ct end;
-
-fun eval_term reff = eval Code_Thingol.eval_term I reff;
+ in Code_Thingol.eval_term thy I evaluator t end;
(* instrumentalization by antiquotation *)
--- a/src/Tools/code/code_thingol.ML Thu Apr 16 17:29:56 2009 +0200
+++ b/src/Tools/code/code_thingol.ML Fri Apr 17 08:36:18 2009 +0200
@@ -84,10 +84,10 @@
val consts_program: theory -> string list -> string list * (naming * program)
val cached_program: theory -> naming * program
val eval_conv: theory
- -> (term -> term * (naming -> program -> typscheme * iterm -> string list -> thm))
+ -> (term -> term) -> (term -> naming -> program -> typscheme * iterm -> string list -> thm)
-> cterm -> thm
val eval_term: theory
- -> (term -> term * (naming -> program -> typscheme * iterm -> string list -> 'a))
+ -> (term -> term) -> (term -> naming -> program -> typscheme * iterm -> string list -> 'a)
-> term -> 'a
end;
@@ -459,7 +459,45 @@
(* translation *)
-fun ensure_class thy (algbr as (_, algebra)) funcgr class =
+fun ensure_tyco thy algbr funcgr tyco =
+ let
+ val stmt_datatype =
+ let
+ val (vs, cos) = Code.get_datatype thy tyco;
+ in
+ fold_map (translate_tyvar_sort thy algbr funcgr) vs
+ ##>> fold_map (fn (c, tys) =>
+ ensure_const thy algbr funcgr c
+ ##>> fold_map (translate_typ thy algbr funcgr) tys) cos
+ #>> (fn info => Datatype (tyco, info))
+ end;
+ in ensure_stmt lookup_tyco (declare_tyco thy) stmt_datatype tyco end
+and ensure_const thy algbr funcgr c =
+ let
+ fun stmt_datatypecons tyco =
+ ensure_tyco thy algbr funcgr tyco
+ #>> (fn tyco => Datatypecons (c, tyco));
+ fun stmt_classparam class =
+ ensure_class thy algbr funcgr class
+ #>> (fn class => Classparam (c, class));
+ fun stmt_fun ((vs, ty), raw_thms) =
+ let
+ val thms = if null (Term.add_tfreesT ty []) orelse (null o fst o strip_type) ty
+ then raw_thms
+ else (map o apfst) (Code_Unit.expand_eta thy 1) raw_thms;
+ in
+ fold_map (translate_tyvar_sort thy algbr funcgr) vs
+ ##>> translate_typ thy algbr funcgr ty
+ ##>> fold_map (translate_eq thy algbr funcgr) thms
+ #>> (fn info => Fun (c, info))
+ end;
+ val stmt_const = case Code.get_datatype_of_constr thy c
+ of SOME tyco => stmt_datatypecons tyco
+ | NONE => (case AxClass.class_of_param thy c
+ of SOME class => stmt_classparam class
+ | NONE => stmt_fun (Code_Wellsorted.typ funcgr c, Code_Wellsorted.eqns funcgr c))
+ in ensure_stmt lookup_const (declare_const thy) stmt_const c end
+and ensure_class thy (algbr as (_, algebra)) funcgr class =
let
val superclasses = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
val cs = #params (AxClass.get_info thy class);
@@ -477,65 +515,6 @@
##>> ensure_class thy algbr funcgr superclass
#>> Classrel;
in ensure_stmt lookup_classrel (declare_classrel thy) stmt_classrel (subclass, superclass) end
-and ensure_tyco thy algbr funcgr tyco =
- let
- val stmt_datatype =
- let
- val (vs, cos) = Code.get_datatype thy tyco;
- in
- fold_map (translate_tyvar_sort thy algbr funcgr) vs
- ##>> fold_map (fn (c, tys) =>
- ensure_const thy algbr funcgr c
- ##>> fold_map (translate_typ thy algbr funcgr) tys) cos
- #>> (fn info => Datatype (tyco, info))
- end;
- in ensure_stmt lookup_tyco (declare_tyco thy) stmt_datatype tyco end
-and translate_tyvar_sort thy (algbr as (proj_sort, _)) funcgr (v, sort) =
- fold_map (ensure_class thy algbr funcgr) (proj_sort sort)
- #>> (fn sort => (unprefix "'" v, sort))
-and translate_typ thy algbr funcgr (TFree (v, _)) =
- pair (ITyVar (unprefix "'" v))
- | translate_typ thy algbr funcgr (Type (tyco, tys)) =
- ensure_tyco thy algbr funcgr tyco
- ##>> fold_map (translate_typ thy algbr funcgr) tys
- #>> (fn (tyco, tys) => tyco `%% tys)
-and translate_dicts thy (algbr as (proj_sort, algebra)) funcgr thm (ty, sort) =
- let
- val pp = Syntax.pp_global thy;
- datatype typarg =
- Global of (class * string) * typarg list list
- | Local of (class * class) list * (string * (int * sort));
- fun class_relation (Global ((_, tyco), yss), _) class =
- Global ((class, tyco), yss)
- | class_relation (Local (classrels, v), subclass) superclass =
- Local ((subclass, superclass) :: classrels, v);
- fun type_constructor tyco yss class =
- Global ((class, tyco), (map o map) fst yss);
- fun type_variable (TFree (v, sort)) =
- let
- val sort' = proj_sort sort;
- in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
- val typargs = Sorts.of_sort_derivation pp algebra
- {class_relation = class_relation, type_constructor = type_constructor,
- type_variable = type_variable} (ty, proj_sort sort)
- handle Sorts.CLASS_ERROR e => not_wellsorted thy thm ty sort e;
- fun mk_dict (Global (inst, yss)) =
- ensure_inst thy algbr funcgr inst
- ##>> (fold_map o fold_map) mk_dict yss
- #>> (fn (inst, dss) => DictConst (inst, dss))
- | mk_dict (Local (classrels, (v, (k, sort)))) =
- fold_map (ensure_classrel thy algbr funcgr) classrels
- #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort))))
- in fold_map mk_dict typargs end
-and translate_eq thy algbr funcgr (thm, linear) =
- let
- val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
- o Logic.unvarify o prop_of) thm;
- in
- fold_map (translate_term thy algbr funcgr (SOME thm)) args
- ##>> translate_term thy algbr funcgr (SOME thm) rhs
- #>> rpair (thm, linear)
- end
and ensure_inst thy (algbr as (_, algebra)) funcgr (class, tyco) =
let
val superclasses = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
@@ -572,31 +551,12 @@
#>> (fn ((((class, tyco), arity), superarities), classparams) =>
Classinst ((class, (tyco, arity)), (superarities, classparams)));
in ensure_stmt lookup_instance (declare_instance thy) stmt_inst (class, tyco) end
-and ensure_const thy algbr funcgr c =
- let
- fun stmt_datatypecons tyco =
+and translate_typ thy algbr funcgr (TFree (v, _)) =
+ pair (ITyVar (unprefix "'" v))
+ | translate_typ thy algbr funcgr (Type (tyco, tys)) =
ensure_tyco thy algbr funcgr tyco
- #>> (fn tyco => Datatypecons (c, tyco));
- fun stmt_classparam class =
- ensure_class thy algbr funcgr class
- #>> (fn class => Classparam (c, class));
- fun stmt_fun ((vs, ty), raw_thms) =
- let
- val thms = if null (Term.add_tfreesT ty []) orelse (null o fst o strip_type) ty
- then raw_thms
- else (map o apfst) (Code_Unit.expand_eta thy 1) raw_thms;
- in
- fold_map (translate_tyvar_sort thy algbr funcgr) vs
- ##>> translate_typ thy algbr funcgr ty
- ##>> fold_map (translate_eq thy algbr funcgr) thms
- #>> (fn info => Fun (c, info))
- end;
- val stmt_const = case Code.get_datatype_of_constr thy c
- of SOME tyco => stmt_datatypecons tyco
- | NONE => (case AxClass.class_of_param thy c
- of SOME class => stmt_classparam class
- | NONE => stmt_fun (Code_Wellsorted.typ funcgr c, Code_Wellsorted.eqns funcgr c))
- in ensure_stmt lookup_const (declare_const thy) stmt_const c end
+ ##>> fold_map (translate_typ thy algbr funcgr) tys
+ #>> (fn (tyco, tys) => tyco `%% tys)
and translate_term thy algbr funcgr thm (Const (c, ty)) =
translate_app thy algbr funcgr thm ((c, ty), [])
| translate_term thy algbr funcgr thm (Free (v, _)) =
@@ -617,6 +577,15 @@
translate_term thy algbr funcgr thm t'
##>> fold_map (translate_term thy algbr funcgr thm) ts
#>> (fn (t, ts) => t `$$ ts)
+and translate_eq thy algbr funcgr (thm, linear) =
+ let
+ val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
+ o Logic.unvarify o prop_of) thm;
+ in
+ fold_map (translate_term thy algbr funcgr (SOME thm)) args
+ ##>> translate_term thy algbr funcgr (SOME thm) rhs
+ #>> rpair (thm, linear)
+ end
and translate_const thy algbr funcgr thm (c, ty) =
let
val tys = Sign.const_typargs thy (c, ty);
@@ -695,7 +664,38 @@
and translate_app thy algbr funcgr thm (c_ty_ts as ((c, _), _)) =
case Code.get_case_scheme thy c
of SOME case_scheme => translate_app_case thy algbr funcgr thm case_scheme c_ty_ts
- | NONE => translate_app_const thy algbr funcgr thm c_ty_ts;
+ | NONE => translate_app_const thy algbr funcgr thm c_ty_ts
+and translate_tyvar_sort thy (algbr as (proj_sort, _)) funcgr (v, sort) =
+ fold_map (ensure_class thy algbr funcgr) (proj_sort sort)
+ #>> (fn sort => (unprefix "'" v, sort))
+and translate_dicts thy (algbr as (proj_sort, algebra)) funcgr thm (ty, sort) =
+ let
+ val pp = Syntax.pp_global thy;
+ datatype typarg =
+ Global of (class * string) * typarg list list
+ | Local of (class * class) list * (string * (int * sort));
+ fun class_relation (Global ((_, tyco), yss), _) class =
+ Global ((class, tyco), yss)
+ | class_relation (Local (classrels, v), subclass) superclass =
+ Local ((subclass, superclass) :: classrels, v);
+ fun type_constructor tyco yss class =
+ Global ((class, tyco), (map o map) fst yss);
+ fun type_variable (TFree (v, sort)) =
+ let
+ val sort' = proj_sort sort;
+ in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
+ val typargs = Sorts.of_sort_derivation pp algebra
+ {class_relation = class_relation, type_constructor = type_constructor,
+ type_variable = type_variable} (ty, proj_sort sort)
+ handle Sorts.CLASS_ERROR e => not_wellsorted thy thm ty sort e;
+ fun mk_dict (Global (inst, yss)) =
+ ensure_inst thy algbr funcgr inst
+ ##>> (fold_map o fold_map) mk_dict yss
+ #>> (fn (inst, dss) => DictConst (inst, dss))
+ | mk_dict (Local (classrels, (v, (k, sort)))) =
+ fold_map (ensure_classrel thy algbr funcgr) classrels
+ #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort))))
+ in fold_map mk_dict typargs end;
(* store *)
@@ -733,14 +733,14 @@
fun generate_consts thy algebra funcgr =
fold_map (ensure_const thy algebra funcgr);
in
- invoke_generation thy (Code_Wellsorted.make thy cs) generate_consts cs
+ invoke_generation thy (Code_Wellsorted.obtain thy cs []) generate_consts cs
|-> project_consts
end;
(* value evaluation *)
-fun ensure_value thy algbr funcgr t =
+fun ensure_value thy algbr funcgr t =
let
val ty = fastype_of t;
val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
@@ -766,18 +766,72 @@
#> term_value
end;
-fun eval thy evaluator t =
+fun eval thy evaluator raw_t algebra funcgr t =
+ let
+ val (((naming, program), (vs_ty_t, deps)), _) =
+ invoke_generation thy (algebra, funcgr) ensure_value t;
+ in evaluator raw_t naming program vs_ty_t deps end;
+
+fun eval_conv thy preproc = Code_Wellsorted.eval_conv thy preproc o eval thy;
+fun eval_term thy preproc = Code_Wellsorted.eval_term thy preproc o eval thy;
+
+
+(** diagnostic commands **)
+
+fun code_depgr thy consts =
+ let
+ val (_, eqngr) = Code_Wellsorted.obtain thy consts [];
+ val select = Graph.all_succs eqngr consts;
+ in
+ eqngr
+ |> not (null consts) ? Graph.subgraph (member (op =) select)
+ |> Graph.map_nodes ((apsnd o map o apfst) (AxClass.overload thy))
+ end;
+
+fun code_thms thy = Pretty.writeln o Code_Wellsorted.pretty thy o code_depgr thy;
+
+fun code_deps thy consts =
let
- val (t', evaluator'') = evaluator t;
- fun evaluator' algebra funcgr =
- let
- val (((naming, program), (vs_ty_t, deps)), _) =
- invoke_generation thy (algebra, funcgr) ensure_value t';
- in evaluator'' naming program vs_ty_t deps end;
- in (t', evaluator') end
+ val eqngr = code_depgr thy consts;
+ val constss = Graph.strong_conn eqngr;
+ val mapping = Symtab.empty |> fold (fn consts => fold (fn const =>
+ Symtab.update (const, consts)) consts) constss;
+ fun succs consts = consts
+ |> maps (Graph.imm_succs eqngr)
+ |> subtract (op =) consts
+ |> map (the o Symtab.lookup mapping)
+ |> distinct (op =);
+ val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss;
+ fun namify consts = map (Code_Unit.string_of_const thy) consts
+ |> commas;
+ val prgr = map (fn (consts, constss) =>
+ { name = namify consts, ID = namify consts, dir = "", unfold = true,
+ path = "", parents = map namify constss }) conn;
+ in Present.display_graph prgr end;
+
+local
-fun eval_conv thy = Code_Wellsorted.eval_conv thy o eval thy;
-fun eval_term thy = Code_Wellsorted.eval_term thy o eval thy;
+structure P = OuterParse
+and K = OuterKeyword
+
+fun code_thms_cmd thy = code_thms thy o op @ o Code_Name.read_const_exprs thy;
+fun code_deps_cmd thy = code_deps thy o op @ o Code_Name.read_const_exprs thy;
+
+in
+
+val _ =
+ OuterSyntax.improper_command "code_thms" "print system of code equations for code" OuterKeyword.diag
+ (Scan.repeat P.term_group
+ >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
+ o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
+
+val _ =
+ OuterSyntax.improper_command "code_deps" "visualize dependencies of code equations for code" OuterKeyword.diag
+ (Scan.repeat P.term_group
+ >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
+ o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
+
+end;
end; (*struct*)
--- a/src/Tools/code/code_wellsorted.ML Thu Apr 16 17:29:56 2009 +0200
+++ b/src/Tools/code/code_wellsorted.ML Fri Apr 17 08:36:18 2009 +0200
@@ -12,12 +12,13 @@
val typ: T -> string -> (string * sort) list * typ
val all: T -> string list
val pretty: theory -> T -> Pretty.T
- val make: theory -> string list
- -> ((sort -> sort) * Sorts.algebra) * T
+ val obtain: theory -> string list -> term list -> ((sort -> sort) * Sorts.algebra) * T
+ val preprocess: theory -> cterm list -> (cterm * (thm -> thm)) list
+ val preprocess_term: theory -> term list -> (term * (term -> term)) list
val eval_conv: theory
- -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> thm)) -> cterm -> thm
+ -> (term -> term) -> (term -> (sort -> sort) * Sorts.algebra -> T -> term -> thm) -> cterm -> thm
val eval_term: theory
- -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> 'a)) -> term -> 'a
+ -> (term -> term) -> (term -> (sort -> sort) * Sorts.algebra -> T -> term -> 'a) -> term -> 'a
end
structure Code_Wellsorted : CODE_WELLSORTED =
@@ -47,8 +48,10 @@
(* auxiliary *)
+fun is_proper_class thy = can (AxClass.get_info thy);
+
fun complete_proper_sort thy =
- Sign.complete_sort thy #> filter (can (AxClass.get_info thy));
+ Sign.complete_sort thy #> filter (is_proper_class thy);
fun inst_params thy tyco =
map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
@@ -232,8 +235,7 @@
((class, tyco), map (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k))
(0 upto Sign.arity_number thy tyco - 1));
-fun add_eqs thy (proj_sort, algebra) vardeps
- (c, (proto_lhs, proto_eqns)) (rhss, eqngr) =
+fun add_eqs thy vardeps (c, (proto_lhs, proto_eqns)) (rhss, eqngr) =
if can (Graph.get_node eqngr) c then (rhss, eqngr)
else let
val lhs = map_index (fn (k, (v, _)) =>
@@ -246,68 +248,26 @@
val eqngr' = Graph.new_node (c, (tyscm, eqns)) eqngr;
in (map (pair c) rhss' @ rhss, eqngr') end;
-fun extend_arities_eqngr thy cs cs_rhss (arities, eqngr) =
+fun extend_arities_eqngr thy cs ts (arities, eqngr) =
let
- val cs_rhss' = (map o apsnd o map) (styp_of NONE) cs_rhss;
+ val cs_rhss = (fold o fold_aterms) (fn Const (c_ty as (c, _)) =>
+ insert (op =) (c, (map (styp_of NONE) o Sign.const_typargs thy) c_ty) | _ => I) ts [];
val (vardeps, (eqntab, insts)) = empty_vardeps_data
|> fold (assert_fun thy arities eqngr) cs
- |> fold (assert_rhs thy arities eqngr) cs_rhss';
+ |> fold (assert_rhs thy arities eqngr) cs_rhss;
val arities' = fold (add_arity thy vardeps) insts arities;
val pp = Syntax.pp_global thy;
- val is_proper_class = can (AxClass.get_info thy);
- val (proj_sort, algebra) = Sorts.subalgebra pp is_proper_class
+ val algebra = Sorts.subalgebra pp (is_proper_class thy)
(AList.lookup (op =) arities') (Sign.classes_of thy);
- val (rhss, eqngr') = Symtab.fold
- (add_eqs thy (proj_sort, algebra) vardeps) eqntab ([], eqngr);
- fun deps_of (c, rhs) = c ::
- maps (dicts_of thy (proj_sort, algebra))
- (rhs ~~ (map snd o fst o fst o Graph.get_node eqngr') c);
+ val (rhss, eqngr') = Symtab.fold (add_eqs thy vardeps) eqntab ([], eqngr);
+ fun deps_of (c, rhs) = c :: maps (dicts_of thy algebra)
+ (rhs ~~ (map snd o fst o fst o Graph.get_node eqngr') c);
val eqngr'' = fold (fn (c, rhs) => fold
(curry Graph.add_edge c) (deps_of rhs)) rhss eqngr';
- in ((proj_sort, algebra), (arities', eqngr'')) end;
+ in (algebra, (arities', eqngr'')) end;
-(** retrieval interfaces **)
-
-fun proto_eval thy cterm_of evaluator_lift evaluator proto_ct arities_eqngr =
- let
- val ct = cterm_of proto_ct;
- val _ = Sign.no_vars (Syntax.pp_global thy) (Thm.term_of ct);
- val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) ();
- fun consts_of t =
- fold_aterms (fn Const c_ty => cons c_ty | _ => I) t [];
- val thm = Code.preprocess_conv thy ct;
- val ct' = Thm.rhs_of thm;
- val t' = Thm.term_of ct';
- val (t'', evaluator_eqngr) = evaluator t';
- val consts = map fst (consts_of t');
- val consts' = consts_of t'';
- val const_matches' = fold (fn (c, ty) =>
- insert (op =) (c, Sign.const_typargs thy (c, ty))) consts' [];
- val (algebra', arities_eqngr') =
- extend_arities_eqngr thy consts const_matches' arities_eqngr;
- in
- (evaluator_lift (evaluator_eqngr algebra') thm (snd arities_eqngr'),
- arities_eqngr')
- end;
-
-fun proto_eval_conv thy =
- let
- fun evaluator_lift evaluator thm1 eqngr =
- let
- val thm2 = evaluator eqngr;
- val thm3 = Code.postprocess_conv thy (Thm.rhs_of thm2);
- in
- Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
- error ("could not construct evaluation proof:\n"
- ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3])
- end;
- in proto_eval thy I evaluator_lift end;
-
-fun proto_eval_term thy =
- let
- fun evaluator_lift evaluator _ eqngr = evaluator eqngr;
- in proto_eval thy (Thm.cterm_of thy) evaluator_lift end;
+(** store **)
structure Wellsorted = CodeDataFun
(
@@ -327,71 +287,62 @@
in (arities', eqngr') end;
);
-fun make thy cs = apsnd snd
- (Wellsorted.change_yield thy (extend_arities_eqngr thy cs []));
-fun eval_conv thy f =
- fst o Wellsorted.change_yield thy o proto_eval_conv thy f;
+(** retrieval interfaces **)
-fun eval_term thy f =
- fst o Wellsorted.change_yield thy o proto_eval_term thy f;
-
-
-(** diagnostic commands **)
+fun obtain thy cs ts = apsnd snd
+ (Wellsorted.change_yield thy (extend_arities_eqngr thy cs ts));
-fun code_depgr thy consts =
+fun preprocess thy cts =
let
- val (_, eqngr) = make thy consts;
- val select = Graph.all_succs eqngr consts;
- in
- eqngr
- |> not (null consts) ? Graph.subgraph (member (op =) select)
- |> Graph.map_nodes ((apsnd o map o apfst) (AxClass.overload thy))
- end;
+ val ts = map Thm.term_of cts;
+ val _ = map
+ (Sign.no_vars (Syntax.pp_global thy) o Term.map_types Type.no_tvars) ts;
+ fun make thm1 = (Thm.rhs_of thm1, fn thm2 =>
+ let
+ val thm3 = Code.postprocess_conv thy (Thm.rhs_of thm2);
+ in
+ Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
+ error ("could not construct evaluation proof:\n"
+ ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3])
+ end);
+ in map (make o Code.preprocess_conv thy) cts end;
-fun code_thms thy = Pretty.writeln o pretty thy o code_depgr thy;
-
-fun code_deps thy consts =
+fun preprocess_term thy ts =
let
- val eqngr = code_depgr thy consts;
- val constss = Graph.strong_conn eqngr;
- val mapping = Symtab.empty |> fold (fn consts => fold (fn const =>
- Symtab.update (const, consts)) consts) constss;
- fun succs consts = consts
- |> maps (Graph.imm_succs eqngr)
- |> subtract (op =) consts
- |> map (the o Symtab.lookup mapping)
- |> distinct (op =);
- val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss;
- fun namify consts = map (Code_Unit.string_of_const thy) consts
- |> commas;
- val prgr = map (fn (consts, constss) =>
- { name = namify consts, ID = namify consts, dir = "", unfold = true,
- path = "", parents = map namify constss }) conn;
- in Present.display_graph prgr end;
+ val cts = map (Thm.cterm_of thy) ts;
+ val postprocess = Code.postprocess_term thy;
+ in map (fn (ct, _) => (Thm.term_of ct, postprocess)) (preprocess thy cts) end;
-local
+(*FIXME rearrange here*)
-structure P = OuterParse
-and K = OuterKeyword
-
-fun code_thms_cmd thy = code_thms thy o op @ o Code_Name.read_const_exprs thy;
-fun code_deps_cmd thy = code_deps thy o op @ o Code_Name.read_const_exprs thy;
-
-in
+fun proto_eval thy cterm_of evaluator_lift preproc evaluator proto_ct =
+ let
+ val ct = cterm_of proto_ct;
+ val _ = Sign.no_vars (Syntax.pp_global thy) (Thm.term_of ct);
+ val _ = Term.map_types Type.no_tvars (Thm.term_of ct);
+ fun consts_of t =
+ fold_aterms (fn Const c_ty => cons c_ty | _ => I) t [];
+ val thm = Code.preprocess_conv thy ct;
+ val ct' = Thm.rhs_of thm;
+ val t' = Thm.term_of ct';
+ val consts = map fst (consts_of t');
+ val t'' = preproc t';
+ val (algebra', eqngr') = obtain thy consts [t''];
+ in evaluator_lift (evaluator t' algebra' eqngr' t'') thm end;
-val _ =
- OuterSyntax.improper_command "code_thms" "print system of code equations for code" OuterKeyword.diag
- (Scan.repeat P.term_group
- >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
- o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
+fun eval_conv thy =
+ let
+ fun evaluator_lift thm2 thm1 =
+ let
+ val thm3 = Code.postprocess_conv thy (Thm.rhs_of thm2);
+ in
+ Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
+ error ("could not construct evaluation proof:\n"
+ ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3])
+ end;
+ in proto_eval thy I evaluator_lift end;
-val _ =
- OuterSyntax.improper_command "code_deps" "visualize dependencies of code equations for code" OuterKeyword.diag
- (Scan.repeat P.term_group
- >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
- o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
-
-end;
+fun eval_term thy = proto_eval thy (Thm.cterm_of thy) (fn t => K t);
end; (*struct*)
--- a/src/Tools/nbe.ML Thu Apr 16 17:29:56 2009 +0200
+++ b/src/Tools/nbe.ML Fri Apr 17 08:36:18 2009 +0200
@@ -431,7 +431,7 @@
(* evaluation with type reconstruction *)
-fun eval thy t naming program vs_ty_t deps =
+fun norm thy t naming program vs_ty_t deps =
let
fun subst_const f = map_aterms (fn t as Term.Const (c, ty) => Term.Const (f c, ty)
| t => t);
@@ -463,10 +463,6 @@
(* evaluation oracle *)
-val (_, norm_oracle) = Context.>>> (Context.map_theory_result
- (Thm.add_oracle (Binding.name "norm", fn (thy, t, naming, program, vs_ty_t, deps) =>
- Thm.cterm_of thy (Logic.mk_equals (t, eval thy t naming program vs_ty_t deps)))));
-
fun add_triv_classes thy =
let
val inters = curry (Sorts.inter_sort (Sign.classes_of thy))
@@ -476,19 +472,20 @@
| TFree (v, sort) => TFree (v, f sort));
in map_sorts inters end;
+val (_, raw_norm_oracle) = Context.>>> (Context.map_theory_result
+ (Thm.add_oracle (Binding.name "norm", fn (thy, t, naming, program, vs_ty_t, deps) =>
+ Thm.cterm_of thy (Logic.mk_equals (t, norm thy t naming program vs_ty_t deps)))));
+
+fun norm_oracle thy t naming program vs_ty_t deps =
+ raw_norm_oracle (thy, t, naming, program, vs_ty_t, deps);
+
fun norm_conv ct =
let
val thy = Thm.theory_of_cterm ct;
- fun evaluator' t naming program vs_ty_t deps =
- norm_oracle (thy, t, naming, program, vs_ty_t, deps);
- fun evaluator t = (add_triv_classes thy t, evaluator' t);
- in Code_Thingol.eval_conv thy evaluator ct end;
+ in Code_Thingol.eval_conv thy (add_triv_classes thy) (norm_oracle thy) ct end;
-fun norm_term thy t =
- let
- fun evaluator' t naming program vs_ty_t deps = eval thy t naming program vs_ty_t deps;
- fun evaluator t = (add_triv_classes thy t, evaluator' t);
- in (Code.postprocess_term thy o Code_Thingol.eval_term thy evaluator) t end;
+fun norm_term thy = Code.postprocess_term thy
+ o Code_Thingol.eval_term thy (add_triv_classes thy) (norm thy);
(* evaluation command *)