# HG changeset patch # User noschinl # Date 1331584960 -3600 # Node ID 48c82ef7d4687ebc947d4a9d664058f037f40c15 # Parent 154dc6ec00411008e2389ed4ff6ccee32befa8c4# Parent d4fdc61d9336446778cd86efcbd4689f3aeeb6cb merged diff -r 154dc6ec0041 -r 48c82ef7d468 Admin/polyml/build --- a/Admin/polyml/build Mon Mar 12 21:41:11 2012 +0100 +++ b/Admin/polyml/build Mon Mar 12 21:42:40 2012 +0100 @@ -51,14 +51,14 @@ OPTIONS=() ;; x86-darwin) - OPTIONS=(--build=i686-darwin CFLAGS='-arch i686 -O3' - CXXFLAGS='-arch i686 -O3' CCASFLAGS='-arch i686 -O3' + OPTIONS=(--build=i686-darwin CFLAGS='-arch i686 -O3 -I../libffi/include' + CXXFLAGS='-arch i686 -O3 -I../libffi/include' CCASFLAGS='-arch i686 -O3' LDFLAGS='-segprot POLY rwx rwx') ;; x86_64-darwin) - OPTIONS=(--build=x86_64-darwin CFLAGS='-arch x86_64 -O3' - CXXFLAGS='-arch x86_64 -O3' CCASFLAGS='-arch x86_64' - LDFLAGS='-segprot POLY rwx rwx') + OPTIONS=(--build=x86_64-darwin CFLAGS='-arch x86_64 -O3 -I../libffi/include' + CXXFLAGS='-arch x86_64 -O3 -I../libffi/include' CCASFLAGS='-arch x86_64' + LDFLAGS='-segprot POLY rwx rwx') ;; x86-cygwin) OPTIONS=() diff -r 154dc6ec0041 -r 48c82ef7d468 src/Provers/classical.ML --- a/src/Provers/classical.ML Mon Mar 12 21:41:11 2012 +0100 +++ b/src/Provers/classical.ML Mon Mar 12 21:42:40 2012 +0100 @@ -301,9 +301,9 @@ error ("Ill-formed destruction rule\n" ^ string_of_thm context th) else Tactic.make_elim th; -fun warn_thm context msg th = - if (case context of SOME (Context.Proof ctxt) => Context_Position.is_visible ctxt | _ => false) - then warning (msg ^ string_of_thm context th) +fun warn_thm opt_context msg th = + if (case opt_context of SOME context => Context_Position.is_visible_proof context | NONE => false) + then warning (msg ^ string_of_thm opt_context th) else (); fun warn_rules context msg rules th = diff -r 154dc6ec0041 -r 48c82ef7d468 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Mon Mar 12 21:41:11 2012 +0100 +++ b/src/Pure/Isar/outer_syntax.ML Mon Mar 12 21:42:40 2012 +0100 @@ -34,7 +34,7 @@ val process_file: Path.T -> theory -> theory type isar val isar: TextIO.instream -> bool -> isar - val read_command: Position.T -> string -> Toplevel.transition + val read_span: outer_syntax -> Token.T list -> Toplevel.transition * bool val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element -> (Toplevel.transition * Toplevel.transition list) list end; @@ -270,12 +270,6 @@ handle ERROR msg => (Toplevel.malformed range_pos msg, true) end; -fun read_command pos str = - let - val (lexs, outer_syntax) = get_syntax (); - val toks = Thy_Syntax.parse_tokens lexs pos str; - in #1 (read_span outer_syntax toks) end; - fun read_element outer_syntax init {head, proof, proper_proof} = let val read = read_span outer_syntax o Thy_Syntax.span_content; diff -r 154dc6ec0041 -r 48c82ef7d468 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Mon Mar 12 21:41:11 2012 +0100 +++ b/src/Pure/PIDE/document.ML Mon Mar 12 21:42:40 2012 +0100 @@ -240,7 +240,7 @@ abstype state = State of {versions: version Inttab.table, (*version_id -> document content*) - commands: (string * Toplevel.transition future) Inttab.table, (*command_id -> name * transition*) + commands: (string * Token.T list future) Inttab.table, (*command_id -> name * span*) execution: version_id * Future.group} (*current execution process*) with @@ -273,17 +273,18 @@ (* commands *) +fun tokenize_command id text = + Position.setmp_thread_data (Position.id_only id) + (fn () => Thy_Syntax.parse_tokens (#1 (Outer_Syntax.get_syntax ())) (Position.id id) text) (); + fun define_command (id: command_id) name text = map_state (fn (versions, commands, execution) => let - val id_string = print_id id; val future = (singleton o Future.forks) {name = "Document.define_command", group = SOME (Future.new_group NONE), deps = [], pri = ~1, interrupts = false} - (fn () => - Position.setmp_thread_data (Position.id_only id_string) - (fn () => Outer_Syntax.read_command (Position.id id_string) text) ()); + (fn () => tokenize_command (print_id id) text); val commands' = Inttab.update_new (id, (name, future)) commands handle Inttab.DUP dup => err_dup "command" dup; @@ -408,16 +409,20 @@ if bad_init andalso is_none init then NONE else let - val (name, tr0) = the_command state command_id' ||> Future.join; + val (name, span) = the_command state command_id' ||> Future.join; val (modify_init, init') = if Keyword.is_theory_begin name then (Toplevel.modify_init (the_default illegal_init init), NONE) else (I, init); val exec_id' = new_id (); - val tr = tr0 - |> modify_init - |> Toplevel.put_id (print_id exec_id'); - val exec' = snd (snd command_exec) |> Lazy.map (fn (st, _) => run_command tr st); + val exec_id'_string = print_id exec_id'; + val tr = + Position.setmp_thread_data (Position.id_only exec_id'_string) + (fn () => + #1 (Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span) + |> modify_init + |> Toplevel.put_id exec_id'_string); + val exec' = snd (snd command_exec) |> Lazy.map (fn (st, _) => run_command (tr ()) st); val command_exec' = (command_id', (exec_id', exec')); in SOME (command_exec' :: execs, command_exec', init') end; diff -r 154dc6ec0041 -r 48c82ef7d468 src/Pure/context_position.ML --- a/src/Pure/context_position.ML Mon Mar 12 21:41:11 2012 +0100 +++ b/src/Pure/context_position.ML Mon Mar 12 21:42:40 2012 +0100 @@ -10,6 +10,7 @@ val set_visible: bool -> Proof.context -> Proof.context val restore_visible: Proof.context -> Proof.context -> Proof.context val if_visible: Proof.context -> ('a -> unit) -> 'a -> unit + val is_visible_proof: Context.generic -> bool val if_visible_proof: Context.generic -> ('a -> unit) -> 'a -> unit val reported_text: Proof.context -> Position.T -> Markup.T -> string -> string val report_text: Proof.context -> Position.T -> Markup.T -> string -> unit @@ -27,8 +28,10 @@ fun if_visible ctxt f x = if is_visible ctxt then f x else (); -fun if_visible_proof (Context.Proof ctxt) f x = if_visible ctxt f x - | if_visible_proof _ _ _ = (); +fun is_visible_proof (Context.Proof ctxt) = is_visible ctxt + | is_visible_proof _ = false; + +fun if_visible_proof context f x = if is_visible_proof context then f x else (); fun reported_text ctxt pos markup txt = if is_visible ctxt then Position.reported_text pos markup txt else ""; diff -r 154dc6ec0041 -r 48c82ef7d468 src/Pure/type_infer_context.ML --- a/src/Pure/type_infer_context.ML Mon Mar 12 21:41:11 2012 +0100 +++ b/src/Pure/type_infer_context.ML Mon Mar 12 21:42:40 2012 +0100 @@ -118,18 +118,14 @@ fun prepare_positions ctxt tms = let - val visible = Context_Position.is_visible ctxt; - fun prepareT (Type (a, Ts)) ps_idx = let val (Ts', ps_idx') = fold_map prepareT Ts ps_idx in (Type (a, Ts'), ps_idx') end | prepareT T (ps, idx) = (case Term_Position.decode_positionT T of SOME pos => - if visible then - let val U = Type_Infer.mk_param idx [] - in (U, ((pos, U) :: ps, idx + 1)) end - else (dummyT, (ps, idx)) + let val U = Type_Infer.mk_param idx [] + in (U, ((pos, U) :: ps, idx + 1)) end | NONE => (T, (ps, idx))); fun prepare (Const ("_type_constraint_", T)) ps_idx = diff -r 154dc6ec0041 -r 48c82ef7d468 src/ZF/Cardinal.thy --- a/src/ZF/Cardinal.thy Mon Mar 12 21:41:11 2012 +0100 +++ b/src/ZF/Cardinal.thy Mon Mar 12 21:42:40 2012 +0100 @@ -440,15 +440,23 @@ finally show "i \ j" . qed -lemma cardinal_mono: "i \ j ==> |i| \ |j|" -apply (rule_tac i = "|i|" and j = "|j|" in Ord_linear_le) -apply (safe intro!: Ord_cardinal le_eqI) -apply (rule cardinal_eq_lemma) -prefer 2 apply assumption -apply (erule le_trans) -apply (erule ltE) -apply (erule Ord_cardinal_le) -done +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 . +next + assume cj: "|j| \ |i|" + have i: "Ord(i)" using ij + by (simp add: lt_Ord) + have ci: "|i| \ j" + by (blast intro: Ord_cardinal_le ij le_trans i) + have "|i| = ||i||" + by (auto simp add: Ord_cardinal_idem i) + also have "... = |j|" + by (rule cardinal_eq_lemma [OF cj ci]) + finally have "|i| = |j|" . + thus ?thesis by simp +qed (*Since we have @{term"|succ(nat)| \ |nat|"}, the converse of cardinal_mono fails!*) lemma cardinal_lt_imp_lt: "[| |i| < |j|; Ord(i); Ord(j) |] ==> i < j" @@ -458,8 +466,7 @@ done lemma Card_lt_imp_lt: "[| |i| < K; Ord(i); Card(K) |] ==> i < K" -apply (simp (no_asm_simp) add: cardinal_lt_imp_lt Card_is_Ord Card_cardinal_eq) -done + by (simp (no_asm_simp) add: cardinal_lt_imp_lt Card_is_Ord Card_cardinal_eq) lemma Card_lt_iff: "[| Ord(i); Card(K) |] ==> (|i| < K) \ (i < K)" by (blast intro: Card_lt_imp_lt Ord_cardinal_le [THEN lt_trans1]) @@ -532,8 +539,9 @@ apply (rule mem_not_refl)+ done + lemma nat_lepoll_imp_le [rule_format]: - "m:nat ==> \n\nat. m \ n \ m \ n" + "m \ nat ==> \n\nat. m \ n \ m \ n" apply (induct_tac m) apply (blast intro!: nat_0_le) apply (rule ballI) @@ -542,7 +550,7 @@ apply (blast intro!: succ_leI dest!: succ_lepoll_succD) done -lemma nat_eqpoll_iff: "[| m:nat; n: nat |] ==> m \ n \ m = n" +lemma nat_eqpoll_iff: "[| m \ nat; n: nat |] ==> m \ n \ m = n" apply (rule iffI) apply (blast intro: nat_lepoll_imp_le le_anti_sym elim!: eqpollE) apply (simp add: eqpoll_refl) @@ -564,7 +572,7 @@ (*Part of Kunen's Lemma 10.6*) -lemma succ_lepoll_natE: "[| succ(n) \ n; n:nat |] ==> P" +lemma succ_lepoll_natE: "[| succ(n) \ n; n \ nat |] ==> P" by (rule nat_lepoll_imp_le [THEN lt_irrefl], auto) lemma nat_lepoll_imp_ex_eqpoll_n: @@ -580,27 +588,32 @@ (** lepoll, \ and natural numbers **) +lemma lepoll_succ: "i \ succ(i)" + by (blast intro: subset_imp_lepoll) + lemma lepoll_imp_lesspoll_succ: - "[| A \ m; m:nat |] ==> A \ succ(m)" -apply (unfold lesspoll_def) -apply (rule conjI) -apply (blast intro: subset_imp_lepoll [THEN [2] lepoll_trans]) -apply (rule notI) -apply (drule eqpoll_sym [THEN eqpoll_imp_lepoll]) -apply (drule lepoll_trans, assumption) -apply (erule succ_lepoll_natE, assumption) + assumes A: "A \ m" and m: "m \ nat" + shows "A \ succ(m)" +proof - + { assume "A \ succ(m)" + hence "succ(m) \ A" by (rule eqpoll_sym) + also have "... \ m" by (rule A) + finally have "succ(m) \ m" . + hence False by (rule succ_lepoll_natE) (rule m) } + moreover have "A \ succ(m)" by (blast intro: lepoll_trans A lepoll_succ) + ultimately show ?thesis by (auto simp add: lesspoll_def) +qed + +lemma lesspoll_succ_imp_lepoll: + "[| A \ succ(m); m \ nat |] ==> A \ m" +apply (unfold lesspoll_def lepoll_def eqpoll_def bij_def) +apply (auto dest: inj_not_surj_succ) done -lemma lesspoll_succ_imp_lepoll: - "[| A \ succ(m); m:nat |] ==> A \ m" -apply (unfold lesspoll_def lepoll_def eqpoll_def bij_def, clarify) -apply (blast intro!: inj_not_surj_succ) -done - -lemma lesspoll_succ_iff: "m:nat ==> A \ succ(m) \ A \ m" +lemma lesspoll_succ_iff: "m \ nat ==> A \ succ(m) \ A \ m" by (blast intro!: lepoll_imp_lesspoll_succ lesspoll_succ_imp_lepoll) -lemma lepoll_succ_disj: "[| A \ succ(m); m:nat |] ==> A \ m | A \ succ(m)" +lemma lepoll_succ_disj: "[| A \ succ(m); m \ nat |] ==> A \ m | A \ succ(m)" apply (rule disjCI) apply (rule lesspoll_succ_imp_lepoll) prefer 2 apply assumption @@ -618,32 +631,51 @@ subsection{*The first infinite cardinal: Omega, or nat *} (*This implies Kunen's Lemma 10.6*) -lemma lt_not_lepoll: "[| n ~ i \ n" -apply (rule notI) -apply (rule succ_lepoll_natE [of n]) -apply (rule lepoll_trans [of _ i]) -apply (erule ltE) -apply (rule Ord_succ_subsetI [THEN subset_imp_lepoll], assumption+) -done +lemma lt_not_lepoll: + assumes n: "n nat" shows "~ i \ n" +proof - + { assume i: "i \ n" + have "succ(n) \ i" using n + by (elim ltE, blast intro: Ord_succ_subsetI [THEN subset_imp_lepoll]) + also have "... \ n" by (rule i) + finally have "succ(n) \ n" . + hence False by (rule succ_lepoll_natE) (rule n) } + thus ?thesis by auto +qed -lemma Ord_nat_eqpoll_iff: "[| Ord(i); n:nat |] ==> i \ n \ i=n" -apply (rule iffI) - prefer 2 apply (simp add: eqpoll_refl) -apply (rule Ord_linear_lt [of i n]) -apply (simp_all add: nat_into_Ord) -apply (erule lt_nat_in_nat [THEN nat_eqpoll_iff, THEN iffD1], assumption+) -apply (rule lt_not_lepoll [THEN notE], assumption+) -apply (erule eqpoll_imp_lepoll) -done +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" + hence "i \ nat" by (rule lt_nat_in_nat) (rule n) + thus ?thesis by (simp add: nat_eqpoll_iff n) +next + assume "i = n" + thus ?thesis by (simp add: eqpoll_refl) +next + assume "n < i" + 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 nat" + hence "~ nat \ i" + by (simp add: lt_def lt_not_lepoll) + hence False using i + by (simp add: eqpoll_iff) + } + hence "(\ i. i \ nat) = nat" by (blast intro: Least_equality eqpoll_refl) + thus ?thesis + by (auto simp add: Card_def cardinal_def) +qed (*Allows showing that |i| is a limit cardinal*) lemma nat_le_cardinal: "nat \ i ==> nat \ |i|" @@ -736,31 +768,35 @@ (*New proofs using cons_lepoll_cons. Could generalise from succ to cons.*) -(*If A has at most n+1 elements and a:A then A-{a} has at most n.*) +text{*If @{term A} has at most @{term"n+1"} elements and @{term"a \ A"} + then @{term"A-{a}"} has at most @{term n}.*} lemma Diff_sing_lepoll: - "[| a:A; A \ succ(n) |] ==> A - {a} \ n" + "[| a \ A; A \ succ(n) |] ==> A - {a} \ n" apply (unfold succ_def) apply (rule cons_lepoll_consD) apply (rule_tac [3] mem_not_refl) apply (erule cons_Diff [THEN ssubst], safe) done -(*If A has at least n+1 elements then A-{a} has at least n.*) +text{*If @{term A} has at least @{term"n+1"} elements then @{term"A-{a}"} has at least @{term n}.*} lemma lepoll_Diff_sing: - "[| succ(n) \ A |] ==> n \ A - {a}" -apply (unfold succ_def) -apply (rule cons_lepoll_consD) -apply (rule_tac [2] mem_not_refl) -prefer 2 apply blast -apply (blast intro: subset_imp_lepoll [THEN [2] lepoll_trans]) -done + assumes A: "succ(n) \ A" shows "n \ A - {a}" +proof - + have "cons(n,n) \ A" using A + by (unfold succ_def) + also have "... \ cons(a, A-{a})" + by (blast intro: subset_imp_lepoll) + finally have "cons(n,n) \ cons(a, A-{a})" . + thus ?thesis + by (blast intro: cons_lepoll_consD mem_irrefl) +qed -lemma Diff_sing_eqpoll: "[| a:A; A \ succ(n) |] ==> A - {a} \ n" +lemma Diff_sing_eqpoll: "[| a \ A; A \ succ(n) |] ==> A - {a} \ n" by (blast intro!: eqpollI elim!: eqpollE intro: Diff_sing_lepoll lepoll_Diff_sing) -lemma lepoll_1_is_sing: "[| A \ 1; a:A |] ==> A = {a}" +lemma lepoll_1_is_sing: "[| A \ 1; a \ A |] ==> A = {a}" apply (frule Diff_sing_lepoll, assumption) apply (drule lepoll_0_is_0) apply (blast elim: equalityE) @@ -768,8 +804,8 @@ lemma Un_lepoll_sum: "A \ B \ A+B" apply (unfold lepoll_def) -apply (rule_tac x = "\x\A \ B. if x:A then Inl (x) else Inr (x) " in exI) -apply (rule_tac d = "%z. snd (z) " in lam_injective) +apply (rule_tac x = "\x\A \ B. if x\A then Inl (x) else Inr (x)" in exI) +apply (rule_tac d = "%z. snd (z)" in lam_injective) apply force apply (simp add: Inl_def Inr_def) done @@ -782,8 +818,8 @@ (*Krzysztof Grabczewski*) lemma disj_Un_eqpoll_sum: "A \ B = 0 ==> A \ B \ A + B" apply (unfold eqpoll_def) -apply (rule_tac x = "\a\A \ B. if a:A then Inl (a) else Inr (a) " in exI) -apply (rule_tac d = "%z. case (%x. x, %x. x, z) " in lam_bijective) +apply (rule_tac x = "\a\A \ B. if a \ A then Inl (a) else Inr (a)" in exI) +apply (rule_tac d = "%z. case (%x. x, %x. x, z)" in lam_bijective) apply auto done @@ -795,7 +831,7 @@ apply (blast intro!: eqpoll_refl nat_0I) done -lemma lepoll_nat_imp_Finite: "[| A \ n; n:nat |] ==> Finite(A)" +lemma lepoll_nat_imp_Finite: "[| A \ n; n \ nat |] ==> Finite(A)" apply (unfold Finite_def) apply (erule rev_mp) apply (erule nat_induct) @@ -811,12 +847,15 @@ done lemma lepoll_Finite: - "[| Y \ X; Finite(X) |] ==> Finite(Y)" -apply (unfold Finite_def) -apply (blast elim!: eqpollE - intro: lepoll_trans [THEN lepoll_nat_imp_Finite - [unfolded Finite_def]]) -done + assumes Y: "Y \ X" and X: "Finite(X)" shows "Finite(Y)" +proof - + obtain n where n: "n \ nat" "X \ n" using X + by (auto simp add: Finite_def) + have "Y \ X" by (rule Y) + also have "... \ n" by (rule n) + finally have "Y \ n" . + thus ?thesis using n by (simp add: lepoll_nat_imp_Finite) +qed lemmas subset_Finite = subset_imp_lepoll [THEN lepoll_Finite] @@ -947,7 +986,7 @@ (*Sidi Ehmety. The contrapositive says ~Finite(A) ==> ~Finite(A-{a}) *) lemma Diff_sing_Finite: "Finite(A - {a}) ==> Finite(A)" apply (unfold Finite_def) -apply (case_tac "a:A") +apply (case_tac "a \ A") apply (subgoal_tac [2] "A-{a}=A", auto) apply (rule_tac x = "succ (n) " in bexI) apply (subgoal_tac "cons (a, A - {a}) = A & cons (n, n) = succ (n) ") @@ -1010,7 +1049,7 @@ (*Krzysztof Grabczewski's proof that the converse of a finite, well-ordered set is well-ordered. Proofs simplified by lcp. *) -lemma nat_wf_on_converse_Memrel: "n:nat ==> wf[n](converse(Memrel(n)))" +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) @@ -1023,7 +1062,7 @@ apply (drule_tac x = Z in spec, blast) done -lemma nat_well_ord_converse_Memrel: "n:nat ==> well_ord(n,converse(Memrel(n)))" +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) @@ -1040,13 +1079,16 @@ done lemma ordertype_eq_n: - "[| well_ord(A,r); A \ n; n:nat |] ==> ordertype(A,r)=n" -apply (rule Ord_ordertype [THEN Ord_nat_eqpoll_iff, THEN iffD1], assumption+) -apply (rule eqpoll_trans) - prefer 2 apply assumption -apply (unfold eqpoll_def) -apply (blast intro!: ordermap_bij [THEN bij_converse_bij]) -done + assumes r: "well_ord(A,r)" and A: "A \ n" and n: "n \ nat" + shows "ordertype(A,r) = n" +proof - + have "ordertype(A,r) \ A" + by (blast intro: bij_imp_eqpoll bij_converse_bij ordermap_bij r) + also have "... \ n" by (rule A) + finally have "ordertype(A,r) \ n" . + thus ?thesis + by (simp add: Ord_nat_eqpoll_iff Ord_ordertype n r) +qed lemma Finite_well_ord_converse: "[| Finite(A); well_ord(A,r) |] ==> well_ord(A,converse(r))" @@ -1055,18 +1097,24 @@ apply (blast dest: ordertype_eq_n intro!: nat_well_ord_converse_Memrel) done -lemma nat_into_Finite: "n:nat ==> Finite(n)" +lemma nat_into_Finite: "n \ nat ==> Finite(n)" apply (unfold Finite_def) apply (fast intro!: eqpoll_refl) done -lemma nat_not_Finite: "~Finite(nat)" -apply (unfold Finite_def, clarify) -apply (drule eqpoll_imp_lepoll [THEN lepoll_cardinal_le], simp) -apply (insert Card_nat) -apply (simp add: Card_def) -apply (drule le_imp_subset) -apply (blast elim: mem_irrefl) -done +lemma nat_not_Finite: "~ Finite(nat)" +proof - + { fix n + assume n: "n \ nat" "nat \ n" + have "n \ nat" by (rule n) + also have "... = n" using n + by (simp add: Ord_nat_eqpoll_iff Ord_nat) + finally have "n \ n" . + hence False + by (blast elim: mem_irrefl) + } + thus ?thesis + by (auto simp add: Finite_def) +qed end