equal
deleted
inserted
replaced
1740 |
1740 |
1741 (* fixme: polish *) |
1741 (* fixme: polish *) |
1742 lemma fundef_ex1_prop: |
1742 lemma fundef_ex1_prop: |
1743 fixes x::"'a::pt" |
1743 fixes x::"'a::pt" |
1744 assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))" |
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" |
1745 assumes P_all: "\<And>x y. G x y \<Longrightarrow> P x y" |
1746 assumes ex1: "\<exists>!y. G x y" |
1746 assumes ex1: "\<exists>!y. G x y" |
1747 shows "P (f x)" |
1747 shows "P x (f x)" |
1748 unfolding f_def |
1748 unfolding f_def |
1749 using ex1 |
1749 using ex1 |
1750 apply(erule_tac ex1E) |
1750 apply(erule_tac ex1E) |
1751 apply(rule THE_defaultI2) |
1751 apply(rule THE_defaultI2) |
1752 apply(assumption) |
1752 apply(assumption) |