0

1 
(* Title: ZF/intrelim.ML


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1993 University of Cambridge


5 


6 
Introduction/elimination rule module  for Inductive/Coinductive Definitions


7 


8 
Features:


9 
* least or greatest fixedpoints


10 
* userspecified product and sum constructions


11 
* mutually recursive definitions


12 
* definitions involving arbitrary monotone operators


13 
* automatically proves introduction and elimination rules


14 


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


16 


17 
Introduction rules have the form


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


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


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


21 
ti, t are any terms


22 
Sj, Sk are two of the sets being defiend in mutual recursion


23 


24 
Sums are used only for mutual recursion;


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


26 
*)


27 


28 
signature FP = (** Description of a fixed point operator **)


29 
sig


30 
val oper : term (*fixed point operator*)


31 
val bnd_mono : term (*monotonicity predicate*)


32 
val bnd_monoI : thm (*intro rule for bnd_mono*)


33 
val subs : thm (*subset theorem for fp*)


34 
val Tarski : thm (*Tarski's fixed point theorem*)


35 
val induct : thm (*induction/coinduction rule*)


36 
end;


37 


38 
signature PR = (** Description of a Cartesian product **)


39 
sig


40 
val sigma : term (*Cartesian product operator*)


41 
val pair : term (*pairing operator*)


42 
val split_const : term (*splitting operator*)


43 
val fsplit_const : term (*splitting operator for formulae*)


44 
val pair_iff : thm (*injectivity of pairing, using <>*)


45 
val split_eq : thm (*equality rule for split*)


46 
val fsplitI : thm (*intro rule for fsplit*)


47 
val fsplitD : thm (*destruct rule for fsplit*)


48 
val fsplitE : thm (*elim rule for fsplit*)


49 
end;


50 


51 
signature SU = (** Description of a disjoint sum **)


52 
sig


53 
val sum : term (*disjoint sum operator*)


54 
val inl : term (*left injection*)


55 
val inr : term (*right injection*)


56 
val elim : term (*case operator*)


57 
val case_inl : thm (*inl equality rule for case*)


58 
val case_inr : thm (*inr equality rule for case*)


59 
val inl_iff : thm (*injectivity of inl, using <>*)


60 
val inr_iff : thm (*injectivity of inr, using <>*)


61 
val distinct : thm (*distinctness of inl, inr using <>*)


62 
val distinct' : thm (*distinctness of inr, inl using <>*)


63 
end;


64 


65 
signature INDUCTIVE = (** Description of a (co)inductive defn **)


66 
sig


67 
val thy : theory (*parent theory*)


68 
val rec_doms : (string*string) list (*recursion ops and their domains*)


69 
val sintrs : string list (*desired introduction rules*)


70 
val monos : thm list (*monotonicity of each M operator*)


71 
val con_defs : thm list (*definitions of the constructors*)


72 
val type_intrs : thm list (*typechecking intro rules*)


73 
val type_elims : thm list (*typechecking elim rules*)


74 
end;


75 


76 
signature INTR_ELIM =


77 
sig


78 
val thy : theory (*new theory*)


79 
val defs : thm list (*definitions made in thy*)


80 
val bnd_mono : thm (*monotonicity for the lfp definition*)


81 
val unfold : thm (*fixedpoint equation*)


82 
val dom_subset : thm (*inclusion of recursive set in dom*)


83 
val intrs : thm list (*introduction rules*)


84 
val elim : thm (*case analysis theorem*)


85 
val raw_induct : thm (*raw induction rule from Fp.induct*)


86 
val mk_cases : thm list > string > thm (*generates case theorems*)


87 
(*internal items...*)


88 
val big_rec_tm : term (*the lhs of the fixedpoint defn*)


89 
val rec_tms : term list (*the mutually recursive sets*)


90 
val domts : term list (*domains of the recursive sets*)


91 
val intr_tms : term list (*terms for the introduction rules*)


92 
val rec_params : term list (*parameters of the recursion*)


93 
val sumprod_free_SEs : thm list (*destruct rules for Su and Pr*)


94 
end;


95 


96 


97 
functor Intr_elim_Fun (structure Ind: INDUCTIVE and


98 
Fp: FP and Pr : PR and Su : SU) : INTR_ELIM =


99 
struct


100 
open Logic Ind;


101 


102 
(*** Extract basic information from arguments ***)


103 


104 
val sign = sign_of Ind.thy;


105 


106 
fun rd T a =


107 
Sign.read_cterm sign (a,T)


108 
handle ERROR => error ("The error above occurred for " ^ a);


109 


110 
val rec_names = map #1 rec_doms


111 
and domts = map (Sign.term_of o rd iT o #2) rec_doms;


112 


113 
val dummy = assert_all Syntax.is_identifier rec_names


114 
(fn a => "Name of recursive set not an identifier: " ^ a);


115 


116 
val dummy = assert_all (is_some o lookup_const sign) rec_names


117 
(fn a => "Name of recursive set not declared as constant: " ^ a);


118 


119 
val intr_tms = map (Sign.term_of o rd propT) sintrs;


120 
val (Const(_,recT),rec_params) = strip_comb (#2 (rule_concl(hd intr_tms)))


121 
val rec_hds = map (fn a=> Const(a,recT)) rec_names;


122 
val rec_tms = map (fn rec_hd=> list_comb(rec_hd,rec_params)) rec_hds;


123 


124 
val dummy = assert_all is_Free rec_params


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


126 
Sign.string_of_term sign t);


127 


128 
(*** Construct the lfp definition ***)


129 


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


131 


132 
val z' = mk_variant"z"


133 
and X' = mk_variant"X"


134 
and w' = mk_variant"w";


135 


136 
(*simple errorchecking in the premises*)


137 
fun chk_prem rec_hd (Const("op &",_) $ _ $ _) =


138 
error"Premises may not be conjuctive"


139 
 chk_prem rec_hd (Const("op :",_) $ t $ X) =


140 
deny (rec_hd occs t) "Recursion term on left of member symbol"


141 
 chk_prem rec_hd t =


142 
deny (rec_hd occs t) "Recursion term in side formula";


143 


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


145 
fun lfp_part intr = (*quantify over rule's free vars except parameters*)


146 
let val prems = map dest_tprop (strip_imp_prems intr)


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


148 
val exfrees = term_frees intr \\ rec_params


149 
val zeq = eq_const $ (Free(z',iT)) $ (#1 (rule_concl intr))


150 
in foldr mk_exists (exfrees, fold_bal (app conj) (zeq::prems)) end;


151 


152 
val dom_sum = fold_bal (app Su.sum) domts;


153 


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


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


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


157 


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


159 
val parts =


160 
map mk_Part (accesses_bal (ap Su.inl, ap Su.inr, Bound 0)


161 
(length rec_doms));


162 


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


164 
val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms;


165 


166 
val lfp_abs = absfree(X', iT,


167 
mk_Collect(z', dom_sum, fold_bal (app disj) part_intrs));


168 


169 
val lfp_rhs = Fp.oper $ dom_sum $ lfp_abs


170 


171 
val dummy = seq (fn rec_hd => deny (rec_hd occs lfp_rhs)


172 
"Illegal occurrence of recursion operator")


173 
rec_hds;


174 


175 
(*** Make the new theory ***)


176 


177 
(*A key definition:


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


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


180 
val big_rec_name = space_implode "_" rec_names;


181 


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


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


184 


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


186 
val axpairs = map (mk_defpair sign)


187 
((big_rec_tm, lfp_rhs) ::


188 
(case parts of


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


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


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


192 


193 
val thy = extend_theory Ind.thy (big_rec_name ^ "_Inductive")


194 
([], [], [], [], [], None) axpairs;


195 


196 
val defs = map (get_axiom thy o #1) axpairs;


197 


198 
val big_rec_def::part_rec_defs = defs;


199 


200 
val prove = prove_term (sign_of thy);


201 


202 
(********)


203 
val dummy = writeln "Proving monotonocity...";


204 


205 
val bnd_mono =


206 
prove [] (mk_tprop (Fp.bnd_mono $ dom_sum $ lfp_abs),


207 
fn _ =>


208 
[rtac (Collect_subset RS bnd_monoI) 1,


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


210 


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


212 


213 
val unfold = standard (bnd_mono RS (big_rec_def RS Fp.Tarski));


214 


215 
(********)


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


217 


218 
(*Mutual recursion: Needs subset rules for the individual sets???*)


219 
val rec_typechecks = [dom_subset] RL (asm_rl::monos) RL [subsetD];


220 


221 
(*Typechecking is hardest aspect of proof;


222 
disjIn selects the correct disjunct after unfolding*)


223 
fun intro_tacsf disjIn prems =


224 
[(*insert prems and underlying sets*)


225 
cut_facts_tac (prems @ (prems RL [PartD1])) 1,


226 
rtac (unfold RS ssubst) 1,


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


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


229 
rtac disjIn 2,


230 
REPEAT (ares_tac [refl,exI,conjI] 2),


231 
rewrite_goals_tac con_defs,


232 
(*Now can solve the trivial equation*)


233 
REPEAT (rtac refl 2),


234 
REPEAT (FIRSTGOAL (eresolve_tac (asm_rl::type_elims)


235 
ORELSE' dresolve_tac rec_typechecks)),


236 
DEPTH_SOLVE (ares_tac type_intrs 1)];


237 


238 
(*combines disjI1 and disjI2 to access the corresponding nested disjunct...*)


239 
val mk_disj_rls =


240 
let fun f rl = rl RS disjI1


241 
and g rl = rl RS disjI2


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


243 


244 
val intrs = map (prove part_rec_defs)


245 
(intr_tms ~~ map intro_tacsf (mk_disj_rls(length intr_tms)));


246 


247 
(********)


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


249 


250 
val elim_rls = [asm_rl, FalseE, conjE, exE, disjE];


251 


252 
val sumprod_free_SEs =


253 
map (gen_make_elim [conjE,FalseE])


254 
([Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff]


255 
RL [iffD1]);


256 


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


258 
val basic_elim_tac =


259 
REPEAT (SOMEGOAL (eresolve_tac (elim_rls@sumprod_free_SEs)


260 
ORELSE' bound_hyp_subst_tac))


261 
THEN prune_params_tac;


262 


263 
val elim = rule_by_tactic basic_elim_tac (unfold RS equals_CollectD);


264 


265 
(*Applies freeness of the given constructors.


266 
NB for datatypes, defs=con_defs; for inference systems, con_defs=[]! *)


267 
fun con_elim_tac defs =


268 
rewrite_goals_tac defs THEN basic_elim_tac THEN fold_con_tac defs;


269 


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


271 
fun mk_cases defs s =


272 
rule_by_tactic (con_elim_tac defs)


273 
(assume_read thy s RS elim);


274 


275 
val defs = big_rec_def::part_rec_defs;


276 


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


278 


279 
end;
