|
section \<open>Section 10.4\<close>
theory Ex1
imports "../LCF"
begin
axiomatization
P :: "'a \ tr" and
G :: "'a \ 'a" and
H :: "'a \ 'a" and
K :: "('a \ 'a) \ ('a \ 'a)"
where
P_strict: "P(UU) = UU" and
K: "K = (\h x. P(x) \ x | h(h(G(x))))" and
H: "H = FIX(K)"
declare P_strict [simp] K [simp]
lemma H_unfold: "H = K(H)"
apply (simplesubst H)
apply (rule FIX_eq [symmetric])
done
lemma H_strict [simp]: "H(UU)=UU"
apply (simplesubst H_unfold)
apply simp
done
lemma H_idemp_lemma: "\x. H(FIX(K,x)) = FIX(K,x)"
apply (induct K)
apply simp
apply (simp split: COND_cases_iff)
apply (intro strip)
apply (subst H_unfold)
apply simp
done
lemma H_idemp: "\x. H(H(x)) = H(x)"
apply (rule H_idemp_lemma [folded H])
done
end
¤ Dauer der Verarbeitung: 0.23 Sekunden
(vorverarbeitet)
¤
|
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.
|
