author | berghofe |

Wed Jul 11 12:23:34 2007 +0200 (2007-07-11) | |

changeset 23783 | e4d514f81d95 |

parent 23782 | 4dd0ba632e40 |

child 23784 | 75e6b9dd5336 |

Added entry for new inductive definition package.

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/