34 typedecl o |
34 typedecl o |
35 |
35 |
36 judgment |
36 judgment |
37 Trueprop :: "o => prop" ("(_)" 5) |
37 Trueprop :: "o => prop" ("(_)" 5) |
38 |
38 |
39 consts |
39 |
40 True :: o |
40 subsubsection {* Equality *} |
41 False :: o |
41 |
42 |
42 axiomatization |
43 (* Connectives *) |
43 eq :: "['a, 'a] => o" (infixl "=" 50) |
44 |
44 where |
45 eq :: "['a, 'a] => o" (infixl "=" 50) |
45 refl: "a=a" and |
46 |
46 subst: "a=b \<Longrightarrow> P(a) \<Longrightarrow> P(b)" |
47 Not :: "o => o" ("~ _" [40] 40) |
47 |
48 conj :: "[o, o] => o" (infixr "&" 35) |
48 |
49 disj :: "[o, o] => o" (infixr "|" 30) |
49 subsubsection {* Propositional logic *} |
50 imp :: "[o, o] => o" (infixr "-->" 25) |
50 |
51 iff :: "[o, o] => o" (infixr "<->" 25) |
51 axiomatization |
52 |
52 False :: o and |
53 (* Quantifiers *) |
53 conj :: "[o, o] => o" (infixr "&" 35) and |
54 |
54 disj :: "[o, o] => o" (infixr "|" 30) and |
55 All :: "('a => o) => o" (binder "ALL " 10) |
55 imp :: "[o, o] => o" (infixr "-->" 25) |
56 Ex :: "('a => o) => o" (binder "EX " 10) |
56 where |
57 Ex1 :: "('a => o) => o" (binder "EX! " 10) |
57 conjI: "[| P; Q |] ==> P&Q" and |
58 |
58 conjunct1: "P&Q ==> P" and |
59 |
59 conjunct2: "P&Q ==> Q" and |
60 abbreviation |
60 |
61 not_equal :: "['a, 'a] => o" (infixl "~=" 50) where |
61 disjI1: "P ==> P|Q" and |
62 "x ~= y == ~ (x = y)" |
62 disjI2: "Q ==> P|Q" and |
|
63 disjE: "[| P|Q; P ==> R; Q ==> R |] ==> R" and |
|
64 |
|
65 impI: "(P ==> Q) ==> P-->Q" and |
|
66 mp: "[| P-->Q; P |] ==> Q" and |
|
67 |
|
68 FalseE: "False ==> P" |
|
69 |
|
70 |
|
71 subsubsection {* Quantifiers *} |
|
72 |
|
73 axiomatization |
|
74 All :: "('a => o) => o" (binder "ALL " 10) and |
|
75 Ex :: "('a => o) => o" (binder "EX " 10) |
|
76 where |
|
77 allI: "(!!x. P(x)) ==> (ALL x. P(x))" and |
|
78 spec: "(ALL x. P(x)) ==> P(x)" and |
|
79 exI: "P(x) ==> (EX x. P(x))" and |
|
80 exE: "[| EX x. P(x); !!x. P(x) ==> R |] ==> R" |
|
81 |
|
82 |
|
83 subsubsection {* Definitions *} |
|
84 |
|
85 definition "True == False-->False" |
|
86 definition Not ("~ _" [40] 40) where not_def: "~P == P-->False" |
|
87 definition iff (infixr "<->" 25) where "P<->Q == (P-->Q) & (Q-->P)" |
|
88 |
|
89 definition Ex1 :: "('a => o) => o" (binder "EX! " 10) |
|
90 where ex1_def: "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)" |
|
91 |
|
92 axiomatization where -- {* Reflection, admissible *} |
|
93 eq_reflection: "(x=y) ==> (x==y)" and |
|
94 iff_reflection: "(P<->Q) ==> (P==Q)" |
|
95 |
|
96 |
|
97 subsubsection {* Additional notation *} |
|
98 |
|
99 abbreviation not_equal :: "['a, 'a] => o" (infixl "~=" 50) |
|
100 where "x ~= y == ~ (x = y)" |
63 |
101 |
64 notation (xsymbols) |
102 notation (xsymbols) |
65 not_equal (infixl "\<noteq>" 50) |
103 not_equal (infixl "\<noteq>" 50) |
66 |
104 |
67 notation (HTML output) |
105 notation (HTML output) |
68 not_equal (infixl "\<noteq>" 50) |
106 not_equal (infixl "\<noteq>" 50) |
69 |
107 |
70 notation (xsymbols) |
108 notation (xsymbols) |
71 Not ("\<not> _" [40] 40) and |
109 Not ("\<not> _" [40] 40) and |
72 conj (infixr "\<and>" 35) and |
110 conj (infixr "\<and>" 35) and |
73 disj (infixr "\<or>" 30) and |
111 disj (infixr "\<or>" 30) and |
74 All (binder "\<forall>" 10) and |
112 All (binder "\<forall>" 10) and |
75 Ex (binder "\<exists>" 10) and |
113 Ex (binder "\<exists>" 10) and |
76 Ex1 (binder "\<exists>!" 10) and |
114 Ex1 (binder "\<exists>!" 10) and |
77 imp (infixr "\<longrightarrow>" 25) and |
115 imp (infixr "\<longrightarrow>" 25) and |
78 iff (infixr "\<longleftrightarrow>" 25) |
116 iff (infixr "\<longleftrightarrow>" 25) |
79 |
117 |
80 notation (HTML output) |
118 notation (HTML output) |
81 Not ("\<not> _" [40] 40) and |
119 Not ("\<not> _" [40] 40) and |
82 conj (infixr "\<and>" 35) and |
120 conj (infixr "\<and>" 35) and |
83 disj (infixr "\<or>" 30) and |
121 disj (infixr "\<or>" 30) and |
84 All (binder "\<forall>" 10) and |
122 All (binder "\<forall>" 10) and |
85 Ex (binder "\<exists>" 10) and |
123 Ex (binder "\<exists>" 10) and |
86 Ex1 (binder "\<exists>!" 10) |
124 Ex1 (binder "\<exists>!" 10) |
87 |
125 |
88 finalconsts |
126 |
89 False All Ex eq conj disj imp |
127 subsection {* Lemmas and proof tools *} |
90 |
|
91 axiomatization where |
|
92 (* Equality *) |
|
93 refl: "a=a" and |
|
94 subst: "a=b \<Longrightarrow> P(a) \<Longrightarrow> P(b)" |
|
95 |
|
96 |
|
97 axiomatization where |
|
98 (* Propositional logic *) |
|
99 conjI: "[| P; Q |] ==> P&Q" and |
|
100 conjunct1: "P&Q ==> P" and |
|
101 conjunct2: "P&Q ==> Q" and |
|
102 |
|
103 disjI1: "P ==> P|Q" and |
|
104 disjI2: "Q ==> P|Q" and |
|
105 disjE: "[| P|Q; P ==> R; Q ==> R |] ==> R" and |
|
106 |
|
107 impI: "(P ==> Q) ==> P-->Q" and |
|
108 mp: "[| P-->Q; P |] ==> Q" and |
|
109 |
|
110 FalseE: "False ==> P" |
|
111 |
|
112 axiomatization where |
|
113 (* Quantifiers *) |
|
114 allI: "(!!x. P(x)) ==> (ALL x. P(x))" and |
|
115 spec: "(ALL x. P(x)) ==> P(x)" and |
|
116 |
|
117 exI: "P(x) ==> (EX x. P(x))" and |
|
118 exE: "[| EX x. P(x); !!x. P(x) ==> R |] ==> R" |
|
119 |
|
120 |
|
121 axiomatization where |
|
122 (* Reflection, admissible *) |
|
123 eq_reflection: "(x=y) ==> (x==y)" and |
|
124 iff_reflection: "(P<->Q) ==> (P==Q)" |
|
125 |
|
126 |
128 |
127 lemmas strip = impI allI |
129 lemmas strip = impI allI |
128 |
|
129 |
|
130 defs |
|
131 (* Definitions *) |
|
132 |
|
133 True_def: "True == False-->False" |
|
134 not_def: "~P == P-->False" |
|
135 iff_def: "P<->Q == (P-->Q) & (Q-->P)" |
|
136 |
|
137 (* Unique existence *) |
|
138 |
|
139 ex1_def: "Ex1(P) == EX x. P(x) & (ALL y. P(y) --> y=x)" |
|
140 |
|
141 |
|
142 subsection {* Lemmas and proof tools *} |
|
143 |
130 |
144 lemma TrueI: True |
131 lemma TrueI: True |
145 unfolding True_def by (rule impI) |
132 unfolding True_def by (rule impI) |
146 |
133 |
147 |
134 |