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"