src/Tools/induct_tacs.ML
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (2 months ago)
changeset 69981 3dced198b9ec
parent 67149 e61557884799
permissions -rw-r--r--
more strict AFP properties;
haftmann@28308
     1
(*  Title:      Tools/induct_tacs.ML
wenzelm@27326
     2
    Author:     Makarius
wenzelm@27326
     3
wenzelm@27326
     4
Unstructured induction and cases analysis.
wenzelm@27326
     5
*)
wenzelm@27326
     6
wenzelm@27326
     7
signature INDUCT_TACS =
wenzelm@27326
     8
sig
wenzelm@59802
     9
  val case_tac: Proof.context -> string -> (binding * string option * mixfix) list ->
wenzelm@59826
    10
    thm option -> int -> tactic
wenzelm@59826
    11
  val induct_tac: Proof.context -> string option list list ->
wenzelm@59826
    12
    thm list option -> int -> tactic
wenzelm@27326
    13
end
wenzelm@27326
    14
wenzelm@45133
    15
structure Induct_Tacs: INDUCT_TACS =
wenzelm@27326
    16
struct
wenzelm@27326
    17
wenzelm@27326
    18
(* case analysis *)
wenzelm@27326
    19
wenzelm@46836
    20
fun check_type ctxt (t, pos) =
wenzelm@27326
    21
  let
wenzelm@27326
    22
    val u = singleton (Variable.polymorphic ctxt) t;
wenzelm@27326
    23
    val U = Term.fastype_of u;
wenzelm@27326
    24
    val _ = Term.is_TVar U andalso
wenzelm@55715
    25
      error ("Cannot determine type of " ^
wenzelm@55715
    26
        quote (Syntax.string_of_term ctxt u) ^ Position.here pos);
wenzelm@27326
    27
  in (u, U) end;
wenzelm@27326
    28
wenzelm@59829
    29
fun case_tac ctxt s fixes opt_rule = SUBGOAL (fn (goal, i) =>
wenzelm@27326
    30
  let
wenzelm@27326
    31
    val rule =
wenzelm@27326
    32
      (case opt_rule of
wenzelm@27326
    33
        SOME rule => rule
wenzelm@27326
    34
      | NONE =>
wenzelm@59802
    35
          let
wenzelm@59827
    36
            val (t, ctxt') = ctxt
wenzelm@59829
    37
              |> Rule_Insts.goal_context goal |> #2
wenzelm@59827
    38
              |> Context_Position.set_visible false
wenzelm@59827
    39
              |> Rule_Insts.read_term s;
wenzelm@59827
    40
            val pos = Syntax.read_input_pos s;
wenzelm@59802
    41
          in
wenzelm@59827
    42
            (case Induct.find_casesT ctxt' (#2 (check_type ctxt' (t, pos))) of
wenzelm@59802
    43
              rule :: _ => rule
wenzelm@59802
    44
            | [] => @{thm case_split})
wenzelm@59802
    45
          end);
wenzelm@27326
    46
    val _ = Method.trace ctxt [rule];
wenzelm@59829
    47
  in
wenzelm@59829
    48
    (case Induct.vars_of (Thm.term_of (Thm.cprem_of rule 1)) handle THM _ => [] of
wenzelm@59829
    49
      Var (xi, _) :: _ => Rule_Insts.res_inst_tac ctxt [((xi, Position.none), s)] fixes rule i
wenzelm@59829
    50
    | _ => no_tac)
wenzelm@59829
    51
  end);
wenzelm@27326
    52
wenzelm@27326
    53
wenzelm@27326
    54
(* induction *)
wenzelm@27326
    55
wenzelm@27326
    56
local
wenzelm@27326
    57
wenzelm@59755
    58
fun prep_var (Var (xi, _), SOME x) = SOME ((xi, Position.none), x)
wenzelm@27326
    59
  | prep_var _ = NONE;
wenzelm@27326
    60
wenzelm@27326
    61
fun prep_inst (concl, xs) =
wenzelm@27326
    62
  let val vs = Induct.vars_of concl
haftmann@33957
    63
  in map_filter prep_var (drop (length vs - length xs) vs ~~ xs) end;
wenzelm@27326
    64
wenzelm@27326
    65
in
wenzelm@27326
    66
wenzelm@59830
    67
fun induct_tac ctxt varss opt_rules i st =
wenzelm@27326
    68
  let
wenzelm@59830
    69
    val goal = Thm.cprem_of st i;
wenzelm@59830
    70
    val (_, goal_ctxt) = Rule_Insts.goal_context (Thm.term_of goal) ctxt
