theory Semantics
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    ("_ \<guillemotleft>_\<guillemotright> _" [80,0,81] 80)  -- "binary operation"


fun binop :: "bop \<Rightarrow> val \<Rightarrow> val \<Rightarrow> val option"
where "binop Eq v\<^isub>1 v\<^isub>2               = Some(Bool(v\<^isub>1 = v\<^isub>2))"
  | "binop And (Bool b\<^isub>1) (Bool b\<^isub>2)  = Some(Bool(b\<^isub>1 \<and> b\<^isub>2))"
  | "binop Less (Intg i\<^isub>1) (Intg i\<^isub>2) = Some(Bool(i\<^isub>1 < i\<^isub>2))"
  | "binop Add (Intg i\<^isub>1) (Intg i\<^isub>2)  = Some(Intg(i\<^isub>1 + i\<^isub>2))"
  | "binop Sub (Intg i\<^isub>1) (Intg i\<^isub>2)  = Some(Intg(i\<^isub>1 - i\<^isub>2))"

  | "binop bop v\<^isub>1 v\<^isub>2                = None"


datatype com
  = Skip
  | LAss vname expr        ("_::=_" [70,70] 70)  -- "local assignment"
  | Seq com com            ("_;;/ _" [61,60] 60)
  | Cond expr com com      ("IF '(_') _/ ELSE _" [80,79,79] 70)
  | While expr com         ("WHILE '(_') _" [80,79] 70)


fun fv :: "expr \<Rightarrow> vname set" --"free variables in an expression"
where
  FVc: "fv (Val v) = {}"
  | FVv: "fv (Var x) = {x}"
  | FVe: "fv (e\<^isub>1 \<guillemotleft>bop\<guillemotright> e\<^isub>2) = fv e\<^isub>1 \<union> fv e\<^isub>2"

subsection {* State *}

type_synonym
  state = "vname \<rightharpoonup> val"


fun "interpret" :: "expr \<Rightarrow> state \<Rightarrow> val option" ("\<lbrakk>_\<rbrakk>_" [0,52] 51)
where Val: "\<lbrakk>Val v\<rbrakk> s = Some v"
  | Var:   "\<lbrakk>Var x\<rbrakk> s = s x"
  | BinOp: "\<lbrakk>e\<^isub>1\<guillemotleft>bop\<guillemotright>e\<^isub>2\<rbrakk> s = (case \<lbrakk>e\<^isub>1\<rbrakk> s of None \<Rightarrow> None
    | Some v\<^isub>1 \<Rightarrow> (case \<lbrakk>e\<^isub>2\<rbrakk> s of None \<Rightarrow> None
      | Some v\<^isub>2 \<Rightarrow> binop bop v\<^isub>1 v\<^isub>2)
    )"

fun interpretTime :: "expr \<Rightarrow> nat" ("\<lbrakk>_\<rbrakk>\<^sub>t" [0] 110)
  (* Untergestelltes t mit "\<lbrakk>e\<rbrakk>\ <^sub>t" (ohne Leerzeichen) *)
where "\<lbrakk>Val v\<rbrakk>\<^sub>t = 1"
  | "\<lbrakk>Var x\<rbrakk>\<^sub>t = 1"
  | "\<lbrakk>e\<^isub>1 \<guillemotleft>bop\<guillemotright> e\<^isub>2\<rbrakk>\<^sub>t = Suc (\<lbrakk>e\<^isub>1\<rbrakk>\<^sub>t + \<lbrakk>e\<^isub>2\<rbrakk>\<^sub>t)"

subsection {* Big Step Semantics *}

