src/HOL/Tools/induct_method.ML
author wenzelm
Sat, 01 Jul 2000 19:55:22 +0200
changeset 9230 17ae63f82ad8
parent 9066 b1e874e38dab
child 9299 c5cda71de65d
permissions -rw-r--r--
GPLed;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6442
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/Tools/induct_method.ML
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
9230
wenzelm
parents: 9066
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
6442
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
     5
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
     6
Proof by cases and induction on types and sets.
6442
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
     7
*)
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
     8
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
     9
signature INDUCT_METHOD =
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
    10
sig
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
    11
  val dest_global_rules: theory ->
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
    12
    {type_cases: (string * thm) list, set_cases: (string * thm) list,
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
    13
      type_induct: (string * thm) list, set_induct: (string * thm) list}
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    14
  val print_global_rules: theory -> unit
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
    15
  val dest_local_rules: Proof.context ->
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
    16
    {type_cases: (string * thm) list, set_cases: (string * thm) list,
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
    17
      type_induct: (string * thm) list, set_induct: (string * thm) list}
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    18
  val print_local_rules: Proof.context -> unit
8431
e5f8ee756a8a export vars_of;
wenzelm
parents: 8400
diff changeset
    19
  val vars_of: term -> term list
8695
850e84526745 export concl_of;
wenzelm
parents: 8688
diff changeset
    20
  val concls_of: thm -> term list
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    21
  val cases_type_global: string -> theory attribute
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    22
  val cases_set_global: string -> theory attribute
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    23
  val cases_type_local: string -> Proof.context attribute
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    24
  val cases_set_local: string -> Proof.context attribute
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    25
  val induct_type_global: string -> theory attribute
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    26
  val induct_set_global: string -> theory attribute
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    27
  val induct_type_local: string -> Proof.context attribute
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    28
  val induct_set_local: string -> Proof.context attribute
8337
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
    29
  val con_elim_tac: simpset -> tactic
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
    30
  val con_elim_solved_tac: simpset -> tactic
6442
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
    31
  val setup: (theory -> theory) list
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
    32
end;
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
    33
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
    34
structure InductMethod: INDUCT_METHOD =
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
    35
struct
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
    36
8337
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
    37
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    38
(** global and local induct data **)
6442
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
    39
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    40
(* rules *)
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    41
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    42
type rules = (string * thm) NetRules.T;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    43
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    44
fun eq_rule ((s1:string, th1), (s2, th2)) = s1 = s2 andalso Thm.eq_thm (th1, th2);
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    45
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    46
val type_rules = NetRules.init eq_rule (Thm.concl_of o #2);
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    47
val set_rules = NetRules.init eq_rule (Thm.major_prem_of o #2);
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    48
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    49
fun lookup_rule (rs:rules) name = Library.assoc (NetRules.rules rs, name);
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    50
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    51
fun print_rules kind rs =
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    52
  let val thms = map snd (NetRules.rules rs)
8315
c9b4f1c47816 tuned msgs;
wenzelm
parents: 8308
diff changeset
    53
  in Pretty.writeln (Pretty.big_list kind (map Display.pretty_thm thms)) end;
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    54
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    55
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    56
(* theory data kind 'HOL/induct_method' *)
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    57
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    58
structure GlobalInductArgs =
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    59
struct
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    60
  val name = "HOL/induct_method";
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    61
  type T = (rules * rules) * (rules * rules);
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    62
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    63
  val empty = ((type_rules, set_rules), (type_rules, set_rules));
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    64
  val copy = I;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    65
  val prep_ext = I;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    66
  fun merge (((casesT1, casesS1), (inductT1, inductS1)),
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    67
      ((casesT2, casesS2), (inductT2, inductS2))) =
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    68
    ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)),
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    69
      (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)));
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    70
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    71
  fun print _ ((casesT, casesS), (inductT, inductS)) =
