Theory Simulink

(**-----------------------------------------------------------------------------
 * © [I Dragomir, V Preoteasa, S Tripakis]
 *
 * Contributors:
 *  Iulia Dragomir
 *  Viorel Preoteasa
 *
 * This software is governed by the MIT licence and abiding by the rules of
 * distribution of free software. You can use, modify and/or redistribute the
 * software under the terms of the MIT licence included in this distribution.
 *)

subsection‹Formalization of Simulink Blocks as Predicate Transformers›

theory Simulink
  imports Complex_Main "../Feedback/TransitionFeedback" SimulinkTypes
begin

  (* This file defines a library for Simulink blocks formalized as predicate transformers *)

  declare comp_skip [simp del]
  declare skip_comp [simp del]
  declare prod_skip_skip [simp del]
  declare fail_comp [simp del]

  declare [[show_sorts=false]]

  (* Definition of empty input *)

  definition "UnitVal = ()"


  (* Constant block *)

  definition "Constant c = [: x::unit ↝ y. y = c:]"

  lemma Constant_func: "Constant c = [- x ↝ c-]"
    by (simp add: Constant_def update_def)


  (* Inport block *)

  definition "Inport = Skip"


  (* Gain block*)

  definition "Gain k = [:x ↝ y. y = x * k:]"

  lemma Gain_func: "Gain k = [- x ↝ x * k-]"
    by (simp add: update_def Gain_def)


  (* Square power block *)

  definition "Square = [:x ↝ y. y = x * x:]"

  lemma Square_func: "Square =  [- x ↝ x * x-]"
    by (simp add: update_def Square_def)


  (* Power block *)

  definition "Power = [: (x, y) ↝ z. z = x ^ y:]"

  lemma Power_func: "Power = [- x, y ↝ x ^ y-]"
    by (simp add: Power_def update_def split_def)


  (* 10 at the power -input- block *)

  definition "Power10 = [: x ↝ y. y = 10 ^ x:]"

  lemma Power10_func: "Power10 = [- x ↝ 10 ^ x-]"
    by (simp add: Power10_def update_def)


  (* Exponential block *)

  definition "Exp = [: x ↝ y. y = s_exp x :]"

  lemma Exp_func: "Exp = [- x ↝ s_exp x-]"
    by (simp add: Exp_def update_def)


  (* Natural logarithm block *)

  definition "Ln = [: x ↝ y. y = s_ln x:]"

  lemma Ln_func: "Ln = [- x ↝  s_ln x-]"
    by (simp add: Ln_def update_def)


  (* Square root block *)

  definition "Sqrt = {. x. x ≥ 0 .} ∘ [:x ↝ y. y = s_sqrt x:]"

  lemma Sqrt_func: "Sqrt = {. x. x ≥ 0 .} ∘ [- x ↝ s_sqrt x-]"
    by (simp add: update_def Sqrt_def)


  (* Outport block *)

  definition "Outport = Skip"
  

  (* Scope block *)  

  definition "Scope = Skip"


  (* Terminator block *)

  definition "Terminator = [: x ↝ (u::unit). True:]"

  lemma Terminator_func: "Terminator = [-  x ↝ ()-]"
    by (simp add: Terminator_def update_def)


  (* Integrator block *)

  definition "Integrator dt = [:(x,s) ↝ (y, s'). y = s ∧ s' = s + x * dt:]"

  lemma Integrator_func: "Integrator dt = [-x, s ↝ s, s + x * dt-]"
    apply (simp add: Integrator_def update_def)
    apply (rule_tac f = demonic in  HOL.arg_cong)
    by fast

  (* The following definitions correspond to the two components of an Integrator block -- used in the nfb translations *)

  definition "IntegratorA = [:s ↝ y. y = s:]"

  lemma IntegratorA_func: "IntegratorA = [-id-]"
    by (simp add: IntegratorA_def update_def)

  definition "IntegratorB dt = [:(x,s) ↝ s'. s' = s + x * dt:]"

  lemma IntegratorB_func: "IntegratorB dt = [- x, s ↝ s + x * dt-]"
    apply (simp add: IntegratorB_def update_def)
    apply (rule_tac f = demonic in  HOL.arg_cong)
    by fast


  (* Integrator with limit block *)

  definition "IntegratorLimit high low dt = [: (x, s) ↝ (y, s'). y = s ∧ s' = (If s + x * dt > high Then high Else If s + x * dt < low Then low Else s + x * dt):]" 

  lemma IntegratorLimit_func : "IntegratorLimit high low dt = [-  x, s ↝ s, If s + x * dt > high Then high Else If s + x * dt < low Then low Else s + x * dt -]"
    apply (simp add: IntegratorLimit_def update_def)
    apply (rule_tac f = demonic in arg_cong)
    by fast

  (* The following definitions correspond to the two components of an Integrator with limit block -- used in the nfb translations *)

  definition "IntegratorLimitA = [:s ↝ y. y = s:]"

  lemma IntegratorLimitA_func: "IntegratorLimitA = [- id -]"
    by (simp add: IntegratorLimitA_def update_def)

  definition "IntegratorLimitB high low dt = [: (x, s) ↝ y. y = (If s + x * dt > high Then high Else If s + x * dt < low Then low Else s + x * dt) :]"

  lemma IntegratorLimitB_func: "IntegratorLimitB high low dt = [- x, s ↝ If s + x * dt > high Then high Else If s + x * dt < low Then low Else s + x * dt -]"
    apply (simp add: IntegratorLimitB_def update_def)
    apply (rule_tac f = demonic in arg_cong)
    by fast


  (* Saturation block *)

  definition "Saturation low_limit high_limit = [: x ↝ y. 
    y = (If x < low_limit Then low_limit 
    Else If x > high_limit Then high_limit 
         Else x):]"

  lemma Saturation_func: "Saturation low_limit high_limit = 
    [- x ↝ If x < low_limit Then low_limit 
            Else If x > high_limit Then high_limit 
            Else x-]"
    by (simp add: Saturation_def update_def)


  (* Relay block *)

  definition "Relay low_limit high_limit value_low value_high = [: x, s ↝ y, s' . 
    y = (If high_limit ≤ x Then value_high 
    Else (If x ≤ low_limit Then value_low Else s)) 
    ∧ s' = y :]"

  lemma Relay_func: "Relay low_limit high_limit value_low value_high = 
    [- x, s ↝ If high_limit ≤ x Then value_high Else If x ≤ low_limit Then value_low Else s, 
               If high_limit ≤ x Then value_high Else If x ≤ low_limit Then value_low Else s-]"
    apply (simp add: Relay_def update_def)
    apply (rule_tac f = demonic in  HOL.arg_cong)
    by fast

  (* The following definitions correspond to the two components of a Relay block -- used in the nfb translations *)

  definition "RelayA low_limit high_limit value_low value_high = [: x, s ↝ y . 
    y = (If high_limit ≤ x Then value_high 
    Else (If x ≤ low_limit Then value_low Else s)) :]"

  lemma RelayA_func: "RelayA low_limit high_limit value_low value_high = 
    [- x, s ↝ If high_limit ≤ x Then value_high Else If x ≤ low_limit Then value_low Else s-]"
    apply (simp add: RelayA_def update_def)
    apply (rule_tac f = demonic in  HOL.arg_cong)
    by fast

  definition "RelayB low_limit high_limit value_low value_high = [: x, s ↝ s' . 
    s' = (If high_limit ≤ x Then value_high 
    Else (If x ≤ low_limit Then value_low Else s)) :]"

  lemma RelayB_func: "RelayB low_limit high_limit value_low value_high = 
    [- x, s ↝ If high_limit ≤ x Then value_high Else If x ≤ low_limit Then value_low Else s-]"
    apply (simp add: RelayB_def update_def)
    apply (rule_tac f = demonic in  HOL.arg_cong)
    by fast


  (* PulseGenerator block *)

  (* Variant with index for measuring time *)

  definition "PulseGenerator period phase_delay pulse_width amplitude dt = [: (i,c) ↝ y, i',c'. i'=i+1 ∧
    (If (i * dt < phase_delay) Then (y = 0 ∧ c' = 0) Else 
     If (i * dt ≥ phase_delay ∧ (c * dt) < (pulse_width * period) ∧ (pulse_width * period) < period) Then (y=amplitude ∧ (c' = c + 1)) Else
     If (i * dt ≥ phase_delay ∧ (c * dt) ≥ (pulse_width * period) ∧ (c * dt) < (period - dt) ∧ (pulse_width * period) < period) Then (y=0 ∧ (c' = c + 1))
     Else (c' = 0 ∧ y = 0)):]"

  lemma PulseGenerator_func: "PulseGenerator period phase_delay pulse_width amplitude dt =  
    [- i, c ↝
     If (i * dt < phase_delay) Then (0, i + 1, 0) Else 
     If (i * dt ≥ phase_delay ∧ (c * dt) < (pulse_width * period) ∧ (pulse_width * period) < period) Then (amplitude, i+1, c + 1) Else
     If (i * dt ≥ phase_delay ∧ (c * dt) ≥ (pulse_width * period) ∧ (c * dt) < (period - dt) ∧ (pulse_width * period) < period) Then (0, i+1, c + 1)
     Else (0, i+1, 0)-]"
    apply (simp add: PulseGenerator_def update_def)
    apply (rule_tac f = demonic in  HOL.arg_cong)
    by (auto simp add: fun_eq_iff MyIf_def)

  (* The following definitions correspond to the three components of a PulseGenerator block -- used in the nfb translations *)

  definition "PulseGeneratorA period phase_delay pulse_width amplitude dt = [: (i,c) ↝ y.
    (If (i * dt < phase_delay) Then y = 0 Else 
     If (i * dt ≥ phase_delay ∧ (c * dt) < (pulse_width * period) ∧ (pulse_width * period) < period) Then y = amplitude
     Else y = 0):]"

  lemma PulseGeneratorA_func : "PulseGeneratorA period phase_delay pulse_width amplitude dt =  
    [- i, c ↝ 
     If (i * dt < phase_delay) Then 0 Else 
     If (i * dt ≥ phase_delay ∧ (c * dt) < (pulse_width * period) ∧ (pulse_width * period) < period) Then amplitude Else 0 -]"
    apply (simp add: PulseGeneratorA_def update_def)
    apply (rule_tac f = demonic in  HOL.arg_cong)
    by (auto simp add: fun_eq_iff MyIf_def)

  definition "PulseGeneratorB = [: i ↝ i'. i' = i + 1 :]"

  lemma PulseGeneratorB_func: "PulseGeneratorB = [- i ↝ i + 1 -]"
    by (simp add: PulseGeneratorB_def update_def)

  definition "PulseGeneratorC period phase_delay pulse_width dt = [: (i,c) ↝ c'. 
    (If (i * dt < phase_delay) Then c' = 0 Else 
     If (i * dt ≥ phase_delay ∧ (c * dt) < (pulse_width * period) ∧ (pulse_width * period) < period) Then c' = c + 1 Else
     If (i * dt ≥ phase_delay ∧ (c * dt) ≥ (pulse_width * period) ∧ (c * dt) < (period - dt) ∧ (pulse_width * period) < period) Then c' = c + 1
     Else c' = 0) :]"

  lemma PulseGeneratorC_func: "PulseGeneratorC period phase_delay pulse_width dt =  
    [- i, c ↝ 
     If (i * dt < phase_delay) Then 0 Else 
     If (i * dt ≥ phase_delay ∧ (c * dt) < (pulse_width * period) ∧ (pulse_width * period) < period) Then c + 1 Else
     If (i * dt ≥ phase_delay ∧ (c * dt) ≥ (pulse_width * period) ∧ (c * dt) < (period - dt) ∧ (pulse_width * period) < period) Then  c + 1
     Else 0-]"
    apply (simp add: PulseGeneratorC_def update_def)
    apply (rule_tac f = demonic in  HOL.arg_cong)
    by (auto simp add: fun_eq_iff MyIf_def)

  (* Variant with explicit time *)

  (* This is no longer used in the compiler -- to remove     
  definition "PulseGeneratorT period phase_delay pulse_width amplitude dt = [: t, c ↝ y, t', c'. t'= t + dt ∧
    (If (t < phase_delay) Then (y = 0 ∧ c' = 0) Else 
     If (t ≥ phase_delay ∧ c < (pulse_width * period) ∧ (pulse_width * period) < period) Then (y = amplitude ∧ (c' = c + dt)) Else
     If (t ≥ phase_delay ∧ c ≥ (pulse_width * period) ∧ c < (period - dt) ∧ (pulse_width * period) < period) Then (y = 0 ∧ (c' = c + dt))
     Else (c' = 0 ∧ y = 0)):]"
    
  lemma PulseGeneratorT_func: "PulseGeneratorT period phase_delay pulse_width amplitude dt =  
    [-λ (t, c) . 
    (If (t < phase_delay) Then (0, t + dt, 0) Else 
     If (t ≥ phase_delay ∧ c < (pulse_width * period) ∧ (pulse_width * period) < period) Then (amplitude, t + dt, c + dt) Else
     If (t ≥ phase_delay ∧ c ≥ (pulse_width * period) ∧ c < (period - dt) ∧ (pulse_width * period) < period) Then (0, t + dt, c + dt)
     Else (0, t + dt, 0))-]"
    apply (simp add: PulseGeneratorT_def update_def)
    apply (rule_tac f = demonic in  HOL.arg_cong)
    by (auto simp add: fun_eq_iff MyIf_def)    
 *)
      
  definition "PulseGeneratorS period phase_delay pulse_width amplitude dt = [: t ↝ y, t'. 
    (If (t < phase_delay) Then (y = 0 ∧ t'= t + dt) Else 
     If t - phase_delay < period * pulse_width / 100 Then (y = amplitude ∧ t' = t + dt) Else
     If t - phase_delay < period Then (y = 0 ∧ t'= t + dt)
     Else (y = amplitude ∧ t' = t + dt - period)):]"

  lemma PulseGeneratorS_func: "PulseGeneratorS period phase_delay pulse_width amplitude dt = [-  t ↝ 
     If (t < phase_delay) Then (0, t + dt) Else 
     If t - phase_delay < period * pulse_width / 100 Then (amplitude, t + dt) Else
     If t - phase_delay < period Then (0, t + dt)
     Else (amplitude, t + dt - period) -]"
    apply (simp add: PulseGeneratorS_def update_def)
    apply (rule_tac f = demonic in  HOL.arg_cong)
    by (auto simp add: fun_eq_iff MyIf_def)

  (* The following definitions correspond to the three components of a PulseGenerator block -- used in the nfb translations *)

  (* This is no longer used in the compiler -- to remove 
  definition "PulseGeneratorTA period phase_delay pulse_width amplitude dt = PulseGeneratorT period phase_delay pulse_width amplitude dt o [:y, t, c ↝ y' . y = y':]"

  lemma PulseGeneratorTA_func : "PulseGeneratorTA period phase_delay pulse_width amplitude dt =  
    [- t, c ↝  
     If (t < phase_delay) Then 0 Else 
     If (t ≥ phase_delay ∧ c < (pulse_width * period) ∧ (pulse_width * period) < period) Then amplitude Else 0 -]"
    apply (simp add: PulseGeneratorTA_def update_def PulseGeneratorT_def demonic_demonic)
    apply (rule_tac f = demonic in  HOL.arg_cong)
    by (auto simp add: fun_eq_iff MyIf_def OO_def) 

  definition "PulseGeneratorTB dt = [:t ↝ t'. t' = t + dt :]"

  lemma PulseGeneratorTB_func: "PulseGeneratorTB dt = [- λ t . t + dt -]"
    by (simp add: PulseGeneratorTB_def update_def)

  definition "PulseGeneratorTC period phase_delay pulse_width dt = [: t, c ↝ c'. 
    (If (t < phase_delay) Then c' = 0 Else 
     If (t ≥ phase_delay ∧ c < (pulse_width * period) ∧ (pulse_width * period) < period) Then c' = c + dt Else
     If (t ≥ phase_delay ∧ c ≥ (pulse_width * period) ∧ c < (period - dt) ∧ (pulse_width * period) < period) Then c' = c + dt
     Else c' = 0) :]"

  lemma PulseGeneratorTC_func: "PulseGeneratorTC period phase_delay pulse_width dt =  
    [- t, c ↝ 
     If (t < phase_delay) Then 0 Else 
     If (t ≥ phase_delay ∧ c < (pulse_width * period) ∧ (pulse_width * period) < period) Then c + dt Else
     If (t ≥ phase_delay ∧ c ≥ (pulse_width * period) ∧ c < (period - dt) ∧ (pulse_width * period) < period) Then  c + dt
     Else 0 -]"
    apply (simp add: PulseGeneratorTC_def update_def)
    apply (rule_tac f = demonic in  HOL.arg_cong)
    by (auto simp add: fun_eq_iff MyIf_def)
  *)
      
  definition "PulseGeneratorSA period phase_delay pulse_width amplitude dt = PulseGeneratorS period phase_delay pulse_width amplitude dt o [:y, t ↝ y' . y = y':]"

  lemma PulseGeneratorSA_func: "PulseGeneratorSA period phase_delay pulse_width amplitude dt = [-  t ↝ 
     If (t < phase_delay) Then 0 Else 
     If t - phase_delay < period * pulse_width / 100 Then amplitude Else
     If t - phase_delay < period Then 0
     Else amplitude -]"
    apply (simp add: PulseGeneratorSA_def PulseGeneratorS_def update_def demonic_demonic)
    apply (rule_tac f = demonic in  HOL.arg_cong)
    by (auto simp add: fun_eq_iff MyIf_def)
      
  thm PulseGeneratorS_def    
      
  definition "PulseGeneratorSB period phase_delay pulse_width dt = [: t ↝ t'. 
     (If (t < phase_delay) Then t' = t + dt Else 
     If t - phase_delay < period * pulse_width / 100 Then t' = t + dt Else
     If t - phase_delay < period Then t' = t + dt
     Else t' = t + dt - period) :]"

  lemma PulseGeneratorSB_func: "PulseGeneratorSB period phase_delay pulse_width dt = [- λ t . 
    (If (t < phase_delay) Then t + dt Else 
     If t - phase_delay < period * pulse_width / 100 Then t + dt Else
     If t - phase_delay < period Then t + dt
     Else t + dt - period) -]"
    apply (simp add: PulseGeneratorSB_def update_def)
    apply (rule_tac f=demonic in HOL.arg_cong)
    by (simp add: fun_eq_iff MyIf_def)

  lemma PulseGeneratorSB_func_real[simp]: "0 ≤ phase_delay ⟹ 0 < period ⟹ 0 < pulse_width ⟹ pulse_width < 100 ⟹ 
    (λ (t::real) . 
    (If (t < phase_delay) Then t + dt Else 
     If t - phase_delay < period * pulse_width / 100 Then t + dt Else
     If t - phase_delay < period Then t + dt
     Else t + dt - period) )
    = (λ (t::real) . (If t - phase_delay < period Then t + dt Else t + dt - period) )"
    apply (simp add: fun_eq_iff MyIf_def, safe)
    proof -
      fix x
      define a where "a ≡ pulse_width / 100"
      assume " x * 100 - phase_delay * 100 < period * pulse_width"
      from this have D: "x - phase_delay < period * a"
        by (simp add: a_def)
      assume "0 < pulse_width"
      from this have A: "0 < a"
        by (simp add: a_def)
      assume "pulse_width < 100"
      from this have B: "a < 1"
        by (simp add: a_def)
      assume "0 < period"
      from this and A and B have C: "period * a < period"
        by (simp add: mult_less_cancel_left2)
      from C and D show "x - phase_delay < period"
        by auto
    qed


  (* Step block *)

  (* Variant with index for measuring time *)

  definition "Step step_time initial_value final_value dt = [:i ↝ y, i'. i' = i + 1 ∧
    y = (If (i * dt) < step_time Then initial_value Else final_value):]"

  lemma Step_func: "Step step_time initial_value final_value dt = [- i ↝ If (i * dt) < step_time Then initial_value Else final_value, i+1-]"
    apply (simp add: Step_def update_def)
    apply (rule_tac f = demonic in  HOL.arg_cong)
    by (auto)

  (* The following definitions correspond to the two components of a Step block -- used in the nfb translations *)

  definition "StepA step_time initial_value final_value dt = [:i ↝ y. 
    y = (If (i * dt) < step_time Then initial_value Else final_value):]"

  lemma StepA_func: "StepA step_time initial_value final_value dt = [- i ↝ If (i * dt) < step_time Then initial_value Else final_value-]"
    by (simp add: StepA_def update_def)

  definition "StepB = [:i ↝ i'. i' = i + 1:]"

  lemma StepB_func: "StepB = [- i ↝ i+1-]"
    by (simp add: StepB_def update_def)

  (* Variant with explicit time *)

  definition "StepT step_time initial_value final_value dt = [:t ↝ y, t'. t' = t + dt ∧
    y = (If t < step_time Then initial_value Else final_value):]"

  lemma StepT_func: "StepT step_time initial_value final_value dt = [-  t ↝ If t < step_time Then initial_value Else final_value, t + dt-]"
    apply (simp add: StepT_def update_def)
    apply (rule_tac f = demonic in  HOL.arg_cong)
    by (auto)

  (* The following definitions correspond to the two components of a Step block -- used in the nfb translations *)

  definition "StepTA step_time initial_value final_value dt = [:t ↝ y. 
    y = (If t < step_time Then initial_value Else final_value):]"

  lemma StepTA_func: "StepTA step_time initial_value final_value dt = [- t ↝ If t < step_time Then initial_value Else final_value -]"
    by (simp add: StepTA_def update_def)

  definition "StepTB dt = [:t ↝ t'. t' = t + dt:]"

  lemma StepTB_func: "StepTB dt = [- t ↝ t + dt-]"
    by (simp add: StepTB_def update_def)


  (* TransferFcn block *)

  (* General TransfFcn are formalized on-the-fly by the model translator following the instructions from
     http://lpsa.swarthmore.edu/Representations/SysRepTransformations/TF2SS.html
  *)

  (* The following definitions are no longer used -- to check and remove *)
      
  (* Only formulas of type k / (s + a) are handled by the following  definitions 
     k denotes the numerator coefficient, a denotes the denominator coefficient: k / (s + a) 
  *)

  (* Variant with index for measuring time *)  
  definition "TransferFcn k a dt = [:(x, i, s) ↝ (y, i', s'). y = (s * s_exp(a * i * dt) + k * x * s_exp(a * (i + 1) * dt) * dt) / s_exp(a * (i + 1) * dt) ∧
    i' = i + 1 ∧ s' = y:]"

  lemma TransferFcn_func: "TransferFcn k a dt = [- x, i, s ↝ (s * s_exp(a * i * dt) + k * x * s_exp(a * (i + 1) * dt) * dt) / s_exp(a * (i + 1) * dt),
    i+1, (s * s_exp(a * i * dt) + k * x * s_exp(a * (i + 1) * dt) * dt) / s_exp(a * (i + 1) * dt)-]"
    apply (simp add: TransferFcn_def update_def)
    apply (rule_tac f=demonic in HOL.arg_cong)
    by auto

  (* The following definitions correspond to the three components of a TransferFcn block -- used in the nfb translations *)

  definition "TransferFcnA k a dt = [: (x, i, s) ↝ y. y = (s * s_exp(a * i * dt) + k * x * s_exp(a * (i + 1) * dt) * dt) / s_exp(a * (i + 1) * dt) :]"

  lemma TransferFcnA_func: "TransferFcnA k a dt = [- x, i, s ↝ (s * s_exp(a * i * dt) + k * x * s_exp(a * (i + 1) * dt) * dt) / s_exp(a * (i + 1) * dt)-]"
    by (simp add: TransferFcnA_def update_def split_def)

  definition "TransferFcnB = [: i ↝ i'. i' = i + 1:]"

  lemma TransferFcnB_func: "TransferFcnB = [- i ↝ i+ 1-]"
    by (simp add: TransferFcnB_def update_def)

  (* Variant with explicit time *)

  definition "TransferTFcn k a dt = [:(x, t, s) ↝ (y, t', s'). y = (s * s_exp(a * t) + k * x * s_exp(a * (t + dt)) * dt) / s_exp(a * (t + dt)) ∧
    t' = t + dt ∧ s' = y:]"

  lemma TransferTFcn_func: "TransferTFcn k a dt = [- x, t, s ↝ (s * s_exp(a * t) + k * x * s_exp(a * (t + dt)) * dt) / s_exp(a * (t + dt)),
    t + dt, (s * s_exp(a * t) + k * x * s_exp(a * (t + dt)) * dt) / s_exp(a * (t + dt))-]"
    apply (simp add: TransferTFcn_def update_def)
    apply (rule_tac f=demonic in HOL.arg_cong)
    by auto

  (* The following definitions correspond to the three components of a TransferFcn block -- used in the nfb translations *)

  definition "TransferTFcnA k a dt = [: (x, t, s) ↝ y. y = (s * s_exp(a * t) + k * x * s_exp(a * (t + dt)) * dt) / s_exp(a * (t + dt)) :]"

  lemma TransferTFcnA_func: "TransferTFcnA k a dt = [- x, t, s ↝ (s * s_exp(a * t) + k * x * s_exp(a * (t + dt)) * dt) / s_exp(a * (t + dt))-]"
    by (simp add: TransferTFcnA_def update_def split_def)

  definition "TransferTFcnB dt = [: t ↝ t'. t' = t + dt:]"

  lemma TransferTFcnB_func: "TransferTFcnB dt = [- t ↝ t + dt-]"
    by (simp add: TransferTFcnB_def update_def)


  (* SinWave block *)

  (* Variant with index for measuring time *)

  definition "SinWave amplitude frequency phase bias dt = [: i ↝ (y, i'). y = amplitude * s_sin(frequency * i * dt + phase) + bias ∧ i' = i + 1 :]"

  lemma SinWave_func: "SinWave amplitude frequency phase bias dt  = [- i ↝ amplitude * s_sin(frequency * i * dt + phase) + bias, i+1-]"
    apply (simp add: SinWave_def update_def)
    apply (rule_tac f= demonic in HOL.arg_cong)
    by auto

  (* The following definitions correspond to the two components of a SinWave block -- used in the nfb translations *)

  definition "SinWaveA amplitude frequency phase bias dt = [: i ↝ y. y = amplitude * s_sin(frequency * i * dt + phase) + bias :]"

  lemma SinWaveA_func : "SinWaveA amplitude frequency phase bias dt = [- i ↝ amplitude * s_sin(frequency * i * dt + phase) + bias -]"
    by (simp add: SinWaveA_def update_def)

  definition "SinWaveB = [: i ↝ i'. i' = i + 1 :]"

  lemma SinWaveB_func : "SinWaveB = [- i ↝ i + 1 -]"
    by (simp add: SinWaveB_def update_def)

  (* Variant with explicit time *)

  definition "SinWaveT amplitude frequency phase bias dt = [: t ↝ (y, t'). y = amplitude * s_sin(frequency * t + phase) + bias ∧ t' = t + dt :]"

  lemma SinWaveT_func: "SinWaveT amplitude frequency phase bias dt  = [- t ↝ amplitude * s_sin(frequency * t + phase) + bias, t + dt-]"
    apply (simp add: SinWaveT_def update_def)
    apply (rule_tac f= demonic in HOL.arg_cong)
    by auto

  (* The following definitions correspond to the two components of a SinWave block -- used in the nfb translations *)

  definition "SinWaveTA amplitude frequency phase bias dt = [: t ↝ y. y = amplitude * s_sin(frequency * t + phase) + bias :]"

  lemma SinWaveTA_func : "SinWaveTA amplitude frequency phase bias dt = [- t ↝ amplitude * s_sin(frequency * t + phase) + bias -]"
    by (simp add: SinWaveTA_def update_def)

  definition "SinWaveTB dt = [: t ↝ t'. t' = t + dt :]"

  lemma SinWaveTB_func : "SinWaveTB dt = [- t ↝ t + dt -]"
    by (simp add: SinWaveTB_def update_def)


  (* Function used in formalizing a MinMax block *)

  fun MIN_S:: "'a::ord list ⇒ 'a" where
    "MIN_S [] = Eps ⊤" |
    "MIN_S [x] = x" |
    "MIN_S (x # xs) = min x (MIN_S xs)"


  (* Function used in formalizing a MinMax block *)

  fun MAX_S:: "'a::ord list ⇒ 'a" where
    "MAX_S [] = Eps ⊤" |
    "MAX_S [x] = x" |
    "MAX_S (x # xs) = max x (MAX_S xs)"


  (* Function used in formalizing a Lookup block *)

  definition "slope_val x xi xj yi yj = (yj - yi) * (x - xi) / (xj - xi) + yi"


  (* Function used in formalizing a SignalGenerator block *)

  definition "siggen_square x = (If s_sin x < 0 Then (-1::'a::simulink) Else (1::'a::simulink))"


  (* Function used in formalizing a ? ?  block *)
  
  (* This is no longer used -- commented out for now   
  definition "switch vals i = vals ! (nat (floor i - 1))"
  *)
    
  (*
  lemma "nat (floor (-1.2::real)) = 0"
    by auto

  definition "sw_index n i = (if n ≤ nat (floor (i - 1)) then n - 1 else nat (floor (i - 1)))"

  definition "switch vals i = vals ! (sw_index (length vals) i)"

  lemma nonempty_sw_index: "vals ≠ [] ⟹ sw_index (length vals) i < length vals"
    by (simp add: sw_index_def)

  lemma nonempty_sw_index_a: "0 < n ⟹ sw_index n i < n"
    by (simp add: sw_index_def)

  lemma distrib_switch: "n < length vals ⟹ f (vals ! n) = (map f vals) ! n"
    apply (induction n)
    by simp_all

  lemma distrib_switch_a: "vals ≠ [] ⟹ f (vals ! (sw_index (length vals) i)) = (map f vals) ! (sw_index (length vals) i)"
    apply (rule distrib_switch)
    apply (rule nonempty_sw_index)
    by simp


  lemma switch_tuple: "n < length vals ⟹(vals ! n) = ((map fst vals)  ! n, (map snd vals)  ! n)"
    apply (induction n)
    by simp_all

  lemma switch_tuple_a: "vals ≠ [] ⟹ (vals ! (sw_index (length vals) i)) = ((map fst vals)  ! (sw_index (length vals) i), (map snd vals)  ! (sw_index (length vals) i))"
    apply (rule switch_tuple)
    apply (rule nonempty_sw_index)
    by simp
  *)


  (*
  definition "is_eq x y = (If (x::'a) = y Then (1::'a::MyNumber) Else (0::'a::MyNumber))"
  definition "is_less x y = (If (x::'a) < y Then (1::'a::MyNumber) Else (0::'a::MyNumber))"
  definition "is_less_eq x y = (If (x::'a) ≤ y Then (1::'a::MyNumber) Else (0::'a::MyNumber))"
  *)
  
  (*
  definition "is_eq_num x y = (If (x::'a) = y Then (1::'a::MyNumber) Else (0::'a::MyNumber))"
  definition "is_less_num x y = (If (x::'a) < y Then (1::'a::MyNumber) Else (0::'a::MyNumber))"
  definition "is_less_eq_num x y = (If (x::'a) ≤ y Then (1::'a::MyNumber) Else (0::'a::MyNumber))"

  definition "is_eq x y = (x = y)"
  definition "is_less x y = (x < y)"
  definition "is_less_eq x y = (x ≤ y)"
  definition "is_gt x y = (x > y)"
  definition "is_ge x y = (x ≥ y)"
  definition "is_neq x y = (x ≠ y)"
  *)

  (* Definition of rewriting rules to be used in expansion/simplification *)

  lemmas additional_simps = 
    (*is_eq_def is_less_def is_less_eq_def is_eq_num_def is_less_num_def 
    is_less_eq_num_def is_gt_def is_ge_def is_neq_def *)
    slope_val_def siggen_square_def MIN_S.simps MAX_S.simps

  lemmas basic_block_rel_simps = 
      Gain_def Square_def Power_def Power10_def Exp_def Ln_def Sqrt_def Constant_def Saturation_def  Relay_def  Integrator_def 
      PulseGenerator_def Step_def TransferFcn_def
      Scope_def Outport_def Inport_def
      IntegratorA_def IntegratorB_def Terminator_def SinWave_def SinWaveA_def SinWaveB_def IntegratorLimit_def IntegratorLimitA_def IntegratorLimitB_def
      (*MIN.simps MAX.simps*)

  lemmas basic_block_func_simps = 
      Gain_func Square_func Power_func Power10_func Exp_func Ln_func Sqrt_func Constant_func Saturation_func  
      Relay_func  RelayA_func RelayB_func
      Integrator_func IntegratorA_func IntegratorB_func 
      PulseGenerator_func PulseGeneratorA_func PulseGeneratorB_func PulseGeneratorC_func
      (*PulseGeneratorT_func PulseGeneratorTA_func PulseGeneratorTB_func PulseGeneratorTC_func*)
      PulseGeneratorS_func PulseGeneratorSA_func PulseGeneratorSB_func
      TransferFcn_func TransferFcnA_func TransferFcnB_func 
      TransferTFcn_func TransferTFcnA_func TransferTFcnB_func
      Scope_def Outport_def Inport_def
      Step_func StepA_func StepB_func 
      StepT_func StepTA_func StepTB_func 
      (*switch_def*) Terminator_func 
      SinWave_func SinWaveA_func SinWaveB_func 
      SinWaveT_func SinWaveTA_func SinWaveTB_func 
      IntegratorLimit_func IntegratorLimitA_func IntegratorLimitB_func
      siggen_square_def (*TO CHECK*)
      (*MIN.simps MAX.simps*)

  lemmas comp_rel_simps = Prod_spec_Skip Prod_Skip_spec Prod_demonic_skip Prod_skip_demonic Prod_demonic Prod_spec_demonic Prod_demonic_spec
     comp_assoc [THEN sym] demonic_demonic comp_demonic_demonic assert_assert_comp comp_demonic_assert demonic_assert_comp 
     OO_def Prod_spec Fail_assert fail_assert_demonic fail_comp             
     prod_skip_skip skip_comp comp_skip prod_fail fail_prod
     update_demonic_comp demonic_update_comp comp_update_demonic comp_demonic_update

  lemmas comp_func_simps =
    (*product*)
    prod_update prod_update_skip prod_skip_update
    prod_assert_update_skip prod_skip_assert_update
    Prod_assert_skip Prod_skip_assert prod_assert_update
    prod_assert_assert_update prod_assert_update_assert
    prod_update_assert_update prod_assert_update_update
    comp_update_update comp_update_assert update_assert_comp
    assert_assert_comp_pred
    update_comp comp_assoc [THEN sym]
    Fail_def fail_comp update_fail assert_fail prod_fail fail_prod
    prod_skip_skip skip_comp comp_skip
    
  lemmas refinement_simps = assert_demonic_refinement spec_demonic_refinement
  
  lemmas simulink_simps = basic_block_func_simps comp_func_simps

  lemmas comp_var_simps = demonic_def assert_def le_fun_def Prod_spec_Skip Prod_Skip_spec Prod_demonic_skip Prod_skip_demonic Prod_demonic Prod_spec_demonic Prod_demonic_spec
     comp_assoc [THEN sym] demonic_demonic comp_demonic_demonic assert_assert_comp comp_demonic_assert demonic_assert_comp OO_def Prod_spec Fail_assert

  lemmas fail_simps =  fail_def demonic_def Prod_spec_Skip Prod_Skip_spec Prod_demonic_skip Prod_skip_demonic assert_def le_fun_def Prod_demonic Prod_spec_demonic Prod_demonic_spec
     comp_assoc [THEN sym] demonic_demonic comp_demonic_demonic assert_assert_comp comp_demonic_assert demonic_assert_comp OO_def Prod_spec Fail_assert

  lemmas prec_simps =  prec_def fail_def demonic_def Prod_spec_Skip Prod_Skip_spec Prod_demonic_skip Prod_skip_demonic assert_def le_fun_def  Prod_spec_demonic Prod_demonic_spec
     comp_assoc [THEN sym] demonic_demonic comp_demonic_demonic assert_assert_comp comp_demonic_assert demonic_assert_comp OO_def Prod_demonic Prod_spec Fail_assert

  lemmas rel_simps =  rel_def demonic_def Prod_spec_Skip Prod_Skip_spec Prod_demonic_skip Prod_skip_demonic assert_def le_fun_def Prod_demonic Prod_spec_demonic Prod_demonic_spec
     comp_assoc [THEN sym] demonic_demonic comp_demonic_demonic assert_assert_comp comp_demonic_assert demonic_assert_comp OO_def Prod_spec Fail_assert

  lemmas sconjunctive_simps = sconjunctive_simp_a sconjunctive_simp_b sconjunctive_simp_c

 lemmas feedback_rel_simps = feedback_simp_a feedback_simp_b feedback_simp_bot

  lemmas feedback_func_simps = feedback_update_simp_aaa feedback_update_simp_bbb feedback_simp_bot  

  lemmas feedbackless_func_simps = feedbackless_update_simp_aaa feedbackless_update_simp_bbb feedback_simp_bot  

  lemma [simp]: "(∃ x y z . x = f y z)"
    by auto

  lemma [simp]: "(∃ x y z . f y z = x)"
    by auto

  lemma [simp]: "(∃ x y  . x = f y )"
    by auto

  lemma [simp]: "(∃ x y  . f y = x)"
    by auto

  lemma [simp]: "(∀x::real. ¬ 0 ≤ x) = False"
    by auto

  lemma [simp]: "Ex ((≤) (0::real)) = True"
    by auto
    
  lemma [simp]: "(∃ a b . a + b = (x::'a::group_add)) = True"
    apply auto
    by (rule_tac x = 0 in exI, auto)

  (*
  lemma [simp]: "(∃ x . p x) = (p True ∨ p False)"
    by (rule Set.ex_bool_eq)

  lemma [simp]: "(∀ x . p x) = (p True ∧ p False)"
    by (rule Set.all_bool_eq)
  *)

  lemma common_imp_right_a[simp]: "((p ⟶ (a ∧ b)) ∧ (¬ p ⟶ (c ∧ b))) = (((p ⟶ a) ∧ (¬ p ⟶ c)) ∧ b)"
    by auto

  lemma common_imp_right_b[simp]: "((¬ p ⟶ (a ∧ b)) ∧ (p ⟶ (c ∧ b))) = (((¬ p ⟶ a) ∧ (p ⟶ c)) ∧ b)"
    by auto

  lemma common_imp_left_a [simp]: "((p ⟶ b ∧ a) ∧ (¬ p ⟶b ∧ c)) = (b ∧ (p ⟶ a) ∧ (¬ p ⟶ c))"
    by auto

  lemma common_imp_left_b [simp]: "((¬ p ⟶ b ∧ a) ∧ (p ⟶b ∧ c)) = (b ∧ (¬ p ⟶ a) ∧ (p ⟶ c))"
    by auto

  lemma common_dimp: "((p ⟶ (q ⟶ a)) ∧ (r ⟶ (q ⟶ b))) = (q ⟶ ((p ⟶ a) ∧ (r ⟶ b)))"
    by auto

  lemma fst_case_prod_eqa: "(⋀ x y . fst (f1 x y) = fst (f2 x y)) ⟹ fst (case_prod f1 p) =  fst (case_prod f2 p)"
    by (simp add: split_def)

  lemma fst_case_prod_eqa_x: "(⋀ x y . f (f1 x y) = f (f2 x y)) ⟹ f (case_prod f1 p) =  f (case_prod f2 p)"
    by (simp add: split_def)

  lemma fst_case_prod_eq: "fst (f1 (fst p1) (snd p1)) = fst (f2 (fst p2) (snd p2)) ⟹ fst (case_prod f1 p1) =  fst (case_prod f2 p2)"
    by (simp add: split_def)

  lemma fst_case_prod_eqc: "(⋀ z . fst (f1 u z) = fst (f2 u' z)) ⟹ fst (case_prod f1 (u, x)) =  fst (case_prod f2 (u', x))"
    by (simp add: split_def)

  lemma fst_case_prod_eqd: "(⋀ y z . fst (f1 y z) = fst (f2 y z)) ⟹ fst (case_prod f1 x) =  fst (case_prod f2 x)"
    by (simp add: split_def)

  definition "Snd = snd"

  lemma fst_case_prod_eqb: "(fst (case_prod f1 p1) =  fst (case_prod f2 p2)) = (fst (f1 (fst p1) (Snd p1)) = fst (f2 (fst p2) (Snd p2)))"
    by (simp add: split_def Snd_def)

  lemma fst_case_prod_eqb_a: "(fst (case_prod f1 (u, x)) =  fst (case_prod f2 (v, x))) = (fst (f1 u x) = fst (f2 v x))"
    by (simp add: split_def Snd_def)

  lemma fst_case_prod_eqb_b: "(fst (case_prod f1 p) =  fst (case_prod f2 p)) = (fst (f1 (fst p) (Snd p)) = fst (f2 (fst p) (Snd p)))"
    by (simp add: split_def Snd_def)

  definition "FstA = fst"

  lemma Fst_simp: "FstA (x,y) = x"
    by (simp add: FstA_def) 

  lemma fst_case_prod_eqc_a: "(fst (case_prod f1 (u, x)) =  fst (case_prod f2 (v, x))) = (FstA (f1 u x) = FstA (f2 v x))"
    by (simp add: split_def Snd_def FstA_def)

  lemma fst_case_prod_eqc_b: "(FstA (case_prod f1 p) =  FstA (case_prod f2 q)) = (FstA (f1 (fst p) (Snd p)) = FstA (f2 (fst q) (Snd q)))"
    by (simp add: split_def Snd_def)

  lemma Snd_simp: "Snd (x, y) = y"
    by (simp add: Snd_def)

  lemma fst_case_prod_eqb_x: "(f (case_prod f1 p1) =  f (case_prod f2 p2)) = (f (f1 (fst p1) (Snd p1)) = f (f2 (fst p2) (Snd p2)))"
    by (simp add: split_def Snd_def)

  (*
  lemma fst_case_prod_eqa_x: "f (case_prod f1 p) =  (case_prod (λ x y . f (f1 x y)) )"
    by (simp add: split_def)
  *)

  lemma fst_case_prod_eqba: "(∀ x . fst (case_prod f1 x) =  fst (case_prod f2 x)) = (∀ x y . fst (f1 x y) = fst (f2 x y))"
    by (simp add: split_def)

  lemma [simp]: "(p ∧ (p ⟶ q)) = (p ∧ q)"
    by auto

  lemma [simp]: "(∀ x. x ≠ y) = False"
    by auto

  lemma [simp]: "(∀ x. y ≠ x) = False"
    by auto

  lemma [simp]: "(∃ x::real. y ≠ x) = True"
    apply safe
    by (rule_tac x = "y+1" in exI, simp)

  lemma [simp]: "(∃ x::real. x ≠ y) = True"
    apply safe
    by (rule_tac x = "y+1" in exI, simp)

  lemma rel_if_expr_1: "p x z ⟹ p (if b then x else y) z = (b ∨  p y z)"
    by auto

  lemma rel_if_expr_2: "p y z ⟹ p (if b then x else y) z = (¬ b ∨ p x z)"
    by auto

  lemma rel_if_not_expr_1: "¬ p x z ⟹ p (if b then x else y) z = (¬ b ∧ p y z)"
    by auto

  lemma rel_if_not_expr_2: "¬ p y z ⟹ p (if b then x else y) z = (b ∧ p x z)"
    by auto

  lemma rel_expr_if_1: "p z x ⟹ p z (if b then x else y) = (b ∨  p z y)"
    by auto

  lemma rel_expr_if_2: "p z y ⟹ p z (if b then x else y) = (¬ b ∨ p z x)"
    by auto

  lemma rel_expr_if_not_1: "¬ p z x ⟹ p z (if b then x else y) = (¬ b ∧ p z y)"
    by auto

  lemma rel_expr_if_not_2: "¬ p z y ⟹ p z (if b then x else y) = (b ∧ p z x)"
    by auto

  lemma if_not: "(if ¬ b then x else y) = (if b then y else x)"
    by auto

  lemma rel_not_if_expr_1: "p y z ⟹ p (if ¬ b then x else y) z = (b ∨ p x z)"
    by auto

  lemma rel_not_if_expr_2: "p x z ⟹ p (if ¬ b then x else y) z = (¬b ∨  p y z)"
    by auto

  lemma rel_not_if_not_expr_1: "¬ p y z ⟹ p (if ¬ b then x else y) z = (¬ b ∧ p x z)"
    by auto

  lemma rel_not_if_not_expr_2: "¬ p x z ⟹ p (if ¬ b then x else y) z = (b ∧ p y z)"
    by auto

  lemma rel_expr_not_if_1: "p z y ⟹ p z (if ¬ b then x else y) = (b ∨ p z x)"
    by auto

  lemma rel_expr_not_if_2: "p z x ⟹ p z (if ¬ b then x else y) = (¬ b ∨ p z y)"
    by auto

  lemma rel_expr_not_if_not_1: "¬ p z y ⟹ p z (if ¬ b then x else y) = (¬ b ∧ p z x)"
    by auto

  lemma rel_expr_not_if_not_2: "¬ p z x ⟹ p z (if ¬ b then x else y) = (b ∧ p z y)"
    by auto

  lemma not_inf: "(¬ (x::real) < y) = (y ≤ x)"
    by auto

  lemmas if_simps = rel_if_expr_1 rel_if_expr_2 rel_if_not_expr_1 rel_if_not_expr_2 rel_expr_if_1 rel_expr_if_2 rel_expr_if_not_1 rel_expr_if_not_2 
      rel_not_if_expr_1 rel_not_if_expr_2 rel_not_if_not_expr_1 rel_not_if_not_expr_2 rel_expr_not_if_1 rel_expr_not_if_2 rel_expr_not_if_not_1 rel_expr_not_if_not_2
      if_not not_inf MyIf_def 

end