# HG changeset patch
# User wenzelm
# Date 1332182994 -3600
# Node ID 63e23fc6259bec875a27b895bf7514c5d66bfd04
# Parent  7bdac8e81f6d532f0bb7437ac82ae1704759e111# Parent  e203b7d7e08dee640b13453c129457aa15a2492e
merged

diff -r e203b7d7e08d -r 63e23fc6259b src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Mon Mar 19 18:18:42 2012 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Mon Mar 19 19:49:54 2012 +0100
@@ -115,8 +115,8 @@
    postfactor = #postfactor Metis_Active.default}
 val waiting_params =
   {symbolsWeight = 1.0,
-   variablesWeight = 0.0,
-   literalsWeight = 0.0,
+   variablesWeight = 0.5,
+   literalsWeight = 0.1,
    models = []}
 val resolution_params = {active = active_params, waiting = waiting_params}
 
diff -r e203b7d7e08d -r 63e23fc6259b src/ZF/Cardinal.thy
--- a/src/ZF/Cardinal.thy	Mon Mar 19 18:18:42 2012 +0100
+++ b/src/ZF/Cardinal.thy	Mon Mar 19 19:49:54 2012 +0100
@@ -251,24 +251,52 @@
 apply (erule Ord_linear_lt, assumption, blast+)
 done
 
-lemma LeastI: "[| P(i);  Ord(i) |] ==> P(\<mu> x. P(x))"
-apply (erule rev_mp)
-apply (erule_tac i=i in trans_induct)
-apply (rule impI)
-apply (rule classical)
-apply (blast intro: Least_equality [THEN ssubst]  elim!: ltE)
-done
+lemma LeastI: 
+  assumes P: "P(i)" and i: "Ord(i)" shows "P(\<mu> x. P(x))"
+proof -
+  { from i have "P(i) \<Longrightarrow> P(\<mu> x. P(x))"
+      proof (induct i rule: trans_induct)
+        case (step i) 
+        show ?case
+          proof (cases "P(\<mu> a. P(a))")
+            case True thus ?thesis .
+          next
+            case False
+            hence "\<And>x. x \<in> i \<Longrightarrow> ~P(x)" using step
+              by blast
+            hence "(\<mu> a. P(a)) = i" using step
+              by (blast intro: Least_equality ltD) 
+            thus ?thesis using step.prems
+              by simp 
+          qed
+      qed
+  }
+  thus ?thesis using P .
+qed
 
-(*Proof is almost identical to the one above!*)
-lemma Least_le: "[| P(i);  Ord(i) |] ==> (\<mu> x. P(x)) \<le> i"
-apply (erule rev_mp)
-apply (erule_tac i=i in trans_induct)
-apply (rule impI)
-apply (rule classical)
-apply (subst Least_equality, assumption+)
-apply (erule_tac [2] le_refl)
-apply (blast elim: ltE intro: leI ltI lt_trans1)
-done
+text{*The proof is almost identical to the one above!*}
+lemma Least_le: 
+  assumes P: "P(i)" and i: "Ord(i)" shows "(\<mu> x. P(x)) \<le> i"
+proof -
+  { from i have "P(i) \<Longrightarrow> (\<mu> x. P(x)) \<le> i"
+      proof (induct i rule: trans_induct)
+        case (step i) 
+        show ?case
+          proof (cases "(\<mu> a. P(a)) \<le> i")
+            case True thus ?thesis .
+          next
+            case False
+            hence "\<And>x. x \<in> i \<Longrightarrow> ~ (\<mu> a. P(a)) \<le> i" using step
+              by blast
+            hence "(\<mu> a. P(a)) = i" using step
+              by (blast elim: ltE intro: ltI Least_equality lt_trans1)
+            thus ?thesis using step
+              by simp 
+          qed
+      qed
+  }
+  thus ?thesis using P .
+qed
 
 (*LEAST really is the smallest*)
 lemma less_LeastE: "[| P(i);  i < (\<mu> x. P(x)) |] ==> Q"
@@ -314,12 +342,11 @@
 
 (*Under AC, the premise becomes trivial; one consequence is ||A|| = |A|*)
 lemma well_ord_cardinal_eqpoll:
