# HG changeset patch
# User wenzelm
# Date 973547767 -3600
# Node ID d8b3613158b162fa3979426a7fd104929c81bbcb
# Parent  998778f8d63bfec50918a179b33a8471b7341d29
improved: 'induct' handle non-atomic goals;

diff -r 998778f8d63b -r d8b3613158b1 src/HOL/Isar_examples/Fibonacci.thy
--- a/src/HOL/Isar_examples/Fibonacci.thy	Mon Nov 06 22:54:13 2000 +0100
+++ b/src/HOL/Isar_examples/Fibonacci.thy	Mon Nov 06 22:56:07 2000 +0100
@@ -126,28 +126,34 @@
 
 lemma gcd_fib_mod:
   "0 < m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
-proof (induct n rule: nat_less_induct)
-  fix n
+proof -
   assume m: "0 < m"
-  and hyp: "ALL ma. ma < n
-           --> gcd (fib m, fib (ma mod m)) = gcd (fib m, fib ma)"
-  have "n mod m = (if n < m then n else (n - m) mod m)"
-    by (rule mod_if)
-  also have "gcd (fib m, fib ...) = gcd (fib m, fib n)"
-  proof cases
-    assume "n < m" thus ?thesis by simp
-  next
-    assume not_lt: "~ n < m" hence le: "m <= n" by simp
-    have "n - m < n" by (simp! add: diff_less)
-    with hyp have "gcd (fib m, fib ((n - m) mod m))
-       = gcd (fib m, fib (n - m))" by simp
-    also from le have "... = gcd (fib m, fib n)"
-      by (rule gcd_fib_diff)
-    finally have "gcd (fib m, fib ((n - m) mod m)) =
-      gcd (fib m, fib n)" .
-    with not_lt show ?thesis by simp
+  show ?thesis
+  proof (induct n rule: nat_less_induct)
+    fix n
+    assume hyp: "ALL ma. ma < n
+      --> gcd (fib m, fib (ma mod m)) = gcd (fib m, fib ma)"
+    show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
+    proof -
+      have "n mod m = (if n < m then n else (n - m) mod m)"
+	by (rule mod_if)
+      also have "gcd (fib m, fib ...) = gcd (fib m, fib n)"
+      proof cases
+	assume "n < m" thus ?thesis by simp
+      next
+	assume not_lt: "~ n < m" hence le: "m <= n" by simp
+	have "n - m < n" by (simp! add: diff_less)
+	with hyp have "gcd (fib m, fib ((n - m) mod m))
+	  = gcd (fib m, fib (n - m))" by simp
+	also from le have "... = gcd (fib m, fib n)"
+	  by (rule gcd_fib_diff)
+	finally have "gcd (fib m, fib ((n - m) mod m)) =
+	  gcd (fib m, fib n)" .
+	with not_lt show ?thesis by simp
+      qed
+      finally show ?thesis .
+    qed
   qed
-  finally show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)" .
 qed
 
 
diff -r 998778f8d63b -r d8b3613158b1 src/HOL/Isar_examples/Hoare.thy
--- a/src/HOL/Isar_examples/Hoare.thy	Mon Nov 06 22:54:13 2000 +0100
+++ b/src/HOL/Isar_examples/Hoare.thy	Mon Nov 06 22:56:07 2000 +0100
@@ -166,28 +166,26 @@
   fix s s' assume s: "s : P"
   assume "Sem (While b X c) s s'"
   then obtain n where iter: "iter n b (Sem c) s s'" by auto
