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