# HG changeset patch # User Christian Urban # Date 1295267651 0 # Node ID 54aade5d0fe63927ab3c8a93a537711896f12760 # Parent 7c5bca97888683a312a7cbc7b7b979a8c91308ec moved high level code from LamTest into the main libraries. diff -r 7c5bca978886 -r 54aade5d0fe6 Nominal/Nominal2_Abs.thy --- a/Nominal/Nominal2_Abs.thy Mon Jan 17 12:33:37 2011 +0000 +++ b/Nominal/Nominal2_Abs.thy Mon Jan 17 12:34:11 2011 +0000 @@ -444,7 +444,7 @@ termination supp_lst by (auto intro!: local.termination) -lemma [eqvt]: +lemma supp_funs_eqvt[eqvt]: shows "(p \ supp_set x) = supp_set (p \ x)" and "(p \ supp_res y) = supp_res (p \ y)" and "(p \ supp_lst z) = supp_lst (p \ z)" @@ -461,7 +461,7 @@ and "a \ Abs_res bs x \ a \ supp_res (Abs_res bs x)" and "a \ Abs_lst cs x \ a \ supp_lst (Abs_lst cs x)" by (rule_tac [!] fresh_fun_eqvt_app) - (simp_all only: eqvts_raw) + (auto simp only: eqvt_def eqvts_raw) lemma Abs_supp_subset1: assumes a: "finite (supp x)" diff -r 7c5bca978886 -r 54aade5d0fe6 Nominal/Nominal2_Base.thy --- a/Nominal/Nominal2_Base.thy Mon Jan 17 12:33:37 2011 +0000 +++ b/Nominal/Nominal2_Base.thy Mon Jan 17 12:34:11 2011 +0000 @@ -415,6 +415,7 @@ shows "p \ (f x) = (p \ f) (p \ x)" unfolding permute_fun_def by simp + subsection {* Permutations for booleans *} instantiation bool :: pt @@ -451,6 +452,16 @@ unfolding permute_fun_def permute_bool_def by (auto, drule_tac x="p \ x" in spec, simp) +lemma ex1_eqvt: + shows "p \ (\!x. P x) = (\!x. (p \ P) x)" + unfolding Ex1_def + apply(simp add: ex_eqvt) + unfolding permute_fun_def + apply(simp add: conj_eqvt all_eqvt) + unfolding permute_fun_def + apply(simp add: imp_eqvt permute_bool_def) + done + lemma permute_boolE: fixes P::"bool" shows "p \ P \ P" @@ -718,7 +729,6 @@ instance int :: pure proof qed (rule permute_int_def) - subsection {* Supp, Freshness and Supports *} context pt @@ -1233,16 +1243,26 @@ unfolding fresh_def by auto -text {* Support of Equivariant Functions *} +text {* Equivariant Functions *} + +definition + "eqvt f \ \p. p \ f = f" + +lemma eqvtI: + shows "(\p. p \ f \ f) \ eqvt f" +unfolding eqvt_def +by simp lemma supp_fun_eqvt: - assumes a: "\p. p \ f = f" + assumes a: "eqvt f" shows "supp f = {}" + using a + unfolding eqvt_def unfolding supp_def - using a by simp + by simp lemma fresh_fun_eqvt_app: - assumes a: "\p. p \ f = f" + assumes a: "eqvt f" shows "a \ x \ a \ f x" proof - from a have "supp f = {}" by (simp add: supp_fun_eqvt) @@ -1251,6 +1271,81 @@ using supp_fun_app by auto qed +text {* equivariance of a function at a given argument *} +definition + "eqvt_at f x \ \p. p \ (f x) = f (p \ x)" + +lemma supp_eqvt_at: + assumes asm: "eqvt_at f x" + and fin: "finite (supp x)" + shows "supp (f x) \ supp x" +apply(rule supp_is_subset) +unfolding supports_def +unfolding fresh_def[symmetric] +using asm +apply(simp add: eqvt_at_def) +apply(simp add: swap_fresh_fresh) +apply(rule fin) +done + +lemma finite_supp_eqvt_at: + assumes asm: "eqvt_at f x" + and fin: "finite (supp x)" + shows "finite (supp (f x))" +apply(rule finite_subset) +apply(rule supp_eqvt_at[OF asm fin]) +apply(rule fin) +done + +lemma fresh_eqvt_at: + assumes asm: "eqvt_at f x" + and fin: "finite (supp x)" + and fresh: "a \ x" + shows "a \ f x" +using fresh +unfolding fresh_def +using supp_eqvt_at[OF asm fin] +by auto + +text {* helper functions for nominal_functions *} + +lemma the_default_eqvt: + assumes unique: "\!x. P x" + shows "(p \ (THE_default d P)) = (THE_default d (p \ P))" + apply(rule THE_default1_equality [symmetric]) + apply(rule_tac p="-p" in permute_boolE) + apply(simp add: ex1_eqvt) + apply(rule unique) + apply(rule_tac p="-p" in permute_boolE) + apply(rule subst[OF permute_fun_app_eq]) + apply(simp) + apply(rule THE_defaultI'[OF unique]) + done + +lemma fundef_ex1_eqvt: + fixes x::"'a::pt" + assumes f_def: "f == (\x::'a. THE_default d (G x))" + assumes eqvt: "eqvt G" + assumes ex1: "\!y. G x y" + shows "(p \ (f x)) = f (p \ x)" + apply(simp only: f_def) + apply(subst the_default_eqvt) + apply(rule ex1) + using eqvt + unfolding eqvt_def + apply(simp add: permute_fun_app_eq) + done + +lemma fundef_ex1_eqvt_at: + fixes x::"'a::pt" + assumes f_def: "f == (\x::'a. THE_default d (G x))" + assumes eqvt: "eqvt G" + assumes ex1: "\!y. G x y" + shows "eqvt_at f x" + unfolding eqvt_at_def + using assms + by (auto intro: fundef_ex1_eqvt) + section {* Support of Finite Sets of Finitely Supported Elements *} @@ -1274,15 +1369,23 @@ unfolding fresh_def by (simp add: supp_finite_atom_set[OF assms]) - lemma Union_fresh: shows "a \ S \ a \ (\x \ S. supp x)" unfolding Union_image_eq[symmetric] apply(rule_tac f="\S. \ supp ` S" in fresh_fun_eqvt_app) - apply(simp add: permute_fun_def UNION_def Collect_def Bex_def ex_eqvt mem_def conj_eqvt) - apply(subst permute_fun_app_eq) - back - apply(simp add: supp_eqvt) + unfolding eqvt_def + unfolding permute_fun_def + apply(simp) + unfolding UNION_def + unfolding Collect_def + unfolding Bex_def + apply(simp add: ex_eqvt) + unfolding permute_fun_def + apply(simp add: conj_eqvt) + apply(simp add: mem_eqvt) + apply(simp add: supp_eqvt) + unfolding permute_fun_def + apply(simp) apply(assumption) done @@ -1547,7 +1650,7 @@ by (metis mem_permute_iff permute_minus_cancel(1) fresh_permute_iff) lemma fresh_star_eqvt: - shows "(p \ (as \* x)) = (p \ as) \* (p \ x)" + shows "p \ (as \* x) \ (p \ as) \* (p \ x)" unfolding fresh_star_def unfolding Ball_def apply(simp add: all_eqvt) diff -r 7c5bca978886 -r 54aade5d0fe6 Nominal/Nominal2_Eqvt.thy --- a/Nominal/Nominal2_Eqvt.thy Mon Jan 17 12:33:37 2011 +0000 +++ b/Nominal/Nominal2_Eqvt.thy Mon Jan 17 12:34:11 2011 +0000 @@ -24,7 +24,7 @@ section {* eqvt lemmas *} lemmas [eqvt] = - conj_eqvt Not_eqvt ex_eqvt all_eqvt imp_eqvt uminus_eqvt + conj_eqvt Not_eqvt ex_eqvt all_eqvt ex1_eqvt imp_eqvt uminus_eqvt imp_eqvt[folded induct_implies_def] all_eqvt[folded induct_forall_def]