# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259201918 -3600
# Node ID 58947b7232ef934e493d39422f8737089d214f60
# Parent  1dd6a21cdd1c5f9cb14940b2b01cac844807c393# Parent  d67240113f68016356e3f56e97eb1dcb0fa474e6
merged

diff -r 1dd6a21cdd1c -r 58947b7232ef FSet.thy
--- a/FSet.thy	Thu Nov 26 02:31:00 2009 +0100
+++ b/FSet.thy	Thu Nov 26 03:18:38 2009 +0100
@@ -304,7 +304,7 @@
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *}
 ML {* val consts = lookup_quot_consts defs *}
-ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *}
+ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs *}
 
 lemma "IN x EMPTY = False"
 by (tactic {* lift_tac_fset @{context} @{thm m1} 1 *})
@@ -334,8 +334,6 @@
 done
 
 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
-apply(tactic {* Induct.fix_tac @{context} 0 [("x", @{typ "'b fset"}), ("xa", @{typ "'b fset"})] 1 *})
-apply(tactic {* ObjectLogic.full_atomize_tac 1 *})
 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *})
 done
 
@@ -412,26 +410,14 @@
 
 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}
 ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *}
-ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *}
+ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs *}
 
-ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.recs(2)})) *}
-ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *}
 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"
 apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *})
-apply (tactic {* (simp_tac (HOL_ss addsimps
-  @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id})) 1 *})
-ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *}
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1 *})
-apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
 done
 
-ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.cases(2)})) *}
-ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *}
 lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa"
 apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *})
-apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
 done
 
 lemma list_induct_part:
@@ -452,7 +438,7 @@
 
 (* Construction site starts here *)
 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
-apply (tactic {* procedure_tac @{thm list_induct_part} @{context} 1 *})
+apply (tactic {* procedure_tac @{context} @{thm list_induct_part} 1 *})
 apply (tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *})
 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
 apply (rule FUN_QUOTIENT)
@@ -478,7 +464,6 @@
 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 {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
 apply (rule IDENTITY_QUOTIENT)
 apply (rule FUN_QUOTIENT)
@@ -503,7 +488,6 @@
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
-apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *})
 apply assumption
 apply (rule refl)
@@ -522,14 +506,7 @@
 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 (simp only:map_id)
-apply (tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *})
-ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *}
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1 *})
-apply (tactic {* lambda_prs_tac @{context} quot 1 *})
-ML_prf {* val t = applic_prs @{context} rty qty absrep @{typ "('b \<Rightarrow> 'c list \<Rightarrow> bool)"} *}
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] [t]) 1 *})
-apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
+apply (tactic {* clean_tac @{context} quot defs reps_same absrep [(@{typ "('a list \<Rightarrow> 'c list \<Rightarrow> bool)"},@{typ "('a list \<Rightarrow> 'c fset \<Rightarrow> bool)"})] 1 *})
 done
 
 end
diff -r 1dd6a21cdd1c -r 58947b7232ef IntEx.thy
--- a/IntEx.thy	Thu Nov 26 02:31:00 2009 +0100
+++ b/IntEx.thy	Thu Nov 26 03:18:38 2009 +0100
@@ -142,7 +142,7 @@
 
 ML {*
 fun lift_tac_fset lthy t =
-  lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs
+  lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs
 *}
 
 lemma "PLUS a b = PLUS b a"
@@ -166,8 +166,6 @@
 
 lemma "foldl PLUS x [] = x"
 apply (tactic {* lift_tac_fset @{context} @{thm ho_tst} 1 *})
-prefer 3
-apply(tactic {* clean_tac @{context} quot @{thms PLUS_def} reps_same 1 *})
 sorry
 
 (*
diff -r 1dd6a21cdd1c -r 58947b7232ef LamEx.thy
--- a/LamEx.thy	Thu Nov 26 02:31:00 2009 +0100
+++ b/LamEx.thy	Thu Nov 26 03:18:38 2009 +0100
@@ -179,7 +179,7 @@
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val consts = lookup_quot_consts defs *}
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *}
-ML {* fun lift_tac_lam lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *}
+ML {* fun lift_tac_lam lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs *}
 
 lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)"
 apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *})
