--- a/Admin/isatest/isatest-makedist Thu Jul 02 16:06:12 2009 +0200
+++ b/Admin/isatest/isatest-makedist Thu Jul 02 18:32:28 2009 +0200
@@ -106,7 +106,7 @@
sleep 15
$SSH atbroy101 "$MAKEALL $HOME/settings/at64-poly"
sleep 15
-$SSH macbroy2 "$MAKEALL $HOME/settings/mac-poly-M4; $MAKEALL $HOME/settings/mac-poly-M8"
+$SSH macbroy2 "$MAKEALL $HOME/settings/mac-poly-M4; $MAKEALL $HOME/settings/mac-poly-M8; $MAKEALL $HOME/settings/mac-poly64-M4"
sleep 15
$SSH macbroy5 "$MAKEALL $HOME/settings/mac-poly"
sleep 15
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isatest/settings/mac-poly64-M4 Thu Jul 02 18:32:28 2009 +0200
@@ -0,0 +1,28 @@
+# -*- shell-script -*- :mode=shellscript:
+
+ POLYML_HOME="/home/polyml/polyml-svn"
+ ML_SYSTEM="polyml-experimental"
+ ML_PLATFORM="x86_64-darwin"
+ ML_HOME="$POLYML_HOME/$ML_PLATFORM"
+ ML_OPTIONS="--mutable 2000 --immutable 2000"
+
+
+ISABELLE_HOME_USER=~/isabelle-mac-poly64-M4
+
+# Where to look for isabelle tools (multiple dirs separated by ':').
+ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
+
+# Location for temporary files (should be on a local file system).
+ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
+
+
+# Heap input locations. ML system identifier is included in lookup.
+ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
+
+# Heap output location. ML system identifier is appended automatically later on.
+ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
+ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
+
+ISABELLE_USEDIR_OPTIONS="-i false -d false -M 4"
+
+HOL_USEDIR_OPTIONS="-p 2 -Q false"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/launch4j/README Thu Jul 02 18:32:28 2009 +0200
@@ -0,0 +1,5 @@
+Cross-platform Java executable wrapper
+======================================
+
+* http://launch4j.sourceforge.net
+
Binary file Admin/launch4j/isabelle.ico has changed
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/launch4j/isabelle.xml Thu Jul 02 18:32:28 2009 +0200
@@ -0,0 +1,23 @@
+<launch4jConfig>
+ <dontWrapJar>true</dontWrapJar>
+ <headerType>gui</headerType>
+ <jar>lib/classes/isabelle-scala.jar</jar>
+ <outfile>Isabelle.exe</outfile>
+ <errTitle></errTitle>
+ <cmdLine></cmdLine>
+ <chdir></chdir>
+ <priority>normal</priority>
+ <downloadUrl>http://java.com/download</downloadUrl>
+ <supportUrl></supportUrl>
+ <customProcName>false</customProcName>
+ <stayAlive>false</stayAlive>
+ <manifest></manifest>
+ <icon>isabelle.ico</icon>
+ <jre>
+ <path></path>
+ <minVersion>1.6.0</minVersion>
+ <maxVersion></maxVersion>
+ <jdkPreference>preferJre</jdkPreference>
+ <opt>-Disabelle.home="%EXEDIR%"</opt>
+ </jre>
+</launch4jConfig>
\ No newline at end of file
--- a/NEWS Thu Jul 02 16:06:12 2009 +0200
+++ b/NEWS Thu Jul 02 18:32:28 2009 +0200
@@ -73,8 +73,16 @@
approximation method.
* "approximate" supports now arithmetic expressions as boundaries of intervals and implements
-interval splitting.
-
+interval splitting and taylor series expansion.
+
+* Changed DERIV_intros to a NamedThmsFun. Each of the theorems in DERIV_intros
+assumes composition with an additional function and matches a variable to the
+derivative, which has to be solved by the simplifier. Hence
+(auto intro!: DERIV_intros) computes the derivative of most elementary terms.
+
+* Maclauren.DERIV_tac and Maclauren.deriv_tac was removed, they are replaced by:
+(auto intro!: DERIV_intros)
+INCOMPATIBILITY.
*** ML ***
--- a/doc-src/Codegen/Thy/document/Introduction.tex Thu Jul 02 16:06:12 2009 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Thu Jul 02 18:32:28 2009 +0200
@@ -249,9 +249,9 @@
\hspace*{0pt}dequeue (AQueue [] []) = (Nothing,~AQueue [] []);\\
\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
\hspace*{0pt}dequeue (AQueue (v :~va) []) =\\
-\hspace*{0pt} ~(let {\char123}\\
+\hspace*{0pt} ~let {\char123}\\
\hspace*{0pt} ~~~(y :~ys) = rev (v :~va);\\
-\hspace*{0pt} ~{\char125}~in (Just y,~AQueue [] ys) );\\
+\hspace*{0pt} ~{\char125}~in (Just y,~AQueue [] ys);\\
\hspace*{0pt}\\
\hspace*{0pt}enqueue ::~forall a.~a -> Queue a -> Queue a;\\
\hspace*{0pt}enqueue x (AQueue xs ys) = AQueue (x :~xs) ys;\\
--- a/doc-src/Codegen/Thy/document/Program.tex Thu Jul 02 16:06:12 2009 +0200
+++ b/doc-src/Codegen/Thy/document/Program.tex Thu Jul 02 18:32:28 2009 +0200
@@ -966,9 +966,9 @@
\noindent%
\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
-\hspace*{0pt} ~(let {\char123}\\
+\hspace*{0pt} ~let {\char123}\\
\hspace*{0pt} ~~~(y :~ys) = rev xs;\\
-\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys) );\\
+\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\
\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/Codegen/Thy/examples/Example.hs Thu Jul 02 16:06:12 2009 +0200
+++ b/doc-src/Codegen/Thy/examples/Example.hs Thu Jul 02 18:32:28 2009 +0200
@@ -23,9 +23,9 @@
dequeue (AQueue [] []) = (Nothing, AQueue [] []);
dequeue (AQueue xs (y : ys)) = (Just y, AQueue xs ys);
dequeue (AQueue (v : va) []) =
- (let {
+ let {
(y : ys) = rev (v : va);
- } in (Just y, AQueue [] ys) );
+ } in (Just y, AQueue [] ys);
enqueue :: forall a. a -> Queue a -> Queue a;
enqueue x (AQueue xs ys) = AQueue (x : xs) ys;
--- a/src/HOL/Decision_Procs/Approximation.thy Thu Jul 02 16:06:12 2009 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Thu Jul 02 18:32:28 2009 +0200
@@ -2069,8 +2069,7 @@
| Atom nat
| Num float
-fun interpret_floatarith :: "floatarith \<Rightarrow> real list \<Rightarrow> real"
-where
+fun interpret_floatarith :: "floatarith \<Rightarrow> real list \<Rightarrow> real" where
"interpret_floatarith (Add a b) vs = (interpret_floatarith a vs) + (interpret_floatarith b vs)" |
"interpret_floatarith (Minus a) vs = - (interpret_floatarith a vs)" |
"interpret_floatarith (Mult a b) vs = (interpret_floatarith a vs) * (interpret_floatarith b vs)" |
@@ -2117,7 +2116,6 @@
and "interpret_floatarith (Num (Float 1 0)) vs = 1"
and "interpret_floatarith (Num (Float (number_of a) 0)) vs = number_of a" by auto
-
subsection "Implement approximation function"
fun lift_bin' :: "(float * float) option \<Rightarrow> (float * float) option \<Rightarrow> (float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> (float * float)) \<Rightarrow> (float * float) option" where
@@ -2632,6 +2630,560 @@
shows "interpret_form f xs"
using approx_form_aux[OF _ bounded_by_None] assms by auto
+subsection {* Implementing Taylor series expansion *}
+
+fun isDERIV :: "nat \<Rightarrow> floatarith \<Rightarrow> real list \<Rightarrow> bool" where
+"isDERIV x (Add a b) vs = (isDERIV x a vs \<and> isDERIV x b vs)" |
+"isDERIV x (Mult a b) vs = (isDERIV x a vs \<and> isDERIV x b vs)" |
+"isDERIV x (Minus a) vs = isDERIV x a vs" |
+"isDERIV x (Inverse a) vs = (isDERIV x a vs \<and> interpret_floatarith a vs \<noteq> 0)" |
+"isDERIV x (Cos a) vs = isDERIV x a vs" |
+"isDERIV x (Arctan a) vs = isDERIV x a vs" |
+"isDERIV x (Min a b) vs = False" |
+"isDERIV x (Max a b) vs = False" |
+"isDERIV x (Abs a) vs = False" |
+"isDERIV x Pi vs = True" |
+"isDERIV x (Sqrt a) vs = (isDERIV x a vs \<and> interpret_floatarith a vs > 0)" |
+"isDERIV x (Exp a) vs = isDERIV x a vs" |
+"isDERIV x (Ln a) vs = (isDERIV x a vs \<and> interpret_floatarith a vs > 0)" |
+"isDERIV x (Power a 0) vs = True" |
+"isDERIV x (Power a (Suc n)) vs = isDERIV x a vs" |
+"isDERIV x (Num f) vs = True" |
+"isDERIV x (Atom n) vs = True"
+
+fun DERIV_floatarith :: "nat \<Rightarrow> floatarith \<Rightarrow> floatarith" where
+"DERIV_floatarith x (Add a b) = Add (DERIV_floatarith x a) (DERIV_floatarith x b)" |
+"DERIV_floatarith x (Mult a b) = Add (Mult a (DERIV_floatarith x b)) (Mult (DERIV_floatarith x a) b)" |
+"DERIV_floatarith x (Minus a) = Minus (DERIV_floatarith x a)" |
+"DERIV_floatarith x (Inverse a) = Minus (Mult (DERIV_floatarith x a) (Inverse (Power a 2)))" |
+"DERIV_floatarith x (Cos a) = Minus (Mult (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) (DERIV_floatarith x a))" |
+"DERIV_floatarith x (Arctan a) = Mult (Inverse (Add (Num 1) (Power a 2))) (DERIV_floatarith x a)" |
+"DERIV_floatarith x (Min a b) = Num 0" |
+"DERIV_floatarith x (Max a b) = Num 0" |
+"DERIV_floatarith x (Abs a) = Num 0" |
+"DERIV_floatarith x Pi = Num 0" |
+"DERIV_floatarith x (Sqrt a) = (Mult (Inverse (Mult (Sqrt a) (Num 2))) (DERIV_floatarith x a))" |
+"DERIV_floatarith x (Exp a) = Mult (Exp a) (DERIV_floatarith x a)" |
+"DERIV_floatarith x (Ln a) = Mult (Inverse a) (DERIV_floatarith x a)" |
+"DERIV_floatarith x (Power a 0) = Num 0" |
+"DERIV_floatarith x (Power a (Suc n)) = Mult (Num (Float (int (Suc n)) 0)) (Mult (Power a n) (DERIV_floatarith x a))" |
+"DERIV_floatarith x (Num f) = Num 0" |
+"DERIV_floatarith x (Atom n) = (if x = n then Num 1 else Num 0)"
+
+lemma DERIV_floatarith:
+ assumes "n < length vs"
+ assumes isDERIV: "isDERIV n f (vs[n := x])"
+ shows "DERIV (\<lambda> x'. interpret_floatarith f (vs[n := x'])) x :>
+ interpret_floatarith (DERIV_floatarith n f) (vs[n := x])"
+ (is "DERIV (?i f) x :> _")
+using isDERIV proof (induct f arbitrary: x)
+ case (Inverse a) thus ?case
+ by (auto intro!: DERIV_intros
+ simp add: algebra_simps power2_eq_square)
+next case (Cos a) thus ?case
+ by (auto intro!: DERIV_intros
+ simp del: interpret_floatarith.simps(5)
+ simp add: interpret_floatarith_sin interpret_floatarith.simps(5)[of a])
+next case (Power a n) thus ?case
+ by (cases n, auto intro!: DERIV_intros
+ simp del: power_Suc simp add: real_eq_of_nat)
+next case (Ln a) thus ?case
+ by (auto intro!: DERIV_intros simp add: divide_inverse)
+next case (Atom i) thus ?case using `n < length vs` by auto
+qed (auto intro!: DERIV_intros)
+
+declare approx.simps[simp del]
+
+fun isDERIV_approx :: "nat \<Rightarrow> nat \<Rightarrow> floatarith \<Rightarrow> (float * float) option list \<Rightarrow> bool" where
+"isDERIV_approx prec x (Add a b) vs = (isDERIV_approx prec x a vs \<and> isDERIV_approx prec x b vs)" |
+"isDERIV_approx prec x (Mult a b) vs = (isDERIV_approx prec x a vs \<and> isDERIV_approx prec x b vs)" |
+"isDERIV_approx prec x (Minus a) vs = isDERIV_approx prec x a vs" |
+"isDERIV_approx prec x (Inverse a) vs =
+ (isDERIV_approx prec x a vs \<and> (case approx prec a vs of Some (l, u) \<Rightarrow> 0 < l \<or> u < 0 | None \<Rightarrow> False))" |
+"isDERIV_approx prec x (Cos a) vs = isDERIV_approx prec x a vs" |
+"isDERIV_approx prec x (Arctan a) vs = isDERIV_approx prec x a vs" |
+"isDERIV_approx prec x (Min a b) vs = False" |
+"isDERIV_approx prec x (Max a b) vs = False" |
+"isDERIV_approx prec x (Abs a) vs = False" |
+"isDERIV_approx prec x Pi vs = True" |
+"isDERIV_approx prec x (Sqrt a) vs =
+ (isDERIV_approx prec x a vs \<and> (case approx prec a vs of Some (l, u) \<Rightarrow> 0 < l | None \<Rightarrow> False))" |
+"isDERIV_approx prec x (Exp a) vs = isDERIV_approx prec x a vs" |
+"isDERIV_approx prec x (Ln a) vs =
+ (isDERIV_approx prec x a vs \<and> (case approx prec a vs of Some (l, u) \<Rightarrow> 0 < l | None \<Rightarrow> False))" |
+"isDERIV_approx prec x (Power a 0) vs = True" |
+"isDERIV_approx prec x (Power a (Suc n)) vs = isDERIV_approx prec x a vs" |
+"isDERIV_approx prec x (Num f) vs = True" |
+"isDERIV_approx prec x (Atom n) vs = True"
+
+lemma isDERIV_approx:
+ assumes "bounded_by xs vs"
+ and isDERIV_approx: "isDERIV_approx prec x f vs"
+ shows "isDERIV x f xs"
+using isDERIV_approx proof (induct f)
+ case (Inverse a)
+ then obtain l u where approx_Some: "Some (l, u) = approx prec a vs"
+ and *: "0 < l \<or> u < 0"
+ by (cases "approx prec a vs", auto)
+ with approx[OF `bounded_by xs vs` approx_Some]
+ have "interpret_floatarith a xs \<noteq> 0" unfolding less_float_def by auto
+ thus ?case using Inverse by auto
+next
+ case (Ln a)
+ then obtain l u where approx_Some: "Some (l, u) = approx prec a vs"
+ and *: "0 < l"
+ by (cases "approx prec a vs", auto)
+ with approx[OF `bounded_by xs vs` approx_Some]
+ have "0 < interpret_floatarith a xs" unfolding less_float_def by auto
+ thus ?case using Ln by auto
+next
+ case (Sqrt a)
+ then obtain l u where approx_Some: "Some (l, u) = approx prec a vs"
+ and *: "0 < l"
+ by (cases "approx prec a vs", auto)
+ with approx[OF `bounded_by xs vs` approx_Some]
+ have "0 < interpret_floatarith a xs" unfolding less_float_def by auto
+ thus ?case using Sqrt by auto
+next
+ case (Power a n) thus ?case by (cases n, auto)
+qed auto
+
+lemma bounded_by_update_var:
+ assumes "bounded_by xs vs" and "vs ! i = Some (l, u)"
+ and bnd: "x \<in> { real l .. real u }"
+ shows "bounded_by (xs[i := x]) vs"
+proof (cases "i < length xs")
+ case False thus ?thesis using `bounded_by xs vs` by auto
+next
+ let ?xs = "xs[i := x]"
+ case True hence "i < length ?xs" by auto
+{ fix j
+ assume "j < length vs"
+ have "case vs ! j of None \<Rightarrow> True | Some (l, u) \<Rightarrow> ?xs ! j \<in> { real l .. real u }"
+ proof (cases "vs ! j")
+ case (Some b)
+ thus ?thesis
+ proof (cases "i = j")
+ case True
+ thus ?thesis using `vs ! i = Some (l, u)` Some and bnd `i < length ?xs`
+ by auto
+ next
+ case False
+ thus ?thesis using `bounded_by xs vs`[THEN bounded_byE, OF `j < length vs`] Some
+ by auto
+ qed
+ qed auto }
+ thus ?thesis unfolding bounded_by_def by auto
+qed
+
+lemma isDERIV_approx':
+ assumes "bounded_by xs vs"
+ and vs_x: "vs ! x = Some (l, u)" and X_in: "X \<in> { real l .. real u }"
+ and approx: "isDERIV_approx prec x f vs"
+ shows "isDERIV x f (xs[x := X])"
+proof -
+ note bounded_by_update_var[OF `bounded_by xs vs` vs_x X_in] approx
+ thus ?thesis by (rule isDERIV_approx)
+qed
+
+lemma DERIV_approx:
+ assumes "n < length xs" and bnd: "bounded_by xs vs"
+ and isD: "isDERIV_approx prec n f vs"
+ and app: "Some (l, u) = approx prec (DERIV_floatarith n f) vs" (is "_ = approx _ ?D _")
+ shows "\<exists>x. real l \<le> x \<and> x \<le> real u \<and>
+ DERIV (\<lambda> x. interpret_floatarith f (xs[n := x])) (xs!n) :> x"
+ (is "\<exists> x. _ \<and> _ \<and> DERIV (?i f) _ :> _")
+proof (rule exI[of _ "?i ?D (xs!n)"], rule conjI[OF _ conjI])
+ let "?i f x" = "interpret_floatarith f (xs[n := x])"
+ from approx[OF bnd app]
+ show "real l \<le> ?i ?D (xs!n)" and "?i ?D (xs!n) \<le> real u"
+ using `n < length xs` by auto
+ from DERIV_floatarith[OF `n < length xs`, of f "xs!n"] isDERIV_approx[OF bnd isD]
+ show "DERIV (?i f) (xs!n) :> (?i ?D (xs!n))" by simp
+qed
+
+fun lift_bin :: "(float * float) option \<Rightarrow> (float * float) option \<Rightarrow> (float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> (float * float) option) \<Rightarrow> (float * float) option" where
+"lift_bin (Some (l1, u1)) (Some (l2, u2)) f = f l1 u1 l2 u2" |
+"lift_bin a b f = None"
+
+lemma lift_bin:
+ assumes lift_bin_Some: "Some (l, u) = lift_bin a b f"
+ obtains l1 u1 l2 u2
+ where "a = Some (l1, u1)"
+ and "b = Some (l2, u2)"
+ and "f l1 u1 l2 u2 = Some (l, u)"
+using assms by (cases a, simp, cases b, simp, auto)
+
+fun approx_tse where
+"approx_tse prec n 0 c k f bs = approx prec f bs" |
+"approx_tse prec n (Suc s) c k f bs =
+ (if isDERIV_approx prec n f bs then
+ lift_bin (approx prec f (bs[n := Some (c,c)]))
+ (approx_tse prec n s c (Suc k) (DERIV_floatarith n f) bs)
+ (\<lambda> l1 u1 l2 u2. approx prec
+ (Add (Atom 0)
+ (Mult (Inverse (Num (Float (int k) 0)))
+ (Mult (Add (Atom (Suc (Suc 0))) (Minus (Num c)))
+ (Atom (Suc 0))))) [Some (l1, u1), Some (l2, u2), bs!n])
+ else approx prec f bs)"
+
+lemma bounded_by_Cons:
+ assumes bnd: "bounded_by xs vs"
+ and x: "x \<in> { real l .. real u }"
+ shows "bounded_by (x#xs) ((Some (l, u))#vs)"
+proof -
+ { fix i assume *: "i < length ((Some (l, u))#vs)"
+ have "case ((Some (l,u))#vs) ! i of Some (l, u) \<Rightarrow> (x#xs)!i \<in> { real l .. real u } | None \<Rightarrow> True"
+ proof (cases i)
+ case 0 with x show ?thesis by auto
+ next
+ case (Suc i) with * have "i < length vs" by auto
+ from bnd[THEN bounded_byE, OF this]
+ show ?thesis unfolding Suc nth_Cons_Suc .
+ qed }
+ thus ?thesis by (auto simp add: bounded_by_def)
+qed
+
+lemma approx_tse_generic:
+ assumes "bounded_by xs vs"
+ and bnd_c: "bounded_by (xs[x := real c]) vs" and "x < length vs" and "x < length xs"
+ and bnd_x: "vs ! x = Some (lx, ux)"
+ and ate: "Some (l, u) = approx_tse prec x s c k f vs"
+ shows "\<exists> n. (\<forall> m < n. \<forall> z \<in> {real lx .. real ux}.
+ DERIV (\<lambda> y. interpret_floatarith ((DERIV_floatarith x ^^ m) f) (xs[x := y])) z :>
+ (interpret_floatarith ((DERIV_floatarith x ^^ (Suc m)) f) (xs[x := z])))
+ \<and> (\<forall> t \<in> {real lx .. real ux}. (\<Sum> i = 0..<n. inverse (real (\<Prod> j \<in> {k..<k+i}. j)) *
+ interpret_floatarith ((DERIV_floatarith x ^^ i) f) (xs[x := real c]) *
+ (xs!x - real c)^i) +
+ inverse (real (\<Prod> j \<in> {k..<k+n}. j)) *
+ interpret_floatarith ((DERIV_floatarith x ^^ n) f) (xs[x := t]) *
+ (xs!x - real c)^n \<in> {real l .. real u})" (is "\<exists> n. ?taylor f k l u n")
+using ate proof (induct s arbitrary: k f l u)
+ case 0
+ { fix t assume "t \<in> {real lx .. real ux}"
+ note bounded_by_update_var[OF `bounded_by xs vs` bnd_x this]
+ from approx[OF this 0[unfolded approx_tse.simps]]
+ have "(interpret_floatarith f (xs[x := t])) \<in> {real l .. real u}"
+ by (auto simp add: algebra_simps)
+ } thus ?case by (auto intro!: exI[of _ 0])
+next
+ case (Suc s)
+ show ?case
+ proof (cases "isDERIV_approx prec x f vs")
+ case False
+ note ap = Suc.prems[unfolded approx_tse.simps if_not_P[OF False]]
+
+ { fix t assume "t \<in> {real lx .. real ux}"
+ note bounded_by_update_var[OF `bounded_by xs vs` bnd_x this]
+ from approx[OF this ap]
+ have "(interpret_floatarith f (xs[x := t])) \<in> {real l .. real u}"
+ by (auto simp add: algebra_simps)
+ } thus ?thesis by (auto intro!: exI[of _ 0])
+ next
+ case True
+ with Suc.prems
+ obtain l1 u1 l2 u2
+ where a: "Some (l1, u1) = approx prec f (vs[x := Some (c,c)])"
+ and ate: "Some (l2, u2) = approx_tse prec x s c (Suc k) (DERIV_floatarith x f) vs"
+ and final: "Some (l, u) = approx prec
+ (Add (Atom 0)
+ (Mult (Inverse (Num (Float (int k) 0)))
+ (Mult (Add (Atom (Suc (Suc 0))) (Minus (Num c)))
+ (Atom (Suc 0))))) [Some (l1, u1), Some (l2, u2), vs!x]"
+ by (auto elim!: lift_bin) blast
+
+ from bnd_c `x < length xs`
+ have bnd: "bounded_by (xs[x:=real c]) (vs[x:= Some (c,c)])"
+ by (auto intro!: bounded_by_update)
+
+ from approx[OF this a]
+ have f_c: "interpret_floatarith ((DERIV_floatarith x ^^ 0) f) (xs[x := real c]) \<in> { real l1 .. real u1 }"
+ (is "?f 0 (real c) \<in> _")
+ by auto
+
+ { fix f :: "'a \<Rightarrow> 'a" fix n :: nat fix x :: 'a
+ have "(f ^^ Suc n) x = (f ^^ n) (f x)"
+ by (induct n, auto) }
+ note funpow_Suc = this[symmetric]
+ from Suc.hyps[OF ate, unfolded this]
+ obtain n
+ where DERIV_hyp: "\<And> m z. \<lbrakk> m < n ; z \<in> { real lx .. real ux } \<rbrakk> \<Longrightarrow> DERIV (?f (Suc m)) z :> ?f (Suc (Suc m)) z"
+ and hyp: "\<forall> t \<in> {real lx .. real ux}. (\<Sum> i = 0..<n. inverse (real (\<Prod> j \<in> {Suc k..<Suc k + i}. j)) * ?f (Suc i) (real c) * (xs!x - real c)^i) +
+ inverse (real (\<Prod> j \<in> {Suc k..<Suc k + n}. j)) * ?f (Suc n) t * (xs!x - real c)^n \<in> {real l2 .. real u2}"
+ (is "\<forall> t \<in> _. ?X (Suc k) f n t \<in> _")
+ by blast
+
+ { fix m z
+ assume "m < Suc n" and bnd_z: "z \<in> { real lx .. real ux }"
+ have "DERIV (?f m) z :> ?f (Suc m) z"
+ proof (cases m)
+ case 0
+ with DERIV_floatarith[OF `x < length xs` isDERIV_approx'[OF `bounded_by xs vs` bnd_x bnd_z True]]
+ show ?thesis by simp
+ next
+ case (Suc m')
+ hence "m' < n" using `m < Suc n` by auto
+ from DERIV_hyp[OF this bnd_z]
+ show ?thesis using Suc by simp
+ qed } note DERIV = this
+
+ have "\<And> k i. k < i \<Longrightarrow> {k ..< i} = insert k {Suc k ..< i}" by auto
+ hence setprod_head_Suc: "\<And> k i. \<Prod> {k ..< k + Suc i} = k * \<Prod> {Suc k ..< Suc k + i}" by auto
+ have setsum_move0: "\<And> k F. setsum F {0..<Suc k} = F 0 + setsum (\<lambda> k. F (Suc k)) {0..<k}"
+ unfolding setsum_shift_bounds_Suc_ivl[symmetric]
+ unfolding setsum_head_upt_Suc[OF zero_less_Suc] ..
+ def C \<equiv> "xs!x - real c"
+
+ { fix t assume t: "t \<in> {real lx .. real ux}"
+ hence "bounded_by [xs!x] [vs!x]"
+ using `bounded_by xs vs`[THEN bounded_byE, OF `x < length vs`]
+ by (cases "vs!x", auto simp add: bounded_by_def)
+
+ with hyp[THEN bspec, OF t] f_c
+ have "bounded_by [?f 0 (real c), ?X (Suc k) f n t, xs!x] [Some (l1, u1), Some (l2, u2), vs!x]"
+ by (auto intro!: bounded_by_Cons)
+ from approx[OF this final, unfolded atLeastAtMost_iff[symmetric]]
+ have "?X (Suc k) f n t * (xs!x - real c) * inverse (real k) + ?f 0 (real c) \<in> {real l .. real u}"
+ by (auto simp add: algebra_simps)
+ also have "?X (Suc k) f n t * (xs!x - real c) * inverse (real k) + ?f 0 (real c) =
+ (\<Sum> i = 0..<Suc n. inverse (real (\<Prod> j \<in> {k..<k+i}. j)) * ?f i (real c) * (xs!x - real c)^i) +
+ inverse (real (\<Prod> j \<in> {k..<k+Suc n}. j)) * ?f (Suc n) t * (xs!x - real c)^Suc n" (is "_ = ?T")
+ unfolding funpow_Suc C_def[symmetric] setsum_move0 setprod_head_Suc
+ by (auto simp add: algebra_simps setsum_right_distrib[symmetric])
+ finally have "?T \<in> {real l .. real u}" . }
+ thus ?thesis using DERIV by blast
+ qed
+qed
+
+lemma setprod_fact: "\<Prod> {1..<1 + k} = fact (k :: nat)"
+proof (induct k)
+ case (Suc k)
+ have "{ 1 ..< Suc (Suc k) } = insert (Suc k) { 1 ..< Suc k }" by auto
+ hence "\<Prod> { 1 ..< Suc (Suc k) } = (Suc k) * \<Prod> { 1 ..< Suc k }" by auto
+ thus ?case using Suc by auto
+qed simp
+
+lemma approx_tse:
+ assumes "bounded_by xs vs"
+ and bnd_x: "vs ! x = Some (lx, ux)" and bnd_c: "real c \<in> {real lx .. real ux}"
+ and "x < length vs" and "x < length xs"
+ and ate: "Some (l, u) = approx_tse prec x s c 1 f vs"
+ shows "interpret_floatarith f xs \<in> { real l .. real u }"
+proof -
+ def F \<equiv> "\<lambda> n z. interpret_floatarith ((DERIV_floatarith x ^^ n) f) (xs[x := z])"
+ hence F0: "F 0 = (\<lambda> z. interpret_floatarith f (xs[x := z]))" by auto
+
+ hence "bounded_by (xs[x := real c]) vs" and "x < length vs" "x < length xs"
+ using `bounded_by xs vs` bnd_x bnd_c `x < length vs` `x < length xs`
+ by (auto intro!: bounded_by_update_var)
+
+ from approx_tse_generic[OF `bounded_by xs vs` this bnd_x ate]
+ obtain n
+ where DERIV: "\<forall> m z. m < n \<and> real lx \<le> z \<and> z \<le> real ux \<longrightarrow> DERIV (F m) z :> F (Suc m) z"
+ and hyp: "\<And> t. t \<in> {real lx .. real ux} \<Longrightarrow>
+ (\<Sum> j = 0..<n. inverse (real (fact j)) * F j (real c) * (xs!x - real c)^j) +
+ inverse (real (fact n)) * F n t * (xs!x - real c)^n
+ \<in> {real l .. real u}" (is "\<And> t. _ \<Longrightarrow> ?taylor t \<in> _")
+ unfolding F_def atLeastAtMost_iff[symmetric] setprod_fact by blast
+
+ have bnd_xs: "xs ! x \<in> { real lx .. real ux }"
+ using `bounded_by xs vs`[THEN bounded_byE, OF `x < length vs`] bnd_x by auto
+
+ show ?thesis
+ proof (cases n)
+ case 0 thus ?thesis using hyp[OF bnd_xs] unfolding F_def by auto
+ next
+ case (Suc n')
+ show ?thesis
+ proof (cases "xs ! x = real c")
+ case True
+ from True[symmetric] hyp[OF bnd_xs] Suc show ?thesis
+ unfolding F_def Suc setsum_head_upt_Suc[OF zero_less_Suc] setsum_shift_bounds_Suc_ivl by auto
+ next
+ case False
+
+ have "real lx \<le> real c" "real c \<le> real ux" "real lx \<le> xs!x" "xs!x \<le> real ux"
+ using Suc bnd_c `bounded_by xs vs`[THEN bounded_byE, OF `x < length vs`] bnd_x by auto
+ from Taylor.taylor[OF zero_less_Suc, of F, OF F0 DERIV[unfolded Suc] this False]
+ obtain t where t_bnd: "if xs ! x < real c then xs ! x < t \<and> t < real c else real c < t \<and> t < xs ! x"
+ and fl_eq: "interpret_floatarith f (xs[x := xs ! x]) =
+ (\<Sum>m = 0..<Suc n'. F m (real c) / real (fact m) * (xs ! x - real c) ^ m) +
+ F (Suc n') t / real (fact (Suc n')) * (xs ! x - real c) ^ Suc n'"
+ by blast
+
+ from t_bnd bnd_xs bnd_c have *: "t \<in> {real lx .. real ux}"
+ by (cases "xs ! x < real c", auto)
+
+ have "interpret_floatarith f (xs[x := xs ! x]) = ?taylor t"
+ unfolding fl_eq Suc by (auto simp add: algebra_simps divide_inverse)
+ also have "\<dots> \<in> {real l .. real u}" using * by (rule hyp)
+ finally show ?thesis by simp
+ qed
+ qed
+qed
+
+fun approx_tse_form' where
+"approx_tse_form' prec t f 0 l u cmp =
+ (case approx_tse prec 0 t ((l + u) * Float 1 -1) 1 f [Some (l, u)]
+ of Some (l, u) \<Rightarrow> cmp l u | None \<Rightarrow> False)" |
+"approx_tse_form' prec t f (Suc s) l u cmp =
+ (let m = (l + u) * Float 1 -1
+ in approx_tse_form' prec t f s l m cmp \<and>
+ approx_tse_form' prec t f s m u cmp)"
+
+lemma approx_tse_form':
+ assumes "approx_tse_form' prec t f s l u cmp" and "x \<in> {real l .. real u}"
+ shows "\<exists> l' u' ly uy. x \<in> { real l' .. real u' } \<and> real l \<le> real l' \<and> real u' \<le> real u \<and> cmp ly uy \<and>
+ approx_tse prec 0 t ((l' + u') * Float 1 -1) 1 f [Some (l', u')] = Some (ly, uy)"
+using assms proof (induct s arbitrary: l u)
+ case 0
+ then obtain ly uy
+ where *: "approx_tse prec 0 t ((l + u) * Float 1 -1) 1 f [Some (l, u)] = Some (ly, uy)"
+ and **: "cmp ly uy" by (auto elim!: option_caseE)
+ with 0 show ?case by (auto intro!: exI)
+next
+ case (Suc s)
+ let ?m = "(l + u) * Float 1 -1"
+ from Suc.prems
+ have l: "approx_tse_form' prec t f s l ?m cmp"
+ and u: "approx_tse_form' prec t f s ?m u cmp"
+ by (auto simp add: Let_def)
+
+ have m_l: "real l \<le> real ?m" and m_u: "real ?m \<le> real u"
+ unfolding le_float_def using Suc.prems by auto
+
+ with `x \<in> { real l .. real u }`
+ have "x \<in> { real l .. real ?m} \<or> x \<in> { real ?m .. real u }" by auto
+ thus ?case
+ proof (rule disjE)
+ assume "x \<in> { real l .. real ?m}"
+ from Suc.hyps[OF l this]
+ obtain l' u' ly uy
+ where "x \<in> { real l' .. real u' } \<and> real l \<le> real l' \<and> real u' \<le> real ?m \<and> cmp ly uy \<and>
+ approx_tse prec 0 t ((l' + u') * Float 1 -1) 1 f [Some (l', u')] = Some (ly, uy)" by blast
+ with m_u show ?thesis by (auto intro!: exI)
+ next
+ assume "x \<in> { real ?m .. real u }"
+ from Suc.hyps[OF u this]
+ obtain l' u' ly uy
+ where "x \<in> { real l' .. real u' } \<and> real ?m \<le> real l' \<and> real u' \<le> real u \<and> cmp ly uy \<and>
+ approx_tse prec 0 t ((l' + u') * Float 1 -1) 1 f [Some (l', u')] = Some (ly, uy)" by blast
+ with m_u show ?thesis by (auto intro!: exI)
+ qed
+qed
+
+lemma approx_tse_form'_less:
+ assumes tse: "approx_tse_form' prec t (Add a (Minus b)) s l u (\<lambda> l u. 0 < l)"
+ and x: "x \<in> {real l .. real u}"
+ shows "interpret_floatarith b [x] < interpret_floatarith a [x]"
+proof -
+ from approx_tse_form'[OF tse x]
+ obtain l' u' ly uy
+ where x': "x \<in> { real l' .. real u' }" and "real l \<le> real l'"
+ and "real u' \<le> real u" and "0 < ly"
+ and tse: "approx_tse prec 0 t ((l' + u') * Float 1 -1) 1 (Add a (Minus b)) [Some (l', u')] = Some (ly, uy)"
+ by blast
+
+ hence "bounded_by [x] [Some (l', u')]" by (auto simp add: bounded_by_def)
+
+ from approx_tse[OF this _ _ _ _ tse[symmetric], of l' u'] x'
+ have "real ly \<le> interpret_floatarith a [x] - interpret_floatarith b [x]"
+ by (auto simp add: diff_minus)
+ from order_less_le_trans[OF `0 < ly`[unfolded less_float_def] this]
+ show ?thesis by auto
+qed
+
+lemma approx_tse_form'_le:
+ assumes tse: "approx_tse_form' prec t (Add a (Minus b)) s l u (\<lambda> l u. 0 \<le> l)"
+ and x: "x \<in> {real l .. real u}"
+ shows "interpret_floatarith b [x] \<le> interpret_floatarith a [x]"
+proof -
+ from approx_tse_form'[OF tse x]
+ obtain l' u' ly uy
+ where x': "x \<in> { real l' .. real u' }" and "real l \<le> real l'"
+ and "real u' \<le> real u" and "0 \<le> ly"
+ and tse: "approx_tse prec 0 t ((l' + u') * Float 1 -1) 1 (Add a (Minus b)) [Some (l', u')] = Some (ly, uy)"
+ by blast
+
+ hence "bounded_by [x] [Some (l', u')]" by (auto simp add: bounded_by_def)
+
+ from approx_tse[OF this _ _ _ _ tse[symmetric], of l' u'] x'
+ have "real ly \<le> interpret_floatarith a [x] - interpret_floatarith b [x]"
+ by (auto simp add: diff_minus)
+ from order_trans[OF `0 \<le> ly`[unfolded le_float_def] this]
+ show ?thesis by auto
+qed
+
+definition
+"approx_tse_form prec t s f =
+ (case f
+ of (Bound x a b f) \<Rightarrow> x = Atom 0 \<and>
+ (case (approx prec a [None], approx prec b [None])
+ of (Some (l, u), Some (l', u')) \<Rightarrow>
+ (case f
+ of Less lf rt \<Rightarrow> approx_tse_form' prec t (Add rt (Minus lf)) s l u' (\<lambda> l u. 0 < l)
+ | LessEqual lf rt \<Rightarrow> approx_tse_form' prec t (Add rt (Minus lf)) s l u' (\<lambda> l u. 0 \<le> l)
+ | AtLeastAtMost x lf rt \<Rightarrow>
+ approx_tse_form' prec t (Add x (Minus lf)) s l u' (\<lambda> l u. 0 \<le> l) \<and>
+ approx_tse_form' prec t (Add rt (Minus x)) s l u' (\<lambda> l u. 0 \<le> l)
+ | _ \<Rightarrow> False)
+ | _ \<Rightarrow> False)
+ | _ \<Rightarrow> False)"
+
+lemma approx_tse_form:
+ assumes "approx_tse_form prec t s f"
+ shows "interpret_form f [x]"
+proof (cases f)
+ case (Bound i a b f') note f_def = this
+ with assms obtain l u l' u'
+ where a: "approx prec a [None] = Some (l, u)"
+ and b: "approx prec b [None] = Some (l', u')"
+ unfolding approx_tse_form_def by (auto elim!: option_caseE)
+
+ from Bound assms have "i = Atom 0" unfolding approx_tse_form_def by auto
+ hence i: "interpret_floatarith i [x] = x" by auto
+
+ { let "?f z" = "interpret_floatarith z [x]"
+ assume "?f i \<in> { ?f a .. ?f b }"
+ with approx[OF _ a[symmetric], of "[x]"] approx[OF _ b[symmetric], of "[x]"]
+ have bnd: "x \<in> { real l .. real u'}" unfolding bounded_by_def i by auto
+
+ have "interpret_form f' [x]"
+ proof (cases f')
+ case (Less lf rt)
+ with Bound a b assms
+ have "approx_tse_form' prec t (Add rt (Minus lf)) s l u' (\<lambda> l u. 0 < l)"
+ unfolding approx_tse_form_def by auto
+ from approx_tse_form'_less[OF this bnd]
+ show ?thesis using Less by auto
+ next
+ case (LessEqual lf rt)
+ with Bound a b assms
+ have "approx_tse_form' prec t (Add rt (Minus lf)) s l u' (\<lambda> l u. 0 \<le> l)"
+ unfolding approx_tse_form_def by auto
+ from approx_tse_form'_le[OF this bnd]
+ show ?thesis using LessEqual by auto
+ next
+ case (AtLeastAtMost x lf rt)
+ with Bound a b assms
+ have "approx_tse_form' prec t (Add rt (Minus x)) s l u' (\<lambda> l u. 0 \<le> l)"
+ and "approx_tse_form' prec t (Add x (Minus lf)) s l u' (\<lambda> l u. 0 \<le> l)"
+ unfolding approx_tse_form_def by auto
+ from approx_tse_form'_le[OF this(1) bnd] approx_tse_form'_le[OF this(2) bnd]
+ show ?thesis using AtLeastAtMost by auto
+ next
+ case (Bound x a b f') with assms
+ show ?thesis by (auto elim!: option_caseE simp add: f_def approx_tse_form_def)
+ next
+ case (Assign x a f') with assms
+ show ?thesis by (auto elim!: option_caseE simp add: f_def approx_tse_form_def)
+ qed } thus ?thesis unfolding f_def by auto
+next case Assign with assms show ?thesis by (auto simp add: approx_tse_form_def)
+next case LessEqual with assms show ?thesis by (auto simp add: approx_tse_form_def)
+next case Less with assms show ?thesis by (auto simp add: approx_tse_form_def)
+next case AtLeastAtMost with assms show ?thesis by (auto simp add: approx_tse_form_def)
+qed
+
subsection {* Implement proof method \texttt{approximation} *}
lemmas interpret_form_equations = interpret_form.simps interpret_floatarith.simps interpret_floatarith_num
@@ -2648,6 +3200,7 @@
@{code_datatype form = Bound | Assign | Less | LessEqual | AtLeastAtMost}
val approx_form = @{code approx_form}
+val approx_tse_form = @{code approx_tse_form}
val approx' = @{code approx'}
end
@@ -2675,6 +3228,7 @@
"Float'_Arith.AtLeastAtMost/ (_,/ _,/ _)")
code_const approx_form (Eval "Float'_Arith.approx'_form")
+code_const approx_tse_form (Eval "Float'_Arith.approx'_tse'_form")
code_const approx' (Eval "Float'_Arith.approx'")
ML {*
@@ -2712,30 +3266,49 @@
val form_equations = PureThy.get_thms @{theory} "interpret_form_equations";
- fun rewrite_interpret_form_tac ctxt prec splitting i st = let
+ fun rewrite_interpret_form_tac ctxt prec splitting taylor i st = let
+ fun lookup_splitting (Free (name, typ))
+ = case AList.lookup (op =) splitting name
+ of SOME s => HOLogic.mk_number @{typ nat} s
+ | NONE => @{term "0 :: nat"}
val vs = nth (prems_of st) (i - 1)
|> Logic.strip_imp_concl
|> HOLogic.dest_Trueprop
|> Term.strip_comb |> snd |> List.last
|> HOLogic.dest_list
- val n = vs |> length
- |> HOLogic.mk_number @{typ nat}
- |> Thm.cterm_of (ProofContext.theory_of ctxt)
val p = prec
|> HOLogic.mk_number @{typ nat}
|> Thm.cterm_of (ProofContext.theory_of ctxt)
- val s = vs
- |> map (fn Free (name, typ) =>
- case AList.lookup (op =) splitting name of
- SOME s => HOLogic.mk_number @{typ nat} s
- | NONE => @{term "0 :: nat"})
- |> HOLogic.mk_list @{typ nat}
+ in case taylor
+ of NONE => let
+ val n = vs |> length
+ |> HOLogic.mk_number @{typ nat}
+ |> Thm.cterm_of (ProofContext.theory_of ctxt)
+ val s = vs
+ |> map lookup_splitting
+ |> HOLogic.mk_list @{typ nat}
+ |> Thm.cterm_of (ProofContext.theory_of ctxt)
+ in
+ (rtac (Thm.instantiate ([], [(@{cpat "?n::nat"}, n),
+ (@{cpat "?prec::nat"}, p),
+ (@{cpat "?ss::nat list"}, s)])
+ @{thm "approx_form"}) i
+ THEN simp_tac @{simpset} i) st
+ end
+
+ | SOME t => if length vs <> 1 then raise (TERM ("More than one variable used for taylor series expansion", [prop_of st]))
+ else let
+ val t = t
+ |> HOLogic.mk_number @{typ nat}
|> Thm.cterm_of (ProofContext.theory_of ctxt)
- in
- rtac (Thm.instantiate ([], [(@{cpat "?n::nat"}, n),
- (@{cpat "?prec::nat"}, p),
- (@{cpat "?ss::nat list"}, s)])
- @{thm "approx_form"}) i st
+ val s = vs |> map lookup_splitting |> hd
+ |> Thm.cterm_of (ProofContext.theory_of ctxt)
+ in
+ rtac (Thm.instantiate ([], [(@{cpat "?s::nat"}, s),
+ (@{cpat "?t::nat"}, t),
+ (@{cpat "?prec::nat"}, p)])
+ @{thm "approx_tse_form"}) i st
+ end
end
(* copied from Tools/induct.ML should probably in args.ML *)
@@ -2751,11 +3324,15 @@
by auto
method_setup approximation = {*
- Scan.lift (OuterParse.nat) --
+ Scan.lift (OuterParse.nat)
+ --
Scan.optional (Scan.lift (Args.$$$ "splitting" |-- Args.colon)
|-- OuterParse.and_list' (free --| Scan.lift (Args.$$$ "=") -- Scan.lift OuterParse.nat)) []
+ --
+ Scan.option (Scan.lift (Args.$$$ "taylor" |-- Args.colon)
+ |-- (free |-- Scan.lift (Args.$$$ "=") |-- Scan.lift OuterParse.nat))
>>
- (fn (prec, splitting) => fn ctxt =>
+ (fn ((prec, splitting), taylor) => fn ctxt =>
SIMPLE_METHOD' (fn i =>
REPEAT (FIRST' [etac @{thm intervalE},
etac @{thm meta_eqE},
@@ -2763,15 +3340,10 @@
THEN METAHYPS (reorder_bounds_tac i) i
THEN TRY (filter_prems_tac (K false) i)
THEN DETERM (Reflection.genreify_tac ctxt form_equations NONE i)
- THEN print_tac "approximation"
- THEN rewrite_interpret_form_tac ctxt prec splitting i
- THEN simp_tac @{simpset} i
+ THEN rewrite_interpret_form_tac ctxt prec splitting taylor i
THEN gen_eval_tac eval_oracle ctxt i))
*} "real number approximation"
-lemma "\<phi> \<in> {0..1 :: real} \<Longrightarrow> \<phi> < \<phi> + 0.7"
- by (approximation 10 splitting: "\<phi>" = 1)
-
ML {*
fun dest_interpret (@{const "interpret_floatarith"} $ b $ xs) = (b, xs)
| dest_interpret t = raise TERM ("dest_interpret", [t])
--- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Thu Jul 02 16:06:12 2009 +0200
+++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Thu Jul 02 18:32:28 2009 +0200
@@ -8,13 +8,28 @@
Here are some examples how to use the approximation method.
-The parameter passed to the method specifies the precision used by the computations, it is specified
-as number of bits to calculate. When a variable is used it needs to be bounded by an interval. This
-interval is specified as a conjunction of the lower and upper bound. It must have the form
-@{text "\<lbrakk> l\<^isub>1 \<le> x\<^isub>1 \<and> x\<^isub>1 \<le> u\<^isub>1 ; \<dots> ; l\<^isub>n \<le> x\<^isub>n \<and> x\<^isub>n \<le> u\<^isub>n \<rbrakk> \<Longrightarrow> F"} where @{term F} is the formula, and
-@{text "x\<^isub>1, \<dots>, x\<^isub>n"} are the variables. The lower bounds @{text "l\<^isub>1, \<dots>, l\<^isub>n"} and the upper bounds
-@{text "u\<^isub>1, \<dots>, u\<^isub>n"} must either be integer numerals, floating point numbers or of the form
-@{term "m * pow2 e"} to specify a exact floating point value.
+The approximation method has the following syntax:
+
+approximate "prec" (splitting: "x" = "depth" and "y" = "depth" ...)? (taylor: "z" = "derivates")?
+
+Here "prec" specifies the precision used in all computations, it is specified as
+number of bits to calculate. In the proposition to prove an arbitrary amount of
+variables can be used, but each one need to be bounded by an upper and lower
+bound.
+
+To specify the bounds either @{term "l\<^isub>1 \<le> x \<and> x \<le> u\<^isub>1"},
+@{term "x \<in> { l\<^isub>1 .. u\<^isub>1 }"} or @{term "x = bnd"} can be used. Where the
+bound specification are again arithmetic formulas containing variables. They can
+be connected using either meta level or HOL equivalence.
+
+To use interval splitting add for each variable whos interval should be splitted
+to the "splitting:" parameter. The parameter specifies how often each interval
+should be divided, e.g. when x = 16 is specified, there will be @{term "65536 = 2^16"}
+intervals to be calculated.
+
+To use taylor series expansion specify the variable to derive. You need to
+specify the amount of derivations to compute. When using taylor series expansion
+only one variable can be used.
*}
@@ -57,4 +72,7 @@
shows "g / v * tan (35 * d) \<in> { 3 * d .. 3.1 * d }"
using assms by (approximation 80)
+lemma "\<phi> \<in> { 0 .. 1 :: real } \<longrightarrow> \<phi> ^ 2 \<le> \<phi>"
+ by (approximation 30 splitting: \<phi>=1 taylor: \<phi> = 3)
+
end
--- a/src/HOL/Deriv.thy Thu Jul 02 16:06:12 2009 +0200
+++ b/src/HOL/Deriv.thy Thu Jul 02 18:32:28 2009 +0200
@@ -115,12 +115,16 @@
text{*Differentiation of finite sum*}
+lemma DERIV_setsum:
+ assumes "finite S"
+ and "\<And> n. n \<in> S \<Longrightarrow> DERIV (%x. f x n) x :> (f' x n)"
+ shows "DERIV (%x. setsum (f x) S) x :> setsum (f' x) S"
+ using assms by induct (auto intro!: DERIV_add)
+
lemma DERIV_sumr [rule_format (no_asm)]:
"(\<forall>r. m \<le> r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x))
--> DERIV (%x. \<Sum>n=m..<n::nat. f n x :: real) x :> (\<Sum>r=m..<n. f' r x)"
-apply (induct "n")
-apply (auto intro: DERIV_add)
-done
+ by (auto intro: DERIV_setsum)
text{*Alternative definition for differentiability*}
@@ -216,7 +220,6 @@
shows "DERIV (\<lambda>x. f x ^ n) x :> of_nat n * (D * f x ^ (n - Suc 0))"
by (cases "n", simp, simp add: DERIV_power_Suc f del: power_Suc)
-
text {* Caratheodory formulation of derivative at a point *}
lemma CARAT_DERIV:
@@ -261,21 +264,23 @@
by (simp add: d dfx real_scaleR_def)
qed
-(* let's do the standard proof though theorem *)
-(* LIM_mult2 follows from a NS proof *)
+text {*
+ Let's do the standard proof, though theorem
+ @{text "LIM_mult2"} follows from a NS proof
+*}
lemma DERIV_cmult:
"DERIV f x :> D ==> DERIV (%x. c * f x) x :> c*D"
by (drule DERIV_mult' [OF DERIV_const], simp)
-(* standard version *)
+text {* Standard version *}
lemma DERIV_chain: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (f o g) x :> Da * Db"
by (drule (1) DERIV_chain', simp add: o_def real_scaleR_def mult_commute)
lemma DERIV_chain2: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (%x. f (g x)) x :> Da * Db"
by (auto dest: DERIV_chain simp add: o_def)
-(*derivative of linear multiplication*)
+text {* Derivative of linear multiplication *}
lemma DERIV_cmult_Id [simp]: "DERIV (op * c) x :> c"
by (cut_tac c = c and x = x in DERIV_ident [THEN DERIV_cmult], simp)
@@ -284,21 +289,21 @@
apply (simp add: real_scaleR_def real_of_nat_def)
done
-text{*Power of -1*}
+text {* Power of @{text "-1"} *}
lemma DERIV_inverse:
fixes x :: "'a::{real_normed_field}"
shows "x \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))"
by (drule DERIV_inverse' [OF DERIV_ident]) simp
-text{*Derivative of inverse*}
+text {* Derivative of inverse *}
lemma DERIV_inverse_fun:
fixes x :: "'a::{real_normed_field}"
shows "[| DERIV f x :> d; f(x) \<noteq> 0 |]
==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"
by (drule (1) DERIV_inverse') (simp add: mult_ac nonzero_inverse_mult_distrib)
-text{*Derivative of quotient*}
+text {* Derivative of quotient *}
lemma DERIV_quotient:
fixes x :: "'a::{real_normed_field}"
shows "[| DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> 0 |]
@@ -308,6 +313,33 @@
lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
by auto
+text {* @{text "DERIV_intros"} *}
+ML {*
+structure DerivIntros = NamedThmsFun
+(
+ val name = "DERIV_intros"
+ val description = "DERIV introduction rules"
+)
+*}
+
+setup DerivIntros.setup
+
+lemma DERIV_cong: "\<lbrakk> DERIV f x :> X ; X = Y \<rbrakk> \<Longrightarrow> DERIV f x :> Y"
+ by simp
+
+declare
+ DERIV_const[THEN DERIV_cong, DERIV_intros]
+ DERIV_ident[THEN DERIV_cong, DERIV_intros]
+ DERIV_add[THEN DERIV_cong, DERIV_intros]
+ DERIV_minus[THEN DERIV_cong, DERIV_intros]
+ DERIV_mult[THEN DERIV_cong, DERIV_intros]
+ DERIV_diff[THEN DERIV_cong, DERIV_intros]
+ DERIV_inverse'[THEN DERIV_cong, DERIV_intros]
+ DERIV_divide[THEN DERIV_cong, DERIV_intros]
+ DERIV_power[where 'a=real, THEN DERIV_cong,
+ unfolded real_of_nat_def[symmetric], DERIV_intros]
+ DERIV_setsum[THEN DERIV_cong, DERIV_intros]
+
subsection {* Differentiability predicate *}
--- a/src/HOL/Finite_Set.thy Thu Jul 02 16:06:12 2009 +0200
+++ b/src/HOL/Finite_Set.thy Thu Jul 02 18:32:28 2009 +0200
@@ -528,7 +528,7 @@
subsection {* A fold functional for finite sets *}
text {* The intended behaviour is
-@{text "fold f z {x\<^isub>1, ..., x\<^isub>n} = f x\<^isub>1 (\<dots> (f x\<^isub>n z)\<dots>)"}
+@{text "fold f z {x1, ..., xn} = f x1 (\<dots> (f xn z)\<dots>)"}
if @{text f} is ``left-commutative'':
*}
@@ -1883,14 +1883,14 @@
(if a:A then setprod f A / f a else setprod f A)"
by (erule finite_induct) (auto simp add: insert_Diff_if)
-lemma setprod_inversef: "finite A ==>
- ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==>
- setprod (inverse \<circ> f) A = inverse (setprod f A)"
+lemma setprod_inversef:
+ fixes f :: "'b \<Rightarrow> 'a::{field,division_by_zero}"
+ shows "finite A ==> setprod (inverse \<circ> f) A = inverse (setprod f A)"
by (erule finite_induct) auto
lemma setprod_dividef:
- "[|finite A;
- \<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})|]
+ fixes f :: "'b \<Rightarrow> 'a::{field,division_by_zero}"
+ shows "finite A
==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
apply (subgoal_tac
"setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
@@ -2725,16 +2725,16 @@
begin
definition
- Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^bsub>fin\<^esub>_" [900] 900)
+ Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>fin_" [900] 900)
where
"Inf_fin = fold1 inf"
definition
- Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^bsub>fin\<^esub>_" [900] 900)
+ Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>fin_" [900] 900)
where
"Sup_fin = fold1 sup"
-lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<le> \<Squnion>\<^bsub>fin\<^esub>A"
+lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>finA \<le> \<Squnion>finA"
apply(unfold Sup_fin_def Inf_fin_def)
apply(subgoal_tac "EX a. a:A")
prefer 2 apply blast
@@ -2745,13 +2745,13 @@
done
lemma sup_Inf_absorb [simp]:
- "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^bsub>fin\<^esub>A) = a"
+ "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>finA) = a"
apply(subst sup_commute)
apply(simp add: Inf_fin_def sup_absorb2 fold1_belowI)
done
lemma inf_Sup_absorb [simp]:
- "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^bsub>fin\<^esub>A) = a"
+ "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>finA) = a"
by (simp add: Sup_fin_def inf_absorb1
lower_semilattice.fold1_belowI [OF dual_lattice])
@@ -2763,7 +2763,7 @@
lemma sup_Inf1_distrib:
assumes "finite A"
and "A \<noteq> {}"
- shows "sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}"
+ shows "sup x (\<Sqinter>finA) = \<Sqinter>fin{sup x a|a. a \<in> A}"
proof -
interpret ab_semigroup_idem_mult inf
by (rule ab_semigroup_idem_mult_inf)
@@ -2775,7 +2775,7 @@
lemma sup_Inf2_distrib:
assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
- shows "sup (\<Sqinter>\<^bsub>fin\<^esub>A) (\<Sqinter>\<^bsub>fin\<^esub>B) = \<Sqinter>\<^bsub>fin\<^esub>{sup a b|a b. a \<in> A \<and> b \<in> B}"
+ shows "sup (\<Sqinter>finA) (\<Sqinter>finB) = \<Sqinter>fin{sup a b|a b. a \<in> A \<and> b \<in> B}"
using A proof (induct rule: finite_ne_induct)
case singleton thus ?case
by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def])
@@ -2792,13 +2792,13 @@
thus ?thesis by(simp add: insert(1) B(1))
qed
have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
- have "sup (\<Sqinter>\<^bsub>fin\<^esub>(insert x A)) (\<Sqinter>\<^bsub>fin\<^esub>B) = sup (inf x (\<Sqinter>\<^bsub>fin\<^esub>A)) (\<Sqinter>\<^bsub>fin\<^esub>B)"
+ have "sup (\<Sqinter>fin(insert x A)) (\<Sqinter>finB) = sup (inf x (\<Sqinter>finA)) (\<Sqinter>finB)"
using insert by (simp add: fold1_insert_idem_def [OF Inf_fin_def])
- also have "\<dots> = inf (sup x (\<Sqinter>\<^bsub>fin\<^esub>B)) (sup (\<Sqinter>\<^bsub>fin\<^esub>A) (\<Sqinter>\<^bsub>fin\<^esub>B))" by(rule sup_inf_distrib2)
- also have "\<dots> = inf (\<Sqinter>\<^bsub>fin\<^esub>{sup x b|b. b \<in> B}) (\<Sqinter>\<^bsub>fin\<^esub>{sup a b|a b. a \<in> A \<and> b \<in> B})"
+ also have "\<dots> = inf (sup x (\<Sqinter>finB)) (sup (\<Sqinter>finA) (\<Sqinter>finB))" by(rule sup_inf_distrib2)
+ also have "\<dots> = inf (\<Sqinter>fin{sup x b|b. b \<in> B}) (\<Sqinter>fin{sup a b|a b. a \<in> A \<and> b \<in> B})"
using insert by(simp add:sup_Inf1_distrib[OF B])
- also have "\<dots> = \<Sqinter>\<^bsub>fin\<^esub>({sup x b |b. b \<in> B} \<union> {sup a b |a b. a \<in> A \<and> b \<in> B})"
- (is "_ = \<Sqinter>\<^bsub>fin\<^esub>?M")
+ also have "\<dots> = \<Sqinter>fin({sup x b |b. b \<in> B} \<union> {sup a b |a b. a \<in> A \<and> b \<in> B})"
+ (is "_ = \<Sqinter>fin?M")
using B insert
by (simp add: Inf_fin_def fold1_Un2 [OF finB _ finAB ne])
also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
@@ -2808,7 +2808,7 @@
lemma inf_Sup1_distrib:
assumes "finite A" and "A \<noteq> {}"
- shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}"
+ shows "inf x (\<Squnion>finA) = \<Squnion>fin{inf x a|a. a \<in> A}"
proof -
interpret ab_semigroup_idem_mult sup
by (rule ab_semigroup_idem_mult_sup)
@@ -2819,7 +2819,7 @@
lemma inf_Sup2_distrib:
assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
- shows "inf (\<Squnion>\<^bsub>fin\<^esub>A) (\<Squnion>\<^bsub>fin\<^esub>B) = \<Squnion>\<^bsub>fin\<^esub>{inf a b|a b. a \<in> A \<and> b \<in> B}"
+ shows "inf (\<Squnion>finA) (\<Squnion>finB) = \<Squnion>fin{inf a b|a b. a \<in> A \<and> b \<in> B}"
using A proof (induct rule: finite_ne_induct)
case singleton thus ?case
by(simp add: inf_Sup1_distrib [OF B] fold1_singleton_def [OF Sup_fin_def])
@@ -2836,13 +2836,13 @@
have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
interpret ab_semigroup_idem_mult sup
by (rule ab_semigroup_idem_mult_sup)
- have "inf (\<Squnion>\<^bsub>fin\<^esub>(insert x A)) (\<Squnion>\<^bsub>fin\<^esub>B) = inf (sup x (\<Squnion>\<^bsub>fin\<^esub>A)) (\<Squnion>\<^bsub>fin\<^esub>B)"
+ have "inf (\<Squnion>fin(insert x A)) (\<Squnion>finB) = inf (sup x (\<Squnion>finA)) (\<Squnion>finB)"
using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def])
- also have "\<dots> = sup (inf x (\<Squnion>\<^bsub>fin\<^esub>B)) (inf (\<Squnion>\<^bsub>fin\<^esub>A) (\<Squnion>\<^bsub>fin\<^esub>B))" by(rule inf_sup_distrib2)
- also have "\<dots> = sup (\<Squnion>\<^bsub>fin\<^esub>{inf x b|b. b \<in> B}) (\<Squnion>\<^bsub>fin\<^esub>{inf a b|a b. a \<in> A \<and> b \<in> B})"
+ also have "\<dots> = sup (inf x (\<Squnion>finB)) (inf (\<Squnion>finA) (\<Squnion>finB))" by(rule inf_sup_distrib2)
+ also have "\<dots> = sup (\<Squnion>fin{inf x b|b. b \<in> B}) (\<Squnion>fin{inf a b|a b. a \<in> A \<and> b \<in> B})"
using insert by(simp add:inf_Sup1_distrib[OF B])
- also have "\<dots> = \<Squnion>\<^bsub>fin\<^esub>({inf x b |b. b \<in> B} \<union> {inf a b |a b. a \<in> A \<and> b \<in> B})"
- (is "_ = \<Squnion>\<^bsub>fin\<^esub>?M")
+ also have "\<dots> = \<Squnion>fin({inf x b |b. b \<in> B} \<union> {inf a b |a b. a \<in> A \<and> b \<in> B})"
+ (is "_ = \<Squnion>fin?M")
using B insert
by (simp add: Sup_fin_def fold1_Un2 [OF finB _ finAB ne])
also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
@@ -2861,7 +2861,7 @@
lemma Inf_fin_Inf:
assumes "finite A" and "A \<noteq> {}"
- shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
+ shows "\<Sqinter>finA = Inf A"
proof -
interpret ab_semigroup_idem_mult inf
by (rule ab_semigroup_idem_mult_inf)
@@ -2872,7 +2872,7 @@
lemma Sup_fin_Sup:
assumes "finite A" and "A \<noteq> {}"
- shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
+ shows "\<Squnion>finA = Sup A"
proof -
interpret ab_semigroup_idem_mult sup
by (rule ab_semigroup_idem_mult_sup)
--- a/src/HOL/Imperative_HOL/Array.thy Thu Jul 02 16:06:12 2009 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy Thu Jul 02 18:32:28 2009 +0200
@@ -1,5 +1,4 @@
-(* Title: HOL/Library/Array.thy
- ID: $Id$
+(* Title: HOL/Imperative_HOL/Array.thy
Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
*)
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Jul 02 16:06:12 2009 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Jul 02 18:32:28 2009 +0200
@@ -306,67 +306,75 @@
code_const "Heap_Monad.Fail" (OCaml "Failure")
code_const "Heap_Monad.raise_exc" (OCaml "!(fun/ ()/ ->/ raise/ _)")
-setup {* let
- open Code_Thingol;
+setup {*
+
+let
- fun lookup naming = the o Code_Thingol.lookup_const naming;
+open Code_Thingol;
+
+fun imp_program naming =
- fun imp_monad_bind'' bind' return' unit' ts =
- let
- val dummy_name = "";
- val dummy_type = ITyVar dummy_name;
- val dummy_case_term = IVar dummy_name;
- (*assumption: dummy values are not relevant for serialization*)
- val unitt = IConst (unit', (([], []), []));
- fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
- | dest_abs (t, ty) =
- let
- val vs = Code_Thingol.fold_varnames cons t [];
- val v = Name.variant vs "x";
- val ty' = (hd o fst o Code_Thingol.unfold_fun) ty;
- in ((v, ty'), t `$ IVar v) end;
- fun force (t as IConst (c, _) `$ t') = if c = return'
- then t' else t `$ unitt
- | force t = t `$ unitt;
- fun tr_bind' [(t1, _), (t2, ty2)] =
- let
- 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 Code_Thingol.unfold_app t
- of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if c = bind'
- then tr_bind' [(x1, ty1), (x2, ty2)]
- else force t
- | _ => force t;
- in (dummy_name, dummy_type) `|=> ICase (((IVar dummy_name, dummy_type),
- [(unitt, tr_bind' ts)]), dummy_case_term) end
- and imp_monad_bind' bind' return' unit' (const as (c, (_, tys))) ts = if c = bind' then case (ts, tys)
- of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' bind' return' unit' [(t1, ty1), (t2, ty2)]
- | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' bind' return' unit' [(t1, ty1), (t2, ty2)] `$ t3
- | (ts, _) => imp_monad_bind bind' return' unit' (eta_expand 2 (const, ts))
- else IConst const `$$ map (imp_monad_bind bind' return' unit') ts
- and imp_monad_bind bind' return' unit' (IConst const) = imp_monad_bind' bind' return' unit' const []
- | imp_monad_bind bind' return' unit' (t as IVar _) = t
- | imp_monad_bind bind' return' unit' (t as _ `$ _) = (case unfold_app t
- of (IConst const, ts) => imp_monad_bind' bind' return' unit' const ts
- | (t, ts) => imp_monad_bind bind' return' unit' t `$$ map (imp_monad_bind bind' return' unit') ts)
- | imp_monad_bind bind' return' unit' (v_ty `|=> t) = v_ty `|=> imp_monad_bind bind' return' unit' t
- | imp_monad_bind bind' return' unit' (ICase (((t, ty), pats), t0)) = ICase
- (((imp_monad_bind bind' return' unit' t, ty), (map o pairself) (imp_monad_bind bind' return' unit') pats), imp_monad_bind bind' return' unit' t0);
+ let
+ 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_return = is_const @{const_name return};
+ val dummy_name = "";
+ val dummy_type = ITyVar dummy_name;
+ val dummy_case_term = IVar NONE;
+ (*assumption: dummy values are not relevant for serialization*)
+ val unitt = case lookup_const naming @{const_name Unity}
+ of SOME unit' => IConst (unit', (([], []), []))
+ | NONE => error ("Must include " ^ @{const_name Unity} ^ " in generated constants.");
+ fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
+ | dest_abs (t, ty) =
+ let
+ val vs = fold_varnames cons t [];
+ val v = Name.variant vs "x";
+ val ty' = (hd o fst o unfold_fun) ty;
+ in ((SOME v, ty'), t `$ IVar (SOME v)) end;
+ fun force (t as IConst (c, _) `$ t') = if is_return c
+ then t' else t `$ unitt
+ | force t = t `$ unitt;
+ fun tr_bind' [(t1, _), (t2, ty2)] =
+ let
+ 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
+ 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)
+ 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))
+ else IConst const `$$ map imp_monad_bind ts
+ and imp_monad_bind (IConst const) = imp_monad_bind' const []
+ | imp_monad_bind (t as IVar _) = t
+ | imp_monad_bind (t as _ `$ _) = (case unfold_app t
+ of (IConst const, ts) => imp_monad_bind' const ts
+ | (t, ts) => imp_monad_bind t `$$ map imp_monad_bind ts)
+ | imp_monad_bind (v_ty `|=> t) = v_ty `|=> imp_monad_bind t
+ | imp_monad_bind (ICase (((t, ty), pats), t0)) = ICase
+ (((imp_monad_bind t, ty),
+ (map o pairself) imp_monad_bind pats),
+ imp_monad_bind t0);
- fun imp_program naming = (Graph.map_nodes o map_terms_stmt)
- (imp_monad_bind (lookup naming @{const_name bindM})
- (lookup naming @{const_name return})
- (lookup naming @{const_name Unity}));
+ in (Graph.map_nodes o map_terms_stmt) imp_monad_bind end;
in
- Code_Target.extend_target ("SML_imp", ("SML", imp_program))
- #> Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program))
+Code_Target.extend_target ("SML_imp", ("SML", imp_program))
+#> Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program))
end
+
*}
-
code_reserved OCaml Failure raise
--- a/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy Thu Jul 02 16:06:12 2009 +0200
+++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy Thu Jul 02 18:32:28 2009 +0200
@@ -1,8 +1,9 @@
(* Title: HOL/Imperative_HOL/Imperative_HOL_ex.thy
- Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
+ Author: John Matthews, Galois Connections;
+ Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
*)
-header {* Mmonadic imperative HOL with examples *}
+header {* Monadic imperative HOL with examples *}
theory Imperative_HOL_ex
imports Imperative_HOL "ex/Imperative_Quicksort"
--- a/src/HOL/IsaMakefile Thu Jul 02 16:06:12 2009 +0200
+++ b/src/HOL/IsaMakefile Thu Jul 02 18:32:28 2009 +0200
@@ -319,7 +319,7 @@
Library/Abstract_Rat.thy \
Library/BigO.thy Library/ContNotDenum.thy Library/Efficient_Nat.thy \
Library/Euclidean_Space.thy Library/Sum_Of_Squares.thy Library/positivstellensatz.ML \
- Library/Code_Set.thy Library/Convex_Euclidean_Space.thy \
+ Library/Fset.thy Library/Convex_Euclidean_Space.thy \
Library/sum_of_squares.ML Library/Glbs.thy Library/normarith.ML \
Library/Executable_Set.thy Library/Infinite_Set.thy \
Library/FuncSet.thy Library/Permutations.thy Library/Determinants.thy\
--- a/src/HOL/Library/Code_Set.thy Thu Jul 02 16:06:12 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,169 +0,0 @@
-
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* Executable finite sets *}
-
-theory Code_Set
-imports List_Set
-begin
-
-lemma foldl_apply_inv:
- assumes "\<And>x. g (h x) = x"
- shows "foldl f (g s) xs = g (foldl (\<lambda>s x. h (f (g s) x)) s xs)"
- by (rule sym, induct xs arbitrary: s) (simp_all add: assms)
-
-subsection {* Lifting *}
-
-datatype 'a fset = Fset "'a set"
-
-primrec member :: "'a fset \<Rightarrow> 'a set" where
- "member (Fset A) = A"
-
-lemma Fset_member [simp]:
- "Fset (member A) = A"
- by (cases A) simp
-
-definition Set :: "'a list \<Rightarrow> 'a fset" where
- "Set xs = Fset (set xs)"
-
-lemma member_Set [simp]:
- "member (Set xs) = set xs"
- by (simp add: Set_def)
-
-code_datatype Set
-
-
-subsection {* Basic operations *}
-
-definition is_empty :: "'a fset \<Rightarrow> bool" where
- "is_empty A \<longleftrightarrow> List_Set.is_empty (member A)"
-
-lemma is_empty_Set [code]:
- "is_empty (Set xs) \<longleftrightarrow> null xs"
- by (simp add: is_empty_def is_empty_set)
-
-definition empty :: "'a fset" where
- "empty = Fset {}"
-
-lemma empty_Set [code]:
- "empty = Set []"
- by (simp add: empty_def Set_def)
-
-definition insert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
- "insert x A = Fset (Set.insert x (member A))"
-
-lemma insert_Set [code]:
- "insert x (Set xs) = Set (List_Set.insert x xs)"
- by (simp add: insert_def Set_def insert_set)
-
-definition remove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
- "remove x A = Fset (List_Set.remove x (member A))"
-
-lemma remove_Set [code]:
- "remove x (Set xs) = Set (remove_all x xs)"
- by (simp add: remove_def Set_def remove_set)
-
-definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" where
- "map f A = Fset (image f (member A))"
-
-lemma map_Set [code]:
- "map f (Set xs) = Set (remdups (List.map f xs))"
- by (simp add: map_def Set_def)
-
-definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
- "project P A = Fset (List_Set.project P (member A))"
-
-lemma project_Set [code]:
- "project P (Set xs) = Set (filter P xs)"
- by (simp add: project_def Set_def project_set)
-
-definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
- "forall P A \<longleftrightarrow> Ball (member A) P"
-
-lemma forall_Set [code]:
- "forall P (Set xs) \<longleftrightarrow> list_all P xs"
- by (simp add: forall_def Set_def ball_set)
-
-definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
- "exists P A \<longleftrightarrow> Bex (member A) P"
-
-lemma exists_Set [code]:
- "exists P (Set xs) \<longleftrightarrow> list_ex P xs"
- by (simp add: exists_def Set_def bex_set)
-
-
-subsection {* Functorial operations *}
-
-definition union :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
- "union A B = Fset (member A \<union> member B)"
-
-lemma union_insert [code]:
- "union (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
-proof -
- have "foldl (\<lambda>A x. Set.insert x A) (member A) xs =
- member (foldl (\<lambda>A x. Fset (Set.insert x (member A))) A xs)"
- by (rule foldl_apply_inv) simp
- then show ?thesis by (simp add: union_def union_set insert_def)
-qed
-
-definition subtract :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
- "subtract A B = Fset (member B - member A)"
-
-lemma subtract_remove [code]:
- "subtract (Set xs) A = foldl (\<lambda>A x. remove x A) A xs"
-proof -
- have "foldl (\<lambda>A x. List_Set.remove x A) (member A) xs =
- member (foldl (\<lambda>A x. Fset (List_Set.remove x (member A))) A xs)"
- by (rule foldl_apply_inv) simp
- then show ?thesis by (simp add: subtract_def minus_set remove_def)
-qed
-
-
-subsection {* Derived operations *}
-
-lemma member_exists [code]:
- "member A y \<longleftrightarrow> exists (\<lambda>x. y = x) A"
- by (simp add: exists_def mem_def)
-
-definition subfset_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where
- "subfset_eq A B \<longleftrightarrow> member A \<subseteq> member B"
-
-lemma subfset_eq_forall [code]:
- "subfset_eq A B \<longleftrightarrow> forall (\<lambda>x. member B x) A"
- by (simp add: subfset_eq_def subset_eq forall_def mem_def)
-
-definition subfset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where
- "subfset A B \<longleftrightarrow> member A \<subset> member B"
-
-lemma subfset_subfset_eq [code]:
- "subfset A B \<longleftrightarrow> subfset_eq A B \<and> \<not> subfset_eq B A"
- by (simp add: subfset_def subfset_eq_def subset)
-
-lemma eq_fset_subfset_eq [code]:
- "eq_class.eq A B \<longleftrightarrow> subfset_eq A B \<and> subfset_eq B A"
- by (cases A, cases B) (simp add: eq subfset_eq_def set_eq)
-
-definition inter :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
- "inter A B = Fset (List_Set.project (member A) (member B))"
-
-lemma inter_project [code]:
- "inter A B = project (member A) B"
- by (simp add: inter_def project_def inter)
-
-
-subsection {* Misc operations *}
-
-lemma size_fset [code]:
- "fset_size f A = 0"
- "size A = 0"
- by (cases A, simp) (cases A, simp)
-
-lemma fset_case_code [code]:
- "fset_case f A = f (member A)"
- by (cases A) simp
-
-lemma fset_rec_code [code]:
- "fset_rec f A = f (member A)"
- by (cases A) simp
-
-end
--- a/src/HOL/Library/Executable_Set.thy Thu Jul 02 16:06:12 2009 +0200
+++ b/src/HOL/Library/Executable_Set.thy Thu Jul 02 18:32:28 2009 +0200
@@ -5,249 +5,43 @@
header {* Implementation of finite sets by lists *}
theory Executable_Set
-imports Main
+imports Main Fset
begin
-subsection {* Definitional rewrites *}
+subsection {* Derived set operations *}
+
+declare member [code]
definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
"subset = op \<le>"
declare subset_def [symmetric, code unfold]
-lemma [code]: "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
- unfolding subset_def subset_eq ..
-
-definition is_empty :: "'a set \<Rightarrow> bool" where
- "is_empty A \<longleftrightarrow> A = {}"
+lemma [code]:
+ "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
+ by (simp add: subset_def subset_eq)
definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
[code del]: "eq_set = op ="
-lemma [code]: "eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
- unfolding eq_set_def by auto
-
(* FIXME allow for Stefan's code generator:
declare set_eq_subset[code unfold]
*)
lemma [code]:
- "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
- unfolding bex_triv_one_point1 ..
-
-definition filter_set :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
- "filter_set P xs = {x\<in>xs. P x}"
-
-declare filter_set_def[symmetric, code unfold]
-
-
-subsection {* Operations on lists *}
-
-subsubsection {* Basic definitions *}
-
-definition
- flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
- "flip f a b = f b a"
-
-definition
- member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
- "member xs x \<longleftrightarrow> x \<in> set xs"
-
-definition
- insertl :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
- "insertl x xs = (if member xs x then xs else x#xs)"
-
-lemma [code target: List]: "member [] y \<longleftrightarrow> False"
- and [code target: List]: "member (x#xs) y \<longleftrightarrow> y = x \<or> member xs y"
- unfolding member_def by (induct xs) simp_all
-
-fun
- drop_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
- "drop_first f [] = []"
-| "drop_first f (x#xs) = (if f x then xs else x # drop_first f xs)"
-declare drop_first.simps [code del]
-declare drop_first.simps [code target: List]
+ "eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
+ by (simp add: eq_set_def set_eq)
-declare remove1.simps [code del]
-lemma [code target: List]:
- "remove1 x xs = (if member xs x then drop_first (\<lambda>y. y = x) xs else xs)"
-proof (cases "member xs x")
- case False thus ?thesis unfolding member_def by (induct xs) auto
-next
- case True
- have "remove1 x xs = drop_first (\<lambda>y. y = x) xs" by (induct xs) simp_all
- with True show ?thesis by simp
-qed
-
-lemma member_nil [simp]:
- "member [] = (\<lambda>x. False)"
-proof (rule ext)
- fix x
- show "member [] x = False" unfolding member_def by simp
-qed
+declare inter [code]
-lemma member_insertl [simp]:
- "x \<in> set (insertl x xs)"
- unfolding insertl_def member_def mem_iff by simp
-
-lemma insertl_member [simp]:
- fixes xs x
- assumes member: "member xs x"
- shows "insertl x xs = xs"
- using member unfolding insertl_def by simp
-
-lemma insertl_not_member [simp]:
- fixes xs x
- assumes member: "\<not> (member xs x)"
- shows "insertl x xs = x # xs"
- using member unfolding insertl_def by simp
-
-lemma foldr_remove1_empty [simp]:
- "foldr remove1 xs [] = []"
- by (induct xs) simp_all
+declare Inter_image_eq [symmetric, code]
+declare Union_image_eq [symmetric, code]
-subsubsection {* Derived definitions *}
-
-function unionl :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
-where
- "unionl [] ys = ys"
-| "unionl xs ys = foldr insertl xs ys"
-by pat_completeness auto
-termination by lexicographic_order
-
-lemmas unionl_eq = unionl.simps(2)
-
-function intersect :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
-where
- "intersect [] ys = []"
-| "intersect xs [] = []"
-| "intersect xs ys = filter (member xs) ys"
-by pat_completeness auto
-termination by lexicographic_order
-
-lemmas intersect_eq = intersect.simps(3)
-
-function subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
-where
- "subtract [] ys = ys"
-| "subtract xs [] = []"
-| "subtract xs ys = foldr remove1 xs ys"
-by pat_completeness auto
-termination by lexicographic_order
-
-lemmas subtract_eq = subtract.simps(3)
-
-function map_distinct :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
-where
- "map_distinct f [] = []"
-| "map_distinct f xs = foldr (insertl o f) xs []"
-by pat_completeness auto
-termination by lexicographic_order
-
-lemmas map_distinct_eq = map_distinct.simps(2)
-
-function unions :: "'a list list \<Rightarrow> 'a list"
-where
- "unions [] = []"
-| "unions xs = foldr unionl xs []"
-by pat_completeness auto
-termination by lexicographic_order
-
-lemmas unions_eq = unions.simps(2)
-
-consts intersects :: "'a list list \<Rightarrow> 'a list"
-primrec
- "intersects (x#xs) = foldr intersect xs x"
-
-definition
- map_union :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
- "map_union xs f = unions (map f xs)"
-
-definition
- map_inter :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
- "map_inter xs f = intersects (map f xs)"
-
-
-subsection {* Isomorphism proofs *}
-
-lemma iso_member:
- "member xs x \<longleftrightarrow> x \<in> set xs"
- unfolding member_def mem_iff ..
+subsection {* Rewrites for primitive operations *}
-lemma iso_insert:
- "set (insertl x xs) = insert x (set xs)"
- unfolding insertl_def iso_member by (simp add: insert_absorb)
-
-lemma iso_remove1:
- assumes distnct: "distinct xs"
- shows "set (remove1 x xs) = set xs - {x}"
- using distnct set_remove1_eq by auto
-
-lemma iso_union:
- "set (unionl xs ys) = set xs \<union> set ys"
- unfolding unionl_eq
- by (induct xs arbitrary: ys) (simp_all add: iso_insert)
-
-lemma iso_intersect:
- "set (intersect xs ys) = set xs \<inter> set ys"
- unfolding intersect_eq Int_def by (simp add: Int_def iso_member) auto
-
-definition
- subtract' :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
- "subtract' = flip subtract"
-
-lemma iso_subtract:
- fixes ys
- assumes distnct: "distinct ys"
- shows "set (subtract' ys xs) = set ys - set xs"
- and "distinct (subtract' ys xs)"
- unfolding subtract'_def flip_def subtract_eq
- using distnct by (induct xs arbitrary: ys) auto
-
-lemma iso_map_distinct:
- "set (map_distinct f xs) = image f (set xs)"
- unfolding map_distinct_eq by (induct xs) (simp_all add: iso_insert)
+declare List_Set.project_def [symmetric, code unfold]
-lemma iso_unions:
- "set (unions xss) = \<Union> set (map set xss)"
- unfolding unions_eq
-proof (induct xss)
- case Nil show ?case by simp
-next
- case (Cons xs xss) thus ?case by (induct xs) (simp_all add: iso_insert)
-qed
-
-lemma iso_intersects:
- "set (intersects (xs#xss)) = \<Inter> set (map set (xs#xss))"
- by (induct xss) (simp_all add: Int_def iso_member, auto)
-
-lemma iso_UNION:
- "set (map_union xs f) = UNION (set xs) (set o f)"
- unfolding map_union_def iso_unions by simp
-
-lemma iso_INTER:
- "set (map_inter (x#xs) f) = INTER (set (x#xs)) (set o f)"
- unfolding map_inter_def iso_intersects by (induct xs) (simp_all add: iso_member, auto)
-
-definition
- Blall :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
- "Blall = flip list_all"
-definition
- Blex :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
- "Blex = flip list_ex"
-
-lemma iso_Ball:
- "Blall xs f = Ball (set xs) f"
- unfolding Blall_def flip_def by (induct xs) simp_all
-
-lemma iso_Bex:
- "Blex xs f = Bex (set xs) f"
- unfolding Blex_def flip_def by (induct xs) simp_all
-
-lemma iso_filter:
- "set (filter P xs) = filter_set P (set xs)"
- unfolding filter_set_def by (induct xs) auto
subsection {* code generator setup *}
@@ -257,23 +51,33 @@
nonfix subset;
*}
-subsubsection {* const serializations *}
+definition flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
+ "flip f a b = f b a"
+
+types_code
+ fset ("(_/ \<module>fset)")
+attach {*
+datatype 'a fset = Set of 'a list;
+*}
+
+consts_code
+ Set ("\<module>Set")
consts_code
- "Set.empty" ("{*[]*}")
- insert ("{*insertl*}")
- is_empty ("{*null*}")
- "op \<union>" ("{*unionl*}")
- "op \<inter>" ("{*intersect*}")
- "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{* flip subtract *}")
- image ("{*map_distinct*}")
- Union ("{*unions*}")
- Inter ("{*intersects*}")
- UNION ("{*map_union*}")
- INTER ("{*map_inter*}")
- Ball ("{*Blall*}")
- Bex ("{*Blex*}")
- filter_set ("{*filter*}")
- fold ("{* foldl o flip *}")
+ "Set.empty" ("{*Fset.empty*}")
+ "List_Set.is_empty" ("{*Fset.is_empty*}")
+ "Set.insert" ("{*Fset.insert*}")
+ "List_Set.remove" ("{*Fset.remove*}")
+ "Set.image" ("{*Fset.map*}")
+ "List_Set.project" ("{*Fset.filter*}")
+ "Ball" ("{*flip Fset.forall*}")
+ "Bex" ("{*flip Fset.exists*}")
+ "op \<union>" ("{*Fset.union*}")
+ "op \<inter>" ("{*Fset.inter*}")
+ "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip Fset.subtract*}")
+ "Set.Union" ("{*Fset.Union*}")
+ "Set.Inter" ("{*Fset.Inter*}")
+ card ("{*Fset.card*}")
+ fold ("{*foldl o flip*}")
-end
+end
\ No newline at end of file
--- a/src/HOL/Library/Float.thy Thu Jul 02 16:06:12 2009 +0200
+++ b/src/HOL/Library/Float.thy Thu Jul 02 18:32:28 2009 +0200
@@ -59,6 +59,12 @@
"real (Float -1 0) = -1" and "real (Float (number_of n) 0) = number_of n"
by auto
+lemma float_number_of[simp]: "real (number_of x :: float) = number_of x"
+ by (simp only:number_of_float_def Float_num[unfolded number_of_is_id])
+
+lemma float_number_of_int[simp]: "real (Float n 0) = real n"
+ by (simp add: Float_num[unfolded number_of_is_id] real_of_float_simp pow2_def)
+
lemma pow2_0[simp]: "pow2 0 = 1" by simp
lemma pow2_1[simp]: "pow2 1 = 2" by simp
lemma pow2_neg: "pow2 x = inverse (pow2 (-x))" by simp
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Fset.thy Thu Jul 02 18:32:28 2009 +0200
@@ -0,0 +1,240 @@
+
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Executable finite sets *}
+
+theory Fset
+imports List_Set
+begin
+
+lemma foldl_apply_inv:
+ assumes "\<And>x. g (h x) = x"
+ shows "foldl f (g s) xs = g (foldl (\<lambda>s x. h (f (g s) x)) s xs)"
+ by (rule sym, induct xs arbitrary: s) (simp_all add: assms)
+
+declare mem_def [simp]
+
+
+subsection {* Lifting *}
+
+datatype 'a fset = Fset "'a set"
+
+primrec member :: "'a fset \<Rightarrow> 'a set" where
+ "member (Fset A) = A"
+
+lemma Fset_member [simp]:
+ "Fset (member A) = A"
+ by (cases A) simp
+
+definition Set :: "'a list \<Rightarrow> 'a fset" where
+ "Set xs = Fset (set xs)"
+
+lemma member_Set [simp]:
+ "member (Set xs) = set xs"
+ by (simp add: Set_def)
+
+code_datatype Set
+
+
+subsection {* Basic operations *}
+
+definition is_empty :: "'a fset \<Rightarrow> bool" where
+ [simp]: "is_empty A \<longleftrightarrow> List_Set.is_empty (member A)"
+
+lemma is_empty_Set [code]:
+ "is_empty (Set xs) \<longleftrightarrow> null xs"
+ by (simp add: is_empty_set)
+
+definition empty :: "'a fset" where
+ [simp]: "empty = Fset {}"
+
+lemma empty_Set [code]:
+ "empty = Set []"
+ by (simp add: Set_def)
+
+definition insert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
+ [simp]: "insert x A = Fset (Set.insert x (member A))"
+
+lemma insert_Set [code]:
+ "insert x (Set xs) = Set (List_Set.insert x xs)"
+ by (simp add: Set_def insert_set)
+
+definition remove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
+ [simp]: "remove x A = Fset (List_Set.remove x (member A))"
+
+lemma remove_Set [code]:
+ "remove x (Set xs) = Set (remove_all x xs)"
+ by (simp add: Set_def remove_set)
+
+definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" where
+ [simp]: "map f A = Fset (image f (member A))"
+
+lemma map_Set [code]:
+ "map f (Set xs) = Set (remdups (List.map f xs))"
+ by (simp add: Set_def)
+
+definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
+ [simp]: "filter P A = Fset (List_Set.project P (member A))"
+
+lemma filter_Set [code]:
+ "filter P (Set xs) = Set (List.filter P xs)"
+ by (simp add: Set_def project_set)
+
+definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
+ [simp]: "forall P A \<longleftrightarrow> Ball (member A) P"
+
+lemma forall_Set [code]:
+ "forall P (Set xs) \<longleftrightarrow> list_all P xs"
+ by (simp add: Set_def ball_set)
+
+definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
+ [simp]: "exists P A \<longleftrightarrow> Bex (member A) P"
+
+lemma exists_Set [code]:
+ "exists P (Set xs) \<longleftrightarrow> list_ex P xs"
+ by (simp add: Set_def bex_set)
+
+definition card :: "'a fset \<Rightarrow> nat" where
+ [simp]: "card A = Finite_Set.card (member A)"
+
+lemma card_Set [code]:
+ "card (Set xs) = length (remdups xs)"
+proof -
+ have "Finite_Set.card (set (remdups xs)) = length (remdups xs)"
+ by (rule distinct_card) simp
+ then show ?thesis by (simp add: Set_def card_def)
+qed
+
+
+subsection {* Derived operations *}
+
+lemma member_exists [code]:
+ "member A y \<longleftrightarrow> exists (\<lambda>x. y = x) A"
+ by simp
+
+definition subfset_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where
+ [simp]: "subfset_eq A B \<longleftrightarrow> member A \<subseteq> member B"
+
+lemma subfset_eq_forall [code]:
+ "subfset_eq A B \<longleftrightarrow> forall (\<lambda>x. member B x) A"
+ by (simp add: subset_eq)
+
+definition subfset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where
+ [simp]: "subfset A B \<longleftrightarrow> member A \<subset> member B"
+
+lemma subfset_subfset_eq [code]:
+ "subfset A B \<longleftrightarrow> subfset_eq A B \<and> \<not> subfset_eq B A"
+ by (simp add: subset)
+
+lemma eq_fset_subfset_eq [code]:
+ "eq_class.eq A B \<longleftrightarrow> subfset_eq A B \<and> subfset_eq B A"
+ by (cases A, cases B) (simp add: eq set_eq)
+
+definition inter :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
+ [simp]: "inter A B = Fset (project (member A) (member B))"
+
+lemma inter_project [code]:
+ "inter A B = filter (member A) B"
+ by (simp add: inter)
+
+
+subsection {* Functorial operations *}
+
+definition union :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
+ [simp]: "union A B = Fset (member A \<union> member B)"
+
+lemma union_insert [code]:
+ "union (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
+proof -
+ have "foldl (\<lambda>A x. Set.insert x A) (member A) xs =
+ member (foldl (\<lambda>A x. Fset (Set.insert x (member A))) A xs)"
+ by (rule foldl_apply_inv) simp
+ then show ?thesis by (simp add: union_set)
+qed
+
+definition subtract :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
+ [simp]: "subtract A B = Fset (member B - member A)"
+
+lemma subtract_remove [code]:
+ "subtract (Set xs) A = foldl (\<lambda>A x. remove x A) A xs"
+proof -
+ have "foldl (\<lambda>A x. List_Set.remove x A) (member A) xs =
+ member (foldl (\<lambda>A x. Fset (List_Set.remove x (member A))) A xs)"
+ by (rule foldl_apply_inv) simp
+ then show ?thesis by (simp add: minus_set)
+qed
+
+definition Inter :: "'a fset fset \<Rightarrow> 'a fset" where
+ [simp]: "Inter A = Fset (Set.Inter (member ` member A))"
+
+lemma Inter_inter [code]:
+ "Inter (Set (A # As)) = foldl inter A As"
+proof -
+ note Inter_image_eq [simp del] set_map [simp del] set.simps [simp del]
+ have "foldl (op \<inter>) (member A) (List.map member As) =
+ member (foldl (\<lambda>B A. Fset (member B \<inter> A)) A (List.map member As))"
+ by (rule foldl_apply_inv) simp
+ then show ?thesis
+ by (simp add: Inter_set image_set inter_def_raw inter foldl_map)
+qed
+
+definition Union :: "'a fset fset \<Rightarrow> 'a fset" where
+ [simp]: "Union A = Fset (Set.Union (member ` member A))"
+
+lemma Union_union [code]:
+ "Union (Set As) = foldl union empty As"
+proof -
+ note Union_image_eq [simp del] set_map [simp del]
+ have "foldl (op \<union>) (member empty) (List.map member As) =
+ member (foldl (\<lambda>B A. Fset (member B \<union> A)) empty (List.map member As))"
+ by (rule foldl_apply_inv) simp
+ then show ?thesis
+ by (simp add: Union_set image_set union_def_raw foldl_map)
+qed
+
+
+subsection {* Misc operations *}
+
+lemma size_fset [code]:
+ "fset_size f A = 0"
+ "size A = 0"
+ by (cases A, simp) (cases A, simp)
+
+lemma fset_case_code [code]:
+ "fset_case f A = f (member A)"
+ by (cases A) simp
+
+lemma fset_rec_code [code]:
+ "fset_rec f A = f (member A)"
+ by (cases A) simp
+
+
+subsection {* Simplified simprules *}
+
+lemma is_empty_simp [simp]:
+ "is_empty A \<longleftrightarrow> member A = {}"
+ by (simp add: List_Set.is_empty_def)
+declare is_empty_def [simp del]
+
+lemma remove_simp [simp]:
+ "remove x A = Fset (member A - {x})"
+ by (simp add: List_Set.remove_def)
+declare remove_def [simp del]
+
+lemma filter_simp [simp]:
+ "filter P A = Fset {x \<in> member A. P x}"
+ by (simp add: List_Set.project_def)
+declare filter_def [simp del]
+
+lemma inter_simp [simp]:
+ "inter A B = Fset (member A \<inter> member B)"
+ by (simp add: inter)
+declare inter_def [simp del]
+
+declare mem_def [simp del]
+
+
+hide (open) const is_empty empty insert remove map filter forall exists card
+ subfset_eq subfset inter union subtract Inter Union
+
+end
--- a/src/HOL/Library/Library.thy Thu Jul 02 16:06:12 2009 +0200
+++ b/src/HOL/Library/Library.thy Thu Jul 02 18:32:28 2009 +0200
@@ -10,7 +10,6 @@
Char_ord
Code_Char_chr
Code_Integer
- Code_Set
Coinductive_List
Commutative_Ring
Continuity
@@ -28,6 +27,7 @@
Formal_Power_Series
Fraction_Field
FrechetDeriv
+ Fset
FuncSet
Fundamental_Theorem_Algebra
Infinite_Set
--- a/src/HOL/Library/List_Set.thy Thu Jul 02 16:06:12 2009 +0200
+++ b/src/HOL/Library/List_Set.thy Thu Jul 02 18:32:28 2009 +0200
@@ -70,7 +70,7 @@
by (auto simp add: remove_def remove_all_def)
lemma image_set:
- "image f (set xs) = set (remdups (map f xs))"
+ "image f (set xs) = set (map f xs)"
by simp
lemma project_set:
@@ -160,4 +160,7 @@
"A \<inter> B = project (\<lambda>x. x \<in> A) B"
by (auto simp add: project_def)
+
+hide (open) const insert
+
end
\ No newline at end of file
--- a/src/HOL/Library/Poly_Deriv.thy Thu Jul 02 16:06:12 2009 +0200
+++ b/src/HOL/Library/Poly_Deriv.thy Thu Jul 02 18:32:28 2009 +0200
@@ -85,13 +85,7 @@
by (rule lemma_DERIV_subst, rule DERIV_add, auto)
lemma poly_DERIV[simp]: "DERIV (%x. poly p x) x :> poly (pderiv p) x"
-apply (induct p)
-apply simp
-apply (simp add: pderiv_pCons)
-apply (rule lemma_DERIV_subst)
-apply (rule DERIV_add DERIV_mult DERIV_const DERIV_ident | assumption)+
-apply simp
-done
+ by (induct p, auto intro!: DERIV_intros simp add: pderiv_pCons)
text{* Consequences of the derivative theorem above*}
--- a/src/HOL/Ln.thy Thu Jul 02 16:06:12 2009 +0200
+++ b/src/HOL/Ln.thy Thu Jul 02 18:32:28 2009 +0200
@@ -343,43 +343,7 @@
done
lemma DERIV_ln: "0 < x ==> DERIV ln x :> 1 / x"
- apply (unfold deriv_def, unfold LIM_eq, clarsimp)
- apply (rule exI)
- apply (rule conjI)
- prefer 2
- apply clarsimp
- apply (subgoal_tac "(ln (x + xa) - ln x) / xa - (1 / x) =
- (ln (1 + xa / x) - xa / x) / xa")
- apply (erule ssubst)
- apply (subst abs_divide)
- apply (rule mult_imp_div_pos_less)
- apply force
- apply (rule order_le_less_trans)
- apply (rule abs_ln_one_plus_x_minus_x_bound)
- apply (subst abs_divide)
- apply (subst abs_of_pos, assumption)
- apply (erule mult_imp_div_pos_le)
- apply (subgoal_tac "abs xa < min (x / 2) (r * x^2 / 2)")
- apply force
- apply assumption
- apply (simp add: power2_eq_square mult_compare_simps)
- apply (rule mult_imp_div_pos_less)
- apply (rule mult_pos_pos, assumption, assumption)
- apply (subgoal_tac "xa * xa = abs xa * abs xa")
- apply (erule ssubst)
- apply (subgoal_tac "abs xa * (abs xa * 2) < abs xa * (r * (x * x))")
- apply (simp only: mult_ac)
- apply (rule mult_strict_left_mono)
- apply (erule conjE, assumption)
- apply force
- apply simp
- apply (subst ln_div [THEN sym])
- apply arith
- apply (auto simp add: algebra_simps add_frac_eq frac_eq_eq
- add_divide_distrib power2_eq_square)
- apply (rule mult_pos_pos, assumption)+
- apply assumption
-done
+ by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse)
lemma ln_x_over_x_mono: "exp 1 <= x ==> x <= y ==> (ln y / y) <= (ln x / x)"
proof -
--- a/src/HOL/MacLaurin.thy Thu Jul 02 16:06:12 2009 +0200
+++ b/src/HOL/MacLaurin.thy Thu Jul 02 18:32:28 2009 +0200
@@ -27,36 +27,6 @@
lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))"
by arith
-text{*A crude tactic to differentiate by proof.*}
-
-lemmas deriv_rulesI =
- DERIV_ident DERIV_const DERIV_cos DERIV_cmult
- DERIV_sin DERIV_exp DERIV_inverse DERIV_pow
- DERIV_add DERIV_diff DERIV_mult DERIV_minus
- DERIV_inverse_fun DERIV_quotient DERIV_fun_pow
- DERIV_fun_exp DERIV_fun_sin DERIV_fun_cos
- DERIV_ident DERIV_const DERIV_cos
-
-ML
-{*
-local
-exception DERIV_name;
-fun get_fun_name (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _)) = f
-| get_fun_name (_ $ (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _))) = f
-| get_fun_name _ = raise DERIV_name;
-
-in
-
-fun deriv_tac ctxt = SUBGOAL (fn (prem, i) =>
- resolve_tac @{thms deriv_rulesI} i ORELSE
- ((rtac (read_instantiate ctxt [(("f", 0), get_fun_name prem)]
- @{thm DERIV_chain2}) i) handle DERIV_name => no_tac));
-
-fun DERIV_tac ctxt = ALLGOALS (fn i => REPEAT (deriv_tac ctxt i));
-
-end
-*}
-
lemma Maclaurin_lemma2:
assumes diff: "\<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
assumes n: "n = Suc k"
@@ -91,13 +61,12 @@
apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc power_Suc)
apply (rule DERIV_cmult)
apply (rule lemma_DERIV_subst)
- apply (best intro: DERIV_chain2 intro!: DERIV_intros)
+ apply (best intro!: DERIV_intros)
apply (subst fact_Suc)
apply (subst real_of_nat_mult)
apply (simp add: mult_ac)
done
-
lemma Maclaurin:
assumes h: "0 < h"
assumes n: "0 < n"
@@ -565,9 +534,7 @@
apply (clarify)
apply (subst (1 2 3) mod_Suc_eq_Suc_mod)
apply (cut_tac m=m in mod_exhaust_less_4)
- apply (safe, simp_all)
- apply (rule DERIV_minus, simp)
- apply (rule lemma_DERIV_subst, rule DERIV_minus, rule DERIV_cos, simp)
+ apply (safe, auto intro!: DERIV_intros)
done
from Maclaurin_all_le [OF diff_0 DERIV_diff]
obtain t where t1: "\<bar>t\<bar> \<le> \<bar>x\<bar>" and
--- a/src/HOL/MicroJava/BV/BVExample.thy Thu Jul 02 16:06:12 2009 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy Thu Jul 02 18:32:28 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/MicroJava/BV/BVExample.thy
- ID: $Id$
Author: Gerwin Klein
*)
@@ -94,7 +93,7 @@
text {* Method and field lookup: *}
lemma method_Object [simp]:
- "method (E, Object) = empty"
+ "method (E, Object) = Map.empty"
by (simp add: method_rec_lemma [OF class_Object wf_subcls1_E])
lemma method_append [simp]:
@@ -436,7 +435,7 @@
"some_elem = (%S. SOME x. x : S)"
consts_code
- "some_elem" ("hd")
+ "some_elem" ("(case/ _ of/ {*Set*}/ xs/ =>/ hd/ xs)")
text {* This code setup is just a demonstration and \emph{not} sound! *}
@@ -451,11 +450,11 @@
qed
lemma [code]:
- "iter f step ss w = while (\<lambda>(ss, w). \<not> (is_empty w))
+ "iter f step ss w = while (\<lambda>(ss, w). \<not> is_empty w)
(\<lambda>(ss, w).
let p = some_elem w in propa f (step p (ss ! p)) ss (w - {p}))
(ss, w)"
- unfolding iter_def is_empty_def some_elem_def ..
+ unfolding iter_def List_Set.is_empty_def some_elem_def ..
lemma JVM_sup_unfold [code]:
"JVMType.sup S m n = lift2 (Opt.sup
@@ -475,7 +474,6 @@
test1 = "test_kil E list_name [Class list_name] (PrimT Void) 3 0
[(Suc 0, 2, 8, Xcpt NullPointer)] append_ins"
test2 = "test_kil E test_name [] (PrimT Void) 3 2 [] make_list_ins"
-
ML BV.test1
ML BV.test2
--- a/src/HOL/NthRoot.thy Thu Jul 02 16:06:12 2009 +0200
+++ b/src/HOL/NthRoot.thy Thu Jul 02 18:32:28 2009 +0200
@@ -372,6 +372,41 @@
using odd_pos [OF n] by (rule isCont_real_root)
qed
+lemma DERIV_even_real_root:
+ assumes n: "0 < n" and "even n"
+ assumes x: "x < 0"
+ shows "DERIV (root n) x :> inverse (- real n * root n x ^ (n - Suc 0))"
+proof (rule DERIV_inverse_function)
+ show "x - 1 < x" by simp
+ show "x < 0" using x .
+next
+ show "\<forall>y. x - 1 < y \<and> y < 0 \<longrightarrow> - (root n y ^ n) = y"
+ proof (rule allI, rule impI, erule conjE)
+ fix y assume "x - 1 < y" and "y < 0"
+ hence "root n (-y) ^ n = -y" using `0 < n` by simp
+ with real_root_minus[OF `0 < n`] and `even n`
+ show "- (root n y ^ n) = y" by simp
+ qed
+next
+ show "DERIV (\<lambda>x. - (x ^ n)) (root n x) :> - real n * root n x ^ (n - Suc 0)"
+ by (auto intro!: DERIV_intros)
+ show "- real n * root n x ^ (n - Suc 0) \<noteq> 0"
+ using n x by simp
+ show "isCont (root n) x"
+ using n by (rule isCont_real_root)
+qed
+
+lemma DERIV_real_root_generic:
+ assumes "0 < n" and "x \<noteq> 0"
+ and even: "\<lbrakk> even n ; 0 < x \<rbrakk> \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
+ and even: "\<lbrakk> even n ; x < 0 \<rbrakk> \<Longrightarrow> D = - inverse (real n * root n x ^ (n - Suc 0))"
+ and odd: "odd n \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
+ shows "DERIV (root n) x :> D"
+using assms by (cases "even n", cases "0 < x",
+ auto intro: DERIV_real_root[THEN DERIV_cong]
+ DERIV_odd_real_root[THEN DERIV_cong]
+ DERIV_even_real_root[THEN DERIV_cong])
+
subsection {* Square Root *}
definition
@@ -456,9 +491,21 @@
lemma isCont_real_sqrt: "isCont sqrt x"
unfolding sqrt_def by (rule isCont_real_root [OF pos2])
+lemma DERIV_real_sqrt_generic:
+ assumes "x \<noteq> 0"
+ assumes "x > 0 \<Longrightarrow> D = inverse (sqrt x) / 2"
+ assumes "x < 0 \<Longrightarrow> D = - inverse (sqrt x) / 2"
+ shows "DERIV sqrt x :> D"
+ using assms unfolding sqrt_def
+ by (auto intro!: DERIV_real_root_generic)
+
lemma DERIV_real_sqrt:
"0 < x \<Longrightarrow> DERIV sqrt x :> inverse (sqrt x) / 2"
-unfolding sqrt_def by (rule DERIV_real_root [OF pos2, simplified])
+ using DERIV_real_sqrt_generic by simp
+
+declare
+ DERIV_real_sqrt_generic[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+ DERIV_real_root_generic[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
lemma not_real_square_gt_zero [simp]: "(~ (0::real) < x*x) = (x = 0)"
apply auto
--- a/src/HOL/Tools/Datatype/datatype.ML Thu Jul 02 16:06:12 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML Thu Jul 02 18:32:28 2009 +0200
@@ -18,7 +18,7 @@
val the_info : theory -> string -> info
val the_descr : theory -> string list
-> descr * (string * sort) list * string list
- * (string list * string list) * (typ list * typ list)
+ * string * (string list * string list) * (typ list * typ list)
val the_spec : theory -> string -> (string * sort) list * (string * typ list) list
val get_constrs : theory -> string -> (string * typ) list option
val get_all : theory -> info Symtab.table
@@ -125,9 +125,10 @@
val names = map Long_Name.base_name (the_default tycos (#alt_names info));
val (auxnames, _) = Name.make_context names
- |> fold_map (yield_singleton Name.variants o name_of_typ) Us
+ |> fold_map (yield_singleton Name.variants o name_of_typ) Us;
+ val prefix = space_implode "_" names;
- in (descr, vs, tycos, (names, auxnames), (Ts, Us)) end;
+ in (descr, vs, tycos, prefix, (names, auxnames), (Ts, Us)) end;
fun get_constrs thy dtco =
case try (the_spec thy) dtco
--- a/src/HOL/Tools/dseq.ML Thu Jul 02 16:06:12 2009 +0200
+++ b/src/HOL/Tools/dseq.ML Thu Jul 02 18:32:28 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/Tools/dseq.ML
- ID: $Id$
Author: Stefan Berghofer, TU Muenchen
Sequences with recursion depth limit.
--- a/src/HOL/Tools/inductive_codegen.ML Thu Jul 02 16:06:12 2009 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Thu Jul 02 18:32:28 2009 +0200
@@ -378,7 +378,7 @@
end
| compile_prems out_ts vs names ps gr =
let
- val vs' = distinct (op =) (List.concat (vs :: map term_vs out_ts));
+ val vs' = distinct (op =) (flat (vs :: map term_vs out_ts));
val SOME (p, mode as SOME (Mode (_, js, _))) =
select_mode_prem thy modes' vs' ps;
val ps' = filter_out (equal p) ps;
@@ -404,7 +404,9 @@
(compile_expr thy defs dep module false modes
(mode, t) gr2)
else
- apfst (fn p => [str "DSeq.of_list", Pretty.brk 1, p])
+ apfst (fn p => Pretty.breaks [str "DSeq.of_list", str "(case", p,
+ str "of", str "Set", str "xs", str "=>", str "xs)"])
+ (*this is a very strong assumption about the generated code!*)
(invoke_codegen thy defs dep module true t gr2);
val (rest, gr4) = compile_prems out_ts''' vs' (fst nvs) ps' gr3;
in
@@ -661,8 +663,10 @@
let val (call_p, gr') = mk_ind_call thy defs dep module true
s T (ts1 @ ts2') names thyname k intrs gr
in SOME ((if brack then parens else I) (Pretty.block
- [str "DSeq.list_of", Pretty.brk 1, str "(",
- conv_ntuple fs ots call_p, str ")"]), gr')
+ [str "Set", Pretty.brk 1, str "(DSeq.list_of", Pretty.brk 1, str "(",
+ conv_ntuple fs ots call_p, str "))"]),
+ (*this is a very strong assumption about the generated code!*)
+ gr')
end
else NONE
end
--- a/src/HOL/Tools/quickcheck_generators.ML Thu Jul 02 16:06:12 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Thu Jul 02 18:32:28 2009 +0200
@@ -11,10 +11,10 @@
-> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
-> seed -> (('a -> 'b) * (unit -> Term.term)) * seed
val ensure_random_typecopy: string -> theory -> theory
- val random_aux_specification: string -> term list -> local_theory -> local_theory
+ val random_aux_specification: string -> string -> term list -> local_theory -> local_theory
val mk_random_aux_eqs: theory -> Datatype.descr -> (string * sort) list
-> string list -> string list * string list -> typ list * typ list
- -> string * (term list * (term * term) list)
+ -> term list * (term * term) list
val ensure_random_datatype: Datatype.config -> string list -> theory -> theory
val eval_ref: (unit -> int -> seed -> term list option * seed) option ref
val setup: theory -> theory
@@ -184,18 +184,18 @@
end;
-fun random_aux_primrec_multi prefix [eq] lthy =
+fun random_aux_primrec_multi auxname [eq] lthy =
lthy
|> random_aux_primrec eq
|>> (fn simp => [simp])
- | random_aux_primrec_multi prefix (eqs as _ :: _ :: _) lthy =
+ | random_aux_primrec_multi auxname (eqs as _ :: _ :: _) lthy =
let
val thy = ProofContext.theory_of lthy;
val (lhss, rhss) = map_split (HOLogic.dest_eq o HOLogic.dest_Trueprop) eqs;
val (vs, (arg as Free (v, _)) :: _) = map_split (fn (t1 $ t2) => (t1, t2)) lhss;
val Ts = map fastype_of lhss;
val tupleT = foldr1 HOLogic.mk_prodT Ts;
- val aux_lhs = Free ("mutual_" ^ prefix, fastype_of arg --> tupleT) $ arg;
+ val aux_lhs = Free ("mutual_" ^ auxname, fastype_of arg --> tupleT) $ arg;
val aux_eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
(aux_lhs, foldr1 HOLogic.mk_prod rhss);
fun mk_proj t [T] = [t]
@@ -223,7 +223,7 @@
|-> (fn (aux_simp, proj_defs) => prove_eqs aux_simp proj_defs)
end;
-fun random_aux_specification prefix eqs lthy =
+fun random_aux_specification prfx name eqs lthy =
let
val vs = fold Term.add_free_names ((snd o strip_comb o fst o HOLogic.dest_eq
o HOLogic.dest_Trueprop o hd) eqs) [];
@@ -237,10 +237,10 @@
val ext_simps = map (fn thm => fun_cong OF [fun_cong OF [thm]]) proto_simps;
val tac = ALLGOALS (ProofContext.fact_tac ext_simps);
in (map (fn prop => SkipProof.prove lthy vs [] prop (K tac)) eqs, lthy) end;
- val b = Binding.qualify true prefix (Binding.name "simps");
+ val b = Binding.qualify true prfx (Binding.qualify true name (Binding.name "simps"));
in
lthy
- |> random_aux_primrec_multi prefix proto_eqs
+ |> random_aux_primrec_multi (name ^ prfx) proto_eqs
|-> (fn proto_simps => prove_simps proto_simps)
|-> (fn simps => LocalTheory.note Thm.generatedK ((b,
Code.add_default_eqn_attrib :: map (Attrib.internal o K)
@@ -252,6 +252,8 @@
(* constructing random instances on datatypes *)
+val random_auxN = "random_aux";
+
fun mk_random_aux_eqs thy descr vs tycos (names, auxnames) (Ts, Us) =
let
val mk_const = curry (Sign.mk_const thy);
@@ -259,7 +261,6 @@
val i1 = @{term "(i\<Colon>code_numeral) - 1"};
val j = @{term "j\<Colon>code_numeral"};
val seed = @{term "s\<Colon>Random.seed"};
- val random_auxN = "random_aux";
val random_auxsN = map (prefix (random_auxN ^ "_")) (names @ auxnames);
fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit \<Rightarrow> term"});
val rTs = Ts @ Us;
@@ -316,10 +317,9 @@
$ seed;
val auxs_lhss = map (fn t => t $ i $ j $ seed) random_auxs;
val auxs_rhss = map mk_select gen_exprss;
- val prefix = space_implode "_" (random_auxN :: names);
- in (prefix, (random_auxs, auxs_lhss ~~ auxs_rhss)) end;
+ in (random_auxs, auxs_lhss ~~ auxs_rhss) end;
-fun mk_random_datatype config descr vs tycos (names, auxnames) (Ts, Us) thy =
+fun mk_random_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
let
val _ = DatatypeAux.message config "Creating quickcheck generators ...";
val i = @{term "i\<Colon>code_numeral"};
@@ -329,14 +329,14 @@
else @{term "max :: code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"}
$ HOLogic.mk_number @{typ code_numeral} l $ i
| NONE => i;
- val (prefix, (random_auxs, auxs_eqs)) = (apsnd o apsnd o map) mk_prop_eq
+ val (random_auxs, auxs_eqs) = (apsnd o map) mk_prop_eq
(mk_random_aux_eqs thy descr vs tycos (names, auxnames) (Ts, Us));
val random_defs = map_index (fn (k, T) => mk_prop_eq
(HOLogic.mk_random T i, nth random_auxs k $ mk_size_arg k $ i)) Ts;
in
thy
|> TheoryTarget.instantiation (tycos, vs, @{sort random})
- |> random_aux_specification prefix auxs_eqs
+ |> random_aux_specification prfx random_auxN auxs_eqs
|> `(fn lthy => map (Syntax.check_term lthy) random_defs)
|-> (fn random_defs' => fold_map (fn random_def =>
Specification.definition (NONE, (Attrib.empty_binding,
@@ -359,7 +359,7 @@
let
val pp = Syntax.pp_global thy;
val algebra = Sign.classes_of thy;
- val (descr, raw_vs, tycos, (names, auxnames), raw_TUs) =
+ val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) =
Datatype.the_descr thy raw_tycos;
val typrep_vs = (map o apsnd)
(curry (Sorts.inter_sort algebra) @{sort typerep}) raw_vs;
@@ -374,7 +374,7 @@
in if has_inst then thy
else case perhaps_constrain thy (random_insts @ term_of_insts) typrep_vs
of SOME constrain => mk_random_datatype config descr
- (map constrain typrep_vs) tycos (names, auxnames)
+ (map constrain typrep_vs) tycos prfx (names, auxnames)
((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
| NONE => thy
end;
--- a/src/HOL/Tools/res_atp.ML Thu Jul 02 16:06:12 2009 +0200
+++ b/src/HOL/Tools/res_atp.ML Thu Jul 02 18:32:28 2009 +0200
@@ -11,8 +11,9 @@
val prepare_clauses : bool -> thm list -> thm list ->
(thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list ->
(thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list -> theory ->
- ResHolClause.axiom_name vector * (ResHolClause.clause list * ResHolClause.clause list *
- ResHolClause.clause list * ResClause.classrelClause list * ResClause.arityClause list)
+ ResHolClause.axiom_name vector *
+ (ResHolClause.clause list * ResHolClause.clause list * ResHolClause.clause list *
+ ResHolClause.clause list * ResClause.classrelClause list * ResClause.arityClause list)
end;
structure ResAtp: RES_ATP =
@@ -218,8 +219,7 @@
handle ConstFree => false
in
case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ rhs) =>
- defs lhs rhs andalso
- (Output.debug (fn () => "Definition found: " ^ name ^ "_" ^ Int.toString n); true)
+ defs lhs rhs
| _ => false
end;
@@ -275,8 +275,7 @@
fun relevance_filter max_new theory_const thy axioms goals =
if run_relevance_filter andalso pass_mark >= 0.1
then
- let val _ = Output.debug (fn () => "Start of relevance filtering");
- val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms
+ let val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms
val goal_const_tab = get_goal_consts_typs thy goals
val _ = Output.debug (fn () => ("Initial constants: " ^
space_implode ", " (Symtab.keys goal_const_tab)));
@@ -405,8 +404,6 @@
fun check_named ("",th) = (warning ("No name for theorem " ^ Display.string_of_thm th); false)
| check_named (_,th) = true;
-fun display_thm (name,th) = Output.debug (fn () => name ^ ": " ^ Display.string_of_thm th);
-
(* get lemmas from claset, simpset, atpset and extra supplied rules *)
fun get_clasimp_atp_lemmas ctxt =
let val included_thms =
@@ -418,7 +415,6 @@
let val atpset_thms =
if include_atpset then ResAxioms.atpset_rules_of ctxt
else []
- val _ = (Output.debug (fn () => "ATP theorems: "); app display_thm atpset_thms)
in atpset_thms end
in
filter check_named included_thms
@@ -550,13 +546,14 @@
and tycons = type_consts_of_terms thy (ccltms@axtms)
(*TFrees in conjecture clauses; TVars in axiom clauses*)
val conjectures = ResHolClause.make_conjecture_clauses dfg thy ccls
+ val (_, extra_clauses) = ListPair.unzip (ResHolClause.make_axiom_clauses dfg thy extra_cls)
val (clnames,axiom_clauses) = ListPair.unzip (ResHolClause.make_axiom_clauses dfg thy axcls)
val helper_clauses = ResHolClause.get_helper_clauses dfg thy isFO (conjectures, extra_cls, [])
val (supers',arity_clauses) = ResClause.make_arity_clauses_dfg dfg thy tycons supers
val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
in
(Vector.fromList clnames,
- (conjectures, axiom_clauses, helper_clauses, classrel_clauses, arity_clauses))
+ (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
end
end;
--- a/src/HOL/Tools/res_clause.ML Thu Jul 02 16:06:12 2009 +0200
+++ b/src/HOL/Tools/res_clause.ML Thu Jul 02 18:32:28 2009 +0200
@@ -381,8 +381,6 @@
| iter_type_class_pairs thy tycons classes =
let val cpairs = type_class_pairs thy tycons classes
val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs))) \\ classes \\ HOLogic.typeS
- val _ = if null newclasses then ()
- else Output.debug (fn _ => "New classes: " ^ space_implode ", " newclasses)
val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
in (classes' union classes, cpairs' union cpairs) end;
--- a/src/HOL/Tools/res_hol_clause.ML Thu Jul 02 16:06:12 2009 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML Thu Jul 02 18:32:28 2009 +0200
@@ -36,10 +36,12 @@
clause list * (thm * (axiom_name * clause_id)) list * string list ->
clause list
val tptp_write_file: bool -> Path.T ->
- clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list ->
+ clause list * clause list * clause list * clause list *
+ ResClause.classrelClause list * ResClause.arityClause list ->
int * int
val dfg_write_file: bool -> Path.T ->
- clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list ->
+ clause list * clause list * clause list * clause list *
+ ResClause.classrelClause list * ResClause.arityClause list ->
int * int
end
@@ -417,13 +419,13 @@
val ct = List.foldl (count_user_clause user_lemmas) ct0 axclauses
fun needed c = valOf (Symtab.lookup ct c) > 0
val IK = if needed "c_COMBI" orelse needed "c_COMBK"
- then (Output.debug (fn () => "Include combinator I K"); cnf_helper_thms thy [comb_I,comb_K])
+ then cnf_helper_thms thy [comb_I,comb_K]
else []
val BC = if needed "c_COMBB" orelse needed "c_COMBC"
- then (Output.debug (fn () => "Include combinator B C"); cnf_helper_thms thy [comb_B,comb_C])
+ then cnf_helper_thms thy [comb_B,comb_C]
else []
val S = if needed "c_COMBS"
- then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms thy [comb_S])
+ then cnf_helper_thms thy [comb_S]
else []
val other = cnf_helper_thms thy [fequal_imp_equal,equal_imp_fequal]
in
@@ -459,11 +461,11 @@
Output.debug (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^
(if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else ""));
-fun count_constants (conjectures, axclauses, helper_clauses, _, _) =
+fun count_constants (conjectures, _, extra_clauses, helper_clauses, _, _) =
if minimize_applies then
let val (const_min_arity, const_needs_hBOOL) =
fold count_constants_clause conjectures (Symtab.empty, Symtab.empty)
- |> fold count_constants_clause axclauses
+ |> fold count_constants_clause extra_clauses
|> fold count_constants_clause helper_clauses
val _ = List.app (display_arity const_needs_hBOOL) (Symtab.dest (const_min_arity))
in (const_min_arity, const_needs_hBOOL) end
@@ -473,7 +475,8 @@
fun tptp_write_file t_full file clauses =
let
- val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses
+ val (conjectures, axclauses, _, helper_clauses,
+ classrel_clauses, arity_clauses) = clauses
val (cma, cnh) = count_constants clauses
val params = (t_full, cma, cnh)
val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
@@ -494,7 +497,8 @@
fun dfg_write_file t_full file clauses =
let
- val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses
+ val (conjectures, axclauses, _, helper_clauses,
+ classrel_clauses, arity_clauses) = clauses
val (cma, cnh) = count_constants clauses
val params = (t_full, cma, cnh)
val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures)
--- a/src/HOL/Tools/res_reconstruct.ML Thu Jul 02 16:06:12 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML Thu Jul 02 18:32:28 2009 +0200
@@ -457,9 +457,28 @@
in trace msg; msg end;
-
- (* ==== CHECK IF PROOF OF E OR VAMPIRE WAS SUCCESSFUL === *)
-
+ (*=== EXTRACTING PROOF-TEXT === *)
+
+ val begin_proof_strings = ["# SZS output start CNFRefutation.",
+ "=========== Refutation ==========",
+ "Here is a proof"];
+ val end_proof_strings = ["# SZS output end CNFRefutation",
+ "======= End of refutation =======",
+ "Formulae used in the proof"];
+ fun get_proof_extract proof =
+ let
+ (*splits to_split by the first possible of a list of splitters*)
+ val (begin_string, end_string) =
+ (find_first (fn s => String.isSubstring s proof) begin_proof_strings,
+ find_first (fn s => String.isSubstring s proof) end_proof_strings)
+ in
+ if is_none begin_string orelse is_none end_string
+ then error "Could not extract proof (no substring indicating a proof)"
+ else proof |> first_field (the begin_string) |> the |> snd
+ |> first_field (the end_string) |> the |> fst end;
+
+(* ==== CHECK IF PROOF OF E OR VAMPIRE WAS SUCCESSFUL === *)
+
val failure_strings_E = ["SZS status: Satisfiable","SZS status Satisfiable",
"SZS status: ResourceOut","SZS status ResourceOut","# Cannot determine problem status"];
val failure_strings_vampire = ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"];
@@ -469,31 +488,15 @@
fun find_failure proof =
let val failures =
map_filter (fn s => if String.isSubstring s proof then SOME s else NONE)
- (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS @ failure_strings_remote)
- in if null failures then NONE else SOME (hd failures) end;
-
- (*=== EXTRACTING PROOF-TEXT === *)
-
- val begin_proof_strings = ["# SZS output start CNFRefutation.",
- "=========== Refutation ==========",
- "Here is a proof"];
- val end_proof_strings = ["# SZS output end CNFRefutation",
- "======= End of refutation =======",
- "Formulae used in the proof"];
- fun get_proof_extract proof =
- let
- (*splits to_split by the first possible of a list of splitters*)
- fun first_field_any [] to_split = NONE
- | first_field_any (splitter::splitters) to_split =
- let
- val result = (first_field splitter to_split)
- in
- if isSome result then result else first_field_any splitters to_split
- end
- val (a:string, b:string) = valOf (first_field_any begin_proof_strings proof)
- val (proofextract:string, c:string) = valOf (first_field_any end_proof_strings b)
- in proofextract end;
-
+ (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS @ failure_strings_remote)
+ val correct = null failures andalso
+ exists (fn s => String.isSubstring s proof) begin_proof_strings andalso
+ exists (fn s => String.isSubstring s proof) end_proof_strings
+ in
+ if correct then NONE
+ else if null failures then SOME "Output of ATP not in proper format"
+ else SOME (hd failures) end;
+
(* === EXTRACTING LEMMAS === *)
(* lines have the form "cnf(108, axiom, ...",
the number (108) has to be extracted)*)
--- a/src/HOL/Transcendental.thy Thu Jul 02 16:06:12 2009 +0200
+++ b/src/HOL/Transcendental.thy Thu Jul 02 18:32:28 2009 +0200
@@ -784,9 +784,8 @@
also have "\<dots> = \<bar>f n * real (Suc n) * R' ^ n\<bar> * \<bar>x - y\<bar>" unfolding abs_mult real_mult_assoc[symmetric] by algebra
finally show ?thesis .
qed }
- { fix n
- from DERIV_pow[of "Suc n" x0, THEN DERIV_cmult[where c="f n"]]
- show "DERIV (\<lambda> x. ?f x n) x0 :> (?f' x0 n)" unfolding real_mult_assoc by auto }
+ { fix n show "DERIV (\<lambda> x. ?f x n) x0 :> (?f' x0 n)"
+ by (auto intro!: DERIV_intros simp del: power_Suc) }
{ fix x assume "x \<in> {-R' <..< R'}" hence "R' \<in> {-R <..< R}" and "norm x < norm R'" using assms `R' < R` by auto
have "summable (\<lambda> n. f n * x^n)"
proof (rule summable_le2[THEN conjunct1, OF _ powser_insidea[OF converges[OF `R' \<in> {-R <..< R}`] `norm x < norm R'`]], rule allI)
@@ -1362,6 +1361,12 @@
by (rule DERIV_cos [THEN DERIV_isCont])
+declare
+ DERIV_exp[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+ DERIV_ln[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+ DERIV_sin[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+ DERIV_cos[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+
subsection {* Properties of Sine and Cosine *}
lemma sin_zero [simp]: "sin 0 = 0"
@@ -1410,24 +1415,17 @@
by auto
lemma DERIV_cos_realpow2b: "DERIV (%x. (cos x)\<twosuperior>) x :> -(2 * cos(x) * sin(x))"
-apply (rule lemma_DERIV_subst)
-apply (rule DERIV_cos_realpow2a, auto)
-done
+ by (auto intro!: DERIV_intros)
(* most useful *)
lemma DERIV_cos_cos_mult3 [simp]:
"DERIV (%x. cos(x)*cos(x)) x :> -(2 * cos(x) * sin(x))"
-apply (rule lemma_DERIV_subst)
-apply (rule DERIV_cos_cos_mult2, auto)
-done
+ by (auto intro!: DERIV_intros)
lemma DERIV_sin_circle_all:
"\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :>
(2*cos(x)*sin(x) - 2*cos(x)*sin(x))"
-apply (simp only: diff_minus, safe)
-apply (rule DERIV_add)
-apply (auto simp add: numeral_2_eq_2)
-done
+ by (auto intro!: DERIV_intros)
lemma DERIV_sin_circle_all_zero [simp]:
"\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :> 0"
@@ -1513,22 +1511,12 @@
apply (rule DERIV_cos, auto)
done
-lemmas DERIV_intros = DERIV_ident DERIV_const DERIV_cos DERIV_cmult
- DERIV_sin DERIV_exp DERIV_inverse DERIV_pow
- DERIV_add DERIV_diff DERIV_mult DERIV_minus
- DERIV_inverse_fun DERIV_quotient DERIV_fun_pow
- DERIV_fun_exp DERIV_fun_sin DERIV_fun_cos
-
(* lemma *)
lemma lemma_DERIV_sin_cos_add:
"\<forall>x.
DERIV (%x. (sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +
(cos (x + y) - (cos x * cos y - sin x * sin y)) ^ 2) x :> 0"
-apply (safe, rule lemma_DERIV_subst)
-apply (best intro!: DERIV_intros intro: DERIV_chain2)
- --{*replaces the old @{text DERIV_tac}*}
-apply (auto simp add: algebra_simps)
-done
+ by (auto intro!: DERIV_intros simp add: algebra_simps)
lemma sin_cos_add [simp]:
"(sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +
@@ -1550,10 +1538,8 @@
lemma lemma_DERIV_sin_cos_minus:
"\<forall>x. DERIV (%x. (sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2) x :> 0"
-apply (safe, rule lemma_DERIV_subst)
-apply (best intro!: DERIV_intros intro: DERIV_chain2)
-apply (simp add: algebra_simps)
-done
+ by (auto intro!: DERIV_intros simp add: algebra_simps)
+
lemma sin_cos_minus:
"(sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2 = 0"
@@ -1722,7 +1708,7 @@
apply (assumption, rule_tac y=y in order_less_le_trans, simp_all)
apply (drule_tac y1 = y in order_le_less_trans [THEN sin_gt_zero], assumption, simp_all)
done
-
+
lemma pi_half: "pi/2 = (THE x. 0 \<le> x & x \<le> 2 & cos x = 0)"
by (simp add: pi_def)
@@ -2121,10 +2107,7 @@
lemma lemma_DERIV_tan:
"cos x \<noteq> 0 ==> DERIV (%x. sin(x)/cos(x)) x :> inverse((cos x)\<twosuperior>)"
-apply (rule lemma_DERIV_subst)
-apply (best intro!: DERIV_intros intro: DERIV_chain2)
-apply (auto simp add: divide_inverse numeral_2_eq_2)
-done
+ by (auto intro!: DERIV_intros simp add: field_simps numeral_2_eq_2)
lemma DERIV_tan [simp]: "cos x \<noteq> 0 ==> DERIV tan x :> inverse((cos x)\<twosuperior>)"
by (auto dest: lemma_DERIV_tan simp add: tan_def [symmetric])
@@ -2500,6 +2483,11 @@
apply (simp, simp, simp, rule isCont_arctan)
done
+declare
+ DERIV_arcsin[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+ DERIV_arccos[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+ DERIV_arctan[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+
subsection {* More Theorems about Sin and Cos *}
lemma cos_45: "cos (pi / 4) = sqrt 2 / 2"
@@ -2589,11 +2577,7 @@
by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto)
lemma DERIV_sin_add [simp]: "DERIV (%x. sin (x + k)) xa :> cos (xa + k)"
-apply (rule lemma_DERIV_subst)
-apply (rule_tac f = sin and g = "%x. x + k" in DERIV_chain2)
-apply (best intro!: DERIV_intros intro: DERIV_chain2)+
-apply (simp (no_asm))
-done
+ by (auto intro!: DERIV_intros)
lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
proof -
@@ -2634,11 +2618,7 @@
by (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib add_divide_distrib, auto)
lemma DERIV_cos_add [simp]: "DERIV (%x. cos (x + k)) xa :> - sin (xa + k)"
-apply (rule lemma_DERIV_subst)
-apply (rule_tac f = cos and g = "%x. x + k" in DERIV_chain2)
-apply (best intro!: DERIV_intros intro: DERIV_chain2)+
-apply (simp (no_asm))
-done
+ by (auto intro!: DERIV_intros)
lemma sin_zero_abs_cos_one: "sin x = 0 ==> \<bar>cos x\<bar> = 1"
by (auto simp add: sin_zero_iff even_mult_two_ex)
--- a/src/HOL/ex/Codegenerator_Candidates.thy Thu Jul 02 16:06:12 2009 +0200
+++ b/src/HOL/ex/Codegenerator_Candidates.thy Thu Jul 02 18:32:28 2009 +0200
@@ -8,7 +8,7 @@
Complex_Main
AssocList
Binomial
- Code_Set
+ Fset
Commutative_Ring
Enum
List_Prefix
--- a/src/HOL/ex/Predicate_Compile_ex.thy Thu Jul 02 16:06:12 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Thu Jul 02 18:32:28 2009 +0200
@@ -58,7 +58,7 @@
lemma [code_pred_intros]:
"r a b ==> tranclp r a b"
-"r a b ==> tranclp r b c ==> tranclp r a c"
+"r a b ==> tranclp r b c ==> tranclp r a c"
by auto
(* Setup requires quick and dirty proof *)
@@ -71,7 +71,6 @@
thm tranclp.equation
*)
-
inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
"succ 0 1"
| "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"
--- a/src/HOL/ex/predicate_compile.ML Thu Jul 02 16:06:12 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML Thu Jul 02 18:32:28 2009 +0200
@@ -9,6 +9,8 @@
type mode = int list option list * int list
val add_equations_of: string list -> theory -> theory
val register_predicate : (thm list * thm * int) -> theory -> theory
+ val is_registered : theory -> string -> bool
+ val fetch_pred_data : theory -> string -> (thm list * thm * int)
val predfun_intro_of: theory -> string -> mode -> thm
val predfun_elim_of: theory -> string -> mode -> thm
val strip_intro_concl: int -> term -> term * (term list * term list)
@@ -17,14 +19,18 @@
val modes_of: theory -> string -> mode list
val intros_of: theory -> string -> thm list
val nparams_of: theory -> string -> int
+ val add_intro: thm -> theory -> theory
+ val set_elim: thm -> theory -> theory
val setup: theory -> theory
val code_pred: string -> Proof.context -> Proof.state
val code_pred_cmd: string -> Proof.context -> Proof.state
-(* val print_alternative_rules: theory -> theory (*FIXME diagnostic command?*) *)
+ val print_stored_rules: theory -> unit
val do_proofs: bool ref
+ val mk_casesrule : Proof.context -> int -> thm list -> term
val analyze_compr: theory -> term -> term
val eval_ref: (unit -> term Predicate.pred) option ref
val add_equations : string -> theory -> theory
+ val code_pred_intros_attrib : attribute
end;
structure Predicate_Compile : PREDICATE_COMPILE =
@@ -187,7 +193,7 @@
of NONE => error ("No such predicate " ^ quote name)
| SOME data => data;
-val is_pred = is_some oo lookup_pred_data
+val is_registered = is_some oo lookup_pred_data
val all_preds_of = Graph.keys o PredData.get
@@ -223,25 +229,26 @@
val predfun_elim_of = #elim ooo the_predfun_data
+fun print_stored_rules thy =
+ let
+ val preds = (Graph.keys o PredData.get) thy
+ fun print pred () = let
+ val _ = writeln ("predicate: " ^ pred)
+ val _ = writeln ("number of parameters: " ^ string_of_int (nparams_of thy pred))
+ val _ = writeln ("introrules: ")
+ val _ = fold (fn thm => fn u => writeln (Display.string_of_thm thm))
+ (rev (intros_of thy pred)) ()
+ in
+ if (has_elim thy pred) then
+ writeln ("elimrule: " ^ Display.string_of_thm (the_elim_of thy pred))
+ else
+ writeln ("no elimrule defined")
+ end
+ in
+ fold print preds ()
+ end;
-(* replaces print_alternative_rules *)
-(* TODO:
-fun print_alternative_rules thy = let
- val d = IndCodegenData.get thy
- val preds = (Symtab.keys (#intro_rules d)) union (Symtab.keys (#elim_rules d))
- val _ = tracing ("preds: " ^ (makestring preds))
- fun print pred = let
- val _ = tracing ("predicate: " ^ pred)
- val _ = tracing ("introrules: ")
- val _ = fold (fn thm => fn u => tracing (makestring thm))
- (rev (Symtab.lookup_list (#intro_rules d) pred)) ()
- val _ = tracing ("casesrule: ")
- val _ = tracing (makestring (Symtab.lookup (#elim_rules d) pred))
- in () end
- val _ = map print preds
- in thy end;
-*)
-
+(** preprocessing rules **)
fun imp_prems_conv cv ct =
case Thm.term_of ct of
@@ -298,6 +305,23 @@
val add = apsnd (cons (mode, mk_predfun_data data))
in PredData.map (Graph.map_node name (map_pred_data add)) end
+fun is_inductive_predicate thy name =
+ is_some (try (Inductive.the_inductive (ProofContext.init thy)) name)
+
+fun depending_preds_of thy intros = fold Term.add_consts (map Thm.prop_of intros) [] |> map fst
+ |> filter (fn c => is_inductive_predicate thy c orelse is_registered thy c)
+
+(* code dependency graph *)
+fun dependencies_of thy name =
+ let
+ val (intros, elim, nparams) = fetch_pred_data thy name
+ val data = mk_pred_data ((intros, SOME elim, nparams), [])
+ val keys = depending_preds_of thy intros
+ in
+ (data, keys)
+ end;
+
+(* TODO: add_edges - by analysing dependencies *)
fun add_intro thm thy = let
val (name, _) = dest_Const (fst (strip_intro_concl 0 (prop_of thm)))
fun cons_intro gr =
@@ -320,10 +344,13 @@
fun set (intros, elim, _ ) = (intros, elim, nparams)
in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end
-fun register_predicate (intros, elim, nparams) = let
+fun register_predicate (intros, elim, nparams) thy = let
val (name, _) = dest_Const (fst (strip_intro_concl nparams (prop_of (hd intros))))
fun set _ = (intros, SOME elim, nparams)
- in PredData.map (Graph.new_node (name, mk_pred_data ((intros, SOME elim, nparams), []))) end
+ in
+ PredData.map (Graph.new_node (name, mk_pred_data ((intros, SOME elim, nparams), []))
+ #> fold Graph.add_edge (map (pair name) (depending_preds_of thy intros))) thy
+ end
(* Mode analysis *)
@@ -625,10 +652,11 @@
and compile_param thy modes (NONE, t) = t
| compile_param thy modes (m as SOME (Mode ((iss, is'), is, ms)), t) =
- (case t of
- Abs _ => compile_param_ext thy modes (m, t)
- | _ => let
- val (f, args) = strip_comb t
+ (* (case t of
+ Abs _ => error "compile_param: Invalid term" *) (* compile_param_ext thy modes (m, t) *)
+ (* | _ => let *)
+ let
+ val (f, args) = strip_comb (Envir.eta_contract t)
val (params, args') = chop (length ms) args
val params' = map (compile_param thy modes) (ms ~~ params)
val f' = case f of
@@ -637,7 +665,7 @@
Const (predfun_name_of thy name (iss, is'), funT'_of (iss, is') T)
else error "compile param: Not an inductive predicate with correct mode"
| Free (name, T) => Free (name, funT_of T (SOME is'))
- in list_comb (f', params' @ args') end)
+ in list_comb (f', params' @ args') end
| compile_param _ _ _ = error "compile params"
@@ -1116,7 +1144,7 @@
(* VERY LARGE SIMILIRATIY to function prove_param
-- join both functions
*)
-(*
+
fun prove_param2 thy modes (NONE, t) = all_tac
| prove_param2 thy modes (m as SOME (Mode (mode, is, ms)), t) = let
val (f, args) = strip_comb t
@@ -1132,7 +1160,7 @@
THEN print_tac "after simplification in prove_args"
THEN (EVERY (map (prove_param2 thy modes) (ms ~~ params)))
end
-*)
+
fun prove_expr2 thy modes (SOME (Mode (mode, is, ms)), t) =
(case strip_comb t of
@@ -1140,14 +1168,16 @@
if AList.defined op = modes name then
etac @{thm bindE} 1
THEN (REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"})))
+ THEN new_print_tac "prove_expr2-before"
THEN (debug_tac (Syntax.string_of_term_global thy
(prop_of (predfun_elim_of thy name mode))))
THEN (etac (predfun_elim_of thy name mode) 1)
THEN new_print_tac "prove_expr2"
(* TODO -- FIXME: replace remove_last_goal*)
- THEN (EVERY (replicate (length args) (remove_last_goal thy)))
+ (* THEN (EVERY (replicate (length args) (remove_last_goal thy))) *)
+ THEN (EVERY (map (prove_param thy modes) (ms ~~ args)))
THEN new_print_tac "finished prove_expr2"
- (* THEN (EVERY (map (prove_param thy modes) (ms ~~ args))) *)
+
else error "Prove expr2 if case not implemented"
| _ => etac @{thm bindE} 1)
| prove_expr2 _ _ _ = error "Prove expr2 not implemented"
@@ -1243,7 +1273,7 @@
end;
val prems_tac = prove_prems2 in_ts' param_vs ps
in
- print_tac "starting prove_clause2"
+ new_print_tac "starting prove_clause2"
THEN etac @{thm bindE} 1
THEN (etac @{thm singleE'} 1)
THEN (TRY (etac @{thm Pair_inject} 1))
@@ -1259,6 +1289,7 @@
(DETERM (TRY (rtac @{thm unit.induct} 1)))
THEN (REPEAT_DETERM (CHANGED (rewtac @{thm split_paired_all})))
THEN (rtac (predfun_intro_of thy pred mode) 1)
+ THEN (REPEAT_DETERM (rtac @{thm refl} 2))
THEN (EVERY (map prove_clause (clauses ~~ (1 upto (length clauses)))))
end;
@@ -1321,7 +1352,7 @@
| Negprem _ => error ("Double negation not allowed in premise: " ^ (Syntax.string_of_term_global thy (c $ t)))
| Sidecond t => Sidecond (c $ t))
| (c as Const (s, _), ts) =>
- if is_pred thy s then
+ if is_registered thy s then
let val (ts1, ts2) = chop (nparams_of thy s) ts
in Prem (ts2, list_comb (c, ts1)) end
else Sidecond t
@@ -1373,7 +1404,7 @@
val _ = map (Output.tracing o (Syntax.string_of_term_global thy')) (flat ts)
val pred_mode =
maps (fn (s, (T, _)) => map (pair (s, T)) ((the o AList.lookup (op =) modes) s)) clauses'
- val _ = tracing "Proving equations..."
+ val _ = Output.tracing "Proving equations..."
val result_thms =
prove_preds thy' all_vs param_vs (extra_modes @ modes) clauses (pred_mode ~~ (flat ts))
val thy'' = fold (fn (name, result_thms) => fn thy => snd (PureThy.add_thmss
@@ -1409,21 +1440,6 @@
val cases = map mk_case intros
in Logic.list_implies (assm :: cases, prop) end;
-(* code dependency graph *)
-
-fun dependencies_of thy name =
- let
- fun is_inductive_predicate thy name =
- is_some (try (Inductive.the_inductive (ProofContext.init thy)) name)
- val (intro, elim, nparams) = fetch_pred_data thy name
- val data = mk_pred_data ((intro, SOME elim, nparams), [])
- val intros = map Thm.prop_of (#intros (rep_pred_data data))
- val keys = fold Term.add_consts intros [] |> map fst
- |> filter (is_inductive_predicate thy)
- in
- (data, keys)
- end;
-
fun add_equations name thy =
let
val thy' = PredData.map (Graph.extend (dependencies_of thy) name) thy |> Theory.checkpoint;
@@ -1437,17 +1453,15 @@
scc thy' |> Theory.checkpoint
in thy'' end
+
+fun attrib f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
+
+val code_pred_intros_attrib = attrib add_intro;
+
(** user interface **)
local
-fun attrib f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
-
-(*
-val add_elim_attrib = attrib set_elim;
-*)
-
-
(* TODO: make TheoryDataFun to GenericDataFun & remove duplication of local theory and theory *)
(* TODO: must create state to prove multiple cases *)
fun generic_code_pred prep_const raw_const lthy =
--- a/src/Pure/General/swing.scala Thu Jul 02 16:06:12 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-/* Title: Pure/General/swing.scala
- Author: Makarius
-
-Swing utilities.
-*/
-
-package isabelle
-
-import javax.swing.SwingUtilities
-
-object Swing
-{
- def now[A](body: => A): A = {
- var result: Option[A] = None
- if (SwingUtilities.isEventDispatchThread) { result = Some(body) }
- else SwingUtilities.invokeAndWait(new Runnable { def run = { result = Some(body) } })
- result.get
- }
-
- def later(body: => Unit) {
- if (SwingUtilities.isEventDispatchThread) body
- else SwingUtilities.invokeLater(new Runnable { def run = body })
- }
-}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/swing_thread.scala Thu Jul 02 18:32:28 2009 +0200
@@ -0,0 +1,24 @@
+/* Title: Pure/General/swing_thread.scala
+ Author: Makarius
+
+Evaluation within the AWT/Swing thread.
+*/
+
+package isabelle
+
+import javax.swing.SwingUtilities
+
+object Swing_Thread
+{
+ def now[A](body: => A): A = {
+ var result: Option[A] = None
+ if (SwingUtilities.isEventDispatchThread) { result = Some(body) }
+ else SwingUtilities.invokeAndWait(new Runnable { def run = { result = Some(body) } })
+ result.get
+ }
+
+ def later(body: => Unit) {
+ if (SwingUtilities.isEventDispatchThread) body
+ else SwingUtilities.invokeLater(new Runnable { def run = body })
+ }
+}
--- a/src/Pure/IsaMakefile Thu Jul 02 16:06:12 2009 +0200
+++ b/src/Pure/IsaMakefile Thu Jul 02 18:32:28 2009 +0200
@@ -118,7 +118,7 @@
## Scala material
SCALA_FILES = General/event_bus.scala General/markup.scala \
- General/position.scala General/scan.scala General/swing.scala \
+ General/position.scala General/scan.scala General/swing_thread.scala \
General/symbol.scala General/xml.scala General/yxml.scala \
Isar/isar.scala Isar/isar_document.scala Isar/outer_keyword.scala \
System/cygwin.scala System/gui_setup.scala \
--- a/src/Pure/Isar/class_target.ML Thu Jul 02 16:06:12 2009 +0200
+++ b/src/Pure/Isar/class_target.ML Thu Jul 02 18:32:28 2009 +0200
@@ -32,6 +32,7 @@
(*instances*)
val init_instantiation: string list * (string * sort) list * sort
-> theory -> local_theory
+ val instance_arity_cmd: xstring list * xstring list * xstring -> theory -> Proof.state
val instantiation_instance: (local_theory -> local_theory)
-> local_theory -> Proof.state
val prove_instantiation_instance: (Proof.context -> tactic)
@@ -44,7 +45,8 @@
val instantiation_param: local_theory -> binding -> string option
val confirm_declaration: binding -> local_theory -> local_theory
val pretty_instantiation: local_theory -> Pretty.T
- val instance_arity_cmd: xstring * xstring list * xstring -> theory -> Proof.state
+ val read_multi_arity: theory -> xstring list * xstring list * xstring
+ -> string list * (string * sort) list * sort
val type_name: string -> string
(*subclasses*)
@@ -419,6 +421,15 @@
|> find_first (fn (_, (v, _)) => Binding.name_of b = v)
|> Option.map (fst o fst);
+fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
+ let
+ val all_arities = map (fn raw_tyco => Sign.read_arity thy
+ (raw_tyco, raw_sorts, raw_sort)) raw_tycos;
+ val tycos = map #1 all_arities;
+ val (_, sorts, sort) = hd all_arities;
+ val vs = Name.names Name.context Name.aT sorts;
+ in (tycos, vs, sort) end;
+
(* syntax *)
@@ -578,15 +589,17 @@
(* simplified instantiation interface with no class parameter *)
-fun instance_arity_cmd arities thy =
+fun instance_arity_cmd raw_arities thy =
let
+ val (tycos, vs, sort) = read_multi_arity thy raw_arities;
+ val sorts = map snd vs;
+ val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
fun after_qed results = ProofContext.theory
((fold o fold) AxClass.add_arity results);
in
thy
|> ProofContext.init
- |> Proof.theorem_i NONE after_qed ((map (fn t => [(t, [])])
- o Logic.mk_arities o Sign.read_arity thy) arities)
+ |> Proof.theorem_i NONE after_qed (map (fn t => [(t, [])]) arities)
end;
--- a/src/Pure/Isar/code.ML Thu Jul 02 16:06:12 2009 +0200
+++ b/src/Pure/Isar/code.ML Thu Jul 02 18:32:28 2009 +0200
@@ -75,7 +75,7 @@
val these_eqns: theory -> string -> (thm * bool) list
val all_eqns: theory -> (thm * bool) list
val get_case_scheme: theory -> string -> (int * (int * string list)) option
- val is_undefined: theory -> string -> bool
+ val undefineds: theory -> string list
val print_codesetup: theory -> unit
end;
@@ -898,7 +898,7 @@
fun get_case_scheme thy = Symtab.lookup ((fst o the_cases o the_exec) thy);
-val is_undefined = Symtab.defined o snd o the_cases o the_exec;
+val undefineds = Symtab.keys o snd o the_cases o the_exec;
structure TypeInterpretation = InterpretationFun(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
--- a/src/Pure/Isar/isar_syn.ML Thu Jul 02 16:06:12 2009 +0200
+++ b/src/Pure/Isar/isar_syn.ML Thu Jul 02 18:32:28 2009 +0200
@@ -465,7 +465,7 @@
val _ =
OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> Class.classrel_cmd ||
- P.arity >> Class.instance_arity_cmd)
+ P.multi_arity >> Class.instance_arity_cmd)
>> (Toplevel.print oo Toplevel.theory_to_proof)
|| Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
--- a/src/Pure/Isar/theory_target.ML Thu Jul 02 16:06:12 2009 +0200
+++ b/src/Pure/Isar/theory_target.ML Thu Jul 02 18:32:28 2009 +0200
@@ -330,15 +330,6 @@
else I)}
and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta;
-fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
- let
- val all_arities = map (fn raw_tyco => Sign.read_arity thy
- (raw_tyco, raw_sorts, raw_sort)) raw_tycos;
- val tycos = map #1 all_arities;
- val (_, sorts, sort) = hd all_arities;
- val vs = Name.names Name.context Name.aT sorts;
- in (tycos, vs, sort) end;
-
fun gen_overloading prep_const raw_ops thy =
let
val ctxt = ProofContext.init thy;
@@ -356,7 +347,7 @@
fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []);
fun instantiation_cmd raw_arities thy =
- instantiation (read_multi_arity thy raw_arities) thy;
+ instantiation (Class_Target.read_multi_arity thy raw_arities) thy;
val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);
val overloading_cmd = gen_overloading Syntax.read_term;
--- a/src/Pure/ML-Systems/multithreading_polyml.ML Thu Jul 02 16:06:12 2009 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML Thu Jul 02 18:32:28 2009 +0200
@@ -38,7 +38,7 @@
val available = true;
-val max_threads = ref 1;
+val max_threads = ref 0;
val tested_platform =
let val ml_platform = getenv "ML_PLATFORM"
--- a/src/Pure/System/gui_setup.scala Thu Jul 02 16:06:12 2009 +0200
+++ b/src/Pure/System/gui_setup.scala Thu Jul 02 18:32:28 2009 +0200
@@ -16,7 +16,7 @@
{
def main(args: Array[String]) =
{
- Swing.later {
+ Swing_Thread.later {
UIManager.setLookAndFeel(Platform.look_and_feel)
top.pack()
top.visible = true
@@ -29,8 +29,8 @@
// components
val text = new TextArea {
editable = false
- columns = 40
- rows = 15
+ columns = 80
+ rows = 20
xLayoutAlignment = 0.5
}
val ok = new Button {
@@ -53,6 +53,7 @@
text.append("Main platform: " + name1 + "\n")
text.append("Alternative platform: " + name2 + "\n")
}
+ text.append("Isabelle home: " + java.lang.System.getProperty("isabelle.home"))
// reactions
listenTo(ok)
--- a/src/Pure/System/session.ML Thu Jul 02 16:06:12 2009 +0200
+++ b/src/Pure/System/session.ML Thu Jul 02 18:32:28 2009 +0200
@@ -103,7 +103,10 @@
val start = start_timing ();
val _ = use root;
val stop = end_timing start;
- val _ = Output.std_error ("Timing " ^ item ^ " (" ^ #message stop ^ ")\n");
+ val _ =
+ Output.std_error ("Timing " ^ item ^ " (" ^
+ string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
+ #message stop ^ ")\n");
in () end
else use root;
finish ()))
--- a/src/Tools/Code/code_haskell.ML Thu Jul 02 16:06:12 2009 +0200
+++ b/src/Tools/Code/code_haskell.ML Thu Jul 02 18:32:28 2009 +0200
@@ -23,14 +23,6 @@
(** Haskell serializer **)
-fun pr_haskell_bind pr_term =
- let
- fun pr_bind ((NONE, NONE), _) = str "_"
- | pr_bind ((SOME v, NONE), _) = str v
- | pr_bind ((NONE, SOME p), _) = p
- | pr_bind ((SOME v, SOME p), _) = brackets [str v, str "@", p];
- in gen_pr_bind pr_bind pr_term end;
-
fun pr_haskell_stmt labelled_name syntax_class syntax_tyco syntax_const
init_syms deresolve is_cons contr_classparam_typs deriving_show =
let
@@ -68,13 +60,14 @@
pr_term tyvars thm vars NOBR t1,
pr_term tyvars thm vars BR t2
])
- | pr_term tyvars thm vars fxy (IVar v) =
+ | pr_term tyvars thm vars fxy (IVar NONE) =
+ str "_"
+ | pr_term tyvars thm vars fxy (IVar (SOME v)) =
(str o Code_Printer.lookup_var vars) v
| pr_term tyvars thm vars fxy (t as _ `|=> _) =
let
- val (binds, t') = Code_Thingol.unfold_abs t;
- fun pr ((v, pat), ty) = pr_bind tyvars thm BR ((SOME v, pat), ty);
- val (ps, vars') = fold_map pr binds vars;
+ val (binds, t') = Code_Thingol.unfold_pat_abs t;
+ val (ps, vars') = fold_map (pr_bind tyvars thm BR o fst) binds vars;
in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars thm vars' NOBR t') end
| pr_term tyvars thm vars fxy (ICase (cases as (_, t0))) =
(case Code_Thingol.unfold_const_app t0
@@ -97,13 +90,13 @@
else (str o deresolve) c :: map (pr_term tyvars thm vars BR) ts
end
and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const
- and pr_bind tyvars = pr_haskell_bind (pr_term tyvars)
+ and pr_bind tyvars thm fxy p = gen_pr_bind (pr_term tyvars) thm fxy p
and pr_case tyvars thm vars fxy (cases as ((_, [_]), _)) =
let
val (binds, body) = Code_Thingol.unfold_let (ICase cases);
fun pr ((pat, ty), t) vars =
vars
- |> pr_bind tyvars thm BR ((NONE, SOME pat), ty)
+ |> pr_bind tyvars thm BR pat
|>> (fn p => semicolon [p, str "=", pr_term tyvars thm vars NOBR t])
val (ps, vars') = fold_map pr binds vars;
in brackify_block fxy (str "let {")
@@ -114,7 +107,7 @@
let
fun pr (pat, body) =
let
- val (p, vars') = pr_bind tyvars thm NOBR ((NONE, SOME pat), ty) vars;
+ val (p, vars') = pr_bind tyvars thm NOBR pat vars;
in semicolon [p, str "->", pr_term tyvars thm vars' NOBR body] end;
in brackify_block fxy
(concat [str "case", pr_term tyvars thm vars NOBR t, str "of", str "{"])
@@ -240,8 +233,6 @@
end
| pr_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
let
- val split_abs_pure = (fn (v, _) `|=> t => SOME (v, t) | _ => NONE);
- val unfold_abs_pure = Code_Thingol.unfoldr split_abs_pure;
val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
fun pr_instdef ((classparam, c_inst), (thm, _)) = case syntax_const classparam
of NONE => semicolon [
@@ -255,10 +246,10 @@
val const = if (is_some o syntax_const) c_inst_name
then NONE else (SOME o Long_Name.base_name o deresolve) c_inst_name;
val proto_rhs = Code_Thingol.eta_expand k (c_inst, []);
- val (vs, rhs) = unfold_abs_pure proto_rhs;
+ val (vs, rhs) = (apfst o map) fst (Code_Thingol.unfold_abs proto_rhs);
val vars = init_syms
|> Code_Printer.intro_vars (the_list const)
- |> Code_Printer.intro_vars vs;
+ |> Code_Printer.intro_vars (map_filter I vs);
val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs;
(*dictionaries are not relevant at this late stage*)
in
@@ -447,30 +438,30 @@
fun pretty_haskell_monad c_bind =
let
- fun dest_bind t1 t2 = case Code_Thingol.split_abs t2
- of SOME (((v, pat), ty), t') =>
- SOME ((SOME (((SOME v, pat), ty), true), t1), t')
+ fun dest_bind t1 t2 = case Code_Thingol.split_pat_abs t2
+ of SOME ((pat, ty), t') =>
+ SOME ((SOME ((pat, ty), true), t1), t')
| NONE => NONE;
fun dest_monad c_bind_name (IConst (c, _) `$ t1 `$ t2) =
if c = c_bind_name then dest_bind t1 t2
else NONE
| dest_monad _ t = case Code_Thingol.split_let t
of SOME (((pat, ty), tbind), t') =>
- SOME ((SOME (((NONE, SOME pat), ty), false), tbind), t')
+ SOME ((SOME ((pat, ty), false), tbind), t')
| NONE => NONE;
fun implode_monad c_bind_name = Code_Thingol.unfoldr (dest_monad c_bind_name);
fun pr_monad pr_bind pr (NONE, t) vars =
(semicolon [pr vars NOBR t], vars)
- | pr_monad pr_bind pr (SOME (bind, true), t) vars = vars
+ | pr_monad pr_bind pr (SOME ((bind, _), true), t) vars = vars
|> pr_bind NOBR bind
|>> (fn p => semicolon [p, str "<-", pr vars NOBR t])
- | pr_monad pr_bind pr (SOME (bind, false), t) vars = vars
+ | pr_monad pr_bind pr (SOME ((bind, _), false), t) vars = vars
|> pr_bind NOBR bind
|>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]);
fun pretty _ [c_bind'] pr thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
of SOME (bind, t') => let
val (binds, t'') = implode_monad c_bind' t'
- val (ps, vars') = fold_map (pr_monad (pr_haskell_bind (K pr) thm) pr) (bind :: binds) vars;
+ val (ps, vars') = fold_map (pr_monad (gen_pr_bind (K pr) thm) pr) (bind :: binds) vars;
in (brackify fxy o single o Pretty.enclose "do {" "}" o Pretty.breaks) (ps @| pr vars' NOBR t'') end
| NONE => brackify_infix (1, L) fxy
[pr vars (INFX (1, L)) t1, str ">>=", pr vars (INFX (1, X)) t2]
--- a/src/Tools/Code/code_ml.ML Thu Jul 02 16:06:12 2009 +0200
+++ b/src/Tools/Code/code_ml.ML Thu Jul 02 18:32:28 2009 +0200
@@ -85,7 +85,9 @@
| pr_typ fxy (ITyVar v) = str ("'" ^ v);
fun pr_term is_closure thm vars fxy (IConst c) =
pr_app is_closure thm vars fxy (c, [])
- | pr_term is_closure thm vars fxy (IVar v) =
+ | pr_term is_closure thm vars fxy (IVar NONE) =
+ str "_"
+ | pr_term is_closure thm vars fxy (IVar (SOME v)) =
str (Code_Printer.lookup_var vars v)
| pr_term is_closure thm vars fxy (t as t1 `$ t2) =
(case Code_Thingol.unfold_const_app t
@@ -94,9 +96,9 @@
[pr_term is_closure thm vars NOBR t1, pr_term is_closure thm vars BR t2])
| pr_term is_closure thm vars fxy (t as _ `|=> _) =
let
- val (binds, t') = Code_Thingol.unfold_abs t;
- fun pr ((v, pat), ty) =
- pr_bind is_closure thm NOBR ((SOME v, pat), ty)
+ val (binds, t') = Code_Thingol.unfold_pat_abs t;
+ fun pr (pat, ty) =
+ pr_bind is_closure thm NOBR pat
#>> (fn p => concat [str "fn", p, str "=>"]);
val (ps, vars') = fold_map pr binds vars;
in brackets (ps @ [pr_term is_closure thm vars' NOBR t']) end
@@ -122,17 +124,13 @@
:: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term is_closure thm vars BR) ts
and pr_app is_closure thm vars = gen_pr_app (pr_app' is_closure) (pr_term is_closure)
syntax_const thm vars
- and pr_bind' ((NONE, NONE), _) = str "_"
- | pr_bind' ((SOME v, NONE), _) = str v
- | pr_bind' ((NONE, SOME p), _) = p
- | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p]
- and pr_bind is_closure = gen_pr_bind pr_bind' (pr_term is_closure)
+ and pr_bind is_closure = gen_pr_bind (pr_term is_closure)
and pr_case is_closure thm vars fxy (cases as ((_, [_]), _)) =
let
val (binds, body) = Code_Thingol.unfold_let (ICase cases);
fun pr ((pat, ty), t) vars =
vars
- |> pr_bind is_closure thm NOBR ((NONE, SOME pat), ty)
+ |> pr_bind is_closure thm NOBR pat
|>> (fn p => semicolon [str "val", p, str "=", pr_term is_closure thm vars NOBR t])
val (ps, vars') = fold_map pr binds vars;
in
@@ -146,7 +144,7 @@
let
fun pr delim (pat, body) =
let
- val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars;
+ val (p, vars') = pr_bind is_closure thm NOBR pat vars;
in
concat [str delim, p, str "=>", pr_term is_closure thm vars' NOBR body]
end;
@@ -394,7 +392,9 @@
| pr_typ fxy (ITyVar v) = str ("'" ^ v);
fun pr_term is_closure thm vars fxy (IConst c) =
pr_app is_closure thm vars fxy (c, [])
- | pr_term is_closure thm vars fxy (IVar v) =
+ | pr_term is_closure thm vars fxy (IVar NONE) =
+ str "_"
+ | pr_term is_closure thm vars fxy (IVar (SOME v)) =
str (Code_Printer.lookup_var vars v)
| pr_term is_closure thm vars fxy (t as t1 `$ t2) =
(case Code_Thingol.unfold_const_app t
@@ -403,9 +403,8 @@
brackify fxy [pr_term is_closure thm vars NOBR t1, pr_term is_closure thm vars BR t2])
| pr_term is_closure thm vars fxy (t as _ `|=> _) =
let
- val (binds, t') = Code_Thingol.unfold_abs t;
- fun pr ((v, pat), ty) = pr_bind is_closure thm BR ((SOME v, pat), ty);
- val (ps, vars') = fold_map pr binds vars;
+ val (binds, t') = Code_Thingol.unfold_pat_abs t;
+ val (ps, vars') = fold_map (pr_bind is_closure thm BR o fst) binds vars;
in brackets (str "fun" :: ps @ str "->" @@ pr_term is_closure thm vars' NOBR t') end
| pr_term is_closure thm vars fxy (ICase (cases as (_, t0))) = (case Code_Thingol.unfold_const_app t0
of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
@@ -427,17 +426,13 @@
:: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term is_closure thm vars BR) ts)
and pr_app is_closure = gen_pr_app (pr_app' is_closure) (pr_term is_closure)
syntax_const
- and pr_bind' ((NONE, NONE), _) = str "_"
- | pr_bind' ((SOME v, NONE), _) = str v
- | pr_bind' ((NONE, SOME p), _) = p
- | pr_bind' ((SOME v, SOME p), _) = brackets [p, str "as", str v]
- and pr_bind is_closure = gen_pr_bind pr_bind' (pr_term is_closure)
+ and pr_bind is_closure = gen_pr_bind (pr_term is_closure)
and pr_case is_closure thm vars fxy (cases as ((_, [_]), _)) =
let
val (binds, body) = Code_Thingol.unfold_let (ICase cases);
fun pr ((pat, ty), t) vars =
vars
- |> pr_bind is_closure thm NOBR ((NONE, SOME pat), ty)
+ |> pr_bind is_closure thm NOBR pat
|>> (fn p => concat
[str "let", p, str "=", pr_term is_closure thm vars NOBR t, str "in"])
val (ps, vars') = fold_map pr binds vars;
@@ -449,7 +444,7 @@
let
fun pr delim (pat, body) =
let
- val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars;
+ val (p, vars') = pr_bind is_closure thm NOBR pat vars;
in concat [str delim, p, str "->", pr_term is_closure thm vars' NOBR body] end;
in
brackets (
@@ -464,7 +459,7 @@
fun fish_params vars eqs =
let
fun fish_param _ (w as SOME _) = w
- | fish_param (IVar v) NONE = SOME v
+ | fish_param (IVar (SOME v)) NONE = SOME v
| fish_param _ NONE = NONE;
fun fillup_param _ (_, SOME v) = v
| fillup_param x (i, NONE) = x ^ string_of_int i;
@@ -781,7 +776,7 @@
val eqs = filter (snd o snd) raw_eqs;
val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs
of [(([], t), thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
- then ([(([IVar "x"], t `$ IVar "x"), thm)], false)
+ then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), thm)], false)
else (eqs, not (Code_Thingol.fold_constnames
(fn name' => fn b => b orelse name = name') t false))
| _ => (eqs, false)
--- a/src/Tools/Code/code_printer.ML Thu Jul 02 16:06:12 2009 +0200
+++ b/src/Tools/Code/code_printer.ML Thu Jul 02 18:32:28 2009 +0200
@@ -68,10 +68,9 @@
-> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
-> (string -> const_syntax option)
-> thm -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
- val gen_pr_bind: ((string option * Pretty.T option) * itype -> Pretty.T)
- -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
+ val gen_pr_bind: (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
-> thm -> fixity
- -> (string option * iterm option) * itype -> var_ctxt -> Pretty.T * var_ctxt
+ -> iterm -> var_ctxt -> Pretty.T * var_ctxt
val mk_name_module: Name.context -> string option -> (string -> string option)
-> 'a Graph.T -> string -> string
@@ -216,16 +215,11 @@
else pr_term thm vars fxy (Code_Thingol.eta_expand k app)
end;
-fun gen_pr_bind pr_bind pr_term thm (fxy : fixity) ((v, pat), ty : itype) vars =
+fun gen_pr_bind pr_term thm (fxy : fixity) pat vars =
let
- val vs = case pat
- of SOME pat => Code_Thingol.fold_varnames (insert (op =)) pat []
- | NONE => [];
- val vars' = intro_vars (the_list v) vars;
- val vars'' = intro_vars vs vars';
- val v' = Option.map (lookup_var vars') v;
- val pat' = Option.map (pr_term thm vars'' fxy) pat;
- in (pr_bind ((v', pat'), ty), vars'') end;
+ val vs = Code_Thingol.fold_varnames (insert (op =)) pat [];
+ val vars' = intro_vars vs vars;
+ in (pr_term thm vars' fxy pat, vars') end;
(* mixfix syntax *)
--- a/src/Tools/Code/code_thingol.ML Thu Jul 02 16:06:12 2009 +0200
+++ b/src/Tools/Code/code_thingol.ML Thu Jul 02 18:32:28 2009 +0200
@@ -23,13 +23,13 @@
type const = string * ((itype list * dict list list) * itype list (*types of arguments*))
datatype iterm =
IConst of const
- | IVar of vname
+ | IVar of vname option
| `$ of iterm * iterm
- | `|=> of (vname * itype) * iterm
+ | `|=> of (vname option * itype) * iterm
| ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
(*((term, type), [(selector pattern, body term )]), primitive term)*)
val `$$ : iterm * iterm list -> iterm;
- val `|==> : (vname * itype) list * iterm -> iterm;
+ val `|==> : (vname option * itype) list * iterm -> iterm;
type typscheme = (vname * sort) list * itype;
end;
@@ -40,13 +40,12 @@
val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a
val unfold_fun: itype -> itype list * itype
val unfold_app: iterm -> iterm * iterm list
- val split_abs: iterm -> (((vname * iterm option) * itype) * iterm) option
- val unfold_abs: iterm -> ((vname * iterm option) * itype) list * iterm
+ val unfold_abs: iterm -> (vname option * itype) list * iterm
val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option
val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm
+ val split_pat_abs: iterm -> ((iterm * itype) * iterm) option
+ val unfold_pat_abs: iterm -> (iterm * itype) list * iterm
val unfold_const_app: iterm -> (const * iterm list) option
- val collapse_let: ((vname * itype) * iterm) * iterm
- -> (iterm * itype) * (iterm * iterm) list
val eta_expand: int -> const * iterm list -> iterm
val contains_dictvar: iterm -> bool
val locally_monomorphic: iterm -> bool
@@ -126,9 +125,9 @@
datatype iterm =
IConst of const
- | IVar of vname
+ | IVar of vname option
| `$ of iterm * iterm
- | `|=> of (vname * itype) * iterm
+ | `|=> of (vname option * itype) * iterm
| ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
(*see also signature*)
@@ -139,14 +138,10 @@
(fn op `$ t => SOME t
| _ => NONE);
-val split_abs =
- (fn (v, ty) `|=> (t as ICase (((IVar w, _), [(p, t')]), _)) =>
- if v = w then SOME (((v, SOME p), ty), t') else SOME (((v, NONE), ty), t)
- | (v, ty) `|=> t => SOME (((v, NONE), ty), t)
+val unfold_abs = unfoldr
+ (fn op `|=> t => SOME t
| _ => NONE);
-val unfold_abs = unfoldr split_abs;
-
val split_let =
(fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t)
| _ => NONE);
@@ -172,39 +167,55 @@
fun fold_varnames f =
let
- fun add (IVar v) = f v
- | add ((v, _) `|=> _) = f v
+ fun add (IVar (SOME v)) = f v
+ | add ((SOME v, _) `|=> _) = f v
| add _ = I;
in fold_aiterms add end;
fun fold_unbound_varnames f =
let
fun add _ (IConst _) = I
- | add vs (IVar v) = if not (member (op =) vs v) then f v else I
+ | add vs (IVar (SOME v)) = if not (member (op =) vs v) then f v else I
+ | add _ (IVar NONE) = I
| add vs (t1 `$ t2) = add vs t1 #> add vs t2
- | add vs ((v, _) `|=> t) = add (insert (op =) v vs) t
- | add vs (ICase (_, t)) = add vs t;
+ | add vs ((SOME v, _) `|=> t) = add (insert (op =) v vs) t
+ | add vs ((NONE, _) `|=> t) = add vs t
+ | add vs (ICase (((t, _), ds), _)) = add vs t #> fold (add_case vs) ds
+ and add_case vs (p, t) = add (fold_varnames (insert (op =)) p vs) t;
in add [] end;
-fun collapse_let (((v, ty), se), be as ICase (((IVar w, _), ds), _)) =
+fun exists_var t v = fold_unbound_varnames (fn w => fn b => v = w orelse b) t false;
+
+fun split_pat_abs ((NONE, ty) `|=> t) = SOME ((IVar NONE, ty), t)
+ | split_pat_abs ((SOME v, ty) `|=> t) = SOME (case t
+ of ICase (((IVar (SOME w), _), [(p, t')]), _) =>
+ if v = w andalso (exists_var p v orelse not (exists_var t' v))
+ then ((p, ty), t')
+ else ((IVar (SOME v), ty), t)
+ | _ => ((IVar (SOME v), ty), t))
+ | split_pat_abs _ = NONE;
+
+val unfold_pat_abs = unfoldr split_pat_abs;
+
+fun unfold_abs_eta [] t = ([], t)
+ | unfold_abs_eta (_ :: tys) (v_ty `|=> t) =
let
- fun exists_v t = fold_unbound_varnames (fn w => fn b =>
- b orelse v = w) t false;
- in if v = w andalso forall (fn (t1, t2) =>
- exists_v t1 orelse not (exists_v t2)) ds
- then ((se, ty), ds)
- else ((se, ty), [(IVar v, be)])
- end
- | collapse_let (((v, ty), se), be) =
- ((se, ty), [(IVar v, be)])
+ val (vs_tys, t') = unfold_abs_eta tys t;
+ in (v_ty :: vs_tys, t') end
+ | unfold_abs_eta tys t =
+ let
+ val ctxt = fold_varnames Name.declare t Name.context;
+ val vs_tys = (map o apfst) SOME (Name.names ctxt "a" tys);
+ in (vs_tys, t `$$ map (IVar o fst) vs_tys) end;
fun eta_expand k (c as (_, (_, tys)), ts) =
let
val j = length ts;
val l = k - j;
val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
- val vs_tys = Name.names ctxt "a" ((curry Library.take l o curry Library.drop j) tys);
- in vs_tys `|==> IConst c `$$ ts @ map (fn (v, _) => IVar v) vs_tys end;
+ val vs_tys = (map o apfst) SOME
+ (Name.names ctxt "a" ((curry Library.take l o curry Library.drop j) tys));
+ in vs_tys `|==> IConst c `$$ ts @ map (IVar o fst) vs_tys end;
fun contains_dictvar t =
let
@@ -574,14 +585,16 @@
and translate_term thy algbr funcgr thm (Const (c, ty)) =
translate_app thy algbr funcgr thm ((c, ty), [])
| translate_term thy algbr funcgr thm (Free (v, _)) =
- pair (IVar v)
+ pair (IVar (SOME v))
| translate_term thy algbr funcgr thm (Abs (abs as (_, ty, _))) =
let
val (v, t) = Syntax.variant_abs abs;
+ val v' = if member (op =) (Term.add_free_names t []) v
+ then SOME v else NONE
in
translate_typ thy algbr funcgr ty
##>> translate_term thy algbr funcgr thm t
- #>> (fn (ty, t) => (v, ty) `|=> t)
+ #>> (fn (ty, t) => (v', ty) `|=> t)
end
| translate_term thy algbr funcgr thm (t as _ $ _) =
case strip_comb t
@@ -618,45 +631,37 @@
#>> (fn (t, ts) => t `$$ ts)
and translate_case thy algbr funcgr thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
let
- val (tys, _) = (chop num_args o fst o strip_type o snd) c_ty;
- val t = nth ts t_pos;
+ fun arg_types num_args ty = (fst o chop num_args o fst o strip_type) ty;
+ val tys = arg_types num_args (snd c_ty);
val ty = nth tys t_pos;
- val ts_clause = nth_drop t_pos ts;
- fun mk_clause (co, num_co_args) t =
+ fun mk_constr c t = let val n = Code.no_args thy c
+ in ((c, arg_types (Code.no_args thy c) (fastype_of t) ---> ty), n) end;
+ val constrs = if null case_pats then []
+ else map2 mk_constr case_pats (nth_drop t_pos ts);
+ fun casify naming constrs ty ts =
let
- val (vs, body) = Term.strip_abs_eta num_co_args t;
- val not_undefined = case body
- of (Const (c, _)) => not (Code.is_undefined thy c)
- | _ => true;
- val pat = list_comb (Const (co, map snd vs ---> ty), map Free vs);
- in (not_undefined, (pat, body)) end;
- val clauses = if null case_pats then let val ([v_ty], body) =
- Term.strip_abs_eta 1 (the_single ts_clause)
- in [(true, (Free v_ty, body))] end
- else map (uncurry mk_clause)
- (AList.make (Code.no_args thy) case_pats ~~ ts_clause);
- fun retermify ty (_, (IVar x, body)) =
- (x, ty) `|=> body
- | retermify _ (_, (pat, body)) =
+ val t = nth ts t_pos;
+ val ts_clause = nth_drop t_pos ts;
+ val undefineds = map_filter (lookup_const naming) (Code.undefineds thy);
+ fun mk_clause ((constr as IConst (_, (_, tys)), n), t) =
let
- val (IConst (_, (_, tys)), ts) = unfold_app pat;
- val vs = map2 (fn IVar x => fn ty => (x, ty)) ts tys;
- in vs `|==> body end;
- fun mk_icase const t ty clauses =
- let
- val (ts1, ts2) = chop t_pos (map (retermify ty) clauses);
- in
- ICase (((t, ty), map_filter (fn (b, d) => if b then SOME d else NONE) clauses),
- const `$$ (ts1 @ t :: ts2))
- end;
+ val (vs, t') = unfold_abs_eta (curry Library.take n tys) t;
+ val is_undefined = case t
+ of IConst (c, _) => member (op =) undefineds c
+ | _ => false;
+ in if is_undefined then NONE else SOME (constr `$$ map (IVar o fst) vs, t') end;
+ val clauses = if null case_pats then let val ([(v, _)], t) =
+ unfold_abs_eta [ty] (the_single ts_clause)
+ in [(IVar v, t)] end
+ else map_filter mk_clause (constrs ~~ ts_clause);
+ in ((t, ty), clauses) end;
in
translate_const thy algbr funcgr thm c_ty
- ##>> translate_term thy algbr funcgr thm t
+ ##>> fold_map (fn (constr, n) => translate_const thy algbr funcgr thm constr #>> rpair n) constrs
##>> translate_typ thy algbr funcgr ty
- ##>> fold_map (fn (b, (pat, body)) => translate_term thy algbr funcgr thm pat
- ##>> translate_term thy algbr funcgr thm body
- #>> pair b) clauses
- #>> (fn (((const, t), ty), ds) => mk_icase const t ty ds)
+ ##>> fold_map (translate_term thy algbr funcgr thm) ts
+ #-> (fn (((t, constrs), ty), ts) =>
+ `(fn (_, (naming, _)) => ICase (casify naming constrs ty ts, t `$$ ts)))
end
and translate_app_case thy algbr funcgr thm (case_scheme as (num_args, _)) ((c, ty), ts) =
if length ts < num_args then
@@ -668,7 +673,7 @@
in
fold_map (translate_typ thy algbr funcgr) tys
##>> translate_case thy algbr funcgr thm case_scheme ((c, ty), ts @ map Free vs)
- #>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|==> t)
+ #>> (fn (tys, t) => map2 (fn (v, _) => pair (SOME v)) vs tys `|==> t)
end
else if length ts > num_args then
translate_case thy algbr funcgr thm case_scheme ((c, ty), Library.take (num_args, ts))
--- a/src/Tools/coherent.ML Thu Jul 02 16:06:12 2009 +0200
+++ b/src/Tools/coherent.ML Thu Jul 02 18:32:28 2009 +0200
@@ -110,9 +110,9 @@
(* Check whether disjunction is valid in given state *)
fun is_valid_disj ctxt facts [] = false
| is_valid_disj ctxt facts ((Ts, ts) :: ds) =
- let val vs = rev (map_index (fn (i, T) => Var (("x", i), T)) Ts)
+ let val vs = map_index (fn (i, T) => Var (("x", i), T)) Ts
in case Seq.pull (valid_conj ctxt facts empty_env
- (map (fn t => subst_bounds (vs, t)) ts)) of
+ (map (fn t => subst_bounds (rev vs, t)) ts)) of
SOME _ => true
| NONE => is_valid_disj ctxt facts ds
end;
@@ -153,10 +153,10 @@
| valid_cases ctxt rules goal dom facts nfacts nparams ((Ts, ts) :: ds) =
let
val _ = message (fn () => "case " ^ commas (map (Syntax.string_of_term ctxt) ts));
- val params = rev (map_index (fn (i, T) =>
- Free ("par" ^ string_of_int (nparams + i), T)) Ts);
+ val params = map_index (fn (i, T) =>
+ Free ("par" ^ string_of_int (nparams + i), T)) Ts;
val ts' = map_index (fn (i, t) =>
- (subst_bounds (params, t), nfacts + i)) ts;
+ (subst_bounds (rev params, t), nfacts + i)) ts;
val dom' = fold (fn (T, p) =>
Typtab.map_default (T, []) (fn ps => ps @ [p]))
(Ts ~~ params) dom;
--- a/src/Tools/nbe.ML Thu Jul 02 16:06:12 2009 +0200
+++ b/src/Tools/nbe.ML Thu Jul 02 18:32:28 2009 +0200
@@ -135,6 +135,8 @@
| nbe_fun i c = "c_" ^ translate_string (fn "." => "_" | c => c) c ^ "_" ^ string_of_int i;
fun nbe_dict v n = "d_" ^ v ^ "_" ^ string_of_int n;
fun nbe_bound v = "v_" ^ v;
+fun nbe_bound_optional NONE = "_"
+ | nbe_bound_optional (SOME v) = nbe_bound v;
fun nbe_default v = "w_" ^ v;
(*note: these three are the "turning spots" where proper argument order is established!*)
@@ -191,9 +193,9 @@
val (t', ts) = Code_Thingol.unfold_app t
in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end
and of_iapp match_cont (IConst (c, ((_, dss), _))) ts = constapp c dss ts
- | of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound v) ts
+ | of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound_optional v) ts
| of_iapp match_cont ((v, _) `|=> t) ts =
- nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound v]) (of_iterm NONE t))) ts
+ nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound_optional v]) (of_iterm NONE t))) ts
| of_iapp match_cont (ICase (((t, _), cs), t0)) ts =
nbe_apps (ml_cases (of_iterm NONE t)
(map (fn (p, t) => (of_iterm NONE p, of_iterm match_cont t)) cs
@@ -212,8 +214,9 @@
else pair (v, [])) vs names;
val samepairs = maps (fn (v, vs) => map (pair v) vs) vs_renames;
fun subst_vars (t as IConst _) samepairs = (t, samepairs)
- | subst_vars (t as IVar v) samepairs = (case AList.lookup (op =) samepairs v
- of SOME v' => (IVar v', AList.delete (op =) v samepairs)
+ | subst_vars (t as IVar NONE) samepairs = (t, samepairs)
+ | subst_vars (t as IVar (SOME v)) samepairs = (case AList.lookup (op =) samepairs v
+ of SOME v' => (IVar (SOME v'), AList.delete (op =) v samepairs)
| NONE => (t, samepairs))
| subst_vars (t1 `$ t2) samepairs = samepairs
|> subst_vars t1
@@ -295,7 +298,8 @@
val params = Name.invent_list [] "d" (length names);
fun mk (k, name) =
(name, ([(v, [])],
- [([IConst (class, (([], []), [])) `$$ map IVar params], IVar (nth params k))]));
+ [([IConst (class, (([], []), [])) `$$ map (IVar o SOME) params],
+ IVar (SOME (nth params k)))]));
in map_index mk names end
| eqns_of_stmt (_, Code_Thingol.Classrel _) =
[]