# HG changeset patch
# User wenzelm
# Date 1003247893 -7200
# Node ID c9ffdd63dd93e710c6a1a4cb729fd713b0388cce
# Parent  c724a9093ebe10642d00a2a18eafb4b233a9e5a8
tuned induction proofs;

diff -r c724a9093ebe -r c9ffdd63dd93 src/HOL/Induct/Term.thy
--- a/src/HOL/Induct/Term.thy	Tue Oct 16 17:56:12 2001 +0200
+++ b/src/HOL/Induct/Term.thy	Tue Oct 16 17:58:13 2001 +0200
@@ -36,7 +36,7 @@
     (subst_term f1 (subst_term f2 t)) \<and>
   (subst_term_list ((subst_term f1) \<circ> f2) ts) =
     (subst_term_list f1 (subst_term_list f2 ts))"
-  apply (induct t and ts rule: term.induct)
+  apply (induct t and ts)
      apply simp_all
   done
 
@@ -50,7 +50,7 @@
 proof -
   case rule_context
   have "P t \<and> list_all P ts"
-    apply (induct t and ts rule: term.induct)
+    apply (induct t and ts)
        apply (rule rule_context)
       apply (rule rule_context)
       apply assumption
diff -r c724a9093ebe -r c9ffdd63dd93 src/HOL/Isar_examples/ExprCompiler.thy
--- a/src/HOL/Isar_examples/ExprCompiler.thy	Tue Oct 16 17:56:12 2001 +0200
+++ b/src/HOL/Isar_examples/ExprCompiler.thy	Tue Oct 16 17:58:13 2001 +0200
@@ -114,15 +114,15 @@
 lemma exec_append:
   "ALL stack. exec (xs @ ys) stack env =
     exec ys (exec xs stack env) env" (is "?P xs")
-proof (induct ?P xs type: list)
+proof (induct xs)
   show "?P []" by simp
-
-  fix x xs assume "?P xs"
-  show "?P (x # xs)" (is "?Q x")
-  proof (induct ?Q x type: instr)
-    show "!!val. ?Q (Const val)" by (simp!)
-    show "!!adr. ?Q (Load adr)" by (simp!)
-    show "!!fun. ?Q (Apply fun)" by (simp!)
+next
+  fix x xs assume hyp: "?P xs"
+  show "?P (x # xs)"
+  proof (induct x)
+    from hyp show "!!val. ?P (Const val # xs)" by simp
+    from hyp show "!!adr. ?P (Load adr # xs)" by simp
+    from hyp show "!!fun. ?P (Apply fun # xs)" by simp
   qed
 qed
 
@@ -130,10 +130,10 @@
 proof -
   have "ALL stack. exec (compile e) stack env =
     eval e env # stack" (is "?P e")
-  proof (induct ?P e type: expr)
+  proof (induct e)
     show "!!adr. ?P (Variable adr)" by simp
     show "!!val. ?P (Constant val)" by simp
-    show "!!fun e1 e2. (?P e1 ==> ?P e2 ==> ?P (Binop fun e1 e2))"
+    show "!!fun e1 e2. ?P e1 ==> ?P e2 ==> ?P (Binop fun e1 e2)"
       by (simp add: exec_append)
   qed
   thus ?thesis by (simp add: execute_def)
@@ -151,7 +151,7 @@
 lemma exec_append:
   "ALL stack. exec (xs @ ys) stack env
     = exec ys (exec xs stack env) env" (is "?P xs")
-proof (induct ?P xs)
+proof (induct xs)
   show "?P []" (is "ALL s. ?Q s")
   proof
     fix s have "exec ([] @ ys) s env = exec ys s env" by simp
diff -r c724a9093ebe -r c9ffdd63dd93 src/HOL/Isar_examples/Fibonacci.thy
--- a/src/HOL/Isar_examples/Fibonacci.thy	Tue Oct 16 17:56:12 2001 +0200
+++ b/src/HOL/Isar_examples/Fibonacci.thy	Tue Oct 16 17:58:13 2001 +0200
@@ -52,7 +52,7 @@
   "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"
   (is "?P n")
   -- {* see \cite[page 280]{Concrete-Math} *}
-proof (induct ?P n rule: fib_induct)
+proof (induct n rule: fib_induct)
   show "?P 0" by simp
   show "?P 1" by simp
   fix n
@@ -71,7 +71,7 @@
 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 n rule: fib_induct)
   show "?P 0" by simp
   show "?P 1" by simp
   fix n
@@ -158,7 +158,7 @@
 
 
 theorem fib_gcd: "fib (gcd (m, n)) = gcd (fib m, fib n)" (is "?P m n")
-proof (induct ?P m n rule: gcd_induct)
+proof (induct m n rule: gcd_induct)
   fix m show "fib (gcd (m, 0)) = gcd (fib m, fib 0)" by simp
   fix n :: nat assume n: "0 < n"
   hence "gcd (m, n) = gcd (n, m mod n)" by (rule gcd_non_0)
