--- a/src/HOL/BNF/Equiv_Relations_More.thy Tue Nov 19 01:29:50 2013 +0100
+++ b/src/HOL/BNF/Equiv_Relations_More.thy Tue Nov 19 01:29:50 2013 +0100
@@ -59,7 +59,7 @@
lemma in_quotient_imp_in_rel:
"\<lbrakk>equiv A r; X \<in> A//r; {x,y} \<subseteq> X\<rbrakk> \<Longrightarrow> (x,y) \<in> r"
-using quotient_eq_iff by fastforce
+using quotient_eq_iff[THEN iffD1] by fastforce
lemma in_quotient_imp_closed:
"\<lbrakk>equiv A r; X \<in> A//r; x \<in> X; (x,y) \<in> r\<rbrakk> \<Longrightarrow> y \<in> X"
--- a/src/HOL/Library/Sublist.thy Tue Nov 19 01:29:50 2013 +0100
+++ b/src/HOL/Library/Sublist.thy Tue Nov 19 01:29:50 2013 +0100
@@ -107,16 +107,22 @@
lemma append_one_prefixeq:
"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')
+ proof (unfold prefixeq_def)
+ assume a1: "\<exists>zs. ys = xs @ zs"
+ then obtain sk :: "'a list" where sk: "ys = xs @ sk" by fastforce
+ assume a2: "length xs < length ys"
+ have f1: "\<And>v. ([]\<Colon>'a list) @ v = v" using append_Nil2 by simp
+ have "[] \<noteq> sk" using a1 a2 sk less_not_refl by force
+ hence "\<exists>v. xs @ hd sk # v = ys" using sk by (metis hd_Cons_tl)
+ thus "\<exists>zs. ys = (xs @ [ys ! length xs]) @ zs" using f1 by fastforce
+ qed
theorem prefixeq_length_le: "prefixeq xs ys \<Longrightarrow> length xs \<le> length ys"
by (auto simp add: prefixeq_def)
lemma prefixeq_same_cases:
"prefixeq (xs\<^sub>1::'a list) ys \<Longrightarrow> prefixeq xs\<^sub>2 ys \<Longrightarrow> prefixeq xs\<^sub>1 xs\<^sub>2 \<or> prefixeq xs\<^sub>2 xs\<^sub>1"
- unfolding prefixeq_def by (metis append_eq_append_conv2)
+ unfolding prefixeq_def by (force simp: append_eq_append_conv2)
lemma set_mono_prefixeq: "prefixeq xs ys \<Longrightarrow> set xs \<subseteq> set ys"
by (auto simp add: prefixeq_def)
@@ -224,9 +230,9 @@
then show ?thesis by (metis append_Nil2 parallelE prefixeqI snoc.prems ys)
next
fix c cs assume ys': "ys' = c # cs"
- then show ?thesis
- by (metis Cons_eq_appendI eq_Nil_appendI parallelE prefixeqI
- same_prefixeq_prefixeq snoc.prems ys)
+ have "x \<noteq> c" using snoc.prems ys ys' by fastforce
+ thus "\<exists>as b bs c cs. b \<noteq> c \<and> xs @ [x] = as @ b # bs \<and> ys = as @ c # cs"
+ using ys ys' by blast
qed
next
assume "prefix ys xs"
@@ -464,7 +470,7 @@
then show ?case by (metis append_Cons)
next
case (list_hembeq_Cons2 x y xs ys)
- then show ?case by (cases xs) (auto, blast+)
+ then show ?case by blast
qed
lemma list_hembeq_appendD:
@@ -475,9 +481,14 @@
case Nil then show ?case by auto
next
case (Cons x xs)
- then obtain us v vs where "zs = us @ v # vs"
- 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)
+ then obtain us v vs where
+ zs: "zs = us @ v # vs" and p: "P\<^sup>=\<^sup>= x v" and lh: "list_hembeq P (xs @ ys) vs"
+ by (auto dest: list_hembeq_ConsD)
+ obtain sk\<^sub>0 :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" and sk\<^sub>1 :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+ sk: "\<forall>x\<^sub>0 x\<^sub>1. \<not> list_hembeq P (xs @ x\<^sub>0) x\<^sub>1 \<or> sk\<^sub>0 x\<^sub>0 x\<^sub>1 @ sk\<^sub>1 x\<^sub>0 x\<^sub>1 = x\<^sub>1 \<and> list_hembeq P xs (sk\<^sub>0 x\<^sub>0 x\<^sub>1) \<and> list_hembeq P x\<^sub>0 (sk\<^sub>1 x\<^sub>0 x\<^sub>1)"
+ using Cons(1) by (metis (no_types))
+ hence "\<forall>x\<^sub>2. list_hembeq P (x # xs) (x\<^sub>2 @ v # sk\<^sub>0 ys vs)" using p lh by auto
+ thus ?case using lh zs sk by (metis (no_types) append_Cons append_assoc)
qed
lemma list_hembeq_suffix:
@@ -550,7 +561,7 @@
by (simp_all)
lemma sublisteq_Cons': "sublisteq (x#xs) ys \<Longrightarrow> sublisteq xs ys"
- by (induct xs) (auto dest: list_hembeq_ConsD)
+ by (induct xs, simp, blast dest: list_hembeq_ConsD)
lemma sublisteq_Cons2':
assumes "sublisteq (x#xs) (x#ys)" shows "sublisteq xs ys"
@@ -579,11 +590,11 @@
from list_hembeq_Nil2 [OF this] show ?case by simp
next
case list_hembeq_Cons2
- then show ?case by simp
+ thus ?case by simp
next
case list_hembeq_Cons
- then show ?case
- by (metis sublisteq_Cons' list_hembeq_length Suc_length_conv Suc_n_not_le_n)
+ hence False using sublisteq_Cons' by fastforce
+ thus ?case ..
qed
lemma sublisteq_trans: "sublisteq xs ys \<Longrightarrow> sublisteq ys zs \<Longrightarrow> sublisteq xs zs"
@@ -650,7 +661,7 @@
lemma sublisteq_filter [simp]:
assumes "sublisteq xs ys" shows "sublisteq (filter P xs) (filter P ys)"
- using assms by (induct) auto
+ using assms by induct auto
lemma "sublisteq xs ys \<longleftrightarrow> (\<exists>N. xs = sublist ys N)" (is "?L = ?R")
proof