# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1339267699 -3600
# Node ID 3641530002d665b9d60834f9c2d2477e149a06e0
# Parent  ae1defecd8c00f32a742e95e0605532af02a1e95
added a rule about inequality of freshness between atoms to the simplifier

diff -r ae1defecd8c0 -r 3641530002d6 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Wed Jun 06 14:50:47 2012 +0100
+++ b/Nominal/Nominal2_Base.thy	Sat Jun 09 19:48:19 2012 +0100
@@ -2829,8 +2829,15 @@
   apply(simp_all add: supp_at_base)
   apply(metis)
   done
-  
-lemma fresh_atom_at_base: 
+
+(* solves the freshness only if the inequality can be shown by the
+   simproc below *)  
+lemma fresh_ineq_at_base [simp]:
+  shows "a \<noteq> atom b \<Longrightarrow> a \<sharp> b"
+  by (simp add: fresh_at_base)
+
+
+lemma fresh_atom_at_base [simp]: 
   fixes b::"'a::at_base"
   shows "a \<sharp> atom b \<longleftrightarrow> a \<sharp> b"
   by (simp add: fresh_def supp_at_base supp_atom)
@@ -2845,6 +2852,7 @@
   and   "atom a \<sharp> x \<Longrightarrow> P (if x = a then t else s) = P s"
 by (simp_all add: fresh_at_base)
 
+
 simproc_setup fresh_ineq ("x \<noteq> (y::'a::at_base)") = {* fn _ => fn ss => fn ctrm =>
   let
     fun first_is_neg lhs rhs [] = NONE