6051

1 
(* Title: ZF/inductive_package.ML


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1994 University of Cambridge


5 


6 
Fixedpoint definition module  for Inductive/Coinductive Definitions


7 


8 
The functor will be instantiated for normal sums/products (inductive defs)


9 
and nonstandard sums/products (coinductive defs)


10 


11 
Sums are used only for mutual recursion;


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


13 
*)


14 


15 


16 
type inductive_result =


17 
{defs : thm list, (*definitions made in thy*)


18 
bnd_mono : thm, (*monotonicity for the lfp definition*)


19 
dom_subset : thm, (*inclusion of recursive set in dom*)


20 
intrs : thm list, (*introduction rules*)


21 
elim : thm, (*case analysis theorem*)

6141

22 
mk_cases : string > thm, (*generates case theorems*)

6051

23 
induct : thm, (*main induction rule*)


24 
mutual_induct : thm}; (*mutual induction rule*)


25 


26 


27 
(*Functor's result signature*)


28 
signature INDUCTIVE_PACKAGE =


29 
sig


30 


31 
(*Insert definitions for the recursive sets, which


32 
must *already* be declared as constants in parent theory!*)


33 
val add_inductive_i :


34 
bool >


35 
term list * term * term list * thm list * thm list * thm list * thm list


36 
> theory > theory * inductive_result


37 


38 
val add_inductive :


39 
string list * string * string list *


40 
thm list * thm list * thm list * thm list


41 
> theory > theory * inductive_result


42 


43 
end;


44 


45 


46 
(*Declares functions to add fixedpoint/constructor defs to a theory.


47 
Recursive sets must *already* be declared as constants.*)


48 
functor Add_inductive_def_Fun


49 
(structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU)


50 
: INDUCTIVE_PACKAGE =


51 
struct


52 
open Logic Ind_Syntax;


53 

7695

54 


55 
(* utils *)


56 


57 
(*make distinct individual variables a1, a2, a3, ..., an. *)


58 
fun mk_frees a [] = []


59 
 mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts;


60 


61 
(*read an assumption in the given theory*)


62 
fun assume_read thy a = Thm.assume (read_cterm (Theory.sign_of thy) (a,propT));


63 


64 


65 
(* add_inductive(_i) *)


66 

6051

67 
(*internal version, accepting terms*)


68 
fun add_inductive_i verbose (rec_tms, dom_sum, intr_tms,


69 
monos, con_defs, type_intrs, type_elims) thy =


70 
let


71 
val dummy = (*has essential ancestors?*)


72 
Theory.requires thy "Inductive" "(co)inductive definitions"


73 


74 
val sign = sign_of thy;


75 


76 
(*recT and rec_params should agree for all mutually recursive components*)


77 
val rec_hds = map head_of rec_tms;


78 


79 
val dummy = assert_all is_Const rec_hds


80 
(fn t => "Recursive set not previously declared as constant: " ^


81 
Sign.string_of_term sign t);


82 


83 
(*Now we know they are all Consts, so get their names, type and params*)


84 
val rec_names = map (#1 o dest_Const) rec_hds


85 
and (Const(_,recT),rec_params) = strip_comb (hd rec_tms);


86 


87 
val rec_base_names = map Sign.base_name rec_names;


88 
val dummy = assert_all Syntax.is_identifier rec_base_names


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


90 


91 
local (*Checking the introduction rules*)


92 
val intr_sets = map (#2 o rule_concl_msg sign) intr_tms;


93 
fun intr_ok set =


94 
case head_of set of Const(a,recT) => a mem rec_names  _ => false;


95 
in


96 
val dummy = assert_all intr_ok intr_sets


97 
(fn t => "Conclusion of rule does not name a recursive set: " ^


98 
Sign.string_of_term sign t);


99 
end;


100 


101 
val dummy = assert_all is_Free rec_params


102 
(fn t => "Param in recursion term not a free variable: " ^


103 
Sign.string_of_term sign t);


104 


105 
(*** Construct the fixedpoint definition ***)


106 
val mk_variant = variant (foldr add_term_names (intr_tms,[]));


107 


108 
val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";


109 


110 
fun dest_tprop (Const("Trueprop",_) $ P) = P


111 
 dest_tprop Q = error ("Illformed premise of introduction rule: " ^


112 
Sign.string_of_term sign Q);


113 


114 
(*Makes a disjunct from an introduction rule*)


115 
fun fp_part intr = (*quantify over rule's free vars except parameters*)


116 
let val prems = map dest_tprop (strip_imp_prems intr)


117 
val dummy = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds


118 
val exfrees = term_frees intr \\ rec_params


119 
val zeq = FOLogic.mk_eq (Free(z',iT), #1 (rule_concl intr))


120 
in foldr FOLogic.mk_exists

7695

121 
(exfrees, fold_bal FOLogic.mk_conj (zeq::prems))

6051

122 
end;


123 


124 
(*The Part(A,h) terms  compose injections to make h*)


125 
fun mk_Part (Bound 0) = Free(X',iT) (*no mutual rec, no Part needed*)


126 
 mk_Part h = Part_const $ Free(X',iT) $ Abs(w',iT,h);


127 


128 
(*Access to balanced disjoint sums via injections*)


129 
val parts =

7695

130 
map mk_Part (accesses_bal (fn t => Su.inl $ t, fn t => Su.inr $ t, Bound 0)

6051

131 
(length rec_tms));


132 


133 
(*replace each set by the corresponding Part(A,h)*)


134 
val part_intrs = map (subst_free (rec_tms ~~ parts) o fp_part) intr_tms;


135 


136 
val fp_abs = absfree(X', iT,


137 
mk_Collect(z', dom_sum,

7695

138 
fold_bal FOLogic.mk_disj part_intrs));

6051

139 


140 
val fp_rhs = Fp.oper $ dom_sum $ fp_abs


141 


142 
val dummy = seq (fn rec_hd => deny (rec_hd occs fp_rhs)


143 
"Illegal occurrence of recursion operator")


144 
rec_hds;


145 


146 
(*** Make the new theory ***)


147 


148 
(*A key definition:


149 
If no mutual recursion then it equals the one recursive set.


150 
If mutual recursion then it differs from all the recursive sets. *)


151 
val big_rec_base_name = space_implode "_" rec_base_names;


152 
val big_rec_name = Sign.intern_const sign big_rec_base_name;


153 


154 


155 
val dummy =


156 
if verbose then

6093

157 
writeln ((if #1 (dest_Const Fp.oper) = "Fixedpt.lfp" then "Inductive"

6051

158 
else "Coinductive") ^ " definition " ^ big_rec_name)


159 
else ();


160 


161 
(*Forbid the inductive definition structure from clashing with a theory


162 
name. This restriction may become obsolete as ML is deemphasized.*)


163 
val dummy = deny (big_rec_base_name mem (Sign.stamp_names_of sign))


164 
("Definition " ^ big_rec_base_name ^


165 
" would clash with the theory of the same name!");


166 


167 
(*Big_rec... is the union of the mutually recursive sets*)


168 
val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);


169 


170 
(*The individual sets must already be declared*)


171 
val axpairs = map Logic.mk_defpair


172 
((big_rec_tm, fp_rhs) ::


173 
(case parts of


174 
[_] => [] (*no mutual recursion*)


175 
 _ => rec_tms ~~ (*define the sets as Parts*)


176 
map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));


177 


178 
(*tracing: print the fixedpoint definition*)


179 
val dummy = if !Ind_Syntax.trace then


180 
seq (writeln o Sign.string_of_term sign o #2) axpairs


181 
else ()


182 


183 
(*add definitions of the inductive sets*)


184 
val thy1 = thy > Theory.add_path big_rec_base_name

8438

185 
> (#1 o PureThy.add_defs_i (map Thm.no_attributes axpairs))

6051

186 


187 


188 
(*fetch fp definitions from the theory*)


189 
val big_rec_def::part_rec_defs =


190 
map (get_def thy1)


191 
(case rec_names of [_] => rec_names


192 
 _ => big_rec_base_name::rec_names);


193 


194 


195 
val sign1 = sign_of thy1;


196 


197 
(********)


198 
val dummy = writeln " Proving monotonicity...";


199 


200 
val bnd_mono =


201 
prove_goalw_cterm []


202 
(cterm_of sign1


203 
(FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs)))


204 
(fn _ =>


205 
[rtac (Collect_subset RS bnd_monoI) 1,


206 
REPEAT (ares_tac (basic_monos @ monos) 1)]);


207 


208 
val dom_subset = standard (big_rec_def RS Fp.subs);


209 


210 
val unfold = standard ([big_rec_def, bnd_mono] MRS Fp.Tarski);


211 


212 
(********)


213 
val dummy = writeln " Proving the introduction rules...";


214 


215 
(*Mutual recursion? Helps to derive subset rules for the


216 
individual sets.*)


217 
val Part_trans =


218 
case rec_names of


219 
[_] => asm_rl


220 
 _ => standard (Part_subset RS subset_trans);


221 


222 
(*To typecheck recursive occurrences of the inductive sets, possibly


223 
enclosed in some monotonic operator M.*)


224 
val rec_typechecks =


225 
[dom_subset] RL (asm_rl :: ([Part_trans] RL monos))


226 
RL [subsetD];


227 


228 
(*Typechecking is hardest aspect of proof;


229 
disjIn selects the correct disjunct after unfolding*)


230 
fun intro_tacsf disjIn prems =


231 
[(*insert prems and underlying sets*)


232 
cut_facts_tac prems 1,


233 
DETERM (stac unfold 1),


234 
REPEAT (resolve_tac [Part_eqI,CollectI] 1),


235 
(*Now 23 subgoals: typechecking, the disjunction, perhaps equality.*)


236 
rtac disjIn 2,


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


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


239 
DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 2 APPEND assume_tac 2),


240 
(*Now solve the equations like Tcons(a,f) = Inl(?b4)*)


241 
rewrite_goals_tac con_defs,


242 
REPEAT (rtac refl 2),


243 
(*Typechecking; this can fail*)

6172

244 
if !Ind_Syntax.trace then print_tac "The typechecking subgoal:"

6051

245 
else all_tac,


246 
REPEAT (FIRSTGOAL ( dresolve_tac rec_typechecks


247 
ORELSE' eresolve_tac (asm_rl::PartE::SigmaE2::


248 
type_elims)


249 
ORELSE' hyp_subst_tac)),


250 
if !Ind_Syntax.trace then print_tac "The subgoal after monos, type_elims:"


251 
else all_tac,


252 
DEPTH_SOLVE (swap_res_tac (SigmaI::subsetI::type_intrs) 1)];


253 


254 
(*combines disjI1 and disjI2 to get the corresponding nested disjunct...*)


255 
val mk_disj_rls =


256 
let fun f rl = rl RS disjI1


257 
and g rl = rl RS disjI2


258 
in accesses_bal(f, g, asm_rl) end;


259 


260 
fun prove_intr (ct, tacsf) = prove_goalw_cterm part_rec_defs ct tacsf;


261 


262 
val intrs = ListPair.map prove_intr


263 
(map (cterm_of sign1) intr_tms,


264 
map intro_tacsf (mk_disj_rls(length intr_tms)))


265 
handle SIMPLIFIER (msg,thm) => (print_thm thm; error msg);


266 


267 
(********)


268 
val dummy = writeln " Proving the elimination rule...";


269 


270 
(*Breaks down logical connectives in the monotonic function*)


271 
val basic_elim_tac =


272 
REPEAT (SOMEGOAL (eresolve_tac (Ind_Syntax.elim_rls @ Su.free_SEs)


273 
ORELSE' bound_hyp_subst_tac))


274 
THEN prune_params_tac


275 
(*Mutual recursion: collapse references to Part(D,h)*)


276 
THEN fold_tac part_rec_defs;


277 


278 
(*Elimination*)


279 
val elim = rule_by_tactic basic_elim_tac


280 
(unfold RS Ind_Syntax.equals_CollectD)


281 


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


283 
the given defs. Cannot simply use the local con_defs because


284 
con_defs=[] for inference systems.


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

6141

286 
fun mk_cases s =


287 
rule_by_tactic (basic_elim_tac THEN


288 
ALLGOALS Asm_full_simp_tac THEN


289 
basic_elim_tac)

6051

290 
(assume_read (theory_of_thm elim) s


291 
(*Don't use thy1: it will be stale*)


292 
RS elim)


293 
> standard;


294 


295 


296 
fun induction_rules raw_induct thy =


297 
let


298 
val dummy = writeln " Proving the induction rule...";


299 


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


301 


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


303 


304 
(*Used to make induction rules;


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


306 
prem is a premise of an intr rule*)


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


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


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


310 
Some pred => prem :: FOLogic.mk_Trueprop (pred $ t) :: iprems


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


312 
let fun mk_sb (rec_tm,pred) =


313 
(rec_tm, Ind_Syntax.Collect_const$rec_tm$pred)


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


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


316 


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


318 
fun induct_prem ind_alist intr =


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


320 
val iprems = foldr (add_induct_prem ind_alist)


321 
(Logic.strip_imp_prems intr,[])


322 
val (t,X) = Ind_Syntax.rule_concl intr


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


324 
val concl = FOLogic.mk_Trueprop (pred $ t)


325 
in list_all_free (quantfrees, Logic.list_implies (iprems,concl)) end


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


327 


328 
(*Minimizes backtracking by delivering the correct premise to each goal.


329 
Intro rules with extra Vars in premises still cause some backtracking *)


330 
fun ind_tac [] 0 = all_tac


331 
 ind_tac(prem::prems) i =


332 
DEPTH_SOLVE_1 (ares_tac [prem, refl] i) THEN


333 
ind_tac prems (i1);


334 


335 
val pred = Free(pred_name, Ind_Syntax.iT > FOLogic.oT);


336 


337 
val ind_prems = map (induct_prem (map (rpair pred) rec_tms))


338 
intr_tms;


339 


340 
val dummy = if !Ind_Syntax.trace then


341 
(writeln "ind_prems = ";


342 
seq (writeln o Sign.string_of_term sign1) ind_prems;


343 
writeln "raw_induct = "; print_thm raw_induct)


344 
else ();


345 


346 


347 
(*We use a MINIMAL simpset. Even FOL_ss contains too many simpules.


348 
If the premises get simplified, then the proofs could fail.*)


349 
val min_ss = empty_ss


350 
setmksimps (map mk_eq o ZF_atomize o gen_all)

7570

351 
setSolver (mk_solver "minimal"


352 
(fn prems => resolve_tac (triv_rls@prems)

6051

353 
ORELSE' assume_tac

7570

354 
ORELSE' etac FalseE));

6051

355 


356 
val quant_induct =


357 
prove_goalw_cterm part_rec_defs


358 
(cterm_of sign1


359 
(Logic.list_implies


360 
(ind_prems,


361 
FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp(big_rec_tm,pred)))))


362 
(fn prems =>


363 
[rtac (impI RS allI) 1,


364 
DETERM (etac raw_induct 1),


365 
(*Push Part inside Collect*)


366 
full_simp_tac (min_ss addsimps [Part_Collect]) 1,


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


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


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


370 
some premise involves disjunction.*)


371 
REPEAT (FIRSTGOAL (eresolve_tac [CollectE, exE, conjE]


372 
ORELSE' hyp_subst_tac)),


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


374 


375 
val dummy = if !Ind_Syntax.trace then


376 
(writeln "quant_induct = "; print_thm quant_induct)


377 
else ();


378 


379 


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


381 


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


383 


384 
(*The components of the element type, several if it is a product*)


385 
val elem_type = CP.pseudo_type dom_sum;


386 
val elem_factors = CP.factors elem_type;


387 
val elem_frees = mk_frees "za" elem_factors;


388 
val elem_tuple = CP.mk_tuple Pr.pair elem_type elem_frees;


389 


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


391 
and a conclusion for the simultaneous induction rule.


392 
NOTE. This will not work for mutually recursive predicates. Previously


393 
a summand 'domt' was also an argument, but this required the domain of


394 
mutual recursion to invariably be a disjoint sum.*)


395 
fun mk_predpair rec_tm =


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


397 
val pfree = Free(pred_name ^ "_" ^ Sign.base_name rec_name,


398 
elem_factors > FOLogic.oT)


399 
val qconcl =


400 
foldr FOLogic.mk_all


401 
(elem_frees,


402 
FOLogic.imp $


403 
(Ind_Syntax.mem_const $ elem_tuple $ rec_tm)


404 
$ (list_comb (pfree, elem_frees)))


405 
in (CP.ap_split elem_type FOLogic.oT pfree,


406 
qconcl)


407 
end;


408 


409 
val (preds,qconcls) = split_list (map mk_predpair rec_tms);


410 


411 
(*Used to form simultaneous induction lemma*)


412 
fun mk_rec_imp (rec_tm,pred) =


413 
FOLogic.imp $ (Ind_Syntax.mem_const $ Bound 0 $ rec_tm) $


414 
(pred $ Bound 0);


415 


416 
(*To instantiate the main induction rule*)


417 
val induct_concl =


418 
FOLogic.mk_Trueprop


419 
(Ind_Syntax.mk_all_imp


420 
(big_rec_tm,


421 
Abs("z", Ind_Syntax.iT,

7695

422 
fold_bal FOLogic.mk_conj

6051

423 
(ListPair.map mk_rec_imp (rec_tms, preds)))))


424 
and mutual_induct_concl =

7695

425 
FOLogic.mk_Trueprop(fold_bal FOLogic.mk_conj qconcls);

6051

426 


427 
val dummy = if !Ind_Syntax.trace then


428 
(writeln ("induct_concl = " ^


429 
Sign.string_of_term sign1 induct_concl);


430 
writeln ("mutual_induct_concl = " ^


431 
Sign.string_of_term sign1 mutual_induct_concl))


432 
else ();


433 


434 


435 
val lemma_tac = FIRST' [eresolve_tac [asm_rl, conjE, PartE, mp],


436 
resolve_tac [allI, impI, conjI, Part_eqI],


437 
dresolve_tac [spec, mp, Pr.fsplitD]];


438 


439 
val need_mutual = length rec_names > 1;


440 


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


442 
if need_mutual then


443 
(writeln " Proving the mutual induction rule...";


444 
prove_goalw_cterm part_rec_defs


445 
(cterm_of sign1 (Logic.mk_implies (induct_concl,


446 
mutual_induct_concl)))


447 
(fn prems =>


448 
[cut_facts_tac prems 1,


449 
REPEAT (rewrite_goals_tac [Pr.split_eq] THEN


450 
lemma_tac 1)]))


451 
else (writeln " [ No mutual induction rule needed ]";


452 
TrueI);


453 


454 
val dummy = if !Ind_Syntax.trace then


455 
(writeln "lemma = "; print_thm lemma)


456 
else ();


457 


458 


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


460 


461 
(*Simplification largely reduces the mutual induction rule to the


462 
standard rule*)


463 
val mut_ss =


464 
min_ss addsimps [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff];


465 


466 
val all_defs = con_defs @ part_rec_defs;


467 


468 
(*Removes Collects caused by Moperators in the intro rules. It is very


469 
hard to simplify


470 
list({v: tf. (v : t > P_t(v)) & (v : f > P_f(v))})


471 
where t==Part(tf,Inl) and f==Part(tf,Inr) to list({v: tf. P_t(v)}).


472 
Instead the following rules extract the relevant conjunct.


473 
*)


474 
val cmonos = [subset_refl RS Collect_mono] RL monos


475 
RLN (2,[rev_subsetD]);


476 


477 
(*Minimizes backtracking by delivering the correct premise to each goal*)


478 
fun mutual_ind_tac [] 0 = all_tac


479 
 mutual_ind_tac(prem::prems) i =


480 
DETERM


481 
(SELECT_GOAL


482 
(


483 
(*Simplify the assumptions and goal by unfolding Part and


484 
using freeness of the Sum constructors; proves all but one


485 
conjunct by contradiction*)


486 
rewrite_goals_tac all_defs THEN


487 
simp_tac (mut_ss addsimps [Part_iff]) 1 THEN


488 
IF_UNSOLVED (*simp_tac may have finished it off!*)


489 
((*simplify assumptions*)


490 
(*some risk of excessive simplification here  might have


491 
to identify the bare minimum set of rewrites*)


492 
full_simp_tac


493 
(mut_ss addsimps conj_simps @ imp_simps @ quant_simps) 1


494 
THEN


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


496 
REPEAT (rtac impI 1) THEN


497 
rtac (rewrite_rule all_defs prem) 1 THEN


498 
(*prem must not be REPEATed below: could loop!*)


499 
DEPTH_SOLVE (FIRSTGOAL (ares_tac [impI] ORELSE'


500 
eresolve_tac (conjE::mp::cmonos))))


501 
) i)


502 
THEN mutual_ind_tac prems (i1);


503 


504 
val mutual_induct_fsplit =


505 
if need_mutual then


506 
prove_goalw_cterm []


507 
(cterm_of sign1


508 
(Logic.list_implies


509 
(map (induct_prem (rec_tms~~preds)) intr_tms,


510 
mutual_induct_concl)))


511 
(fn prems =>


512 
[rtac (quant_induct RS lemma) 1,


513 
mutual_ind_tac (rev prems) (length prems)])


514 
else TrueI;


515 


516 
(** Uncurrying the predicate in the ordinary induction rule **)


517 


518 
(*instantiate the variable to a tuple, if it is nontrivial, in order to


519 
allow the predicate to be "opened up".


520 
The name "x.1" comes from the "RS spec" !*)


521 
val inst =


522 
case elem_frees of [_] => I


523 
 _ => instantiate ([], [(cterm_of sign1 (Var(("x",1), Ind_Syntax.iT)),


524 
cterm_of sign1 elem_tuple)]);


525 


526 
(*strip quantifier and the implication*)


527 
val induct0 = inst (quant_induct RS spec RSN (2,rev_mp));


528 


529 
val Const ("Trueprop", _) $ (pred_var $ _) = concl_of induct0


530 


531 
val induct = CP.split_rule_var(pred_var, elem_type>FOLogic.oT, induct0)


532 
> standard


533 
and mutual_induct = CP.remove_split mutual_induct_fsplit

8438

534 


535 
val (thy', [induct', mutual_induct']) =


536 
thy > PureThy.add_thms [(("induct", induct), []), (("mutual_induct", mutual_induct), [])];


537 
in (thy', induct', mutual_induct')

6051

538 
end; (*of induction_rules*)


539 


540 
val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct)


541 


542 
val (thy2, induct, mutual_induct) =

6093

543 
if #1 (dest_Const Fp.oper) = "Fixedpt.lfp" then induction_rules raw_induct thy1

6051

544 
else (thy1, raw_induct, TrueI)


545 
and defs = big_rec_def :: part_rec_defs


546 


547 

8438

548 
val (thy3, ([bnd_mono', dom_subset', elim'], [defs', intrs'])) =


549 
thy2


550 
> (PureThy.add_thms o map Thm.no_attributes)


551 
[("bnd_mono", bnd_mono),


552 
("dom_subset", dom_subset),


553 
("elim", elim)]


554 
>>> (PureThy.add_thmss o map Thm.no_attributes)


555 
[("defs", defs),


556 
("intrs", intrs)]


557 
>> Theory.parent_path;


558 
in


559 
(thy3,


560 
{defs = defs',


561 
bnd_mono = bnd_mono',


562 
dom_subset = dom_subset',


563 
intrs = intrs',


564 
elim = elim',


565 
mk_cases = mk_cases,


566 
induct = induct,


567 
mutual_induct = mutual_induct})


568 
end;

6051

569 


570 


571 
(*external version, accepting strings*)


572 
fun add_inductive (srec_tms, sdom_sum, sintrs, monos,


573 
con_defs, type_intrs, type_elims) thy =


574 
let val rec_tms = map (readtm (sign_of thy) Ind_Syntax.iT) srec_tms


575 
and dom_sum = readtm (sign_of thy) Ind_Syntax.iT sdom_sum


576 
and intr_tms = map (readtm (sign_of thy) propT) sintrs


577 
in


578 
add_inductive_i true (rec_tms, dom_sum, intr_tms,


579 
monos, con_defs, type_intrs, type_elims) thy


580 


581 
end


582 
end;
