# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265182344 -3600
# Node ID bcf6e7d20c20a8d77eea9cebb15e1f0112732123
# Parent  07f97267a3921e2f62fcb7b35048f0bb362ae24a
More ingredients in Terms.

diff -r 07f97267a392 -r bcf6e7d20c20 Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Tue Feb 02 17:10:42 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 03 08:32:24 2010 +0100
@@ -100,10 +100,6 @@
 apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
 done
 
-lemma rfv_trm1_eqvt[eqvt]:
-  shows "(pi\<bullet>rfv_trm1 t) = rfv_trm1 (pi\<bullet>t)"
-  sorry
-
 (* Shouyld we derive it? But bv is given by the user? *)
 lemma bv1_eqvt[eqvt]:
   shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)"
@@ -112,8 +108,19 @@
 apply (rule atom_eqvt)
 done
 
+lemma rfv_trm1_eqvt[eqvt]:
+  shows "(pi\<bullet>rfv_trm1 t) = rfv_trm1 (pi\<bullet>t)"
+  apply (induct t)
+  apply (simp_all add: eqvts)
+  apply (rule atom_eqvt) 
+  apply (simp add: atom_eqvt) 
+  done
+
+
 lemma alpha1_eqvt:
   shows "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)"
+  apply (induct t s rule: alpha1.inducts)
+  apply (simp_all add:eqvts alpha1_inj)
   sorry
 
 lemma alpha1_equivp: "equivp alpha1" 
@@ -260,6 +267,34 @@
 unfolding alpha_gen apply (lifting alpha1_inj[unfolded alpha_gen])
 done
 
+lemma lm1_supp_pre:
+  shows "(supp (atom x, t)) supports (Lm1 x t) "
+apply(simp add: supports_def)
+apply(fold fresh_def)
+apply(simp add: fresh_Pair swap_fresh_fresh)
+apply(clarify)
+apply(subst swap_at_base_simps(3))
+apply(simp_all add: fresh_atom)
+done
+
+lemma lt1_supp_pre:
+  shows "(supp (x, t, s)) supports (Lt1 t x s) "
+apply(simp add: supports_def)
+apply(fold fresh_def)
+apply(simp add: fresh_Pair swap_fresh_fresh)
+done
+
+lemma bp_supp: "finite (supp (bp :: bp))"
+  apply (induct bp)
+  apply(simp_all add: supp_def)
+  apply (fold supp_def)
+  apply (simp add: supp_at_base)
+  apply(simp add: Collect_imp_eq)
+  apply(simp add: Collect_neg_eq[symmetric])
+  apply (fold supp_def)
+  apply (simp)
+  done
+
 instance trm1 :: fs
 apply default
 apply(induct_tac x rule: trm1_bp_inducts(1))
@@ -268,8 +303,13 @@
 apply(simp add: supp_def[symmetric] supp_at_base)
 apply(simp only: supp_def alpha1_INJ eqvts permute_trm1)
 apply(simp add: Collect_imp_eq Collect_neg_eq)
-sorry
-
+apply(rule supports_finite)
+apply(rule lm1_supp_pre)
+apply(simp add: supp_Pair supp_atom)
+apply(rule supports_finite)
+apply(rule lt1_supp_pre)
+apply(simp add: supp_Pair supp_atom bp_supp)
+done
 
 lemma supp_fv:
   shows "supp t = fv_trm1 t"
@@ -296,8 +336,6 @@
 apply(simp add: Collect_imp_eq Collect_neg_eq)
 done
 
-
-
 section {*** lets with single assignments ***}
 
 datatype trm2 =