equal
deleted
inserted
replaced
78 nominal_primrec |
78 nominal_primrec |
79 subst :: "Subst \<Rightarrow> ty \<Rightarrow> ty" ("_<_>" [100,60] 120) |
79 subst :: "Subst \<Rightarrow> ty \<Rightarrow> ty" ("_<_>" [100,60] 120) |
80 where |
80 where |
81 "\<theta><Var X> = lookup \<theta> X" |
81 "\<theta><Var X> = lookup \<theta> X" |
82 | "\<theta><T1 \<rightarrow> T2> = (\<theta><T1>) \<rightarrow> (\<theta><T2>)" |
82 | "\<theta><T1 \<rightarrow> T2> = (\<theta><T1>) \<rightarrow> (\<theta><T2>)" |
83 unfolding eqvt_def subst_graph_def |
83 apply(simp add: eqvt_def subst_graph_aux_def) |
84 apply (rule, perm_simp, rule) |
|
85 apply(rule TrueI) |
84 apply(rule TrueI) |
86 apply(case_tac x) |
85 apply(case_tac x) |
87 apply(rule_tac y="b" in ty.exhaust) |
86 apply(rule_tac y="b" in ty.exhaust) |
88 apply(blast) |
87 apply(blast) |
89 apply(blast) |
88 apply(blast) |
117 |
116 |
118 nominal_primrec |
117 nominal_primrec |
119 substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" ("_<_>" [100,60] 120) |
118 substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" ("_<_>" [100,60] 120) |
120 where |
119 where |
121 "fset (map_fset atom Xs) \<sharp>* \<theta> \<Longrightarrow> \<theta><All [Xs].T> = All [Xs].(\<theta><T>)" |
120 "fset (map_fset atom Xs) \<sharp>* \<theta> \<Longrightarrow> \<theta><All [Xs].T> = All [Xs].(\<theta><T>)" |
122 unfolding eqvt_def substs_graph_def |
121 apply(simp add: eqvt_def substs_graph_aux_def) |
123 apply (rule, perm_simp, rule) |
|
124 apply auto[2] |
122 apply auto[2] |
125 apply (rule_tac y="b" and c="a" in tys.strong_exhaust) |
123 apply (rule_tac y="b" and c="a" in tys.strong_exhaust) |
126 apply auto[1] |
124 apply auto[1] |
127 apply(simp) |
125 apply(simp) |
128 apply(erule conjE) |
126 apply(erule conjE) |
277 nominal_primrec |
275 nominal_primrec |
278 generalises :: "ty \<Rightarrow> tys \<Rightarrow> bool" ("_ \<prec>\<prec> _") |
276 generalises :: "ty \<Rightarrow> tys \<Rightarrow> bool" ("_ \<prec>\<prec> _") |
279 where |
277 where |
280 "atom ` (fset Xs) \<sharp>* T \<Longrightarrow> |
278 "atom ` (fset Xs) \<sharp>* T \<Longrightarrow> |
281 T \<prec>\<prec> All [Xs].T' \<longleftrightarrow> (\<exists>\<theta>. T = \<theta><T'> \<and> atom ` Dom \<theta> = atom ` fset Xs \<inter> supp T')" |
279 T \<prec>\<prec> All [Xs].T' \<longleftrightarrow> (\<exists>\<theta>. T = \<theta><T'> \<and> atom ` Dom \<theta> = atom ` fset Xs \<inter> supp T')" |
282 unfolding generalises_graph_def |
280 apply(simp add: generalises_graph_aux_def eqvt_def) |
283 unfolding eqvt_def |
|
284 apply(perm_simp) |
|
285 apply(simp) |
|
286 apply(rule TrueI) |
281 apply(rule TrueI) |
287 apply(case_tac x) |
282 apply(case_tac x) |
288 apply(simp) |
283 apply(simp) |
289 apply(rule_tac y="b" and c="a" in tys.strong_exhaust) |
284 apply(rule_tac y="b" and c="a" in tys.strong_exhaust) |
290 apply(simp) |
285 apply(simp) |
407 nominal_primrec |
402 nominal_primrec |
408 ftv :: "ty \<Rightarrow> name fset" |
403 ftv :: "ty \<Rightarrow> name fset" |
409 where |
404 where |
410 "ftv (Var X) = {|X|}" |
405 "ftv (Var X) = {|X|}" |
411 | "ftv (T1 \<rightarrow> T2) = (ftv T1) |\<union>| (ftv T2)" |
406 | "ftv (T1 \<rightarrow> T2) = (ftv T1) |\<union>| (ftv T2)" |
412 unfolding eqvt_def ftv_graph_def |
407 apply(simp add: eqvt_def ftv_graph_aux_def) |
413 apply (rule, perm_simp, rule) |
|
414 apply(rule TrueI) |
408 apply(rule TrueI) |
415 apply(rule_tac y="x" in ty.exhaust) |
409 apply(rule_tac y="x" in ty.exhaust) |
416 apply(blast) |
410 apply(blast) |
417 apply(blast) |
411 apply(blast) |
418 apply(simp_all) |
412 apply(simp_all) |