author  ballarin 
Wed, 19 Jul 2006 19:25:58 +0200  
changeset 20168  ed7bced29e1b 
parent 19904  9956ecabd9af 
child 20288  8ff4a0ea49b2 
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 

11735  5 
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

6 
*) 
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 
signature INDUCT_METHOD_DATA = 
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

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

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

11 
val atomize: thm list 
18465
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

12 
val rulify: thm list 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

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

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

15 

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

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

17 
sig 
18250
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

18 
val fix_tac: Proof.context > int > (string * typ) list > int > tactic 
18287  19 
val add_defs: (string option * term) option list > Proof.context > 
20 
(term option list * thm list) * Proof.context 

18250
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

21 
val atomize_term: theory > term > term 
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

22 
val atomize_tac: int > tactic 
18512  23 
val inner_atomize_tac: int > tactic 
18250
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

24 
val rulified_term: thm > theory * term 
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

25 
val rulify_tac: int > tactic 
18580  26 
val internalize: int > thm > thm 
18259  27 
val guess_instance: thm > int > thm > thm Seq.seq 
16391  28 
val cases_tac: Proof.context > bool > term option list list > thm option > 
18224  29 
thm list > int > cases_tactic 
18178
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

30 
val induct_tac: Proof.context > bool > (string option * term) option list list > 
18465
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

31 
(string * typ) list list > term option list > thm list option > thm list > int > 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

32 
cases_tactic 
18235  33 
val coinduct_tac: Proof.context > bool > term option list > term option list > 
34 
thm option > thm list > int > cases_tactic 

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

36 
end; 
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 
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

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

40 

18465
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

41 
val meta_spec = thm "Pure.meta_spec"; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

42 
val all_conjunction = thm "Pure.all_conjunction"; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

43 
val imp_conjunction = thm "Pure.imp_conjunction"; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

44 
val conjunction_imp = thm "Pure.conjunction_imp"; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

45 
val conjunction_congs = [all_conjunction, imp_conjunction]; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

46 

16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

47 

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

48 

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

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

50 

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

52 

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

53 
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

54 
let val m = length xs and n = length ys 
18678  55 
in if m < n then error 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

56 

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

57 
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

58 
let val m = length xs and n = length ys 
18678  59 
in if m < n then error 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

60 

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

61 

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

63 

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

65 
let 
18205  66 
val cert = Thm.cterm_of thy; 
15531  67 
fun prep_var (x, SOME t) = 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

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

69 
val cx = cert x; 
18147  70 
val {T = xT, thy, ...} = Thm.rep_cterm cx; 
12799
5472afdd3bd3
MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents:
12305
diff
changeset

71 
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

