| products/sources/formale sprachen/Isabelle/ZF/Induct/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: weighted_digraphs.prf Sprache: IsabelleOriginal von: Isabelle© |
|
||||||
|
(* Title: ZF/Induct/Acc.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge *) section \<open>The accessible part of a relation\<close> theory Acc imports ZF begin text \<open> Inductive definition of \<open>acc(r)\<close>; see @{cite "paulin-tlca"}. \<close> consts acc :: "i => i" inductive domains "acc(r)" \<subseteq> "field(r)" intros vimage: "[| r-``{a}: Pow(acc(r)); a \ monos Pow_mono text \<open> The introduction rule must require \<^prop>\<open>a \<in> field(r)\<close>, otherwise \<open>acc(r)\<close> would be a proper class! \medskip The intended introduction rule: \<close> lemma accI: "[| !!b. by (blast intro: acc.intros) lemma acc_downward: "[| b \ by (erule acc.cases) blast lemma acc_induct [consumes 1, case_names vimage, induct set: acc]: "[| a \ !!x. [| x \<in> acc(r); \<forall>y. <y,x>:r \<longrightarrow> P(y) |] ==> P(x) |] ==> P(a)" by (erule acc.induct) (blast intro: acc.intros) lemma wf_on_acc: "wf[acc(r)](r)" apply (rule wf_onI2) apply (erule acc_induct) apply fast done lemma acc_wfI: "field(r) \ by (erule wf_on_acc [THEN wf_on_subset_A, THEN wf_on_field_imp_wf]) lemma acc_wfD: "wf(r) ==> field(r) \ apply (rule subsetI) apply (erule wf_induct2, assumption) apply (blast intro: accI)+ done lemma wf_acc_iff: "wf(r) \ by (rule iffI, erule acc_wfD, erule acc_wfI) end ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
