--- a/src/HOL/Induct/QuoDataType.thy Thu Dec 22 00:28:41 2005 +0100
+++ b/src/HOL/Induct/QuoDataType.thy Thu Dec 22 00:28:43 2005 +0100
@@ -49,13 +49,14 @@
text{*Proving that it is an equivalence relation*}
lemma msgrel_refl: "X \<sim> X"
-by (induct X, (blast intro: msgrel.intros)+)
+ by (induct X) (blast intro: msgrel.intros)+
theorem equiv_msgrel: "equiv UNIV msgrel"
-proof (simp add: equiv_def, intro conjI)
- show "reflexive msgrel" by (simp add: refl_def msgrel_refl)
- show "sym msgrel" by (simp add: sym_def, blast intro: msgrel.SYM)
- show "trans msgrel" by (simp add: trans_def, blast intro: msgrel.TRANS)
+proof -
+ have "reflexive msgrel" by (simp add: refl_def msgrel_refl)
+ moreover have "sym msgrel" by (simp add: sym_def, blast intro: msgrel.SYM)
+ moreover have "trans msgrel" by (simp add: trans_def, blast intro: msgrel.TRANS)
+ ultimately show ?thesis by (simp add: equiv_def)
qed
@@ -78,7 +79,7 @@
equivalence relation. It also helps us prove that Nonce
(the abstract constructor) is injective*}
theorem msgrel_imp_eq_freenonces: "U \<sim> V \<Longrightarrow> freenonces U = freenonces V"
-by (erule msgrel.induct, auto)
+ by (induct set: msgrel) auto
subsubsection{*The Left Projection*}
@@ -97,7 +98,7 @@
(the abstract constructor) is injective*}
theorem msgrel_imp_eqv_freeleft:
"U \<sim> V \<Longrightarrow> freeleft U \<sim> freeleft V"
-by (erule msgrel.induct, auto intro: msgrel.intros)
+ by (induct set: msgrel) (auto intro: msgrel.intros)
subsubsection{*The Right Projection*}
@@ -115,7 +116,7 @@
(the abstract constructor) is injective*}
theorem msgrel_imp_eqv_freeright:
"U \<sim> V \<Longrightarrow> freeright U \<sim> freeright V"
-by (erule msgrel.induct, auto intro: msgrel.intros)
+ by (induct set: msgrel) (auto intro: msgrel.intros)
subsubsection{*The Discriminator for Constructors*}
@@ -131,13 +132,13 @@
text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*}
theorem msgrel_imp_eq_freediscrim:
"U \<sim> V \<Longrightarrow> freediscrim U = freediscrim V"
-by (erule msgrel.induct, auto)
+ by (induct set: msgrel) auto
subsection{*The Initial Algebra: A Quotiented Message Type*}
typedef (Msg) msg = "UNIV//msgrel"
- by (auto simp add: quotient_def)
+ by (auto simp add: quotient_def)
text{*The abstract message constructors*}
@@ -402,9 +403,9 @@
and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)"
and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)"
shows "P msg"
-proof (cases msg, erule ssubst)
- fix U::freemsg
- show "P (Abs_Msg (msgrel `` {U}))"
+proof (cases msg)
+ case (Abs_Msg U)
+ have "P (Abs_Msg (msgrel `` {U}))"
proof (induct U)
case (NONCE N)
with N show ?case by (simp add: Nonce_def)
@@ -421,6 +422,7 @@
with D [of "Abs_Msg (msgrel `` {X})"]
show ?case by (simp add: Decrypt)
qed
+ with Abs_Msg show ?thesis by (simp only:)
qed
--- a/src/HOL/Induct/QuoNestedDataType.thy Thu Dec 22 00:28:41 2005 +0100
+++ b/src/HOL/Induct/QuoNestedDataType.thy Thu Dec 22 00:28:43 2005 +0100
@@ -45,23 +45,20 @@
text{*Proving that it is an equivalence relation*}
-lemma exprel_refl_conj: "X \<sim> X & (Xs,Xs) \<in> listrel(exprel)"
-apply (induct X and Xs)
-apply (blast intro: exprel.intros listrel.intros)+
-done
-
-lemmas exprel_refl = exprel_refl_conj [THEN conjunct1]
-lemmas list_exprel_refl = exprel_refl_conj [THEN conjunct2]
+lemma exprel_refl: "X \<sim> X"
+ and list_exprel_refl: "(Xs,Xs) \<in> listrel(exprel)"
+ by (induct X and Xs) (blast intro: exprel.intros listrel.intros)+
theorem equiv_exprel: "equiv UNIV exprel"
-proof (simp add: equiv_def, intro conjI)
- show "reflexive exprel" by (simp add: refl_def exprel_refl)
- show "sym exprel" by (simp add: sym_def, blast intro: exprel.SYM)
- show "trans exprel" by (simp add: trans_def, blast intro: exprel.TRANS)
+proof -
+ have "reflexive exprel" by (simp add: refl_def exprel_refl)
+ moreover have "sym exprel" by (simp add: sym_def, blast intro: exprel.SYM)
+ moreover have "trans exprel" by (simp add: trans_def, blast intro: exprel.TRANS)
+ ultimately show ?thesis by (simp add: equiv_def)
qed
theorem equiv_list_exprel: "equiv UNIV (listrel exprel)"
-by (insert equiv_listrel [OF equiv_exprel], simp)
+ using equiv_listrel [OF equiv_exprel] by simp
lemma FNCALL_Nil: "FNCALL F [] \<sim> FNCALL F []"
@@ -100,7 +97,7 @@
equivalence relation. It also helps us prove that Variable
(the abstract constructor) is injective*}
theorem exprel_imp_eq_freevars: "U \<sim> V \<Longrightarrow> freevars U = freevars V"
-apply (erule exprel.induct)
+apply (induct set: exprel)
apply (erule_tac [4] listrel.induct)
apply (simp_all add: Un_assoc)
done
@@ -118,7 +115,7 @@
theorem exprel_imp_eq_freediscrim:
"U \<sim> V \<Longrightarrow> freediscrim U = freediscrim V"
-by (erule exprel.induct, auto)
+ by (induct set: exprel) auto
text{*This function, which returns the function name, is used to
@@ -132,7 +129,7 @@
theorem exprel_imp_eq_freefun:
"U \<sim> V \<Longrightarrow> freefun U = freefun V"
-by (erule exprel.induct, simp_all add: listrel.intros)
+ by (induct set: exprel) (simp_all add: listrel.intros)
text{*This function, which returns the list of function arguments, is used to
@@ -145,7 +142,7 @@
theorem exprel_imp_eqv_freeargs:
"U \<sim> V \<Longrightarrow> (freeargs U, freeargs V) \<in> listrel exprel"
-apply (erule exprel.induct)
+apply (induct set: exprel)
apply (erule_tac [4] listrel.induct)
apply (simp_all add: listrel.intros)
apply (blast intro: symD [OF equiv.sym [OF equiv_list_exprel]])
@@ -265,7 +262,7 @@
lemma listset_Rep_Exp_Abs_Exp:
"listset (map Rep_Exp (Abs_ExpList Us)) = listrel exprel `` {Us}";
-by (induct Us, simp_all add: listrel_Cons Abs_ExpList_def)
+ by (induct Us) (simp_all add: listrel_Cons Abs_ExpList_def)
lemma FnCall:
"FnCall F (Abs_ExpList Us) = Abs_Exp (exprel``{FNCALL F Us})"
@@ -372,7 +369,7 @@
relations, but with little benefit here.*}
lemma Abs_ExpList_eq:
"(y, z) \<in> listrel exprel \<Longrightarrow> Abs_ExpList (y) = Abs_ExpList (z)"
-by (erule listrel.induct, simp_all)
+ by (induct set: listrel) simp_all
lemma args_respects: "(%U. {Abs_ExpList (freeargs U)}) respects exprel"
by (simp add: congruent_def Abs_ExpList_eq exprel_imp_eqv_freeargs)
@@ -426,19 +423,19 @@
text{*The structural induction rule for the abstract type*}
-theorem exp_induct:
+theorem exp_inducts:
assumes V: "\<And>nat. P1 (Var nat)"
and P: "\<And>exp1 exp2. \<lbrakk>P1 exp1; P1 exp2\<rbrakk> \<Longrightarrow> P1 (Plus exp1 exp2)"
and F: "\<And>nat list. P2 list \<Longrightarrow> P1 (FnCall nat list)"
and Nil: "P2 []"
and Cons: "\<And>exp list. \<lbrakk>P1 exp; P2 list\<rbrakk> \<Longrightarrow> P2 (exp # list)"
- shows "P1 exp & P2 list"
-proof (cases exp, rule eq_Abs_ExpList [of list], clarify)
- fix U Us
- show "P1 (Abs_Exp (exprel `` {U})) \<and>
- P2 (Abs_ExpList Us)"
+ shows "P1 exp" and "P2 list"
+proof -
+ obtain U where exp: "exp = (Abs_Exp (exprel `` {U}))" by (cases exp)
+ obtain Us where list: "list = Abs_ExpList Us" by (rule eq_Abs_ExpList)
+ have "P1 (Abs_Exp (exprel `` {U}))" and "P2 (Abs_ExpList Us)"
proof (induct U and Us)
- case (VAR nat)
+ case (VAR nat)
with V show ?case by (simp add: Var_def)
next
case (PLUS X Y)
@@ -453,9 +450,9 @@
with Nil show ?case by simp
next
case Cons_freeExp
- with Cons
- show ?case by simp
+ with Cons show ?case by simp
qed
+ with exp and list show "P1 exp" and "P2 list" by (simp_all only:)
qed
end
--- a/src/HOL/Isar_examples/NestedDatatype.thy Thu Dec 22 00:28:41 2005 +0100
+++ b/src/HOL/Isar_examples/NestedDatatype.thy Thu Dec 22 00:28:43 2005 +0100
@@ -27,10 +27,9 @@
\medskip A simple lemma about composition of substitutions.
*}
-lemma
- "subst_term (subst_term f1 o f2) t =
- subst_term f1 (subst_term f2 t) &
- subst_term_list (subst_term f1 o f2) ts =
+lemma "subst_term (subst_term f1 o f2) t =
+ subst_term f1 (subst_term f2 t)"
+ and "subst_term_list (subst_term f1 o f2) ts =
subst_term_list f1 (subst_term_list f2 ts)"
by (induct t and ts) simp_all
--- a/src/HOL/Lambda/Eta.thy Thu Dec 22 00:28:41 2005 +0100
+++ b/src/HOL/Lambda/Eta.thy Thu Dec 22 00:28:43 2005 +0100
@@ -392,47 +392,46 @@
*}
theorem par_eta_beta: "s \<Rightarrow>\<^sub>\<eta> t \<Longrightarrow> t => u \<Longrightarrow> \<exists>t'. s => t' \<and> t' \<Rightarrow>\<^sub>\<eta> u"
-proof (induct t fixing: s u
- rule: measure_induct [of size, rule_format])
- case (1 t)
- from 1(3)
+proof (induct t fixing: s u taking: "size :: dB \<Rightarrow> nat" rule: measure_induct_rule)
+ case (less t)
+ from `t => u`
show ?case
proof cases
case (var n)
- with 1 show ?thesis
+ with less show ?thesis
by (auto intro: par_beta_refl)
next
case (abs r' r'')
- with 1 have "s \<Rightarrow>\<^sub>\<eta> Abs r'" by simp
+ with less have "s \<Rightarrow>\<^sub>\<eta> Abs r'" by simp
then obtain r k where s: "s = eta_expand k (Abs r)" and rr: "r \<Rightarrow>\<^sub>\<eta> r'"
by (blast dest: par_eta_elim_abs)
from abs have "size r' < size t" by simp
with abs(2) rr obtain t' where rt: "r => t'" and t': "t' \<Rightarrow>\<^sub>\<eta> r''"
- by (blast dest: 1)
+ by (blast dest: less)
with s abs show ?thesis
by (auto intro: eta_expand_red eta_expand_eta)
next
case (app q' q'' r' r'')
- with 1 have "s \<Rightarrow>\<^sub>\<eta> q' \<degree> r'" by simp
+ with less have "s \<Rightarrow>\<^sub>\<eta> q' \<degree> r'" by simp
then obtain q r k where s: "s = eta_expand k (q \<degree> r)"
and qq: "q \<Rightarrow>\<^sub>\<eta> q'" and rr: "r \<Rightarrow>\<^sub>\<eta> r'"
by (blast dest: par_eta_elim_app [OF _ refl])
from app have "size q' < size t" and "size r' < size t" by simp_all
with app(2,3) qq rr obtain t' t'' where "q => t'" and
"t' \<Rightarrow>\<^sub>\<eta> q''" and "r => t''" and "t'' \<Rightarrow>\<^sub>\<eta> r''"
- by (blast dest: 1)
+ by (blast dest: less)
with s app show ?thesis
by (fastsimp intro: eta_expand_red eta_expand_eta)
next
case (beta q' q'' r' r'')
- with 1 have "s \<Rightarrow>\<^sub>\<eta> Abs q' \<degree> r'" by simp
+ with less have "s \<Rightarrow>\<^sub>\<eta> Abs q' \<degree> r'" by simp
then obtain q r k k' where s: "s = eta_expand k (eta_expand k' (Abs q) \<degree> r)"
and qq: "q \<Rightarrow>\<^sub>\<eta> q'" and rr: "r \<Rightarrow>\<^sub>\<eta> r'"
by (blast dest: par_eta_elim_app par_eta_elim_abs)
from beta have "size q' < size t" and "size r' < size t" by simp_all
with beta(2,3) qq rr obtain t' t'' where "q => t'" and
"t' \<Rightarrow>\<^sub>\<eta> q''" and "r => t''" and "t'' \<Rightarrow>\<^sub>\<eta> r''"
- by (blast dest: 1)
+ by (blast dest: less)
with s beta show ?thesis
by (auto intro: eta_expand_red eta_expand_beta eta_expand_eta par_eta_subst)
qed
--- a/src/ZF/Induct/Tree_Forest.thy Thu Dec 22 00:28:41 2005 +0100
+++ b/src/ZF/Induct/Tree_Forest.thy Thu Dec 22 00:28:43 2005 +0100
@@ -18,6 +18,12 @@
datatype "tree(A)" = Tcons ("a \<in> A", "f \<in> forest(A)")
and "forest(A)" = Fnil | Fcons ("t \<in> tree(A)", "f \<in> forest(A)")
+(* FIXME *)
+lemmas tree'induct =
+ tree_forest.mutual_induct [THEN conjunct1, THEN spec, THEN [2] rev_mp, of concl: _ t, standard, consumes 1]
+ and forest'induct =
+ tree_forest.mutual_induct [THEN conjunct2, THEN spec, THEN [2] rev_mp, of concl: _ f, standard, consumes 1]
+
declare tree_forest.intros [simp, TC]
lemma tree_def: "tree(A) == Part(tree_forest(A), Inl)"
@@ -158,36 +164,28 @@
lemma list_of_TF_type [TC]:
"z \<in> tree_forest(A) ==> list_of_TF(z) \<in> list(tree(A))"
- apply (erule tree_forest.induct)
- apply simp_all
- done
+ by (induct set: tree_forest) simp_all
lemma of_list_type [TC]: "l \<in> list(tree(A)) ==> of_list(l) \<in> forest(A)"
- apply (erule list.induct)
- apply simp_all
- done
+ by (induct set: list) simp_all
text {*
\medskip @{text map}.
*}
lemma
- assumes h_type: "!!x. x \<in> A ==> h(x): B"
+ assumes "!!x. x \<in> A ==> h(x): B"
shows map_tree_type: "t \<in> tree(A) ==> map(h,t) \<in> tree(B)"
and map_forest_type: "f \<in> forest(A) ==> map(h,f) \<in> forest(B)"
- apply (induct rule: tree_forest.mutual_induct)
- apply (insert h_type)
- apply simp_all
- done
+ using prems
+ by (induct rule: tree'induct forest'induct) simp_all
text {*
\medskip @{text size}.
*}
lemma size_type [TC]: "z \<in> tree_forest(A) ==> size(z) \<in> nat"
- apply (erule tree_forest.induct)
- apply simp_all
- done
+ by (induct set: tree_forest) simp_all
text {*
@@ -195,9 +193,7 @@
*}
lemma preorder_type [TC]: "z \<in> tree_forest(A) ==> preorder(z) \<in> list(A)"
- apply (erule tree_forest.induct)
- apply simp_all
- done
+ by (induct set: tree_forest) simp_all
text {*
@@ -229,15 +225,11 @@
*}
lemma map_ident: "z \<in> tree_forest(A) ==> map(\<lambda>u. u, z) = z"
- apply (erule tree_forest.induct)
- apply simp_all
- done
+ by (induct set: tree_forest) simp_all
lemma map_compose:
"z \<in> tree_forest(A) ==> map(h, map(j,z)) = map(\<lambda>u. h(j(u)), z)"
- apply (erule tree_forest.induct)
- apply simp_all
- done
+ by (induct set: tree_forest) simp_all
text {*
@@ -245,14 +237,10 @@
*}
lemma size_map: "z \<in> tree_forest(A) ==> size(map(h,z)) = size(z)"
- apply (erule tree_forest.induct)
- apply simp_all
- done
+ by (induct set: tree_forest) simp_all
lemma size_length: "z \<in> tree_forest(A) ==> size(z) = length(preorder(z))"
- apply (erule tree_forest.induct)
- apply (simp_all add: length_app)
- done
+ by (induct set: tree_forest) (simp_all add: length_app)
text {*
\medskip Theorems about @{text preorder}.
@@ -260,8 +248,6 @@
lemma preorder_map:
"z \<in> tree_forest(A) ==> preorder(map(h,z)) = List.map(h, preorder(z))"
- apply (erule tree_forest.induct)
- apply (simp_all add: map_app_distrib)
- done
+ by (induct set: tree_forest) (simp_all add: map_app_distrib)
end