# HG changeset patch
# User berghofe
# Date 1184149414 -7200
# Node ID e4d514f81d95cc5615fbbe06cdf05c87ad041d97
# Parent  4dd0ba632e404874066b2f335e7a331e59c12555
Added entry for new inductive definition package.

diff -r 4dd0ba632e40 -r e4d514f81d95 NEWS
--- a/NEWS	Wed Jul 11 12:01:10 2007 +0200
+++ b/NEWS	Wed Jul 11 12:23:34 2007 +0200
@@ -541,6 +541,102 @@
 
 *** HOL ***
 
+* New package for inductive predicates
+
+  An n-ary predicate p with m parameters z_1, ..., z_m can now be defined via
+
+    inductive
+      p :: "U_1 => ... => U_m => T_1 => ... => T_n => bool"
+      for z_1 :: U_1 and ... and z_n :: U_m
+    where
+      rule_1: "... ==> p z_1 ... z_m t_1_1 ... t_1_n"
+    | ...
+
+  rather than
+
+    consts s :: "U_1 => ... => U_m => (T_1 * ... * T_n) set"
+
+    abbreviation p :: "U_1 => ... => U_m => T_1 => ... => T_n => bool"
+    where "p z_1 ... z_m x_1 ... x_n == (x_1, ..., x_n) : s z_1 ... z_m"
+
+    inductive "s z_1 ... z_m"
+    intros
+      rule_1: "... ==> (t_1_1, ..., t_1_n) : s z_1 ... z_m"
+      ...
+
+  For backward compatibility, there is a wrapper allowing inductive
+  sets to be defined with the new package via
+
+    inductive_set
+      s :: "U_1 => ... => U_m => (T_1 * ... * T_n) set"
+      for z_1 :: U_1 and ... and z_n :: U_m
+    where
+      rule_1: "... ==> (t_1_1, ..., t_1_n) : s z_1 ... z_m"
+    | ...
+
+  or
+
+    inductive_set
+      s :: "U_1 => ... => U_m => (T_1 * ... * T_n) set"
+      and p :: "U_1 => ... => U_m => T_1 => ... => T_n => bool"
+      for z_1 :: U_1 and ... and z_n :: U_m
+    where
+      "p z_1 ... z_m x_1 ... x_n == (x_1, ..., x_n) : s z_1 ... z_m"
+    | rule_1: "... ==> p z_1 ... z_m t_1_1 ... t_1_n"
+    | ...
+
+  if the additional syntax "p ..." is required.
+
+  Many examples can be found in the subdirectories Auth, Bali, Induct,
+  or MicroJava.
+
+  INCOMPATIBILITIES:
+
+  - Since declaration and definition of inductive sets or predicates
+    is no longer separated, abbreviations involving the newly introduced
+    sets or predicates must be specified together with the introduction
+    rules after the "where" keyword (see example above), rather than before
+    the actual inductive definition.
+
+  - The variables in induction and elimination rules are now quantified
+    in the order of their occurrence in the introduction rules, rather than
+    in alphabetical order. Since this may break some proofs, these proofs
+    either have to be repaired, e.g. by reordering the variables
+    a_i_1 ... a_i_{k_i} in Isar "case" statements of the form
+
+      case (rule_i a_i_1 ... a_i_{k_i})
+
+    or the old order of quantification has to be restored by explicitly adding
+    meta-level quantifiers in the introduction rules, i.e.
+
+      | rule_i: "!!a_i_1 ... a_i_{k_i}. ... ==> p z_1 ... z_m t_i_1 ... t_i_n"
+
+  - The format of the elimination rules is now
+
+      p z_1 ... z_m x_1 ... x_n ==>
+        (!!a_1_1 ... a_1_{k_1}. x_1 = t_1_1 ==> ... ==> x_n = t_1_n ==> ... ==> P)
+        ==> ... ==> P
+
+    for predicates and
+
+      (x_1, ..., x_n) : s z_1 ... z_m ==>
+        (!!a_1_1 ... a_1_{k_1}. x_1 = t_1_1 ==> ... ==> x_n = t_1_n ==> ... ==> P)
+        ==> ... ==> P
+
+    for sets rather than
+
+      x : s z_1 ... z_m ==>
+        (!!a_1_1 ... a_1_{k_1}. x = (t_1_1, ..., t_1_n) ==> ... ==> P)
+        ==> ... ==> P
+
+    This may require terms in goals to be expanded to n-tuples (e.g. using case_tac
+    or simplification with the split_paired_all rule) before the above elimination
+    rule is applicable.
+
+  - The elimination or case analysis rules for (mutually) inductive sets or
+    predicates are now called "p_1.cases" ... "p_k.cases". The list of rules
+    "p_1_..._p_k.elims" is no longer available.
+
 * Method "metis" proves goals by applying the Metis general-purpose
 resolution prover.  Examples are in the directory MetisExamples.  See
 also http://gilith.com/software/metis/