# HG changeset patch
# User wenzelm
# Date 1314880551 -7200
# Node ID 74fb317aaeb547059180635410159097b7f98864
# Parent  13f86edf3db36837ba0a9a6be844c86609a07ea0# Parent  5db68864a967eecf825a313e58a5340f7e56b299
merged

diff -r 5db68864a967 -r 74fb317aaeb5 src/HOL/Import/HOLLight/HOLLight.thy
--- a/src/HOL/Import/HOLLight/HOLLight.thy	Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Import/HOLLight/HOLLight.thy	Thu Sep 01 14:35:51 2011 +0200
@@ -759,12 +759,12 @@
 ==> EX f::nat => 'A. ALL x::nat. f x = H f x"
   by (import hollight WF_REC_num)
 
-lemma WF_MEASURE: "wfP (%(a::'A) b::'A. measure (m::'A => nat) (a, b))"
+lemma WF_MEASURE: "wfP (%(a::'A) b::'A. (a, b) : measure (m::'A => nat))"
   by (import hollight WF_MEASURE)
 
 lemma MEASURE_LE: "(ALL x::'q_12099.
-    measure (m::'q_12099 => nat) (x, a::'q_12099) -->
-    measure m (x, b::'q_12099)) =
+    (x, a::'q_12099) : measure (m::'q_12099 => nat) -->
+    (x, b::'q_12099) : measure m) =
 (m a <= m b)"
   by (import hollight MEASURE_LE)
 
diff -r 5db68864a967 -r 74fb317aaeb5 src/HOL/Import/HOLLight/hollight.imp
--- a/src/HOL/Import/HOLLight/hollight.imp	Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Import/HOLLight/hollight.imp	Thu Sep 01 14:35:51 2011 +0200
@@ -590,6 +590,8 @@
   "UNIONS_INSERT" > "Complete_Lattice.Union_insert"
   "UNIONS_IMAGE" > "HOLLight.hollight.UNIONS_IMAGE"
   "UNIONS_GSPEC" > "HOLLight.hollight.UNIONS_GSPEC"
+  "UNIONS_2" > "Complete_Lattice.Un_eq_Union"
+  "UNIONS_1" > "Complete_Lattice.complete_lattice_class.Sup_singleton"
   "UNIONS_0" > "Complete_Lattice.Union_empty"
   "UNCURRY_def" > "HOLLight.hollight.UNCURRY_def"
   "TYDEF_recspace" > "HOLLight.hollight.TYDEF_recspace"
@@ -1595,6 +1597,8 @@
   "INTERS_INSERT" > "Complete_Lattice.Inter_insert"
   "INTERS_IMAGE" > "HOLLight.hollight.INTERS_IMAGE"
   "INTERS_GSPEC" > "HOLLight.hollight.INTERS_GSPEC"
+  "INTERS_2" > "Complete_Lattice.Int_eq_Inter"
+  "INTERS_1" > "Complete_Lattice.complete_lattice_class.Inf_singleton"
   "INTERS_0" > "Complete_Lattice.Inter_empty"
   "INSERT_UNIV" > "HOLLight.hollight.INSERT_UNIV"
   "INSERT_UNION_EQ" > "Set.Un_insert_left"
@@ -1684,7 +1688,7 @@
   "HAS_SIZE_0" > "HOLLight.hollight.HAS_SIZE_0"
   "GE_C" > "HOLLight.hollight.GE_C"
   "FUN_IN_IMAGE" > "Set.imageI"
-  "FUN_EQ_THM" > "Fun.fun_eq_iff"
+  "FUN_EQ_THM" > "HOL.fun_eq_iff"
   "FUNCTION_FACTORS_RIGHT" > "HOLLight.hollight.FUNCTION_FACTORS_RIGHT"
   "FUNCTION_FACTORS_LEFT" > "HOLLight.hollight.FUNCTION_FACTORS_LEFT"
   "FST" > "Product_Type.fst_conv"
@@ -2010,7 +2014,7 @@
   "DEF__equal__equal__greaterthan_" > "HOLLightCompat.DEF__equal__equal__greaterthan_"
   "DEF__equal__equal_" > "HOLLight.hollight.DEF__equal__equal_"
   "DEF__equal__c" > "HOLLight.hollight.DEF__equal__c"
-  "DEF__dot__dot_" > "HOLLightCompat.DEF__dot__dot_"
+  "DEF__dot__dot_" > "HOLLightCompat.dotdot_def"
   "DEF__backslash__slash_" > "HOL.or_def"
   "DEF__UNGUARDED_PATTERN" > "HOLLight.hollight.DEF__UNGUARDED_PATTERN"
   "DEF__SEQPATTERN" > "HOLLight.hollight.DEF__SEQPATTERN"
@@ -2080,7 +2084,7 @@
   "DEF_IMAGE" > "HOLLightCompat.DEF_IMAGE"
   "DEF_I" > "Fun.id_apply"
   "DEF_HAS_SIZE" > "HOLLight.hollight.DEF_HAS_SIZE"
-  "DEF_GSPEC" > "HOLLightCompat.DEF_GSPEC"
+  "DEF_GSPEC" > "Set.Collect_def"
   "DEF_GEQ" > "HOLLightCompat.DEF_GEQ"
   "DEF_GABS" > "HOLLightCompat.DEF_GABS"
   "DEF_FST" > "HOLLightCompat.DEF_FST"
diff -r 5db68864a967 -r 74fb317aaeb5 src/HOL/Import/HOLLightCompat.thy
--- a/src/HOL/Import/HOLLightCompat.thy	Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Import/HOLLightCompat.thy	Thu Sep 01 14:35:51 2011 +0200
@@ -22,19 +22,16 @@
   by simp
 
 lemma num_Axiom:
-  "\<forall>e f. \<exists>!fn. fn 0 = e \<and> (\<forall>n. fn (Suc n) = f (fn n) n)"
-  apply (intro allI)
-  apply (rule_tac a="nat_rec e (%n e. f e n)" in ex1I)
-  apply auto
-  apply (simp add: fun_eq_iff)
-  apply (intro allI)
-  apply (induct_tac xa)
+  "\<exists>!fn. fn 0 = e \<and> (\<forall>n. fn (Suc n) = f (fn n) n)"
+  apply (rule ex1I[of _ "nat_rec e (%n e. f e n)"])
+  apply (auto simp add: fun_eq_iff)
+  apply (induct_tac x)
   apply simp_all
   done
 
 lemma SUC_INJ:
   "\<forall>m n. Suc m = Suc n \<longleftrightarrow> m = n"
-  by auto
+  by simp
 
 lemma PAIR:
   "(fst x, snd x) = x"
@@ -47,8 +44,7 @@
 lemma DEF__star_:
   "op * = (SOME mult. (\<forall>n. mult 0 n = 0) \<and> (\<forall>m n. mult (Suc m) n = mult m n + n))"
   apply (rule some_equality[symmetric])
-  apply auto
-  apply (rule ext)+
+  apply (auto simp add: fun_eq_iff)
   apply (induct_tac x)
   apply auto
   done
@@ -93,30 +89,32 @@
 lemma DEF_WF:
   "wfP = (\<lambda>u. \<forall>P. (\<exists>x. P x) \<longrightarrow> (\<exists>x. P x \<and> (\<forall>y. u y x \<longrightarrow> \<not> P y)))"
   unfolding fun_eq_iff
-  apply (intro allI, rule, intro allI impI, elim exE)
-  apply (drule_tac wfE_min[to_pred, unfolded mem_def])
-  apply assumption
-  prefer 2
-  apply assumption
-  apply auto[1]
-  apply (intro wfI_min[to_pred, unfolded mem_def])
-  apply (drule_tac x="Q" in spec)
-  apply auto
-  apply (rule_tac x="xb" in bexI)
-  apply (auto simp add: mem_def)
-  done
+proof (intro allI iffI impI wfI_min[to_pred], elim exE wfE_min[to_pred])
+  fix P :: "'a \<Rightarrow> bool" and xa :: "'a"
+  assume "P xa"
+  then show "xa \<in> Collect P" by simp
+next
+  fix x P xa z
+  assume "P xa" "z \<in> {a. P a}" "\<And>y. x y z \<Longrightarrow> y \<notin> {a. P a}"
+  then show "\<exists>xa. P xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> P y)" by auto
+next
+  fix x :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and xa :: "'a" and Q
+  assume a: "xa \<in> Q"
+  assume b: "\<forall>P. Ex P \<longrightarrow> (\<exists>xa. P xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> P y))"
+  then have "Ex (\<lambda>x. x \<in> Q) \<longrightarrow> (\<exists>xa. (\<lambda>x. x \<in> Q) xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> (\<lambda>x. x \<in> Q) y))" by auto
+  then show "\<exists>z\<in>Q. \<forall>y. x y z \<longrightarrow> y \<notin> Q" using a by auto
+qed
 
-lemma DEF_UNIV: "UNIV = (%x. True)"
-  by (auto simp add: mem_def)
+lemma DEF_UNIV: "top = (%x. True)"
+  by (rule ext) (simp add: top1I)
 
 lemma DEF_UNIONS:
   "Sup = (\<lambda>u. {ua. \<exists>x. (\<exists>ua. ua \<in> u \<and> x \<in> ua) \<and> ua = x})"
-  by (simp add: fun_eq_iff Collect_def)
-     (metis UnionE complete_lattice_class.Sup_upper mem_def predicate1D)
+  by (auto simp add: Union_eq)
 
 lemma DEF_UNION:
   "op \<union> = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<or> x \<in> ua) \<and> ub = x})"
-  by (auto simp add: mem_def fun_eq_iff Collect_def)
+  by auto
 
 lemma DEF_SUBSET: "op \<subseteq> = (\<lambda>u ua. \<forall>x. x \<in> u \<longrightarrow> x \<in> ua)"
   by (metis set_rev_mp subsetI)
@@ -129,7 +127,7 @@
 definition [simp, hol4rew]: "SETSPEC x P y \<longleftrightarrow> P & x = y"
 
 lemma DEF_PSUBSET: "op \<subset> = (\<lambda>u ua. u \<subseteq> ua & u \<noteq> ua)"
-  by (auto simp add: mem_def fun_eq_iff)
+  by (metis psubset_eq)
 
 definition [hol4rew]: "Pred n = n - (Suc 0)"
 
@@ -174,8 +172,8 @@
 definition "MEASURE = (%u x y. (u x :: nat) < u y)"
 
 lemma [hol4rew]:
-  "MEASURE u = (%a b. measure u (a, b))"
-  unfolding MEASURE_def measure_def fun_eq_iff inv_image_def Collect_def
+  "MEASURE u = (%a b. (a, b) \<in> measure u)"
+  unfolding MEASURE_def measure_def
   by simp
 
 definition
@@ -187,12 +185,11 @@
 
 lemma DEF_INTERS:
   "Inter = (\<lambda>u. {ua. \<exists>x. (\<forall>ua. ua \<in> u \<longrightarrow> x \<in> ua) \<and> ua = x})"
-  by (auto simp add: fun_eq_iff mem_def Collect_def)
-     (metis InterD InterI mem_def)+
+  by auto
 
 lemma DEF_INTER:
   "op \<inter> = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<and> x \<in> ua) \<and> ub = x})"
-  by (auto simp add: mem_def fun_eq_iff Collect_def)
+  by auto
 
 lemma DEF_INSERT:
   "insert = (%u ua y. y \<in> ua | y = u)"
@@ -202,10 +199,6 @@
   "op ` = (\<lambda>u ua. {ub. \<exists>y. (\<exists>x. x \<in> ua \<and> y = u x) \<and> ub = y})"
   by (simp add: fun_eq_iff image_def Bex_def)
 
-lemma DEF_GSPEC:
-  "Collect = (\<lambda>u. u)"
-  by (simp add: Collect_def ext)
-
 lemma DEF_GEQ:
   "(op =) = (op =)"
   by simp
@@ -226,9 +219,7 @@
   apply (erule finite_induct)
   apply auto[2]
   apply (drule_tac x="finite" in spec)
-  apply auto
-  apply (metis Collect_def Collect_empty_eq finite.emptyI)
-  by (metis (no_types) finite.insertI predicate1I sup.commute sup_absorb1)
+  by (metis finite_insert infinite_imp_nonempty infinite_super predicate1I)
 
 lemma DEF_FACT:
   "fact = (SOME FACT. FACT 0 = 1 & (\<forall>n. FACT (Suc n) = Suc n * FACT n))"
@@ -260,10 +251,9 @@
   apply simp_all
   done
 
-lemma DEF_EMPTY: "{} = (%x. False)"
-  unfolding fun_eq_iff empty_def
-  by auto
-
+lemma DEF_EMPTY: "bot = (%x. False)"
+  by (rule ext) auto
+  
 lemma DEF_DIV:
   "op div = (SOME q. \<exists>r. \<forall>m n. if n = (0 :: nat) then q m n = 0 \<and> r m n = m
      else m = q m n * n + r m n \<and> r m n < n)"
@@ -286,8 +276,7 @@
 
 lemma DEF_DIFF:
   "op - = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<and> x \<notin> ua) \<and> ub = x})"
-  by (simp add: fun_eq_iff Collect_def)
-     (metis DiffE DiffI mem_def)
+  by (metis set_diff_eq)
 
 definition [hol4rew]: "DELETE s e = s - {e}"
 
@@ -345,11 +334,8 @@
 lemma DEF_CHOICE: "Eps = (%u. SOME x. x \<in> u)"
   by (simp add: mem_def)
 
-definition dotdot :: "nat => nat => nat => bool"
-  where "dotdot == %(u::nat) ua::nat. {ub::nat. EX x::nat. (u <= x & x <= ua) & ub = x}"
-
-lemma DEF__dot__dot_: "dotdot = (%u ua. {ub. EX x. (u <= x & x <= ua) & ub = x})"
-  by (simp add: dotdot_def)
+definition dotdot :: "nat => nat => nat set"
+  where "dotdot u ua = {ub. EX x. (u <= x & x <= ua) & ub = x}"
 
 lemma [hol4rew]: "dotdot a b = {a..b}"
   unfolding fun_eq_iff atLeastAtMost_def atLeast_def atMost_def dotdot_def
diff -r 5db68864a967 -r 74fb317aaeb5 src/HOL/Import/HOLLightReal.thy
--- a/src/HOL/Import/HOLLightReal.thy	Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Import/HOLLightReal.thy	Thu Sep 01 14:35:51 2011 +0200
@@ -301,10 +301,7 @@
   "(\<exists>(x :: real). P x) \<and> (\<exists>(M :: real). \<forall>x. P x \<longrightarrow> x \<le> M) \<longrightarrow>
    (\<exists>M. (\<forall>x. P x \<longrightarrow> x \<le> M) \<and>
           (\<forall>M'. (\<forall>x. P x \<longrightarrow> x \<le> M') \<longrightarrow> M \<le> M'))"
-  apply (intro allI impI, elim conjE)
-  apply (drule complete_real[unfolded Ball_def mem_def])
-  apply simp_all
-  done
+  using complete_real[unfolded Ball_def, of "Collect P"] by auto
 
 lemma REAL_COMPLETE_SOMEPOS:
   "(\<exists>(x :: real). P x \<and> 0 \<le> x) \<and> (\<exists>M. \<forall>x. P x \<longrightarrow> x \<le> M) \<longrightarrow>
diff -r 5db68864a967 -r 74fb317aaeb5 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Limits.thy	Thu Sep 01 14:35:51 2011 +0200
@@ -916,21 +916,6 @@
   thus ?thesis by (rule BfunI)
 qed
 
-lemma tendsto_inverse_lemma:
-  fixes a :: "'a::real_normed_div_algebra"
-  shows "\<lbrakk>(f ---> a) F; a \<noteq> 0; eventually (\<lambda>x. f x \<noteq> 0) F\<rbrakk>
-         \<Longrightarrow> ((\<lambda>x. inverse (f x)) ---> inverse a) F"
-  apply (subst tendsto_Zfun_iff)
-  apply (rule Zfun_ssubst)
-  apply (erule eventually_elim1)
-  apply (erule (1) inverse_diff_inverse)
-  apply (rule Zfun_minus)
-  apply (rule Zfun_mult_left)
-  apply (rule bounded_bilinear.Bfun_prod_Zfun [OF bounded_bilinear_mult])
-  apply (erule (1) Bfun_inverse)
-  apply (simp add: tendsto_Zfun_iff)
-  done
-
 lemma tendsto_inverse [tendsto_intros]:
   fixes a :: "'a::real_normed_div_algebra"
   assumes f: "(f ---> a) F"
@@ -942,8 +927,15 @@
     by (rule tendstoD)
   then have "eventually (\<lambda>x. f x \<noteq> 0) F"
     unfolding dist_norm by (auto elim!: eventually_elim1)
-  with f a show ?thesis
-    by (rule tendsto_inverse_lemma)
+  with a have "eventually (\<lambda>x. inverse (f x) - inverse a =
+    - (inverse (f x) * (f x - a) * inverse a)) F"
+    by (auto elim!: eventually_elim1 simp: inverse_diff_inverse)
+  moreover have "Zfun (\<lambda>x. - (inverse (f x) * (f x - a) * inverse a)) F"
+    by (intro Zfun_minus Zfun_mult_left
+      bounded_bilinear.Bfun_prod_Zfun [OF bounded_bilinear_mult]
+      Bfun_inverse [OF f a] f [unfolded tendsto_Zfun_iff])
+  ultimately show ?thesis
+    unfolding tendsto_Zfun_iff by (rule Zfun_ssubst)
 qed
 
 lemma tendsto_divide [tendsto_intros]:
diff -r 5db68864a967 -r 74fb317aaeb5 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/List.thy	Thu Sep 01 14:35:51 2011 +0200
@@ -2929,6 +2929,14 @@
     by (induct xs' ys' rule: list_induct2) (auto elim: in_set_zipE)
 qed
 
+(* The next two lemmas help Sledgehammer. *)
+
+lemma distinct_singleton: "distinct [x]" by simp
+
+lemma distinct_length_2_or_more:
+"distinct (a # b # xs) \<longleftrightarrow> (a \<noteq> b \<and> distinct (a # xs) \<and> distinct (b # xs))"
+by (metis distinct.simps(2) hd.simps hd_in_set list.simps(2) set_ConsD set_rev_mp set_subset_Cons)
+
 
 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
 
@@ -4906,8 +4914,11 @@
 lemma list_size_map[simp]: "list_size f (map g xs) = list_size (f o g) xs"
 by (induct xs) auto
 
+lemma list_size_append[simp]: "list_size f (xs @ ys) = list_size f xs + list_size f ys"
+by (induct xs, auto)
+
 lemma list_size_pointwise[termination_simp]: 
-  "(\<And>x. x \<in> set xs \<Longrightarrow> f x < g x) \<Longrightarrow> list_size f xs \<le> list_size g xs"
+  "(\<And>x. x \<in> set xs \<Longrightarrow> f x \<le> g x) \<Longrightarrow> list_size f xs \<le> list_size g xs"
 by (induct xs) force+
 
 
diff -r 5db68864a967 -r 74fb317aaeb5 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Sep 01 14:35:51 2011 +0200
@@ -378,9 +378,7 @@
                  #> (Option.map (Config.put ATP_Systems.e_weight_method)
                        e_weight_method |> the_default I)
                  #> (Option.map (Config.put ATP_Systems.force_sos)
