merged
authorhuffman
Tue Sep 06 07:41:15 2011 -0700 (2011-09-06)
changeset 44747ab7522fbe1a2
parent 44746 9e4f7d3b5376
parent 44744 bdf8eb8f126b
child 44748 7f6838b3474a
merged
     1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Mon Sep 05 22:30:25 2011 -0700
     1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Tue Sep 06 07:41:15 2011 -0700
     1.3 @@ -108,11 +108,11 @@
     1.4  results are correct by construction.
     1.5  
     1.6  In this manual, we will explicitly invoke the \textbf{sledgehammer} command.
     1.7 -Sledgehammer also provides an automatic mode that can be enabled via the
     1.8 -``Auto Sledgehammer'' option from the ``Isabelle'' menu in Proof General. In
     1.9 -this mode, Sledgehammer is run on every newly entered theorem. The time limit
    1.10 -for Auto Sledgehammer and other automatic tools can be set using the ``Auto
    1.11 -Tools Time Limit'' option.
    1.12 +Sledgehammer also provides an automatic mode that can be enabled via the ``Auto
    1.13 +Sledgehammer'' option in Proof General's ``Isabelle'' menu. In this mode,
    1.14 +Sledgehammer is run on every newly entered theorem. The time limit for Auto
    1.15 +Sledgehammer and other automatic tools can be set using the ``Auto Tools Time
    1.16 +Limit'' option.
    1.17  
    1.18  \newbox\boxA
    1.19  \setbox\boxA=\hbox{\texttt{nospam}}
    1.20 @@ -633,8 +633,8 @@
    1.21  highly-relevant and \qty{facts\/_{\mathrm{2}}} fully irrelevant.
    1.22  
    1.23  You can instruct Sledgehammer to run automatically on newly entered theorems by
    1.24 -enabling the ``Auto Sledgehammer'' option from the ``Isabelle'' menu in Proof
    1.25 -General. For automatic runs, only the first prover set using \textit{provers}
    1.26 +enabling the ``Auto Sledgehammer'' option in Proof General's ``Isabelle'' menu.
    1.27 +For automatic runs, only the first prover set using \textit{provers}
    1.28  (\S\ref{mode-of-operation}) is considered, fewer facts are passed to the prover,
    1.29  \textit{slicing} (\S\ref{mode-of-operation}) is disabled, \textit{sound}
    1.30  (\S\ref{problem-encoding}) is enabled, \textit{verbose} (\S\ref{output-format})
    1.31 @@ -724,7 +724,7 @@
    1.32  
    1.33  \item[$\bullet$] \textbf{\textit{leo2}:} LEO-II is an automatic
    1.34  higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},
    1.35 -with support for the TPTP higher-order syntax (THF).
    1.36 +with support for the TPTP many-typed higher-order syntax (THF0).
    1.37  
    1.38  \item[$\bullet$] \textbf{\textit{metis}:} Although it is much less powerful than
    1.39  the external provers, Metis itself can be used for proof search.
    1.40 @@ -737,7 +737,7 @@
    1.41  
    1.42  \item[$\bullet$] \textbf{\textit{satallax}:} Satallax is an automatic
    1.43  higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with
    1.44 -support for the TPTP higher-order syntax (THF).
    1.45 +support for the TPTP many-typed higher-order syntax (THF0).
    1.46  
    1.47  \item[$\bullet$] \textbf{\textit{spass}:} SPASS is a first-order resolution
    1.48  prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}.
    1.49 @@ -752,7 +752,7 @@
    1.50  \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire}
    1.51  executable and \texttt{VAMPIRE\_VERSION} to the version number (e.g., ``1.8'').
    1.52  Sledgehammer has been tested with versions 0.6, 1.0, and 1.8. Vampire 1.8
    1.53 -supports the TPTP many-typed first-order format (TFF).
    1.54 +supports the TPTP many-typed first-order format (TFF0).
    1.55  
    1.56  \item[$\bullet$] \textbf{\textit{yices}:} Yices is an SMT solver developed at
    1.57  SRI \cite{yices}. To use Yices, set the environment variable
    1.58 @@ -767,7 +767,7 @@
    1.59  
    1.60  \item[$\bullet$] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be
    1.61  an ATP, exploiting Z3's support for the TPTP untyped and many-typed first-order
    1.62 -formats (FOF and TFF). It is included for experimental purposes. It requires
    1.63 +formats (FOF and TFF0). It is included for experimental purposes. It requires
    1.64  version 3.0 or above.
    1.65  \end{enum}
    1.66  
    1.67 @@ -787,7 +787,7 @@
    1.68  
    1.69  \item[$\bullet$] \textbf{\textit{remote\_e\_tofof}:} E-ToFoF is a metaprover
    1.70  developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami
    1.71 -servers. This ATP supports the TPTP many-typed first-order format (TFF). The
    1.72 +servers. This ATP supports the TPTP many-typed first-order format (TFF0). The
    1.73  remote version of E-ToFoF runs on Geoff Sutcliffe's Miami servers.
    1.74  
    1.75  \item[$\bullet$] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II
    1.76 @@ -798,7 +798,7 @@
    1.77  
    1.78  \item[$\bullet$] \textbf{\textit{remote\_snark}:} SNARK is a first-order
    1.79  resolution prover developed by Stickel et al.\ \cite{snark}. It supports the
    1.80 -TPTP many-typed first-order format (TFF). The remote version of SNARK runs on
    1.81 +TPTP many-typed first-order format (TFF0). The remote version of SNARK runs on
    1.82  Geoff Sutcliffe's Miami servers.
    1.83  
    1.84  \item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of
    1.85 @@ -818,17 +818,16 @@
    1.86  with TPTP syntax'' runs on Geoff Sutcliffe's Miami servers.
    1.87  \end{enum}
    1.88  
    1.89 -By default, Sledgehammer will run E, E-SInE, SPASS, Vampire, Z3 (or whatever
    1.90 +By default, Sledgehammer runs E, E-SInE, SPASS, Vampire, Z3 (or whatever
    1.91  the SMT module's \textit{smt\_solver} configuration option is set to), and (if
    1.92  appropriate) Waldmeister in parallel---either locally or remotely, depending on
    1.93  the number of processor cores available. For historical reasons, the default
    1.94  value of this option can be overridden using the option ``Sledgehammer:
    1.95 -Provers'' from the ``Isabelle'' menu in Proof General.
    1.96 +Provers'' in Proof General's ``Isabelle'' menu.
    1.97  
    1.98 -It is a good idea to run several provers in parallel, although it could slow
    1.99 -down your machine. Running E, SPASS, and Vampire for 5~seconds yields a similar
   1.100 -success rate to running the most effective of these for 120~seconds
   1.101 -\cite{boehme-nipkow-2010}.
   1.102 +It is generally a good idea to run several provers in parallel. Running E,
   1.103 +SPASS, and Vampire for 5~seconds yields a similar success rate to running the
   1.104 +most effective of these for 120~seconds \cite{boehme-nipkow-2010}.
   1.105  
   1.106  For the \textit{min} subcommand, the default prover is \textit{metis}. If
   1.107  several provers are set, the first one is used.
   1.108 @@ -884,7 +883,13 @@
   1.109  Specifies the type encoding to use in ATP problems. Some of the type encodings
   1.110  are unsound, meaning that they can give rise to spurious proofs
   1.111  (unreconstructible using Metis). The supported type encodings are listed below,
   1.112 -with an indication of their soundness in parentheses:
   1.113 +with an indication of their soundness in parentheses.
   1.114 +%
   1.115 +All the encodings with \textit{guards} or \textit{tags} in their name are
   1.116 +available in a ``uniform'' and a ``nonuniform'' variant. The nonuniform variants
   1.117 +are generally more efficient and are the default; the uniform variants are
   1.118 +identified by the suffix \textit{\_uniform} (e.g.,
   1.119 +\textit{mono\_guards\_uniform}{?}).
   1.120  
   1.121  \begin{enum}
   1.122  \item[$\bullet$] \textbf{\textit{erased} (very unsound):} No type information is
   1.123 @@ -926,27 +931,27 @@
   1.124  $\mathit{type\/}(\tau, t)$ becomes a unary function
   1.125  $\mathit{type\_}\tau(t)$.
   1.126  
   1.127 -\item[$\bullet$] \textbf{\textit{simple} (sound):} Exploit simple first-order
   1.128 -types if the prover supports the TFF or THF syntax; otherwise, fall back on
   1.129 -\textit{mono\_guards}. The problem is monomorphized.
   1.130 +\item[$\bullet$] \textbf{\textit{mono\_simple} (sound):} Exploits simple
   1.131 +first-order types if the prover supports the TFF0 or THF0 syntax; otherwise,
   1.132 +falls back on \textit{mono\_guards\_uniform}. The problem is monomorphized.
   1.133  
   1.134 -\item[$\bullet$] \textbf{\textit{simple\_higher} (sound):} Exploit simple
   1.135 -higher-order types if the prover supports the THF syntax; otherwise, fall back
   1.136 -on \textit{simple} or \textit{mono\_guards\_uniform}. The problem is
   1.137 +\item[$\bullet$] \textbf{\textit{mono\_simple\_higher} (sound):} Exploits simple
   1.138 +higher-order types if the prover supports the THF0 syntax; otherwise, falls back
   1.139 +on \textit{mono\_simple} or \textit{mono\_guards\_uniform}. The problem is
   1.140  monomorphized.
   1.141  
   1.142  \item[$\bullet$]
   1.143  \textbf{%
   1.144  \textit{poly\_guards}?, \textit{poly\_tags}?, \textit{raw\_mono\_guards}?, \\
   1.145  \textit{raw\_mono\_tags}?, \textit{mono\_guards}?, \textit{mono\_tags}?, \\
   1.146 -\textit{simple}? (quasi-sound):} \\
   1.147 +\textit{mono\_simple}? (quasi-sound):} \\
   1.148  The type encodings \textit{poly\_guards}, \textit{poly\_tags},
   1.149  \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
   1.150 -\textit{mono\_tags}, and \textit{simple} are fully
   1.151 +\textit{mono\_tags}, and \textit{mono\_simple} are fully
   1.152  typed and sound. For each of these, Sledgehammer also provides a lighter,
   1.153  virtually sound variant identified by a question mark (`{?}')\ that detects and
   1.154 -erases monotonic types, notably infinite types. (For \textit{simple}, the types
   1.155 -are not actually erased but rather replaced by a shared uniform type of
   1.156 +erases monotonic types, notably infinite types. (For \textit{mono\_simple}, the
   1.157 +types are not actually erased but rather replaced by a shared uniform type of
   1.158  individuals.) As argument to the \textit{metis} proof method, the question mark
   1.159  is replaced by a \hbox{``\textit{\_query}''} suffix. If the \emph{sound} option
   1.160  is enabled, these encodings are fully sound.
   1.161 @@ -954,30 +959,25 @@
   1.162  \item[$\bullet$]
   1.163  \textbf{%
   1.164  \textit{poly\_guards}!, \textit{poly\_tags}!, \textit{raw\_mono\_guards}!, \\
   1.165 -\textit{raw\_mono\_tags}!, \textit{mono\_guards}!, \textit{mono\_tags}!, \textit{simple}!, \\
   1.166 -\textit{simple\_higher}! (mildly unsound):} \\
   1.167 +\textit{raw\_mono\_tags}!, \textit{mono\_guards}!, \textit{mono\_tags}!, \\
   1.168 +\textit{mono\_simple}!, \textit{mono\_simple\_higher}! (mildly unsound):} \\
   1.169  The type encodings \textit{poly\_guards}, \textit{poly\_tags},
   1.170  \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
   1.171 -\textit{mono\_tags}, \textit{simple}, and \textit{simple\_higher} also admit
   1.172 -a mildly unsound (but very efficient) variant identified by an exclamation mark
   1.173 -(`{!}') that detects and erases erases all types except those that are clearly
   1.174 -finite (e.g., \textit{bool}). (For \textit{simple} and \textit{simple\_higher},
   1.175 -the types are not actually erased but rather replaced by a shared uniform type
   1.176 -of individuals.) As argument to the \textit{metis} proof method, the exclamation
   1.177 -mark is replaced by the suffix \hbox{``\textit{\_bang}''}.
   1.178 +\textit{mono\_tags}, \textit{mono\_simple}, and \textit{mono\_simple\_higher}
   1.179 +also admit a mildly unsound (but very efficient) variant identified by an
   1.180 +exclamation mark (`{!}') that detects and erases erases all types except those
   1.181 +that are clearly finite (e.g., \textit{bool}). (For \textit{mono\_simple} and
   1.182 +\textit{mono\_simple\_higher}, the types are not actually erased but rather
   1.183 +replaced by a shared uniform type of individuals.) As argument to the
   1.184 +\textit{metis} proof method, the exclamation mark is replaced by the suffix
   1.185 +\hbox{``\textit{\_bang}''}.
   1.186  
   1.187  \item[$\bullet$] \textbf{\textit{smart}:} The actual encoding used depends on
   1.188  the ATP and should be the most efficient virtually sound encoding for that ATP.
   1.189  \end{enum}
   1.190  
   1.191 -In addition, all the \textit{guards} and \textit{tags} type encodings are
   1.192 -available in two variants, a ``uniform'' and a ``nonuniform'' variant. The
   1.193 -nonuniform variants are generally more efficient and are the default; the
   1.194 -uniform variants are identified by the suffix \textit{\_uniform} (e.g.,
   1.195 -\textit{mono\_guards\_uniform}{?}).
   1.196 -
   1.197 -For SMT solvers, the type encoding is always \textit{simple}, irrespective of
   1.198 -the value of this option.
   1.199 +For SMT solvers, the type encoding is always \textit{mono\_simple}, irrespective
   1.200 +of the value of this option.
   1.201  
   1.202  \nopagebreak
   1.203  {\small See also \textit{max\_new\_mono\_instances} (\S\ref{relevance-filter})
   1.204 @@ -1091,8 +1091,7 @@
   1.205  Specifies the maximum number of seconds that the automatic provers should spend
   1.206  searching for a proof. This excludes problem preparation and is a soft limit.
   1.207  For historical reasons, the default value of this option can be overridden using
   1.208 -the option ``Sledgehammer: Time Limit'' from the ``Isabelle'' menu in Proof
   1.209 -General.
   1.210 +the option ``Sledgehammer: Time Limit'' in Proof General's ``Isabelle'' menu.
   1.211  
   1.212  \opdefault{preplay\_timeout}{float\_or\_none}{\upshape 4}
   1.213  Specifies the maximum number of seconds that Metis should be spent trying to
     2.1 --- a/src/HOL/Finite_Set.thy	Mon Sep 05 22:30:25 2011 -0700
     2.2 +++ b/src/HOL/Finite_Set.thy	Tue Sep 06 07:41:15 2011 -0700
     2.3 @@ -2054,6 +2054,11 @@
     2.4   apply(auto intro:ccontr)
     2.5  done
     2.6  
     2.7 +lemma card_le_Suc_iff: "finite A \<Longrightarrow>
     2.8 +  Suc n \<le> card A = (\<exists>a B. A = insert a B \<and> a \<notin> B \<and> n \<le> card B \<and> finite B)"
     2.9 +by (fastsimp simp: card_Suc_eq less_eq_nat.simps(2) insert_eq_iff
    2.10 +  dest: subset_singletonD split: nat.splits if_splits)
    2.11 +
    2.12  lemma finite_fun_UNIVD2:
    2.13    assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
    2.14    shows "finite (UNIV :: 'b set)"
     3.1 --- a/src/HOL/Fun.thy	Mon Sep 05 22:30:25 2011 -0700
     3.2 +++ b/src/HOL/Fun.thy	Tue Sep 06 07:41:15 2011 -0700
     3.3 @@ -612,6 +612,10 @@
     3.4  lemma fun_upd_comp: "f \<circ> (g(x := y)) = (f \<circ> g)(x := f y)"
     3.5  by (auto intro: ext)
     3.6  
     3.7 +lemma UNION_fun_upd:
     3.8 +  "UNION J (A(i:=B)) = (UNION (J-{i}) A \<union> (if i\<in>J then B else {}))"
     3.9 +by (auto split: if_splits)
    3.10 +
    3.11  
    3.12  subsection {* @{text override_on} *}
    3.13  
     4.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Mon Sep 05 22:30:25 2011 -0700
     4.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Tue Sep 06 07:41:15 2011 -0700
     4.3 @@ -12,17 +12,20 @@
     4.4  
     4.5  import_theory bool;
     4.6  
     4.7 +type_maps
     4.8 +  bool            > HOL.bool;
     4.9 +
    4.10  const_maps
    4.11 -  T               > True
    4.12 -  F               > False
    4.13 -  "!"             > All
    4.14 +  T               > HOL.True
    4.15 +  F               > HOL.False
    4.16 +  "!"             > HOL.All
    4.17    "/\\"           > HOL.conj
    4.18    "\\/"           > HOL.disj
    4.19 -  "?"             > Ex
    4.20 -  "?!"            > Ex1
    4.21 -  "~"             > Not
    4.22 +  "?"             > HOL.Ex
    4.23 +  "?!"            > HOL.Ex1
    4.24 +  "~"             > HOL.Not
    4.25    COND            > HOL.If
    4.26 -  bool_case       > Datatype.bool.bool_case
    4.27 +  bool_case       > Product_Type.bool.bool_case
    4.28    ONE_ONE         > HOL4Setup.ONE_ONE
    4.29    ONTO            > Fun.surj
    4.30    TYPE_DEFINITION > HOL4Setup.TYPE_DEFINITION
    4.31 @@ -46,7 +49,7 @@
    4.32  import_theory sum;
    4.33  
    4.34  type_maps
    4.35 -  sum > "+";
    4.36 +  sum > Sum_Type.sum;
    4.37  
    4.38  const_maps
    4.39    INL      > Sum_Type.Inl
    4.40 @@ -55,7 +58,7 @@
    4.41    ISR      > HOL4Compat.ISR
    4.42    OUTL     > HOL4Compat.OUTL
    4.43    OUTR     > HOL4Compat.OUTR
    4.44 -  sum_case > Datatype.sum.sum_case;
    4.45 +  sum_case > Sum_Type.sum.sum_case;
    4.46  
    4.47  ignore_thms
    4.48    sum_TY_DEF
    4.49 @@ -63,7 +66,6 @@
    4.50    IS_SUM_REP
    4.51    INL_DEF
    4.52    INR_DEF
    4.53 -  sum_axiom
    4.54    sum_Axiom;
    4.55  
    4.56  end_import;
    4.57 @@ -125,13 +127,13 @@
    4.58      prod > Product_Type.prod;
    4.59  
    4.60  const_maps
    4.61 -    ","       > Pair
    4.62 -    FST       > fst
    4.63 -    SND       > snd
    4.64 -    CURRY     > curry
    4.65 -    UNCURRY   > split
    4.66 -    "##"      > map_pair
    4.67 -    pair_case > split;
    4.68 +    ","       > Product_Type.Pair
    4.69 +    FST       > Product_Type.fst
    4.70 +    SND       > Product_Type.snd
    4.71 +    CURRY     > Product_Type.curry
    4.72 +    UNCURRY   > Product_Type.prod.prod_case
    4.73 +    "##"      > Product_Type.map_pair
    4.74 +    pair_case > Product_Type.prod.prod_case;
    4.75  
    4.76  ignore_thms
    4.77      prod_TY_DEF
    4.78 @@ -145,11 +147,11 @@
    4.79  import_theory num;
    4.80  
    4.81  type_maps
    4.82 -  num > nat;
    4.83 +  num > Nat.nat;
    4.84  
    4.85  const_maps
    4.86 -  SUC > Suc
    4.87 -  0   > 0 :: nat;
    4.88 +  SUC > Nat.Suc
    4.89 +  0   > Groups.zero_class.zero :: nat;
    4.90  
    4.91  ignore_thms
    4.92      num_TY_DEF
    4.93 @@ -165,7 +167,7 @@
    4.94  import_theory prim_rec;
    4.95  
    4.96  const_maps
    4.97 -    "<" > Orderings.less :: "[nat,nat]=>bool";
    4.98 +    "<" > Orderings.ord_class.less :: "nat \<Rightarrow> nat \<Rightarrow> bool";
    4.99  
   4.100  end_import;
   4.101  
   4.102 @@ -180,15 +182,15 @@
   4.103    ">"          > HOL4Compat.nat_gt
   4.104    ">="         > HOL4Compat.nat_ge
   4.105    FUNPOW       > HOL4Compat.FUNPOW
   4.106 -  "<="         > Orderings.less_eq :: "[nat,nat]=>bool"
   4.107 -  "+"          > Groups.plus :: "[nat,nat]=>nat"
   4.108 -  "*"          > Groups.times :: "[nat,nat]=>nat"
   4.109 -  "-"          > Groups.minus :: "[nat,nat]=>nat"
   4.110 -  MIN          > Orderings.min :: "[nat,nat]=>nat"
   4.111 -  MAX          > Orderings.max :: "[nat,nat]=>nat"
   4.112 -  DIV          > Divides.div :: "[nat,nat]=>nat"
   4.113 -  MOD          > Divides.mod :: "[nat,nat]=>nat"
   4.114 -  EXP          > Power.power :: "[nat,nat]=>nat";
   4.115 +  "<="         > Orderings.ord_class.less_eq :: "nat \<Rightarrow> nat \<Rightarrow> bool"
   4.116 +  "+"          > Groups.plus_class.plus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   4.117 +  "*"          > Groups.times_class.times :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   4.118 +  "-"          > Groups.minus_class.minus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   4.119 +  MIN          > Orderings.ord_class.min :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   4.120 +  MAX          > Orderings.ord_class.max :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   4.121 +  DIV          > Divides.div_class.div :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   4.122 +  MOD          > Divides.div_class.mod :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   4.123 +  EXP          > Power.power_class.power :: "nat \<Rightarrow> nat \<Rightarrow> nat";
   4.124  
   4.125  end_import;
   4.126  
   4.127 @@ -207,7 +209,7 @@
   4.128  import_theory divides;
   4.129  
   4.130  const_maps
   4.131 -  divides > Divides.times_class.dvd :: "[nat,nat]=>bool";
   4.132 +  divides > Rings.dvd_class.dvd :: "nat \<Rightarrow> nat \<Rightarrow> bool";
   4.133  
   4.134  end_import;
   4.135  
   4.136 @@ -227,7 +229,7 @@
   4.137    HD        > List.hd
   4.138    TL        > List.tl
   4.139    MAP       > List.map
   4.140 -  MEM       > "List.op mem"
   4.141 +  MEM       > HOL4Compat.list_mem
   4.142    FILTER    > List.filter
   4.143    FOLDL     > List.foldl
   4.144    EVERY     > List.list_all
   4.145 @@ -236,12 +238,12 @@
   4.146    FRONT     > List.butlast
   4.147    APPEND    > List.append
   4.148    FLAT      > List.concat
   4.149 -  LENGTH    > Nat.size
   4.150 +  LENGTH    > Nat.size_class.size
   4.151    REPLICATE > List.replicate
   4.152    list_size > HOL4Compat.list_size
   4.153    SUM       > HOL4Compat.sum
   4.154    FOLDR     > HOL4Compat.FOLDR
   4.155 -  EXISTS    > HOL4Compat.list_exists
   4.156 +  EXISTS    > List.list_ex
   4.157    MAP2      > HOL4Compat.map2
   4.158    ZIP       > HOL4Compat.ZIP
   4.159    UNZIP     > HOL4Compat.unzip;
     5.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Mon Sep 05 22:30:25 2011 -0700
     5.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Tue Sep 06 07:41:15 2011 -0700
     5.3 @@ -16,13 +16,17 @@
     5.4    real > RealDef.real;
     5.5  
     5.6  const_maps
     5.7 -  real_0   > Groups.zero      :: real
     5.8 -  real_1   > Groups.one       :: real
     5.9 -  real_neg > Groups.uminus    :: "real => real"
    5.10 -  inv      > Groups.inverse   :: "real => real"
    5.11 -  real_add > Groups.plus      :: "[real,real] => real"
    5.12 -  real_mul > Groups.times     :: "[real,real] => real"
    5.13 -  real_lt  > Orderings.less      :: "[real,real] => bool";
    5.14 +  real_0   > Groups.zero_class.zero :: real
    5.15 +  real_1   > Groups.one_class.one   :: real
    5.16 +  real_neg > Groups.uminus_class.uminus :: "real \<Rightarrow> real"
    5.17 +  inv > Fields.inverse_class.inverse :: "real \<Rightarrow> real"
    5.18 +  real_add > Groups.plus_class.plus :: "real \<Rightarrow> real \<Rightarrow> real"
    5.19 +  real_sub > Groups.minus_class.minus :: "real \<Rightarrow> real \<Rightarrow> real"
    5.20 +  real_mul > Groups.times_class.times :: "real \<Rightarrow> real \<Rightarrow> real"
    5.21 +  real_div > Fields.inverse_class.divide :: "real \<Rightarrow> real \<Rightarrow> real"
    5.22 +  real_lt > Orderings.ord_class.less :: "real \<Rightarrow> real \<Rightarrow> bool"
    5.23 +  mk_real > HOL.undefined   (* Otherwise proof_import_concl fails *)
    5.24 +  dest_real > HOL.undefined
    5.25  
    5.26  ignore_thms
    5.27      real_TY_DEF
    5.28 @@ -50,11 +54,11 @@
    5.29  const_maps
    5.30    real_gt     > HOL4Compat.real_gt
    5.31    real_ge     > HOL4Compat.real_ge
    5.32 -  real_lte    > Orderings.less_eq :: "[real,real] => bool"
    5.33 -  real_sub    > Groups.minus :: "[real,real] => real"
    5.34 -  "/"         > Fields.divide :: "[real,real] => real"
    5.35 -  pow         > Power.power :: "[real,nat] => real"
    5.36 -  abs         > Groups.abs :: "real => real"
    5.37 +  real_lte    > Orderings.ord_class.less_eq :: "real \<Rightarrow> real \<Rightarrow> bool"
    5.38 +  real_sub    > Groups.minus_class.minus :: "real \<Rightarrow> real \<Rightarrow> real"
    5.39 +  "/"         > Fields.inverse_class.divide :: "real \<Rightarrow> real \<Rightarrow> real"
    5.40 +  pow         > Power.power_class.power :: "real \<Rightarrow> nat \<Rightarrow> real"
    5.41 +  abs         > Groups.abs_class.abs :: "real => real"
    5.42    real_of_num > RealDef.real :: "nat => real";
    5.43  
    5.44  end_import;
     6.1 --- a/src/HOL/Import/HOL4Compat.thy	Mon Sep 05 22:30:25 2011 -0700
     6.2 +++ b/src/HOL/Import/HOL4Compat.thy	Tue Sep 06 07:41:15 2011 -0700
     6.3 @@ -63,6 +63,14 @@
     6.4  lemma OUTR: "OUTR (Inr x) = x"
     6.5    by simp
     6.6  
     6.7 +lemma sum_axiom: "EX! h. h o Inl = f & h o Inr = g"
     6.8 +  apply (intro allI ex1I[of _ "sum_case f g"] conjI)
     6.9 +  apply (simp_all add: o_def fun_eq_iff)
    6.10 +  apply (rule)
    6.11 +  apply (induct_tac x)
    6.12 +  apply simp_all
    6.13 +  done
    6.14 +
    6.15  lemma sum_case_def: "(ALL f g x. sum_case f g (Inl x) = f x) & (ALL f g y. sum_case f g (Inr y) = g y)"
    6.16    by simp
    6.17  
    6.18 @@ -491,4 +499,6 @@
    6.19  lemma real_ge: "ALL x y. (y <= x) = (y <= x)"
    6.20    by simp
    6.21  
    6.22 +definition [hol4rew]: "list_mem x xs = List.member xs x"
    6.23 +
    6.24  end
     7.1 --- a/src/HOL/Set.thy	Mon Sep 05 22:30:25 2011 -0700
     7.2 +++ b/src/HOL/Set.thy	Tue Sep 06 07:41:15 2011 -0700
     7.3 @@ -785,6 +785,26 @@
     7.4  lemma insert_ident: "x ~: A ==> x ~: B ==> (insert x A = insert x B) = (A = B)"
     7.5  by auto
     7.6  
     7.7 +lemma insert_eq_iff: assumes "a \<notin> A" "b \<notin> B"
     7.8 +shows "insert a A = insert b B \<longleftrightarrow>
     7.9 +  (if a=b then A=B else \<exists>C. A = insert b C \<and> b \<notin> C \<and> B = insert a C \<and> a \<notin> C)"
    7.10 +  (is "?L \<longleftrightarrow> ?R")
    7.11 +proof
    7.12 +  assume ?L
    7.13 +  show ?R
    7.14 +  proof cases
    7.15 +    assume "a=b" with assms `?L` show ?R by (simp add: insert_ident)
    7.16 +  next
    7.17 +    assume "a\<noteq>b"
    7.18 +    let ?C = "A - {b}"
    7.19 +    have "A = insert b ?C \<and> b \<notin> ?C \<and> B = insert a ?C \<and> a \<notin> ?C"
    7.20 +      using assms `?L` `a\<noteq>b` by auto
    7.21 +    thus ?R using `a\<noteq>b` by auto
    7.22 +  qed
    7.23 +next
    7.24 +  assume ?R thus ?L by(auto split: if_splits)
    7.25 +qed
    7.26 +
    7.27  subsubsection {* Singletons, using insert *}
    7.28  
    7.29  lemma singletonI [intro!,no_atp]: "a : {a}"
     8.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Mon Sep 05 22:30:25 2011 -0700
     8.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Sep 06 07:41:15 2011 -0700
     8.3 @@ -263,7 +263,7 @@
     8.4        | str _ (ATyAbs (ss, ty)) =
     8.5          tptp_pi_binder ^ "[" ^
     8.6          commas (map (suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types))
     8.7 -                    ss) ^ "] : " ^ str false ty
     8.8 +                    ss) ^ "]: " ^ str false ty
     8.9    in str true ty end
    8.10  
    8.11  fun string_for_type (THF0 _) ty = str_for_type ty
    8.12 @@ -308,7 +308,7 @@
    8.13         | (_, true, [AAbs ((s', ty), tm)]) =>
    8.14           (*There is code in ATP_Translate to ensure that Eps is always applied
    8.15             to an abstraction*)
    8.16 -         tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "] : " ^
    8.17 +         tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^
    8.18             string_for_term format tm ^ ""
    8.19           |> enclose "(" ")"
    8.20  
    8.21 @@ -320,12 +320,12 @@
    8.22               s ^ "(" ^ commas ss ^ ")"
    8.23           end)
    8.24    | string_for_term (format as THF0 _) (AAbs ((s, ty), tm)) =
    8.25 -    "(^[" ^ s ^ " : " ^ string_for_type format ty ^ "] : " ^
    8.26 +    "(^[" ^ s ^ " : " ^ string_for_type format ty ^ "]: " ^
    8.27      string_for_term format tm ^ ")"
    8.28    | string_for_term _ _ = raise Fail "unexpected term in first-order format"
    8.29  and string_for_formula format (AQuant (q, xs, phi)) =
    8.30      string_for_quantifier q ^
    8.31 -    "[" ^ commas (map (string_for_bound_var format) xs) ^ "] : " ^
    8.32 +    "[" ^ commas (map (string_for_bound_var format) xs) ^ "]: " ^
    8.33      string_for_formula format phi
    8.34      |> enclose "(" ")"
    8.35    | string_for_formula format
     9.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Sep 05 22:30:25 2011 -0700
     9.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Sep 06 07:41:15 2011 -0700
     9.3 @@ -579,14 +579,18 @@
     9.4    |> (fn (poly, (level, (uniformity, core))) =>
     9.5           case (core, (poly, level, uniformity)) of
     9.6             ("simple", (SOME poly, _, Nonuniform)) =>
     9.7 -           (case poly of
     9.8 -              Raw_Monomorphic => raise Same.SAME
     9.9 -            | _ => Simple_Types (First_Order, poly, level))
    9.10 +           (case (poly, level) of
    9.11 +              (Polymorphic, All_Types) =>
    9.12 +              Simple_Types (First_Order, Polymorphic, All_Types)
    9.13 +            | (Mangled_Monomorphic, _) =>
    9.14 +              Simple_Types (First_Order, Mangled_Monomorphic, level)
    9.15 +            | _ => raise Same.SAME)
    9.16           | ("simple_higher", (SOME poly, _, Nonuniform)) =>
    9.17             (case (poly, level) of
    9.18 -              (Raw_Monomorphic, _) => raise Same.SAME
    9.19 -            | (_, Noninf_Nonmono_Types _) => raise Same.SAME
    9.20 -            | _ => Simple_Types (Higher_Order, poly, level))
    9.21 +              (_, Noninf_Nonmono_Types _) => raise Same.SAME
    9.22 +            | (Mangled_Monomorphic, _) =>
    9.23 +              Simple_Types (Higher_Order, Mangled_Monomorphic, level)
    9.24 +            | _ => raise Same.SAME)
    9.25           | ("guards", (SOME poly, _, _)) => Guards (poly, level, uniformity)
    9.26           | ("tags", (SOME Polymorphic, _, _)) =>
    9.27             Tags (Polymorphic, level, uniformity)
    9.28 @@ -1369,16 +1373,14 @@
    9.29  
    9.30  fun filter_type_args _ _ _ [] = []
    9.31    | filter_type_args thy s arity T_args =
    9.32 -    let val U = robust_const_type thy s in
    9.33 -      case Term.add_tvarsT (U |> chop_fun arity |> snd) [] of
    9.34 -        [] => []
    9.35 -      | res_U_vars =>
    9.36 -        let val U_args = (s, U) |> Sign.const_typargs thy in
    9.37 -          U_args ~~ T_args
    9.38 -          |> map (fn (U, T) =>
    9.39 -                     if member (op =) res_U_vars (dest_TVar U) then T
    9.40 -                     else dummyT)
    9.41 -        end
    9.42 +    let
    9.43 +      val U = robust_const_type thy s
    9.44 +      val arg_U_vars = fold Term.add_tvarsT (U |> chop_fun arity |> fst) []
    9.45 +      val U_args = (s, U) |> robust_const_typargs thy
    9.46 +    in
    9.47 +      U_args ~~ T_args
    9.48 +      |> map (fn (U, T) =>
    9.49 +                 if member (op =) arg_U_vars (dest_TVar U) then dummyT else T)
    9.50      end
    9.51      handle TYPE _ => T_args
    9.52  
    9.53 @@ -1394,14 +1396,13 @@
    9.54           | SOME s'' =>
    9.55             let
    9.56               val s'' = invert_const s''
    9.57 -             fun filtered_T_args false = T_args
    9.58 -               | filtered_T_args true = filter_type_args thy s'' arity T_args
    9.59 +             fun filter_T_args false = T_args
    9.60 +               | filter_T_args true = filter_type_args thy s'' arity T_args
    9.61             in
    9.62               case type_arg_policy type_enc s'' of
    9.63 -               Explicit_Type_Args drop_args =>
    9.64 -               (name, filtered_T_args drop_args)
    9.65 +               Explicit_Type_Args drop_args => (name, filter_T_args drop_args)
    9.66               | Mangled_Type_Args drop_args =>
    9.67 -               (mangled_const_name format type_enc (filtered_T_args drop_args)
    9.68 +               (mangled_const_name format type_enc (filter_T_args drop_args)
    9.69                                     name, [])
    9.70               | No_Type_Args => (name, [])
    9.71             end)
    9.72 @@ -1555,9 +1556,8 @@
    9.73    let
    9.74      fun add (Const (@{const_name Meson.skolem}, _) $ _) = I
    9.75        | add (t $ u) = add t #> add u
    9.76 -      | add (Const (x as (s, _))) =
    9.77 -        if String.isPrefix skolem_const_prefix s then I
    9.78 -        else x |> Sign.const_typargs thy |> fold (fold_type_constrs set_insert)
    9.79 +      | add (Const x) =
    9.80 +        x |> robust_const_typargs thy |> fold (fold_type_constrs set_insert)
    9.81        | add (Free (s, T)) =
    9.82          if String.isPrefix polymorphic_free_prefix s then
    9.83            T |> fold_type_constrs set_insert