-  show "s' : P Int -b"
-  proof -
-    have "ALL s s'. iter n b (Sem c) s s' --> s : P --> s' : P Int -b"
-      (is "?P n")
-    proof (induct (stripped) n)
-      fix s s' assume s: "s : P"
-      {
-        assume "iter 0 b (Sem c) s s'"
-        with s show "s' : P Int -b" by auto
-      next
-        fix n assume hyp: "?P n"
-        assume "iter (Suc n) b (Sem c) s s'"
-        then obtain s'' where b: "s : b" and sem: "Sem c s s''"
-            and iter: "iter n b (Sem c) s'' s'"
-          by auto
-        from s b have "s : P Int b" by simp
-        with body sem have "s'' : P" ..
-        with hyp iter show "s' : P Int -b" by simp
-      }
-    qed
-    with iter s show ?thesis by simp
+
+  have "!!s. iter n b (Sem c) s s' ==> s : P ==> s' : P Int -b"
+    (is "PROP ?P n")
+  proof (induct n)
+    fix s assume s: "s : P"
+    {
+      assume "iter 0 b (Sem c) s s'"
+      with s show "?thesis s" by auto
+    next
+      fix n assume hyp: "PROP ?P n"
+      assume "iter (Suc n) b (Sem c) s s'"
+      then obtain s'' where b: "s : b" and sem: "Sem c s s''"
+        and iter: "iter n b (Sem c) s'' s'"
+        by auto
+      from s b have "s : P Int b" by simp
+      with body sem have "s'' : P" ..
+      with iter show "?thesis s" by (rule hyp)
+    }
   qed
+  from this iter s show "s' : P Int -b" .
 qed
 
 
diff -r 998778f8d63b -r d8b3613158b1 src/HOL/Isar_examples/MutilatedCheckerboard.thy
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Mon Nov 06 22:54:13 2000 +0100
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Mon Nov 06 22:56:07 2000 +0100
@@ -23,31 +23,38 @@
 inductive "tiling A"
   intros
     empty: "{} : tiling A"
-    Un:    "a : A ==> t : tiling A ==> a <= - t
-              ==> a Un t : tiling A"
+    Un: "a : A ==> t : tiling A ==> a <= - t ==> a Un t : tiling A"
 
 
 text "The union of two disjoint tilings is a tiling."
 
 lemma tiling_Un:
-  "t : tiling A --> u : tiling A --> t Int u = {}
-    --> t Un u : tiling A"
-proof
-  assume "t : tiling A" (is "_ : ?T")
-  thus "u : ?T --> t Int u = {} --> t Un u : ?T" (is "?P t")
-  proof (induct (stripped) t)
-    assume "u : ?T" "{} Int u = {}"
-    thus "{} Un u : ?T" by simp
+  "t : tiling A ==> u : tiling A ==> t Int u = {}
+    ==> t Un u : tiling A"
+proof -
+  let ?T = "tiling A"
+  assume u: "u : ?T"
+  assume "t : ?T"
+  thus "t Int u = {} ==> t Un u : ?T" (is "PROP ?P t")
+  proof (induct t)
+    from u show "{} Un u : ?T" by simp
   next
     fix a t
-    assume "a : A" "t : ?T" "?P t" "a <= - t"
-    assume "u : ?T" "(a Un t) Int u = {}"
-    have hyp: "t Un u: ?T" by (blast!)
-    have "a <= - (t Un u)" by (blast!)
-    with _ hyp have "a Un (t Un u) : ?T" by (rule tiling.Un)
-    also have "a Un (t Un u) = (a Un t) Un u"
-      by (simp only: Un_assoc)
-    finally show "... : ?T" .
+    assume "a : A" and hyp: "PROP ?P t"
+      and at: "a <= - t" and atu: "(a Un t) Int u = {}"
+    show "(a Un t) Un u : ?T"
+    proof -
+      have "a Un (t Un u) : ?T"
+      proof (rule tiling.Un)
+        show "a : A" .
+        from atu have "t Int u = {}" by blast
+        thus "t Un u: ?T" by (rule hyp)
+        from at atu show "a <= - (t Un u)" by blast
+      qed
+      also have "a Un (t Un u) = (a Un t) Un u"
+        by (simp only: Un_assoc)
+      finally show ?thesis .
+    qed
   qed
 qed
 
@@ -112,13 +119,13 @@
 
 subsection {* Dominoes *}
 
-consts 
+consts
   domino :: "(nat * nat) set set"
 
 inductive domino
   intros
-    horiz:  "{(i, j), (i, j + 1)} : domino"
-    vertl:  "{(i, j), (i + 1, j)} : domino"
+    horiz: "{(i, j), (i, j + 1)} : domino"
+    vertl: "{(i, j), (i + 1, j)} : domino"
 
 lemma dominoes_tile_row:
   "{i} <*> below (2 * n) : tiling domino"
@@ -154,7 +161,7 @@
 
   have "?B (Suc m) = ?t Un ?B m" by (simp add: Sigma_Suc)
   also have "... : ?T"
