# HG changeset patch
# User wenzelm
# Date 1004459845 -3600
# Node ID bf31b35949ce67ac39ac8513f9b013d3426318a8
# Parent  26b95a6f3f79c376e546fa482cb129d40d67f9f8
tuned induct proofs;

diff -r 26b95a6f3f79 -r bf31b35949ce src/HOL/Isar_examples/Hoare.thy
--- a/src/HOL/Isar_examples/Hoare.thy	Tue Oct 30 17:33:56 2001 +0100
+++ b/src/HOL/Isar_examples/Hoare.thy	Tue Oct 30 17:37:25 2001 +0100
@@ -166,24 +166,18 @@
   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
-
   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)
-    }
+    case (0 s)
+    thus ?case by auto
+  next
+    case (Suc n 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 Suc and b have "s : P Int b" by simp
+    with body sem have "s'' : P" ..
+    with iter show ?case by (rule Suc)
   qed
   from this iter s show "s' : P Int -b" .
 qed
diff -r 26b95a6f3f79 -r bf31b35949ce src/HOL/Isar_examples/MutilatedCheckerboard.thy
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Tue Oct 30 17:33:56 2001 +0100
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Tue Oct 30 17:37:25 2001 +0100
@@ -37,19 +37,20 @@
   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
+    case empty
+    with u show "{} Un u : ?T" by simp
   next
-    fix a t
-    assume "a : A" and hyp: "PROP ?P t"
-      and at: "a <= - t" and atu: "(a Un t) Int u = {}"
+    case (Un a t)
     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
+	have atu: "(a Un t) Int u = {}" .
+	hence "t Int u = {}" by blast
+        thus "t Un u: ?T" by (rule Un)
+	have "a <= - t" .
+	with 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)
@@ -129,13 +130,13 @@
 
 lemma dominoes_tile_row:
   "{i} <*> below (2 * n) : tiling domino"
-  (is "?P n" is "?B n : ?T")
+  (is "?B n : ?T")
 proof (induct n)
-  show "?P 0" by (simp add: below_0 tiling.empty)
-
-  fix n assume hyp: "?P n"
+  case 0
+  show ?case by (simp add: below_0 tiling.empty)
+next
+  case (Suc n)
   let ?a = "{i} <*> {2 * n + 1} Un {i} <*> {2 * n}"
-
   have "?B (Suc n) = ?a Un ?B n"
     by (auto simp add: Sigma_Suc Un_assoc)
   also have "... : ?T"
@@ -144,29 +145,29 @@
       by (rule domino.horiz)
     also have "{(i, 2 * n), (i, 2 * n + 1)} = ?a" by blast
     finally show "... : domino" .
-    from hyp show "?B n : ?T" .
+    show "?B n : ?T" by (rule Suc)
     show "?a <= - ?B n" by blast
   qed
-  finally show "?P (Suc n)" .
+  finally show ?case .
 qed
 
 lemma dominoes_tile_matrix:
   "below m <*> below (2 * n) : tiling domino"
-  (is "?P m" is "?B m : ?T")
+  (is "?B m : ?T")
 proof (induct m)
-  show "?P 0" by (simp add: below_0 tiling.empty)
-
-  fix m assume hyp: "?P m"
+  case 0
+  show ?case by (simp add: below_0 tiling.empty)
+next
+  case (Suc m)
   let ?t = "{m} <*> below (2 * n)"
-
   have "?B (Suc m) = ?t Un ?B m" by (simp add: Sigma_Suc)
   also have "... : ?T"
   proof (rule tiling_Un)
     show "?t : ?T" by (rule dominoes_tile_row)
-    from hyp show "?B m : ?T" .
+    show "?B m : ?T" by (rule Suc)
     show "?t Int ?B m = {}" by blast
   qed
-  finally show "?P (Suc m)" .
+  finally show ?case .
 qed
 
 lemma domino_singleton:
@@ -213,19 +214,18 @@
 
 lemma tiling_domino_01:
   "t : tiling domino ==> card (evnodd t 0) = card (evnodd t 1)"
-  (is "t : ?T ==> ?P t")
+  (is "t : ?T ==> _")
 proof -
   assume "t : ?T"
-  thus "?P t"
+  thus ?thesis
   proof induct
-    show "?P {}" by (simp add: evnodd_def)
-
-    fix a t
+    case empty
+    show ?case by (simp add: evnodd_def)
+  next
+    case (Un a t)
     let ?e = evnodd
