(*  Title:      Nominal2_Eqvt

    Authors:    Brian Huffman, Christian Urban

    Equivariance, Supp and Fresh Lemmas for Operators. 

*)

theory Nominal2_Eqvt

imports Nominal2_Base

uses ("nominal_thmdecls.ML")

begin

section {* Logical Operators *}

lemma eq_eqvt:

  shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)"

  unfolding permute_eq_iff permute_bool_def ..

lemma if_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:

  shows "p \<bullet> True = True"

  unfolding permute_bool_def ..

lemma False_eqvt:

  shows "p \<bullet> False = False"

  unfolding permute_bool_def ..

lemma imp_eqvt:

  shows "p \<bullet> (A \<longrightarrow> B) = ((p \<bullet> A) \<longrightarrow> (p \<bullet> B))"

  by (simp add: permute_bool_def)

lemma conj_eqvt:

  shows "p \<bullet> (A \<and> B) = ((p \<bullet> A) \<and> (p \<bullet> B))"

  by (simp add: permute_bool_def)

lemma disj_eqvt:

  shows "p \<bullet> (A \<or> B) = ((p \<bullet> A) \<or> (p \<bullet> B))"

  by (simp add: permute_bool_def)

lemma Not_eqvt:

  shows "p \<bullet> (\<not> A) = (\<not> (p \<bullet> A))"

  by (simp add: permute_bool_def)

lemma all_eqvt:

  shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. p \<bullet> P (- p \<bullet> x))"

  unfolding permute_fun_def permute_bool_def

  by (auto, drule_tac x="p \<bullet> x" in spec, simp)

lemma ex_eqvt:

  shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. p \<bullet> P (- p \<bullet> x))"

  unfolding permute_fun_def permute_bool_def

  by (auto, rule_tac x="p \<bullet> x" in exI, simp)

lemma ex1_eqvt:

  shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. p \<bullet> P (- p \<bullet> x))"

  unfolding Ex1_def ex_eqvt conj_eqvt all_eqvt imp_eqvt eq_eqvt

  by simp

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_eqvt[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_eqvt:

  shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"

  unfolding mem_def permute_fun_def by simp

lemma not_mem_eqvt:

  shows "p \<bullet> (x \<notin> A) \<longleftrightarrow> (p \<bullet> x) \<notin> (p \<bullet> A)"

  unfolding mem_def permute_fun_def by (simp add: Not_eqvt)

lemma Collect_eqvt:

  shows "p \<bullet> {x. P x} = {x. p \<bullet> (P (-p \<bullet> x))}"

  unfolding Collect_def permute_fun_def ..

lemma empty_eqvt:

  shows "p \<bullet> {} = {}"

  unfolding empty_def Collect_eqvt False_eqvt ..

lemma supp_set_empty:

  shows "supp {} = {}"

  by (simp add: supp_def empty_eqvt)

lemma fresh_set_empty:

  shows "a \<sharp> {}"

  by (simp add: fresh_def supp_set_empty)

lemma UNIV_eqvt:

  shows "p \<bullet> UNIV = UNIV"

  unfolding UNIV_def Collect_eqvt True_eqvt ..

lemma union_eqvt:

  shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)"

  unfolding Un_def Collect_eqvt disj_eqvt mem_eqvt by simp

lemma inter_eqvt:

  shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"

  unfolding Int_def Collect_eqvt conj_eqvt mem_eqvt by simp

lemma Diff_eqvt:

  fixes A B :: "'a::pt set"

  shows "p \<bullet> (A - B) = p \<bullet> A - p \<bullet> B"

  unfolding set_diff_eq Collect_eqvt conj_eqvt Not_eqvt mem_eqvt by simp

lemma Compl_eqvt:

  fixes A :: "'a::pt set"

  shows "p \<bullet> (- A) = - (p \<bullet> A)"

  unfolding Compl_eq_Diff_UNIV Diff_eqvt UNIV_eqvt ..

lemma insert_eqvt:

  shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)"

  unfolding permute_set_eq_image image_insert ..

lemma vimage_eqvt:

  shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)"

  unfolding vimage_def permute_fun_def [where f=f]

  unfolding Collect_eqvt mem_eqvt ..

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

  shows "p \<bullet> finite A = finite (p \<bullet> A)"

  unfolding finite_permute_iff permute_bool_def ..

lemma supp_eqvt: "p \<bullet> supp S = supp (p \<bullet> S)"

  unfolding supp_def

  by (simp only: Collect_eqvt Not_eqvt finite_eqvt eq_eqvt

      permute_eqvt [of p] swap_eqvt permute_minus_cancel)

section {* List Operations *}

lemma append_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:

  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:

  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"

*)

section {* Product Operations *}

lemma fst_eqvt:

  "p \<bullet> (fst x) = fst (p \<bullet> x)"

 by (cases x) simp

lemma snd_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 {* Equivariance automation *}

text {* 

  below is a construction site for a conversion that  

  pushes permutations into a term as far as possible 

*}

text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_force} *}

use "nominal_thmdecls.ML"

