src/HOL/Infinite_Set.thy
 changeset 19537 213ff8b0c60c parent 19457 b6eb4b4546fa child 19656 09be06943252
```--- a/src/HOL/Infinite_Set.thy	Tue May 02 20:42:32 2006 +0200
+++ b/src/HOL/Infinite_Set.thy	Tue May 02 20:42:33 2006 +0200
@@ -24,17 +24,17 @@

lemma infinite_nonempty:
"\<not> (infinite {})"
-by simp
+  by simp

lemma infinite_remove:
"infinite S \<Longrightarrow> infinite (S - {a})"
-by simp
+  by simp

lemma Diff_infinite_finite:
assumes T: "finite T" and S: "infinite S"
shows "infinite (S-T)"
-using T
-proof (induct)
+  using T
+proof induct
from S
show "infinite (S - {})" by auto
next
@@ -49,17 +49,15 @@

lemma Un_infinite:
"infinite S \<Longrightarrow> infinite (S \<union> T)"
-by simp
+  by simp

lemma infinite_super:
assumes T: "S \<subseteq> T" and S: "infinite S"
shows "infinite T"
proof (rule ccontr)
assume "\<not>(infinite T)"
-  with T
-  have "finite S" by (simp add: finite_subset)
-  with S
-  show False by simp
+  with T have "finite S" by (simp add: finite_subset)
+  with S show False by simp
qed

text {*
@@ -356,13 +354,17 @@
INF_def:  "Inf_many P \<equiv> infinite {x. P x}"
MOST_def: "Alm_all P \<equiv> \<not>(INF x. \<not> P x)"

-syntax (xsymbols)
-  "MOST " :: "[idts, bool] \<Rightarrow> bool"       ("(3\<forall>\<^sub>\<infinity>_./ _)" [0,10] 10)
-  "INF "    :: "[idts, bool] \<Rightarrow> bool"     ("(3\<exists>\<^sub>\<infinity>_./ _)" [0,10] 10)
+abbreviation (xsymbols)
+  Inf_many1  (binder "\<exists>\<^sub>\<infinity>" 10)
+  "Inf_many1 == Inf_many"
+  Alm_all1  (binder "\<forall>\<^sub>\<infinity>" 10)
+  "Alm_all1 == Alm_all"

-syntax (HTML output)
-  "MOST " :: "[idts, bool] \<Rightarrow> bool"       ("(3\<forall>\<^sub>\<infinity>_./ _)" [0,10] 10)
-  "INF "    :: "[idts, bool] \<Rightarrow> bool"     ("(3\<exists>\<^sub>\<infinity>_./ _)" [0,10] 10)
+abbreviation (HTML output)
+  Inf_many2  (binder "\<exists>\<^sub>\<infinity>" 10)
+  "Inf_many2 == Inf_many"
+  Alm_all2  (binder "\<forall>\<^sub>\<infinity>" 10)
+  "Alm_all2 == Alm_all"

lemma INF_EX:
"(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"
@@ -421,12 +423,12 @@
"atmost_one S \<equiv> \<forall>x y. x\<in>S \<and> y\<in>S \<longrightarrow> x=y"

lemma atmost_one_empty: "S={} \<Longrightarrow> atmost_one S"