# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271661943 -7200
# Node ID a08eaea622d125357303b78dc560b0dfa23d5ed9
# Parent  6d4e4bf9bce661b00bbb2f6084c1fe7e29576ea5
minor FSet3 edits.

diff -r 6d4e4bf9bce6 -r a08eaea622d1 Attic/Quot/Examples/FSet3.thy
--- a/Attic/Quot/Examples/FSet3.thy	Fri Apr 16 16:29:11 2010 +0200
+++ b/Attic/Quot/Examples/FSet3.thy	Mon Apr 19 09:25:43 2010 +0200
@@ -245,12 +245,6 @@
 is
  "concat"
 
-(*lemma fconcat_rsp[quot_respect]:
-  shows "((list_rel op \<approx>) ===> op \<approx>) concat concat"
-apply(auto)
-sorry
-*)
-
 (* PROBLEM: these lemmas needs to be restated, since  *)
 (* concat.simps(1) and concat.simps(2) contain the    *)
 (* type variables ?'a1.0 (which are turned into frees *)
@@ -263,9 +257,21 @@
   shows "concat (x # xs) \<approx> x @ concat xs"
 by (simp)
 
-lemma concat_rsp[quot_respect]:
+lemma concat_rsp:
+  "\<lbrakk>list_rel op \<approx> x x'; x' \<approx> y'; list_rel op \<approx> y' y\<rbrakk> \<Longrightarrow> concat x \<approx> concat y"
+  apply (induct x y arbitrary: x' y' rule: list_induct2')
+  apply simp
+  defer defer
+  apply (simp only: concat.simps)
+  sorry
+
+lemma [quot_respect]:
   shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"
-  sorry
+  apply (simp only: fun_rel_def)
+  apply clarify
+  apply (rule concat_rsp)
+  apply assumption+
+  done
 
 lemma nil_rsp2[quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []"
   apply (metis FSet3.nil_rsp list_rel.simps(1) pred_comp.intros)
@@ -360,8 +366,6 @@
   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
@@ -709,19 +713,4 @@
 lemma "funion (funion x xa) xb = funion x (funion xa xb)"
 by (lifting append_assoc)
 
-quotient_definition
-  "fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
-is
-  "list_case"
-
-(* NOT SURE IF TRUE *)
-lemma list_case_rsp[quot_respect]:
-  "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
-  apply (auto)
-  sorry
-
-lemma "fset_case (f1::'t) f2 (finsert a xa) = f2 a xa"
-apply (lifting list.cases(2))
-done
-
 end