-  proof (rule tiling_Un [rule_format])
+  proof (rule tiling_Un)
     show "?t : ?T" by (rule dominoes_tile_row)
     from hyp show "?B m : ?T" .
     show "?t Int ?B m = {}" by blast
@@ -178,10 +185,14 @@
 qed
 
 lemma domino_finite: "d: domino ==> finite d"
-proof (induct set: domino)
-  fix i j :: nat
-  show "finite {(i, j), (i, j + 1)}" by (intro Finites.intros)
-  show "finite {(i, j), (i + 1, j)}" by (intro Finites.intros)
+proof -
+  assume "d: domino"
+  thus ?thesis
+  proof induct
+    fix i j :: nat
+    show "finite {(i, j), (i, j + 1)}" by (intro Finites.intros)
+    show "finite {(i, j), (i + 1, j)}" by (intro Finites.intros)
+  qed
 qed
 
 
@@ -211,27 +222,27 @@
 
     fix a t
     let ?e = evnodd
-    assume "a : domino" "t : ?T"
+    assume "a : domino" and "t : ?T"
       and hyp: "card (?e t 0) = card (?e t 1)"
-      and "a <= - t"
+      and at: "a <= - t"
 
     have card_suc:
       "!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))"
     proof -
       fix b assume "b < 2"
       have "?e (a Un t) b = ?e a b Un ?e t b" by (rule evnodd_Un)
-      also obtain i j where "?e a b = {(i, j)}"
+      also obtain i j where e: "?e a b = {(i, j)}"
       proof -
-	have "EX i j. ?e a b = {(i, j)}" by (rule domino_singleton)
-	thus ?thesis by (blast intro: that)
+        have "EX i j. ?e a b = {(i, j)}" by (rule domino_singleton)
+        thus ?thesis by (blast intro: that)
       qed
       also have "... Un ?e t b = insert (i, j) (?e t b)" by simp
       also have "card ... = Suc (card (?e t b))"
       proof (rule card_insert_disjoint)
-	show "finite (?e t b)"
+        show "finite (?e t b)"
           by (rule evnodd_finite, rule tiling_domino_finite)
-	have "(i, j) : ?e a b" by (simp!)
-	thus "(i, j) ~: ?e t b" by (blast! dest: evnoddD)
+        from e have "(i, j) : ?e a b" by simp
+        with at show "(i, j) ~: ?e t b" by (blast dest: evnoddD)
       qed
       finally show "?thesis b" .
     qed
