(*  Title:      Nominal2_Base

    Authors:    Christian Urban, Brian Huffman, Cezary Kaliszyk

    Basic definitions and lemma infrastructure for 

    Nominal Isabelle. 

*)

theory Nominal2_Base

imports Main 

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

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

        "GPerm"

  "~~/src/HOL/Library/List_lexord"

  "~~/src/HOL/Library/Product_ord"

  "~~/src/HOL/Library/Efficient_Nat"

  "~~/src/HOL/Library/Char_ord"

  "~~/src/HOL/Library/Code_Char_chr"

  "~~/src/HOL/Library/Code_Char_ord"

keywords

  "atom_decl" "equivariance" :: thy_decl

uses ("nominal_basics.ML")

     ("nominal_thmdecls.ML")

     ("nominal_permeq.ML")

     ("nominal_library.ML")

     ("nominal_atoms.ML")

     ("nominal_eqvt.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 n) = 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 *}

definition "sort_respecting p \<longleftrightarrow> (\<forall>a. sort_of (gpermute p a) = sort_of a)"

lemma sort_respecting_0[simp]:

  "sort_respecting (0\<Colon>atom gperm)"

  by (simp add: sort_respecting_def)

typedef (open) perm = "{p::atom gperm. sort_respecting p}"

  by (auto intro: exI[of _ "0"])

setup_lifting type_definition_perm

lemma perm_eq_rep:

  "p = q \<longleftrightarrow> Rep_perm p = Rep_perm q"

  by (simp add: Rep_perm_inject)

lift_definition mk_perm :: "atom gperm \<Rightarrow> perm" is

  "\<lambda>p. if sort_respecting p then p else 0" by simp

lemma Rep_perm_mk_perm [simp]:

  "Rep_perm (mk_perm p) = (if sort_respecting p then p else 0)"

  by (simp add: mk_perm_def Abs_perm_inverse)

instance perm :: size ..

subsection {* Permutations form a (multiplicative) group *}

instantiation perm :: group_add

begin

lift_definition zero_perm :: "perm" is "0" by simp

lift_definition uminus_perm :: "perm \<Rightarrow> perm" is "uminus"

  unfolding sort_respecting_def

  by transfer (auto, metis perm_apply_minus)

lift_definition plus_perm :: "perm \<Rightarrow> perm \<Rightarrow> perm" is "plus"

  unfolding sort_respecting_def

  by transfer (simp add: perm_add_apply)

definition "(p :: perm) - q = p + - q"

lemma Rep_perm_0 [simp, code abstract]:

  "Rep_perm 0 = 0"

  by (metis (mono_tags) zero_perm.rep_eq)

lemma Rep_perm_uminus [simp, code abstract]:

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

  by (metis uminus_perm.rep_eq)

lemma Rep_perm_add [simp, code abstract]:

  "Rep_perm (p + q) = (Rep_perm p) + (Rep_perm q)"

  by (simp add: plus_perm.rep_eq)

instance

  apply default

  unfolding minus_perm_def

  by (transfer, simp add: add_assoc)+

end

section {* Implementation of swappings *}

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

  is "(\<lambda>a b. (if sort_of a = sort_of b then mk_perm (gswap a b) else 0))" .

lemma sort_respecting_swap [simp]:

  "sort_of a = sort_of b \<Longrightarrow> sort_respecting (gswap a b)"

  unfolding sort_respecting_def

  by transfer auto

lemma Rep_swap [simp, code abstract]:

  "Rep_perm (swap a b) = (if sort_of a = sort_of b then gswap a b else 0)"

  by (simp add: swap_def)

lemma swap_different_sorts [simp]:

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

  by (simp add: perm_eq_rep)

lemma swap_cancel:

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

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

  by (simp_all add: perm_eq_rep)

lemma swap_self [simp]:

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

  by (simp add: perm_eq_rep)

lemma minus_swap [simp]:

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

  by (simp add: perm_eq_rep)

lemma swap_commute:

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

  by (simp add: perm_eq_rep swap_commute)

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 (simp add: perm_eq_rep swap_triple)

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 = gpermute (Rep_perm p) a"

instance

  by default (simp_all add: permute_atom_def)

end

lemma sort_of_permute [simp]:

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

  by (metis Rep_perm mem_Collect_eq sort_respecting_def permute_atom_def)

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)"

  by (auto simp add: permute_atom_def)

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

  fixes p q :: "perm"

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

  unfolding permute_atom_def perm_eq_rep

  by (simp add: gperm_eq)

