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;
nipkow@243
     1
(*  Title: 	HOLCF/dnat2.ML
nipkow@243
     2
    ID:         $Id$
nipkow@243
     3
    Author: 	Franz Regensburger
nipkow@243
     4
    Copyright   1993 Technische Universitaet Muenchen
nipkow@243
     5
nipkow@243
     6
Lemmas for theory Dnat2.thy
nipkow@243
     7
*)
nipkow@243
     8
nipkow@243
     9
open Dnat2;
nipkow@243
    10
nipkow@243
    11
nipkow@243
    12
(* ------------------------------------------------------------------------- *)
nipkow@243
    13
(* expand fixed point properties                                             *)
nipkow@243
    14
(* ------------------------------------------------------------------------- *)
nipkow@243
    15
nipkow@243
    16
val iterator_def2 = fix_prover Dnat2.thy iterator_def 
nipkow@243
    17
	"iterator = (LAM n f x. dnat_when[x][LAM m.f[iterator[m][f][x]]][n])";
nipkow@243
    18
nipkow@243
    19
(* ------------------------------------------------------------------------- *)
nipkow@243
    20
(* recursive  properties                                                     *)
nipkow@243
    21
(* ------------------------------------------------------------------------- *)
nipkow@243
    22
nipkow@243
    23
val iterator1 = prove_goal Dnat2.thy "iterator[UU][f][x] = UU"
nipkow@243
    24
 (fn prems =>
nipkow@243
    25
	[
nipkow@243
    26
	(rtac (iterator_def2 RS ssubst) 1),
nipkow@243
    27
	(simp_tac (HOLCF_ss addsimps dnat_when) 1)
nipkow@243
    28
	]);
nipkow@243
    29
nipkow@243
    30
val iterator2 = prove_goal Dnat2.thy "iterator[dzero][f][x] = x"
nipkow@243
    31
 (fn prems =>
nipkow@243
    32
	[
nipkow@243
    33
	(rtac (iterator_def2 RS ssubst) 1),
nipkow@243
    34
	(simp_tac (HOLCF_ss addsimps dnat_when) 1)
nipkow@243
    35
	]);
nipkow@243
    36
nipkow@243
    37
val iterator3 = prove_goal Dnat2.thy 
nipkow@243
    38
"n~=UU ==> iterator[dsucc[n]][f][x] = f[iterator[n][f][x]]"
nipkow@243
    39
 (fn prems =>
nipkow@243
    40
	[
nipkow@243
    41
	(cut_facts_tac prems 1),
nipkow@243
    42
	(rtac trans 1),
nipkow@243
    43
	(rtac (iterator_def2 RS ssubst) 1),
nipkow@243
    44
	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
nipkow@243
    45
	(rtac refl 1)
nipkow@243
    46
	]);
nipkow@243
    47
nipkow@243
    48
val dnat2_rews = 
nipkow@243
    49
	[iterator1, iterator2, iterator3];
nipkow@243
    50
nipkow@243
    51
nipkow@243
    52