Added entry for new inductive definition package.
authorberghofe
Wed Jul 11 12:23:34 2007 +0200 (2007-07-11)
changeset 23783e4d514f81d95
parent 23782 4dd0ba632e40
child 23784 75e6b9dd5336
Added entry for new inductive definition package.
NEWS
     1.1 --- a/NEWS	Wed Jul 11 12:01:10 2007 +0200
     1.2 +++ b/NEWS	Wed Jul 11 12:23:34 2007 +0200
     1.3 @@ -541,6 +541,102 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* New package for inductive predicates
     1.8 +
     1.9 +  An n-ary predicate p with m parameters z_1, ..., z_m can now be defined via
    1.10 +
    1.11 +    inductive
    1.12 +      p :: "U_1 => ... => U_m => T_1 => ... => T_n => bool"
    1.13 +      for z_1 :: U_1 and ... and z_n :: U_m
    1.14 +    where
    1.15 +      rule_1: "... ==> p z_1 ... z_m t_1_1 ... t_1_n"
    1.16 +    | ...
    1.17 +
    1.18 +  rather than
    1.19 +
    1.20 +    consts s :: "U_1 => ... => U_m => (T_1 * ... * T_n) set"
    1.21 +
    1.22 +    abbreviation p :: "U_1 => ... => U_m => T_1 => ... => T_n => bool"
    1.23 +    where "p z_1 ... z_m x_1 ... x_n == (x_1, ..., x_n) : s z_1 ... z_m"
    1.24 +
    1.25 +    inductive "s z_1 ... z_m"
    1.26 +    intros
    1.27 +      rule_1: "... ==> (t_1_1, ..., t_1_n) : s z_1 ... z_m"
    1.28 +      ...
    1.29 +
    1.30 +  For backward compatibility, there is a wrapper allowing inductive
    1.31 +  sets to be defined with the new package via
    1.32 +
    1.33 +    inductive_set
    1.34 +      s :: "U_1 => ... => U_m => (T_1 * ... * T_n) set"
    1.35 +      for z_1 :: U_1 and ... and z_n :: U_m
    1.36 +    where
    1.37 +      rule_1: "... ==> (t_1_1, ..., t_1_n) : s z_1 ... z_m"
    1.38 +    | ...
    1.39 +
    1.40 +  or
    1.41 +
    1.42 +    inductive_set
    1.43 +      s :: "U_1 => ... => U_m => (T_1 * ... * T_n) set"
    1.44 +      and p :: "U_1 => ... => U_m => T_1 => ... => T_n => bool"
    1.45 +      for z_1 :: U_1 and ... and z_n :: U_m
    1.46 +    where
    1.47 +      "p z_1 ... z_m x_1 ... x_n == (x_1, ..., x_n) : s z_1 ... z_m"
    1.48 +    | rule_1: "... ==> p z_1 ... z_m t_1_1 ... t_1_n"
    1.49 +    | ...
    1.50 +
    1.51 +  if the additional syntax "p ..." is required.
    1.52 +
    1.53 +  Many examples can be found in the subdirectories Auth, Bali, Induct,
    1.54 +  or MicroJava.
    1.55 +
    1.56 +  INCOMPATIBILITIES:
    1.57 +
    1.58 +  - Since declaration and definition of inductive sets or predicates
    1.59 +    is no longer separated, abbreviations involving the newly introduced
    1.60 +    sets or predicates must be specified together with the introduction
    1.61 +    rules after the "where" keyword (see example above), rather than before
    1.62 +    the actual inductive definition.
    1.63 +
    1.64 +  - The variables in induction and elimination rules are now quantified
    1.65 +    in the order of their occurrence in the introduction rules, rather than
    1.66 +    in alphabetical order. Since this may break some proofs, these proofs
    1.67 +    either have to be repaired, e.g. by reordering the variables
    1.68 +    a_i_1 ... a_i_{k_i} in Isar "case" statements of the form
    1.69 +
    1.70 +      case (rule_i a_i_1 ... a_i_{k_i})
    1.71 +
    1.72 +    or the old order of quantification has to be restored by explicitly adding
    1.73 +    meta-level quantifiers in the introduction rules, i.e.
    1.74 +
    1.75 +      | rule_i: "!!a_i_1 ... a_i_{k_i}. ... ==> p z_1 ... z_m t_i_1 ... t_i_n"
    1.76 +
    1.77 +  - The format of the elimination rules is now
    1.78 +
    1.79 +      p z_1 ... z_m x_1 ... x_n ==>
    1.80 +        (!!a_1_1 ... a_1_{k_1}. x_1 = t_1_1 ==> ... ==> x_n = t_1_n ==> ... ==> P)
    1.81 +        ==> ... ==> P
    1.82 +
    1.83 +    for predicates and
    1.84 +
    1.85 +      (x_1, ..., x_n) : s z_1 ... z_m ==>
    1.86 +        (!!a_1_1 ... a_1_{k_1}. x_1 = t_1_1 ==> ... ==> x_n = t_1_n ==> ... ==> P)
    1.87 +        ==> ... ==> P
    1.88 +
    1.89 +    for sets rather than
    1.90 +
    1.91 +      x : s z_1 ... z_m ==>
    1.92 +        (!!a_1_1 ... a_1_{k_1}. x = (t_1_1, ..., t_1_n) ==> ... ==> P)
    1.93 +        ==> ... ==> P
    1.94 +
    1.95 +    This may require terms in goals to be expanded to n-tuples (e.g. using case_tac
    1.96 +    or simplification with the split_paired_all rule) before the above elimination
    1.97 +    rule is applicable.
    1.98 +
    1.99 +  - The elimination or case analysis rules for (mutually) inductive sets or
   1.100 +    predicates are now called "p_1.cases" ... "p_k.cases". The list of rules
   1.101 +    "p_1_..._p_k.elims" is no longer available.
   1.102 +
   1.103  * Method "metis" proves goals by applying the Metis general-purpose
   1.104  resolution prover.  Examples are in the directory MetisExamples.  See
   1.105  also http://gilith.com/software/metis/