Theory HAKripke
section ‹Kripke Structures as Hierarchical Automata›
theory HAKripke
imports HASem Kripke
begin
type_synonym ('s,'e,'d)hakripke = "(('s,'e,'d)status,('s,'e,'d)atomar)kripke"
type_synonym ('s,'e,'d)hactl = "(('s,'e,'d)status,('s,'e,'d)atomar)ctl"
definition
LabelFunSem :: "('s,'e,'d)hierauto
=> (('s,'e,'d)status ⇀ ((('s,'e,'d) atomar) set))" where
"LabelFunSem a = (λ ST.
(if (HA ST = a) then
(let
In_preds = (λ s. (IN s)) ` (Conf ST);
En_preds = (λ e. (EN e)) ` (Events ST);
Val_preds = { x . (∃ P. (x = (VAL P)) ∧ P (Value ST)) }
in
Some (In_preds ∪ En_preds ∪ Val_preds ∪ {atomar.TRUE}))
else
None))"
definition
HA2Kripke :: "('s,'e,'d)hierauto => ('s,'e,'d)hakripke" where
"HA2Kripke a =
Abs_kripke ({ST. HA ST = a},
{InitStatus a},
StepRelSem a,
LabelFunSem a)"
definition
eval_ctl_HA :: "[('s,'e,'d)hierauto, ('s,'e,'d)hactl]
=> bool" (‹_ |=H= _› [92,91]90) where
"eval_ctl_HA a f = ((HA2Kripke a), (InitStatus a) |=c= f)"
lemma Kripke_HA [simp]:
"Kripke {ST. HA ST = a} {InitStatus a} (StepRelSem a) (LabelFunSem a)"
apply (unfold Kripke_def)
apply auto
apply (unfold StepRelSem_def)
apply auto
apply (unfold LabelFunSem_def Let_def If_def dom_def)
apply auto
prefer 2
apply (rename_tac ST S)
apply (case_tac "HA ST = a")
apply auto
apply (rename_tac ST)
apply (case_tac "HPT ST = {}")
apply auto
apply (rename_tac TSS)
apply (erule_tac x="StepStatus ST TSS (@ u. u : ResolveRacing TSS)" in allE)
apply (erule_tac x=TSS in ballE)
apply auto
done
lemma LabelFun_LabelFunSem [simp]:
"(LabelFun (HA2Kripke a)) = (LabelFunSem a)"
apply (unfold HA2Kripke_def LabelFun_def)
apply auto
apply (subst Abs_kripke_inverse)
apply auto
apply (unfold kripke_def)
apply auto
done
lemma InitStatuses_InitStatus [simp]:
"(InitStatuses (HA2Kripke a)) = {(InitStatus a)}"
apply (unfold HA2Kripke_def InitStatuses_def)
apply simp
apply (subst Abs_kripke_inverse)
apply (unfold kripke_def)
apply auto
done
lemma Statuses_StatusesOfHA [simp]:
"(Statuses (HA2Kripke a)) = {ST. HA ST = a}"
apply (unfold HA2Kripke_def Statuses_def)
apply simp
apply (subst Abs_kripke_inverse)
apply (unfold kripke_def)
apply auto
done
lemma StepRel_StepRelSem [simp]:
"(StepRel (HA2Kripke a)) = (StepRelSem a)"
apply (unfold HA2Kripke_def StepRel_def)
apply simp
apply (subst Abs_kripke_inverse)
apply (unfold kripke_def)
apply auto
done
lemma TRUE_LabelFunSem [simp]:
"atomar.TRUE ∈ the (LabelFunSem (HA ST) ST)"
apply (unfold LabelFunSem_def Let_def)
apply auto
done
lemma FALSE_LabelFunSem [simp]:
"atomar.FALSE ∉ the (LabelFunSem (HA ST) ST)"
apply (unfold LabelFunSem_def Let_def)
apply auto
done
lemma Conf_LabelFunSem [simp]:
"((IN S) ∈ the (LabelFunSem (HA ST) ST)) = (S ∈ (Conf ST))"
apply (unfold LabelFunSem_def Let_def)
apply auto
done
lemma Events_LabelFunSem [simp]:
"((EN S) ∈ the (LabelFunSem (HA ST) ST)) = (S ∈ (Events ST))"
apply (unfold LabelFunSem_def Let_def)
apply auto
done
lemma Value_LabelFunSem [simp]:
"((VAL P) ∈ the (LabelFunSem (HA ST) ST)) = (P (Value ST))"
apply (unfold LabelFunSem_def Let_def)
apply auto
done
lemma AtomTRUE_EvalCTLHA [simp]:
"a |=H= (Atom (atomar.TRUE))"
apply (unfold eval_ctl_HA_def)
apply auto
apply (subst HA_InitStatus [THEN sym])
apply (rule TRUE_LabelFunSem)
done
lemma AtomFalse_EvalCTLHA [simp]:
"¬ a |=H= (Atom (atomar.FALSE))"
apply (unfold eval_ctl_HA_def)
apply auto
apply (subst (asm) HA_InitStatus [THEN sym])
apply (simp only: FALSE_LabelFunSem)
done
lemma Events_InitStatus_EvalCTLHA [simp]:
"(a |=H= (Atom (EN S))) = (S ∈ (Events (InitStatus a)))"
apply (unfold eval_ctl_HA_def)
apply simp
apply (subst HA_InitStatus [THEN sym])
apply (rule Events_LabelFunSem)
done
lemma Conf_InitStatus_EvalCTLHA [simp]:
"(a |=H= (Atom (IN S))) = (S ∈ (Conf (InitStatus a)))"
apply (unfold eval_ctl_HA_def)
apply simp
apply (subst HA_InitStatus [THEN sym])
apply (subst Conf_LabelFunSem)
apply simp
done
lemma HAInitValue_EvalCTLHA [simp]:
"(a |=H= (Atom (VAL P))) = (P (HAInitValue a))"
apply (unfold eval_ctl_HA_def)
apply simp
apply (subst HA_InitStatus [THEN sym])
apply (subst Value_LabelFunSem)
apply auto
done
end