Theory Shallow

section ‹Shallow embedding of HyperCTL*›

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

text‹We define a notion of ``shallow'' HyperCTL* formula (sfmla) that captures
HyperCTL* binders as meta-level HOL binders. We also define a proof system for this
shallow 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.  
The atomic formulas (operator $\textit{atom}$) are parameterized by atomic propositions (as customary in temporal logic), 
and additionally by a number indicating the position, in the list of paths, of the path to which the atomic proposition 
refers -- for example, $\textit{atom}\;a\;i$ holds for the list of paths $\pi l$ just in case proposition $a$ holds 
at 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 
list $\pi l$ synchronously.  Finally, the existential quantifier refers to the existence of a path whose origin state is that of 
the last path in $\pi l$.  

As an example: $\textit{exi}\; (\textit{exi}\; (\textit{until}\; (\textit{atom}\;a\;0)\;(\textit{atom}\;b\;1)))$ holds for the empty list 
iff 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
for 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
(*>*)