# HG changeset patch # User urbanc # Date 1130666156 -3600 # Node ID 7003308ff73a9f71186e951432b9823e72e8f0fa # Parent 3d643b13eb65acb9277fb2ffbec77a1700538565 tuned my last commit diff -r 3d643b13eb65 -r 7003308ff73a src/HOL/Nominal/Nominal.thy --- a/src/HOL/Nominal/Nominal.thy Sun Oct 30 10:37:57 2005 +0100 +++ b/src/HOL/Nominal/Nominal.thy Sun Oct 30 10:55:56 2005 +0100 @@ -2054,25 +2054,16 @@ and a :: "'x" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" - shows "((supp ([a].x))::'x set) \ (supp x)\{a}" -proof - - have "((supp ([a].x))::'x set) \ (supp (x,a))" - proof - fix c - assume "c\((supp ([a].x))::'x set)" - hence "infinite {b. [(c,b)]\([a].x) \ [a].x}" by (simp add: supp_def) - hence "infinite {b. [([(c,b)]\a)].([(c,b)]\x) \ [a].x}" by (simp add: abs_fun_pi[OF pt, OF at]) - moreover - have "{b. [([(c,b)]\a)].([(c,b)]\x) \ [a].x} \ {b. ([(c,b)]\x,[(c,b)]\a) \ (x, a)}" - apply(rule subsetI) - apply(simp only: mem_Collect_eq) - apply(auto) - done - (*by force*) - ultimately have "infinite {b. ([(c,b)]\x,[(c,b)]\a) \ (x, a)}" by (simp add: infinite_super) - thus "c\(supp (x,a))" by (simp add: supp_def) - qed - thus ?thesis by (simp add: supp_prod at_supp[OF at]) + shows "((supp ([a].x))::'x set) \ (supp (x,a))" +proof + fix c + assume "c\((supp ([a].x))::'x set)" + hence "infinite {b. [(c,b)]\([a].x) \ [a].x}" by (simp add: supp_def) + hence "infinite {b. [([(c,b)]\a)].([(c,b)]\x) \ [a].x}" by (simp add: abs_fun_pi[OF pt, OF at]) + moreover + have "{b. [([(c,b)]\a)].([(c,b)]\x) \ [a].x} \ {b. ([(c,b)]\x,[(c,b)]\a) \ (x, a)}" by force + ultimately have "infinite {b. ([(c,b)]\x,[(c,b)]\a) \ (x, a)}" by (simp add: infinite_super) + thus "c\(supp (x,a))" by (simp add: supp_def) qed lemma abs_fun_finite_supp: @@ -2083,9 +2074,10 @@ and f: "finite ((supp x)::'x set)" shows "finite ((supp ([a].x))::'x set)" proof - - from f have f1: "finite (((supp x)::'x set)\{a})" by force - thus ?thesis using abs_fun_supp_approx[OF pt, OF at, of "a" "x"] - by (simp add: finite_subset) + from f have "finite ((supp (x,a))::'x set)" by (simp add: supp_prod at_supp[OF at]) + moreover + have "((supp ([a].x))::'x set) \ (supp (x,a))" by (rule abs_fun_supp_approx[OF pt, OF at]) + ultimately show ?thesis by (simp add: finite_subset) qed lemma fresh_abs_funI1: @@ -2192,8 +2184,7 @@ shows "supp ([a].x) = (supp x)-{a}" by (force simp add: supp_fresh_iff fresh_abs_fun_iff[OF pt, OF at, OF f]) -(* maybe needs to be stated by supp -supp *) - +(* maybe needs to be better stated as supp intersection supp *) lemma abs_fun_supp_ineq: fixes a :: "'y" and x :: "'a" @@ -2221,8 +2212,8 @@ shows "b\([a].x) = b\x" by (simp add: fresh_def abs_fun_supp_ineq[OF pta, OF ptb, OF at, OF cp, OF dj]) -section {* abstraction type for the datatype package (not really needed anymore) *} -(*===============================================================================*) +section {* abstraction type for the parsing in nominal datatype *} +(*==============================================================*) consts "ABS_set" :: "('x\('a nOption)) set" inductive ABS_set @@ -2238,7 +2229,7 @@ syntax ABS :: "type \ type \ type" ("\_\_" [1000,1000] 1000) -section {* Lemmas for Deciding Permutation Equations *} +section {* lemmas for deciding permutation equations *} (*===================================================*) lemma perm_eq_app: