author wenzelm Wed Oct 06 18:50:51 1999 +0200 (1999-10-06) changeset 7761 7fab9592384f parent 7760 43f8d28dbc6e child 7762 c98d70538033
improved presentation;
     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