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 "P a" "\<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 |
1703 |
|
1704 thm THE_default1_equality |
|
1705 |
1704 lemma the_default_eqvt: |
1706 lemma the_default_eqvt: |
1705 assumes unique: "\<exists>!x. P x" |
1707 assumes unique: "\<exists>!x. P x" |
1706 shows "(p \<bullet> (THE_default d P)) = (THE_default d (p \<bullet> P))" |
1708 shows "(p \<bullet> (THE_default d P)) = (THE_default (p \<bullet> d) (p \<bullet> P))" |
1707 apply(rule THE_default1_equality [symmetric]) |
1709 apply(rule THE_default1_equality [symmetric]) |
1708 apply(rule_tac p="-p" in permute_boolE) |
1710 apply(rule_tac p="-p" in permute_boolE) |
1709 apply(simp add: ex1_eqvt) |
1711 apply(simp add: ex1_eqvt) |
1710 apply(rule unique) |
1712 apply(rule unique) |
1711 apply(rule_tac p="-p" in permute_boolE) |
1713 apply(rule_tac p="-p" in permute_boolE) |
1714 apply(rule THE_defaultI'[OF unique]) |
1716 apply(rule THE_defaultI'[OF unique]) |
1715 done |
1717 done |
1716 |
1718 |
1717 lemma fundef_ex1_eqvt: |
1719 lemma fundef_ex1_eqvt: |
1718 fixes x::"'a::pt" |
1720 fixes x::"'a::pt" |
1719 assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))" |
1721 assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (G x))" |
1720 assumes eqvt: "eqvt G" |
1722 assumes eqvt: "eqvt G" |
1721 assumes ex1: "\<exists>!y. G x y" |
1723 assumes ex1: "\<exists>!y. G x y" |
1722 shows "(p \<bullet> (f x)) = f (p \<bullet> x)" |
1724 shows "(p \<bullet> (f x)) = f (p \<bullet> x)" |
1723 apply(simp only: f_def) |
1725 apply(simp only: f_def) |
1724 apply(subst the_default_eqvt) |
1726 apply(subst the_default_eqvt) |
1725 apply(rule ex1) |
1727 apply(rule ex1) |
|
1728 apply(rule THE_default1_equality [symmetric]) |
|
1729 apply(rule_tac p="-p" in permute_boolE) |
|
1730 apply(perm_simp add: permute_minus_cancel) |
1726 using eqvt |
1731 using eqvt |
1727 unfolding eqvt_def |
1732 unfolding eqvt_def |
1728 apply(simp add: permute_fun_app_eq) |
1733 apply(simp) |
|
1734 apply(rule ex1) |
|
1735 apply(rule_tac p="-p" in permute_boolE) |
|
1736 apply(subst permute_fun_app_eq) |
|
1737 back |
|
1738 apply(subst the_default_eqvt) |
|
1739 apply(rule_tac p="-p" in permute_boolE) |
|
1740 apply(perm_simp add: permute_minus_cancel) |
|
1741 apply(rule ex1) |
|
1742 apply(perm_simp add: permute_minus_cancel) |
|
1743 using eqvt |
|
1744 unfolding eqvt_def |
|
1745 apply(simp) |
|
1746 apply(rule THE_defaultI'[OF ex1]) |
1729 done |
1747 done |
1730 |
1748 |
1731 lemma fundef_ex1_eqvt_at: |
1749 lemma fundef_ex1_eqvt_at: |
1732 fixes x::"'a::pt" |
1750 fixes x::"'a::pt" |
1733 assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))" |
1751 assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (G x))" |
1734 assumes eqvt: "eqvt G" |
1752 assumes eqvt: "eqvt G" |
1735 assumes ex1: "\<exists>!y. G x y" |
1753 assumes ex1: "\<exists>!y. G x y" |
1736 shows "eqvt_at f x" |
1754 shows "eqvt_at f x" |
1737 unfolding eqvt_at_def |
1755 unfolding eqvt_at_def |
1738 using assms |
1756 using assms |
1739 by (auto intro: fundef_ex1_eqvt) |
1757 by (auto intro: fundef_ex1_eqvt) |
1740 |
1758 |
1741 (* fixme: polish *) |
1759 (* fixme: polish *) |
1742 lemma fundef_ex1_prop: |
1760 lemma fundef_ex1_prop: |
1743 fixes x::"'a::pt" |
1761 fixes x::"'a::pt" |
1744 assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))" |
1762 assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (G x))" |
1745 assumes P_all: "\<And>x y. G x y \<Longrightarrow> P x y" |
1763 assumes P_all: "\<And>x y. G x y \<Longrightarrow> P x y" |
1746 assumes ex1: "\<exists>!y. G x y" |
1764 assumes ex1: "\<exists>!y. G x y" |
1747 shows "P x (f x)" |
1765 shows "P x (f x)" |
1748 unfolding f_def |
1766 unfolding f_def |
1749 using ex1 |
1767 using ex1 |