<commit_before>(*  Title:      HOL/Accessible_Part.thy
    ID:         $Id$
    Author:     <NAME>, Cambridge University Computer Laboratory
    Copyright   1994  University of Cambridge
*)

header {* The accessible part of a relation *}

theory Accessible_Part
imports Wellfounded_Recursion
begin

subsection {* Inductive definition *}

text {*
 Inductive definition of the accessible part @{term "acc r"} of a
 relation; see also \cite{paulin-tlca}.
*}

inductive_set
  acc :: "('a * 'a) set => 'a set"
  for r :: "('a * 'a) set"
  where
    accI: "(!!y. (y, x) : r ==> y : acc r) ==> x : acc r"

abbreviation
  termip :: "('a => 'a => bool) => 'a => bool" where
  "termip r == accp (r\<inverse>\<inverse>)"

abbreviation
  termi :: "('a * 'a) set => 'a set" where
  "termi r == acc (r\<inverse>)"


subsection {* Induction rules *}
<commit_msg>added lemma binding: accpI = accp.accI<commit_after>(*  Title:      HOL/Accessible_Part.thy
    ID:         $Id$
    Author:     <NAME>, Cambridge University Computer Laboratory
    Copyright   1994  University of Cambridge
*)

header {* The accessible part of a relation *}

theory Accessible_Part
imports Wellfounded_Recursion
begin

subsection {* Inductive definition *}

text {*
 Inductive definition of the accessible part @{term "acc r"} of a
 relation; see also \cite{paulin-tlca}.
*}

inductive_set
  acc :: "('a * 'a) set => 'a set"
  for r :: "('a * 'a) set"
  where
    accI: "(!!y. (y, x) : r ==> y : acc r) ==> x : acc r"

abbreviation
  termip :: "('a => 'a => bool) => 'a => bool" where
  "termip r == accp (r\<inverse>\<inverse>)"

abbreviation
  termi :: "('a * 'a) set => 'a set" where
  "termi r == acc (r\<inverse>)"

lemmas accpI = accp.accI

subsection {* Induction rules *}

{'fraction_non_alphanumeric': 0.15768348623853212, 'fraction_numerical': 0.0045871559633027525, 'mean_word_length': 3.2769607843137254, 'pattern_counts': {'":': 0, '<': 11, '<?xml version=': 0, '>': 27, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5973446', 'n_tokens_mistral': 648, 'n_tokens_neox': 621, 'n_words': 203}