[isabelle-dev] NEWS: New package for inductive predicates
Stefan Berghofer
berghofe at in.tum.de
Wed Jul 11 12:38:23 CEST 2007
Dear users,
please find attached a section from our Isabelle NEWS file concerning the new
inductive definition package, which will be part of the forthcoming Isabelle
release.
Greetings,
Stefan
* 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.
--
Dr. Stefan Berghofer E-Mail: berghofe at in.tum.de
Institut fuer Informatik Phone: +49 89 289 17328
Technische Universitaet Muenchen Fax: +49 89 289 17307
Boltzmannstr. 3 Room: 01.11.059
85748 Garching, GERMANY http://www.in.tum.de/~berghofe
More information about the isabelle-dev
mailing list