diff -r 2cb5745f403e -r 7be9b054f672 Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Sat Jan 23 17:25:18 2010 +0100
+++ b/Quot/Examples/FSet.thy	Sun Jan 24 23:41:27 2010 +0100
@@ -1,5 +1,5 @@
 theory FSet
-imports "../QuotMain" "../QuotList" List
+imports "../QuotMain" "../QuotList" "../QuotProd" List
 begin
 
 inductive
@@ -377,6 +377,46 @@
 apply(assumption)
 done
 
+lemma [quot_respect]:
+  "((op \<approx> ===> op \<approx> ===> op =) ===> prod_rel op \<approx> op \<approx> ===> op =) split split"
+apply(simp)
+done
+
+thm quot_preserve
+term split
+
+
+lemma [quot_preserve]:
+  shows "(((abs_fset ---> abs_fset ---> id) ---> prod_fun rep_fset rep_fset ---> id) split) = split"
+apply(simp add: expand_fun_eq)
+apply(simp add: Quotient_abs_rep[OF Quotient_fset])
+done
+
+
+lemma test: "All (\<lambda>(x::'a list, y). x = y)"
+sorry
+
+lemma  "All (\<lambda>(x::'a fset, y). x = y)"
+apply(lifting test)
+apply(cleaning)
+thm all_prs
+apply(rule all_prs)
+apply(tactic {* Quotient_Tacs.quotient_tac @{context} 1*})
+done
+
+lemma test2: "Ex (\<lambda>(x::'a list, y). x = y)"
+sorry
+
+lemma  "Ex (\<lambda>(x::'a fset, y). x = y)"
+apply(lifting test2)
+apply(cleaning)
+apply(rule ex_prs)
+apply(tactic {* Quotient_Tacs.quotient_tac @{context} 1*})
+done
+
+ML {* @{term "Ex (\<lambda>(x::'a fset, y). x = y)"} *}
+
+
 
 
 end