100 "supp t = set (frees_lst t)" |
100 "supp t = set (frees_lst t)" |
101 apply(induct t rule: lam.induct) |
101 apply(induct t rule: lam.induct) |
102 apply(simp_all add: lam.supp supp_at_base) |
102 apply(simp_all add: lam.supp supp_at_base) |
103 done |
103 done |
104 |
104 |
|
105 nominal_datatype ln = |
|
106 LNBnd nat |
|
107 | LNVar name |
|
108 | LNApp ln ln |
|
109 | LNLam ln |
|
110 |
|
111 fun |
|
112 lookup :: "name list \<Rightarrow> nat \<Rightarrow> name \<Rightarrow> ln" |
|
113 where |
|
114 "lookup [] n x = LNVar x" |
|
115 | "lookup (y # ys) n x = (if x = y then LNBnd n else (lookup ys (n + 1) x))" |
|
116 |
|
117 lemma [eqvt]: |
|
118 shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)" |
|
119 apply(induct xs arbitrary: n) |
|
120 apply(simp_all add: permute_pure) |
|
121 done |
|
122 |
|
123 nominal_primrec |
|
124 trans :: "lam \<Rightarrow> name list \<Rightarrow> ln" |
|
125 where |
|
126 "trans (Var x) xs = lookup xs 0 x" |
|
127 | "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)" |
|
128 | "atom x \<sharp> xs \<Longrightarrow> trans (Lam x t) xs = LNLam (trans t (x # xs))" |
|
129 apply(case_tac x) |
|
130 apply(simp) |
|
131 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
|
132 apply(simp_all)[3] |
|
133 apply(blast) |
|
134 apply(blast) |
|
135 apply(simp add: fresh_star_def) |
|
136 apply(simp_all add: lam.distinct) |
|
137 apply(simp add: lam.eq_iff) |
|
138 apply(simp add: lam.eq_iff) |
|
139 apply(simp add: lam.eq_iff) |
|
140 apply(simp add: Abs_eq_iff) |
|
141 apply(erule conjE) |
|
142 apply(erule exE) |
|
143 apply(simp add: alphas) |
|
144 apply(simp add: atom_eqvt) |
|
145 apply(clarify) |
|
146 apply(rule trans) |
|
147 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
|
148 apply(simp (no_asm) add: ln.supp) |
|
149 apply(drule supp_eqvt_at) |
|
150 apply(simp add: finite_supp) |
|
151 oops |
|
152 |
|
153 |
|
154 |
|
155 |
|
156 |
105 nominal_datatype db = |
157 nominal_datatype db = |
106 DBVar nat |
158 DBVar nat |
107 | DBApp db db |
159 | DBApp db db |
108 | DBLam db |
160 | DBLam db |
109 |
161 |
110 abbreviation |
162 abbreviation |
111 mbind :: "'a option => ('a => 'b option) => 'b option" ("_ \<guillemotright>= _" [65,65] 65) |
163 mbind :: "'a option => ('a => 'b option) => 'b option" ("_ \<guillemotright>= _" [65,65] 65) |
112 where |
164 where |
113 "c \<guillemotright>= f \<equiv> case c of None => None | (Some v) => f v" |
165 "c \<guillemotright>= f \<equiv> case c of None => None | (Some v) => f v" |
114 |
|
115 |
166 |
116 lemma mbind_eqvt: |
167 lemma mbind_eqvt: |
117 fixes c::"'a::pt option" |
168 fixes c::"'a::pt option" |
118 shows "(p \<bullet> (c \<guillemotright>= f)) = ((p \<bullet> c) \<guillemotright>= (p \<bullet> f))" |
169 shows "(p \<bullet> (c \<guillemotright>= f)) = ((p \<bullet> c) \<guillemotright>= (p \<bullet> f))" |
119 apply(cases c) |
170 apply(cases c) |