no built-in reflexivity of list embedding (which is more standard; now embedding is reflexive whenever the base-order is)
authorChristian Sternagel
Thu Jul 03 09:55:15 2014 +0200 (2014-07-03)
changeset 57498ea44ec62a574
parent 57497 4106a2bc066a
child 57499 7e22776f2d32
no built-in reflexivity of list embedding (which is more standard; now embedding is reflexive whenever the base-order is)
src/HOL/Library/Sublist.thy
     1.1 --- a/src/HOL/Library/Sublist.thy	Thu Jul 03 09:55:15 2014 +0200
     1.2 +++ b/src/HOL/Library/Sublist.thy	Thu Jul 03 09:55:15 2014 +0200
     1.3 @@ -433,15 +433,16 @@
     1.4  where
     1.5    list_emb_Nil [intro, simp]: "list_emb P [] ys"
     1.6  | list_emb_Cons [intro] : "list_emb P xs ys \<Longrightarrow> list_emb P xs (y#ys)"
     1.7 -| list_emb_Cons2 [intro]: "P\<^sup>=\<^sup>= x y \<Longrightarrow> list_emb P xs ys \<Longrightarrow> list_emb P (x#xs) (y#ys)"
     1.8 +| list_emb_Cons2 [intro]: "P x y \<Longrightarrow> list_emb P xs ys \<Longrightarrow> list_emb P (x#xs) (y#ys)"
     1.9  
    1.10  lemma list_emb_Nil2 [simp]:
    1.11    assumes "list_emb P xs []" shows "xs = []"
    1.12    using assms by (cases rule: list_emb.cases) auto
    1.13  
    1.14 -lemma list_emb_refl [simp, intro!]:
    1.15 -  "list_emb P xs xs"
    1.16 -  by (induct xs) auto
    1.17 +lemma list_emb_refl:
    1.18 +  assumes "\<And>x. x \<in> set xs \<Longrightarrow> P x x"
    1.19 +  shows "list_emb P xs xs"
    1.20 +  using assms by (induct xs) auto
    1.21  
    1.22  lemma list_emb_Cons_Nil [simp]: "list_emb P (x#xs) [] = False"
    1.23  proof -
    1.24 @@ -463,7 +464,7 @@
    1.25  
    1.26  lemma list_emb_ConsD:
    1.27    assumes "list_emb P (x#xs) ys"
    1.28 -  shows "\<exists>us v vs. ys = us @ v # vs \<and> P\<^sup>=\<^sup>= x v \<and> list_emb P xs vs"
    1.29 +  shows "\<exists>us v vs. ys = us @ v # vs \<and> P x v \<and> list_emb P xs vs"
    1.30  using assms
    1.31  proof (induct x \<equiv> "x # xs" ys arbitrary: x xs)
    1.32    case list_emb_Cons
    1.33 @@ -482,7 +483,7 @@
    1.34  next
    1.35    case (Cons x xs)
    1.36    then obtain us v vs where
    1.37 -    zs: "zs = us @ v # vs" and p: "P\<^sup>=\<^sup>= x v" and lh: "list_emb P (xs @ ys) vs"
    1.38 +    zs: "zs = us @ v # vs" and p: "P x v" and lh: "list_emb P (xs @ ys) vs"
    1.39      by (auto dest: list_emb_ConsD)
    1.40    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
    1.41      sk: "\<forall>x\<^sub>0 x\<^sub>1. \<not> list_emb 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_emb P xs (sk\<^sub>0 x\<^sub>0 x\<^sub>1) \<and> list_emb P x\<^sub>0 (sk\<^sub>1 x\<^sub>0 x\<^sub>1)"
    1.42 @@ -518,21 +519,21 @@
    1.43    next
    1.44      case (list_emb_Cons xs ys y)
    1.45      from list_emb_ConsD [OF `list_emb P (y#ys) zs`] obtain us v vs
    1.46 -      where zs: "zs = us @ v # vs" and "P\<^sup>=\<^sup>= y v" and "list_emb P ys vs" by blast
    1.47 +      where zs: "zs = us @ v # vs" and "P y v" and "list_emb P ys vs" by blast
    1.48      then have "list_emb P ys (v#vs)" by blast
    1.49      then have "list_emb P ys zs" unfolding zs by (rule list_emb_append2)
    1.50      from list_emb_Cons.IH [OF this] and list_emb_Cons.prems show ?case by simp
    1.51    next
    1.52      case (list_emb_Cons2 x y xs ys)
    1.53      from list_emb_ConsD [OF `list_emb P (y#ys) zs`] obtain us v vs
    1.54 -      where zs: "zs = us @ v # vs" and "P\<^sup>=\<^sup>= y v" and "list_emb P ys vs" by blast
    1.55 +      where zs: "zs = us @ v # vs" and "P y v" and "list_emb P ys vs" by blast
    1.56      with list_emb_Cons2 have "list_emb P xs vs" by simp
    1.57 -    moreover have "P\<^sup>=\<^sup>= x v"
    1.58 +    moreover have "P x v"
    1.59      proof -
    1.60        from zs and `zs \<in> lists A` have "v \<in> A" by auto
    1.61        moreover have "x \<in> A" and "y \<in> A" using list_emb_Cons2 by simp_all
    1.62        ultimately show ?thesis
    1.63 -        using `P\<^sup>=\<^sup>= x y` and `P\<^sup>=\<^sup>= y v` and assms
    1.64 +        using `P x y` and `P y v` and assms
    1.65          by blast
    1.66      qed
    1.67      ultimately have "list_emb P (x#xs) (v#vs)" by blast
    1.68 @@ -635,7 +636,7 @@
    1.69        { fix us vs assume "xs=x#us" "ys=x#vs" then have ?case using list_emb_Cons2 by auto}
    1.70        moreover
    1.71        { fix us assume "xs=x#us" "ys=[]" then have ?case using list_emb_Cons2(2) by bestsimp }
    1.72 -      ultimately show ?case using `op =\<^sup>=\<^sup>= x y` by (auto simp: Cons_eq_append_conv)
    1.73 +      ultimately show ?case using `op = x y` by (auto simp: Cons_eq_append_conv)
    1.74      qed }
    1.75    moreover assume ?l
    1.76    ultimately show ?r by blast