tuned headers etc.;
authorwenzelm
Wed Sep 14 22:08:08 2005 +0200 (2005-09-14)
changeset 17388495c799df31d
parent 17387 40ce48cc45f7
child 17389 b4743198b939
tuned headers etc.;
src/HOL/Commutative_Ring.thy
src/HOL/ex/Adder.thy
src/HOL/ex/CTL.thy
src/HOL/ex/Commutative_RingEx.thy
src/HOL/ex/Commutative_Ring_Complete.thy
src/HOL/ex/InductiveInvariant.thy
src/HOL/ex/InductiveInvariant_examples.thy
src/HOL/ex/Intuitionistic.thy
src/HOL/ex/Lagrange.thy
src/HOL/ex/Locales.thy
src/HOL/ex/MonoidGroup.thy
src/HOL/ex/PresburgerEx.thy
src/HOL/ex/Puzzle.thy
src/HOL/ex/Quickcheck_Examples.thy
src/HOL/ex/Reflected_Presburger.thy
src/HOL/ex/SVC_Oracle.thy
src/HOL/ex/StringEx.thy
src/HOL/ex/Tuple.thy
src/HOL/ex/svc_test.thy
     1.1 --- a/src/HOL/Commutative_Ring.thy	Wed Sep 14 22:04:38 2005 +0200
     1.2 +++ b/src/HOL/Commutative_Ring.thy	Wed Sep 14 22:08:08 2005 +0200
     1.3 @@ -1,31 +1,32 @@
     1.4 -
     1.5  (*  ID:         $Id$
     1.6      Author:     Bernhard Haeupler
     1.7  
     1.8 -  Proving equalities in a commutative Ring done "right" in Isabelle/HOL
     1.9 +Proving equalities in commutative rings done "right" in Isabelle/HOL.
    1.10  *)
    1.11  
    1.12 +header {* Proving equalities in commutative rings *}
    1.13 +
    1.14  theory Commutative_Ring
    1.15  imports List
    1.16  uses ("Tools/comm_ring.ML")
    1.17  begin
    1.18  
    1.19    (* Syntax of multivariate polynomials (pol) and polynomial expressions*)
    1.20 -datatype 'a pol = 
    1.21 -  Pc 'a 
    1.22 -  | Pinj nat "'a pol" 
    1.23 +datatype 'a pol =
    1.24 +  Pc 'a
    1.25 +  | Pinj nat "'a pol"
    1.26    | PX "'a pol" nat "'a pol"
    1.27  
    1.28 -datatype 'a polex = 
    1.29 -  Pol "'a pol" 
    1.30 -  | Add "'a polex" "'a polex" 
    1.31 -  | Sub "'a polex" "'a polex" 
    1.32 -  | Mul "'a polex" "'a polex" 
    1.33 +datatype 'a polex =
    1.34 +  Pol "'a pol"
    1.35 +  | Add "'a polex" "'a polex"
    1.36 +  | Sub "'a polex" "'a polex"
    1.37 +  | Mul "'a polex" "'a polex"
    1.38    | Pow "'a polex" nat
    1.39    | Neg "'a polex"
    1.40  
    1.41    (* Interpretation functions for the shadow syntax *)
    1.42 -consts 
    1.43 +consts
    1.44    Ipol :: "('a::{comm_ring,recpower}) list \<Rightarrow> 'a pol \<Rightarrow> 'a"
    1.45    Ipolex :: "('a::{comm_ring,recpower}) list \<Rightarrow> 'a polex \<Rightarrow> 'a"
    1.46  
    1.47 @@ -44,7 +45,7 @@
    1.48  
    1.49    (* Create polynomial normalized polynomials given normalized inputs *)
    1.50  constdefs mkPinj :: "nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol"
    1.51 -  mkPinj_def: "mkPinj x P \<equiv> (case P of   
    1.52 +  mkPinj_def: "mkPinj x P \<equiv> (case P of
    1.53    (Pc c) \<Rightarrow> (Pc c) |
    1.54    (Pinj y P) \<Rightarrow> Pinj (x+y) P |
    1.55    (PX p1 y p2) \<Rightarrow> Pinj x P )"
    1.56 @@ -71,21 +72,21 @@
    1.57    "add (Pinj i P, Pc c) = Pinj i (add (P, Pc c))"
    1.58    "add (Pc c, PX P i Q) = PX P i (add (Q, Pc c))"
    1.59    "add (PX P i Q, Pc c) = PX P i (add (Q, Pc c))"
    1.60 -  "add (Pinj x P, Pinj y Q) = 
    1.61 -  (if x=y then mkPinj x (add (P, Q)) 
    1.62 +  "add (Pinj x P, Pinj y Q) =
    1.63 +  (if x=y then mkPinj x (add (P, Q))
    1.64     else (if x>y then mkPinj y (add (Pinj (x-y) P, Q))
    1.65           else mkPinj x (add (Pinj (y-x) Q, P)) ))"
    1.66 -  "add (Pinj x P, PX Q y R) = 
    1.67 -  (if x=0 then add(P, PX Q y R) 
    1.68 -   else (if x=1 then PX Q y (add (R, P)) 
    1.69 +  "add (Pinj x P, PX Q y R) =
    1.70 +  (if x=0 then add(P, PX Q y R)
    1.71 +   else (if x=1 then PX Q y (add (R, P))
    1.72           else PX Q y (add (R, Pinj (x - 1) P))))"
    1.73 -  "add (PX P x R, Pinj y Q) = 
    1.74 -  (if y=0 then add(PX P x R, Q) 
    1.75 -   else (if y=1 then PX P x (add (R, Q)) 
    1.76 +  "add (PX P x R, Pinj y Q) =
    1.77 +  (if y=0 then add(PX P x R, Q)
    1.78 +   else (if y=1 then PX P x (add (R, Q))
    1.79           else PX P x (add (R, Pinj (y - 1) Q))))"
    1.80 -  "add (PX P1 x P2, PX Q1 y Q2) = 
    1.81 -  (if x=y then mkPX (add (P1, Q1)) x (add (P2, Q2)) 
    1.82 -  else (if x>y then mkPX (add (PX P1 (x-y) (Pc 0), Q1)) y (add (P2,Q2)) 
    1.83 +  "add (PX P1 x P2, PX Q1 y Q2) =
    1.84 +  (if x=y then mkPX (add (P1, Q1)) x (add (P2, Q2))
    1.85 +  else (if x>y then mkPX (add (PX P1 (x-y) (Pc 0), Q1)) y (add (P2,Q2))
    1.86          else mkPX (add (PX Q1 (y-x) (Pc 0), P1)) x (add (P2,Q2)) ))"
    1.87  
    1.88    (* Multiplication *)
    1.89 @@ -93,24 +94,24 @@
    1.90    "mul (Pc a, Pc b) = Pc (a*b)"
    1.91    "mul (Pc c, Pinj i P) = (if c=0 then Pc 0 else mkPinj i (mul (P, Pc c)))"
    1.92    "mul (Pinj i P, Pc c) = (if c=0 then Pc 0 else mkPinj i (mul (P, Pc c)))"
    1.93 -  "mul (Pc c, PX P i Q) = 
    1.94 +  "mul (Pc c, PX P i Q) =
    1.95    (if c=0 then Pc 0 else mkPX (mul (P, Pc c)) i (mul (Q, Pc c)))"
    1.96 -  "mul (PX P i Q, Pc c) = 
    1.97 +  "mul (PX P i Q, Pc c) =
    1.98    (if c=0 then Pc 0 else mkPX (mul (P, Pc c)) i (mul (Q, Pc c)))"
    1.99 -  "mul (Pinj x P, Pinj y Q) = 
   1.100 -  (if x=y then mkPinj x (mul (P, Q)) 
   1.101 +  "mul (Pinj x P, Pinj y Q) =
   1.102 +  (if x=y then mkPinj x (mul (P, Q))
   1.103     else (if x>y then mkPinj y (mul (Pinj (x-y) P, Q))
   1.104           else mkPinj x (mul (Pinj (y-x) Q, P)) ))"
   1.105 -  "mul (Pinj x P, PX Q y R) = 
   1.106 -  (if x=0 then mul(P, PX Q y R) 
   1.107 -   else (if x=1 then mkPX (mul (Pinj x P, Q)) y (mul (R, P)) 
   1.108 +  "mul (Pinj x P, PX Q y R) =
   1.109 +  (if x=0 then mul(P, PX Q y R)
   1.110 +   else (if x=1 then mkPX (mul (Pinj x P, Q)) y (mul (R, P))
   1.111           else mkPX (mul (Pinj x P, Q)) y (mul (R, Pinj (x - 1) P))))"
   1.112 -  "mul (PX P x R, Pinj y Q) = 
   1.113 -  (if y=0 then mul(PX P x R, Q) 
   1.114 -   else (if y=1 then mkPX (mul (Pinj y Q, P)) x (mul (R, Q)) 
   1.115 +  "mul (PX P x R, Pinj y Q) =
   1.116 +  (if y=0 then mul(PX P x R, Q)
   1.117 +   else (if y=1 then mkPX (mul (Pinj y Q, P)) x (mul (R, Q))
   1.118           else mkPX (mul (Pinj y Q, P)) x (mul (R, Pinj (y - 1) Q))))"
   1.119 -  "mul (PX P1 x P2, PX Q1 y Q2) =  
   1.120 -  add (mkPX (mul (P1, Q1)) (x+y) (mul (P2, Q2)), 
   1.121 +  "mul (PX P1 x P2, PX Q1 y Q2) =
   1.122 +  add (mkPX (mul (P1, Q1)) (x+y) (mul (P2, Q2)),
   1.123    add (mkPX (mul (P1, mkPinj 1 Q2)) x (Pc 0), mkPX (mul (Q1, mkPinj 1 P2)) y (Pc 0)) )"
   1.124  (hints simp add: mkPinj_def split: pol.split)
   1.125  
   1.126 @@ -146,16 +147,16 @@
   1.127  
   1.128  lemma number_of_nat_even: "even (number_of (w BIT bit.B0)::nat)"
   1.129  by simp
   1.130 -  
   1.131 +
   1.132  lemma pow_even : "pow (p, number_of(w BIT bit.B0)) = pow (sqr p, number_of w)"
   1.133    ( is "pow(?p,?n) = pow (_,?n2)")
   1.134  proof-
   1.135    have "even ?n" by simp
   1.136 -  hence "pow (p, ?n) = pow (sqr p, ?n div 2)" 
   1.137 +  hence "pow (p, ?n) = pow (sqr p, ?n div 2)"
   1.138      apply simp
   1.139      apply (cases "IntDef.neg (number_of w)")
   1.140      apply simp
   1.141 -    done  
   1.142 +    done
   1.143  *)
   1.144    (* Normalization of polynomial expressions *)
   1.145  
   1.146 @@ -197,7 +198,7 @@
   1.147      then obtain d where "d+y=x"..
   1.148      with prems have ?case by (auto simp add: mkPinj_ci ring_eq_simps) }
   1.149    ultimately show ?case by blast
   1.150 -next 
   1.151 +next
   1.152    case (7 x P Q y R)
   1.153    have "x=0 \<or> (x = 1) \<or> (x > 1)" by arith
   1.154    moreover
   1.155 @@ -219,7 +220,7 @@
   1.156      then obtain d where "d+1=y" ..
   1.157      with prems have ?case by auto }
   1.158    ultimately show ?case by blast
   1.159 -next 
   1.160 +next
   1.161    case (9 P1 x P2 Q1 y Q2)
   1.162    have "y < x \<or> x = y \<or> x < y" by arith
   1.163    moreover
   1.164 @@ -236,8 +237,8 @@
   1.165  qed (auto simp add: ring_eq_simps)
   1.166  
   1.167      (* Multiplication *)
   1.168 -lemma mul_ci: "ALL l. Ipol l (mul (P, Q)) = Ipol l P * Ipol l Q" 
   1.169 -  by (induct P Q rule: mul.induct, auto simp add: mkPX_ci mkPinj_ci ring_eq_simps add_ci power_add) 
   1.170 +lemma mul_ci: "ALL l. Ipol l (mul (P, Q)) = Ipol l P * Ipol l Q"
   1.171 +  by (induct P Q rule: mul.induct, auto simp add: mkPX_ci mkPinj_ci ring_eq_simps add_ci power_add)
   1.172  
   1.173    (* Substraction *)
   1.174  lemma sub_ci: "\<forall> l. Ipol l (sub p q) = (Ipol l p) - (Ipol l q)"
   1.175 @@ -254,7 +255,7 @@
   1.176  proof(induct n rule: nat_less_induct)
   1.177    case (1 k)
   1.178    have two:"2=Suc( Suc 0)" by simp
   1.179 -  from prems show ?case 
   1.180 +  from prems show ?case
   1.181    proof(cases k)
   1.182      case (Suc l)
   1.183      hence KL:"k=Suc l" by simp
   1.184 @@ -272,12 +273,12 @@
   1.185      {assume OL:"odd l"
   1.186        with prems have "\<lbrakk>\<forall>m<Suc l. \<forall>p. Ipol ls (pow (p, m)) = Ipol ls p ^ m; k = Suc l; odd l\<rbrakk> \<Longrightarrow> \<forall>p. Ipol ls (sqr p) ^ (Suc l div 2) = Ipol ls p ^ Suc l"
   1.187        proof(cases l)
   1.188 -	case (Suc w)
   1.189 -	from prems have EW:"even w" by simp
   1.190 -	from two have two_times:"(2 * (w div 2))= w" by (simp only: even_nat_div_two_times_two[OF EW])
   1.191 -	have A:"ALL p. (Ipol ls p * Ipol ls p) = (Ipol ls p) ^ (Suc (Suc 0))" by (simp add: power_Suc)
   1.192 -	from A two[symmetric] have "ALL p.(Ipol ls p * Ipol ls p) = (Ipol ls p) ^ 2" by simp
   1.193 -	with prems show ?thesis by (auto simp add: power_mult[symmetric, of _ 2 _] two_times mul_ci sqr_ci)
   1.194 +        case (Suc w)
   1.195 +        from prems have EW:"even w" by simp
   1.196 +        from two have two_times:"(2 * (w div 2))= w" by (simp only: even_nat_div_two_times_two[OF EW])
   1.197 +        have A:"ALL p. (Ipol ls p * Ipol ls p) = (Ipol ls p) ^ (Suc (Suc 0))" by (simp add: power_Suc)
   1.198 +        from A two[symmetric] have "ALL p.(Ipol ls p * Ipol ls p) = (Ipol ls p) ^ 2" by simp
   1.199 +        with prems show ?thesis by (auto simp add: power_mult[symmetric, of _ 2 _] two_times mul_ci sqr_ci)
   1.200        qed(simp)
   1.201        with prems have ?thesis by simp }
   1.202      ultimately show ?thesis by blast
   1.203 @@ -290,7 +291,7 @@
   1.204  
   1.205  (* Reflection lemma: Key to the (incomplete) decision procedure *)
   1.206  lemma norm_eq:
   1.207 -  assumes A:"norm P1  = norm P2" 
   1.208 +  assumes A:"norm P1  = norm P2"
   1.209    shows "Ipolex l P1 = Ipolex l P2"
   1.210  proof -
   1.211    from A have "Ipol l (norm P1) = Ipol l (norm P2)" by simp
   1.212 @@ -303,8 +304,7 @@
   1.213  Does not work, since no generic ring operations implementation is there
   1.214  generate_code ("ring.ML") test = "norm"*)
   1.215  
   1.216 -
   1.217 - use "Tools/comm_ring.ML"
   1.218 +use "Tools/comm_ring.ML"
   1.219  setup "CommRing.setup"
   1.220  
   1.221  end
     2.1 --- a/src/HOL/ex/Adder.thy	Wed Sep 14 22:04:38 2005 +0200
     2.2 +++ b/src/HOL/ex/Adder.thy	Wed Sep 14 22:08:08 2005 +0200
     2.3 @@ -1,11 +1,9 @@
     2.4  (*  Title:      HOL/ex/Adder.thy
     2.5      ID:         $Id$
     2.6      Author:     Sergey Tverdyshev (Universitaet des Saarlandes)
     2.7 -
     2.8 -Implementation of carry chain incrementor and adder.
     2.9  *)
    2.10  
    2.11 -header{* Adder *}
    2.12 +header {* Implementation of carry chain incrementor and adder *}
    2.13  
    2.14  theory Adder imports Main Word begin
    2.15  
     3.1 --- a/src/HOL/ex/CTL.thy	Wed Sep 14 22:04:38 2005 +0200
     3.2 +++ b/src/HOL/ex/CTL.thy	Wed Sep 14 22:08:08 2005 +0200
     3.3 @@ -1,4 +1,3 @@
     3.4 -
     3.5  (*  Title:      HOL/ex/CTL.thy
     3.6      ID:         $Id$
     3.7      Author:     Gertrud Bauer
     3.8 @@ -8,8 +7,6 @@
     3.9  
    3.10  theory CTL imports Main begin
    3.11  
    3.12 -
    3.13 -
    3.14  text {*
    3.15    We formalize basic concepts of Computational Tree Logic (CTL)
    3.16    \cite{McMillan-PhDThesis,McMillan-LectureNotes} within the
     4.1 --- a/src/HOL/ex/Commutative_RingEx.thy	Wed Sep 14 22:04:38 2005 +0200
     4.2 +++ b/src/HOL/ex/Commutative_RingEx.thy	Wed Sep 14 22:08:08 2005 +0200
     4.3 @@ -1,10 +1,13 @@
     4.4 - (* $Id$ *)
     4.5 +(*  ID:         $Id$
     4.6 +    Author:     Bernhard Haeupler
     4.7 +*)
     4.8 +
     4.9 +header {* Some examples demonstrating the comm-ring method *}
    4.10 +
    4.11  theory Commutative_RingEx
    4.12  imports Main
    4.13  begin
    4.14  
    4.15 -  (* Some examples demonstrating the comm_ring method *)
    4.16 -
    4.17  lemma "4*(x::int)^5*y^3*x^2*3 + x*z + 3^5 = 12*x^7*y^3 + z*x + 243"
    4.18  by comm_ring
    4.19  
    4.20 @@ -44,4 +47,4 @@
    4.21  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 )"
    4.22  by comm_ring
    4.23  
    4.24 -end
    4.25 \ No newline at end of file
    4.26 +end
     5.1 --- a/src/HOL/ex/Commutative_Ring_Complete.thy	Wed Sep 14 22:04:38 2005 +0200
     5.2 +++ b/src/HOL/ex/Commutative_Ring_Complete.thy	Wed Sep 14 22:08:08 2005 +0200
     5.3 @@ -1,9 +1,12 @@
     5.4  (*  ID:         $Id$
     5.5      Author:     Bernhard Haeupler
     5.6  
     5.7 -  This theory is about the relative completeness of the tactic 
     5.8 -  As long as the reified atomic polynomials of type 'a pol 
     5.9 -  are in normal form, the cring method is complete *)	
    5.10 +This theory is about of the relative completeness of method comm-ring
    5.11 +method.  As long as the reified atomic polynomials of type 'a pol are
    5.12 +in normal form, the cring method is complete.
    5.13 +*)
    5.14 +
    5.15 +header {* Proof of the relative completeness of method comm-ring *}
    5.16  
    5.17  theory Commutative_Ring_Complete
    5.18  imports Main
    5.19 @@ -381,4 +384,4 @@
    5.20    qed(simp)
    5.21  qed
    5.22  
    5.23 -end
    5.24 \ No newline at end of file
    5.25 +end
     6.1 --- a/src/HOL/ex/InductiveInvariant.thy	Wed Sep 14 22:04:38 2005 +0200
     6.2 +++ b/src/HOL/ex/InductiveInvariant.thy	Wed Sep 14 22:08:08 2005 +0200
     6.3 @@ -1,12 +1,15 @@
     6.4 +(*  ID:         $Id$
     6.5 +    Author:	Sava Krsti\'{c} and John Matthews
     6.6 +*)
     6.7 +
     6.8 +header {* Some of the results in Inductive Invariants for Nested Recursion *}
     6.9 +
    6.10  theory InductiveInvariant imports Main begin
    6.11  
    6.12 -(** Authors: Sava Krsti\'{c} and John Matthews **)
    6.13 -(**    Date: Sep 12, 2003                      **)
    6.14 -
    6.15 -text {* A formalization of some of the results in
    6.16 -        \emph{Inductive Invariants for Nested Recursion},
    6.17 -        by Sava Krsti\'{c} and John Matthews.
    6.18 -        Appears in the proceedings of TPHOLs 2003, LNCS vol. 2758, pp. 253-269. *}
    6.19 +text {* A formalization of some of the results in \emph{Inductive
    6.20 +  Invariants for Nested Recursion}, by Sava Krsti\'{c} and John
    6.21 +  Matthews.  Appears in the proceedings of TPHOLs 2003, LNCS
    6.22 +  vol. 2758, pp. 253-269. *}
    6.23  
    6.24  
    6.25  text "S is an inductive invariant of the functional F with respect to the wellfounded relation r."
    6.26 @@ -86,4 +89,4 @@
    6.27   ==> S x (f x)"
    6.28  by (simp add: indinv_on_wfrec)
    6.29  
    6.30 -end
    6.31 \ No newline at end of file
    6.32 +end
     7.1 --- a/src/HOL/ex/InductiveInvariant_examples.thy	Wed Sep 14 22:04:38 2005 +0200
     7.2 +++ b/src/HOL/ex/InductiveInvariant_examples.thy	Wed Sep 14 22:08:08 2005 +0200
     7.3 @@ -1,7 +1,10 @@
     7.4 -theory InductiveInvariant_examples imports InductiveInvariant  begin
     7.5 +(*  ID:         $Id$
     7.6 +    Author:	Sava Krsti\'{c} and John Matthews
     7.7 +*)
     7.8  
     7.9 -(** Authors: Sava Krsti\'{c} and John Matthews **)
    7.10 -(**    Date: Oct 17, 2003                      **)
    7.11 +header {* Example use if an inductive invariant to solve termination conditions *}
    7.12 +
    7.13 +theory InductiveInvariant_examples imports InductiveInvariant  begin
    7.14  
    7.15  text "A simple example showing how to use an inductive invariant
    7.16        to solve termination conditions generated by recdef on
    7.17 @@ -124,4 +127,4 @@
    7.18  by (subst ninety_one.simps,
    7.19      simp add: ninety_one_tc measure_def inv_image_def)
    7.20  
    7.21 -end
    7.22 \ No newline at end of file
    7.23 +end
     8.1 --- a/src/HOL/ex/Intuitionistic.thy	Wed Sep 14 22:04:38 2005 +0200
     8.2 +++ b/src/HOL/ex/Intuitionistic.thy	Wed Sep 14 22:08:08 2005 +0200
     8.3 @@ -3,11 +3,11 @@
     8.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.5      Copyright   1991  University of Cambridge
     8.6  
     8.7 -Higher-Order Logic: Intuitionistic predicate calculus problems
     8.8 -
     8.9  Taken from FOL/ex/int.ML
    8.10  *)
    8.11  
    8.12 +header {* Higher-Order Logic: Intuitionistic predicate calculus problems *}
    8.13 +
    8.14  theory Intuitionistic imports Main begin
    8.15  
    8.16  
     9.1 --- a/src/HOL/ex/Lagrange.thy	Wed Sep 14 22:04:38 2005 +0200
     9.2 +++ b/src/HOL/ex/Lagrange.thy	Wed Sep 14 22:08:08 2005 +0200
     9.3 @@ -2,28 +2,31 @@
     9.4      ID:         $Id$
     9.5      Author:     Tobias Nipkow
     9.6      Copyright   1996 TU Muenchen
     9.7 -
     9.8 -
     9.9 -This theory only contains a single theorem, which is a lemma in Lagrange's
    9.10 -proof that every natural number is the sum of 4 squares.  Its sole purpose is
    9.11 -to demonstrate ordered rewriting for commutative rings.
    9.12 -
    9.13 -The enterprising reader might consider proving all of Lagrange's theorem.
    9.14  *)
    9.15  
    9.16 +header {* A lemma for Lagrange's theorem *}
    9.17 +
    9.18  theory Lagrange imports Main begin
    9.19  
    9.20 +text {* This theory only contains a single theorem, which is a lemma
    9.21 +in Lagrange's proof that every natural number is the sum of 4 squares.
    9.22 +Its sole purpose is to demonstrate ordered rewriting for commutative
    9.23 +rings.
    9.24 +
    9.25 +The enterprising reader might consider proving all of Lagrange's
    9.26 +theorem.  *}
    9.27 +
    9.28  constdefs sq :: "'a::times => 'a"
    9.29           "sq x == x*x"
    9.30  
    9.31 -(* The following lemma essentially shows that every natural number is the sum
    9.32 -of four squares, provided all prime numbers are.  However, this is an
    9.33 -abstract theorem about commutative rings.  It has, a priori, nothing to do
    9.34 -with nat.*)
    9.35 +text {* The following lemma essentially shows that every natural
    9.36 +number is the sum of four squares, provided all prime numbers are.
    9.37 +However, this is an abstract theorem about commutative rings.  It has,
    9.38 +a priori, nothing to do with nat. *}
    9.39  
    9.40  ML"Delsimprocs[ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]"
    9.41  
    9.42 -(*once a slow step, but now (2001) just three seconds!*)
    9.43 +-- {* once a slow step, but now (2001) just three seconds! *}
    9.44  lemma Lagrange_lemma:
    9.45   "!!x1::'a::comm_ring.
    9.46    (sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
    9.47 @@ -36,7 +39,6 @@
    9.48  
    9.49  text{*A challenge by John Harrison. Takes about 74s on a 2.5GHz Apple G5.*}
    9.50  
    9.51 -(*
    9.52  lemma "!!p1::'a::comm_ring.
    9.53   (sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) * 
    9.54   (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2) 
    9.55 @@ -48,6 +50,8 @@
    9.56      sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +
    9.57      sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +
    9.58      sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)"
    9.59 +oops
    9.60 +(*
    9.61  by(simp add: sq_def ring_eq_simps)
    9.62  *)
    9.63  
    10.1 --- a/src/HOL/ex/Locales.thy	Wed Sep 14 22:04:38 2005 +0200
    10.2 +++ b/src/HOL/ex/Locales.thy	Wed Sep 14 22:08:08 2005 +0200
    10.3 @@ -3,7 +3,7 @@
    10.4      Author:     Markus Wenzel, LMU München
    10.5  *)
    10.6  
    10.7 -header {* Using locales in Isabelle/Isar *}
    10.8 +header {* Using locales in Isabelle/Isar -- outdated version! *}
    10.9  
   10.10  theory Locales imports Main begin
   10.11  
    11.1 --- a/src/HOL/ex/MonoidGroup.thy	Wed Sep 14 22:04:38 2005 +0200
    11.2 +++ b/src/HOL/ex/MonoidGroup.thy	Wed Sep 14 22:08:08 2005 +0200
    11.3 @@ -1,11 +1,9 @@
    11.4  (*  Title:      HOL/ex/MonoidGroup.thy
    11.5      ID:         $Id$
    11.6      Author:     Markus Wenzel
    11.7 -
    11.8 -Monoids and Groups as predicates over record schemes.
    11.9  *)
   11.10  
   11.11 -header {* Monoids and Groups *}
   11.12 +header {* Monoids and Groups as predicates over record schemes *}
   11.13  
   11.14  theory MonoidGroup imports Main begin
   11.15  
    12.1 --- a/src/HOL/ex/PresburgerEx.thy	Wed Sep 14 22:04:38 2005 +0200
    12.2 +++ b/src/HOL/ex/PresburgerEx.thy	Wed Sep 14 22:08:08 2005 +0200
    12.3 @@ -1,9 +1,9 @@
    12.4  (*  Title:      HOL/ex/PresburgerEx.thy
    12.5      ID:         $Id$
    12.6      Author:     Amine Chaieb, TU Muenchen
    12.7 +*)
    12.8  
    12.9 -Some examples for Presburger Arithmetic
   12.10 -*)
   12.11 +header {* Some examples for Presburger Arithmetic *}
   12.12  
   12.13  theory PresburgerEx imports Main begin
   12.14  
    13.1 --- a/src/HOL/ex/Puzzle.thy	Wed Sep 14 22:04:38 2005 +0200
    13.2 +++ b/src/HOL/ex/Puzzle.thy	Wed Sep 14 22:08:08 2005 +0200
    13.3 @@ -8,6 +8,8 @@
    13.4  Proof due to Herbert Ehler
    13.5  *)
    13.6  
    13.7 +header {* A question from ``Bundeswettbewerb Mathematik'' *}
    13.8 +
    13.9  theory Puzzle imports Main begin
   13.10  
   13.11  consts f :: "nat => nat"
    14.1 --- a/src/HOL/ex/Quickcheck_Examples.thy	Wed Sep 14 22:04:38 2005 +0200
    14.2 +++ b/src/HOL/ex/Quickcheck_Examples.thy	Wed Sep 14 22:08:08 2005 +0200
    14.3 @@ -144,5 +144,3 @@
    14.4    oops
    14.5  
    14.6  end
    14.7 -
    14.8 -
    15.1 --- a/src/HOL/ex/Reflected_Presburger.thy	Wed Sep 14 22:04:38 2005 +0200
    15.2 +++ b/src/HOL/ex/Reflected_Presburger.thy	Wed Sep 14 22:08:08 2005 +0200
    15.3 @@ -1,10 +1,15 @@
    15.4 -(* A formalization of quantifier elimination for Presburger arithmetic*)
    15.5 -(* based on a generic quantifier elimination algorithm and 
    15.6 -   cooper's methos to eliminate on \<exists> *)
    15.7 +(*  Title:      HOL/ex/PresburgerEx.thy
    15.8 +    ID:         $Id$
    15.9 +    Author:     Amine Chaieb, TU Muenchen
   15.10 +
   15.11 +A formalization of quantifier elimination for Presburger arithmetic
   15.12 +based on a generic quantifier elimination algorithm and Cooper's
   15.13 +methos to eliminate on \<exists>. *)
   15.14 +
   15.15 +header {* Quantifier elimination for Presburger arithmetic *}
   15.16  
   15.17  theory Reflected_Presburger
   15.18  imports Main
   15.19 -(* uses ("rcooper.ML") ("rpresbtac.ML") *)
   15.20  begin
   15.21  
   15.22  (* Shadow syntax for integer terms *)
   15.23 @@ -2051,7 +2056,6 @@
   15.24    and dvd: "i dvd l"
   15.25    shows "(i*x + r = 0) = (l*x + ((l div i)*r) = 0)"
   15.26  proof-
   15.27 -  thm dvd_div_pos[OF lpos inz dvd]
   15.28    have ldvdii: "(l div i)*i = l" by (rule dvd_div_pos[OF lpos inz dvd])
   15.29    have ldivinz: "l div i \<noteq> 0" using inz ldvdii lpos by auto
   15.30    have "(i*x + r = 0) = ((l div i)*(i*x + r) = (l div i)*0)"
   15.31 @@ -2224,7 +2228,6 @@
   15.32  	    assume nz: "n=0"
   15.33  	    from prems have inz: "i \<noteq> 0" by auto
   15.34  	    from prems nz have idvdl: "i dvd l" by simp
   15.35 -	    thm adjustcoeff_eq_corr[OF lpos inz idvdl]
   15.36  	    have "(i * a + (i' * (a # ats) ! n' + I_intterm (a # ats) r) = 0) =
   15.37  	      (l * a + l div i * (i' * (a # ats) ! n' + I_intterm (a # ats) r) = 0)"
   15.38  	      by (rule adjustcoeff_eq_corr[OF lpos inz idvdl])
   15.39 @@ -2700,7 +2703,6 @@
   15.40    assumes 
   15.41    linp: "islinform p"
   15.42    shows "alldivide (divlcm p,p)"
   15.43 -thm nz_le[OF divlcm_pos[OF linp]]
   15.44    using linp divlcm_pos
   15.45  proof (induct p rule: divlcm.induct,simp_all add: zdvd_refl_abs,clarsimp simp add: Nat.gr0_conv_Suc)
   15.46    case (goal1 f)
   15.47 @@ -5722,4 +5724,5 @@
   15.48  use "rpresbtac.ML"
   15.49  setup RPresburger.setup
   15.50  *)
   15.51 +
   15.52  end
    16.1 --- a/src/HOL/ex/SVC_Oracle.thy	Wed Sep 14 22:04:38 2005 +0200
    16.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Wed Sep 14 22:08:08 2005 +0200
    16.3 @@ -3,10 +3,10 @@
    16.4      Author:     Lawrence C Paulson
    16.5      Copyright   1999  University of Cambridge
    16.6  
    16.7 -Installing the oracle for SVC (Stanford Validity Checker)
    16.8 +Based upon the work of Søren T. Heilmann.
    16.9 +*)
   16.10  
   16.11 -Based upon the work of Søren T. Heilmann
   16.12 -*)
   16.13 +header {* Installing an oracle for SVC (Stanford Validity Checker) *}
   16.14  
   16.15  theory SVC_Oracle
   16.16  imports Main
    17.1 --- a/src/HOL/ex/StringEx.thy	Wed Sep 14 22:04:38 2005 +0200
    17.2 +++ b/src/HOL/ex/StringEx.thy	Wed Sep 14 22:08:08 2005 +0200
    17.3 @@ -1,3 +1,4 @@
    17.4 +(* $Id$ *)
    17.5  
    17.6  header {* String examples *}
    17.7  
    18.1 --- a/src/HOL/ex/Tuple.thy	Wed Sep 14 22:04:38 2005 +0200
    18.2 +++ b/src/HOL/ex/Tuple.thy	Wed Sep 14 22:08:08 2005 +0200
    18.3 @@ -1,11 +1,6 @@
    18.4  (*  Title:      HOL/ex/Tuple.thy
    18.5      ID:         $Id$
    18.6      Author:     Markus Wenzel, TU Muenchen
    18.7 -
    18.8 -Properly nested products (see also theory Prod).
    18.9 -
   18.10 -Unquestionably, this should be used as the standard representation of
   18.11 -tuples in HOL, but it breaks many existing theories!
   18.12  *)
   18.13  
   18.14  header {* Properly nested products *}
    19.1 --- a/src/HOL/ex/svc_test.thy	Wed Sep 14 22:04:38 2005 +0200
    19.2 +++ b/src/HOL/ex/svc_test.thy	Wed Sep 14 22:08:08 2005 +0200
    19.3 @@ -1,5 +1,11 @@
    19.4  
    19.5 -svc_test = SVC_Oracle +
    19.6 +(* $Id$ *)
    19.7 +
    19.8 +header {* Demonstrating the interface SVC *}
    19.9 +
   19.10 +theory svc_test
   19.11 +imports SVC_Oracle
   19.12 +begin
   19.13  
   19.14  syntax
   19.15      "<->"         :: [bool, bool] => bool                  (infixr 25)