src/HOL/Tools/inductive.ML
author wenzelm
Sat, 27 Apr 2013 20:50:20 +0200
changeset 51798 ad3a241def73
parent 51717 9e7d1c139569
child 52059 2f970c7f722b
permissions -rw-r--r--
uniform Proof.context for hyp_subst_tac;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31723
f5cafe803b55 discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents: 31177
diff changeset
     1
(*  Title:      HOL/Tools/inductive.ML
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
21367
7a0cc1bb4dcc inductive: canonical specification syntax (flattened result only);
wenzelm
parents: 21350
diff changeset
     3
    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
     4
6424
ceab9e663e08 tuned comments;
wenzelm
parents: 6394
diff changeset
     5
(Co)Inductive Definition module for HOL.
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
     6
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
     7
Features:
6424
ceab9e663e08 tuned comments;
wenzelm
parents: 6394
diff changeset
     8
  * least or greatest fixedpoints
ceab9e663e08 tuned comments;
wenzelm
parents: 6394
diff changeset
     9
  * mutually recursive definitions
ceab9e663e08 tuned comments;
wenzelm
parents: 6394
diff changeset
    10
  * definitions involving arbitrary monotone operators
ceab9e663e08 tuned comments;
wenzelm
parents: 6394
diff changeset
    11
  * automatically proves introduction and elimination rules
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
    12
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
    13
  Introduction rules have the form
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
    14
  [| M Pj ti, ..., Q x, ... |] ==> Pk t
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
    15
  where M is some monotone operator (usually the identity)
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
    16
  Q x is any side condition on the free variables
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
    17
  ti, t are any terms
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
    18
  Pj, Pk are two of the predicates being defined in mutual recursion
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
    19
*)
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
    20
31723
f5cafe803b55 discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents: 31177
diff changeset
    21
signature BASIC_INDUCTIVE =
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
    22
sig
33458
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
    23
  type inductive_result =
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
    24
    {preds: term list, elims: thm list, raw_induct: thm,
37734
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
    25
     induct: thm, inducts: thm list, intrs: thm list, eqs: thm list}
45290
f599ac41e7f5 tuned signature -- refined terminology;
wenzelm
parents: 44868
diff changeset
    26
  val transform_result: morphism -> inductive_result -> inductive_result
33458
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
    27
  type inductive_info = {names: string list, coind: bool} * inductive_result
21526
1e6bd5ed7abc added morh_result, the_inductive, add_inductive_global;
wenzelm
parents: 21508
diff changeset
    28
  val the_inductive: Proof.context -> string -> inductive_info
21367
7a0cc1bb4dcc inductive: canonical specification syntax (flattened result only);
wenzelm
parents: 21350
diff changeset
    29
  val print_inductives: Proof.context -> unit
45651
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
    30
  val get_monos: Proof.context -> thm list
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    31
  val mono_add: attribute
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    32
  val mono_del: attribute
21367
7a0cc1bb4dcc inductive: canonical specification syntax (flattened result only);
wenzelm
parents: 21350
diff changeset
    33
  val mk_cases: Proof.context -> term -> thm
10910
058775a575db export inductive_forall_name, inductive_forall_def, rulify;
wenzelm
parents: 10804
diff changeset
    34
  val inductive_forall_def: thm
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51658
diff changeset
    35
  val rulify: Proof.context -> thm -> thm
28839
32d498cf7595 eliminated rewrite_tac/fold_tac, which are not well-formed tactics due to change of main conclusion;
wenzelm
parents: 28791
diff changeset
    36
  val inductive_cases: (Attrib.binding * string list) list -> local_theory ->
28084
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28083
diff changeset
    37
    thm list list * local_theory
28839
32d498cf7595 eliminated rewrite_tac/fold_tac, which are not well-formed tactics due to change of main conclusion;
wenzelm
parents: 28791
diff changeset
    38
  val inductive_cases_i: (Attrib.binding * term list) list -> local_theory ->
28084
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28083
diff changeset
    39
    thm list list * local_theory
33458
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
    40
  type inductive_flags =
33669
ae9a2ea9a989 inductive: eliminated obsolete kind;
wenzelm
parents: 33666
diff changeset
    41
    {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool,
49170
03bee3a6a1b7 discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
wenzelm
parents: 47876
diff changeset
    42
      no_elim: bool, no_ind: bool, skip_mono: bool}
24815
f7093e90f36c tuned internal interfaces: flags record, added kind for results;
wenzelm
parents: 24744
diff changeset
    43
  val add_inductive_i:
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29388
diff changeset
    44
    inductive_flags -> ((binding * typ) * mixfix) list ->
