# HG changeset patch
# User wenzelm
# Date 1355485207 -3600
# Node ID bd145273e7c67cab612c6d04c15e41392d87602f
# Parent  0799339fea0f3cdf961a3c6f1bf3b48a68fec48b# Parent  4a389d115b4fa1eaf3c6ed39a5d38f531666d474
merged

diff -r 4a389d115b4f -r bd145273e7c6 NEWS
--- a/NEWS	Fri Dec 14 12:18:51 2012 +0100
+++ b/NEWS	Fri Dec 14 12:40:07 2012 +0100
@@ -172,8 +172,8 @@
     syntax "xs >>= ys"; use "suffixeq ys xs" instead.  Renamed lemmas
     accordingly.  INCOMPATIBILITY.
 
-  - New constant "emb" for homeomorphic embedding on lists. New
-    abbreviation "sub" for special case "emb (op =)".
+  - New constant "list_hembeq" for homeomorphic embedding on lists. New
+    abbreviation "sublisteq" for special case "list_hembeq (op =)".
 
   - Library/Sublist does no longer provide "order" and "bot" type class
     instances for the prefix order (merely corresponding locale
@@ -181,24 +181,24 @@
     Library/Prefix_Order. INCOMPATIBILITY.
 
   - The sublist relation from Library/Sublist_Order is now based on
-    "Sublist.sub". Replaced lemmas:
-
-      le_list_append_le_same_iff ~> Sublist.sub_append_le_same_iff
-      le_list_append_mono ~> Sublist.emb_append_mono
-      le_list_below_empty ~> Sublist.emb_Nil, Sublist.emb_Nil2
-      le_list_Cons_EX ~> Sublist.emb_ConsD
-      le_list_drop_Cons2 ~> Sublist.sub_Cons2'
-      le_list_drop_Cons_neq ~> Sublist.sub_Cons2_neq
-      le_list_drop_Cons ~> Sublist.sub_Cons'
-      le_list_drop_many ~> Sublist.sub_drop_many
-      le_list_filter_left ~> Sublist.sub_filter_left
-      le_list_rev_drop_many ~> Sublist.sub_rev_drop_many
-      le_list_rev_take_iff ~> Sublist.sub_append
-      le_list_same_length ~> Sublist.sub_same_length
-      le_list_take_many_iff ~> Sublist.sub_append'
+    "Sublist.sublisteq". Replaced lemmas:
+
+      le_list_append_le_same_iff ~> Sublist.sublisteq_append_le_same_iff
+      le_list_append_mono ~> Sublist.list_hembeq_append_mono
+      le_list_below_empty ~> Sublist.list_hembeq_Nil, Sublist.list_hembeq_Nil2
+      le_list_Cons_EX ~> Sublist.list_hembeq_ConsD
+      le_list_drop_Cons2 ~> Sublist.sublisteq_Cons2'
+      le_list_drop_Cons_neq ~> Sublist.sublisteq_Cons2_neq
+      le_list_drop_Cons ~> Sublist.sublisteq_Cons'
+      le_list_drop_many ~> Sublist.sublisteq_drop_many
+      le_list_filter_left ~> Sublist.sublisteq_filter_left
+      le_list_rev_drop_many ~> Sublist.sublisteq_rev_drop_many
+      le_list_rev_take_iff ~> Sublist.sublisteq_append
+      le_list_same_length ~> Sublist.sublisteq_same_length
+      le_list_take_many_iff ~> Sublist.sublisteq_append'
       less_eq_list.drop ~> less_eq_list_drop
       less_eq_list.induct ~> less_eq_list_induct
-      not_le_list_length ~> Sublist.not_sub_length
+      not_le_list_length ~> Sublist.not_sublisteq_length
 
     INCOMPATIBILITY.
 
diff -r 4a389d115b4f -r bd145273e7c6 src/HOL/BNF/Examples/Koenig.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF/Examples/Koenig.thy	Fri Dec 14 12:40:07 2012 +0100
@@ -0,0 +1,147 @@
+(*  Title:      HOL/BNF/Examples/Stream.thy
+    Author:     Dmitriy Traytel, TU Muenchen
+    Author:     Andrei Popescu, TU Muenchen
+    Copyright   2012
+
+Koenig's lemma.
+*)
+
+header {* Koenig's lemma *}
+
+theory Koenig
+imports TreeFI Stream
+begin
+
+(* selectors for streams *)
+lemma shd_def': "shd as = fst (stream_dtor as)"
+unfolding shd_def stream_case_def fst_def by (rule refl)
+
+lemma stl_def': "stl as = snd (stream_dtor as)"
+unfolding stl_def stream_case_def snd_def by (rule refl)
+
+lemma unfold_pair_fun_shd[simp]: "shd (stream_dtor_unfold (f \<odot> g) t) = f t"
+unfolding shd_def' pair_fun_def stream.dtor_unfold by simp
+
+lemma unfold_pair_fun_stl[simp]: "stl (stream_dtor_unfold (f \<odot> g) t) =
+ stream_dtor_unfold (f \<odot> g) (g t)"
+unfolding stl_def' pair_fun_def stream.dtor_unfold by simp
+
+(* infinite trees: *)
+coinductive infiniteTr where
+"\<lbrakk>tr' \<in> listF_set (sub tr); infiniteTr tr'\<rbrakk> \<Longrightarrow> infiniteTr tr"
+
+lemma infiniteTr_strong_coind[consumes 1, case_names sub]:
+assumes *: "phi tr" and
+**: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> listF_set (sub tr). phi tr' \<or> infiniteTr tr'"
+shows "infiniteTr tr"
+using assms by (elim infiniteTr.coinduct) blast
+
+lemma infiniteTr_coind[consumes 1, case_names sub, induct pred: infiniteTr]:
+assumes *: "phi tr" and
+**: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> listF_set (sub tr). phi tr'"
+shows "infiniteTr tr"
+using assms by (elim infiniteTr.coinduct) blast
+
+lemma infiniteTr_sub[simp]:
+"infiniteTr tr \<Longrightarrow> (\<exists> tr' \<in> listF_set (sub tr). infiniteTr tr')"
+by (erule infiniteTr.cases) blast
+
+definition "konigPath \<equiv> stream_dtor_unfold
+  (lab \<odot> (\<lambda>tr. SOME tr'. tr' \<in> listF_set (sub tr) \<and> infiniteTr tr'))"
+
+lemma konigPath_simps[simp]:
+"shd (konigPath t) = lab t"
+"stl (konigPath t) = konigPath (SOME tr. tr \<in> listF_set (sub t) \<and> infiniteTr tr)"
+unfolding konigPath_def by simp+
+
+(* proper paths in trees: *)
+coinductive properPath where
+"\<lbrakk>shd as = lab tr; tr' \<in> listF_set (sub tr); properPath (stl as) tr'\<rbrakk> \<Longrightarrow>
+ properPath as tr"
+
+lemma properPath_strong_coind[consumes 1, case_names shd_lab sub]:
+assumes *: "phi as tr" and
+**: "\<And> as tr. phi as tr \<Longrightarrow> shd as = lab tr" and
+***: "\<And> as tr.
+         phi as tr \<Longrightarrow>
+         \<exists> tr' \<in> listF_set (sub tr). phi (stl as) tr' \<or> properPath (stl as) tr'"
+shows "properPath as tr"
+using assms by (elim properPath.coinduct) blast
+
+lemma properPath_coind[consumes 1, case_names shd_lab sub, induct pred: properPath]:
+assumes *: "phi as tr" and
+**: "\<And> as tr. phi as tr \<Longrightarrow> shd as = lab tr" and
+***: "\<And> as tr.
+         phi as tr \<Longrightarrow>
+         \<exists> tr' \<in> listF_set (sub tr). phi (stl as) tr'"
+shows "properPath as tr"
+using properPath_strong_coind[of phi, OF * **] *** by blast
+
+lemma properPath_shd_lab:
+"properPath as tr \<Longrightarrow> shd as = lab tr"
+by (erule properPath.cases) blast
+
+lemma properPath_sub:
+"properPath as tr \<Longrightarrow>
+ \<exists> tr' \<in> listF_set (sub tr). phi (stl as) tr' \<or> properPath (stl as) tr'"
+by (erule properPath.cases) blast
+
+(* prove the following by coinduction *)
+theorem Konig:
+  assumes "infiniteTr tr"
+  shows "properPath (konigPath tr) tr"
+proof-
+  {fix as
+   assume "infiniteTr tr \<and> as = konigPath tr" hence "properPath as tr"
+   proof (induct rule: properPath_coind, safe)
+     fix t
+     let ?t = "SOME t'. t' \<in> listF_set (sub t) \<and> infiniteTr t'"
+     assume "infiniteTr t"
+     hence "\<exists>t' \<in> listF_set (sub t). infiniteTr t'" by simp
+     hence "\<exists>t'. t' \<in> listF_set (sub t) \<and> infiniteTr t'" by blast
+     hence "?t \<in> listF_set (sub t) \<and> infiniteTr ?t" by (elim someI_ex)
+     moreover have "stl (konigPath t) = konigPath ?t" by simp
+     ultimately show "\<exists>t' \<in> listF_set (sub t).
+             infiniteTr t' \<and> stl (konigPath t) = konigPath t'" by blast
+   qed simp
+  }
+  thus ?thesis using assms by blast
+qed
+
+(* some more stream theorems *)
+
+lemma stream_map[simp]: "stream_map f = stream_dtor_unfold (f o shd \<odot> stl)"
+unfolding stream_map_def pair_fun_def shd_def'[abs_def] stl_def'[abs_def]
+  map_pair_def o_def prod_case_beta by simp
+
+definition plus :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<oplus>" 66) where
+  [simp]: "plus xs ys =
+    stream_dtor_unfold ((%(xs, ys). shd xs + shd ys) \<odot> (%(xs, ys). (stl xs, stl ys))) (xs, ys)"
+
+definition scalar :: "nat \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<cdot>" 68) where
+  [simp]: "scalar n = stream_map (\<lambda>x. n * x)"
+
+definition ones :: "nat stream" where [simp]: "ones = stream_dtor_unfold ((%x. 1) \<odot> id) ()"
+definition twos :: "nat stream" where [simp]: "twos = stream_dtor_unfold ((%x. 2) \<odot> id) ()"
+definition ns :: "nat \<Rightarrow> nat stream" where [simp]: "ns n = scalar n ones"
+
+lemma "ones \<oplus> ones = twos"
+by (rule stream.coinduct[of "%x1 x2. \<exists>x. x1 = ones \<oplus> ones \<and> x2 = twos"]) auto
+
+lemma "n \<cdot> twos = ns (2 * n)"
+by (rule stream.coinduct[of "%x1 x2. \<exists>n. x1 = n \<cdot> twos \<and> x2 = ns (2 * n)"]) force+
+
+lemma prod_scalar: "(n * m) \<cdot> xs = n \<cdot> m \<cdot> xs"
+by (rule stream.coinduct[of "%x1 x2. \<exists>n m xs. x1 = (n * m) \<cdot> xs \<and> x2 = n \<cdot> m \<cdot> xs"]) force+
+
+lemma scalar_plus: "n \<cdot> (xs \<oplus> ys) = n \<cdot> xs \<oplus> n \<cdot> ys"
+by (rule stream.coinduct[of "%x1 x2. \<exists>n xs ys. x1 = n \<cdot> (xs \<oplus> ys) \<and> x2 = n \<cdot> xs \<oplus> n \<cdot> ys"])
+   (force simp: add_mult_distrib2)+
+
+lemma plus_comm: "xs \<oplus> ys = ys \<oplus> xs"
+by (rule stream.coinduct[of "%x1 x2. \<exists>xs ys. x1 = xs \<oplus> ys \<and> x2 = ys \<oplus> xs"]) force+
+
+lemma plus_assoc: "(xs \<oplus> ys) \<oplus> zs = xs \<oplus> ys \<oplus> zs"
+by (rule stream.coinduct[of "%x1 x2. \<exists>xs ys zs. x1 = (xs \<oplus> ys) \<oplus> zs \<and> x2 = xs \<oplus> ys \<oplus> zs"]) force+
+
+end
diff -r 4a389d115b4f -r bd145273e7c6 src/HOL/BNF/Examples/Stream.thy
--- a/src/HOL/BNF/Examples/Stream.thy	Fri Dec 14 12:18:51 2012 +0100
+++ b/src/HOL/BNF/Examples/Stream.thy	Fri Dec 14 12:40:07 2012 +0100
@@ -9,141 +9,184 @@
 header {* Infinite Streams *}
 
 theory Stream
-imports TreeFI
+imports "../BNF"
 begin
 
-codata 'a stream = Stream (hdd: 'a) (tll: "'a stream")
-
-(* selectors for streams *)
-lemma hdd_def': "hdd as = fst (stream_dtor as)"
-unfolding hdd_def stream_case_def fst_def by (rule refl)
-
-lemma tll_def': "tll as = snd (stream_dtor as)"
-unfolding tll_def stream_case_def snd_def by (rule refl)
+codata 'a stream = Stream (shd: 'a) (stl: "'a stream")
 
-lemma unfold_pair_fun_hdd[simp]: "hdd (stream_dtor_unfold (f \<odot> g) t) = f t"
-unfolding hdd_def' pair_fun_def stream.dtor_unfold by simp
+(* TODO: Provide by the package*)
+theorem stream_set_induct:
+   "\<lbrakk>\<And>s. P (shd s) s; \<And>s y. \<lbrakk>y \<in> stream_set (stl s); P y (stl s)\<rbrakk> \<Longrightarrow> P y s\<rbrakk> \<Longrightarrow>
+   \<forall>y \<in> stream_set s. P y s"
+by (rule stream.dtor_set_induct)
+   (auto simp add:  shd_def stl_def stream_case_def fsts_def snds_def split_beta)
 
-lemma unfold_pair_fun_tll[simp]: "tll (stream_dtor_unfold (f \<odot> g) t) =
- stream_dtor_unfold (f \<odot> g) (g t)"
-unfolding tll_def' pair_fun_def stream.dtor_unfold by simp
+theorem shd_stream_set: "shd s \<in> stream_set s"
+by (auto simp add: shd_def stl_def stream_case_def fsts_def snds_def split_beta)
+   (metis UnCI fsts_def insertI1 stream.dtor_set)
 
-(* infinite trees: *)
-coinductive infiniteTr where
-"\<lbrakk>tr' \<in> listF_set (sub tr); infiniteTr tr'\<rbrakk> \<Longrightarrow> infiniteTr tr"
+theorem stl_stream_set: "y \<in> stream_set (stl s) \<Longrightarrow> y \<in> stream_set s"
+by (auto simp add: shd_def stl_def stream_case_def fsts_def snds_def split_beta)
+   (metis insertI1 set_mp snds_def stream.dtor_set_set_incl)
 
-lemma infiniteTr_strong_coind[consumes 1, case_names sub]:
-assumes *: "phi tr" and
-**: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> listF_set (sub tr). phi tr' \<or> infiniteTr tr'"
-shows "infiniteTr tr"
-using assms by (elim infiniteTr.coinduct) blast
+(* only for the non-mutual case: *)
+theorem stream_set_induct1[consumes 1, case_names shd stl, induct set: "stream_set"]:
+  assumes "y \<in> stream_set s" and "\<And>s. P (shd s) s"
+  and "\<And>s y. \<lbrakk>y \<in> stream_set (stl s); P y (stl s)\<rbrakk> \<Longrightarrow> P y s"
+  shows "P y s"
+using assms stream_set_induct by blast
+(* end TODO *)
 
-lemma infiniteTr_coind[consumes 1, case_names sub, induct pred: infiniteTr]:
-assumes *: "phi tr" and
-**: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> listF_set (sub tr). phi tr'"
-shows "infiniteTr tr"
-using assms by (elim infiniteTr.coinduct) blast
+
+subsection {* prepend list to stream *}
 
-lemma infiniteTr_sub[simp]:
-"infiniteTr tr \<Longrightarrow> (\<exists> tr' \<in> listF_set (sub tr). infiniteTr tr')"
-by (erule infiniteTr.cases) blast
+primrec shift :: "'a list \<Rightarrow> 'a stream \<Rightarrow> 'a stream" (infixr "@-" 65) where
+  "shift [] s = s"
+| "shift (x # xs) s = Stream x (shift xs s)"
+
+lemma shift_append[simp]: "(xs @ ys) @- s = xs @- ys @- s"
+by (induct xs) auto
 
-definition "konigPath \<equiv> stream_dtor_unfold
-  (lab \<odot> (\<lambda>tr. SOME tr'. tr' \<in> listF_set (sub tr) \<and> infiniteTr tr'))"
+lemma shift_simps[simp]:
+   "shd (xs @- s) = (if xs = [] then shd s else hd xs)"
+   "stl (xs @- s) = (if xs = [] then stl s else tl xs @- s)"
+by (induct xs) auto
 
-lemma konigPath_simps[simp]:
-"hdd (konigPath t) = lab t"
-"tll (konigPath t) = konigPath (SOME tr. tr \<in> listF_set (sub t) \<and> infiniteTr tr)"
-unfolding konigPath_def by simp+
+
+subsection {* recurring stream out of a list *}
 
-(* proper paths in trees: *)
-coinductive properPath where
-"\<lbrakk>hdd as = lab tr; tr' \<in> listF_set (sub tr); properPath (tll as) tr'\<rbrakk> \<Longrightarrow>
- properPath as tr"
+definition cycle :: "'a list \<Rightarrow> 'a stream" where
+  "cycle = stream_unfold hd (\<lambda>xs. tl xs @ [hd xs])"
+
+lemma cycle_simps[simp]:
+  "shd (cycle u) = hd u"
+  "stl (cycle u) = cycle (tl u @ [hd u])"
+by (auto simp: cycle_def)
 
-lemma properPath_strong_coind[consumes 1, case_names hdd_lab sub]:
-assumes *: "phi as tr" and
-**: "\<And> as tr. phi as tr \<Longrightarrow> hdd as = lab tr" and
-***: "\<And> as tr.
-         phi as tr \<Longrightarrow>
-         \<exists> tr' \<in> listF_set (sub tr). phi (tll as) tr' \<or> properPath (tll as) tr'"
-shows "properPath as tr"
-using assms by (elim properPath.coinduct) blast
 
-lemma properPath_coind[consumes 1, case_names hdd_lab sub, induct pred: properPath]:
-assumes *: "phi as tr" and
-**: "\<And> as tr. phi as tr \<Longrightarrow> hdd as = lab tr" and
-***: "\<And> as tr.
-         phi as tr \<Longrightarrow>
-         \<exists> tr' \<in> listF_set (sub tr). phi (tll as) tr'"
-shows "properPath as tr"
-using properPath_strong_coind[of phi, OF * **] *** by blast
+lemma cycle_decomp: "u \<noteq> [] \<Longrightarrow> cycle u = u @- cycle u"
+proof (coinduct rule: stream.coinduct[of "\<lambda>s1 s2. \<exists>u. s1 = cycle u \<and> s2 = u @- cycle u \<and> u \<noteq> []"])
+  case (2 s1 s2)
+  then obtain u where "s1 = cycle u \<and> s2 = u @- cycle u \<and> u \<noteq> []" by blast
+  thus ?case using stream.unfold[of hd "\<lambda>xs. tl xs @ [hd xs]" u] by (auto simp: cycle_def)
+qed auto
 
-lemma properPath_hdd_lab:
-"properPath as tr \<Longrightarrow> hdd as = lab tr"
-by (erule properPath.cases) blast
+lemma cycle_Cons: "cycle (x # xs) = Stream x (cycle (xs @ [x]))"
+proof (coinduct rule: stream.coinduct[of "\<lambda>s1 s2. \<exists>x xs. s1 = cycle (x # xs) \<and> s2 = Stream x (cycle (xs @ [x]))"])
+  case (2 s1 s2)
+  then obtain x xs where "s1 = cycle (x # xs) \<and> s2 = Stream x (cycle (xs @ [x]))" by blast
+  thus ?case
+    by (auto simp: cycle_def intro!: exI[of _ "hd (xs @ [x])"] exI[of _ "tl (xs @ [x])"] stream.unfold)
+qed auto
 
-lemma properPath_sub:
-"properPath as tr \<Longrightarrow>
- \<exists> tr' \<in> listF_set (sub tr). phi (tll as) tr' \<or> properPath (tll as) tr'"
-by (erule properPath.cases) blast
+coinductive_set
+  streams :: "'a set => 'a stream set"
+  for A :: "'a set"
+where
+  Stream[intro!, simp, no_atp]: "\<lbrakk>a \<in> A; s \<in> streams A\<rbrakk> \<Longrightarrow> Stream a s \<in> streams A"
 
-(* prove the following by coinduction *)
-theorem Konig:
-  assumes "infiniteTr tr"
-  shows "properPath (konigPath tr) tr"
-proof-
-  {fix as
-   assume "infiniteTr tr \<and> as = konigPath tr" hence "properPath as tr"
-   proof (induct rule: properPath_coind, safe)
-     fix t
-     let ?t = "SOME t'. t' \<in> listF_set (sub t) \<and> infiniteTr t'"
-     assume "infiniteTr t"
-     hence "\<exists>t' \<in> listF_set (sub t). infiniteTr t'" by simp
-     hence "\<exists>t'. t' \<in> listF_set (sub t) \<and> infiniteTr t'" by blast
-     hence "?t \<in> listF_set (sub t) \<and> infiniteTr ?t" by (elim someI_ex)
-     moreover have "tll (konigPath t) = konigPath ?t" by simp
-     ultimately show "\<exists>t' \<in> listF_set (sub t).
-             infiniteTr t' \<and> tll (konigPath t) = konigPath t'" by blast
-   qed simp
-  }
-  thus ?thesis using assms by blast
+lemma shift_streams: "\<lbrakk>w \<in> lists A; s \<in> streams A\<rbrakk> \<Longrightarrow> w @- s \<in> streams A"
+by (induct w) auto
+
+lemma stream_set_streams:
+  assumes "stream_set s \<subseteq> A"
+  shows "s \<in> streams A"
+proof (coinduct rule: streams.coinduct[of "\<lambda>s'. \<exists>a s. s' = Stream a s \<and> a \<in> A \<and> stream_set s \<subseteq> A"])
+  case streams from assms show ?case by (cases s) auto
+next
+  fix s' assume "\<exists>a s. s' = Stream a s \<and> a \<in> A \<and> stream_set s \<subseteq> A"
+  then guess a s by (elim exE)
+  with assms show "\<exists>a l. s' = Stream a l \<and>
+    a \<in> A \<and> ((\<exists>a s. l = Stream a s \<and> a \<in> A \<and> stream_set s \<subseteq> A) \<or> l \<in> streams A)"
+    by (cases s) auto
 qed
 
-(* some more stream theorems *)
+
+subsection {* flatten a stream of lists *}
+
+definition flat where
+  "flat \<equiv> stream_unfold (hd o shd) (\<lambda>s. if tl (shd s) = [] then stl s else Stream (tl (shd s)) (stl s))"
 
-lemma stream_map[simp]: "stream_map f = stream_dtor_unfold (f o hdd \<odot> tll)"
-unfolding stream_map_def pair_fun_def hdd_def'[abs_def] tll_def'[abs_def]
-  map_pair_def o_def prod_case_beta by simp
+lemma flat_simps[simp]:
+  "shd (flat ws) = hd (shd ws)"
+  "stl (flat ws) = flat (if tl (shd ws) = [] then stl ws else Stream (tl (shd ws)) (stl ws))"
+unfolding flat_def by auto
+
+lemma flat_Cons[simp]: "flat (Stream (x#xs) w) = Stream x (flat (if xs = [] then w else Stream xs w))"
+unfolding flat_def using stream.unfold[of "hd o shd" _ "Stream (x#xs) w"] by auto
+
+lemma flat_Stream[simp]: "xs \<noteq> [] \<Longrightarrow> flat (Stream xs ws) = xs @- flat ws"
+by (induct xs) auto
+
+lemma flat_unfold: "shd ws \<noteq> [] \<Longrightarrow> flat ws = shd ws @- flat (stl ws)"
+by (cases ws) auto
+
 
-definition plus :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<oplus>" 66) where
-  [simp]: "plus xs ys =
-    stream_dtor_unfold ((%(xs, ys). hdd xs + hdd ys) \<odot> (%(xs, ys). (tll xs, tll ys))) (xs, ys)"
+subsection {* take, drop, nth for streams *}
+
+primrec stake :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a list" where
+  "stake 0 s = []"
+| "stake (Suc n) s = shd s # stake n (stl s)"
+
+primrec sdrop :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where
+  "sdrop 0 s = s"
+| "sdrop (Suc n) s = sdrop n (stl s)"
 
-definition scalar :: "nat \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<cdot>" 68) where
-  [simp]: "scalar n = stream_map (\<lambda>x. n * x)"
+primrec snth :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a" where
+  "snth 0 s = shd s"
+| "snth (Suc n) s = snth n (stl s)"
 
-definition ones :: "nat stream" where [simp]: "ones = stream_dtor_unfold ((%x. 1) \<odot> id) ()"
-definition twos :: "nat stream" where [simp]: "twos = stream_dtor_unfold ((%x. 2) \<odot> id) ()"
-definition ns :: "nat \<Rightarrow> nat stream" where [simp]: "ns n = scalar n ones"
+lemma stake_sdrop: "stake n s @- sdrop n s = s"
+by (induct n arbitrary: s) auto
+
+lemma stake_empty: "stake n s = [] \<longleftrightarrow> n = 0"
+by (cases n) auto
+
+lemma sdrop_shift: "\<lbrakk>s = w @- s'; length w = n\<rbrakk> \<Longrightarrow> sdrop n s = s'"
+by (induct n arbitrary: w s) auto
 
-lemma "ones \<oplus> ones = twos"
-by (rule stream.coinduct[of "%x1 x2. \<exists>x. x1 = ones \<oplus> ones \<and> x2 = twos"]) auto
+lemma stake_shift: "\<lbrakk>s = w @- s'; length w = n\<rbrakk> \<Longrightarrow> stake n s = w"
+by (induct n arbitrary: w s) auto
+
+lemma stake_add[simp]: "stake m s @ stake n (sdrop m s) = stake (m + n) s"
+by (induct m arbitrary: s) auto
 
-lemma "n \<cdot> twos = ns (2 * n)"
-by (rule stream.coinduct[of "%x1 x2. \<exists>n. x1 = n \<cdot> twos \<and> x2 = ns (2 * n)"]) force+
+lemma sdrop_add[simp]: "sdrop n (sdrop m s) = sdrop (m + n) s"
+by (induct m arbitrary: s) auto
 
-lemma prod_scalar: "(n * m) \<cdot> xs = n \<cdot> m \<cdot> xs"
-by (rule stream.coinduct[of "%x1 x2. \<exists>n m xs. x1 = (n * m) \<cdot> xs \<and> x2 = n \<cdot> m \<cdot> xs"]) force+
+lemma cycle_rotated: "\<lbrakk>v \<noteq> []; cycle u = v @- s\<rbrakk> \<Longrightarrow> cycle (tl u @ [hd u]) = tl v @- s"
+by (auto dest: arg_cong[of _ _ stl])
+
+lemma stake_append: "stake n (u @- s) = take (min (length u) n) u @ stake (n - length u) s"
+proof (induct n arbitrary: u)
+  case (Suc n) thus ?case by (cases u) auto
+qed auto
 
-lemma scalar_plus: "n \<cdot> (xs \<oplus> ys) = n \<cdot> xs \<oplus> n \<cdot> ys"
-by (rule stream.coinduct[of "%x1 x2. \<exists>n xs ys. x1 = n \<cdot> (xs \<oplus> ys) \<and> x2 = n \<cdot> xs \<oplus> n \<cdot> ys"])
-   (force simp: add_mult_distrib2)+
+lemma stake_cycle_le[simp]:
+  assumes "u \<noteq> []" "n < length u"
+  shows "stake n (cycle u) = take n u"
+using min_absorb2[OF less_imp_le_nat[OF assms(2)]]
+by (subst cycle_decomp[OF assms(1)], subst stake_append) auto
+
+lemma stake_cycle_eq[simp]: "u \<noteq> [] \<Longrightarrow> stake (length u) (cycle u) = u"
+by (metis cycle_decomp stake_shift)
+
+lemma sdrop_cycle_eq[simp]: "u \<noteq> [] \<Longrightarrow> sdrop (length u) (cycle u) = cycle u"
+by (metis cycle_decomp sdrop_shift)
 
-lemma plus_comm: "xs \<oplus> ys = ys \<oplus> xs"
-by (rule stream.coinduct[of "%x1 x2. \<exists>xs ys. x1 = xs \<oplus> ys \<and> x2 = ys \<oplus> xs"]) force+
+lemma stake_cycle_eq_mod_0[simp]: "\<lbrakk>u \<noteq> []; n mod length u = 0\<rbrakk> \<Longrightarrow>
+   stake n (cycle u) = concat (replicate (n div length u) u)"
+by (induct "n div length u" arbitrary: n u) (auto simp: stake_add[symmetric])
 
-lemma plus_assoc: "(xs \<oplus> ys) \<oplus> zs = xs \<oplus> ys \<oplus> zs"
-by (rule stream.coinduct[of "%x1 x2. \<exists>xs ys zs. x1 = (xs \<oplus> ys) \<oplus> zs \<and> x2 = xs \<oplus> ys \<oplus> zs"]) force+
+lemma sdrop_cycle_eq_mod_0[simp]: "\<lbrakk>u \<noteq> []; n mod length u = 0\<rbrakk> \<Longrightarrow>
+   sdrop n (cycle u) = cycle u"
+by (induct "n div length u" arbitrary: n u) (auto simp: sdrop_add[symmetric])
+
+lemma stake_cycle: "u \<noteq> [] \<Longrightarrow>
+   stake n (cycle u) = concat (replicate (n div length u) u) @ take (n mod length u) u"
+by (subst mod_div_equality[of n "length u", symmetric], unfold stake_add[symmetric]) auto
+
+lemma sdrop_cycle: "u \<noteq> [] \<Longrightarrow> sdrop n (cycle u) = cycle (rotate (n mod length u) u)"
+by (induct n arbitrary: u) (auto simp: rotate1_rotate_swap rotate1_hd_tl rotate_conv_mod[symmetric])
 
 end
diff -r 4a389d115b4f -r bd145273e7c6 src/HOL/BNF/Examples/TreeFI.thy
--- a/src/HOL/BNF/Examples/TreeFI.thy	Fri Dec 14 12:18:51 2012 +0100
+++ b/src/HOL/BNF/Examples/TreeFI.thy	Fri Dec 14 12:40:07 2012 +0100
@@ -12,8 +12,6 @@
 imports ListF
 begin
 
-hide_const (open) Sublist.sub
-
 codata 'a treeFI = Tree (lab: 'a) (sub: "'a treeFI listF")
 
 lemma pre_treeFI_listF_set[simp]: "pre_treeFI_set2 (i, xs) = listF_set xs"
diff -r 4a389d115b4f -r bd145273e7c6 src/HOL/BNF/Examples/TreeFsetI.thy
--- a/src/HOL/BNF/Examples/TreeFsetI.thy	Fri Dec 14 12:18:51 2012 +0100
+++ b/src/HOL/BNF/Examples/TreeFsetI.thy	Fri Dec 14 12:40:07 2012 +0100
@@ -12,7 +12,6 @@
 imports "../BNF"
 begin
 
-hide_const (open) Sublist.sub
 hide_fact (open) Quotient_Product.prod_rel_def
 
 codata 'a treeFsetI = Tree (lab: 'a) (sub: "'a treeFsetI fset")