inductive eval :: "com \<Rightarrow> state \<Rightarrow> state \<Rightarrow> nat \<Rightarrow> bool" ("((1\<langle>_,/_\<rangle>) \<Rightarrow>/ _ : _)" [0,0,0,0] 0)
where
  EvalSkip: "\<langle>Skip,s\<rangle> \<Rightarrow> s : 1"

  | EvalLAss: "\<langle>x::=e,s\<rangle> \<Rightarrow> s(x := \<lbrakk>e\<rbrakk>s) : Suc (\<lbrakk>e\<rbrakk>\<^sub>t)"

  | EvalSeq:
  "\<lbrakk>\<langle>c\<^isub>1,s\<rangle> \<Rightarrow> s'' : t\<^isub>1; \<langle>c\<^isub>2,s''\<rangle> \<Rightarrow> s' : t\<^isub>2\<rbrakk> \<Longrightarrow> \<langle>c\<^isub>1;;c\<^isub>2,s\<rangle> \<Rightarrow> s' : Suc (t\<^isub>1 + t\<^isub>2)"

  | EvalCondTrue:
  "\<lbrakk>\<lbrakk>b\<rbrakk> s = Some true; \<langle>c\<^isub>1,s\<rangle> \<Rightarrow> s' : t\<rbrakk> \<Longrightarrow> \<langle>IF (b) c\<^isub>1 ELSE c\<^isub>2,s\<rangle> \<Rightarrow> s' : Suc (\<lbrakk>b\<rbrakk>\<^sub>t + t)"

  | EvalCondFalse:
  "\<lbrakk>\<lbrakk>b\<rbrakk> s = Some false; \<langle>c\<^isub>2,s\<rangle> \<Rightarrow> s' : t\<rbrakk> \<Longrightarrow> \<langle>IF (b) c\<^isub>1 ELSE c\<^isub>2,s\<rangle> \<Rightarrow> s' : Suc (\<lbrakk>b\<rbrakk>\<^sub>t + t)"

  | EvalWhileTrue:
  "\<lbrakk>\<lbrakk>b\<rbrakk> s = Some true; \<langle>c,s\<rangle> \<Rightarrow> s'' : t\<^isub>c; \<langle>WHILE (b) c,s''\<rangle> \<Rightarrow> s' : t\<^isub>w\<rbrakk>
  \<Longrightarrow> \<langle>WHILE (b) c,s\<rangle> \<Rightarrow> s' : Suc (\<lbrakk>b\<rbrakk>\<^sub>t + t\<^isub>c + t\<^isub>w)"

  | EvalWhileFalse:
  "\<lbrakk>b\<rbrakk> s = Some false \<Longrightarrow> \<langle>WHILE (b) c,s\<rangle> \<Rightarrow> s : Suc (\<lbrakk>b\<rbrakk>\<^sub>t)"

text {* Some example programs: *}

text {* x = 8; 
        y = 10; 
        if (x < y) { 
          x++; 
        } else { 
          y = y + 3; 
        } 
  *} 

value "''x''::=Val(Intg 8);; ''y''::=Val(Intg 10);;
  IF (Var ''x'' \<guillemotleft>Less\<guillemotright> Var ''y'') (''x''::= Var ''x'' \<guillemotleft>Add\<guillemotright> Val(Intg 1)) 
  ELSE (''y''::= Var ''y'' \<guillemotleft>Add\<guillemotright> Val(Intg 3))"


text {* x = 8; 
        if (x < y) { 
          x++; 
        } else { 
          y = y + 3; 
          x = 9; 
        } 
        y = x;
  *} 

value "''x''::=Val(Intg 8);;
  (IF (Var ''x'' \<guillemotleft>Less\<guillemotright> Var ''y'') (''x''::= Var ''x'' \<guillemotleft>Add\<guillemotright> Val(Intg 1)) 
   ELSE (''y''::= Var ''y'' \<guillemotleft>Add\<guillemotright> Val(Intg 3);; ''x''::=Val(Intg 9)));; 
  ''y''::=Var ''x''"


text {* if (x < 10) {
          x = 8;
        } else {
          x = 14;
        }
        while (x < 7) {
          x = x + x;
        }
  *}

