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";
```