author wenzelm Tue, 16 Oct 2001 17:58:13 +0200 changeset 11809 c9ffdd63dd93 parent 11808 c724a9093ebe child 11810 4768258b29a5
tuned induction proofs;
 src/HOL/Induct/Term.thy file | annotate | diff | comparison | revisions src/HOL/Isar_examples/ExprCompiler.thy file | annotate | diff | comparison | revisions src/HOL/Isar_examples/Fibonacci.thy file | annotate | diff | comparison | revisions src/HOL/Isar_examples/NestedDatatype.thy file | annotate | diff | comparison | revisions src/HOL/Isar_examples/W_correct.thy file | annotate | diff | comparison | revisions src/HOL/Library/Nested_Environment.thy file | annotate | diff | comparison | revisions src/HOL/Unix/Unix.thy file | annotate | diff | comparison | revisions
```--- 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 "!!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 "!!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 "!!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)"
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 @@
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```