src/Tools/induct.ML
author wenzelm
Mon Mar 12 11:17:59 2018 +0100 (18 months ago)
changeset 67835 c8e4ee2b5482
parent 67649 1e1782c1aedf
child 69590 e65314985426
permissions -rw-r--r--
tuned imports;
     1 (*  Title:      Tools/induct.ML
     2     Author:     Markus Wenzel, TU Muenchen
     3 
     4 Proof by cases, induction, and coinduction.
     5 *)
     6 
     7 signature INDUCT_ARGS =
     8 sig
     9   val cases_default: thm
    10   val atomize: thm list
    11   val rulify: thm list
    12   val rulify_fallback: thm list
    13   val equal_def: thm
    14   val dest_def: term -> (term * term) option
    15   val trivial_tac: Proof.context -> int -> tactic
    16 end;
    17 
    18 signature INDUCT =
    19 sig
    20   (*rule declarations*)
    21   val vars_of: term -> term list
    22   val dest_rules: Proof.context ->
    23     {type_cases: (string * thm) list, pred_cases: (string * thm) list,
    24       type_induct: (string * thm) list, pred_induct: (string * thm) list,
    25       type_coinduct: (string * thm) list, pred_coinduct: (string * thm) list}
    26   val print_rules: Proof.context -> unit
    27   val lookup_casesT: Proof.context -> string -> thm option
    28   val lookup_casesP: Proof.context -> string -> thm option
    29   val lookup_inductT: Proof.context -> string -> thm option
    30   val lookup_inductP: Proof.context -> string -> thm option
    31   val lookup_coinductT: Proof.context -> string -> thm option
    32   val lookup_coinductP: Proof.context -> string -> thm option
    33   val find_casesT: Proof.context -> typ -> thm list
    34   val find_casesP: Proof.context -> term -> thm list
    35   val find_inductT: Proof.context -> typ -> thm list
    36   val find_inductP: Proof.context -> term -> thm list
    37   val find_coinductT: Proof.context -> typ -> thm list
    38   val find_coinductP: Proof.context -> term -> thm list
    39   val cases_type: string -> attribute
    40   val cases_pred: string -> attribute
    41   val cases_del: attribute
    42   val induct_type: string -> attribute
    43   val induct_pred: string -> attribute
    44   val induct_del: attribute
    45   val coinduct_type: string -> attribute
    46   val coinduct_pred: string -> attribute
    47   val coinduct_del: attribute
    48   val map_simpset: (Proof.context -> Proof.context) -> Context.generic -> Context.generic
    49   val induct_simp_add: attribute
    50   val induct_simp_del: attribute
    51   val no_simpN: string
    52   val casesN: string
    53   val inductN: string
    54   val coinductN: string
    55   val typeN: string
    56   val predN: string
    57   val setN: string
    58   (*proof methods*)
    59   val arbitrary_tac: Proof.context -> int -> (string * typ) list -> int -> tactic
    60   val add_defs: (binding option * (term * bool)) option list -> Proof.context ->
    61     (term option list * thm list) * Proof.context
    62   val atomize_term: Proof.context -> term -> term
    63   val atomize_cterm: Proof.context -> conv
    64   val atomize_tac: Proof.context -> int -> tactic
    65   val inner_atomize_tac: Proof.context -> int -> tactic
    66   val rulified_term: Proof.context -> thm -> term
    67   val rulify_tac: Proof.context -> int -> tactic
    68   val simplified_rule: Proof.context -> thm -> thm
    69   val simplify_tac: Proof.context -> int -> tactic
    70   val trivial_tac: Proof.context -> int -> tactic
    71   val rotate_tac: int -> int -> int -> tactic
    72   val internalize: Proof.context -> int -> thm -> thm
    73   val guess_instance: Proof.context -> thm -> int -> thm -> thm Seq.seq
    74   val cases_context_tactic: bool -> term option list list -> thm option ->
    75     thm list -> int -> context_tactic
    76   val cases_tac: Proof.context -> bool -> term option list list -> thm option ->
    77     thm list -> int -> tactic
    78   val get_inductT: Proof.context -> term option list list -> thm list list
    79   val gen_induct_context_tactic: ((Rule_Cases.info * int) * thm -> (Rule_Cases.info * int) * thm) ->
    80     bool -> (binding option * (term * bool)) option list list ->
    81     (string * typ) list list -> term option list -> thm list option ->
    82     thm list -> int -> context_tactic
    83   val gen_induct_tac: Proof.context ->
    84     ((Rule_Cases.info * int) * thm -> (Rule_Cases.info * int) * thm) ->
    85     bool -> (binding option * (term * bool)) option list list ->
    86     (string * typ) list list -> term option list -> thm list option ->
    87     thm list -> int -> tactic
    88   val induct_context_tactic: bool ->
    89     (binding option * (term * bool)) option list list ->
    90     (string * typ) list list -> term option list -> thm list option ->
    91     thm list -> int -> context_tactic
    92   val induct_tac: Proof.context -> bool ->
    93     (binding option * (term * bool)) option list list ->
    94     (string * typ) list list -> term option list -> thm list option ->
    95     thm list -> int -> tactic
    96   val coinduct_context_tactic: term option list -> term option list -> thm option ->
    97     thm list -> int -> context_tactic
    98   val coinduct_tac: Proof.context -> term option list -> term option list -> thm option ->
    99     thm list -> int -> tactic
   100   val gen_induct_setup: binding ->
   101    (bool -> (binding option * (term * bool)) option list list ->
   102     (string * typ) list list -> term option list -> thm list option ->
   103     thm list -> int -> context_tactic) -> local_theory -> local_theory
   104 end;
   105 
   106 functor Induct(Induct_Args: INDUCT_ARGS): INDUCT =
   107 struct
   108 
   109 (** variables -- ordered left-to-right, preferring right **)
   110 
   111 fun vars_of tm =
   112   rev (distinct (op =) (Term.fold_aterms (fn t as Var _ => cons t | _ => I) tm []));
   113 
   114 local
   115 
   116 val mk_var = Net.encode_type o #2 o Term.dest_Var;
   117 
   118 fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle List.Empty =>
   119   raise THM ("No variables in conclusion of rule", 0, [thm]);
   120 
   121 in
   122 
   123 fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle List.Empty =>
   124   raise THM ("No variables in major premise of rule", 0, [thm]);
   125 
   126 val left_var_concl = concl_var hd;
   127 val right_var_concl = concl_var List.last;
   128 
   129 end;
   130 
   131 
   132 
   133 (** constraint simplification **)
   134 
   135 (* rearrange parameters and premises to allow application of one-point-rules *)
   136 
   137 fun swap_params_conv ctxt i j cv =
   138   let
   139     fun conv1 0 ctxt = Conv.forall_conv (cv o snd) ctxt
   140       | conv1 k ctxt =
   141           Conv.rewr_conv @{thm swap_params} then_conv
   142           Conv.forall_conv (conv1 (k - 1) o snd) ctxt;
   143     fun conv2 0 ctxt = conv1 j ctxt
   144       | conv2 k ctxt = Conv.forall_conv (conv2 (k - 1) o snd) ctxt;
   145   in conv2 i ctxt end;
   146 
   147 fun swap_prems_conv 0 = Conv.all_conv
   148   | swap_prems_conv i =
   149       Conv.implies_concl_conv (swap_prems_conv (i - 1)) then_conv
   150       Conv.rewr_conv Drule.swap_prems_eq;
   151 
   152 fun find_eq ctxt t =
   153   let
   154     val l = length (Logic.strip_params t);
   155     val Hs = Logic.strip_assums_hyp t;
   156     fun find (i, t) =
   157       (case Induct_Args.dest_def (Object_Logic.drop_judgment ctxt t) of
   158         SOME (Bound j, _) => SOME (i, j)
   159       | SOME (_, Bound j) => SOME (i, j)
   160       | _ => NONE);
   161   in
   162     (case get_first find (map_index I Hs) of
   163       NONE => NONE
   164     | SOME (0, 0) => NONE
   165     | SOME (i, j) => SOME (i, l - j - 1, j))
   166   end;
   167 
   168 fun mk_swap_rrule ctxt ct =
   169   (case find_eq ctxt (Thm.term_of ct) of
   170     NONE => NONE
   171   | SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct));
   172 
   173 val rearrange_eqs_simproc =
   174   Simplifier.make_simproc @{context} "rearrange_eqs"
   175    {lhss = [@{term "Pure.all (t :: 'a::{} \<Rightarrow> prop)"}],
   176     proc = fn _ => fn ctxt => fn ct => mk_swap_rrule ctxt ct};
   177 
   178 
   179 (* rotate k premises to the left by j, skipping over first j premises *)
   180 
   181 fun rotate_conv 0 _ 0 = Conv.all_conv
   182   | rotate_conv 0 j k = swap_prems_conv j then_conv rotate_conv 1 j (k - 1)
   183   | rotate_conv i j k = Conv.implies_concl_conv (rotate_conv (i - 1) j k);
   184 
   185 fun rotate_tac _ 0 = K all_tac
   186   | rotate_tac j k = SUBGOAL (fn (goal, i) =>
   187       CONVERSION (rotate_conv
   188         j (length (Logic.strip_assums_hyp goal) - j - k) k) i);
   189 
   190 
   191 (* rulify operators around definition *)
   192 
   193 fun rulify_defs_conv ctxt ct =
   194   if exists_subterm (is_some o Induct_Args.dest_def) (Thm.term_of ct) andalso
   195     not (is_some (Induct_Args.dest_def (Object_Logic.drop_judgment ctxt (Thm.term_of ct))))
   196   then
   197     (Conv.forall_conv (rulify_defs_conv o snd) ctxt else_conv
   198      Conv.implies_conv (Conv.try_conv (rulify_defs_conv ctxt))
   199        (Conv.try_conv (rulify_defs_conv ctxt)) else_conv
   200      Conv.first_conv (map Conv.rewr_conv Induct_Args.rulify) then_conv
   201        Conv.try_conv (rulify_defs_conv ctxt)) ct
   202   else Conv.no_conv ct;
   203 
   204 
   205 
   206 (** induct data **)
   207 
   208 (* rules *)
   209 
   210 type rules = (string * thm) Item_Net.T;
   211 
   212 fun init_rules index : rules =
   213   Item_Net.init
   214     (fn ((s1, th1), (s2, th2)) => s1 = s2 andalso Thm.eq_thm_prop (th1, th2))
   215     (single o index);
   216 
   217 fun filter_rules (rs: rules) th =
   218   filter (fn (_, th') => Thm.eq_thm_prop (th, th')) (Item_Net.content rs);
   219 
   220 fun pretty_rules ctxt kind rs =
   221   let val thms = map snd (Item_Net.content rs)
   222   in Pretty.big_list kind (map (Thm.pretty_thm_item ctxt) thms) end;
   223 
   224 
   225 (* context data *)
   226 
   227 structure Data = Generic_Data
   228 (
   229   type T = (rules * rules) * (rules * rules) * (rules * rules) * simpset;
   230   val empty =
   231     ((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)),
   232      (init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)),
   233      (init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)),
   234      simpset_of (empty_simpset @{context}
   235       addsimprocs [rearrange_eqs_simproc] addsimps [Drule.norm_hhf_eq]));
   236   val extend = I;
   237   fun merge (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1), simpset1),
   238       ((casesT2, casesP2), (inductT2, inductP2), (coinductT2, coinductP2), simpset2)) =
   239     ((Item_Net.merge (casesT1, casesT2), Item_Net.merge (casesP1, casesP2)),
   240      (Item_Net.merge (inductT1, inductT2), Item_Net.merge (inductP1, inductP2)),
   241      (Item_Net.merge (coinductT1, coinductT2), Item_Net.merge (coinductP1, coinductP2)),
   242      merge_ss (simpset1, simpset2));
   243 );
   244 
   245 val get_local = Data.get o Context.Proof;
   246 
   247 fun dest_rules ctxt =
   248   let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP), _) = get_local ctxt in
   249     {type_cases = Item_Net.content casesT,
   250      pred_cases = Item_Net.content casesP,
   251      type_induct = Item_Net.content inductT,
   252      pred_induct = Item_Net.content inductP,
   253      type_coinduct = Item_Net.content coinductT,
   254      pred_coinduct = Item_Net.content coinductP}
   255   end;
   256 
   257 fun print_rules ctxt =
   258   let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP), _) = get_local ctxt in
   259    [pretty_rules ctxt "coinduct type:" coinductT,
   260     pretty_rules ctxt "coinduct pred:" coinductP,
   261     pretty_rules ctxt "induct type:" inductT,
   262     pretty_rules ctxt "induct pred:" inductP,
   263     pretty_rules ctxt "cases type:" casesT,
   264     pretty_rules ctxt "cases pred:" casesP]
   265     |> Pretty.writeln_chunks
   266   end;
   267 
   268 val _ =
   269   Outer_Syntax.command \<^command_keyword>\<open>print_induct_rules\<close>
   270     "print induction and cases rules"
   271     (Scan.succeed (Toplevel.keep (print_rules o Toplevel.context_of)));
   272 
   273 
   274 (* access rules *)
   275 
   276 local
   277 
   278 fun lookup_rule which ctxt =
   279   AList.lookup (op =) (Item_Net.content (which (get_local ctxt)))
   280   #> Option.map (Thm.transfer' ctxt);
   281 
   282 fun find_rules which how ctxt x =
   283   Item_Net.retrieve (which (get_local ctxt)) (how x)
   284   |> map (Thm.transfer' ctxt o snd);
   285 
   286 in
   287 
   288 val lookup_casesT = lookup_rule (#1 o #1);
   289 val lookup_casesP = lookup_rule (#2 o #1);
   290 val lookup_inductT = lookup_rule (#1 o #2);
   291 val lookup_inductP = lookup_rule (#2 o #2);
   292 val lookup_coinductT = lookup_rule (#1 o #3);
   293 val lookup_coinductP = lookup_rule (#2 o #3);
   294 
   295 val find_casesT = find_rules (#1 o #1) Net.encode_type;
   296 val find_casesP = find_rules (#2 o #1) I;
   297 val find_inductT = find_rules (#1 o #2) Net.encode_type;
   298 val find_inductP = find_rules (#2 o #2) I;
   299 val find_coinductT = find_rules (#1 o #3) Net.encode_type;
   300 val find_coinductP = find_rules (#2 o #3) I;
   301 
   302 end;
   303 
   304 
   305 
   306 (** attributes **)
   307 
   308 local
   309 
   310 fun mk_att f g name =
   311   Thm.mixed_attribute (fn (context, thm) =>
   312     let
   313       val thm' = g thm;
   314       val context' =
   315         if Thm.is_free_dummy thm then context
   316         else Data.map (f (name, Thm.trim_context thm')) context;
   317     in (context', thm') end);
   318 
   319 fun del_att which =
   320   Thm.declaration_attribute (fn th => Data.map (which (apply2 (fn rs =>
   321     fold Item_Net.remove (filter_rules rs th) rs))));
   322 
   323 fun add_casesT rule x = @{apply 4(1)} (apfst (Item_Net.update rule)) x;
   324 fun add_casesP rule x = @{apply 4(1)} (apsnd (Item_Net.update rule)) x;
   325 fun add_inductT rule x = @{apply 4(2)} (apfst (Item_Net.update rule)) x;
   326 fun add_inductP rule x = @{apply 4(2)} (apsnd (Item_Net.update rule)) x;
   327 fun add_coinductT rule x = @{apply 4(3)} (apfst (Item_Net.update rule)) x;
   328 fun add_coinductP rule x = @{apply 4(3)} (apsnd (Item_Net.update rule)) x;
   329 
   330 val consumes0 = Rule_Cases.default_consumes 0;
   331 val consumes1 = Rule_Cases.default_consumes 1;
   332 
   333 in
   334 
   335 val cases_type = mk_att add_casesT consumes0;
   336 val cases_pred = mk_att add_casesP consumes1;
   337 val cases_del = del_att @{apply 4(1)};
   338 
   339 val induct_type = mk_att add_inductT consumes0;
   340 val induct_pred = mk_att add_inductP consumes1;
   341 val induct_del = del_att @{apply 4(2)};
   342 
   343 val coinduct_type = mk_att add_coinductT consumes0;
   344 val coinduct_pred = mk_att add_coinductP consumes1;
   345 val coinduct_del = del_att @{apply 4(3)};
   346 
   347 fun map_simpset f context =
   348   context |> (Data.map o @{apply 4(4)} o Simplifier.simpset_map (Context.proof_of context)) f;
   349 
   350 fun induct_simp f =
   351   Thm.declaration_attribute (fn thm => map_simpset (fn ctxt => f (ctxt, [thm])));
   352 
   353 val induct_simp_add = induct_simp (op addsimps);
   354 val induct_simp_del = induct_simp (op delsimps);
   355 
   356 end;
   357 
   358 
   359 
   360 (** attribute syntax **)
   361 
   362 val no_simpN = "no_simp";
   363 val casesN = "cases";
   364 val inductN = "induct";
   365 val coinductN = "coinduct";
   366 
   367 val typeN = "type";
   368 val predN = "pred";
   369 val setN = "set";
   370 
   371 local
   372 
   373 fun spec k arg =
   374   Scan.lift (Args.$$$ k -- Args.colon) |-- arg ||
   375   Scan.lift (Args.$$$ k) >> K "";
   376 
   377 fun attrib add_type add_pred del =
   378   spec typeN (Args.type_name {proper = false, strict = false}) >> add_type ||
   379   spec predN (Args.const {proper = false, strict = false}) >> add_pred ||
   380   spec setN (Args.const {proper = false, strict = false}) >> add_pred ||
   381   Scan.lift Args.del >> K del;
   382 
   383 in
   384 
   385 val _ =
   386   Theory.local_setup
   387    (Attrib.local_setup \<^binding>\<open>cases\<close> (attrib cases_type cases_pred cases_del)
   388       "declaration of cases rule" #>
   389     Attrib.local_setup \<^binding>\<open>induct\<close> (attrib induct_type induct_pred induct_del)
   390       "declaration of induction rule" #>
   391     Attrib.local_setup \<^binding>\<open>coinduct\<close> (attrib coinduct_type coinduct_pred coinduct_del)
   392       "declaration of coinduction rule" #>
   393     Attrib.local_setup \<^binding>\<open>induct_simp\<close> (Attrib.add_del induct_simp_add induct_simp_del)
   394       "declaration of rules for simplifying induction or cases rules");
   395 
   396 end;
   397 
   398 
   399 
   400 (** method utils **)
   401 
   402 (* alignment *)
   403 
   404 fun align_left msg xs ys =
   405   let val m = length xs and n = length ys
   406   in if m < n then error msg else (take n xs ~~ ys) end;
   407 
   408 fun align_right msg xs ys =
   409   let val m = length xs and n = length ys
   410   in if m < n then error msg else (drop (m - n) xs ~~ ys) end;
   411 
   412 
   413 (* prep_inst *)
   414 
   415 fun prep_inst ctxt align tune (tm, ts) =
   416   let
   417     fun prep_var (Var (x, xT), SOME t) =
   418           let
   419             val ct = Thm.cterm_of ctxt (tune t);
   420             val tT = Thm.typ_of_cterm ct;
   421           in
   422             if Type.could_unify (tT, xT) then SOME (x, ct)
   423             else error (Pretty.string_of (Pretty.block
   424              [Pretty.str "Ill-typed instantiation:", Pretty.fbrk,
   425               Syntax.pretty_term ctxt (Thm.term_of ct), Pretty.str " ::", Pretty.brk 1,
   426               Syntax.pretty_typ ctxt tT]))
   427           end
   428       | prep_var (_, NONE) = NONE;
   429     val xs = vars_of tm;
   430   in
   431     align "Rule has fewer variables than instantiations given" xs ts
   432     |> map_filter prep_var
   433   end;
   434 
   435 
   436 (* trace_rules *)
   437 
   438 fun trace_rules _ kind [] = error ("Unable to figure out " ^ kind ^ " rule")
   439   | trace_rules ctxt _ rules = Method.trace ctxt rules;
   440 
   441 
   442 (* mark equality constraints in cases rule *)
   443 
   444 val equal_def' = Thm.symmetric Induct_Args.equal_def;
   445 
   446 fun mark_constraints n ctxt = Conv.fconv_rule
   447   (Conv.prems_conv ~1 (Conv.params_conv ~1 (K (Conv.prems_conv n
   448      (Raw_Simplifier.rewrite ctxt false [equal_def']))) ctxt));
   449 
   450 fun unmark_constraints ctxt =
   451   Conv.fconv_rule (Raw_Simplifier.rewrite ctxt true [Induct_Args.equal_def]);
   452 
   453 
   454 (* simplify *)
   455 
   456 fun simplify_conv' ctxt =
   457   Simplifier.full_rewrite (put_simpset (#4 (get_local ctxt)) ctxt);
   458 
   459 fun simplify_conv ctxt ct =
   460   if exists_subterm (is_some o Induct_Args.dest_def) (Thm.term_of ct) then
   461     (Conv.try_conv (rulify_defs_conv ctxt) then_conv simplify_conv' ctxt) ct
   462   else Conv.all_conv ct;
   463 
   464 fun gen_simplified_rule cv ctxt =
   465   Conv.fconv_rule (Conv.prems_conv ~1 (cv ctxt));
   466 
   467 val simplified_rule' = gen_simplified_rule simplify_conv';
   468 val simplified_rule = gen_simplified_rule simplify_conv;
   469 
   470 fun simplify_tac ctxt = CONVERSION (simplify_conv ctxt);
   471 
   472 val trivial_tac = Induct_Args.trivial_tac;
   473 
   474 
   475 
   476 (** cases method **)
   477 
   478 (*
   479   rule selection scheme:
   480           cases         - default case split
   481     `A t` cases ...     - predicate/set cases
   482           cases t       - type cases
   483     ...   cases ... r   - explicit rule
   484 *)
   485 
   486 local
   487 
   488 fun get_casesT ctxt ((SOME t :: _) :: _) = find_casesT ctxt (Term.fastype_of t)
   489   | get_casesT _ _ = [];
   490 
   491 fun get_casesP ctxt (fact :: _) = find_casesP ctxt (Thm.concl_of fact)
   492   | get_casesP _ _ = [];
   493 
   494 in
   495 
   496 fun cases_context_tactic simp insts opt_rule facts i : context_tactic =
   497   fn (ctxt, st) =>
   498     let
   499       fun inst_rule r =
   500         (if null insts then r
   501          else
   502            (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
   503              |> maps (prep_inst ctxt align_left I)
   504              |> infer_instantiate ctxt) r)
   505         |> simp ? mark_constraints (Rule_Cases.get_constraints r) ctxt
   506         |> pair (Rule_Cases.get r);
   507   
   508       val (opt_rule', facts') =
   509         (case (opt_rule, facts) of
   510           (NONE, th :: ths) =>
   511             if is_some (Object_Logic.elim_concl ctxt th) then (SOME th, ths)
   512             else (opt_rule, facts)
   513         | _ => (opt_rule, facts));
   514   
   515       val ruleq =
   516         (case opt_rule' of
   517           SOME r => Seq.single (inst_rule r)
   518         | NONE =>
   519             (get_casesP ctxt facts' @ get_casesT ctxt insts @ [Induct_Args.cases_default])
   520             |> tap (trace_rules ctxt casesN)
   521             |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
   522     in
   523       ruleq
   524       |> Seq.maps (Rule_Cases.consume ctxt [] facts')
   525       |> Seq.maps (fn ((cases, (_, facts'')), rule) =>
   526         let
   527           val rule' = rule
   528             |> simp ? (simplified_rule' ctxt #> unmark_constraints ctxt);
   529         in
   530           CONTEXT_CASES (Rule_Cases.make_common ctxt
   531               (Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
   532             ((Method.insert_tac ctxt facts'' THEN' resolve_tac ctxt [rule'] THEN_ALL_NEW
   533                 (if simp then TRY o trivial_tac ctxt else K all_tac)) i) (ctxt, st)
   534         end)
   535     end;
   536 
   537 fun cases_tac ctxt x1 x2 x3 x4 x5 =
   538   Method.NO_CONTEXT_TACTIC ctxt (cases_context_tactic x1 x2 x3 x4 x5);
   539 
   540 end;
   541 
   542 
   543 
   544 (** induct method **)
   545 
   546 val conjunction_congs = @{thms Pure.all_conjunction imp_conjunction};
   547 
   548 
   549 (* atomize *)
   550 
   551 fun atomize_term ctxt =
   552   Raw_Simplifier.rewrite_term (Proof_Context.theory_of ctxt) Induct_Args.atomize []
   553   #> Object_Logic.drop_judgment ctxt;
   554 
   555 fun atomize_cterm ctxt = Raw_Simplifier.rewrite ctxt true Induct_Args.atomize;
   556 
   557 fun atomize_tac ctxt = rewrite_goal_tac ctxt Induct_Args.atomize;
   558 
   559 fun inner_atomize_tac ctxt =
   560   rewrite_goal_tac ctxt (map Thm.symmetric conjunction_congs) THEN' atomize_tac ctxt;
   561 
   562 
   563 (* rulify *)
   564 
   565 fun rulify_term thy =
   566   Raw_Simplifier.rewrite_term thy (Induct_Args.rulify @ conjunction_congs) [] #>
   567   Raw_Simplifier.rewrite_term thy Induct_Args.rulify_fallback [];
   568 
   569 fun rulified_term ctxt thm =
   570   let
   571     val rulify = rulify_term (Proof_Context.theory_of ctxt);
   572     val (As, B) = Logic.strip_horn (Thm.prop_of thm);
   573   in Logic.list_implies (map rulify As, rulify B) end;
   574 
   575 fun rulify_tac ctxt =
   576   rewrite_goal_tac ctxt (Induct_Args.rulify @ conjunction_congs) THEN'
   577   rewrite_goal_tac ctxt Induct_Args.rulify_fallback THEN'
   578   Goal.conjunction_tac THEN_ALL_NEW
   579   (rewrite_goal_tac ctxt @{thms Pure.conjunction_imp} THEN' Goal.norm_hhf_tac ctxt);
   580 
   581 
   582 (* prepare rule *)
   583 
   584 fun rule_instance ctxt inst rule =
   585   infer_instantiate ctxt (prep_inst ctxt align_left I (Thm.prop_of rule, inst)) rule;
   586 
   587 fun internalize ctxt k th =
   588   th |> Thm.permute_prems 0 k
   589   |> Conv.fconv_rule (Conv.concl_conv (Thm.nprems_of th - k) (atomize_cterm ctxt));
   590 
   591 
   592 (* guess rule instantiation -- cannot handle pending goal parameters *)
   593 
   594 local
   595 
   596 fun dest_env ctxt env =
   597   let
   598     val pairs = Vartab.dest (Envir.term_env env);
   599     val types = Vartab.dest (Envir.type_env env);
   600     val ts = map (Thm.cterm_of ctxt o Envir.norm_term env o #2 o #2) pairs;
   601     val xs = map #1 pairs ~~ map Thm.typ_of_cterm ts;
   602   in (map (fn (ai, (S, T)) => ((ai, S), Thm.ctyp_of ctxt T)) types, xs ~~ ts) end;
   603 
   604 in
   605 
   606 fun guess_instance ctxt rule i st =
   607   let
   608     val maxidx = Thm.maxidx_of st;
   609     val goal = Thm.term_of (Thm.cprem_of st i);  (*exception Subscript*)
   610     val params = rev (Term.rename_wrt_term goal (Logic.strip_params goal));
   611   in
   612     if not (null params) then
   613       (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^
   614         commas_quote (map (Syntax.string_of_term ctxt o Syntax_Trans.mark_bound_abs) params));
   615       Seq.single rule)
   616     else
   617       let
   618         val rule' = Thm.incr_indexes (maxidx + 1) rule;
   619         val concl = Logic.strip_assums_concl goal;
   620       in
   621         Unify.smash_unifiers (Context.Proof ctxt)
   622           [(Thm.concl_of rule', concl)] (Envir.empty (Thm.maxidx_of rule'))
   623         |> Seq.map (fn env => Drule.instantiate_normalize (dest_env ctxt env) rule')
   624       end
   625   end
   626   handle General.Subscript => Seq.empty;
   627 
   628 end;
   629 
   630 
   631 (* special renaming of rule parameters *)
   632 
   633 fun special_rename_params ctxt [[SOME (Free (z, Type (T, _)))]] [thm] =
   634       let
   635         val x = Name.clean (Variable.revert_fixed ctxt z);
   636         fun index _ [] = []
   637           | index i (y :: ys) =
   638               if x = y then x ^ string_of_int i :: index (i + 1) ys
   639               else y :: index i ys;
   640         fun rename_params [] = []
   641           | rename_params ((y, Type (U, _)) :: ys) =
   642               (if U = T then x else y) :: rename_params ys
   643           | rename_params ((y, _) :: ys) = y :: rename_params ys;
   644         fun rename_asm A =
   645           let
   646             val xs = rename_params (Logic.strip_params A);
   647             val xs' =
   648               (case filter (fn x' => x' = x) xs of
   649                 [] => xs
   650               | [_] => xs
   651               | _ => index 1 xs);
   652           in Logic.list_rename_params xs' A end;
   653         fun rename_prop prop =
   654           let val (As, C) = Logic.strip_horn prop
   655           in Logic.list_implies (map rename_asm As, C) end;
   656         val thm' = Thm.renamed_prop (rename_prop (Thm.prop_of thm)) thm;
   657       in [Rule_Cases.save thm thm'] end
   658   | special_rename_params _ _ ths = ths;
   659 
   660 
   661 (* arbitrary_tac *)
   662 
   663 local
   664 
   665 fun goal_prefix k ((c as Const (@{const_name Pure.all}, _)) $ Abs (a, T, B)) =
   666       c $ Abs (a, T, goal_prefix k B)
   667   | goal_prefix 0 _ = Term.dummy_prop
   668   | goal_prefix k ((c as Const (@{const_name Pure.imp}, _)) $ A $ B) =
   669       c $ A $ goal_prefix (k - 1) B
   670   | goal_prefix _ _ = Term.dummy_prop;
   671 
   672 fun goal_params k (Const (@{const_name Pure.all}, _) $ Abs (_, _, B)) = goal_params k B + 1
   673   | goal_params 0 _ = 0
   674   | goal_params k (Const (@{const_name Pure.imp}, _) $ _ $ B) = goal_params (k - 1) B
   675   | goal_params _ _ = 0;
   676 
   677 fun meta_spec_tac ctxt n (x, T) = SUBGOAL (fn (goal, i) =>
   678   let
   679     val v = Free (x, T);
   680     fun spec_rule prfx (xs, body) =
   681       @{thm Pure.meta_spec}
   682       |> Thm.rename_params_rule ([Name.clean (Variable.revert_fixed ctxt x)], 1)
   683       |> Thm.lift_rule (Thm.cterm_of ctxt prfx)
   684       |> `(Thm.prop_of #> Logic.strip_assums_concl)
   685       |-> (fn pred $ arg =>
   686         infer_instantiate ctxt
   687           [(#1 (dest_Var (head_of pred)), Thm.cterm_of ctxt (Logic.rlist_abs (xs, body))),
   688            (#1 (dest_Var (head_of arg)), Thm.cterm_of ctxt (Logic.rlist_abs (xs, v)))]);
   689 
   690     fun goal_concl k xs (Const (@{const_name Pure.all}, _) $ Abs (a, T, B)) =
   691           goal_concl k ((a, T) :: xs) B
   692       | goal_concl 0 xs B =
   693           if not (Term.exists_subterm (fn t => t aconv v) B) then NONE
   694           else SOME (xs, absfree (x, T) (Term.incr_boundvars 1 B))
   695       | goal_concl k xs (Const (@{const_name Pure.imp}, _) $ _ $ B) =
   696           goal_concl (k - 1) xs B
   697       | goal_concl _ _ _ = NONE;
   698   in
   699     (case goal_concl n [] goal of
   700       SOME concl =>
   701         (compose_tac ctxt (false, spec_rule (goal_prefix n goal) concl, 1) THEN'
   702           resolve_tac ctxt [asm_rl]) i
   703     | NONE => all_tac)
   704   end);
   705 
   706 fun miniscope_tac p =
   707   CONVERSION o
   708     Conv.params_conv p (fn ctxt =>
   709       Raw_Simplifier.rewrite ctxt true [Thm.symmetric Drule.norm_hhf_eq]);
   710 
   711 in
   712 
   713 fun arbitrary_tac _ _ [] = K all_tac
   714   | arbitrary_tac ctxt n xs = SUBGOAL (fn (goal, i) =>
   715      (EVERY' (map (meta_spec_tac ctxt n) xs) THEN'
   716       (miniscope_tac (goal_params n goal) ctxt)) i);
   717 
   718 end;
   719 
   720 
   721 (* add_defs *)
   722 
   723 fun add_defs def_insts =
   724   let
   725     fun add (SOME (_, (t, true))) ctxt = ((SOME t, []), ctxt)
   726       | add (SOME (SOME x, (t, _))) ctxt =
   727           let val ([(lhs, (_, th))], ctxt') =
   728             Local_Defs.define [((x, NoSyn), ((Thm.def_binding x, []), t))] ctxt
   729           in ((SOME lhs, [th]), ctxt') end
   730       | add (SOME (NONE, (t as Free _, _))) ctxt = ((SOME t, []), ctxt)
   731       | add (SOME (NONE, (t, _))) ctxt =
   732           let
   733             val (s, _) = Name.variant "x" (Variable.names_of ctxt);
   734             val x = Binding.name s;
   735             val ([(lhs, (_, th))], ctxt') = ctxt
   736               |> Local_Defs.define [((x, NoSyn), ((Thm.def_binding x, []), t))];
   737           in ((SOME lhs, [th]), ctxt') end
   738       | add NONE ctxt = ((NONE, []), ctxt);
   739   in fold_map add def_insts #> apfst (split_list #> apsnd flat) end;
   740 
   741 
   742 (* induct_tac *)
   743 
   744 (*
   745   rule selection scheme:
   746     `A x` induct ...     - predicate/set induction
   747           induct x       - type induction
   748     ...   induct ... r   - explicit rule
   749 *)
   750 
   751 fun get_inductT ctxt insts =
   752   fold_rev (map_product cons) (insts |> map
   753       ((fn [] => NONE | ts => List.last ts) #>
   754         (fn NONE => TVar (("'a", 0), []) | SOME t => Term.fastype_of t) #>
   755         find_inductT ctxt)) [[]]
   756   |> filter_out (forall Rule_Cases.is_inner_rule);
   757 
   758 fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
   759   | get_inductP _ _ = [];
   760 
   761 fun gen_induct_context_tactic mod_cases simp def_insts arbitrary taking opt_rule facts =
   762   CONTEXT_SUBGOAL (fn (_, i) => fn (ctxt, st) =>
   763     let
   764       val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
   765       val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs;
   766 
   767       fun inst_rule (concls, r) =
   768         (if null insts then `Rule_Cases.get r
   769          else (align_left "Rule has fewer conclusions than arguments given"
   770             (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
   771           |> maps (prep_inst ctxt align_right (atomize_term ctxt))
   772           |> infer_instantiate ctxt) r |> pair (Rule_Cases.get r))
   773         |> mod_cases
   774         |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
   775 
   776       val ruleq =
   777         (case opt_rule of
   778           SOME rs => Seq.single (inst_rule (Rule_Cases.strict_mutual_rule ctxt rs))
   779         | NONE =>
   780             (get_inductP ctxt facts @
   781               map (special_rename_params defs_ctxt insts) (get_inductT ctxt insts))
   782             |> map_filter (Rule_Cases.mutual_rule ctxt)
   783             |> tap (trace_rules ctxt inductN o map #2)
   784             |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
   785 
   786       fun rule_cases ctxt rule cases =
   787         let
   788           val rule' = Rule_Cases.internalize_params rule;
   789           val rule'' = rule' |> simp ? simplified_rule ctxt;
   790           val nonames = map (fn ((cn, _), cls) => ((cn, []), cls));
   791           val cases' = if Thm.eq_thm_prop (rule', rule'') then cases else nonames cases;
   792         in Rule_Cases.make_nested ctxt (Thm.prop_of rule'') (rulified_term ctxt rule'') cases' end;
   793 
   794       fun context_tac _ _ =
   795         ruleq
   796         |> Seq.maps (Rule_Cases.consume defs_ctxt (flat defs) facts)
   797         |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
   798           (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
   799             (CONJUNCTS (ALLGOALS
   800               let
   801                 val adefs = nth_list atomized_defs (j - 1);
   802                 val frees = fold (Term.add_frees o Thm.prop_of) adefs [];
   803                 val xs = nth_list arbitrary (j - 1);
   804                 val k = nth concls (j - 1) + more_consumes;
   805               in
   806                 Method.insert_tac defs_ctxt (more_facts @ adefs) THEN'
   807                   (if simp then
   808                      rotate_tac k (length adefs) THEN'
   809                      arbitrary_tac defs_ctxt k (List.partition (member op = frees) xs |> op @)
   810                    else
   811                      arbitrary_tac defs_ctxt k xs)
   812                end)
   813             THEN' inner_atomize_tac defs_ctxt) j))
   814           THEN' atomize_tac defs_ctxt) i st
   815         |> Seq.maps (fn st' =>
   816               guess_instance ctxt (internalize ctxt more_consumes rule) i st'
   817               |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
   818               |> Seq.maps (fn rule' =>
   819                 CONTEXT_CASES (rule_cases ctxt rule' cases)
   820                   (resolve_tac ctxt [rule'] i THEN
   821                     PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) (ctxt, st'))));
   822     in
   823       (context_tac CONTEXT_THEN_ALL_NEW
   824         ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac ctxt) else K all_tac)
   825          THEN_ALL_NEW rulify_tac ctxt)) i (ctxt, st)
   826     end)
   827 
   828 val induct_context_tactic = gen_induct_context_tactic I;
   829 
   830 fun gen_induct_tac ctxt x1 x2 x3 x4 x5 x6 x7 x8 =
   831   Method.NO_CONTEXT_TACTIC ctxt (gen_induct_context_tactic x1 x2 x3 x4 x5 x6 x7 x8);
   832 
   833 fun induct_tac ctxt x1 x2 x3 x4 x5 x6 x7 =
   834   Method.NO_CONTEXT_TACTIC ctxt (induct_context_tactic x1 x2 x3 x4 x5 x6 x7);
   835 
   836 
   837 
   838 (** coinduct method **)
   839 
   840 (*
   841   rule selection scheme:
   842     goal "A x" coinduct ...   - predicate/set coinduction
   843                coinduct x     - type coinduction
   844                coinduct ... r - explicit rule
   845 *)
   846 
   847 local
   848 
   849 fun get_coinductT ctxt (SOME t :: _) = find_coinductT ctxt (Term.fastype_of t)
   850   | get_coinductT _ _ = [];
   851 
   852 fun get_coinductP ctxt goal = find_coinductP ctxt (Logic.strip_assums_concl goal);
   853 
   854 fun main_prop_of th =
   855   if Rule_Cases.get_consumes th > 0 then Thm.major_prem_of th else Thm.concl_of th;
   856 
   857 in
   858 
   859 fun coinduct_context_tactic inst taking opt_rule facts =
   860   CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) =>
   861     let
   862       fun inst_rule r =
   863         if null inst then `Rule_Cases.get r
   864         else
   865           infer_instantiate ctxt (prep_inst ctxt align_right I (main_prop_of r, inst)) r
   866           |> pair (Rule_Cases.get r);
   867     in
   868       (case opt_rule of
   869         SOME r => Seq.single (inst_rule r)
   870       | NONE =>
   871           (get_coinductP ctxt goal @ get_coinductT ctxt inst)
   872           |> tap (trace_rules ctxt coinductN)
   873           |> Seq.of_list |> Seq.maps (Seq.try inst_rule))
   874       |> Seq.maps (Rule_Cases.consume ctxt [] facts)
   875       |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
   876         guess_instance ctxt rule i st
   877         |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
   878         |> Seq.maps (fn rule' =>
   879           CONTEXT_CASES (Rule_Cases.make_common ctxt
   880               (Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
   881             (Method.insert_tac ctxt more_facts i THEN resolve_tac ctxt [rule'] i) (ctxt, st)))
   882     end);
   883 
   884 fun coinduct_tac ctxt x1 x2 x3 x4 x5 =
   885   Method.NO_CONTEXT_TACTIC ctxt (coinduct_context_tactic x1 x2 x3 x4 x5);
   886 
   887 end;
   888 
   889 
   890 
   891 (** concrete syntax **)
   892 
   893 val arbitraryN = "arbitrary";
   894 val takingN = "taking";
   895 val ruleN = "rule";
   896 
   897 local
   898 
   899 fun single_rule [rule] = rule
   900   | single_rule _ = error "Single rule expected";
   901 
   902 fun named_rule k arg get =
   903   Scan.lift (Args.$$$ k -- Args.colon) |-- Scan.repeat arg :|--
   904     (fn names => Scan.peek (fn context => Scan.succeed (names |> map (fn name =>
   905       (case get (Context.proof_of context) name of SOME x => x
   906       | NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
   907 
   908 fun rule get_type get_pred =
   909   named_rule typeN (Args.type_name {proper = false, strict = false}) get_type ||
   910   named_rule predN (Args.const {proper = false, strict = false}) get_pred ||
   911   named_rule setN (Args.const {proper = false, strict = false}) get_pred ||
   912   Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;
   913 
   914 val cases_rule = rule lookup_casesT lookup_casesP >> single_rule;
   915 val induct_rule = rule lookup_inductT lookup_inductP;
   916 val coinduct_rule = rule lookup_coinductT lookup_coinductP >> single_rule;
   917 
   918 val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME;
   919 
   920 val inst' = Scan.lift (Args.$$$ "_") >> K NONE ||
   921   Args.term >> (SOME o rpair false) ||
   922   Scan.lift (Args.$$$ "(") |-- (Args.term >> (SOME o rpair true)) --|
   923     Scan.lift (Args.$$$ ")");
   924 
   925 val def_inst =
   926   ((Scan.lift (Args.binding --| (Args.$$$ "\<equiv>" || Args.$$$ "==")) >> SOME)
   927       -- (Args.term >> rpair false)) >> SOME ||
   928     inst' >> Option.map (pair NONE);
   929 
   930 val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
   931   error ("Bad free variable: " ^ Syntax.string_of_term ctxt t));
   932 
   933 fun unless_more_args scan = Scan.unless (Scan.lift
   934   ((Args.$$$ arbitraryN || Args.$$$ takingN || Args.$$$ typeN ||
   935     Args.$$$ predN || Args.$$$ setN || Args.$$$ ruleN) -- Args.colon)) scan;
   936 
   937 val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN -- Args.colon) |--
   938   Parse.and_list1' (Scan.repeat (unless_more_args free))) [];
   939 
   940 val taking = Scan.optional (Scan.lift (Args.$$$ takingN -- Args.colon) |--
   941   Scan.repeat1 (unless_more_args inst)) [];
   942 
   943 in
   944 
   945 fun gen_induct_setup binding tac =
   946   Method.local_setup binding
   947     (Scan.lift (Args.mode no_simpN) --
   948       (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
   949         (arbitrary -- taking -- Scan.option induct_rule)) >>
   950       (fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn _ => fn facts =>
   951         Seq.DETERM (tac (not no_simp) insts arbitrary taking opt_rule facts 1)))
   952     "induction on types or predicates/sets";
   953 
   954 val _ =
   955   Theory.local_setup
   956     (Method.local_setup \<^binding>\<open>cases\<close>
   957       (Scan.lift (Args.mode no_simpN) --
   958         (Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
   959         (fn (no_simp, (insts, opt_rule)) => fn _ =>
   960           CONTEXT_METHOD (fn facts =>
   961             Seq.DETERM (cases_context_tactic (not no_simp) insts opt_rule facts 1))))
   962       "case analysis on types or predicates/sets" #>
   963     gen_induct_setup \<^binding>\<open>induct\<close> induct_context_tactic #>
   964      Method.local_setup \<^binding>\<open>coinduct\<close>
   965       (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
   966         (fn ((insts, taking), opt_rule) => fn _ => fn facts =>
   967           Seq.DETERM (coinduct_context_tactic insts taking opt_rule facts 1)))
   968       "coinduction on types or predicates/sets");
   969 
   970 end;
   971 
   972 end;