equal
deleted
inserted
replaced
42 (*The inclusion is POSITIVE! *) |
42 (*The inclusion is POSITIVE! *) |
43 val [prem] = goal Set.thy |
43 val [prem] = goal Set.thy |
44 "[| !!x. f(x)<=g(x) |] ==> (INT x. f(x)) <= (INT x. g(x))"; |
44 "[| !!x. f(x)<=g(x) |] ==> (INT x. f(x)) <= (INT x. g(x))"; |
45 by (fast_tac (!claset addIs [prem RS subsetD]) 1); |
45 by (fast_tac (!claset addIs [prem RS subsetD]) 1); |
46 qed "INT1_mono"; |
46 qed "INT1_mono"; |
|
47 |
|
48 goal Set.thy "!!C D. C<=D ==> insert a C <= insert a D"; |
|
49 by (Fast_tac 1); |
|
50 qed "insert_mono"; |
47 |
51 |
48 goal Set.thy "!!A B. [| A<=C; B<=D |] ==> A Un B <= C Un D"; |
52 goal Set.thy "!!A B. [| A<=C; B<=D |] ==> A Un B <= C Un D"; |
49 by (Fast_tac 1); |
53 by (Fast_tac 1); |
50 qed "Un_mono"; |
54 qed "Un_mono"; |
51 |
55 |