@@ -224,16 +224,12 @@
 apply (tactic {* lift_tac_lam @{context} @{thm alpha.cases} 1 *})
 done
 
-ML {* val aps = findaps rty (prop_of (atomize_thm @{thm alpha.induct})) *}
-ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *}
 lemma alpha_induct: "\<lbrakk>(qx\<Colon>lam) = (qxa\<Colon>lam); \<And>(a\<Colon>name) b\<Colon>name. a = b \<Longrightarrow> (qxb\<Colon>lam \<Rightarrow> lam \<Rightarrow> bool) (Var a) (Var b);
      \<And>(x\<Colon>lam) (xa\<Colon>lam) (xb\<Colon>lam) xc\<Colon>lam. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc);
      \<And>(x\<Colon>lam) (a\<Colon>name) (b\<Colon>name) xa\<Colon>lam.
         \<lbrakk>x = [(a, b)] \<bullet> xa; qxb x ([(a, b)] \<bullet> xa); a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> qxb (Lam a x) (Lam b xa)\<rbrakk>
     \<Longrightarrow> qxb qx qxa"
 apply (tactic {* lift_tac_lam @{context} @{thm alpha.induct} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *})
-apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
 done
 
 lemma var_inject: "(Var a = Var b) = (a = b)"
diff -r 1dd6a21cdd1c -r 58947b7232ef QuotMain.thy
--- a/QuotMain.thy	Thu Nov 26 02:31:00 2009 +0100
+++ b/QuotMain.thy	Thu Nov 26 03:18:38 2009 +0100
@@ -817,7 +817,9 @@
   (FIRST' [
     rtac trans_thm,
     LAMBDA_RES_TAC ctxt,
+    rtac @{thm RES_FORALL_RSP},
     ball_rsp_tac ctxt,
+    rtac @{thm RES_EXISTS_RSP},
     bex_rsp_tac ctxt,
     FIRST' (map rtac rsp_thms),
     rtac refl,
@@ -928,7 +930,7 @@
 *}
 
 ML {*
-fun applic_prs lthy rty qty absrep ty =
+fun applic_prs_old lthy rty qty absrep ty =
   let
     val rty = Logic.varifyT rty;
     val qty = Logic.varifyT qty;
@@ -961,6 +963,30 @@
   end
 *}
 
+ML {*
+fun applic_prs lthy absrep (rty, qty) =
+  let
+    fun mk_rep (T, T') tm = (Quotient_Def.get_fun repF lthy (T, T')) $ tm;
+    fun mk_abs (T, T') tm = (Quotient_Def.get_fun absF lthy (T, T')) $ tm;
+    val (raty, rgty) = Term.strip_type rty;
+    val (qaty, qgty) = Term.strip_type qty;
+    val vs = map (fn _ => "x") qaty;
+    val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy;
+    val f = Free (fname, qaty ---> qgty);
+    val args = map Free (vfs ~~ qaty);
+    val rhs = list_comb(f, args);
+    val largs = map2 mk_rep (raty ~~ qaty) args;
+    val lhs = mk_abs (rgty, qgty) (list_comb((mk_rep (raty ---> rgty, qaty ---> qgty) f), largs));
+    val llhs = Syntax.check_term lthy lhs;
+    val eq = Logic.mk_equals (llhs, rhs);
+    val ceq = cterm_of (ProofContext.theory_of lthy') eq;
+    val sctxt = HOL_ss addsimps (absrep :: @{thms fun_map.simps map_id id_apply});
+    val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1)
+    val t_id = MetaSimplifier.rewrite_rule @{thms eq_reflection[OF id_apply] id_def_sym} t;
+  in
+    singleton (ProofContext.export lthy' lthy) t_id
+  end
+*}
 
 ML {*
 fun findaps_all rty tm =
@@ -976,6 +1002,23 @@
 
 
 ML {*
+fun find_aps_all rtm qtm =
+  case (rtm, qtm) of
+    (Abs(_, T1, s1), Abs(_, T2, s2)) =>
+      find_aps_all (subst_bound ((Free ("x", T1)), s1)) (subst_bound ((Free ("x", T2)), s2))
+  | (((f1 as (Free (_, T1))) $ a1), ((f2 as (Free (_, T2))) $ a2)) =>
+      let
+        val sub = (find_aps_all f1 f2) @ (find_aps_all a1 a2)
+      in
+        if T1 = T2 then sub else (T1, T2) :: sub
+      end
+  | ((f1 $ a1), (f2 $ a2)) => (find_aps_all f1 f2) @ (find_aps_all a1 a2)
+  | _ => [];
+
+fun find_aps rtm qtm = distinct (op =) (find_aps_all rtm qtm)
+*}
+
+ML {*
 (* FIXME: allex_prs and lambda_prs can be one function *)
 fun allex_prs_tac lthy quot =
   (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]})
