5094

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


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Stefan Berghofer, TU Muenchen


5 
Copyright 1994 University of Cambridge


6 
1998 TU Muenchen


7 


8 
(Co)Inductive Definition module for HOL


9 


10 
Features:


11 
* least or greatest fixedpoints


12 
* userspecified product and sum constructions


13 
* mutually recursive definitions


14 
* definitions involving arbitrary monotone operators


15 
* automatically proves introduction and elimination rules


16 


17 
The recursive sets must *already* be declared as constants in parent theory!


18 


19 
Introduction rules have the form


20 
[ ti:M(Sj), ..., P(x), ... ] ==> t: Sk ]


21 
where M is some monotone operator (usually the identity)


22 
P(x) is any side condition on the free variables


23 
ti, t are any terms


24 
Sj, Sk are two of the sets being defined in mutual recursion


25 


26 
Sums are used only for mutual recursion;


27 
Products are used only to derive "streamlined" induction rules for relations


28 
*)


29 


30 
signature INDUCTIVE_PACKAGE =


31 
sig


32 
val add_inductive_i : bool > bool > bstring > bool > bool > bool > term list >


33 
term list > thm list > thm list > theory > theory *


34 
{defs:thm list, elims:thm list, raw_induct:thm, induct:thm,


35 
intrs:thm list,


36 
mk_cases:thm list > string > thm, mono:thm,


37 
unfold:thm}


38 
val add_inductive : bool > bool > string list > string list


39 
> thm list > thm list > theory > theory *


40 
{defs:thm list, elims:thm list, raw_induct:thm, induct:thm,


41 
intrs:thm list,


42 
mk_cases:thm list > string > thm, mono:thm,


43 
unfold:thm}


44 
end;


45 


46 
structure InductivePackage : INDUCTIVE_PACKAGE =


47 
struct


48 


49 
(*For proving monotonicity of recursion operator*)


50 
val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono,


51 
ex_mono, Collect_mono, in_mono, vimage_mono];


52 


53 
val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (concl_of vimageD);


54 


55 
(*Delete needless equality assumptions*)


56 
val refl_thin = prove_goal HOL.thy "!!P. [ a=a; P ] ==> P"


57 
(fn _ => [assume_tac 1]);


58 


59 
(*For simplifying the elimination rule*)


60 
val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, disjE, Pair_inject];


61 


62 
val vimage_name = Sign.intern_const (sign_of Vimage.thy) "op ``";


63 
val mono_name = Sign.intern_const (sign_of Ord.thy) "mono";


64 


65 
(* make injections needed in mutually recursive definitions *)


66 


67 
fun mk_inj cs sumT c x =


68 
let


69 
fun mk_inj' T n i =


70 
if n = 1 then x else


71 
let val n2 = n div 2;


72 
val Type (_, [T1, T2]) = T


73 
in


74 
if i <= n2 then


75 
Const ("Inl", T1 > T) $ (mk_inj' T1 n2 i)


76 
else


77 
Const ("Inr", T2 > T) $ (mk_inj' T2 (n  n2) (i  n2))


78 
end


79 
in mk_inj' sumT (length cs) (1 + find_index_eq c cs)


80 
end;


81 


82 
(* make "vimage" terms for selecting out components of mutually rec.def. *)


83 


84 
fun mk_vimage cs sumT t c = if length cs < 2 then t else


85 
let


86 
val cT = HOLogic.dest_setT (fastype_of c);


87 
val vimageT = [cT > sumT, HOLogic.mk_setT sumT] > HOLogic.mk_setT cT


88 
in


89 
Const (vimage_name, vimageT) $


90 
Abs ("y", cT, mk_inj cs sumT c (Bound 0)) $ t


91 
end;


92 


93 
(**************************** wellformedness checks **************************)


94 


95 
fun err_in_rule sign t msg = error ("Illformed introduction rule\n" ^


96 
(Sign.string_of_term sign t) ^ "\n" ^ msg);


97 


98 
fun err_in_prem sign t p msg = error ("Illformed premise\n" ^


99 
(Sign.string_of_term sign p) ^ "\nin introduction rule\n" ^


100 
(Sign.string_of_term sign t) ^ "\n" ^ msg);


101 


102 
val msg1 = "Conclusion of introduction rule must have form\


103 
\ ' t : S_i '";


104 
val msg2 = "Premises mentioning recursive sets must have form\


105 
\ ' t : M S_i '";


106 
val msg3 = "Recursion term on left of member symbol";


107 


108 
fun check_rule sign cs r =


109 
let


110 
fun check_prem prem = if exists (Logic.occs o (rpair prem)) cs then


111 
(case prem of


112 
(Const ("op :", _) $ t $ u) =>


113 
if exists (Logic.occs o (rpair t)) cs then


114 
err_in_prem sign r prem msg3 else ()


115 
 _ => err_in_prem sign r prem msg2)


116 
else ()


117 


118 
in (case (HOLogic.dest_Trueprop o Logic.strip_imp_concl) r of


119 
(Const ("op :", _) $ _ $ u) =>


120 
if u mem cs then map (check_prem o HOLogic.dest_Trueprop)


121 
(Logic.strip_imp_prems r)


122 
else err_in_rule sign r msg1


123 
 _ => err_in_rule sign r msg1)


124 
end;


125 


126 
fun try' f msg sign t = (f t) handle _ => error (msg ^ Sign.string_of_term sign t);


127 


128 
(*********************** properties of (co)inductive sets *********************)


129 


130 
(***************************** elimination rules ******************************)


131 


132 
fun mk_elims cs cTs params intr_ts =


133 
let


134 
val used = foldr add_term_names (intr_ts, []);


135 
val [aname, pname] = variantlist (["a", "P"], used);


136 
val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));


