--- a/CONTRIBUTORS Wed Sep 07 08:13:38 2011 +0200
+++ b/CONTRIBUTORS Thu Sep 08 00:35:22 2011 +0200
@@ -6,6 +6,12 @@
Contributions to this Isabelle version
--------------------------------------
+* September 2011: Peter Gammie
+ Theory HOL/Libary/Saturated: numbers with saturated arithmetic.
+
+* August 2011: Florian Haftmann, Johannes Hölzl and Lars Noschinski, TUM
+ Refined theory on complete lattices.
+
Contributions to Isabelle2011
-----------------------------
--- a/NEWS Wed Sep 07 08:13:38 2011 +0200
+++ b/NEWS Thu Sep 08 00:35:22 2011 +0200
@@ -9,27 +9,38 @@
* Improved Isabelle/jEdit Prover IDE (PIDE), which can be invoked as
"isabelle jedit" on the command line.
- . Management of multiple theory files directly from the editor
+ - Management of multiple theory files directly from the editor
buffer store -- bypassing the file-system (no requirement to save
files for checking).
- . Markup of formal entities within the text buffer, with semantic
+ - Markup of formal entities within the text buffer, with semantic
highlighting, tooltips and hyperlinks to jump to defining source
positions.
- . Refined scheduling of proof checking and printing of results,
+ - Improved text rendering, with sub/superscripts in the source
+ buffer (including support for copy/paste wrt. output panel, HTML
+ theory output and other non-Isabelle text boxes).
+
+ - Refined scheduling of proof checking and printing of results,
based on interactive editor view. (Note: jEdit folding and
narrowing allows to restrict buffer perspectives explicitly.)
- . Reduced CPU performance requirements, usable on machines with few
+ - Reduced CPU performance requirements, usable on machines with few
cores.
- . Reduced memory requirements due to pruning of unused document
+ - Reduced memory requirements due to pruning of unused document
versions (garbage collection).
See also ~~/src/Tools/jEdit/README.html for further information,
including some remaining limitations.
+* Theory loader: source files are exclusively located via the master
+directory of each theory node (where the .thy file itself resides).
+The global load path (such as src/HOL/Library) has been discontinued.
+Note that the path element ~~ may be used to reference theories in the
+Isabelle home folder -- for instance, "~~/src/HOL/Library/FuncSet".
+INCOMPATIBILITY.
+
* Theory loader: source files are identified by content via SHA1
digests. Discontinued former path/modtime identification and optional
ISABELLE_FILE_IDENT plugin scripts.
@@ -44,13 +55,6 @@
* Discontinued old lib/scripts/polyml-platform, which has been
obsolete since Isabelle2009-2.
-* Theory loader: source files are exclusively located via the master
-directory of each theory node (where the .thy file itself resides).
-The global load path (such as src/HOL/Library) has been discontinued.
-Note that the path element ~~ may be used to reference theories in the
-Isabelle home folder -- for instance, "~~/src/HOL/Library/FuncSet".
-INCOMPATIBILITY.
-
* Various optional external tools are referenced more robustly and
uniformly by explicit Isabelle settings as follows:
@@ -78,29 +82,38 @@
that the result needs to be unique, which means fact specifications
may have to be refined after enriching a proof context.
+* Attribute "case_names" has been refined: the assumptions in each case
+can be named now by following the case name with [name1 name2 ...].
+
* Isabelle/Isar reference manual provides more formal references in
syntax diagrams.
-* Attribute case_names has been refined: the assumptions in each case can
-be named now by following the case name with [name1 name2 ...].
-
*** HOL ***
-* Classes bot and top require underlying partial order rather than preorder:
-uniqueness of bot and top is guaranteed. INCOMPATIBILITY.
+* Theory Library/Saturated provides type of numbers with saturated
+arithmetic.
+
+* Classes bot and top require underlying partial order rather than
+preorder: uniqueness of bot and top is guaranteed. INCOMPATIBILITY.
* Class complete_lattice: generalized a couple of lemmas from sets;
-generalized theorems INF_cong and SUP_cong. New type classes for complete
-boolean algebras and complete linear orders. Lemmas Inf_less_iff,
-less_Sup_iff, INF_less_iff, less_SUP_iff now reside in class complete_linorder.
-Changed proposition of lemmas Inf_bool_def, Sup_bool_def, Inf_fun_def, Sup_fun_def,
-Inf_apply, Sup_apply.
+generalized theorems INF_cong and SUP_cong. New type classes for
+complete boolean algebras and complete linear orders. Lemmas
+Inf_less_iff, less_Sup_iff, INF_less_iff, less_SUP_iff now reside in
+class complete_linorder.
+
+Changed proposition of lemmas Inf_bool_def, Sup_bool_def, Inf_fun_def,
+Sup_fun_def, Inf_apply, Sup_apply.
+
Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary, Sup_binary,
INF_eq, SUP_eq, INF_UNIV_range, SUP_UNIV_range, Int_eq_Inter,
-INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union, UNION_eq_Union_image,
-Union_def, UN_singleton, UN_eq have been discarded.
-More consistent and less misunderstandable names:
+INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union,
+UNION_eq_Union_image, Union_def, UN_singleton, UN_eq have been
+discarded.
+
+More consistent and comprehensive names:
+
INFI_def ~> INF_def
SUPR_def ~> SUP_def
INF_leI ~> INF_lower
@@ -118,30 +131,35 @@
INCOMPATIBILITY.
-* Theorem collections ball_simps and bex_simps do not contain theorems referring
-to UNION any longer; these have been moved to collection UN_ball_bex_simps.
-INCOMPATIBILITY.
-
-* Archimedean_Field.thy:
- floor now is defined as parameter of a separate type class floor_ceiling.
-
-* Finite_Set.thy: more coherent development of fold_set locales:
+* Theorem collections ball_simps and bex_simps do not contain theorems
+referring to UNION any longer; these have been moved to collection
+UN_ball_bex_simps. INCOMPATIBILITY.
+
+* Theory Archimedean_Field: floor now is defined as parameter of a
+separate type class floor_ceiling.
+
+* Theory Finite_Set: more coherent development of fold_set locales:
locale fun_left_comm ~> locale comp_fun_commute
locale fun_left_comm_idem ~> locale comp_fun_idem
-
-Both use point-free characterisation; interpretation proofs may need adjustment.
-INCOMPATIBILITY.
+
+Both use point-free characterization; interpretation proofs may need
+adjustment. INCOMPATIBILITY.
* Code generation:
- - theory Library/Code_Char_ord provides native ordering of characters
- in the target language.
- - commands code_module and code_library are legacy, use export_code instead.
- - method evaluation is legacy, use method eval instead.
- - legacy evaluator "SML" is deactivated by default. To activate it, add the following
- line in your theory:
+
+ - Theory Library/Code_Char_ord provides native ordering of
+ characters in the target language.
+
+ - Commands code_module and code_library are legacy, use export_code instead.
+
+ - Method "evaluation" is legacy, use method "eval" instead.
+
+ - Legacy evaluator "SML" is deactivated by default. May be
+ reactivated by the following theory command:
+
setup {* Value.add_evaluator ("SML", Codegen.eval_term) *}
-
+
* Declare ext [intro] by default. Rare INCOMPATIBILITY.
* Nitpick:
@@ -164,51 +182,57 @@
- Removed "metisF" -- use "metis" instead. INCOMPATIBILITY.
- Obsoleted "metisFT" -- use "metis (full_types)" instead. INCOMPATIBILITY.
-* "try":
- - Renamed "try_methods" and added "simp:", "intro:", "dest:", and "elim:"
- options. INCOMPATIBILITY.
- - Introduced "try" that not only runs "try_methods" but also "solve_direct",
- "sledgehammer", "quickcheck", and "nitpick".
+* Command 'try':
+ - Renamed 'try_methods' and added "simp:", "intro:", "dest:", and
+ "elim:" options. INCOMPATIBILITY.
+ - Introduced 'tryÄ that not only runs 'try_methods' but also
+ 'solve_direct', 'sledgehammer', 'quickcheck', and 'nitpick'.
* Quickcheck:
+
- Added "eval" option to evaluate terms for the found counterexample
- (currently only supported by the default (exhaustive) tester)
+ (currently only supported by the default (exhaustive) tester).
+
- Added post-processing of terms to obtain readable counterexamples
- (currently only supported by the default (exhaustive) tester)
+ (currently only supported by the default (exhaustive) tester).
+
- New counterexample generator quickcheck[narrowing] enables
- narrowing-based testing.
- It requires that the Glasgow Haskell compiler is installed and
- its location is known to Isabelle with the environment variable
- ISABELLE_GHC.
+ narrowing-based testing. Requires the Glasgow Haskell compiler
+ with its installation location defined in the Isabelle settings
+ environment as ISABELLE_GHC.
+
- Removed quickcheck tester "SML" based on the SML code generator
- from HOL-Library
+ (formly in HOL/Library).
* Function package: discontinued option "tailrec".
-INCOMPATIBILITY. Use partial_function instead.
-
-* HOL-Probability:
+INCOMPATIBILITY. Use 'partial_function' instead.
+
+* Session HOL-Probability:
- Caratheodory's extension lemma is now proved for ring_of_sets.
- Infinite products of probability measures are now available.
- - Use extended reals instead of positive extended reals.
- INCOMPATIBILITY.
-
-* Old recdef package has been moved to Library/Old_Recdef.thy, where it
-must be loaded explicitly. INCOMPATIBILITY.
-
-* Well-founded recursion combinator "wfrec" has been moved to
-Library/Wfrec.thy. INCOMPATIBILITY.
-
-* Theory Library/Nat_Infinity has been renamed to Library/Extended_Nat.
-The names of the following types and constants have changed:
- inat (type) ~> enat
+ - Use extended reals instead of positive extended
+ reals. INCOMPATIBILITY.
+
+* Old 'recdef' package has been moved to theory Library/Old_Recdef,
+from where it must be imported explicitly. INCOMPATIBILITY.
+
+* Well-founded recursion combinator "wfrec" has been moved to theory
+Library/Wfrec. INCOMPATIBILITY.
+
+* Theory Library/Nat_Infinity has been renamed to
+Library/Extended_Nat, with name changes of the following types and
+constants:
+
+ type inat ~> type enat
Fin ~> enat
Infty ~> infinity (overloaded)
iSuc ~> eSuc
the_Fin ~> the_enat
+
Every theorem name containing "inat", "Fin", "Infty", or "iSuc" has
been renamed accordingly.
-* Limits.thy: Type "'a net" has been renamed to "'a filter", in
+* Theory Limits: Type "'a net" has been renamed to "'a filter", in
accordance with standard mathematical terminology. INCOMPATIBILITY.
* Session Multivariate_Analysis: Type "('a, 'b) cart" has been renamed
@@ -279,10 +303,10 @@
real_abs_sub_norm ~> norm_triangle_ineq3
norm_cauchy_schwarz_abs ~> Cauchy_Schwarz_ineq2
-* Complex_Main: The locale interpretations for the bounded_linear and
-bounded_bilinear locales have been removed, in order to reduce the
-number of duplicate lemmas. Users must use the original names for
-distributivity theorems, potential INCOMPATIBILITY.
+* Theory Complex_Main: The locale interpretations for the
+bounded_linear and bounded_bilinear locales have been removed, in
+order to reduce the number of duplicate lemmas. Users must use the
+original names for distributivity theorems, potential INCOMPATIBILITY.
divide.add ~> add_divide_distrib
divide.diff ~> diff_divide_distrib
@@ -292,7 +316,7 @@
mult_right.setsum ~> setsum_right_distrib
mult_left.diff ~> left_diff_distrib
-* Complex_Main: Several redundant theorems have been removed or
+* Theory Complex_Main: Several redundant theorems have been removed or
replaced by more general versions. INCOMPATIBILITY.
real_0_le_divide_iff ~> zero_le_divide_iff
@@ -360,26 +384,30 @@
*** Document preparation ***
-* Discontinued special treatment of hard tabulators, which are better
-avoided in the first place. Implicit tab-width is 1.
-
-* Antiquotation @{rail} layouts railroad syntax diagrams, see also
-isar-ref manual.
-
-* Antiquotation @{value} evaluates the given term and presents its result.
-
* Localized \isabellestyle switch can be used within blocks or groups
like this:
\isabellestyle{it} %preferred default
{\isabellestylett @{text "typewriter stuff"}}
-* New term style "isub" as ad-hoc conversion of variables x1, y23 into
-subscripted form x\<^isub>1, y\<^isub>2\<^isub>3.
+* Antiquotation @{rail} layouts railroad syntax diagrams, see also
+isar-ref manual, both for description and actual application of the
+same.
+
+* Antiquotation @{value} evaluates the given term and presents its
+result.
+
+* Antiquotations: term style "isub" provides ad-hoc conversion of
+variables x1, y23 into subscripted form x\<^isub>1,
+y\<^isub>2\<^isub>3.
* Predefined LaTeX macros for Isabelle symbols \<bind> and \<then>
(e.g. see ~~/src/HOL/Library/Monad_Syntax.thy).
+* Discontinued special treatment of hard tabulators, which are better
+avoided in the first place (no universally agreed standard expansion).
+Implicit tab-width is now 1.
+
*** ML ***
@@ -439,11 +467,14 @@
proper Proof.context.
* Scala layer provides JVM method invocation service for static
-methods of type (String)String, see Invoke_Scala.method in ML.
-For example:
+methods of type (String)String, see Invoke_Scala.method in ML. For
+example:
Invoke_Scala.method "java.lang.System.getProperty" "java.home"
+Togeter with YXML.string_of_body/parse_body and XML.Encode/Decode this
+allows to pass structured values between ML and Scala.
+
New in Isabelle2011 (January 2011)
--- a/doc-src/Sledgehammer/sledgehammer.tex Wed Sep 07 08:13:38 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Thu Sep 08 00:35:22 2011 +0200
@@ -883,13 +883,7 @@
Specifies the type encoding to use in ATP problems. Some of the type encodings
are unsound, meaning that they can give rise to spurious proofs
(unreconstructible using Metis). The supported type encodings are listed below,
-with an indication of their soundness in parentheses.
-%
-All the encodings with \textit{guards} or \textit{tags} in their name are
-available in a ``uniform'' and a ``nonuniform'' variant. The nonuniform variants
-are generally more efficient and are the default; the uniform variants are
-identified by the suffix \textit{\_uniform} (e.g.,
-\textit{mono\_guards\_uniform}{?}).
+with an indication of their soundness in parentheses:
\begin{enum}
\item[$\bullet$] \textbf{\textit{erased} (very unsound):} No type information is
@@ -933,12 +927,11 @@
\item[$\bullet$] \textbf{\textit{mono\_simple} (sound):} Exploits simple
first-order types if the prover supports the TFF0 or THF0 syntax; otherwise,
-falls back on \textit{mono\_guards\_uniform}. The problem is monomorphized.
+falls back on \textit{mono\_guards}. The problem is monomorphized.
\item[$\bullet$] \textbf{\textit{mono\_simple\_higher} (sound):} Exploits simple
higher-order types if the prover supports the THF0 syntax; otherwise, falls back
-on \textit{mono\_simple} or \textit{mono\_guards\_uniform}. The problem is
-monomorphized.
+on \textit{mono\_simple} or \textit{mono\_guards}. The problem is monomorphized.
\item[$\bullet$]
\textbf{%
@@ -949,12 +942,29 @@
\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
\textit{mono\_tags}, and \textit{mono\_simple} are fully
typed and sound. For each of these, Sledgehammer also provides a lighter,
-virtually sound variant identified by a question mark (`{?}')\ that detects and
-erases monotonic types, notably infinite types. (For \textit{mono\_simple}, the
-types are not actually erased but rather replaced by a shared uniform type of
-individuals.) As argument to the \textit{metis} proof method, the question mark
-is replaced by a \hbox{``\textit{\_query}''} suffix. If the \emph{sound} option
-is enabled, these encodings are fully sound.
+virtually sound variant identified by a question mark (`\hbox{?}')\ that detects
+and erases monotonic types, notably infinite types. (For \textit{mono\_simple},
+the types are not actually erased but rather replaced by a shared uniform type
+of individuals.) As argument to the \textit{metis} proof method, the question
+mark is replaced by a \hbox{``\textit{\_query}''} suffix. If the \emph{sound}
+option is enabled, these encodings are fully sound.
+
+\item[$\bullet$]
+\textbf{%
+\textit{poly\_guards}??, \textit{poly\_tags}??, \textit{raw\_mono\_guards}??, \\
+\textit{raw\_mono\_tags}??, \textit{mono\_guards}??, \textit{mono\_tags}?? \\
+(quasi-sound):} \\
+Even lighter versions of the `\hbox{?}' encodings. As argument to the
+\textit{metis} proof method, the `\hbox{??}' suffix is replaced by
+\hbox{``\textit{\_query\_query}''}.
+
+\item[$\bullet$]
+\textbf{%
+\textit{poly\_guards}@?, \textit{poly\_tags}@?, \textit{raw\_mono\_guards}@?, \\
+\textit{raw\_mono\_tags}@? (quasi-sound):} \\
+Alternative versions of the `\hbox{??}' encodings. As argument to the
+\textit{metis} proof method, the `\hbox{@?}' suffix is replaced by
+\hbox{``\textit{\_at\_query}''}.
\item[$\bullet$]
\textbf{%
@@ -965,13 +975,30 @@
\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
\textit{mono\_tags}, \textit{mono\_simple}, and \textit{mono\_simple\_higher}
also admit a mildly unsound (but very efficient) variant identified by an
-exclamation mark (`{!}') that detects and erases erases all types except those
-that are clearly finite (e.g., \textit{bool}). (For \textit{mono\_simple} and
-\textit{mono\_simple\_higher}, the types are not actually erased but rather
+exclamation mark (`\hbox{!}') that detects and erases erases all types except
+those that are clearly finite (e.g., \textit{bool}). (For \textit{mono\_simple}
+and \textit{mono\_simple\_higher}, the types are not actually erased but rather
replaced by a shared uniform type of individuals.) As argument to the
\textit{metis} proof method, the exclamation mark is replaced by the suffix
\hbox{``\textit{\_bang}''}.
+\item[$\bullet$]
+\textbf{%
+\textit{poly\_guards}!!, \textit{poly\_tags}!!, \textit{raw\_mono\_guards}!!, \\
+\textit{raw\_mono\_tags}!!, \textit{mono\_guards}!!, \textit{mono\_tags}!! \\
+(mildly unsound):} \\
+Even lighter versions of the `\hbox{!}' encodings. As argument to the
+\textit{metis} proof method, the `\hbox{!!}' suffix is replaced by
+\hbox{``\textit{\_bang\_bang}''}.
+
+\item[$\bullet$]
+\textbf{%
+\textit{poly\_guards}@!, \textit{poly\_tags}@!, \textit{raw\_mono\_guards}@!, \\
+\textit{raw\_mono\_tags}@! (mildly unsound):} \\
+Alternative versions of the `\hbox{!!}' encodings. As argument to the
+\textit{metis} proof method, the `\hbox{@!}' suffix is replaced by
+\hbox{``\textit{\_at\_bang}''}.
+
\item[$\bullet$] \textbf{\textit{smart}:} The actual encoding used depends on
the ATP and should be the most efficient virtually sound encoding for that ATP.
\end{enum}
--- a/doc-src/System/Thy/Misc.thy Wed Sep 07 08:13:38 2011 +0200
+++ b/doc-src/System/Thy/Misc.thy Thu Sep 08 00:35:22 2011 +0200
@@ -336,8 +336,8 @@
sub-chunks separated by @{text "\<^bold>Y"}. Markup chunks start
with an empty sub-chunk, and a second empty sub-chunk indicates
close of an element. Any other non-empty chunk consists of plain
- text. For example, see @{file "~~/src/Pure/General/yxml.ML"} or
- @{file "~~/src/Pure/General/yxml.scala"}.
+ text. For example, see @{file "~~/src/Pure/PIDE/yxml.ML"} or
+ @{file "~~/src/Pure/PIDE/yxml.scala"}.
YXML documents may be detected quickly by checking that the first
two characters are @{text "\<^bold>X\<^bold>Y"}.
--- a/doc-src/System/Thy/document/Misc.tex Wed Sep 07 08:13:38 2011 +0200
+++ b/doc-src/System/Thy/document/Misc.tex Thu Sep 08 00:35:22 2011 +0200
@@ -376,8 +376,8 @@
sub-chunks separated by \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}}. Markup chunks start
with an empty sub-chunk, and a second empty sub-chunk indicates
close of an element. Any other non-empty chunk consists of plain
- text. For example, see \verb|~~/src/Pure/General/yxml.ML| or
- \verb|~~/src/Pure/General/yxml.scala|.
+ text. For example, see \verb|~~/src/Pure/PIDE/yxml.ML| or
+ \verb|~~/src/Pure/PIDE/yxml.scala|.
YXML documents may be detected quickly by checking that the first
two characters are \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}}.%
--- a/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy Wed Sep 07 08:13:38 2011 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy Thu Sep 08 00:35:22 2011 +0200
@@ -12,8 +12,7 @@
begin
text {* Formalization of normal form *}
-fun
- isnorm :: "('a::{comm_ring}) pol \<Rightarrow> bool"
+fun isnorm :: "'a::comm_ring pol \<Rightarrow> bool"
where
"isnorm (Pc c) \<longleftrightarrow> True"
| "isnorm (Pinj i (Pc c)) \<longleftrightarrow> False"
@@ -26,35 +25,40 @@
| "isnorm (PX P i Q) \<longleftrightarrow> isnorm P \<and> isnorm Q"
(* Some helpful lemmas *)
-lemma norm_Pinj_0_False:"isnorm (Pinj 0 P) = False"
-by(cases P, auto)
+lemma norm_Pinj_0_False: "isnorm (Pinj 0 P) = False"
+ by (cases P) auto
-lemma norm_PX_0_False:"isnorm (PX (Pc 0) i Q) = False"
-by(cases i, auto)
+lemma norm_PX_0_False: "isnorm (PX (Pc 0) i Q) = False"
+ by (cases i) auto
-lemma norm_Pinj:"isnorm (Pinj i Q) \<Longrightarrow> isnorm Q"
-by(cases i,simp add: norm_Pinj_0_False norm_PX_0_False,cases Q) auto
+lemma norm_Pinj: "isnorm (Pinj i Q) \<Longrightarrow> isnorm Q"
+ by (cases i) (simp add: norm_Pinj_0_False norm_PX_0_False, cases Q, auto)
-lemma norm_PX2:"isnorm (PX P i Q) \<Longrightarrow> isnorm Q"
-by(cases i, auto, cases P, auto, case_tac pol2, auto)
+lemma norm_PX2: "isnorm (PX P i Q) \<Longrightarrow> isnorm Q"
+ by (cases i) (auto, cases P, auto, case_tac pol2, auto)
+
+lemma norm_PX1: "isnorm (PX P i Q) \<Longrightarrow> isnorm P"
+ by (cases i) (auto, cases P, auto, case_tac pol2, auto)
-lemma norm_PX1:"isnorm (PX P i Q) \<Longrightarrow> isnorm P"
-by(cases i, auto, cases P, auto, case_tac pol2, auto)
-
-lemma mkPinj_cn:"\<lbrakk>y~=0; isnorm Q\<rbrakk> \<Longrightarrow> isnorm (mkPinj y Q)"
-apply(auto simp add: mkPinj_def norm_Pinj_0_False split: pol.split)
-apply(case_tac nat, auto simp add: norm_Pinj_0_False)
-by(case_tac pol, auto) (case_tac y, auto)
+lemma mkPinj_cn: "y ~= 0 \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (mkPinj y Q)"
+ apply (auto simp add: mkPinj_def norm_Pinj_0_False split: pol.split)
+ apply (case_tac nat, auto simp add: norm_Pinj_0_False)
+ apply (case_tac pol, auto)
+ apply (case_tac y, auto)
+ done
lemma norm_PXtrans:
- assumes A:"isnorm (PX P x Q)" and "isnorm Q2"
+ assumes A: "isnorm (PX P x Q)" and "isnorm Q2"
shows "isnorm (PX P x Q2)"
-proof(cases P)
- case (PX p1 y p2) with assms show ?thesis by(cases x, auto, cases p2, auto)
+proof (cases P)
+ case (PX p1 y p2)
+ with assms show ?thesis by (cases x) (auto, cases p2, auto)
next
- case Pc with assms show ?thesis by (cases x) auto
+ case Pc
+ with assms show ?thesis by (cases x) auto
next
- case Pinj with assms show ?thesis by (cases x) auto
+ case Pinj
+ with assms show ?thesis by (cases x) auto
qed
lemma norm_PXtrans2:
@@ -62,7 +66,7 @@
shows "isnorm (PX P (Suc (n+x)) Q2)"
proof (cases P)
case (PX p1 y p2)
- with assms show ?thesis by (cases x, auto, cases p2, auto)
+ with assms show ?thesis by (cases x) (auto, cases p2, auto)
next
case Pc
with assms show ?thesis by (cases x) auto
@@ -83,27 +87,33 @@
with assms show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def)
next
case (PX P1 y P2)
- with assms have Y0: "y>0" by (cases y) auto
+ with assms have Y0: "y > 0" by (cases y) auto
from assms PX have "isnorm P1" "isnorm P2"
by (auto simp add: norm_PX1[of P1 y P2] norm_PX2[of P1 y P2])
from assms PX Y0 show ?thesis
- by (cases x, auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _], cases P2, auto)
+ by (cases x) (auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _], cases P2, auto)
qed
text {* add conserves normalizedness *}
-lemma add_cn:"isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<oplus> Q)"
-proof(induct P Q rule: add.induct)
- case (2 c i P2) thus ?case by (cases P2, simp_all, cases i, simp_all)
+lemma add_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<oplus> Q)"
+proof (induct P Q rule: add.induct)
+ case (2 c i P2)
+ thus ?case by (cases P2) (simp_all, cases i, simp_all)
next
- case (3 i P2 c) thus ?case by (cases P2, simp_all, cases i, simp_all)
+ case (3 i P2 c)
+ thus ?case by (cases P2) (simp_all, cases i, simp_all)
next
case (4 c P2 i Q2)
- then have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
- with 4 show ?case by(cases i, simp, cases P2, auto, case_tac pol2, auto)
+ then have "isnorm P2" "isnorm Q2"
+ by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
+ with 4 show ?case
+ by (cases i) (simp, cases P2, auto, case_tac pol2, auto)
next
case (5 P2 i Q2 c)
- then have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
- with 5 show ?case by(cases i, simp, cases P2, auto, case_tac pol2, auto)
+ then have "isnorm P2" "isnorm Q2"
+ by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
+ with 5 show ?case
+ by (cases i) (simp, cases P2, auto, case_tac pol2, auto)
next
case (6 x P2 y Q2)
then have Y0: "y>0" by (cases y) (auto simp add: norm_Pinj_0_False)
@@ -115,14 +125,17 @@
moreover
note 6 X0
moreover
- from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
+ from 6 have "isnorm P2" "isnorm Q2"
+ by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
moreover
- from 6 `x < y` y have "isnorm (Pinj d Q2)" by (cases d, simp, cases Q2, auto)
+ from 6 `x < y` y have "isnorm (Pinj d Q2)"
+ by (cases d, simp, cases Q2, auto)
ultimately have ?case by (simp add: mkPinj_cn) }
moreover
{ assume "x=y"
moreover
- from 6 have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
+ from 6 have "isnorm P2" "isnorm Q2"
+ by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
moreover
note 6 Y0
moreover
@@ -133,30 +146,35 @@
moreover
note 6 Y0
moreover
- from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
+ from 6 have "isnorm P2" "isnorm Q2"
+ by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
moreover
- from 6 `x > y` x have "isnorm (Pinj d P2)" by (cases d, simp, cases P2, auto)
- ultimately have ?case by (simp add: mkPinj_cn)}
+ from 6 `x > y` x have "isnorm (Pinj d P2)"
+ by (cases d) (simp, cases P2, auto)
+ ultimately have ?case by (simp add: mkPinj_cn) }
ultimately show ?case by blast
next
case (7 x P2 Q2 y R)
- have "x=0 \<or> (x = 1) \<or> (x > 1)" by arith
+ have "x = 0 \<or> x = 1 \<or> x > 1" by arith
moreover
{ assume "x = 0"
with 7 have ?case by (auto simp add: norm_Pinj_0_False) }
moreover
{ assume "x = 1"
- from 7 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
+ from 7 have "isnorm R" "isnorm P2"
+ by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
with 7 `x = 1` have "isnorm (R \<oplus> P2)" by simp
- with 7 `x = 1` have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
+ with 7 `x = 1` have ?case
+ by (simp add: norm_PXtrans[of Q2 y _]) }
moreover
{ assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
- then obtain d where X:"x=Suc (Suc d)" ..
+ then obtain d where X: "x=Suc (Suc d)" ..
with 7 have NR: "isnorm R" "isnorm P2"
by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
with 7 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
with 7 X NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" by simp
- with `isnorm (PX Q2 y R)` X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
+ with `isnorm (PX Q2 y R)` X have ?case
+ by (simp add: norm_PXtrans[of Q2 y _]) }
ultimately show ?case by blast
next
case (8 Q2 y R x P2)
@@ -183,7 +201,7 @@
with 9 have X0: "x>0" by (cases x) auto
with 9 have NP1: "isnorm P1" and NP2: "isnorm P2"
by (auto simp add: norm_PX1[of P1 _ P2] norm_PX2[of P1 _ P2])
- with 9 have NQ1:"isnorm Q1" and NQ2: "isnorm Q2"
+ with 9 have NQ1: "isnorm Q1" and NQ2: "isnorm Q2"
by (auto simp add: norm_PX1[of Q1 _ Q2] norm_PX2[of Q1 _ Q2])
have "y < x \<or> x = y \<or> x < y" by arith
moreover
@@ -194,7 +212,7 @@
have "isnorm (PX P1 d (Pc 0))"
proof (cases P1)
case (PX p1 y p2)
- with 9 sm1 sm2 show ?thesis by - (cases d, simp, cases p2, auto)
+ with 9 sm1 sm2 show ?thesis by (cases d) (simp, cases p2, auto)
next
case Pc with 9 sm1 sm2 show ?thesis by (cases d) auto
next
@@ -214,35 +232,37 @@
have "isnorm (PX Q1 d (Pc 0))"
proof (cases Q1)
case (PX p1 y p2)
- with 9 sm1 sm2 show ?thesis by - (cases d, simp, cases p2, auto)
+ with 9 sm1 sm2 show ?thesis by (cases d) (simp, cases p2, auto)
next
case Pc with 9 sm1 sm2 show ?thesis by (cases d) auto
next
case Pinj with 9 sm1 sm2 show ?thesis by (cases d) auto
qed
ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \<oplus> P1)" by auto
- with X0 sm1 sm2 have ?case by (simp add: mkPX_cn)}
+ with X0 sm1 sm2 have ?case by (simp add: mkPX_cn) }
ultimately show ?case by blast
qed simp
text {* mul concerves normalizedness *}
-lemma mul_cn :"isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<otimes> Q)"
-proof(induct P Q rule: mul.induct)
+lemma mul_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<otimes> Q)"
+proof (induct P Q rule: mul.induct)
case (2 c i P2) thus ?case
- by (cases P2, simp_all) (cases "i",simp_all add: mkPinj_cn)
+ by (cases P2) (simp_all, cases i, simp_all add: mkPinj_cn)
next
case (3 i P2 c) thus ?case
- by (cases P2, simp_all) (cases "i",simp_all add: mkPinj_cn)
+ by (cases P2) (simp_all, cases i, simp_all add: mkPinj_cn)
next
case (4 c P2 i Q2)
- then have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
+ then have "isnorm P2" "isnorm Q2"
+ by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
with 4 show ?case
- by - (cases "c = 0", simp_all, cases "i = 0", simp_all add: mkPX_cn)
+ by (cases "c = 0") (simp_all, cases "i = 0", simp_all add: mkPX_cn)
next
case (5 P2 i Q2 c)
- then have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
+ then have "isnorm P2" "isnorm Q2"
+ by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
with 5 show ?case
- by - (cases "c = 0", simp_all, cases "i = 0", simp_all add: mkPX_cn)
+ by (cases "c = 0") (simp_all, cases "i = 0", simp_all add: mkPX_cn)
next
case (6 x P2 y Q2)
have "x < y \<or> x = y \<or> x > y" by arith
@@ -256,7 +276,7 @@
moreover
from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
moreover
- from 6 `x < y` y have "isnorm (Pinj d Q2)" by - (cases d, simp, cases Q2, auto)
+ from 6 `x < y` y have "isnorm (Pinj d Q2)" by (cases d) (simp, cases Q2, auto)
ultimately have ?case by (simp add: mkPinj_cn) }
moreover
{ assume "x = y"
@@ -278,7 +298,7 @@
moreover
from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
moreover
- from 6 `x > y` x have "isnorm (Pinj d P2)" by - (cases d, simp, cases P2, auto)
+ from 6 `x > y` x have "isnorm (Pinj d P2)" by (cases d) (simp, cases P2, auto)
ultimately have ?case by (simp add: mkPinj_cn) }
ultimately show ?case by blast
next
@@ -356,7 +376,7 @@
proof (induct P)
case (Pinj i P2)
then have "isnorm P2" by (simp add: norm_Pinj[of i P2])
- with Pinj show ?case by - (cases P2, auto, cases i, auto)
+ with Pinj show ?case by (cases P2) (auto, cases i, auto)
next
case (PX P1 x P2) note PX1 = this
from PX have "isnorm P2" "isnorm P1"
@@ -364,7 +384,7 @@
with PX show ?case
proof (cases P1)
case (PX p1 y p2)
- with PX1 show ?thesis by - (cases x, auto, cases p2, auto)
+ with PX1 show ?thesis by (cases x) (auto, cases p2, auto)
next
case Pinj
with PX1 show ?thesis by (cases x) auto
@@ -372,15 +392,18 @@
qed simp
text {* sub conserves normalizedness *}
-lemma sub_cn:"isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)"
-by (simp add: sub_def add_cn neg_cn)
+lemma sub_cn: "isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)"
+ by (simp add: sub_def add_cn neg_cn)
text {* sqr conserves normalizizedness *}
-lemma sqr_cn:"isnorm P \<Longrightarrow> isnorm (sqr P)"
+lemma sqr_cn: "isnorm P \<Longrightarrow> isnorm (sqr P)"
proof (induct P)
+ case Pc
+ then show ?case by simp
+next
case (Pinj i Q)
then show ?case
- by - (cases Q, auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn)
+ by (cases Q) (auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn)
next
case (PX P1 x P2)
then have "x + x ~= 0" "isnorm P2" "isnorm P1"
@@ -389,20 +412,23 @@
and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))"
by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
then show ?case by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
-qed simp
+qed
text {* pow conserves normalizedness *}
-lemma pow_cn:"isnorm P \<Longrightarrow> isnorm (pow n P)"
-proof (induct n arbitrary: P rule: nat_less_induct)
- case (1 k)
+lemma pow_cn: "isnorm P \<Longrightarrow> isnorm (pow n P)"
+proof (induct n arbitrary: P rule: less_induct)
+ case (less k)
show ?case
proof (cases "k = 0")
+ case True
+ then show ?thesis by simp
+ next
case False
then have K2: "k div 2 < k" by (cases k) auto
- from 1 have "isnorm (sqr P)" by (simp add: sqr_cn)
- with 1 False K2 show ?thesis
- by - (simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn)
- qed simp
+ from less have "isnorm (sqr P)" by (simp add: sqr_cn)
+ with less False K2 show ?thesis
+ by (simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn)
+ qed
qed
end
--- a/src/HOL/Decision_Procs/Ferrack.thy Wed Sep 07 08:13:38 2011 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy Thu Sep 08 00:35:22 2011 +0200
@@ -676,13 +676,13 @@
{assume nz: "n = 0" hence ?thesis by (simp add: Let_def simp_num_pair_def)}
moreover
{ assume nnz: "n \<noteq> 0"
- {assume "\<not> ?g > 1" hence ?thesis by (simp add: Let_def simp_num_pair_def simpnum_ci) }
+ {assume "\<not> ?g > 1" hence ?thesis by (simp add: Let_def simp_num_pair_def) }
moreover
{assume g1:"?g>1" hence g0: "?g > 0" by simp
from g1 nnz have gp0: "?g' \<noteq> 0" by simp
hence g'p: "?g' > 0" using gcd_ge_0_int[where x="n" and y="numgcd ?t'"] by arith
hence "?g'= 1 \<or> ?g' > 1" by arith
- moreover {assume "?g'=1" hence ?thesis by (simp add: Let_def simp_num_pair_def simpnum_ci)}
+ moreover {assume "?g'=1" hence ?thesis by (simp add: Let_def simp_num_pair_def)}
moreover {assume g'1:"?g'>1"
from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff ?t' ?g" ..
let ?tt = "reducecoeffh ?t' ?g'"
@@ -800,32 +800,34 @@
proof(induct p rule: simpfm.induct)
case (6 a) hence nb: "numbound0 a" by simp
hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
- thus ?case by (cases "simpnum a", auto simp add: Let_def)
+ thus ?case by (cases "simpnum a") (auto simp add: Let_def)
next
case (7 a) hence nb: "numbound0 a" by simp
hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
- thus ?case by (cases "simpnum a", auto simp add: Let_def)
+ thus ?case by (cases "simpnum a") (auto simp add: Let_def)
next
case (8 a) hence nb: "numbound0 a" by simp
hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
- thus ?case by (cases "simpnum a", auto simp add: Let_def)
+ thus ?case by (cases "simpnum a") (auto simp add: Let_def)
next
case (9 a) hence nb: "numbound0 a" by simp
hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
- thus ?case by (cases "simpnum a", auto simp add: Let_def)
+ thus ?case by (cases "simpnum a") (auto simp add: Let_def)
next
case (10 a) hence nb: "numbound0 a" by simp
hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
- thus ?case by (cases "simpnum a", auto simp add: Let_def)
+ thus ?case by (cases "simpnum a") (auto simp add: Let_def)
next
case (11 a) hence nb: "numbound0 a" by simp
hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
- thus ?case by (cases "simpnum a", auto simp add: Let_def)
+ thus ?case by (cases "simpnum a") (auto simp add: Let_def)
qed(auto simp add: disj_def imp_def iff_def conj_def not_bn)
lemma simpfm_qf: "qfree p \<Longrightarrow> qfree (simpfm p)"
-by (induct p rule: simpfm.induct, auto simp add: disj_qf imp_qf iff_qf conj_qf not_qf Let_def)
- (case_tac "simpnum a",auto)+
+ apply (induct p rule: simpfm.induct)
+ apply (auto simp add: Let_def)
+ apply (case_tac "simpnum a", auto)+
+ done
consts prep :: "fm \<Rightarrow> fm"
recdef prep "measure fmsize"
@@ -854,7 +856,7 @@
"prep p = p"
(hints simp add: fmsize_pos)
lemma prep: "\<And> bs. Ifm bs (prep p) = Ifm bs p"
-by (induct p rule: prep.induct, auto)
+ by (induct p rule: prep.induct) auto
(* Generic quantifier elimination *)
function (sequential) qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm" where
@@ -1037,7 +1039,7 @@
assumes qfp: "qfree p"
shows "(Ifm bs (rlfm p) = Ifm bs p) \<and> isrlfm (rlfm p)"
using qfp
-by (induct p rule: rlfm.induct, auto simp add: lt le gt ge eq neq conj disj conj_lin disj_lin)
+by (induct p rule: rlfm.induct) (auto simp add: lt le gt ge eq neq conj disj conj_lin disj_lin)
(* Operations needed for Ferrante and Rackoff *)
lemma rminusinf_inf:
@@ -1045,9 +1047,11 @@
shows "\<exists> z. \<forall> x < z. Ifm (x#bs) (minusinf p) = Ifm (x#bs) p" (is "\<exists> z. \<forall> x. ?P z x p")
using lp
proof (induct p rule: minusinf.induct)
- case (1 p q) thus ?case by (auto,rule_tac x= "min z za" in exI) auto
+ case (1 p q)
+ thus ?case apply auto apply (rule_tac x= "min z za" in exI) apply auto done
next
- case (2 p q) thus ?case by (auto,rule_tac x= "min z za" in exI) auto
+ case (2 p q)
+ thus ?case apply auto apply (rule_tac x= "min z za" in exI) apply auto done
next
case (3 c e)
from 3 have nb: "numbound0 e" by simp
--- a/src/HOL/HOLCF/Representable.thy Wed Sep 07 08:13:38 2011 +0200
+++ b/src/HOL/HOLCF/Representable.thy Thu Sep 08 00:35:22 2011 +0200
@@ -5,7 +5,7 @@
header {* Representable domains *}
theory Representable
-imports Algebraic Map_Functions Countable
+imports Algebraic Map_Functions "~~/src/HOL/Library/Countable"
begin
default_sort cpo
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Wed Sep 07 08:13:38 2011 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Sep 08 00:35:22 2011 +0200
@@ -628,7 +628,9 @@
val dummy_case_term = IVar NONE;
(*assumption: dummy values are not relevant for serialization*)
val (unitt, unitT) = case lookup_const naming @{const_name Unity}
- of SOME unit' => (IConst (unit', (([], []), [])), the (lookup_tyco naming @{type_name unit}) `%% [])
+ of SOME unit' =>
+ let val unitT = the (lookup_tyco naming @{type_name unit}) `%% []
+ in (IConst (unit', ((([], []), ([], unitT)), false)), unitT) end
| NONE => error ("Must include " ^ @{const_name Unity} ^ " in generated constants.");
fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
| dest_abs (t, ty) =
@@ -645,13 +647,13 @@
val ((v, ty), t) = dest_abs (t2, ty2);
in ICase (((force t1, ty), [(IVar v, tr_bind' t)]), dummy_case_term) end
and tr_bind' t = case unfold_app t
- of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if is_bind c
+ of (IConst (c, ((_, (ty1 :: ty2 :: _, _)), _)), [x1, x2]) => if is_bind c
then tr_bind'' [(x1, ty1), (x2, ty2)]
else force t
| _ => force t;
fun imp_monad_bind'' ts = (SOME dummy_name, unitT) `|=> ICase (((IVar (SOME dummy_name), unitT),
[(unitt, tr_bind'' ts)]), dummy_case_term)
- fun imp_monad_bind' (const as (c, (_, tys))) ts = if is_bind c then case (ts, tys)
+ fun imp_monad_bind' (const as (c, ((_, (tys, _)), _))) ts = if is_bind c then case (ts, tys)
of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)]
| ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3
| (ts, _) => imp_monad_bind (eta_expand 2 (const, ts))
--- a/src/HOL/IsaMakefile Wed Sep 07 08:13:38 2011 +0200
+++ b/src/HOL/IsaMakefile Thu Sep 08 00:35:22 2011 +0200
@@ -463,10 +463,10 @@
Library/Quotient_Option.thy Library/Quotient_Product.thy \
Library/Quotient_Sum.thy Library/Quotient_Syntax.thy \
Library/Quotient_Type.thy Library/RBT.thy Library/RBT_Impl.thy \
- Library/RBT_Mapping.thy Library/README.html Library/Set_Algebras.thy \
- Library/State_Monad.thy Library/Ramsey.thy Library/Reflection.thy \
- Library/Sublist_Order.thy Library/Sum_of_Squares.thy \
- Library/Sum_of_Squares/sos_wrapper.ML \
+ Library/RBT_Mapping.thy Library/README.html Library/Saturated.thy \
+ Library/Set_Algebras.thy Library/State_Monad.thy Library/Ramsey.thy \
+ Library/Reflection.thy Library/Sublist_Order.thy \
+ Library/Sum_of_Squares.thy Library/Sum_of_Squares/sos_wrapper.ML \
Library/Sum_of_Squares/sum_of_squares.ML \
Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy \
Library/Wfrec.thy Library/While_Combinator.thy Library/Zorn.thy \
--- a/src/HOL/Library/Abstract_Rat.thy Wed Sep 07 08:13:38 2011 +0200
+++ b/src/HOL/Library/Abstract_Rat.thy Thu Sep 08 00:35:22 2011 +0200
@@ -10,64 +10,57 @@
type_synonym Num = "int \<times> int"
-abbreviation
- Num0_syn :: Num ("0\<^sub>N")
-where "0\<^sub>N \<equiv> (0, 0)"
+abbreviation Num0_syn :: Num ("0\<^sub>N")
+ where "0\<^sub>N \<equiv> (0, 0)"
-abbreviation
- Numi_syn :: "int \<Rightarrow> Num" ("_\<^sub>N")
-where "i\<^sub>N \<equiv> (i, 1)"
+abbreviation Numi_syn :: "int \<Rightarrow> Num" ("_\<^sub>N")
+ where "i\<^sub>N \<equiv> (i, 1)"
-definition
- isnormNum :: "Num \<Rightarrow> bool"
-where
+definition isnormNum :: "Num \<Rightarrow> bool" where
"isnormNum = (\<lambda>(a,b). (if a = 0 then b = 0 else b > 0 \<and> gcd a b = 1))"
-definition
- normNum :: "Num \<Rightarrow> Num"
-where
- "normNum = (\<lambda>(a,b). (if a=0 \<or> b = 0 then (0,0) else
- (let g = gcd a b
- in if b > 0 then (a div g, b div g) else (- (a div g), - (b div g)))))"
+definition normNum :: "Num \<Rightarrow> Num" where
+ "normNum = (\<lambda>(a,b).
+ (if a=0 \<or> b = 0 then (0,0) else
+ (let g = gcd a b
+ in if b > 0 then (a div g, b div g) else (- (a div g), - (b div g)))))"
-declare gcd_dvd1_int[presburger]
-declare gcd_dvd2_int[presburger]
+declare gcd_dvd1_int[presburger] gcd_dvd2_int[presburger]
+
lemma normNum_isnormNum [simp]: "isnormNum (normNum x)"
proof -
- have " \<exists> a b. x = (a,b)" by auto
- then obtain a b where x[simp]: "x = (a,b)" by blast
- {assume "a=0 \<or> b = 0" hence ?thesis by (simp add: normNum_def isnormNum_def)}
+ obtain a b where x: "x = (a, b)" by (cases x)
+ { assume "a=0 \<or> b = 0" hence ?thesis by (simp add: x normNum_def isnormNum_def) }
moreover
- {assume anz: "a \<noteq> 0" and bnz: "b \<noteq> 0"
+ { assume anz: "a \<noteq> 0" and bnz: "b \<noteq> 0"
let ?g = "gcd a b"
let ?a' = "a div ?g"
let ?b' = "b div ?g"
let ?g' = "gcd ?a' ?b'"
- from anz bnz have "?g \<noteq> 0" by simp with gcd_ge_0_int[of a b]
+ from anz bnz have "?g \<noteq> 0" by simp with gcd_ge_0_int[of a b]
have gpos: "?g > 0" by arith
- have gdvd: "?g dvd a" "?g dvd b" by arith+
- from zdvd_mult_div_cancel[OF gdvd(1)] zdvd_mult_div_cancel[OF gdvd(2)]
- anz bnz
- have nz':"?a' \<noteq> 0" "?b' \<noteq> 0"
- by - (rule notI, simp)+
- from anz bnz have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith
+ have gdvd: "?g dvd a" "?g dvd b" by arith+
+ from zdvd_mult_div_cancel[OF gdvd(1)] zdvd_mult_div_cancel[OF gdvd(2)] anz bnz
+ have nz': "?a' \<noteq> 0" "?b' \<noteq> 0" by - (rule notI, simp)+
+ from anz bnz have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith
from div_gcd_coprime_int[OF stupid] have gp1: "?g' = 1" .
from bnz have "b < 0 \<or> b > 0" by arith
moreover
- {assume b: "b > 0"
- from b have "?b' \<ge> 0"
- by (presburger add: pos_imp_zdiv_nonneg_iff[OF gpos])
- with nz' have b': "?b' > 0" by arith
- from b b' anz bnz nz' gp1 have ?thesis
- by (simp add: isnormNum_def normNum_def Let_def split_def fst_conv snd_conv)}
- moreover {assume b: "b < 0"
- {assume b': "?b' \<ge> 0"
+ { assume b: "b > 0"
+ from b have "?b' \<ge> 0"
+ by (presburger add: pos_imp_zdiv_nonneg_iff[OF gpos])
+ with nz' have b': "?b' > 0" by arith
+ from b b' anz bnz nz' gp1 have ?thesis
+ by (simp add: x isnormNum_def normNum_def Let_def split_def) }
+ moreover {
+ assume b: "b < 0"
+ { assume b': "?b' \<ge> 0"
from gpos have th: "?g \<ge> 0" by arith
from mult_nonneg_nonneg[OF th b'] zdvd_mult_div_cancel[OF gdvd(2)]
have False using b by arith }
- hence b': "?b' < 0" by (presburger add: linorder_not_le[symmetric])
- from anz bnz nz' b b' gp1 have ?thesis
- by (simp add: isnormNum_def normNum_def Let_def split_def)}
+ hence b': "?b' < 0" by (presburger add: linorder_not_le[symmetric])
+ from anz bnz nz' b b' gp1 have ?thesis
+ by (simp add: x isnormNum_def normNum_def Let_def split_def) }
ultimately have ?thesis by blast
}
ultimately show ?thesis by blast
@@ -75,63 +68,55 @@
text {* Arithmetic over Num *}
-definition
- Nadd :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "+\<^sub>N" 60)
-where
- "Nadd = (\<lambda>(a,b) (a',b'). if a = 0 \<or> b = 0 then normNum(a',b')
- else if a'=0 \<or> b' = 0 then normNum(a,b)
+definition Nadd :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "+\<^sub>N" 60) where
+ "Nadd = (\<lambda>(a,b) (a',b'). if a = 0 \<or> b = 0 then normNum(a',b')
+ else if a'=0 \<or> b' = 0 then normNum(a,b)
else normNum(a*b' + b*a', b*b'))"
-definition
- Nmul :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "*\<^sub>N" 60)
-where
- "Nmul = (\<lambda>(a,b) (a',b'). let g = gcd (a*a') (b*b')
+definition Nmul :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "*\<^sub>N" 60) where
+ "Nmul = (\<lambda>(a,b) (a',b'). let g = gcd (a*a') (b*b')
in (a*a' div g, b*b' div g))"
-definition
- Nneg :: "Num \<Rightarrow> Num" ("~\<^sub>N")
-where
- "Nneg \<equiv> (\<lambda>(a,b). (-a,b))"
+definition Nneg :: "Num \<Rightarrow> Num" ("~\<^sub>N")
+ where "Nneg \<equiv> (\<lambda>(a,b). (-a,b))"
-definition
- Nsub :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "-\<^sub>N" 60)
-where
- "Nsub = (\<lambda>a b. a +\<^sub>N ~\<^sub>N b)"
+definition Nsub :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "-\<^sub>N" 60)
+ where "Nsub = (\<lambda>a b. a +\<^sub>N ~\<^sub>N b)"
-definition
- Ninv :: "Num \<Rightarrow> Num"
-where
- "Ninv \<equiv> \<lambda>(a,b). if a < 0 then (-b, \<bar>a\<bar>) else (b,a)"
+definition Ninv :: "Num \<Rightarrow> Num"
+ where "Ninv = (\<lambda>(a,b). if a < 0 then (-b, \<bar>a\<bar>) else (b,a))"
-definition
- Ndiv :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "\<div>\<^sub>N" 60)
-where
- "Ndiv \<equiv> \<lambda>a b. a *\<^sub>N Ninv b"
+definition Ndiv :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "\<div>\<^sub>N" 60)
+ where "Ndiv = (\<lambda>a b. a *\<^sub>N Ninv b)"
lemma Nneg_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (~\<^sub>N x)"
- by(simp add: isnormNum_def Nneg_def split_def)
+ by (simp add: isnormNum_def Nneg_def split_def)
+
lemma Nadd_normN[simp]: "isnormNum (x +\<^sub>N y)"
by (simp add: Nadd_def split_def)
+
lemma Nsub_normN[simp]: "\<lbrakk> isnormNum y\<rbrakk> \<Longrightarrow> isnormNum (x -\<^sub>N y)"
by (simp add: Nsub_def split_def)
-lemma Nmul_normN[simp]: assumes xn:"isnormNum x" and yn: "isnormNum y"
+
+lemma Nmul_normN[simp]:
+ assumes xn: "isnormNum x" and yn: "isnormNum y"
shows "isnormNum (x *\<^sub>N y)"
-proof-
- have "\<exists>a b. x = (a,b)" and "\<exists> a' b'. y = (a',b')" by auto
- then obtain a b a' b' where ab: "x = (a,b)" and ab': "y = (a',b')" by blast
- {assume "a = 0"
- hence ?thesis using xn ab ab'
- by (simp add: isnormNum_def Let_def Nmul_def split_def)}
+proof -
+ obtain a b where x: "x = (a, b)" by (cases x)
+ obtain a' b' where y: "y = (a', b')" by (cases y)
+ { assume "a = 0"
+ hence ?thesis using xn x y
+ by (simp add: isnormNum_def Let_def Nmul_def split_def) }
moreover
- {assume "a' = 0"
- hence ?thesis using yn ab ab'
- by (simp add: isnormNum_def Let_def Nmul_def split_def)}
+ { assume "a' = 0"
+ hence ?thesis using yn x y
+ by (simp add: isnormNum_def Let_def Nmul_def split_def) }
moreover
- {assume a: "a \<noteq>0" and a': "a'\<noteq>0"
- hence bp: "b > 0" "b' > 0" using xn yn ab ab' by (simp_all add: isnormNum_def)
- from mult_pos_pos[OF bp] have "x *\<^sub>N y = normNum (a*a', b*b')"
- using ab ab' a a' bp by (simp add: Nmul_def Let_def split_def normNum_def)
- hence ?thesis by simp}
+ { assume a: "a \<noteq>0" and a': "a'\<noteq>0"
+ hence bp: "b > 0" "b' > 0" using xn yn x y by (simp_all add: isnormNum_def)
+ from mult_pos_pos[OF bp] have "x *\<^sub>N y = normNum (a * a', b * b')"
+ using x y a a' bp by (simp add: Nmul_def Let_def split_def normNum_def)
+ hence ?thesis by simp }
ultimately show ?thesis by blast
qed
@@ -139,89 +124,77 @@
by (simp add: Ninv_def isnormNum_def split_def)
(cases "fst x = 0", auto simp add: gcd_commute_int)
-lemma isnormNum_int[simp]:
+lemma isnormNum_int[simp]:
"isnormNum 0\<^sub>N" "isnormNum ((1::int)\<^sub>N)" "i \<noteq> 0 \<Longrightarrow> isnormNum (i\<^sub>N)"
by (simp_all add: isnormNum_def)
text {* Relations over Num *}
-definition
- Nlt0:: "Num \<Rightarrow> bool" ("0>\<^sub>N")
-where
- "Nlt0 = (\<lambda>(a,b). a < 0)"
+definition Nlt0:: "Num \<Rightarrow> bool" ("0>\<^sub>N")
+ where "Nlt0 = (\<lambda>(a,b). a < 0)"
-definition
- Nle0:: "Num \<Rightarrow> bool" ("0\<ge>\<^sub>N")
-where
- "Nle0 = (\<lambda>(a,b). a \<le> 0)"
+definition Nle0:: "Num \<Rightarrow> bool" ("0\<ge>\<^sub>N")
+ where "Nle0 = (\<lambda>(a,b). a \<le> 0)"
-definition
- Ngt0:: "Num \<Rightarrow> bool" ("0<\<^sub>N")
-where
- "Ngt0 = (\<lambda>(a,b). a > 0)"
+definition Ngt0:: "Num \<Rightarrow> bool" ("0<\<^sub>N")
+ where "Ngt0 = (\<lambda>(a,b). a > 0)"
-definition
- Nge0:: "Num \<Rightarrow> bool" ("0\<le>\<^sub>N")
-where
- "Nge0 = (\<lambda>(a,b). a \<ge> 0)"
+definition Nge0:: "Num \<Rightarrow> bool" ("0\<le>\<^sub>N")
+ where "Nge0 = (\<lambda>(a,b). a \<ge> 0)"
-definition
- Nlt :: "Num \<Rightarrow> Num \<Rightarrow> bool" (infix "<\<^sub>N" 55)
-where
- "Nlt = (\<lambda>a b. 0>\<^sub>N (a -\<^sub>N b))"
+definition Nlt :: "Num \<Rightarrow> Num \<Rightarrow> bool" (infix "<\<^sub>N" 55)
+ where "Nlt = (\<lambda>a b. 0>\<^sub>N (a -\<^sub>N b))"
-definition
- Nle :: "Num \<Rightarrow> Num \<Rightarrow> bool" (infix "\<le>\<^sub>N" 55)
-where
- "Nle = (\<lambda>a b. 0\<ge>\<^sub>N (a -\<^sub>N b))"
+definition Nle :: "Num \<Rightarrow> Num \<Rightarrow> bool" (infix "\<le>\<^sub>N" 55)
+ where "Nle = (\<lambda>a b. 0\<ge>\<^sub>N (a -\<^sub>N b))"
-definition
- "INum = (\<lambda>(a,b). of_int a / of_int b)"
+definition "INum = (\<lambda>(a,b). of_int a / of_int b)"
lemma INum_int [simp]: "INum (i\<^sub>N) = ((of_int i) ::'a::field)" "INum 0\<^sub>N = (0::'a::field)"
by (simp_all add: INum_def)
-lemma isnormNum_unique[simp]:
- assumes na: "isnormNum x" and nb: "isnormNum y"
+lemma isnormNum_unique[simp]:
+ assumes na: "isnormNum x" and nb: "isnormNum y"
shows "((INum x ::'a::{field_char_0, field_inverse_zero}) = INum y) = (x = y)" (is "?lhs = ?rhs")
proof
- have "\<exists> a b a' b'. x = (a,b) \<and> y = (a',b')" by auto
- then obtain a b a' b' where xy[simp]: "x = (a,b)" "y=(a',b')" by blast
- assume H: ?lhs
- {assume "a = 0 \<or> b = 0 \<or> a' = 0 \<or> b' = 0"
+ obtain a b where x: "x = (a, b)" by (cases x)
+ obtain a' b' where y: "y = (a', b')" by (cases y)
+ assume H: ?lhs
+ { assume "a = 0 \<or> b = 0 \<or> a' = 0 \<or> b' = 0"
hence ?rhs using na nb H
- by (simp add: INum_def split_def isnormNum_def split: split_if_asm)}
+ by (simp add: x y INum_def split_def isnormNum_def split: split_if_asm) }
moreover
{ assume az: "a \<noteq> 0" and bz: "b \<noteq> 0" and a'z: "a'\<noteq>0" and b'z: "b'\<noteq>0"
- from az bz a'z b'z na nb have pos: "b > 0" "b' > 0" by (simp_all add: isnormNum_def)
- from H bz b'z have eq:"a * b' = a'*b"
- by (simp add: INum_def eq_divide_eq divide_eq_eq of_int_mult[symmetric] del: of_int_mult)
- from az a'z na nb have gcd1: "gcd a b = 1" "gcd b a = 1" "gcd a' b' = 1" "gcd b' a' = 1"
- by (simp_all add: isnormNum_def add: gcd_commute_int)
- from eq have raw_dvd: "a dvd a'*b" "b dvd b'*a" "a' dvd a*b'" "b' dvd b*a'"
- apply -
+ from az bz a'z b'z na nb have pos: "b > 0" "b' > 0" by (simp_all add: x y isnormNum_def)
+ from H bz b'z have eq: "a * b' = a'*b"
+ by (simp add: x y INum_def eq_divide_eq divide_eq_eq of_int_mult[symmetric] del: of_int_mult)
+ from az a'z na nb have gcd1: "gcd a b = 1" "gcd b a = 1" "gcd a' b' = 1" "gcd b' a' = 1"
+ by (simp_all add: x y isnormNum_def add: gcd_commute_int)
+ from eq have raw_dvd: "a dvd a' * b" "b dvd b' * a" "a' dvd a * b'" "b' dvd b * a'"
+ apply -
apply algebra
apply algebra
apply simp
apply algebra
done
from zdvd_antisym_abs[OF coprime_dvd_mult_int[OF gcd1(2) raw_dvd(2)]
- coprime_dvd_mult_int[OF gcd1(4) raw_dvd(4)]]
+ coprime_dvd_mult_int[OF gcd1(4) raw_dvd(4)]]
have eq1: "b = b'" using pos by arith
with eq have "a = a'" using pos by simp
- with eq1 have ?rhs by simp}
+ with eq1 have ?rhs by (simp add: x y) }
ultimately show ?rhs by blast
next
assume ?rhs thus ?lhs by simp
qed
-lemma isnormNum0[simp]: "isnormNum x \<Longrightarrow> (INum x = (0::'a::{field_char_0, field_inverse_zero})) = (x = 0\<^sub>N)"
+lemma isnormNum0[simp]:
+ "isnormNum x \<Longrightarrow> (INum x = (0::'a::{field_char_0, field_inverse_zero})) = (x = 0\<^sub>N)"
unfolding INum_int(2)[symmetric]
- by (rule isnormNum_unique, simp_all)
+ by (rule isnormNum_unique) simp_all
-lemma of_int_div_aux: "d ~= 0 ==> ((of_int x)::'a::field_char_0) / (of_int d) =
+lemma of_int_div_aux: "d ~= 0 ==> ((of_int x)::'a::field_char_0) / (of_int d) =
of_int (x div d) + (of_int (x mod d)) / ((of_int d)::'a)"
proof -
assume "d ~= 0"
@@ -231,7 +204,7 @@
by auto
then have eq: "of_int x = ?t"
by (simp only: of_int_mult[symmetric] of_int_add [symmetric])
- then have "of_int x / of_int d = ?t / of_int d"
+ then have "of_int x / of_int d = ?t / of_int d"
using cong[OF refl[of ?f] eq] by simp
then show ?thesis by (simp add: add_divide_distrib algebra_simps `d ~= 0`)
qed
@@ -241,25 +214,26 @@
apply (frule of_int_div_aux [of d n, where ?'a = 'a])
apply simp
apply (simp add: dvd_eq_mod_eq_0)
-done
+ done
lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{field_char_0, field_inverse_zero})"
-proof-
- have "\<exists> a b. x = (a,b)" by auto
- then obtain a b where x[simp]: "x = (a,b)" by blast
- {assume "a=0 \<or> b = 0" hence ?thesis
- by (simp add: INum_def normNum_def split_def Let_def)}
- moreover
- {assume a: "a\<noteq>0" and b: "b\<noteq>0"
+proof -
+ obtain a b where x: "x = (a, b)" by (cases x)
+ { assume "a = 0 \<or> b = 0"
+ hence ?thesis by (simp add: x INum_def normNum_def split_def Let_def) }
+ moreover
+ { assume a: "a \<noteq> 0" and b: "b \<noteq> 0"
let ?g = "gcd a b"
from a b have g: "?g \<noteq> 0"by simp
from of_int_div[OF g, where ?'a = 'a]
- have ?thesis by (auto simp add: INum_def normNum_def split_def Let_def)}
+ have ?thesis by (auto simp add: x INum_def normNum_def split_def Let_def) }
ultimately show ?thesis by blast
qed
-lemma INum_normNum_iff: "(INum x ::'a::{field_char_0, field_inverse_zero}) = INum y \<longleftrightarrow> normNum x = normNum y" (is "?lhs = ?rhs")
+lemma INum_normNum_iff:
+ "(INum x ::'a::{field_char_0, field_inverse_zero}) = INum y \<longleftrightarrow> normNum x = normNum y"
+ (is "?lhs = ?rhs")
proof -
have "normNum x = normNum y \<longleftrightarrow> (INum (normNum x) :: 'a) = INum (normNum y)"
by (simp del: normNum)
@@ -268,139 +242,157 @@
qed
lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: {field_char_0, field_inverse_zero})"
-proof-
-let ?z = "0:: 'a"
- have " \<exists> a b. x = (a,b)" " \<exists> a' b'. y = (a',b')" by auto
- then obtain a b a' b' where x[simp]: "x = (a,b)"
- and y[simp]: "y = (a',b')" by blast
- {assume "a=0 \<or> a'= 0 \<or> b =0 \<or> b' = 0" hence ?thesis
- apply (cases "a=0",simp_all add: Nadd_def)
- apply (cases "b= 0",simp_all add: INum_def)
- apply (cases "a'= 0",simp_all)
- apply (cases "b'= 0",simp_all)
+proof -
+ let ?z = "0:: 'a"
+ obtain a b where x: "x = (a, b)" by (cases x)
+ obtain a' b' where y: "y = (a', b')" by (cases y)
+ { assume "a=0 \<or> a'= 0 \<or> b =0 \<or> b' = 0"
+ hence ?thesis
+ apply (cases "a=0", simp_all add: x y Nadd_def)
+ apply (cases "b= 0", simp_all add: INum_def)
+ apply (cases "a'= 0", simp_all)
+ apply (cases "b'= 0", simp_all)
done }
- moreover
- {assume aa':"a \<noteq> 0" "a'\<noteq> 0" and bb': "b \<noteq> 0" "b' \<noteq> 0"
- {assume z: "a * b' + b * a' = 0"
+ moreover
+ { assume aa': "a \<noteq> 0" "a'\<noteq> 0" and bb': "b \<noteq> 0" "b' \<noteq> 0"
+ { assume z: "a * b' + b * a' = 0"
hence "of_int (a*b' + b*a') / (of_int b* of_int b') = ?z" by simp
- hence "of_int b' * of_int a / (of_int b * of_int b') + of_int b * of_int a' / (of_int b * of_int b') = ?z" by (simp add:add_divide_distrib)
- hence th: "of_int a / of_int b + of_int a' / of_int b' = ?z" using bb' aa' by simp
- from z aa' bb' have ?thesis
- by (simp add: th Nadd_def normNum_def INum_def split_def)}
- moreover {assume z: "a * b' + b * a' \<noteq> 0"
+ hence "of_int b' * of_int a / (of_int b * of_int b') +
+ of_int b * of_int a' / (of_int b * of_int b') = ?z"
+ by (simp add:add_divide_distrib)
+ hence th: "of_int a / of_int b + of_int a' / of_int b' = ?z" using bb' aa'
+ by simp
+ from z aa' bb' have ?thesis
+ by (simp add: x y th Nadd_def normNum_def INum_def split_def) }
+ moreover {
+ assume z: "a * b' + b * a' \<noteq> 0"
let ?g = "gcd (a * b' + b * a') (b*b')"
have gz: "?g \<noteq> 0" using z by simp
have ?thesis using aa' bb' z gz
- of_int_div[where ?'a = 'a, OF gz gcd_dvd1_int[where x="a * b' + b * a'" and y="b*b'"]] of_int_div[where ?'a = 'a,
- OF gz gcd_dvd2_int[where x="a * b' + b * a'" and y="b*b'"]]
- by (simp add: Nadd_def INum_def normNum_def Let_def add_divide_distrib)}
- ultimately have ?thesis using aa' bb'
- by (simp add: Nadd_def INum_def normNum_def Let_def) }
+ of_int_div[where ?'a = 'a, OF gz gcd_dvd1_int[where x="a * b' + b * a'" and y="b*b'"]]
+ of_int_div[where ?'a = 'a, OF gz gcd_dvd2_int[where x="a * b' + b * a'" and y="b*b'"]]
+ by (simp add: x y Nadd_def INum_def normNum_def Let_def add_divide_distrib) }
+ ultimately have ?thesis using aa' bb'
+ by (simp add: x y Nadd_def INum_def normNum_def Let_def) }
ultimately show ?thesis by blast
qed
-lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a :: {field_char_0, field_inverse_zero}) "
-proof-
+lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a :: {field_char_0, field_inverse_zero})"
+proof -
let ?z = "0::'a"
- have " \<exists> a b. x = (a,b)" " \<exists> a' b'. y = (a',b')" by auto
- then obtain a b a' b' where x: "x = (a,b)" and y: "y = (a',b')" by blast
- {assume "a=0 \<or> a'= 0 \<or> b = 0 \<or> b' = 0" hence ?thesis
- apply (cases "a=0",simp_all add: x y Nmul_def INum_def Let_def)
- apply (cases "b=0",simp_all)
- apply (cases "a'=0",simp_all)
+ obtain a b where x: "x = (a, b)" by (cases x)
+ obtain a' b' where y: "y = (a', b')" by (cases y)
+ { assume "a=0 \<or> a'= 0 \<or> b = 0 \<or> b' = 0"
+ hence ?thesis
+ apply (cases "a=0", simp_all add: x y Nmul_def INum_def Let_def)
+ apply (cases "b=0", simp_all)
+ apply (cases "a'=0", simp_all)
done }
moreover
- {assume z: "a \<noteq> 0" "a' \<noteq> 0" "b \<noteq> 0" "b' \<noteq> 0"
+ { assume z: "a \<noteq> 0" "a' \<noteq> 0" "b \<noteq> 0" "b' \<noteq> 0"
let ?g="gcd (a*a') (b*b')"
have gz: "?g \<noteq> 0" using z by simp
- from z of_int_div[where ?'a = 'a, OF gz gcd_dvd1_int[where x="a*a'" and y="b*b'"]]
- of_int_div[where ?'a = 'a , OF gz gcd_dvd2_int[where x="a*a'" and y="b*b'"]]
- have ?thesis by (simp add: Nmul_def x y Let_def INum_def)}
+ from z of_int_div[where ?'a = 'a, OF gz gcd_dvd1_int[where x="a*a'" and y="b*b'"]]
+ of_int_div[where ?'a = 'a , OF gz gcd_dvd2_int[where x="a*a'" and y="b*b'"]]
+ have ?thesis by (simp add: Nmul_def x y Let_def INum_def) }
ultimately show ?thesis by blast
qed
lemma Nneg[simp]: "INum (~\<^sub>N x) = - (INum x ::'a:: field)"
by (simp add: Nneg_def split_def INum_def)
-lemma Nsub[simp]: shows "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {field_char_0, field_inverse_zero})"
-by (simp add: Nsub_def split_def)
+lemma Nsub[simp]: "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {field_char_0, field_inverse_zero})"
+ by (simp add: Nsub_def split_def)
lemma Ninv[simp]: "INum (Ninv x) = (1::'a :: field_inverse_zero) / (INum x)"
by (simp add: Ninv_def INum_def split_def)
-lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y ::'a :: {field_char_0, field_inverse_zero})" by (simp add: Ndiv_def)
+lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y ::'a :: {field_char_0, field_inverse_zero})"
+ by (simp add: Ndiv_def)
-lemma Nlt0_iff[simp]: assumes nx: "isnormNum x"
- shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})< 0) = 0>\<^sub>N x "
-proof-
- have " \<exists> a b. x = (a,b)" by simp
- then obtain a b where x[simp]:"x = (a,b)" by blast
- {assume "a = 0" hence ?thesis by (simp add: Nlt0_def INum_def) }
+lemma Nlt0_iff[simp]:
+ assumes nx: "isnormNum x"
+ shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})< 0) = 0>\<^sub>N x"
+proof -
+ obtain a b where x: "x = (a, b)" by (cases x)
+ { assume "a = 0" hence ?thesis by (simp add: x Nlt0_def INum_def) }
moreover
- {assume a: "a\<noteq>0" hence b: "(of_int b::'a) > 0" using nx by (simp add: isnormNum_def)
+ { assume a: "a \<noteq> 0" hence b: "(of_int b::'a) > 0"
+ using nx by (simp add: x isnormNum_def)
from pos_divide_less_eq[OF b, where b="of_int a" and a="0::'a"]
- have ?thesis by (simp add: Nlt0_def INum_def)}
+ have ?thesis by (simp add: x Nlt0_def INum_def) }
ultimately show ?thesis by blast
qed
-lemma Nle0_iff[simp]:assumes nx: "isnormNum x"
+lemma Nle0_iff[simp]:
+ assumes nx: "isnormNum x"
shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) \<le> 0) = 0\<ge>\<^sub>N x"
-proof-
- have " \<exists> a b. x = (a,b)" by simp
- then obtain a b where x[simp]:"x = (a,b)" by blast
- {assume "a = 0" hence ?thesis by (simp add: Nle0_def INum_def) }
+proof -
+ obtain a b where x: "x = (a, b)" by (cases x)
+ { assume "a = 0" hence ?thesis by (simp add: x Nle0_def INum_def) }
moreover
- {assume a: "a\<noteq>0" hence b: "(of_int b :: 'a) > 0" using nx by (simp add: isnormNum_def)
+ { assume a: "a \<noteq> 0" hence b: "(of_int b :: 'a) > 0"
+ using nx by (simp add: x isnormNum_def)
from pos_divide_le_eq[OF b, where b="of_int a" and a="0::'a"]
- have ?thesis by (simp add: Nle0_def INum_def)}
+ have ?thesis by (simp add: x Nle0_def INum_def) }
ultimately show ?thesis by blast
qed
-lemma Ngt0_iff[simp]:assumes nx: "isnormNum x" shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})> 0) = 0<\<^sub>N x"
-proof-
- have " \<exists> a b. x = (a,b)" by simp
- then obtain a b where x[simp]:"x = (a,b)" by blast
- {assume "a = 0" hence ?thesis by (simp add: Ngt0_def INum_def) }
+lemma Ngt0_iff[simp]:
+ assumes nx: "isnormNum x"
+ shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})> 0) = 0<\<^sub>N x"
+proof -
+ obtain a b where x: "x = (a, b)" by (cases x)
+ { assume "a = 0" hence ?thesis by (simp add: x Ngt0_def INum_def) }
moreover
- {assume a: "a\<noteq>0" hence b: "(of_int b::'a) > 0" using nx by (simp add: isnormNum_def)
+ { assume a: "a \<noteq> 0" hence b: "(of_int b::'a) > 0" using nx
+ by (simp add: x isnormNum_def)
from pos_less_divide_eq[OF b, where b="of_int a" and a="0::'a"]
- have ?thesis by (simp add: Ngt0_def INum_def)}
- ultimately show ?thesis by blast
-qed
-lemma Nge0_iff[simp]:assumes nx: "isnormNum x"
- shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) \<ge> 0) = 0\<le>\<^sub>N x"
-proof-
- have " \<exists> a b. x = (a,b)" by simp
- then obtain a b where x[simp]:"x = (a,b)" by blast
- {assume "a = 0" hence ?thesis by (simp add: Nge0_def INum_def) }
- moreover
- {assume a: "a\<noteq>0" hence b: "(of_int b::'a) > 0" using nx by (simp add: isnormNum_def)
- from pos_le_divide_eq[OF b, where b="of_int a" and a="0::'a"]
- have ?thesis by (simp add: Nge0_def INum_def)}
+ have ?thesis by (simp add: x Ngt0_def INum_def) }
ultimately show ?thesis by blast
qed
-lemma Nlt_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y"
+lemma Nge0_iff[simp]:
+ assumes nx: "isnormNum x"
+ shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) \<ge> 0) = 0\<le>\<^sub>N x"
+proof -
+ obtain a b where x: "x = (a, b)" by (cases x)
+ { assume "a = 0" hence ?thesis by (simp add: x Nge0_def INum_def) }
+ moreover
+ { assume "a \<noteq> 0" hence b: "(of_int b::'a) > 0" using nx
+ by (simp add: x isnormNum_def)
+ from pos_le_divide_eq[OF b, where b="of_int a" and a="0::'a"]
+ have ?thesis by (simp add: x Nge0_def INum_def) }
+ ultimately show ?thesis by blast
+qed
+
+lemma Nlt_iff[simp]:
+ assumes nx: "isnormNum x" and ny: "isnormNum y"
shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) < INum y) = (x <\<^sub>N y)"
-proof-
+proof -
let ?z = "0::'a"
- have "((INum x ::'a) < INum y) = (INum (x -\<^sub>N y) < ?z)" using nx ny by simp
- also have "\<dots> = (0>\<^sub>N (x -\<^sub>N y))" using Nlt0_iff[OF Nsub_normN[OF ny]] by simp
+ have "((INum x ::'a) < INum y) = (INum (x -\<^sub>N y) < ?z)"
+ using nx ny by simp
+ also have "\<dots> = (0>\<^sub>N (x -\<^sub>N y))"
+ using Nlt0_iff[OF Nsub_normN[OF ny]] by simp
finally show ?thesis by (simp add: Nlt_def)
qed
-lemma Nle_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y"
+lemma Nle_iff[simp]:
+ assumes nx: "isnormNum x" and ny: "isnormNum y"
shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})\<le> INum y) = (x \<le>\<^sub>N y)"
-proof-
- have "((INum x ::'a) \<le> INum y) = (INum (x -\<^sub>N y) \<le> (0::'a))" using nx ny by simp
- also have "\<dots> = (0\<ge>\<^sub>N (x -\<^sub>N y))" using Nle0_iff[OF Nsub_normN[OF ny]] by simp
+proof -
+ have "((INum x ::'a) \<le> INum y) = (INum (x -\<^sub>N y) \<le> (0::'a))"
+ using nx ny by simp
+ also have "\<dots> = (0\<ge>\<^sub>N (x -\<^sub>N y))"
+ using Nle0_iff[OF Nsub_normN[OF ny]] by simp
finally show ?thesis by (simp add: Nle_def)
qed
lemma Nadd_commute:
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "x +\<^sub>N y = y +\<^sub>N x"
-proof-
+proof -
have n: "isnormNum (x +\<^sub>N y)" "isnormNum (y +\<^sub>N x)" by simp_all
have "(INum (x +\<^sub>N y)::'a) = INum (y +\<^sub>N x)" by simp
with isnormNum_unique[OF n] show ?thesis by simp
@@ -409,7 +401,7 @@
lemma [simp]:
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "(0, b) +\<^sub>N y = normNum y"
- and "(a, 0) +\<^sub>N y = normNum y"
+ and "(a, 0) +\<^sub>N y = normNum y"
and "x +\<^sub>N (0, b) = normNum x"
and "x +\<^sub>N (a, 0) = normNum x"
apply (simp add: Nadd_def split_def)
@@ -420,14 +412,13 @@
lemma normNum_nilpotent_aux[simp]:
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
- assumes nx: "isnormNum x"
+ assumes nx: "isnormNum x"
shows "normNum x = x"
-proof-
+proof -
let ?a = "normNum x"
have n: "isnormNum ?a" by simp
- have th:"INum ?a = (INum x ::'a)" by simp
- with isnormNum_unique[OF n nx]
- show ?thesis by simp
+ have th: "INum ?a = (INum x ::'a)" by simp
+ with isnormNum_unique[OF n nx] show ?thesis by simp
qed
lemma normNum_nilpotent[simp]:
@@ -445,7 +436,7 @@
lemma Nadd_normNum1[simp]:
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "normNum x +\<^sub>N y = x +\<^sub>N y"
-proof-
+proof -
have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)" by simp_all
have "INum (normNum x +\<^sub>N y) = INum x + (INum y :: 'a)" by simp
also have "\<dots> = INum (x +\<^sub>N y)" by simp
@@ -455,7 +446,7 @@
lemma Nadd_normNum2[simp]:
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "x +\<^sub>N normNum y = x +\<^sub>N y"
-proof-
+proof -
have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)" by simp_all
have "INum (x +\<^sub>N normNum y) = INum x + (INum y :: 'a)" by simp
also have "\<dots> = INum (x +\<^sub>N y)" by simp
@@ -465,7 +456,7 @@
lemma Nadd_assoc:
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "x +\<^sub>N y +\<^sub>N z = x +\<^sub>N (y +\<^sub>N z)"
-proof-
+proof -
have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))" by simp_all
have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp
with isnormNum_unique[OF n] show ?thesis by simp
@@ -476,10 +467,10 @@
lemma Nmul_assoc:
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
- assumes nx: "isnormNum x" and ny:"isnormNum y" and nz:"isnormNum z"
+ assumes nx: "isnormNum x" and ny: "isnormNum y" and nz: "isnormNum z"
shows "x *\<^sub>N y *\<^sub>N z = x *\<^sub>N (y *\<^sub>N z)"
-proof-
- from nx ny nz have n: "isnormNum (x *\<^sub>N y *\<^sub>N z)" "isnormNum (x *\<^sub>N (y *\<^sub>N z))"
+proof -
+ from nx ny nz have n: "isnormNum (x *\<^sub>N y *\<^sub>N z)" "isnormNum (x *\<^sub>N (y *\<^sub>N z))"
by simp_all
have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp
with isnormNum_unique[OF n] show ?thesis by simp
@@ -487,14 +478,15 @@
lemma Nsub0:
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
- assumes x: "isnormNum x" and y:"isnormNum y" shows "(x -\<^sub>N y = 0\<^sub>N) = (x = y)"
-proof-
- { fix h :: 'a
- from isnormNum_unique[where 'a = 'a, OF Nsub_normN[OF y], where y="0\<^sub>N"]
- have "(x -\<^sub>N y = 0\<^sub>N) = (INum (x -\<^sub>N y) = (INum 0\<^sub>N :: 'a)) " by simp
- also have "\<dots> = (INum x = (INum y :: 'a))" by simp
- also have "\<dots> = (x = y)" using x y by simp
- finally show ?thesis . }
+ assumes x: "isnormNum x" and y: "isnormNum y"
+ shows "x -\<^sub>N y = 0\<^sub>N \<longleftrightarrow> x = y"
+proof -
+ fix h :: 'a
+ from isnormNum_unique[where 'a = 'a, OF Nsub_normN[OF y], where y="0\<^sub>N"]
+ have "(x -\<^sub>N y = 0\<^sub>N) = (INum (x -\<^sub>N y) = (INum 0\<^sub>N :: 'a)) " by simp
+ also have "\<dots> = (INum x = (INum y :: 'a))" by simp
+ also have "\<dots> = (x = y)" using x y by simp
+ finally show ?thesis .
qed
lemma Nmul0[simp]: "c *\<^sub>N 0\<^sub>N = 0\<^sub>N" " 0\<^sub>N *\<^sub>N c = 0\<^sub>N"
@@ -502,24 +494,26 @@
lemma Nmul_eq0[simp]:
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
- assumes nx:"isnormNum x" and ny: "isnormNum y"
- shows "(x*\<^sub>N y = 0\<^sub>N) = (x = 0\<^sub>N \<or> y = 0\<^sub>N)"
-proof-
- { fix h :: 'a
- have " \<exists> a b a' b'. x = (a,b) \<and> y= (a',b')" by auto
- then obtain a b a' b' where xy[simp]: "x = (a,b)" "y = (a',b')" by blast
- have n0: "isnormNum 0\<^sub>N" by simp
- show ?thesis using nx ny
- apply (simp only: isnormNum_unique[where ?'a = 'a, OF Nmul_normN[OF nx ny] n0, symmetric] Nmul[where ?'a = 'a])
- by (simp add: INum_def split_def isnormNum_def split: split_if_asm)
- }
+ assumes nx: "isnormNum x" and ny: "isnormNum y"
+ shows "x*\<^sub>N y = 0\<^sub>N \<longleftrightarrow> x = 0\<^sub>N \<or> y = 0\<^sub>N"
+proof -
+ fix h :: 'a
+ obtain a b where x: "x = (a, b)" by (cases x)
+ obtain a' b' where y: "y = (a', b')" by (cases y)
+ have n0: "isnormNum 0\<^sub>N" by simp
+ show ?thesis using nx ny
+ apply (simp only: isnormNum_unique[where ?'a = 'a, OF Nmul_normN[OF nx ny] n0, symmetric]
+ Nmul[where ?'a = 'a])
+ apply (simp add: x y INum_def split_def isnormNum_def split: split_if_asm)
+ done
qed
+
lemma Nneg_Nneg[simp]: "~\<^sub>N (~\<^sub>N c) = c"
by (simp add: Nneg_def split_def)
-lemma Nmul1[simp]:
- "isnormNum c \<Longrightarrow> 1\<^sub>N *\<^sub>N c = c"
- "isnormNum c \<Longrightarrow> c *\<^sub>N (1\<^sub>N) = c"
+lemma Nmul1[simp]:
+ "isnormNum c \<Longrightarrow> 1\<^sub>N *\<^sub>N c = c"
+ "isnormNum c \<Longrightarrow> c *\<^sub>N (1\<^sub>N) = c"
apply (simp_all add: Nmul_def Let_def split_def isnormNum_def)
apply (cases "fst c = 0", simp_all, cases c, simp_all)+
done
--- a/src/HOL/Library/Library.thy Wed Sep 07 08:13:38 2011 +0200
+++ b/src/HOL/Library/Library.thy Thu Sep 08 00:35:22 2011 +0200
@@ -55,6 +55,7 @@
Ramsey
Reflection
RBT_Mapping
+ Saturated
Set_Algebras
State_Monad
Sum_of_Squares
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Saturated.thy Thu Sep 08 00:35:22 2011 +0200
@@ -0,0 +1,242 @@
+(* Author: Brian Huffman *)
+(* Author: Peter Gammie *)
+(* Author: Florian Haftmann *)
+
+header {* Saturated arithmetic *}
+
+theory Saturated
+imports Main "~~/src/HOL/Library/Numeral_Type" "~~/src/HOL/Word/Type_Length"
+begin
+
+subsection {* The type of saturated naturals *}
+
+typedef (open) ('a::len) sat = "{.. len_of TYPE('a)}"
+ morphisms nat_of Abs_sat
+ by auto
+
+lemma sat_eqI:
+ "nat_of m = nat_of n \<Longrightarrow> m = n"
+ by (simp add: nat_of_inject)
+
+lemma sat_eq_iff:
+ "m = n \<longleftrightarrow> nat_of m = nat_of n"
+ by (simp add: nat_of_inject)
+
+lemma Abs_sa_nat_of [code abstype]:
+ "Abs_sat (nat_of n) = n"
+ by (fact nat_of_inverse)
+
+definition Sat :: "nat \<Rightarrow> 'a::len sat" where
+ "Sat n = Abs_sat (min (len_of TYPE('a)) n)"
+
+lemma nat_of_Sat [simp]:
+ "nat_of (Sat n :: ('a::len) sat) = min (len_of TYPE('a)) n"
+ unfolding Sat_def by (rule Abs_sat_inverse) simp
+
+lemma nat_of_le_len_of [simp]:
+ "nat_of (n :: ('a::len) sat) \<le> len_of TYPE('a)"
+ using nat_of [where x = n] by simp
+
+lemma min_len_of_nat_of [simp]:
+ "min (len_of TYPE('a)) (nat_of (n::('a::len) sat)) = nat_of n"
+ by (rule min_max.inf_absorb2 [OF nat_of_le_len_of])
+
+lemma min_nat_of_len_of [simp]:
+ "min (nat_of (n::('a::len) sat)) (len_of TYPE('a)) = nat_of n"
+ by (subst min_max.inf.commute) simp
+
+lemma Sat_nat_of [simp]:
+ "Sat (nat_of n) = n"
+ by (simp add: Sat_def nat_of_inverse)
+
+instantiation sat :: (len) linorder
+begin
+
+definition
+ less_eq_sat_def: "x \<le> y \<longleftrightarrow> nat_of x \<le> nat_of y"
+
+definition
+ less_sat_def: "x < y \<longleftrightarrow> nat_of x < nat_of y"
+
+instance
+by default (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min_max.le_infI1 nat_mult_commute)
+
+end
+
+instantiation sat :: (len) "{minus, comm_semiring_0, comm_semiring_1}"
+begin
+
+definition
+ "0 = Sat 0"
+
+definition
+ "1 = Sat 1"
+
+lemma nat_of_zero_sat [simp, code abstract]:
+ "nat_of 0 = 0"
+ by (simp add: zero_sat_def)
+
+lemma nat_of_one_sat [simp, code abstract]:
+ "nat_of 1 = min 1 (len_of TYPE('a))"
+ by (simp add: one_sat_def)
+
+definition
+ "x + y = Sat (nat_of x + nat_of y)"
+
+lemma nat_of_plus_sat [simp, code abstract]:
+ "nat_of (x + y) = min (nat_of x + nat_of y) (len_of TYPE('a))"
+ by (simp add: plus_sat_def)
+
+definition
+ "x - y = Sat (nat_of x - nat_of y)"
+
+lemma nat_of_minus_sat [simp, code abstract]:
+ "nat_of (x - y) = nat_of x - nat_of y"
+proof -
+ from nat_of_le_len_of [of x] have "nat_of x - nat_of y \<le> len_of TYPE('a)" by arith
+ then show ?thesis by (simp add: minus_sat_def)
+qed
+
+definition
+ "x * y = Sat (nat_of x * nat_of y)"
+
+lemma nat_of_times_sat [simp, code abstract]:
+ "nat_of (x * y) = min (nat_of x * nat_of y) (len_of TYPE('a))"
+ by (simp add: times_sat_def)
+
+instance proof
+ fix a b c :: "('a::len) sat"
+ show "a * b * c = a * (b * c)"
+ proof(cases "a = 0")
+ case True thus ?thesis by (simp add: sat_eq_iff)
+ next
+ case False show ?thesis
+ proof(cases "c = 0")
+ case True thus ?thesis by (simp add: sat_eq_iff)
+ next
+ case False with `a \<noteq> 0` show ?thesis
+ by (simp add: sat_eq_iff nat_mult_min_left nat_mult_min_right mult_assoc min_max.inf_assoc min_max.inf_absorb2)
+ qed
+ qed
+next
+ fix a :: "('a::len) sat"
+ show "1 * a = a"
+ apply (simp add: sat_eq_iff)
+ apply (metis One_nat_def len_gt_0 less_Suc0 less_zeroE linorder_not_less min_max.le_iff_inf min_nat_of_len_of nat_mult_1_right nat_mult_commute)
+ done
+next
+ fix a b c :: "('a::len) sat"
+ show "(a + b) * c = a * c + b * c"
+ proof(cases "c = 0")
+ case True thus ?thesis by (simp add: sat_eq_iff)
+ next
+ case False thus ?thesis
+ by (simp add: sat_eq_iff nat_mult_min_left add_mult_distrib nat_add_min_left nat_add_min_right min_max.inf_assoc min_max.inf_absorb2)
+ qed
+qed (simp_all add: sat_eq_iff mult.commute)
+
+end
+
+instantiation sat :: (len) ordered_comm_semiring
+begin
+
+instance
+by default (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min_max.le_infI1 nat_mult_commute)
+
+end
+
+instantiation sat :: (len) number
+begin
+
+definition
+ number_of_sat_def [code del]: "number_of = Sat \<circ> nat"
+
+instance ..
+
+end
+
+lemma [code abstract]:
+ "nat_of (number_of n :: ('a::len) sat) = min (nat n) (len_of TYPE('a))"
+ unfolding number_of_sat_def by simp
+
+instance sat :: (len) finite
+proof
+ show "finite (UNIV::'a sat set)"
+ unfolding type_definition.univ [OF type_definition_sat]
+ using finite by simp
+qed
+
+instantiation sat :: (len) equal
+begin
+
+definition
+ "HOL.equal A B \<longleftrightarrow> nat_of A = nat_of B"
+
+instance proof
+qed (simp add: equal_sat_def nat_of_inject)
+
+end
+
+instantiation sat :: (len) "{bounded_lattice, distrib_lattice}"
+begin
+
+definition
+ "(inf :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = min"
+
+definition
+ "(sup :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = max"
+
+definition
+ "bot = (0 :: 'a sat)"
+
+definition
+ "top = Sat (len_of TYPE('a))"
+
+instance proof
+qed (simp_all add: inf_sat_def sup_sat_def bot_sat_def top_sat_def min_max.sup_inf_distrib1,
+ simp_all add: less_eq_sat_def)
+
+end
+
+instantiation sat :: (len) complete_lattice
+begin
+
+definition
+ "Inf (A :: 'a sat set) = fold min top A"
+
+definition
+ "Sup (A :: 'a sat set) = fold max bot A"
+
+instance proof
+ fix x :: "'a sat"
+ fix A :: "'a sat set"
+ note finite
+ moreover assume "x \<in> A"
+ ultimately have "fold min top A \<le> min x top" by (rule min_max.fold_inf_le_inf)
+ then show "Inf A \<le> x" by (simp add: Inf_sat_def)
+next
+ fix z :: "'a sat"
+ fix A :: "'a sat set"
+ note finite
+ moreover assume z: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
+ ultimately have "min z top \<le> fold min top A" by (blast intro: min_max.inf_le_fold_inf)
+ then show "z \<le> Inf A" by (simp add: Inf_sat_def min_def)
+next
+ fix x :: "'a sat"
+ fix A :: "'a sat set"
+ note finite
+ moreover assume "x \<in> A"
+ ultimately have "max x bot \<le> fold max bot A" by (rule min_max.sup_le_fold_sup)
+ then show "x \<le> Sup A" by (simp add: Sup_sat_def)
+next
+ fix z :: "'a sat"
+ fix A :: "'a sat set"
+ note finite
+ moreover assume z: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
+ ultimately have "fold max bot A \<le> max z bot" by (blast intro: min_max.fold_sup_le_sup)
+ then show "Sup A \<le> z" by (simp add: Sup_sat_def max_def bot_unique)
+qed
+
+end
+
+end
--- a/src/HOL/Metis_Examples/Proxies.thy Wed Sep 07 08:13:38 2011 +0200
+++ b/src/HOL/Metis_Examples/Proxies.thy Thu Sep 08 00:35:22 2011 +0200
@@ -58,206 +58,206 @@
lemma "id (op =) x x"
sledgehammer [type_enc = erased, expect = none] (id_apply)
-sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
-sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis (full_types) id_apply)
lemma "id True"
sledgehammer [type_enc = erased, expect = some] (id_apply)
-sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
-sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "\<not> id False"
sledgehammer [type_enc = erased, expect = some] (id_apply)
-sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
-sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "x = id True \<or> x = id False"
sledgehammer [type_enc = erased, expect = some] (id_apply)
-sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
-sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id x = id True \<or> id x = id False"
sledgehammer [type_enc = erased, expect = some] (id_apply)
-sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
-sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
sledgehammer [type_enc = erased, expect = none] ()
sledgehammer [type_enc = poly_args, expect = none] ()
-sledgehammer [type_enc = poly_tags?, expect = some] ()
+sledgehammer [type_enc = poly_tags??, expect = some] ()
sledgehammer [type_enc = poly_tags, expect = some] ()
-sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] ()
-sledgehammer [type_enc = mono_tags?, expect = some] ()
+sledgehammer [type_enc = mono_tags??, expect = some] ()
sledgehammer [type_enc = mono_tags, expect = some] ()
-sledgehammer [type_enc = mono_guards?, expect = some] ()
+sledgehammer [type_enc = mono_guards??, expect = some] ()
sledgehammer [type_enc = mono_guards, expect = some] ()
by (metis (full_types))
lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
sledgehammer [type_enc = erased, expect = some] (id_apply)
-sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
-sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
sledgehammer [type_enc = erased, expect = some] (id_apply)
-sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
-sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
sledgehammer [type_enc = erased, expect = some] (id_apply)
-sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
-sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (a \<and> b) \<Longrightarrow> id a"
sledgehammer [type_enc = erased, expect = some] (id_apply)
-sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
-sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (a \<and> b) \<Longrightarrow> id b"
sledgehammer [type_enc = erased, expect = some] (id_apply)
-sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
-sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
sledgehammer [type_enc = erased, expect = some] (id_apply)
-sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
-sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id a \<Longrightarrow> id (a \<or> b)"
sledgehammer [type_enc = erased, expect = some] (id_apply)
-sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
-sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id b \<Longrightarrow> id (a \<or> b)"
sledgehammer [type_enc = erased, expect = some] (id_apply)
-sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
-sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
sledgehammer [type_enc = erased, expect = some] (id_apply)
-sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
-sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
sledgehammer [type_enc = erased, expect = some] (id_apply)
-sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
-sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
sledgehammer [type_enc = erased, expect = some] (id_apply)
-sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
-sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
--- a/src/HOL/Metis_Examples/Type_Encodings.thy Wed Sep 07 08:13:38 2011 +0200
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy Thu Sep 08 00:35:22 2011 +0200
@@ -25,44 +25,46 @@
val type_encs =
["erased",
"poly_guards",
- "poly_guards_uniform",
+ "poly_guards?",
+ "poly_guards??",
+ "poly_guards@?",
+ "poly_guards!",
+ "poly_guards!!",
+ "poly_guards@!",
"poly_tags",
- "poly_tags_uniform",
+ "poly_tags?",
+ "poly_tags??",
+ "poly_tags@?",
+ "poly_tags!",
+ "poly_tags!!",
+ "poly_tags@!",
"poly_args",
"raw_mono_guards",
- "raw_mono_guards_uniform",
+ "raw_mono_guards?",
+ "raw_mono_guards??",
+ "raw_mono_guards@?",
+ "raw_mono_guards!",
+ "raw_mono_guards!!",
+ "raw_mono_guards@!",
"raw_mono_tags",
- "raw_mono_tags_uniform",
+ "raw_mono_tags?",
+ "raw_mono_tags??",
+ "raw_mono_tags@?",
+ "raw_mono_tags!",
+ "raw_mono_tags!!",
+ "raw_mono_tags@!",
"raw_mono_args",
"mono_guards",
- "mono_guards_uniform",
+ "mono_guards?",
+ "mono_guards??",
+ "mono_guards!",
+ "mono_guards!!",
"mono_tags",
- "mono_tags_uniform",
- "mono_args",
- "poly_guards?",
- "poly_guards_uniform?",
- "poly_tags?",
- "poly_tags_uniform?",
- "raw_mono_guards?",
- "raw_mono_guards_uniform?",
- "raw_mono_tags?",
- "raw_mono_tags_uniform?",
- "mono_guards?",
- "mono_guards_uniform?",
"mono_tags?",
- "mono_tags_uniform?",
- "poly_guards!",
- "poly_guards_uniform!",
- "poly_tags!",
- "poly_tags_uniform!",
- "raw_mono_guards!",
- "raw_mono_guards_uniform!",
- "raw_mono_tags!",
- "raw_mono_tags_uniform!",
- "mono_guards!",
- "mono_guards_uniform!",
+ "mono_tags??",
"mono_tags!",
- "mono_tags_uniform!"]
+ "mono_tags!!",
+ "mono_args"]
fun metis_exhaust_tac ctxt ths =
let
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Sep 07 08:13:38 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Sep 08 00:35:22 2011 +0200
@@ -574,9 +574,10 @@
relevance_override
in
if !reconstructor = "sledgehammer_tac" then
- sledge_tac 0.25 ATP_Systems.z3_tptpN "mono_simple"
- ORELSE' sledge_tac 0.25 ATP_Systems.eN "mono_guards?"
- ORELSE' sledge_tac 0.25 ATP_Systems.spassN "poly_tags_uniform"
+ sledge_tac 0.2 ATP_Systems.z3_tptpN "mono_simple"
+ ORELSE' sledge_tac 0.2 ATP_Systems.eN "mono_guards??"
+ ORELSE' sledge_tac 0.2 ATP_Systems.vampireN "mono_guards??"
+ ORELSE' sledge_tac 0.2 ATP_Systems.spassN "poly_tags"
ORELSE' Metis_Tactic.metis_tac [] ctxt thms
else if !reconstructor = "smt" then
SMT_Solver.smt_tac ctxt thms
--- a/src/HOL/Nat.thy Wed Sep 07 08:13:38 2011 +0200
+++ b/src/HOL/Nat.thy Thu Sep 08 00:35:22 2011 +0200
@@ -657,46 +657,6 @@
by (cases m) simp_all
-subsubsection {* @{term min} and @{term max} *}
-
-lemma mono_Suc: "mono Suc"
-by (rule monoI) simp
-
-lemma min_0L [simp]: "min 0 n = (0::nat)"
-by (rule min_leastL) simp
-
-lemma min_0R [simp]: "min n 0 = (0::nat)"
-by (rule min_leastR) simp
-
-lemma min_Suc_Suc [simp]: "min (Suc m) (Suc n) = Suc (min m n)"
-by (simp add: mono_Suc min_of_mono)
-
-lemma min_Suc1:
- "min (Suc n) m = (case m of 0 => 0 | Suc m' => Suc(min n m'))"
-by (simp split: nat.split)
-
-lemma min_Suc2:
- "min m (Suc n) = (case m of 0 => 0 | Suc m' => Suc(min m' n))"
-by (simp split: nat.split)
-
-lemma max_0L [simp]: "max 0 n = (n::nat)"
-by (rule max_leastL) simp
-
-lemma max_0R [simp]: "max n 0 = (n::nat)"
-by (rule max_leastR) simp
-
-lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc(max m n)"
-by (simp add: mono_Suc max_of_mono)
-
-lemma max_Suc1:
- "max (Suc n) m = (case m of 0 => Suc n | Suc m' => Suc(max n m'))"
-by (simp split: nat.split)
-
-lemma max_Suc2:
- "max m (Suc n) = (case m of 0 => Suc n | Suc m' => Suc(max m' n))"
-by (simp split: nat.split)
-
-
subsubsection {* Monotonicity of Addition *}
lemma Suc_pred [simp]: "n>0 ==> Suc (n - Suc 0) = n"
@@ -753,11 +713,85 @@
fix a::nat and b::nat show "a ~= 0 \<Longrightarrow> b ~= 0 \<Longrightarrow> a * b ~= 0" by auto
qed
-lemma nat_mult_1: "(1::nat) * n = n"
-by simp
+
+subsubsection {* @{term min} and @{term max} *}
+
+lemma mono_Suc: "mono Suc"
+by (rule monoI) simp
+
+lemma min_0L [simp]: "min 0 n = (0::nat)"
+by (rule min_leastL) simp
+
+lemma min_0R [simp]: "min n 0 = (0::nat)"
+by (rule min_leastR) simp
+
+lemma min_Suc_Suc [simp]: "min (Suc m) (Suc n) = Suc (min m n)"
+by (simp add: mono_Suc min_of_mono)
+
+lemma min_Suc1:
+ "min (Suc n) m = (case m of 0 => 0 | Suc m' => Suc(min n m'))"
+by (simp split: nat.split)
+
+lemma min_Suc2:
+ "min m (Suc n) = (case m of 0 => 0 | Suc m' => Suc(min m' n))"
+by (simp split: nat.split)
+
+lemma max_0L [simp]: "max 0 n = (n::nat)"
+by (rule max_leastL) simp
+
+lemma max_0R [simp]: "max n 0 = (n::nat)"
+by (rule max_leastR) simp
+
+lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc(max m n)"
+by (simp add: mono_Suc max_of_mono)
+
+lemma max_Suc1:
+ "max (Suc n) m = (case m of 0 => Suc n | Suc m' => Suc(max n m'))"
+by (simp split: nat.split)
+
+lemma max_Suc2:
+ "max m (Suc n) = (case m of 0 => Suc n | Suc m' => Suc(max m' n))"
+by (simp split: nat.split)
-lemma nat_mult_1_right: "n * (1::nat) = n"
-by simp
+lemma nat_add_min_left:
+ fixes m n q :: nat
+ shows "min m n + q = min (m + q) (n + q)"
+ by (simp add: min_def)
+
+lemma nat_add_min_right:
+ fixes m n q :: nat
+ shows "m + min n q = min (m + n) (m + q)"
+ by (simp add: min_def)
+
+lemma nat_mult_min_left:
+ fixes m n q :: nat
+ shows "min m n * q = min (m * q) (n * q)"
+ by (simp add: min_def not_le) (auto dest: mult_right_le_imp_le mult_right_less_imp_less le_less_trans)
+
+lemma nat_mult_min_right:
+ fixes m n q :: nat
+ shows "m * min n q = min (m * n) (m * q)"
+ by (simp add: min_def not_le) (auto dest: mult_left_le_imp_le mult_left_less_imp_less le_less_trans)
+
+lemma nat_add_max_left:
+ fixes m n q :: nat
+ shows "max m n + q = max (m + q) (n + q)"
+ by (simp add: max_def)
+
+lemma nat_add_max_right:
+ fixes m n q :: nat
+ shows "m + max n q = max (m + n) (m + q)"
+ by (simp add: max_def)
+
+lemma nat_mult_max_left:
+ fixes m n q :: nat
+ shows "max m n * q = max (m * q) (n * q)"
+ by (simp add: max_def not_le) (auto dest: mult_right_le_imp_le mult_right_less_imp_less le_less_trans)
+
+lemma nat_mult_max_right:
+ fixes m n q :: nat
+ shows "m * max n q = max (m * n) (m * q)"
+ by (simp add: max_def not_le) (auto dest: mult_left_le_imp_le mult_left_less_imp_less le_less_trans)
subsubsection {* Additional theorems about @{term "op \<le>"} *}
@@ -1700,6 +1734,15 @@
by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
+subsection {* aliasses *}
+
+lemma nat_mult_1: "(1::nat) * n = n"
+ by simp
+
+lemma nat_mult_1_right: "n * (1::nat) = n"
+ by simp
+
+
subsection {* size of a datatype value *}
class size =
--- a/src/HOL/Nominal/Nominal.thy Wed Sep 07 08:13:38 2011 +0200
+++ b/src/HOL/Nominal/Nominal.thy Thu Sep 08 00:35:22 2011 +0200
@@ -50,7 +50,7 @@
perm_nprod \<equiv> "perm :: 'x prm \<Rightarrow> ('a, 'b) nprod \<Rightarrow> ('a, 'b) nprod" (unchecked)
begin
-definition
+definition perm_fun :: "'x prm \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
"perm_fun pi f = (\<lambda>x. pi \<bullet> f (rev pi \<bullet> x))"
definition perm_bool :: "'x prm \<Rightarrow> bool \<Rightarrow> bool" where
@@ -2262,7 +2262,7 @@
and at: "at TYPE('x)"
shows "pi\<bullet>(X_to_Un_supp X) = ((X_to_Un_supp (pi\<bullet>X))::'x set)"
apply(simp add: X_to_Un_supp_def)
- apply(simp add: UNION_f_eqvt[OF pt, OF at] perm_fun_def [where 'd="'x set"])
+ apply(simp add: UNION_f_eqvt[OF pt, OF at] perm_fun_def [where 'b="'x set"])
apply(simp add: pt_perm_supp[OF pt, OF at])
apply(simp add: pt_pi_rev[OF pt, OF at])
done
--- a/src/HOL/Tools/ATP/atp_problem.ML Wed Sep 07 08:13:38 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Thu Sep 08 00:35:22 2011 +0200
@@ -236,6 +236,12 @@
| string_for_kind Hypothesis = "hypothesis"
| string_for_kind Conjecture = "conjecture"
+fun string_for_app format func args =
+ if is_format_thf format then
+ "(" ^ space_implode (" " ^ tptp_app ^ " ") (func :: args) ^ ")"
+ else
+ func ^ "(" ^ commas args ^ ")"
+
fun flatten_type (ATyAbs (tys, ty)) = ATyAbs (tys, flatten_type ty)
| flatten_type (ty as AFun (ty1 as AType _, ty2)) =
(case flatten_type ty2 of
@@ -247,16 +253,17 @@
| flatten_type _ =
raise Fail "unexpected higher-order type in first-order format"
-fun str_for_type ty =
+fun str_for_type format ty =
let
fun str _ (AType (s, [])) = s
| str _ (AType (s, tys)) =
- tys |> map (str false)
- |> (if s = tptp_product_type then
- space_implode (" " ^ tptp_product_type ^ " ")
- #> length tys > 1 ? enclose "(" ")"
- else
- commas #> enclose "(" ")" #> prefix s)
+ let val ss = tys |> map (str false) in
+ if s = tptp_product_type then
+ ss |> space_implode (" " ^ tptp_product_type ^ " ")
+ |> length ss > 1 ? enclose "(" ")"
+ else
+ string_for_app format s ss
+ end
| str rhs (AFun (ty1, ty2)) =
str false ty1 ^ " " ^ tptp_fun_type ^ " " ^ str true ty2
|> not rhs ? enclose "(" ")"
@@ -266,8 +273,8 @@
ss) ^ "]: " ^ str false ty
in str true ty end
-fun string_for_type (THF _) ty = str_for_type ty
- | string_for_type (TFF _) ty = str_for_type (flatten_type ty)
+fun string_for_type (format as THF _) ty = str_for_type format ty
+ | string_for_type (format as TFF _) ty = str_for_type format (flatten_type ty)
| string_for_type _ _ = raise Fail "unexpected type in untyped format"
fun string_for_quantifier AForall = tptp_forall
@@ -293,35 +300,27 @@
fun string_for_term _ (ATerm (s, [])) = s
| string_for_term format (ATerm (s, ts)) =
- if s = tptp_empty_list then
- (* used for lists in the optional "source" field of a derivation *)
- "[" ^ commas (map (string_for_term format) ts) ^ "]"
- else if is_tptp_equal s then
- space_implode (" " ^ tptp_equal ^ " ") (map (string_for_term format) ts)
- |> is_format_thf format ? enclose "(" ")"
- else
- (case (s = tptp_ho_forall orelse s = tptp_ho_exists,
- s = tptp_choice andalso is_format_with_choice format, ts) of
- (true, _, [AAbs ((s', ty), tm)]) =>
- (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever
- possible, to work around LEO-II 1.2.8 parser limitation. *)
- string_for_formula format
- (AQuant (if s = tptp_ho_forall then AForall else AExists,
- [(s', SOME ty)], AAtom tm))
- | (_, true, [AAbs ((s', ty), tm)]) =>
- (* There is code in "ATP_Translate" to ensure that "Eps" is always
- applied to an abstraction. *)
- tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^
- string_for_term format tm ^ ""
- |> enclose "(" ")"
-
- | _ =>
- let val ss = map (string_for_term format) ts in
- if is_format_thf format then
- "(" ^ space_implode (" " ^ tptp_app ^ " ") (s :: ss) ^ ")"
- else
- s ^ "(" ^ commas ss ^ ")"
- end)
+ (if s = tptp_empty_list then
+ (* used for lists in the optional "source" field of a derivation *)
+ "[" ^ commas (map (string_for_term format) ts) ^ "]"
+ else if is_tptp_equal s then
+ space_implode (" " ^ tptp_equal ^ " ") (map (string_for_term format) ts)
+ |> is_format_thf format ? enclose "(" ")"
+ else case (s = tptp_ho_forall orelse s = tptp_ho_exists,
+ s = tptp_choice andalso is_format_with_choice format, ts) of
+ (true, _, [AAbs ((s', ty), tm)]) =>
+ (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever
+ possible, to work around LEO-II 1.2.8 parser limitation. *)
+ string_for_formula format
+ (AQuant (if s = tptp_ho_forall then AForall else AExists,
+ [(s', SOME ty)], AAtom tm))
+ | (_, true, [AAbs ((s', ty), tm)]) =>
+ (* There is code in "ATP_Translate" to ensure that "Eps" is always
+ applied to an abstraction. *)
+ tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^
+ string_for_term format tm ^ ""
+ |> enclose "(" ")"
+ | _ => string_for_app format s (map (string_for_term format) ts))
| string_for_term (format as THF _) (AAbs ((s, ty), tm)) =
"(^[" ^ s ^ " : " ^ string_for_type format ty ^ "]: " ^
string_for_term format tm ^ ")"
--- a/src/HOL/Tools/ATP/atp_proof.ML Wed Sep 07 08:13:38 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Sep 08 00:35:22 2011 +0200
@@ -92,9 +92,6 @@
InternalError |
UnknownError of string
-fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
-val strip_spaces_except_between_ident_chars = strip_spaces true is_ident_char
-
fun elide_string threshold s =
if size s > threshold then
String.extract (s, 0, SOME (threshold div 2 - 5)) ^ " ...... " ^
@@ -475,7 +472,7 @@
fun parse_line problem spass_names =
parse_tstp_line problem || parse_spass_line spass_names
fun parse_proof problem spass_names tstp =
- tstp |> strip_spaces_except_between_ident_chars
+ tstp |> strip_spaces_except_between_idents
|> raw_explode
|> Scan.finite Symbol.stopper
(Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Sep 07 08:13:38 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Thu Sep 08 00:35:22 2011 +0200
@@ -21,7 +21,7 @@
datatype play =
Played of reconstructor * Time.time |
- Trust_Playable of reconstructor * Time.time option|
+ Trust_Playable of reconstructor * Time.time option |
Failed_to_Play of reconstructor
type minimize_command = string list -> string
@@ -41,8 +41,8 @@
val make_tvar : string -> typ
val make_tfree : Proof.context -> string -> typ
val term_from_atp :
- Proof.context -> bool -> int Symtab.table -> typ option -> (string, string) ho_term
- -> term
+ Proof.context -> bool -> int Symtab.table -> typ option
+ -> (string, string) ho_term -> term
val prop_from_atp :
Proof.context -> bool -> int Symtab.table
-> (string, string, (string, string) ho_term) formula -> term
@@ -152,7 +152,7 @@
union (op =) (resolve_fact facts_offset fact_names name)
| add_fact ctxt _ _ (Inference (_, _, deps)) =
if AList.defined (op =) deps leo2_ext then
- insert (op =) (ext_name ctxt, Extensionality)
+ insert (op =) (ext_name ctxt, General)
else
I
| add_fact _ _ _ _ = I
@@ -360,10 +360,10 @@
val var_index = if textual then 0 else 1
fun do_term extra_ts opt_T u =
case u of
- ATerm (a, us) =>
- if String.isPrefix simple_type_prefix a then
+ ATerm (s, us) =>
+ if String.isPrefix simple_type_prefix s then
@{const True} (* ignore TPTP type information *)
- else if a = tptp_equal then
+ else if s = tptp_equal then
let val ts = map (do_term [] NONE) us in
if textual andalso length ts = 2 andalso
hd ts aconv List.last ts then
@@ -372,10 +372,11 @@
else
list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
end
- else case strip_prefix_and_unascii const_prefix a of
- SOME s =>
+ else case strip_prefix_and_unascii const_prefix s of
+ SOME s' =>
let
- val ((s', s), mangled_us) = s |> unmangled_const |>> `invert_const
+ val ((s', s''), mangled_us) =
+ s' |> unmangled_const |>> `invert_const
in
if s' = type_tag_name then
case mangled_us @ us of
@@ -396,7 +397,7 @@
@{const True} (* ignore type predicates *)
else
let
- val new_skolem = String.isPrefix new_skolem_const_prefix s
+ val new_skolem = String.isPrefix new_skolem_const_prefix s''
val num_ty_args =
length us - the_default 0 (Symtab.lookup sym_tab s)
val (type_us, term_us) =
@@ -422,7 +423,7 @@
| NONE => HOLogic.typeT))
val t =
if new_skolem then
- Var ((new_skolem_var_name_from_const s, var_index), T)
+ Var ((new_skolem_var_name_from_const s'', var_index), T)
else
Const (unproxify_const s', T)
in list_comb (t, term_ts @ extra_ts) end
@@ -432,15 +433,15 @@
val ts = map (do_term [] NONE) us @ extra_ts
val T = map slack_fastype_of ts ---> HOLogic.typeT
val t =
- case strip_prefix_and_unascii fixed_var_prefix a of
- SOME b =>
+ case strip_prefix_and_unascii fixed_var_prefix s of
+ SOME s =>
(* FIXME: reconstruction of lambda-lifting *)
- Free (b, T)
+ Free (s, T)
| NONE =>
- case strip_prefix_and_unascii schematic_var_prefix a of
- SOME b => Var ((b, var_index), T)
+ case strip_prefix_and_unascii schematic_var_prefix s of
+ SOME s => Var ((s, var_index), T)
| NONE =>
- Var ((a |> textual ? repair_variable_name Char.toLower,
+ Var ((s |> textual ? repair_variable_name Char.toLower,
var_index), T)
in list_comb (t, ts) end
in do_term [] end
@@ -627,7 +628,8 @@
| add_desired_line isar_shrink_factor conjecture_shape fact_names frees
(Inference (name, t, deps)) (j, lines) =
(j + 1,
- if is_fact fact_names name orelse is_conjecture conjecture_shape name orelse
+ if is_fact fact_names name orelse
+ is_conjecture conjecture_shape name orelse
(* the last line must be kept *)
j = 0 orelse
(not (is_only_type_information t) andalso
--- a/src/HOL/Tools/ATP/atp_systems.ML Wed Sep 07 08:13:38 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Sep 08 00:35:22 2011 +0200
@@ -222,11 +222,11 @@
let val method = effective_e_weight_method ctxt in
(* FUDGE *)
if method = e_smartN then
- [(0.333, (true, (500, FOF, "mono_tags?", e_fun_weightN))),
- (0.334, (true, (50, FOF, "mono_guards?", e_fun_weightN))),
- (0.333, (true, (1000, FOF, "mono_tags?", e_sym_offset_weightN)))]
+ [(0.333, (true, (500, FOF, "mono_tags??", e_fun_weightN))),
+ (0.334, (true, (50, FOF, "mono_guards??", e_fun_weightN))),
+ (0.333, (true, (1000, FOF, "mono_tags??", e_sym_offset_weightN)))]
else
- [(1.0, (true, (500, FOF, "mono_tags?", method)))]
+ [(1.0, (true, (500, FOF, "mono_tags??", method)))]
end}
val e = (eN, e_config)
@@ -304,9 +304,9 @@
prem_kind = Conjecture,
best_slices = fn ctxt =>
(* FUDGE *)
- [(0.333, (false, (150, FOF, "mono_tags", sosN))),
- (0.333, (false, (300, FOF, "poly_tags?", sosN))),
- (0.334, (true, (50, FOF, "mono_tags?", no_sosN)))]
+ [(0.333, (false, (150, FOF, "mono_tags??", sosN))),
+ (0.333, (false, (300, FOF, "poly_tags??", sosN))),
+ (0.334, (true, (50, FOF, "mono_tags??", no_sosN)))]
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}
@@ -349,11 +349,11 @@
best_slices = fn ctxt =>
(* FUDGE *)
(if is_old_vampire_version () then
- [(0.333, (false, (150, FOF, "poly_guards", sosN))),
- (0.333, (false, (500, FOF, "mono_tags?", sosN))),
- (0.334, (true, (50, FOF, "mono_guards?", no_sosN)))]
+ [(0.333, (false, (150, FOF, "poly_guards??", sosN))),
+ (0.333, (false, (500, FOF, "mono_tags??", sosN))),
+ (0.334, (true, (50, FOF, "mono_guards??", no_sosN)))]
else
- [(0.333, (false, (150, vampire_tff0, "poly_guards", sosN))),
+ [(0.333, (false, (150, vampire_tff0, "poly_guards??", sosN))),
(0.333, (false, (500, vampire_tff0, "mono_simple", sosN))),
(0.334, (true, (50, vampire_tff0, "mono_simple", no_sosN)))])
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
@@ -403,11 +403,11 @@
prem_kind = Hypothesis,
best_slices = K [(1.0, (false, (200, format, type_enc, "")))]}
-val pff_format = TFF (TPTP_Polymorphic, TPTP_Implicit)
+val pff_format = TFF (TPTP_Polymorphic, TPTP_Explicit)
val pff_config = dummy_config pff_format "poly_simple"
val pff = (pffN, pff_config)
-val phf_format = THF (TPTP_Polymorphic, TPTP_Implicit, THF_With_Choice)
+val phf_format = THF (TPTP_Polymorphic, TPTP_Explicit, THF_With_Choice)
val phf_config = dummy_config phf_format "poly_simple_higher"
val phf = (phfN, phf_config)
@@ -490,7 +490,7 @@
val remote_e =
remotify_atp e "EP" ["1.0", "1.1", "1.2"]
- (K (750, FOF, "mono_tags?") (* FUDGE *))
+ (K (750, FOF, "mono_tags??") (* FUDGE *))
val remote_leo2 =
remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
(K (100, leo2_thf0, "mono_simple_higher") (* FUDGE *))
@@ -499,13 +499,13 @@
(K (100, satallax_thf0, "mono_simple_higher") (* FUDGE *))
val remote_vampire =
remotify_atp vampire "Vampire" ["1.8"]
- (K (250, FOF, "mono_guards?") (* FUDGE *))
+ (K (250, FOF, "mono_guards??") (* FUDGE *))
val remote_z3_tptp =
remotify_atp z3_tptp "Z3" ["3.0"]
(K (250, z3_tff0, "mono_simple") (* FUDGE *))
val remote_e_sine =
remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
- Conjecture (K (500, FOF, "mono_guards?") (* FUDGE *))
+ Conjecture (K (500, FOF, "mono_guards??") (* FUDGE *))
val remote_snark =
remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
[("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
@@ -519,7 +519,7 @@
[(OutOfResources, "Too many function symbols"),
(Crashed, "Unrecoverable Segmentation Fault")]
Hypothesis Hypothesis
- (K (50, CNF_UEQ, "mono_tags?") (* FUDGE *))
+ (K (50, CNF_UEQ, "mono_tags??") (* FUDGE *))
(* Setup *)
--- a/src/HOL/Tools/ATP/atp_translate.ML Wed Sep 07 08:13:38 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Thu Sep 08 00:35:22 2011 +0200
@@ -16,24 +16,18 @@
type 'a problem = 'a ATP_Problem.problem
datatype locality =
- General | Helper | Induction | Extensionality | Intro | Elim | Simp |
- Local | Assum | Chained
+ General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained
- datatype order = First_Order | Higher_Order
datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
datatype soundness = Sound_Modulo_Infiniteness | Sound
+ datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
datatype type_level =
All_Types |
- Noninf_Nonmono_Types of soundness |
- Fin_Nonmono_Types |
+ Noninf_Nonmono_Types of soundness * granularity |
+ Fin_Nonmono_Types of granularity |
Const_Arg_Types |
No_Types
- datatype type_uniformity = Uniform | Nonuniform
-
- datatype type_enc =
- Simple_Types of order * polymorphism * type_level |
- Guards of polymorphism * type_level * type_uniformity |
- Tags of polymorphism * type_level * type_uniformity
+ type type_enc
val type_tag_idempotence : bool Config.T
val type_tag_arguments : bool Config.T
@@ -86,12 +80,12 @@
val new_skolem_var_name_from_const : string -> string
val atp_irrelevant_consts : string list
val atp_schematic_consts_of : term -> typ list Symtab.table
- val type_enc_from_string : soundness -> string -> type_enc
val is_type_enc_higher_order : type_enc -> bool
val polymorphism_of_type_enc : type_enc -> polymorphism
val level_of_type_enc : type_enc -> type_level
val is_type_enc_quasi_sound : type_enc -> bool
val is_type_enc_fairly_sound : type_enc -> bool
+ val type_enc_from_string : soundness -> string -> type_enc
val adjust_type_enc : tptp_format -> type_enc -> type_enc
val mk_aconns :
connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
@@ -408,7 +402,7 @@
fun multi_arity_clause [] = []
| multi_arity_clause ((tcons, ars) :: tc_arlists) =
- arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
+ arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
(* Generate all pairs (tycon, class, sorts) such that tycon belongs to class in
theory thy provided its arguments have the corresponding sorts. *)
@@ -531,28 +525,76 @@
in (IAbs ((name, T), tm), union (op =) atomic_Ts (atyps_of T)) end
datatype locality =
- General | Helper | Induction | Extensionality | Intro | Elim | Simp |
- Local | Assum | Chained
+ General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained
datatype order = First_Order | Higher_Order
datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
datatype soundness = Sound_Modulo_Infiniteness | Sound
+datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
datatype type_level =
All_Types |
- Noninf_Nonmono_Types of soundness |
- Fin_Nonmono_Types |
+ Noninf_Nonmono_Types of soundness * granularity |
+ Fin_Nonmono_Types of granularity |
Const_Arg_Types |
No_Types
-datatype type_uniformity = Uniform | Nonuniform
datatype type_enc =
Simple_Types of order * polymorphism * type_level |
- Guards of polymorphism * type_level * type_uniformity |
- Tags of polymorphism * type_level * type_uniformity
+ Guards of polymorphism * type_level |
+ Tags of polymorphism * type_level
+
+fun is_type_enc_higher_order (Simple_Types (Higher_Order, _, _)) = true
+ | is_type_enc_higher_order _ = false
+
+fun polymorphism_of_type_enc (Simple_Types (_, poly, _)) = poly
+ | polymorphism_of_type_enc (Guards (poly, _)) = poly
+ | polymorphism_of_type_enc (Tags (poly, _)) = poly
+
+fun level_of_type_enc (Simple_Types (_, _, level)) = level
+ | level_of_type_enc (Guards (_, level)) = level
+ | level_of_type_enc (Tags (_, level)) = level
+
+fun granularity_of_type_level (Noninf_Nonmono_Types (_, grain)) = grain
+ | granularity_of_type_level (Fin_Nonmono_Types grain) = grain
+ | granularity_of_type_level _ = All_Vars
+
+fun is_type_level_quasi_sound All_Types = true
+ | is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true
+ | is_type_level_quasi_sound _ = false
+val is_type_enc_quasi_sound = is_type_level_quasi_sound o level_of_type_enc
+
+fun is_type_level_fairly_sound (Fin_Nonmono_Types _) = true
+ | is_type_level_fairly_sound level = is_type_level_quasi_sound level
+val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
+
+fun is_type_level_monotonicity_based (Noninf_Nonmono_Types _) = true
+ | is_type_level_monotonicity_based (Fin_Nonmono_Types _) = true
+ | is_type_level_monotonicity_based _ = false
+
+(* "_query", "_bang", and "_at" are for the ASCII-challenged Metis and
+ Mirabelle. *)
+val queries = ["?", "_query"]
+val bangs = ["!", "_bang"]
+val ats = ["@", "_at"]
fun try_unsuffixes ss s =
fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
+fun try_nonmono constr suffixes fallback s =
+ case try_unsuffixes suffixes s of
+ SOME s =>
+ (case try_unsuffixes suffixes s of
+ SOME s => (constr Positively_Naked_Vars, s)
+ | NONE =>
+ case try_unsuffixes ats s of
+ SOME s => (constr Ghost_Type_Arg_Vars, s)
+ | NONE => (constr All_Vars, s))
+ | NONE => fallback s
+
+fun is_incompatible_type_level poly level =
+ poly = Mangled_Monomorphic andalso
+ granularity_of_type_level level = Ghost_Type_Arg_Vars
+
fun type_enc_from_string soundness s =
(case try (unprefix "poly_") s of
SOME s => (SOME Polymorphic, s)
@@ -563,75 +605,44 @@
case try (unprefix "mono_") s of
SOME s => (SOME Mangled_Monomorphic, s)
| NONE => (NONE, s))
- ||> (fn s =>
- (* "_query" and "_bang" are for the ASCII-challenged Metis and
- Mirabelle. *)
- case try_unsuffixes ["?", "_query"] s of
- SOME s => (Noninf_Nonmono_Types soundness, s)
- | NONE =>
- case try_unsuffixes ["!", "_bang"] s of
- SOME s => (Fin_Nonmono_Types, s)
- | NONE => (All_Types, s))
- ||> apsnd (fn s =>
- case try (unsuffix "_uniform") s of
- SOME s => (Uniform, s)
- | NONE => (Nonuniform, s))
- |> (fn (poly, (level, (uniformity, core))) =>
- case (core, (poly, level, uniformity)) of
- ("simple", (SOME poly, _, Nonuniform)) =>
+ ||> (pair All_Types
+ |> try_nonmono Fin_Nonmono_Types bangs
+ |> try_nonmono (curry Noninf_Nonmono_Types soundness) queries)
+ |> (fn (poly, (level, core)) =>
+ case (core, (poly, level)) of
+ ("simple", (SOME poly, _)) =>
(case (poly, level) of
(Polymorphic, All_Types) =>
Simple_Types (First_Order, Polymorphic, All_Types)
| (Mangled_Monomorphic, _) =>
- Simple_Types (First_Order, Mangled_Monomorphic, level)
+ if granularity_of_type_level level = All_Vars then
+ Simple_Types (First_Order, Mangled_Monomorphic, level)
+ else
+ raise Same.SAME
| _ => raise Same.SAME)
- | ("simple_higher", (SOME poly, _, Nonuniform)) =>
+ | ("simple_higher", (SOME poly, _)) =>
(case (poly, level) of
(Polymorphic, All_Types) =>
Simple_Types (Higher_Order, Polymorphic, All_Types)
| (_, Noninf_Nonmono_Types _) => raise Same.SAME
| (Mangled_Monomorphic, _) =>
- Simple_Types (Higher_Order, Mangled_Monomorphic, level)
+ if granularity_of_type_level level = All_Vars then
+ Simple_Types (Higher_Order, Mangled_Monomorphic, level)
+ else
+ raise Same.SAME
| _ => raise Same.SAME)
- | ("guards", (SOME poly, _, _)) => Guards (poly, level, uniformity)
- | ("tags", (SOME Polymorphic, _, _)) =>
- Tags (Polymorphic, level, uniformity)
- | ("tags", (SOME poly, _, _)) => Tags (poly, level, uniformity)
- | ("args", (SOME poly, All_Types (* naja *), Nonuniform)) =>
- Guards (poly, Const_Arg_Types, Nonuniform)
- | ("erased", (NONE, All_Types (* naja *), Nonuniform)) =>
- Guards (Polymorphic, No_Types, Nonuniform)
+ | ("guards", (SOME poly, _)) =>
+ if is_incompatible_type_level poly level then raise Same.SAME
+ else Guards (poly, level)
+ | ("tags", (SOME poly, _)) =>
+ if is_incompatible_type_level poly level then raise Same.SAME
+ else Tags (poly, level)
+ | ("args", (SOME poly, All_Types (* naja *))) =>
+ Guards (poly, Const_Arg_Types)
+ | ("erased", (NONE, All_Types (* naja *))) =>
+ Guards (Polymorphic, No_Types)
| _ => raise Same.SAME)
- handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
-
-fun is_type_enc_higher_order (Simple_Types (Higher_Order, _, _)) = true
- | is_type_enc_higher_order _ = false
-
-fun polymorphism_of_type_enc (Simple_Types (_, poly, _)) = poly
- | polymorphism_of_type_enc (Guards (poly, _, _)) = poly
- | polymorphism_of_type_enc (Tags (poly, _, _)) = poly
-
-fun level_of_type_enc (Simple_Types (_, _, level)) = level
- | level_of_type_enc (Guards (_, level, _)) = level
- | level_of_type_enc (Tags (_, level, _)) = level
-
-fun uniformity_of_type_enc (Simple_Types _) = Uniform
- | uniformity_of_type_enc (Guards (_, _, uniformity)) = uniformity
- | uniformity_of_type_enc (Tags (_, _, uniformity)) = uniformity
-
-fun is_type_level_quasi_sound All_Types = true
- | is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true
- | is_type_level_quasi_sound _ = false
-val is_type_enc_quasi_sound =
- is_type_level_quasi_sound o level_of_type_enc
-
-fun is_type_level_fairly_sound level =
- is_type_level_quasi_sound level orelse level = Fin_Nonmono_Types
-val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
-
-fun is_type_level_monotonicity_based (Noninf_Nonmono_Types _) = true
- | is_type_level_monotonicity_based Fin_Nonmono_Types = true
- | is_type_level_monotonicity_based _ = false
+ handle Same.SAME => error ("Unknown type encoding: " ^ quote s ^ ".")
fun adjust_type_enc (THF (TPTP_Monomorphic, _, _))
(Simple_Types (order, _, level)) =
@@ -642,7 +653,7 @@
| adjust_type_enc (TFF _) (Simple_Types (_, poly, level)) =
Simple_Types (First_Order, poly, level)
| adjust_type_enc format (Simple_Types (_, poly, level)) =
- adjust_type_enc format (Guards (poly, level, Uniform))
+ adjust_type_enc format (Guards (poly, level))
| adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =
(if is_type_enc_fairly_sound type_enc then Tags else Guards) stuff
| adjust_type_enc _ type_enc = type_enc
@@ -693,34 +704,28 @@
(* The Booleans indicate whether all type arguments should be kept. *)
datatype type_arg_policy =
Explicit_Type_Args of bool |
- Mangled_Type_Args of bool |
+ Mangled_Type_Args |
No_Type_Args
-fun should_drop_arg_type_args (Simple_Types _) = false
- | should_drop_arg_type_args type_enc =
- level_of_type_enc type_enc = All_Types andalso
- uniformity_of_type_enc type_enc = Uniform
-
fun type_arg_policy type_enc s =
- if s = type_tag_name then
- (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
- Mangled_Type_Args
- else
- Explicit_Type_Args) false
- else case type_enc of
- Tags (_, All_Types, Uniform) => No_Type_Args
- | _ =>
- let val level = level_of_type_enc type_enc in
- if level = No_Types orelse s = @{const_name HOL.eq} orelse
- (s = app_op_name andalso level = Const_Arg_Types) then
- No_Type_Args
- else
- should_drop_arg_type_args type_enc
- |> (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
- Mangled_Type_Args
- else
- Explicit_Type_Args)
- end
+ let val mangled = (polymorphism_of_type_enc type_enc = Mangled_Monomorphic) in
+ if s = type_tag_name then
+ if mangled then Mangled_Type_Args else Explicit_Type_Args false
+ else case type_enc of
+ Tags (_, All_Types) => No_Type_Args
+ | _ =>
+ let val level = level_of_type_enc type_enc in
+ if level = No_Types orelse s = @{const_name HOL.eq} orelse
+ (s = app_op_name andalso level = Const_Arg_Types) then
+ No_Type_Args
+ else if mangled then
+ Mangled_Type_Args
+ else
+ Explicit_Type_Args
+ (level = All_Types orelse
+ granularity_of_type_level level = Ghost_Type_Arg_Vars)
+ end
+ end
(* Make atoms for sorted type variables. *)
fun generic_add_sorts_on_type (_, []) = I
@@ -900,7 +905,7 @@
(hd ss, map unmangled_type (tl ss))
end
-fun introduce_proxies type_enc =
+fun introduce_proxies_in_iterm type_enc =
let
fun tweak_ho_quant ho_quant T [IAbs _] = IConst (`I ho_quant, T, [])
| tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _]))
@@ -949,11 +954,79 @@
| intro _ _ tm = tm
in intro true [] end
-fun iformula_from_prop thy format type_enc eq_as_iff =
+fun mangle_type_args_in_iterm format type_enc =
+ if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
+ let
+ fun mangle (IApp (tm1, tm2)) = IApp (mangle tm1, mangle tm2)
+ | mangle (tm as IConst (_, _, [])) = tm
+ | mangle (tm as IConst (name as (s, _), T, T_args)) =
+ (case strip_prefix_and_unascii const_prefix s of
+ NONE => tm
+ | SOME s'' =>
+ case type_arg_policy type_enc (invert_const s'') of
+ Mangled_Type_Args =>
+ IConst (mangled_const_name format type_enc T_args name, T, [])
+ | _ => tm)
+ | mangle (IAbs (bound, tm)) = IAbs (bound, mangle tm)
+ | mangle tm = tm
+ in mangle end
+ else
+ I
+
+fun chop_fun 0 T = ([], T)
+ | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
+ chop_fun (n - 1) ran_T |>> cons dom_T
+ | chop_fun _ T = ([], T)
+
+fun filter_const_type_args _ _ _ [] = []
+ | filter_const_type_args thy s ary T_args =
+ let
+ val U = robust_const_type thy s
+ val arg_U_vars = fold Term.add_tvarsT (U |> chop_fun ary |> fst) []
+ val U_args = (s, U) |> robust_const_typargs thy
+ in
+ U_args ~~ T_args
+ |> map (fn (U, T) =>
+ if member (op =) arg_U_vars (dest_TVar U) then dummyT else T)
+ end
+ handle TYPE _ => T_args
+
+fun filter_type_args_in_iterm thy type_enc =
let
+ fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2)
+ | filt _ (tm as IConst (_, _, [])) = tm
+ | filt ary (IConst (name as (s, _), T, T_args)) =
+ (case strip_prefix_and_unascii const_prefix s of
+ NONE =>
+ (name,
+ if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then
+ []
+ else
+ T_args)
+ | SOME s'' =>
+ let
+ val s'' = invert_const s''
+ fun filter_T_args false = T_args
+ | filter_T_args true = filter_const_type_args thy s'' ary T_args
+ in
+ case type_arg_policy type_enc s'' of
+ Explicit_Type_Args drop_args => (name, filter_T_args drop_args)
+ | No_Type_Args => (name, [])
+ | Mangled_Type_Args => raise Fail "unexpected (un)mangled symbol"
+ end)
+ |> (fn (name, T_args) => IConst (name, T, T_args))
+ | filt _ (IAbs (bound, tm)) = IAbs (bound, filt 0 tm)
+ | filt _ tm = tm
+ in filt 0 end
+
+fun iformula_from_prop ctxt format type_enc eq_as_iff =
+ let
+ val thy = Proof_Context.theory_of ctxt
fun do_term bs t atomic_types =
iterm_from_term thy format bs (Envir.eta_contract t)
- |>> (introduce_proxies type_enc #> AAtom)
+ |>> (introduce_proxies_in_iterm type_enc
+ #> mangle_type_args_in_iterm format type_enc
+ #> AAtom)
||> union (op =) atomic_types
fun do_quant bs q pos s T t' =
let
@@ -1021,28 +1094,31 @@
t
else
let
- fun aux Ts t =
+ fun trans Ts t =
case t of
- @{const Not} $ t1 => @{const Not} $ aux Ts t1
+ @{const Not} $ t1 => @{const Not} $ trans Ts t1
| (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
- t0 $ Abs (s, T, aux (T :: Ts) t')
+ t0 $ Abs (s, T, trans (T :: Ts) t')
| (t0 as Const (@{const_name All}, _)) $ t1 =>
- aux Ts (t0 $ eta_expand Ts t1 1)
+ trans Ts (t0 $ eta_expand Ts t1 1)
| (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
- t0 $ Abs (s, T, aux (T :: Ts) t')
+ t0 $ Abs (s, T, trans (T :: Ts) t')
| (t0 as Const (@{const_name Ex}, _)) $ t1 =>
- aux Ts (t0 $ eta_expand Ts t1 1)
- | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
- | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
- | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ trans Ts (t0 $ eta_expand Ts t1 1)
+ | (t0 as @{const HOL.conj}) $ t1 $ t2 =>
+ t0 $ trans Ts t1 $ trans Ts t2
+ | (t0 as @{const HOL.disj}) $ t1 $ t2 =>
+ t0 $ trans Ts t1 $ trans Ts t2
+ | (t0 as @{const HOL.implies}) $ t1 $ t2 =>
+ t0 $ trans Ts t1 $ trans Ts t2
| (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
$ t1 $ t2 =>
- t0 $ aux Ts t1 $ aux Ts t2
+ t0 $ trans Ts t1 $ trans Ts t2
| _ =>
if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
else t |> Envir.eta_contract |> do_lambdas ctxt Ts
val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
- in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
+ in t |> trans [] |> singleton (Variable.export_terms ctxt' ctxt) end
end
fun do_cheaply_conceal_lambdas Ts (t1 $ t2) =
@@ -1080,12 +1156,12 @@
same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
fun freeze_term t =
let
- fun aux (t $ u) = aux t $ aux u
- | aux (Abs (s, T, t)) = Abs (s, T, aux t)
- | aux (Var ((s, i), T)) =
+ fun freeze (t $ u) = freeze t $ freeze u
+ | freeze (Abs (s, T, t)) = Abs (s, T, freeze t)
+ | freeze (Var ((s, i), T)) =
Free (atp_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
- | aux t = t
- in t |> exists_subterm is_Var t ? aux end
+ | freeze t = t
+ in t |> exists_subterm is_Var t ? freeze end
fun presimp_prop ctxt presimp_consts t =
let
@@ -1103,34 +1179,57 @@
end
(* making fact and conjecture formulas *)
-fun make_formula thy format type_enc eq_as_iff name loc kind t =
+fun make_formula ctxt format type_enc eq_as_iff name loc kind t =
let
val (iformula, atomic_types) =
- iformula_from_prop thy format type_enc eq_as_iff (SOME (kind <> Conjecture)) t []
+ iformula_from_prop ctxt format type_enc eq_as_iff
+ (SOME (kind <> Conjecture)) t []
in
{name = name, locality = loc, kind = kind, iformula = iformula,
atomic_types = atomic_types}
end
fun make_fact ctxt format type_enc eq_as_iff ((name, loc), t) =
- let val thy = Proof_Context.theory_of ctxt in
- case t |> make_formula thy format type_enc (eq_as_iff andalso format <> CNF)
- name loc Axiom of
- formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
- if s = tptp_true then NONE else SOME formula
- | formula => SOME formula
- end
+ case t |> make_formula ctxt format type_enc (eq_as_iff andalso format <> CNF)
+ name loc Axiom of
+ formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
+ if s = tptp_true then NONE else SOME formula
+ | formula => SOME formula
fun s_not_trueprop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
| s_not_trueprop t = s_not t
-fun make_conjecture thy format type_enc =
+fun make_conjecture ctxt format type_enc =
map (fn ((name, loc), (kind, t)) =>
t |> kind = Conjecture ? s_not_trueprop
- |> make_formula thy format type_enc (format <> CNF) name loc kind)
+ |> make_formula ctxt format type_enc (format <> CNF) name loc kind)
(** Finite and infinite type inference **)
+fun tvar_footprint thy s ary =
+ (case strip_prefix_and_unascii const_prefix s of
+ SOME s =>
+ s |> invert_const |> robust_const_type thy |> chop_fun ary |> fst
+ |> map (fn T => Term.add_tvarsT T [] |> map fst)
+ | NONE => [])
+ handle TYPE _ => []
+
+fun ghost_type_args thy s ary =
+ let
+ val footprint = tvar_footprint thy s ary
+ fun ghosts _ [] = []
+ | ghosts seen ((i, tvars) :: args) =
+ ghosts (union (op =) seen tvars) args
+ |> exists (not o member (op =) seen) tvars ? cons i
+ in
+ if forall null footprint then
+ []
+ else
+ 0 upto length footprint - 1 ~~ footprint
+ |> sort (rev_order o list_ord Term_Ord.indexname_ord o pairself snd)
+ |> ghosts []
+ end
+
type monotonicity_info =
{maybe_finite_Ts : typ list,
surely_finite_Ts : typ list,
@@ -1154,24 +1253,25 @@
fun should_encode_type _ (_ : monotonicity_info) All_Types _ = true
| should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
maybe_nonmono_Ts, ...}
- (Noninf_Nonmono_Types soundness) T =
- exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
- not (exists (type_instance ctxt T) surely_infinite_Ts orelse
- (not (member (type_aconv ctxt) maybe_finite_Ts T) andalso
- is_type_kind_of_surely_infinite ctxt soundness surely_infinite_Ts T))
+ (Noninf_Nonmono_Types (soundness, grain)) T =
+ grain = Ghost_Type_Arg_Vars orelse
+ (exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
+ not (exists (type_instance ctxt T) surely_infinite_Ts orelse
+ (not (member (type_aconv ctxt) maybe_finite_Ts T) andalso
+ is_type_kind_of_surely_infinite ctxt soundness surely_infinite_Ts
+ T)))
| should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
maybe_nonmono_Ts, ...}
- Fin_Nonmono_Types T =
- exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
- (exists (type_generalization ctxt T) surely_finite_Ts orelse
- (not (member (type_aconv ctxt) maybe_infinite_Ts T) andalso
- is_type_surely_finite ctxt T))
+ (Fin_Nonmono_Types grain) T =
+ grain = Ghost_Type_Arg_Vars orelse
+ (exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
+ (exists (type_generalization ctxt T) surely_finite_Ts orelse
+ (not (member (type_aconv ctxt) maybe_infinite_Ts T) andalso
+ is_type_surely_finite ctxt T)))
| should_encode_type _ _ _ _ = false
-fun should_guard_type ctxt mono (Guards (_, level, uniformity)) should_guard_var
- T =
- (uniformity = Uniform orelse should_guard_var ()) andalso
- should_encode_type ctxt mono level T
+fun should_guard_type ctxt mono (Guards (_, level)) should_guard_var T =
+ should_guard_var () andalso should_encode_type ctxt mono level T
| should_guard_type _ _ _ _ _ = false
fun is_maybe_universal_var (IConst ((s, _), _, _)) =
@@ -1183,15 +1283,20 @@
datatype tag_site =
Top_Level of bool option |
Eq_Arg of bool option |
+ Arg of string * int |
Elsewhere
fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
- | should_tag_with_type ctxt mono (Tags (_, level, uniformity)) site u T =
- (case uniformity of
- Uniform => should_encode_type ctxt mono level T
- | Nonuniform =>
+ | should_tag_with_type ctxt mono (Tags (_, level)) site u T =
+ (case granularity_of_type_level level of
+ All_Vars => should_encode_type ctxt mono level T
+ | grain =>
case (site, is_maybe_universal_var u) of
(Eq_Arg _, true) => should_encode_type ctxt mono level T
+ | (Arg (s, j), true) =>
+ grain = Ghost_Type_Arg_Vars andalso
+ member (op =)
+ (ghost_type_args (Proof_Context.theory_of ctxt) s (j + 1)) j
| _ => false)
| should_tag_with_type _ _ _ _ _ _ = false
@@ -1211,7 +1316,7 @@
fun add_iterm_syms_to_table ctxt explicit_apply =
let
- fun consider_var_arity const_T var_T max_ary =
+ fun consider_var_ary const_T var_T max_ary =
let
fun iter ary T =
if ary = max_ary orelse type_instance ctxt var_T T orelse
@@ -1225,9 +1330,9 @@
(can dest_funT T orelse T = @{typ bool}) then
let
val bool_vars' = bool_vars orelse body_type T = @{typ bool}
- fun repair_min_arity {pred_sym, min_ary, max_ary, types} =
+ fun repair_min_ary {pred_sym, min_ary, max_ary, types} =
{pred_sym = pred_sym andalso not bool_vars',
- min_ary = fold (fn T' => consider_var_arity T' T) types min_ary,
+ min_ary = fold (fn T' => consider_var_ary T' T) types min_ary,
max_ary = max_ary, types = types}
val fun_var_Ts' =
fun_var_Ts |> can dest_funT T ? insert_type ctxt I T
@@ -1236,7 +1341,7 @@
pointer_eq (fun_var_Ts', fun_var_Ts) then
accum
else
- ((bool_vars', fun_var_Ts'), Symtab.map (K repair_min_arity) sym_tab)
+ ((bool_vars', fun_var_Ts'), Symtab.map (K repair_min_ary) sym_tab)
end
else
accum
@@ -1263,7 +1368,7 @@
pointer_eq (types', types) then
min_ary
else
- fold (consider_var_arity T) fun_var_Ts min_ary
+ fold (consider_var_ary T) fun_var_Ts min_ary
in
Symtab.update (s, {pred_sym = pred_sym,
min_ary = Int.min (ary, min_ary),
@@ -1278,7 +1383,7 @@
case explicit_apply of
SOME true => 0
| SOME false => ary
- | NONE => fold (consider_var_arity T) fun_var_Ts ary
+ | NONE => fold (consider_var_ary T) fun_var_Ts ary
in
Symtab.update_new (s, {pred_sym = pred_sym,
min_ary = min_ary, max_ary = ary,
@@ -1296,23 +1401,23 @@
K (add_iterm_syms_to_table ctxt explicit_apply)
|> formula_fold NONE |> fact_lift
-val default_sym_tab_entries : (string * sym_info) list =
- (prefixed_predicator_name,
- {pred_sym = true, min_ary = 1, max_ary = 1, types = []})
- (* FIXME: needed? *) ::
+fun default_sym_tab_entries type_enc =
(make_fixed_const NONE @{const_name undefined},
- {pred_sym = false, min_ary = 0, max_ary = 0, types = []}) ::
+ {pred_sym = false, min_ary = 0, max_ary = 0, types = []}) ::
([tptp_false, tptp_true]
|> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @
([tptp_equal, tptp_old_equal]
|> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = []}))
+ |> not (is_type_enc_higher_order type_enc)
+ ? cons (prefixed_predicator_name,
+ {pred_sym = true, min_ary = 1, max_ary = 1, types = []})
-fun sym_table_for_facts ctxt explicit_apply facts =
+fun sym_table_for_facts ctxt type_enc explicit_apply facts =
((false, []), Symtab.empty)
|> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd
- |> fold Symtab.update default_sym_tab_entries
+ |> fold Symtab.update (default_sym_tab_entries type_enc)
-fun min_arity_of sym_tab s =
+fun min_ary_of sym_tab s =
case Symtab.lookup sym_tab s of
SOME ({min_ary, ...} : sym_info) => min_ary
| NONE =>
@@ -1336,92 +1441,42 @@
pred_sym andalso min_ary = max_ary
| NONE => false
+val app_op = `(make_fixed_const NONE) app_op_name
val predicator_combconst =
IConst (`(make_fixed_const NONE) predicator_name, @{typ "bool => bool"}, [])
-fun predicator tm = IApp (predicator_combconst, tm)
-
-fun introduce_predicators_in_iterm sym_tab tm =
- case strip_iterm_comb tm of
- (IConst ((s, _), _, _), _) =>
- if is_pred_sym sym_tab s then tm else predicator tm
- | _ => predicator tm
fun list_app head args = fold (curry (IApp o swap)) args head
+fun predicator tm = IApp (predicator_combconst, tm)
-val app_op = `(make_fixed_const NONE) app_op_name
-
-fun explicit_app arg head =
+fun firstorderize_fact thy format type_enc sym_tab =
let
- val head_T = ityp_of head
- val (arg_T, res_T) = dest_funT head_T
- val explicit_app = IConst (app_op, head_T --> head_T, [arg_T, res_T])
- in list_app explicit_app [head, arg] end
-fun list_explicit_app head args = fold explicit_app args head
-
-fun introduce_explicit_apps_in_iterm sym_tab =
- let
- fun aux tm =
+ fun do_app arg head =
+ let
+ val head_T = ityp_of head
+ val (arg_T, res_T) = dest_funT head_T
+ val app =
+ IConst (app_op, head_T --> head_T, [arg_T, res_T])
+ |> mangle_type_args_in_iterm format type_enc
+ in list_app app [head, arg] end
+ fun list_app_ops head args = fold do_app args head
+ fun introduce_app_ops tm =
case strip_iterm_comb tm of
(head as IConst ((s, _), _, _), args) =>
- args |> map aux
- |> chop (min_arity_of sym_tab s)
+ args |> map introduce_app_ops
+ |> chop (min_ary_of sym_tab s)
|>> list_app head
- |-> list_explicit_app
- | (head, args) => list_explicit_app head (map aux args)
- in aux end
-
-fun chop_fun 0 T = ([], T)
- | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
- chop_fun (n - 1) ran_T |>> cons dom_T
- | chop_fun _ _ = raise Fail "unexpected non-function"
-
-fun filter_type_args _ _ _ [] = []
- | filter_type_args thy s arity T_args =
- let
- val U = robust_const_type thy s
- val arg_U_vars = fold Term.add_tvarsT (U |> chop_fun arity |> fst) []
- val U_args = (s, U) |> robust_const_typargs thy
- in
- U_args ~~ T_args
- |> map (fn (U, T) =>
- if member (op =) arg_U_vars (dest_TVar U) then dummyT else T)
- end
- handle TYPE _ => T_args
-
-fun enforce_type_arg_policy_in_iterm ctxt format type_enc =
- let
- val thy = Proof_Context.theory_of ctxt
- fun aux arity (IApp (tm1, tm2)) = IApp (aux (arity + 1) tm1, aux 0 tm2)
- | aux arity (IConst (name as (s, _), T, T_args)) =
- (case strip_prefix_and_unascii const_prefix s of
- NONE =>
- (name, if level_of_type_enc type_enc = No_Types orelse s = tptp_choice
- then [] else T_args)
- | SOME s'' =>
- let
- val s'' = invert_const s''
- fun filter_T_args false = T_args
- | filter_T_args true = filter_type_args thy s'' arity T_args
- in
- case type_arg_policy type_enc s'' of
- Explicit_Type_Args drop_args => (name, filter_T_args drop_args)
- | Mangled_Type_Args drop_args =>
- (mangled_const_name format type_enc (filter_T_args drop_args)
- name, [])
- | No_Type_Args => (name, [])
- end)
- |> (fn (name, T_args) => IConst (name, T, T_args))
- | aux _ (IAbs (bound, tm)) = IAbs (bound, aux 0 tm)
- | aux _ tm = tm
- in aux 0 end
-
-fun repair_iterm ctxt format type_enc sym_tab =
- not (is_type_enc_higher_order type_enc)
- ? (introduce_explicit_apps_in_iterm sym_tab
- #> introduce_predicators_in_iterm sym_tab)
- #> enforce_type_arg_policy_in_iterm ctxt format type_enc
-fun repair_fact ctxt format type_enc sym_tab =
- update_iformula (formula_map (repair_iterm ctxt format type_enc sym_tab))
+ |-> list_app_ops
+ | (head, args) => list_app_ops head (map introduce_app_ops args)
+ fun introduce_predicators tm =
+ case strip_iterm_comb tm of
+ (IConst ((s, _), _, _), _) =>
+ if is_pred_sym sym_tab s then tm else predicator tm
+ | _ => predicator tm
+ val do_iterm =
+ not (is_type_enc_higher_order type_enc)
+ ? (introduce_app_ops #> introduce_predicators)
+ #> filter_type_args_in_iterm thy type_enc
+ in update_iformula (formula_map do_iterm) end
(** Helper facts **)
@@ -1598,7 +1653,7 @@
|>> apfst (map (apsnd (apsnd freeze_term)))
else
((conjs, facts), [])
- val conjs = conjs |> make_conjecture thy format type_enc
+ val conjs = conjs |> make_conjecture ctxt format type_enc
val (fact_names, facts) =
facts
|> map_filter (fn (name, (_, t)) =>
@@ -1622,21 +1677,45 @@
val type_guard = `(make_fixed_const NONE) type_guard_name
-fun type_guard_iterm ctxt format type_enc T tm =
+fun type_guard_iterm format type_enc T tm =
IApp (IConst (type_guard, T --> @{typ bool}, [T])
- |> enforce_type_arg_policy_in_iterm ctxt format type_enc, tm)
+ |> mangle_type_args_in_iterm format type_enc, tm)
fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
| is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
| is_var_positively_naked_in_term _ _ _ _ = true
-fun should_guard_var_in_formula pos phi (SOME true) name =
- formula_fold pos (is_var_positively_naked_in_term name) phi false
- | should_guard_var_in_formula _ _ _ _ = true
+fun is_var_ghost_type_arg_in_term thy name pos tm accum =
+ is_var_positively_naked_in_term name pos tm accum orelse
+ let
+ val var = ATerm (name, [])
+ fun is_nasty_in_term (ATerm (_, [])) = false
+ | is_nasty_in_term (ATerm ((s, _), tms)) =
+ (member (op =) tms var andalso
+ let val ary = length tms in
+ case ghost_type_args thy s ary of
+ [] => false
+ | ghosts =>
+ exists (fn (j, tm) => tm = var andalso member (op =) ghosts j)
+ (0 upto length tms - 1 ~~ tms)
+ end) orelse
+ exists is_nasty_in_term tms
+ | is_nasty_in_term _ = true
+ in is_nasty_in_term tm end
+
+fun should_guard_var_in_formula thy level pos phi (SOME true) name =
+ (case granularity_of_type_level level of
+ All_Vars => true
+ | Positively_Naked_Vars =>
+ formula_fold pos (is_var_positively_naked_in_term name) phi false
+ | Ghost_Type_Arg_Vars =>
+ formula_fold pos (is_var_ghost_type_arg_in_term thy name) phi false)
+ | should_guard_var_in_formula _ _ _ _ _ _ = true
fun should_generate_tag_bound_decl _ _ _ (SOME true) _ = false
- | should_generate_tag_bound_decl ctxt mono (Tags (_, level, Nonuniform)) _ T =
+ | should_generate_tag_bound_decl ctxt mono (Tags (_, level)) _ T =
+ granularity_of_type_level level <> All_Vars andalso
should_encode_type ctxt mono level T
| should_generate_tag_bound_decl _ _ _ _ _ = false
@@ -1645,33 +1724,35 @@
fun tag_with_type ctxt format mono type_enc pos T tm =
IConst (type_tag, T --> T, [T])
- |> enforce_type_arg_policy_in_iterm ctxt format type_enc
+ |> mangle_type_args_in_iterm format type_enc
|> ho_term_from_iterm ctxt format mono type_enc (Top_Level pos)
|> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])
| _ => raise Fail "unexpected lambda-abstraction")
and ho_term_from_iterm ctxt format mono type_enc =
let
- fun aux site u =
+ fun term site u =
let
val (head, args) = strip_iterm_comb u
val pos =
case site of
Top_Level pos => pos
| Eq_Arg pos => pos
- | Elsewhere => NONE
+ | _ => NONE
val t =
case head of
IConst (name as (s, _), _, T_args) =>
let
- val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere
+ fun arg_site j =
+ if is_tptp_equal s then Eq_Arg pos else Arg (s, j)
in
- mk_aterm format type_enc name T_args (map (aux arg_site) args)
+ mk_aterm format type_enc name T_args
+ (map2 (term o arg_site) (0 upto length args - 1) args)
end
| IVar (name, _) =>
- mk_aterm format type_enc name [] (map (aux Elsewhere) args)
+ mk_aterm format type_enc name [] (map (term Elsewhere) args)
| IAbs ((name, T), tm) =>
AAbs ((name, ho_type_from_typ format type_enc true 0 T),
- aux Elsewhere tm)
+ term Elsewhere tm)
| IApp _ => raise Fail "impossible \"IApp\""
val T = ityp_of u
in
@@ -1680,20 +1761,22 @@
else
I)
end
- in aux end
+ in term end
and formula_from_iformula ctxt format mono type_enc should_guard_var =
let
+ val thy = Proof_Context.theory_of ctxt
+ val level = level_of_type_enc type_enc
val do_term = ho_term_from_iterm ctxt format mono type_enc o Top_Level
val do_bound_type =
case type_enc of
- Simple_Types (_, _, level) => fused_type ctxt mono level 0
+ Simple_Types _ => fused_type ctxt mono level 0
#> ho_type_from_typ format type_enc false 0 #> SOME
| _ => K NONE
fun do_out_of_bound_type pos phi universal (name, T) =
if should_guard_type ctxt mono type_enc
- (fn () => should_guard_var pos phi universal name) T then
+ (fn () => should_guard_var thy level pos phi universal name) T then
IVar (name, T)
- |> type_guard_iterm ctxt format type_enc T
+ |> type_guard_iterm format type_enc T
|> do_term pos |> AAtom |> SOME
else if should_generate_tag_bound_decl ctxt mono type_enc universal T then
let
@@ -1798,15 +1881,14 @@
map (decl_line_for_class order) classes
| _ => []
-fun sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
- (conjs, facts) =
+fun sym_decl_table_for_facts ctxt format type_enc sym_tab (conjs, facts) =
let
fun add_iterm_syms in_conj tm =
let val (head, args) = strip_iterm_comb tm in
(case head of
IConst ((s, s'), T, T_args) =>
let
- val pred_sym = is_pred_sym repaired_sym_tab s
+ val pred_sym = is_pred_sym sym_tab s
val decl_sym =
(case type_enc of
Guards _ => not pred_sym
@@ -1840,7 +1922,7 @@
val (s, s') =
`(make_fixed_const NONE) @{const_name undefined}
|> (case type_arg_policy type_enc @{const_name undefined} of
- Mangled_Type_Args _ => mangled_const_name format type_enc [T]
+ Mangled_Type_Args => mangled_const_name format type_enc [T]
| _ => I)
in
Symtab.map_default (s, [])
@@ -1858,8 +1940,8 @@
? (fold (add_fact_syms true) conjs
#> fold (add_fact_syms false) facts
#> (case type_enc of
- Simple_Types (_, poly, _) =>
- if poly = Polymorphic then add_TYPE_const () else I
+ Simple_Types (First_Order, Polymorphic, _) => add_TYPE_const ()
+ | Simple_Types _ => I
| _ => fold add_undefined_const (var_types ())))
end
@@ -1870,7 +1952,7 @@
maybe_infinite_Ts = known_infinite_types,
surely_infinite_Ts =
case level of
- Noninf_Nonmono_Types Sound => []
+ Noninf_Nonmono_Types (Sound, _) => []
| _ => known_infinite_types,
maybe_nonmono_Ts = [@{typ bool}]}
@@ -1883,7 +1965,7 @@
surely_infinite_Ts, maybe_nonmono_Ts}) =
if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then
case level of
- Noninf_Nonmono_Types soundness =>
+ Noninf_Nonmono_Types (soundness, _) =>
if exists (type_instance ctxt T) surely_infinite_Ts orelse
member (type_aconv ctxt) maybe_finite_Ts T then
mono
@@ -1900,7 +1982,7 @@
maybe_infinite_Ts = maybe_infinite_Ts,
surely_infinite_Ts = surely_infinite_Ts,
maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
- | Fin_Nonmono_Types =>
+ | Fin_Nonmono_Types _ =>
if exists (type_instance ctxt T) surely_finite_Ts orelse
member (type_aconv ctxt) maybe_infinite_Ts T then
mono
@@ -1943,19 +2025,22 @@
fun add_fact_monotonic_types ctxt mono type_enc =
add_iformula_monotonic_types ctxt mono type_enc |> fact_lift
fun monotonic_types_for_facts ctxt mono type_enc facts =
- [] |> (polymorphism_of_type_enc type_enc = Polymorphic andalso
- is_type_level_monotonicity_based (level_of_type_enc type_enc))
- ? fold (add_fact_monotonic_types ctxt mono type_enc) facts
+ let val level = level_of_type_enc type_enc in
+ [] |> (polymorphism_of_type_enc type_enc = Polymorphic andalso
+ is_type_level_monotonicity_based level andalso
+ granularity_of_type_level level <> Ghost_Type_Arg_Vars)
+ ? fold (add_fact_monotonic_types ctxt mono type_enc) facts
+ end
fun formula_line_for_guards_mono_type ctxt format mono type_enc T =
Formula (guards_sym_formula_prefix ^
ascii_of (mangled_type format type_enc T),
Axiom,
IConst (`make_bound_var "X", T, [])
- |> type_guard_iterm ctxt format type_enc T
+ |> type_guard_iterm format type_enc T
|> AAtom
|> formula_from_iformula ctxt format mono type_enc
- (K (K (K (K true)))) (SOME true)
+ (K (K (K (K (K (K true)))))) (SOME true)
|> bound_tvars type_enc (atyps_of T)
|> close_formula_universally type_enc,
isabelle_info introN, NONE)
@@ -2008,39 +2093,49 @@
fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono type_enc n s
j (s', T_args, T, _, ary, in_conj) =
let
+ val thy = Proof_Context.theory_of ctxt
val (kind, maybe_negate) =
if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
else (Axiom, I)
val (arg_Ts, res_T) = chop_fun ary T
- val num_args = length arg_Ts
- val bound_names =
- 1 upto num_args |> map (`I o make_bound_var o string_of_int)
+ val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
val bounds =
bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, []))
- val sym_needs_arg_types = exists (curry (op =) dummyT) T_args
- fun should_keep_arg_type T =
- sym_needs_arg_types andalso
- should_guard_type ctxt mono type_enc (K true) T
val bound_Ts =
- arg_Ts |> map (fn T => if should_keep_arg_type T then SOME T else NONE)
+ if exists (curry (op =) dummyT) T_args then
+ case level_of_type_enc type_enc of
+ All_Types => map SOME arg_Ts
+ | level =>
+ if granularity_of_type_level level = Ghost_Type_Arg_Vars then
+ let val ghosts = ghost_type_args thy s ary in
+ map2 (fn j => if member (op =) ghosts j then SOME else K NONE)
+ (0 upto ary - 1) arg_Ts
+ end
+ else
+ replicate ary NONE
+ else
+ replicate ary NONE
in
Formula (guards_sym_formula_prefix ^ s ^
(if n > 1 then "_" ^ string_of_int j else ""), kind,
IConst ((s, s'), T, T_args)
|> fold (curry (IApp o swap)) bounds
- |> type_guard_iterm ctxt format type_enc res_T
+ |> type_guard_iterm format type_enc res_T
|> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
|> formula_from_iformula ctxt format mono type_enc
- (K (K (K (K true)))) (SOME true)
+ (K (K (K (K (K (K true)))))) (SOME true)
|> n > 1 ? bound_tvars type_enc (atyps_of T)
|> close_formula_universally type_enc
|> maybe_negate,
isabelle_info introN, NONE)
end
-fun formula_lines_for_nonuniform_tags_sym_decl ctxt format conj_sym_kind mono
- type_enc n s (j, (s', T_args, T, pred_sym, ary, in_conj)) =
+fun formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono type_enc n s
+ (j, (s', T_args, T, pred_sym, ary, in_conj)) =
let
+ val thy = Proof_Context.theory_of ctxt
+ val level = level_of_type_enc type_enc
+ val grain = granularity_of_type_level level
val ident_base =
tags_sym_formula_prefix ^ s ^
(if n > 1 then "_" ^ string_of_int j else "")
@@ -2048,19 +2143,28 @@
if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
else (Axiom, I)
val (arg_Ts, res_T) = chop_fun ary T
- val bound_names =
- 1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
+ val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
val bounds = bound_names |> map (fn name => ATerm (name, []))
val cst = mk_aterm format type_enc (s, s') T_args
val eq = maybe_negate oo eq_formula type_enc (atyps_of T) pred_sym
- val should_encode =
- should_encode_type ctxt mono (level_of_type_enc type_enc)
+ val should_encode = should_encode_type ctxt mono level
val tag_with = tag_with_type ctxt format mono type_enc NONE
val add_formula_for_res =
if should_encode res_T then
- cons (Formula (ident_base ^ "_res", kind,
- eq (tag_with res_T (cst bounds)) (cst bounds),
- isabelle_info simpN, NONE))
+ let
+ val tagged_bounds =
+ if grain = Ghost_Type_Arg_Vars then
+ let val ghosts = ghost_type_args thy s ary in
+ map2 (fn (j, arg_T) => member (op =) ghosts j ? tag_with arg_T)
+ (0 upto ary - 1 ~~ arg_Ts) bounds
+ end
+ else
+ bounds
+ in
+ cons (Formula (ident_base ^ "_res", kind,
+ eq (tag_with res_T (cst bounds)) (cst tagged_bounds),
+ isabelle_info simpN, NONE))
+ end
else
I
fun add_formula_for_arg k =
@@ -2078,7 +2182,8 @@
end
in
[] |> not pred_sym ? add_formula_for_res
- |> Config.get ctxt type_tag_arguments
+ |> (Config.get ctxt type_tag_arguments andalso
+ grain = Positively_Naked_Vars)
? fold add_formula_for_arg (ary - 1 downto 0)
end
@@ -2089,7 +2194,7 @@
case type_enc of
Simple_Types _ =>
decls |> map (decl_line_for_sym ctxt format mono type_enc s)
- | Guards (_, level, _) =>
+ | Guards (_, level) =>
let
val decls =
case decls of
@@ -2111,15 +2216,15 @@
|-> map2 (formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono
type_enc n s)
end
- | Tags (_, _, uniformity) =>
- (case uniformity of
- Uniform => []
- | Nonuniform =>
- let val n = length decls in
- (0 upto n - 1 ~~ decls)
- |> maps (formula_lines_for_nonuniform_tags_sym_decl ctxt format
- conj_sym_kind mono type_enc n s)
- end)
+ | Tags (_, level) =>
+ if granularity_of_type_level level = All_Vars then
+ []
+ else
+ let val n = length decls in
+ (0 upto n - 1 ~~ decls)
+ |> maps (formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono
+ type_enc n s)
+ end
fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono type_enc
mono_Ts sym_decl_tab =
@@ -2133,11 +2238,10 @@
syms []
in mono_lines @ decl_lines end
-fun needs_type_tag_idempotence ctxt (Tags (poly, level, uniformity)) =
+fun needs_type_tag_idempotence ctxt (Tags (poly, level)) =
Config.get ctxt type_tag_idempotence andalso
- poly <> Mangled_Monomorphic andalso
- ((level = All_Types andalso uniformity = Nonuniform) orelse
- is_type_level_monotonicity_based level)
+ is_type_level_monotonicity_based level andalso
+ poly <> Mangled_Monomorphic
| needs_type_tag_idempotence _ _ = false
fun offset_of_heading_in_problem _ [] j = j
@@ -2154,12 +2258,22 @@
val conjsN = "Conjectures"
val free_typesN = "Type variables"
-val explicit_apply = NONE (* for experiments *)
+val explicit_apply_threshold = 50
fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
lambda_trans readable_names preproc hyp_ts concl_t facts =
let
+ val thy = Proof_Context.theory_of ctxt
val type_enc = type_enc |> adjust_type_enc format
+ (* Forcing explicit applications is expensive for polymorphic encodings,
+ because it takes only one existential variable ranging over "'a => 'b" to
+ ruin everything. Hence we do it only if there are few facts. *)
+ val explicit_apply =
+ if polymorphism_of_type_enc type_enc <> Polymorphic orelse
+ length facts <= explicit_apply_threshold then
+ NONE
+ else
+ SOME false
val lambda_trans =
if lambda_trans = smartN then
if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
@@ -2190,22 +2304,23 @@
val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses) =
translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
hyp_ts concl_t facts
- val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
+ val sym_tab =
+ conjs @ facts |> sym_table_for_facts ctxt type_enc explicit_apply
val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
- val repair = repair_fact ctxt format type_enc sym_tab
- val (conjs, facts) = (conjs, facts) |> pairself (map repair)
- val repaired_sym_tab =
- conjs @ facts |> sym_table_for_facts ctxt (SOME false)
+ val firstorderize = firstorderize_fact thy format type_enc sym_tab
+ val (conjs, facts) = (conjs, facts) |> pairself (map firstorderize)
+ val sym_tab =
+ conjs @ facts |> sym_table_for_facts ctxt type_enc (SOME false)
val helpers =
- repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc
- |> map repair
+ sym_tab |> helper_facts_for_sym_table ctxt format type_enc
+ |> map firstorderize
val mono_Ts =
helpers @ conjs @ facts
|> monotonic_types_for_facts ctxt mono type_enc
val class_decl_lines = decl_lines_for_classes type_enc classes
val sym_decl_lines =
(conjs, helpers @ facts)
- |> sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
+ |> sym_decl_table_for_facts ctxt format type_enc sym_tab
|> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono
type_enc mono_Ts
val helper_lines =
@@ -2249,13 +2364,8 @@
else NONE)
((helpers_offset + 1 upto helpers_offset + length helpers)
~~ helpers)
- fun add_sym_arity (s, {min_ary, ...} : sym_info) =
- if min_ary > 0 then
- case strip_prefix_and_unascii const_prefix s of
- SOME s => Symtab.insert (op =) (s, min_ary)
- | NONE => I
- else
- I
+ fun add_sym_ary (s, {min_ary, ...} : sym_info) =
+ min_ary > 0 ? Symtab.insert (op =) (s, min_ary)
in
(problem,
case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
@@ -2263,7 +2373,7 @@
offset_of_heading_in_problem factsN problem 0,
fact_names |> Vector.fromList,
typed_helpers,
- Symtab.empty |> Symtab.fold add_sym_arity sym_tab)
+ Symtab.empty |> Symtab.fold add_sym_ary sym_tab)
end
(* FUDGE *)
--- a/src/HOL/Tools/ATP/atp_util.ML Wed Sep 07 08:13:38 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML Thu Sep 08 00:35:22 2011 +0200
@@ -10,6 +10,7 @@
val hash_string : string -> int
val hash_term : term -> int
val strip_spaces : bool -> (char -> bool) -> string -> string
+ val strip_spaces_except_between_idents : string -> string
val nat_subscript : int -> string
val unyxml : string -> string
val maybe_quote : string -> string
@@ -88,6 +89,9 @@
fun strip_spaces skip_comments is_evil =
implode o strip_spaces_in_list skip_comments is_evil o String.explode
+fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
+val strip_spaces_except_between_idents = strip_spaces true is_ident_char
+
val subscript = implode o map (prefix "\<^isub>") o raw_explode (* FIXME Symbol.explode (?) *)
fun nat_subscript n =
n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
--- a/src/HOL/Tools/Metis/metis_tactic.ML Wed Sep 07 08:13:38 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Thu Sep 08 00:35:22 2011 +0200
@@ -39,8 +39,8 @@
val partial_typesN = "partial_types"
val no_typesN = "no_types"
-val really_full_type_enc = "mono_tags_uniform"
-val full_type_enc = "poly_guards_uniform_query"
+val really_full_type_enc = "mono_tags"
+val full_type_enc = "poly_guards_query"
val partial_type_enc = "poly_args"
val no_type_enc = "erased"
--- a/src/HOL/Tools/Metis/metis_translate.ML Wed Sep 07 08:13:38 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Thu Sep 08 00:35:22 2011 +0200
@@ -59,8 +59,9 @@
((prefixed_predicator_name, 1), (K metis_predicator, false)),
((prefixed_app_op_name, 2), (K metis_app_op, false)),
((prefixed_type_tag_name, 2),
- (fn Tags (_, All_Types, Uniform) => metis_systematic_type_tag
- | _ => metis_ad_hoc_type_tag, true))]
+ (fn type_enc =>
+ if level_of_type_enc type_enc = All_Types then metis_systematic_type_tag
+ else metis_ad_hoc_type_tag, true))]
fun old_skolem_const_name i j num_T_args =
old_skolem_const_prefix ^ Long_Name.separator ^
--- a/src/HOL/Tools/Nitpick/nitrox.ML Wed Sep 07 08:13:38 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitrox.ML Thu Sep 08 00:35:22 2011 +0200
@@ -21,8 +21,7 @@
exception SYNTAX of string
-fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
-val tptp_explode = raw_explode o strip_spaces true is_ident_char
+val tptp_explode = raw_explode o strip_spaces_except_between_idents
fun parse_file_path (c :: ss) =
if c = "'" orelse c = "\"" then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Sep 07 08:13:38 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Sep 08 00:35:22 2011 +0200
@@ -144,7 +144,6 @@
(j + 1,
((nth_name j,
if member Thm.eq_thm_prop chained_ths th then Chained
- else if Thm.eq_thm_prop (th, @{thm ext}) then Extensionality
else General), th) :: rest))
|> snd
end
@@ -576,7 +575,7 @@
| _ => SOME tab
in aux (prop_of th) [] end
-(* FIXME: This is currently only useful for polymorphic type systems. *)
+(* FIXME: This is currently only useful for polymorphic type encodings. *)
fun could_benefit_from_ext is_built_in_const facts =
fold (consider_arities is_built_in_const o snd) facts (SOME Symtab.empty)
|> is_none
@@ -845,8 +844,7 @@
else if global then
case Termtab.lookup clasimpset_table (prop_of th) of
SOME loc => loc
- | NONE => if Thm.eq_thm_prop (th, @{thm ext}) then Extensionality
- else General
+ | NONE => General
else if is_assum th then Assum else Local
fun is_good_unnamed_local th =
not (Thm.has_name_hint th) andalso
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Sep 07 08:13:38 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Sep 08 00:35:22 2011 +0200
@@ -19,6 +19,7 @@
structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
struct
+open ATP_Util
open ATP_Systems
open ATP_Translate
open Sledgehammer_Util
@@ -151,11 +152,9 @@
error ("Unknown parameter: " ^ quote name ^ "."))
-(* Ensure that type systems such as "mono_simple!" and "mono_guards?" are
- handled correctly. *)
-fun implode_param [s, "?"] = s ^ "?"
- | implode_param [s, "!"] = s ^ "!"
- | implode_param ss = space_implode " " ss
+(* Ensures that type encodings such as "mono_simple?" and "poly_guards!!" are
+ read correctly. *)
+val implode_param = strip_spaces_except_between_idents o space_implode " "
structure Data = Theory_Data
(
@@ -376,12 +375,11 @@
|> sort_strings |> cat_lines))
end))
+val parse_query_bang = Parse.$$$ "?" || Parse.$$$ "!" || Parse.$$$ "!!"
val parse_key =
- Scan.repeat1 (Parse.typ_group || Parse.$$$ "?" || Parse.$$$ "!")
- >> implode_param
+ Scan.repeat1 (Parse.typ_group || parse_query_bang) >> implode_param
val parse_value =
- Scan.repeat1 (Parse.xname || Parse.float_number || Parse.$$$ "?"
- || Parse.$$$ "!")
+ Scan.repeat1 (Parse.xname || Parse.float_number || parse_query_bang)
val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
val parse_fact_refs =
--- a/src/Pure/System/isabelle_charset.scala Wed Sep 07 08:13:38 2011 +0200
+++ b/src/Pure/System/isabelle_charset.scala Thu Sep 08 00:35:22 2011 +0200
@@ -37,14 +37,18 @@
{
override def charsetForName(name: String): Charset =
{
- if (name.equalsIgnoreCase(Isabelle_Charset.name)) Isabelle_Charset.charset
- else null
+ // FIXME inactive
+ // if (name.equalsIgnoreCase(Isabelle_Charset.name)) Isabelle_Charset.charset
+ // else null
+ null
}
override def charsets(): java.util.Iterator[Charset] =
{
import scala.collection.JavaConversions._
- Iterator(Isabelle_Charset.charset)
+ // FIXME inactive
+ // Iterator(Isabelle_Charset.charset)
+ Iterator()
}
}
--- a/src/Pure/System/isabelle_process.scala Wed Sep 07 08:13:38 2011 +0200
+++ b/src/Pure/System/isabelle_process.scala Thu Sep 08 00:35:22 2011 +0200
@@ -205,12 +205,6 @@
def join() { process_manager.join() }
- def interrupt()
- {
- try { process.interrupt }
- catch { case e: IOException => system_result("Failed to interrupt Isabelle: " + e.getMessage) }
- }
-
def terminate()
{
close()
--- a/src/Pure/System/session.scala Wed Sep 07 08:13:38 2011 +0200
+++ b/src/Pure/System/session.scala Thu Sep 08 00:35:22 2011 +0200
@@ -137,7 +137,7 @@
/* actor messages */
private case class Start(timeout: Time, args: List[String])
- private case object Interrupt
+ private case object Cancel_Execution
private case class Init_Node(name: Document.Node.Name,
header: Document.Node_Header, perspective: Text.Perspective, text: String)
private case class Edit_Node(name: Document.Node.Name,
@@ -423,8 +423,8 @@
receiver.cancel()
reply(())
- case Interrupt if prover.isDefined =>
- prover.get.interrupt
+ case Cancel_Execution if prover.isDefined =>
+ prover.get.cancel_execution()
case Init_Node(name, header, perspective, text) if prover.isDefined =>
// FIXME compare with existing node
@@ -471,7 +471,7 @@
def stop() { commands_changed_buffer !? Stop; session_actor !? Stop }
- def interrupt() { session_actor ! Interrupt }
+ def cancel_execution() { session_actor ! Cancel_Execution }
def init_node(name: Document.Node.Name,
header: Document.Node_Header, perspective: Text.Perspective, text: String)
--- a/src/Tools/Code/code_haskell.ML Wed Sep 07 08:13:38 2011 +0200
+++ b/src/Tools/Code/code_haskell.ML Thu Sep 08 00:35:22 2011 +0200
@@ -25,7 +25,7 @@
(** Haskell serializer **)
fun print_haskell_stmt labelled_name class_syntax tyco_syntax const_syntax
- reserved deresolve contr_classparam_typs deriving_show =
+ reserved deresolve deriving_show =
let
fun class_name class = case class_syntax class
of NONE => deresolve class
@@ -75,20 +75,14 @@
then print_case tyvars some_thm vars fxy cases
else print_app tyvars some_thm vars fxy c_ts
| NONE => print_case tyvars some_thm vars fxy cases)
- and print_app_expr tyvars some_thm vars ((c, (_, function_typs)), ts) = case contr_classparam_typs c
- of [] => (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts
- | fingerprint => let
- val ts_fingerprint = ts ~~ take (length ts) fingerprint;
- val needs_annotation = forall (fn (_, NONE) => true | (t, SOME _) =>
- (not o Code_Thingol.locally_monomorphic) t) ts_fingerprint;
- fun print_term_anno (t, NONE) _ = print_term tyvars some_thm vars BR t
- | print_term_anno (t, SOME _) ty =
- brackets [print_term tyvars some_thm vars NOBR t, str "::", print_typ tyvars NOBR ty];
- in
- if needs_annotation then
- (str o deresolve) c :: map2 print_term_anno ts_fingerprint (take (length ts) function_typs)
- else (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts
- end
+ and print_app_expr tyvars some_thm vars ((c, ((_, (function_typs, body_typ)), annotate)), ts) =
+ let
+ val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (function_typs, body_typ)
+ fun put_annotation c = brackets [c, str "::", print_typ tyvars NOBR ty]
+ in
+ ((if annotate then put_annotation else I)
+ ((str o deresolve) c)) :: map (print_term tyvars some_thm vars BR) ts
+ end
and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax
and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p
and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
@@ -230,14 +224,14 @@
]
| SOME k =>
let
- val (c, (_, tys)) = const;
+ val (c, ((_, tys), _)) = const; (* FIXME: pass around the need annotation flag here? *)
val (vs, rhs) = (apfst o map) fst
(Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
val s = if (is_some o const_syntax) c
then NONE else (SOME o Long_Name.base_name o deresolve) c;
val vars = reserved
|> intro_vars (map_filter I (s :: vs));
- val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs;
+ val lhs = IConst (classparam, ((([], []), tys), false (* FIXME *))) `$$ map IVar vs;
(*dictionaries are not relevant at this late stage*)
in
semicolon [
@@ -304,7 +298,6 @@
labelled_name module_alias module_prefix (Name.make_context reserved) program;
(* print statements *)
- val contr_classparam_typs = Code_Thingol.contr_classparam_typs program;
fun deriving_show tyco =
let
fun deriv _ "fun" = false
@@ -320,7 +313,7 @@
in deriv [] tyco end;
fun print_stmt deresolve = print_haskell_stmt labelled_name
class_syntax tyco_syntax const_syntax (make_vars reserved)
- deresolve contr_classparam_typs
+ deresolve
(if string_classes then deriving_show else K false);
(* print modules *)
--- a/src/Tools/Code/code_ml.ML Wed Sep 07 08:13:38 2011 +0200
+++ b/src/Tools/Code/code_ml.ML Thu Sep 08 00:35:22 2011 +0200
@@ -117,7 +117,7 @@
then print_case is_pseudo_fun some_thm vars fxy cases
else print_app is_pseudo_fun some_thm vars fxy c_ts
| NONE => print_case is_pseudo_fun some_thm vars fxy cases)
- and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), function_typs)), ts)) =
+ and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), (function_typs, _)), _)), ts)) =
if is_cons c then
let val k = length function_typs in
if k < 2 orelse length ts = k
@@ -417,7 +417,7 @@
then print_case is_pseudo_fun some_thm vars fxy cases
else print_app is_pseudo_fun some_thm vars fxy c_ts
| NONE => print_case is_pseudo_fun some_thm vars fxy cases)
- and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), tys)), ts)) =
+ and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), (tys, _)), _)), ts)) =
if is_cons c then
let val k = length tys in
if length ts = k
--- a/src/Tools/Code/code_printer.ML Wed Sep 07 08:13:38 2011 +0200
+++ b/src/Tools/Code/code_printer.ML Thu Sep 08 00:35:22 2011 +0200
@@ -315,7 +315,7 @@
|-> (fn cs' => pair (Complex_const_syntax (n, f literals cs')));
fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
- (app as ((c, (_, function_typs)), ts)) =
+ (app as ((c, ((_, (function_typs, _)), _)), ts)) =
case const_syntax c of
NONE => brackify fxy (print_app_expr some_thm vars app)
| SOME (Plain_const_syntax (_, s)) =>
--- a/src/Tools/Code/code_scala.ML Wed Sep 07 08:13:38 2011 +0200
+++ b/src/Tools/Code/code_scala.ML Thu Sep 08 00:35:22 2011 +0200
@@ -72,7 +72,7 @@
else print_app tyvars is_pat some_thm vars fxy c_ts
| NONE => print_case tyvars some_thm vars fxy cases)
and print_app tyvars is_pat some_thm vars fxy
- (app as ((c, ((arg_typs, _), function_typs)), ts)) =
+ (app as ((c, (((arg_typs, _), (function_typs, _)), _)), ts)) =
let
val k = length ts;
val arg_typs' = if is_pat orelse
@@ -265,7 +265,7 @@
let
val tyvars = intro_tyvars vs reserved;
val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
- fun print_classparam_instance ((classparam, const as (_, (_, tys))), (thm, _)) =
+ fun print_classparam_instance ((classparam, const as (_, ((_, (tys, _)), _))), (thm, _)) =
let
val aux_tys = Name.invent_names (snd reserved) "a" tys;
val auxs = map fst aux_tys;
--- a/src/Tools/Code/code_thingol.ML Wed Sep 07 08:13:38 2011 +0200
+++ b/src/Tools/Code/code_thingol.ML Thu Sep 08 00:35:22 2011 +0200
@@ -22,7 +22,7 @@
datatype itype =
`%% of string * itype list
| ITyVar of vname;
- type const = string * ((itype list * dict list list) * itype list)
+ type const = string * (((itype list * dict list list) * (itype list * itype)) * bool)
(* f [T1..Tn] {dicts} (_::S1) .. (_..Sm) =^= (f, (([T1..Tn], dicts), [S1..Sm]) *)
datatype iterm =
IConst of const
@@ -55,7 +55,6 @@
val is_IAbs: iterm -> bool
val eta_expand: int -> const * iterm list -> iterm
val contains_dict_var: iterm -> bool
- val locally_monomorphic: iterm -> bool
val add_constnames: iterm -> string list -> string list
val add_tyconames: iterm -> string list -> string list
val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
@@ -88,7 +87,6 @@
val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt
val is_cons: program -> string -> bool
val is_case: stmt -> bool
- val contr_classparam_typs: program -> string -> itype option list
val labelled_name: theory -> program -> string -> string
val group_stmts: theory -> program
-> ((string * stmt) list * (string * stmt) list
@@ -145,7 +143,8 @@
`%% of string * itype list
| ITyVar of vname;
-type const = string * ((itype list * dict list list) * itype list (*types of arguments*))
+type const = string * (((itype list * dict list list) *
+ (itype list (*types of arguments*) * itype (*body type*))) * bool (*requires type annotation*))
datatype iterm =
IConst of const
@@ -198,7 +197,7 @@
fun add_tycos (tyco `%% tys) = insert (op =) tyco #> fold add_tycos tys
| add_tycos (ITyVar _) = I;
-val add_tyconames = fold_constexprs (fn (_, ((tys, _), _)) => fold add_tycos tys);
+val add_tyconames = fold_constexprs (fn (_, (((tys, _), _), _)) => fold add_tycos tys);
fun fold_varnames f =
let
@@ -240,7 +239,7 @@
val vs_tys = (map o apfst) SOME (Name.invent_names ctxt "a" tys);
in (vs_tys, t `$$ map (IVar o fst) vs_tys) end;
-fun eta_expand k (c as (name, (_, tys)), ts) =
+fun eta_expand k (c as (name, ((_, (tys, _)), _)), ts) =
let
val j = length ts;
val l = k - j;
@@ -256,18 +255,12 @@
fun cont_dict (Dict (_, d)) = cont_plain_dict d
and cont_plain_dict (Dict_Const (_, dss)) = (exists o exists) cont_dict dss
| cont_plain_dict (Dict_Var _) = true;
- fun cont_term (IConst (_, ((_, dss), _))) = (exists o exists) cont_dict dss
+ fun cont_term (IConst (_, (((_, dss), _), _))) = (exists o exists) cont_dict dss
| cont_term (IVar _) = false
| cont_term (t1 `$ t2) = cont_term t1 orelse cont_term t2
| cont_term (_ `|=> t) = cont_term t
| cont_term (ICase (_, t)) = cont_term t;
in cont_term t end;
-
-fun locally_monomorphic (IConst _) = false
- | locally_monomorphic (IVar _) = true
- | locally_monomorphic (t `$ _) = locally_monomorphic t
- | locally_monomorphic (_ `|=> t) = locally_monomorphic t
- | locally_monomorphic (ICase ((_, ds), _)) = exists (locally_monomorphic o snd) ds;
(** namings **)
@@ -480,28 +473,6 @@
(fn (_, (Classinst ((class, _), (_, (param_insts, _))), _)) =>
Option.map (fn ((const, _), _) => (class, const))
(find_first (fn ((_, (inst_const, _)), _) => inst_const = name) param_insts) | _ => NONE)
-
-fun contr_classparam_typs program name =
- let
- fun contr_classparam_typs' (class, name) =
- let
- val Class (_, (_, (_, params))) = Graph.get_node program class;
- val SOME ty = AList.lookup (op =) params name;
- val (tys, res_ty) = unfold_fun ty;
- fun no_tyvar (_ `%% tys) = forall no_tyvar tys
- | no_tyvar (ITyVar _) = false;
- in if no_tyvar res_ty
- then map (fn ty => if no_tyvar ty then NONE else SOME ty) tys
- else []
- end
- in
- case Graph.get_node program name
- of Classparam (_, class) => contr_classparam_typs' (class, name)
- | Fun (c, _) => (case lookup_classparam_instance program name
- of NONE => []
- | SOME (class, name) => the_default [] (try contr_classparam_typs' (class, name)))
- | _ => []
- end;
fun labelled_name thy program name =
let val ctxt = Proof_Context.init_global thy in
@@ -608,6 +579,42 @@
(err_typ ^ "\n" ^ err_class)
end;
+(* inference of type annotations for disambiguation with type classes *)
+
+fun annotate_term (Const (c', T'), Const (c, T)) tvar_names =
+ let
+ val tvar_names' = Term.add_tvar_namesT T' tvar_names
+ in
+ (Const (c, if eq_set (op =) (tvar_names, tvar_names') then T else Type("", [T])), tvar_names')
+ end
+ | annotate_term (t1 $ u1, t $ u) tvar_names =
+ let
+ val (u', tvar_names') = annotate_term (u1, u) tvar_names
+ val (t', tvar_names'') = annotate_term (t1, t) tvar_names'
+ in
+ (t' $ u', tvar_names'')
+ end
+ | annotate_term (Abs (_, _, t1) , Abs (x, T, t)) tvar_names =
+ apfst (fn t => Abs (x, T, t)) (annotate_term (t1, t) tvar_names)
+ | annotate_term (_, t) tvar_names = (t, tvar_names)
+
+fun annotate_eqns thy eqns =
+ let
+ val ctxt = ProofContext.init_global thy |> Config.put Type_Infer_Context.const_sorts false
+ val erase = map_types (fn _ => Type_Infer.anyT [])
+ val reinfer = singleton (Type_Infer_Context.infer_types ctxt)
+ fun add_annotations ((args, (rhs, some_abs)), (SOME th, proper)) =
+ let
+ val (lhs, drhs) = Logic.dest_equals (prop_of (Thm.unvarify_global th))
+ val drhs' = snd (Logic.dest_equals (reinfer (Logic.mk_equals (lhs, erase drhs))))
+ val (rhs', _) = annotate_term (drhs', rhs) []
+ in
+ ((args, (rhs', some_abs)), (SOME th, proper))
+ end
+ | add_annotations eqn = eqn
+ in
+ map add_annotations eqns
+ end;
(* translation *)
@@ -633,11 +640,12 @@
fun stmt_fun cert =
let
val ((vs, ty), eqns) = Code.equations_of_cert thy cert;
+ val eqns' = annotate_eqns thy eqns
val some_case_cong = Code.get_case_cong thy c;
in
fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
##>> translate_typ thy algbr eqngr permissive ty
- ##>> translate_eqns thy algbr eqngr permissive eqns
+ ##>> translate_eqns thy algbr eqngr permissive eqns'
#>> (fn info => Fun (c, (info, some_case_cong)))
end;
val stmt_const = case Code.get_type_of_constr_or_abstr thy c
@@ -748,15 +756,17 @@
then translation_error thy permissive some_thm
"Abstraction violation" ("constant " ^ Code.string_of_const thy c)
else ()
- val arg_typs = Sign.const_typargs thy (c, ty);
+ val (annotate, ty') = (case ty of Type("", [ty']) => (true, ty') | ty' => (false, ty'))
+ val arg_typs = Sign.const_typargs thy (c, ty');
val sorts = Code_Preproc.sortargs eqngr c;
- val function_typs = Term.binder_types ty;
+ val (function_typs, body_typ) = Term.strip_type ty';
in
ensure_const thy algbr eqngr permissive c
##>> fold_map (translate_typ thy algbr eqngr permissive) arg_typs
##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (arg_typs ~~ sorts)
- ##>> fold_map (translate_typ thy algbr eqngr permissive) function_typs
- #>> (fn (((c, arg_typs), dss), function_typs) => IConst (c, ((arg_typs, dss), function_typs)))
+ ##>> fold_map (translate_typ thy algbr eqngr permissive) (body_typ :: function_typs)
+ #>> (fn (((c, arg_typs), dss), body_typ :: function_typs) =>
+ IConst (c, (((arg_typs, dss), (function_typs, body_typ)), annotate)))
end
and translate_app_const thy algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
translate_const thy algbr eqngr permissive some_thm (c_ty, some_abs)
@@ -801,7 +811,7 @@
val ts_clause = nth_drop t_pos ts;
val clauses = if null case_pats
then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause)
- else maps (fn ((constr as IConst (_, (_, tys)), n), t) =>
+ else maps (fn ((constr as IConst (_, ((_, (tys, _)), _)), n), t) =>
mk_clause (fn (ts, body) => (constr `$$ ts, body)) (take n tys) t)
(constrs ~~ ts_clause);
in ((t, ty), clauses) end;
--- a/src/Tools/jEdit/src/document_model.scala Wed Sep 07 08:13:38 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Thu Sep 08 00:35:22 2011 +0200
@@ -69,6 +69,8 @@
/* perspective */
+ def buffer_range(): Text.Range = Text.Range(0, (buffer.getLength - 1) max 0)
+
def perspective(): Text.Perspective =
{
Swing_Thread.require()
@@ -136,6 +138,12 @@
pending_edits.update_perspective()
}
+ def full_perspective()
+ {
+ pending_edits.flush()
+ session.edit_node(name, node_header(), Text.Perspective(List(buffer_range())), Nil)
+ }
+
/* snapshot */
--- a/src/Tools/jEdit/src/document_view.scala Wed Sep 07 08:13:38 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Thu Sep 08 00:35:22 2011 +0200
@@ -118,7 +118,7 @@
def perspective(): Text.Perspective =
{
Swing_Thread.require()
- val buffer_range = Text.Range(0, (model.buffer.getLength - 1) max 0)
+ val buffer_range = model.buffer_range()
Text.Perspective(
for {
i <- 0 until text_area.getVisibleLines
--- a/src/Tools/jEdit/src/session_dockable.scala Wed Sep 07 08:13:38 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala Thu Sep 08 00:35:22 2011 +0200
@@ -61,13 +61,31 @@
session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
session_phase.tooltip = "Prover status"
+ private val cancel = new Button("Cancel") {
+ reactions += { case ButtonClicked(_) => Isabelle.session.cancel_execution }
+ }
+ cancel.tooltip = "Cancel current proof checking process"
+
+ private val check = new Button("Check") {
+ reactions +=
+ {
+ case ButtonClicked(_) =>
+ Isabelle.document_model(view.getBuffer) match {
+ case None =>
+ case Some(model) => model.full_perspective()
+ }
+ }
+ }
+ check.tooltip = "Commence full proof checking of current buffer"
+
private val logic = Isabelle.logic_selector(Isabelle.Property("logic"))
logic.listenTo(logic.selection)
logic.reactions += {
case SelectionChanged(_) => Isabelle.Property("logic") = logic.selection.item.name
}
- private val controls = new FlowPanel(FlowPanel.Alignment.Right)(session_phase, logic)
+ private val controls =
+ new FlowPanel(FlowPanel.Alignment.Right)(check, cancel, session_phase, logic)
add(controls.peer, BorderLayout.NORTH)
--- a/src/Tools/nbe.ML Wed Sep 07 08:13:38 2011 +0200
+++ b/src/Tools/nbe.ML Thu Sep 08 00:35:22 2011 +0200
@@ -315,7 +315,7 @@
let
val (t', ts) = Code_Thingol.unfold_app t
in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end
- and of_iapp match_cont (IConst (c, ((_, dss), _))) ts = constapp c dss ts
+ and of_iapp match_cont (IConst (c, (((_, dss), _), _))) ts = constapp c dss ts
| of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound_optional v) ts
| of_iapp match_cont ((v, _) `|=> t) ts =
nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound_optional v]) (of_iterm NONE t))) ts
@@ -425,7 +425,7 @@
val params = Name.invent Name.context "d" (length names);
fun mk (k, name) =
(name, ([(v, [])],
- [([IConst (class, (([], []), [])) `$$ map (IVar o SOME) params],
+ [([IConst (class, ((([], []), ([], ITyVar "")), false)) `$$ map (IVar o SOME) params],
IVar (SOME (nth params k)))]));
in map_index mk names end
| eqns_of_stmt (_, Code_Thingol.Classrel _) =
@@ -433,8 +433,8 @@
| eqns_of_stmt (_, Code_Thingol.Classparam _) =
[]
| eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arity_args)), (super_instances, (classparam_instances, _)))) =
- [(inst, (arity_args, [([], IConst (class, (([], []), [])) `$$
- map (fn (_, (_, (inst, dss))) => IConst (inst, (([], dss), []))) super_instances
+ [(inst, (arity_args, [([], IConst (class, ((([], []), ([], ITyVar "")), false)) `$$
+ map (fn (_, (_, (inst, dss))) => IConst (inst, ((([], dss), ([], ITyVar "")), false))) super_instances
@ map (IConst o snd o fst) classparam_instances)]))];