# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271324548 -7200
# Node ID 05b2dd2b0e8a09b864eb699dac0f0cb37cbf25df
# Parent  0e70f3c82876a78352af68c3fa7bc89103a84738
Prove insert_rsp2

diff -r 0e70f3c82876 -r 05b2dd2b0e8a Attic/Quot/Examples/FSet3.thy
--- a/Attic/Quot/Examples/FSet3.thy	Thu Apr 15 11:05:54 2010 +0200
+++ b/Attic/Quot/Examples/FSet3.thy	Thu Apr 15 11:42:28 2010 +0200
@@ -72,9 +72,13 @@
   shows "[] \<approx> []"
 by simp
 
-lemma cons_rsp[quot_respect]: 
+lemma cons_rsp:
+  "xa \<approx> ya \<Longrightarrow> y # xa \<approx> y # ya"
+  by simp
+
+lemma [quot_respect]:
   shows "(op = ===> op \<approx> ===> op \<approx>) op # op #"
-by simp
+  by simp
 
 
 section {* Augmenting a set -- @{const finsert} *}
@@ -257,11 +261,11 @@
 
 lemma concat2:
   shows "concat (x # xs) \<approx> x @ concat xs"
-by (simp add: id_simps)
+by (simp)
 
 lemma concat_rsp[quot_respect]:
   shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"
-sorry
+  sorry
 
 lemma nil_rsp2[quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []"
   apply (metis FSet3.nil_rsp list_rel.simps(1) pred_comp.intros)
@@ -344,25 +348,31 @@
   apply (metis equivp_def fset_equivp)
   apply rule
   apply rule
-  apply(rule quotient_compose_list_pre)
+  apply (rule quotient_compose_list_pre)
   done
 
 lemma fconcat_empty:
   shows "fconcat {||} = {||}"
-apply(lifting concat1)
-apply(cleaning)
-apply(simp add: comp_def)
-apply(fold fempty_def[simplified id_simps])
-apply(rule refl)
-done
+  apply(lifting concat1)
+  apply(cleaning)
+  apply(simp add: comp_def)
+  apply(fold fempty_def[simplified id_simps])
+  apply(rule refl)
+  done
 
 (* Should be true *)
 
 lemma insert_rsp2[quot_respect]:
   "(op \<approx> ===> list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx>) op # op #"
-apply auto
-apply (simp add: set_in_eq)
-sorry
+  apply auto
+  apply (simp add: set_in_eq)
+  apply (rule_tac b="x # b" in pred_compI)
+  apply auto
+  apply (rule_tac b="x # ba" in pred_compI)
+  apply (rule cons_rsp)
+  apply simp
+  apply (auto)[1]
+  done
 
 lemma append_rsp[quot_respect]:
   "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
@@ -370,11 +380,11 @@
 
 lemma fconcat_insert:
   shows "fconcat (finsert x S) = x |\<union>| fconcat S"
-apply(lifting concat2)
-apply(cleaning)
-apply (simp add: finsert_def fconcat_def comp_def)
-apply cleaning
-done
+  apply(lifting concat2)
+  apply(cleaning)
+  apply (simp add: finsert_def fconcat_def comp_def)
+  apply cleaning
+  done
 
 text {* raw section *}