# HG changeset patch
# User nipkow
# Date 1082031465 -7200
# Node ID 78b75a9eec010f8ba875055694e56c6b8ba5e80e
# Parent  1acde8c391793b7d32a4c04145410b583ef30621
Added ex/Exceptions.thy

diff -r 1acde8c39179 -r 78b75a9eec01 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Apr 15 13:04:50 2004 +0200
+++ b/src/HOL/IsaMakefile	Thu Apr 15 14:17:45 2004 +0200
@@ -583,7 +583,8 @@
 HOL-ex: HOL $(LOG)/HOL-ex.gz
 
 $(LOG)/HOL-ex.gz: $(OUT)/HOL ex/Antiquote.thy \
-  ex/BT.thy ex/BinEx.thy ex/Group.ML ex/Group.thy ex/Higher_Order_Logic.thy \
+  ex/BT.thy ex/BinEx.thy ex/Exceptions.thy \
+  ex/Group.ML ex/Group.thy ex/Higher_Order_Logic.thy \
   ex/Hilbert_Classical.thy ex/InSort.thy ex/IntRing.ML \
   ex/InductiveInvariant.thy  ex/InductiveInvariant_examples.thy\
   ex/IntRing.thy ex/Intuitionistic.thy \
diff -r 1acde8c39179 -r 78b75a9eec01 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Thu Apr 15 13:04:50 2004 +0200
+++ b/src/HOL/Ring_and_Field.thy	Thu Apr 15 14:17:45 2004 +0200
@@ -5,10 +5,7 @@
     License: GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
-header {*
-  \title{Ring and field structures}
-  \author{Gertrud Bauer, L. C. Paulson and Markus Wenzel}
-*}
+header {* Ring and field structures *}
 
 theory Ring_and_Field = Inductive:
 
diff -r 1acde8c39179 -r 78b75a9eec01 src/HOL/ex/Adder.thy
--- a/src/HOL/ex/Adder.thy	Thu Apr 15 13:04:50 2004 +0200
+++ b/src/HOL/ex/Adder.thy	Thu Apr 15 14:17:45 2004 +0200
@@ -5,6 +5,8 @@
 Implementation of carry chain incrementor and adder.
 *)
 
+header{* Adder *}
+
 theory Adder = Main + Word:
 
 lemma [simp]: "bv_to_nat [b] = bitval b"
diff -r 1acde8c39179 -r 78b75a9eec01 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
diff -r 1acde8c39179 -r 78b75a9eec01 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Thu Apr 15 13:04:50 2004 +0200
+++ b/src/HOL/ex/ROOT.ML	Thu Apr 15 14:17:45 2004 +0200
@@ -30,10 +30,15 @@
 time_use_thy "MergeSort";
 time_use_thy "Puzzle";
 
+no_document use_thy "List_Prefix";
+time_use_thy "Exceptions";
+
 time_use_thy "IntRing";
 
 time_use_thy "set";
 time_use_thy "MT";
+
+no_document use_thy "FuncSet";
 time_use_thy "Tarski";
 
 time_use_thy "SVC_Oracle";
@@ -41,4 +46,6 @@
 
 time_use_thy "Refute_Examples";
 
+no_document use_thy "Word";
 time_use_thy "Adder";
+
diff -r 1acde8c39179 -r 78b75a9eec01 src/HOL/ex/Tarski.thy
--- a/src/HOL/ex/Tarski.thy	Thu Apr 15 13:04:50 2004 +0200
+++ b/src/HOL/ex/Tarski.thy	Thu Apr 15 14:17:45 2004 +0200
@@ -125,7 +125,7 @@
                       (| pset=intY1, order=induced intY1 r|)"
 
 
-subsubsection {* Partial Order *}
+subsection {* Partial Order *}
 
 lemma (in PO) PO_imp_refl: "refl A r"
 apply (insert cl_po)
@@ -300,7 +300,7 @@
 done
 
 
-subsubsection {* sublattice *}
+subsection {* sublattice *}
 
 lemma (in PO) sublattice_imp_CL:
      "S <<= cl  ==> (| pset = S, order = induced S r |) \<in> CompleteLattice"
@@ -312,7 +312,7 @@
 by (simp add: sublattice_def A_def r_def)
 
 
-subsubsection {* lub *}
+subsection {* lub *}
 
 lemma (in CL) lub_unique: "[| S <= A; isLub S cl x; isLub S cl L|] ==> x = L"
 apply (rule antisymE)
@@ -379,7 +379,7 @@
 by (simp add: isLub_def A_def r_def)
 
 
-subsubsection {* glb *}
+subsection {* glb *}
 
 lemma (in CL) glb_in_lattice: "S <= A ==> glb S cl \<in> A"
 apply (subst glb_dual_lub)
@@ -427,7 +427,7 @@
 done
 
 
-subsubsection {* fixed points *}
+subsection {* fixed points *}
 
 lemma fix_subset: "fix f A <= A"
 by (simp add: fix_def, fast)
@@ -441,7 +441,7 @@
 done
 
 
-subsubsection {* lemmas for Tarski, lub *}
+subsection {* lemmas for Tarski, lub *}
 lemma (in CLF) lubH_le_flubH:
      "H = {x. (x, f x) \<in> r & x \<in> A} ==> (lub H cl, f (lub H cl)) \<in> r"
 apply (rule lub_least, fast)
@@ -511,7 +511,7 @@
 apply (rule lubH_is_fixp, assumption)
 done
 
-subsubsection {* Tarski fixpoint theorem 1, first part *}
+subsection {* Tarski fixpoint theorem 1, first part *}
 lemma (in CLF) T_thm_1_lub: "lub P cl = lub {x. (x, f x) \<in> r & x \<in> A} cl"
 apply (rule sym)
 apply (simp add: P_def)
@@ -540,7 +540,7 @@
                  dualPO CL_dualCL CLF_dual dualr_iff)
 done
 
-subsubsection {* interval *}
+subsection {* interval *}
 
 lemma (in CLF) rel_imp_elem: "(x, y) \<in> r ==> x \<in> A"
 apply (insert CO_refl)
@@ -680,7 +680,7 @@
     interval_is_sublattice [THEN sublattice_imp_CL]
 
 
-subsubsection {* Top and Bottom *}
+subsection {* Top and Bottom *}
 lemma (in CLF) Top_dual_Bot: "Top cl = Bot (dual cl)"
 by (simp add: Top_def Bot_def least_def greatest_def dualA_iff dualr_iff)
 
@@ -741,7 +741,7 @@
                  dualA_iff A_def dualPO CL_dualCL CLF_dual)
 done
 
-subsubsection {* fixed points form a partial order *}
+subsection {* fixed points form a partial order *}
 
 lemma (in CLF) fixf_po: "(| pset = P, order = induced P r|) \<in> PartialOrder"
 by (simp add: P_def fix_subset po_subset_po)
diff -r 1acde8c39179 -r 78b75a9eec01 src/HOL/ex/document/root.bib
--- a/src/HOL/ex/document/root.bib	Thu Apr 15 13:04:50 2004 +0200
+++ b/src/HOL/ex/document/root.bib	Thu Apr 15 14:17:45 2004 +0200
@@ -7,6 +7,11 @@
   number =       68
 }
 
+@inproceedings{HuttonW04,author={Graham Hutton and Joel Wright},
+title={Compiling Exceptions Correctly},
+booktitle={Proc.\ Conf.\ Mathematics of Program Construction},
+year=2004,note={To appear}}
+
 @InProceedings{Kamm-et-al:1999,
   author =       {Florian Kamm{\"u}ller and Markus Wenzel and
                   Lawrence C. Paulson},