--- a/src/ZF/Induct/Binary_Trees.thy Thu Dec 15 19:42:02 2005 +0100
+++ b/src/ZF/Induct/Binary_Trees.thy Thu Dec 15 19:42:03 2005 +0100
@@ -18,8 +18,8 @@
declare bt.intros [simp]
-lemma Br_neq_left: "l \<in> bt(A) ==> (!!x r. Br(x, l, r) \<noteq> l)"
- by (induct set: bt) auto
+lemma Br_neq_left: "l \<in> bt(A) ==> Br(x, l, r) \<noteq> l"
+ by (induct fixing: x r set: bt) auto
lemma Br_iff: "Br(a, l, r) = Br(a', l', r') <-> a = a' & l = l' & r = r'"
-- "Proving a freeness theorem."
@@ -73,24 +73,27 @@
"n_nodes(Br(a, l, r)) = succ(n_nodes(l) #+ n_nodes(r))"
lemma n_nodes_type [simp]: "t \<in> bt(A) ==> n_nodes(t) \<in> nat"
- by (induct_tac t) auto
+ by (induct set: bt) auto
consts n_nodes_aux :: "i => i"
primrec
"n_nodes_aux(Lf) = (\<lambda>k \<in> nat. k)"
- "n_nodes_aux(Br(a, l, r)) =
+ "n_nodes_aux(Br(a, l, r)) =
(\<lambda>k \<in> nat. n_nodes_aux(r) ` (n_nodes_aux(l) ` succ(k)))"
-lemma n_nodes_aux_eq [rule_format]:
- "t \<in> bt(A) ==> \<forall>k \<in> nat. n_nodes_aux(t)`k = n_nodes(t) #+ k"
- by (induct_tac t, simp_all)
+lemma n_nodes_aux_eq:
+ "t \<in> bt(A) ==> k \<in> nat ==> n_nodes_aux(t)`k = n_nodes(t) #+ k"
+ apply (induct fixing: k set: bt)
+ apply simp
+ apply (atomize, simp)
+ done
constdefs
n_nodes_tail :: "i => i"
- "n_nodes_tail(t) == n_nodes_aux(t) ` 0"
+ "n_nodes_tail(t) == n_nodes_aux(t) ` 0"
lemma "t \<in> bt(A) ==> n_nodes_tail(t) = n_nodes(t)"
- by (simp add: n_nodes_tail_def n_nodes_aux_eq)
+ by (simp add: n_nodes_tail_def n_nodes_aux_eq)
subsection {* Number of leaves *}
@@ -102,7 +105,7 @@
"n_leaves(Br(a, l, r)) = n_leaves(l) #+ n_leaves(r)"
lemma n_leaves_type [simp]: "t \<in> bt(A) ==> n_leaves(t) \<in> nat"
- by (induct_tac t) auto
+ by (induct set: bt) auto
subsection {* Reflecting trees *}
@@ -114,23 +117,23 @@
"bt_reflect(Br(a, l, r)) = Br(a, bt_reflect(r), bt_reflect(l))"
lemma bt_reflect_type [simp]: "t \<in> bt(A) ==> bt_reflect(t) \<in> bt(A)"
- by (induct_tac t) auto
+ by (induct set: bt) auto
text {*
\medskip Theorems about @{term n_leaves}.
*}
lemma n_leaves_reflect: "t \<in> bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)"
- by (induct_tac t) (simp_all add: add_commute n_leaves_type)
+ by (induct set: bt) (simp_all add: add_commute n_leaves_type)
lemma n_leaves_nodes: "t \<in> bt(A) ==> n_leaves(t) = succ(n_nodes(t))"
- by (induct_tac t) (simp_all add: add_succ_right)
+ by (induct set: bt) (simp_all add: add_succ_right)
text {*
Theorems about @{term bt_reflect}.
*}
lemma bt_reflect_bt_reflect_ident: "t \<in> bt(A) ==> bt_reflect(bt_reflect(t)) = t"
- by (induct_tac t) simp_all
+ by (induct set: bt) simp_all
end
--- a/src/ZF/Induct/Comb.thy Thu Dec 15 19:42:02 2005 +0100
+++ b/src/ZF/Induct/Comb.thy Thu Dec 15 19:42:03 2005 +0100
@@ -247,7 +247,7 @@
*}
lemma contract_imp_parcontract: "p-1->q ==> p=1=>q"
- by (erule contract.induct) auto
+ by (induct set: contract) auto
lemma reduce_imp_parreduce: "p--->q ==> p===>q"
apply (frule rtrancl_type [THEN subsetD, THEN SigmaD1])
@@ -259,7 +259,7 @@
done
lemma parcontract_imp_reduce: "p=1=>q ==> p--->q"
- apply (erule parcontract.induct)
+ apply (induct set: parcontract)
apply (blast intro: reduction_rls)
apply (blast intro: reduction_rls)
apply (blast intro: reduction_rls)
--- a/src/ZF/Induct/ListN.thy Thu Dec 15 19:42:02 2005 +0100
+++ b/src/ZF/Induct/ListN.thy Thu Dec 15 19:42:03 2005 +0100
@@ -23,7 +23,7 @@
lemma list_into_listn: "l \<in> list(A) ==> <length(l),l> \<in> listn(A)"
- by (erule list.induct) (simp_all add: listn.intros)
+ by (induct set: list) (simp_all add: listn.intros)
lemma listn_iff: "<n,l> \<in> listn(A) <-> l \<in> list(A) & length(l)=n"
apply (rule iffI)
--- a/src/ZF/Induct/Multiset.thy Thu Dec 15 19:42:02 2005 +0100
+++ b/src/ZF/Induct/Multiset.thy Thu Dec 15 19:42:03 2005 +0100
@@ -372,7 +372,8 @@
lemma setsum_mcount_Int:
"Finite(A) ==> setsum(%a. $# mcount(N, a), A Int mset_of(N))
= setsum(%a. $# mcount(N, a), A)"
-apply (erule Finite_induct, auto)
+apply (induct rule: Finite_induct)
+ apply auto
apply (subgoal_tac "Finite (B Int mset_of (N))")
prefer 2 apply (blast intro: subset_Finite)
apply (auto simp add: mcount_def Int_cons_left)
@@ -434,7 +435,7 @@
by (auto simp add: multiset_equality)
lemma nat_add_eq_1_cases: "[| m \<in> nat; n \<in> nat |] ==> (m #+ n = 1) <-> (m=1 & n=0) | (m=0 & n=1)"
-by (induct_tac "n", auto)
+by (induct_tac n) auto
lemma munion_is_single:
"[|multiset(M); multiset(N)|]
--- a/src/ZF/Induct/Mutil.thy Thu Dec 15 19:42:02 2005 +0100
+++ b/src/ZF/Induct/Mutil.thy Thu Dec 15 19:42:03 2005 +0100
@@ -92,13 +92,13 @@
done
lemma tiling_domino_Finite: "t \<in> tiling(domino) ==> Finite(t)"
- apply (induct rule: tiling.induct)
+ apply (induct set: tiling)
apply (rule Finite_0)
apply (blast intro!: Finite_Un intro: domino_Finite)
done
lemma tiling_domino_0_1: "t \<in> tiling(domino) ==> |evnodd(t,0)| = |evnodd(t,1)|"
- apply (induct rule: tiling.induct)
+ apply (induct set: tiling)
apply (simp add: evnodd_def)
apply (rule_tac b1 = 0 in domino_singleton [THEN exE])
prefer 2
--- a/src/ZF/Induct/Primrec.thy Thu Dec 15 19:42:02 2005 +0100
+++ b/src/ZF/Induct/Primrec.thy Thu Dec 15 19:42:03 2005 +0100
@@ -104,7 +104,7 @@
declare rec_type [TC]
lemma ACK_in_prim_rec [TC]: "i \<in> nat ==> ACK(i) \<in> prim_rec"
- by (induct_tac i) simp_all
+ by (induct set: nat) simp_all
lemma ack_type [TC]: "[| i \<in> nat; j \<in> nat |] ==> ack(i,j) \<in> nat"
by auto
@@ -129,11 +129,10 @@
and [simp del] = ACK.simps
-lemma lt_ack2 [rule_format]: "i \<in> nat ==> \<forall>j \<in> nat. j < ack(i,j)"
+lemma lt_ack2: "i \<in> nat ==> j \<in> nat ==> j < ack(i,j)"
-- {* PROPERTY A 4 *}
- apply (induct_tac i)
+ apply (induct i fixing: j set: nat)
apply simp
- apply (rule ballI)
apply (induct_tac j)
apply (erule_tac [2] succ_leI [THEN lt_trans1])
apply (rule nat_0I [THEN nat_0_le, THEN lt_trans])
@@ -142,7 +141,7 @@
lemma ack_lt_ack_succ2: "[|i\<in>nat; j\<in>nat|] ==> ack(i,j) < ack(i, succ(j))"
-- {* PROPERTY A 5-, the single-step lemma *}
- by (induct_tac i) (simp_all add: lt_ack2)
+ by (induct set: nat) (simp_all add: lt_ack2)
lemma ack_lt_mono2: "[| j<k; i \<in> nat; k \<in> nat |] ==> ack(i,j) < ack(i,k)"
-- {* PROPERTY A 5, monotonicity for @{text "<"} *}
@@ -193,11 +192,11 @@
lemma ack_1: "j \<in> nat ==> ack(1,j) = succ(succ(j))"
-- {* PROPERTY A 8 *}
- by (induct_tac j) simp_all
+ by (induct set: nat) simp_all
lemma ack_2: "j \<in> nat ==> ack(succ(1),j) = succ(succ(succ(j#+j)))"
-- {* PROPERTY A 9 *}
- by (induct_tac j) (simp_all add: ack_1)
+ by (induct set: nat) (simp_all add: ack_1)
lemma ack_nest_bound:
"[| i1 \<in> nat; i2 \<in> nat; j \<in> nat |]
@@ -281,7 +280,7 @@
"fs \<in> list({f \<in> prim_rec. \<exists>kf \<in> nat. \<forall>l \<in> list(nat). f`l < ack(kf, list_add(l))})
==> \<exists>k \<in> nat. \<forall>l \<in> list(nat).
list_add(map(\<lambda>f. f ` l, fs)) < ack(k, list_add(l))"
- apply (erule list.induct)
+ apply (induct set: list)
apply (rule_tac x = 0 in bexI)
apply (simp_all add: lt_ack1 nat_0_le)
apply clarify
@@ -359,7 +358,7 @@
lemma ack_bounds_prim_rec:
"f \<in> prim_rec ==> \<exists>k \<in> nat. \<forall>l \<in> list(nat). f`l < ack(k, list_add(l))"
- apply (erule prim_rec.induct)
+ apply (induct set: prim_rec)
apply (auto intro: SC_case CONST_case PROJ_case COMP_case PREC_case)
done
--- a/src/ZF/Induct/PropLog.thy Thu Dec 15 19:42:02 2005 +0100
+++ b/src/ZF/Induct/PropLog.thy Thu Dec 15 19:42:03 2005 +0100
@@ -180,7 +180,7 @@
theorem soundness: "H |- p ==> H |= p"
apply (unfold logcon_def)
- apply (erule thms.induct)
+ apply (induct set: thms)
apply auto
done
@@ -256,7 +256,7 @@
lemma hyps_Diff:
"p \<in> propn ==> hyps(p, t-{v}) \<subseteq> cons(#v=>Fls, hyps(p,t)-{#v})"
- by (induct_tac p) auto
+ by (induct set: propn) auto
text {*
For the case @{prop "hyps(p,t)-cons(#v => Fls,Y) |- p"} we also have
@@ -265,7 +265,7 @@
lemma hyps_cons:
"p \<in> propn ==> hyps(p, cons(v,t)) \<subseteq> cons(#v, hyps(p,t)-{#v=>Fls})"
- by (induct_tac p) auto
+ by (induct set: propn) auto
text {* Two lemmas for use with @{text weaken_left} *}
@@ -282,7 +282,7 @@
*}
lemma hyps_finite: "p \<in> propn ==> hyps(p,t) \<in> Fin(\<Union>v \<in> nat. {#v, #v=>Fls})"
- by (induct_tac p) auto
+ by (induct set: propn) auto
lemmas Diff_weaken_left = Diff_mono [OF _ subset_refl, THEN weaken_left]
@@ -325,9 +325,9 @@
-- {* A semantic analogue of the Deduction Theorem *}
by (simp add: logcon_def)
-lemma completeness [rule_format]:
- "H \<in> Fin(propn) ==> \<forall>p \<in> propn. H |= p --> H |- p"
- apply (erule Fin_induct)
+lemma completeness:
+ "H \<in> Fin(propn) ==> p \<in> propn \<Longrightarrow> H |= p \<Longrightarrow> H |- p"
+ apply (induct fixing: p set: Fin)
apply (safe intro!: completeness_0)
apply (rule weaken_left_cons [THEN thms_MP])
apply (blast intro!: logcon_Imp propn.intros)
--- a/src/ZF/Induct/Term.thy Thu Dec 15 19:42:02 2005 +0100
+++ b/src/ZF/Induct/Term.thy Thu Dec 15 19:42:03 2005 +0100
@@ -58,7 +58,7 @@
apply (auto dest: list_CollectD)
done
-lemma term_induct_eqn:
+lemma term_induct_eqn [consumes 1, case_names Apply]:
"[| t \<in> term(A);
!!x zs. [| x \<in> A; zs: list(term(A)); map(f,zs) = map(g,zs) |] ==>
f(Apply(x,zs)) = g(Apply(x,zs))
@@ -122,27 +122,21 @@
done
lemma term_rec_type:
- "[| t \<in> term(A);
- !!x zs r. [| x \<in> A; zs: list(term(A));
- r \<in> list(\<Union>t \<in> term(A). C(t)) |]
- ==> d(x, zs, r): C(Apply(x,zs))
- |] ==> term_rec(t,d) \<in> C(t)"
- -- {* Slightly odd typing condition on @{text r} in the second premise! *}
-proof -
- assume a: "!!x zs r. [| x \<in> A; zs: list(term(A));
+ assumes t: "t \<in> term(A)"
+ and a: "!!x zs r. [| x \<in> A; zs: list(term(A));
r \<in> list(\<Union>t \<in> term(A). C(t)) |]
==> d(x, zs, r): C(Apply(x,zs))"
- assume "t \<in> term(A)"
- thus ?thesis
- apply induct
- apply (frule list_CollectD)
- apply (subst term_rec)
- apply (assumption | rule a)+
- apply (erule list.induct)
- apply (simp add: term_rec)
- apply (auto simp add: term_rec)
- done
-qed
+ shows "term_rec(t,d) \<in> C(t)"
+ -- {* Slightly odd typing condition on @{text r} in the second premise! *}
+ using t
+ apply induct
+ apply (frule list_CollectD)
+ apply (subst term_rec)
+ apply (assumption | rule a)+
+ apply (erule list.induct)
+ apply (simp add: term_rec)
+ apply (auto simp add: term_rec)
+ done
lemma def_term_rec:
"[| !!t. j(t)==term_rec(t,d); ts: list(A) |] ==>
@@ -239,21 +233,15 @@
declare List.map_compose [simp]
lemma term_map_ident: "t \<in> term(A) ==> term_map(\<lambda>u. u, t) = t"
- apply (erule term_induct_eqn)
- apply simp
- done
+ by (induct rule: term_induct_eqn) simp
lemma term_map_compose:
"t \<in> term(A) ==> term_map(f, term_map(g,t)) = term_map(\<lambda>u. f(g(u)), t)"
- apply (erule term_induct_eqn)
- apply simp
- done
+ by (induct rule: term_induct_eqn) simp
lemma term_map_reflect:
"t \<in> term(A) ==> term_map(f, reflect(t)) = reflect(term_map(f,t))"
- apply (erule term_induct_eqn)
- apply (simp add: rev_map_distrib [symmetric])
- done
+ by (induct rule: term_induct_eqn) (simp add: rev_map_distrib [symmetric])
text {*
@@ -261,19 +249,13 @@
*}
lemma term_size_term_map: "t \<in> term(A) ==> term_size(term_map(f,t)) = term_size(t)"
- apply (erule term_induct_eqn)
- apply simp
- done
+ by (induct rule: term_induct_eqn) simp
lemma term_size_reflect: "t \<in> term(A) ==> term_size(reflect(t)) = term_size(t)"
- apply (erule term_induct_eqn)
- apply (simp add: rev_map_distrib [symmetric] list_add_rev)
- done
+ by (induct rule: term_induct_eqn) (simp add: rev_map_distrib [symmetric] list_add_rev)
lemma term_size_length: "t \<in> term(A) ==> term_size(t) = length(preorder(t))"
- apply (erule term_induct_eqn)
- apply (simp add: length_flat)
- done
+ by (induct rule: term_induct_eqn) (simp add: length_flat)
text {*
@@ -281,9 +263,7 @@
*}
lemma reflect_reflect_ident: "t \<in> term(A) ==> reflect(reflect(t)) = t"
- apply (erule term_induct_eqn)
- apply (simp add: rev_map_distrib)
- done
+ by (induct rule: term_induct_eqn) (simp add: rev_map_distrib)
text {*
@@ -292,14 +272,11 @@
lemma preorder_term_map:
"t \<in> term(A) ==> preorder(term_map(f,t)) = map(f, preorder(t))"
- apply (erule term_induct_eqn)
- apply (simp add: map_flat)
- done
+ by (induct rule: term_induct_eqn) (simp add: map_flat)
lemma preorder_reflect_eq_rev_postorder:
"t \<in> term(A) ==> preorder(reflect(t)) = rev(postorder(t))"
- apply (erule term_induct_eqn)
- apply (simp add: rev_app_distrib rev_flat rev_map_distrib [symmetric])
- done
+ by (induct rule: term_induct_eqn)
+ (simp add: rev_app_distrib rev_flat rev_map_distrib [symmetric])
end
--- a/src/ZF/Induct/Tree_Forest.thy Thu Dec 15 19:42:02 2005 +0100
+++ b/src/ZF/Induct/Tree_Forest.thy Thu Dec 15 19:42:03 2005 +0100
@@ -204,7 +204,7 @@
\medskip Theorems about @{text list_of_TF} and @{text of_list}.
*}
-lemma forest_induct:
+lemma forest_induct [consumes 1, case_names Fnil Fcons]:
"[| f \<in> forest(A);
R(Fnil);
!!t f. [| t \<in> tree(A); f \<in> forest(A); R(f) |] ==> R(Fcons(t,f))
@@ -218,14 +218,10 @@
done
lemma forest_iso: "f \<in> forest(A) ==> of_list(list_of_TF(f)) = f"
- apply (erule forest_induct)
- apply simp_all
- done
+ by (induct rule: forest_induct) simp_all
lemma tree_list_iso: "ts: list(tree(A)) ==> list_of_TF(of_list(ts)) = ts"
- apply (erule list.induct)
- apply simp_all
- done
+ by (induct set: list) simp_all
text {*