diff -r 4a389d115b4f -r bd145273e7c6 src/HOL/Library/Sublist.thy
--- a/src/HOL/Library/Sublist.thy	Fri Dec 14 12:18:51 2012 +0100
+++ b/src/HOL/Library/Sublist.thy	Fri Dec 14 12:40:07 2012 +0100
@@ -3,7 +3,7 @@
     Author:     Christian Sternagel, JAIST
 *)
 
-header {* List prefixes, suffixes, and embedding*}
+header {* List prefixes, suffixes, and homeomorphic embedding *}
 
 theory Sublist
 imports Main
@@ -11,10 +11,10 @@
 
 subsection {* Prefix order on lists *}
 
-definition prefixeq :: "'a list => 'a list => bool"
+definition prefixeq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   where "prefixeq xs ys \<longleftrightarrow> (\<exists>zs. ys = xs @ zs)"
 
-definition prefix :: "'a list => 'a list => bool"
+definition prefix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   where "prefix xs ys \<longleftrightarrow> prefixeq xs ys \<and> xs \<noteq> ys"
 
 interpretation prefix_order: order prefixeq prefix
@@ -23,7 +23,7 @@
 interpretation prefix_bot: bot prefixeq prefix Nil
   by default (simp add: prefixeq_def)
 
-lemma prefixeqI [intro?]: "ys = xs @ zs ==> prefixeq xs ys"
+lemma prefixeqI [intro?]: "ys = xs @ zs \<Longrightarrow> prefixeq xs ys"
   unfolding prefixeq_def by blast
 
 lemma prefixeqE [elim?]:
