(*  Title:      Nominal2_Base

    Authors:    Brian Huffman, Christian Urban

    Basic definitions and lemma infrastructure for 

    Nominal Isabelle. 

*)

theory Nominal2_Base

imports Main 

        "~~/src/HOL/Library/Infinite_Set"

        "~~/src/HOL/Quotient_Examples/FSet"

uses ("nominal_library.ML")

     ("nominal_atoms.ML")

begin

section {* Atoms and Sorts *}

text {* A simple implementation for atom_sorts is strings. *}

(* types atom_sort = string *)

text {* To deal with Church-like binding we use trees of  

  strings as sorts. *}

datatype atom_sort = Sort "string" "atom_sort list"

datatype atom = Atom atom_sort nat

text {* Basic projection function. *}

primrec

  sort_of :: "atom \<Rightarrow> atom_sort"

where

  "sort_of (Atom s i) = s"

primrec

  nat_of :: "atom \<Rightarrow> nat"

where

  "nat_of (Atom s n) = n"

text {* There are infinitely many atoms of each sort. *}

lemma INFM_sort_of_eq: 

  shows "INFM a. sort_of a = s"

proof -

  have "INFM i. sort_of (Atom s i) = s" by simp

  moreover have "inj (Atom s)" by (simp add: inj_on_def)

  ultimately show "INFM a. sort_of a = s" by (rule INFM_inj)

qed

lemma infinite_sort_of_eq:

  shows "infinite {a. sort_of a = s}"

  using INFM_sort_of_eq unfolding INFM_iff_infinite .

lemma atom_infinite [simp]: 

  shows "infinite (UNIV :: atom set)"

  using subset_UNIV infinite_sort_of_eq

  by (rule infinite_super)

lemma obtain_atom:

  fixes X :: "atom set"

  assumes X: "finite X"

  obtains a where "a \<notin> X" "sort_of a = s"

proof -

  from X have "MOST a. a \<notin> X"

    unfolding MOST_iff_cofinite by simp

  with INFM_sort_of_eq

  have "INFM a. sort_of a = s \<and> a \<notin> X"

    by (rule INFM_conjI)

  then obtain a where "a \<notin> X" "sort_of a = s"

    by (auto elim: INFM_E)

  then show ?thesis ..

qed

lemma atom_components_eq_iff:

  fixes a b :: atom

  shows "a = b \<longleftrightarrow> sort_of a = sort_of b \<and> nat_of a = nat_of b"

  by (induct a, induct b, simp)

section {* Sort-Respecting Permutations *}

typedef perm =

  "{f. bij f \<and> finite {a. f a \<noteq> a} \<and> (\<forall>a. sort_of (f a) = sort_of a)}"

proof

  show "id \<in> ?perm" by simp

qed

lemma permI:

  assumes "bij f" and "MOST x. f x = x" and "\<And>a. sort_of (f a) = sort_of a"

  shows "f \<in> perm"

  using assms unfolding perm_def MOST_iff_cofinite by simp

lemma perm_is_bij: "f \<in> perm \<Longrightarrow> bij f"

  unfolding perm_def by simp

lemma perm_is_finite: "f \<in> perm \<Longrightarrow> finite {a. f a \<noteq> a}"

  unfolding perm_def by simp

lemma perm_is_sort_respecting: "f \<in> perm \<Longrightarrow> sort_of (f a) = sort_of a"

  unfolding perm_def by simp

lemma perm_MOST: "f \<in> perm \<Longrightarrow> MOST x. f x = x"

  unfolding perm_def MOST_iff_cofinite by simp

lemma perm_id: "id \<in> perm"

  unfolding perm_def by simp

lemma perm_comp:

  assumes f: "f \<in> perm" and g: "g \<in> perm"

  shows "(f \<circ> g) \<in> perm"

apply (rule permI)

apply (rule bij_comp)

apply (rule perm_is_bij [OF g])

apply (rule perm_is_bij [OF f])

apply (rule MOST_rev_mp [OF perm_MOST [OF g]])

apply (rule MOST_rev_mp [OF perm_MOST [OF f]])

