src/ZF/Order.thy
 changeset 24893 b8ef7afe3a6b parent 16417 9bc16273c2d4 child 27703 cb6c513922e0
```     1.1 --- a/src/ZF/Order.thy	Sun Oct 07 15:49:25 2007 +0200
1.2 +++ b/src/ZF/Order.thy	Sun Oct 07 21:19:31 2007 +0200
1.3 @@ -11,41 +11,48 @@
1.4
1.5  theory Order imports WF Perm begin
1.6
1.7 -constdefs
1.8 -
1.9 -  part_ord :: "[i,i]=>o"          	(*Strict partial ordering*)
1.10 +definition
1.11 +  part_ord :: "[i,i]=>o"          	(*Strict partial ordering*)  where
1.12     "part_ord(A,r) == irrefl(A,r) & trans[A](r)"
1.13
1.14 -  linear   :: "[i,i]=>o"          	(*Strict total ordering*)
1.15 +definition
1.16 +  linear   :: "[i,i]=>o"          	(*Strict total ordering*)  where
1.17     "linear(A,r) == (ALL x:A. ALL y:A. <x,y>:r | x=y | <y,x>:r)"
1.18
1.19 -  tot_ord  :: "[i,i]=>o"          	(*Strict total ordering*)
1.20 +definition
1.21 +  tot_ord  :: "[i,i]=>o"          	(*Strict total ordering*)  where
1.22     "tot_ord(A,r) == part_ord(A,r) & linear(A,r)"
1.23
1.24 -  well_ord :: "[i,i]=>o"          	(*Well-ordering*)
1.25 +definition
1.26 +  well_ord :: "[i,i]=>o"          	(*Well-ordering*)  where
1.27     "well_ord(A,r) == tot_ord(A,r) & wf[A](r)"
1.28
1.29 -  mono_map :: "[i,i,i,i]=>i"      	(*Order-preserving maps*)
1.30 +definition
1.31 +  mono_map :: "[i,i,i,i]=>i"      	(*Order-preserving maps*)  where
1.32     "mono_map(A,r,B,s) ==
1.33  	      {f: A->B. ALL x:A. ALL y:A. <x,y>:r --> <f`x,f`y>:s}"
1.34
1.35 -  ord_iso  :: "[i,i,i,i]=>i"		(*Order isomorphisms*)
1.36 +definition
1.37 +  ord_iso  :: "[i,i,i,i]=>i"		(*Order isomorphisms*)  where
1.38     "ord_iso(A,r,B,s) ==
1.39  	      {f: bij(A,B). ALL x:A. ALL y:A. <x,y>:r <-> <f`x,f`y>:s}"
1.40
1.41 -  pred     :: "[i,i,i]=>i"		(*Set of predecessors*)
1.42 +definition
1.43 +  pred     :: "[i,i,i]=>i"		(*Set of predecessors*)  where
1.44     "pred(A,x,r) == {y:A. <y,x>:r}"
1.45
1.46 -  ord_iso_map :: "[i,i,i,i]=>i"      	(*Construction for linearity theorem*)
1.47 +definition
1.48 +  ord_iso_map :: "[i,i,i,i]=>i"      	(*Construction for linearity theorem*)  where
1.49     "ord_iso_map(A,r,B,s) ==
1.50       \<Union>x\<in>A. \<Union>y\<in>B. \<Union>f \<in> ord_iso(pred(A,x,r), r, pred(B,y,s), s). {<x,y>}"
1.51
1.52 -  first :: "[i, i, i] => o"
1.53 +definition
1.54 +  first :: "[i, i, i] => o"  where
1.55      "first(u, X, R) == u:X & (ALL v:X. v~=u --> <u,v> : R)"
1.56
1.57
1.58 -syntax (xsymbols)
1.59 -    ord_iso :: "[i,i,i,i]=>i"      ("(\<langle>_, _\<rangle> \<cong>/ \<langle>_, _\<rangle>)" 51)
1.60 +notation (xsymbols)
1.61 +  ord_iso  ("(\<langle>_, _\<rangle> \<cong>/ \<langle>_, _\<rangle>)" 51)
1.62
1.63
1.64  subsection{*Immediate Consequences of the Definitions*}
1.65 @@ -157,7 +164,7 @@
1.66  done
1.67
1.68  lemma wf_on_Int_iff: "wf[A](r Int A*A) <-> wf[A](r)"
1.69 -apply (unfold wf_on_def wf_def, fast) (*10 times faster than Blast_tac!*)
1.70 +apply (unfold wf_on_def wf_def, fast) (*10 times faster than blast!*)
1.71  done
1.72
1.73  lemma well_ord_Int_iff: "well_ord(A,r Int A*A) <-> well_ord(A,r)"
1.74 @@ -638,91 +645,4 @@
1.75  apply (erule theI)
1.76  done
1.77
1.78 -ML {*
1.79 -val pred_def = thm "pred_def"
1.80 -val linear_def = thm "linear_def"
1.81 -val part_ord_def = thm "part_ord_def"
1.82 -val tot_ord_def = thm "tot_ord_def"
1.83 -val well_ord_def = thm "well_ord_def"
1.84 -val ord_iso_def = thm "ord_iso_def"
1.85 -val mono_map_def = thm "mono_map_def";
1.86 -
1.87 -val part_ord_Imp_asym = thm "part_ord_Imp_asym";
1.88 -val linearE = thm "linearE";
1.89 -val well_ordI = thm "well_ordI";
1.90 -val well_ord_is_wf = thm "well_ord_is_wf";
1.91 -val well_ord_is_trans_on = thm "well_ord_is_trans_on";
1.92 -val well_ord_is_linear = thm "well_ord_is_linear";
1.93 -val pred_iff = thm "pred_iff";
1.94 -val predI = thm "predI";
1.95 -val predE = thm "predE";
1.96 -val pred_subset_under = thm "pred_subset_under";
1.97 -val pred_subset = thm "pred_subset";
1.98 -val pred_pred_eq = thm "pred_pred_eq";
1.99 -val trans_pred_pred_eq = thm "trans_pred_pred_eq";
1.100 -val part_ord_subset = thm "part_ord_subset";
1.101 -val linear_subset = thm "linear_subset";
1.102 -val tot_ord_subset = thm "tot_ord_subset";
1.103 -val well_ord_subset = thm "well_ord_subset";
1.104 -val irrefl_Int_iff = thm "irrefl_Int_iff";
1.105 -val trans_on_Int_iff = thm "trans_on_Int_iff";
1.106 -val part_ord_Int_iff = thm "part_ord_Int_iff";
1.107 -val linear_Int_iff = thm "linear_Int_iff";
1.108 -val tot_ord_Int_iff = thm "tot_ord_Int_iff";
1.109 -val wf_on_Int_iff = thm "wf_on_Int_iff";
1.110 -val well_ord_Int_iff = thm "well_ord_Int_iff";
1.111 -val irrefl_0 = thm "irrefl_0";
1.112 -val trans_on_0 = thm "trans_on_0";
1.113 -val part_ord_0 = thm "part_ord_0";
1.114 -val linear_0 = thm "linear_0";
1.115 -val tot_ord_0 = thm "tot_ord_0";
1.116 -val wf_on_0 = thm "wf_on_0";
1.117 -val well_ord_0 = thm "well_ord_0";
1.118 -val tot_ord_unit = thm "tot_ord_unit";
1.119 -val well_ord_unit = thm "well_ord_unit";
1.120 -val mono_map_is_fun = thm "mono_map_is_fun";
1.121 -val mono_map_is_inj = thm "mono_map_is_inj";
1.122 -val ord_isoI = thm "ord_isoI";
1.123 -val ord_iso_is_mono_map = thm "ord_iso_is_mono_map";
1.124 -val ord_iso_is_bij = thm "ord_iso_is_bij";
1.125 -val ord_iso_apply = thm "ord_iso_apply";
1.126 -val ord_iso_converse = thm "ord_iso_converse";
1.127 -val ord_iso_refl = thm "ord_iso_refl";
1.128 -val ord_iso_sym = thm "ord_iso_sym";
1.129 -val mono_map_trans = thm "mono_map_trans";
1.130 -val ord_iso_trans = thm "ord_iso_trans";
1.131 -val mono_ord_isoI = thm "mono_ord_isoI";
1.132 -val well_ord_mono_ord_isoI = thm "well_ord_mono_ord_isoI";
1.133 -val part_ord_ord_iso = thm "part_ord_ord_iso";
1.134 -val linear_ord_iso = thm "linear_ord_iso";
1.135 -val wf_on_ord_iso = thm "wf_on_ord_iso";
1.136 -val well_ord_ord_iso = thm "well_ord_ord_iso";
1.137 -val well_ord_iso_predE = thm "well_ord_iso_predE";
1.138 -val well_ord_iso_pred_eq = thm "well_ord_iso_pred_eq";
1.139 -val ord_iso_image_pred = thm "ord_iso_image_pred";
1.140 -val ord_iso_restrict_pred = thm "ord_iso_restrict_pred";
1.141 -val well_ord_iso_preserving = thm "well_ord_iso_preserving";
1.142 -val well_ord_iso_unique = thm "well_ord_iso_unique";
1.143 -val ord_iso_map_subset = thm "ord_iso_map_subset";
1.144 -val domain_ord_iso_map = thm "domain_ord_iso_map";
1.145 -val range_ord_iso_map = thm "range_ord_iso_map";
1.146 -val converse_ord_iso_map = thm "converse_ord_iso_map";
1.147 -val function_ord_iso_map = thm "function_ord_iso_map";
1.148 -val ord_iso_map_fun = thm "ord_iso_map_fun";
1.149 -val ord_iso_map_mono_map = thm "ord_iso_map_mono_map";
1.150 -val ord_iso_map_ord_iso = thm "ord_iso_map_ord_iso";
1.151 -val domain_ord_iso_map_subset = thm "domain_ord_iso_map_subset";
1.152 -val domain_ord_iso_map_cases = thm "domain_ord_iso_map_cases";
1.153 -val range_ord_iso_map_cases = thm "range_ord_iso_map_cases";
1.154 -val well_ord_trichotomy = thm "well_ord_trichotomy";
1.155 -val irrefl_converse = thm "irrefl_converse";
1.156 -val trans_on_converse = thm "trans_on_converse";
1.157 -val part_ord_converse = thm "part_ord_converse";
1.158 -val linear_converse = thm "linear_converse";
1.159 -val tot_ord_converse = thm "tot_ord_converse";
1.160 -val first_is_elem = thm "first_is_elem";
1.161 -val well_ord_imp_ex1_first = thm "well_ord_imp_ex1_first";
1.162 -val the_first_in = thm "the_first_in";
1.163 -*}
1.164 -
1.165  end
```