Theory Com

header {* \isachapter{Instantiating the Framework with a simple While-Language}
  \isaheader{Commands} *}

theory Com imports Main begin

section {* 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"

section {* 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

section {* The state *}

type_synonym state = "vname \<rightharpoonup> 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