src/HOL/HOLCF/ex/Dnat.thy
author huffman
Thu Sep 22 12:55:19 2011 -0700 (2011-09-22)
changeset 45049 13efaee97111
parent 42151 4da4fc77664b
child 62175 8ffc4d0e652d
permissions -rw-r--r--
discontinued HOLCF legacy theorem names
     1 (*  Title:      HOL/HOLCF/ex/Dnat.thy
     2     Author:     Franz Regensburger
     3 
     4 Theory for the domain of natural numbers  dnat = one ++ dnat
     5 *)
     6 
     7 theory Dnat
     8 imports HOLCF
     9 begin
    10 
    11 domain dnat = dzero | dsucc (dpred :: dnat)
    12 
    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))"
    18 
    19 text {*
    20   \medskip Expand fixed point properties.
    21 *}
    22 
    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
    31 
    32 text {* \medskip Recursive properties. *}
    33 
    34 lemma iterator1: "iterator $ UU $ f $ x = UU"
    35   apply (subst iterator_def2)
    36   apply simp
    37   done
    38 
    39 lemma iterator2: "iterator $ dzero $ f $ x = x"
    40   apply (subst iterator_def2)
    41   apply simp
    42   done
    43 
    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
    50 
    51 lemmas iterator_rews = iterator1 iterator2 iterator3
    52 
    53 lemma dnat_flat: "ALL x y::dnat. x<<y --> x=UU | x=y"
    54   apply (rule allI)
    55   apply (induct_tac x)
    56     apply fast
    57    apply (rule allI)
    58    apply (case_tac y)
    59      apply simp
    60     apply simp
    61    apply simp
    62   apply (rule allI)
    63   apply (case_tac y)
    64     apply (fast intro!: bottomI)
    65    apply (thin_tac "ALL y. dnat << y --> dnat = UU | dnat = y")
    66    apply simp
    67   apply (simp (no_asm_simp))
    68   apply (drule_tac x="dnata" in spec)
    69   apply simp
    70   done
    71 
    72 end