-    "well_ord(A,r) ==> |A| \<approx> A"
-apply (unfold cardinal_def)
-apply (rule LeastI)
-apply (erule_tac [2] Ord_ordertype)
-apply (erule ordermap_bij [THEN bij_converse_bij, THEN bij_imp_eqpoll])
-done
+  assumes r: "well_ord(A,r)" shows "|A| \<approx> A"
+proof (unfold cardinal_def)
+  show "(\<mu> i. i \<approx> A) \<approx> A"
+    by (best intro: LeastI Ord_ordertype ordermap_bij bij_converse_bij bij_imp_eqpoll r) 
+qed
 
 (* @{term"Ord(A) ==> |A| \<approx> A"} *)
 lemmas Ord_cardinal_eqpoll = well_ord_Memrel [THEN well_ord_cardinal_eqpoll]
@@ -358,7 +385,7 @@
 lemma CardI: "[| Ord(i);  !!j. j<i ==> ~(j \<approx> i) |] ==> Card(i)"
 apply (unfold Card_def cardinal_def)
 apply (subst Least_equality)
-apply (blast intro: eqpoll_refl )+
+apply (blast intro: eqpoll_refl)+
 done
 
 lemma Card_is_Ord: "Card(i) ==> Ord(i)"
@@ -376,14 +403,21 @@
 apply (rule Ord_Least)
 done
 
-(*The cardinals are the initial ordinals*)
+text{*The cardinals are the initial ordinals.*}
 lemma Card_iff_initial: "Card(K) \<longleftrightarrow> Ord(K) & (\<forall>j. j<K \<longrightarrow> ~ j \<approx> K)"
-apply (safe intro!: CardI Card_is_Ord)
- prefer 2 apply blast
-apply (unfold Card_def cardinal_def)
-apply (rule less_LeastE)
-apply (erule_tac [2] subst, assumption+)
-done
+proof -
+  { fix j
+    assume K: "Card(K)" "j \<approx> K"
+    assume "j < K"
+    also have "... = (\<mu> i. i \<approx> K)" using K
+      by (simp add: Card_def cardinal_def)
+    finally have "j < (\<mu> i. i \<approx> K)" .
+    hence "False" using K
+      by (best dest: less_LeastE) 
+  }
+  then show ?thesis
+    by (blast intro: CardI Card_is_Ord elim:) 
+qed
 
 lemma lt_Card_imp_lesspoll: "[| Card(a); i<a |] ==> i \<prec> a"
 apply (unfold lesspoll_def)
@@ -442,10 +476,11 @@
 
 lemma cardinal_mono:
   assumes ij: "i \<le> j" shows "|i| \<le> |j|"
-proof (cases rule: Ord_linear_le [OF Ord_cardinal Ord_cardinal])
-  assume "|i| \<le> |j|" thus ?thesis .
+using Ord_cardinal [of i] Ord_cardinal [of j]
+proof (cases rule: Ord_linear_le)
+  case le thus ?thesis .
 next
-  assume cj: "|j| \<le> |i|"
+  case ge
   have i: "Ord(i)" using ij
     by (simp add: lt_Ord)
   have ci: "|i| \<le> j"
@@ -453,12 +488,12 @@
   have "|i| = ||i||"
     by (auto simp add: Ord_cardinal_idem i)
   also have "... = |j|"
-    by (rule cardinal_eq_lemma [OF cj ci])
+    by (rule cardinal_eq_lemma [OF ge ci])
   finally have "|i| = |j|" .
   thus ?thesis by simp
 qed
 
-(*Since we have @{term"|succ(nat)| \<le> |nat|"}, the converse of cardinal_mono fails!*)
+text{*Since we have @{term"|succ(nat)| \<le> |nat|"}, the converse of @{text cardinal_mono} fails!*}
 lemma cardinal_lt_imp_lt: "[| |i| < |j|;  Ord(i);  Ord(j) |] ==> i < j"
 apply (rule Ord_linear2 [of i j], assumption+)
 apply (erule lt_trans2 [THEN lt_irrefl])
@@ -478,12 +513,15 @@
 lemma well_ord_lepoll_imp_Card_le:
   assumes wB: "well_ord(B,r)" and AB: "A \<lesssim> B"
   shows "|A| \<le> |B|"
-proof (rule Ord_linear_le [of "|A|" "|B|", OF Ord_cardinal Ord_cardinal], assumption)
-  assume BA: "|B| \<le> |A|"
+using Ord_cardinal [of A] Ord_cardinal [of B]
+proof (cases rule: Ord_linear_le)
+  case le thus ?thesis .
+next
+  case ge
   from lepoll_well_ord [OF AB wB]
   obtain s where s: "well_ord(A, s)" by blast
   have "B  \<approx> |B|" by (blast intro: wB eqpoll_sym well_ord_cardinal_eqpoll)
