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