97 |
97 |
98 goalw LList.thy [LList_corec_def] |
98 goalw LList.thy [LList_corec_def] |
99 "LList_corec(a,f) <= case(f(a), %u.NIL, \ |
99 "LList_corec(a,f) <= case(f(a), %u.NIL, \ |
100 \ %v. split(v, %z w. CONS(z, LList_corec(w,f))))"; |
100 \ %v. split(v, %z w. CONS(z, LList_corec(w,f))))"; |
101 by (rtac UN1_least 1); |
101 by (rtac UN1_least 1); |
102 by (nat_ind_tac "k" 1); |
102 by (res_inst_tac [("n","k")] natE 1); |
103 by (ALLGOALS(simp_tac corec_fun_ss)); |
103 by (ALLGOALS (asm_simp_tac corec_fun_ss)); |
104 by (REPEAT (resolve_tac [allI, impI, subset_refl RS CONS_mono, UN1_upper] 1)); |
104 by (REPEAT (resolve_tac [allI, impI, subset_refl RS CONS_mono, UN1_upper] 1)); |
105 val LList_corec_subset1 = result(); |
105 val LList_corec_subset1 = result(); |
106 |
106 |
107 goalw LList.thy [LList_corec_def] |
107 goalw LList.thy [LList_corec_def] |
108 "case(f(a), %u.NIL, %v. split(v, %z w. CONS(z, LList_corec(w,f)))) <= \ |
108 "case(f(a), %u.NIL, %v. split(v, %z w. CONS(z, LList_corec(w,f)))) <= \ |