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.6  
     1.7 -section {*Relativized Wellorderings*}
     1.8 +section \<open>Relativized Wellorderings\<close>
     1.9  
    1.10  theory Wellorderings imports Relative begin
    1.11  
    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.19  
    1.20  
    1.21 -subsection{*Wellorderings*}
    1.22 +subsection\<open>Wellorderings\<close>
    1.23  
    1.24  definition
    1.25    irreflexive :: "[i=>o,i,i]=>o" where
    1.26 @@ -32,23 +32,23 @@
    1.27  
    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.40  
    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.47  
    1.48  
    1.49 -subsubsection {*Trivial absoluteness proofs*}
    1.50 +subsubsection \<open>Trivial absoluteness proofs\<close>
    1.51  
    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.56  
    1.57  
    1.58 -subsubsection {*Well-founded relations*}
    1.59 +subsubsection \<open>Well-founded relations\<close>
    1.60  
    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.65  
    1.66  
    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.69  
    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.75  
    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.81  
    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.84  
    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.89  
    1.90  
    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.93  
    1.94 -text{*Subset properties-- proved outside the locale*}
    1.95 +text\<open>Subset properties-- proved outside the locale\<close>
    1.96  
    1.97  lemma linear_rel_subset: 
    1.98      "[| linear_rel(M,A,r);  B<=A |] ==> linear_rel(M,B,r)"