equal
deleted
inserted
replaced
45 |
45 |
46 goal CoUnit.thy "lfp(univ(0), %x. Con2(x,x)) : counit2"; |
46 goal CoUnit.thy "lfp(univ(0), %x. Con2(x,x)) : counit2"; |
47 by (rtac (singletonI RS counit2.coinduct) 1); |
47 by (rtac (singletonI RS counit2.coinduct) 1); |
48 by (rtac (qunivI RS singleton_subsetI) 1); |
48 by (rtac (qunivI RS singleton_subsetI) 1); |
49 by (rtac ([lfp_subset, empty_subsetI RS univ_mono] MRS subset_trans) 1); |
49 by (rtac ([lfp_subset, empty_subsetI RS univ_mono] MRS subset_trans) 1); |
50 by (fast_tac (!claset addSIs [Con2_bnd_mono RS lfp_Tarski]) 1); |
50 by (fast_tac (claset() addSIs [Con2_bnd_mono RS lfp_Tarski]) 1); |
51 qed "lfp_Con2_in_counit2"; |
51 qed "lfp_Con2_in_counit2"; |
52 |
52 |
53 (*Lemma for proving finality. Borrowed from ex/llist_eq.ML!*) |
53 (*Lemma for proving finality. Borrowed from ex/llist_eq.ML!*) |
54 goal CoUnit.thy |
54 goal CoUnit.thy |
55 "!!i. Ord(i) ==> ALL x y. x: counit2 & y: counit2 --> x Int Vset(i) <= y"; |
55 "!!i. Ord(i) ==> ALL x y. x: counit2 & y: counit2 --> x Int Vset(i) <= y"; |