equal
deleted
inserted
replaced
59 |
59 |
60 Goal "[| #0 $< k; k \\<in> int |] ==> 0 < zmagnitude(k)"; |
60 Goal "[| #0 $< k; k \\<in> int |] ==> 0 < zmagnitude(k)"; |
61 by (dtac zero_zless_imp_znegative_zminus 1); |
61 by (dtac zero_zless_imp_znegative_zminus 1); |
62 by (dtac zneg_int_of 2); |
62 by (dtac zneg_int_of 2); |
63 by (auto_tac (claset(), simpset() addsimps [inst "x" "k" zminus_equation])); |
63 by (auto_tac (claset(), simpset() addsimps [inst "x" "k" zminus_equation])); |
64 by (subgoal_tac "0 < zmagnitude($# succ(x))" 1); |
64 by (subgoal_tac "0 < zmagnitude($# succ(n))" 1); |
65 by (Asm_full_simp_tac 1); |
65 by (Asm_full_simp_tac 1); |
66 by (asm_full_simp_tac (FOL_ss addsimps [zmagnitude_int_of]) 1); |
66 by (asm_full_simp_tac (FOL_ss addsimps [zmagnitude_int_of]) 1); |
67 by (Asm_full_simp_tac 1); |
67 by (Asm_full_simp_tac 1); |
68 qed "zero_lt_zmagnitude"; |
68 qed "zero_lt_zmagnitude"; |
69 |
69 |
77 by (res_inst_tac [("x","0")] bexI 3); |
77 by (res_inst_tac [("x","0")] bexI 3); |
78 by (TRYALL (dtac sym)); |
78 by (TRYALL (dtac sym)); |
79 by (cut_inst_tac [("m","m")] int_succ_int_1 1); |
79 by (cut_inst_tac [("m","m")] int_succ_int_1 1); |
80 by (cut_inst_tac [("m","n")] int_succ_int_1 1); |
80 by (cut_inst_tac [("m","n")] int_succ_int_1 1); |
81 by (Asm_full_simp_tac 1); |
81 by (Asm_full_simp_tac 1); |
82 by (eres_inst_tac [("n","x")] natE 1); |
82 by (etac natE 1); |
83 by Auto_tac; |
83 by Auto_tac; |
84 by (res_inst_tac [("x","succ(x)")] bexI 1); |
84 by (res_inst_tac [("x","succ(n)")] bexI 1); |
85 by Auto_tac; |
85 by Auto_tac; |
86 qed "zless_add_succ_iff"; |
86 qed "zless_add_succ_iff"; |
87 |
87 |
88 Goal "z \\<in> int ==> (w $+ $# succ(m) $<= z) <-> (w $+ $#m $< z)"; |
88 Goal "z \\<in> int ==> (w $+ $# succ(m) $<= z) <-> (w $+ $#m $< z)"; |
89 by (asm_simp_tac (simpset_of Int.thy addsimps |
89 by (asm_simp_tac (simpset_of Int.thy addsimps |