-  also have "... \<lesssim> |A|" by (rule le_imp_lepoll [OF BA])
+  also have "... \<lesssim> |A|" by (rule le_imp_lepoll [OF ge])
   also have "... \<approx> A" by (rule well_ord_cardinal_eqpoll [OF s])
   finally have "B \<lesssim> A" .
   hence "A \<approx> B" by (blast intro: eqpollI AB)
@@ -652,17 +690,16 @@
 text{*A slightly weaker version of @{text nat_eqpoll_iff}*}
 lemma Ord_nat_eqpoll_iff:
   assumes i: "Ord(i)" and n: "n \<in> nat" shows "i \<approx> n \<longleftrightarrow> i=n"
-proof (cases rule: Ord_linear_lt [OF i])
-  show "Ord(n)" using n by auto
-next
-  assume "i < n"
+using i nat_into_Ord [OF n]
+proof (cases rule: Ord_linear_lt)
+  case lt
   hence  "i \<in> nat" by (rule lt_nat_in_nat) (rule n)
   thus ?thesis by (simp add: nat_eqpoll_iff n)
 next
-  assume "i = n"
+  case eq
   thus ?thesis by (simp add: eqpoll_refl)
 next
-  assume "n < i"
+  case gt
   hence  "~ i \<lesssim> n" using n  by (rule lt_not_lepoll)
   hence  "~ i \<approx> n" using n  by (blast intro: eqpoll_imp_lepoll)
   moreover have "i \<noteq> n" using `n<i` by auto
@@ -832,19 +869,47 @@
 
 subsection {*Finite and infinite sets*}
 
+lemma eqpoll_imp_Finite_iff: "A \<approx> B ==> Finite(A) \<longleftrightarrow> Finite(B)"
+apply (unfold Finite_def)
+apply (blast intro: eqpoll_trans eqpoll_sym)
+done
+
 lemma Finite_0 [simp]: "Finite(0)"
 apply (unfold Finite_def)
 apply (blast intro!: eqpoll_refl nat_0I)
 done
 
-lemma lepoll_nat_imp_Finite: "[| A \<lesssim> n;  n \<in> nat |] ==> Finite(A)"
+lemma Finite_cons: "Finite(x) ==> Finite(cons(y,x))"
 apply (unfold Finite_def)
-apply (erule rev_mp)
-apply (erule nat_induct)
-apply (blast dest!: lepoll_0_is_0 intro!: eqpoll_refl nat_0I)
-apply (blast dest!: lepoll_succ_disj)
+apply (case_tac "y \<in> x")
+apply (simp add: cons_absorb)
+apply (erule bexE)
+apply (rule bexI)
+apply (erule_tac [2] nat_succI)
+apply (simp (no_asm_simp) add: succ_def cons_eqpoll_cong mem_not_refl)
+done
+
+lemma Finite_succ: "Finite(x) ==> Finite(succ(x))"
+apply (unfold succ_def)
+apply (erule Finite_cons)
 done
 
+lemma lepoll_nat_imp_Finite:
+  assumes A: "A \<lesssim> n" and n: "n \<in> nat" shows "Finite(A)"
+proof -
+  have "A \<lesssim> n \<Longrightarrow> Finite(A)" using n
+    proof (induct n)
+      case 0
+      hence "A = 0" by (rule lepoll_0_is_0) 
+      thus ?case by simp
+    next
+      case (succ n)
+      hence "A \<lesssim> n \<or> A \<approx> succ(n)" by (blast dest: lepoll_succ_disj)
+      thus ?case using succ by (auto simp add: Finite_def) 
+    qed
+  thus ?thesis using A .
+qed
+
 lemma lesspoll_nat_is_Finite:
      "A \<prec> nat ==> Finite(A)"
 apply (unfold Finite_def)
@@ -865,32 +930,17 @@
 
 lemmas subset_Finite = subset_imp_lepoll [THEN lepoll_Finite]
 