-                       force_sos |> the_default I)
-                 #> Config.put Sledgehammer_Provers.measure_run_time true
-                 #> Config.put Sledgehammer_Provers.atp_sound_modulo_infiniteness false)
+                       force_sos |> the_default I))
     val params as {relevance_thresholds, max_relevant, slicing, ...} =
       Sledgehammer_Isar.default_params ctxt
           [("verbose", "true"),
@@ -416,12 +414,12 @@
       let
         val _ = if is_appropriate_prop concl_t then ()
                 else raise Fail "inappropriate"
-        val is_ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover_name
+        val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover_name
         val facts =
-          Sledgehammer_Filter.nearly_all_facts ctxt is_ho_atp
-                          relevance_override chained_ths hyp_ts concl_t
+          Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override
+            chained_ths hyp_ts concl_t
           |> filter (is_appropriate_prop o prop_of o snd)
-          |> Sledgehammer_Filter.relevant_facts ctxt is_ho_atp relevance_thresholds
+          |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
                  (the_default default_max_relevant max_relevant)
                  is_built_in_const relevance_fudge relevance_override
                  chained_ths hyp_ts concl_t
diff -r 5db68864a967 -r 74fb317aaeb5 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Thu Sep 01 14:35:51 2011 +0200
@@ -129,12 +129,12 @@
          val relevance_override = {add = [], del = [], only = false}
          val subgoal = 1
          val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal subgoal
-         val is_ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
+         val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
          val facts =
-          Sledgehammer_Filter.nearly_all_facts ctxt is_ho_atp relevance_override
+          Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override
                                                chained_ths hyp_ts concl_t
           |> filter (is_appropriate_prop o prop_of o snd)
-          |> Sledgehammer_Filter.relevant_facts ctxt is_ho_atp relevance_thresholds
+          |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
                  (the_default default_max_relevant max_relevant)
                  is_built_in_const relevance_fudge relevance_override
                  chained_ths hyp_ts concl_t
diff -r 5db68864a967 -r 74fb317aaeb5 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Sep 01 14:35:51 2011 +0200
@@ -524,7 +524,7 @@
   show ?thesis apply(simp add: affine_hull_finite affine_hull_finite_step)
     unfolding * apply auto
     apply(rule_tac x=v in exI) apply(rule_tac x=va in exI) apply auto
-    apply(rule_tac x=u in exI) by(auto intro!: exI)
+    apply(rule_tac x=u in exI) by force
 qed
 
 lemma mem_affine:
@@ -3028,7 +3028,7 @@
     hence "\<exists>x. norm x = 1 \<and> (\<forall>y\<in>c. 0 \<le> inner y x)" apply(rule_tac x="inverse(norm a) *\<^sub>R a" in exI)
        using hull_subset[of c convex] unfolding subset_eq and inner_scaleR
        apply- apply rule defer apply rule apply(rule mult_nonneg_nonneg)
-       by(auto simp add: inner_commute elim!: ballE)
+       by(auto simp add: inner_commute del: ballE elim!: ballE)
     thus "frontier (cball 0 1) \<inter> \<Inter>f \<noteq> {}" unfolding c(1) frontier_cball dist_norm by auto
   qed(insert closed_halfspace_ge, auto)
   then obtain x where "norm x = 1" "\<forall>y\<in>s. x\<in>?k y" unfolding frontier_cball dist_norm by auto
@@ -3062,7 +3062,7 @@
   apply(rule,rule,rule,rule,rule,rule,rule,rule,rule) apply(erule_tac exE)+
   apply(rule_tac x="\<lambda>n. u *\<^sub>R xb n + v *\<^sub>R xc n" in exI) apply(rule,rule)
   apply(rule assms[unfolded convex_def, rule_format]) prefer 6
-  by (auto intro!: tendsto_intros)
+  by (auto del: tendsto_const intro!: tendsto_intros)
 
 lemma convex_interior:
   fixes s :: "'a::real_normed_vector set"
@@ -4156,7 +4156,7 @@
         using component_le_norm[of "y - x" i]
         using y[unfolded min_less_iff_conj dist_norm, THEN conjunct2] by(auto simp add: norm_minus_commute)
       thus "y $$ i \<le> x $$ i + ?d" by auto qed
-    also have "\<dots> \<le> 1" unfolding setsum_addf setsum_constant card_enum real_eq_of_nat by(auto simp add: Suc_le_eq)
+    also have "\<dots> \<le> 1" unfolding setsum_addf setsum_constant real_eq_of_nat by(auto simp add: Suc_le_eq)
     finally show "(\<forall>i<DIM('a). 0 \<le> y $$ i) \<and> setsum (op $$ y) {..<DIM('a)} \<le> 1" 
     proof safe fix i assume i:"i<DIM('a)"
       have "norm (x - y) < x$$i" apply(rule less_le_trans) 
@@ -4176,7 +4176,7 @@
   show ?thesis apply(rule that[of ?a]) unfolding interior_std_simplex mem_Collect_eq proof safe
     fix i assume i:"i<DIM('a)" show "0 < ?a $$ i" unfolding **[OF i] by(auto simp add: Suc_le_eq)
   next have "setsum (op $$ ?a) ?D = setsum (\<lambda>i. inverse (2 * real DIM('a))) ?D" apply(rule setsum_cong2, rule **) by auto
-    also have "\<dots> < 1" unfolding setsum_constant card_enum real_eq_of_nat divide_inverse[THEN sym] by (auto simp add:field_simps)
+    also have "\<dots> < 1" unfolding setsum_constant real_eq_of_nat divide_inverse[THEN sym] by (auto simp add:field_simps)
     finally show "setsum (op $$ ?a) ?D < 1" by auto qed qed
 
 lemma rel_interior_substd_simplex: assumes "d\<subseteq>{..<DIM('a::euclidean_space)}"
@@ -4251,7 +4251,7 @@
         using y[unfolded min_less_iff_conj dist_norm, THEN conjunct2]
         by(auto simp add: norm_minus_commute)
       thus "y $$ i \<le> x $$ i + ?d" by auto qed
-    also have "\<dots> \<le> 1" unfolding setsum_addf setsum_constant card_enum real_eq_of_nat
+    also have "\<dots> \<le> 1" unfolding setsum_addf setsum_constant real_eq_of_nat
       using `0 < card d` by auto
     finally show "setsum (op $$ y) d \<le> 1" .
      
@@ -4294,7 +4294,7 @@
     finally show "0 < ?a $$ i" by auto
   next have "setsum (op $$ ?a) ?D = setsum (\<lambda>i. inverse (2 * real (card d))) ?D" 
       by(rule setsum_cong2, rule **) 
-    also have "\<dots> < 1" unfolding setsum_constant card_enum real_eq_of_nat real_divide_def[THEN sym]
+    also have "\<dots> < 1" unfolding setsum_constant real_eq_of_nat real_divide_def[THEN sym]
       by (auto simp add:field_simps)
     finally show "setsum (op $$ ?a) ?D < 1" by auto
   next fix i assume "i<DIM('a)" and "i~:d"
diff -r 5db68864a967 -r 74fb317aaeb5 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Thu Sep 01 14:35:51 2011 +0200
@@ -7,7 +7,7 @@
 
 theory Euclidean_Space
 imports
-  Complex_Main
+  L2_Norm
   "~~/src/HOL/Library/Inner_Product"
   "~~/src/HOL/Library/Product_Vector"
 begin
@@ -216,10 +216,20 @@
     simp add: inner_setsum_left inner_setsum_right
     dot_basis if_distrib setsum_cases mult_commute)
 
