Theory MTX_Examples

(*  Title:       Verification Examples
    Author:      Jonathan Julián Huerta y Munive, 2021
    Maintainer:  Jonathan Julián Huerta y Munive <jonjulian23@gmail.com>
*)

section ‹ Verification examples ›


theory MTX_Examples
  imports 
    MTX_Flows 
    Hybrid_Systems_VCs.HS_VC_Spartan

begin


subsection ‹ Examples ›

abbreviation hoareT :: "('a ⇒ bool) ⇒ ('a ⇒ 'a set) ⇒ ('a ⇒ bool) ⇒ bool" 
  (‹PRE_ HP _ POST _› [85,85]85) where "PRE P HP X POST Q ≡ (P ≤ |X]Q)"


subsubsection ‹ Verification by uniqueness. ›

abbreviation mtx_circ :: "2 sq_mtx" (‹A›)
  where "A ≡ mtx  
   ([0,  1] # 
    [-1, 0] # [])"

abbreviation mtx_circ_flow :: "real ⇒ real^2 ⇒ real^2" (‹φ›)
  where "φ t s ≡ (χ i. if i = 1 then s$1 * cos t + s$2 * sin t else - s$1 * sin t + s$2 * cos t)"

lemma mtx_circ_flow_eq: "exp (t *R A) *V s = φ t s"
  apply(rule local_flow.eq_solution[OF local_flow_sq_mtx_linear, symmetric, of _ "λs. UNIV"], simp_all)
    apply(rule ivp_solsI, simp_all add: sq_mtx_vec_mult_eq vec_eq_iff)
  unfolding UNIV_2 using exhaust_2
  by (force intro!: poly_derivatives simp: matrix_vector_mult_def)+

lemma mtx_circ: 
  "PRE(λs. r2 = (s $ 1)2 + (s $ 2)2) 
  HP x´=(*V) A & G 
  POST (λs. r2 = (s $ 1)2 + (s $ 2)2)"
  apply(subst local_flow.fbox_g_ode_subset[OF local_flow_sq_mtx_linear])
  unfolding mtx_circ_flow_eq by auto

no_notation mtx_circ (‹A›)
        and mtx_circ_flow (‹φ›)


subsubsection ‹ Flow of diagonalisable matrix. ›

abbreviation mtx_hOsc :: "real ⇒ real ⇒ 2 sq_mtx" (‹A›)
  where "A a b ≡ mtx  
   ([0, 1] # 
    [a, b] # [])"

abbreviation mtx_chB_hOsc :: "real ⇒ real ⇒ 2 sq_mtx" (‹P›)
  where "P a b ≡ mtx
   ([a, b] # 
    [1, 1] # [])"

lemma inv_mtx_chB_hOsc: 
  "a ≠ b ⟹ (P a b)-1 = (1/(a - b)) *R mtx 
   ([ 1, -b] # 
    [-1,  a] # [])"
  apply(rule sq_mtx_inv_unique, unfold scaleR_mtx2 times_mtx2)
  by (simp add: diff_divide_distrib[symmetric] one_mtx2)+

lemma invertible_mtx_chB_hOsc: "a ≠ b ⟹ mtx_invertible (P a b)"
  apply(rule mtx_invertibleI[of _ "(P a b)-1"])
   apply(unfold inv_mtx_chB_hOsc scaleR_mtx2 times_mtx2 one_mtx2)
  by (subst sq_mtx_eq_iff, simp add: vector_def frac_diff_eq1)+

lemma mtx_hOsc_diagonalizable:
  fixes a b :: real
  defines "ι1 ≡ (b - sqrt (b^2+4*a))/2" and "ι2 ≡ (b + sqrt (b^2+4*a))/2"
  assumes "b2 + a * 4 > 0" and "a ≠ 0"
  shows "A a b = P (-ι2/a) (-ι1/a) * (𝖽𝗂𝖺𝗀 i. if i = 1 then ι1 else ι2) * (P (-ι2/a) (-ι1/a))-1"
  unfolding assms apply(subst inv_mtx_chB_hOsc)
  using assms(3,4) apply(simp_all add: diag2_eq[symmetric])
  unfolding sq_mtx_times_eq sq_mtx_scaleR_eq UNIV_2 apply(subst sq_mtx_eq_iff)
  using exhaust_2 assms by (auto simp: field_simps, auto simp: field_power_simps)

lemma mtx_hOsc_solution_eq:
  fixes a b :: real
  defines "ι1 ≡ (b - sqrt (b2+4*a))/2" and "ι2 ≡ (b + sqrt (b2+4*a))/2"
  defines "Φ t ≡ mtx (
   [ι2*exp(t*ι1) - ι1*exp(t*ι2),     exp(t*ι2)-exp(t*ι1)]#
   [a*exp(t*ι2) - a*exp(t*ι1), ι2*exp(t*ι2)-ι1*exp(t*ι1)]#[])"
  assumes "b2 + a * 4 > 0" and "a ≠ 0"
  shows "P (-ι2/a) (-ι1/a) * (𝖽𝗂𝖺𝗀 i. exp (t * (if i=1 then ι1 else ι2))) * (P (-ι2/a) (-ι1/a))-1 
  = (1/sqrt (b2 + a * 4)) *R (Φ t)"
  unfolding assms apply(subst inv_mtx_chB_hOsc)
  using assms apply(simp_all add: mtx_times_scaleR_commute, subst sq_mtx_eq_iff)
  unfolding UNIV_2 sq_mtx_times_eq sq_mtx_scaleR_eq sq_mtx_uminus_eq apply(simp_all add: axis_def)
  by (auto simp: field_simps, auto simp: field_power_simps)+
 
lemma local_flow_mtx_hOsc:
  fixes a b
  defines "ι1 ≡ (b - sqrt (b^2+4*a))/2" and "ι2 ≡ (b + sqrt (b^2+4*a))/2"
  defines "Φ t ≡ mtx (
   [ι2*exp(t*ι1) - ι1*exp(t*ι2),     exp(t*ι2)-exp(t*ι1)]#
   [a*exp(t*ι2) - a*exp(t*ι1), ι2*exp(t*ι2)-ι1*exp(t*ι1)]#[])"
  assumes "b2 + a * 4 > 0" and "a ≠ 0"
  shows "local_flow ((*V) (A a b)) UNIV UNIV (λt. (*V) ((1/sqrt (b2 + a * 4)) *R Φ t))"
  unfolding assms using local_flow_sq_mtx_linear[of "A a b"] assms
  apply(subst (asm) exp_scaleR_diagonal2[OF invertible_mtx_chB_hOsc mtx_hOsc_diagonalizable])
     apply(simp, simp, simp)
  by (subst (asm) mtx_hOsc_solution_eq) simp_all

lemma overdamped_door_arith:
  assumes "b2 + a * 4 > 0" and "a < 0" and "b ≤ 0" and "t ≥ 0" and "s1 > 0"
  shows "0 ≤ ((b + sqrt (b2 + 4 * a)) * exp (t * (b - sqrt (b2 + 4 * a)) / 2) / 2 - 
(b - sqrt (b2 + 4 * a)) * exp (t * (b + sqrt (b2 + 4 * a)) / 2) / 2) * s1 / sqrt (b2 + a * 4)"
proof(subst diff_divide_distrib[symmetric], simp)
  have f0: "s1 / (2 * sqrt (b2 + a * 4)) > 0"  (is "s1/?c3 > 0")
    using assms(1,5) by simp
  have f1: "(b - sqrt (b2 + 4 * a)) < (b + sqrt (b2 + 4 * a))" (is "?c2 < ?c1") 
    and f2: "(b + sqrt (b2 + 4 * a)) < 0"
    using sqrt_ge_absD[of b "b2 + 4 * a"] assms by (force, linarith)
  hence f3: "exp (t * ?c2 / 2) ≤ exp (t * ?c1 / 2)" (is "exp ?t1 ≤ exp ?t2")
    unfolding exp_le_cancel_iff 
    using assms(4) by (case_tac "t=0", simp_all)
  hence "?c2 * exp ?t2 ≤ ?c2 * exp ?t1"
    using f1 f2 mult_le_cancel_left_pos[of "-?c2" "exp ?t1" "exp ?t2"] by linarith 
  also have "... < ?c1 * exp ?t1"
    using f1 by auto
  also have"... ≤ ?c1 * exp ?t1"
    using f1 f2 by auto
  ultimately show "0 ≤ (?c1 * exp ?t1 - ?c2 * exp ?t2) * s1 / ?c3"
    using f0 f1 assms(5) by auto
qed

abbreviation "open_door s ≡ {s. s$1 > 0 ∧ s$2 = 0}"

lemma overdamped_door:
  assumes "b2 + a * 4 > 0" and "a < 0" and "b ≤ 0"
  shows "PRE (λs. s$1 = 0)
  HP (LOOP open_door; (x´=((*V) (A a b)) & G) INV (λs. 0 ≤ s$1))
  POST (λs. 0 ≤ s $ 1)"
  apply(rule fbox_loopI, simp_all add: le_fun_def)
  apply(subst local_flow.fbox_g_ode_subset[OF local_flow_mtx_hOsc[OF assms(1)]])
  using assms apply(simp_all add: le_fun_def fbox_def)
  unfolding sq_mtx_scaleR_eq UNIV_2 sq_mtx_vec_mult_eq
  by (clarsimp simp: overdamped_door_arith)


no_notation mtx_hOsc (‹A›)
        and mtx_chB_hOsc (‹P›)


subsubsection ‹ Flow of non-diagonalisable matrix. ›

abbreviation mtx_cnst_acc :: "3 sq_mtx" (‹K›)
  where "K ≡ mtx (
  [0,1,0] #
  [0,0,1] # 
  [0,0,0] # [])"

lemma pow2_scaleR_mtx_cnst_acc: "(t *R K)2 = mtx (
  [0,0,t2] #
  [0,0,0] # 
  [0,0,0] # [])"
  unfolding power2_eq_square apply(subst sq_mtx_eq_iff)
  unfolding sq_mtx_times_eq UNIV_3 by auto

lemma powN_scaleR_mtx_cnst_acc: "n > 2 ⟹ (t *R K)^n = 0"
  apply(induct n, simp, case_tac "n ≤ 2")
   apply(subgoal_tac "n = 2", erule ssubst)
  unfolding power_Suc2 pow2_scaleR_mtx_cnst_acc sq_mtx_times_eq UNIV_3
  by (auto simp: sq_mtx_eq_iff)

lemma exp_mtx_cnst_acc: "exp (t *R K) = ((t *R K)2/R 2) + (t *R K) + 1"
  unfolding exp_def apply(subst suminf_eq_sum[of 2])
  using powN_scaleR_mtx_cnst_acc by (simp_all add: numeral_2_eq_2)
 
lemma exp_mtx_cnst_acc_simps:
  "exp (t *R K) $$ 1 $ 1 = 1" "exp (t *R K) $$ 1 $ 2 = t" "exp (t *R K) $$ 1 $ 3 = t^2/2"
  "exp (t *R K) $$ 2 $ 1 = 0" "exp (t *R K) $$ 2 $ 2 = 1" "exp (t *R K) $$ 2 $ 3 = t"
  "exp (t *R K) $$ 3 $ 1 = 0" "exp (t *R K) $$ 3 $ 2 = 0" "exp (t *R K) $$ 3 $ 3 = 1"
  unfolding exp_mtx_cnst_acc one_mtx3 pow2_scaleR_mtx_cnst_acc by simp_all

lemma exp_mtx_cnst_acc_vec_mult_eq: "exp (t *R K) *V s = 
  vector [s$3 * t^2/2 + s$2 * t + s$1, s$3 * t + s$2, s$3]"
  apply(subst exp_mtx_cnst_acc, subst pow2_scaleR_mtx_cnst_acc)
  apply(simp add: sq_mtx_vec_mult_eq vector_def)
  unfolding UNIV_3 by (simp add: fun_eq_iff)

lemma local_flow_mtx_cnst_acc:
  "local_flow ((*V) K) UNIV UNIV (λt s. ((t *R K)2/R 2 + (t *R K) + 1) *V s)"
  using local_flow_sq_mtx_linear[of K] unfolding exp_mtx_cnst_acc .  

lemma docking_station_arith:
  assumes "(d::real) > x" and "v > 0"
  shows "(v = v2 * t / (2 * d - 2 * x)) ⟷ (v * t - v2 * t2 / (4 * d - 4 * x) + x = d)"
proof
  assume "v = v2 * t / (2 * d - 2 * x)"
  hence "v * t = 2 * (d - x)"
    using assms by (simp add: eq_divide_eq power2_eq_square) 
  hence "v * t - v2 * t2 / (4 * d - 4 * x) + x = 2 * (d - x) - 4 * (d - x)2 / (4 * (d - x)) + x"
    apply(subst power_mult_distrib[symmetric])
    by (erule ssubst, subst power_mult_distrib, simp)
  also have "... = d"
    apply(simp only: mult_divide_mult_cancel_left_if)
    using assms by (auto simp: power2_eq_square)
  finally show "v * t - v2 * t2 / (4 * d - 4 * x) + x = d" .
next
  assume "v * t - v2 * t2 / (4 * d - 4 * x) + x = d"
  hence "0 = v2 * t2 / (4 * (d - x)) + (d - x) - v * t"
    by auto
  hence "0 = (4 * (d - x)) * (v2 * t2 / (4 * (d - x)) + (d - x) - v * t)"
    by auto
  also have "... = v2 * t2 + 4 * (d - x)2  - (4 * (d - x)) * (v * t)"
    using assms apply(simp add: distrib_left right_diff_distrib)
    apply(subst right_diff_distrib[symmetric])+
    by (simp add: power2_eq_square)
  also have "... = (v * t - 2 * (d - x))2"
    by (simp only: power2_diff, auto simp: field_simps power2_diff)
  finally have "0 = (v * t - 2 * (d - x))2" .
  hence "v * t = 2 * (d - x)"
    by auto
  thus "v = v2 * t / (2 * d - 2 * x)"
    apply(subst power2_eq_square, subst mult.assoc)
    apply(erule ssubst, subst right_diff_distrib[symmetric])
    using assms by auto
qed

lemma docking_station:
  assumes "d > x0" and "v0 > 0"
  shows "PRE (λs. s$1 = x0 ∧ s$2 = v0)
  HP ((3 ::= (λs. -(v0^2/(2*(d-x0))))); x´=(*V) K & G)
  POST (λs. s$2 = 0 ⟷ s$1 = d)"
  apply(clarsimp simp: le_fun_def local_flow.fbox_g_ode_subset[OF local_flow_sq_mtx_linear[of K]])
  unfolding exp_mtx_cnst_acc_vec_mult_eq using assms by (simp add: docking_station_arith)

no_notation mtx_cnst_acc (‹K›)

end