# HG changeset patch # User Lars Noschinski # Date 1429285639 -7200 # Node ID 3334ababa5266d64b4390f4430dbbd23cfe720fd # Parent 2712f40d6309e98fdfd055e76a7e9b57dd013edb# Parent 5d90d301ad661ea08355a645718fc5c4c811307a merged diff -r 2712f40d6309 -r 3334ababa526 ANNOUNCE --- 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: diff -r 2712f40d6309 -r 3334ababa526 NEWS --- 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. diff -r 2712f40d6309 -r 3334ababa526 src/HOL/Algebra/FiniteProduct.thy --- 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) \\<^bsub>G\<^esub> A - else undefined)" + else \\<^bsub>G\<^esub>)" syntax "_finprod" :: "index => idt => 'a set => 'b => 'b" @@ -311,6 +311,10 @@ "finprod G f {} = \" by (simp add: finprod_def) +lemma (in comm_monoid) finprod_infinite[simp]: + "\ finite A \ finprod G f A = \" + by (simp add: finprod_def) + declare funcsetI [intro] funcset_mem [dest] @@ -335,28 +339,28 @@ done lemma finprod_one [simp]: - "finite A ==> (\i:A. \) = \" -proof (induct set: finite) + "(\i:A. \) = \" +proof (induct A rule: infinite_finite_induct) case empty show ?case by simp next case (insert a A) have "(%i. \) \ 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 \ A -> carrier G" + assumes f: "f \ A -> carrier G" shows "finprod G f A \ 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 \ carrier G" by fast from insert have A: "f \ A -> carrier G" by fast from insert A a show ?case by simp -qed +qed simp lemma funcset_Int_left [simp, intro]: "[| f \ A -> C; f \ B -> C |] ==> f \ A Int B -> C" @@ -390,9 +394,9 @@ done lemma finprod_multf: - "[| finite A; f \ A -> carrier G; g \ A -> carrier G |] ==> + "[| f \ A -> carrier G; g \ A -> carrier G |] ==> finprod G (%x. f x \ g x) A = (finprod G f A \ 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 \ 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) \ carrier G \ + "f : (h ` A) \ carrier G \ 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 "\ finite (h ` A)" + using finite_imageD by blast + with `\ 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 \ (\x\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. *) diff -r 2712f40d6309 -r 3334ababa526 src/HOL/Algebra/IntRing.thy --- 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 \ - where "finprod \ f A = (if finite A then setprod f A else undefined)" + where "finprod \ f A = setprod f A" proof - -- "Specification" show "comm_monoid \" by default auto @@ -83,28 +83,15 @@ { fix x y have "mult \ x y = x * y" by simp } note mult = this have one: "one \ = 1" by simp - show "finprod \ 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 \ f A = setprod f A" + by (induct A rule: infinite_finite_induct, auto) qed interpretation int: abelian_monoid \ where int_carrier_eq: "carrier \ = UNIV" and int_zero_eq: "zero \ = 0" and int_add_eq: "add \ x y = x + y" - and int_finsum_eq: "finsum \ f A = (if finite A then setsum f A else undefined)" + and int_finsum_eq: "finsum \ f A = setsum f A" proof - -- "Specification" show "abelian_monoid \" by default auto @@ -118,21 +105,8 @@ note add = this show zero: "zero \ = 0" by simp - show "finsum \ 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 \ f A = setsum f A" + by (induct A rule: infinite_finite_induct, auto) qed interpretation int: abelian_group \ @@ -143,7 +117,7 @@ where "carrier \ = UNIV" and "zero \ = 0" and "add \ x y = x + y" - and "finsum \ f A = (if finite A then setsum f A else undefined)" + and "finsum \ f A = setsum f A" and int_a_inv_eq: "a_inv \ x = - x" and int_a_minus_eq: "a_minus \ x y = x - y" proof - @@ -176,7 +150,7 @@ where "carrier \ = UNIV" and "zero \ = 0" and "add \ x y = x + y" - and "finsum \ f A = (if finite A then setsum f A else undefined)" + and "finsum \ f A = setsum f A" and "a_inv \ x = - x" and "a_minus \ x y = x - y" proof - diff -r 2712f40d6309 -r 3334ababa526 src/HOL/Algebra/Ring.thy --- 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 \ A -> carrier R |] ==> + "f \ 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 \ A -> carrier R |] ==> + "f \ 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] diff -r 2712f40d6309 -r 3334ababa526 src/HOL/Algebra/UnivPoly.thy --- 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 \ A -> carrier R |] ==> + "f \ 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