-    assume "a : domino" and "t : ?T"
-      and hyp: "card (?e t 0) = card (?e t 1)"
-      and at: "a <= - t"
-
+    have hyp: "card (?e t 0) = card (?e t 1)" .
+    have at: "a <= - t" .
     have card_suc:
       "!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))"
     proof -
@@ -250,7 +250,7 @@
     also from hyp have "card (?e t 0) = card (?e t 1)" .
     also from card_suc have "Suc ... = card (?e (a Un t) 1)"
       by simp
-    finally show "?P (a Un t)" .
+    finally show ?case .
   qed
 qed
 
diff -r 26b95a6f3f79 -r bf31b35949ce src/HOL/Isar_examples/W_correct.thy
--- a/src/HOL/Isar_examples/W_correct.thy	Tue Oct 30 17:33:56 2001 +0100
+++ b/src/HOL/Isar_examples/W_correct.thy	Tue Oct 30 17:37:25 2001 +0100
@@ -46,8 +46,8 @@
 proof -
   assume "a |- e :: t"
   thus ?thesis (is "?P a e t")
-  proof (induct (open) a e t)
-    case Var
+  proof induct
+    case (Var a n)
     hence "n < length (map ($ s) a)" by simp
     hence "map ($ s) a |- Var n :: map ($ s) a ! n"
       by (rule has_type.Var)
@@ -57,7 +57,7 @@
       by (simp only: app_subst_list)
     finally show "?P a (Var n) (a ! n)" .
   next
-    case Abs
+    case (Abs a e t1 t2)
     hence "$ s t1 # map ($ s) a |- e :: $ s t2"
       by (simp add: app_subst_list)
     hence "map ($ s) a |- Abs e :: $ s t1 -> $ s t2"
@@ -66,7 +66,7 @@
       by (simp add: app_subst_list)
   next
     case App
-    thus "?P a (App e1 e2) t1" by (simp add: has_type.App)
+    thus ?case by (simp add: has_type.App)
   qed
 qed
 
diff -r 26b95a6f3f79 -r bf31b35949ce src/HOL/Lambda/Type.thy
--- a/src/HOL/Lambda/Type.thy	Tue Oct 30 17:33:56 2001 +0100
+++ b/src/HOL/Lambda/Type.thy	Tue Oct 30 17:37:25 2001 +0100
@@ -95,11 +95,11 @@
 
 subsection {* n-ary function types *}
 
-lemma list_app_typeD [rule_format]:
-    "\<forall>t T. e \<turnstile> t \<^sub>\<degree>\<^sub>\<degree> ts : T \<longrightarrow> (\<exists>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<and> e \<tturnstile> ts : Ts)"
-  apply (induct_tac ts)
+lemma list_app_typeD:
+    "\<And>t T. e \<turnstile> t \<^sub>\<degree>\<^sub>\<degree> ts : T \<Longrightarrow> \<exists>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<and> e \<tturnstile> ts : Ts"
+  apply (induct ts)
    apply simp
-  apply (intro strip)
+  apply atomize
   apply simp
   apply (erule_tac x = "t \<^sub>\<degree> a" in allE)
   apply (erule_tac x = T in allE)
@@ -115,12 +115,11 @@
   "e \<turnstile> t \<^sub>\<degree>\<^sub>\<degree> ts : T \<Longrightarrow> (\<And>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> C) \<Longrightarrow> C"
   by (insert list_app_typeD) fast
 
-lemma list_app_typeI [rule_format]:
-    "\<forall>t T Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<longrightarrow> e \<tturnstile> ts : Ts \<longrightarrow> e \<turnstile> t \<^sub>\<degree>\<^sub>\<degree> ts : T"
-  apply (induct_tac ts)
-   apply (intro strip)
+lemma list_app_typeI:
+    "\<And>t T Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t \<^sub>\<degree>\<^sub>\<degree> ts : T"
+  apply (induct ts)
    apply simp
-  apply (intro strip)
+  apply atomize
   apply (case_tac Ts)
    apply simp
   apply simp
@@ -134,15 +133,13 @@
   apply blast
   done
 
-lemma lists_typings [rule_format]:
-    "\<forall>Ts. e \<tturnstile> ts : Ts \<longrightarrow> ts \<in> lists {t. \<exists>T. e \<turnstile> t : T}"
-  apply (induct_tac ts)
-   apply (intro strip)
+lemma lists_typings:
+    "\<And>Ts. e \<tturnstile> ts : Ts \<Longrightarrow> ts \<in> lists {t. \<exists>T. e \<turnstile> t : T}"
+  apply (induct ts)
    apply (case_tac Ts)
      apply simp
      apply (rule lists.Nil)
     apply simp
