# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1307457732 -32400
# Node ID a4d6689504e27ae7bd085178909769223763864a
# Parent  44d937e8ae78c64aafdbbb4fc242da27f74ebf4e
remove garbage (proofs that assumes the invariant outside function)

diff -r 44d937e8ae78 -r a4d6689504e2 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Tue Jun 07 23:38:39 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Tue Jun 07 23:42:12 2011 +0900
@@ -472,61 +472,6 @@
 apply(simp add: fresh_star_def)
 done
 
-(* lemma helpr: "atom x \<sharp> ta \<Longrightarrow> Lam [xa]. ta = Lam [x]. ((xa \<leftrightarrow> x) \<bullet> ta)"
-  apply (case_tac "x = xa")
-  apply simp
-  apply (simp add: lam.eq_iff Abs1_eq_iff flip_def[symmetric])
-  by (metis atom_eqvt flip_at_simps(2) fresh_permute_iff)
-
-lemma supp_lookup: "supp (lookup l n name) = {atom name} - supp l"
-  apply (induct l arbitrary: n)
-  apply (simp_all add: ln.supp supp_at_base supp_Nil supp_Cons pure_supp)
-  done
-
-lemma trans_eqvt[eqvt]: "p \<bullet> (trans t l) = trans (p \<bullet> t) (p \<bullet> l)"
-  apply (induct t l rule: trans.induct)
-  apply simp_all
-  apply (simp add: eqvts permute_pure)
-  done
-
-lemma diff_un: "a - (b \<union> c) = a - b - c"
-  by blast
-
-lemma supp_trans: "supp (trans t l) = supp t - supp l"
-  apply (induct t arbitrary: l rule: lam.induct)
-  apply (simp_all add: lam.supp supp_at_base supp_lookup ln.supp)
-  apply blast
-  apply (rule_tac x="(lam, l)" and ?'a="name" in obtain_fresh)
-  apply (simp add: fresh_Pair)
-  apply clarify
-  apply (subgoal_tac "supp (Lambda.trans (Lam [a]. ((name \<leftrightarrow> a) \<bullet> lam)) l) =
-    supp lam - {atom name} - supp l")
-  using helpr
-  apply simp
-  apply (simp add: ln.supp)
-  apply (subgoal_tac "supp ((name \<leftrightarrow> a) \<bullet> (Lambda.trans lam ((name \<leftrightarrow> a) \<bullet> (a # l)))) = supp lam - {atom name} - supp l")
-  apply (simp add: trans_eqvt)
-  apply (simp add: supp_eqvt[symmetric])
-  apply (simp add: Diff_eqvt)
-  apply (simp add: supp_eqvt supp_Cons  union_eqvt)
-  apply (simp add: diff_un)
-  apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*})
-  apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*})
-  apply rule
-  prefer 2
-  apply rule
-  apply (simp add: supp_at_base)
-  apply (subgoal_tac "(name \<leftrightarrow> a) \<bullet> (supp lam - {atom name}) = supp lam - {atom name}")
-  apply (simp add: eqvts)
-  unfolding flip_def
-  apply (rule swap_fresh_fresh)
-apply (metis fresh_at_base fresh_def fresh_minus_atom_set lam.fsupp supp_at_base)
-by (metis fresh_def fresh_finite_atom_set fresh_minus_atom_set lam.fsupp)
-
-lemma "atom x \<sharp> trans_sumC (t, x # xsa)"
-  by (simp add: fresh_def meta_eq_to_obj_eq[OF trans_def, symmetric, unfolded fun_eq_iff] supp_trans supp_Cons supp_at_base)
-*)
-
 nominal_datatype db = 
   DBVar nat
 | DBApp db db