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         Nominal2_Eqvt

     9 uses ("nominal_atoms.ML")

    10 begin

    11 

    12 section {* Infrastructure for concrete atom types *}

    13 

    14 

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

    16   

    17 definition

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

    19 where

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

    21 

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

    23   unfolding flip_def by (rule swap_self)

    24 

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

    26   unfolding flip_def by (rule swap_commute)

    27 

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

    29   unfolding flip_def by (rule minus_swap)

    30 

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

    32   unfolding flip_def by (rule swap_cancel)

    33 

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

    35   unfolding permute_plus [symmetric] add_flip_cancel by simp

    36 

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

    38   by (simp add: flip_commute)

    39 

    40 lemma flip_eqvt[eqvt]: 

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

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

    43   unfolding flip_def

    44   by (simp add: swap_eqvt atom_eqvt)

    45 

    46 lemma flip_at_base_simps [simp]:

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

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

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

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

    51   unfolding flip_def

    52   unfolding atom_eq_iff [symmetric]

    53   unfolding atom_eqvt [symmetric]

    54   by simp_all

    55 

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

    57   only for single sort atoms from at *}

    58 

    59 lemma permute_flip_at:

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

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

    62   unfolding flip_def

    63   apply (rule atom_eq_iff [THEN iffD1])

    64   apply (subst atom_eqvt [symmetric])

    65   apply (simp add: swap_atom)

    66   done

    67 

    68 lemma flip_at_simps [simp]:

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

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

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

    72   unfolding permute_flip_at by simp_all

    73 

    74 lemma flip_fresh_fresh:

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

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

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

    78 using assms

    79 by (simp add: flip_def swap_fresh_fresh)

    80 

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

    82 

    83 syntax

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

    85 

    86 translations

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

    88 

    89 

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

    91 

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

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

    94 

    95 text {*

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

    97 *}

    98 

    99 lemma exists_eq_simple_sort: 

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

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

   102 

   103 lemma exists_eq_sort: 

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

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

   106 

   107 lemma at_base_class:

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

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

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

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

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

   113   shows "OFCLASS('a, at_base_class)"

   114 proof

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

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

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

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

   119     unfolding permute_def by (simp add: Rep_inverse)

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

   121     unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)

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

   123     unfolding atom_def by (simp add: Rep_inject)

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

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

   126 qed

   127 

   128 (*

   129 lemma at_class:

   130   fixes s :: atom_sort

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

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

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

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

   135   shows "OFCLASS('a, at_class)"

   136 proof

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

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

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

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

   141     unfolding permute_def by (simp add: Rep_inverse)

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

   143     unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)

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

   145     unfolding atom_def by (simp add: sort_of_Rep)

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

   147     unfolding atom_def by (simp add: Rep_inject)

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

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

   150 qed

   151 *)

   152 

   153 lemma at_class:

   154   fixes s :: atom_sort

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

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

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

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

   159   shows "OFCLASS('a, at_class)"

   160 proof

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

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

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

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

   165     unfolding permute_def by (simp add: Rep_inverse)

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

   167     unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)

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

   169     unfolding atom_def by (simp add: sort_of_Rep)

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

   171     unfolding atom_def by (simp add: Rep_inject)

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

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

   174 qed

   175 

   176 setup {* Sign.add_const_constraint

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

   178 setup {* Sign.add_const_constraint

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

   180 

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

   182 

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

   184 

   185 use "nominal_atoms.ML"

   186 

   187 

   188 end