--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Nominal2_Eqvt.thy Sun Nov 14 16:34:47 2010 +0000
@@ -0,0 +1,382 @@
+(* Title: Nominal2_Eqvt
+ Author: Brian Huffman,
+ Author: Christian Urban
+
+ Equivariance, supp and freshness lemmas for various operators
+ (contains many, but not all such lemmas).
+*)
+theory Nominal2_Eqvt
+imports Nominal2_Base
+uses ("nominal_thmdecls.ML")
+ ("nominal_permeq.ML")
+ ("nominal_eqvt.ML")
+begin
+
+
+section {* Permsimp and Eqvt infrastructure *}
+
+text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *}
+
+use "nominal_thmdecls.ML"
+setup "Nominal_ThmDecls.setup"
+
+
+section {* eqvt lemmas *}
+
+lemmas [eqvt] =
+ conj_eqvt Not_eqvt ex_eqvt all_eqvt imp_eqvt
+ imp_eqvt[folded induct_implies_def]
+ uminus_eqvt
+
+ (* nominal *)
+ supp_eqvt fresh_eqvt fresh_star_eqvt add_perm_eqvt atom_eqvt
+ swap_eqvt flip_eqvt
+
+ (* datatypes *)
+ Pair_eqvt permute_list.simps
+
+ (* sets *)
+ mem_eqvt empty_eqvt insert_eqvt set_eqvt
+
+ (* fsets *)
+ permute_fset fset_eqvt
+
+text {* helper lemmas for the perm_simp *}
+
+definition
+ "unpermute p = permute (- p)"
+
+lemma eqvt_apply:
+ fixes f :: "'a::pt \<Rightarrow> 'b::pt"
+ and x :: "'a::pt"
+ shows "p \<bullet> (f x) \<equiv> (p \<bullet> f) (p \<bullet> x)"
+ unfolding permute_fun_def by simp
+
+lemma eqvt_lambda:
+ fixes f :: "'a::pt \<Rightarrow> 'b::pt"
+ shows "p \<bullet> (\<lambda>x. f x) \<equiv> (\<lambda>x. p \<bullet> (f (unpermute p x)))"
+ unfolding permute_fun_def unpermute_def by simp
+
+lemma eqvt_bound:
+ shows "p \<bullet> unpermute p x \<equiv> x"
+ unfolding unpermute_def by simp
+
+text {* provides perm_simp methods *}
+
+use "nominal_permeq.ML"
+setup Nominal_Permeq.setup
+
+method_setup perm_simp =
+ {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_simp_meth *}
+ {* pushes permutations inside. *}
+
+method_setup perm_strict_simp =
+ {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *}
+ {* pushes permutations inside, raises an error if it cannot solve all permutations. *}
+
+(* the normal version of this lemma would cause loops *)
+lemma permute_eqvt_raw[eqvt_raw]:
+ shows "p \<bullet> permute \<equiv> permute"
+apply(simp add: fun_eq_iff permute_fun_def)
+apply(subst permute_eqvt)
+apply(simp)
+done
+
+subsection {* Equivariance of Logical Operators *}
+
+lemma eq_eqvt[eqvt]:
+ shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)"
+ unfolding permute_eq_iff permute_bool_def ..
+
+lemma if_eqvt[eqvt]:
+ shows "p \<bullet> (if b then x else y) = (if p \<bullet> b then p \<bullet> x else p \<bullet> y)"
+ by (simp add: permute_fun_def permute_bool_def)
+
+lemma True_eqvt[eqvt]:
+ shows "p \<bullet> True = True"
+ unfolding permute_bool_def ..
+
+lemma False_eqvt[eqvt]:
+ shows "p \<bullet> False = False"
+ unfolding permute_bool_def ..
+
+lemma disj_eqvt[eqvt]:
+ shows "p \<bullet> (A \<or> B) = ((p \<bullet> A) \<or> (p \<bullet> B))"
+ by (simp add: permute_bool_def)
+
+lemma all_eqvt2:
+ shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. p \<bullet> P (- p \<bullet> x))"
+ by (perm_simp add: permute_minus_cancel) (rule refl)
+
+lemma ex_eqvt2:
+ shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. p \<bullet> P (- p \<bullet> x))"
+ by (perm_simp add: permute_minus_cancel) (rule refl)
+
+lemma ex1_eqvt[eqvt]:
+ shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)"
+ unfolding Ex1_def
+ by (perm_simp) (rule refl)
+
+lemma ex1_eqvt2:
+ shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. p \<bullet> P (- p \<bullet> x))"
+ by (perm_simp add: permute_minus_cancel) (rule refl)
+
+lemma the_eqvt:
+ assumes unique: "\<exists>!x. P x"
+ shows "(p \<bullet> (THE x. P x)) = (THE x. p \<bullet> P (- p \<bullet> x))"
+ apply(rule the1_equality [symmetric])
+ apply(simp add: ex1_eqvt2[symmetric])
+ apply(simp add: permute_bool_def unique)
+ apply(simp add: permute_bool_def)
+ apply(rule theI'[OF unique])
+ done
+
+subsection {* Equivariance Set Operations *}
+
+lemma not_mem_eqvt:
+ shows "p \<bullet> (x \<notin> A) \<longleftrightarrow> (p \<bullet> x) \<notin> (p \<bullet> A)"
+ by (perm_simp) (rule refl)
+
+lemma Collect_eqvt[eqvt]:
+ shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}"
+ unfolding Collect_def permute_fun_def ..
+
+lemma Collect_eqvt2:
+ shows "p \<bullet> {x. P x} = {x. p \<bullet> (P (-p \<bullet> x))}"
+ by (perm_simp add: permute_minus_cancel) (rule refl)
+
+lemma Bex_eqvt[eqvt]:
+ shows "p \<bullet> (\<exists>x \<in> S. P x) = (\<exists>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
+ unfolding Bex_def
+ by (perm_simp) (rule refl)
+
+lemma Ball_eqvt[eqvt]:
+ shows "p \<bullet> (\<forall>x \<in> S. P x) = (\<forall>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
+ unfolding Ball_def
+ by (perm_simp) (rule refl)
+
+lemma supp_set_empty:
+ shows "supp {} = {}"
+ unfolding supp_def
+ by (simp add: empty_eqvt)
+
+lemma fresh_set_empty:
+ shows "a \<sharp> {}"
+ by (simp add: fresh_def supp_set_empty)
+
+lemma UNIV_eqvt[eqvt]:
+ shows "p \<bullet> UNIV = UNIV"
+ unfolding UNIV_def
+ by (perm_simp) (rule refl)
+
+lemma union_eqvt[eqvt]:
+ shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)"
+ unfolding Un_def
+ by (perm_simp) (rule refl)
+
+lemma inter_eqvt[eqvt]:
+ shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
+ unfolding Int_def
+ by (perm_simp) (rule refl)
+
+lemma Diff_eqvt[eqvt]:
+ fixes A B :: "'a::pt set"
+ shows "p \<bullet> (A - B) = p \<bullet> A - p \<bullet> B"
+ unfolding set_diff_eq
+ by (perm_simp) (rule refl)
+
+lemma Compl_eqvt[eqvt]:
+ fixes A :: "'a::pt set"
+ shows "p \<bullet> (- A) = - (p \<bullet> A)"
+ unfolding Compl_eq_Diff_UNIV
+ by (perm_simp) (rule refl)
+
+lemma image_eqvt:
+ shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
+ unfolding permute_set_eq_image
+ unfolding permute_fun_def [where f=f]
+ by (simp add: image_image)
+
+lemma vimage_eqvt[eqvt]:
+ shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)"
+ unfolding vimage_def
+ by (perm_simp) (rule refl)
+
+lemma Union_eqvt[eqvt]:
+ shows "p \<bullet> (\<Union> S) = \<Union> (p \<bullet> S)"
+ unfolding Union_eq
+ by (perm_simp) (rule refl)
+
+lemma finite_permute_iff:
+ shows "finite (p \<bullet> A) \<longleftrightarrow> finite A"
+ unfolding permute_set_eq_vimage
+ using bij_permute by (rule finite_vimage_iff)
+
+lemma finite_eqvt[eqvt]:
+ shows "p \<bullet> finite A = finite (p \<bullet> A)"
+ unfolding finite_permute_iff permute_bool_def ..
+
+lemma supp_set:
+ fixes xs :: "('a::fs) list"
+ shows "supp (set xs) = supp xs"
+apply(induct xs)
+apply(simp add: supp_set_empty supp_Nil)
+apply(simp add: supp_Cons supp_of_finite_insert)
+done
+
+
+section {* List Operations *}
+
+lemma append_eqvt[eqvt]:
+ shows "p \<bullet> (xs @ ys) = (p \<bullet> xs) @ (p \<bullet> ys)"
+ by (induct xs) auto
+
+lemma supp_append:
+ shows "supp (xs @ ys) = supp xs \<union> supp ys"
+ by (induct xs) (auto simp add: supp_Nil supp_Cons)
+
+lemma fresh_append:
+ shows "a \<sharp> (xs @ ys) \<longleftrightarrow> a \<sharp> xs \<and> a \<sharp> ys"
+ by (induct xs) (simp_all add: fresh_Nil fresh_Cons)
+
+lemma rev_eqvt[eqvt]:
+ shows "p \<bullet> (rev xs) = rev (p \<bullet> xs)"
+ by (induct xs) (simp_all add: append_eqvt)
+
+lemma supp_rev:
+ shows "supp (rev xs) = supp xs"
+ by (induct xs) (auto simp add: supp_append supp_Cons supp_Nil)
+
+lemma fresh_rev:
+ shows "a \<sharp> rev xs \<longleftrightarrow> a \<sharp> xs"
+ by (induct xs) (auto simp add: fresh_append fresh_Cons fresh_Nil)
+
+lemma map_eqvt[eqvt]:
+ shows "p \<bullet> (map f xs) = map (p \<bullet> f) (p \<bullet> xs)"
+ by (induct xs) (simp_all, simp only: permute_fun_app_eq)
+
+
+subsection {* Equivariance for fsets *}
+
+lemma map_fset_eqvt[eqvt]:
+ shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)"
+ by (lifting map_eqvt)
+
+
+subsection {* Product Operations *}
+
+lemma fst_eqvt[eqvt]:
+ "p \<bullet> (fst x) = fst (p \<bullet> x)"
+ by (cases x) simp
+
+lemma snd_eqvt[eqvt]:
+ "p \<bullet> (snd x) = snd (p \<bullet> x)"
+ by (cases x) simp
+
+lemma split_eqvt[eqvt]:
+ shows "p \<bullet> (split P x) = split (p \<bullet> P) (p \<bullet> x)"
+ unfolding split_def
+ by (perm_simp) (rule refl)
+
+
+section {* Test cases *}
+
+
+declare [[trace_eqvt = false]]
+(* declare [[trace_eqvt = true]] *)
+
+lemma
+ fixes B::"'a::pt"
+ shows "p \<bullet> (B = C)"
+apply(perm_simp)
+oops
+
+lemma
+ fixes B::"bool"
+ shows "p \<bullet> (B = C)"
+apply(perm_simp)
+oops
+
+lemma
+ fixes B::"bool"
+ shows "p \<bullet> (A \<longrightarrow> B = C)"
+apply (perm_simp)
+oops
+
+lemma
+ shows "p \<bullet> (\<lambda>(x::'a::pt). A \<longrightarrow> (B::'a \<Rightarrow> bool) x = C) = foo"
+apply(perm_simp)
+oops
+
+lemma
+ shows "p \<bullet> (\<lambda>B::bool. A \<longrightarrow> (B = C)) = foo"
+apply (perm_simp)
+oops
+
+lemma
+ shows "p \<bullet> (\<lambda>x y. \<exists>z. x = z \<and> x = y \<longrightarrow> z \<noteq> x) = foo"
+apply (perm_simp)
+oops
+
+lemma
+ shows "p \<bullet> (\<lambda>f x. f (g (f x))) = foo"
+apply (perm_simp)
+oops
+
+lemma
+ fixes p q::"perm"
+ and x::"'a::pt"
+ shows "p \<bullet> (q \<bullet> x) = foo"
+apply(perm_simp)
+oops
+
+lemma
+ fixes p q r::"perm"
+ and x::"'a::pt"
+ shows "p \<bullet> (q \<bullet> r \<bullet> x) = foo"
+apply(perm_simp)
+oops
+
+lemma
+ fixes p r::"perm"
+ shows "p \<bullet> (\<lambda>q::perm. q \<bullet> (r \<bullet> x)) = foo"
+apply (perm_simp)
+oops
+
+lemma
+ fixes C D::"bool"
+ shows "B (p \<bullet> (C = D))"
+apply(perm_simp)
+oops
+
+declare [[trace_eqvt = false]]
+
+text {* there is no raw eqvt-rule for The *}
+lemma "p \<bullet> (THE x. P x) = foo"
+apply(perm_strict_simp exclude: The)
+apply(perm_simp exclude: The)
+oops
+
+lemma
+ fixes P :: "(('b \<Rightarrow> bool) \<Rightarrow> ('b::pt)) \<Rightarrow> ('a::pt)"
+ shows "p \<bullet> (P The) = foo"
+apply(perm_simp exclude: The)
+oops
+
+lemma
+ fixes P :: "('a::pt) \<Rightarrow> ('b::pt) \<Rightarrow> bool"
+ shows "p \<bullet> (\<lambda>(a, b). P a b) = (\<lambda>(a, b). (p \<bullet> P) a b)"
+apply(perm_simp)
+oops
+
+thm eqvts
+thm eqvts_raw
+
+ML {* Nominal_ThmDecls.is_eqvt @{context} @{term "supp"} *}
+
+
+section {* automatic equivariance procedure for inductive definitions *}
+
+use "nominal_eqvt.ML"
+
+end