(*  Title:      Nominal2_Atoms

    Authors:    Brian Huffman, Christian Urban

    Definitions for concrete atom types. 

*)

theory Nominal2_Atoms

imports Nominal2_Base

        Nominal2_Eqvt

uses ("nominal_atoms.ML")

begin

section {* Concrete atom types *}

text {*

  Class @{text at_base} allows types containing multiple sorts of atoms.

  Class @{text at} only allows types with a single sort.

*}

lemma atom_image_cong:

  shows "(atom ` X = atom ` Y) = (X = Y)"

  apply(rule inj_image_eq_iff)

  apply(simp add: inj_on_def)

  done

lemma atom_image_supp:

  "supp S = supp (atom ` S)"

  apply(simp add: supp_def)

  apply(simp add: image_eqvt)

  apply(subst (2) permute_fun_def)

  apply(simp add: atom_eqvt)

  apply(simp add: atom_image_cong)

  done

lemma supp_finite_at_set:

  assumes a: "finite S"

  shows "supp S = atom ` S"

qed

lemma supp_at_insert:

  assumes a: "finite S"

  shows "supp (insert a S) = supp a \<union> supp S"

  using a by (simp add: supp_finite_at_set supp_at_base)

section {* A swapping operation for concrete atoms *}

definition

  flip :: "'a::at_base \<Rightarrow> 'a \<Rightarrow> perm" ("'(_ \<leftrightarrow> _')")

where

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

lemma flip_self [simp]: "(a \<leftrightarrow> a) = 0"

  unfolding flip_def by (rule swap_self)

lemma flip_commute: "(a \<leftrightarrow> b) = (b \<leftrightarrow> a)"

  unfolding flip_def by (rule swap_commute)

lemma minus_flip [simp]: "- (a \<leftrightarrow> b) = (a \<leftrightarrow> b)"

  unfolding flip_def by (rule minus_swap)

lemma add_flip_cancel: "(a \<leftrightarrow> b) + (a \<leftrightarrow> b) = 0"

  unfolding flip_def by (rule swap_cancel)

lemma permute_flip_cancel [simp]: "(a \<leftrightarrow> b) \<bullet> (a \<leftrightarrow> b) \<bullet> x = x"

  unfolding permute_plus [symmetric] add_flip_cancel by simp

lemma permute_flip_cancel2 [simp]: "(a \<leftrightarrow> b) \<bullet> (b \<leftrightarrow> a) \<bullet> x = x"

  by (simp add: flip_commute)

lemma flip_eqvt: 

  fixes a b c::"'a::at_base"

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

  unfolding flip_def

  by (simp add: swap_eqvt atom_eqvt)

lemma flip_at_base_simps [simp]:

  shows "sort_of (atom a) = sort_of (atom b) \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> a = b"

  and   "sort_of (atom a) = sort_of (atom b) \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> b = a"

  and   "\<lbrakk>a \<noteq> c; b \<noteq> c\<rbrakk> \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> c = c"

  and   "sort_of (atom a) \<noteq> sort_of (atom b) \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> x = x"

  unfolding flip_def

  unfolding atom_eq_iff [symmetric]

  unfolding atom_eqvt [symmetric]

  by simp_all

text {* the following two lemmas do not hold for at_base, 

  only for single sort atoms from at *}

lemma permute_flip_at:

  fixes a b c::"'a::at"

  shows "(a \<leftrightarrow> b) \<bullet> c = (if c = a then b else if c = b then a else c)"

  unfolding flip_def

  apply (rule atom_eq_iff [THEN iffD1])

  apply (subst atom_eqvt [symmetric])

  apply (simp add: swap_atom)

  done

lemma flip_at_simps [simp]:

  fixes a b::"'a::at"

  shows "(a \<leftrightarrow> b) \<bullet> a = b" 

  and   "(a \<leftrightarrow> b) \<bullet> b = a"

  unfolding permute_flip_at by simp_all

lemma flip_fresh_fresh:

  fixes a b::"'a::at_base"

  assumes "atom a \<sharp> x" "atom b \<sharp> x"

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

using assms

by (simp add: flip_def swap_fresh_fresh)

subsection {* Syntax for coercing at-elements to the atom-type *}

syntax

  "_atom_constrain" :: "logic \<Rightarrow> type \<Rightarrow> logic" ("_:::_" [4, 0] 3)

