src/HOLCF/dnat2.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 243 c22b85994e17
permissions -rw-r--r--
made tutorial first;
     1 (*  Title: 	HOLCF/dnat2.ML
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Lemmas for theory Dnat2.thy
     7 *)
     8 
     9 open Dnat2;
    10 
    11 
    12 (* ------------------------------------------------------------------------- *)
    13 (* expand fixed point properties                                             *)
    14 (* ------------------------------------------------------------------------- *)
    15 
    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])";
    18 
    19 (* ------------------------------------------------------------------------- *)
    20 (* recursive  properties                                                     *)
    21 (* ------------------------------------------------------------------------- *)
    22 
    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 	]);
    29 
    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 	]);
    36 
    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 	]);
    47 
    48 val dnat2_rews = 
    49 	[iterator1, iterator2, iterator3];
    50 
    51 
    52