src/HOLCF/explicit_domains/Dnat2.ML
changeset 2679 3eac428cdd1b
parent 2678 d5fe793293ac
child 2680 20fa49e610ca
     1.1 --- a/src/HOLCF/explicit_domains/Dnat2.ML	Mon Feb 24 09:46:12 1997 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,52 +0,0 @@
     1.4 -(*  Title:      HOLCF/Dnat2.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Franz Regensburger
     1.7 -    Copyright   1993 Technische Universitaet Muenchen
     1.8 -
     1.9 -Lemmas for theory Dnat2.thy
    1.10 -*)
    1.11 -
    1.12 -open Dnat2;
    1.13 -
    1.14 -
    1.15 -(* ------------------------------------------------------------------------- *)
    1.16 -(* expand fixed point properties                                             *)
    1.17 -(* ------------------------------------------------------------------------- *)
    1.18 -
    1.19 -val iterator_def2 = fix_prover2 Dnat2.thy iterator_def 
    1.20 -        "iterator = (LAM n f x. dnat_when`x`(LAM m.f`(iterator`m`f`x)) `n)";
    1.21 -
    1.22 -(* ------------------------------------------------------------------------- *)
    1.23 -(* recursive  properties                                                     *)
    1.24 -(* ------------------------------------------------------------------------- *)
    1.25 -
    1.26 -qed_goal "iterator1" Dnat2.thy "iterator`UU`f`x = UU"
    1.27 - (fn prems =>
    1.28 -        [
    1.29 -        (stac iterator_def2 1),
    1.30 -        (simp_tac (!simpset addsimps dnat_when) 1)
    1.31 -        ]);
    1.32 -
    1.33 -qed_goal "iterator2" Dnat2.thy "iterator`dzero`f`x = x"
    1.34 - (fn prems =>
    1.35 -        [
    1.36 -        (stac iterator_def2 1),
    1.37 -        (simp_tac (!simpset addsimps dnat_when) 1)
    1.38 -        ]);
    1.39 -
    1.40 -qed_goal "iterator3" Dnat2.thy 
    1.41 -"n~=UU ==> iterator`(dsucc`n)`f`x = f`(iterator`n`f`x)"
    1.42 - (fn prems =>
    1.43 -        [
    1.44 -        (cut_facts_tac prems 1),
    1.45 -        (rtac trans 1),
    1.46 -        (stac iterator_def2 1),
    1.47 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
    1.48 -        (rtac refl 1)
    1.49 -        ]);
    1.50 -
    1.51 -val dnat2_rews = 
    1.52 -        [iterator1, iterator2, iterator3];
    1.53 -
    1.54 -
    1.55 -