src/HOL/HOLCF/ex/Dnat.thy
changeset 40774 0437dbc127b3
parent 35781 b7738ab762b1
child 42151 4da4fc77664b
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/HOLCF/ex/Dnat.thy	Sat Nov 27 16:08:10 2010 -0800
     1.3 @@ -0,0 +1,72 @@
     1.4 +(*  Title:      HOLCF/Dnat.thy
     1.5 +    Author:     Franz Regensburger
     1.6 +
     1.7 +Theory for the domain of natural numbers  dnat = one ++ dnat
     1.8 +*)
     1.9 +
    1.10 +theory Dnat
    1.11 +imports HOLCF
    1.12 +begin
    1.13 +
    1.14 +domain dnat = dzero | dsucc (dpred :: dnat)
    1.15 +
    1.16 +definition
    1.17 +  iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a" where
    1.18 +  "iterator = fix $ (LAM h n f x.
    1.19 +    case n of dzero => x
    1.20 +      | dsucc $ m => f $ (h $ m $ f $ x))"
    1.21 +
    1.22 +text {*
    1.23 +  \medskip Expand fixed point properties.
    1.24 +*}
    1.25 +
    1.26 +lemma iterator_def2:
    1.27 +  "iterator = (LAM n f x. case n of dzero => x | dsucc$m => f$(iterator$m$f$x))"
    1.28 +  apply (rule trans)
    1.29 +  apply (rule fix_eq2)
    1.30 +  apply (rule iterator_def [THEN eq_reflection])
    1.31 +  apply (rule beta_cfun)
    1.32 +  apply simp
    1.33 +  done
    1.34 +
    1.35 +text {* \medskip Recursive properties. *}
    1.36 +
    1.37 +lemma iterator1: "iterator $ UU $ f $ x = UU"
    1.38 +  apply (subst iterator_def2)
    1.39 +  apply simp
    1.40 +  done
    1.41 +
    1.42 +lemma iterator2: "iterator $ dzero $ f $ x = x"
    1.43 +  apply (subst iterator_def2)
    1.44 +  apply simp
    1.45 +  done
    1.46 +
    1.47 +lemma iterator3: "n ~= UU ==> iterator $ (dsucc $ n) $ f $ x = f $ (iterator $ n $ f $ x)"
    1.48 +  apply (rule trans)
    1.49 +   apply (subst iterator_def2)
    1.50 +   apply simp
    1.51 +  apply (rule refl)
    1.52 +  done
    1.53 +
    1.54 +lemmas iterator_rews = iterator1 iterator2 iterator3
    1.55 +
    1.56 +lemma dnat_flat: "ALL x y::dnat. x<<y --> x=UU | x=y"
    1.57 +  apply (rule allI)
    1.58 +  apply (induct_tac x)
    1.59 +    apply fast
    1.60 +   apply (rule allI)
    1.61 +   apply (case_tac y)
    1.62 +     apply simp
    1.63 +    apply simp
    1.64 +   apply simp
    1.65 +  apply (rule allI)
    1.66 +  apply (case_tac y)
    1.67 +    apply (fast intro!: UU_I)
    1.68 +   apply (thin_tac "ALL y. dnat << y --> dnat = UU | dnat = y")
    1.69 +   apply simp
    1.70 +  apply (simp (no_asm_simp))
    1.71 +  apply (drule_tac x="dnata" in spec)
    1.72 +  apply simp
    1.73 +  done
    1.74 +
    1.75 +end