1 theory Name_Exec

     2 imports "../../Nominal2"

     3 begin

     4 

     5 atom_decl name

     6 

     7 definition Name :: "nat \<Rightarrow> name" where "Name n = Abs_name (Atom (Sort ''Name_Exec.name'' []) n)"

     8 

     9 definition "nat_of_name n = nat_of (Rep_name n)"

    10 

    11 code_datatype Name

    12 

    13 definition [code]: "N0 = Name 0"

    14 definition [code]: "N1 = Name 1"

    15 definition [code]: "N2 = Name 2"

    16 

    17 instantiation name :: equal begin

    18 

    19 definition equal_name_def: "equal_name a b \<longleftrightarrow> nat_of_name a = nat_of_name b"

    20 

    21 instance

    22   by default

    23     (metis (lifting) Rep_name_inject atom_components_eq_iff atom_name_def equal_name_def nat_of_name_def sort_of_atom_eq)

    24 

    25 end

    26 

    27 lemma [simp]: "nat_of_name (Name n) = n"

    28   unfolding nat_of_name_def Name_def

    29   by (simp add: Abs_name_inverse)

    30 

    31 lemma equal_name_code [code]: "(equal_class.equal (Name x) (Name y)) \<longleftrightarrow> (x = y)"

    32   by (auto simp add: equal_name_def)

    33 

    34 lemma atom_name_code[code]:

    35   "atom (Name n) = Atom (Sort ''Name_Exec.name'' []) n"

    36   by (simp add: Abs_name_inject[symmetric] Name_def)

    37      (simp add: atom_name_def Rep_name_inverse)

    38 

    39 lemma permute_name_code[code]: "p \<bullet> n = Name (nat_of (p \<bullet> (atom n)))"

    40   apply (simp add: atom_eqvt)

    41   apply (simp add: atom_name_def Name_def)

    42   by (metis Rep_name_inverse atom_name_def atom_name_sort nat_of.simps sort_of.simps atom.exhaust)

    43 

    44 (*

    45 Test:

    46 definition "t \<longleftrightarrow> 0 = (N0 \<leftrightarrow> N1)"

    47 

    48 export_code t in SML

    49 

    50 value "(N0 \<leftrightarrow> N1) + (N1 \<leftrightarrow> N0) = 0"

    51 *)

    52 

    53 end

    54 

    55 

    56