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.12 +  radd    :: "[i,i,i,i]=>i"  where
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.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
```