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