src/ZF/OrderArith.thy
 changeset 13356 c9cfe1638bf2 parent 13269 3ba9be497c33 child 13512 80edb859fd24
```     1.1 --- a/src/ZF/OrderArith.thy	Sun Jul 14 15:11:21 2002 +0200
1.2 +++ b/src/ZF/OrderArith.thy	Sun Jul 14 15:14:43 2002 +0200
1.3 @@ -3,9 +3,10 @@
1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.5      Copyright   1994  University of Cambridge
1.6
1.7 -Towards ordinal arithmetic.  Also useful with wfrec.
1.8  *)
1.9
1.10 +header{*Combining Orderings: Foundations of Ordinal Arithmetic*}
1.11 +
1.12  theory OrderArith = Order + Sum + Ordinal:
1.13  constdefs
1.14
1.15 @@ -32,29 +33,25 @@
1.16      "measure(A,f) == {<x,y>: A*A. f(x) < f(y)}"
1.17
1.18
1.19 -(**** Addition of relations -- disjoint sum ****)
1.20 +subsection{*Addition of Relations -- Disjoint Sum*}
1.21
1.22  (** Rewrite rules.  Can be used to obtain introduction rules **)
1.23
1.25      "<Inl(a), Inr(b)> : radd(A,r,B,s)  <->  a:A & b:B"
1.27 -done
1.29
1.31      "<Inl(a'), Inl(a)> : radd(A,r,B,s)  <->  a':A & a:A & <a',a>:r"
1.33 -done
1.35
1.37      "<Inr(b'), Inr(b)> : radd(A,r,B,s) <->  b':B & b:B & <b',b>:s"
1.39 -done
1.41
1.43      "<Inr(b), Inl(a)> : radd(A,r,B,s) <->  False"
1.45 -done
1.47
1.48  (** Elimination Rule **)
1.49
1.50 @@ -64,8 +61,7 @@
1.51          !!x' x. [| p'=Inl(x'); p=Inl(x); <x',x>: r; x':A; x:A |] ==> Q;
1.52          !!y' y. [| p'=Inr(y'); p=Inr(y); <y',y>: s; y':B; y:B |] ==> Q
1.53       |] ==> Q"
1.55 -done
1.57
1.58  (** Type checking **)
1.59
1.60 @@ -80,8 +76,7 @@
1.61
1.63      "[| linear(A,r);  linear(B,s) |] ==> linear(A+B,radd(A,r,B,s))"
1.64 -apply (unfold linear_def, blast)
1.65 -done
1.66 +by (unfold linear_def, blast)
1.67
1.68
1.69  (** Well-foundedness **)
1.70 @@ -119,7 +114,8 @@
1.71  lemma sum_bij:
1.72       "[| f: bij(A,C);  g: bij(B,D) |]
1.73        ==> (lam z:A+B. case(%x. Inl(f`x), %y. Inr(g`y), z)) : bij(A+B, C+D)"
1.74 -apply (rule_tac d = "case (%x. Inl (converse (f) `x), %y. Inr (converse (g) `y))" in lam_bijective)
1.75 +apply (rule_tac d = "case (%x. Inl (converse(f)`x), %y. Inr(converse(g)`y))"
1.76 +       in lam_bijective)
1.77  apply (typecheck add: bij_is_inj inj_is_fun)
1.78  apply (auto simp add: left_inverse_bij right_inverse_bij)
1.79  done
1.80 @@ -156,11 +152,10 @@
1.81       "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z))
1.84 -apply (rule sum_assoc_bij [THEN ord_isoI], auto)
1.85 -done
1.86 +by (rule sum_assoc_bij [THEN ord_isoI], auto)
1.87
1.88
1.89 -(**** Multiplication of relations -- lexicographic product ****)
1.90 +subsection{*Multiplication of Relations -- Lexicographic Product*}
1.91
1.92  (** Rewrite rule.  Can be used to obtain introduction rules **)
1.93
1.94 @@ -169,23 +164,19 @@
1.95              (<a',a>: r  & a':A & a:A & b': B & b: B) |
1.96              (<b',b>: s  & a'=a & a:A & b': B & b: B)"
1.97
1.98 -apply (unfold rmult_def, blast)
1.99 -done
1.100 +by (unfold rmult_def, blast)
1.101
1.102  lemma rmultE:
1.103      "[| <<a',b'>, <a,b>> : rmult(A,r,B,s);
1.104          [| <a',a>: r;  a':A;  a:A;  b':B;  b:B |] ==> Q;
1.105          [| <b',b>: s;  a:A;  a'=a;  b':B;  b:B |] ==> Q
1.106       |] ==> Q"
1.107 -apply blast
1.108 -done
1.109 +by blast
1.110
1.111  (** Type checking **)
1.112
1.113  lemma rmult_type: "rmult(A,r,B,s) <= (A*B) * (A*B)"
1.114 -apply (unfold rmult_def)
1.115 -apply (rule Collect_subset)
1.116 -done
1.117 +by (unfold rmult_def, rule Collect_subset)
1.118
1.119  lemmas field_rmult = rmult_type [THEN field_rel_subset]
1.120
1.121 @@ -193,8 +184,7 @@
1.122
1.123  lemma linear_rmult:
1.124      "[| linear(A,r);  linear(B,s) |] ==> linear(A*B,rmult(A,r,B,s))"
1.125 -apply (simp add: linear_def, blast)
1.126 -done
1.127 +by (simp add: linear_def, blast)
1.128
1.129  (** Well-foundedness **)
1.130
1.131 @@ -289,33 +279,28 @@
1.132  lemma sum_prod_distrib_bij:
1.133       "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x))
1.134        : bij((A+B)*C, (A*C)+(B*C))"
1.135 -apply (rule_tac d = "case (%<x,y>.<Inl (x),y>, %<x,y>.<Inr (x),y>) "
1.136 -       in lam_bijective)
1.137 -apply auto
1.138 -done
1.139 +by (rule_tac d = "case (%<x,y>.<Inl (x),y>, %<x,y>.<Inr (x),y>) "
1.140 +    in lam_bijective, auto)
1.141
1.142  lemma sum_prod_distrib_ord_iso:
1.143   "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x))
1.144    : ord_iso((A+B)*C, rmult(A+B, radd(A,r,B,s), C, t),
1.145              (A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))"
1.146 -apply (rule sum_prod_distrib_bij [THEN ord_isoI], auto)
1.147 -done
1.148 +by (rule sum_prod_distrib_bij [THEN ord_isoI], auto)
1.149
1.150  (** Associativity **)
1.151
1.152  lemma prod_assoc_bij:
1.153       "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) : bij((A*B)*C, A*(B*C))"
1.154 -apply (rule_tac d = "%<x, <y,z>>. <<x,y>, z>" in lam_bijective, auto)
1.155 -done
1.156 +by (rule_tac d = "%<x, <y,z>>. <<x,y>, z>" in lam_bijective, auto)
1.157
1.158  lemma prod_assoc_ord_iso:
1.159   "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>)
1.160    : ord_iso((A*B)*C, rmult(A*B, rmult(A,r,B,s), C, t),
1.161              A*(B*C), rmult(A, r, B*C, rmult(B,s,C,t)))"
1.162 -apply (rule prod_assoc_bij [THEN ord_isoI], auto)
1.163 -done
1.164 +by (rule prod_assoc_bij [THEN ord_isoI], auto)
1.165
1.166 -(**** Inverse image of a relation ****)
1.167 +subsection{*Inverse Image of a Relation*}
1.168
1.169  (** Rewrite rule **)
1.170
1.171 @@ -325,8 +310,7 @@
1.172  (** Type checking **)
1.173
1.174  lemma rvimage_type: "rvimage(A,f,r) <= A*A"
1.175 -apply (unfold rvimage_def)
1.176 -apply (rule Collect_subset)
1.177 +apply (unfold rvimage_def, rule Collect_subset)
1.178  done
1.179
1.180  lemmas field_rvimage = rvimage_type [THEN field_rel_subset]
1.181 @@ -410,8 +394,7 @@
1.182
1.183  lemma ord_iso_rvimage_eq:
1.184      "f: ord_iso(A,r, B,s) ==> rvimage(A,f,s) = r Int A*A"
1.185 -apply (unfold ord_iso_def rvimage_def, blast)
1.186 -done
1.187 +by (unfold ord_iso_def rvimage_def, blast)
1.188
1.189
1.190  (** The "measure" relation is useful with wfrec **)
1.191 @@ -424,12 +407,10 @@
1.192  done
1.193
1.194  lemma wf_measure [iff]: "wf(measure(A,f))"
1.195 -apply (simp (no_asm) add: measure_eq_rvimage_Memrel wf_Memrel wf_rvimage)
1.196 -done
1.197 +by (simp (no_asm) add: measure_eq_rvimage_Memrel wf_Memrel wf_rvimage)
1.198
1.199  lemma measure_iff [iff]: "<x,y> : measure(A,f) <-> x:A & y:A & f(x)<f(y)"
1.200 -apply (simp (no_asm) add: measure_def)
1.201 -done
1.202 +by (simp (no_asm) add: measure_def)
1.203
1.204  ML {*
1.205  val measure_def = thm "measure_def";
```