equal
deleted
inserted
replaced
1694 by auto |
1694 by auto |
1695 |
1695 |
1696 |
1696 |
1697 subsection {* helper functions for nominal_functions *} |
1697 subsection {* helper functions for nominal_functions *} |
1698 |
1698 |
|
1699 lemma THE_defaultI2: |
|
1700 assumes "P a" "\<exists>!x. P x" "\<And>x. P x \<Longrightarrow> Q x" |
|
1701 shows "Q (THE_default d P)" |
|
1702 by (iprover intro: assms THE_defaultI') |
|
1703 |
1699 lemma the_default_eqvt: |
1704 lemma the_default_eqvt: |
1700 assumes unique: "\<exists>!x. P x" |
1705 assumes unique: "\<exists>!x. P x" |
1701 shows "(p \<bullet> (THE_default d P)) = (THE_default d (p \<bullet> P))" |
1706 shows "(p \<bullet> (THE_default d P)) = (THE_default d (p \<bullet> P))" |
1702 apply(rule THE_default1_equality [symmetric]) |
1707 apply(rule THE_default1_equality [symmetric]) |
1703 apply(rule_tac p="-p" in permute_boolE) |
1708 apply(rule_tac p="-p" in permute_boolE) |
1730 assumes ex1: "\<exists>!y. G x y" |
1735 assumes ex1: "\<exists>!y. G x y" |
1731 shows "eqvt_at f x" |
1736 shows "eqvt_at f x" |
1732 unfolding eqvt_at_def |
1737 unfolding eqvt_at_def |
1733 using assms |
1738 using assms |
1734 by (auto intro: fundef_ex1_eqvt) |
1739 by (auto intro: fundef_ex1_eqvt) |
|
1740 |
|
1741 (* fixme: polish *) |
|
1742 lemma fundef_ex1_prop: |
|
1743 fixes x::"'a::pt" |
|
1744 assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))" |
|
1745 assumes P_all: "\<And>y. G x y \<Longrightarrow> P y" |
|
1746 assumes ex1: "\<exists>!y. G x y" |
|
1747 shows "P (f x)" |
|
1748 unfolding f_def |
|
1749 using ex1 |
|
1750 apply(erule_tac ex1E) |
|
1751 apply(rule THE_defaultI2) |
|
1752 apply(assumption) |
|
1753 apply(blast) |
|
1754 apply(rule P_all) |
|
1755 apply(assumption) |
|
1756 done |
1735 |
1757 |
1736 |
1758 |
1737 section {* Support of Finite Sets of Finitely Supported Elements *} |
1759 section {* Support of Finite Sets of Finitely Supported Elements *} |
1738 |
1760 |
1739 text {* support and freshness for atom sets *} |
1761 text {* support and freshness for atom sets *} |