# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1270631111 -7200
# Node ID fa0e354e6a39fd2bcdb5d4ca44a16263460b263c
# Parent  59f6773a7d1d8700adb9dfd9fc078dee6d3c4588
simplified induction case in finite_psubset_induct; tuned the proof that uses this induction principle

diff -r 59f6773a7d1d -r fa0e354e6a39 src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Tue Apr 06 11:00:57 2010 +0200
+++ b/src/HOL/Big_Operators.thy	Wed Apr 07 11:05:11 2010 +0200
@@ -1676,27 +1676,31 @@
 qed
 
 lemma finite_linorder_max_induct[consumes 1, case_names empty insert]:
- "finite A \<Longrightarrow> P {} \<Longrightarrow>
-  (!!b A. finite A \<Longrightarrow> ALL a:A. a < b \<Longrightarrow> P A \<Longrightarrow> P(insert b A))
-  \<Longrightarrow> P A"
+ assumes fin: "finite A"
+ and   empty: "P {}" 
+ and  insert: "(!!b A. finite A \<Longrightarrow> ALL a:A. a < b \<Longrightarrow> P A \<Longrightarrow> P(insert b A))"
+ shows "P A"
+using fin empty insert
 proof (induct rule: finite_psubset_induct)
-  fix A :: "'a set"
-  assume IH: "!! B. finite B \<Longrightarrow> B < A \<Longrightarrow> P {} \<Longrightarrow>
-                 (!!b A. finite A \<Longrightarrow> (\<forall>a\<in>A. a<b) \<Longrightarrow> P A \<Longrightarrow> P (insert b A))
-                  \<Longrightarrow> P B"
-  and "finite A" and "P {}"
-  and step: "!!b A. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)"
+  case (psubset A)
+  have IH: "\<And>B. \<lbrakk>B < A; P {}; (\<And>A b. \<lbrakk>finite A; \<forall>a\<in>A. a<b; P A\<rbrakk> \<Longrightarrow> P (insert b A))\<rbrakk> \<Longrightarrow> P B" by fact 
+  have fin: "finite A" by fact 
+  have empty: "P {}" by fact
+  have step: "\<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)" by fact
   show "P A"
   proof (cases "A = {}")
-    assume "A = {}" thus "P A" using `P {}` by simp
+    assume "A = {}" 
+    then show "P A" using `P {}` by simp
   next
-    let ?B = "A - {Max A}" let ?A = "insert (Max A) ?B"
+    let ?B = "A - {Max A}" 
+    let ?A = "insert (Max A) ?B"
+    have "finite ?B" using `finite A` by simp
     assume "A \<noteq> {}"
     with `finite A` have "Max A : A" by auto
-    hence A: "?A = A" using insert_Diff_single insert_absorb by auto
-    moreover have "finite ?B" using `finite A` by simp
-    ultimately have "P ?B" using `P {}` step IH[of ?B] by blast
-    moreover have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF `finite A`] by fastsimp
+    then have A: "?A = A" using insert_Diff_single insert_absorb by auto
+    then have "P ?B" using `P {}` step IH[of ?B] by blast
+    moreover 
+    have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF `finite A`] by fastsimp
     ultimately show "P A" using A insert_Diff_single step[OF `finite ?B`] by fastsimp
   qed
 qed
diff -r 59f6773a7d1d -r fa0e354e6a39 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Apr 06 11:00:57 2010 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Apr 07 11:05:11 2010 +0200
@@ -2045,15 +2045,24 @@
 by auto
 
 lemma finite_psubset_induct[consumes 1, case_names psubset]:
-  assumes "finite A" and "!!A. finite A \<Longrightarrow> (!!B. finite B \<Longrightarrow> B \<subset> A \<Longrightarrow> P(B)) \<Longrightarrow> P(A)" shows "P A"
-using assms(1)
-proof (induct A rule: measure_induct_rule[where f=card])
+  assumes fin: "finite A" 
+  and     major: "\<And>A. finite A \<Longrightarrow> (\<And>B. B \<subset> A \<Longrightarrow> P B) \<Longrightarrow> P A" 
+  shows "P A"
+using fin
+proof (induct A taking: card rule: measure_induct_rule)
   case (less A)
-  show ?case
-  proof(rule assms(2)[OF less(2)])
-    fix B assume "finite B" "B \<subset> A"
-    show "P B" by(rule less(1)[OF psubset_card_mono[OF less(2) `B \<subset> A`] `finite B`])
-  qed
+  have fin: "finite A" by fact
+  have ih: "\<And>B. \<lbrakk>card B < card A; finite B\<rbrakk> \<Longrightarrow> P B" by fact
+  { fix B 
+    assume asm: "B \<subset> A"
+    from asm have "card B < card A" using psubset_card_mono fin by blast
+    moreover
+    from asm have "B \<subseteq> A" by auto
+    then have "finite B" using fin finite_subset by blast
+    ultimately 
+    have "P B" using ih by simp
+  }
+  with fin show "P A" using major by blast
 qed
 
 text{* main cardinality theorem *}