-lemma Finite_Int: "Finite(A) | Finite(B) ==> Finite(A \<inter> B)"
-by (blast intro: subset_Finite)
-
-lemmas Finite_Diff = Diff_subset [THEN subset_Finite]
-
-lemma Finite_cons: "Finite(x) ==> Finite(cons(y,x))"
-apply (unfold Finite_def)
-apply (case_tac "y \<in> x")
-apply (simp add: cons_absorb)
-apply (erule bexE)
-apply (rule bexI)
-apply (erule_tac [2] nat_succI)
-apply (simp (no_asm_simp) add: succ_def cons_eqpoll_cong mem_not_refl)
-done
-
-lemma Finite_succ: "Finite(x) ==> Finite(succ(x))"
-apply (unfold succ_def)
-apply (erule Finite_cons)
-done
-
 lemma Finite_cons_iff [iff]: "Finite(cons(y,x)) \<longleftrightarrow> Finite(x)"
 by (blast intro: Finite_cons subset_Finite)
 
 lemma Finite_succ_iff [iff]: "Finite(succ(x)) \<longleftrightarrow> Finite(x)"
 by (simp add: succ_def)
 
+lemma Finite_Int: "Finite(A) | Finite(B) ==> Finite(A \<inter> B)"
+by (blast intro: subset_Finite)
+
+lemmas Finite_Diff = Diff_subset [THEN subset_Finite]
+
 lemma nat_le_infinite_Ord:
       "[| Ord(i);  ~ Finite(i) |] ==> nat \<le> i"
 apply (unfold Finite_def)
@@ -931,11 +981,6 @@
 lemma Finite_Fin: "[| Finite(A); A \<subseteq> X |] ==> A \<in> Fin(X)"
 by (unfold Finite_def, blast intro: Finite_Fin_lemma)
 
-lemma eqpoll_imp_Finite_iff: "A \<approx> B ==> Finite(A) \<longleftrightarrow> Finite(B)"
-apply (unfold Finite_def)
-apply (blast intro: eqpoll_trans eqpoll_sym)
-done
-
 lemma Fin_lemma [rule_format]: "n \<in> nat ==> \<forall>A. A \<approx> n \<longrightarrow> A \<in> Fin(A)"
 apply (induct_tac n)
 apply (simp add: eqpoll_0_iff, clarify)
@@ -1056,22 +1101,30 @@
   set is well-ordered.  Proofs simplified by lcp. *)
 
 lemma nat_wf_on_converse_Memrel: "n \<in> nat ==> wf[n](converse(Memrel(n)))"
-apply (erule nat_induct)
-apply (blast intro: wf_onI)
-apply (rule wf_onI)
-apply (simp add: wf_on_def wf_def)
-apply (case_tac "x \<in> Z")
- txt{*true case*}
- apply (drule_tac x = x in bspec, assumption)
- apply (blast elim: mem_irrefl mem_asym)
-txt{*other case*}
-apply (drule_tac x = Z in spec, blast)
-done
+proof (induct n rule: nat_induct)
+  case 0 thus ?case by (blast intro: wf_onI)
+next
+  case (succ x)
+  hence wfx: "\<And>Z. Z = 0 \<or> (\<exists>z\<in>Z. \<forall>y. z \<in> y \<and> z \<in> x \<and> y \<in> x \<and> z \<in> x \<longrightarrow> y \<notin> Z)"
+    by (simp add: wf_on_def wf_def)  --{*not easy to erase the duplicate @{term"z \<in> x"}!*}
+  show ?case
+    proof (rule wf_onI)
+      fix Z u
+      assume Z: "u \<in> Z" "\<forall>z\<in>Z. \<exists>y\<in>Z. \<langle>y, z\<rangle> \<in> converse(Memrel(succ(x)))"
+      show False 
+        proof (cases "x \<in> Z")
+          case True thus False using Z
+            by (blast elim: mem_irrefl mem_asym)
+          next
+          case False thus False using wfx [of Z] Z
+            by blast
+        qed
+    qed
+qed
 
 lemma nat_well_ord_converse_Memrel: "n \<in> nat ==> well_ord(n,converse(Memrel(n)))"
 apply (frule Ord_nat [THEN Ord_in_Ord, THEN well_ord_Memrel])
-apply (unfold well_ord_def)
-apply (blast intro!: tot_ord_converse nat_wf_on_converse_Memrel)
+apply (simp add: well_ord_def tot_ord_converse nat_wf_on_converse_Memrel) 
 done
 
 lemma well_ord_converse:
@@ -1104,9 +1157,7 @@
 done
 
 lemma nat_into_Finite: "n \<in> nat ==> Finite(n)"
-apply (unfold Finite_def)
-apply (fast intro!: eqpoll_refl)
-done
+  by (auto simp add: Finite_def intro: eqpoll_refl) 
 
 lemma nat_not_Finite: "~ Finite(nat)"
 proof -