Theory BoolProgs_Simple

theory BoolProgs_Simple
imports 
  "../BoolProgs_Extras"
begin

context begin interpretation BoolProg_Syntax .

fun simple_prog :: "nat ⇒ nat ⇒ (bexp × com) list" where
  "simple_prog _ 0 = []"
| "simple_prog r (Suc n) = (V n, [n] ::= [FF]) # simple_prog r n"

definition simple :: "nat ⇒ bprog × config" where 
  "simple n = (optcomp 
    (WHILE TT DO IF simple_prog n n FI), 
    (0, foldl (λxs i. bs_insert i xs) (bs_empty ()) [0..<n]))"

definition simple_const :: "nat ⇒ const_map"  where
  "simple_const n ≡ Mapping.empty"

definition simple_fun :: "nat ⇒ fun_map" where
  "simple_fun n ≡ mapping_from_list [(STR ''var'', λi. V i)]"

end

end