apply (simp)

apply (simp add: perm_is_sort_respecting [OF f])

apply (simp add: perm_is_sort_respecting [OF g])

done

lemma perm_inv:

  assumes f: "f \<in> perm"

  shows "(inv f) \<in> perm"

apply (rule permI)

apply (rule bij_imp_bij_inv)

apply (rule perm_is_bij [OF f])

apply (rule MOST_mono [OF perm_MOST [OF f]])

apply (erule subst, rule inv_f_f)

apply (rule bij_is_inj [OF perm_is_bij [OF f]])

apply (rule perm_is_sort_respecting [OF f, THEN sym, THEN trans])

apply (simp add: surj_f_inv_f [OF bij_is_surj [OF perm_is_bij [OF f]]])

done

lemma bij_Rep_perm: "bij (Rep_perm p)"

  using Rep_perm [of p] unfolding perm_def by simp

lemma finite_Rep_perm: "finite {a. Rep_perm p a \<noteq> a}"

  using Rep_perm [of p] unfolding perm_def by simp

lemma sort_of_Rep_perm: "sort_of (Rep_perm p a) = sort_of a"

  using Rep_perm [of p] unfolding perm_def by simp

lemma Rep_perm_ext:

  "Rep_perm p1 = Rep_perm p2 \<Longrightarrow> p1 = p2"

  by (simp add: fun_eq_iff Rep_perm_inject [symmetric])

instance perm :: size ..

subsection {* Permutations form a group *}

instantiation perm :: group_add

begin

definition

  "0 = Abs_perm id"

definition

  "- p = Abs_perm (inv (Rep_perm p))"

definition

  "p + q = Abs_perm (Rep_perm p \<circ> Rep_perm q)"

definition

  "(p1::perm) - p2 = p1 + - p2"

lemma Rep_perm_0: "Rep_perm 0 = id"

  unfolding zero_perm_def

  by (simp add: Abs_perm_inverse perm_id)

lemma Rep_perm_add:

  "Rep_perm (p1 + p2) = Rep_perm p1 \<circ> Rep_perm p2"

  unfolding plus_perm_def

  by (simp add: Abs_perm_inverse perm_comp Rep_perm)

lemma Rep_perm_uminus:

  "Rep_perm (- p) = inv (Rep_perm p)"

  unfolding uminus_perm_def

  by (simp add: Abs_perm_inverse perm_inv Rep_perm)

instance

apply default

unfolding Rep_perm_inject [symmetric]

unfolding minus_perm_def

unfolding Rep_perm_add

unfolding Rep_perm_uminus

unfolding Rep_perm_0

by (simp_all add: o_assoc inv_o_cancel [OF bij_is_inj [OF bij_Rep_perm]])

end

section {* Implementation of swappings *}

definition

  swap :: "atom \<Rightarrow> atom \<Rightarrow> perm" ("'(_ \<rightleftharpoons> _')")

where

  "(a \<rightleftharpoons> b) =

    Abs_perm (if sort_of a = sort_of b 

              then (\<lambda>c. if a = c then b else if b = c then a else c) 

              else id)"

lemma Rep_perm_swap:

  "Rep_perm (a \<rightleftharpoons> b) =

    (if sort_of a = sort_of b 

     then (\<lambda>c. if a = c then b else if b = c then a else c)

     else id)"

unfolding swap_def

apply (rule Abs_perm_inverse)

apply (rule permI)

apply (auto simp add: bij_def inj_on_def surj_def)[1]

apply (rule MOST_rev_mp [OF MOST_neq(1) [of a]])

apply (rule MOST_rev_mp [OF MOST_neq(1) [of b]])

apply (simp)

apply (simp)

done

lemmas Rep_perm_simps =

  Rep_perm_0

  Rep_perm_add

  Rep_perm_uminus

  Rep_perm_swap

lemma swap_different_sorts [simp]:

  "sort_of a \<noteq> sort_of b \<Longrightarrow> (a \<rightleftharpoons> b) = 0"

  by (rule Rep_perm_ext) (simp add: Rep_perm_simps)

