# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1268823236 -3600
# Node ID 1ea4ca823266448fbf691c334fd4134825c993ba
# Parent  b4216d0e109a99e57a3eace6aa9621b533b51942
added proof of supp/fv for type schemes

diff -r b4216d0e109a -r 1ea4ca823266 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Wed Mar 17 10:34:25 2010 +0100
+++ b/Nominal/Abs.thy	Wed Mar 17 11:53:56 2010 +0100
@@ -300,31 +300,38 @@
   apply(simp_all)
   done
 
-lemma supp_Abs_subset1:
-  fixes x::"'a::fs"
+lemma finite_supp_Abs_subset1:
+  assumes "finite (supp x)"
   shows "(supp x) - as \<subseteq> supp (Abs as x)"
   apply(simp add: supp_conv_fresh)
   apply(auto)
   apply(drule_tac supp_Abs_fun_fresh)
   apply(simp only: supp_Abs_fun_simp)
   apply(simp add: fresh_def)
-  apply(simp add: supp_finite_atom_set finite_supp)
+  apply(simp add: supp_finite_atom_set assms)
   done
 
-lemma supp_Abs_subset2:
-  fixes x::"'a::fs"
+lemma finite_supp_Abs_subset2:
+  assumes "finite (supp x)"
   shows "supp (Abs as x) \<subseteq> (supp x) - as"
   apply(rule supp_is_subset)
   apply(rule Abs_supports)
-  apply(simp add: finite_supp)
+  apply(simp add: assms)
+  done
+
+lemma finite_supp_Abs:
+  assumes "finite (supp x)"
+  shows "supp (Abs as x) = (supp x) - as"
+  apply(rule_tac subset_antisym)
+  apply(rule finite_supp_Abs_subset2[OF assms])
+  apply(rule finite_supp_Abs_subset1[OF assms])
   done
 
 lemma supp_Abs:
   fixes x::"'a::fs"
   shows "supp (Abs as x) = (supp x) - as"
-  apply(rule_tac subset_antisym)
-  apply(rule supp_Abs_subset2)
-  apply(rule supp_Abs_subset1)
+  apply(rule finite_supp_Abs)
+  apply(simp add: finite_supp)
   done
 
 instance abs :: (fs) fs
diff -r b4216d0e109a -r 1ea4ca823266 Nominal/Test.thy
--- a/Nominal/Test.thy	Wed Mar 17 10:34:25 2010 +0100
+++ b/Nominal/Test.thy	Wed Mar 17 11:53:56 2010 +0100
@@ -107,6 +107,44 @@
 
 thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]]
 
+lemma supports_lam_bp:
+  "(supp (atom a)) supports (VAR a)"
+  "(supp t \<union> supp s) supports (APP t s)"
+  "(supp (atom a) \<union> supp t) supports (LAM a t)"
+  "(supp b \<union> supp t) supports (LET b t)"
+  "(supp (atom a) \<union> supp t) supports (BP a t)"
+apply -
+apply(tactic {* supports_tac @{thms lam_bp_perm} 1 *})
+apply(tactic {* supports_tac @{thms lam_bp_perm} 1 *})
+apply(tactic {* supports_tac @{thms lam_bp_perm} 1 *})
+apply(tactic {* supports_tac @{thms lam_bp_perm} 1 *})
+apply(tactic {* supports_tac @{thms lam_bp_perm} 1 *})
+done
+
+lemma finite_supp_lam_bp:
+  fixes lam::"lam" 
+  and   bp::"bp"
+  shows "finite (supp lam)"
+  and   "finite (supp bp)"
+apply(induct lam and bp rule: lam_bp_inducts)
+apply(rule supports_finite)
+apply(rule supports_lam_bp)
+apply(simp add: supp_atom)
+apply(rule supports_finite)
+apply(rule supports_lam_bp)
+apply(simp)
+apply(rule supports_finite)
+apply(rule supports_lam_bp)
+apply(simp add: supp_atom)
+apply(rule supports_finite)
+apply(rule supports_lam_bp)
+apply(simp)
+apply(rule supports_finite)
+apply(rule supports_lam_bp)
+apply(simp add: supp_atom)
+done
+
+
 ML {* val _ = cheat_alpha_eqvt := true *}
 ML {* val _ = recursive := true *}
 
@@ -335,6 +373,23 @@
 ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *}
 ML {* Sign.of_sort @{theory} (@{typ tyS}, @{sort fs}) *}
 
+lemma supports_subset:
+  fixes S1 S2 :: "atom set"
+  assumes  a: "S1 supports x"
+  and      b: "S1 \<subseteq> S2"
+  shows "S2 supports x"
+  using a b
+  by (auto simp add: supports_def)
+
+lemma finite_fv_t_tyS:
+  fixes T::"t"
+  and   S::"tyS"
+  shows "finite (fv_t T)" 
+  and   "finite (fv_tyS S)"
+apply(induct T and S rule: t_tyS_inducts)
+apply(simp_all add: t_tyS_fv)
+done
+
 lemma supp_fv_t_tyS:
   shows "supp T = fv_t T" 
   and   "supp S = fv_tyS S"
@@ -365,9 +420,11 @@
 apply(simp only: alpha_gen)
 apply(simp only: supp_eqvt[symmetric])
 apply(simp only: eqvts)
-oops
-(*apply(simp only: supp_Abs)
-done*)
+apply(rule trans)
+apply(rule finite_supp_Abs)
+apply(simp add: finite_fv_t_tyS)
+apply(simp)
+done
 
 (* example 1 from Terms.thy *)