src/ZF/intr_elim.ML
author lcp
Thu Aug 18 17:41:40 1994 +0200 (1994-08-18 ago)
changeset 543 e961b2092869
parent 516 1957113f0d7d
child 578 efc648d29dd0
permissions -rw-r--r--
ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
ZF/ind_syntax/prove_term: deleted

ZF/constructor, indrule, intr_elim: now call prove_goalw_cterm and
Logic.unvarify
     1 (*  Title: 	ZF/intr-elim.ML
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 Introduction/elimination rule module -- for Inductive/Coinductive Definitions
     7 *)
     8 
     9 signature INDUCTIVE_ARG =	(** Description of a (co)inductive def **)
    10   sig
    11   val thy        : theory               (*new theory with inductive defs*)
    12   val monos      : thm list		(*monotonicity of each M operator*)
    13   val con_defs   : thm list		(*definitions of the constructors*)
    14   val type_intrs : thm list		(*type-checking intro rules*)
    15   val type_elims : thm list		(*type-checking elim rules*)
    16   end;
    17 
    18 (*internal items*)
    19 signature INDUCTIVE_I =
    20   sig
    21   val rec_tms    : term list		(*the recursive sets*)
    22   val domts      : term list		(*their domains*)
    23   val intr_tms   : term list		(*terms for the introduction rules*)
    24   end;
    25 
    26 signature INTR_ELIM =
    27   sig
    28   val thy        : theory               (*copy of input theory*)
    29   val defs	 : thm list		(*definitions made in thy*)
    30   val bnd_mono   : thm			(*monotonicity for the lfp definition*)
    31   val unfold     : thm			(*fixed-point equation*)
    32   val dom_subset : thm			(*inclusion of recursive set in dom*)
    33   val intrs      : thm list		(*introduction rules*)
    34   val elim       : thm			(*case analysis theorem*)
    35   val raw_induct : thm			(*raw induction rule from Fp.induct*)
    36   val mk_cases : thm list -> string -> thm	(*generates case theorems*)
    37   val rec_names  : string list		(*names of recursive sets*)
    38   val sumprod_free_SEs : thm list       (*destruct rules for Su and Pr*)
    39   end;
    40 
    41 (*prove intr/elim rules for a fixedpoint definition*)
    42 functor Intr_elim_Fun
    43     (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end  
    44      and Fp: FP and Pr : PR and Su : SU) : INTR_ELIM =
    45 struct
    46 open Logic Inductive Ind_Syntax;
    47 
    48 val rec_names = map (#1 o dest_Const o head_of) rec_tms;
    49 val big_rec_name = space_implode "_" rec_names;
    50 
    51 (*fetch fp definitions from the theory*)
    52 val big_rec_def::part_rec_defs = 
    53   map (get_def thy)
    54       (case rec_names of [_] => rec_names | _ => big_rec_name::rec_names);
    55 
    56 
    57 val sign = sign_of thy;
    58 
    59 (********)
    60 val _ = writeln "  Proving monotonicity...";
    61 
    62 val Const("==",_) $ _ $ (_ $ dom_sum $ fp_abs) =
    63     big_rec_def |> rep_thm |> #prop |> Logic.unvarify;
    64 
    65 val bnd_mono = 
    66     prove_goalw_cterm [] 
    67       (cterm_of sign (mk_tprop (Fp.bnd_mono $ dom_sum $ fp_abs)))
    68       (fn _ =>
    69        [rtac (Collect_subset RS bnd_monoI) 1,
    70 	REPEAT (ares_tac (basic_monos @ monos) 1)]);
    71 
    72 val dom_subset = standard (big_rec_def RS Fp.subs);
    73 
    74 val unfold = standard (bnd_mono RS (big_rec_def RS Fp.Tarski));
    75 
    76 (********)
    77 val _ = writeln "  Proving the introduction rules...";
    78 
    79 (*Mutual recursion: Needs subset rules for the individual sets???*)
    80 val rec_typechecks = [dom_subset] RL (asm_rl::monos) RL [subsetD];
    81 
    82 (*Type-checking is hardest aspect of proof;
    83   disjIn selects the correct disjunct after unfolding*)
    84 fun intro_tacsf disjIn prems = 
    85   [(*insert prems and underlying sets*)
    86    cut_facts_tac prems 1,
    87    rtac (unfold RS ssubst) 1,
    88    REPEAT (resolve_tac [Part_eqI,CollectI] 1),
    89    (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
    90    rtac disjIn 2,
    91    REPEAT (ares_tac [refl,exI,conjI] 2),
    92    rewrite_goals_tac con_defs,
    93    (*Now can solve the trivial equation*)
    94    REPEAT (rtac refl 2),
    95    REPEAT (FIRSTGOAL (        dresolve_tac rec_typechecks
    96 		      ORELSE' eresolve_tac (asm_rl::PartE::SigmaE2::type_elims)
    97 		      ORELSE' hyp_subst_tac)),
    98    DEPTH_SOLVE (swap_res_tac (SigmaI::type_intrs) 1)];
    99 
   100 (*combines disjI1 and disjI2 to access the corresponding nested disjunct...*)
   101 val mk_disj_rls = 
   102     let fun f rl = rl RS disjI1
   103 	and g rl = rl RS disjI2
   104     in  accesses_bal(f, g, asm_rl)  end;
   105 
   106 val intrs = map (uncurry (prove_goalw_cterm part_rec_defs))
   107             (map (cterm_of sign) intr_tms ~~ 
   108 	     map intro_tacsf (mk_disj_rls(length intr_tms)));
   109 
   110 (********)
   111 val _ = writeln "  Proving the elimination rule...";
   112 
   113 (*Includes rules for succ and Pair since they are common constructions*)
   114 val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0, 
   115 		Pair_neq_0, sym RS Pair_neq_0, make_elim succ_inject, 
   116 		refl_thin, conjE, exE, disjE];
   117 
   118 val sumprod_free_SEs = 
   119     map (gen_make_elim [conjE,FalseE])
   120 	([Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff] 
   121 	 RL [iffD1]);
   122 
   123 (*Breaks down logical connectives in the monotonic function*)
   124 val basic_elim_tac =
   125     REPEAT (SOMEGOAL (eresolve_tac (elim_rls@sumprod_free_SEs)
   126 	      ORELSE' bound_hyp_subst_tac))
   127     THEN prune_params_tac;
   128 
   129 val elim = rule_by_tactic basic_elim_tac (unfold RS equals_CollectD);
   130 
   131 (*Applies freeness of the given constructors, which *must* be unfolded by
   132   the given defs.  Cannot simply use the local con_defs because con_defs=[] 
   133   for inference systems. *)
   134 fun con_elim_tac defs =
   135     rewrite_goals_tac defs THEN basic_elim_tac THEN fold_tac defs;
   136 
   137 (*String s should have the form t:Si where Si is an inductive set*)
   138 fun mk_cases defs s = 
   139     rule_by_tactic (con_elim_tac defs)
   140       (assume_read thy s  RS  elim);
   141 
   142 val defs = big_rec_def::part_rec_defs;
   143 
   144 val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct);
   145 end;
   146