+lemma euclidean_dist_l2:
+  fixes x y :: "'a::euclidean_space"
+  shows "dist x y = setL2 (\<lambda>i. dist (x $$ i) (y $$ i)) {..<DIM('a)}"
+  unfolding dist_norm norm_eq_sqrt_inner setL2_def
+  by (simp add: euclidean_inner power2_eq_square)
+
 lemma component_le_norm: "\<bar>x$$i\<bar> \<le> norm (x::'a::euclidean_space)"
   unfolding euclidean_component_def
   by (rule order_trans [OF Cauchy_Schwarz_ineq2]) simp
 
+lemma dist_nth_le: "dist (x $$ i) (y $$ i) \<le> dist x (y::'a::euclidean_space)"
+  unfolding euclidean_dist_l2 [where 'a='a]
+  by (cases "i < DIM('a)", rule member_le_setL2, auto)
+
 subsection {* Subclass relationships *}
 
 instance euclidean_space \<subseteq> perfect_space
diff -r 5db68864a967 -r 74fb317aaeb5 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Thu Sep 01 14:35:51 2011 +0200
@@ -206,6 +206,9 @@
     by simp
 qed
 
+lemma isCont_vec_nth [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x $ i) a"
+  unfolding isCont_def by (rule tendsto_vec_nth)
+
 lemma eventually_Ball_finite: (* TODO: move *)
   assumes "finite A" and "\<forall>y\<in>A. eventually (\<lambda>x. P x y) net"
   shows "eventually (\<lambda>x. \<forall>y\<in>A. P x y) net"
