1 (*  Title:      Nominal2_Atoms

     2     Authors:    Brian Huffman, Christian Urban

     3 

     4     Definitions for concrete atom types. 

     5 *)

     6 theory Nominal2_Atoms

     7 imports Nominal2_Base

     8 uses ("nominal_atoms.ML")

     9 begin

    10 

    11 section {* Concrete atom types *}

    12 

    13 text {*

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

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

    16 *}

    17 

    18 class at_base = pt +

    19   fixes atom :: "'a \<Rightarrow> atom"

    20   assumes atom_eq_iff [simp]: "atom a = atom b \<longleftrightarrow> a = b"

    21   assumes atom_eqvt: "p \<bullet> (atom a) = atom (p \<bullet> a)"

    22 

    23 class at = at_base +

    24   assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)"

    25 

    26 lemma supp_at_base: 

    27   fixes a::"'a::at_base"

    28   shows "supp a = {atom a}"

    29   by (simp add: supp_atom [symmetric] supp_def atom_eqvt)

    30 

    31 lemma fresh_at_base: 

    32   shows "a \<sharp> b \<longleftrightarrow> a \<noteq> atom b"

    33   unfolding fresh_def by (simp add: supp_at_base)

    34 

    35 instance at_base < fs

    36 proof qed (simp add: supp_at_base)

    37 

    38 lemma at_base_infinite [simp]:

    39   shows "infinite (UNIV :: 'a::at_base set)" (is "infinite ?U")

    40 proof

    41   obtain a :: 'a where "True" by auto

    42   assume "finite ?U"

    43   hence "finite (atom ` ?U)"

    44     by (rule finite_imageI)

    45   then obtain b where b: "b \<notin> atom ` ?U" "sort_of b = sort_of (atom a)"

    46     by (rule obtain_atom)

    47   from b(2) have "b = atom ((atom a \<rightleftharpoons> b) \<bullet> a)"

    48     unfolding atom_eqvt [symmetric]

    49     by (simp add: swap_atom)

    50   hence "b \<in> atom ` ?U" by simp

    51   with b(1) show "False" by simp

    52 qed

    53 

    54 lemma swap_at_base_simps [simp]:

    55   fixes x y::"'a::at_base"

    56   shows "sort_of (atom x) = sort_of (atom y) \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> x = y"

    57   and   "sort_of (atom x) = sort_of (atom y) \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> y = x"

    58   and   "atom x \<noteq> a \<Longrightarrow> atom x \<noteq> b \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> x = x"

    59   unfolding atom_eq_iff [symmetric]

    60   unfolding atom_eqvt [symmetric]

    61   by simp_all

    62 

    63 lemma obtain_at_base:

    64   assumes X: "finite X"

    65   obtains a::"'a::at_base" where "atom a \<notin> X"

    66 proof -

    67   have "inj (atom :: 'a \<Rightarrow> atom)"

    68     by (simp add: inj_on_def)

    69   with X have "finite (atom -` X :: 'a set)"

    70     by (rule finite_vimageI)

    71   with at_base_infinite have "atom -` X \<noteq> (UNIV :: 'a set)"

    72     by auto

    73   then obtain a :: 'a where "atom a \<notin> X"

    74     by auto

    75   thus ?thesis ..

    76 qed

    77 

    78 

    79 section {* A swapping operation for concrete atoms *}

    80   

    81 definition

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

    83 where

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

    85 

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

    87   unfolding flip_def by (rule swap_self)

    88 

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

    90   unfolding flip_def by (rule swap_commute)

    91 

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

    93   unfolding flip_def by (rule minus_swap)

    94 

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

    96   unfolding flip_def by (rule swap_cancel)

    97 

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

    99   unfolding permute_plus [symmetric] add_flip_cancel by simp

   100 

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

   102   by (simp add: flip_commute)

   103 

   104 lemma flip_eqvt: 

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

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

   107   unfolding flip_def

   108   by (simp add: swap_eqvt atom_eqvt)

   109 

   110 lemma flip_at_base_simps [simp]:

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

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

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

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

   115   unfolding flip_def

   116   unfolding atom_eq_iff [symmetric]

   117   unfolding atom_eqvt [symmetric]

   118   by simp_all

   119 

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

   121   only for single sort atoms from at *}

   122 

   123 lemma permute_flip_at:

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

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

   126   unfolding flip_def

   127   apply (rule atom_eq_iff [THEN iffD1])

   128   apply (subst atom_eqvt [symmetric])

   129   apply (simp add: swap_atom)

   130   done

   131 

   132 lemma flip_at_simps [simp]:

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

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

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

   136   unfolding permute_flip_at by simp_all

   137 

   138 lemma flip_fresh_fresh:

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

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

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

   142 using assms

   143 by (simp add: flip_def swap_fresh_fresh)

   144 

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

   146 

   147 syntax

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

   149 

   150 translations

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

   152 

   153 

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

   155 

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

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

   158 

   159 text {*

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

   161 *}

   162 

   163 lemma exists_eq_simple_sort: 

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

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

   166 

   167 lemma exists_eq_sort: 

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

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

   170 

   171 lemma at_base_class:

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

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

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

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

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

   177   shows "OFCLASS('a, at_base_class)"

   178 proof

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

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

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

   182   show "0 \<bullet> a = a"

   183     unfolding permute_def by (simp add: Rep_inverse)

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

   185     unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)

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

   187     unfolding atom_def by (simp add: Rep_inject)

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

   189     unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)

   190 qed

   191 

   192 (*

   193 lemma at_class:

   194   fixes s :: atom_sort

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

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

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

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

   199   shows "OFCLASS('a, at_class)"

   200 proof

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

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

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

   204   show "0 \<bullet> a = a"

   205     unfolding permute_def by (simp add: Rep_inverse)

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

   207     unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)

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

   209     unfolding atom_def by (simp add: sort_of_Rep)

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

   211     unfolding atom_def by (simp add: Rep_inject)

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

   213     unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)

   214 qed

   215 *)

   216 

   217 lemma at_class:

   218   fixes s :: atom_sort

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

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

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

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

   223   shows "OFCLASS('a, at_class)"

   224 proof

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

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

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

   228   show "0 \<bullet> a = a"

   229     unfolding permute_def by (simp add: Rep_inverse)

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

   231     unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)

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

   233     unfolding atom_def by (simp add: sort_of_Rep)

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

   235     unfolding atom_def by (simp add: Rep_inject)

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

   237     unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)

   238 qed

   239 

   240 setup {* Sign.add_const_constraint

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

   242 setup {* Sign.add_const_constraint

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

   244 

   245 

   246 section {* Automation for creating concrete atom types *}

   247 

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

   249 

   250 use "nominal_atoms.ML"

   251 

   252 

   253 

   254 

   255 end