theory Com imports Main begin section \The Language\ 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 ("(2_/ \_\ _)" [80,0,81] 80) \ \binary operation\ fun binop :: "bop \ val \ val \ val option" where "binop Eq v\<^sub>1 v\<^sub>2 = Some(Bool(v\<^sub>1 = v\<^sub>2))" | "binop And (Bool b\<^sub>1) (Bool b\<^sub>2) = Some(Bool(b\<^sub>1 \ b\<^sub>2))" | "binop Less (Intg i\<^sub>1) (Intg i\<^sub>2) = Some(Bool(i\<^sub>1 < i\<^sub>2))" | "binop Add (Intg i\<^sub>1) (Intg i\<^sub>2) = Some(Intg(i\<^sub>1 + i\<^sub>2))" | "binop Sub (Intg i\<^sub>1) (Intg i\<^sub>2) = Some(Intg(i\<^sub>1 - i\<^sub>2))" | "binop bop v\<^sub>1 v\<^sub>2 = None" datatype com = Skip | LAss vname expr ("(2_ ::=/ _)" [70,70] 70) \ \local assignment\ | Seq com com ("_;;// _" [61,60] 60) | Cond expr com com ("(2IF '(_')/ _/ ELSE/ _)" [80,79,79] 70) | While expr com ("(2WHILE '(_')/ _)" [80,79] 70) end