8315
c9b4f1c47816 tuned msgs;
wenzelm
parents: 8308
diff changeset
    72
    (print_rules "type cases:" casesT;
c9b4f1c47816 tuned msgs;
wenzelm
parents: 8308
diff changeset
    73
      print_rules "set cases:" casesS;
c9b4f1c47816 tuned msgs;
wenzelm
parents: 8308
diff changeset
    74
      print_rules "type induct:" inductT;
c9b4f1c47816 tuned msgs;
wenzelm
parents: 8308
diff changeset
    75
      print_rules "set induct:" inductS);
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
    76
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
    77
  fun dest ((casesT, casesS), (inductT, inductS)) =
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
    78
    {type_cases = NetRules.rules casesT,
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
    79
     set_cases = NetRules.rules casesS,
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
    80
     type_induct = NetRules.rules inductT,
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
    81
     set_induct = NetRules.rules inductS};
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    82
end;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    83
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    84
structure GlobalInduct = TheoryDataFun(GlobalInductArgs);
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    85
val print_global_rules = GlobalInduct.print;
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
    86
val dest_global_rules = GlobalInductArgs.dest o GlobalInduct.get;
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    87
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    88
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    89
(* proof data kind 'HOL/induct_method' *)
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    90
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    91
structure LocalInductArgs =
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    92
struct
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    93
  val name = "HOL/induct_method";
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    94
  type T = GlobalInductArgs.T;
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
    95
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    96
  fun init thy = GlobalInduct.get thy;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    97
  fun print x = GlobalInductArgs.print x;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    98
end;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    99
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   100
structure LocalInduct = ProofDataFun(LocalInductArgs);
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   101
val print_local_rules = LocalInduct.print;
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   102
val dest_local_rules = GlobalInductArgs.dest o LocalInduct.get;
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   103
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   104
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   105
(* access rules *)
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   106
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   107
val get_cases = #1 o LocalInduct.get;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   108
val get_induct = #2 o LocalInduct.get;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   109
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   110
val lookup_casesT = lookup_rule o #1 o get_cases;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   111
val lookup_casesS = lookup_rule o #2 o get_cases;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   112
val lookup_inductT = lookup_rule o #1 o get_induct;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   113
val lookup_inductS = lookup_rule o #2 o get_induct;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   114
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   115
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   116
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   117
(** attributes **)
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   118
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   119
local
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   120
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   121
fun mk_att f g name (x, thm) = (f (g (name, thm)) x, thm);
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   122
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   123
fun add_casesT rule x = apfst (apfst (NetRules.insert rule)) x;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   124
fun add_casesS rule x = apfst (apsnd (NetRules.insert rule)) x;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   125
fun add_inductT rule x = apsnd (apfst (NetRules.insert rule)) x;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   126
fun add_inductS rule x = apsnd (apsnd (NetRules.insert rule)) x;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   127
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   128
in
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   129
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   130
val cases_type_global = mk_att GlobalInduct.map add_casesT;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   131
val cases_set_global = mk_att GlobalInduct.map add_casesS;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   132
val induct_type_global = mk_att GlobalInduct.map add_inductT;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   133
val induct_set_global = mk_att GlobalInduct.map add_inductS;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   134
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   135
val cases_type_local = mk_att LocalInduct.map add_casesT;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   136
val cases_set_local = mk_att LocalInduct.map add_casesS;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   137
val induct_type_local = mk_att LocalInduct.map add_inductT;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   138
val induct_set_local = mk_att LocalInduct.map add_inductS;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   139
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   140
end;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   141
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   142
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   143
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   144
(** misc utils **)
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   145
8695
850e84526745 export concl_of;
wenzelm
parents: 8688
diff changeset
   146
(* thms and terms *)
850e84526745 export concl_of;
wenzelm
parents: 8688
diff changeset
   147
850e84526745 export concl_of;
wenzelm
parents: 8688
diff changeset
   148
val concls_of = HOLogic.dest_conj o HOLogic.dest_Trueprop o Thm.concl_of;
8344
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   149
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   150
fun vars_of tm =        (*ordered left-to-right, preferring right!*)
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   151
  Term.foldl_aterms (fn (ts, t as Var _) => t :: ts | (ts, _) => ts) ([], tm)
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   152
  |> Library.distinct |> rev;
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   153
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   154
fun type_name t =
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   155
  #1 (Term.dest_Type (Term.type_of t))
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   156
    handle TYPE _ => raise TERM ("Bad type of term argument", [t]);
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   157
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   158
8337
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
   159
(* simplifying cases rules *)
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
   160
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
   161
local
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
   162
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
   163
(*delete needless equality assumptions*)
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
   164
