82 |
82 |
83 (* Disjunction *) |
83 (* Disjunction *) |
84 |
84 |
85 disjI1 "a:P ==> inl(a):P|Q" |
85 disjI1 "a:P ==> inl(a):P|Q" |
86 disjI2 "b:Q ==> inr(b):P|Q" |
86 disjI2 "b:Q ==> inr(b):P|Q" |
87 disjE "[| a:P|Q; !!x.x:P ==> f(x):R; !!x.x:Q ==> g(x):R |
87 disjE "[| a:P|Q; !!x. x:P ==> f(x):R; !!x. x:Q ==> g(x):R |
88 |] ==> when(a,f,g):R" |
88 |] ==> when(a,f,g):R" |
89 |
89 |
90 (* Implication *) |
90 (* Implication *) |
91 |
91 |
92 impI "(!!x.x:P ==> f(x):Q) ==> lam x.f(x):P-->Q" |
92 impI "(!!x. x:P ==> f(x):Q) ==> lam x. f(x):P-->Q" |
93 mp "[| f:P-->Q; a:P |] ==> f`a:Q" |
93 mp "[| f:P-->Q; a:P |] ==> f`a:Q" |
94 |
94 |
95 (*Quantifiers*) |
95 (*Quantifiers*) |
96 |
96 |
97 allI "(!!x. f(x) : P(x)) ==> all x.f(x) : ALL x.P(x)" |
97 allI "(!!x. f(x) : P(x)) ==> all x. f(x) : ALL x. P(x)" |
98 spec "(f:ALL x.P(x)) ==> f^x : P(x)" |
98 spec "(f:ALL x. P(x)) ==> f^x : P(x)" |
99 |
99 |
100 exI "p : P(x) ==> [x,p] : EX x.P(x)" |
100 exI "p : P(x) ==> [x,p] : EX x. P(x)" |
101 exE "[| p: EX x.P(x); !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R" |
101 exE "[| p: EX x. P(x); !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R" |
102 |
102 |
103 (**** Equality between proofs ****) |
103 (**** Equality between proofs ****) |
104 |
104 |
105 prefl "a : P ==> a = a : P" |
105 prefl "a : P ==> a = a : P" |
106 psym "a = b : P ==> b = a : P" |
106 psym "a = b : P ==> b = a : P" |
107 ptrans "[| a = b : P; b = c : P |] ==> a = c : P" |
107 ptrans "[| a = b : P; b = c : P |] ==> a = c : P" |
108 |
108 |
109 idpeelB "[| !!x.f(x) : P(x,x) |] ==> idpeel(ideq(a),f) = f(a) : P(a,a)" |
109 idpeelB "[| !!x. f(x) : P(x,x) |] ==> idpeel(ideq(a),f) = f(a) : P(a,a)" |
110 |
110 |
111 fstB "a:P ==> fst(<a,b>) = a : P" |
111 fstB "a:P ==> fst(<a,b>) = a : P" |
112 sndB "b:Q ==> snd(<a,b>) = b : Q" |
112 sndB "b:Q ==> snd(<a,b>) = b : Q" |
113 pairEC "p:P&Q ==> p = <fst(p),snd(p)> : P&Q" |
113 pairEC "p:P&Q ==> p = <fst(p),snd(p)> : P&Q" |
114 |
114 |
115 whenBinl "[| a:P; !!x.x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q" |
115 whenBinl "[| a:P; !!x. x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q" |
116 whenBinr "[| b:P; !!x.x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q" |
116 whenBinr "[| b:P; !!x. x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q" |
117 plusEC "a:P|Q ==> when(a,%x.inl(x),%y.inr(y)) = p : P|Q" |
117 plusEC "a:P|Q ==> when(a,%x. inl(x),%y. inr(y)) = p : P|Q" |
118 |
118 |
119 applyB "[| a:P; !!x.x:P ==> b(x) : Q |] ==> (lam x.b(x)) ` a = b(a) : Q" |
119 applyB "[| a:P; !!x. x:P ==> b(x) : Q |] ==> (lam x. b(x)) ` a = b(a) : Q" |
120 funEC "f:P ==> f = lam x.f`x : P" |
120 funEC "f:P ==> f = lam x. f`x : P" |
121 |
121 |
122 specB "[| !!x.f(x) : P(x) |] ==> (all x.f(x)) ^ a = f(a) : P(a)" |
122 specB "[| !!x. f(x) : P(x) |] ==> (all x. f(x)) ^ a = f(a) : P(a)" |
123 |
123 |
124 |
124 |
125 (**** Definitions ****) |
125 (**** Definitions ****) |
126 |
126 |
127 not_def "~P == P-->False" |
127 not_def "~P == P-->False" |