equal
deleted
inserted
replaced
468 by (rtac (Ord_rank RS iprem) 1); |
468 by (rtac (Ord_rank RS iprem) 1); |
469 qed "Int_Vset_subset"; |
469 qed "Int_Vset_subset"; |
470 |
470 |
471 (** Set up an environment for simplification **) |
471 (** Set up an environment for simplification **) |
472 |
472 |
|
473 goalw Univ.thy [Inl_def] "rank(a) < rank(Inl(a))"; |
|
474 by (rtac rank_pair2 1); |
|
475 qed "rank_Inl"; |
|
476 |
|
477 goalw Univ.thy [Inr_def] "rank(a) < rank(Inr(a))"; |
|
478 by (rtac rank_pair2 1); |
|
479 qed "rank_Inr"; |
|
480 |
473 val rank_rls = [rank_Inl, rank_Inr, rank_pair1, rank_pair2]; |
481 val rank_rls = [rank_Inl, rank_Inr, rank_pair1, rank_pair2]; |
474 val rank_trans_rls = rank_rls @ (rank_rls RLN (2, [lt_trans])); |
482 val rank_trans_rls = rank_rls @ (rank_rls RLN (2, [lt_trans])); |
475 |
483 |
476 val rank_ss = !simpset addsimps [VsetI] addsimps rank_trans_rls; |
484 val rank_ss = !simpset addsimps [VsetI] addsimps rank_trans_rls; |
477 |
485 |