author wenzelm Sat Aug 19 12:44:39 2000 +0200 (2000-08-19) changeset 9659 b9cf6801f3da parent 9658 97d6d0a72d35 child 9660 80d14ea0e200
tuned;
 src/HOL/Induct/Multiset.thy file | annotate | diff | revisions src/HOL/Isar_examples/BasicLogic.thy file | annotate | diff | revisions src/HOL/Isar_examples/ExprCompiler.thy file | annotate | diff | revisions src/HOL/Isar_examples/Fibonacci.thy file | annotate | diff | revisions src/HOL/Isar_examples/MultisetOrder.thy file | annotate | diff | revisions src/HOL/Isar_examples/MutilatedCheckerboard.thy file | annotate | diff | revisions src/HOL/Isar_examples/NestedDatatype.thy file | annotate | diff | revisions src/HOL/Isar_examples/Summation.thy file | annotate | diff | revisions src/HOL/Isar_examples/W_correct.thy file | annotate | diff | revisions src/HOL/Isar_examples/document/style.tex file | annotate | diff | revisions src/HOL/Real/HahnBanach/document/root.tex file | annotate | diff | revisions
     1.1 --- a/src/HOL/Induct/Multiset.thy	Sat Aug 19 12:44:20 2000 +0200
1.2 +++ b/src/HOL/Induct/Multiset.thy	Sat Aug 19 12:44:39 2000 +0200
1.3 @@ -5,8 +5,6 @@
1.4
1.5  A definitional theory of multisets,
1.6  including a wellfoundedness proof for the multiset order.
1.7 -use_thy"Multiset";
1.8 -
1.9  *)
1.10
1.11  Multiset = Multiset0 + Acc +

     2.1 --- a/src/HOL/Isar_examples/BasicLogic.thy	Sat Aug 19 12:44:20 2000 +0200
2.2 +++ b/src/HOL/Isar_examples/BasicLogic.thy	Sat Aug 19 12:44:39 2000 +0200
2.3 @@ -221,7 +221,7 @@
2.4  qed;
2.5
2.6  text {*
2.7 - We can still push forward reasoning a bit further, even at the risk
2.8 + We can still push forward-reasoning a bit further, even at the risk
2.9   of getting ridiculous.  Note that we force the initial proof step to
2.10   do nothing here, by referring to the -'' proof method.
2.11  *};

     3.1 --- a/src/HOL/Isar_examples/ExprCompiler.thy	Sat Aug 19 12:44:20 2000 +0200