-  apply (intro strip)
   apply (case_tac Ts)
    apply simp
   apply simp
@@ -192,11 +189,10 @@
     by induct auto
 qed
 
-lemma lift_typings [rule_format]:
-  "\<forall>Ts. e \<tturnstile> ts : Ts \<longrightarrow> e\<langle>i:U\<rangle> \<tturnstile> (map (\<lambda>t. lift t i) ts) : Ts"
-  apply (induct_tac ts)
+lemma lift_typings:
+  "\<And>Ts. e \<tturnstile> ts : Ts \<Longrightarrow> e\<langle>i:U\<rangle> \<tturnstile> (map (\<lambda>t. lift t i) ts) : Ts"
+  apply (induct ts)
    apply simp
-  apply (intro strip)
   apply (case_tac Ts)
    apply auto
   done
diff -r 26b95a6f3f79 -r bf31b35949ce src/HOL/Library/List_Prefix.thy
--- a/src/HOL/Library/List_Prefix.thy	Tue Oct 30 17:33:56 2001 +0100
+++ b/src/HOL/Library/List_Prefix.thy	Tue Oct 30 17:37:25 2001 +0100
@@ -151,27 +151,25 @@
 
 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"
-  (is "PROP ?P xs" concl is "?E xs")
 proof (induct xs rule: rev_induct)
-  assume "[] \<parallel> ys" hence False by auto
-  thus "?E []" ..
+  case Nil
+  hence False by auto
+  thus ?case ..
 next
-  fix x xs
-  assume hyp: "PROP ?P xs"
-  assume asm: "xs @ [x] \<parallel> ys"
-  show "?E (xs @ [x])"
+  case (snoc x xs)
+  show ?case
   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
+      with snoc 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:)
+      with snoc 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:)
@@ -179,11 +177,11 @@
     qed
   next
     assume "ys < xs" hence "ys \<le> xs @ [x]" by (simp add: strict_prefix_def)
-    with asm have False by blast
+    with snoc 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"
+    with snoc 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
diff -r 26b95a6f3f79 -r bf31b35949ce src/HOL/MicroJava/J/TypeRel.thy
--- a/src/HOL/MicroJava/J/TypeRel.thy	Tue Oct 30 17:33:56 2001 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Tue Oct 30 17:37:25 2001 +0100
@@ -193,11 +193,11 @@
 (*####theorem widen_trans: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
 proof -
   assume "G\<turnstile>S\<preceq>U"
-  thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T" (*(is "PROP ?P S U")*)
-  proof (induct (*cases*) (open) (*?P S U*) rule: widen.induct [consumes 1])
+  thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T" ( *(is "PROP ?P S U")* )
+  proof (induct ( *cases* ) (open) ( *?P S U* ) rule: widen.induct [consumes 1])
     case refl
     fix T' assume "G\<turnstile>T\<preceq>T'" thus "G\<turnstile>T\<preceq>T'".
-      (* fix T' show "PROP ?P T T".*)
+      ( * fix T' show "PROP ?P T T".* )
   next
     case subcls
     fix T assume "G\<turnstile>Class D\<preceq>T"
@@ -215,24 +215,19 @@
 theorem widen_trans: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
 proof -
   assume "G\<turnstile>S\<preceq>U"
-  thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T" (*(is "PROP ?P S U")*)
-  proof (induct (*cases*) (open) (*?P S U*)) (* rule: widen.induct *)
-    case refl
-    fix T' assume "G\<turnstile>T\<preceq>T'" thus "G\<turnstile>T\<preceq>T'".
-      (* fix T' show "PROP ?P T T".*)
+  thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T"
+  proof induct
+    case (refl T T')
+    thus "G\<turnstile>T\<preceq>T'" .
   next
-    case subcls
-    fix T assume "G\<turnstile>Class D\<preceq>T"
+    case (subcls C D T)
     then obtain E where "T = Class E" by (blast dest: widen_Class)
-    from prems show "G\<turnstile>Class C\<preceq>T" proof (auto elim: rtrancl_trans) qed
+    with subcls show "G\<turnstile>Class C\<preceq>T" by (auto elim: rtrancl_trans)
   next
-    case null
-    fix RT assume "G\<turnstile>RefT R\<preceq>RT"
+    case (null R RT)
     then obtain rt where "RT = RefT rt" by (blast dest: widen_RefT)
     thus "G\<turnstile>NT\<preceq>RT" by auto
   qed
 qed
 
-
-
 end