src/ZF/Tools/induct_tacs.ML
author wenzelm
Fri, 19 Jan 2007 22:08:08 +0100
changeset 22101 6d13239d5f52
parent 21350 6e58289b6685
child 22846 fb79144af9a3
permissions -rw-r--r--
moved parts of OuterParse to SpecParse;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
     1
(*  Title:      ZF/Tools/induct_tacs.ML
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
     2
    ID:         $Id$
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
     5
12204
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
     6
Induction and exhaustion tactics for Isabelle/ZF.  The theory
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
     7
information needed to support them (and to support primrec).  Also a
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
     8
function to install other sets as if they were datatypes.
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
     9
*)
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
    10
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
    11
signature DATATYPE_TACTICS =
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
    12
sig
12204
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
    13
  val induct_tac: string -> int -> tactic
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
    14
  val exhaust_tac: string -> int -> tactic
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
    15
  val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15574
diff changeset
    16
  val rep_datatype: thmref * Attrib.src list -> thmref * Attrib.src list ->
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15574
diff changeset
    17
    (thmref * Attrib.src list) list -> (thmref * Attrib.src list) list -> theory -> theory
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18688
diff changeset
    18
  val setup: theory -> theory
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
    19
end;
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
    20
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
    21
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    22
(** Datatype information, e.g. associated theorems **)
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    23
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    24
type datatype_info =
12175
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
    25
  {inductive: bool,             (*true if inductive, not coinductive*)
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    26
   constructors : term list,    (*the constructors, as Consts*)
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    27
   rec_rewrites : thm list,     (*recursor equations*)
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    28
   case_rewrites : thm list,    (*case equations*)
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    29
   induct : thm,
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    30
   mutual_induct : thm,
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    31
   exhaustion : thm};
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    32
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16364
diff changeset
    33
structure DatatypesData = TheoryDataFun
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16364
diff changeset
    34