lemma swap_cancel:

  "(a \<rightleftharpoons> b) + (a \<rightleftharpoons> b) = 0"

  by (rule Rep_perm_ext) 

     (simp add: Rep_perm_simps fun_eq_iff)

lemma swap_self [simp]:

  "(a \<rightleftharpoons> a) = 0"

  by (rule Rep_perm_ext, simp add: Rep_perm_simps fun_eq_iff)

lemma minus_swap [simp]:

  "- (a \<rightleftharpoons> b) = (a \<rightleftharpoons> b)"

  by (rule minus_unique [OF swap_cancel])

lemma swap_commute:

  "(a \<rightleftharpoons> b) = (b \<rightleftharpoons> a)"

  by (rule Rep_perm_ext)

     (simp add: Rep_perm_swap fun_eq_iff)

lemma swap_triple:

  assumes "a \<noteq> b" and "c \<noteq> b"

  assumes "sort_of a = sort_of b" "sort_of b = sort_of c"

  shows "(a \<rightleftharpoons> c) + (b \<rightleftharpoons> c) + (a \<rightleftharpoons> c) = (a \<rightleftharpoons> b)"

  using assms

  by (rule_tac Rep_perm_ext)

     (auto simp add: Rep_perm_simps fun_eq_iff)

section {* Permutation Types *}

text {*

  Infix syntax for @{text permute} has higher precedence than

  addition, but lower than unary minus.

*}

class pt =

  fixes permute :: "perm \<Rightarrow> 'a \<Rightarrow> 'a" ("_ \<bullet> _" [76, 75] 75)

  assumes permute_zero [simp]: "0 \<bullet> x = x"

  assumes permute_plus [simp]: "(p + q) \<bullet> x = p \<bullet> (q \<bullet> x)"

begin

lemma permute_diff [simp]:

  shows "(p - q) \<bullet> x = p \<bullet> - q \<bullet> x"

  unfolding diff_minus by simp

lemma permute_minus_cancel [simp]:

  shows "p \<bullet> - p \<bullet> x = x"

  and   "- p \<bullet> p \<bullet> x = x"

  unfolding permute_plus [symmetric] by simp_all

lemma permute_swap_cancel [simp]:

  shows "(a \<rightleftharpoons> b) \<bullet> (a \<rightleftharpoons> b) \<bullet> x = x"

  unfolding permute_plus [symmetric]

  by (simp add: swap_cancel)

lemma permute_swap_cancel2 [simp]:

  shows "(a \<rightleftharpoons> b) \<bullet> (b \<rightleftharpoons> a) \<bullet> x = x"

  unfolding permute_plus [symmetric]

  by (simp add: swap_commute)

lemma inj_permute [simp]: 

  shows "inj (permute p)"

  by (rule inj_on_inverseI)

     (rule permute_minus_cancel)

lemma surj_permute [simp]: 

  shows "surj (permute p)"

  by (rule surjI, rule permute_minus_cancel)

lemma bij_permute [simp]: 

  shows "bij (permute p)"

  by (rule bijI [OF inj_permute surj_permute])

lemma inv_permute: 

  shows "inv (permute p) = permute (- p)"

  by (rule inv_equality) (simp_all)

lemma permute_minus: 

  shows "permute (- p) = inv (permute p)"

  by (simp add: inv_permute)

lemma permute_eq_iff [simp]: 

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

  by (rule inj_permute [THEN inj_eq])

end

subsection {* Permutations for atoms *}

instantiation atom :: pt

begin

definition

  "p \<bullet> a = (Rep_perm p) a"

instance 

apply(default)

apply(simp_all add: permute_atom_def Rep_perm_simps)

done

end

lemma sort_of_permute [simp]:

  shows "sort_of (p \<bullet> a) = sort_of a"

  unfolding permute_atom_def by (rule sort_of_Rep_perm)

lemma swap_atom:

  shows "(a \<rightleftharpoons> b) \<bullet> c =

           (if sort_of a = sort_of b

            then (if c = a then b else if c = b then a else c) else c)"

  unfolding permute_atom_def

  by (simp add: Rep_perm_swap)

