chapter ‹Instantiating the Framework with a simple While-Language›

section ‹Commands›

theory Com imports Main begin

subsection ‹Variables and Values›

type_synonym vname = string ― ‹names for variables›

datatype val
  = Bool bool      ― ‹Boolean value›
  | Intg int       ― ‹integer value›

abbreviation "true == Bool True"
abbreviation "false == Bool False"

subsection ‹Expressions and Commands›

datatype bop = Eq | And | Less | Add | Sub     ― ‹names of binary operations›

datatype expr
  = Val val                                          ― ‹value›
  | Var vname                                        ― ‹local variable›
  | BinOp expr bop expr    (‹_ «_¬ _› [80,0,81] 80)  ― ‹binary operation›


fun binop :: "bop → val → val → val option"
where "binop Eq v₁ v₂ = Some(Bool(v₁ = v₂))"
  | "binop And (Bool b₁) (Bool b₂) = Some(Bool(b₁ ∧ b₂))"
  | "binop Less (Intg i₁) (Intg i₂) = Some(Bool(i₁ < i₂))"
  | "binop Add (Intg i₁) (Intg i₂) = Some(Intg(i₁ + i₂))"
  | "binop Sub (Intg i₁) (Intg i₂) = Some(Intg(i₁ - i₂))"
  | "binop bop v₁ v₂ = None"


datatype cmd
  = Skip
  | LAss vname expr        (‹_:=_› [70,70] 70)  ― ‹local assignment›
  | Seq cmd cmd            (‹_;;/ _› [61,60] 60)
  | Cond expr cmd cmd      (‹if '(_') _/ else _› [80,79,79] 70)
  | While expr cmd         (‹while '(_') _› [80,79] 70)


fun num_inner_nodes :: "cmd → nat" (‹#:_›)
where "#:Skip = 1"
  | "#:(V:=e) = 2"       (* zusätzlicher Skip-Knoten *)
  | "#:(c₁;;c₂) = #:c₁ + #:c₂"
  | "#:(if (b) c₁ else c₂) = #:c₁ + #:c₂ + 1"
  | "#:(while (b) c) = #:c + 2" (* zusätzlicher Skip-Knoten *)
  


lemma num_inner_nodes_gr_0:"#:c > 0"
by(induct c) auto

lemma [dest]:"#:c = 0 ==> False"
by(induct c) auto

subsection ‹The state›

type_synonym state = "vname ⇀ val"

fun "interpret" :: "expr → state → val option"
where Val: "interpret (Val v) s = Some v"
  | Var: "interpret (Var V) s = s V"
  | BinOp: "interpret (e₁«bop¬e₂) s =
    (case interpret e₁ s of None → None
                         | Some v₁ → (case interpret e₂ s of None → None
                                                           | Some v₂ → (
      case binop bop v₁ v₂ of None → None | Some v → Some v)))"

end