Theory During_Execution

section ‹During-execution security› 

theory During_Execution 
imports Bisim Language_Semantics begin


subsection ‹Basic setting›

locale PL_Indis = PL tval aval 
  for 
    tval :: "'test ⇒ 'state ⇒ bool" and 
    aval :: "'atom ⇒ 'state ⇒ 'state"
  +
  fixes 
    indis :: "'state rel" 
  assumes 
    equiv_indis: "equiv UNIV indis" 
    

(*******************************************)
context PL_Indis 
begin 

abbreviation indisAbbrev (infix "≈" 50)
where "s1 ≈ s2 ≡ (s1,s2) ∈ indis"

definition indisE (infix "≈e" 50) where 
"se1 ≈e se2 ≡ 
 case (se1,se2) of 
   (Inl s1, Inl s2) ⇒ s1 ≈ s2
  |(Inr err1, Inr err2) ⇒ err1 = err2"

lemma refl_indis: "refl indis"
and trans_indis: "trans indis"
and sym_indis: "sym indis"
using equiv_indis unfolding equiv_def by auto

lemma indis_refl[intro]: "s ≈ s"
using refl_indis unfolding refl_on_def by simp

lemma indis_trans: "⟦s ≈ s'; s' ≈ s''⟧ ⟹ s ≈ s''"
using trans_indis unfolding trans_def by blast

lemma indis_sym: "s ≈ s' ⟹ s' ≈ s"
using sym_indis unfolding sym_def by blast


subsection‹Compatibility and discreetness› 

definition compatTst where 
"compatTst tst ≡ 
 ∀ s t. s ≈ t ⟶ tval tst s = tval tst t"

definition compatAtm where 
"compatAtm atm ≡ 
 ∀ s t. s ≈ t ⟶ aval atm s ≈ aval atm t"

(* ≈-preservation: *)
definition presAtm where 
"presAtm atm ≡ 
 ∀ s. s ≈ aval atm s"

coinductive discr where 
intro: 
"⟦⋀ s c' s'. (c,s) →c (c',s') ⟹ s ≈ s' ∧ discr c'; 
  ⋀ s s'. (c,s) →t s' ⟹ s ≈ s'⟧ 
  ⟹ discr c"

lemma presAtm_compatAtm[simp]:
assumes "presAtm atm"
shows "compatAtm atm"
using assms unfolding compatAtm_def
by (metis presAtm_def indis_sym indis_trans)

text‹Coinduction for discreetness:›

lemma discr_coind:
assumes *: "phi c" and 
**: "⋀ c s c' s'. ⟦phi c; (c,s) →c (c',s')⟧ ⟹ s ≈ s' ∧ (phi c' ∨ discr c')" and 
***: "⋀ c s s'. ⟦phi c; (c,s) →t s'⟧ ⟹ s ≈ s'"
shows "discr c"
using * apply - apply(erule discr.coinduct) using ** *** by auto

lemma discr_raw_coind:
assumes *: "phi c" and 
**: "⋀ c s c' s'. ⟦phi c; (c,s) →c (c',s')⟧ ⟹ s ≈ s' ∧ phi c'" and 
***: "⋀ c s s'. ⟦phi c; (c,s) →t s'⟧ ⟹ s ≈ s'"
shows "discr c"
using * apply - apply(erule discr_coind) using ** *** by blast+

text‹Discreetness versus transition:›

lemma discr_transC:
assumes *: "discr c" and **: "(c,s) →c (c',s')"
shows "discr c'"
using * apply - apply(erule discr.cases) using ** by blast

lemma discr_MtransC:
assumes "discr c" and "(c,s) →*c (c',s')"
shows "discr c'"
proof-
  have "(c,s) →*c (c',s') ⟹ discr c ⟶ discr c'"
  apply(erule MtransC_induct2) using discr_transC by blast+
  thus ?thesis using assms by blast
qed

lemma discr_transC_indis:
assumes *: "discr c" and **: "(c,s) →c (c',s')"
shows "s ≈ s'"
using * apply - apply(erule discr.cases) using ** by blast

lemma discr_MtransC_indis:
assumes "discr c" and "(c,s) →*c (c',s')"
shows "s ≈ s'"
proof-
  have "(c,s) →*c (c',s') ⟹ discr c ⟶ s ≈ s'"
  apply(erule MtransC_induct2)
  apply (metis indis_refl)
  by (metis discr.cases discr_MtransC indis_trans)
  thus ?thesis using assms by blast
qed

lemma discr_transT:
assumes *: "discr c" and **: "(c,s) →t s'"
shows "s ≈ s'"
using * apply - apply(erule discr.cases) using ** by blast

lemma discr_MtransT:
assumes *: "discr c" and **: "(c,s) →*t s'"
shows "s ≈ s'"
proof-
  obtain d' t' where 
  cs: "(c,s) →*c (d',t')" and d't': "(d',t') →t s'"
  using ** by(rule MtransT_invert2)
  hence "s ≈ t'" using * discr_MtransC_indis by blast
  moreover 
  {have "discr d'" using cs * discr_MtransC by blast 
   hence "t' ≈ s'" using d't' discr_transT by blast
  }
  ultimately show ?thesis using indis_trans by blast
qed 


subsection‹Terminating-interctive discreetness›

coinductive discr0 where 
intro: 
"⟦⋀ s c' s'. ⟦mustT c s; (c,s) →c (c',s')⟧ ⟹ s ≈ s' ∧ discr0 c'; 
  ⋀ s s'. ⟦mustT c s; (c,s) →t s'⟧ ⟹ s ≈ s'⟧ 
  ⟹ discr0 c" 

text‹Coinduction for 0-discreetness:›

lemma discr0_coind[consumes 1, case_names Cont Term, induct pred: discr0]:
assumes *: "phi c" and 
**: "⋀ c s c' s'. 
       ⟦mustT c s; phi c; (c,s) →c (c',s')⟧ ⟹ 
       s ≈ s' ∧ (phi c' ∨ discr0 c')" and 
***: "⋀ c s s'. ⟦mustT c s; phi c; (c,s) →t s'⟧ ⟹ s ≈ s'"
shows "discr0 c"
using * apply - apply(erule discr0.coinduct) using ** *** by auto

