src/Tools/cong_tac.ML
author wenzelm
Thu, 07 Apr 2016 20:51:52 +0200
changeset 62908 d7009a515733
parent 60784 4f590c08fd5d
permissions -rw-r--r--
clarified mode of ROOT.ML files;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32733
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
diff changeset
     1
(*  Title:      Tools/cong_tac.ML
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
diff changeset
     2
    Author:     Stefan Berghofer, TU Muenchen
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
diff changeset
     3
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
diff changeset
     4
Congruence tactic based on explicit instantiation.
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
diff changeset
     5
*)
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
diff changeset
     6
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
diff changeset
     7
signature CONG_TAC =
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
diff changeset
     8
sig
58956
a816aa3ff391 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents: 55627
diff changeset
     9
  val cong_tac: Proof.context -> thm -> int -> tactic
32733
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
diff changeset
    10
end;
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
diff changeset
    11
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
diff changeset
    12
structure Cong_Tac: CONG_TAC =
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
diff changeset
    13
struct
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
diff changeset
    14
58956
a816aa3ff391 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents: 55627
diff changeset
    15
fun cong_tac ctxt cong = CSUBGOAL (fn (cgoal, i) =>
32733
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
diff changeset
    16
  let
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
diff changeset
    17
    val goal = Thm.term_of cgoal;
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
diff changeset
    18
  in
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
diff changeset
    19
    (case Logic.strip_assums_concl goal of
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
diff changeset
    20
      _ $ (_ $ (f $ x) $ (g $ y)) =>
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
diff changeset
    21
        let
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
diff changeset
    22
          val cong' = Thm.lift_rule cgoal cong;
55627
95c8ef02f04b tuned whitespace;
wenzelm
parents: 46219
diff changeset
    23
          val _ $ (_ $ (f' $ x') $ (g' $ y')) = Logic.strip_assums_concl (Thm.prop_of cong');
32733
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
diff changeset
    24
          val ps = Logic.strip_params (Thm.concl_of cong');
55627
95c8ef02f04b tuned whitespace;
wenzelm
parents: 46219
diff changeset
    25
          val insts =
60784
4f590c08fd5d updated to infer_instantiate;
wenzelm
parents: 59642
diff changeset
    26
            [(f', f), (g', g), (x', x), (y', y)] |> map (fn (t, u) =>
4f590c08fd5d updated to infer_instantiate;
wenzelm
parents: 59642
diff changeset
    27
              (#1 (dest_Var (head_of t)), Thm.cterm_of ctxt (fold_rev Term.abs ps u)));
32733
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
diff changeset
    28
        in
55627
95c8ef02f04b tuned whitespace;
wenzelm
parents: 46219
diff changeset
    29
          fn st =>
60784
4f590c08fd5d updated to infer_instantiate;
wenzelm
parents: 59642
diff changeset
    30
            compose_tac ctxt (false, infer_instantiate ctxt insts cong', 2) i st
55627
95c8ef02f04b tuned whitespace;
wenzelm
parents: 46219
diff changeset
    31
              handle THM _ => no_tac st
32733
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
diff changeset
    32
        end
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
diff changeset
    33
    | _ => no_tac)
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
diff changeset
    34
  end);
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
diff changeset
    35
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
diff changeset
    36
end;
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
diff changeset
    37