src/HOLCF/explicit_domains/Dnat2.ML

ex_impE was incorrectly listed as Safe

(*  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_prover2 Dnat2.thy iterator_def 
        "iterator = (LAM n f x. dnat_when`x`(LAM m.f`(iterator`m`f`x)) `n)";

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

qed_goal "iterator1" Dnat2.thy "iterator`UU`f`x = UU"
 (fn prems =>
        [
        (stac iterator_def2 1),
        (simp_tac (!simpset addsimps dnat_when) 1)
        ]);

qed_goal "iterator2" Dnat2.thy "iterator`dzero`f`x = x"
 (fn prems =>
        [
        (stac iterator_def2 1),
        (simp_tac (!simpset addsimps dnat_when) 1)
        ]);

qed_goal "iterator3" Dnat2.thy 
"n~=UU ==> iterator`(dsucc`n)`f`x = f`(iterator`n`f`x)"
 (fn prems =>
        [
        (cut_facts_tac prems 1),
        (rtac trans 1),
        (stac iterator_def2 1),
        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
        (rtac refl 1)
        ]);

val dnat2_rews = 
        [iterator1, iterator2, iterator3];