Quelle  Shallow.thy

section ‹Shallow embedding of HyperCTL*›

(*<*)
theory Shallow
imports Prelim
begin
(*>*)

text‹We define a notion of ``shallow'' HyperCTL* formula (sfmla) that captures
 * binders as meta-level HOL binders. We also define a proof system for this
  embedding.›


subsection‹Kripke structures and paths›

type_synonym ('state,'aprop) path = "('state × 'aprop set) stream"

abbreviation stateOf where "stateOf π ≡ fst (shd π)"
abbreviation apropsOf where "apropsOf π ≡ snd (shd π)"

locale Kripke =
  fixes S :: "'state set" and s0 :: 'state and δ :: "'state ==> 'state set"
  and AP :: "'aprop set" and L :: "'state ==> 'aprop set"
  assumes s0: "s0 ∈ S" and δ: "∧ s. s ∈ S ==> δ s ⊆ S"
  and L : "∧ s. s ∈ S ==> L s ⊆ AP"
begin

text‹Well-formed paths›

coinductive wfp :: "'aprop set ==> ('state,'aprop) path ==> bool"
for AP' :: "'aprop set"
where
intro:
"[s ∈ S; A ⊆ AP'; A ∩ AP = L s; stateOf π ∈ δ s; wfp AP' π]
 ==>
 wfp AP' ((s,A) ## π)"

lemma wfp:
"wfp AP' π ⟷
 (∀ i. fst (π !! i) ∈ S ∧ snd (π !! i) ⊆ AP' ∧
       snd (π !! i) ∩ AP = L (fst (π !! i)) ∧
       fst (π !! (Suc i)) ∈ δ (fst (π !! i))
 )"
(is "?L ⟷ (∀ i. ?R i)")
proof (intro iffI allI)
  fix i assume ?L thus "?R i"
  apply(induction i arbitrary: π)
  by (metis snth.simps fst_conv snd_conv stream.sel wfp.cases)+
next
  assume R: "∀ i. ?R i"  thus ?L
  apply (coinduct)
  using s0 fst_conv snd_conv snth.simps stream.sel 
  by (metis inf_commute stream.collapse surj_pair)
qed

lemma wfp_sdrop[simp]:
"wfp AP' π ==> wfp AP' (sdrop i π)"
unfolding wfp by simp (metis sdrop_add sdrop_simps(1))

(*<*)
end (* context Kripke *)
(*>*)

text‹end-of-context Kripke›


subsection‹Shallow representations of formulas›

text‹A shallow (representation of a) HyperCTL* formula will be a predicate on lists of paths.
  atomic formulas (operator $\textit{atom}$) are parameterized by atomic propositions (as customary in temporal logic),
  additionally by a number indicating the position, in the list of paths, of the path to which the atomic proposition
  -- for example, $\textit{atom}\;a\;i$ holds for the list of paths $\pi l$ just in case proposition $a$ holds
  the first state of $\pi l!i$, the $i$'th path in $\pi l$. The temporal operators $\textit{next}$ and $\textit{until}$ act on all the paths of the argument
  $\pi l$ synchronously. Finally, the existential quantifier refers to the existence of a path whose origin state is that of
  last path in $\pi l$.

  an example: $\textit{exi}\; (\textit{exi}\; (\textit{until}\; (\textit{atom}\;a\;0)\;(\textit{atom}\;b\;1)))$ holds for the empty list
  there exist two paths $\rho_0$ and $\rho_1$ such that, synchronously,
 a$ holds on $\rho_0$ until $b$ holds on $\rho_1$. Another example will be the formula encoding Goguen-Meseguer noninterference.
 ›

text‹Shallow HyperCTL* formulas:›

type_synonym ('state,'aprop) sfmla = "('state,'aprop) path list ==> bool"


locale Shallow = Kripke S "s0" δ AP L
  for S :: "'state set" and s0 :: 'state and δ :: "'state ==> 'state set"
  and AP :: "'aprop set" and L :: "'state ==> 'aprop set"
+
  fixes AP' assumes AP_AP': "AP ⊆ AP'"
begin

text‹Primitive operators›

(* I include false as a primitive since otherwise I would have to assume nonemptyness of
  the atomic propositions *)
definition fls :: "('state,'aprop) sfmla" where
"fls πl ≡ False"

definition atom :: "'aprop ==> nat ==> ('state,'aprop) sfmla" where
"atom a i πl ≡ a ∈ apropsOf (πl!i)"

definition neg :: "('state,'aprop) sfmla ==> ('state,'aprop) sfmla" where
"neg φ πl ≡ ¬ φ πl"

