# HG changeset patch
# User Cezary Kaliszyk <cezarykaliszyk@gmail.com>
# Date 1333010229 -7200
# Node ID 319964ecf1f6a01efaf75a81a1fcf2d6854247f9
# Parent  5179ff4806c5267928a666afb1d76bbc387a2d26
Change definition of Aux to include alpha-convertibility for non-closed terms.

diff -r 5179ff4806c5 -r 319964ecf1f6 Nominal/Ex/AuxNoFCB.thy
--- a/Nominal/Ex/AuxNoFCB.thy	Tue Mar 27 14:56:06 2012 +0200
+++ b/Nominal/Ex/AuxNoFCB.thy	Thu Mar 29 10:37:09 2012 +0200
@@ -8,7 +8,7 @@
 | Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)
 
 nominal_primrec lam2_rec where
-  "lam2_rec faa fll xs (Var n) (Var m) = ((n, m) \<in> set xs)"
+  "lam2_rec faa fll xs (Var n) (Var m) = (n = m \<or> (n, m) \<in> set xs)"
 | "lam2_rec faa fll xs (Var n) (App l r) = False"
 | "lam2_rec faa fll xs (Var n) (Lam [x]. t) = False"
 | "lam2_rec faa fll xs (App l r) (Var n) = False"
@@ -117,8 +117,8 @@
 termination (eqvt)
   by (relation "measure (\<lambda>(l, r, xs). size l + size r)") simp_all
 
-lemma aux_simps:
-  "aux (Var x) (Var y) xs = ((x, y) \<in> set xs)"
+lemma aux_simps[simp]:
+  "aux (Var x) (Var y) xs = (x = y \<or> (x, y) \<in> set xs)"
   "aux (App t1 t2) (App s1 s2) xs = (aux t1 s1 xs \<and> aux t2 s2 xs)"
   "aux (Var x) (App t1 t2) xs = False"
   "aux (Var x) (Lam [y].t) xs = False"