tuned induct proofs;
authorwenzelm
Thu Nov 24 00:00:20 2005 +0100 (2005-11-24)
changeset 182422215049cd29c
parent 18241 afdba6b3e383
child 18243 1287b15f27ef
tuned induct proofs;
src/HOL/Induct/Mutil.thy
src/HOL/Induct/QuoNestedDataType.thy
src/HOL/Induct/Tree.thy
     1.1 --- a/src/HOL/Induct/Mutil.thy	Wed Nov 23 22:26:13 2005 +0100
     1.2 +++ b/src/HOL/Induct/Mutil.thy	Thu Nov 24 00:00:20 2005 +0100
     1.3 @@ -72,7 +72,7 @@
     1.4    done
     1.5  
     1.6  lemma dominoes_tile_matrix: "(lessThan m) \<times> lessThan (2 * n) \<in> tiling domino"
     1.7 -  by (induct m, auto)
     1.8 +  by (induct m) auto
     1.9  
    1.10  
    1.11  text {* \medskip @{term coloured} and Dominoes *}
    1.12 @@ -98,7 +98,7 @@
    1.13  text {* \medskip Tilings of dominoes *}
    1.14  
    1.15  lemma tiling_domino_finite [simp]: "t \<in> tiling domino ==> finite t"
    1.16 -  by (induct set: tiling, auto)
    1.17 +  by (induct set: tiling) auto
    1.18  
    1.19  declare
    1.20    Int_Un_distrib [simp]
     2.1 --- a/src/HOL/Induct/QuoNestedDataType.thy	Wed Nov 23 22:26:13 2005 +0100
     2.2 +++ b/src/HOL/Induct/QuoNestedDataType.thy	Thu Nov 24 00:00:20 2005 +0100
     2.3 @@ -265,7 +265,7 @@
     2.4  
     2.5  lemma listset_Rep_Exp_Abs_Exp:
     2.6       "listset (map Rep_Exp (Abs_ExpList Us)) = listrel exprel `` {Us}";
     2.7 -by (induct_tac Us, simp_all add: listrel_Cons Abs_ExpList_def)
     2.8 +by (induct Us, simp_all add: listrel_Cons Abs_ExpList_def)
     2.9  
    2.10  lemma FnCall:
    2.11       "FnCall F (Abs_ExpList Us) = Abs_Exp (exprel``{FNCALL F Us})"
    2.12 @@ -459,4 +459,3 @@
    2.13  qed
    2.14  
    2.15  end
    2.16 -
     3.1 --- a/src/HOL/Induct/Tree.thy	Wed Nov 23 22:26:13 2005 +0100
     3.2 +++ b/src/HOL/Induct/Tree.thy	Thu Nov 24 00:00:20 2005 +0100
     3.3 @@ -46,7 +46,7 @@
     3.4    "add i (Lim f) = Lim (%n. add i (f n))"
     3.5  
     3.6  lemma add_assoc: "add (add i j) k = add i (add j k)"
     3.7 -by (induct k, auto)
     3.8 +  by (induct k) auto
     3.9  
    3.10  text{*Multiplication of ordinals*}
    3.11  consts
    3.12 @@ -57,14 +57,10 @@
    3.13    "mult i (Lim f) = Lim (%n. mult i (f n))"
    3.14  
    3.15  lemma add_mult_distrib: "mult i (add j k) = add (mult i j) (mult i k)"
    3.16 -apply (induct k) 
    3.17 -apply (auto simp add: add_assoc) 
    3.18 -done
    3.19 +  by (induct k) (auto simp add: add_assoc)
    3.20  
    3.21  lemma mult_assoc: "mult (mult i j) k = mult i (mult j k)"
    3.22 -apply (induct k) 
    3.23 -apply (auto simp add: add_mult_distrib) 
    3.24 -done
    3.25 +  by (induct k) (auto simp add: add_mult_distrib)
    3.26  
    3.27  text{*We could probably instantiate some axiomatic type classes and use
    3.28  the standard infix operators.*}
    3.29 @@ -104,7 +100,6 @@
    3.30    (hints recdef_wf: wf_brouwer_order)
    3.31  
    3.32  lemma add2_assoc: "add2 (add2 (i, j), k) = add2 (i, add2 (j, k))"
    3.33 -by (induct k, auto)
    3.34 -
    3.35 +  by (induct k) auto
    3.36  
    3.37  end