# HG changeset patch # User urbanc # Date 1217182096 -7200 # Node ID 224a18d1a3acd94632c45a735cf58cdd7bfbc8a8 # Parent d1dbe31655be88ea739f732f7bfe600acc4ac015 simplified a proof diff -r d1dbe31655be -r 224a18d1a3ac src/HOL/Nominal/Nominal.thy --- a/src/HOL/Nominal/Nominal.thy Sat Jul 26 09:00:26 2008 +0200 +++ b/src/HOL/Nominal/Nominal.thy Sun Jul 27 20:08:16 2008 +0200 @@ -1743,29 +1743,17 @@ shows "pi\(c\x) = (pi\c)\(pi\x)" by (simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj] perm_bool) --- "three helper lemmas for the perm_fresh_fresh-lemma" -lemma comprehension_neg_UNIV: "{b. \ P b} = UNIV - {b. P b}" - by (auto) - -lemma infinite_or_neg_infinite: - assumes h:"infinite (UNIV::'a set)" - shows "infinite {b::'a. P b} \ infinite {b::'a. \ P b}" -proof (subst comprehension_neg_UNIV, case_tac "finite {b. P b}") - assume j:"finite {b::'a. P b}" - have "infinite ((UNIV::'a set) - {b::'a. P b})" - using Diff_infinite_finite[OF j h] by auto - thus "infinite {b::'a. P b} \ infinite (UNIV - {b::'a. P b})" .. -next - assume j:"infinite {b::'a. P b}" - thus "infinite {b::'a. P b} \ infinite (UNIV - {b::'a. P b})" by simp -qed - --"the co-set of a finite set is infinte" lemma finite_infinite: assumes a: "finite {b::'x. P b}" and b: "infinite (UNIV::'x set)" shows "infinite {b. \P b}" - using a and infinite_or_neg_infinite[OF b] by simp +proof - + from a b have "infinite (UNIV - {b::'x. P b})" by (simp add: Diff_infinite_finite) + moreover + have "{b::'x. \P b} = UNIV - {b::'x. P b}" by auto + ultimately show "infinite {b::'x. \P b}" by simp +qed lemma pt_fresh_fresh: fixes x :: "'a"