137 


138 
fun dest_intr r =


139 
let val Const ("op :", _) $ t $ u =


140 
HOLogic.dest_Trueprop (Logic.strip_imp_concl r)


141 
in (u, t, Logic.strip_imp_prems r) end;


142 


143 
val intrs = map dest_intr intr_ts;


144 


145 
fun mk_elim (c, T) =


146 
let


147 
val a = Free (aname, T);


148 


149 
fun mk_elim_prem (_, t, ts) =


150 
list_all_free (map dest_Free ((foldr add_term_frees (t::ts, [])) \\ params),


151 
Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P));


152 
in


153 
Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) ::


154 
map mk_elim_prem (filter (equal c o #1) intrs), P)


155 
end


156 
in


157 
map mk_elim (cs ~~ cTs)


158 
end;


159 


160 
(***************** premises and conclusions of induction rules ****************)


161 


162 
fun mk_indrule cs cTs params intr_ts =


163 
let


164 
val used = foldr add_term_names (intr_ts, []);


165 


166 
(* predicates for induction rule *)


167 


168 
val preds = map Free (variantlist (if length cs < 2 then ["P"] else


169 
map (fn i => "P" ^ string_of_int i) (1 upto length cs), used) ~~


170 
map (fn T => T > HOLogic.boolT) cTs);


171 


172 
(* transform an introduction rule into a premise for induction rule *)


173 


174 
fun mk_ind_prem r =


175 
let


176 
val frees = map dest_Free ((add_term_frees (r, [])) \\ params);


177 


178 
fun subst (prem as (Const ("op :", T) $ t $ u), prems) =


179 
let val n = find_index_eq u cs in


180 
if n >= 0 then prem :: (nth_elem (n, preds)) $ t :: prems else


181 
(subst_free (map (fn (c, P) => (c, HOLogic.mk_binop "op Int"


182 
(c, HOLogic.Collect_const (HOLogic.dest_setT


183 
(fastype_of c)) $ P))) (cs ~~ preds)) prem)::prems


184 
end


185 
 subst (prem, prems) = prem::prems;


186 


187 
val Const ("op :", _) $ t $ u =


188 
HOLogic.dest_Trueprop (Logic.strip_imp_concl r)


189 


190 
in list_all_free (frees,


191 
Logic.list_implies (map HOLogic.mk_Trueprop (foldr subst


192 
(map HOLogic.dest_Trueprop (Logic.strip_imp_prems r), [])),


193 
HOLogic.mk_Trueprop (nth_elem (find_index_eq u cs, preds) $ t)))


194 
end;


195 


196 
val ind_prems = map mk_ind_prem intr_ts;


197 


198 
(* make conclusions for induction rules *)


199 


200 
fun mk_ind_concl ((c, P), (ts, x)) =


201 
let val T = HOLogic.dest_setT (fastype_of c);


202 
val Ts = HOLogic.prodT_factors T;


203 
val (frees, x') = foldr (fn (T', (fs, s)) =>


204 
((Free (s, T'))::fs, bump_string s)) (Ts, ([], x));


205 
val tuple = HOLogic.mk_tuple T frees;


206 
in ((HOLogic.mk_binop "op >"


207 
(HOLogic.mk_mem (tuple, c), P $ tuple))::ts, x')


208 
end;


209 


210 
val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 (app HOLogic.conj)


211 
(fst (foldr mk_ind_concl (cs ~~ preds, ([], "xa")))))


212 


213 
in (preds, ind_prems, mutual_ind_concl)


214 
end;


215 


216 
(********************** proofs for (co)inductive sets *************************)


217 


218 
(**************************** prove monotonicity ******************************)


219 


220 
fun prove_mono setT fp_fun monos thy =


221 
let


222 
val _ = writeln " Proving monotonicity...";


223 


224 
val mono = prove_goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop


225 
(Const (mono_name, (setT > setT) > HOLogic.boolT) $ fp_fun)))


226 
(fn _ => [rtac monoI 1, REPEAT (ares_tac (basic_monos @ monos) 1)])


227 


228 
in mono end;


229 


230 
(************************* prove introduction rules ***************************)


231 


232 
fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy =


233 
let


234 
val _ = writeln " Proving the introduction rules...";


235 


236 
val unfold = standard (mono RS (fp_def RS


237 
(if coind then def_gfp_Tarski else def_lfp_Tarski)));


238 


239 
fun select_disj 1 1 = []


240 
 select_disj _ 1 = [rtac disjI1]


241 
 select_disj n i = (rtac disjI2)::(select_disj (n  1) (i  1));


242 


243 
val intrs = map (fn (i, intr) => prove_goalw_cterm rec_sets_defs


244 
(cterm_of (sign_of thy) intr) (fn prems =>


245 
[(*insert prems and underlying sets*)


246 
cut_facts_tac prems 1,


247 
stac unfold 1,


248 
REPEAT (resolve_tac [vimageI2, CollectI] 1),


249 
(*Now 12 subgoals: the disjunction, perhaps equality.*)


250 
EVERY1 (select_disj (length intr_ts) i),


251 
(*Not ares_tac, since refl must be tried before any equality assumptions;


252 
backtracking may occur if the premises have extra variables!*)


253 
DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 1 APPEND assume_tac 1),


254 
(*Now solve the equations like Inl 0 = Inl ?b2*)


255 
rewrite_goals_tac con_defs,


256 
REPEAT (rtac refl 1)])) (1 upto (length intr_ts) ~~ intr_ts)


257 


258 
in (intrs, unfold) end;


259 


260 
(*************************** prove elimination rules **************************)


261 


262 
fun prove_elims cs cTs params intr_ts unfold rec_sets_defs thy =


263 
let


264 
val _ = writeln " Proving the elimination rules...";


265 


266 
val rules1 = [CollectE, disjE, make_elim vimageD];


267 
val rules2 = [exE, conjE, Inl_neq_Inr, Inr_neq_Inl] @


268 
map make_elim [Inl_inject, Inr_inject];


269 


270 
val elims = map (fn t => prove_goalw_cterm rec_sets_defs


271 
(cterm_of (sign_of thy) t) (fn prems =>


272 
[cut_facts_tac [hd prems] 1,


273 
dtac (unfold RS subst) 1,


274 
REPEAT (FIRSTGOAL (eresolve_tac rules1)),


275 
REPEAT (FIRSTGOAL (eresolve_tac rules2)),


276 
EVERY (map (fn prem =>


277 
DEPTH_SOLVE_1 (ares_tac (prem::[conjI]) 1)) (tl prems))]))


278 
(mk_elims cs cTs params intr_ts)


279 


280 
in elims end;


281 


282 
(** derivation of simplified elimination rules **)


283 


284 
(*Applies freeness of the given constructors, which *must* be unfolded by


285 
the given defs. Cannot simply use the local con_defs because con_defs=[]


286 
for inference systems.


287 
FIXME: proper handling of conjunctive / disjunctive side conditions?!


288 
*)


289 
fun con_elim_tac simps =


290 
let val elim_tac = REPEAT o (eresolve_tac elim_rls)


291 
in ALLGOALS(EVERY'[elim_tac,


292 
asm_full_simp_tac (simpset_of Nat.thy addsimps simps),


293 
elim_tac,


294 
REPEAT o bound_hyp_subst_tac])


295 
THEN prune_params_tac


296 
end;


297 


298 
(*String s should have the form t:Si where Si is an inductive set*)


299 
fun mk_cases elims defs s =


300 
let val prem = assume (read_cterm (sign_of_thm (hd elims)) (s, propT));


301 
val elims' = map (try (fn r =>


302 
rule_by_tactic (con_elim_tac defs) (prem RS r) > standard)) elims


