--- a/FSet.thy	Tue Nov 03 14:04:45 2009 +0100
+++ b/FSet.thy	Tue Nov 03 16:17:19 2009 +0100
@@ -309,9 +309,6 @@
 
 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *}
 
-lemma eq_r: "a = b \<Longrightarrow> a \<approx> b"
-by (simp add: list_eq_refl)
-
 (* ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *} *)
 ML {* lift_thm_fset @{context} @{thm m1} *}
 ML {* lift_thm_fset @{context} @{thm m2} *}
@@ -320,6 +317,7 @@
 ML {* lift_thm_fset @{context} @{thm card1_suc} *}
 (*ML {* lift_thm_fset @{context} @{thm map_append} *}*)
 ML {* lift_thm_fset @{context} @{thm append_assoc} *}
+ML {* lift_thm_fset @{context} @{thm list.induct} *}
 
 thm fold1.simps(2)
 thm list.recs(2)
@@ -343,17 +341,13 @@
   apply (atomize(full))
   apply (tactic {* tac @{context} 1 *}) *)
 ML {* val ind_r_r = regularize ind_r_a rty rel rel_eqv rel_refl @{context} *}
-(* ML {*
+(*ML {*
   val rt = build_repabs_term @{context} ind_r_r consts rty qty
   val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt);
 *}
 prove rg
 apply(atomize(full))
 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *}
-apply (tactic {*  (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {*  (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {*  (r_mk_comb_tac_fset @{context}) 1 *})
-
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 done*)
 ML {* val ind_r_t =
@@ -365,6 +359,8 @@
 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm list.induct})) *}
 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *}
 ML {* val simp_app_prs_thms = map (make_simp_prs_thm @{context} quot @{thm APP_PRS}) aps *}
+thm APP_PRS
+ML aps
 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *}
 ML {* val ind_r_l = repeat_eqsubst_thm @{context} (simp_app_prs_thms @ simp_lam_prs_thms) ind_r_t *}
 ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT]]} *}

--- a/LamEx.thy	Tue Nov 03 14:04:45 2009 +0100
+++ b/LamEx.thy	Tue Nov 03 16:17:19 2009 +0100
@@ -282,81 +282,17 @@
 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *}
 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm alpha.induct})) *}
 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm alpha.induct})) *}
-ML {* prop_of (atomize_thm @{thm alpha.induct}) *}
-ML {*
-  fun findall_all rty qty tm =
-    case tm of
-      Const (@{const_name All}, T) $ (s as (Abs(_, _, b))) =>
-        let
-          val tys = findall_all rty qty s
-        in if needs_lift rty T then
-          (( T) :: tys)
-        else tys end
-    | Abs(_, T, b) =>
-        findall_all rty qty (subst_bound ((Free ("x", T)), b))
-    | f $ a => (findall_all rty qty f) @ (findall_all rty qty a)
-    | _ => [];
-  fun findall rty qty tm =
-    map domain_type (
-      map (old_exchange_ty rty qty)
-      (distinct (op =) (findall_all rty qty tm))
-    )
-*}
-ML {* val alls = findall rty qty (prop_of (atomize_thm @{thm alpha.induct})) *}
-
-ML {*
-fun make_simp_all_prs_thm lthy quot_thm thm typ =
-  let
-    val (_, [lty, rty]) = dest_Type typ;
-    val thy = ProofContext.theory_of lthy;
-    val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty)
-    val inst = [NONE, SOME lcty];
-    val lpi = Drule.instantiate' inst [] thm;
-    val tac =
-      (compose_tac (false, lpi, 1)) THEN_ALL_NEW
-      (quotient_tac quot_thm);
-    val gc = Drule.strip_imp_concl (cprop_of lpi);
-    val t = Goal.prove_internal [] gc (fn _ => tac 1)
-  in
-    MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t
-  end
-*}
+ML {* val (alls, exs) = findallex rty qty (prop_of (atomize_thm @{thm alpha.induct})) *}
+ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS} ) alls *}
+ML {* val exthms = map (make_allex_prs_thm @{context} quot @{thm EXISTS_PRS} ) exs *}
+ML {* val t_a = MetaSimplifier.rewrite_rule allthms t_t *}
 ML {* val simp_app_prs_thms = map (make_simp_prs_thm @{context} quot @{thm APP_PRS}) aps *}
