Theory SteamBoiler

(*<*)
(*
   Title:  Theory SteamBoiler.thy (Steam Boiler System: Specification)
   Author: Maria Spichkova <maria.spichkova at rmit.edu.au>, 2013
*)
(*>*)

section ‹Steam Boiler System: Specification›

theory  SteamBoiler 
imports stream BitBoolTS
begin

definition
 ControlSystem :: "nat istream ⇒ bool"
where
 "ControlSystem s ≡  
  (ts s) ∧ 
   (∀ (j::nat). (200::nat) ≤ hd (s j) ∧ hd (s j) ≤ (800:: nat))"

definition
  SteamBoiler :: "bit istream ⇒ nat istream ⇒ nat istream ⇒ bool"
where
 "SteamBoiler x s y ≡  
  ts x 
  ⟶ 
  ((ts y) ∧ (ts s) ∧ (y = s) ∧ 
   ((s 0) = [500::nat]) ∧ 
   (∀ (j::nat). (∃ (r::nat). 
                (0::nat) < r ∧ r ≤ (10::nat) ∧ 
                hd (s (Suc j)) = 
                   (if hd (x j) = Zero 
                    then (hd (s j)) - r 
                    else (hd (s j)) + r)) ))"

definition
  Converter :: "bit istream ⇒ bit istream ⇒ bool"
where
 "Converter z x 
  ≡ 
  (ts x) 
  ∧ 
  (∀ (t::nat). 
    hd (x t) = 
        (if  (fin_make_untimed (inf_truncate z t) = [])
         then  
             Zero
         else 
             (fin_make_untimed (inf_truncate z t)) ! 
                 ((length (fin_make_untimed (inf_truncate z t))) - (1::nat)) 
       ))"

definition
  Controller_L :: 
    "nat istream ⇒ bit iustream ⇒ bit iustream ⇒ bit istream ⇒ bool"
where
 "Controller_L y lIn lOut z 
  ≡ 
  (z 0 = [Zero]) 
  ∧
  (∀ (t::nat). 
  ( if (lIn t) = Zero 
    then ( if 300 < hd (y t)  
           then  (z t) = []    ∧ (lOut t) = Zero
           else  (z t) = [One] ∧ (lOut t) = One 
          )
    else ( if  hd (y t) < 700  
           then  (z t) = []     ∧ (lOut t) = One   
           else  (z t) = [Zero] ∧ (lOut t) = Zero ) ))"

definition 
  Controller :: "nat istream ⇒ bit istream ⇒ bool"
where
 "Controller y z 
  ≡ 
  (ts y)
  ⟶ 
  (∃ l. Controller_L y (fin_inf_append [Zero] l) l z)"

definition
  ControlSystemArch :: "nat istream ⇒ bool"
where
 "ControlSystemArch s 
  ≡ 
  ∃ x z :: bit istream. ∃ y :: nat istream.
    ( SteamBoiler x s y ∧ Controller y z ∧ Converter z x )"

end