303 
in case find_first is_some elims' of


304 
Some (Some r) => r


305 
 None => error ("mk_cases: string '" ^ s ^ "' not of form 't : S_i'")


306 
end;


307 


308 
(**************************** prove induction rule ****************************)


309 


310 
fun prove_indrule cs cTs sumT rec_const params intr_ts mono


311 
fp_def rec_sets_defs thy =


312 
let


313 
val _ = writeln " Proving the induction rule...";


314 


315 
val sign = sign_of thy;


316 


317 
val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;


318 


319 
(* make predicate for instantiation of abstract induction rule *)


320 


321 
fun mk_ind_pred _ [P] = P


322 
 mk_ind_pred T Ps =


323 
let val n = (length Ps) div 2;


324 
val Type (_, [T1, T2]) = T


325 
in Const ("sum_case",


326 
[T1 > HOLogic.boolT, T2 > HOLogic.boolT, T] > HOLogic.boolT) $


327 
mk_ind_pred T1 (take (n, Ps)) $ mk_ind_pred T2 (drop (n, Ps))


328 
end;


329 


330 
val ind_pred = mk_ind_pred sumT preds;


331 


332 
val ind_concl = HOLogic.mk_Trueprop


333 
(HOLogic.all_const sumT $ Abs ("x", sumT, HOLogic.mk_binop "op >"


334 
(HOLogic.mk_mem (Bound 0, rec_const), ind_pred $ Bound 0)));