diff -r c724a9093ebe -r c9ffdd63dd93 src/HOL/Isar_examples/NestedDatatype.thy
--- a/src/HOL/Isar_examples/NestedDatatype.thy	Tue Oct 16 17:56:12 2001 +0200
+++ b/src/HOL/Isar_examples/NestedDatatype.thy	Tue Oct 16 17:58:13 2001 +0200
@@ -30,7 +30,7 @@
       subst_term f1 (subst_term f2 t) &
     subst_term_list (subst_term f1 o f2) ts =
       subst_term_list f1 (subst_term_list f2 ts)"
-  by (induct t and ts rule: term.induct) simp_all
+  by (induct t and ts) simp_all
 
 lemma "subst_term (subst_term f1 o f2) t =
   subst_term f1 (subst_term f2 t)"
@@ -62,7 +62,7 @@
   assume var: "!!a. P (Var a)"
   assume app: "!!b ts. list_all P ts ==> P (App b ts)"
   show ?thesis
-  proof (induct P t)
+  proof (induct t)
     fix a show "P (Var a)" by (rule var)
   next
     fix b t ts assume "list_all P ts"
@@ -78,12 +78,12 @@
 lemma
   "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)"
   (is "?P t")
-proof (induct (open) ?P t rule: term_induct')
-  case Var
+proof (induct t rule: term_induct')
+  case (Var a)
   show "?P (Var a)" by (simp add: o_def)
 next
-  case App
-  show "?P (App b ts)" by (insert App, induct ts) simp_all
+  case (App b ts)
+  thus "?P (App b ts)" by (induct ts) simp_all
 qed
 
 end
diff -r c724a9093ebe -r c9ffdd63dd93 src/HOL/Isar_examples/W_correct.thy
--- a/src/HOL/Isar_examples/W_correct.thy	Tue Oct 16 17:56:12 2001 +0200
+++ b/src/HOL/Isar_examples/W_correct.thy	Tue Oct 16 17:58:13 2001 +0200
@@ -34,9 +34,9 @@
 
 inductive has_type
   intros
-    Var [simp]: "n < length a ==> a |- Var n :: a ! n"
-    Abs [simp]: "t1#a |- e :: t2 ==> a |- Abs e :: t1 -> t2"
-    App [simp]: "a |- e1 :: t2 -> t1 ==> a |- e2 :: t2
+    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"
 
 
@@ -46,7 +46,7 @@
 proof -
   assume "a |- e :: t"
   thus ?thesis (is "?P a e t")
-  proof (induct (open) ?P a e t)
+  proof (induct (open) a e t)
     case Var
     hence "n < length (map ($ s) a)" by simp
     hence "map ($ s) a |- Var n :: map ($ s) a ! n"
@@ -66,7 +66,7 @@
       by (simp add: app_subst_list)
   next
     case App
-    thus "?P a (App e1 e2) t1" by simp
+    thus "?P a (App e1 e2) t1" by (simp add: has_type.App)
   qed
 qed
 
@@ -98,7 +98,7 @@
   {
     fix i
     assume "Ok (s, t, m) = W (Var i) a n"
-    thus "$ s a |- Var i :: t" by (simp split: if_splits)
+    thus "$ s a |- Var i :: t" by (simp add: has_type.Var split: if_splits)
   next
     fix e assume hyp: "PROP ?P e"
     assume "Ok (s, t, m) = W (Abs e) a n"
diff -r c724a9093ebe -r c9ffdd63dd93 src/HOL/Library/Nested_Environment.thy
--- a/src/HOL/Library/Nested_Environment.thy	Tue Oct 16 17:56:12 2001 +0200
+++ b/src/HOL/Library/Nested_Environment.thy	Tue Oct 16 17:58:13 2001 +0200
@@ -216,7 +216,7 @@
       es' y = Some env' \<and>
       lookup env' ys = Some e"
   (is "PROP ?P xs" is "!!env e. ?A env e xs ==> ?C env e xs")
-proof (induct ?P xs)
+proof (induct xs)
   fix env e let ?A = "?A env e" and ?C = "?C env e"
   {
     assume "?A []"
diff -r c724a9093ebe -r c9ffdd63dd93 src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Tue Oct 16 17:56:12 2001 +0200
+++ b/src/HOL/Unix/Unix.thy	Tue Oct 16 17:58:13 2001 +0200
@@ -591,7 +591,7 @@
   assume r: "\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow>  P x \<Longrightarrow> Q r'"
   assume "root =xs\<Rightarrow> root'"
   thus "Q root \<Longrightarrow> (\<forall>x \<in> set xs. P x) \<Longrightarrow> Q root'" (is "PROP ?P root xs root'")
-  proof (induct ?P root xs root')
+  proof (induct root xs root')
     fix root assume "Q root"
     thus "Q root" .
   next