Quelle  Deep.thy

section ‹Deep representation of HyperCTL* -- syntax and semantics›

(*<*)
theory Deep
imports Shallow "HOL-Library.Infinite_Set"
begin
(*>*)

subsection‹Path variables and environments›

datatype pvar = Pvariable (natOf : nat)

text ‹Deeply embedded (syntactic) formulas›

datatype 'aprop dfmla =
  Atom 'aprop pvar |
  Fls | Neg "'aprop dfmla" | Dis "'aprop dfmla" "'aprop dfmla" |
  Next "'aprop dfmla" | Until "'aprop dfmla" "'aprop dfmla" |
  Exi pvar "'aprop dfmla"

text‹Derived operators›

definition "Tr ≡ Neg Fls"
definition "Con φ ψ ≡ Neg (Dis (Neg φ) (Neg ψ))"
definition "Imp φ ψ ≡ Dis (Neg φ) ψ"
definition "Eq φ ψ ≡ Con (Imp φ ψ) (Imp ψ φ) "
definition "Fall p φ ≡ Neg (Exi p (Neg φ))"
definition "Ev φ ≡ Until Tr φ"
definition "Alw φ ≡ Neg (Ev (Neg φ))"
definition "Wuntil φ ψ ≡ Dis (Until φ ψ) (Alw φ)"
definition "Fall2 p p' φ ≡ Fall p (Fall p' φ)"

lemmas der_Op_defs =
Tr_def Con_def Imp_def Eq_def Ev_def Alw_def Wuntil_def Fall_def Fall2_def

text‹Well-formed formulas are those that do not have a temporal operator
  the scope of any quantifier -- indeed, in HyperCTL* such a situation does not make sense,
  the temporal operators refer to previously introduced/quantified paths.›

primrec wff :: "'aprop dfmla ==> bool" where
 "wff (Atom a p) = True"
|"wff Fls = True"
|"wff (Neg φ) = wff φ"
|"wff (Dis φ ψ) = (wff φ ∧ wff ψ)"
|"wff (Next φ) = False"
|"wff (Until φ ψ) = False"
|"wff (Exi p φ) = True"


text ‹The ability to pick a fresh variable›

lemma finite_fresh_pvar:
assumes "finite (P :: pvar set)"
obtains p where "p ∉ P"
proof-
  have "finite (natOf ` P)" by (metis assms finite_imageI)
  then obtain n where "n ∉ natOf ` P" by (metis unbounded_k_infinite)
  hence "Pvariable n ∉ P" by (metis imageI pvar.sel)
  thus ?thesis using that by auto
qed

definition getFresh :: "pvar set ==> pvar" where
"getFresh P ≡ SOME p. p ∉ P"

lemma getFresh:
assumes "finite P" shows "getFresh P ∉ P"
by (metis assms exE_some finite_fresh_pvar getFresh_def)


text ‹The free-variables operator›

primrec FV :: "'aprop dfmla ==> pvar set" where
 "FV (Atom a p) = {p}"
|"FV Fls = {}"
|"FV (Neg φ) = FV φ"
|"FV (Dis φ ψ) = FV φ ∪ FV ψ"
|"FV (Next φ) = FV φ"
|"FV (Until φ ψ) = FV φ ∪ FV ψ"
|"FV (Exi p φ) = FV φ - {p}"

text‹Environments›

type_synonym env = "pvar ==> nat"

definition "eqOn P env env1 ≡ ∀ p. p ∈ P ⟶ env p = env1 p"

lemma eqOn_Un[simp]:
"eqOn (P ∪ Q) env env1 ⟷ eqOn P env env1 ∧ eqOn Q env env1"
unfolding eqOn_def by auto

lemma eqOn_update[simp]:
"eqOn P (env(p := π)) (env1(p := π)) ⟷ eqOn (P - {p}) env env1"
unfolding eqOn_def by auto

lemma eqOn_singl[simp]:
"eqOn {p} env env1 ⟷ env p = env1 p"
unfolding eqOn_def by auto


context Shallow
begin

subsection ‹The semantic operator›


text‹The semantics will interpret deep (syntactic) formulas as shallow formulas.
  that the latter are predicates on lists of paths -- the interpretation will
  parameterized by an environment mapping each path variable to a number indicating
  index (in the list) for the path denoted by the variable.

  semantics will only
  meaningful if the indexes of a formula's free variables are smaller than the length
  the path list -- we call this property ``compatibility''.›

primrec sem :: "'aprop dfmla ==> env ==> ('state,'aprop) sfmla" where
 "sem (Atom a p) env = atom a (env p)"
|"sem Fls env = fls"
|"sem (Neg φ) env = neg (sem φ env)"
|"sem (Dis φ ψ) env = dis (sem φ env) (sem ψ env)"
|"sem (Next φ) env = next (sem φ env)"
|"sem (Until φ ψ) env = until (sem φ env) (sem ψ env)"
|"sem (Exi p φ) env = exi (λ π πl. sem φ (env(p := length πl)) (πl @ [π]))"

