0

1 
(* Title: ZF/indrule.ML


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1993 University of Cambridge


5 


6 
Induction rule module  for Inductive/Coinductive Definitions


7 


8 
Proves a strong induction rule and a mutual induction rule


9 
*)


10 


11 
signature INDRULE =


12 
sig


13 
val induct : thm (*main induction rule*)


14 
val mutual_induct : thm (*mutual induction rule*)


15 
end;


16 


17 


18 
functor Indrule_Fun (structure Ind: INDUCTIVE and


19 
Pr: PR and Intr_elim: INTR_ELIM) : INDRULE =


20 
struct


21 
open Logic Ind Intr_elim;


22 


23 
val dummy = writeln "Proving the induction rules...";


24 


25 
(*** Prove the main induction rule ***)


26 


27 
val pred_name = "P"; (*name for predicate variables*)


28 


29 
val prove = prove_term (sign_of Intr_elim.thy);


30 


31 
val big_rec_def::part_rec_defs = Intr_elim.defs;


32 


33 
(*Used to make induction rules;


34 
ind_alist = [(rec_tm1,pred1),...]  associates predicates with rec ops


35 
prem is a premise of an intr rule*)


36 
fun add_induct_prem ind_alist (prem as Const("Trueprop",_) $


37 
(Const("op :",_)$t$X), iprems) =


38 
(case gen_assoc (op aconv) (ind_alist, X) of


39 
Some pred => prem :: mk_tprop (pred $ t) :: iprems


40 
 None => (*possibly membership in M(rec_tm), for M monotone*)


41 
let fun mk_sb (rec_tm,pred) = (rec_tm, Collect_const$rec_tm$pred)


42 
in subst_free (map mk_sb ind_alist) prem :: iprems end)


43 
 add_induct_prem ind_alist (prem,iprems) = prem :: iprems;


44 


45 
(*Make a premise of the induction rule.*)


46 
fun induct_prem ind_alist intr =


47 
let val quantfrees = map dest_Free (term_frees intr \\ rec_params)


48 
val iprems = foldr (add_induct_prem ind_alist)


49 
(strip_imp_prems intr,[])


50 
val (t,X) = rule_concl intr


51 
val (Some pred) = gen_assoc (op aconv) (ind_alist, X)


52 
val concl = mk_tprop (pred $ t)


53 
in list_all_free (quantfrees, list_implies (iprems,concl)) end


54 
handle Bind => error"Recursion term not found in conclusion";


55 


56 
(*Avoids backtracking by delivering the correct premise to each goal*)


57 
fun ind_tac [] 0 = all_tac


58 
 ind_tac(prem::prems) i = REPEAT (ares_tac [Part_eqI,prem] i) THEN


59 
ind_tac prems (i1);


60 


61 
val pred = Free(pred_name, iT>oT);


62 


63 
val ind_prems = map (induct_prem (map (rpair pred) rec_tms)) intr_tms;


64 


65 
val quant_induct =


66 
prove part_rec_defs


67 
(list_implies (ind_prems, mk_tprop (mk_all_imp(big_rec_tm,pred))),


68 
fn prems =>


69 
[rtac (impI RS allI) 1,


70 
etac raw_induct 1,


71 
REPEAT (FIRSTGOAL (eresolve_tac [CollectE,exE,conjE,disjE,ssubst])),


72 
REPEAT (FIRSTGOAL (eresolve_tac [PartE,CollectE])),


73 
ind_tac (rev prems) (length prems) ]);


74 


75 
(*** Prove the simultaneous induction rule ***)


76 


77 
(*Make distinct predicates for each inductive set*)


78 


79 
(*Sigmas and Cartesian products may nest ONLY to the right!*)


80 
fun mk_pred_typ (t $ A $ B) =


81 
if t = Pr.sigma then iT > mk_pred_typ B


82 
else iT > oT


83 
 mk_pred_typ _ = iT > oT


84 


