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.11 -by (res_inst_tac [("x","k")] exI 1);
1.12 +by (res_inst_tac [("x","k")] bexI 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.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.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.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";
```