setup "NominalThmDecls.setup"

lemmas [eqvt] = 

  (* connectives *)

  eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt 

  True_eqvt False_eqvt

  imp_eqvt [folded induct_implies_def]

  (* datatypes *)

  permute_prod.simps

  fst_eqvt snd_eqvt

  (* sets *)

  empty_eqvt UNIV_eqvt union_eqvt inter_eqvt

  Diff_eqvt Compl_eqvt insert_eqvt

(* A simple conversion pushing permutations into a term *)

ML {*

fun OF1 thm1 thm2 = thm2 RS thm1

fun get_eqvt_thms ctxt =

  map (OF1 @{thm eq_reflection}) (NominalThmDecls.get_eqvt_thms ctxt)  

*}

ML {* 

fun eqvt_conv ctxt ctrm =

  case (term_of ctrm) of

    (Const (@{const_name "permute"}, _) $ _ $ t) =>

       (if is_Const (head_of t)

        then (More_Conv.rewrs_conv (get_eqvt_thms ctxt) 

              then_conv eqvt_conv ctxt) ctrm

        else Conv.comb_conv (eqvt_conv ctxt) ctrm)

     | _ $ _ => Conv.comb_conv (eqvt_conv ctxt) ctrm

     | Abs _ => Conv.abs_conv (fn (_, ctxt) => eqvt_conv ctxt) ctxt ctrm

     | _ => Conv.all_conv ctrm

*}

ML {*

fun eqvt_tac ctxt = 

  CONVERSION (More_Conv.bottom_conv (fn ctxt => eqvt_conv ctxt) ctxt)

*}

lemma "p \<bullet> (A \<longrightarrow> B = (C::bool))"

apply(tactic {* eqvt_tac @{context} 1 *}) 

oops

text {*

  Another conversion for pushing permutations into a term.

  It is designed not to apply rules like @{term permute_pure} to

  applications or abstractions, only to constants or free

  variables. Thus permutations are not removed too early, and they

  have a chance to cancel with bound variables.

*}

definition

  "unpermute p = permute (- p)"

lemma push_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 push_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 push_bound:

  shows "p \<bullet> unpermute p x \<equiv> x"

  unfolding unpermute_def by simp

ML {*

structure PushData = Named_Thms

(

  val name = "push"

  val description = "push permutations"

)

local

fun push_apply_conv ctxt ct =

  case (term_of ct) of

    (Const (@{const_name "permute"}, _) $ _ $ (_ $ _)) =>

      let

        val (perm, t) = Thm.dest_comb ct

        val (_, p) = Thm.dest_comb perm

        val (f, x) = Thm.dest_comb t

        val a = ctyp_of_term x;

        val b = ctyp_of_term t;

        val ty_insts = map SOME [b, a]

        val term_insts = map SOME [p, f, x]

      in

        Drule.instantiate' ty_insts term_insts @{thm push_apply}

      end

  | _ => Conv.no_conv ct

fun push_lambda_conv ctxt ct =

  case (term_of ct) of

    (Const (@{const_name "permute"}, _) $ _ $ Abs _) =>

      Conv.rewr_conv @{thm push_lambda} ct

  | _ => Conv.no_conv ct

in

fun push_conv ctxt ct =

  Conv.first_conv

    [ Conv.rewr_conv @{thm push_bound},

      push_apply_conv ctxt

        then_conv Conv.comb_conv (push_conv ctxt),

      push_lambda_conv ctxt

        then_conv Conv.abs_conv (fn (v, ctxt) => push_conv ctxt) ctxt,

      More_Conv.rewrs_conv (PushData.get ctxt),

      Conv.all_conv

    ] ct

fun push_tac ctxt = 

  CONVERSION (More_Conv.bottom_conv (fn ctxt => push_conv ctxt) ctxt)

end

*}

setup PushData.setup

declare permute_pure [THEN eq_reflection, push]

lemma push_eq [THEN eq_reflection, push]:

  "p \<bullet> (op =) = (op =)"

  by (simp add: expand_fun_eq permute_fun_def eq_eqvt)

lemma push_All [THEN eq_reflection, push]:

  "p \<bullet> All = All"

  by (simp add: expand_fun_eq permute_fun_def all_eqvt)

lemma push_Ex [THEN eq_reflection, push]:

  "p \<bullet> Ex = Ex"

  by (simp add: expand_fun_eq permute_fun_def ex_eqvt)

lemma "p \<bullet> (A \<longrightarrow> B = (C::bool))"

apply (tactic {* push_tac @{context} 1 *}) 

oops

lemma "p \<bullet> (\<lambda>x. A \<longrightarrow> B x = (C::bool)) = foo"

apply (tactic {* push_tac @{context} 1 *})

oops

lemma "p \<bullet> (\<lambda>x y. \<exists>z. x = z \<and> x = y \<longrightarrow> z \<noteq> x) = foo"

apply (tactic {* push_tac @{context} 1 *})

oops

lemma "p \<bullet> (\<lambda>f x. f (g (f x))) = foo"

apply (tactic {* push_tac @{context} 1 *})

oops

end