author  wenzelm 
Thu, 17 Jan 2002 21:02:18 +0100  
changeset 12799  5472afdd3bd3 
parent 12305  3c3f98b3d9e7 
child 12852  c6a8e310aec5 
permissions  rwrr 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

1 
(* Title: Provers/induct_method.ML 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

3 
Author: Markus Wenzel, TU Muenchen 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

5 

11735  6 
Proof by cases and induction on sets and types. 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

7 
*) 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

8 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

9 
signature INDUCT_METHOD_DATA = 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

10 
sig 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

11 
val dest_concls: term > term list 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

12 
val cases_default: thm 
11996
b409a8cbe1fb
induct: internalize ``missing'' consumesfacts from goal state
wenzelm
parents:
11984
diff
changeset

13 
val local_impI: thm 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

14 
val conjI: thm 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

15 
val atomize: thm list 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

16 
val rulify1: thm list 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

17 
val rulify2: thm list 
12240  18 
val localize: thm list 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

19 
end; 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

20 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

21 
signature INDUCT_METHOD = 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

22 
sig 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

23 
val setup: (theory > theory) list 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

24 
end; 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

25 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

26 
functor InductMethodFun(Data: INDUCT_METHOD_DATA): INDUCT_METHOD = 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

27 
struct 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

28 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

29 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

30 
(** misc utils **) 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

31 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

32 
(* align lists *) 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

33 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

34 
fun align_left msg xs ys = 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

35 
let val m = length xs and n = length ys 
11735  36 
in if m < n then raise ERROR_MESSAGE msg else (Library.take (n, xs) ~~ ys) end; 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

37 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

38 
fun align_right msg xs ys = 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

39 
let val m = length xs and n = length ys 
11735  40 
in if m < n then raise ERROR_MESSAGE msg else (Library.drop (m  n, xs) ~~ ys) end; 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

41 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

42 

11735  43 
(* prep_inst *) 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

44 

11735  45 
fun prep_inst align cert tune (tm, ts) = 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

46 
let 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

47 
fun prep_var (x, Some t) = 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

48 
let 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

49 
val cx = cert x; 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

50 
val {T = xT, sign, ...} = Thm.rep_cterm cx; 
12799
5472afdd3bd3
MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents:
12305
diff
changeset

51 
val ct = cert (tune t); 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

52 
in 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

