1598 >> (fn ((config, fixes), statements) => function_cmd fixes statements config)) |
1598 >> (fn ((config, fixes), statements) => function_cmd fixes statements config)) |
1599 *} |
1599 *} |
1600 |
1600 |
1601 ML {* trace := true *} |
1601 ML {* trace := true *} |
1602 |
1602 |
|
1603 lemma test: |
|
1604 assumes a: "[[x]]lst. t = [[x]]lst. t'" |
|
1605 shows "t = t'" |
|
1606 using a |
|
1607 apply(simp add: Abs_eq_iff) |
|
1608 apply(erule exE) |
|
1609 apply(simp only: alphas) |
|
1610 apply(erule conjE)+ |
|
1611 apply(rule sym) |
|
1612 apply(clarify) |
|
1613 apply(rule supp_perm_eq) |
|
1614 apply(subgoal_tac "set [x] \<sharp>* p") |
|
1615 apply(auto simp add: fresh_star_def)[1] |
|
1616 apply(simp) |
|
1617 apply(simp add: fresh_star_def) |
|
1618 apply(simp add: fresh_perm) |
|
1619 done |
|
1620 |
|
1621 lemma test2: |
|
1622 assumes "a \<sharp> x" "c \<sharp> x" "b \<sharp> y" "c \<sharp> y" |
|
1623 and "(a \<rightleftharpoons> c) \<bullet> x = (b \<rightleftharpoons> c) \<bullet> y" |
|
1624 shows "x = y" |
|
1625 using assms by (simp add: swap_fresh_fresh) |
|
1626 |
|
1627 lemma test3: |
|
1628 assumes "x = y" |
|
1629 and "a \<sharp> x" "c \<sharp> x" "b \<sharp> y" "c \<sharp> y" |
|
1630 shows "(a \<rightleftharpoons> c) \<bullet> x = (b \<rightleftharpoons> c) \<bullet> y" |
|
1631 using assms by (simp add: swap_fresh_fresh) |
|
1632 |
1603 nominal_primrec |
1633 nominal_primrec |
1604 depth :: "lam \<Rightarrow> nat" |
1634 depth :: "lam \<Rightarrow> nat" |
1605 where |
1635 where |
1606 "depth (Var x) = 1" |
1636 "depth (Var x) = 1" |
1607 | "depth (App t1 t2) = (max (depth t1) (depth t2)) + 1" |
1637 | "depth (App t1 t2) = (max (depth t1) (depth t2)) + 1" |
1608 | "depth (Lam x t) = (depth t) + 1" |
1638 | "depth (Lam x t) = (depth t) + 1" |
1609 thm depth_graph.intros |
|
1610 apply(rule_tac y="x" in lam.exhaust) |
1639 apply(rule_tac y="x" in lam.exhaust) |
1611 apply(simp_all)[3] |
1640 apply(simp_all)[3] |
1612 apply(simp_all only: lam.distinct) |
1641 apply(simp_all only: lam.distinct) |
1613 apply(simp add: lam.eq_iff) |
1642 apply(simp add: lam.eq_iff) |
1614 apply(simp add: lam.eq_iff) |
1643 apply(simp add: lam.eq_iff) |
1615 sorry |
1644 apply(subgoal_tac "finite (supp (x, xa, t, ta, depth_sumC t, depth_sumC ta))") |
|
1645 apply(erule_tac ?'a="name" in obtain_at_base) |
|
1646 unfolding fresh_def[symmetric] |
|
1647 apply(drule_tac a="atom x" and b="atom xa" and c="atom a" in test3) |
|
1648 apply(simp add: Abs_fresh_iff) |
|
1649 apply(simp add: Abs_fresh_iff) |
|
1650 apply(simp add: Abs_fresh_iff) |
|
1651 apply(simp add: Abs_fresh_iff) |
|
1652 apply(rule_tac a="atom x" and b="atom xa" and c="atom a" in test2) |
|
1653 apply(simp add: pure_fresh) |
|
1654 apply(simp add: pure_fresh) |
|
1655 apply(simp add: pure_fresh) |
|
1656 apply(simp add: pure_fresh) |
|
1657 apply(simp add: eqvt_at_def) |
|
1658 apply(drule test) |
|
1659 apply(simp) |
|
1660 apply(simp add: finite_supp) |
|
1661 done |
|
1662 |
|
1663 termination depth |
|
1664 apply(relation "measure size") |
|
1665 apply(auto simp add: lam.size) |
|
1666 done |
1616 |
1667 |
1617 thm depth.psimps |
1668 thm depth.psimps |
|
1669 thm depth.simps |
1618 |
1670 |
1619 nominal_primrec |
1671 nominal_primrec |
1620 frees :: "lam \<Rightarrow> name set" |
1672 frees :: "lam \<Rightarrow> name set" |
1621 where |
1673 where |
1622 "frees (Var x) = {x}" |
1674 "frees (Var x) = {x}" |
1626 apply(simp_all)[3] |
1678 apply(simp_all)[3] |
1627 apply(simp_all only: lam.distinct) |
1679 apply(simp_all only: lam.distinct) |
1628 apply(simp add: lam.eq_iff) |
1680 apply(simp add: lam.eq_iff) |
1629 apply(simp add: lam.eq_iff) |
1681 apply(simp add: lam.eq_iff) |
1630 apply(simp add: lam.eq_iff) |
1682 apply(simp add: lam.eq_iff) |
1631 sorry |
1683 apply(subgoal_tac "finite (supp (x, xa, t, ta, frees_sumC t, frees_sumC ta))") |
|
1684 apply(erule_tac ?'a="name" in obtain_at_base) |
|
1685 unfolding fresh_def[symmetric] |
|
1686 apply(drule_tac a="atom x" and b="atom xa" and c="atom a" in test3) |
|
1687 apply(simp add: Abs_fresh_iff) |
|
1688 apply(simp add: Abs_fresh_iff) |
|
1689 apply(simp add: Abs_fresh_iff) |
|
1690 apply(simp add: Abs_fresh_iff) |
|
1691 apply(simp) |
|
1692 apply(drule test) |
|
1693 oops |
1632 |
1694 |
1633 nominal_primrec |
1695 nominal_primrec |
1634 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [100,100,100] 100) |
1696 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [100,100,100] 100) |
1635 where |
1697 where |
1636 "(Var x)[y ::= s] = (if x=y then s else (Var x))" |
1698 "(Var x)[y ::= s] = (if x=y then s else (Var x))" |
1642 apply(simp add: lam.eq_iff lam.distinct) |
1704 apply(simp add: lam.eq_iff lam.distinct) |
1643 apply(auto)[1] |
1705 apply(auto)[1] |
1644 apply(simp add: lam.eq_iff lam.distinct) |
1706 apply(simp add: lam.eq_iff lam.distinct) |
1645 apply(auto)[1] |
1707 apply(auto)[1] |
1646 apply(simp add: fresh_star_def lam.eq_iff lam.distinct) |
1708 apply(simp add: fresh_star_def lam.eq_iff lam.distinct) |
1647 apply(simp_all add: lam.distinct) |
1709 apply(simp_all add: lam.distinct)[5] |
1648 apply(simp add: lam.eq_iff) |
1710 apply(simp add: lam.eq_iff) |
1649 apply(simp add: lam.eq_iff) |
1711 apply(simp add: lam.eq_iff) |
1650 apply(simp add: lam.eq_iff) |
1712 apply(simp add: lam.eq_iff) |
1651 sorry |
1713 apply(subgoal_tac "finite (supp (ya, sa, x, xa, t, ta, subst_sumC (t, ya, sa), subst_sumC (ta, ya, sa)))") |
|
1714 apply(erule_tac ?'a="name" in obtain_at_base) |
|
1715 unfolding fresh_def[symmetric] |
|
1716 apply(rule_tac a="atom x" and b="atom xa" and c="atom a" in test2) |
|
1717 apply(simp add: Abs_fresh_iff) |
|
1718 apply(simp add: Abs_fresh_iff) |
|
1719 apply(simp add: Abs_fresh_iff) |
|
1720 apply(simp add: Abs_fresh_iff) |
|
1721 apply(erule conjE)+ |
|
1722 apply(drule_tac a="atom x" and b="atom xa" and c="atom a" in test3) |
|
1723 apply(simp add: Abs_fresh_iff) |
|
1724 apply(simp add: Abs_fresh_iff) |
|
1725 apply(simp add: Abs_fresh_iff) |
|
1726 apply(simp add: Abs_fresh_iff) |
|
1727 apply(simp add: eqvt_at_def) |
|
1728 apply(drule test) |
|
1729 apply(simp) |
|
1730 apply(subst (2) swap_fresh_fresh) |
|
1731 apply(simp) |
|
1732 apply(simp) |
|
1733 apply(subst (2) swap_fresh_fresh) |
|
1734 apply(simp) |
|
1735 apply(simp) |
|
1736 apply(subst (3) swap_fresh_fresh) |
|
1737 apply(simp) |
|
1738 apply(simp) |
|
1739 apply(subst (3) swap_fresh_fresh) |
|
1740 apply(simp) |
|
1741 apply(simp) |
|
1742 apply(simp) |
|
1743 apply(simp add: finite_supp) |
|
1744 done |
1652 |
1745 |
1653 (* this should not work *) |
1746 (* this should not work *) |
1654 nominal_primrec |
1747 nominal_primrec |
1655 bnds :: "lam \<Rightarrow> name set" |
1748 bnds :: "lam \<Rightarrow> name set" |
1656 where |
1749 where |