3.2 +++ b/src/HOL/Isar_examples/ExprCompiler.thy	Sat Aug 19 12:44:39 2000 +0200
3.3 @@ -169,7 +169,8 @@
3.4            exec (Const val # xs @ ys) s env";
3.5          by simp;
3.6        also; have "... = exec (xs @ ys) (val # s) env"; by simp;
3.7 -      also; from hyp; have "... = exec ys (exec xs (val # s) env) env"; ..;
3.8 +      also; from hyp;
3.9 +        have "... = exec ys (exec xs (val # s) env) env"; ..;
3.10        also; have "... = exec ys (exec (Const val # xs) s env) env";
3.11          by simp;
3.12        finally; show "?Q s"; .;
3.13 @@ -188,7 +189,8 @@
3.14            exec (xs @ ys) (fun (hd s) (hd (tl s)) # (tl (tl s))) env";
3.15          by simp;
3.16        also; from hyp; have "... =
3.17 -        exec ys (exec xs (fun (hd s) (hd (tl s)) # tl (tl s)) env) env"; ..;
3.18 +        exec ys (exec xs (fun (hd s) (hd (tl s)) # tl (tl s)) env) env";
3.19 +        ..;
3.20        also; have "... = exec ys (exec (Apply fun # xs) s env) env"; by simp;
3.21        finally; show "?Q s"; .;
3.22      qed;
3.23 @@ -198,7 +200,8 @@
3.24  theorem correctness: "execute (compile e) env = eval e env";
3.25  proof -;
3.26    have exec_compile:
3.27 -  "ALL stack. exec (compile e) stack env = eval e env # stack" (is "?P e");
3.28 +    "ALL stack. exec (compile e) stack env = eval e env # stack"
3.29 +    (is "?P e");
3.30    proof (induct e);
3.31      fix adr; show "?P (Variable adr)" (is "ALL s. ?Q s");
3.32      proof;
3.33 @@ -217,15 +220,18 @@
3.34      proof;
3.35        fix s; have "exec (compile (Binop fun e1 e2)) s env
3.36          = exec (compile e2 @ compile e1 @ [Apply fun]) s env"; by simp;
3.37 -      also; have "... =
3.38 -          exec [Apply fun] (exec (compile e1) (exec (compile e2) s env) env) env";
3.39 +      also; have "... = exec [Apply fun]
3.40 +          (exec (compile e1) (exec (compile e2) s env) env) env";
3.41          by (simp only: exec_append);
3.42 -      also; from hyp2; have "exec (compile e2) s env = eval e2 env # s"; ..;
3.43 -      also; from hyp1; have "exec (compile e1) ... env = eval e1 env # ..."; ..;
3.44 +      also; from hyp2;
3.45 +        have "exec (compile e2) s env = eval e2 env # s"; ..;
3.46 +      also; from hyp1;
3.47 +        have "exec (compile e1) ... env = eval e1 env # ..."; ..;
3.48        also; have "exec [Apply fun] ... env =
3.49          fun (hd ...) (hd (tl ...)) # (tl (tl ...))"; by simp;
3.50        also; have "... = fun (eval e1 env) (eval e2 env) # s"; by simp;
3.51 -      also; have "fun (eval e1 env) (eval e2 env) = eval (Binop fun e1 e2) env";
3.52 +      also; have "fun (eval e1 env) (eval e2 env) =
3.53 +          eval (Binop fun e1 e2) env";
3.54          by simp;
3.55        finally; show "?Q s"; .;
3.56      qed;
3.57 @@ -233,7 +239,8 @@
3.58
3.59    have "execute (compile e) env = hd (exec (compile e) [] env)";
3.61 -  also; from exec_compile; have "exec (compile e) [] env = [eval e env]"; ..;
3.62 +  also; from exec_compile;
3.63 +    have "exec (compile e) [] env = [eval e env]"; ..;
3.64    also; have "hd ... = eval e env"; by simp;
3.65    finally; show ?thesis; .;
3.66  qed;

     4.1 --- a/src/HOL/Isar_examples/Fibonacci.thy	Sat Aug 19 12:44:20 2000 +0200
4.2 +++ b/src/HOL/Isar_examples/Fibonacci.thy	Sat Aug 19 12:44:39 2000 +0200
4.3 @@ -39,7 +39,7 @@
4.4  text {* Alternative induction rule. *};
4.5
4.6  theorem fib_induct:
4.7 -"[| P 0; P 1; !!n. [| P (n + 1); P n |] ==> P (n + 2) |] ==> P n";
4.8 +    "P 0 ==> P 1 ==> (!!n. P (n + 1) ==> P n ==> P (n + 2)) ==> P n";
4.9    by (induct rule: fib.induct, simp+);
4.10
4.11
4.12 @@ -48,10 +48,11 @@
4.13
4.14  text {* A few laws taken from \cite{Concrete-Math}. *};
4.15
4.18    "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"
4.19 -  (is "?P n");
4.20 -proof (induct ?P n rule: fib_induct) -- {* see \cite[page 280]{Concrete-Math} *};
4.21 +  (is "?P n")
4.22 +  -- {* see \cite[page 280]{Concrete-Math} *};
4.23 +proof (induct ?P n rule: fib_induct);
4.24    show "?P 0"; by simp;
4.25    show "?P 1"; by simp;
4.26    fix n;
4.27 @@ -70,11 +71,11 @@
4.28  qed;
4.29
4.30  lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (n + 1)) = 1" (is "?P n");
4.31 -proof (induct ?P n rule: fib_induct);
4.32 +proof (induct ?P n rule: fib_induct);
4.33    show "?P 0"; by simp;
4.34    show "?P 1"; by simp;
4.35 -  fix n;
4.36 -  have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)";
4.37 +  fix n;
4.38 +  have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)";
4.39      by simp;
4.40    also; have "gcd (fib (n + 2), ...) = gcd (fib (n + 2), fib (n + 1))";
4.42 @@ -87,64 +88,65 @@
4.43  lemma gcd_mult_add: "0 < n ==> gcd (n * k + m, n) = gcd (m, n)";
4.44  proof -;
4.45    assume "0 < n";
4.46 -  hence "gcd (n * k + m, n) = gcd (n, m mod n)";
4.47 +  hence "gcd (n * k + m, n) = gcd (n, m mod n)";
4.49    also; have "... = gcd (m, n)"; by (simp! add: gcd_non_0);
4.50    finally; show ?thesis; .;
4.51  qed;
4.52
4.53 -lemma gcd_fib_add: "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)";
4.54 +lemma gcd_fib_add: "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)";
4.55  proof (cases m);
4.56    assume "m = 0";
4.57    thus ?thesis; by simp;
4.58  next;
4.59 -  fix k; assume "m = Suc k";
4.60 +  fix k; assume "m = Suc k";
4.61    hence "gcd (fib m, fib (n + m)) = gcd (fib (n + k + 1), fib (k + 1))";
4.63 -  also; have "fib (n + k + 1)
4.64 +  also; have "fib (n + k + 1)
4.65      = fib (k + 1) * fib (n + 1) + fib k * fib n";
4.67 -  also; have "gcd (..., fib (k + 1)) = gcd (fib k * fib n, fib (k + 1))";
4.68 +  also; have "gcd (..., fib (k + 1)) = gcd (fib k * fib n, fib (k + 1))";
4.70 -  also; have "... = gcd (fib n, fib (k + 1))";
4.71 +  also; have "... = gcd (fib n, fib (k + 1))";
4.72      by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel);
4.73 -  also; have "... = gcd (fib m, fib n)";
4.74 +  also; have "... = gcd (fib m, fib n)";
4.76    finally; show ?thesis; .;
4.77  qed;
4.78
4.79 -lemma gcd_fib_diff:
4.80 +lemma gcd_fib_diff:
4.81    "m <= n ==> gcd (fib m, fib (n - m)) = gcd (fib m, fib n)";
4.82 -proof -;
4.83 +proof -;
4.84    assume "m <= n";
4.85 -  have "gcd (fib m, fib (n - m)) = gcd (fib m, fib (n - m + m))";
4.86 +  have "gcd (fib m, fib (n - m)) = gcd (fib m, fib (n - m + m))";
4.88 -  also; have "n - m + m = n"; by (simp!);
4.89 +  also; have "n - m + m = n"; by (simp!);
4.90    finally; show ?thesis; .;
4.91  qed;
4.92
4.93 -lemma if_cases:    (* FIXME move to HOL.thy (!?) *)
4.94 -  "[| Q ==> P x; ~ Q ==> P y |] ==> P (if Q then x else y)"; by simp;
4.95 -
4.96 -lemma gcd_fib_mod:
4.97 +lemma gcd_fib_mod:
4.98    "0 < m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)";
4.99  proof (induct n rule: less_induct);
4.100 -  fix n;
4.101 +  fix n;
4.102    assume m: "0 < m"
4.103 -  and hyp: "ALL ma. ma < n
4.104 +  and hyp: "ALL ma. ma < n
4.105             --> gcd (fib m, fib (ma mod m)) = gcd (fib m, fib ma)";
4.106    have "n mod m = (if n < m then n else (n - m) mod m)";
4.107      by (rule mod_if);
4.108    also; have "gcd (fib m, fib ...) = gcd (fib m, fib n)";
4.109 -  proof (rule if_cases);
4.110 -    assume "~ n < m"; hence m_le_n: "m <= n"; by simp;
4.111 +  proof cases;
4.112 +    assume "n < m"; thus ?thesis; by simp;
4.113 +  next;
4.114 +    assume not_lt: "~ n < m"; hence le: "m <= n"; by simp;
4.115      have "n - m < n"; by (simp! add: diff_less);
4.116      with hyp; have "gcd (fib m, fib ((n - m) mod m))
4.117         = gcd (fib m, fib (n - m))"; by simp;
4.118 -    also; from m_le_n; have "... = gcd (fib m, fib n)";
4.119 +    also; from le; have "... = gcd (fib m, fib n)";
4.120        by (rule gcd_fib_diff);
4.121 -    finally; show "gcd (fib m, fib ((n - m) mod m)) = gcd (fib m, fib n)"; .;
4.122 -  qed simp;
4.123 +    finally; have "gcd (fib m, fib ((n - m) mod m)) =
4.124 +      gcd (fib m, fib n)"; .;
4.125 +    with not_lt; show ?thesis; by simp;
4.126 +  qed;
4.127    finally; show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"; .;
4.128  qed;
4.129

     5.1 --- a/src/HOL/Isar_examples/MultisetOrder.thy	Sat Aug 19 12:44:20 2000 +0200
5.2 +++ b/src/HOL/Isar_examples/MultisetOrder.thy	Sat Aug 19 12:44:39 2000 +0200
5.3 @@ -25,11 +25,11 @@
5.4
5.5  lemma less_add: "(N, M0 + {#a#}) : mult1 r ==>
5.6      (EX M. (M, M0) : mult1 r & N = M + {#a#}) |
5.7 -    (EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K)"
5.8 +    (EX K. (ALL b. b :# K --> (b, a) : r) & N = M0 + K)"
5.9    (concl is "?case1 (mult1 r) | ?case2");
5.10  proof (unfold mult1_def);
5.11 -  let ?r = "\\<lambda>K a. ALL b. elem K b --> (b, a) : r";
5.12 -  let ?R = "\\<lambda>N M. EX a M0 K. M = M0 + {#a#} & N = M0 + K & ?r K a";
5.13 +  let ?r = "\<lambda>K a. ALL b. b :# K --> (b, a) : r";
5.14 +  let ?R = "\<lambda>N M. EX a M0 K. M = M0 + {#a#} & N = M0 + K & ?r K a";
5.15    let ?case1 = "?case1 {(N, M). ?R N M}";
5.16
5.17    assume "(N, M0 + {#a#}) : {(N, M). ?R N M}";
5.18 @@ -77,7 +77,7 @@
5.19        fix N;
5.20        assume "(N, M0 + {#a#}) : ?R";
5.21        hence "((EX M. (M, M0) : ?R & N = M + {#a#}) |
5.22 -          (EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K))";
5.23 +          (EX K. (ALL b. b :# K --> (b, a) : r) & N = M0 + K))";
5.25        thus "N : ?W";
5.26        proof (elim exE disjE conjE);
5.27 @@ -88,7 +88,7 @@
5.28        next;
5.29  	fix K;
5.30  	assume N: "N = M0 + K";
5.31 -	assume "ALL b. elem K b --> (b, a) : r";
5.32 +	assume "ALL b. b :# K --> (b, a) : r";
5.33  	have "?this --> M0 + K : ?W" (is "?P K");
5.34  	proof (induct K);
5.35  	  from M0; have "M0 + {#} : ?W"; by simp;
5.36 @@ -97,7 +97,7 @@
5.37  	  fix K x; assume hyp: "?P K";
5.38  	  show "?P (K + {#x#})";
5.39  	  proof;
5.40 -	    assume a: "ALL b. elem (K + {#x#}) b --> (b, a) : r";
5.41 +	    assume a: "ALL b. b :# (K + {#x#}) --> (b, a) : r";
5.42  	    hence "(x, a) : r"; by simp;
5.43  	    with wf_hyp; have b: "ALL M:?W. M + {#x#} : ?W"; by blast;
5.44

     6.1 --- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Sat Aug 19 12:44:20 2000 +0200
6.2 +++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Sat Aug 19 12:44:39 2000 +0200
6.3 @@ -69,7 +69,8 @@
6.4    by (simp add: below_def less_Suc_eq) blast;
6.5
6.6  lemma Sigma_Suc2:
6.7 -    "m = n + 2 ==> A <*> below m = (A <*> {n}) Un (A <*> {n + 1}) Un (A <*> below n)";
6.8 +    "m = n + 2 ==> A <*> below m =
6.9 +      (A <*> {n}) Un (A <*> {n + 1}) Un (A <*> below n)";
6.10    by (auto simp add: below_def) arith;
6.11
6.12  lemmas Sigma_Suc = Sigma_Suc1 Sigma_Suc2;
6.13 @@ -112,7 +113,7 @@
6.14  subsection {* Dominoes *};
6.15
6.16  consts
6.17 -  domino  :: "(nat * nat) set set";
6.18 +  domino :: "(nat * nat) set set";
6.19
6.20  inductive domino
6.21    intros

     7.1 --- a/src/HOL/Isar_examples/NestedDatatype.thy	Sat Aug 19 12:44:20 2000 +0200
7.2 +++ b/src/HOL/Isar_examples/NestedDatatype.thy	Sat Aug 19 12:44:39 2000 +0200
7.3 @@ -32,7 +32,8 @@
7.4        subst_term_list f1 (subst_term_list f2 ts)";
7.5    by (induct t and ts rule: term.induct) simp_all;
7.6
7.7 -lemma "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)";
7.8 +lemma "subst_term (subst_term f1 o f2) t =
7.9 +  subst_term f1 (subst_term f2 t)";
7.10  proof -;
7.11    let "?P t" = ?thesis;
7.12    let ?Q = "\\<lambda>ts. subst_term_list (subst_term f1 o f2) ts =
7.13 @@ -55,7 +56,8 @@
7.14  subsection {* Alternative induction *};
7.15
7.16  theorem term_induct' [case_names Var App]:
7.17 - "(!!a. P (Var a)) ==> (!!b ts. list_all P ts ==> P (App b ts)) ==> P t";
7.18 +  "(!!a. P (Var a)) ==>
7.19 +   (!!b ts. list_all P ts ==> P (App b ts)) ==> P t";
7.20  proof -;
7.21    assume var: "!!a. P (Var a)";
7.22    assume app: "!!b ts. list_all P ts ==> P (App b ts)";
7.23 @@ -76,7 +78,7 @@
7.24  lemma
7.25    "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)"
7.26    (is "?P t");
7.27 -proof (induct ?P t rule: term_induct');
7.28 +proof (induct (open) ?P t rule: term_induct');
7.29    case Var;
7.30    show "?P (Var a)"; by (simp add: o_def);
7.31  next;

     8.1 --- a/src/HOL/Isar_examples/Summation.thy	Sat Aug 19 12:44:20 2000 +0200
8.2 +++ b/src/HOL/Isar_examples/Summation.thy	Sat Aug 19 12:44:39 2000 +0200
8.3 @@ -153,7 +153,8 @@
8.4    show "?P 0"; by (simp add: power_eq_if);
8.5
8.6    fix n;
8.7 -  have "?S (n + 1) = ?S n + #4 * (n + 1)^#3"; by (simp add: power_eq_if distrib);
8.8 +  have "?S (n + 1) = ?S n + #4 * (n + 1)^#3";
8.9 +    by (simp add: power_eq_if distrib);
8.10    also; assume "?S n = (n * (n + 1))^2";
8.11    also; have "... + #4 * (n + 1)^#3 = ((n + 1) * ((n + 1) + 1))^2";
8.12      by (simp add: power_eq_if distrib);

     9.1 --- a/src/HOL/Isar_examples/W_correct.thy	Sat Aug 19 12:44:20 2000 +0200
9.2 +++ b/src/HOL/Isar_examples/W_correct.thy	Sat Aug 19 12:44:39 2000 +0200
9.3 @@ -36,8 +36,8 @@
9.4    intros [simp]
9.5      Var: "n < length a ==> a |- Var n :: a ! n"
9.6      Abs: "t1#a |- e :: t2 ==> a |- Abs e :: t1 -> t2"
9.7 -    App: "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |]
9.8 -              ==> a |- App e1 e2 :: t1";
9.9 +    App: "a |- e1 :: t2 -> t1 ==> a |- e2 :: t2
9.10 +      ==> a |- App e1 e2 :: t1";
9.11
9.12
9.13  text {* Type assigment is closed wrt.\ substitution. *};
9.14 @@ -46,7 +46,7 @@
9.15  proof -;
9.16    assume "a |- e :: t";
9.17    thus ?thesis (is "?P a e t");
9.18 -  proof (induct ?P a e t);
9.19 +  proof (induct (open) ?P a e t);
9.20      case Var;
9.21      hence "n < length (map ($s) a)"; by simp; 9.22 hence "map ($ s) a |- Var n :: map (\$ s) a ! n";

    10.1 --- a/src/HOL/Isar_examples/document/style.tex	Sat Aug 19 12:44:20 2000 +0200
10.2 +++ b/src/HOL/Isar_examples/document/style.tex	Sat Aug 19 12:44:39 2000 +0200
10.3 @@ -3,6 +3,7 @@
10.4
10.5  \documentclass[11pt,a4paper]{article}
10.6  \usepackage{proof,isabelle,isabellesym,pdfsetup}
10.7 +\urlstyle{rm}
10.8
10.10

    11.1 --- a/src/HOL/Real/HahnBanach/document/root.tex	Sat Aug 19 12:44:20 2000 +0200
11.2 +++ b/src/HOL/Real/HahnBanach/document/root.tex	Sat Aug 19 12:44:39 2000 +0200
11.3 @@ -4,6 +4,7 @@
11.4  \usepackage{latexsym,theorem}
11.5  \usepackage{isabelle,isabellesym,bbb}
11.6  \usepackage{pdfsetup} %last one!
11.7 +\urlstyle{rm}
11.8
11.9  \input{notation}
11.10
11.11 @@ -13,10 +14,8 @@
11.12  \pagenumbering{arabic}
11.13
11.14  \title{The Hahn-Banach Theorem for Real Vector Spaces}
11.15 -
11.16  \author{Gertrud Bauer \\ \url{http://www.in.tum.de/~bauerg/}}
11.17  \maketitle
11.18 -\maketitle
11.19
11.20  \begin{abstract}
11.21    The Hahn-Banach Theorem is one of the most fundamental results in functional