lemma discr0_raw_coind[consumes 1, case_names Cont Term]:
assumes *: "phi c" and 
**: "⋀ c s c' s'. ⟦mustT c s; phi c; (c,s) →c (c',s')⟧ ⟹ s ≈ s' ∧ phi c'" and 
***: "⋀ c s s'. ⟦mustT c s; phi c; (c,s) →t s'⟧ ⟹ s ≈ s'"
shows "discr0 c"
using * apply - apply(erule discr0_coind) using ** *** by blast+

text‹0-Discreetness versus transition:›

lemma discr0_transC:
assumes *: "discr0 c" and **: "mustT c s" "(c,s) →c (c',s')"
shows "discr0 c'"
using * apply - apply(erule discr0.cases) using ** by blast

lemma discr0_MtransC:
assumes "discr0 c" and "mustT c s" "(c,s) →*c (c',s')"
shows "discr0 c'"
proof-
  have "(c,s) →*c (c',s') ⟹ mustT c s ∧ discr0 c ⟶ discr0 c'"
  apply(erule MtransC_induct2) using discr0_transC mustT_MtransC
  by blast+
  thus ?thesis using assms by blast
qed

lemma discr0_transC_indis:
assumes *: "discr0 c" and **: "mustT c s" "(c,s) →c (c',s')"
shows "s ≈ s'"
using * apply - apply(erule discr0.cases) using ** by blast

lemma discr0_MtransC_indis:
assumes "discr0 c" and "mustT c s" "(c,s) →*c (c',s')"
shows "s ≈ s'"
proof-
  have "(c,s) →*c (c',s') ⟹ mustT c s ∧ discr0 c ⟶ s ≈ s'"
  apply(erule MtransC_induct2)
  apply (metis indis_refl)
  by (metis discr0_MtransC discr0_transC_indis indis_trans mustT_MtransC)
  thus ?thesis using assms by blast
qed

lemma discr0_transT:
assumes *: "discr0 c" and **: "mustT c s" "(c,s) →t s'"
shows "s ≈ s'"
using * apply - apply(erule discr0.cases) using ** by blast

lemma discr0_MtransT:
assumes *: "discr0 c" and ***: "mustT c s" and **: "(c,s) →*t s'"
shows "s ≈ s'"
proof-
  obtain d' t' where 
  cs: "(c,s) →*c (d',t')" and d't': "(d',t') →t s'"
  using ** by(rule MtransT_invert2)
  hence "s ≈ t'" using * discr0_MtransC_indis *** by blast
  moreover 
  {have "discr0 d'" using cs * discr0_MtransC *** by blast 
   hence "t' ≈ s'"
   using *** by (metis mustT_MtransC cs d't' discr0_transT) 
  }
  ultimately show ?thesis using indis_trans by blast
qed 

lemma discr_discr0[simp]: "discr c ⟹ discr0 c"
  by (induct rule: discr0_coind)
     (metis discr_transC discr_transC_indis discr_transT)+

subsection‹Self-isomorphism›  

coinductive siso where 
intro: 
"⟦⋀ s c' s'. (c,s) →c (c',s') ⟹ siso c'; 
  ⋀ s t c' s'. ⟦s ≈ t; (c,s) →c (c',s')⟧ ⟹ ∃ t'. s' ≈ t' ∧ (c,t) →c (c',t');
  ⋀ s t s'. ⟦s ≈ t; (c,s) →t s'⟧ ⟹ ∃ t'. s' ≈ t' ∧ (c,t) →t t'⟧ 
  ⟹ siso c"

text‹Coinduction for self-isomorphism:›

lemma siso_coind:
assumes *: "phi c" and 
**: "⋀ c s c' s'. ⟦phi c; (c,s) →c (c',s')⟧ ⟹ phi c' ∨ siso c'" and 
***: "⋀ c s t c' s'. ⟦phi c; s ≈ t; (c,s) →c (c',s')⟧ ⟹ ∃ t'. s' ≈ t' ∧ (c,t) →c (c',t')" and 
****: "⋀ c s t s'. ⟦phi c; s ≈ t; (c,s) →t s'⟧ ⟹ ∃ t'. s' ≈ t' ∧ (c,t) →t t'"
shows "siso c"
using * apply - apply(erule siso.coinduct) using ** *** **** by auto

lemma siso_raw_coind:
assumes *: "phi c" and 
**: "⋀ c s c' s'. ⟦phi c; (c,s) →c (c',s')⟧ ⟹ phi c'" and 
***: "⋀ c s t c' s'. ⟦phi c; s ≈ t; (c,s) →c (c',s')⟧ ⟹ ∃ t'. s' ≈ t' ∧ (c,t) →c (c',t')" and 
****: "⋀ c s t s'. ⟦phi c; s ≈ t; (c,s) →t s'⟧ ⟹ ∃ t'. s' ≈ t' ∧ (c,t) →t t'"
shows "siso c"
using * apply - apply(erule siso_coind) using ** *** **** by blast+

text‹Self-Isomorphism versus transition:›

lemma siso_transC:
assumes *: "siso c" and **: "(c,s) →c (c',s')"
shows "siso c'"
using * apply - apply(erule siso.cases) using ** by blast

lemma siso_MtransC:
assumes "siso c" and "(c,s) →*c (c',s')"
shows "siso c'"
proof-
  have "(c,s) →*c (c',s') ⟹ siso c ⟶ siso c'"
  apply(erule MtransC_induct2) using siso_transC by blast+
  thus ?thesis using assms by blast
qed

lemma siso_transC_indis:
assumes *: "siso c" and **: "(c,s) →c (c',s')" and ***: "s ≈ t"
shows "∃ t'. s' ≈ t' ∧ (c,t) →c (c',t')"
using * apply - apply(erule siso.cases) using ** *** by blast

lemma siso_transT:
assumes *: "siso c" and **: "(c,s) →t s'" and ***: "s ≈ t"
shows "∃ t'. s' ≈ t' ∧ (c,t) →t t'"
using * apply - apply(erule siso.cases) using ** *** by blast


subsection‹MustT-interactive self-isomorphism›  