72 
in 
18147  73 
if Sign.typ_instance thy (#T (Thm.rep_cterm ct), xT) then SOME (cx, ct) 
18678  74 
else error (Pretty.string_of (Pretty.block 
11735  75 
[Pretty.str "Illtyped instantiation:", Pretty.fbrk, 
76 
Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1, 

77 
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

78 
end 
15531  79 
 prep_var (_, NONE) = NONE; 
11735  80 
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

81 
in 
11735  82 
align "Rule has fewer variables than instantiations given" xs ts 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19121
diff
changeset

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

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

85 

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

86 

18205  87 
(* trace_rules *) 
88 

89 
fun trace_rules _ kind [] = error ("Unable to figure out " ^ kind ^ " rule") 

90 
 trace_rules ctxt _ rules = Method.trace ctxt rules; 

91 

92 

93 
(* make_cases *) 

18178
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

94 

18224  95 
fun make_cases is_open rule = 
18602  96 
RuleCases.make_common is_open (Thm.theory_of_thm rule, Thm.prop_of rule); 
18224  97 

18178
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

98 
fun warn_open true = warning "Encountered open rule cases  deprecated" 
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

99 
 warn_open false = (); 
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

100 

9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

101 

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

102 

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

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

104 

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

105 
(* 
11735  106 
rule selection scheme: 
18178
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

107 
cases  default case split 
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

108 
`x:A` cases ...  set cases 
11735  109 
cases t  type cases 
18178
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

110 
... 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

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

112 

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

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

114 

18178
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

115 
fun find_casesT ctxt ((SOME t :: _) :: _) = InductAttrib.find_casesT ctxt (Term.fastype_of t) 
11735  116 
 find_casesT _ _ = []; 
117 

18224  118 
fun find_casesS ctxt (fact :: _) = InductAttrib.find_casesS ctxt (Thm.concl_of fact) 
11735  119 
 find_casesS _ _ = []; 
120 

16391  121 
in 
122 

123 
fun cases_tac ctxt is_open 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

124 
let 
18224  125 
val _ = warn_open is_open; 
18147  126 
val thy = ProofContext.theory_of ctxt; 
127 
val cert = Thm.cterm_of thy; 

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

128 

11735  129 
fun inst_rule r = 
18224  130 
if null insts then `RuleCases.get r 
11735  131 
else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19121
diff
changeset

132 
> maps (prep_inst thy align_left I) 
18224  133 
> Drule.cterm_instantiate) r > pair (RuleCases.get r); 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

134 

11735  135 
val ruleq = 
12852  136 
(case opt_rule of 
18205  137 
SOME r => Seq.single (inst_rule r) 
138 
 NONE => 

139 
(find_casesS ctxt facts @ find_casesT ctxt insts @ [Data.cases_default]) 

140 
> tap (trace_rules ctxt InductAttrib.casesN) 

18224  141 
> Seq.of_list > Seq.maps (Seq.try inst_rule)); 
18178
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

142 
in 
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

143 
fn i => fn st => 
18224  144 
ruleq 
18235  145 
> Seq.maps (RuleCases.consume [] facts) 
18224  146 
> Seq.maps (fn ((cases, (_, more_facts)), rule) => 
147 
CASES (make_cases is_open rule cases) 

148 
(Method.insert_tac more_facts i THEN Tactic.rtac rule i) st) 

18178
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

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

150 

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

151 
end; 
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 

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

154 

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

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

156 

18465
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

157 
(* atomize *) 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

158 

18512  159 
fun atomize_term thy = 
160 
MetaSimplifier.rewrite_term thy Data.atomize [] 

18465
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

161 
#> ObjectLogic.drop_judgment thy; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

162 

18512  163 
val atomize_cterm = Tactic.rewrite true Data.atomize; 
18465
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

164 

18512  165 
val atomize_tac = Tactic.rewrite_goal_tac Data.atomize; 
18465
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

166 

18512  167 
val inner_atomize_tac = 
168 
Tactic.rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac; 

18465
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

169 

16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

170 

16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

171 
(* rulify *) 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

172 

16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

173 
fun rulify_term thy = 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

174 
MetaSimplifier.rewrite_term thy (Data.rulify @ conjunction_congs) [] #> 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

175 
MetaSimplifier.rewrite_term thy Data.rulify_fallback []; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

176 

16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

177 
fun rulified_term thm = 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

178 
let 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

179 
val thy = Thm.theory_of_thm thm; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

180 
val rulify = rulify_term thy; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

181 
val (As, B) = Logic.strip_horn (Thm.prop_of thm); 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

182 
in (thy, Logic.list_implies (map rulify As, rulify B)) end; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

183 

16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

184 
val rulify_tac = 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

185 
Tactic.rewrite_goal_tac (Data.rulify @ conjunction_congs) THEN' 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

186 
Tactic.rewrite_goal_tac Data.rulify_fallback THEN' 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

187 
Tactic.conjunction_tac THEN_ALL_NEW 
19121  188 
(Tactic.rewrite_goal_tac [conjunction_imp] THEN' Tactic.norm_hhf_tac); 
18465
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

189 

16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

190 

16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

191 
(* prepare rule *) 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

192 

16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

193 
fun rule_instance thy inst rule = 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

194 
Drule.cterm_instantiate (prep_inst thy align_left I (Thm.prop_of rule, inst)) rule; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

195 

18512  196 
fun internalize k th = 
18465
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

197 
th > Thm.permute_prems 0 k 
18512  198 
> Drule.fconv_rule (Drule.concl_conv (Thm.nprems_of th  k) atomize_cterm); 
18465
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

199 

16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

200 

16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

201 
(* guess rule instantiation  cannot handle pending goal parameters *) 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

202 

16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

203 
local 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

204 

16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

205 
fun dest_env thy (env as Envir.Envir {iTs, ...}) = 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

206 
let 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

207 
val cert = Thm.cterm_of thy; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

208 
val certT = Thm.ctyp_of thy; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

209 
val pairs = Envir.alist_of env; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

210 
val ts = map (cert o Envir.norm_term env o #2 o #2) pairs; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

211 
val xs = map2 (curry (cert o Var)) (map #1 pairs) (map (#T o Thm.rep_cterm) ts); 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

212 
in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) (Vartab.dest iTs), xs ~~ ts) end; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

213 

16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

214 
in 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

215 

16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

216 
fun guess_instance rule i st = 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

217 
let 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

218 
val {thy, maxidx, ...} = Thm.rep_thm st; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

219 
val goal = Thm.term_of (Thm.cprem_of st i); (*exception Subscript*) 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

220 
val params = rev (rename_wrt_term goal (Logic.strip_params goal)); 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

221 
in 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

222 
if not (null params) then 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

223 
(warning ("Cannot determine rule instantiation due to pending parameter(s): " ^ 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

224 
commas_quote (map (Sign.string_of_term thy o Syntax.mark_boundT) params)); 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

225 
Seq.single rule) 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

226 
else 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

227 
let 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

228 
val rule' = Thm.incr_indexes (maxidx + 1) rule; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

229 
val concl = Logic.strip_assums_concl goal; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

230 
in 
19861  231 
Unify.smash_unifiers thy [(Thm.concl_of rule', concl)] 
232 
(Envir.empty (#maxidx (Thm.rep_thm rule'))) 

18465
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

233 
> Seq.map (fn env => Drule.instantiate (dest_env thy env) rule') 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

234 
end 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

235 
end handle Subscript => Seq.empty; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

236 

16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

237 
end; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

238 

16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

239 

16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

240 
(* special renaming of rule parameters *) 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

241 

16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

242 
fun special_rename_params ctxt [[SOME (Free (z, Type (T, _)))]] [thm] = 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

243 
let 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

244 
val x = ProofContext.revert_skolem ctxt z; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

245 
fun index i [] = [] 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

246 
 index i (y :: ys) = 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

247 
if x = y then x ^ string_of_int i :: index (i + 1) ys 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

248 
else y :: index i ys; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

249 
fun rename_params [] = [] 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

250 
 rename_params ((y, Type (U, _)) :: ys) = 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

251 
(if U = T then x else y) :: rename_params ys 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

252 
 rename_params ((y, _) :: ys) = y :: rename_params ys; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

253 
fun rename_asm A = 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

254 
let 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

255 
val xs = rename_params (Logic.strip_params A); 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

256 
val xs' = 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

257 
(case List.filter (equal x) xs of 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

258 
[] => xs  [_] => xs  _ => index 1 xs); 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

259 
in Logic.list_rename_params (xs', A) end; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

260 
fun rename_prop p = 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

261 
let val (As, C) = Logic.strip_horn p 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

262 
in Logic.list_implies (map rename_asm As, C) end; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

263 
val cp' = cterm_fun rename_prop (Thm.cprop_of thm); 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

264 
val thm' = Thm.equal_elim (Thm.reflexive cp') thm; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

265 
in [RuleCases.save thm thm'] end 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

266 
 special_rename_params _ _ ths = ths; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

267 

16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

268 

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

270 

18250
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

271 
local 
18240  272 

18250
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

273 
fun goal_prefix k ((c as Const ("all", _)) $ Abs (a, T, B)) = c $ Abs (a, T, goal_prefix k B) 
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

274 
 goal_prefix 0 _ = Term.dummy_pattern propT 
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

275 
 goal_prefix k ((c as Const ("==>", _)) $ A $ B) = c $ A $ goal_prefix (k  1) B 
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

276 
 goal_prefix _ _ = Term.dummy_pattern propT; 
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

277 

dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

278 
fun goal_params k (Const ("all", _) $ Abs (_, _, B)) = goal_params k B + 1 
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

279 
 goal_params 0 _ = 0 
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

280 
 goal_params k (Const ("==>", _) $ _ $ B) = goal_params (k  1) B 
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

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

282 

18250
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

283 
fun meta_spec_tac ctxt n (x, T) = SUBGOAL (fn (goal, i) => 
18178
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

284 
let 
18250
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

285 
val thy = ProofContext.theory_of ctxt; 
18178
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

286 
val cert = Thm.cterm_of thy; 
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

287 
val certT = Thm.ctyp_of thy; 
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

288 

9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

289 
val v = Free (x, T); 
18250
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

290 
fun spec_rule prfx (xs, body) = 
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

291 
meta_spec 
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

292 
> Thm.rename_params_rule ([ProofContext.revert_skolem ctxt x], 1) 
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

293 
> Thm.lift_rule (cert prfx) 
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

294 
> `(Thm.prop_of #> Logic.strip_assums_concl) 
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

295 
> (fn pred $ arg => 
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

296 
Drule.cterm_instantiate 
18933  297 
[(cert (Term.head_of pred), cert (Logic.rlist_abs (xs, body))), 
298 
(cert (Term.head_of arg), cert (Logic.rlist_abs (xs, v)))]); 

18250
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

299 

dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

300 
fun goal_concl k xs (Const ("all", _) $ Abs (a, T, B)) = goal_concl k ((a, T) :: xs) B 
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

301 
 goal_concl 0 xs B = 
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

302 
if not (Term.exists_subterm (fn t => t aconv v) B) then NONE 
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

303 
else SOME (xs, Term.absfree (x, T, Term.incr_boundvars 1 B)) 
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

304 
 goal_concl k xs (Const ("==>", _) $ _ $ B) = goal_concl (k  1) xs B 
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

305 
 goal_concl _ _ _ = NONE; 
18205  306 
in 
18250
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

307 
(case goal_concl n [] goal of 
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

308 
SOME concl => 
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

309 
(compose_tac (false, spec_rule (goal_prefix n goal) concl, 1) THEN' rtac asm_rl) i 
18631  310 
 NONE => all_tac) 
18250
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

311 
end); 
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

312 

18465
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

313 
fun miniscope_tac p i = PRIMITIVE (Drule.fconv_rule 
18250
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

314 
(Drule.goals_conv (Library.equal i) 
18465
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

315 
(Drule.forall_conv p (Tactic.rewrite true [Thm.symmetric Drule.norm_hhf_eq])))); 
18178
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

316 

9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

317 
in 
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

318 

18250
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

319 
fun fix_tac _ _ [] = K all_tac 
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

320 
 fix_tac ctxt n xs = SUBGOAL (fn (goal, i) => 
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

321 
(EVERY' (map (meta_spec_tac ctxt n) xs) THEN' 
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

322 
(miniscope_tac (goal_params n goal))) i); 
18178
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

323 

9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

324 
end; 
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

325 

9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

326 

18235  327 
(* add_defs *) 
18178
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

328 

9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

329 
fun add_defs def_insts = 
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

330 
let 
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

331 
fun add (SOME (SOME x, t)) ctxt = 
18818  332 
let val ((lhs, def), ctxt') = LocalDefs.add_def (x, t) ctxt 
18178
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

333 
in ((SOME (Free lhs), [def]), ctxt') end 
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

334 
 add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt) 
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

335 
 add NONE ctxt = ((NONE, []), ctxt); 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19121
diff
changeset

336 
in fold_map add def_insts #> apfst (split_list #> apsnd flat) end; 
18178
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

337 

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

338 

18178
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

339 
(* induct_tac *) 
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

340 

9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

341 
(* 
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

342 
rule selection scheme: 
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

343 
`x:A` induct ...  set induction 
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

344 
induct x  type induction 
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

345 
... induct ... r  explicit rule 
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

346 
*) 
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

347 

9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

348 
local 
15235
614a804d7116
Induction now preserves the name of the induction variable.
nipkow
parents:
14981
diff
changeset

349 

11735  350 
fun find_inductT ctxt insts = 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19121
diff
changeset

351 
fold_rev multiply (insts > map_filter (fn [] => NONE  ts => List.last ts) 
18205  352 
> map (InductAttrib.find_inductT ctxt o Term.fastype_of)) [[]] 
18799  353 
> filter_out (forall PureThy.is_internal); 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

354 

18465
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

355 
fun find_inductS ctxt (fact :: _) = map single (InductAttrib.find_inductS ctxt (Thm.concl_of fact)) 
11735  356 
 find_inductS _ _ = []; 
357 

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

359 

18512  360 
fun induct_tac ctxt is_open def_insts fixing taking opt_rule facts = 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

361 
let 
18224  362 
val _ = warn_open is_open; 
18147  363 
val thy = ProofContext.theory_of ctxt; 
364 
val cert = Thm.cterm_of thy; 

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

365 

18178
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

366 
val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt >> split_list; 
18259  367 
val atomized_defs = map (map ObjectLogic.atomize_thm) defs; 
18178
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

368 

18465
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

369 
fun inst_rule (concls, r) = 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

370 
(if null insts then `RuleCases.get r 
18512  371 
else (align_left "Rule has fewer conclusions than arguments given" 
18465
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

372 
(map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19121
diff
changeset

373 
> maps (prep_inst thy align_right (atomize_term thy)) 
18465
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

374 
> Drule.cterm_instantiate) r > pair (RuleCases.get r)) 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

375 
> (fn ((cases, consumes), th) => (((cases, concls), consumes), th)); 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

376 

11735  377 
val ruleq = 
378 
(case opt_rule of 

19904  379 
SOME rs => Seq.single (inst_rule (RuleCases.strict_mutual_rule ctxt rs)) 
18205  380 
 NONE => 
381 
(find_inductS ctxt facts @ 

382 
map (special_rename_params defs_ctxt insts) (find_inductT ctxt insts)) 

19904  383 
> map_filter (RuleCases.mutual_rule ctxt) 
18465
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

384 
> tap (trace_rules ctxt InductAttrib.inductN o map #2) 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

385 
> Seq.of_list > Seq.maps (Seq.try inst_rule)); 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

386 

18602  387 
fun rule_cases rule = 
388 
RuleCases.make_nested is_open (Thm.prop_of rule) (rulified_term rule); 

18178
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

389 
in 
18205  390 
(fn i => fn st => 
18224  391 
ruleq 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19121
diff
changeset

392 
> Seq.maps (RuleCases.consume (flat defs) facts) 
18465
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

393 
> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) => 
18496
ef36f9be255e
proper treatment of nested conjunctions, i.e. simultaneous goals and mutual rules;
wenzelm
parents:
18465
diff
changeset

394 
(PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j => 
ef36f9be255e
proper treatment of nested conjunctions, i.e. simultaneous goals and mutual rules;
wenzelm
parents:
18465
diff
changeset

395 
(CONJUNCTS (ALLGOALS 
18465
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

396 
(Method.insert_tac (more_facts @ nth_list atomized_defs (j  1)) 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

397 
THEN' fix_tac defs_ctxt 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

398 
(nth concls (j  1) + more_consumes) 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

399 
(nth_list fixing (j  1)))) 
18512  400 
THEN' inner_atomize_tac) j)) 
401 
THEN' atomize_tac) i st > Seq.maps (fn st' => 

402 
guess_instance (internalize more_consumes rule) i st' 

18235  403 
> Seq.map (rule_instance thy taking) 
404 
> Seq.maps (fn rule' => 

18224  405 
CASES (rule_cases rule' cases) 
406 
(Tactic.rtac rule' i THEN 

19904  407 
PRIMSEQ (Seq.singleton (ProofContext.exports defs_ctxt ctxt))) st')))) 
18178
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

408 
THEN_ALL_NEW_CASES rulify_tac 
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

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

410 

18205  411 
end; 
412 

413 

414 

415 
(** coinduct method **) 

416 

417 
(* 

418 
rule selection scheme: 

18224  419 
goal "x:A" coinduct ...  set coinduction 
420 
coinduct x  type coinduction 

421 
coinduct ... r  explicit rule 

18205  422 
*) 
423 

424 
local 

425 

426 
fun find_coinductT ctxt (SOME t :: _) = InductAttrib.find_coinductT ctxt (Term.fastype_of t) 

427 
 find_coinductT _ _ = []; 

428 

18224  429 
fun find_coinductS ctxt goal = InductAttrib.find_coinductS ctxt (Logic.strip_assums_concl goal); 
18205  430 

431 
in 

432 

18235  433 
fun coinduct_tac ctxt is_open inst taking opt_rule facts = 
18205  434 
let 
18224  435 
val _ = warn_open is_open; 
18205  436 
val thy = ProofContext.theory_of ctxt; 
437 
val cert = Thm.cterm_of thy; 

438 

18465
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

439 
fun inst_rule r = 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

440 
if null inst then `RuleCases.get r 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

441 
else Drule.cterm_instantiate (prep_inst thy align_left I (Thm.concl_of r, inst)) r 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

442 
> pair (RuleCases.get r); 
18205  443 

18224  444 
fun ruleq goal = 
18205  445 
(case opt_rule of 
18465
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

446 
SOME r => Seq.single (inst_rule r) 
18205  447 
 NONE => 
18224  448 
(find_coinductS ctxt goal @ find_coinductT ctxt inst) 
18205  449 
> tap (trace_rules ctxt InductAttrib.coinductN) 
18465
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

450 
> Seq.of_list > Seq.maps (Seq.try inst_rule)); 
18205  451 
in 
18224  452 
SUBGOAL_CASES (fn (goal, i) => fn st => 
453 
ruleq goal 

18235  454 
> Seq.maps (RuleCases.consume [] facts) 
18224  455 
> Seq.maps (fn ((cases, (_, more_facts)), rule) => 
18259  456 
guess_instance rule i st 
18235  457 
> Seq.map (rule_instance thy taking) 
458 
> Seq.maps (fn rule' => 

18224  459 
CASES (make_cases is_open rule' cases) 
460 
(Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st))) 

18205  461 
end; 
462 

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

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

464 

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

465 

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

466 

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

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

468 

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

469 
val openN = "open"; 
18205  470 
val fixingN = "fixing"; 
18235  471 
val takingN = "taking"; 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

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

473 

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

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

475 

18465
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

476 
fun single_rule [rule] = rule 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

477 
 single_rule _ = error "Single rule expected"; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

478 

15703  479 
fun named_rule k arg get = 
18465
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

480 
Scan.lift (Args.$$$ k  Args.colon)  Scan.repeat arg : 
18988  481 
(fn names => Scan.peek (fn context => Scan.succeed (names > map (fn name => 
482 
(case get (Context.proof_of context) name of SOME x => x 

18465
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

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

484 

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

485 
fun rule get_type get_set = 
18988  486 
named_rule InductAttrib.typeN Args.tyname get_type  
487 
named_rule InductAttrib.setN Args.const get_set  

488 
Scan.lift (Args.$$$ ruleN  Args.colon)  Attrib.thms; 

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

489 

18465
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

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

491 
val induct_rule = rule InductAttrib.lookup_inductT InductAttrib.lookup_inductS; 
18465
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

492 
val coinduct_rule = 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

493 
rule InductAttrib.lookup_coinductT InductAttrib.lookup_coinductS >> single_rule; 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

494 

18988  495 
val inst = Scan.lift (Args.$$$ "_") >> K NONE  Args.term >> SOME; 
18147  496 

18178
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

497 
val def_inst = 
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

498 
((Scan.lift (Args.name  (Args.$$$ "\\<equiv>"  Args.$$$ "==")) >> SOME) 
18988  499 
 Args.term) >> SOME  
18178
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

500 
inst >> Option.map (pair NONE); 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

501 

18988  502 
val free = Scan.state  Args.term >> (fn (_, Free v) => v  (context, t) => 
503 
error ("Bad free variable: " ^ ProofContext.string_of_term (Context.proof_of context) t)); 

18147  504 

18178
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

505 
fun unless_more_args scan = Scan.unless (Scan.lift 
18235  506 
((Args.$$$ fixingN  Args.$$$ takingN  Args.$$$ InductAttrib.typeN  
507 
Args.$$$ InductAttrib.setN  Args.$$$ ruleN)  Args.colon)) scan; 

18205  508 

509 
val fixing = Scan.optional (Scan.lift (Args.$$$ fixingN  Args.colon)  

510 
Args.and_list1 (Scan.repeat (unless_more_args free))) []; 

18178
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

511 

18235  512 
val taking = Scan.optional (Scan.lift (Args.$$$ takingN  Args.colon)  
513 
Scan.repeat1 (unless_more_args inst)) []; 

514 

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

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

516 

18235  517 
fun cases_meth src = 
518 
Method.syntax (Args.mode openN  

519 
(Args.and_list (Scan.repeat (unless_more_args inst))  Scan.option cases_rule)) src 

520 
#> (fn (ctxt, (is_open, (insts, opt_rule))) => 

521 
Method.METHOD_CASES (fn facts => 

522 
Seq.DETERM (HEADGOAL (cases_tac ctxt is_open insts opt_rule facts)))); 

18178
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

523 

18512  524 
fun induct_meth src = 
18235  525 
Method.syntax (Args.mode openN  
526 
(Args.and_list (Scan.repeat (unless_more_args def_inst))  

527 
(fixing  taking  Scan.option induct_rule))) src 

528 
#> (fn (ctxt, (is_open, (insts, ((fixing, taking), opt_rule)))) => 

529 
Method.RAW_METHOD_CASES (fn facts => 

18512  530 
Seq.DETERM (HEADGOAL (induct_tac ctxt is_open insts fixing taking opt_rule facts)))); 
18205  531 

18235  532 
fun coinduct_meth src = 
533 
Method.syntax (Args.mode openN  

534 
(Scan.repeat (unless_more_args inst)  taking  Scan.option coinduct_rule)) src 

535 
#> (fn (ctxt, (is_open, ((insts, taking), opt_rule))) => 

536 
Method.RAW_METHOD_CASES (fn facts => 

537 
Seq.DETERM (HEADGOAL (coinduct_tac ctxt is_open insts taking opt_rule facts)))); 

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

538 

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

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

540 

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

541 

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

542 

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

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

544 

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

545 
val setup = 
18708  546 
Method.add_methods 
18235  547 
[(InductAttrib.casesN, cases_meth, "case analysis on types or sets"), 
18512  548 
(InductAttrib.inductN, induct_meth, "induction on types or sets"), 
18708  549 
(InductAttrib.coinductN, coinduct_meth, "coinduction on types or sets")]; 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

550 

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

551 
end; 