# HG changeset patch # User wenzelm # Date 1177684280 -7200 # Node ID c1a6a2159e69123e520c26dc093c9683c2b3dc53 # Parent 15b2e7ec1f3b48d65ec47726abc511e5d07c83e5 removed obsolete induct/simp tactic; diff -r 15b2e7ec1f3b -r c1a6a2159e69 src/FOL/IsaMakefile --- 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 diff -r 15b2e7ec1f3b -r c1a6a2159e69 src/FOL/ROOT.ML --- 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"; diff -r 15b2e7ec1f3b -r c1a6a2159e69 src/FOL/ex/List.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 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"; diff -r 15b2e7ec1f3b -r c1a6a2159e69 src/FOL/ex/List.thy --- 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 diff -r 15b2e7ec1f3b -r c1a6a2159e69 src/FOL/ex/Nat2.ML --- 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 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<=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<=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 i=j | i 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) mP(succ(n)) |] ==> All(P)" - -ML {* use_legacy_bindings (the_context ()) *} - -end diff -r 15b2e7ec1f3b -r c1a6a2159e69 src/FOL/ex/ROOT.ML --- 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!*) diff -r 15b2e7ec1f3b -r c1a6a2159e69 src/FOL/simpdata.ML --- 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' *) diff -r 15b2e7ec1f3b -r c1a6a2159e69 src/Provers/ind.ML --- 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;