# HG changeset patch # User urbanc # Date 1130665077 -3600 # Node ID 3d643b13eb65acb9277fb2ffbec77a1700538565 # Parent b7389981170b657c32a0bf42520ed4c447228acb simplified the abs_supp_approx proof and tuned some comments in nominal_permeq.ML diff -r b7389981170b -r 3d643b13eb65 src/HOL/Nominal/Nominal.thy --- a/src/HOL/Nominal/Nominal.thy Sat Oct 29 15:01:25 2005 +0200 +++ b/src/HOL/Nominal/Nominal.thy Sun Oct 30 10:37:57 2005 +0100 @@ -2049,43 +2049,30 @@ qed qed --- "two helpers for the abst_supp_approx-lemma" -lemma finite_minus: - assumes a: "finite {b. P b}" - shows "finite {b. b \ x \ P b}" - using a by (force simp add: Collect_conj_eq) - -lemma infinite_minus: - assumes a: "infinite {b. P b}" - shows "infinite {b. b \ x \ P b}" -proof - - have "{b. b \ x \ P b}={b. P b}-{x}" by force - with a show ?thesis by force -qed - lemma abs_fun_supp_approx: fixes x :: "'a" 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 (unfold supp_def, auto simp only: abs_fun_pi[OF pt, OF at] at_calc[OF at] if_False) - fix c - assume a: "c\a" - assume "finite {b::'x. [(c, b)]\x \ x}" - hence f: "finite {b::'x. b\a \ [(c, b)]\x \ x}" by (rule finite_minus) - assume "infinite {b::'x. [(if (b=a) then c else a)].([(c,b)]\x) \ ([a].x)}" - hence "infinite {b::'x. b\a \ [(if (b=a) then c else a)].([(c,b)]\x) \ ([a].x)}" - by (rule infinite_minus) - hence i: "infinite {b::'x. b\a \ [a].([(c,b)]\x) \ ([a].x)}" - proof (auto split add: split_if_asm) - assume c1: "infinite {b::'x. b\a \ (b=a \ b\a \ [a].([(c,b)]\x) \ ([a].x))}" - assume c2: "finite {b::'x. b\a \ [a].([(c, b)]\x) \ ([a].x)}" - have "{b::'x. b\a \ (b=a \ b\a \ [a].([(c,b)]\x) \ ([a].x))} = - {b::'x. b\a \ [a].([(c,b)]\x) \ ([a].x)}" by force - with c1 c2 show False by simp - qed - from f i show False by (simp add: abs_fun_eq1) +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]) qed lemma abs_fun_finite_supp: @@ -2271,15 +2258,14 @@ by (simp add: perm_fun_def) - (***************************************) (* setup for the individial atom-kinds *) -(* and datatype *) +(* and nominal datatypes *) use "nominal_package.ML" setup "NominalPackage.setup" -(**********************************) -(* setup for induction principles *) +(*****************************************) +(* setup for induction principles method *) use "nominal_induct.ML"; method_setup nominal_induct = {* nominal_induct_method *} @@ -2295,7 +2281,7 @@ method_setup perm_simp_debug = {* perm_eq_meth_debug *} - {* tactic for deciding equalities involving permutations including debuging facilities*} + {* tactic for deciding equalities involving permutations including debuging facilities *} method_setup supports_simp = {* supports_meth *} @@ -2303,7 +2289,7 @@ method_setup supports_simp_debug = {* supports_meth_debug *} - {* tactic for deciding equalities involving permutations including debuging facilities*} + {* tactic for deciding equalities involving permutations including debuging facilities *} end