164 lemma append_rsp_fst:

   164 lemma append_rsp_aux1:

   165   assumes a : "l1 \<approx> l2"

   165   assumes a : "l2 \<approx> r2 "

   166   shows "(l1 @ s) \<approx> (l2 @ s)"

   166   shows "(h @ l2) \<approx> (h @ r2)"

   167   using a

   167 using a

   168   by (induct) (auto intro: list_eq.intros list_eq_refl)

   168 apply(induct h)

   169 

   169 apply(auto intro: list_eq.intros(5))

   170 lemma append_end:

   170 done

   171   shows "(e # l) \<approx> (l @ [e])"

   171 

   172   apply (induct l)

   172 lemma append_rsp_aux2:

   173   apply (auto intro: list_eq.intros list_eq_refl)

   173   assumes a : "l1 \<approx> r1" "l2 \<approx> r2 "

   174   done

   175 

   176 lemma rev_rsp:

   177   shows "a \<approx> rev a"

   178   apply (induct a)

   179   apply simp

   180   apply (rule list_eq_refl)

   181   apply simp_all

   182   apply (rule list_eq.intros(6))

   183   prefer 2

   184   apply (rule append_rsp_fst)

   185   apply assumption

   186   apply (rule append_end)

   187   done

   188 

   189 lemma append_sym_rsp:

   190   shows "(a @ b) \<approx> (b @ a)"

   191   apply (rule list_eq.intros(6))

   192   apply (rule append_rsp_fst)

   193   apply (rule rev_rsp)

   194   apply (rule list_eq.intros(6))

   195   apply (rule rev_rsp)

   196   apply (simp)

   197   apply (rule append_rsp_fst)

   198   apply (rule list_eq.intros(3))

   199   apply (rule rev_rsp)

   200   done

   201 

   202 lemma append_rsp:

   203   assumes a : "l1 \<approx> r1"

   204   assumes b : "l2 \<approx> r2 "

   206   apply (rule list_eq.intros(6))

   175 using a

   207   apply (rule append_rsp_fst)

   176 apply(induct arbitrary: l2 r2)

   208   using a apply (assumption)

   177 apply(simp_all)

   209   apply (rule list_eq.intros(6))

   178 apply(blast intro: list_eq.intros append_rsp_aux1)+

   210   apply (rule append_sym_rsp)

   179 done

   211   apply (rule list_eq.intros(6))

   180 

   212   apply (rule append_rsp_fst)

   181 lemma append_rsp[quot_respect]:

   213   using b apply (assumption)

   214   apply (rule append_sym_rsp)

   215   done

   216 

   217 lemma ho_append_rsp[quot_respect]:

   219   by (simp add: append_rsp)

   183   by (auto simp add: append_rsp_aux2)