1(* Title: ZF/Induct/Acc.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1994 University of Cambridge 4*) 5 6section \<open>The accessible part of a relation\<close> 7 8theory Acc imports ZF begin 9 10text \<open> 11 Inductive definition of \<open>acc(r)\<close>; see @{cite "paulin-tlca"}. 12\<close> 13 14consts 15 acc :: "i => i" 16 17inductive 18 domains "acc(r)" \<subseteq> "field(r)" 19 intros 20 vimage: "[| r-``{a}: Pow(acc(r)); a \<in> field(r) |] ==> a \<in> acc(r)" 21 monos Pow_mono 22 23text \<open> 24 The introduction rule must require \<^prop>\<open>a \<in> field(r)\<close>, 25 otherwise \<open>acc(r)\<close> would be a proper class! 26 27 \medskip 28 The intended introduction rule: 29\<close> 30 31lemma accI: "[| !!b. <b,a>:r ==> b \<in> acc(r); a \<in> field(r) |] ==> a \<in> acc(r)" 32 by (blast intro: acc.intros) 33 34lemma acc_downward: "[| b \<in> acc(r); <a,b>: r |] ==> a \<in> acc(r)" 35 by (erule acc.cases) blast 36 37lemma acc_induct [consumes 1, case_names vimage, induct set: acc]: 38 "[| a \<in> acc(r); 39 !!x. [| x \<in> acc(r); \<forall>y. <y,x>:r \<longrightarrow> P(y) |] ==> P(x) 40 |] ==> P(a)" 41 by (erule acc.induct) (blast intro: acc.intros) 42 43lemma wf_on_acc: "wf[acc(r)](r)" 44 apply (rule wf_onI2) 45 apply (erule acc_induct) 46 apply fast 47 done 48 49lemma acc_wfI: "field(r) \<subseteq> acc(r) \<Longrightarrow> wf(r)" 50 by (erule wf_on_acc [THEN wf_on_subset_A, THEN wf_on_field_imp_wf]) 51 52lemma acc_wfD: "wf(r) ==> field(r) \<subseteq> acc(r)" 53 apply (rule subsetI) 54 apply (erule wf_induct2, assumption) 55 apply (blast intro: accI)+ 56 done 57 58lemma wf_acc_iff: "wf(r) \<longleftrightarrow> field(r) \<subseteq> acc(r)" 59 by (rule iffI, erule acc_wfD, erule acc_wfI) 60 61end 62