Up to index of Isabelle/HOL/HOL-Complex/ex
theory Accessible_Part(* Title: HOL/Library/Accessible_Part.thy ID: $Id: Accessible_Part.thy,v 1.6 2004/08/18 09:10:01 nipkow Exp $ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge *) header {* The accessible part of a relation *} theory Accessible_Part imports Main begin subsection {* Inductive definition *} text {* Inductive definition of the accessible part @{term "acc r"} of a relation; see also \cite{paulin-tlca}. *} consts acc :: "('a × 'a) set => 'a set" inductive "acc r" intros accI: "(!!y. (y, x) ∈ r ==> y ∈ acc r) ==> x ∈ acc r" syntax termi :: "('a × 'a) set => 'a set" translations "termi r" == "acc (r¯)" subsection {* Induction rules *} theorem acc_induct: "a ∈ acc r ==> (!!x. x ∈ acc r ==> ∀y. (y, x) ∈ r --> P y ==> P x) ==> P a" proof - assume major: "a ∈ acc r" assume hyp: "!!x. x ∈ acc r ==> ∀y. (y, x) ∈ r --> P y ==> P x" show ?thesis apply (rule major [THEN acc.induct]) apply (rule hyp) apply (rule accI) apply fast apply fast done qed theorems acc_induct_rule = acc_induct [rule_format, induct set: acc] theorem acc_downward: "b ∈ acc r ==> (a, b) ∈ r ==> a ∈ acc r" apply (erule acc.elims) apply fast done lemma acc_downwards_aux: "(b, a) ∈ r* ==> a ∈ acc r --> b ∈ acc r" apply (erule rtrancl_induct) apply blast apply (blast dest: acc_downward) done theorem acc_downwards: "a ∈ acc r ==> (b, a) ∈ r* ==> b ∈ acc r" apply (blast dest: acc_downwards_aux) done theorem acc_wfI: "∀x. x ∈ acc r ==> wf r" apply (rule wfUNIVI) apply (induct_tac P x rule: acc_induct) apply blast apply blast done theorem acc_wfD: "wf r ==> x ∈ acc r" apply (erule wf_induct) apply (rule accI) apply blast done theorem wf_acc_iff: "wf r = (∀x. x ∈ acc r)" apply (blast intro: acc_wfI dest: acc_wfD) done end
theorem acc_induct:
[| a ∈ acc r; !!x. [| x ∈ acc r; ∀y. (y, x) ∈ r --> P y |] ==> P x |] ==> P a
theorems acc_induct_rule:
[| a ∈ acc r; !!x. [| x ∈ acc r; !!y. (y, x) ∈ r ==> P y |] ==> P x |] ==> P a
theorems acc_induct_rule:
[| a ∈ acc r; !!x. [| x ∈ acc r; !!y. (y, x) ∈ r ==> P y |] ==> P x |] ==> P a
theorem acc_downward:
[| b ∈ acc r; (a, b) ∈ r |] ==> a ∈ acc r
lemma acc_downwards_aux:
(b, a) ∈ r* ==> a ∈ acc r --> b ∈ acc r
theorem acc_downwards:
[| a ∈ acc r; (b, a) ∈ r* |] ==> b ∈ acc r
theorem acc_wfI:
∀x. x ∈ acc r ==> wf r
theorem acc_wfD:
wf r ==> x ∈ acc r
theorem wf_acc_iff:
wf r = (∀x. x ∈ acc r)