tuned induction proofs;
authorwenzelm
Tue Oct 16 17:58:13 2001 +0200 (2001-10-16)
changeset 11809c9ffdd63dd93
parent 11808 c724a9093ebe
child 11810 4768258b29a5
tuned induction proofs;
src/HOL/Induct/Term.thy
src/HOL/Isar_examples/ExprCompiler.thy
src/HOL/Isar_examples/Fibonacci.thy
src/HOL/Isar_examples/NestedDatatype.thy
src/HOL/Isar_examples/W_correct.thy
src/HOL/Library/Nested_Environment.thy
src/HOL/Unix/Unix.thy
     1.1 --- a/src/HOL/Induct/Term.thy	Tue Oct 16 17:56:12 2001 +0200
     1.2 +++ b/src/HOL/Induct/Term.thy	Tue Oct 16 17:58:13 2001 +0200
     1.3 @@ -36,7 +36,7 @@
     1.4      (subst_term f1 (subst_term f2 t)) \<and>
     1.5    (subst_term_list ((subst_term f1) \<circ> f2) ts) =
     1.6      (subst_term_list f1 (subst_term_list f2 ts))"
     1.7 -  apply (induct t and ts rule: term.induct)
     1.8 +  apply (induct t and ts)
     1.9       apply simp_all
    1.10    done
    1.11  
    1.12 @@ -50,7 +50,7 @@
    1.13  proof -
    1.14    case rule_context
    1.15    have "P t \<and> list_all P ts"
    1.16 -    apply (induct t and ts rule: term.induct)
    1.17 +    apply (induct t and ts)
    1.18         apply (rule rule_context)
    1.19        apply (rule rule_context)
    1.20        apply assumption
     2.1 --- a/src/HOL/Isar_examples/ExprCompiler.thy	Tue Oct 16 17:56:12 2001 +0200
     2.2 +++ b/src/HOL/Isar_examples/ExprCompiler.thy	Tue Oct 16 17:58:13 2001 +0200
     2.3 @@ -114,15 +114,15 @@
     2.4  lemma exec_append:
     2.5    "ALL stack. exec (xs @ ys) stack env =
     2.6      exec ys (exec xs stack env) env" (is "?P xs")
     2.7 -proof (induct ?P xs type: list)
     2.8 +proof (induct xs)
     2.9    show "?P []" by simp
    2.10 -
    2.11 -  fix x xs assume "?P xs"
    2.12 -  show "?P (x # xs)" (is "?Q x")
    2.13 -  proof (induct ?Q x type: instr)
    2.14 -    show "!!val. ?Q (Const val)" by (simp!)
    2.15 -    show "!!adr. ?Q (Load adr)" by (simp!)
    2.16 -    show "!!fun. ?Q (Apply fun)" by (simp!)
    2.17 +next
    2.18 +  fix x xs assume hyp: "?P xs"
    2.19 +  show "?P (x # xs)"
    2.20 +  proof (induct x)
    2.21 +    from hyp show "!!val. ?P (Const val # xs)" by simp
    2.22 +    from hyp show "!!adr. ?P (Load adr # xs)" by simp
    2.23 +    from hyp show "!!fun. ?P (Apply fun # xs)" by simp
    2.24    qed
    2.25  qed
    2.26  
    2.27 @@ -130,10 +130,10 @@
    2.28  proof -
    2.29    have "ALL stack. exec (compile e) stack env =
    2.30      eval e env # stack" (is "?P e")
    2.31 -  proof (induct ?P e type: expr)
    2.32 +  proof (induct e)
    2.33      show "!!adr. ?P (Variable adr)" by simp
    2.34      show "!!val. ?P (Constant val)" by simp
    2.35 -    show "!!fun e1 e2. (?P e1 ==> ?P e2 ==> ?P (Binop fun e1 e2))"
    2.36 +    show "!!fun e1 e2. ?P e1 ==> ?P e2 ==> ?P (Binop fun e1 e2)"
    2.37        by (simp add: exec_append)
    2.38    qed
    2.39    thus ?thesis by (simp add: execute_def)
    2.40 @@ -151,7 +151,7 @@
    2.41  lemma exec_append:
    2.42    "ALL stack. exec (xs @ ys) stack env
    2.43      = exec ys (exec xs stack env) env" (is "?P xs")
    2.44 -proof (induct ?P xs)
    2.45 +proof (induct xs)
    2.46    show "?P []" (is "ALL s. ?Q s")
    2.47    proof
    2.48      fix s have "exec ([] @ ys) s env = exec ys s env" by simp
     3.1 --- a/src/HOL/Isar_examples/Fibonacci.thy	Tue Oct 16 17:56:12 2001 +0200
     3.2 +++ b/src/HOL/Isar_examples/Fibonacci.thy	Tue Oct 16 17:58:13 2001 +0200
     3.3 @@ -52,7 +52,7 @@
     3.4    "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"
     3.5    (is "?P n")
     3.6    -- {* see \cite[page 280]{Concrete-Math} *}
     3.7 -proof (induct ?P n rule: fib_induct)
     3.8 +proof (induct n rule: fib_induct)
     3.9    show "?P 0" by simp
    3.10    show "?P 1" by simp
    3.11    fix n
    3.12 @@ -71,7 +71,7 @@
    3.13  qed
    3.14  
    3.15  lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (n + 1)) = 1" (is "?P n")
    3.16 -proof (induct ?P n rule: fib_induct)
    3.17 +proof (induct n rule: fib_induct)
    3.18    show "?P 0" by simp
    3.19    show "?P 1" by simp
    3.20    fix n
    3.21 @@ -158,7 +158,7 @@
    3.22  
    3.23  
    3.24  theorem fib_gcd: "fib (gcd (m, n)) = gcd (fib m, fib n)" (is "?P m n")
    3.25 -proof (induct ?P m n rule: gcd_induct)
    3.26 +proof (induct m n rule: gcd_induct)
    3.27    fix m show "fib (gcd (m, 0)) = gcd (fib m, fib 0)" by simp
    3.28    fix n :: nat assume n: "0 < n"
    3.29    hence "gcd (m, n) = gcd (n, m mod n)" by (rule gcd_non_0)
     4.1 --- a/src/HOL/Isar_examples/NestedDatatype.thy	Tue Oct 16 17:56:12 2001 +0200
     4.2 +++ b/src/HOL/Isar_examples/NestedDatatype.thy	Tue Oct 16 17:58:13 2001 +0200
     4.3 @@ -30,7 +30,7 @@
     4.4        subst_term f1 (subst_term f2 t) &
     4.5      subst_term_list (subst_term f1 o f2) ts =
     4.6        subst_term_list f1 (subst_term_list f2 ts)"
     4.7 -  by (induct t and ts rule: term.induct) simp_all
     4.8 +  by (induct t and ts) simp_all
     4.9  
    4.10  lemma "subst_term (subst_term f1 o f2) t =
    4.11    subst_term f1 (subst_term f2 t)"
    4.12 @@ -62,7 +62,7 @@
    4.13    assume var: "!!a. P (Var a)"
    4.14    assume app: "!!b ts. list_all P ts ==> P (App b ts)"
    4.15    show ?thesis
    4.16 -  proof (induct P t)
    4.17 +  proof (induct t)
    4.18      fix a show "P (Var a)" by (rule var)
    4.19    next
    4.20      fix b t ts assume "list_all P ts"
    4.21 @@ -78,12 +78,12 @@
    4.22  lemma
    4.23    "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)"
    4.24    (is "?P t")
    4.25 -proof (induct (open) ?P t rule: term_induct')
    4.26 -  case Var
    4.27 +proof (induct t rule: term_induct')
    4.28 +  case (Var a)
    4.29    show "?P (Var a)" by (simp add: o_def)
    4.30  next
    4.31 -  case App
    4.32 -  show "?P (App b ts)" by (insert App, induct ts) simp_all
    4.33 +  case (App b ts)
    4.34 +  thus "?P (App b ts)" by (induct ts) simp_all
    4.35  qed
    4.36  
    4.37  end
     5.1 --- a/src/HOL/Isar_examples/W_correct.thy	Tue Oct 16 17:56:12 2001 +0200
     5.2 +++ b/src/HOL/Isar_examples/W_correct.thy	Tue Oct 16 17:58:13 2001 +0200
     5.3 @@ -34,9 +34,9 @@
     5.4  
     5.5  inductive has_type
     5.6    intros
     5.7 -    Var [simp]: "n < length a ==> a |- Var n :: a ! n"
     5.8 -    Abs [simp]: "t1#a |- e :: t2 ==> a |- Abs e :: t1 -> t2"
     5.9 -    App [simp]: "a |- e1 :: t2 -> t1 ==> a |- e2 :: t2
    5.10 +    Var: "n < length a ==> a |- Var n :: a ! n"
    5.11 +    Abs: "t1#a |- e :: t2 ==> a |- Abs e :: t1 -> t2"
    5.12 +    App: "a |- e1 :: t2 -> t1 ==> a |- e2 :: t2
    5.13        ==> a |- App e1 e2 :: t1"
    5.14  
    5.15  
    5.16 @@ -46,7 +46,7 @@
    5.17  proof -
    5.18    assume "a |- e :: t"
    5.19    thus ?thesis (is "?P a e t")
    5.20 -  proof (induct (open) ?P a e t)
    5.21 +  proof (induct (open) a e t)
    5.22      case Var
    5.23      hence "n < length (map ($ s) a)" by simp
    5.24      hence "map ($ s) a |- Var n :: map ($ s) a ! n"
    5.25 @@ -66,7 +66,7 @@
    5.26        by (simp add: app_subst_list)
    5.27    next
    5.28      case App
    5.29 -    thus "?P a (App e1 e2) t1" by simp
    5.30 +    thus "?P a (App e1 e2) t1" by (simp add: has_type.App)
    5.31    qed
    5.32  qed
    5.33  
    5.34 @@ -98,7 +98,7 @@
    5.35    {
    5.36      fix i
    5.37      assume "Ok (s, t, m) = W (Var i) a n"
    5.38 -    thus "$ s a |- Var i :: t" by (simp split: if_splits)
    5.39 +    thus "$ s a |- Var i :: t" by (simp add: has_type.Var split: if_splits)
    5.40    next
    5.41      fix e assume hyp: "PROP ?P e"
    5.42      assume "Ok (s, t, m) = W (Abs e) a n"
     6.1 --- a/src/HOL/Library/Nested_Environment.thy	Tue Oct 16 17:56:12 2001 +0200
     6.2 +++ b/src/HOL/Library/Nested_Environment.thy	Tue Oct 16 17:58:13 2001 +0200
     6.3 @@ -216,7 +216,7 @@
     6.4        es' y = Some env' \<and>
     6.5        lookup env' ys = Some e"
     6.6    (is "PROP ?P xs" is "!!env e. ?A env e xs ==> ?C env e xs")
     6.7 -proof (induct ?P xs)
     6.8 +proof (induct xs)
     6.9    fix env e let ?A = "?A env e" and ?C = "?C env e"
    6.10    {
    6.11      assume "?A []"
     7.1 --- a/src/HOL/Unix/Unix.thy	Tue Oct 16 17:56:12 2001 +0200
     7.2 +++ b/src/HOL/Unix/Unix.thy	Tue Oct 16 17:58:13 2001 +0200
     7.3 @@ -591,7 +591,7 @@
     7.4    assume r: "\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow>  P x \<Longrightarrow> Q r'"
     7.5    assume "root =xs\<Rightarrow> root'"
     7.6    thus "Q root \<Longrightarrow> (\<forall>x \<in> set xs. P x) \<Longrightarrow> Q root'" (is "PROP ?P root xs root'")
     7.7 -  proof (induct ?P root xs root')
     7.8 +  proof (induct root xs root')
     7.9      fix root assume "Q root"
    7.10      thus "Q root" .
    7.11    next