Theory LTL_alike
subsection ‹Termporal Combinators›
theory
LTL_alike
imports
Main
begin
text‹
In the following, we present a small embbeding of temporal combinators, that may help to
formulate typical temporal properties in traces and protocols concisely. It is based on
\emph{finite} lists, therefore the properties of this logic are not fully compatible with
LTL based on Kripke-structures. For the purpose of this demonstration, however, the difference
does not matter.
›
fun nxt :: "('α list ⇒ bool) ⇒ 'α list ⇒ bool" (‹N›)
where
"nxt p [] = False"
| "nxt p (a # S) = (p S)"
text‹Predicate $p$ holds at first position.›
fun atom :: "('α ⇒ bool) ⇒ 'α list ⇒ bool" (‹«_»›)
where
"atom p [] = False"
| "atom p (a # S) = (p a)"
lemma holds_mono : "«q» s ⟹ «q» (s @ t)"
by(cases "s",simp_all)
fun always :: "('α list ⇒ bool) ⇒ 'α list ⇒ bool" (‹□›)
where
"always p [] = True"
| "always p (a # S) = ((p (a # S)) ∧ always p S)"
text‹
Always is a generalization of the \verb+list_all+ combinator from the List-library; if arguing
locally, this paves the way to a wealth of library lemmas.
›
lemma always_is_listall : "(□ «p») (t) = list_all (p) (t)"
by(induct "t", simp_all)
fun eventually :: "('α list ⇒ bool) ⇒ 'α list ⇒ bool" (‹♢›)
where
"eventually p [] = False"
| "eventually p (a # S) = ((p (a # S)) ∨ eventually p S)"
text‹
Eventually is a generalization of the \verb+list_ex+ combinator from the List-library; if arguing
locally, this paves the way to a wealth of library lemmas.
›
lemma eventually_is_listex : "(♢ «p») (t) = list_ex (p) (t)"
by(induct "t", simp_all)
text‹
The next two constants will help us later in defining the state transitions. The constant
‹before› is ‹True› if for all elements which appear before the first element
for which ‹q› holds, ‹p› must hold.
›
fun before :: "('α ⇒ bool) ⇒ ('α ⇒ bool) ⇒ 'α list ⇒ bool"
where
"before p q [] = False"
| "before p q (a # S) = (q a ∨ (p a ∧ (before p q S)))"
text‹
Analogously there is an operator ‹not_before› which returns
‹True› if for all elements which appear before the first
element for which ‹q› holds, ‹p› must not hold.
›
fun not_before :: "('α ⇒ bool) ⇒ ('α ⇒ bool) ⇒ 'α list ⇒ bool"
where
"not_before p q [] = False"
| "not_before p q (a # S) = (q a ∨ (¬ (p a) ∧ (not_before p q S)))"
lemma not_before_superfluous:
"not_before p q = before (Not o p) q"
apply(rule ext)
subgoal for n
apply(induct_tac "n")
apply(simp_all)
done
done
text‹General "before":›
fun until :: "('α list ⇒ bool) ⇒ ('α list ⇒ bool) ⇒ 'α list ⇒ bool" (infixl ‹U› 66)
where
"until p q [] = False"
| "until p q (a # S) = (∃ s t. a # S= s @ t ∧ p s ∧ q t)"
text‹This leads to this amazingly tricky proof:›
lemma before_vs_until:
"(before p q) = ((□«p») U «q»)"
proof -
have A:"⋀a. q a ⟹ (∃s t. [a] = s @ t ∧ □ «p» s ∧ «q» t)"
apply(rule_tac x="[]" in exI)
apply(rule_tac x="[a]" in exI, simp)
done
have B:"⋀a. (∃s t. [a] = s @ t ∧ □ «p» s ∧ «q» t) ⟹ q a"
apply auto
apply(case_tac "t=[]", auto simp:List.neq_Nil_conv)
apply(case_tac "s=[]", auto simp:List.neq_Nil_conv)
done
have C:"⋀a aa list.(q a ∨ p a ∧ (∃s t. aa # list = s @ t ∧ □ «p» s ∧ «q» t))
⟹ (∃s t. a # aa # list = s @ t ∧ □ «p» s ∧ «q» t)"
apply auto[1]
apply(rule_tac x="[]" in exI)
apply(rule_tac x="a # aa # list" in exI, simp)
apply(rule_tac x="a # s" in exI)
apply(rule_tac x="t" in exI,simp)
done
have D:"⋀a aa list.(∃s t. a # aa # list = s @ t ∧ □ «p» s ∧ «q» t)
⟹ (q a ∨ p a ∧ (∃s t. aa # list = s @ t ∧ □ «p» s ∧ «q» t))"
apply auto[1]
apply(case_tac "s", auto simp:List.neq_Nil_conv)
apply(case_tac "s", auto simp:List.neq_Nil_conv)
done
show ?thesis
apply(rule ext)
subgoal for n
apply(induct_tac "n")
apply(simp)
subgoal for x xs
apply(case_tac "xs")
apply(simp,rule iffI,erule A, erule B)
apply(simp,rule iffI,erule C, erule D)
done
done
done
qed
end