# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260545560 -3600
# Node ID 1e08743b6997a8d32a5e1e168848cb4e8c94ca00
# Parent  3d7a9d4d2bb67107f3e43ce787e0c953130543a7
FSet3 minor fixes + cases

diff -r 3d7a9d4d2bb6 -r 1e08743b6997 FIXME-TODO
--- a/FIXME-TODO	Fri Dec 11 15:58:15 2009 +0100
+++ b/FIXME-TODO	Fri Dec 11 16:32:40 2009 +0100
@@ -20,15 +20,14 @@
 Lower Priority
 ==============
 
+- accept partial equvalence relations
+
 - inductions from the datatype package have a strange
   order of quantifiers in assumptions.
 
 - wrapper that translates an an original theorem given
   a list of quotient_types as an attribute
 
-
-
-
 - find clean ways how to write down the "mathematical"
   procedure for a possible submission (Peter submitted 
   his work only to TPHOLs 2005...we would have to go
diff -r 3d7a9d4d2bb6 -r 1e08743b6997 Quot/Examples/FSet3.thy
--- a/Quot/Examples/FSet3.thy	Fri Dec 11 15:58:15 2009 +0100
+++ b/Quot/Examples/FSet3.thy	Fri Dec 11 16:32:40 2009 +0100
@@ -22,7 +22,7 @@
 quotient fset = "'a list" / "list_eq"
   by (rule list_eq_equivp)
 
-lemma not_nil_equiv_cons: "[] \<noteq> a # A" sorry
+lemma not_nil_equiv_cons: "\<not>[] \<approx> a # A" sorry
 
 (* The 2 lemmas below are different from the ones in QuotList *)
 lemma nil_rsp[quot_respect]:
@@ -276,4 +276,20 @@
 lemma "funion (funion x xa) xb = funion x (funion xa xb)"
 by (lifting append_assoc)
 
+quotient_def
+  "fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
+as
+  "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 (Insert a xa) = f2 a xa"
+apply (lifting list.cases(2))
+done
+
+
 end