added embedding for lists (constant emb)
authorChristian Sternagel
Wed Aug 29 10:48:28 2012 +0900 (2012-08-29)
changeset 49080f60ed8769a9d
parent 49079 919e393510f4
child 49081 092668a120cc
added embedding for lists (constant emb)
src/HOL/Library/Sublist.thy
     1.1 --- a/src/HOL/Library/Sublist.thy	Wed Aug 29 10:46:11 2012 +0900
     1.2 +++ b/src/HOL/Library/Sublist.thy	Wed Aug 29 10:48:28 2012 +0900
     1.3 @@ -379,4 +379,52 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 +
     1.8 +subsection {* Embedding on lists *}
     1.9 +
    1.10 +inductive
    1.11 +  emb :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    1.12 +  for P :: "('a \<Rightarrow> 'a \<Rightarrow> bool)"
    1.13 +where
    1.14 +  emb_Nil [intro, simp]: "emb P [] ys"
    1.15 +| emb_Cons [intro] : "emb P xs ys \<Longrightarrow> emb P xs (y#ys)"
    1.16 +| emb_Cons2 [intro]: "P x y \<Longrightarrow> emb P xs ys \<Longrightarrow> emb P (x#xs) (y#ys)"
    1.17 +
    1.18 +lemma emb_Nil2 [simp]:
    1.19 +  assumes "emb P xs []" shows "xs = []"
    1.20 +  using assms by (cases rule: emb.cases) auto
    1.21 +
    1.22 +lemma emb_append2 [intro]:
    1.23 +  "emb P xs ys \<Longrightarrow> emb P xs (zs @ ys)"
    1.24 +  by (induct zs) auto
    1.25 +
    1.26 +lemma emb_prefix [intro]:
    1.27 +  assumes "emb P xs ys" shows "emb P xs (ys @ zs)"
    1.28 +  using assms
    1.29 +  by (induct arbitrary: zs) auto
    1.30 +
    1.31 +lemma emb_ConsD:
    1.32 +  assumes "emb P (x#xs) ys"
    1.33 +  shows "\<exists>us v vs. ys = us @ v # vs \<and> P x v \<and> emb P xs vs"
    1.34 +using assms
    1.35 +proof (induct x\<equiv>"x#xs" y\<equiv>"ys" arbitrary: x xs ys)
    1.36 +  case emb_Cons thus ?case by (metis append_Cons)
    1.37 +next
    1.38 +  case (emb_Cons2 x y xs ys)
    1.39 +  thus ?case by (cases xs) (auto, blast+)
    1.40 +qed
    1.41 +
    1.42 +lemma emb_appendD:
    1.43 +  assumes "emb P (xs @ ys) zs"
    1.44 +  shows "\<exists>us vs. zs = us @ vs \<and> emb P xs us \<and> emb P ys vs"
    1.45 +using assms
    1.46 +proof (induction xs arbitrary: ys zs)
    1.47 +  case Nil thus ?case by auto
    1.48 +next
    1.49 +  case (Cons x xs)
    1.50 +  then obtain us v vs where "zs = us @ v # vs"
    1.51 +    and "P x v" and "emb P (xs @ ys) vs" by (auto dest: emb_ConsD)
    1.52 +  with Cons show ?case by (metis append_Cons append_assoc emb_Cons2 emb_append2)
    1.53 +qed
    1.54 +
    1.55  end