equal
deleted
inserted
replaced
248 shows "(a\<sharp>(Var b)) = (a\<sharp>b)" |
248 shows "(a\<sharp>(Var b)) = (a\<sharp>b)" |
249 apply(simp add: fresh_def) |
249 apply(simp add: fresh_def) |
250 apply(simp add: var_supp) |
250 apply(simp add: var_supp) |
251 done |
251 done |
252 |
252 |
253 |
|
254 |
|
255 |
|
256 |
|
257 |
|
258 |
|
259 |
|
260 |
|
261 |
|
262 |
|
263 |
|
264 (* Construction Site code *) |
|
265 |
|
266 |
|
267 fun |
|
268 option_map::"('a \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)" |
|
269 where |
|
270 "option_map f (nSome x) = nSome (f x)" |
|
271 | "option_map f nNone = nNone" |
|
272 |
|
273 fun |
|
274 option_rel |
|
275 where |
|
276 "option_rel r (nSome x) (nSome y) = r x y" |
|
277 | "option_rel r _ _ = False" |
|
278 |
|
279 declare [[map noption = (option_map, option_rel)]] |
|
280 |
|
281 lemma "option_map id = id" |
|
282 sorry |
|
283 |
|
284 lemma option_Quotient: |
|
285 assumes q: "Quotient R Abs Rep" |
|
286 shows "Quotient (option_rel R) (option_map Abs) (option_map Rep)" |
|
287 apply (unfold Quotient_def) |
|
288 apply (auto) |
|
289 using q |
|
290 apply (unfold Quotient_def) |
|
291 apply (case_tac "a :: 'b noption") |
|
292 apply (simp) |
|
293 apply (simp) |
|
294 apply (case_tac "a :: 'b noption") |
|
295 apply (simp only: option_map.simps) |
|
296 apply (subst option_rel.simps) |
|
297 (* Simp starts hanging so don't know how to continue *) |
|
298 sorry |
|
299 |
|