Theory Bound_Effect

theory "Bound_Effect"
imports
  Ordinary_Differential_Equations.ODE_Analysis
  "Ids"
  "Lib"
  "Syntax"
  "Denotational_Semantics"
  "Frechet_Correctness"
  "Static_Semantics"
  "Coincidence"
begin
section ‹Bound Effect Theorem›
text ‹The bound effect lemma says that a program can only modify its bound variables and nothing else.
  This is one of the major lemmas for showing correctness of uniform substitution. ›

context ids begin
lemma bound_effect:
  fixes I::"('sf,'sc,'sz) interp"
  assumes good_interp:"is_interp I"
  shows "⋀ν :: 'sz state. ⋀ω ::'sz state. hpsafe α ⟹ (ν, ω) ∈ prog_sem I α ⟹ Vagree ν ω (- (BVP α))"
proof (induct rule: hp_induct)
  case Var then show "?case" 
    using agree_nil Compl_UNIV_eq BVP.simps(1) by fastforce
next
  case Test then show "?case"
    by auto(simp add: agree_refl Compl_UNIV_eq Vagree_def)
next
  case (Choice a b ν ω)
  assume IH1:"⋀ν'. ⋀ω'. hpsafe a ⟹((ν', ω') ∈ prog_sem I a ⟹ Vagree ν' ω' (- BVP a))"
  assume IH2:"⋀ν'. ⋀ω'. hpsafe b ⟹((ν', ω') ∈ prog_sem I b ⟹ Vagree ν' ω' (- BVP b))"
  assume sem:"(ν, ω) ∈ prog_sem I (a ∪∪ b)"
  assume safe:"hpsafe (Choice a b)"
  from safe have safes:"hpsafe a" "hpsafe b" by (auto dest: hpsafe.cases)
  have sems:"(ν, ω) ∈ prog_sem I (a) ∨ (ν, ω) ∈ prog_sem I (b)" using sem by auto
  have agrees:"Vagree ν ω (- BVP a) ∨ Vagree ν ω (- BVP b)" using IH1 IH2 sems safes by blast
  have sub1:"-(BVP a) ⊇ (- BVP a ∩ - BVP b)" by auto
  have sub2:"-(BVP a) ⊇ (- BVP a ∩ - BVP b)" by auto
  have res:"Vagree ν ω (- BVP a ∩ - BVP b)" using agrees sub1 sub2 agree_supset by blast
  then show "?case" by auto
next
  case (Compose a b ν ω) 
  assume IH1:"⋀ν'. ⋀ω'. hpsafe a ⟹ (ν', ω') ∈ prog_sem I a ⟹ Vagree ν' ω' (- BVP a)"
  assume IH2:"⋀ν'. ⋀ω'. hpsafe b ⟹ (ν', ω') ∈ prog_sem I b ⟹ Vagree ν' ω' (- BVP b)"
  assume sem:"(ν, ω) ∈ prog_sem I (a ;; b)"
  assume safe:"hpsafe (a ;; b)"
  from safe have safes:"hpsafe a" "hpsafe b" by (auto dest: hpsafe.cases)  
  then show "?case" 
    using agree_trans IH1 IH2 sem safes by fastforce
next
  fix ODE::"('sf,'sz) ODE" and P::"('sf,'sc,'sz) formula" and ν ω
  assume safe:"hpsafe (EvolveODE ODE P)"
  from safe have osafe:"osafe ODE" and fsafe:"fsafe P" by (auto dest: hpsafe.cases)
  show "(ν, ω) ∈ prog_sem I (EvolveODE ODE P) ⟹ Vagree ν ω (- BVP (EvolveODE ODE P))"
  proof -
    assume sem:"(ν, ω) ∈ prog_sem I (EvolveODE ODE P)"
    from sem have agree:"Vagree ν ω (- BVO ODE)"
      apply(simp only: prog_sem.simps(8) mem_Collect_eq osafe fsafe)
      apply(erule exE)+
    proof -
      fix ν' sol t  
      assume assm:
        "(ν, ω) = (ν', mk_v I ODE ν' (sol t)) ∧
         0 ≤ t ∧
         (sol solves_ode (λ_. ODE_sem I ODE)) {0..t} {x. mk_v I ODE ν' x ∈ fml_sem I P} ∧  (sol 0) = (fst ν')"
      have semBV:"-BVO ODE ⊆ -semBV I ODE"
        by(induction ODE, auto)
      from assm have "Vagree ω ν (- BVO ODE)" using mk_v_agree[of I ODE ν "(sol t)"] 
        using agree_sub[OF semBV] by auto
      thus  "Vagree ν ω (- BVO ODE)" by (rule agree_comm)
    qed 
    thus "Vagree ν ω (- BVP (EvolveODE ODE P))" by auto
  qed
next
  case (Star a ν ω) then
  have IH:"(⋀ν ω. hpsafe a ⟹ (ν, ω) ∈ prog_sem I a ⟹ Vagree ν ω (- BVP a))"
    and safe:"hpsafe a**"
    and sem:"(ν, ω) ∈ prog_sem I a**"
    by auto
  from safe have asafe:"hpsafe a" by (auto dest: hpsafe.cases)
  show "Vagree ν ω (- BVP a**)" 
    using sem apply (simp only: prog_sem.simps)
    apply (erule converse_rtrancl_induct)
     subgoal by(rule agree_refl)
    subgoal for y z using IH[of y z, OF asafe] sem by (auto simp add: Vagree_def)
    done
qed (auto simp add: Vagree_def)
end end