Theory Finite_DCR_Hierarchy

(*     License:    LGPL  *)

section ‹Preliminaries›

subsection ‹Formal definition of finite levels of the DCR hierarchy›

theory Finite_DCR_Hierarchy
  imports Main
begin

subsubsection ‹Auxiliary definitions›

definition confl_rel
  where "confl_rel r ≡ (∀a b c. (a,b) ∈ r^* ∧ (a,c) ∈ r^* ⟶ (∃ d. (b,d) ∈ r^* ∧ (c,d) ∈ r^*) )"

definition jn00 :: "'a rel ⇒ 'a ⇒ 'a ⇒ bool"
where
  "jn00 r0 b c ≡ (∃ d. (b,d) ∈ r0^= ∧ (c,d) ∈ r0^=)"

definition jn01 :: "'a rel ⇒ 'a rel ⇒ 'a ⇒ 'a ⇒ bool"
where
  "jn01 r0 r1 b c ≡ (∃b' d. (b,b') ∈ r1^= ∧ (b',d) ∈ r0^* ∧ (c,d) ∈ r0^*)"

definition jn10 :: "'a rel ⇒ 'a rel ⇒ 'a ⇒ 'a ⇒ bool"
where
  "jn10 r0 r1 b c ≡ (∃c' d. (b,d) ∈ r0^* ∧ (c,c') ∈ r1^= ∧ (c',d) ∈ r0^*)"

definition jn11 :: "'a rel ⇒ 'a rel ⇒ 'a ⇒ 'a ⇒ bool"
where
  "jn11 r0 r1 b c ≡ (∃b' b'' c' c'' d.  (b,b') ∈ r0^* ∧ (b',b'') ∈ r1^= ∧ (b'',d) ∈ r0^* 
                                          ∧ (c,c') ∈ r0^* ∧ (c',c'') ∈ r1^= ∧ (c'',d) ∈ r0^*)"

definition jn02 :: "'a rel ⇒ 'a rel ⇒ 'a rel ⇒ 'a ⇒ 'a ⇒ bool"
where
  "jn02 r0 r1 r2 b c ≡ (∃b' d.  (b,b') ∈ r2^= ∧ (b',d) ∈ (r0 ∪ r1)^* ∧ (c,d) ∈ (r0 ∪ r1)^* )"

definition jn12 :: "'a rel ⇒ 'a rel ⇒ 'a rel ⇒ 'a ⇒ 'a ⇒ bool"
where
  "jn12 r0 r1 r2 b c ≡ (∃b' b'' d.  (b,b') ∈ (r0)^* ∧ (b',b'') ∈ r2^= ∧ (b'',d) ∈ (r0 ∪ r1)^* 
                                          ∧ (c,d) ∈ (r0 ∪ r1)^*)"

definition jn22 :: "'a rel ⇒ 'a rel ⇒ 'a rel ⇒ 'a ⇒ 'a ⇒ bool"
where
  "jn22 r0 r1 r2 b c ≡ (∃b' b'' c' c'' d.  (b,b') ∈ (r0 ∪ r1)^* ∧ (b',b'') ∈ r2^= ∧ (b'',d) ∈ (r0 ∪ r1)^* 
                                          ∧ (c,c') ∈ (r0 ∪ r1)^* ∧ (c',c'') ∈ r2^= ∧ (c'',d) ∈ (r0 ∪ r1)^*)"

definition LD2 :: "'a rel ⇒ 'a rel ⇒ 'a rel ⇒ bool"
where
  "LD2 r r0 r1 ≡ ( r = r0 ∪ r1 
              ∧ (∀ a b c. (a,b) ∈ r0 ∧ (a,c) ∈ r0 ⟶ jn00 r0 b c)
              ∧ (∀ a b c. (a,b) ∈ r0 ∧ (a,c) ∈ r1 ⟶ jn01 r0 r1 b c)
              ∧ (∀ a b c. (a,b) ∈ r1 ∧ (a,c) ∈ r1 ⟶ jn11 r0 r1 b c) )"

definition LD3 :: "'a rel ⇒ 'a rel ⇒ 'a rel ⇒ 'a rel ⇒ bool"
where
  "LD3 r r0 r1 r2 ≡ ( r = r0 ∪ r1 ∪ r2
              ∧ (∀ a b c. (a,b) ∈ r0 ∧ (a,c) ∈ r0 ⟶ jn00 r0 b c)
              ∧ (∀ a b c. (a,b) ∈ r0 ∧ (a,c) ∈ r1 ⟶ jn01 r0 r1 b c)
              ∧ (∀ a b c. (a,b) ∈ r1 ∧ (a,c) ∈ r1 ⟶ jn11 r0 r1 b c)
              ∧ (∀ a b c. (a,b) ∈ r0 ∧ (a,c) ∈ r2 ⟶ jn02 r0 r1 r2 b c)
              ∧ (∀ a b c. (a,b) ∈ r1 ∧ (a,c) ∈ r2 ⟶ jn12 r0 r1 r2 b c)
              ∧ (∀ a b c. (a,b) ∈ r2 ∧ (a,c) ∈ r2 ⟶ jn22 r0 r1 r2 b c))"

definition DCR2 :: "'a rel ⇒ bool"
where
  "DCR2 r ≡ ( ∃r0 r1. LD2 r r0 r1 )"

definition DCR3 :: "'a rel ⇒ bool"
where
  "DCR3 r ≡ ( ∃r0 r1 r2. LD3 r r0 r1 r2 )"

definition 𝔏1 :: "(nat ⇒ 'U rel) ⇒ nat ⇒ 'U rel"
where
  "𝔏1 g α ≡ ⋃ {A. ∃ α'. (α' < α) ∧ A = g α'}"

definition 𝔏v :: "(nat ⇒ 'U rel) ⇒ nat ⇒ nat ⇒ 'U rel"
where
  "𝔏v g α β ≡ ⋃ {A. ∃ α'. (α' < α ∨ α' < β) ∧ A = g α'}"

definition 𝔇 :: "(nat ⇒ 'U rel) ⇒ nat ⇒ nat ⇒ ('U × 'U × 'U × 'U) set"
where
  "𝔇 g α β = {(b,b',b'',d). (b,b') ∈ (𝔏1 g α)^* ∧ (b',b'') ∈ (g β)^= ∧ (b'',d) ∈ (𝔏v g α β)^*}"

definition DCR_generating :: "(nat ⇒ 'U rel) ⇒ bool"
where
  "DCR_generating g ≡ (∀ α β a b c. (a,b) ∈ (g α) ∧ (a,c) ∈ (g β)
             ⟶  (∃ b' b'' c' c'' d. (b,b',b'',d) ∈ (𝔇 g α β) ∧ (c,c',c'',d) ∈ (𝔇 g β α) ))"

subsubsection ‹Result›

text ‹The next definition formalizes the condition ``an ARS with a reduction relation $r$ belongs to the class $DCR_n$'', where $n$ is a natural number.›

definition DCR :: "nat ⇒ 'U rel ⇒ bool"
where
  "DCR n r ≡ (∃ g::(nat ⇒ 'U rel). DCR_generating g ∧ r = ⋃ { r'. ∃ α'. α' < n ∧ r' = g α' } )"

end