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
```