val refl_thin = prove_goal HOL.thy "!!P. [| a=a;  P |] ==> P"
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
   165
     (fn _ => [assume_tac 1]);
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
   166
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
   167
val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject];
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
   168
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
   169
val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
   170
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
   171
fun simp_case_tac ss = 
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
   172
  EVERY' [elim_tac, asm_full_simp_tac ss, elim_tac, REPEAT o bound_hyp_subst_tac];
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
   173
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
   174
in
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
   175
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
   176
fun con_elim_tac ss = ALLGOALS (simp_case_tac ss) THEN prune_params_tac;
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
   177
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
   178
fun con_elim_solved_tac ss =
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
   179
  ALLGOALS (fn i => TRY (simp_case_tac ss i THEN_MAYBE no_tac)) THEN prune_params_tac;
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
   180
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
   181
end;
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
   182
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
   183
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   184
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   185
(** cases method **)
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   186
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   187
(*
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   188
  rule selection:
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   189
        cases         - classical case split
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   190
        cases t       - datatype exhaustion
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   191
  <x:A> cases ...     - set elimination
8451
614f18139d47 tuned comments;
wenzelm
parents: 8431
diff changeset
   192
  ...   cases ... R   - explicit rule
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   193
*)
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   194
9066
b1e874e38dab theorems [cases type: bool] = case_split;
wenzelm
parents: 8815
diff changeset
   195
val case_split = RuleCases.name ["True", "False"] case_split_thm;
b1e874e38dab theorems [cases type: bool] = case_split;
wenzelm
parents: 8815
diff changeset
   196
8344
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   197
local
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   198
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   199
fun cases_var thm =
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   200
  (case try (hd o vars_of o hd o Logic.strip_assums_hyp o Library.last_elem o Thm.prems_of) thm of
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   201
    None => raise THM ("Malformed cases rule", 0, [thm])
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   202
  | Some x => x);
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   203
8337
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
   204
fun simplify_cases ctxt =
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
   205
  Tactic.rule_by_tactic (con_elim_solved_tac (Simplifier.get_local_simpset ctxt));
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
   206
8344
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   207
fun cases_tac (ctxt, (simplified, args)) facts =
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   208
  let
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   209
    val sg = ProofContext.sign_of ctxt;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   210
    val cert = Thm.cterm_of sg;
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   211
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   212
    fun inst_rule t thm =
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   213
      Drule.cterm_instantiate [(cert (cases_var thm), cert t)] thm;
