src/HOL/Tools/inductive_package.ML
 author wenzelm Fri Mar 03 21:01:57 2000 +0100 (2000-03-03) changeset 8336 fdf3ac335f77 parent 8316 74639e19eca0 child 8375 0544749a5e8f permissions -rw-r--r--
mk_cases / inductive_cases: use InductMethod.con_elim_(solved_)tac;
```     1 (*  Title:      HOL/Tools/inductive_package.ML
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4                 Stefan Berghofer,   TU Muenchen
```
```     5     Copyright   1994  University of Cambridge
```
```     6                 1998  TU Muenchen
```
```     7
```
```     8 (Co)Inductive Definition module for HOL.
```
```     9
```
```    10 Features:
```
```    11   * least or greatest fixedpoints
```
```    12   * user-specified product and sum constructions
```
```    13   * mutually recursive definitions
```
```    14   * definitions involving arbitrary monotone operators
```
```    15   * automatically proves introduction and elimination rules
```
```    16
```
```    17 The recursive sets must *already* be declared as constants in the
```
```    18 current theory!
```
```    19
```
```    20   Introduction rules have the form
```
```    21   [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk
```
```    22   where M is some monotone operator (usually the identity)
```
```    23   P(x) is any side condition on the free variables
```
```    24   ti, t are any terms
```
```    25   Sj, Sk are two of the sets being defined in mutual recursion
```
```    26
```
```    27 Sums are used only for mutual recursion.  Products are used only to
```
```    28 derive "streamlined" induction rules for relations.
```
```    29 *)
```
```    30
```
```    31 signature INDUCTIVE_PACKAGE =
```
```    32 sig
```
```    33   val quiet_mode: bool ref
```
```    34   val unify_consts: Sign.sg -> term list -> term list -> term list * term list
```
```    35   val get_inductive: theory -> string ->
```
```    36     {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
```
```    37       induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
```
```    38   val print_inductives: theory -> unit
```
```    39   val mono_add_global: theory attribute
```
```    40   val mono_del_global: theory attribute
```
```    41   val get_monos: theory -> thm list
```
```    42   val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
```
```    43     theory attribute list -> ((bstring * term) * theory attribute list) list ->
```
```    44       thm list -> thm list -> theory -> theory *
```
```    45       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
```
```    46        intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
```
```    47   val add_inductive: bool -> bool -> string list -> Args.src list ->
```
```    48     ((bstring * string) * Args.src list) list -> (xstring * Args.src list) list ->
```
```    49       (xstring * Args.src list) list -> theory -> theory *
```
```    50       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
```
```    51        intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
```
```    52   val inductive_cases: (((bstring * Args.src list) * xstring) * string list) * Comment.text
```
```    53     -> theory -> theory
```
```    54   val inductive_cases_i: (((bstring * theory attribute list) * string) * term list) * Comment.text
```
```    55     -> theory -> theory
```
```    56   val setup: (theory -> theory) list
```
```    57 end;
```
```    58
```
```    59 structure InductivePackage: INDUCTIVE_PACKAGE =
```
```    60 struct
```
```    61
```
```    62 (*** theory data ***)
```
```    63
```
```    64 (* data kind 'HOL/inductive' *)
```
```    65
```
```    66 type inductive_info =
```
```    67   {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
```
```    68     induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm};
```
```    69
```
```    70 structure InductiveArgs =
```
```    71 struct
```
```    72   val name = "HOL/inductive";
```
```    73   type T = inductive_info Symtab.table * thm list;
```
```    74
```
```    75   val empty = (Symtab.empty, []);
```
```    76   val copy = I;
```
```    77   val prep_ext = I;
```
```    78   fun merge ((tab1, monos1), (tab2, monos2)) = (Symtab.merge (K true) (tab1, tab2),
```
```    79     Library.generic_merge Thm.eq_thm I I monos1 monos2);
```
```    80
```
```    81   fun print sg (tab, monos) =
```
```    82     (Pretty.writeln (Pretty.strs ("(co)inductives:" ::
```
```    83        map #1 (Sign.cond_extern_table sg Sign.constK tab)));
```
```    84      Pretty.writeln (Pretty.big_list "monotonicity rules:" (map Display.pretty_thm monos)));
```
```    85 end;
```
```    86
```
```    87 structure InductiveData = TheoryDataFun(InductiveArgs);
```
```    88 val print_inductives = InductiveData.print;
```
```    89
```
```    90
```
```    91 (* get and put data *)
```
```    92
```
```    93 fun get_inductive thy name =
```
```    94   (case Symtab.lookup (fst (InductiveData.get thy), name) of
```
```    95     Some info => info
```
```    96   | None => error ("Unknown (co)inductive set " ^ quote name));
```
```    97
```
```    98 fun put_inductives names info thy =
```
```    99   let
```
```   100     fun upd ((tab, monos), name) = (Symtab.update_new ((name, info), tab), monos);
```
```   101     val tab_monos = foldl upd (InductiveData.get thy, names)
```
```   102       handle Symtab.DUP name => error ("Duplicate definition of (co)inductive set " ^ quote name);
```
```   103   in InductiveData.put tab_monos thy end;
```
```   104
```
```   105
```
```   106
```
```   107 (** monotonicity rules **)
```
```   108
```
```   109 val get_monos = snd o InductiveData.get;
```
```   110 fun put_monos thms thy = InductiveData.put (fst (InductiveData.get thy), thms) thy;
```
```   111
```
```   112 fun mk_mono thm =
```
```   113   let
```
```   114     fun eq2mono thm' = [standard (thm' RS (thm' RS eq_to_mono))] @
```
```   115       (case concl_of thm of
```
```   116           (_ \$ (_ \$ (Const ("Not", _) \$ _) \$ _)) => []
```
```   117         | _ => [standard (thm' RS (thm' RS eq_to_mono2))]);
```
```   118     val concl = concl_of thm
```
```   119   in
```
```   120     if Logic.is_equals concl then
```
```   121       eq2mono (thm RS meta_eq_to_obj_eq)
```
```   122     else if can (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl then
```
```   123       eq2mono thm
```
```   124     else [thm]
```
```   125   end;
```
```   126
```
```   127 (* mono add/del *)
```
```   128
```
```   129 local
```
```   130
```
```   131 fun map_rules_global f thy = put_monos (f (get_monos thy)) thy;
```
```   132
```
```   133 fun add_mono thm rules = Library.gen_union Thm.eq_thm (mk_mono thm, rules);
```
```   134 fun del_mono thm rules = Library.gen_rems Thm.eq_thm (rules, mk_mono thm);
```
```   135
```
```   136 fun mk_att f g (x, thm) = (f (g thm) x, thm);
```
```   137
```
```   138 in
```
```   139
```
```   140 val mono_add_global = mk_att map_rules_global add_mono;
```
```   141 val mono_del_global = mk_att map_rules_global del_mono;
```
```   142
```
```   143 end;
```
```   144
```
```   145
```
```   146 (* concrete syntax *)
```
```   147
```
```   148 val monoN = "mono";
```
```   149 val addN = "add";
```
```   150 val delN = "del";
```
```   151
```
```   152 fun mono_att add del =
```
```   153   Attrib.syntax (Scan.lift (Args.\$\$\$ addN >> K add || Args.\$\$\$ delN >> K del || Scan.succeed add));
```
```   154
```
```   155 val mono_attr =
```
```   156   (mono_att mono_add_global mono_del_global, mono_att Attrib.undef_local_attribute Attrib.undef_local_attribute);
```
```   157
```
```   158
```
```   159
```
```   160 (** utilities **)
```
```   161
```
```   162 (* messages *)
```
```   163
```
```   164 val quiet_mode = ref false;
```
```   165 fun message s = if !quiet_mode then () else writeln s;
```
```   166
```
```   167 fun coind_prefix true = "co"
```
```   168   | coind_prefix false = "";
```
```   169
```
```   170
```
```   171 (* the following code ensures that each recursive set *)
```
```   172 (* always has the same type in all introduction rules *)
```
```   173
```
```   174 fun unify_consts sign cs intr_ts =
```
```   175   (let
```
```   176     val {tsig, ...} = Sign.rep_sg sign;
```
```   177     val add_term_consts_2 =
```
```   178       foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs);
```
```   179     fun varify (t, (i, ts)) =
```
```   180       let val t' = map_term_types (incr_tvar (i + 1)) (Type.varify (t, []))
```
```   181       in (maxidx_of_term t', t'::ts) end;
```
```   182     val (i, cs') = foldr varify (cs, (~1, []));
```
```   183     val (i', intr_ts') = foldr varify (intr_ts, (i, []));
```
```   184     val rec_consts = foldl add_term_consts_2 ([], cs');
```
```   185     val intr_consts = foldl add_term_consts_2 ([], intr_ts');
```
```   186     fun unify (env, (cname, cT)) =
```
```   187       let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
```
```   188       in foldl (fn ((env', j'), Tp) => (Type.unify tsig j' env' Tp))
```
```   189           (env, (replicate (length consts) cT) ~~ consts)
```
```   190       end;
```
```   191     val (env, _) = foldl unify (([], i'), rec_consts);
```
```   192     fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars env T
```
```   193       in if T = T' then T else typ_subst_TVars_2 env T' end;
```
```   194     val subst = fst o Type.freeze_thaw o
```
```   195       (map_term_types (typ_subst_TVars_2 env))
```
```   196
```
```   197   in (map subst cs', map subst intr_ts')
```
```   198   end) handle Type.TUNIFY =>
```
```   199     (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
```
```   200
```
```   201
```
```   202 (* misc *)
```
```   203
```
```   204 val Const _ \$ (vimage_f \$ _) \$ _ = HOLogic.dest_Trueprop (concl_of vimageD);
```
```   205
```
```   206 val vimage_name = Sign.intern_const (Theory.sign_of Vimage.thy) "op -``";
```
```   207 val mono_name = Sign.intern_const (Theory.sign_of Ord.thy) "mono";
```
```   208
```
```   209 (* make injections needed in mutually recursive definitions *)
```
```   210
```
```   211 fun mk_inj cs sumT c x =
```
```   212   let
```
```   213     fun mk_inj' T n i =
```
```   214       if n = 1 then x else
```
```   215       let val n2 = n div 2;
```
```   216           val Type (_, [T1, T2]) = T
```
```   217       in
```
```   218         if i <= n2 then
```
```   219           Const ("Inl", T1 --> T) \$ (mk_inj' T1 n2 i)
```
```   220         else
```
```   221           Const ("Inr", T2 --> T) \$ (mk_inj' T2 (n - n2) (i - n2))
```
```   222       end
```
```   223   in mk_inj' sumT (length cs) (1 + find_index_eq c cs)
```
```   224   end;
```
```   225
```
```   226 (* make "vimage" terms for selecting out components of mutually rec.def. *)
```
```   227
```
```   228 fun mk_vimage cs sumT t c = if length cs < 2 then t else
```
```   229   let
```
```   230     val cT = HOLogic.dest_setT (fastype_of c);
```
```   231     val vimageT = [cT --> sumT, HOLogic.mk_setT sumT] ---> HOLogic.mk_setT cT
```
```   232   in
```
```   233     Const (vimage_name, vimageT) \$
```
```   234       Abs ("y", cT, mk_inj cs sumT c (Bound 0)) \$ t
```
```   235   end;
```
```   236
```
```   237
```
```   238
```
```   239 (** well-formedness checks **)
```
```   240
```
```   241 fun err_in_rule sign t msg = error ("Ill-formed introduction rule\n" ^
```
```   242   (Sign.string_of_term sign t) ^ "\n" ^ msg);
```
```   243
```
```   244 fun err_in_prem sign t p msg = error ("Ill-formed premise\n" ^
```
```   245   (Sign.string_of_term sign p) ^ "\nin introduction rule\n" ^
```
```   246   (Sign.string_of_term sign t) ^ "\n" ^ msg);
```
```   247
```
```   248 val msg1 = "Conclusion of introduction rule must have form\
```
```   249           \ ' t : S_i '";
```
```   250 val msg2 = "Non-atomic premise";
```
```   251 val msg3 = "Recursion term on left of member symbol";
```
```   252
```
```   253 fun check_rule sign cs r =
```
```   254   let
```
```   255     fun check_prem prem = if can HOLogic.dest_Trueprop prem then ()
```
```   256       else err_in_prem sign r prem msg2;
```
```   257
```
```   258   in (case HOLogic.dest_Trueprop (Logic.strip_imp_concl r) of
```
```   259         (Const ("op :", _) \$ t \$ u) =>
```
```   260           if u mem cs then
```
```   261             if exists (Logic.occs o (rpair t)) cs then
```
```   262               err_in_rule sign r msg3
```
```   263             else
```
```   264               seq check_prem (Logic.strip_imp_prems r)
```
```   265           else err_in_rule sign r msg1
```
```   266       | _ => err_in_rule sign r msg1)
```
```   267   end;
```
```   268
```
```   269 fun try' f msg sign t = (case (try f t) of
```
```   270       Some x => x
```
```   271     | None => error (msg ^ Sign.string_of_term sign t));
```
```   272
```
```   273
```
```   274
```
```   275 (*** properties of (co)inductive sets ***)
```
```   276
```
```   277 (** elimination rules **)
```
```   278
```
```   279 fun mk_elims cs cTs params intr_ts =
```
```   280   let
```
```   281     val used = foldr add_term_names (intr_ts, []);
```
```   282     val [aname, pname] = variantlist (["a", "P"], used);
```
```   283     val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
```
```   284
```
```   285     fun dest_intr r =
```
```   286       let val Const ("op :", _) \$ t \$ u =
```
```   287         HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
```
```   288       in (u, t, Logic.strip_imp_prems r) end;
```
```   289
```
```   290     val intrs = map dest_intr intr_ts;
```
```   291
```
```   292     fun mk_elim (c, T) =
```
```   293       let
```
```   294         val a = Free (aname, T);
```
```   295
```
```   296         fun mk_elim_prem (_, t, ts) =
```
```   297           list_all_free (map dest_Free ((foldr add_term_frees (t::ts, [])) \\ params),
```
```   298             Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P));
```
```   299       in
```
```   300         Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) ::
```
```   301           map mk_elim_prem (filter (equal c o #1) intrs), P)
```
```   302       end
```
```   303   in
```
```   304     map mk_elim (cs ~~ cTs)
```
```   305   end;
```
```   306
```
```   307
```
```   308
```
```   309 (** premises and conclusions of induction rules **)
```
```   310
```
```   311 fun mk_indrule cs cTs params intr_ts =
```
```   312   let
```
```   313     val used = foldr add_term_names (intr_ts, []);
```
```   314
```
```   315     (* predicates for induction rule *)
```
```   316
```
```   317     val preds = map Free (variantlist (if length cs < 2 then ["P"] else
```
```   318       map (fn i => "P" ^ string_of_int i) (1 upto length cs), used) ~~
```
```   319         map (fn T => T --> HOLogic.boolT) cTs);
```
```   320
```
```   321     (* transform an introduction rule into a premise for induction rule *)
```
```   322
```
```   323     fun mk_ind_prem r =
```
```   324       let
```
```   325         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
```
```   326
```
```   327         val pred_of = curry (Library.gen_assoc (op aconv)) (cs ~~ preds);
```
```   328
```
```   329         fun subst (s as ((m as Const ("op :", T)) \$ t \$ u)) =
```
```   330               (case pred_of u of
```
```   331                   None => (m \$ fst (subst t) \$ fst (subst u), None)
```
```   332                 | Some P => (HOLogic.conj \$ s \$ (P \$ t), Some (s, P \$ t)))
```
```   333           | subst s =
```
```   334               (case pred_of s of
```
```   335                   Some P => (HOLogic.mk_binop "op Int"
```
```   336                     (s, HOLogic.Collect_const (HOLogic.dest_setT
```
```   337                       (fastype_of s)) \$ P), None)
```
```   338                 | None => (case s of
```
```   339                      (t \$ u) => (fst (subst t) \$ fst (subst u), None)
```
```   340                    | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), None)
```
```   341                    | _ => (s, None)));
```
```   342
```
```   343         fun mk_prem (s, prems) = (case subst s of
```
```   344               (_, Some (t, u)) => t :: u :: prems
```
```   345             | (t, _) => t :: prems);
```
```   346
```
```   347         val Const ("op :", _) \$ t \$ u =
```
```   348           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
```
```   349
```
```   350       in list_all_free (frees,
```
```   351            Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem
```
```   352              (map HOLogic.dest_Trueprop (Logic.strip_imp_prems r), [])),
```
```   353                HOLogic.mk_Trueprop (the (pred_of u) \$ t)))
```
```   354       end;
```
```   355
```
```   356     val ind_prems = map mk_ind_prem intr_ts;
```
```   357
```
```   358     (* make conclusions for induction rules *)
```
```   359
```
```   360     fun mk_ind_concl ((c, P), (ts, x)) =
```
```   361       let val T = HOLogic.dest_setT (fastype_of c);
```
```   362           val Ts = HOLogic.prodT_factors T;
```
```   363           val (frees, x') = foldr (fn (T', (fs, s)) =>
```
```   364             ((Free (s, T'))::fs, bump_string s)) (Ts, ([], x));
```
```   365           val tuple = HOLogic.mk_tuple T frees;
```
```   366       in ((HOLogic.mk_binop "op -->"
```
```   367         (HOLogic.mk_mem (tuple, c), P \$ tuple))::ts, x')
```
```   368       end;
```
```   369
```
```   370     val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
```
```   371         (fst (foldr mk_ind_concl (cs ~~ preds, ([], "xa")))))
```
```   372
```
```   373   in (preds, ind_prems, mutual_ind_concl)
```
```   374   end;
```
```   375
```
```   376
```
```   377
```
```   378 (** prepare cases and induct rules **)
```
```   379
```
```   380 (*
```
```   381   transform mutual rule:
```
```   382     HH ==> (x1:A1 --> P1 x1) & ... & (xn:An --> Pn xn)
```
```   383   into i-th projection:
```
```   384     xi:Ai ==> HH ==> Pi xi
```
```   385 *)
```
```   386
```
```   387 fun project_rules [name] rule = [(name, rule)]
```
```   388   | project_rules names mutual_rule =
```
```   389       let
```
```   390         val n = length names;
```
```   391         fun proj i =
```
```   392           (if i < n then (fn th => th RS conjunct1) else I)
```
```   393             (Library.funpow (i - 1) (fn th => th RS conjunct2) mutual_rule)
```
```   394             RS mp |> Thm.permute_prems 0 ~1 |> Drule.standard;
```
```   395       in names ~~ map proj (1 upto n) end;
```
```   396
```
```   397 fun add_cases_induct no_elim no_ind names elims induct =
```
```   398   let
```
```   399     val cases_specs =
```
```   400       if no_elim then []
```
```   401       else map2 (fn (name, elim) => (("", elim), [InductMethod.cases_set_global name]))
```
```   402         (names, elims);
```
```   403
```
```   404     val induct_specs =
```
```   405       if no_ind then []
```
```   406       else map (fn (name, th) => (("", th), [InductMethod.induct_set_global name]))
```
```   407         (project_rules names induct);
```
```   408   in PureThy.add_thms (cases_specs @ induct_specs) end;
```
```   409
```
```   410
```
```   411
```
```   412 (*** proofs for (co)inductive sets ***)
```
```   413
```
```   414 (** prove monotonicity **)
```
```   415
```
```   416 fun prove_mono setT fp_fun monos thy =
```
```   417   let
```
```   418     val _ = message "  Proving monotonicity ...";
```
```   419
```
```   420     val mono = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop
```
```   421       (Const (mono_name, (setT --> setT) --> HOLogic.boolT) \$ fp_fun)))
```
```   422         (fn _ => [rtac monoI 1, REPEAT (ares_tac (get_monos thy @ flat (map mk_mono monos)) 1)])
```
```   423
```
```   424   in mono end;
```
```   425
```
```   426
```
```   427
```
```   428 (** prove introduction rules **)
```
```   429
```
```   430 fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy =
```
```   431   let
```
```   432     val _ = message "  Proving the introduction rules ...";
```
```   433
```
```   434     val unfold = standard (mono RS (fp_def RS
```
```   435       (if coind then def_gfp_Tarski else def_lfp_Tarski)));
```
```   436
```
```   437     fun select_disj 1 1 = []
```
```   438       | select_disj _ 1 = [rtac disjI1]
```
```   439       | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
```
```   440
```
```   441     val intrs = map (fn (i, intr) => prove_goalw_cterm rec_sets_defs
```
```   442       (cterm_of (Theory.sign_of thy) intr) (fn prems =>
```
```   443        [(*insert prems and underlying sets*)
```
```   444        cut_facts_tac prems 1,
```
```   445        stac unfold 1,
```
```   446        REPEAT (resolve_tac [vimageI2, CollectI] 1),
```
```   447        (*Now 1-2 subgoals: the disjunction, perhaps equality.*)
```
```   448        EVERY1 (select_disj (length intr_ts) i),
```
```   449        (*Not ares_tac, since refl must be tried before any equality assumptions;
```
```   450          backtracking may occur if the premises have extra variables!*)
```
```   451        DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 1 APPEND assume_tac 1),
```
```   452        (*Now solve the equations like Inl 0 = Inl ?b2*)
```
```   453        rewrite_goals_tac con_defs,
```
```   454        REPEAT (rtac refl 1)])) (1 upto (length intr_ts) ~~ intr_ts)
```
```   455
```
```   456   in (intrs, unfold) end;
```
```   457
```
```   458
```
```   459
```
```   460 (** prove elimination rules **)
```
```   461
```
```   462 fun prove_elims cs cTs params intr_ts unfold rec_sets_defs thy =
```
```   463   let
```
```   464     val _ = message "  Proving the elimination rules ...";
```
```   465
```
```   466     val rules1 = [CollectE, disjE, make_elim vimageD, exE];
```
```   467     val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @
```
```   468       map make_elim [Inl_inject, Inr_inject];
```
```   469
```
```   470     val elims = map (fn t => prove_goalw_cterm rec_sets_defs
```
```   471       (cterm_of (Theory.sign_of thy) t) (fn prems =>
```
```   472         [cut_facts_tac [hd prems] 1,
```
```   473          dtac (unfold RS subst) 1,
```
```   474          REPEAT (FIRSTGOAL (eresolve_tac rules1)),
```
```   475          REPEAT (FIRSTGOAL (eresolve_tac rules2)),
```
```   476          EVERY (map (fn prem =>
```
```   477            DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))]))
```
```   478       (mk_elims cs cTs params intr_ts)
```
```   479
```
```   480   in elims end;
```
```   481
```
```   482
```
```   483 (** derivation of simplified elimination rules **)
```
```   484
```
```   485 (*Applies freeness of the given constructors, which *must* be unfolded by
```
```   486   the given defs.  Cannot simply use the local con_defs because con_defs=[]
```
```   487   for inference systems.
```
```   488  *)
```
```   489
```
```   490 (*cprop should have the form t:Si where Si is an inductive set*)
```
```   491 fun mk_cases_i solved elims ss cprop =
```
```   492   let
```
```   493     val prem = Thm.assume cprop;
```
```   494     val tac = if solved then InductMethod.con_elim_solved_tac else InductMethod.con_elim_tac;
```
```   495     fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic (tac ss) (prem RS rl));
```
```   496   in
```
```   497     (case get_first (try mk_elim) elims of
```
```   498       Some r => r
```
```   499     | None => error (Pretty.string_of (Pretty.block
```
```   500         [Pretty.str "mk_cases: proposition not of form 't : S_i'", Pretty.fbrk,
```
```   501           Display.pretty_cterm cprop])))
```
```   502   end;
```
```   503
```
```   504 fun mk_cases elims s =
```
```   505   mk_cases_i false elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT));
```
```   506
```
```   507
```
```   508 (* inductive_cases(_i) *)
```
```   509
```
```   510 fun gen_inductive_cases prep_att prep_const prep_prop
```
```   511     ((((name, raw_atts), raw_set), raw_props), comment) thy =
```
```   512   let
```
```   513     val sign = Theory.sign_of thy;
```
```   514
```
```   515     val atts = map (prep_att thy) raw_atts;
```
```   516     val (_, {elims, ...}) = get_inductive thy (prep_const sign raw_set);
```
```   517     val cprops = map (Thm.cterm_of sign o prep_prop (ProofContext.init thy)) raw_props;
```
```   518     val thms = map (mk_cases_i true elims (Simplifier.simpset_of thy)) cprops;
```
```   519   in
```
```   520     thy
```
```   521     |> IsarThy.have_theorems_i (((name, atts), map Thm.no_attributes thms), comment)
```
```   522   end;
```
```   523
```
```   524 val inductive_cases =
```
```   525   gen_inductive_cases Attrib.global_attribute Sign.intern_const ProofContext.read_prop;
```
```   526
```
```   527 val inductive_cases_i = gen_inductive_cases (K I) (K I) ProofContext.cert_prop;
```
```   528
```
```   529
```
```   530
```
```   531 (** prove induction rule **)
```
```   532
```
```   533 fun prove_indrule cs cTs sumT rec_const params intr_ts mono
```
```   534     fp_def rec_sets_defs thy =
```
```   535   let
```
```   536     val _ = message "  Proving the induction rule ...";
```
```   537
```
```   538     val sign = Theory.sign_of thy;
```
```   539
```
```   540     val sum_case_rewrites = (case ThyInfo.lookup_theory "Datatype" of
```
```   541         None => []
```
```   542       | Some thy' => map mk_meta_eq (PureThy.get_thms thy' "sum.cases"));
```
```   543
```
```   544     val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
```
```   545
```
```   546     (* make predicate for instantiation of abstract induction rule *)
```
```   547
```
```   548     fun mk_ind_pred _ [P] = P
```
```   549       | mk_ind_pred T Ps =
```
```   550          let val n = (length Ps) div 2;
```
```   551              val Type (_, [T1, T2]) = T
```
```   552          in Const ("Datatype.sum.sum_case",
```
```   553            [T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) \$
```
```   554              mk_ind_pred T1 (take (n, Ps)) \$ mk_ind_pred T2 (drop (n, Ps))
```
```   555          end;
```
```   556
```
```   557     val ind_pred = mk_ind_pred sumT preds;
```
```   558
```
```   559     val ind_concl = HOLogic.mk_Trueprop
```
```   560       (HOLogic.all_const sumT \$ Abs ("x", sumT, HOLogic.mk_binop "op -->"
```
```   561         (HOLogic.mk_mem (Bound 0, rec_const), ind_pred \$ Bound 0)));
```
```   562
```
```   563     (* simplification rules for vimage and Collect *)
```
```   564
```
```   565     val vimage_simps = if length cs < 2 then [] else
```
```   566       map (fn c => prove_goalw_cterm [] (cterm_of sign
```
```   567         (HOLogic.mk_Trueprop (HOLogic.mk_eq
```
```   568           (mk_vimage cs sumT (HOLogic.Collect_const sumT \$ ind_pred) c,
```
```   569            HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) \$
```
```   570              nth_elem (find_index_eq c cs, preds)))))
```
```   571         (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites,
```
```   572           rtac refl 1])) cs;
```
```   573
```
```   574     val induct = prove_goalw_cterm [] (cterm_of sign
```
```   575       (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
```
```   576         [rtac (impI RS allI) 1,
```
```   577          DETERM (etac (mono RS (fp_def RS def_induct)) 1),
```
```   578          rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)),
```
```   579          fold_goals_tac rec_sets_defs,
```
```   580          (*This CollectE and disjE separates out the introduction rules*)
```
```   581          REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE, exE])),
```
```   582          (*Now break down the individual cases.  No disjE here in case
```
```   583            some premise involves disjunction.*)
```
```   584          REPEAT (FIRSTGOAL (etac conjE ORELSE' hyp_subst_tac)),
```
```   585          rewrite_goals_tac sum_case_rewrites,
```
```   586          EVERY (map (fn prem =>
```
```   587            DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
```
```   588
```
```   589     val lemma = prove_goalw_cterm rec_sets_defs (cterm_of sign
```
```   590       (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
```
```   591         [cut_facts_tac prems 1,
```
```   592          REPEAT (EVERY
```
```   593            [REPEAT (resolve_tac [conjI, impI] 1),
```
```   594             TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
```
```   595             rewrite_goals_tac sum_case_rewrites,
```
```   596             atac 1])])
```
```   597
```
```   598   in standard (split_rule (induct RS lemma))
```
```   599   end;
```
```   600
```
```   601
```
```   602
```
```   603 (*** specification of (co)inductive sets ****)
```
```   604
```
```   605 (** definitional introduction of (co)inductive sets **)
```
```   606
```
```   607 fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
```
```   608     atts intros monos con_defs thy params paramTs cTs cnames =
```
```   609   let
```
```   610     val _ = if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
```
```   611       commas_quote cnames) else ();
```
```   612
```
```   613     val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
```
```   614     val setT = HOLogic.mk_setT sumT;
```
```   615
```
```   616     val fp_name = if coind then Sign.intern_const (Theory.sign_of Gfp.thy) "gfp"
```
```   617       else Sign.intern_const (Theory.sign_of Lfp.thy) "lfp";
```
```   618
```
```   619     val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
```
```   620
```
```   621     val used = foldr add_term_names (intr_ts, []);
```
```   622     val [sname, xname] = variantlist (["S", "x"], used);
```
```   623
```
```   624     (* transform an introduction rule into a conjunction  *)
```
```   625     (*   [| t : ... S_i ... ; ... |] ==> u : S_j          *)
```
```   626     (* is transformed into                                *)
```
```   627     (*   x = Inj_j u & t : ... Inj_i -`` S ... & ...      *)
```
```   628
```
```   629     fun transform_rule r =
```
```   630       let
```
```   631         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
```
```   632         val subst = subst_free
```
```   633           (cs ~~ (map (mk_vimage cs sumT (Free (sname, setT))) cs));
```
```   634         val Const ("op :", _) \$ t \$ u =
```
```   635           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
```
```   636
```
```   637       in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
```
```   638         (frees, foldr1 HOLogic.mk_conj
```
```   639           (((HOLogic.eq_const sumT) \$ Free (xname, sumT) \$ (mk_inj cs sumT u t))::
```
```   640             (map (subst o HOLogic.dest_Trueprop)
```
```   641               (Logic.strip_imp_prems r))))
```
```   642       end
```
```   643
```
```   644     (* make a disjunction of all introduction rules *)
```
```   645
```
```   646     val fp_fun = absfree (sname, setT, (HOLogic.Collect_const sumT) \$
```
```   647       absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts)));
```
```   648
```
```   649     (* add definiton of recursive sets to theory *)
```
```   650
```
```   651     val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
```
```   652     val full_rec_name = Sign.full_name (Theory.sign_of thy) rec_name;
```
```   653
```
```   654     val rec_const = list_comb
```
```   655       (Const (full_rec_name, paramTs ---> setT), params);
```
```   656
```
```   657     val fp_def_term = Logic.mk_equals (rec_const,
```
```   658       Const (fp_name, (setT --> setT) --> setT) \$ fp_fun)
```
```   659
```
```   660     val def_terms = fp_def_term :: (if length cs < 2 then [] else
```
```   661       map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs);
```
```   662
```
```   663     val thy' = thy |>
```
```   664       (if declare_consts then
```
```   665         Theory.add_consts_i (map (fn (c, n) =>
```
```   666           (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
```
```   667        else I) |>
```
```   668       (if length cs < 2 then I else
```
```   669        Theory.add_consts_i [(rec_name, paramTs ---> setT, NoSyn)]) |>
```
```   670       Theory.add_path rec_name |>
```
```   671       PureThy.add_defss_i [(("defs", def_terms), [])];
```
```   672
```
```   673     (* get definitions from theory *)
```
```   674
```
```   675     val fp_def::rec_sets_defs = PureThy.get_thms thy' "defs";
```
```   676
```
```   677     (* prove and store theorems *)
```
```   678
```
```   679     val mono = prove_mono setT fp_fun monos thy';
```
```   680     val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts con_defs
```
```   681       rec_sets_defs thy';
```
```   682     val elims = if no_elim then [] else
```
```   683       prove_elims cs cTs params intr_ts unfold rec_sets_defs thy';
```
```   684     val raw_induct = if no_ind then Drule.asm_rl else
```
```   685       if coind then standard (rule_by_tactic
```
```   686         (rewrite_tac [mk_meta_eq vimage_Un] THEN
```
```   687           fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct)))
```
```   688       else
```
```   689         prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def
```
```   690           rec_sets_defs thy';
```
```   691     val induct = if coind orelse no_ind orelse length cs > 1 then raw_induct
```
```   692       else standard (raw_induct RSN (2, rev_mp));
```
```   693
```
```   694     val thy'' = thy'
```
```   695       |> PureThy.add_thmss [(("intrs", intrs), atts)]
```
```   696       |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts)
```
```   697       |> (if no_elim then I else PureThy.add_thmss [(("elims", elims), [])])
```
```   698       |> (if no_ind then I else PureThy.add_thms
```
```   699         [((coind_prefix coind ^ "induct", induct), [])])
```
```   700       |> Theory.parent_path;
```
```   701     val intrs' = PureThy.get_thms thy'' "intrs";
```
```   702     val elims' = if no_elim then elims else PureThy.get_thms thy'' "elims";  (* FIXME improve *)
```
```   703     val induct' = if no_ind then induct else PureThy.get_thm thy'' (coind_prefix coind ^ "induct");  (* FIXME improve *)
```
```   704   in (thy'',
```
```   705     {defs = fp_def::rec_sets_defs,
```
```   706      mono = mono,
```
```   707      unfold = unfold,
```
```   708      intrs = intrs',
```
```   709      elims = elims',
```
```   710      mk_cases = mk_cases elims',
```
```   711      raw_induct = raw_induct,
```
```   712      induct = induct'})
```
```   713   end;
```
```   714
```
```   715
```
```   716
```
```   717 (** axiomatic introduction of (co)inductive sets **)
```
```   718
```
```   719 fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs
```
```   720     atts intros monos con_defs thy params paramTs cTs cnames =
```
```   721   let
```
```   722     val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
```
```   723
```
```   724     val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
```
```   725     val elim_ts = mk_elims cs cTs params intr_ts;
```
```   726
```
```   727     val (_, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
```
```   728     val ind_t = Logic.list_implies (ind_prems, mutual_ind_concl);
```
```   729
```
```   730     val thy' = thy
```
```   731       |> (if declare_consts then
```
```   732             Theory.add_consts_i
```
```   733               (map (fn (c, n) => (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
```
```   734          else I)
```
```   735       |> Theory.add_path rec_name
```
```   736       |> PureThy.add_axiomss_i [(("intrs", intr_ts), atts), (("elims", elim_ts), [])]
```
```   737       |> (if coind then I else
```
```   738             PureThy.add_axioms_i [(("raw_induct", ind_t), [apsnd (standard o split_rule)])]);
```
```   739
```
```   740     val intrs = PureThy.get_thms thy' "intrs";
```
```   741     val elims = PureThy.get_thms thy' "elims";
```
```   742     val raw_induct = if coind then Drule.asm_rl else PureThy.get_thm thy' "raw_induct";
```
```   743     val induct = if coind orelse length cs > 1 then raw_induct
```
```   744       else standard (raw_induct RSN (2, rev_mp));
```
```   745
```
```   746     val thy'' =
```
```   747       thy'
```
```   748       |> (if coind then I else PureThy.add_thms [(("induct", induct), [])])
```
```   749       |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts)
```
```   750       |> Theory.parent_path;
```
```   751     val induct' = if coind then raw_induct else PureThy.get_thm thy'' "induct";
```
```   752   in (thy'',
```
```   753     {defs = [],
```
```   754      mono = Drule.asm_rl,
```
```   755      unfold = Drule.asm_rl,
```
```   756      intrs = intrs,
```
```   757      elims = elims,
```
```   758      mk_cases = mk_cases elims,
```
```   759      raw_induct = raw_induct,
```
```   760      induct = induct'})
```
```   761   end;
```
```   762
```
```   763
```
```   764
```
```   765 (** introduction of (co)inductive sets **)
```
```   766
```
```   767 fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs
```
```   768     atts intros monos con_defs thy =
```
```   769   let
```
```   770     val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
```
```   771     val sign = Theory.sign_of thy;
```
```   772
```
```   773     (*parameters should agree for all mutually recursive components*)
```
```   774     val (_, params) = strip_comb (hd cs);
```
```   775     val paramTs = map (try' (snd o dest_Free) "Parameter in recursive\
```
```   776       \ component is not a free variable: " sign) params;
```
```   777
```
```   778     val cTs = map (try' (HOLogic.dest_setT o fastype_of)
```
```   779       "Recursive component not of type set: " sign) cs;
```
```   780
```
```   781     val full_cnames = map (try' (fst o dest_Const o head_of)
```
```   782       "Recursive set not previously declared as constant: " sign) cs;
```
```   783     val cnames = map Sign.base_name full_cnames;
```
```   784
```
```   785     val _ = seq (check_rule sign cs o snd o fst) intros;
```
```   786
```
```   787     val (thy1, result) =
```
```   788       (if ! quick_and_dirty then add_ind_axm else add_ind_def)
```
```   789         verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos
```
```   790         con_defs thy params paramTs cTs cnames;
```
```   791     val thy2 = thy1
```
```   792       |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result)
```
```   793       |> add_cases_induct no_elim no_ind full_cnames (#elims result) (#induct result);
```
```   794   in (thy2, result) end;
```
```   795
```
```   796
```
```   797
```
```   798 (** external interface **)
```
```   799
```
```   800 fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy =
```
```   801   let
```
```   802     val sign = Theory.sign_of thy;
```
```   803     val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings;
```
```   804
```
```   805     val atts = map (Attrib.global_attribute thy) srcs;
```
```   806     val intr_names = map (fst o fst) intro_srcs;
```
```   807     val intr_ts = map (term_of o Thm.read_cterm sign o rpair propT o snd o fst) intro_srcs;
```
```   808     val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
```
```   809     val (cs', intr_ts') = unify_consts sign cs intr_ts;
```
```   810
```
```   811     val ((thy', con_defs), monos) = thy
```
```   812       |> IsarThy.apply_theorems raw_monos
```
```   813       |> apfst (IsarThy.apply_theorems raw_con_defs);
```
```   814   in
```
```   815     add_inductive_i verbose false "" coind false false cs'
```
```   816       atts ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy'
```
```   817   end;
```
```   818
```
```   819
```
```   820
```
```   821 (** package setup **)
```
```   822
```
```   823 (* setup theory *)
```
```   824
```
```   825 val setup = [InductiveData.init,
```
```   826              Attrib.add_attributes [(monoN, mono_attr, "monotonicity rule")]];
```
```   827
```
```   828
```
```   829 (* outer syntax *)
```
```   830
```
```   831 local structure P = OuterParse and K = OuterSyntax.Keyword in
```
```   832
```
```   833 fun mk_ind coind (((sets, (atts, intrs)), monos), con_defs) =
```
```   834   #1 o add_inductive true coind sets atts (map P.triple_swap intrs) monos con_defs;
```
```   835
```
```   836 fun ind_decl coind =
```
```   837   (Scan.repeat1 P.term --| P.marg_comment) --
```
```   838   (P.\$\$\$ "intrs" |--
```
```   839     P.!!! (P.opt_attribs -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) --
```
```   840   Scan.optional (P.\$\$\$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
```
```   841   Scan.optional (P.\$\$\$ "con_defs" |-- P.!!! P.xthms1 --| P.marg_comment) []
```
```   842   >> (Toplevel.theory o mk_ind coind);
```
```   843
```
```   844 val inductiveP =
```
```   845   OuterSyntax.command "inductive" "define inductive sets" K.thy_decl (ind_decl false);
```
```   846
```
```   847 val coinductiveP =
```
```   848   OuterSyntax.command "coinductive" "define coinductive sets" K.thy_decl (ind_decl true);
```
```   849
```
```   850
```
```   851 val ind_cases =
```
```   852   P.opt_thm_name "=" -- P.xname --| P.\$\$\$ ":" -- Scan.repeat1 P.prop -- P.marg_comment
```
```   853   >> (Toplevel.theory o inductive_cases);
```
```   854
```
```   855 val inductive_casesP =
```
```   856   OuterSyntax.command "inductive_cases" "create simplified instances of elimination rules"
```
```   857     K.thy_decl ind_cases;
```
```   858
```
```   859 val _ = OuterSyntax.add_keywords ["intrs", "monos", "con_defs"];
```
```   860 val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP];
```
```   861
```
```   862 end;
```
```   863
```
```   864
```
```   865 end;
```