# HG changeset patch # User haftmann # Date 1246552348 -7200 # Node ID 9fb31e1a119660562d25e80e3883910968ed357a # Parent b8784cb17a3583752a9716db6c579b1df7faae53# Parent 0bf275fbe93ad0fefc3c6994512385345946349b merged diff -r 0bf275fbe93a -r 9fb31e1a1196 Admin/isatest/isatest-makedist --- 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 diff -r 0bf275fbe93a -r 9fb31e1a1196 Admin/isatest/settings/mac-poly64-M4 --- /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" diff -r 0bf275fbe93a -r 9fb31e1a1196 Admin/launch4j/README --- /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 + diff -r 0bf275fbe93a -r 9fb31e1a1196 Admin/launch4j/isabelle.ico Binary file Admin/launch4j/isabelle.ico has changed diff -r 0bf275fbe93a -r 9fb31e1a1196 Admin/launch4j/isabelle.xml --- /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 @@ + + true + gui + lib/classes/isabelle-scala.jar + Isabelle.exe + + + + normal + http://java.com/download + + false + false + + isabelle.ico + + + 1.6.0 + + preferJre + -Disabelle.home="%EXEDIR%" + + \ No newline at end of file diff -r 0bf275fbe93a -r 9fb31e1a1196 NEWS --- 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 *** diff -r 0bf275fbe93a -r 9fb31e1a1196 doc-src/Codegen/Thy/document/Introduction.tex --- 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;\\ diff -r 0bf275fbe93a -r 9fb31e1a1196 doc-src/Codegen/Thy/document/Program.tex --- 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% diff -r 0bf275fbe93a -r 9fb31e1a1196 doc-src/Codegen/Thy/examples/Example.hs --- 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; diff -r 0bf275fbe93a -r 9fb31e1a1196 src/HOL/Decision_Procs/Approximation.thy --- 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 \ real list \ real" -where +fun interpret_floatarith :: "floatarith \ real list \ 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 \ (float * float) option \ (float \ float \ float \ float \ (float * float)) \ (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 \ floatarith \ real list \ bool" where +"isDERIV x (Add a b) vs = (isDERIV x a vs \ isDERIV x b vs)" | +"isDERIV x (Mult a b) vs = (isDERIV x a vs \ isDERIV x b vs)" | +"isDERIV x (Minus a) vs = isDERIV x a vs" | +"isDERIV x (Inverse a) vs = (isDERIV x a vs \ interpret_floatarith a vs \ 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 \ interpret_floatarith a vs > 0)" | +"isDERIV x (Exp a) vs = isDERIV x a vs" | +"isDERIV x (Ln a) vs = (isDERIV x a vs \ 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 \ floatarith \ 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 (\ 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 \ nat \ floatarith \ (float * float) option list \ bool" where +"isDERIV_approx prec x (Add a b) vs = (isDERIV_approx prec x a vs \ isDERIV_approx prec x b vs)" | +"isDERIV_approx prec x (Mult a b) vs = (isDERIV_approx prec x a vs \ 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 \ (case approx prec a vs of Some (l, u) \ 0 < l \ u < 0 | None \ 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 \ (case approx prec a vs of Some (l, u) \ 0 < l | None \ 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 \ (case approx prec a vs of Some (l, u) \ 0 < l | None \ 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 \ u < 0" + by (cases "approx prec a vs", auto) + with approx[OF `bounded_by xs vs` approx_Some] + have "interpret_floatarith a xs \ 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 \ { 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 \ True | Some (l, u) \ ?xs ! j \ { 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 \ { 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 "\x. real l \ x \ x \ real u \ + DERIV (\ x. interpret_floatarith f (xs[n := x])) (xs!n) :> x" + (is "\ x. _ \ _ \ 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 \ ?i ?D (xs!n)" and "?i ?D (xs!n) \ 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 \ (float * float) option \ (float \ float \ float \ float \ (float * float) option) \ (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) + (\ 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 \ { 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) \ (x#xs)!i \ { real l .. real u } | None \ 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 "\ n. (\ m < n. \ z \ {real lx .. real ux}. + DERIV (\ y. interpret_floatarith ((DERIV_floatarith x ^^ m) f) (xs[x := y])) z :> + (interpret_floatarith ((DERIV_floatarith x ^^ (Suc m)) f) (xs[x := z]))) + \ (\ t \ {real lx .. real ux}. (\ i = 0.. j \ {k.. j \ {k.. {real l .. real u})" (is "\ n. ?taylor f k l u n") +using ate proof (induct s arbitrary: k f l u) + case 0 + { fix t assume "t \ {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])) \ {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 \ {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])) \ {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]) \ { real l1 .. real u1 }" + (is "?f 0 (real c) \ _") + by auto + + { fix f :: "'a \ '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: "\ m z. \ m < n ; z \ { real lx .. real ux } \ \ DERIV (?f (Suc m)) z :> ?f (Suc (Suc m)) z" + and hyp: "\ t \ {real lx .. real ux}. (\ i = 0.. j \ {Suc k.. j \ {Suc k.. {real l2 .. real u2}" + (is "\ t \ _. ?X (Suc k) f n t \ _") + by blast + + { fix m z + assume "m < Suc n" and bnd_z: "z \ { 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 "\ k i. k < i \ {k ..< i} = insert k {Suc k ..< i}" by auto + hence setprod_head_Suc: "\ k i. \ {k ..< k + Suc i} = k * \ {Suc k ..< Suc k + i}" by auto + have setsum_move0: "\ k F. setsum F {0.. k. F (Suc k)) {0.. "xs!x - real c" + + { fix t assume t: "t \ {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) \ {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) = + (\ i = 0.. j \ {k.. j \ {k.. {real l .. real u}" . } + thus ?thesis using DERIV by blast + qed +qed + +lemma setprod_fact: "\ {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 "\ { 1 ..< Suc (Suc k) } = (Suc k) * \ { 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 \ {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 \ { real l .. real u }" +proof - + def F \ "\ n z. interpret_floatarith ((DERIV_floatarith x ^^ n) f) (xs[x := z])" + hence F0: "F 0 = (\ 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: "\ m z. m < n \ real lx \ z \ z \ real ux \ DERIV (F m) z :> F (Suc m) z" + and hyp: "\ t. t \ {real lx .. real ux} \ + (\ j = 0.. {real l .. real u}" (is "\ t. _ \ ?taylor t \ _") + unfolding F_def atLeastAtMost_iff[symmetric] setprod_fact by blast + + have bnd_xs: "xs ! x \ { 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 \ real c" "real c \ real ux" "real lx \ xs!x" "xs!x \ 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 \ t < real c else real c < t \ t < xs ! x" + and fl_eq: "interpret_floatarith f (xs[x := xs ! x]) = + (\m = 0.. {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 "\ \ {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) \ cmp l u | None \ 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 \ + 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 \ {real l .. real u}" + shows "\ l' u' ly uy. x \ { real l' .. real u' } \ real l \ real l' \ real u' \ real u \ cmp ly uy \ + 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 \ real ?m" and m_u: "real ?m \ real u" + unfolding le_float_def using Suc.prems by auto + + with `x \ { real l .. real u }` + have "x \ { real l .. real ?m} \ x \ { real ?m .. real u }" by auto + thus ?case + proof (rule disjE) + assume "x \ { real l .. real ?m}" + from Suc.hyps[OF l this] + obtain l' u' ly uy + where "x \ { real l' .. real u' } \ real l \ real l' \ real u' \ real ?m \ cmp ly uy \ + 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 \ { real ?m .. real u }" + from Suc.hyps[OF u this] + obtain l' u' ly uy + where "x \ { real l' .. real u' } \ real ?m \ real l' \ real u' \ real u \ cmp ly uy \ + 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 (\ l u. 0 < l)" + and x: "x \ {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 \ { real l' .. real u' }" and "real l \ real l'" + and "real u' \ 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 \ 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 (\ l u. 0 \ l)" + and x: "x \ {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 \ { real l' .. real u' }" and "real l \ real l'" + and "real u' \ 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 \ interpret_floatarith a [x] - interpret_floatarith b [x]" + by (auto simp add: diff_minus) + from order_trans[OF `0 \ 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) \ x = Atom 0 \ + (case (approx prec a [None], approx prec b [None]) + of (Some (l, u), Some (l', u')) \ + (case f + of Less lf rt \ approx_tse_form' prec t (Add rt (Minus lf)) s l u' (\ l u. 0 < l) + | LessEqual lf rt \ approx_tse_form' prec t (Add rt (Minus lf)) s l u' (\ l u. 0 \ l) + | AtLeastAtMost x lf rt \ + approx_tse_form' prec t (Add x (Minus lf)) s l u' (\ l u. 0 \ l) \ + approx_tse_form' prec t (Add rt (Minus x)) s l u' (\ l u. 0 \ l) + | _ \ False) + | _ \ False) + | _ \ 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 \ { ?f a .. ?f b }" + with approx[OF _ a[symmetric], of "[x]"] approx[OF _ b[symmetric], of "[x]"] + have bnd: "x \ { 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' (\ 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' (\ l u. 0 \ 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' (\ l u. 0 \ l)" + and "approx_tse_form' prec t (Add x (Minus lf)) s l u' (\ l u. 0 \ 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 "\ \ {0..1 :: real} \ \ < \ + 0.7" - by (approximation 10 splitting: "\" = 1) - ML {* fun dest_interpret (@{const "interpret_floatarith"} $ b $ xs) = (b, xs) | dest_interpret t = raise TERM ("dest_interpret", [t]) diff -r 0bf275fbe93a -r 9fb31e1a1196 src/HOL/Decision_Procs/ex/Approximation_Ex.thy --- 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 "\ l\<^isub>1 \ x\<^isub>1 \ x\<^isub>1 \ u\<^isub>1 ; \ ; l\<^isub>n \ x\<^isub>n \ x\<^isub>n \ u\<^isub>n \ \ F"} where @{term F} is the formula, and -@{text "x\<^isub>1, \, x\<^isub>n"} are the variables. The lower bounds @{text "l\<^isub>1, \, l\<^isub>n"} and the upper bounds -@{text "u\<^isub>1, \, 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 \ x \ x \ u\<^isub>1"}, +@{term "x \ { 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) \ { 3 * d .. 3.1 * d }" using assms by (approximation 80) +lemma "\ \ { 0 .. 1 :: real } \ \ ^ 2 \ \" + by (approximation 30 splitting: \=1 taylor: \ = 3) + end diff -r 0bf275fbe93a -r 9fb31e1a1196 src/HOL/Deriv.thy --- 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 "\ n. n \ S \ 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)]: "(\r. m \ r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x)) --> DERIV (%x. \n=m.. (\r=m..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 \ 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) \ 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) \ 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: "\ DERIV f x :> X ; X = Y \ \ 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 *} diff -r 0bf275fbe93a -r 9fb31e1a1196 src/HOL/Finite_Set.thy --- 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 (\ (f x\<^isub>n z)\)"} +@{text "fold f z {x1, ..., xn} = f x1 (\ (f xn z)\)"} 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 \ (0::'a::{field,division_by_zero}) ==> - setprod (inverse \ f) A = inverse (setprod f A)" +lemma setprod_inversef: + fixes f :: "'b \ 'a::{field,division_by_zero}" + shows "finite A ==> setprod (inverse \ f) A = inverse (setprod f A)" by (erule finite_induct) auto lemma setprod_dividef: - "[|finite A; - \x \ A. g x \ (0::'a::{field,division_by_zero})|] + fixes f :: "'b \ '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 \ g) x) A") @@ -2725,16 +2725,16 @@ begin definition - Inf_fin :: "'a set \ 'a" ("\\<^bsub>fin\<^esub>_" [900] 900) + Inf_fin :: "'a set \ 'a" ("\fin_" [900] 900) where "Inf_fin = fold1 inf" definition - Sup_fin :: "'a set \ 'a" ("\\<^bsub>fin\<^esub>_" [900] 900) + Sup_fin :: "'a set \ 'a" ("\fin_" [900] 900) where "Sup_fin = fold1 sup" -lemma Inf_le_Sup [simp]: "\ finite A; A \ {} \ \ \\<^bsub>fin\<^esub>A \ \\<^bsub>fin\<^esub>A" +lemma Inf_le_Sup [simp]: "\ finite A; A \ {} \ \ \finA \ \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 \ a \ A \ sup a (\\<^bsub>fin\<^esub>A) = a" + "finite A \ a \ A \ sup a (\finA) = a" apply(subst sup_commute) apply(simp add: Inf_fin_def sup_absorb2 fold1_belowI) done lemma inf_Sup_absorb [simp]: - "finite A \ a \ A \ inf a (\\<^bsub>fin\<^esub>A) = a" + "finite A \ a \ A \ inf a (\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 \ {}" - shows "sup x (\\<^bsub>fin\<^esub>A) = \\<^bsub>fin\<^esub>{sup x a|a. a \ A}" + shows "sup x (\finA) = \fin{sup x a|a. a \ 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 \ {}" and B: "finite B" "B \ {}" - shows "sup (\\<^bsub>fin\<^esub>A) (\\<^bsub>fin\<^esub>B) = \\<^bsub>fin\<^esub>{sup a b|a b. a \ A \ b \ B}" + shows "sup (\finA) (\finB) = \fin{sup a b|a b. a \ A \ b \ 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 \ A \ b \ B} \ {}" using insert B by blast - have "sup (\\<^bsub>fin\<^esub>(insert x A)) (\\<^bsub>fin\<^esub>B) = sup (inf x (\\<^bsub>fin\<^esub>A)) (\\<^bsub>fin\<^esub>B)" + have "sup (\fin(insert x A)) (\finB) = sup (inf x (\finA)) (\finB)" using insert by (simp add: fold1_insert_idem_def [OF Inf_fin_def]) - also have "\ = inf (sup x (\\<^bsub>fin\<^esub>B)) (sup (\\<^bsub>fin\<^esub>A) (\\<^bsub>fin\<^esub>B))" by(rule sup_inf_distrib2) - also have "\ = inf (\\<^bsub>fin\<^esub>{sup x b|b. b \ B}) (\\<^bsub>fin\<^esub>{sup a b|a b. a \ A \ b \ B})" + also have "\ = inf (sup x (\finB)) (sup (\finA) (\finB))" by(rule sup_inf_distrib2) + also have "\ = inf (\fin{sup x b|b. b \ B}) (\fin{sup a b|a b. a \ A \ b \ B})" using insert by(simp add:sup_Inf1_distrib[OF B]) - also have "\ = \\<^bsub>fin\<^esub>({sup x b |b. b \ B} \ {sup a b |a b. a \ A \ b \ B})" - (is "_ = \\<^bsub>fin\<^esub>?M") + also have "\ = \fin({sup x b |b. b \ B} \ {sup a b |a b. a \ A \ b \ B})" + (is "_ = \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 \ insert x A \ b \ B}" @@ -2808,7 +2808,7 @@ lemma inf_Sup1_distrib: assumes "finite A" and "A \ {}" - shows "inf x (\\<^bsub>fin\<^esub>A) = \\<^bsub>fin\<^esub>{inf x a|a. a \ A}" + shows "inf x (\finA) = \fin{inf x a|a. a \ 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 \ {}" and B: "finite B" "B \ {}" - shows "inf (\\<^bsub>fin\<^esub>A) (\\<^bsub>fin\<^esub>B) = \\<^bsub>fin\<^esub>{inf a b|a b. a \ A \ b \ B}" + shows "inf (\finA) (\finB) = \fin{inf a b|a b. a \ A \ b \ 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 \ A \ b \ B} \ {}" using insert B by blast interpret ab_semigroup_idem_mult sup by (rule ab_semigroup_idem_mult_sup) - have "inf (\\<^bsub>fin\<^esub>(insert x A)) (\\<^bsub>fin\<^esub>B) = inf (sup x (\\<^bsub>fin\<^esub>A)) (\\<^bsub>fin\<^esub>B)" + have "inf (\fin(insert x A)) (\finB) = inf (sup x (\finA)) (\finB)" using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def]) - also have "\ = sup (inf x (\\<^bsub>fin\<^esub>B)) (inf (\\<^bsub>fin\<^esub>A) (\\<^bsub>fin\<^esub>B))" by(rule inf_sup_distrib2) - also have "\ = sup (\\<^bsub>fin\<^esub>{inf x b|b. b \ B}) (\\<^bsub>fin\<^esub>{inf a b|a b. a \ A \ b \ B})" + also have "\ = sup (inf x (\finB)) (inf (\finA) (\finB))" by(rule inf_sup_distrib2) + also have "\ = sup (\fin{inf x b|b. b \ B}) (\fin{inf a b|a b. a \ A \ b \ B})" using insert by(simp add:inf_Sup1_distrib[OF B]) - also have "\ = \\<^bsub>fin\<^esub>({inf x b |b. b \ B} \ {inf a b |a b. a \ A \ b \ B})" - (is "_ = \\<^bsub>fin\<^esub>?M") + also have "\ = \fin({inf x b |b. b \ B} \ {inf a b |a b. a \ A \ b \ B})" + (is "_ = \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 \ insert x A \ b \ B}" @@ -2861,7 +2861,7 @@ lemma Inf_fin_Inf: assumes "finite A" and "A \ {}" - shows "\\<^bsub>fin\<^esub>A = Inf A" + shows "\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 \ {}" - shows "\\<^bsub>fin\<^esub>A = Sup A" + shows "\finA = Sup A" proof - interpret ab_semigroup_idem_mult sup by (rule ab_semigroup_idem_mult_sup) diff -r 0bf275fbe93a -r 9fb31e1a1196 src/HOL/Imperative_HOL/Array.thy --- 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 *) diff -r 0bf275fbe93a -r 9fb31e1a1196 src/HOL/Imperative_HOL/Heap_Monad.thy --- 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 diff -r 0bf275fbe93a -r 9fb31e1a1196 src/HOL/Imperative_HOL/Imperative_HOL_ex.thy --- 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" diff -r 0bf275fbe93a -r 9fb31e1a1196 src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy diff -r 0bf275fbe93a -r 9fb31e1a1196 src/HOL/IsaMakefile --- 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\ diff -r 0bf275fbe93a -r 9fb31e1a1196 src/HOL/Library/Code_Set.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 "\x. g (h x) = x" - shows "foldl f (g s) xs = g (foldl (\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 \ 'a set" where - "member (Fset A) = A" - -lemma Fset_member [simp]: - "Fset (member A) = A" - by (cases A) simp - -definition Set :: "'a list \ '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 \ bool" where - "is_empty A \ List_Set.is_empty (member A)" - -lemma is_empty_Set [code]: - "is_empty (Set xs) \ 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 \ 'a fset \ '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 \ 'a fset \ '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 \ 'b) \ 'a fset \ '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 \ bool) \ 'a fset \ '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 \ bool) \ 'a fset \ bool" where - "forall P A \ Ball (member A) P" - -lemma forall_Set [code]: - "forall P (Set xs) \ list_all P xs" - by (simp add: forall_def Set_def ball_set) - -definition exists :: "('a \ bool) \ 'a fset \ bool" where - "exists P A \ Bex (member A) P" - -lemma exists_Set [code]: - "exists P (Set xs) \ list_ex P xs" - by (simp add: exists_def Set_def bex_set) - - -subsection {* Functorial operations *} - -definition union :: "'a fset \ 'a fset \ 'a fset" where - "union A B = Fset (member A \ member B)" - -lemma union_insert [code]: - "union (Set xs) A = foldl (\A x. insert x A) A xs" -proof - - have "foldl (\A x. Set.insert x A) (member A) xs = - member (foldl (\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 \ 'a fset \ 'a fset" where - "subtract A B = Fset (member B - member A)" - -lemma subtract_remove [code]: - "subtract (Set xs) A = foldl (\A x. remove x A) A xs" -proof - - have "foldl (\A x. List_Set.remove x A) (member A) xs = - member (foldl (\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 \ exists (\x. y = x) A" - by (simp add: exists_def mem_def) - -definition subfset_eq :: "'a fset \ 'a fset \ bool" where - "subfset_eq A B \ member A \ member B" - -lemma subfset_eq_forall [code]: - "subfset_eq A B \ forall (\x. member B x) A" - by (simp add: subfset_eq_def subset_eq forall_def mem_def) - -definition subfset :: "'a fset \ 'a fset \ bool" where - "subfset A B \ member A \ member B" - -lemma subfset_subfset_eq [code]: - "subfset A B \ subfset_eq A B \ \ subfset_eq B A" - by (simp add: subfset_def subfset_eq_def subset) - -lemma eq_fset_subfset_eq [code]: - "eq_class.eq A B \ subfset_eq A B \ subfset_eq B A" - by (cases A, cases B) (simp add: eq subfset_eq_def set_eq) - -definition inter :: "'a fset \ 'a fset \ '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 diff -r 0bf275fbe93a -r 9fb31e1a1196 src/HOL/Library/Executable_Set.thy --- 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 \ 'a set \ bool" where "subset = op \" declare subset_def [symmetric, code unfold] -lemma [code]: "subset A B \ (\x\A. x \ B)" - unfolding subset_def subset_eq .. - -definition is_empty :: "'a set \ bool" where - "is_empty A \ A = {}" +lemma [code]: + "subset A B \ (\x\A. x \ B)" + by (simp add: subset_def subset_eq) definition eq_set :: "'a set \ 'a set \ bool" where [code del]: "eq_set = op =" -lemma [code]: "eq_set A B \ A \ B \ B \ A" - unfolding eq_set_def by auto - (* FIXME allow for Stefan's code generator: declare set_eq_subset[code unfold] *) lemma [code]: - "a \ A \ (\x\A. x = a)" - unfolding bex_triv_one_point1 .. - -definition filter_set :: "('a \ bool) \ 'a set \ 'a set" where - "filter_set P xs = {x\xs. P x}" - -declare filter_set_def[symmetric, code unfold] - - -subsection {* Operations on lists *} - -subsubsection {* Basic definitions *} - -definition - flip :: "('a \ 'b \ 'c) \ 'b \ 'a \ 'c" where - "flip f a b = f b a" - -definition - member :: "'a list \ 'a \ bool" where - "member xs x \ x \ set xs" - -definition - insertl :: "'a \ 'a list \ 'a list" where - "insertl x xs = (if member xs x then xs else x#xs)" - -lemma [code target: List]: "member [] y \ False" - and [code target: List]: "member (x#xs) y \ y = x \ member xs y" - unfolding member_def by (induct xs) simp_all - -fun - drop_first :: "('a \ bool) \ 'a list \ '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 \ A \ B \ B \ 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 (\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 (\y. y = x) xs" by (induct xs) simp_all - with True show ?thesis by simp -qed - -lemma member_nil [simp]: - "member [] = (\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 \ 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: "\ (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 \ 'a list \ '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 \ 'a list \ '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 \ 'a list \ '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 \ 'b) \ 'a list \ '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 \ '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 \ 'a list" -primrec - "intersects (x#xs) = foldr intersect xs x" - -definition - map_union :: "'a list \ ('a \ 'b list) \ 'b list" where - "map_union xs f = unions (map f xs)" - -definition - map_inter :: "'a list \ ('a \ 'b list) \ 'b list" where - "map_inter xs f = intersects (map f xs)" - - -subsection {* Isomorphism proofs *} - -lemma iso_member: - "member xs x \ x \ 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 \ set ys" - unfolding unionl_eq - by (induct xs arbitrary: ys) (simp_all add: iso_insert) - -lemma iso_intersect: - "set (intersect xs ys) = set xs \ set ys" - unfolding intersect_eq Int_def by (simp add: Int_def iso_member) auto - -definition - subtract' :: "'a list \ 'a list \ '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) = \ 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)) = \ 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 \ ('a \ bool) \ bool" where - "Blall = flip list_all" -definition - Blex :: "'a list \ ('a \ bool) \ 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 \ 'b \ 'c) \ 'b \ 'a \ 'c" where + "flip f a b = f b a" + +types_code + fset ("(_/ \fset)") +attach {* +datatype 'a fset = Set of 'a list; +*} + +consts_code + Set ("\Set") consts_code - "Set.empty" ("{*[]*}") - insert ("{*insertl*}") - is_empty ("{*null*}") - "op \" ("{*unionl*}") - "op \" ("{*intersect*}") - "op - \ 'a set \ 'a set \ '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 \" ("{*Fset.union*}") + "op \" ("{*Fset.inter*}") + "op - \ 'a set \ 'a set \ '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 diff -r 0bf275fbe93a -r 9fb31e1a1196 src/HOL/Library/Float.thy --- 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 diff -r 0bf275fbe93a -r 9fb31e1a1196 src/HOL/Library/Fset.thy --- /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 "\x. g (h x) = x" + shows "foldl f (g s) xs = g (foldl (\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 \ 'a set" where + "member (Fset A) = A" + +lemma Fset_member [simp]: + "Fset (member A) = A" + by (cases A) simp + +definition Set :: "'a list \ '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 \ bool" where + [simp]: "is_empty A \ List_Set.is_empty (member A)" + +lemma is_empty_Set [code]: + "is_empty (Set xs) \ 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 \ 'a fset \ '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 \ 'a fset \ '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 \ 'b) \ 'a fset \ '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 \ bool) \ 'a fset \ '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 \ bool) \ 'a fset \ bool" where + [simp]: "forall P A \ Ball (member A) P" + +lemma forall_Set [code]: + "forall P (Set xs) \ list_all P xs" + by (simp add: Set_def ball_set) + +definition exists :: "('a \ bool) \ 'a fset \ bool" where + [simp]: "exists P A \ Bex (member A) P" + +lemma exists_Set [code]: + "exists P (Set xs) \ list_ex P xs" + by (simp add: Set_def bex_set) + +definition card :: "'a fset \ 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 \ exists (\x. y = x) A" + by simp + +definition subfset_eq :: "'a fset \ 'a fset \ bool" where + [simp]: "subfset_eq A B \ member A \ member B" + +lemma subfset_eq_forall [code]: + "subfset_eq A B \ forall (\x. member B x) A" + by (simp add: subset_eq) + +definition subfset :: "'a fset \ 'a fset \ bool" where + [simp]: "subfset A B \ member A \ member B" + +lemma subfset_subfset_eq [code]: + "subfset A B \ subfset_eq A B \ \ subfset_eq B A" + by (simp add: subset) + +lemma eq_fset_subfset_eq [code]: + "eq_class.eq A B \ subfset_eq A B \ subfset_eq B A" + by (cases A, cases B) (simp add: eq set_eq) + +definition inter :: "'a fset \ 'a fset \ '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 \ 'a fset \ 'a fset" where + [simp]: "union A B = Fset (member A \ member B)" + +lemma union_insert [code]: + "union (Set xs) A = foldl (\A x. insert x A) A xs" +proof - + have "foldl (\A x. Set.insert x A) (member A) xs = + member (foldl (\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 \ 'a fset \ 'a fset" where + [simp]: "subtract A B = Fset (member B - member A)" + +lemma subtract_remove [code]: + "subtract (Set xs) A = foldl (\A x. remove x A) A xs" +proof - + have "foldl (\A x. List_Set.remove x A) (member A) xs = + member (foldl (\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 \ '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 \) (member A) (List.map member As) = + member (foldl (\B A. Fset (member B \ 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 \ '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 \) (member empty) (List.map member As) = + member (foldl (\B A. Fset (member B \ 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 \ 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 \ 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 \ 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 diff -r 0bf275fbe93a -r 9fb31e1a1196 src/HOL/Library/Library.thy --- 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 diff -r 0bf275fbe93a -r 9fb31e1a1196 src/HOL/Library/List_Set.thy --- 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 \ B = project (\x. x \ A) B" by (auto simp add: project_def) + +hide (open) const insert + end \ No newline at end of file diff -r 0bf275fbe93a -r 9fb31e1a1196 src/HOL/Library/Poly_Deriv.thy --- 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*} diff -r 0bf275fbe93a -r 9fb31e1a1196 src/HOL/Ln.thy --- 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 - diff -r 0bf275fbe93a -r 9fb31e1a1196 src/HOL/MacLaurin.thy --- 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: "\m t. m < n \ 0\t \ t\h \ 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: "\t\ \ \x\" and diff -r 0bf275fbe93a -r 9fb31e1a1196 src/HOL/MicroJava/BV/BVExample.thy --- 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 (\(ss, w). \ (is_empty w)) + "iter f step ss w = while (\(ss, w). \ is_empty w) (\(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 diff -r 0bf275fbe93a -r 9fb31e1a1196 src/HOL/NthRoot.thy --- 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 "\y. x - 1 < y \ y < 0 \ - (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 (\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) \ 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 \ 0" + and even: "\ even n ; 0 < x \ \ D = inverse (real n * root n x ^ (n - Suc 0))" + and even: "\ even n ; x < 0 \ \ D = - inverse (real n * root n x ^ (n - Suc 0))" + and odd: "odd n \ 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 \ 0" + assumes "x > 0 \ D = inverse (sqrt x) / 2" + assumes "x < 0 \ 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 \ 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 diff -r 0bf275fbe93a -r 9fb31e1a1196 src/HOL/Tools/Datatype/datatype.ML --- 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 diff -r 0bf275fbe93a -r 9fb31e1a1196 src/HOL/Tools/dseq.ML --- 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. diff -r 0bf275fbe93a -r 9fb31e1a1196 src/HOL/Tools/inductive_codegen.ML --- 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 diff -r 0bf275fbe93a -r 9fb31e1a1196 src/HOL/Tools/quickcheck_generators.ML --- 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\code_numeral) - 1"}; val j = @{term "j\code_numeral"}; val seed = @{term "s\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 \ 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\code_numeral"}; @@ -329,14 +329,14 @@ else @{term "max :: code_numeral \ code_numeral \ 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; diff -r 0bf275fbe93a -r 9fb31e1a1196 src/HOL/Tools/res_atp.ML --- 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; diff -r 0bf275fbe93a -r 9fb31e1a1196 src/HOL/Tools/res_clause.ML --- 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; diff -r 0bf275fbe93a -r 9fb31e1a1196 src/HOL/Tools/res_hol_clause.ML --- 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) diff -r 0bf275fbe93a -r 9fb31e1a1196 src/HOL/Tools/res_reconstruct.ML --- 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)*) diff -r 0bf275fbe93a -r 9fb31e1a1196 src/HOL/Transcendental.thy --- 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 "\ = \f n * real (Suc n) * R' ^ n\ * \x - y\" 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 (\ x. ?f x n) x0 :> (?f' x0 n)" unfolding real_mult_assoc by auto } + { fix n show "DERIV (\ x. ?f x n) x0 :> (?f' x0 n)" + by (auto intro!: DERIV_intros simp del: power_Suc) } { fix x assume "x \ {-R' <..< R'}" hence "R' \ {-R <..< R}" and "norm x < norm R'" using assms `R' < R` by auto have "summable (\ n. f n * x^n)" proof (rule summable_le2[THEN conjunct1, OF _ powser_insidea[OF converges[OF `R' \ {-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)\) 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: "\x. DERIV (%x. (sin x)\ + (cos x)\) 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]: "\x. DERIV (%x. (sin x)\ + (cos x)\) 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: "\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: "\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 \ x & x \ 2 & cos x = 0)" by (simp add: pi_def) @@ -2121,10 +2107,7 @@ lemma lemma_DERIV_tan: "cos x \ 0 ==> DERIV (%x. sin(x)/cos(x)) x :> inverse((cos x)\)" -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 \ 0 ==> DERIV tan x :> inverse((cos x)\)" 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 ==> \cos x\ = 1" by (auto simp add: sin_zero_iff even_mult_two_ex) diff -r 0bf275fbe93a -r 9fb31e1a1196 src/HOL/ex/Codegenerator_Candidates.thy --- 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 diff -r 0bf275fbe93a -r 9fb31e1a1196 src/HOL/ex/Predicate_Compile_ex.thy --- 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 \ nat \ bool" where "succ 0 1" | "succ m n \ succ (Suc m) (Suc n)" diff -r 0bf275fbe93a -r 9fb31e1a1196 src/HOL/ex/predicate_compile.ML --- 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 = diff -r 0bf275fbe93a -r 9fb31e1a1196 src/Pure/General/swing.scala --- 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 }) - } -} diff -r 0bf275fbe93a -r 9fb31e1a1196 src/Pure/General/swing_thread.scala --- /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 }) + } +} diff -r 0bf275fbe93a -r 9fb31e1a1196 src/Pure/IsaMakefile --- 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 \ diff -r 0bf275fbe93a -r 9fb31e1a1196 src/Pure/Isar/class_target.ML --- 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; diff -r 0bf275fbe93a -r 9fb31e1a1196 src/Pure/Isar/code.ML --- 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); diff -r 0bf275fbe93a -r 9fb31e1a1196 src/Pure/Isar/isar_syn.ML --- 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.$$$ "\\" || 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))); diff -r 0bf275fbe93a -r 9fb31e1a1196 src/Pure/Isar/theory_target.ML --- 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; diff -r 0bf275fbe93a -r 9fb31e1a1196 src/Pure/ML-Systems/multithreading_polyml.ML --- 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" diff -r 0bf275fbe93a -r 9fb31e1a1196 src/Pure/System/cygwin.scala diff -r 0bf275fbe93a -r 9fb31e1a1196 src/Pure/System/gui_setup.scala --- 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) diff -r 0bf275fbe93a -r 9fb31e1a1196 src/Pure/System/isabelle_system.scala diff -r 0bf275fbe93a -r 9fb31e1a1196 src/Pure/System/platform.scala diff -r 0bf275fbe93a -r 9fb31e1a1196 src/Pure/System/session.ML --- 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 ())) diff -r 0bf275fbe93a -r 9fb31e1a1196 src/Tools/Code/code_haskell.ML --- 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] diff -r 0bf275fbe93a -r 9fb31e1a1196 src/Tools/Code/code_ml.ML --- 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) diff -r 0bf275fbe93a -r 9fb31e1a1196 src/Tools/Code/code_printer.ML --- 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 *) diff -r 0bf275fbe93a -r 9fb31e1a1196 src/Tools/Code/code_thingol.ML --- 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)) diff -r 0bf275fbe93a -r 9fb31e1a1196 src/Tools/coherent.ML --- 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; diff -r 0bf275fbe93a -r 9fb31e1a1196 src/Tools/nbe.ML --- 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 _) = []