# HG changeset patch # User haftmann # Date 1315434922 -7200 # Node ID 096ec174be5d22742893495578f7f064c1e9cc27 # Parent fe33d66551860470552a44950262f7b48007cccc# Parent 859fc95860c5758254dbe46fad549d78ab2e1d0f merged diff -r 859fc95860c5 -r 096ec174be5d CONTRIBUTORS --- 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 ----------------------------- diff -r 859fc95860c5 -r 096ec174be5d NEWS --- 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 \ and \ (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) diff -r 859fc95860c5 -r 096ec174be5d doc-src/Sledgehammer/sledgehammer.tex --- 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} diff -r 859fc95860c5 -r 096ec174be5d doc-src/System/Thy/Misc.thy --- 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"}. diff -r 859fc95860c5 -r 096ec174be5d doc-src/System/Thy/document/Misc.tex --- 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}}}.% diff -r 859fc95860c5 -r 096ec174be5d src/HOL/Decision_Procs/Commutative_Ring_Complete.thy --- 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 \ bool" +fun isnorm :: "'a::comm_ring pol \ bool" where "isnorm (Pc c) \ True" | "isnorm (Pinj i (Pc c)) \ False" @@ -26,35 +25,40 @@ | "isnorm (PX P i Q) \ isnorm P \ 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) \ 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) \ 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) \ isnorm Q" -by(cases i, auto, cases P, auto, case_tac pol2, auto) +lemma norm_PX2: "isnorm (PX P i Q) \ isnorm Q" + by (cases i) (auto, cases P, auto, case_tac pol2, auto) + +lemma norm_PX1: "isnorm (PX P i Q) \ isnorm P" + by (cases i) (auto, cases P, auto, case_tac pol2, auto) -lemma norm_PX1:"isnorm (PX P i Q) \ isnorm P" -by(cases i, auto, cases P, auto, case_tac pol2, auto) - -lemma mkPinj_cn:"\y~=0; isnorm Q\ \ 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 \ isnorm Q \ 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 \ isnorm Q \ isnorm (P \ 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 \ isnorm Q \ isnorm (P \ 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 \ (x = 1) \ (x > 1)" by arith + have "x = 0 \ x = 1 \ 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 \ 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 \ 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 \ x = y \ 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 \ Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \ 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 \ isnorm Q \ isnorm (P \ Q)" -proof(induct P Q rule: mul.induct) +lemma mul_cn: "isnorm P \ isnorm Q \ isnorm (P \ 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 \ x = y \ 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 \ isnorm q \ isnorm (p \ q)" -by (simp add: sub_def add_cn neg_cn) +lemma sub_cn: "isnorm p \ isnorm q \ isnorm (p \ q)" + by (simp add: sub_def add_cn neg_cn) text {* sqr conserves normalizizedness *} -lemma sqr_cn:"isnorm P \ isnorm (sqr P)" +lemma sqr_cn: "isnorm P \ 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 \ isnorm (pow n P)" -proof (induct n arbitrary: P rule: nat_less_induct) - case (1 k) +lemma pow_cn: "isnorm P \ 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 diff -r 859fc95860c5 -r 096ec174be5d src/HOL/Decision_Procs/Ferrack.thy --- 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 \ 0" - {assume "\ ?g > 1" hence ?thesis by (simp add: Let_def simp_num_pair_def simpnum_ci) } + {assume "\ ?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' \ 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 \ ?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 \ 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 \ fm" recdef prep "measure fmsize" @@ -854,7 +856,7 @@ "prep p = p" (hints simp add: fmsize_pos) lemma prep: "\ 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 \ (fm \ fm) \ fm" where @@ -1037,7 +1039,7 @@ assumes qfp: "qfree p" shows "(Ifm bs (rlfm p) = Ifm bs p) \ 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 "\ z. \ x < z. Ifm (x#bs) (minusinf p) = Ifm (x#bs) p" (is "\ z. \ 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 diff -r 859fc95860c5 -r 096ec174be5d src/HOL/HOLCF/Representable.thy --- 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 diff -r 859fc95860c5 -r 096ec174be5d src/HOL/Imperative_HOL/Heap_Monad.thy --- 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)) diff -r 859fc95860c5 -r 096ec174be5d src/HOL/IsaMakefile --- 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 \ diff -r 859fc95860c5 -r 096ec174be5d src/HOL/Library/Abstract_Rat.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 \ int" -abbreviation - Num0_syn :: Num ("0\<^sub>N") -where "0\<^sub>N \ (0, 0)" +abbreviation Num0_syn :: Num ("0\<^sub>N") + where "0\<^sub>N \ (0, 0)" -abbreviation - Numi_syn :: "int \ Num" ("_\<^sub>N") -where "i\<^sub>N \ (i, 1)" +abbreviation Numi_syn :: "int \ Num" ("_\<^sub>N") + where "i\<^sub>N \ (i, 1)" -definition - isnormNum :: "Num \ bool" -where +definition isnormNum :: "Num \ bool" where "isnormNum = (\(a,b). (if a = 0 then b = 0 else b > 0 \ gcd a b = 1))" -definition - normNum :: "Num \ Num" -where - "normNum = (\(a,b). (if a=0 \ 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 \ Num" where + "normNum = (\(a,b). + (if a=0 \ 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 " \ a b. x = (a,b)" by auto - then obtain a b where x[simp]: "x = (a,b)" by blast - {assume "a=0 \ 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 \ b = 0" hence ?thesis by (simp add: x normNum_def isnormNum_def) } moreover - {assume anz: "a \ 0" and bnz: "b \ 0" + { assume anz: "a \ 0" and bnz: "b \ 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 \ 0" by simp with gcd_ge_0_int[of a b] + from anz bnz have "?g \ 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' \ 0" "?b' \ 0" - by - (rule notI, simp)+ - from anz bnz have stupid: "a \ 0 \ b \ 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' \ 0" "?b' \ 0" by - (rule notI, simp)+ + from anz bnz have stupid: "a \ 0 \ b \ 0" by arith from div_gcd_coprime_int[OF stupid] have gp1: "?g' = 1" . from bnz have "b < 0 \ b > 0" by arith moreover - {assume b: "b > 0" - from b have "?b' \ 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' \ 0" + { assume b: "b > 0" + from b have "?b' \ 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' \ 0" from gpos have th: "?g \ 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 \ Num \ Num" (infixl "+\<^sub>N" 60) -where - "Nadd = (\(a,b) (a',b'). if a = 0 \ b = 0 then normNum(a',b') - else if a'=0 \ b' = 0 then normNum(a,b) +definition Nadd :: "Num \ Num \ Num" (infixl "+\<^sub>N" 60) where + "Nadd = (\(a,b) (a',b'). if a = 0 \ b = 0 then normNum(a',b') + else if a'=0 \ b' = 0 then normNum(a,b) else normNum(a*b' + b*a', b*b'))" -definition - Nmul :: "Num \ Num \ Num" (infixl "*\<^sub>N" 60) -where - "Nmul = (\(a,b) (a',b'). let g = gcd (a*a') (b*b') +definition Nmul :: "Num \ Num \ Num" (infixl "*\<^sub>N" 60) where + "Nmul = (\(a,b) (a',b'). let g = gcd (a*a') (b*b') in (a*a' div g, b*b' div g))" -definition - Nneg :: "Num \ Num" ("~\<^sub>N") -where - "Nneg \ (\(a,b). (-a,b))" +definition Nneg :: "Num \ Num" ("~\<^sub>N") + where "Nneg \ (\(a,b). (-a,b))" -definition - Nsub :: "Num \ Num \ Num" (infixl "-\<^sub>N" 60) -where - "Nsub = (\a b. a +\<^sub>N ~\<^sub>N b)" +definition Nsub :: "Num \ Num \ Num" (infixl "-\<^sub>N" 60) + where "Nsub = (\a b. a +\<^sub>N ~\<^sub>N b)" -definition - Ninv :: "Num \ Num" -where - "Ninv \ \(a,b). if a < 0 then (-b, \a\) else (b,a)" +definition Ninv :: "Num \ Num" + where "Ninv = (\(a,b). if a < 0 then (-b, \a\) else (b,a))" -definition - Ndiv :: "Num \ Num \ Num" (infixl "\
\<^sub>N" 60) -where - "Ndiv \ \a b. a *\<^sub>N Ninv b" +definition Ndiv :: "Num \ Num \ Num" (infixl "\
\<^sub>N" 60) + where "Ndiv = (\a b. a *\<^sub>N Ninv b)" lemma Nneg_normN[simp]: "isnormNum x \ 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]: "\ isnormNum y\ \ 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 "\a b. x = (a,b)" and "\ 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 \0" and a': "a'\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 \0" and a': "a'\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 \ 0 \ isnormNum (i\<^sub>N)" by (simp_all add: isnormNum_def) text {* Relations over Num *} -definition - Nlt0:: "Num \ bool" ("0>\<^sub>N") -where - "Nlt0 = (\(a,b). a < 0)" +definition Nlt0:: "Num \ bool" ("0>\<^sub>N") + where "Nlt0 = (\(a,b). a < 0)" -definition - Nle0:: "Num \ bool" ("0\\<^sub>N") -where - "Nle0 = (\(a,b). a \ 0)" +definition Nle0:: "Num \ bool" ("0\\<^sub>N") + where "Nle0 = (\(a,b). a \ 0)" -definition - Ngt0:: "Num \ bool" ("0<\<^sub>N") -where - "Ngt0 = (\(a,b). a > 0)" +definition Ngt0:: "Num \ bool" ("0<\<^sub>N") + where "Ngt0 = (\(a,b). a > 0)" -definition - Nge0:: "Num \ bool" ("0\\<^sub>N") -where - "Nge0 = (\(a,b). a \ 0)" +definition Nge0:: "Num \ bool" ("0\\<^sub>N") + where "Nge0 = (\(a,b). a \ 0)" -definition - Nlt :: "Num \ Num \ bool" (infix "<\<^sub>N" 55) -where - "Nlt = (\a b. 0>\<^sub>N (a -\<^sub>N b))" +definition Nlt :: "Num \ Num \ bool" (infix "<\<^sub>N" 55) + where "Nlt = (\a b. 0>\<^sub>N (a -\<^sub>N b))" -definition - Nle :: "Num \ Num \ bool" (infix "\\<^sub>N" 55) -where - "Nle = (\a b. 0\\<^sub>N (a -\<^sub>N b))" +definition Nle :: "Num \ Num \ bool" (infix "\\<^sub>N" 55) + where "Nle = (\a b. 0\\<^sub>N (a -\<^sub>N b))" -definition - "INum = (\(a,b). of_int a / of_int b)" +definition "INum = (\(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 "\ a b a' b'. x = (a,b) \ 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 \ b = 0 \ a' = 0 \ 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 \ b = 0 \ a' = 0 \ 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 \ 0" and bz: "b \ 0" and a'z: "a'\0" and b'z: "b'\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 \ (INum x = (0::'a::{field_char_0, field_inverse_zero})) = (x = 0\<^sub>N)" +lemma isnormNum0[simp]: + "isnormNum x \ (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 "\ a b. x = (a,b)" by auto - then obtain a b where x[simp]: "x = (a,b)" by blast - {assume "a=0 \ b = 0" hence ?thesis - by (simp add: INum_def normNum_def split_def Let_def)} - moreover - {assume a: "a\0" and b: "b\0" +proof - + obtain a b where x: "x = (a, b)" by (cases x) + { assume "a = 0 \ b = 0" + hence ?thesis by (simp add: x INum_def normNum_def split_def Let_def) } + moreover + { assume a: "a \ 0" and b: "b \ 0" let ?g = "gcd a b" from a b have g: "?g \ 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 \ normNum x = normNum y" (is "?lhs = ?rhs") +lemma INum_normNum_iff: + "(INum x ::'a::{field_char_0, field_inverse_zero}) = INum y \ normNum x = normNum y" + (is "?lhs = ?rhs") proof - have "normNum x = normNum y \ (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 " \ a b. x = (a,b)" " \ 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 \ a'= 0 \ b =0 \ 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 \ a'= 0 \ b =0 \ 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 \ 0" "a'\ 0" and bb': "b \ 0" "b' \ 0" - {assume z: "a * b' + b * a' = 0" + moreover + { assume aa': "a \ 0" "a'\ 0" and bb': "b \ 0" "b' \ 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' \ 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' \ 0" let ?g = "gcd (a * b' + b * a') (b*b')" have gz: "?g \ 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 " \ a b. x = (a,b)" " \ 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 \ a'= 0 \ b = 0 \ 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 \ a'= 0 \ b = 0 \ 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 \ 0" "a' \ 0" "b \ 0" "b' \ 0" + { assume z: "a \ 0" "a' \ 0" "b \ 0" "b' \ 0" let ?g="gcd (a*a') (b*b')" have gz: "?g \ 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 \
\<^sub>N y) = INum x / (INum y ::'a :: {field_char_0, field_inverse_zero})" by (simp add: Ndiv_def) +lemma Ndiv[simp]: "INum (x \
\<^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 " \ 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\0" hence b: "(of_int b::'a) > 0" using nx by (simp add: isnormNum_def) + { assume a: "a \ 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}) \ 0) = 0\\<^sub>N x" -proof- - have " \ 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\0" hence b: "(of_int b :: 'a) > 0" using nx by (simp add: isnormNum_def) + { assume a: "a \ 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 " \ 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\0" hence b: "(of_int b::'a) > 0" using nx by (simp add: isnormNum_def) + { assume a: "a \ 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}) \ 0) = 0\\<^sub>N x" -proof- - have " \ 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\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}) \ 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 Nge0_def INum_def) } + moreover + { assume "a \ 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 "\ = (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 "\ = (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})\ INum y) = (x \\<^sub>N y)" -proof- - have "((INum x ::'a) \ INum y) = (INum (x -\<^sub>N y) \ (0::'a))" using nx ny by simp - also have "\ = (0\\<^sub>N (x -\<^sub>N y))" using Nle0_iff[OF Nsub_normN[OF ny]] by simp +proof - + have "((INum x ::'a) \ INum y) = (INum (x -\<^sub>N y) \ (0::'a))" + using nx ny by simp + also have "\ = (0\\<^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 "\ = 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 "\ = 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 "\ = (INum x = (INum y :: 'a))" by simp - also have "\ = (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 \ 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 "\ = (INum x = (INum y :: 'a))" by simp + also have "\ = (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 \ y = 0\<^sub>N)" -proof- - { fix h :: 'a - have " \ a b a' b'. x = (a,b) \ 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 \ x = 0\<^sub>N \ 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 \ 1\<^sub>N *\<^sub>N c = c" - "isnormNum c \ c *\<^sub>N (1\<^sub>N) = c" +lemma Nmul1[simp]: + "isnormNum c \ 1\<^sub>N *\<^sub>N c = c" + "isnormNum c \ 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 diff -r 859fc95860c5 -r 096ec174be5d src/HOL/Library/Library.thy --- 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 diff -r 859fc95860c5 -r 096ec174be5d src/HOL/Library/Saturated.thy --- /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 \ m = n" + by (simp add: nat_of_inject) + +lemma sat_eq_iff: + "m = n \ 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 \ '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) \ 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 \ y \ nat_of x \ nat_of y" + +definition + less_sat_def: "x < y \ 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 \ 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 \ 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 \ 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 \ 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 \ 'a sat \ 'a sat) = min" + +definition + "(sup :: 'a sat \ 'a sat \ '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 \ A" + ultimately have "fold min top A \ min x top" by (rule min_max.fold_inf_le_inf) + then show "Inf A \ x" by (simp add: Inf_sat_def) +next + fix z :: "'a sat" + fix A :: "'a sat set" + note finite + moreover assume z: "\x. x \ A \ z \ x" + ultimately have "min z top \ fold min top A" by (blast intro: min_max.inf_le_fold_inf) + then show "z \ 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 \ A" + ultimately have "max x bot \ fold max bot A" by (rule min_max.sup_le_fold_sup) + then show "x \ Sup A" by (simp add: Sup_sat_def) +next + fix z :: "'a sat" + fix A :: "'a sat set" + note finite + moreover assume z: "\x. x \ A \ x \ z" + ultimately have "fold max bot A \ max z bot" by (blast intro: min_max.fold_sup_le_sup) + then show "Sup A \ z" by (simp add: Sup_sat_def max_def bot_unique) +qed + +end + +end diff -r 859fc95860c5 -r 096ec174be5d src/HOL/Metis_Examples/Proxies.thy --- 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 "\ 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 \ 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 \ 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 \ P False \ 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 (\ a) \ \ 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) \ 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 (\ (id (\ a))) \ 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 \ b) \ 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 \ b) \ 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 \ id b \ id (a \ 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 \ id (a \ 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 \ id (a \ 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) \ id (\ b) \ id (\ (a \ 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) \ id (a \ 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 \ b) \ id (\ a \ 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) diff -r 859fc95860c5 -r 096ec174be5d src/HOL/Metis_Examples/Type_Encodings.thy --- 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 diff -r 859fc95860c5 -r 096ec174be5d src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- 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 diff -r 859fc95860c5 -r 096ec174be5d src/HOL/Nat.thy --- 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 \ b ~= 0 \ 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 \"} *} @@ -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 = diff -r 859fc95860c5 -r 096ec174be5d src/HOL/Nominal/Nominal.thy --- 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 \ "perm :: 'x prm \ ('a, 'b) nprod \ ('a, 'b) nprod" (unchecked) begin -definition +definition perm_fun :: "'x prm \ ('a \ 'b) \ 'a \ 'b" where "perm_fun pi f = (\x. pi \ f (rev pi \ x))" definition perm_bool :: "'x prm \ bool \ bool" where @@ -2262,7 +2262,7 @@ and at: "at TYPE('x)" shows "pi\(X_to_Un_supp X) = ((X_to_Un_supp (pi\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 diff -r 859fc95860c5 -r 096ec174be5d src/HOL/Tools/ATP/atp_problem.ML --- 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 ^ ")" diff -r 859fc95860c5 -r 096ec174be5d src/HOL/Tools/ATP/atp_proof.ML --- 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 ()) diff -r 859fc95860c5 -r 096ec174be5d src/HOL/Tools/ATP/atp_reconstruct.ML --- 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 diff -r 859fc95860c5 -r 096ec174be5d src/HOL/Tools/ATP/atp_systems.ML --- 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 *) diff -r 859fc95860c5 -r 096ec174be5d src/HOL/Tools/ATP/atp_translate.ML --- 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 *) diff -r 859fc95860c5 -r 096ec174be5d src/HOL/Tools/ATP/atp_util.ML --- 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 diff -r 859fc95860c5 -r 096ec174be5d src/HOL/Tools/Metis/metis_tactic.ML --- 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" diff -r 859fc95860c5 -r 096ec174be5d src/HOL/Tools/Metis/metis_translate.ML --- 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 ^ diff -r 859fc95860c5 -r 096ec174be5d src/HOL/Tools/Nitpick/nitrox.ML --- 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 diff -r 859fc95860c5 -r 096ec174be5d src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- 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 diff -r 859fc95860c5 -r 096ec174be5d src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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 = diff -r 859fc95860c5 -r 096ec174be5d src/Pure/System/isabelle_charset.scala --- 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() } } diff -r 859fc95860c5 -r 096ec174be5d src/Pure/System/isabelle_process.scala --- 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() diff -r 859fc95860c5 -r 096ec174be5d src/Pure/System/session.scala --- 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) diff -r 859fc95860c5 -r 096ec174be5d src/Tools/Code/code_haskell.ML --- 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 *) diff -r 859fc95860c5 -r 096ec174be5d src/Tools/Code/code_ml.ML --- 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 diff -r 859fc95860c5 -r 096ec174be5d src/Tools/Code/code_printer.ML --- 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)) => diff -r 859fc95860c5 -r 096ec174be5d src/Tools/Code/code_scala.ML --- 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; diff -r 859fc95860c5 -r 096ec174be5d src/Tools/Code/code_thingol.ML --- 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; diff -r 859fc95860c5 -r 096ec174be5d src/Tools/jEdit/src/document_model.scala --- 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 */ diff -r 859fc95860c5 -r 096ec174be5d src/Tools/jEdit/src/document_view.scala --- 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 diff -r 859fc95860c5 -r 096ec174be5d src/Tools/jEdit/src/session_dockable.scala --- 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) diff -r 859fc95860c5 -r 096ec174be5d src/Tools/nbe.ML --- 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)]))];