*** empty log message ***
authornipkow
Mon Jul 12 12:11:46 2004 +0200 (2004-07-12 ago)
changeset 1503719b3b0382303
parent 15036 cab1c1fc1851
child 15038 eb2469e495cd
*** empty log message ***
src/HOL/IsaMakefile
src/HOL/ex/Exceptions.thy
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Sun Jul 11 20:35:50 2004 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Jul 12 12:11:46 2004 +0200
     1.3 @@ -583,8 +583,7 @@
     1.4  HOL-ex: HOL $(LOG)/HOL-ex.gz
     1.5  
     1.6  $(LOG)/HOL-ex.gz: $(OUT)/HOL ex/Antiquote.thy \
     1.7 -  ex/BT.thy ex/BinEx.thy ex/Exceptions.thy \
     1.8 -  ex/Higher_Order_Logic.thy \
     1.9 +  ex/BT.thy ex/BinEx.thy ex/Higher_Order_Logic.thy \
    1.10    ex/Hilbert_Classical.thy ex/InSort.thy \
    1.11    ex/InductiveInvariant.thy  ex/InductiveInvariant_examples.thy\
    1.12    ex/Intuitionistic.thy \
     2.1 --- a/src/HOL/ex/Exceptions.thy	Sun Jul 11 20:35:50 2004 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,187 +0,0 @@
     2.4 -(*  Title:      HOL/ex/Exceptions.thy
     2.5 -    ID:         $Id$
     2.6 -    Author:     Tobias Nipkow
     2.7 -    Copyright   2004 TU Muenchen
     2.8 -*)
     2.9 -
    2.10 -header {* Compiling exception handling *}
    2.11 -
    2.12 -theory Exceptions = List_Prefix:
    2.13 -
    2.14 -text{* This is a formalization of \cite{HuttonW04}. *}
    2.15 -
    2.16 -subsection{*The source language*}
    2.17 -
    2.18 -datatype expr = Val int | Add expr expr | Throw | Catch expr expr
    2.19 -
    2.20 -consts eval :: "expr \<Rightarrow> int option"
    2.21 -primrec
    2.22 -"eval (Val i) = Some i"
    2.23 -"eval (Add x y) =
    2.24 - (case eval x of None \<Rightarrow> None
    2.25 -  | Some i \<Rightarrow> (case eval y of None \<Rightarrow> None
    2.26 -               | Some j \<Rightarrow> Some(i+j)))"
    2.27 -"eval Throw = None"
    2.28 -"eval (Catch x h) = (case eval x of None \<Rightarrow> eval h | Some i \<Rightarrow> Some i)"
    2.29 -
    2.30 -subsection{*The target language*}
    2.31 -
    2.32 -datatype instr =
    2.33 -  Push int | ADD | THROW | Mark nat | Unmark | Label nat | Jump nat
    2.34 -
    2.35 -datatype item = VAL int | HAN nat
    2.36 -
    2.37 -types code = "instr list"
    2.38 -      stack = "item list"
    2.39 -
    2.40 -consts
    2.41 -  exec2 :: "bool * code * stack \<Rightarrow> stack"
    2.42 -  jump :: "nat * code \<Rightarrow> code"
    2.43 -
    2.44 -recdef jump "measure(%(l,cs). size cs)"
    2.45 -"jump(l,[]) = []"
    2.46 -"jump(l, Label l' # cs) = (if l = l' then cs else jump(l,cs))"
    2.47 -"jump(l, c # cs) = jump(l,cs)"
    2.48 -
    2.49 -lemma size_jump1: "size (jump (l, cs)) < Suc(size cs)"
    2.50 -apply(induct cs)
    2.51 - apply simp
    2.52 -apply(case_tac a)
    2.53 -apply auto
    2.54 -done
    2.55 -
    2.56 -lemma size_jump2: "size (jump (l, cs)) < size cs \<or> jump(l,cs) = cs"
    2.57 -apply(induct cs)
    2.58 - apply simp
    2.59 -apply(case_tac a)
    2.60 -apply auto
    2.61 -done
    2.62 -
    2.63 -syntax
    2.64 -  exec   :: "code \<Rightarrow> stack \<Rightarrow> stack"
    2.65 -  unwind :: "code \<Rightarrow> stack \<Rightarrow> stack"
    2.66 -translations
    2.67 -  "exec cs s" == "exec2(True,cs,s)"
    2.68 -  "unwind cs s" == "exec2(False,cs,s)"
    2.69 -
    2.70 -recdef exec2
    2.71 - "inv_image (measure(%cs. size cs) <*lex*> measure(%s. size s))
    2.72 -            (%(b,cs,s). (cs,s))"
    2.73 -"exec [] s = s"
    2.74 -"exec (Push i#cs) s = exec cs (VAL i # s)"
    2.75 -"exec (ADD#cs) (VAL j # VAL i # s) = exec cs (VAL(i+j) # s)"
    2.76 -"exec (THROW#cs) s = unwind cs s"
    2.77 -"exec (Mark l#cs) s = exec cs (HAN l # s)"
    2.78 -"exec (Unmark#cs) (v # HAN l # s) = exec cs (v # s)"
    2.79 -"exec (Label l#cs) s = exec cs s"
    2.80 -"exec (Jump l#cs) s = exec (jump(l,cs)) s"
    2.81 -
    2.82 -"unwind cs [] = []"
    2.83 -"unwind cs (VAL i # s) = unwind cs s"
    2.84 -"unwind cs (HAN l # s) = exec (jump(l,cs)) s"
    2.85 -
    2.86 -(hints recdef_simp: size_jump1 size_jump2)
    2.87 -
    2.88 -subsection{*The compiler*}
    2.89 -
    2.90 -consts
    2.91 -  compile :: "nat \<Rightarrow> expr \<Rightarrow> code * nat"
    2.92 -primrec
    2.93 -"compile l (Val i) = ([Push i], l)"
    2.94 -"compile l (Add x y) = (let (xs,m) = compile l x; (ys,n) = compile m y
    2.95 -                     in (xs @ ys @ [ADD], n))"
    2.96 -"compile l Throw = ([THROW],l)"
    2.97 -"compile l (Catch x h) =
    2.98 -  (let (xs,m) = compile (l+2) x; (hs,n) = compile m h
    2.99 -   in (Mark l # xs @ [Unmark, Jump (l+1), Label l] @ hs @ [Label(l+1)], n))"
   2.100 -
   2.101 -syntax cmp :: "nat \<Rightarrow> expr \<Rightarrow> code"
   2.102 -translations "cmp l e" == "fst(compile l e)"
   2.103 -
   2.104 -consts
   2.105 -  isFresh :: "nat \<Rightarrow> stack \<Rightarrow> bool"
   2.106 -primrec
   2.107 -"isFresh l [] = True"
   2.108 -"isFresh l (it#s) = (case it of VAL i \<Rightarrow> isFresh l s
   2.109 -                     | HAN l' \<Rightarrow> l' < l \<and> isFresh l s)"
   2.110 -
   2.111 -constdefs
   2.112 -  conv :: "code \<Rightarrow> stack \<Rightarrow> int option \<Rightarrow> stack"
   2.113 - "conv cs s io == case io of None \<Rightarrow> unwind cs s
   2.114 -                  | Some i \<Rightarrow> exec cs (VAL i # s)"
   2.115 -
   2.116 -subsection{* The proofs*}
   2.117 -
   2.118 -declare
   2.119 -  conv_def[simp] option.splits[split] Let_def[simp]
   2.120 -
   2.121 -lemma 3:
   2.122 -  "(\<And>l. c = Label l \<Longrightarrow> isFresh l s) \<Longrightarrow> unwind (c#cs) s = unwind cs s"
   2.123 -apply(induct s)
   2.124 - apply simp
   2.125 -apply(auto)
   2.126 -apply(case_tac a)
   2.127 -apply auto
   2.128 -apply(case_tac c)
   2.129 -apply auto
   2.130 -done
   2.131 -
   2.132 -corollary [simp]:
   2.133 -  "(!!l. c \<noteq> Label l) \<Longrightarrow> unwind (c#cs) s = unwind cs s"
   2.134 -by(blast intro: 3)
   2.135 -
   2.136 -corollary [simp]:
   2.137 -  "isFresh l s \<Longrightarrow> unwind (Label l#cs) s = unwind cs s"
   2.138 -by(blast intro: 3)
   2.139 -
   2.140 -
   2.141 -lemma 5: "\<lbrakk> isFresh l s; l \<le> m \<rbrakk> \<Longrightarrow> isFresh m s"
   2.142 -apply(induct s)
   2.143 - apply simp
   2.144 -apply(auto split:item.split)
   2.145 -done
   2.146 -
   2.147 -corollary [simp]: "isFresh l s \<Longrightarrow> isFresh (Suc l) s"
   2.148 -by(auto intro:5)
   2.149 -
   2.150 -
   2.151 -lemma 6: "\<And>l. l \<le> snd(compile l e)"
   2.152 -proof(induct e)
   2.153 -  case Val thus ?case by simp
   2.154 -next
   2.155 -  case (Add x y)
   2.156 -  have "l \<le> snd (compile l x)"
   2.157 -   and "snd (compile l x) \<le> snd (compile (snd (compile l x)) y)" .
   2.158 -  thus ?case by(simp_all add:split_def)
   2.159 -next
   2.160 -  case Throw thus ?case by simp
   2.161 -next
   2.162 -  case (Catch x h)
   2.163 -  have "l+2 \<le> snd (compile (l+2) x)"
   2.164 -   and "snd (compile (l+2) x) \<le> snd (compile (snd (compile (l+2) x)) h)" .
   2.165 -  thus ?case by(simp_all add:split_def)
   2.166 -qed
   2.167 -
   2.168 -corollary [simp]: "l < m \<Longrightarrow> l < snd(compile m e)"
   2.169 -using 6[where l = m and e = e] by auto
   2.170 -
   2.171 -corollary [simp]: "isFresh l s \<Longrightarrow> isFresh (snd(compile l e)) s"
   2.172 -using 5 6 by blast
   2.173 -
   2.174 -
   2.175 -text{* Contrary to the order of the lemmas in the paper, lemma 4 needs the
   2.176 -above corollary of 5 and 6. *}
   2.177 -
   2.178 -lemma 4 [simp]: "\<And>l cs. isFresh l s \<Longrightarrow> unwind (cmp l e @ cs) s = unwind cs s"
   2.179 -by (induct e) (auto simp add:split_def)
   2.180 -
   2.181 -
   2.182 -lemma 7[simp]: "\<And>m cs. l < m \<Longrightarrow> jump(l, cmp m e @ cs) = jump(l, cs)"
   2.183 -by (induct e) (simp_all add:split_def)
   2.184 -
   2.185 -text{* The compiler correctness theorem: *}
   2.186 -
   2.187 -theorem "\<And>l s cs. isFresh l s \<Longrightarrow> exec (cmp l e @ cs) s = conv cs s (eval e)"
   2.188 -by(induct e)(auto simp add:split_def)
   2.189 -
   2.190 -end
     3.1 --- a/src/HOL/ex/ROOT.ML	Sun Jul 11 20:35:50 2004 +0200
     3.2 +++ b/src/HOL/ex/ROOT.ML	Mon Jul 12 12:11:46 2004 +0200
     3.3 @@ -30,9 +30,6 @@
     3.4  time_use_thy "MergeSort";
     3.5  time_use_thy "Puzzle";
     3.6  
     3.7 -no_document use_thy "List_Prefix";
     3.8 -time_use_thy "Exceptions";
     3.9 -
    3.10  time_use_thy "Lagrange";
    3.11  
    3.12  time_use_thy "set";