279 declare [[map noption = (option_map, option_rel)]] |
279 declare [[map noption = (option_map, option_rel)]] |
280 |
280 |
281 lemma "option_map id = id" |
281 lemma "option_map id = id" |
282 sorry |
282 sorry |
283 |
283 |
284 lemma OPT_QUOTIENT: |
284 lemma option_Quotient: |
285 assumes q: "QUOTIENT R Abs Rep" |
285 assumes q: "Quotient R Abs Rep" |
286 shows "QUOTIENT (option_rel R) (option_map Abs) (option_map Rep)" |
286 shows "Quotient (option_rel R) (option_map Abs) (option_map Rep)" |
287 apply (unfold QUOTIENT_def) |
287 apply (unfold Quotient_def) |
288 apply (auto) |
288 apply (auto) |
289 using q |
289 using q |
290 apply (unfold QUOTIENT_def) |
290 apply (unfold Quotient_def) |
291 apply (case_tac "a :: 'b noption") |
291 apply (case_tac "a :: 'b noption") |
292 apply (simp) |
292 apply (simp) |
293 apply (simp) |
293 apply (simp) |
294 apply (case_tac "a :: 'b noption") |
294 apply (case_tac "a :: 'b noption") |
295 apply (simp only: option_map.simps) |
295 apply (simp only: option_map.simps) |
296 apply (subst option_rel.simps) |
296 apply (subst option_rel.simps) |
297 (* Simp starts hanging so don't know how to continue *) |
297 (* Simp starts hanging so don't know how to continue *) |
298 sorry |
298 sorry |
299 |
299 |
300 lemma real_alpha_pre: |
|
301 assumes a: "t = [(a,b)]\<bullet>s" "a\<sharp>[b].s" |
|
302 shows "rLam a t \<approx> rLam b s" |
|
303 sorry |
|
304 |
|
305 lemma perm_prs : "(id ---> option_map ABS_lam) ([b].REP_lam s) = [b].s" |
|
306 sorry |
|
307 |
|
308 lemma perm_prs2: "(id ---> option_map ABS_lam) ((id ---> option_map REP_lam) ([b].(s::lam))) = [b].s" |
|
309 sorry |
|
310 |
|
311 lemma real_alpha_lift: |
|
312 "\<lbrakk>t = [(a, b)] \<bullet> s; a \<sharp> [b].s\<rbrakk> \<Longrightarrow> Lam a t = Lam b s" |
|
313 apply (tactic {* procedure_tac @{context} @{thm real_alpha_pre} 1 *}) |
|
314 prefer 2 |
|
315 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
|
316 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
|
317 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
|
318 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
|
319 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
|
320 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
|
321 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
|
322 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
|
323 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
|
324 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
|
325 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
|
326 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
|
327 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
|
328 apply (tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
|
329 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
|
330 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
|
331 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
|
332 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
|
333 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
|
334 apply (simp only: perm_prs) |
|
335 prefer 2 |
|
336 apply (tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
|
337 prefer 3 |
|
338 apply (tactic {* clean_tac @{context} 1 *}) |
|
339 apply (simp only: perm_prs) |
|
340 (*apply (tactic {* regularize_tac @{context} 1 *})*) |
|
341 sorry |
|
342 |
|