tuned;
authorwenzelm
Sat Aug 19 12:44:39 2000 +0200 (2000-08-19)
changeset 9659b9cf6801f3da
parent 9658 97d6d0a72d35
child 9660 80d14ea0e200
tuned;
src/HOL/Induct/Multiset.thy
src/HOL/Isar_examples/BasicLogic.thy
src/HOL/Isar_examples/ExprCompiler.thy
src/HOL/Isar_examples/Fibonacci.thy
src/HOL/Isar_examples/MultisetOrder.thy
src/HOL/Isar_examples/MutilatedCheckerboard.thy
src/HOL/Isar_examples/NestedDatatype.thy
src/HOL/Isar_examples/Summation.thy
src/HOL/Isar_examples/W_correct.thy
src/HOL/Isar_examples/document/style.tex
src/HOL/Real/HahnBanach/document/root.tex
     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.60      by (simp add: execute_def);
    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.16 -lemma fib_add: 
    4.17 +lemma fib_add:
    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.41      by (simp only: gcd_add2);
    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.48      by (simp add: gcd_non_0 add_commute);
    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.62      by (simp add: gcd_commute);
    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.66      by (rule fib_add);
    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.69      by (simp add: gcd_mult_add);
    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.75      by (simp! add: gcd_commute);
    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.87      by (simp add: gcd_fib_add);
    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.24  	by (rule less_add);
    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.9  \renewcommand{\isamarkupheader}[1]{\section{#1}}
   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