# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269680195 -3600
# Node ID ba3f6e33d647233565e14055b8a58b1485dd8a03
# Parent  141a36535f1d25c3b632ad1936e60ca0c2a14361
Automatically compute support if only one type of Abs is present in the type.

diff -r 141a36535f1d -r ba3f6e33d647 Nominal/ExTySch.thy
--- a/Nominal/ExTySch.thy	Sat Mar 27 09:41:00 2010 +0100
+++ b/Nominal/ExTySch.thy	Sat Mar 27 09:56:35 2010 +0100
@@ -12,23 +12,7 @@
 and tyS =
   All xs::"name fset" ty::"t" bind xs in ty
 
-lemma t_tyS_supp_fv: "fv_t t = supp t \<and> fv_tyS tyS = supp tyS"
-apply (induct rule: t_tyS.induct)
-apply (simp_all only: t_tyS.fv)
-apply (simp_all only: supp_abs(2)[symmetric])
-apply(simp_all (no_asm) only: supp_def)
-apply(simp_all only: t_tyS.perm permute_abs)
-apply(simp only: t_tyS.eq_iff supp_at_base[simplified supp_def])
-apply(simp only: t_tyS.eq_iff Collect_disj_eq[symmetric] infinite_Un[symmetric])
-apply simp
-apply(simp only: Abs_eq_iff t_tyS.eq_iff)
-apply (simp add: alphas)
-apply (simp add: eqvts[symmetric])
-apply (simp add: eqvts eqvts_raw)
-done
-
-lemmas t_tyS_supp = t_tyS.fv[simplified t_tyS_supp_fv]
-
+lemmas t_tyS_supp = t_tyS.fv[simplified t_tyS.supp]
 
 lemma size_eqvt_raw:
   "size (pi \<bullet> t :: t_raw) = size t"
diff -r 141a36535f1d -r ba3f6e33d647 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Sat Mar 27 09:41:00 2010 +0100
+++ b/Nominal/Fv.thy	Sat Mar 27 09:56:35 2010 +0100
@@ -888,14 +888,32 @@
   apply blast
   done
 
+(* TODO: this is a hack, it assumes that only one type of Abs's is present
+   in the type and chooses this supp_abs *)
+ML {*
+fun choose_alpha_abs eqiff =
+let
+  fun exists_subterms f ts = true mem (map (exists_subterm f) ts);
+  val terms = map prop_of eqiff;
+  fun check cname = exists_subterms (fn x => fst(dest_Const x) = cname handle _ => false) terms
+  val no =
+    if check @{const_name alpha_gen} then 0 else
+    if check @{const_name alpha_res} then 1 else
+    if check @{const_name alpha_lst} then 2 else
+    error "Failure choosing supp_abs"
+in
+  nth @{thms supp_abs[symmetric]} no
+end
+*}
+
 ML {*
 fun supp_eq_tac ind fv perm eqiff ctxt =
   rel_indtac ind THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_abs[symmetric]}) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_basic_ss addsimps [choose_alpha_abs eqiff]) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps (@{thm permute_abs} :: perm)) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps (@{thms permute_abs} @ perm)) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps (@{thms Abs_eq_iff} @ eqiff)) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms alphas}) THEN_ALL_NEW