equal
deleted
inserted
replaced
1707 apply(rule subst[OF permute_fun_app_eq]) |
1707 apply(rule subst[OF permute_fun_app_eq]) |
1708 apply(simp) |
1708 apply(simp) |
1709 apply(rule THE_defaultI'[OF unique]) |
1709 apply(rule THE_defaultI'[OF unique]) |
1710 done |
1710 done |
1711 |
1711 |
1712 lemma fundef_ex1_eqvt2: |
|
1713 fixes x::"'a::pt" |
|
1714 assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))" |
|
1715 assumes eqvt: "eqvt_at G x" |
|
1716 assumes ex1: "\<exists>!y. G x y" |
|
1717 shows "(p \<bullet> (f x)) = f (p \<bullet> x)" |
|
1718 apply(simp only: f_def) |
|
1719 apply(subst the_default_eqvt) |
|
1720 apply(rule ex1) |
|
1721 using eqvt |
|
1722 unfolding eqvt_at_def |
|
1723 apply(simp) |
|
1724 done |
|
1725 |
|
1726 lemma fundef_ex1_eqvt: |
1712 lemma fundef_ex1_eqvt: |
1727 fixes x::"'a::pt" |
1713 fixes x::"'a::pt" |
1728 assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))" |
1714 assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))" |
1729 assumes eqvt: "eqvt G" |
1715 assumes eqvt: "eqvt G" |
1730 assumes ex1: "\<exists>!y. G x y" |
1716 assumes ex1: "\<exists>!y. G x y" |
1734 apply(rule ex1) |
1720 apply(rule ex1) |
1735 using eqvt |
1721 using eqvt |
1736 unfolding eqvt_def |
1722 unfolding eqvt_def |
1737 apply(simp add: permute_fun_app_eq) |
1723 apply(simp add: permute_fun_app_eq) |
1738 done |
1724 done |
1739 |
|
1740 lemma fundef_ex1_eqvt_at2: |
|
1741 fixes x::"'a::pt" |
|
1742 assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))" |
|
1743 assumes eqvt: "eqvt_at G x" |
|
1744 assumes ex1: "\<exists>!y. G x y" |
|
1745 shows "eqvt_at f x" |
|
1746 unfolding eqvt_at_def |
|
1747 using assms |
|
1748 by (auto intro: fundef_ex1_eqvt2) |
|
1749 |
1725 |
1750 lemma fundef_ex1_eqvt_at: |
1726 lemma fundef_ex1_eqvt_at: |
1751 fixes x::"'a::pt" |
1727 fixes x::"'a::pt" |
1752 assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))" |
1728 assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))" |
1753 assumes eqvt: "eqvt G" |
1729 assumes eqvt: "eqvt G" |