@@ -1068,13 +1111,14 @@
 *}
 
 ML {*
-fun clean_tac lthy quot defs reps_same =
+fun clean_tac lthy quot defs reps_same absrep aps =
   let
     val lower = flat (map (add_lower_defs lthy) defs)
+    val aps_thms = map (applic_prs lthy absrep) aps
   in
     EVERY' [TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot), 
             lambda_prs_tac lthy quot,
-            (* TODO: cleaning according to app_prs *)
+            TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] aps_thms),
             TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower),
             simp_tac (HOL_ss addsimps [reps_same])]
   end
@@ -1165,30 +1209,40 @@
   @{thm procedure}
 end
 *}
-  
+
+(* Left for debugging *)
 ML {*
-fun procedure_tac rthm ctxt =
-  ObjectLogic.full_atomize_tac 
-  THEN' gen_frees_tac ctxt
+fun procedure_tac lthy rthm =
+  ObjectLogic.full_atomize_tac
+  THEN' gen_frees_tac lthy
   THEN' Subgoal.FOCUS (fn {context, concl, ...} =>
-          let
-            val rthm' = atomize_thm rthm
-            val rule = procedure_inst context (prop_of rthm') (Envir.beta_norm (term_of concl))
-          in
-           EVERY1 [rtac rule, rtac rthm']
-        end) ctxt
+    let
+      val rthm' = atomize_thm rthm
+      val rule = procedure_inst context (prop_of rthm') (term_of concl)
+    in
+      rtac rule THEN' rtac rthm'
+    end 1) lthy
 *}
 
 ML {*
-fun lift_tac lthy thm rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs =
-  procedure_tac thm lthy THEN'
-  RANGE [regularize_tac lthy rel_eqv rel_refl,
-         REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms), 
-         clean_tac lthy quot defs reps_same]
+fun lift_tac lthy rthm rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs =
+  ObjectLogic.full_atomize_tac
+  THEN' gen_frees_tac lthy
+  THEN' Subgoal.FOCUS (fn {context, concl, ...} =>
+    let
+      val rthm' = atomize_thm rthm
+      val rule = procedure_inst context (prop_of rthm') (term_of concl)
+      val aps = find_aps (prop_of rthm') (term_of concl)
+    in
+      rtac rule THEN' RANGE [
+        rtac rthm',
+        regularize_tac lthy rel_eqv rel_refl,
+        REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms),
+        clean_tac lthy quot defs reps_same absrep aps
+      ]
+    end 1) lthy
 *}
 
-
-
 end
 
 
diff -r 1dd6a21cdd1c -r 58947b7232ef quotient_def.ML
--- a/quotient_def.ML	Thu Nov 26 02:31:00 2009 +0100
+++ b/quotient_def.ML	Thu Nov 26 03:18:38 2009 +0100
@@ -55,6 +55,7 @@
    change *)
 
 fun get_fun flag lthy (rty, qty) =
+  if rty = qty then mk_identity qty else
   case (rty, qty) of 
     (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>
      let