definition dis :: "('state,'aprop) sfmla ==> ('state,'aprop) sfmla ==> ('state,'aprop) sfmla" where
"dis φ ψ πl ≡ φ πl ∨ ψ πl"

definition "next" :: "('state,'aprop) sfmla ==> ('state,'aprop) sfmla" where
"next φ πl ≡ φ (map stl πl)"

definition until :: "('state,'aprop) sfmla ==> ('state,'aprop) sfmla ==> ('state,'aprop) sfmla" where
"until φ ψ πl ≡
 ∃ i. ψ (map (sdrop i) πl) ∧ (∀ j ∈{0..<i}. φ (map (sdrop j) πl))"

definition exii :: "('state,'aprop) sfmla ==> ('state,'aprop) sfmla" where
"exii φ πl ≡
 ∃ π. wfp AP' π ∧ stateOf π = (if πl ≠ [] then stateOf (last πl) else s0)
      ∧ φ (πl @ [π])"

definition exi :: "(('state,'aprop) path ==> ('state,'aprop) sfmla) ==> ('state,'aprop) sfmla" where
"exi F πl ≡
 ∃ π. wfp AP' π ∧ stateOf π = (if πl ≠ [] then stateOf (last πl) else s0)
      ∧ F π πl"

text‹Derived operators›

definition "tr ≡ neg fls"
definition "con φ ψ ≡ neg (dis (neg φ) (neg ψ))"
definition "imp φ ψ ≡ dis (neg φ) ψ"
definition "eq φ ψ ≡ con (imp φ ψ) (imp ψ φ) "
definition "fall F ≡ neg (exi (λ π. neg (F π)))"
definition "ev φ ≡ until tr φ"
definition "alw φ ≡ neg (ev (neg φ))"
definition "wuntil φ ψ ≡ dis (until φ ψ) (alw φ)"

lemmas main_op_defs =
fls_def atom_def neg_def dis_def next_def until_def exi_def

lemmas der_op_defs =
tr_def con_def imp_def eq_def ev_def alw_def wuntil_def fall_def

lemmas op_defs = main_op_defs der_op_defs


subsection‹Reasoning rules›

text‹We provide introduction, elimination, unfolding and (co)induction rules
  the connectives and quantifiers.›

text‹Boolean operators›

lemma fls_elim[elim!]:
assumes "fls πl" shows φ
using assms unfolding op_defs by auto

lemma tr_intro[intro!, simp]: "tr πl"
unfolding op_defs by auto

lemma dis_introL[intro]:
assumes "φ πl" shows "dis φ ψ πl"
using assms unfolding op_defs by auto

lemma dis_introR[intro]:
assumes "ψ πl" shows "dis φ ψ πl"
using assms unfolding op_defs by auto

lemma dis_elim[elim]:
assumes "dis φ ψ πl" and "φ πl ==> χ" and "ψ πl ==> χ"
shows χ
using assms unfolding op_defs by auto

lemma con_intro[intro!]:
assumes "φ πl" and "ψ πl" shows "con φ ψ πl"
using assms unfolding op_defs by auto

lemma con_elim[elim]:
assumes "con φ ψ πl" and "φ πl ==> ψ πl ==> χ" shows χ
using assms unfolding op_defs by auto

lemma neg_intro[intro!]:
assumes "φ πl ==> False"  shows "neg φ πl"
using assms unfolding op_defs by auto

lemma neg_elim[elim]:
assumes "neg φ πl" and "φ πl"  shows χ
using assms unfolding op_defs by auto

lemma imp_intro[intro!]:
assumes "φ πl ==> ψ πl"  shows "imp φ ψ πl"
using assms unfolding op_defs by auto

lemma imp_elim[elim]:
assumes "imp φ ψ πl" and "φ πl" and "ψ πl ==> χ" shows χ
using assms unfolding op_defs by auto

lemma imp_mp[elim]:
assumes "imp φ ψ πl" and "φ πl" shows "ψ πl"
using assms unfolding op_defs by auto

lemma eq_intro[intro!]:
assumes "φ πl ==> ψ πl" and "ψ πl ==> φ πl" shows "eq φ ψ πl"
using assms unfolding op_defs by auto

lemma eq_elimL[elim]:
assumes "eq φ ψ πl" and "φ πl" and "ψ πl ==> χ" shows χ
using assms unfolding op_defs by auto

lemma eq_elimR[elim]:
assumes "eq φ ψ πl" and "ψ πl" and "φ πl ==> χ" shows χ
using assms unfolding op_defs by auto

lemma eq_equals: "eq φ ψ πl ⟷ φ πl = ψ πl"
by (metis eq_elimL eq_elimR eq_intro)


text‹Quantifiers›

