--- a/src/HOL/IsaMakefile Sun Jul 11 20:35:50 2004 +0200
+++ b/src/HOL/IsaMakefile Mon Jul 12 12:11:46 2004 +0200
@@ -583,8 +583,7 @@
HOL-ex: HOL $(LOG)/HOL-ex.gz
$(LOG)/HOL-ex.gz: $(OUT)/HOL ex/Antiquote.thy \
- ex/BT.thy ex/BinEx.thy ex/Exceptions.thy \
- ex/Higher_Order_Logic.thy \
+ ex/BT.thy ex/BinEx.thy ex/Higher_Order_Logic.thy \
ex/Hilbert_Classical.thy ex/InSort.thy \
ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy\
ex/Intuitionistic.thy \
--- a/src/HOL/ex/Exceptions.thy Sun Jul 11 20:35:50 2004 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,187 +0,0 @@
-(* 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 Sun Jul 11 20:35:50 2004 +0200
+++ b/src/HOL/ex/ROOT.ML Mon Jul 12 12:11:46 2004 +0200
@@ -30,9 +30,6 @@
time_use_thy "MergeSort";
time_use_thy "Puzzle";
-no_document use_thy "List_Prefix";
-time_use_thy "Exceptions";
-
time_use_thy "Lagrange";
time_use_thy "set";