--- a/src/HOL/Finite_Set.thy Tue Jun 13 15:07:47 2006 +0200
+++ b/src/HOL/Finite_Set.thy Tue Jun 13 15:07:58 2006 +0200
@@ -236,6 +236,9 @@
apply (subst insert_Diff, simp_all)
done
+lemma finite_Diff_singleton [simp]: "finite (A - {a}) = finite A"
+ by simp
+
text {* Image and Inverse Image over Finite Sets *}
--- a/src/HOL/Nat.thy Tue Jun 13 15:07:47 2006 +0200
+++ b/src/HOL/Nat.thy Tue Jun 13 15:07:58 2006 +0200
@@ -750,6 +750,26 @@
subsection {* Additional theorems about "less than" *}
+text{*An induction rule for estabilishing binary relations*}
+lemma less_Suc_induct:
+ assumes less: "i < j"
+ and step: "!!i. P i (Suc i)"
+ and trans: "!!i j k. P i j ==> P j k ==> P i k"
+ shows "P i j"
+proof -
+ from less obtain k where j: "j = Suc(i+k)" by (auto dest: less_imp_Suc_add)
+ have "P i (Suc(i+k))"
+ proof (induct k)
+ case 0
+ show ?case by (simp add: step)
+ next
+ case (Suc k)
+ thus ?case by (auto intro: prems)
+ qed
+ thus "P i j" by (simp add: j)
+qed
+
+
text {* A [clumsy] way of lifting @{text "<"}
monotonicity to @{text "\<le>"} monotonicity *}
lemma less_mono_imp_le_mono:
--- a/src/HOL/Set.thy Tue Jun 13 15:07:47 2006 +0200
+++ b/src/HOL/Set.thy Tue Jun 13 15:07:58 2006 +0200
@@ -785,6 +785,9 @@
lemma diff_single_insert: "A - {x} \<subseteq> B ==> x \<in> A ==> A \<subseteq> insert x B"
by blast
+lemma doubleton_eq_iff: "({a,b} = {c,d}) = (a=c & b=d | a=d & b=c)"
+ by (blast elim: equalityE)
+
subsubsection {* Unions of families *}
--- a/src/HOL/Wellfounded_Recursion.thy Tue Jun 13 15:07:47 2006 +0200
+++ b/src/HOL/Wellfounded_Recursion.thy Tue Jun 13 15:07:58 2006 +0200
@@ -86,25 +86,22 @@
done
-subsubsection{*Minimal-element characterization of well-foundedness*}
-
-lemma lemma1: "wf r ==> x:Q --> (EX z:Q. ALL y. (y,z):r --> y~:Q)"
-apply (unfold wf_def)
-apply (drule spec)
-apply (erule mp [THEN spec], blast)
-done
-
-lemma lemma2: "(ALL Q x. x:Q --> (EX z:Q. ALL y. (y,z):r --> y~:Q)) ==> wf r"
-apply (unfold wf_def, clarify)
-apply (drule_tac x = "{x. ~ P x}" in spec, blast)
-done
-
-lemma wf_eq_minimal: "wf r = (ALL Q x. x:Q --> (EX z:Q. ALL y. (y,z):r --> y~:Q))"
-by (blast intro!: lemma1 lemma2)
-
subsubsection{*Other simple well-foundedness results*}
+text{*Minimal-element characterization of well-foundedness*}
+lemma wf_eq_minimal: "wf r = (\<forall>Q x. x\<in>Q --> (\<exists>z\<in>Q. \<forall>y. (y,z)\<in>r --> y\<notin>Q))"
+proof (intro iffI strip)
+ fix Q::"'a set" and x
+ assume "wf r" and "x \<in> Q"
+ thus "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q"
+ by (unfold wf_def,
+ blast dest: spec [of _ "%x. x\<in>Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y,z) \<in> r \<longrightarrow> y\<notin>Q)"])
+next
+ assume "\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q)"
+ thus "wf r" by (unfold wf_def, force)
+qed
+
text{*Well-foundedness of subsets*}
lemma wf_subset: "[| wf(r); p<=r |] ==> wf(p)"
apply (simp (no_asm_use) add: wf_eq_minimal)
@@ -115,6 +112,12 @@
lemma wf_empty [iff]: "wf({})"
by (simp add: wf_def)
+lemma wf_Int1: "wf r ==> wf (r Int r')"
+by (erule wf_subset, rule Int_lower1)
+
+lemma wf_Int2: "wf r ==> wf (r' Int r)"
+by (erule wf_subset, rule Int_lower2)
+
text{*Well-foundedness of insert*}
lemma wf_insert [iff]: "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)"
apply (rule iffI)