subsection {* Permutations for permutations *}

instantiation perm :: pt

begin

definition

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

instance

  by default

     (simp_all add: permute_perm_def diff_minus minus_add add_assoc)

end

lemma permute_self:

  shows "p \<bullet> p = p"

  unfolding permute_perm_def

  by (simp add: diff_minus add_assoc)

lemma pemute_minus_self:

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

  unfolding permute_perm_def

  by (simp add: diff_minus 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

  by default

     (simp_all add: permute_fun_def minus_add)

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

  by (default)

     (simp_all add: permute_bool_def)

end

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 *}

instantiation "set" :: (pt) pt

begin

definition

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

instance

apply default

apply (auto simp add: permute_set_def)

done

end

lemma permute_set_eq:

  shows "p \<bullet> X = {x. - p \<bullet> x \<in> X}"

unfolding permute_set_def

by (auto) (metis permute_minus_cancel(1))

lemma permute_set_eq_image:

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

  unfolding permute_set_def by auto

lemma permute_set_eq_vimage:

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

  unfolding permute_set_eq vimage_def

  by simp

lemma permute_finite [simp]:

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

  unfolding permute_set_eq_vimage

  using bij_permute by (rule finite_vimage_iff)

lemma swap_set_not_in:

  assumes a: "a \<notin> S" "b \<notin> S"

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

  unfolding permute_set_def

  using a by (auto simp add: swap_atom)

lemma swap_set_in:

  assumes a: "a \<in> S" "b \<notin> S" "sort_of a = sort_of b"

  shows "(a \<rightleftharpoons> b) \<bullet> S \<noteq> S"

  unfolding permute_set_def

  using a by (auto simp add: swap_atom)

lemma swap_set_in_eq:

  assumes a: "a \<in> S" "b \<notin> S" "sort_of a = sort_of b"

  shows "(a \<rightleftharpoons> b) \<bullet> S = (S - {a}) \<union> {b}"

  unfolding permute_set_def

  using a by (auto simp add: swap_atom)

lemma swap_set_both_in:

  assumes a: "a \<in> S" "b \<in> S"

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

  unfolding permute_set_def

  using a by (auto simp add: swap_atom)

lemma mem_permute_iff:

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

  unfolding permute_set_def

  by auto

lemma empty_eqvt:

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

  unfolding permute_set_def

  by (simp)

lemma insert_eqvt:

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

  unfolding permute_set_eq_image image_insert ..

subsection {* Permutations for @{typ unit} *}

instantiation unit :: pt

begin

definition "p \<bullet> (u::unit) = u"

instance 

by (default) (simp_all add: permute_unit_def)

end

subsection {* Permutations for products *}

instantiation prod :: (pt, pt) pt

begin

primrec 

  permute_prod 

where

  Pair_eqvt: "p \<bullet> (x, y) = (p \<bullet> x, p \<bullet> y)"

instance

by default auto

end

subsection {* Permutations for sums *}

instantiation sum :: (pt, pt) pt

begin

primrec 

  permute_sum 

where

  Inl_eqvt: "p \<bullet> (Inl x) = Inl (p \<bullet> x)"

| Inr_eqvt: "p \<bullet> (Inr y) = Inr (p \<bullet> y)"

instance 

by (default) (case_tac [!] x, simp_all)

end

subsection {* Permutations for @{typ "'a list"} *}

instantiation list :: (pt) pt

begin

primrec 

  permute_list 

where

  Nil_eqvt:  "p \<bullet> [] = []"

| Cons_eqvt: "p \<bullet> (x # xs) = p \<bullet> x # p \<bullet> xs"

instance 

by (default) (induct_tac [!] x, simp_all)

end

lemma set_eqvt:

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

  by (induct xs) (simp_all add: empty_eqvt insert_eqvt)

subsection {* Permutations for @{typ "'a option"} *}

instantiation option :: (pt) pt

begin

primrec 

  permute_option 

where

  None_eqvt: "p \<bullet> None = None"

| Some_eqvt: "p \<bullet> (Some x) = Some (p \<bullet> x)"

instance 

by (default) (induct_tac [!] x, simp_all)

end

subsection {* Permutations for @{typ "'a multiset"} *}

instantiation multiset :: (pt) pt

begin

definition

  "p \<bullet> M = {# p \<bullet> x. x :# M #}"

instance 

proof

  fix M :: "'a multiset" and p q :: "perm"