(struct
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    35
  val name = "ZF/datatypes";
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    36
  type T = datatype_info Symtab.table;
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    37
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    38
  val empty = Symtab.empty;
6556
daa00919502b theory data: copy;
wenzelm
parents: 6141
diff changeset
    39
  val copy = I;
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16364
diff changeset
    40
  val extend = I;
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16364
diff changeset
    41
  fun merge _ tabs : T = Symtab.merge (K true) tabs;
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    42
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16364
diff changeset
    43
  fun print thy tab =
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    44
    Pretty.writeln (Pretty.strs ("datatypes:" ::
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16364
diff changeset
    45
      map #1 (NameSpace.extern_table (Sign.type_space thy, tab))));
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16364
diff changeset
    46
end);
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    47
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    48
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    49
(** Constructor information: needed to map constructors to datatypes **)
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    50
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    51
type constructor_info =
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    52
  {big_rec_name : string,     (*name of the mutually recursive set*)
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    53
   constructors : term list,  (*the constructors, as Consts*)
6141
a6922171b396 removal of the (thm list) argument of mk_cases
paulson
parents: 6112
diff changeset
    54
   free_iffs    : thm list,   (*freeness simprules*)
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    55
   rec_rewrites : thm list};  (*recursor equations*)
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    56
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    57
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16364
diff changeset
    58
structure ConstructorsData = TheoryDataFun
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16364
diff changeset
    59
(struct
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    60
  val name = "ZF/constructors"
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    61
  type T = constructor_info Symtab.table
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    62
  val empty = Symtab.empty
6556
daa00919502b theory data: copy;
wenzelm
parents: 6141
diff changeset
    63
  val copy = I;
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16364
diff changeset
    64
  val extend = I
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16364
diff changeset
    65
  fun merge _ tabs: T = Symtab.merge (K true) tabs;
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16364
diff changeset
    66
  fun print _ _= ();
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16364
diff changeset
    67
end);
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    68
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
    69
structure DatatypeTactics : DATATYPE_TACTICS =
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
    70
struct
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
    71
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16364
diff changeset
    72
fun datatype_info thy name =
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17314
diff changeset
    73
  (case Symtab.lookup (DatatypesData.get thy) name of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15462
diff changeset
    74
    SOME info => info
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15462
diff changeset
    75
  | NONE => error ("Unknown datatype " ^ quote name));
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
    76
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
    77
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
    78
(*Given a variable, find the inductive set associated it in the assumptions*)
14153
76a6ba67bd15 new case_tac
paulson
parents: 12311
diff changeset
    79
exception Find_tname of string
76a6ba67bd15 new case_tac
paulson
parents: 12311
diff changeset
    80
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
    81
fun find_tname var Bi =
12175
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
    82
  let fun mk_pair (Const("op :",_) $ Free (v,_) $ A) =
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
    83
             (v, #1 (dest_Const (head_of A)))
12175
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
    84
        | mk_pair _ = raise Match
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
    85
      val pairs = List.mapPartial (try (mk_pair o FOLogic.dest_Trueprop))
12175
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
    86
          (#2 (strip_context Bi))
17314
04e21a27c0ad introduces some modern-style AList operations
haftmann
parents: 17223
diff changeset
    87
  in case AList.lookup (op =) pairs var of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15462
diff changeset
    88
       NONE => raise Find_tname ("Cannot determine datatype of " ^ quote var)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15462
diff changeset
    89
     | SOME t => t
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
    90
  end;
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
    91
12175
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
    92
(** generic exhaustion and induction tactic for datatypes
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
    93
    Differences from HOL:
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
    94
      (1) no checking if the induction var occurs in premises, since it always
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
    95
          appears in one of them, and it's hard to check for other occurrences
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
    96
      (2) exhaustion works for VARIABLES in the premises, not general terms
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
    97
**)
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
    98
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
    99
fun exhaust_induct_tac exh var i state =
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
   100
  let
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
   101
    val (_, _, Bi, _) = dest_state (state, i)
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16364
diff changeset
   102
    val thy = Thm.theory_of_thm state
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
   103
    val tn = find_tname var Bi
12175
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
   104
    val rule =
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16364
diff changeset
   105
        if exh then #exhaustion (datatype_info thy tn)
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16364
diff changeset
   106
               else #induct  (datatype_info thy tn)
12175
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
   107
    val (Const("op :",_) $ Var(ixn,_) $ _) =
6112
5e4871c5136b datatype package improvements
paulson
parents: 6092
diff changeset
   108
        (case prems_of rule of
12175
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
   109
             [] => error "induction is not available for this datatype"
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
   110
           | major::_ => FOLogic.dest_Trueprop major)
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
   111
  in
15462
b4208fbf9439 Eliminated hack for deleting leading question mark from induction
berghofe
parents: 14153
diff changeset
   112
    Tactic.eres_inst_tac' [(ixn, var)] rule i state
14153
76a6ba67bd15 new case_tac
paulson
parents: 12311
diff changeset
   113
  end
76a6ba67bd15 new case_tac
paulson
parents: 12311
diff changeset
   114
  handle Find_tname msg =>
76a6ba67bd15 new case_tac
paulson
parents: 12311
diff changeset
   115
            if exh then (*try boolean case analysis instead*)
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16364
diff changeset
   116
                case_tac var i state
14153
76a6ba67bd15 new case_tac
paulson
parents: 12311
diff changeset
   117
            else error msg;
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
   118
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
   119
val exhaust_tac = exhaust_induct_tac true;
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
   120
val induct_tac = exhaust_induct_tac false;
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
   121
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
   122
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
   123
(**** declare non-datatype as datatype ****)
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
   124
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
   125
fun rep_datatype_i elim induct case_eqns recursor_eqns thy =
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
   126
  let
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
   127
    (*analyze the LHS of a case equation to get a constructor*)
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
   128
    fun const_of (Const("op =", _) $ (_ $ c) $ _) = c
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
   129
      | const_of eqn = error ("Ill-formed case equation: " ^
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16364
diff changeset
   130
                              Sign.string_of_term thy eqn);
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
   131
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
   132
    val constructors =
12175
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
   133
        map (head_of o const_of o FOLogic.dest_Trueprop o
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
   134
             #prop o rep_thm) case_eqns;
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
   135
6112
5e4871c5136b datatype package improvements
paulson
parents: 6092
diff changeset
   136
    val Const ("op :", _) $ _ $ data =
12175
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
   137
        FOLogic.dest_Trueprop (hd (prems_of elim));
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
   138
6112
5e4871c5136b datatype package improvements
paulson
parents: 6092
diff changeset
   139
    val Const(big_rec_name, _) = head_of data;
5e4871c5136b datatype package improvements
paulson
parents: 6092
diff changeset
   140
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
   141
    val simps = case_eqns @ recursor_eqns;
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
   142
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
   143
    val dt_info =
12175
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
   144
          {inductive = true,
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
   145
           constructors = constructors,
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
   146
           rec_rewrites = recursor_eqns,
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
   147
           case_rewrites = case_eqns,
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
   148
           induct = induct,
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
   149
           mutual_induct = TrueI,  (*No need for mutual induction*)
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
   150
           exhaustion = elim};
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
   151
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
   152
    val con_info =
12175
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
   153
          {big_rec_name = big_rec_name,
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
   154
           constructors = constructors,
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
   155
              (*let primrec handle definition by cases*)
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
   156
           free_iffs = [],  (*thus we expect the necessary freeness rewrites
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
   157
                              to be in the simpset already, as is the case for
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
   158
                              Nat and disjoint sum*)
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
   159
           rec_rewrites = (case recursor_eqns of
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
   160
                               [] => case_eqns | _ => recursor_eqns)};
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
   161
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
   162
    (*associate with each constructor the datatype name and rewrites*)
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
   163
    val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
   164
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
   165
  in
17223
430edc6b7826 curried_lookup/update;
wenzelm
parents: 17057
diff changeset
   166
    thy
430edc6b7826 curried_lookup/update;
wenzelm
parents: 17057
diff changeset
   167
    |> Theory.add_path (Sign.base_name big_rec_name)
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   168
    |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add])] |> snd
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17314
diff changeset
   169
    |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17314
diff changeset
   170
    |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
17223
430edc6b7826 curried_lookup/update;
wenzelm
parents: 17057
diff changeset
   171
    |> Theory.parent_path
12204
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
   172
  end;
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents:
diff changeset
   173
12204
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
   174
fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =
18418
bf448d999b7e re-arranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents: 18377
diff changeset
   175
  thy
21350
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 18728
diff changeset
   176
  |> IsarCmd.apply_theorems [raw_elim]
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 18728
diff changeset
   177
  ||>> IsarCmd.apply_theorems [raw_induct]
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 18728
diff changeset
   178
  ||>> IsarCmd.apply_theorems raw_case_eqns
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 18728
diff changeset
   179
  ||>> IsarCmd.apply_theorems raw_recursor_eqns
18418
bf448d999b7e re-arranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents: 18377
diff changeset
   180
  |-> (fn (((elims, inducts), case_eqns), recursor_eqns) =>
bf448d999b7e re-arranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents: 18377
diff changeset
   181
          rep_datatype_i (PureThy.single_thm "elimination" elims)
bf448d999b7e re-arranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents: 18377
diff changeset
   182
            (PureThy.single_thm "induction" inducts) case_eqns recursor_eqns);
12175
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
   183
12204
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
   184
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
   185
(* theory setup *)
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
   186
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
   187
val setup =
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18688
diff changeset
   188
 (DatatypesData.init #>
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18688
diff changeset
   189
  ConstructorsData.init #>
12175
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
   190
  Method.add_methods
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
   191
    [("induct_tac", Method.goal_args Args.name induct_tac,
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 12109
diff changeset
   192
      "induct_tac emulation (dynamic instantiation!)"),
14153
76a6ba67bd15 new case_tac
paulson
parents: 12311
diff changeset
   193
     ("case_tac", Method.goal_args Args.name exhaust_tac,
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18688
diff changeset
   194
      "datatype case_tac emulation (dynamic instantiation!)")]);
12204
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
   195
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
   196
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
   197
(* outer syntax *)
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
   198
17057
0934ac31985f OuterKeyword;
wenzelm
parents: 16458
diff changeset
   199
local structure P = OuterParse and K = OuterKeyword in
12204
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
   200
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
   201
val rep_datatype_decl =
22101
6d13239d5f52 moved parts of OuterParse to SpecParse;
wenzelm
parents: 21350
diff changeset
   202
  (P.$$$ "elimination" |-- P.!!! SpecParse.xthm) --
6d13239d5f52 moved parts of OuterParse to SpecParse;
wenzelm
parents: 21350
diff changeset
   203
  (P.$$$ "induction" |-- P.!!! SpecParse.xthm) --
6d13239d5f52 moved parts of OuterParse to SpecParse;
wenzelm
parents: 21350
diff changeset
   204
  (P.$$$ "case_eqns" |-- P.!!! SpecParse.xthms1) --
6d13239d5f52 moved parts of OuterParse to SpecParse;
wenzelm
parents: 21350
diff changeset
   205
  Scan.optional (P.$$$ "recursor_eqns" |-- P.!!! SpecParse.xthms1) []
12204
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
   206
  >> (fn (((x, y), z), w) => rep_datatype x y z w);
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
   207
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
   208
val rep_datatypeP =
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
   209
  OuterSyntax.command "rep_datatype" "represent existing set inductively" K.thy_decl
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
   210
    (rep_datatype_decl >> Toplevel.theory);
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
   211
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
   212
val _ = OuterSyntax.add_keywords ["elimination", "induction", "case_eqns", "recursor_eqns"];
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
   213
val _ = OuterSyntax.add_parsers [rep_datatypeP];
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
   214
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
   215
end;
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
   216
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
   217
end;
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
   218
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
   219
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
   220
val exhaust_tac = DatatypeTactics.exhaust_tac;
98115606ee42 Isar version of 'rep_datatype';
wenzelm
parents: 12175
diff changeset
   221
val induct_tac  = DatatypeTactics.induct_tac;