@@ -31,7 +31,7 @@
   obtains zs where "ys = xs @ zs"
   using assms unfolding prefixeq_def by blast
 
-lemma prefixI' [intro?]: "ys = xs @ z # zs ==> prefix xs ys"
+lemma prefixI' [intro?]: "ys = xs @ z # zs \<Longrightarrow> prefix xs ys"
   unfolding prefix_def prefixeq_def by blast
 
 lemma prefixE' [elim?]:
@@ -43,7 +43,7 @@
   with that show ?thesis by (auto simp add: neq_Nil_conv)
 qed
 
-lemma prefixI [intro?]: "prefixeq xs ys ==> xs \<noteq> ys ==> prefix xs ys"
+lemma prefixI [intro?]: "prefixeq xs ys \<Longrightarrow> xs \<noteq> ys \<Longrightarrow> prefix xs ys"
   unfolding prefix_def by blast
 
 lemma prefixE [elim?]:
@@ -88,7 +88,7 @@
 lemma same_prefixeq_nil [iff]: "prefixeq (xs @ ys) xs = (ys = [])"
   by (metis append_Nil2 append_self_conv prefix_order.eq_iff prefixeqI)
 
-lemma prefixeq_prefixeq [simp]: "prefixeq xs ys ==> prefixeq xs (ys @ zs)"
+lemma prefixeq_prefixeq [simp]: "prefixeq xs ys \<Longrightarrow> prefixeq xs (ys @ zs)"
   by (metis prefix_order.le_less_trans prefixeqI prefixE prefixI)
 
 lemma append_prefixeqD: "prefixeq (xs @ ys) zs \<Longrightarrow> prefixeq xs zs"
@@ -106,12 +106,12 @@
   done
 
 lemma append_one_prefixeq:
