--- a/src/ZF/Ordinal.thy Thu Jul 23 14:20:51 2015 +0200
+++ b/src/ZF/Ordinal.thy Thu Jul 23 14:25:05 2015 +0200
@@ -3,7 +3,7 @@
Copyright 1994 University of Cambridge
*)
-section{*Transitive Sets and Ordinals*}
+section\<open>Transitive Sets and Ordinals\<close>
theory Ordinal imports WF Bool equalities begin
@@ -38,9 +38,9 @@
le (infixl "\<le>" 50)
-subsection{*Rules for Transset*}
+subsection\<open>Rules for Transset\<close>
-subsubsection{*Three Neat Characterisations of Transset*}
+subsubsection\<open>Three Neat Characterisations of Transset\<close>
lemma Transset_iff_Pow: "Transset(A) <-> A<=Pow(A)"
by (unfold Transset_def, blast)
@@ -53,7 +53,7 @@
lemma Transset_iff_Union_subset: "Transset(A) <-> \<Union>(A) \<subseteq> A"
by (unfold Transset_def, blast)
-subsubsection{*Consequences of Downwards Closure*}
+subsubsection\<open>Consequences of Downwards Closure\<close>
lemma Transset_doubleton_D:
"[| Transset(C); {a,b}: C |] ==> a\<in>C & b\<in>C"
@@ -73,7 +73,7 @@
"[| Transset(C); A*B \<subseteq> C; a \<in> A |] ==> B \<subseteq> C"
by (blast dest: Transset_Pair_D)
-subsubsection{*Closure Properties*}
+subsubsection\<open>Closure Properties\<close>
lemma Transset_0: "Transset(0)"
by (unfold Transset_def, blast)
@@ -112,7 +112,7 @@
by (rule Transset_Inter_family, auto)
-subsection{*Lemmas for Ordinals*}
+subsection\<open>Lemmas for Ordinals\<close>
lemma OrdI:
"[| Transset(i); !!x. x\<in>i ==> Transset(x) |] ==> Ord(i)"
@@ -149,7 +149,7 @@
by (blast dest: OrdmemD)
-subsection{*The Construction of Ordinals: 0, succ, Union*}
+subsection\<open>The Construction of Ordinals: 0, succ, Union\<close>
lemma Ord_0 [iff,TC]: "Ord(0)"
by (blast intro: OrdI Transset_0)
@@ -172,7 +172,7 @@
apply (blast intro!: Transset_Int)
done
-text{*There is no set of all ordinals, for then it would contain itself*}
+text\<open>There is no set of all ordinals, for then it would contain itself\<close>
lemma ON_class: "~ (\<forall>i. i\<in>X <-> Ord(i))"
proof (rule notI)
assume X: "\<forall>i. i \<in> X \<longleftrightarrow> Ord(i)"
@@ -187,7 +187,7 @@
thus "False" by (rule mem_irrefl)
qed
-subsection{*< is 'less Than' for Ordinals*}
+subsection\<open>< is 'less Than' for Ordinals\<close>
lemma ltI: "[| i\<in>j; Ord(j) |] ==> i<j"
by (unfold lt_def, blast)
@@ -236,7 +236,7 @@
done
-text{* Recall that @{term"i \<le> j"} abbreviates @{term"i<succ(j)"} !! *}
+text\<open>Recall that @{term"i \<le> j"} abbreviates @{term"i<succ(j)"} !!\<close>
lemma le_iff: "i \<le> j <-> i<j | (i=j & Ord(j))"
by (unfold lt_def, blast)
@@ -270,7 +270,7 @@
lemmas le0D = le0_iff [THEN iffD1, dest!]
-subsection{*Natural Deduction Rules for Memrel*}
+subsection\<open>Natural Deduction Rules for Memrel\<close>
(*The lemmas MemrelI/E give better speed than [iff] here*)
lemma Memrel_iff [simp]: "<a,b> \<in> Memrel(A) <-> a\<in>b & a\<in>A & b\<in>A"
@@ -307,12 +307,12 @@
apply (rule foundation [THEN disjE, THEN allI], erule disjI1, blast)
done
-text{*The premise @{term "Ord(i)"} does not suffice.*}
+text\<open>The premise @{term "Ord(i)"} does not suffice.\<close>
lemma trans_Memrel:
"Ord(i) ==> trans(Memrel(i))"
by (unfold Ord_def Transset_def trans_def, blast)
-text{*However, the following premise is strong enough.*}
+text\<open>However, the following premise is strong enough.\<close>
lemma Transset_trans_Memrel:
"\<forall>j\<in>i. Transset(j) ==> trans(Memrel(i))"
by (unfold Transset_def trans_def, blast)
@@ -323,7 +323,7 @@
by (unfold Transset_def, blast)
-subsection{*Transfinite Induction*}
+subsection\<open>Transfinite Induction\<close>
(*Epsilon induction over a transitive set*)
lemma Transset_induct:
@@ -348,17 +348,17 @@
done
-section{*Fundamental properties of the epsilon ordering (< on ordinals)*}
+section\<open>Fundamental properties of the epsilon ordering (< on ordinals)\<close>
-subsubsection{*Proving That < is a Linear Ordering on the Ordinals*}
+subsubsection\<open>Proving That < is a Linear Ordering on the Ordinals\<close>
lemma Ord_linear:
"Ord(i) \<Longrightarrow> Ord(j) \<Longrightarrow> i\<in>j | i=j | j\<in>i"
proof (induct i arbitrary: j rule: trans_induct)
case (step i)
note step_i = step
- show ?case using `Ord(j)`
+ show ?case using \<open>Ord(j)\<close>
proof (induct j rule: trans_induct)
case (step j)
thus ?case using step_i
@@ -366,7 +366,7 @@
qed
qed
-text{*The trichotomy law for ordinals*}
+text\<open>The trichotomy law for ordinals\<close>
lemma Ord_linear_lt:
assumes o: "Ord(i)" "Ord(j)"
obtains (lt) "i<j" | (eq) "i=j" | (gt) "j<i"
@@ -395,7 +395,7 @@
lemma not_lt_imp_le: "[| ~ i<j; Ord(i); Ord(j) |] ==> j \<le> i"
by (rule_tac i = i and j = j in Ord_linear2, auto)
-subsubsection{*Some Rewrite Rules for <, le*}
+subsubsection\<open>Some Rewrite Rules for <, le\<close>
lemma Ord_mem_iff_lt: "Ord(j) ==> i\<in>j <-> i<j"
by (unfold lt_def, blast)
@@ -419,7 +419,7 @@
by (blast intro: Ord_0_lt)
-subsection{*Results about Less-Than or Equals*}
+subsection\<open>Results about Less-Than or Equals\<close>
(** For ordinals, @{term"j\<subseteq>i"} implies @{term"j \<le> i"} (less-than or equals) **)
@@ -446,7 +446,7 @@
lemma all_lt_imp_le: "[| Ord(i); Ord(j); !!x. x<j ==> x<i |] ==> j \<le> i"
by (blast intro: not_lt_imp_le dest: lt_irrefl)
-subsubsection{*Transitivity Laws*}
+subsubsection\<open>Transitivity Laws\<close>
lemma lt_trans1: "[| i \<le> j; j<k |] ==> i<k"
by (blast elim!: leE intro: lt_trans)
@@ -498,7 +498,7 @@
apply (simp add: lt_def)
done
-subsubsection{*Union and Intersection*}
+subsubsection\<open>Union and Intersection\<close>
lemma Un_upper1_le: "[| Ord(i); Ord(j) |] ==> i \<le> i \<union> j"
by (rule Un_upper1 [THEN subset_imp_le], auto)
@@ -560,7 +560,7 @@
by (blast intro: Ord_trans)
-subsection{*Results about Limits*}
+subsection\<open>Results about Limits\<close>
lemma Ord_Union [intro,simp,TC]: "[| !!i. i\<in>A ==> Ord(i) |] ==> Ord(\<Union>(A))"
apply (rule Ord_is_Transset [THEN Transset_Union_family, THEN OrdI])
@@ -633,7 +633,7 @@
by (blast intro: Ord_trans)
-subsection{*Limit Ordinals -- General Properties*}
+subsection\<open>Limit Ordinals -- General Properties\<close>
lemma Limit_Union_eq: "Limit(i) ==> \<Union>(i) = i"
apply (unfold Limit_def)
@@ -701,7 +701,7 @@
by (blast elim!: leE)
-subsubsection{*Traditional 3-Way Case Analysis on Ordinals*}
+subsubsection\<open>Traditional 3-Way Case Analysis on Ordinals\<close>
lemma Ord_cases_disj: "Ord(i) ==> i=0 | (\<exists>j. Ord(j) & i=succ(j)) | Limit(i)"
by (blast intro!: non_succ_LimitI Ord_0_lt)
@@ -723,8 +723,8 @@
lemmas trans_induct3 = trans_induct3_raw [rule_format, case_names 0 succ limit, consumes 1]
-text{*A set of ordinals is either empty, contains its own union, or its
-union is a limit ordinal.*}
+text\<open>A set of ordinals is either empty, contains its own union, or its
+union is a limit ordinal.\<close>
lemma Union_le: "[| !!x. x\<in>I ==> x\<le>j; Ord(j) |] ==> \<Union>(I) \<le> j"
by (auto simp add: le_subset_iff Union_least)
@@ -757,7 +757,7 @@
assume "Limit(\<Union>I)" thus ?thesis by auto
qed
-text{*If the union of a set of ordinals is a successor, then it is an element of that set.*}
+text\<open>If the union of a set of ordinals is a successor, then it is an element of that set.\<close>
lemma Ord_Union_eq_succD: "[|\<forall>x\<in>X. Ord(x); \<Union>X = succ(j)|] ==> succ(j) \<in> X"
by (drule Ord_set_cases, auto)