equal
deleted
inserted
replaced
45 Goal "(x::'a::order) <= y = (x < y | x = y)"; |
45 Goal "(x::'a::order) <= y = (x < y | x = y)"; |
46 by (simp_tac (simpset() addsimps [order_less_le]) 1); |
46 by (simp_tac (simpset() addsimps [order_less_le]) 1); |
47 (*NOT suitable for AddIffs, since it can cause PROOF FAILED*) |
47 (*NOT suitable for AddIffs, since it can cause PROOF FAILED*) |
48 by (blast_tac (claset() addSIs [order_refl]) 1); |
48 by (blast_tac (claset() addSIs [order_refl]) 1); |
49 qed "order_le_less"; |
49 qed "order_le_less"; |
|
50 |
|
51 Goal "!!x::'a::order. x < y ==> x <= y"; |
|
52 by (asm_full_simp_tac (simpset() addsimps [order_less_le]) 1); |
|
53 qed "order_less_imp_le"; |
50 |
54 |
51 (** Asymmetry **) |
55 (** Asymmetry **) |
52 |
56 |
53 Goal "(x::'a::order) < y ==> ~ (y<x)"; |
57 Goal "(x::'a::order) < y ==> ~ (y<x)"; |
54 by (asm_full_simp_tac (simpset() addsimps [order_less_le, order_antisym]) 1); |
58 by (asm_full_simp_tac (simpset() addsimps [order_less_le, order_antisym]) 1); |