lemma exi_intro[intro]:
assumes "wfp AP' π"
and "πl ≠ [] ==> stateOf π = stateOf (last πl)"
and "πl = [] ==> stateOf π = s0"
and "F π πl"
shows "exi F πl"
using assms unfolding exi_def by auto

lemma exi_elim[elim]:
assumes "exi F πl"
and
"∧ π. [wfp AP' π; πl ≠ [] ==> stateOf π = stateOf (last πl); πl = [] ==> stateOf π = s0; F π πl] ==> χ"
shows χ
using assms unfolding exi_def by auto

lemma fall_intro[intro]:
assumes
"∧ π. [wfp AP' π; πl ≠ [] ==> stateOf π = stateOf (last πl) ; πl = [] ==> stateOf π = s0]
       ==> F π πl"
shows "fall F πl"
using assms unfolding fall_def by (metis exi_def neg_def)

lemma fall_elim[elim]:
assumes "fall F πl"
and
"(∧π. [wfp AP' π; πl ≠ [] ==> stateOf π = stateOf (last πl); πl = [] ==> stateOf π = s0]
        ==> F π πl)
  ==> χ"
shows χ
using assms unfolding fall_def
by (metis exi_def neg_elim neg_intro)


text‹Temporal connectives›

lemma next_intro[intro]:
assumes "φ (map stl πl)"  shows "next φ πl"
using assms unfolding op_defs by auto

lemma next_elim[elim]:
assumes "next φ πl" and "φ (map stl πl) ==> χ"  shows χ
using assms unfolding op_defs by auto

lemma until_introR[intro]:
assumes "ψ πl" shows "until φ ψ πl"
using assms unfolding op_defs by (auto intro: exI[of _ 0])

lemma until_introL[intro]:
assumes φ: "φ πl" and u: "until φ ψ (map stl πl)"
shows "until φ ψ πl"
proof-
  obtain i where ψ: "ψ (map (sdrop (Suc i)) πl)" and 1: "∀j∈{0..<i}. φ (map (sdrop (Suc j)) πl)"
  using u unfolding op_defs by auto
  {fix j assume "j ∈ {0..<Suc i}"
   hence "φ (map (sdrop j) πl)" using 1 φ by (cases j) auto
  }
  thus ?thesis using ψ unfolding op_defs by auto
qed

text‹The elimination rules for until and eventually are induction rules.›

lemma until_induct[induct pred: until, consumes 1, case_names Base Step]:
assumes u: "until φ ψ πl"
and b: "∧ πl. ψ πl ==> χ πl"
and i: "∧ πl. [φ πl; until φ ψ (map stl πl); χ (map stl πl)] ==> χ πl"
shows "χ πl"
proof-
  obtain i where ψ: "ψ (map (sdrop i) πl)" and 1:  "∀j∈{0..<i}. φ (map (sdrop j) πl)"
  using u unfolding until_def next_def by auto
  {fix k assume k: "k ≤ i"
   hence "until φ ψ (map (sdrop k) πl) ∧ χ (map (sdrop k) πl)"
   proof (induction "i-k" arbitrary: k)
     case 0 hence "k=i" by auto
     with b[OF ψ] u ψ show ?case by (auto intro: until_introR)
   next
     case (Suc ii)  let ?πl' = "map (sdrop k) πl"
     have "until φ ψ (map stl ?πl') ∧ χ (map stl ?πl')" using Suc by auto
     moreover have "φ ?πl'" using 1 Suc by auto
     ultimately show ?case using i by auto
   qed
  }
  from this[of 0] show ?thesis by simp
qed

lemma until_unfold:
"until φ ψ πl = (ψ πl ∨ φ πl ∧ until φ ψ (map stl πl))" (is "?L = ?R")
proof
  assume ?L thus ?R by induct auto
qed auto

lemma ev_introR[intro]:
assumes "φ πl" shows "ev φ πl"
using assms unfolding ev_def by (auto intro: until_introR)

lemma ev_introL[intro]:
assumes "ev φ (map stl πl)"  shows "ev φ πl"
using assms unfolding ev_def by (auto intro: until_introL)

lemma ev_induct[induct pred: ev, consumes 1, case_names Base Step]:
assumes "ev φ πl" and "∧ πl. φ πl ==> χ πl"
and "∧ πl. [ev φ (map stl πl); χ (map stl πl)] ==> χ πl"
shows "χ πl"
using assms unfolding ev_def by induct (auto simp: assms)

lemma ev_unfold:
"ev φ πl = (φ πl ∨ ev φ (map stl πl))"
unfolding ev_def by (metis tr_intro until_unfold)

lemma ev: "ev φ πl ⟷ (∃ i. φ (map (sdrop i) πl))"
unfolding ev_def until_def by auto


