1 (*  Title:      Atoms

     2     Authors:    Brian Huffman, Christian Urban

     3 

     4     Instantiations of concrete atoms 

     5 *)

     6 theory Atoms

     7 imports Nominal2_Base

     8 uses "~~/src/Tools/subtyping.ML"

     9 begin

    10 

    11 

    12 

    13 section {* @{const nat_of} is an example of a function 

    14   without finite support *}

    15 

    16 

    17 lemma not_fresh_nat_of:

    18   shows "\<not> a \<sharp> nat_of"

    19 unfolding fresh_def supp_def

    20 proof (clarsimp)

    21   assume "finite {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"

    22   hence "finite ({a} \<union> {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of})"

    23     by simp

    24   then obtain b where

    25     b1: "b \<noteq> a" and

    26     b2: "sort_of b = sort_of a" and

    27     b3: "(a \<rightleftharpoons> b) \<bullet> nat_of = nat_of"

    28     by (rule obtain_atom) auto

    29   have "nat_of a = (a \<rightleftharpoons> b) \<bullet> (nat_of a)" by (simp add: permute_nat_def)

    30   also have "\<dots> = ((a \<rightleftharpoons> b) \<bullet> nat_of) ((a \<rightleftharpoons> b) \<bullet> a)" by (simp add: permute_fun_app_eq)

    31   also have "\<dots> = nat_of ((a \<rightleftharpoons> b) \<bullet> a)" using b3 by simp

    32   also have "\<dots> = nat_of b" using b2 by simp

    33   finally have "nat_of a = nat_of b" by simp

    34   with b2 have "a = b" by (simp add: atom_components_eq_iff)

    35   with b1 show "False" by simp

    36 qed

    37 

    38 lemma supp_nat_of:

    39   shows "supp nat_of = UNIV"

    40   using not_fresh_nat_of [unfolded fresh_def] by auto

    41 

    42 

    43 section {* Manual instantiation of class @{text at}. *}

    44 

    45 typedef (open) name = "{a. sort_of a = Sort ''name'' []}"

    46 by (rule exists_eq_simple_sort)

    47 

    48 instantiation name :: at

    49 begin

    50 

    51 definition

    52   "p \<bullet> a = Abs_name (p \<bullet> Rep_name a)"

    53 

    54 definition

    55   "atom a = Rep_name a"

    56 

    57 instance

    58 apply (rule at_class)

    59 apply (rule type_definition_name)

    60 apply (rule atom_name_def)

    61 apply (rule permute_name_def)

    62 done

    63 

    64 end

    65 

    66 lemma sort_of_atom_name: 

    67   shows "sort_of (atom (a::name)) = Sort ''name'' []"

    68   unfolding atom_name_def using Rep_name by simp

    69 

    70 text {* Custom syntax for concrete atoms of type at *}

    71 

    72 term "a:::name"

    73 

    74 text {* 

    75   a:::name stands for (atom a) with a being of concrete atom 

    76   type name. The above lemma can therefore also be stated as

    77 

    78   "sort_of (a:::name) = Sort ''name'' []"

    79 

    80   This does not work for multi-sorted atoms.

    81 *}

    82 

    83 

    84 section {* Automatic instantiation of class @{text at}. *}

    85 

    86 atom_decl name2

    87 

    88 lemma sort_of_atom_name2:

    89   "sort_of (atom (a::name2)) = Sort ''Atoms.name2'' []"

    90 unfolding atom_name2_def 

    91 using Rep_name2 

    92 by simp

    93 

    94 text {* example swappings *}

    95 lemma

    96   fixes a b::"atom"

    97   assumes "sort_of a = sort_of b"

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

    99 using assms

   100 by simp

   101 

   102 lemma

   103   fixes a b::"name2"

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

   105 by simp

   106 

   107 section {* An example for multiple-sort atoms *}

   108 

   109 datatype ty =

   110   TVar string

   111 | Fun ty ty ("_ \<rightarrow> _")

   112 

   113 primrec

   114   sort_of_ty::"ty \<Rightarrow> atom_sort"

   115 where

   116   "sort_of_ty (TVar s) = Sort ''TVar'' [Sort s []]"

   117 | "sort_of_ty (Fun ty1 ty2) = Sort ''Fun'' [sort_of_ty ty1, sort_of_ty ty2]"

   118 

   119 lemma sort_of_ty_eq_iff:

   120   shows "sort_of_ty x = sort_of_ty y \<longleftrightarrow> x = y"

   121 apply(induct x arbitrary: y)

   122 apply(case_tac [!] y)

   123 apply(simp_all)

   124 done

   125 

   126 declare sort_of_ty.simps [simp del]

   127 

   128 typedef (open) var = "{a. sort_of a \<in> range sort_of_ty}"

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

   130 

   131 instantiation var :: at_base

   132 begin

   133 

   134 definition

   135   "p \<bullet> a = Abs_var (p \<bullet> Rep_var a)"

   136 

   137 definition

   138   "atom a = Rep_var a"

   139 

   140 instance

   141 apply (rule at_base_class)

   142 apply (rule type_definition_var)

   143 apply (rule atom_var_def)

   144 apply (rule permute_var_def)

   145 done

   146 

   147 end

   148 

   149 text {* Constructor for variables. *}

   150 

   151 definition

   152   Var :: "nat \<Rightarrow> ty \<Rightarrow> var"

   153 where

   154   "Var x t = Abs_var (Atom (sort_of_ty t) x)"

   155 

   156 lemma Var_eq_iff [simp]:

   157   shows "Var x s = Var y t \<longleftrightarrow> x = y \<and> s = t"

   158   unfolding Var_def

   159   by (auto simp add: Abs_var_inject sort_of_ty_eq_iff)

   160 

   161 lemma sort_of_atom_var [simp]:

   162   "sort_of (atom (Var n ty)) = sort_of_ty ty"

   163   unfolding atom_var_def Var_def

   164   by (simp add: Abs_var_inverse)

   165 

   166 lemma 

   167   assumes "\<alpha> \<noteq> \<beta>" 

   168   shows "(Var x \<alpha> \<leftrightarrow> Var y \<alpha>) \<bullet> (Var x \<alpha>, Var x \<beta>) = (Var y \<alpha>, Var x \<beta>)"

   169   using assms by simp

   170 

   171 text {* Projecting out the type component of a variable. *}

   172 

   173 definition

   174   ty_of :: "var \<Rightarrow> ty"

   175 where

   176   "ty_of x = inv sort_of_ty (sort_of (atom x))"

   177 

   178 text {*

   179   Functions @{term Var}/@{term ty_of} satisfy many of the same

   180   properties as @{term Atom}/@{term sort_of}.

   181 *}

   182 

   183 lemma ty_of_Var [simp]:

   184   shows "ty_of (Var x t) = t"

   185   unfolding ty_of_def

   186   unfolding sort_of_atom_var

   187   apply (rule inv_f_f)

   188   apply (simp add: inj_on_def sort_of_ty_eq_iff)

   189   done

   190 

   191 lemma ty_of_permute [simp]:

   192   shows "ty_of (p \<bullet> x) = ty_of x"

   193   unfolding ty_of_def

   194   unfolding atom_eqvt [symmetric]

   195   by simp

   196 

   197 

   198 section {* Tests with subtyping and automatic coercions *}

   199 

   200 setup Subtyping.setup

   201 

   202 atom_decl var1

   203 atom_decl var2

   204 

   205 declare [[coercion "atom::var1\<Rightarrow>atom"]]

   206 

   207 declare [[coercion "atom::var2\<Rightarrow>atom"]]

   208 

   209 lemma

   210   fixes a::"var1" and b::"var2"

   211   shows "a \<sharp> t \<and> b \<sharp> t"

   212 oops

   213 

   214 (* does not yet work: it needs image as

   215    coercion map *)

   216 

   217 lemma

   218   fixes as::"var1 set"

   219   shows "atom ` as \<sharp>* t"

   220 oops

   221 

   222 end