--- a/doc-src/IsarImplementation/Thy/Integration.thy Thu Oct 29 16:21:43 2009 +0000
+++ b/doc-src/IsarImplementation/Thy/Integration.thy Thu Oct 29 16:22:14 2009 +0000
@@ -274,7 +274,8 @@
@{index_ML Isar.state: "unit -> Toplevel.state"} \\
@{index_ML Isar.exn: "unit -> (exn * string) option"} \\
@{index_ML Isar.context: "unit -> Proof.context"} \\
- @{index_ML Isar.goal: "unit -> thm"} \\
+ @{index_ML Isar.goal: "unit ->
+ {context: Proof.context, facts: thm list, goal: thm}"} \\
\end{mldecls}
\begin{description}
@@ -293,8 +294,9 @@
"Isar.state ()"}, analogous to @{ML Context.proof_of}
(\secref{sec:generic-context}).
- \item @{ML "Isar.goal ()"} picks the tactical goal from @{ML
- "Isar.state ()"}, represented as a theorem according to
+ \item @{ML "Isar.goal ()"} produces the full Isar goal state,
+ consisting of proof context, facts that have been indicated for
+ immediate use, and the tactical goal according to
\secref{sec:tactical-goals}.
\end{description}
--- a/doc-src/IsarImplementation/Thy/document/Integration.tex Thu Oct 29 16:21:43 2009 +0000
+++ b/doc-src/IsarImplementation/Thy/document/Integration.tex Thu Oct 29 16:22:14 2009 +0000
@@ -335,7 +335,8 @@
\indexdef{}{ML}{Isar.state}\verb|Isar.state: unit -> Toplevel.state| \\
\indexdef{}{ML}{Isar.exn}\verb|Isar.exn: unit -> (exn * string) option| \\
\indexdef{}{ML}{Isar.context}\verb|Isar.context: unit -> Proof.context| \\
- \indexdef{}{ML}{Isar.goal}\verb|Isar.goal: unit -> thm| \\
+ \indexdef{}{ML}{Isar.goal}\verb|Isar.goal: unit ->|\isasep\isanewline%
+\verb| {context: Proof.context, facts: thm list, goal: thm}| \\
\end{mldecls}
\begin{description}
@@ -353,7 +354,9 @@
\item \verb|Isar.context ()| produces the proof context from \verb|Isar.state ()|, analogous to \verb|Context.proof_of|
(\secref{sec:generic-context}).
- \item \verb|Isar.goal ()| picks the tactical goal from \verb|Isar.state ()|, represented as a theorem according to
+ \item \verb|Isar.goal ()| produces the full Isar goal state,
+ consisting of proof context, facts that have been indicated for
+ immediate use, and the tactical goal according to
\secref{sec:tactical-goals}.
\end{description}%
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Thu Oct 29 16:21:43 2009 +0000
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Thu Oct 29 16:22:14 2009 +0000
@@ -132,18 +132,19 @@
This \verb!no_vars! business can become a bit tedious.
If you would rather never see question marks, simply put
\begin{verbatim}
-reset show_question_marks;
+show_question_marks := false;
\end{verbatim}
at the beginning of your file \texttt{ROOT.ML}.
-The rest of this document is produced with this flag reset.
+The rest of this document is produced with this flag set to \texttt{false}.
-Hint: Resetting \verb!show_question_marks! only suppresses question
-marks; variables that end in digits, e.g. @{text"x1"}, are still
-printed with a trailing @{text".0"}, e.g. @{text"x1.0"}, their
-internal index. This can be avoided by turning the last digit into a
-subscript: write \verb!x\<^isub>1! and obtain the much nicer @{text"x\<^isub>1"}. *}
+Hint: Setting \verb!show_question_marks! to \texttt{false} only
+suppresses question marks; variables that end in digits,
+e.g. @{text"x1"}, are still printed with a trailing @{text".0"},
+e.g. @{text"x1.0"}, their internal index. This can be avoided by
+turning the last digit into a subscript: write \verb!x\<^isub>1! and
+obtain the much nicer @{text"x\<^isub>1"}. *}
-(*<*)ML"Unsynchronized.reset show_question_marks"(*>*)
+(*<*)ML"show_question_marks := false"(*>*)
subsection {*Qualified names*}
@@ -415,7 +416,7 @@
\begin{quote}
\verb!\begin{center}!\\
\verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
- \verb!@!\verb!{thm (lhs) foldl_Nil} & @!\verb!{thm (rhs) foldl_Nil}!\\
+ \verb!@!\verb!{thm (lhs) foldl_Nil} & @!\verb!{thm (rhs) foldl_Nil}\\!\\
\verb!@!\verb!{thm (lhs) foldl_Cons} & @!\verb!{thm (rhs) foldl_Cons}!\\
\verb!\end{tabular}!\\
\verb!\end{center}!
@@ -430,16 +431,16 @@
Likewise, \verb!concl! may be used as a style to show just the
conclusion of a proposition. For example, take \verb!hd_Cons_tl!:
\begin{center}
- @{thm [show_types] hd_Cons_tl}
+ @{thm hd_Cons_tl}
\end{center}
To print just the conclusion,
\begin{center}
- @{thm [show_types] (concl) hd_Cons_tl}
+ @{thm (concl) hd_Cons_tl}
\end{center}
type
\begin{quote}
\verb!\begin{center}!\\
- \verb!@!\verb!{thm [show_types] (concl) hd_Cons_tl}!\\
+ \verb!@!\verb!{thm (concl) hd_Cons_tl}!\\
\verb!\end{center}!
\end{quote}
Beware that any options must be placed \emph{before}
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Thu Oct 29 16:21:43 2009 +0000
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Thu Oct 29 16:22:14 2009 +0000
@@ -173,16 +173,17 @@
This \verb!no_vars! business can become a bit tedious.
If you would rather never see question marks, simply put
\begin{verbatim}
-reset show_question_marks;
+show_question_marks := false;
\end{verbatim}
at the beginning of your file \texttt{ROOT.ML}.
-The rest of this document is produced with this flag reset.
+The rest of this document is produced with this flag set to \texttt{false}.
-Hint: Resetting \verb!show_question_marks! only suppresses question
-marks; variables that end in digits, e.g. \isa{x{\isadigit{1}}}, are still
-printed with a trailing \isa{{\isachardot}{\isadigit{0}}}, e.g. \isa{x{\isadigit{1}}{\isachardot}{\isadigit{0}}}, their
-internal index. This can be avoided by turning the last digit into a
-subscript: write \verb!x\<^isub>1! and obtain the much nicer \isa{x\isactrlisub {\isadigit{1}}}.%
+Hint: Setting \verb!show_question_marks! to \texttt{false} only
+suppresses question marks; variables that end in digits,
+e.g. \isa{x{\isadigit{1}}}, are still printed with a trailing \isa{{\isachardot}{\isadigit{0}}},
+e.g. \isa{x{\isadigit{1}}{\isachardot}{\isadigit{0}}}, their internal index. This can be avoided by
+turning the last digit into a subscript: write \verb!x\<^isub>1! and
+obtain the much nicer \isa{x\isactrlisub {\isadigit{1}}}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -537,7 +538,7 @@
\begin{quote}
\verb!\begin{center}!\\
\verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
- \verb!@!\verb!{thm (lhs) foldl_Nil} & @!\verb!{thm (rhs) foldl_Nil}!\\
+ \verb!@!\verb!{thm (lhs) foldl_Nil} & @!\verb!{thm (rhs) foldl_Nil}\\!\\
\verb!@!\verb!{thm (lhs) foldl_Cons} & @!\verb!{thm (rhs) foldl_Cons}!\\
\verb!\end{tabular}!\\
\verb!\end{center}!
@@ -552,16 +553,16 @@
Likewise, \verb!concl! may be used as a style to show just the
conclusion of a proposition. For example, take \verb!hd_Cons_tl!:
\begin{center}
- \isa{{\isacharparenleft}xs\ {\isasymColon}\ {\isacharprime}a\ list{\isacharparenright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}
+ \isa{xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}
\end{center}
To print just the conclusion,
\begin{center}
- \isa{hd\ {\isacharparenleft}xs\ {\isasymColon}\ {\isacharprime}a\ list{\isacharparenright}{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}
+ \isa{hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}
\end{center}
type
\begin{quote}
\verb!\begin{center}!\\
- \verb!@!\verb!{thm [show_types] (concl) hd_Cons_tl}!\\
+ \verb!@!\verb!{thm (concl) hd_Cons_tl}!\\
\verb!\end{center}!
\end{quote}
Beware that any options must be placed \emph{before}
--- a/doc-src/LaTeXsugar/Sugar/document/root.tex Thu Oct 29 16:21:43 2009 +0000
+++ b/doc-src/LaTeXsugar/Sugar/document/root.tex Thu Oct 29 16:22:14 2009 +0000
@@ -33,7 +33,7 @@
\hyphenation{Isa-belle}
\begin{document}
-\title{\LaTeX\ Sugar for Isabelle documents}
+\title{\LaTeX\ Sugar for Isabelle Documents}
\author{Florian Haftmann, Gerwin Klein, Tobias Nipkow, Norbert Schirmer}
\maketitle
--- a/etc/symbols Thu Oct 29 16:21:43 2009 +0000
+++ b/etc/symbols Thu Oct 29 16:22:14 2009 +0000
@@ -244,10 +244,10 @@
\<Inter> code: 0x0022c2 font: Isabelle abbrev: Inter
\<union> code: 0x00222a font: Isabelle abbrev: Un
\<Union> code: 0x0022c3 font: Isabelle abbrev: Union
-\<squnion> code: 0x002294 font: Isabelle abbrev: |_|
-\<Squnion> code: 0x002a06 font: Isabelle abbrev: |||
-\<sqinter> code: 0x002293 font: Isabelle abbrev: &&
-\<Sqinter> code: 0x002a05 font: Isabelle abbrev: &&&
+\<squnion> code: 0x002294 font: Isabelle
+\<Squnion> code: 0x002a06 font: Isabelle
+\<sqinter> code: 0x002293 font: Isabelle
+\<Sqinter> code: 0x002a05 font: Isabelle
\<setminus> code: 0x002216 font: Isabelle
\<propto> code: 0x00221d font: Isabelle
\<uplus> code: 0x00228e font: Isabelle
--- a/lib/scripts/getsettings Thu Oct 29 16:21:43 2009 +0000
+++ b/lib/scripts/getsettings Thu Oct 29 16:22:14 2009 +0000
@@ -86,7 +86,7 @@
local COMPONENT="$1"
if [ ! -d "$COMPONENT" ]; then
- echo >&2 "Bad Isabelle component: $COMPONENT"
+ echo >&2 "Bad Isabelle component: \"$COMPONENT\""
exit 2
elif [ -z "$ISABELLE_COMPONENTS" ]; then
ISABELLE_COMPONENTS="$COMPONENT"
--- a/src/HOL/Code_Numeral.thy Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Code_Numeral.thy Thu Oct 29 16:22:14 2009 +0000
@@ -3,7 +3,7 @@
header {* Type of target language numerals *}
theory Code_Numeral
-imports Nat_Numeral
+imports Nat_Numeral Nat_Transfer Divides
begin
text {*
--- a/src/HOL/Divides.thy Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Divides.thy Thu Oct 29 16:22:14 2009 +0000
@@ -6,8 +6,16 @@
header {* The division operators div and mod *}
theory Divides
-imports Nat Power Product_Type
-uses "~~/src/Provers/Arith/cancel_div_mod.ML"
+imports Nat_Numeral Nat_Transfer
+uses
+ "~~/src/Provers/Arith/assoc_fold.ML"
+ "~~/src/Provers/Arith/cancel_numerals.ML"
+ "~~/src/Provers/Arith/combine_numerals.ML"
+ "~~/src/Provers/Arith/cancel_numeral_factor.ML"
+ "~~/src/Provers/Arith/extract_common_term.ML"
+ ("Tools/numeral_simprocs.ML")
+ ("Tools/nat_numeral_simprocs.ML")
+ "~~/src/Provers/Arith/cancel_div_mod.ML"
begin
subsection {* Syntactic division operations *}
@@ -178,6 +186,9 @@
lemma dvd_div_mult_self: "a dvd b \<Longrightarrow> (b div a) * a = b"
by (subst (2) mod_div_equality [of b a, symmetric]) (simp add:dvd_imp_mod_0)
+lemma dvd_mult_div_cancel: "a dvd b \<Longrightarrow> a * (b div a) = b"
+by (drule dvd_div_mult_self) (simp add: mult_commute)
+
lemma dvd_div_mult: "a dvd b \<Longrightarrow> (b div a) * c = b * c div a"
apply (cases "a = 0")
apply simp
@@ -866,79 +877,6 @@
apply (auto simp add: Suc_diff_le le_mod_geq)
done
-
-subsubsection {* The Divides Relation *}
-
-lemma dvd_1_left [iff]: "Suc 0 dvd k"
- unfolding dvd_def by simp
-
-lemma dvd_1_iff_1 [simp]: "(m dvd Suc 0) = (m = Suc 0)"
-by (simp add: dvd_def)
-
-lemma nat_dvd_1_iff_1 [simp]: "m dvd (1::nat) \<longleftrightarrow> m = 1"
-by (simp add: dvd_def)
-
-lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
- unfolding dvd_def
- by (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff)
-
-text {* @{term "op dvd"} is a partial order *}
-
-interpretation dvd: order "op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"
- proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym)
-
-lemma dvd_diff_nat[simp]: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
-unfolding dvd_def
-by (blast intro: diff_mult_distrib2 [symmetric])
-
-lemma dvd_diffD: "[| k dvd m-n; k dvd n; n\<le>m |] ==> k dvd (m::nat)"
- apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
- apply (blast intro: dvd_add)
- done
-
-lemma dvd_diffD1: "[| k dvd m-n; k dvd m; n\<le>m |] ==> k dvd (n::nat)"
-by (drule_tac m = m in dvd_diff_nat, auto)
-
-lemma dvd_reduce: "(k dvd n + k) = (k dvd (n::nat))"
- apply (rule iffI)
- apply (erule_tac [2] dvd_add)
- apply (rule_tac [2] dvd_refl)
- apply (subgoal_tac "n = (n+k) -k")
- prefer 2 apply simp
- apply (erule ssubst)
- apply (erule dvd_diff_nat)
- apply (rule dvd_refl)
- done
-
-lemma dvd_mult_cancel: "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n"
- unfolding dvd_def
- apply (erule exE)
- apply (simp add: mult_ac)
- done
-
-lemma dvd_mult_cancel1: "0<m ==> (m*n dvd m) = (n = (1::nat))"
- apply auto
- apply (subgoal_tac "m*n dvd m*1")
- apply (drule dvd_mult_cancel, auto)
- done
-
-lemma dvd_mult_cancel2: "0<m ==> (n*m dvd m) = (n = (1::nat))"
- apply (subst mult_commute)
- apply (erule dvd_mult_cancel1)
- 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 dvd_mult_div_cancel: "n dvd m ==> n * (m div n) = (m::nat)"
- by (simp add: dvd_eq_mod_eq_0 mult_div_cancel)
-
-lemma power_dvd_imp_le:
- "i ^ m dvd i ^ n \<Longrightarrow> (1::nat) < i \<Longrightarrow> m \<le> n"
- apply (rule power_le_imp_le_exp, assumption)
- apply (erule dvd_imp_le, simp)
- done
-
lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
@@ -1162,9 +1100,158 @@
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)
+lemma div2_Suc_Suc [simp]: "Suc (Suc m) div 2 = Suc (m div 2)"
+by (auto simp add: numeral_2_eq_2 le_div_geq)
+
+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]: "0 < (m\<Colon>nat) mod 2 \<longleftrightarrow> m mod 2 = 1"
+proof -
+ { fix n :: nat have "(n::nat) < 2 \<Longrightarrow> n = 0 \<or> n = 1" by (induct n) simp_all }
+ moreover have "m mod 2 < 2" by simp
+ ultimately have "m mod 2 = 0 \<or> m mod 2 = 1" .
+ then show ?thesis by auto
+qed
+
+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]
+
+
+subsection {* Proof Tools setup; Combination and Cancellation Simprocs *}
+
+declare split_div[of _ _ "number_of k", standard, arith_split]
+declare split_mod[of _ _ "number_of k", standard, arith_split]
+
+
+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)
+
+
+use "Tools/numeral_simprocs.ML"
+
+use "Tools/nat_numeral_simprocs.ML"
+
+declaration {*
+ K (Lin_Arith.add_simps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}])
+ #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1},
+ @{thm nat_0}, @{thm nat_1},
+ @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of},
+ @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less},
+ @{thm le_Suc_number_of}, @{thm le_number_of_Suc},
+ @{thm less_Suc_number_of}, @{thm less_number_of_Suc},
+ @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc},
+ @{thm mult_Suc}, @{thm mult_Suc_right},
+ @{thm add_Suc}, @{thm add_Suc_right},
+ @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},
+ @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of},
+ @{thm if_True}, @{thm if_False}])
+ #> Lin_Arith.add_simprocs (Numeral_Simprocs.assoc_fold_simproc
+ :: Numeral_Simprocs.combine_numerals
+ :: Numeral_Simprocs.cancel_numerals)
+ #> Lin_Arith.add_simprocs (Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals))
+*}
end
--- a/src/HOL/Fact.thy Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Fact.thy Thu Oct 29 16:22:14 2009 +0000
@@ -8,7 +8,7 @@
header{*Factorial Function*}
theory Fact
-imports Nat_Transfer
+imports Main
begin
class fact =
@@ -266,9 +266,6 @@
lemma of_nat_fact_not_zero [simp]: "of_nat (fact n) \<noteq> (0::'a::semiring_char_0)"
by auto
-class ordered_semiring_1 = ordered_semiring + semiring_1
-class ordered_semiring_1_strict = ordered_semiring_strict + semiring_1
-
lemma of_nat_fact_gt_zero [simp]: "(0::'a::{ordered_semidom}) < of_nat(fact n)" by auto
lemma of_nat_fact_ge_zero [simp]: "(0::'a::ordered_semidom) \<le> of_nat(fact n)"
--- a/src/HOL/Fun.thy Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Fun.thy Thu Oct 29 16:22:14 2009 +0000
@@ -7,7 +7,6 @@
theory Fun
imports Complete_Lattice
-uses ("Tools/transfer.ML")
begin
text{*As a simplification rule, it replaces all function equalities by
@@ -604,16 +603,6 @@
*}
-subsection {* Generic transfer procedure *}
-
-definition TransferMorphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
- where "TransferMorphism a B \<longleftrightarrow> True"
-
-use "Tools/transfer.ML"
-
-setup Transfer.setup
-
-
subsection {* Code generator setup *}
types_code
--- a/src/HOL/GCD.thy Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/GCD.thy Thu Oct 29 16:22:14 2009 +0000
@@ -28,7 +28,7 @@
header {* GCD *}
theory GCD
-imports Fact
+imports Fact Parity
begin
declare One_nat_def [simp del]
--- a/src/HOL/Groebner_Basis.thy Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Groebner_Basis.thy Thu Oct 29 16:22:14 2009 +0000
@@ -5,7 +5,7 @@
header {* Semiring normalization and Groebner Bases *}
theory Groebner_Basis
-imports Nat_Numeral
+imports IntDiv
uses
"Tools/Groebner_Basis/misc.ML"
"Tools/Groebner_Basis/normalizer_data.ML"
--- a/src/HOL/Int.thy Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Int.thy Thu Oct 29 16:22:14 2009 +0000
@@ -13,12 +13,6 @@
("Tools/numeral.ML")
("Tools/numeral_syntax.ML")
("Tools/int_arith.ML")
- "~~/src/Provers/Arith/assoc_fold.ML"
- "~~/src/Provers/Arith/cancel_numerals.ML"
- "~~/src/Provers/Arith/combine_numerals.ML"
- "~~/src/Provers/Arith/cancel_numeral_factor.ML"
- "~~/src/Provers/Arith/extract_common_term.ML"
- ("Tools/numeral_simprocs.ML")
begin
subsection {* The equivalence relation underlying the integers *}
@@ -1093,7 +1087,7 @@
lemmas double_eq_0_iff = double_zero
lemma odd_nonzero:
- "1 + z + z \<noteq> (0::int)";
+ "1 + z + z \<noteq> (0::int)"
proof (cases z rule: int_cases)
case (nonneg n)
have le: "0 \<le> z+z" by (simp add: nonneg add_increasing)
@@ -1163,7 +1157,7 @@
qed
lemma odd_less_0:
- "(1 + z + z < 0) = (z < (0::int))";
+ "(1 + z + z < 0) = (z < (0::int))"
proof (cases z rule: int_cases)
case (nonneg n)
thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
@@ -1368,7 +1362,7 @@
lemma Ints_odd_less_0:
assumes in_Ints: "a \<in> Ints"
- shows "(1 + a + a < 0) = (a < (0::'a::ordered_idom))";
+ shows "(1 + a + a < 0) = (a < (0::'a::ordered_idom))"
proof -
from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
then obtain z where a: "a = of_int z" ..
@@ -1503,8 +1497,6 @@
of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult
of_int_0 of_int_1 of_int_add of_int_mult
-use "Tools/numeral_simprocs.ML"
-
use "Tools/int_arith.ML"
setup {* Int_Arith.global_setup *}
declaration {* K Int_Arith.setup *}
@@ -1540,11 +1532,7 @@
text{*Lemmas for specialist use, NOT as default simprules*}
lemma mult_2: "2 * z = (z+z::'a::number_ring)"
-proof -
- have "2*z = (1 + 1)*z" by simp
- also have "... = z+z" by (simp add: left_distrib)
- finally show ?thesis .
-qed
+unfolding one_add_one_is_two [symmetric] left_distrib by simp
lemma mult_2_right: "z * 2 = (z+z::'a::number_ring)"
by (subst mult_commute, rule mult_2)
@@ -1830,14 +1818,15 @@
apply (frule pos_zmult_eq_1_iff_lemma, auto)
done
-(* Could be simplified but Presburger only becomes available too late *)
-lemma infinite_UNIV_int: "~finite(UNIV::int set)"
+lemma infinite_UNIV_int: "\<not> finite (UNIV::int set)"
proof
- assume "finite(UNIV::int set)"
- moreover have "~(EX i::int. 2*i = 1)"
- by (auto simp: pos_zmult_eq_1_iff)
- ultimately show False using finite_UNIV_inj_surj[of "%n::int. n+n"]
- by (simp add:inj_on_def surj_def) (blast intro:sym)
+ assume "finite (UNIV::int set)"
+ moreover have "inj (\<lambda>i\<Colon>int. 2 * i)"
+ by (rule injI) simp
+ ultimately have "surj (\<lambda>i\<Colon>int. 2 * i)"
+ by (rule finite_UNIV_inj_surj)
+ then obtain i :: int where "1 = 2 * i" by (rule surjE)
+ then show False by (simp add: pos_zmult_eq_1_iff)
qed
@@ -1995,6 +1984,135 @@
lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2, standard]
+subsection {* The divides relation *}
+
+lemma zdvd_anti_sym:
+ "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
+ apply (simp add: dvd_def, auto)
+ apply (simp add: mult_assoc zero_less_mult_iff zmult_eq_1_iff)
+ done
+
+lemma zdvd_dvd_eq: assumes "a \<noteq> 0" and "(a::int) dvd b" and "b dvd a"
+ shows "\<bar>a\<bar> = \<bar>b\<bar>"
+proof-
+ from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast
+ from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast
+ from k k' have "a = a*k*k'" by simp
+ with mult_cancel_left1[where c="a" and b="k*k'"]
+ have kk':"k*k' = 1" using `a\<noteq>0` by (simp add: mult_assoc)
+ hence "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" by (simp add: zmult_eq_1_iff)
+ thus ?thesis using k k' by auto
+qed
+
+lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
+ apply (subgoal_tac "m = n + (m - n)")
+ apply (erule ssubst)
+ apply (blast intro: dvd_add, simp)
+ done
+
+lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
+apply (rule iffI)
+ apply (erule_tac [2] dvd_add)
+ apply (subgoal_tac "n = (n + k * m) - k * m")
+ apply (erule ssubst)
+ apply (erule dvd_diff)
+ apply(simp_all)
+done
+
+lemma dvd_imp_le_int:
+ fixes d i :: int
+ assumes "i \<noteq> 0" and "d dvd i"
+ shows "\<bar>d\<bar> \<le> \<bar>i\<bar>"
+proof -
+ from `d dvd i` obtain k where "i = d * k" ..
+ with `i \<noteq> 0` have "k \<noteq> 0" by auto
+ then have "1 \<le> \<bar>k\<bar>" and "0 \<le> \<bar>d\<bar>" by auto
+ then have "\<bar>d\<bar> * 1 \<le> \<bar>d\<bar> * \<bar>k\<bar>" by (rule mult_left_mono)
+ with `i = d * k` show ?thesis by (simp add: abs_mult)
+qed
+
+lemma zdvd_not_zless:
+ fixes m n :: int
+ assumes "0 < m" and "m < n"
+ shows "\<not> n dvd m"
+proof
+ from assms have "0 < n" by auto
+ assume "n dvd m" then obtain k where k: "m = n * k" ..
+ with `0 < m` have "0 < n * k" by auto
+ with `0 < n` have "0 < k" by (simp add: zero_less_mult_iff)
+ with k `0 < n` `m < n` have "n * k < n * 1" by simp
+ with `0 < n` `0 < k` show False unfolding mult_less_cancel_left by auto
+qed
+
+lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)"
+ shows "m dvd n"
+proof-
+ from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast
+ {assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp
+ with h have False by (simp add: mult_assoc)}
+ hence "n = m * h" by blast
+ thus ?thesis by simp
+qed
+
+theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
+proof -
+ have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y"
+ proof -
+ fix k
+ assume A: "int y = int x * k"
+ then show "x dvd y" proof (cases k)
+ case (1 n) with A have "y = x * n" by (simp add: of_nat_mult [symmetric])
+ then show ?thesis ..
+ next
+ case (2 n) with A have "int y = int x * (- int (Suc n))" by simp
+ also have "\<dots> = - (int x * int (Suc n))" by (simp only: mult_minus_right)
+ also have "\<dots> = - int (x * Suc n)" by (simp only: of_nat_mult [symmetric])
+ finally have "- int (x * Suc n) = int y" ..
+ then show ?thesis by (simp only: negative_eq_positive) auto
+ qed
+ qed
+ then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left of_nat_mult)
+qed
+
+lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
+proof
+ assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp
+ hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)
+ hence "nat \<bar>x\<bar> = 1" by simp
+ thus "\<bar>x\<bar> = 1" by (cases "x < 0", auto)
+next
+ assume "\<bar>x\<bar>=1"
+ then have "x = 1 \<or> x = -1" by auto
+ then show "x dvd 1" by (auto intro: dvdI)
+qed
+
+lemma zdvd_mult_cancel1:
+ assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
+proof
+ assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m"
+ by (cases "n >0", auto simp add: minus_dvd_iff minus_equation_iff)
+next
+ assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp
+ from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
+qed
+
+lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
+ unfolding zdvd_int by (cases "z \<ge> 0") simp_all
+
+lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
+ unfolding zdvd_int by (cases "z \<ge> 0") simp_all
+
+lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
+ by (auto simp add: dvd_int_iff)
+
+lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
+ apply (rule_tac z=n in int_cases)
+ apply (auto simp add: dvd_int_iff)
+ apply (rule_tac z=z in int_cases)
+ apply (auto simp add: dvd_imp_le)
+ done
+
+
subsection {* Configuration of the code generator *}
code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int"
--- a/src/HOL/IntDiv.thy Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/IntDiv.thy Thu Oct 29 16:22:14 2009 +0000
@@ -1024,139 +1024,16 @@
lemmas zdvd_iff_zmod_eq_0_number_of [simp] =
dvd_eq_mod_eq_0 [of "number_of x::int" "number_of y::int", standard]
-lemma zdvd_anti_sym:
- "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
- apply (simp add: dvd_def, auto)
- apply (simp add: mult_assoc zero_less_mult_iff zmult_eq_1_iff)
- done
-
-lemma zdvd_dvd_eq: assumes "a \<noteq> 0" and "(a::int) dvd b" and "b dvd a"
- shows "\<bar>a\<bar> = \<bar>b\<bar>"
-proof-
- from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast
- from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast
- from k k' have "a = a*k*k'" by simp
- with mult_cancel_left1[where c="a" and b="k*k'"]
- have kk':"k*k' = 1" using `a\<noteq>0` by (simp add: mult_assoc)
- hence "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" by (simp add: zmult_eq_1_iff)
- thus ?thesis using k k' by auto
-qed
-
-lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
- apply (subgoal_tac "m = n + (m - n)")
- apply (erule ssubst)
- apply (blast intro: dvd_add, simp)
- done
-
-lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
-apply (rule iffI)
- apply (erule_tac [2] dvd_add)
- apply (subgoal_tac "n = (n + k * m) - k * m")
- apply (erule ssubst)
- apply (erule dvd_diff)
- apply(simp_all)
-done
-
lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
by (rule dvd_mod) (* TODO: remove *)
lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
by (rule dvd_mod_imp_dvd) (* TODO: remove *)
-lemma dvd_imp_le_int: "(i::int) ~= 0 ==> d dvd i ==> abs d <= abs i"
-apply(auto simp:abs_if)
- apply(clarsimp simp:dvd_def mult_less_0_iff)
- using mult_le_cancel_left_neg[of _ "-1::int"]
- apply(clarsimp simp:dvd_def mult_less_0_iff)
- apply(clarsimp simp:dvd_def mult_less_0_iff
- minus_mult_right simp del: mult_minus_right)
-apply(clarsimp simp:dvd_def mult_less_0_iff)
-done
-
-lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)"
- apply (auto elim!: dvdE)
- apply (subgoal_tac "0 < n")
- prefer 2
- apply (blast intro: order_less_trans)
- apply (simp add: zero_less_mult_iff)
- done
-
lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)"
using zmod_zdiv_equality[where a="m" and b="n"]
by (simp add: algebra_simps)
-lemma zdvd_mult_div_cancel:"(n::int) dvd m \<Longrightarrow> n * (m div n) = m"
-apply (subgoal_tac "m mod n = 0")
- apply (simp add: zmult_div_cancel)
-apply (simp only: dvd_eq_mod_eq_0)
-done
-
-lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)"
- shows "m dvd n"
-proof-
- from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast
- {assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp
- with h have False by (simp add: mult_assoc)}
- hence "n = m * h" by blast
- thus ?thesis by simp
-qed
-
-theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
-proof -
- have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y"
- proof -
- fix k
- assume A: "int y = int x * k"
- then show "x dvd y" proof (cases k)
- case (1 n) with A have "y = x * n" by (simp add: zmult_int)
- then show ?thesis ..
- next
- case (2 n) with A have "int y = int x * (- int (Suc n))" by simp
- also have "\<dots> = - (int x * int (Suc n))" by (simp only: mult_minus_right)
- also have "\<dots> = - int (x * Suc n)" by (simp only: zmult_int)
- finally have "- int (x * Suc n) = int y" ..
- then show ?thesis by (simp only: negative_eq_positive) auto
- qed
- qed
- then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left int_mult)
-qed
-
-lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
-proof
- assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp
- hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)
- hence "nat \<bar>x\<bar> = 1" by simp
- thus "\<bar>x\<bar> = 1" by (cases "x < 0", auto)
-next
- assume "\<bar>x\<bar>=1" thus "x dvd 1"
- by(cases "x < 0",simp_all add: minus_equation_iff dvd_eq_mod_eq_0)
-qed
-lemma zdvd_mult_cancel1:
- assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
-proof
- assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m"
- by (cases "n >0", auto simp add: minus_dvd_iff minus_equation_iff)
-next
- assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp
- from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
-qed
-
-lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
- unfolding zdvd_int by (cases "z \<ge> 0") simp_all
-
-lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
- unfolding zdvd_int by (cases "z \<ge> 0") simp_all
-
-lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
- by (auto simp add: dvd_int_iff)
-
-lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
- apply (rule_tac z=n in int_cases)
- apply (auto simp add: dvd_int_iff)
- apply (rule_tac z=z in int_cases)
- apply (auto simp add: dvd_imp_le)
- done
-
lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m"
apply (induct "y", auto)
apply (rule zmod_zmult1_eq [THEN trans])
@@ -1182,6 +1059,12 @@
lemma abs_div: "(y::int) dvd x \<Longrightarrow> abs (x div y) = abs x div abs y"
by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)
+lemma zdvd_mult_div_cancel:"(n::int) dvd m \<Longrightarrow> n * (m div n) = m"
+apply (subgoal_tac "m mod n = 0")
+ apply (simp add: zmult_div_cancel)
+apply (simp only: dvd_eq_mod_eq_0)
+done
+
text{*Suggested by Matthias Daum*}
lemma int_power_div_base:
"\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"
@@ -1318,6 +1201,73 @@
thus ?lhs by simp
qed
+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])
+
+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])
+
+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]
+
+
+subsection {* Transfer setup *}
+
+lemma transfer_nat_int_functions:
+ "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
+ "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
+ by (auto simp add: nat_div_distrib nat_mod_distrib)
+
+lemma transfer_nat_int_function_closures:
+ "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
+ "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
+ apply (cases "y = 0")
+ apply (auto simp add: pos_imp_zdiv_nonneg_iff)
+ apply (cases "y = 0")
+ apply auto
+done
+
+declare TransferMorphism_nat_int[transfer add return:
+ transfer_nat_int_functions
+ transfer_nat_int_function_closures
+]
+
+lemma transfer_int_nat_functions:
+ "(int x) div (int y) = int (x div y)"
+ "(int x) mod (int y) = int (x mod y)"
+ by (auto simp add: zdiv_int zmod_int)
+
+lemma transfer_int_nat_function_closures:
+ "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
+ "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
+ by (simp_all only: is_nat_def transfer_nat_int_function_closures)
+
+declare TransferMorphism_int_nat[transfer add return:
+ transfer_int_nat_functions
+ transfer_int_nat_function_closures
+]
+
subsection {* Code generation *}
--- a/src/HOL/IsaMakefile Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/IsaMakefile Thu Oct 29 16:22:14 2009 +0000
@@ -138,7 +138,6 @@
PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES)\
Complete_Lattice.thy \
Datatype.thy \
- Divides.thy \
Extraction.thy \
Finite_Set.thy \
Fun.thy \
@@ -224,7 +223,6 @@
Tools/sat_funcs.ML \
Tools/sat_solver.ML \
Tools/split_rule.ML \
- Tools/transfer.ML \
Tools/typecopy.ML \
Tools/typedef_codegen.ML \
Tools/typedef.ML \
@@ -246,6 +244,7 @@
ATP_Linkup.thy \
Code_Evaluation.thy \
Code_Numeral.thy \
+ Divides.thy \
Equiv_Relations.thy \
Groebner_Basis.thy \
Hilbert_Choice.thy \
@@ -255,6 +254,7 @@
Main.thy \
Map.thy \
Nat_Numeral.thy \
+ Nat_Transfer.thy \
Presburger.thy \
Predicate_Compile.thy \
Quickcheck.thy \
@@ -276,6 +276,7 @@
Tools/Groebner_Basis/misc.ML \
Tools/Groebner_Basis/normalizer.ML \
Tools/Groebner_Basis/normalizer_data.ML \
+ Tools/choice_specification.ML \
Tools/int_arith.ML \
Tools/list_code.ML \
Tools/meson.ML \
@@ -299,7 +300,6 @@
Tools/Qelim/presburger.ML \
Tools/Qelim/qelim.ML \
Tools/recdef.ML \
- Tools/choice_specification.ML \
Tools/res_atp.ML \
Tools/res_axioms.ML \
Tools/res_clause.ML \
@@ -307,6 +307,7 @@
Tools/res_reconstruct.ML \
Tools/string_code.ML \
Tools/string_syntax.ML \
+ Tools/transfer.ML \
Tools/TFL/casesplit.ML \
Tools/TFL/dcterm.ML \
Tools/TFL/post.ML \
@@ -334,7 +335,6 @@
Log.thy \
Lubs.thy \
MacLaurin.thy \
- Nat_Transfer.thy \
NthRoot.thy \
PReal.thy \
Parity.thy \
@@ -1069,6 +1069,7 @@
Multivariate_Analysis/Convex_Euclidean_Space.thy
@cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Multivariate_Analysis
+
## HOL-Probability
HOL-Probability: HOL $(LOG)/HOL-Probability.gz
@@ -1079,7 +1080,8 @@
Probability/SeriesPlus.thy \
Probability/Caratheodory.thy \
Probability/Measure.thy
- $(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Probability
+ @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Probability
+
## HOL-Nominal
--- a/src/HOL/List.thy Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/List.thy Thu Oct 29 16:22:14 2009 +0000
@@ -3587,8 +3587,8 @@
by (blast intro: listrel.intros)
lemma listrel_Cons:
- "listrel r `` {x#xs} = set_Cons (r``{x}) (listrel r `` {xs})";
-by (auto simp add: set_Cons_def intro: listrel.intros)
+ "listrel r `` {x#xs} = set_Cons (r``{x}) (listrel r `` {xs})"
+by (auto simp add: set_Cons_def intro: listrel.intros)
subsection {* Size function *}
@@ -3615,6 +3615,45 @@
by (induct xs) force+
+subsection {* Transfer *}
+
+definition
+ embed_list :: "nat list \<Rightarrow> int list"
+where
+ "embed_list l = map int l"
+
+definition
+ nat_list :: "int list \<Rightarrow> bool"
+where
+ "nat_list l = nat_set (set l)"
+
+definition
+ return_list :: "int list \<Rightarrow> nat list"
+where
+ "return_list l = map nat l"
+
+lemma transfer_nat_int_list_return_embed: "nat_list l \<longrightarrow>
+ embed_list (return_list l) = l"
+ unfolding embed_list_def return_list_def nat_list_def nat_set_def
+ apply (induct l)
+ apply auto
+done
+
+lemma transfer_nat_int_list_functions:
+ "l @ m = return_list (embed_list l @ embed_list m)"
+ "[] = return_list []"
+ unfolding return_list_def embed_list_def
+ apply auto
+ apply (induct l, auto)
+ apply (induct m, auto)
+done
+
+(*
+lemma transfer_nat_int_fold1: "fold f l x =
+ fold (%x. f (nat x)) (embed_list l) x";
+*)
+
+
subsection {* Code generator *}
subsubsection {* Setup *}
@@ -4017,5 +4056,4 @@
"list_ex P [i..j] = (~ all_from_to_int (%x. ~P x) i j)"
by(simp add: all_from_to_int_iff_ball list_ex_iff)
-
end
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Thu Oct 29 16:22:14 2009 +0000
@@ -151,11 +151,11 @@
(* Mirabelle utility functions *)
-val goal_thm_of = snd o snd o Proof.get_goal
+val goal_thm_of = #goal o Proof.raw_goal (* FIXME ?? *)
fun can_apply time tac st =
let
- val (ctxt, (facts, goal)) = Proof.get_goal st
+ val {context = ctxt, facts, goal} = Proof.raw_goal st (* FIXME ?? *)
val full_tac = HEADGOAL (Method.insert_tac facts THEN' tac ctxt)
in
(case TimeLimit.timeLimit time (Seq.pull o full_tac) goal of
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Oct 29 16:22:14 2009 +0000
@@ -301,13 +301,13 @@
fun run_sh prover hard_timeout timeout dir st =
let
- val (ctxt, goal) = Proof.get_goal st
+ val {context = ctxt, facts, goal} = Proof.raw_goal st (* FIXME ?? *)
val change_dir = (fn SOME d => Config.put ATP_Wrapper.destdir d | _ => I)
val ctxt' =
ctxt
|> change_dir dir
|> Config.put ATP_Wrapper.measure_runtime true
- val problem = ATP_Wrapper.problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', goal);
+ val problem = ATP_Wrapper.problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', (facts, goal));
val time_limit =
(case hard_timeout of
@@ -424,7 +424,7 @@
end
fun sledgehammer_action args id (st as {log, pre, name, ...}: Mirabelle.run_args) =
- let val goal = Thm.major_prem_of(snd(snd(Proof.get_goal pre))) in
+ let val goal = Thm.major_prem_of (#goal (Proof.raw_goal pre)) (* FIXME ?? *) in
if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal
then () else
let
--- a/src/HOL/Nat.thy Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Nat.thy Thu Oct 29 16:22:14 2009 +0000
@@ -8,7 +8,7 @@
header {* Natural numbers *}
theory Nat
-imports Inductive Ring_and_Field
+imports Inductive Product_Type Ring_and_Field
uses
"~~/src/Tools/rat.ML"
"~~/src/Provers/Arith/cancel_sums.ML"
@@ -1600,6 +1600,75 @@
Least_Suc}, since there appears to be no need.*}
+subsection {* The divides relation on @{typ nat} *}
+
+lemma dvd_1_left [iff]: "Suc 0 dvd k"
+unfolding dvd_def by simp
+
+lemma dvd_1_iff_1 [simp]: "(m dvd Suc 0) = (m = Suc 0)"
+by (simp add: dvd_def)
+
+lemma nat_dvd_1_iff_1 [simp]: "m dvd (1::nat) \<longleftrightarrow> m = 1"
+by (simp add: dvd_def)
+
+lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
+ unfolding dvd_def
+ by (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff)
+
+text {* @{term "op dvd"} is a partial order *}
+
+interpretation dvd: order "op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"
+ proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym)
+
+lemma dvd_diff_nat[simp]: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
+unfolding dvd_def
+by (blast intro: diff_mult_distrib2 [symmetric])
+
+lemma dvd_diffD: "[| k dvd m-n; k dvd n; n\<le>m |] ==> k dvd (m::nat)"
+ apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
+ apply (blast intro: dvd_add)
+ done
+
+lemma dvd_diffD1: "[| k dvd m-n; k dvd m; n\<le>m |] ==> k dvd (n::nat)"
+by (drule_tac m = m in dvd_diff_nat, auto)
+
+lemma dvd_reduce: "(k dvd n + k) = (k dvd (n::nat))"
+ apply (rule iffI)
+ apply (erule_tac [2] dvd_add)
+ apply (rule_tac [2] dvd_refl)
+ apply (subgoal_tac "n = (n+k) -k")
+ prefer 2 apply simp
+ apply (erule ssubst)
+ apply (erule dvd_diff_nat)
+ apply (rule dvd_refl)
+ done
+
+lemma dvd_mult_cancel: "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n"
+ unfolding dvd_def
+ apply (erule exE)
+ apply (simp add: mult_ac)
+ done
+
+lemma dvd_mult_cancel1: "0<m ==> (m*n dvd m) = (n = (1::nat))"
+ apply auto
+ apply (subgoal_tac "m*n dvd m*1")
+ apply (drule dvd_mult_cancel, auto)
+ done
+
+lemma dvd_mult_cancel2: "0<m ==> (n*m dvd m) = (n = (1::nat))"
+ apply (subst mult_commute)
+ apply (erule dvd_mult_cancel1)
+ 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:
+ 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)
+
+
subsection {* size of a datatype value *}
class size =
--- a/src/HOL/Nat_Numeral.thy Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Nat_Numeral.thy Thu Oct 29 16:22:14 2009 +0000
@@ -6,8 +6,7 @@
header {* Binary numerals for the natural numbers *}
theory Nat_Numeral
-imports IntDiv
-uses ("Tools/nat_numeral_simprocs.ML")
+imports Int
begin
subsection {* Numerals for natural numbers *}
@@ -246,12 +245,12 @@
lemma power2_sum:
fixes x y :: "'a::number_ring"
shows "(x + y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> + 2 * x * y"
- by (simp add: ring_distribs power2_eq_square)
+ by (simp add: ring_distribs power2_eq_square mult_2) (rule mult_commute)
lemma power2_diff:
fixes x y :: "'a::number_ring"
shows "(x - y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> - 2 * x * y"
- by (simp add: ring_distribs power2_eq_square)
+ by (simp add: ring_distribs power2_eq_square mult_2) (rule mult_commute)
subsection {* Predicate for negative binary numbers *}
@@ -417,45 +416,6 @@
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]
-
-
subsection{*Comparisons*}
subsubsection{*Equals (=) *}
@@ -687,21 +647,16 @@
lemma power_number_of_even:
fixes z :: "'a::number_ring"
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
+by (cases "w \<ge> 0") (auto simp add: Let_def Bit0_def nat_number_of_def number_of_is_id
+ nat_add_distrib power_add simp del: nat_number_of)
lemma power_number_of_odd:
fixes z :: "'a::number_ring"
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)
+apply (auto simp add: Let_def Bit1_def nat_number_of_def number_of_is_id
+ mult_assoc nat_add_distrib power_add not_le simp del: nat_number_of)
+apply (simp add: not_le mult_2 [symmetric] add_assoc)
done
lemmas zpower_number_of_even = power_number_of_even [where 'a=int]
@@ -713,11 +668,6 @@
lemmas power_number_of_odd_number_of [simp] =
power_number_of_odd [of "number_of v", standard]
-
-(* 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)
@@ -727,22 +677,24 @@
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
+by (cases "w \<ge> 0") (auto simp add: Let_def Bit0_def nat_number_of_def number_of_is_id
+ nat_add_distrib simp del: nat_number_of)
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
+apply (auto simp add: Let_def Bit1_def nat_number_of_def number_of_is_id neg_def
+ nat_add_distrib simp del: nat_number_of)
+apply (simp add: mult_2 [symmetric] add_assoc)
+done
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)
+ by (fact Let_def)
lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::{number_ring})"
by (simp only: number_of_Min power_minus1_even)
@@ -750,6 +702,20 @@
lemma power_m1_odd: "(-1) ^ Suc(2*n) = (-1::'a::{number_ring})"
by (simp only: number_of_Min power_minus1_odd)
+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)"
+by (auto simp add: neg_def)
+
+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 (auto simp add: not_less Pls_def nat_number_of_def number_of_is_id
+ nat_mult_distrib simp del: nat_number_of)
+
subsection{*Literal arithmetic and @{term of_nat}*}
@@ -765,7 +731,7 @@
(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);
+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) =
@@ -774,124 +740,6 @@
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_numeral_simprocs.ML"
-
-declaration {*
- K (Lin_Arith.add_simps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}])
- #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1},
- @{thm nat_0}, @{thm nat_1},
- @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of},
- @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less},
- @{thm le_Suc_number_of}, @{thm le_number_of_Suc},
- @{thm less_Suc_number_of}, @{thm less_number_of_Suc},
- @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc},
- @{thm mult_Suc}, @{thm mult_Suc_right},
- @{thm add_Suc}, @{thm add_Suc_right},
- @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},
- @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of},
- @{thm if_True}, @{thm if_False}])
- #> Lin_Arith.add_simprocs (Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals))
-*}
-
-
subsubsection{*For simplifying @{term "Suc m - K"} and @{term "K - Suc m"}*}
text{*Where K above is a literal*}
@@ -977,35 +825,14 @@
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
+unfolding nat_1_add_1 [symmetric] left_distrib by simp
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
+by (auto simp add: nat_1_add_1 [symmetric])
text{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*}
@@ -1019,29 +846,4 @@
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/Nat_Transfer.thy Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Nat_Transfer.thy Thu Oct 29 16:22:14 2009 +0000
@@ -1,15 +1,26 @@
(* Authors: Jeremy Avigad and Amine Chaieb *)
-header {* Sets up transfer from nats to ints and back. *}
+header {* Generic transfer machinery; specific transfer from nats to ints and back. *}
theory Nat_Transfer
-imports Main Parity
+imports Nat_Numeral
+uses ("Tools/transfer.ML")
begin
+subsection {* Generic transfer machinery *}
+
+definition TransferMorphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
+ where "TransferMorphism a B \<longleftrightarrow> True"
+
+use "Tools/transfer.ML"
+
+setup Transfer.setup
+
+
subsection {* Set up transfer from nat to int *}
-(* set up transfer direction *)
+text {* set up transfer direction *}
lemma TransferMorphism_nat_int: "TransferMorphism nat (op <= (0::int))"
by (simp add: TransferMorphism_def)
@@ -20,7 +31,7 @@
labels: natint
]
-(* basic functions and relations *)
+text {* basic functions and relations *}
lemma transfer_nat_int_numerals:
"(0::nat) = nat 0"
@@ -43,31 +54,20 @@
"(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) * (nat y) = nat (x * y)"
"(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) - (nat y) = nat (tsub x y)"
"(x::int) >= 0 \<Longrightarrow> (nat x)^n = nat (x^n)"
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
by (auto simp add: eq_nat_nat_iff nat_mult_distrib
- nat_power_eq nat_div_distrib nat_mod_distrib tsub_def)
+ nat_power_eq tsub_def)
lemma transfer_nat_int_function_closures:
"(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x + y >= 0"
"(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x * y >= 0"
"(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> tsub x y >= 0"
"(x::int) >= 0 \<Longrightarrow> x^n >= 0"
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
"(0::int) >= 0"
"(1::int) >= 0"
"(2::int) >= 0"
"(3::int) >= 0"
"int z >= 0"
apply (auto simp add: zero_le_mult_iff tsub_def)
- apply (case_tac "y = 0")
- apply auto
- apply (subst pos_imp_zdiv_nonneg_iff, auto)
- apply (case_tac "y = 0")
- apply force
- apply (rule pos_mod_sign)
- apply arith
done
lemma transfer_nat_int_relations:
@@ -89,7 +89,21 @@
]
-(* first-order quantifiers *)
+text {* first-order quantifiers *}
+
+lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))"
+ by (simp split add: split_nat)
+
+lemma ex_nat: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> P (nat x))"
+proof
+ assume "\<exists>x. P x"
+ then obtain x where "P x" ..
+ then have "int x \<ge> 0 \<and> P (nat (int x))" by simp
+ then show "\<exists>x\<ge>0. P (nat x)" ..
+next
+ assume "\<exists>x\<ge>0. P (nat x)"
+ then show "\<exists>x. P x" by auto
+qed
lemma transfer_nat_int_quantifiers:
"(ALL (x::nat). P x) = (ALL (x::int). x >= 0 \<longrightarrow> P (nat x))"
@@ -110,7 +124,7 @@
cong: all_cong ex_cong]
-(* if *)
+text {* if *}
lemma nat_if_cong: "(if P then (nat x) else (nat y)) =
nat (if P then x else y)"
@@ -119,7 +133,7 @@
declare TransferMorphism_nat_int [transfer add return: nat_if_cong]
-(* operations with sets *)
+text {* operations with sets *}
definition
nat_set :: "int set \<Rightarrow> bool"
@@ -132,8 +146,6 @@
"A Un B = nat ` (int ` A Un int ` B)"
"A Int B = nat ` (int ` A Int int ` B)"
"{x. P x} = nat ` {x. x >= 0 & P(nat x)}"
- "{..n} = nat ` {0..int n}"
- "{m..n} = nat ` {int m..int n}" (* need all variants of these! *)
apply (rule card_image [symmetric])
apply (auto simp add: inj_on_def image_def)
apply (rule_tac x = "int x" in bexI)
@@ -144,17 +156,12 @@
apply auto
apply (rule_tac x = "int x" in exI)
apply auto
- apply (rule_tac x = "int x" in bexI)
- apply auto
- apply (rule_tac x = "int x" in bexI)
- apply auto
done
lemma transfer_nat_int_set_function_closures:
"nat_set {}"
"nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
"nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
- "x >= 0 \<Longrightarrow> nat_set {x..y}"
"nat_set {x. x >= 0 & P x}"
"nat_set (int ` C)"
"nat_set A \<Longrightarrow> x : A \<Longrightarrow> x >= 0" (* does it hurt to turn this on? *)
@@ -167,7 +174,6 @@
"(A = B) = (int ` A = int ` B)"
"(A < B) = (int ` A < int ` B)"
"(A <= B) = (int ` A <= int ` B)"
-
apply (rule iffI)
apply (erule finite_imageI)
apply (erule finite_imageD)
@@ -194,7 +200,7 @@
]
-(* setsum and setprod *)
+text {* setsum and setprod *}
(* this handles the case where the *domain* of f is nat *)
lemma transfer_nat_int_sum_prod:
@@ -262,52 +268,10 @@
transfer_nat_int_sum_prod_closure
cong: transfer_nat_int_sum_prod_cong]
-(* lists *)
-
-definition
- embed_list :: "nat list \<Rightarrow> int list"
-where
- "embed_list l = map int l";
-
-definition
- nat_list :: "int list \<Rightarrow> bool"
-where
- "nat_list l = nat_set (set l)";
-
-definition
- return_list :: "int list \<Rightarrow> nat list"
-where
- "return_list l = map nat l";
-
-thm nat_0_le;
-
-lemma transfer_nat_int_list_return_embed: "nat_list l \<longrightarrow>
- embed_list (return_list l) = l";
- unfolding embed_list_def return_list_def nat_list_def nat_set_def
- apply (induct l);
- apply auto;
-done;
-
-lemma transfer_nat_int_list_functions:
- "l @ m = return_list (embed_list l @ embed_list m)"
- "[] = return_list []";
- unfolding return_list_def embed_list_def;
- apply auto;
- apply (induct l, auto);
- apply (induct m, auto);
-done;
-
-(*
-lemma transfer_nat_int_fold1: "fold f l x =
- fold (%x. f (nat x)) (embed_list l) x";
-*)
-
-
-
subsection {* Set up transfer from int to nat *}
-(* set up transfer direction *)
+text {* set up transfer direction *}
lemma TransferMorphism_int_nat: "TransferMorphism int (UNIV :: nat set)"
by (simp add: TransferMorphism_def)
@@ -319,7 +283,11 @@
]
-(* basic functions and relations *)
+text {* basic functions and relations *}
+
+lemma UNIV_apply:
+ "UNIV x = True"
+ by (simp add: top_fun_eq top_bool_eq)
definition
is_nat :: "int \<Rightarrow> bool"
@@ -338,17 +306,13 @@
"(int x) * (int y) = int (x * y)"
"tsub (int x) (int y) = int (x - y)"
"(int x)^n = int (x^n)"
- "(int x) div (int y) = int (x div y)"
- "(int x) mod (int y) = int (x mod y)"
- by (auto simp add: int_mult tsub_def int_power zdiv_int zmod_int)
+ by (auto simp add: int_mult tsub_def int_power)
lemma transfer_int_nat_function_closures:
"is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)"
"is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x * y)"
"is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (tsub x y)"
"is_nat x \<Longrightarrow> is_nat (x^n)"
- "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
- "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
"is_nat 0"
"is_nat 1"
"is_nat 2"
@@ -361,12 +325,7 @@
"(int x < int y) = (x < y)"
"(int x <= int y) = (x <= y)"
"(int x dvd int y) = (x dvd y)"
- "(even (int x)) = (even x)"
- by (auto simp add: zdvd_int even_nat_def)
-
-lemma UNIV_apply:
- "UNIV x = True"
- by (simp add: top_fun_eq top_bool_eq)
+ by (auto simp add: zdvd_int)
declare TransferMorphism_int_nat[transfer add return:
transfer_int_nat_numerals
@@ -377,7 +336,7 @@
]
-(* first-order quantifiers *)
+text {* first-order quantifiers *}
lemma transfer_int_nat_quantifiers:
"(ALL (x::int) >= 0. P x) = (ALL (x::nat). P (int x))"
@@ -392,7 +351,7 @@
return: transfer_int_nat_quantifiers]
-(* if *)
+text {* if *}
lemma int_if_cong: "(if P then (int x) else (int y)) =
int (if P then x else y)"
@@ -402,7 +361,7 @@
-(* operations with sets *)
+text {* operations with sets *}
lemma transfer_int_nat_set_functions:
"nat_set A \<Longrightarrow> card A = card (nat ` A)"
@@ -410,7 +369,6 @@
"nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Un B = int ` (nat ` A Un nat ` B)"
"nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Int B = int ` (nat ` A Int nat ` B)"
"{x. x >= 0 & P x} = int ` {x. P(int x)}"
- "is_nat m \<Longrightarrow> is_nat n \<Longrightarrow> {m..n} = int ` {nat m..nat n}"
(* need all variants of these! *)
by (simp_all only: is_nat_def transfer_nat_int_set_functions
transfer_nat_int_set_function_closures
@@ -421,7 +379,6 @@
"nat_set {}"
"nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
"nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
- "is_nat x \<Longrightarrow> nat_set {x..y}"
"nat_set {x. x >= 0 & P x}"
"nat_set (int ` C)"
"nat_set A \<Longrightarrow> x : A \<Longrightarrow> is_nat x"
@@ -454,7 +411,7 @@
]
-(* setsum and setprod *)
+text {* setsum and setprod *}
(* this handles the case where the *domain* of f is int *)
lemma transfer_int_nat_sum_prod:
--- a/src/HOL/Nominal/nominal_datatype.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Nominal/nominal_datatype.ML Thu Oct 29 16:22:14 2009 +0000
@@ -567,13 +567,16 @@
val rep_set_names'' = map (Sign.full_bname thy3) rep_set_names';
val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
- Inductive.add_inductive_global (serial ())
+ thy3
+ |> Sign.map_naming Name_Space.conceal
+ |> Inductive.add_inductive_global (serial ())
{quiet_mode = false, verbose = false, kind = Thm.internalK,
alt_name = Binding.name big_rep_name, coind = false, no_elim = true, no_ind = false,
skip_mono = true, fork_mono = false}
(map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
(rep_set_names' ~~ recTs'))
- [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] thy3;
+ [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) []
+ ||> Sign.restore_naming thy3;
(**** Prove that representing set is closed under permutation ****)
@@ -1508,15 +1511,17 @@
([], [], [], [], 0);
val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) =
- thy10 |>
- Inductive.add_inductive_global (serial ())
+ thy10
+ |> Sign.map_naming Name_Space.conceal
+ |> Inductive.add_inductive_global (serial ())
{quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
alt_name = Binding.name big_rec_name, coind = false, no_elim = false, no_ind = false,
skip_mono = true, fork_mono = false}
(map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
(map dest_Free rec_fns)
- (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] ||>
- PureThy.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct");
+ (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []
+ ||> PureThy.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct")
+ ||> Sign.restore_naming thy10;
(** equivariance **)
--- a/src/HOL/Parity.thy Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Parity.thy Thu Oct 29 16:22:14 2009 +0000
@@ -28,6 +28,13 @@
end
+lemma transfer_int_nat_relations:
+ "even (int x) \<longleftrightarrow> even x"
+ by (simp add: even_nat_def)
+
+declare TransferMorphism_int_nat[transfer add return:
+ transfer_int_nat_relations
+]
lemma even_zero_int[simp]: "even (0::int)" by presburger
@@ -310,6 +317,8 @@
subsection {* General Lemmas About Division *}
+(*FIXME move to Divides.thy*)
+
lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1"
apply (induct "m")
apply (simp_all add: mod_Suc)
--- a/src/HOL/Plain.thy Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Plain.thy Thu Oct 29 16:22:14 2009 +0000
@@ -1,7 +1,7 @@
header {* Plain HOL *}
theory Plain
-imports Datatype FunDef Record Extraction Divides
+imports Datatype FunDef Record Extraction
begin
text {*
--- a/src/HOL/Power.thy Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Power.thy Thu Oct 29 16:22:14 2009 +0000
@@ -452,6 +452,12 @@
from power_strict_increasing_iff [OF this] less show ?thesis ..
qed
+lemma power_dvd_imp_le:
+ "i ^ m dvd i ^ n \<Longrightarrow> (1::nat) < i \<Longrightarrow> m \<le> n"
+ apply (rule power_le_imp_le_exp, assumption)
+ apply (erule dvd_imp_le, simp)
+ done
+
subsection {* Code generator tweak *}
--- a/src/HOL/Presburger.thy Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Presburger.thy Thu Oct 29 16:22:14 2009 +0000
@@ -385,20 +385,6 @@
text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}
-lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))"
- by (simp split add: split_nat)
-
-lemma ex_nat: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> P (nat x))"
-proof
- assume "\<exists>x. P x"
- then obtain x where "P x" ..
- then have "int x \<ge> 0 \<and> P (nat (int x))" by simp
- then show "\<exists>x\<ge>0. P (nat x)" ..
-next
- assume "\<exists>x\<ge>0. P (nat x)"
- then show "\<exists>x. P x" by auto
-qed
-
lemma zdiff_int_split: "P (int (x - y)) =
((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
by (case_tac "y \<le> x", simp_all add: zdiff_int)
--- a/src/HOL/Product_Type.thy Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Product_Type.thy Thu Oct 29 16:22:14 2009 +0000
@@ -6,7 +6,7 @@
header {* Cartesian products *}
theory Product_Type
-imports Inductive Nat
+imports Inductive
uses
("Tools/split_rule.ML")
("Tools/inductive_set.ML")
@@ -94,8 +94,6 @@
text {* code generator setup *}
-instance unit :: eq ..
-
lemma [code]:
"eq_class.eq (u\<Colon>unit) v \<longleftrightarrow> True" unfolding eq unit_eq [of u] unit_eq [of v] by rule+
@@ -932,8 +930,6 @@
subsubsection {* Code generator setup *}
-instance * :: (eq, eq) eq ..
-
lemma [code]:
"eq_class.eq (x1\<Colon>'a\<Colon>eq, y1\<Colon>'b\<Colon>eq) (x2, y2) \<longleftrightarrow> x1 = x2 \<and> y1 = y2" by (simp add: eq)
--- a/src/HOL/Ring_and_Field.thy Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Ring_and_Field.thy Thu Oct 29 16:22:14 2009 +0000
@@ -767,6 +767,8 @@
end
+class ordered_semiring_1 = ordered_semiring + semiring_1
+
class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +
assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
@@ -884,6 +886,8 @@
end
+class ordered_semiring_1_strict = ordered_semiring_strict + semiring_1
+
class mult_mono1 = times + zero + ord +
assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
@@ -2025,15 +2029,15 @@
lemma mult_right_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1
==> x * y <= x"
-by (auto simp add: mult_compare_simps);
+by (auto simp add: mult_compare_simps)
lemma mult_left_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1
==> y * x <= x"
-by (auto simp add: mult_compare_simps);
+by (auto simp add: mult_compare_simps)
lemma mult_imp_div_pos_le: "0 < (y::'a::ordered_field) ==> x <= z * y ==>
- x / y <= z";
-by (subst pos_divide_le_eq, assumption+);
+ x / y <= z"
+by (subst pos_divide_le_eq, assumption+)
lemma mult_imp_le_div_pos: "0 < (y::'a::ordered_field) ==> z * y <= x ==>
z <= x / y"
@@ -2060,8 +2064,8 @@
lemma frac_less: "(0::'a::ordered_field) <= x ==>
x < y ==> 0 < w ==> w <= z ==> x / z < y / w"
apply (rule mult_imp_div_pos_less)
- apply simp;
- apply (subst times_divide_eq_left);
+ apply simp
+ apply (subst times_divide_eq_left)
apply (rule mult_imp_less_div_pos, assumption)
apply (erule mult_less_le_imp_less)
apply simp_all
@@ -2071,7 +2075,7 @@
x <= y ==> 0 < w ==> w < z ==> x / z < y / w"
apply (rule mult_imp_div_pos_less)
apply simp_all
- apply (subst times_divide_eq_left);
+ apply (subst times_divide_eq_left)
apply (rule mult_imp_less_div_pos, assumption)
apply (erule mult_le_less_imp_less)
apply simp_all
--- a/src/HOL/SMT/Examples/SMT_Examples.thy Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/SMT/Examples/SMT_Examples.thy Thu Oct 29 16:22:14 2009 +0000
@@ -62,7 +62,7 @@
symm_f: "symm_f x y = symm_f y x"
lemma "a = a \<and> symm_f a b = symm_f b a"
using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_prop_09"]]
- by (smt add: symm_f)
+ by (smt symm_f)
(*
Taken from ~~/src/HOL/ex/SAT_Examples.thy.
@@ -524,7 +524,7 @@
"prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
lemma "prime_nat (4*m + 1) \<Longrightarrow> m \<ge> (1::nat)"
using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_nat_arith_07"]]
- by (smt add: prime_nat_def)
+ by (smt prime_nat_def)
section {* Bitvectors *}
@@ -686,7 +686,7 @@
lemma "id 3 = 3 \<and> id True = True"
using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_hol_03"]]
- by (smt add: id_def)
+ by (smt id_def)
lemma "i \<noteq> i1 \<and> i \<noteq> i2 \<Longrightarrow> ((f (i1 := v1)) (i2 := v2)) i = f i"
using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_hol_04"]]
@@ -694,7 +694,7 @@
lemma "map (\<lambda>i::nat. i + 1) [0, 1] = [1, 2]"
using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_hol_05"]]
- by (smt add: map.simps)
+ by (smt map.simps)
lemma "(ALL x. P x) | ~ All P"
using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_hol_06"]]
@@ -704,7 +704,7 @@
"dec_10 n = (if n < 10 then n else dec_10 (n - 10))"
lemma "dec_10 (4 * dec_10 4) = 6"
using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_hol_07"]]
- by (smt add: dec_10.simps)
+ by (smt dec_10.simps)
axiomatization
eval_dioph :: "int list \<Rightarrow> nat list \<Rightarrow> int"
@@ -721,7 +721,7 @@
eval_dioph ks (map (\<lambda>x. x div 2) xs) =
(l - eval_dioph ks (map (\<lambda>x. x mod 2) xs)) div 2)"
using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_hol_08"]]
- by (smt add: eval_dioph_mod[where n=2] eval_dioph_div_mult[where n=2])
+ by (smt eval_dioph_mod[where n=2] eval_dioph_div_mult[where n=2])
section {* Monomorphization examples *}
@@ -730,7 +730,7 @@
lemma poly_P: "P x \<and> (P [x] \<or> \<not>P[x])" by (simp add: P_def)
lemma "P (1::int)"
using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_mono_01"]]
- by (smt add: poly_P)
+ by (smt poly_P)
consts g :: "'a \<Rightarrow> nat"
axioms
@@ -739,6 +739,6 @@
g3: "g xs = length xs"
lemma "g (Some (3::int)) = g (Some True)"
using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_mono_02"]]
- by (smt add: g1 g2 g3 list.size)
+ by (smt g1 g2 g3 list.size)
end
--- a/src/HOL/SMT/Tools/smt_normalize.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/SMT/Tools/smt_normalize.ML Thu Oct 29 16:22:14 2009 +0000
@@ -33,7 +33,8 @@
AddFunUpdRules |
AddAbsMinMaxRules
- val normalize: config list -> Proof.context -> thm list -> cterm list * thm list
+ val normalize: config list -> Proof.context -> thm list ->
+ cterm list * thm list
val setup: theory -> theory
end
@@ -41,10 +42,42 @@
structure SMT_Normalize: SMT_NORMALIZE =
struct
-val norm_binder_conv = Conv.try_conv (More_Conv.rewrs_conv [
- @{lemma "All P == ALL x. P x" by (rule reflexive)},
- @{lemma "Ex P == EX x. P x" by (rule reflexive)},
- @{lemma "Let c P == let x = c in P x" by (rule reflexive)}])
+local
+ val all1 = @{lemma "All P == ALL x. P x" by (rule reflexive)}
+ val all2 = @{lemma "All == (%P. ALL x. P x)" by (rule reflexive)}
+ val ex1 = @{lemma "Ex P == EX x. P x" by (rule reflexive)}
+ val ex2 = @{lemma "Ex == (%P. EX x. P x)" by (rule reflexive)}
+ val let1 = @{lemma "Let c P == let x = c in P x" by (rule reflexive)}
+ val let2 = @{lemma "Let c == (%P. let x = c in P x)" by (rule reflexive)}
+ val let3 = @{lemma "Let == (%c P. let x = c in P x)" by (rule reflexive)}
+
+ fun all_abs_conv cv ctxt =
+ Conv.abs_conv (all_abs_conv cv o snd) ctxt else_conv cv ctxt
+ fun keep_conv ctxt = More_Conv.binder_conv norm_conv ctxt
+ and unfold_conv rule ctxt =
+ Conv.rewr_conv rule then_conv all_abs_conv keep_conv ctxt
+ and unfold_let_conv rule ctxt =
+ Conv.rewr_conv rule then_conv
+ all_abs_conv (fn cx => Conv.combination_conv
+ (Conv.arg_conv (norm_conv cx)) (Conv.abs_conv (norm_conv o snd) cx)) ctxt
+ and norm_conv ctxt ct =
+ (case Thm.term_of ct of
+ Const (@{const_name All}, _) $ Abs _ => keep_conv
+ | Const (@{const_name All}, _) $ _ => unfold_conv all1
+ | Const (@{const_name All}, _) => unfold_conv all2
+ | Const (@{const_name Ex}, _) $ Abs _ => keep_conv
+ | Const (@{const_name Ex}, _) $ _ => unfold_conv ex1
+ | Const (@{const_name Ex}, _) => unfold_conv ex2
+ | Const (@{const_name Let}, _) $ _ $ Abs _ => keep_conv
+ | Const (@{const_name Let}, _) $ _ $ _ => unfold_let_conv let1
+ | Const (@{const_name Let}, _) $ _ => unfold_let_conv let2
+ | Const (@{const_name Let}, _) => unfold_let_conv let3
+ | Abs _ => Conv.abs_conv (norm_conv o snd)
+ | _ $ _ => Conv.comb_conv o norm_conv
+ | _ => K Conv.all_conv) ctxt ct
+in
+val norm_binder_conv = norm_conv
+end
fun cert ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
@@ -65,10 +98,10 @@
Conv.fconv_rule (
Thm.beta_conversion true then_conv
Thm.eta_conversion then_conv
- More_Conv.bottom_conv (K norm_binder_conv) ctxt) #>
+ norm_binder_conv ctxt) #>
norm_def ctxt #>
Drule.forall_intr_vars #>
- Conv.fconv_rule ObjectLogic.atomize
+ Conv.fconv_rule (ObjectLogic.atomize then_conv norm_binder_conv ctxt)
fun instantiate_free (cv, ct) thm =
if Term.exists_subterm (equal (Thm.term_of cv)) (Thm.prop_of thm)
@@ -321,11 +354,9 @@
| Abs _ => at_lambda cvs
| _ $ _ => in_comb (repl cvs) (repl cvs)
| _ => none) ct
- and at_lambda cvs ct cx =
- let
- val (thm1, cx') = in_abs repl cvs ct cx
- val (thm2, cx'') = replace ctxt cvs (Thm.rhs_of thm1) cx'
- in (Thm.transitive thm1 thm2, cx'') end
+ and at_lambda cvs ct =
+ in_abs repl cvs ct #-> (fn thm =>
+ replace ctxt cvs (Thm.rhs_of thm) #>> Thm.transitive thm)
in repl [] end
in
fun lift_lambdas ctxt thms =
--- a/src/HOL/SMT/Tools/smt_solver.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/SMT/Tools/smt_solver.ML Thu Oct 29 16:22:14 2009 +0000
@@ -230,7 +230,7 @@
val smt_tac = smt_tac' false
val smt_method =
- Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) [] >>
+ Scan.optional Attrib.thms [] >>
(fn thms => fn ctxt => METHOD (fn facts =>
HEADGOAL (smt_tac ctxt (thms @ facts))))
--- a/src/HOL/SMT/Tools/smt_translate.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/SMT/Tools/smt_translate.ML Thu Oct 29 16:22:14 2009 +0000
@@ -201,9 +201,9 @@
fun dest_trigger (@{term trigger} $ tl $ t) = (HOLogic.dest_list tl, t)
| dest_trigger t = ([], t)
- fun pat f ps (Const (@{const_name pat}, _) $ p) = SPat (rev (f p :: ps))
- | pat f ps (Const (@{const_name nopat}, _) $ p) = SNoPat (rev (f p :: ps))
- | pat f ps (Const (@{const_name andpat}, _) $ p $ t) = pat f (f p :: ps) t
+ fun pat f ts (Const (@{const_name pat}, _) $ t) = SPat (rev (f t :: ts))
+ | pat f ts (Const (@{const_name nopat}, _) $ t) = SNoPat (rev (f t :: ts))
+ | pat f ts (Const (@{const_name andpat}, _) $ p $ t) = pat f (f t :: ts) p
| pat _ _ t = raise TERM ("pat", [t])
fun trans Ts t =
--- a/src/HOL/SMT/Tools/z3_solver.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/SMT/Tools/z3_solver.ML Thu Oct 29 16:22:14 2009 +0000
@@ -43,8 +43,11 @@
fun check_unsat recon output =
let
- val raw = not o String.isPrefix "WARNING" orf String.isPrefix "ERROR"
- val (ls, l) = the_default ([], "") (try split_last (filter raw output))
+ fun jnk l =
+ String.isPrefix "WARNING" l orelse
+ String.isPrefix "ERROR" l orelse
+ forall Symbol.is_ascii_blank (Symbol.explode l)
+ val (ls, l) = the_default ([], "") (try split_last (filter_out jnk output))
in
if String.isPrefix "unsat" l then ls
else if String.isPrefix "sat" l then raise_cex true recon ls
--- a/src/HOL/SetInterval.thy Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/SetInterval.thy Thu Oct 29 16:22:14 2009 +0000
@@ -9,7 +9,7 @@
header {* Set intervals *}
theory SetInterval
-imports Int
+imports Int Nat_Transfer
begin
context ord
@@ -1150,4 +1150,41 @@
"\<Prod>i\<le>n. t" == "CONST setprod (\<lambda>i. t) {..n}"
"\<Prod>i<n. t" == "CONST setprod (\<lambda>i. t) {..<n}"
+subsection {* Transfer setup *}
+
+lemma transfer_nat_int_set_functions:
+ "{..n} = nat ` {0..int n}"
+ "{m..n} = nat ` {int m..int n}" (* need all variants of these! *)
+ apply (auto simp add: image_def)
+ apply (rule_tac x = "int x" in bexI)
+ apply auto
+ apply (rule_tac x = "int x" in bexI)
+ apply auto
+ done
+
+lemma transfer_nat_int_set_function_closures:
+ "x >= 0 \<Longrightarrow> nat_set {x..y}"
+ by (simp add: nat_set_def)
+
+declare TransferMorphism_nat_int[transfer add
+ return: transfer_nat_int_set_functions
+ transfer_nat_int_set_function_closures
+]
+
+lemma transfer_int_nat_set_functions:
+ "is_nat m \<Longrightarrow> is_nat n \<Longrightarrow> {m..n} = int ` {nat m..nat n}"
+ by (simp only: is_nat_def transfer_nat_int_set_functions
+ transfer_nat_int_set_function_closures
+ transfer_nat_int_set_return_embed nat_0_le
+ cong: transfer_nat_int_set_cong)
+
+lemma transfer_int_nat_set_function_closures:
+ "is_nat x \<Longrightarrow> nat_set {x..y}"
+ by (simp only: transfer_nat_int_set_function_closures is_nat_def)
+
+declare TransferMorphism_int_nat[transfer add
+ return: transfer_int_nat_set_functions
+ transfer_int_nat_set_function_closures
+]
+
end
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Thu Oct 29 16:22:14 2009 +0000
@@ -254,7 +254,7 @@
NONE => warning ("Unknown external prover: " ^ quote name)
| SOME prover =>
let
- val full_goal as (ctxt, (_, goal)) = Proof.get_goal proof_state;
+ val {context = ctxt, facts, goal} = Proof.raw_goal proof_state; (* FIXME Proof.goal *)
val desc =
"external prover " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
@@ -262,7 +262,7 @@
val _ = SimpleThread.fork true (fn () =>
let
val _ = register birth_time death_time (Thread.self (), desc);
- val problem = ATP_Wrapper.problem_of_goal (! full_types) i full_goal;
+ val problem = ATP_Wrapper.problem_of_goal (! full_types) i (ctxt, (facts, goal));
val result =
let val {success, message, ...} = prover (! timeout) problem;
in (success, message) end
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Thu Oct 29 16:22:14 2009 +0000
@@ -104,10 +104,11 @@
val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ " theorems... ")
val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
+ val {context = ctxt, facts, goal} = Proof.raw_goal state (* FIXME ?? *)
val problem =
{with_full_types = ! ATP_Manager.full_types,
subgoal = subgoalno,
- goal = Proof.get_goal state,
+ goal = (ctxt, (facts, goal)),
axiom_clauses = SOME axclauses,
filtered_clauses = filtered}
val (result, proof) = produce_answer (prover time_limit problem)
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Oct 29 16:22:14 2009 +0000
@@ -153,13 +153,17 @@
(descr' ~~ recTs ~~ rec_sets') ([], 0);
val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
- Inductive.add_inductive_global (serial ())
+ thy0
+ |> Sign.map_naming Name_Space.conceal
+ |> Inductive.add_inductive_global (serial ())
{quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true,
skip_mono = true, fork_mono = false}
(map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
(map dest_Free rec_fns)
- (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] thy0;
+ (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []
+ ||> Sign.restore_naming thy0
+ ||> Theory.checkpoint;
(* prove uniqueness and termination of primrec combinators *)
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Thu Oct 29 16:22:14 2009 +0000
@@ -170,12 +170,16 @@
((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names');
val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
- Inductive.add_inductive_global (serial ())
+ thy1
+ |> Sign.map_naming Name_Space.conceal
+ |> Inductive.add_inductive_global (serial ())
{quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
alt_name = Binding.name big_rec_name, coind = false, no_elim = true, no_ind = false,
skip_mono = true, fork_mono = false}
(map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') []
- (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] thy1;
+ (map (fn x => (Attrib.empty_binding, x)) intr_ts) []
+ ||> Sign.restore_naming thy1
+ ||> Theory.checkpoint;
(********************************* typedef ********************************)
--- a/src/HOL/Tools/Function/function_core.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Tools/Function/function_core.ML Thu Oct 29 16:22:14 2009 +0000
@@ -488,7 +488,9 @@
|> Syntax.check_term lthy
val ((f, (_, f_defthm)), lthy) =
- LocalTheory.define Thm.internalK ((Binding.name (function_name fname), mixfix), ((Binding.name fdefname, []), f_def)) lthy
+ LocalTheory.define Thm.internalK
+ ((Binding.name (function_name fname), mixfix),
+ ((Binding.conceal (Binding.name fdefname), []), f_def)) lthy
in
((f, f_defthm), lthy)
end
--- a/src/HOL/Tools/Function/inductive_wrap.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Tools/Function/inductive_wrap.ML Thu Oct 29 16:22:14 2009 +0000
@@ -39,7 +39,9 @@
fun inductive_def defs (((R, T), mixfix), lthy) =
let
val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) =
- Inductive.add_inductive_i
+ lthy
+ |> LocalTheory.conceal
+ |> Inductive.add_inductive_i
{quiet_mode = false,
verbose = ! Toplevel.debug,
kind = Thm.internalK,
@@ -53,7 +55,7 @@
[] (* no parameters *)
(map (fn t => (Attrib.empty_binding, t)) defs) (* the intros *)
[] (* no special monos *)
- lthy
+ ||> LocalTheory.restore_naming lthy
val intrs = map2 (requantify lthy (R, T)) defs intrs_gen
--- a/src/HOL/Tools/Function/mutual.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Tools/Function/mutual.ML Thu Oct 29 16:22:14 2009 +0000
@@ -146,9 +146,9 @@
fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
let
val ((f, (_, f_defthm)), lthy') =
- LocalTheory.define Thm.internalK ((Binding.name fname, mixfix),
- ((Binding.name (fname ^ "_def"), []), Term.subst_bound (fsum, f_def)))
- lthy
+ LocalTheory.define Thm.internalK
+ ((Binding.name fname, mixfix),
+ (apfst Binding.conceal Attrib.empty_binding, Term.subst_bound (fsum, f_def))) lthy
in
(MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def,
f=SOME f, f_defthm=SOME f_defthm },
--- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Oct 29 16:22:14 2009 +0000
@@ -854,7 +854,7 @@
fun pick_nits_in_subgoal state params auto subgoal =
let
val ctxt = Proof.context_of state
- val t = state |> Proof.get_goal |> snd |> snd |> prop_of
+ val t = state |> Proof.raw_goal |> #goal |> prop_of
in
if Logic.count_prems t = 0 then
(priority "No subgoal!"; ("none", state))
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Oct 29 16:22:14 2009 +0000
@@ -417,7 +417,7 @@
let
val thy = Proof.theory_of state
val ctxt = Proof.context_of state
- val thm = snd (snd (Proof.get_goal state))
+ val thm = #goal (Proof.raw_goal state)
val _ = List.app check_raw_param override_params
val params as {blocking, debug, ...} =
extract_params ctxt auto (default_raw_params thy) override_params
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Oct 29 16:22:14 2009 +0000
@@ -368,14 +368,18 @@
if is_some (try (map (cterm_of thy)) intr_ts) then
let
val (ind_result, thy') =
- Inductive.add_inductive_global (serial ())
+ thy
+ |> Sign.map_naming Name_Space.conceal
+ |> Inductive.add_inductive_global (serial ())
{quiet_mode = false, verbose = false, kind = Thm.internalK,
alt_name = Binding.empty, coind = false, no_elim = false,
no_ind = false, skip_mono = false, fork_mono = false}
- (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (distinct (op =) (map dest_Free preds)))
+ (map (fn (s, T) =>
+ ((Binding.name s, T), NoSyn)) (distinct (op =) (map dest_Free preds)))
pnames
(map (fn x => (Attrib.empty_binding, x)) intr_ts)
- [] thy
+ []
+ ||> Sign.restore_naming thy
val prednames = map (fst o dest_Const) (#preds ind_result)
(* val rewr_thms = map mk_rewr_eq ((distinct (op =) funs) ~~ (#preds ind_result)) *)
(* add constants to my table *)
--- a/src/HOL/Tools/inductive.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Tools/inductive.ML Thu Oct 29 16:22:14 2009 +0000
@@ -592,7 +592,7 @@
(** specification of (co)inductive predicates **)
fun mk_ind_def quiet_mode skip_mono fork_mono alt_name coind cs intr_ts monos params cnames_syn ctxt =
- let
+ let (* FIXME proper naming convention: lthy *)
val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp};
val argTs = fold (combine (op =) o arg_types_of (length params)) cs [];
@@ -649,30 +649,37 @@
Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn))
else alt_name;
- val ((rec_const, (_, fp_def)), ctxt') = ctxt |>
- LocalTheory.define Thm.internalK
+ val ((rec_const, (_, fp_def)), ctxt') = ctxt
+ |> LocalTheory.conceal
+ |> LocalTheory.define Thm.internalK
((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
(Attrib.empty_binding, fold_rev lambda params
- (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)));
+ (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
+ ||> LocalTheory.restore_naming ctxt;
val fp_def' = Simplifier.rewrite (HOL_basic_ss addsimps [fp_def])
(cterm_of (ProofContext.theory_of ctxt') (list_comb (rec_const, params)));
- val specs = if length cs < 2 then [] else
- map_index (fn (i, (name_mx, c)) =>
- let
- val Ts = arg_types_of (length params) c;
- val xs = map Free (Variable.variant_frees ctxt intr_ts
- (mk_names "x" (length Ts) ~~ Ts))
- in
- (name_mx, (Attrib.empty_binding, fold_rev lambda (params @ xs)
- (list_comb (rec_const, params @ make_bool_args' bs i @
- make_args argTs (xs ~~ Ts)))))
- end) (cnames_syn ~~ cs);
- val (consts_defs, ctxt'') = fold_map (LocalTheory.define Thm.internalK) specs ctxt';
+ val specs =
+ if length cs < 2 then []
+ else
+ map_index (fn (i, (name_mx, c)) =>
+ let
+ val Ts = arg_types_of (length params) c;
+ val xs = map Free (Variable.variant_frees ctxt intr_ts
+ (mk_names "x" (length Ts) ~~ Ts))
+ in
+ (name_mx, (Attrib.empty_binding, fold_rev lambda (params @ xs)
+ (list_comb (rec_const, params @ make_bool_args' bs i @
+ make_args argTs (xs ~~ Ts)))))
+ end) (cnames_syn ~~ cs);
+ val (consts_defs, ctxt'') = ctxt'
+ |> LocalTheory.conceal
+ |> fold_map (LocalTheory.define Thm.internalK) specs
+ ||> LocalTheory.restore_naming ctxt';
val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos ctxt'';
val ((_, [mono']), ctxt''') =
- LocalTheory.note Thm.internalK (Attrib.empty_binding, [mono]) ctxt'';
+ LocalTheory.note Thm.internalK (apfst Binding.conceal Attrib.empty_binding, [mono]) ctxt'';
in (ctxt''', rec_name, mono', fp_def', map (#2 o #2) consts_defs,
list_comb (rec_const, params), preds, argTs, bs, xs)
@@ -697,7 +704,8 @@
val (intrs', ctxt1) =
ctxt |>
LocalTheory.notes kind
- (map (rec_qualified false) intr_bindings ~~ intr_atts ~~ map (fn th => [([th],
+ (map (rec_qualified false) intr_bindings ~~ intr_atts ~~
+ map (fn th => [([th],
[Attrib.internal (K (ContextRules.intro_query NONE)),
Attrib.internal (K Nitpick_Intros.add)])]) intrs) |>>
map (hd o snd);
--- a/src/HOL/Tools/inductive_set.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Tools/inductive_set.ML Thu Oct 29 16:22:14 2009 +0000
@@ -407,7 +407,7 @@
fun add_ind_set_def
{quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
cs intros monos params cnames_syn ctxt =
- let
+ let (* FIXME proper naming convention: lthy *)
val thy = ProofContext.theory_of ctxt;
val {set_arities, pred_arities, to_pred_simps, ...} =
PredSetConvData.get (Context.Proof ctxt);
@@ -419,7 +419,8 @@
val new_arities = filter_out
(fn (x as Free (_, T), _) => x mem params andalso length (binder_types T) > 1
| _ => false) (fold (snd #> infer) intros []);
- val params' = map (fn x => (case AList.lookup op = new_arities x of
+ val params' = map (fn x =>
+ (case AList.lookup op = new_arities x of
SOME fs =>
let
val T = HOLogic.dest_setT (fastype_of x);
@@ -482,11 +483,14 @@
cs' intros' monos' params1 cnames_syn' ctxt;
(* define inductive sets using previously defined predicates *)
- val (defs, ctxt2) = fold_map (LocalTheory.define Thm.internalK)
- (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
- fold_rev lambda params (HOLogic.Collect_const U $
- HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
- (cnames_syn ~~ cs_info ~~ preds)) ctxt1;
+ val (defs, ctxt2) = ctxt1
+ |> LocalTheory.conceal (* FIXME ?? *)
+ |> fold_map (LocalTheory.define Thm.internalK)
+ (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
+ fold_rev lambda params (HOLogic.Collect_const U $
+ HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
+ (cnames_syn ~~ cs_info ~~ preds))
+ ||> LocalTheory.restore_naming ctxt1;
(* prove theorems for converting predicate to set notation *)
val ctxt3 = fold
--- a/src/HOL/Tools/int_arith.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Tools/int_arith.ML Thu Oct 29 16:22:14 2009 +0000
@@ -98,9 +98,7 @@
#> Lin_Arith.add_lessD @{thm zless_imp_add1_zle}
#> Lin_Arith.add_simps (@{thms simp_thms} @ @{thms arith_simps} @ @{thms rel_simps}
@ @{thms arith_special} @ @{thms int_arith_rules})
- #> Lin_Arith.add_simprocs (Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc
- :: Numeral_Simprocs.combine_numerals
- :: Numeral_Simprocs.cancel_numerals)
+ #> Lin_Arith.add_simprocs [zero_one_idom_simproc]
#> Lin_Arith.set_number_of number_of
#> Lin_Arith.add_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT)
#> Lin_Arith.add_discrete_type @{type_name Int.int}
--- a/src/HOL/Tools/quickcheck_generators.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Tools/quickcheck_generators.ML Thu Oct 29 16:22:14 2009 +0000
@@ -84,7 +84,7 @@
thy
|> TheoryTarget.instantiation ([tyco], vs, @{sort random})
|> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition (NONE, (apfst (Binding.conceal) Attrib.empty_binding, eq)))
+ |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
|> snd
|> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
end;
@@ -177,7 +177,7 @@
val proj_eqs = map2 (fn v => fn proj => (v, lambda arg proj)) vs projs;
val proj_defs = map2 (fn Free (name, _) => fn (_, rhs) =>
((Binding.conceal (Binding.name name), NoSyn),
- (apfst (Binding.conceal) Attrib.empty_binding, rhs))) vs proj_eqs;
+ (apfst Binding.conceal Attrib.empty_binding, rhs))) vs proj_eqs;
val aux_eq' = Pattern.rewrite_term thy proj_eqs [] aux_eq;
fun prove_eqs aux_simp proj_defs lthy =
let
@@ -305,7 +305,7 @@
|> random_aux_specification prfx random_auxN auxs_eqs
|> `(fn lthy => map (Syntax.check_term lthy) random_defs)
|-> (fn random_defs' => fold_map (fn random_def =>
- Specification.definition (NONE, (apfst (Binding.conceal)
+ Specification.definition (NONE, (apfst Binding.conceal
Attrib.empty_binding, random_def))) random_defs')
|> snd
|> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
--- a/src/HOL/Tools/recdef.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Tools/recdef.ML Thu Oct 29 16:22:14 2009 +0000
@@ -263,8 +263,9 @@
error ("No termination condition #" ^ string_of_int i ^
" in recdef definition of " ^ quote name);
in
- Specification.theorem Thm.internalK NONE (K I) (Binding.name bname, atts)
- [] (Element.Shows [(Attrib.empty_binding, [(HOLogic.mk_Trueprop tc, [])])]) int lthy
+ Specification.theorem Thm.internalK NONE (K I)
+ (Binding.conceal (Binding.name bname), atts) []
+ (Element.Shows [(Attrib.empty_binding, [(HOLogic.mk_Trueprop tc, [])])]) int lthy
end;
val recdef_tc = gen_recdef_tc Attrib.intern_src Sign.intern_const;
--- a/src/HOL/Tools/refute_isar.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Tools/refute_isar.ML Thu Oct 29 16:22:14 2009 +0000
@@ -28,7 +28,7 @@
Toplevel.keep (fn state =>
let
val thy = Toplevel.theory_of state;
- val (_, st) = Proof.flat_goal (Toplevel.proof_of state);
+ val {goal = st, ...} = Proof.raw_goal (Toplevel.proof_of state);
in Refute.refute_goal thy parms st i end)));
--- a/src/HOL/Tools/transfer.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/Tools/transfer.ML Thu Oct 29 16:22:14 2009 +0000
@@ -14,8 +14,15 @@
structure Transfer : TRANSFER =
struct
-type entry = {inj : thm list, emb : thm list, ret : thm list, cong : thm list,
- guess : bool, hints : string list};
+type entry = { inj : thm list, emb : thm list, ret : thm list, cong : thm list,
+ guess : bool, hints : string list };
+
+fun merge_entry ({ inj = inj1, emb = emb1, ret = ret1, cong = cong1, guess = guess1, hints = hints1 } : entry,
+ { inj = inj2, emb = emb2, ret = ret2, cong = cong2, guess = guess2, hints = hints2 } : entry) =
+ { inj = merge Thm.eq_thm (inj1, inj2), emb = merge Thm.eq_thm (emb1, emb2),
+ ret = merge Thm.eq_thm (ret1, ret2), cong = merge Thm.eq_thm (cong1, cong2),
+ guess = guess1 andalso guess2, hints = merge (op =) (hints1, hints2) };
+
type data = simpset * (thm * entry) list;
structure Data = GenericDataFun
@@ -24,7 +31,7 @@
val empty = (HOL_ss, []);
val extend = I;
fun merge _ ((ss1, e1), (ss2, e2)) =
- (merge_ss (ss1, ss2), AList.merge Thm.eq_thm (K true) (e1, e2));
+ (merge_ss (ss1, ss2), AList.join Thm.eq_thm (K merge_entry) (e1, e2));
);
val get = Data.get o Context.Proof;
--- a/src/HOL/ex/Numeral.thy Thu Oct 29 16:21:43 2009 +0000
+++ b/src/HOL/ex/Numeral.thy Thu Oct 29 16:22:14 2009 +0000
@@ -5,7 +5,7 @@
header {* An experimental alternative numeral representation. *}
theory Numeral
-imports Int Inductive
+imports Plain Divides
begin
subsection {* The @{text num} type *}
--- a/src/Pure/General/name_space.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/Pure/General/name_space.ML Thu Oct 29 16:22:14 2009 +0000
@@ -40,6 +40,7 @@
val root_path: naming -> naming
val parent_path: naming -> naming
val mandatory_path: string -> naming -> naming
+ val transform_binding: naming -> binding -> binding
val full_name: naming -> binding -> string
val external_names: naming -> string -> string list
val declare: bool -> naming -> binding -> T -> string * T
@@ -254,14 +255,17 @@
(* full name *)
+fun transform_binding (Naming {conceal = true, ...}) = Binding.conceal
+ | transform_binding _ = I;
+
fun err_bad binding = error ("Bad name binding " ^ quote (Binding.str_of binding));
-fun name_spec (Naming {conceal = conceal1, path, ...}) binding =
+fun name_spec (naming as Naming {path, ...}) raw_binding =
let
- val (conceal2, prefix, name) = Binding.dest binding;
+ val binding = transform_binding naming raw_binding;
+ val (concealed, prefix, name) = Binding.dest binding;
val _ = Long_Name.is_qualified name andalso err_bad binding;
- val concealed = conceal1 orelse conceal2;
val spec1 = maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix);
val spec2 = if name = "" then [] else [(name, true)];
val spec = spec1 @ spec2;
--- a/src/Pure/Isar/expression.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/Pure/Isar/expression.ML Thu Oct 29 16:22:14 2009 +0000
@@ -641,7 +641,8 @@
|> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
|> Sign.declare_const ((bname, predT), NoSyn) |> snd
|> PureThy.add_defs false
- [((Binding.map_name Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])];
+ [((Binding.conceal (Binding.map_name Thm.def_name bname), Logic.mk_equals (head, body)),
+ [Thm.kind_internal])];
val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
val cert = Thm.cterm_of defs_thy;
@@ -682,7 +683,7 @@
thy'
|> Sign.mandatory_path (Binding.name_of aname)
|> PureThy.note_thmss Thm.internalK
- [((Binding.name introN, []), [([intro], [Locale.unfold_add])])]
+ [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.unfold_add])])]
||> Sign.restore_naming thy';
in (SOME statement, SOME intro, axioms, thy'') end;
val (b_pred, b_intro, b_axioms, thy'''') =
@@ -696,8 +697,8 @@
thy'''
|> Sign.mandatory_path (Binding.name_of pname)
|> PureThy.note_thmss Thm.internalK
- [((Binding.name introN, []), [([intro], [Locale.intro_add])]),
- ((Binding.name axiomsN, []),
+ [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.intro_add])]),
+ ((Binding.conceal (Binding.name axiomsN), []),
[(map (Drule.standard o Element.conclude_witness) axioms, [])])]
||> Sign.restore_naming thy''';
in (SOME statement, SOME intro, axioms, thy'''') end;
@@ -753,10 +754,10 @@
val asm = if is_some b_statement then b_statement else a_statement;
val notes =
- if is_some asm
- then [(Thm.internalK, [((Binding.suffix_name ("_" ^ axiomsN) bname, []),
- [([Assumption.assume (cterm_of thy' (the asm))],
- [(Attrib.internal o K) Locale.witness_add])])])]
+ if is_some asm then
+ [(Thm.internalK, [((Binding.conceal (Binding.suffix_name ("_" ^ axiomsN) bname), []),
+ [([Assumption.assume (cterm_of thy' (the asm))],
+ [(Attrib.internal o K) Locale.witness_add])])])]
else [];
val notes' = body_elems |>
--- a/src/Pure/Isar/isar_cmd.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/Pure/Isar/isar_cmd.ML Thu Oct 29 16:22:14 2009 +0000
@@ -454,7 +454,7 @@
(case arg of
NONE =>
let
- val (ctxt, thm) = Proof.flat_goal state;
+ val {context = ctxt, goal = thm} = Proof.simple_goal state;
val thy = ProofContext.theory_of ctxt;
val prf = Thm.proof_of thm;
val prop = Thm.full_prop_of thm;
--- a/src/Pure/Isar/isar_syn.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/Pure/Isar/isar_syn.ML Thu Oct 29 16:22:14 2009 +0000
@@ -222,22 +222,13 @@
(* constant definitions and abbreviations *)
-val constdecl =
- P.binding --
- (P.where_ >> K (NONE, NoSyn) ||
- P.$$$ "::" |-- P.!!! ((P.typ >> SOME) -- P.opt_mixfix' --| P.where_) ||
- Scan.ahead (P.$$$ "(") |-- P.!!! (P.mixfix' --| P.where_ >> pair NONE))
- >> P.triple2;
-
-val constdef = Scan.option constdecl -- (SpecParse.opt_thm_name ":" -- P.prop);
-
val _ =
OuterSyntax.local_theory "definition" "constant definition" K.thy_decl
- (constdef >> (fn args => #2 o Specification.definition_cmd args));
+ (SpecParse.constdef >> (fn args => #2 o Specification.definition_cmd args));
val _ =
OuterSyntax.local_theory "abbreviation" "constant abbreviation" K.thy_decl
- (opt_mode -- (Scan.option constdecl -- P.prop)
+ (opt_mode -- (Scan.option SpecParse.constdecl -- P.prop)
>> (fn (mode, args) => Specification.abbreviation_cmd mode args));
val _ =
--- a/src/Pure/Isar/local_theory.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/Pure/Isar/local_theory.ML Thu Oct 29 16:22:14 2009 +0000
@@ -15,6 +15,7 @@
val map_naming: (Name_Space.naming -> Name_Space.naming) -> local_theory -> local_theory
val conceal: local_theory -> local_theory
val set_group: serial -> local_theory -> local_theory
+ val restore_naming: local_theory -> local_theory -> local_theory
val target_of: local_theory -> Proof.context
val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
val raw_theory: (theory -> theory) -> local_theory -> local_theory
@@ -24,6 +25,8 @@
val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
val map_contexts: (Context.generic -> Context.generic) -> local_theory -> local_theory
+ val standard_morphism: local_theory -> Proof.context -> morphism
+ val target_morphism: local_theory -> morphism
val pretty: local_theory -> Pretty.T list
val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
(term * term) * local_theory
@@ -36,7 +39,6 @@
val term_syntax: declaration -> local_theory -> local_theory
val declaration: declaration -> local_theory -> local_theory
val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
- val target_morphism: local_theory -> morphism
val init: string -> operations -> Proof.context -> local_theory
val restore: local_theory -> local_theory
val reinit: local_theory -> local_theory
@@ -111,6 +113,8 @@
val conceal = map_naming Name_Space.conceal;
val set_group = map_naming o Name_Space.set_group;
+val restore_naming = map_naming o K o naming_of;
+
(* target *)
@@ -163,6 +167,15 @@
Context.proof_map f;
+(* morphisms *)
+
+fun standard_morphism lthy ctxt =
+ ProofContext.norm_export_morphism lthy ctxt $>
+ Morphism.binding_morphism (Name_Space.transform_binding (naming_of lthy));
+
+fun target_morphism lthy = standard_morphism lthy (target_of lthy);
+
+
(* basic operations *)
fun operation f lthy = f (#operations (get_lthy lthy)) lthy;
@@ -179,9 +192,6 @@
fun note kind (a, ths) = notes kind [(a, [(ths, [])])] #>> the_single;
-fun target_morphism lthy =
- ProofContext.norm_export_morphism lthy (target_of lthy);
-
fun notation add mode raw_args lthy =
let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args
in term_syntax (ProofContext.target_notation add mode args) lthy end;
@@ -215,14 +225,14 @@
fun exit_result f (x, lthy) =
let
val ctxt = exit lthy;
- val phi = ProofContext.norm_export_morphism lthy ctxt;
+ val phi = standard_morphism lthy ctxt;
in (f phi x, ctxt) end;
fun exit_result_global f (x, lthy) =
let
val thy = exit_global lthy;
val thy_ctxt = ProofContext.init thy;
- val phi = ProofContext.norm_export_morphism lthy thy_ctxt;
+ val phi = standard_morphism lthy thy_ctxt;
in (f phi x, thy) end;
end;
--- a/src/Pure/Isar/locale.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/Pure/Isar/locale.ML Thu Oct 29 16:22:14 2009 +0000
@@ -553,7 +553,8 @@
fun add_decls add loc decl =
ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, stamp ()))) #>
add_thmss loc Thm.internalK
- [((Binding.empty, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
+ [((Binding.conceal Binding.empty, [Attrib.internal (decl_attrib decl)]),
+ [([Drule.dummy_thm], [])])];
in
--- a/src/Pure/Isar/proof.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/Pure/Isar/proof.ML Thu Oct 29 16:22:14 2009 +0000
@@ -29,7 +29,6 @@
val assert_no_chain: state -> state
val enter_forward: state -> state
val goal_message: (unit -> Pretty.T) -> state -> state
- val get_goal: state -> context * (thm list * thm)
val show_main_goal: bool Unsynchronized.ref
val verbose: bool Unsynchronized.ref
val pretty_state: int -> state -> Pretty.T list
@@ -37,9 +36,11 @@
val refine: Method.text -> state -> state Seq.seq
val refine_end: Method.text -> state -> state Seq.seq
val refine_insert: thm list -> state -> state
- val flat_goal: state -> Proof.context * thm
val goal_tac: thm -> int -> tactic
val refine_goals: (context -> thm -> unit) -> context -> thm list -> state -> state Seq.seq
+ val raw_goal: state -> {context: context, facts: thm list, goal: thm}
+ val goal: state -> {context: context, facts: thm list, goal: thm}
+ val simple_goal: state -> {context: context, goal: thm}
val match_bind: (string list * string) list -> state -> state
val match_bind_i: (term list * term) list -> state -> state
val let_bind: (string list * string) list -> state -> state
@@ -436,12 +437,6 @@
end;
-fun flat_goal state =
- let
- val (_, (using, _)) = get_goal state;
- val (ctxt, (_, goal)) = get_goal (refine_insert using state);
- in (ctxt, goal) end;
-
(* refine via sub-proof *)
@@ -508,6 +503,21 @@
in recover_result propss results end;
+(* goal views -- corresponding to methods *)
+
+fun raw_goal state =
+ let val (ctxt, (facts, goal)) = get_goal state
+ in {context = ctxt, facts = facts, goal = goal} end;
+
+val goal = raw_goal o refine_insert [];
+
+fun simple_goal state =
+ let
+ val (_, (facts, _)) = get_goal state;
+ val (ctxt, (_, goal)) = get_goal (refine_insert facts state);
+ in {context = ctxt, goal = goal} end;
+
+
(*** structured proof commands ***)
--- a/src/Pure/Isar/spec_parse.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/Pure/Isar/spec_parse.ML Thu Oct 29 16:22:14 2009 +0000
@@ -18,6 +18,8 @@
val xthm: (Facts.ref * Attrib.src list) parser
val xthms1: (Facts.ref * Attrib.src list) list parser
val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
+ val constdecl: (binding * string option * mixfix) parser
+ val constdef: ((binding * string option * mixfix) option * (Attrib.binding * string)) parser
val locale_mixfix: mixfix parser
val locale_fixes: (binding * string option * mixfix) list parser
val locale_insts: (string option list * (Attrib.binding * string) list) parser
@@ -66,6 +68,18 @@
val name_facts = P.and_list1 (opt_thm_name "=" -- xthms1);
+(* basic constant specifications *)
+
+val constdecl =
+ P.binding --
+ (P.where_ >> K (NONE, NoSyn) ||
+ P.$$$ "::" |-- P.!!! ((P.typ >> SOME) -- P.opt_mixfix' --| P.where_) ||
+ Scan.ahead (P.$$$ "(") |-- P.!!! (P.mixfix' --| P.where_ >> pair NONE))
+ >> P.triple2;
+
+val constdef = Scan.option constdecl -- (opt_thm_name ":" -- P.prop);
+
+
(* locale and context elements *)
val locale_mixfix = P.$$$ "(" -- P.$$$ "structure" -- P.!!! (P.$$$ ")") >> K Structure || P.mixfix;
--- a/src/Pure/Isar/theory_target.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/Pure/Isar/theory_target.ML Thu Oct 29 16:22:14 2009 +0000
@@ -181,9 +181,10 @@
val similar_body = Type.similar_types (rhs, rhs');
(* FIXME workaround based on educated guess *)
val prefix' = Binding.prefix_of b';
- val class_global = Binding.eq_name (b, b')
- andalso not (null prefix')
- andalso (fst o snd o split_last) prefix' = Class_Target.class_prefix target;
+ val class_global =
+ Binding.eq_name (b, b') andalso
+ not (null prefix') andalso
+ fst (snd (split_last prefix')) = Class_Target.class_prefix target;
in
not (is_class andalso (similar_body orelse class_global)) ?
(Context.mapping_result
@@ -202,7 +203,7 @@
val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
val U = map #2 xs ---> T;
val (mx1, mx2, mx3) = fork_mixfix ta mx;
- val declare_const =
+ val (const, lthy') = lthy |>
(case Class_Target.instantiation_param lthy b of
SOME c' =>
if mx3 <> NoSyn then syntax_error c'
@@ -215,7 +216,6 @@
else LocalTheory.theory_result (Overloading.declare (c', U))
##> Overloading.confirm b
| NONE => LocalTheory.theory_result (Sign.declare_const ((b, U), mx3))));
- val (const, lthy') = lthy |> declare_const;
val t = Term.list_comb (const, map Free xs);
in
lthy'
@@ -275,13 +275,13 @@
(*def*)
val (global_def, lthy3) = lthy2
- |> LocalTheory.theory_result (case Overloading.operation lthy b of
- SOME (_, checked) =>
- Overloading.define checked name' ((fst o dest_Const) lhs', rhs')
+ |> LocalTheory.theory_result
+ (case Overloading.operation lthy b of
+ SOME (_, checked) => Overloading.define checked name' (fst (dest_Const lhs'), rhs')
| NONE =>
if is_none (Class_Target.instantiation_param lthy b)
then Thm.add_def false false (name', Logic.mk_equals (lhs', rhs'))
- else AxClass.define_overloaded name' ((fst o dest_Const) lhs', rhs'));
+ else AxClass.define_overloaded name' (fst (dest_Const lhs'), rhs'));
val def = LocalDefs.trans_terms lthy3
[(*c == global.c xs*) local_def,
(*global.c xs == rhs'*) global_def,
@@ -341,6 +341,9 @@
fun context "-" thy = init NONE thy
| context target thy = init (SOME (Locale.intern thy target)) thy;
+
+(* other targets *)
+
fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []);
fun instantiation_cmd raw_arities thy =
instantiation (Class_Target.read_multi_arity thy raw_arities) thy;
--- a/src/Pure/System/isar.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/Pure/System/isar.ML Thu Oct 29 16:22:14 2009 +0000
@@ -10,7 +10,7 @@
val exn: unit -> (exn * string) option
val state: unit -> Toplevel.state
val context: unit -> Proof.context
- val goal: unit -> thm
+ val goal: unit -> {context: Proof.context, facts: thm list, goal: thm}
val print: unit -> unit
val >> : Toplevel.transition -> bool
val >>> : Toplevel.transition list -> unit
@@ -60,7 +60,7 @@
fun context () = Toplevel.context_of (state ())
handle Toplevel.UNDEF => error "Unknown context";
-fun goal () = #2 (#2 (Proof.get_goal (Toplevel.proof_of (state ()))))
+fun goal () = Proof.goal (Toplevel.proof_of (state ()))
handle Toplevel.UNDEF => error "No goal present";
fun print () = Toplevel.print_state false (state ());
--- a/src/Pure/Tools/find_theorems.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/Pure/Tools/find_theorems.ML Thu Oct 29 16:22:14 2009 +0000
@@ -456,7 +456,7 @@
let
val proof_state = Toplevel.enter_proof_body state;
val ctxt = Proof.context_of proof_state;
- val opt_goal = try Proof.flat_goal proof_state |> Option.map #2;
+ val opt_goal = try Proof.simple_goal proof_state |> Option.map #goal;
in print_theorems ctxt opt_goal opt_lim rem_dups spec end);
local
--- a/src/Pure/axclass.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/Pure/axclass.ML Thu Oct 29 16:22:14 2009 +0000
@@ -311,7 +311,7 @@
(Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
#>> Thm.varifyT
#-> (fn thm => add_inst_param (c, tyco) (c'', thm)
- #> PureThy.add_thm ((Binding.name c', thm), [Thm.kind_internal])
+ #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [Thm.kind_internal])
#> snd
#> Sign.restore_naming thy
#> pair (Const (c, T))))
--- a/src/Pure/conjunction.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/Pure/conjunction.ML Thu Oct 29 16:22:14 2009 +0000
@@ -83,15 +83,16 @@
in
-val conjunctionD1 = Drule.store_standard_thm "conjunctionD1" (conjunctionD #1);
-val conjunctionD2 = Drule.store_standard_thm "conjunctionD2" (conjunctionD #2);
+val conjunctionD1 = Drule.store_standard_thm (Binding.name "conjunctionD1") (conjunctionD #1);
+val conjunctionD2 = Drule.store_standard_thm (Binding.name "conjunctionD2") (conjunctionD #2);
-val conjunctionI = Drule.store_standard_thm "conjunctionI"
- (Drule.implies_intr_list [A, B]
- (Thm.equal_elim
- (Thm.symmetric conjunction_def)
- (Thm.forall_intr C (Thm.implies_intr ABC
- (Drule.implies_elim_list (Thm.assume ABC) [Thm.assume A, Thm.assume B])))));
+val conjunctionI =
+ Drule.store_standard_thm (Binding.name "conjunctionI")
+ (Drule.implies_intr_list [A, B]
+ (Thm.equal_elim
+ (Thm.symmetric conjunction_def)
+ (Thm.forall_intr C (Thm.implies_intr ABC
+ (Drule.implies_elim_list (Thm.assume ABC) [Thm.assume A, Thm.assume B])))));
fun intr tha thb =
--- a/src/Pure/drule.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/Pure/drule.ML Thu Oct 29 16:22:14 2009 +0000
@@ -78,10 +78,10 @@
val standard: thm -> thm
val standard': thm -> thm
val get_def: theory -> xstring -> thm
- val store_thm: bstring -> thm -> thm
- val store_standard_thm: bstring -> thm -> thm
- val store_thm_open: bstring -> thm -> thm
- val store_standard_thm_open: bstring -> thm -> thm
+ val store_thm: binding -> thm -> thm
+ val store_standard_thm: binding -> thm -> thm
+ val store_thm_open: binding -> thm -> thm
+ val store_standard_thm_open: binding -> thm -> thm
val compose_single: thm * int * thm -> thm
val imp_cong_rule: thm -> thm -> thm
val arg_cong_rule: cterm -> thm -> thm
@@ -455,27 +455,32 @@
fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name;
fun store_thm name th =
- Context.>>> (Context.map_theory_result (PureThy.store_thm (Binding.name name, th)));
+ Context.>>> (Context.map_theory_result (PureThy.store_thm (name, th)));
fun store_thm_open name th =
- Context.>>> (Context.map_theory_result (PureThy.store_thm_open (Binding.name name, th)));
+ Context.>>> (Context.map_theory_result (PureThy.store_thm_open (name, th)));
fun store_standard_thm name th = store_thm name (standard th);
fun store_standard_thm_open name thm = store_thm_open name (standard' thm);
val reflexive_thm =
let val cx = certify (Var(("x",0),TVar(("'a",0),[])))
- in store_standard_thm_open "reflexive" (Thm.reflexive cx) end;
+ in store_standard_thm_open (Binding.name "reflexive") (Thm.reflexive cx) end;
val symmetric_thm =
- let val xy = read_prop "x::'a == y::'a"
- in store_standard_thm_open "symmetric" (Thm.implies_intr xy (Thm.symmetric (Thm.assume xy))) end;
+ let
+ val xy = read_prop "x::'a == y::'a";
+ val thm = Thm.implies_intr xy (Thm.symmetric (Thm.assume xy));
+ in store_standard_thm_open (Binding.name "symmetric") thm end;
val transitive_thm =
- let val xy = read_prop "x::'a == y::'a"
- val yz = read_prop "y::'a == z::'a"
- val xythm = Thm.assume xy and yzthm = Thm.assume yz
- in store_standard_thm_open "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
+ let
+ val xy = read_prop "x::'a == y::'a";
+ val yz = read_prop "y::'a == z::'a";
+ val xythm = Thm.assume xy;
+ val yzthm = Thm.assume yz;
+ val thm = Thm.implies_intr yz (Thm.transitive xythm yzthm);
+ in store_standard_thm_open (Binding.name "transitive") thm end;
fun symmetric_fun thm = thm RS symmetric_thm;
@@ -485,7 +490,8 @@
in equal_elim (eta_conversion (cprop_of eq')) eq' end;
val equals_cong =
- store_standard_thm_open "equals_cong" (Thm.reflexive (read_prop "x::'a == y::'a"));
+ store_standard_thm_open (Binding.name "equals_cong")
+ (Thm.reflexive (read_prop "x::'a == y::'a"));
val imp_cong =
let
@@ -494,7 +500,7 @@
val AC = read_prop "A ==> C"
val A = read_prop "A"
in
- store_standard_thm_open "imp_cong" (implies_intr ABC (equal_intr
+ store_standard_thm_open (Binding.name "imp_cong") (implies_intr ABC (equal_intr
(implies_intr AB (implies_intr A
(equal_elim (implies_elim (assume ABC) (assume A))
(implies_elim (assume AB) (assume A)))))
@@ -510,11 +516,12 @@
val A = read_prop "A"
val B = read_prop "B"
in
- store_standard_thm_open "swap_prems_eq" (equal_intr
- (implies_intr ABC (implies_intr B (implies_intr A
- (implies_elim (implies_elim (assume ABC) (assume A)) (assume B)))))
- (implies_intr BAC (implies_intr A (implies_intr B
- (implies_elim (implies_elim (assume BAC) (assume B)) (assume A))))))
+ store_standard_thm_open (Binding.name "swap_prems_eq")
+ (equal_intr
+ (implies_intr ABC (implies_intr B (implies_intr A
+ (implies_elim (implies_elim (assume ABC) (assume A)) (assume B)))))
+ (implies_intr BAC (implies_intr A (implies_intr B
+ (implies_elim (implies_elim (assume BAC) (assume B)) (assume A))))))
end;
val imp_cong_rule = Thm.combination o Thm.combination (Thm.reflexive implies);
@@ -577,37 +584,41 @@
(*** Some useful meta-theorems ***)
(*The rule V/V, obtains assumption solving for eresolve_tac*)
-val asm_rl = store_standard_thm_open "asm_rl" (Thm.trivial (read_prop "?psi"));
-val _ = store_thm_open "_" asm_rl;
+val asm_rl = store_standard_thm_open (Binding.name "asm_rl") (Thm.trivial (read_prop "?psi"));
+val _ = store_thm_open (Binding.name "_") asm_rl;
(*Meta-level cut rule: [| V==>W; V |] ==> W *)
val cut_rl =
- store_standard_thm_open "cut_rl"
+ store_standard_thm_open (Binding.name "cut_rl")
(Thm.trivial (read_prop "?psi ==> ?theta"));
(*Generalized elim rule for one conclusion; cut_rl with reversed premises:
[| PROP V; PROP V ==> PROP W |] ==> PROP W *)
val revcut_rl =
- let val V = read_prop "V"
- and VW = read_prop "V ==> W";
+ let
+ val V = read_prop "V";
+ val VW = read_prop "V ==> W";
in
- store_standard_thm_open "revcut_rl"
+ store_standard_thm_open (Binding.name "revcut_rl")
(implies_intr V (implies_intr VW (implies_elim (assume VW) (assume V))))
end;
(*for deleting an unwanted assumption*)
val thin_rl =
- let val V = read_prop "V"
- and W = read_prop "W";
- in store_standard_thm_open "thin_rl" (implies_intr V (implies_intr W (assume W))) end;
+ let
+ val V = read_prop "V";
+ val W = read_prop "W";
+ val thm = implies_intr V (implies_intr W (assume W));
+ in store_standard_thm_open (Binding.name "thin_rl") thm end;
(* (!!x. PROP ?V) == PROP ?V Allows removal of redundant parameters*)
val triv_forall_equality =
- let val V = read_prop "V"
- and QV = read_prop "!!x::'a. V"
- and x = certify (Free ("x", Term.aT []));
+ let
+ val V = read_prop "V";
+ val QV = read_prop "!!x::'a. V";
+ val x = certify (Free ("x", Term.aT []));
in
- store_standard_thm_open "triv_forall_equality"
+ store_standard_thm_open (Binding.name "triv_forall_equality")
(equal_intr (implies_intr QV (forall_elim x (assume QV)))
(implies_intr V (forall_intr x (assume V))))
end;
@@ -617,10 +628,10 @@
*)
val distinct_prems_rl =
let
- val AAB = read_prop "Phi ==> Phi ==> Psi"
+ val AAB = read_prop "Phi ==> Phi ==> Psi";
val A = read_prop "Phi";
in
- store_standard_thm_open "distinct_prems_rl"
+ store_standard_thm_open (Binding.name "distinct_prems_rl")
(implies_intr_list [AAB, A] (implies_elim_list (assume AAB) [assume A, assume A]))
end;
@@ -629,15 +640,17 @@
`thm COMP swap_prems_rl' swaps the first two premises of `thm'
*)
val swap_prems_rl =
- let val cmajor = read_prop "PhiA ==> PhiB ==> Psi";
- val major = assume cmajor;
- val cminor1 = read_prop "PhiA";
- val minor1 = assume cminor1;
- val cminor2 = read_prop "PhiB";
- val minor2 = assume cminor2;
- in store_standard_thm_open "swap_prems_rl"
- (implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1
- (implies_elim (implies_elim major minor1) minor2))))
+ let
+ val cmajor = read_prop "PhiA ==> PhiB ==> Psi";
+ val major = assume cmajor;
+ val cminor1 = read_prop "PhiA";
+ val minor1 = assume cminor1;
+ val cminor2 = read_prop "PhiB";
+ val minor2 = assume cminor2;
+ in
+ store_standard_thm_open (Binding.name "swap_prems_rl")
+ (implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1
+ (implies_elim (implies_elim major minor1) minor2))))
end;
(* [| PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi |]
@@ -645,29 +658,36 @@
Introduction rule for == as a meta-theorem.
*)
val equal_intr_rule =
- let val PQ = read_prop "phi ==> psi"
- and QP = read_prop "psi ==> phi"
+ let
+ val PQ = read_prop "phi ==> psi";
+ val QP = read_prop "psi ==> phi";
in
- store_standard_thm_open "equal_intr_rule"
+ store_standard_thm_open (Binding.name "equal_intr_rule")
(implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP))))
end;
(* PROP ?phi == PROP ?psi ==> PROP ?phi ==> PROP ?psi *)
val equal_elim_rule1 =
- let val eq = read_prop "phi::prop == psi::prop"
- and P = read_prop "phi"
- in store_standard_thm_open "equal_elim_rule1"
- (Thm.equal_elim (assume eq) (assume P) |> implies_intr_list [eq, P])
+ let
+ val eq = read_prop "phi::prop == psi::prop";
+ val P = read_prop "phi";
+ in
+ store_standard_thm_open (Binding.name "equal_elim_rule1")
+ (Thm.equal_elim (assume eq) (assume P) |> implies_intr_list [eq, P])
end;
(* PROP ?psi == PROP ?phi ==> PROP ?phi ==> PROP ?psi *)
val equal_elim_rule2 =
- store_standard_thm_open "equal_elim_rule2" (symmetric_thm RS equal_elim_rule1);
+ store_standard_thm_open (Binding.name "equal_elim_rule2")
+ (symmetric_thm RS equal_elim_rule1);
(* PROP ?phi ==> PROP ?phi ==> PROP ?psi ==> PROP ?psi *)
val remdups_rl =
- let val P = read_prop "phi" and Q = read_prop "psi";
- in store_standard_thm_open "remdups_rl" (implies_intr_list [P, P, Q] (Thm.assume Q)) end;
+ let
+ val P = read_prop "phi";
+ val Q = read_prop "psi";
+ val thm = implies_intr_list [P, P, Q] (Thm.assume Q);
+ in store_standard_thm_open (Binding.name "remdups_rl") thm end;
@@ -688,13 +708,18 @@
val protect = Thm.capply (certify Logic.protectC);
-val protectI = store_thm "protectI" (Thm.kind_rule Thm.internalK (standard
- (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A))));
+val protectI =
+ store_thm (Binding.conceal (Binding.name "protectI"))
+ (Thm.kind_rule Thm.internalK (standard
+ (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A))));
-val protectD = store_thm "protectD" (Thm.kind_rule Thm.internalK (standard
- (Thm.equal_elim prop_def (Thm.assume (protect A)))));
+val protectD =
+ store_thm (Binding.conceal (Binding.name "protectD"))
+ (Thm.kind_rule Thm.internalK (standard
+ (Thm.equal_elim prop_def (Thm.assume (protect A)))));
-val protect_cong = store_standard_thm_open "protect_cong" (Thm.reflexive (protect A));
+val protect_cong =
+ store_standard_thm_open (Binding.name "protect_cong") (Thm.reflexive (protect A));
fun implies_intr_protected asms th =
let val asms' = map protect asms in
@@ -707,8 +732,10 @@
(* term *)
-val termI = store_thm "termI" (Thm.kind_rule Thm.internalK (standard
- (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A)))));
+val termI =
+ store_thm (Binding.conceal (Binding.name "termI"))
+ (Thm.kind_rule Thm.internalK (standard
+ (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A)))));
fun mk_term ct =
let
@@ -735,13 +762,17 @@
(* sort_constraint *)
-val sort_constraintI = store_thm "sort_constraintI" (Thm.kind_rule Thm.internalK (standard
- (Thm.equal_elim (Thm.symmetric sort_constraint_def) (mk_term T))));
+val sort_constraintI =
+ store_thm (Binding.conceal (Binding.name "sort_constraintI"))
+ (Thm.kind_rule Thm.internalK (standard
+ (Thm.equal_elim (Thm.symmetric sort_constraint_def) (mk_term T))));
-val sort_constraint_eq = store_thm "sort_constraint_eq" (Thm.kind_rule Thm.internalK (standard
- (Thm.equal_intr
- (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA) (Thm.unvarify sort_constraintI)))
- (implies_intr_list [A, C] (Thm.assume A)))));
+val sort_constraint_eq =
+ store_thm (Binding.conceal (Binding.name "sort_constraint_eq"))
+ (Thm.kind_rule Thm.internalK (standard
+ (Thm.equal_intr
+ (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA) (Thm.unvarify sort_constraintI)))
+ (implies_intr_list [A, C] (Thm.assume A)))));
end;
@@ -773,7 +804,7 @@
|> Thm.forall_intr cx
|> Thm.implies_intr cphi
|> Thm.implies_intr rhs)
- |> store_standard_thm_open "norm_hhf_eq"
+ |> store_standard_thm_open (Binding.name "norm_hhf_eq")
end;
val norm_hhf_prop = Logic.dest_equals (Thm.prop_of norm_hhf_eq);
--- a/src/Tools/auto_solve.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/Tools/auto_solve.ML Thu Oct 29 16:22:14 2009 +0000
@@ -61,9 +61,9 @@
end;
fun seek_against_goal () =
- (case try Proof.flat_goal state of
+ (case try Proof.simple_goal state of
NONE => NONE
- | SOME (_, st) =>
+ | SOME {goal = st, ...} =>
let
val subgoals = Drule.strip_imp_prems (Thm.cprop_of st);
val rs =
--- a/src/Tools/quickcheck.ML Thu Oct 29 16:21:43 2009 +0000
+++ b/src/Tools/quickcheck.ML Thu Oct 29 16:22:14 2009 +0000
@@ -143,7 +143,7 @@
val thy = Proof.theory_of state;
fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t
| strip t = t;
- val (_, st) = Proof.flat_goal state;
+ val {goal = st, ...} = Proof.raw_goal state;
val (gi, frees) = Logic.goal_params (prop_of st) i;
val gi' = Logic.list_implies (assms, subst_bounds (frees, strip gi))
|> monomorphic_term thy insts default_T