wneuper/isa: src/HOLCF/ex/Dnat.thy@31cbcb019003

     1 (*  Title:      HOLCF/Dnat.thy

     2     Author:     Franz Regensburger

     4 Theory for the domain of natural numbers  dnat = one ++ dnat

     5 *)

     7 theory Dnat

     8 imports HOLCF

     9 begin

    11 domain dnat = dzero | dsucc (dpred :: dnat)

    13 definition

    14   iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a" where

    15   "iterator = fix $ (LAM h n f x.

    16     case n of dzero => x

    17       | dsucc $ m => f $ (h $ m $ f $ x))"

    19 text {*

    20   \medskip Expand fixed point properties.

    21 *}

    23 lemma iterator_def2:

    24   "iterator = (LAM n f x. case n of dzero => x | dsucc$m => f$(iterator$m$f$x))"

    25   apply (rule trans)

    26   apply (rule fix_eq2)

    27   apply (rule iterator_def [THEN eq_reflection])

    28   apply (rule beta_cfun)

    29   apply simp

    30   done

    32 text {* \medskip Recursive properties. *}

    34 lemma iterator1: "iterator $ UU $ f $ x = UU"

    35   apply (subst iterator_def2)

    36   apply simp

    37   done

    39 lemma iterator2: "iterator $ dzero $ f $ x = x"

    40   apply (subst iterator_def2)

    41   apply simp

    42   done

    44 lemma iterator3: "n ~= UU ==> iterator $ (dsucc $ n) $ f $ x = f $ (iterator $ n $ f $ x)"

    45   apply (rule trans)

    46    apply (subst iterator_def2)

    47    apply simp

    48   apply (rule refl)

    49   done

    51 lemmas iterator_rews = iterator1 iterator2 iterator3

    53 lemma dnat_flat: "ALL x y::dnat. x<<y --> x=UU | x=y"

    54   apply (rule allI)

    55   apply (induct_tac x rule: dnat.ind)

    56     apply fast

    57    apply (rule allI)

    58    apply (rule_tac x = y in dnat.casedist)

    59      apply simp

    60     apply simp

    61    apply simp

    62   apply (rule allI)

    63   apply (rule_tac x = y in dnat.casedist)

    64     apply (fast intro!: UU_I)

    65    apply (thin_tac "ALL y. d << y --> d = UU | d = y")

    66    apply simp

    67   apply (simp (no_asm_simp))

    68   apply (drule_tac x="da" in spec)

    69   apply simp

    70   done

    72 end

author	huffman
	Wed, 17 Feb 2010 09:08:58 -0800
changeset 35169	31cbcb019003
parent 27108	e447b3107696
child 35429	2e0f9516947e
permissions	-rw-r--r--