# HG changeset patch
# User wenzelm
# Date 951661531 -3600
# Node ID e132d147374b4f692e057d30f5a4cc53544cf512
# Parent  5e7037409118072d3234e7c35bdf576862d6d411
even better induct setup;

diff -r 5e7037409118 -r e132d147374b src/HOL/Isar_examples/ExprCompiler.thy
--- a/src/HOL/Isar_examples/ExprCompiler.thy	Sun Feb 27 15:23:28 2000 +0100
+++ b/src/HOL/Isar_examples/ExprCompiler.thy	Sun Feb 27 15:25:31 2000 +0100
@@ -114,12 +114,12 @@
 lemma exec_append:
   "ALL stack. exec (xs @ ys) stack env =
     exec ys (exec xs stack env) env" (is "?P xs");
-proof (induct ?P xs in type: list);
+proof (induct ?P xs type: list);
   show "?P []"; by simp;
 
   fix x xs; assume "?P xs";
   show "?P (x # xs)" (is "?Q x");
-  proof (induct ?Q x in type: instr);
+  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!);
@@ -130,7 +130,7 @@
 proof -;
   have "ALL stack. exec (compile e) stack env =
     eval e env # stack" (is "?P e");
-  proof (induct ?P e in type: expr);
+  proof (induct ?P e type: expr);
     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))";
diff -r 5e7037409118 -r e132d147374b src/HOL/Isar_examples/Fibonacci.thy
--- a/src/HOL/Isar_examples/Fibonacci.thy	Sun Feb 27 15:23:28 2000 +0100
+++ b/src/HOL/Isar_examples/Fibonacci.thy	Sun Feb 27 15:25:31 2000 +0100
@@ -35,14 +35,14 @@
 lemmas [simp] = fib.rules;
 
 lemma [simp]: "0 < fib (Suc n)";
-  by (induct n in function: fib) (simp+);
+  by (induct n rule: fib.induct) (simp+);
 
 
 text {* Alternative induction rule. *};
 
-theorem fib_induct: 
+theorem fib_induct:
 "[| P 0; P 1; !!n. [| P (n + 1); P n |] ==> P (n + 2) |] ==> P n";
-  by (induct function: fib, simp+);
+  by (induct rule: fib.induct, simp+);
 
 
 
@@ -53,7 +53,7 @@
 lemma fib_add: 
   "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"
   (is "?P n");
-proof (rule fib_induct [of ?P n]) -- {* see \cite[page 280]{Concrete-Math} *};
+proof (induct ?P n rule: fib_induct) -- {* see \cite[page 280]{Concrete-Math} *};
   show "?P 0"; by simp;
   show "?P 1"; by simp;
   fix n;
@@ -72,7 +72,7 @@
 qed;
 
 lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (n + 1)) = 1" (is "?P n");
-proof (rule fib_induct [of ?P n]); 
+proof (induct ?P n rule: fib_induct); 
   show "?P 0"; by simp;
   show "?P 1"; by simp;
   fix n; 
@@ -130,7 +130,7 @@
 
 lemma gcd_fib_mod: 
   "0 < m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)";
-proof (rule less_induct [of _ n]);
+proof (induct n rule: less_induct);
   fix n; 
   assume m: "0 < m"
   and hyp: "ALL ma. ma < n 
@@ -152,7 +152,7 @@
 
 
 theorem fib_gcd: "fib (gcd (m, n)) = gcd (fib m, fib n)" (is "?P m n");
-proof (rule gcd_induct [of ?P m n]);
+proof (induct ?P m n rule: gcd_induct);
   fix m; show "fib (gcd (m, 0)) = gcd (fib m, fib 0)"; by simp;
   fix n; assume n: "0 < n";
   hence "gcd (m, n) = gcd (n, m mod n)"; by (rule gcd_non_0);
diff -r 5e7037409118 -r e132d147374b src/HOL/Isar_examples/MultisetOrder.thy
--- a/src/HOL/Isar_examples/MultisetOrder.thy	Sun Feb 27 15:23:28 2000 +0100
+++ b/src/HOL/Isar_examples/MultisetOrder.thy	Sun Feb 27 15:25:31 2000 +0100
@@ -15,6 +15,13 @@
  based on a pen-and-paper proof due to Wilfried Buchholz.}
 *};
 
+(* FIXME move? *)
+
+theorems [induct type: multiset] = multiset_induct;
+theorems [induct set: wf] = wf_induct;
+theorems [induct set: acc] = acc_induct;
+
+
 subsection {* A technical lemma *};
 
 lemma less_add: "(N, M0 + {#a#}) : mult1 r ==>
@@ -84,7 +91,7 @@
 	assume N: "N = M0 + K";
 	assume "ALL b. elem K b --> (b, a) : r";
 	have "?this --> M0 + K : ?W" (is "?P K");
-	proof (induct K in rule: multiset_induct);
+	proof (induct K);
 	  from M0; have "M0 + {#} : ?W"; by simp;
 	  thus "?P {#}"; ..;
 
@@ -109,7 +116,7 @@
   assume wf: "wf r";
   fix M;
   show "M : ?W";
-  proof (induct M in rule: multiset_induct);
+  proof (induct M);
     show "{#} : ?W";
     proof (rule accI);
       fix b; assume "(b, {#}) : ?R";
@@ -118,7 +125,7 @@
 
     fix M a; assume "M : ?W";
     from wf; have "ALL M:?W. M + {#a#} : ?W";
-    proof (rule wf_induct [of r]);
+    proof induct;
       fix a;
       assume "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)";
       show "ALL M:?W. M + {#a#} : ?W";