equal
deleted
inserted
replaced
25 by (rtac (rmap.dom_subset RS subset_trans) 1); |
25 by (rtac (rmap.dom_subset RS subset_trans) 1); |
26 by (REPEAT (ares_tac [domain_rel_subset, range_rel_subset, |
26 by (REPEAT (ares_tac [domain_rel_subset, range_rel_subset, |
27 Sigma_mono, list_mono] 1)); |
27 Sigma_mono, list_mono] 1)); |
28 qed "rmap_rel_type"; |
28 qed "rmap_rel_type"; |
29 |
29 |
30 Goal |
30 Goal "A <= domain(r) ==> list(A) <= domain(rmap(r))"; |
31 "!!r. A <= domain(r) ==> list(A) <= domain(rmap(r))"; |
|
32 by (rtac subsetI 1); |
31 by (rtac subsetI 1); |
33 by (etac list.induct 1); |
32 by (etac list.induct 1); |
34 by (ALLGOALS Fast_tac); |
33 by (ALLGOALS Fast_tac); |
35 qed "rmap_total"; |
34 qed "rmap_total"; |
36 |
35 |