# HG changeset patch # User wenzelm # Date 939388154 -7200 # Node ID 8ee919e42174255c96247699692bd79b9bbfc424 # Parent 4c69318e6a6d1102c0a319c466bea91ffb40da30 improved presentation; diff -r 4c69318e6a6d -r 8ee919e42174 src/HOL/Induct/Acc.thy --- a/src/HOL/Induct/Acc.thy Fri Oct 08 15:08:47 1999 +0200 +++ b/src/HOL/Induct/Acc.thy Fri Oct 08 15:09:14 1999 +0200 @@ -18,10 +18,12 @@ inductive "acc r" intrs - accI [rulify_prems]: "ALL y. (y, x) : r --> y : acc r ==> x : acc r" - + accI [rulify_prems]: + "ALL y. (y, x) : r --> y : acc r ==> x : acc r" -syntax termi :: "('a * 'a)set => 'a set" -translations "termi r" == "acc(r^-1)" +syntax + termi :: "('a * 'a)set => 'a set" +translations + "termi r" == "acc(r^-1)" end diff -r 4c69318e6a6d -r 8ee919e42174 src/HOL/Isar_examples/Cantor.thy --- a/src/HOL/Isar_examples/Cantor.thy Fri Oct 08 15:08:47 1999 +0200 +++ b/src/HOL/Isar_examples/Cantor.thy Fri Oct 08 15:09:14 1999 +0200 @@ -6,15 +6,16 @@ chapter of "Isabelle's Object-Logics" (Larry Paulson). *) -header {* More classical proofs: Cantor's Theorem *}; +header {* Cantor's Theorem *}; theory Cantor = Main:; text {* Cantor's Theorem states that every set has more subsets than it has - elements. It has become a favourite basic example in higher-order logic - since it is so easily expressed: \[\all{f::\alpha \To \alpha \To \idt{bool}} - \ex{S::\alpha \To \idt{bool}} \all{x::\alpha}. f \ap x \not= S\] + elements. It has become a favorite basic example in pure + higher-order logic since it is so easily expressed: \[\all{f::\alpha + \To \alpha \To \idt{bool}} \ex{S::\alpha \To \idt{bool}} + \all{x::\alpha}. f \ap x \not= S\] Viewing types as sets, $\alpha \To \idt{bool}$ represents the powerset of $\alpha$. This version of the theorem states that for every function from diff -r 4c69318e6a6d -r 8ee919e42174 src/HOL/Isar_examples/Group.thy --- a/src/HOL/Isar_examples/Group.thy Fri Oct 08 15:08:47 1999 +0200 +++ b/src/HOL/Isar_examples/Group.thy Fri Oct 08 15:09:14 1999 +0200 @@ -11,7 +11,8 @@ text {* We define an axiomatic type class of general groups over signature - $({\times}, \idt{one}, \idt{inv})$. + $({\times} :: \alpha \To \alpha \To \alpha, \idt{one} :: \alpha, + \idt{inv} :: \alpha \To \alpha)$. *}; consts diff -r 4c69318e6a6d -r 8ee919e42174 src/HOL/Isar_examples/MultisetOrder.thy --- a/src/HOL/Isar_examples/MultisetOrder.thy Fri Oct 08 15:08:47 1999 +0200 +++ b/src/HOL/Isar_examples/MultisetOrder.thy Fri Oct 08 15:09:14 1999 +0200 @@ -25,12 +25,14 @@ let ?case1 = "?case1 {(N, M). ?R N M}"; assume "(N, M0 + {#a#}) : {(N, M). ?R N M}"; - hence "EX a' M0' K. M0 + {#a#} = M0' + {#a'#} & N = M0' + K & ?r K a'"; by simp; + hence "EX a' M0' K. + M0 + {#a#} = M0' + {#a'#} & N = M0' + K & ?r K a'"; by simp; thus "?case1 | ?case2"; proof (elim exE conjE); fix a' M0' K; assume N: "N = M0' + K" and r: "?r K a'"; assume "M0 + {#a#} = M0' + {#a'#}"; - hence "M0 = M0' & a = a' | (EX K'. M0 = K' + {#a'#} & M0' = K' + {#a#})"; + hence "M0 = M0' & a = a' | + (EX K'. M0 = K' + {#a'#} & M0' = K' + {#a#})"; by (simp only: add_eq_conv_ex); thus ?thesis; proof (elim disjE conjE exE); @@ -59,14 +61,14 @@ {{; fix M M0 a; - assume wf_hyp: "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)" - and M0: "M0 : ?W" + assume M0: "M0 : ?W" + and wf_hyp: "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)" and acc_hyp: "ALL M. (M, M0) : ?R --> M + {#a#} : ?W"; have "M0 + {#a#} : ?W"; proof (rule accI [of "M0 + {#a#}"]); fix N; assume "(N, M0 + {#a#}) : ?R"; hence "((EX M. (M, M0) : ?R & N = M + {#a#}) | - (EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K))"; + (EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K))"; by (rule less_add); thus "N : ?W"; proof (elim exE disjE conjE); @@ -88,7 +90,7 @@ proof; assume a: "ALL b. elem (K + {#x#}) b --> (b, a) : r"; hence "(x, a) : r"; by simp; - with wf_hyp [RS spec]; have b: "ALL M:?W. M + {#x#} : ?W"; ..; + with wf_hyp; have b: "ALL M:?W. M + {#x#} : ?W"; by blast; from a hyp; have "M0 + K : ?W"; by simp; with b; have "(M0 + K) + {#x#} : ?W"; ..; @@ -114,11 +116,13 @@ fix M a; assume "M : ?W"; from wf; have "ALL M:?W. M + {#a#} : ?W"; proof (rule wf_induct [of r]); - fix a; assume "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)"; + fix a; + assume "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)"; show "ALL M:?W. M + {#a#} : ?W"; proof; fix M; assume "M : ?W"; - thus "M + {#a#} : ?W"; by (rule acc_induct) (rule tedious_reasoning); + thus "M + {#a#} : ?W"; + by (rule acc_induct) (rule tedious_reasoning); qed; qed; thus "M + {#a#} : ?W"; ..; diff -r 4c69318e6a6d -r 8ee919e42174 src/HOL/Isar_examples/MutilatedCheckerboard.thy --- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy Fri Oct 08 15:08:47 1999 +0200 +++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy Fri Oct 08 15:09:14 1999 +0200 @@ -23,13 +23,15 @@ inductive "tiling A" intrs empty: "{} : tiling A" - Un: "[| a : A; t : tiling A; a <= - t |] ==> a Un t : tiling A"; + Un: "[| a : A; t : tiling A; a <= - t |] + ==> a Un t : tiling A"; -text "The union of two disjoint tilings is a tiling"; +text "The union of two disjoint tilings is a tiling."; lemma tiling_Un: - "t : tiling A --> u : tiling A --> t Int u = {} --> t Un u : tiling A"; + "t : tiling A --> u : tiling A --> t Int u = {} + --> t Un u : tiling A"; proof; assume "t : tiling A" (is "_ : ?T"); thus "u : ?T --> t Int u = {} --> t Un u : ?T" (is "?P t"); @@ -119,7 +121,8 @@ horiz: "{(i, j), (i, j + 1)} : domino" vertl: "{(i, j), (i + 1, j)} : domino"; -lemma dominoes_tile_row: "{i} Times below (2 * n) : tiling domino" +lemma dominoes_tile_row: + "{i} Times below (2 * n) : tiling domino" (is "?P n" is "?B n : ?T"); proof (induct n); show "?P 0"; by (simp add: below_0 tiling.empty); @@ -268,9 +271,11 @@ note [simp] = evnodd_iff evnodd_empty evnodd_insert evnodd_Diff; have "card (?e ?t'' 0) < card (?e ?t' 0)"; proof -; - have "card (?e ?t' 0 - {(2 * m + 1, 2 * n + 1)}) < card (?e ?t' 0)"; + have "card (?e ?t' 0 - {(2 * m + 1, 2 * n + 1)}) + < card (?e ?t' 0)"; proof (rule card_Diff1_less); - show "finite (?e ?t' 0)"; by (rule finite_subset, rule fin) force; + show "finite (?e ?t' 0)"; + by (rule finite_subset, rule fin) force; show "(2 * m + 1, 2 * n + 1) : ?e ?t' 0"; by simp; qed; thus ?thesis; by simp; @@ -282,7 +287,8 @@ by (rule card_Diff1_less); thus ?thesis; by simp; qed; - also; from t; have "... = card (?e ?t 1)"; by (rule tiling_domino_01); + also; from t; have "... = card (?e ?t 1)"; + by (rule tiling_domino_01); also; have "?e ?t 1 = ?e ?t'' 1"; by simp; also; from t''; have "card ... = card (?e ?t'' 0)"; by (rule tiling_domino_01 [RS sym]); diff -r 4c69318e6a6d -r 8ee919e42174 src/HOL/Isar_examples/ROOT.ML --- a/src/HOL/Isar_examples/ROOT.ML Fri Oct 08 15:08:47 1999 +0200 +++ b/src/HOL/Isar_examples/ROOT.ML Fri Oct 08 15:09:14 1999 +0200 @@ -6,8 +6,8 @@ *) time_use_thy "BasicLogic"; +time_use_thy "Cantor"; time_use_thy "Peirce"; -time_use_thy "Cantor"; time_use_thy "ExprCompiler"; time_use_thy "Group"; time_use_thy "Summation"; diff -r 4c69318e6a6d -r 8ee919e42174 src/HOL/Isar_examples/Summation.thy --- a/src/HOL/Isar_examples/Summation.thy Fri Oct 08 15:08:47 1999 +0200 +++ b/src/HOL/Isar_examples/Summation.thy Fri Oct 08 15:09:14 1999 +0200 @@ -22,13 +22,16 @@ "sum f (Suc n) = f n + sum f n"; syntax - "_SUM" :: "idt => nat => nat => nat" ("SUM _ < _. _" [0, 0, 10] 10); + "_SUM" :: "idt => nat => nat => nat" + ("SUM _ < _. _" [0, 0, 10] 10); translations "SUM i < k. b" == "sum (%i. b) k"; subsection {* Summation laws *}; +verbatim {* \begin{comment} *}; + (* FIXME binary arithmetic does not yet work here *) syntax @@ -43,8 +46,11 @@ theorems [simp] = add_mult_distrib add_mult_distrib2 mult_ac; +verbatim {* \end{comment} *}; -theorem sum_of_naturals: "2 * (SUM i < n + 1. i) = n * (n + 1)" + +theorem sum_of_naturals: + "2 * (SUM i < n + 1. i) = n * (n + 1)" (is "?P n" is "?S n = _"); proof (induct n); show "?P 0"; by simp; @@ -56,7 +62,8 @@ finally; show "?P (Suc n)"; by simp; qed; -theorem sum_of_odds: "(SUM i < n. 2 * i + 1) = n^2" +theorem sum_of_odds: + "(SUM i < n. 2 * i + 1) = n^2" (is "?P n" is "?S n = _"); proof (induct n); show "?P 0"; by simp; @@ -77,12 +84,13 @@ fix n; have "?S (n + 1) = ?S n + 6 * (n + 1)^2"; by simp; also; assume "?S n = n * (n + 1) * (2 * n + 1)"; - also; have "... + 6 * (n + 1)^2 = (n + 1) * (n + 2) * (2 * (n + 1) + 1)"; - by simp; + also; have "... + 6 * (n + 1)^2 = + (n + 1) * (n + 2) * (2 * (n + 1) + 1)"; by simp; finally; show "?P (Suc n)"; by simp; qed; -theorem sum_of_cubes: "4 * (SUM i < n + 1. i^3) = (n * (n + 1))^2" +theorem sum_of_cubes: + "4 * (SUM i < n + 1. i^3) = (n * (n + 1))^2" (is "?P n" is "?S n = _"); proof (induct n); show "?P 0"; by simp; diff -r 4c69318e6a6d -r 8ee919e42174 src/HOL/Isar_examples/W_correct.thy --- a/src/HOL/Isar_examples/W_correct.thy Fri Oct 08 15:08:47 1999 +0200 +++ b/src/HOL/Isar_examples/W_correct.thy Fri Oct 08 15:09:14 1999 +0200 @@ -6,7 +6,7 @@ Based upon HOL/W0 by Dieter Nazareth and Tobias Nipkow. *) -header {* Correctness of Milner's type inference algorithm~W (let-free version) *}; +header {* Milner's type inference algorithm~W (let-free version) *}; theory W_correct = Main + Type:; @@ -47,8 +47,10 @@ hence "n < length (map ($ s) a)"; by simp; hence "map ($ s) a |- Var n :: map ($ s) a ! n"; by (rule has_type.VarI); - also; have "map ($ s) a ! n = $ s (a ! n)"; by (rule nth_map); - also; have "map ($ s) a = $ s a"; by (simp only: app_subst_list); (* FIXME unfold fails!? *) + also; have "map ($ s) a ! n = $ s (a ! n)"; + by (rule nth_map); + also; have "map ($ s) a = $ s a"; + by (simp only: app_subst_list); (* FIXME unfold fails!? *) finally; show "?P a (Var n) (a ! n)"; .; next; fix a e t1 t2; @@ -114,10 +116,11 @@ proof (intro allI impI); fix a s t m n; assume "Ok (s, t, m) = W (App e1 e2) a n"; hence "EX s1 t1 n1 s2 t2 n2 u. - s = $ u o $ s2 o s1 & t = u n2 & - mgu ($ s2 t1) (t2 -> TVar n2) = Ok u & - W e2 ($ s1 a) n1 = Ok (s2, t2, n2) & - W e1 a n = Ok (s1, t1, n1)"; by (rule rev_mp) (simp, force); (* FIXME force fails !??*) + s = $ u o $ s2 o s1 & t = u n2 & + mgu ($ s2 t1) (t2 -> TVar n2) = Ok u & + W e2 ($ s1 a) n1 = Ok (s2, t2, n2) & + W e1 a n = Ok (s1, t1, n1)"; + by (rule rev_mp) (simp, force); (* FIXME force fails !??*) thus "$ s a |- App e1 e2 :: t"; proof (elim exE conjE); fix s1 t1 n1 s2 t2 n2 u; @@ -132,7 +135,8 @@ by (simp add: subst_comp_tel o_def); show "$s a |- e1 :: $ u t2 -> t"; proof -; - from hyp1 W1_ok [RS sym]; have "$ s1 a |- e1 :: t1"; by blast; + from hyp1 W1_ok [RS sym]; have "$ s1 a |- e1 :: t1"; + by blast; hence "$ u ($ s2 ($ s1 a)) |- e1 :: $ u ($ s2 t1)"; by (intro has_type_subst_closed); with s' t mgu_ok; show ?thesis; by simp; diff -r 4c69318e6a6d -r 8ee919e42174 src/HOL/Isar_examples/document/root.tex --- a/src/HOL/Isar_examples/document/root.tex Fri Oct 08 15:08:47 1999 +0200 +++ b/src/HOL/Isar_examples/document/root.tex Fri Oct 08 15:09:14 1999 +0200 @@ -3,7 +3,6 @@ \hyphenation{Isabelle} - \begin{document} \title{Miscellaneous Isabelle/Isar examples for Higher-Order Logic} @@ -18,7 +17,6 @@ \end{abstract} \tableofcontents - \input{session} \end{document} diff -r 4c69318e6a6d -r 8ee919e42174 src/HOL/Isar_examples/document/style.tex --- a/src/HOL/Isar_examples/document/style.tex Fri Oct 08 15:08:47 1999 +0200 +++ b/src/HOL/Isar_examples/document/style.tex Fri Oct 08 15:09:14 1999 +0200 @@ -2,7 +2,7 @@ %% $Id$ \documentclass[11pt,a4paper]{article} -\usepackage{isabelle,pdfsetup} +\usepackage{comment,isabelle,pdfsetup} \renewcommand{\isamarkupheader}[1]{\section{#1}} \parindent 0pt \parskip 0.5ex diff -r 4c69318e6a6d -r 8ee919e42174 src/Pure/Thy/latex.ML --- a/src/Pure/Thy/latex.ML Fri Oct 08 15:08:47 1999 +0200 +++ b/src/Pure/Thy/latex.ML Fri Oct 08 15:09:14 1999 +0200 @@ -26,25 +26,16 @@ "%" => "\\%" | "#" => "\\#" | "_" => "\\_" | - "{" => "{\\textbraceleft}" | - "}" => "{\\textbraceright}" | - "~" => "{\\textasciitilde}" | - "^" => "{\\textasciicircum}" | + "{" => "{\\isabraceleft}" | + "}" => "{\\isabraceright}" | + "~" => "{\\isatilde}" | + "^" => "{\\isacircum}" | "\"" => "{\"}" | - "\\" => "\\verb,\\," | + "\\" => "{\\isabackslash}" | c => c; -val output_chr' = fn - "\\" => "{\\textbackslash}" | - "|" => "{\\textbar}" | - "<" => "{\\textless}" | - ">" => "{\\textgreater}" | - c => output_chr c; - - (* FIXME replace \ etc. *) val output_sym = implode o map output_chr o explode; -val output_sym' = implode o map output_chr' o explode; (* token output *) @@ -63,14 +54,18 @@ fun output_tok (Basic tok) = let val s = T.val_of tok in if invisible_token tok then "" - else if T.is_kind T.Command tok then "\\isacommand{" ^ output_sym' s ^ "}" - else if T.is_kind T.Keyword tok then "\\isakeyword{" ^ output_sym' s ^ "}" + else if T.is_kind T.Command tok then + if s = "{{" then "{\\isabeginblock}" + else if s = "}}" then "{\\isaendblock}" + else "\\isacommand{" ^ output_sym s ^ "}" + else if T.is_kind T.Keyword tok andalso Syntax.is_identifier s then + "\\isakeyword{" ^ output_sym s ^ "}" else if T.is_kind T.String tok then output_sym (quote s) else if T.is_kind T.Verbatim tok then output_sym (enclose "{*" "*}" s) else output_sym s end - | output_tok (Markup (cmd, arg)) = "\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks arg ^ "}\n" - | output_tok (Verbatim txt) = "\n" ^ txt ^ "\n"; + | output_tok (Markup (cmd, txt)) = "\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks txt ^ "}\n" + | output_tok (Verbatim txt) = "\n" ^ strip_blanks txt ^ "\n"; val output_tokens = implode o map output_tok;