@@ -296,44 +299,45 @@
     apply (simp add: setL2_mono dist_triangle2)
     done
 next
-  (* FIXME: long proof! *)
   fix S :: "('a ^ 'b) set"
   show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
-    unfolding open_vec_def open_dist
-    apply safe
-     apply (drule (1) bspec)
-     apply clarify
-     apply (subgoal_tac "\<exists>e>0. \<forall>i y. dist y (x$i) < e \<longrightarrow> y \<in> A i")
-      apply clarify
-      apply (rule_tac x=e in exI, clarify)
-      apply (drule spec, erule mp, clarify)
-      apply (drule spec, drule spec, erule mp)
-      apply (erule le_less_trans [OF dist_vec_nth_le])
-     apply (subgoal_tac "\<forall>i\<in>UNIV. \<exists>e>0. \<forall>y. dist y (x$i) < e \<longrightarrow> y \<in> A i")
-      apply (drule finite_choice [OF finite], clarify)
-      apply (rule_tac x="Min (range f)" in exI, simp)
-     apply clarify
-     apply (drule_tac x=i in spec, clarify)
-     apply (erule (1) bspec)
-    apply (drule (1) bspec, clarify)
-    apply (subgoal_tac "\<exists>r. (\<forall>i::'b. 0 < r i) \<and> e = setL2 r UNIV")
-     apply clarify
-     apply (rule_tac x="\<lambda>i. {y. dist y (x$i) < r i}" in exI)
-     apply (rule conjI)
-      apply clarify
-      apply (rule conjI)
-       apply (clarify, rename_tac y)
-       apply (rule_tac x="r i - dist y (x$i)" in exI, rule conjI, simp)
-       apply clarify
-       apply (simp only: less_diff_eq)
-       apply (erule le_less_trans [OF dist_triangle])
-      apply simp
-     apply clarify
-     apply (drule spec, erule mp)
-     apply (simp add: dist_vec_def setL2_strict_mono)
-    apply (rule_tac x="\<lambda>i. e / sqrt (of_nat CARD('b))" in exI)
-    apply (simp add: divide_pos_pos setL2_constant)
-    done
+  proof
+    assume "open S" show "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S"
+    proof
+      fix x assume "x \<in> S"
+      obtain A where A: "\<forall>i. open (A i)" "\<forall>i. x $ i \<in> A i"
+        and S: "\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S"
+        using `open S` and `x \<in> S` unfolding open_vec_def by metis
+      have "\<forall>i\<in>UNIV. \<exists>r>0. \<forall>y. dist y (x $ i) < r \<longrightarrow> y \<in> A i"
+        using A unfolding open_dist by simp
+      hence "\<exists>r. \<forall>i\<in>UNIV. 0 < r i \<and> (\<forall>y. dist y (x $ i) < r i \<longrightarrow> y \<in> A i)"
+        by (rule finite_choice [OF finite])
+      then obtain r where r1: "\<forall>i. 0 < r i"
+        and r2: "\<forall>i y. dist y (x $ i) < r i \<longrightarrow> y \<in> A i" by fast
+      have "0 < Min (range r) \<and> (\<forall>y. dist y x < Min (range r) \<longrightarrow> y \<in> S)"
+        by (simp add: r1 r2 S le_less_trans [OF dist_vec_nth_le])
+      thus "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" ..
+    qed
+  next
+    assume *: "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" show "open S"
+    proof (unfold open_vec_def, rule)
+      fix x assume "x \<in> S"
+      then obtain e where "0 < e" and S: "\<forall>y. dist y x < e \<longrightarrow> y \<in> S"
+        using * by fast
+      def r \<equiv> "\<lambda>i::'b. e / sqrt (of_nat CARD('b))"
+      from `0 < e` have r: "\<forall>i. 0 < r i"
+        unfolding r_def by (simp_all add: divide_pos_pos)
+      from `0 < e` have e: "e = setL2 r UNIV"
+        unfolding r_def by (simp add: setL2_constant)
+      def A \<equiv> "\<lambda>i. {y. dist (x $ i) y < r i}"
+      have "\<forall>i. open (A i) \<and> x $ i \<in> A i"
+        unfolding A_def by (simp add: open_ball r)
+      moreover have "\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S"
+        by (simp add: A_def S dist_vec_def e setL2_strict_mono dist_commute)
+      ultimately show "\<exists>A. (\<forall>i. open (A i) \<and> x $ i \<in> A i) \<and>
+        (\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S)" by metis
+    qed
+  qed
 qed
 
 end
