# HG changeset patch # User wenzelm # Date 1126728488 -7200 # Node ID 495c799df31d88b8cc6fb2bc7fa743db3dcda49e # Parent 40ce48cc45f74b22995ea170f77b98d4b3d02a73 tuned headers etc.; diff -r 40ce48cc45f7 -r 495c799df31d src/HOL/Commutative_Ring.thy --- a/src/HOL/Commutative_Ring.thy Wed Sep 14 22:04:38 2005 +0200 +++ b/src/HOL/Commutative_Ring.thy Wed Sep 14 22:08:08 2005 +0200 @@ -1,31 +1,32 @@ - (* ID: $Id$ Author: Bernhard Haeupler - Proving equalities in a commutative Ring done "right" in Isabelle/HOL +Proving equalities in commutative rings done "right" in Isabelle/HOL. *) +header {* Proving equalities in commutative rings *} + theory Commutative_Ring imports List uses ("Tools/comm_ring.ML") begin (* Syntax of multivariate polynomials (pol) and polynomial expressions*) -datatype 'a pol = - Pc 'a - | Pinj nat "'a pol" +datatype 'a pol = + Pc 'a + | Pinj nat "'a pol" | PX "'a pol" nat "'a pol" -datatype 'a polex = - Pol "'a pol" - | Add "'a polex" "'a polex" - | Sub "'a polex" "'a polex" - | Mul "'a polex" "'a polex" +datatype 'a polex = + Pol "'a pol" + | Add "'a polex" "'a polex" + | Sub "'a polex" "'a polex" + | Mul "'a polex" "'a polex" | Pow "'a polex" nat | Neg "'a polex" (* Interpretation functions for the shadow syntax *) -consts +consts Ipol :: "('a::{comm_ring,recpower}) list \ 'a pol \ 'a" Ipolex :: "('a::{comm_ring,recpower}) list \ 'a polex \ 'a" @@ -44,7 +45,7 @@ (* Create polynomial normalized polynomials given normalized inputs *) constdefs mkPinj :: "nat \ 'a pol \ 'a pol" - mkPinj_def: "mkPinj x P \ (case P of + mkPinj_def: "mkPinj x P \ (case P of (Pc c) \ (Pc c) | (Pinj y P) \ Pinj (x+y) P | (PX p1 y p2) \ Pinj x P )" @@ -71,21 +72,21 @@ "add (Pinj i P, Pc c) = Pinj i (add (P, Pc c))" "add (Pc c, PX P i Q) = PX P i (add (Q, Pc c))" "add (PX P i Q, Pc c) = PX P i (add (Q, Pc c))" - "add (Pinj x P, Pinj y Q) = - (if x=y then mkPinj x (add (P, Q)) + "add (Pinj x P, Pinj y Q) = + (if x=y then mkPinj x (add (P, Q)) else (if x>y then mkPinj y (add (Pinj (x-y) P, Q)) else mkPinj x (add (Pinj (y-x) Q, P)) ))" - "add (Pinj x P, PX Q y R) = - (if x=0 then add(P, PX Q y R) - else (if x=1 then PX Q y (add (R, P)) + "add (Pinj x P, PX Q y R) = + (if x=0 then add(P, PX Q y R) + else (if x=1 then PX Q y (add (R, P)) else PX Q y (add (R, Pinj (x - 1) P))))" - "add (PX P x R, Pinj y Q) = - (if y=0 then add(PX P x R, Q) - else (if y=1 then PX P x (add (R, Q)) + "add (PX P x R, Pinj y Q) = + (if y=0 then add(PX P x R, Q) + else (if y=1 then PX P x (add (R, Q)) else PX P x (add (R, Pinj (y - 1) Q))))" - "add (PX P1 x P2, PX Q1 y Q2) = - (if x=y then mkPX (add (P1, Q1)) x (add (P2, Q2)) - else (if x>y then mkPX (add (PX P1 (x-y) (Pc 0), Q1)) y (add (P2,Q2)) + "add (PX P1 x P2, PX Q1 y Q2) = + (if x=y then mkPX (add (P1, Q1)) x (add (P2, Q2)) + else (if x>y then mkPX (add (PX P1 (x-y) (Pc 0), Q1)) y (add (P2,Q2)) else mkPX (add (PX Q1 (y-x) (Pc 0), P1)) x (add (P2,Q2)) ))" (* Multiplication *) @@ -93,24 +94,24 @@ "mul (Pc a, Pc b) = Pc (a*b)" "mul (Pc c, Pinj i P) = (if c=0 then Pc 0 else mkPinj i (mul (P, Pc c)))" "mul (Pinj i P, Pc c) = (if c=0 then Pc 0 else mkPinj i (mul (P, Pc c)))" - "mul (Pc c, PX P i Q) = + "mul (Pc c, PX P i Q) = (if c=0 then Pc 0 else mkPX (mul (P, Pc c)) i (mul (Q, Pc c)))" - "mul (PX P i Q, Pc c) = + "mul (PX P i Q, Pc c) = (if c=0 then Pc 0 else mkPX (mul (P, Pc c)) i (mul (Q, Pc c)))" - "mul (Pinj x P, Pinj y Q) = - (if x=y then mkPinj x (mul (P, Q)) + "mul (Pinj x P, Pinj y Q) = + (if x=y then mkPinj x (mul (P, Q)) else (if x>y then mkPinj y (mul (Pinj (x-y) P, Q)) else mkPinj x (mul (Pinj (y-x) Q, P)) ))" - "mul (Pinj x P, PX Q y R) = - (if x=0 then mul(P, PX Q y R) - else (if x=1 then mkPX (mul (Pinj x P, Q)) y (mul (R, P)) + "mul (Pinj x P, PX Q y R) = + (if x=0 then mul(P, PX Q y R) + else (if x=1 then mkPX (mul (Pinj x P, Q)) y (mul (R, P)) else mkPX (mul (Pinj x P, Q)) y (mul (R, Pinj (x - 1) P))))" - "mul (PX P x R, Pinj y Q) = - (if y=0 then mul(PX P x R, Q) - else (if y=1 then mkPX (mul (Pinj y Q, P)) x (mul (R, Q)) + "mul (PX P x R, Pinj y Q) = + (if y=0 then mul(PX P x R, Q) + else (if y=1 then mkPX (mul (Pinj y Q, P)) x (mul (R, Q)) else mkPX (mul (Pinj y Q, P)) x (mul (R, Pinj (y - 1) Q))))" - "mul (PX P1 x P2, PX Q1 y Q2) = - add (mkPX (mul (P1, Q1)) (x+y) (mul (P2, Q2)), + "mul (PX P1 x P2, PX Q1 y Q2) = + add (mkPX (mul (P1, Q1)) (x+y) (mul (P2, Q2)), add (mkPX (mul (P1, mkPinj 1 Q2)) x (Pc 0), mkPX (mul (Q1, mkPinj 1 P2)) y (Pc 0)) )" (hints simp add: mkPinj_def split: pol.split) @@ -146,16 +147,16 @@ lemma number_of_nat_even: "even (number_of (w BIT bit.B0)::nat)" by simp - + lemma pow_even : "pow (p, number_of(w BIT bit.B0)) = pow (sqr p, number_of w)" ( is "pow(?p,?n) = pow (_,?n2)") proof- have "even ?n" by simp - hence "pow (p, ?n) = pow (sqr p, ?n div 2)" + hence "pow (p, ?n) = pow (sqr p, ?n div 2)" apply simp apply (cases "IntDef.neg (number_of w)") apply simp - done + done *) (* Normalization of polynomial expressions *) @@ -197,7 +198,7 @@ then obtain d where "d+y=x".. with prems have ?case by (auto simp add: mkPinj_ci ring_eq_simps) } ultimately show ?case by blast -next +next case (7 x P Q y R) have "x=0 \ (x = 1) \ (x > 1)" by arith moreover @@ -219,7 +220,7 @@ then obtain d where "d+1=y" .. with prems have ?case by auto } ultimately show ?case by blast -next +next case (9 P1 x P2 Q1 y Q2) have "y < x \ x = y \ x < y" by arith moreover @@ -236,8 +237,8 @@ qed (auto simp add: ring_eq_simps) (* Multiplication *) -lemma mul_ci: "ALL l. Ipol l (mul (P, Q)) = Ipol l P * Ipol l Q" - by (induct P Q rule: mul.induct, auto simp add: mkPX_ci mkPinj_ci ring_eq_simps add_ci power_add) +lemma mul_ci: "ALL l. Ipol l (mul (P, Q)) = Ipol l P * Ipol l Q" + by (induct P Q rule: mul.induct, auto simp add: mkPX_ci mkPinj_ci ring_eq_simps add_ci power_add) (* Substraction *) lemma sub_ci: "\ l. Ipol l (sub p q) = (Ipol l p) - (Ipol l q)" @@ -254,7 +255,7 @@ proof(induct n rule: nat_less_induct) case (1 k) have two:"2=Suc( Suc 0)" by simp - from prems show ?case + from prems show ?case proof(cases k) case (Suc l) hence KL:"k=Suc l" by simp @@ -272,12 +273,12 @@ {assume OL:"odd l" with prems have "\\mp. Ipol ls (pow (p, m)) = Ipol ls p ^ m; k = Suc l; odd l\ \ \p. Ipol ls (sqr p) ^ (Suc l div 2) = Ipol ls p ^ Suc l" proof(cases l) - case (Suc w) - from prems have EW:"even w" by simp - from two have two_times:"(2 * (w div 2))= w" by (simp only: even_nat_div_two_times_two[OF EW]) - have A:"ALL p. (Ipol ls p * Ipol ls p) = (Ipol ls p) ^ (Suc (Suc 0))" by (simp add: power_Suc) - from A two[symmetric] have "ALL p.(Ipol ls p * Ipol ls p) = (Ipol ls p) ^ 2" by simp - with prems show ?thesis by (auto simp add: power_mult[symmetric, of _ 2 _] two_times mul_ci sqr_ci) + case (Suc w) + from prems have EW:"even w" by simp + from two have two_times:"(2 * (w div 2))= w" by (simp only: even_nat_div_two_times_two[OF EW]) + have A:"ALL p. (Ipol ls p * Ipol ls p) = (Ipol ls p) ^ (Suc (Suc 0))" by (simp add: power_Suc) + from A two[symmetric] have "ALL p.(Ipol ls p * Ipol ls p) = (Ipol ls p) ^ 2" by simp + with prems show ?thesis by (auto simp add: power_mult[symmetric, of _ 2 _] two_times mul_ci sqr_ci) qed(simp) with prems have ?thesis by simp } ultimately show ?thesis by blast @@ -290,7 +291,7 @@ (* Reflection lemma: Key to the (incomplete) decision procedure *) lemma norm_eq: - assumes A:"norm P1 = norm P2" + assumes A:"norm P1 = norm P2" shows "Ipolex l P1 = Ipolex l P2" proof - from A have "Ipol l (norm P1) = Ipol l (norm P2)" by simp @@ -303,8 +304,7 @@ Does not work, since no generic ring operations implementation is there generate_code ("ring.ML") test = "norm"*) - - use "Tools/comm_ring.ML" +use "Tools/comm_ring.ML" setup "CommRing.setup" end diff -r 40ce48cc45f7 -r 495c799df31d src/HOL/ex/Adder.thy --- a/src/HOL/ex/Adder.thy Wed Sep 14 22:04:38 2005 +0200 +++ b/src/HOL/ex/Adder.thy Wed Sep 14 22:08:08 2005 +0200 @@ -1,11 +1,9 @@ (* Title: HOL/ex/Adder.thy ID: $Id$ Author: Sergey Tverdyshev (Universitaet des Saarlandes) - -Implementation of carry chain incrementor and adder. *) -header{* Adder *} +header {* Implementation of carry chain incrementor and adder *} theory Adder imports Main Word begin diff -r 40ce48cc45f7 -r 495c799df31d src/HOL/ex/CTL.thy --- a/src/HOL/ex/CTL.thy Wed Sep 14 22:04:38 2005 +0200 +++ b/src/HOL/ex/CTL.thy Wed Sep 14 22:08:08 2005 +0200 @@ -1,4 +1,3 @@ - (* Title: HOL/ex/CTL.thy ID: $Id$ Author: Gertrud Bauer @@ -8,8 +7,6 @@ theory CTL imports Main begin - - text {* We formalize basic concepts of Computational Tree Logic (CTL) \cite{McMillan-PhDThesis,McMillan-LectureNotes} within the diff -r 40ce48cc45f7 -r 495c799df31d src/HOL/ex/Commutative_RingEx.thy --- a/src/HOL/ex/Commutative_RingEx.thy Wed Sep 14 22:04:38 2005 +0200 +++ b/src/HOL/ex/Commutative_RingEx.thy Wed Sep 14 22:08:08 2005 +0200 @@ -1,10 +1,13 @@ - (* $Id$ *) +(* ID: $Id$ + Author: Bernhard Haeupler +*) + +header {* Some examples demonstrating the comm-ring method *} + theory Commutative_RingEx imports Main begin - (* Some examples demonstrating the comm_ring method *) - lemma "4*(x::int)^5*y^3*x^2*3 + x*z + 3^5 = 12*x^7*y^3 + z*x + 243" by comm_ring @@ -44,4 +47,4 @@ lemma "(a::int)^10 - b^10 = (a - b) * (a^9 + a^8*b + a^7*b^2 + a^6*b^3 + a^5*b^4 + a^4*b^5 + a^3*b^6 + a^2*b^7 + a*b^8 + b^9 )" by comm_ring -end \ No newline at end of file +end diff -r 40ce48cc45f7 -r 495c799df31d src/HOL/ex/Commutative_Ring_Complete.thy --- a/src/HOL/ex/Commutative_Ring_Complete.thy Wed Sep 14 22:04:38 2005 +0200 +++ b/src/HOL/ex/Commutative_Ring_Complete.thy Wed Sep 14 22:08:08 2005 +0200 @@ -1,9 +1,12 @@ (* ID: $Id$ Author: Bernhard Haeupler - This theory is about the relative completeness of the tactic - As long as the reified atomic polynomials of type 'a pol - are in normal form, the cring method is complete *) +This theory is about of the relative completeness of method comm-ring +method. As long as the reified atomic polynomials of type 'a pol are +in normal form, the cring method is complete. +*) + +header {* Proof of the relative completeness of method comm-ring *} theory Commutative_Ring_Complete imports Main @@ -381,4 +384,4 @@ qed(simp) qed -end \ No newline at end of file +end diff -r 40ce48cc45f7 -r 495c799df31d src/HOL/ex/InductiveInvariant.thy --- a/src/HOL/ex/InductiveInvariant.thy Wed Sep 14 22:04:38 2005 +0200 +++ b/src/HOL/ex/InductiveInvariant.thy Wed Sep 14 22:08:08 2005 +0200 @@ -1,12 +1,15 @@ +(* ID: $Id$ + Author: Sava Krsti\'{c} and John Matthews +*) + +header {* Some of the results in Inductive Invariants for Nested Recursion *} + theory InductiveInvariant imports Main begin -(** Authors: Sava Krsti\'{c} and John Matthews **) -(** Date: Sep 12, 2003 **) - -text {* A formalization of some of the results in - \emph{Inductive Invariants for Nested Recursion}, - by Sava Krsti\'{c} and John Matthews. - Appears in the proceedings of TPHOLs 2003, LNCS vol. 2758, pp. 253-269. *} +text {* A formalization of some of the results in \emph{Inductive + Invariants for Nested Recursion}, by Sava Krsti\'{c} and John + Matthews. Appears in the proceedings of TPHOLs 2003, LNCS + vol. 2758, pp. 253-269. *} text "S is an inductive invariant of the functional F with respect to the wellfounded relation r." @@ -86,4 +89,4 @@ ==> S x (f x)" by (simp add: indinv_on_wfrec) -end \ No newline at end of file +end diff -r 40ce48cc45f7 -r 495c799df31d src/HOL/ex/InductiveInvariant_examples.thy --- a/src/HOL/ex/InductiveInvariant_examples.thy Wed Sep 14 22:04:38 2005 +0200 +++ b/src/HOL/ex/InductiveInvariant_examples.thy Wed Sep 14 22:08:08 2005 +0200 @@ -1,7 +1,10 @@ -theory InductiveInvariant_examples imports InductiveInvariant begin +(* ID: $Id$ + Author: Sava Krsti\'{c} and John Matthews +*) -(** Authors: Sava Krsti\'{c} and John Matthews **) -(** Date: Oct 17, 2003 **) +header {* Example use if an inductive invariant to solve termination conditions *} + +theory InductiveInvariant_examples imports InductiveInvariant begin text "A simple example showing how to use an inductive invariant to solve termination conditions generated by recdef on @@ -124,4 +127,4 @@ by (subst ninety_one.simps, simp add: ninety_one_tc measure_def inv_image_def) -end \ No newline at end of file +end diff -r 40ce48cc45f7 -r 495c799df31d src/HOL/ex/Intuitionistic.thy --- a/src/HOL/ex/Intuitionistic.thy Wed Sep 14 22:04:38 2005 +0200 +++ b/src/HOL/ex/Intuitionistic.thy Wed Sep 14 22:08:08 2005 +0200 @@ -3,11 +3,11 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge -Higher-Order Logic: Intuitionistic predicate calculus problems - Taken from FOL/ex/int.ML *) +header {* Higher-Order Logic: Intuitionistic predicate calculus problems *} + theory Intuitionistic imports Main begin diff -r 40ce48cc45f7 -r 495c799df31d src/HOL/ex/Lagrange.thy --- a/src/HOL/ex/Lagrange.thy Wed Sep 14 22:04:38 2005 +0200 +++ b/src/HOL/ex/Lagrange.thy Wed Sep 14 22:08:08 2005 +0200 @@ -2,28 +2,31 @@ ID: $Id$ Author: Tobias Nipkow Copyright 1996 TU Muenchen - - -This theory only contains a single theorem, which is a lemma in Lagrange's -proof that every natural number is the sum of 4 squares. Its sole purpose is -to demonstrate ordered rewriting for commutative rings. - -The enterprising reader might consider proving all of Lagrange's theorem. *) +header {* A lemma for Lagrange's theorem *} + theory Lagrange imports Main begin +text {* This theory only contains a single theorem, which is a lemma +in Lagrange's proof that every natural number is the sum of 4 squares. +Its sole purpose is to demonstrate ordered rewriting for commutative +rings. + +The enterprising reader might consider proving all of Lagrange's +theorem. *} + constdefs sq :: "'a::times => 'a" "sq x == x*x" -(* The following lemma essentially shows that every natural number is the sum -of four squares, provided all prime numbers are. However, this is an -abstract theorem about commutative rings. It has, a priori, nothing to do -with nat.*) +text {* The following lemma essentially shows that every natural +number is the sum of four squares, provided all prime numbers are. +However, this is an abstract theorem about commutative rings. It has, +a priori, nothing to do with nat. *} ML"Delsimprocs[ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]" -(*once a slow step, but now (2001) just three seconds!*) +-- {* once a slow step, but now (2001) just three seconds! *} lemma Lagrange_lemma: "!!x1::'a::comm_ring. (sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) = @@ -36,7 +39,6 @@ text{*A challenge by John Harrison. Takes about 74s on a 2.5GHz Apple G5.*} -(* lemma "!!p1::'a::comm_ring. (sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) * (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2) @@ -48,6 +50,8 @@ sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) + sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) + sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)" +oops +(* by(simp add: sq_def ring_eq_simps) *) diff -r 40ce48cc45f7 -r 495c799df31d src/HOL/ex/Locales.thy --- a/src/HOL/ex/Locales.thy Wed Sep 14 22:04:38 2005 +0200 +++ b/src/HOL/ex/Locales.thy Wed Sep 14 22:08:08 2005 +0200 @@ -3,7 +3,7 @@ Author: Markus Wenzel, LMU München *) -header {* Using locales in Isabelle/Isar *} +header {* Using locales in Isabelle/Isar -- outdated version! *} theory Locales imports Main begin diff -r 40ce48cc45f7 -r 495c799df31d src/HOL/ex/MonoidGroup.thy --- a/src/HOL/ex/MonoidGroup.thy Wed Sep 14 22:04:38 2005 +0200 +++ b/src/HOL/ex/MonoidGroup.thy Wed Sep 14 22:08:08 2005 +0200 @@ -1,11 +1,9 @@ (* Title: HOL/ex/MonoidGroup.thy ID: $Id$ Author: Markus Wenzel - -Monoids and Groups as predicates over record schemes. *) -header {* Monoids and Groups *} +header {* Monoids and Groups as predicates over record schemes *} theory MonoidGroup imports Main begin diff -r 40ce48cc45f7 -r 495c799df31d src/HOL/ex/PresburgerEx.thy --- a/src/HOL/ex/PresburgerEx.thy Wed Sep 14 22:04:38 2005 +0200 +++ b/src/HOL/ex/PresburgerEx.thy Wed Sep 14 22:08:08 2005 +0200 @@ -1,9 +1,9 @@ (* Title: HOL/ex/PresburgerEx.thy ID: $Id$ Author: Amine Chaieb, TU Muenchen +*) -Some examples for Presburger Arithmetic -*) +header {* Some examples for Presburger Arithmetic *} theory PresburgerEx imports Main begin diff -r 40ce48cc45f7 -r 495c799df31d src/HOL/ex/Puzzle.thy --- a/src/HOL/ex/Puzzle.thy Wed Sep 14 22:04:38 2005 +0200 +++ b/src/HOL/ex/Puzzle.thy Wed Sep 14 22:08:08 2005 +0200 @@ -8,6 +8,8 @@ Proof due to Herbert Ehler *) +header {* A question from ``Bundeswettbewerb Mathematik'' *} + theory Puzzle imports Main begin consts f :: "nat => nat" diff -r 40ce48cc45f7 -r 495c799df31d src/HOL/ex/Quickcheck_Examples.thy --- a/src/HOL/ex/Quickcheck_Examples.thy Wed Sep 14 22:04:38 2005 +0200 +++ b/src/HOL/ex/Quickcheck_Examples.thy Wed Sep 14 22:08:08 2005 +0200 @@ -144,5 +144,3 @@ oops end - - diff -r 40ce48cc45f7 -r 495c799df31d src/HOL/ex/Reflected_Presburger.thy --- a/src/HOL/ex/Reflected_Presburger.thy Wed Sep 14 22:04:38 2005 +0200 +++ b/src/HOL/ex/Reflected_Presburger.thy Wed Sep 14 22:08:08 2005 +0200 @@ -1,10 +1,15 @@ -(* A formalization of quantifier elimination for Presburger arithmetic*) -(* based on a generic quantifier elimination algorithm and - cooper's methos to eliminate on \ *) +(* Title: HOL/ex/PresburgerEx.thy + ID: $Id$ + Author: Amine Chaieb, TU Muenchen + +A formalization of quantifier elimination for Presburger arithmetic +based on a generic quantifier elimination algorithm and Cooper's +methos to eliminate on \. *) + +header {* Quantifier elimination for Presburger arithmetic *} theory Reflected_Presburger imports Main -(* uses ("rcooper.ML") ("rpresbtac.ML") *) begin (* Shadow syntax for integer terms *) @@ -2051,7 +2056,6 @@ and dvd: "i dvd l" shows "(i*x + r = 0) = (l*x + ((l div i)*r) = 0)" proof- - thm dvd_div_pos[OF lpos inz dvd] have ldvdii: "(l div i)*i = l" by (rule dvd_div_pos[OF lpos inz dvd]) have ldivinz: "l div i \ 0" using inz ldvdii lpos by auto have "(i*x + r = 0) = ((l div i)*(i*x + r) = (l div i)*0)" @@ -2224,7 +2228,6 @@ assume nz: "n=0" from prems have inz: "i \ 0" by auto from prems nz have idvdl: "i dvd l" by simp - thm adjustcoeff_eq_corr[OF lpos inz idvdl] have "(i * a + (i' * (a # ats) ! n' + I_intterm (a # ats) r) = 0) = (l * a + l div i * (i' * (a # ats) ! n' + I_intterm (a # ats) r) = 0)" by (rule adjustcoeff_eq_corr[OF lpos inz idvdl]) @@ -2700,7 +2703,6 @@ assumes linp: "islinform p" shows "alldivide (divlcm p,p)" -thm nz_le[OF divlcm_pos[OF linp]] using linp divlcm_pos proof (induct p rule: divlcm.induct,simp_all add: zdvd_refl_abs,clarsimp simp add: Nat.gr0_conv_Suc) case (goal1 f) @@ -5722,4 +5724,5 @@ use "rpresbtac.ML" setup RPresburger.setup *) + end diff -r 40ce48cc45f7 -r 495c799df31d src/HOL/ex/SVC_Oracle.thy --- a/src/HOL/ex/SVC_Oracle.thy Wed Sep 14 22:04:38 2005 +0200 +++ b/src/HOL/ex/SVC_Oracle.thy Wed Sep 14 22:08:08 2005 +0200 @@ -3,10 +3,10 @@ Author: Lawrence C Paulson Copyright 1999 University of Cambridge -Installing the oracle for SVC (Stanford Validity Checker) +Based upon the work of Søren T. Heilmann. +*) -Based upon the work of Søren T. Heilmann -*) +header {* Installing an oracle for SVC (Stanford Validity Checker) *} theory SVC_Oracle imports Main diff -r 40ce48cc45f7 -r 495c799df31d src/HOL/ex/StringEx.thy --- a/src/HOL/ex/StringEx.thy Wed Sep 14 22:04:38 2005 +0200 +++ b/src/HOL/ex/StringEx.thy Wed Sep 14 22:08:08 2005 +0200 @@ -1,3 +1,4 @@ +(* $Id$ *) header {* String examples *} diff -r 40ce48cc45f7 -r 495c799df31d src/HOL/ex/Tuple.thy --- a/src/HOL/ex/Tuple.thy Wed Sep 14 22:04:38 2005 +0200 +++ b/src/HOL/ex/Tuple.thy Wed Sep 14 22:08:08 2005 +0200 @@ -1,11 +1,6 @@ (* Title: HOL/ex/Tuple.thy ID: $Id$ Author: Markus Wenzel, TU Muenchen - -Properly nested products (see also theory Prod). - -Unquestionably, this should be used as the standard representation of -tuples in HOL, but it breaks many existing theories! *) header {* Properly nested products *} diff -r 40ce48cc45f7 -r 495c799df31d src/HOL/ex/svc_test.thy --- a/src/HOL/ex/svc_test.thy Wed Sep 14 22:04:38 2005 +0200 +++ b/src/HOL/ex/svc_test.thy Wed Sep 14 22:08:08 2005 +0200 @@ -1,5 +1,11 @@ -svc_test = SVC_Oracle + +(* $Id$ *) + +header {* Demonstrating the interface SVC *} + +theory svc_test +imports SVC_Oracle +begin syntax "<->" :: [bool, bool] => bool (infixr 25)