Quelle Acc.thy Sprache: 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>\<open>"paulin-tlca"\<close>.
\<close>

consts
  acc :: "i \ i"

inductive
  domains "acc(r)" \<subseteq> "field(r)"
  intros
    vimage:  "\r-``{a}: Pow(acc(r)); a \ field(r)\ \ a \ acc(r)"
  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. \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) blast

lemma 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 fast
  done

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

quality96%

¤ Dauer der Verarbeitung: 0.1 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.