@@ -434,9 +438,6 @@
 apply (rule_tac x="1" in exI, simp add: norm_nth_le)
 done
 
-lemmas isCont_vec_nth [simp] =
-  bounded_linear.isCont [OF bounded_linear_vec_nth]
-
 instance vec :: (banach, finite) banach ..
 
 
diff -r 5db68864a967 -r 74fb317aaeb5 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Sep 01 14:35:51 2011 +0200
@@ -2534,8 +2534,6 @@
   unfolding infnorm_set_image  ball_simps
   by (metis component_le_norm)
 
-lemma card_enum: "card {1 .. n} = n" by auto
-
 lemma norm_le_infnorm: "norm(x) <= sqrt(real DIM('a)) * infnorm(x::'a::euclidean_space)"
 proof-
   let ?d = "DIM('a)"
diff -r 5db68864a967 -r 74fb317aaeb5 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Sep 01 14:35:51 2011 +0200
@@ -7,19 +7,9 @@
 header {* Elementary topology in Euclidean space. *}
 
 theory Topology_Euclidean_Space
-imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs" Norm_Arith L2_Norm
+imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs" Norm_Arith
 begin
 
-(* to be moved elsewhere *)
-
-lemma euclidean_dist_l2:"dist x (y::'a::euclidean_space) = setL2 (\<lambda>i. dist(x$$i) (y$$i)) {..<DIM('a)}"
-  unfolding dist_norm norm_eq_sqrt_inner setL2_def apply(subst euclidean_inner)
-  by(auto simp add:power2_eq_square)
-
-lemma dist_nth_le: "dist (x $$ i) (y $$ i) \<le> dist x (y::'a::euclidean_space)"
-  apply(subst(2) euclidean_dist_l2) apply(cases "i<DIM('a)")
-  apply(rule member_le_setL2) by auto
-
 subsection {* General notion of a topology as a value *}
 
 definition "istopology L \<longleftrightarrow> L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union> K))"
@@ -2252,6 +2242,8 @@
     unfolding convergent_def by auto
 qed
 
+instance euclidean_space \<subseteq> banach ..
+
 lemma complete_univ: "complete (UNIV :: 'a::complete_space set)"
 proof(simp add: complete_def, rule, rule)
   fix f :: "nat \<Rightarrow> 'a" assume "Cauchy f"
@@ -2286,21 +2278,13 @@
 
 lemma convergent_eq_cauchy:
   fixes s :: "nat \<Rightarrow> 'a::complete_space"
-  shows "(\<exists>l. (s ---> l) sequentially) \<longleftrightarrow> Cauchy s" (is "?lhs = ?rhs")
-proof
-  assume ?lhs then obtain l where "(s ---> l) sequentially" by auto
-  thus ?rhs using convergent_imp_cauchy by auto
-next
-  assume ?rhs thus ?lhs using complete_univ[unfolded complete_def, THEN spec[where x=s]] by auto
-qed
+  shows "(\<exists>l. (s ---> l) sequentially) \<longleftrightarrow> Cauchy s"
+  unfolding Cauchy_convergent_iff convergent_def ..
 
 lemma convergent_imp_bounded:
   fixes s :: "nat \<Rightarrow> 'a::metric_space"
-  shows "(s ---> l) sequentially ==> bounded (s ` (UNIV::(nat set)))"
-  using convergent_imp_cauchy[of s]
-  using cauchy_imp_bounded[of s]
-  unfolding image_def
-  by auto
+  shows "(s ---> l) sequentially \<Longrightarrow> bounded (range s)"
+  by (intro cauchy_imp_bounded convergent_imp_cauchy)
 
 subsubsection{* Total boundedness *}
 
@@ -2953,7 +2937,7 @@
           "\<forall>n. (s n \<noteq> {})"
           "\<forall>m n. m \<le> n --> s n \<subseteq> s m"
           "\<forall>e>0. \<exists>n. \<forall>x \<in> (s n). \<forall> y \<in> (s n). dist x y < e"
-  shows "\<exists>a::'a::heine_borel. \<forall>n::nat. a \<in> s n"
+  shows "\<exists>a::'a::complete_space. \<forall>n::nat. a \<in> s n"
 proof-
   have "\<forall>n. \<exists> x. x\<in>s n" using assms(2) by auto
   hence "\<exists>t. \<forall>n. t n \<in> s n" using choice[of "\<lambda> n x. x \<in> s n"] by auto
@@ -2982,7 +2966,7 @@
 text {* Strengthen it to the intersection actually being a singleton. *}
 
 lemma decreasing_closed_nest_sing:
-  fixes s :: "nat \<Rightarrow> 'a::heine_borel set"
+  fixes s :: "nat \<Rightarrow> 'a::complete_space set"
   assumes "\<forall>n. closed(s n)"
           "\<forall>n. s n \<noteq> {}"
           "\<forall>m n. m \<le> n --> s n \<subseteq> s m"
@@ -5874,10 +5858,6 @@
   ultimately show "\<exists>!x\<in>s. g x = x" using `a\<in>s` by blast
 qed
 
-
-(** TODO move this someplace else within this theory **)
-instance euclidean_space \<subseteq> banach ..
-
 declare tendsto_const [intro] (* FIXME: move *)
 
 end
diff -r 5db68864a967 -r 74fb317aaeb5 src/HOL/TPTP/atp_export.ML
--- a/src/HOL/TPTP/atp_export.ML	Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/TPTP/atp_export.ML	Thu Sep 01 14:35:51 2011 +0200
@@ -27,8 +27,7 @@
 val fact_name_of = prefix fact_prefix o ascii_of
 
 fun facts_of thy =
-  Sledgehammer_Filter.all_facts (Proof_Context.init_global thy)
-                                false(*FIXME works only for first-order*)
+  Sledgehammer_Filter.all_facts (Proof_Context.init_global thy) false
                                 Symtab.empty true [] []
   |> filter (curry (op =) @{typ bool} o fastype_of
              o Object_Logic.atomize_term thy o prop_of o snd)
diff -r 5db68864a967 -r 74fb317aaeb5 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu Sep 01 14:35:51 2011 +0200
@@ -479,14 +479,19 @@
 fun declared_syms_in_problem problem =
   fold (fold add_declared_syms_in_problem_line o snd) problem []
 
+fun nary_type_constr_type n =
+  funpow n (curry AFun atype_of_types) atype_of_types
+
 fun undeclared_syms_in_problem declared problem =
   let
     fun do_sym name ty =
       if member (op =) declared name then I else AList.default (op =) (name, ty)
