--- 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
--- 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
--- 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)
--- 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
--- 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"
--- 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 []"
--- 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