translations

  "_atom_constrain a t" => "CONST atom (_constrain a t)"

subsection {* A lemma for proving instances of class @{text at}. *}

setup {* Sign.add_const_constraint (@{const_name "permute"}, NONE) *}

setup {* Sign.add_const_constraint (@{const_name "atom"}, NONE) *}

text {*

  New atom types are defined as subtypes of @{typ atom}.

*}

lemma exists_eq_simple_sort: 

  shows "\<exists>a. a \<in> {a. sort_of a = s}"

  by (rule_tac x="Atom s 0" in exI, simp)

lemma exists_eq_sort: 

  shows "\<exists>a. a \<in> {a. sort_of a \<in> range sort_fun}"

  by (rule_tac x="Atom (sort_fun x) y" in exI, simp)

lemma at_base_class:

  fixes sort_fun :: "'b \<Rightarrow>atom_sort"

  fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"

  assumes type: "type_definition Rep Abs {a. sort_of a \<in> range sort_fun}"

  assumes atom_def: "\<And>a. atom a = Rep a"

  assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)"

  shows "OFCLASS('a, at_base_class)"

proof

  interpret type_definition Rep Abs "{a. sort_of a \<in> range sort_fun}" by (rule type)

  have sort_of_Rep: "\<And>a. sort_of (Rep a) \<in> range sort_fun" using Rep by simp

  fix a b :: 'a and p p1 p2 :: perm

  show "0 \<bullet> a = a"

    unfolding permute_def by (simp add: Rep_inverse)

  show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a"

    unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)

  show "atom a = atom b \<longleftrightarrow> a = b"

    unfolding atom_def by (simp add: Rep_inject)

  show "p \<bullet> atom a = atom (p \<bullet> a)"

    unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)

qed

(*

lemma at_class:

  fixes s :: atom_sort

  fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"

  assumes type: "type_definition Rep Abs {a. sort_of a \<in> range (\<lambda>x::unit. s)}"

  assumes atom_def: "\<And>a. atom a = Rep a"

  assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)"

  shows "OFCLASS('a, at_class)"

proof

  interpret type_definition Rep Abs "{a. sort_of a \<in> range (\<lambda>x::unit. s)}" by (rule type)

  have sort_of_Rep: "\<And>a. sort_of (Rep a) = s" using Rep by (simp add: image_def)

  fix a b :: 'a and p p1 p2 :: perm

  show "0 \<bullet> a = a"

    unfolding permute_def by (simp add: Rep_inverse)

  show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a"

    unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)

  show "sort_of (atom a) = sort_of (atom b)"

    unfolding atom_def by (simp add: sort_of_Rep)

  show "atom a = atom b \<longleftrightarrow> a = b"

    unfolding atom_def by (simp add: Rep_inject)

  show "p \<bullet> atom a = atom (p \<bullet> a)"

    unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)

qed

*)

lemma at_class:

  fixes s :: atom_sort

  fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"

  assumes type: "type_definition Rep Abs {a. sort_of a = s}"

  assumes atom_def: "\<And>a. atom a = Rep a"

  assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)"

  shows "OFCLASS('a, at_class)"

proof

  interpret type_definition Rep Abs "{a. sort_of a = s}" by (rule type)

  have sort_of_Rep: "\<And>a. sort_of (Rep a) = s" using Rep by (simp add: image_def)

  fix a b :: 'a and p p1 p2 :: perm

  show "0 \<bullet> a = a"

    unfolding permute_def by (simp add: Rep_inverse)

  show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a"

    unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)

  show "sort_of (atom a) = sort_of (atom b)"

    unfolding atom_def by (simp add: sort_of_Rep)

  show "atom a = atom b \<longleftrightarrow> a = b"

    unfolding atom_def by (simp add: Rep_inject)

  show "p \<bullet> atom a = atom (p \<bullet> a)"

    unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)

qed

setup {* Sign.add_const_constraint

  (@{const_name "permute"}, SOME @{typ "perm \<Rightarrow> 'a::pt \<Rightarrow> 'a"}) *}

setup {* Sign.add_const_constraint

  (@{const_name "atom"}, SOME @{typ "'a::at_base \<Rightarrow> atom"}) *}

section {* Automation for creating concrete atom types *}

text {* at the moment only single-sort concrete atoms are supported *}

use "nominal_atoms.ML"

end