src/HOLCF/dnat2.ML

revised for new treatment of integers

(*  Title: 	HOLCF/dnat2.ML
    ID:         $Id$
    Author: 	Franz Regensburger
    Copyright   1993 Technische Universitaet Muenchen

Lemmas for theory Dnat2.thy
*)

open Dnat2;


(* ------------------------------------------------------------------------- *)
(* expand fixed point properties                                             *)
(* ------------------------------------------------------------------------- *)

val iterator_def2 = fix_prover Dnat2.thy iterator_def 
	"iterator = (LAM n f x. dnat_when[x][LAM m.f[iterator[m][f][x]]][n])";

(* ------------------------------------------------------------------------- *)
(* recursive  properties                                                     *)
(* ------------------------------------------------------------------------- *)

val iterator1 = prove_goal Dnat2.thy "iterator[UU][f][x] = UU"
 (fn prems =>
	[
	(rtac (iterator_def2 RS ssubst) 1),
	(simp_tac (HOLCF_ss addsimps dnat_when) 1)
	]);

val iterator2 = prove_goal Dnat2.thy "iterator[dzero][f][x] = x"
 (fn prems =>
	[
	(rtac (iterator_def2 RS ssubst) 1),
	(simp_tac (HOLCF_ss addsimps dnat_when) 1)
	]);

val iterator3 = prove_goal Dnat2.thy 
"n~=UU ==> iterator[dsucc[n]][f][x] = f[iterator[n][f][x]]"
 (fn prems =>
	[
	(cut_facts_tac prems 1),
	(rtac trans 1),
	(rtac (iterator_def2 RS ssubst) 1),
	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
	(rtac refl 1)
	]);

val dnat2_rews = 
	[iterator1, iterator2, iterator3];