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;