src/HOL/ex/Exceptions.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Exceptions.thy	Thu Apr 15 14:17:45 2004 +0200
@@ -0,0 +1,187 @@
+(*  Title:      HOL/ex/Exceptions.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   2004 TU Muenchen
+*)
+
+header {* Compiling exception handling *}
+
+theory Exceptions = List_Prefix:
+
+text{* This is a formalization of \cite{HuttonW04}. *}
+
+subsection{*The source language*}
+
+datatype expr = Val int | Add expr expr | Throw | Catch expr expr
+
+consts eval :: "expr \<Rightarrow> int option"
+primrec
+"eval (Val i) = Some i"
+"eval (Add x y) =
+ (case eval x of None \<Rightarrow> None
+  | Some i \<Rightarrow> (case eval y of None \<Rightarrow> None
+               | Some j \<Rightarrow> Some(i+j)))"
+"eval Throw = None"
+"eval (Catch x h) = (case eval x of None \<Rightarrow> eval h | Some i \<Rightarrow> Some i)"
+
+subsection{*The target language*}
+
+datatype instr =
+  Push int | ADD | THROW | Mark nat | Unmark | Label nat | Jump nat
+
+datatype item = VAL int | HAN nat
+
+types code = "instr list"
+      stack = "item list"
+
+consts
+  exec2 :: "bool * code * stack \<Rightarrow> stack"
+  jump :: "nat * code \<Rightarrow> code"
+
+recdef jump "measure(%(l,cs). size cs)"
+"jump(l,[]) = []"
+"jump(l, Label l' # cs) = (if l = l' then cs else jump(l,cs))"
+"jump(l, c # cs) = jump(l,cs)"
+
+lemma size_jump1: "size (jump (l, cs)) < Suc(size cs)"
+apply(induct cs)
+ apply simp
+apply(case_tac a)
+apply auto
+done
+
+lemma size_jump2: "size (jump (l, cs)) < size cs \<or> jump(l,cs) = cs"
+apply(induct cs)
+ apply simp
+apply(case_tac a)
+apply auto
+done
+
+syntax
+  exec   :: "code \<Rightarrow> stack \<Rightarrow> stack"
+  unwind :: "code \<Rightarrow> stack \<Rightarrow> stack"
+translations
+  "exec cs s" == "exec2(True,cs,s)"
+  "unwind cs s" == "exec2(False,cs,s)"
+
+recdef exec2
+ "inv_image (measure(%cs. size cs) <*lex*> measure(%s. size s))
+            (%(b,cs,s). (cs,s))"
+"exec [] s = s"
+"exec (Push i#cs) s = exec cs (VAL i # s)"
+"exec (ADD#cs) (VAL j # VAL i # s) = exec cs (VAL(i+j) # s)"
+"exec (THROW#cs) s = unwind cs s"
+"exec (Mark l#cs) s = exec cs (HAN l # s)"
+"exec (Unmark#cs) (v # HAN l # s) = exec cs (v # s)"
+"exec (Label l#cs) s = exec cs s"
+"exec (Jump l#cs) s = exec (jump(l,cs)) s"
+
+"unwind cs [] = []"
+"unwind cs (VAL i # s) = unwind cs s"
+"unwind cs (HAN l # s) = exec (jump(l,cs)) s"
+
+(hints recdef_simp: size_jump1 size_jump2)
+
+subsection{*The compiler*}
+
+consts
+  compile :: "nat \<Rightarrow> expr \<Rightarrow> code * nat"
+primrec
+"compile l (Val i) = ([Push i], l)"
+"compile l (Add x y) = (let (xs,m) = compile l x; (ys,n) = compile m y
+                     in (xs @ ys @ [ADD], n))"
+"compile l Throw = ([THROW],l)"
+"compile l (Catch x h) =
+  (let (xs,m) = compile (l+2) x; (hs,n) = compile m h
+   in (Mark l # xs @ [Unmark, Jump (l+1), Label l] @ hs @ [Label(l+1)], n))"
+
+syntax cmp :: "nat \<Rightarrow> expr \<Rightarrow> code"
+translations "cmp l e" == "fst(compile l e)"
+
+consts
+  isFresh :: "nat \<Rightarrow> stack \<Rightarrow> bool"
+primrec
+"isFresh l [] = True"
+"isFresh l (it#s) = (case it of VAL i \<Rightarrow> isFresh l s
+                     | HAN l' \<Rightarrow> l' < l \<and> isFresh l s)"
+
+constdefs
+  conv :: "code \<Rightarrow> stack \<Rightarrow> int option \<Rightarrow> stack"
+ "conv cs s io == case io of None \<Rightarrow> unwind cs s
+                  | Some i \<Rightarrow> exec cs (VAL i # s)"
+
+subsection{* The proofs*}
+
+declare
+  conv_def[simp] option.splits[split] Let_def[simp]
+
+lemma 3:
+  "(\<And>l. c = Label l \<Longrightarrow> isFresh l s) \<Longrightarrow> unwind (c#cs) s = unwind cs s"
+apply(induct s)
+ apply simp
+apply(auto)
+apply(case_tac a)
+apply auto
+apply(case_tac c)
+apply auto
+done
+
+corollary [simp]:
+  "(!!l. c \<noteq> Label l) \<Longrightarrow> unwind (c#cs) s = unwind cs s"
+by(blast intro: 3)
+
+corollary [simp]:
+  "isFresh l s \<Longrightarrow> unwind (Label l#cs) s = unwind cs s"
+by(blast intro: 3)
+
+
+lemma 5: "\<lbrakk> isFresh l s; l \<le> m \<rbrakk> \<Longrightarrow> isFresh m s"
+apply(induct s)
+ apply simp
+apply(auto split:item.split)
+done
+
+corollary [simp]: "isFresh l s \<Longrightarrow> isFresh (Suc l) s"
+by(auto intro:5)
+
+
+lemma 6: "\<And>l. l \<le> snd(compile l e)"
+proof(induct e)
+  case Val thus ?case by simp
+next
+  case (Add x y)
+  have "l \<le> snd (compile l x)"
+   and "snd (compile l x) \<le> snd (compile (snd (compile l x)) y)" .
+  thus ?case by(simp_all add:split_def)
+next
+  case Throw thus ?case by simp
+next
+  case (Catch x h)
+  have "l+2 \<le> snd (compile (l+2) x)"
+   and "snd (compile (l+2) x) \<le> snd (compile (snd (compile (l+2) x)) h)" .
+  thus ?case by(simp_all add:split_def)
+qed
+
+corollary [simp]: "l < m \<Longrightarrow> l < snd(compile m e)"
+using 6[where l = m and e = e] by auto
+
+corollary [simp]: "isFresh l s \<Longrightarrow> isFresh (snd(compile l e)) s"
+using 5 6 by blast
+
+
+text{* Contrary to the order of the lemmas in the paper, lemma 4 needs the
+above corollary of 5 and 6. *}
+
+lemma 4 [simp]: "\<And>l cs. isFresh l s \<Longrightarrow> unwind (cmp l e @ cs) s = unwind cs s"
+by (induct e) (auto simp add:split_def)
+
+
+lemma 7[simp]: "\<And>m cs. l < m \<Longrightarrow> jump(l, cmp m e @ cs) = jump(l, cs)"
+by (induct e) (simp_all add:split_def)
+
+text{* The compiler correctness theorem: *}
+
+theorem "\<And>l s cs. isFresh l s \<Longrightarrow> exec (cmp l e @ cs) s = conv cs s (eval e)"
+by(induct e)(auto simp add:split_def)
+
+end