# HG changeset patch
# User wenzelm
# Date 1134672123 -3600
# Node ID eb68dc98bda2232037d9cda7b2b56d2a49009cda
# Parent  560f89584ada3ae835a7aabcde265ab9c4b77f33
improved proofs;

diff -r 560f89584ada -r eb68dc98bda2 src/ZF/Induct/Binary_Trees.thy
--- 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
diff -r 560f89584ada -r eb68dc98bda2 src/ZF/Induct/Comb.thy
--- 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)
diff -r 560f89584ada -r eb68dc98bda2 src/ZF/Induct/ListN.thy
--- 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)
diff -r 560f89584ada -r eb68dc98bda2 src/ZF/Induct/Multiset.thy
--- 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)|] 
diff -r 560f89584ada -r eb68dc98bda2 src/ZF/Induct/Mutil.thy
--- 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
diff -r 560f89584ada -r eb68dc98bda2 src/ZF/Induct/Primrec.thy
--- 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
 
diff -r 560f89584ada -r eb68dc98bda2 src/ZF/Induct/PropLog.thy
--- 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)
diff -r 560f89584ada -r eb68dc98bda2 src/ZF/Induct/Term.thy
--- 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
diff -r 560f89584ada -r eb68dc98bda2 src/ZF/Induct/Tree_Forest.thy
--- 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 {*