--- 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
--- /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
+
--- 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)
---------------------------------
--- 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
--- 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
--- 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"
--- 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:
--- 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<label.length();i++)
{
--- a/lib/browser/GraphBrowser/Region.java Tue Jul 06 21:33:14 2010 +0200
+++ b/lib/browser/GraphBrowser/Region.java Sat Jul 10 21:38:16 2010 +0200
@@ -79,7 +79,7 @@
public int spaceBetween(Region r2) {
return ((Vertex)(r2.getVertices().nextElement())).leftX()-
((Vertex)(vertices.lastElement())).rightX()-
- gra.box_hspace+gra.box_width;
+ 20;
}
public boolean touching(Region r2) {
--- a/lib/browser/GraphBrowser/Vertex.java Tue Jul 06 21:33:14 2010 +0200
+++ b/lib/browser/GraphBrowser/Vertex.java Sat Jul 10 21:38:16 2010 +0200
@@ -178,6 +178,10 @@
return succs;
}
+ public int box_width() { return getLabelSize(gra.gfx).width+8; }
+
+ public int box_width2() { return box_width()/2; }
+
public void setX(int x) {this.x=x;}
public void setY(int y) {this.y=y;}
--- a/src/FOLP/classical.ML Tue Jul 06 21:33:14 2010 +0200
+++ b/src/FOLP/classical.ML Sat Jul 10 21:38:16 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: FOLP/classical
+(* Title: FOLP/classical.ML
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
--- a/src/FOLP/hypsubst.ML Tue Jul 06 21:33:14 2010 +0200
+++ b/src/FOLP/hypsubst.ML Sat Jul 10 21:38:16 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: FOLP/hypsubst
+(* Title: FOLP/hypsubst.ML
Author: Martin D Coen, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
--- a/src/HOL/Codegenerator_Test/Generate.thy Tue Jul 06 21:33:14 2010 +0200
+++ b/src/HOL/Codegenerator_Test/Generate.thy Sat Jul 10 21:38:16 2010 +0200
@@ -7,9 +7,23 @@
imports Candidates
begin
-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
--- a/src/HOL/Codegenerator_Test/Generate_Pretty.thy Tue Jul 06 21:33:14 2010 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Pretty.thy Sat Jul 10 21:38:16 2010 +0200
@@ -12,9 +12,23 @@
lemma [code, code del]: "(less_eq :: char \<Rightarrow> _) = less_eq" ..
lemma [code, code del]: "(less :: char \<Rightarrow> _) = 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
--- 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.
*)
--- 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
--- 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
--- 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
*)
--- 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 \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "o>" 60)
+ fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "\<circ>>" 60)
where
- "f o> g = (\<lambda>x. g (f x))"
+ "f \<circ>> g = (\<lambda>x. g (f x))"
-lemma fcomp_apply: "(f o> g) x = g (f x)"
+lemma fcomp_apply [simp]: "(f \<circ>> 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 \<circ>> g) \<circ>> h = f \<circ>> (g \<circ>> h)"
by (simp add: fcomp_def)
-lemma id_fcomp [simp]: "id o> g = g"
+lemma id_fcomp [simp]: "id \<circ>> g = g"
by (simp add: fcomp_def)
-lemma fcomp_id [simp]: "f o> id = f"
+lemma fcomp_id [simp]: "f \<circ>> id = f"
by (simp add: fcomp_def)
code_const fcomp
(Eval infixl 1 "#>")
-no_notation fcomp (infixl "o>" 60)
+no_notation fcomp (infixl "\<circ>>" 60)
subsection {* Injectivity and Surjectivity *}
--- 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 = (\<exists>n. i = f n \<and> (e,sigma) -a-> n)"
- by (rule,cases set: evala) auto
-
-lemma [simp]:
- "(Op2 f a1 a2,sigma) -a-> i =
- (\<exists>n0 n1. i = f n0 n1 \<and> (a1, sigma) -a-> n0 \<and> (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)"
--- 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:
- "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s)"
- by auto
-
-lemma assign:
- "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s[x\<mapsto>a s])"
- by auto
-
-lemma semi:
- "\<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>c s' = (\<exists>s''. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'' \<and> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>c s')"
- by auto
+inductive_simps
+ skip: "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s'"
+ and assign: "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s'"
+ and semi: "\<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
lemma ifTrue:
"b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'"
--- 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 \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> bool" where*)
array_present :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> bool" where
"array_present a h \<longleftrightarrow> addr_of_array a < lim h"
-definition
+definition (*FIXME get :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a list" where*)
get_array :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> '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\<Colon>heap array \<Rightarrow> 'a list \<Rightarrow> heap \<Rightarrow> heap" where
"set_array a x =
arrays_update (\<lambda>h. h(TYPEREP('a) := ((h(TYPEREP('a))) (addr_of_array a:=map to_nat x))))"
-definition array :: "'a list \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where
+definition (*FIXME alloc*)
+ array :: "'a list \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where
"array xs h = (let
l = lim h;
r = Array l;
h'' = set_array r xs (h\<lparr>lim := l + 1\<rparr>)
in (r, h''))"
-definition length :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> nat" where
+definition (*FIXME length :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> nat" where*)
+ length :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> nat" where
"length a h = List.length (get_array a h)"
-definition change :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
+definition (*FIXME update*)
+ change :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> 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\<Colon>heap array \<Rightarrow> 'b\<Colon>heap array \<Rightarrow> bool" (infix "=!!=" 70) where
+ "r =!!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_array r \<noteq> addr_of_array s"
+
+
+subsection {* Monad operations *}
+
+definition new :: "nat \<Rightarrow> 'a\<Colon>heap \<Rightarrow> 'a array Heap" where
+ [code del]: "new n x = Heap_Monad.heap (array (replicate n x))"
+
+definition of_list :: "'a\<Colon>heap list \<Rightarrow> 'a array Heap" where
+ [code del]: "of_list xs = Heap_Monad.heap (array xs)"
+
+definition make :: "nat \<Rightarrow> (nat \<Rightarrow> 'a\<Colon>heap) \<Rightarrow> 'a array Heap" where
+ [code del]: "make n f = Heap_Monad.heap (array (map f [0 ..< n]))"
+
+definition len :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where
+ [code del]: "len a = Heap_Monad.tap (\<lambda>h. length a h)"
+
+definition nth :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a Heap" where
+ [code del]: "nth a i = Heap_Monad.guard (\<lambda>h. i < length a h)
+ (\<lambda>h. (get_array a h ! i, h))"
+
+definition upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap" where
+ [code del]: "upd i x a = Heap_Monad.guard (\<lambda>h. i < length a h)
+ (\<lambda>h. (a, change a i x h))"
+
+definition map_entry :: "nat \<Rightarrow> ('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap" where
+ [code del]: "map_entry i f a = Heap_Monad.guard (\<lambda>h. i < length a h)
+ (\<lambda>h. (a, change a i (f (get_array a h ! i)) h))"
+
+definition swap :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a Heap" where
+ [code del]: "swap i x a = Heap_Monad.guard (\<lambda>h. i < length a h)
+ (\<lambda>h. (get_array a h ! i, change a i x h))"
+
+definition freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap" where
+ [code del]: "freeze a = Heap_Monad.tap (\<lambda>h. get_array a h)"
+
+
+subsection {* Properties *}
text {* FIXME: Does there exist a "canonical" array axiomatisation in
the literature? *}
-definition noteq_arrs :: "('a\<Colon>heap) array \<Rightarrow> ('b\<Colon>heap) array \<Rightarrow> bool" (infix "=!!=" 70) where
- "r =!!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_array r \<noteq> addr_of_array s"
+text {* Primitives *}
lemma noteq_arrs_sym: "a =!!= b \<Longrightarrow> b =!!= a"
and unequal_arrs [simp]: "a \<noteq> a' \<longleftrightarrow> 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 \<Rightarrow> 'a\<Colon>heap \<Rightarrow> '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\<Colon>heap list \<Rightarrow> '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\<Colon>heap array \<Rightarrow> nat Heap" where
- [code del]: "len arr = Heap_Monad.heap (\<lambda>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 \<Longrightarrow>
+ execute (nth a i) h = Some (get_array a h ! i, h)"
+ "i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None"
+ by (simp_all add: nth_def execute_simps)
-definition
- nth :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a Heap"
-where
- [code del]: "nth a i = (do len \<leftarrow> len a;
- (if i < len
- then Heap_Monad.heap (\<lambda>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 \<Longrightarrow> success (nth a i) h"
+ by (auto intro: success_intros simp add: nth_def)
+
+lemma execute_upd [execute_simps]:
+ "i < length a h \<Longrightarrow>
+ execute (upd i x a) h = Some (a, change a i x h)"
+ "i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None"
+ by (simp_all add: upd_def execute_simps)
+
+lemma success_updI [success_intros]:
+ "i < length a h \<Longrightarrow> 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 \<Longrightarrow>
+ execute (map_entry i f a) h =
+ Some (a, change a i (f (get_array a h ! i)) h)"
+ "i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None"
+ by (simp_all add: map_entry_def execute_simps)
-definition
- upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap"
-where
- [code del]: "upd i x a = (do len \<leftarrow> len a;
- (if i < len
- then Heap_Monad.heap (\<lambda>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 \<Longrightarrow> 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 \<Longrightarrow>
+ execute (swap i x a) h =
+ Some (get_array a h ! i, change a i x h)"
+ "i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None"
+ by (simp_all add: swap_def execute_simps)
+
+lemma success_swapI [success_intros]:
+ "i < length a h \<Longrightarrow> 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 \<guillemotright> 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 \<Rightarrow> ('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap"
-where
- "map_entry i f a = (do
- x \<leftarrow> nth a i;
- upd i (f x) a
- done)"
+ by (rule Heap_eqI) (simp add: bind_def guard_def upd_def)
-definition
- swap :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a Heap"
-where
- "swap i x a = (do
- y \<leftarrow> nth a i;
- upd i x a;
- return y
- done)"
-
-definition
- make :: "nat \<Rightarrow> (nat \<Rightarrow> 'a\<Colon>heap) \<Rightarrow> 'a array Heap"
-where
- "make n f = of_list (map f [0 ..< n])"
+lemma array_make:
+ "new n x = make n (\<lambda>_. x)"
+ by (rule Heap_eqI) (simp add: map_replicate_trivial)
-definition
- freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap"
-where
- "freeze a = (do
- n \<leftarrow> len a;
- mapM (nth a) [0..<n]
- done)"
+lemma array_of_list_make:
+ "of_list xs = make (List.length xs) (\<lambda>n. xs ! n)"
+ by (rule Heap_eqI) (simp add: map_nth)
-definition
- map :: "('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap"
-where
- "map f a = (do
- n \<leftarrow> len a;
- mapM (\<lambda>n. map_entry n f a) [0..<n];
- return a
- done)"
-
-
-
-subsection {* Properties *}
-
-lemma array_make [code]:
- "Array.new n x = make n (\<lambda>_. 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) (\<lambda>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 \<guillemotright>= (\<lambda>n. return (Code_Numeral.of_nat n))"
-hide_const (open) len'
+
lemma [code]:
- "Array.len a = Array.len' a \<guillemotright>= (\<lambda>i. return (Code_Numeral.nat_of i))"
+ "Array.len a = len' a \<guillemotright>= (\<lambda>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 \<guillemotright> return ()"
-hide_const (open) upd'
+
lemma [code]:
- "Array.upd i x a = Array.upd' a (Code_Numeral.of_nat i) x \<guillemotright> return a"
+ "Array.upd i x a = upd' a (Code_Numeral.of_nat i) x \<guillemotright> return a"
by (simp add: upd'_def upd_return)
+lemma [code]:
+ "map_entry i f a = (do
+ x \<leftarrow> 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 \<leftarrow> 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 \<leftarrow> len a;
+ Heap_Monad.fold_map (\<lambda>i. nth a i) [0..<n]
+ done)"
+proof (rule Heap_eqI)
+ fix h
+ have *: "List.map
+ (\<lambda>x. fst (the (if x < length a h
+ then Some (get_array a h ! x, h) else None)))
+ [0..<length a h] =
+ List.map (List.nth (get_array a h)) [0..<length a h]"
+ by simp
+ have "execute (Heap_Monad.fold_map (Array.nth a) [0..<length a h]) h =
+ Some (get_array a h, h)"
+ apply (subst execute_fold_map_unchanged_heap)
+ apply (simp_all add: nth_def guard_def *)
+ apply (simp add: length_def map_nth)
+ done
+ then have "execute (do
+ n \<leftarrow> len a;
+ Heap_Monad.fold_map (Array.nth a) [0..<n]
+ done) h = Some (get_array a h, h)"
+ by (auto intro: execute_eq_SomeI)
+ then show "execute (freeze a) h = execute (do
+ n \<leftarrow> len a;
+ Heap_Monad.fold_map (Array.nth a) [0..<n]
+ done) h" by simp
+qed
+
+hide_const (open) new' of_list' make' len' nth' upd'
+
+
+text {* SML *}
code_type array (SML "_/ array")
code_const Array (SML "raise/ (Fail/ \"bare Array\")")
@@ -268,7 +363,7 @@
code_reserved SML Array
-subsubsection {* OCaml *}
+text {* OCaml *}
code_type array (OCaml "_/ array")
code_const Array (OCaml "failwith/ \"bare Array\"")
@@ -281,7 +376,7 @@
code_reserved OCaml Array
-subsubsection {* Haskell *}
+text {* Haskell *}
code_type array (Haskell "Heap.STArray/ Heap.RealWorld/ _")
code_const Array (Haskell "error/ \"bare Array\"")
@@ -291,6 +386,4 @@
code_const Array.nth' (Haskell "Heap.readArray")
code_const Array.upd' (Haskell "Heap.writeArray")
-hide_const (open) new map -- {* avoid clashed with some popular names *}
-
end
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jul 06 21:33:14 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Sat Jul 10 21:38:16 2010 +0200
@@ -10,7 +10,7 @@
subsection {* The monad *}
-subsubsection {* Monad combinators *}
+subsubsection {* Monad construction *}
text {* Monadic heap actions either produce values
and transform the heap, or fail *}
@@ -19,6 +19,13 @@
primrec execute :: "'a Heap \<Rightarrow> heap \<Rightarrow> ('a \<times> heap) option" where
[code del]: "execute (Heap f) = f"
+lemma Heap_cases [case_names succeed fail]:
+ fixes f and h
+ assumes succeed: "\<And>x h'. execute f h = Some (x, h') \<Longrightarrow> P"
+ assumes fail: "execute f h = None \<Longrightarrow> 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 @@
"(\<And>h. execute f h = execute g h) \<Longrightarrow> f = g"
by (cases f, cases g) (auto simp: expand_fun_eq)
-lemma Heap_eqI':
- "(\<And>h. (\<lambda>x. execute (f x) h) = (\<lambda>y. execute (g y) h)) \<Longrightarrow> 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 \<Rightarrow> 'a) \<Rightarrow> 'a Heap" where
+ [code del]: "tap f = Heap (\<lambda>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 \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where
[code del]: "heap f = Heap (Some \<circ> f)"
-lemma execute_heap [simp]:
+lemma execute_heap [simp, execute_simps]:
"execute (heap f) = Some \<circ> f"
by (simp add: heap_def)
-lemma heap_cases [case_names succeed fail]:
- fixes f and h
- assumes succeed: "\<And>x h'. execute f h = Some (x, h') \<Longrightarrow> P"
- assumes fail: "execute f h = None \<Longrightarrow> P"
- shows P
- using assms by (cases "execute f h") auto
+definition guard :: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where
+ [code del]: "guard P f = Heap (\<lambda>h. if P h then Some (f h) else None)"
+
+lemma execute_guard [execute_simps]:
+ "\<not> P h \<Longrightarrow> execute (guard P f) h = None"
+ "P h \<Longrightarrow> execute (guard P f) h = Some (f h)"
+ by (simp_all add: guard_def)
+
+
+subsubsection {* Predicate classifying successful computations *}
+
+definition success :: "'a Heap \<Rightarrow> heap \<Rightarrow> bool" where
+ "success f h \<longleftrightarrow> execute f h \<noteq> None"
+
+lemma successI:
+ "execute f h \<noteq> None \<Longrightarrow> 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 \<Longrightarrow> success (guard P f) h"
+ by (rule successI) (simp add: execute_guard)
+
+lemma success_LetI [success_intros]:
+ "x = t \<Longrightarrow> success (f x) h \<Longrightarrow> success (let x = t in f x) h"
+ by (simp add: Let_def)
+
+
+subsubsection {* Monad combinators *}
definition return :: "'a \<Rightarrow> 'a Heap" where
[code del]: "return x = heap (Pair x)"
-lemma execute_return [simp]:
+lemma execute_return [simp, execute_simps]:
"execute (return x) = Some \<circ> Pair x"
by (simp add: return_def)
+lemma success_returnI [iff, success_intros]:
+ "success (return x) h"
+ by (rule successI) simp
+
definition raise :: "string \<Rightarrow> 'a Heap" where -- {* the string is just decoration *}
[code del]: "raise s = Heap (\<lambda>_. None)"
-lemma execute_raise [simp]:
+lemma execute_raise [simp, execute_simps]:
"execute (raise s) = (\<lambda>_. None)"
by (simp add: raise_def)
-definition bindM :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where
+definition bind :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where
[code del]: "f >>= g = Heap (\<lambda>h. case execute f h of
Some (x, h') \<Rightarrow> execute (g x) h'
| None \<Rightarrow> None)"
-notation bindM (infixl "\<guillemotright>=" 54)
+notation bind (infixl "\<guillemotright>=" 54)
-lemma execute_bind [simp]:
+lemma execute_bind [execute_simps]:
"execute f h = Some (x, h') \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g x) h'"
"execute f h = None \<Longrightarrow> execute (f \<guillemotright>= g) h = None"
- by (simp_all add: bindM_def)
+ by (simp_all add: bind_def)
+
+lemma success_bindI [success_intros]:
+ "success f h \<Longrightarrow> success (g (fst (the (execute f h)))) (snd (the (execute f h))) \<Longrightarrow> success (f \<guillemotright>= g) h"
+ by (auto intro!: successI elim!: successE simp add: bind_def)
-lemma execute_bind_heap [simp]:
- "execute (heap f \<guillemotright>= 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 \<Longrightarrow> execute (f \<guillemotright>= 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 \<guillemotright>= g) h = Some (y, h'')"
+ using assms by (simp add: bind_def)
+
lemma return_bind [simp]: "return x \<guillemotright>= f = f x"
- by (rule Heap_eqI) simp
+ by (rule Heap_eqI) (simp add: execute_bind)
lemma bind_return [simp]: "f \<guillemotright>= 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 \<guillemotright>= g) \<guillemotright>= k = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= 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 \<guillemotright>= f = raise e"
- by (rule Heap_eqI) simp
+ by (rule Heap_eqI) (simp add: execute_bind)
-abbreviation chainM :: "'a Heap \<Rightarrow> 'b Heap \<Rightarrow> 'b Heap" (infixl ">>" 54) where
+abbreviation chain :: "'a Heap \<Rightarrow> 'b Heap \<Rightarrow> 'b Heap" (infixl ">>" 54) where
"f >> g \<equiv> f >>= (\<lambda>_. g)"
-notation chainM (infixl "\<guillemotright>" 54)
+notation chain (infixl "\<guillemotright>" 54)
subsubsection {* do-syntax *}
@@ -105,9 +185,9 @@
syntax
"_do" :: "do_expr \<Rightarrow> 'a"
("(do (_)//done)" [12] 100)
- "_bindM" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
+ "_bind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
("_ <- _;//_" [1000, 13, 12] 12)
- "_chainM" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
+ "_chain" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
("_;//_" [13, 12] 12)
"_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
("let _ = _;//_" [1000, 13, 12] 12)
@@ -115,13 +195,13 @@
("_" [12] 12)
syntax (xsymbols)
- "_bindM" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
+ "_bind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
("_ \<leftarrow> _;//_" [1000, 13, 12] 12)
translations
"_do f" => "f"
- "_bindM x f g" => "f \<guillemotright>= (\<lambda>x. g)"
- "_chainM f g" => "f \<guillemotright> g"
+ "_bind x f g" => "f \<guillemotright>= (\<lambda>x. g)"
+ "_chain f g" => "f \<guillemotright> g"
"_let x t f" => "CONST Let t (\<lambda>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 \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a Heap" where
"assert P x = (if P x then return x else raise ''assert'')"
+lemma execute_assert [execute_simps]:
+ "P x \<Longrightarrow> execute (assert P x) h = Some (x, h)"
+ "\<not> P x \<Longrightarrow> execute (assert P x) h = None"
+ by (simp_all add: assert_def)
+
+lemma success_assertI [success_intros]:
+ "P x \<Longrightarrow> success (assert P x) h"
+ by (rule successI) (simp add: execute_assert)
+
lemma assert_cong [fundef_cong]:
assumes "P = P'"
assumes "\<And>x. P' x \<Longrightarrow> 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 \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b Heap" where
- "liftM f = return o f"
+definition lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> '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 \<guillemotright>= liftM g) = (f \<guillemotright>= (\<lambda>x. return (g x)))"
- by (simp add: liftM_def comp_def)
+lemma bind_lift:
+ "(f \<guillemotright>= lift g) = (f \<guillemotright>= (\<lambda>x. return (g x)))"
+ by (simp add: lift_def comp_def)
+
-primrec mapM :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b list Heap" where
- "mapM f [] = return []"
-| "mapM f (x#xs) = do
+subsubsection {* Iteration -- warning: this is rarely useful! *}
+
+primrec fold_map :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b list Heap" where
+ "fold_map f [] = return []"
+| "fold_map f (x # xs) = do
y \<leftarrow> f x;
- ys \<leftarrow> mapM f xs;
+ ys \<leftarrow> fold_map f xs;
return (y # ys)
done"
+lemma fold_map_append:
+ "fold_map f (xs @ ys) = fold_map f xs \<guillemotright>= (\<lambda>xs. fold_map f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))"
+ by (induct xs) simp_all
+
+lemma execute_fold_map_unchanged_heap [execute_simps]:
+ assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<exists>y. execute (f x) h = Some (y, h)"
+ shows "execute (fold_map f xs) h =
+ Some (List.map (\<lambda>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 (\<lambda>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 \<guillemotright>=" (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
--- 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 \<Rightarrow> 'a\<Colon>heap ref \<Rightarrow> bool" where
"present h r \<longleftrightarrow> addr_of_ref r < lim h"
@@ -35,6 +35,31 @@
definition noteq :: "'a\<Colon>heap ref \<Rightarrow> 'b\<Colon>heap ref \<Rightarrow> bool" (infix "=!=" 70) where
"r =!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_ref r \<noteq> addr_of_ref s"
+
+subsection {* Monad operations *}
+
+definition ref :: "'a\<Colon>heap \<Rightarrow> 'a ref Heap" where
+ [code del]: "ref v = Heap_Monad.heap (alloc v)"
+
+definition lookup :: "'a\<Colon>heap ref \<Rightarrow> 'a Heap" ("!_" 61) where
+ [code del]: "lookup r = Heap_Monad.tap (\<lambda>h. get h r)"
+
+definition update :: "'a ref \<Rightarrow> 'a\<Colon>heap \<Rightarrow> unit Heap" ("_ := _" 62) where
+ [code del]: "update r v = Heap_Monad.heap (\<lambda>h. ((), set r v h))"
+
+definition change :: "('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a ref \<Rightarrow> 'a Heap" where
+ "change f r = (do
+ x \<leftarrow> ! r;
+ let y = f x;
+ r := y;
+ return y
+ done)"
+
+
+subsection {* Properties *}
+
+text {* Primitives *}
+
lemma noteq_sym: "r =!= s \<Longrightarrow> s =!= r"
and unequal [simp]: "r \<noteq> r' \<longleftrightarrow> 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\<Colon>heap \<Rightarrow> '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\<Colon>heap ref \<Rightarrow> 'a Heap" ("!_" 61) where
- [code del]: "lookup r = Heap_Monad.heap (\<lambda>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 \<Rightarrow> 'a\<Colon>heap \<Rightarrow> unit Heap" ("_ := _" 62) where
- [code del]: "update r v = Heap_Monad.heap (\<lambda>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\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a ref \<Rightarrow> 'a Heap" where
- "change f r = (do
- x \<leftarrow> ! 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 \<guillemotright> 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 (\<lambda>_. e) r \<guillemotright> 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
--- 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 "\<And>h h'. P f [] h h' []"
- assumes "\<And>h h1 h' x xs y ys. \<lbrakk> crel (f x) h h1 y; crel (mapM f xs) h1 h' ys; P f xs h1 h' ys \<rbrakk> \<Longrightarrow> P f (x#xs) h h' (y#ys)"
+ assumes "\<And>h h1 h' x xs y ys. \<lbrakk> crel (f x) h h1 y; crel (Heap_Monad.fold_map f xs) h1 h' ys; P f xs h1 h' ys \<rbrakk> \<Longrightarrow> 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 \<Longrightarrow> 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 \<le> b"
shows "[b - Suc a..<b] = (b - Suc a)#[b - a..<b]"
proof -
@@ -158,9 +161,9 @@
with l show ?thesis by (simp add: upt_conv_Cons)
qed
-lemma crel_mapM_nth:
+lemma crel_fold_map_nth:
assumes
- "crel (mapM (Array.nth a) [Array.length a h - n..<Array.length a h]) h h' xs"
+ "crel (Heap_Monad.fold_map (Array.nth a) [Array.length a h - n..<Array.length a h]) h h' xs"
assumes "n \<le> Array.length a h"
shows "h = h' \<and> 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..<Array.length a h] = (Array.length a h - Suc n)#[Array.length a h - n..<Array.length a h]"
by (simp add: upt_conv_Cons')
with Suc(2) obtain r where
- crel_mapM: "crel (mapM (Array.nth a) [Array.length a h - n..<Array.length a h]) h h' r"
+ crel_fold_map: "crel (Heap_Monad.fold_map (Array.nth a) [Array.length a h - n..<Array.length a h]) h h' r"
and xs_def: "xs = get_array a h ! (Array.length a h - Suc n) # r"
by (auto elim!: crelE crel_nth crel_return)
from Suc(3) have "Array.length a h - n = Suc (Array.length a h - Suc n)"
by arith
- with Suc.hyps[OF crel_mapM] xs_def show ?case
+ with Suc.hyps[OF crel_fold_map] xs_def show ?case
unfolding Array.length_def
by (auto simp add: nth_drop')
qed
@@ -185,17 +188,11 @@
lemma crel_freeze:
assumes "crel (Array.freeze a) h h' xs"
obtains "h = h'" "xs = get_array a h"
-proof
- from assms have "crel (mapM (Array.nth a) [0..<Array.length a h]) h h' xs"
- unfolding freeze_def
- by (auto elim: crelE crel_length)
- hence "crel (mapM (Array.nth a) [(Array.length a h - Array.length a h)..<Array.length a h]) h h' xs"
- by simp
- from crel_mapM_nth[OF this] show "h = h'" and "xs = get_array a h" by auto
-qed
+ using assms unfolding freeze_def
+ by (elim crel_tap) simp
-lemma crel_mapM_map_entry_remains:
- assumes "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h h' r"
+lemma crel_fold_map_map_entry_remains:
+ assumes "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h h' r"
assumes "i < Array.length a h - n"
shows "get_array a h ! i = get_array a h' ! i"
using assms
@@ -209,16 +206,16 @@
from Suc(3) have "[Array.length a h - Suc n..<Array.length a h] = (Array.length a h - Suc n)#[Array.length a h - n..<Array.length a h]"
by (simp add: upt_conv_Cons')
from Suc(2) this obtain r where
- crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
+ crel_fold_map: "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
by (auto simp add: elim!: crelE crel_map_entry crel_return)
have length_remains: "Array.length a ?h1 = Array.length a h" by simp
- from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a ?h1 - n..<Array.length a ?h1]) ?h1 h' r"
+ from crel_fold_map have crel_fold_map': "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a ?h1 - n..<Array.length a ?h1]) ?h1 h' r"
by simp
from Suc(1)[OF this] length_remains Suc(3) show ?case by simp
qed
-lemma crel_mapM_map_entry_changes:
- assumes "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h h' r"
+lemma crel_fold_map_map_entry_changes:
+ assumes "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h h' r"
assumes "n \<le> Array.length a h"
assumes "i \<ge> 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..<Array.length a h] = (Array.length a h - Suc n)#[Array.length a h - n..<Array.length a h]"
by (simp add: upt_conv_Cons')
from Suc(2) this obtain r where
- crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
+ crel_fold_map: "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
by (auto simp add: elim!: crelE crel_map_entry crel_return)
have length_remains: "Array.length a ?h1 = Array.length a h" by simp
from Suc(3) have less: "Array.length a h - Suc n < Array.length a h - n" by arith
from Suc(3) have less2: "Array.length a h - Suc n < Array.length a h" by arith
from Suc(4) length_remains have cases: "i = Array.length a ?h1 - Suc n \<or> i \<ge> Array.length a ?h1 - n" by arith
- from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a ?h1 - n..<Array.length a ?h1]) ?h1 h' r"
+ from crel_fold_map have crel_fold_map': "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a ?h1 - n..<Array.length a ?h1]) ?h1 h' r"
by simp
from Suc(1)[OF this] cases Suc(3) Suc(5) length_remains
- crel_mapM_map_entry_remains[OF this, of "Array.length a h - Suc n", symmetric] less less2
+ crel_fold_map_map_entry_remains[OF this, of "Array.length a h - Suc n", symmetric] less less2
show ?case
by (auto simp add: nth_list_update_eq Array.length_def)
qed
-lemma crel_mapM_map_entry_length:
- assumes "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h h' r"
+lemma crel_fold_map_map_entry_length:
+ assumes "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h h' r"
assumes "n \<le> 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..<Array.length a h] = (Array.length a h - Suc n)#[Array.length a h - n..<Array.length a h]"
by (simp add: upt_conv_Cons')
from Suc(2) this obtain r where
- crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
+ crel_fold_map: "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
by (auto elim!: crelE crel_map_entry crel_return)
have length_remains: "Array.length a ?h1 = Array.length a h" by simp
- from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a ?h1 - n..<Array.length a ?h1]) ?h1 h' r"
+ from crel_fold_map have crel_fold_map': "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a ?h1 - n..<Array.length a ?h1]) ?h1 h' r"
by simp
from Suc(1)[OF this] length_remains Suc(3) show ?case by simp
qed
-lemma crel_mapM_map_entry:
-assumes "crel (mapM (\<lambda>n. map_entry n f a) [0..<Array.length a h]) h h' r"
+lemma crel_fold_map_map_entry:
+assumes "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [0..<Array.length a h]) h h' r"
shows "get_array a h' = List.map f (get_array a h)"
proof -
- from assms have "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - Array.length a h..<Array.length a h]) h h' r" by simp
- from crel_mapM_map_entry_length[OF this]
- crel_mapM_map_entry_changes[OF this] show ?thesis
+ from assms have "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - Array.length a h..<Array.length a h]) h h' r" by simp
+ from crel_fold_map_map_entry_length[OF this]
+ crel_fold_map_map_entry_changes[OF this] show ?thesis
unfolding Array.length_def
by (auto intro: nth_equalityI)
qed
-lemma crel_map_weak:
- assumes crel_map: "crel (Array.map f a) h h' r"
- obtains "r = a" "get_array a h' = List.map f (get_array a h)"
-proof
- from assms crel_mapM_map_entry show "get_array a h' = List.map f (get_array a h)"
- unfolding Array.map_def
- by (fastsimp elim!: crelE crel_length crel_return)
- from assms show "r = a"
- unfolding Array.map_def
- by (elim crelE crel_return)
-qed
subsection {* Elimination rules for reference commands *}
@@ -333,23 +319,20 @@
lemma crel_lookup:
assumes "crel (!r') h h' r"
obtains "h = h'" "r = Ref.get h r'"
-using assms
-unfolding Ref.lookup_def
-by (auto elim: crel_heap)
+ using assms unfolding Ref.lookup_def
+ by (auto elim: crel_tap)
lemma crel_update:
assumes "crel (r' := v) h h' r"
obtains "h' = Ref.set r' v h" "r = ()"
-using assms
-unfolding Ref.update_def
-by (auto elim: crel_heap)
+ using assms unfolding Ref.update_def
+ by (auto elim: crel_heap)
lemma crel_change:
assumes "crel (Ref.change f r') h h' r"
obtains "h' = Ref.set r' (f (Ref.get h r')) h" "r = f (Ref.get h r')"
-using assms
-unfolding Ref.change_def Let_def
-by (auto elim!: crelE crel_lookup crel_update crel_return)
+ using assms unfolding Ref.change_def Let_def
+ by (auto elim!: crelE crel_lookup crel_update crel_return)
subsection {* Elimination rules for the assert command *}
@@ -361,7 +344,7 @@
by (elim crel_if crel_return crel_raise) auto
lemma crel_assert_eq: "(\<And>h h' r. crel f h h' r \<Longrightarrow> P r) \<Longrightarrow> f \<guillemotright>= 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 "\<exists>h' rs'. crel f h h' rs' \<and> (\<exists>h'' rs. crel (g rs') h' h'' rs)"
shows "\<exists>h'' rs. crel (f\<guillemotright>= 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 \<Rightarrow> heap \<Rightarrow> bool"
-where
- "noError c h \<longleftrightarrow> (\<exists>r h'. Some (r, h') = Heap_Monad.execute c h)"
-
-lemma noError_def': -- FIXME
- "noError c h \<longleftrightarrow> (\<exists>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 "\<exists>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 "\<And>h' r. crel f h h' r \<Longrightarrow> noError (g r) h'"
- shows "noError (f \<guillemotright>= g) h"
- using assms
- by (auto simp add: noError_def' crel_def' bindM_def)
-
-lemma noErrorI':
- assumes "noError f h"
- assumes "\<And>h' r. crel f h h' r \<Longrightarrow> noError g h'"
- shows "noError (f \<guillemotright> g) h"
- using assms
- by (auto simp add: noError_def' crel_def' bindM_def)
-
-lemma noErrorI2:
-"\<lbrakk>crel f h h' r ; noError f h; noError (g r) h'\<rbrakk>
-\<Longrightarrow> noError (f \<guillemotright>= 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 \<Longrightarrow> noError t h" "\<not> c \<Longrightarrow> noError e h"
- shows "noError (if c then t else e) h"
- using assms
- unfolding noError_def
- by auto
-
-lemma noError_option_case:
- assumes "\<And>y. x = Some y \<Longrightarrow> noError (s y) h"
- assumes "noError n h"
- shows "noError (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h"
-using assms
-by (auto split: option.split)
-
-lemma noError_mapM:
-assumes "\<forall>x \<in> set xs. noError (f x) h \<and> 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 \<guillemotright>= (\<lambda>xs. mapM f ys \<guillemotright>= (\<lambda>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 _ _ _ "\<lambda>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 \<le> Array.length a h"
- shows "noError (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h"
+ shows "success (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h"
using assms
proof (induct n arbitrary: h)
case 0
- thus ?case by (auto intro: noError_return)
+ thus ?case by (auto intro: success_returnI)
next
case (Suc n)
- from Suc.prems have "[Array.length a h - Suc n..<Array.length a h] = (Array.length a h - Suc n)#[Array.length a h - n..<Array.length a h]"
+ from Suc.prems have "[Array.length a h - Suc n..<Array.length a h] =
+ (Array.length a h - Suc n) # [Array.length a h - n..<Array.length a h]"
by (simp add: upt_conv_Cons')
- with Suc.hyps[of "(Array.change a (Array.length a h - Suc n) (f (get_array a h ! (Array.length a h - Suc n))) h)"] Suc.prems show ?case
- by (auto simp add: intro!: noErrorI noError_return noError_map_entry elim: crel_map_entry)
+ with Suc.hyps [of "(Array.change a (Array.length a h - Suc n) (f (get_array a h ! (Array.length a h - Suc n))) h)"] Suc.prems show ?case apply -
+ apply (auto simp add: execute_simps intro!: successI success_returnI success_map_entryI elim: crel_map_entry)
+ apply (subst execute_bind) apply (auto simp add: execute_simps)
+ done
qed
-lemma noError_map:
- shows "noError (Array.map f a) h"
-using noError_mapM_map_entry[of "Array.length a h" a h]
-unfolding Array.map_def
-by (auto intro: noErrorI noError_length noError_return elim!: crel_length)
-
-subsection {* Introduction rules for the reference commands *}
-
-lemma noError_Ref_new:
- shows "noError (ref v) h"
- unfolding Ref.ref_def by (intro noError_heap)
-
-lemma noError_lookup:
- shows "noError (!r) h"
- unfolding lookup_def by (intro noError_heap)
-
-lemma noError_update:
- shows "noError (r := v) h"
- unfolding update_def by (intro noError_heap)
-
-lemma noError_change:
- shows "noError (Ref.change f r) h"
- unfolding Ref.change_def Let_def by (intro noErrorI noError_lookup noError_update noError_return)
-
-subsection {* Introduction rules for the assert command *}
-
-lemma noError_assert:
- assumes "P x"
- shows "noError (assert P x) h"
- using assms
- unfolding assert_def
- by (auto intro: noError_if noError_return)
section {* Cumulative lemmas *}
lemmas crel_elim_all =
crelE crelE' crel_return crel_raise crel_if crel_option_case
- crel_length crel_new_weak crel_nth crel_upd crel_of_list_weak crel_map_entry crel_swap crel_make_weak crel_freeze crel_map_weak
+ crel_length crel_new_weak crel_nth crel_upd crel_of_list_weak crel_map_entry crel_swap crel_make_weak crel_freeze
crel_ref crel_lookup crel_update crel_change
crel_assert
@@ -705,10 +527,5 @@
(* crel_Ref_newI *) crel_lookupI crel_updateI crel_changeI
crel_assert
-lemmas noError_intro_all =
- noErrorI noErrorI' noError_return noError_if noError_option_case
- noError_length noError_new noError_nth noError_upd noError_of_list noError_map_entry noError_swap noError_make noError_freeze noError_map
- noError_Ref_new noError_lookup noError_update noError_change
- noError_assert
end
\ No newline at end of file
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Tue Jul 06 21:33:14 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Sat Jul 10 21:38:16 2010 +0200
@@ -575,23 +575,35 @@
text {* We have proved that quicksort sorts (if no exceptions occur).
We will now show that exceptions do not occur. *}
-lemma noError_part1:
+lemma success_part1I:
assumes "l < Array.length a h" "r < Array.length a h"
- shows "noError (part1 a l r p) h"
+ shows "success (part1 a l r p) h"
using assms
proof (induct a l r p arbitrary: h rule: part1.induct)
case (1 a l r p)
thus ?case
unfolding part1.simps [of a l r] swap_def
- by (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd elim!: crelE crel_upd crel_nth crel_return)
+ by (auto simp add: execute_simps intro!: success_intros elim!: crelE crel_upd crel_nth crel_return)
qed
-lemma noError_partition:
+lemma success_ifI: (*FIXME move*)
+ assumes "c \<Longrightarrow> success t h" "\<not> c \<Longrightarrow> 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 "\<And>h' r. crel f h h' r \<Longrightarrow> success (g r) h'"
+ shows "success (f \<guillemotright>= 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 -
--- 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
--- 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
--- 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 @@
\<Longrightarrow> FDERIV (\<lambda>x. f x - g x) x :> (\<lambda>h. F h - G h)"
by (simp only: diff_minus FDERIV_add FDERIV_minus)
+subsection {* Uniqueness *}
+
+lemma FDERIV_zero_unique:
+ assumes "FDERIV (\<lambda>x. 0) x :> F" shows "F = (\<lambda>h. 0)"
+proof -
+ interpret F: bounded_linear F
+ using assms by (rule FDERIV_bounded_linear)
+ let ?r = "\<lambda>h. norm (F h) / norm h"
+ have *: "?r -- 0 --> 0"
+ using assms unfolding fderiv_def by simp
+ show "F = (\<lambda>h. 0)"
+ proof
+ fix h show "F h = 0"
+ proof (rule ccontr)
+ assume "F h \<noteq> 0"
+ moreover from this have h: "h \<noteq> 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: "\<And>x. x \<noteq> 0 \<Longrightarrow> norm x < s \<Longrightarrow> ?r x < ?r h" by auto
+ from dense [OF s] obtain t where t: "0 < t \<and> t < s" ..
+ let ?x = "scaleR (t / norm h) h"
+ have "?x \<noteq> 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 (\<lambda>x. 0) x :> (\<lambda>h. F h - F' h)"
+ using FDERIV_diff [OF assms] by simp
+ hence "(\<lambda>h. F h - F' h) = (\<lambda>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 "\<dots> = norm (?inv (x + h) - ?inv x) * norm (?inv x)"
by simp
finally show "norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h
- \<le> norm (?inv (x + h) - ?inv x) * norm (?inv x)" .
+ \<le> norm (?inv (x + h) - ?inv x) * norm (?inv x)" .
qed
qed
qed
--- 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 @@
\<Rightarrow> 'a fset \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
[code_unfold]: "setify xs = Code_Evaluation.valtermify Set {\<cdot>} xs"
-notation fcomp (infixl "o>" 60)
-notation scomp (infixl "o\<rightarrow>" 60)
+notation fcomp (infixl "\<circ>>" 60)
+notation scomp (infixl "\<circ>\<rightarrow>" 60)
instantiation fset :: (random) random
begin
definition
- "Quickcheck.random i = Quickcheck.random i o\<rightarrow> (\<lambda>xs. Pair (setify xs))"
+ "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (setify xs))"
instance ..
end
-no_notation fcomp (infixl "o>" 60)
-no_notation scomp (infixl "o\<rightarrow>" 60)
+no_notation fcomp (infixl "\<circ>>" 60)
+no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
subsection {* Lattice instantiation *}
--- 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 @@
\<Rightarrow> 'a multiset \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
[code_unfold]: "bagify xs = Code_Evaluation.valtermify Bag {\<cdot>} xs"
-notation fcomp (infixl "o>" 60)
-notation scomp (infixl "o\<rightarrow>" 60)
+notation fcomp (infixl "\<circ>>" 60)
+notation scomp (infixl "\<circ>\<rightarrow>" 60)
instantiation multiset :: (random) random
begin
definition
- "Quickcheck.random i = Quickcheck.random i o\<rightarrow> (\<lambda>xs. Pair (bagify xs))"
+ "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (bagify xs))"
instance ..
end
-no_notation fcomp (infixl "o>" 60)
-no_notation scomp (infixl "o\<rightarrow>" 60)
+no_notation fcomp (infixl "\<circ>>" 60)
+no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
hide_const (open) bagify
--- 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 "\<circ>>" 60)
+notation (xsymbols) fcomp (infixl "\<circ>>" 60)
notation scomp (infixl "o->" 60)
-notation (xsymbols) scomp (infixl "o\<rightarrow>" 60)
+notation (xsymbols) scomp (infixl "\<circ>\<rightarrow>" 60)
abbreviation (input)
"return \<equiv> 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 \<circ>>"} combinator,
+ forming a forward composition: @{prop "(f \<circ>> 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\<rightarrow>"} combinator:
- @{prop "(f o\<rightarrow> (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.
+ is the purpose of the @{term "op \<circ>\<rightarrow>"} combinator:
+ @{prop "(f \<circ>\<rightarrow> (\<lambda>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\<rightarrow> (\<lambda>x. g)"
- "_fcomp f g" => "f o> g"
+ "_scomp x f g" => "f \<circ>\<rightarrow> (\<lambda>x. g)"
+ "_fcomp f g" => "f \<circ>> g"
"_let x t f" => "CONST Let t (\<lambda>x. f)"
"_done f" => "f"
--- 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
--- 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 \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where
+"while_option b c s = (if (\<exists>k. ~ b ((c ^^ k) s))
+ then Some ((c ^^ (LEAST k. ~ b ((c ^^ k) s))) s)
+ else None)"
-function (tailrec) while :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> '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 "\<exists>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: "\<exists>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 "~ (\<exists>l. ~ b ((c ^^ Suc l) s))" by blast
+ then have "~ (\<exists>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 "\<exists>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: "\<exists>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<k. b ((c ^^ i) s)"
+ by (auto simp: k_def dest: not_less_Least)
+
+ { fix i assume "i <= k" then have "P ((c ^^ i) s)"
+ by (induct i) (auto simp: init step 1) }
+ thus "P t" by (auto simp: t)
+qed
+
+
+subsection {* Total version *}
+
+definition while :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> '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 "\<dots> = (if test x then while test do (do x) else x)"
- by(rule while_unfold)
- also have "\<dots> = (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 (\<lambda>(A, fA). A \<noteq> fA) (\<lambda>(A, fA). (fA, f fA)) ({}, f {}))"
-apply (rule_tac P = "\<lambda>(A, B). (A \<subseteq> U \<and> B = f A \<and> A \<subseteq> B \<and> B \<subseteq> lfp f)" and
- r = "((Pow U \<times> UNIV) \<times> (Pow U \<times> UNIV)) \<inter>
- 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 (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> 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 \<or> B n} = {f n | n. A n} \<union> {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
--- 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.
--- 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 "\<And>x y u v. \<lbrakk>x \<in> s; y \<in> s; 0 \<le> u; 0 \<le> v; u + v = 1\<rbrakk> \<Longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> 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 \<in> s" "y \<in> s" "0 \<le> u" "0 \<le> v" "u + v = (1::real)"
hence *:"u = 1 - v" "1 - v \<ge> 0" and **:"v = 1 - u" "1 - u \<ge> 0" by auto
{ fix a b assume "\<not> b \<le> 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 \<Longrightarrow> connected s"
using is_interval_convex convex_connected by auto
--- 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 "\<exists>x. x \<noteq> a")
+ case True then obtain x where x: "x \<noteq> a" ..
+ have "\<not> 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 "\<exists>d>0. \<forall>xa. 0 < dist xa x \<and> dist xa x < d \<longrightarrow>
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 "\<exists>s>0. \<forall>xa. xa \<noteq> 0 \<and> dist xa 0 < s \<longrightarrow> 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 \<in> s \<Longrightarrow> open s \<Longrightarrow> ((f has_derivative f') (at a within s) \<longleftrightarrow> (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 \<Longrightarrow> linear f" (* TODO: move elsewhere *)
proof -
@@ -272,7 +289,7 @@
lemma differentiable_within_open: assumes "a \<in> s" "open s" shows
"f differentiable (at a within s) \<longleftrightarrow> (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 \<Longrightarrow> (f differentiable_on s \<longleftrightarrow> (\<forall>x\<in>s. f differentiable at x))"
unfolding differentiable_on_def by(auto simp add: differentiable_within_open)
@@ -477,10 +494,12 @@
\<Longrightarrow> (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 \<Rightarrow> '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 \<Rightarrow> 'b::real_normed_vector"
+lemma frechet_derivative_unique_at:
shows "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f'') (at x) \<Longrightarrow> 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 \<Rightarrow> 'b::real_normed_vector"
+lemma frechet_derivative_at:
shows "(f has_derivative f') (at x) \<Longrightarrow> (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\<Rightarrow> 'n::euclidean_space"
- assumes "(f has_vector_derivative f') (at x)" "(f has_vector_derivative f'') (at x)" shows "f' = f''" proof-
- have *:"(\<lambda>x. x *\<^sub>R f') = (\<lambda>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' \<noteq> f''" moreover
- hence "(\<lambda>x. x *\<^sub>R f') = (\<lambda>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 "(\<lambda>x. x *\<^sub>R f') = (\<lambda>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 \<Rightarrow> 'n::ordered_euclidean_space"
assumes "a < b" "x \<in> {a..b}"
@@ -1260,8 +1282,8 @@
hence "(\<lambda>x. x *\<^sub>R f') 1 = (\<lambda>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 \<Rightarrow> 'a::euclidean_space" shows
- "(f has_vector_derivative f') (at x) \<Longrightarrow> vector_derivative f (at x) = f'"
+lemma vector_derivative_at:
+ shows "(f has_vector_derivative f') (at x) \<Longrightarrow> 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
--- 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
--- 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) \<longleftrightarrow>
+definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
(\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i<DIM('a). ((a$$i \<le> x$$i \<and> x$$i \<le> b$$i) \<or> (b$$i \<le> x$$i \<and> x$$i \<le> a$$i))) \<longrightarrow> x \<in> s)"
lemma is_interval_interval: "is_interval {a .. b::'a::ordered_euclidean_space}" (is ?th1)
--- 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.
--- 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
--- 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
--- 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.
*)
--- 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 "\<circ>>" 60)
-definition scomp :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl "o\<rightarrow>" 60) where
- "f o\<rightarrow> g = (\<lambda>x. split g (f x))"
+definition scomp :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl "\<circ>\<rightarrow>" 60) where
+ "f \<circ>\<rightarrow> g = (\<lambda>x. prod_case g (f x))"
lemma scomp_unfold: "scomp = (\<lambda>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\<rightarrow> g) x = split g (f x)"
- by (simp add: scomp_unfold split_def)
+lemma scomp_apply [simp]: "(f \<circ>\<rightarrow> g) x = prod_case g (f x)"
+ by (simp add: scomp_unfold prod_case_unfold)
-lemma Pair_scomp: "Pair x o\<rightarrow> f = f x"
+lemma Pair_scomp: "Pair x \<circ>\<rightarrow> f = f x"
by (simp add: expand_fun_eq scomp_apply)
-lemma scomp_Pair: "x o\<rightarrow> Pair = x"
+lemma scomp_Pair: "x \<circ>\<rightarrow> Pair = x"
by (simp add: expand_fun_eq scomp_apply)
-lemma scomp_scomp: "(f o\<rightarrow> g) o\<rightarrow> h = f o\<rightarrow> (\<lambda>x. g x o\<rightarrow> h)"
+lemma scomp_scomp: "(f \<circ>\<rightarrow> g) \<circ>\<rightarrow> h = f \<circ>\<rightarrow> (\<lambda>x. g x \<circ>\<rightarrow> h)"
by (simp add: expand_fun_eq scomp_unfold)
-lemma scomp_fcomp: "(f o\<rightarrow> g) o> h = f o\<rightarrow> (\<lambda>x. g x o> h)"
+lemma scomp_fcomp: "(f \<circ>\<rightarrow> g) \<circ>> h = f \<circ>\<rightarrow> (\<lambda>x. g x \<circ>> h)"
by (simp add: expand_fun_eq scomp_unfold fcomp_def)
-lemma fcomp_scomp: "(f o> g) o\<rightarrow> h = f o> (g o\<rightarrow> h)"
+lemma fcomp_scomp: "(f \<circ>> g) \<circ>\<rightarrow> h = f \<circ>> (g \<circ>\<rightarrow> 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\<rightarrow>" 60)
+no_notation fcomp (infixl "\<circ>>" 60)
+no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
text {*
@{term prod_fun} --- action of the product functor upon
--- 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\<rightarrow>" 60)
+notation fcomp (infixl "\<circ>>" 60)
+notation scomp (infixl "\<circ>\<rightarrow>" 60)
subsection {* The @{text random} class *}
@@ -23,7 +23,7 @@
begin
definition
- "random i = Random.range 2 o\<rightarrow>
+ "random i = Random.range 2 \<circ>\<rightarrow>
(\<lambda>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\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Evaluation.term_of c))"
+ "random _ = Random.select chars \<circ>\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Evaluation.term_of c))"
instance ..
@@ -64,7 +64,7 @@
begin
definition random_nat :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed" where
- "random_nat i = Random.range (i + 1) o\<rightarrow> (\<lambda>k. Pair (
+ "random_nat i = Random.range (i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
let n = Code_Numeral.nat_of k
in (n, \<lambda>_. Code_Evaluation.term_of n)))"
@@ -76,7 +76,7 @@
begin
definition
- "random i = Random.range (2 * i + 1) o\<rightarrow> (\<lambda>k. Pair (
+ "random i = Random.range (2 * i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
let j = (if k \<ge> i then Code_Numeral.int_of (k - i) else - Code_Numeral.int_of (i - k))
in (j, \<lambda>_. Code_Evaluation.term_of j)))"
@@ -110,7 +110,7 @@
text {* Towards type copies and datatypes *}
definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
- "collapse f = (f o\<rightarrow> id)"
+ "collapse f = (f \<circ>\<rightarrow> id)"
definition beyond :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> 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\<rightarrow>" 60)
+no_notation fcomp (infixl "\<circ>>" 60)
+no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
subsection {* The Random-Predicate Monad *}
--- 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\<rightarrow>" 60)
+notation fcomp (infixl "\<circ>>" 60)
+notation scomp (infixl "\<circ>\<rightarrow>" 60)
subsection {* Auxiliary functions *}
@@ -48,12 +48,12 @@
subsection {* Base selectors *}
fun iterate :: "code_numeral \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
- "iterate k f x = (if k = 0 then Pair x else f x o\<rightarrow> iterate (k - 1) f)"
+ "iterate k f x = (if k = 0 then Pair x else f x \<circ>\<rightarrow> iterate (k - 1) f)"
definition range :: "code_numeral \<Rightarrow> seed \<Rightarrow> code_numeral \<times> seed" where
"range k = iterate (log 2147483561 k)
- (\<lambda>l. next o\<rightarrow> (\<lambda>v. Pair (v + l * 2147483561))) 1
- o\<rightarrow> (\<lambda>v. Pair (v mod k))"
+ (\<lambda>l. next \<circ>\<rightarrow> (\<lambda>v. Pair (v + l * 2147483561))) 1
+ \<circ>\<rightarrow> (\<lambda>v. Pair (v mod k))"
lemma range:
"k > 0 \<Longrightarrow> fst (range k s) < k"
@@ -61,7 +61,7 @@
definition select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
"select xs = range (Code_Numeral.of_nat (length xs))
- o\<rightarrow> (\<lambda>k. Pair (nth xs (Code_Numeral.nat_of k)))"
+ \<circ>\<rightarrow> (\<lambda>k. Pair (nth xs (Code_Numeral.nat_of k)))"
lemma select:
assumes "xs \<noteq> []"
@@ -97,7 +97,7 @@
definition select_weight :: "(code_numeral \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
"select_weight xs = range (listsum (map fst xs))
- o\<rightarrow> (\<lambda>k. Pair (pick xs k))"
+ \<circ>\<rightarrow> (\<lambda>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\<rightarrow>" 60)
+no_notation fcomp (infixl "\<circ>>" 60)
+no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
end
--- 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 \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> rat \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
[code_unfold]: "valterm_fract k l = Code_Evaluation.valtermify Fract {\<cdot>} k {\<cdot>} l"
-notation fcomp (infixl "o>" 60)
-notation scomp (infixl "o\<rightarrow>" 60)
+notation fcomp (infixl "\<circ>>" 60)
+notation scomp (infixl "\<circ>\<rightarrow>" 60)
instantiation rat :: random
begin
definition
- "Quickcheck.random i = Quickcheck.random i o\<rightarrow> (\<lambda>num. Random.range i o\<rightarrow> (\<lambda>denom. Pair (
+ "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>num. Random.range i \<circ>\<rightarrow> (\<lambda>denom. Pair (
let j = Code_Numeral.int_of (denom + 1)
in valterm_fract num (j, \<lambda>u. Code_Evaluation.term_of j))))"
@@ -1129,8 +1129,8 @@
end
-no_notation fcomp (infixl "o>" 60)
-no_notation scomp (infixl "o\<rightarrow>" 60)
+no_notation fcomp (infixl "\<circ>>" 60)
+no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
text {* Setup for SML code generator *}
--- 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 \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
[code_unfold]: "valterm_ratreal k = Code_Evaluation.valtermify Ratreal {\<cdot>} k"
-notation fcomp (infixl "o>" 60)
-notation scomp (infixl "o\<rightarrow>" 60)
+notation fcomp (infixl "\<circ>>" 60)
+notation scomp (infixl "\<circ>\<rightarrow>" 60)
instantiation real :: random
begin
definition
- "Quickcheck.random i = Quickcheck.random i o\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))"
+ "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))"
instance ..
end
-no_notation fcomp (infixl "o>" 60)
-no_notation scomp (infixl "o\<rightarrow>" 60)
+no_notation fcomp (infixl "\<circ>>" 60)
+no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
text {* Setup for SML code generator *}
--- 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
--- 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.
--- 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.
--- 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.
--- 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.
--- 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.
--- 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
--- 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
--- 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.
--- 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.
*)
--- 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
*)
--- 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.
--- 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;
--- 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;
--- 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.
*)
--- 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.
*)
--- 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.
--- 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
--- 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.
*)
--- 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.
*)
--- 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\<rightarrow>" 60)
+notation fcomp (infixl "\<circ>>" 60)
+notation scomp (infixl "\<circ>\<rightarrow>" 60)
instantiation word :: ("{len0, typerep}") random
begin
definition
- "random_word i = Random.range (max i (2 ^ len_of TYPE('a))) o\<rightarrow> (\<lambda>k. Pair (
+ "random_word i = Random.range (max i (2 ^ len_of TYPE('a))) \<circ>\<rightarrow> (\<lambda>k. Pair (
let j = word_of_int (Code_Numeral.int_of k) :: 'a word
in (j, \<lambda>_::unit. Code_Evaluation.term_of j)))"
@@ -41,8 +41,8 @@
end
-no_notation fcomp (infixl "o>" 60)
-no_notation scomp (infixl "o\<rightarrow>" 60)
+no_notation fcomp (infixl "\<circ>>" 60)
+no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
subsection {* Type conversions and casting *}
--- 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",
--- /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 (\<lambda>(A, fA). A \<noteq> fA) (\<lambda>(A, fA). (fA, f fA)) ({}, f {}))"
+apply (rule_tac P = "\<lambda>(A, B). (A \<subseteq> U \<and> B = f A \<and> A \<subseteq> B \<and> B \<subseteq> lfp f)" and
+ r = "((Pow U \<times> UNIV) \<times> (Pow U \<times> UNIV)) \<inter>
+ 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 (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> 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 \<or> B n} = {f n | n. A n} \<union> {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
--- 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
--- 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.
--- 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
--- 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.
*)
--- 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.
*)
--- 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
*)
(*
--- 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);
--- 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.
--- 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 =
--- 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 =
--- 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
--- 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.
--- 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 =
--- 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.
--- 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));
--- 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.
--- 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) \
+ "")
--- 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
--- 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 =>
--- 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.