new lemmas
authorpaulson
Tue Jul 16 16:28:26 2002 +0200 (2002-07-16)
changeset 133615005d34425bb
parent 13360 ece4b151f963
child 13362 cd7f9ea58338
new lemmas
src/ZF/Arith.thy
     1.1 --- a/src/ZF/Arith.thy	Tue Jul 16 09:36:11 2002 +0200
     1.2 +++ b/src/ZF/Arith.thy	Tue Jul 16 16:28:26 2002 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4  
     1.5  constdefs
     1.6    pred   :: "i=>i"    (*inverse of succ*)
     1.7 -    "pred(y) == THE x. y = succ(x)"
     1.8 +    "pred(y) == nat_case(0, %x. x, y)"
     1.9  
    1.10    natify :: "i=>i"    (*coerces non-nats to nats*)
    1.11      "natify == Vrecursor(%f a. if a = succ(pred(a)) then succ(f`pred(a))
    1.12 @@ -376,6 +376,48 @@
    1.13  apply auto
    1.14  done
    1.15  
    1.16 +lemma pred_0 [simp]: "pred(0) = 0"
    1.17 +by (simp add: pred_def)
    1.18 +
    1.19 +lemma eq_succ_imp_eq_m1: "[|i = succ(j); i\<in>nat|] ==> j = i #- 1 & j \<in>nat"
    1.20 +by simp 
    1.21 +
    1.22 +lemma pred_Un_distrib:
    1.23 +    "[|i\<in>nat; j\<in>nat|] ==> pred(i Un j) = pred(i) Un pred(j)"
    1.24 +apply (erule_tac n=i in natE, simp) 
    1.25 +apply (erule_tac n=j in natE, simp) 
    1.26 +apply (simp add:  succ_Un_distrib [symmetric])
    1.27 +done
    1.28 +
    1.29 +lemma pred_type [TC,simp]:
    1.30 +    "i \<in> nat ==> pred(i) \<in> nat"
    1.31 +by (simp add: pred_def split: split_nat_case)
    1.32 +
    1.33 +lemma nat_diff_pred: "[|i\<in>nat; j\<in>nat|] ==> i #- succ(j) = pred(i #- j)";
    1.34 +apply (rule_tac m=i and n=j in diff_induct) 
    1.35 +apply (auto simp add: pred_def nat_imp_quasinat split: split_nat_case)
    1.36 +done
    1.37 +
    1.38 +lemma diff_succ_eq_pred: "i #- succ(j) = pred(i #- j)";
    1.39 +apply (insert nat_diff_pred [of "natify(i)" "natify(j)"])
    1.40 +apply (simp add: natify_succ [symmetric]) 
    1.41 +done
    1.42 +
    1.43 +lemma nat_diff_Un_distrib:
    1.44 +    "[|i\<in>nat; j\<in>nat; k\<in>nat|] ==> (i Un j) #- k = (i#-k) Un (j#-k)"
    1.45 +apply (rule_tac n=k in nat_induct) 
    1.46 +apply (simp_all add: diff_succ_eq_pred pred_Un_distrib) 
    1.47 +done
    1.48 +
    1.49 +lemma diff_Un_distrib:
    1.50 +    "[|i\<in>nat; j\<in>nat|] ==> (i Un j) #- k = (i#-k) Un (j#-k)"
    1.51 +by (insert nat_diff_Un_distrib [of i j "natify(k)"], simp)
    1.52 +
    1.53 +text{*We actually prove @{term "i #- j #- k = i #- (j #+ k)"}*}
    1.54 +lemma diff_diff_left [simplified]:
    1.55 +     "natify(i)#-natify(j)#-k = natify(i) #- (natify(j)#+k)";
    1.56 +by (rule_tac m="natify(i)" and n="natify(j)" in diff_induct, auto)
    1.57 +
    1.58  
    1.59  (** Lemmas for the CancelNumerals simproc **)
    1.60