coinductive siso0 where 
intro: 
"⟦⋀ s c' s'. ⟦mustT c s; (c,s) →c (c',s')⟧ ⟹ siso0 c'; 
  ⋀ s t c' s'. 
    ⟦mustT c s; mustT c t; s ≈ t; (c,s) →c (c',s')⟧ ⟹ 
    ∃ t'. s' ≈ t' ∧ (c,t) →c (c',t');
  ⋀ s t s'. 
    ⟦mustT c s; mustT c t; s ≈ t; (c,s) →t s'⟧ ⟹ 
    ∃ t'. s' ≈ t' ∧ (c,t) →t t'⟧ 
  ⟹ siso0 c"

text‹Coinduction for self-isomorphism:›

lemma siso0_coind[consumes 1, case_names Indef Cont Term, induct pred: discr0]:
assumes *: "phi c" and 
**: "⋀ c s c' s'. ⟦phi c; mustT c s; (c,s) →c (c',s')⟧ ⟹ phi c' ∨ siso0 c'" and 
***: "⋀ c s t c' s'. 
        ⟦phi c; mustT c s; mustT c t; s ≈ t; (c,s) →c (c',s')⟧ ⟹ 
        ∃ t'. s' ≈ t' ∧ (c,t) →c (c',t')" and 
****: "⋀ c s t s'. 
         ⟦mustT c s; mustT c t; phi c; s ≈ t; (c,s) →t s'⟧ ⟹ 
         ∃ t'. s' ≈ t' ∧ (c,t) →t t'"
shows "siso0 c"
using * apply - apply(erule siso0.coinduct) using ** *** **** by auto

lemma siso0_raw_coind[consumes 1, case_names Indef Cont Term]:
assumes *: "phi c" and 
**: "⋀ c s c' s'. ⟦phi c; mustT c s; (c,s) →c (c',s')⟧ ⟹ phi c'" and 
***: "⋀ c s t c' s'. 
        ⟦phi c; mustT c s; mustT c t; s ≈ t; (c,s) →c (c',s')⟧ ⟹ 
        ∃ t'. s' ≈ t' ∧ (c,t) →c (c',t')" and 
****: "⋀ c s t s'. 
         ⟦phi c; mustT c s; mustT c t; s ≈ t; (c,s) →t s'⟧ ⟹ 
         ∃ t'. s' ≈ t' ∧ (c,t) →t t'"
shows "siso0 c"
using * apply - apply(erule siso0_coind) using ** *** **** by blast+

text‹Self-Isomorphism versus transition:›

lemma siso0_transC:
assumes *: "siso0 c" and **: "mustT c s" "(c,s) →c (c',s')"
shows "siso0 c'"
using * apply - apply(erule siso0.cases) using ** by blast

lemma siso0_MtransC:
assumes "siso0 c" and "mustT c s" and "(c,s) →*c (c',s')"
shows "siso0 c'"
proof-
  have "(c,s) →*c (c',s') ⟹ mustT c s ∧ siso0 c ⟶ siso0 c'"
  apply(erule MtransC_induct2) using siso0_transC mustT_MtransC siso0_transC
  by blast+
  thus ?thesis using assms by blast
qed

lemma siso0_transC_indis:
assumes *: "siso0 c" 
and **: "mustT c s" "mustT c t" "(c,s) →c (c',s')" 
and ***: "s ≈ t"
shows "∃ t'. s' ≈ t' ∧ (c,t) →c (c',t')"
using * apply - apply(erule siso0.cases) using ** *** by blast

lemma siso0_transT:
assumes *: "siso0 c" 
and **: "mustT c s" "mustT c t" "(c,s) →t s'" 
and ***: "s ≈ t"
shows "∃ t'. s' ≈ t' ∧ (c,t) →t t'"
using * apply - apply(erule siso0.cases) using ** *** by blast


subsection‹Notions of bisimilarity› 

text‹Matchers:›

(* Notations and conventions:
\\- ``<u>_<v>" means: ``match u by v", where u, v can be: 
C (one continuation step), MC (multiple continuation steps), 
ZOC (zero or one continuation steps), 
T (termination step), MT (multiple steps leading to termination).   *)

definition matchC_C where 
"matchC_C theta c d ≡ 
 ∀ s t c' s'. 
   s ≈ t ∧ (c,s) →c (c',s') 
   ⟶ 
   (∃ d' t'. (d,t) →c (d',t') ∧ s' ≈ t' ∧ (c',d') ∈ theta)"

definition matchC_ZOC where 
"matchC_ZOC theta c d ≡ 
 ∀ s t c' s'. 
   s ≈ t ∧ (c,s) →c (c',s') 
   ⟶ 
   (s' ≈ t ∧ (c',d) ∈ theta)
   ∨ 
   (∃ d' t'. (d,t) →c (d',t') ∧ s' ≈ t' ∧ (c',d') ∈ theta)"