28084
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28083
diff changeset
    45
    (string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory ->
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28083
diff changeset
    46
    inductive_result * local_theory
28083
103d9282a946 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27882
diff changeset
    47
  val add_inductive: bool -> bool ->
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29388
diff changeset
    48
    (binding * string option * mixfix) list ->
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29388
diff changeset
    49
    (binding * string option * mixfix) list ->
28084
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28083
diff changeset
    50
    (Attrib.binding * string) list ->
28083
103d9282a946 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27882
diff changeset
    51
    (Facts.ref * Attrib.src list) list ->
49324
4f28543ae7fa removed obsolete argument "int" and thus made SML/NJ happy (cf. 03bee3a6a1b7);
wenzelm
parents: 49170
diff changeset
    52
    local_theory -> inductive_result * local_theory
33726
0878aecbf119 eliminated slightly odd name space grouping -- now managed by Isar toplevel;
wenzelm
parents: 33671
diff changeset
    53
  val add_inductive_global: inductive_flags ->
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29388
diff changeset
    54
    ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
28084
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28083
diff changeset
    55
    thm list -> theory -> inductive_result * theory
22789
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
    56
  val arities_of: thm -> (string * int) list
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
    57
  val params_of: thm -> term list
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
    58
  val partition_rules: thm -> thm list -> (string * thm list) list
25822
05756950011c Added function partition_rules'.
berghofe
parents: 25510
diff changeset
    59
  val partition_rules': thm -> (thm * 'a) list -> (string * (thm * 'a) list) list
22789
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
    60
  val unpartition_rules: thm list -> (string * 'a list) list -> 'a list
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
    61
  val infer_intro_vars: thm -> int -> thm list -> term list list
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18678
diff changeset
    62
  val setup: theory -> theory
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
    63
end;
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
    64
31723
f5cafe803b55 discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents: 31177
diff changeset
    65
signature INDUCTIVE =
23762
24eef53a9ad3 Reorganization due to introduction of inductive_set wrapper.
berghofe
parents: 23577
diff changeset
    66
sig
31723
f5cafe803b55 discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents: 31177
diff changeset
    67
  include BASIC_INDUCTIVE
33458
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
    68
  type add_ind_def =
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
    69
    inductive_flags ->
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
    70
    term list -> (Attrib.binding * term) list -> thm list ->
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
    71
    term list -> (binding * mixfix) list ->
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
    72
    local_theory -> inductive_result * local_theory
35757
c2884bec5463 adding Spec_Rules to definitional package inductive and inductive_set
bulwahn
parents: 35646
diff changeset
    73
  val declare_rules: binding -> bool -> bool -> string list -> term list ->
34986
7f7939c9370f Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents: 33966
diff changeset
    74
    thm list -> binding list -> Attrib.src list list -> (thm * string list * int) list ->
37734
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
    75
    thm list -> thm -> local_theory -> thm list * thm list * thm list * thm * thm list * local_theory
23762
24eef53a9ad3 Reorganization due to introduction of inductive_set wrapper.
berghofe
parents: 23577
diff changeset
    76
  val add_ind_def: add_ind_def
28083
103d9282a946 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27882
diff changeset
    77
  val gen_add_inductive_i: add_ind_def -> inductive_flags ->
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29388
diff changeset
    78
    ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
28084
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28083
diff changeset
    79
    thm list -> local_theory -> inductive_result * local_theory
28083
103d9282a946 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27882
diff changeset
    80
  val gen_add_inductive: add_ind_def -> bool -> bool ->
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29388
diff changeset
    81
    (binding * string option * mixfix) list ->
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29388
diff changeset
    82
    (binding * string option * mixfix) list ->
28084
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28083
diff changeset
    83
    (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
49324
4f28543ae7fa removed obsolete argument "int" and thus made SML/NJ happy (cf. 03bee3a6a1b7);
wenzelm
parents: 49170
diff changeset
    84
    local_theory -> inductive_result * local_theory
4f28543ae7fa removed obsolete argument "int" and thus made SML/NJ happy (cf. 03bee3a6a1b7);
wenzelm
parents: 49170
diff changeset
    85
  val gen_ind_decl: add_ind_def -> bool -> (local_theory -> local_theory) parser
23762
24eef53a9ad3 Reorganization due to introduction of inductive_set wrapper.
berghofe
parents: 23577
diff changeset
    86
end;
24eef53a9ad3 Reorganization due to introduction of inductive_set wrapper.
berghofe
parents: 23577
diff changeset
    87
31723
f5cafe803b55 discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents: 31177
diff changeset
    88
structure Inductive: INDUCTIVE =
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
    89
struct
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
    90
10729
1b3350c4ee92 handle proper rules;
wenzelm
parents: 10569
diff changeset
    91
(** theory context references **)
1b3350c4ee92 handle proper rules;
wenzelm
parents: 10569
diff changeset
    92
32602
f2b741473860 more antiquotations
haftmann
parents: 32181
diff changeset
    93
val inductive_forall_def = @{thm induct_forall_def};
11991
da6ee05d9f3d use HOL.induct_XXX;
wenzelm
parents: 11880
diff changeset
    94
val inductive_conj_name = "HOL.induct_conj";
32602
f2b741473860 more antiquotations
haftmann
parents: 32181
diff changeset
    95
val inductive_conj_def = @{thm induct_conj_def};
f2b741473860 more antiquotations
haftmann
parents: 32181
diff changeset
    96
val inductive_conj = @{thms induct_conj};
f2b741473860 more antiquotations
haftmann
parents: 32181
diff changeset
    97
val inductive_atomize = @{thms induct_atomize};
f2b741473860 more antiquotations
haftmann
parents: 32181
diff changeset
    98
val inductive_rulify = @{thms induct_rulify};
f2b741473860 more antiquotations
haftmann
parents: 32181
diff changeset
    99
val inductive_rulify_fallback = @{thms induct_rulify_fallback};
10729
1b3350c4ee92 handle proper rules;
wenzelm
parents: 10569
diff changeset
   100
45649
wenzelm
parents: 45648
diff changeset
   101
val simp_thms1 =
wenzelm
parents: 45648
diff changeset
   102
  map mk_meta_eq
wenzelm
parents: 45648
diff changeset
   103
    @{lemma "(~ True) = False" "(~ False) = True"
wenzelm
parents: 45648
diff changeset
   104
        "(True --> P) = P" "(False --> P) = True"
wenzelm
parents: 45648
diff changeset
   105
        "(P & True) = P" "(True & P) = P"
wenzelm
parents: 45648
diff changeset
   106
      by (fact simp_thms)+};
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   107
45649
wenzelm
parents: 45648
diff changeset
   108
val simp_thms2 =
wenzelm
parents: 45648
diff changeset
   109
  map mk_meta_eq [@{thm inf_fun_def}, @{thm inf_bool_def}] @ simp_thms1;
32652
3175e23b79f3 stripped legacy ML bindings
haftmann
parents: 32610
diff changeset
   110
45649
wenzelm
parents: 45648
diff changeset
   111
val simp_thms3 =
wenzelm
parents: 45648
diff changeset
   112
  map mk_meta_eq [@{thm le_fun_def}, @{thm le_bool_def}, @{thm sup_fun_def}, @{thm sup_bool_def}];
10729
1b3350c4ee92 handle proper rules;
wenzelm
parents: 10569
diff changeset
   113
1b3350c4ee92 handle proper rules;
wenzelm
parents: 10569
diff changeset
   114
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   115
10735
dfaf75f0076f simplified quick_and_dirty stuff;
wenzelm
parents: 10729
diff changeset
   116
(** misc utilities **)
6424
ceab9e663e08 tuned comments;
wenzelm
parents: 6394
diff changeset
   117
26477
ecf06644f6cb eliminated quiete_mode ref (turned into proper argument);
wenzelm
parents: 26336
diff changeset
   118
fun message quiet_mode s = if quiet_mode then () else writeln s;
ecf06644f6cb eliminated quiete_mode ref (turned into proper argument);
wenzelm
parents: 26336
diff changeset
   119
fun clean_message quiet_mode s = if ! quick_and_dirty then () else message quiet_mode s;
5662
72a2e33d3b9e Added quiet_mode flag.
berghofe
parents: 5553
diff changeset
   120
6424
ceab9e663e08 tuned comments;
wenzelm
parents: 6394
diff changeset
   121
fun coind_prefix true = "co"
ceab9e663e08 tuned comments;
wenzelm
parents: 6394
diff changeset
   122
  | coind_prefix false = "";
ceab9e663e08 tuned comments;
wenzelm
parents: 6394
diff changeset
   123
45651
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   124
fun log (b: int) m n = if m >= n then 0 else 1 + log b (b * m) n;
6424
ceab9e663e08 tuned comments;
wenzelm
parents: 6394
diff changeset
   125
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   126
fun make_bool_args f g [] i = []
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   127
  | make_bool_args f g (x :: xs) i =
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   128
      (if i mod 2 = 0 then f x else g x) :: make_bool_args f g xs (i div 2);
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   129
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   130
fun make_bool_args' xs =
45740
132a3e1c0fe5 more antiquotations;
wenzelm
parents: 45652
diff changeset
   131
  make_bool_args (K @{term False}) (K @{term True}) xs;
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   132
33957
e9afca2118d4 normalized uncurry take/drop
haftmann
parents: 33955
diff changeset
   133
fun arg_types_of k c = drop k (binder_types (fastype_of c));
33077
3c9cf88ec841 arg_types_of auxiliary function; using multiset operations
haftmann
parents: 33056
diff changeset
   134
40316
665862241968 replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
wenzelm
parents: 39248
diff changeset
   135
fun find_arg T x [] = raise Fail "find_arg"
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   136
  | find_arg T x ((p as (_, (SOME _, _))) :: ps) =
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   137
      apsnd (cons p) (find_arg T x ps)
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   138
  | find_arg T x ((p as (U, (NONE, y))) :: ps) =
23577
c5b93c69afd3 avoid polymorphic equality;
wenzelm
parents: 22997
diff changeset
   139
      if (T: typ) = U then (y, (U, (SOME x, y)) :: ps)
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   140
      else apsnd (cons p) (find_arg T x ps);
7020
75ff179df7b7 Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents: 6851
diff changeset
   141
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   142
fun make_args Ts xs =
28524
644b62cf678f arbitrary is undefined
haftmann
parents: 28107
diff changeset
   143
  map (fn (T, (NONE, ())) => Const (@{const_name undefined}, T) | (_, (SOME t, ())) => t)
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   144
    (fold (fn (t, T) => snd o find_arg T t) xs (map (rpair (NONE, ())) Ts));
7020
75ff179df7b7 Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents: 6851
diff changeset
   145
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   146
fun make_args' Ts xs Us =
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   147
  fst (fold_map (fn T => find_arg T ()) Us (Ts ~~ map (pair NONE) xs));
7020
75ff179df7b7 Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents: 6851
diff changeset
   148
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   149
fun dest_predicate cs params t =
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   150
  let
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   151
    val k = length params;
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   152
    val (c, ts) = strip_comb t;
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   153
    val (xs, ys) = chop k ts;
31986
a68f88d264f7 dropped find_index_eq
haftmann
parents: 31902
diff changeset
   154
    val i = find_index (fn c' => c' = c) cs;
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   155
  in
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   156
    if xs = params andalso i >= 0 then
33077
3c9cf88ec841 arg_types_of auxiliary function; using multiset operations
haftmann
parents: 33056
diff changeset
   157
      SOME (c, i, ys, chop (length ys) (arg_types_of k c))
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   158
    else NONE
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   159
  end;
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   160
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   161
fun mk_names a 0 = []
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   162
  | mk_names a 1 = [a]
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   163
  | mk_names a n = map (fn i => a ^ string_of_int i) (1 upto n);
10988
e0016a009c17 Splitting of arguments of product types in induction rules is now less
berghofe
parents: 10910
diff changeset
   164
37734
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   165
fun select_disj 1 1 = []
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   166
  | select_disj _ 1 = [rtac disjI1]
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   167
  | select_disj n i = rtac disjI2 :: select_disj (n - 1) (i - 1);
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   168
6424
ceab9e663e08 tuned comments;
wenzelm
parents: 6394
diff changeset
   169
ceab9e663e08 tuned comments;
wenzelm
parents: 6394
diff changeset
   170
45651
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   171
(** context data **)
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   172
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   173
type inductive_result =
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   174
  {preds: term list, elims: thm list, raw_induct: thm,
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   175
   induct: thm, inducts: thm list, intrs: thm list, eqs: thm list};
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   176
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   177
fun transform_result phi {preds, elims, raw_induct: thm, induct, inducts, intrs, eqs} =
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   178
  let
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   179
    val term = Morphism.term phi;
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   180
    val thm = Morphism.thm phi;
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   181
    val fact = Morphism.fact phi;
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   182
  in
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   183
   {preds = map term preds, elims = fact elims, raw_induct = thm raw_induct,
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   184
    induct = thm induct, inducts = fact inducts, intrs = fact intrs, eqs = fact eqs}
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   185
  end;
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   186
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   187
type inductive_info = {names: string list, coind: bool} * inductive_result;
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   188
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   189
val empty_equations =
45652
18214436e1d3 permissive update for improved "tool compliance";
wenzelm
parents: 45651
diff changeset
   190
  Item_Net.init Thm.eq_thm_prop
18214436e1d3 permissive update for improved "tool compliance";
wenzelm
parents: 45651
diff changeset
   191
    (single o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of);
45651
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   192
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   193
datatype data = Data of
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   194
 {infos: inductive_info Symtab.table,
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   195
  monos: thm list,
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   196
  equations: thm Item_Net.T};
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   197
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   198
fun make_data (infos, monos, equations) =
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   199
  Data {infos = infos, monos = monos, equations = equations};
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   200
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   201
structure Data = Generic_Data
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   202
(
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   203
  type T = data;
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   204
  val empty = make_data (Symtab.empty, [], empty_equations);
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   205
  val extend = I;
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   206
  fun merge (Data {infos = infos1, monos = monos1, equations = equations1},
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   207
      Data {infos = infos2, monos = monos2, equations = equations2}) =
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   208
    make_data (Symtab.merge (K true) (infos1, infos2),
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   209
      Thm.merge_thms (monos1, monos2),
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   210
      Item_Net.merge (equations1, equations2));
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   211
);
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   212
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   213
fun map_data f =
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   214
  Data.map (fn Data {infos, monos, equations} => make_data (f (infos, monos, equations)));
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   215
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   216
fun rep_data ctxt = Data.get (Context.Proof ctxt) |> (fn Data rep => rep);
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   217
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   218
fun print_inductives ctxt =
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   219
  let
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   220
    val {infos, monos, ...} = rep_data ctxt;
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   221
    val space = Consts.space_of (Proof_Context.consts_of ctxt);
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   222
  in
50301
56b4c9afd7be print formal entities with markup;
wenzelm
parents: 50214
diff changeset
   223
    [Pretty.block
56b4c9afd7be print formal entities with markup;
wenzelm
parents: 50214
diff changeset
   224
      (Pretty.breaks
56b4c9afd7be print formal entities with markup;
wenzelm
parents: 50214
diff changeset
   225
        (Pretty.str "(co)inductives:" ::
56b4c9afd7be print formal entities with markup;
wenzelm
parents: 50214
diff changeset
   226
          map (Pretty.mark_str o #1) (Name_Space.extern_table ctxt (space, infos)))),
51584
98029ceda8ce more item markup;
wenzelm
parents: 51580
diff changeset
   227
     Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_item ctxt) monos)]
50301
56b4c9afd7be print formal entities with markup;
wenzelm
parents: 50214
diff changeset
   228
  end |> Pretty.chunks |> Pretty.writeln;
45651
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   229
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   230
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   231
(* inductive info *)
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   232
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   233
fun the_inductive ctxt name =
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   234
  (case Symtab.lookup (#infos (rep_data ctxt)) name of
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   235
    NONE => error ("Unknown (co)inductive predicate " ^ quote name)
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   236
  | SOME info => info);
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   237
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   238
fun put_inductives names info =
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   239
  map_data (fn (infos, monos, equations) =>
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   240
    (fold (fn name => Symtab.update (name, info)) names infos, monos, equations));
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   241
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   242
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   243
(* monotonicity rules *)
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   244
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   245
val get_monos = #monos o rep_data;
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   246
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   247
fun mk_mono ctxt thm =
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   248
  let
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   249
    fun eq_to_mono thm' = thm' RS (thm' RS @{thm eq_to_mono});
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   250
    fun dest_less_concl thm = dest_less_concl (thm RS @{thm le_funD})
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   251
      handle THM _ => thm RS @{thm le_boolD}
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   252
  in
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   253
    (case concl_of thm of
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   254
      Const ("==", _) $ _ $ _ => eq_to_mono (thm RS meta_eq_to_obj_eq)
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   255
    | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => eq_to_mono thm
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   256
    | _ $ (Const (@{const_name Orderings.less_eq}, _) $ _ $ _) =>
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   257
      dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   258
        (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   259
    | _ => thm)
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   260
  end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm ctxt thm);
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   261
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   262
val mono_add =
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   263
  Thm.declaration_attribute (fn thm => fn context =>
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   264
    map_data (fn (infos, monos, equations) =>
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   265
      (infos, Thm.add_thm (mk_mono (Context.proof_of context) thm) monos, equations)) context);
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   266
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   267
val mono_del =
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   268
  Thm.declaration_attribute (fn thm => fn context =>
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   269
    map_data (fn (infos, monos, equations) =>
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   270
      (infos, Thm.del_thm (mk_mono (Context.proof_of context) thm) monos, equations)) context);
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   271
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   272
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   273
(* equations *)
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   274
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   275
val get_equations = #equations o rep_data;
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   276
45652
18214436e1d3 permissive update for improved "tool compliance";
wenzelm
parents: 45651
diff changeset
   277
val equation_add_permissive =
45651
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   278
  Thm.declaration_attribute (fn thm =>
45652
18214436e1d3 permissive update for improved "tool compliance";
wenzelm
parents: 45651
diff changeset
   279
    map_data (fn (infos, monos, equations) =>
18214436e1d3 permissive update for improved "tool compliance";
wenzelm
parents: 45651
diff changeset
   280
      (infos, monos, perhaps (try (Item_Net.update thm)) equations)));
45651
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   281
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   282
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   283
10729
1b3350c4ee92 handle proper rules;
wenzelm
parents: 10569
diff changeset
   284
(** process rules **)
1b3350c4ee92 handle proper rules;
wenzelm
parents: 10569
diff changeset
   285
1b3350c4ee92 handle proper rules;
wenzelm
parents: 10569
diff changeset
   286
local
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   287
23762
24eef53a9ad3 Reorganization due to introduction of inductive_set wrapper.
berghofe
parents: 23577
diff changeset
   288
fun err_in_rule ctxt name t msg =
42381
309ec68442c6 added Binding.print convenience, which includes quote already;
wenzelm
parents: 42364
diff changeset
   289
  error (cat_lines ["Ill-formed introduction rule " ^ Binding.print name,
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24915
diff changeset
   290
    Syntax.string_of_term ctxt t, msg]);
10729
1b3350c4ee92 handle proper rules;
wenzelm
parents: 10569
diff changeset
   291
23762
24eef53a9ad3 Reorganization due to introduction of inductive_set wrapper.
berghofe
parents: 23577
diff changeset
   292
fun err_in_prem ctxt name t p msg =
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24915
diff changeset
   293
  error (cat_lines ["Ill-formed premise", Syntax.string_of_term ctxt p,
42381
309ec68442c6 added Binding.print convenience, which includes quote already;
wenzelm
parents: 42364
diff changeset
   294
    "in introduction rule " ^ Binding.print name, Syntax.string_of_term ctxt t, msg]);
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   295
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   296
val bad_concl = "Conclusion of introduction rule must be an inductive predicate";
10729
1b3350c4ee92 handle proper rules;
wenzelm
parents: 10569
diff changeset
   297
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   298
val bad_ind_occ = "Inductive predicate occurs in argument of inductive predicate";
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   299
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   300
val bad_app = "Inductive predicate must be applied to parameter(s) ";
11358
416ea5c009f5 now checks for leading meta-quantifiers and complains, instead of
paulson
parents: 11036
diff changeset
   301
41228
e1fce873b814 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents: 41075
diff changeset
   302
fun atomize_term thy = Raw_Simplifier.rewrite_term thy inductive_atomize [];
10729
1b3350c4ee92 handle proper rules;
wenzelm
parents: 10569
diff changeset
   303
1b3350c4ee92 handle proper rules;
wenzelm
parents: 10569
diff changeset
   304
in
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   305
28083
103d9282a946 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27882
diff changeset
   306
fun check_rule ctxt cs params ((binding, att), rule) =
10729
1b3350c4ee92 handle proper rules;
wenzelm
parents: 10569
diff changeset
   307
  let
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   308
    val params' = Term.variant_frees rule (Logic.strip_params rule);
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   309
    val frees = rev (map Free params');
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   310
    val concl = subst_bounds (frees, Logic.strip_assums_concl rule);
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   311
    val prems = map (curry subst_bounds frees) (Logic.strip_assums_hyp rule);
23762
24eef53a9ad3 Reorganization due to introduction of inductive_set wrapper.
berghofe
parents: 23577
diff changeset
   312
    val rule' = Logic.list_implies (prems, concl);
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42358
diff changeset
   313
    val aprems = map (atomize_term (Proof_Context.theory_of ctxt)) prems;
46215
0da9433f959e discontinued old-style Term.list_all_free in favour of plain Logic.all;
wenzelm
parents: 45740
diff changeset
   314
    val arule = fold_rev (Logic.all o Free) params' (Logic.list_implies (aprems, concl));
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   315
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   316
    fun check_ind err t =
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   317
      (case dest_predicate cs params t of
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   318
        NONE => err (bad_app ^
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24915
diff changeset
   319
          commas (map (Syntax.string_of_term ctxt) params))
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   320
      | SOME (_, _, ys, _) =>
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   321
          if exists (fn c => exists (fn t => Logic.occs (c, t)) ys) cs
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   322
          then err bad_ind_occ else ());
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   323
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   324
    fun check_prem' prem t =
36692
54b64d4ad524 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents: 36642
diff changeset
   325
      if member (op =) cs (head_of t) then
42381
309ec68442c6 added Binding.print convenience, which includes quote already;
wenzelm
parents: 42364
diff changeset
   326
        check_ind (err_in_prem ctxt binding rule prem) t
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   327
      else
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   328
        (case t of
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   329
          Abs (_, _, t) => check_prem' prem t
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   330
        | t $ u => (check_prem' prem t; check_prem' prem u)
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   331
        | _ => ());
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   332
10729
1b3350c4ee92 handle proper rules;
wenzelm
parents: 10569
diff changeset
   333
    fun check_prem (prem, aprem) =
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   334
      if can HOLogic.dest_Trueprop aprem then check_prem' prem prem
42381
309ec68442c6 added Binding.print convenience, which includes quote already;
wenzelm
parents: 42364
diff changeset
   335
      else err_in_prem ctxt binding rule prem "Non-atomic premise";
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   336
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   337
    val _ =
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   338
      (case concl of
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   339
        Const (@{const_name Trueprop}, _) $ t =>
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   340
          if member (op =) cs (head_of t) then
42381
309ec68442c6 added Binding.print convenience, which includes quote already;
wenzelm
parents: 42364
diff changeset
   341
           (check_ind (err_in_rule ctxt binding rule') t;
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   342
            List.app check_prem (prems ~~ aprems))
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   343
          else err_in_rule ctxt binding rule' bad_concl
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   344
       | _ => err_in_rule ctxt binding rule' bad_concl);
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   345
  in
28083
103d9282a946 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27882
diff changeset
   346
    ((binding, att), arule)
10729
1b3350c4ee92 handle proper rules;
wenzelm
parents: 10569
diff changeset
   347
  end;
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   348
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51658
diff changeset
   349
fun rulify ctxt =
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51658
diff changeset
   350
  hol_simplify ctxt inductive_conj
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51658
diff changeset
   351
  #> hol_simplify ctxt inductive_rulify
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51658
diff changeset
   352
  #> hol_simplify ctxt inductive_rulify_fallback
30552
58db56278478 provide Simplifier.norm_hhf(_protect) as regular simplifier operation;
wenzelm
parents: 30528
diff changeset
   353
  #> Simplifier.norm_hhf;
10729
1b3350c4ee92 handle proper rules;
wenzelm
parents: 10569
diff changeset
   354
1b3350c4ee92 handle proper rules;
wenzelm
parents: 10569
diff changeset
   355
end;
1b3350c4ee92 handle proper rules;
wenzelm
parents: 10569
diff changeset
   356
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   357
6424
ceab9e663e08 tuned comments;
wenzelm
parents: 6394
diff changeset
   358
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   359
(** proofs for (co)inductive predicates **)
6424
ceab9e663e08 tuned comments;
wenzelm
parents: 6394
diff changeset
   360
26534
a2cb4de2a1aa Added skip_mono flag and inductive_flags type.
berghofe
parents: 26477
diff changeset
   361
(* prove monotonicity *)
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   362
49170
03bee3a6a1b7 discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
wenzelm
parents: 47876
diff changeset
   363
fun prove_mono quiet_mode skip_mono predT fp_fun monos ctxt =
03bee3a6a1b7 discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
wenzelm
parents: 47876
diff changeset
   364
 (message (quiet_mode orelse skip_mono andalso ! quick_and_dirty)
26534
a2cb4de2a1aa Added skip_mono flag and inductive_flags type.
berghofe
parents: 26477
diff changeset
   365
    "  Proving monotonicity ...";
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 50771
diff changeset
   366
  (if skip_mono then Goal.prove_sorry else Goal.prove_future) ctxt
36642
084470c3cea2 Corrected handling of "for" parameters.
berghofe
parents: 36546
diff changeset
   367
    [] []
17985
d5d576b72371 avoid legacy goals;
wenzelm
parents: 17959
diff changeset
   368
    (HOLogic.mk_Trueprop
24815
f7093e90f36c tuned internal interfaces: flags record, added kind for results;
wenzelm
parents: 24744
diff changeset
   369
      (Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
25380
03201004c77e put_inductives: be permissive about multiple versions
wenzelm
parents: 25365
diff changeset
   370
    (fn _ => EVERY [rtac @{thm monoI} 1,
32652
3175e23b79f3 stripped legacy ML bindings
haftmann
parents: 32610
diff changeset
   371
      REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI'}] 1),
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   372
      REPEAT (FIRST
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   373
        [atac 1,
42439
9efdd0af15ac eliminated Display.string_of_thm_without_context;
wenzelm
parents: 42381
diff changeset
   374
         resolve_tac (map (mk_mono ctxt) monos @ get_monos ctxt) 1,
32652
3175e23b79f3 stripped legacy ML bindings
haftmann
parents: 32610
diff changeset
   375
         etac @{thm le_funE} 1, dtac @{thm le_boolD} 1])]));
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   376
6424
ceab9e663e08 tuned comments;
wenzelm
parents: 6394
diff changeset
   377
10735
dfaf75f0076f simplified quick_and_dirty stuff;
wenzelm
parents: 10729
diff changeset
   378
(* prove introduction rules *)
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   379
36642
084470c3cea2 Corrected handling of "for" parameters.
berghofe
parents: 36546
diff changeset
   380
fun prove_intrs quiet_mode coind mono fp_def k intr_ts rec_preds_defs ctxt ctxt' =
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   381
  let
26477
ecf06644f6cb eliminated quiete_mode ref (turned into proper argument);
wenzelm
parents: 26336
diff changeset
   382
    val _ = clean_message quiet_mode "  Proving the introduction rules ...";
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   383
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   384
    val unfold = funpow k (fn th => th RS fun_cong)
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   385
      (mono RS (fp_def RS
32652
3175e23b79f3 stripped legacy ML bindings
haftmann
parents: 32610
diff changeset
   386
        (if coind then @{thm def_gfp_unfold} else @{thm def_lfp_unfold})));
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   387
45648
7654f750fb43 more antiquotations;
wenzelm
parents: 45647
diff changeset
   388
    val rules = [refl, TrueI, @{lemma "~ False" by (rule notI)}, exI, conjI];
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   389
36642
084470c3cea2 Corrected handling of "for" parameters.
berghofe
parents: 36546
diff changeset
   390
    val intrs = map_index (fn (i, intr) =>
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 50771
diff changeset
   391
      Goal.prove_sorry ctxt [] [] intr (fn _ => EVERY
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   392
       [rewrite_goals_tac rec_preds_defs,
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   393
        rtac (unfold RS iffD2) 1,
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   394
        EVERY1 (select_disj (length intr_ts) (i + 1)),
17985
d5d576b72371 avoid legacy goals;
wenzelm
parents: 17959
diff changeset
   395
        (*Not ares_tac, since refl must be tried before any equality assumptions;
d5d576b72371 avoid legacy goals;
wenzelm
parents: 17959
diff changeset
   396
          backtracking may occur if the premises have extra variables!*)
36642
084470c3cea2 Corrected handling of "for" parameters.
berghofe
parents: 36546
diff changeset
   397
        DEPTH_SOLVE_1 (resolve_tac rules 1 APPEND assume_tac 1)])
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42358
diff changeset
   398
       |> singleton (Proof_Context.export ctxt ctxt')) intr_ts
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   399
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   400
  in (intrs, unfold) end;
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   401
6424
ceab9e663e08 tuned comments;
wenzelm
parents: 6394
diff changeset
   402
10735
dfaf75f0076f simplified quick_and_dirty stuff;
wenzelm
parents: 10729
diff changeset
   403
(* prove elimination rules *)
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   404
36642
084470c3cea2 Corrected handling of "for" parameters.
berghofe
parents: 36546
diff changeset
   405
fun prove_elims quiet_mode cs params intr_ts intr_names unfold rec_preds_defs ctxt ctxt''' =
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   406
  let
26477
ecf06644f6cb eliminated quiete_mode ref (turned into proper argument);
wenzelm
parents: 26336
diff changeset
   407
    val _ = clean_message quiet_mode "  Proving the elimination rules ...";
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   408
36642
084470c3cea2 Corrected handling of "for" parameters.
berghofe
parents: 36546
diff changeset
   409
    val ([pname], ctxt') = Variable.variant_fixes ["P"] ctxt;
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   410
    val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   411
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   412
    fun dest_intr r =
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   413
      (the (dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))),
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   414
       Logic.strip_assums_hyp r, Logic.strip_params r);
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   415
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   416
    val intrs = map dest_intr intr_ts ~~ intr_names;
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   417
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   418
    val rules1 = [disjE, exE, FalseE];
45648
7654f750fb43 more antiquotations;
wenzelm
parents: 45647
diff changeset
   419
    val rules2 = [conjE, FalseE, @{lemma "~ True ==> R" by (rule notE [OF _ TrueI])}];
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   420
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   421
    fun prove_elim c =
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   422
      let
33077
3c9cf88ec841 arg_types_of auxiliary function; using multiset operations
haftmann
parents: 33056
diff changeset
   423
        val Ts = arg_types_of (length params) c;
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   424
        val (anames, ctxt'') = Variable.variant_fixes (mk_names "a" (length Ts)) ctxt';
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   425
        val frees = map Free (anames ~~ Ts);
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   426
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   427
        fun mk_elim_prem ((_, _, us, _), ts, params') =
46218
ecf6375e2abb renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
wenzelm
parents: 46215
diff changeset
   428
          Logic.list_all (params',
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   429
            Logic.list_implies (map (HOLogic.mk_Trueprop o HOLogic.mk_eq)
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   430
              (frees ~~ us) @ ts, P));
33317
b4534348b8fd standardized filter/filter_out;
wenzelm
parents: 33278
diff changeset
   431
        val c_intrs = filter (equal c o #1 o #1 o #1) intrs;
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   432
        val prems = HOLogic.mk_Trueprop (list_comb (c, params @ frees)) ::
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   433
           map mk_elim_prem (map #1 c_intrs)
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   434
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 50771
diff changeset
   435
        (Goal.prove_sorry ctxt'' [] prems P
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   436
          (fn {prems, ...} => EVERY
46708
b138dee7bed3 prefer cut_tac, where it is clear that the special variants cut_rules_tac or cut_facts_tac are not required;
wenzelm
parents: 46219
diff changeset
   437
            [cut_tac (hd prems) 1,
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   438
             rewrite_goals_tac rec_preds_defs,
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   439
             dtac (unfold RS iffD1) 1,
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   440
             REPEAT (FIRSTGOAL (eresolve_tac rules1)),
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   441
             REPEAT (FIRSTGOAL (eresolve_tac rules2)),
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   442
             EVERY (map (fn prem =>
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   443
               DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_preds_defs prem, conjI] 1)) (tl prems))])
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42358
diff changeset
   444
          |> singleton (Proof_Context.export ctxt'' ctxt'''),
34986
7f7939c9370f Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents: 33966
diff changeset
   445
         map #2 c_intrs, length Ts)
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   446
      end
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   447
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   448
   in map prove_elim cs end;
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   449
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   450
37734
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   451
(* prove simplification equations *)
6424
ceab9e663e08 tuned comments;
wenzelm
parents: 6394
diff changeset
   452
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   453
fun prove_eqs quiet_mode cs params intr_ts intrs
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   454
    (elims: (thm * bstring list * int) list) ctxt ctxt'' =  (* FIXME ctxt'' ?? *)
37734
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   455
  let
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   456
    val _ = clean_message quiet_mode "  Proving the simplification rules ...";
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   457
37734
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   458
    fun dest_intr r =
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   459
      (the (dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))),
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   460
       Logic.strip_assums_hyp r, Logic.strip_params r);
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   461
    val intr_ts' = map dest_intr intr_ts;
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   462
37901
ea7d4423cb5b make SML/NJ happy, by adhoc type-constraints;
wenzelm
parents: 37734
diff changeset
   463
    fun prove_eq c (elim: thm * 'a * 'b) =
37734
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   464
      let
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   465
        val Ts = arg_types_of (length params) c;
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   466
        val (anames, ctxt') = Variable.variant_fixes (mk_names "a" (length Ts)) ctxt;
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   467
        val frees = map Free (anames ~~ Ts);
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   468
        val c_intrs = filter (equal c o #1 o #1 o #1) (intr_ts' ~~ intrs);
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   469
        fun mk_intr_conj (((_, _, us, _), ts, params'), _) =
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   470
          let
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   471
            fun list_ex ([], t) = t
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   472
              | list_ex ((a, T) :: vars, t) =
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   473
                  HOLogic.exists_const T $ Abs (a, T, list_ex (vars, t));
47876
0521ee2e504d tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents: 46961
diff changeset
   474
            val conjs = map2 (curry HOLogic.mk_eq) frees us @ map HOLogic.dest_Trueprop ts;
37734
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   475
          in
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   476
            list_ex (params', if null conjs then @{term True} else foldr1 HOLogic.mk_conj conjs)
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   477
          end;
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   478
        val lhs = list_comb (c, params @ frees);
37734
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   479
        val rhs =
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   480
          if null c_intrs then @{term False}
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   481
          else foldr1 HOLogic.mk_disj (map mk_intr_conj c_intrs);
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   482
        val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
37734
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   483
        fun prove_intr1 (i, _) = Subgoal.FOCUS_PREMS (fn {params, prems, ...} =>
47876
0521ee2e504d tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents: 46961
diff changeset
   484
            EVERY1 (select_disj (length c_intrs) (i + 1)) THEN
0521ee2e504d tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents: 46961
diff changeset
   485
            EVERY (replicate (length params) (rtac @{thm exI} 1)) THEN
0521ee2e504d tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents: 46961
diff changeset
   486
            (if null prems then rtac @{thm TrueI} 1
0521ee2e504d tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents: 46961
diff changeset
   487
             else
0521ee2e504d tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents: 46961
diff changeset
   488
              let
0521ee2e504d tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents: 46961
diff changeset
   489
                val (prems', last_prem) = split_last prems;
0521ee2e504d tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents: 46961
diff changeset
   490
              in
0521ee2e504d tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents: 46961
diff changeset
   491
                EVERY (map (fn prem => (rtac @{thm conjI} 1 THEN rtac prem 1)) prems') THEN
0521ee2e504d tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents: 46961
diff changeset
   492
                rtac last_prem 1
0521ee2e504d tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents: 46961
diff changeset
   493
              end)) ctxt' 1;
37734
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   494
        fun prove_intr2 (((_, _, us, _), ts, params'), intr) =
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   495
          EVERY (replicate (length params') (etac @{thm exE} 1)) THEN
47876
0521ee2e504d tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents: 46961
diff changeset
   496
          (if null ts andalso null us then rtac intr 1
0521ee2e504d tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents: 46961
diff changeset
   497
           else
0521ee2e504d tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents: 46961
diff changeset
   498
            EVERY (replicate (length ts + length us - 1) (etac @{thm conjE} 1)) THEN
0521ee2e504d tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents: 46961
diff changeset
   499
            Subgoal.FOCUS_PREMS (fn {params, prems, ...} =>
0521ee2e504d tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents: 46961
diff changeset
   500
              let
0521ee2e504d tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents: 46961
diff changeset
   501
                val (eqs, prems') = chop (length us) prems;
0521ee2e504d tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents: 46961
diff changeset
   502
                val rew_thms = map (fn th => th RS @{thm eq_reflection}) eqs;
0521ee2e504d tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents: 46961
diff changeset
   503
              in
0521ee2e504d tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents: 46961
diff changeset
   504
                rewrite_goal_tac rew_thms 1 THEN
0521ee2e504d tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents: 46961
diff changeset
   505
                rtac intr 1 THEN
0521ee2e504d tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents: 46961
diff changeset
   506
                EVERY (map (fn p => rtac p 1) prems')
0521ee2e504d tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents: 46961
diff changeset
   507
              end) ctxt' 1);
37734
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   508
      in
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 50771
diff changeset
   509
        Goal.prove_sorry ctxt' [] [] eq (fn _ =>
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   510
          rtac @{thm iffI} 1 THEN etac (#1 elim) 1 THEN
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   511
          EVERY (map_index prove_intr1 c_intrs) THEN
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   512
          (if null c_intrs then etac @{thm FalseE} 1
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   513
           else
37734
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   514
            let val (c_intrs', last_c_intr) = split_last c_intrs in
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   515
              EVERY (map (fn ci => etac @{thm disjE} 1 THEN prove_intr2 ci) c_intrs') THEN
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   516
              prove_intr2 last_c_intr
37734
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   517
            end))
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51658
diff changeset
   518
        |> rulify ctxt'
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42358
diff changeset
   519
        |> singleton (Proof_Context.export ctxt' ctxt'')
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   520
      end;
37734
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   521
  in
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   522
    map2 prove_eq cs elims
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   523
  end;
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   524
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   525
10735
dfaf75f0076f simplified quick_and_dirty stuff;
wenzelm
parents: 10729
diff changeset
   526
(* derivation of simplified elimination rules *)
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   527
11682
d9063229b4a1 simp_case_tac is back again from induct_method.ML;
wenzelm
parents: 11628
diff changeset
   528
local
d9063229b4a1 simp_case_tac is back again from induct_method.ML;
wenzelm
parents: 11628
diff changeset
   529
d9063229b4a1 simp_case_tac is back again from induct_method.ML;
wenzelm
parents: 11628
diff changeset
   530
(*delete needless equality assumptions*)
29064
70a61d58460e more antiquotations;
wenzelm
parents: 29006
diff changeset
   531
val refl_thin = Goal.prove_global @{theory HOL} [] [] @{prop "!!P. a = a ==> P ==> P"}
22838
haftmann
parents: 22789
diff changeset
   532
  (fn _ => assume_tac 1);
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   533
val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE];
11682
d9063229b4a1 simp_case_tac is back again from induct_method.ML;
wenzelm
parents: 11628
diff changeset
   534
val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
d9063229b4a1 simp_case_tac is back again from induct_method.ML;
wenzelm
parents: 11628
diff changeset
   535
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51658
diff changeset
   536
fun simp_case_tac ctxt i =
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51717
diff changeset
   537
  EVERY' [elim_tac, asm_full_simp_tac ctxt, elim_tac, REPEAT o bound_hyp_subst_tac ctxt] i;
21367
7a0cc1bb4dcc inductive: canonical specification syntax (flattened result only);
wenzelm
parents: 21350
diff changeset
   538
11682
d9063229b4a1 simp_case_tac is back again from induct_method.ML;
wenzelm
parents: 11628
diff changeset
   539
in
9598
65ee72db0236 raplaced "intrs" by "intrs" (new-style only);
wenzelm
parents: 9562
diff changeset
   540
21367
7a0cc1bb4dcc inductive: canonical specification syntax (flattened result only);
wenzelm
parents: 21350
diff changeset
   541
fun mk_cases ctxt prop =
7107
ce69de572bca inductive_cases(_i): Isar interface to mk_cases;
wenzelm
parents: 7020
diff changeset
   542
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42358
diff changeset
   543
    val thy = Proof_Context.theory_of ctxt;
21367
7a0cc1bb4dcc inductive: canonical specification syntax (flattened result only);
wenzelm
parents: 21350
diff changeset
   544
21526
1e6bd5ed7abc added morh_result, the_inductive, add_inductive_global;
wenzelm
parents: 21508
diff changeset
   545
    fun err msg =
1e6bd5ed7abc added morh_result, the_inductive, add_inductive_global;
wenzelm
parents: 21508
diff changeset
   546
      error (Pretty.string_of (Pretty.block
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24915
diff changeset
   547
        [Pretty.str msg, Pretty.fbrk, Syntax.pretty_term ctxt prop]));
21526
1e6bd5ed7abc added morh_result, the_inductive, add_inductive_global;
wenzelm
parents: 21508
diff changeset
   548
24861
cc669ca5f382 tuned Induct interface: prefer pred'' over set'';
wenzelm
parents: 24830
diff changeset
   549
    val elims = Induct.find_casesP ctxt prop;
21367
7a0cc1bb4dcc inductive: canonical specification syntax (flattened result only);
wenzelm
parents: 21350
diff changeset
   550
7a0cc1bb4dcc inductive: canonical specification syntax (flattened result only);
wenzelm
parents: 21350
diff changeset
   551
    val cprop = Thm.cterm_of thy prop;
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51658
diff changeset
   552
    val tac = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac;
21367
7a0cc1bb4dcc inductive: canonical specification syntax (flattened result only);
wenzelm
parents: 21350
diff changeset
   553
    fun mk_elim rl =
36546
a9873318fe30 proper context for rule_by_tactic;
wenzelm
parents: 36468
diff changeset
   554
      Thm.implies_intr cprop (Tactic.rule_by_tactic ctxt tac (Thm.assume cprop RS rl))
21367
7a0cc1bb4dcc inductive: canonical specification syntax (flattened result only);
wenzelm
parents: 21350
diff changeset
   555
      |> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt);
7107
ce69de572bca inductive_cases(_i): Isar interface to mk_cases;
wenzelm
parents: 7020
diff changeset
   556
  in
ce69de572bca inductive_cases(_i): Isar interface to mk_cases;
wenzelm
parents: 7020
diff changeset
   557
    (case get_first (try mk_elim) elims of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15525
diff changeset
   558
      SOME r => r
21526
1e6bd5ed7abc added morh_result, the_inductive, add_inductive_global;
wenzelm
parents: 21508
diff changeset
   559
    | NONE => err "Proposition not an inductive predicate:")
7107
ce69de572bca inductive_cases(_i): Isar interface to mk_cases;
wenzelm
parents: 7020
diff changeset
   560
  end;
ce69de572bca inductive_cases(_i): Isar interface to mk_cases;
wenzelm
parents: 7020
diff changeset
   561
11682
d9063229b4a1 simp_case_tac is back again from induct_method.ML;
wenzelm
parents: 11628
diff changeset
   562
end;
d9063229b4a1 simp_case_tac is back again from induct_method.ML;
wenzelm
parents: 11628
diff changeset
   563
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   564
21367
7a0cc1bb4dcc inductive: canonical specification syntax (flattened result only);
wenzelm
parents: 21350
diff changeset
   565
(* inductive_cases *)
7107
ce69de572bca inductive_cases(_i): Isar interface to mk_cases;
wenzelm
parents: 7020
diff changeset
   566
21367
7a0cc1bb4dcc inductive: canonical specification syntax (flattened result only);
wenzelm
parents: 21350
diff changeset
   567
fun gen_inductive_cases prep_att prep_prop args lthy =
9598
65ee72db0236 raplaced "intrs" by "intrs" (new-style only);
wenzelm
parents: 9562
diff changeset
   568
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42358
diff changeset
   569
    val thy = Proof_Context.theory_of lthy;
46915
4b2eccaec3f6 more parallel inductive_cases;
wenzelm
parents: 46893
diff changeset
   570
    val thmss =
4b2eccaec3f6 more parallel inductive_cases;
wenzelm
parents: 46893
diff changeset
   571
      map snd args
4b2eccaec3f6 more parallel inductive_cases;
wenzelm
parents: 46893
diff changeset
   572
      |> burrow (grouped 10 Par_List.map (mk_cases lthy o prep_prop lthy));
4b2eccaec3f6 more parallel inductive_cases;
wenzelm
parents: 46893
diff changeset
   573
    val facts =
4b2eccaec3f6 more parallel inductive_cases;
wenzelm
parents: 46893
diff changeset
   574
      map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att thy) atts), [(thms, [])]))
4b2eccaec3f6 more parallel inductive_cases;
wenzelm
parents: 46893
diff changeset
   575
        args thmss;
33671
4b0f2599ed48 modernized structure Local_Theory;
wenzelm
parents: 33670
diff changeset
   576
  in lthy |> Local_Theory.notes facts |>> map snd end;
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   577
24509
23ee6b7788c2 replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents: 24133
diff changeset
   578
val inductive_cases = gen_inductive_cases Attrib.intern_src Syntax.read_prop;
23ee6b7788c2 replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents: 24133
diff changeset
   579
val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
7107
ce69de572bca inductive_cases(_i): Isar interface to mk_cases;
wenzelm
parents: 7020
diff changeset
   580
6424
ceab9e663e08 tuned comments;
wenzelm
parents: 6394
diff changeset
   581
30722
623d4831c8cf simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents: 30552
diff changeset
   582
val ind_cases_setup =
623d4831c8cf simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents: 30552
diff changeset
   583
  Method.setup @{binding ind_cases}
623d4831c8cf simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents: 30552
diff changeset
   584
    (Scan.lift (Scan.repeat1 Args.name_source --
42491
4bb5de0aae66 more precise position information via Variable.add_fixes_binding;
wenzelm
parents: 42439
diff changeset
   585
      Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.binding) []) >>
30722
623d4831c8cf simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents: 30552
diff changeset
   586
      (fn (raw_props, fixes) => fn ctxt =>
623d4831c8cf simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents: 30552
diff changeset
   587
        let
42491
4bb5de0aae66 more precise position information via Variable.add_fixes_binding;
wenzelm
parents: 42439
diff changeset
   588
          val (_, ctxt') = Variable.add_fixes_binding fixes ctxt;
30722
623d4831c8cf simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents: 30552
diff changeset
   589
          val props = Syntax.read_props ctxt' raw_props;
623d4831c8cf simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents: 30552
diff changeset
   590
          val ctxt'' = fold Variable.declare_term props ctxt';
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42358
diff changeset
   591
          val rules = Proof_Context.export ctxt'' ctxt (map (mk_cases ctxt'') props)
30722
623d4831c8cf simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents: 30552
diff changeset
   592
        in Method.erule 0 rules end))
623d4831c8cf simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents: 30552
diff changeset
   593
    "dynamic case analysis on predicates";
9598
65ee72db0236 raplaced "intrs" by "intrs" (new-style only);
wenzelm
parents: 9562
diff changeset
   594
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   595
37734
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   596
(* derivation of simplified equation *)
9598
65ee72db0236 raplaced "intrs" by "intrs" (new-style only);
wenzelm
parents: 9562
diff changeset
   597
37734
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   598
fun mk_simp_eq ctxt prop =
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   599
  let
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   600
    val thy = Proof_Context.theory_of ctxt;
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   601
    val ctxt' = Variable.auto_fixes prop ctxt;
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   602
    val lhs_of = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of;
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   603
    val substs =
45649
wenzelm
parents: 45648
diff changeset
   604
      Item_Net.retrieve (get_equations ctxt) (HOLogic.dest_Trueprop prop)
38665
e92223c886f8 introducing simplification equations for inductive sets; added data structure for storing equations; rewriting retrieval of simplification equation for inductive predicates and sets
bulwahn
parents: 38388
diff changeset
   605
      |> map_filter
e92223c886f8 introducing simplification equations for inductive sets; added data structure for storing equations; rewriting retrieval of simplification equation for inductive predicates and sets
bulwahn
parents: 38388
diff changeset
   606
        (fn eq => SOME (Pattern.match thy (lhs_of eq, HOLogic.dest_Trueprop prop)
e92223c886f8 introducing simplification equations for inductive sets; added data structure for storing equations; rewriting retrieval of simplification equation for inductive predicates and sets
bulwahn
parents: 38388
diff changeset
   607
            (Vartab.empty, Vartab.empty), eq)
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   608
          handle Pattern.MATCH => NONE);
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   609
    val (subst, eq) =
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   610
      (case substs of
38665
e92223c886f8 introducing simplification equations for inductive sets; added data structure for storing equations; rewriting retrieval of simplification equation for inductive predicates and sets
bulwahn
parents: 38388
diff changeset
   611
        [s] => s
e92223c886f8 introducing simplification equations for inductive sets; added data structure for storing equations; rewriting retrieval of simplification equation for inductive predicates and sets
bulwahn
parents: 38388
diff changeset
   612
      | _ => error
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   613
        ("equations matching pattern " ^ Syntax.string_of_term ctxt prop ^ " is not unique"));
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   614
    val inst =
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   615
      map (fn v => (cterm_of thy (Var v), cterm_of thy (Envir.subst_term subst (Var v))))
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   616
        (Term.add_vars (lhs_of eq) []);
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   617
  in
45651
172aa230ce69 just one data slot per module;
wenzelm
parents: 45649
diff changeset
   618
    Drule.cterm_instantiate inst eq
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51658
diff changeset
   619
    |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (Simplifier.full_rewrite ctxt)))
37734
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   620
    |> singleton (Variable.export ctxt' ctxt)
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   621
  end
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   622
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   623
37734
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   624
(* inductive simps *)
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   625
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   626
fun gen_inductive_simps prep_att prep_prop args lthy =
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   627
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42358
diff changeset
   628
    val thy = Proof_Context.theory_of lthy;
37734
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   629
    val facts = args |> map (fn ((a, atts), props) =>
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   630
      ((a, map (prep_att thy) atts),
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   631
        map (Thm.no_attributes o single o mk_simp_eq lthy o prep_prop lthy) props));
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   632
  in lthy |> Local_Theory.notes facts |>> map snd end;
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   633
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   634
val inductive_simps = gen_inductive_simps Attrib.intern_src Syntax.read_prop;
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   635
val inductive_simps_i = gen_inductive_simps (K I) Syntax.check_prop;
40902
bulwahn
parents: 40316
diff changeset
   636
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   637
10735
dfaf75f0076f simplified quick_and_dirty stuff;
wenzelm
parents: 10729
diff changeset
   638
(* prove induction rule *)
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   639
26477
ecf06644f6cb eliminated quiete_mode ref (turned into proper argument);
wenzelm
parents: 26336
diff changeset
   640
fun prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   641
    fp_def rec_preds_defs ctxt ctxt''' =  (* FIXME ctxt''' ?? *)
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   642
  let
26477
ecf06644f6cb eliminated quiete_mode ref (turned into proper argument);
wenzelm
parents: 26336
diff changeset
   643
    val _ = clean_message quiet_mode "  Proving the induction rule ...";
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   644
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   645
    (* predicates for induction rule *)
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   646
36642
084470c3cea2 Corrected handling of "for" parameters.
berghofe
parents: 36546
diff changeset
   647
    val (pnames, ctxt') = Variable.variant_fixes (mk_names "P" (length cs)) ctxt;
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   648
    val preds =
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   649
      map2 (curry Free) pnames
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   650
        (map (fn c => arg_types_of (length params) c ---> HOLogic.boolT) cs);
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   651
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   652
    (* transform an introduction rule into a premise for induction rule *)
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   653
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   654
    fun mk_ind_prem r =
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   655
      let
33669
ae9a2ea9a989 inductive: eliminated obsolete kind;
wenzelm
parents: 33666
diff changeset
   656
        fun subst s =
ae9a2ea9a989 inductive: eliminated obsolete kind;
wenzelm
parents: 33666
diff changeset
   657
          (case dest_predicate cs params s of
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   658
            SOME (_, i, ys, (_, Ts)) =>
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   659
              let
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   660
                val k = length Ts;
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   661
                val bs = map Bound (k - 1 downto 0);
42364
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 42361
diff changeset
   662
                val P = list_comb (nth preds i, map (incr_boundvars k) ys @ bs);
46219
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 46218
diff changeset
   663
                val Q =
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 46218
diff changeset
   664
                  fold_rev Term.abs (mk_names "x" k ~~ Ts)
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 46218
diff changeset
   665
                    (HOLogic.mk_binop inductive_conj_name
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 46218
diff changeset
   666
                      (list_comb (incr_boundvars k s, bs), P));
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   667
              in (Q, case Ts of [] => SOME (s, P) | _ => NONE) end
33669
ae9a2ea9a989 inductive: eliminated obsolete kind;
wenzelm
parents: 33666
diff changeset
   668
          | NONE =>
ae9a2ea9a989 inductive: eliminated obsolete kind;
wenzelm
parents: 33666
diff changeset
   669
              (case s of
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   670
                t $ u => (fst (subst t) $ fst (subst u), NONE)
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   671
              | Abs (a, T, t) => (Abs (a, T, fst (subst t)), NONE)
33669
ae9a2ea9a989 inductive: eliminated obsolete kind;
wenzelm
parents: 33666
diff changeset
   672
              | _ => (s, NONE)));
7293
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents: 7257
diff changeset
   673
33338
de76079f973a eliminated some old folds;
wenzelm
parents: 33317
diff changeset
   674
        fun mk_prem s prems =
de76079f973a eliminated some old folds;
wenzelm
parents: 33317
diff changeset
   675
          (case subst s of
de76079f973a eliminated some old folds;
wenzelm
parents: 33317
diff changeset
   676
            (_, SOME (t, u)) => t :: u :: prems
de76079f973a eliminated some old folds;
wenzelm
parents: 33317
diff changeset
   677
          | (t, _) => t :: prems);
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   678
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   679
        val SOME (_, i, ys, _) =
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   680
          dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r));
42364
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 42361
diff changeset
   681
      in
46215
0da9433f959e discontinued old-style Term.list_all_free in favour of plain Logic.all;
wenzelm
parents: 45740
diff changeset
   682
        fold_rev (Logic.all o Free) (Logic.strip_params r)
0da9433f959e discontinued old-style Term.list_all_free in favour of plain Logic.all;
wenzelm
parents: 45740
diff changeset
   683
          (Logic.list_implies (map HOLogic.mk_Trueprop (fold_rev mk_prem
42364
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 42361
diff changeset
   684
            (map HOLogic.dest_Trueprop (Logic.strip_assums_hyp r)) []),
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 42361
diff changeset
   685
              HOLogic.mk_Trueprop (list_comb (nth preds i, ys))))
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   686
      end;
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   687
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   688
    val ind_prems = map mk_ind_prem intr_ts;
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   689
21526
1e6bd5ed7abc added morh_result, the_inductive, add_inductive_global;
wenzelm
parents: 21508
diff changeset
   690
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   691
    (* make conclusions for induction rules *)
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   692
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   693
    val Tss = map (binder_types o fastype_of) preds;
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   694
    val (xnames, ctxt'') = Variable.variant_fixes (mk_names "x" (length (flat Tss))) ctxt';
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   695
    val mutual_ind_concl =
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   696
      HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   697
        (map (fn (((xnames, Ts), c), P) =>
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   698
          let val frees = map Free (xnames ~~ Ts)
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   699
          in HOLogic.mk_imp (list_comb (c, params @ frees), list_comb (P, frees)) end)
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   700
        (unflat Tss xnames ~~ Tss ~~ cs ~~ preds)));
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   701
13626
282fbabec862 Fixed bug involving inductive definitions having equalities in the premises,
paulson
parents: 13197
diff changeset
   702
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   703
    (* make predicate for instantiation of abstract induction rule *)
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   704
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   705
    val ind_pred =
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   706
      fold_rev lambda (bs @ xs) (foldr1 HOLogic.mk_conj
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   707
        (map_index (fn (i, P) => fold_rev (curry HOLogic.mk_imp)
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   708
           (make_bool_args HOLogic.mk_not I bs i)
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   709
           (list_comb (P, make_args' argTs xs (binder_types (fastype_of P))))) preds));
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   710
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   711
    val ind_concl =
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   712
      HOLogic.mk_Trueprop
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   713
        (HOLogic.mk_binrel @{const_name Orderings.less_eq} (rec_const, ind_pred));
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   714
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   715
    val raw_fp_induct = mono RS (fp_def RS @{thm def_lfp_induct});
13626
282fbabec862 Fixed bug involving inductive definitions having equalities in the premises,
paulson
parents: 13197
diff changeset
   716
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 50771
diff changeset
   717
    val induct = Goal.prove_sorry ctxt'' [] ind_prems ind_concl
20248
7916ce5bb069 Goal.prove: more tactic arguments;
wenzelm
parents: 20071
diff changeset
   718
      (fn {prems, ...} => EVERY
17985
d5d576b72371 avoid legacy goals;
wenzelm
parents: 17959
diff changeset
   719
        [rewrite_goals_tac [inductive_conj_def],
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   720
         DETERM (rtac raw_fp_induct 1),
32652
3175e23b79f3 stripped legacy ML bindings
haftmann
parents: 32610
diff changeset
   721
         REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI}] 1),
45649
wenzelm
parents: 45648
diff changeset
   722
         rewrite_goals_tac simp_thms2,
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   723
         (*This disjE separates out the introduction rules*)
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   724
         REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])),
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   725
         (*Now break down the individual cases.  No disjE here in case
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   726
           some premise involves disjunction.*)
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51717
diff changeset
   727
         REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac ctxt'')),
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   728
         REPEAT (FIRSTGOAL
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   729
           (resolve_tac [conjI, impI] ORELSE' (etac notE THEN' atac))),
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   730
         EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule
45649
wenzelm
parents: 45648
diff changeset
   731
             (inductive_conj_def :: rec_preds_defs @ simp_thms2) prem,
22980
1226d861eefb Fixed bug that caused proof of induction theorem to fail if
berghofe
parents: 22846
diff changeset
   732
           conjI, refl] 1)) prems)]);
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   733
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 50771
diff changeset
   734
    val lemma = Goal.prove_sorry ctxt'' [] []
17985
d5d576b72371 avoid legacy goals;
wenzelm
parents: 17959
diff changeset
   735
      (Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn _ => EVERY
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   736
        [rewrite_goals_tac rec_preds_defs,
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   737
         REPEAT (EVERY
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   738
           [REPEAT (resolve_tac [conjI, impI] 1),
32652
3175e23b79f3 stripped legacy ML bindings
haftmann
parents: 32610
diff changeset
   739
            REPEAT (eresolve_tac [@{thm le_funE}, @{thm le_boolE}] 1),
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   740
            atac 1,
45649
wenzelm
parents: 45648
diff changeset
   741
            rewrite_goals_tac simp_thms1,
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   742
            atac 1])]);
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   743
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42358
diff changeset
   744
  in singleton (Proof_Context.export ctxt'' ctxt''') (induct RS lemma) end;
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   745
6424
ceab9e663e08 tuned comments;
wenzelm
parents: 6394
diff changeset
   746
ceab9e663e08 tuned comments;
wenzelm
parents: 6394
diff changeset
   747
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   748
(** specification of (co)inductive predicates **)
10729
1b3350c4ee92 handle proper rules;
wenzelm
parents: 10569
diff changeset
   749
49170
03bee3a6a1b7 discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
wenzelm
parents: 47876
diff changeset
   750
fun mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts monos params cnames_syn lthy =
33458
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
   751
  let
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24867
diff changeset
   752
    val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp};
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   753
33077
3c9cf88ec841 arg_types_of auxiliary function; using multiset operations
haftmann
parents: 33056
diff changeset
   754
    val argTs = fold (combine (op =) o arg_types_of (length params)) cs [];
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   755
    val k = log 2 1 (length cs);
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   756
    val predT = replicate k HOLogic.boolT ---> argTs ---> HOLogic.boolT;
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   757
    val p :: xs =
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   758
      map Free (Variable.variant_frees lthy intr_ts
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   759
        (("p", predT) :: (mk_names "x" (length argTs) ~~ argTs)));
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   760
    val bs =
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   761
      map Free (Variable.variant_frees lthy (p :: xs @ intr_ts)
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   762
        (map (rpair HOLogic.boolT) (mk_names "b" k)));
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   763
33458
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
   764
    fun subst t =
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
   765
      (case dest_predicate cs params t of
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   766
        SOME (_, i, ts, (Ts, Us)) =>
23762
24eef53a9ad3 Reorganization due to introduction of inductive_set wrapper.
berghofe
parents: 23577
diff changeset
   767
          let
24eef53a9ad3 Reorganization due to introduction of inductive_set wrapper.
berghofe
parents: 23577
diff changeset
   768
            val l = length Us;
33669
ae9a2ea9a989 inductive: eliminated obsolete kind;
wenzelm
parents: 33666
diff changeset
   769
            val zs = map Bound (l - 1 downto 0);
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   770
          in
46219
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 46218
diff changeset
   771
            fold_rev (Term.abs o pair "z") Us
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 46218
diff changeset
   772
              (list_comb (p,
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 46218
diff changeset
   773
                make_bool_args' bs i @ make_args argTs
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 46218
diff changeset
   774
                  ((map (incr_boundvars l) ts ~~ Ts) @ (zs ~~ Us))))
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   775
          end
33669
ae9a2ea9a989 inductive: eliminated obsolete kind;
wenzelm
parents: 33666
diff changeset
   776
      | NONE =>
ae9a2ea9a989 inductive: eliminated obsolete kind;
wenzelm
parents: 33666
diff changeset
   777
          (case t of
ae9a2ea9a989 inductive: eliminated obsolete kind;
wenzelm
parents: 33666
diff changeset
   778
            t1 $ t2 => subst t1 $ subst t2
ae9a2ea9a989 inductive: eliminated obsolete kind;
wenzelm
parents: 33666
diff changeset
   779
          | Abs (x, T, u) => Abs (x, T, subst u)
ae9a2ea9a989 inductive: eliminated obsolete kind;
wenzelm
parents: 33666
diff changeset
   780
          | _ => t));
5149
10f0be29c0d1 Fixed bug in transform_rule.
berghofe
parents: 5120
diff changeset
   781
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   782
    (* transform an introduction rule into a conjunction  *)
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   783
    (*   [| p_i t; ... |] ==> p_j u                       *)
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   784
    (* is transformed into                                *)
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   785
    (*   b_j & x_j = u & p b_j t & ...                    *)
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   786
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   787
    fun transform_rule r =
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   788
      let
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   789
        val SOME (_, i, ts, (Ts, _)) =
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   790
          dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r));
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   791
        val ps =
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   792
          make_bool_args HOLogic.mk_not I bs i @
21048
e57e91f72831 Restructured and repaired code dealing with case names
berghofe
parents: 21024
diff changeset
   793
          map HOLogic.mk_eq (make_args' argTs xs Ts ~~ ts) @
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   794
          map (subst o HOLogic.dest_Trueprop) (Logic.strip_assums_hyp r);
33338
de76079f973a eliminated some old folds;
wenzelm
parents: 33317
diff changeset
   795
      in
de76079f973a eliminated some old folds;
wenzelm
parents: 33317
diff changeset
   796
        fold_rev (fn (x, T) => fn P => HOLogic.exists_const T $ Abs (x, T, P))
de76079f973a eliminated some old folds;
wenzelm
parents: 33317
diff changeset
   797
          (Logic.strip_params r)
45740
132a3e1c0fe5 more antiquotations;
wenzelm
parents: 45652
diff changeset
   798
          (if null ps then @{term True} else foldr1 HOLogic.mk_conj ps)
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   799
      end;
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   800
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   801
    (* make a disjunction of all introduction rules *)
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   802
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   803
    val fp_fun =
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   804
      fold_rev lambda (p :: bs @ xs)
45740
132a3e1c0fe5 more antiquotations;
wenzelm
parents: 45652
diff changeset
   805
        (if null intr_ts then @{term False}
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   806
         else foldr1 HOLogic.mk_disj (map transform_rule intr_ts));
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   807
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   808
    (* add definiton of recursive predicates to theory *)
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   809
28083
103d9282a946 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27882
diff changeset
   810
    val rec_name =
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28941
diff changeset
   811
      if Binding.is_empty alt_name then
30223
24d975352879 renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents: 30218
diff changeset
   812
        Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn))
28083
103d9282a946 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27882
diff changeset
   813
      else alt_name;
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   814
33458
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
   815
    val ((rec_const, (_, fp_def)), lthy') = lthy
33671
4b0f2599ed48 modernized structure Local_Theory;
wenzelm
parents: 33670
diff changeset
   816
      |> Local_Theory.conceal
33766
c679f05600cd adapted Local_Theory.define -- eliminated odd thm kind;
wenzelm
parents: 33726
diff changeset
   817
      |> Local_Theory.define
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   818
        ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
46915
4b2eccaec3f6 more parallel inductive_cases;
wenzelm
parents: 46893
diff changeset
   819
         ((Thm.def_binding rec_name, @{attributes [nitpick_unfold]}),
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45291
diff changeset
   820
           fold_rev lambda params
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45291
diff changeset
   821
             (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
33671
4b0f2599ed48 modernized structure Local_Theory;
wenzelm
parents: 33670
diff changeset
   822
      ||> Local_Theory.restore_naming lthy;
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   823
    val fp_def' =
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51658
diff changeset
   824
      Simplifier.rewrite (put_simpset HOL_basic_ss lthy' addsimps [fp_def])
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   825
        (cterm_of (Proof_Context.theory_of lthy') (list_comb (rec_const, params)));
33278
ba9f52f56356 conceal internal bindings;
wenzelm
parents: 33171
diff changeset
   826
    val specs =
ba9f52f56356 conceal internal bindings;
wenzelm
parents: 33171
diff changeset
   827
      if length cs < 2 then []
ba9f52f56356 conceal internal bindings;
wenzelm
parents: 33171
diff changeset
   828
      else
ba9f52f56356 conceal internal bindings;
wenzelm
parents: 33171
diff changeset
   829
        map_index (fn (i, (name_mx, c)) =>
ba9f52f56356 conceal internal bindings;
wenzelm
parents: 33171
diff changeset
   830
          let
ba9f52f56356 conceal internal bindings;
wenzelm
parents: 33171
diff changeset
   831
            val Ts = arg_types_of (length params) c;
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   832
            val xs =
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   833
              map Free (Variable.variant_frees lthy intr_ts (mk_names "x" (length Ts) ~~ Ts));
33278
ba9f52f56356 conceal internal bindings;
wenzelm
parents: 33171
diff changeset
   834
          in
39248
4a3747517552 only conceal primitive definition theorems, not predicate names
haftmann
parents: 38864
diff changeset
   835
            (name_mx, (apfst Binding.conceal Attrib.empty_binding, fold_rev lambda (params @ xs)
33278
ba9f52f56356 conceal internal bindings;
wenzelm
parents: 33171
diff changeset
   836
              (list_comb (rec_const, params @ make_bool_args' bs i @
ba9f52f56356 conceal internal bindings;
wenzelm
parents: 33171
diff changeset
   837
                make_args argTs (xs ~~ Ts)))))
ba9f52f56356 conceal internal bindings;
wenzelm
parents: 33171
diff changeset
   838
          end) (cnames_syn ~~ cs);
33458
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
   839
    val (consts_defs, lthy'') = lthy'
39248
4a3747517552 only conceal primitive definition theorems, not predicate names
haftmann
parents: 38864
diff changeset
   840
      |> fold_map Local_Theory.define specs;
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   841
    val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   842
36642
084470c3cea2 Corrected handling of "for" parameters.
berghofe
parents: 36546
diff changeset
   843
    val (_, lthy''') = Variable.add_fixes (map (fst o dest_Free) params) lthy'';
49170
03bee3a6a1b7 discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
wenzelm
parents: 47876
diff changeset
   844
    val mono = prove_mono quiet_mode skip_mono predT fp_fun monos lthy''';
36642
084470c3cea2 Corrected handling of "for" parameters.
berghofe
parents: 36546
diff changeset
   845
    val (_, lthy'''') =
084470c3cea2 Corrected handling of "for" parameters.
berghofe
parents: 36546
diff changeset
   846
      Local_Theory.note (apfst Binding.conceal Attrib.empty_binding,
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42358
diff changeset
   847
        Proof_Context.export lthy''' lthy'' [mono]) lthy'';
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   848
36642
084470c3cea2 Corrected handling of "for" parameters.
berghofe
parents: 36546
diff changeset
   849
  in (lthy'''', lthy''', rec_name, mono, fp_def', map (#2 o #2) consts_defs,
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   850
    list_comb (rec_const, params), preds, argTs, bs, xs)
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   851
  end;
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   852
33669
ae9a2ea9a989 inductive: eliminated obsolete kind;
wenzelm
parents: 33666
diff changeset
   853
fun declare_rules rec_binding coind no_ind cnames
37734
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   854
    preds intrs intr_bindings intr_atts elims eqs raw_induct lthy =
23762
24eef53a9ad3 Reorganization due to introduction of inductive_set wrapper.
berghofe
parents: 23577
diff changeset
   855
  let
30223
24d975352879 renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents: 30218
diff changeset
   856
    val rec_name = Binding.name_of rec_binding;
32773
f6fd4ccd8eea mandatory prefix where appropriate
haftmann
parents: 32652
diff changeset
   857
    fun rec_qualified qualified = Binding.qualify qualified rec_name;
30223
24d975352879 renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents: 30218
diff changeset
   858
    val intr_names = map Binding.name_of intr_bindings;
33368
b1cf34f1855c modernized structure Rule_Cases;
wenzelm
parents: 33338
diff changeset
   859
    val ind_case_names = Rule_Cases.case_names intr_names;
23762
24eef53a9ad3 Reorganization due to introduction of inductive_set wrapper.
berghofe
parents: 23577
diff changeset
   860
    val induct =
24eef53a9ad3 Reorganization due to introduction of inductive_set wrapper.
berghofe
parents: 23577
diff changeset
   861
      if coind then
50771
2852f997bfb5 prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
wenzelm
parents: 50302
diff changeset
   862
        (raw_induct,
2852f997bfb5 prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
wenzelm
parents: 50302
diff changeset
   863
         [Rule_Cases.case_names [rec_name],
33368
b1cf34f1855c modernized structure Rule_Cases;
wenzelm
parents: 33338
diff changeset
   864
          Rule_Cases.case_conclusion (rec_name, intr_names),
50771
2852f997bfb5 prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
wenzelm
parents: 50302
diff changeset
   865
          Rule_Cases.consumes (1 - Thm.nprems_of raw_induct),
2852f997bfb5 prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
wenzelm
parents: 50302
diff changeset
   866
          Induct.coinduct_pred (hd cnames)])
23762
24eef53a9ad3 Reorganization due to introduction of inductive_set wrapper.
berghofe
parents: 23577
diff changeset
   867
      else if no_ind orelse length cnames > 1 then
50771
2852f997bfb5 prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
wenzelm
parents: 50302
diff changeset
   868
        (raw_induct,
2852f997bfb5 prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
wenzelm
parents: 50302
diff changeset
   869
          [ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of raw_induct))])
2852f997bfb5 prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
wenzelm
parents: 50302
diff changeset
   870
      else
2852f997bfb5 prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
wenzelm
parents: 50302
diff changeset
   871
        (raw_induct RSN (2, rev_mp),
2852f997bfb5 prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
wenzelm
parents: 50302
diff changeset
   872
          [ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of raw_induct))]);
23762
24eef53a9ad3 Reorganization due to introduction of inductive_set wrapper.
berghofe
parents: 23577
diff changeset
   873
33458
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
   874
    val (intrs', lthy1) =
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
   875
      lthy |>
35757
c2884bec5463 adding Spec_Rules to definitional package inductive and inductive_set
bulwahn
parents: 35646
diff changeset
   876
      Spec_Rules.add
c2884bec5463 adding Spec_Rules to definitional package inductive and inductive_set
bulwahn
parents: 35646
diff changeset
   877
        (if coind then Spec_Rules.Co_Inductive else Spec_Rules.Inductive) (preds, intrs) |>
33671
4b0f2599ed48 modernized structure Local_Theory;
wenzelm
parents: 33670
diff changeset
   878
      Local_Theory.notes
33278
ba9f52f56356 conceal internal bindings;
wenzelm
parents: 33171
diff changeset
   879
        (map (rec_qualified false) intr_bindings ~~ intr_atts ~~
ba9f52f56356 conceal internal bindings;
wenzelm
parents: 33171
diff changeset
   880
          map (fn th => [([th],
37264
8b931fb51cc6 removed "nitpick_intro" attribute -- Nitpick noew uses Spec_Rules instead
blanchet
parents: 36960
diff changeset
   881
           [Attrib.internal (K (Context_Rules.intro_query NONE))])]) intrs) |>>
24744
dcb8cf5fc99c - add_inductive_i now takes typ instead of typ option as argument
berghofe
parents: 24721
diff changeset
   882
      map (hd o snd);
33458
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
   883
    val (((_, elims'), (_, [induct'])), lthy2) =
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
   884
      lthy1 |>
33671
4b0f2599ed48 modernized structure Local_Theory;
wenzelm
parents: 33670
diff changeset
   885
      Local_Theory.note ((rec_qualified true (Binding.name "intros"), []), intrs') ||>>
34986
7f7939c9370f Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents: 33966
diff changeset
   886
      fold_map (fn (name, (elim, cases, k)) =>
33671
4b0f2599ed48 modernized structure Local_Theory;
wenzelm
parents: 33670
diff changeset
   887
        Local_Theory.note
33458
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
   888
          ((Binding.qualify true (Long_Name.base_name name) (Binding.name "cases"),
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
   889
            [Attrib.internal (K (Rule_Cases.case_names cases)),
50771
2852f997bfb5 prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
wenzelm
parents: 50302
diff changeset
   890
             Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of elim))),
34986
7f7939c9370f Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents: 33966
diff changeset
   891
             Attrib.internal (K (Rule_Cases.constraints k)),
33458
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
   892
             Attrib.internal (K (Induct.cases_pred name)),
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
   893
             Attrib.internal (K (Context_Rules.elim_query NONE))]), [elim]) #>
23762
24eef53a9ad3 Reorganization due to introduction of inductive_set wrapper.
berghofe
parents: 23577
diff changeset
   894
        apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
33671
4b0f2599ed48 modernized structure Local_Theory;
wenzelm
parents: 33670
diff changeset
   895
      Local_Theory.note
32773
f6fd4ccd8eea mandatory prefix where appropriate
haftmann
parents: 32652
diff changeset
   896
        ((rec_qualified true (Binding.name (coind_prefix coind ^ "induct")),
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51658
diff changeset
   897
          map (Attrib.internal o K) (#2 induct)), [rulify lthy1 (#1 induct)]);
23762
24eef53a9ad3 Reorganization due to introduction of inductive_set wrapper.
berghofe
parents: 23577
diff changeset
   898
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   899
    val (eqs', lthy3) = lthy2 |>
37734
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   900
      fold_map (fn (name, eq) => Local_Theory.note
38665
e92223c886f8 introducing simplification equations for inductive sets; added data structure for storing equations; rewriting retrieval of simplification equation for inductive predicates and sets
bulwahn
parents: 38388
diff changeset
   901
          ((Binding.qualify true (Long_Name.base_name name) (Binding.name "simps"),
45652
18214436e1d3 permissive update for improved "tool compliance";
wenzelm
parents: 45651
diff changeset
   902
            [Attrib.internal (K equation_add_permissive)]), [eq])
37734
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   903
          #> apfst (hd o snd))
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   904
        (if null eqs then [] else (cnames ~~ eqs))
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   905
    val (inducts, lthy4) =
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   906
      if no_ind orelse coind then ([], lthy3)
33458
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
   907
      else
37734
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   908
        let val inducts = cnames ~~ Project_Rule.projects lthy3 (1 upto length cnames) induct' in
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   909
          lthy3 |>
33671
4b0f2599ed48 modernized structure Local_Theory;
wenzelm
parents: 33670
diff changeset
   910
          Local_Theory.notes [((rec_qualified true (Binding.name "inducts"), []),
33458
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
   911
            inducts |> map (fn (name, th) => ([th],
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
   912
              [Attrib.internal (K ind_case_names),
50771
2852f997bfb5 prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
wenzelm
parents: 50302
diff changeset
   913
               Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th))),
35646
b32d6c1bdb4d Added inducts field to inductive_result.
berghofe
parents: 35625
diff changeset
   914
               Attrib.internal (K (Induct.induct_pred name))])))] |>> snd o hd
33458
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
   915
        end;
37734
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   916
  in (intrs', elims', eqs', induct', inducts, lthy4) end;
23762
24eef53a9ad3 Reorganization due to introduction of inductive_set wrapper.
berghofe
parents: 23577
diff changeset
   917
26534
a2cb4de2a1aa Added skip_mono flag and inductive_flags type.
berghofe
parents: 26477
diff changeset
   918
type inductive_flags =
33669
ae9a2ea9a989 inductive: eliminated obsolete kind;
wenzelm
parents: 33666
diff changeset
   919
  {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool,
49170
03bee3a6a1b7 discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
wenzelm
parents: 47876
diff changeset
   920
    no_elim: bool, no_ind: bool, skip_mono: bool};
26534
a2cb4de2a1aa Added skip_mono flag and inductive_flags type.
berghofe
parents: 26477
diff changeset
   921
a2cb4de2a1aa Added skip_mono flag and inductive_flags type.
berghofe
parents: 26477
diff changeset
   922
type add_ind_def =
a2cb4de2a1aa Added skip_mono flag and inductive_flags type.
berghofe
parents: 26477
diff changeset
   923
  inductive_flags ->
28084
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28083
diff changeset
   924
  term list -> (Attrib.binding * term) list -> thm list ->
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29388
diff changeset
   925
  term list -> (binding * mixfix) list ->
33458
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
   926
  local_theory -> inductive_result * local_theory;
23762
24eef53a9ad3 Reorganization due to introduction of inductive_set wrapper.
berghofe
parents: 23577
diff changeset
   927
49170
03bee3a6a1b7 discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
wenzelm
parents: 47876
diff changeset
   928
fun add_ind_def {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono}
33458
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
   929
    cs intros monos params cnames_syn lthy =
9072
a4896cf23638 Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents: 8720
diff changeset
   930
  let
25288
6e0c8dd213df improved error message for missing predicates;
wenzelm
parents: 25143
diff changeset
   931
    val _ = null cnames_syn andalso error "No inductive predicates given";
30223
24d975352879 renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents: 30218
diff changeset
   932
    val names = map (Binding.name_of o fst) cnames_syn;
26477
ecf06644f6cb eliminated quiete_mode ref (turned into proper argument);
wenzelm
parents: 26336
diff changeset
   933
    val _ = message (quiet_mode andalso not verbose)
28083
103d9282a946 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27882
diff changeset
   934
      ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ commas_quote names);
9072
a4896cf23638 Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents: 8720
diff changeset
   935
33671
4b0f2599ed48 modernized structure Local_Theory;
wenzelm
parents: 33670
diff changeset
   936
    val cnames = map (Local_Theory.full_name lthy o #1) cnames_syn;  (* FIXME *)
23762
24eef53a9ad3 Reorganization due to introduction of inductive_set wrapper.
berghofe
parents: 23577
diff changeset
   937
    val ((intr_names, intr_atts), intr_ts) =
33458
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
   938
      apfst split_list (split_list (map (check_rule lthy cs params) intros));
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   939
36642
084470c3cea2 Corrected handling of "for" parameters.
berghofe
parents: 36546
diff changeset
   940
    val (lthy1, lthy2, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds,
49170
03bee3a6a1b7 discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
wenzelm
parents: 47876
diff changeset
   941
      argTs, bs, xs) = mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts
33458
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
   942
        monos params cnames_syn lthy;
9072
a4896cf23638 Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents: 8720
diff changeset
   943
26477
ecf06644f6cb eliminated quiete_mode ref (turned into proper argument);
wenzelm
parents: 26336
diff changeset
   944
    val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs)
36642
084470c3cea2 Corrected handling of "for" parameters.
berghofe
parents: 36546
diff changeset
   945
      intr_ts rec_preds_defs lthy2 lthy1;
33459
wenzelm
parents: 33458
diff changeset
   946
    val elims =
wenzelm
parents: 33458
diff changeset
   947
      if no_elim then []
wenzelm
parents: 33458
diff changeset
   948
      else
wenzelm
parents: 33458
diff changeset
   949
        prove_elims quiet_mode cs params intr_ts (map Binding.name_of intr_names)
36642
084470c3cea2 Corrected handling of "for" parameters.
berghofe
parents: 36546
diff changeset
   950
          unfold rec_preds_defs lthy2 lthy1;
22605
41b092e7d89a - Removed occurrences of ProofContext.export in add_ind_def that
berghofe
parents: 22460
diff changeset
   951
    val raw_induct = zero_var_indexes
33459
wenzelm
parents: 33458
diff changeset
   952
      (if no_ind then Drule.asm_rl
wenzelm
parents: 33458
diff changeset
   953
       else if coind then
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42358
diff changeset
   954
         singleton (Proof_Context.export lthy2 lthy1)
35625
9c818cab0dd0 modernized structure Object_Logic;
wenzelm
parents: 35624
diff changeset
   955
           (rotate_prems ~1 (Object_Logic.rulify
28839
32d498cf7595 eliminated rewrite_tac/fold_tac, which are not well-formed tactics due to change of main conclusion;
wenzelm
parents: 28791
diff changeset
   956
             (fold_rule rec_preds_defs
45649
wenzelm
parents: 45648
diff changeset
   957
               (rewrite_rule simp_thms3
32652
3175e23b79f3 stripped legacy ML bindings
haftmann
parents: 32610
diff changeset
   958
                (mono RS (fp_def RS @{thm def_coinduct}))))))
21024
63ab84bb64d1 Completely rewrote inductive definition package. Now allows to
berghofe
parents: 20901
diff changeset
   959
       else
26477
ecf06644f6cb eliminated quiete_mode ref (turned into proper argument);
wenzelm
parents: 26336
diff changeset
   960
         prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def
36642
084470c3cea2 Corrected handling of "for" parameters.
berghofe
parents: 36546
diff changeset
   961
           rec_preds_defs lthy2 lthy1);
37734
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   962
    val eqs =
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   963
      if no_elim then [] else prove_eqs quiet_mode cs params intr_ts intrs elims lthy2 lthy1;
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   964
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51658
diff changeset
   965
    val elims' = map (fn (th, ns, i) => (rulify lthy1 th, ns, i)) elims;
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51658
diff changeset
   966
    val intrs' = map (rulify lthy1) intrs;
37734
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   967
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   968
    val (intrs'', elims'', eqs', induct, inducts, lthy3) =
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   969
      declare_rules rec_name coind no_ind
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
   970
        cnames preds intrs' intr_names intr_atts elims' eqs raw_induct lthy1;
21048
e57e91f72831 Restructured and repaired code dealing with case names
berghofe
parents: 21024
diff changeset
   971
e57e91f72831 Restructured and repaired code dealing with case names
berghofe
parents: 21024
diff changeset
   972
    val result =
e57e91f72831 Restructured and repaired code dealing with case names
berghofe
parents: 21024
diff changeset
   973
      {preds = preds,
37734
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   974
       intrs = intrs'',
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   975
       elims = elims'',
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51658
diff changeset
   976
       raw_induct = rulify lthy3 raw_induct,
35646
b32d6c1bdb4d Added inducts field to inductive_result.
berghofe
parents: 35625
diff changeset
   977
       induct = induct,
37734
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   978
       inducts = inducts,
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
   979
       eqs = eqs'};
21367
7a0cc1bb4dcc inductive: canonical specification syntax (flattened result only);
wenzelm
parents: 21350
diff changeset
   980
36642
084470c3cea2 Corrected handling of "for" parameters.
berghofe
parents: 36546
diff changeset
   981
    val lthy4 = lthy3
45291
57cd50f98fdc uniform Local_Theory.declaration with explicit params;
wenzelm
parents: 45290
diff changeset
   982
      |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi =>
45290
f599ac41e7f5 tuned signature -- refined terminology;
wenzelm
parents: 44868
diff changeset
   983
        let val result' = transform_result phi result;
25380
03201004c77e put_inductives: be permissive about multiple versions
wenzelm
parents: 25365
diff changeset
   984
        in put_inductives cnames (*global names!?*) ({names = cnames, coind = coind}, result') end);
36642
084470c3cea2 Corrected handling of "for" parameters.
berghofe
parents: 36546
diff changeset
   985
  in (result, lthy4) end;
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   986
6424
ceab9e663e08 tuned comments;
wenzelm
parents: 6394
diff changeset
   987
10735
dfaf75f0076f simplified quick_and_dirty stuff;
wenzelm
parents: 10729
diff changeset
   988
(* external interfaces *)
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   989
26477
ecf06644f6cb eliminated quiete_mode ref (turned into proper argument);
wenzelm
parents: 26336
diff changeset
   990
fun gen_add_inductive_i mk_def
49170
03bee3a6a1b7 discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
wenzelm
parents: 47876
diff changeset
   991
    (flags as {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono})
25029
3a72718c5ddd gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents: 25016
diff changeset
   992
    cnames_syn pnames spec monos lthy =
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   993
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42358
diff changeset
   994
    val thy = Proof_Context.theory_of lthy;
6424
ceab9e663e08 tuned comments;
wenzelm
parents: 6394
diff changeset
   995
    val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
   996
21766
3eb48154388e Abbreviations can now be specified simultaneously
berghofe
parents: 21658
diff changeset
   997
25029
3a72718c5ddd gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents: 25016
diff changeset
   998
    (* abbrevs *)
3a72718c5ddd gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents: 25016
diff changeset
   999
30223
24d975352879 renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents: 30218
diff changeset
  1000
    val (_, ctxt1) = Variable.add_fixes (map (Binding.name_of o fst o fst) cnames_syn) lthy;
21766
3eb48154388e Abbreviations can now be specified simultaneously
berghofe
parents: 21658
diff changeset
  1001
25029
3a72718c5ddd gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents: 25016
diff changeset
  1002
    fun get_abbrev ((name, atts), t) =
3a72718c5ddd gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents: 25016
diff changeset
  1003
      if can (Logic.strip_assums_concl #> Logic.dest_equals) t then
3a72718c5ddd gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents: 25016
diff changeset
  1004
        let
29006
abe0f11cfa4e Name.name_of -> Binding.base_name
haftmann
parents: 28965
diff changeset
  1005
          val _ = Binding.is_empty name andalso null atts orelse
25029
3a72718c5ddd gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents: 25016
diff changeset
  1006
            error "Abbreviations may not have names or attributes";
35624
c4e29a0bb8c1 modernized structure Local_Defs;
wenzelm
parents: 35364
diff changeset
  1007
          val ((x, T), rhs) = Local_Defs.abs_def (snd (Local_Defs.cert_def ctxt1 t));
28083
103d9282a946 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27882
diff changeset
  1008
          val var =
30223
24d975352879 renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents: 30218
diff changeset
  1009
            (case find_first (fn ((c, _), _) => Binding.name_of c = x) cnames_syn of
25029
3a72718c5ddd gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents: 25016
diff changeset
  1010
              NONE => error ("Undeclared head of abbreviation " ^ quote x)
28083
103d9282a946 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27882
diff changeset
  1011
            | SOME ((b, T'), mx) =>
25029
3a72718c5ddd gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents: 25016
diff changeset
  1012
                if T <> T' then error ("Bad type specification for abbreviation " ^ quote x)
28083
103d9282a946 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27882
diff changeset
  1013
                else (b, mx));
103d9282a946 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27882
diff changeset
  1014
        in SOME (var, rhs) end
25029
3a72718c5ddd gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents: 25016
diff changeset
  1015
      else NONE;
21766
3eb48154388e Abbreviations can now be specified simultaneously
berghofe
parents: 21658
diff changeset
  1016
25029
3a72718c5ddd gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents: 25016
diff changeset
  1017
    val abbrevs = map_filter get_abbrev spec;
30223
24d975352879 renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents: 30218
diff changeset
  1018
    val bs = map (Binding.name_of o fst o fst) abbrevs;
25029
3a72718c5ddd gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents: 25016
diff changeset
  1019
21766
3eb48154388e Abbreviations can now be specified simultaneously
berghofe
parents: 21658
diff changeset
  1020
25029
3a72718c5ddd gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents: 25016
diff changeset
  1021
    (* predicates *)
21766
3eb48154388e Abbreviations can now be specified simultaneously
berghofe
parents: 21658
diff changeset
  1022
25029
3a72718c5ddd gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents: 25016
diff changeset
  1023
    val pre_intros = filter_out (is_some o get_abbrev) spec;
30223
24d975352879 renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents: 30218
diff changeset
  1024
    val cnames_syn' = filter_out (member (op =) bs o Binding.name_of o fst o fst) cnames_syn;
24d975352879 renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents: 30218
diff changeset
  1025
    val cs = map (Free o apfst Binding.name_of o fst) cnames_syn';
25029
3a72718c5ddd gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents: 25016
diff changeset
  1026
    val ps = map Free pnames;
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
  1027
30223
24d975352879 renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents: 30218
diff changeset
  1028
    val (_, ctxt2) = lthy |> Variable.add_fixes (map (Binding.name_of o fst o fst) cnames_syn');
35624
c4e29a0bb8c1 modernized structure Local_Defs;
wenzelm
parents: 35364
diff changeset
  1029
    val _ = map (fn abbr => Local_Defs.fixed_abbrev abbr ctxt2) abbrevs;
c4e29a0bb8c1 modernized structure Local_Defs;
wenzelm
parents: 35364
diff changeset
  1030
    val ctxt3 = ctxt2 |> fold (snd oo Local_Defs.fixed_abbrev) abbrevs;
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42358
diff changeset
  1031
    val expand = Assumption.export_term ctxt3 lthy #> Proof_Context.cert_term lthy;
25029
3a72718c5ddd gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents: 25016
diff changeset
  1032
46215
0da9433f959e discontinued old-style Term.list_all_free in favour of plain Logic.all;
wenzelm
parents: 45740
diff changeset
  1033
    fun close_rule r =
0da9433f959e discontinued old-style Term.list_all_free in favour of plain Logic.all;
wenzelm
parents: 45740
diff changeset
  1034
      fold (Logic.all o Free) (fold_aterms
0da9433f959e discontinued old-style Term.list_all_free in favour of plain Logic.all;
wenzelm
parents: 45740
diff changeset
  1035
        (fn t as Free (v as (s, _)) =>
0da9433f959e discontinued old-style Term.list_all_free in favour of plain Logic.all;
wenzelm
parents: 45740
diff changeset
  1036
            if Variable.is_fixed ctxt1 s orelse
0da9433f959e discontinued old-style Term.list_all_free in favour of plain Logic.all;
wenzelm
parents: 45740
diff changeset
  1037
              member (op =) ps t then I else insert (op =) v
0da9433f959e discontinued old-style Term.list_all_free in favour of plain Logic.all;
wenzelm
parents: 45740
diff changeset
  1038
          | _ => I) r []) r;
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
  1039
26736
e6091328718f added explicit check phase after reading of specification
haftmann
parents: 26534
diff changeset
  1040
    val intros = map (apsnd (Syntax.check_term lthy #> close_rule #> expand)) pre_intros;
25029
3a72718c5ddd gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents: 25016
diff changeset
  1041
    val preds = map (fn ((c, _), mx) => (c, mx)) cnames_syn';
21048
e57e91f72831 Restructured and repaired code dealing with case names
berghofe
parents: 21024
diff changeset
  1042
  in
25029
3a72718c5ddd gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents: 25016
diff changeset
  1043
    lthy
3a72718c5ddd gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents: 25016
diff changeset
  1044
    |> mk_def flags cs intros monos ps preds
33671
4b0f2599ed48 modernized structure Local_Theory;
wenzelm
parents: 33670
diff changeset
  1045
    ||> fold (snd oo Local_Theory.abbrev Syntax.mode_default) abbrevs
21048
e57e91f72831 Restructured and repaired code dealing with case names
berghofe
parents: 21024
diff changeset
  1046
  end;
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
  1047
49324
4f28543ae7fa removed obsolete argument "int" and thus made SML/NJ happy (cf. 03bee3a6a1b7);
wenzelm
parents: 49170
diff changeset
  1048
fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos lthy =
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
  1049
  let
30486
9cdc7ce0e389 simplified preparation and outer parsing of specification;
wenzelm
parents: 30435
diff changeset
  1050
    val ((vars, intrs), _) = lthy
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42358
diff changeset
  1051
      |> Proof_Context.set_mode Proof_Context.mode_abbrev
30486
9cdc7ce0e389 simplified preparation and outer parsing of specification;
wenzelm
parents: 30435
diff changeset
  1052
      |> Specification.read_spec (cnames_syn @ pnames_syn) intro_srcs;
24721
2a029b78db60 proper Specification.read_specification;
wenzelm
parents: 24516
diff changeset
  1053
    val (cs, ps) = chop (length cnames_syn) vars;
2a029b78db60 proper Specification.read_specification;
wenzelm
parents: 24516
diff changeset
  1054
    val monos = Attrib.eval_thms lthy raw_monos;
49170
03bee3a6a1b7 discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
wenzelm
parents: 47876
diff changeset
  1055
    val flags =
03bee3a6a1b7 discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
wenzelm
parents: 47876
diff changeset
  1056
     {quiet_mode = false, verbose = verbose, alt_name = Binding.empty,
03bee3a6a1b7 discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
wenzelm
parents: 47876
diff changeset
  1057
      coind = coind, no_elim = false, no_ind = false, skip_mono = false};
26128
fe2d24c26e0c inductive package: simplified group handling;
wenzelm
parents: 25978
diff changeset
  1058
  in
fe2d24c26e0c inductive package: simplified group handling;
wenzelm
parents: 25978
diff changeset
  1059
    lthy
30223
24d975352879 renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents: 30218
diff changeset
  1060
    |> gen_add_inductive_i mk_def flags cs (map (apfst Binding.name_of o fst) ps) intrs monos
26128
fe2d24c26e0c inductive package: simplified group handling;
wenzelm
parents: 25978
diff changeset
  1061
  end;
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
  1062
23762
24eef53a9ad3 Reorganization due to introduction of inductive_set wrapper.
berghofe
parents: 23577
diff changeset
  1063
val add_inductive_i = gen_add_inductive_i add_ind_def;
24eef53a9ad3 Reorganization due to introduction of inductive_set wrapper.
berghofe
parents: 23577
diff changeset
  1064
val add_inductive = gen_add_inductive add_ind_def;
24eef53a9ad3 Reorganization due to introduction of inductive_set wrapper.
berghofe
parents: 23577
diff changeset
  1065
33726
0878aecbf119 eliminated slightly odd name space grouping -- now managed by Isar toplevel;
wenzelm
parents: 33671
diff changeset
  1066
fun add_inductive_global flags cnames_syn pnames pre_intros monos thy =
25380
03201004c77e put_inductives: be permissive about multiple versions
wenzelm
parents: 25365
diff changeset
  1067
  let
29006
abe0f11cfa4e Name.name_of -> Binding.base_name
haftmann
parents: 28965
diff changeset
  1068
    val name = Sign.full_name thy (fst (fst (hd cnames_syn)));
25380
03201004c77e put_inductives: be permissive about multiple versions
wenzelm
parents: 25365
diff changeset
  1069
    val ctxt' = thy
38388
94d5624dd1f7 Named_Target.theory_init
haftmann
parents: 38350
diff changeset
  1070
      |> Named_Target.theory_init
25380
03201004c77e put_inductives: be permissive about multiple versions
wenzelm
parents: 25365
diff changeset
  1071
      |> add_inductive_i flags cnames_syn pnames pre_intros monos |> snd
33671
4b0f2599ed48 modernized structure Local_Theory;
wenzelm
parents: 33670
diff changeset
  1072
      |> Local_Theory.exit;
25380
03201004c77e put_inductives: be permissive about multiple versions
wenzelm
parents: 25365
diff changeset
  1073
    val info = #2 (the_inductive ctxt' name);
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42358
diff changeset
  1074
  in (info, Proof_Context.theory_of ctxt') end;
6424
ceab9e663e08 tuned comments;
wenzelm
parents: 6394
diff changeset
  1075
ceab9e663e08 tuned comments;
wenzelm
parents: 6394
diff changeset
  1076
22789
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1077
(* read off arities of inductive predicates from raw induction rule *)
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1078
fun arities_of induct =
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1079
  map (fn (_ $ t $ u) =>
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1080
      (fst (dest_Const (head_of t)), length (snd (strip_comb u))))
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1081
    (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1082
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1083
(* read off parameters of inductive predicate from raw induction rule *)
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1084
fun params_of induct =
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1085
  let
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
  1086
    val (_ $ t $ u :: _) = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct));
22789
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1087
    val (_, ts) = strip_comb t;
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
  1088
    val (_, us) = strip_comb u;
22789
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1089
  in
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1090
    List.take (ts, length ts - length us)
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1091
  end;
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1092
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1093
val pname_of_intr =
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1094
  concl_of #> HOLogic.dest_Trueprop #> head_of #> dest_Const #> fst;
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1095
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1096
(* partition introduction rules according to predicate name *)
25822
05756950011c Added function partition_rules'.
berghofe
parents: 25510
diff changeset
  1097
fun gen_partition_rules f induct intros =
05756950011c Added function partition_rules'.
berghofe
parents: 25510
diff changeset
  1098
  fold_rev (fn r => AList.map_entry op = (pname_of_intr (f r)) (cons r)) intros
22789
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1099
    (map (rpair [] o fst) (arities_of induct));
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1100
25822
05756950011c Added function partition_rules'.
berghofe
parents: 25510
diff changeset
  1101
val partition_rules = gen_partition_rules I;
05756950011c Added function partition_rules'.
berghofe
parents: 25510
diff changeset
  1102
fun partition_rules' induct = gen_partition_rules fst induct;
05756950011c Added function partition_rules'.
berghofe
parents: 25510
diff changeset
  1103
22789
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1104
fun unpartition_rules intros xs =
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1105
  fold_map (fn r => AList.map_entry_yield op = (pname_of_intr r)
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1106
    (fn x :: xs => (x, xs)) #>> the) intros xs |> fst;
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1107
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1108
(* infer order of variables in intro rules from order of quantifiers in elim rule *)
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1109
fun infer_intro_vars elim arity intros =
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1110
  let
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1111
    val thy = theory_of_thm elim;
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1112
    val _ :: cases = prems_of elim;
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1113
    val used = map (fst o fst) (Term.add_vars (prop_of elim) []);
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1114
    fun mtch (t, u) =
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1115
      let
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1116
        val params = Logic.strip_params t;
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
  1117
        val vars =
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
  1118
          map (Var o apfst (rpair 0))
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
  1119
            (Name.variant_list used (map fst params) ~~ map snd params);
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
  1120
        val ts =
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
  1121
          map (curry subst_bounds (rev vars))
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
  1122
            (List.drop (Logic.strip_assums_hyp t, arity));
22789
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1123
        val us = Logic.strip_imp_prems u;
45647
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
  1124
        val tab =
96af0578571c misc tuning;
wenzelm
parents: 45592
diff changeset
  1125
          fold (Pattern.first_order_match thy) (ts ~~ us) (Vartab.empty, Vartab.empty);
22789
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1126
      in
32035
8e77b6a250d5 tuned/modernized Envir.subst_XXX;
wenzelm
parents: 31986
diff changeset
  1127
        map (Envir.subst_term tab) vars
22789
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1128
      end
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1129
  in
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1130
    map (mtch o apsnd prop_of) (cases ~~ intros)
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1131
  end;
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1132
4d03dc1cad04 Added functions arities_of, params_of, partition_rules, and
berghofe
parents: 22675
diff changeset
  1133
25978
8ba1eba8d058 added theorem group;
wenzelm
parents: 25822
diff changeset
  1134
6437
9bdfe07ba8e9 'HOL/inductive' theory data;
wenzelm
parents: 6430
diff changeset
  1135
(** package setup **)
9bdfe07ba8e9 'HOL/inductive' theory data;
wenzelm
parents: 6430
diff changeset
  1136
9bdfe07ba8e9 'HOL/inductive' theory data;
wenzelm
parents: 6430
diff changeset
  1137
(* setup theory *)
9bdfe07ba8e9 'HOL/inductive' theory data;
wenzelm
parents: 6430
diff changeset
  1138
8634
3f34637cb9c0 use Attrib.add_del_args;
wenzelm
parents: 8433
diff changeset
  1139
val setup =
30722
623d4831c8cf simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents: 30552
diff changeset
  1140
  ind_cases_setup #>
30528
7173bf123335 simplified attribute setup;
wenzelm
parents: 30515
diff changeset
  1141
  Attrib.setup @{binding mono} (Attrib.add_del mono_add mono_del)
7173bf123335 simplified attribute setup;
wenzelm
parents: 30515
diff changeset
  1142
    "declaration of monotonicity rule";
6437
9bdfe07ba8e9 'HOL/inductive' theory data;
wenzelm
parents: 6430
diff changeset
  1143
9bdfe07ba8e9 'HOL/inductive' theory data;
wenzelm
parents: 6430
diff changeset
  1144
9bdfe07ba8e9 'HOL/inductive' theory data;
wenzelm
parents: 6430
diff changeset
  1145
(* outer syntax *)
6424
ceab9e663e08 tuned comments;
wenzelm
parents: 6394
diff changeset
  1146
23762
24eef53a9ad3 Reorganization due to introduction of inductive_set wrapper.
berghofe
parents: 23577
diff changeset
  1147
fun gen_ind_decl mk_def coind =
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36958
diff changeset
  1148
  Parse.fixes -- Parse.for_fixes --
36954
ef698bd61057 prefer structure Parse_Spec;
wenzelm
parents: 36692
diff changeset
  1149
  Scan.optional Parse_Spec.where_alt_specs [] --
46949
94aa7b81bcf6 prefer formally checked @{keyword} parser;
wenzelm
parents: 46947
diff changeset
  1150
  Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse_Spec.xthms1) []
26988
742e26213212 more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents: 26928
diff changeset
  1151
  >> (fn (((preds, params), specs), monos) =>
49324
4f28543ae7fa removed obsolete argument "int" and thus made SML/NJ happy (cf. 03bee3a6a1b7);
wenzelm
parents: 49170
diff changeset
  1152
      (snd o gen_add_inductive mk_def true coind preds params specs monos));
23762
24eef53a9ad3 Reorganization due to introduction of inductive_set wrapper.
berghofe
parents: 23577
diff changeset
  1153
24eef53a9ad3 Reorganization due to introduction of inductive_set wrapper.
berghofe
parents: 23577
diff changeset
  1154
val ind_decl = gen_ind_decl add_ind_def;
6424
ceab9e663e08 tuned comments;
wenzelm
parents: 6394
diff changeset
  1155
33458
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
  1156
val _ =
49324
4f28543ae7fa removed obsolete argument "int" and thus made SML/NJ happy (cf. 03bee3a6a1b7);
wenzelm
parents: 49170
diff changeset
  1157
  Outer_Syntax.local_theory @{command_spec "inductive"} "define inductive predicates"
33458
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
  1158
    (ind_decl false);
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
  1159
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
  1160
val _ =
49324
4f28543ae7fa removed obsolete argument "int" and thus made SML/NJ happy (cf. 03bee3a6a1b7);
wenzelm
parents: 49170
diff changeset
  1161
  Outer_Syntax.local_theory @{command_spec "coinductive"} "define coinductive predicates"
33458
ae1f5d89b082 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents: 33457
diff changeset
  1162
    (ind_decl true);
6723
f342449d73ca outer syntax keyword classification;
wenzelm
parents: 6556
diff changeset
  1163
24867
e5b55d7be9bb simplified interfaces for outer syntax;
wenzelm
parents: 24861
diff changeset
  1164
val _ =
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46949
diff changeset
  1165
  Outer_Syntax.local_theory @{command_spec "inductive_cases"}
50214
67fb9a168d10 tuned command descriptions;
wenzelm
parents: 49324
diff changeset
  1166
    "create simplified instances of elimination rules"
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36958
diff changeset
  1167
    (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_cases));
7107
ce69de572bca inductive_cases(_i): Isar interface to mk_cases;
wenzelm
parents: 7020
diff changeset
  1168
37734
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
  1169
val _ =
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46949
diff changeset
  1170
  Outer_Syntax.local_theory @{command_spec "inductive_simps"}
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46949
diff changeset
  1171
    "create simplification rules for inductive predicates"
37734
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
  1172
    (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_simps));
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents: 37264
diff changeset
  1173
50302
9149a07a6c67 added 'print_inductives' command;
wenzelm
parents: 50301
diff changeset
  1174
val _ =
9149a07a6c67 added 'print_inductives' command;
wenzelm
parents: 50301
diff changeset
  1175
  Outer_Syntax.improper_command @{command_spec "print_inductives"}
9149a07a6c67 added 'print_inductives' command;
wenzelm
parents: 50301
diff changeset
  1176
    "print (co)inductive definitions and monotonicity rules"
51658
21c10672633b discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents: 51584
diff changeset
  1177
    (Scan.succeed (Toplevel.unknown_context o
21c10672633b discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents: 51584
diff changeset
  1178
      Toplevel.keep (print_inductives o Toplevel.context_of)));
50302
9149a07a6c67 added 'print_inductives' command;
wenzelm
parents: 50301
diff changeset
  1179
5094
ddcc3c114a0e New inductive definition package
berghofe
parents:
diff changeset
  1180
end;