--- /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.
--- 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 ***
--- 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}
*}
--- 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
--- 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}%
--- 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
--- 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 \<le> 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) \<noteq> 0)" (is ?concl)
+lemma less_ncols: "(n < ncols A) = (? j i. n <= i & (Rep_matrix A j i) \<noteq> 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) = (\<forall> m. (\<forall> j i. m <= i \<longrightarrow> (Rep_matrix A j i) = 0) \<longrightarrow> n <= m)" (is ?concl)
+lemma le_ncols: "(n <= ncols A) = (\<forall> m. (\<forall> j i. m <= i \<longrightarrow> (Rep_matrix A j i) = 0) \<longrightarrow> 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 \<longrightarrow> (Rep_matrix A j i) = 0)" by (auto)
qed
-lemma less_nrows: "(m < nrows A) = (? j i. m <= j & (Rep_matrix A j i) \<noteq> 0)" (is ?concl)
+lemma less_nrows: "(m < nrows A) = (? j i. m <= j & (Rep_matrix A j i) \<noteq> 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) = (\<forall> m. (\<forall> j i. m <= j \<longrightarrow> (Rep_matrix A j i) = 0) \<longrightarrow> n <= m)" (is ?concl)
+lemma le_nrows: "(n <= nrows A) = (\<forall> m. (\<forall> j i. m <= j \<longrightarrow> (Rep_matrix A j i) = 0) \<longrightarrow> 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 \<longrightarrow> 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 \<longrightarrow> s i = t i) \<longrightarrow> foldseq f s m = foldseq f t m"
apply (induct_tac m)
@@ -496,10 +496,12 @@
have d:"!! s t. (\<forall>i\<le>n. s i = t i) \<Longrightarrow> foldseq f s n = foldseq f t n" by (simp add: a)
show "f (t 0) (foldseq f (\<lambda>k. s (Suc k)) n) = f (t 0) (foldseq f (\<lambda>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 \<Longrightarrow> 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 \<Longrightarrow> ?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. \<lbrakk>a <= Suc b; a \<noteq> Suc b\<rbrakk> \<Longrightarrow> a <= b" by arith
have a:"!! a b c . a = b \<Longrightarrow> 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 \<Longrightarrow> ?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 \<longrightarrow> 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 \<Longrightarrow> m \<noteq> n \<Longrightarrow> ? k. m-n = Suc k" by arith
have c: "0 <= m" by simp
have d: "!! k. k \<noteq> 0 \<Longrightarrow> ? 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 \<noteq> j \<longrightarrow> 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 \<longrightarrow> s i = 0" by simp
from s0 have b: "! i. j < i \<longrightarrow> 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 \<Rightarrow> (('a::zero) \<Rightarrow> ('b::zero) \<Rightarrow> ('c::zero)) \<Rightarrow> ('c \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> 'a matrix \<Rightarrow> 'b matrix \<Rightarrow> '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 \<le> n" (is ?An) "nrows B \<le> 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 \<le> n" (is ?An) "nrows B \<le> 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 "\<dots> = 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 "\<dots> = 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 \<Longrightarrow> 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 \<Longrightarrow> 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) \<Longrightarrow> 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) \<le> 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) \<le> 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 \<Longrightarrow> (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 \<Longrightarrow> 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 \<longrightarrow> s i <= t i) \<longrightarrow> 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 \<longrightarrow> s i <= t i) \<longrightarrow> 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 \<Longrightarrow> P j i" by blast
lemma neg_imp: "(\<not> Q \<longrightarrow> \<not> P) \<Longrightarrow> P \<longrightarrow> 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 "\<dots> = Y * (A * X)"
- apply (insert prems)
+ apply (insert assms)
apply (frule right_inverse_matrix_dim)
by (simp add: right_inverse_matrix_def)
also have "\<dots> = (Y * A) * X" by (simp add: mult_assoc)
also have "\<dots> = 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
--- 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;
--- 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;
--- 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 *)
--- 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);
--- 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) ||
--- 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
--- 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));
--- 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 ***)