# HG changeset patch # User Christian Urban # Date 1304424548 -3600 # Node ID 75a95431cd8bdfbe00059a6441113fd68886e5d6 # Parent d29a8a6f3138a3f1d7c2cc6e63de6b95b3c41943 proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates) diff -r d29a8a6f3138 -r 75a95431cd8b Nominal/Ex/Datatypes.thy --- a/Nominal/Ex/Datatypes.thy Thu Apr 28 11:51:01 2011 +0800 +++ b/Nominal/Ex/Datatypes.thy Tue May 03 13:09:08 2011 +0100 @@ -67,7 +67,29 @@ thm baz.fv_bn_eqvt thm baz.size_eqvt thm baz.supp + +(* + a nominal datatype with a set argument of + pure type +*) +nominal_datatype set_ty = + Set_ty "nat set" +| Fun "nat \ nat" +| Var "name" +| Lam x::"name" t::"set_ty" bind x in t + +thm set_ty.distinct +thm set_ty.induct +thm set_ty.exhaust +thm set_ty.strong_exhaust +thm set_ty.fv_defs +thm set_ty.bn_defs +thm set_ty.perm_simps +thm set_ty.eq_iff +thm set_ty.fv_bn_eqvt +thm set_ty.size_eqvt +thm set_ty.supp end diff -r d29a8a6f3138 -r 75a95431cd8b Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Thu Apr 28 11:51:01 2011 +0800 +++ b/Nominal/Ex/Lambda.thy Tue May 03 13:09:08 2011 +0100 @@ -15,6 +15,13 @@ where Var: "triv (Var x) n" +lemma + "p \ (triv t x) = triv (p \ t) (p \ x)" +unfolding triv_def +apply(perm_simp) +oops +(*apply(perm_simp)*) + equivariance triv nominal_inductive triv avoids Var: "{}::name set" apply(auto simp add: fresh_star_def) diff -r d29a8a6f3138 -r 75a95431cd8b Nominal/Nominal2_Base.thy --- a/Nominal/Nominal2_Base.thy Thu Apr 28 11:51:01 2011 +0800 +++ b/Nominal/Nominal2_Base.thy Tue May 03 13:09:08 2011 +0100 @@ -789,7 +789,6 @@ unfolding permute_perm_def by (simp add: diff_minus minus_add add_assoc) - subsubsection {* Equivariance of Logical Operators *} lemma eq_eqvt [eqvt]: @@ -951,6 +950,12 @@ unfolding Union_eq by (perm_simp) (rule refl) +lemma Inter_eqvt [eqvt]: + shows "p \ (\ S) = \ (p \ S)" + unfolding Inter_eq + by (perm_simp) (rule refl) + + (* FIXME: eqvt attribute *) lemma Sigma_eqvt: shows "(p \ (X \ Y)) = (p \ X) \ (p \ Y)" @@ -958,9 +963,78 @@ unfolding UNION_eq_Union_image by (perm_simp) (rule refl) +text {* + In order to prove that lfp is equivariant we need two + auxiliary classes which specify that (op <=) and + Inf are equivariant. Instances for bool and fun are + given. +*} + +class le_eqvt = order + + assumes le_eqvt [eqvt]: "p \ (x \ y) = ((p \ x) \ (p \ (y::('a::{pt, order}))))" + +class inf_eqvt = complete_lattice + + assumes inf_eqvt [eqvt]: "p \ (Inf X) = Inf (p \ (X::('a::{pt, Inf}) set))" + +instantiation bool :: le_eqvt +begin + +instance +apply(default) +unfolding le_bool_def +apply(perm_simp) +apply(rule refl) +done + +end + +instantiation "fun" :: (pt, le_eqvt) le_eqvt +begin + +instance +apply(default) +unfolding le_fun_def +apply(perm_simp) +apply(rule refl) +done + +end + +instantiation bool :: inf_eqvt +begin + +instance +apply(default) +unfolding Inf_bool_def +apply(perm_simp) +apply(rule refl) +done + +end + +instantiation "fun" :: (pt, inf_eqvt) inf_eqvt +begin + +instance +apply(default) +unfolding Inf_fun_def +apply(perm_simp) +apply(rule refl) +done + +end + +lemma lfp_eqvt [eqvt]: + fixes F::"('a \ 'b) \ ('a::pt \ 'b::{inf_eqvt, le_eqvt})" + shows "p \ (lfp F) = lfp (p \ F)" +unfolding lfp_def +by (perm_simp) (rule refl) + lemma finite_eqvt [eqvt]: shows "p \ finite A = finite (p \ A)" - unfolding permute_finite permute_bool_def .. +unfolding finite_def +by (perm_simp) (rule refl) + subsubsection {* Equivariance for product operations *}