# 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(\ 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(\ x. P(x))" +proof - + { from i have "P(i) \ P(\ x. P(x))" + proof (induct i rule: trans_induct) + case (step i) + show ?case + proof (cases "P(\ a. P(a))") + case True thus ?thesis . + next + case False + hence "\x. x \ i \ ~P(x)" using step + by blast + hence "(\ 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) |] ==> (\ x. P(x)) \ 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 "(\ x. P(x)) \ i" +proof - + { from i have "P(i) \ (\ x. P(x)) \ i" + proof (induct i rule: trans_induct) + case (step i) + show ?case + proof (cases "(\ a. P(a)) \ i") + case True thus ?thesis . + next + case False + hence "\x. x \ i \ ~ (\ a. P(a)) \ i" using step + by blast + hence "(\ 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 < (\ 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| \ 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| \ A" +proof (unfold cardinal_def) + show "(\ i. i \ A) \ A" + by (best intro: LeastI Ord_ordertype ordermap_bij bij_converse_bij bij_imp_eqpoll r) +qed (* @{term"Ord(A) ==> |A| \ A"} *) lemmas Ord_cardinal_eqpoll = well_ord_Memrel [THEN well_ord_cardinal_eqpoll] @@ -358,7 +385,7 @@ lemma CardI: "[| Ord(i); !!j. j ~(j \ 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) \ Ord(K) & (\j. j ~ j \ 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 \ K" + assume "j < K" + also have "... = (\ i. i \ K)" using K + by (simp add: Card_def cardinal_def) + finally have "j < (\ i. i \ 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 i \ a" apply (unfold lesspoll_def) @@ -442,10 +476,11 @@ lemma cardinal_mono: assumes ij: "i \ j" shows "|i| \ |j|" -proof (cases rule: Ord_linear_le [OF Ord_cardinal Ord_cardinal]) - assume "|i| \ |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| \ |i|" + case ge have i: "Ord(i)" using ij by (simp add: lt_Ord) have ci: "|i| \ 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)| \ |nat|"}, the converse of cardinal_mono fails!*) +text{*Since we have @{term"|succ(nat)| \ |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 \ B" shows "|A| \ |B|" -proof (rule Ord_linear_le [of "|A|" "|B|", OF Ord_cardinal Ord_cardinal], assumption) - assume BA: "|B| \ |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 \ |B|" by (blast intro: wB eqpoll_sym well_ord_cardinal_eqpoll) - also have "... \ |A|" by (rule le_imp_lepoll [OF BA]) + also have "... \ |A|" by (rule le_imp_lepoll [OF ge]) also have "... \ A" by (rule well_ord_cardinal_eqpoll [OF s]) finally have "B \ A" . hence "A \ 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 \ nat" shows "i \ n \ 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 \ 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 \ n" using n by (rule lt_not_lepoll) hence "~ i \ n" using n by (blast intro: eqpoll_imp_lepoll) moreover have "i \ n" using `n B ==> Finite(A) \ 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 \ n; n \ 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 \ 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 \ n" and n: "n \ nat" shows "Finite(A)" +proof - + have "A \ n \ 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 \ n \ A \ 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 \ 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 \ 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 \ 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)) \ Finite(x)" by (blast intro: Finite_cons subset_Finite) lemma Finite_succ_iff [iff]: "Finite(succ(x)) \ Finite(x)" by (simp add: succ_def) +lemma Finite_Int: "Finite(A) | Finite(B) ==> Finite(A \ B)" +by (blast intro: subset_Finite) + +lemmas Finite_Diff = Diff_subset [THEN subset_Finite] + lemma nat_le_infinite_Ord: "[| Ord(i); ~ Finite(i) |] ==> nat \ i" apply (unfold Finite_def) @@ -931,11 +981,6 @@ lemma Finite_Fin: "[| Finite(A); A \ X |] ==> A \ Fin(X)" by (unfold Finite_def, blast intro: Finite_Fin_lemma) -lemma eqpoll_imp_Finite_iff: "A \ B ==> Finite(A) \ Finite(B)" -apply (unfold Finite_def) -apply (blast intro: eqpoll_trans eqpoll_sym) -done - lemma Fin_lemma [rule_format]: "n \ nat ==> \A. A \ n \ A \ 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 \ 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 \ 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: "\Z. Z = 0 \ (\z\Z. \y. z \ y \ z \ x \ y \ x \ z \ x \ y \ Z)" + by (simp add: wf_on_def wf_def) --{*not easy to erase the duplicate @{term"z \ x"}!*} + show ?case + proof (rule wf_onI) + fix Z u + assume Z: "u \ Z" "\z\Z. \y\Z. \y, z\ \ converse(Memrel(succ(x)))" + show False + proof (cases "x \ 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 \ 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 \ 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 -