author paulson Tue, 13 Jun 2006 15:07:58 +0200 changeset 19870 ef037d1b32d1 parent 19869 eba1b9e7c458 child 19871 88e8f6173bab
new results
 src/HOL/Finite_Set.thy file | annotate | diff | comparison | revisions src/HOL/Nat.thy file | annotate | diff | comparison | revisions src/HOL/Set.thy file | annotate | diff | comparison | revisions src/HOL/Wellfounded_Recursion.thy file | annotate | diff | comparison | revisions
```--- 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)```