src/Provers/induct_method.ML
author wenzelm
Tue, 10 Jan 2006 19:33:30 +0100
changeset 18631 ca56111fe69c
parent 18602 8f25a0f7f446
child 18678 dd0c569fa43d
permissions -rw-r--r--
fix_tac: no warning;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
     1
(*  Title:      Provers/induct_method.ML
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
     4
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
     5
Proof by cases and induction on sets and types.
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
     6
*)
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
     7
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
     8
signature INDUCT_METHOD_DATA =
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
     9
sig
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    10
  val cases_default: thm
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    11
  val atomize: thm list
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
    12
  val rulify: thm list
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
    13
  val rulify_fallback: thm list
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    14
end;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    15
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    16
signature INDUCT_METHOD =
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    17
sig
18250
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
    18
  val fix_tac: Proof.context -> int -> (string * typ) list -> int -> tactic
18287
28efcdae34dc moved nth_list to Pure/library.ML;
wenzelm
parents: 18259
diff changeset
    19
  val add_defs: (string option * term) option list -> Proof.context ->
28efcdae34dc moved nth_list to Pure/library.ML;
wenzelm
parents: 18259
diff changeset
    20
    (term option list * thm list) * Proof.context
18250
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
    21
  val atomize_term: theory -> term -> term
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
    22
  val atomize_tac: int -> tactic
18512
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
    23
  val inner_atomize_tac: int -> tactic
18250
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
    24
  val rulified_term: thm -> theory * term
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
    25
  val rulify_tac: int -> tactic
18580
4fdd39ea2f40 RuleCases.strict_mutual_rule;
wenzelm
parents: 18512
diff changeset
    26
  val internalize: int -> thm -> thm
18259
7b14579c58f2 induct: insert defs in object-logic form;
wenzelm
parents: 18250
diff changeset
    27
  val guess_instance: thm -> int -> thm -> thm Seq.seq
16391
65c8070844ea export cases_tac, induct_tac;
wenzelm
parents: 15794
diff changeset
    28
  val cases_tac: Proof.context -> bool -> term option list list -> thm option ->
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
    29
    thm list -> int -> cases_tactic
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
    30
  val induct_tac: Proof.context -> bool -> (string option * term) option list list ->
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
    31
    (string * typ) list list -> term option list -> thm list option -> thm list -> int ->
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
    32
    cases_tactic
18235
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
    33
  val coinduct_tac: Proof.context -> bool -> term option list -> term option list ->
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
    34
    thm option -> thm list -> int -> cases_tactic
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    35
  val setup: (theory -> theory) list
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    36
end;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    37
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    38
functor InductMethodFun(Data: INDUCT_METHOD_DATA): INDUCT_METHOD =
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    39
struct
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    40
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
    41
val meta_spec = thm "Pure.meta_spec";
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
    42
val all_conjunction = thm "Pure.all_conjunction";
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
    43
val imp_conjunction = thm "Pure.imp_conjunction";
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
    44
val conjunction_imp = thm "Pure.conjunction_imp";
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
    45
val conjunction_assoc = thm "Pure.conjunction_assoc";
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
    46
val conjunction_congs = [all_conjunction, imp_conjunction];
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
    47
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
    48
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    49
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    50
(** misc utils **)
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    51
18287
28efcdae34dc moved nth_list to Pure/library.ML;
wenzelm
parents: 18259
diff changeset
    52
(* alignment *)
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    53
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    54
fun align_left msg xs ys =
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    55
  let val m = length xs and n = length ys
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    56
  in if m < n then raise ERROR_MESSAGE msg else (Library.take (n, xs) ~~ ys) end;
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    57
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    58
fun align_right msg xs ys =
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    59
  let val m = length xs and n = length ys
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    60
  in if m < n then raise ERROR_MESSAGE msg else (Library.drop (m - n, xs) ~~ ys) end;
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    61
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    62
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    63
(* prep_inst *)
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    64
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
    65
