Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong
uses lemma sum_bij; proof of prod_eqpoll_cong uses lemma prod_bij.
(* Title: HOLCF/dnat2.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Additional constants for dnat
*)
Dnat2 = Dnat +
consts
iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a"
rules
iterator_def "iterator = fix[LAM h n f x.\
\ dnat_when[x][LAM m.f[h[m][f][x]]][n]]"
end
(*
iterator[UU][f][x] = UU
iterator[dzero][f][x] = x
n~=UU --> iterator[dsucc[n]][f][x] = f[iterator[n][f][x]]
*)