335 


336 
(* simplification rules for vimage and Collect *)


337 


338 
val vimage_simps = if length cs < 2 then [] else


339 
map (fn c => prove_goalw_cterm [] (cterm_of sign


340 
(HOLogic.mk_Trueprop (HOLogic.mk_eq


341 
(mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c,


342 
HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $


343 
nth_elem (find_index_eq c cs, preds)))))


344 
(fn _ => [rtac vimage_Collect 1, rewrite_goals_tac


345 
(map mk_meta_eq [sum_case_Inl, sum_case_Inr]),


346 
rtac refl 1])) cs;


347 


348 
val induct = prove_goalw_cterm [] (cterm_of sign


349 
(Logic.list_implies (ind_prems, ind_concl))) (fn prems =>


350 
[rtac (impI RS allI) 1,


351 
DETERM (etac (mono RS (fp_def RS def_induct)) 1),


352 
rewrite_goals_tac (map mk_meta_eq (vimage_Int::vimage_simps)),


353 
fold_goals_tac rec_sets_defs,


354 
(*This CollectE and disjE separates out the introduction rules*)


355 
REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE])),


356 
(*Now break down the individual cases. No disjE here in case


357 
some premise involves disjunction.*)


358 
REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE]


359 
ORELSE' hyp_subst_tac)),


360 
rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),


361 
EVERY (map (fn prem =>


362 
DEPTH_SOLVE_1 (ares_tac (prem::[conjI, refl]) 1)) prems)]);


363 


364 
val lemma = prove_goalw_cterm rec_sets_defs (cterm_of sign


365 
(Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>


366 
[cut_facts_tac prems 1,


367 
REPEAT (EVERY


368 
[REPEAT (resolve_tac [conjI, impI] 1),


369 
TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,


370 
rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),


371 
atac 1])])


372 


373 
in standard (split_rule (induct RS lemma))


374 
end;


375 


376 
(*************** definitional introduction of (co)inductive sets **************)


377 


378 
fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs


379 
intr_ts monos con_defs thy params paramTs cTs cnames =


380 
let


381 
val _ = if verbose then writeln ("Proofs for " ^


382 
(if coind then "co" else "") ^ "inductive set(s) " ^ commas cnames) else ();


383 


384 
val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;


385 
val setT = HOLogic.mk_setT sumT;


386 


387 
val fp_name = if coind then Sign.intern_const (sign_of Gfp.thy) "gfp"


388 
else Sign.intern_const (sign_of Lfp.thy) "lfp";


389 


390 
(* transform an introduction rule into a conjunction *)


391 
(* [ t : ... S_i ... ; ... ] ==> u : S_j *)


392 
(* is transformed into *)


393 
(* x = Inj_j u & t : ... Inj_i `` S ... & ... *)


394 


395 
fun transform_rule r =


396 
let


397 
val frees = map dest_Free ((add_term_frees (r, [])) \\ params);


398 
val idx = length frees;


