# HG changeset patch # User urbanc # Date 1133064043 -3600 # Node ID 3b808e24667b8b4e08f6ba12c95f7ade75d1b33d # Parent 7f75925498da6a0d5794f8118a74a82ab6bba21c added the version of nominal.thy that contains all properties about support of finite sets diff -r 7f75925498da -r 3b808e24667b src/HOL/Nominal/Nominal.thy --- a/src/HOL/Nominal/Nominal.thy Sun Nov 27 04:59:20 2005 +0100 +++ b/src/HOL/Nominal/Nominal.thy Sun Nov 27 05:00:43 2005 +0100 @@ -5,7 +5,7 @@ uses ("nominal_atoms.ML") ("nominal_package.ML") -(* ("nominal_induct.ML") *) + ("nominal_induct.ML") ("nominal_permeq.ML") begin @@ -26,6 +26,10 @@ defs (overloaded) perm_set_def: "pi\(X::'a set) \ {pi\a | a. a\X}" +lemma perm_union: + shows "pi \ (X \ Y) = (pi \ X) \ (pi \ Y)" + by (auto simp add: perm_set_def) + (* permutation on units and products *) primrec (perm_unit) "pi\() = ()" @@ -68,6 +72,10 @@ perm_true_def: "pi\True = True" perm_false_def: "pi\False = False" +lemma perm_bool: + shows "pi\(b::bool) = b" + by (cases "b", auto) + (* permutation on options *) primrec (perm_option) perm_some_def: "pi\Some(x) = Some(pi\x)" @@ -121,6 +129,14 @@ shows "supp () = {}" by (simp add: supp_def) +lemma supp_set_empty: + shows "supp {} = {}" + by (force simp add: supp_def perm_set_def) + +lemma supp_singleton: + shows "supp {x} = supp x" + by (force simp add: supp_def perm_set_def) + lemma supp_prod: fixes x :: "'a" and y :: "'b" @@ -175,6 +191,10 @@ apply(simp add: supp_def perm_int_def) done +lemma fresh_set_empty: + shows "a\{}" + by (simp add: fresh_def supp_set_empty) + lemma fresh_prod: fixes a :: "'x" and x :: "'a" @@ -184,7 +204,7 @@ lemma fresh_list_nil: fixes a :: "'x" - shows "a\([]::'a list)" + shows "a\[]" by (simp add: fresh_def supp_list_nil) lemma fresh_list_cons: @@ -220,6 +240,7 @@ apply(simp add: fresh_def supp_some) done + section {* Abstract Properties for Permutations and Atoms *} (*=========================================================*) @@ -911,6 +932,16 @@ shows "(pi\x)\(pi\X)" using a by (simp add: pt_set_bij[OF pt, OF at]) +lemma pt_set_bij2a: + fixes pi :: "'x prm" + and x :: "'a" + and X :: "'a set" + assumes pt: "pt TYPE('a) TYPE('x)" + and at: "at TYPE('x)" + and a: "x\((rev pi)\X)" + shows "(pi\x)\X" + using a by (simp add: pt_set_bij1[OF pt, OF at]) + lemma pt_set_bij3: fixes pi :: "'x prm" and x :: "'a" @@ -943,13 +974,6 @@ thus "x\(pi\Y)" by (force simp add: pt_set_bij1a[OF pt, OF at]) qed -lemma pt_list_set_pi: - fixes pi :: "'x prm" - and xs :: "'a list" - assumes pt: "pt TYPE('a) TYPE('x)" - shows "pi\(set xs) = set (pi\xs)" -by (induct xs, auto simp add: perm_set_def pt1[OF pt]) - -- "some helper lemmas for the pt_perm_supp_ineq lemma" lemma Collect_permI: fixes pi :: "'x prm" @@ -1296,18 +1320,6 @@ using a b by (force simp add: "op supports_def") -lemma supp_supports: - fixes x :: "'a" - assumes pt: "pt TYPE('a) TYPE('x)" - and at: "at TYPE ('x)" - shows "((supp x)::'x set) supports x" -proof (unfold "op supports_def", intro strip) - fix a b - assume "(a::'x)\(supp x) \ (b::'x)\(supp x)" - hence "a\x" and "b\x" by (auto simp add: fresh_def) - thus "[(a,b)]\x = x" by (rule pt_fresh_fresh[OF pt, OF at]) -qed - lemma supp_is_subset: fixes S :: "'x set" and x :: "'a" @@ -1325,6 +1337,18 @@ with b1 show False by simp qed +lemma supp_supports: + fixes x :: "'a" + assumes pt: "pt TYPE('a) TYPE('x)" + and at: "at TYPE ('x)" + shows "((supp x)::'x set) supports x" +proof (unfold "op supports_def", intro strip) + fix a b + assume "(a::'x)\(supp x) \ (b::'x)\(supp x)" + hence "a\x" and "b\x" by (auto simp add: fresh_def) + thus "[(a,b)]\x = x" by (rule pt_fresh_fresh[OF pt, OF at]) +qed + lemma supports_finite: fixes S :: "'x set" and x :: "'a" @@ -1516,7 +1540,7 @@ have "x#xs = [x]@xs" by simp hence "(x#xs)\y = ([x]@xs)\y" by simp hence "(x#xs)\y = [x]\(xs\y)" by (simp only: pt2[OF pt]) - thus ?case using a i p by (force) + thus ?case using a i p by force qed lemma pt_swap_eq: @@ -1633,6 +1657,231 @@ from a1 a2 a3 show False by (force dest: finite_subset) qed +section {* Facts about the support of finite sets of finitely supported things *} +(*=============================================================================*) + +constdefs + X_to_Un_supp :: "('a set) \ 'x set" + "X_to_Un_supp X \ \x\X. ((supp x)::'x set)" + +lemma UNION_f_eqvt: + fixes X::"('a set)" + and f::"'a \ 'x set" + and pi::"'x prm" + assumes pt: "pt TYPE('a) TYPE('x)" + and at: "at TYPE('x)" + shows "pi\(\x\X. f x) = (\x\(pi\X). (pi\f) x)" +proof - + have pt_x: "pt TYPE('x) TYPE('x)" by (force intro: at_pt_inst at) + show ?thesis + apply(auto simp add: perm_set_def) + apply(rule_tac x="pi\xa" in exI) + apply(rule conjI) + apply(rule_tac x="xa" in exI) + apply(simp) + apply(subgoal_tac "(pi\f) (pi\xa) = pi\(f xa)")(*A*) + apply(simp) + apply(rule pt_set_bij2[OF pt_x, OF at]) + apply(assumption) + apply(rule sym) + apply(rule pt_fun_app_eq[OF pt, OF at]) + apply(rule_tac x="(rev pi)\x" in exI) + apply(rule conjI) + apply(rule sym) + apply(rule pt_pi_rev[OF pt_x, OF at]) + apply(rule_tac x="a" in bexI) + apply(simp add: pt_set_bij1[OF pt_x, OF at]) + apply(simp add: pt_fun_app_eq[OF pt, OF at]) + apply(assumption) + done +qed + +lemma X_to_Un_supp_eqvt: + fixes X::"('a set)" + and pi::"'x prm" + assumes pt: "pt TYPE('a) TYPE('x)" + and at: "at TYPE('x)" + shows "pi\(X_to_Un_supp X) = ((X_to_Un_supp (pi\X))::'x set)" + apply(simp add: X_to_Un_supp_def) + apply(simp add: UNION_f_eqvt[OF pt, OF at] perm_fun_def) + apply(simp add: pt_perm_supp[OF pt, OF at]) + apply(simp add: pt_pi_rev[OF pt, OF at]) + done + +lemma Union_supports_set: + fixes X::"('a set)" + assumes pt: "pt TYPE('a) TYPE('x)" + and at: "at TYPE('x)" + shows "(\x\X. ((supp x)::'x set)) supports X" + apply(simp add: "op supports_def" fresh_def[symmetric]) + apply(rule allI)+ + apply(rule impI) + apply(erule conjE) + apply(simp add: perm_set_def) + apply(auto) + apply(subgoal_tac "[(a,b)]\aa = aa")(*A*) + apply(simp) + apply(rule pt_fresh_fresh[OF pt, OF at]) + apply(force) + apply(force) + apply(rule_tac x="x" in exI) + apply(simp) + apply(rule sym) + apply(rule pt_fresh_fresh[OF pt, OF at]) + apply(force)+ + done + +lemma Union_of_fin_supp_sets: + fixes X::"('a set)" + assumes fs: "fs TYPE('a) TYPE('x)" + and fi: "finite X" + shows "finite (\x\X. ((supp x)::'x set))" +using fi by (induct, auto simp add: fs1[OF fs]) + +lemma Union_included_in_supp: + fixes X::"('a set)" + assumes pt: "pt TYPE('a) TYPE('x)" + and at: "at TYPE('x)" + and fs: "fs TYPE('a) TYPE('x)" + and fi: "finite X" + shows "(\x\X. ((supp x)::'x set)) \ supp X" +proof - + have "supp ((X_to_Un_supp X)::'x set) \ ((supp X)::'x set)" + apply(rule pt_empty_supp_fun_subset) + apply(force intro: pt_set_inst at_pt_inst pt at)+ + apply(rule pt_eqvt_fun2b) + apply(force intro: pt_set_inst at_pt_inst pt at)+ + apply(rule allI) + apply(rule allI) + apply(rule X_to_Un_supp_eqvt[OF pt, OF at]) + done + hence "supp (\x\X. ((supp x)::'x set)) \ ((supp X)::'x set)" by (simp add: X_to_Un_supp_def) + moreover + have "supp (\x\X. ((supp x)::'x set)) = (\x\X. ((supp x)::'x set))" + apply(rule at_fin_set_supp[OF at]) + apply(rule Union_of_fin_supp_sets[OF fs, OF fi]) + done + ultimately show ?thesis by force +qed + +lemma supp_of_fin_sets: + fixes X::"('a set)" + assumes pt: "pt TYPE('a) TYPE('x)" + and at: "at TYPE('x)" + and fs: "fs TYPE('a) TYPE('x)" + and fi: "finite X" + shows "(supp X) = (\x\X. ((supp x)::'x set))" +apply(rule subset_antisym) +apply(rule supp_is_subset) +apply(rule Union_supports_set[OF pt, OF at]) +apply(rule Union_of_fin_supp_sets[OF fs, OF fi]) +apply(rule Union_included_in_supp[OF pt, OF at, OF fs, OF fi]) +done + +lemma supp_fin_union: + fixes X::"('a set)" + and Y::"('a set)" + assumes pt: "pt TYPE('a) TYPE('x)" + and at: "at TYPE('x)" + and fs: "fs TYPE('a) TYPE('x)" + and f1: "finite X" + and f2: "finite Y" + shows "(supp (X\Y)) = (supp X)\((supp Y)::'x set)" +using f1 f2 by (force simp add: supp_of_fin_sets[OF pt, OF at, OF fs]) + +lemma supp_fin_insert: + fixes X::"('a set)" + and x::"'a" + assumes pt: "pt TYPE('a) TYPE('x)" + and at: "at TYPE('x)" + and fs: "fs TYPE('a) TYPE('x)" + and f: "finite X" + shows "(supp (insert x X)) = (supp x)\((supp X)::'x set)" +proof - + have "(supp (insert x X)) = ((supp ({x}\(X::'a set)))::'x set)" by simp + also have "\ = (supp {x})\(supp X)" + by (rule supp_fin_union[OF pt, OF at, OF fs], simp_all add: f) + finally show "(supp (insert x X)) = (supp x)\((supp X)::'x set)" + by (simp add: supp_singleton) +qed + +lemma fresh_fin_union: + fixes X::"('a set)" + and Y::"('a set)" + and a::"'x" + assumes pt: "pt TYPE('a) TYPE('x)" + and at: "at TYPE('x)" + and fs: "fs TYPE('a) TYPE('x)" + and f1: "finite X" + and f2: "finite Y" + shows "a\(X\Y) = (a\X \ a\Y)" +apply(simp add: fresh_def) +apply(simp add: supp_fin_union[OF pt, OF at, OF fs, OF f1, OF f2]) +done + +lemma fresh_fin_insert: + fixes X::"('a set)" + and x::"'a" + and a::"'x" + assumes pt: "pt TYPE('a) TYPE('x)" + and at: "at TYPE('x)" + and fs: "fs TYPE('a) TYPE('x)" + and f: "finite X" + shows "a\(insert x X) = (a\x \ a\X)" +apply(simp add: fresh_def) +apply(simp add: supp_fin_insert[OF pt, OF at, OF fs, OF f]) +done + +lemma fresh_fin_insert1: + fixes X::"('a set)" + and x::"'a" + and a::"'x" + assumes pt: "pt TYPE('a) TYPE('x)" + and at: "at TYPE('x)" + and fs: "fs TYPE('a) TYPE('x)" + and f: "finite X" + and a1: "a\x" + and a2: "a\X" + shows "a\(insert x X)" +using a1 a2 +apply(simp add: fresh_fin_insert[OF pt, OF at, OF fs, OF f]) +done + +lemma pt_list_set_pi: + fixes pi :: "'x prm" + and xs :: "'a list" + assumes pt: "pt TYPE('a) TYPE('x)" + shows "pi\(set xs) = set (pi\xs)" +by (induct xs, auto simp add: perm_set_def pt1[OF pt]) + +lemma pt_list_set_supp: + fixes xs :: "'a list" + assumes pt: "pt TYPE('a) TYPE('x)" + and at: "at TYPE('x)" + and fs: "fs TYPE('a) TYPE('x)" + shows "supp (set xs) = ((supp xs)::'x set)" +proof - + have "supp (set xs) = (\x\(set xs). ((supp x)::'x set))" + by (rule supp_of_fin_sets[OF pt, OF at, OF fs], rule finite_set) + also have "(\x\(set xs). ((supp x)::'x set)) = (supp xs)" + proof(induct xs) + case Nil show ?case by (simp add: supp_list_nil) + next + case (Cons h t) thus ?case by (simp add: supp_list_cons) + qed + finally show ?thesis by simp +qed + +lemma pt_list_set_fresh: + fixes a :: "'x" + and xs :: "'a list" + assumes pt: "pt TYPE('a) TYPE('x)" + and at: "at TYPE('x)" + and fs: "fs TYPE('a) TYPE('x)" + and a: "a\xs" + shows "a\(set xs) = a\xs" +by (simp add: fresh_def pt_list_set_supp[OF pt, OF at, OF fs]) + section {* Andy's freshness lemma *} (*================================*) @@ -2283,12 +2532,10 @@ (*****************************************) (* setup for induction principles method *) -(* use "nominal_induct.ML"; method_setup nominal_induct = {* nominal_induct_method *} {* nominal induction *} -*) (*******************************) (* permutation equality tactic *)