(* Title: HOLCF/Dnat.thy ID: $Id: Dnat.thy,v 1.6 2005/06/17 14:15:09 haftmann Exp $ Author: Franz Regensburger Theory for the domain of natural numbers dnat = one ++ dnat *) theory Dnat imports HOLCF begin domain dnat = dzero | dsucc (dpred :: dnat) constdefs iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a" "iterator == fix $ (LAM h n f x. case n of dzero => x | dsucc $ m => f $ (h $ m $ f $ x))" text {* \medskip Expand fixed point properties. *} ML_setup {* bind_thm ("iterator_def2", fix_prover2 (the_context ()) (thm "iterator_def") "iterator = (LAM n f x. case n of dzero => x | dsucc$m => f$(iterator$m$f$x))"); *} text {* \medskip Recursive properties. *} lemma iterator1: "iterator $ UU $ f $ x = UU" apply (subst iterator_def2) apply (simp add: dnat.rews) done lemma iterator2: "iterator $ dzero $ f $ x = x" apply (subst iterator_def2) apply (simp add: dnat.rews) done lemma iterator3: "n ~= UU ==> iterator $ (dsucc $ n) $ f $ x = f $ (iterator $ n $ f $ x)" apply (rule trans) apply (subst iterator_def2) apply (simp add: dnat.rews) apply (rule refl) done lemmas iterator_rews = iterator1 iterator2 iterator3 lemma dnat_flat: "ALL x y::dnat. x<<y --> x=UU | x=y" apply (rule allI) apply (induct_tac x rule: dnat.ind) apply fast apply (rule allI) apply (rule_tac x = y in dnat.casedist) apply (fast intro!: UU_I) apply simp apply (simp add: dnat.dist_les) apply (rule allI) apply (rule_tac x = y in dnat.casedist) apply (fast intro!: UU_I) apply (simp add: dnat.dist_les) apply (simp (no_asm_simp) add: dnat.rews) apply (intro strip) apply (subgoal_tac "d << da") apply (erule allE) apply (drule mp) apply assumption apply (erule disjE) apply (tactic "contr_tac 1") apply simp apply (erule (1) dnat.inverts) done end
theorem iterator_def2:
iterator = (LAM n f x. case n of dzero => x | dsucc·m => f·(iterator·m·f·x))
lemma iterator1:
iterator·UU·f·x = UU
lemma iterator2:
iterator·dzero·f·x = x
lemma iterator3:
n ≠ UU ==> iterator·(dsucc·n)·f·x = f·(iterator·n·f·x)
lemmas iterator_rews:
iterator·UU·f·x = UU
iterator·dzero·f·x = x
n ≠ UU ==> iterator·(dsucc·n)·f·x = f·(iterator·n·f·x)
lemmas iterator_rews:
iterator·UU·f·x = UU
iterator·dzero·f·x = x
n ≠ UU ==> iterator·(dsucc·n)·f·x = f·(iterator·n·f·x)
lemma dnat_flat:
∀x y. x << y --> x = UU ∨ x = y