isabelle: src/HOLCF/dnat2.ML@645f46a24c72

     1 (*  Title: 	HOLCF/dnat2.ML

     2     ID:         $Id$

     3     Author: 	Franz Regensburger

     4     Copyright   1993 Technische Universitaet Muenchen

     6 Lemmas for theory Dnat2.thy

     7 *)

     9 open Dnat2;

    12 (* ------------------------------------------------------------------------- *)

    13 (* expand fixed point properties                                             *)

    14 (* ------------------------------------------------------------------------- *)

    16 val iterator_def2 = fix_prover Dnat2.thy iterator_def

    17 	"iterator = (LAM n f x. dnat_when[x][LAM m.f[iterator[m][f][x]]][n])";

    19 (* ------------------------------------------------------------------------- *)

    20 (* recursive  properties                                                     *)

    21 (* ------------------------------------------------------------------------- *)

    23 val iterator1 = prove_goal Dnat2.thy "iterator[UU][f][x] = UU"

    24  (fn prems =>

    25 	[

    26 	(rtac (iterator_def2 RS ssubst) 1),

    27 	(simp_tac (HOLCF_ss addsimps dnat_when) 1)

    28 	]);

    30 val iterator2 = prove_goal Dnat2.thy "iterator[dzero][f][x] = x"

    31  (fn prems =>

    32 	[

    33 	(rtac (iterator_def2 RS ssubst) 1),

    34 	(simp_tac (HOLCF_ss addsimps dnat_when) 1)

    35 	]);

    37 val iterator3 = prove_goal Dnat2.thy

    38 "n~=UU ==> iterator[dsucc[n]][f][x] = f[iterator[n][f][x]]"

    39  (fn prems =>

    40 	[

    41 	(cut_facts_tac prems 1),

    42 	(rtac trans 1),

    43 	(rtac (iterator_def2 RS ssubst) 1),

    44 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),

    45 	(rtac refl 1)

    46 	]);

    48 val dnat2_rews =

    49 	[iterator1, iterator2, iterator3];

author	wenzelm
	Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400	645f46a24c72
parent 243	c22b85994e17
permissions	-rw-r--r--