# Theory Com

```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⇩1 v⇩2               = Some(Bool(v⇩1 = v⇩2))"
| "binop And (Bool b⇩1) (Bool b⇩2)  = Some(Bool(b⇩1 ∧ b⇩2))"
| "binop Less (Intg i⇩1) (Intg i⇩2) = Some(Bool(i⇩1 < i⇩2))"
| "binop Add (Intg i⇩1) (Intg i⇩2)  = Some(Intg(i⇩1 + i⇩2))"
| "binop Sub (Intg i⇩1) (Intg i⇩2)  = Some(Intg(i⇩1 - i⇩2))"
| "binop bop v⇩1 v⇩2                = 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⇩1;;c⇩2)            = #:c⇩1 + #:c⇩2"
| "#:(if (b) c⇩1 else c⇩2) = #:c⇩1 + #:c⇩2 + 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⇩1«bop»e⇩2) s =
(case interpret e⇩1 s of None ⇒ None
| Some v⇩1 ⇒ (case interpret e⇩2 s of None ⇒ None
| Some v⇩2 ⇒ (
case binop bop v⇩1 v⇩2 of None ⇒ None | Some v ⇒ Some v)))"

end
```