Theory Syntactic_Criteria

section ‹Syntactic Criteria›
theory Syntactic_Criteria
  imports Compositionality
begin

context PL_Indis
begin

lemma proper_intros[intro]:
  "proper Done"
  "proper (Atm atm)"
  "proper c1 ⟹ proper c2 ⟹ proper (Seq c1 c2)"
  "proper c1 ⟹ proper c2 ⟹ proper (Ch ch c1 c2)"
  "proper c ⟹ proper (While tst c)"
  "properL cs ⟹ proper (Par cs)"
  "properL cs ⟹ proper (ParT cs)"
  "(⋀c. c ∈ set cs ⟹ proper c) ⟹ cs ≠ [] ⟹ properL cs"
  by auto

lemma discr:
  "discr Done"
  "presAtm atm ⟹ discr (Atm atm)"
  "discr c1 ⟹ discr c2 ⟹ discr (Seq c1 c2)"
  "discr c1 ⟹ discr c2 ⟹ discr (Ch ch c1 c2)"
  "discr c ⟹ discr (While tst c)"
  "properL cs ⟹ (⋀c. c ∈ set cs ⟹ discr c) ⟹ discr (Par cs)"
  "properL cs ⟹ (⋀c. c ∈ set cs ⟹ discr c) ⟹ discr (ParT cs)"
  by (auto intro!: discr_Par discr_ParT)

lemma siso:
  "compatAtm atm ⟹ siso (Atm atm)"
  "siso c1 ⟹ siso c2 ⟹ siso (Seq c1 c2)"
  "compatCh ch ⟹ siso c1 ⟹ siso c2 ⟹ siso (Ch ch c1 c2)"
  "compatTst tst ⟹ siso c ⟹ siso (While tst c)"
  "properL cs ⟹ (⋀c. c ∈ set cs ⟹ siso c) ⟹ siso (Par cs)"
  "properL cs ⟹ (⋀c. c ∈ set cs ⟹ siso c) ⟹ siso (ParT cs)"
  by (auto intro!: siso_Par siso_ParT)

lemma Sbis:
  "compatAtm atm ⟹ Atm atm ≈s Atm atm"
  "siso c1 ⟹ c2 ≈s c2 ⟹ Seq c1 c2 ≈s Seq c1 c2"
  "proper c1 ⟹ proper c2 ⟹ c1 ≈s c1 ⟹ discr c2 ⟹ Seq c1 c2 ≈s Seq c1 c2"
  "compatCh ch ⟹ c1 ≈s c1 ⟹ c2 ≈s c2 ⟹ Ch ch c1 c2 ≈s Ch ch c1 c2"
  "properL cs ⟹ (⋀c. c ∈ set cs ⟹ c ≈s c) ⟹ Par cs ≈s Par cs"
  by (auto intro!: Par_Sbis)

lemma ZObis:
  "compatAtm atm ⟹ Atm atm ≈01 Atm atm"
  "siso c1 ⟹ c2 ≈01 c2 ⟹ Seq c1 c2 ≈01 Seq c1 c2"
  "proper c1 ⟹ proper c2 ⟹ c1 ≈01 c1 ⟹ discr c2 ⟹ Seq c1 c2 ≈01 Seq c1 c2"
  "compatCh ch ⟹ c1 ≈01 c1 ⟹ c2 ≈01 c2 ⟹ Ch ch c1 c2 ≈01 Ch ch c1 c2"
  "properL cs ⟹ (⋀c. c ∈ set cs ⟹ c ≈s c) ⟹ ParT cs ≈01 ParT cs"
  by (auto intro!: ParT_ZObis)

lemma discr_imp_Sbis: "proper c ⟹ discr c ⟹ c ≈s c"
  by auto

lemma siso_imp_Sbis: "siso c ⟹ c ≈s c"
  by auto

lemma Sbis_imp_ZObis: "c ≈s c ⟹ c ≈01 c"
  by auto