399 
val subst = subst_free (cs ~~ (map (mk_vimage cs sumT (Bound (idx + 1))) cs));


400 
val Const ("op :", _) $ t $ u =


401 
HOLogic.dest_Trueprop (Logic.strip_imp_concl r)


402 


403 
in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))


404 
(frees, foldr1 (app HOLogic.conj)


405 
(((HOLogic.eq_const sumT) $ Bound idx $ (mk_inj cs sumT u t))::


406 
(map (subst o HOLogic.dest_Trueprop)


407 
(Logic.strip_imp_prems r))))


408 
end


409 


410 
(* make a disjunction of all introduction rules *)


411 


412 
val fp_fun = Abs ("S", setT, (HOLogic.Collect_const sumT) $


413 
Abs ("x", sumT, foldr1 (app HOLogic.disj) (map transform_rule intr_ts)));


414 


415 
(* add definiton of recursive sets to theory *)


416 


417 
val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;


418 
val full_rec_name = Sign.full_name (sign_of thy) rec_name;


419 


420 
val rec_const = list_comb


421 
(Const (full_rec_name, paramTs > setT), params);


422 


423 
val fp_def_term = Logic.mk_equals (rec_const,


424 
Const (fp_name, (setT > setT) > setT) $ fp_fun)


425 


426 
val def_terms = fp_def_term :: (if length cs < 2 then [] else


427 
map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs);


428 


429 
val thy' = thy >


430 
(if declare_consts then


431 
Theory.add_consts_i (map (fn (c, n) =>


432 
(n, paramTs > fastype_of c, NoSyn)) (cs ~~ cnames))


433 
else I) >


434 
(if length cs < 2 then I else


435 
Theory.add_consts_i [(rec_name, paramTs > setT, NoSyn)]) >


436 
Theory.add_path rec_name >


437 
PureThy.add_defss_i [(("defs", def_terms), [])];


438 


439 
(* get definitions from theory *)


440 


441 
val fp_def::rec_sets_defs = get_thms thy' "defs";


442 


443 
(* prove and store theorems *)


444 


445 
val mono = prove_mono setT fp_fun monos thy';


446 
val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts con_defs


447 
rec_sets_defs thy';


448 
val elims = if no_elim then [] else


449 
prove_elims cs cTs params intr_ts unfold rec_sets_defs thy';


450 
val raw_induct = if no_ind then TrueI else


451 
if coind then standard (rule_by_tactic


452 
(rewrite_tac [mk_meta_eq vimage_Un] THEN


453 
fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct)))


454 
else


455 
prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def


456 
rec_sets_defs thy';


457 
val induct = if coind orelse length cs > 1 then raw_induct


458 
else standard (raw_induct RSN (2, rev_mp));


459 


460 
val thy'' = thy' >


461 
PureThy.add_tthmss [(("intrs", map Attribute.tthm_of intrs), [])] >


462 
(if no_elim then I else PureThy.add_tthmss


463 
[(("elims", map Attribute.tthm_of elims), [])]) >


464 
(if no_ind then I else PureThy.add_tthms


465 
[(((if coind then "co" else "") ^ "induct",


466 
Attribute.tthm_of induct), [])]) >


467 
Theory.parent_path;


468 


469 
in (thy'',


470 
{defs = fp_def::rec_sets_defs,


471 
mono = mono,


472 
unfold = unfold,


473 
intrs = intrs,


474 
elims = elims,


475 
mk_cases = mk_cases elims,


476 
raw_induct = raw_induct,


477 
induct = induct})


478 
end;


479 


480 
(***************** axiomatic introduction of (co)inductive sets ***************)


481 


482 
fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs


483 
intr_ts monos con_defs thy params paramTs cTs cnames =


484 
let


485 
val _ = if verbose then writeln ("Adding axioms for " ^


486 
(if coind then "co" else "") ^ "inductive set(s) " ^ commas cnames) else ();


487 


488 
val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;


489 


490 
val elim_ts = mk_elims cs cTs params intr_ts;


491 


