equal
deleted
inserted
replaced
1695 |
1695 |
1696 |
1696 |
1697 subsection {* helper functions for nominal_functions *} |
1697 subsection {* helper functions for nominal_functions *} |
1698 |
1698 |
1699 lemma THE_defaultI2: |
1699 lemma THE_defaultI2: |
1700 assumes "P a" "\<exists>!x. P x" "\<And>x. P x \<Longrightarrow> Q x" |
1700 assumes "\<exists>!x. P x" "\<And>x. P x \<Longrightarrow> Q x" |
1701 shows "Q (THE_default d P)" |
1701 shows "Q (THE_default d P)" |
1702 by (iprover intro: assms THE_defaultI') |
1702 by (iprover intro: assms THE_defaultI') |
1703 |
|
1704 thm THE_default1_equality |
|
1705 |
1703 |
1706 lemma the_default_eqvt: |
1704 lemma the_default_eqvt: |
1707 assumes unique: "\<exists>!x. P x" |
1705 assumes unique: "\<exists>!x. P x" |
1708 shows "(p \<bullet> (THE_default d P)) = (THE_default (p \<bullet> d) (p \<bullet> P))" |
1706 shows "(p \<bullet> (THE_default d P)) = (THE_default (p \<bullet> d) (p \<bullet> P))" |
1709 apply(rule THE_default1_equality [symmetric]) |
1707 apply(rule THE_default1_equality [symmetric]) |
1726 apply(subst the_default_eqvt) |
1724 apply(subst the_default_eqvt) |
1727 apply(rule ex1) |
1725 apply(rule ex1) |
1728 apply(rule THE_default1_equality [symmetric]) |
1726 apply(rule THE_default1_equality [symmetric]) |
1729 apply(rule_tac p="-p" in permute_boolE) |
1727 apply(rule_tac p="-p" in permute_boolE) |
1730 apply(perm_simp add: permute_minus_cancel) |
1728 apply(perm_simp add: permute_minus_cancel) |
1731 using eqvt |
1729 using eqvt[simplified eqvt_def] |
1732 unfolding eqvt_def |
|
1733 apply(simp) |
1730 apply(simp) |
1734 apply(rule ex1) |
1731 apply(rule ex1) |
1735 apply(rule_tac p="-p" in permute_boolE) |
1732 apply(rule THE_defaultI2) |
1736 apply(subst permute_fun_app_eq) |
|
1737 back |
|
1738 apply(subst the_default_eqvt) |
|
1739 apply(rule_tac p="-p" in permute_boolE) |
1733 apply(rule_tac p="-p" in permute_boolE) |
1740 apply(perm_simp add: permute_minus_cancel) |
1734 apply(perm_simp add: permute_minus_cancel) |
1741 apply(rule ex1) |
1735 apply(rule ex1) |
1742 apply(perm_simp add: permute_minus_cancel) |
1736 apply(perm_simp) |
1743 using eqvt |
1737 using eqvt[simplified eqvt_def] |
1744 unfolding eqvt_def |
|
1745 apply(simp) |
1738 apply(simp) |
1746 apply(rule THE_defaultI'[OF ex1]) |
|
1747 done |
1739 done |
1748 |
1740 |
1749 lemma fundef_ex1_eqvt_at: |
1741 lemma fundef_ex1_eqvt_at: |
1750 fixes x::"'a::pt" |
1742 fixes x::"'a::pt" |
1751 assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (G x))" |
1743 assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (G x))" |
1754 shows "eqvt_at f x" |
1746 shows "eqvt_at f x" |
1755 unfolding eqvt_at_def |
1747 unfolding eqvt_at_def |
1756 using assms |
1748 using assms |
1757 by (auto intro: fundef_ex1_eqvt) |
1749 by (auto intro: fundef_ex1_eqvt) |
1758 |
1750 |
1759 (* fixme: polish *) |
|
1760 lemma fundef_ex1_prop: |
1751 lemma fundef_ex1_prop: |
1761 fixes x::"'a::pt" |
1752 fixes x::"'a::pt" |
1762 assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (G x))" |
1753 assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (G x))" |
1763 assumes P_all: "\<And>x y. G x y \<Longrightarrow> P x y" |
1754 assumes P_all: "\<And>x y. G x y \<Longrightarrow> P x y" |
1764 assumes ex1: "\<exists>!y. G x y" |
1755 assumes ex1: "\<exists>!y. G x y" |
1765 shows "P x (f x)" |
1756 shows "P x (f x)" |
1766 unfolding f_def |
1757 unfolding f_def |
1767 using ex1 |
1758 using ex1 |
1768 apply(erule_tac ex1E) |
1759 apply(erule_tac ex1E) |
1769 apply(rule THE_defaultI2) |
1760 apply(rule THE_defaultI2) |
1770 apply(assumption) |
|
1771 apply(blast) |
1761 apply(blast) |
1772 apply(rule P_all) |
1762 apply(rule P_all) |
1773 apply(assumption) |
1763 apply(assumption) |
1774 done |
1764 done |
1775 |
1765 |