# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260411079 -3600
# Node ID 3c6419a5a7fc9f8780313fbd85358b36f53175fa
# Parent  d003f9e00c29623360fbfd181063ddb16db5864d
simplified proofs

diff -r d003f9e00c29 -r 3c6419a5a7fc Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Thu Dec 10 02:46:08 2009 +0100
+++ b/Quot/Examples/FSet.thy	Thu Dec 10 03:11:19 2009 +0100
@@ -161,62 +161,26 @@
   "(op = ===> op \<approx> ===> op \<approx>) op # op #"
   by (simp add: cons_rsp)
 
-lemma append_rsp_fst:
-  assumes a : "l1 \<approx> l2"
-  shows "(l1 @ s) \<approx> (l2 @ s)"
-  using a
-  by (induct) (auto intro: list_eq.intros list_eq_refl)
-
-lemma append_end:
-  shows "(e # l) \<approx> (l @ [e])"
-  apply (induct l)
-  apply (auto intro: list_eq.intros list_eq_refl)
-  done
-
-lemma rev_rsp:
-  shows "a \<approx> rev a"
-  apply (induct a)
-  apply simp
-  apply (rule list_eq_refl)
-  apply simp_all
-  apply (rule list_eq.intros(6))
-  prefer 2
-  apply (rule append_rsp_fst)
-  apply assumption
-  apply (rule append_end)
-  done
+lemma append_rsp_aux1:
+  assumes a : "l2 \<approx> r2 "
+  shows "(h @ l2) \<approx> (h @ r2)"
+using a
+apply(induct h)
+apply(auto intro: list_eq.intros(5))
+done
 
-lemma append_sym_rsp:
-  shows "(a @ b) \<approx> (b @ a)"
-  apply (rule list_eq.intros(6))
-  apply (rule append_rsp_fst)
-  apply (rule rev_rsp)
-  apply (rule list_eq.intros(6))
-  apply (rule rev_rsp)
-  apply (simp)
-  apply (rule append_rsp_fst)
-  apply (rule list_eq.intros(3))
-  apply (rule rev_rsp)
-  done
+lemma append_rsp_aux2:
+  assumes a : "l1 \<approx> r1" "l2 \<approx> r2 "
+  shows "(l1 @ l2) \<approx> (r1 @ r2)"
+using a
+apply(induct arbitrary: l2 r2)
+apply(simp_all)
+apply(blast intro: list_eq.intros append_rsp_aux1)+
+done
 
-lemma append_rsp:
-  assumes a : "l1 \<approx> r1"
-  assumes b : "l2 \<approx> r2 "
-  shows "(l1 @ l2) \<approx> (r1 @ r2)"
-  apply (rule list_eq.intros(6))
-  apply (rule append_rsp_fst)
-  using a apply (assumption)
-  apply (rule list_eq.intros(6))
-  apply (rule append_sym_rsp)
-  apply (rule list_eq.intros(6))
-  apply (rule append_rsp_fst)
-  using b apply (assumption)
-  apply (rule append_sym_rsp)
-  done
-
-lemma ho_append_rsp[quot_respect]:
+lemma append_rsp[quot_respect]:
   "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
-  by (simp add: append_rsp)
+  by (auto simp add: append_rsp_aux2)
 
 lemma map_rsp:
   assumes a: "a \<approx> b"