84 impI: "(P ==> Q) ==> P-->Q" |
91 impI: "(P ==> Q) ==> P-->Q" |
85 mp: "[| P-->Q; P |] ==> Q" |
92 mp: "[| P-->Q; P |] ==> Q" |
86 |
93 |
87 FalseE: "False ==> P" |
94 FalseE: "False ==> P" |
88 |
95 |
89 |
96 (* Quantifiers *) |
|
97 |
|
98 allI: "(!!x. P(x)) ==> (ALL x. P(x))" |
|
99 spec: "(ALL x. P(x)) ==> P(x)" |
|
100 |
|
101 exI: "P(x) ==> (EX x. P(x))" |
|
102 exE: "[| EX x. P(x); !!x. P(x) ==> R |] ==> R" |
|
103 |
|
104 (* Reflection *) |
|
105 |
|
106 eq_reflection: "(x=y) ==> (x==y)" |
|
107 iff_reflection: "(P<->Q) ==> (P==Q)" |
|
108 |
|
109 |
|
110 defs |
90 (* Definitions *) |
111 (* Definitions *) |
91 |
112 |
92 True_def: "True == False-->False" |
113 True_def: "True == False-->False" |
93 not_def: "~P == P-->False" |
114 not_def: "~P == P-->False" |
94 iff_def: "P<->Q == (P-->Q) & (Q-->P)" |
115 iff_def: "P<->Q == (P-->Q) & (Q-->P)" |
95 |
116 |
96 (* Unique existence *) |
117 (* Unique existence *) |
97 |
118 |
98 ex1_def: "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)" |
119 ex1_def: "Ex1(P) == EX x. P(x) & (ALL y. P(y) --> y=x)" |
99 |
|
100 |
|
101 (* Quantifiers *) |
|
102 |
|
103 allI: "(!!x. P(x)) ==> (ALL x. P(x))" |
|
104 spec: "(ALL x. P(x)) ==> P(x)" |
|
105 |
|
106 exI: "P(x) ==> (EX x. P(x))" |
|
107 exE: "[| EX x. P(x); !!x. P(x) ==> R |] ==> R" |
|
108 |
|
109 (* Reflection *) |
|
110 |
|
111 eq_reflection: "(x=y) ==> (x==y)" |
|
112 iff_reflection: "(P<->Q) ==> (P==Q)" |
|
113 |
|
114 |
120 |
115 |
121 |
116 subsection {* Lemmas and proof tools *} |
122 subsection {* Lemmas and proof tools *} |
117 |
123 |
118 setup Simplifier.setup |
124 setup Simplifier.setup |