src/Provers/induct_method.ML
author ballarin
Wed, 19 Jul 2006 19:25:58 +0200
changeset 20168 ed7bced29e1b
parent 19904 9956ecabd9af
child 20288 8ff4a0ea49b2
permissions -rw-r--r--
Reimplemented algebra method; now controlled by attribute.
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
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18678
diff changeset
    35
  val setup: theory -> theory
11670
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_congs = [all_conjunction, imp_conjunction];
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
    46
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
    47
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    48
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    49
(** misc utils **)
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    50
18287
28efcdae34dc moved nth_list to Pure/library.ML;
wenzelm
parents: 18259
diff changeset
    51
(* alignment *)
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    52
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    53
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
    54
  let val m = length xs and n = length ys
18678
dd0c569fa43d sane ERROR handling;
wenzelm
parents: 18631
diff changeset
    55
  in if m < n then error 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
    56
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    57
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
    58
  let val m = length xs and n = length ys
18678
dd0c569fa43d sane ERROR handling;
wenzelm
parents: 18631
diff changeset
    59
  in if m < n then error 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
    60
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    61
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    62
(* prep_inst *)
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    63
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
    64
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
    65
  let
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
    66
    val cert = Thm.cterm_of thy;
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15235
diff changeset
    67
    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
    68
          let
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    69
            val cx = cert x;
18147
31634a2af39e induct method: fixes;
wenzelm
parents: 18023
diff changeset
    70
            val {T = xT, thy, ...} = Thm.rep_cterm cx;
12799
5472afdd3bd3 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents: 12305
diff changeset
    71
            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
    72
          in
