equal
deleted
inserted
replaced
196 (*** Rules for Descriptions ***) |
196 (*** Rules for Descriptions ***) |
197 |
197 |
198 qed_goalw "the_equality" thy [the_def] |
198 qed_goalw "the_equality" thy [the_def] |
199 "[| P(a); !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a" |
199 "[| P(a); !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a" |
200 (fn [pa,eq] => |
200 (fn [pa,eq] => |
201 [ (fast_tac (!claset addSIs [pa] addIs [equalityI] |
201 [ (fast_tac (!claset addSIs [pa] addEs [eq RS subst]) 1) ]); |
202 addEs [eq RS subst]) 1) ]); |
|
203 |
202 |
204 (* Only use this if you already know EX!x. P(x) *) |
203 (* Only use this if you already know EX!x. P(x) *) |
205 qed_goal "the_equality2" thy |
204 qed_goal "the_equality2" thy |
206 "!!P. [| EX! x. P(x); P(a) |] ==> (THE x. P(x)) = a" |
205 "!!P. [| EX! x. P(x); P(a) |] ==> (THE x. P(x)) = a" |
207 (fn _ => |
206 (fn _ => |
224 (THE x.P(x)) rewrites to (THE x. Q(x)) *) |
223 (THE x.P(x)) rewrites to (THE x. Q(x)) *) |
225 |
224 |
226 (*If it's "undefined", it's zero!*) |
225 (*If it's "undefined", it's zero!*) |
227 qed_goalw "the_0" thy [the_def] |
226 qed_goalw "the_0" thy [the_def] |
228 "!!P. ~ (EX! x. P(x)) ==> (THE x. P(x))=0" |
227 "!!P. ~ (EX! x. P(x)) ==> (THE x. P(x))=0" |
229 (fn _ => [ (fast_tac (!claset addIs [equalityI] addSEs [ReplaceE]) 1) ]); |
228 (fn _ => [ (fast_tac (!claset addSEs [ReplaceE]) 1) ]); |
230 |
229 |
231 |
230 |
232 (*** if -- a conditional expression for formulae ***) |
231 (*** if -- a conditional expression for formulae ***) |
233 |
232 |
234 goalw thy [if_def] "if(True,a,b) = a"; |
233 goalw thy [if_def] "if(True,a,b) = a"; |