Theory SymbolicPrimitive

theory SymbolicPrimitive
imports Run
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 =
― ‹@{term ‹c ⇓ n @ τ›} constrains clock @{term ‹c›} to have time @{term ‹τ›}
    at instant @{term ‹n›} of the run.›
  Timestamp     ‹clock›   ‹instant_index› ‹'τ tag_const›         (‹_ ⇓ _ @ _›)
(* TODO: text *)
― ‹@{term ‹c ⇓ n @♯ τexpr›} constrains clock @{term ‹c›} to have time @{term ‹τexpr›}
    at instant @{term ‹n›} of the run.
    @{term ‹τexpr›} refers to the time at some previous instant on a clock›
| TimestampTvar    ‹clock›   ‹instant_index› ‹'τ tag_expr›          (‹_ ⇓ _ @♯ _›)
― ‹@{term ‹m @ n ⊕ δt ⇒ s›} constrains clock @{term ‹s›} to tick at the
    first instant at which the time on @{term ‹m›} has increased by @{term ‹δt›}
    from the value it had at instant @{term ‹n›} of the run.›
| TimeDelay     ‹clock›   ‹instant_index› ‹'τ tag_const› ‹clock› (‹_ @ _ ⊕ _ ⇒ _›)
― ‹@{term ‹c ⇑ n›} constrains clock @{term ‹c›} to tick
    at instant @{term ‹n›} of the run.›
| Ticks         ‹clock›   ‹instant_index›                        (‹_ ⇑ _›)
― ‹@{term ‹c ¬⇑ n›} constrains clock @{term ‹c›} not to tick
    at instant @{term ‹n›} of the run.›
| NotTicks      ‹clock›   ‹instant_index›                        (‹_ ¬⇑ _›)
― ‹@{term ‹c ¬⇑ < n›} constrains clock @{term ‹c›} not to tick
    before instant @{term ‹n›} of the run.›
| NotTicksUntil ‹clock›   ‹instant_index›                        (‹_ ¬⇑ < _›)
― ‹@{term ‹c ¬⇑ ≥ n›} constrains clock @{term ‹c›} not to tick
    at and after instant @{term ‹n›} of the run.›
| NotTicksFrom  ‹clock›   ‹instant_index›                        (‹_ ¬⇑ ≥ _›)
― ‹@{term ‹⌊τ1, τ2⌋ ∈ R›} constrains tag variables @{term ‹τ1›} and  @{term ‹τ2›} 
    to be in relation @{term ‹R›}.›
| TagArith      ‹tag_var› ‹tag_var› ‹('τ tag_const × 'τ tag_const) ⇒ bool› (‹⌊_, _⌋ ∈ _›)
― ‹@{term ‹⌈k1, k2⌉ ∈ R›} constrains counter expressions @{term ‹k1›} and  @{term ‹k2›} 
    to be in relation @{term ‹R›}.›
| TickCntArith  ‹cnt_expr› ‹cnt_expr› ‹(nat × nat) ⇒ bool›      (‹⌈_, _⌉ ∈ _›)
― ‹@{term ‹k1 ≼ k2›} constrains counter expression @{term ‹k1›} to be less or equal 
    to counter expression @{term ‹k2›}.›
| 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›
  (‹⟦ _ ⊢ _ ⟧cntexpr)
where
  ‹⟦ ρ ⊢ #< clk indx ⟧cntexpr = run_tick_count_strictly ρ clk indx›
| ‹⟦ ρ ⊢ # clk indx ⟧cntexpr = run_tick_count ρ clk indx›