-    fun do_type_name name = do_sym name (K atype_of_types)
-    fun do_type (AType (name, tys)) = do_type_name name #> fold do_type tys
+    fun do_type (AType (name as (s, _), tys)) =
+        is_tptp_user_symbol s
+        ? do_sym name (fn _ => nary_type_constr_type (length tys))
+        #> fold do_type tys
       | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
-      | do_type (ATyAbs (names, ty)) = fold do_type_name names #> do_type ty
+      | do_type (ATyAbs (_, ty)) = do_type ty
     fun do_term pred_sym (ATerm (name as (s, _), tms)) =
         is_tptp_user_symbol s
         ? do_sym name (fn _ => default_type pred_sym (length tms))
diff -r 5db68864a967 -r 74fb317aaeb5 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Sep 01 14:35:51 2011 +0200
@@ -21,7 +21,7 @@
 
   datatype order = First_Order | Higher_Order
   datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
-  datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound
+  datatype soundness = Sound_Modulo_Infiniteness | Sound
   datatype type_level =
     All_Types |
     Noninf_Nonmono_Types of soundness |
@@ -139,6 +139,11 @@
 val elimN = "elim"
 val simpN = "simp"
 
+(* TFF1 is still in development, and it is still unclear whether symbols will be
+   allowed to have types like "$tType > $o" (i.e., "![A : $tType] : $o"), with
+   "dummy" type variables. *)
+val exploit_tff1_dummy_type_vars = false
+
 val bound_var_prefix = "B_"
 val all_bound_var_prefix = "BA_"
 val exist_bound_var_prefix = "BE_"
@@ -360,27 +365,19 @@
 
 (** Definitions and functions for FOL clauses and formulas for TPTP **)
 
-(* The first component is the type class; the second is a "TVar" or "TFree". *)
-datatype type_literal =
-  TyLitVar of name * name |
-  TyLitFree of name * name
-
-
 (** Isabelle arities **)
 
-datatype arity_literal =
-  TConsLit of name * name * name list |
-  TVarLit of name * name
+type arity_atom = name * name * name list
 
 val type_class = the_single @{sort type}
 
-fun add_packed_sort tvar =
-  fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar))
-
 type arity_clause =
   {name : string,
-   prem_lits : arity_literal list,
-   concl_lits : arity_literal}
+   prem_atoms : arity_atom list,
+   concl_atom : arity_atom}
+
+fun add_prem_atom tvar =
+  fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar, []))
 
 (* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
 fun make_axiom_arity_clause (tcons, name, (cls, args)) =
@@ -389,9 +386,9 @@
     val tvars_srts = ListPair.zip (tvars, args)
   in
     {name = name,
-     prem_lits = [] |> fold (uncurry add_packed_sort) tvars_srts |> map TVarLit,
-     concl_lits = TConsLit (`make_type_class cls, `make_fixed_type_const tcons,
-                            tvars ~~ tvars)}
+     prem_atoms = [] |> fold (uncurry add_prem_atom) tvars_srts,
+     concl_atom = (`make_type_class cls, `make_fixed_type_const tcons,
+                   tvars ~~ tvars)}
   end
 
 fun arity_clause _ _ (_, []) = []
@@ -539,7 +536,7 @@
 
 datatype order = First_Order | Higher_Order
 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
-datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound
+datatype soundness = Sound_Modulo_Infiniteness | Sound
 datatype type_level =
   All_Types |
   Noninf_Nonmono_Types of soundness |
@@ -718,24 +715,40 @@
               Explicit_Type_Args)
     end
 
-(* Make literals for sorted type variables. *)
+(* Make atoms for sorted type variables. *)
 fun generic_add_sorts_on_type (_, []) = I
   | generic_add_sorts_on_type ((x, i), s :: ss) =
     generic_add_sorts_on_type ((x, i), ss)
     #> (if s = the_single @{sort HOL.type} then
           I
         else if i = ~1 then
-          insert (op =) (TyLitFree (`make_type_class s, `make_fixed_type_var x))
+          insert (op =) (`make_type_class s, `make_fixed_type_var x)
         else
-          insert (op =) (TyLitVar (`make_type_class s,
-                                   (make_schematic_type_var (x, i), x))))
+          insert (op =) (`make_type_class s,
+                         (make_schematic_type_var (x, i), x)))
 fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S)
   | add_sorts_on_tfree _ = I
 fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
   | add_sorts_on_tvar _ = I
 
-fun type_literals_for_types type_enc add_sorts_on_typ Ts =
+val tvar_a_str = "'a"
+val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS)
+val tvar_a_name = (make_schematic_type_var (tvar_a_str, 0), tvar_a_str)
+val itself_name = `make_fixed_type_const @{type_name itself}
+val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
+val tvar_a_atype = AType (tvar_a_name, [])
+val a_itself_atype = AType (itself_name, [tvar_a_atype])
+
+fun type_class_formula type_enc class arg =
+  AAtom (ATerm (class, arg ::
+      (case type_enc of
+         Simple_Types (_, Polymorphic, _) =>
+         if exploit_tff1_dummy_type_vars then [] else [ATerm (TYPE_name, [arg])]
+       | _ => [])))
+fun formulas_for_types type_enc add_sorts_on_typ Ts =
   [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
+     |> map (fn (class, name) =>
+                type_class_formula type_enc class (ATerm (name, [])))
 
 fun mk_aconns c phis =
   let val (phis', phi') = split_last phis in
@@ -1120,11 +1133,10 @@
 (* These types witness that the type classes they belong to allow infinite
    models and hence that any types with these type classes is monotonic. *)
 val known_infinite_types =
-  [@{typ nat}, Type ("Int.int", []), @{typ "nat => bool"}]
+  [@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}]
 
 fun is_type_kind_of_surely_infinite ctxt soundness cached_Ts T =
-  soundness <> Sound andalso
-  is_type_surely_infinite ctxt (soundness <> Unsound) cached_Ts T
+  soundness <> Sound andalso is_type_surely_infinite ctxt true cached_Ts T
 
 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
    dangerous because their "exhaust" properties can easily lead to unsound ATP
@@ -1276,8 +1288,6 @@
   K (add_iterm_syms_to_table ctxt explicit_apply)
   |> formula_fold NONE |> fact_lift
 
-val tvar_a = TVar (("'a", 0), HOLogic.typeS)
-
 val default_sym_tab_entries : (string * sym_info) list =
   (prefixed_predicator_name,
    {pred_sym = true, min_ary = 1, max_ary = 1, types = []})
@@ -1450,16 +1460,8 @@
    (("If", true), @{thms if_True if_False True_or_False})]
   |> map (apsnd (map zero_var_indexes))
 
-fun fo_literal_from_type_literal (TyLitVar (class, name)) =
-    (true, ATerm (class, [ATerm (name, [])]))
-  | fo_literal_from_type_literal (TyLitFree (class, name)) =
-    (true, ATerm (class, [ATerm (name, [])]))
-
-fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
-
-fun bound_tvars type_enc Ts =
-  mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
-                (type_literals_for_types type_enc add_sorts_on_tvar Ts))
+fun bound_tvars type_enc =
+  mk_ahorn o formulas_for_types type_enc add_sorts_on_tvar
 
 fun eq_formula type_enc atomic_Ts pred_sym tm1 tm2 =
   (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
@@ -1738,25 +1740,23 @@
 
 fun formula_line_for_class_rel_clause type_enc
         ({name, subclass, superclass, ...} : class_rel_clause) =
-  let val ty_arg = ATerm ((make_schematic_type_var ("'a", 0), "'a"), []) in
+  let val ty_arg = ATerm (tvar_a_name, []) in
     Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
-             AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
-                               AAtom (ATerm (superclass, [ty_arg]))])
+             AConn (AImplies,
+                    [type_class_formula type_enc subclass ty_arg,
+                     type_class_formula type_enc superclass ty_arg])
              |> close_formula_universally type_enc, isabelle_info introN, NONE)
   end
 
-fun fo_literal_from_arity_literal (TConsLit (c, t, args)) =
-    (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
-  | fo_literal_from_arity_literal (TVarLit (c, sort)) =
-    (false, ATerm (c, [ATerm (sort, [])]))
+fun formula_from_arity_atom type_enc (class, t, args) =
+  ATerm (t, map (fn arg => ATerm (arg, [])) args)
+  |> type_class_formula type_enc class
 
 fun formula_line_for_arity_clause type_enc
-        ({name, prem_lits, concl_lits, ...} : arity_clause) =
+        ({name, prem_atoms, concl_atom, ...} : arity_clause) =
   Formula (arity_clause_prefix ^ name, Axiom,
-           mk_ahorn (map (formula_from_fo_literal o apfst not
-                          o fo_literal_from_arity_literal) prem_lits)
-                    (formula_from_fo_literal
-                         (fo_literal_from_arity_literal concl_lits))
+           mk_ahorn (map (formula_from_arity_atom type_enc) prem_atoms)
+                    (formula_from_arity_atom type_enc concl_atom)
            |> close_formula_universally type_enc, isabelle_info introN, NONE)
 
 fun formula_line_for_conjecture ctxt format mono type_enc
@@ -1768,24 +1768,24 @@
            |> bound_tvars type_enc atomic_types
            |> close_formula_universally type_enc, NONE, NONE)
 
-fun free_type_literals type_enc ({atomic_types, ...} : translated_formula) =
-  atomic_types |> type_literals_for_types type_enc add_sorts_on_tfree
-               |> map fo_literal_from_type_literal
-
-fun formula_line_for_free_type j lit =
-  Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,
-           formula_from_fo_literal lit, NONE, NONE)
-fun formula_lines_for_free_types type_enc facts =
+fun formula_line_for_free_type j phi =
+  Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, NONE)
+fun formula_lines_for_free_types type_enc (facts : translated_formula list) =
   let
-    val litss = map (free_type_literals type_enc) facts
-    val lits = fold (union (op =)) litss []
-  in map2 formula_line_for_free_type (0 upto length lits - 1) lits end
+    val phis =
+      fold (union (op =)) (map #atomic_types facts) []
+      |> formulas_for_types type_enc add_sorts_on_tfree
+  in map2 formula_line_for_free_type (0 upto length phis - 1) phis end
 
 (** Symbol declarations **)
 
 fun decl_line_for_class s =
   let val name as (s, _) = `make_type_class s in
