src/ZF/Order.thy
changeset 60770 240563fbf41d
parent 59788 6f7b6adac439
child 61400 045b4d7a53e2
     1.1 --- a/src/ZF/Order.thy	Thu Jul 23 14:20:51 2015 +0200
     1.2 +++ b/src/ZF/Order.thy	Thu Jul 23 14:25:05 2015 +0200
     1.3 @@ -7,13 +7,13 @@
     1.4  Additional definitions and lemmas for reflexive orders.
     1.5  *)
     1.6  
     1.7 -section{*Partial and Total Orderings: Basic Definitions and Properties*}
     1.8 +section\<open>Partial and Total Orderings: Basic Definitions and Properties\<close>
     1.9  
    1.10  theory Order imports WF Perm begin
    1.11  
    1.12 -text {* We adopt the following convention: @{text ord} is used for
    1.13 +text \<open>We adopt the following convention: @{text ord} is used for
    1.14    strict orders and @{text order} is used for their reflexive
    1.15 -  counterparts. *}
    1.16 +  counterparts.\<close>
    1.17  
    1.18  definition
    1.19    part_ord :: "[i,i]=>o"                (*Strict partial ordering*)  where
    1.20 @@ -71,7 +71,7 @@
    1.21    ord_iso  ("(\<langle>_, _\<rangle> \<cong>/ \<langle>_, _\<rangle>)" 51)
    1.22  
    1.23  
    1.24 -subsection{*Immediate Consequences of the Definitions*}
    1.25 +subsection\<open>Immediate Consequences of the Definitions\<close>
    1.26  
    1.27  lemma part_ord_Imp_asym:
    1.28      "part_ord(A,r) ==> asym(r \<inter> A*A)"
    1.29 @@ -131,7 +131,7 @@
    1.30  by (unfold trans_on_def pred_def, blast)
    1.31  
    1.32  
    1.33 -subsection{*Restricting an Ordering's Domain*}
    1.34 +subsection\<open>Restricting an Ordering's Domain\<close>
    1.35  
    1.36  (** The ordering's properties hold over all subsets of its domain
    1.37      [including initial segments of the form pred(A,x,r) **)
    1.38 @@ -189,13 +189,13 @@
    1.39  done
    1.40  
    1.41  
    1.42 -subsection{*Empty and Unit Domains*}
    1.43 +subsection\<open>Empty and Unit Domains\<close>
    1.44  
    1.45  (*The empty relation is well-founded*)
    1.46  lemma wf_on_any_0: "wf[A](0)"
    1.47  by (simp add: wf_on_def wf_def, fast)
    1.48  
    1.49 -subsubsection{*Relations over the Empty Set*}
    1.50 +subsubsection\<open>Relations over the Empty Set\<close>
    1.51  
    1.52  lemma irrefl_0: "irrefl(0,r)"
    1.53  by (unfold irrefl_def, blast)
    1.54 @@ -225,9 +225,9 @@
    1.55  done
    1.56  
    1.57  
    1.58 -subsubsection{*The Empty Relation Well-Orders the Unit Set*}
    1.59 +subsubsection\<open>The Empty Relation Well-Orders the Unit Set\<close>
    1.60  
    1.61 -text{*by Grabczewski*}
    1.62 +text\<open>by Grabczewski\<close>
    1.63  
    1.64  lemma tot_ord_unit: "tot_ord({a},0)"
    1.65  by (simp add: irrefl_def trans_on_def part_ord_def linear_def tot_ord_def)
    1.66 @@ -238,9 +238,9 @@
    1.67  done
    1.68  
    1.69  
    1.70 -subsection{*Order-Isomorphisms*}
    1.71 +subsection\<open>Order-Isomorphisms\<close>
    1.72  
    1.73 -text{*Suppes calls them "similarities"*}
    1.74 +text\<open>Suppes calls them "similarities"\<close>
    1.75  
    1.76  (** Order-preserving (monotone) maps **)
    1.77  
    1.78 @@ -372,7 +372,7 @@
    1.79  done
    1.80  
    1.81  
    1.82 -subsection{*Main results of Kunen, Chapter 1 section 6*}
    1.83 +subsection\<open>Main results of Kunen, Chapter 1 section 6\<close>
    1.84  
    1.85  (*Inductive argument for Kunen's Lemma 6.1, etc.
    1.86    Simple proof from Halmos, page 72*)
    1.87 @@ -486,7 +486,7 @@
    1.88                      well_ord_is_linear well_ord_ord_iso ord_iso_sym)
    1.89  done
    1.90  
    1.91 -subsection{*Towards Kunen's Theorem 6.3: Linearity of the Similarity Relation*}
    1.92 +subsection\<open>Towards Kunen's Theorem 6.3: Linearity of the Similarity Relation\<close>
    1.93  
    1.94  lemma ord_iso_map_subset: "ord_iso_map(A,r,B,s) \<subseteq> A*B"
    1.95  by (unfold ord_iso_map_def, blast)
    1.96 @@ -594,7 +594,7 @@
    1.97  apply (simp add: domain_ord_iso_map_cases)
    1.98  done
    1.99  
   1.100 -text{*Kunen's Theorem 6.3: Fundamental Theorem for Well-Ordered Sets*}
   1.101 +text\<open>Kunen's Theorem 6.3: Fundamental Theorem for Well-Ordered Sets\<close>
   1.102  theorem well_ord_trichotomy:
   1.103     "[| well_ord(A,r);  well_ord(B,s) |]
   1.104      ==> ord_iso_map(A,r,B,s) \<in> ord_iso(A, r, B, s) |
   1.105 @@ -615,7 +615,7 @@
   1.106  done
   1.107  
   1.108  
   1.109 -subsection{*Miscellaneous Results by Krzysztof Grabczewski*}
   1.110 +subsection\<open>Miscellaneous Results by Krzysztof Grabczewski\<close>
   1.111  
   1.112  (** Properties of converse(r) **)
   1.113  
   1.114 @@ -662,7 +662,7 @@
   1.115  done
   1.116  
   1.117  
   1.118 -subsection {* Lemmas for the Reflexive Orders *}
   1.119 +subsection \<open>Lemmas for the Reflexive Orders\<close>
   1.120  
   1.121  lemma subset_vimage_vimage_iff:
   1.122    "[| Preorder(r); A \<subseteq> field(r); B \<subseteq> field(r) |] ==>