# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1256909137 -3600
# Node ID 60acf3d3a4a0bca761d78bb84ecbc38c1a21c98e
# Parent  6cff34032a005a71d46a4f40ac90db923524d1af
Finding applications and duplicates filtered out in abstractions

diff -r 6cff34032a00 -r 60acf3d3a4a0 FSet.thy
--- a/FSet.thy	Fri Oct 30 12:22:03 2009 +0100
+++ b/FSet.thy	Fri Oct 30 14:25:37 2009 +0100
@@ -295,6 +295,7 @@
   ((map f a) ::'a list) @ (map f b)"
  by simp (rule list_eq_refl)
 
+
 ML {* val qty = @{typ "'a fset"} *}
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val (trans2, reps_same, quot) = lookup_quot_thms @{context} "fset" *}
@@ -342,7 +343,10 @@
   repabs @{context} ind_r_r consts rty qty quot rel_refl trans2 rsp_thms
   )
 *}
+
 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_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *}
 ML {* val ind_r_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms ind_r_t *}
 lemma app_prs_for_induct: "(ABS_fset ---> id) f (REP_fset T1) = f T1"
diff -r 6cff34032a00 -r 60acf3d3a4a0 QuotMain.thy
--- a/QuotMain.thy	Fri Oct 30 12:22:03 2009 +0100
+++ b/QuotMain.thy	Fri Oct 30 14:25:37 2009 +0100
@@ -903,19 +903,31 @@
   end
 *}
 
-text {* the proper way to do it *}
 ML {*
-  fun findabs rty tm =
+  fun findabs_all rty tm =
     case tm of
       Abs(_, T, b) =>
         let
           val b' = subst_bound ((Free ("x", T)), b);
-          val tys = findabs rty b'
+          val tys = findabs_all rty b'
           val ty = fastype_of tm
         in if needs_lift rty ty then (ty :: tys) else tys
         end
-    | f $ a => (findabs rty f) @ (findabs rty a)
-    | _ => []
+    | f $ a => (findabs_all rty f) @ (findabs_all rty a)
+    | _ => [];
+  fun findabs rty tm = distinct (op =) (findabs_all rty tm)
+*}
+
+
+ML {*
+  fun findaps_all rty tm =
+    case tm of
+      Abs(_, T, b) =>
+        findaps_all rty (subst_bound ((Free ("x", T)), b))
+    | (f $ a) => (findaps_all rty f @ findaps_all rty a)
+    | Free (_, (T as (Type (_, (_ :: _))))) => (if needs_lift rty T then [T] else [])
+    | _ => [];
+  fun findaps rty tm = distinct (op =) (findaps_all rty tm)
 *}
 
 ML {*