-    Decl (sym_decl_prefix ^ s, name, AFun (atype_of_types, bool_atype))
+    Decl (sym_decl_prefix ^ s, name,
+          if exploit_tff1_dummy_type_vars then
+            AFun (atype_of_types, bool_atype)
+          else
+            ATyAbs ([tvar_a_name], AFun (a_itself_atype, bool_atype)))
   end
 
 fun decl_lines_for_classes type_enc classes =
@@ -1833,7 +1833,7 @@
     fun add_undefined_const T =
       let
         val (s, s') =
-          `(make_fixed_const (SOME format)) @{const_name undefined}
+          `(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]
               | _ => I)
@@ -1841,22 +1841,32 @@
         Symtab.map_default (s, [])
                            (insert_type ctxt #3 (s', [T], T, false, 0, false))
       end
+    fun add_TYPE_const () =
+      let val (s, s') = TYPE_name in
+        Symtab.map_default (s, [])
+            (insert_type ctxt #3
+                         (s', [tvar_a], @{typ "'a itself"}, false, 0, false))
+      end
   in
     Symtab.empty
     |> is_type_enc_fairly_sound type_enc
        ? (fold (add_fact_syms true) conjs
           #> fold (add_fact_syms false) facts
           #> (case type_enc of
-                Simple_Types _ => I
+                Simple_Types (_, poly, _) =>
+                if poly = Polymorphic then add_TYPE_const () else I
               | _ => fold add_undefined_const (var_types ())))
   end
 
 (* We add "bool" in case the helper "True_or_False" is included later. *)
-val default_mono =
+fun default_mono level =
   {maybe_finite_Ts = [@{typ bool}],
    surely_finite_Ts = [@{typ bool}],
    maybe_infinite_Ts = known_infinite_types,
-   surely_infinite_Ts = known_infinite_types,
+   surely_infinite_Ts =
+     case level of
+       Noninf_Nonmono_Types Sound => []
+     | _ => known_infinite_types,
    maybe_nonmono_Ts = [@{typ bool}]}
 
 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
@@ -1911,7 +1921,7 @@
                (add_iterm_mononotonicity_info ctxt level) iformula
 fun mononotonicity_info_for_facts ctxt type_enc facts =
   let val level = level_of_type_enc type_enc in
-    default_mono
+    default_mono level
     |> is_type_level_monotonicity_based level
        ? fold (add_fact_mononotonicity_info ctxt level) facts
   end
diff -r 5db68864a967 -r 74fb317aaeb5 src/HOL/Tools/Metis/metis_tactics.ML
--- a/src/HOL/Tools/Metis/metis_tactics.ML	Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Thu Sep 01 14:35:51 2011 +0200
@@ -121,7 +121,7 @@
       val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
       val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths
       val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
-      val type_enc = type_enc_from_string Unsound type_enc
+      val type_enc = type_enc_from_string Sound type_enc
       val (sym_tab, axioms, old_skolems) =
         prepare_metis_problem ctxt type_enc cls ths
       fun get_isa_thm mth Isa_Reflexive_or_Trivial =
diff -r 5db68864a967 -r 74fb317aaeb5 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Sep 01 14:35:51 2011 +0200
@@ -52,7 +52,7 @@
     Proof.context -> bool -> relevance_override -> thm list -> term list -> term
     -> (((unit -> string) * locality) * thm) list
   val relevant_facts :
-    Proof.context -> bool -> real * real -> int
+    Proof.context -> real * real -> int
     -> (string * typ -> term list -> bool * term list) -> relevance_fudge
     -> relevance_override -> thm list -> term list -> term
     -> (((unit -> string) * locality) * thm) list
@@ -586,7 +586,7 @@
    facts are included. *)
 val special_fact_index = 75
 
-fun relevance_filter ctxt ho_atp threshold0 decay max_relevant is_built_in_const
+fun relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
         (fudge as {threshold_divisor, ridiculous_threshold, ...})
         ({add, del, ...} : relevance_override) facts chained_ts hyp_ts concl_t =
   let
@@ -938,9 +938,9 @@
     |> uniquify
   end
 
-fun relevant_facts ctxt ho_atp (threshold0, threshold1) max_relevant
-                   is_built_in_const fudge (override as {only, ...}) chained_ths
-                   hyp_ts concl_t facts =
+fun relevant_facts ctxt (threshold0, threshold1) max_relevant is_built_in_const
+                   fudge (override as {only, ...}) chained_ths hyp_ts concl_t
+                   facts =
   let
     val thy = Proof_Context.theory_of ctxt
     val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
@@ -954,9 +954,9 @@
              max_relevant = 0 then
        []
      else
-       relevance_filter ctxt ho_atp threshold0 decay max_relevant
-           is_built_in_const fudge override facts (chained_ths |> map prop_of)
-           hyp_ts (concl_t |> theory_constify fudge (Context.theory_name thy)))
+       relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
+           fudge override facts (chained_ths |> map prop_of) hyp_ts
+           (concl_t |> theory_constify fudge (Context.theory_name thy)))
     |> map (apfst (apfst (fn f => f ())))
   end
 
diff -r 5db68864a967 -r 74fb317aaeb5 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Sep 01 14:35:51 2011 +0200
@@ -62,10 +62,8 @@
 
   val dest_dir : string Config.T
   val problem_prefix : string Config.T
-  val measure_run_time : bool Config.T
   val atp_lambda_translation : string Config.T
   val atp_full_names : bool Config.T
-  val atp_sound_modulo_infiniteness : bool Config.T
   val smt_triggers : bool Config.T
   val smt_weights : bool Config.T
   val smt_weight_min_facts : int Config.T
@@ -340,8 +338,6 @@
   Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")
 val problem_prefix =
   Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob")