wenzelm@60695
    71
    and ((_, goal'), _) = Variable.focus_cterm NONE goal ctxt;
wenzelm@59830
    72
    val (prems, concl) = Logic.strip_horn (Thm.term_of goal');
wenzelm@27326
    73
wenzelm@27326
    74
    fun induct_var name =
wenzelm@27326
    75
      let
wenzelm@59830
    76
        val t = Syntax.read_term goal_ctxt name;
wenzelm@59795
    77
        val pos = Syntax.read_input_pos name;
wenzelm@27326
    78
        val (x, _) = Term.dest_Free t handle TERM _ =>
wenzelm@46836
    79
          error ("Induction argument not a variable: " ^
wenzelm@59830
    80
            quote (Syntax.string_of_term goal_ctxt t) ^ Position.here pos);
wenzelm@27326
    81
        val eq_x = fn Free (y, _) => x = y | _ => false;
wenzelm@27326
    82
        val _ =
wenzelm@27326
    83
          if Term.exists_subterm eq_x concl then ()
wenzelm@46836
    84
          else
wenzelm@46836
    85
            error ("No such variable in subgoal: " ^
wenzelm@59830
    86
              quote (Syntax.string_of_term goal_ctxt t) ^ Position.here pos);
wenzelm@27326
    87
        val _ =
wenzelm@27326
    88
          if (exists o Term.exists_subterm) eq_x prems then
wenzelm@46836
    89
            warning ("Induction variable occurs also among premises: " ^
wenzelm@59830
    90
              quote (Syntax.string_of_term goal_ctxt t) ^ Position.here pos)
wenzelm@27326
    91
          else ();
wenzelm@59830
    92
      in #1 (check_type goal_ctxt (t, pos)) end;
wenzelm@27326
    93
wenzelm@59830
    94
    val argss = (map o map o Option.map) induct_var varss;
wenzelm@27326
    95
    val rule =
wenzelm@27326
    96
      (case opt_rules of
wenzelm@33368
    97
        SOME rules => #2 (Rule_Cases.strict_mutual_rule ctxt rules)
wenzelm@27326
    98
      | NONE =>
wenzelm@33368
    99
          (case map_filter (Rule_Cases.mutual_rule ctxt) (Induct.get_inductT ctxt argss) of
wenzelm@27326
   100
            (_, rule) :: _ => rule
wenzelm@27326
   101
          | [] => raise THM ("No induction rules", 0, [])));
wenzelm@27326
   102
wenzelm@54742
   103
    val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 (Object_Logic.atomize ctxt));
wenzelm@27326
   104
    val _ = Method.trace ctxt [rule'];
wenzelm@27326
   105
wenzelm@27326
   106
    val concls = Logic.dest_conjunctions (Thm.concl_of rule);
wenzelm@40722
   107
    val insts = maps prep_inst (concls ~~ varss) handle ListPair.UnequalLengths =>
wenzelm@27326
   108
      error "Induction rule has different numbers of variables";
wenzelm@59780
   109
  in Rule_Insts.res_inst_tac ctxt insts [] rule' i st end
wenzelm@27326
   110
  handle THM _ => Seq.empty;
wenzelm@27326
   111
wenzelm@27326
   112
end;
wenzelm@27326
   113
wenzelm@27326
   114
wenzelm@27326
   115
(* method syntax *)
wenzelm@27326
   116
wenzelm@27326
   117
local
wenzelm@27326
   118
wenzelm@27326
   119
val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.$$$ ":");
wenzelm@27326
   120
val opt_rule = Scan.option (rule_spec |-- Attrib.thm);
wenzelm@27326
   121
val opt_rules = Scan.option (rule_spec |-- Attrib.thms);
wenzelm@27326
   122
wenzelm@27326
   123
val varss =
wenzelm@55111
   124
  Parse.and_list'
wenzelm@63120
   125
    (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.embedded_inner_syntax))));
wenzelm@27326
   126
wenzelm@27326
   127
in
wenzelm@27326
   128
wenzelm@58826
   129
val _ =
wenzelm@58826
   130
  Theory.setup
wenzelm@67149
   131
   (Method.setup \<^binding>\<open>case_tac\<close>
wenzelm@63120
   132
      (Args.goal_spec -- Scan.lift (Args.embedded_inner_syntax -- Parse.for_fixes) -- opt_rule >>
wenzelm@59826
   133
        (fn ((quant, (s, xs)), r) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s xs r)))
wenzelm@58826
   134
      "unstructured case analysis on types" #>
wenzelm@67149
   135
    Method.setup \<^binding>\<open>induct_tac\<close>
wenzelm@58826
   136
      (Args.goal_spec -- varss -- opt_rules >>
wenzelm@59826
   137
        (fn ((quant, vs), rs) => fn ctxt => SIMPLE_METHOD'' quant (induct_tac ctxt vs rs)))
wenzelm@58826
   138
      "unstructured induction on types");
wenzelm@27326
   139
wenzelm@27326
   140
end;
wenzelm@27326
   141
wenzelm@27326
   142
end;