src/ZF/OrderArith.thy
changeset 24893 b8ef7afe3a6b
parent 22710 f44439cdce77
child 35762 af3ff2ba4c54
     1.1 --- a/src/ZF/OrderArith.thy	Sun Oct 07 15:49:25 2007 +0200
     1.2 +++ b/src/ZF/OrderArith.thy	Sun Oct 07 21:19:31 2007 +0200
     1.3 @@ -8,28 +8,31 @@
     1.4  header{*Combining Orderings: Foundations of Ordinal Arithmetic*}
     1.5  
     1.6  theory OrderArith imports Order Sum Ordinal begin
     1.7 -constdefs
     1.8  
     1.9 +definition
    1.10    (*disjoint sum of two relations; underlies ordinal addition*)
    1.11 -  radd    :: "[i,i,i,i]=>i"
    1.12 +  radd    :: "[i,i,i,i]=>i"  where
    1.13      "radd(A,r,B,s) == 
    1.14                  {z: (A+B) * (A+B).  
    1.15                      (EX x y. z = <Inl(x), Inr(y)>)   |   
    1.16                      (EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r)   |      
    1.17                      (EX y' y. z = <Inr(y'), Inr(y)> & <y',y>:s)}"
    1.18  
    1.19 +definition
    1.20    (*lexicographic product of two relations; underlies ordinal multiplication*)
    1.21 -  rmult   :: "[i,i,i,i]=>i"
    1.22 +  rmult   :: "[i,i,i,i]=>i"  where
    1.23      "rmult(A,r,B,s) == 
    1.24                  {z: (A*B) * (A*B).  
    1.25                      EX x' y' x y. z = <<x',y'>, <x,y>> &         
    1.26                         (<x',x>: r | (x'=x & <y',y>: s))}"
    1.27  
    1.28 +definition
    1.29    (*inverse image of a relation*)
    1.30 -  rvimage :: "[i,i,i]=>i"
    1.31 +  rvimage :: "[i,i,i]=>i"  where
    1.32      "rvimage(A,f,r) == {z: A*A. EX x y. z = <x,y> & <f`x,f`y>: r}"
    1.33  
    1.34 -  measure :: "[i, i\<Rightarrow>i] \<Rightarrow> i"
    1.35 +definition
    1.36 +  measure :: "[i, i\<Rightarrow>i] \<Rightarrow> i"  where
    1.37      "measure(A,f) == {<x,y>: A*A. f(x) < f(y)}"
    1.38  
    1.39  
    1.40 @@ -406,12 +409,12 @@
    1.41  by (blast intro: wf_rvimage wf_Memrel)
    1.42  
    1.43  
    1.44 -constdefs
    1.45 -  wfrank :: "[i,i]=>i"
    1.46 +definition
    1.47 +  wfrank :: "[i,i]=>i"  where
    1.48      "wfrank(r,a) == wfrec(r, a, %x f. \<Union>y \<in> r-``{x}. succ(f`y))"
    1.49  
    1.50 -constdefs
    1.51 -  wftype :: "i=>i"
    1.52 +definition
    1.53 +  wftype :: "i=>i"  where
    1.54      "wftype(r) == \<Union>y \<in> range(r). succ(wfrank(r,y))"
    1.55  
    1.56  lemma wfrank: "wf(r) ==> wfrank(r,a) = (\<Union>y \<in> r-``{a}. succ(wfrank(r,y)))"
    1.57 @@ -564,60 +567,4 @@
    1.58  apply (rule fun_extension, auto)
    1.59  by blast
    1.60  
    1.61 -
    1.62 -ML {*
    1.63 -val measure_def = thm "measure_def";
    1.64 -val radd_Inl_Inr_iff = thm "radd_Inl_Inr_iff";
    1.65 -val radd_Inl_iff = thm "radd_Inl_iff";
    1.66 -val radd_Inr_iff = thm "radd_Inr_iff";
    1.67 -val radd_Inr_Inl_iff = thm "radd_Inr_Inl_iff";
    1.68 -val raddE = thm "raddE";
    1.69 -val radd_type = thm "radd_type";
    1.70 -val field_radd = thm "field_radd";
    1.71 -val linear_radd = thm "linear_radd";
    1.72 -val wf_on_radd = thm "wf_on_radd";
    1.73 -val wf_radd = thm "wf_radd";
    1.74 -val well_ord_radd = thm "well_ord_radd";
    1.75 -val sum_bij = thm "sum_bij";
    1.76 -val sum_ord_iso_cong = thm "sum_ord_iso_cong";
    1.77 -val sum_disjoint_bij = thm "sum_disjoint_bij";
    1.78 -val sum_assoc_bij = thm "sum_assoc_bij";
    1.79 -val sum_assoc_ord_iso = thm "sum_assoc_ord_iso";
    1.80 -val rmult_iff = thm "rmult_iff";
    1.81 -val rmultE = thm "rmultE";
    1.82 -val rmult_type = thm "rmult_type";
    1.83 -val field_rmult = thm "field_rmult";
    1.84 -val linear_rmult = thm "linear_rmult";
    1.85 -val wf_on_rmult = thm "wf_on_rmult";
    1.86 -val wf_rmult = thm "wf_rmult";
    1.87 -val well_ord_rmult = thm "well_ord_rmult";
    1.88 -val prod_bij = thm "prod_bij";
    1.89 -val prod_ord_iso_cong = thm "prod_ord_iso_cong";
    1.90 -val singleton_prod_bij = thm "singleton_prod_bij";
    1.91 -val singleton_prod_ord_iso = thm "singleton_prod_ord_iso";
    1.92 -val prod_sum_singleton_bij = thm "prod_sum_singleton_bij";
    1.93 -val prod_sum_singleton_ord_iso = thm "prod_sum_singleton_ord_iso";
    1.94 -val sum_prod_distrib_bij = thm "sum_prod_distrib_bij";
    1.95 -val sum_prod_distrib_ord_iso = thm "sum_prod_distrib_ord_iso";
    1.96 -val prod_assoc_bij = thm "prod_assoc_bij";
    1.97 -val prod_assoc_ord_iso = thm "prod_assoc_ord_iso";
    1.98 -val rvimage_iff = thm "rvimage_iff";
    1.99 -val rvimage_type = thm "rvimage_type";
   1.100 -val field_rvimage = thm "field_rvimage";
   1.101 -val rvimage_converse = thm "rvimage_converse";
   1.102 -val irrefl_rvimage = thm "irrefl_rvimage";
   1.103 -val trans_on_rvimage = thm "trans_on_rvimage";
   1.104 -val part_ord_rvimage = thm "part_ord_rvimage";
   1.105 -val linear_rvimage = thm "linear_rvimage";
   1.106 -val tot_ord_rvimage = thm "tot_ord_rvimage";
   1.107 -val wf_rvimage = thm "wf_rvimage";
   1.108 -val wf_on_rvimage = thm "wf_on_rvimage";
   1.109 -val well_ord_rvimage = thm "well_ord_rvimage";
   1.110 -val ord_iso_rvimage = thm "ord_iso_rvimage";
   1.111 -val ord_iso_rvimage_eq = thm "ord_iso_rvimage_eq";
   1.112 -val measure_eq_rvimage_Memrel = thm "measure_eq_rvimage_Memrel";
   1.113 -val wf_measure = thm "wf_measure";
   1.114 -val measure_iff = thm "measure_iff";
   1.115 -*}
   1.116 -
   1.117  end