equal
deleted
inserted
replaced
34 assumes 1: "Porder.chain Y" |
34 assumes 1: "Porder.chain Y" |
35 assumes 2: "!i. P (Y i)" |
35 assumes 2: "!i. P (Y i)" |
36 assumes 3: "(!!Y. [| Porder.chain Y; !i. P (Y i); !k. ? j. Fin k < #((Y j)::'a::flat stream)|] |
36 assumes 3: "(!!Y. [| Porder.chain Y; !i. P (Y i); !k. ? j. Fin k < #((Y j)::'a::flat stream)|] |
37 ==> P(lub (range Y)))" |
37 ==> P(lub (range Y)))" |
38 shows "P(lub (range Y))" |
38 shows "P(lub (range Y))" |
39 apply (rule increasing_chain_adm_lemma [OF 1 2]) |
39 apply (rule increasing_chain_adm_lemma [of _ P, OF 1 2]) |
40 apply (erule 3, assumption) |
40 apply (erule 3, assumption) |
41 apply (erule thin_rl) |
41 apply (erule thin_rl) |
42 apply (rule allI) |
42 apply (rule allI) |
43 apply (case_tac "!j. stream_finite (Y j)") |
43 apply (case_tac "!j. stream_finite (Y j)") |
44 apply ( rule chain_incr) |
44 apply ( rule chain_incr) |