-  "prefixeq xs ys ==> length xs < length ys ==> prefixeq (xs @ [ys ! length xs]) ys"
+  "prefixeq xs ys \<Longrightarrow> length xs < length ys \<Longrightarrow> prefixeq (xs @ [ys ! length xs]) ys"
   unfolding prefixeq_def
   by (metis Cons_eq_appendI append_eq_appendI append_eq_conv_conj
     eq_Nil_appendI nth_drop')
 
-theorem prefixeq_length_le: "prefixeq xs ys ==> length xs \<le> length ys"
+theorem prefixeq_length_le: "prefixeq xs ys \<Longrightarrow> length xs \<le> length ys"
   by (auto simp add: prefixeq_def)
 
 lemma prefixeq_same_cases:
@@ -191,10 +191,10 @@
 
 subsection {* Parallel lists *}
 
-definition parallel :: "'a list => 'a list => bool"  (infixl "\<parallel>" 50)
+definition parallel :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"  (infixl "\<parallel>" 50)
   where "(xs \<parallel> ys) = (\<not> prefixeq xs ys \<and> \<not> prefixeq ys xs)"
 
-lemma parallelI [intro]: "\<not> prefixeq xs ys ==> \<not> prefixeq ys xs ==> xs \<parallel> ys"
+lemma parallelI [intro]: "\<not> prefixeq xs ys \<Longrightarrow> \<not> prefixeq ys xs \<Longrightarrow> xs \<parallel> ys"
   unfolding parallel_def by blast
 
 lemma parallelE [elim]:
@@ -207,7 +207,7 @@
   unfolding parallel_def prefix_def by blast
 
 theorem parallel_decomp:
-  "xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs"
+  "xs \<parallel> ys \<Longrightarrow> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs"
 proof (induct xs rule: rev_induct)
   case Nil
   then have False by auto
@@ -268,7 +268,7 @@
   "suffix xs ys \<Longrightarrow> suffixeq xs ys"
   by (auto simp: suffixeq_def suffix_def)
 
-lemma suffixeqI [intro?]: "ys = zs @ xs ==> suffixeq xs ys"
+lemma suffixeqI [intro?]: "ys = zs @ xs \<Longrightarrow> suffixeq xs ys"
   unfolding suffixeq_def by blast
 
 lemma suffixeqE [elim?]:
@@ -420,268 +420,262 @@
   unfolding suffix_def by auto
 
 
-subsection {* Embedding on lists *}
+subsection {* Homeomorphic embedding on lists *}
 
-inductive emb :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
+inductive list_hembeq :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   for P :: "('a \<Rightarrow> 'a \<Rightarrow> bool)"
 where
-  emb_Nil [intro, simp]: "emb P [] ys"
-| emb_Cons [intro] : "emb P xs ys \<Longrightarrow> emb P xs (y#ys)"
-| emb_Cons2 [intro]: "P x y \<Longrightarrow> emb P xs ys \<Longrightarrow> emb P (x#xs) (y#ys)"
+  list_hembeq_Nil [intro, simp]: "list_hembeq P [] ys"
+| list_hembeq_Cons [intro] : "list_hembeq P xs ys \<Longrightarrow> list_hembeq P xs (y#ys)"
+| list_hembeq_Cons2 [intro]: "P\<^sup>=\<^sup>= x y \<Longrightarrow> list_hembeq P xs ys \<Longrightarrow> list_hembeq P (x#xs) (y#ys)"
+
+lemma list_hembeq_Nil2 [simp]:
+  assumes "list_hembeq P xs []" shows "xs = []"
+  using assms by (cases rule: list_hembeq.cases) auto
 
-lemma emb_Nil2 [simp]:
-  assumes "emb P xs []" shows "xs = []"
-  using assms by (cases rule: emb.cases) auto
+lemma list_hembeq_refl [simp, intro!]:
+  "list_hembeq P xs xs"
+  by (induct xs) auto
 
-lemma emb_Cons_Nil [simp]: "emb P (x#xs) [] = False"
+lemma list_hembeq_Cons_Nil [simp]: "list_hembeq P (x#xs) [] = False"
 proof -
-  { assume "emb P (x#xs) []"
-    from emb_Nil2 [OF this] have False by simp
+  { assume "list_hembeq P (x#xs) []"
+    from list_hembeq_Nil2 [OF this] have False by simp
   } moreover {
     assume False
-    then have "emb P (x#xs) []" by simp
+    then have "list_hembeq P (x#xs) []" by simp
   } ultimately show ?thesis by blast
 qed
 
-lemma emb_append2 [intro]: "emb P xs ys \<Longrightarrow> emb P xs (zs @ ys)"
+lemma list_hembeq_append2 [intro]: "list_hembeq P xs ys \<Longrightarrow> list_hembeq P xs (zs @ ys)"
   by (induct zs) auto
 
-lemma emb_prefix [intro]:
-  assumes "emb P xs ys" shows "emb P xs (ys @ zs)"
+lemma list_hembeq_prefix [intro]:
+  assumes "list_hembeq P xs ys" shows "list_hembeq P xs (ys @ zs)"
   using assms
   by (induct arbitrary: zs) auto
 
-lemma emb_ConsD:
-  assumes "emb P (x#xs) ys"
-  shows "\<exists>us v vs. ys = us @ v # vs \<and> P x v \<and> emb P xs vs"
+lemma list_hembeq_ConsD:
+  assumes "list_hembeq P (x#xs) ys"
+  shows "\<exists>us v vs. ys = us @ v # vs \<and> P\<^sup>=\<^sup>= x v \<and> list_hembeq P xs vs"
 using assms
 proof (induct x \<equiv> "x # xs" ys arbitrary: x xs)
-  case emb_Cons
+  case list_hembeq_Cons
   then show ?case by (metis append_Cons)
 next
-  case (emb_Cons2 x y xs ys)
+  case (list_hembeq_Cons2 x y xs ys)
   then show ?case by (cases xs) (auto, blast+)
 qed
 
-lemma emb_appendD:
-  assumes "emb P (xs @ ys) zs"
-  shows "\<exists>us vs. zs = us @ vs \<and> emb P xs us \<and> emb P ys vs"
+lemma list_hembeq_appendD:
+  assumes "list_hembeq P (xs @ ys) zs"
+  shows "\<exists>us vs. zs = us @ vs \<and> list_hembeq P xs us \<and> list_hembeq P ys vs"
 using assms
 proof (induction xs arbitrary: ys zs)
   case Nil then show ?case by auto
 next
   case (Cons x xs)
   then obtain us v vs where "zs = us @ v # vs"
-    and "P x v" and "emb P (xs @ ys) vs" by (auto dest: emb_ConsD)
-  with Cons show ?case by (metis append_Cons append_assoc emb_Cons2 emb_append2)
+    and "P\<^sup>=\<^sup>= x v" and "list_hembeq P (xs @ ys) vs" by (auto dest: list_hembeq_ConsD)
+  with Cons show ?case by (metis append_Cons append_assoc list_hembeq_Cons2 list_hembeq_append2)
 qed
 
-lemma emb_suffix:
-  assumes "emb P xs ys" and "suffix ys zs"
-  shows "emb P xs zs"
-  using assms(2) and emb_append2 [OF assms(1)] by (auto simp: suffix_def)
-
-lemma emb_suffixeq:
-  assumes "emb P xs ys" and "suffixeq ys zs"
-  shows "emb P xs zs"
-  using assms and emb_suffix unfolding suffixeq_suffix_reflclp_conv by auto
+lemma list_hembeq_suffix:
+  assumes "list_hembeq P xs ys" and "suffix ys zs"
+  shows "list_hembeq P xs zs"
+  using assms(2) and list_hembeq_append2 [OF assms(1)] by (auto simp: suffix_def)
 
-lemma emb_length: "emb P xs ys \<Longrightarrow> length xs \<le> length ys"
-  by (induct rule: emb.induct) auto
+lemma list_hembeq_suffixeq:
+  assumes "list_hembeq P xs ys" and "suffixeq ys zs"
+  shows "list_hembeq P xs zs"
+  using assms and list_hembeq_suffix unfolding suffixeq_suffix_reflclp_conv by auto
 
-(*FIXME: move*)
-definition transp_on :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
-  where "transp_on P A \<longleftrightarrow> (\<forall>a\<in>A. \<forall>b\<in>A. \<forall>c\<in>A. P a b \<and> P b c \<longrightarrow> P a c)"
-lemma transp_onI [Pure.intro]:
-  "(\<And>a b c. \<lbrakk>a \<in> A; b \<in> A; c \<in> A; P a b; P b c\<rbrakk> \<Longrightarrow> P a c) \<Longrightarrow> transp_on P A"
-  unfolding transp_on_def by blast
+lemma list_hembeq_length: "list_hembeq P xs ys \<Longrightarrow> length xs \<le> length ys"
+  by (induct rule: list_hembeq.induct) auto
 
-lemma transp_on_emb:
-  assumes "transp_on P A"
-  shows "transp_on (emb P) (lists A)"
-proof
+lemma list_hembeq_trans:
+  assumes "\<And>x y z. \<lbrakk>x \<in> A; y \<in> A; z \<in> A; P x y; P y z\<rbrakk> \<Longrightarrow> P x z"
+  shows "\<And>xs ys zs. \<lbrakk>xs \<in> lists A; ys \<in> lists A; zs \<in> lists A;
+    list_hembeq P xs ys; list_hembeq P ys zs\<rbrakk> \<Longrightarrow> list_hembeq P xs zs"
+proof -
   fix xs ys zs
-  assume "emb P xs ys" and "emb P ys zs"
+  assume "list_hembeq P xs ys" and "list_hembeq P ys zs"
     and "xs \<in> lists A" and "ys \<in> lists A" and "zs \<in> lists A"
-  then show "emb P xs zs"
+  then show "list_hembeq P xs zs"
   proof (induction arbitrary: zs)
-    case emb_Nil show ?case by blast
+    case list_hembeq_Nil show ?case by blast
   next
-    case (emb_Cons xs ys y)
-    from emb_ConsD [OF `emb P (y#ys) zs`] obtain us v vs
-      where zs: "zs = us @ v # vs" and "P y v" and "emb P ys vs" by blast
-    then have "emb P ys (v#vs)" by blast
-    then have "emb P ys zs" unfolding zs by (rule emb_append2)
-    from emb_Cons.IH [OF this] and emb_Cons.prems show ?case by simp
+    case (list_hembeq_Cons xs ys y)
+    from list_hembeq_ConsD [OF `list_hembeq P (y#ys) zs`] obtain us v vs
+      where zs: "zs = us @ v # vs" and "P\<^sup>=\<^sup>= y v" and "list_hembeq P ys vs" by blast
+    then have "list_hembeq P ys (v#vs)" by blast
+    then have "list_hembeq P ys zs" unfolding zs by (rule list_hembeq_append2)
+    from list_hembeq_Cons.IH [OF this] and list_hembeq_Cons.prems show ?case by simp
   next
-    case (emb_Cons2 x y xs ys)
-    from emb_ConsD [OF `emb P (y#ys) zs`] obtain us v vs
-      where zs: "zs = us @ v # vs" and "P y v" and "emb P ys vs" by blast
-    with emb_Cons2 have "emb P xs vs" by simp
-    moreover have "P x v"
+    case (list_hembeq_Cons2 x y xs ys)
+    from list_hembeq_ConsD [OF `list_hembeq P (y#ys) zs`] obtain us v vs
+      where zs: "zs = us @ v # vs" and "P\<^sup>=\<^sup>= y v" and "list_hembeq P ys vs" by blast
+    with list_hembeq_Cons2 have "list_hembeq P xs vs" by simp
+    moreover have "P\<^sup>=\<^sup>= x v"
     proof -
       from zs and `zs \<in> lists A` have "v \<in> A" by auto
-      moreover have "x \<in> A" and "y \<in> A" using emb_Cons2 by simp_all
-      ultimately show ?thesis using `P x y` and `P y v` and assms
-        unfolding transp_on_def by blast
+      moreover have "x \<in> A" and "y \<in> A" using list_hembeq_Cons2 by simp_all
+      ultimately show ?thesis
+        using `P\<^sup>=\<^sup>= x y` and `P\<^sup>=\<^sup>= y v` and assms
+        by blast
     qed
-    ultimately have "emb P (x#xs) (v#vs)" by blast
-    then show ?case unfolding zs by (rule emb_append2)
+    ultimately have "list_hembeq P (x#xs) (v#vs)" by blast
+    then show ?case unfolding zs by (rule list_hembeq_append2)
   qed
 qed
 
 
-subsection {* Sublists (special case of embedding) *}
+subsection {* Sublists (special case of homeomorphic embedding) *}
 
-abbreviation sub :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
-  where "sub xs ys \<equiv> emb (op =) xs ys"
+abbreviation sublisteq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
+  where "sublisteq xs ys \<equiv> list_hembeq (op =) xs ys"
 
-lemma sub_Cons2: "sub xs ys \<Longrightarrow> sub (x#xs) (x#ys)" by auto
+lemma sublisteq_Cons2: "sublisteq xs ys \<Longrightarrow> sublisteq (x#xs) (x#ys)" by auto
 
-lemma sub_same_length:
-  assumes "sub xs ys" and "length xs = length ys" shows "xs = ys"
-  using assms by (induct) (auto dest: emb_length)
+lemma sublisteq_same_length:
+  assumes "sublisteq xs ys" and "length xs = length ys" shows "xs = ys"
+  using assms by (induct) (auto dest: list_hembeq_length)
 
-lemma not_sub_length [simp]: "length ys < length xs \<Longrightarrow> \<not> sub xs ys"
-  by (metis emb_length linorder_not_less)
+lemma not_sublisteq_length [simp]: "length ys < length xs \<Longrightarrow> \<not> sublisteq xs ys"
+  by (metis list_hembeq_length linorder_not_less)
 
 lemma [code]:
-  "emb P [] ys \<longleftrightarrow> True"
-  "emb P (x#xs) [] \<longleftrightarrow> False"
+  "list_hembeq P [] ys \<longleftrightarrow> True"
+  "list_hembeq P (x#xs) [] \<longleftrightarrow> False"
   by (simp_all)
 
-lemma sub_Cons': "sub (x#xs) ys \<Longrightarrow> sub xs ys"
-  by (induct xs) (auto dest: emb_ConsD)
+lemma sublisteq_Cons': "sublisteq (x#xs) ys \<Longrightarrow> sublisteq xs ys"
+  by (induct xs) (auto dest: list_hembeq_ConsD)
 
-lemma sub_Cons2':
-  assumes "sub (x#xs) (x#ys)" shows "sub xs ys"
-  using assms by (cases) (rule sub_Cons')
+lemma sublisteq_Cons2':
+  assumes "sublisteq (x#xs) (x#ys)" shows "sublisteq xs ys"
+  using assms by (cases) (rule sublisteq_Cons')
 
-lemma sub_Cons2_neq:
-  assumes "sub (x#xs) (y#ys)"
-  shows "x \<noteq> y \<Longrightarrow> sub (x#xs) ys"
+lemma sublisteq_Cons2_neq:
+  assumes "sublisteq (x#xs) (y#ys)"
+  shows "x \<noteq> y \<Longrightarrow> sublisteq (x#xs) ys"
   using assms by (cases) auto
 
-lemma sub_Cons2_iff [simp, code]:
-  "sub (x#xs) (y#ys) = (if x = y then sub xs ys else sub (x#xs) ys)"
-  by (metis emb_Cons emb_Cons2 [of "op =", OF refl] sub_Cons2' sub_Cons2_neq)
+lemma sublisteq_Cons2_iff [simp, code]:
+  "sublisteq (x#xs) (y#ys) = (if x = y then sublisteq xs ys else sublisteq (x#xs) ys)"
+  by (metis list_hembeq_Cons sublisteq_Cons2 sublisteq_Cons2' sublisteq_Cons2_neq)
 
-lemma sub_append': "sub (zs @ xs) (zs @ ys) \<longleftrightarrow> sub xs ys"
+lemma sublisteq_append': "sublisteq (zs @ xs) (zs @ ys) \<longleftrightarrow> sublisteq xs ys"
   by (induct zs) simp_all
 
-lemma sub_refl [simp, intro!]: "sub xs xs" by (induct xs) simp_all
+lemma sublisteq_refl [simp, intro!]: "sublisteq xs xs" by (induct xs) simp_all
 
-lemma sub_antisym:
-  assumes "sub xs ys" and "sub ys xs"
+lemma sublisteq_antisym:
+  assumes "sublisteq xs ys" and "sublisteq ys xs"
   shows "xs = ys"
 using assms
 proof (induct)
-  case emb_Nil
-  from emb_Nil2 [OF this] show ?case by simp
+  case list_hembeq_Nil
+  from list_hembeq_Nil2 [OF this] show ?case by simp
 next
-  case emb_Cons2
+  case list_hembeq_Cons2
   then show ?case by simp
 next
-  case emb_Cons
+  case list_hembeq_Cons
   then show ?case
-    by (metis sub_Cons' emb_length Suc_length_conv Suc_n_not_le_n)
+    by (metis sublisteq_Cons' list_hembeq_length Suc_length_conv Suc_n_not_le_n)
 qed
 
-lemma transp_on_sub: "transp_on sub UNIV"
-proof -
-  have "transp_on (op =) UNIV" by (simp add: transp_on_def)
-  from transp_on_emb [OF this] show ?thesis by simp
-qed
+lemma sublisteq_trans: "sublisteq xs ys \<Longrightarrow> sublisteq ys zs \<Longrightarrow> sublisteq xs zs"
+  by (rule list_hembeq_trans [of UNIV "op ="]) auto
 
-lemma sub_trans: "sub xs ys \<Longrightarrow> sub ys zs \<Longrightarrow> sub xs zs"
-  using transp_on_sub [unfolded transp_on_def] by blast
+lemma sublisteq_append_le_same_iff: "sublisteq (xs @ ys) ys \<longleftrightarrow> xs = []"
+  by (auto dest: list_hembeq_length)
 
-lemma sub_append_le_same_iff: "sub (xs @ ys) ys \<longleftrightarrow> xs = []"
-  by (auto dest: emb_length)
-
-lemma emb_append_mono:
-  "\<lbrakk> emb P xs xs'; emb P ys ys' \<rbrakk> \<Longrightarrow> emb P (xs@ys) (xs'@ys')"
-  apply (induct rule: emb.induct)
-    apply (metis eq_Nil_appendI emb_append2)
-   apply (metis append_Cons emb_Cons)
-  apply (metis append_Cons emb_Cons2)
+lemma list_hembeq_append_mono:
+  "\<lbrakk> list_hembeq P xs xs'; list_hembeq P ys ys' \<rbrakk> \<Longrightarrow> list_hembeq P (xs@ys) (xs'@ys')"
+  apply (induct rule: list_hembeq.induct)
+    apply (metis eq_Nil_appendI list_hembeq_append2)
+   apply (metis append_Cons list_hembeq_Cons)
+  apply (metis append_Cons list_hembeq_Cons2)
   done
 
 
 subsection {* Appending elements *}
 
-lemma sub_append [simp]:
-  "sub (xs @ zs) (ys @ zs) \<longleftrightarrow> sub xs ys" (is "?l = ?r")
+lemma sublisteq_append [simp]:
+  "sublisteq (xs @ zs) (ys @ zs) \<longleftrightarrow> sublisteq xs ys" (is "?l = ?r")
 proof
-  { fix xs' ys' xs ys zs :: "'a list" assume "sub xs' ys'"
-    then have "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> sub xs ys"
+  { fix xs' ys' xs ys zs :: "'a list" assume "sublisteq xs' ys'"
+    then have "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> sublisteq xs ys"
     proof (induct arbitrary: xs ys zs)
-      case emb_Nil show ?case by simp
+      case list_hembeq_Nil show ?case by simp
     next
-      case (emb_Cons xs' ys' x)
-      { assume "ys=[]" then have ?case using emb_Cons(1) by auto }
+      case (list_hembeq_Cons xs' ys' x)
+      { assume "ys=[]" then have ?case using list_hembeq_Cons(1) by auto }
       moreover
       { fix us assume "ys = x#us"
-        then have ?case using emb_Cons(2) by(simp add: emb.emb_Cons) }
+        then have ?case using list_hembeq_Cons(2) by(simp add: list_hembeq.list_hembeq_Cons) }
       ultimately show ?case by (auto simp:Cons_eq_append_conv)
     next
-      case (emb_Cons2 x y xs' ys')
-      { assume "xs=[]" then have ?case using emb_Cons2(1) by auto }
+      case (list_hembeq_Cons2 x y xs' ys')
+      { assume "xs=[]" then have ?case using list_hembeq_Cons2(1) by auto }
       moreover
-      { fix us vs assume "xs=x#us" "ys=x#vs" then have ?case using emb_Cons2 by auto}
+      { fix us vs assume "xs=x#us" "ys=x#vs" then have ?case using list_hembeq_Cons2 by auto}
       moreover
-      { fix us assume "xs=x#us" "ys=[]" then have ?case using emb_Cons2(2) by bestsimp }
-      ultimately show ?case using `x = y` by (auto simp: Cons_eq_append_conv)
+      { fix us assume "xs=x#us" "ys=[]" then have ?case using list_hembeq_Cons2(2) by bestsimp }
+      ultimately show ?case using `op =\<^sup>=\<^sup>= x y` by (auto simp: Cons_eq_append_conv)
     qed }
   moreover assume ?l
   ultimately show ?r by blast
 next
-  assume ?r then show ?l by (metis emb_append_mono sub_refl)
+  assume ?r then show ?l by (metis list_hembeq_append_mono sublisteq_refl)
 qed
 
-lemma sub_drop_many: "sub xs ys \<Longrightarrow> sub xs (zs @ ys)"
+lemma sublisteq_drop_many: "sublisteq xs ys \<Longrightarrow> sublisteq xs (zs @ ys)"
   by (induct zs) auto
 
-lemma sub_rev_drop_many: "sub xs ys \<Longrightarrow> sub xs (ys @ zs)"
-  by (metis append_Nil2 emb_Nil emb_append_mono)
+lemma sublisteq_rev_drop_many: "sublisteq xs ys \<Longrightarrow> sublisteq xs (ys @ zs)"
+  by (metis append_Nil2 list_hembeq_Nil list_hembeq_append_mono)
 
 
 subsection {* Relation to standard list operations *}
 
-lemma sub_map:
-  assumes "sub xs ys" shows "sub (map f xs) (map f ys)"
+lemma sublisteq_map:
+  assumes "sublisteq xs ys" shows "sublisteq (map f xs) (map f ys)"
   using assms by (induct) auto
 
-lemma sub_filter_left [simp]: "sub (filter P xs) xs"
+lemma sublisteq_filter_left [simp]: "sublisteq (filter P xs) xs"
   by (induct xs) auto
 
-lemma sub_filter [simp]:
-  assumes "sub xs ys" shows "sub (filter P xs) (filter P ys)"
+lemma sublisteq_filter [simp]:
+  assumes "sublisteq xs ys" shows "sublisteq (filter P xs) (filter P ys)"
   using assms by (induct) auto
 
-lemma "sub xs ys \<longleftrightarrow> (\<exists>N. xs = sublist ys N)" (is "?L = ?R")
+lemma "sublisteq xs ys \<longleftrightarrow> (\<exists>N. xs = sublist ys N)" (is "?L = ?R")
 proof
   assume ?L
   then show ?R
   proof (induct)
-    case emb_Nil show ?case by (metis sublist_empty)
+    case list_hembeq_Nil show ?case by (metis sublist_empty)
   next
-    case (emb_Cons xs ys x)
+    case (list_hembeq_Cons xs ys x)
     then obtain N where "xs = sublist ys N" by blast
     then have "xs = sublist (x#ys) (Suc ` N)"
       by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
     then show ?case by blast
   next
-    case (emb_Cons2 x y xs ys)
+    case (list_hembeq_Cons2 x y xs ys)
     then obtain N where "xs = sublist ys N" by blast
     then have "x#xs = sublist (x#ys) (insert 0 (Suc ` N))"
       by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
-    then show ?case unfolding `x = y` by blast
+    moreover from list_hembeq_Cons2 have "x = y" by simp
+    ultimately show ?case by blast
   qed
 next
   assume ?R
   then obtain N where "xs = sublist ys N" ..
-  moreover have "sub (sublist ys N) ys"
+  moreover have "sublisteq (sublist ys N) ys"
   proof (induct ys arbitrary: N)
     case Nil show ?case by simp
   next
diff -r 4a389d115b4f -r bd145273e7c6 src/HOL/Library/Sublist_Order.thy
--- a/src/HOL/Library/Sublist_Order.thy	Fri Dec 14 12:18:51 2012 +0100
+++ b/src/HOL/Library/Sublist_Order.thy	Fri Dec 14 12:40:07 2012 +0100
@@ -21,7 +21,7 @@
 begin
 
 definition
-  "(xs :: 'a list) \<le> ys \<longleftrightarrow> sub xs ys"
+  "(xs :: 'a list) \<le> ys \<longleftrightarrow> sublisteq xs ys"
 
 definition
   "(xs :: 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
@@ -40,41 +40,41 @@
 next
   fix xs ys :: "'a list"
   assume "xs <= ys" and "ys <= xs"
-  thus "xs = ys" by (unfold less_eq_list_def) (rule sub_antisym)
+  thus "xs = ys" by (unfold less_eq_list_def) (rule sublisteq_antisym)
 next
   fix xs ys zs :: "'a list"
   assume "xs <= ys" and "ys <= zs"
-  thus "xs <= zs" by (unfold less_eq_list_def) (rule sub_trans)
+  thus "xs <= zs" by (unfold less_eq_list_def) (rule sublisteq_trans)
 qed
 
 lemmas less_eq_list_induct [consumes 1, case_names empty drop take] =
-  emb.induct [of "op =", folded less_eq_list_def]
-lemmas less_eq_list_drop = emb.emb_Cons [of "op =", folded less_eq_list_def]
-lemmas le_list_Cons2_iff [simp, code] = sub_Cons2_iff [folded less_eq_list_def]
-lemmas le_list_map = sub_map [folded less_eq_list_def]
-lemmas le_list_filter = sub_filter [folded less_eq_list_def]
-lemmas le_list_length = emb_length [of "op =", folded less_eq_list_def]
+  list_hembeq.induct [of "op =", folded less_eq_list_def]
+lemmas less_eq_list_drop = list_hembeq.list_hembeq_Cons [of "op =", folded less_eq_list_def]
+lemmas le_list_Cons2_iff [simp, code] = sublisteq_Cons2_iff [folded less_eq_list_def]
+lemmas le_list_map = sublisteq_map [folded less_eq_list_def]
+lemmas le_list_filter = sublisteq_filter [folded less_eq_list_def]
+lemmas le_list_length = list_hembeq_length [of "op =", folded less_eq_list_def]
 
 lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys"
-  by (metis emb_length sub_same_length le_neq_implies_less less_list_def less_eq_list_def)
+  by (metis list_hembeq_length sublisteq_same_length le_neq_implies_less less_list_def less_eq_list_def)
 
 lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []"
-  by (metis less_eq_list_def emb_Nil order_less_le)
+  by (metis less_eq_list_def list_hembeq_Nil order_less_le)
 
 lemma less_list_below_empty [simp]: "xs < [] \<longleftrightarrow> False"
-  by (metis emb_Nil less_eq_list_def less_list_def)
+  by (metis list_hembeq_Nil less_eq_list_def less_list_def)
 
 lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys"
   by (unfold less_le less_eq_list_def) (auto)
 
 lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys"
-  by (metis sub_Cons2_iff less_list_def less_eq_list_def)
+  by (metis sublisteq_Cons2_iff less_list_def less_eq_list_def)
 
 lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys"
-  by (metis sub_append_le_same_iff sub_drop_many order_less_le self_append_conv2 less_eq_list_def)
+  by (metis sublisteq_append_le_same_iff sublisteq_drop_many order_less_le self_append_conv2 less_eq_list_def)
 
 lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys"
-  by (metis less_list_def less_eq_list_def sub_append')
+  by (metis less_list_def less_eq_list_def sublisteq_append')
 
 lemma less_list_rev_take: "xs @ zs < ys @ zs \<longleftrightarrow> xs < ys"
   by (unfold less_le less_eq_list_def) auto
diff -r 4a389d115b4f -r bd145273e7c6 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Fri Dec 14 12:18:51 2012 +0100
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Fri Dec 14 12:40:07 2012 +0100
@@ -1217,10 +1217,10 @@
   shows "reduced label n x = r" apply(rule le_antisym) apply(rule_tac[!] ccontr) unfolding not_le
   using reduced_labelling[of label n x] using assms by auto
 
-lemma reduced_labelling_0: assumes "j\<in>{1..n}" "label x j = 0" shows "reduced label n x \<noteq> j - 1"
+lemma reduced_labelling_zero: assumes "j\<in>{1..n}" "label x j = 0" shows "reduced label n x \<noteq> j - 1"
   using reduced_labelling[of label n x] using assms by fastforce 
 
-lemma reduced_labelling_1: assumes "j\<in>{1..n}" "label x j \<noteq> 0" shows "reduced label n x < j"
+lemma reduced_labelling_nonzero: assumes "j\<in>{1..n}" "label x j \<noteq> 0" shows "reduced label n x < j"
   using assms and reduced_labelling[of label n x] apply(erule_tac x=j in allE) by auto
 
 lemma reduced_labelling_Suc:
@@ -1235,13 +1235,13 @@
   ((reduced lab (n + 1)) ` f = {0..n}) \<and> (\<forall>x\<in>f. x (n + 1) = p)" (is "?l = ?r") proof
   assume ?l (is "?as \<and> (?a \<or> ?b)") thus ?r apply-apply(rule,erule conjE,assumption) proof(cases ?a)
     case True then guess j .. note j=this {fix x assume x:"x\<in>f"
-      have "reduced lab (n+1) x \<noteq> j - 1" using j apply-apply(rule reduced_labelling_0) defer apply(rule assms(1)[rule_format]) using x by auto }
+      have "reduced lab (n+1) x \<noteq> j - 1" using j apply-apply(rule reduced_labelling_zero) defer apply(rule assms(1)[rule_format]) using x by auto }
     moreover have "j - 1 \<in> {0..n}" using j by auto
     then guess y unfolding `?l`[THEN conjunct1,THEN sym] and image_iff .. note y = this
     ultimately have False by auto thus "\<forall>x\<in>f. x (n + 1) = p" by auto next
 
     case False hence ?b using `?l` by blast then guess j .. note j=this {fix x assume x:"x\<in>f"
-      have "reduced lab (n+1) x < j" using j apply-apply(rule reduced_labelling_1) using assms(2)[rule_format,of x j] and x by auto } note * = this
+      have "reduced lab (n+1) x < j" using j apply-apply(rule reduced_labelling_nonzero) using assms(2)[rule_format,of x j] and x by auto } note * = this
     have "j = n + 1" proof(rule ccontr) case goal1 hence "j < n + 1" using j by auto moreover
       have "n \<in> {0..n}" by auto then guess y unfolding `?l`[THEN conjunct1,THEN sym] image_iff ..
       ultimately show False using *[of y] by auto qed
@@ -1261,7 +1261,7 @@
     have *:"\<forall>x\<in>f. \<forall>j\<in>{1..n + 1}. x j = 0 \<longrightarrow> lab x j = 0" "\<forall>x\<in>f. \<forall>j\<in>{1..n + 1}. x j = p \<longrightarrow> lab x j = 1"
       using assms(2-3) using as(1)[unfolded ksimplex_def] by auto
     have allp:"\<forall>x\<in>f. x (n + 1) = p" using assms(2) using as(1)[unfolded ksimplex_def] by auto
-    { fix x assume "x\<in>f" hence "reduced lab (n + 1) x < n + 1" apply-apply(rule reduced_labelling_1)
+    { fix x assume "x\<in>f" hence "reduced lab (n + 1) x < n + 1" apply-apply(rule reduced_labelling_nonzero)
         defer using assms(3) using as(1)[unfolded ksimplex_def] by auto
       hence "reduced lab (n + 1) x = reduced lab n x" apply-apply(rule reduced_labelling_Suc) using reduced_labelling(1) by auto }
     hence "reduced lab (n + 1) ` f = {0..n}" unfolding as(2)[THEN sym] apply- apply(rule set_eqI) unfolding image_iff by auto
@@ -1278,14 +1278,14 @@
         using reduced_labelling(1) by auto }
     thus part1:"reduced lab n ` f = {0..n}" unfolding sa(4)[THEN sym] apply-apply(rule set_eqI) unfolding image_iff by auto
     have *:"\<forall>x\<in>f. x (n + 1) = p" proof(cases "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0")
-      case True then guess j .. hence "\<And>x. x\<in>f \<Longrightarrow> reduced lab (n + 1) x \<noteq> j - 1" apply-apply(rule reduced_labelling_0) apply assumption
+      case True then guess j .. hence "\<And>x. x\<in>f \<Longrightarrow> reduced lab (n + 1) x \<noteq> j - 1" apply-apply(rule reduced_labelling_zero) apply assumption
         apply(rule assms(2)[rule_format]) using sa(1)[unfolded ksimplex_def] unfolding sa by auto moreover
       have "j - 1 \<in> {0..n}" using `j\<in>{1..n+1}` by auto
       ultimately have False unfolding sa(4)[THEN sym] unfolding image_iff by fastforce thus ?thesis by auto next
       case False hence "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p" using sa(5) by fastforce then guess j .. note j=this
       thus ?thesis proof(cases "j = n+1")
         case False hence *:"j\<in>{1..n}" using j by auto
-        hence "\<And>x. x\<in>f \<Longrightarrow> reduced lab n x < j" apply(rule reduced_labelling_1) proof- fix x assume "x\<in>f"
+        hence "\<And>x. x\<in>f \<Longrightarrow> reduced lab n x < j" apply(rule reduced_labelling_nonzero) proof- fix x assume "x\<in>f"
           hence "lab x j = 1" apply-apply(rule assms(3)[rule_format,OF j(1)]) 
             using sa(1)[unfolded ksimplex_def] using j unfolding sa by auto thus "lab x j \<noteq> 0" by auto qed
         moreover have "j\<in>{0..n}" using * by auto
@@ -1306,7 +1306,7 @@
   have "a = (\<lambda>x. p)" using ksimplexD(5)[OF l, rule_format, OF a(1)] by(rule,auto) thus ?r using a by auto next
   assume r:?r show ?l unfolding r ksimplex_eq by auto qed
 
-lemma reduce_labelling_0[simp]: "reduced lab 0 x = 0" apply(rule reduced_labelling_unique) by auto
+lemma reduce_labelling_zero[simp]: "reduced lab 0 x = 0" apply(rule reduced_labelling_unique) by auto
 
 lemma kuhn_combinatorial:
   assumes "0 < p" "\<forall>x j. (\<forall>j. x(j) \<le> p) \<and> 1 \<le> j \<and> j \<le> n \<and> (x j = 0) \<longrightarrow> (lab x j = 0)"
diff -r 4a389d115b4f -r bd145273e7c6 src/HOL/ROOT
--- a/src/HOL/ROOT	Fri Dec 14 12:18:51 2012 +0100
+++ b/src/HOL/ROOT	Fri Dec 14 12:40:07 2012 +0100
@@ -633,7 +633,7 @@
     TreeFsetI
     "Derivation_Trees/Gram_Lang"
     "Derivation_Trees/Parallel"
-    Stream
+    Koenig
   theories [condition = ISABELLE_FULL_TEST]
     Misc_Codata
     Misc_Data
diff -r 4a389d115b4f -r bd145273e7c6 src/HOL/TPTP/MaSh_Eval.thy
--- a/src/HOL/TPTP/MaSh_Eval.thy	Fri Dec 14 12:18:51 2012 +0100
+++ b/src/HOL/TPTP/MaSh_Eval.thy	Fri Dec 14 12:40:07 2012 +0100
@@ -11,7 +11,7 @@
 ML_file "mash_eval.ML"
 
 sledgehammer_params
-  [provers = spass, max_relevant = 32, strict, dont_slice, type_enc = mono_native,
+  [provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native,
    lam_trans = combs_and_lifting, timeout = 15, dont_preplay, minimize]
 
 declare [[sledgehammer_instantiate_inducts]]
@@ -27,7 +27,9 @@
 ML {*
 val do_it = false (* switch to "true" to generate the files *)
 val params = Sledgehammer_Isar.default_params @{context} []
-val prob_dir = "/tmp/mash_problems"
+val dir = "List"
+val prefix = "/tmp/" ^ dir ^ "/"
+val prob_dir = prefix ^ "mash_problems"
 *}
 
 ML {*
@@ -40,7 +42,7 @@
 ML {*
 if do_it then
   evaluate_mash_suggestions @{context} params (SOME prob_dir)
-      "/tmp/mash_suggestions" "/tmp/mash_eval.out"
+      (prefix ^ "mash_suggestions") (prefix ^ "mash_eval")
 else
   ()
 *}
diff -r 4a389d115b4f -r bd145273e7c6 src/HOL/TPTP/MaSh_Export.thy
--- a/src/HOL/TPTP/MaSh_Export.thy	Fri Dec 14 12:18:51 2012 +0100
+++ b/src/HOL/TPTP/MaSh_Export.thy	Fri Dec 14 12:40:07 2012 +0100
@@ -11,12 +11,16 @@
 ML_file "mash_export.ML"
 
 sledgehammer_params
-  [provers = spass, max_relevant = 32, strict, dont_slice, type_enc = mono_native,
+  [provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native,
    lam_trans = combs_and_lifting, timeout = 2, dont_preplay, minimize]
 
 declare [[sledgehammer_instantiate_inducts]]
 
 ML {*
+!Multithreading.max_threads
+*}
+
+ML {*
 open MaSh_Export
 *}
 
@@ -25,7 +29,7 @@
 val thys = [@{theory List}]
 val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} []
 val prover = hd provers
-val dir = space_implode "__" (map Context.theory_name thys)
+val dir = "List"
 val prefix = "/tmp/" ^ dir ^ "/"
 *}
 
diff -r 4a389d115b4f -r bd145273e7c6 src/HOL/TPTP/atp_theory_export.ML
--- a/src/HOL/TPTP/atp_theory_export.ML	Fri Dec 14 12:18:51 2012 +0100
+++ b/src/HOL/TPTP/atp_theory_export.ML	Fri Dec 14 12:40:07 2012 +0100
@@ -34,8 +34,8 @@
 fun inference infers ident =
   these (AList.lookup (op =) infers ident) |> inference_term
 fun add_inferences_to_problem_line infers
-                                   (Formula (ident, Axiom, phi, NONE, tms)) =
-    Formula (ident, Lemma, phi, inference infers ident, tms)
+        (Formula ((ident, alt), Axiom, phi, NONE, tms)) =
+    Formula ((ident, alt), Lemma, phi, inference infers ident, tms)
   | add_inferences_to_problem_line _ line = line
 fun add_inferences_to_problem infers =
   map (apsnd (map (add_inferences_to_problem_line infers)))
@@ -44,7 +44,7 @@
   | ident_of_problem_line (Type_Decl (ident, _, _)) = ident
   | ident_of_problem_line (Sym_Decl (ident, _, _)) = ident
   | ident_of_problem_line (Class_Memb (ident, _, _, _)) = ident
-  | ident_of_problem_line (Formula (ident, _, _, _, _)) = ident
+  | ident_of_problem_line (Formula ((ident, _), _, _, _, _)) = ident
 
 fun atp_for_format (THF (Polymorphic, _, _, _)) = dummy_thfN
   | atp_for_format (THF (Monomorphic, _, _, _)) = satallaxN
@@ -83,11 +83,12 @@
   [@{theory HOL}, @{theory Meson}, @{theory ATP}, @{theory Metis}]
   |> map (fact_name_of o Context.theory_name)
 
-fun is_problem_line_tautology ctxt format (Formula (ident, _, phi, _, _)) =
+fun is_problem_line_tautology ctxt format
+                              (Formula ((ident, alt), _, phi, _, _)) =
     exists (fn prefix => String.isPrefix prefix ident)
            tautology_prefixes andalso
     is_none (run_some_atp ctxt format
-                 [(factsN, [Formula (ident, Conjecture, phi, NONE, [])])])
+        [(factsN, [Formula ((ident, alt), Conjecture, phi, NONE, [])])])
   | is_problem_line_tautology _ _ _ = false
 
 fun order_facts ord = sort (ord o pairself ident_of_problem_line)
diff -r 4a389d115b4f -r bd145273e7c6 src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Fri Dec 14 12:18:51 2012 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Fri Dec 14 12:40:07 2012 +0100
@@ -97,11 +97,13 @@
           | set_file_name _ NONE = I
         fun prove ok heading get facts =
           let
+            fun nickify ((_, stature), th) = ((K (nickname_of th), stature), th)
             val facts =
-              facts |> map get
-                    |> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts
-                                                                   concl_t
-                    |> take (the max_facts)
+              facts
+              |> map get
+              |> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t
+              |> take (the max_facts)
+              |> map nickify
             val ctxt = ctxt |> set_file_name heading prob_dir_name
             val res as {outcome, ...} =
               run_prover_for_mash ctxt params prover facts goal
diff -r 4a389d115b4f -r bd145273e7c6 src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Fri Dec 14 12:18:51 2012 +0100
+++ b/src/HOL/TPTP/mash_export.ML	Fri Dec 14 12:40:07 2012 +0100
@@ -97,18 +97,21 @@
       in File.append path s end
   in List.app do_fact facts end
 
-fun isar_or_prover_dependencies_of ctxt params_opt facts all_names th =
+fun isar_or_prover_dependencies_of ctxt params_opt facts all_names th
+                                   isar_deps_opt =
   (case params_opt of
      SOME (params as {provers = prover :: _, ...}) =>
      prover_dependencies_of ctxt params prover 0 facts all_names th |> snd
-   | NONE => isar_dependencies_of all_names th)
+   | NONE =>
+     case isar_deps_opt of
+       SOME deps => deps
+     | NONE => isar_dependencies_of all_names th)
   |> these
 
 fun generate_isar_or_prover_dependencies ctxt params_opt thys include_thys
                                          file_name =
   let
     val path = file_name |> Path.explode
-    val _ = File.write path ""
     val facts =
       all_facts ctxt |> not include_thys ? filter_out (has_thys thys o snd)
     val all_names = build_all_names nickname_of facts
@@ -116,10 +119,10 @@
       let
         val name = nickname_of th
         val deps =
-          isar_or_prover_dependencies_of ctxt params_opt facts all_names th
-        val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
-      in File.append path s end
-  in List.app do_fact facts end
+          isar_or_prover_dependencies_of ctxt params_opt facts all_names th NONE
+      in escape_meta name ^ ": " ^ escape_metas deps ^ "\n" end
+    val lines = Par_List.map do_fact facts
+  in File.write_list path lines end
 
 fun generate_isar_dependencies ctxt =
   generate_isar_or_prover_dependencies ctxt NONE
@@ -127,32 +130,39 @@
 fun generate_prover_dependencies ctxt params =
   generate_isar_or_prover_dependencies ctxt (SOME params)
 
+fun is_bad_query ctxt ho_atp th isar_deps =
+  Thm.legacy_get_kind th = "" orelse null isar_deps orelse
+  is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th)
+
 fun generate_isar_or_prover_commands ctxt prover params_opt thys file_name =
   let
+    val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
     val path = file_name |> Path.explode
-    val _ = File.write path ""
     val facts = all_facts ctxt
     val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
     val all_names = build_all_names nickname_of facts
-    fun do_fact ((_, stature), th) prevs =
+    fun do_fact ((name, ((_, stature), th)), prevs) =
       let
-        val name = nickname_of th
         val feats =
           features_of ctxt prover (theory_of_thm th) stature [prop_of th]
+        val isar_deps = isar_dependencies_of all_names th
         val deps =
           isar_or_prover_dependencies_of ctxt params_opt facts all_names th
-        val kind = Thm.legacy_get_kind th
+                                         (SOME isar_deps)
         val core =
           escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^
           encode_features feats
         val query =
-          if kind = "" orelse null deps then "" else "? " ^ core ^ "\n"
+          if is_bad_query ctxt ho_atp th (these isar_deps) then ""
+          else "? " ^ core ^ "\n"
         val update = "! " ^ core ^ "; " ^ escape_metas deps ^ "\n"
-        val _ = File.append path (query ^ update)
-      in [name] end
+      in query ^ update end
     val thy_map = old_facts |> thy_map_from_facts
     val parents = fold (add_thy_parent_facts thy_map) thys []
-  in fold do_fact new_facts parents; () end
+    val new_facts = new_facts |> map (`(nickname_of o snd))
+    val prevss = fst (split_last (parents :: map (single o fst) new_facts))
+    val lines = Par_List.map do_fact (new_facts ~~ prevss)
+  in File.write_list path lines end
 
 fun generate_isar_commands ctxt prover =
   generate_isar_or_prover_commands ctxt prover NONE
@@ -160,33 +170,35 @@
 fun generate_prover_commands ctxt (params as {provers = prover :: _, ...}) =
   generate_isar_or_prover_commands ctxt prover (SOME params)
 
-fun generate_mepo_suggestions ctxt (params as {provers, ...}) thys max_relevant
-                              file_name =
+fun generate_mepo_suggestions ctxt (params as {provers = prover :: _, ...}) thys
+                              max_facts file_name =
   let
+    val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
     val path = file_name |> Path.explode
-    val _ = File.write path ""
-    val prover = hd provers
     val facts = all_facts ctxt
     val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
-    fun do_fact (fact as (_, th)) old_facts =
+    val all_names = build_all_names nickname_of facts
+    fun do_fact ((_, th), old_facts) =
       let
         val name = nickname_of th
         val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
         val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
-        val kind = Thm.legacy_get_kind th
-        val _ =
-          if kind <> "" then
-            let
-              val suggs =
-                old_facts
-                |> Sledgehammer_MePo.mepo_suggested_facts ctxt params prover
-                       max_relevant NONE hyp_ts concl_t
-                |> map (nickname_of o snd)
-              val s = escape_meta name ^ ": " ^ escape_metas suggs ^ "\n"
-            in File.append path s end
-          else
-            ()
-      in fact :: old_facts end
-  in fold do_fact new_facts old_facts; () end
+        val isar_deps = isar_dependencies_of all_names th
+      in
+        if is_bad_query ctxt ho_atp th (these isar_deps) then
+          ""
+        else
+          let
+            val suggs =
+              old_facts
+              |> Sledgehammer_MePo.mepo_suggested_facts ctxt params prover
+                     max_facts NONE hyp_ts concl_t
+              |> map (nickname_of o snd)
+          in escape_meta name ^ ": " ^ escape_metas suggs ^ "\n" end
+      end
+    fun accum x (yss as ys :: _) = (x :: ys) :: yss
+    val old_factss = tl (fold accum new_facts [old_facts])
+    val lines = Par_List.map do_fact (new_facts ~~ rev old_factss)
+  in File.write_list path lines end
 
 end;
diff -r 4a389d115b4f -r bd145273e7c6 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Fri Dec 14 12:18:51 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Fri Dec 14 12:40:07 2012 +0100
@@ -51,7 +51,7 @@
     Type_Decl of string * 'a * int |
     Sym_Decl of string * 'a * 'a ho_type |
     Class_Memb of string * ('a * 'a list) list * 'a ho_type * 'a |
-    Formula of string * formula_role
+    Formula of (string * string) * formula_role
                * ('a, 'a ho_type, ('a, 'a ho_type) ho_term, 'a) formula
                * (string, string ho_type) ho_term option
                * (string, string ho_type) ho_term list
@@ -190,7 +190,7 @@
   Type_Decl of string * 'a * int |
   Sym_Decl of string * 'a * 'a ho_type |
   Class_Memb of string * ('a * 'a list) list * 'a ho_type * 'a |
-  Formula of string * formula_role
+  Formula of (string * string) * formula_role
              * ('a, 'a ho_type, ('a, 'a ho_type) ho_term, 'a) formula
              * (string, string ho_type) ho_term option
              * (string, string ho_type) ho_term list
@@ -479,15 +479,18 @@
 
 fun nary_type_decl_type n = funpow n (curry AFun atype_of_types) atype_of_types
 
+fun maybe_alt "" = ""
+  | maybe_alt s = " % " ^ s
+
 fun tptp_string_for_line format (Type_Decl (ident, ty, ary)) =
     tptp_string_for_line format (Sym_Decl (ident, ty, nary_type_decl_type ary))
   | tptp_string_for_line format (Sym_Decl (ident, sym, ty)) =
     tptp_string_for_format format ^ "(" ^ ident ^ ", type,\n    " ^ sym ^
     " : " ^ string_for_type format ty ^ ").\n"
-  | tptp_string_for_line format (Formula (ident, kind, phi, source, _)) =
+  | tptp_string_for_line format (Formula ((ident, alt), kind, phi, source, _)) =
     tptp_string_for_format format ^ "(" ^ ident ^ ", " ^
-    tptp_string_for_role kind ^ ",\n    (" ^
-    tptp_string_for_formula format phi ^ ")" ^
+    tptp_string_for_role kind ^ "," ^ maybe_alt alt ^
+    "\n    (" ^ tptp_string_for_formula format phi ^ ")" ^
     (case source of
        SOME tm => ", " ^ tptp_string_for_term format tm
      | NONE => "") ^ ").\n"
@@ -582,13 +585,14 @@
        else "[" ^ commas (map str_for_bound_tvar xs) ^ "], ") ^
       str_for_typ ty ^ ", " ^ cl ^ ")."
     fun subclass_of sub super = "subclass(" ^ sub ^ ", " ^ super ^ ")."
-    fun formula pred (Formula (ident, kind, phi, _, info)) =
+    fun formula pred (Formula ((ident, alt), kind, phi, _, info)) =
         if pred kind then
           let val rank = extract_isabelle_rank info in
             "formula(" ^ dfg_string_for_formula poly gen_simp info phi ^
             ", " ^ ident ^
             (if rank = default_rank then "" else ", " ^ string_of_int rank) ^
-            ")." |> SOME
+            ")." ^ maybe_alt alt
+            |> SOME
           end
         else
           NONE
@@ -725,13 +729,13 @@
     clausify_formula true (AConn (AImplies, rev phis))
   | clausify_formula _ _ = raise CLAUSIFY ()
 
-fun clausify_formula_line (Formula (ident, kind, phi, source, info)) =
+fun clausify_formula_line (Formula ((ident, alt), kind, phi, source, info)) =
     let
       val (n, phis) = phi |> try (clausify_formula true) |> these |> `length
     in
       map2 (fn phi => fn j =>
-               Formula (ident ^ replicate_string (j - 1) "x", kind, phi, source,
-                        info))
+               Formula ((ident ^ replicate_string (j - 1) "x", alt), kind, phi,
+                        source, info))
            phis (1 upto n)
     end
   | clausify_formula_line _ = []
diff -r 4a389d115b4f -r bd145273e7c6 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Dec 14 12:18:51 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Dec 14 12:40:07 2012 +0100
@@ -2128,8 +2128,8 @@
    the remote provers might care. *)
 fun line_for_fact ctxt prefix encode freshen pos mono type_enc rank
         (j, {name, stature = (_, status), role, iformula, atomic_types}) =
-  Formula (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^
-           encode name,
+  Formula ((prefix ^ (if freshen then string_of_int j ^ "_" else "") ^
+            encode name, name),
            role,
            iformula
            |> formula_from_iformula ctxt mono type_enc
@@ -2139,7 +2139,7 @@
            NONE, isabelle_info (string_of_status status) (rank j))
 
 fun lines_for_subclass type_enc sub super =
-  Formula (subclass_prefix ^ ascii_of sub ^ "___" ^ ascii_of super, Axiom,
+  Formula ((subclass_prefix ^ ascii_of sub ^ "___" ^ ascii_of super, ""), Axiom,
            AConn (AImplies,
                   [sub, super] |> map (fn s => class_atom type_enc (s, tvar_a)))
            |> bound_tvars type_enc false [tvar_a],
@@ -2160,7 +2160,7 @@
                     prems,
                 native_ho_type_from_typ type_enc false 0 T, `make_class cl)
   else
-    Formula (tcon_clause_prefix ^ name, Axiom,
+    Formula ((tcon_clause_prefix ^ name, ""), Axiom,
              mk_ahorn (maps (class_atoms type_enc) prems)
                       (class_atom type_enc (cl, T))
              |> bound_tvars type_enc true (snd (dest_Type T)),
@@ -2168,7 +2168,7 @@
 
 fun line_for_conjecture ctxt mono type_enc
                         ({name, role, iformula, atomic_types, ...} : ifact) =
-  Formula (conjecture_prefix ^ name, role,
+  Formula ((conjecture_prefix ^ name, ""), role,
            iformula
            |> formula_from_iformula ctxt mono type_enc
                   should_guard_var_in_formula (SOME false)
@@ -2186,7 +2186,7 @@
                       native_ho_type_from_typ type_enc false 0 T,
                       `make_class cl)
         else
-          Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,
+          Formula ((tfree_clause_prefix ^ string_of_int j, ""), Hypothesis,
                    class_atom type_enc (cl, T), NONE, [])
       val membs =
         fold (union (op =)) (map #atomic_types facts) []
@@ -2347,8 +2347,7 @@
   end
 
 fun line_for_guards_mono_type ctxt mono type_enc T =
-  Formula (guards_sym_formula_prefix ^
-           ascii_of (mangled_type type_enc T),
+  Formula ((guards_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), ""),
            Axiom,
            IConst (`make_bound_var "X", T, [])
            |> type_guard_iterm type_enc T
@@ -2361,8 +2360,7 @@
 
 fun line_for_tags_mono_type ctxt mono type_enc T =
   let val x_var = ATerm ((`make_bound_var "X", []), []) in
-    Formula (tags_sym_formula_prefix ^
-             ascii_of (mangled_type type_enc T),
+    Formula ((tags_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), ""),
              Axiom,
              eq_formula type_enc (atomic_types_of T) [] false
                   (tag_with_type ctxt mono type_enc NONE T x_var) x_var,
@@ -2419,8 +2417,9 @@
         end
       | _ => replicate ary NONE
   in
-    Formula (guards_sym_formula_prefix ^ s ^
-             (if n > 1 then "_" ^ string_of_int j else ""), role,
+    Formula ((guards_sym_formula_prefix ^ s ^
+              (if n > 1 then "_" ^ string_of_int j else ""), ""),
+             role,
              IConst ((s, s'), T, T_args)
              |> fold (curry (IApp o swap)) bounds
              |> type_guard_iterm type_enc res_T
@@ -2449,8 +2448,8 @@
     val eq = maybe_negate oo eq_formula type_enc (atomic_types_of T) [] pred_sym
     val tag_with = tag_with_type ctxt mono type_enc NONE
     fun formula c =
-      [Formula (ident, role, eq (tag_with res_T c) c, NONE, isabelle_info
-                non_rec_defN helper_rank)]
+      [Formula ((ident, ""), role, eq (tag_with res_T c) c, NONE,
+                isabelle_info non_rec_defN helper_rank)]
   in
     if pred_sym orelse not (should_encode_type ctxt mono level res_T) then
       []
@@ -2549,8 +2548,9 @@
                      (ho_term_of tm1) (ho_term_of tm2)
       in
         ([tm1, tm2],
-         [Formula (uncurried_alias_eq_prefix ^ s2, role, eq |> maybe_negate,
-                   NONE, isabelle_info non_rec_defN helper_rank)])
+         [Formula ((uncurried_alias_eq_prefix ^ s2, ""), role,
+                   eq |> maybe_negate, NONE,
+                   isabelle_info non_rec_defN helper_rank)])
         |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I
             else pair_append (do_alias (ary - 1)))
       end
diff -r 4a389d115b4f -r bd145273e7c6 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Fri Dec 14 12:18:51 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Fri Dec 14 12:40:07 2012 +0100
@@ -364,7 +364,7 @@
   | is_same_formula _ subst (AAtom tm1) (AAtom tm2) = is_same_term subst tm1 tm2
   | is_same_formula _ _ _ _ = false
 
-fun matching_formula_line_identifier phi (Formula (ident, _, phi', _, _)) =
+fun matching_formula_line_identifier phi (Formula ((ident, _), _, phi', _, _)) =
     if is_same_formula true [] phi phi' then SOME (ident, phi') else NONE
   | matching_formula_line_identifier _ _ = NONE
 
diff -r 4a389d115b4f -r bd145273e7c6 src/HOL/Tools/Metis/metis_generate.ML
--- a/src/HOL/Tools/Metis/metis_generate.ML	Fri Dec 14 12:18:51 2012 +0100
+++ b/src/HOL/Tools/Metis/metis_generate.ML	Fri Dec 14 12:40:07 2012 +0100
@@ -161,7 +161,7 @@
 fun metis_literals_from_atp type_enc (AConn (AOr, phis)) =
     maps (metis_literals_from_atp type_enc) phis
   | metis_literals_from_atp type_enc phi = [metis_literal_from_atp type_enc phi]
-fun metis_axiom_from_atp type_enc clauses (Formula (ident, _, phi, _, _)) =
+fun metis_axiom_from_atp type_enc clauses (Formula ((ident, _), _, phi, _, _)) =
     let
       fun some isa =
         SOME (phi |> metis_literals_from_atp type_enc
diff -r 4a389d115b4f -r bd145273e7c6 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Dec 14 12:18:51 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Dec 14 12:40:07 2012 +0100
@@ -24,6 +24,7 @@
     Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
     -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
   val backquote_thm : Proof.context -> thm -> string
+  val is_blacklisted_or_something : Proof.context -> bool -> string -> bool
   val clasimpset_rule_table_of : Proof.context -> status Termtab.table
   val build_all_names :
     (thm -> string) -> ('a * thm) list -> string Symtab.table
@@ -173,15 +174,15 @@
     else
       term_has_too_many_lambdas max_lambda_nesting t
 
-(* The max apply depth of any "metis" call in "Metis_Examples" (on 2007-10-31)
-   was 11. *)
+(* The maximum apply depth of any "metis" call in "Metis_Examples" (on
+   2007-10-31) was 11. *)
 val max_apply_depth = 18
 
 fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
   | apply_depth (Abs (_, _, t)) = apply_depth t
   | apply_depth _ = 0
 
-fun is_formula_too_complex ho_atp t =
+fun is_too_complex ho_atp t =
   apply_depth t > max_apply_depth orelse
   (not ho_atp andalso formula_has_too_many_lambdas [] t)
 
@@ -208,7 +209,7 @@
   andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN
                            | _ => false) (prop_of th)
 
-fun is_likely_tautology_or_too_meta th =
+fun is_likely_tautology_too_meta_or_too_technical th =
   let
     fun is_interesting_subterm (Const (s, _)) =
         not (member (op =) atp_widely_irrelevant_consts s)
@@ -227,18 +228,18 @@
       | is_boring_prop _ (Const (@{const_name "=="}, _) $ t $ u) =
         is_boring_bool t andalso is_boring_bool u
       | is_boring_prop _ _ = true
+    val t = prop_of th
   in
-    is_boring_prop [] (prop_of th) andalso
-    not (Thm.eq_thm_prop (@{thm ext}, th))
-  end
-
-fun is_theorem_bad_for_atps ho_atp th =
-  let val t = prop_of th in
-    is_formula_too_complex ho_atp t orelse
+    (is_boring_prop [] (prop_of th) andalso
+     not (Thm.eq_thm_prop (@{thm ext}, th))) orelse
     exists_type type_has_top_sort t orelse exists_technical_const t orelse
     exists_low_level_class_const t orelse is_that_fact th
   end
 
+fun is_blacklisted_or_something ctxt ho_atp name =
+  (not (Config.get ctxt ignore_no_atp) andalso is_package_def name) orelse
+  exists (fn s => String.isSuffix s name) (multi_base_blacklist ctxt ho_atp)
+
 fun hackish_string_for_term ctxt =
   with_vanilla_print_mode (Syntax.string_of_term ctxt) #> simplify_spaces
 
@@ -402,7 +403,7 @@
 fun maybe_filter_no_atps ctxt =
   not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
 
-fun all_facts ctxt really_all ho_atp reserved add_ths chained css =
+fun all_facts ctxt generous ho_atp reserved add_ths chained css =
   let
     val thy = Proof_Context.theory_of ctxt
     val global_facts = Global_Theory.facts_of thy
@@ -419,15 +420,12 @@
       Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
     fun add_facts global foldx facts =
       foldx (fn (name0, ths) =>
-        if not really_all andalso
-           name0 <> "" andalso
+        if name0 <> "" andalso
            forall (not o member Thm.eq_thm_prop add_ths) ths andalso
            (Facts.is_concealed facts name0 orelse
             not (can (Proof_Context.get_thms ctxt) name0) orelse
-            (not (Config.get ctxt ignore_no_atp) andalso
-             is_package_def name0) orelse
-            exists (fn s => String.isSuffix s name0)
-                   (multi_base_blacklist ctxt ho_atp)) then
+            (not generous andalso
+             is_blacklisted_or_something ctxt ho_atp name0)) then
           I
         else
           let
@@ -442,9 +440,9 @@
             #> fold_rev (fn th => fn (j, (multis, unis)) =>
                    (j - 1,
                     if not (member Thm.eq_thm_prop add_ths th) andalso
-                       is_likely_tautology_or_too_meta th orelse
-                       (not really_all andalso
-                        is_theorem_bad_for_atps ho_atp th) then
+                       (is_likely_tautology_too_meta_or_too_technical th orelse
+                        (not generous andalso
+                         is_too_complex ho_atp (prop_of th))) then
                       (multis, unis)
                     else
                       let