492 
val (_, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;


493 
val ind_t = Logic.list_implies (ind_prems, mutual_ind_concl);


494 


495 
val thy' = thy >


496 
(if declare_consts then


497 
Theory.add_consts_i (map (fn (c, n) =>


498 
(n, paramTs > fastype_of c, NoSyn)) (cs ~~ cnames))


499 
else I) >


500 
Theory.add_path rec_name >


501 
PureThy.add_axiomss_i [(("intrs", intr_ts), []), (("elims", elim_ts), [])] >


502 
(if coind then I


503 
else PureThy.add_axioms_i [(("internal_induct", ind_t), [])]);


504 


505 
val intrs = get_thms thy' "intrs";


506 
val elims = get_thms thy' "elims";


507 
val raw_induct = if coind then TrueI else


508 
standard (split_rule (get_thm thy' "internal_induct"));


509 
val induct = if coind orelse length cs > 1 then raw_induct


510 
else standard (raw_induct RSN (2, rev_mp));


511 


512 
val thy'' = thy' >


513 
(if coind then I


514 
else PureThy.add_tthms [(("induct", Attribute.tthm_of induct), [])]) >


515 
Theory.parent_path


516 


517 
in (thy'',


518 
{defs = [],


519 
mono = TrueI,


520 
unfold = TrueI,


521 
intrs = intrs,


522 
elims = elims,


523 
mk_cases = mk_cases elims,


524 
raw_induct = raw_induct,


525 
induct = induct})


526 
end;


527 


528 
(********************** introduction of (co)inductive sets ********************)


529 


530 
fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs


531 
intr_ts monos con_defs thy =


532 
let


533 
val _ = Theory.requires thy "Inductive"


534 
((if coind then "co" else "") ^ "inductive definitions");


535 


536 
val sign = sign_of thy;


537 


538 
(*parameters should agree for all mutually recursive components*)


539 
val (_, params) = strip_comb (hd cs);


540 
val paramTs = map (try' (snd o dest_Free) "Parameter in recursive\


541 
\ component is not a free variable: " sign) params;


542 


543 
val cTs = map (try' (HOLogic.dest_setT o fastype_of)


544 
"Recursive component not of type set: " sign) cs;


545 


546 
val cnames = map (try' (Sign.base_name o fst o dest_Const o head_of)


547 
"Recursive set not previously declared as constant: " sign) cs;


548 


549 
val _ = assert_all Syntax.is_identifier cnames


550 
(fn a => "Base name of recursive set not an identifier: " ^ a);


551 


552 
val _ = map (check_rule sign cs) intr_ts;


553 


554 
in


555 
(if !quick_and_dirty then add_ind_axm else add_ind_def)


556 
verbose declare_consts alt_name coind no_elim no_ind cs intr_ts monos


557 
con_defs thy params paramTs cTs cnames


558 
end;


559 


560 
(***************************** external interface *****************************)


561 


562 
fun add_inductive verbose coind c_strings intr_strings monos con_defs thy =


563 
let


564 
val sign = sign_of thy;


565 
val cs = map (readtm (sign_of thy) HOLogic.termTVar) c_strings;


566 
val intr_ts = map (readtm (sign_of thy) propT) intr_strings;


567 


568 
(* the following code ensures that each recursive set *)


569 
(* always has the same type in all introduction rules *)


570 


571 
val {tsig, ...} = Sign.rep_sg sign;


572 
val add_term_consts_2 =


573 
foldl_aterms (fn (cs, Const c) => c ins cs  (cs, _) => cs);


574 
fun varify (t, (i, ts)) =


575 
let val t' = map_term_types (incr_tvar (i + 1)) (Type.varify (t, []))


576 
in (maxidx_of_term t', t'::ts) end;


577 
val (i, cs') = foldr varify (cs, (~1, []));


578 
val (i', intr_ts') = foldr varify (intr_ts, (i, []));


579 
val rec_consts = foldl add_term_consts_2 ([], cs');


580 
val intr_consts = foldl add_term_consts_2 ([], intr_ts');


581 
fun unify (env, (cname, cT)) =


582 
let val consts = map snd (filter (fn c => fst c = cname) intr_consts)


583 
in (foldl (fn ((env', j'), Tp) => Type.unify tsig j' env' Tp)


584 
(env, (replicate (length consts) cT) ~~ consts)) handle _ =>


585 
error ("Occurrences of constant '" ^ cname ^


586 
"' have incompatible types")


587 
end;


588 
val (env, _) = foldl unify (([], i'), rec_consts);


589 
fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars env T


590 
in if T = T' then T else typ_subst_TVars_2 env T' end;


591 
val subst = fst o Type.freeze_thaw o


592 
(map_term_types (typ_subst_TVars_2 env));


593 
val cs'' = map subst cs';


594 
val intr_ts'' = map subst intr_ts';


595 


596 
in add_inductive_i verbose false "" coind false false cs'' intr_ts''


597 
monos con_defs thy


598 
end;


599 


600 
end;
