# HG changeset patch # User urbanc # Date 1141836895 -3600 # Node ID a45baf1ac094e3f5ec29c238fd7673f03e725415 # Parent 03abed544f1e007376f0d6fa570b4d3120e451d0 tuned some of the proofs about fresh_fun diff -r 03abed544f1e -r a45baf1ac094 src/HOL/Nominal/Nominal.thy --- a/src/HOL/Nominal/Nominal.thy Wed Mar 08 17:23:46 2006 +0100 +++ b/src/HOL/Nominal/Nominal.thy Wed Mar 08 17:54:55 2006 +0100 @@ -1488,7 +1488,7 @@ hence "\a. a\(supp x) \ a\S" by force then obtain a where b1: "a\supp x" and b2: "a\S" by force from a1 b2 have "\b. (b\S \ ([(a,b)]\x = x))" by (unfold "op supports_def", force) - with a1 have "{b. [(a,b)]\x \ x}\S" by (unfold "op supports_def", force) + hence "{b. [(a,b)]\x \ x}\S" by force with a2 have "finite {b. [(a,b)]\x \ x}" by (simp add: finite_subset) hence "a\(supp x)" by (unfold supp_def, auto) with b1 show False by simp @@ -2140,37 +2140,6 @@ with b show "fr = h a" by force qed - -lemma fresh_fun_supports: - fixes h :: "'x\'a" - assumes pt: "pt TYPE('a) TYPE('x)" - and at: "at TYPE('x)" - and f1: "finite ((supp h)::'x set)" - and a: "\(a::'x). (a\h \ a\(h a))" - shows "((supp h)::'x set) supports (fresh_fun h)" - apply(simp add: "op supports_def") - apply(fold fresh_def) - apply(auto) - apply(subgoal_tac "\(a''::'x). a''\(h,a,b)")(*A*) - apply(erule exE) - apply(simp add: fresh_prod) - apply(auto) - apply(rotate_tac 2) - apply(drule fresh_fun_app[OF pt, OF at, OF f1, OF a]) - apply(simp add: at_fresh[OF at]) - apply(simp add: pt_fun_app_eq[OF at_pt_inst[OF at], OF at]) - apply(auto simp add: at_calc[OF at]) - apply(subgoal_tac "[(a, b)]\h = h")(*B*) - apply(simp) - (*B*) - apply(rule pt_fresh_fresh[OF pt_fun_inst[OF at_pt_inst[OF at], OF pt], OF at, OF at]) - apply(assumption)+ - (*A*) - apply(rule at_exists_fresh[OF at]) - apply(simp add: supp_prod) - apply(simp add: f1 at_supp[OF at]) - done - lemma fresh_fun_equiv: fixes h :: "'x\'a" and pi:: "'x prm" @@ -2200,6 +2169,19 @@ have d2: "?RHS = (pi\h) (pi\a')" using c3 a2 by (simp add: fresh_fun_app[OF pta, OF at, OF f2]) show ?thesis using d1 d2 by (simp add: pt_fun_app_eq[OF ptb, OF at]) qed + +lemma fresh_fun_supports: + fixes h :: "'x\'a" + assumes pt: "pt TYPE('a) TYPE('x)" + and at: "at TYPE('x)" + and f1: "finite ((supp h)::'x set)" + and a: "\(a::'x). (a\h \ a\(h a))" + shows "((supp h)::'x set) supports (fresh_fun h)" + apply(simp add: "op supports_def" fresh_def[symmetric]) + apply(auto) + apply(simp add: fresh_fun_equiv[OF pt, OF at, OF f1, OF a]) + apply(simp add: pt_fresh_fresh[OF pt_fun_inst[OF at_pt_inst[OF at], OF pt], OF at, OF at]) + done section {* disjointness properties *} (*=================================*)