-ML {* val aps = @{typ "LamEx.rlam \<Rightarrow> bool"} :: aps; *}
 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *}
-ML {* val t_l = repeat_eqsubst_thm @{context} (simp_app_prs_thms @  simp_lam_prs_thms) t_a *}
-ML {* val typ = hd (alls) *}
-
-
-ML {*
-    val (_, [lty, rty]) = dest_Type typ;
-    val thy = @{theory};
-    val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty)
-    val inst = [NONE, SOME lcty];
-    val lpi = Drule.instantiate' inst [] @{thm FORALL_PRS};
-    val tac =
-      (compose_tac (false, lpi, 1)) THEN_ALL_NEW
-      (quotient_tac quot);
-    val gc = Drule.strip_imp_concl (cprop_of lpi);
-*}
-prove tst: {*term_of gc*}
-apply (tactic {*compose_tac (false, lpi, 1) 1 *})
-apply (tactic {*quotient_tac quot 1 *})
-done
-thm tst
-
-
-
-
-
-ML {* val thms = (make_simp_all_prs_thm @{context} quot @{thm FORALL_PRS} o domain_type) (hd (rev alls)) *}
-ML {* val thm =
-  @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_lam FUN_QUOTIENT[OF QUOTIENT_lam IDENTITY_QUOTIENT]]]} *}
-ML {* val t_a = simp_allex_prs quot [thm] t_t *}
+ML {* val t_l = repeat_eqsubst_thm @{context} (simp_lam_prs_thms) t_a *}
+ML {* val t_l1 = repeat_eqsubst_thm @{context} simp_app_prs_thms t_l *}
 ML {* val defs_sym = add_lower_defs @{context} defs; *}
 ML {* val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym *}
-ML t_l
-ML {* val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l *}
+ML {* val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l1 *}
 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_d0 *}
 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *}
 ML {* val t_r1 = repeat_eqsubst_thm @{context} @{thms fun_map.simps} t_r *}

--- a/QuotMain.thy	Tue Nov 03 14:04:45 2009 +0100
+++ b/QuotMain.thy	Tue Nov 03 16:17:19 2009 +0100
@@ -538,12 +538,13 @@
 *}
 
 lemma universal_twice: "(\<And>x. (P x \<longrightarrow> Q x)) \<Longrightarrow> ((\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x))"
-apply (auto)
-done
+by auto
 
 lemma implication_twice: "(c \<longrightarrow> a) \<Longrightarrow> (a \<Longrightarrow> b \<longrightarrow> d) \<Longrightarrow> (a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
-apply (auto)
-done
+by auto
+
+(*lemma equality_twice: "a = c \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> c = d)"
+by auto*)
 
 ML {*
 fun regularize thm rty rel rel_eqv rel_refl lthy =
@@ -557,6 +558,7 @@
       rtac @{thm universal_twice},
       (rtac @{thm impI} THEN' atac),
       rtac @{thm implication_twice},
+      (*rtac @{thm equality_twice},*)
       EqSubst.eqsubst_tac ctxt [0]
         [(@{thm equiv_res_forall} OF [rel_eqv]),
          (@{thm equiv_res_exists} OF [rel_eqv])],
@@ -708,21 +710,6 @@
 )
 *}
 
