Respectfullness and preservation of list_rel
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Thu Apr 15 16:55:12 2010 +0200 (2010-04-15)
changeset 3615411c6106d7787
parent 36147 b43b22f63665
child 36155 3a63df985e46
Respectfullness and preservation of list_rel
src/HOL/Library/Quotient_List.thy
src/HOL/List.thy
     1.1 --- a/src/HOL/Library/Quotient_List.thy	Thu Apr 15 12:27:14 2010 +0200
     1.2 +++ b/src/HOL/Library/Quotient_List.thy	Thu Apr 15 16:55:12 2010 +0200
     1.3 @@ -217,6 +217,52 @@
     1.4    apply (simp_all)
     1.5    done
     1.6  
     1.7 +lemma list_rel_rsp:
     1.8 +  assumes r: "\<forall>x y. R x y \<longrightarrow> (\<forall>a b. R a b \<longrightarrow> S x a = T y b)"
     1.9 +  and l1: "list_rel R x y"
    1.10 +  and l2: "list_rel R a b"
    1.11 +  shows "list_rel S x a = list_rel T y b"
    1.12 +  proof -
    1.13 +    have a: "length y = length x" by (rule list_rel_len[OF l1, symmetric])
    1.14 +    have c: "length a = length b" by (rule list_rel_len[OF l2])
    1.15 +    show ?thesis proof (cases "length x = length a")
    1.16 +      case True
    1.17 +      have b: "length x = length a" by fact
    1.18 +      show ?thesis using a b c r l1 l2 proof (induct rule: list_induct4)
    1.19 +        case Nil
    1.20 +        show ?case using assms by simp
    1.21 +      next
    1.22 +        case (Cons h t)
    1.23 +        then show ?case by auto
    1.24 +      qed
    1.25 +    next
    1.26 +      case False
    1.27 +      have d: "length x \<noteq> length a" by fact
    1.28 +      then have e: "\<not>list_rel S x a" using list_rel_len by auto
    1.29 +      have "length y \<noteq> length b" using d a c by simp
    1.30 +      then have "\<not>list_rel T y b" using list_rel_len by auto
    1.31 +      then show ?thesis using e by simp
    1.32 +    qed
    1.33 +  qed
    1.34 +
    1.35 +lemma[quot_respect]:
    1.36 +  "((R ===> R ===> op =) ===> list_rel R ===> list_rel R ===> op =) list_rel list_rel"
    1.37 +  by (simp add: list_rel_rsp)
    1.38 +
    1.39 +lemma[quot_preserve]:
    1.40 +  assumes a: "Quotient R abs1 rep1"
    1.41 +  shows "((abs1 ---> abs1 ---> id) ---> map rep1 ---> map rep1 ---> id) list_rel = list_rel"
    1.42 +  apply (simp add: expand_fun_eq)
    1.43 +  apply clarify
    1.44 +  apply (induct_tac xa xb rule: list_induct2')
    1.45 +  apply (simp_all add: Quotient_abs_rep[OF a])
    1.46 +  done
    1.47 +
    1.48 +lemma[quot_preserve]:
    1.49 +  assumes a: "Quotient R abs1 rep1"
    1.50 +  shows "(list_rel ((rep1 ---> rep1 ---> id) R) l m) = (l = m)"
    1.51 +  by (induct l m rule: list_induct2') (simp_all add: Quotient_rel_rep[OF a])
    1.52 +
    1.53  lemma list_rel_eq[id_simps]:
    1.54    shows "(list_rel (op =)) = (op =)"
    1.55    unfolding expand_fun_eq
     2.1 --- a/src/HOL/List.thy	Thu Apr 15 12:27:14 2010 +0200
     2.2 +++ b/src/HOL/List.thy	Thu Apr 15 16:55:12 2010 +0200
     2.3 @@ -513,6 +513,17 @@
     2.4      (cases zs, simp_all)
     2.5  qed
     2.6  
     2.7 +lemma list_induct4 [consumes 3, case_names Nil Cons]:
     2.8 +  "length xs = length ys \<Longrightarrow> length ys = length zs \<Longrightarrow> length zs = length ws \<Longrightarrow>
     2.9 +   P [] [] [] [] \<Longrightarrow> (\<And>x xs y ys z zs w ws. length xs = length ys \<Longrightarrow>
    2.10 +   length ys = length zs \<Longrightarrow> length zs = length ws \<Longrightarrow> P xs ys zs ws \<Longrightarrow>
    2.11 +   P (x#xs) (y#ys) (z#zs) (w#ws)) \<Longrightarrow> P xs ys zs ws"
    2.12 +proof (induct xs arbitrary: ys zs ws)
    2.13 +  case Nil then show ?case by simp
    2.14 +next
    2.15 +  case (Cons x xs ys zs ws) then show ?case by ((cases ys, simp_all), (cases zs,simp_all)) (cases ws, simp_all)
    2.16 +qed
    2.17 +
    2.18  lemma list_induct2': 
    2.19    "\<lbrakk> P [] [];
    2.20    \<And>x xs. P (x#xs) [];