85 
(*Given a recursive set and its domain, return the "fsplit" predicate


86 
and a conclusion for the simultaneous induction rule*)


87 
fun mk_predpair (rec_tm,domt) =


88 
let val rec_name = (#1 o dest_Const o head_of) rec_tm


89 
val T = mk_pred_typ domt


90 
val pfree = Free(pred_name ^ "_" ^ rec_name, T)


91 
val frees = mk_frees "za" (binder_types T)


92 
val qconcl =


93 
foldr mk_all (frees,


94 
imp $ (mem_const $ foldr1 (app Pr.pair) frees $ rec_tm)


95 
$ (list_comb (pfree,frees)))


96 
in (ap_split Pr.fsplit_const pfree (binder_types T),


97 
qconcl)


98 
end;


99 


100 
val (preds,qconcls) = split_list (map mk_predpair (rec_tms~~domts));


101 


102 
(*Used to form simultaneous induction lemma*)


103 
fun mk_rec_imp (rec_tm,pred) =


104 
imp $ (mem_const $ Bound 0 $ rec_tm) $ (pred $ Bound 0);


105 


106 
(*To instantiate the main induction rule*)


107 
val induct_concl =


108 
mk_tprop(mk_all_imp(big_rec_tm,


109 
Abs("z", iT,


110 
fold_bal (app conj)


111 
(map mk_rec_imp (rec_tms~~preds)))))


112 
and mutual_induct_concl = mk_tprop(fold_bal (app conj) qconcls);


113 


114 
val lemma = (*makes the link between the two induction rules*)


115 
prove part_rec_defs


116 
(mk_implies (induct_concl,mutual_induct_concl),


117 
fn prems =>


118 
[cut_facts_tac prems 1,


119 
REPEAT (eresolve_tac [asm_rl,conjE,PartE,mp] 1


120 
ORELSE resolve_tac [allI,impI,conjI,Part_eqI] 1


121 
ORELSE dresolve_tac [spec, mp, Pr.fsplitD] 1)]);


122 


123 
(*Mutual induction follows by freeness of Inl/Inr.*)


124 


125 
(*Removes Collects caused by Moperators in the intro rules*)


126 
val cmonos = [subset_refl RS Collect_mono] RL monos RLN (2,[rev_subsetD]);


127 


128 
(*Avoids backtracking by delivering the correct premise to each goal*)


129 
fun mutual_ind_tac [] 0 = all_tac


130 
 mutual_ind_tac(prem::prems) i =


131 
SELECT_GOAL


132 
((*unpackage and use "prem" in the corresponding place*)


133 
REPEAT (FIRSTGOAL


134 
(eresolve_tac ([conjE,mp]@cmonos) ORELSE'


135 
ares_tac [prem,impI,conjI]))


136 
(*prove remaining goals by contradiction*)


137 
THEN rewrite_goals_tac (con_defs@part_rec_defs)


138 
THEN REPEAT (eresolve_tac (PartE :: sumprod_free_SEs) 1))


139 
i THEN mutual_ind_tac prems (i1);


140 


141 
val mutual_induct_fsplit =


142 
prove []


143 
(list_implies (map (induct_prem (rec_tms~~preds)) intr_tms,


144 
mutual_induct_concl),


145 
fn prems =>


146 
[rtac (quant_induct RS lemma) 1,


147 
mutual_ind_tac (rev prems) (length prems)]);


148 


149 
(*Attempts to remove all occurrences of fsplit*)


150 
val fsplit_tac =


151 
REPEAT (SOMEGOAL (FIRST' [rtac Pr.fsplitI,


152 
dtac Pr.fsplitD,


153 
etac Pr.fsplitE,


154 
bound_hyp_subst_tac]))


155 
THEN prune_params_tac;


156 


157 
(*strip quantifier*)


158 
val induct = standard (quant_induct RS spec RSN (2,rev_mp));


159 


160 
val mutual_induct = rule_by_tactic fsplit_tac mutual_induct_fsplit;


161 


162 
end;
