equal
deleted
inserted
replaced
56 |
56 |
57 (*Easily provable by induction also*) |
57 (*Easily provable by induction also*) |
58 goalw Ntree.thy (ntree.defs@ntree.con_defs) "ntree(univ(A)) <= univ(A)"; |
58 goalw Ntree.thy (ntree.defs@ntree.con_defs) "ntree(univ(A)) <= univ(A)"; |
59 by (rtac lfp_lowerbound 1); |
59 by (rtac lfp_lowerbound 1); |
60 by (rtac (A_subset_univ RS univ_mono) 2); |
60 by (rtac (A_subset_univ RS univ_mono) 2); |
61 by (safe_tac (claset())); |
61 by Safe_tac; |
62 by (REPEAT (ares_tac [Pair_in_univ, nat_fun_univ RS subsetD] 1)); |
62 by (REPEAT (ares_tac [Pair_in_univ, nat_fun_univ RS subsetD] 1)); |
63 qed "ntree_univ"; |
63 qed "ntree_univ"; |
64 |
64 |
65 val ntree_subset_univ = [ntree_mono, ntree_univ] MRS subset_trans |> standard; |
65 val ntree_subset_univ = [ntree_mono, ntree_univ] MRS subset_trans |> standard; |
66 |
66 |