definition matchC_ZO where 
"matchC_ZO theta c d ≡ 
 ∀ s t c' s'. 
   s ≈ t ∧ (c,s) →c (c',s') 
   ⟶ 
   (s' ≈ t ∧ (c',d) ∈ theta)
   ∨ 
   (∃ d' t'. (d,t) →c (d',t') ∧ s' ≈ t' ∧ (c',d') ∈ theta) 
   ∨ 
   (∃ t'. (d,t) →t t' ∧ s' ≈ t' ∧ discr c')"

definition matchT_T where 
"matchT_T c d ≡ 
 ∀ s t s'. 
   s ≈ t ∧ (c,s) →t s' 
   ⟶ 
   (∃ t'. (d,t) →t t' ∧ s' ≈ t')"

definition matchT_ZO where 
"matchT_ZO c d ≡ 
 ∀ s t s'. 
   s ≈ t ∧ (c,s) →t s' 
   ⟶ 
   (s' ≈ t ∧ discr d)
   ∨ 
   (∃ d' t'. (d,t) →c (d',t') ∧ s' ≈ t' ∧ discr d')
   ∨ 
   (∃ t'. (d,t) →t t' ∧ s' ≈ t')"

(*  *)

definition matchC_MC where 
"matchC_MC theta c d ≡ 
 ∀ s t c' s'. 
   s ≈ t ∧ (c,s) →c (c',s') 
   ⟶ 
   (∃ d' t'. (d,t) →*c (d',t') ∧ s' ≈ t' ∧ (c',d') ∈ theta)"

definition matchC_TMC where 
"matchC_TMC theta c d ≡ 
 ∀ s t c' s'. 
   mustT c s ∧ mustT d t ∧ s ≈ t ∧ (c,s) →c (c',s') 
   ⟶ 
   (∃ d' t'. (d,t) →*c (d',t') ∧ s' ≈ t' ∧ (c',d') ∈ theta)"

definition matchC_M where 
"matchC_M theta c d ≡ 
 ∀ s t c' s'. 
   s ≈ t ∧ (c,s) →c (c',s') 
   ⟶ 
   (∃ d' t'. (d,t) →*c (d',t') ∧ s' ≈ t' ∧ (c',d') ∈ theta) 
   ∨ 
   (∃ t'. (d,t) →*t t' ∧ s' ≈ t' ∧ discr c')"

definition matchT_MT where 
"matchT_MT c d ≡ 
 ∀ s t s'. 
   s ≈ t ∧ (c,s) →t s' 
   ⟶ 
   (∃ t'. (d,t) →*t t' ∧ s' ≈ t')"

definition matchT_TMT where 
"matchT_TMT c d ≡ 
 ∀ s t s'. 
   mustT c s ∧ mustT d t ∧ s ≈ t ∧ (c,s) →t s' 
   ⟶ 
   (∃ t'. (d,t) →*t t' ∧ s' ≈ t')"

definition matchT_M where 
"matchT_M c d ≡ 
 ∀ s t s'. 
   s ≈ t ∧ (c,s) →t s' 
   ⟶ 
   (∃ d' t'. (d,t) →*c (d',t') ∧ s' ≈ t' ∧ discr d')
   ∨ 
   (∃ t'. (d,t) →*t t' ∧ s' ≈ t')"

lemmas match_defs = 
matchC_C_def 
matchC_ZOC_def matchC_ZO_def
matchT_T_def matchT_ZO_def
matchC_MC_def matchC_M_def
matchT_MT_def matchT_M_def
matchC_TMC_def matchT_TMT_def

(* For convenience, indis-symmetric variations of the above definitions: *)

lemma matchC_C_def2: 
"matchC_C theta d c =
 (∀ s t d' t'. 
   s ≈ t ∧ (d,t) →c (d',t') 
   ⟶ 
   (∃ c' s'. (c,s) →c (c',s') ∧ s' ≈ t' ∧ (d',c') ∈ theta))"
unfolding matchC_C_def using indis_sym by blast

lemma matchC_ZOC_def2:  
"matchC_ZOC theta d c= 
 (∀ s t d' t'. 
   s ≈ t ∧ (d,t) →c (d',t') 
   ⟶ 
   (s ≈ t' ∧ (d',c) ∈ theta)
   ∨ 
   (∃ c' s'. (c,s) →c (c',s') ∧ s' ≈ t' ∧ (d',c') ∈ theta))"
unfolding matchC_ZOC_def using indis_sym by blast

lemma matchC_ZO_def2:
"matchC_ZO theta d c = 
 (∀ s t d' t'. 
   s ≈ t ∧ (d,t) →c (d',t') 
   ⟶ 
   (s ≈ t' ∧ (d',c) ∈ theta)
   ∨ 
   (∃ c' s'. (c,s) →c (c',s') ∧ s' ≈ t' ∧ (d',c') ∈ theta) 
   ∨ 
   (∃ s'. (c,s) →t s' ∧ s' ≈ t' ∧ discr d'))"
unfolding matchC_ZO_def using indis_sym by blast

lemma matchT_T_def2:
"matchT_T d c = 
 (∀ s t t'. 
   s ≈ t ∧ (d,t) →t t' 
   ⟶ 
   (∃ s'. (c,s) →t s' ∧ s' ≈ t'))"
unfolding matchT_T_def using indis_sym by blast

lemma matchT_ZO_def2:
"matchT_ZO d c = 
 (∀ s t t'. 
   s ≈ t ∧ (d,t) →t t' 
   ⟶ 
   (s ≈ t' ∧ discr c)
   ∨ 
   (∃ c' s'. (c,s) →c (c',s') ∧ s' ≈ t' ∧ discr c')
   ∨ 
   (∃ s'. (c,s) →t s' ∧ s' ≈ t'))"    
unfolding matchT_ZO_def using indis_sym by blast

(*  *)

lemma matchC_MC_def2:  
"matchC_MC theta d c= 
 (∀ s t d' t'. 
   s ≈ t ∧ (d,t) →c (d',t') 
   ⟶ 
   (∃ c' s'. (c,s) →*c (c',s') ∧ s' ≈ t' ∧ (d',c') ∈ theta))"
unfolding matchC_MC_def using indis_sym by blast

lemma matchC_TMC_def2:  
"matchC_TMC theta d c= 
 (∀ s t d' t'. 
   mustT c s ∧ mustT d t ∧ s ≈ t ∧ (d,t) →c (d',t') 
   ⟶ 
   (∃ c' s'. (c,s) →*c (c',s') ∧ s' ≈ t' ∧ (d',c') ∈ theta))"
unfolding matchC_TMC_def using indis_sym by blast

lemma matchC_M_def2:
"matchC_M theta d c = 
 (∀ s t d' t'. 
   s ≈ t ∧ (d,t) →c (d',t') 
   ⟶ 
   (∃ c' s'. (c,s) →*c (c',s') ∧ s' ≈ t' ∧ (d',c') ∈ theta) 
   ∨ 
   (∃ s'. (c,s) →*t s' ∧ s' ≈ t' ∧ discr d'))"
unfolding matchC_M_def using indis_sym by blast

lemma matchT_MT_def2:
"matchT_MT d c = 
 (∀ s t t'. 
   s ≈ t ∧ (d,t) →t t' 
   ⟶ 
   (∃ s'. (c,s) →*t s' ∧ s' ≈ t'))"
unfolding matchT_MT_def using indis_sym by blast

lemma matchT_TMT_def2:
"matchT_TMT d c = 
 (∀ s t t'. 
   mustT c s ∧ mustT d t ∧ s ≈ t ∧ (d,t) →t t' 
   ⟶ 
   (∃ s'. (c,s) →*t s' ∧ s' ≈ t'))"
unfolding matchT_TMT_def using indis_sym by blast

lemma matchT_M_def2:
"matchT_M d c = 
 (∀ s t t'. 
   s ≈ t ∧ (d,t) →t t' 
   ⟶ 
   (∃ c' s'. (c,s) →*c (c',s') ∧ s' ≈ t' ∧ discr c')
   ∨ 
   (∃ s'. (c,s) →*t s' ∧ s' ≈ t'))"    
unfolding matchT_M_def using indis_sym by blast

text‹Retracts:›

(* Strong retract: *)
definition Sretr where 
"Sretr theta ≡ 
 {(c,d). 
    matchC_C theta c d ∧ 
    matchT_T c d}"

(* Zero-one retract: *)
definition ZOretr where 
"ZOretr theta ≡ 
 {(c,d). 
    matchC_ZO theta c d ∧ 
    matchT_ZO c d}"

(* Zero-one termination-sensitive retract: *)
definition ZOretrT where 
"ZOretrT theta ≡ 
 {(c,d). 
    matchC_ZOC theta c d ∧ 
    matchT_T c d}"

(* Weak retract: *)
definition Wretr where 
"Wretr theta ≡ 
 {(c,d). 
    matchC_M theta c d ∧ 
    matchT_M c d }"

(* Weak termination-sensitive retract: *)
definition WretrT where 
"WretrT theta ≡ 
 {(c,d). 
    matchC_MC theta c d ∧ 
    matchT_MT c d}"

(* Weak terminating-interactive termination-sensitive retract: *)
definition RetrT where 
"RetrT theta ≡ 
 {(c,d). 
    matchC_TMC theta c d ∧ 
    matchT_TMT c d}"

lemmas Retr_defs = 
Sretr_def 
ZOretr_def ZOretrT_def 
Wretr_def WretrT_def 
RetrT_def

text‹The associated bisimilarity relations:›

definition Sbis where "Sbis ≡ bis Sretr"
definition ZObis where "ZObis ≡ bis ZOretr"
definition ZObisT where "ZObisT ≡ bis ZOretrT"
definition Wbis where "Wbis ≡ bis Wretr"
definition WbisT where "WbisT ≡ bis WretrT"
definition BisT where "BisT ≡ bis RetrT"

lemmas bis_defs = 
Sbis_def 
ZObis_def ZObisT_def 
Wbis_def WbisT_def 
BisT_def

abbreviation Sbis_abbrev (infix "≈s" 55) where "c1 ≈s c2 ≡ (c1,c2) ∈ Sbis"
abbreviation ZObis_abbrev (infix "≈01" 55) where "c1 ≈01 c2 ≡ (c1,c2) ∈ ZObis"
abbreviation ZObisT_abbrev (infix "≈01T" 55) where "c1 ≈01T c2 ≡ (c1,c2) ∈ ZObisT"
abbreviation Wbis_abbrev (infix "≈w" 55) where "c1 ≈w c2 ≡ (c1,c2) ∈ Wbis"
abbreviation WbisT_abbrev (infix "≈wT" 55) where "c1 ≈wT c2 ≡ (c1,c2) ∈ WbisT"
abbreviation BisT_abbrev (infix "≈T" 55) where "c1 ≈T c2 ≡ (c1,c2) ∈ BisT"


lemma mono_Retr:
"mono Sretr"
"mono ZOretr"  "mono ZOretrT"
"mono Wretr"  "mono WretrT"
"mono RetrT"
unfolding mono_def Retr_defs match_defs by blast+

(* Sbis: *)
lemma Sbis_prefix:
"Sbis ⊆ Sretr Sbis"
unfolding Sbis_def using mono_Retr bis_prefix by blast

lemma Sbis_sym: "sym Sbis"
unfolding Sbis_def using mono_Retr sym_bis by blast

lemma Sbis_Sym: "c ≈s d ⟹ d ≈s c"
using Sbis_sym unfolding sym_def by blast

lemma Sbis_converse:
"((c,d) ∈ theta^-1 ∪ Sbis) = ((d,c) ∈ theta ∪ Sbis)"
by (metis Sbis_sym converseI converse_Un converse_converse sym_conv_converse_eq)

lemma
Sbis_matchC_C: "⋀ s t. c ≈s d ⟹ matchC_C Sbis c d"
and 
Sbis_matchT_T: "⋀ c d. c ≈s d ⟹ matchT_T c d"
using Sbis_prefix unfolding Sretr_def by auto

lemmas Sbis_step = Sbis_matchC_C Sbis_matchT_T

lemma
Sbis_matchC_C_rev: "⋀ s t. s ≈s t ⟹ matchC_C Sbis t s"
and 
Sbis_matchT_T_rev: "⋀ s t. s ≈s t ⟹ matchT_T t s"
using Sbis_step Sbis_sym unfolding sym_def by blast+

lemmas Sbis_step_rev = Sbis_matchC_C_rev Sbis_matchT_T_rev

lemma Sbis_coind:  
assumes "sym theta" and "theta ⊆ Sretr (theta ∪ Sbis)"
shows "theta ⊆ Sbis"
using assms mono_Retr bis_coind 
unfolding Sbis_def by blast

lemma Sbis_raw_coind:  
assumes "sym theta" and "theta ⊆ Sretr theta"
shows "theta ⊆ Sbis"
using assms mono_Retr bis_raw_coind 
unfolding Sbis_def by blast

lemma Sbis_coind2:
assumes "theta ⊆ Sretr (theta ∪ Sbis)" and 
"theta ^-1 ⊆ Sretr ((theta ^-1) ∪ Sbis)"
shows "theta ⊆ Sbis"
using assms mono_Retr bis_coind2 
unfolding Sbis_def by blast

lemma Sbis_raw_coind2:
assumes "theta ⊆ Sretr theta" and 
"theta ^-1 ⊆ Sretr (theta ^-1)"
shows "theta ⊆ Sbis"
using assms mono_Retr bis_raw_coind2 
unfolding Sbis_def by blast

(* ZObis: *)
lemma ZObis_prefix:
"ZObis ⊆ ZOretr ZObis"
unfolding ZObis_def using mono_Retr bis_prefix by blast

lemma ZObis_sym: "sym ZObis"
unfolding ZObis_def using mono_Retr sym_bis by blast

lemma ZObis_converse:
"((c,d) ∈ theta^-1 ∪ ZObis) = ((d,c) ∈ theta ∪ ZObis)"
by (metis ZObis_sym converseI converse_Un converse_converse sym_conv_converse_eq)

lemma ZObis_Sym: "s ≈01 t ⟹ t ≈01 s"
using ZObis_sym unfolding sym_def by blast

lemma
ZObis_matchC_ZO: "⋀ s t. s ≈01 t ⟹ matchC_ZO ZObis s t"
and 
ZObis_matchT_ZO: "⋀ s t. s ≈01 t ⟹ matchT_ZO s t"
using ZObis_prefix unfolding ZOretr_def by auto

lemmas ZObis_step = ZObis_matchC_ZO ZObis_matchT_ZO 

lemma
ZObis_matchC_ZO_rev: "⋀ s t. s ≈01 t ⟹ matchC_ZO ZObis t s"
and 
ZObis_matchT_ZO_rev: "⋀ s t. s ≈01 t ⟹ matchT_ZO t s"
using ZObis_step ZObis_sym unfolding sym_def by blast+

lemmas ZObis_step_rev = ZObis_matchC_ZO_rev ZObis_matchT_ZO_rev

lemma ZObis_coind:  
assumes "sym theta" and "theta ⊆ ZOretr (theta ∪ ZObis)"
shows "theta ⊆ ZObis"
using assms mono_Retr bis_coind 
unfolding ZObis_def by blast

lemma ZObis_raw_coind:  
assumes "sym theta" and "theta ⊆ ZOretr theta"
shows "theta ⊆ ZObis"
using assms mono_Retr bis_raw_coind 
unfolding ZObis_def by blast

lemma ZObis_coind2:
assumes "theta ⊆ ZOretr (theta ∪ ZObis)" and 
"theta ^-1 ⊆ ZOretr ((theta ^-1) ∪ ZObis)"
shows "theta ⊆ ZObis"
using assms mono_Retr bis_coind2 
unfolding ZObis_def by blast

lemma ZObis_raw_coind2:
assumes "theta ⊆ ZOretr theta" and 
"theta ^-1 ⊆ ZOretr (theta ^-1)"
shows "theta ⊆ ZObis"
using assms mono_Retr bis_raw_coind2 
unfolding ZObis_def by blast

(* ZObisT: *)
lemma ZObisT_prefix:
"ZObisT ⊆ ZOretrT ZObisT"
unfolding ZObisT_def using mono_Retr bis_prefix by blast

lemma ZObisT_sym: "sym ZObisT"
unfolding ZObisT_def using mono_Retr sym_bis by blast

lemma ZObisT_Sym: "s ≈01T t ⟹ t ≈01T s"
using ZObisT_sym unfolding sym_def by blast

lemma ZObisT_converse:
"((c,d) ∈ theta^-1 ∪ ZObisT) = ((d,c) ∈ theta ∪ ZObisT)"
by (metis ZObisT_sym converseI converse_Un converse_converse sym_conv_converse_eq)

lemma
ZObisT_matchC_ZOC: "⋀ s t. s ≈01T t ⟹ matchC_ZOC ZObisT s t"
and 
ZObisT_matchT_T: "⋀ s t. s ≈01T t ⟹ matchT_T s t"
using ZObisT_prefix unfolding ZOretrT_def by auto

lemmas ZObisT_step = ZObisT_matchC_ZOC ZObisT_matchT_T

lemma
ZObisT_matchC_ZOC_rev: "⋀ s t. s ≈01T t ⟹ matchC_ZOC ZObisT t s"
and 
ZObisT_matchT_T_rev: "⋀ s t. s ≈01T t ⟹ matchT_T t s"
using ZObisT_step ZObisT_sym unfolding sym_def by blast+

lemmas ZObisT_step_rev = ZObisT_matchC_ZOC_rev ZObisT_matchT_T_rev 

lemma ZObisT_coind:  
assumes "sym theta" and "theta ⊆ ZOretrT (theta ∪ ZObisT)"
shows "theta ⊆ ZObisT"
using assms mono_Retr bis_coind 
unfolding ZObisT_def by blast

lemma ZObisT_raw_coind:  
assumes "sym theta" and "theta ⊆ ZOretrT theta"
shows "theta ⊆ ZObisT"
using assms mono_Retr bis_raw_coind 
unfolding ZObisT_def by blast

lemma ZObisT_coind2:
assumes "theta ⊆ ZOretrT (theta ∪ ZObisT)" and 
"theta ^-1 ⊆ ZOretrT ((theta ^-1) ∪ ZObisT)"
shows "theta ⊆ ZObisT"
using assms mono_Retr bis_coind2 
unfolding ZObisT_def by blast

lemma ZObisT_raw_coind2:
assumes "theta ⊆ ZOretrT theta" and 
"theta ^-1 ⊆ ZOretrT (theta ^-1)"
shows "theta ⊆ ZObisT"
using assms mono_Retr bis_raw_coind2 
unfolding ZObisT_def by blast

(* Wbis: *)
lemma Wbis_prefix:
"Wbis ⊆ Wretr Wbis"
unfolding Wbis_def using mono_Retr bis_prefix by blast

lemma Wbis_sym: "sym Wbis"
unfolding Wbis_def using mono_Retr sym_bis by blast

lemma Wbis_converse:
"((c,d) ∈ theta^-1 ∪ Wbis) = ((d,c) ∈ theta ∪ Wbis)"
by (metis Wbis_sym converseI converse_Un converse_converse sym_conv_converse_eq)

lemma Wbis_Sym: "c ≈w d ⟹ d ≈w c"
using Wbis_sym unfolding sym_def by blast

lemma
Wbis_matchC_M: "⋀ c d. c ≈w d ⟹ matchC_M Wbis c d"
and 
Wbis_matchT_M: "⋀ c d. c ≈w d ⟹ matchT_M c d"
using Wbis_prefix unfolding Wretr_def by auto

lemmas Wbis_step = Wbis_matchC_M Wbis_matchT_M 

lemma
Wbis_matchC_M_rev: "⋀ s t. s ≈w t ⟹ matchC_M Wbis t s"
and 
Wbis_matchT_M_rev: "⋀ s t. s ≈w t ⟹ matchT_M t s"
using Wbis_step Wbis_sym unfolding sym_def by blast+

lemmas Wbis_step_rev = Wbis_matchC_M_rev Wbis_matchT_M_rev

lemma Wbis_coind:  
assumes "sym theta" and "theta ⊆ Wretr (theta ∪ Wbis)"
shows "theta ⊆ Wbis"
using assms mono_Retr bis_coind 
unfolding Wbis_def by blast

lemma Wbis_raw_coind:  
assumes "sym theta" and "theta ⊆ Wretr theta"
shows "theta ⊆ Wbis"
using assms mono_Retr bis_raw_coind 
unfolding Wbis_def by blast

lemma Wbis_coind2:
assumes "theta ⊆ Wretr (theta ∪ Wbis)" and 
"theta ^-1 ⊆ Wretr ((theta ^-1) ∪ Wbis)"
shows "theta ⊆ Wbis"
using assms mono_Retr bis_coind2 
unfolding Wbis_def by blast

lemma Wbis_raw_coind2:
assumes "theta ⊆ Wretr theta" and 
"theta ^-1 ⊆ Wretr (theta ^-1)"
shows "theta ⊆ Wbis"
using assms mono_Retr bis_raw_coind2 
unfolding Wbis_def by blast

(* WbisT: *)
lemma WbisT_prefix:
"WbisT ⊆ WretrT WbisT"
unfolding WbisT_def using mono_Retr bis_prefix by blast

lemma WbisT_sym: "sym WbisT"
unfolding WbisT_def using mono_Retr sym_bis by blast

lemma WbisT_Sym: "c ≈wT d ⟹ d ≈wT c"
using WbisT_sym unfolding sym_def by blast

lemma WbisT_converse:
"((c,d) ∈ theta^-1 ∪ WbisT) = ((d,c) ∈ theta ∪ WbisT)"
by (metis WbisT_sym converseI converse_Un converse_converse sym_conv_converse_eq)

lemma
WbisT_matchC_MC: "⋀ c d. c ≈wT d ⟹ matchC_MC WbisT c d"
and 
WbisT_matchT_MT: "⋀ c d. c ≈wT d ⟹ matchT_MT c d"
using WbisT_prefix unfolding WretrT_def by auto

lemmas WbisT_step = WbisT_matchC_MC WbisT_matchT_MT

lemma
WbisT_matchC_MC_rev: "⋀ s t. s ≈wT t ⟹ matchC_MC WbisT t s"
and 
WbisT_matchT_MT_rev: "⋀ s t. s ≈wT t ⟹ matchT_MT t s"
using WbisT_step WbisT_sym unfolding sym_def by blast+

lemmas WbisT_step_rev = WbisT_matchC_MC_rev WbisT_matchT_MT_rev 

lemma WbisT_coind:  
assumes "sym theta" and "theta ⊆ WretrT (theta ∪ WbisT)"
shows "theta ⊆ WbisT"
using assms mono_Retr bis_coind 
unfolding WbisT_def by blast

lemma WbisT_raw_coind:  
assumes "sym theta" and "theta ⊆ WretrT theta"
shows "theta ⊆ WbisT"
using assms mono_Retr bis_raw_coind 
unfolding WbisT_def by blast

lemma WbisT_coind2:
assumes "theta ⊆ WretrT (theta ∪ WbisT)" and 
"theta ^-1 ⊆ WretrT ((theta ^-1) ∪ WbisT)"
shows "theta ⊆ WbisT"
using assms mono_Retr bis_coind2 
unfolding WbisT_def by blast

lemma WbisT_raw_coind2:
assumes "theta ⊆ WretrT theta" and 
"theta ^-1 ⊆ WretrT (theta ^-1)"
shows "theta ⊆ WbisT"
using assms mono_Retr bis_raw_coind2 
unfolding WbisT_def by blast

lemma WbisT_coinduct[consumes 1, case_names sym cont termi]:
  assumes φ: "φ c d"
  assumes S: "⋀c d. φ c d ⟹ φ d c"
  assumes C: "⋀c s d t c' s'.
    ⟦ φ c d ; s ≈ t ; (c, s) →c (c', s') ⟧ ⟹ ∃d' t'. (d, t) →*c (d', t') ∧ s' ≈ t' ∧ (φ c' d' ∨ c' ≈wT d')"
  assumes T: "⋀c s d t s'.
    ⟦ φ c d ; s ≈ t ; (c, s) →t s' ⟧ ⟹ ∃t'. (d, t) →*t t' ∧ s' ≈ t'"
  shows "c ≈wT d"
proof -
  let ?θ = "{(c, d). φ c d}"
  have "sym ?θ" by (auto intro!: symI S)
  moreover 
  have "?θ ⊆ WretrT (?θ ∪ WbisT)"
    using C T by (auto simp: WretrT_def matchC_MC_def matchT_MT_def)
  ultimately have "?θ ⊆ WbisT"
    using WbisT_coind by auto
  with φ show ?thesis
    by auto
qed

(* BisT: *)
lemma BisT_prefix:
"BisT ⊆ RetrT BisT"
unfolding BisT_def using mono_Retr bis_prefix by blast

lemma BisT_sym: "sym BisT"
unfolding BisT_def using mono_Retr sym_bis by blast

lemma BisT_Sym: "c ≈T d ⟹ d ≈T c"
using BisT_sym unfolding sym_def by blast

lemma BisT_converse:
"((c,d) ∈ theta^-1 ∪ BisT) = ((d,c) ∈ theta ∪ BisT)"
by (metis BisT_sym converseI converse_Un converse_converse sym_conv_converse_eq)

lemma
BisT_matchC_TMC: "⋀ c d. c ≈T d ⟹ matchC_TMC BisT c d"
and 
BisT_matchT_TMT: "⋀ c d. c ≈T d ⟹ matchT_TMT c d"
using BisT_prefix unfolding RetrT_def by auto

lemmas BisT_step = BisT_matchC_TMC BisT_matchT_TMT

lemma
BisT_matchC_TMC_rev: "⋀ c d. c ≈T d ⟹ matchC_TMC BisT d c"
and 
BisT_matchT_TMT_rev: "⋀ c d. c ≈T d ⟹ matchT_TMT d c"
using BisT_step BisT_sym unfolding sym_def by blast+

lemmas BisT_step_rev = BisT_matchC_TMC_rev BisT_matchT_TMT_rev 

lemma BisT_coind:  
assumes "sym theta" and "theta ⊆ RetrT (theta ∪ BisT)"
shows "theta ⊆ BisT"
using assms mono_Retr bis_coind 
unfolding BisT_def by blast

lemma BisT_raw_coind:  
assumes "sym theta" and "theta ⊆ RetrT theta"
shows "theta ⊆ BisT"
using assms mono_Retr bis_raw_coind 
unfolding BisT_def by blast

lemma BisT_coind2:
assumes "theta ⊆ RetrT (theta ∪ BisT)" and 
"theta ^-1 ⊆ RetrT ((theta ^-1) ∪ BisT)"
shows "theta ⊆ BisT"
using assms mono_Retr bis_coind2 
unfolding BisT_def by blast

lemma BisT_raw_coind2:
assumes "theta ⊆ RetrT theta" and 
"theta ^-1 ⊆ RetrT (theta ^-1)"
shows "theta ⊆ BisT"
using assms mono_Retr bis_raw_coind2 
unfolding BisT_def by blast

text‹Inclusions between bisimilarities:›

lemma match_imp[simp]:
"⋀ theta c1 c2. matchC_C theta c1 c2 ⟹ matchC_ZOC theta c1 c2"
(*  *)
"⋀ theta c1 c2. matchC_ZOC theta c1 c2 ⟹ matchC_ZO theta c1 c2"
(*  *)
"⋀ theta c1 c2. matchC_ZOC theta c1 c2 ⟹ matchC_MC theta c1 c2"
(*  *)
"⋀ theta c1 c2. matchC_ZO theta c1 c2 ⟹ matchC_M theta c1 c2"
(*  *)
"⋀ theta c1 c2. matchC_MC theta c1 c2 ⟹ matchC_M theta c1 c2"
(*  *)
(*  *)
"⋀ c1 c2. matchT_T c1 c2 ⟹ matchT_ZO c1 c2"
(*  *)
"⋀ c1 c2. matchT_T c1 c2 ⟹ matchT_MT c1 c2"
(*  *)
"⋀ c1 c2. matchT_ZO c1 c2 ⟹ matchT_M c1 c2"
(*  *)
"⋀ c1 c2. matchT_MT c1 c2 ⟹ matchT_M c1 c2"
(*  *)
"⋀ theta c1 c2. matchC_MC theta c1 c2 ⟹ matchC_TMC theta c1 c2"
(*  *)
"⋀ theta c1 c2. matchT_MT c1 c2 ⟹ matchT_TMT c1 c2"
unfolding match_defs apply(tactic ‹mauto_no_simp_tac @{context}›)
apply fastforce apply fastforce
apply (metis MtransC_Refl transC_MtransC)
by force+

lemma Retr_incl:
"⋀theta. Sretr theta ⊆ ZOretrT theta"
(*  *)
"⋀theta. ZOretrT theta ⊆ ZOretr theta"
(*  *)
"⋀theta. ZOretrT theta ⊆ WretrT theta"
(*  *)
"⋀theta. ZOretr theta ⊆ Wretr theta"
(*  *)
"⋀theta. WretrT theta ⊆ Wretr theta"
(*  *)
"⋀theta. WretrT theta ⊆ RetrT theta"
unfolding Retr_defs by auto

lemma bis_incl:
"Sbis ⊆ ZObisT"
(*  *)
"ZObisT ⊆ ZObis"
(*  *)
"ZObisT ⊆ WbisT"
(*  *)
"ZObis ⊆ Wbis"
(*  *)
"WbisT ⊆ Wbis"
(*  *)
"WbisT ⊆ BisT"
unfolding bis_defs 
using Retr_incl mono_bis mono_Retr by blast+

lemma bis_imp[simp]:
"⋀ c1 c2. c1 ≈s c2 ⟹ c1 ≈01T c2"
(*  *)
"⋀ c1 c2. c1 ≈01T c2 ⟹ c1 ≈01 c2"
(*  *)
"⋀ c1 c2. c1 ≈01T c2 ⟹ c1 ≈wT c2"
(*  *)
"⋀ c1 c2. c1 ≈01 c2 ⟹ c1 ≈w c2"
(*  *)
"⋀ c1 c2. c1 ≈wT c2 ⟹ c1 ≈w c2"
(*  *)
"⋀ c1 c2. c1 ≈wT c2 ⟹ c1 ≈T c2"
using bis_incl rev_subsetD by auto

text‹Self-isomorphism implies strong bisimilarity:›

lemma siso_Sbis[simp]:
assumes "siso c"
shows "c ≈s c"
proof-
  let ?theta = "{(c,c) | c . siso c}"
  have "?theta ⊆ Sbis"
  proof(rule Sbis_raw_coind)
    show "sym ?theta" unfolding sym_def by blast
  next
    show "?theta ⊆ Sretr ?theta"
    proof clarify
      fix c assume c: "siso c"
      show "(c, c) ∈ Sretr ?theta"
      unfolding Sretr_def proof (clarify, intro conjI)
        show "matchC_C ?theta c c"
        unfolding matchC_C_def apply simp
        by (metis c siso_transC siso_transC_indis)
      next
        show "matchT_T c c"
        unfolding matchT_T_def
        by (metis c siso_transT)           
      qed
    qed
  qed
  thus ?thesis using assms by blast
qed

text‹0-Self-isomorphism implies weak T 0-bisimilarity:›

lemma siso0_Sbis[simp]:
assumes "siso0 c"
shows "c ≈T c"
proof-
  let ?theta = "{(c,c) | c . siso0 c}"
  have "?theta ⊆ BisT"
  proof(rule BisT_raw_coind)
    show "sym ?theta" unfolding sym_def by blast
  next
    show "?theta ⊆ RetrT ?theta"
    proof clarify
      fix c assume c: "siso0 c"
      show "(c, c) ∈ RetrT ?theta"
      unfolding RetrT_def proof (clarify, intro conjI)
        show "matchC_TMC ?theta c c"
        unfolding matchC_TMC_def apply simp
        by (metis c siso0_transC siso0_transC_indis transC_MtransC)
      next
        show "matchT_TMT c c"
        unfolding matchC_TMC_def
        by (metis c matchT_TMT_def siso0_transT transT_MtransT)
      qed
    qed
  qed
  thus ?thesis using assms by blast
qed
 

end 
(* context PL_Indis *)


end