18147
31634a2af39e induct method: fixes;
wenzelm
parents: 18023
diff changeset
    73
            if Sign.typ_instance thy (#T (Thm.rep_cterm ct), xT) then SOME (cx, ct)
18678
dd0c569fa43d sane ERROR handling;
wenzelm
parents: 18631
diff changeset
    74
            else error (Pretty.string_of (Pretty.block
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    75
             [Pretty.str "Ill-typed instantiation:", Pretty.fbrk,
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    76
              Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1,
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    77
              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
    78
          end
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15235
diff changeset
    79
      | prep_var (_, NONE) = NONE;
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    80
    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
    81
  in
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    82
    align "Rule has fewer variables than instantiations given" xs ts
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19121
diff changeset
    83
    |> map_filter prep_var
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    84
  end;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    85
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    86
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
    87
(* trace_rules *)
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
    88
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
    89
fun trace_rules _ kind [] = error ("Unable to figure out " ^ kind ^ " rule")
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
    90
  | trace_rules ctxt _ rules = Method.trace ctxt rules;
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
    91
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
    92
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
    93
(* make_cases *)
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
    94
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
    95
fun make_cases is_open rule =
18602
8f25a0f7f446 RuleCases.make_common/nested;
wenzelm
parents: 18580
diff changeset
    96
  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
    97
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
    98
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
    99
  | warn_open false = ();
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   100
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   101
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   102
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   103
(** cases method **)
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   104
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   105
(*
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   106
  rule selection scheme:
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   107
          cases         - default case split
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   108
    `x:A` cases ...     - set cases
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   109
          cases t       - type cases
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   110
    ...   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
   111
*)
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
local
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   114
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   115
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
   116
  | find_casesT _ _ = [];
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   117
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   118
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
   119
  | find_casesS _ _ = [];
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   120
16391
65c8070844ea export cases_tac, induct_tac;
wenzelm
parents: 15794
diff changeset
   121
in
65c8070844ea export cases_tac, induct_tac;
wenzelm
parents: 15794
diff changeset
   122
65c8070844ea export cases_tac, induct_tac;
wenzelm
parents: 15794
diff changeset
   123
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
   124
  let
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   125
    val _ = warn_open is_open;
18147
31634a2af39e induct method: fixes;
wenzelm
parents: 18023
diff changeset
   126
    val thy = ProofContext.theory_of ctxt;
31634a2af39e induct method: fixes;
wenzelm
parents: 18023
diff changeset
   127
    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
   128
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   129
    fun inst_rule r =
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   130
      if null insts then `RuleCases.get r
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   131
      else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19121
diff changeset
   132
        |> maps (prep_inst thy align_left I)
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   133
        |> 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
   134
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   135
    val ruleq =
12852
c6a8e310aec5 cases: really append cases_default;
wenzelm
parents: 12799
diff changeset
   136
      (case opt_rule of
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   137
        SOME r => Seq.single (inst_rule r)
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   138
      | NONE =>
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   139
          (find_casesS ctxt facts @ find_casesT ctxt insts @ [Data.cases_default])
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   140
          |> tap (trace_rules ctxt InductAttrib.casesN)
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   141
          |> 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
   142
  in
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   143
    fn i => fn st =>
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   144
      ruleq
18235
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   145
      |> Seq.maps (RuleCases.consume [] facts)
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   146
      |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   147
        CASES (make_cases is_open rule cases)
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   148
          (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
   149
  end;
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   150
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   151
end;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   152
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
(** induct method **)
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   156
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   157
(* atomize *)
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   158
18512
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   159
fun atomize_term thy =
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   160
  MetaSimplifier.rewrite_term thy Data.atomize []
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   161
  #> ObjectLogic.drop_judgment thy;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   162
18512
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   163
val atomize_cterm = Tactic.rewrite true Data.atomize;
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   164
18512
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   165
val atomize_tac = Tactic.rewrite_goal_tac Data.atomize;
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   166
18512
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   167
val inner_atomize_tac =
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   168
  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
   169
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
(* rulify *)
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   172
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   173
fun rulify_term thy =
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   174
  MetaSimplifier.rewrite_term thy (Data.rulify @ conjunction_congs) [] #>
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   175
  MetaSimplifier.rewrite_term thy Data.rulify_fallback [];
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   176
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   177
fun rulified_term thm =
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   178
  let
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   179
    val thy = Thm.theory_of_thm thm;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   180
    val rulify = rulify_term thy;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   181
    val (As, B) = Logic.strip_horn (Thm.prop_of thm);
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   182
  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
   183
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   184
val rulify_tac =
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   185
  Tactic.rewrite_goal_tac (Data.rulify @ conjunction_congs) THEN'
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   186
  Tactic.rewrite_goal_tac Data.rulify_fallback THEN'
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   187
  Tactic.conjunction_tac THEN_ALL_NEW
19121
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 18988
diff changeset
   188
  (Tactic.rewrite_goal_tac [conjunction_imp] THEN' Tactic.norm_hhf_tac);
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   189
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   190
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   191
(* prepare rule *)
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   192
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   193
fun rule_instance thy inst rule =
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   194
  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
   195
18512
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   196
fun internalize k th =
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   197
  th |> Thm.permute_prems 0 k
18512
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   198
  |> 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
   199
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   200
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   201
(* guess rule instantiation -- cannot handle pending goal parameters *)
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
local
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   204
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   205
fun dest_env thy (env as Envir.Envir {iTs, ...}) =
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   206
  let
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   207
    val cert = Thm.cterm_of thy;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   208
    val certT = Thm.ctyp_of thy;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   209
    val pairs = Envir.alist_of env;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   210
    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
   211
    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
   212
  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
   213
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   214
in
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
fun guess_instance rule i st =
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   217
  let
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   218
    val {thy, maxidx, ...} = Thm.rep_thm st;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   219
    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
   220
    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
   221
  in
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   222
    if not (null params) then
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   223
      (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   224
        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
   225
      Seq.single rule)
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   226
    else
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   227
      let
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   228
        val rule' = Thm.incr_indexes (maxidx + 1) rule;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   229
        val concl = Logic.strip_assums_concl goal;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   230
      in
19861
620d90091788 tuned Seq/Envir/Unify interfaces;
wenzelm
parents: 19482
diff changeset
   231
        Unify.smash_unifiers thy [(Thm.concl_of rule', concl)]
620d90091788 tuned Seq/Envir/Unify interfaces;
wenzelm
parents: 19482
diff changeset
   232
          (Envir.empty (#maxidx (Thm.rep_thm rule')))
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   233
        |> 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
   234
      end
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   235
  end handle Subscript => Seq.empty;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   236
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   237
end;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   238
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   239
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   240
(* special renaming of rule parameters *)
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   241
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   242
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
   243
      let
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   244
        val x = ProofContext.revert_skolem ctxt z;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   245
        fun index i [] = []
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   246
          | index i (y :: ys) =
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   247
              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
   248
              else y :: index i ys;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   249
        fun rename_params [] = []
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   250
          | rename_params ((y, Type (U, _)) :: ys) =
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   251
              (if U = T then x else y) :: rename_params ys
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   252
          | rename_params ((y, _) :: ys) = y :: rename_params ys;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   253
        fun rename_asm A =
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   254
          let
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   255
            val xs = rename_params (Logic.strip_params A);
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   256
            val xs' =
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   257
              (case List.filter (equal x) xs of
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   258
                [] => xs | [_] => xs | _ => index 1 xs);
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   259
          in Logic.list_rename_params (xs', A) end;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   260
        fun rename_prop p =
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   261
          let val (As, C) = Logic.strip_horn p
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   262
          in Logic.list_implies (map rename_asm As, C) end;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   263
        val cp' = cterm_fun rename_prop (Thm.cprop_of thm);
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   264
        val thm' = Thm.equal_elim (Thm.reflexive cp') thm;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   265
      in [RuleCases.save thm thm'] end
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   266
  | special_rename_params _ _ ths = ths;
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   267
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   268
18235
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   269
(* fix_tac *)
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   270
18250
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   271
local
18240
3b72f559e942 more robust revert_skolem;
wenzelm
parents: 18235
diff changeset
   272
18250
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   273
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
   274
  | goal_prefix 0 _ = Term.dummy_pattern propT
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   275
  | 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
   276
  | goal_prefix _ _ = Term.dummy_pattern propT;
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   277
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   278
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
   279
  | goal_params 0 _ = 0
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   280
  | 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
   281
  | goal_params _ _ = 0;
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   282
18250
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   283
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
   284
  let
18250
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   285
    val thy = ProofContext.theory_of ctxt;
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   286
    val cert = Thm.cterm_of thy;
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   287
    val certT = Thm.ctyp_of thy;
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   288
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   289
    val v = Free (x, T);
18250
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   290
    fun spec_rule prfx (xs, body) =
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   291
      meta_spec
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   292
      |> 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
   293
      |> Thm.lift_rule (cert prfx)
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   294
      |> `(Thm.prop_of #> Logic.strip_assums_concl)
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   295
      |-> (fn pred $ arg =>
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   296
        Drule.cterm_instantiate
18933
057b32b8f1fd Logic.rlist_abs;
wenzelm
parents: 18818
diff changeset
   297
          [(cert (Term.head_of pred), cert (Logic.rlist_abs (xs, body))),
057b32b8f1fd Logic.rlist_abs;
wenzelm
parents: 18818
diff changeset
   298
           (cert (Term.head_of arg), cert (Logic.rlist_abs (xs, v)))]);
18250
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   299
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   300
    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
   301
      | goal_concl 0 xs B =
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   302
          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
   303
          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
   304
      | 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
   305
      | goal_concl _ _ _ = NONE;
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   306
  in
18250
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   307
    (case goal_concl n [] goal of
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   308
      SOME concl =>
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   309
        (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
   310
    | NONE => all_tac)
18250
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   311
  end);
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   312
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   313
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
   314
  (Drule.goals_conv (Library.equal i)
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   315
    (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
   316
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   317
in
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   318
18250
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   319
fun fix_tac _ _ [] = K all_tac
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   320
  | fix_tac ctxt n xs = SUBGOAL (fn (goal, i) =>
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   321
     (EVERY' (map (meta_spec_tac ctxt n) xs) THEN'
dfe5d09514eb fix_tac: proper treatment of major premises in goal;
wenzelm
parents: 18240
diff changeset
   322
      (miniscope_tac (goal_params n goal))) i);
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   323
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   324
end;
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   325
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   326
18235
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   327
(* add_defs *)
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   328
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   329
fun add_defs def_insts =
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   330
  let
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   331
    fun add (SOME (SOME x, t)) ctxt =
18818
86eec44dae66 LocalDefs.add_def;
wenzelm
parents: 18799
diff changeset
   332
          let val ((lhs, def), ctxt') = LocalDefs.add_def (x, t) ctxt
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   333
          in ((SOME (Free lhs), [def]), ctxt') end
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   334
      | add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt)
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   335
      | add NONE ctxt = ((NONE, []), ctxt);
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19121
diff changeset
   336
  in fold_map add def_insts #> apfst (split_list #> apsnd flat) end;
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   337
11790
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   338
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   339
(* induct_tac *)
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   340
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
  rule selection scheme:
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   343
    `x:A` induct ...     - set induction
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   344
          induct x       - type induction
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   345
    ...   induct ... r   - explicit rule
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   346
*)
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   347
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   348
local
15235
614a804d7116 Induction now preserves the name of the induction variable.
nipkow
parents: 14981
diff changeset
   349
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   350
fun find_inductT ctxt insts =
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19121
diff changeset
   351
  fold_rev multiply (insts |> map_filter (fn [] => NONE | ts => List.last ts)
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   352
    |> map (InductAttrib.find_inductT ctxt o Term.fastype_of)) [[]]
18799
f137c5e971f5 moved theorem tags from Drule to PureThy;
wenzelm
parents: 18708
diff changeset
   353
  |> filter_out (forall PureThy.is_internal);
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   354
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   355
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
   356
  | find_inductS _ _ = [];
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   357
16391
65c8070844ea export cases_tac, induct_tac;
wenzelm
parents: 15794
diff changeset
   358
in
11790
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   359
18512
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   360
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
   361
  let
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   362
    val _ = warn_open is_open;
18147
31634a2af39e induct method: fixes;
wenzelm
parents: 18023
diff changeset
   363
    val thy = ProofContext.theory_of ctxt;
31634a2af39e induct method: fixes;
wenzelm
parents: 18023
diff changeset
   364
    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
   365
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   366
    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
   367
    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
   368
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   369
    fun inst_rule (concls, r) =
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   370
      (if null insts then `RuleCases.get r
18512
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   371
       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
   372
          (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19121
diff changeset
   373
        |> maps (prep_inst thy align_right (atomize_term thy))
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   374
        |> Drule.cterm_instantiate) r |> pair (RuleCases.get r))
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   375
      |> (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
   376
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   377
    val ruleq =
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   378
      (case opt_rule of
19904
9956ecabd9af RuleCases.mutual_rule: ctxt;
wenzelm
parents: 19861
diff changeset
   379
        SOME rs => Seq.single (inst_rule (RuleCases.strict_mutual_rule ctxt rs))
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   380
      | NONE =>
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   381
          (find_inductS ctxt facts @
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   382
            map (special_rename_params defs_ctxt insts) (find_inductT ctxt insts))
19904
9956ecabd9af RuleCases.mutual_rule: ctxt;
wenzelm
parents: 19861
diff changeset
   383
          |> map_filter (RuleCases.mutual_rule ctxt)
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   384
          |> tap (trace_rules ctxt InductAttrib.inductN o map #2)
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   385
          |> 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
   386
18602
8f25a0f7f446 RuleCases.make_common/nested;
wenzelm
parents: 18580
diff changeset
   387
    fun rule_cases rule =
8f25a0f7f446 RuleCases.make_common/nested;
wenzelm
parents: 18580
diff changeset
   388
      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
   389
  in
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   390
    (fn i => fn st =>
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   391
      ruleq
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19121
diff changeset
   392
      |> Seq.maps (RuleCases.consume (flat defs) facts)
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   393
      |> 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
   394
        (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
   395
          (CONJUNCTS (ALLGOALS
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   396
            (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
   397
              THEN' fix_tac defs_ctxt
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   398
                (nth concls (j - 1) + more_consumes)
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   399
                (nth_list fixing (j - 1))))
18512
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   400
          THEN' inner_atomize_tac) j))
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   401
        THEN' atomize_tac) i st |> Seq.maps (fn st' =>
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   402
            guess_instance (internalize more_consumes rule) i st'
18235
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   403
            |> Seq.map (rule_instance thy taking)
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   404
            |> Seq.maps (fn rule' =>
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   405
              CASES (rule_cases rule' cases)
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   406
                (Tactic.rtac rule' i THEN
19904
9956ecabd9af RuleCases.mutual_rule: ctxt;
wenzelm
parents: 19861
diff changeset
   407
                  PRIMSEQ (Seq.singleton (ProofContext.exports defs_ctxt ctxt))) st'))))
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   408
    THEN_ALL_NEW_CASES rulify_tac
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   409
  end;
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   410
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   411
end;
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   412
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   413
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   414
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   415
(** coinduct method **)
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   416
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   417
(*
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   418
  rule selection scheme:
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   419
    goal "x:A" coinduct ...   - set coinduction
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   420
               coinduct x     - type coinduction
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   421
               coinduct ... r - explicit rule
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   422
*)
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   423
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   424
local
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   425
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   426
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
   427
  | find_coinductT _ _ = [];
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   428
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   429
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
   430
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   431
in
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   432
18235
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   433
fun coinduct_tac ctxt is_open inst taking opt_rule facts =
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   434
  let
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   435
    val _ = warn_open is_open;
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   436
    val thy = ProofContext.theory_of ctxt;
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   437
    val cert = Thm.cterm_of thy;
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   438
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   439
    fun inst_rule r =
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   440
      if null inst then `RuleCases.get r
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   441
      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
   442
        |> pair (RuleCases.get r);
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   443
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   444
    fun ruleq goal =
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   445
      (case opt_rule of
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   446
        SOME r => Seq.single (inst_rule r)
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   447
      | NONE =>
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   448
          (find_coinductS ctxt goal @ find_coinductT ctxt inst)
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   449
          |> tap (trace_rules ctxt InductAttrib.coinductN)
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   450
          |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   451
  in
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   452
    SUBGOAL_CASES (fn (goal, i) => fn st =>
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   453
      ruleq goal
18235
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   454
      |> Seq.maps (RuleCases.consume [] facts)
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   455
      |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
18259
7b14579c58f2 induct: insert defs in object-logic form;
wenzelm
parents: 18250
diff changeset
   456
        guess_instance rule i st
18235
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   457
        |> Seq.map (rule_instance thy taking)
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   458
        |> Seq.maps (fn rule' =>
18224
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   459
          CASES (make_cases is_open rule' cases)
1b191bb611f4 make coinduct actually work;
wenzelm
parents: 18205
diff changeset
   460
            (Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st)))
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   461
  end;
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   462
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   463
end;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   464
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   465
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   466
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   467
(** concrete syntax **)
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   468
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   469
val openN = "open";
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   470
val fixingN = "fixing";
18235
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   471
val takingN = "taking";
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   472
val ruleN = "rule";
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   473
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   474
local
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   475
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   476
fun single_rule [rule] = rule
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   477
  | single_rule _ = error "Single rule expected";
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   478
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15574
diff changeset
   479
fun named_rule k arg get =
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   480
  Scan.lift (Args.$$$ k -- Args.colon) |-- Scan.repeat arg :--
18988
d6e5fa2ba8b8 Args/Attrib syntax: Context.generic;
wenzelm
parents: 18933
diff changeset
   481
    (fn names => Scan.peek (fn context => Scan.succeed (names |> map (fn name =>
d6e5fa2ba8b8 Args/Attrib syntax: Context.generic;
wenzelm
parents: 18933
diff changeset
   482
      (case get (Context.proof_of context) name of SOME x => x
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   483
      | 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
   484
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   485
fun rule get_type get_set =
18988
d6e5fa2ba8b8 Args/Attrib syntax: Context.generic;
wenzelm
parents: 18933
diff changeset
   486
  named_rule InductAttrib.typeN Args.tyname get_type ||
d6e5fa2ba8b8 Args/Attrib syntax: Context.generic;
wenzelm
parents: 18933
diff changeset
   487
  named_rule InductAttrib.setN Args.const get_set ||
d6e5fa2ba8b8 Args/Attrib syntax: Context.generic;
wenzelm
parents: 18933
diff changeset
   488
  Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   489
18465
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   490
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
   491
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
   492
val coinduct_rule =
16dcd36499b8 simplified setup: removed dest_concls, local_impI, conjI;
wenzelm
parents: 18330
diff changeset
   493
  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
   494
18988
d6e5fa2ba8b8 Args/Attrib syntax: Context.generic;
wenzelm
parents: 18933
diff changeset
   495
val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME;
18147
31634a2af39e induct method: fixes;
wenzelm
parents: 18023
diff changeset
   496
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   497
val def_inst =
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   498
  ((Scan.lift (Args.name --| (Args.$$$ "\\<equiv>" || Args.$$$ "==")) >> SOME)
18988
d6e5fa2ba8b8 Args/Attrib syntax: Context.generic;
wenzelm
parents: 18933
diff changeset
   499
      -- Args.term) >> SOME ||
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   500
    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
   501
18988
d6e5fa2ba8b8 Args/Attrib syntax: Context.generic;
wenzelm
parents: 18933
diff changeset
   502
val free = Scan.state -- Args.term >> (fn (_, Free v) => v | (context, t) =>
d6e5fa2ba8b8 Args/Attrib syntax: Context.generic;
wenzelm
parents: 18933
diff changeset
   503
  error ("Bad free variable: " ^ ProofContext.string_of_term (Context.proof_of context) t));
18147
31634a2af39e induct method: fixes;
wenzelm
parents: 18023
diff changeset
   504
18178
9e4dfe031525 induct: support local definitions to be passed through the induction;
wenzelm
parents: 18147
diff changeset
   505
fun unless_more_args scan = Scan.unless (Scan.lift
18235
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   506
  ((Args.$$$ fixingN || Args.$$$ takingN || Args.$$$ InductAttrib.typeN ||
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   507
    Args.$$$ InductAttrib.setN || Args.$$$ ruleN) -- Args.colon)) scan;
18205
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   508
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   509
val fixing = Scan.optional (Scan.lift (Args.$$$ fixingN -- Args.colon) |--
744803a2d5a5 induct: CONJUNCTS for multiple goals;
wenzelm
parents: 18178
diff changeset
   510
  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
   511
18235
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   512
val taking = Scan.optional (Scan.lift (Args.$$$ takingN -- Args.colon) |--
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   513
  Scan.repeat1 (unless_more_args inst)) [];
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   514
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   515
in
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   516
18235
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   517
fun cases_meth src =
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   518
  Method.syntax (Args.mode openN --
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   519
    (Args.and_list (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule)) src
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   520
  #> (fn (ctxt, (is_open, (insts, opt_rule))) =>
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   521
    Method.METHOD_CASES (fn facts =>
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   522
      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
   523
18512
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   524
fun induct_meth src =
18235
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   525
  Method.syntax (Args.mode openN --
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   526
    (Args.and_list (Scan.repeat (unless_more_args def_inst)) --
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   527
    (fixing -- taking -- Scan.option induct_rule))) src
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   528
  #> (fn (ctxt, (is_open, (insts, ((fixing, taking), opt_rule)))) =>
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   529
    Method.RAW_METHOD_CASES (fn facts =>
18512
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   530
      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
   531
18235
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   532
fun coinduct_meth src =
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   533
  Method.syntax (Args.mode openN --
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   534
    (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule)) src
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   535
  #> (fn (ctxt, (is_open, ((insts, taking), opt_rule))) =>
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   536
    Method.RAW_METHOD_CASES (fn facts =>
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   537
      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
   538
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   539
end;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   540
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   541
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   542
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   543
(** theory setup **)
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   544
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   545
val setup =
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18678
diff changeset
   546
  Method.add_methods
18235
63da52e2d6dc (co)induct: taking;
wenzelm
parents: 18224
diff changeset
   547
    [(InductAttrib.casesN, cases_meth, "case analysis on types or sets"),
18512
f8df49d4af35 removed obsolete atomize_old;
wenzelm
parents: 18496
diff changeset
   548
     (InductAttrib.inductN, induct_meth, "induction on types or sets"),
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18678
diff changeset
   549
     (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
   550
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   551
end;