31 subsubsection {* Basic logical connectives *} |
31 subsubsection {* Basic logical connectives *} |
32 |
32 |
33 judgment |
33 judgment |
34 Trueprop :: "o \<Rightarrow> prop" ("_" 5) |
34 Trueprop :: "o \<Rightarrow> prop" ("_" 5) |
35 |
35 |
36 consts |
36 axiomatization |
37 imp :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<longrightarrow>" 25) |
37 imp :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<longrightarrow>" 25) and |
38 All :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<forall>" 10) |
38 All :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<forall>" 10) |
39 |
39 where |
40 axioms |
40 impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B" and |
41 impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B" |
41 impE [dest, trans]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B" and |
42 impE [dest, trans]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B" |
42 allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x" and |
43 allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x" |
|
44 allE [dest]: "\<forall>x. P x \<Longrightarrow> P a" |
43 allE [dest]: "\<forall>x. P x \<Longrightarrow> P a" |
45 |
44 |
46 |
45 |
47 subsubsection {* Extensional equality *} |
46 subsubsection {* Extensional equality *} |
48 |
47 |
49 consts |
48 axiomatization |
50 equal :: "'a \<Rightarrow> 'a \<Rightarrow> o" (infixl "=" 50) |
49 equal :: "'a \<Rightarrow> 'a \<Rightarrow> o" (infixl "=" 50) |
51 |
50 where |
52 axioms |
51 refl [intro]: "x = x" and |
53 refl [intro]: "x = x" |
|
54 subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y" |
52 subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y" |
55 ext [intro]: "(\<And>x. f x = g x) \<Longrightarrow> f = g" |
53 |
|
54 axiomatization where |
|
55 ext [intro]: "(\<And>x. f x = g x) \<Longrightarrow> f = g" and |
56 iff [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A = B" |
56 iff [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A = B" |
57 |
57 |
58 theorem sym [sym]: "x = y \<Longrightarrow> y = x" |
58 theorem sym [sym]: "x = y \<Longrightarrow> y = x" |
59 proof - |
59 proof - |
60 assume "x = y" |
60 assume "x = y" |
99 disj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<or>" 30) where |
99 disj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<or>" 30) where |
100 "disj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" |
100 "disj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" |
101 |
101 |
102 definition |
102 definition |
103 Ex :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<exists>" 10) where |
103 Ex :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<exists>" 10) where |
104 "Ex \<equiv> \<lambda>P. \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C" |
104 "\<exists>x. P x \<equiv> \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C" |
105 |
105 |
106 abbreviation |
106 abbreviation |
107 not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o" (infixl "\<noteq>" 50) where |
107 not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o" (infixl "\<noteq>" 50) where |
108 "x \<noteq> y \<equiv> \<not> (x = y)" |
108 "x \<noteq> y \<equiv> \<not> (x = y)" |
109 |
109 |