text‹The introduction rules for always and weak until are coinduction rules.›

lemma alw_coinduct[coinduct pred: alw, consumes 1, case_names Hyp]:
assumes "χ πl"
and "∧ πl. χ πl ==> alw φ πl ∨ (φ πl ∧ χ (map stl πl))"
shows "alw φ πl"
proof-
  {assume "ev (neg φ) πl"
   hence "¬ χ πl"
   apply induct
   using assms unfolding op_defs by auto (metis assms alw_def ev_def neg_def until_introR)
  }
  thus ?thesis using assms unfolding op_defs by auto
qed

lemma alw_elim[elim]:
assumes "alw φ πl"
and "[φ πl; alw φ (map stl πl)] ==> χ"
shows "χ"
using assms unfolding alw_def by(auto elim: ev_introR simp: neg_def)

lemma alw_destL: "alw φ πl ==> φ πl" by auto
lemma alw_destR: "alw φ πl ==> alw φ (map stl πl)" by auto

lemma alw_unfold:
"alw φ πl = (φ πl ∧ alw φ (map stl πl))"
by (metis alw_def ev_unfold neg_elim neg_intro)

lemma alw: "alw φ πl ⟷ (∀ i. φ (map (sdrop i) πl))"
unfolding alw_def ev neg_def by simp

lemma sdrop_imp_alw:
assumes "∧ i. (∧j. j ≤ i ==> φ [sdrop j π, sdrop j π']) ==> ψ [sdrop i π, sdrop i π']"
shows "imp (alw φ) (alw ψ) [π, π']"
using assms by(auto simp: alw)

lemma wuntil_coinduct[coinduct pred: wuntil, consumes 1, case_names Hyp]:
assumes χ: "χ πl"
and 0: "∧ πl. χ πl ==> ψ πl ∨ (φ πl ∧ χ (map stl πl))"
shows "wuntil φ ψ πl"
proof-
  {assume "¬ until φ ψ πl ∧ χ πl"
   hence "alw φ πl"
   apply coinduct using 0 by (auto intro: until_introL until_introR)
  }
  thus ?thesis using χ unfolding wuntil_def dis_def by auto
qed

lemma wuntil_elim[elim]:
assumes w: "wuntil φ ψ πl"
and 1: "ψ πl ==> χ"
and 2: "[φ πl; wuntil φ ψ (map stl πl)] ==> χ"
shows χ
proof(cases "alw φ πl")
  case True
  thus ?thesis apply standard using 2 unfolding wuntil_def by auto
next
  case False
  hence "until φ ψ πl" using w unfolding wuntil_def dis_def by auto
  thus ?thesis by (metis assms dis_introL until_unfold wuntil_def)
qed

lemma wuntil_unfold:
"wuntil φ ψ πl = (ψ πl ∨ φ πl ∧ wuntil φ ψ (map stl πl))"
by (metis alw_unfold dis_def until_unfold wuntil_def)


subsection‹More derived operators›

text‹The conjunction of an arbitrary set of formulas:›

definition scon ::
"('state,'aprop) sfmla set ==> ('state,'aprop) sfmla" where
"scon φs πl ≡ ∀ φ ∈ φs. φ πl"

lemma mcon_intro[intro!]:
assumes "∧ φ. φ ∈ φs ==> φ πl" shows "scon φs πl"
using assms unfolding scon_def by auto

lemma scon_elim[elim]:
assumes "scon φs πl" and "(∧ φ. φ ∈ φs ==> φ πl) ==> χ"
shows χ
using assms unfolding scon_def by auto

text‹Double-binding forall:›

definition "fall2 F ≡ fall (λ π. fall (F π))"

lemma fall2_intro[intro]:
assumes
"∧ π π'. [wfp AP' π; wfp AP' π';
           πl ≠ [] ==> stateOf π = stateOf (last πl);
           πl = [] ==> stateOf π = s0;
           stateOf π' = stateOf π
          ]
       ==> F π π' πl"
shows "fall2 F πl"
using assms unfolding fall2_def by (auto intro!: fall_intro)

lemma fall2_elim[elim]:
assumes "fall2 F πl"
and
"(∧π π'. [wfp AP' π; wfp AP' π';
           πl ≠ [] ==> stateOf π = stateOf (last πl); πl = [] ==> stateOf π = s0;
           stateOf π' = stateOf π
          ]
          ==> F π π' πl)
  ==> χ"
shows χ
using assms unfolding fall2_def by (auto elim!: fall_elim) (metis fall_elim)

(*<*)
end (* context Shallow *)
(*>*)

text‹end-of-context Shallow›


(*<*)
end
(*>*)