src/ZF/intr_elim.ML
 author clasohm Fri Jul 01 11:03:42 1994 +0200 (1994-07-01 ago) changeset 444 3ca9d49fd662 parent 435 ca5356bd315a child 454 0d19ab250cc9 permissions -rw-r--r--
replaced extend_theory by new add_* functions;
changed syntax of datatype declaration
 clasohm@0 ` 1` ```(* Title: ZF/intr-elim.ML ``` clasohm@0 ` 2` ``` ID: \$Id\$ ``` clasohm@0 ` 3` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` clasohm@0 ` 4` ``` Copyright 1993 University of Cambridge ``` clasohm@0 ` 5` clasohm@0 ` 6` ```Introduction/elimination rule module -- for Inductive/Coinductive Definitions ``` clasohm@0 ` 7` clasohm@0 ` 8` ```Features: ``` clasohm@0 ` 9` ```* least or greatest fixedpoints ``` clasohm@0 ` 10` ```* user-specified product and sum constructions ``` clasohm@0 ` 11` ```* mutually recursive definitions ``` clasohm@0 ` 12` ```* definitions involving arbitrary monotone operators ``` clasohm@0 ` 13` ```* automatically proves introduction and elimination rules ``` clasohm@0 ` 14` clasohm@0 ` 15` ```The recursive sets must *already* be declared as constants in parent theory! ``` clasohm@0 ` 16` clasohm@0 ` 17` ``` Introduction rules have the form ``` clasohm@0 ` 18` ``` [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk |] ``` clasohm@0 ` 19` ``` where M is some monotone operator (usually the identity) ``` clasohm@0 ` 20` ``` P(x) is any (non-conjunctive) side condition on the free variables ``` clasohm@0 ` 21` ``` ti, t are any terms ``` lcp@25 ` 22` ``` Sj, Sk are two of the sets being defined in mutual recursion ``` clasohm@0 ` 23` clasohm@0 ` 24` ```Sums are used only for mutual recursion; ``` clasohm@0 ` 25` ```Products are used only to derive "streamlined" induction rules for relations ``` clasohm@0 ` 26` ```*) ``` clasohm@0 ` 27` clasohm@0 ` 28` ```signature FP = (** Description of a fixed point operator **) ``` clasohm@0 ` 29` ``` sig ``` clasohm@0 ` 30` ``` val oper : term (*fixed point operator*) ``` clasohm@0 ` 31` ``` val bnd_mono : term (*monotonicity predicate*) ``` clasohm@0 ` 32` ``` val bnd_monoI : thm (*intro rule for bnd_mono*) ``` clasohm@0 ` 33` ``` val subs : thm (*subset theorem for fp*) ``` clasohm@0 ` 34` ``` val Tarski : thm (*Tarski's fixed point theorem*) ``` clasohm@0 ` 35` ``` val induct : thm (*induction/coinduction rule*) ``` clasohm@0 ` 36` ``` end; ``` clasohm@0 ` 37` clasohm@0 ` 38` ```signature PR = (** Description of a Cartesian product **) ``` clasohm@0 ` 39` ``` sig ``` clasohm@0 ` 40` ``` val sigma : term (*Cartesian product operator*) ``` clasohm@0 ` 41` ``` val pair : term (*pairing operator*) ``` clasohm@0 ` 42` ``` val split_const : term (*splitting operator*) ``` clasohm@0 ` 43` ``` val fsplit_const : term (*splitting operator for formulae*) ``` clasohm@0 ` 44` ``` val pair_iff : thm (*injectivity of pairing, using <->*) ``` clasohm@0 ` 45` ``` val split_eq : thm (*equality rule for split*) ``` clasohm@0 ` 46` ``` val fsplitI : thm (*intro rule for fsplit*) ``` clasohm@0 ` 47` ``` val fsplitD : thm (*destruct rule for fsplit*) ``` clasohm@0 ` 48` ``` val fsplitE : thm (*elim rule for fsplit*) ``` clasohm@0 ` 49` ``` end; ``` clasohm@0 ` 50` clasohm@0 ` 51` ```signature SU = (** Description of a disjoint sum **) ``` clasohm@0 ` 52` ``` sig ``` clasohm@0 ` 53` ``` val sum : term (*disjoint sum operator*) ``` clasohm@0 ` 54` ``` val inl : term (*left injection*) ``` clasohm@0 ` 55` ``` val inr : term (*right injection*) ``` clasohm@0 ` 56` ``` val elim : term (*case operator*) ``` clasohm@0 ` 57` ``` val case_inl : thm (*inl equality rule for case*) ``` clasohm@0 ` 58` ``` val case_inr : thm (*inr equality rule for case*) ``` clasohm@0 ` 59` ``` val inl_iff : thm (*injectivity of inl, using <->*) ``` clasohm@0 ` 60` ``` val inr_iff : thm (*injectivity of inr, using <->*) ``` clasohm@0 ` 61` ``` val distinct : thm (*distinctness of inl, inr using <->*) ``` clasohm@0 ` 62` ``` val distinct' : thm (*distinctness of inr, inl using <->*) ``` clasohm@0 ` 63` ``` end; ``` clasohm@0 ` 64` clasohm@0 ` 65` ```signature INDUCTIVE = (** Description of a (co)inductive defn **) ``` clasohm@0 ` 66` ``` sig ``` clasohm@0 ` 67` ``` val thy : theory (*parent theory*) ``` clasohm@0 ` 68` ``` val rec_doms : (string*string) list (*recursion ops and their domains*) ``` clasohm@0 ` 69` ``` val sintrs : string list (*desired introduction rules*) ``` clasohm@0 ` 70` ``` val monos : thm list (*monotonicity of each M operator*) ``` clasohm@0 ` 71` ``` val con_defs : thm list (*definitions of the constructors*) ``` clasohm@0 ` 72` ``` val type_intrs : thm list (*type-checking intro rules*) ``` clasohm@0 ` 73` ``` val type_elims : thm list (*type-checking elim rules*) ``` clasohm@0 ` 74` ``` end; ``` clasohm@0 ` 75` clasohm@0 ` 76` ```signature INTR_ELIM = ``` clasohm@0 ` 77` ``` sig ``` clasohm@0 ` 78` ``` val thy : theory (*new theory*) ``` clasohm@0 ` 79` ``` val defs : thm list (*definitions made in thy*) ``` clasohm@0 ` 80` ``` val bnd_mono : thm (*monotonicity for the lfp definition*) ``` clasohm@0 ` 81` ``` val unfold : thm (*fixed-point equation*) ``` clasohm@0 ` 82` ``` val dom_subset : thm (*inclusion of recursive set in dom*) ``` clasohm@0 ` 83` ``` val intrs : thm list (*introduction rules*) ``` clasohm@0 ` 84` ``` val elim : thm (*case analysis theorem*) ``` clasohm@0 ` 85` ``` val raw_induct : thm (*raw induction rule from Fp.induct*) ``` clasohm@0 ` 86` ``` val mk_cases : thm list -> string -> thm (*generates case theorems*) ``` clasohm@0 ` 87` ``` (*internal items...*) ``` clasohm@0 ` 88` ``` val big_rec_tm : term (*the lhs of the fixedpoint defn*) ``` clasohm@0 ` 89` ``` val rec_tms : term list (*the mutually recursive sets*) ``` clasohm@0 ` 90` ``` val domts : term list (*domains of the recursive sets*) ``` clasohm@0 ` 91` ``` val intr_tms : term list (*terms for the introduction rules*) ``` clasohm@0 ` 92` ``` val rec_params : term list (*parameters of the recursion*) ``` clasohm@0 ` 93` ``` val sumprod_free_SEs : thm list (*destruct rules for Su and Pr*) ``` clasohm@0 ` 94` ``` end; ``` clasohm@0 ` 95` clasohm@0 ` 96` clasohm@0 ` 97` ```functor Intr_elim_Fun (structure Ind: INDUCTIVE and ``` clasohm@0 ` 98` ``` Fp: FP and Pr : PR and Su : SU) : INTR_ELIM = ``` clasohm@0 ` 99` ```struct ``` clasohm@0 ` 100` ```open Logic Ind; ``` clasohm@0 ` 101` clasohm@0 ` 102` ```(*** Extract basic information from arguments ***) ``` clasohm@0 ` 103` clasohm@0 ` 104` ```val sign = sign_of Ind.thy; ``` clasohm@0 ` 105` clasohm@0 ` 106` ```fun rd T a = ``` lcp@231 ` 107` ``` read_cterm sign (a,T) ``` clasohm@0 ` 108` ``` handle ERROR => error ("The error above occurred for " ^ a); ``` clasohm@0 ` 109` clasohm@0 ` 110` ```val rec_names = map #1 rec_doms ``` lcp@231 ` 111` ```and domts = map (term_of o rd iT o #2) rec_doms; ``` clasohm@0 ` 112` clasohm@0 ` 113` ```val dummy = assert_all Syntax.is_identifier rec_names ``` clasohm@0 ` 114` ``` (fn a => "Name of recursive set not an identifier: " ^ a); ``` clasohm@0 ` 115` clasohm@0 ` 116` ```val dummy = assert_all (is_some o lookup_const sign) rec_names ``` clasohm@0 ` 117` ``` (fn a => "Name of recursive set not declared as constant: " ^ a); ``` clasohm@0 ` 118` lcp@231 ` 119` ```val intr_tms = map (term_of o rd propT) sintrs; ``` lcp@14 ` 120` lcp@14 ` 121` ```local (*Checking the introduction rules*) ``` lcp@435 ` 122` ``` val intr_sets = map (#2 o rule_concl_msg sign) intr_tms; ``` lcp@14 ` 123` lcp@14 ` 124` ``` fun intr_ok set = ``` lcp@14 ` 125` ``` case head_of set of Const(a,recT) => a mem rec_names | _ => false; ``` lcp@14 ` 126` lcp@14 ` 127` ``` val dummy = assert_all intr_ok intr_sets ``` lcp@14 ` 128` ``` (fn t => "Conclusion of rule does not name a recursive set: " ^ ``` lcp@14 ` 129` ``` Sign.string_of_term sign t); ``` lcp@14 ` 130` ```in ``` lcp@14 ` 131` ```val (Const(_,recT),rec_params) = strip_comb (hd intr_sets) ``` lcp@14 ` 132` ```end; ``` lcp@14 ` 133` clasohm@0 ` 134` ```val rec_hds = map (fn a=> Const(a,recT)) rec_names; ``` clasohm@0 ` 135` ```val rec_tms = map (fn rec_hd=> list_comb(rec_hd,rec_params)) rec_hds; ``` clasohm@0 ` 136` clasohm@0 ` 137` ```val dummy = assert_all is_Free rec_params ``` clasohm@0 ` 138` ``` (fn t => "Param in recursion term not a free variable: " ^ ``` clasohm@0 ` 139` ``` Sign.string_of_term sign t); ``` clasohm@0 ` 140` clasohm@0 ` 141` ```(*** Construct the lfp definition ***) ``` clasohm@0 ` 142` clasohm@0 ` 143` ```val mk_variant = variant (foldr add_term_names (intr_tms,[])); ``` clasohm@0 ` 144` clasohm@0 ` 145` ```val z' = mk_variant"z" ``` clasohm@0 ` 146` ```and X' = mk_variant"X" ``` clasohm@0 ` 147` ```and w' = mk_variant"w"; ``` clasohm@0 ` 148` clasohm@0 ` 149` ```(*simple error-checking in the premises*) ``` clasohm@0 ` 150` ```fun chk_prem rec_hd (Const("op &",_) \$ _ \$ _) = ``` clasohm@0 ` 151` ``` error"Premises may not be conjuctive" ``` clasohm@0 ` 152` ``` | chk_prem rec_hd (Const("op :",_) \$ t \$ X) = ``` clasohm@0 ` 153` ``` deny (rec_hd occs t) "Recursion term on left of member symbol" ``` clasohm@0 ` 154` ``` | chk_prem rec_hd t = ``` clasohm@0 ` 155` ``` deny (rec_hd occs t) "Recursion term in side formula"; ``` clasohm@0 ` 156` lcp@435 ` 157` ```fun dest_tprop (Const("Trueprop",_) \$ P) = P ``` lcp@435 ` 158` ``` | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^ ``` lcp@435 ` 159` ``` Sign.string_of_term sign Q); ``` lcp@435 ` 160` clasohm@0 ` 161` ```(*Makes a disjunct from an introduction rule*) ``` clasohm@0 ` 162` ```fun lfp_part intr = (*quantify over rule's free vars except parameters*) ``` clasohm@0 ` 163` ``` let val prems = map dest_tprop (strip_imp_prems intr) ``` clasohm@0 ` 164` ``` val dummy = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds ``` clasohm@0 ` 165` ``` val exfrees = term_frees intr \\ rec_params ``` clasohm@0 ` 166` ``` val zeq = eq_const \$ (Free(z',iT)) \$ (#1 (rule_concl intr)) ``` clasohm@0 ` 167` ``` in foldr mk_exists (exfrees, fold_bal (app conj) (zeq::prems)) end; ``` clasohm@0 ` 168` clasohm@0 ` 169` ```val dom_sum = fold_bal (app Su.sum) domts; ``` clasohm@0 ` 170` clasohm@0 ` 171` ```(*The Part(A,h) terms -- compose injections to make h*) ``` clasohm@0 ` 172` ```fun mk_Part (Bound 0) = Free(X',iT) (*no mutual rec, no Part needed*) ``` clasohm@0 ` 173` ``` | mk_Part h = Part_const \$ Free(X',iT) \$ Abs(w',iT,h); ``` clasohm@0 ` 174` clasohm@0 ` 175` ```(*Access to balanced disjoint sums via injections*) ``` clasohm@0 ` 176` ```val parts = ``` clasohm@0 ` 177` ``` map mk_Part (accesses_bal (ap Su.inl, ap Su.inr, Bound 0) ``` clasohm@0 ` 178` ``` (length rec_doms)); ``` clasohm@0 ` 179` clasohm@0 ` 180` ```(*replace each set by the corresponding Part(A,h)*) ``` clasohm@0 ` 181` ```val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms; ``` clasohm@0 ` 182` clasohm@0 ` 183` ```val lfp_abs = absfree(X', iT, ``` clasohm@0 ` 184` ``` mk_Collect(z', dom_sum, fold_bal (app disj) part_intrs)); ``` clasohm@0 ` 185` clasohm@0 ` 186` ```val lfp_rhs = Fp.oper \$ dom_sum \$ lfp_abs ``` clasohm@0 ` 187` clasohm@0 ` 188` ```val dummy = seq (fn rec_hd => deny (rec_hd occs lfp_rhs) ``` clasohm@0 ` 189` ``` "Illegal occurrence of recursion operator") ``` clasohm@0 ` 190` ``` rec_hds; ``` clasohm@0 ` 191` clasohm@0 ` 192` ```(*** Make the new theory ***) ``` clasohm@0 ` 193` clasohm@0 ` 194` ```(*A key definition: ``` clasohm@0 ` 195` ``` If no mutual recursion then it equals the one recursive set. ``` clasohm@0 ` 196` ``` If mutual recursion then it differs from all the recursive sets. *) ``` clasohm@0 ` 197` ```val big_rec_name = space_implode "_" rec_names; ``` clasohm@0 ` 198` clasohm@0 ` 199` ```(*Big_rec... is the union of the mutually recursive sets*) ``` clasohm@0 ` 200` ```val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params); ``` clasohm@0 ` 201` clasohm@0 ` 202` ```(*The individual sets must already be declared*) ``` clasohm@0 ` 203` ```val axpairs = map (mk_defpair sign) ``` clasohm@0 ` 204` ``` ((big_rec_tm, lfp_rhs) :: ``` clasohm@0 ` 205` ``` (case parts of ``` clasohm@0 ` 206` ``` [_] => [] (*no mutual recursion*) ``` clasohm@0 ` 207` ``` | _ => rec_tms ~~ (*define the sets as Parts*) ``` clasohm@0 ` 208` ``` map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts)); ``` clasohm@0 ` 209` clasohm@444 ` 210` ```val thy = ``` clasohm@444 ` 211` ``` Ind.thy ``` clasohm@444 ` 212` ``` |> add_axioms axpairs ``` clasohm@444 ` 213` ``` |> add_thyname (big_rec_name ^ "_Inductive"); ``` clasohm@0 ` 214` clasohm@0 ` 215` ```val defs = map (get_axiom thy o #1) axpairs; ``` clasohm@0 ` 216` clasohm@0 ` 217` ```val big_rec_def::part_rec_defs = defs; ``` clasohm@0 ` 218` clasohm@0 ` 219` ```val prove = prove_term (sign_of thy); ``` clasohm@0 ` 220` clasohm@0 ` 221` ```(********) ``` lcp@435 ` 222` ```val dummy = writeln "Proving monotonicity..."; ``` clasohm@0 ` 223` clasohm@0 ` 224` ```val bnd_mono = ``` clasohm@0 ` 225` ``` prove [] (mk_tprop (Fp.bnd_mono \$ dom_sum \$ lfp_abs), ``` clasohm@0 ` 226` ``` fn _ => ``` clasohm@0 ` 227` ``` [rtac (Collect_subset RS bnd_monoI) 1, ``` clasohm@0 ` 228` ``` REPEAT (ares_tac (basic_monos @ monos) 1)]); ``` clasohm@0 ` 229` clasohm@0 ` 230` ```val dom_subset = standard (big_rec_def RS Fp.subs); ``` clasohm@0 ` 231` clasohm@0 ` 232` ```val unfold = standard (bnd_mono RS (big_rec_def RS Fp.Tarski)); ``` clasohm@0 ` 233` clasohm@0 ` 234` ```(********) ``` clasohm@0 ` 235` ```val dummy = writeln "Proving the introduction rules..."; ``` clasohm@0 ` 236` clasohm@0 ` 237` ```(*Mutual recursion: Needs subset rules for the individual sets???*) ``` clasohm@0 ` 238` ```val rec_typechecks = [dom_subset] RL (asm_rl::monos) RL [subsetD]; ``` clasohm@0 ` 239` clasohm@0 ` 240` ```(*Type-checking is hardest aspect of proof; ``` clasohm@0 ` 241` ``` disjIn selects the correct disjunct after unfolding*) ``` clasohm@0 ` 242` ```fun intro_tacsf disjIn prems = ``` clasohm@0 ` 243` ``` [(*insert prems and underlying sets*) ``` lcp@55 ` 244` ``` cut_facts_tac prems 1, ``` clasohm@0 ` 245` ``` rtac (unfold RS ssubst) 1, ``` clasohm@0 ` 246` ``` REPEAT (resolve_tac [Part_eqI,CollectI] 1), ``` clasohm@0 ` 247` ``` (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*) ``` clasohm@0 ` 248` ``` rtac disjIn 2, ``` clasohm@0 ` 249` ``` REPEAT (ares_tac [refl,exI,conjI] 2), ``` clasohm@0 ` 250` ``` rewrite_goals_tac con_defs, ``` clasohm@0 ` 251` ``` (*Now can solve the trivial equation*) ``` clasohm@0 ` 252` ``` REPEAT (rtac refl 2), ``` lcp@55 ` 253` ``` REPEAT (FIRSTGOAL (eresolve_tac (asm_rl::PartE::type_elims) ``` lcp@55 ` 254` ``` ORELSE' hyp_subst_tac ``` clasohm@0 ` 255` ``` ORELSE' dresolve_tac rec_typechecks)), ``` lcp@55 ` 256` ``` DEPTH_SOLVE (swap_res_tac type_intrs 1)]; ``` clasohm@0 ` 257` clasohm@0 ` 258` ```(*combines disjI1 and disjI2 to access the corresponding nested disjunct...*) ``` clasohm@0 ` 259` ```val mk_disj_rls = ``` clasohm@0 ` 260` ``` let fun f rl = rl RS disjI1 ``` clasohm@0 ` 261` ``` and g rl = rl RS disjI2 ``` clasohm@0 ` 262` ``` in accesses_bal(f, g, asm_rl) end; ``` clasohm@0 ` 263` clasohm@0 ` 264` ```val intrs = map (prove part_rec_defs) ``` clasohm@0 ` 265` ``` (intr_tms ~~ map intro_tacsf (mk_disj_rls(length intr_tms))); ``` clasohm@0 ` 266` clasohm@0 ` 267` ```(********) ``` clasohm@0 ` 268` ```val dummy = writeln "Proving the elimination rule..."; ``` clasohm@0 ` 269` lcp@55 ` 270` ```(*Includes rules for succ and Pair since they are common constructions*) ``` lcp@55 ` 271` ```val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0, ``` lcp@70 ` 272` ``` Pair_neq_0, sym RS Pair_neq_0, make_elim succ_inject, ``` lcp@70 ` 273` ``` refl_thin, conjE, exE, disjE]; ``` clasohm@0 ` 274` clasohm@0 ` 275` ```val sumprod_free_SEs = ``` clasohm@0 ` 276` ``` map (gen_make_elim [conjE,FalseE]) ``` clasohm@0 ` 277` ``` ([Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff] ``` clasohm@0 ` 278` ``` RL [iffD1]); ``` clasohm@0 ` 279` clasohm@0 ` 280` ```(*Breaks down logical connectives in the monotonic function*) ``` clasohm@0 ` 281` ```val basic_elim_tac = ``` clasohm@0 ` 282` ``` REPEAT (SOMEGOAL (eresolve_tac (elim_rls@sumprod_free_SEs) ``` clasohm@0 ` 283` ``` ORELSE' bound_hyp_subst_tac)) ``` clasohm@0 ` 284` ``` THEN prune_params_tac; ``` clasohm@0 ` 285` clasohm@0 ` 286` ```val elim = rule_by_tactic basic_elim_tac (unfold RS equals_CollectD); ``` clasohm@0 ` 287` lcp@14 ` 288` ```(*Applies freeness of the given constructors, which *must* be unfolded by ``` lcp@14 ` 289` ``` the given defs. Cannot simply use the local con_defs because con_defs=[] ``` lcp@14 ` 290` ``` for inference systems. *) ``` clasohm@0 ` 291` ```fun con_elim_tac defs = ``` lcp@70 ` 292` ``` rewrite_goals_tac defs THEN basic_elim_tac THEN fold_tac defs; ``` clasohm@0 ` 293` clasohm@0 ` 294` ```(*String s should have the form t:Si where Si is an inductive set*) ``` clasohm@0 ` 295` ```fun mk_cases defs s = ``` clasohm@0 ` 296` ``` rule_by_tactic (con_elim_tac defs) ``` clasohm@0 ` 297` ``` (assume_read thy s RS elim); ``` clasohm@0 ` 298` clasohm@0 ` 299` ```val defs = big_rec_def::part_rec_defs; ``` clasohm@0 ` 300` clasohm@0 ` 301` ```val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct); ``` clasohm@0 ` 302` clasohm@0 ` 303` ```end; ```