Theory PythonSimulation

(**-----------------------------------------------------------------------------
 * © [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‹Python Simulation Code Generation›

theory PythonSimulation imports SimulinkTypes
begin

  (* This file defines the rewriting rules for generating python code from a simplified predicate transformer *)

  (* constant "pi" definition *)

  definition "PI_PY = (λx::nat. s_pi)"

  lemma PI_PY_gen_simp: "s_pi = PI_PY(0)"
    by (simp add: PI_PY_def)

  lemma PI_PY_simp: "pi = PI_PY(0)"
    by (simp add: PI_PY_def)


  (* "not" definition *)

  definition "NOT_PY = Not"

  lemma NOT_PY_simp: "Not x = NOT_PY(x)"
    by (simp add: NOT_PY_def)


  (* "and" definition *)

  definition "AND_PY = (λ (x, y). x ∧ y)"

  lemma AND_PY_simp: "(x ∧ y) = AND_PY(x,y)"
    by (simp add: AND_PY_def)


  (* "or" definition *)

  definition "OR_PY = (λ (x,y). x ∨ y)"

  lemma OR_PY_simp: "(x ∨ y) = OR_PY(x,y)"
    by (simp add: OR_PY_def)


  (* "less than" definition *)

  definition "LESS_PY = (λ (x, y) . x < y)"

  lemma LESS_PY_simp: "(x < y) = LESS_PY (x, y)"
    by (simp add: LESS_PY_def)


  (* "less or equal than " definition *)

  definition "LE_PY = (λ (x, y) . x ≤ y)"

  lemma LE_PY_simp: "(x ≤ y) = LE_PY (x, y)"
    by (simp add: LE_PY_def)


  (* "equal" definition *)

  definition "EQ_PY = (λ (x, y) . x = y)"

  lemma EQ_PY_simp: "(x = y) = EQ_PY (x, y)"
    by (simp add: EQ_PY_def)


  (* "addition" definition *)

  definition "ADD_PY = (λ (x, y). x + y)"

  lemma ADD_PY_simp: "(x + y) = ADD_PY (x, y)"
    by (simp add: ADD_PY_def)  


  (* "subtraction" definition *)

  definition "SUBS_PY = (λ (x, y). x - y)"

  lemma SUBS_PY_simp: "(x - y) = SUBS_PY (x, y)"
    by (simp add: SUBS_PY_def) 


  (* "multiplication" definition *)

  definition "MULT_PY = (λ (x, y). x * y)"

  lemma MULT_PY_simp: "(x * y) = MULT_PY (x, y)"
    by (simp add: MULT_PY_def) 


  (* "division" definition *)

  definition "DIV_PY = (λ (x,y) . x / y)"
   
  lemma DIV_PY_simp: "x / y = DIV_PY (x, y)"
    by (simp add: DIV_PY_def)


  (* "absolute value" definition *)

  definition "ABS_PY = (λ x. s_abs x)"

  lemma ABS_PY_gen_simp: "s_abs x = ABS_PY x"
    by (simp add: ABS_PY_def)

  lemma ABS_PY_simp: "abs (x::real) = ABS_PY x"
    by (simp add: ABS_PY_def)


  (* "x to the power of y" definiton *)

  definition "POW_PY = (λ(x,y). power x y)"


  lemma POW_PY_simp: "(x ^ y) = POW_PY (x, y)"
    by (simp add: POW_PY_def)

 
  (* "sqrt" definition *)
      

  definition "SQRT_PY = s_sqrt"

  lemma SQRT_PY_gen_simp: "s_sqrt x = SQRT_PY(x)"
    by (simp add: SQRT_PY_def)

  lemma SQRT_PY_simp: "sqrt x = SQRT_PY(x)"
    by (simp add: SQRT_PY_def)


  (* "exp" definition *)

  definition "EXP_PY = s_exp"

  lemma EXP_PY_gen_simp: "s_exp x = EXP_PY(x)"
    by (simp add: EXP_PY_def)

  lemma EXP_PY_simp: "exp (x::real) = EXP_PY(x)"
    by (simp add: EXP_PY_def)


  (* "sin" definition *)

  definition "SIN_PY = s_sin"

  lemma SIN_PY_gen_simp: "s_sin x = SIN_PY(x)"
    by (simp add: SIN_PY_def)

  lemma SIN_PY_simp: "sin (x::real) = SIN_PY(x)"
    by (simp add: SIN_PY_def)


  (* "fst" element of a tuple definition *)

  definition "FST_PY = fst"

  lemma FST_PY_simp: "fst x = FST_PY (x)"
    by (simp add: FST_PY_def)


  (* "snd" element of a tuple definition *)

  definition "SND_PY = snd"

  lemma SND_PY_simp: "snd x = SND_PY (x)"
    by (simp add: SND_PY_def)


  (* "if" definition *)

  definition "IF_PY = (λ (b, x, y) . If b Then x Else y)"

  lemma IF_PY_gen_simp: "(If b Then x Else y) = IF_PY (b, x, y)"
    by (simp add: IF_PY_def)

  lemma IF_PY_simp: "(if b then x else y) = IF_PY (b, x, y)"
    by (simp add: IF_PY_def MyIf_def)

  (* "implies" definition *)

  definition "IMP_PY = (λ (x, y) . x ⟶ y)"

  lemma IMP_PY_simp: "(x ⟶ y) = IMP_PY (x, y)"
    by (simp add: IMP_PY_def)

 
  (* "conversion" definition *)

  definition "CONVERSION_PY = (λ (x, y::nat) . conversion x)"

  lemma CONVERSION_PY_simp: "conversion x = CONVERSION_PY (x,0)"
    by (simp add: CONVERSION_PY_def)

  (* "max" definition *)

  definition "MAX_PY = (λ (x, y). max x y)"

  lemma MAX_PY_simp: "max x y = MAX_PY(x, y)"
    by (simp add: MAX_PY_def)

  (* "min" definition *)

  definition "MIN_PY = (λ (x, y). min x y)"

  lemma MIN_PY_simp: "min x y = MIN_PY(x, y)"
    by (simp add: MIN_PY_def)

  definition "SUC_PY = Suc"

  lemma SUC_PY_simp: "Suc x = SUC_PY x"
    by (simp add: SUC_PY_def)


  lemmas python_simps = PI_PY_simp PI_PY_gen_simp NOT_PY_simp AND_PY_simp OR_PY_simp LESS_PY_simp LE_PY_simp EQ_PY_simp 
                        ADD_PY_simp  SUBS_PY_simp MULT_PY_simp DIV_PY_simp ABS_PY_gen_simp ABS_PY_simp 
                        (*POW_PY_gen_simp*) POW_PY_simp SQRT_PY_gen_simp SQRT_PY_simp
                        EXP_PY_gen_simp EXP_PY_simp SIN_PY_gen_simp SIN_PY_simp
                        FST_PY_simp SND_PY_simp  
                        IF_PY_simp IF_PY_gen_simp IMP_PY_simp
                        CONVERSION_PY_simp 
                        MAX_PY_simp MIN_PY_simp SUC_PY_simp
                        
end