src/ZF/intr-elim.ML
 author clasohm Thu, 16 Sep 1993 12:20:38 +0200 changeset 0 a5a9c433f639 child 14 1c0926788772 permissions -rw-r--r--
Initial revision
```
(*  Title: 	ZF/intr-elim.ML
ID:         \$Id\$
Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory

Introduction/elimination rule module -- for Inductive/Coinductive Definitions

Features:
* least or greatest fixedpoints
* user-specified product and sum constructions
* mutually recursive definitions
* definitions involving arbitrary monotone operators
* automatically proves introduction and elimination rules

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

Introduction rules have the form
[| ti:M(Sj), ..., P(x), ... |] ==> t: Sk |]
where M is some monotone operator (usually the identity)
P(x) is any (non-conjunctive) side condition on the free variables
ti, t are any terms
Sj, Sk are two of the sets being defiend in mutual recursion

Sums are used only for mutual recursion;
Products are used only to derive "streamlined" induction rules for relations
*)

signature FP =		(** Description of a fixed point operator **)
sig
val oper	: term			(*fixed point operator*)
val bnd_mono	: term			(*monotonicity predicate*)
val bnd_monoI	: thm			(*intro rule for bnd_mono*)
val subs	: thm			(*subset theorem for fp*)
val Tarski	: thm			(*Tarski's fixed point theorem*)
val induct	: thm			(*induction/coinduction rule*)
end;

signature PR =			(** Description of a Cartesian product **)
sig
val sigma	: term			(*Cartesian product operator*)
val pair	: term			(*pairing operator*)
val split_const  : term		(*splitting operator*)
val fsplit_const : term		(*splitting operator for formulae*)
val pair_iff	: thm			(*injectivity of pairing, using <->*)
val split_eq	: thm			(*equality rule for split*)
val fsplitI	: thm			(*intro rule for fsplit*)
val fsplitD	: thm			(*destruct rule for fsplit*)
val fsplitE	: thm			(*elim rule for fsplit*)
end;

signature SU =			(** Description of a disjoint sum **)
sig
val sum	: term			(*disjoint sum operator*)
val inl	: term			(*left injection*)
val inr	: term			(*right injection*)
val elim	: term			(*case operator*)
val case_inl	: thm			(*inl equality rule for case*)
val case_inr	: thm			(*inr equality rule for case*)
val inl_iff	: thm			(*injectivity of inl, using <->*)
val inr_iff	: thm			(*injectivity of inr, using <->*)
val distinct	: thm			(*distinctness of inl, inr using <->*)
val distinct'	: thm			(*distinctness of inr, inl using <->*)
end;

signature INDUCTIVE =		(** Description of a (co)inductive defn **)
sig
val thy        : theory		(*parent theory*)
val rec_doms   : (string*string) list	(*recursion ops and their domains*)
val sintrs     : string list		(*desired introduction rules*)
val monos      : thm list		(*monotonicity of each M operator*)
val con_defs   : thm list		(*definitions of the constructors*)
val type_intrs : thm list		(*type-checking intro rules*)
val type_elims : thm list		(*type-checking elim rules*)
end;

signature INTR_ELIM =
sig
val thy        : theory		(*new theory*)
val defs	 : thm list		(*definitions made in thy*)
val bnd_mono   : thm			(*monotonicity for the lfp definition*)
val unfold     : thm			(*fixed-point equation*)
val dom_subset : thm			(*inclusion of recursive set in dom*)
val intrs      : thm list		(*introduction rules*)
val elim       : thm			(*case analysis theorem*)
val raw_induct : thm			(*raw induction rule from Fp.induct*)
val mk_cases : thm list -> string -> thm	(*generates case theorems*)
(*internal items...*)
val big_rec_tm : term			(*the lhs of the fixedpoint defn*)
val rec_tms    : term list		(*the mutually recursive sets*)
val domts      : term list		(*domains of the recursive sets*)
val intr_tms   : term list		(*terms for the introduction rules*)
val rec_params : term list		(*parameters of the recursion*)
val sumprod_free_SEs : thm list       (*destruct rules for Su and Pr*)
end;

functor Intr_elim_Fun (structure Ind: INDUCTIVE and
Fp: FP and Pr : PR and Su : SU) : INTR_ELIM =
struct
open Logic Ind;

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

val sign = sign_of Ind.thy;

fun rd T a =
handle ERROR => error ("The error above occurred for " ^ a);

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

val dummy = assert_all Syntax.is_identifier rec_names
(fn a => "Name of recursive set not an identifier: " ^ a);

val dummy = assert_all (is_some o lookup_const sign) rec_names
(fn a => "Name of recursive set not declared as constant: " ^ a);

val intr_tms = map (Sign.term_of o rd propT) sintrs;
val (Const(_,recT),rec_params) = strip_comb (#2 (rule_concl(hd intr_tms)))
val rec_hds = map (fn a=> Const(a,recT)) rec_names;
val rec_tms = map (fn rec_hd=> list_comb(rec_hd,rec_params)) rec_hds;

val dummy = assert_all is_Free rec_params
(fn t => "Param in recursion term not a free variable: " ^
Sign.string_of_term sign t);

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

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

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

(*simple error-checking in the premises*)
fun chk_prem rec_hd (Const("op &",_) \$ _ \$ _) =
error"Premises may not be conjuctive"
| chk_prem rec_hd (Const("op :",_) \$ t \$ X) =
deny (rec_hd occs t) "Recursion term on left of member symbol"
| chk_prem rec_hd t =
deny (rec_hd occs t) "Recursion term in side formula";

(*Makes a disjunct from an introduction rule*)
fun lfp_part intr = (*quantify over rule's free vars except parameters*)
let val prems = map dest_tprop (strip_imp_prems intr)
val dummy = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds
val exfrees = term_frees intr \\ rec_params
val zeq = eq_const \$ (Free(z',iT)) \$ (#1 (rule_concl intr))
in foldr mk_exists (exfrees, fold_bal (app conj) (zeq::prems)) end;

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

(*The Part(A,h) terms -- compose injections to make h*)
fun mk_Part (Bound 0) = Free(X',iT)	(*no mutual rec, no Part needed*)
| mk_Part h         = Part_const \$ Free(X',iT) \$ Abs(w',iT,h);

val parts =
map mk_Part (accesses_bal (ap Su.inl, ap Su.inr, Bound 0)
(length rec_doms));

(*replace each set by the corresponding Part(A,h)*)
val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms;

val lfp_abs = absfree(X', iT,
mk_Collect(z', dom_sum, fold_bal (app disj) part_intrs));

val lfp_rhs = Fp.oper \$ dom_sum \$ lfp_abs

val dummy = seq (fn rec_hd => deny (rec_hd occs lfp_rhs)
"Illegal occurrence of recursion operator")
rec_hds;

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

(*A key definition:
If no mutual recursion then it equals the one recursive set.
If mutual recursion then it differs from all the recursive sets. *)
val big_rec_name = space_implode "_" rec_names;

(*Big_rec... is the union of the mutually recursive sets*)
val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);

(*The individual sets must already be declared*)
val axpairs = map (mk_defpair sign)
((big_rec_tm, lfp_rhs) ::
(case parts of
[_] => [] 			(*no mutual recursion*)
| _ => rec_tms ~~		(*define the sets as Parts*)
map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));

val thy = extend_theory Ind.thy (big_rec_name ^ "_Inductive")
([], [], [], [], [], None) axpairs;

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

val big_rec_def::part_rec_defs = defs;

val prove = prove_term (sign_of thy);

(********)
val dummy = writeln "Proving monotonocity...";

val bnd_mono =
prove [] (mk_tprop (Fp.bnd_mono \$ dom_sum \$ lfp_abs),
fn _ =>
[rtac (Collect_subset RS bnd_monoI) 1,
REPEAT (ares_tac (basic_monos @ monos) 1)]);

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

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

(********)
val dummy = writeln "Proving the introduction rules...";

(*Mutual recursion: Needs subset rules for the individual sets???*)
val rec_typechecks = [dom_subset] RL (asm_rl::monos) RL [subsetD];

(*Type-checking is hardest aspect of proof;
disjIn selects the correct disjunct after unfolding*)
fun intro_tacsf disjIn prems =
[(*insert prems and underlying sets*)
cut_facts_tac (prems @ (prems RL [PartD1])) 1,
rtac (unfold RS ssubst) 1,
REPEAT (resolve_tac [Part_eqI,CollectI] 1),
(*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
rtac disjIn 2,
REPEAT (ares_tac [refl,exI,conjI] 2),
rewrite_goals_tac con_defs,
(*Now can solve the trivial equation*)
REPEAT (rtac refl 2),
REPEAT (FIRSTGOAL (eresolve_tac (asm_rl::type_elims)
ORELSE' dresolve_tac rec_typechecks)),
DEPTH_SOLVE (ares_tac type_intrs 1)];

(*combines disjI1 and disjI2 to access the corresponding nested disjunct...*)
val mk_disj_rls =
let fun f rl = rl RS disjI1
and g rl = rl RS disjI2
in  accesses_bal(f, g, asm_rl)  end;

val intrs = map (prove part_rec_defs)
(intr_tms ~~ map intro_tacsf (mk_disj_rls(length intr_tms)));

(********)
val dummy = writeln "Proving the elimination rule...";

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

val sumprod_free_SEs =
map (gen_make_elim [conjE,FalseE])
([Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff]
RL [iffD1]);

(*Breaks down logical connectives in the monotonic function*)
val basic_elim_tac =
REPEAT (SOMEGOAL (eresolve_tac (elim_rls@sumprod_free_SEs)
ORELSE' bound_hyp_subst_tac))
THEN prune_params_tac;

val elim = rule_by_tactic basic_elim_tac (unfold RS equals_CollectD);

(*Applies freeness of the given constructors.
NB for datatypes, defs=con_defs; for inference systems, con_defs=[]! *)
fun con_elim_tac defs =
rewrite_goals_tac defs THEN basic_elim_tac THEN fold_con_tac defs;

(*String s should have the form t:Si where Si is an inductive set*)
fun mk_cases defs s =
rule_by_tactic (con_elim_tac defs)