(*  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 ex1_eqvt imp_eqvt uminus_eqvt

  imp_eqvt[folded induct_implies_def]

  all_eqvt[folded induct_forall_def]

  (* nominal *)

  supp_eqvt fresh_eqvt fresh_star_eqvt add_perm_eqvt atom_eqvt 

  swap_eqvt flip_eqvt

  (* datatypes *)

  Pair_eqvt permute_list.simps permute_option.simps 

  permute_sum.simps

  (* sets *)

  mem_eqvt empty_eqvt insert_eqvt set_eqvt inter_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_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) x)"

  apply(rule the1_equality [symmetric])

  apply(rule_tac p="-p" in permute_boolE)

  apply(perm_simp add: permute_minus_cancel)

  apply(rule unique)

  apply(rule_tac p="-p" in permute_boolE)

  apply(perm_simp add: permute_minus_cancel)

  apply(rule theI'[OF unique])

  done

lemma the_eqvt2:

  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 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 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 subset_eqvt[eqvt]:

  shows "p \<bullet> (S \<subseteq> T) \<longleftrightarrow> (p \<bullet> S) \<subseteq> (p \<bullet> T)"

  unfolding subset_eq

  by (perm_simp) (rule refl)

lemma psubset_eqvt[eqvt]:

  shows "p \<bullet> (S \<subset> T) \<longleftrightarrow> (p \<bullet> S) \<subset> (p \<bullet> T)"

  unfolding psubset_eq

  by (perm_simp) (rule refl)

lemma image_eqvt[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 Sigma_eqvt:

  shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)"

unfolding Sigma_def

unfolding UNION_eq_Union_image

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 ..

section {* List Operations *}

lemma append_eqvt[eqvt]:

  shows "p \<bullet> (xs @ ys) = (p \<bullet> xs) @ (p \<bullet> ys)"

  by (induct xs) auto

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)

lemma removeAll_eqvt[eqvt]:

  shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"

  by (induct xs) (auto)

lemma supp_removeAll:

  fixes x::"atom"

  shows "supp (removeAll x xs) = supp xs - {x}"

  by (induct xs)

     (auto simp add: supp_Nil supp_Cons supp_atom)

lemma filter_eqvt[eqvt]:

  shows "p \<bullet> (filter f xs) = filter (p \<bullet> f) (p \<bullet> xs)"

apply(induct xs)

apply(simp)

apply(simp only: filter.simps permute_list.simps if_eqvt)

apply(simp only: permute_fun_app_eq)

done

lemma distinct_eqvt[eqvt]:

  shows "p \<bullet> (distinct xs) = distinct (p \<bullet> xs)"

apply(induct xs)

apply(simp add: permute_bool_def)

apply(simp add: conj_eqvt Not_eqvt mem_eqvt set_eqvt)

done

lemma length_eqvt[eqvt]:

  shows "p \<bullet> (length xs) = length (p \<bullet> xs)"

by (induct xs) (simp_all add: permute_pure)

subsection {* Equivariance Finite-Set Operations *}

lemma in_fset_eqvt[eqvt]:

  shows "(p \<bullet> (x |\<in>| S)) = ((p \<bullet> x) |\<in>| (p \<bullet> S))"

unfolding in_fset

by (perm_simp) (simp)

lemma union_fset_eqvt[eqvt]:

  shows "(p \<bullet> (S |\<union>| T)) = ((p \<bullet> S) |\<union>| (p \<bullet> T))"

by (induct S) (simp_all)

lemma supp_union_fset:

  fixes S T::"'a::fs fset"

  shows "supp (S |\<union>| T) = supp S \<union> supp T"

by (induct S) (auto)

lemma fresh_union_fset:

  fixes S T::"'a::fs fset"

  shows "a \<sharp> S |\<union>| T \<longleftrightarrow> a \<sharp> S \<and> a \<sharp> T"

unfolding fresh_def

by (simp add: supp_union_fset)

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