Theory RCRS_Demo

(**-----------------------------------------------------------------------------
 * © [I Dragomir, V Preoteasa, S Tripakis]
 *
 * Contributors:
 *  Iulia Dragomir
 *
 * 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.
 *)

theory RCRS_Demo imports "Simulink/SimplifyRCRS" "RefinementReactive/Temporal"
begin
  declare [[eta_contract=false]]
  
  named_theorems basic_simps
  lemmas [basic_simps] = simulink_simps
  
  definition [basic_simps] : "SqrRoot = {. x. x≥0 .} o [- x ↝ sqrt x -]"
  definition [basic_simps] : "Cst1 = [- u ↝ 1 -]"
  
  simplify_RCRS "Syst1 = Cst1 o SqrRoot"
    "u" "y"
    
  thm Syst1_simp
    
  definition [basic_simps] : "Cst2 = [- u ↝ -1 -]"
  
  simplify_RCRS "Syst2 = Cst2 o SqrRoot"
    "u" "y"
    
  thm Syst2_simp
    
  lemmas [basic_simps] = simulink_simps comp_rel_simps
  
  definition [basic_simps] : "true = [: u ↝ y::real. True :]"
  
  simplify_RCRS "Syst3 = true o SqrRoot"
    "u" "y"
    
  thm Syst3_simp
    
  lemma aux1: "(∀y::real. 0 ≤y) = False"
    (*sledgehammer *)
    using le_minus_one_simps(3) by blast

  
  simplify_RCRS "Syst4 = true o SqrRoot"
    "u" "y"
    use (aux1)
  
  thm Syst4_simp
    
  definition [basic_simps] : "A = [: x ↝ y. y ≥ x + 1 :]"
  
  simplify_RCRS "Syst5 = A o SqrRoot"
    "x" "y"
    
  thm Syst5_simp
    
lemma aux2: "(∀y::real≥x+1. 0≤y) = (-1 ≤ x)"
    by auto
    
  simplify_RCRS "Syst6 = A o SqrRoot"  
    "x" "y"
    use(aux2)
    
  thm Syst6_simp

  lemma aux3:  "-1 ≤ x ⟹ (∃z. z ≥ (x + 1) ∧ y = sqrt z) = (sqrt (x + 1) ≤ y)"
  proof (safe, simp_all)
    fix x y
    assume A[simp]: "sqrt (x + 1) ≤ y"
    assume "-1 ≤ x"
    from this have B[simp]: "0 ≤ x + 1"
      by simp
    have "(sqrt (x + 1))^2 ≤ y^2"
      by (rule power_mono, simp_all)
    from this have [simp]: "x + 1 ≤ y^2"
      by simp
    have [simp]: "0 ≤ y"
      using A B by (metis order_trans real_sqrt_ge_0_iff)
    show " ∃ z ≥ x + 1. y = sqrt z"
      by (rule_tac x = "y^2" in exI, simp)
  qed

  lemma prec_rel: "(⋀ x y . p x ⟹ r x y = r' x y) ⟹ {.p.} o [:r:] = {.p.} o [:r':]"
    by (auto simp add: fun_eq_iff assert_def demonic_def le_fun_def)

  lemma "Syst6 = {. x. x ≥ -1 .} o [: x ↝ z . z ≥ sqrt (x + 1) :]"
  proof -
    have "Syst6 =  {. x . -1 ≤ x .} o [: x ↝ y . ∃ z ≥ x + 1. y = sqrt z :]"
      by (simp add: Syst6_simp)
    also have "... = {. x . -1 ≤ x .} o [: x ↝ y. (sqrt (x + 1) ≤ y) :]"
      by (rule prec_rel, simp add: aux3)
    finally show ?thesis
      by simp
  qed

  lemmas [basic_simps] = comp_rel_simps basic_block_rel_simps update_def refinement_simps

  definition [basic_simps] : "NonDetSqrt = {. x . x ≥ 0 .} o [: x ↝ y. y ≥ 0 :]"
  
  lemma "NonDetSqrt ≤ SqrRoot"
    by (auto simp add: basic_simps)
  
  definition [basic_simps] : "ReceptiveSqrt = [: x ↝ y . x ≥ 0 ⟶ y = sqrt x:]"
      
  lemma "SqrRoot ≤ ReceptiveSqrt" 
    by (simp add: basic_simps)

  definition "Syst7 = {. □ ♢ (ltl x . x ) .} o [: □ ♢(ltl x y . y) :]"
  definition "Syst8 = [: ♢ □  (ltl x y . ¬ y):]"


  lemma simp_ltl: "(∀ y . (♢ □ (ltl x y . ¬ y)) x y ⟶ (□ ♢ (ltl x. x)) y) = False"
    apply (simp add: LTL_def always_def eventually_def at_fun_def) (*expanding definitions*)
    apply (rule_tac x = ⊥ in exI)
    by auto

  simplify_RCRS "Syst9 = Syst8 o Syst7"
    "x" "y"
    use (Syst7_def Syst8_def simp_ltl)

  thm Syst9_simp

  definition [basic_simps]: "Add = [- f, g ↝ f+g -]"
  definition [basic_simps]: "UnitDelay = [- d, s ↝ s, d -]"
  definition [basic_simps]: "Split = [- a ↝ a , a -]"

  simplify_RCRS "Summation = feedback([- f, g, s ↝ (f, g), s-]
      o (Add ** Skip) o UnitDelay o (Split ** Skip) o [- (f, h), s' ↝ f, h, s' -])"
    "(g,s)" "(h, s')"

  (*Next theorem is created by simplify_RCRS*)
  thm Summation_simp

  (*Next lemma states explicitly the result of simplify_RCRS for Summation. *)
  lemma "Summation = [:(g, s)↝(h, s').h = s ∧ s' = s + g:]"
    by (rule Summation_simp)

end