|
1 (* Title: Atoms |
|
2 Authors: Brian Huffman, Christian Urban |
|
3 |
|
4 Instantiations of concrete atoms |
|
5 *) |
|
6 theory Atoms |
|
7 imports Nominal2_Atoms |
|
8 begin |
|
9 |
|
10 section {* Manual instantiation of class @{text at}. *} |
|
11 |
|
12 typedef (open) name = "{a. sort_of a = Sort ''name'' []}" |
|
13 by (rule exists_eq_simple_sort) |
|
14 |
|
15 instantiation name :: at |
|
16 begin |
|
17 |
|
18 definition |
|
19 "p \<bullet> a = Abs_name (p \<bullet> Rep_name a)" |
|
20 |
|
21 definition |
|
22 "atom a = Rep_name a" |
|
23 |
|
24 instance |
|
25 apply (rule at_class) |
|
26 apply (rule type_definition_name) |
|
27 apply (rule atom_name_def) |
|
28 apply (rule permute_name_def) |
|
29 done |
|
30 |
|
31 end |
|
32 |
|
33 lemma sort_of_atom_name: |
|
34 shows "sort_of (atom (a::name)) = Sort ''name'' []" |
|
35 unfolding atom_name_def using Rep_name by simp |
|
36 |
|
37 text {* Custom syntax for concrete atoms of type at *} |
|
38 |
|
39 term "a:::name" |
|
40 |
|
41 text {* |
|
42 a:::name stands for (atom a) with a being of concrete atom |
|
43 type name. The above lemma can therefore also be stated as |
|
44 |
|
45 "sort_of (a:::name) = Sort ''name'' []" |
|
46 |
|
47 This does not work for multi-sorted atoms. |
|
48 *} |
|
49 |
|
50 |
|
51 section {* Automatic instantiation of class @{text at}. *} |
|
52 |
|
53 atom_decl name2 |
|
54 |
|
55 lemma sort_of_atom_name2: |
|
56 "sort_of (atom (a::name2)) = Sort ''Atoms.name2'' []" |
|
57 unfolding atom_name2_def |
|
58 using Rep_name2 |
|
59 by simp |
|
60 |
|
61 text {* example swappings *} |
|
62 lemma |
|
63 fixes a b::"atom" |
|
64 assumes "sort_of a = sort_of b" |
|
65 shows "(a \<rightleftharpoons> b) \<bullet> (a, b) = (b, a)" |
|
66 using assms |
|
67 by simp |
|
68 |
|
69 lemma |
|
70 fixes a b::"name2" |
|
71 shows "(a \<leftrightarrow> b) \<bullet> (a, b) = (b, a)" |
|
72 by simp |
|
73 |
|
74 section {* An example for multiple-sort atoms *} |
|
75 |
|
76 datatype ty = |
|
77 TVar string |
|
78 | Fun ty ty ("_ \<rightarrow> _") |
|
79 |
|
80 primrec |
|
81 sort_of_ty::"ty \<Rightarrow> atom_sort" |
|
82 where |
|
83 "sort_of_ty (TVar s) = Sort ''TVar'' [Sort s []]" |
|
84 | "sort_of_ty (Fun ty1 ty2) = Sort ''Fun'' [sort_of_ty ty1, sort_of_ty ty2]" |
|
85 |
|
86 lemma sort_of_ty_eq_iff: |
|
87 shows "sort_of_ty x = sort_of_ty y \<longleftrightarrow> x = y" |
|
88 apply(induct x arbitrary: y) |
|
89 apply(case_tac [!] y) |
|
90 apply(simp_all) |
|
91 done |
|
92 |
|
93 declare sort_of_ty.simps [simp del] |
|
94 |
|
95 typedef (open) var = "{a. sort_of a \<in> range sort_of_ty}" |
|
96 by (rule_tac x="Atom (sort_of_ty x) y" in exI, simp) |
|
97 |
|
98 instantiation var :: at_base |
|
99 begin |
|
100 |
|
101 definition |
|
102 "p \<bullet> a = Abs_var (p \<bullet> Rep_var a)" |
|
103 |
|
104 definition |
|
105 "atom a = Rep_var a" |
|
106 |
|
107 instance |
|
108 apply (rule at_base_class) |
|
109 apply (rule type_definition_var) |
|
110 apply (rule atom_var_def) |
|
111 apply (rule permute_var_def) |
|
112 done |
|
113 |
|
114 end |
|
115 |
|
116 text {* Constructor for variables. *} |
|
117 |
|
118 definition |
|
119 Var :: "nat \<Rightarrow> ty \<Rightarrow> var" |
|
120 where |
|
121 "Var x t = Abs_var (Atom (sort_of_ty t) x)" |
|
122 |
|
123 lemma Var_eq_iff [simp]: |
|
124 shows "Var x s = Var y t \<longleftrightarrow> x = y \<and> s = t" |
|
125 unfolding Var_def |
|
126 by (auto simp add: Abs_var_inject sort_of_ty_eq_iff) |
|
127 |
|
128 lemma sort_of_atom_var [simp]: |
|
129 "sort_of (atom (Var n ty)) = sort_of_ty ty" |
|
130 unfolding atom_var_def Var_def |
|
131 by (simp add: Abs_var_inverse) |
|
132 |
|
133 lemma |
|
134 assumes "\<alpha> \<noteq> \<beta>" |
|
135 shows "(Var x \<alpha> \<leftrightarrow> Var y \<alpha>) \<bullet> (Var x \<alpha>, Var x \<beta>) = (Var y \<alpha>, Var x \<beta>)" |
|
136 using assms by simp |
|
137 |
|
138 text {* Projecting out the type component of a variable. *} |
|
139 |
|
140 definition |
|
141 ty_of :: "var \<Rightarrow> ty" |
|
142 where |
|
143 "ty_of x = inv sort_of_ty (sort_of (atom x))" |
|
144 |
|
145 text {* |
|
146 Functions @{term Var}/@{term ty_of} satisfy many of the same |
|
147 properties as @{term Atom}/@{term sort_of}. |
|
148 *} |
|
149 |
|
150 lemma ty_of_Var [simp]: |
|
151 shows "ty_of (Var x t) = t" |
|
152 unfolding ty_of_def |
|
153 unfolding sort_of_atom_var |
|
154 apply (rule inv_f_f) |
|
155 apply (simp add: inj_on_def sort_of_ty_eq_iff) |
|
156 done |
|
157 |
|
158 lemma ty_of_permute [simp]: |
|
159 shows "ty_of (p \<bullet> x) = ty_of x" |
|
160 unfolding ty_of_def |
|
161 unfolding atom_eqvt [symmetric] |
|
162 by simp |
|
163 |
|
164 end |