equal
deleted
inserted
replaced
1505 |
1505 |
1506 |
1506 |
1507 (* outer syntax *) |
1507 (* outer syntax *) |
1508 |
1508 |
1509 val _ = |
1509 val _ = |
1510 Outer_Syntax.local_theory_to_proof "nominal_primrec" "define recursive functions for nominal types" |
1510 Outer_Syntax.local_theory_to_proof "nominal_function" "define recursive functions for nominal types" |
1511 Keyword.thy_goal |
1511 Keyword.thy_goal |
1512 (function_parser default_config |
1512 (function_parser default_config |
1513 >> (fn ((config, fixes), statements) => function_cmd fixes statements config)) |
1513 >> (fn ((config, fixes), statements) => function_cmd fixes statements config)) |
1514 *} |
1514 *} |
1515 |
1515 |
1543 assumes "x = y" |
1543 assumes "x = y" |
1544 and "a \<sharp> x" "c \<sharp> x" "b \<sharp> y" "c \<sharp> y" |
1544 and "a \<sharp> x" "c \<sharp> x" "b \<sharp> y" "c \<sharp> y" |
1545 shows "(a \<rightleftharpoons> c) \<bullet> x = (b \<rightleftharpoons> c) \<bullet> y" |
1545 shows "(a \<rightleftharpoons> c) \<bullet> x = (b \<rightleftharpoons> c) \<bullet> y" |
1546 using assms by (simp add: swap_fresh_fresh) |
1546 using assms by (simp add: swap_fresh_fresh) |
1547 |
1547 |
1548 nominal_primrec |
1548 nominal_function |
1549 depth :: "lam \<Rightarrow> nat" |
1549 depth :: "lam \<Rightarrow> nat" |
1550 where |
1550 where |
1551 "depth (Var x) = 1" |
1551 "depth (Var x) = 1" |
1552 | "depth (App t1 t2) = (max (depth t1) (depth t2)) + 1" |
1552 | "depth (App t1 t2) = (max (depth t1) (depth t2)) + 1" |
1553 | "depth (Lam x t) = (depth t) + 1" |
1553 | "depth (Lam x t) = (depth t) + 1" |
1564 |
1564 |
1565 lemma removeAll_eqvt[eqvt]: |
1565 lemma removeAll_eqvt[eqvt]: |
1566 shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)" |
1566 shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)" |
1567 by (induct xs) (auto) |
1567 by (induct xs) (auto) |
1568 |
1568 |
1569 nominal_primrec |
1569 nominal_function |
1570 frees_lst :: "lam \<Rightarrow> atom list" |
1570 frees_lst :: "lam \<Rightarrow> atom list" |
1571 where |
1571 where |
1572 "frees_lst (Var x) = [atom x]" |
1572 "frees_lst (Var x) = [atom x]" |
1573 | "frees_lst (App t1 t2) = (frees_lst t1) @ (frees_lst t2)" |
1573 | "frees_lst (App t1 t2) = (frees_lst t1) @ (frees_lst t2)" |
1574 | "frees_lst (Lam x t) = removeAll (atom x) (frees_lst t)" |
1574 | "frees_lst (Lam x t) = removeAll (atom x) (frees_lst t)" |
1583 apply(simp add: alphas) |
1583 apply(simp add: alphas) |
1584 apply(simp add: atom_eqvt) |
1584 apply(simp add: atom_eqvt) |
1585 apply(clarify) |
1585 apply(clarify) |
1586 oops |
1586 oops |
1587 |
1587 |
1588 nominal_primrec |
1588 nominal_function |
1589 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [100,100,100] 100) |
1589 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [100,100,100] 100) |
1590 where |
1590 where |
1591 "(Var x)[y ::= s] = (if x=y then s else (Var x))" |
1591 "(Var x)[y ::= s] = (if x=y then s else (Var x))" |
1592 | "(App t\<^isub>1 t\<^isub>2)[y ::= s] = App (t\<^isub>1[y ::= s]) (t\<^isub>2[y ::= s])" |
1592 | "(App t\<^isub>1 t\<^isub>2)[y ::= s] = App (t\<^isub>1[y ::= s]) (t\<^isub>2[y ::= s])" |
1593 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])" |
1593 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])" |
1606 apply(erule conjE)+ |
1606 apply(erule conjE)+ |
1607 oops |
1607 oops |
1608 |
1608 |
1609 |
1609 |
1610 |
1610 |
1611 nominal_primrec |
1611 nominal_function |
1612 depth :: "lam \<Rightarrow> nat" |
1612 depth :: "lam \<Rightarrow> nat" |
1613 where |
1613 where |
1614 "depth (Var x) = 1" |
1614 "depth (Var x) = 1" |
1615 | "depth (App t1 t2) = (max (depth t1) (depth t2)) + 1" |
1615 | "depth (App t1 t2) = (max (depth t1) (depth t2)) + 1" |
1616 | "depth (Lam x t) = (depth t) + 1" |
1616 | "depth (Lam x t) = (depth t) + 1" |
1663 |
1663 |
1664 lemma removeAll_eqvt[eqvt]: |
1664 lemma removeAll_eqvt[eqvt]: |
1665 shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)" |
1665 shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)" |
1666 by (induct xs) (auto) |
1666 by (induct xs) (auto) |
1667 |
1667 |
1668 nominal_primrec |
1668 nominal_function |
1669 frees_lst :: "lam \<Rightarrow> atom list" |
1669 frees_lst :: "lam \<Rightarrow> atom list" |
1670 where |
1670 where |
1671 "frees_lst (Var x) = [atom x]" |
1671 "frees_lst (Var x) = [atom x]" |
1672 | "frees_lst (App t1 t2) = (frees_lst t1) @ (frees_lst t2)" |
1672 | "frees_lst (App t1 t2) = (frees_lst t1) @ (frees_lst t2)" |
1673 | "frees_lst (Lam x t) = removeAll (atom x) (frees_lst t)" |
1673 | "frees_lst (Lam x t) = removeAll (atom x) (frees_lst t)" |
1685 apply(rule trans) |
1685 apply(rule trans) |
1686 apply(rule sym) |
1686 apply(rule sym) |
1687 apply(rule_tac p="p" in supp_perm_eq) |
1687 apply(rule_tac p="p" in supp_perm_eq) |
1688 oops |
1688 oops |
1689 |
1689 |
1690 nominal_primrec |
1690 nominal_function |
1691 frees :: "lam \<Rightarrow> name set" |
1691 frees :: "lam \<Rightarrow> name set" |
1692 where |
1692 where |
1693 "frees (Var x) = {x}" |
1693 "frees (Var x) = {x}" |
1694 | "frees (App t1 t2) = (frees t1) \<union> (frees t2)" |
1694 | "frees (App t1 t2) = (frees t1) \<union> (frees t2)" |
1695 | "frees (Lam x t) = (frees t) - {x}" |
1695 | "frees (Lam x t) = (frees t) - {x}" |
1769 apply(erule exE) |
1769 apply(erule exE) |
1770 apply(rule_tac x="q" in exI) |
1770 apply(rule_tac x="q" in exI) |
1771 apply(simp add: set_eqvt) |
1771 apply(simp add: set_eqvt) |
1772 sorry |
1772 sorry |
1773 |
1773 |
1774 nominal_primrec |
1774 nominal_function |
1775 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [100,100,100] 100) |
1775 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [100,100,100] 100) |
1776 where |
1776 where |
1777 "(Var x)[y ::= s] = (if x=y then s else (Var x))" |
1777 "(Var x)[y ::= s] = (if x=y then s else (Var x))" |
1778 | "(App t\<^isub>1 t\<^isub>2)[y ::= s] = App (t\<^isub>1[y ::= s]) (t\<^isub>2[y ::= s])" |
1778 | "(App t\<^isub>1 t\<^isub>2)[y ::= s] = App (t\<^isub>1[y ::= s]) (t\<^isub>2[y ::= s])" |
1779 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])" |
1779 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])" |
1820 apply(rule fresh_star_supp_conv) |
1820 apply(rule fresh_star_supp_conv) |
1821 apply(auto simp add: fresh_star_def fresh_Pair)[1] |
1821 apply(auto simp add: fresh_star_def fresh_Pair)[1] |
1822 |
1822 |
1823 |
1823 |
1824 |
1824 |
1825 nominal_primrec |
1825 nominal_function |
1826 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [100,100,100] 100) |
1826 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [100,100,100] 100) |
1827 where |
1827 where |
1828 "(Var x)[y ::= s] = (if x=y then s else (Var x))" |
1828 "(Var x)[y ::= s] = (if x=y then s else (Var x))" |
1829 | "(App t\<^isub>1 t\<^isub>2)[y ::= s] = App (t\<^isub>1[y ::= s]) (t\<^isub>2[y ::= s])" |
1829 | "(App t\<^isub>1 t\<^isub>2)[y ::= s] = App (t\<^isub>1[y ::= s]) (t\<^isub>2[y ::= s])" |
1830 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])" |
1830 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])" |
1872 apply(simp) |
1872 apply(simp) |
1873 apply(simp add: finite_supp) |
1873 apply(simp add: finite_supp) |
1874 done |
1874 done |
1875 |
1875 |
1876 (* this should not work *) |
1876 (* this should not work *) |
1877 nominal_primrec |
1877 nominal_function |
1878 bnds :: "lam \<Rightarrow> name set" |
1878 bnds :: "lam \<Rightarrow> name set" |
1879 where |
1879 where |
1880 "bnds (Var x) = {}" |
1880 "bnds (Var x) = {}" |
1881 | "bnds (App t1 t2) = (bnds t1) \<union> (bnds t2)" |
1881 | "bnds (App t1 t2) = (bnds t1) \<union> (bnds t2)" |
1882 | "bnds (Lam x t) = (bnds t) \<union> {x}" |
1882 | "bnds (Lam x t) = (bnds t) \<union> {x}" |