# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260309880 -3600
# Node ID fac547bde4c49fcf5ba6aa8de3cbd48dbb18a217
# Parent  bbaa07eea39673648d064b6b719a030d726a7da6# Parent  0b29650e3fd8bff03966535924b0a9ec06a9c786
merge

diff -r 0b29650e3fd8 -r fac547bde4c4 Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Tue Dec 08 22:26:01 2009 +0100
+++ b/Quot/Examples/FSet.thy	Tue Dec 08 23:04:40 2009 +0100
@@ -444,6 +444,15 @@
 (* apply (tactic {* procedure_tac @{context} @{thm ttt3} 1 *}) *)
 sorry
 
+(* Always safe to apply, but not too helpful *)
+lemma app_prs2:
+  assumes q1: "Quotient R1 abs1 rep1"
+  and     q2: "Quotient R2 abs2 rep2"
+  shows  "((abs1 ---> rep2) ((rep1 ---> abs2) f) (rep1 x)) = rep2 (((rep1 ---> abs2) f) x)"
+unfolding expand_fun_eq
+using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
+by simp
+
 lemma hard: "(\<lambda>P. \<lambda>Q. P (Q (x::'a list))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a list)))"
 sorry
 
@@ -452,14 +461,26 @@
 defer
 apply(injection)
 apply(subst babs_prs)
-defer defer
+apply(tactic {* quotient_tac @{context} 1 *})
+apply(tactic {* quotient_tac @{context} 1 *})
 apply(subst babs_prs)
-defer defer
+apply(tactic {* quotient_tac @{context} 1 *})
+apply(tactic {* quotient_tac @{context} 1 *})
 apply(subst babs_prs)
-defer defer
+apply(tactic {* quotient_tac @{context} 1 *})
+apply(tactic {* quotient_tac @{context} 1 *})
 apply(subst babs_prs)
-defer defer
+apply(tactic {* quotient_tac @{context} 1 *})
+apply(tactic {* quotient_tac @{context} 1 *})
+apply(subst all_prs)
+apply(tactic {* quotient_tac @{context} 1 *})
+apply(tactic {* lambda_prs_tac @{context} 1 *})
+apply(subst fun_map.simps)
 apply(tactic {* lambda_prs_tac @{context} 1 *})
-(* Until here is ok *)
+apply(subst fun_map.simps)
+apply(subst fun_map.simps)
+apply(tactic {* lambda_prs_tac @{context} 1 *})
 apply(cleaning)
+sorry
+
 end