# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260219254 -3600
# Node ID bb5d3278f02eac68ea294ff2d8d9c26f3ed91877
# Parent  2bee5ca44ef567a900b96124e27fcfb5af6a19b9# Parent  6ce4f274b0fab0b4571e232840d57daaaa455fc9
merged

diff -r 2bee5ca44ef5 -r bb5d3278f02e Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Mon Dec 07 21:53:50 2009 +0100
+++ b/Quot/Examples/FSet.thy	Mon Dec 07 21:54:14 2009 +0100
@@ -427,5 +427,28 @@
 apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *})
 done
 
+lemma ttt: "((op @) x ((op #) e [])) = (((op #) e x))"
+sorry
+lemma "(FUNION x (INSERT e EMPTY)) = ((INSERT e x))"
+apply (tactic {* lift_tac @{context} @{thm ttt} 1 *})
+done
+
+lemma ttt2: "(\<lambda>e. ((op @) x ((op #) e []))) = (\<lambda>e. ((op #) e x))"
+sorry
+
+lemma "(\<lambda>e. (FUNION x (INSERT e EMPTY))) = (\<lambda>e. (INSERT e x))"
+apply (tactic {* procedure_tac @{context} @{thm ttt2} 1 *})
+apply(tactic {* regularize_tac @{context} 1 *})
+defer
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac_fset @{context}) 1*})
+(* apply(tactic {* clean_tac @{context} 1 *}) *)
+sorry
+
+lemma ttt3: "(\<lambda>x. ((op @) x ((op #) e []))) = (\<lambda>x. ((op #) e x))"
+sorry
+
+lemma "(\<lambda>x. (FUNION x (INSERT e EMPTY))) = (\<lambda>x. (INSERT e x))"
+(* apply (tactic {* procedure_tac @{context} @{thm ttt3} 1 *}) *)
+sorry
 
 end
diff -r 2bee5ca44ef5 -r bb5d3278f02e Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Mon Dec 07 21:53:50 2009 +0100
+++ b/Quot/QuotMain.thy	Mon Dec 07 21:54:14 2009 +0100
@@ -1000,7 +1000,7 @@
 fun lambda_prs_simple_conv ctxt ctrm =
   case (term_of ctrm) of
    ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>
-     let
+     (let
        val thy = ProofContext.theory_of ctxt
        val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
        val (ty_c, ty_d) = dest_fun_type (fastype_of a2)
@@ -1015,7 +1015,7 @@
            val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm)
          in
            Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
-         end handle Bind =>
+         end handle _ => (* TODO handle only Bind | Error "make_inst" *)
          let
            val (insp, inst) = make_inst2 (term_of (Thm.lhs_of te)) (term_of ctrm)
            val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te
@@ -1032,6 +1032,7 @@
      in
        Conv.rewr_conv ti ctrm
      end
+     handle _ => Conv.all_conv ctrm)
   | _ => Conv.all_conv ctrm
 *}
 
diff -r 2bee5ca44ef5 -r bb5d3278f02e Quot/QuotScript.thy
--- a/Quot/QuotScript.thy	Mon Dec 07 21:53:50 2009 +0100
+++ b/Quot/QuotScript.thy	Mon Dec 07 21:54:14 2009 +0100
@@ -338,12 +338,23 @@
   using Quotient_rel[OF q]
   by metis
 
+lemma babs_prs:
+  assumes q1: "Quotient R1 Abs1 Rep1"
+  and     q2: "Quotient R2 Abs2 Rep2"
+  shows "(Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f)) \<equiv> f"
+  apply(rule eq_reflection)
+  apply(rule ext)
+  apply simp
+  apply (subgoal_tac "Rep1 x \<in> Respects R1")
+  apply (simp add: Babs_def Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
+  apply (simp add: in_respects Quotient_rel_rep[OF q1])
+  done
+
 (* needed for regularising? *)
 lemma babs_reg_eqv:
   shows "equivp R \<Longrightarrow> Babs (Respects R) P = P"
 by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp)
 
-
 (* 2 lemmas needed for cleaning of quantifiers *)
 lemma all_prs:
   assumes a: "Quotient R absf repf"