src/ZF/Order.thy
changeset 13701 0a9228532106
parent 13615 449a70d88b38
child 16417 9bc16273c2d4
     1.1 --- a/src/ZF/Order.thy	Thu Nov 07 12:35:34 2002 +0100
     1.2 +++ b/src/ZF/Order.thy	Fri Nov 08 10:28:29 2002 +0100
     1.3 @@ -168,7 +168,11 @@
     1.4  
     1.5  subsection{*Empty and Unit Domains*}
     1.6  
     1.7 -(** Relations over the Empty Set **)
     1.8 +(*The empty relation is well-founded*)
     1.9 +lemma wf_on_any_0: "wf[A](0)"
    1.10 +by (simp add: wf_on_def wf_def, fast)
    1.11 +
    1.12 +subsubsection{*Relations over the Empty Set*}
    1.13  
    1.14  lemma irrefl_0: "irrefl(0,r)"
    1.15  by (unfold irrefl_def, blast)
    1.16 @@ -198,17 +202,16 @@
    1.17  done
    1.18  
    1.19  
    1.20 -(** The unit set is well-ordered by the empty relation (Grabczewski) **)
    1.21 +subsubsection{*The Empty Relation Well-Orders the Unit Set*}
    1.22 +
    1.23 +text{*by Grabczewski*}
    1.24  
    1.25  lemma tot_ord_unit: "tot_ord({a},0)"
    1.26  by (simp add: irrefl_def trans_on_def part_ord_def linear_def tot_ord_def)
    1.27  
    1.28 -lemma wf_on_unit: "wf[{a}](0)"
    1.29 -by (simp add: wf_on_def wf_def, fast)
    1.30 -
    1.31  lemma well_ord_unit: "well_ord({a},0)"
    1.32  apply (unfold well_ord_def)
    1.33 -apply (simp add: tot_ord_unit wf_on_unit)
    1.34 +apply (simp add: tot_ord_unit wf_on_any_0)
    1.35  done
    1.36  
    1.37  
    1.38 @@ -676,7 +679,6 @@
    1.39  val wf_on_0 = thm "wf_on_0";
    1.40  val well_ord_0 = thm "well_ord_0";
    1.41  val tot_ord_unit = thm "tot_ord_unit";
    1.42 -val wf_on_unit = thm "wf_on_unit";
    1.43  val well_ord_unit = thm "well_ord_unit";
    1.44  val mono_map_is_fun = thm "mono_map_is_fun";
    1.45  val mono_map_is_inj = thm "mono_map_is_inj";