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.24  lemma radd_Inl_Inr_iff [iff]: 
    1.25      "<Inl(a), Inr(b)> : radd(A,r,B,s)  <->  a:A & b:B"
    1.26 -apply (unfold radd_def, blast)
    1.27 -done
    1.28 +by (unfold radd_def, blast)
    1.29  
    1.30  lemma radd_Inl_iff [iff]: 
    1.31      "<Inl(a'), Inl(a)> : radd(A,r,B,s)  <->  a':A & a:A & <a',a>:r"
    1.32 -apply (unfold radd_def, blast)
    1.33 -done
    1.34 +by (unfold radd_def, blast)
    1.35  
    1.36  lemma radd_Inr_iff [iff]: 
    1.37      "<Inr(b'), Inr(b)> : radd(A,r,B,s) <->  b':B & b:B & <b',b>:s"
    1.38 -apply (unfold radd_def, blast)
    1.39 -done
    1.40 +by (unfold radd_def, blast)
    1.41  
    1.42  lemma radd_Inr_Inl_iff [iff]: 
    1.43      "<Inr(b), Inl(a)> : radd(A,r,B,s) <->  False"
    1.44 -apply (unfold radd_def, blast)
    1.45 -done
    1.46 +by (unfold radd_def, blast)
    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.54 -apply (unfold radd_def, blast) 
    1.55 -done
    1.56 +by (unfold radd_def, blast) 
    1.57  
    1.58  (** Type checking **)
    1.59  
    1.60 @@ -80,8 +76,7 @@
    1.61  
    1.62  lemma linear_radd: 
    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.82        : ord_iso((A+B)+C, radd(A+B, radd(A,r,B,s), C, t),     
    1.83                  A+(B+C), radd(A, r, B+C, radd(B,s,C,t)))"
    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";