# HG changeset patch # User blanchet # Date 1305206959 -7200 # Node ID ebf603e5406114d669f5d01eb6cfa04faa9caf14 # Parent 6b7ef9b724fdf40edf77e4ac42e9f9a74e3fbe74 remove problematic Isar proof diff -r 6b7ef9b724fd -r ebf603e54061 src/HOL/Metis_Examples/Abstraction.thy --- a/src/HOL/Metis_Examples/Abstraction.thy Thu May 12 15:29:19 2011 +0200 +++ b/src/HOL/Metis_Examples/Abstraction.thy Thu May 12 15:29:19 2011 +0200 @@ -68,18 +68,6 @@ lemma "(a, b) \ (SIGMA x:A. {y. x = f y}) \ a \ A \ a = f b" proof - assume A1: "(a, b) \ (SIGMA x:A. {y. x = f y})" - have F1: "\u. {u} = op = u" by (metis singleton_conv2 Collect_def) - have F2: "\y w v. v \ w -` op = y \ w v = y" - by (metis F1 vimage_singleton_eq) - have F3: "\x w. (\R. w (x R)) = x -` w" - by (metis vimage_Collect_eq Collect_def) - show "a \ A \ a = f b" by (metis A1 F2 F3 mem_Sigma_iff Collect_def) -qed - -(* Alternative structured proof *) -lemma "(a, b) \ (SIGMA x:A. {y. x = f y}) \ a \ A \ a = f b" -proof - - assume A1: "(a, b) \ (SIGMA x:A. {y. x = f y})" hence F1: "a \ A" by (metis mem_Sigma_iff) have "b \ {R. a = f R}" by (metis A1 mem_Sigma_iff) hence F2: "b \ (\R. a = f R)" by (metis Collect_def)