48 thm tys2.size_eqvt |
49 thm tys2.size_eqvt |
49 thm tys2.supports |
50 thm tys2.supports |
50 thm tys2.supp |
51 thm tys2.supp |
51 thm tys2.fresh |
52 thm tys2.fresh |
52 |
53 |
|
54 fun |
|
55 lookup :: "(name \<times> ty2) list \<Rightarrow> name \<Rightarrow> ty2" |
|
56 where |
|
57 "lookup [] Y = Var2 Y" |
|
58 | "lookup ((X, T) # Ts) Y = (if X = Y then T else lookup Ts Y)" |
53 |
59 |
54 text {* Some Tests *} |
60 lemma lookup_eqvt[eqvt]: |
|
61 shows "(p \<bullet> lookup Ts T) = lookup (p \<bullet> Ts) (p \<bullet> T)" |
|
62 apply(induct Ts T rule: lookup.induct) |
|
63 apply(simp_all) |
|
64 done |
|
65 |
|
66 function |
|
67 subst :: "(name \<times> ty2) list \<Rightarrow> ty2 \<Rightarrow> ty2" |
|
68 where |
|
69 "subst \<theta> (Var2 X) = lookup \<theta> X" |
|
70 | "subst \<theta> (Fun2 T1 T2) = Fun2 (subst \<theta> T1) (subst \<theta> T2)" |
|
71 apply(case_tac x) |
|
72 apply(simp) |
|
73 apply(rule_tac y="b" in ty2.exhaust) |
|
74 apply(blast) |
|
75 apply(blast) |
|
76 apply(simp_all add: ty2.distinct) |
|
77 apply(simp add: ty2.eq_iff) |
|
78 apply(simp add: ty2.eq_iff) |
|
79 done |
|
80 |
|
81 termination |
|
82 apply(relation "measure (size o snd)") |
|
83 apply(simp_all add: ty2.size) |
|
84 done |
|
85 |
|
86 lemma subst_eqvt[eqvt]: |
|
87 shows "(p \<bullet> subst \<theta> T) = subst (p \<bullet> \<theta>) (p \<bullet> T)" |
|
88 apply(induct \<theta> T rule: subst.induct) |
|
89 apply(simp_all add: lookup_eqvt) |
|
90 done |
|
91 |
|
92 lemma j: |
|
93 assumes "a \<sharp> Ts" " a \<sharp> X" |
|
94 shows "a \<sharp> lookup Ts X" |
|
95 using assms |
|
96 apply(induct Ts X rule: lookup.induct) |
|
97 apply(auto simp add: ty2.fresh fresh_Cons fresh_Pair) |
|
98 done |
|
99 |
|
100 lemma i: |
|
101 assumes "a \<sharp> t" " a \<sharp> \<theta>" |
|
102 shows "a \<sharp> subst \<theta> t" |
|
103 using assms |
|
104 apply(induct \<theta> t rule: subst.induct) |
|
105 apply(auto simp add: ty2.fresh j) |
|
106 done |
|
107 |
|
108 lemma k: |
|
109 assumes "as \<sharp>* t" " as \<sharp>* \<theta>" |
|
110 shows "as \<sharp>* subst \<theta> t" |
|
111 using assms |
|
112 by (simp add: fresh_star_def i) |
|
113 |
|
114 lemma h: |
|
115 assumes "as \<subseteq> bs \<union> cs" |
|
116 and " cs \<sharp>* x" |
|
117 shows "(as - bs) \<sharp>* x" |
|
118 using assms |
|
119 by (auto simp add: fresh_star_def) |
|
120 |
|
121 nominal_primrec |
|
122 substs :: "(name \<times> ty2) list \<Rightarrow> tys2 \<Rightarrow> tys2" |
|
123 where |
|
124 "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All2 xs t) = All2 xs (subst \<theta> t)" |
|
125 oops |
|
126 |
|
127 |
|
128 text {* Some Tests about Alpha-Equality *} |
55 |
129 |
56 lemma |
130 lemma |
57 shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))" |
131 shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))" |
58 apply(simp add: ty_tys.eq_iff) |
132 apply(simp add: ty_tys.eq_iff Abs_eq_iff) |
59 apply(simp add: Abs_eq_iff) |
|
60 apply(rule_tac x="0::perm" in exI) |
133 apply(rule_tac x="0::perm" in exI) |
61 apply(simp add: alphas) |
134 apply(simp add: alphas fresh_star_def ty_tys.supp supp_at_base) |
62 apply(simp add: fresh_star_def fresh_zero_perm supp_at_base) |
|
63 apply(simp add: ty_tys.supp supp_at_base) |
|
64 done |
135 done |
65 |
136 |
66 lemma |
137 lemma |
67 shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))" |
138 shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))" |
68 apply(simp add: ty_tys.eq_iff Abs_eq_iff) |
139 apply(simp add: ty_tys.eq_iff Abs_eq_iff) |
86 apply(simp add: alphas fresh_star_def ty_tys.eq_iff ty_tys.supp supp_at_base) |
157 apply(simp add: alphas fresh_star_def ty_tys.eq_iff ty_tys.supp supp_at_base) |
87 apply auto |
158 apply auto |
88 done |
159 done |
89 |
160 |
90 |
161 |
91 text {* Some lemmas about fsets *} |
|
92 |
|
93 lemma atom_map_fset_cong: |
|
94 shows "map_fset atom x = map_fset atom y \<longleftrightarrow> x = y" |
|
95 apply(rule inj_map_fset_cong) |
|
96 apply(simp add: inj_on_def) |
|
97 done |
|
98 |
|
99 lemma supp_map_fset_atom: |
|
100 shows "supp (map_fset atom S) = supp S" |
|
101 unfolding supp_def |
|
102 apply(perm_simp) |
|
103 apply(simp add: atom_map_fset_cong) |
|
104 done |
|
105 |
|
106 lemma supp_at_fset: |
|
107 fixes S::"('a::at_base) fset" |
|
108 shows "supp S = fset (map_fset atom S)" |
|
109 apply (induct S) |
|
110 apply (simp add: supp_empty_fset) |
|
111 apply (simp add: supp_insert_fset) |
|
112 apply (simp add: supp_at_base) |
|
113 done |
|
114 |
|
115 lemma fresh_star_atom: |
|
116 fixes a::"'a::at_base" |
|
117 shows "fset S \<sharp>* a \<Longrightarrow> atom a \<sharp> fset S" |
|
118 apply (induct S) |
|
119 apply (simp add: fresh_set_empty) |
|
120 apply simp |
|
121 apply (unfold fresh_def) |
|
122 apply (simp add: supp_of_finite_insert) |
|
123 apply (rule conjI) |
|
124 apply (unfold fresh_star_def) |
|
125 apply simp |
|
126 apply (unfold fresh_def) |
|
127 apply (simp add: supp_at_base supp_atom) |
|
128 apply clarify |
|
129 apply auto |
|
130 done |
|
131 |
|
132 |
|
133 |
|
134 (* |
|
135 fun |
|
136 lookup :: "(name \<times> ty) list \<Rightarrow> name \<Rightarrow> ty" |
|
137 where |
|
138 "lookup [] n = Var n" |
|
139 | "lookup ((p, s) # t) n = (if p = n then s else lookup t n)" |
|
140 |
|
141 locale subst_loc = |
|
142 fixes |
|
143 subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty" |
|
144 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" |
|
145 assumes |
|
146 s1: "subst \<theta> (Var n) = lookup \<theta> n" |
|
147 and s2: "subst \<theta> (Fun l r) = Fun (subst \<theta> l) (subst \<theta> r)" |
|
148 and s3: "fset (fmap atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs t) = All xs (subst \<theta> t)" |
|
149 begin |
|
150 |
|
151 lemma subst_ty: |
|
152 assumes x: "atom x \<sharp> t" |
|
153 shows "subst [(x, S)] t = t" |
|
154 using x |
|
155 apply (induct t rule: ty_tys.induct[of _ "\<lambda>t. True" _ , simplified]) |
|
156 by (simp_all add: s1 s2 fresh_def ty_tys.fv[simplified ty_tys.supp] supp_at_base) |
|
157 |
|
158 lemma subst_tyS: |
|
159 shows "atom x \<sharp> T \<longrightarrow> substs [(x, S)] T = T" |
|
160 apply (rule strong_induct[of |
|
161 "\<lambda>a t. True" "\<lambda>(x, S) T. (atom x \<sharp> T \<longrightarrow> substs [(x, S)] T = T)" _ "t" "(x, S)", simplified]) |
|
162 apply clarify |
|
163 apply (subst s3) |
|
164 apply (simp add: fresh_star_def fresh_Cons fresh_Nil) |
|
165 apply (subst subst_ty) |
|
166 apply (simp_all add: fresh_star_prod_elim) |
|
167 apply (drule fresh_star_atom) |
|
168 apply (simp add: fresh_def ty_tys.fv[simplified ty_tys.supp]) |
|
169 apply (subgoal_tac "atom a \<notin> fset (fmap atom fset)") |
|
170 apply blast |
|
171 apply (metis supp_finite_atom_set finite_fset) |
|
172 done |
|
173 |
|
174 lemma subst_lemma_pre: |
|
175 "z \<sharp> (N,L) \<longrightarrow> z \<sharp> (subst [(y, L)] N)" |
|
176 apply (induct N rule: ty_tys.induct[of _ "\<lambda>t. True" _ , simplified]) |
|
177 apply (simp add: s1) |
|
178 apply (auto simp add: fresh_Pair) |
|
179 apply (auto simp add: fresh_def ty_tys.fv[simplified ty_tys.supp])[3] |
|
180 apply (simp add: s2) |
|
181 apply (auto simp add: fresh_def ty_tys.fv[simplified ty_tys.supp]) |
|
182 done |
|
183 |
|
184 lemma substs_lemma_pre: |
|
185 "atom z \<sharp> (N,L) \<longrightarrow> atom z \<sharp> (substs [(y, L)] N)" |
|
186 apply (rule strong_induct[of |
|
187 "\<lambda>a t. True" "\<lambda>(z, y, L) N. (atom z \<sharp> (N, L) \<longrightarrow> atom z \<sharp> (substs [(y, L)] N))" _ _ "(z, y, L)", simplified]) |
|
188 apply clarify |
|
189 apply (subst s3) |
|
190 apply (simp add: fresh_star_def fresh_Cons fresh_Nil fresh_Pair) |
|
191 apply (simp_all add: fresh_star_prod_elim fresh_Pair) |
|
192 apply clarify |
|
193 apply (drule fresh_star_atom) |
|
194 apply (drule fresh_star_atom) |
|
195 apply (simp add: fresh_def) |
|
196 apply (simp only: ty_tys.fv[simplified ty_tys.supp]) |
|
197 apply (subgoal_tac "atom a \<notin> supp (subst [(aa, b)] t)") |
|
198 apply blast |
|
199 apply (subgoal_tac "atom a \<notin> supp t") |
|
200 apply (fold fresh_def)[1] |
|
201 apply (rule mp[OF subst_lemma_pre]) |
|
202 apply (simp add: fresh_Pair) |
|
203 apply (subgoal_tac "atom a \<notin> (fset (fmap atom fset))") |
|
204 apply blast |
|
205 apply (metis supp_finite_atom_set finite_fset) |
|
206 done |
|
207 |
|
208 lemma subst_lemma: |
|
209 shows "x \<noteq> y \<and> atom x \<sharp> L \<longrightarrow> |
|
210 subst [(y, L)] (subst [(x, N)] M) = |
|
211 subst [(x, (subst [(y, L)] N))] (subst [(y, L)] M)" |
|
212 apply (induct M rule: ty_tys.induct[of _ "\<lambda>t. True" _ , simplified]) |
|
213 apply (simp_all add: s1 s2) |
|
214 apply clarify |
|
215 apply (subst (2) subst_ty) |
|
216 apply simp_all |
|
217 done |
|
218 |
|
219 lemma substs_lemma: |
|
220 shows "x \<noteq> y \<and> atom x \<sharp> L \<longrightarrow> |
|
221 substs [(y, L)] (substs [(x, N)] M) = |
|
222 substs [(x, (subst [(y, L)] N))] (substs [(y, L)] M)" |
|
223 apply (rule strong_induct[of |
|
224 "\<lambda>a t. True" "\<lambda>(x, y, N, L) M. x \<noteq> y \<and> atom x \<sharp> L \<longrightarrow> |
|
225 substs [(y, L)] (substs [(x, N)] M) = |
|
226 substs [(x, (subst [(y, L)] N))] (substs [(y, L)] M)" _ _ "(x, y, N, L)", simplified]) |
|
227 apply clarify |
|
228 apply (simp_all add: fresh_star_prod_elim fresh_Pair) |
|
229 apply (subst s3) |
|
230 apply (unfold fresh_star_def)[1] |
|
231 apply (simp add: fresh_Cons fresh_Nil fresh_Pair) |
|
232 apply (subst s3) |
|
233 apply (unfold fresh_star_def)[1] |
|
234 apply (simp add: fresh_Cons fresh_Nil fresh_Pair) |
|
235 apply (subst s3) |
|
236 apply (unfold fresh_star_def)[1] |
|
237 apply (simp add: fresh_Cons fresh_Nil fresh_Pair) |
|
238 apply (subst s3) |
|
239 apply (unfold fresh_star_def)[1] |
|
240 apply (simp add: fresh_Cons fresh_Nil fresh_Pair) |
|
241 apply (rule ballI) |
|
242 apply (rule mp[OF subst_lemma_pre]) |
|
243 apply (simp add: fresh_Pair) |
|
244 apply (subst subst_lemma) |
|
245 apply simp_all |
|
246 done |
|
247 |
|
248 end |
|
249 *) |
|
250 |
162 |
251 |
163 |
252 end |
164 end |