318 done |
320 done |
319 |
321 |
320 termination |
322 termination |
321 by lexicographic_order |
323 by lexicographic_order |
322 |
324 |
|
325 |
|
326 text {* count the occurences of lambdas in a term *} |
|
327 |
|
328 nominal_primrec |
|
329 cntlams :: "lam \<Rightarrow> nat" |
|
330 where |
|
331 "cntlams (Var x) = 0" |
|
332 | "cntlams (App t1 t2) = (cntlams t1) + (cntlams t2)" |
|
333 | "cntlams (Lam [x]. t) = Suc (cntlams t)" |
|
334 apply(simp add: eqvt_def cntlams_graph_def) |
|
335 apply(rule, perm_simp, rule) |
|
336 apply(rule TrueI) |
|
337 apply(rule_tac y="x" in lam.exhaust) |
|
338 apply(auto)[3] |
|
339 apply(all_trivials) |
|
340 apply(simp) |
|
341 apply(simp) |
|
342 apply(erule_tac c="()" in Abs_lst1_fcb2') |
|
343 apply(simp add: pure_fresh) |
|
344 apply(simp add: fresh_star_def pure_fresh) |
|
345 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
346 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
347 done |
|
348 |
|
349 termination |
|
350 by lexicographic_order |
|
351 |
|
352 |
323 text {* count the bound-variable occurences in a lambda-term *} |
353 text {* count the bound-variable occurences in a lambda-term *} |
324 |
354 |
325 nominal_primrec |
355 nominal_primrec |
326 cbvs :: "lam \<Rightarrow> name list \<Rightarrow> nat" |
356 cntbvs :: "lam \<Rightarrow> name list \<Rightarrow> nat" |
327 where |
357 where |
328 "cbvs (Var x) xs = (if x \<in> set xs then 1 else 0)" |
358 "cntbvs (Var x) xs = (if x \<in> set xs then 1 else 0)" |
329 | "cbvs (App t1 t2) xs = (cbvs t1 xs) + (cbvs t2 xs)" |
359 | "cntbvs (App t1 t2) xs = (cntbvs t1 xs) + (cntbvs t2 xs)" |
330 | "atom x \<sharp> xs \<Longrightarrow> cbvs (Lam [x]. t) xs = cbvs t (x # xs)" |
360 | "atom x \<sharp> xs \<Longrightarrow> cntbvs (Lam [x]. t) xs = cntbvs t (x # xs)" |
331 apply(simp add: eqvt_def cbvs_graph_def) |
361 apply(simp add: eqvt_def cntbvs_graph_def) |
332 apply(rule, perm_simp, rule) |
362 apply(rule, perm_simp, rule) |
333 apply(simp_all) |
363 apply(rule TrueI) |
334 apply(case_tac x) |
364 apply(case_tac x) |
335 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
365 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
336 apply(auto simp add: fresh_star_def)[3] |
366 apply(auto simp add: fresh_star_def)[3] |
|
367 apply(all_trivials) |
|
368 apply(simp) |
|
369 apply(simp) |
|
370 apply(simp) |
337 apply(erule conjE) |
371 apply(erule conjE) |
338 apply(erule Abs_lst1_fcb2') |
372 apply(erule Abs_lst1_fcb2') |
339 apply(simp add: pure_fresh fresh_star_def) |
373 apply(simp add: pure_fresh fresh_star_def) |
340 apply(simp add: pure_fresh fresh_star_def) |
374 apply(simp add: fresh_star_def) |
341 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
375 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
342 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
376 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
343 done |
377 done |
344 |
378 |
345 termination |
379 termination |
378 |
412 |
379 lemma vindex_eqvt[eqvt]: |
413 lemma vindex_eqvt[eqvt]: |
380 "(p \<bullet> vindex l v n) = vindex (p \<bullet> l) (p \<bullet> v) (p \<bullet> n)" |
414 "(p \<bullet> vindex l v n) = vindex (p \<bullet> l) (p \<bullet> v) (p \<bullet> n)" |
381 by (induct l arbitrary: n) (simp_all add: permute_pure) |
415 by (induct l arbitrary: n) (simp_all add: permute_pure) |
382 |
416 |
|
417 |
|
418 |
383 nominal_primrec |
419 nominal_primrec |
384 transdb :: "lam \<Rightarrow> name list \<Rightarrow> db option" |
420 transdb :: "lam \<Rightarrow> name list \<Rightarrow> db option" |
385 where |
421 where |
386 "transdb (Var x) l = vindex l x 0" |
422 "transdb (Var x) l = vindex l x 0" |
387 | "transdb (App t1 t2) xs = Option.bind (transdb t1 xs) (\<lambda>d1. Option.bind (transdb t2 xs) (\<lambda>d2. Some (DBApp d1 d2)))" |
423 | "transdb (App t1 t2) xs = |
|
424 Option.bind (transdb t1 xs) (\<lambda>d1. Option.bind (transdb t2 xs) (\<lambda>d2. Some (DBApp d1 d2)))" |
388 | "x \<notin> set xs \<Longrightarrow> transdb (Lam [x].t) xs = Option.map DBLam (transdb t (x # xs))" |
425 | "x \<notin> set xs \<Longrightarrow> transdb (Lam [x].t) xs = Option.map DBLam (transdb t (x # xs))" |
389 unfolding eqvt_def transdb_graph_def |
426 unfolding eqvt_def transdb_graph_def |
390 apply (rule, perm_simp, rule) |
427 apply (rule, perm_simp, rule) |
391 apply(rule TrueI) |
428 apply(rule TrueI) |
392 apply (case_tac x) |
429 apply (case_tac x) |
418 lemma db_trans_test: |
455 lemma db_trans_test: |
419 assumes a: "y \<noteq> x" |
456 assumes a: "y \<noteq> x" |
420 shows "transdb (Lam [x]. Lam [y]. App (Var x) (Var y)) [] = |
457 shows "transdb (Lam [x]. Lam [y]. App (Var x) (Var y)) [] = |
421 Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))" |
458 Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))" |
422 using a by simp |
459 using a by simp |
423 |
|
424 |
|
425 abbreviation |
|
426 mbind :: "'a option => ('a => 'b option) => 'b option" ("_ \<guillemotright>= _" [65,65] 65) |
|
427 where |
|
428 "c \<guillemotright>= f \<equiv> case c of None => None | (Some v) => f v" |
|
429 |
|
430 lemma mbind_eqvt: |
|
431 fixes c::"'a::pt option" |
|
432 shows "(p \<bullet> (c \<guillemotright>= f)) = ((p \<bullet> c) \<guillemotright>= (p \<bullet> f))" |
|
433 apply(cases c) |
|
434 apply(simp_all) |
|
435 apply(perm_simp) |
|
436 apply(rule refl) |
|
437 done |
|
438 |
|
439 lemma mbind_eqvt_raw[eqvt_raw]: |
|
440 shows "(p \<bullet> option_case) \<equiv> option_case" |
|
441 apply(rule eq_reflection) |
|
442 apply(rule ext)+ |
|
443 apply(case_tac xb) |
|
444 apply(simp_all) |
|
445 apply(rule_tac p="-p" in permute_boolE) |
|
446 apply(perm_simp add: permute_minus_cancel) |
|
447 apply(simp) |
|
448 apply(rule_tac p="-p" in permute_boolE) |
|
449 apply(perm_simp add: permute_minus_cancel) |
|
450 apply(simp) |
|
451 done |
|
452 |
|
453 fun |
|
454 index :: "atom list \<Rightarrow> nat \<Rightarrow> atom \<Rightarrow> nat option" |
|
455 where |
|
456 "index [] n x = None" |
|
457 | "index (y # ys) n x = (if x = y then (Some n) else (index ys (n + 1) x))" |
|
458 |
|
459 lemma [eqvt]: |
|
460 shows "(p \<bullet> index xs n x) = index (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)" |
|
461 apply(induct xs arbitrary: n) |
|
462 apply(simp_all add: permute_pure) |
|
463 done |
|
464 |
460 |
465 lemma supp_subst: |
461 lemma supp_subst: |
466 "supp (t[x ::= s]) \<subseteq> supp t \<union> supp s" |
462 "supp (t[x ::= s]) \<subseteq> supp t \<union> supp s" |
467 by (induct t x s rule: subst.induct) (auto simp add: lam.supp) |
463 by (induct t x s rule: subst.induct) (auto simp add: lam.supp) |
468 |
464 |
567 done |
563 done |
568 |
564 |
569 termination |
565 termination |
570 by lexicographic_order |
566 by lexicographic_order |
571 |
567 |
|
568 |
|
569 (* |
|
570 abbreviation |
|
571 mbind :: "'a option => ('a => 'b option) => 'b option" ("_ \<guillemotright>= _" [65,65] 65) |
|
572 where |
|
573 "c \<guillemotright>= f \<equiv> case c of None => None | (Some v) => f v" |
|
574 |
|
575 lemma mbind_eqvt: |
|
576 fixes c::"'a::pt option" |
|
577 shows "(p \<bullet> (c \<guillemotright>= f)) = ((p \<bullet> c) \<guillemotright>= (p \<bullet> f))" |
|
578 apply(cases c) |
|
579 apply(simp_all) |
|
580 apply(perm_simp) |
|
581 apply(rule refl) |
|
582 done |
|
583 |
|
584 lemma mbind_eqvt_raw[eqvt_raw]: |
|
585 shows "(p \<bullet> option_case) \<equiv> option_case" |
|
586 apply(rule eq_reflection) |
|
587 apply(rule ext)+ |
|
588 apply(case_tac xb) |
|
589 apply(simp_all) |
|
590 apply(rule_tac p="-p" in permute_boolE) |
|
591 apply(perm_simp add: permute_minus_cancel) |
|
592 apply(simp) |
|
593 apply(rule_tac p="-p" in permute_boolE) |
|
594 apply(perm_simp add: permute_minus_cancel) |
|
595 apply(simp) |
|
596 done |
|
597 |
|
598 fun |
|
599 index :: "atom list \<Rightarrow> nat \<Rightarrow> atom \<Rightarrow> nat option" |
|
600 where |
|
601 "index [] n x = None" |
|
602 | "index (y # ys) n x = (if x = y then (Some n) else (index ys (n + 1) x))" |
|
603 |
|
604 lemma [eqvt]: |
|
605 shows "(p \<bullet> index xs n x) = index (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)" |
|
606 apply(induct xs arbitrary: n) |
|
607 apply(simp_all add: permute_pure) |
|
608 done |
|
609 *) |
|
610 |
|
611 (* |
572 nominal_primrec |
612 nominal_primrec |
573 trans2 :: "lam \<Rightarrow> atom list \<Rightarrow> db option" |
613 trans2 :: "lam \<Rightarrow> atom list \<Rightarrow> db option" |
574 where |
614 where |
575 "trans2 (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n. Some (DBVar n)))" |
615 "trans2 (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n::nat. Some (DBVar n)))" |
576 | "trans2 (App t1 t2) xs = ((trans2 t1 xs) \<guillemotright>= (\<lambda>db1. (trans2 t2 xs) \<guillemotright>= (\<lambda>db2. Some (DBApp db1 db2))))" |
616 | "trans2 (App t1 t2) xs = |
577 | "trans2 (Lam [x].t) xs = (trans2 t (atom x # xs) \<guillemotright>= (\<lambda>db. Some (DBLam db)))" |
617 ((trans2 t1 xs) \<guillemotright>= (\<lambda>db1::db. (trans2 t2 xs) \<guillemotright>= (\<lambda>db2::db. Some (DBApp db1 db2))))" |
|
618 | "trans2 (Lam [x].t) xs = (trans2 t (atom x # xs) \<guillemotright>= (\<lambda>db::db. Some (DBLam db)))" |
578 oops |
619 oops |
|
620 *) |
579 |
621 |
580 nominal_primrec |
622 nominal_primrec |
581 CPS :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam" |
623 CPS :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam" |
582 where |
624 where |
583 "CPS (Var x) k = Var x" |
625 "CPS (Var x) k = Var x" |