src/ZF/Integ/Int.ML
changeset 9578 ab26d6c8ebfe
parent 9576 3df14e0a3a51
child 9883 c1c8647af477
     1.1 --- a/src/ZF/Integ/Int.ML	Fri Aug 11 13:26:40 2000 +0200
     1.2 +++ b/src/ZF/Integ/Int.ML	Fri Aug 11 13:27:17 2000 +0200
     1.3 @@ -702,15 +702,15 @@
     1.4  
     1.5  (*This lemma allows direct proofs of other <-properties*)
     1.6  Goalw [zless_def, znegative_def, zdiff_def, int_def] 
     1.7 -    "[| w $< z; w: int; z: int |] ==> (EX n. z = w $+ $#(succ(n)))";
     1.8 +    "[| w $< z; w: int; z: int |] ==> (EX n: nat. z = w $+ $#(succ(n)))";
     1.9  by (auto_tac (claset() addSDs [less_imp_succ_add], 
    1.10                simpset() addsimps [zadd, zminus, int_of_def]));  
    1.11 -by (res_inst_tac [("x","k")] exI 1);
    1.12 +by (res_inst_tac [("x","k")] bexI 1);
    1.13  by (etac add_left_cancel 1);
    1.14  by Auto_tac;  
    1.15  val lemma = result();
    1.16  
    1.17 -Goal "w $< z ==> (EX n. w $+ $#(succ(n)) = intify(z))";
    1.18 +Goal "w $< z ==> (EX n: nat. w $+ $#(succ(n)) = intify(z))";
    1.19  by (subgoal_tac "intify(w) $< intify(z)" 1);
    1.20  by (dres_inst_tac [("w","intify(w)")] lemma 1);
    1.21  by Auto_tac;  
    1.22 @@ -729,10 +729,11 @@
    1.23  by Auto_tac;  
    1.24  qed "zless_succ_zadd";
    1.25  
    1.26 -Goal "w $< z <-> (EX n. w $+ $#(succ(n)) = intify(z))";
    1.27 +Goal "w $< z <-> (EX n: nat. w $+ $#(succ(n)) = intify(z))";
    1.28  by (rtac iffI 1);
    1.29  by (etac zless_imp_succ_zadd 1);
    1.30  by Auto_tac;  
    1.31 +by (rename_tac "n" 1);
    1.32  by (cut_inst_tac [("w","w"),("n","n")] zless_succ_zadd 1);
    1.33  by Auto_tac;  
    1.34  qed "zless_iff_succ_zadd";
    1.35 @@ -763,6 +764,16 @@
    1.36  (* [| z $< w; ~ P ==> w $< z |] ==> P *)
    1.37  bind_thm ("zless_asym", zless_not_sym RS swap);
    1.38  
    1.39 +Goalw [zle_def] "z $< w ==> z $<= w";
    1.40 +by (blast_tac (claset() addEs [zless_asym]) 1);
    1.41 +qed "zless_imp_zle";
    1.42 +
    1.43 +Goal "z $<= w | w $<= z";
    1.44 +by (simp_tac (simpset() addsimps [zle_def]) 1);
    1.45 +by (cut_facts_tac [zless_linear] 1);
    1.46 +by (Blast_tac 1);
    1.47 +qed "zle_linear";
    1.48 +
    1.49  
    1.50  (*** "Less Than or Equals", $<= ***)
    1.51  
    1.52 @@ -770,9 +781,18 @@
    1.53  by Auto_tac;  
    1.54  qed "zle_refl";
    1.55  
    1.56 +Goal "x=y ==> x $<= y";
    1.57 +by (asm_simp_tac (simpset() addsimps [zle_refl]) 1);
    1.58 +qed "zle_eq_refl";
    1.59 +
    1.60  Goalw [zle_def] "[| x $<= y; y $<= x |] ==> intify(x) = intify(y)";
    1.61  by Auto_tac;  
    1.62  by (blast_tac (claset() addDs [zless_trans]) 1);
    1.63 +qed "zle_anti_sym_intify";
    1.64 +
    1.65 +Goal "[| x $<= y; y $<= x; x: int; y: int |] ==> x=y"; 
    1.66 +by (dtac zle_anti_sym_intify 1);
    1.67 +by Auto_tac;  
    1.68  qed "zle_anti_sym";
    1.69  
    1.70  Goalw [zle_def] "[| x: int; y: int; z: int; x $<= y; y $<= z |] ==> x $<= z";