lemma sem_Exi_explicit:
"sem (Exi p φ) env πl ⟷
 (∃ π. wfp AP' π ∧ stateOf π = (if πl ≠ [] then stateOf (last πl) else s0) ∧
       sem φ (env(p := length πl)) (πl @ [π]))"
unfolding sem.simps
unfolding exi_def ..

lemma sem_derived[simp]:
 "sem Tr env = tr"
 "sem (Con φ ψ) env = con (sem φ env) (sem ψ env)"
 "sem (Imp φ ψ) env = imp (sem φ env) (sem ψ env)"
 "sem (Eq φ ψ) env = eq (sem φ env) (sem ψ env)"
 "sem (Fall p φ) env = fall (λ π πl. sem φ (env(p := length πl)) (πl @ [π]))"
 "sem (Ev φ) env = ev (sem φ env)"
 "sem (Alw φ) env = alw (sem φ env)"
 "sem (Wuntil φ ψ) env = wuntil (sem φ env) (sem ψ env)"
unfolding der_Op_defs der_op_defs by (auto simp: neg_def[abs_def])

lemma sem_Fall2[simp]:
"sem (Fall2 p p' φ) env =
 fall2 (λ π' π πl. sem φ (env (p := length πl, p' := Suc(length πl))) (πl @ [π,π']))"
unfolding Fall2_def fall2_def by (auto simp add: fall_def exi_def[abs_def] neg_def[abs_def])


text‹Compatibility of a pair (environment,path list) on a set of variables means
  out-or-range references:›

definition "cpt P env πl ≡ ∀ p ∈ P. env p < length πl"

lemma cpt_Un[simp]:
"cpt (P ∪ Q) env πl ⟷ cpt P env πl ∧ cpt Q env πl"
unfolding cpt_def by auto

lemma cpt_singl[simp]:
"cpt {p} env πl ⟷ env p < length πl"
unfolding cpt_def by auto

lemma cpt_map_stl[simp]:
"cpt P env πl ==> cpt P env (map stl πl)"
unfolding cpt_def by auto


text ‹Next we prove that the semantics of well-formed formulas only depends on the interpretation
  the free variables of a formula and on the current state of the last recorded path --
  call the latter the ``pointer'' of the path list.›

fun pointerOf :: "('state,'aprop) path list ==> 'state" where
"pointerOf πl = (if πl ≠ [] then stateOf (last πl) else s0)"

text‹Equality of two pairs (environment,path list) on a set of variables:›

definition eqOn ::
"pvar set ==> env ==> ('state,'aprop) path list ==> env ==> ('state,'aprop) path list ==> bool"
where
"eqOn P env πl env1 πl1 ≡ ∀ p. p ∈ P ⟶ πl!(env p) = πl1!(env1 p)"

lemma eqOn_Un[simp]:
"eqOn (P ∪ Q) env πl env1 πl1 ⟷ eqOn P env πl env1 πl1 ∧ eqOn Q env πl env1 πl1"
unfolding eqOn_def by auto

lemma eqOn_singl[simp]:
"eqOn {p} env πl env1 πl1 ⟷ πl!(env p) = πl1!(env1 p)"
unfolding eqOn_def by auto

lemma eqOn_map_stl[simp]:
"cpt P env πl ==> cpt P env1 πl1 ==>
 eqOn P env πl env1 πl1 ==> eqOn P env (map stl πl) env1 (map stl πl1)"
unfolding eqOn_def cpt_def by auto

lemma cpt_map_sdrop[simp]:
"cpt P env πl ==> cpt P env (map (sdrop i) πl)"
unfolding cpt_def by auto

lemma cpt_update[simp]:
assumes "cpt (P - {p}) env πl"
shows "cpt P (env(p := length πl)) (πl @ [π])"
using assms unfolding cpt_def by simp (metis Diff_iff less_SucI singleton_iff)

lemma eqOn_map_sdrop[simp]:
"cpt V env πl ==> cpt V env1 πl1 ==>
 eqOn V env πl env1 πl1 ==> eqOn V env (map (sdrop i) πl) env1 (map (sdrop i) πl1)"
unfolding eqOn_def cpt_def by auto

lemma eqOn_update[simp]:
assumes "cpt (P - {p}) env πl" and "cpt (P - {p}) env1 πl1"
shows
"eqOn P (env(p := length πl)) (πl @ [π]) (env1(p := length πl1)) (πl1 @ [π])
 ⟷
 eqOn (P - {p}) env πl env1 πl1"
using assms unfolding eqOn_def cpt_def by simp (metis DiffI nth_append singleton_iff)

lemma eqOn_FV_sem_NE:
assumes "cpt (FV φ) env πl" and "cpt (FV φ) env1 πl1" and "eqOn (FV φ) env πl env1 πl1"
and "πl ≠ []" and "πl1 ≠ []" and "last πl = last πl1"
shows "sem φ env πl = sem φ env1 πl1"
using assms proof (induction φ arbitrary: env πl env1 πl1)
  case (Until φ ψ env πl env1 πl1)
  hence "∧ i. sem φ env (map (sdrop i) πl) = sem φ env1 (map (sdrop i) πl1) ∧
              sem ψ env (map (sdrop i) πl) = sem ψ env1 (map (sdrop i) πl1)"
  using Until by (auto simp: last_map)
  thus ?case by (auto simp: op_defs)
next
  case (Exi p φ env πl env1 πl1)
  hence 1:
  "∧ π. cpt (FV φ) (env(p := length πl)) (πl @ [π]) ∧
         cpt (FV φ) (env1(p := length πl1)) (πl1 @ [π]) ∧
         eqOn (FV φ) (env(p := length πl)) (πl @ [π]) (env1(p := length πl1)) (πl1 @ [π])"
  by simp_all
  thus ?case unfolding sem.simps exi_def using Exi
  by (intro iff_exI) (metis append_is_Nil_conv last_snoc)
qed(auto simp: last_map op_defs)

text‹The next theorem states that the semantics of a formula on an environment
  a list of paths only depends on the pointer of the list of paths.
 ›

theorem eqOn_FV_sem:
assumes "wff φ" and "pointerOf πl = pointerOf πl1"
and "cpt (FV φ) env πl" and "cpt (FV φ) env1 πl1" and "eqOn (FV φ) env πl env1 πl1"
shows "sem φ env πl = sem φ env1 πl1"
using assms proof (induction φ arbitrary: env πl env1 πl1)
  case (Until φ ψ env πl env1 πl1)
  hence "∧ i. sem φ env (map (sdrop i) πl) = sem φ env1 (map (sdrop i) πl1) ∧
              sem ψ env (map (sdrop i) πl) = sem ψ env1 (map (sdrop i) πl1)"
  using Until by (auto simp: last_map)
  thus ?case by (auto simp: op_defs)
next
  case (Exi p φ env πl env1 πl1)
  have "∧ π. sem φ (env(p := length πl)) (πl @ [π]) =
             sem φ (env1(p := length πl1)) (πl1 @ [π])"
  apply(rule eqOn_FV_sem_NE) using Exi by auto
  thus ?case unfolding sem.simps exi_def using Exi by (intro iff_exI conj_cong) simp_all
qed(auto simp: last_map op_defs)

corollary FV_sem:
assumes "wff φ" and "∀ p ∈ FV φ. env p = env1 p"
and "cpt (FV φ) env πl" and "cpt (FV φ) env1 πl"
shows "sem φ env πl = sem φ env1 πl"
apply(rule eqOn_FV_sem)
using assms unfolding eqOn_def by auto

text‹As a consequence, the interpretation of a closed formula (i.e., a formula
  no free variables) will not depend on the environment and, from the
  of paths, will only depend on its pointer:›

corollary interp_closed:
assumes "wff φ" and "FV φ = {}" and "pointerOf πl = pointerOf πl1"
shows "sem φ env πl = sem φ env1 πl1"
apply(rule eqOn_FV_sem)
using assms unfolding eqOn_def cpt_def by auto


text‹Therefore, it makes sense to define the interpretation of a closed formula
  choosing any environment and any list of paths such that its pointer is the initial state
 e.g., the empty list) -- knowing that the choices are irrelevant.›

definition "semClosed φ ≡ sem φ (any::env) (SOME πl. pointerOf πl = s0)"

lemma semClosed:
assumes φ: "wff φ" "FV φ = {}" and p: "pointerOf πl = s0"
shows "semClosed φ = sem φ env πl"
proof-
  have "pointerOf (SOME πl. pointerOf πl = s0) = s0"
  by (rule someI[of _ "[]"]) simp
  thus ?thesis unfolding semClosed_def using interp_closed[OF φ] p by auto
qed

lemma semClosed_Nil:
assumes φ: "wff φ" "FV φ = {}"
shows "semClosed φ = sem φ env []"
using assms semClosed by auto



subsection‹The conjunction of a finite set of formulas›


text‹This is defined by making the set into a list (by choosing any ordering of the
 ) and iterating binary conjunction.›

definition Scon :: "'aprop dfmla set ==> 'aprop dfmla" where
"Scon φs ≡ foldr Con (asList φs) Tr"

lemma sem_Scon[simp]:
assumes "finite φs"
shows "sem (Scon φs) env = scon ((λ φ. sem φ env) ` φs)"
proof-
  define φl where "φl = asList φs"
  have "sem (foldr Con φl Tr) env = scon ((λ φ. sem φ env) ` (set φl))"
  by (induct φl) (auto simp: scon_def)
  thus ?thesis unfolding φl_def Scon_def by (metis assms set_asList)
qed

lemma FV_Scon[simp]:
assumes "finite φs"
shows "FV (Scon φs) = ∪ (FV ` φs)"
proof-
  define φl where "φl = asList φs"
  have "FV (foldr Con φl Tr) = ∪ (set (map FV φl))"
  by (induct φl) (auto simp: der_Op_defs)
  thus ?thesis unfolding φl_def Scon_def by (metis assms set_map set_asList)
qed



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

text‹end-of-context Shallow›


(*<*)
end
(*>*)