src/HOL/intr_elim.ML
author paulson
Fri Feb 28 15:46:41 1997 +0100 (1997-02-28)
changeset 2688 889a1cbd1aca
parent 2414 13df7d6c5c3b
child 3978 7e1cfed19d94
permissions -rw-r--r--
rule_by_tactic no longer standardizes its result
     1 (*  Title:      HOL/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   end;
    15 
    16 
    17 signature INDUCTIVE_I = (** Terms read from the theory section **)
    18   sig
    19   val rec_tms    : term list            (*the recursive sets*)
    20   val intr_tms   : term list            (*terms for the introduction rules*)
    21   end;
    22 
    23 signature INTR_ELIM =
    24   sig
    25   val thy        : theory               (*copy of input theory*)
    26   val defs       : thm list             (*definitions made in thy*)
    27   val mono       : thm                  (*monotonicity for the lfp definition*)
    28   val intrs      : thm list             (*introduction rules*)
    29   val elim       : thm                  (*case analysis theorem*)
    30   val mk_cases   : thm list -> string -> thm    (*generates case theorems*)
    31   end;
    32 
    33 signature INTR_ELIM_AUX =       (** Used to make induction rules **)
    34   sig
    35   val raw_induct : thm                  (*raw induction rule from Fp.induct*)
    36   val rec_names  : string list          (*names of recursive sets*)
    37   end;
    38 
    39 (*prove intr/elim rules for a fixedpoint definition*)
    40 functor Intr_elim_Fun
    41     (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end  
    42      and Fp: FP) 
    43     : sig include INTR_ELIM INTR_ELIM_AUX end =
    44 let
    45 val rec_names = map (#1 o dest_Const o head_of) Inductive.rec_tms;
    46 val big_rec_name = space_implode "_" rec_names;
    47 
    48 val _ = deny (big_rec_name  mem  map ! (stamps_of_thy Inductive.thy))
    49              ("Definition " ^ big_rec_name ^ 
    50               " would clash with the theory of the same name!");
    51 
    52 (*fetch fp definitions from the theory*)
    53 val big_rec_def::part_rec_defs = 
    54   map (get_def Inductive.thy)
    55       (case rec_names of [_] => rec_names | _ => big_rec_name::rec_names);
    56 
    57 
    58 val sign = sign_of Inductive.thy;
    59 
    60 (********)
    61 val _ = writeln "  Proving monotonicity...";
    62 
    63 val Const("==",_) $ _ $ (Const(_,fpT) $ fp_abs) =
    64     big_rec_def |> rep_thm |> #prop |> Logic.unvarify;
    65 
    66 (*For the type of the argument of mono*)
    67 val [monoT] = binder_types fpT;
    68 
    69 val mono = 
    70     prove_goalw_cterm [] 
    71       (cterm_of sign (Ind_Syntax.mk_Trueprop 
    72                       (Const("mono", monoT --> Ind_Syntax.boolT) $ fp_abs)))
    73       (fn _ =>
    74        [rtac monoI 1,
    75         REPEAT (ares_tac (basic_monos @ Inductive.monos) 1)]);
    76 
    77 val unfold = standard (mono RS (big_rec_def RS Fp.Tarski));
    78 
    79 (********)
    80 val _ = writeln "  Proving the introduction rules...";
    81 
    82 fun intro_tacsf disjIn prems = 
    83   [(*insert prems and underlying sets*)
    84    cut_facts_tac prems 1,
    85    stac unfold 1,
    86    REPEAT (resolve_tac [Part_eqI,CollectI] 1),
    87    (*Now 1-2 subgoals: the disjunction, perhaps equality.*)
    88    rtac disjIn 1,
    89    (*Not ares_tac, since refl must be tried before any equality assumptions;
    90      backtracking may occur if the premises have extra variables!*)
    91    DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 1 APPEND assume_tac 1),
    92    (*Now solve the equations like Inl 0 = Inl ?b2*)
    93    rewrite_goals_tac Inductive.con_defs,
    94    REPEAT (rtac refl 1)];
    95 
    96 
    97 (*combines disjI1 and disjI2 to access the corresponding nested disjunct...*)
    98 val mk_disj_rls = 
    99     let fun f rl = rl RS disjI1
   100         and g rl = rl RS disjI2
   101     in  accesses_bal(f, g, asm_rl)  end;
   102 
   103 val intrs = ListPair.map (uncurry (prove_goalw_cterm part_rec_defs))
   104             (map (cterm_of sign) Inductive.intr_tms,
   105              map intro_tacsf (mk_disj_rls(length Inductive.intr_tms)));
   106 
   107 (********)
   108 val _ = writeln "  Proving the elimination rule...";
   109 
   110 (*Breaks down logical connectives in the monotonic function*)
   111 val basic_elim_tac =
   112     REPEAT (SOMEGOAL (eresolve_tac (Ind_Syntax.elim_rls @ 
   113                                     Ind_Syntax.sumprod_free_SEs)
   114               ORELSE' bound_hyp_subst_tac))
   115     THEN prune_params_tac;
   116 
   117 (*Applies freeness of the given constructors, which *must* be unfolded by
   118   the given defs.  Cannot simply use the local con_defs because con_defs=[] 
   119   for inference systems.
   120 fun con_elim_tac defs =
   121     rewrite_goals_tac defs THEN basic_elim_tac THEN fold_tac defs;
   122  *)
   123 fun con_elim_tac simps =
   124   let val elim_tac = REPEAT o (eresolve_tac (Ind_Syntax.elim_rls @ 
   125                                              Ind_Syntax.sumprod_free_SEs))
   126   in ALLGOALS(EVERY'[elim_tac,
   127                      asm_full_simp_tac (simpset_of "Nat" addsimps simps),
   128                      elim_tac,
   129                      REPEAT o bound_hyp_subst_tac])
   130      THEN prune_params_tac
   131   end;
   132 
   133 
   134 in
   135   struct
   136   val thy   = Inductive.thy
   137   and defs  = big_rec_def :: part_rec_defs
   138   and mono  = mono
   139   and intrs = intrs;
   140 
   141   val elim = rule_by_tactic basic_elim_tac 
   142                   (unfold RS Ind_Syntax.equals_CollectD);
   143 
   144   (*String s should have the form t:Si where Si is an inductive set*)
   145   fun mk_cases defs s = 
   146       rule_by_tactic (con_elim_tac defs)
   147           (assume_read Inductive.thy s  RS  elim) 
   148       |> standard;
   149 
   150   val raw_induct = standard ([big_rec_def, mono] MRS Fp.induct)
   151   and rec_names = rec_names
   152   end
   153 end;
   154