# HG changeset patch # User nipkow # Date 861898006 -7200 # Node ID 7d48671753da641613d73ea7ba39a7eaf65e980e # Parent bbf4e3738ef04b1e60d9166b2c9746318603ef39 Introduced a generic "induct_tac" which picks up the right induction scheme automatically. Also changed nat_ind_tac, which does no longer append a "1" to the name of the induction variable. This caused some changes... diff -r bbf4e3738ef0 -r 7d48671753da src/HOL/Hoare/Arith2.ML --- a/src/HOL/Hoare/Arith2.ML Thu Apr 24 18:03:23 1997 +0200 +++ b/src/HOL/Hoare/Arith2.ML Thu Apr 24 18:06:46 1997 +0200 @@ -189,7 +189,7 @@ by (nat_ind_tac "m" 1); by (Simp_tac 1); by (etac mod_less 1); -by (dres_inst_tac [("n","n"),("m","m1*n")] mod_eq_add 1); +by (dres_inst_tac [("m","m*n")] mod_eq_add 1); by (asm_full_simp_tac ((simpset_of "Arith") addsimps [add_commute]) 1); qed "mod_prod_nn_is_0"; diff -r bbf4e3738ef0 -r 7d48671753da src/HOL/IOA/meta_theory/IOA.ML --- a/src/HOL/IOA/meta_theory/IOA.ML Thu Apr 24 18:03:23 1997 +0200 +++ b/src/HOL/IOA/meta_theory/IOA.ML Thu Apr 24 18:06:46 1997 +0200 @@ -81,8 +81,8 @@ by (res_inst_tac [("Q","reachable A (snd ex n)")] conjunct1 1); by (nat_ind_tac "n" 1); by (fast_tac (!claset addIs [p1,reachable_0]) 1); - by (eres_inst_tac[("x","n1")]allE 1); - by (eres_inst_tac[("P","%x.!a.?Q x a"), ("opt","fst ex n1")] optionE 1); + by (eres_inst_tac[("x","n")]allE 1); + by (eres_inst_tac[("P","%x.!a.?Q x a"), ("opt","fst ex n")] optionE 1); by (Asm_simp_tac 1); by (safe_tac (!claset)); by (etac (p2 RS mp) 1); diff -r bbf4e3738ef0 -r 7d48671753da src/HOL/List.ML --- a/src/HOL/List.ML Thu Apr 24 18:03:23 1997 +0200 +++ b/src/HOL/List.ML Thu Apr 24 18:06:46 1997 +0200 @@ -7,13 +7,13 @@ *) goal thy "!x. xs ~= x#xs"; -by (list.induct_tac "xs" 1); +by (induct_tac "xs" 1); by (ALLGOALS Asm_simp_tac); qed_spec_mp "not_Cons_self"; Addsimps [not_Cons_self]; goal thy "(xs ~= []) = (? y ys. xs = y#ys)"; -by (list.induct_tac "xs" 1); +by (induct_tac "xs" 1); by (Simp_tac 1); by (Asm_simp_tac 1); qed "neq_Nil_conv"; @@ -24,18 +24,18 @@ goal thy "P(list_case a f xs) = ((xs=[] --> P(a)) & \ \ (!y ys. xs=y#ys --> P(f y ys)))"; -by (list.induct_tac "xs" 1); +by (induct_tac "xs" 1); by (ALLGOALS Asm_simp_tac); by (Blast_tac 1); qed "expand_list_case"; val prems = goal thy "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)"; -by(list.induct_tac "xs" 1); +by(induct_tac "xs" 1); by(REPEAT(resolve_tac prems 1)); qed "list_cases"; goal thy "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)"; -by (list.induct_tac "xs" 1); +by (induct_tac "xs" 1); by (Blast_tac 1); by (Blast_tac 1); bind_thm("list_eq_cases", @@ -45,55 +45,55 @@ (** @ - append **) goal thy "(xs@ys)@zs = xs@(ys@zs)"; -by (list.induct_tac "xs" 1); +by (induct_tac "xs" 1); by (ALLGOALS Asm_simp_tac); qed "append_assoc"; Addsimps [append_assoc]; goal thy "xs @ [] = xs"; -by (list.induct_tac "xs" 1); +by (induct_tac "xs" 1); by (ALLGOALS Asm_simp_tac); qed "append_Nil2"; Addsimps [append_Nil2]; goal thy "(xs@ys = []) = (xs=[] & ys=[])"; -by (list.induct_tac "xs" 1); +by (induct_tac "xs" 1); by (ALLGOALS Asm_simp_tac); qed "append_is_Nil_conv"; AddIffs [append_is_Nil_conv]; goal thy "([] = xs@ys) = (xs=[] & ys=[])"; -by (list.induct_tac "xs" 1); +by (induct_tac "xs" 1); by (ALLGOALS Asm_simp_tac); by(Blast_tac 1); qed "Nil_is_append_conv"; AddIffs [Nil_is_append_conv]; goal thy "(xs @ ys = xs @ zs) = (ys=zs)"; -by (list.induct_tac "xs" 1); +by (induct_tac "xs" 1); by (ALLGOALS Asm_simp_tac); qed "same_append_eq"; AddIffs [same_append_eq]; goal thy "!ys. (xs @ [x] = ys @ [y]) = (xs = ys & x = y)"; -by(list.induct_tac "xs" 1); +by(induct_tac "xs" 1); br allI 1; - by(list.induct_tac "ys" 1); + by(induct_tac "ys" 1); by(ALLGOALS Asm_simp_tac); br allI 1; -by(list.induct_tac "ys" 1); +by(induct_tac "ys" 1); by(ALLGOALS Asm_simp_tac); qed_spec_mp "append1_eq_conv"; AddIffs [append1_eq_conv]; goal thy "xs ~= [] --> hd xs # tl xs = xs"; -by(list.induct_tac "xs" 1); +by(induct_tac "xs" 1); by(ALLGOALS Asm_simp_tac); qed_spec_mp "hd_Cons_tl"; Addsimps [hd_Cons_tl]; goal thy "hd(xs@ys) = (if xs=[] then hd ys else hd xs)"; -by (list.induct_tac "xs" 1); +by (induct_tac "xs" 1); by (ALLGOALS Asm_simp_tac); qed "hd_append"; @@ -105,44 +105,44 @@ goal thy "(!x. x : set_of_list xs --> f x = g x) --> map f xs = map g xs"; -by(list.induct_tac "xs" 1); +by(induct_tac "xs" 1); by(ALLGOALS Asm_simp_tac); bind_thm("map_ext", impI RS (allI RS (result() RS mp))); goal thy "map (%x.x) = (%xs.xs)"; by (rtac ext 1); -by (list.induct_tac "xs" 1); +by (induct_tac "xs" 1); by (ALLGOALS Asm_simp_tac); qed "map_ident"; Addsimps[map_ident]; goal thy "map f (xs@ys) = map f xs @ map f ys"; -by (list.induct_tac "xs" 1); +by (induct_tac "xs" 1); by (ALLGOALS Asm_simp_tac); qed "map_append"; Addsimps[map_append]; goalw thy [o_def] "map (f o g) xs = map f (map g xs)"; -by (list.induct_tac "xs" 1); +by (induct_tac "xs" 1); by (ALLGOALS Asm_simp_tac); qed "map_compose"; Addsimps[map_compose]; goal thy "rev(map f xs) = map f (rev xs)"; -by (list.induct_tac "xs" 1); +by (induct_tac "xs" 1); by (ALLGOALS Asm_simp_tac); qed "rev_map"; (** rev **) goal thy "rev(xs@ys) = rev(ys) @ rev(xs)"; -by (list.induct_tac "xs" 1); +by (induct_tac "xs" 1); by (ALLGOALS Asm_simp_tac); qed "rev_append"; Addsimps[rev_append]; goal thy "rev(rev l) = l"; -by (list.induct_tac "l" 1); +by (induct_tac "l" 1); by (ALLGOALS Asm_simp_tac); qed "rev_rev_ident"; Addsimps[rev_rev_ident]; @@ -151,13 +151,13 @@ (** mem **) goal thy "x mem (xs@ys) = (x mem xs | x mem ys)"; -by (list.induct_tac "xs" 1); +by (induct_tac "xs" 1); by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if])))); qed "mem_append"; Addsimps[mem_append]; goal thy "x mem [x:xs.P(x)] = (x mem xs & P(x))"; -by (list.induct_tac "xs" 1); +by (induct_tac "xs" 1); by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if])))); qed "mem_filter"; Addsimps[mem_filter]; @@ -165,14 +165,14 @@ (** set_of_list **) goal thy "set_of_list (xs@ys) = (set_of_list xs Un set_of_list ys)"; -by (list.induct_tac "xs" 1); +by (induct_tac "xs" 1); by (ALLGOALS Asm_simp_tac); by (Blast_tac 1); qed "set_of_list_append"; Addsimps[set_of_list_append]; goal thy "(x mem xs) = (x: set_of_list xs)"; -by (list.induct_tac "xs" 1); +by (induct_tac "xs" 1); by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if])))); by (Blast_tac 1); qed "set_of_list_mem_eq"; @@ -183,20 +183,20 @@ qed "set_of_list_subset_Cons"; goal thy "(set_of_list xs = {}) = (xs = [])"; -by(list.induct_tac "xs" 1); +by(induct_tac "xs" 1); by(ALLGOALS Asm_simp_tac); qed "set_of_list_empty"; Addsimps [set_of_list_empty]; goal thy "set_of_list(rev xs) = set_of_list(xs)"; -by(list.induct_tac "xs" 1); +by(induct_tac "xs" 1); by(ALLGOALS Asm_simp_tac); by(Blast_tac 1); qed "set_of_list_rev"; Addsimps [set_of_list_rev]; goal thy "set_of_list(map f xs) = f``(set_of_list xs)"; -by(list.induct_tac "xs" 1); +by(induct_tac "xs" 1); by(ALLGOALS Asm_simp_tac); qed "set_of_list_map"; Addsimps [set_of_list_map]; @@ -205,19 +205,19 @@ (** list_all **) goal thy "list_all (%x.True) xs = True"; -by (list.induct_tac "xs" 1); +by (induct_tac "xs" 1); by (ALLGOALS Asm_simp_tac); qed "list_all_True"; Addsimps [list_all_True]; goal thy "list_all p (xs@ys) = (list_all p xs & list_all p ys)"; -by (list.induct_tac "xs" 1); +by (induct_tac "xs" 1); by (ALLGOALS Asm_simp_tac); qed "list_all_append"; Addsimps [list_all_append]; goal thy "list_all P xs = (!x. x mem xs --> P(x))"; -by (list.induct_tac "xs" 1); +by (induct_tac "xs" 1); by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if])))); by (Blast_tac 1); qed "list_all_mem_conv"; @@ -226,7 +226,7 @@ (** filter **) goal thy "[x:xs@ys . P] = [x:xs . P] @ [y:ys . P]"; -by(list.induct_tac "xs" 1); +by(induct_tac "xs" 1); by(ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if])))); qed "filter_append"; Addsimps [filter_append]; @@ -235,44 +235,44 @@ (** concat **) goal thy "concat(xs@ys) = concat(xs)@concat(ys)"; -by (list.induct_tac "xs" 1); +by (induct_tac "xs" 1); by (ALLGOALS Asm_simp_tac); qed"concat_append"; Addsimps [concat_append]; goal thy "rev(concat ls) = concat (map rev (rev ls))"; -by (list.induct_tac "ls" 1); +by (induct_tac "ls" 1); by (ALLGOALS Asm_simp_tac); qed "rev_concat"; (** length **) goal thy "length(xs@ys) = length(xs)+length(ys)"; -by (list.induct_tac "xs" 1); +by (induct_tac "xs" 1); by (ALLGOALS Asm_simp_tac); qed"length_append"; Addsimps [length_append]; goal thy "length (map f l) = length l"; -by (list.induct_tac "l" 1); +by (induct_tac "l" 1); by (ALLGOALS Simp_tac); qed "length_map"; Addsimps [length_map]; goal thy "length(rev xs) = length(xs)"; -by (list.induct_tac "xs" 1); +by (induct_tac "xs" 1); by (ALLGOALS Asm_simp_tac); qed "length_rev"; Addsimps [length_rev]; goal thy "(length xs = 0) = (xs = [])"; -by(list.induct_tac "xs" 1); +by(induct_tac "xs" 1); by(ALLGOALS Asm_simp_tac); qed "length_0_conv"; AddIffs [length_0_conv]; goal thy "(0 < length xs) = (xs ~= [])"; -by(list.induct_tac "xs" 1); +by(induct_tac "xs" 1); by(ALLGOALS Asm_simp_tac); qed "length_greater_0_conv"; AddIffs [length_greater_0_conv]; @@ -294,7 +294,7 @@ qed_spec_mp "nth_append"; goal thy "!n. n < length xs --> nth n (map f xs) = f (nth n xs)"; -by (list.induct_tac "xs" 1); +by (induct_tac "xs" 1); (* case [] *) by (Asm_full_simp_tac 1); (* case x#xl *) @@ -305,7 +305,7 @@ Addsimps [nth_map]; goal thy "!n. n < length xs --> list_all P xs --> P(nth n xs)"; -by (list.induct_tac "xs" 1); +by (induct_tac "xs" 1); (* case [] *) by (Simp_tac 1); (* case x#xl *) @@ -315,7 +315,7 @@ qed_spec_mp "list_all_nth"; goal thy "!n. n < length xs --> (nth n xs) mem xs"; -by (list.induct_tac "xs" 1); +by (induct_tac "xs" 1); (* case [] *) by (Simp_tac 1); (* case x#xl *) @@ -333,12 +333,12 @@ section "take & drop"; goal thy "take 0 xs = []"; -by (list.induct_tac "xs" 1); +by (induct_tac "xs" 1); by (ALLGOALS Asm_simp_tac); qed "take_0"; goal thy "drop 0 xs = xs"; -by (list.induct_tac "xs" 1); +by (induct_tac "xs" 1); by (ALLGOALS Asm_simp_tac); qed "drop_0"; @@ -451,7 +451,7 @@ goal thy "!n i. i < n --> nth i (take n xs) = nth i xs"; -by(list.induct_tac "xs" 1); +by(induct_tac "xs" 1); by(ALLGOALS Asm_simp_tac); by(strip_tac 1); by(res_inst_tac [("n","n")] natE 1); @@ -475,7 +475,7 @@ goal thy "x:set_of_list xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs"; -by(list.induct_tac "xs" 1); +by(induct_tac "xs" 1); by(Simp_tac 1); by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1); by(Blast_tac 1); @@ -484,7 +484,7 @@ goal thy "(!x:set_of_list xs.P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys"; -by(list.induct_tac "xs" 1); +by(induct_tac "xs" 1); by(Simp_tac 1); by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1); bind_thm("takeWhile_append2", ballI RS (result() RS mp)); @@ -492,7 +492,7 @@ goal thy "x:set_of_list xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys"; -by(list.induct_tac "xs" 1); +by(induct_tac "xs" 1); by(Simp_tac 1); by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1); by(Blast_tac 1); @@ -501,14 +501,14 @@ goal thy "(!x:set_of_list xs.P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys"; -by(list.induct_tac "xs" 1); +by(induct_tac "xs" 1); by(Simp_tac 1); by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1); bind_thm("dropWhile_append2", ballI RS (result() RS mp)); Addsimps [dropWhile_append2]; goal thy "x:set_of_list(takeWhile P xs) --> x:set_of_list xs & P x"; -by(list.induct_tac "xs" 1); +by(induct_tac "xs" 1); by(Simp_tac 1); by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1); qed_spec_mp"set_of_list_take_whileD"; diff -r bbf4e3738ef0 -r 7d48671753da src/HOL/NatDef.ML --- a/src/HOL/NatDef.ML Thu Apr 24 18:03:23 1997 +0200 +++ b/src/HOL/NatDef.ML Thu Apr 24 18:06:46 1997 +0200 @@ -33,7 +33,7 @@ val prems = goalw thy [Zero_def,Suc_def] "[| P(0); \ -\ !!k. P(k) ==> P(Suc(k)) |] ==> P(n)"; +\ !!n. P(n) ==> P(Suc(n)) |] ==> P(n)"; by (rtac (Rep_Nat_inverse RS subst) 1); (*types force good instantiation*) by (rtac (Rep_Nat RS Nat_induct) 1); by (REPEAT (ares_tac prems 1 @@ -42,8 +42,16 @@ (*Perform induction on n. *) fun nat_ind_tac a i = - EVERY [res_inst_tac [("n",a)] nat_induct i, - rename_last_tac a ["1"] (i+1)]; + EVERY[res_inst_tac [("n",a)] nat_induct i, + COND (Datatype.occs_in_prems a (i+1)) all_tac + (rename_last_tac a [""] (i+1))]; + +(*Install 'automatic' induction tactic, pretending nat is a datatype *) +(*except for induct_tac, everything is dummy*) +datatypes := [("nat",{case_const = Bound 0, case_rewrites = [], + constructors = [], induct_tac = nat_ind_tac, + nchotomy = flexpair_def, case_cong = flexpair_def})]; + (*A special form of induction for reasoning about m add_trrules xrules |> add_axioms rules, add_primrec) end -end -end + +(*Check if the (induction) variable occurs among the premises, which + usually signals a mistake *) +fun occs_in_prems a i state = + let val (_, _, Bi, _) = dest_state(state,i) + val prems = Logic.strip_assums_hyp Bi + in a mem map (#1 o dest_Free) (foldr add_term_frees (prems,[])) end; + +end; + +end; (* Informal description of functions used in datatype.ML for the Isabelle/HOL @@ -492,8 +501,7 @@ (* The following has been written by Konrad Slind. *) -type dtype_info = {case_const:term, case_rewrites:thm list, - constructors:term list, nchotomy:thm, case_cong:thm}; +(* type dtype_info is defined in simpdata.ML *) signature Dtype_sig = sig @@ -832,10 +840,15 @@ fun const s = Const(s, the(Sign.const_type sign s)) val case_rewrites = map (fn c => get_fact thy (ty^"_case_"^c)) cl val {nchotomy,case_cong} = case_thms sign case_rewrites itac + fun induct_tac a i = itac a i THEN + COND (Datatype.occs_in_prems a i) + (warning "Induction variable occurs also among premises!"; + all_tac) all_tac in (ty, {constructors = map(fn s => const s handle _ => const("op "^s)) cl, case_const = const (ty^"_case"), case_rewrites = map mk_rw case_rewrites, + induct_tac = induct_tac, nchotomy = nchotomy, case_cong = case_cong}) end diff -r bbf4e3738ef0 -r 7d48671753da src/HOL/ex/Mutil.ML --- a/src/HOL/ex/Mutil.ML Thu Apr 24 18:03:23 1997 +0200 +++ b/src/HOL/ex/Mutil.ML Thu Apr 24 18:06:46 1997 +0200 @@ -53,8 +53,8 @@ by (resolve_tac tiling.intrs 1); by (assume_tac 2); by (subgoal_tac (*seems the easiest way of turning one to the other*) - "({i} Times {Suc(n1+n1)}) Un ({i} Times {n1+n1}) = \ -\ {(i, n1+n1), (i, Suc(n1+n1))}" 1); + "({i} Times {Suc(n+n)}) Un ({i} Times {n+n}) = \ +\ {(i, n+n), (i, Suc(n+n))}" 1); by (Blast_tac 2); by (asm_simp_tac (!simpset addsimps [domino.horiz]) 1); by (blast_tac (!claset addEs [less_irrefl, less_asym] diff -r bbf4e3738ef0 -r 7d48671753da src/HOL/simpdata.ML --- a/src/HOL/simpdata.ML Thu Apr 24 18:03:23 1997 +0200 +++ b/src/HOL/simpdata.ML Thu Apr 24 18:06:46 1997 +0200 @@ -347,8 +347,12 @@ ("simpset", ThyMethods {merge = merge, put = put, get = get}) end; -type dtype_info = {case_const:term, case_rewrites:thm list, - constructors:term list, nchotomy:thm, case_cong:thm}; +type dtype_info = {case_const:term, + case_rewrites:thm list, + constructors:term list, + induct_tac: string -> int -> tactic, + nchotomy:thm, + case_cong:thm}; exception DT_DATA of (string * dtype_info) list; val datatypes = ref [] : (string * dtype_info) list ref; diff -r bbf4e3738ef0 -r 7d48671753da src/HOL/thy_data.ML --- a/src/HOL/thy_data.ML Thu Apr 24 18:03:23 1997 +0200 +++ b/src/HOL/thy_data.ML Thu Apr 24 18:06:46 1997 +0200 @@ -49,6 +49,27 @@ in (map #case_cong info, flat (map #case_rewrites info)) end; in {case_congs = congs, case_rewrites = rewrites} end; +(* generic induction tactic for datatypes *) +fun induct_tac var i = + let fun find_tname Bi = + let val frees = map (fn Free x => x) (term_frees Bi) + val params = Logic.strip_params Bi; + in case assoc (frees@params, var) of + None => error("No such variable in subgoal: " ^ quote var) + | Some(Type(tn,_)) => tn + | _ => error("Cannot induct on type of " ^ quote var) + end; + fun get_ind_tac sign tn = + (case get_thydata (thyname_of_sign sign) "datatypes" of + None => error ("No such datatype: " ^ quote tn) + | Some (DT_DATA ds) => + (case assoc (ds, tn) of + Some {induct_tac, ...} => induct_tac + | None => error ("Not a datatype: " ^ quote tn))); + fun induct state = + let val (_, _, Bi, _) = dest_state (state, i) + in get_ind_tac (#sign(rep_thm state)) (find_tname Bi) var i end + in STATE induct end; (*Must be redefined in order to refer to the new instance of bind_thm created by init_thy_reader.*) @@ -62,4 +83,3 @@ fun qed_goalw_spec_mp name thy defs s p = bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p)); -