src/ZF/Constructible/Wellorderings.thy
 changeset 60770 240563fbf41d parent 58871 c399ae4b836f child 61798 27f3c10b0b50
1.1 --- a/src/ZF/Constructible/Wellorderings.thy	Thu Jul 23 14:20:51 2015 +0200
1.2 +++ b/src/ZF/Constructible/Wellorderings.thy	Thu Jul 23 14:25:05 2015 +0200
1.3 @@ -2,18 +2,18 @@
1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.5  *)
1.7 -section {*Relativized Wellorderings*}
1.8 +section \<open>Relativized Wellorderings\<close>
1.10  theory Wellorderings imports Relative begin
1.12 -text{*We define functions analogous to @{term ordermap} @{term ordertype}
1.13 +text\<open>We define functions analogous to @{term ordermap} @{term ordertype}
1.14        but without using recursion.  Instead, there is a direct appeal
1.15        to Replacement.  This will be the basis for a version relativized
1.16        to some class @{text M}.  The main result is Theorem I 7.6 in Kunen,
1.17 -      page 17.*}
1.18 +      page 17.\<close>
1.21 -subsection{*Wellorderings*}
1.22 +subsection\<open>Wellorderings\<close>
1.24  definition
1.25    irreflexive :: "[i=>o,i,i]=>o" where
1.26 @@ -32,23 +32,23 @@
1.28  definition
1.29    wellfounded :: "[i=>o,i]=>o" where
1.30 -    --{*EVERY non-empty set has an @{text r}-minimal element*}
1.31 +    --\<open>EVERY non-empty set has an @{text r}-minimal element\<close>
1.32      "wellfounded(M,r) ==
1.33          \<forall>x[M]. x\<noteq>0 \<longrightarrow> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & <z,y> \<in> r))"
1.34  definition
1.35    wellfounded_on :: "[i=>o,i,i]=>o" where
1.36 -    --{*every non-empty SUBSET OF @{text A} has an @{text r}-minimal element*}
1.37 +    --\<open>every non-empty SUBSET OF @{text A} has an @{text r}-minimal element\<close>
1.38      "wellfounded_on(M,A,r) ==
1.39          \<forall>x[M]. x\<noteq>0 \<longrightarrow> x\<subseteq>A \<longrightarrow> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & <z,y> \<in> r))"
1.41  definition
1.42    wellordered :: "[i=>o,i,i]=>o" where
1.43 -    --{*linear and wellfounded on @{text A}*}
1.44 +    --\<open>linear and wellfounded on @{text A}\<close>
1.45      "wellordered(M,A,r) ==
1.46          transitive_rel(M,A,r) & linear_rel(M,A,r) & wellfounded_on(M,A,r)"
1.49 -subsubsection {*Trivial absoluteness proofs*}
1.50 +subsubsection \<open>Trivial absoluteness proofs\<close>
1.52  lemma (in M_basic) irreflexive_abs [simp]:
1.53       "M(A) ==> irreflexive(M,A,r) \<longleftrightarrow> irrefl(A,r)"
1.54 @@ -83,7 +83,7 @@
1.55  by (simp add: wellfounded_on_def, blast)
1.58 -subsubsection {*Well-founded relations*}
1.59 +subsubsection \<open>Well-founded relations\<close>
1.61  lemma  (in M_basic) wellfounded_on_iff_wellfounded:
1.62       "wellfounded_on(M,A,r) \<longleftrightarrow> wellfounded(M, r \<inter> A*A)"
1.63 @@ -126,7 +126,7 @@
1.64  done
1.67 -subsubsection {*Kunen's lemma IV 3.14, page 123*}
1.68 +subsubsection \<open>Kunen's lemma IV 3.14, page 123\<close>
1.70  lemma (in M_basic) linear_imp_relativized:
1.71       "linear(A,r) ==> linear_rel(M,A,r)"
1.72 @@ -153,11 +153,11 @@
1.73  by (simp add: wellordered_def well_ord_def tot_ord_def part_ord_def
1.74         linear_imp_relativized trans_on_imp_relativized wf_on_imp_relativized)
1.76 -text{*The property being well founded (and hence of being well ordered) is not absolute:
1.77 +text\<open>The property being well founded (and hence of being well ordered) is not absolute:
1.78  the set that doesn't contain a minimal element may not exist in the class M.
1.79 -However, every set that is well founded in a transitive model M is well founded (page 124).*}
1.80 +However, every set that is well founded in a transitive model M is well founded (page 124).\<close>
1.82 -subsection{* Relativized versions of order-isomorphisms and order types *}
1.83 +subsection\<open>Relativized versions of order-isomorphisms and order types\<close>
1.85  lemma (in M_basic) order_isomorphism_abs [simp]:
1.86       "[| M(A); M(B); M(f) |]
1.87 @@ -203,9 +203,9 @@
1.88  done
1.91 -subsection {* Main results of Kunen, Chapter 1 section 6 *}
1.92 +subsection \<open>Main results of Kunen, Chapter 1 section 6\<close>
1.94 -text{*Subset properties-- proved outside the locale*}
1.95 +text\<open>Subset properties-- proved outside the locale\<close>
1.97  lemma linear_rel_subset:
1.98      "[| linear_rel(M,A,r);  B<=A |] ==> linear_rel(M,B,r)"