src/HOLCF/ex/Dnat.thy
changeset 40774 0437dbc127b3
parent 40773 6c12f5e24e34
child 40775 ed7a4eadb2f6
     1.1 --- a/src/HOLCF/ex/Dnat.thy	Sat Nov 27 14:34:54 2010 -0800
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,72 +0,0 @@
     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