# HG changeset patch # User wenzelm # Date 966681879 -7200 # Node ID b9cf6801f3da7d1ae14167d6224f7b8743b65aef # Parent 97d6d0a72d35065e287bf6b6442c09dd5981cfbb tuned; diff -r 97d6d0a72d35 -r b9cf6801f3da src/HOL/Induct/Multiset.thy --- a/src/HOL/Induct/Multiset.thy Sat Aug 19 12:44:20 2000 +0200 +++ b/src/HOL/Induct/Multiset.thy Sat Aug 19 12:44:39 2000 +0200 @@ -5,8 +5,6 @@ A definitional theory of multisets, including a wellfoundedness proof for the multiset order. -use_thy"Multiset"; - *) Multiset = Multiset0 + Acc + diff -r 97d6d0a72d35 -r b9cf6801f3da src/HOL/Isar_examples/BasicLogic.thy --- a/src/HOL/Isar_examples/BasicLogic.thy Sat Aug 19 12:44:20 2000 +0200 +++ b/src/HOL/Isar_examples/BasicLogic.thy Sat Aug 19 12:44:39 2000 +0200 @@ -221,7 +221,7 @@ qed; text {* - We can still push forward reasoning a bit further, even at the risk + We can still push forward-reasoning a bit further, even at the risk of getting ridiculous. Note that we force the initial proof step to do nothing here, by referring to the ``-'' proof method. *}; diff -r 97d6d0a72d35 -r b9cf6801f3da src/HOL/Isar_examples/ExprCompiler.thy --- a/src/HOL/Isar_examples/ExprCompiler.thy Sat Aug 19 12:44:20 2000 +0200 +++ b/src/HOL/Isar_examples/ExprCompiler.thy Sat Aug 19 12:44:39 2000 +0200 @@ -169,7 +169,8 @@ exec (Const val # xs @ ys) s env"; by simp; also; have "... = exec (xs @ ys) (val # s) env"; by simp; - also; from hyp; have "... = exec ys (exec xs (val # s) env) env"; ..; + also; from hyp; + have "... = exec ys (exec xs (val # s) env) env"; ..; also; have "... = exec ys (exec (Const val # xs) s env) env"; by simp; finally; show "?Q s"; .; @@ -188,7 +189,8 @@ exec (xs @ ys) (fun (hd s) (hd (tl s)) # (tl (tl s))) env"; by simp; also; from hyp; have "... = - exec ys (exec xs (fun (hd s) (hd (tl s)) # tl (tl s)) env) env"; ..; + exec ys (exec xs (fun (hd s) (hd (tl s)) # tl (tl s)) env) env"; + ..; also; have "... = exec ys (exec (Apply fun # xs) s env) env"; by simp; finally; show "?Q s"; .; qed; @@ -198,7 +200,8 @@ theorem correctness: "execute (compile e) env = eval e env"; proof -; have exec_compile: - "ALL stack. exec (compile e) stack env = eval e env # stack" (is "?P e"); + "ALL stack. exec (compile e) stack env = eval e env # stack" + (is "?P e"); proof (induct e); fix adr; show "?P (Variable adr)" (is "ALL s. ?Q s"); proof; @@ -217,15 +220,18 @@ proof; fix s; have "exec (compile (Binop fun e1 e2)) s env = exec (compile e2 @ compile e1 @ [Apply fun]) s env"; by simp; - also; have "... = - exec [Apply fun] (exec (compile e1) (exec (compile e2) s env) env) env"; + also; have "... = exec [Apply fun] + (exec (compile e1) (exec (compile e2) s env) env) env"; by (simp only: exec_append); - also; from hyp2; have "exec (compile e2) s env = eval e2 env # s"; ..; - also; from hyp1; have "exec (compile e1) ... env = eval e1 env # ..."; ..; + also; from hyp2; + have "exec (compile e2) s env = eval e2 env # s"; ..; + also; from hyp1; + have "exec (compile e1) ... env = eval e1 env # ..."; ..; also; have "exec [Apply fun] ... env = fun (hd ...) (hd (tl ...)) # (tl (tl ...))"; by simp; also; have "... = fun (eval e1 env) (eval e2 env) # s"; by simp; - also; have "fun (eval e1 env) (eval e2 env) = eval (Binop fun e1 e2) env"; + also; have "fun (eval e1 env) (eval e2 env) = + eval (Binop fun e1 e2) env"; by simp; finally; show "?Q s"; .; qed; @@ -233,7 +239,8 @@ have "execute (compile e) env = hd (exec (compile e) [] env)"; by (simp add: execute_def); - also; from exec_compile; have "exec (compile e) [] env = [eval e env]"; ..; + also; from exec_compile; + have "exec (compile e) [] env = [eval e env]"; ..; also; have "hd ... = eval e env"; by simp; finally; show ?thesis; .; qed; diff -r 97d6d0a72d35 -r b9cf6801f3da src/HOL/Isar_examples/Fibonacci.thy --- a/src/HOL/Isar_examples/Fibonacci.thy Sat Aug 19 12:44:20 2000 +0200 +++ b/src/HOL/Isar_examples/Fibonacci.thy Sat Aug 19 12:44:39 2000 +0200 @@ -39,7 +39,7 @@ text {* Alternative induction rule. *}; theorem fib_induct: -"[| P 0; P 1; !!n. [| P (n + 1); P n |] ==> P (n + 2) |] ==> P n"; + "P 0 ==> P 1 ==> (!!n. P (n + 1) ==> P n ==> P (n + 2)) ==> P n"; by (induct rule: fib.induct, simp+); @@ -48,10 +48,11 @@ text {* A few laws taken from \cite{Concrete-Math}. *}; -lemma fib_add: +lemma fib_add: "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n" - (is "?P n"); -proof (induct ?P n rule: fib_induct) -- {* see \cite[page 280]{Concrete-Math} *}; + (is "?P n") + -- {* see \cite[page 280]{Concrete-Math} *}; +proof (induct ?P n rule: fib_induct); show "?P 0"; by simp; show "?P 1"; by simp; fix n; @@ -70,11 +71,11 @@ qed; lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (n + 1)) = 1" (is "?P n"); -proof (induct ?P n rule: fib_induct); +proof (induct ?P n rule: fib_induct); show "?P 0"; by simp; show "?P 1"; by simp; - fix n; - have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"; + fix n; + have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"; by simp; also; have "gcd (fib (n + 2), ...) = gcd (fib (n + 2), fib (n + 1))"; by (simp only: gcd_add2); @@ -87,64 +88,65 @@ lemma gcd_mult_add: "0 < n ==> gcd (n * k + m, n) = gcd (m, n)"; proof -; assume "0 < n"; - hence "gcd (n * k + m, n) = gcd (n, m mod n)"; + hence "gcd (n * k + m, n) = gcd (n, m mod n)"; by (simp add: gcd_non_0 add_commute); also; have "... = gcd (m, n)"; by (simp! add: gcd_non_0); finally; show ?thesis; .; qed; -lemma gcd_fib_add: "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)"; +lemma gcd_fib_add: "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)"; proof (cases m); assume "m = 0"; thus ?thesis; by simp; next; - fix k; assume "m = Suc k"; + fix k; assume "m = Suc k"; hence "gcd (fib m, fib (n + m)) = gcd (fib (n + k + 1), fib (k + 1))"; by (simp add: gcd_commute); - also; have "fib (n + k + 1) + also; have "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"; by (rule fib_add); - also; have "gcd (..., fib (k + 1)) = gcd (fib k * fib n, fib (k + 1))"; + also; have "gcd (..., fib (k + 1)) = gcd (fib k * fib n, fib (k + 1))"; by (simp add: gcd_mult_add); - also; have "... = gcd (fib n, fib (k + 1))"; + also; have "... = gcd (fib n, fib (k + 1))"; by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel); - also; have "... = gcd (fib m, fib n)"; + also; have "... = gcd (fib m, fib n)"; by (simp! add: gcd_commute); finally; show ?thesis; .; qed; -lemma gcd_fib_diff: +lemma gcd_fib_diff: "m <= n ==> gcd (fib m, fib (n - m)) = gcd (fib m, fib n)"; -proof -; +proof -; assume "m <= n"; - have "gcd (fib m, fib (n - m)) = gcd (fib m, fib (n - m + m))"; + have "gcd (fib m, fib (n - m)) = gcd (fib m, fib (n - m + m))"; by (simp add: gcd_fib_add); - also; have "n - m + m = n"; by (simp!); + also; have "n - m + m = n"; by (simp!); finally; show ?thesis; .; qed; -lemma if_cases: (* FIXME move to HOL.thy (!?) *) - "[| Q ==> P x; ~ Q ==> P y |] ==> P (if Q then x else y)"; by simp; - -lemma gcd_fib_mod: +lemma gcd_fib_mod: "0 < m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"; proof (induct n rule: less_induct); - fix n; + fix n; assume m: "0 < m" - and hyp: "ALL ma. ma < n + and hyp: "ALL ma. ma < n --> gcd (fib m, fib (ma mod m)) = gcd (fib m, fib ma)"; have "n mod m = (if n < m then n else (n - m) mod m)"; by (rule mod_if); also; have "gcd (fib m, fib ...) = gcd (fib m, fib n)"; - proof (rule if_cases); - assume "~ n < m"; hence m_le_n: "m <= n"; by simp; + proof cases; + assume "n < m"; thus ?thesis; by simp; + next; + assume not_lt: "~ n < m"; hence le: "m <= n"; by simp; have "n - m < n"; by (simp! add: diff_less); with hyp; have "gcd (fib m, fib ((n - m) mod m)) = gcd (fib m, fib (n - m))"; by simp; - also; from m_le_n; have "... = gcd (fib m, fib n)"; + also; from le; have "... = gcd (fib m, fib n)"; by (rule gcd_fib_diff); - finally; show "gcd (fib m, fib ((n - m) mod m)) = gcd (fib m, fib n)"; .; - qed simp; + finally; have "gcd (fib m, fib ((n - m) mod m)) = + gcd (fib m, fib n)"; .; + with not_lt; show ?thesis; by simp; + qed; finally; show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"; .; qed; diff -r 97d6d0a72d35 -r b9cf6801f3da src/HOL/Isar_examples/MultisetOrder.thy --- a/src/HOL/Isar_examples/MultisetOrder.thy Sat Aug 19 12:44:20 2000 +0200 +++ b/src/HOL/Isar_examples/MultisetOrder.thy Sat Aug 19 12:44:39 2000 +0200 @@ -25,11 +25,11 @@ lemma less_add: "(N, M0 + {#a#}) : mult1 r ==> (EX M. (M, M0) : mult1 r & N = M + {#a#}) | - (EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K)" + (EX K. (ALL b. b :# K --> (b, a) : r) & N = M0 + K)" (concl is "?case1 (mult1 r) | ?case2"); proof (unfold mult1_def); - let ?r = "\\K a. ALL b. elem K b --> (b, a) : r"; - let ?R = "\\N M. EX a M0 K. M = M0 + {#a#} & N = M0 + K & ?r K a"; + let ?r = "\K a. ALL b. b :# K --> (b, a) : r"; + let ?R = "\N M. EX a M0 K. M = M0 + {#a#} & N = M0 + K & ?r K a"; let ?case1 = "?case1 {(N, M). ?R N M}"; assume "(N, M0 + {#a#}) : {(N, M). ?R N M}"; @@ -77,7 +77,7 @@ 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. b :# K --> (b, a) : r) & N = M0 + K))"; by (rule less_add); thus "N : ?W"; proof (elim exE disjE conjE); @@ -88,7 +88,7 @@ next; fix K; assume N: "N = M0 + K"; - assume "ALL b. elem K b --> (b, a) : r"; + assume "ALL b. b :# K --> (b, a) : r"; have "?this --> M0 + K : ?W" (is "?P K"); proof (induct K); from M0; have "M0 + {#} : ?W"; by simp; @@ -97,7 +97,7 @@ fix K x; assume hyp: "?P K"; show "?P (K + {#x#})"; proof; - assume a: "ALL b. elem (K + {#x#}) b --> (b, a) : r"; + assume a: "ALL b. b :# (K + {#x#}) --> (b, a) : r"; hence "(x, a) : r"; by simp; with wf_hyp; have b: "ALL M:?W. M + {#x#} : ?W"; by blast; diff -r 97d6d0a72d35 -r b9cf6801f3da src/HOL/Isar_examples/MutilatedCheckerboard.thy --- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy Sat Aug 19 12:44:20 2000 +0200 +++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy Sat Aug 19 12:44:39 2000 +0200 @@ -69,7 +69,8 @@ by (simp add: below_def less_Suc_eq) blast; lemma Sigma_Suc2: - "m = n + 2 ==> A <*> below m = (A <*> {n}) Un (A <*> {n + 1}) Un (A <*> below n)"; + "m = n + 2 ==> A <*> below m = + (A <*> {n}) Un (A <*> {n + 1}) Un (A <*> below n)"; by (auto simp add: below_def) arith; lemmas Sigma_Suc = Sigma_Suc1 Sigma_Suc2; @@ -112,7 +113,7 @@ subsection {* Dominoes *}; consts - domino :: "(nat * nat) set set"; + domino :: "(nat * nat) set set"; inductive domino intros diff -r 97d6d0a72d35 -r b9cf6801f3da src/HOL/Isar_examples/NestedDatatype.thy --- a/src/HOL/Isar_examples/NestedDatatype.thy Sat Aug 19 12:44:20 2000 +0200 +++ b/src/HOL/Isar_examples/NestedDatatype.thy Sat Aug 19 12:44:39 2000 +0200 @@ -32,7 +32,8 @@ subst_term_list f1 (subst_term_list f2 ts)"; by (induct t and ts rule: term.induct) simp_all; -lemma "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)"; +lemma "subst_term (subst_term f1 o f2) t = + subst_term f1 (subst_term f2 t)"; proof -; let "?P t" = ?thesis; let ?Q = "\\ts. subst_term_list (subst_term f1 o f2) ts = @@ -55,7 +56,8 @@ subsection {* Alternative induction *}; theorem term_induct' [case_names Var App]: - "(!!a. P (Var a)) ==> (!!b ts. list_all P ts ==> P (App b ts)) ==> P t"; + "(!!a. P (Var a)) ==> + (!!b ts. list_all P ts ==> P (App b ts)) ==> P t"; proof -; assume var: "!!a. P (Var a)"; assume app: "!!b ts. list_all P ts ==> P (App b ts)"; @@ -76,7 +78,7 @@ lemma "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)" (is "?P t"); -proof (induct ?P t rule: term_induct'); +proof (induct (open) ?P t rule: term_induct'); case Var; show "?P (Var a)"; by (simp add: o_def); next; diff -r 97d6d0a72d35 -r b9cf6801f3da src/HOL/Isar_examples/Summation.thy --- a/src/HOL/Isar_examples/Summation.thy Sat Aug 19 12:44:20 2000 +0200 +++ b/src/HOL/Isar_examples/Summation.thy Sat Aug 19 12:44:39 2000 +0200 @@ -153,7 +153,8 @@ show "?P 0"; by (simp add: power_eq_if); fix n; - have "?S (n + 1) = ?S n + #4 * (n + 1)^#3"; by (simp add: power_eq_if distrib); + have "?S (n + 1) = ?S n + #4 * (n + 1)^#3"; + by (simp add: power_eq_if distrib); also; assume "?S n = (n * (n + 1))^2"; also; have "... + #4 * (n + 1)^#3 = ((n + 1) * ((n + 1) + 1))^2"; by (simp add: power_eq_if distrib); diff -r 97d6d0a72d35 -r b9cf6801f3da src/HOL/Isar_examples/W_correct.thy --- a/src/HOL/Isar_examples/W_correct.thy Sat Aug 19 12:44:20 2000 +0200 +++ b/src/HOL/Isar_examples/W_correct.thy Sat Aug 19 12:44:39 2000 +0200 @@ -36,8 +36,8 @@ intros [simp] Var: "n < length a ==> a |- Var n :: a ! n" Abs: "t1#a |- e :: t2 ==> a |- Abs e :: t1 -> t2" - App: "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |] - ==> a |- App e1 e2 :: t1"; + App: "a |- e1 :: t2 -> t1 ==> a |- e2 :: t2 + ==> a |- App e1 e2 :: t1"; text {* Type assigment is closed wrt.\ substitution. *}; @@ -46,7 +46,7 @@ proof -; assume "a |- e :: t"; thus ?thesis (is "?P a e t"); - proof (induct ?P a e t); + proof (induct (open) ?P a e t); case Var; hence "n < length (map ($ s) a)"; by simp; hence "map ($ s) a |- Var n :: map ($ s) a ! n"; diff -r 97d6d0a72d35 -r b9cf6801f3da src/HOL/Isar_examples/document/style.tex --- a/src/HOL/Isar_examples/document/style.tex Sat Aug 19 12:44:20 2000 +0200 +++ b/src/HOL/Isar_examples/document/style.tex Sat Aug 19 12:44:39 2000 +0200 @@ -3,6 +3,7 @@ \documentclass[11pt,a4paper]{article} \usepackage{proof,isabelle,isabellesym,pdfsetup} +\urlstyle{rm} \renewcommand{\isamarkupheader}[1]{\section{#1}} diff -r 97d6d0a72d35 -r b9cf6801f3da src/HOL/Real/HahnBanach/document/root.tex --- a/src/HOL/Real/HahnBanach/document/root.tex Sat Aug 19 12:44:20 2000 +0200 +++ b/src/HOL/Real/HahnBanach/document/root.tex Sat Aug 19 12:44:39 2000 +0200 @@ -4,6 +4,7 @@ \usepackage{latexsym,theorem} \usepackage{isabelle,isabellesym,bbb} \usepackage{pdfsetup} %last one! +\urlstyle{rm} \input{notation} @@ -13,10 +14,8 @@ \pagenumbering{arabic} \title{The Hahn-Banach Theorem for Real Vector Spaces} - \author{Gertrud Bauer \\ \url{http://www.in.tum.de/~bauerg/}} \maketitle -\maketitle \begin{abstract} The Hahn-Banach Theorem is one of the most fundamental results in functional