6442
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
   214
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   215
    val cond_simp = if simplified then simplify_cases ctxt else I;
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   216
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   217
    fun find_cases th =
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   218
      NetRules.may_unify (#2 (get_cases ctxt))
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   219
        (Logic.strip_assums_concl (#prop (Thm.rep_thm th)));
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   220
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   221
    val rules =
8344
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   222
      (case (args, facts) of
9066
b1e874e38dab theorems [cases type: bool] = case_split;
wenzelm
parents: 8815
diff changeset
   223
        ((None, None), []) => [RuleCases.add case_split]
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   224
      | ((Some t, None), []) =>
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   225
          let val name = type_name t in
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   226
            (case lookup_casesT ctxt name of
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   227
              None => error ("No cases rule for type: " ^ quote name)
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   228
            | Some thm => [(inst_rule t thm, RuleCases.get thm)])
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   229
          end
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   230
      | ((None, None), th :: _) => map (RuleCases.add o #2) (find_cases th)
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   231
      | ((Some t, None), th :: _) =>
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   232
          (case find_cases th of	(*may instantiate first rule only!*)
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   233
            (_, thm) :: _ => [(inst_rule t thm, RuleCases.get thm)]
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   234
          | [] => [])
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   235
      | ((None, Some thm), _) => [RuleCases.add thm]
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   236
      | ((Some t, Some thm), _) => [(inst_rule t thm, RuleCases.get thm)]);
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   237
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   238
    fun prep_rule (thm, cases) =
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   239
      Seq.map (rpair cases o cond_simp) (Method.multi_resolves facts [thm]);
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   240
  in Method.resolveq_cases_tac (Seq.flat (Seq.map prep_rule (Seq.of_list rules))) end;
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   241
8344
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   242
in
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   243
8671
6ce91a80f616 HEADGOAL;
wenzelm
parents: 8540
diff changeset
   244
val cases_meth = Method.METHOD_CASES o (HEADGOAL oo cases_tac);
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   245
8344
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   246
end;
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   247
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   248
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   249
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   250
(** induct method **)
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   251
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   252
(*
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   253
  rule selection:
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   254
        induct         - mathematical induction
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   255
        induct x       - datatype induction
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   256
  <x:A> induct ...     - set induction
8451
614f18139d47 tuned comments;
wenzelm
parents: 8431
diff changeset
   257
  ...   induct ... R   - explicit rule
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   258
*)
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   259
8344
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   260
local
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   261
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   262
infix 1 THEN_ALL_NEW_CASES;
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   263
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   264
fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   265
  st |> Seq.THEN (tac1 i, (fn (st', cases) =>
8540
3a45bc1ff175 tuned degenerate cases / induct;
wenzelm
parents: 8451
diff changeset
   266
    Seq.map (rpair cases) (Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st) st')));
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   267
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   268
8330
c411706dc503 join induct rules;
wenzelm
parents: 8315
diff changeset
   269
fun induct_rule ctxt t =
c411706dc503 join induct rules;
wenzelm
parents: 8315
diff changeset
   270
  let val name = type_name t in
c411706dc503 join induct rules;
wenzelm
parents: 8315
diff changeset
   271
    (case lookup_inductT ctxt name of
c411706dc503 join induct rules;
wenzelm
parents: 8315
diff changeset
   272
      None => error ("No induct rule for type: " ^ quote name)
8332
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   273
    | Some thm => (name, thm))
8330
c411706dc503 join induct rules;
wenzelm
parents: 8315
diff changeset
   274
  end;
c411706dc503 join induct rules;
wenzelm
parents: 8315
diff changeset
   275
8332
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   276
fun join_rules [(_, thm)] = thm
8330
c411706dc503 join induct rules;
wenzelm
parents: 8315
diff changeset
   277
  | join_rules raw_thms =
c411706dc503 join induct rules;
wenzelm
parents: 8315
diff changeset
   278
      let
8332
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   279
        val thms = (map (apsnd Drule.freeze_all) raw_thms);
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   280
        fun eq_prems ((_, th1), (_, th2)) =
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   281
          Term.aconvs (Thm.prems_of th1, Thm.prems_of th2);
8330
c411706dc503 join induct rules;
wenzelm
parents: 8315
diff changeset
   282
      in
8332
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   283
        (case Library.gen_distinct eq_prems thms of
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   284
          [(_, thm)] =>
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   285
            let
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   286
              val cprems = Drule.cprems_of thm;
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   287
              val asms = map Thm.assume cprems;
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   288
              fun strip (_, th) = Drule.implies_elim_list th asms;
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   289
            in
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   290
              foldr1 (fn (th, th') => [th, th'] MRS conjI) (map strip thms)
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   291
              |> Drule.implies_intr_list cprems
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   292
              |> Drule.standard
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   293
            end
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   294
        | [] => error "No rule given"
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   295
        | bads => error ("Incompatible rules for " ^ commas_quote (map #1 bads)))
8330
c411706dc503 join induct rules;
wenzelm
parents: 8315
diff changeset
   296
      end;
c411706dc503 join induct rules;
wenzelm
parents: 8315
diff changeset
   297
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   298
8344
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   299
fun induct_tac (ctxt, (stripped, args)) facts =
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   300
  let
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   301
    val sg = ProofContext.sign_of ctxt;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   302
    val cert = Thm.cterm_of sg;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   303
8695
850e84526745 export concl_of;
wenzelm
parents: 8688
diff changeset
   304
    fun prep_var (x, Some t) = Some (cert x, cert t)
850e84526745 export concl_of;
wenzelm
parents: 8688
diff changeset
   305
      | prep_var (_, None) = None;
850e84526745 export concl_of;
wenzelm
parents: 8688
diff changeset
   306
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   307
    fun prep_inst (concl, ts) =
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   308
      let val xs = vars_of concl; val n = length xs - length ts in
8695
850e84526745 export concl_of;
wenzelm
parents: 8688
diff changeset
   309
        if n < 0 then error "More variables than given than in induction rule"
850e84526745 export concl_of;
wenzelm
parents: 8688
diff changeset
   310
        else mapfilter prep_var (Library.drop (n, xs) ~~ ts)
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   311
      end;
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   312
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   313
    fun inst_rule insts thm =
8695
850e84526745 export concl_of;
wenzelm
parents: 8688
diff changeset
   314
      let val concls = concls_of thm in
850e84526745 export concl_of;
wenzelm
parents: 8688
diff changeset
   315
        if length concls < length insts then
850e84526745 export concl_of;
wenzelm
parents: 8688
diff changeset
   316
          error "More arguments than given than in induction rule"
850e84526745 export concl_of;
wenzelm
parents: 8688
diff changeset
   317
        else Drule.cterm_instantiate (flat (map prep_inst (concls ~~ insts))) thm
850e84526745 export concl_of;
wenzelm
parents: 8688
diff changeset
   318
      end;
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   319
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   320
    fun find_induct th =
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   321
      NetRules.may_unify (#2 (get_induct ctxt))
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   322
        (Logic.strip_assums_concl (#prop (Thm.rep_thm th)));
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   323
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   324
    val rules =
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   325
      (case (args, facts) of
8540
3a45bc1ff175 tuned degenerate cases / induct;
wenzelm
parents: 8451
diff changeset
   326
        (([], None), []) => []
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   327
      | ((insts, None), []) =>
8695
850e84526745 export concl_of;
wenzelm
parents: 8688
diff changeset
   328
          let val thms = map (induct_rule ctxt o last_elem o mapfilter I) insts
850e84526745 export concl_of;
wenzelm
parents: 8688
diff changeset
   329
            handle Library.LIST _ => error "Unable to figure out type induction rule"
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   330
          in [(inst_rule insts (join_rules thms), RuleCases.get (#2 (hd thms)))] end
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   331
      | (([], None), th :: _) => map (RuleCases.add o #2) (find_induct th)
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   332
      | ((insts, None), th :: _) =>
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   333
          (case find_induct th of	(*may instantiate first rule only!*)
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   334
	    (_, thm) :: _ => [(inst_rule insts thm, RuleCases.get thm)]
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   335
          | [] => [])
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   336
      | (([], Some thm), _) => [RuleCases.add thm]
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   337
      | ((insts, Some thm), _) => [(inst_rule insts thm, RuleCases.get thm)]);
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   338
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   339
    fun prep_rule (thm, cases) =
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   340
      Seq.map (rpair cases) (Method.multi_resolves facts [thm]);
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   341
    val tac = Method.resolveq_cases_tac (Seq.flat (Seq.map prep_rule (Seq.of_list rules)));
8344
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   342
  in
8688
63b267d41b96 induct stripped: match_tac;
wenzelm
parents: 8671
diff changeset
   343
    if stripped then tac THEN_ALL_NEW_CASES (REPEAT o Tactic.match_tac [impI, allI, ballI])
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   344
    else tac
8344
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   345
  end;
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   346
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   347
in
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   348
8671
6ce91a80f616 HEADGOAL;
wenzelm
parents: 8540
diff changeset
   349
val induct_meth = Method.METHOD_CASES o (HEADGOAL oo induct_tac);
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   350
8344
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   351
end;
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   352
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   353
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   354
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   355
(** concrete syntax **)
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   356
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   357
val casesN = "cases";
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   358
val inductN = "induct";
8344
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   359
8337
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
   360
val simplifiedN = "simplified";
8344
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   361
val strippedN = "stripped";
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   362
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   363
val typeN = "type";
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   364
val setN = "set";
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   365
val ruleN = "rule";
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   366
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   367
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   368
(* attributes *)
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   369
8815
187547eae4c5 use Args.colon / Args.parens;
wenzelm
parents: 8695
diff changeset
   370
fun spec k = (Args.$$$ k -- Args.colon) |-- Args.!!! Args.name;
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   371
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   372
fun attrib sign_of add_type add_set = Scan.depend (fn x =>
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   373
  let val sg = sign_of x in
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   374
    spec typeN >> (add_type o Sign.intern_tycon sg) ||
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   375
    spec setN  >> (add_set o Sign.intern_const sg)
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   376
  end >> pair x);
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   377
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   378
val cases_attr =
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   379
  (Attrib.syntax (attrib Theory.sign_of cases_type_global cases_set_global),
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   380
   Attrib.syntax (attrib ProofContext.sign_of cases_type_local cases_set_local));
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   381
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   382
val induct_attr =
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   383
  (Attrib.syntax (attrib Theory.sign_of induct_type_global induct_set_global),
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   384
   Attrib.syntax (attrib ProofContext.sign_of induct_type_local induct_set_local));
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   385
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   386
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   387
(* methods *)
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   388
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   389
local
6442
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
   390
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   391
fun err k get name =
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   392
  (case get name of Some x => x
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   393
  | None => error ("No rule for " ^ k ^ " " ^ quote name));
6442
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
   394
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   395
fun rule get_type get_set =
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   396
  Scan.depend (fn ctxt =>
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   397
    let val sg = ProofContext.sign_of ctxt in
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   398
      spec typeN >> (err typeN (get_type ctxt) o Sign.intern_tycon sg) ||
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   399
      spec setN >> (err setN (get_set ctxt) o Sign.intern_const sg)
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   400
    end >> pair ctxt) ||
8815
187547eae4c5 use Args.colon / Args.parens;
wenzelm
parents: 8695
diff changeset
   401
  Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.local_thm;
6442
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
   402
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   403
val cases_rule = rule lookup_casesT lookup_casesS;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   404
val induct_rule = rule lookup_inductT lookup_inductS;
6442
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
   405
8815
187547eae4c5 use Args.colon / Args.parens;
wenzelm
parents: 8695
diff changeset
   406
val kind = (Args.$$$ typeN || Args.$$$ setN || Args.$$$ ruleN) -- Args.colon;
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   407
val term = Scan.unless (Scan.lift kind) Args.local_term;
8695
850e84526745 export concl_of;
wenzelm
parents: 8688
diff changeset
   408
val term_dummy = Scan.unless (Scan.lift kind)
850e84526745 export concl_of;
wenzelm
parents: 8688
diff changeset
   409
  (Scan.lift (Args.$$$ "_") >> K None || Args.local_term >> Some);
6446
583add9799c3 may specify induction predicates as well;
wenzelm
parents: 6442
diff changeset
   410
8344
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   411
fun mode name =
8815
187547eae4c5 use Args.colon / Args.parens;
wenzelm
parents: 8695
diff changeset
   412
  Scan.lift (Scan.optional (Args.parens (Args.$$$ name) >> K true) false);
8337
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
   413
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   414
in
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   415
8695
850e84526745 export concl_of;
wenzelm
parents: 8688
diff changeset
   416
val cases_args = Method.syntax (mode simplifiedN -- (Scan.option term -- Scan.option cases_rule));
850e84526745 export concl_of;
wenzelm
parents: 8688
diff changeset
   417
val induct_args = Method.syntax
850e84526745 export concl_of;
wenzelm
parents: 8688
diff changeset
   418
  (mode strippedN -- (Args.and_list (Scan.repeat term_dummy) -- Scan.option induct_rule));
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   419
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   420
end;
6446
583add9799c3 may specify induction predicates as well;
wenzelm
parents: 6442
diff changeset
   421
583add9799c3 may specify induction predicates as well;
wenzelm
parents: 6442
diff changeset
   422
6442
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
   423
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   424
(** theory setup **)
6446
583add9799c3 may specify induction predicates as well;
wenzelm
parents: 6442
diff changeset
   425
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   426
val setup =
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   427
  [GlobalInduct.init, LocalInduct.init,
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   428
   Attrib.add_attributes
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   429
    [(casesN, cases_attr, "cases rule for type or set"),
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   430
     (inductN, induct_attr, "induction rule for type or set")],
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   431
   Method.add_methods
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   432
    [("cases", cases_meth oo cases_args, "case analysis on types or sets"),
9066
b1e874e38dab theorems [cases type: bool] = case_split;
wenzelm
parents: 8815
diff changeset
   433
     ("induct", induct_meth oo induct_args, "induction on types or sets")],
b1e874e38dab theorems [cases type: bool] = case_split;
wenzelm
parents: 8815
diff changeset
   434
   (#1 o PureThy.add_thms [(("case_split", case_split), [])])];
6442
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
   435
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
   436
end;