# HG changeset patch
# User haftmann
# Date 1302174087 -7200
# Node ID a46a13b4be5fadab51f225bd27b1ab3068d79460
# Parent  7d08265f181dfb0c12dd1bb1d2cf443c5001782e
dropped unused lemmas; proper Isar proof

diff -r 7d08265f181d -r a46a13b4be5f src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Apr 07 12:16:27 2011 +0200
+++ b/src/HOL/Finite_Set.thy	Thu Apr 07 13:01:27 2011 +0200
@@ -561,14 +561,6 @@
 @{text fold_comm}, @{text fold_reindex} and @{text fold_distrib}.
 The proofs become ugly. It is not worth the effort. (???) *}
 
-
-lemma Diff1_fold_graph:
-  "fold_graph f z (A - {x}) y \<Longrightarrow> x \<in> A \<Longrightarrow> fold_graph f z A (f x y)"
-by (erule insert_Diff [THEN subst], rule fold_graph.intros, auto)
-
-lemma fold_graph_imp_finite: "fold_graph f z A x \<Longrightarrow> finite A"
-by (induct set: fold_graph) auto
-
 lemma finite_imp_fold_graph: "finite A \<Longrightarrow> \<exists>x. fold_graph f z A x"
 by (induct rule: finite_induct) auto
 
@@ -617,13 +609,16 @@
   "fold_graph f z A y \<Longrightarrow> fold f z A = y"
 by (unfold fold_def) (blast intro: fold_graph_determ)
 
-lemma fold_graph_fold: "finite A \<Longrightarrow> fold_graph f z A (fold f z A)"
-unfolding fold_def
-apply (rule theI')
-apply (rule ex_ex1I)
-apply (erule finite_imp_fold_graph)
-apply (erule (1) fold_graph_determ)
-done
+lemma fold_graph_fold:
+  assumes "finite A"
+  shows "fold_graph f z A (fold f z A)"
+proof -
+  from assms have "\<exists>x. fold_graph f z A x" by (rule finite_imp_fold_graph)
+  moreover note fold_graph_determ
+  ultimately have "\<exists>!x. fold_graph f z A x" by (rule ex_ex1I)
+  then have "fold_graph f z A (The (fold_graph f z A))" by (rule theI')
+  then show ?thesis by (unfold fold_def)
+qed
 
 text{* The base case for @{text fold}: *}