@@ -274,9 +285,9 @@
       have "card (?e ?t' 0 - {(2 * m + 1, 2 * n + 1)})
         < card (?e ?t' 0)"
       proof (rule card_Diff1_less)
-	from _ fin show "finite (?e ?t' 0)"
+        from _ fin show "finite (?e ?t' 0)"
           by (rule finite_subset) auto
-	show "(2 * m + 1, 2 * n + 1) : ?e ?t' 0" by simp
+        show "(2 * m + 1, 2 * n + 1) : ?e ?t' 0" by simp
       qed
       thus ?thesis by simp
     qed
diff -r 998778f8d63b -r d8b3613158b1 src/HOL/Isar_examples/W_correct.thy
--- a/src/HOL/Isar_examples/W_correct.thy	Mon Nov 06 22:54:13 2000 +0100
+++ b/src/HOL/Isar_examples/W_correct.thy	Mon Nov 06 22:56:07 2000 +0100
@@ -27,7 +27,7 @@
   has_type :: "(typ list * expr * typ) set"
 
 syntax
-  "_has_type" :: "[typ list, expr, typ] => bool"
+  "_has_type" :: "typ list => expr => typ => bool"
     ("((_) |-/ (_) :: (_))" [60, 0, 60] 60)
 translations
   "a |- e :: t" == "(a, e, t) : has_type"
@@ -74,7 +74,7 @@
 subsection {* Type inference algorithm W *}
 
 consts
-  W :: "[expr, typ list, nat] => (subst * typ * nat) maybe"
+  W :: "expr => typ list => nat => (subst * typ * nat) maybe"
 
 primrec
   "W (Var i) a n =
@@ -91,59 +91,52 @@
 
 subsection {* Correctness theorem *}
 
-theorem W_correct: "W e a n = Ok (s, t, m) ==> $ s a |- e :: t"
-proof -
-  assume W_ok: "W e a n = Ok (s, t, m)"
-  have "ALL a s t m n. Ok (s, t, m) = W e a n --> $ s a |- e :: t"
-    (is "?P e")
-  proof (induct (stripped) e)
-    fix a s t m n
-    {
-      fix i
-      assume "Ok (s, t, m) = W (Var i) a n"
-      thus "$ s a |- Var i :: t" by (simp split: if_splits)
-    next
-      fix e assume hyp: "?P e"
-      assume "Ok (s, t, m) = W (Abs e) a n"
-      then obtain t' where "t = s n -> t'"
-	  and "Ok (s, t', m) = W e (TVar n # a) (Suc n)"
-	by (auto split: bind_splits)
-      with hyp show "$ s a |- Abs e :: t"
-	by (force intro: has_type.Abs)
-    next
-      fix e1 e2 assume hyp1: "?P e1" and hyp2: "?P e2"
-      assume "Ok (s, t, m) = W (App e1 e2) a n"
-      then obtain s1 t1 n1 s2 t2 n2 u where
+theorem W_correct: "!!a s t m n. Ok (s, t, m) = W e a n ==> $ s a |- e :: t"
+  (is "PROP ?P e")
+proof (induct e)
+  fix a s t m n
+  {
+    fix i
+    assume "Ok (s, t, m) = W (Var i) a n"
+    thus "$ s a |- Var i :: t" by (simp split: if_splits)
+  next
+    fix e assume hyp: "PROP ?P e"
+    assume "Ok (s, t, m) = W (Abs e) a n"
+    then obtain t' where "t = s n -> t'"
+        and "Ok (s, t', m) = W e (TVar n # a) (Suc n)"
+      by (auto split: bind_splits)
+    with hyp show "$ s a |- Abs e :: t"
+      by (force intro: has_type.Abs)
+  next
+    fix e1 e2 assume hyp1: "PROP ?P e1" and hyp2: "PROP ?P e2"
+    assume "Ok (s, t, m) = W (App e1 e2) a n"
+    then obtain s1 t1 n1 s2 t2 n2 u where
           s: "s = $ u o $ s2 o s1"
-          and t: "t = u n2"
-          and mgu_ok: "mgu ($ s2 t1) (t2 -> TVar n2) = Ok u"
-          and W1_ok: "W e1 a n = Ok (s1, t1, n1)"
-          and W2_ok: "W e2 ($ s1 a) n1 = Ok (s2, t2, n2)"
-	by (auto split: bind_splits simp: that)
-      show "$ s a |- App e1 e2 :: t"
-      proof (rule has_type.App)
-        from s have s': "$ u ($ s2 ($ s1 a)) = $s a"
-          by (simp add: subst_comp_tel o_def)
-        show "$s a |- e1 :: $ u t2 -> t"
-        proof -
-          from hyp1 W1_ok [symmetric] have "$ s1 a |- e1 :: t1"
-            by blast
-          hence "$ u ($ s2 ($ s1 a)) |- e1 :: $ u ($ s2 t1)"
-            by (intro has_type_subst_closed)
-          with s' t mgu_ok show ?thesis by simp
-        qed
-        show "$ s a |- e2 :: $ u t2"
-        proof -
-          from hyp2 W2_ok [symmetric]
-          have "$ s2 ($ s1 a) |- e2 :: t2" by blast
-          hence "$ u ($ s2 ($ s1 a)) |- e2 :: $ u t2"
-            by (rule has_type_subst_closed)
-          with s' show ?thesis by simp
-        qed
+        and t: "t = u n2"
+        and mgu_ok: "mgu ($ s2 t1) (t2 -> TVar n2) = Ok u"
+        and W1_ok: "Ok (s1, t1, n1) = W e1 a n"
+        and W2_ok: "Ok (s2, t2, n2) = W e2 ($ s1 a) n1"
+      by (auto split: bind_splits simp: that)
+    show "$ s a |- App e1 e2 :: t"
+    proof (rule has_type.App)
+      from s have s': "$ u ($ s2 ($ s1 a)) = $s a"
+        by (simp add: subst_comp_tel o_def)
+      show "$s a |- e1 :: $ u t2 -> t"
+      proof -
+        from W1_ok have "$ s1 a |- e1 :: t1" by (rule hyp1)
+        hence "$ u ($ s2 ($ s1 a)) |- e1 :: $ u ($ s2 t1)"
+          by (intro has_type_subst_closed)
+        with s' t mgu_ok show ?thesis by simp
       qed
-    }
-  qed
-  with W_ok [symmetric] show ?thesis by blast
+      show "$ s a |- e2 :: $ u t2"
+      proof -
+        from W2_ok have "$ s2 ($ s1 a) |- e2 :: t2" by (rule hyp2)
+        hence "$ u ($ s2 ($ s1 a)) |- e2 :: $ u t2"
+          by (rule has_type_subst_closed)
+        with s' show ?thesis by simp
+      qed
+    qed
+  }
 qed
 
 end
diff -r 998778f8d63b -r d8b3613158b1 src/HOL/Library/List_Prefix.thy
--- a/src/HOL/Library/List_Prefix.thy	Mon Nov 06 22:54:13 2000 +0100
+++ b/src/HOL/Library/List_Prefix.thy	Mon Nov 06 22:56:07 2000 +0100
@@ -137,49 +137,44 @@
 
 theorem parallel_decomp:
   "xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs"
-  (concl is "?E xs")
-proof -
-  assume "xs \<parallel> ys"
-  have "?this --> ?E xs" (is "?P xs")
-  proof (induct (stripped) xs rule: rev_induct)
-    assume "[] \<parallel> ys" hence False by auto
-    thus "?E []" ..
-  next
-    fix x xs
-    assume hyp: "?P xs"
-    assume asm: "xs @ [x] \<parallel> ys"
-    show "?E (xs @ [x])"
-    proof (rule prefix_cases)
-      assume le: "xs \<le> ys"
-      then obtain ys' where ys: "ys = xs @ ys'" ..
-      show ?thesis
-      proof (cases ys')
-        assume "ys' = []" with ys have "xs = ys" by simp
-        with asm have "[x] \<parallel> []" by auto
-        hence False by blast
-        thus ?thesis ..
-      next
-        fix c cs assume ys': "ys' = c # cs"
-        with asm ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:)
-        hence "x \<noteq> c" by auto
-        moreover have "xs @ [x] = xs @ x # []" by simp
-        moreover from ys ys' have "ys = xs @ c # cs" by (simp only:)
-        ultimately show ?thesis by blast
-      qed
-    next
-      assume "ys \<le> xs" hence "ys \<le> xs @ [x]" by simp
-      with asm have False by blast
+  (is "PROP ?P xs" concl is "?E xs")
+proof (induct xs rule: rev_induct)
+  assume "[] \<parallel> ys" hence False by auto
+  thus "?E []" ..
+next
+  fix x xs
+  assume hyp: "PROP ?P xs"
+  assume asm: "xs @ [x] \<parallel> ys"
+  show "?E (xs @ [x])"
+  proof (rule prefix_cases)
+    assume le: "xs \<le> ys"
+    then obtain ys' where ys: "ys = xs @ ys'" ..
+    show ?thesis
+    proof (cases ys')
+      assume "ys' = []" with ys have "xs = ys" by simp
+      with asm have "[x] \<parallel> []" by auto
+      hence False by blast
       thus ?thesis ..
     next
-      assume "xs \<parallel> ys"
-      with hyp obtain as b bs c cs where neq: "(b::'a) \<noteq> c"
-          and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs"
-	by blast
-      from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp
-      with neq ys show ?thesis by blast
+      fix c cs assume ys': "ys' = c # cs"
+      with asm ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:)
+      hence "x \<noteq> c" by auto
+      moreover have "xs @ [x] = xs @ x # []" by simp
+      moreover from ys ys' have "ys = xs @ c # cs" by (simp only:)
+      ultimately show ?thesis by blast
     qed
+  next
+    assume "ys \<le> xs" hence "ys \<le> xs @ [x]" by simp
+    with asm have False by blast
+    thus ?thesis ..
+  next
+    assume "xs \<parallel> ys"
+    with hyp obtain as b bs c cs where neq: "(b::'a) \<noteq> c"
+      and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs"
+      by blast
+    from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp
+    with neq ys show ?thesis by blast
   qed
-  thus ?thesis ..
 qed
 
 end