# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1338462073 -3600
# Node ID 5335c0ea743aec641a3686669ed18a7a72079cc3
# Parent  ca162f0a7957f93146e2144f05e8c4707ecaaf86# Parent  9eeea01bdbc0eecf92ea7923dd8bc983c2decd40
merged

diff -r 9eeea01bdbc0 -r 5335c0ea743a Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Thu May 31 12:44:37 2012 +0200
+++ b/Nominal/Ex/Lambda.thy	Thu May 31 12:01:13 2012 +0100
@@ -299,13 +299,13 @@
 lemma forget:
   shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"
   by (nominal_induct t avoiding: x s rule: lam.strong_induct)
-     (auto simp add: lam.fresh fresh_at_base)
+     (auto simp add: fresh_at_base)
 
 text {* same lemma but with subst.induction *}
 lemma forget2:
   shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"
   by (induct t x s rule: subst.induct)
-     (auto simp add: lam.fresh fresh_at_base fresh_Pair)
+     (auto simp add:  fresh_at_base fresh_Pair)
 
 lemma fresh_fact:
   fixes z::"name"
@@ -314,7 +314,7 @@
   shows "atom z \<sharp> t[y ::= s]"
   using a b
   by (nominal_induct t avoiding: z y s rule: lam.strong_induct)
-      (auto simp add: lam.fresh fresh_at_base)
+      (auto simp add:  fresh_at_base)
 
 lemma substitution_lemma:  
   assumes a: "x \<noteq> y" "atom x \<sharp> u"
@@ -328,7 +328,7 @@
   shows "t[x ::= s] = ((y \<leftrightarrow> x) \<bullet>t)[y ::= s]"
 using a 
 apply (nominal_induct t avoiding: x y s rule: lam.strong_induct)
-apply (auto simp add: lam.fresh fresh_at_base)
+apply (auto simp add:  fresh_at_base)
 done
 
 lemma height_ge_one:
@@ -368,7 +368,7 @@
 
 nominal_inductive beta
   avoids b4: "x"
-  by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)
+  by (simp_all add: fresh_star_def fresh_Pair  fresh_fact)
 
 text {* One-Reduction *}
 
@@ -385,7 +385,7 @@
 nominal_inductive One 
   avoids o3: "x"
       |  o4: "x"
-  by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)
+  by (simp_all add: fresh_star_def fresh_Pair  fresh_fact)
 
 lemma One_refl:
   shows "t \<longrightarrow>1 t"
@@ -610,7 +610,7 @@
 
 lemma var_fresh_subst:
   "atom x \<sharp> s \<Longrightarrow> atom x \<sharp> (t[x ::= s])"
-  by (induct t x s rule: subst.induct) (auto simp add: lam.supp lam.fresh fresh_at_base)
+  by (induct t x s rule: subst.induct) (auto simp add: lam.supp  fresh_at_base)
 
 (* function that evaluates a lambda term *)
 nominal_primrec
@@ -841,7 +841,7 @@
   apply(drule_tac x="namea" in meta_spec)
   apply(drule_tac x="lam" in meta_spec)
   apply(simp add: fresh_star_Pair)
-  apply(simp add: fresh_star_def fresh_at_base lam.fresh)
+  apply(simp add: fresh_star_def fresh_at_base )
   apply(auto)[1]
   apply(simp_all)[44]
   apply(simp del: Product_Type.prod.inject)  
@@ -880,7 +880,7 @@
   apply(drule_tac x="name" in meta_spec)
   apply(drule_tac x="lam" in meta_spec)
   apply(drule_tac x="(name \<leftrightarrow> namea) \<bullet> lama" in meta_spec)
-  apply(simp add: Abs1_eq_iff fresh_star_def fresh_Pair_elim fresh_at_base lam.fresh flip_def)
+  apply(simp add: Abs1_eq_iff fresh_star_def fresh_Pair_elim fresh_at_base flip_def)
   apply (metis Nominal2_Base.swap_commute fresh_permute_iff sort_of_atom_eq swap_atom_simps(2))
   apply simp_all
   apply (simp add: abs_same_binder)
diff -r 9eeea01bdbc0 -r 5335c0ea743a Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Thu May 31 12:44:37 2012 +0200
+++ b/Nominal/Nominal2.thy	Thu May 31 12:01:13 2012 +0100
@@ -522,7 +522,7 @@
      ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms)
      ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms)
      ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs)
-     ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs)
+     ||>> Local_Theory.note ((thms_suffix "fresh", [simp_attr]), qfresh_constrs)
      ||>> Local_Theory.note ((thms_suffix "perm_bn_simps", []), qperm_bn_simps)
      ||>> Local_Theory.note ((thms_suffix "bn_finite", []), qbn_finite_thms)
      ||>> Local_Theory.note ((thms_suffix "perm_bn_alpha", []), qperm_bn_alpha_thms)
diff -r 9eeea01bdbc0 -r 5335c0ea743a Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Thu May 31 12:44:37 2012 +0200
+++ b/Nominal/Nominal2_Base.thy	Thu May 31 12:01:13 2012 +0100
@@ -876,6 +876,10 @@
   shows "p \<bullet> (if b then x else y) = (if p \<bullet> b then p \<bullet> x else p \<bullet> y)"
   by (simp add: permute_fun_def permute_bool_def)
 
+lemma Let_eqvt [eqvt]:
+  shows "p \<bullet> Let x y = Let (p \<bullet> x) (p \<bullet> y)"
+  unfolding Let_def permute_fun_app_eq ..
+
 lemma True_eqvt [eqvt]:
   shows "p \<bullet> True = True"
   unfolding permute_bool_def ..
diff -r 9eeea01bdbc0 -r 5335c0ea743a Nominal/Nominal2_Base_Exec.thy
--- a/Nominal/Nominal2_Base_Exec.thy	Thu May 31 12:44:37 2012 +0200
+++ b/Nominal/Nominal2_Base_Exec.thy	Thu May 31 12:01:13 2012 +0100
@@ -796,6 +796,10 @@
   shows "p \<bullet> (if b then x else y) = (if p \<bullet> b then p \<bullet> x else p \<bullet> y)"
   by (simp add: permute_fun_def permute_bool_def)
 
+lemma Let_eqvt [eqvt]:
+  shows "p \<bullet> Let x y = Let (p \<bullet> x) (p \<bullet> y)"
+  unfolding Let_def permute_fun_app_eq ..
+
 lemma True_eqvt [eqvt]:
   shows "p \<bullet> True = True"
   unfolding permute_bool_def ..