Theory SimulinkTypes

(**-----------------------------------------------------------------------------
 * © [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.
 *)

section‹\label{sec_Simulink}Formalizing Simulink in RCRS›

subsection‹Types for Simulink Modeling Elements›

theory SimulinkTypes imports  Complex_Main
begin

  instantiation bool::zero
  begin
    definition zero_bool_def[simp]: "0 = False"
    instance proof qed
  end

  instantiation bool::one
  begin
    definition one_bool_def[simp]: "1 = True"
    instance proof qed
  end

  instantiation bool::plus
  begin
    definition plus_bool_def[simp]: "(a::bool) + b = (a ∨ b)"
    instance proof qed
  end
 
  instance bool::semigroup_add
    proof qed auto

  instantiation bool::numeral
  begin
    instance proof qed
    lemma [simp]: "numeral a = True"
    apply (induction a)
    by (simp_all add: numeral_Bit0 numeral_Bit1)
  end

  instantiation bool::divide
  begin
    definition divide_bool_def[simp]: "(a::bool) div b = (a ∧ b)"
    instance proof qed
  end

  instantiation bool::inverse
  begin
    definition inverse_bool_def[simp]: "inverse (a::bool) = a"
    instance proof qed
  end
  

  class s_pi = 
    fixes s_pi::'a

  instantiation real::s_pi
  begin
    definition s_pi_real_def[simp]: "s_pi = pi"
    instance proof qed
  end

  class s_sqrt = 
    fixes s_sqrt:: "'a ⇒ 'a"

  instantiation real::s_sqrt
  begin
    definition s_sqrt_real_def[simp]: "s_sqrt = sqrt"
    instance proof qed
  end

  class s_abs = 
    fixes s_abs:: "'a ⇒ 'a"

  instantiation real::s_abs
  begin
    definition s_abs_real_def[simp]: "s_abs = (abs::real ⇒ real)"
    instance proof qed
  end

  class s_exp = 
    fixes s_exp:: "'a ⇒ 'a"

  instantiation real::s_exp
  begin
    definition s_exp_real_def[simp]: "s_exp = (exp :: real ⇒ real)"
    instance proof qed
  end

  class s_ln = 
    fixes s_ln:: "'a ⇒ 'a"

  instantiation real::s_ln
  begin
    definition s_ln_real_def[simp]: "s_ln = (ln::real ⇒ real)"
    instance proof qed
  end

  class s_sin = 
    fixes s_sin:: "'a ⇒ 'a"

class s_cos = 
    fixes s_cos:: "'a ⇒ 'a"


  instantiation real::s_sin
begin
  (*
    definition s_sin_real_def[simp]: "s_sin = (λ a::real . sin a)"
  *)
    definition s_sin_real_def[simp]: "s_sin = (sin :: real ⇒ real)"
    instance proof qed
  end

instantiation real::s_cos
begin
  (*
    definition s_cos_real_def[simp]: "s_cos = (λ a::real . cos a)"
  *)
    definition s_cos_real_def[simp]: "s_cos = (cos :: real ⇒ real)"
    instance proof qed
  end


 definition MyIf:: "bool ⇒ 'a ⇒ 'a ⇒ 'a"  ("(If (_)/ Then (_)/ Else (_))" [0, 0, 10] 10) where
    "(If b Then x Else y) = (if b then x else y)"

  lemma If_prod: "(If b Then (x, y) Else (u, v)) = ((If b Then x Else u), (If b Then y Else v))"
    by (simp add: MyIf_def)

  lemma If_eq: "(If b Then x Else x) = x"
    by (simp add: MyIf_def)

(*
  class ToReal =
    fixes ToReal::"'a => real"

  instantiation bool::ToReal
    begin
      definition ToReal_bool_def[simp]: "ToReal x = (if x then 1 else 0)"
      instance proof qed 
    end

  instantiation real::ToReal
    begin
      definition ToReal_real_def[simp]: "ToReal = id"
      instance proof qed 
    end

  class ToBool =
    fixes ToBool::"'a => bool"

  instantiation bool::ToBool
    begin
      definition ToBool_bool_def[simp]: "ToBool = id"
      instance proof qed 
    end

  instantiation real::ToBool
    begin
      definition ToBool_real_def[simp]: "ToBool (x::real) = (x ≠ 0)"
      instance proof qed 
    end
*)
(*
  class MyNumber = minus + uminus + numeral + power + zero + ord + MySqrt + MyExp + MyPi + MyTrue + MyFalse + MyOr + MyAnd + MyNot + ToReal + ToBool + inverse
*)


  class simulink = minus + uminus + numeral + power + zero + ord + s_sqrt + s_abs + s_exp + s_ln + s_sin + s_cos + s_pi + inverse +
    assumes numeral_nzero[simp]: "numeral n ≠ 0"
  begin
    lemma [simp]: "(1 = 0) = False"
      using local.numeral.numeral_One local.numeral_nzero by blast
    lemma [simp]: "(0 = 1) = False"
      using local.numeral.numeral_One local.numeral_nzero by blast

    lemma [simp]: "((if b then (1::'a) else 0) = 0) = (¬ b)"
      by auto
  
    lemma [simp]: "((if b then (1::'a) else 0) = 1) = b"
      by auto

  end

  lemma [simp]: "(if b then True else False) = b"
    by auto


  instantiation real::simulink
    begin
    instance proof qed auto
    end

  instantiation nat::simulink
    begin
    instance proof qed auto
    end

  instantiation bool::simulink
    begin
    instance proof qed auto
    end

  definition "is_eq_num x y = (if x = y then 1 else 0)"
  lemma is_eq_num_a: "((is_eq_num x y)::bool) = (x = y)"
    by (auto simp add: is_eq_num_def)
  lemmas is_eq_num_simp [simp] = is_eq_num_a is_eq_num_def

  definition "is_neq_num x y = (if x ≠ y then 1 else 0)"
  lemma is_neq_num_a: "((is_neq_num x y)::bool) = (x ≠ y)"
    by (auto simp add: is_neq_num_def)
  lemmas is_neq_num_simp [simp] = is_neq_num_a is_neq_num_def

  definition "is_less_num x y = (if x < y then 1 else 0)"
  lemma is_less_num_a: "((is_less_num x y)::bool) = (x < y)"
    by (auto simp add: is_less_num_def)
  lemmas  is_less_num_simp [simp] = is_less_num_a  is_less_num_def
  
  definition "is_less_eq_num x y = (if x ≤ y then 1 else 0)"
  lemma is_less_eq_num_a: "((is_less_eq_num x y)::bool) = (x ≤ y)"
    by (simp add: is_less_eq_num_def)
  lemmas is_less_eq_num_simp [simp] = is_less_eq_num_a is_less_eq_num_def

  definition "is_gt_num x y = (if x > y then 1 else 0)"
  lemma is_gt_num_a: "((is_gt_num x y)::bool) = (x > y)"
    by (simp add: is_gt_num_def)
  lemmas is_gt_num_simp [simp] = is_gt_num_a is_gt_num_def

  definition "is_ge_num x y = (if x ≥ y then 1 else 0)"
lemma is_ge_num_a: "((is_ge_num x y)::bool) = (x ≥ y)"
    by (simp add: is_ge_num_def)
 
  lemmas is_ge_num_simp [simp] = is_ge_num_a is_ge_num_def

  consts conversion :: "'a ⇒ 'b"
  
   overloading  
     conversion_id ≡ "conversion:: 'a ⇒ 'a"  (unchecked)
     conversion_bool_real ≡ "conversion:: bool ⇒ real"   (unchecked)
     conversion_bool_nat ≡ "conversion:: bool ⇒ nat"   (unchecked)
     conversion_real_bool ≡ "conversion:: real ⇒ bool"   (unchecked)
   begin  
     definition [simp]: "conversion_id a = a"
     definition [simp]: "conversion_bool_real (b::bool) = (if b then (1::real) else 0)"
     definition [simp]: "conversion_bool_nat (b::bool) = (if b then (1::nat) else 0)"
     definition [simp]: "conversion_real_bool (x::real) = (x ≠ 0)"
   end


end