author  wenzelm 
Tue, 10 Jan 2006 19:33:30 +0100  
changeset 18631  ca56111fe69c 
parent 18602  8f25a0f7f446 
child 18678  dd0c569fa43d 
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 

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

35 
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

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_assoc = thm "Pure.conjunction_assoc"; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

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

47 

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

48 

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

49 

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

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

51 

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

53 

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

54 
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

55 
let val m = length xs and n = length ys 
11735  56 
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

57 

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

58 
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

59 
let val m = length xs and n = length ys 
11735  60 
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

61 

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

62 

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

64 

18205  65 
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

66 
let 
18205  67 
val cert = Thm.cterm_of thy; 
15531  68 
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

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

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

72 
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

73 
in 
18147  74 
if Sign.typ_instance thy (#T (Thm.rep_cterm ct), xT) then SOME (cx, ct) 
11735  75 
else raise ERROR_MESSAGE (Pretty.string_of (Pretty.block 
76 
[Pretty.str "Illtyped instantiation:", Pretty.fbrk, 

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

78 
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

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

82 
in 
11735  83 
align "Rule has fewer variables than instantiations given" xs ts 
15570  84 
> List.mapPartial prep_var 
11670
59f79df42d1f
proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff
changeset

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

86 

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

87 

18205  88 
(* trace_rules *) 
89 

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

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

92 

93 

94 
(* make_cases *) 

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

95 

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

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

99 
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

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

101 

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

102 

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

103 

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

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

105 

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

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

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

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

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

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

113 

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

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

115 

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

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

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

16391  122 
in 
123 

124 
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

125 
let 
18224  126 
val _ = warn_open is_open; 
18147  127 
val thy = ProofContext.theory_of ctxt; 
128 
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

129 

11735  130 
fun inst_rule r = 
18224  131 
if null insts then `RuleCases.get r 
11735  132 
else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts 
18205  133 
> (List.concat o map (prep_inst thy align_left I)) 
18224  134 
> 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

135 

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

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

141 
> tap (trace_rules ctxt InductAttrib.casesN) 

18224  142 
> 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

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

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

149 
(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

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

151 

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

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

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

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

157 

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

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

159 

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

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

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

163 

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

165 

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

167 

18512  168 
val inner_atomize_tac = 
169 
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

170 

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

171 

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

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

173 

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

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

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

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

177 

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

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

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

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

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

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

183 
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

184 

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

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

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

187 
val rule = conjunction_imp; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

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

189 
val proc = Simplifier.simproc_i thy "curry_prems" 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

190 
[#1 (Logic.dest_equals (Thm.prop_of rule))] 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

191 
(fn _ => fn ss => fn _ => (*WORKAROUND: prevent descending into meta conjunctions*) 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

192 
if exists (equal propT o #2 o #1) (#2 (#bounds (#1 (Simplifier.rep_ss ss)))) 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

193 
then NONE else SOME rule); 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

194 
val ss = MetaSimplifier.theory_context thy Simplifier.empty_ss addsimprocs [proc]; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

195 
in Simplifier.full_simp_tac ss end; 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

196 

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

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

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

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

200 
Tactic.conjunction_tac THEN_ALL_NEW 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

201 
(curry_prems_tac THEN' Tactic.norm_hhf_tac); 
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 

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

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

205 

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

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

207 
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

208 

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

210 
th > Thm.permute_prems 0 k 
18512  211 
> 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

212 

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 
(* guess rule instantiation  cannot handle pending goal parameters *) 
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 
local 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

217 

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

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

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

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

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

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

223 
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

224 
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

225 
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

226 

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

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

228 

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

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

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

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

232 
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

233 
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

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

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

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

237 
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

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

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

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

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

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

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

244 
Unify.smash_unifiers (thy, Envir.empty (#maxidx (Thm.rep_thm rule')), 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

245 
[(Thm.concl_of rule', concl)]) 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

246 
> 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

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

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

249 

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

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

251 

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

252 

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

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

254 

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

255 
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

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

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

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

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

260 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

280 

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

281 

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

283 

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

284 
local 
18240  285 

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

286 
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

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

288 
 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

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

290 

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

291 
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

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

293 
 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

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

295 

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

296 
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

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

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

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

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

301 

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

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

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

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

305 
> 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

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

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

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

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

310 
[(cert (Term.head_of pred), cert (Unify.rlist_abs (xs, body))), 
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

311 
(cert (Term.head_of arg), cert (Unify.rlist_abs (xs, v)))]); 
dfe5d09514eb
fix_tac: proper treatment of major premises in goal;
wenzelm
parents:
18240
diff
changeset

312 

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

313 
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

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

315 
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

316 
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

317 
 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

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

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

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

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

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

325 

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

326 
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

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

328 
(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

329 

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

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

331 

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

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

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

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

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

336 

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

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

338 

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

339 

18235  340 
(* add_defs *) 
18178
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 
fun add_defs def_insts = 
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

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

344 
fun add (SOME (SOME x, t)) ctxt = 
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

345 
let val ((lhs, def), ctxt') = ProofContext.add_def (x, t) ctxt 
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

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

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

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

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

350 

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

351 

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

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

353 

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

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

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

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

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

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

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

360 

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

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

362 

11735  363 
fun find_inductT ctxt insts = 
18147  364 
fold_rev multiply (insts > List.mapPartial (fn [] => NONE  ts => List.last ts) 
18205  365 
> map (InductAttrib.find_inductT ctxt o Term.fastype_of)) [[]] 
18465
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

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

367 

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

368 
fun find_inductS ctxt (fact :: _) = map single (InductAttrib.find_inductS ctxt (Thm.concl_of fact)) 
11735  369 
 find_inductS _ _ = []; 
370 

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

372 

18512  373 
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

374 
let 
18224  375 
val _ = warn_open is_open; 
18147  376 
val thy = ProofContext.theory_of ctxt; 
377 
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

378 

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

379 
val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt >> split_list; 
18259  380 
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

381 

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

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

383 
(if null insts then `RuleCases.get r 
18512  384 
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

385 
(map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts 
18512  386 
> (List.concat o map (prep_inst thy align_right (atomize_term thy))) 
18465
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

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

388 
> (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

389 

11735  390 
val ruleq = 
391 
(case opt_rule of 

18580  392 
SOME rs => Seq.single (inst_rule (RuleCases.strict_mutual_rule rs)) 
18205  393 
 NONE => 
394 
(find_inductS ctxt facts @ 

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

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

396 
> List.mapPartial RuleCases.mutual_rule 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

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

398 
> 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

399 

18602  400 
fun rule_cases rule = 
401 
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

402 
in 
18205  403 
(fn i => fn st => 
18224  404 
ruleq 
18235  405 
> Seq.maps (RuleCases.consume (List.concat defs) facts) 
18465
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

406 
> 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

407 
(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

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

409 
(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

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

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

412 
(nth_list fixing (j  1)))) 
18512  413 
THEN' inner_atomize_tac) j)) 
414 
THEN' atomize_tac) i st > Seq.maps (fn st' => 

415 
guess_instance (internalize more_consumes rule) i st' 

18235  416 
> Seq.map (rule_instance thy taking) 
417 
> Seq.maps (fn rule' => 

18224  418 
CASES (rule_cases rule' cases) 
419 
(Tactic.rtac rule' i THEN 

420 
PRIMSEQ (ProofContext.exports defs_ctxt ctxt)) st')))) 

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

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

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

423 

18205  424 
end; 
425 

426 

427 

428 
(** coinduct method **) 

429 

430 
(* 

431 
rule selection scheme: 

18224  432 
goal "x:A" coinduct ...  set coinduction 
433 
coinduct x  type coinduction 

434 
coinduct ... r  explicit rule 

18205  435 
*) 
436 

437 
local 

438 

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

440 
 find_coinductT _ _ = []; 

441 

18224  442 
fun find_coinductS ctxt goal = InductAttrib.find_coinductS ctxt (Logic.strip_assums_concl goal); 
18205  443 

444 
in 

445 

18235  446 
fun coinduct_tac ctxt is_open inst taking opt_rule facts = 
18205  447 
let 
18224  448 
val _ = warn_open is_open; 
18205  449 
val thy = ProofContext.theory_of ctxt; 
450 
val cert = Thm.cterm_of thy; 

451 

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

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

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

454 
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

455 
> pair (RuleCases.get r); 
18205  456 

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

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

463 
> Seq.of_list > Seq.maps (Seq.try inst_rule)); 
18205  464 
in 
18224  465 
SUBGOAL_CASES (fn (goal, i) => fn st => 
466 
ruleq goal 

18235  467 
> Seq.maps (RuleCases.consume [] facts) 
18224  468 
> Seq.maps (fn ((cases, (_, more_facts)), rule) => 
18259  469 
guess_instance rule i st 
18235  470 
> Seq.map (rule_instance thy taking) 
471 
> Seq.maps (fn rule' => 

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

18205  474 
end; 
475 

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

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

477 

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

478 

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

479 

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

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

481 

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

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

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

486 

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

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

488 

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

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

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

491 

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

493 
Scan.lift (Args.$$$ k  Args.colon)  Scan.repeat arg : 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

494 
(fn names => Scan.peek (fn ctxt => Scan.succeed (names > map (fn name => 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

495 
(case get ctxt name of SOME x => x 
16dcd36499b8
simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents:
18330
diff
changeset

496 
 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

497 

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

498 
fun rule get_type get_set = 
15703  499 
named_rule InductAttrib.typeN Args.local_tyname get_type  
500 
named_rule InductAttrib.setN Args.local_const get_set  

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

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

502 

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

503 
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

504 
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

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

506 
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

507 

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

508 
val inst = Scan.lift (Args.$$$ "_") >> K NONE  Args.local_term >> SOME; 
18147  509 

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

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

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

512 
 Args.local_term) >> SOME  
9e4dfe031525
induct: support local definitions to be passed through the induction;
wenzelm
parents:
18147
diff
changeset

513 
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

514 

18147  515 
val free = Scan.state  Args.local_term >> (fn (_, Free v) => v  (ctxt, t) => 
516 
error ("Bad free variable: " ^ ProofContext.string_of_term ctxt t)); 

517 

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

518 
fun unless_more_args scan = Scan.unless (Scan.lift 
18235  519 
((Args.$$$ fixingN  Args.$$$ takingN  Args.$$$ InductAttrib.typeN  
520 
Args.$$$ InductAttrib.setN  Args.$$$ ruleN)  Args.colon)) scan; 

18205  521 

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

523 
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

524 

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

527 

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

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

529 

18235  530 
fun cases_meth src = 
531 
Method.syntax (Args.mode openN  

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

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

534 
Method.METHOD_CASES (fn facts => 

535 
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

536 

18512  537 
fun induct_meth src = 
18235  538 
Method.syntax (Args.mode openN  
539 
(Args.and_list (Scan.repeat (unless_more_args def_inst))  

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

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

542 
Method.RAW_METHOD_CASES (fn facts => 

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

18235  545 
fun coinduct_meth src = 
546 
Method.syntax (Args.mode openN  

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

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

549 
Method.RAW_METHOD_CASES (fn facts => 

550 
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

551 

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

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

553 

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

554 

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

555 

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

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

557 

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

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

559 
[Method.add_methods 
18235  560 
[(InductAttrib.casesN, cases_meth, "case analysis on types or sets"), 
18512  561 
(InductAttrib.inductN, induct_meth, "induction on types or sets"), 
18235  562 
(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

563 

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

564 
end; 