improved presentation;
authorwenzelm
Wed Oct 06 18:50:51 1999 +0200 (1999-10-06)
changeset 77617fab9592384f
parent 7760 43f8d28dbc6e
child 7762 c98d70538033
improved presentation;
src/HOL/Isar_examples/BasicLogic.thy
src/HOL/Isar_examples/ExprCompiler.thy
src/HOL/Isar_examples/Group.thy
src/HOL/Isar_examples/KnasterTarski.thy
src/HOL/Isar_examples/MultisetOrder.thy
src/HOL/Isar_examples/MutilatedCheckerboard.thy
src/HOL/Isar_examples/Summation.thy
src/HOL/Isar_examples/W_correct.thy
src/HOL/Isar_examples/document/style.tex
     1.1 --- a/src/HOL/Isar_examples/BasicLogic.thy	Wed Oct 06 18:50:40 1999 +0200
     1.2 +++ b/src/HOL/Isar_examples/BasicLogic.thy	Wed Oct 06 18:50:51 1999 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4  
     1.5  theory BasicLogic = Main:;
     1.6  
     1.7 +
     1.8  subsection {* Some trivialities *};
     1.9  
    1.10  text {* Just a few toy examples to get an idea of how Isabelle/Isar
    1.11 @@ -62,7 +63,8 @@
    1.12    qed;
    1.13  qed;
    1.14  
    1.15 -text {* Variations of backward vs.\ forward reasoning \dots *};
    1.16 +
    1.17 +subsection {* Variations of backward vs.\ forward reasoning \dots *};
    1.18  
    1.19  lemma "A & B --> B & A";
    1.20  proof;
     2.1 --- a/src/HOL/Isar_examples/ExprCompiler.thy	Wed Oct 06 18:50:40 1999 +0200
     2.2 +++ b/src/HOL/Isar_examples/ExprCompiler.thy	Wed Oct 06 18:50:51 1999 +0200
     2.3 @@ -37,7 +37,8 @@
     2.4  *};
     2.5  
     2.6  consts
     2.7 -  exec :: "(('adr, 'val) instr) list => 'val list => ('adr => 'val) => 'val list";
     2.8 +  exec :: "(('adr, 'val) instr) list
     2.9 +    => 'val list => ('adr => 'val) => 'val list";
    2.10  
    2.11  primrec
    2.12    "exec [] stack env = stack"
    2.13 @@ -45,7 +46,8 @@
    2.14      (case instr of
    2.15        Const c => exec instrs (c # stack) env
    2.16      | Load x => exec instrs (env x # stack) env
    2.17 -    | Apply f => exec instrs (f (hd stack) (hd (tl stack)) # (tl (tl stack))) env)";
    2.18 +    | Apply f => exec instrs (f (hd stack) (hd (tl stack))
    2.19 +                   # (tl (tl stack))) env)";
    2.20  
    2.21  constdefs
    2.22    execute :: "(('adr, 'val) instr) list => ('adr => 'val) => 'val"
    2.23 @@ -55,8 +57,8 @@
    2.24  subsection {* Expressions *};
    2.25  
    2.26  text {*
    2.27 - We introduce a simple language of expressions: variables ---
    2.28 - constants --- binary operations.
    2.29 + We introduce a simple language of expressions: variables, constants,
    2.30 + binary operations.
    2.31  *};
    2.32  
    2.33  datatype ('adr, 'val) expr =
     3.1 --- a/src/HOL/Isar_examples/Group.thy	Wed Oct 06 18:50:40 1999 +0200
     3.2 +++ b/src/HOL/Isar_examples/Group.thy	Wed Oct 06 18:50:51 1999 +0200
     3.3 @@ -71,11 +71,11 @@
     3.4  qed;
     3.5  
     3.6  text {*
     3.7 - There are only two Isar language elements for calculational proofs:
     3.8 - \isakeyword{also} for initial or intermediate calculational steps,
     3.9 - and \isakeyword{finally} for building the result of a calculation.
    3.10 - These constructs are not hardwired into Isabelle/Isar, but defined on
    3.11 - top of the basic Isar/VM interpreter.  Expanding the
    3.12 + \bigskip There are only two Isar language elements for calculational
    3.13 + proofs: \isakeyword{also} for initial or intermediate calculational
    3.14 + steps, and \isakeyword{finally} for building the result of a
    3.15 + calculation.  These constructs are not hardwired into Isabelle/Isar,
    3.16 + but defined on top of the basic Isar/VM interpreter.  Expanding the
    3.17   \isakeyword{also} and \isakeyword{finally} derived language elements,
    3.18   calculations may be simulated as demonstrated below.
    3.19  
    3.20 @@ -117,7 +117,7 @@
    3.21  qed;
    3.22  
    3.23  
    3.24 -subsection {* Groups and monoids *};
    3.25 +subsection {* Groups as monoids *};
    3.26  
    3.27  text {*
    3.28    Monoids are usually defined like this.
     4.1 --- a/src/HOL/Isar_examples/KnasterTarski.thy	Wed Oct 06 18:50:40 1999 +0200
     4.2 +++ b/src/HOL/Isar_examples/KnasterTarski.thy	Wed Oct 06 18:50:51 1999 +0200
     4.3 @@ -5,16 +5,20 @@
     4.4  Typical textbook proof example.
     4.5  *)
     4.6  
     4.7 +header {* Textbook-style reasoning: the Knaster-Tarski Theorem *};
     4.8  
     4.9  theory KnasterTarski = Main:;
    4.10  
    4.11 +
    4.12 +subsection {* Prose version *};
    4.13 +
    4.14  text {*
    4.15   According to the book ``Introduction to Lattices and Order'' (by
    4.16   B. A. Davey and H. A. Priestley, CUP 1990), the Knaster-Tarski
    4.17 - fixpoint theorem is as follows (pages 93--94).  Note that we have
    4.18 - dualized their argument, and tuned the notation a little bit.
    4.19 + fixpoint theorem is as follows (pages 93--94).\footnote{We have
    4.20 + dualized their argument, and tuned the notation a little bit.}
    4.21  
    4.22 - \paragraph{The Knaster-Tarski Fixpoint Theorem.}  Let $L$ be a
    4.23 + \medskip \textbf{The Knaster-Tarski Fixpoint Theorem.}  Let $L$ be a
    4.24   complete lattice and $f \colon L \to L$ an order-preserving map.
    4.25   Then $\bigwedge \{ x \in L \mid f(x) \le x \}$ is a fixpoint of $f$.
    4.26  
    4.27 @@ -27,9 +31,12 @@
    4.28   \le f(a)$.
    4.29  *};
    4.30  
    4.31 +
    4.32 +subsection {* Formal version *};
    4.33 +
    4.34  text {*
    4.35 - Our proof below closely follows this presentation.  Virtually all of
    4.36 - the prose narration has been rephrased in terms of formal Isar
    4.37 + Our proof below closely follows the original presentation.  Virtually
    4.38 + all of the prose narration has been rephrased in terms of formal Isar
    4.39   language elements.  Just as many textbook-style proofs, there is a
    4.40   strong bias towards forward reasoning, and little hierarchical
    4.41   structure.
    4.42 @@ -62,5 +69,4 @@
    4.43    qed;
    4.44  qed;
    4.45  
    4.46 -
    4.47  end;
     5.1 --- a/src/HOL/Isar_examples/MultisetOrder.thy	Wed Oct 06 18:50:40 1999 +0200
     5.2 +++ b/src/HOL/Isar_examples/MultisetOrder.thy	Wed Oct 06 18:50:51 1999 +0200
     5.3 @@ -8,10 +8,13 @@
     5.4  HOL/Induct/Multiset).  Pen-and-paper proof by Wilfried Buchholz.
     5.5  *)
     5.6  
     5.7 +header {* Wellfoundedness of multiset ordering *};
     5.8  
     5.9  theory MultisetOrder = Multiset:;
    5.10  
    5.11  
    5.12 +subsection {* A technical lemma *};
    5.13 +
    5.14  lemma less_add: "(N, M0 + {#a#}) : mult1 r ==>
    5.15      (EX M. (M, M0) : mult1 r & N = M + {#a#}) |
    5.16      (EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K)"
    5.17 @@ -47,12 +50,13 @@
    5.18  qed;
    5.19  
    5.20  
    5.21 +subsection {* The key property *};
    5.22 +
    5.23  lemma all_accessible: "wf r ==> ALL M. M : acc (mult1 r)";
    5.24  proof;
    5.25    let ?R = "mult1 r";
    5.26    let ?W = "acc ?R";
    5.27  
    5.28 -
    5.29    {{;
    5.30      fix M M0 a;
    5.31      assume wf_hyp: "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)"
    5.32 @@ -97,7 +101,6 @@
    5.33      qed;
    5.34    }}; note tedious_reasoning = this;
    5.35  
    5.36 -
    5.37    assume wf: "wf r";
    5.38    fix M;
    5.39    show "M : ?W";
    5.40 @@ -123,11 +126,12 @@
    5.41  qed;
    5.42  
    5.43  
    5.44 +subsection {* Main result *};
    5.45 +
    5.46  theorem wf_mult1: "wf r ==> wf (mult1 r)";
    5.47    by (rule acc_wfI, rule all_accessible);
    5.48  
    5.49  theorem wf_mult: "wf r ==> wf (mult r)";
    5.50    by (unfold mult_def, rule wf_trancl, rule wf_mult1);
    5.51  
    5.52 -
    5.53  end;
     6.1 --- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Wed Oct 06 18:50:40 1999 +0200
     6.2 +++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Wed Oct 06 18:50:51 1999 +0200
     6.3 @@ -10,10 +10,12 @@
     6.4  See also HOL/Induct/Mutil for the original Isabelle tactic scripts.
     6.5  *)
     6.6  
     6.7 +header {* The Mutilated Checker Board Problem *};
     6.8 +
     6.9  theory MutilatedCheckerboard = Main:;
    6.10  
    6.11  
    6.12 -section {* Tilings *};
    6.13 +subsection {* Tilings *};
    6.14  
    6.15  consts
    6.16    tiling :: "'a set set => 'a set set";
    6.17 @@ -26,7 +28,8 @@
    6.18  
    6.19  text "The union of two disjoint tilings is a tiling";
    6.20  
    6.21 -lemma tiling_Un: "t : tiling A --> u : tiling A --> t Int u = {} --> t Un u : tiling A";
    6.22 +lemma tiling_Un:
    6.23 +  "t : tiling A --> u : tiling A --> t Int u = {} --> t Un u : tiling A";
    6.24  proof;
    6.25    assume "t : tiling A" (is "_ : ?T");
    6.26    thus "u : ?T --> t Int u = {} --> t Un u : ?T" (is "?P t");
    6.27 @@ -41,14 +44,15 @@
    6.28        have hyp: "t Un u: ?T"; by (blast!);
    6.29        have "a <= - (t Un u)"; by (blast!);
    6.30        with _ hyp; have "a Un (t Un u) : ?T"; by (rule tiling.Un);
    6.31 -      also; have "a Un (t Un u) = (a Un t) Un u"; by (simp only: Un_assoc);
    6.32 +      also; have "a Un (t Un u) = (a Un t) Un u";
    6.33 +        by (simp only: Un_assoc);
    6.34        finally; show "... : ?T"; .;
    6.35      qed;
    6.36    qed;
    6.37  qed;
    6.38  
    6.39  
    6.40 -section {* Basic properties of below *};
    6.41 +subsection {* Basic properties of below *};
    6.42  
    6.43  constdefs
    6.44    below :: "nat => nat set"
    6.45 @@ -60,22 +64,25 @@
    6.46  lemma below_0: "below 0 = {}";
    6.47    by (simp add: below_def);
    6.48  
    6.49 -lemma Sigma_Suc1: "below (Suc n) Times B = ({n} Times B) Un (below n Times B)";
    6.50 +lemma Sigma_Suc1:
    6.51 +    "below (Suc n) Times B = ({n} Times B) Un (below n Times B)";
    6.52    by (simp add: below_def less_Suc_eq) blast;
    6.53  
    6.54 -lemma Sigma_Suc2: "A Times below (Suc n) = (A Times {n}) Un (A Times (below n))";
    6.55 +lemma Sigma_Suc2:
    6.56 +    "A Times below (Suc n) = (A Times {n}) Un (A Times (below n))";
    6.57    by (simp add: below_def less_Suc_eq) blast;
    6.58  
    6.59  lemmas Sigma_Suc = Sigma_Suc1 Sigma_Suc2;
    6.60  
    6.61  
    6.62 -section {* Basic properties of evnodd *};
    6.63 +subsection {* Basic properties of evnodd *};
    6.64  
    6.65  constdefs
    6.66    evnodd :: "(nat * nat) set => nat => (nat * nat) set"
    6.67    "evnodd A b == A Int {(i, j). (i + j) mod 2 = b}";
    6.68  
    6.69 -lemma evnodd_iff: "(i, j): evnodd A b = ((i, j): A  & (i + j) mod 2 = b)";
    6.70 +lemma evnodd_iff:
    6.71 +    "(i, j): evnodd A b = ((i, j): A  & (i + j) mod 2 = b)";
    6.72    by (simp add: evnodd_def);
    6.73  
    6.74  lemma evnodd_subset: "evnodd A b <= A";
    6.75 @@ -97,11 +104,12 @@
    6.76    by (simp add: evnodd_def);
    6.77  
    6.78  lemma evnodd_insert: "evnodd (insert (i, j) C) b =
    6.79 -  (if (i + j) mod 2 = b then insert (i, j) (evnodd C b) else evnodd C b)";
    6.80 +    (if (i + j) mod 2 = b
    6.81 +      then insert (i, j) (evnodd C b) else evnodd C b)";
    6.82    by (simp add: evnodd_def) blast;
    6.83  
    6.84  
    6.85 -section {* Dominoes *};
    6.86 +subsection {* Dominoes *};
    6.87  
    6.88  consts 
    6.89    domino  :: "(nat * nat) set set";
    6.90 @@ -111,7 +119,6 @@
    6.91      horiz:  "{(i, j), (i, j + 1)} : domino"
    6.92      vertl:  "{(i, j), (i + 1, j)} : domino";
    6.93  
    6.94 -
    6.95  lemma dominoes_tile_row: "{i} Times below (2 * n) : tiling domino"
    6.96    (is "?P n" is "?B n : ?T");
    6.97  proof (induct n);
    6.98 @@ -123,7 +130,8 @@
    6.99    have "?B (Suc n) = ?a Un ?B n"; by (simp add: Sigma_Suc Un_assoc);
   6.100    also; have "... : ?T";
   6.101    proof (rule tiling.Un);
   6.102 -    have "{(i, 2 * n), (i, 2 * n + 1)} : domino"; by (rule domino.horiz);
   6.103 +    have "{(i, 2 * n), (i, 2 * n + 1)} : domino";
   6.104 +      by (rule domino.horiz);
   6.105      also; have "{(i, 2 * n), (i, 2 * n + 1)} = ?a"; by blast;
   6.106      finally; show "... : domino"; .;
   6.107      from hyp; show "?B n : ?T"; .;
   6.108 @@ -132,7 +140,8 @@
   6.109    finally; show "?P (Suc n)"; .;
   6.110  qed;
   6.111  
   6.112 -lemma dominoes_tile_matrix: "below m Times below (2 * n) : tiling domino"
   6.113 +lemma dominoes_tile_matrix:
   6.114 +  "below m Times below (2 * n) : tiling domino"
   6.115    (is "?P m" is "?B m : ?T");
   6.116  proof (induct m);
   6.117    show "?P 0"; by (simp add: below_0 tiling.empty);
   6.118 @@ -150,8 +159,8 @@
   6.119    finally; show "?P (Suc m)"; .;
   6.120  qed;
   6.121  
   6.122 -
   6.123 -lemma domino_singleton: "[| d : domino; b < 2 |] ==> EX i j. evnodd d b = {(i, j)}";
   6.124 +lemma domino_singleton:
   6.125 +  "[| d : domino; b < 2 |] ==> EX i j. evnodd d b = {(i, j)}";
   6.126  proof -;
   6.127    assume b: "b < 2";
   6.128    assume "d : domino";
   6.129 @@ -173,9 +182,10 @@
   6.130  qed;
   6.131  
   6.132  
   6.133 -section {* Tilings of dominoes *};
   6.134 +subsection {* Tilings of dominoes *};
   6.135  
   6.136 -lemma tiling_domino_finite: "t : tiling domino ==> finite t" (is "t : ?T ==> ?F t");
   6.137 +lemma tiling_domino_finite:
   6.138 +  "t : tiling domino ==> finite t" (is "t : ?T ==> ?F t");
   6.139  proof -;
   6.140    assume "t : ?T";
   6.141    thus "?F t";
   6.142 @@ -187,7 +197,8 @@
   6.143    qed;
   6.144  qed;
   6.145  
   6.146 -lemma tiling_domino_01: "t : tiling domino ==> card (evnodd t 0) = card (evnodd t 1)"
   6.147 +lemma tiling_domino_01:
   6.148 +  "t : tiling domino ==> card (evnodd t 0) = card (evnodd t 1)"
   6.149    (is "t : ?T ==> ?P t");
   6.150  proof -;
   6.151    assume "t : ?T";
   6.152 @@ -201,7 +212,8 @@
   6.153        and hyp: "card (?e t 0) = card (?e t 1)"
   6.154        and "a <= - t";
   6.155  
   6.156 -    have card_suc: "!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))";
   6.157 +    have card_suc:
   6.158 +      "!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))";
   6.159      proof -;
   6.160        fix b; assume "b < 2";
   6.161        have "EX i j. ?e a b = {(i, j)}"; by (rule domino_singleton);
   6.162 @@ -212,7 +224,8 @@
   6.163  	also; have "... Un ?e t b = insert (i, j) (?e t b)"; by simp;
   6.164  	also; have "card ... = Suc (card (?e t b))";
   6.165  	proof (rule card_insert_disjoint);
   6.166 -	  show "finite (?e t b)"; by (rule evnodd_finite, rule tiling_domino_finite);
   6.167 +	  show "finite (?e t b)";
   6.168 +            by (rule evnodd_finite, rule tiling_domino_finite);
   6.169  	  have "(i, j) : ?e a b"; by (simp!);
   6.170  	  thus "(i, j) ~: ?e t b"; by (force! dest: evnoddD);
   6.171  	qed;
   6.172 @@ -221,18 +234,20 @@
   6.173      qed;
   6.174      hence "card (?e (a Un t) 0) = Suc (card (?e t 0))"; by simp;
   6.175      also; from hyp; have "card (?e t 0) = card (?e t 1)"; .;
   6.176 -    also; from card_suc; have "Suc ... = card (?e (a Un t) 1)"; by simp;
   6.177 +    also; from card_suc; have "Suc ... = card (?e (a Un t) 1)";
   6.178 +      by simp;
   6.179      finally; show "?P (a Un t)"; .;
   6.180    qed;
   6.181  qed;
   6.182  
   6.183  
   6.184 -section {* Main theorem *};
   6.185 +subsection {* Main theorem *};
   6.186  
   6.187  constdefs
   6.188    mutilated_board :: "nat => nat => (nat * nat) set"
   6.189 -  "mutilated_board m n == below (2 * (m + 1)) Times below (2 * (n + 1))
   6.190 -    - {(0, 0)} - {(2 * m + 1, 2 * n + 1)}";
   6.191 +  "mutilated_board m n ==
   6.192 +    below (2 * (m + 1)) Times below (2 * (n + 1))
   6.193 +      - {(0, 0)} - {(2 * m + 1, 2 * n + 1)}";
   6.194  
   6.195  theorem mutil_not_tiling: "mutilated_board m n ~: tiling domino";
   6.196  proof (unfold mutilated_board_def);
   6.197 @@ -240,13 +255,15 @@
   6.198    let ?t = "below (2 * (m + 1)) Times below (2 * (n + 1))";
   6.199    let ?t' = "?t - {(0, 0)}";
   6.200    let ?t'' = "?t' - {(2 * m + 1, 2 * n + 1)}";
   6.201 +
   6.202    show "?t'' ~: ?T";
   6.203    proof;
   6.204      have t: "?t : ?T"; by (rule dominoes_tile_matrix);
   6.205      assume t'': "?t'' : ?T";
   6.206  
   6.207      let ?e = evnodd;
   6.208 -    have fin: "finite (?e ?t 0)"; by (rule evnodd_finite, rule tiling_domino_finite, rule t);
   6.209 +    have fin: "finite (?e ?t 0)";
   6.210 +      by (rule evnodd_finite, rule tiling_domino_finite, rule t);
   6.211  
   6.212      note [simp] = evnodd_iff evnodd_empty evnodd_insert evnodd_Diff;
   6.213      have "card (?e ?t'' 0) < card (?e ?t' 0)";
   6.214 @@ -261,15 +278,16 @@
   6.215      also; have "... < card (?e ?t 0)";
   6.216      proof -;
   6.217        have "(0, 0) : ?e ?t 0"; by simp;
   6.218 -      with fin; have "card (?e ?t 0 - {(0, 0)}) < card (?e ?t 0)"; by (rule card_Diff1_less);
   6.219 +      with fin; have "card (?e ?t 0 - {(0, 0)}) < card (?e ?t 0)";
   6.220 +        by (rule card_Diff1_less);
   6.221        thus ?thesis; by simp;
   6.222      qed;
   6.223      also; from t; have "... = card (?e ?t 1)"; by (rule tiling_domino_01);
   6.224      also; have "?e ?t 1 = ?e ?t'' 1"; by simp;
   6.225 -    also; from t''; have "card ... = card (?e ?t'' 0)"; by (rule tiling_domino_01 [RS sym]);
   6.226 +    also; from t''; have "card ... = card (?e ?t'' 0)";
   6.227 +      by (rule tiling_domino_01 [RS sym]);
   6.228      finally; show False; ..;
   6.229    qed;
   6.230  qed;
   6.231  
   6.232 -
   6.233  end;
     7.1 --- a/src/HOL/Isar_examples/Summation.thy	Wed Oct 06 18:50:40 1999 +0200
     7.2 +++ b/src/HOL/Isar_examples/Summation.thy	Wed Oct 06 18:50:51 1999 +0200
     7.3 @@ -11,6 +11,7 @@
     7.4  
     7.5  theory Summation = Main:;
     7.6  
     7.7 +
     7.8  subsection {* A summation operator *};
     7.9  
    7.10  consts
    7.11 @@ -21,14 +22,16 @@
    7.12    "sum f (Suc n) = f n + sum f n";
    7.13  
    7.14  syntax
    7.15 -  "_SUM" :: "idt => nat => nat => nat"       ("SUM _ < _. _" [0, 0, 10] 10);
    7.16 +  "_SUM" :: "idt => nat => nat => nat"  ("SUM _ < _. _" [0, 0, 10] 10);
    7.17  translations
    7.18    "SUM i < k. b" == "sum (%i. b) k";
    7.19  
    7.20  
    7.21  subsection {* Summation laws *};
    7.22  
    7.23 -syntax				(* FIXME binary arithmetic does not yet work here *)
    7.24 +(* FIXME binary arithmetic does not yet work here *)
    7.25 +
    7.26 +syntax
    7.27    "3" :: nat  ("3")
    7.28    "4" :: nat  ("4")
    7.29    "6" :: nat  ("6");
    7.30 @@ -65,7 +68,8 @@
    7.31    finally; show "?P (Suc n)"; by simp;
    7.32  qed;
    7.33  
    7.34 -theorem sum_of_squares: "6 * (SUM i < n + 1. i^2) = n * (n + 1) * (2 * n + 1)"
    7.35 +theorem sum_of_squares:
    7.36 +  "6 * (SUM i < n + 1. i^2) = n * (n + 1) * (2 * n + 1)"
    7.37    (is "?P n" is "?S n = _");
    7.38  proof (induct n);
    7.39    show "?P 0"; by simp;
    7.40 @@ -73,7 +77,8 @@
    7.41    fix n;
    7.42    have "?S (n + 1) = ?S n + 6 * (n + 1)^2"; by simp;
    7.43    also; assume "?S n = n * (n + 1) * (2 * n + 1)";
    7.44 -  also; have "... + 6 * (n + 1)^2 = (n + 1) * (n + 2) * (2 * (n + 1) + 1)"; by simp;
    7.45 +  also; have "... + 6 * (n + 1)^2 = (n + 1) * (n + 2) * (2 * (n + 1) + 1)";
    7.46 +    by simp;
    7.47    finally; show "?P (Suc n)"; by simp;
    7.48  qed;
    7.49  
    7.50 @@ -85,7 +90,8 @@
    7.51    fix n;
    7.52    have "?S (n + 1) = ?S n + 4 * (n + 1)^3"; by simp;
    7.53    also; assume "?S n = (n * (n + 1))^2";
    7.54 -  also; have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^2"; by simp;
    7.55 +  also; have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^2";
    7.56 +    by simp;
    7.57    finally; show "?P (Suc n)"; by simp;
    7.58  qed;
    7.59  
     8.1 --- a/src/HOL/Isar_examples/W_correct.thy	Wed Oct 06 18:50:40 1999 +0200
     8.2 +++ b/src/HOL/Isar_examples/W_correct.thy	Wed Oct 06 18:50:51 1999 +0200
     8.3 @@ -6,22 +6,25 @@
     8.4  Based upon HOL/W0 by Dieter Nazareth and Tobias Nipkow.
     8.5  *)
     8.6  
     8.7 +header {* Correctness of Milner's type inference algorithm~W (let-free version) *};
     8.8 +
     8.9  theory W_correct = Main + Type:;
    8.10  
    8.11  
    8.12 -section "Mini ML with type inference rules";
    8.13 +subsection "Mini ML with type inference rules";
    8.14  
    8.15  datatype
    8.16    expr = Var nat | Abs expr | App expr expr;
    8.17  
    8.18  
    8.19 -text {* type inference rules *};
    8.20 +text {* Type inference rules. *};
    8.21  
    8.22  consts
    8.23    has_type :: "(typ list * expr * typ) set";
    8.24  
    8.25  syntax
    8.26 -  "@has_type" :: "[typ list, expr, typ] => bool"  ("((_) |-/ (_) :: (_))" [60, 0, 60] 60);
    8.27 +  "@has_type" :: "[typ list, expr, typ] => bool"
    8.28 +    ("((_) |-/ (_) :: (_))" [60, 0, 60] 60);
    8.29  translations
    8.30    "a |- e :: t" == "(a,e,t) : has_type";
    8.31  
    8.32 @@ -32,6 +35,8 @@
    8.33      AppI: "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |]
    8.34                ==> a |- App e1 e2 :: t1";
    8.35  
    8.36 +text {* Type assigment is close wrt.\ substitution. *};
    8.37 +
    8.38  lemma has_type_subst_closed: "a |- e :: t ==> $s a |- e :: $s t";
    8.39  proof -;
    8.40    assume "a |- e :: t";
    8.41 @@ -40,15 +45,18 @@
    8.42      fix a n;
    8.43      assume "n < length a";
    8.44      hence "n < length (map ($ s) a)"; by simp;
    8.45 -    hence "map ($ s) a |- Var n :: map ($ s) a ! n"; by (rule has_type.VarI);
    8.46 +    hence "map ($ s) a |- Var n :: map ($ s) a ! n";
    8.47 +      by (rule has_type.VarI);
    8.48      also; have "map ($ s) a ! n = $ s (a ! n)"; by (rule nth_map);
    8.49      also; have "map ($ s) a = $ s a"; by (simp only: app_subst_list);   (* FIXME unfold fails!? *)
    8.50      finally; show "?P a (Var n) (a ! n)"; .;
    8.51    next;
    8.52      fix a e t1 t2;
    8.53      assume "?P (t1 # a) e t2";
    8.54 -    hence "$ s t1 # map ($ s) a |- e :: $ s t2"; by (simp add: app_subst_list);
    8.55 -    hence "map ($ s) a |- Abs e :: $ s t1 -> $ s t2"; by (rule has_type.AbsI);
    8.56 +    hence "$ s t1 # map ($ s) a |- e :: $ s t2";
    8.57 +      by (simp add: app_subst_list);
    8.58 +    hence "map ($ s) a |- Abs e :: $ s t1 -> $ s t2";
    8.59 +      by (rule has_type.AbsI);
    8.60      thus "?P a (Abs e) (t1 -> t2)"; by (simp add: app_subst_list);
    8.61    next;
    8.62      fix a e1 e2 t1 t2;
    8.63 @@ -58,7 +66,7 @@
    8.64  qed;
    8.65  
    8.66  
    8.67 -section {* Type inference algorithm W *};
    8.68 +subsection {* Type inference algorithm W *};
    8.69  
    8.70  consts
    8.71    W :: "[expr, typ list, nat] => (subst * typ * nat) maybe";
    8.72 @@ -76,13 +84,16 @@
    8.73         Ok ($u o $s2 o s1, $u (TVar m2), Suc m2))";
    8.74  
    8.75  
    8.76 +subsection {* Correctness theorem *};
    8.77 +
    8.78  (* FIXME proper split att/mod *)
    8.79  ML_setup {* Addsplits [split_bind]; *};
    8.80  
    8.81  theorem W_correct: "W e a n = Ok (s, t, m) ==> $ s a |- e :: t";
    8.82  proof -;
    8.83    assume W_ok: "W e a n = Ok (s, t, m)";
    8.84 -  have "ALL a s t m n . Ok (s, t, m) = W e a n --> $ s a |- e :: t" (is "?P e");
    8.85 +  have "ALL a s t m n . Ok (s, t, m) = W e a n --> $ s a |- e :: t"
    8.86 +    (is "?P e");
    8.87    proof (induct e);
    8.88      fix n; show "?P (Var n)"; by simp;
    8.89    next;
    8.90 @@ -91,7 +102,8 @@
    8.91      proof (intro allI impI);
    8.92        fix a s t m n;
    8.93        assume "Ok (s, t, m) = W (Abs e) a n";
    8.94 -      hence "EX t'. t = s n -> t' & Ok (s, t', m) = W e (TVar n # a) (Suc n)";
    8.95 +      hence "EX t'. t = s n -> t' &
    8.96 +          Ok (s, t', m) = W e (TVar n # a) (Suc n)";
    8.97          by (rule rev_mp) simp;
    8.98        with hyp; show "$ s a |- Abs e :: t";
    8.99          by (force intro: has_type.AbsI);
   8.100 @@ -116,7 +128,8 @@
   8.101            and W2_ok: "W e2 ($ s1 a) n1 = Ok (s2, t2, n2)";
   8.102          show ?thesis;
   8.103          proof (rule has_type.AppI);
   8.104 -          from s; have s': "$ u ($ s2 ($ s1 a)) = $s a"; by (simp add: subst_comp_tel o_def);
   8.105 +          from s; have s': "$ u ($ s2 ($ s1 a)) = $s a";
   8.106 +            by (simp add: subst_comp_tel o_def);
   8.107            show "$s a |- e1 :: $ u t2 -> t";
   8.108            proof -;
   8.109              from hyp1 W1_ok [RS sym]; have "$ s1 a |- e1 :: t1"; by blast;
   8.110 @@ -126,7 +139,8 @@
   8.111            qed;
   8.112            show "$ s a |- e2 :: $ u t2";
   8.113            proof -;
   8.114 -            from hyp2 W2_ok [RS sym]; have "$ s2 ($ s1 a) |- e2 :: t2"; by blast;
   8.115 +            from hyp2 W2_ok [RS sym]; have "$ s2 ($ s1 a) |- e2 :: t2";
   8.116 +              by blast;
   8.117              hence "$ u ($ s2 ($ s1 a)) |- e2 :: $ u t2";
   8.118                by (rule has_type_subst_closed);
   8.119              with s'; show ?thesis; by simp;
   8.120 @@ -138,5 +152,4 @@
   8.121    with W_ok [RS sym]; show ?thesis; by blast;
   8.122  qed;
   8.123  
   8.124 -
   8.125  end;
     9.1 --- a/src/HOL/Isar_examples/document/style.tex	Wed Oct 06 18:50:40 1999 +0200
     9.2 +++ b/src/HOL/Isar_examples/document/style.tex	Wed Oct 06 18:50:51 1999 +0200
     9.3 @@ -1,9 +1,11 @@
     9.4 +
     9.5 +%% $Id$
     9.6  
     9.7  \documentclass[11pt,a4paper]{article}
     9.8  \usepackage{isabelle,pdfsetup}
     9.9  
    9.10  \renewcommand{\isamarkupheader}[1]{\section{#1}}
    9.11 -%\parindent 0pt \parskip 0.5ex
    9.12 +\parindent 0pt \parskip 0.5ex
    9.13  
    9.14  \newcommand{\name}[1]{\textsf{#1}}
    9.15