# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1294649511 0
# Node ID 33a6b690fb53fa598c7940914590d8ed53300ba3
# Parent  1c3ad1256f16f00d3f3e98367f5e57623badc8a1
added a property about finite support in the presense of eqvt_at

diff -r 1c3ad1256f16 -r 33a6b690fb53 Nominal/Ex/LamTest.thy
--- a/Nominal/Ex/LamTest.thy	Sun Jan 09 05:38:53 2011 +0000
+++ b/Nominal/Ex/LamTest.thy	Mon Jan 10 08:51:51 2011 +0000
@@ -12,6 +12,20 @@
 definition
  "eqvt_at f x \<equiv> \<forall>p. p \<bullet> (f x) = f (p \<bullet> x)"
 
+lemma supp_eqvt_at:
+  assumes asm: "eqvt_at f x"
+  and     fin: "finite (supp x)"
+  shows "supp (f x) \<subseteq> supp x"
+apply(rule supp_is_subset)
+unfolding supports_def
+unfolding fresh_def[symmetric]
+using asm
+apply(simp add: eqvt_at_def)
+apply(simp add: swap_fresh_fresh)
+apply(rule fin)
+done
+
+
 definition
  "eqvt f \<equiv> \<forall>p. p \<bullet> f = f"
 
@@ -500,6 +514,7 @@
 *}
 
 ML Thm.forall_elim_vars
+ML Thm.implies_intr
 
 ML {* (ex1_implies_ex, ex1_implies_un) *}
 thm fundef_ex1_eqvt_at