(* The syntactic predicates: SC_φ corresponds to the paper's overlined φ: *) 

fun SC_discr where
  "SC_discr Done          ⟷ True"
| "SC_discr (Atm atm)     ⟷ presAtm atm"
| "SC_discr (Seq c1 c2)   ⟷ SC_discr c1 ∧ SC_discr c2"
| "SC_discr (Ch ch c1 c2) ⟷ SC_discr c1 ∧ SC_discr c2"
| "SC_discr (While tst c) ⟷ SC_discr c"
| "SC_discr (ParT cs) ⟷ (∀c∈set cs. SC_discr c)"
| "SC_discr (Par cs)  ⟷ (∀c∈set cs. SC_discr c)"

theorem SC_discr_discr[intro]: "proper c ⟹ SC_discr c ⟹ discr c"
  by (induct c) (auto intro!: discr)

fun SC_siso where
  "SC_siso Done           ⟷ True"
| "SC_siso (Atm atm)      ⟷ compatAtm atm"
| "SC_siso (Seq c1 c2)    ⟷ SC_siso c1 ∧ SC_siso c2"
| "SC_siso (Ch ch c1 c2)  ⟷ compatCh ch ∧ SC_siso c1 ∧ SC_siso c2"
| "SC_siso (While tst c)  ⟷ compatTst tst ∧ SC_siso c"
| "SC_siso (Par cs)   ⟷ (∀c∈set cs. SC_siso c)"
| "SC_siso (ParT cs)  ⟷ (∀c∈set cs. SC_siso c)"

theorem SC_siso_siso[intro]: "proper c ⟹ SC_siso c ⟹ siso c"
  by (induct c) (auto intro!: siso)

fun SC_Sbis where
  "SC_Sbis Done           ⟷ True"
| "SC_Sbis (Atm atm)      ⟷ compatAtm atm"
| "SC_Sbis (Seq c1 c2)    ⟷ (SC_siso c1 ∧ SC_Sbis c2) ∨
                             (SC_Sbis c1 ∧ SC_discr c2) ∨
                             SC_discr (Seq c1 c2) ∨ SC_siso (Seq c1 c2)"
| "SC_Sbis (Ch ch c1 c2)  ⟷ (if compatCh ch
                             then SC_Sbis c1 ∧ SC_Sbis c2
                             else (SC_discr (Ch ch c1 c2) ∨ SC_siso (Ch ch c1 c2)))"
| "SC_Sbis (While tst c)  ⟷ SC_discr (While tst c) ∨ SC_siso (While tst c)"
| "SC_Sbis (Par cs)   ⟷ (∀c∈set cs. SC_Sbis c)"
| "SC_Sbis (ParT cs)  ⟷ SC_siso (ParT cs) ∨ SC_discr (ParT cs)"

theorem SC_siso_SCbis[intro]: "SC_siso c ⟹ SC_Sbis c"
  by (induct c) auto

theorem SC_discr_SCbis[intro]: "SC_discr c ⟹ SC_Sbis c"
  by (induct c) auto

declare SC_siso.simps[simp del]

declare SC_discr.simps[simp del]

theorem SC_Sbis_Sbis[intro]: "proper c ⟹ SC_Sbis c ⟹ c ≈s c"
  by (induct c)
     (auto intro: Sbis discr_imp_Sbis siso_imp_Sbis
           split: if_split_asm)

fun SC_ZObis where
  "SC_ZObis Done           ⟷ True"
| "SC_ZObis (Atm atm)      ⟷ compatAtm atm"
| "SC_ZObis (Seq c1 c2)    ⟷ (SC_siso c1 ∧ SC_ZObis c2) ∨
                             (SC_ZObis c1 ∧ SC_discr c2) ∨
                             SC_Sbis (Seq c1 c2)"
| "SC_ZObis (Ch ch c1 c2)  ⟷ (if compatCh ch
                             then SC_ZObis c1 ∧ SC_ZObis c2
                             else SC_Sbis (Ch ch c1 c2))"
| "SC_ZObis (While tst c)  ⟷ SC_Sbis (While tst c)"
| "SC_ZObis (Par cs)   ⟷ SC_Sbis (Par cs)"
| "SC_ZObis (ParT cs)  ⟷ (∀c∈set cs. SC_Sbis c)"

theorem SC_Sbis_SC_ZObis[intro]: "SC_Sbis c ⟹ SC_ZObis c"
  by (induct c) (auto simp: SC_siso.simps SC_discr.simps)

declare SC_Sbis.simps[simp del]

theorem SC_ZObis_ZObis: "proper c ⟹ SC_ZObis c ⟹ c ≈01 c"
  apply (induct c)
  apply (auto intro: Sbis_imp_ZObis ZObis split: if_split_asm)
  apply (auto intro!: ZObis(5))
  done

end

end