improved presentation;
authorwenzelm
Fri Oct 08 15:09:14 1999 +0200 (1999-10-08)
changeset 78008ee919e42174
parent 7799 4c69318e6a6d
child 7801 535112d1f316
improved presentation;
src/HOL/Induct/Acc.thy
src/HOL/Isar_examples/Cantor.thy
src/HOL/Isar_examples/Group.thy
src/HOL/Isar_examples/MultisetOrder.thy
src/HOL/Isar_examples/MutilatedCheckerboard.thy
src/HOL/Isar_examples/ROOT.ML
src/HOL/Isar_examples/Summation.thy
src/HOL/Isar_examples/W_correct.thy
src/HOL/Isar_examples/document/root.tex
src/HOL/Isar_examples/document/style.tex
src/Pure/Thy/latex.ML
     1.1 --- a/src/HOL/Induct/Acc.thy	Fri Oct 08 15:08:47 1999 +0200
     1.2 +++ b/src/HOL/Induct/Acc.thy	Fri Oct 08 15:09:14 1999 +0200
     1.3 @@ -18,10 +18,12 @@
     1.4  
     1.5  inductive "acc r"
     1.6    intrs
     1.7 -    accI [rulify_prems]: "ALL y. (y, x) : r --> y : acc r ==> x : acc r"
     1.8 -
     1.9 +    accI [rulify_prems]:
    1.10 +      "ALL y. (y, x) : r --> y : acc r ==> x : acc r"
    1.11  
    1.12 -syntax        termi :: "('a * 'a)set => 'a set"
    1.13 -translations "termi r" == "acc(r^-1)"
    1.14 +syntax
    1.15 +  termi :: "('a * 'a)set => 'a set"
    1.16 +translations
    1.17 +  "termi r" == "acc(r^-1)"
    1.18  
    1.19  end
     2.1 --- a/src/HOL/Isar_examples/Cantor.thy	Fri Oct 08 15:08:47 1999 +0200
     2.2 +++ b/src/HOL/Isar_examples/Cantor.thy	Fri Oct 08 15:09:14 1999 +0200
     2.3 @@ -6,15 +6,16 @@
     2.4  chapter of "Isabelle's Object-Logics" (Larry Paulson).
     2.5  *)
     2.6  
     2.7 -header {* More classical proofs: Cantor's Theorem *};
     2.8 +header {* Cantor's Theorem *};
     2.9  
    2.10  theory Cantor = Main:;
    2.11  
    2.12  text {*
    2.13    Cantor's Theorem states that every set has more subsets than it has
    2.14 -  elements.  It has become a favourite basic example in higher-order logic
    2.15 -  since it is so easily expressed: \[\all{f::\alpha \To \alpha \To \idt{bool}}
    2.16 -  \ex{S::\alpha \To \idt{bool}} \all{x::\alpha}. f \ap x \not= S\]
    2.17 +  elements.  It has become a favorite basic example in pure
    2.18 +  higher-order logic since it is so easily expressed: \[\all{f::\alpha
    2.19 +  \To \alpha \To \idt{bool}} \ex{S::\alpha \To \idt{bool}}
    2.20 +  \all{x::\alpha}. f \ap x \not= S\]
    2.21    
    2.22    Viewing types as sets, $\alpha \To \idt{bool}$ represents the powerset of
    2.23    $\alpha$.  This version of the theorem states that for every function from
     3.1 --- a/src/HOL/Isar_examples/Group.thy	Fri Oct 08 15:08:47 1999 +0200
     3.2 +++ b/src/HOL/Isar_examples/Group.thy	Fri Oct 08 15:09:14 1999 +0200
     3.3 @@ -11,7 +11,8 @@
     3.4  
     3.5  text {*
     3.6   We define an axiomatic type class of general groups over signature
     3.7 - $({\times}, \idt{one}, \idt{inv})$.
     3.8 + $({\times} :: \alpha \To \alpha \To \alpha, \idt{one} :: \alpha,
     3.9 + \idt{inv} :: \alpha \To \alpha)$.
    3.10  *};
    3.11  
    3.12  consts
     4.1 --- a/src/HOL/Isar_examples/MultisetOrder.thy	Fri Oct 08 15:08:47 1999 +0200
     4.2 +++ b/src/HOL/Isar_examples/MultisetOrder.thy	Fri Oct 08 15:09:14 1999 +0200
     4.3 @@ -25,12 +25,14 @@
     4.4    let ?case1 = "?case1 {(N, M). ?R N M}";
     4.5  
     4.6    assume "(N, M0 + {#a#}) : {(N, M). ?R N M}";
     4.7 -  hence "EX a' M0' K. M0 + {#a#} = M0' + {#a'#} & N = M0' + K & ?r K a'"; by simp;
     4.8 +  hence "EX a' M0' K.
     4.9 +      M0 + {#a#} = M0' + {#a'#} & N = M0' + K & ?r K a'"; by simp;
    4.10    thus "?case1 | ?case2";
    4.11    proof (elim exE conjE);
    4.12      fix a' M0' K; assume N: "N = M0' + K" and r: "?r K a'";
    4.13      assume "M0 + {#a#} = M0' + {#a'#}";
    4.14 -    hence "M0 = M0' & a = a' | (EX K'. M0 = K' + {#a'#} & M0' = K' + {#a#})";
    4.15 +    hence "M0 = M0' & a = a' |
    4.16 +        (EX K'. M0 = K' + {#a'#} & M0' = K' + {#a#})";
    4.17        by (simp only: add_eq_conv_ex);
    4.18      thus ?thesis;
    4.19      proof (elim disjE conjE exE);
    4.20 @@ -59,14 +61,14 @@
    4.21  
    4.22    {{;
    4.23      fix M M0 a;
    4.24 -    assume wf_hyp: "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)"
    4.25 -      and M0: "M0 : ?W"
    4.26 +    assume M0: "M0 : ?W"
    4.27 +      and wf_hyp: "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)"
    4.28        and acc_hyp: "ALL M. (M, M0) : ?R --> M + {#a#} : ?W";
    4.29      have "M0 + {#a#} : ?W";
    4.30      proof (rule accI [of "M0 + {#a#}"]);
    4.31        fix N; assume "(N, M0 + {#a#}) : ?R";
    4.32        hence "((EX M. (M, M0) : ?R & N = M + {#a#}) |
    4.33 -             (EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K))";
    4.34 +          (EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K))";
    4.35  	by (rule less_add);
    4.36        thus "N : ?W";
    4.37        proof (elim exE disjE conjE);
    4.38 @@ -88,7 +90,7 @@
    4.39  	  proof;
    4.40  	    assume a: "ALL b. elem (K + {#x#}) b --> (b, a) : r";
    4.41  	    hence "(x, a) : r"; by simp;
    4.42 -	    with wf_hyp [RS spec]; have b: "ALL M:?W. M + {#x#} : ?W"; ..;
    4.43 +	    with wf_hyp; have b: "ALL M:?W. M + {#x#} : ?W"; by blast;
    4.44  
    4.45  	    from a hyp; have "M0 + K : ?W"; by simp;
    4.46  	    with b; have "(M0 + K) + {#x#} : ?W"; ..;
    4.47 @@ -114,11 +116,13 @@
    4.48      fix M a; assume "M : ?W";
    4.49      from wf; have "ALL M:?W. M + {#a#} : ?W";
    4.50      proof (rule wf_induct [of r]);
    4.51 -      fix a; assume "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)";
    4.52 +      fix a;
    4.53 +      assume "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)";
    4.54        show "ALL M:?W. M + {#a#} : ?W";
    4.55        proof;
    4.56  	fix M; assume "M : ?W";
    4.57 -	thus "M + {#a#} : ?W"; by (rule acc_induct) (rule tedious_reasoning);
    4.58 +	thus "M + {#a#} : ?W";
    4.59 +          by (rule acc_induct) (rule tedious_reasoning);
    4.60        qed;
    4.61      qed;
    4.62      thus "M + {#a#} : ?W"; ..;
     5.1 --- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Fri Oct 08 15:08:47 1999 +0200
     5.2 +++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Fri Oct 08 15:09:14 1999 +0200
     5.3 @@ -23,13 +23,15 @@
     5.4  inductive "tiling A"
     5.5    intrs
     5.6      empty: "{} : tiling A"
     5.7 -    Un:    "[| a : A;  t : tiling A;  a <= - t |] ==> a Un t : tiling A";
     5.8 +    Un:    "[| a : A;  t : tiling A;  a <= - t |]
     5.9 +              ==> a Un t : tiling A";
    5.10  
    5.11  
    5.12 -text "The union of two disjoint tilings is a tiling";
    5.13 +text "The union of two disjoint tilings is a tiling.";
    5.14  
    5.15  lemma tiling_Un:
    5.16 -  "t : tiling A --> u : tiling A --> t Int u = {} --> t Un u : tiling A";
    5.17 +  "t : tiling A --> u : tiling A --> t Int u = {}
    5.18 +    --> t Un u : tiling A";
    5.19  proof;
    5.20    assume "t : tiling A" (is "_ : ?T");
    5.21    thus "u : ?T --> t Int u = {} --> t Un u : ?T" (is "?P t");
    5.22 @@ -119,7 +121,8 @@
    5.23      horiz:  "{(i, j), (i, j + 1)} : domino"
    5.24      vertl:  "{(i, j), (i + 1, j)} : domino";
    5.25  
    5.26 -lemma dominoes_tile_row: "{i} Times below (2 * n) : tiling domino"
    5.27 +lemma dominoes_tile_row:
    5.28 +  "{i} Times below (2 * n) : tiling domino"
    5.29    (is "?P n" is "?B n : ?T");
    5.30  proof (induct n);
    5.31    show "?P 0"; by (simp add: below_0 tiling.empty);
    5.32 @@ -268,9 +271,11 @@
    5.33      note [simp] = evnodd_iff evnodd_empty evnodd_insert evnodd_Diff;
    5.34      have "card (?e ?t'' 0) < card (?e ?t' 0)";
    5.35      proof -;
    5.36 -      have "card (?e ?t' 0 - {(2 * m + 1, 2 * n + 1)}) < card (?e ?t' 0)";
    5.37 +      have "card (?e ?t' 0 - {(2 * m + 1, 2 * n + 1)})
    5.38 +        < card (?e ?t' 0)";
    5.39        proof (rule card_Diff1_less);
    5.40 -	show "finite (?e ?t' 0)"; by (rule finite_subset, rule fin) force;
    5.41 +	show "finite (?e ?t' 0)";
    5.42 +          by (rule finite_subset, rule fin) force;
    5.43  	show "(2 * m + 1, 2 * n + 1) : ?e ?t' 0"; by simp;
    5.44        qed;
    5.45        thus ?thesis; by simp;
    5.46 @@ -282,7 +287,8 @@
    5.47          by (rule card_Diff1_less);
    5.48        thus ?thesis; by simp;
    5.49      qed;
    5.50 -    also; from t; have "... = card (?e ?t 1)"; by (rule tiling_domino_01);
    5.51 +    also; from t; have "... = card (?e ?t 1)";
    5.52 +      by (rule tiling_domino_01);
    5.53      also; have "?e ?t 1 = ?e ?t'' 1"; by simp;
    5.54      also; from t''; have "card ... = card (?e ?t'' 0)";
    5.55        by (rule tiling_domino_01 [RS sym]);
     6.1 --- a/src/HOL/Isar_examples/ROOT.ML	Fri Oct 08 15:08:47 1999 +0200
     6.2 +++ b/src/HOL/Isar_examples/ROOT.ML	Fri Oct 08 15:09:14 1999 +0200
     6.3 @@ -6,8 +6,8 @@
     6.4  *)
     6.5  
     6.6  time_use_thy "BasicLogic";
     6.7 +time_use_thy "Cantor";
     6.8  time_use_thy "Peirce";
     6.9 -time_use_thy "Cantor";
    6.10  time_use_thy "ExprCompiler";
    6.11  time_use_thy "Group";
    6.12  time_use_thy "Summation";
     7.1 --- a/src/HOL/Isar_examples/Summation.thy	Fri Oct 08 15:08:47 1999 +0200
     7.2 +++ b/src/HOL/Isar_examples/Summation.thy	Fri Oct 08 15:09:14 1999 +0200
     7.3 @@ -22,13 +22,16 @@
     7.4    "sum f (Suc n) = f n + sum f n";
     7.5  
     7.6  syntax
     7.7 -  "_SUM" :: "idt => nat => nat => nat"  ("SUM _ < _. _" [0, 0, 10] 10);
     7.8 +  "_SUM" :: "idt => nat => nat => nat"
     7.9 +    ("SUM _ < _. _" [0, 0, 10] 10);
    7.10  translations
    7.11    "SUM i < k. b" == "sum (%i. b) k";
    7.12  
    7.13  
    7.14  subsection {* Summation laws *};
    7.15  
    7.16 +verbatim {* \begin{comment} *};
    7.17 +
    7.18  (* FIXME binary arithmetic does not yet work here *)
    7.19  
    7.20  syntax
    7.21 @@ -43,8 +46,11 @@
    7.22  
    7.23  theorems [simp] = add_mult_distrib add_mult_distrib2 mult_ac;
    7.24  
    7.25 +verbatim {* \end{comment} *};
    7.26  
    7.27 -theorem sum_of_naturals: "2 * (SUM i < n + 1. i) = n * (n + 1)"
    7.28 +
    7.29 +theorem sum_of_naturals:
    7.30 +  "2 * (SUM i < n + 1. i) = n * (n + 1)"
    7.31    (is "?P n" is "?S n = _");
    7.32  proof (induct n);
    7.33    show "?P 0"; by simp;
    7.34 @@ -56,7 +62,8 @@
    7.35    finally; show "?P (Suc n)"; by simp;
    7.36  qed;
    7.37  
    7.38 -theorem sum_of_odds: "(SUM i < n. 2 * i + 1) = n^2"
    7.39 +theorem sum_of_odds:
    7.40 +  "(SUM i < n. 2 * i + 1) = n^2"
    7.41    (is "?P n" is "?S n = _");
    7.42  proof (induct n);
    7.43    show "?P 0"; by simp;
    7.44 @@ -77,12 +84,13 @@
    7.45    fix n;
    7.46    have "?S (n + 1) = ?S n + 6 * (n + 1)^2"; by simp;
    7.47    also; assume "?S n = n * (n + 1) * (2 * n + 1)";
    7.48 -  also; have "... + 6 * (n + 1)^2 = (n + 1) * (n + 2) * (2 * (n + 1) + 1)";
    7.49 -    by simp;
    7.50 +  also; have "... + 6 * (n + 1)^2 =
    7.51 +    (n + 1) * (n + 2) * (2 * (n + 1) + 1)"; by simp;
    7.52    finally; show "?P (Suc n)"; by simp;
    7.53  qed;
    7.54  
    7.55 -theorem sum_of_cubes: "4 * (SUM i < n + 1. i^3) = (n * (n + 1))^2"
    7.56 +theorem sum_of_cubes:
    7.57 +  "4 * (SUM i < n + 1. i^3) = (n * (n + 1))^2"
    7.58    (is "?P n" is "?S n = _");
    7.59  proof (induct n);
    7.60    show "?P 0"; by simp;
     8.1 --- a/src/HOL/Isar_examples/W_correct.thy	Fri Oct 08 15:08:47 1999 +0200
     8.2 +++ b/src/HOL/Isar_examples/W_correct.thy	Fri Oct 08 15:09:14 1999 +0200
     8.3 @@ -6,7 +6,7 @@
     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 +header {* Milner's type inference algorithm~W (let-free version) *};
     8.9  
    8.10  theory W_correct = Main + Type:;
    8.11  
    8.12 @@ -47,8 +47,10 @@
    8.13      hence "n < length (map ($ s) a)"; by simp;
    8.14      hence "map ($ s) a |- Var n :: map ($ s) a ! n";
    8.15        by (rule has_type.VarI);
    8.16 -    also; have "map ($ s) a ! n = $ s (a ! n)"; by (rule nth_map);
    8.17 -    also; have "map ($ s) a = $ s a"; by (simp only: app_subst_list);   (* FIXME unfold fails!? *)
    8.18 +    also; have "map ($ s) a ! n = $ s (a ! n)";
    8.19 +      by (rule nth_map);
    8.20 +    also; have "map ($ s) a = $ s a";
    8.21 +      by (simp only: app_subst_list);   (* FIXME unfold fails!? *)
    8.22      finally; show "?P a (Var n) (a ! n)"; .;
    8.23    next;
    8.24      fix a e t1 t2;
    8.25 @@ -114,10 +116,11 @@
    8.26      proof (intro allI impI);
    8.27        fix a s t m n; assume "Ok (s, t, m) = W (App e1 e2) a n";
    8.28        hence "EX s1 t1 n1 s2 t2 n2 u.
    8.29 -        s = $ u o $ s2 o s1 & t = u n2 &
    8.30 -        mgu ($ s2 t1) (t2 -> TVar n2) = Ok u &
    8.31 -           W e2 ($ s1 a) n1 = Ok (s2, t2, n2) &
    8.32 -           W e1 a n = Ok (s1, t1, n1)"; by (rule rev_mp) (simp, force); (* FIXME force fails !??*)
    8.33 +          s = $ u o $ s2 o s1 & t = u n2 &
    8.34 +          mgu ($ s2 t1) (t2 -> TVar n2) = Ok u &
    8.35 +             W e2 ($ s1 a) n1 = Ok (s2, t2, n2) &
    8.36 +             W e1 a n = Ok (s1, t1, n1)";
    8.37 +        by (rule rev_mp) (simp, force); (* FIXME force fails !??*)
    8.38        thus "$ s a |- App e1 e2 :: t";
    8.39        proof (elim exE conjE);
    8.40          fix s1 t1 n1 s2 t2 n2 u;
    8.41 @@ -132,7 +135,8 @@
    8.42              by (simp add: subst_comp_tel o_def);
    8.43            show "$s a |- e1 :: $ u t2 -> t";
    8.44            proof -;
    8.45 -            from hyp1 W1_ok [RS sym]; have "$ s1 a |- e1 :: t1"; by blast;
    8.46 +            from hyp1 W1_ok [RS sym]; have "$ s1 a |- e1 :: t1";
    8.47 +              by blast;
    8.48              hence "$ u ($ s2 ($ s1 a)) |- e1 :: $ u ($ s2 t1)";
    8.49                by (intro has_type_subst_closed);
    8.50              with s' t mgu_ok; show ?thesis; by simp;
     9.1 --- a/src/HOL/Isar_examples/document/root.tex	Fri Oct 08 15:08:47 1999 +0200
     9.2 +++ b/src/HOL/Isar_examples/document/root.tex	Fri Oct 08 15:09:14 1999 +0200
     9.3 @@ -3,7 +3,6 @@
     9.4  
     9.5  \hyphenation{Isabelle}
     9.6  
     9.7 -
     9.8  \begin{document}
     9.9  
    9.10  \title{Miscellaneous Isabelle/Isar examples for Higher-Order Logic}
    9.11 @@ -18,7 +17,6 @@
    9.12  \end{abstract}
    9.13  
    9.14  \tableofcontents
    9.15 -
    9.16  \input{session}
    9.17  
    9.18  \end{document}
    10.1 --- a/src/HOL/Isar_examples/document/style.tex	Fri Oct 08 15:08:47 1999 +0200
    10.2 +++ b/src/HOL/Isar_examples/document/style.tex	Fri Oct 08 15:09:14 1999 +0200
    10.3 @@ -2,7 +2,7 @@
    10.4  %% $Id$
    10.5  
    10.6  \documentclass[11pt,a4paper]{article}
    10.7 -\usepackage{isabelle,pdfsetup}
    10.8 +\usepackage{comment,isabelle,pdfsetup}
    10.9  
   10.10  \renewcommand{\isamarkupheader}[1]{\section{#1}}
   10.11  \parindent 0pt \parskip 0.5ex
    11.1 --- a/src/Pure/Thy/latex.ML	Fri Oct 08 15:08:47 1999 +0200
    11.2 +++ b/src/Pure/Thy/latex.ML	Fri Oct 08 15:09:14 1999 +0200
    11.3 @@ -26,25 +26,16 @@
    11.4    "%" => "\\%" |
    11.5    "#" => "\\#" |
    11.6    "_" => "\\_" |
    11.7 -  "{" => "{\\textbraceleft}" |
    11.8 -  "}" => "{\\textbraceright}" |
    11.9 -  "~" => "{\\textasciitilde}" |
   11.10 -  "^" => "{\\textasciicircum}" |
   11.11 +  "{" => "{\\isabraceleft}" |
   11.12 +  "}" => "{\\isabraceright}" |
   11.13 +  "~" => "{\\isatilde}" |
   11.14 +  "^" => "{\\isacircum}" |
   11.15    "\"" => "{\"}" |
   11.16 -  "\\" => "\\verb,\\," |
   11.17 +  "\\" => "{\\isabackslash}" |
   11.18    c => c;
   11.19  
   11.20 -val output_chr' = fn
   11.21 -  "\\" => "{\\textbackslash}" |
   11.22 -  "|" => "{\\textbar}" |
   11.23 -  "<" => "{\\textless}" |
   11.24 -  ">" => "{\\textgreater}" |
   11.25 -  c => output_chr c;
   11.26 -
   11.27 -
   11.28  (* FIXME replace \<forall> etc. *)
   11.29  val output_sym = implode o map output_chr o explode;
   11.30 -val output_sym' = implode o map output_chr' o explode;
   11.31  
   11.32  
   11.33  (* token output *)
   11.34 @@ -63,14 +54,18 @@
   11.35  fun output_tok (Basic tok) =
   11.36        let val s = T.val_of tok in
   11.37          if invisible_token tok then ""
   11.38 -        else if T.is_kind T.Command tok then "\\isacommand{" ^ output_sym' s ^ "}"
   11.39 -        else if T.is_kind T.Keyword tok then "\\isakeyword{" ^ output_sym' s ^ "}"
   11.40 +        else if T.is_kind T.Command tok then
   11.41 +          if s = "{{" then "{\\isabeginblock}"
   11.42 +          else if s = "}}" then "{\\isaendblock}"
   11.43 +          else "\\isacommand{" ^ output_sym s ^ "}"
   11.44 +        else if T.is_kind T.Keyword tok andalso Syntax.is_identifier s then
   11.45 +          "\\isakeyword{" ^ output_sym s ^ "}"
   11.46          else if T.is_kind T.String tok then output_sym (quote s)
   11.47          else if T.is_kind T.Verbatim tok then output_sym (enclose "{*" "*}" s)
   11.48          else output_sym s
   11.49        end
   11.50 -  | output_tok (Markup (cmd, arg)) = "\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks arg ^ "}\n"
   11.51 -  | output_tok (Verbatim txt) = "\n" ^ txt ^ "\n";
   11.52 +  | output_tok (Markup (cmd, txt)) = "\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks txt ^ "}\n"
   11.53 +  | output_tok (Verbatim txt) = "\n" ^ strip_blanks txt ^ "\n";
   11.54  
   11.55  
   11.56  val output_tokens = implode o map output_tok;