fun symbolic_run_interpretation_primitive
  ::‹('τ::linordered_field) constr ⇒ 'τ run set› (‹⟦ _ ⟧prim)
where
  ‹⟦ K ⇑ n  ⟧prim     = {ρ. ticks ((Rep_run ρ) n K) }›
| ‹⟦ K @ n0 ⊕ δt ⇒ K' ⟧prim =
                  {ρ. ∀n ≥ n0. first_time ρ K n (time ((Rep_run ρ) n0 K) + δt)
                               ⟶ ticks ((Rep_run ρ) n K')}›
| ‹⟦ K ¬⇑ n ⟧prim     = {ρ. ¬ticks ((Rep_run ρ) n K) }›
| ‹⟦ K ¬⇑ < n ⟧prim   = {ρ. ∀i < n. ¬ ticks ((Rep_run ρ) i K)}›
| ‹⟦ K ¬⇑ ≥ n ⟧prim   = {ρ. ∀i ≥ n. ¬ ticks ((Rep_run ρ) i K) }›
| ‹⟦ K ⇓ n @ τ ⟧prim = {ρ. time ((Rep_run ρ) n K) = τ }›
| ‹⟦ K ⇓ n @♯ ⦇τvar(K', n') ⊕ δτ⦈ ⟧prim = {ρ. time ((Rep_run ρ) n K) = time ((Rep_run ρ) n' K') + δτ }›
| ‹⟦ ⌊τvar(C1, n1), τvar(C2, n2)⌋ ∈ R ⟧prim =
    { ρ. R (time ((Rep_run ρ) n1 C1), time ((Rep_run ρ) n2 C2)) }›
| ‹⟦ ⌈e1, e2⌉ ∈ R ⟧prim = { ρ. R (⟦ ρ ⊢ e1cntexpr, ⟦ ρ ⊢ e2cntexpr) }›
| ‹⟦ cnt_e1 ≼ cnt_e2prim = { ρ. ⟦ ρ ⊢ cnt_e1cntexpr ≤ ⟦ ρ ⊢ cnt_e2cntexpr }›

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›
  (‹⟦⟦ _ ⟧⟧prim)
where
  ‹⟦⟦ [] ⟧⟧prim = {ρ. True }›
| ‹⟦⟦ γ # Γ ⟧⟧prim = ⟦ γ ⟧prim ∩ ⟦⟦ Γ ⟧⟧prim

lemma symbolic_run_interp_cons_morph:
  ‹⟦ γ ⟧prim ∩ ⟦⟦ Γ ⟧⟧prim = ⟦⟦ γ # Γ ⟧⟧prim
by auto

definition consistent_context :: ‹('τ::linordered_field) constr list ⇒ bool›
where 
  ‹consistent_context Γ ≡ ( ⟦⟦ Γ ⟧⟧prim ≠ {}) ›

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, τcst 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

― ‹This is very restrictive›
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:
  ‹⋂ ((λγ. ⟦ γ ⟧prim) ` set Γ) = ⟦⟦ Γ ⟧⟧prim
by (induction Γ, simp+)

subsection ‹Expansion law›
text ‹Similar to the expansion laws of lattices›

theorem symrun_interp_expansion:
  ‹⟦⟦ Γ1 @ Γ2 ⟧⟧prim = ⟦⟦ Γ1 ⟧⟧prim ∩ ⟦⟦ Γ2 ⟧⟧prim
by (induction Γ1, simp, auto)

section ‹Equations for the interpretation of symbolic primitives› 
subsection ‹General laws›

lemma symrun_interp_assoc:
  ‹⟦⟦ (Γ1 @ Γ2) @ Γ3 ⟧⟧prim = ⟦⟦ Γ1 @ (Γ2 @ Γ3) ⟧⟧prim
by auto

lemma symrun_interp_commute:
  ‹⟦⟦ Γ1 @ Γ2 ⟧⟧prim = ⟦⟦ Γ2 @ Γ1 ⟧⟧prim
by (simp add: symrun_interp_expansion inf_sup_aci(1))

lemma symrun_interp_left_commute:
  ‹⟦⟦ Γ1 @ (Γ2 @ Γ3) ⟧⟧prim = ⟦⟦ Γ2 @ (Γ1 @ Γ3) ⟧⟧prim
unfolding symrun_interp_expansion by auto

lemma symrun_interp_idem:
  ‹⟦⟦ Γ @ Γ ⟧⟧prim = ⟦⟦ Γ ⟧⟧prim
using symrun_interp_expansion by auto

lemma symrun_interp_left_idem:
  ‹⟦⟦ Γ1 @ (Γ1 @ Γ2) ⟧⟧prim = ⟦⟦ Γ1 @ Γ2 ⟧⟧prim
using symrun_interp_expansion by auto

lemma symrun_interp_right_idem:
  ‹⟦⟦ (Γ1 @ Γ2) @ Γ2 ⟧⟧prim = ⟦⟦ Γ1 @ Γ2 ⟧⟧prim
unfolding symrun_interp_expansion by auto

lemmas symrun_interp_aci =  symrun_interp_commute
                            symrun_interp_assoc
                            symrun_interp_left_commute
                            symrun_interp_left_idem

― ‹Identity element›
lemma symrun_interp_neutral1:
  ‹⟦⟦ [] @ Γ ⟧⟧prim = ⟦⟦ Γ ⟧⟧prim
by simp

lemma symrun_interp_neutral2:
  ‹⟦⟦ Γ @ [] ⟧⟧prim = ⟦⟦ Γ ⟧⟧prim
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:
  ‹⟦⟦ Γ ⟧⟧prim ⊇ ⟦⟦ γ # Γ ⟧⟧prim
by simp

lemma TESL_sem_decreases_tail:
  ‹⟦⟦ Γ ⟧⟧prim ⊇ ⟦⟦ Γ @ [γ] ⟧⟧prim
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 ‹⟦⟦ γ # Γ ⟧⟧prim = ⟦⟦ Γ ⟧⟧prim
proof -
  have ‹γ # Γ = [γ] @ Γ› by simp
  hence ‹⟦⟦ γ # Γ ⟧⟧prim = ⟦⟦ [γ] ⟧⟧prim ∩ ⟦⟦ Γ ⟧⟧prim
    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:
  ‹⟦⟦ Γ ⟧⟧prim = ⟦⟦ remdups Γ ⟧⟧prim
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 ‹⟦⟦ Γ ⟧⟧prim = ⟦⟦ Γ' ⟧⟧prim
proof -     
  have ‹set (remdups Γ) = set (remdups Γ')›
    by (simp add: assms)
  moreover have fxpntΓ: ‹⋂ ((λγ. ⟦ γ ⟧prim) ` set Γ) = ⟦⟦ Γ ⟧⟧prim
    by (simp add: symrun_interp_fixpoint)
  moreover have fxpntΓ': ‹⋂ ((λγ. ⟦ γ ⟧prim) ` set Γ') = ⟦⟦ Γ' ⟧⟧prim
    by (simp add: symrun_interp_fixpoint)
  moreover have ‹⋂ ((λγ. ⟦ γ ⟧prim) ` set Γ) = ⋂ ((λγ. ⟦ γ ⟧prim) ` 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 ‹⟦⟦ Γ ⟧⟧prim ⊇ ⟦⟦ Γ' ⟧⟧prim
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 ‹⟦⟦ Γ' ⟧⟧prim = ⟦⟦ Γ @ Γr ⟧⟧prim
    using symrun_interp_set_lifting decompose by blast
  moreover have ‹⟦⟦ Γ @ Γr ⟧⟧prim = ⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ Γr ⟧⟧prim
    by (simp add: symrun_interp_expansion)
  moreover have ‹⟦⟦ Γ ⟧⟧prim ⊇ ⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ Γr ⟧⟧prim by simp
  ultimately show ?thesis by simp
qed

lemma symrun_interp_decreases_add_head:
  assumes ‹set Γ ⊆ set Γ'›
    shows ‹⟦⟦ γ # Γ ⟧⟧prim ⊇ ⟦⟦ γ # Γ' ⟧⟧prim
using symrun_interp_decreases_setinc assms by auto

lemma symrun_interp_decreases_add_tail:
  assumes ‹set Γ ⊆ set Γ'›
    shows ‹⟦⟦ Γ @ [γ] ⟧⟧prim ⊇ ⟦⟦ Γ' @ [γ] ⟧⟧prim
proof -
  from symrun_interp_decreases_setinc[OF assms] have ‹⟦⟦ Γ' ⟧⟧prim ⊆ ⟦⟦ Γ ⟧⟧prim .
  thus ?thesis by (simp add: symrun_interp_expansion dual_order.trans)
qed

lemma symrun_interp_absorb1:
  assumes ‹set Γ1 ⊆ set Γ2
    shows ‹⟦⟦ Γ1 @ Γ2 ⟧⟧prim = ⟦⟦ Γ2 ⟧⟧prim
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 ⟧⟧prim = ⟦⟦ Γ1 ⟧⟧prim
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