-ML {*
-fun res_forall_rsp_tac ctxt =
-  (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
-  THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
-  THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN'
-  (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
-*}
-
-ML {*
-fun res_exists_rsp_tac ctxt =
-  (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
-  THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
-  THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'
-  (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
-*}
 
 
 ML {*
@@ -770,6 +757,34 @@
 *}
 
 ML {*
+val res_forall_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
+  let
+    val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _)) = term_of concl
+  in
+    ((simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
+    THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
+    THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN'
+    (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))) 1
+  end
+  handle _ => no_tac
+  )
+*}
+
+ML {*
+val res_exists_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
+  let
+    val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _)) = term_of concl
+  in
+    ((simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
+    THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
+    THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'
+    (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))) 1
+  end
+  handle _ => no_tac
+  )
+*}
+
+ML {*
 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
   (FIRST' [
 (*    rtac @{thm FUN_QUOTIENT},
@@ -779,10 +794,7 @@
     LAMBDA_RES_TAC ctxt,
     res_forall_rsp_tac ctxt,
     res_exists_rsp_tac ctxt,
-    (
-     (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps rsp_thms))
-     THEN_ALL_NEW (fn _ => no_tac)
-    ),
+    FIRST' (map rtac rsp_thms),
     (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
     rtac refl,
 (*    rtac @{thm arg_cong2[of _ _ _ _ "op ="]},*)
@@ -893,17 +905,63 @@
 *}
 
 ML {*
-  fun simp_allex_prs quot thms thm =
+  fun findallex_all rty qty tm =
+    case tm of
+      Const (@{const_name All}, T) $ (s as (Abs(_, _, b))) =>
+        let
+          val (tya, tye) = findallex_all rty qty s
+        in if needs_lift rty T then
+          ((T :: tya), tye)
+        else (tya, tye) end
+    | Const (@{const_name Ex}, T) $ (s as (Abs(_, _, b))) =>
+        let
+          val (tya, tye) = findallex_all rty qty s
+        in if needs_lift rty T then
+          (tya, (T :: tye))
+        else (tya, tye) end
+    | Abs(_, T, b) =>
+        findallex_all rty qty (subst_bound ((Free ("x", T)), b))
+    | f $ a =>
+        let
+          val (a1, e1) = findallex_all rty qty f;
+          val (a2, e2) = findallex_all rty qty a;
+        in (a1 @ a2, e1 @ e2) end
+    | _ => ([], []);
+*}
+ML {*
+  fun findallex rty qty tm =
     let
-      val ts = [@{thm FORALL_PRS} OF [quot], @{thm EXISTS_PRS} OF [quot]] @ thms
-      val sym_ts = map (fn x => @{thm "HOL.sym"} OF [x]) ts;
-      val eq_ts = map (fn x => @{thm "eq_reflection"} OF [x]) sym_ts
+      val (a, e) = findallex_all rty qty tm;
+      val (ad, ed) = (map domain_type a, map domain_type e);
+      val (au, eu) = (distinct (op =) ad, distinct (op =) ed)
     in
-      MetaSimplifier.rewrite_rule eq_ts thm
+      (map (old_exchange_ty rty qty) au, map (old_exchange_ty rty qty) eu)
     end
 *}
 
 ML {*
+fun make_allex_prs_thm lthy quot_thm thm typ =
+  let
+    val (_, [lty, rty]) = dest_Type typ;
+    val thy = ProofContext.theory_of lthy;
+    val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty)
+    val inst = [NONE, SOME lcty];
+    val lpi = Drule.instantiate' inst [] thm;
+    val tac =
+      (compose_tac (false, lpi, 1)) THEN_ALL_NEW
+      (quotient_tac quot_thm);
+    val gc = Drule.strip_imp_concl (cprop_of lpi);
+    val t = Goal.prove_internal [] gc (fn _ => tac 1)
+    val t_noid = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t;
+    val t_sym = @{thm "HOL.sym"} OF [t_noid];
+    val t_eq = @{thm "eq_reflection"} OF [t_sym]
+  in
+    t_eq
+  end
+*}
+
+
+ML {*
 fun lookup_quot_data lthy qty =
   let
     val SOME quotdata = find_first (fn x => matches ((#qtyp x), qty)) (quotdata_lookup lthy)
@@ -947,11 +1005,14 @@
   val t_a = atomize_thm t;
   val t_r = regularize t_a rty rel rel_eqv rel_refl lthy;
   val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms;
+  val (alls, exs) = findallex rty qty (prop_of t_a);
+  val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls
+  val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs
+  val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t
   val abs = findabs rty (prop_of t_a);
   val aps = findaps rty (prop_of t_a);
   val app_prs_thms = map (make_simp_prs_thm lthy quot @{thm APP_PRS}) aps;
   val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs;
-  val t_a = simp_allex_prs quot [] t_t;
   val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a;
   val defs_sym = add_lower_defs lthy defs;
   val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym;