tuned document;
authorwenzelm
Sun Jun 03 23:16:47 2007 +0200 (2007-06-03)
changeset 2321987ad6e8a5f2c
parent 23218 01c4d19f597e
child 23220 9e04da929160
tuned document;
src/HOL/ex/CTL.thy
src/HOL/ex/LocaleTest2.thy
src/HOL/ex/Refute_Examples.thy
src/HOL/ex/Sudoku.thy
src/HOL/ex/ThreeDivides.thy
src/HOL/ex/Unification.thy
     1.1 --- a/src/HOL/ex/CTL.thy	Sun Jun 03 23:16:46 2007 +0200
     1.2 +++ b/src/HOL/ex/CTL.thy	Sun Jun 03 23:16:47 2007 +0200
     1.3 @@ -80,7 +80,7 @@
     1.4  lemmas [simp] = EX_def EG_def AX_def EF_def AF_def AG_def
     1.5  
     1.6  
     1.7 -section {* Basic fixed point properties *}
     1.8 +subsection {* Basic fixed point properties *}
     1.9  
    1.10  text {*
    1.11    First of all, we use the de-Morgan property of fixed points
    1.12 @@ -187,7 +187,7 @@
    1.13    by (simp only: AG_gfp) (rule gfp_upperbound)
    1.14  
    1.15  
    1.16 -section {* The tree induction principle \label{sec:calc-ctl-tree-induct} *}
    1.17 +subsection {* The tree induction principle \label{sec:calc-ctl-tree-induct} *}
    1.18  
    1.19  text {*
    1.20    With the most basic facts available, we are now able to establish a
    1.21 @@ -283,7 +283,7 @@
    1.22  qed
    1.23  
    1.24  
    1.25 -section {* An application of tree induction \label{sec:calc-ctl-commute} *}
    1.26 +subsection {* An application of tree induction \label{sec:calc-ctl-commute} *}
    1.27  
    1.28  text {*
    1.29    Further interesting properties of CTL expressions may be
     2.1 --- a/src/HOL/ex/LocaleTest2.thy	Sun Jun 03 23:16:46 2007 +0200
     2.2 +++ b/src/HOL/ex/LocaleTest2.thy	Sun Jun 03 23:16:47 2007 +0200
     2.3 @@ -19,7 +19,8 @@
     2.4  ML {* set show_hyps *}
     2.5  ML {* set show_sorts *}
     2.6  
     2.7 -section {* Interpretation of Defined Concepts *}
     2.8 +
     2.9 +subsection {* Interpretation of Defined Concepts *}
    2.10  
    2.11  text {* Naming convention for global objects: prefixes D and d *}
    2.12  
     3.1 --- a/src/HOL/ex/Refute_Examples.thy	Sun Jun 03 23:16:46 2007 +0200
     3.2 +++ b/src/HOL/ex/Refute_Examples.thy	Sun Jun 03 23:16:47 2007 +0200
     3.3 @@ -9,7 +9,6 @@
     3.4  header {* Examples for the 'refute' command *}
     3.5  
     3.6  theory Refute_Examples imports Main
     3.7 -
     3.8  begin
     3.9  
    3.10  refute_params [satsolver="dpll"]
    3.11 @@ -26,9 +25,9 @@
    3.12  
    3.13  (******************************************************************************)
    3.14  
    3.15 -section {* Examples and Test Cases *}
    3.16 +subsection {* Examples and Test Cases *}
    3.17  
    3.18 -subsection {* Propositional logic *}
    3.19 +subsubsection {* Propositional logic *}
    3.20  
    3.21  lemma "True"
    3.22    refute
    3.23 @@ -69,7 +68,7 @@
    3.24  
    3.25  (******************************************************************************)
    3.26  
    3.27 -subsection {* Predicate logic *}
    3.28 +subsubsection {* Predicate logic *}
    3.29  
    3.30  lemma "P x y z"
    3.31    refute
    3.32 @@ -85,7 +84,7 @@
    3.33  
    3.34  (******************************************************************************)
    3.35  
    3.36 -subsection {* Equality *}
    3.37 +subsubsection {* Equality *}
    3.38  
    3.39  lemma "P = True"
    3.40    refute
    3.41 @@ -119,7 +118,7 @@
    3.42  
    3.43  (******************************************************************************)
    3.44  
    3.45 -subsection {* First-Order Logic *}
    3.46 +subsubsection {* First-Order Logic *}
    3.47  
    3.48  lemma "\<exists>x. P x"
    3.49    refute
    3.50 @@ -213,7 +212,7 @@
    3.51  
    3.52  (******************************************************************************)
    3.53  
    3.54 -subsection {* Higher-Order Logic *}
    3.55 +subsubsection {* Higher-Order Logic *}
    3.56  
    3.57  lemma "\<exists>P. P"
    3.58    refute
    3.59 @@ -314,7 +313,7 @@
    3.60  
    3.61  (******************************************************************************)
    3.62  
    3.63 -subsection {* Meta-logic *}
    3.64 +subsubsection {* Meta-logic *}
    3.65  
    3.66  lemma "!!x. P x"
    3.67    refute
    3.68 @@ -346,7 +345,7 @@
    3.69  
    3.70  (******************************************************************************)
    3.71  
    3.72 -subsection {* Schematic variables *}
    3.73 +subsubsection {* Schematic variables *}
    3.74  
    3.75  lemma "?P"
    3.76    refute
    3.77 @@ -360,7 +359,7 @@
    3.78  
    3.79  (******************************************************************************)
    3.80  
    3.81 -subsection {* Abstractions *}
    3.82 +subsubsection {* Abstractions *}
    3.83  
    3.84  lemma "(\<lambda>x. x) = (\<lambda>x. y)"
    3.85    refute
    3.86 @@ -377,7 +376,7 @@
    3.87  
    3.88  (******************************************************************************)
    3.89  
    3.90 -subsection {* Sets *}
    3.91 +subsubsection {* Sets *}
    3.92  
    3.93  lemma "P (A::'a set)"
    3.94    refute
    3.95 @@ -422,7 +421,7 @@
    3.96  
    3.97  (******************************************************************************)
    3.98  
    3.99 -subsection {* arbitrary *}
   3.100 +subsubsection {* arbitrary *}
   3.101  
   3.102  lemma "arbitrary"
   3.103    refute
   3.104 @@ -442,7 +441,7 @@
   3.105  
   3.106  (******************************************************************************)
   3.107  
   3.108 -subsection {* The *}
   3.109 +subsubsection {* The *}
   3.110  
   3.111  lemma "The P"
   3.112    refute
   3.113 @@ -466,7 +465,7 @@
   3.114  
   3.115  (******************************************************************************)
   3.116  
   3.117 -subsection {* Eps *}
   3.118 +subsubsection {* Eps *}
   3.119  
   3.120  lemma "Eps P"
   3.121    refute
   3.122 @@ -491,7 +490,7 @@
   3.123  
   3.124  (******************************************************************************)
   3.125  
   3.126 -subsection {* Subtypes (typedef), typedecl *}
   3.127 +subsubsection {* Subtypes (typedef), typedecl *}
   3.128  
   3.129  text {* A completely unspecified non-empty subset of @{typ "'a"}: *}
   3.130  
   3.131 @@ -513,7 +512,7 @@
   3.132  
   3.133  (******************************************************************************)
   3.134  
   3.135 -subsection {* Inductive datatypes *}
   3.136 +subsubsection {* Inductive datatypes *}
   3.137  
   3.138  text {* With @{text quick_and_dirty} set, the datatype package does
   3.139    not generate certain axioms for recursion operators.  Without these
   3.140 @@ -521,7 +520,7 @@
   3.141  
   3.142  ML {* reset quick_and_dirty *}
   3.143  
   3.144 -subsubsection {* unit *}
   3.145 +text {* unit *}
   3.146  
   3.147  lemma "P (x::unit)"
   3.148    refute
   3.149 @@ -543,7 +542,7 @@
   3.150    refute
   3.151  oops
   3.152  
   3.153 -subsubsection {* option *}
   3.154 +text {* option *}
   3.155  
   3.156  lemma "P (x::'a option)"
   3.157    refute
   3.158 @@ -569,7 +568,7 @@
   3.159    refute
   3.160  oops
   3.161  
   3.162 -subsubsection {* * *}
   3.163 +text {* * *}
   3.164  
   3.165  lemma "P (x::'a*'b)"
   3.166    refute
   3.167 @@ -603,7 +602,7 @@
   3.168    refute
   3.169  oops
   3.170  
   3.171 -subsubsection {* + *}
   3.172 +text {* + *}
   3.173  
   3.174  lemma "P (x::'a+'b)"
   3.175    refute
   3.176 @@ -633,7 +632,7 @@
   3.177    refute
   3.178  oops
   3.179  
   3.180 -subsubsection {* Non-recursive datatypes *}
   3.181 +text {* Non-recursive datatypes *}
   3.182  
   3.183  datatype T1 = A | B
   3.184  
   3.185 @@ -701,7 +700,7 @@
   3.186    refute
   3.187  oops
   3.188  
   3.189 -subsubsection {* Recursive datatypes *}
   3.190 +text {* Recursive datatypes *}
   3.191  
   3.192  text {* nat *}
   3.193  
   3.194 @@ -783,7 +782,7 @@
   3.195    refute
   3.196  oops
   3.197  
   3.198 -subsubsection {* Mutually recursive datatypes *}
   3.199 +text {* Mutually recursive datatypes *}
   3.200  
   3.201  datatype 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp"
   3.202       and 'a bexp = Equal "'a aexp" "'a aexp"
   3.203 @@ -824,7 +823,7 @@
   3.204    refute
   3.205  oops
   3.206  
   3.207 -subsubsection {* Other datatype examples *}
   3.208 +text {* Other datatype examples *}
   3.209  
   3.210  datatype Trie = TR "Trie list"
   3.211  
   3.212 @@ -915,7 +914,7 @@
   3.213  
   3.214  (******************************************************************************)
   3.215  
   3.216 -subsection {* Records *}
   3.217 +subsubsection {* Records *}
   3.218  
   3.219  (*TODO: make use of pair types, rather than typedef, for record types*)
   3.220  
   3.221 @@ -936,7 +935,7 @@
   3.222  
   3.223  (******************************************************************************)
   3.224  
   3.225 -subsection {* Inductively defined sets *}
   3.226 +subsubsection {* Inductively defined sets *}
   3.227  
   3.228  consts
   3.229    arbitrarySet :: "'a set"
   3.230 @@ -974,7 +973,7 @@
   3.231  
   3.232  (******************************************************************************)
   3.233  
   3.234 -subsection {* Examples involving special functions *}
   3.235 +subsubsection {* Examples involving special functions *}
   3.236  
   3.237  lemma "card x = 0"
   3.238    refute
   3.239 @@ -1026,7 +1025,7 @@
   3.240  
   3.241  (******************************************************************************)
   3.242  
   3.243 -subsection {* Axiomatic type classes and overloading *}
   3.244 +subsubsection {* Axiomatic type classes and overloading *}
   3.245  
   3.246  text {* A type class without axioms: *}
   3.247  
     4.1 --- a/src/HOL/ex/Sudoku.thy	Sun Jun 03 23:16:46 2007 +0200
     4.2 +++ b/src/HOL/ex/Sudoku.thy	Sun Jun 03 23:16:47 2007 +0200
     4.3 @@ -7,9 +7,7 @@
     4.4  header {* A SAT-based Sudoku Solver *}
     4.5  
     4.6  theory Sudoku
     4.7 -
     4.8  imports Main
     4.9 -
    4.10  begin
    4.11  
    4.12  text {*
     5.1 --- a/src/HOL/ex/ThreeDivides.thy	Sun Jun 03 23:16:46 2007 +0200
     5.2 +++ b/src/HOL/ex/ThreeDivides.thy	Sun Jun 03 23:16:47 2007 +0200
     5.3 @@ -9,7 +9,7 @@
     5.4  imports Main LaTeXsugar
     5.5  begin
     5.6  
     5.7 -section {* Abstract *}
     5.8 +subsection {* Abstract *}
     5.9  
    5.10  text {*
    5.11  The following document presents a proof of the Three Divides N theorem
    5.12 @@ -27,9 +27,10 @@
    5.13  @{text "\<box>"}
    5.14  *}
    5.15  
    5.16 -section {* Formal proof *}
    5.17  
    5.18 -subsection {* Miscellaneous summation lemmas *}
    5.19 +subsection {* Formal proof *}
    5.20 +
    5.21 +subsubsection {* Miscellaneous summation lemmas *}
    5.22  
    5.23  text {* If $a$ divides @{text "A x"} for all x then $a$ divides any
    5.24  sum over terms of the form @{text "(A x)*(P x)"} for arbitrary $P$. *}
    5.25 @@ -48,7 +49,8 @@
    5.26    thus ?case by simp
    5.27  qed
    5.28  
    5.29 -subsection {* Generalised Three Divides *}
    5.30 +
    5.31 +subsubsection {* Generalised Three Divides *}
    5.32  
    5.33  text {* This section solves a generalised form of the three divides
    5.34  problem. Here we show that for any sequence of numbers the theorem
    5.35 @@ -131,14 +133,15 @@
    5.36  qed
    5.37  
    5.38  
    5.39 -subsection {* Three Divides Natural *}
    5.40 +subsubsection {* Three Divides Natural *}
    5.41  
    5.42  text {* This section shows that for all natural numbers we can
    5.43  generate a sequence of digits less than ten that represent the decimal
    5.44  expansion of the number. We then use the lemma @{text
    5.45  "three_div_general"} to prove our final theorem. *}
    5.46  
    5.47 -subsubsection {* Definitions of length and digit sum *}
    5.48 +
    5.49 +text {* \medskip Definitions of length and digit sum. *}
    5.50  
    5.51  text {* This section introduces some functions to calculate the
    5.52  required properties of natural numbers. We then proceed to prove some
    5.53 @@ -215,7 +218,7 @@
    5.54  qed
    5.55  
    5.56  
    5.57 -subsubsection {* Final theorem *}
    5.58 +text {* \medskip Final theorem. *}
    5.59  
    5.60  text {* We now combine the general theorem @{text "three_div_general"}
    5.61  and existence result of @{text "exp_exists"} to prove our final
    5.62 @@ -234,5 +237,4 @@
    5.63    show "3 dvd n = (3 dvd (\<Sum>x<nlen n. n div 10^x mod 10))" by simp
    5.64  qed
    5.65  
    5.66 -
    5.67  end
     6.1 --- a/src/HOL/ex/Unification.thy	Sun Jun 03 23:16:46 2007 +0200
     6.2 +++ b/src/HOL/ex/Unification.thy	Sun Jun 03 23:16:47 2007 +0200
     6.3 @@ -4,9 +4,9 @@
     6.4  
     6.5  header {* Case study: Unification Algorithm *}
     6.6  
     6.7 -(*<*)theory Unification
     6.8 +theory Unification
     6.9  imports Main
    6.10 -begin(*>*)
    6.11 +begin
    6.12  
    6.13  text {* 
    6.14    This is a formalization of a first-order unification
    6.15 @@ -15,7 +15,7 @@
    6.16  
    6.17    This is basically a modernized version of a previous formalization
    6.18    by Konrad Slind (see: HOL/Subst/Unify.thy), which itself builds on
    6.19 -  previous work by Paulson and Manna @{text "&"} Waldinger (for details, see
    6.20 +  previous work by Paulson and Manna \& Waldinger (for details, see
    6.21    there).
    6.22  
    6.23    Unlike that formalization, where the proofs of termination and
    6.24 @@ -23,6 +23,7 @@
    6.25    partial correctness and termination separately.
    6.26  *}
    6.27  
    6.28 +
    6.29  subsection {* Basic definitions *}
    6.30  
    6.31  datatype 'a trm = 
    6.32 @@ -62,6 +63,7 @@
    6.33  where
    6.34    "s1 =\<^sub>s s2 \<equiv> \<forall>t. t \<triangleleft> s1 = t \<triangleleft> s2" 
    6.35  
    6.36 +
    6.37  subsection {* Basic lemmas *}
    6.38  
    6.39  lemma apply_empty[simp]: "t \<triangleleft> [] = t"
    6.40 @@ -105,6 +107,7 @@
    6.41  lemma compose_assoc: "(a \<bullet> b) \<bullet> c =\<^sub>s a \<bullet> (b \<bullet> c)"
    6.42    by auto
    6.43  
    6.44 +
    6.45  subsection {* Specification: Most general unifiers *}
    6.46  
    6.47  definition
    6.48 @@ -492,7 +495,6 @@
    6.49  
    6.50  subsection {* Termination proof *}
    6.51  
    6.52 -
    6.53  termination unify
    6.54  proof 
    6.55    let ?R = "measures [\<lambda>(M,N). card (vars_of M \<union> vars_of N),
    6.56 @@ -532,23 +534,4 @@
    6.57    qed
    6.58  qed
    6.59  
    6.60 -
    6.61 -(*<*)end(*>*)
    6.62 -
    6.63 -
    6.64 -
    6.65 -
    6.66 -
    6.67 -
    6.68 -
    6.69 -
    6.70 -
    6.71 -
    6.72 -
    6.73 -
    6.74 -
    6.75 -
    6.76 -
    6.77 -
    6.78 -
    6.79 -
    6.80 +end