equal
deleted
inserted
replaced
311 qed "THE_eq"; |
311 qed "THE_eq"; |
312 |
312 |
313 goal thy "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))"; |
313 goal thy "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))"; |
314 by (rtac (transrec2_def RS def_transrec RS trans) 1); |
314 by (rtac (transrec2_def RS def_transrec RS trans) 1); |
315 by (simp_tac (!simpset addsimps [succ_not_0, THE_eq, if_P] |
315 by (simp_tac (!simpset addsimps [succ_not_0, THE_eq, if_P] |
316 setsolver K Fast_tac) 1); |
316 setSolver K Fast_tac) 1); |
317 qed "transrec2_succ"; |
317 qed "transrec2_succ"; |
318 |
318 |
319 goal thy "!!i. Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))"; |
319 goal thy "!!i. Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))"; |
320 by (rtac (transrec2_def RS def_transrec RS trans) 1); |
320 by (rtac (transrec2_def RS def_transrec RS trans) 1); |
321 by (resolve_tac [if_not_P RS trans] 1 THEN |
321 by (resolve_tac [if_not_P RS trans] 1 THEN |