fun prep_inst thy align tune (tm, ts) =
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    66
  let
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
    67
    val cert = Thm.cterm_of thy;
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15235
diff changeset
    68
    fun prep_var (x, SOME t) =
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    69
          let
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    70
            val cx = cert x;
18147
31634a2af39e induct method: fixes;
wenzelm
parents: 18023
diff changeset
    71
            val {T = xT, thy, ...} = Thm.rep_cterm cx;
12799
5472afdd3bd3 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents: 12305
diff changeset
    72
            val ct = cert (tune t);
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    73
          in
18147
31634a2af39e induct method: fixes;
wenzelm
parents: 18023
diff changeset
    74
            if Sign.typ_instance thy (#T (Thm.rep_cterm ct), xT) then SOME (cx, ct)
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    75
            else raise ERROR_MESSAGE (Pretty.string_of (Pretty.block
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    76
             [Pretty.str "Ill-typed instantiation:", Pretty.fbrk,
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    77
              Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1,
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    78
              Display.pretty_ctyp (#T (Thm.crep_cterm ct))]))
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    79
          end
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15235
diff changeset
    80
      | prep_var (_, NONE) = NONE;
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    81
    val xs = InductAttrib.vars_of tm;
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    82
  in
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    83
    align "Rule has fewer variables than instantiations given" xs ts
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
    84
    |> List.mapPartial prep_var
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    85
  end;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    86
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    87
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
    88
(* trace_rules *)
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
    89
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
    90
fun trace_rules _ kind [] = error ("Unable to figure out " ^ kind ^ " rule")
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
    91
  | trace_rules ctxt _ rules = Method.trace ctxt rules;
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
    92
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
    93
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
    94
(* make_cases *)
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
    95
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
    96
fun make_cases is_open rule =
18602
8f25a0f7f446 RuleCases.make_common/nested;
wenzelm
parents: 18580
diff changeset
    97
  RuleCases.make_common is_open (Thm.theory_of_thm rule, Thm.prop_of rule);
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
    98
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
    99
fun warn_open true = warning "Encountered open rule cases -- deprecated"
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   100
  | warn_open false = ();
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   101
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   102
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   103
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   104
(** cases method **)
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   105
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   106
(*
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   107
  rule selection scheme:
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   108
          cases         - default case split
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   109
    `x:A` cases ...     - set cases
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   110
          cases t       - type cases
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   111
    ...   cases ... r   - explicit rule
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   112
*)
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   113
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   114
local
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   115
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   116
fun find_casesT ctxt ((SOME t :: _) :: _) = InductAttrib.find_casesT ctxt (Term.fastype_of t)
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   117
  | find_casesT _ _ = [];
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   118
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   119
fun find_casesS ctxt (fact :: _) = InductAttrib.find_casesS ctxt (Thm.concl_of fact)
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   120
  | find_casesS _ _ = [];
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   121
16391
65c8070844ea export cases_tac, induct_tac;
wenzelm
parents: 15794
diff changeset
   122
in
65c8070844ea export cases_tac, induct_tac;
wenzelm
parents: 15794
diff changeset
   123
65c8070844ea export cases_tac, induct_tac;
wenzelm
parents: 15794
diff changeset
   124
fun cases_tac ctxt is_open insts opt_rule facts =
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   125
  let
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   126
    val _ = warn_open is_open;
18147
31634a2af39e induct method: fixes;
wenzelm
parents: 18023
diff changeset
   127
    val thy = ProofContext.theory_of ctxt;
31634a2af39e induct method: fixes;
wenzelm
parents: 18023
diff changeset
   128
    val cert = Thm.cterm_of thy;
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   129
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   130
    fun inst_rule r =
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   131
      if null insts then `RuleCases.get r
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   132
      else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   133
        |> (List.concat o map (prep_inst thy align_left I))
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   134
        |> Drule.cterm_instantiate) r |> pair (RuleCases.get r);
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   135
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   136
    val ruleq =
12852
c6a8e310aec5 cases: really append cases_default;
wenzelm
parents: 12799
diff changeset
   137
      (case opt_rule of
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   138
        SOME r => Seq.single (inst_rule r)
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   139
      | NONE =>
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   140
          (find_casesS ctxt facts @ find_casesT ctxt insts @ [Data.cases_default])
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   141
          |> tap (trace_rules ctxt InductAttrib.casesN)
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   142
          |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   143
  in
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   144
    fn i => fn st =>
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   145
      ruleq
18235
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   146
      |> Seq.maps (RuleCases.consume [] facts)
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   147
      |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   148
        CASES (make_cases is_open rule cases)
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   149
          (Method.insert_tac more_facts i THEN Tactic.rtac rule i) st)
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   150
  end;
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   151
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   152
end;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   153
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   154
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   155
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   156
(** induct method **)
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   157
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   158
(* atomize *)
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   159
18512
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   160
fun atomize_term thy =
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   161
  MetaSimplifier.rewrite_term thy Data.atomize []
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   162
  #> ObjectLogic.drop_judgment thy;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   163
18512
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   164
val atomize_cterm = Tactic.rewrite true Data.atomize;
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   165
18512
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   166
val atomize_tac = Tactic.rewrite_goal_tac Data.atomize;
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   167
18512
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   168
val inner_atomize_tac =
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   169
  Tactic.rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac;
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   170
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   171
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   172
(* rulify *)
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   173
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   174
fun rulify_term thy =
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   175
  MetaSimplifier.rewrite_term thy (Data.rulify @ conjunction_congs) [] #>
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   176
  MetaSimplifier.rewrite_term thy Data.rulify_fallback [];
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   177
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   178
fun rulified_term thm =
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   179
  let
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   180
    val thy = Thm.theory_of_thm thm;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   181
    val rulify = rulify_term thy;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   182
    val (As, B) = Logic.strip_horn (Thm.prop_of thm);
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   183
  in (thy, Logic.list_implies (map rulify As, rulify B)) end;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   184
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   185
val curry_prems_tac =
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   186
  let
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   187
    val rule = conjunction_imp;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   188
    val thy = Thm.theory_of_thm rule;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   189
    val proc = Simplifier.simproc_i thy "curry_prems"
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   190
      [#1 (Logic.dest_equals (Thm.prop_of rule))]
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   191
      (fn _ => fn ss => fn _ =>  (*WORKAROUND: prevent descending into meta conjunctions*)
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   192
        if exists (equal propT o #2 o #1) (#2 (#bounds (#1 (Simplifier.rep_ss ss))))
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   193
        then NONE else SOME rule);
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   194
    val ss = MetaSimplifier.theory_context thy Simplifier.empty_ss addsimprocs [proc];
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   195
  in Simplifier.full_simp_tac ss end;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   196
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   197
val rulify_tac =
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   198
  Tactic.rewrite_goal_tac (Data.rulify @ conjunction_congs) THEN'
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   199
  Tactic.rewrite_goal_tac Data.rulify_fallback THEN'
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   200
  Tactic.conjunction_tac THEN_ALL_NEW
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   201
  (curry_prems_tac THEN' Tactic.norm_hhf_tac);
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   202
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   203
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   204
(* prepare rule *)
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   205
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   206
fun rule_instance thy inst rule =
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   207
  Drule.cterm_instantiate (prep_inst thy align_left I (Thm.prop_of rule, inst)) rule;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   208
18512
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   209
fun internalize k th =
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   210
  th |> Thm.permute_prems 0 k
18512
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   211
  |> Drule.fconv_rule (Drule.concl_conv (Thm.nprems_of th - k) atomize_cterm);
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   212
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   213
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   214
(* guess rule instantiation -- cannot handle pending goal parameters *)
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   215
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   216
local
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   217
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   218
fun dest_env thy (env as Envir.Envir {iTs, ...}) =
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   219
  let
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   220
    val cert = Thm.cterm_of thy;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   221
    val certT = Thm.ctyp_of thy;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   222
    val pairs = Envir.alist_of env;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   223
    val ts = map (cert o Envir.norm_term env o #2 o #2) pairs;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   224
    val xs = map2 (curry (cert o Var)) (map #1 pairs) (map (#T o Thm.rep_cterm) ts);
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   225
  in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) (Vartab.dest iTs), xs ~~ ts) end;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   226
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   227
in
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   228
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   229
fun guess_instance rule i st =
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   230
  let
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   231
    val {thy, maxidx, ...} = Thm.rep_thm st;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   232
    val goal = Thm.term_of (Thm.cprem_of st i);  (*exception Subscript*)
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   233
    val params = rev (rename_wrt_term goal (Logic.strip_params goal));
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   234
  in
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   235
    if not (null params) then
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   236
      (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   237
        commas_quote (map (Sign.string_of_term thy o Syntax.mark_boundT) params));
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   238
      Seq.single rule)
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   239
    else
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   240
      let
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   241
        val rule' = Thm.incr_indexes (maxidx + 1) rule;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   242
        val concl = Logic.strip_assums_concl goal;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   243
      in
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   244
        Unify.smash_unifiers (thy, Envir.empty (#maxidx (Thm.rep_thm rule')),
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   245
          [(Thm.concl_of rule', concl)])
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   246
        |> Seq.map (fn env => Drule.instantiate (dest_env thy env) rule')
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   247
      end
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   248
  end handle Subscript => Seq.empty;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   249
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   250
end;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   251
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   252
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   253
(* special renaming of rule parameters *)
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   254
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   255
fun special_rename_params ctxt [[SOME (Free (z, Type (T, _)))]] [thm] =
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   256
      let
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   257
        val x = ProofContext.revert_skolem ctxt z;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   258
        fun index i [] = []
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   259
          | index i (y :: ys) =
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   260
              if x = y then x ^ string_of_int i :: index (i + 1) ys
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   261
              else y :: index i ys;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   262
        fun rename_params [] = []
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   263
          | rename_params ((y, Type (U, _)) :: ys) =
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   264
              (if U = T then x else y) :: rename_params ys
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   265
          | rename_params ((y, _) :: ys) = y :: rename_params ys;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   266
        fun rename_asm A =
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   267
          let
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   268
            val xs = rename_params (Logic.strip_params A);
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   269
            val xs' =
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   270
              (case List.filter (equal x) xs of
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   271
                [] => xs | [_] => xs | _ => index 1 xs);
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   272
          in Logic.list_rename_params (xs', A) end;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   273
        fun rename_prop p =
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   274
          let val (As, C) = Logic.strip_horn p
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   275
          in Logic.list_implies (map rename_asm As, C) end;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   276
        val cp' = cterm_fun rename_prop (Thm.cprop_of thm);
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   277
        val thm' = Thm.equal_elim (Thm.reflexive cp') thm;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   278
      in [RuleCases.save thm thm'] end
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   279
  | special_rename_params _ _ ths = ths;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   280
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   281
18235
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   282
(* fix_tac *)
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   283
18250
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   284
local
18240
3b72f559e942 more robust revert_skolem;
wenzelm
parents: 18235
diff changeset
   285
18250
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   286
fun goal_prefix k ((c as Const ("all", _)) $ Abs (a, T, B)) = c $ Abs (a, T, goal_prefix k B)
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   287
  | goal_prefix 0 _ = Term.dummy_pattern propT
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   288
  | goal_prefix k ((c as Const ("==>", _)) $ A $ B) = c $ A $ goal_prefix (k - 1) B
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   289
  | goal_prefix _ _ = Term.dummy_pattern propT;
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   290
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   291
fun goal_params k (Const ("all", _) $ Abs (_, _, B)) = goal_params k B + 1
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   292
  | goal_params 0 _ = 0
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   293
  | goal_params k (Const ("==>", _) $ _ $ B) = goal_params (k - 1) B
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   294
  | goal_params _ _ = 0;
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   295
18250
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   296
fun meta_spec_tac ctxt n (x, T) = SUBGOAL (fn (goal, i) =>
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   297
  let
18250
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   298
    val thy = ProofContext.theory_of ctxt;
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   299
    val cert = Thm.cterm_of thy;
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   300
    val certT = Thm.ctyp_of thy;
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   301
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   302
    val v = Free (x, T);
18250
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   303
    fun spec_rule prfx (xs, body) =
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   304
      meta_spec
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   305
      |> Thm.rename_params_rule ([ProofContext.revert_skolem ctxt x], 1)
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   306
      |> Thm.lift_rule (cert prfx)
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   307
      |> `(Thm.prop_of #> Logic.strip_assums_concl)
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   308
      |-> (fn pred $ arg =>
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   309
        Drule.cterm_instantiate
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   310
          [(cert (Term.head_of pred), cert (Unify.rlist_abs (xs, body))),
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   311
           (cert (Term.head_of arg), cert (Unify.rlist_abs (xs, v)))]);
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   312
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   313
    fun goal_concl k xs (Const ("all", _) $ Abs (a, T, B)) = goal_concl k ((a, T) :: xs) B
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   314
      | goal_concl 0 xs B =
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   315
          if not (Term.exists_subterm (fn t => t aconv v) B) then NONE
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   316
          else SOME (xs, Term.absfree (x, T, Term.incr_boundvars 1 B))
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   317
      | goal_concl k xs (Const ("==>", _) $ _ $ B) = goal_concl (k - 1) xs B
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   318
      | goal_concl _ _ _ = NONE;
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   319
  in
18250
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   320
    (case goal_concl n [] goal of
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   321
      SOME concl =>
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   322
        (compose_tac (false, spec_rule (goal_prefix n goal) concl, 1) THEN' rtac asm_rl) i
18631
ca56111fe69c fix_tac: no warning;
wenzelm
parents: 18602
diff changeset
   323
    | NONE => all_tac)
18250
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   324
  end);
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   325
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   326
fun miniscope_tac p i = PRIMITIVE (Drule.fconv_rule
18250
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   327
  (Drule.goals_conv (Library.equal i)
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   328
    (Drule.forall_conv p (Tactic.rewrite true [Thm.symmetric Drule.norm_hhf_eq]))));
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   329
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   330
in
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   331
18250
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   332
fun fix_tac _ _ [] = K all_tac
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   333
  | fix_tac ctxt n xs = SUBGOAL (fn (goal, i) =>
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   334
     (EVERY' (map (meta_spec_tac ctxt n) xs) THEN'
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   335
      (miniscope_tac (goal_params n goal))) i);
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   336
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   337
end;
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   338
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   339
18235
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   340
(* add_defs *)
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   341
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   342
fun add_defs def_insts =
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   343
  let
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   344
    fun add (SOME (SOME x, t)) ctxt =
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   345
          let val ((lhs, def), ctxt') = ProofContext.add_def (x, t) ctxt
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   346
          in ((SOME (Free lhs), [def]), ctxt') end
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   347
      | add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt)
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   348
      | add NONE ctxt = ((NONE, []), ctxt);
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   349
  in fold_map add def_insts #> apfst (split_list #> apsnd List.concat) end;
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   350
11790
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   351
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   352
(* induct_tac *)
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   353
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   354
(*
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   355
  rule selection scheme:
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   356
    `x:A` induct ...     - set induction
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   357
          induct x       - type induction
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   358
    ...   induct ... r   - explicit rule
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   359
*)
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   360
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   361
local
15235
614a804d7116 Induction now preserves the name of the induction variable.
nipkow
parents: 14981
diff changeset
   362
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   363
fun find_inductT ctxt insts =
18147
31634a2af39e induct method: fixes;
wenzelm
parents: 18023
diff changeset
   364
  fold_rev multiply (insts |> List.mapPartial (fn [] => NONE | ts => List.last ts)
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   365
    |> map (InductAttrib.find_inductT ctxt o Term.fastype_of)) [[]]
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   366
  |> filter_out (forall Drule.is_internal);
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   367
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   368
fun find_inductS ctxt (fact :: _) = map single (InductAttrib.find_inductS ctxt (Thm.concl_of fact))
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   369
  | find_inductS _ _ = [];
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   370
16391
65c8070844ea export cases_tac, induct_tac;
wenzelm
parents: 15794
diff changeset
   371
in
11790
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   372
18512
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   373
fun induct_tac ctxt is_open def_insts fixing taking opt_rule facts =
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   374
  let
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   375
    val _ = warn_open is_open;
18147
31634a2af39e induct method: fixes;
wenzelm
parents: 18023
diff changeset
   376
    val thy = ProofContext.theory_of ctxt;
31634a2af39e induct method: fixes;
wenzelm
parents: 18023
diff changeset
   377
    val cert = Thm.cterm_of thy;
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   378
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   379
    val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
18259
7b14579c58f2 induct: insert defs in object-logic form;
wenzelm
parents: 18250
diff changeset
   380
    val atomized_defs = map (map ObjectLogic.atomize_thm) defs;
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   381
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   382
    fun inst_rule (concls, r) =
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   383
      (if null insts then `RuleCases.get r
18512
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   384
       else (align_left "Rule has fewer conclusions than arguments given"
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   385
          (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
18512
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   386
        |> (List.concat o map (prep_inst thy align_right (atomize_term thy)))
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   387
        |> Drule.cterm_instantiate) r |> pair (RuleCases.get r))
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   388
      |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   389
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   390
    val ruleq =
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   391
      (case opt_rule of
18580
4fdd39ea2f40 RuleCases.strict_mutual_rule;
wenzelm
parents: 18512
diff changeset
   392
        SOME rs => Seq.single (inst_rule (RuleCases.strict_mutual_rule rs))
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   393
      | NONE =>
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   394
          (find_inductS ctxt facts @
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   395
            map (special_rename_params defs_ctxt insts) (find_inductT ctxt insts))
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   396
          |> List.mapPartial RuleCases.mutual_rule
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   397
          |> tap (trace_rules ctxt InductAttrib.inductN o map #2)
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   398
          |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   399
18602
8f25a0f7f446 RuleCases.make_common/nested;
wenzelm
parents: 18580
diff changeset
   400
    fun rule_cases rule =
8f25a0f7f446 RuleCases.make_common/nested;
wenzelm
parents: 18580
diff changeset
   401
      RuleCases.make_nested is_open (Thm.prop_of rule) (rulified_term rule);
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   402
  in
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   403
    (fn i => fn st =>
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   404
      ruleq
18235
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   405
      |> Seq.maps (RuleCases.consume (List.concat defs) facts)
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   406
      |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
18496
ef36f9be255e proper treatment of nested conjunctions, i.e. simultaneous goals and mutual rules;
wenzelm
parents: 18465
diff changeset
   407
        (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
ef36f9be255e proper treatment of nested conjunctions, i.e. simultaneous goals and mutual rules;
wenzelm
parents: 18465
diff changeset
   408
          (CONJUNCTS (ALLGOALS
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   409
            (Method.insert_tac (more_facts @ nth_list atomized_defs (j - 1))
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   410
              THEN' fix_tac defs_ctxt
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   411
                (nth concls (j - 1) + more_consumes)
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   412
                (nth_list fixing (j - 1))))
18512
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   413
          THEN' inner_atomize_tac) j))
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   414
        THEN' atomize_tac) i st |> Seq.maps (fn st' =>
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   415
            guess_instance (internalize more_consumes rule) i st'
18235
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   416
            |> Seq.map (rule_instance thy taking)
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   417
            |> Seq.maps (fn rule' =>
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   418
              CASES (rule_cases rule' cases)
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   419
                (Tactic.rtac rule' i THEN
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   420
                  PRIMSEQ (ProofContext.exports defs_ctxt ctxt)) st'))))
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   421
    THEN_ALL_NEW_CASES rulify_tac
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   422
  end;
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   423
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   424
end;
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   425
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   426
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   427
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   428
(** coinduct method **)
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   429
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   430
(*
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   431
  rule selection scheme:
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   432
    goal "x:A" coinduct ...   - set coinduction
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   433
               coinduct x     - type coinduction
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   434
               coinduct ... r - explicit rule
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   435
*)
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   436
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   437
local
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   438
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   439
fun find_coinductT ctxt (SOME t :: _) = InductAttrib.find_coinductT ctxt (Term.fastype_of t)
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   440
  | find_coinductT _ _ = [];
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   441
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   442
fun find_coinductS ctxt goal = InductAttrib.find_coinductS ctxt (Logic.strip_assums_concl goal);
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   443
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   444
in
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   445
18235
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   446
fun coinduct_tac ctxt is_open inst taking opt_rule facts =
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   447
  let
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   448
    val _ = warn_open is_open;
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   449
    val thy = ProofContext.theory_of ctxt;
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   450
    val cert = Thm.cterm_of thy;
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   451
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   452
    fun inst_rule r =
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   453
      if null inst then `RuleCases.get r
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   454
      else Drule.cterm_instantiate (prep_inst thy align_left I (Thm.concl_of r, inst)) r
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   455
        |> pair (RuleCases.get r);
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   456
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   457
    fun ruleq goal =
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   458
      (case opt_rule of
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   459
        SOME r => Seq.single (inst_rule r)
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   460
      | NONE =>
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   461
          (find_coinductS ctxt goal @ find_coinductT ctxt inst)
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   462
          |> tap (trace_rules ctxt InductAttrib.coinductN)
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   463
          |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   464
  in
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   465
    SUBGOAL_CASES (fn (goal, i) => fn st =>
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   466
      ruleq goal
18235
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   467
      |> Seq.maps (RuleCases.consume [] facts)
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   468
      |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
18259
7b14579c58f2 induct: insert defs in object-logic form;
wenzelm
parents: 18250
diff changeset
   469
        guess_instance rule i st
18235
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   470
        |> Seq.map (rule_instance thy taking)
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   471
        |> Seq.maps (fn rule' =>
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   472
          CASES (make_cases is_open rule' cases)
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   473
            (Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st)))
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   474
  end;
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   475
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   476
end;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   477
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   478
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   479
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   480
(** concrete syntax **)
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   481
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   482
val openN = "open";
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   483
val fixingN = "fixing";
18235
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   484
val takingN = "taking";
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   485
val ruleN = "rule";
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   486
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   487
local
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   488
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   489
fun single_rule [rule] = rule
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   490
  | single_rule _ = error "Single rule expected";
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   491
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15574
diff changeset
   492
fun named_rule k arg get =
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   493
  Scan.lift (Args.$$$ k -- Args.colon) |-- Scan.repeat arg :--
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   494
    (fn names => Scan.peek (fn ctxt => Scan.succeed (names |> map (fn name =>
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   495
      (case get ctxt name of SOME x => x
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   496
      | NONE => error ("No rule for " ^ k ^ " " ^ quote name)))))) >> #2;
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   497
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   498
fun rule get_type get_set =
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15574
diff changeset
   499
  named_rule InductAttrib.typeN Args.local_tyname get_type ||
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15574
diff changeset
   500
  named_rule InductAttrib.setN Args.local_const get_set ||
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   501
  Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.local_thmss;
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   502
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   503
val cases_rule = rule InductAttrib.lookup_casesT InductAttrib.lookup_casesS >> single_rule;
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   504
val induct_rule = rule InductAttrib.lookup_inductT InductAttrib.lookup_inductS;
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   505
val coinduct_rule =
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   506
  rule InductAttrib.lookup_coinductT InductAttrib.lookup_coinductS >> single_rule;
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   507
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   508
val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.local_term >> SOME;
18147
31634a2af39e induct method: fixes;
wenzelm
parents: 18023
diff changeset
   509
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   510
val def_inst =
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   511
  ((Scan.lift (Args.name --| (Args.$$$ "\\<equiv>" || Args.$$$ "==")) >> SOME)
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   512
      -- Args.local_term) >> SOME ||
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   513
    inst >> Option.map (pair NONE);
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   514
18147
31634a2af39e induct method: fixes;
wenzelm
parents: 18023
diff changeset
   515
val free = Scan.state -- Args.local_term >> (fn (_, Free v) => v | (ctxt, t) =>
31634a2af39e induct method: fixes;
wenzelm
parents: 18023
diff changeset
   516
  error ("Bad free variable: " ^ ProofContext.string_of_term ctxt t));
31634a2af39e induct method: fixes;
wenzelm
parents: 18023
diff changeset
   517
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   518
fun unless_more_args scan = Scan.unless (Scan.lift
18235
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   519
  ((Args.$$$ fixingN || Args.$$$ takingN || Args.$$$ InductAttrib.typeN ||
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   520
    Args.$$$ InductAttrib.setN || Args.$$$ ruleN) -- Args.colon)) scan;
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   521
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   522
val fixing = Scan.optional (Scan.lift (Args.$$$ fixingN -- Args.colon) |--
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   523
  Args.and_list1 (Scan.repeat (unless_more_args free))) [];
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   524
18235
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   525
val taking = Scan.optional (Scan.lift (Args.$$$ takingN -- Args.colon) |--
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   526
  Scan.repeat1 (unless_more_args inst)) [];
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   527
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   528
in
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   529
18235
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   530
fun cases_meth src =
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   531
  Method.syntax (Args.mode openN --
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   532
    (Args.and_list (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule)) src
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   533
  #> (fn (ctxt, (is_open, (insts, opt_rule))) =>
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   534
    Method.METHOD_CASES (fn facts =>
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   535
      Seq.DETERM (HEADGOAL (cases_tac ctxt is_open insts opt_rule facts))));
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   536
18512
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   537
fun induct_meth src =
18235
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   538
  Method.syntax (Args.mode openN --
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   539
    (Args.and_list (Scan.repeat (unless_more_args def_inst)) --
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   540
    (fixing -- taking -- Scan.option induct_rule))) src
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   541
  #> (fn (ctxt, (is_open, (insts, ((fixing, taking), opt_rule)))) =>
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   542
    Method.RAW_METHOD_CASES (fn facts =>
18512
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   543
      Seq.DETERM (HEADGOAL (induct_tac ctxt is_open insts fixing taking opt_rule facts))));
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   544
18235
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   545
fun coinduct_meth src =
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   546
  Method.syntax (Args.mode openN --
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   547
    (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule)) src
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   548
  #> (fn (ctxt, (is_open, ((insts, taking), opt_rule))) =>
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   549
    Method.RAW_METHOD_CASES (fn facts =>
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   550
      Seq.DETERM (HEADGOAL (coinduct_tac ctxt is_open insts taking opt_rule facts))));
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   551
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   552
end;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   553
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   554
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   555
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   556
(** theory setup **)
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   557
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   558
val setup =
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   559
  [Method.add_methods
18235
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   560
    [(InductAttrib.casesN, cases_meth, "case analysis on types or sets"),
18512
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   561
     (InductAttrib.inductN, induct_meth, "induction on types or sets"),
18235
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   562
     (InductAttrib.coinductN, coinduct_meth, "coinduction on types or sets")]];
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   563
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   564
end;