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
```     1 (*  Title: 	ZF/intr-elim.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 * user-specified 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 (non-conjunctive) side condition on the free variables
```
```    21   ti, t are any terms
```
```    22   Sj, Sk are two of the sets being defined 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		(*type-checking intro rules*)
```
```    73   val type_elims : thm list		(*type-checking 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			(*fixed-point 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     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 (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 (term_of o rd propT) sintrs;
```
```   120
```
```   121 local (*Checking the introduction rules*)
```
```   122   val intr_sets = map (#2 o rule_concl_msg sign) intr_tms;
```
```   123
```
```   124   fun intr_ok set =
```
```   125       case head_of set of Const(a,recT) => a mem rec_names | _ => false;
```
```   126
```
```   127   val dummy =  assert_all intr_ok intr_sets
```
```   128      (fn t => "Conclusion of rule does not name a recursive set: " ^
```
```   129 	      Sign.string_of_term sign t);
```
```   130 in
```
```   131 val (Const(_,recT),rec_params) = strip_comb (hd intr_sets)
```
```   132 end;
```
```   133
```
```   134 val rec_hds = map (fn a=> Const(a,recT)) rec_names;
```
```   135 val rec_tms = map (fn rec_hd=> list_comb(rec_hd,rec_params)) rec_hds;
```
```   136
```
```   137 val dummy = assert_all is_Free rec_params
```
```   138     (fn t => "Param in recursion term not a free variable: " ^
```
```   139              Sign.string_of_term sign t);
```
```   140
```
```   141 (*** Construct the lfp definition ***)
```
```   142
```
```   143 val mk_variant = variant (foldr add_term_names (intr_tms,[]));
```
```   144
```
```   145 val z' = mk_variant"z"
```
```   146 and X' = mk_variant"X"
```
```   147 and w' = mk_variant"w";
```
```   148
```
```   149 (*simple error-checking in the premises*)
```
```   150 fun chk_prem rec_hd (Const("op &",_) \$ _ \$ _) =
```
```   151 	error"Premises may not be conjuctive"
```
```   152   | chk_prem rec_hd (Const("op :",_) \$ t \$ X) =
```
```   153 	deny (rec_hd occs t) "Recursion term on left of member symbol"
```
```   154   | chk_prem rec_hd t =
```
```   155 	deny (rec_hd occs t) "Recursion term in side formula";
```
```   156
```
```   157 fun dest_tprop (Const("Trueprop",_) \$ P) = P
```
```   158   | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^
```
```   159 			  Sign.string_of_term sign Q);
```
```   160
```
```   161 (*Makes a disjunct from an introduction rule*)
```
```   162 fun lfp_part intr = (*quantify over rule's free vars except parameters*)
```
```   163   let val prems = map dest_tprop (strip_imp_prems intr)
```
```   164       val dummy = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds
```
```   165       val exfrees = term_frees intr \\ rec_params
```
```   166       val zeq = eq_const \$ (Free(z',iT)) \$ (#1 (rule_concl intr))
```
```   167   in foldr mk_exists (exfrees, fold_bal (app conj) (zeq::prems)) end;
```
```   168
```
```   169 val dom_sum = fold_bal (app Su.sum) domts;
```
```   170
```
```   171 (*The Part(A,h) terms -- compose injections to make h*)
```
```   172 fun mk_Part (Bound 0) = Free(X',iT)	(*no mutual rec, no Part needed*)
```
```   173   | mk_Part h         = Part_const \$ Free(X',iT) \$ Abs(w',iT,h);
```
```   174
```
```   175 (*Access to balanced disjoint sums via injections*)
```
```   176 val parts =
```
```   177     map mk_Part (accesses_bal (ap Su.inl, ap Su.inr, Bound 0)
```
```   178 		              (length rec_doms));
```
```   179
```
```   180 (*replace each set by the corresponding Part(A,h)*)
```
```   181 val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms;
```
```   182
```
```   183 val lfp_abs = absfree(X', iT,
```
```   184 	         mk_Collect(z', dom_sum, fold_bal (app disj) part_intrs));
```
```   185
```
```   186 val lfp_rhs = Fp.oper \$ dom_sum \$ lfp_abs
```
```   187
```
```   188 val dummy = seq (fn rec_hd => deny (rec_hd occs lfp_rhs)
```
```   189 			   "Illegal occurrence of recursion operator")
```
```   190 	 rec_hds;
```
```   191
```
```   192 (*** Make the new theory ***)
```
```   193
```
```   194 (*A key definition:
```
```   195   If no mutual recursion then it equals the one recursive set.
```
```   196   If mutual recursion then it differs from all the recursive sets. *)
```
```   197 val big_rec_name = space_implode "_" rec_names;
```
```   198
```
```   199 (*Big_rec... is the union of the mutually recursive sets*)
```
```   200 val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
```
```   201
```
```   202 (*The individual sets must already be declared*)
```
```   203 val axpairs = map (mk_defpair sign)
```
```   204       ((big_rec_tm, lfp_rhs) ::
```
```   205        (case parts of
```
```   206 	   [_] => [] 			(*no mutual recursion*)
```
```   207 	 | _ => rec_tms ~~		(*define the sets as Parts*)
```
```   208 		map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));
```
```   209
```
```   210 val thy =
```
```   211   Ind.thy
```
```   212   |> add_axioms axpairs
```
```   213   |> add_thyname (big_rec_name ^ "_Inductive");
```
```   214
```
```   215 val defs = map (get_axiom thy o #1) axpairs;
```
```   216
```
```   217 val big_rec_def::part_rec_defs = defs;
```
```   218
```
```   219 val prove = prove_term (sign_of thy);
```
```   220
```
```   221 (********)
```
```   222 val dummy = writeln "Proving monotonicity...";
```
```   223
```
```   224 val bnd_mono =
```
```   225     prove [] (mk_tprop (Fp.bnd_mono \$ dom_sum \$ lfp_abs),
```
```   226        fn _ =>
```
```   227        [rtac (Collect_subset RS bnd_monoI) 1,
```
```   228 	REPEAT (ares_tac (basic_monos @ monos) 1)]);
```
```   229
```
```   230 val dom_subset = standard (big_rec_def RS Fp.subs);
```
```   231
```
```   232 val unfold = standard (bnd_mono RS (big_rec_def RS Fp.Tarski));
```
```   233
```
```   234 (********)
```
```   235 val dummy = writeln "Proving the introduction rules...";
```
```   236
```
```   237 (*Mutual recursion: Needs subset rules for the individual sets???*)
```
```   238 val rec_typechecks = [dom_subset] RL (asm_rl::monos) RL [subsetD];
```
```   239
```
```   240 (*Type-checking is hardest aspect of proof;
```
```   241   disjIn selects the correct disjunct after unfolding*)
```
```   242 fun intro_tacsf disjIn prems =
```
```   243   [(*insert prems and underlying sets*)
```
```   244    cut_facts_tac prems 1,
```
```   245    rtac (unfold RS ssubst) 1,
```
```   246    REPEAT (resolve_tac [Part_eqI,CollectI] 1),
```
```   247    (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
```
```   248    rtac disjIn 2,
```
```   249    REPEAT (ares_tac [refl,exI,conjI] 2),
```
```   250    rewrite_goals_tac con_defs,
```
```   251    (*Now can solve the trivial equation*)
```
```   252    REPEAT (rtac refl 2),
```
```   253    REPEAT (FIRSTGOAL (eresolve_tac (asm_rl::PartE::type_elims)
```
```   254 		      ORELSE' hyp_subst_tac
```
```   255 		      ORELSE' dresolve_tac rec_typechecks)),
```
```   256    DEPTH_SOLVE (swap_res_tac type_intrs 1)];
```
```   257
```
```   258 (*combines disjI1 and disjI2 to access the corresponding nested disjunct...*)
```
```   259 val mk_disj_rls =
```
```   260     let fun f rl = rl RS disjI1
```
```   261         and g rl = rl RS disjI2
```
```   262     in  accesses_bal(f, g, asm_rl)  end;
```
```   263
```
```   264 val intrs = map (prove part_rec_defs)
```
```   265 	       (intr_tms ~~ map intro_tacsf (mk_disj_rls(length intr_tms)));
```
```   266
```
```   267 (********)
```
```   268 val dummy = writeln "Proving the elimination rule...";
```
```   269
```
```   270 (*Includes rules for succ and Pair since they are common constructions*)
```
```   271 val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0,
```
```   272 		Pair_neq_0, sym RS Pair_neq_0, make_elim succ_inject,
```
```   273 		refl_thin, conjE, exE, disjE];
```
```   274
```
```   275 val sumprod_free_SEs =
```
```   276     map (gen_make_elim [conjE,FalseE])
```
```   277         ([Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff]
```
```   278 	 RL [iffD1]);
```
```   279
```
```   280 (*Breaks down logical connectives in the monotonic function*)
```
```   281 val basic_elim_tac =
```
```   282     REPEAT (SOMEGOAL (eresolve_tac (elim_rls@sumprod_free_SEs)
```
```   283               ORELSE' bound_hyp_subst_tac))
```
```   284     THEN prune_params_tac;
```
```   285
```
```   286 val elim = rule_by_tactic basic_elim_tac (unfold RS equals_CollectD);
```
```   287
```
```   288 (*Applies freeness of the given constructors, which *must* be unfolded by
```
```   289   the given defs.  Cannot simply use the local con_defs because con_defs=[]
```
```   290   for inference systems. *)
```
```   291 fun con_elim_tac defs =
```
```   292     rewrite_goals_tac defs THEN basic_elim_tac THEN fold_tac defs;
```
```   293
```
```   294 (*String s should have the form t:Si where Si is an inductive set*)
```
```   295 fun mk_cases defs s =
```
```   296     rule_by_tactic (con_elim_tac defs)
```
```   297       (assume_read thy s  RS  elim);
```
```   298
```
```   299 val defs = big_rec_def::part_rec_defs;
```
```   300
```
```   301 val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct);
```
```   302
```
```   303 end;
```