6442

1 
(* Title: HOL/Tools/induct_method.ML


2 
ID: $Id$


3 
Author: Markus Wenzel, TU Muenchen


4 


5 
Proof by induction on types / set / functions.


6 
*)


7 


8 
signature INDUCT_METHOD =


9 
sig


10 
val setup: (theory > theory) list


11 
end;


12 


13 
structure InductMethod: INDUCT_METHOD =


14 
struct


15 


16 


17 
(* type induct_kind *)


18 

7512

19 
datatype induct_kind = Type  Set  Function  Rule;

6442

20 

7512

21 
val kind_name =


22 
Args.$$$ "type" >> K Type 


23 
Args.$$$ "set" >> K Set 


24 
Args.$$$ "function" >> K Function 


25 
Args.$$$ "rule" >> K Rule;

6442

26 

7512

27 
val kind = kind_name  Args.$$$ ":";

6442

28 


29 

6446

30 
(* induct_rule *)


31 

7017

32 
fun kind_rule Type = (#induction oo DatatypePackage.datatype_info_err, Sign.intern_tycon)

6446

33 
 kind_rule Set = ((#induct o #2) oo InductivePackage.get_inductive, Sign.intern_const)

7512

34 
 kind_rule Function = (#induct oo RecdefPackage.get_recdef, Sign.intern_const)


35 
 kind_rule Rule = (PureThy.get_thm, K I);

6446

36 


37 
fun induct_rule thy kind name =


38 
let val (ind_rule, intern) = kind_rule kind


39 
in ind_rule thy (intern (Theory.sign_of thy) name) end;


40 


41 

6442

42 
(* induct_tac *)


43 

6518

44 
fun induct_tac thy insts opt_kind_name facts i state =

6442

45 
let


46 
val (kind, name) =


47 
(case opt_kind_name of Some kind_name => kind_name  None =>

6446

48 
(case try (#1 o Term.dest_Type o Term.type_of o #2 o hd) insts of

6442

49 
Some name => (Type, name)


50 
 None => error "Unable to figure out induction rule"));


51 
val rule = Drule.incr_indexes_wrt [] [] [] [state] (induct_rule thy kind name);


52 

6446

53 
val cert = Thm.cterm_of (Sign.merge (pairself Thm.sign_of_thm (state, rule)));


54 


55 
fun prep_inst ((P $ x), (Some Q, y)) = [(cert P, cert Q), (cert x, cert y)]


56 
 prep_inst ((_ $ x), (None, y)) = [(cert x, cert y)]


57 
 prep_inst _ = raise THM ("Malformed induction rule", 0, [rule]);


58 


59 
val prep_insts = flat o map2 prep_inst;


60 


61 
val inst_rule =


62 
if null insts then rule


63 
else Drule.cterm_instantiate (prep_insts


64 
(DatatypeAux.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of rule)), insts)) rule;

6518

65 
in Method.rule_tac [inst_rule] facts i state end;

6442

66 


67 


68 
(* induct_method *)


69 


70 
val term = Scan.unless (Scan.lift kind) Args.local_term;

6446

71 
val inst = term  term >> (apfst Some)  term >> pair None;

6442

72 


73 
fun induct ctxt =

6446

74 
Args.and_list inst  Scan.option (Scan.lift (kind  Args.name))

6518

75 
>> (fn (is, k) => Method.METHOD (FIRSTGOAL o induct_tac (ProofContext.theory_of ctxt) is k));

6442

76 


77 
fun induct_meth src ctxt = #2 (Method.syntax (induct ctxt) ctxt src);

7512

78 
val induct_method = ("induct", induct_meth, "induction on types, sets, functions etc.");

6442

79 


80 


81 
(* theory setup *)


82 


83 
val setup = [Method.add_methods [induct_method]];


84 


85 


86 
end;
