author  haftmann 
Mon, 22 Sep 2008 08:00:24 +0200  
changeset 28308  d4396a28fb29 
parent 27882  eaa9fef9f4c1 
child 30161  c26e515f1c29 
permissions  rwrr 
28308  1 
(* Title: Tools/induct_tacs.ML 
27326
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

3 
Author: Makarius 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

4 

d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

5 
Unstructured induction and cases analysis. 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

6 
*) 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

7 

d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

8 
signature INDUCT_TACS = 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

9 
sig 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

10 
val case_tac: Proof.context > string > int > tactic 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

11 
val case_rule_tac: Proof.context > string > thm > int > tactic 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

12 
val induct_tac: Proof.context > string option list list > int > tactic 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

13 
val induct_rules_tac: Proof.context > string option list list > thm list > int > tactic 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

14 
val setup: theory > theory 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

15 
end 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

16 

d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

17 
structure InductTacs: INDUCT_TACS = 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

18 
struct 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

19 

d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

20 
(* case analysis *) 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

21 

d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

22 
fun check_type ctxt t = 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

23 
let 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

24 
val u = singleton (Variable.polymorphic ctxt) t; 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

25 
val U = Term.fastype_of u; 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

26 
val _ = Term.is_TVar U andalso 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

27 
error ("Cannot determine type of " ^ Syntax.string_of_term ctxt u); 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

28 
in (u, U) end; 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

29 

d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

30 
fun gen_case_tac ctxt0 (s, opt_rule) i st = 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

31 
let 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

32 
val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0; 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

33 
val rule = 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

34 
(case opt_rule of 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

35 
SOME rule => rule 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

36 
 NONE => 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

37 
(case Induct.find_casesT ctxt 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

38 
(#2 (check_type ctxt (ProofContext.read_term_schematic ctxt s))) of 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

39 
rule :: _ => rule 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

40 
 [] => @{thm case_split})); 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

41 
val _ = Method.trace ctxt [rule]; 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

42 

d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

43 
val xi = 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

44 
(case Induct.vars_of (Thm.term_of (Thm.cprem_of rule 1)) of 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

45 
Var (xi, _) :: _ => xi 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

46 
 _ => raise THM ("Malformed cases rule", 0, [rule])); 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

47 
in res_inst_tac ctxt [(xi, s)] rule i st end 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

48 
handle THM _ => Seq.empty; 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

49 

d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

50 
fun case_tac ctxt s = gen_case_tac ctxt (s, NONE); 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

51 
fun case_rule_tac ctxt s rule = gen_case_tac ctxt (s, SOME rule); 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

52 

d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

53 

d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

54 
(* induction *) 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

55 

d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

56 
local 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

57 

d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

58 
fun prep_var (Var (ixn, _), SOME x) = SOME (ixn, x) 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

59 
 prep_var _ = NONE; 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

60 

d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

61 
fun prep_inst (concl, xs) = 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

62 
let val vs = Induct.vars_of concl 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

63 
in map_filter prep_var (Library.drop (length vs  length xs, vs) ~~ xs) end; 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

64 

d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

65 
in 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

66 

d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

67 
fun gen_induct_tac ctxt0 (varss, opt_rules) i st = 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

68 
let 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

69 
val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0; 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

70 
val (prems, concl) = Logic.strip_horn (Thm.term_of goal); 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

71 

d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

72 
fun induct_var name = 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

73 
let 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

74 
val t = Syntax.read_term ctxt name; 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

75 
val (x, _) = Term.dest_Free t handle TERM _ => 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

76 
error ("Induction argument not a variable: " ^ Syntax.string_of_term ctxt t); 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

77 
val eq_x = fn Free (y, _) => x = y  _ => false; 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

78 
val _ = 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

79 
if Term.exists_subterm eq_x concl then () 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

80 
else error ("No such variable in subgoal: " ^ Syntax.string_of_term ctxt t); 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

81 
val _ = 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

82 
if (exists o Term.exists_subterm) eq_x prems then 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

83 
warning ("Induction variable occurs also among premises: " ^ Syntax.string_of_term ctxt t) 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

84 
else (); 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

85 
in #1 (check_type ctxt t) end; 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

86 

d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

87 
val argss = map (map (Option.map induct_var)) varss; 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

88 
val rule = 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

89 
(case opt_rules of 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

90 
SOME rules => #2 (RuleCases.strict_mutual_rule ctxt rules) 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

91 
 NONE => 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

92 
(case map_filter (RuleCases.mutual_rule ctxt) (Induct.get_inductT ctxt argss) of 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

93 
(_, rule) :: _ => rule 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

94 
 [] => raise THM ("No induction rules", 0, []))); 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

95 

d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

96 
val rule' = rule > Conv.fconv_rule (Conv.concl_conv ~1 ObjectLogic.atomize); 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

97 
val _ = Method.trace ctxt [rule']; 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

98 

d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

99 
val concls = Logic.dest_conjunctions (Thm.concl_of rule); 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

100 
val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths => 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

101 
error "Induction rule has different numbers of variables"; 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

102 
in res_inst_tac ctxt insts rule' i st end 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

103 
handle THM _ => Seq.empty; 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

104 

d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

105 
end; 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

106 

d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

107 
fun induct_tac ctxt args = gen_induct_tac ctxt (args, NONE); 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

108 
fun induct_rules_tac ctxt args rules = gen_induct_tac ctxt (args, SOME rules); 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

109 

d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

110 

d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

111 
(* method syntax *) 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

112 

d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

113 
local 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

114 

d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

115 
val rule_spec = Scan.lift (Args.$$$ "rule"  Args.$$$ ":"); 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

116 
val opt_rule = Scan.option (rule_spec  Attrib.thm); 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

117 
val opt_rules = Scan.option (rule_spec  Attrib.thms); 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

118 

d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

119 
val varss = 
27882
eaa9fef9f4c1
Args.name_source(_position) for proper position information;
wenzelm
parents:
27809
diff
changeset

120 
OuterParse.and_list' 
eaa9fef9f4c1
Args.name_source(_position) for proper position information;
wenzelm
parents:
27809
diff
changeset

121 
(Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_source)))); 
27326
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

122 

d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

123 
in 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

124 

d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

125 
val setup = 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

126 
Method.add_methods 
27882
eaa9fef9f4c1
Args.name_source(_position) for proper position information;
wenzelm
parents:
27809
diff
changeset

127 
[("case_tac", Method.goal_args_ctxt' (Scan.lift Args.name_source  opt_rule) gen_case_tac, 
27326
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

128 
"unstructured case analysis on types"), 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

129 
("induct_tac", Method.goal_args_ctxt' (varss  opt_rules) gen_induct_tac, 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

130 
"unstructured induction on types")]; 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

131 

d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

132 
end; 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

133 

d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

134 
end; 
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff
changeset

135 