equal
deleted
inserted
replaced
208 "[| A = B; [| A<=B; B<=(A::'a set) |] ==> P |] ==> P"; |
208 "[| A = B; [| A<=B; B<=(A::'a set) |] ==> P |] ==> P"; |
209 by (resolve_tac prems 1); |
209 by (resolve_tac prems 1); |
210 by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1)); |
210 by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1)); |
211 qed "equalityE"; |
211 qed "equalityE"; |
212 |
212 |
213 AddEs [equalityE]; |
|
214 |
|
215 val major::prems = Goal |
213 val major::prems = Goal |
216 "[| A = B; [| c:A; c:B |] ==> P; [| c~:A; c~:B |] ==> P |] ==> P"; |
214 "[| A = B; [| c:A; c:B |] ==> P; [| c~:A; c~:B |] ==> P |] ==> P"; |
217 by (rtac (major RS equalityE) 1); |
215 by (rtac (major RS equalityE) 1); |
218 by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1)); |
216 by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1)); |
219 qed "equalityCE"; |
217 qed "equalityCE"; |
|
218 |
|
219 AddEs [equalityCE]; |
220 |
220 |
221 (*Lemma for creating induction formulae -- for "pattern matching" on p |
221 (*Lemma for creating induction formulae -- for "pattern matching" on p |
222 To make the induction hypotheses usable, apply "spec" or "bspec" to |
222 To make the induction hypotheses usable, apply "spec" or "bspec" to |
223 put universal quantifiers over the free variables in p. *) |
223 put universal quantifiers over the free variables in p. *) |
224 val prems = Goal |
224 val prems = Goal |