removed obsolete induct/simp tactic;

--- a/src/FOL/IsaMakefile	Fri Apr 27 14:21:23 2007 +0200
+++ b/src/FOL/IsaMakefile	Fri Apr 27 16:31:20 2007 +0200
@@ -35,7 +35,7 @@
   $(SRC)/Provers/IsaPlanner/rw_tools.ML	\
   $(SRC)/Provers/IsaPlanner/rw_inst.ML \
   $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML			\
-  $(SRC)/Provers/ind.ML $(SRC)/Provers/induct_method.ML			\
+  $(SRC)/Provers/induct_method.ML			\
   $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML		\
   $(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML blastdata.ML cladata.ML 		\
   document/root.tex fologic.ML hypsubstdata.ML intprover.ML simpdata.ML
@@ -47,8 +47,8 @@
 FOL-ex: FOL $(LOG)/FOL-ex.gz
 
 $(LOG)/FOL-ex.gz: $(OUT)/FOL$(ML_SUFFIX) ex/First_Order_Logic.thy \
-  ex/If.thy ex/IffOracle.thy ex/List.ML ex/List.thy ex/LocaleTest.thy \
-  ex/Nat.thy ex/Nat2.ML ex/Nat2.thy ex/Natural_Numbers.thy ex/Miniscope.thy \
+  ex/If.thy ex/IffOracle.thy ex/LocaleTest.thy \
+  ex/Nat.thy ex/Natural_Numbers.thy ex/Miniscope.thy \
   ex/Prolog.thy ex/ROOT.ML ex/Classical.thy ex/document/root.tex \
   ex/Foundation.thy ex/Intuitionistic.thy ex/Intro.thy ex/prop.ML ex/quant.ML
 	@$(ISATOOL) usedir $(OUT)/FOL ex

--- a/src/FOL/ROOT.ML	Fri Apr 27 14:21:23 2007 +0200
+++ b/src/FOL/ROOT.ML	Fri Apr 27 16:31:20 2007 +0200
@@ -9,7 +9,6 @@
 writeln banner;
 
 use "~~/src/Provers/splitter.ML";
-use "~~/src/Provers/ind.ML";
 use "~~/src/Provers/hypsubst.ML";
 use "~~/src/Provers/IsaPlanner/zipper.ML";
 use "~~/src/Provers/IsaPlanner/isand.ML";

--- a/src/FOL/ex/List.ML	Fri Apr 27 14:21:23 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-(*  Title:      FOL/ex/list
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1991  University of Cambridge
-*)
-
-val prems = goal (the_context ()) "[| P([]);  !!x l. P(x . l) |] ==> All(P)";
-by (rtac list_ind 1);
-by (REPEAT (resolve_tac (prems@[allI,impI]) 1));
-qed "list_exh";
-
-Addsimps [list_distinct1, list_distinct2, app_nil, app_cons,
-	  hd_eq, tl_eq, forall_nil, forall_cons, list_free,
-	  len_nil, len_cons, at_0, at_succ];
-
-Goal "~l=[] --> hd(l).tl(l) = l";
-by (IND_TAC list_exh Simp_tac "l" 1);
-result();
-
-Goal "(l1++l2)++l3 = l1++(l2++l3)";
-by (IND_TAC list_ind Simp_tac "l1" 1);
-qed "append_assoc";
-
-Goal "l++[] = l";
-by (IND_TAC list_ind Simp_tac "l" 1);
-qed "app_nil_right";
-
-Goal "l1++l2=[] <-> l1=[] & l2=[]";
-by (IND_TAC list_exh Simp_tac "l1" 1);
-qed "app_eq_nil_iff";
-
-Goal "forall(l++l',P) <-> forall(l,P) & forall(l',P)";
-by (IND_TAC list_ind Simp_tac "l" 1);
-qed "forall_app";
-
-Goal "forall(l,%x. P(x)&Q(x)) <-> forall(l,P) & forall(l,Q)";
-by (IND_TAC list_ind Simp_tac "l" 1);
-by (Fast_tac 1);
-qed "forall_conj";
-
-Goal "~l=[] --> forall(l,P) <-> P(hd(l)) & forall(tl(l),P)";
-by (IND_TAC list_ind Simp_tac "l" 1);
-qed "forall_ne";
-
-(*** Lists with natural numbers ***)
-
-Goal "len(l1++l2) = len(l1)+len(l2)";
-by (IND_TAC list_ind Simp_tac "l1" 1);
-qed "len_app";
-
-Goal "i<len(l1) --> at(l1++l2,i) = at(l1,i)";
-by (IND_TAC list_ind Simp_tac "l1" 1);
-by (REPEAT (rtac allI 1));
-by (rtac impI 1);
-by (ALL_IND_TAC nat_exh Asm_simp_tac 1);
-qed "at_app1";
-
-Goal "at(l1++(x . l2), len(l1)) = x";
-by (IND_TAC list_ind Simp_tac "l1" 1);
-qed "at_app_hd2";

--- a/src/FOL/ex/List.thy	Fri Apr 27 14:21:23 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-(*  Title:      FOL/ex/list
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1991  University of Cambridge
-*)
-
-header {* Examples of simplification and induction on lists *}
-
-theory List
-imports Nat2
-begin
-
-typedecl 'a list
-arities list :: ("term") "term"
-
-consts
-   hd           :: "'a list => 'a"
-   tl           :: "'a list => 'a list"
-   forall       :: "['a list, 'a => o] => o"
-   len          :: "'a list => nat"
-   at           :: "['a list, nat] => 'a"
-   Nil          :: "'a list"                          ("[]")
-   Cons         :: "['a, 'a list] => 'a list"         (infixr "." 80)
-   app          :: "['a list, 'a list] => 'a list"    (infixr "++" 70)
-
-axioms
- list_ind: "[| P([]);  ALL x l. P(l)-->P(x . l) |] ==> All(P)"
-
- forall_cong:
-  "[| l = l';  !!x. P(x)<->P'(x) |] ==> forall(l,P) <-> forall(l',P')"
-
- list_distinct1: "~[] = x . l"
- list_distinct2: "~x . l = []"
-
- list_free:      "x . l = x' . l' <-> x=x' & l=l'"
-
- app_nil:        "[]++l = l"
- app_cons:       "(x . l)++l' = x .(l++l')"
- tl_eq:  "tl(m . q) = q"
- hd_eq:  "hd(m . q) = m"
-
- forall_nil: "forall([],P)"
- forall_cons: "forall(x . l,P) <-> P(x) & forall(l,P)"
-
- len_nil: "len([]) = 0"
- len_cons: "len(m . q) = succ(len(q))"
-
- at_0: "at(m . q,0) = m"
- at_succ: "at(m . q,succ(n)) = at(q,n)"
-
-ML {* use_legacy_bindings (the_context ()) *}
-
-end

--- a/src/FOL/ex/Nat2.ML	Fri Apr 27 14:21:23 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,159 +0,0 @@
-(*  Title:      FOL/ex/nat2.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1991  University of Cambridge
-*)
-
-Addsimps [pred_0, pred_succ, plus_0, plus_succ,
-          nat_distinct1, nat_distinct2, succ_inject,
-          leq_0, leq_succ_succ, leq_succ_0,
-          lt_0_succ, lt_succ_succ, lt_0];
-
-
-val prems = goal (the_context ())
-    "[| P(0);  !!x. P(succ(x)) |] ==> All(P)";
-by (rtac nat_ind 1);
-by (REPEAT (resolve_tac (prems@[allI,impI]) 1));
-qed "nat_exh";
-
-Goal "~ n=succ(n)";
-by (IND_TAC nat_ind Simp_tac "n" 1);
-result();
-
-Goal "~ succ(n)=n";
-by (IND_TAC nat_ind Simp_tac "n" 1);
-result();
-
-Goal "~ succ(succ(n))=n";
-by (IND_TAC nat_ind Simp_tac "n" 1);
-result();
-
-Goal "~ n=succ(succ(n))";
-by (IND_TAC nat_ind Simp_tac "n" 1);
-result();
-
-Goal "m+0 = m";
-by (IND_TAC nat_ind Simp_tac "m" 1);
-qed "plus_0_right";
-
-Goal "m+succ(n) = succ(m+n)";
-by (IND_TAC nat_ind Simp_tac "m" 1);
-qed "plus_succ_right";
-
-Addsimps [plus_0_right, plus_succ_right];
-
-Goal "~n=0 --> m+pred(n) = pred(m+n)";
-by (IND_TAC nat_ind Simp_tac "n" 1);
-result();
-
-Goal "~n=0 --> succ(pred(n))=n";
-by (IND_TAC nat_ind Simp_tac "n" 1);
-result();
-
-Goal "m+n=0 <-> m=0 & n=0";
-by (IND_TAC nat_ind Simp_tac "m" 1);
-result();
-
-Goal "m <= n --> m <= succ(n)";
-by (IND_TAC nat_ind Simp_tac "m" 1);
-by (rtac (impI RS allI) 1);
-by (ALL_IND_TAC nat_ind Simp_tac 1);
-by (Fast_tac 1);
-bind_thm("le_imp_le_succ", result() RS mp);
-
-Goal "n<succ(n)";
-by (IND_TAC nat_ind Simp_tac "n" 1);
-result();
-
-Goal "~ n<n";
-by (IND_TAC nat_ind Simp_tac "n" 1);
-result();
-
-Goal "m < n --> m < succ(n)";
-by (IND_TAC nat_ind Simp_tac "m" 1);
-by (rtac (impI RS allI) 1);
-by (ALL_IND_TAC nat_ind Simp_tac 1);
-by (Fast_tac 1);
-result();
-
-Goal "m <= n --> m <= n+k";
-by (IND_TAC nat_ind (simp_tac (simpset() addsimps [le_imp_le_succ]))
-     "k" 1);
-qed "le_plus";
-
-Goal "succ(m) <= n --> m <= n";
-by (res_inst_tac [("x","n")]spec 1);
-by (ALL_IND_TAC nat_exh (simp_tac (simpset() addsimps [le_imp_le_succ])) 1);
-qed "succ_le";
-
-Goal "~m<n <-> n<=m";
-by (IND_TAC nat_ind Simp_tac "n" 1);
-by (rtac (impI RS allI) 1);
-by (ALL_IND_TAC nat_ind Asm_simp_tac 1);
-qed "not_less";
-
-Goal "n<=m --> ~m<n";
-by (simp_tac (simpset() addsimps [not_less]) 1);
-qed "le_imp_not_less";
-
-Goal "m<n --> ~n<=m";
-by (cut_facts_tac [not_less] 1 THEN Fast_tac 1);
-qed "not_le";
-
-Goal "m+k<=n --> m<=n";
-by (IND_TAC nat_ind (K all_tac) "k" 1);
-by (Simp_tac 1);
-by (rtac (impI RS allI) 1);
-by (Simp_tac 1);
-by (REPEAT (resolve_tac [allI,impI] 1));
-by (cut_facts_tac [succ_le] 1);
-by (Fast_tac 1);
-qed "plus_le";
-
-val prems = goal (the_context ()) "[| ~m=0;  m <= n |] ==> ~n=0";
-by (cut_facts_tac prems 1);
-by (REPEAT (etac rev_mp 1));
-by (IND_TAC nat_exh Simp_tac "m" 1);
-by (ALL_IND_TAC nat_exh Simp_tac 1);
-qed "not0";
-
-Goal "a<=a' & b<=b' --> a+b<=a'+b'";
-by (IND_TAC nat_ind (simp_tac (simpset() addsimps [le_plus])) "b" 1);
-by (resolve_tac [impI RS allI] 1);
-by (resolve_tac [allI RS allI] 1);
-by (ALL_IND_TAC nat_exh Asm_simp_tac 1);
-qed "plus_le_plus";
-
-Goal "i<=j --> j<=k --> i<=k";
-by (IND_TAC nat_ind (K all_tac) "i" 1);
-by (Simp_tac 1);
-by (resolve_tac [impI RS allI] 1);
-by (ALL_IND_TAC nat_exh Simp_tac 1);
-by (rtac impI 1);
-by (ALL_IND_TAC nat_exh Simp_tac 1);
-by (Fast_tac 1);
-qed "le_trans";
-
-Goal "i < j --> j <=k --> i < k";
-by (IND_TAC nat_ind (K all_tac) "j" 1);
-by (Simp_tac 1);
-by (resolve_tac [impI RS allI] 1);
-by (ALL_IND_TAC nat_exh Simp_tac 1);
-by (ALL_IND_TAC nat_exh Simp_tac 1);
-by (ALL_IND_TAC nat_exh Simp_tac 1);
-by (Fast_tac 1);
-qed "less_le_trans";
-
-Goal "succ(i) <= j <-> i < j";
-by (IND_TAC nat_ind Simp_tac "j" 1);
-by (resolve_tac [impI RS allI] 1);
-by (ALL_IND_TAC nat_exh Asm_simp_tac 1);
-qed "succ_le2";
-
-Goal "i<succ(j) <-> i=j | i<j";
-by (IND_TAC nat_ind Simp_tac "j" 1);
-by (ALL_IND_TAC nat_exh Simp_tac 1);
-by (resolve_tac [impI RS allI] 1);
-by (ALL_IND_TAC nat_exh Simp_tac 1);
-by (Asm_simp_tac 1);
-qed "less_succ";

--- a/src/FOL/ex/Nat2.thy	Fri Apr 27 14:21:23 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-(*  Title:      FOL/ex/nat2.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1994  University of Cambridge
-*)
-
-header {* Theory for examples of simplification and induction on the natural numbers *}
-
-theory Nat2
-imports FOL
-begin
-
-typedecl nat
-arities nat :: "term"
-
-consts
-  succ :: "nat => nat"
-  pred :: "nat => nat"
-  0 :: nat    ("0")
-  add :: "[nat,nat] => nat"    (infixr "+" 90)
-  lt :: "[nat,nat] => o"    (infixr "<" 70)
-  leq :: "[nat,nat] => o"    (infixr "<=" 70)
-
-axioms
- pred_0:         "pred(0) = 0"
- pred_succ:      "pred(succ(m)) = m"
-
- plus_0:         "0+n = n"
- plus_succ:      "succ(m)+n = succ(m+n)"
-
- nat_distinct1:  "~ 0=succ(n)"
- nat_distinct2:  "~ succ(m)=0"
- succ_inject:    "succ(m)=succ(n) <-> m=n"
-
- leq_0:          "0 <= n"
- leq_succ_succ:  "succ(m)<=succ(n) <-> m<=n"
- leq_succ_0:     "~ succ(m) <= 0"
-
- lt_0_succ:      "0 < succ(n)"
- lt_succ_succ:   "succ(m)<succ(n) <-> m<n"
- lt_0:           "~ m < 0"
-
- nat_ind:        "[| P(0); ALL n. P(n)-->P(succ(n)) |] ==> All(P)"
-
-ML {* use_legacy_bindings (the_context ()) *}
-
-end

--- a/src/FOL/ex/ROOT.ML	Fri Apr 27 14:21:23 2007 +0200
+++ b/src/FOL/ex/ROOT.ML	Fri Apr 27 16:31:20 2007 +0200
@@ -30,10 +30,6 @@
 
 time_use_thy "NatClass";
 
-writeln"\n** Simplification examples **\n";
-time_use_thy "Nat2";
-time_use_thy "List";
-
 time_use_thy "IffOracle";
 
 (*regression test for locales -- sets several global flags!*)

--- a/src/FOL/simpdata.ML	Fri Apr 27 14:21:23 2007 +0200
+++ b/src/FOL/simpdata.ML	Fri Apr 27 16:31:20 2007 +0200
@@ -275,11 +275,6 @@
 
 (*** Standard simpsets ***)
 
-structure Induction = InductionFun(struct val spec = spec end);
-
-open Induction;
-
-
 bind_thms ("meta_simps",
  [triv_forall_equality,   (* prunes params *)
   thm "True_implies_equals"]);  (* prune asms `True' *)

--- a/src/Provers/ind.ML	Fri Apr 27 14:21:23 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,64 +0,0 @@
-(*  Title: 	Provers/ind
-    ID:         $Id$
-    Author: 	Tobias Nipkow
-    Copyright   1991  University of Cambridge
-
-Generic induction package -- for use with simplifier
-*)
-
-signature IND_DATA =
-  sig
-  val spec: thm (* All(?P) ==> ?P(?a) *)
-  end;
-
-
-signature IND =
-  sig
-  val all_frees_tac: string -> int -> tactic
-  val ALL_IND_TAC: thm -> (int -> tactic) -> (int -> tactic)
-  val IND_TAC: thm -> (int -> tactic) -> string -> (int -> tactic)
-  end;
-
-
-functor InductionFun(Ind_Data: IND_DATA):IND =
-struct
-local open Ind_Data in
-
-val _$(_$Var(a_ixname,aT)) = concl_of spec;
-
-fun add_term_frees thy =
-let fun add(tm, vars) = case tm of
-	Free(v,T) => if Sign.typ_instance thy (T,aT) then insert (op =) v vars
-		     else vars
-      | Abs (_,_,body) => add(body,vars)
-      | rator$rand => add(rator, add(rand, vars))
-      | _ => vars
-in add end;
-
-
-fun qnt_tac i = fn (tac,var) => tac THEN Tactic.res_inst_tac' [(a_ixname,var)] spec i;
-
-(*Generalizes over all free variables, with the named var outermost.*)
-fun all_frees_tac (var:string) i thm = 
-    let val frees = add_term_frees (Thm.theory_of_thm thm) (List.nth(prems_of thm,i-1),[var]);
-        val frees' = sort (rev_order o string_ord) (remove (op =) var frees) @ [var]
-    in Library.foldl (qnt_tac i) (all_tac,frees') thm end;
-
-fun REPEAT_SIMP_TAC simp_tac n i =
-let fun repeat thm = 
-        (COND (has_fewer_prems n) all_tac
-	 let val k = nprems_of thm
-	 in simp_tac i THEN COND (has_fewer_prems k) repeat all_tac end)
-	thm
-in repeat end;
-
-fun ALL_IND_TAC sch simp_tac i thm = 
-	(resolve_tac [sch] i THEN
-	 REPEAT_SIMP_TAC simp_tac (nprems_of thm) i) thm;
-
-fun IND_TAC sch simp_tac var =
-	all_frees_tac var THEN' ALL_IND_TAC sch simp_tac;
-
-
-end
-end;