equal
deleted
inserted
replaced
106 Goalw [less_def] "wf {(x,y::nat). x<y}"; |
106 Goalw [less_def] "wf {(x,y::nat). x<y}"; |
107 by (rtac (wf_pred_nat RS wf_trancl RS wf_subset) 1); |
107 by (rtac (wf_pred_nat RS wf_trancl RS wf_subset) 1); |
108 by (Blast_tac 1); |
108 by (Blast_tac 1); |
109 qed "wf_less"; |
109 qed "wf_less"; |
110 |
110 |
111 (*Used in TFL/post.sml*) |
111 Goalw [less_def] "((m,n) : pred_nat^+) = (m<n)"; |
112 Goalw [less_def] "(m,n) : pred_nat^+ = (m<n)"; |
|
113 by (rtac refl 1); |
112 by (rtac refl 1); |
114 qed "less_eq"; |
113 qed "less_eq"; |
115 |
114 |
116 (** Introduction properties **) |
115 (** Introduction properties **) |
117 |
116 |
424 qed "Suc_le_mono"; |
423 qed "Suc_le_mono"; |
425 |
424 |
426 AddIffs [Suc_le_mono]; |
425 AddIffs [Suc_le_mono]; |
427 |
426 |
428 (* Axiom 'order_less_le' of class 'order': *) |
427 (* Axiom 'order_less_le' of class 'order': *) |
429 Goal "(m::nat) < n = (m <= n & m ~= n)"; |
428 Goal "((m::nat) < n) = (m <= n & m ~= n)"; |
430 by (simp_tac (simpset() addsimps [le_def, nat_neq_iff]) 1); |
429 by (simp_tac (simpset() addsimps [le_def, nat_neq_iff]) 1); |
431 by (blast_tac (claset() addSEs [less_asym]) 1); |
430 by (blast_tac (claset() addSEs [less_asym]) 1); |
432 qed "nat_less_le"; |
431 qed "nat_less_le"; |
433 |
432 |
434 (* [| m <= n; m ~= n |] ==> m < n *) |
433 (* [| m <= n; m ~= n |] ==> m < n *) |