Quelle Dnat.thy Sprache: Isabelle

(*  Title:      HOL/HOLCF/ex/Dnat.thy
    Author:     Franz Regensburger

Theory for the domain of natural numbers  dnat = one ++ dnat
*)

theory Dnat
imports HOLCF
begin

domain dnat = dzero | dsucc (dpred :: dnat)

definition
  iterator :: "dnat \ ('a \ 'a) \ 'a \ 'a" where
  "iterator = fix\(LAM h n f x.
    case n of dzero \<Rightarrow> x
      | dsucc\<cdot>m \<Rightarrow> f\<cdot>(h\<cdot>m\<cdot>f\<cdot>x))"

text \<open>
  \medskip Expand fixed point properties.
\<close>

lemma iterator_def2:
  "iterator = (LAM n f x. case n of dzero \ x | dsucc\m \ f\(iterator\m\f\x))"
  apply (rule trans)
  apply (rule fix_eq2)
  apply (rule iterator_def [THEN eq_reflection])
  apply (rule beta_cfun)
  apply simp
  done

text \<open>\medskip Recursive properties.\<close>

lemma iterator1: "iterator\UU\f\x = UU"
  apply (subst iterator_def2)
  apply simp
  done

lemma iterator2: "iterator\dzero\f\x = x"
  apply (subst iterator_def2)
  apply simp
  done

lemma iterator3: "n \ UU \ iterator\(dsucc\n)\f\x = f\(iterator\n\f\x)"
  apply (rule trans)
   apply (subst iterator_def2)
   apply simp
  apply (rule refl)
  done

lemmas iterator_rews = iterator1 iterator2 iterator3

lemma dnat_flat: "\x y::dnat. x \ y \ x = UU \ x = y"
  apply (rule allI)
  apply (induct_tac x)
    apply fast
   apply (rule allI)
   apply (case_tac y)
     apply simp
    apply simp
   apply simp
  apply (rule allI)
  apply (case_tac y)
    apply (fast intro!: bottomI)
   apply (thin_tac "\y. dnat \ y \ dnat = UU \ dnat = y")
   apply simp
  apply (simp (no_asm_simp))
  apply (drule_tac x="dnata" in spec)
  apply simp
  done

end

quality100%

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.