38 |
38 |
39 |
39 |
40 fun qnt_tac i = fn (tac,var) => tac THEN res_inst_tac [(a_name,var)] spec i; |
40 fun qnt_tac i = fn (tac,var) => tac THEN res_inst_tac [(a_name,var)] spec i; |
41 |
41 |
42 (*Generalizes over all free variables, with the named var outermost.*) |
42 (*Generalizes over all free variables, with the named var outermost.*) |
43 fun all_frees_tac (var:string) i = Tactic(fn thm => |
43 fun all_frees_tac (var:string) i thm = |
44 let val tsig = #tsig(Sign.rep_sg(#sign(rep_thm thm))); |
44 let val tsig = #tsig(Sign.rep_sg(#sign(rep_thm thm))); |
45 val frees = add_term_frees tsig (nth_elem(i-1,prems_of thm),[var]); |
45 val frees = add_term_frees tsig (nth_elem(i-1,prems_of thm),[var]); |
46 val frees' = sort(op>)(frees \ var) @ [var] |
46 val frees' = sort(op>)(frees \ var) @ [var] |
47 in tapply(foldl (qnt_tac i) (all_tac,frees'), thm) end); |
47 in foldl (qnt_tac i) (all_tac,frees') thm end; |
48 |
48 |
49 fun REPEAT_SIMP_TAC simp_tac n i = |
49 fun REPEAT_SIMP_TAC simp_tac n i = |
50 let fun repeat thm = tapply(COND (has_fewer_prems n) all_tac |
50 let fun repeat thm = |
51 let val k = length(prems_of thm) |
51 (COND (has_fewer_prems n) all_tac |
52 in simp_tac i THEN COND (has_fewer_prems k) (Tactic repeat) all_tac |
52 let val k = nprems_of thm |
53 end, thm) |
53 in simp_tac i THEN COND (has_fewer_prems k) repeat all_tac end) |
54 in Tactic repeat end; |
54 thm |
|
55 in repeat end; |
55 |
56 |
56 fun ALL_IND_TAC sch simp_tac i = Tactic(fn thm => tapply( |
57 fun ALL_IND_TAC sch simp_tac i thm = |
57 resolve_tac [sch] i THEN |
58 (resolve_tac [sch] i THEN |
58 REPEAT_SIMP_TAC simp_tac (length(prems_of thm)) i, thm)); |
59 REPEAT_SIMP_TAC simp_tac (nprems_of thm) i) thm; |
59 |
60 |
60 fun IND_TAC sch simp_tac var = |
61 fun IND_TAC sch simp_tac var = |
61 all_frees_tac var THEN' ALL_IND_TAC sch simp_tac; |
62 all_frees_tac var THEN' ALL_IND_TAC sch simp_tac; |
62 |
63 |
63 |
64 |