<commit_before>(*  Title:      HOL/Tools/induct_tacs.ML
    ID:         $Id$
    Author:     Makarius

Unstructured induction and cases analysis.
*)

signature INDUCT_TACS =
sig
  val case_tac: Proof.context -> string -> int -> tactic
  val case_rule_tac: Proof.context -> string -> thm -> int -> tactic
  val induct_tac: Proof.context -> string option list list -> int -> tactic
  val induct_rules_tac: Proof.context -> string option list list -> thm list -> int -> tactic
  val setup: theory -> theory
end

structure InductTacs: INDUCT_TACS =
struct

(* case analysis *)

fun check_type ctxt t =
  let
    val u = singleton (Variable.polymorphic ctxt) t;
    val U = Term.fastype_of u;
    val _ = Term.is_TVar U andalso
      error ("Cannot determine type of " ^ Syntax.string_of_term ctxt u);
  in (u, U) end;

fun gen_case_tac ctxt0 (s, opt_rule) i st =
  let
    val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
    val rule =
      (case opt_rule of
        SOME rule => rule
      | NONE =>
          (case Induct.find_casesT ctxt
              (#2 (check_type ctxt (ProofContext.read_term_schematic ctxt s))) of
            rule :: _ => rule
          | [] => @{thm case_split}));
    val _ = Method.trace ctxt [rule];

    val xi =
      (case Induct.vars_of (Thm.term_of (Thm.cprem_of rule 1)) of
        Var (xi, _) :: _ => xi
      | _ => raise THM ("Malformed cases rule", 0, [rule]));
  in res_inst_tac ctxt [(xi, s)] rule i st end
  handle THM _ => Seq.empty;

fun case_tac ctxt s = gen_case_tac ctxt (s, NONE);
fun case_rule_tac ctxt s rule = gen_case_tac ctxt (s, SOME rule);


(* induction *)

local

fun prep_var (Var (ixn, _), SOME x) = SOME (ixn, x)
  | prep_var _ = NONE;

fun prep_inst (concl, xs) =
  let val vs = Induct.vars_of concl
  in map_filter prep_var (Library.drop (length vs - length xs, vs) ~~ xs) end;

in

fun gen_induct_tac ctxt0 (varss, opt_rules) i st =
  let
    val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
    val (prems, concl) = Logic.strip_horn (Thm.term_of goal);

    fun induct_var name =
      let
        val t = Syntax.read_term ctxt name;
        val (x, _) = Term.dest_Free t handle TERM _ =>
          error ("Induction argument not a variable: " ^ Syntax.string_of_term ctxt t);
        val eq_x = fn Free (y, _) => x = y | _ => false;
        val _ =
          if Term.exists_subterm eq_x concl then ()
          else error ("No such variable in subgoal: " ^ Syntax.string_of_term ctxt t);
        val _ =
          if (exists o Term.exists_subterm) eq_x prems then
            warning ("Induction variable occurs also among premises: " ^ Syntax.string_of_term ctxt t)
          else ();
      in #1 (check_type ctxt t) end;

    val argss = map (map (Option.map induct_var)) varss;
    val _ = forall null argss andalso raise THM ("No induction arguments", 0, []);

    val rule =
      (case opt_rules of
        SOME rules => #2 (RuleCases.strict_mutual_rule ctxt rules)
      | NONE =>
          (case map_filter (RuleCases.mutual_rule ctxt) (Induct.get_inductT ctxt argss) of
            (_, rule) :: _ => rule
          | [] => raise THM ("No induction rules", 0, [])));

    val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 ObjectLogic.atomize);
    val _ = Method.trace ctxt [rule'];

    val concls = Logic.dest_conjunctions (Thm.concl_of rule);
    val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths =>
      error "Induction rule has different numbers of variables";
  in res_inst_tac ctxt insts rule' i st end
  handle THM _ => Seq.empty;

end;
<commit_msg>induct_tac: allow omission of arguments;<commit_after>(*  Title:      HOL/Tools/induct_tacs.ML
    ID:         $Id$
    Author:     Makarius

Unstructured induction and cases analysis.
*)

signature INDUCT_TACS =
sig
  val case_tac: Proof.context -> string -> int -> tactic
  val case_rule_tac: Proof.context -> string -> thm -> int -> tactic
  val induct_tac: Proof.context -> string option list list -> int -> tactic
  val induct_rules_tac: Proof.context -> string option list list -> thm list -> int -> tactic
  val setup: theory -> theory
end

structure InductTacs: INDUCT_TACS =
struct

(* case analysis *)

fun check_type ctxt t =
  let
    val u = singleton (Variable.polymorphic ctxt) t;
    val U = Term.fastype_of u;
    val _ = Term.is_TVar U andalso
      error ("Cannot determine type of " ^ Syntax.string_of_term ctxt u);
  in (u, U) end;

fun gen_case_tac ctxt0 (s, opt_rule) i st =
  let
    val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
    val rule =
      (case opt_rule of
        SOME rule => rule
      | NONE =>
          (case Induct.find_casesT ctxt
              (#2 (check_type ctxt (ProofContext.read_term_schematic ctxt s))) of
            rule :: _ => rule
          | [] => @{thm case_split}));
    val _ = Method.trace ctxt [rule];

    val xi =
      (case Induct.vars_of (Thm.term_of (Thm.cprem_of rule 1)) of
        Var (xi, _) :: _ => xi
      | _ => raise THM ("Malformed cases rule", 0, [rule]));
  in res_inst_tac ctxt [(xi, s)] rule i st end
  handle THM _ => Seq.empty;

fun case_tac ctxt s = gen_case_tac ctxt (s, NONE);
fun case_rule_tac ctxt s rule = gen_case_tac ctxt (s, SOME rule);


(* induction *)

local

fun prep_var (Var (ixn, _), SOME x) = SOME (ixn, x)
  | prep_var _ = NONE;

fun prep_inst (concl, xs) =
  let val vs = Induct.vars_of concl
  in map_filter prep_var (Library.drop (length vs - length xs, vs) ~~ xs) end;

in

fun gen_induct_tac ctxt0 (varss, opt_rules) i st =
  let
    val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
    val (prems, concl) = Logic.strip_horn (Thm.term_of goal);

    fun induct_var name =
      let
        val t = Syntax.read_term ctxt name;
        val (x, _) = Term.dest_Free t handle TERM _ =>
          error ("Induction argument not a variable: " ^ Syntax.string_of_term ctxt t);
        val eq_x = fn Free (y, _) => x = y | _ => false;
        val _ =
          if Term.exists_subterm eq_x concl then ()
          else error ("No such variable in subgoal: " ^ Syntax.string_of_term ctxt t);
        val _ =
          if (exists o Term.exists_subterm) eq_x prems then
            warning ("Induction variable occurs also among premises: " ^ Syntax.string_of_term ctxt t)
          else ();
      in #1 (check_type ctxt t) end;

    val argss = map (map (Option.map induct_var)) varss;
    val rule =
      (case opt_rules of
        SOME rules => #2 (RuleCases.strict_mutual_rule ctxt rules)
      | NONE =>
          (case map_filter (RuleCases.mutual_rule ctxt) (Induct.get_inductT ctxt argss) of
            (_, rule) :: _ => rule
          | [] => raise THM ("No induction rules", 0, [])));

    val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 ObjectLogic.atomize);
    val _ = Method.trace ctxt [rule'];

    val concls = Logic.dest_conjunctions (Thm.concl_of rule);
    val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths =>
      error "Induction rule has different numbers of variables";
  in res_inst_tac ctxt insts rule' i st end
  handle THM _ => Seq.empty;

end;

{'fraction_non_alphanumeric': 0.11003236245954692, 'fraction_numerical': 0.003236245954692557, 'mean_word_length': 2.6154628687690744, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 67, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '482393', 'n_tokens_mistral': 2555, 'n_tokens_neox': 2471, 'n_words': 793}