--- a/ANNOUNCE Fri Apr 17 16:59:43 2015 +0200
+++ b/ANNOUNCE Fri Apr 17 17:47:19 2015 +0200
@@ -4,9 +4,28 @@
Isabelle2015 is now available.
This version improves upon Isabelle2014 in many ways, see the NEWS file in
-the distribution for more details. Important points are:
+the distribution for more details. Some important points are as follows.
+
+* Improved Isabelle/jEdit Prover IDE: folding / bracket matching for Isar,
+support for BibTeX files, improved graphview panel, improved scheduling for
+asynchronous print commands (e.g. Slegehammer provers).
+
+* Support for 'private' and 'qualified' name space modifiers.
+
+* Structural composition of proof methods (meth1; meth2) in Isar.
-* FIXME
+* HOL: BNF datatypes and codatatypes are now standard.
+
+* HOL: numerous tool improvements: Nitpick, Sledgehammer, SMT, including a
+new free (!) version of Z3.
+
+* HOL: numerous library refinements and enhancements.
+
+* New proof method "rewrite" for single-step rewriting with subterm
+selection based on patterns.
+
+* Updated manuals: datatypes, implementation, isar-ref, jedit, sledgehammer,
+system.
You may get Isabelle2015 from the following mirror sites:
--- a/NEWS Fri Apr 17 16:59:43 2015 +0200
+++ b/NEWS Fri Apr 17 17:47:19 2015 +0200
@@ -51,6 +51,11 @@
context, without implicit global state. Potential for accidental
INCOMPATIBILITY, make sure that required theories are really imported.
+* Historical command-line terminator ";" is no longer accepted (and
+already used differently in Isar). Minor INCOMPATIBILITY, use "isabelle
+update_semicolons" to remove obsolete semicolons from old theory
+sources.
+
* Structural composition of proof methods (meth1; meth2) in Isar
corresponds to (tac1 THEN_ALL_NEW tac2) in ML.
@@ -77,8 +82,8 @@
* Improved graphview panel with optional output of PNG or PDF, for
display of 'thy_deps', 'locale_deps', 'class_deps' etc.
-* Command 'thy_deps' allows optional bounds, analogously to
-'class_deps'.
+* The commands 'thy_deps' and 'class_deps' allow optional bounds to
+restrict the visualized hierarchy.
* Improved scheduling for asynchronous print commands (e.g. provers
managed by the Sledgehammer panel) wrt. ongoing document processing.
@@ -141,9 +146,6 @@
INCOMPATIBILITY, explicit instantiation sometimes needs to refer to
different index.
-* Command "class_deps" takes optional sort arguments to constrain then
-resulting class hierarchy.
-
* Lexical separation of signed and unsigned numerals: categories "num"
and "float" are unsigned. INCOMPATIBILITY: subtle change in precedence
of numeral signs, particularly in expressions involving infix syntax
@@ -198,6 +200,15 @@
BNF_Constructions_on_Wellorders ~> BNF_Wellorder_Constructions
Cardinals/Constructions_on_Wellorders ~> Cardinals/Wellorder_Constructions
INCOMPATIBILITY.
+ - Lifting and Transfer setup for basic HOL types sum and prod (also
+ option) is now performed by the BNF package. Theories Lifting_Sum,
+ Lifting_Product and Lifting_Option from Main became obsolete and
+ were removed. Changed definitions of the relators rel_prod and
+ rel_sum (using inductive).
+ INCOMPATIBILITY: use rel_prod.simps and rel_sum.simps instead
+ of rel_prod_def and rel_sum_def.
+ Minor INCOMPATIBILITY: (rarely used by name) transfer theorem names
+ changed (e.g. map_prod_transfer ~> prod.map_transfer).
* Old datatype package:
- The old 'datatype' command has been renamed 'old_datatype', and
@@ -464,10 +475,6 @@
look-and-feel, via internal class name or symbolic name as in the jEdit
menu Global Options / Appearance.
-* Historical command-line terminator ";" is no longer accepted. Minor
-INCOMPATIBILITY, use "isabelle update_semicolons" to remove obsolete
-semicolons from theory sources.
-
* Support for Proof General and Isar TTY loop has been discontinued.
Minor INCOMPATIBILITY, use standard PIDE infrastructure instead.
--- a/src/HOL/Algebra/FiniteProduct.thy Fri Apr 17 16:59:43 2015 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy Fri Apr 17 17:47:19 2015 +0200
@@ -292,7 +292,7 @@
where "finprod G f A =
(if finite A
then foldD (carrier G) (mult G o f) \<one>\<^bsub>G\<^esub> A
- else undefined)"
+ else \<one>\<^bsub>G\<^esub>)"
syntax
"_finprod" :: "index => idt => 'a set => 'b => 'b"
@@ -311,6 +311,10 @@
"finprod G f {} = \<one>"
by (simp add: finprod_def)
+lemma (in comm_monoid) finprod_infinite[simp]:
+ "\<not> finite A \<Longrightarrow> finprod G f A = \<one>"
+ by (simp add: finprod_def)
+
declare funcsetI [intro]
funcset_mem [dest]
@@ -335,28 +339,28 @@
done
lemma finprod_one [simp]:
- "finite A ==> (\<Otimes>i:A. \<one>) = \<one>"
-proof (induct set: finite)
+ "(\<Otimes>i:A. \<one>) = \<one>"
+proof (induct A rule: infinite_finite_induct)
case empty show ?case by simp
next
case (insert a A)
have "(%i. \<one>) \<in> A -> carrier G" by auto
with insert show ?case by simp
-qed
+qed simp
lemma finprod_closed [simp]:
fixes A
- assumes fin: "finite A" and f: "f \<in> A -> carrier G"
+ assumes f: "f \<in> A -> carrier G"
shows "finprod G f A \<in> carrier G"
-using fin f
-proof induct
+using f
+proof (induct A rule: infinite_finite_induct)
case empty show ?case by simp
next
case (insert a A)
then have a: "f a \<in> carrier G" by fast
from insert have A: "f \<in> A -> carrier G" by fast
from insert A a show ?case by simp
-qed
+qed simp
lemma funcset_Int_left [simp, intro]:
"[| f \<in> A -> C; f \<in> B -> C |] ==> f \<in> A Int B -> C"
@@ -390,9 +394,9 @@
done
lemma finprod_multf:
- "[| finite A; f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
+ "[| f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
finprod G (%x. f x \<otimes> g x) A = (finprod G f A \<otimes> finprod G g A)"
-proof (induct set: finite)
+proof (induct A rule: infinite_finite_induct)
case empty show ?case by simp
next
case (insert a A) then
@@ -404,7 +408,7 @@
by (simp add: Pi_def)
show ?case
by (simp add: insert fA fa gA ga fgA m_ac)
-qed
+qed simp
lemma finprod_cong':
"[| A = B; g \<in> B -> carrier G;
@@ -443,7 +447,7 @@
qed
with prems show ?thesis by simp
next
- case False with prems show ?thesis by (simp add: finprod_def)
+ case False with prems show ?thesis by simp
qed
qed
@@ -494,23 +498,26 @@
(* The following two were contributed by Jeremy Avigad. *)
lemma finprod_reindex:
- assumes fin: "finite A"
- shows "f : (h ` A) \<rightarrow> carrier G \<Longrightarrow>
+ "f : (h ` A) \<rightarrow> carrier G \<Longrightarrow>
inj_on h A ==> finprod G f (h ` A) = finprod G (%x. f (h x)) A"
- using fin
- by induct (auto simp add: Pi_def)
+proof (induct A rule: infinite_finite_induct)
+ case (infinite A)
+ hence "\<not> finite (h ` A)"
+ using finite_imageD by blast
+ with `\<not> finite A` show ?case by simp
+qed (auto simp add: Pi_def)
lemma finprod_const:
- assumes fin [simp]: "finite A"
- and a [simp]: "a : carrier G"
+ assumes a [simp]: "a : carrier G"
shows "finprod G (%x. a) A = a (^) card A"
- using fin apply induct
- apply force
- apply (subst finprod_insert)
- apply auto
- apply (subst m_comm)
- apply auto
- done
+proof (induct A rule: infinite_finite_induct)
+ case (insert b A)
+ show ?case
+ proof (subst finprod_insert[OF insert(1-2)])
+ show "a \<otimes> (\<Otimes>x\<in>A. a) = a (^) card (insert b A)"
+ by (insert insert, auto, subst m_comm, auto)
+ qed auto
+qed auto
(* The following lemma was contributed by Jesus Aransay. *)
--- a/src/HOL/Algebra/IntRing.thy Fri Apr 17 16:59:43 2015 +0200
+++ b/src/HOL/Algebra/IntRing.thy Fri Apr 17 17:47:19 2015 +0200
@@ -73,7 +73,7 @@
qed
interpretation int: comm_monoid \<Z>
- where "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
+ where "finprod \<Z> f A = setprod f A"
proof -
-- "Specification"
show "comm_monoid \<Z>" by default auto
@@ -83,28 +83,15 @@
{ fix x y have "mult \<Z> x y = x * y" by simp }
note mult = this
have one: "one \<Z> = 1" by simp
- show "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
- proof (cases "finite A")
- case True
- then show ?thesis
- proof induct
- case empty
- show ?case by (simp add: one)
- next
- case insert
- then show ?case by (simp add: Pi_def mult)
- qed
- next
- case False
- then show ?thesis by (simp add: finprod_def)
- qed
+ show "finprod \<Z> f A = setprod f A"
+ by (induct A rule: infinite_finite_induct, auto)
qed
interpretation int: abelian_monoid \<Z>
where int_carrier_eq: "carrier \<Z> = UNIV"
and int_zero_eq: "zero \<Z> = 0"
and int_add_eq: "add \<Z> x y = x + y"
- and int_finsum_eq: "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
+ and int_finsum_eq: "finsum \<Z> f A = setsum f A"
proof -
-- "Specification"
show "abelian_monoid \<Z>" by default auto
@@ -118,21 +105,8 @@
note add = this
show zero: "zero \<Z> = 0"
by simp
- show "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
- proof (cases "finite A")
- case True
- then show ?thesis
- proof induct
- case empty
- show ?case by (simp add: zero)
- next
- case insert
- then show ?case by (simp add: Pi_def add)
- qed
- next
- case False
- then show ?thesis by (simp add: finsum_def finprod_def)
- qed
+ show "finsum \<Z> f A = setsum f A"
+ by (induct A rule: infinite_finite_induct, auto)
qed
interpretation int: abelian_group \<Z>
@@ -143,7 +117,7 @@
where "carrier \<Z> = UNIV"
and "zero \<Z> = 0"
and "add \<Z> x y = x + y"
- and "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
+ and "finsum \<Z> f A = setsum f A"
and int_a_inv_eq: "a_inv \<Z> x = - x"
and int_a_minus_eq: "a_minus \<Z> x y = x - y"
proof -
@@ -176,7 +150,7 @@
where "carrier \<Z> = UNIV"
and "zero \<Z> = 0"
and "add \<Z> x y = x + y"
- and "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
+ and "finsum \<Z> f A = setsum f A"
and "a_inv \<Z> x = - x"
and "a_minus \<Z> x y = x - y"
proof -
--- a/src/HOL/Algebra/Ring.thy Fri Apr 17 16:59:43 2015 +0200
+++ b/src/HOL/Algebra/Ring.thy Fri Apr 17 17:47:19 2015 +0200
@@ -143,6 +143,7 @@
lemmas finsum_Suc = add.finprod_Suc
lemmas finsum_Suc2 = add.finprod_Suc2
lemmas finsum_add = add.finprod_mult
+lemmas finsum_infinite = add.finprod_infinite
lemmas finsum_cong = add.finprod_cong
text {*Usually, if this rule causes a failed congruence proof error,
@@ -680,22 +681,14 @@
qed
lemma (in ring_hom_cring) hom_finsum [simp]:
- "[| finite A; f \<in> A -> carrier R |] ==>
+ "f \<in> A -> carrier R ==>
h (finsum R f A) = finsum S (h o f) A"
-proof (induct set: finite)
- case empty then show ?case by simp
-next
- case insert then show ?case by (simp add: Pi_def)
-qed
+ by (induct A rule: infinite_finite_induct, auto simp: Pi_def)
lemma (in ring_hom_cring) hom_finprod:
- "[| finite A; f \<in> A -> carrier R |] ==>
+ "f \<in> A -> carrier R ==>
h (finprod R f A) = finprod S (h o f) A"
-proof (induct set: finite)
- case empty then show ?case by simp
-next
- case insert then show ?case by (simp add: Pi_def)
-qed
+ by (induct A rule: infinite_finite_induct, auto simp: Pi_def)
declare ring_hom_cring.hom_finprod [simp]
--- a/src/HOL/Algebra/UnivPoly.thy Fri Apr 17 16:59:43 2015 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Fri Apr 17 17:47:19 2015 +0200
@@ -1208,13 +1208,9 @@
maybe it is not that necessary.*}
lemma (in ring_hom_ring) hom_finsum [simp]:
- "[| finite A; f \<in> A -> carrier R |] ==>
+ "f \<in> A -> carrier R ==>
h (finsum R f A) = finsum S (h o f) A"
-proof (induct set: finite)
- case empty then show ?case by simp
-next
- case insert then show ?case by (simp add: Pi_def)
-qed
+ by (induct A rule: infinite_finite_induct, auto simp: Pi_def)
context UP_pre_univ_prop
begin