lemma swap_atom_simps [simp]:

  "sort_of a = sort_of b \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> a = b"

  "sort_of a = sort_of b \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> b = a"

  "c \<noteq> a \<Longrightarrow> c \<noteq> b \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> c = c"

  unfolding swap_atom by simp_all

lemma expand_perm_eq:

  fixes p q :: "perm"

  shows "p = q \<longleftrightarrow> (\<forall>a::atom. p \<bullet> a = q \<bullet> a)"

  unfolding permute_atom_def

  by (metis Rep_perm_ext ext)

subsection {* Permutations for permutations *}

instantiation perm :: pt

begin

definition

  "p \<bullet> q = p + q - p"

instance

apply default

apply (simp add: permute_perm_def)

apply (simp add: permute_perm_def diff_minus minus_add add_assoc)

done

end

lemma permute_self: 

  shows "p \<bullet> p = p"

  unfolding permute_perm_def 

  by (simp add: diff_minus add_assoc)

lemma permute_eqvt:

  shows "p \<bullet> (q \<bullet> x) = (p \<bullet> q) \<bullet> (p \<bullet> x)"

  unfolding permute_perm_def by simp

lemma zero_perm_eqvt:

  shows "p \<bullet> (0::perm) = 0"

  unfolding permute_perm_def by simp

lemma add_perm_eqvt:

  fixes p p1 p2 :: perm

  shows "p \<bullet> (p1 + p2) = p \<bullet> p1 + p \<bullet> p2"

  unfolding permute_perm_def

  by (simp add: expand_perm_eq)

lemma swap_eqvt:

  shows "p \<bullet> (a \<rightleftharpoons> b) = (p \<bullet> a \<rightleftharpoons> p \<bullet> b)"

  unfolding permute_perm_def

  by (auto simp add: swap_atom expand_perm_eq)

lemma uminus_eqvt:

  fixes p q::"perm"

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

  unfolding permute_perm_def

  by (simp add: diff_minus minus_add add_assoc)

subsection {* Permutations for functions *}

instantiation "fun" :: (pt, pt) pt

begin

definition

  "p \<bullet> f = (\<lambda>x. p \<bullet> (f (- p \<bullet> x)))"

instance

apply default

apply (simp add: permute_fun_def)

apply (simp add: permute_fun_def minus_add)

done

end

lemma permute_fun_app_eq:

  shows "p \<bullet> (f x) = (p \<bullet> f) (p \<bullet> x)"

  unfolding permute_fun_def by simp

subsection {* Permutations for booleans *}

instantiation bool :: pt

begin

definition "p \<bullet> (b::bool) = b"

instance

apply(default) 

apply(simp_all add: permute_bool_def)

done

end

lemma Not_eqvt:

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

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

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

  by (simp add: permute_bool_def)

lemma ex_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 all_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 ex1_eqvt:

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

  unfolding Ex1_def

  apply(simp add: ex_eqvt)

  unfolding permute_fun_def 

  apply(simp add: conj_eqvt all_eqvt)

  unfolding permute_fun_def

  apply(simp add: imp_eqvt permute_bool_def)

  done

lemma permute_boolE:

  fixes P::"bool"

  shows "p \<bullet> P \<Longrightarrow> P"

  by (simp add: permute_bool_def)

lemma permute_boolI:

  fixes P::"bool"

  shows "P \<Longrightarrow> p \<bullet> P"

  by(simp add: permute_bool_def)

subsection {* Permutations for sets *}

lemma permute_set_eq:

  fixes x::"'a::pt"

  and   p::"perm"

  shows "(p \<bullet> X) = {p \<bullet> x | x. x \<in> X}"

  unfolding permute_fun_def

  unfolding permute_bool_def

  apply(auto simp add: mem_def)

  apply(rule_tac x="- p \<bullet> x" in exI)

  apply(simp)

  done

lemma permute_set_eq_image:

  shows "p \<bullet> X = permute p ` X"

  unfolding permute_set_eq by auto

lemma permute_set_eq_vimage:

  shows "p \<bullet> X = permute (- p) -` X"