# HG changeset patch # User haftmann # Date 1267902991 -3600 # Node ID 7415cd10694200fd3008e445e997636f3823ccd4 # Parent b342390d296f2fe9c07b7ac4bc014be2ab346bfa# Parent b5f6481772f3d4b64f7b613b2c504e06be3063e7 merged diff -r b5f6481772f3 -r 7415cd106942 Admin/PLATFORMS --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/PLATFORMS Sat Mar 06 20:16:31 2010 +0100 @@ -0,0 +1,81 @@ +Some notes on platform support of Isabelle +========================================== + +Preamble +-------- + +The general programming model is that of a stylized ML + Scala + POSIX +environment, with hardly any system specific code in user-space tools +and packages. + +The basic Isabelle system infrastructure provides some facilities to +make this work, e.g. see the ML structures File and Path, or functions +like bash_output. The settings environment also provides some means +for portability, e.g. jvm_path to hold up the impression that even +Java on Windows/Cygwin adheres to Isabelle/POSIX standards. + +When producing add-on tools, it is important to stay within this clean +room of Isabelle, and refrain from overly ambitious system hacking. + + +Supported platforms +------------------- + +The following hardware and operating system platforms are officially +supported by the Isabelle distribution (and bundled tools): + + x86-linux + x86-darwin + x86-cygwin + x86_64-linux + x86_64-darwin + +As of Cygwin 1.7 there is only a 32 bit version of that platform. The +other 64 bit platforms become more and more important for power users +and always need to be taken into account when testing tools. + +All of the above platforms are 100% supported -- end-users should not +have to care about the differences at all. There are also some +secondary platforms where Poly/ML also happens to work: + + ppc-darwin + sparc-solaris + x86-solaris + x86-bsd + +There is no guarantee that Isabelle add-ons work on these fringe +platforms. Even Isabelle/Scala already fails on ppc-darwin due to +lack of JVM 1.6 support on that platform. + + +Dependable system tools +----------------------- + +The following portable system tools can be taken for granted: + + * GNU bash as uniform shell on all platforms. Note that the POSIX + "standard" shell /bin/sh is *not* appropriate, because there are + too many different implementations of it. + + * Perl as largely portable system programming language. In some + situations Python may as an alternative, but it usually performs + not as well in addressing various delicate details of basic + operating system concepts (processes, signals, sockets etc.). + + * Scala with Java Runtime 1.6. The Isabelle/Pure.jar library irons + out many oddities and portability problems of the Java platform. + + +Known problems +-------------- + +* Mac OS: If MacPorts is installed and its version of Perl takes + precedence over /usr/bin/perl in the PATH, then the end-user needs + to take care of installing add-on modules, e.g. HTTP support. Such + add-ons are usually included in Apple's /usr/bin/perl by default. + +* The Java runtime has its own idea about the underlying platform, + e.g. on 64 bit machine Isabelle/ML could be x86-linux, but the JVM + could be x86_64-linux. This affects Java native libraries in + particular -- which are very hard to support in a platform + independent manner, and should be avoided in the first place. diff -r b5f6481772f3 -r 7415cd106942 NEWS --- a/NEWS Sat Mar 06 15:31:31 2010 +0100 +++ b/NEWS Sat Mar 06 20:16:31 2010 +0100 @@ -58,6 +58,9 @@ * Type constructors admit general mixfix syntax, not just infix. +* Use of cumulative prems via "!" in some proof methods has been +discontinued (legacy feature). + *** Pure *** diff -r b5f6481772f3 -r 7415cd106942 doc-src/IsarRef/Thy/Generic.thy --- a/doc-src/IsarRef/Thy/Generic.thy Sat Mar 06 15:31:31 2010 +0100 +++ b/doc-src/IsarRef/Thy/Generic.thy Sat Mar 06 20:16:31 2010 +0100 @@ -364,7 +364,7 @@ \indexouternonterm{simpmod} \begin{rail} - ('simp' | 'simp\_all') ('!' ?) opt? (simpmod *) + ('simp' | 'simp\_all') opt? (simpmod *) ; opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' ) ')' @@ -404,9 +404,7 @@ proofs this is usually quite well behaved in practice: just the local premises of the actual goal are involved, additional facts may be inserted via explicit forward-chaining (via @{command "then"}, - @{command "from"}, @{command "using"} etc.). The full context of - premises is only included if the ``@{text "!"}'' (bang) argument is - given, which should be used with some care, though. + @{command "from"}, @{command "using"} etc.). Additional Simplifier options may be specified to tune the behavior further (mostly for unstructured scripts with many accidental local @@ -603,9 +601,9 @@ \indexouternonterm{clamod} \begin{rail} - 'blast' ('!' ?) nat? (clamod *) + 'blast' nat? (clamod *) ; - ('fast' | 'slow' | 'best' | 'safe' | 'clarify') ('!' ?) (clamod *) + ('fast' | 'slow' | 'best' | 'safe' | 'clarify') (clamod *) ; clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs @@ -629,9 +627,7 @@ Any of the above methods support additional modifiers of the context of classical rules. Their semantics is analogous to the attributes given before. Facts provided by forward chaining are inserted into - the goal before commencing proof search. The ``@{text - "!"}''~argument causes the full context of assumptions to be - included as well. + the goal before commencing proof search. *} @@ -649,9 +645,9 @@ \indexouternonterm{clasimpmod} \begin{rail} - 'auto' '!'? (nat nat)? (clasimpmod *) + 'auto' (nat nat)? (clasimpmod *) ; - ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') '!'? (clasimpmod *) + ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') (clasimpmod *) ; clasimpmod: ('simp' (() | 'add' | 'del' | 'only') | @@ -674,8 +670,7 @@ here. Facts provided by forward chaining are inserted into the goal before - doing the search. The ``@{text "!"}'' argument causes the full - context of assumptions to be included as well. + doing the search. \end{description} *} diff -r b5f6481772f3 -r 7415cd106942 doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Sat Mar 06 15:31:31 2010 +0100 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Sat Mar 06 20:16:31 2010 +0100 @@ -795,16 +795,15 @@ \end{matharray} \begin{rail} - 'iprover' ('!' ?) ( rulemod * ) + 'iprover' ( rulemod * ) ; \end{rail} The @{method (HOL) iprover} method performs intuitionistic proof search, depending on specifically declared rules from the context, or given as explicit arguments. Chained facts are inserted into the - goal before commencing proof search; ``@{method (HOL) iprover}@{text - "!"}'' means to include the current @{fact prems} as well. - + goal before commencing proof search. + Rules need to be classified as @{attribute (Pure) intro}, @{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the ``@{text "!"}'' indicator refers to ``safe'' rules, which may be diff -r b5f6481772f3 -r 7415cd106942 doc-src/IsarRef/Thy/document/Generic.tex --- a/doc-src/IsarRef/Thy/document/Generic.tex Sat Mar 06 15:31:31 2010 +0100 +++ b/doc-src/IsarRef/Thy/document/Generic.tex Sat Mar 06 20:16:31 2010 +0100 @@ -384,7 +384,7 @@ \indexouternonterm{simpmod} \begin{rail} - ('simp' | 'simp\_all') ('!' ?) opt? (simpmod *) + ('simp' | 'simp\_all') opt? (simpmod *) ; opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' ) ')' @@ -424,9 +424,7 @@ proofs this is usually quite well behaved in practice: just the local premises of the actual goal are involved, additional facts may be inserted via explicit forward-chaining (via \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}, - \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}, \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}} etc.). The full context of - premises is only included if the ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' (bang) argument is - given, which should be used with some care, though. + \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}, \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}} etc.). Additional Simplifier options may be specified to tune the behavior further (mostly for unstructured scripts with many accidental local @@ -626,9 +624,9 @@ \indexouternonterm{clamod} \begin{rail} - 'blast' ('!' ?) nat? (clamod *) + 'blast' nat? (clamod *) ; - ('fast' | 'slow' | 'best' | 'safe' | 'clarify') ('!' ?) (clamod *) + ('fast' | 'slow' | 'best' | 'safe' | 'clarify') (clamod *) ; clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs @@ -650,8 +648,7 @@ Any of the above methods support additional modifiers of the context of classical rules. Their semantics is analogous to the attributes given before. Facts provided by forward chaining are inserted into - the goal before commencing proof search. The ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}''~argument causes the full context of assumptions to be - included as well.% + the goal before commencing proof search.% \end{isamarkuptext}% \isamarkuptrue% % @@ -671,9 +668,9 @@ \indexouternonterm{clasimpmod} \begin{rail} - 'auto' '!'? (nat nat)? (clasimpmod *) + 'auto' (nat nat)? (clasimpmod *) ; - ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') '!'? (clasimpmod *) + ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') (clasimpmod *) ; clasimpmod: ('simp' (() | 'add' | 'del' | 'only') | @@ -694,8 +691,7 @@ here. Facts provided by forward chaining are inserted into the goal before - doing the search. The ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' argument causes the full - context of assumptions to be included as well. + doing the search. \end{description}% \end{isamarkuptext}% diff -r b5f6481772f3 -r 7415cd106942 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Sat Mar 06 15:31:31 2010 +0100 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Sat Mar 06 20:16:31 2010 +0100 @@ -805,15 +805,15 @@ \end{matharray} \begin{rail} - 'iprover' ('!' ?) ( rulemod * ) + 'iprover' ( rulemod * ) ; \end{rail} The \hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}} method performs intuitionistic proof search, depending on specifically declared rules from the context, or given as explicit arguments. Chained facts are inserted into the - goal before commencing proof search; ``\hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' means to include the current \hyperlink{fact.prems}{\mbox{\isa{prems}}} as well. - + goal before commencing proof search. + Rules need to be classified as \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}, \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, or \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}; here the ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' indicator refers to ``safe'' rules, which may be diff -r b5f6481772f3 -r 7415cd106942 src/HOL/Matrix/Matrix.thy --- a/src/HOL/Matrix/Matrix.thy Sat Mar 06 15:31:31 2010 +0100 +++ b/src/HOL/Matrix/Matrix.thy Sat Mar 06 20:16:31 2010 +0100 @@ -32,7 +32,7 @@ lemma nrows: assumes hyp: "nrows A \ m" - shows "(Rep_matrix A m n) = 0" (is ?concl) + shows "(Rep_matrix A m n) = 0" proof cases assume "nonzero_positions(Rep_matrix A) = {}" then show "(Rep_matrix A m n) = 0" by (simp add: nonzero_positions_def) @@ -157,13 +157,13 @@ ultimately show "False" using b by (simp) qed -lemma less_ncols: "(n < ncols A) = (? j i. n <= i & (Rep_matrix A j i) \ 0)" (is ?concl) +lemma less_ncols: "(n < ncols A) = (? j i. n <= i & (Rep_matrix A j i) \ 0)" proof - have a: "!! (a::nat) b. (a < b) = (~(b <= a))" by arith - show ?concl by (simp add: a ncols_le) + show ?thesis by (simp add: a ncols_le) qed -lemma le_ncols: "(n <= ncols A) = (\ m. (\ j i. m <= i \ (Rep_matrix A j i) = 0) \ n <= m)" (is ?concl) +lemma le_ncols: "(n <= ncols A) = (\ m. (\ j i. m <= i \ (Rep_matrix A j i) = 0) \ n <= m)" apply (auto) apply (subgoal_tac "ncols A <= m") apply (simp) @@ -179,13 +179,13 @@ finally show "(nrows A <= n) = (! j i. n <= j \ (Rep_matrix A j i) = 0)" by (auto) qed -lemma less_nrows: "(m < nrows A) = (? j i. m <= j & (Rep_matrix A j i) \ 0)" (is ?concl) +lemma less_nrows: "(m < nrows A) = (? j i. m <= j & (Rep_matrix A j i) \ 0)" proof - have a: "!! (a::nat) b. (a < b) = (~(b <= a))" by arith - show ?concl by (simp add: a nrows_le) + show ?thesis by (simp add: a nrows_le) qed -lemma le_nrows: "(n <= nrows A) = (\ m. (\ j i. m <= j \ (Rep_matrix A j i) = 0) \ n <= m)" (is ?concl) +lemma le_nrows: "(n <= nrows A) = (\ m. (\ j i. m <= j \ (Rep_matrix A j i) = 0) \ n <= m)" apply (auto) apply (subgoal_tac "nrows A <= m") apply (simp) @@ -479,7 +479,7 @@ lemma foldseq_significant_positions: assumes p: "! i. i <= N \ S i = T i" - shows "foldseq f S N = foldseq f T N" (is ?concl) + shows "foldseq f S N = foldseq f T N" proof - have "!! m . ! s t. (! i. i<=m \ s i = t i) \ foldseq f s m = foldseq f t m" apply (induct_tac m) @@ -496,10 +496,12 @@ have d:"!! s t. (\i\n. s i = t i) \ foldseq f s n = foldseq f t n" by (simp add: a) show "f (t 0) (foldseq f (\k. s (Suc k)) n) = f (t 0) (foldseq f (\k. t (Suc k)) n)" by (rule c, simp add: d b) qed - with p show ?concl by simp + with p show ?thesis by simp qed -lemma foldseq_tail: "M <= N \ foldseq f S N = foldseq f (% k. (if k < M then (S k) else (foldseq f (% k. S(k+M)) (N-M)))) M" (is "?p \ ?concl") +lemma foldseq_tail: + assumes "M <= N" + shows "foldseq f S N = foldseq f (% k. (if k < M then (S k) else (foldseq f (% k. S(k+M)) (N-M)))) M" proof - have suc: "!! a b. \a <= Suc b; a \ Suc b\ \ a <= b" by arith have a:"!! a b c . a = b \ f c a = f c b" by blast @@ -533,7 +535,7 @@ apply (rule a) by (simp add: subc if_def) qed - then show "?p \ ?concl" by simp + then show ?thesis using assms by simp qed lemma foldseq_zerotail: @@ -556,14 +558,13 @@ assumes "! x. f x 0 = x" and "! i. n < i \ s i = 0" and nm: "n <= m" - shows - "foldseq f s n = foldseq f s m" (is ?concl) + shows "foldseq f s n = foldseq f s m" proof - - have "f 0 0 = 0" by (simp add: prems) + have "f 0 0 = 0" by (simp add: assms) have b:"!! m n. n <= m \ m \ n \ ? k. m-n = Suc k" by arith have c: "0 <= m" by simp have d: "!! k. k \ 0 \ ? l. k = Suc l" by arith - show ?concl + show ?thesis apply (subst foldseq_tail[OF nm]) apply (rule foldseq_significant_positions) apply (auto) @@ -572,10 +573,11 @@ apply (drule b[OF nm]) apply (auto) apply (case_tac "k=0") - apply (simp add: prems) + apply (simp add: assms) apply (drule d) apply (auto) - by (simp add: prems foldseq_zero) + apply (simp add: assms foldseq_zero) + done qed lemma foldseq_zerostart: @@ -623,11 +625,11 @@ lemma foldseq_almostzero: assumes f0x:"! x. f 0 x = x" and fx0: "! x. f x 0 = x" and s0:"! i. i \ j \ s i = 0" - shows "foldseq f s n = (if (j <= n) then (s j) else 0)" (is ?concl) + shows "foldseq f s n = (if (j <= n) then (s j) else 0)" proof - from s0 have a: "! i. i < j \ s i = 0" by simp from s0 have b: "! i. j < i \ s i = 0" by simp - show ?concl + show ?thesis apply auto apply (subst foldseq_zerotail2[of f, OF fx0, of j, OF b, of n, THEN sym]) apply simp @@ -639,7 +641,7 @@ lemma foldseq_distr_unary: assumes "!! a b. g (f a b) = f (g a) (g b)" - shows "g(foldseq f s n) = foldseq f (% x. g(s x)) n" (is ?concl) + shows "g(foldseq f s n) = foldseq f (% x. g(s x)) n" proof - have "! s. g(foldseq f s n) = foldseq f (% x. g(s x)) n" apply (induct_tac n) @@ -647,8 +649,8 @@ apply (simp) apply (auto) apply (drule_tac x="% k. s (Suc k)" in spec) - by (simp add: prems) - then show ?concl by simp + by (simp add: assms) + then show ?thesis by simp qed definition mult_matrix_n :: "nat \ (('a::zero) \ ('b::zero) \ ('c::zero)) \ ('c \ 'c \ 'c) \ 'a matrix \ 'b matrix \ 'c matrix" where @@ -658,21 +660,24 @@ "mult_matrix fmul fadd A B == mult_matrix_n (max (ncols A) (nrows B)) fmul fadd A B" lemma mult_matrix_n: - assumes prems: "ncols A \ n" (is ?An) "nrows B \ n" (is ?Bn) "fadd 0 0 = 0" "fmul 0 0 = 0" - shows c:"mult_matrix fmul fadd A B = mult_matrix_n n fmul fadd A B" (is ?concl) + assumes "ncols A \ n" (is ?An) "nrows B \ n" (is ?Bn) "fadd 0 0 = 0" "fmul 0 0 = 0" + shows c:"mult_matrix fmul fadd A B = mult_matrix_n n fmul fadd A B" proof - - show ?concl using prems + show ?thesis using assms apply (simp add: mult_matrix_def mult_matrix_n_def) apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+) - by (rule foldseq_zerotail, simp_all add: nrows_le ncols_le prems) + apply (rule foldseq_zerotail, simp_all add: nrows_le ncols_le assms) + done qed lemma mult_matrix_nm: - assumes prems: "ncols A <= n" "nrows B <= n" "ncols A <= m" "nrows B <= m" "fadd 0 0 = 0" "fmul 0 0 = 0" + assumes "ncols A <= n" "nrows B <= n" "ncols A <= m" "nrows B <= m" "fadd 0 0 = 0" "fmul 0 0 = 0" shows "mult_matrix_n n fmul fadd A B = mult_matrix_n m fmul fadd A B" proof - - from prems have "mult_matrix_n n fmul fadd A B = mult_matrix fmul fadd A B" by (simp add: mult_matrix_n) - also from prems have "\ = mult_matrix_n m fmul fadd A B" by (simp add: mult_matrix_n[THEN sym]) + from assms have "mult_matrix_n n fmul fadd A B = mult_matrix fmul fadd A B" + by (simp add: mult_matrix_n) + also from assms have "\ = mult_matrix_n m fmul fadd A B" + by (simp add: mult_matrix_n[THEN sym]) finally show "mult_matrix_n n fmul fadd A B = mult_matrix_n m fmul fadd A B" by simp qed @@ -689,23 +694,23 @@ lemma max2: "!! b x y. (b::nat) <= y \ b <= max x y" by (arith) lemma r_distributive_matrix: - assumes prems: + assumes "r_distributive fmul fadd" "associative fadd" "commutative fadd" "fadd 0 0 = 0" "! a. fmul a 0 = 0" "! a. fmul 0 a = 0" - shows "r_distributive (mult_matrix fmul fadd) (combine_matrix fadd)" (is ?concl) + shows "r_distributive (mult_matrix fmul fadd) (combine_matrix fadd)" proof - - from prems show ?concl + from assms show ?thesis apply (simp add: r_distributive_def mult_matrix_def, auto) proof - fix a::"'a matrix" fix u::"'b matrix" fix v::"'b matrix" let ?mx = "max (ncols a) (max (nrows u) (nrows v))" - from prems show "mult_matrix_n (max (ncols a) (nrows (combine_matrix fadd u v))) fmul fadd a (combine_matrix fadd u v) = + from assms show "mult_matrix_n (max (ncols a) (nrows (combine_matrix fadd u v))) fmul fadd a (combine_matrix fadd u v) = combine_matrix fadd (mult_matrix_n (max (ncols a) (nrows u)) fmul fadd a u) (mult_matrix_n (max (ncols a) (nrows v)) fmul fadd a v)" apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul]) apply (simp add: max1 max2 combine_nrows combine_ncols)+ @@ -729,23 +734,23 @@ qed lemma l_distributive_matrix: - assumes prems: + assumes "l_distributive fmul fadd" "associative fadd" "commutative fadd" "fadd 0 0 = 0" "! a. fmul a 0 = 0" "! a. fmul 0 a = 0" - shows "l_distributive (mult_matrix fmul fadd) (combine_matrix fadd)" (is ?concl) + shows "l_distributive (mult_matrix fmul fadd) (combine_matrix fadd)" proof - - from prems show ?concl + from assms show ?thesis apply (simp add: l_distributive_def mult_matrix_def, auto) proof - fix a::"'b matrix" fix u::"'a matrix" fix v::"'a matrix" let ?mx = "max (nrows a) (max (ncols u) (ncols v))" - from prems show "mult_matrix_n (max (ncols (combine_matrix fadd u v)) (nrows a)) fmul fadd (combine_matrix fadd u v) a = + from assms show "mult_matrix_n (max (ncols (combine_matrix fadd u v)) (nrows a)) fmul fadd (combine_matrix fadd u v) a = combine_matrix fadd (mult_matrix_n (max (ncols u) (nrows a)) fmul fadd u a) (mult_matrix_n (max (ncols v) (nrows a)) fmul fadd v a)" apply (subst mult_matrix_nm[of v _ _ ?mx fadd fmul]) apply (simp add: max1 max2 combine_nrows combine_ncols)+ @@ -995,7 +1000,7 @@ by (simp add: nrows) lemma mult_matrix_singleton_right[simp]: - assumes prems: + assumes "! x. fmul x 0 = 0" "! x. fmul 0 x = 0" "! x. fadd 0 x = x" @@ -1004,11 +1009,11 @@ apply (simp add: mult_matrix_def) apply (subst mult_matrix_nm[of _ _ _ "max (ncols A) (Suc j)"]) apply (auto) - apply (simp add: prems)+ + apply (simp add: assms)+ apply (simp add: mult_matrix_n_def apply_matrix_def apply_infmatrix_def) apply (rule comb[of "Abs_matrix" "Abs_matrix"], auto, (rule ext)+) apply (subst foldseq_almostzero[of _ j]) - apply (simp add: prems)+ + apply (simp add: assms)+ apply (auto) apply (metis comm_monoid_add.mult_1 le_antisym le_diff_eq not_neg_nat zero_le_imp_of_nat zle_int) done @@ -1038,7 +1043,7 @@ let ?S = "singleton_matrix I 0 e" let ?comp = "mult_matrix fmul fadd" have d: "!!x f g. f = g \ f x = g x" by blast - have e: "(% x. fmul x e) 0 = 0" by (simp add: prems) + have e: "(% x. fmul x e) 0 = 0" by (simp add: assms) have "~(?comp A ?S = ?comp B ?S)" apply (rule notI) apply (simp add: fprems eprops) @@ -1058,12 +1063,12 @@ assumes "! a b c d. g(f a b) (f c d) = f (g a c) (g b d)" shows - "foldmatrix f g A m n = foldmatrix_transposed g f (transpose_infmatrix A) n m" (is ?concl) + "foldmatrix f g A m n = foldmatrix_transposed g f (transpose_infmatrix A) n m" proof - have forall:"!! P x. (! x. P x) \ P x" by auto have tworows:"! A. foldmatrix f g A 1 n = foldmatrix_transposed g f (transpose_infmatrix A) n 1" apply (induct n) - apply (simp add: foldmatrix_def foldmatrix_transposed_def prems)+ + apply (simp add: foldmatrix_def foldmatrix_transposed_def assms)+ apply (auto) by (drule_tac x="(% j i. A j (Suc i))" in forall, simp) show "foldmatrix f g A m n = foldmatrix_transposed g f (transpose_infmatrix A) n m" @@ -1083,7 +1088,7 @@ shows "foldseq g (% j. foldseq f (A j) n) m = foldseq f (% j. foldseq g ((transpose_infmatrix A) j) m) n" apply (insert foldmatrix_transpose[of g f A m n]) - by (simp add: foldmatrix_def foldmatrix_transposed_def foldseq_assoc[THEN sym] prems) + by (simp add: foldmatrix_def foldmatrix_transposed_def foldseq_assoc[THEN sym] assms) lemma mult_n_nrows: assumes @@ -1095,10 +1100,11 @@ apply (simp add: mult_matrix_n_def) apply (subst RepAbs_matrix) apply (rule_tac x="nrows A" in exI) -apply (simp add: nrows prems foldseq_zero) +apply (simp add: nrows assms foldseq_zero) apply (rule_tac x="ncols B" in exI) -apply (simp add: ncols prems foldseq_zero) -by (simp add: nrows prems foldseq_zero) +apply (simp add: ncols assms foldseq_zero) +apply (simp add: nrows assms foldseq_zero) +done lemma mult_n_ncols: assumes @@ -1110,10 +1116,11 @@ apply (simp add: mult_matrix_n_def) apply (subst RepAbs_matrix) apply (rule_tac x="nrows A" in exI) -apply (simp add: nrows prems foldseq_zero) +apply (simp add: nrows assms foldseq_zero) apply (rule_tac x="ncols B" in exI) -apply (simp add: ncols prems foldseq_zero) -by (simp add: ncols prems foldseq_zero) +apply (simp add: ncols assms foldseq_zero) +apply (simp add: ncols assms foldseq_zero) +done lemma mult_nrows: assumes @@ -1121,7 +1128,7 @@ "! a. fmul a 0 = 0" "fadd 0 0 = 0" shows "nrows (mult_matrix fmul fadd A B) \ nrows A" -by (simp add: mult_matrix_def mult_n_nrows prems) +by (simp add: mult_matrix_def mult_n_nrows assms) lemma mult_ncols: assumes @@ -1129,7 +1136,7 @@ "! a. fmul a 0 = 0" "fadd 0 0 = 0" shows "ncols (mult_matrix fmul fadd A B) \ ncols B" -by (simp add: mult_matrix_def mult_n_ncols prems) +by (simp add: mult_matrix_def mult_n_ncols assms) lemma nrows_move_matrix_le: "nrows (move_matrix A j i) <= nat((int (nrows A)) + j)" apply (auto simp add: nrows_le) @@ -1144,7 +1151,7 @@ done lemma mult_matrix_assoc: - assumes prems: + assumes "! a. fmul1 0 a = 0" "! a. fmul1 a 0 = 0" "! a. fmul2 0 a = 0" @@ -1157,50 +1164,52 @@ "! a b c. fmul2 (fmul1 a b) c = fmul1 a (fmul2 b c)" "! a b c. fmul2 (fadd1 a b) c = fadd1 (fmul2 a c) (fmul2 b c)" "! a b c. fmul1 c (fadd2 a b) = fadd2 (fmul1 c a) (fmul1 c b)" - shows "mult_matrix fmul2 fadd2 (mult_matrix fmul1 fadd1 A B) C = mult_matrix fmul1 fadd1 A (mult_matrix fmul2 fadd2 B C)" (is ?concl) + shows "mult_matrix fmul2 fadd2 (mult_matrix fmul1 fadd1 A B) C = mult_matrix fmul1 fadd1 A (mult_matrix fmul2 fadd2 B C)" proof - have comb_left: "!! A B x y. A = B \ (Rep_matrix (Abs_matrix A)) x y = (Rep_matrix(Abs_matrix B)) x y" by blast have fmul2fadd1fold: "!! x s n. fmul2 (foldseq fadd1 s n) x = foldseq fadd1 (% k. fmul2 (s k) x) n" - by (rule_tac g1 = "% y. fmul2 y x" in ssubst [OF foldseq_distr_unary], simp_all!) + by (rule_tac g1 = "% y. fmul2 y x" in ssubst [OF foldseq_distr_unary], insert assms, simp_all) have fmul1fadd2fold: "!! x s n. fmul1 x (foldseq fadd2 s n) = foldseq fadd2 (% k. fmul1 x (s k)) n" - by (rule_tac g1 = "% y. fmul1 x y" in ssubst [OF foldseq_distr_unary], simp_all!) + using assms by (rule_tac g1 = "% y. fmul1 x y" in ssubst [OF foldseq_distr_unary], simp_all) let ?N = "max (ncols A) (max (ncols B) (max (nrows B) (nrows C)))" - show ?concl + show ?thesis apply (simp add: Rep_matrix_inject[THEN sym]) apply (rule ext)+ apply (simp add: mult_matrix_def) apply (simplesubst mult_matrix_nm[of _ "max (ncols (mult_matrix_n (max (ncols A) (nrows B)) fmul1 fadd1 A B)) (nrows C)" _ "max (ncols B) (nrows C)"]) - apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+ - apply (simplesubst mult_matrix_nm[of _ "max (ncols A) (nrows (mult_matrix_n (max (ncols B) (nrows C)) fmul2 fadd2 B C))" _ "max (ncols A) (nrows B)"]) apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+ + apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+ + apply (simplesubst mult_matrix_nm[of _ "max (ncols A) (nrows (mult_matrix_n (max (ncols B) (nrows C)) fmul2 fadd2 B C))" _ "max (ncols A) (nrows B)"]) + apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+ apply (simplesubst mult_matrix_nm[of _ _ _ "?N"]) - apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+ + apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+ apply (simplesubst mult_matrix_nm[of _ _ _ "?N"]) - apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+ + apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+ apply (simplesubst mult_matrix_nm[of _ _ _ "?N"]) - apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+ + apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+ apply (simplesubst mult_matrix_nm[of _ _ _ "?N"]) - apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+ + apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+ apply (simp add: mult_matrix_n_def) apply (rule comb_left) apply ((rule ext)+, simp) apply (simplesubst RepAbs_matrix) apply (rule exI[of _ "nrows B"]) - apply (simp add: nrows prems foldseq_zero) + apply (simp add: nrows assms foldseq_zero) apply (rule exI[of _ "ncols C"]) - apply (simp add: prems ncols foldseq_zero) + apply (simp add: assms ncols foldseq_zero) apply (subst RepAbs_matrix) apply (rule exI[of _ "nrows A"]) - apply (simp add: nrows prems foldseq_zero) + apply (simp add: nrows assms foldseq_zero) apply (rule exI[of _ "ncols B"]) - apply (simp add: prems ncols foldseq_zero) - apply (simp add: fmul2fadd1fold fmul1fadd2fold prems) + apply (simp add: assms ncols foldseq_zero) + apply (simp add: fmul2fadd1fold fmul1fadd2fold assms) apply (subst foldseq_foldseq) - apply (simp add: prems)+ - by (simp add: transpose_infmatrix) + apply (simp add: assms)+ + apply (simp add: transpose_infmatrix) + done qed lemma - assumes prems: + assumes "! a. fmul1 0 a = 0" "! a. fmul1 a 0 = 0" "! a. fmul2 0 a = 0" @@ -1217,10 +1226,11 @@ "(mult_matrix fmul1 fadd1 A) o (mult_matrix fmul2 fadd2 B) = mult_matrix fmul2 fadd2 (mult_matrix fmul1 fadd1 A B)" apply (rule ext)+ apply (simp add: comp_def ) -by (simp add: mult_matrix_assoc prems) +apply (simp add: mult_matrix_assoc assms) +done lemma mult_matrix_assoc_simple: - assumes prems: + assumes "! a. fmul 0 a = 0" "! a. fmul a 0 = 0" "fadd 0 0 = 0" @@ -1228,14 +1238,16 @@ "commutative fadd" "associative fmul" "distributive fmul fadd" - shows "mult_matrix fmul fadd (mult_matrix fmul fadd A B) C = mult_matrix fmul fadd A (mult_matrix fmul fadd B C)" (is ?concl) + shows "mult_matrix fmul fadd (mult_matrix fmul fadd A B) C = mult_matrix fmul fadd A (mult_matrix fmul fadd B C)" proof - have "!! a b c d. fadd (fadd a b) (fadd c d) = fadd (fadd a c) (fadd b d)" - by (simp! add: associative_def commutative_def) - then show ?concl + using assms by (simp add: associative_def commutative_def) + then show ?thesis apply (subst mult_matrix_assoc) - apply (simp_all!) - by (simp add: associative_def distributive_def l_distributive_def r_distributive_def)+ + using assms + apply simp_all + apply (simp_all add: associative_def distributive_def l_distributive_def r_distributive_def) + done qed lemma transpose_apply_matrix: "f 0 = 0 \ transpose_matrix (apply_matrix f A) = apply_matrix f (transpose_matrix A)" @@ -1258,9 +1270,10 @@ foldseq fadd (% k. fmul (Rep_matrix A j k) (Rep_matrix B k i)) (max (ncols A) (nrows B))" apply (simp add: mult_matrix_def mult_matrix_n_def) apply (subst RepAbs_matrix) -apply (rule exI[of _ "nrows A"], simp! add: nrows foldseq_zero) -apply (rule exI[of _ "ncols B"], simp! add: ncols foldseq_zero) -by simp +apply (rule exI[of _ "nrows A"], insert assms, simp add: nrows foldseq_zero) +apply (rule exI[of _ "ncols B"], insert assms, simp add: ncols foldseq_zero) +apply simp +done lemma transpose_mult_matrix: assumes @@ -1272,7 +1285,9 @@ "transpose_matrix (mult_matrix fmul fadd A B) = mult_matrix fmul fadd (transpose_matrix B) (transpose_matrix A)" apply (simp add: Rep_matrix_inject[THEN sym]) apply (rule ext)+ - by (simp! add: Rep_mult_matrix max_ac) + using assms + apply (simp add: Rep_mult_matrix max_ac) + done lemma column_transpose_matrix: "column_of_matrix (transpose_matrix A) n = transpose_matrix (row_of_matrix A n)" apply (simp add: Rep_matrix_inject[THEN sym]) @@ -1318,7 +1333,7 @@ "(a::('a::{ord, zero}) matrix) <= b" shows "apply_matrix f a <= apply_matrix f b" - by (simp! add: le_matrix_def) + using assms by (simp add: le_matrix_def) lemma le_combine_matrix: assumes @@ -1328,7 +1343,7 @@ "C <= D" shows "combine_matrix f A C <= combine_matrix f B D" -by (simp! add: le_matrix_def) + using assms by (simp add: le_matrix_def) lemma le_left_combine_matrix: assumes @@ -1337,7 +1352,7 @@ "A <= B" shows "combine_matrix f C A <= combine_matrix f C B" - by (simp! add: le_matrix_def) + using assms by (simp add: le_matrix_def) lemma le_right_combine_matrix: assumes @@ -1346,7 +1361,7 @@ "A <= B" shows "combine_matrix f A C <= combine_matrix f B C" - by (simp! add: le_matrix_def) + using assms by (simp add: le_matrix_def) lemma le_transpose_matrix: "(A <= B) = (transpose_matrix A <= transpose_matrix B)" by (simp add: le_matrix_def, auto) @@ -1358,8 +1373,9 @@ shows "foldseq f s n <= foldseq f t n" proof - - have "! s t. (! i. i<=n \ s i <= t i) \ foldseq f s n <= foldseq f t n" by (induct_tac n, simp_all!) - then show "foldseq f s n <= foldseq f t n" by (simp!) + have "! s t. (! i. i<=n \ s i <= t i) \ foldseq f s n <= foldseq f t n" + by (induct n) (simp_all add: assms) + then show "foldseq f s n <= foldseq f t n" using assms by simp qed lemma le_left_mult: @@ -1373,11 +1389,13 @@ "A <= B" shows "mult_matrix fmul fadd C A <= mult_matrix fmul fadd C B" - apply (simp! add: le_matrix_def Rep_mult_matrix) + using assms + apply (simp add: le_matrix_def Rep_mult_matrix) apply (auto) apply (simplesubst foldseq_zerotail[of _ _ _ "max (ncols C) (max (nrows A) (nrows B))"], simp_all add: nrows ncols max1 max2)+ apply (rule le_foldseq) - by (auto) + apply (auto) + done lemma le_right_mult: assumes @@ -1390,11 +1408,13 @@ "A <= B" shows "mult_matrix fmul fadd A C <= mult_matrix fmul fadd B C" - apply (simp! add: le_matrix_def Rep_mult_matrix) + using assms + apply (simp add: le_matrix_def Rep_mult_matrix) apply (auto) apply (simplesubst foldseq_zerotail[of _ _ _ "max (nrows C) (max (ncols A) (ncols B))"], simp_all add: nrows ncols max1 max2)+ apply (rule le_foldseq) - by (auto) + apply (auto) + done lemma spec2: "! j i. P j i \ P j i" by blast lemma neg_imp: "(\ Q \ \ P) \ P \ Q" by blast @@ -1720,15 +1740,16 @@ proof - have "Y = Y * one_matrix (nrows A)" apply (subst one_matrix_mult_right) - apply (insert prems) - by (simp_all add: left_inverse_matrix_def) + using assms + apply (simp_all add: left_inverse_matrix_def) + done also have "\ = Y * (A * X)" - apply (insert prems) + apply (insert assms) apply (frule right_inverse_matrix_dim) by (simp add: right_inverse_matrix_def) also have "\ = (Y * A) * X" by (simp add: mult_assoc) also have "\ = X" - apply (insert prems) + apply (insert assms) apply (frule left_inverse_matrix_dim) apply (simp_all add: left_inverse_matrix_def right_inverse_matrix_def one_matrix_mult_left) done diff -r b5f6481772f3 -r 7415cd106942 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Sat Mar 06 15:31:31 2010 +0100 +++ b/src/HOL/Tools/record.ML Sat Mar 06 20:16:31 2010 +0100 @@ -859,12 +859,12 @@ fun strip_fields T = (case T of - Type (ext, args) => + Type (ext, args as _ :: _) => (case try (unsuffix ext_typeN) ext of SOME ext' => (case get_extfields thy ext' of - SOME fields => - (case get_fieldext thy (fst (hd fields)) of + SOME (fields as (x, _) :: _) => + (case get_fieldext thy x of SOME (_, alphas) => (let val f :: fs = but_last fields; @@ -877,9 +877,9 @@ in fields'' @ strip_fields more end handle Type.TYPE_MATCH => [("", T)] | Library.UnequalLengths => [("", T)]) - | NONE => [("", T)]) - | NONE => [("", T)]) - | NONE => [("", T)]) + | _ => [("", T)]) + | _ => [("", T)]) + | _ => [("", T)]) | _ => [("", T)]); val (fields, (_, moreT)) = split_last (strip_fields T); @@ -896,25 +896,7 @@ fun record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt tm = let val thy = ProofContext.theory_of ctxt; - - (*tm is term representation of a (nested) field type. We first reconstruct the - type from tm so that we can continue on the type level rather then the term level*) - - (* FIXME !??? *) - (*WORKAROUND: - If a record type occurs in an error message of type inference there - may be some internal frees donoted by ??: - (Const "_tfree",_) $ Free ("??'a", _). - - This will unfortunately be translated to Type ("??'a", []) instead of - TFree ("??'a", _) by typ_of_term, which will confuse unify below. - fixT works around.*) - fun fixT (T as Type (x, [])) = - if String.isPrefix "??'" x then TFree (x, Sign.defaultS thy) else T - | fixT (Type (x, xs)) = Type (x, map fixT xs) - | fixT T = T; - - val T = fixT (decode_type thy tm); + val T = decode_type thy tm; val midx = maxidx_of_typ T; val varifyT = varifyT midx; diff -r b5f6481772f3 -r 7415cd106942 src/Provers/blast.ML --- a/src/Provers/blast.ML Sat Mar 06 15:31:31 2010 +0100 +++ b/src/Provers/blast.ML Sat Mar 06 20:16:31 2010 +0100 @@ -57,7 +57,7 @@ safe0_netpair: netpair, safep_netpair: netpair, haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: Context_Rules.netpair} val cla_modifiers: Method.modifier parser list - val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method + val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method end; signature BLAST = @@ -1309,10 +1309,9 @@ val setup = setup_depth_limit #> Method.setup @{binding blast} - (Args.bang_facts -- Scan.lift (Scan.option OuterParse.nat) --| - Method.sections Data.cla_modifiers >> - (fn (prems, NONE) => Data.cla_meth' blast_tac prems - | (prems, SOME lim) => Data.cla_meth' (fn cs => depth_tac cs lim) prems)) + (Scan.lift (Scan.option OuterParse.nat) --| Method.sections Data.cla_modifiers >> + (fn NONE => Data.cla_meth' blast_tac + | SOME lim => Data.cla_meth' (fn cs => depth_tac cs lim))) "classical tableau prover"; end; diff -r b5f6481772f3 -r 7415cd106942 src/Provers/clasimp.ML --- a/src/Provers/clasimp.ML Sat Mar 06 15:31:31 2010 +0100 +++ b/src/Provers/clasimp.ML Sat Mar 06 20:16:31 2010 +0100 @@ -258,21 +258,21 @@ (* methods *) -fun clasimp_meth tac prems ctxt = METHOD (fn facts => - ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (clasimpset_of ctxt)); +fun clasimp_meth tac ctxt = METHOD (fn facts => + ALLGOALS (Method.insert_tac facts) THEN tac (clasimpset_of ctxt)); -fun clasimp_meth' tac prems ctxt = METHOD (fn facts => - HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (clasimpset_of ctxt))); +fun clasimp_meth' tac ctxt = METHOD (fn facts => + HEADGOAL (Method.insert_tac facts THEN' tac (clasimpset_of ctxt))); fun clasimp_method' tac = - Args.bang_facts --| Method.sections clasimp_modifiers >> (clasimp_meth' tac); + Method.sections clasimp_modifiers >> K (clasimp_meth' tac); val auto_method = - Args.bang_facts -- Scan.lift (Scan.option (OuterParse.nat -- OuterParse.nat)) --| - Method.sections clasimp_modifiers >> - (fn (prems, NONE) => clasimp_meth (CHANGED_PROP o auto_tac) prems - | (prems, SOME (m, n)) => clasimp_meth (CHANGED_PROP o (fn css => mk_auto_tac css m n)) prems); + Scan.lift (Scan.option (OuterParse.nat -- OuterParse.nat)) --| + Method.sections clasimp_modifiers >> + (fn NONE => clasimp_meth (CHANGED_PROP o auto_tac) + | SOME (m, n) => clasimp_meth (CHANGED_PROP o (fn css => mk_auto_tac css m n))); (* theory setup *) diff -r b5f6481772f3 -r 7415cd106942 src/Provers/classical.ML --- a/src/Provers/classical.ML Sat Mar 06 15:31:31 2010 +0100 +++ b/src/Provers/classical.ML Sat Mar 06 20:16:31 2010 +0100 @@ -125,8 +125,8 @@ val haz_intro: int option -> attribute val rule_del: attribute val cla_modifiers: Method.modifier parser list - val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method - val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method + val cla_meth: (claset -> tactic) -> Proof.context -> Proof.method + val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method val cla_method: (claset -> tactic) -> (Proof.context -> Proof.method) context_parser val cla_method': (claset -> int -> tactic) -> (Proof.context -> Proof.method) context_parser val setup: theory -> theory @@ -969,14 +969,14 @@ Args.$$$ introN -- Args.colon >> K (I, haz_intro NONE), Args.del -- Args.colon >> K (I, rule_del)]; -fun cla_meth tac prems ctxt = METHOD (fn facts => - ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (claset_of ctxt)); +fun cla_meth tac ctxt = METHOD (fn facts => + ALLGOALS (Method.insert_tac facts) THEN tac (claset_of ctxt)); -fun cla_meth' tac prems ctxt = METHOD (fn facts => - HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (claset_of ctxt))); +fun cla_meth' tac ctxt = METHOD (fn facts => + HEADGOAL (Method.insert_tac facts THEN' tac (claset_of ctxt))); -fun cla_method tac = Args.bang_facts --| Method.sections cla_modifiers >> (cla_meth tac); -fun cla_method' tac = Args.bang_facts --| Method.sections cla_modifiers >> (cla_meth' tac); +fun cla_method tac = Method.sections cla_modifiers >> K (cla_meth tac); +fun cla_method' tac = Method.sections cla_modifiers >> K (cla_meth' tac); diff -r b5f6481772f3 -r 7415cd106942 src/Pure/Isar/args.ML --- a/src/Pure/Isar/args.ML Sat Mar 06 15:31:31 2010 +0100 +++ b/src/Pure/Isar/args.ML Sat Mar 06 20:16:31 2010 +0100 @@ -57,7 +57,6 @@ val type_name: bool -> string context_parser val const: bool -> string context_parser val const_proper: bool -> string context_parser - val bang_facts: thm list context_parser val goal_spec: ((int -> tactic) -> tactic) context_parser val parse: token list parser val parse1: (string -> bool) -> token list parser @@ -224,11 +223,6 @@ (* improper method arguments *) -val bang_facts = Scan.peek (fn context => - P.position ($$$ "!") >> (fn (_, pos) => - (legacy_feature ("use of cumulative prems (!) in proof method" ^ Position.str_of pos); - Assumption.all_prems_of (Context.proof_of context))) || Scan.succeed []); - val from_to = P.nat -- ($$$ "-" |-- P.nat) >> (fn (i, j) => fn tac => Seq.INTERVAL tac i j) || P.nat --| $$$ "-" >> (fn i => fn tac => fn st => Seq.INTERVAL tac i (Thm.nprems_of st) st) || diff -r b5f6481772f3 -r 7415cd106942 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Sat Mar 06 15:31:31 2010 +0100 +++ b/src/Pure/Isar/proof_context.ML Sat Mar 06 20:16:31 2010 +0100 @@ -64,6 +64,7 @@ val expand_abbrevs: Proof.context -> term -> term val cert_term: Proof.context -> term -> term val cert_prop: Proof.context -> term -> term + val def_type: Proof.context -> indexname -> typ option val goal_export: Proof.context -> Proof.context -> thm list -> thm list val export: Proof.context -> Proof.context -> thm list -> thm list val export_morphism: Proof.context -> Proof.context -> morphism @@ -628,13 +629,15 @@ (* type checking/inference *) +fun def_type ctxt = + let val Mode {pattern, ...} = get_mode ctxt + in Variable.def_type ctxt pattern end; + fun standard_infer_types ctxt ts = - let val Mode {pattern, ...} = get_mode ctxt in - TypeInfer.infer_types (Syntax.pp ctxt) (tsig_of ctxt) (Syntax.check_typs ctxt) - (try (Consts.the_constraint (consts_of ctxt))) (Variable.def_type ctxt pattern) - (Variable.names_of ctxt) (Variable.maxidx_of ctxt) ts - handle TYPE (msg, _, _) => error msg - end; + TypeInfer.infer_types (Syntax.pp ctxt) (tsig_of ctxt) (Syntax.check_typs ctxt) + (try (Consts.the_constraint (consts_of ctxt))) (def_type ctxt) + (Variable.names_of ctxt) (Variable.maxidx_of ctxt) ts + handle TYPE (msg, _, _) => error msg; local diff -r b5f6481772f3 -r 7415cd106942 src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Sat Mar 06 15:31:31 2010 +0100 +++ b/src/Pure/simplifier.ML Sat Mar 06 20:16:31 2010 +0100 @@ -15,15 +15,15 @@ val simpset_of: Proof.context -> simpset val generic_simp_tac: bool -> bool * bool * bool -> simpset -> int -> tactic val safe_asm_full_simp_tac: simpset -> int -> tactic - val simp_tac: simpset -> int -> tactic - val asm_simp_tac: simpset -> int -> tactic - val full_simp_tac: simpset -> int -> tactic - val asm_lr_simp_tac: simpset -> int -> tactic - val asm_full_simp_tac: simpset -> int -> tactic - val simplify: simpset -> thm -> thm - val asm_simplify: simpset -> thm -> thm - val full_simplify: simpset -> thm -> thm - val asm_lr_simplify: simpset -> thm -> thm + val simp_tac: simpset -> int -> tactic + val asm_simp_tac: simpset -> int -> tactic + val full_simp_tac: simpset -> int -> tactic + val asm_lr_simp_tac: simpset -> int -> tactic + val asm_full_simp_tac: simpset -> int -> tactic + val simplify: simpset -> thm -> thm + val asm_simplify: simpset -> thm -> thm + val full_simplify: simpset -> thm -> thm + val asm_lr_simplify: simpset -> thm -> thm val asm_full_simplify: simpset -> thm -> thm end; @@ -41,10 +41,10 @@ -> (theory -> simpset -> term -> thm option) -> simproc val simproc: theory -> string -> string list -> (theory -> simpset -> term -> thm option) -> simproc - val rewrite: simpset -> conv - val asm_rewrite: simpset -> conv - val full_rewrite: simpset -> conv - val asm_lr_rewrite: simpset -> conv + val rewrite: simpset -> conv + val asm_rewrite: simpset -> conv + val full_rewrite: simpset -> conv + val asm_lr_rewrite: simpset -> conv val asm_full_rewrite: simpset -> conv val get_ss: Context.generic -> simpset val map_ss: (simpset -> simpset) -> Context.generic -> Context.generic @@ -371,9 +371,9 @@ Scan.succeed asm_full_simp_tac); fun simp_method more_mods meth = - Args.bang_facts -- Scan.lift simp_options --| + Scan.lift simp_options --| Method.sections (more_mods @ simp_modifiers') >> - (fn (prems, tac) => fn ctxt => METHOD (fn facts => meth ctxt tac (prems @ facts))); + (fn tac => fn ctxt => METHOD (fn facts => meth ctxt tac facts)); diff -r b5f6481772f3 -r 7415cd106942 src/Pure/tactic.ML --- a/src/Pure/tactic.ML Sat Mar 06 15:31:31 2010 +0100 +++ b/src/Pure/tactic.ML Sat Mar 06 20:16:31 2010 +0100 @@ -63,8 +63,6 @@ sig include BASIC_TACTIC val innermost_params: int -> thm -> (string * typ) list - val term_lift_inst_rule: - thm * int * ((indexname * sort) * typ) list * ((indexname * typ) * term) list * thm -> thm val insert_tagged_brl: 'a * (bool * thm) -> ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net -> ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net @@ -193,40 +191,6 @@ (*params of subgoal i as they are printed*) fun params_of_state i st = rev (innermost_params i st); -(* -Like lift_inst_rule but takes terms, not strings, where the terms may contain -Bounds referring to parameters of the subgoal. - -insts: [...,(vj,tj),...] - -The tj may contain references to parameters of subgoal i of the state st -in the form of Bound k, i.e. the tj may be subterms of the subgoal. -To saturate the lose bound vars, the tj are enclosed in abstractions -corresponding to the parameters of subgoal i, thus turning them into -functions. At the same time, the types of the vj are lifted. - -NB: the types in insts must be correctly instantiated already, - i.e. Tinsts is not applied to insts. -*) -fun term_lift_inst_rule (st, i, Tinsts, insts, rule) = -let - val thy = Thm.theory_of_thm st - val cert = Thm.cterm_of thy - val certT = Thm.ctyp_of thy - val maxidx = Thm.maxidx_of st - val paramTs = map #2 (params_of_state i st) - val inc = maxidx+1 - fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> Logic.incr_tvar inc T) - (*lift only Var, not term, which must be lifted already*) - fun liftpair (v,t) = (cert (liftvar v), cert t) - fun liftTpair (((a, i), S), T) = - (certT (TVar ((a, i + inc), S)), - certT (Logic.incr_tvar inc T)) -in Drule.instantiate (map liftTpair Tinsts, map liftpair insts) - (Thm.lift_rule (Thm.cprem_of st i) rule) -end; - - (*** Applications of cut_rl ***)