equal
deleted
inserted
replaced
8 |
8 |
9 text\<open>Allows quantification over any term. Used to quantify over classes. |
9 text\<open>Allows quantification over any term. Used to quantify over classes. |
10 Yields a proposition rather than a FOL formula.\<close> |
10 Yields a proposition rather than a FOL formula.\<close> |
11 |
11 |
12 definition |
12 definition |
13 ex :: "(('a::{}) \<Rightarrow> prop) \<Rightarrow> prop" (binder "\<Or>" 0) where |
13 ex :: "(('a::{}) \<Rightarrow> prop) \<Rightarrow> prop" (binder \<open>\<Or>\<close> 0) where |
14 "ex(P) == (\<And>Q. (\<And>x. PROP P(x) \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q)" |
14 "ex(P) == (\<And>Q. (\<And>x. PROP P(x) \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q)" |
15 |
15 |
16 lemma meta_exI: "PROP P(x) ==> (\<Or>x. PROP P(x))" |
16 lemma meta_exI: "PROP P(x) ==> (\<Or>x. PROP P(x))" |
17 proof (unfold ex_def) |
17 proof (unfold ex_def) |
18 assume P: "PROP P(x)" |
18 assume P: "PROP P(x)" |