# HG changeset patch
# User paulson
# Date 1150204078 -7200
# Node ID ef037d1b32d15042ce24233af61080b9f7d79984
# Parent  eba1b9e7c45852558117fa8787dcafe8864a40d3
new results

diff -r eba1b9e7c458 -r ef037d1b32d1 src/HOL/Finite_Set.thy
--- 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 *}
 
diff -r eba1b9e7c458 -r ef037d1b32d1 src/HOL/Nat.thy
--- 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:
diff -r eba1b9e7c458 -r ef037d1b32d1 src/HOL/Set.thy
--- 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 *}
 
diff -r eba1b9e7c458 -r ef037d1b32d1 src/HOL/Wellfounded_Recursion.thy
--- 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)