theory WhileLang imports Main (* Code_Integer *) begin datatype var = V nat (".v_" 90) datatype iexp = Var var | Const int | Plus iexp iexp | Mult iexp iexp datatype bexp = Le iexp iexp ("_ .\. _" [80, 80] 10) datatype com = SKIP | Asgn var iexp ("_::= _" [80, 80] 10) | Semi com com ("_; _" [70, 60] 10) | Cond bexp com com ("IF _ THEN _ ELSE _" 60) | While bexp com ("WHILE _ DO _" 60) type_synonym state = "var \ int" fun ieval :: "state \ iexp \ int" where "ieval s (Var v) = (s v)" | "ieval s (Const i) = i" | "ieval s (Plus li ri) = (ieval s li) + (ieval s ri)" | "ieval s (Mult li ri) = (ieval s li) * (ieval s ri)" fun beval :: "state \ bexp \ bool" where "beval s (Le li ri) = ((ieval s li) \ (ieval s ri))" (* export_code ieval beval in Haskell module_name While file haskell *) (* Big Step Semantics *) inductive exec :: "state \ com \ state \ bool" ("_/ -_\/ _" [50,0,50] 50) where Skip: "s -SKIP\ s" | Asgn: "s -x::=e\ s(x:= ieval s e)" | Semi: "\ s0 -c1\ s1; s1 -c2\ s2 \ \ s0 -c1;c2\ s2" | IfT: "\ (beval s b); s -c1\ t \ \ s -IF b THEN c1 ELSE c2\ t" | IfF: "\ \(beval s b); s -c2\ t \ \ s -IF b THEN c1 ELSE c2\ t" | WhileF: "\(beval s b) \ s -WHILE b DO c\ s" | WhileT: "\ (beval s b); s -c\ t; t -WHILE b DO c\ u \ \ s -WHILE b DO c\ u" lemma [iff]: "(s -SKIP\ t) = (s=t)" by (best elim: exec.cases intro:exec.intros) lemma [iff]: "(s -x::=e\ t) = (s(x:= ieval s e)=t)" by (best elim: exec.cases intro:exec.intros) lemma semic_eqv: "(s -c;d\ u) = (\t. s -c\ t \ t -d\ u)" by (best elim: exec.cases intro:exec.intros) lemma [iff]: "(s -IF b THEN c ELSE d\ t) = (s -if (beval s b) then c else d\ t)" by auto (blast elim: exec.cases intro:exec.intros)+ (* Small Step Semantics *) datatype config = Config state com ("\_, _\") | Termin state ("\_\") ("_/ \\<^sub>1/ _" [50,50] 50) end