equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header {* Notions about functions *} |
6 header {* Notions about functions *} |
7 |
7 |
8 theory Fun |
8 theory Fun |
9 imports Complete_Lattice |
9 imports Complete_Lattices |
10 uses ("Tools/enriched_type.ML") |
10 uses ("Tools/enriched_type.ML") |
11 begin |
11 begin |
12 |
12 |
13 lemma apply_inverse: |
13 lemma apply_inverse: |
14 "f x = u \<Longrightarrow> (\<And>x. P x \<Longrightarrow> g (f x) = x) \<Longrightarrow> P x \<Longrightarrow> x = g u" |
14 "f x = u \<Longrightarrow> (\<And>x. P x \<Longrightarrow> g (f x) = x) \<Longrightarrow> P x \<Longrightarrow> x = g u" |