--- 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 \
--- 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:
--- 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"
--- /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
--- 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";
+
--- 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)
--- 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},