src/HOL/Tools/inductive_package.ML
 author paulson Fri Oct 20 11:04:15 2006 +0200 (2006-10-20 ago) changeset 21070 0a898140fea2 parent 21048 e57e91f72831 child 21350 6e58289b6685 permissions -rw-r--r--
```     1 (*  Title:      HOL/Tools/inductive_package.ML
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Author:     Stefan Berghofer, TU Muenchen
```
```     5     Author:     Markus Wenzel, TU Muenchen
```
```     6
```
```     7 (Co)Inductive Definition module for HOL.
```
```     8
```
```     9 Features:
```
```    10   * least or greatest fixedpoints
```
```    11   * mutually recursive definitions
```
```    12   * definitions involving arbitrary monotone operators
```
```    13   * automatically proves introduction and elimination rules
```
```    14
```
```    15   Introduction rules have the form
```
```    16   [| M Pj ti, ..., Q x, ... |] ==> Pk t
```
```    17   where M is some monotone operator (usually the identity)
```
```    18   Q x is any side condition on the free variables
```
```    19   ti, t are any terms
```
```    20   Pj, Pk are two of the predicates being defined in mutual recursion
```
```    21 *)
```
```    22
```
```    23 signature INDUCTIVE_PACKAGE =
```
```    24 sig
```
```    25   val quiet_mode: bool ref
```
```    26   val trace: bool ref
```
```    27   type inductive_result
```
```    28   type inductive_info
```
```    29   val get_inductive: Context.generic -> string -> inductive_info option
```
```    30   val the_mk_cases: Context.generic -> string -> string -> thm
```
```    31   val print_inductives: Context.generic -> unit
```
```    32   val mono_add: attribute
```
```    33   val mono_del: attribute
```
```    34   val get_monos: Context.generic -> thm list
```
```    35   val inductive_forall_name: string
```
```    36   val inductive_forall_def: thm
```
```    37   val rulify: thm -> thm
```
```    38   val inductive_cases: ((bstring * Attrib.src list) * string list) list -> theory -> theory
```
```    39   val inductive_cases_i: ((bstring * attribute list) * term list) list -> theory -> theory
```
```    40   val add_inductive_i: bool -> bstring -> bool -> bool -> bool -> (string * typ option * mixfix) list ->
```
```    41     (string * typ option) list -> ((bstring * Attrib.src list) * term) list -> thm list ->
```
```    42       local_theory -> local_theory * inductive_result
```
```    43   val add_inductive: bool -> bool -> (string * string option * mixfix) list ->
```
```    44     (string * string option * mixfix) list ->
```
```    45     ((bstring * Attrib.src list) * string) list -> (thmref * Attrib.src list) list ->
```
```    46     local_theory -> local_theory * inductive_result
```
```    47   val setup: theory -> theory
```
```    48 end;
```
```    49
```
```    50 structure InductivePackage: INDUCTIVE_PACKAGE =
```
```    51 struct
```
```    52
```
```    53
```
```    54 (** theory context references **)
```
```    55
```
```    56 val mono_name = "Orderings.mono";
```
```    57 val gfp_name = "FixedPoint.gfp";
```
```    58 val lfp_name = "FixedPoint.lfp";
```
```    59
```
```    60 val inductive_forall_name = "HOL.induct_forall";
```
```    61 val inductive_forall_def = thm "induct_forall_def";
```
```    62 val inductive_conj_name = "HOL.induct_conj";
```
```    63 val inductive_conj_def = thm "induct_conj_def";
```
```    64 val inductive_conj = thms "induct_conj";
```
```    65 val inductive_atomize = thms "induct_atomize";
```
```    66 val inductive_rulify = thms "induct_rulify";
```
```    67 val inductive_rulify_fallback = thms "induct_rulify_fallback";
```
```    68
```
```    69 val notTrueE = TrueI RSN (2, notE);
```
```    70 val notFalseI = Seq.hd (atac 1 notI);
```
```    71 val simp_thms' = map (fn s => mk_meta_eq (the (find_first
```
```    72   (equal (term_of (read_cterm HOL.thy (s, propT))) o prop_of) simp_thms)))
```
```    73   ["(~True) = False", "(~False) = True",
```
```    74    "(True --> ?P) = ?P", "(False --> ?P) = True",
```
```    75    "(?P & True) = ?P", "(True & ?P) = ?P"];
```
```    76
```
```    77
```
```    78
```
```    79 (** theory data **)
```
```    80
```
```    81 type inductive_result =
```
```    82   {preds: term list, defs: thm list, elims: thm list, raw_induct: thm,
```
```    83    induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm};
```
```    84
```
```    85 type inductive_info =
```
```    86   {names: string list, coind: bool} * inductive_result;
```
```    87
```
```    88 structure InductiveData = GenericDataFun
```
```    89 (struct
```
```    90   val name = "HOL/inductive2";
```
```    91   type T = inductive_info Symtab.table * thm list;
```
```    92
```
```    93   val empty = (Symtab.empty, []);
```
```    94   val extend = I;
```
```    95   fun merge _ ((tab1, monos1), (tab2, monos2)) =
```
```    96     (Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2));
```
```    97
```
```    98   fun print generic (tab, monos) =
```
```    99     [Pretty.strs ("(co)inductives:" ::
```
```   100       map #1 (NameSpace.extern_table
```
```   101         (Sign.const_space (Context.theory_of generic), tab))),  (* FIXME? *)
```
```   102      Pretty.big_list "monotonicity rules:"
```
```   103         (map (ProofContext.pretty_thm (Context.proof_of generic)) monos)]
```
```   104     |> Pretty.chunks |> Pretty.writeln;
```
```   105 end);
```
```   106
```
```   107 val print_inductives = InductiveData.print;
```
```   108
```
```   109
```
```   110 (* get and put data *)
```
```   111
```
```   112 val get_inductive = Symtab.lookup o #1 o InductiveData.get;
```
```   113
```
```   114 fun the_inductive thy name =
```
```   115   (case get_inductive thy name of
```
```   116     NONE => error ("Unknown (co)inductive predicate " ^ quote name)
```
```   117   | SOME info => info);
```
```   118
```
```   119 val the_mk_cases = (#mk_cases o #2) oo the_inductive;
```
```   120
```
```   121 fun put_inductives names info = InductiveData.map (apfst (fn tab =>
```
```   122   fold (fn name => Symtab.update_new (name, info)) names tab
```
```   123     handle Symtab.DUP dup => error ("Duplicate definition of (co)inductive predicate " ^ quote dup)));
```
```   124
```
```   125
```
```   126
```
```   127 (** monotonicity rules **)
```
```   128
```
```   129 val get_monos = #2 o InductiveData.get;
```
```   130 val map_monos = InductiveData.map o Library.apsnd;
```
```   131
```
```   132 fun mk_mono thm =
```
```   133   let
```
```   134     fun eq2mono thm' = [(*standard*) (thm' RS (thm' RS eq_to_mono))] @
```
```   135       (case concl_of thm of
```
```   136           (_ \$ (_ \$ (Const ("Not", _) \$ _) \$ _)) => []
```
```   137         | _ => [(*standard*) (thm' RS (thm' RS eq_to_mono2))]);
```
```   138     val concl = concl_of thm
```
```   139   in
```
```   140     if can Logic.dest_equals concl then
```
```   141       eq2mono (thm RS meta_eq_to_obj_eq)
```
```   142     else if can (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl then
```
```   143       eq2mono thm
```
```   144     else [thm]
```
```   145   end;
```
```   146
```
```   147
```
```   148 (* attributes *)
```
```   149
```
```   150 val mono_add = Thm.declaration_attribute (fn th =>
```
```   151   map_monos (fold Drule.add_rule (mk_mono th)));
```
```   152
```
```   153 val mono_del = Thm.declaration_attribute (fn th =>
```
```   154   map_monos (fold Drule.del_rule (mk_mono th)));
```
```   155
```
```   156
```
```   157
```
```   158 (** misc utilities **)
```
```   159
```
```   160 val quiet_mode = ref false;
```
```   161 val trace = ref false;  (*for debugging*)
```
```   162 fun message s = if ! quiet_mode then () else writeln s;
```
```   163 fun clean_message s = if ! quick_and_dirty then () else message s;
```
```   164
```
```   165 fun coind_prefix true = "co"
```
```   166   | coind_prefix false = "";
```
```   167
```
```   168 fun log b m n = if m >= n then 0 else 1 + log b (b * m) n;
```
```   169
```
```   170 fun make_bool_args f g [] i = []
```
```   171   | make_bool_args f g (x :: xs) i =
```
```   172       (if i mod 2 = 0 then f x else g x) :: make_bool_args f g xs (i div 2);
```
```   173
```
```   174 fun make_bool_args' xs =
```
```   175   make_bool_args (K HOLogic.false_const) (K HOLogic.true_const) xs;
```
```   176
```
```   177 fun find_arg T x [] = sys_error "find_arg"
```
```   178   | find_arg T x ((p as (_, (SOME _, _))) :: ps) =
```
```   179       apsnd (cons p) (find_arg T x ps)
```
```   180   | find_arg T x ((p as (U, (NONE, y))) :: ps) =
```
```   181       if T = U then (y, (U, (SOME x, y)) :: ps)
```
```   182       else apsnd (cons p) (find_arg T x ps);
```
```   183
```
```   184 fun make_args Ts xs =
```
```   185   map (fn (T, (NONE, ())) => Const ("arbitrary", T) | (_, (SOME t, ())) => t)
```
```   186     (fold (fn (t, T) => snd o find_arg T t) xs (map (rpair (NONE, ())) Ts));
```
```   187
```
```   188 fun make_args' Ts xs Us =
```
```   189   fst (fold_map (fn T => find_arg T ()) Us (Ts ~~ map (pair NONE) xs));
```
```   190
```
```   191 fun dest_predicate cs params t =
```
```   192   let
```
```   193     val k = length params;
```
```   194     val (c, ts) = strip_comb t;
```
```   195     val (xs, ys) = chop k ts;
```
```   196     val i = find_index_eq c cs;
```
```   197   in
```
```   198     if xs = params andalso i >= 0 then
```
```   199       SOME (c, i, ys, chop (length ys)
```
```   200         (List.drop (binder_types (fastype_of c), k)))
```
```   201     else NONE
```
```   202   end;
```
```   203
```
```   204 fun mk_names a 0 = []
```
```   205   | mk_names a 1 = [a]
```
```   206   | mk_names a n = map (fn i => a ^ string_of_int i) (1 upto n);
```
```   207
```
```   208
```
```   209
```
```   210 (** process rules **)
```
```   211
```
```   212 local
```
```   213
```
```   214 fun err_in_rule thy name t msg =
```
```   215   error (cat_lines ["Ill-formed introduction rule " ^ quote name,
```
```   216     Sign.string_of_term thy t, msg]);
```
```   217
```
```   218 fun err_in_prem thy name t p msg =
```
```   219   error (cat_lines ["Ill-formed premise", Sign.string_of_term thy p,
```
```   220     "in introduction rule " ^ quote name, Sign.string_of_term thy t, msg]);
```
```   221
```
```   222 val bad_concl = "Conclusion of introduction rule must be an inductive predicate";
```
```   223
```
```   224 val bad_ind_occ = "Inductive predicate occurs in argument of inductive predicate";
```
```   225
```
```   226 val bad_app = "Inductive predicate must be applied to parameter(s) ";
```
```   227
```
```   228 fun atomize_term thy = MetaSimplifier.rewrite_term thy inductive_atomize [];
```
```   229
```
```   230 in
```
```   231
```
```   232 fun check_rule thy cs params ((name, att), rule) =
```
```   233   let
```
```   234     val params' = Term.variant_frees rule (Logic.strip_params rule);
```
```   235     val frees = rev (map Free params');
```
```   236     val concl = subst_bounds (frees, Logic.strip_assums_concl rule);
```
```   237     val prems = map (curry subst_bounds frees) (Logic.strip_assums_hyp rule);
```
```   238     val aprems = map (atomize_term thy) prems;
```
```   239     val arule = list_all_free (params', Logic.list_implies (aprems, concl));
```
```   240
```
```   241     fun check_ind err t = case dest_predicate cs params t of
```
```   242         NONE => err (bad_app ^
```
```   243           commas (map (Sign.string_of_term thy) params))
```
```   244       | SOME (_, _, ys, _) =>
```
```   245           if exists (fn c => exists (fn t => Logic.occs (c, t)) ys) cs
```
```   246           then err bad_ind_occ else ();
```
```   247
```
```   248     fun check_prem' prem t =
```
```   249       if head_of t mem cs then
```
```   250         check_ind (err_in_prem thy name rule prem) t
```
```   251       else (case t of
```
```   252           Abs (_, _, t) => check_prem' prem t
```
```   253         | t \$ u => (check_prem' prem t; check_prem' prem u)
```
```   254         | _ => ());
```
```   255
```
```   256     fun check_prem (prem, aprem) =
```
```   257       if can HOLogic.dest_Trueprop aprem then check_prem' prem prem
```
```   258       else err_in_prem thy name rule prem "Non-atomic premise";
```
```   259   in
```
```   260     (case concl of
```
```   261        Const ("Trueprop", _) \$ t =>
```
```   262          if head_of t mem cs then
```
```   263            (check_ind (err_in_rule thy name rule) t;
```
```   264             List.app check_prem (prems ~~ aprems))
```
```   265          else err_in_rule thy name rule bad_concl
```
```   266      | _ => err_in_rule thy name rule bad_concl);
```
```   267     ((name, att), arule)
```
```   268   end;
```
```   269
```
```   270 val rulify =  (* FIXME norm_hhf *)
```
```   271   hol_simplify inductive_conj
```
```   272   #> hol_simplify inductive_rulify
```
```   273   #> hol_simplify inductive_rulify_fallback
```
```   274   (*#> standard*);
```
```   275
```
```   276 end;
```
```   277
```
```   278
```
```   279
```
```   280 (** proofs for (co)inductive predicates **)
```
```   281
```
```   282 (* prove monotonicity -- NOT subject to quick_and_dirty! *)
```
```   283
```
```   284 fun prove_mono predT fp_fun monos ctxt =
```
```   285  (message "  Proving monotonicity ...";
```
```   286   Goal.prove ctxt [] []   (*NO quick_and_dirty here!*)
```
```   287     (HOLogic.mk_Trueprop
```
```   288       (Const (mono_name, (predT --> predT) --> HOLogic.boolT) \$ fp_fun))
```
```   289     (fn _ => EVERY [rtac monoI 1,
```
```   290       REPEAT (resolve_tac [le_funI, le_boolI'] 1),
```
```   291       REPEAT (FIRST
```
```   292         [atac 1,
```
```   293          resolve_tac (List.concat (map mk_mono monos) @
```
```   294            get_monos (Context.Proof ctxt)) 1,
```
```   295          etac le_funE 1, dtac le_boolD 1])]));
```
```   296
```
```   297
```
```   298 (* prove introduction rules *)
```
```   299
```
```   300 fun prove_intrs coind mono fp_def k intr_ts rec_preds_defs ctxt =
```
```   301   let
```
```   302     val _ = clean_message "  Proving the introduction rules ...";
```
```   303
```
```   304     val unfold = funpow k (fn th => th RS fun_cong)
```
```   305       (mono RS (fp_def RS
```
```   306         (if coind then def_gfp_unfold else def_lfp_unfold)));
```
```   307
```
```   308     fun select_disj 1 1 = []
```
```   309       | select_disj _ 1 = [rtac disjI1]
```
```   310       | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
```
```   311
```
```   312     val rules = [refl, TrueI, notFalseI, exI, conjI];
```
```   313
```
```   314     val intrs = map_index (fn (i, intr) =>
```
```   315       rulify (SkipProof.prove ctxt [] [] intr (fn _ => EVERY
```
```   316        [rewrite_goals_tac rec_preds_defs,
```
```   317         rtac (unfold RS iffD2) 1,
```
```   318         EVERY1 (select_disj (length intr_ts) (i + 1)),
```
```   319         (*Not ares_tac, since refl must be tried before any equality assumptions;
```
```   320           backtracking may occur if the premises have extra variables!*)
```
```   321         DEPTH_SOLVE_1 (resolve_tac rules 1 APPEND assume_tac 1)]))) intr_ts
```
```   322
```
```   323   in (intrs, unfold) end;
```
```   324
```
```   325
```
```   326 (* prove elimination rules *)
```
```   327
```
```   328 fun prove_elims cs params intr_ts intr_names unfold rec_preds_defs ctxt =
```
```   329   let
```
```   330     val _ = clean_message "  Proving the elimination rules ...";
```
```   331
```
```   332     val ([pname], ctxt') = Variable.variant_fixes ["P"] ctxt;
```
```   333     val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
```
```   334
```
```   335     fun dest_intr r =
```
```   336       (the (dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))),
```
```   337        Logic.strip_assums_hyp r, Logic.strip_params r);
```
```   338
```
```   339     val intrs = map dest_intr intr_ts ~~ intr_names;
```
```   340
```
```   341     val rules1 = [disjE, exE, FalseE];
```
```   342     val rules2 = [conjE, FalseE, notTrueE];
```
```   343
```
```   344     fun prove_elim c =
```
```   345       let
```
```   346         val Ts = List.drop (binder_types (fastype_of c), length params);
```
```   347         val (anames, ctxt'') = Variable.variant_fixes (mk_names "a" (length Ts)) ctxt';
```
```   348         val frees = map Free (anames ~~ Ts);
```
```   349
```
```   350         fun mk_elim_prem ((_, _, us, _), ts, params') =
```
```   351           list_all (params',
```
```   352             Logic.list_implies (map (HOLogic.mk_Trueprop o HOLogic.mk_eq)
```
```   353               (frees ~~ us) @ ts, P));
```
```   354         val c_intrs = (List.filter (equal c o #1 o #1 o #1) intrs);
```
```   355         val prems = HOLogic.mk_Trueprop (list_comb (c, params @ frees)) ::
```
```   356            map mk_elim_prem (map #1 c_intrs)
```
```   357       in
```
```   358         (SkipProof.prove ctxt'' [] prems P
```
```   359           (fn {prems, ...} => EVERY
```
```   360             [cut_facts_tac [hd prems] 1,
```
```   361              rewrite_goals_tac rec_preds_defs,
```
```   362              dtac (unfold RS iffD1) 1,
```
```   363              REPEAT (FIRSTGOAL (eresolve_tac rules1)),
```
```   364              REPEAT (FIRSTGOAL (eresolve_tac rules2)),
```
```   365              EVERY (map (fn prem =>
```
```   366                DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_preds_defs prem, conjI] 1)) (tl prems))])
```
```   367           |> rulify
```
```   368           |> singleton (ProofContext.export ctxt'' ctxt),
```
```   369          map #2 c_intrs)
```
```   370       end
```
```   371
```
```   372    in map prove_elim cs end;
```
```   373
```
```   374
```
```   375 (* derivation of simplified elimination rules *)
```
```   376
```
```   377 local
```
```   378
```
```   379 (*cprop should have the form "Si t" where Si is an inductive predicate*)
```
```   380 val mk_cases_err = "mk_cases: proposition not an inductive predicate";
```
```   381
```
```   382 (*delete needless equality assumptions*)
```
```   383 val refl_thin = prove_goal HOL.thy "!!P. a = a ==> P ==> P" (fn _ => [assume_tac 1]);
```
```   384 val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE];
```
```   385 val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
```
```   386
```
```   387 fun simp_case_tac solved ss i =
```
```   388   EVERY' [elim_tac, asm_full_simp_tac ss, elim_tac, REPEAT o bound_hyp_subst_tac] i
```
```   389   THEN_MAYBE (if solved then no_tac else all_tac);
```
```   390
```
```   391 in
```
```   392
```
```   393 fun mk_cases_i elims ss cprop =
```
```   394   let
```
```   395     val prem = Thm.assume cprop;
```
```   396     val tac = ALLGOALS (simp_case_tac false ss) THEN prune_params_tac;
```
```   397     fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic tac (prem RS rl));
```
```   398   in
```
```   399     (case get_first (try mk_elim) elims of
```
```   400       SOME r => r
```
```   401     | NONE => error (Pretty.string_of (Pretty.block
```
```   402         [Pretty.str mk_cases_err, Pretty.fbrk, Display.pretty_cterm cprop])))
```
```   403   end;
```
```   404
```
```   405 fun mk_cases elims s =
```
```   406   mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.theory_of_thm (hd elims)) (s, propT));
```
```   407
```
```   408 fun smart_mk_cases ctxt ss cprop =
```
```   409   let
```
```   410     val c = #1 (Term.dest_Const (Term.head_of (HOLogic.dest_Trueprop
```
```   411       (Logic.strip_imp_concl (Thm.term_of cprop))))) handle TERM _ => error mk_cases_err;
```
```   412     val (_, {elims, ...}) = the_inductive ctxt c;
```
```   413   in mk_cases_i elims ss cprop end;
```
```   414
```
```   415 end;
```
```   416
```
```   417
```
```   418 (* inductive_cases(_i) *)
```
```   419
```
```   420 fun gen_inductive_cases prep_att prep_prop args thy =
```
```   421   let
```
```   422     val cert_prop = Thm.cterm_of thy o prep_prop (ProofContext.init thy);
```
```   423     val mk_cases = smart_mk_cases (Context.Theory thy) (Simplifier.simpset_of thy) o cert_prop;
```
```   424
```
```   425     val facts = args |> map (fn ((a, atts), props) =>
```
```   426      ((a, map (prep_att thy) atts), map (Thm.no_attributes o single o mk_cases) props));
```
```   427   in thy |> PureThy.note_thmss_i "" facts |> snd end;
```
```   428
```
```   429 val inductive_cases = gen_inductive_cases Attrib.attribute ProofContext.read_prop;
```
```   430 val inductive_cases_i = gen_inductive_cases (K I) ProofContext.cert_prop;
```
```   431
```
```   432
```
```   433 (* mk_cases_meth *)
```
```   434
```
```   435 fun mk_cases_meth (ctxt, raw_props) =
```
```   436   let
```
```   437     val thy = ProofContext.theory_of ctxt;
```
```   438     val ss = local_simpset_of ctxt;
```
```   439     val cprops = map (Thm.cterm_of thy o ProofContext.read_prop ctxt) raw_props;
```
```   440   in Method.erule 0 (map (smart_mk_cases (Context.Theory thy) ss) cprops) end;
```
```   441
```
```   442 val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name));
```
```   443
```
```   444
```
```   445 (* prove induction rule *)
```
```   446
```
```   447 fun prove_indrule cs argTs bs xs rec_const params intr_ts mono
```
```   448     fp_def rec_preds_defs ctxt =
```
```   449   let
```
```   450     val _ = clean_message "  Proving the induction rule ...";
```
```   451     val thy = ProofContext.theory_of ctxt;
```
```   452
```
```   453     (* predicates for induction rule *)
```
```   454
```
```   455     val (pnames, ctxt') = Variable.variant_fixes (mk_names "P" (length cs)) ctxt;
```
```   456     val preds = map Free (pnames ~~
```
```   457       map (fn c => List.drop (binder_types (fastype_of c), length params) --->
```
```   458         HOLogic.boolT) cs);
```
```   459
```
```   460     (* transform an introduction rule into a premise for induction rule *)
```
```   461
```
```   462     fun mk_ind_prem r =
```
```   463       let
```
```   464         fun subst s = (case dest_predicate cs params s of
```
```   465             SOME (_, i, ys, (_, Ts)) =>
```
```   466               let
```
```   467                 val k = length Ts;
```
```   468                 val bs = map Bound (k - 1 downto 0);
```
```   469                 val P = list_comb (List.nth (preds, i), ys @ bs);
```
```   470                 val Q = list_abs (mk_names "x" k ~~ Ts,
```
```   471                   HOLogic.mk_binop inductive_conj_name (list_comb (s, bs), P))
```
```   472               in (Q, case Ts of [] => SOME (s, P) | _ => NONE) end
```
```   473           | NONE => (case s of
```
```   474               (t \$ u) => (fst (subst t) \$ fst (subst u), NONE)
```
```   475             | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), NONE)
```
```   476             | _ => (s, NONE)));
```
```   477
```
```   478         fun mk_prem (s, prems) = (case subst s of
```
```   479               (_, SOME (t, u)) => t :: u :: prems
```
```   480             | (t, _) => t :: prems);
```
```   481
```
```   482         val SOME (_, i, ys, _) = dest_predicate cs params
```
```   483           (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))
```
```   484
```
```   485       in list_all_free (Logic.strip_params r,
```
```   486         Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem
```
```   487           [] (map HOLogic.dest_Trueprop (Logic.strip_assums_hyp r))),
```
```   488             HOLogic.mk_Trueprop (list_comb (List.nth (preds, i), ys))))
```
```   489       end;
```
```   490
```
```   491     val ind_prems = map mk_ind_prem intr_ts;
```
```   492
```
```   493     (* make conclusions for induction rules *)
```
```   494
```
```   495     val Tss = map (binder_types o fastype_of) preds;
```
```   496     val (xnames, ctxt'') =
```
```   497       Variable.variant_fixes (mk_names "x" (length (flat Tss))) ctxt';
```
```   498     val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
```
```   499         (map (fn (((xnames, Ts), c), P) =>
```
```   500            let val frees = map Free (xnames ~~ Ts)
```
```   501            in HOLogic.mk_imp
```
```   502              (list_comb (c, params @ frees), list_comb (P, frees))
```
```   503            end) (unflat Tss xnames ~~ Tss ~~ cs ~~ preds)));
```
```   504
```
```   505     val dummy = if !trace then
```
```   506                 (writeln "ind_prems = ";
```
```   507                  List.app (writeln o Sign.string_of_term thy) ind_prems)
```
```   508             else ();
```
```   509
```
```   510     (* make predicate for instantiation of abstract induction rule *)
```
```   511
```
```   512     val ind_pred = fold_rev lambda (bs @ xs) (foldr1 HOLogic.mk_conj
```
```   513       (map_index (fn (i, P) => foldr HOLogic.mk_imp
```
```   514          (list_comb (P, make_args' argTs xs (binder_types (fastype_of P))))
```
```   515          (make_bool_args HOLogic.mk_not I bs i)) preds));
```
```   516
```
```   517     val ind_concl = HOLogic.mk_Trueprop
```
```   518       (HOLogic.mk_binrel "Orderings.less_eq" (rec_const, ind_pred));
```
```   519
```
```   520     val raw_fp_induct = (mono RS (fp_def RS def_lfp_induct));
```
```   521
```
```   522     val dummy = if !trace then
```
```   523                 (writeln "raw_fp_induct = "; print_thm raw_fp_induct)
```
```   524             else ();
```
```   525
```
```   526     val induct = SkipProof.prove ctxt'' [] ind_prems ind_concl
```
```   527       (fn {prems, ...} => EVERY
```
```   528         [rewrite_goals_tac [inductive_conj_def],
```
```   529          DETERM (rtac raw_fp_induct 1),
```
```   530          REPEAT (resolve_tac [le_funI, le_boolI] 1),
```
```   531          rewrite_goals_tac (map mk_meta_eq [meet_fun_eq, meet_bool_eq] @ simp_thms'),
```
```   532          (*This disjE separates out the introduction rules*)
```
```   533          REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])),
```
```   534          (*Now break down the individual cases.  No disjE here in case
```
```   535            some premise involves disjunction.*)
```
```   536          REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac)),
```
```   537          REPEAT (FIRSTGOAL
```
```   538            (resolve_tac [conjI, impI] ORELSE' (etac notE THEN' atac))),
```
```   539          EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule
```
```   540            (inductive_conj_def :: rec_preds_defs) prem, conjI, refl] 1)) prems)]);
```
```   541
```
```   542     val lemma = SkipProof.prove ctxt'' [] []
```
```   543       (Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn _ => EVERY
```
```   544         [rewrite_goals_tac rec_preds_defs,
```
```   545          REPEAT (EVERY
```
```   546            [REPEAT (resolve_tac [conjI, impI] 1),
```
```   547             REPEAT (eresolve_tac [le_funE, le_boolE] 1),
```
```   548             atac 1,
```
```   549             rewrite_goals_tac simp_thms',
```
```   550             atac 1])])
```
```   551
```
```   552   in singleton (ProofContext.export ctxt'' ctxt) (induct RS lemma) end;
```
```   553
```
```   554
```
```   555
```
```   556 (** specification of (co)inductive predicates **)
```
```   557
```
```   558 fun mk_ind_def alt_name coind cs intr_ts monos
```
```   559       params cnames_syn ctxt =
```
```   560   let
```
```   561     val fp_name = if coind then gfp_name else lfp_name;
```
```   562
```
```   563     val argTs = fold (fn c => fn Ts => Ts @
```
```   564       (List.drop (binder_types (fastype_of c), length params) \\ Ts)) cs [];
```
```   565     val k = log 2 1 (length cs);
```
```   566     val predT = replicate k HOLogic.boolT ---> argTs ---> HOLogic.boolT;
```
```   567     val p :: xs = map Free (Variable.variant_frees ctxt intr_ts
```
```   568       (("p", predT) :: (mk_names "x" (length argTs) ~~ argTs)));
```
```   569     val bs = map Free (Variable.variant_frees ctxt (p :: xs @ intr_ts)
```
```   570       (map (rpair HOLogic.boolT) (mk_names "b" k)));
```
```   571
```
```   572     fun subst t = (case dest_predicate cs params t of
```
```   573         SOME (_, i, ts, (Ts, Us)) =>
```
```   574           let val zs = map Bound (length Us - 1 downto 0)
```
```   575           in
```
```   576             list_abs (map (pair "z") Us, list_comb (p,
```
```   577               make_bool_args' bs i @ make_args argTs ((ts ~~ Ts) @ (zs ~~ Us))))
```
```   578           end
```
```   579       | NONE => (case t of
```
```   580           t1 \$ t2 => subst t1 \$ subst t2
```
```   581         | Abs (x, T, u) => Abs (x, T, subst u)
```
```   582         | _ => t));
```
```   583
```
```   584     (* transform an introduction rule into a conjunction  *)
```
```   585     (*   [| p_i t; ... |] ==> p_j u                       *)
```
```   586     (* is transformed into                                *)
```
```   587     (*   b_j & x_j = u & p b_j t & ...                    *)
```
```   588
```
```   589     fun transform_rule r =
```
```   590       let
```
```   591         val SOME (_, i, ts, (Ts, _)) = dest_predicate cs params
```
```   592           (HOLogic.dest_Trueprop (Logic.strip_assums_concl r));
```
```   593         val ps = make_bool_args HOLogic.mk_not I bs i @
```
```   594           map HOLogic.mk_eq (make_args' argTs xs Ts ~~ ts) @
```
```   595           map (subst o HOLogic.dest_Trueprop)
```
```   596             (Logic.strip_assums_hyp r)
```
```   597       in foldr (fn ((x, T), P) => HOLogic.exists_const T \$ (Abs (x, T, P)))
```
```   598         (if null ps then HOLogic.true_const else foldr1 HOLogic.mk_conj ps)
```
```   599         (Logic.strip_params r)
```
```   600       end
```
```   601
```
```   602     (* make a disjunction of all introduction rules *)
```
```   603
```
```   604     val fp_fun = fold_rev lambda (p :: bs @ xs)
```
```   605       (if null intr_ts then HOLogic.false_const
```
```   606        else foldr1 HOLogic.mk_disj (map transform_rule intr_ts));
```
```   607
```
```   608     (* add definiton of recursive predicates to theory *)
```
```   609
```
```   610     val rec_name = if alt_name = "" then
```
```   611       space_implode "_" (map fst cnames_syn) else alt_name;
```
```   612
```
```   613     val ((rec_const, (_, fp_def)), ctxt') = ctxt |>
```
```   614       Variable.add_fixes (map (fst o dest_Free) params) |> snd |>
```
```   615       fold Variable.declare_term intr_ts |>
```
```   616       LocalTheory.def
```
```   617         ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
```
```   618          (("", []), fold_rev lambda params
```
```   619            (Const (fp_name, (predT --> predT) --> predT) \$ fp_fun)));
```
```   620     val fp_def' = Simplifier.rewrite (HOL_basic_ss addsimps [fp_def])
```
```   621       (cterm_of (ProofContext.theory_of ctxt') (list_comb (rec_const, params)));
```
```   622     val specs = if length cs < 2 then [] else
```
```   623       map_index (fn (i, (name_mx, c)) =>
```
```   624         let
```
```   625           val Ts = List.drop (binder_types (fastype_of c), length params);
```
```   626           val xs = map Free (Variable.variant_frees ctxt intr_ts
```
```   627             (mk_names "x" (length Ts) ~~ Ts))
```
```   628         in
```
```   629           (name_mx, (("", []), fold_rev lambda (params @ xs)
```
```   630             (list_comb (rec_const, params @ make_bool_args' bs i @
```
```   631               make_args argTs (xs ~~ Ts)))))
```
```   632         end) (cnames_syn ~~ cs);
```
```   633     val (consts_defs, ctxt'') = fold_map LocalTheory.def specs ctxt';
```
```   634     val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
```
```   635
```
```   636     val mono = prove_mono predT fp_fun monos ctxt''
```
```   637
```
```   638   in (ctxt'', rec_name, mono, fp_def', map (#2 o #2) consts_defs,
```
```   639     list_comb (rec_const, params), preds, argTs, bs, xs)
```
```   640   end;
```
```   641
```
```   642 fun add_ind_def verbose alt_name coind no_elim no_ind cs
```
```   643     intros monos params cnames_syn ctxt =
```
```   644   let
```
```   645     val _ =
```
```   646       if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^
```
```   647         commas_quote (map fst cnames_syn)) else ();
```
```   648
```
```   649     val cnames = map (Sign.full_name (ProofContext.theory_of ctxt) o #1) cnames_syn;
```
```   650     val ((intr_names, intr_atts), intr_ts) = apfst split_list (split_list intros);
```
```   651
```
```   652     val (ctxt1, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds,
```
```   653       argTs, bs, xs) = mk_ind_def alt_name coind cs intr_ts
```
```   654         monos params cnames_syn ctxt;
```
```   655
```
```   656     val (intrs, unfold) = prove_intrs coind mono fp_def (length bs + length xs)
```
```   657       intr_ts rec_preds_defs ctxt1;
```
```   658     val elims = if no_elim then [] else
```
```   659       cnames ~~ map (apfst (singleton (ProofContext.export ctxt1 ctxt)))
```
```   660         (prove_elims cs params intr_ts intr_names unfold rec_preds_defs ctxt1);
```
```   661     val raw_induct = singleton (ProofContext.export ctxt1 ctxt)
```
```   662       (if no_ind then Drule.asm_rl else
```
```   663        if coind then ObjectLogic.rulify (rule_by_tactic
```
```   664          (rewrite_tac [le_fun_def, le_bool_def] THEN
```
```   665            fold_tac rec_preds_defs) (mono RS (fp_def RS def_coinduct)))
```
```   666        else
```
```   667          prove_indrule cs argTs bs xs rec_const params intr_ts mono fp_def
```
```   668            rec_preds_defs ctxt1);
```
```   669     val induct_cases = map (#1 o #1) intros;
```
```   670     val ind_case_names = RuleCases.case_names induct_cases;
```
```   671     val induct =
```
```   672       if coind then
```
```   673         (raw_induct, [RuleCases.case_names [rec_name],
```
```   674           RuleCases.case_conclusion (rec_name, induct_cases),
```
```   675           RuleCases.consumes 1])
```
```   676       else if no_ind orelse length cs > 1 then
```
```   677         (raw_induct, [ind_case_names, RuleCases.consumes 0])
```
```   678       else (raw_induct RSN (2, rev_mp), [ind_case_names, RuleCases.consumes 1]);
```
```   679
```
```   680     val (intrs', ctxt2) =
```
```   681       ctxt1 |>
```
```   682       LocalTheory.notes
```
```   683         (map (fn "" => "" | name => NameSpace.append rec_name name) intr_names ~~
```
```   684          intr_atts ~~
```
```   685          map (single o rpair [] o single) (ProofContext.export ctxt1 ctxt intrs)) |>>
```
```   686       map (hd o snd); (* FIXME? *)
```
```   687     val (((_, elims'), (_, [induct'])), ctxt3) =
```
```   688       ctxt2 |>
```
```   689       LocalTheory.note ((NameSpace.append rec_name "intros", []), intrs') ||>>
```
```   690       fold_map (fn (name, (elim, cases)) =>
```
```   691         LocalTheory.note ((NameSpace.append (Sign.base_name name) "cases",
```
```   692           [Attrib.internal (RuleCases.case_names cases),
```
```   693            Attrib.internal (RuleCases.consumes 1),
```
```   694            Attrib.internal (InductAttrib.cases_set name)]), [elim]) #>
```
```   695         apfst (hd o snd)) elims ||>>
```
```   696       LocalTheory.note ((NameSpace.append rec_name (coind_prefix coind ^ "induct"),
```
```   697         map Attrib.internal (#2 induct)), [rulify (#1 induct)]);
```
```   698
```
```   699     val induct_att = if coind then InductAttrib.coinduct_set else InductAttrib.induct_set;
```
```   700     val ctxt4 = if no_ind then ctxt3 else
```
```   701       let val inducts = cnames ~~ ProjectRule.projects ctxt (1 upto length cnames) induct'
```
```   702       in
```
```   703         ctxt3 |>
```
```   704         LocalTheory.notes (inducts |> map (fn (name, th) => (("",
```
```   705           [Attrib.internal ind_case_names,
```
```   706            Attrib.internal (RuleCases.consumes 1),
```
```   707            Attrib.internal (induct_att name)]), [([th], [])]))) |> snd |>
```
```   708         LocalTheory.note ((NameSpace.append rec_name (coind_prefix coind ^ "inducts"),
```
```   709           [Attrib.internal ind_case_names,
```
```   710            Attrib.internal (RuleCases.consumes 1)]), map snd inducts) |> snd
```
```   711       end;
```
```   712
```
```   713     val result =
```
```   714       {preds = preds,
```
```   715        defs = fp_def :: rec_preds_defs,
```
```   716        mono = singleton (ProofContext.export ctxt1 ctxt) mono,
```
```   717        unfold = singleton (ProofContext.export ctxt1 ctxt) unfold,
```
```   718        intrs = intrs',
```
```   719        elims = elims',
```
```   720        mk_cases = mk_cases elims',
```
```   721        raw_induct = rulify raw_induct,
```
```   722        induct = induct'}
```
```   723
```
```   724   in
```
```   725     (LocalTheory.declaration
```
```   726        (put_inductives cnames ({names = cnames, coind = coind}, result)) ctxt4,
```
```   727      result)
```
```   728   end;
```
```   729
```
```   730
```
```   731 (* external interfaces *)
```
```   732
```
```   733 fun add_inductive_i verbose alt_name coind no_elim no_ind cnames_syn pnames pre_intros monos ctxt =
```
```   734   let
```
```   735     val thy = ProofContext.theory_of ctxt;
```
```   736     val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
```
```   737
```
```   738     val frees = fold (Term.add_frees o snd) pre_intros [];
```
```   739     fun type_of s = (case AList.lookup op = frees s of
```
```   740       NONE => error ("No such variable: " ^ s) | SOME T => T);
```
```   741
```
```   742     val params = map
```
```   743       (fn (s, SOME T) => Free (s, T) | (s, NONE) => Free (s, type_of s)) pnames;
```
```   744     val cs = map
```
```   745       (fn (s, SOME T, _) => Free (s, T) | (s, NONE, _) => Free (s, type_of s)) cnames_syn;
```
```   746     val cnames_syn' = map (fn (s, _, mx) => (s, mx)) cnames_syn;
```
```   747
```
```   748     fun close_rule (x, r) = (x, list_all_free (rev (fold_aterms
```
```   749       (fn t as Free (v as (s, _)) =>
```
```   750             if Variable.is_fixed ctxt s orelse member op = cs t orelse
```
```   751               member op = params t then I else insert op = v
```
```   752         | _ => I) r []), r));
```
```   753
```
```   754     val intros = map (close_rule o check_rule thy cs params) pre_intros;
```
```   755   in
```
```   756     add_ind_def verbose alt_name coind no_elim no_ind cs intros monos
```
```   757       params cnames_syn' ctxt
```
```   758   end;
```
```   759
```
```   760 fun add_inductive verbose coind cnames_syn pnames_syn intro_srcs raw_monos ctxt =
```
```   761   let
```
```   762     val (_, ctxt') = Specification.read_specification (cnames_syn @ pnames_syn) [] ctxt;
```
```   763     val intrs = map (fn spec => apsnd hd (hd (snd (fst
```
```   764       (Specification.read_specification [] [apsnd single spec] ctxt'))))) intro_srcs;
```
```   765     val pnames = map (fn (s, _, _) =>
```
```   766       (s, SOME (ProofContext.infer_type ctxt' s))) pnames_syn;
```
```   767     val cnames_syn' = map (fn (s, _, mx) =>
```
```   768       (s, SOME (ProofContext.infer_type ctxt' s), mx)) cnames_syn;
```
```   769     val (monos, ctxt'') = LocalTheory.theory_result (IsarThy.apply_theorems raw_monos) ctxt;
```
```   770   in
```
```   771     add_inductive_i verbose "" coind false false cnames_syn' pnames intrs monos ctxt''
```
```   772   end;
```
```   773
```
```   774
```
```   775
```
```   776 (** package setup **)
```
```   777
```
```   778 (* setup theory *)
```
```   779
```
```   780 val setup =
```
```   781   InductiveData.init #>
```
```   782   Method.add_methods [("ind_cases2", mk_cases_meth oo mk_cases_args,
```
```   783     "dynamic case analysis on predicates")] #>
```
```   784   Attrib.add_attributes [("mono2", Attrib.add_del_args mono_add mono_del,
```
```   785     "declaration of monotonicity rule")];
```
```   786
```
```   787
```
```   788 (* outer syntax *)
```
```   789
```
```   790 local structure P = OuterParse and K = OuterKeyword in
```
```   791
```
```   792 fun mk_ind coind ((((loc, preds), params), intrs), monos) =
```
```   793   Toplevel.local_theory loc
```
```   794     (#1 o add_inductive true coind preds params intrs monos);
```
```   795
```
```   796 fun ind_decl coind =
```
```   797   P.opt_locale_target --
```
```   798   P.fixes -- Scan.optional (P.\$\$\$ "for" |-- P.fixes) [] --
```
```   799   (P.\$\$\$ "intros" |--
```
```   800     P.!!! (Scan.repeat (P.opt_thm_name ":" -- P.prop))) --
```
```   801   Scan.optional (P.\$\$\$ "monos" |-- P.!!! P.xthms1) []
```
```   802   >> mk_ind coind;
```
```   803
```
```   804 val inductiveP =
```
```   805   OuterSyntax.command "inductive2" "define inductive predicates" K.thy_decl (ind_decl false);
```
```   806
```
```   807 val coinductiveP =
```
```   808   OuterSyntax.command "coinductive2" "define coinductive predicates" K.thy_decl (ind_decl true);
```
```   809
```
```   810
```
```   811 val ind_cases =
```
```   812   P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop)
```
```   813   >> (Toplevel.theory o inductive_cases);
```
```   814
```
```   815 val inductive_casesP =
```
```   816   OuterSyntax.command "inductive_cases2"
```
```   817     "create simplified instances of elimination rules (improper)" K.thy_script ind_cases;
```
```   818
```
```   819 val _ = OuterSyntax.add_keywords ["intros", "monos"];
```
```   820 val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP];
```
```   821
```
```   822 end;
```
```   823
```
```   824 end;
```
```   825
```