src/Provers/induct_method.ML
author wenzelm
Tue May 07 14:26:32 2002 +0200 (2002-05-07)
changeset 13105 3d1e7a199bdc
parent 12852 c6a8e310aec5
child 13197 0567f4fd1415
permissions -rw-r--r--
use eq_thm_prop instead of slightly inadequate eq_thm;
     1 (*  Title:      Provers/induct_method.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Proof by cases and induction on sets and types.
     7 *)
     8 
     9 signature INDUCT_METHOD_DATA =
    10 sig
    11   val dest_concls: term -> term list
    12   val cases_default: thm
    13   val local_impI: thm
    14   val conjI: thm
    15   val atomize: thm list
    16   val rulify1: thm list
    17   val rulify2: thm list
    18   val localize: thm list
    19 end;
    20 
    21 signature INDUCT_METHOD =
    22 sig
    23   val setup: (theory -> theory) list
    24 end;
    25 
    26 functor InductMethodFun(Data: INDUCT_METHOD_DATA): INDUCT_METHOD =
    27 struct
    28 
    29 
    30 (** misc utils **)
    31 
    32 (* align lists *)
    33 
    34 fun align_left msg xs ys =
    35   let val m = length xs and n = length ys
    36   in if m < n then raise ERROR_MESSAGE msg else (Library.take (n, xs) ~~ ys) end;
    37 
    38 fun align_right msg xs ys =
    39   let val m = length xs and n = length ys
    40   in if m < n then raise ERROR_MESSAGE msg else (Library.drop (m - n, xs) ~~ ys) end;
    41 
    42 
    43 (* prep_inst *)
    44 
    45 fun prep_inst align cert tune (tm, ts) =
    46   let
    47     fun prep_var (x, Some t) =
    48           let
    49             val cx = cert x;
    50             val {T = xT, sign, ...} = Thm.rep_cterm cx;
    51             val ct = cert (tune t);
    52           in
    53             if Sign.typ_instance sign (#T (Thm.rep_cterm ct), xT) then Some (cx, ct)
    54             else raise ERROR_MESSAGE (Pretty.string_of (Pretty.block
    55              [Pretty.str "Ill-typed instantiation:", Pretty.fbrk,
    56               Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1,
    57               Display.pretty_ctyp (#T (Thm.crep_cterm ct))]))
    58           end
    59       | prep_var (_, None) = None;
    60     val xs = InductAttrib.vars_of tm;
    61   in
    62     align "Rule has fewer variables than instantiations given" xs ts
    63     |> mapfilter prep_var
    64   end;
    65 
    66 
    67 
    68 (** cases method **)
    69 
    70 (*
    71   rule selection scheme:
    72           cases         - classical case split
    73     <x:A> cases ...     - set cases
    74           cases t       - type cases
    75     ...   cases ... R   - explicit rule
    76 *)
    77 
    78 local
    79 
    80 fun resolveq_cases_tac make ruleq i st =
    81   ruleq |> Seq.map (fn (rule, (cases, facts)) =>
    82     (Method.insert_tac facts THEN' Tactic.rtac rule) i st
    83     |> Seq.map (rpair (make (Thm.sign_of_thm rule, Thm.prop_of rule) cases)))
    84   |> Seq.flat;
    85 
    86 fun find_casesT ctxt ((Some t :: _) :: _) = InductAttrib.find_casesT ctxt (fastype_of t)
    87   | find_casesT _ _ = [];
    88 
    89 fun find_casesS ctxt (fact :: _) = InductAttrib.find_casesS ctxt fact
    90   | find_casesS _ _ = [];
    91 
    92 fun cases_tac (ctxt, (open_parms, (insts, opt_rule))) facts =
    93   let
    94     val sg = ProofContext.sign_of ctxt;
    95     val cert = Thm.cterm_of sg;
    96 
    97     fun inst_rule r =
    98       if null insts then RuleCases.add r
    99       else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
   100         |> (flat o map (prep_inst align_left cert I))
   101         |> Drule.cterm_instantiate) r |> rpair (RuleCases.get r);
   102 
   103     val ruleq =
   104       (case opt_rule of
   105         None =>
   106           let val rules = find_casesS ctxt facts @ find_casesT ctxt insts @ [Data.cases_default] in
   107             Method.trace ctxt rules;
   108             Seq.flat (Seq.map (Seq.try inst_rule) (Seq.of_list rules))
   109           end
   110       | Some r => Seq.single (inst_rule r));
   111 
   112     fun prep_rule (th, (cases, n)) = Seq.map (apsnd (rpair (drop (n, facts))) o rpair cases)
   113       (Method.multi_resolves (take (n, facts)) [th]);
   114   in resolveq_cases_tac (RuleCases.make open_parms) (Seq.flat (Seq.map prep_rule ruleq)) end;
   115 
   116 in
   117 
   118 val cases_meth = Method.METHOD_CASES o ((Seq.DETERM o HEADGOAL) oo cases_tac);
   119 
   120 end;
   121 
   122 
   123 
   124 (** induct method **)
   125 
   126 (*
   127   rule selection scheme:
   128     <x:A> induct ...     - set induction
   129           induct x       - type induction
   130     ...   induct ... R   - explicit rule
   131 *)
   132 
   133 local
   134 
   135 
   136 (* atomize and rulify *)
   137 
   138 fun atomize_term sg =
   139   ObjectLogic.drop_judgment sg o MetaSimplifier.rewrite_term sg Data.atomize;
   140 
   141 fun rulified_term thm =
   142   let val sg = Thm.sign_of_thm thm in
   143     Thm.prop_of thm
   144     |> MetaSimplifier.rewrite_term sg Data.rulify1
   145     |> MetaSimplifier.rewrite_term sg Data.rulify2
   146     |> pair sg
   147   end;
   148 
   149 val atomize_tac = Tactic.rewrite_goal_tac Data.atomize;
   150 
   151 val rulify_tac =
   152   Tactic.rewrite_goal_tac Data.rulify1 THEN'
   153   Tactic.rewrite_goal_tac Data.rulify2 THEN'
   154   Tactic.norm_hhf_tac;
   155 
   156 val localize = Tactic.norm_hhf_rule o Tactic.simplify false Data.localize;
   157 
   158 
   159 (* imp_intr --- limited to atomic prems *)
   160 
   161 fun imp_intr i raw_th =
   162   let
   163     val th = Thm.permute_prems (i - 1) 1 raw_th;
   164     val cprems = Drule.cprems_of th;
   165     val As = take (length cprems - 1, cprems);
   166     val C = Thm.cterm_of (Thm.sign_of_thm th) (Var (("C", #maxidx (Thm.rep_thm th) + 1), propT));
   167     val dummy_st = Drule.mk_triv_goal (Drule.list_implies (As, C));
   168   in th COMP Thm.lift_rule (dummy_st, 1) Data.local_impI end;
   169 
   170 
   171 (* join multi-rules *)
   172 
   173 val eq_prems = curry (Term.aconvs o pairself Thm.prems_of);
   174 
   175 fun join_rules [] = []
   176   | join_rules [th] = [th]
   177   | join_rules (rules as r :: rs) =
   178       if not (forall (eq_prems r) rs) then []
   179       else
   180         let
   181           val th :: ths = map Drule.freeze_all rules;
   182           val cprems = Drule.cprems_of th;
   183           val asms = map Thm.assume cprems;
   184         in
   185           [foldr1 (fn (x, x') => [x, x'] MRS Data.conjI)
   186             (map (fn x => Drule.implies_elim_list x asms) (th :: ths))
   187           |> Drule.implies_intr_list cprems
   188           |> Drule.standard'
   189           |> RuleCases.save th]
   190         end;
   191 
   192 
   193 (* divinate rule instantiation (cannot handle pending goal parameters) *)
   194 
   195 fun dest_env sign (env as Envir.Envir {asol, iTs, ...}) =
   196   let
   197     val pairs = Vartab.dest asol;
   198     val ts = map (Thm.cterm_of sign o Envir.norm_term env o #2) pairs;
   199     val xs = map2 (Thm.cterm_of sign o Var) (map #1 pairs, map (#T o Thm.rep_cterm) ts);
   200   in (map (apsnd (Thm.ctyp_of sign)) (Vartab.dest iTs), xs ~~ ts) end;
   201 
   202 fun divinate_inst rule i st =
   203   let
   204     val {sign, maxidx, ...} = Thm.rep_thm st;
   205     val goal = List.nth (Thm.prems_of st, i - 1);  (*exception Subscript*)
   206     val params = rev (rename_wrt_term goal (Logic.strip_params goal));  (*as they are printed :-*)
   207   in
   208     if not (null params) then
   209       (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^
   210         commas (map (Sign.string_of_term sign o Syntax.mark_boundT) params));
   211       Seq.single rule)
   212     else
   213       let
   214         val rule' = Thm.incr_indexes (maxidx + 1) rule;
   215         val concl = Logic.strip_assums_concl goal;
   216       in
   217         Unify.smash_unifiers (sign, Envir.empty (#maxidx (Thm.rep_thm rule')),
   218           [(Thm.concl_of rule', concl)])
   219         |> Seq.map (fn env => Drule.instantiate (dest_env sign env) rule')
   220       end
   221   end handle Subscript => Seq.empty;
   222 
   223 
   224 (* compose tactics with cases *)
   225 
   226 fun internalize k th = if k > 0 then internalize (k - 1) (imp_intr k th) else th;
   227 
   228 fun resolveq_cases_tac' make ruleq i st =
   229   ruleq |> Seq.map (fn (rule, (cases, k, more_facts)) => st
   230     |> (Method.insert_tac more_facts THEN' atomize_tac) i
   231     |> Seq.map (fn st' => divinate_inst (internalize k rule) i st' |> Seq.map (fn rule' =>
   232           st' |> Tactic.rtac rule' i
   233           |> Seq.map (rpair (make (rulified_term rule') cases)))
   234       |> Seq.flat)
   235     |> Seq.flat)
   236   |> Seq.flat;
   237 
   238 infix 1 THEN_ALL_NEW_CASES;
   239 
   240 fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
   241   st |> Seq.THEN (tac1 i, (fn (st', cases) =>
   242     Seq.map (rpair cases) (Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st) st')));
   243 
   244 
   245 (* find rules *)
   246 
   247 fun find_inductT ctxt insts =
   248   foldr multiply (insts |> mapfilter (fn [] => None | ts => last_elem ts)
   249     |> map (InductAttrib.find_inductT ctxt o fastype_of), [[]])
   250   |> map join_rules |> flat;
   251 
   252 fun find_inductS ctxt (fact :: _) = InductAttrib.find_inductS ctxt fact
   253   | find_inductS _ _ = [];
   254 
   255 
   256 (* main tactic *)
   257 
   258 fun induct_tac (ctxt, (open_parms, (insts, opt_rule))) facts =
   259   let
   260     val sg = ProofContext.sign_of ctxt;
   261     val cert = Thm.cterm_of sg;
   262 
   263     fun rule_versions r = Seq.cons (r, Seq.filter (not o curry Thm.eq_thm r)
   264         (Seq.make (fn () => Some (localize r, Seq.empty))))
   265       |> Seq.map (rpair (RuleCases.get r));
   266 
   267     val inst_rule = apfst (fn r =>
   268       if null insts then r
   269       else (align_right "Rule has fewer conclusions than arguments given"
   270           (Data.dest_concls (Thm.concl_of r)) insts
   271         |> (flat o map (prep_inst align_right cert (atomize_term sg)))
   272         |> Drule.cterm_instantiate) r);
   273 
   274     val ruleq =
   275       (case opt_rule of
   276         None =>
   277           let val rules = find_inductS ctxt facts @ find_inductT ctxt insts in
   278             conditional (null rules) (fn () => error "Unable to figure out induct rule");
   279             Method.trace ctxt rules;
   280             rules |> Seq.THEN (Seq.of_list, Seq.THEN (rule_versions, Seq.try inst_rule))
   281           end
   282       | Some r => r |> Seq.THEN (rule_versions, Seq.single o inst_rule));
   283 
   284     fun prep_rule (th, (cases, n)) =
   285       Seq.map (rpair (cases, n - length facts, drop (n, facts)))
   286         (Method.multi_resolves (take (n, facts)) [th]);
   287     val tac = resolveq_cases_tac' (RuleCases.make open_parms) (Seq.flat (Seq.map prep_rule ruleq));
   288   in tac THEN_ALL_NEW_CASES rulify_tac end;
   289 
   290 in
   291 
   292 val induct_meth = Method.RAW_METHOD_CASES o ((Seq.DETERM o HEADGOAL) oo induct_tac);
   293 
   294 end;
   295 
   296 
   297 
   298 (** concrete syntax **)
   299 
   300 val openN = "open";
   301 val ruleN = "rule";
   302 val ofN = "of";
   303 
   304 local
   305 
   306 fun check k get name =
   307   (case get name of Some x => x
   308   | None => error ("No rule for " ^ k ^ " " ^ quote name));
   309 
   310 fun spec k = (Args.$$$ k -- Args.colon) |-- Args.!!! Args.name;
   311 
   312 fun rule get_type get_set =
   313   Scan.depend (fn ctxt =>
   314     let val sg = ProofContext.sign_of ctxt in
   315       spec InductAttrib.typeN >> (check InductAttrib.typeN (get_type ctxt) o
   316         Sign.certify_tyname sg o Sign.intern_tycon sg) ||
   317       spec InductAttrib.setN >> (check InductAttrib.setN (get_set ctxt) o
   318         Sign.certify_const sg o Sign.intern_const sg)
   319     end >> pair ctxt) ||
   320   Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.local_thm;
   321 
   322 val cases_rule = rule InductAttrib.lookup_casesT InductAttrib.lookup_casesS;
   323 val induct_rule = rule InductAttrib.lookup_inductT InductAttrib.lookup_inductS;
   324 
   325 val kind_inst =
   326   (Args.$$$ InductAttrib.typeN || Args.$$$ InductAttrib.setN || Args.$$$ ruleN || Args.$$$ ofN)
   327     -- Args.colon;
   328 val term = Scan.unless (Scan.lift kind_inst) Args.local_term;
   329 val term_dummy = Scan.unless (Scan.lift kind_inst)
   330   (Scan.lift (Args.$$$ "_") >> K None || Args.local_term >> Some);
   331 
   332 val instss = Args.and_list (Scan.repeat1 term_dummy);
   333 
   334 in
   335 
   336 val cases_args = Method.syntax (Args.mode openN -- (instss -- Scan.option cases_rule));
   337 val induct_args = Method.syntax (Args.mode openN -- (instss -- Scan.option induct_rule));
   338 
   339 end;
   340 
   341 
   342 
   343 (** theory setup **)
   344 
   345 val setup =
   346   [Method.add_methods
   347     [(InductAttrib.casesN, cases_meth oo cases_args, "case analysis on types or sets"),
   348      (InductAttrib.inductN, induct_meth oo induct_args, "induction on types or sets")]];
   349 
   350 end;