53 
if Sign.typ_instance sign (#T (Thm.rep_cterm ct), xT) then Some (cx, ct) 
11735  54 
else raise ERROR_MESSAGE (Pretty.string_of (Pretty.block 
55 
[Pretty.str "Illtyped instantiation:", Pretty.fbrk, 

56 
Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1, 

57 
Display.pretty_ctyp (#T (Thm.crep_cterm ct))])) 

11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

58 
end 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

59 
 prep_var (_, None) = None; 
11735  60 
val xs = InductAttrib.vars_of tm; 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

61 
in 
11735  62 
align "Rule has fewer variables than instantiations given" xs ts 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

63 
> mapfilter prep_var 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

64 
end; 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

65 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

66 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

67 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

68 
(** cases method **) 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

69 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

70 
(* 
11735  71 
rule selection scheme: 
72 
cases  classical case split 

73 
<x:A> cases ...  set cases 

74 
cases t  type cases 

75 
... cases ... R  explicit rule 

11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

76 
*) 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

77 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

78 
local 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

79 

11790
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

80 
fun resolveq_cases_tac make ruleq i st = 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

81 
ruleq > Seq.map (fn (rule, (cases, facts)) => 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

82 
(Method.insert_tac facts THEN' Tactic.rtac rule) i st 
12799
5472afdd3bd3
MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents:
12305
diff
changeset

83 
> Seq.map (rpair (make (Thm.sign_of_thm rule, Thm.prop_of rule) cases))) 
11790
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

84 
> Seq.flat; 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

85 

11735  86 
fun find_casesT ctxt ((Some t :: _) :: _) = InductAttrib.find_casesT ctxt (fastype_of t) 
87 
 find_casesT _ _ = []; 

88 

89 
fun find_casesS ctxt (fact :: _) = InductAttrib.find_casesS ctxt fact 

90 
 find_casesS _ _ = []; 

91 

92 
fun cases_tac (ctxt, (open_parms, (insts, opt_rule))) facts = 

11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

93 
let 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

94 
val sg = ProofContext.sign_of ctxt; 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

95 
val cert = Thm.cterm_of sg; 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

96 

11735  97 
fun inst_rule r = 
98 
if null insts then RuleCases.add r 

99 
else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts 

11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

100 
> (flat o map (prep_inst align_left cert I)) 
11735  101 
> Drule.cterm_instantiate) r > rpair (RuleCases.get r); 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

102 

11735  103 
val ruleq = 
104 
(case (facts, insts, opt_rule) of 

105 
([], [], None) => Seq.single (RuleCases.add Data.cases_default) 

106 
 (_, _, None) => 

107 
let val rules = find_casesS ctxt facts @ find_casesT ctxt insts in 

108 
if null rules then error "Unable to figure out cases rule" else (); 

12053  109 
Method.trace ctxt rules; 
11735  110 
Seq.flat (Seq.map (Seq.try inst_rule) (Seq.of_list rules)) 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

111 
end 
11735  112 
 (_, _, Some r) => Seq.single (inst_rule r)); 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

113 

11735  114 
fun prep_rule (th, (cases, n)) = Seq.map (apsnd (rpair (drop (n, facts))) o rpair cases) 
115 
(Method.multi_resolves (take (n, facts)) [th]); 

11790
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

116 
in resolveq_cases_tac (RuleCases.make open_parms) (Seq.flat (Seq.map prep_rule ruleq)) end; 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

117 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

118 
in 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

119 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

120 
val cases_meth = Method.METHOD_CASES o (HEADGOAL oo cases_tac); 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

121 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

122 
end; 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

123 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

124 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

125 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

126 
(** induct method **) 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

127 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

128 
(* 
11735  129 
rule selection scheme: 
130 
<x:A> induct ...  set induction 

131 
induct x  type induction 

132 
... induct ... R  explicit rule 

11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

133 
*) 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

134 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

135 
local 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

136 

11790
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

137 

42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

138 
(* atomize and rulify *) 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

139 

12799
5472afdd3bd3
MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents:
12305
diff
changeset

140 
fun atomize_term sg = 
5472afdd3bd3
MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents:
12305
diff
changeset

141 
ObjectLogic.drop_judgment sg o MetaSimplifier.rewrite_term sg Data.atomize; 
5472afdd3bd3
MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents:
12305
diff
changeset

142 

5472afdd3bd3
MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents:
12305
diff
changeset

143 
fun rulified_term thm = 
5472afdd3bd3
MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents:
12305
diff
changeset

144 
let val sg = Thm.sign_of_thm thm in 
5472afdd3bd3
MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents:
12305
diff
changeset

145 
Thm.prop_of thm 
5472afdd3bd3
MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents:
12305
diff
changeset

146 
> MetaSimplifier.rewrite_term sg Data.rulify1 
5472afdd3bd3
MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents:
12305
diff
changeset

147 
> MetaSimplifier.rewrite_term sg Data.rulify2 
5472afdd3bd3
MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents:
12305
diff
changeset

148 
> pair sg 
5472afdd3bd3
MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents:
12305
diff
changeset

149 
end; 
11756  150 

11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

151 
val atomize_tac = Tactic.rewrite_goal_tac Data.atomize; 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

152 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

153 
val rulify_tac = 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

154 
Tactic.rewrite_goal_tac Data.rulify1 THEN' 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

155 
Tactic.rewrite_goal_tac Data.rulify2 THEN' 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

156 
Tactic.norm_hhf_tac; 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

157 

12799
5472afdd3bd3
MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents:
12305
diff
changeset

158 
val localize = Tactic.norm_hhf_rule o Tactic.simplify false Data.localize; 
12162  159 

11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

160 

11996
b409a8cbe1fb
induct: internalize ``missing'' consumesfacts from goal state
wenzelm
parents:
11984
diff
changeset

161 
(* imp_intr  limited to atomic prems *) 
b409a8cbe1fb
induct: internalize ``missing'' consumesfacts from goal state
wenzelm
parents:
11984
diff
changeset

162 

b409a8cbe1fb
induct: internalize ``missing'' consumesfacts from goal state
wenzelm
parents:
11984
diff
changeset

163 
fun imp_intr i raw_th = 
b409a8cbe1fb
induct: internalize ``missing'' consumesfacts from goal state
wenzelm
parents:
11984
diff
changeset

164 
let 
b409a8cbe1fb
induct: internalize ``missing'' consumesfacts from goal state
wenzelm
parents:
11984
diff
changeset

165 
val th = Thm.permute_prems (i  1) 1 raw_th; 
b409a8cbe1fb
induct: internalize ``missing'' consumesfacts from goal state
wenzelm
parents:
11984
diff
changeset

166 
val cprems = Drule.cprems_of th; 
b409a8cbe1fb
induct: internalize ``missing'' consumesfacts from goal state
wenzelm
parents:
11984
diff
changeset

167 
val As = take (length cprems  1, cprems); 
b409a8cbe1fb
induct: internalize ``missing'' consumesfacts from goal state
wenzelm
parents:
11984
diff
changeset

168 
val C = Thm.cterm_of (Thm.sign_of_thm th) (Var (("C", #maxidx (Thm.rep_thm th) + 1), propT)); 
b409a8cbe1fb
induct: internalize ``missing'' consumesfacts from goal state
wenzelm
parents:
11984
diff
changeset

169 
val dummy_st = Drule.mk_triv_goal (Drule.list_implies (As, C)); 
b409a8cbe1fb
induct: internalize ``missing'' consumesfacts from goal state
wenzelm
parents:
11984
diff
changeset

170 
in th COMP Thm.lift_rule (dummy_st, 1) Data.local_impI end; 
b409a8cbe1fb
induct: internalize ``missing'' consumesfacts from goal state
wenzelm
parents:
11984
diff
changeset

171 

b409a8cbe1fb
induct: internalize ``missing'' consumesfacts from goal state
wenzelm
parents:
11984
diff
changeset

172 

11790
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

173 
(* join multirules *) 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

174 

11735  175 
val eq_prems = curry (Term.aconvs o pairself Thm.prems_of); 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

176 

11735  177 
fun join_rules [] = [] 
178 
 join_rules [th] = [th] 

179 
 join_rules (rules as r :: rs) = 

180 
if not (forall (eq_prems r) rs) then [] 

181 
else 

182 
let 

183 
val th :: ths = map Drule.freeze_all rules; 

184 
val cprems = Drule.cprems_of th; 

185 
val asms = map Thm.assume cprems; 

186 
in 

187 
[foldr1 (fn (x, x') => [x, x'] MRS Data.conjI) 

188 
(map (fn x => Drule.implies_elim_list x asms) (th :: ths)) 

189 
> Drule.implies_intr_list cprems 

12305  190 
> Drule.standard' 
191 
> RuleCases.save th] 

11735  192 
end; 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

193 

11790
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

194 

42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

195 
(* divinate rule instantiation (cannot handle pending goal parameters) *) 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

196 

11808  197 
fun dest_env sign (env as Envir.Envir {asol, iTs, ...}) = 
11790
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

198 
let 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

199 
val pairs = Vartab.dest asol; 
11808  200 
val ts = map (Thm.cterm_of sign o Envir.norm_term env o #2) pairs; 
11790
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

201 
val xs = map2 (Thm.cterm_of sign o Var) (map #1 pairs, map (#T o Thm.rep_cterm) ts); 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

202 
in (map (apsnd (Thm.ctyp_of sign)) (Vartab.dest iTs), xs ~~ ts) end; 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

203 

42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

204 
fun divinate_inst rule i st = 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

205 
let 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

206 
val {sign, maxidx, ...} = Thm.rep_thm st; 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

207 
val goal = List.nth (Thm.prems_of st, i  1); (*exception Subscript*) 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

208 
val params = rev (rename_wrt_term goal (Logic.strip_params goal)); (*as they are printed :*) 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

209 
in 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

210 
if not (null params) then 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

211 
(warning ("Cannot determine rule instantiation due to pending parameter(s): " ^ 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

212 
commas (map (Sign.string_of_term sign o Syntax.mark_boundT) params)); 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

213 
Seq.single rule) 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

214 
else 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

215 
let 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

216 
val rule' = Thm.incr_indexes (maxidx + 1) rule; 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

217 
val concl = Logic.strip_assums_concl goal; 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

218 
in 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

219 
Unify.smash_unifiers (sign, Envir.empty (#maxidx (Thm.rep_thm rule')), 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

220 
[(Thm.concl_of rule', concl)]) 
12162  221 
> Seq.map (fn env => Drule.instantiate (dest_env sign env) rule') 
11790
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

222 
end 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

223 
end handle Subscript => Seq.empty; 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

224 

42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

225 

42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

226 
(* compose tactics with cases *) 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

227 

11996
b409a8cbe1fb
induct: internalize ``missing'' consumesfacts from goal state
wenzelm
parents:
11984
diff
changeset

228 
fun internalize k th = if k > 0 then internalize (k  1) (imp_intr k th) else th; 
b409a8cbe1fb
induct: internalize ``missing'' consumesfacts from goal state
wenzelm
parents:
11984
diff
changeset

229 

11790
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

230 
fun resolveq_cases_tac' make ruleq i st = 
11996
b409a8cbe1fb
induct: internalize ``missing'' consumesfacts from goal state
wenzelm
parents:
11984
diff
changeset

231 
ruleq > Seq.map (fn (rule, (cases, k, more_facts)) => st 
b409a8cbe1fb
induct: internalize ``missing'' consumesfacts from goal state
wenzelm
parents:
11984
diff
changeset

232 
> (Method.insert_tac more_facts THEN' atomize_tac) i 
b409a8cbe1fb
induct: internalize ``missing'' consumesfacts from goal state
wenzelm
parents:
11984
diff
changeset

233 
> Seq.map (fn st' => divinate_inst (internalize k rule) i st' > Seq.map (fn rule' => 
12799
5472afdd3bd3
MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents:
12305
diff
changeset

234 
st' > Tactic.rtac rule' i 
5472afdd3bd3
MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents:
12305
diff
changeset

235 
> Seq.map (rpair (make (rulified_term rule') cases))) 
5472afdd3bd3
MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents:
12305
diff
changeset

236 
> Seq.flat) 
11790
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

237 
> Seq.flat) 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

238 
> Seq.flat; 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

239 

42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

240 
infix 1 THEN_ALL_NEW_CASES; 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

241 

42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

242 
fun (tac1 THEN_ALL_NEW_CASES tac2) i st = 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

243 
st > Seq.THEN (tac1 i, (fn (st', cases) => 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

244 
Seq.map (rpair cases) (Seq.INTERVAL tac2 i (i + nprems_of st'  nprems_of st) st'))); 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

245 

42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

246 

42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

247 
(* find rules *) 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

248 

11735  249 
fun find_inductT ctxt insts = 
250 
foldr multiply (insts > mapfilter (fn [] => None  ts => last_elem ts) 

251 
> map (InductAttrib.find_inductT ctxt o fastype_of), [[]]) 

252 
> map join_rules > flat; 

11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

253 

11735  254 
fun find_inductS ctxt (fact :: _) = InductAttrib.find_inductS ctxt fact 
255 
 find_inductS _ _ = []; 

256 

11790
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

257 

42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

258 
(* main tactic *) 
42393a11642d
simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents:
11781
diff
changeset

259 

11735  260 
fun induct_tac (ctxt, (open_parms, (insts, opt_rule))) facts = 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

261 
let 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

262 
val sg = ProofContext.sign_of ctxt; 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

263 
val cert = Thm.cterm_of sg; 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

264 

12168
dc93c2e82205
induct: rule_versions produces localized variants;
wenzelm
parents:
12162
diff
changeset

265 
fun rule_versions r = Seq.cons (r, Seq.filter (not o curry eq_thm r) 
dc93c2e82205
induct: rule_versions produces localized variants;
wenzelm
parents:
12162
diff
changeset

266 
(Seq.make (fn () => Some (localize r, Seq.empty)))) 
dc93c2e82205
induct: rule_versions produces localized variants;
wenzelm
parents:
12162
diff
changeset

267 
> Seq.map (rpair (RuleCases.get r)); 
dc93c2e82205
induct: rule_versions produces localized variants;
wenzelm
parents:
12162
diff
changeset

268 

dc93c2e82205
induct: rule_versions produces localized variants;
wenzelm
parents:
12162
diff
changeset

269 
val inst_rule = apfst (fn r => 
dc93c2e82205
induct: rule_versions produces localized variants;
wenzelm
parents:
12162
diff
changeset

270 
if null insts then r 
11735  271 
else (align_right "Rule has fewer conclusions than arguments given" 
272 
(Data.dest_concls (Thm.concl_of r)) insts 

12799
5472afdd3bd3
MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents:
12305
diff
changeset

273 
> (flat o map (prep_inst align_right cert (atomize_term sg))) 
12168
dc93c2e82205
induct: rule_versions produces localized variants;
wenzelm
parents:
12162
diff
changeset

274 
> Drule.cterm_instantiate) r); 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

275 

11735  276 
val ruleq = 
277 
(case opt_rule of 

278 
None => 

279 
let val rules = find_inductS ctxt facts @ find_inductT ctxt insts in 

12168
dc93c2e82205
induct: rule_versions produces localized variants;
wenzelm
parents:
12162
diff
changeset

280 
conditional (null rules) (fn () => error "Unable to figure out induct rule"); 
12053  281 
Method.trace ctxt rules; 
12168
dc93c2e82205
induct: rule_versions produces localized variants;
wenzelm
parents:
12162
diff
changeset

282 
rules > Seq.THEN (Seq.of_list, Seq.THEN (rule_versions, Seq.try inst_rule)) 
11735  283 
end 
12168
dc93c2e82205
induct: rule_versions produces localized variants;
wenzelm
parents:
12162
diff
changeset

284 
 Some r => r > Seq.THEN (rule_versions, Seq.single o inst_rule)); 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

285 

11735  286 
fun prep_rule (th, (cases, n)) = 
11996
b409a8cbe1fb
induct: internalize ``missing'' consumesfacts from goal state
wenzelm
parents:
11984
diff
changeset

287 
Seq.map (rpair (cases, n  length facts, drop (n, facts))) 
b409a8cbe1fb
induct: internalize ``missing'' consumesfacts from goal state
wenzelm
parents:
11984
diff
changeset

288 
(Method.multi_resolves (take (n, facts)) [th]); 
11984  289 
val tac = resolveq_cases_tac' (RuleCases.make open_parms) (Seq.flat (Seq.map prep_rule ruleq)); 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

290 
in tac THEN_ALL_NEW_CASES rulify_tac end; 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

291 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

292 
in 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

293 

12162  294 
val induct_meth = Method.RAW_METHOD_CASES o (HEADGOAL oo induct_tac); 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

295 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

296 
end; 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

297 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

298 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

299 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

300 
(** concrete syntax **) 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

301 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

302 
val openN = "open"; 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

303 
val ruleN = "rule"; 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

304 
val ofN = "of"; 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

305 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

306 
local 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

307 

11735  308 
fun check k get name = 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

309 
(case get name of Some x => x 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

310 
 None => error ("No rule for " ^ k ^ " " ^ quote name)); 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

311 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

312 
fun spec k = (Args.$$$ k  Args.colon)  Args.!!! Args.name; 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

313 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

314 
fun rule get_type get_set = 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

315 
Scan.depend (fn ctxt => 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

316 
let val sg = ProofContext.sign_of ctxt in 
11735  317 
spec InductAttrib.typeN >> (check InductAttrib.typeN (get_type ctxt) o 
318 
Sign.certify_tyname sg o Sign.intern_tycon sg)  

319 
spec InductAttrib.setN >> (check InductAttrib.setN (get_set ctxt) o 

320 
Sign.certify_const sg o Sign.intern_const sg) 

11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

321 
end >> pair ctxt)  
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

322 
Scan.lift (Args.$$$ ruleN  Args.colon)  Attrib.local_thm; 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

323 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

324 
val cases_rule = rule InductAttrib.lookup_casesT InductAttrib.lookup_casesS; 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

325 
val induct_rule = rule InductAttrib.lookup_inductT InductAttrib.lookup_inductS; 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

326 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

327 
val kind_inst = 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

328 
(Args.$$$ InductAttrib.typeN  Args.$$$ InductAttrib.setN  Args.$$$ ruleN  Args.$$$ ofN) 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

329 
 Args.colon; 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

330 
val term = Scan.unless (Scan.lift kind_inst) Args.local_term; 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

331 
val term_dummy = Scan.unless (Scan.lift kind_inst) 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

332 
(Scan.lift (Args.$$$ "_") >> K None  Args.local_term >> Some); 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

333 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

334 
val instss = Args.and_list (Scan.repeat1 term_dummy); 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

335 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

336 
in 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

337 

11735  338 
val cases_args = Method.syntax (Args.mode openN  (instss  Scan.option cases_rule)); 
339 
val induct_args = Method.syntax (Args.mode openN  (instss  Scan.option induct_rule)); 

11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

340 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

341 
end; 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

342 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

343 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

344 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

345 
(** theory setup **) 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

346 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

347 
val setup = 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

348 
[Method.add_methods 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

349 
[(InductAttrib.casesN, cases_meth oo cases_args, "case analysis on types or sets"), 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

350 
(InductAttrib.inductN, induct_meth oo induct_args, "induction on types or sets")]]; 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

351 

59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

352 
end; 