value "IF (Var ''x'' \<guillemotleft>Less\<guillemotright> Val(Intg 10)) (''x''::=Val(Intg 8))
       ELSE (''x''::=Val(Intg 14));;
       WHILE (Var ''x'' \<guillemotleft>Less\<guillemotright> Val(Intg 7)) (''x''::= Var ''x'' \<guillemotleft>Add\<guillemotright>Var ''x'')"


text {* x = 13;
        y = 7;
        while (y == x - 5) {
          x++;
        }
  *}

value "''x''::=Val(Intg 13);; ''y''::=Val(Intg 7);;
       WHILE (Var ''y'' \<guillemotleft>Eq\<guillemotright> (Var ''x'' \<guillemotleft>Sub\<guillemotright> Val(Intg 5))) 
             (''x''::= Var ''x'' \<guillemotleft>Add\<guillemotright> Val(Intg 1))"



subsection {* Type System *}

datatype ty = Boolean | Integer

type_synonym env = "vname \<rightharpoonup> ty"

inductive expr_typing :: "env \<Rightarrow> expr \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [51,0,100] 0)
  for \<Gamma>::env
where 
  TypeValIntg: "\<Gamma> \<turnstile> Val(Intg i) : Integer"
  
  | TypeValBool: "\<Gamma> \<turnstile> Val(Bool b) : Boolean"

  | TypeVar: "\<Gamma> x = Some T \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"

  | TypeBopEq: "\<lbrakk>\<Gamma> \<turnstile> e\<^isub>1 : T; \<Gamma> \<turnstile> e\<^isub>2 : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> e\<^isub>1 \<guillemotleft>Eq\<guillemotright> e\<^isub>2 : Boolean"

  | TypeBopAnd: "\<lbrakk>\<Gamma> \<turnstile> e\<^isub>1 : Boolean; \<Gamma> \<turnstile> e\<^isub>2 : Boolean\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> e\<^isub>1 \<guillemotleft>And\<guillemotright> e\<^isub>2 : Boolean"

  | TypeBopLess: "\<lbrakk>\<Gamma> \<turnstile> e\<^isub>1 : Integer; \<Gamma> \<turnstile> e\<^isub>2 : Integer\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> e\<^isub>1 \<guillemotleft>Less\<guillemotright> e\<^isub>2 : Boolean"

  | TypeBopAdd: "\<lbrakk>\<Gamma> \<turnstile> e\<^isub>1 : Integer; \<Gamma> \<turnstile> e\<^isub>2 : Integer\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> e\<^isub>1 \<guillemotleft>Add\<guillemotright> e\<^isub>2 : Integer"

  | TypeBopSub: "\<lbrakk>\<Gamma> \<turnstile> e\<^isub>1 : Integer; \<Gamma> \<turnstile> e\<^isub>2 : Integer\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> e\<^isub>1 \<guillemotleft>Sub\<guillemotright> e\<^isub>2 : Integer"


inductive WT :: "env \<Rightarrow> com \<Rightarrow> bool" ("_ \<turnstile> _" [51,51] 0)
  for \<Gamma>::env
where 
  WTSkip: "\<Gamma> \<turnstile> Skip"

  | WTLAss: "\<lbrakk>\<Gamma> x = Some T; \<Gamma> \<turnstile> e : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> x ::= e"

  | WTSeq: "\<lbrakk>\<Gamma> \<turnstile> c\<^isub>1; \<Gamma> \<turnstile> c\<^isub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> c\<^isub>1;;c\<^isub>2"

  | WTCond: "\<lbrakk>\<Gamma> \<turnstile> b : Boolean; \<Gamma> \<turnstile> c\<^isub>1; \<Gamma> \<turnstile> c\<^isub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> IF (b) c\<^isub>1 ELSE c\<^isub>2"

  | WTWhile: "\<lbrakk>\<Gamma> \<turnstile> b : Boolean; \<Gamma> \<turnstile> c\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> WHILE (b) c"

end