# HG changeset patch # User wenzelm # Date 1278790696 -7200 # Node ID b55f848f34fcfd2211ffcc37fef2d08adaede7ef # Parent decac8d1c8e71e1e036b02a897e76332824550a7# Parent 5d2b3e8273718144ca21ab5477e2ec94887f55b7 merged diff -r 5d2b3e827371 -r b55f848f34fc Admin/check_ml_headers --- a/Admin/check_ml_headers Tue Jul 06 21:33:14 2010 +0200 +++ b/Admin/check_ml_headers Sat Jul 10 21:38:16 2010 +0200 @@ -1,14 +1,14 @@ #!/usr/bin/env bash # -# check_ml_headers - check headers of *.ML files in Distribution for inconsistencies +# check_ml_headers - check headers of *.ML files in distribution for inconsistencies # # requires some GNU tools # -ONLY_FILENAMES=1 +ONLY_FILENAMES="" if [ "$1" == "-o" ] then - ONLY_FILENAMES="" + ONLY_FILENAMES=1 fi REPORT_EMPTY="" @@ -25,9 +25,9 @@ FILELOC="${LOC:${#ISABELLE_SRC}}" if [ "$TITLE" != "$FILELOC" ] then - if [ -n "$REPORT_EMPTY" -o -n "$TITLE" ] + if [ -n "$TITLE" -o \( -n "$REPORT_EMPTY" -a $(basename "$FILELOC") != "ROOT.ML" \) ] then - if [ -n "$ONLY_FILENAMES" ] + if [ -z "$ONLY_FILENAMES" ] then echo "Inconsistency in $LOC: $TITLE" else diff -r 5d2b3e827371 -r b55f848f34fc Admin/isatest/crontab.macbroy28 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/isatest/crontab.macbroy28 Sat Jul 10 21:38:16 2010 +0200 @@ -0,0 +1,12 @@ +17 10 * * 1-6 $HOME/afp/devel/admin/regression - +32 12 * * 0 $HOME/afp/release/admin/regression Isabelle2009-2 + +03 00 * * * $HOME/bin/checkout-admin +17 00 * * * $HOME/bin/isatest-makedist +01 08 * * * $HOME/bin/isatest-check +17 08 * * * $HOME/bin/isatest-doc + +04 23 31 1,3,5,7,8,10,12 * $HOME/bin/logmove +04 23 30 4,6,9,11 * $HOME/bin/logmove +04 23 28 2 * $HOME/bin/logmove + diff -r 5d2b3e827371 -r b55f848f34fc NEWS --- a/NEWS Tue Jul 06 21:33:14 2010 +0200 +++ b/NEWS Sat Jul 10 21:38:16 2010 +0200 @@ -95,6 +95,10 @@ INCOMPATIBILITY. +* Inductive package: offers new command "inductive_simps" to automatically + derive instantiated and simplified equations for inductive predicates, + similar to inductive_cases. + New in Isabelle2009-2 (June 2010) --------------------------------- diff -r 5d2b3e827371 -r b55f848f34fc doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Jul 06 21:33:14 2010 +0200 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Sat Jul 10 21:38:16 2010 +0200 @@ -1000,7 +1000,7 @@ \begin{rail} 'export\_code' ( constexpr + ) \\ ( ( 'in' target ( 'module\_name' string ) ? \\ - ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ? + 'file' ( string | '-' ) ( '(' args ')' ) ?) + ) ? ; const: term @@ -1092,8 +1092,7 @@ single file; for \emph{Haskell}, it refers to a whole directory, where code is generated in multiple files reflecting the module hierarchy. The file specification ``@{text "-"}'' denotes standard - output. For \emph{SML}, omitting the file specification compiles - code internally in the context of the current ML session. + output. Serializers take an optional list of arguments in parentheses. For \emph{SML} and \emph{OCaml}, ``@{text no_signatures}`` omits diff -r 5d2b3e827371 -r b55f848f34fc doc-src/IsarRef/Thy/document/HOL_Specific.tex --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Jul 06 21:33:14 2010 +0200 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Sat Jul 10 21:38:16 2010 +0200 @@ -1016,7 +1016,7 @@ \begin{rail} 'export\_code' ( constexpr + ) \\ ( ( 'in' target ( 'module\_name' string ) ? \\ - ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ? + 'file' ( string | '-' ) ( '(' args ')' ) ?) + ) ? ; const: term @@ -1107,8 +1107,7 @@ single file; for \emph{Haskell}, it refers to a whole directory, where code is generated in multiple files reflecting the module hierarchy. The file specification ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' denotes standard - output. For \emph{SML}, omitting the file specification compiles - code internally in the context of the current ML session. + output. Serializers take an optional list of arguments in parentheses. For \emph{SML} and \emph{OCaml}, ``\isa{no{\isacharunderscore}signatures}`` omits diff -r 5d2b3e827371 -r b55f848f34fc etc/isar-keywords.el --- a/etc/isar-keywords.el Tue Jul 06 21:33:14 2010 +0200 +++ b/etc/isar-keywords.el Sat Jul 10 21:38:16 2010 +0200 @@ -120,6 +120,7 @@ "inductive" "inductive_cases" "inductive_set" + "inductive_simps" "init_toplevel" "instance" "instantiation" @@ -550,7 +551,8 @@ "use")) (defconst isar-keywords-theory-script - '("inductive_cases")) + '("inductive_cases" + "inductive_simps")) (defconst isar-keywords-theory-goal '("ax_specification" diff -r 5d2b3e827371 -r b55f848f34fc lib/browser/GraphBrowser/Graph.java --- a/lib/browser/GraphBrowser/Graph.java Tue Jul 06 21:33:14 2010 +0200 +++ b/lib/browser/GraphBrowser/Graph.java Sat Jul 10 21:38:16 2010 +0200 @@ -17,9 +17,7 @@ public int box_height=0; public int box_height2; - public int box_width; - public int box_width2; - public int box_hspace; + public Graphics gfx; Vector vertices=new Vector(10,10); Vector splines=new Vector(10,10); @@ -185,19 +183,16 @@ public void setParameters(Graphics g) { Enumeration e1=vertices.elements(); - int h,w; - h=w=Integer.MIN_VALUE; + int h; + h=Integer.MIN_VALUE; while (e1.hasMoreElements()) { Box dim=((Vertex)(e1.nextElement())).getLabelSize(g); h=Math.max(h,dim.height); - w=Math.max(w,dim.width); } box_height=h+4; box_height2=box_height/2; - box_width=w+8; - box_width2=box_width/2; - box_hspace=box_width+20; + gfx=g; } /********************************************************************/ @@ -538,12 +533,12 @@ while (e1.hasMoreElements()) { Vector v1=(Vector)(e1.nextElement()); Enumeration e2=v1.elements(); - int x=box_width2; + int x=0; while (e2.hasMoreElements()) { Vertex ve=(Vertex)(e2.nextElement()); - ve.setX(x); + ve.setX(x+ve.box_width2()); ve.setY(y); - x+=box_hspace; + x+=ve.box_width()+20; } y+=box_height+Math.max(35,7*(((Integer)(e3.nextElement())).intValue())); } @@ -638,8 +633,8 @@ } d2=(n!=0?d/n:0); - if (d<0 && (i==0 || ((Vertex)(v.elementAt(i-1))).rightX()+box_hspace-box_width < vx.leftX()+d2) || - d>0 && (i==v.size()-1 || ((Vertex)(v.elementAt(i+1))).leftX()-box_hspace+box_width > vx.rightX()+d2)) + if (d<0 && (i==0 || ((Vertex)(v.elementAt(i-1))).rightX()+20 < vx.leftX()+d2) || + d>0 && (i==v.size()-1 || ((Vertex)(v.elementAt(i+1))).leftX()-20 > vx.rightX()+d2)) vx.setX(vx.getX()+d2); } } @@ -743,8 +738,6 @@ vx2=(Vertex)((vx2.getChildren()).nextElement()); x3=vx2.getX(); y3=vx2.getY(); - // spc=(box_hspace-box_width)/3; - // spc=box_height*3/4; spc=0; leftx = k==0 /* || ((Vertex)(layer.elementAt(k-1))).isDummy() */ ? Integer.MIN_VALUE: diff -r 5d2b3e827371 -r b55f848f34fc lib/browser/GraphBrowser/NormalVertex.java --- a/lib/browser/GraphBrowser/NormalVertex.java Tue Jul 06 21:33:14 2010 +0200 +++ b/lib/browser/GraphBrowser/NormalVertex.java Sat Jul 10 21:38:16 2010 +0200 @@ -58,28 +58,23 @@ public void setDir(String d) { dir=d; } - public int leftX() { return getX()-gra.box_width2; } + public int leftX() { return getX()-box_width2(); } - public int rightX() { return getX()+gra.box_width2; } + public int rightX() { return getX()+box_width2(); } public void drawBox(Graphics g,Color boxColor) { FontMetrics fm = g.getFontMetrics(g.getFont()); int h=fm.getAscent()+fm.getDescent(); g.setColor(boxColor); - g.fillRect(getX()-gra.box_width2,getY(),gra.box_width,gra.box_height); + g.fillRect(getX()-box_width2(),getY(),box_width(),gra.box_height); g.setColor(Color.black); - g.drawRect(getX()-gra.box_width2,getY(),gra.box_width,gra.box_height); - if (getNumber()<0) { + g.drawRect(getX()-box_width2(),getY(),box_width(),gra.box_height); + if (getNumber()<0) g.setColor(Color.red); - label=label.substring(1,label.length()-1); - while (label.length()>0 && fm.stringWidth("["+label+"]")>gra.box_width-8) - label=label.substring(0,label.length()-1); - label="["+label+"]"; - } g.drawString(label, - (int)Math.round((gra.box_width-fm.stringWidth(label))/2.0)+getX()-gra.box_width2, + (int)Math.round((box_width()-fm.stringWidth(label))/2.0)+getX()-box_width2(), fm.getAscent()+(int)Math.round((gra.box_height-h)/2.0)+getY()); } @@ -136,7 +131,7 @@ } public void PS(PrintWriter p) { - p.print(leftX()+" "+getY()+" "+gra.box_width+" "+ + p.print(leftX()+" "+getY()+" "+box_width()+" "+ gra.box_height+" ("); for (int i=0;i _) = less_eq" .. lemma [code, code del]: "(less :: char \ _) = less" .. -export_code * in SML module_name Code_Test - in OCaml module_name Code_Test file - - in Haskell file - - in Scala file - +subsection {* Check whether generated code compiles *} + +text {* + If any of the @{text ML} ... check fails, inspect the code generated + by the previous @{text export_code} command. +*} + +export_code "*" in SML module_name Code_Test file - +ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_ML.check_SML @{theory}) *} + +export_code "*" in OCaml module_name Code_Test file - +ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_ML.check_OCaml @{theory}) *} + +export_code "*" in Haskell module_name Code_Test file - +ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_Haskell.check @{theory}) *} + +export_code "*" in Scala module_name Code_Test file - +ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_Scala.check @{theory}) *} end diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Decision_Procs/commutative_ring_tac.ML --- a/src/HOL/Decision_Procs/commutative_ring_tac.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,5 @@ -(* Author: Amine Chaieb +(* Title: HOL/Decision_Procs/commutative_ring_tac.ML + Author: Amine Chaieb Tactic for solving equalities over commutative rings. *) diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Decision_Procs/ferrante_rackoff.ML --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Tools/Qelim/ferrante_rackoff.ML +(* Title: HOL/Decision_Procs/ferrante_rackoff.ML Author: Amine Chaieb, TU Muenchen Ferrante and Rackoff's algorithm for quantifier elimination in dense diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Decision_Procs/ferrante_rackoff_data.ML --- a/src/HOL/Decision_Procs/ferrante_rackoff_data.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Decision_Procs/ferrante_rackoff_data.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Tools/Qelim/ferrante_rackoff_data.ML +(* Title: HOL/Decision_Procs/ferrante_rackoff_data.ML Author: Amine Chaieb, TU Muenchen Context data for Ferrante and Rackoff's algorithm for quantifier diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Decision_Procs/langford.ML --- a/src/HOL/Decision_Procs/langford.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Decision_Procs/langford.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Tools/Qelim/langford.ML +(* Title: HOL/Decision_Procs/langford.ML Author: Amine Chaieb, TU Muenchen *) diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Fun.thy --- a/src/HOL/Fun.thy Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Fun.thy Sat Jul 10 21:38:16 2010 +0200 @@ -95,26 +95,26 @@ subsection {* The Forward Composition Operator @{text fcomp} *} definition - fcomp :: "('a \ 'b) \ ('b \ 'c) \ 'a \ 'c" (infixl "o>" 60) + fcomp :: "('a \ 'b) \ ('b \ 'c) \ 'a \ 'c" (infixl "\>" 60) where - "f o> g = (\x. g (f x))" + "f \> g = (\x. g (f x))" -lemma fcomp_apply: "(f o> g) x = g (f x)" +lemma fcomp_apply [simp]: "(f \> g) x = g (f x)" by (simp add: fcomp_def) -lemma fcomp_assoc: "(f o> g) o> h = f o> (g o> h)" +lemma fcomp_assoc: "(f \> g) \> h = f \> (g \> h)" by (simp add: fcomp_def) -lemma id_fcomp [simp]: "id o> g = g" +lemma id_fcomp [simp]: "id \> g = g" by (simp add: fcomp_def) -lemma fcomp_id [simp]: "f o> id = f" +lemma fcomp_id [simp]: "f \> id = f" by (simp add: fcomp_def) code_const fcomp (Eval infixl 1 "#>") -no_notation fcomp (infixl "o>" 60) +no_notation fcomp (infixl "\>" 60) subsection {* Injectivity and Surjectivity *} diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/IMP/Expr.thy --- a/src/HOL/IMP/Expr.thy Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/IMP/Expr.thy Sat Jul 10 21:38:16 2010 +0200 @@ -85,46 +85,18 @@ | "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))" | "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))" -lemma [simp]: "(N(n),s) -a-> n' = (n = n')" - by (rule,cases set: evala) auto - -lemma [simp]: "(X(x),sigma) -a-> i = (i = sigma x)" - by (rule,cases set: evala) auto - -lemma [simp]: - "(Op1 f e,sigma) -a-> i = (\n. i = f n \ (e,sigma) -a-> n)" - by (rule,cases set: evala) auto - -lemma [simp]: - "(Op2 f a1 a2,sigma) -a-> i = - (\n0 n1. i = f n0 n1 \ (a1, sigma) -a-> n0 \ (a2, sigma) -a-> n1)" - by (rule,cases set: evala) auto - -lemma [simp]: "((true,sigma) -b-> w) = (w=True)" - by (rule,cases set: evalb) auto - -lemma [simp]: - "((false,sigma) -b-> w) = (w=False)" - by (rule,cases set: evalb) auto - -lemma [simp]: - "((ROp f a0 a1,sigma) -b-> w) = - (? m. (a0,sigma) -a-> m & (? n. (a1,sigma) -a-> n & w = f m n))" - by (rule,cases set: evalb) blast+ - -lemma [simp]: - "((noti(b),sigma) -b-> w) = (? x. (b,sigma) -b-> x & w = (~x))" - by (rule,cases set: evalb) blast+ - -lemma [simp]: - "((b0 andi b1,sigma) -b-> w) = - (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x&y)))" - by (rule,cases set: evalb) blast+ - -lemma [simp]: - "((b0 ori b1,sigma) -b-> w) = - (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x|y)))" - by (rule,cases set: evalb) blast+ +inductive_simps + evala_simps [simp]: + "(N(n),s) -a-> n'" + "(X(x),sigma) -a-> i" + "(Op1 f e,sigma) -a-> i" + "(Op2 f a1 a2,sigma) -a-> i" + "((true,sigma) -b-> w)" + "((false,sigma) -b-> w)" + "((ROp f a0 a1,sigma) -b-> w)" + "((noti(b),sigma) -b-> w)" + "((b0 andi b1,sigma) -b-> w)" + "((b0 ori b1,sigma) -b-> w)" lemma aexp_iff: "((a,s) -a-> n) = (A a s = n)" diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/IMP/Natural.thy --- a/src/HOL/IMP/Natural.thy Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/IMP/Natural.thy Sat Jul 10 21:38:16 2010 +0200 @@ -79,17 +79,10 @@ text {* The next proofs are all trivial by rule inversion. *} -lemma skip: - "\\,s\ \\<^sub>c s' = (s' = s)" - by auto - -lemma assign: - "\x :== a,s\ \\<^sub>c s' = (s' = s[x\a s])" - by auto - -lemma semi: - "\c0; c1, s\ \\<^sub>c s' = (\s''. \c0,s\ \\<^sub>c s'' \ \c1,s''\ \\<^sub>c s')" - by auto +inductive_simps + skip: "\\,s\ \\<^sub>c s'" + and assign: "\x :== a,s\ \\<^sub>c s'" + and semi: "\c0; c1, s\ \\<^sub>c s'" lemma ifTrue: "b s \ \\ b \ c0 \ c1, s\ \\<^sub>c s' = \c0,s\ \\<^sub>c s'" diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Imperative_HOL/Array.thy --- a/src/HOL/Imperative_HOL/Array.thy Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Imperative_HOL/Array.thy Sat Jul 10 21:38:16 2010 +0200 @@ -8,41 +8,82 @@ imports Heap_Monad begin -subsection {* Primitive layer *} +subsection {* Primitives *} -definition +definition (*FIXME present :: "heap \ 'a\heap array \ bool" where*) array_present :: "'a\heap array \ heap \ bool" where "array_present a h \ addr_of_array a < lim h" -definition +definition (*FIXME get :: "heap \ 'a\heap array \ 'a list" where*) get_array :: "'a\heap array \ heap \ 'a list" where "get_array a h = map from_nat (arrays h (TYPEREP('a)) (addr_of_array a))" -definition +definition (*FIXME set*) set_array :: "'a\heap array \ 'a list \ heap \ heap" where "set_array a x = arrays_update (\h. h(TYPEREP('a) := ((h(TYPEREP('a))) (addr_of_array a:=map to_nat x))))" -definition array :: "'a list \ heap \ 'a\heap array \ heap" where +definition (*FIXME alloc*) + array :: "'a list \ heap \ 'a\heap array \ heap" where "array xs h = (let l = lim h; r = Array l; h'' = set_array r xs (h\lim := l + 1\) in (r, h''))" -definition length :: "'a\heap array \ heap \ nat" where +definition (*FIXME length :: "heap \ 'a\heap array \ nat" where*) + length :: "'a\heap array \ heap \ nat" where "length a h = List.length (get_array a h)" -definition change :: "'a\heap array \ nat \ 'a \ heap \ heap" where +definition (*FIXME update*) + change :: "'a\heap array \ nat \ 'a \ heap \ heap" where "change a i x h = set_array a ((get_array a h)[i:=x]) h" -text {* Properties of imperative arrays *} +definition (*FIXME noteq*) + noteq_arrs :: "'a\heap array \ 'b\heap array \ bool" (infix "=!!=" 70) where + "r =!!= s \ TYPEREP('a) \ TYPEREP('b) \ addr_of_array r \ addr_of_array s" + + +subsection {* Monad operations *} + +definition new :: "nat \ 'a\heap \ 'a array Heap" where + [code del]: "new n x = Heap_Monad.heap (array (replicate n x))" + +definition of_list :: "'a\heap list \ 'a array Heap" where + [code del]: "of_list xs = Heap_Monad.heap (array xs)" + +definition make :: "nat \ (nat \ 'a\heap) \ 'a array Heap" where + [code del]: "make n f = Heap_Monad.heap (array (map f [0 ..< n]))" + +definition len :: "'a\heap array \ nat Heap" where + [code del]: "len a = Heap_Monad.tap (\h. length a h)" + +definition nth :: "'a\heap array \ nat \ 'a Heap" where + [code del]: "nth a i = Heap_Monad.guard (\h. i < length a h) + (\h. (get_array a h ! i, h))" + +definition upd :: "nat \ 'a \ 'a\heap array \ 'a\heap array Heap" where + [code del]: "upd i x a = Heap_Monad.guard (\h. i < length a h) + (\h. (a, change a i x h))" + +definition map_entry :: "nat \ ('a\heap \ 'a) \ 'a array \ 'a array Heap" where + [code del]: "map_entry i f a = Heap_Monad.guard (\h. i < length a h) + (\h. (a, change a i (f (get_array a h ! i)) h))" + +definition swap :: "nat \ 'a \ 'a\heap array \ 'a Heap" where + [code del]: "swap i x a = Heap_Monad.guard (\h. i < length a h) + (\h. (get_array a h ! i, change a i x h))" + +definition freeze :: "'a\heap array \ 'a list Heap" where + [code del]: "freeze a = Heap_Monad.tap (\h. get_array a h)" + + +subsection {* Properties *} text {* FIXME: Does there exist a "canonical" array axiomatisation in the literature? *} -definition noteq_arrs :: "('a\heap) array \ ('b\heap) array \ bool" (infix "=!!=" 70) where - "r =!!= s \ TYPEREP('a) \ TYPEREP('b) \ addr_of_array r \ addr_of_array s" +text {* Primitives *} lemma noteq_arrs_sym: "a =!!= b \ b =!!= a" and unequal_arrs [simp]: "a \ a' \ a =!!= a'" @@ -115,96 +156,103 @@ by (simp add: change_def array_present_def set_array_def get_array_def) +text {* Monad operations *} -subsection {* Primitives *} +lemma execute_new [simp, execute_simps]: + "execute (new n x) h = Some (array (replicate n x) h)" + by (simp add: new_def) -definition - new :: "nat \ 'a\heap \ 'a array Heap" where - [code del]: "new n x = Heap_Monad.heap (Array.array (replicate n x))" +lemma success_newI [iff, success_intros]: + "success (new n x) h" + by (simp add: new_def) + +lemma execute_of_list [simp, execute_simps]: + "execute (of_list xs) h = Some (array xs h)" + by (simp add: of_list_def) + +lemma success_of_listI [iff, success_intros]: + "success (of_list xs) h" + by (simp add: of_list_def) -definition - of_list :: "'a\heap list \ 'a array Heap" where - [code del]: "of_list xs = Heap_Monad.heap (Array.array xs)" +lemma execute_make [simp, execute_simps]: + "execute (make n f) h = Some (array (map f [0 ..< n]) h)" + by (simp add: make_def) + +lemma success_makeI [iff, success_intros]: + "success (make n f) h" + by (simp add: make_def) -definition - len :: "'a\heap array \ nat Heap" where - [code del]: "len arr = Heap_Monad.heap (\h. (Array.length arr h, h))" +lemma execute_len [simp, execute_simps]: + "execute (len a) h = Some (length a h, h)" + by (simp add: len_def) + +lemma success_lenI [iff, success_intros]: + "success (len a) h" + by (simp add: len_def) + +lemma execute_nth [execute_simps]: + "i < length a h \ + execute (nth a i) h = Some (get_array a h ! i, h)" + "i \ length a h \ execute (nth a i) h = None" + by (simp_all add: nth_def execute_simps) -definition - nth :: "'a\heap array \ nat \ 'a Heap" -where - [code del]: "nth a i = (do len \ len a; - (if i < len - then Heap_Monad.heap (\h. (get_array a h ! i, h)) - else raise ''array lookup: index out of range'') - done)" +lemma success_nthI [success_intros]: + "i < length a h \ success (nth a i) h" + by (auto intro: success_intros simp add: nth_def) + +lemma execute_upd [execute_simps]: + "i < length a h \ + execute (upd i x a) h = Some (a, change a i x h)" + "i \ length a h \ execute (nth a i) h = None" + by (simp_all add: upd_def execute_simps) + +lemma success_updI [success_intros]: + "i < length a h \ success (upd i x a) h" + by (auto intro: success_intros simp add: upd_def) + +lemma execute_map_entry [execute_simps]: + "i < length a h \ + execute (map_entry i f a) h = + Some (a, change a i (f (get_array a h ! i)) h)" + "i \ length a h \ execute (nth a i) h = None" + by (simp_all add: map_entry_def execute_simps) -definition - upd :: "nat \ 'a \ 'a\heap array \ 'a\heap array Heap" -where - [code del]: "upd i x a = (do len \ len a; - (if i < len - then Heap_Monad.heap (\h. (a, change a i x h)) - else raise ''array update: index out of range'') - done)" +lemma success_map_entryI [success_intros]: + "i < length a h \ success (map_entry i f a) h" + by (auto intro: success_intros simp add: map_entry_def) + +lemma execute_swap [execute_simps]: + "i < length a h \ + execute (swap i x a) h = + Some (get_array a h ! i, change a i x h)" + "i \ length a h \ execute (nth a i) h = None" + by (simp_all add: swap_def execute_simps) + +lemma success_swapI [success_intros]: + "i < length a h \ success (swap i x a) h" + by (auto intro: success_intros simp add: swap_def) + +lemma execute_freeze [simp, execute_simps]: + "execute (freeze a) h = Some (get_array a h, h)" + by (simp add: freeze_def) + +lemma success_freezeI [iff, success_intros]: + "success (freeze a) h" + by (simp add: freeze_def) lemma upd_return: "upd i x a \ return a = upd i x a" - by (rule Heap_eqI) (simp add: upd_def bindM_def split: option.split) - - -subsection {* Derivates *} - -definition - map_entry :: "nat \ ('a\heap \ 'a) \ 'a array \ 'a array Heap" -where - "map_entry i f a = (do - x \ nth a i; - upd i (f x) a - done)" + by (rule Heap_eqI) (simp add: bind_def guard_def upd_def) -definition - swap :: "nat \ 'a \ 'a\heap array \ 'a Heap" -where - "swap i x a = (do - y \ nth a i; - upd i x a; - return y - done)" - -definition - make :: "nat \ (nat \ 'a\heap) \ 'a array Heap" -where - "make n f = of_list (map f [0 ..< n])" +lemma array_make: + "new n x = make n (\_. x)" + by (rule Heap_eqI) (simp add: map_replicate_trivial) -definition - freeze :: "'a\heap array \ 'a list Heap" -where - "freeze a = (do - n \ len a; - mapM (nth a) [0..n. xs ! n)" + by (rule Heap_eqI) (simp add: map_nth) -definition - map :: "('a\heap \ 'a) \ 'a array \ 'a array Heap" -where - "map f a = (do - n \ len a; - mapM (\n. map_entry n f a) [0.._. x)" - by (rule Heap_eqI) (simp add: make_def new_def map_replicate_trivial of_list_def) - -lemma array_of_list_make [code]: - "of_list xs = make (List.length xs) (\n. xs ! n)" - by (rule Heap_eqI) (simp add: make_def map_nth) +hide_const (open) new map subsection {* Code generator setup *} @@ -213,48 +261,95 @@ definition new' where [code del]: "new' = Array.new o Code_Numeral.nat_of" -hide_const (open) new' + lemma [code]: - "Array.new = Array.new' o Code_Numeral.of_nat" + "Array.new = new' o Code_Numeral.of_nat" by (simp add: new'_def o_def) definition of_list' where [code del]: "of_list' i xs = Array.of_list (take (Code_Numeral.nat_of i) xs)" -hide_const (open) of_list' + lemma [code]: - "Array.of_list xs = Array.of_list' (Code_Numeral.of_nat (List.length xs)) xs" + "Array.of_list xs = of_list' (Code_Numeral.of_nat (List.length xs)) xs" by (simp add: of_list'_def) definition make' where [code del]: "make' i f = Array.make (Code_Numeral.nat_of i) (f o Code_Numeral.of_nat)" -hide_const (open) make' + lemma [code]: - "Array.make n f = Array.make' (Code_Numeral.of_nat n) (f o Code_Numeral.nat_of)" + "Array.make n f = make' (Code_Numeral.of_nat n) (f o Code_Numeral.nat_of)" by (simp add: make'_def o_def) definition len' where [code del]: "len' a = Array.len a \= (\n. return (Code_Numeral.of_nat n))" -hide_const (open) len' + lemma [code]: - "Array.len a = Array.len' a \= (\i. return (Code_Numeral.nat_of i))" + "Array.len a = len' a \= (\i. return (Code_Numeral.nat_of i))" by (simp add: len'_def) definition nth' where [code del]: "nth' a = Array.nth a o Code_Numeral.nat_of" -hide_const (open) nth' + lemma [code]: - "Array.nth a n = Array.nth' a (Code_Numeral.of_nat n)" + "Array.nth a n = nth' a (Code_Numeral.of_nat n)" by (simp add: nth'_def) definition upd' where [code del]: "upd' a i x = Array.upd (Code_Numeral.nat_of i) x a \ return ()" -hide_const (open) upd' + lemma [code]: - "Array.upd i x a = Array.upd' a (Code_Numeral.of_nat i) x \ return a" + "Array.upd i x a = upd' a (Code_Numeral.of_nat i) x \ return a" by (simp add: upd'_def upd_return) +lemma [code]: + "map_entry i f a = (do + x \ nth a i; + upd i (f x) a + done)" + by (rule Heap_eqI) (simp add: bind_def guard_def map_entry_def execute_simps) -subsubsection {* SML *} +lemma [code]: + "swap i x a = (do + y \ nth a i; + upd i x a; + return y + done)" + by (rule Heap_eqI) (simp add: bind_def guard_def swap_def execute_simps) + +lemma [code]: + "freeze a = (do + n \ len a; + Heap_Monad.fold_map (\i. nth a i) [0..x. fst (the (if x < length a h + then Some (get_array a h ! x, h) else None))) + [0.. len a; + Heap_Monad.fold_map (Array.nth a) [0.. len a; + Heap_Monad.fold_map (Array.nth a) [0.. heap \ ('a \ heap) option" where [code del]: "execute (Heap f) = f" +lemma Heap_cases [case_names succeed fail]: + fixes f and h + assumes succeed: "\x h'. execute f h = Some (x, h') \ P" + assumes fail: "execute f h = None \ P" + shows P + using assms by (cases "execute f h") auto + lemma Heap_execute [simp]: "Heap (execute f) = f" by (cases f) simp_all @@ -26,70 +33,143 @@ "(\h. execute f h = execute g h) \ f = g" by (cases f, cases g) (auto simp: expand_fun_eq) -lemma Heap_eqI': - "(\h. (\x. execute (f x) h) = (\y. execute (g y) h)) \ f = g" - by (auto simp: expand_fun_eq intro: Heap_eqI) +ML {* structure Execute_Simps = Named_Thms( + val name = "execute_simps" + val description = "simplification rules for execute" +) *} + +setup Execute_Simps.setup + +lemma execute_Let [simp, execute_simps]: + "execute (let x = t in f x) = (let x = t in execute (f x))" + by (simp add: Let_def) + + +subsubsection {* Specialised lifters *} + +definition tap :: "(heap \ 'a) \ 'a Heap" where + [code del]: "tap f = Heap (\h. Some (f h, h))" + +lemma execute_tap [simp, execute_simps]: + "execute (tap f) h = Some (f h, h)" + by (simp add: tap_def) definition heap :: "(heap \ 'a \ heap) \ 'a Heap" where [code del]: "heap f = Heap (Some \ f)" -lemma execute_heap [simp]: +lemma execute_heap [simp, execute_simps]: "execute (heap f) = Some \ f" by (simp add: heap_def) -lemma heap_cases [case_names succeed fail]: - fixes f and h - assumes succeed: "\x h'. execute f h = Some (x, h') \ P" - assumes fail: "execute f h = None \ P" - shows P - using assms by (cases "execute f h") auto +definition guard :: "(heap \ bool) \ (heap \ 'a \ heap) \ 'a Heap" where + [code del]: "guard P f = Heap (\h. if P h then Some (f h) else None)" + +lemma execute_guard [execute_simps]: + "\ P h \ execute (guard P f) h = None" + "P h \ execute (guard P f) h = Some (f h)" + by (simp_all add: guard_def) + + +subsubsection {* Predicate classifying successful computations *} + +definition success :: "'a Heap \ heap \ bool" where + "success f h \ execute f h \ None" + +lemma successI: + "execute f h \ None \ success f h" + by (simp add: success_def) + +lemma successE: + assumes "success f h" + obtains r h' where "execute f h = Some (r, h')" + using assms by (auto simp add: success_def) + +ML {* structure Success_Intros = Named_Thms( + val name = "success_intros" + val description = "introduction rules for success" +) *} + +setup Success_Intros.setup + +lemma success_tapI [iff, success_intros]: + "success (tap f) h" + by (rule successI) simp + +lemma success_heapI [iff, success_intros]: + "success (heap f) h" + by (rule successI) simp + +lemma success_guardI [success_intros]: + "P h \ success (guard P f) h" + by (rule successI) (simp add: execute_guard) + +lemma success_LetI [success_intros]: + "x = t \ success (f x) h \ success (let x = t in f x) h" + by (simp add: Let_def) + + +subsubsection {* Monad combinators *} definition return :: "'a \ 'a Heap" where [code del]: "return x = heap (Pair x)" -lemma execute_return [simp]: +lemma execute_return [simp, execute_simps]: "execute (return x) = Some \ Pair x" by (simp add: return_def) +lemma success_returnI [iff, success_intros]: + "success (return x) h" + by (rule successI) simp + definition raise :: "string \ 'a Heap" where -- {* the string is just decoration *} [code del]: "raise s = Heap (\_. None)" -lemma execute_raise [simp]: +lemma execute_raise [simp, execute_simps]: "execute (raise s) = (\_. None)" by (simp add: raise_def) -definition bindM :: "'a Heap \ ('a \ 'b Heap) \ 'b Heap" (infixl ">>=" 54) where +definition bind :: "'a Heap \ ('a \ 'b Heap) \ 'b Heap" (infixl ">>=" 54) where [code del]: "f >>= g = Heap (\h. case execute f h of Some (x, h') \ execute (g x) h' | None \ None)" -notation bindM (infixl "\=" 54) +notation bind (infixl "\=" 54) -lemma execute_bind [simp]: +lemma execute_bind [execute_simps]: "execute f h = Some (x, h') \ execute (f \= g) h = execute (g x) h'" "execute f h = None \ execute (f \= g) h = None" - by (simp_all add: bindM_def) + by (simp_all add: bind_def) + +lemma success_bindI [success_intros]: + "success f h \ success (g (fst (the (execute f h)))) (snd (the (execute f h))) \ success (f \= g) h" + by (auto intro!: successI elim!: successE simp add: bind_def) -lemma execute_bind_heap [simp]: - "execute (heap f \= g) h = execute (g (fst (f h))) (snd (f h))" - by (simp add: bindM_def split_def) +lemma execute_bind_successI [execute_simps]: + "success f h \ execute (f \= g) h = execute (g (fst (the (execute f h)))) (snd (the (execute f h)))" + by (cases f h rule: Heap_cases) (auto elim!: successE simp add: bind_def) +lemma execute_eq_SomeI: + assumes "Heap_Monad.execute f h = Some (x, h')" + and "Heap_Monad.execute (g x) h' = Some (y, h'')" + shows "Heap_Monad.execute (f \= g) h = Some (y, h'')" + using assms by (simp add: bind_def) + lemma return_bind [simp]: "return x \= f = f x" - by (rule Heap_eqI) simp + by (rule Heap_eqI) (simp add: execute_bind) lemma bind_return [simp]: "f \= return = f" - by (rule Heap_eqI) (simp add: bindM_def split: option.splits) + by (rule Heap_eqI) (simp add: bind_def split: option.splits) lemma bind_bind [simp]: "(f \= g) \= k = f \= (\x. g x \= k)" - by (rule Heap_eqI) (simp add: bindM_def split: option.splits) + by (rule Heap_eqI) (simp add: bind_def split: option.splits) lemma raise_bind [simp]: "raise e \= f = raise e" - by (rule Heap_eqI) simp + by (rule Heap_eqI) (simp add: execute_bind) -abbreviation chainM :: "'a Heap \ 'b Heap \ 'b Heap" (infixl ">>" 54) where +abbreviation chain :: "'a Heap \ 'b Heap \ 'b Heap" (infixl ">>" 54) where "f >> g \ f >>= (\_. g)" -notation chainM (infixl "\" 54) +notation chain (infixl "\" 54) subsubsection {* do-syntax *} @@ -105,9 +185,9 @@ syntax "_do" :: "do_expr \ 'a" ("(do (_)//done)" [12] 100) - "_bindM" :: "pttrn \ 'a \ do_expr \ do_expr" + "_bind" :: "pttrn \ 'a \ do_expr \ do_expr" ("_ <- _;//_" [1000, 13, 12] 12) - "_chainM" :: "'a \ do_expr \ do_expr" + "_chain" :: "'a \ do_expr \ do_expr" ("_;//_" [13, 12] 12) "_let" :: "pttrn \ 'a \ do_expr \ do_expr" ("let _ = _;//_" [1000, 13, 12] 12) @@ -115,13 +195,13 @@ ("_" [12] 12) syntax (xsymbols) - "_bindM" :: "pttrn \ 'a \ do_expr \ do_expr" + "_bind" :: "pttrn \ 'a \ do_expr \ do_expr" ("_ \ _;//_" [1000, 13, 12] 12) translations "_do f" => "f" - "_bindM x f g" => "f \= (\x. g)" - "_chainM f g" => "f \ g" + "_bind x f g" => "f \= (\x. g)" + "_chain f g" => "f \ g" "_let x t f" => "CONST Let t (\x. f)" "_nil f" => "f" @@ -135,19 +215,19 @@ let val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0); in (Free (v, dummyT), t) end; - fun unfold_monad (Const (@{const_syntax bindM}, _) $ f $ g) = + fun unfold_monad (Const (@{const_syntax bind}, _) $ f $ g) = let val (v, g') = dest_abs_eta g; val vs = fold_aterms (fn Free (v, _) => insert (op =) v | _ => I) v []; val v_used = fold_aterms (fn Free (w, _) => (fn s => s orelse member (op =) vs w) | _ => I) g' false; in if v_used then - Const (@{syntax_const "_bindM"}, dummyT) $ v $ f $ unfold_monad g' + Const (@{syntax_const "_bind"}, dummyT) $ v $ f $ unfold_monad g' else - Const (@{syntax_const "_chainM"}, dummyT) $ f $ unfold_monad g' + Const (@{syntax_const "_chain"}, dummyT) $ f $ unfold_monad g' end - | unfold_monad (Const (@{const_syntax chainM}, _) $ f $ g) = - Const (@{syntax_const "_chainM"}, dummyT) $ f $ unfold_monad g + | unfold_monad (Const (@{const_syntax chain}, _) $ f $ g) = + Const (@{syntax_const "_chain"}, dummyT) $ f $ unfold_monad g | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) = let val (v, g') = dest_abs_eta g; @@ -155,56 +235,90 @@ | unfold_monad (Const (@{const_syntax Pair}, _) $ f) = Const (@{const_syntax return}, dummyT) $ f | unfold_monad f = f; - fun contains_bindM (Const (@{const_syntax bindM}, _) $ _ $ _) = true - | contains_bindM (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) = - contains_bindM t; - fun bindM_monad_tr' (f::g::ts) = list_comb + fun contains_bind (Const (@{const_syntax bind}, _) $ _ $ _) = true + | contains_bind (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) = + contains_bind t; + fun bind_monad_tr' (f::g::ts) = list_comb (Const (@{syntax_const "_do"}, dummyT) $ - unfold_monad (Const (@{const_syntax bindM}, dummyT) $ f $ g), ts); + unfold_monad (Const (@{const_syntax bind}, dummyT) $ f $ g), ts); fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) = - if contains_bindM g' then list_comb + if contains_bind g' then list_comb (Const (@{syntax_const "_do"}, dummyT) $ unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts) else raise Match; in - [(@{const_syntax bindM}, bindM_monad_tr'), + [(@{const_syntax bind}, bind_monad_tr'), (@{const_syntax Let}, Let_monad_tr')] end; *} -subsection {* Monad properties *} +subsection {* Generic combinators *} -subsection {* Generic combinators *} +subsubsection {* Assertions *} definition assert :: "('a \ bool) \ 'a \ 'a Heap" where "assert P x = (if P x then return x else raise ''assert'')" +lemma execute_assert [execute_simps]: + "P x \ execute (assert P x) h = Some (x, h)" + "\ P x \ execute (assert P x) h = None" + by (simp_all add: assert_def) + +lemma success_assertI [success_intros]: + "P x \ success (assert P x) h" + by (rule successI) (simp add: execute_assert) + lemma assert_cong [fundef_cong]: assumes "P = P'" assumes "\x. P' x \ f x = f' x" shows "(assert P x >>= f) = (assert P' x >>= f')" - using assms by (auto simp add: assert_def return_bind raise_bind) + by (rule Heap_eqI) (insert assms, simp add: assert_def) + + +subsubsection {* Plain lifting *} -definition liftM :: "('a \ 'b) \ 'a \ 'b Heap" where - "liftM f = return o f" +definition lift :: "('a \ 'b) \ 'a \ 'b Heap" where + "lift f = return o f" -lemma liftM_collapse [simp]: - "liftM f x = return (f x)" - by (simp add: liftM_def) +lemma lift_collapse [simp]: + "lift f x = return (f x)" + by (simp add: lift_def) -lemma bind_liftM: - "(f \= liftM g) = (f \= (\x. return (g x)))" - by (simp add: liftM_def comp_def) +lemma bind_lift: + "(f \= lift g) = (f \= (\x. return (g x)))" + by (simp add: lift_def comp_def) + -primrec mapM :: "('a \ 'b Heap) \ 'a list \ 'b list Heap" where - "mapM f [] = return []" -| "mapM f (x#xs) = do +subsubsection {* Iteration -- warning: this is rarely useful! *} + +primrec fold_map :: "('a \ 'b Heap) \ 'a list \ 'b list Heap" where + "fold_map f [] = return []" +| "fold_map f (x # xs) = do y \ f x; - ys \ mapM f xs; + ys \ fold_map f xs; return (y # ys) done" +lemma fold_map_append: + "fold_map f (xs @ ys) = fold_map f xs \= (\xs. fold_map f ys \= (\ys. return (xs @ ys)))" + by (induct xs) simp_all + +lemma execute_fold_map_unchanged_heap [execute_simps]: + assumes "\x. x \ set xs \ \y. execute (f x) h = Some (y, h)" + shows "execute (fold_map f xs) h = + Some (List.map (\x. fst (the (execute (f x) h))) xs, h)" +using assms proof (induct xs) + case Nil show ?case by simp +next + case (Cons x xs) + from Cons.prems obtain y + where y: "execute (f x) h = Some (y, h)" by auto + moreover from Cons.prems Cons.hyps have "execute (fold_map f xs) h = + Some (map (\x. fst (the (execute (f x) h))) xs, h)" by auto + ultimately show ?case by (simp, simp only: execute_bind(1), simp) +qed + subsubsection {* A monadic combinator for simple recursive functions *} @@ -276,7 +390,7 @@ g x s z done) done)" unfolding MREC_def - unfolding bindM_def return_def + unfolding bind_def return_def apply simp apply (rule ext) apply (unfold mrec_rule[of x]) @@ -371,7 +485,7 @@ code_const return (SML "!(fn/ ()/ =>/ _)") code_const Heap_Monad.raise' (SML "!(raise/ Fail/ _)") -code_type Heap (OCaml "_") +code_type Heap (OCaml "unit/ ->/ _") code_const "op \=" (OCaml "!(fun/ f'_/ ()/ ->/ f'_/ (_/ ())/ ())") code_const return (OCaml "!(fun/ ()/ ->/ _)") code_const Heap_Monad.raise' (OCaml "failwith/ _") @@ -388,7 +502,7 @@ fun is_const c = case lookup_const naming c of SOME c' => (fn c'' => c' = c'') | NONE => K false; - val is_bindM = is_const @{const_name bindM}; + val is_bind = is_const @{const_name bind}; val is_return = is_const @{const_name return}; val dummy_name = ""; val dummy_type = ITyVar dummy_name; @@ -412,13 +526,13 @@ val ((v, ty), t) = dest_abs (t2, ty2); in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end and tr_bind'' t = case unfold_app t - of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if is_bindM c + of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if is_bind c then tr_bind' [(x1, ty1), (x2, ty2)] else force t | _ => force t; fun imp_monad_bind'' ts = (SOME dummy_name, dummy_type) `|=> ICase (((IVar (SOME dummy_name), dummy_type), [(unitt, tr_bind' ts)]), dummy_case_term) - and imp_monad_bind' (const as (c, (_, tys))) ts = if is_bindM c then case (ts, tys) + and imp_monad_bind' (const as (c, (_, tys))) ts = if is_bind c then case (ts, tys) of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3 | (ts, _) => imp_monad_bind (eta_expand 2 (const, ts)) @@ -489,6 +603,6 @@ code_const return (Haskell "return") code_const Heap_Monad.raise' (Haskell "error/ _") -hide_const (open) Heap heap execute raise' +hide_const (open) Heap heap guard raise' fold_map end diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Imperative_HOL/Ref.thy --- a/src/HOL/Imperative_HOL/Ref.thy Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Imperative_HOL/Ref.thy Sat Jul 10 21:38:16 2010 +0200 @@ -14,7 +14,7 @@ and http://www.smlnj.org/doc/Conversion/top-level-comparison.html *} -subsection {* Primitive layer *} +subsection {* Primitives *} definition present :: "heap \ 'a\heap ref \ bool" where "present h r \ addr_of_ref r < lim h" @@ -35,6 +35,31 @@ definition noteq :: "'a\heap ref \ 'b\heap ref \ bool" (infix "=!=" 70) where "r =!= s \ TYPEREP('a) \ TYPEREP('b) \ addr_of_ref r \ addr_of_ref s" + +subsection {* Monad operations *} + +definition ref :: "'a\heap \ 'a ref Heap" where + [code del]: "ref v = Heap_Monad.heap (alloc v)" + +definition lookup :: "'a\heap ref \ 'a Heap" ("!_" 61) where + [code del]: "lookup r = Heap_Monad.tap (\h. get h r)" + +definition update :: "'a ref \ 'a\heap \ unit Heap" ("_ := _" 62) where + [code del]: "update r v = Heap_Monad.heap (\h. ((), set r v h))" + +definition change :: "('a\heap \ 'a) \ 'a ref \ 'a Heap" where + "change f r = (do + x \ ! r; + let y = f x; + r := y; + return y + done)" + + +subsection {* Properties *} + +text {* Primitives *} + lemma noteq_sym: "r =!= s \ s =!= r" and unequal [simp]: "r \ r' \ r =!= r'" -- "same types!" by (auto simp add: noteq_def) @@ -104,34 +129,43 @@ by (auto simp add: noteq_def present_def) -subsection {* Primitives *} +text {* Monad operations *} -definition ref :: "'a\heap \ 'a ref Heap" where - [code del]: "ref v = Heap_Monad.heap (alloc v)" +lemma execute_ref [simp, execute_simps]: + "execute (ref v) h = Some (alloc v h)" + by (simp add: ref_def) -definition lookup :: "'a\heap ref \ 'a Heap" ("!_" 61) where - [code del]: "lookup r = Heap_Monad.heap (\h. (get h r, h))" +lemma success_refI [iff, success_intros]: + "success (ref v) h" + by (auto simp add: ref_def) -definition update :: "'a ref \ 'a\heap \ unit Heap" ("_ := _" 62) where - [code del]: "update r v = Heap_Monad.heap (\h. ((), set r v h))" - +lemma execute_lookup [simp, execute_simps]: + "Heap_Monad.execute (lookup r) h = Some (get h r, h)" + by (simp add: lookup_def) -subsection {* Derivates *} +lemma success_lookupI [iff, success_intros]: + "success (lookup r) h" + by (auto simp add: lookup_def) + +lemma execute_update [simp, execute_simps]: + "Heap_Monad.execute (update r v) h = Some ((), set r v h)" + by (simp add: update_def) -definition change :: "('a\heap \ 'a) \ 'a ref \ 'a Heap" where - "change f r = (do - x \ ! r; - let y = f x; - r := y; - return y - done)" +lemma success_updateI [iff, success_intros]: + "success (update r v) h" + by (auto simp add: update_def) +lemma execute_change [simp, execute_simps]: + "Heap_Monad.execute (change f r) h = Some (f (get h r), set r (f (get h r)) h)" + by (simp add: change_def bind_def Let_def) -subsection {* Properties *} +lemma success_changeI [iff, success_intros]: + "success (change f r) h" + by (auto intro!: success_intros simp add: change_def) lemma lookup_chain: "(!r \ f) = f" - by (rule Heap_eqI) (simp add: lookup_def) + by (rule Heap_eqI) (auto simp add: lookup_def execute_simps) lemma update_change [code]: "r := e = change (\_. e) r \ return ()" @@ -189,7 +223,7 @@ subsection {* Code generator setup *} -subsubsection {* SML *} +text {* SML *} code_type ref (SML "_/ Unsynchronized.ref") code_const Ref (SML "raise/ (Fail/ \"bare Ref\")") @@ -200,7 +234,7 @@ code_reserved SML ref -subsubsection {* OCaml *} +text {* OCaml *} code_type ref (OCaml "_/ ref") code_const Ref (OCaml "failwith/ \"bare Ref\")") @@ -211,7 +245,7 @@ code_reserved OCaml ref -subsubsection {* Haskell *} +text {* Haskell *} code_type ref (Haskell "Heap.STRef/ Heap.RealWorld/ _") code_const Ref (Haskell "error/ \"bare Ref\"") @@ -219,4 +253,4 @@ code_const Ref.lookup (Haskell "Heap.readSTRef") code_const Ref.update (Haskell "Heap.writeSTRef") -end \ No newline at end of file +end diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Imperative_HOL/Relational.thy --- a/src/HOL/Imperative_HOL/Relational.thy Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Imperative_HOL/Relational.thy Sat Jul 10 21:38:16 2010 +0200 @@ -23,12 +23,28 @@ text {* For all commands, we define simple elimination rules. *} (* FIXME: consumes 1 necessary ?? *) +lemma crel_tap: + assumes "crel (Heap_Monad.tap f) h h' r" + obtains "h' = h" "r = f h" + using assms by (simp add: crel_def) + +lemma crel_heap: + assumes "crel (Heap_Monad.heap f) h h' r" + obtains "h' = snd (f h)" "r = fst (f h)" + using assms by (cases "f h") (simp add: crel_def) + +lemma crel_guard: + assumes "crel (Heap_Monad.guard P f) h h' r" + obtains "h' = snd (f h)" "r = fst (f h)" "P h" + using assms by (cases "f h", cases "P h") (simp_all add: crel_def execute_simps) + + subsection {* Elimination rules for basic monadic commands *} lemma crelE[consumes 1]: assumes "crel (f >>= g) h h'' r'" obtains h' r where "crel f h h' r" "crel (g r) h' h'' r'" - using assms by (auto simp add: crel_def bindM_def split: option.split_asm) + using assms by (auto simp add: crel_def bind_def split: option.split_asm) lemma crelE'[consumes 1]: assumes "crel (f >> g) h h'' r'" @@ -62,10 +78,10 @@ using assms unfolding crel_def by auto -lemma crel_mapM: - assumes "crel (mapM f xs) h h' r" +lemma crel_fold_map: + assumes "crel (Heap_Monad.fold_map f xs) h h' r" assumes "\h h'. P f [] h h' []" - assumes "\h h1 h' x xs y ys. \ crel (f x) h h1 y; crel (mapM f xs) h1 h' ys; P f xs h1 h' ys \ \ P f (x#xs) h h' (y#ys)" + assumes "\h h1 h' x xs y ys. \ crel (f x) h h1 y; crel (Heap_Monad.fold_map f xs) h1 h' ys; P f xs h1 h' ys \ \ P f (x#xs) h h' (y#ys)" shows "P f xs h h' r" using assms(1) proof (induct xs arbitrary: h h' r) @@ -74,29 +90,17 @@ next case (Cons x xs) from Cons(2) obtain h1 y ys where crel_f: "crel (f x) h h1 y" - and crel_mapM: "crel (mapM f xs) h1 h' ys" + and crel_fold_map: "crel (Heap_Monad.fold_map f xs) h1 h' ys" and r_def: "r = y#ys" - unfolding mapM.simps + unfolding fold_map.simps by (auto elim!: crelE crel_return) - from Cons(1)[OF crel_mapM] crel_mapM crel_f assms(3) r_def + from Cons(1)[OF crel_fold_map] crel_fold_map crel_f assms(3) r_def show ?case by auto qed -lemma crel_heap: - assumes "crel (Heap_Monad.heap f) h h' r" - obtains "h' = snd (f h)" "r = fst (f h)" - using assms by (cases "f h") (simp add: crel_def) - subsection {* Elimination rules for array commands *} -lemma crel_length: - assumes "crel (len a) h h' r" - obtains "h = h'" "r = Array.length a h'" - using assms - unfolding Array.len_def - by (elim crel_heap) simp - (* Strong version of the lemma for this operation is missing *) lemma crel_new_weak: assumes "crel (Array.new n v) h h' r" @@ -104,52 +108,51 @@ using assms unfolding Array.new_def by (elim crel_heap) (auto simp: array_def Let_def split_def) -lemma crel_nth[consumes 1]: - assumes "crel (nth a i) h h' r" - obtains "r = (get_array a h) ! i" "h = h'" "i < Array.length a h" - using assms - unfolding nth_def - by (auto elim!: crelE crel_if crel_raise crel_length crel_heap) - -lemma crel_upd[consumes 1]: - assumes "crel (upd i v a) h h' r" - obtains "r = a" "h' = Array.change a i v h" - using assms - unfolding upd_def - by (elim crelE crel_if crel_return crel_raise - crel_length crel_heap) auto - (* Strong version of the lemma for this operation is missing *) lemma crel_of_list_weak: assumes "crel (Array.of_list xs) h h' r" obtains "get_array r h' = xs" - using assms - unfolding of_list_def - by (elim crel_heap) (simp add:get_array_init_array_list) - -lemma crel_map_entry: - assumes "crel (Array.map_entry i f a) h h' r" - obtains "r = a" "h' = Array.change a i (f (get_array a h ! i)) h" - using assms - unfolding Array.map_entry_def - by (elim crelE crel_upd crel_nth) auto - -lemma crel_swap: - assumes "crel (Array.swap i x a) h h' r" - obtains "r = get_array a h ! i" "h' = Array.change a i x h" - using assms - unfolding Array.swap_def - by (elim crelE crel_upd crel_nth crel_return) auto + using assms unfolding of_list_def + by (elim crel_heap) (simp add: get_array_init_array_list) (* Strong version of the lemma for this operation is missing *) lemma crel_make_weak: assumes "crel (Array.make n f) h h' r" obtains "i < n \ get_array r h' ! i = f i" - using assms - unfolding Array.make_def - by (elim crel_of_list_weak) auto + using assms unfolding Array.make_def + by (elim crel_heap) (auto simp: array_def Let_def split_def) + +lemma crel_length: + assumes "crel (len a) h h' r" + obtains "h = h'" "r = Array.length a h'" + using assms unfolding Array.len_def + by (elim crel_tap) simp + +lemma crel_nth[consumes 1]: + assumes "crel (nth a i) h h' r" + obtains "r = get_array a h ! i" "h = h'" "i < Array.length a h" + using assms unfolding nth_def + by (elim crel_guard) (clarify, simp) -lemma upt_conv_Cons': +lemma crel_upd[consumes 1]: + assumes "crel (upd i v a) h h' r" + obtains "r = a" "h' = Array.change a i v h" "i < Array.length a h" + using assms unfolding upd_def + by (elim crel_guard) simp + +lemma crel_map_entry: + assumes "crel (Array.map_entry i f a) h h' r" + obtains "r = a" "h' = Array.change a i (f (get_array a h ! i)) h" "i < Array.length a h" + using assms unfolding Array.map_entry_def + by (elim crel_guard) simp + +lemma crel_swap: + assumes "crel (Array.swap i x a) h h' r" + obtains "r = get_array a h ! i" "h' = Array.change a i x h" + using assms unfolding Array.swap_def + by (elim crel_guard) simp + +lemma upt_conv_Cons': (*FIXME move*) assumes "Suc a \ b" shows "[b - Suc a.. Array.length a h" shows "h = h' \ xs = drop (Array.length a h - n) (get_array a h)" using assms @@ -172,12 +175,12 @@ from Suc(3) have "[Array.length a h - Suc n..n. map_entry n f a) [Array.length a h - n..n. map_entry n f a) [Array.length a h - n..n. map_entry n f a) [Array.length a h - n..n. map_entry n f a) [Array.length a h - n..n. map_entry n f a) [Array.length a ?h1 - n..n. map_entry n f a) [Array.length a ?h1 - n..n. map_entry n f a) [Array.length a h - n..n. map_entry n f a) [Array.length a h - n.. Array.length a h" assumes "i \ Array.length a h - n" assumes "i < Array.length a h" @@ -234,22 +231,22 @@ from Suc(3) have "[Array.length a h - Suc n..n. map_entry n f a) [Array.length a h - n..n. map_entry n f a) [Array.length a h - n.. i \ Array.length a ?h1 - n" by arith - from crel_mapM have crel_mapM': "crel (mapM (\n. map_entry n f a) [Array.length a ?h1 - n..n. map_entry n f a) [Array.length a ?h1 - n..n. map_entry n f a) [Array.length a h - n..n. map_entry n f a) [Array.length a h - n.. Array.length a h" shows "Array.length a h' = Array.length a h" using assms @@ -262,36 +259,25 @@ from Suc(3) have "[Array.length a h - Suc n..n. map_entry n f a) [Array.length a h - n..n. map_entry n f a) [Array.length a h - n..n. map_entry n f a) [Array.length a ?h1 - n..n. map_entry n f a) [Array.length a ?h1 - n..n. map_entry n f a) [0..n. map_entry n f a) [0..n. map_entry n f a) [Array.length a h - Array.length a h..n. map_entry n f a) [Array.length a h - Array.length a h..h h' r. crel f h h' r \ P r) \ f \= assert P = f" -unfolding crel_def bindM_def Let_def assert_def +unfolding crel_def bind_def Let_def assert_def raise_def return_def prod_case_beta apply (cases f) apply simp @@ -378,7 +361,7 @@ lemma crelI: assumes "crel f h h' r" "crel (g r) h' h'' r'" shows "crel (f >>= g) h h'' r'" - using assms by (simp add: crel_def' bindM_def) + using assms by (simp add: crel_def' bind_def) lemma crelI': assumes "crel f h h' r" "crel g h' h'' r'" @@ -407,16 +390,26 @@ using assms by (auto split: option.split) +lemma crel_tapI: + assumes "h' = h" "r = f h" + shows "crel (Heap_Monad.tap f) h h' r" + using assms by (simp add: crel_def) + lemma crel_heapI: shows "crel (Heap_Monad.heap f) h (snd (f h)) (fst (f h))" by (simp add: crel_def apfst_def split_def prod_fun_def) -lemma crel_heapI': +lemma crel_heapI': (*FIXME keep only this version*) assumes "h' = snd (f h)" "r = fst (f h)" shows "crel (Heap_Monad.heap f) h h' r" using assms by (simp add: crel_def split_def apfst_def prod_fun_def) +lemma crel_guardI: + assumes "P h" "h' = snd (f h)" "r = fst (f h)" + shows "crel (Heap_Monad.guard P f) h h' r" + using assms by (simp add: crel_def execute_simps) + lemma crelI2: assumes "\h' rs'. crel f h h' rs' \ (\h'' rs. crel (g rs') h' h'' rs)" shows "\h'' rs. crel (f\= g) h h'' rs" @@ -432,25 +425,19 @@ lemma crel_lengthI: shows "crel (Array.len a) h h (Array.length a h)" - unfolding len_def - by (rule crel_heapI') auto + unfolding len_def by (rule crel_tapI) simp_all (* thm crel_newI for Array.new is missing *) lemma crel_nthI: assumes "i < Array.length a h" shows "crel (nth a i) h h ((get_array a h) ! i)" - using assms - unfolding nth_def - by (auto intro!: crelI crel_ifI crel_raiseI crel_lengthI crel_heapI') + using assms unfolding nth_def by (auto intro: crel_guardI) lemma crel_updI: assumes "i < Array.length a h" shows "crel (upd i v a) h (Array.change a i v h) a" - using assms - unfolding upd_def - by (auto intro!: crelI crel_ifI crel_returnI crel_raiseI - crel_lengthI crel_heapI') + using assms unfolding upd_def by (auto intro: crel_guardI) (* thm crel_of_listI is missing *) @@ -468,7 +455,7 @@ lemma crel_lookupI: shows "crel (!r) h h (Ref.get h r)" - unfolding lookup_def by (auto intro!: crel_heapI') + unfolding lookup_def by (auto intro!: crel_tapI) lemma crel_updateI: shows "crel (r := v) h (Ref.set r v h) ()" @@ -476,7 +463,7 @@ lemma crel_changeI: shows "crel (Ref.change f r) h (Ref.set r (f (Ref.get h r)) h) (f (Ref.get h r))" -unfolding change_def Let_def by (auto intro!: crelI crel_returnI crel_lookupI crel_updateI) + unfolding change_def Let_def by (auto intro!: crelI crel_returnI crel_lookupI crel_updateI) subsubsection {* Introduction rules for the assert command *} @@ -506,196 +493,31 @@ next qed (auto simp add: assms(2)[unfolded crel_def]) -section {* Definition of the noError predicate *} -text {* We add a simple definitional setting for crel intro rules - where we only would like to show that the computation does not result in a exception for heap h, - but we do not care about statements about the resulting heap and return value.*} - -definition noError :: "'a Heap \ heap \ bool" -where - "noError c h \ (\r h'. Some (r, h') = Heap_Monad.execute c h)" - -lemma noError_def': -- FIXME - "noError c h \ (\r h'. Heap_Monad.execute c h = Some (r, h'))" - unfolding noError_def apply auto proof - - fix r h' - assume "Some (r, h') = Heap_Monad.execute c h" - then have "Heap_Monad.execute c h = Some (r, h')" .. - then show "\r h'. Heap_Monad.execute c h = Some (r, h')" by blast -qed - -subsection {* Introduction rules for basic monadic commands *} - -lemma noErrorI: - assumes "noError f h" - assumes "\h' r. crel f h h' r \ noError (g r) h'" - shows "noError (f \= g) h" - using assms - by (auto simp add: noError_def' crel_def' bindM_def) - -lemma noErrorI': - assumes "noError f h" - assumes "\h' r. crel f h h' r \ noError g h'" - shows "noError (f \ g) h" - using assms - by (auto simp add: noError_def' crel_def' bindM_def) - -lemma noErrorI2: -"\crel f h h' r ; noError f h; noError (g r) h'\ -\ noError (f \= g) h" -by (auto simp add: noError_def' crel_def' bindM_def) - -lemma noError_return: - shows "noError (return x) h" - unfolding noError_def return_def - by auto - -lemma noError_if: - assumes "c \ noError t h" "\ c \ noError e h" - shows "noError (if c then t else e) h" - using assms - unfolding noError_def - by auto - -lemma noError_option_case: - assumes "\y. x = Some y \ noError (s y) h" - assumes "noError n h" - shows "noError (case x of None \ n | Some y \ s y) h" -using assms -by (auto split: option.split) - -lemma noError_mapM: -assumes "\x \ set xs. noError (f x) h \ crel (f x) h h (r x)" -shows "noError (mapM f xs) h" -using assms -proof (induct xs) - case Nil - thus ?case - unfolding mapM.simps by (intro noError_return) -next - case (Cons x xs) - thus ?case - unfolding mapM.simps - by (auto intro: noErrorI2[of "f x"] noErrorI noError_return) -qed - -lemma noError_heap: - shows "noError (Heap_Monad.heap f) h" - by (simp add: noError_def' apfst_def prod_fun_def split_def) - -subsection {* Introduction rules for array commands *} - -lemma noError_length: - shows "noError (Array.len a) h" - unfolding len_def - by (intro noError_heap) - -lemma noError_new: - shows "noError (Array.new n v) h" -unfolding Array.new_def by (intro noError_heap) - -lemma noError_upd: - assumes "i < Array.length a h" - shows "noError (Array.upd i v a) h" - using assms - unfolding upd_def - by (auto intro!: noErrorI noError_if noError_return noError_length noError_heap) (auto elim: crel_length) - -lemma noError_nth: -assumes "i < Array.length a h" - shows "noError (Array.nth a i) h" - using assms - unfolding nth_def - by (auto intro!: noErrorI noError_if noError_return noError_length noError_heap) (auto elim: crel_length) - -lemma noError_of_list: - shows "noError (of_list ls) h" - unfolding of_list_def by (rule noError_heap) - -lemma noError_map_entry: - assumes "i < Array.length a h" - shows "noError (map_entry i f a) h" - using assms - unfolding map_entry_def - by (auto elim: crel_nth intro!: noErrorI noError_nth noError_upd) - -lemma noError_swap: - assumes "i < Array.length a h" - shows "noError (swap i x a) h" - using assms - unfolding swap_def - by (auto elim: crel_nth intro!: noErrorI noError_return noError_nth noError_upd) - -lemma noError_make: - shows "noError (make n f) h" - unfolding make_def - by (auto intro: noError_of_list) - -(*TODO: move to HeapMonad *) -lemma mapM_append: - "mapM f (xs @ ys) = mapM f xs \= (\xs. mapM f ys \= (\ys. return (xs @ ys)))" - by (induct xs) simp_all - -lemma noError_freeze: - shows "noError (freeze a) h" -unfolding freeze_def -by (auto intro!: noErrorI noError_length noError_mapM[of _ _ _ "\x. get_array a h ! x"] - noError_nth crel_nthI elim: crel_length) - -lemma noError_mapM_map_entry: +lemma success_fold_map_map_entry: assumes "n \ Array.length a h" - shows "noError (mapM (\n. map_entry n f a) [Array.length a h - n..n. map_entry n f a) [Array.length a h - n.. success t h" "\ c \ success e h" + shows "success (if c then t else e) h" + using assms + unfolding success_def + by auto + +lemma success_bindI' [success_intros]: (*FIXME move*) + assumes "success f h" + assumes "\h' r. crel f h h' r \ success (g r) h'" + shows "success (f \= g) h" + using assms by (auto intro!: successI elim!: successE simp add: bind_def crel_def success_def) blast + +lemma success_partitionI: assumes "l < r" "l < Array.length a h" "r < Array.length a h" - shows "noError (partition a l r) h" -using assms -unfolding partition.simps swap_def -apply (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd noError_part1 elim!: crelE crel_upd crel_nth crel_return) + shows "success (partition a l r) h" +using assms unfolding partition.simps swap_def +apply (auto intro!: success_bindI' success_ifI success_returnI success_nthI success_updI success_part1I elim!: crelE crel_upd crel_nth crel_return simp add:) apply (frule part_length_remains) apply (frule part_returns_index_in_bounds) apply auto @@ -602,15 +614,15 @@ apply auto done -lemma noError_quicksort: +lemma success_quicksortI: assumes "l < Array.length a h" "r < Array.length a h" - shows "noError (quicksort a l r) h" + shows "success (quicksort a l r) h" using assms proof (induct a l r arbitrary: h rule: quicksort.induct) case (1 a l ri h) thus ?case unfolding quicksort.simps [of a l ri] - apply (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd noError_assert noError_partition) + apply (auto intro!: success_ifI success_bindI' success_returnI success_nthI success_updI success_assertI success_partitionI) apply (frule partition_returns_index_in_bounds) apply auto apply (frule partition_returns_index_in_bounds) @@ -620,7 +632,7 @@ apply (erule disjE) apply auto unfolding quicksort.simps [of a "Suc ri" ri] - apply (auto intro!: noError_if noError_return) + apply (auto intro!: success_ifI success_returnI) done qed @@ -637,7 +649,7 @@ ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *} -export_code qsort in SML_imp module_name QSort +export_code qsort in SML_imp module_name QSort file - export_code qsort in OCaml module_name QSort file - export_code qsort in OCaml_imp module_name QSort file - export_code qsort in Haskell module_name QSort file - diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Imperative_HOL/ex/Linked_Lists.thy --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Sat Jul 10 21:38:16 2010 +0200 @@ -999,4 +999,9 @@ ML {* @{code test_2} () *} ML {* @{code test_3} () *} +export_code test_1 test_2 test_3 in SML_imp module_name QSort file - +export_code test_1 test_2 test_3 in OCaml module_name QSort file - +export_code test_1 test_2 test_3 in OCaml_imp module_name QSort file - +export_code test_1 test_2 test_3 in Haskell module_name QSort file - + end diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/IsaMakefile Sat Jul 10 21:38:16 2010 +0200 @@ -31,7 +31,6 @@ HOL-Auth \ HOL-Bali \ HOL-Boogie-Examples \ - HOL-Codegenerator_Test \ HOL-Decision_Procs \ HOL-Hahn_Banach \ HOL-Hoare \ @@ -44,6 +43,7 @@ HOL-Induct \ HOL-Isar_Examples \ HOL-Lattice \ + HOL-Library-Codegenerator_Test \ HOL-Matrix \ HOL-Metis_Examples \ HOL-MicroJava \ @@ -531,7 +531,7 @@ HOL-Generate-HOLLight: HOL $(LOG)/HOL-Generate-HOLLight.gz -$(LOG)/HOL-Generate-HOLLight.gz: $(OUT)/HOL \ +$(LOG)/HOL-Generate-HOLLight.gz: $(OUT)/HOL \ $(IMPORTER_HOLLIGHT_FILES) Import/Generate-HOLLight/GenHOLLight.thy \ Import/Generate-HOLLight/ROOT.ML @cd Import; $(ISABELLE_TOOL) usedir $(OUT)/HOL Generate-HOLLight @@ -552,7 +552,7 @@ seq.imp state_transformer.imp sum.imp topology.imp transc.imp word32.imp \ word_base.imp word_bitop.imp word_num.imp -$(LOG)/HOL4.gz: $(OUT)/HOL $(IMPORTER_FILES) \ +$(LOG)/HOL4.gz: $(OUT)/HOL $(IMPORTER_FILES) \ $(HOL_IMPORT_FILES:%=Import/HOL/%) Import/HOL/HOL4Base.thy \ Import/HOL/HOL4Prob.thy Import/HOL/HOL4Real.thy \ Import/HOL/HOL4Vec.thy Import/HOL/HOL4Word32.thy Import/HOL/HOL4.thy \ @@ -561,7 +561,7 @@ HOLLight: HOL $(LOG)/HOLLight.gz -$(LOG)/HOLLight.gz: $(OUT)/HOL $(IMPORTER_HOLLIGHT_FILES) \ +$(LOG)/HOLLight.gz: $(OUT)/HOL $(IMPORTER_HOLLIGHT_FILES) \ Import/HOLLight/hollight.imp Import/HOLLight/HOLLight.thy \ Import/HOLLight/ROOT.ML @cd Import/HOLLight; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOLLight @@ -634,12 +634,13 @@ @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hoare_Parallel -## HOL-Codegenerator_Test +## HOL-Library-Codegenerator_Test + +HOL-Library-Codegenerator_Test: HOL-Library $(LOG)/HOL-Library-Codegenerator_Test.gz -HOL-Codegenerator_Test: HOL-Library $(LOG)/HOL-Codegenerator_Test.gz - -$(LOG)/HOL-Codegenerator_Test.gz: $(OUT)/HOL-Library \ - Codegenerator_Test/ROOT.ML Codegenerator_Test/Candidates.thy \ +$(LOG)/HOL-Library-Codegenerator_Test.gz: $(OUT)/HOL-Library \ + Codegenerator_Test/ROOT.ML \ + Codegenerator_Test/Candidates.thy \ Codegenerator_Test/Candidates_Pretty.thy \ Codegenerator_Test/Generate.thy \ Codegenerator_Test/Generate_Pretty.thy @@ -650,10 +651,10 @@ HOL-Metis_Examples: HOL $(LOG)/HOL-Metis_Examples.gz -$(LOG)/HOL-Metis_Examples.gz: $(OUT)/HOL Metis_Examples/ROOT.ML \ - Metis_Examples/Abstraction.thy Metis_Examples/BigO.thy \ - Metis_Examples/BT.thy Metis_Examples/Message.thy \ - Metis_Examples/Tarski.thy Metis_Examples/TransClosure.thy \ +$(LOG)/HOL-Metis_Examples.gz: $(OUT)/HOL Metis_Examples/ROOT.ML \ + Metis_Examples/Abstraction.thy Metis_Examples/BigO.thy \ + Metis_Examples/BT.thy Metis_Examples/Message.thy \ + Metis_Examples/Tarski.thy Metis_Examples/TransClosure.thy \ Metis_Examples/set.thy @$(ISABELLE_TOOL) usedir $(OUT)/HOL Metis_Examples @@ -778,8 +779,8 @@ HOL-Unix: HOL $(LOG)/HOL-Unix.gz -$(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/Nested_Environment.thy \ - Library/List_Prefix.thy Unix/ROOT.ML Unix/Unix.thy \ +$(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/Nested_Environment.thy \ + Library/List_Prefix.thy Unix/ROOT.ML Unix/Unix.thy \ Unix/document/root.bib Unix/document/root.tex @$(ISABELLE_TOOL) usedir $(OUT)/HOL Unix @@ -797,10 +798,10 @@ HOL-Modelcheck: HOL $(LOG)/HOL-Modelcheck.gz -$(LOG)/HOL-Modelcheck.gz: $(OUT)/HOL Modelcheck/CTL.thy \ - Modelcheck/EindhovenExample.thy Modelcheck/EindhovenSyn.thy \ - Modelcheck/MuCalculus.thy Modelcheck/MuckeExample1.thy \ - Modelcheck/MuckeExample2.thy Modelcheck/MuckeSyn.thy \ +$(LOG)/HOL-Modelcheck.gz: $(OUT)/HOL Modelcheck/CTL.thy \ + Modelcheck/EindhovenExample.thy Modelcheck/EindhovenSyn.thy \ + Modelcheck/MuCalculus.thy Modelcheck/MuckeExample1.thy \ + Modelcheck/MuckeExample2.thy Modelcheck/MuckeSyn.thy \ Modelcheck/ROOT.ML Modelcheck/mucke_oracle.ML @$(ISABELLE_TOOL) usedir $(OUT)/HOL Modelcheck @@ -859,7 +860,7 @@ HOL-Docs: HOL $(LOG)/HOL-Docs.gz -$(LOG)/HOL-Docs.gz: $(OUT)/HOL Docs/Main_Doc.thy Docs/ROOT.ML \ +$(LOG)/HOL-Docs.gz: $(OUT)/HOL Docs/Main_Doc.thy Docs/ROOT.ML \ Docs/document/root.tex @$(ISABELLE_TOOL) usedir -D generated $(OUT)/HOL Docs @@ -1005,7 +1006,8 @@ ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \ ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Sudoku.thy \ ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy ex/Tree23.thy \ - ex/Unification.thy ex/document/root.bib ex/document/root.tex \ + ex/Unification.thy ex/While_Combinator_Example.thy ex/document/root.bib \ + ex/document/root.tex \ ex/set.thy ex/svc_funcs.ML ex/svc_test.thy @$(ISABELLE_TOOL) usedir $(OUT)/HOL ex @@ -1124,8 +1126,8 @@ Multivariate_Analysis/Real_Integration.thy \ Multivariate_Analysis/Topology_Euclidean_Space.thy \ Multivariate_Analysis/document/root.tex \ - Multivariate_Analysis/normarith.ML Library/Glbs.thy \ - Library/Inner_Product.thy Library/Numeral_Type.thy \ + Multivariate_Analysis/normarith.ML Library/Glbs.thy \ + Library/Inner_Product.thy Library/Numeral_Type.thy \ Library/Convex.thy Library/FrechetDeriv.thy \ Library/Product_Vector.thy Library/Product_plus.thy @cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Multivariate_Analysis @@ -1135,15 +1137,15 @@ HOL-Probability: HOL $(OUT)/HOL-Probability -$(OUT)/HOL-Probability: $(OUT)/HOL Probability/ROOT.ML \ - Probability/Probability.thy Probability/Sigma_Algebra.thy \ - Probability/SeriesPlus.thy Probability/Caratheodory.thy \ - Probability/Borel.thy Probability/Measure.thy \ - Probability/Lebesgue.thy Probability/Product_Measure.thy \ - Probability/Probability_Space.thy Probability/Information.thy \ - Probability/ex/Dining_Cryptographers.thy Library/FuncSet.thy \ - Library/Convex.thy Library/Product_Vector.thy \ - Library/Product_plus.thy Library/Inner_Product.thy \ +$(OUT)/HOL-Probability: $(OUT)/HOL Probability/ROOT.ML \ + Probability/Probability.thy Probability/Sigma_Algebra.thy \ + Probability/SeriesPlus.thy Probability/Caratheodory.thy \ + Probability/Borel.thy Probability/Measure.thy \ + Probability/Lebesgue.thy Probability/Product_Measure.thy \ + Probability/Probability_Space.thy Probability/Information.thy \ + Probability/ex/Dining_Cryptographers.thy Library/FuncSet.thy \ + Library/Convex.thy Library/Product_Vector.thy \ + Library/Product_plus.thy Library/Inner_Product.thy \ Library/Nat_Bijection.thy @cd Probability; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Probability @@ -1252,7 +1254,7 @@ HOL-NSA-Examples: HOL-NSA $(LOG)/HOL-NSA-Examples.gz -$(LOG)/HOL-NSA-Examples.gz: $(OUT)/HOL-NSA NSA/Examples/ROOT.ML \ +$(LOG)/HOL-NSA-Examples.gz: $(OUT)/HOL-NSA NSA/Examples/ROOT.ML \ NSA/Examples/NSPrimes.thy @cd NSA; $(ISABELLE_TOOL) usedir $(OUT)/HOL-NSA Examples @@ -1320,7 +1322,7 @@ HOL-Quotient_Examples: HOL $(LOG)/HOL-Quotient_Examples.gz $(LOG)/HOL-Quotient_Examples.gz: $(OUT)/HOL \ - Quotient_Examples/FSet.thy Quotient_Examples/Quotient_Int.thy \ + Quotient_Examples/FSet.thy Quotient_Examples/Quotient_Int.thy \ Quotient_Examples/Quotient_Message.thy @$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Library/FrechetDeriv.thy --- a/src/HOL/Library/FrechetDeriv.thy Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Library/FrechetDeriv.thy Sat Jul 10 21:38:16 2010 +0200 @@ -139,6 +139,47 @@ \ FDERIV (\x. f x - g x) x :> (\h. F h - G h)" by (simp only: diff_minus FDERIV_add FDERIV_minus) +subsection {* Uniqueness *} + +lemma FDERIV_zero_unique: + assumes "FDERIV (\x. 0) x :> F" shows "F = (\h. 0)" +proof - + interpret F: bounded_linear F + using assms by (rule FDERIV_bounded_linear) + let ?r = "\h. norm (F h) / norm h" + have *: "?r -- 0 --> 0" + using assms unfolding fderiv_def by simp + show "F = (\h. 0)" + proof + fix h show "F h = 0" + proof (rule ccontr) + assume "F h \ 0" + moreover from this have h: "h \ 0" + by (clarsimp simp add: F.zero) + ultimately have "0 < ?r h" + by (simp add: divide_pos_pos) + from LIM_D [OF * this] obtain s where s: "0 < s" + and r: "\x. x \ 0 \ norm x < s \ ?r x < ?r h" by auto + from dense [OF s] obtain t where t: "0 < t \ t < s" .. + let ?x = "scaleR (t / norm h) h" + have "?x \ 0" and "norm ?x < s" using t h by simp_all + hence "?r ?x < ?r h" by (rule r) + thus "False" using t h by (simp add: F.scaleR) + qed + qed +qed + +lemma FDERIV_unique: + assumes "FDERIV f x :> F" and "FDERIV f x :> F'" shows "F = F'" +proof - + have "FDERIV (\x. 0) x :> (\h. F h - F' h)" + using FDERIV_diff [OF assms] by simp + hence "(\h. F h - F' h) = (\h. 0)" + by (rule FDERIV_zero_unique) + thus "F = F'" + unfolding expand_fun_eq right_minus_eq . +qed + subsection {* Continuity *} lemma FDERIV_isCont: @@ -470,7 +511,7 @@ also have "\ = norm (?inv (x + h) - ?inv x) * norm (?inv x)" by simp finally show "norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h - \ norm (?inv (x + h) - ?inv x) * norm (?inv x)" . + \ norm (?inv (x + h) - ?inv x) * norm (?inv x)" . qed qed qed diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Library/Fset.thy --- a/src/HOL/Library/Fset.thy Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Library/Fset.thy Sat Jul 10 21:38:16 2010 +0200 @@ -69,21 +69,21 @@ \ 'a fset \ (unit \ Code_Evaluation.term)" where [code_unfold]: "setify xs = Code_Evaluation.valtermify Set {\} xs" -notation fcomp (infixl "o>" 60) -notation scomp (infixl "o\" 60) +notation fcomp (infixl "\>" 60) +notation scomp (infixl "\\" 60) instantiation fset :: (random) random begin definition - "Quickcheck.random i = Quickcheck.random i o\ (\xs. Pair (setify xs))" + "Quickcheck.random i = Quickcheck.random i \\ (\xs. Pair (setify xs))" instance .. end -no_notation fcomp (infixl "o>" 60) -no_notation scomp (infixl "o\" 60) +no_notation fcomp (infixl "\>" 60) +no_notation scomp (infixl "\\" 60) subsection {* Lattice instantiation *} diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Library/Multiset.thy Sat Jul 10 21:38:16 2010 +0200 @@ -954,21 +954,21 @@ \ 'a multiset \ (unit \ Code_Evaluation.term)" where [code_unfold]: "bagify xs = Code_Evaluation.valtermify Bag {\} xs" -notation fcomp (infixl "o>" 60) -notation scomp (infixl "o\" 60) +notation fcomp (infixl "\>" 60) +notation scomp (infixl "\\" 60) instantiation multiset :: (random) random begin definition - "Quickcheck.random i = Quickcheck.random i o\ (\xs. Pair (bagify xs))" + "Quickcheck.random i = Quickcheck.random i \\ (\xs. Pair (bagify xs))" instance .. end -no_notation fcomp (infixl "o>" 60) -no_notation scomp (infixl "o\" 60) +no_notation fcomp (infixl "\>" 60) +no_notation scomp (infixl "\\" 60) hide_const (open) bagify diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Library/State_Monad.thy --- a/src/HOL/Library/State_Monad.thy Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Library/State_Monad.thy Sat Jul 10 21:38:16 2010 +0200 @@ -55,23 +55,23 @@ we use a set of monad combinators: *} -notation fcomp (infixl "o>" 60) -notation (xsymbols) fcomp (infixl "o>" 60) +notation fcomp (infixl "\>" 60) +notation (xsymbols) fcomp (infixl "\>" 60) notation scomp (infixl "o->" 60) -notation (xsymbols) scomp (infixl "o\" 60) +notation (xsymbols) scomp (infixl "\\" 60) abbreviation (input) "return \ Pair" text {* Given two transformations @{term f} and @{term g}, they - may be directly composed using the @{term "op o>"} combinator, - forming a forward composition: @{prop "(f o> g) s = f (g s)"}. + may be directly composed using the @{term "op \>"} combinator, + forming a forward composition: @{prop "(f \> g) s = f (g s)"}. After any yielding transformation, we bind the side result immediately using a lambda abstraction. This - is the purpose of the @{term "op o\"} combinator: - @{prop "(f o\ (\x. g)) s = (let (x, s') = f s in g s')"}. + is the purpose of the @{term "op \\"} combinator: + @{prop "(f \\ (\x. g)) s = (let (x, s') = f s in g s')"}. For queries, the existing @{term "Let"} is appropriate. @@ -141,8 +141,8 @@ translations "_do f" => "f" - "_scomp x f g" => "f o\ (\x. g)" - "_fcomp f g" => "f o> g" + "_scomp x f g" => "f \\ (\x. g)" + "_fcomp f g" => "f \> g" "_let x t f" => "CONST Let t (\x. f)" "_done f" => "f" diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML --- a/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: positivstellensatz_tools.ML +(* Title: HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML Author: Philipp Meyer, TU Muenchen Functions for generating a certificate from a positivstellensatz and vice versa diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Library/While_Combinator.thy --- a/src/HOL/Library/While_Combinator.thy Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Library/While_Combinator.thy Sat Jul 10 21:38:16 2010 +0200 @@ -1,5 +1,6 @@ (* Title: HOL/Library/While_Combinator.thy Author: Tobias Nipkow + Author: Alexander Krauss Copyright 2000 TU Muenchen *) @@ -9,27 +10,90 @@ imports Main begin -text {* - We define the while combinator as the "mother of all tail recursive functions". -*} +subsection {* Partial version *} + +definition while_option :: "('a \ bool) \ ('a \ 'a) \ 'a \ 'a option" where +"while_option b c s = (if (\k. ~ b ((c ^^ k) s)) + then Some ((c ^^ (LEAST k. ~ b ((c ^^ k) s))) s) + else None)" -function (tailrec) while :: "('a \ bool) \ ('a \ 'a) \ 'a \ 'a" -where - while_unfold[simp del]: "while b c s = (if b s then while b c (c s) else s)" -by auto +theorem while_option_unfold[code]: +"while_option b c s = (if b s then while_option b c (c s) else Some s)" +proof cases + assume "b s" + show ?thesis + proof (cases "\k. ~ b ((c ^^ k) s)") + case True + then obtain k where 1: "~ b ((c ^^ k) s)" .. + with `b s` obtain l where "k = Suc l" by (cases k) auto + with 1 have "~ b ((c ^^ l) (c s))" by (auto simp: funpow_swap1) + then have 2: "\l. ~ b ((c ^^ l) (c s))" .. + from 1 + have "(LEAST k. ~ b ((c ^^ k) s)) = Suc (LEAST l. ~ b ((c ^^ Suc l) s))" + by (rule Least_Suc) (simp add: `b s`) + also have "... = Suc (LEAST l. ~ b ((c ^^ l) (c s)))" + by (simp add: funpow_swap1) + finally + show ?thesis + using True 2 `b s` by (simp add: funpow_swap1 while_option_def) + next + case False + then have "~ (\l. ~ b ((c ^^ Suc l) s))" by blast + then have "~ (\l. ~ b ((c ^^ l) (c s)))" + by (simp add: funpow_swap1) + with False `b s` show ?thesis by (simp add: while_option_def) + qed +next + assume [simp]: "~ b s" + have least: "(LEAST k. ~ b ((c ^^ k) s)) = 0" + by (rule Least_equality) auto + moreover + have "\k. ~ b ((c ^^ k) s)" by (rule exI[of _ "0::nat"]) auto + ultimately show ?thesis unfolding while_option_def by auto +qed -declare while_unfold[code] +lemma while_option_stop: +assumes "while_option b c s = Some t" +shows "~ b t" +proof - + from assms have ex: "\k. ~ b ((c ^^ k) s)" + and t: "t = (c ^^ (LEAST k. ~ b ((c ^^ k) s))) s" + by (auto simp: while_option_def split: if_splits) + from LeastI_ex[OF ex] + show "~ b t" unfolding t . +qed + +theorem while_option_rule: +assumes step: "!!s. P s ==> b s ==> P (c s)" +and result: "while_option b c s = Some t" +and init: "P s" +shows "P t" +proof - + def k == "LEAST k. ~ b ((c ^^ k) s)" + from assms have t: "t = (c ^^ k) s" + by (simp add: while_option_def k_def split: if_splits) + have 1: "ALL i bool) \ ('a \ 'a) \ 'a \ 'a" +where "while b c s = the (while_option b c s)" + +lemma while_unfold: + "while b c s = (if b s then while b c (c s) else s)" +unfolding while_def by (subst while_option_unfold) simp lemma def_while_unfold: assumes fdef: "f == while test do" shows "f x = (if test x then f(do x) else x)" -proof - - have "f x = while test do x" using fdef by simp - also have "\ = (if test x then while test do (do x) else x)" - by(rule while_unfold) - also have "\ = (if test x then f(do x) else x)" by(simp add:fdef[symmetric]) - finally show ?thesis . -qed +unfolding fdef by (fact while_unfold) text {* @@ -63,56 +127,5 @@ apply blast done -text {* - \medskip An application: computation of the @{term lfp} on finite - sets via iteration. -*} - -theorem lfp_conv_while: - "[| mono f; finite U; f U = U |] ==> - lfp f = fst (while (\(A, fA). A \ fA) (\(A, fA). (fA, f fA)) ({}, f {}))" -apply (rule_tac P = "\(A, B). (A \ U \ B = f A \ A \ B \ B \ lfp f)" and - r = "((Pow U \ UNIV) \ (Pow U \ UNIV)) \ - inv_image finite_psubset (op - U o fst)" in while_rule) - apply (subst lfp_unfold) - apply assumption - apply (simp add: monoD) - apply (subst lfp_unfold) - apply assumption - apply clarsimp - apply (blast dest: monoD) - apply (fastsimp intro!: lfp_lowerbound) - apply (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset]) -apply (clarsimp simp add: finite_psubset_def order_less_le) -apply (blast intro!: finite_Diff dest: monoD) -done - - -text {* - An example of using the @{term while} combinator. -*} - -text{* Cannot use @{thm[source]set_eq_subset} because it leads to -looping because the antisymmetry simproc turns the subset relationship -back into equality. *} - -theorem "P (lfp (\N::int set. {0} \ {(n + 2) mod 6 | n. n \ N})) = - P {0, 4, 2}" -proof - - have seteq: "!!A B. (A = B) = ((!a : A. a:B) & (!b:B. b:A))" - by blast - have aux: "!!f A B. {f n | n. A n \ B n} = {f n | n. A n} \ {f n | n. B n}" - apply blast - done - show ?thesis - apply (subst lfp_conv_while [where ?U = "{0, 1, 2, 3, 4, 5}"]) - apply (rule monoI) - apply blast - apply simp - apply (simp add: aux set_eq_subset) - txt {* The fixpoint computation is performed purely by rewriting: *} - apply (simp add: while_unfold aux seteq del: subset_empty) - done -qed end diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Library/reify_data.ML --- a/src/HOL/Library/reify_data.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Library/reify_data.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Library/reflection_data.ML +(* Title: HOL/Library/reify_data.ML Author: Amine Chaieb, TU Muenchen Data for the reification and reflection methods. diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sat Jul 10 21:38:16 2010 +0200 @@ -1940,10 +1940,15 @@ subsection {* Convexity of general and special intervals. *} +lemma convexI: (* TODO: move to Library/Convex.thy *) + assumes "\x y u v. \x \ s; y \ s; 0 \ u; 0 \ v; u + v = 1\ \ u *\<^sub>R x + v *\<^sub>R y \ s" + shows "convex s" +using assms unfolding convex_def by fast + lemma is_interval_convex: - fixes s :: "('a::ordered_euclidean_space) set" + fixes s :: "('a::euclidean_space) set" assumes "is_interval s" shows "convex s" - unfolding convex_def apply(rule,rule,rule,rule,rule,rule,rule) proof- +proof (rule convexI) fix x y u v assume as:"x \ s" "y \ s" "0 \ u" "0 \ v" "u + v = (1::real)" hence *:"u = 1 - v" "1 - v \ 0" and **:"v = 1 - u" "1 - u \ 0" by auto { fix a b assume "\ b \ u * a + v * b" @@ -1959,7 +1964,7 @@ using as(3-) DIM_positive[where 'a='a] by(auto simp add:euclidean_simps) qed lemma is_interval_connected: - fixes s :: "('a::ordered_euclidean_space) set" + fixes s :: "('a::euclidean_space) set" shows "is_interval s \ connected s" using is_interval_convex convex_connected by auto diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Sat Jul 10 21:38:16 2010 +0200 @@ -39,7 +39,24 @@ unfolding dist_norm diff_0_right norm_scaleR unfolding dist_norm netlimit_at[of x] by(auto simp add:algebra_simps *) qed -lemma FDERIV_conv_has_derivative:"FDERIV f (x::'a::{real_normed_vector,perfect_space}) :> f' = (f has_derivative f') (at x)" (is "?l = ?r") proof +lemma netlimit_at_vector: + fixes a :: "'a::real_normed_vector" + shows "netlimit (at a) = a" +proof (cases "\x. x \ a") + case True then obtain x where x: "x \ a" .. + have "\ trivial_limit (at a)" + unfolding trivial_limit_def eventually_at dist_norm + apply clarsimp + apply (rule_tac x="a + scaleR (d / 2) (sgn (x - a))" in exI) + apply (simp add: norm_sgn sgn_zero_iff x) + done + thus ?thesis + by (rule netlimit_within [of a UNIV, unfolded within_UNIV]) +qed simp + +lemma FDERIV_conv_has_derivative: + shows "FDERIV f x :> f' = (f has_derivative f') (at x)" (is "?l = ?r") +proof assume ?l note as = this[unfolded fderiv_def] show ?r unfolding has_derivative_def Lim_at apply-apply(rule,rule as[THEN conjunct1]) proof(rule,rule) fix e::real assume "e>0" @@ -47,14 +64,14 @@ thus "\d>0. \xa. 0 < dist xa x \ dist xa x < d \ dist ((1 / norm (xa - netlimit (at x))) *\<^sub>R (f xa - (f (netlimit (at x)) + f' (xa - netlimit (at x))))) (0) < e" apply(rule_tac x=d in exI) apply(erule conjE,rule,assumption) apply rule apply(erule_tac x="xa - x" in allE) - unfolding dist_norm netlimit_at[of x] by (auto simp add: diff_diff_eq) qed next + unfolding dist_norm netlimit_at_vector[of x] by (auto simp add: diff_diff_eq) qed next assume ?r note as = this[unfolded has_derivative_def] show ?l unfolding fderiv_def LIM_def apply-apply(rule,rule as[THEN conjunct1]) proof(rule,rule) fix e::real assume "e>0" guess d using as[THEN conjunct2,unfolded Lim_at,rule_format,OF`e>0`] .. thus "\s>0. \xa. xa \ 0 \ dist xa 0 < s \ dist (norm (f (x + xa) - f x - f' xa) / norm xa) 0 < e" apply- apply(rule_tac x=d in exI) apply(erule conjE,rule,assumption) apply rule apply(erule_tac x="xa + x" in allE) - unfolding dist_norm netlimit_at[of x] by (auto simp add: diff_diff_eq add.commute) qed qed + unfolding dist_norm netlimit_at_vector[of x] by (auto simp add: diff_diff_eq add.commute) qed qed subsection {* These are the only cases we'll care about, probably. *} @@ -86,7 +103,7 @@ lemma has_derivative_within_open: "a \ s \ open s \ ((f has_derivative f') (at a within s) \ (f has_derivative f') (at a))" - unfolding has_derivative_within has_derivative_at using Lim_within_open by auto + by (simp only: at_within_interior interior_open) lemma bounded_linear_imp_linear: "bounded_linear f \ linear f" (* TODO: move elsewhere *) proof - @@ -272,7 +289,7 @@ lemma differentiable_within_open: assumes "a \ s" "open s" shows "f differentiable (at a within s) \ (f differentiable (at a))" - unfolding differentiable_def has_derivative_within_open[OF assms] by auto + using assms by (simp only: at_within_interior interior_open) lemma differentiable_on_eq_differentiable_at: "open s \ (f differentiable_on s \ (\x\s. f differentiable at x))" unfolding differentiable_on_def by(auto simp add: differentiable_within_open) @@ -477,10 +494,12 @@ \ (g o f) differentiable (at x within s)" unfolding differentiable_def by(meson diff_chain_within) -subsection {* Uniqueness of derivative. *) -(* *) -(* The general result is a bit messy because we need approachability of the *) -(* limit point from any direction. But OK for nontrivial intervals etc. *} +subsection {* Uniqueness of derivative *} + +text {* + The general result is a bit messy because we need approachability of the + limit point from any direction. But OK for nontrivial intervals etc. +*} lemma frechet_derivative_unique_within: fixes f::"'a::euclidean_space \ 'b::real_normed_vector" assumes "(f has_derivative f') (at x within s)" "(f has_derivative f'') (at x within s)" @@ -507,10 +526,10 @@ unfolding dist_norm unfolding f'.scaleR f''.scaleR f'.add f''.add f'.diff f''.diff scaleR_scaleR scaleR_right_diff_distrib scaleR_right_distrib using i by auto qed qed -lemma frechet_derivative_unique_at: fixes f::"'a::euclidean_space \ 'b::real_normed_vector" +lemma frechet_derivative_unique_at: shows "(f has_derivative f') (at x) \ (f has_derivative f'') (at x) \ f' = f''" - apply(rule frechet_derivative_unique_within[of f f' x UNIV f'']) unfolding within_UNIV apply(assumption)+ - apply(rule,rule,rule,rule) apply(rule_tac x="e/2" in exI) by auto + unfolding FDERIV_conv_has_derivative [symmetric] + by (rule FDERIV_unique) lemma "isCont f x = continuous (at x) f" unfolding isCont_def LIM_def unfolding continuous_at Lim_at unfolding dist_nz by auto @@ -547,7 +566,7 @@ by (rule frechet_derivative_unique_at) qed -lemma frechet_derivative_at: fixes f::"'a::euclidean_space \ 'b::real_normed_vector" +lemma frechet_derivative_at: shows "(f has_derivative f') (at x) \ (f' = frechet_derivative f (at x))" apply(rule frechet_derivative_unique_at[of f],assumption) unfolding frechet_derivative_works[THEN sym] using differentiable_def by auto @@ -1241,13 +1260,16 @@ using f' unfolding scaleR[THEN sym] by auto next assume ?r thus ?l unfolding vector_derivative_def has_vector_derivative_def differentiable_def by auto qed -lemma vector_derivative_unique_at: fixes f::"real\ 'n::euclidean_space" - assumes "(f has_vector_derivative f') (at x)" "(f has_vector_derivative f'') (at x)" shows "f' = f''" proof- - have *:"(\x. x *\<^sub>R f') = (\x. x *\<^sub>R f'')" apply(rule frechet_derivative_unique_at) - using assms[unfolded has_vector_derivative_def] by auto - show ?thesis proof(rule ccontr) assume "f' \ f''" moreover - hence "(\x. x *\<^sub>R f') = (\x. x *\<^sub>R f'')" using * by auto - ultimately show False unfolding expand_fun_eq by auto qed qed +lemma vector_derivative_unique_at: + assumes "(f has_vector_derivative f') (at x)" + assumes "(f has_vector_derivative f'') (at x)" + shows "f' = f''" +proof- + have "(\x. x *\<^sub>R f') = (\x. x *\<^sub>R f'')" + using assms [unfolded has_vector_derivative_def] + by (rule frechet_derivative_unique_at) + thus ?thesis unfolding expand_fun_eq by auto +qed lemma vector_derivative_unique_within_closed_interval: fixes f::"real \ 'n::ordered_euclidean_space" assumes "a < b" "x \ {a..b}" @@ -1260,8 +1282,8 @@ hence "(\x. x *\<^sub>R f') 1 = (\x. x *\<^sub>R f'') 1" using * by (auto simp: expand_fun_eq) ultimately show False unfolding o_def by auto qed qed -lemma vector_derivative_at: fixes f::"real \ 'a::euclidean_space" shows - "(f has_vector_derivative f') (at x) \ vector_derivative f (at x) = f'" +lemma vector_derivative_at: + shows "(f has_vector_derivative f') (at x) \ vector_derivative f (at x) = f'" apply(rule vector_derivative_unique_at) defer apply assumption unfolding vector_derivative_works[THEN sym] differentiable_def unfolding has_vector_derivative_def by auto diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Multivariate_Analysis/Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Sat Jul 10 21:38:16 2010 +0200 @@ -3315,9 +3315,7 @@ apply simp done -print_antiquotations - -section "Instanciate @{typ real} and @{typ complex} as typeclass @{text ordered_euclidean_space}." +subsection "Instantiate @{typ real} and @{typ complex} as typeclass @{text ordered_euclidean_space}." instantiation real :: real_basis_with_inner begin diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sat Jul 10 21:38:16 2010 +0200 @@ -5023,7 +5023,7 @@ text {* Intervals in general, including infinite and mixtures of open and closed. *} -definition "is_interval (s::('a::ordered_euclidean_space) set) \ +definition "is_interval (s::('a::euclidean_space) set) \ (\a\s. \b\s. \x. (\i x$$i \ x$$i \ b$$i) \ (b$$i \ x$$i \ x$$i \ a$$i))) \ x \ s)" lemma is_interval_interval: "is_interval {a .. b::'a::ordered_euclidean_space}" (is ?th1) diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Multivariate_Analysis/normarith.ML --- a/src/HOL/Multivariate_Analysis/normarith.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/normarith.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: Library/normarith.ML +(* Title: HOL/Multivariate_Analysis/normarith.ML Author: Amine Chaieb, University of Cambridge Simple decision procedure for linear problems in Euclidean space. diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Mutabelle/mutabelle.ML --- a/src/HOL/Mutabelle/mutabelle.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Mutabelle/mutabelle.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,5 +1,4 @@ -(* - Title: HOL/Mutabelle/mutabelle.ML +(* Title: HOL/Mutabelle/mutabelle.ML Author: Veronika Ortner, TU Muenchen Mutation of theorems diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,5 +1,4 @@ -(* - Title: HOL/Mutabelle/mutabelle_extra.ML +(* Title: HOL/Mutabelle/mutabelle_extra.ML Author: Stefan Berghofer, Jasmin Blanchette, Lukas Bulwahn, TU Muenchen Invokation of Counterexample generators diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/NSA/transfer.ML --- a/src/HOL/NSA/transfer.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/NSA/transfer.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,6 +1,5 @@ -(* Title : HOL/Hyperreal/transfer.ML - ID : $Id$ - Author : Brian Huffman +(* Title: HOL/NSA/transfer.ML + Author: Brian Huffman Transfer principle tactic for nonstandard analysis. *) diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Product_Type.thy Sat Jul 10 21:38:16 2010 +0200 @@ -791,37 +791,37 @@ The composition-uncurry combinator. *} -notation fcomp (infixl "o>" 60) +notation fcomp (infixl "\>" 60) -definition scomp :: "('a \ 'b \ 'c) \ ('b \ 'c \ 'd) \ 'a \ 'd" (infixl "o\" 60) where - "f o\ g = (\x. split g (f x))" +definition scomp :: "('a \ 'b \ 'c) \ ('b \ 'c \ 'd) \ 'a \ 'd" (infixl "\\" 60) where + "f \\ g = (\x. prod_case g (f x))" lemma scomp_unfold: "scomp = (\f g x. g (fst (f x)) (snd (f x)))" - by (simp add: expand_fun_eq scomp_def split_def) + by (simp add: expand_fun_eq scomp_def prod_case_unfold) -lemma scomp_apply: "(f o\ g) x = split g (f x)" - by (simp add: scomp_unfold split_def) +lemma scomp_apply [simp]: "(f \\ g) x = prod_case g (f x)" + by (simp add: scomp_unfold prod_case_unfold) -lemma Pair_scomp: "Pair x o\ f = f x" +lemma Pair_scomp: "Pair x \\ f = f x" by (simp add: expand_fun_eq scomp_apply) -lemma scomp_Pair: "x o\ Pair = x" +lemma scomp_Pair: "x \\ Pair = x" by (simp add: expand_fun_eq scomp_apply) -lemma scomp_scomp: "(f o\ g) o\ h = f o\ (\x. g x o\ h)" +lemma scomp_scomp: "(f \\ g) \\ h = f \\ (\x. g x \\ h)" by (simp add: expand_fun_eq scomp_unfold) -lemma scomp_fcomp: "(f o\ g) o> h = f o\ (\x. g x o> h)" +lemma scomp_fcomp: "(f \\ g) \> h = f \\ (\x. g x \> h)" by (simp add: expand_fun_eq scomp_unfold fcomp_def) -lemma fcomp_scomp: "(f o> g) o\ h = f o> (g o\ h)" +lemma fcomp_scomp: "(f \> g) \\ h = f \> (g \\ h)" by (simp add: expand_fun_eq scomp_unfold fcomp_apply) code_const scomp (Eval infixl 3 "#->") -no_notation fcomp (infixl "o>" 60) -no_notation scomp (infixl "o\" 60) +no_notation fcomp (infixl "\>" 60) +no_notation scomp (infixl "\\" 60) text {* @{term prod_fun} --- action of the product functor upon diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Quickcheck.thy --- a/src/HOL/Quickcheck.thy Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Quickcheck.thy Sat Jul 10 21:38:16 2010 +0200 @@ -7,8 +7,8 @@ uses ("Tools/quickcheck_generators.ML") begin -notation fcomp (infixl "o>" 60) -notation scomp (infixl "o\" 60) +notation fcomp (infixl "\>" 60) +notation scomp (infixl "\\" 60) subsection {* The @{text random} class *} @@ -23,7 +23,7 @@ begin definition - "random i = Random.range 2 o\ + "random i = Random.range 2 \\ (\k. Pair (if k = 0 then Code_Evaluation.valtermify False else Code_Evaluation.valtermify True))" instance .. @@ -44,7 +44,7 @@ begin definition - "random _ = Random.select chars o\ (\c. Pair (c, \u. Code_Evaluation.term_of c))" + "random _ = Random.select chars \\ (\c. Pair (c, \u. Code_Evaluation.term_of c))" instance .. @@ -64,7 +64,7 @@ begin definition random_nat :: "code_numeral \ Random.seed \ (nat \ (unit \ Code_Evaluation.term)) \ Random.seed" where - "random_nat i = Random.range (i + 1) o\ (\k. Pair ( + "random_nat i = Random.range (i + 1) \\ (\k. Pair ( let n = Code_Numeral.nat_of k in (n, \_. Code_Evaluation.term_of n)))" @@ -76,7 +76,7 @@ begin definition - "random i = Random.range (2 * i + 1) o\ (\k. Pair ( + "random i = Random.range (2 * i + 1) \\ (\k. Pair ( let j = (if k \ i then Code_Numeral.int_of (k - i) else - Code_Numeral.int_of (i - k)) in (j, \_. Code_Evaluation.term_of j)))" @@ -110,7 +110,7 @@ text {* Towards type copies and datatypes *} definition collapse :: "('a \ ('a \ 'b \ 'a) \ 'a) \ 'a \ 'b \ 'a" where - "collapse f = (f o\ id)" + "collapse f = (f \\ id)" definition beyond :: "code_numeral \ code_numeral \ code_numeral" where "beyond k l = (if l > k then l else 0)" @@ -139,8 +139,8 @@ code_reserved Quickcheck Quickcheck_Generators -no_notation fcomp (infixl "o>" 60) -no_notation scomp (infixl "o\" 60) +no_notation fcomp (infixl "\>" 60) +no_notation scomp (infixl "\\" 60) subsection {* The Random-Predicate Monad *} diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Random.thy --- a/src/HOL/Random.thy Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Random.thy Sat Jul 10 21:38:16 2010 +0200 @@ -7,8 +7,8 @@ imports Code_Numeral List begin -notation fcomp (infixl "o>" 60) -notation scomp (infixl "o\" 60) +notation fcomp (infixl "\>" 60) +notation scomp (infixl "\\" 60) subsection {* Auxiliary functions *} @@ -48,12 +48,12 @@ subsection {* Base selectors *} fun iterate :: "code_numeral \ ('b \ 'a \ 'b \ 'a) \ 'b \ 'a \ 'b \ 'a" where - "iterate k f x = (if k = 0 then Pair x else f x o\ iterate (k - 1) f)" + "iterate k f x = (if k = 0 then Pair x else f x \\ iterate (k - 1) f)" definition range :: "code_numeral \ seed \ code_numeral \ seed" where "range k = iterate (log 2147483561 k) - (\l. next o\ (\v. Pair (v + l * 2147483561))) 1 - o\ (\v. Pair (v mod k))" + (\l. next \\ (\v. Pair (v + l * 2147483561))) 1 + \\ (\v. Pair (v mod k))" lemma range: "k > 0 \ fst (range k s) < k" @@ -61,7 +61,7 @@ definition select :: "'a list \ seed \ 'a \ seed" where "select xs = range (Code_Numeral.of_nat (length xs)) - o\ (\k. Pair (nth xs (Code_Numeral.nat_of k)))" + \\ (\k. Pair (nth xs (Code_Numeral.nat_of k)))" lemma select: assumes "xs \ []" @@ -97,7 +97,7 @@ definition select_weight :: "(code_numeral \ 'a) list \ seed \ 'a \ seed" where "select_weight xs = range (listsum (map fst xs)) - o\ (\k. Pair (pick xs k))" + \\ (\k. Pair (pick xs k))" lemma select_weight_member: assumes "0 < listsum (map fst xs)" @@ -184,8 +184,8 @@ iterate range select pick select_weight hide_fact (open) range_def -no_notation fcomp (infixl "o>" 60) -no_notation scomp (infixl "o\" 60) +no_notation fcomp (infixl "\>" 60) +no_notation scomp (infixl "\\" 60) end diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Rat.thy --- a/src/HOL/Rat.thy Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Rat.thy Sat Jul 10 21:38:16 2010 +0200 @@ -1114,14 +1114,14 @@ valterm_fract :: "int \ (unit \ Code_Evaluation.term) \ int \ (unit \ Code_Evaluation.term) \ rat \ (unit \ Code_Evaluation.term)" where [code_unfold]: "valterm_fract k l = Code_Evaluation.valtermify Fract {\} k {\} l" -notation fcomp (infixl "o>" 60) -notation scomp (infixl "o\" 60) +notation fcomp (infixl "\>" 60) +notation scomp (infixl "\\" 60) instantiation rat :: random begin definition - "Quickcheck.random i = Quickcheck.random i o\ (\num. Random.range i o\ (\denom. Pair ( + "Quickcheck.random i = Quickcheck.random i \\ (\num. Random.range i \\ (\denom. Pair ( let j = Code_Numeral.int_of (denom + 1) in valterm_fract num (j, \u. Code_Evaluation.term_of j))))" @@ -1129,8 +1129,8 @@ end -no_notation fcomp (infixl "o>" 60) -no_notation scomp (infixl "o\" 60) +no_notation fcomp (infixl "\>" 60) +no_notation scomp (infixl "\\" 60) text {* Setup for SML code generator *} diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/RealDef.thy --- a/src/HOL/RealDef.thy Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/RealDef.thy Sat Jul 10 21:38:16 2010 +0200 @@ -1743,21 +1743,21 @@ valterm_ratreal :: "rat \ (unit \ Code_Evaluation.term) \ real \ (unit \ Code_Evaluation.term)" where [code_unfold]: "valterm_ratreal k = Code_Evaluation.valtermify Ratreal {\} k" -notation fcomp (infixl "o>" 60) -notation scomp (infixl "o\" 60) +notation fcomp (infixl "\>" 60) +notation scomp (infixl "\\" 60) instantiation real :: random begin definition - "Quickcheck.random i = Quickcheck.random i o\ (\r. Pair (valterm_ratreal r))" + "Quickcheck.random i = Quickcheck.random i \\ (\r. Pair (valterm_ratreal r))" instance .. end -no_notation fcomp (infixl "o>" 60) -no_notation scomp (infixl "o\" 60) +no_notation fcomp (infixl "\>" 60) +no_notation scomp (infixl "\\" 60) text {* Setup for SML code generator *} diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/String.thy --- a/src/HOL/String.thy Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/String.thy Sat Jul 10 21:38:16 2010 +0200 @@ -219,4 +219,16 @@ hide_type (open) literal + +text {* Code generator setup *} + +code_modulename SML + String String + +code_modulename OCaml + String String + +code_modulename Haskell + String String + end \ No newline at end of file diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Tools/Function/function.ML --- a/src/HOL/Tools/Function/function.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Tools/Function/function.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Tools/Function/fundef.ML +(* Title: HOL/Tools/Function/function.ML Author: Alexander Krauss, TU Muenchen A package for general recursive function definitions. diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Tools/Function/function_lib.ML --- a/src/HOL/Tools/Function/function_lib.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Tools/Function/function_lib.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Tools/Function/fundef_lib.ML +(* Title: HOL/Tools/Function/function_lib.ML Author: Alexander Krauss, TU Muenchen A package for general recursive function definitions. diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Tools/Function/pat_completeness.ML --- a/src/HOL/Tools/Function/pat_completeness.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Tools/Function/pat_completeness.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Tools/Function/fundef_datatype.ML +(* Title: HOL/Tools/Function/pat_completeness.ML Author: Alexander Krauss, TU Muenchen Method "pat_completeness" to prove completeness of datatype patterns. diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Tools/Quotient/quotient_def.ML --- a/src/HOL/Tools/Quotient/quotient_def.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_def.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Tools/Quotient/quotient_def.thy +(* Title: HOL/Tools/Quotient/quotient_def.ML Author: Cezary Kaliszyk and Christian Urban Definitions for constants on quotient types. diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Tools/Quotient/quotient_info.ML --- a/src/HOL/Tools/Quotient/quotient_info.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_info.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Tools/Quotient/quotient_info.thy +(* Title: HOL/Tools/Quotient/quotient_info.ML Author: Cezary Kaliszyk and Christian Urban Data slots for the quotient package. diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Tools/Quotient/quotient_tacs.ML --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Tools/Quotient/quotient_tacs.thy +(* Title: HOL/Tools/Quotient/quotient_tacs.ML Author: Cezary Kaliszyk and Christian Urban Tactics for solving goal arising from lifting theorems to quotient diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Tools/Quotient/quotient_term.ML --- a/src/HOL/Tools/Quotient/quotient_term.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_term.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Tools/Quotient/quotient_term.thy +(* Title: HOL/Tools/Quotient/quotient_term.ML Author: Cezary Kaliszyk and Christian Urban Constructs terms corresponding to goals from lifting theorems to diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Tools/Quotient/quotient_typ.ML --- a/src/HOL/Tools/Quotient/quotient_typ.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Tools/Quotient/quotient_typ.thy +(* Title: HOL/Tools/Quotient/quotient_typ.ML Author: Cezary Kaliszyk and Christian Urban Definition of a quotient type. diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Tools/float_syntax.ML --- a/src/HOL/Tools/float_syntax.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Tools/float_syntax.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,5 @@ -(* Author: Tobias Nipkow, TU Muenchen +(* Title: HOL/Tools/float_syntax.ML + Author: Tobias Nipkow, TU Muenchen Concrete syntax for floats. *) diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Tools/groebner.ML --- a/src/HOL/Tools/groebner.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Tools/groebner.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Tools/Groebner_Basis/groebner.ML +(* Title: HOL/Tools/groebner.ML Author: Amine Chaieb, TU Muenchen *) diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Tools/hologic.ML --- a/src/HOL/Tools/hologic.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Tools/hologic.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/hologic.ML +(* Title: HOL/Tools/hologic.ML Author: Lawrence C Paulson and Markus Wenzel Abstract syntax operations for HOL. diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Tools/inductive.ML Sat Jul 10 21:38:16 2010 +0200 @@ -22,7 +22,7 @@ sig type inductive_result = {preds: term list, elims: thm list, raw_induct: thm, - induct: thm, inducts: thm list, intrs: thm list} + induct: thm, inducts: thm list, intrs: thm list, eqs: thm list} val morph_result: morphism -> inductive_result -> inductive_result type inductive_info = {names: string list, coind: bool} * inductive_result val the_inductive: Proof.context -> string -> inductive_info @@ -73,7 +73,7 @@ local_theory -> inductive_result * local_theory val declare_rules: binding -> bool -> bool -> string list -> term list -> thm list -> binding list -> Attrib.src list list -> (thm * string list * int) list -> - thm -> local_theory -> thm list * thm list * thm * thm list * local_theory + thm list -> thm -> local_theory -> thm list * thm list * thm list * thm * thm list * local_theory val add_ind_def: add_ind_def val gen_add_inductive_i: add_ind_def -> inductive_flags -> ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list -> @@ -120,16 +120,16 @@ type inductive_result = {preds: term list, elims: thm list, raw_induct: thm, - induct: thm, inducts: thm list, intrs: thm list}; + induct: thm, inducts: thm list, intrs: thm list, eqs: thm list}; -fun morph_result phi {preds, elims, raw_induct: thm, induct, inducts, intrs} = +fun morph_result phi {preds, elims, raw_induct: thm, induct, inducts, intrs, eqs} = let val term = Morphism.term phi; val thm = Morphism.thm phi; val fact = Morphism.fact phi; in {preds = map term preds, elims = fact elims, raw_induct = thm raw_induct, - induct = thm induct, inducts = fact inducts, intrs = fact intrs} + induct = thm induct, inducts = fact inducts, intrs = fact intrs, eqs = fact eqs} end; type inductive_info = @@ -244,6 +244,9 @@ | mk_names a 1 = [a] | mk_names a n = map (fn i => a ^ string_of_int i) (1 upto n); +fun select_disj 1 1 = [] + | select_disj _ 1 = [rtac disjI1] + | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1)); (** process rules **) @@ -347,10 +350,6 @@ (mono RS (fp_def RS (if coind then @{thm def_gfp_unfold} else @{thm def_lfp_unfold}))); - fun select_disj 1 1 = [] - | select_disj _ 1 = [rtac disjI1] - | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1)); - val rules = [refl, TrueI, notFalseI, exI, conjI]; val intrs = map_index (fn (i, intr) => @@ -361,7 +360,6 @@ (*Not ares_tac, since refl must be tried before any equality assumptions; backtracking may occur if the premises have extra variables!*) DEPTH_SOLVE_1 (resolve_tac rules 1 APPEND assume_tac 1)]) - |> rulify |> singleton (ProofContext.export ctxt ctxt')) intr_ts in (intrs, unfold) end; @@ -408,14 +406,78 @@ REPEAT (FIRSTGOAL (eresolve_tac rules2)), EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_preds_defs prem, conjI] 1)) (tl prems))]) - |> rulify |> singleton (ProofContext.export ctxt'' ctxt'''), map #2 c_intrs, length Ts) end in map prove_elim cs end; +(* prove simplification equations *) +fun prove_eqs quiet_mode cs params intr_ts intrs elims ctxt ctxt'' = + let + val _ = clean_message quiet_mode " Proving the simplification rules ..."; + + fun dest_intr r = + (the (dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))), + Logic.strip_assums_hyp r, Logic.strip_params r); + val intr_ts' = map dest_intr intr_ts; + fun prove_eq c elim = + let + val Ts = arg_types_of (length params) c; + val (anames, ctxt') = Variable.variant_fixes (mk_names "a" (length Ts)) ctxt; + val frees = map Free (anames ~~ Ts); + val c_intrs = filter (equal c o #1 o #1 o #1) (intr_ts' ~~ intrs); + fun mk_intr_conj (((_, _, us, _), ts, params'), _) = + let + fun list_ex ([], t) = t + | list_ex ((a,T)::vars, t) = + (HOLogic.exists_const T) $ (Abs(a, T, list_ex(vars,t))); + val conjs = map2 (curry HOLogic.mk_eq) frees us @ (map HOLogic.dest_Trueprop ts) + in + list_ex (params', if null conjs then @{term True} else foldr1 HOLogic.mk_conj conjs) + end; + val lhs = list_comb (c, params @ frees) + val rhs = + if null c_intrs then @{term False} else foldr1 HOLogic.mk_disj (map mk_intr_conj c_intrs) + val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) + fun prove_intr1 (i, _) = Subgoal.FOCUS_PREMS (fn {params, prems, ...} => + let + val (prems', last_prem) = split_last prems + in + EVERY1 (select_disj (length c_intrs) (i + 1)) + THEN EVERY (replicate (length params) (rtac @{thm exI} 1)) + THEN EVERY (map (fn prem => (rtac @{thm conjI} 1 THEN rtac prem 1)) prems') + THEN rtac last_prem 1 + end) ctxt' 1 + fun prove_intr2 (((_, _, us, _), ts, params'), intr) = + EVERY (replicate (length params') (etac @{thm exE} 1)) + THEN EVERY (replicate (length ts + length us - 1) (etac @{thm conjE} 1)) + THEN Subgoal.FOCUS_PREMS (fn {params, prems, ...} => + let + val (eqs, prems') = chop (length us) prems + val rew_thms = map (fn th => th RS @{thm eq_reflection}) eqs + in + rewrite_goal_tac rew_thms 1 + THEN rtac intr 1 + THEN (EVERY (map (fn p => rtac p 1) prems')) + end) ctxt' 1 + in + Skip_Proof.prove ctxt' [] [] eq (fn {...} => + rtac @{thm iffI} 1 THEN etac (#1 elim) 1 + THEN EVERY (map_index prove_intr1 c_intrs) + THEN (if null c_intrs then etac @{thm FalseE} 1 else + let val (c_intrs', last_c_intr) = split_last c_intrs in + EVERY (map (fn ci => etac @{thm disjE} 1 THEN prove_intr2 ci) c_intrs') + THEN prove_intr2 last_c_intr + end)) + |> rulify + |> singleton (ProofContext.export ctxt' ctxt'') + end; + in + map2 prove_eq cs elims + end; + (* derivation of simplified elimination rules *) local @@ -455,7 +517,6 @@ end; - (* inductive_cases *) fun gen_inductive_cases prep_att prep_prop args lthy = @@ -483,7 +544,37 @@ in Method.erule 0 rules end)) "dynamic case analysis on predicates"; +(* derivation of simplified equation *) +fun mk_simp_eq ctxt prop = + let + val (c, args) = strip_comb (HOLogic.dest_Trueprop prop) + val ctxt' = Variable.auto_fixes prop ctxt + val cname = fst (dest_Const c) + val info = the_inductive ctxt cname + val eq = nth (#eqs (snd info)) (find_index (fn c => c = cname) (#names (fst info))) + val (_, args') = strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of eq)))) + val certify = cterm_of (ProofContext.theory_of ctxt) + in + cterm_instantiate (map (pairself certify) (args' ~~ args)) eq + |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv + (Simplifier.full_rewrite (simpset_of ctxt)))) + |> singleton (Variable.export ctxt' ctxt) + end + +(* inductive simps *) + +fun gen_inductive_simps prep_att prep_prop args lthy = + let + val thy = ProofContext.theory_of lthy; + val facts = args |> map (fn ((a, atts), props) => + ((a, map (prep_att thy) atts), + map (Thm.no_attributes o single o mk_simp_eq lthy o prep_prop lthy) props)); + in lthy |> Local_Theory.notes facts |>> map snd end; + +val inductive_simps = gen_inductive_simps Attrib.intern_src Syntax.read_prop; +val inductive_simps_i = gen_inductive_simps (K I) Syntax.check_prop; + (* prove induction rule *) fun prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono @@ -697,7 +788,7 @@ end; fun declare_rules rec_binding coind no_ind cnames - preds intrs intr_bindings intr_atts elims raw_induct lthy = + preds intrs intr_bindings intr_atts elims eqs raw_induct lthy = let val rec_name = Binding.name_of rec_binding; fun rec_qualified qualified = Binding.qualify qualified rec_name; @@ -737,18 +828,23 @@ ((rec_qualified true (Binding.name (coind_prefix coind ^ "induct")), map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]); - val (inducts, lthy3) = - if no_ind orelse coind then ([], lthy2) + val (eqs', lthy3) = lthy2 |> + fold_map (fn (name, eq) => Local_Theory.note + ((Binding.qualify true (Long_Name.base_name name) (Binding.name "simps"), []), [eq]) + #> apfst (hd o snd)) + (if null eqs then [] else (cnames ~~ eqs)) + val (inducts, lthy4) = + if no_ind orelse coind then ([], lthy3) else - let val inducts = cnames ~~ Project_Rule.projects lthy2 (1 upto length cnames) induct' in - lthy2 |> + let val inducts = cnames ~~ Project_Rule.projects lthy3 (1 upto length cnames) induct' in + lthy3 |> Local_Theory.notes [((rec_qualified true (Binding.name "inducts"), []), inducts |> map (fn (name, th) => ([th], [Attrib.internal (K ind_case_names), Attrib.internal (K (Rule_Cases.consumes 1)), Attrib.internal (K (Induct.induct_pred name))])))] |>> snd o hd end; - in (intrs', elims', induct', inducts, lthy3) end; + in (intrs', elims', eqs', induct', inducts, lthy4) end; type inductive_flags = {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool, @@ -794,17 +890,23 @@ else prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def rec_preds_defs lthy2 lthy1); + val eqs = + if no_elim then [] else prove_eqs quiet_mode cs params intr_ts intrs elims lthy2 lthy1 - val (intrs', elims', induct, inducts, lthy3) = declare_rules rec_name coind no_ind - cnames preds intrs intr_names intr_atts elims raw_induct lthy1; + val elims' = map (fn (th, ns, i) => (rulify th, ns, i)) elims + val intrs' = map rulify intrs + + val (intrs'', elims'', eqs', induct, inducts, lthy3) = declare_rules rec_name coind no_ind + cnames preds intrs' intr_names intr_atts elims' eqs raw_induct lthy1; val result = {preds = preds, - intrs = intrs', - elims = elims', + intrs = intrs'', + elims = elims'', raw_induct = rulify raw_induct, induct = induct, - inducts = inducts}; + inducts = inducts, + eqs = eqs'}; val lthy4 = lthy3 |> Local_Theory.declaration false (fn phi => @@ -993,4 +1095,9 @@ "create simplified instances of elimination rules (improper)" Keyword.thy_script (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_cases)); +val _ = + Outer_Syntax.local_theory "inductive_simps" + "create simplification rules for inductive predicates" Keyword.thy_script + (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_simps)); + end; diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Tools/inductive_set.ML Sat Jul 10 21:38:16 2010 +0200 @@ -520,16 +520,17 @@ val cnames = map (Local_Theory.full_name lthy3 o #1) cnames_syn; (* FIXME *) val (intr_names, intr_atts) = split_list (map fst intros); val raw_induct' = to_set [] (Context.Proof lthy3) raw_induct; - val (intrs', elims', induct, inducts, lthy4) = + val eqs = [] (* TODO: define equations *) + val (intrs', elims', eqs', induct, inducts, lthy4) = Inductive.declare_rules rec_name coind no_ind cnames (map fst defs) (map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts (map (fn th => (to_set [] (Context.Proof lthy3) th, map fst (fst (Rule_Cases.get th)), Rule_Cases.get_constraints th)) elims) - raw_induct' lthy3; + eqs raw_induct' lthy3; in ({intrs = intrs', elims = elims', induct = induct, inducts = inducts, - raw_induct = raw_induct', preds = map fst defs}, + raw_induct = raw_induct', preds = map fst defs, eqs = eqs'}, lthy4) end; diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Tools/list_code.ML --- a/src/HOL/Tools/list_code.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Tools/list_code.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,5 @@ -(* Author: Florian Haftmann, TU Muenchen +(* Title: HOL/Tools/list_code.ML + Author: Florian Haftmann, TU Muenchen Code generation for list literals. *) diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Tools/quickcheck_generators.ML --- a/src/HOL/Tools/quickcheck_generators.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Tools/quickcheck_generators.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,5 @@ -(* Author: Florian Haftmann, TU Muenchen +(* Title: HOL/Tools/quickcheck_generators.ML + Author: Florian Haftmann, TU Muenchen Quickcheck generators for various types. *) diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Tools/semiring_normalizer.ML --- a/src/HOL/Tools/semiring_normalizer.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Tools/semiring_normalizer.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Tools/Groebner_Basis/normalizer.ML +(* Title: HOL/Tools/semiring_normalizer.ML Author: Amine Chaieb, TU Muenchen Normalization of expressions in semirings. diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Tools/simpdata.ML --- a/src/HOL/Tools/simpdata.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Tools/simpdata.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/simpdata.ML +(* Title: HOL/Tools/simpdata.ML Author: Tobias Nipkow Copyright 1991 University of Cambridge diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Tools/string_code.ML --- a/src/HOL/Tools/string_code.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Tools/string_code.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,5 @@ -(* Author: Florian Haftmann, TU Muenchen +(* Title: HOL/Tools/string_code.ML + Author: Florian Haftmann, TU Muenchen Code generation for character and string literals. *) diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Tools/transfer.ML --- a/src/HOL/Tools/transfer.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Tools/transfer.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,6 +1,7 @@ -(* Author: Amine Chaieb, University of Cambridge, 2009 - Jeremy Avigad, Carnegie Mellon University - Florian Haftmann, TU Muenchen +(* Title: HOL/Tools/transfer.ML + Author: Amine Chaieb, University of Cambridge, 2009 + Jeremy Avigad, Carnegie Mellon University + Florian Haftmann, TU Muenchen Simple transfer principle on theorems. *) diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/Word/Word.thy Sat Jul 10 21:38:16 2010 +0200 @@ -26,14 +26,14 @@ code_datatype word_of_int -notation fcomp (infixl "o>" 60) -notation scomp (infixl "o\" 60) +notation fcomp (infixl "\>" 60) +notation scomp (infixl "\\" 60) instantiation word :: ("{len0, typerep}") random begin definition - "random_word i = Random.range (max i (2 ^ len_of TYPE('a))) o\ (\k. Pair ( + "random_word i = Random.range (max i (2 ^ len_of TYPE('a))) \\ (\k. Pair ( let j = word_of_int (Code_Numeral.int_of k) :: 'a word in (j, \_::unit. Code_Evaluation.term_of j)))" @@ -41,8 +41,8 @@ end -no_notation fcomp (infixl "o>" 60) -no_notation scomp (infixl "o\" 60) +no_notation fcomp (infixl "\>" 60) +no_notation scomp (infixl "\\" 60) subsection {* Type conversions and casting *} diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOL/ex/ROOT.ML Sat Jul 10 21:38:16 2010 +0200 @@ -23,6 +23,7 @@ "InductiveInvariant_examples", "LocaleTest2", "Records", + "While_Combinator_Example", "MonoidGroup", "BinEx", "Hex_Bin_Examples", diff -r 5d2b3e827371 -r b55f848f34fc src/HOL/ex/While_Combinator_Example.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/While_Combinator_Example.thy Sat Jul 10 21:38:16 2010 +0200 @@ -0,0 +1,60 @@ +(* Title: HOL/Library/While_Combinator.thy + Author: Tobias Nipkow + Copyright 2000 TU Muenchen +*) + +header {* An application of the While combinator *} + +theory While_Combinator_Example +imports While_Combinator +begin + +text {* Computation of the @{term lfp} on finite sets via + iteration. *} + +theorem lfp_conv_while: + "[| mono f; finite U; f U = U |] ==> + lfp f = fst (while (\(A, fA). A \ fA) (\(A, fA). (fA, f fA)) ({}, f {}))" +apply (rule_tac P = "\(A, B). (A \ U \ B = f A \ A \ B \ B \ lfp f)" and + r = "((Pow U \ UNIV) \ (Pow U \ UNIV)) \ + inv_image finite_psubset (op - U o fst)" in while_rule) + apply (subst lfp_unfold) + apply assumption + apply (simp add: monoD) + apply (subst lfp_unfold) + apply assumption + apply clarsimp + apply (blast dest: monoD) + apply (fastsimp intro!: lfp_lowerbound) + apply (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset]) +apply (clarsimp simp add: finite_psubset_def order_less_le) +apply (blast intro!: finite_Diff dest: monoD) +done + + +subsection {* Example *} + +text{* Cannot use @{thm[source]set_eq_subset} because it leads to +looping because the antisymmetry simproc turns the subset relationship +back into equality. *} + +theorem "P (lfp (\N::int set. {0} \ {(n + 2) mod 6 | n. n \ N})) = + P {0, 4, 2}" +proof - + have seteq: "!!A B. (A = B) = ((!a : A. a:B) & (!b:B. b:A))" + by blast + have aux: "!!f A B. {f n | n. A n \ B n} = {f n | n. A n} \ {f n | n. B n}" + apply blast + done + show ?thesis + apply (subst lfp_conv_while [where ?U = "{0, 1, 2, 3, 4, 5}"]) + apply (rule monoI) + apply blast + apply simp + apply (simp add: aux set_eq_subset) + txt {* The fixpoint computation is performed purely by rewriting: *} + apply (simp add: while_unfold aux seteq del: subset_empty) + done +qed + +end \ No newline at end of file diff -r 5d2b3e827371 -r b55f848f34fc src/HOLCF/Tools/Domain/domain_constructors.ML --- a/src/HOLCF/Tools/Domain/domain_constructors.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: HOLCF/Tools/domain/domain_constructors.ML +(* Title: HOLCF/Tools/Domain/domain_constructors.ML Author: Brian Huffman Defines constructor functions for a given domain isomorphism diff -r 5d2b3e827371 -r b55f848f34fc src/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: HOLCF/Tools/domain/domain_isomorphism.ML +(* Title: HOLCF/Tools/Domain/domain_isomorphism.ML Author: Brian Huffman Defines new types satisfying the given domain equations. diff -r 5d2b3e827371 -r b55f848f34fc src/HOLCF/Tools/Domain/domain_take_proofs.ML --- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: HOLCF/Tools/domain/domain_take_proofs.ML +(* Title: HOLCF/Tools/Domain/domain_take_proofs.ML Author: Brian Huffman Defines take functions for the given domain equation diff -r 5d2b3e827371 -r b55f848f34fc src/Provers/order.ML --- a/src/Provers/order.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/Provers/order.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,5 @@ -(* Author: Oliver Kutter, TU Muenchen +(* Title: Provers/order.ML + Author: Oliver Kutter, TU Muenchen Transitivity reasoner for partial and linear orders. *) diff -r 5d2b3e827371 -r b55f848f34fc src/Provers/quasi.ML --- a/src/Provers/quasi.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/Provers/quasi.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,5 @@ -(* Author: Oliver Kutter, TU Muenchen +(* Title: Provers/quasi.ML + Author: Oliver Kutter, TU Muenchen Reasoner for simple transitivity and quasi orders. *) diff -r 5d2b3e827371 -r b55f848f34fc src/Provers/trancl.ML --- a/src/Provers/trancl.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/Provers/trancl.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,6 +1,7 @@ -(* - Title: Transitivity reasoner for transitive closures of relations +(* Title: Provers/trancl.ML Author: Oliver Kutter, TU Muenchen + +Transitivity reasoner for transitive closures of relations *) (* diff -r 5d2b3e827371 -r b55f848f34fc src/Pure/General/file.ML --- a/src/Pure/General/file.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/Pure/General/file.ML Sat Jul 10 21:38:16 2010 +0200 @@ -20,6 +20,7 @@ val exists: Path.T -> bool val check: Path.T -> unit val rm: Path.T -> unit + val rm_tree: Path.T -> unit val mkdir: Path.T -> unit val mkdir_leaf: Path.T -> unit val open_input: (TextIO.instream -> 'a) -> Path.T -> 'a @@ -134,6 +135,8 @@ val rm = OS.FileSys.remove o platform_path; +fun rm_tree path = system_command ("rm -r " ^ shell_path path); + fun mkdir path = system_command ("mkdir -p " ^ shell_path path); fun mkdir_leaf path = (check (Path.dir path); mkdir path); diff -r 5d2b3e827371 -r b55f848f34fc src/Tools/Code/code_eval.ML --- a/src/Tools/Code/code_eval.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/Tools/Code/code_eval.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: Tools/code/code_eval.ML +(* Title: Tools/Code/code_eval.ML Author: Florian Haftmann, TU Muenchen Runtime services building on code generation into implementation language SML. diff -r 5d2b3e827371 -r b55f848f34fc src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/Tools/Code/code_haskell.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: Tools/code/code_haskell.ML +(* Title: Tools/Code/code_haskell.ML Author: Florian Haftmann, TU Muenchen Serializer for Haskell. @@ -6,6 +6,8 @@ signature CODE_HASKELL = sig + val target: string + val check: theory -> Path.T -> unit val setup: theory -> theory end; @@ -388,7 +390,7 @@ ^ code_of_pretty content) end in - Code_Target.mk_serialization target NONE + Code_Target.mk_serialization target (fn NONE => K () o map (code_writeln o snd) | SOME file => K () o map (write_module (check_destination file))) (rpair [] o cat_lines o map (code_of_pretty o snd)) @@ -462,6 +464,14 @@ else error "Only Haskell target allows for monad syntax" end; +(** formal checking of compiled code **) + +fun check thy = Code_Target.external_check thy target + "EXEC_GHC" I (fn ghc => fn p => fn module_name => + ghc ^ " -fglasgow-exts -odir build -hidir build -stubdir build -e \"\" " ^ module_name ^ ".hs"); + + + (** Isar setup **) fun isar_seri_haskell module_name = diff -r 5d2b3e827371 -r b55f848f34fc src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/Tools/Code/code_ml.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: Tools/code/code_ml.ML +(* Title: Tools/Code/code_ml.ML Author: Florian Haftmann, TU Muenchen Serializer for SML and OCaml. @@ -7,10 +7,13 @@ signature CODE_ML = sig val target_SML: string + val target_OCaml: string val evaluation_code_of: theory -> string -> string -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list val print_tuple: (Code_Printer.fixity -> 'a -> Pretty.T) -> Code_Printer.fixity -> 'a list -> Pretty.T option + val check_SML: theory -> Path.T -> unit + val check_OCaml: theory -> Path.T -> unit val setup: theory -> theory end; @@ -904,7 +907,7 @@ error ("Unknown statement name: " ^ labelled_name name); in (deresolver, nodes) end; -fun serialize_ml target compile print_module print_stmt raw_module_name with_signatures labelled_name +fun serialize_ml target print_module print_stmt raw_module_name with_signatures labelled_name reserved includes raw_module_alias _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination = let val is_cons = Code_Thingol.is_cons program; @@ -935,7 +938,6 @@ val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] nodes)); in Code_Target.mk_serialization target - (case compile of SOME compile => SOME (compile o code_of_pretty) | NONE => NONE) (fn NONE => code_writeln | SOME file => File.write file o code_of_pretty) (rpair stmt_names' o code_of_pretty) p destination end; @@ -947,7 +949,18 @@ fun evaluation_code_of thy target struct_name = Code_Target.serialize_custom thy (target, (fn _ => fn [] => - serialize_ml target (SOME (K ())) print_sml_module print_sml_stmt (SOME struct_name) true, literals_sml)); + serialize_ml target print_sml_module print_sml_stmt (SOME struct_name) true, literals_sml)); + + +(** formal checking of compiled code **) + +fun check_SML thy = Code_Target.external_check thy target_SML + "ISABELLE_PROCESS" (fn p => Path.append p (Path.explode "ROOT.ML")) + (fn isabelle => fn p => fn _ => isabelle ^ " -r -q -u Pure"); + +fun check_OCaml thy = Code_Target.external_check thy target_OCaml + "EXEC_OCAML" (fn p => Path.append p (Path.explode "ROOT.ocaml")) + (fn ocaml => fn p => fn _ => ocaml ^ " -w pu nums.cma " ^ File.shell_path p); (** Isar setup **) @@ -955,12 +968,11 @@ fun isar_seri_sml module_name = Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true >> (fn with_signatures => serialize_ml target_SML - (SOME (use_text ML_Env.local_context (1, "generated code") false)) print_sml_module print_sml_stmt module_name with_signatures)); fun isar_seri_ocaml module_name = Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true - >> (fn with_signatures => serialize_ml target_OCaml NONE + >> (fn with_signatures => serialize_ml target_OCaml print_ocaml_module print_ocaml_stmt module_name with_signatures)); val setup = diff -r 5d2b3e827371 -r b55f848f34fc src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/Tools/Code/code_preproc.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: Tools/code/code_preproc.ML +(* Title: Tools/Code/code_preproc.ML Author: Florian Haftmann, TU Muenchen Preprocessing code equations into a well-sorted system diff -r 5d2b3e827371 -r b55f848f34fc src/Tools/Code/code_printer.ML --- a/src/Tools/Code/code_printer.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/Tools/Code/code_printer.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: Tools/code/code_printer.ML +(* Title: Tools/Code/code_printer.ML Author: Florian Haftmann, TU Muenchen Generic operations for pretty printing of target language code. diff -r 5d2b3e827371 -r b55f848f34fc src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/Tools/Code/code_scala.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,10 +1,13 @@ -(* Author: Florian Haftmann, TU Muenchen +(* Title: Tools/Code/code_scala.ML + Author: Florian Haftmann, TU Muenchen Serializer for Scala. *) signature CODE_SCALA = sig + val target: string + val check: theory -> Path.T -> unit val setup: theory -> theory end; @@ -379,7 +382,7 @@ val _ = File.mkdir_leaf (Path.dir pathname); in File.write pathname (code_of_pretty content) end in - Code_Target.mk_serialization target NONE + Code_Target.mk_serialization target (fn NONE => K () o map (code_writeln o snd) | SOME file => K () o map (write_module (check_destination file))) (rpair [] o cat_lines o map (code_of_pretty o snd)) @@ -411,6 +414,14 @@ } end; +(** formal checking of compiled code **) + +fun check thy = Code_Target.external_check thy target + "SCALA_HOME" I (fn scala_home => fn p => fn _ => + Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " *.scala"); + + + (** Isar setup **) fun isar_seri_scala module_name = diff -r 5d2b3e827371 -r b55f848f34fc src/Tools/Code/code_simp.ML --- a/src/Tools/Code/code_simp.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/Tools/Code/code_simp.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: Tools/code/code_simp.ML +(* Title: Tools/Code/code_simp.ML Author: Florian Haftmann, TU Muenchen Connecting the simplifier and the code generator. diff -r 5d2b3e827371 -r b55f848f34fc src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/Tools/Code/code_target.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: Tools/code/code_target.ML +(* Title: Tools/Code/code_target.ML Author: Florian Haftmann, TU Muenchen Serializer from intermediate language ("Thin-gol") to target languages. @@ -21,8 +21,7 @@ type serialization val parse_args: 'a parser -> Token.T list -> 'a val stmt_names_of_destination: destination -> string list - val mk_serialization: string -> ('a -> unit) option - -> (Path.T option -> 'a -> unit) + val mk_serialization: string -> (Path.T option -> 'a -> unit) -> ('a -> string * string option list) -> 'a -> serialization val serialize: theory -> string -> int option -> string option -> Token.T list @@ -30,12 +29,13 @@ val serialize_custom: theory -> string * (serializer * literals) -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list val the_literals: theory -> string -> literals - val compile: serialization -> unit val export: serialization -> unit val file: Path.T -> serialization -> unit val string: string list -> serialization -> string val code_of: theory -> string -> int option -> string -> string list -> (Code_Thingol.naming -> string list) -> string + val external_check: theory -> string -> string + -> (Path.T -> Path.T) -> (string -> Path.T -> string -> string) -> Path.T -> unit val set_default_code_width: int -> theory -> theory val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit @@ -62,10 +62,9 @@ (** basics **) -datatype destination = Compile | Export | File of Path.T | String of string list; +datatype destination = Export | File of Path.T | String of string list; type serialization = destination -> (string * string option list) option; -fun compile f = (f Compile; ()); fun export f = (f Export; ()); fun file p f = (f (File p); ()); fun string stmts f = fst (the (f (String stmts))); @@ -73,11 +72,9 @@ fun stmt_names_of_destination (String stmts) = stmts | stmt_names_of_destination _ = []; -fun mk_serialization target (SOME comp) _ _ code Compile = (comp code; NONE) - | mk_serialization target NONE _ _ _ Compile = error (target ^ ": no internal compilation") - | mk_serialization target _ output _ code Export = (output NONE code ; NONE) - | mk_serialization target _ output _ code (File file) = (output (SOME file) code; NONE) - | mk_serialization target _ _ string code (String _) = SOME (string code); +fun mk_serialization target output _ code Export = (output NONE code ; NONE) + | mk_serialization target output _ code (File file) = (output (SOME file) code; NONE) + | mk_serialization target _ string code (String _) = SOME (string code); (** theory data **) @@ -355,13 +352,33 @@ if member (op =) names3 name then SOME c else NONE) (cs2 ~~ names2); in union (op =) cs3 cs1 end; +fun external_check thy target env_var make_destination make_command p = + let + val env_param = getenv env_var; + fun ext_check env_param = + let + val module_name = "Code_Test"; + val (cs, (naming, program)) = + Code_Thingol.consts_program thy false (read_const_exprs thy ["*"]); + val destination = make_destination p; + val _ = file destination (serialize thy target (SOME 80) + (SOME module_name) [] naming program cs); + val cmd = make_command env_param destination module_name; + in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd) <> 0 + then error ("Code check failed for " ^ target ^ ": " ^ cmd) + else () + end; + in if env_param = "" + then warning (env_var ^ " not set; skipped code check for " ^ target) + else ext_check env_param + end; + fun export_code thy cs seris = let val (cs', (naming, program)) = Code_Thingol.consts_program thy false cs; fun mk_seri_dest dest = case dest - of NONE => compile - | SOME "-" => export - | SOME f => file (Path.explode f) + of "-" => export + | f => file (Path.explode f) val _ = map (fn (((target, module), dest), args) => (mk_seri_dest dest (serialize thy target NONE module args naming program cs'))) seris; in () end; @@ -507,7 +524,7 @@ (Scan.repeat1 Parse.term_group -- Scan.repeat (Parse.$$$ inK |-- Parse.name -- Scan.option (Parse.$$$ module_nameK |-- Parse.name) - -- Scan.option (Parse.$$$ fileK |-- Parse.name) + --| Parse.$$$ fileK -- Parse.name -- Scan.optional (Parse.$$$ "(" |-- Args.parse --| Parse.$$$ ")") [] ) >> (fn (raw_cs, seris) => export_code_cmd raw_cs seris)); diff -r 5d2b3e827371 -r b55f848f34fc src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/Tools/Code/code_thingol.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: Tools/code/code_thingol.ML +(* Title: Tools/Code/code_thingol.ML Author: Florian Haftmann, TU Muenchen Intermediate language ("Thin-gol") representing executable code. diff -r 5d2b3e827371 -r b55f848f34fc src/Tools/Code/etc/settings --- a/src/Tools/Code/etc/settings Tue Jul 06 21:33:14 2010 +0200 +++ b/src/Tools/Code/etc/settings Sat Jul 10 21:38:16 2010 +0200 @@ -4,9 +4,11 @@ EXEC_GHC=$(choosefrom \ "$ISABELLE_HOME/contrib/ghc" \ "$ISABELLE_HOME/../ghc" \ - $(type -p ghc)) + $(type -p ghc) \ + "") EXEC_OCAML=$(choosefrom \ "$ISABELLE_HOME/contrib/ocaml" \ "$ISABELLE_HOME/../ocaml" \ - $(type -p ocaml)) + $(type -p ocaml) \ + "") diff -r 5d2b3e827371 -r b55f848f34fc src/Tools/WWW_Find/html_unicode.ML --- a/src/Tools/WWW_Find/html_unicode.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/Tools/WWW_Find/html_unicode.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: html_unicode.ML +(* Title: Tools/WWW_Find/html_unicode.ML Author: Timothy Bourke, NICTA Based on Pure/Thy/html.ML by Markus Wenzel and Stefan Berghofer, TU Muenchen diff -r 5d2b3e827371 -r b55f848f34fc src/Tools/cache_io.ML --- a/src/Tools/cache_io.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/Tools/cache_io.ML Sat Jul 10 21:38:16 2010 +0200 @@ -7,6 +7,7 @@ signature CACHE_IO = sig val with_tmp_file: string -> (Path.T -> 'a) -> 'a + val with_tmp_dir: string -> (Path.T -> 'a) -> 'a val run: (Path.T -> Path.T -> string) -> string -> string list * string list type cache @@ -31,6 +32,14 @@ val _ = try File.rm path in Exn.release x end +fun with_tmp_dir name f = + let + val path = File.tmp_path (Path.explode (name ^ serial_string ())) + val _ = File.mkdir path + val x = Exn.capture f path + val _ = try File.rm_tree path + in Exn.release x end + fun run make_cmd str = with_tmp_file cache_io_prefix (fn in_path => with_tmp_file cache_io_prefix (fn out_path => diff -r 5d2b3e827371 -r b55f848f34fc src/Tools/value.ML --- a/src/Tools/value.ML Tue Jul 06 21:33:14 2010 +0200 +++ b/src/Tools/value.ML Sat Jul 10 21:38:16 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: Pure/Tools/value.ML +(* Title: Tools/value.ML Author: Florian Haftmann, TU Muenchen Generic value command for arbitrary evaluators.