equal
deleted
inserted
replaced
15 |
15 |
16 val [prem] = Goalw [mono_def] |
16 val [prem] = Goalw [mono_def] |
17 "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)"; |
17 "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)"; |
18 by (REPEAT (ares_tac [allI, impI, prem] 1)); |
18 by (REPEAT (ares_tac [allI, impI, prem] 1)); |
19 qed "monoI"; |
19 qed "monoI"; |
|
20 AddXIs [monoI]; |
20 |
21 |
21 Goalw [mono_def] "[| mono(f); A <= B |] ==> f(A) <= f(B)"; |
22 Goalw [mono_def] "[| mono(f); A <= B |] ==> f(A) <= f(B)"; |
22 by (Fast_tac 1); |
23 by (Fast_tac 1); |
23 qed "monoD"; |
24 qed "monoD"; |
|
25 AddXDs [monoD]; |
24 |
26 |
25 |
27 |
26 section "Orders"; |
28 section "Orders"; |
27 |
29 |
28 (** Reflexivity **) |
30 (** Reflexivity **) |