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
wenzelm@42151
     1
(*  Title:      HOL/HOLCF/ex/Dnat.thy
oheimb@2570
     2
    Author:     Franz Regensburger
oheimb@2570
     3
oheimb@2570
     4
Theory for the domain of natural numbers  dnat = one ++ dnat
oheimb@2570
     5
*)
oheimb@2570
     6
haftmann@27108
     7
theory Dnat
haftmann@27108
     8
imports HOLCF
haftmann@27108
     9
begin
oheimb@2570
    10
oheimb@2570
    11
domain dnat = dzero | dsucc (dpred :: dnat)
oheimb@2570
    12
wenzelm@19763
    13
definition
wenzelm@21404
    14
  iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a" where
wenzelm@19763
    15
  "iterator = fix $ (LAM h n f x.
wenzelm@12035
    16
    case n of dzero => x
wenzelm@12035
    17
      | dsucc $ m => f $ (h $ m $ f $ x))"
oheimb@2570
    18
wenzelm@12035
    19
text {*
wenzelm@12035
    20
  \medskip Expand fixed point properties.
wenzelm@12035
    21
*}
wenzelm@12035
    22
wenzelm@19764
    23
lemma iterator_def2:
wenzelm@19764
    24
  "iterator = (LAM n f x. case n of dzero => x | dsucc$m => f$(iterator$m$f$x))"
wenzelm@19764
    25
  apply (rule trans)
wenzelm@19764
    26
  apply (rule fix_eq2)
wenzelm@19764
    27
  apply (rule iterator_def [THEN eq_reflection])
wenzelm@19764
    28
  apply (rule beta_cfun)
wenzelm@19764
    29
  apply simp
wenzelm@19764
    30
  done
wenzelm@12035
    31
wenzelm@19764
    32
text {* \medskip Recursive properties. *}
wenzelm@12035
    33
wenzelm@12035
    34
lemma iterator1: "iterator $ UU $ f $ x = UU"
wenzelm@12035
    35
  apply (subst iterator_def2)
huffman@35169
    36
  apply simp
wenzelm@12035
    37
  done
wenzelm@12035
    38
wenzelm@12035
    39
lemma iterator2: "iterator $ dzero $ f $ x = x"
wenzelm@12035
    40
  apply (subst iterator_def2)
huffman@35169
    41
  apply simp
wenzelm@12035
    42
  done
wenzelm@12035
    43
wenzelm@12035
    44
lemma iterator3: "n ~= UU ==> iterator $ (dsucc $ n) $ f $ x = f $ (iterator $ n $ f $ x)"
wenzelm@12035
    45
  apply (rule trans)
wenzelm@12035
    46
   apply (subst iterator_def2)
huffman@35169
    47
   apply simp
wenzelm@12035
    48
  apply (rule refl)
wenzelm@12035
    49
  done
wenzelm@12035
    50
wenzelm@12035
    51
lemmas iterator_rews = iterator1 iterator2 iterator3
wenzelm@12035
    52
wenzelm@12035
    53
lemma dnat_flat: "ALL x y::dnat. x<<y --> x=UU | x=y"
wenzelm@12035
    54
  apply (rule allI)
huffman@35781
    55
  apply (induct_tac x)
wenzelm@12035
    56
    apply fast
wenzelm@12035
    57
   apply (rule allI)
huffman@35532
    58
   apply (case_tac y)
huffman@19550
    59
     apply simp
wenzelm@12035
    60
    apply simp
huffman@35169
    61
   apply simp
wenzelm@12035
    62
  apply (rule allI)
huffman@35532
    63
  apply (case_tac y)
huffman@45049
    64
    apply (fast intro!: bottomI)
huffman@35443
    65
   apply (thin_tac "ALL y. dnat << y --> dnat = UU | dnat = y")
huffman@35169
    66
   apply simp
huffman@35169
    67
  apply (simp (no_asm_simp))
huffman@35443
    68
  apply (drule_tac x="dnata" in spec)
huffman@19550
    69
  apply simp
wenzelm@12035
    70
  done
oheimb@2570
    71
oheimb@2570
    72
end