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