-val measure_run_time =
-  Attrib.setup_config_bool @{binding sledgehammer_measure_run_time} (K false)
 
 val atp_lambda_translation =
   Attrib.setup_config_string @{binding sledgehammer_atp_lambda_translation}
@@ -351,9 +347,6 @@
    provers (e.g., E). For these reason, short names are enabled by default. *)
 val atp_full_names =
   Attrib.setup_config_bool @{binding sledgehammer_atp_full_names} (K false)
-val atp_sound_modulo_infiniteness =
-  Attrib.setup_config_bool @{binding sledgehammer_atp_sound_modulo_infiniteness}
-                           (K true)
 
 val smt_triggers =
   Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
@@ -510,9 +503,6 @@
   #> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf
       is_exhaustive_finite)
 
-fun int_opt_add (SOME m) (SOME n) = SOME (m + n)
-  | int_opt_add _ _ = NONE
-
 (* Important messages are important but not so important that users want to see
    them each time. *)
 val atp_important_message_keep_quotient = 10
@@ -573,7 +563,6 @@
         Path.append (Path.explode dest_dir) problem_file_name
       else
         error ("No such directory: " ^ quote dest_dir ^ ".")
-    val measure_run_time = verbose orelse Config.get ctxt measure_run_time
     val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
     fun split_time s =
       let
@@ -585,7 +574,7 @@
         val num3 = as_num (digit ::: digit ::: (digit >> single))
         val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b)
         val as_time = Scan.read Symbol.stopper time o raw_explode
-      in (output, as_time t) end
+      in (output, as_time t |> the_default 0 (* can't happen *)) end
     fun run_on prob_file =
       case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of
         (home_var, _) :: _ =>
@@ -627,13 +616,7 @@
                   length facts |> is_none max_relevant
                                   ? Integer.min best_max_relevant
                 val soundness =
-                  if sound then
-                    if Config.get ctxt atp_sound_modulo_infiniteness then
-                      Sound_Modulo_Infiniteness
-                    else
-                      Sound
-                  else
-                    Unsound
+                  if sound then Sound else Sound_Modulo_Infiniteness
                 val type_enc =
                   type_enc |> choose_type_enc soundness best_type_enc format
                 val fairly_sound = is_type_enc_fairly_sound type_enc
@@ -676,11 +659,7 @@
                   File.shell_path command ^ " " ^
                   arguments ctxt full_proof extra slice_timeout weights ^ " " ^
                   File.shell_path prob_file
-                val command =
-                  (if measure_run_time then
-                     "TIMEFORMAT='%3R'; { time " ^ core ^ " ; }"
-                   else
-                     "exec " ^ core) ^ " 2>&1"
+                val command = "TIMEFORMAT='%3R'; { time " ^ core ^ " ; } 2>&1"
                 val _ =
                   atp_problem
                   |> tptp_lines_for_atp_problem format
@@ -691,13 +670,13 @@
                     upto conjecture_offset + length hyp_ts + 1
                   |> map single
                 val ((output, msecs), (atp_proof, outcome)) =
-                  TimeLimit.timeLimit generous_slice_timeout Isabelle_System.bash_output command
+                  TimeLimit.timeLimit generous_slice_timeout
+                                      Isabelle_System.bash_output command
                   |>> (if overlord then
                          prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
                        else
                          I)
-                  |> fst
-                  |> (if measure_run_time then split_time else rpair NONE)
+                  |> fst |> split_time
                   |> (fn accum as (output, _) =>
                          (accum,
                           extract_tstplike_proof_and_outcome verbose complete
@@ -706,7 +685,7 @@
                           handle UNRECOGNIZED_ATP_PROOF () =>
                                  ([], SOME ProofIncomplete)))
                   handle TimeLimit.TimeOut =>
-                         (("", SOME (Time.toMilliseconds slice_timeout)),
+                         (("", Time.toMilliseconds slice_timeout),
                           ([], SOME TimedOut))
                 val outcome =
                   case outcome of
@@ -733,15 +712,15 @@
                   if Time.<= (time_left, Time.zeroTime) then
                     result
                   else
-                    (run_slice slice time_left
-                     |> (fn (stuff, (output, msecs, atp_proof, outcome)) =>
-                            (stuff, (output, int_opt_add msecs0 msecs,
-                                     atp_proof, outcome))))
+                    run_slice slice time_left
+                    |> (fn (stuff, (output, msecs, atp_proof, outcome)) =>
+                           (stuff, (output, msecs0 + msecs, atp_proof,
+                                    outcome)))
                 end
               | maybe_run_slice _ result = result
           in
             ((Symtab.empty, [], 0, Vector.fromList [], [], Symtab.empty),
-             ("", SOME 0, [], SOME InternalError))
+             ("", 0, [], SOME InternalError))
             |> fold maybe_run_slice actual_slices
           end
         else
@@ -802,7 +781,7 @@
               in proof_text ctxt isar_proof isar_params one_line_params end,
            (if verbose then
               "\nATP real CPU time: " ^
-              string_from_time (Time.fromMilliseconds (the msecs)) ^ "."
+              string_from_time (Time.fromMilliseconds msecs) ^ "."
             else
               "") ^
            (if important_message <> "" then
@@ -814,7 +793,7 @@
       | SOME failure =>
         ([], K (Failed_to_Play Metis), fn _ => string_for_failure failure, "")
   in
-    {outcome = outcome, used_facts = used_facts, run_time_in_msecs = msecs,
+    {outcome = outcome, used_facts = used_facts, run_time_in_msecs = SOME msecs,
      preplay = preplay, message = message, message_tail = message_tail}
   end
 
diff -r 5db68864a967 -r 74fb317aaeb5 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Sep 01 14:35:51 2011 +0200
@@ -269,9 +269,10 @@
       val {facts = chained_ths, goal, ...} = Proof.goal state
       val chained_ths = chained_ths |> normalize_chained_theorems
       val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i
-      val is_ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
-      val facts = nearly_all_facts ctxt is_ho_atp relevance_override
-                                   chained_ths hyp_ts concl_t
+      val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
+      val facts =
+        nearly_all_facts ctxt ho_atp relevance_override chained_ths hyp_ts
+                         concl_t
       val _ = () |> not blocking ? kill_provers
       val _ = case find_first (not o is_prover_supported ctxt) provers of
                 SOME name => error ("No such prover: " ^ name ^ ".")
@@ -323,9 +324,9 @@
           |> (case is_appropriate_prop of
                 SOME is_app => filter (is_app o prop_of o snd)
               | NONE => I)
-          |> relevant_facts ctxt is_ho_atp relevance_thresholds
-                            max_max_relevant is_built_in_const relevance_fudge
-                            relevance_override chained_ths hyp_ts concl_t
+          |> relevant_facts ctxt relevance_thresholds max_max_relevant
+                            is_built_in_const relevance_fudge relevance_override
+                            chained_ths hyp_ts concl_t
           |> tap (fn facts =>
                      if debug then
                        label ^ plural_s (length provers) ^ ": " ^
diff -r 5db68864a967 -r 74fb317aaeb5 src/HOL/ex/sledgehammer_tactics.ML
--- a/src/HOL/ex/sledgehammer_tactics.ML	Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/ex/sledgehammer_tactics.ML	Thu Sep 01 14:35:51 2011 +0200
@@ -37,13 +37,11 @@
     val relevance_fudge =
       Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
     val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
-    val is_ho_atp =
-      exists (Sledgehammer_Provers.is_ho_atp ctxt)
-        provers(*FIXME: duplicated from sledgehammer_run.ML*)
+    val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
     val facts =
-      Sledgehammer_Filter.nearly_all_facts ctxt is_ho_atp relevance_override
+      Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override
                                            chained_ths hyp_ts concl_t
-      |> Sledgehammer_Filter.relevant_facts ctxt is_ho_atp relevance_thresholds
+      |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
              (the_default default_max_relevant max_relevant) is_built_in_const
              relevance_fudge relevance_override chained_ths hyp_ts concl_t
     val problem =