(* Title: ZF/Induct/Acc.thy Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge \<open>The accessible part of a relation\<close> theory Acc imports ZF begin text \<open> Inductive definition of \<open>acc(r)\<close>; see \<^cite>\<open>"paulin-tlca"\<close>. \<close> consts "i \ i" inductive "acc(r)" \<subseteq> "field(r)" intros "\r-``{a}: Pow(acc(r)); a \ field(r)\ \ a \ acc(r)" monos Pow_monotext \<open> \<^prop>\<open>a \<in> field(r)\<close>, otherwise \<open>acc(r)\<close> would be a proper class! \medskip \<close> lemma accI: "\\b. \b,a\:r \ b \ acc(r); a \ field(r)\ \ a \ acc(r)" by (blast intro: acc.intros )lemma acc_downward: "\b \ acc(r); \a,b\: r\ \ a \ acc(r)" by (erule acc.cases) blastlemma acc_induct [consumes 1, case_names vimage, induct set: acc]:"\a \ acc(r); \<And>x. \<lbrakk>x \<in> acc(r); \<forall>y. \<langle>y,x\<rangle>:r \<longrightarrow> P(y)\<rbrakk> \<Longrightarrow> P(x) \<rbrakk> \<Longrightarrow> 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 fastdone lemma acc_wfI: "field(r) \ acc(r) \ wf(r)" by (erule wf_on_acc [THEN wf_on_subset_A, THEN wf_on_field_imp_wf])lemma acc_wfD: "wf(r) \ field(r) \ acc(r)" apply (rule subsetI)apply (erule wf_induct2, assumption)apply (blast intro: accI)+done lemma wf_acc_iff: "wf(r) \ field(r) \ acc(r)" by (rule iffI, erule acc_wfD, erule acc_wfI)end quality 96%
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
