(*  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"

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: expand_fun_eq permute_fun_def)
apply(subst permute_eqvt)
apply(simp)
done

section {* 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 imp_eqvt[eqvt]:
  shows "p \<bullet> (A \<longrightarrow> B) = ((p \<bullet> A) \<longrightarrow> (p \<bullet> B))"
  by (simp add: permute_bool_def)

lemma conj_eqvt[eqvt]:
  shows "p \<bullet> (A \<and> B) = ((p \<bullet> A) \<and> (p \<bullet> B))"
  by (simp add: 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 Not_eqvt[eqvt]:
  shows "p \<bullet> (\<not> A) \<longleftrightarrow> \<not> (p \<bullet> A)"
  by (simp add: permute_bool_def)

lemma all_eqvt[eqvt]:
  shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)"
  unfolding permute_fun_def permute_bool_def
  by (auto, drule_tac x="p \<bullet> x" in spec, simp)

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_eqvt[eqvt]:
  shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)"
  unfolding permute_fun_def permute_bool_def
  by (auto, rule_tac x="p \<bullet> x" in exI, simp)

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

section {* Set Operations *}

lemma mem_permute_iff:
  shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"
  unfolding mem_def permute_fun_def permute_bool_def
  by simp

lemma mem_eqvt[eqvt]:
  shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
  unfolding mem_def
  by (perm_simp) (rule refl)

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 empty_eqvt[eqvt]:
  shows "p \<bullet> {} = {}"
  unfolding empty_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 insert_eqvt[eqvt]:
  shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)"
  unfolding permute_set_eq_image image_insert ..

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

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 set_eqvt[eqvt]:
  shows "p \<bullet> (set xs) = set (p \<bullet> xs)"
  by (induct xs) (simp_all add: empty_eqvt insert_eqvt)

(* needs finite support premise
lemma supp_set:
  fixes x :: "'a::pt"
  shows "supp (set xs) = supp xs"
*)

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)

section {* 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

section {* Units *}

lemma supp_unit:
  shows "supp () = {}"
  by (simp add: supp_def)

lemma fresh_unit:
  shows "a \<sharp> ()"
  by (simp add: fresh_def supp_unit)


section {* additional eqvt lemmas *}

lemmas [eqvt] = 
  imp_eqvt [folded induct_implies_def]

  (* nominal *)
  supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt

  (* datatypes *)
  Pair_eqvt permute_list.simps

  (* sets *)
  image_eqvt


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 {* Problem: 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

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