tuned induct proofs;
authorwenzelm
Thu Dec 22 00:28:43 2005 +0100 (2005-12-22)
changeset 184609a1458cb2956
parent 18459 2b102759160d
child 18461 9125d278fdc8
tuned induct proofs;
src/HOL/Induct/QuoDataType.thy
src/HOL/Induct/QuoNestedDataType.thy
src/HOL/Isar_examples/NestedDatatype.thy
src/HOL/Lambda/Eta.thy
src/ZF/Induct/Tree_Forest.thy
     1.1 --- a/src/HOL/Induct/QuoDataType.thy	Thu Dec 22 00:28:41 2005 +0100
     1.2 +++ b/src/HOL/Induct/QuoDataType.thy	Thu Dec 22 00:28:43 2005 +0100
     1.3 @@ -49,13 +49,14 @@
     1.4  text{*Proving that it is an equivalence relation*}
     1.5  
     1.6  lemma msgrel_refl: "X \<sim> X"
     1.7 -by (induct X, (blast intro: msgrel.intros)+)
     1.8 +  by (induct X) (blast intro: msgrel.intros)+
     1.9  
    1.10  theorem equiv_msgrel: "equiv UNIV msgrel"
    1.11 -proof (simp add: equiv_def, intro conjI)
    1.12 -  show "reflexive msgrel" by (simp add: refl_def msgrel_refl)
    1.13 -  show "sym msgrel" by (simp add: sym_def, blast intro: msgrel.SYM)
    1.14 -  show "trans msgrel" by (simp add: trans_def, blast intro: msgrel.TRANS)
    1.15 +proof -
    1.16 +  have "reflexive msgrel" by (simp add: refl_def msgrel_refl)
    1.17 +  moreover have "sym msgrel" by (simp add: sym_def, blast intro: msgrel.SYM)
    1.18 +  moreover have "trans msgrel" by (simp add: trans_def, blast intro: msgrel.TRANS)
    1.19 +  ultimately show ?thesis by (simp add: equiv_def)
    1.20  qed
    1.21  
    1.22  
    1.23 @@ -78,7 +79,7 @@
    1.24  equivalence relation.  It also helps us prove that Nonce
    1.25    (the abstract constructor) is injective*}
    1.26  theorem msgrel_imp_eq_freenonces: "U \<sim> V \<Longrightarrow> freenonces U = freenonces V"
    1.27 -by (erule msgrel.induct, auto) 
    1.28 +  by (induct set: msgrel) auto
    1.29  
    1.30  
    1.31  subsubsection{*The Left Projection*}
    1.32 @@ -97,7 +98,7 @@
    1.33    (the abstract constructor) is injective*}
    1.34  theorem msgrel_imp_eqv_freeleft:
    1.35       "U \<sim> V \<Longrightarrow> freeleft U \<sim> freeleft V"
    1.36 -by (erule msgrel.induct, auto intro: msgrel.intros)
    1.37 +  by (induct set: msgrel) (auto intro: msgrel.intros)
    1.38  
    1.39  
    1.40  subsubsection{*The Right Projection*}
    1.41 @@ -115,7 +116,7 @@
    1.42    (the abstract constructor) is injective*}
    1.43  theorem msgrel_imp_eqv_freeright:
    1.44       "U \<sim> V \<Longrightarrow> freeright U \<sim> freeright V"
    1.45 -by (erule msgrel.induct, auto intro: msgrel.intros)
    1.46 +  by (induct set: msgrel) (auto intro: msgrel.intros)
    1.47  
    1.48  
    1.49  subsubsection{*The Discriminator for Constructors*}
    1.50 @@ -131,13 +132,13 @@
    1.51  text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*}
    1.52  theorem msgrel_imp_eq_freediscrim:
    1.53       "U \<sim> V \<Longrightarrow> freediscrim U = freediscrim V"
    1.54 -by (erule msgrel.induct, auto)
    1.55 +  by (induct set: msgrel) auto
    1.56  
    1.57  
    1.58  subsection{*The Initial Algebra: A Quotiented Message Type*}
    1.59  
    1.60  typedef (Msg)  msg = "UNIV//msgrel"
    1.61 -    by (auto simp add: quotient_def)
    1.62 +  by (auto simp add: quotient_def)
    1.63  
    1.64  
    1.65  text{*The abstract message constructors*}
    1.66 @@ -402,9 +403,9 @@
    1.67        and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)"
    1.68        and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)"
    1.69    shows "P msg"
    1.70 -proof (cases msg, erule ssubst)  
    1.71 -  fix U::freemsg
    1.72 -  show "P (Abs_Msg (msgrel `` {U}))"
    1.73 +proof (cases msg)
    1.74 +  case (Abs_Msg U)
    1.75 +  have "P (Abs_Msg (msgrel `` {U}))"
    1.76    proof (induct U)
    1.77      case (NONCE N) 
    1.78      with N show ?case by (simp add: Nonce_def) 
    1.79 @@ -421,6 +422,7 @@
    1.80      with D [of "Abs_Msg (msgrel `` {X})"]
    1.81      show ?case by (simp add: Decrypt)
    1.82    qed
    1.83 +  with Abs_Msg show ?thesis by (simp only:)
    1.84  qed
    1.85  
    1.86  
     2.1 --- a/src/HOL/Induct/QuoNestedDataType.thy	Thu Dec 22 00:28:41 2005 +0100
     2.2 +++ b/src/HOL/Induct/QuoNestedDataType.thy	Thu Dec 22 00:28:43 2005 +0100
     2.3 @@ -45,23 +45,20 @@
     2.4  
     2.5  text{*Proving that it is an equivalence relation*}
     2.6  
     2.7 -lemma exprel_refl_conj: "X \<sim> X & (Xs,Xs) \<in> listrel(exprel)"
     2.8 -apply (induct X and Xs)
     2.9 -apply (blast intro: exprel.intros listrel.intros)+
    2.10 -done
    2.11 -
    2.12 -lemmas exprel_refl = exprel_refl_conj [THEN conjunct1]
    2.13 -lemmas list_exprel_refl = exprel_refl_conj [THEN conjunct2]
    2.14 +lemma exprel_refl: "X \<sim> X"
    2.15 +  and list_exprel_refl: "(Xs,Xs) \<in> listrel(exprel)"
    2.16 +  by (induct X and Xs) (blast intro: exprel.intros listrel.intros)+
    2.17  
    2.18  theorem equiv_exprel: "equiv UNIV exprel"
    2.19 -proof (simp add: equiv_def, intro conjI)
    2.20 -  show "reflexive exprel" by (simp add: refl_def exprel_refl)
    2.21 -  show "sym exprel" by (simp add: sym_def, blast intro: exprel.SYM)
    2.22 -  show "trans exprel" by (simp add: trans_def, blast intro: exprel.TRANS)
    2.23 +proof -
    2.24 +  have "reflexive exprel" by (simp add: refl_def exprel_refl)
    2.25 +  moreover have "sym exprel" by (simp add: sym_def, blast intro: exprel.SYM)
    2.26 +  moreover have "trans exprel" by (simp add: trans_def, blast intro: exprel.TRANS)
    2.27 +  ultimately show ?thesis by (simp add: equiv_def)
    2.28  qed
    2.29  
    2.30  theorem equiv_list_exprel: "equiv UNIV (listrel exprel)"
    2.31 -by (insert equiv_listrel [OF equiv_exprel], simp)
    2.32 +  using equiv_listrel [OF equiv_exprel] by simp
    2.33  
    2.34  
    2.35  lemma FNCALL_Nil: "FNCALL F [] \<sim> FNCALL F []"
    2.36 @@ -100,7 +97,7 @@
    2.37  equivalence relation.  It also helps us prove that Variable
    2.38    (the abstract constructor) is injective*}
    2.39  theorem exprel_imp_eq_freevars: "U \<sim> V \<Longrightarrow> freevars U = freevars V"
    2.40 -apply (erule exprel.induct) 
    2.41 +apply (induct set: exprel) 
    2.42  apply (erule_tac [4] listrel.induct) 
    2.43  apply (simp_all add: Un_assoc)
    2.44  done
    2.45 @@ -118,7 +115,7 @@
    2.46  
    2.47  theorem exprel_imp_eq_freediscrim:
    2.48       "U \<sim> V \<Longrightarrow> freediscrim U = freediscrim V"
    2.49 -by (erule exprel.induct, auto)
    2.50 +  by (induct set: exprel) auto
    2.51  
    2.52  
    2.53  text{*This function, which returns the function name, is used to
    2.54 @@ -132,7 +129,7 @@
    2.55  
    2.56  theorem exprel_imp_eq_freefun:
    2.57       "U \<sim> V \<Longrightarrow> freefun U = freefun V"
    2.58 -by (erule exprel.induct, simp_all add: listrel.intros)
    2.59 +  by (induct set: exprel) (simp_all add: listrel.intros)
    2.60  
    2.61  
    2.62  text{*This function, which returns the list of function arguments, is used to
    2.63 @@ -145,7 +142,7 @@
    2.64  
    2.65  theorem exprel_imp_eqv_freeargs:
    2.66       "U \<sim> V \<Longrightarrow> (freeargs U, freeargs V) \<in> listrel exprel"
    2.67 -apply (erule exprel.induct)  
    2.68 +apply (induct set: exprel)
    2.69  apply (erule_tac [4] listrel.induct) 
    2.70  apply (simp_all add: listrel.intros)
    2.71  apply (blast intro: symD [OF equiv.sym [OF equiv_list_exprel]])
    2.72 @@ -265,7 +262,7 @@
    2.73  
    2.74  lemma listset_Rep_Exp_Abs_Exp:
    2.75       "listset (map Rep_Exp (Abs_ExpList Us)) = listrel exprel `` {Us}";
    2.76 -by (induct Us, simp_all add: listrel_Cons Abs_ExpList_def)
    2.77 +  by (induct Us) (simp_all add: listrel_Cons Abs_ExpList_def)
    2.78  
    2.79  lemma FnCall:
    2.80       "FnCall F (Abs_ExpList Us) = Abs_Exp (exprel``{FNCALL F Us})"
    2.81 @@ -372,7 +369,7 @@
    2.82  relations, but with little benefit here.*}
    2.83  lemma Abs_ExpList_eq:
    2.84       "(y, z) \<in> listrel exprel \<Longrightarrow> Abs_ExpList (y) = Abs_ExpList (z)"
    2.85 -by (erule listrel.induct, simp_all)
    2.86 +  by (induct set: listrel) simp_all
    2.87  
    2.88  lemma args_respects: "(%U. {Abs_ExpList (freeargs U)}) respects exprel"
    2.89  by (simp add: congruent_def Abs_ExpList_eq exprel_imp_eqv_freeargs) 
    2.90 @@ -426,19 +423,19 @@
    2.91  
    2.92  
    2.93  text{*The structural induction rule for the abstract type*}
    2.94 -theorem exp_induct:
    2.95 +theorem exp_inducts:
    2.96    assumes V:    "\<And>nat. P1 (Var nat)"
    2.97        and P:    "\<And>exp1 exp2. \<lbrakk>P1 exp1; P1 exp2\<rbrakk> \<Longrightarrow> P1 (Plus exp1 exp2)"
    2.98        and F:    "\<And>nat list. P2 list \<Longrightarrow> P1 (FnCall nat list)"
    2.99        and Nil:  "P2 []"
   2.100        and Cons: "\<And>exp list. \<lbrakk>P1 exp; P2 list\<rbrakk> \<Longrightarrow> P2 (exp # list)"
   2.101 -  shows "P1 exp & P2 list"
   2.102 -proof (cases exp, rule eq_Abs_ExpList [of list], clarify)  
   2.103 -  fix U Us
   2.104 -  show "P1 (Abs_Exp (exprel `` {U})) \<and>
   2.105 -        P2 (Abs_ExpList Us)"
   2.106 +  shows "P1 exp" and "P2 list"
   2.107 +proof -
   2.108 +  obtain U where exp: "exp = (Abs_Exp (exprel `` {U}))" by (cases exp)
   2.109 +  obtain Us where list: "list = Abs_ExpList Us" by (rule eq_Abs_ExpList)
   2.110 +  have "P1 (Abs_Exp (exprel `` {U}))" and "P2 (Abs_ExpList Us)"
   2.111    proof (induct U and Us)
   2.112 -    case (VAR nat) 
   2.113 +    case (VAR nat)
   2.114      with V show ?case by (simp add: Var_def) 
   2.115    next
   2.116      case (PLUS X Y)
   2.117 @@ -453,9 +450,9 @@
   2.118      with Nil show ?case by simp
   2.119    next
   2.120      case Cons_freeExp
   2.121 -     with Cons
   2.122 -    show ?case by simp
   2.123 +    with Cons show ?case by simp
   2.124    qed
   2.125 +  with exp and list show "P1 exp" and "P2 list" by (simp_all only:)
   2.126  qed
   2.127  
   2.128  end
     3.1 --- a/src/HOL/Isar_examples/NestedDatatype.thy	Thu Dec 22 00:28:41 2005 +0100
     3.2 +++ b/src/HOL/Isar_examples/NestedDatatype.thy	Thu Dec 22 00:28:43 2005 +0100
     3.3 @@ -27,10 +27,9 @@
     3.4   \medskip A simple lemma about composition of substitutions.
     3.5  *}
     3.6  
     3.7 -lemma
     3.8 -   "subst_term (subst_term f1 o f2) t =
     3.9 -      subst_term f1 (subst_term f2 t) &
    3.10 -    subst_term_list (subst_term f1 o f2) ts =
    3.11 +lemma "subst_term (subst_term f1 o f2) t =
    3.12 +      subst_term f1 (subst_term f2 t)"
    3.13 +  and "subst_term_list (subst_term f1 o f2) ts =
    3.14        subst_term_list f1 (subst_term_list f2 ts)"
    3.15    by (induct t and ts) simp_all
    3.16  
     4.1 --- a/src/HOL/Lambda/Eta.thy	Thu Dec 22 00:28:41 2005 +0100
     4.2 +++ b/src/HOL/Lambda/Eta.thy	Thu Dec 22 00:28:43 2005 +0100
     4.3 @@ -392,47 +392,46 @@
     4.4  *}
     4.5  
     4.6  theorem par_eta_beta: "s \<Rightarrow>\<^sub>\<eta> t \<Longrightarrow> t => u \<Longrightarrow> \<exists>t'. s => t' \<and> t' \<Rightarrow>\<^sub>\<eta> u"
     4.7 -proof (induct t fixing: s u
     4.8 -    rule: measure_induct [of size, rule_format])
     4.9 -  case (1 t)
    4.10 -  from 1(3)
    4.11 +proof (induct t fixing: s u taking: "size :: dB \<Rightarrow> nat" rule: measure_induct_rule)
    4.12 +  case (less t)
    4.13 +  from `t => u`
    4.14    show ?case
    4.15    proof cases
    4.16      case (var n)
    4.17 -    with 1 show ?thesis
    4.18 +    with less show ?thesis
    4.19        by (auto intro: par_beta_refl)
    4.20    next
    4.21      case (abs r' r'')
    4.22 -    with 1 have "s \<Rightarrow>\<^sub>\<eta> Abs r'" by simp
    4.23 +    with less have "s \<Rightarrow>\<^sub>\<eta> Abs r'" by simp
    4.24      then obtain r k where s: "s = eta_expand k (Abs r)" and rr: "r \<Rightarrow>\<^sub>\<eta> r'"
    4.25        by (blast dest: par_eta_elim_abs)
    4.26      from abs have "size r' < size t" by simp
    4.27      with abs(2) rr obtain t' where rt: "r => t'" and t': "t' \<Rightarrow>\<^sub>\<eta> r''"
    4.28 -      by (blast dest: 1)
    4.29 +      by (blast dest: less)
    4.30      with s abs show ?thesis
    4.31        by (auto intro: eta_expand_red eta_expand_eta)
    4.32    next
    4.33      case (app q' q'' r' r'')
    4.34 -    with 1 have "s \<Rightarrow>\<^sub>\<eta> q' \<degree> r'" by simp
    4.35 +    with less have "s \<Rightarrow>\<^sub>\<eta> q' \<degree> r'" by simp
    4.36      then obtain q r k where s: "s = eta_expand k (q \<degree> r)"
    4.37        and qq: "q \<Rightarrow>\<^sub>\<eta> q'" and rr: "r \<Rightarrow>\<^sub>\<eta> r'"
    4.38        by (blast dest: par_eta_elim_app [OF _ refl])
    4.39      from app have "size q' < size t" and "size r' < size t" by simp_all
    4.40      with app(2,3) qq rr obtain t' t'' where "q => t'" and
    4.41        "t' \<Rightarrow>\<^sub>\<eta> q''" and "r => t''" and "t'' \<Rightarrow>\<^sub>\<eta> r''"
    4.42 -      by (blast dest: 1)
    4.43 +      by (blast dest: less)
    4.44      with s app show ?thesis
    4.45        by (fastsimp intro: eta_expand_red eta_expand_eta)
    4.46    next
    4.47      case (beta q' q'' r' r'')
    4.48 -    with 1 have "s \<Rightarrow>\<^sub>\<eta> Abs q' \<degree> r'" by simp
    4.49 +    with less have "s \<Rightarrow>\<^sub>\<eta> Abs q' \<degree> r'" by simp
    4.50      then obtain q r k k' where s: "s = eta_expand k (eta_expand k' (Abs q) \<degree> r)"
    4.51        and qq: "q \<Rightarrow>\<^sub>\<eta> q'" and rr: "r \<Rightarrow>\<^sub>\<eta> r'"
    4.52        by (blast dest: par_eta_elim_app par_eta_elim_abs)
    4.53      from beta have "size q' < size t" and "size r' < size t" by simp_all
    4.54      with beta(2,3) qq rr obtain t' t'' where "q => t'" and
    4.55        "t' \<Rightarrow>\<^sub>\<eta> q''" and "r => t''" and "t'' \<Rightarrow>\<^sub>\<eta> r''"
    4.56 -      by (blast dest: 1)
    4.57 +      by (blast dest: less)
    4.58      with s beta show ?thesis
    4.59        by (auto intro: eta_expand_red eta_expand_beta eta_expand_eta par_eta_subst)
    4.60    qed
     5.1 --- a/src/ZF/Induct/Tree_Forest.thy	Thu Dec 22 00:28:41 2005 +0100
     5.2 +++ b/src/ZF/Induct/Tree_Forest.thy	Thu Dec 22 00:28:43 2005 +0100
     5.3 @@ -18,6 +18,12 @@
     5.4  datatype "tree(A)" = Tcons ("a \<in> A", "f \<in> forest(A)")
     5.5    and "forest(A)" = Fnil | Fcons ("t \<in> tree(A)", "f \<in> forest(A)")
     5.6  
     5.7 +(* FIXME *)
     5.8 +lemmas tree'induct =
     5.9 +    tree_forest.mutual_induct [THEN conjunct1, THEN spec, THEN [2] rev_mp, of concl: _ t, standard, consumes 1]
    5.10 +  and forest'induct =
    5.11 +    tree_forest.mutual_induct [THEN conjunct2, THEN spec, THEN [2] rev_mp, of concl: _ f, standard, consumes 1]
    5.12 +
    5.13  declare tree_forest.intros [simp, TC]
    5.14  
    5.15  lemma tree_def: "tree(A) == Part(tree_forest(A), Inl)"
    5.16 @@ -158,36 +164,28 @@
    5.17  
    5.18  lemma list_of_TF_type [TC]:
    5.19      "z \<in> tree_forest(A) ==> list_of_TF(z) \<in> list(tree(A))"
    5.20 -  apply (erule tree_forest.induct)
    5.21 -  apply simp_all
    5.22 -  done
    5.23 +  by (induct set: tree_forest) simp_all
    5.24  
    5.25  lemma of_list_type [TC]: "l \<in> list(tree(A)) ==> of_list(l) \<in> forest(A)"
    5.26 -  apply (erule list.induct)
    5.27 -  apply simp_all
    5.28 -  done
    5.29 +  by (induct set: list) simp_all
    5.30  
    5.31  text {*
    5.32    \medskip @{text map}.
    5.33  *}
    5.34  
    5.35  lemma
    5.36 -  assumes h_type: "!!x. x \<in> A ==> h(x): B"
    5.37 +  assumes "!!x. x \<in> A ==> h(x): B"
    5.38    shows map_tree_type: "t \<in> tree(A) ==> map(h,t) \<in> tree(B)"
    5.39      and map_forest_type: "f \<in> forest(A) ==> map(h,f) \<in> forest(B)"
    5.40 -  apply (induct rule: tree_forest.mutual_induct)
    5.41 -    apply (insert h_type)
    5.42 -    apply simp_all
    5.43 -  done
    5.44 +  using prems
    5.45 +  by (induct rule: tree'induct forest'induct) simp_all
    5.46  
    5.47  text {*
    5.48    \medskip @{text size}.
    5.49  *}
    5.50  
    5.51  lemma size_type [TC]: "z \<in> tree_forest(A) ==> size(z) \<in> nat"
    5.52 -  apply (erule tree_forest.induct)
    5.53 -  apply simp_all
    5.54 -  done
    5.55 +  by (induct set: tree_forest) simp_all
    5.56  
    5.57  
    5.58  text {*
    5.59 @@ -195,9 +193,7 @@
    5.60  *}
    5.61  
    5.62  lemma preorder_type [TC]: "z \<in> tree_forest(A) ==> preorder(z) \<in> list(A)"
    5.63 -  apply (erule tree_forest.induct)
    5.64 -  apply simp_all
    5.65 -  done
    5.66 +  by (induct set: tree_forest) simp_all
    5.67  
    5.68  
    5.69  text {*
    5.70 @@ -229,15 +225,11 @@
    5.71  *}
    5.72  
    5.73  lemma map_ident: "z \<in> tree_forest(A) ==> map(\<lambda>u. u, z) = z"
    5.74 -  apply (erule tree_forest.induct)
    5.75 -    apply simp_all
    5.76 -  done
    5.77 +  by (induct set: tree_forest) simp_all
    5.78  
    5.79  lemma map_compose:
    5.80      "z \<in> tree_forest(A) ==> map(h, map(j,z)) = map(\<lambda>u. h(j(u)), z)"
    5.81 -  apply (erule tree_forest.induct)
    5.82 -    apply simp_all
    5.83 -  done
    5.84 +  by (induct set: tree_forest) simp_all
    5.85  
    5.86  
    5.87  text {*
    5.88 @@ -245,14 +237,10 @@
    5.89  *}
    5.90  
    5.91  lemma size_map: "z \<in> tree_forest(A) ==> size(map(h,z)) = size(z)"
    5.92 -  apply (erule tree_forest.induct)
    5.93 -    apply simp_all
    5.94 -  done
    5.95 +  by (induct set: tree_forest) simp_all
    5.96  
    5.97  lemma size_length: "z \<in> tree_forest(A) ==> size(z) = length(preorder(z))"
    5.98 -  apply (erule tree_forest.induct)
    5.99 -    apply (simp_all add: length_app)
   5.100 -  done
   5.101 +  by (induct set: tree_forest) (simp_all add: length_app)
   5.102  
   5.103  text {*
   5.104    \medskip Theorems about @{text preorder}.
   5.105 @@ -260,8 +248,6 @@
   5.106  
   5.107  lemma preorder_map:
   5.108      "z \<in> tree_forest(A) ==> preorder(map(h,z)) = List.map(h, preorder(z))"
   5.109 -  apply (erule tree_forest.induct)
   5.110 -    apply (simp_all add: map_app_distrib)
   5.111 -  done
   5.112 +  by (induct set: tree_forest) (simp_all add: map_app_distrib)
   5.113  
   5.114  end