chapter ‹Symbolic Primitives for Building Runs›
theory SymbolicPrimitive
imports Run
keywords
"reflect_ML_exports" :: thy_decl
begin
text‹
We define here the primitive constraints on runs, towards which we translate
TESL specifications in the operational semantics.
These constraints refer to a specific symbolic run and can therefore access
properties of the run at particular instants (for instance, the fact that a clock
ticks at instant @{term ‹n›} of the run, or the time on a given clock at
that instant).
In the previous chapters, we had no reference to particular instants of a run
because the TESL language should be invariant by stuttering in order to allow
the composition of specifications: adding an instant where no clock ticks to
a run that satisfies a formula should yield another run that satisfies the
same formula. However, when constructing runs that satisfy a formula, we
need to be able to refer to the time or ticking predicate of a clock at a given
instant.
›
text‹
Counter expressions are used to get the number of ticks of a clock up to
(strictly or not) a given instant index.
›
datatype cnt_expr =
TickCountLess ‹clock› ‹instant_index› (‹#⇧<›)
| TickCountLeq ‹clock› ‹instant_index› (‹#⇧≤›)
subsection‹ Symbolic Primitives for Runs ›
datatype 'τ constr =
Timestamp ‹clock› ‹instant_index› ‹'τ tag_const› (‹_ ⇓ _ @ _›)
| TimestampTvar ‹clock› ‹instant_index› ‹'τ tag_expr› (‹_ ⇓ _ @♯ _›)
| TimeDelay ‹clock› ‹instant_index› ‹'τ tag_const› ‹clock› (‹_ @ _ ⊕ _ ⇒ _›)
| Ticks ‹clock› ‹instant_index› (‹_ ⇑ _›)
| NotTicks ‹clock› ‹instant_index› (‹_ ¬⇑ _›)
| NotTicksUntil ‹clock› ‹instant_index› (‹_ ¬⇑ < _›)
| NotTicksFrom ‹clock› ‹instant_index› (‹_ ¬⇑ ≥ _›)
| TagArith ‹tag_var› ‹tag_var› ‹('τ tag_const × 'τ tag_const) ⇒ bool› (‹⌊_, _⌋ ∈ _›)
| TickCntArith ‹cnt_expr› ‹cnt_expr› ‹(nat × nat) ⇒ bool› (‹⌈_, _⌉ ∈ _›)
| TickCntLeq ‹cnt_expr› ‹cnt_expr› (‹_ ≼ _›)
type_synonym 'τ system = ‹'τ constr list›
text ‹
The abstract machine has configurations composed of:
▪ the past @{term‹Γ›}, which captures choices that have already be made as a
list of symbolic primitive constraints on the run;
▪ the current index @{term ‹n›}, which is the index of the present instant;
▪ the present @{term‹Ψ›}, which captures the formulae that must be satisfied
in the current instant;
▪ the future @{term‹Φ›}, which captures the constraints on the future of the run.
›
type_synonym 'τ config =
‹'τ system * instant_index * 'τ TESL_formula * 'τ TESL_formula›
section ‹Semantics of Primitive Constraints ›
text‹
The semantics of the primitive constraints is defined in a way similar to
the semantics of TESL formulae.
›
fun counter_expr_eval :: ‹('τ::linordered_field) run ⇒ cnt_expr ⇒ nat›
(‹⟦ _ ⊢ _ ⟧⇩c⇩n⇩t⇩e⇩x⇩p⇩r›)
where
‹⟦ ρ ⊢ #⇧< clk indx ⟧⇩c⇩n⇩t⇩e⇩x⇩p⇩r = run_tick_count_strictly ρ clk indx›
| ‹⟦ ρ ⊢ #⇧≤ clk indx ⟧⇩c⇩n⇩t⇩e⇩x⇩p⇩r = run_tick_count ρ clk indx›
fun symbolic_run_interpretation_primitive
::‹('τ::linordered_field) constr ⇒ 'τ run set› (‹⟦ _ ⟧⇩p⇩r⇩i⇩m›)
where
‹⟦ K ⇑ n ⟧⇩p⇩r⇩i⇩m = {ρ. ticks ((Rep_run ρ) n K) }›
| ‹⟦ K @ n⇩0 ⊕ δt ⇒ K' ⟧⇩p⇩r⇩i⇩m =
{ρ. ∀n ≥ n⇩0. first_time ρ K n (time ((Rep_run ρ) n⇩0 K) + δt)
⟶ ticks ((Rep_run ρ) n K')}›
| ‹⟦ K ¬⇑ n ⟧⇩p⇩r⇩i⇩m = {ρ. ¬ticks ((Rep_run ρ) n K) }›
| ‹⟦ K ¬⇑ < n ⟧⇩p⇩r⇩i⇩m = {ρ. ∀i < n. ¬ ticks ((Rep_run ρ) i K)}›
| ‹⟦ K ¬⇑ ≥ n ⟧⇩p⇩r⇩i⇩m = {ρ. ∀i ≥ n. ¬ ticks ((Rep_run ρ) i K) }›
| ‹⟦ K ⇓ n @ τ ⟧⇩p⇩r⇩i⇩m = {ρ. time ((Rep_run ρ) n K) = τ }›
| ‹⟦ K ⇓ n @♯ ⦇τ⇩v⇩a⇩r(K', n') ⊕ δτ⦈ ⟧⇩p⇩r⇩i⇩m = {ρ. time ((Rep_run ρ) n K) = time ((Rep_run ρ) n' K') + δτ }›
| ‹⟦ ⌊τ⇩v⇩a⇩r(C⇩1, n⇩1), τ⇩v⇩a⇩r(C⇩2, n⇩2)⌋ ∈ R ⟧⇩p⇩r⇩i⇩m =
{ ρ. R (time ((Rep_run ρ) n⇩1 C⇩1), time ((Rep_run ρ) n⇩2 C⇩2)) }›
| ‹⟦ ⌈e⇩1, e⇩2⌉ ∈ R ⟧⇩p⇩r⇩i⇩m = { ρ. R (⟦ ρ ⊢ e⇩1 ⟧⇩c⇩n⇩t⇩e⇩x⇩p⇩r, ⟦ ρ ⊢ e⇩2 ⟧⇩c⇩n⇩t⇩e⇩x⇩p⇩r) }›
| ‹⟦ cnt_e⇩1 ≼ cnt_e⇩2 ⟧⇩p⇩r⇩i⇩m = { ρ. ⟦ ρ ⊢ cnt_e⇩1 ⟧⇩c⇩n⇩t⇩e⇩x⇩p⇩r ≤ ⟦ ρ ⊢ cnt_e⇩2 ⟧⇩c⇩n⇩t⇩e⇩x⇩p⇩r }›
text‹
The composition of primitive constraints is their conjunction, and we get the
set of satisfying runs by intersection.
›
fun symbolic_run_interpretation
::‹('τ::linordered_field) constr list ⇒ ('τ::linordered_field) run set›
(‹⟦⟦ _ ⟧⟧⇩p⇩r⇩i⇩m›)
where
‹⟦⟦ [] ⟧⟧⇩p⇩r⇩i⇩m = {ρ. True }›
| ‹⟦⟦ γ # Γ ⟧⟧⇩p⇩r⇩i⇩m = ⟦ γ ⟧⇩p⇩r⇩i⇩m ∩ ⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m›
lemma symbolic_run_interp_cons_morph:
‹⟦ γ ⟧⇩p⇩r⇩i⇩m ∩ ⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ γ # Γ ⟧⟧⇩p⇩r⇩i⇩m›
by auto
definition consistent_context :: ‹('τ::linordered_field) constr list ⇒ bool›
where
‹consistent_context Γ ≡ ( ⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m ≠ {}) ›
subsection ‹Defining a method for witness construction›
text‹
In order to build a run, we can start from an initial run in which no clock
ticks and the time is always 0 on any clock.
›
abbreviation initial_run :: ‹('τ::linordered_field) run› (‹ρ⇩⊙›) where
‹ρ⇩⊙ ≡ Abs_run ((λ_ _. (False, τ⇩c⇩s⇩t 0)) ::nat ⇒ clock ⇒ (bool × 'τ tag_const))›
text‹
To help avoiding that time flows backward, setting the time on a clock at a given
instant sets it for the future instants too.
›
fun time_update
:: ‹nat ⇒ clock ⇒ ('τ::linordered_field) tag_const ⇒ (nat ⇒ 'τ instant)
⇒ (nat ⇒ 'τ instant)›
where
‹time_update n K τ ρ = (λn' K'. if K = K' ∧ n ≤ n'
then (ticks (ρ n K), τ)
else ρ n' K')›
section ‹Rules and properties of consistence›
lemma context_consistency_preservationI:
‹consistent_context ((γ::('τ::linordered_field) constr)#Γ) ⟹ consistent_context Γ›
unfolding consistent_context_def by auto
inductive context_independency
::‹('τ::linordered_field) constr ⇒ 'τ constr list ⇒ bool› (‹_ ⨝ _›)
where
NotTicks_independency:
‹(K ⇑ n) ∉ set Γ ⟹ (K ¬⇑ n) ⨝ Γ›
| Ticks_independency:
‹(K ¬⇑ n) ∉ set Γ ⟹ (K ⇑ n) ⨝ Γ›
| Timestamp_independency:
‹(∄τ'. τ' = τ ∧ (K ⇓ n @ τ) ∈ set Γ) ⟹ (K ⇓ n @ τ) ⨝ Γ›
section‹Major Theorems›
subsection ‹Interpretation of a context›
text‹
The interpretation of a context is the intersection of the interpretation
of its components.
›
theorem symrun_interp_fixpoint:
‹⋂ ((λγ. ⟦ γ ⟧⇩p⇩r⇩i⇩m) ` set Γ) = ⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m›
by (induction Γ, simp+)
subsection ‹Expansion law›
text ‹Similar to the expansion laws of lattices›
theorem symrun_interp_expansion:
‹⟦⟦ Γ⇩1 @ Γ⇩2 ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ Γ⇩1 ⟧⟧⇩p⇩r⇩i⇩m ∩ ⟦⟦ Γ⇩2 ⟧⟧⇩p⇩r⇩i⇩m›
by (induction Γ⇩1, simp, auto)
section ‹Equations for the interpretation of symbolic primitives›
subsection ‹General laws›
lemma symrun_interp_assoc:
‹⟦⟦ (Γ⇩1 @ Γ⇩2) @ Γ⇩3 ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ Γ⇩1 @ (Γ⇩2 @ Γ⇩3) ⟧⟧⇩p⇩r⇩i⇩m›
by auto
lemma symrun_interp_commute:
‹⟦⟦ Γ⇩1 @ Γ⇩2 ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ Γ⇩2 @ Γ⇩1 ⟧⟧⇩p⇩r⇩i⇩m›
by (simp add: symrun_interp_expansion inf_sup_aci(1))
lemma symrun_interp_left_commute:
‹⟦⟦ Γ⇩1 @ (Γ⇩2 @ Γ⇩3) ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ Γ⇩2 @ (Γ⇩1 @ Γ⇩3) ⟧⟧⇩p⇩r⇩i⇩m›
unfolding symrun_interp_expansion by auto
lemma symrun_interp_idem:
‹⟦⟦ Γ @ Γ ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m›
using symrun_interp_expansion by auto
lemma symrun_interp_left_idem:
‹⟦⟦ Γ⇩1 @ (Γ⇩1 @ Γ⇩2) ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ Γ⇩1 @ Γ⇩2 ⟧⟧⇩p⇩r⇩i⇩m›
using symrun_interp_expansion by auto
lemma symrun_interp_right_idem:
‹⟦⟦ (Γ⇩1 @ Γ⇩2) @ Γ⇩2 ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ Γ⇩1 @ Γ⇩2 ⟧⟧⇩p⇩r⇩i⇩m›
unfolding symrun_interp_expansion by auto
lemmas symrun_interp_aci = symrun_interp_commute
symrun_interp_assoc
symrun_interp_left_commute
symrun_interp_left_idem
lemma symrun_interp_neutral1:
‹⟦⟦ [] @ Γ ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m›
by simp
lemma symrun_interp_neutral2:
‹⟦⟦ Γ @ [] ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m›
by simp
subsection ‹Decreasing interpretation of symbolic primitives›
text‹
Adding constraints to a context reduces the number of satisfying runs.
›
lemma TESL_sem_decreases_head:
‹⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m ⊇ ⟦⟦ γ # Γ ⟧⟧⇩p⇩r⇩i⇩m›
by simp
lemma TESL_sem_decreases_tail:
‹⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m ⊇ ⟦⟦ Γ @ [γ] ⟧⟧⇩p⇩r⇩i⇩m›
by (simp add: symrun_interp_expansion)
text‹
Adding a constraint that is already in the context does not change the
interpretation of the context.
›
lemma symrun_interp_formula_stuttering:
assumes ‹γ ∈ set Γ›
shows ‹⟦⟦ γ # Γ ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m›
proof -
have ‹γ # Γ = [γ] @ Γ› by simp
hence ‹⟦⟦ γ # Γ ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ [γ] ⟧⟧⇩p⇩r⇩i⇩m ∩ ⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m›
using symrun_interp_expansion by simp
thus ?thesis using assms symrun_interp_fixpoint by fastforce
qed
text‹
Removing duplicate constraints from a context does not change the
interpretation of the context.
›
lemma symrun_interp_remdups_absorb:
‹⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ remdups Γ ⟧⟧⇩p⇩r⇩i⇩m›
proof (induction Γ)
case Cons
thus ?case using symrun_interp_formula_stuttering by auto
qed simp
text‹
Two identical sets of constraints have the same interpretation,
the order in the context does not matter.
›
lemma symrun_interp_set_lifting:
assumes ‹set Γ = set Γ'›
shows ‹⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ Γ' ⟧⟧⇩p⇩r⇩i⇩m›
proof -
have ‹set (remdups Γ) = set (remdups Γ')›
by (simp add: assms)
moreover have fxpntΓ: ‹⋂ ((λγ. ⟦ γ ⟧⇩p⇩r⇩i⇩m) ` set Γ) = ⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m›
by (simp add: symrun_interp_fixpoint)
moreover have fxpntΓ': ‹⋂ ((λγ. ⟦ γ ⟧⇩p⇩r⇩i⇩m) ` set Γ') = ⟦⟦ Γ' ⟧⟧⇩p⇩r⇩i⇩m›
by (simp add: symrun_interp_fixpoint)
moreover have ‹⋂ ((λγ. ⟦ γ ⟧⇩p⇩r⇩i⇩m) ` set Γ) = ⋂ ((λγ. ⟦ γ ⟧⇩p⇩r⇩i⇩m) ` set Γ')›
by (simp add: assms)
ultimately show ?thesis using symrun_interp_remdups_absorb by auto
qed
text‹
The interpretation of contexts is contravariant with regard to set inclusion.
›
theorem symrun_interp_decreases_setinc:
assumes ‹set Γ ⊆ set Γ'›
shows ‹⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m ⊇ ⟦⟦ Γ' ⟧⟧⇩p⇩r⇩i⇩m›
proof -
obtain Γ⇩r where decompose: ‹set (Γ @ Γ⇩r) = set Γ'› using assms by auto
hence ‹set (Γ @ Γ⇩r) = set Γ'› using assms by blast
moreover have ‹(set Γ) ∪ (set Γ⇩r) = set Γ'› using assms decompose by auto
moreover have ‹⟦⟦ Γ' ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ Γ @ Γ⇩r ⟧⟧⇩p⇩r⇩i⇩m›
using symrun_interp_set_lifting decompose by blast
moreover have ‹⟦⟦ Γ @ Γ⇩r ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m ∩ ⟦⟦ Γ⇩r ⟧⟧⇩p⇩r⇩i⇩m›
by (simp add: symrun_interp_expansion)
moreover have ‹⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m ⊇ ⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m ∩ ⟦⟦ Γ⇩r ⟧⟧⇩p⇩r⇩i⇩m› by simp
ultimately show ?thesis by simp
qed
lemma symrun_interp_decreases_add_head:
assumes ‹set Γ ⊆ set Γ'›
shows ‹⟦⟦ γ # Γ ⟧⟧⇩p⇩r⇩i⇩m ⊇ ⟦⟦ γ # Γ' ⟧⟧⇩p⇩r⇩i⇩m›
using symrun_interp_decreases_setinc assms by auto
lemma symrun_interp_decreases_add_tail:
assumes ‹set Γ ⊆ set Γ'›
shows ‹⟦⟦ Γ @ [γ] ⟧⟧⇩p⇩r⇩i⇩m ⊇ ⟦⟦ Γ' @ [γ] ⟧⟧⇩p⇩r⇩i⇩m›
proof -
from symrun_interp_decreases_setinc[OF assms] have ‹⟦⟦ Γ' ⟧⟧⇩p⇩r⇩i⇩m ⊆ ⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m› .
thus ?thesis by (simp add: symrun_interp_expansion dual_order.trans)
qed
lemma symrun_interp_absorb1:
assumes ‹set Γ⇩1 ⊆ set Γ⇩2›
shows ‹⟦⟦ Γ⇩1 @ Γ⇩2 ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ Γ⇩2 ⟧⟧⇩p⇩r⇩i⇩m›
by (simp add: Int_absorb1 symrun_interp_decreases_setinc
symrun_interp_expansion assms)
lemma symrun_interp_absorb2:
assumes ‹set Γ⇩2 ⊆ set Γ⇩1›
shows ‹⟦⟦ Γ⇩1 @ Γ⇩2 ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ Γ⇩1 ⟧⟧⇩p⇩r⇩i⇩m›
using symrun_interp_absorb1 symrun_interp_commute assms by blast
section‹Code-Generation›
export_code TickCountLess TickCountLeq
TSchematic
Timestamp
TimeDelay Ticks NotTicks
NotTicksUntil NotTicksFrom TagArith
TickCntArith TickCntLeq
in SML module_name HyggePrimitives
subsection‹Infrastructure for Reflecting exported SML code›
ML‹
fun reflect_local_ML_exports args trans = let
fun eval_ML_context ctxt = let
fun is_sml_file f = String.isSuffix ".ML" (Path.implode (#path f))
val files = (map (Generated_Files.check_files_in (Context.proof_of ctxt)) args)
val ml_files = filter is_sml_file (map #1 (maps Generated_Files.get_files_in files))
val ml_content = map (fn f => Syntax.read_input (#content f)) ml_files
fun eval ml_content = fold (fn sml => (ML_Context.exec
(fn () => ML_Context.eval_source ML_Compiler.flags sml)))
ml_content
in
(eval ml_content #> Local_Theory.propagate_ml_env) ctxt
end
in
Toplevel.generic_theory eval_ML_context trans
end
val files_in_theory =
(Parse.underscore >> K [] || Scan.repeat1 Parse.path_binding) --
Scan.option (\<^keyword>‹(› |-- Parse.!!! (\<^keyword>‹in›
|-- Parse.theory_name --| \<^keyword>‹)›));
val _ =
Outer_Syntax.command \<^command_keyword>‹reflect_ML_exports›
"evaluate generated Standard ML files"
(Parse.and_list1 files_in_theory >> (fn args => reflect_local_ML_exports args));
›
reflect_ML_exports _
ML‹open HyggePrimitives›
end