--- a/QuotMain.thy	Fri Oct 23 11:24:43 2009 +0200
+++ b/QuotMain.thy	Fri Oct 23 16:01:13 2009 +0200
@@ -966,6 +966,7 @@
 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *}
 ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *}
 
+thm fun_map.simps
 text {* Respectfullness *}
 
 lemma mem_respects:
@@ -1057,9 +1058,12 @@
     res_forall_rsp_tac ctxt,
     (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
     (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
-      rtac reflex_thm,
-      atac,
-      ((simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps}))  THEN_ALL_NEW (fn _ => no_tac))
+    rtac reflex_thm,
+    atac,
+    (
+     (simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps}))
+     THEN_ALL_NEW (fn _ => no_tac)
+    )
     ])
 *}
 
@@ -1139,7 +1143,7 @@
 ML {* val nthm = MetaSimplifier.rewrite_rule fset_defs_sym (snd (no_vars (Context.Theory @{theory}, @{thm list_induct_t}))) *}
 
 thm list.recs(2)
-
+thm m2
 ML {* atomize_thm @{thm m2} *}
 
 prove m2_r_p: {*
@@ -1203,18 +1207,43 @@
 apply (tactic {* rtac m2_r 1 *})
 done
 
+lemma id_apply2 [simp]: "id x \<equiv> x"
+  by (simp add: id_def)
+
+
 thm LAMBDA_PRS
 ML {*
  val t = prop_of @{thm LAMBDA_PRS}
  val tt = Drule.instantiate' [SOME @{ctyp "'a list"}, SOME @{ctyp "'a fset"}] [] @{thm LAMBDA_PRS}
- val ttt = tt OF [@{thm QUOTIENT_fset}, @{thm IDENTITY_QUOTIENT}]
+ val ttt = @{thm LAMBDA_PRS} OF [@{thm QUOTIENT_fset}, @{thm IDENTITY_QUOTIENT}]
+ val tttt = @{thm "HOL.sym"} OF [ttt]
+*}
+ML {*
+ val ttttt = MetaSimplifier.rewrite_rule [@{thm id_apply2}] tttt
+ val zzz = @{thm m2_t} 
 *}
-ML {* val tttt = @{thm "HOL.sym"} OF [ttt] *}
-ML {* val zzzz = MetaSimplifier.rewrite_rule  [tttt] @{thm m2_t} *}
 
+ML {*
+fun eqsubst_thm ctxt thms thm =
+  let
+    val goalstate = Goal.init (Thm.cprop_of thm)
+    val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
+      NONE => error "eqsubst_thm"
+    | SOME th => cprem_of th 1
+    val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1
+    val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a'))
+    val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac));
+  in
+    Simplifier.rewrite_rule [rt] thm
+  end
+*}
+ML {* val m2_t' = eqsubst_thm @{context} [ttttt] @{thm m2_t} *}
+ML {* val rwr = @{thm FORALL_PRS[OF QUOTIENT_fset]} *}
+ML {* val rwrs = @{thm "HOL.sym"} OF [ObjectLogic.rulify rwr] *}
+ML {* rwrs; m2_t' *}
+ML {* eqsubst_thm @{context} [rwrs] m2_t' *}
+thm INSERT_def
 
-thm m2_t
-ML {* @{thm m2_t} *}
 
 ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *}
 

--- a/QuotScript.thy	Fri Oct 23 11:24:43 2009 +0200
+++ b/QuotScript.thy	Fri Oct 23 16:01:13 2009 +0200
@@ -473,11 +473,31 @@
   shows "Ex P \<Longrightarrow> Bex R Q"
   using a by (metis COMBC_def Collect_def Collect_mem_eq)
 
+(* TODO: Add similar *)
 lemma RES_FORALL_RSP:
   shows "\<And>f g. (R ===> (op =)) f g ==>
         (Ball (Respects R) f = Ball (Respects R) g)"
   apply (simp add: FUN_REL.simps Ball_def IN_RESPECTS)
   done
 
+(* TODO: 
+- [FORALL_PRS, EXISTS_PRS, COND_PRS];
+> val it =
+    [|- !R abs rep.
+          QUOTIENT R abs rep ==>
+          !f. $! f <=> RES_FORALL (respects R) ((abs --> I) f),
+     |- !R abs rep.
+          QUOTIENT R abs rep ==>
+          !f. $? f <=> RES_EXISTS (respects R) ((abs --> I) f),
+     |- !R abs rep.
+          QUOTIENT R abs rep ==>
+          !a b c. (if a then b else c) = abs (if a then rep b else rep c)] :
+*)
+lemma FORALL_PRS:
+  assumes a: "QUOTIENT R absf repf"
+  shows "!f. All f = Ball (Respects R) ((absf ---> id) f)"
+  sorry
+
+
 end