ADTs for KeY #3161

Extension of the KeY grammar to allow the definition of ADTs.

The grammar for ADTs follows the typical defintions in KeY. ADTs are defined within a \datatypes { ... } block, and are translated onto the existing infrastructure (Sorts, Functions, Taclets). The grammar is as follows:

\datatypes { <name> := <constructor> | ... | <constructor>; ... }

where constructor is a function definition <cname>( <sort> <argName>, ...).

Currently, three taclets are generated for each datatype definiton:

1. Axiom taclets that adds the induction as an axiom on the sequence

$$ \frac{ (\forall a \in ADT.~ \phi) \leftrightarrow \phi[a/c_1] \wedge \ldots \wedge \phi[a/c_n] \Longrightarrow }{ \forall a \in ADT.~ \phi[a] } $$

1. Induction taclets for proving a sentence for all ADTs.

$$ \frac{ \begin{matrix} \forall a \in ADT; \phi \Longrightarrow \ \Longrightarrow \phi[a/c_1] \ \Longrightarrow \ldots \ \Longrightarrow phi[a/c_n] \end{matrix} }{ \Longrightarrow \forall a \in ADT.~ \phi[a] } $$

A direct consequence of the induction formula in (1).

1. A case distinction taclet

This is a direct consequence of the disjunction $x = c_1 \vee\ldots\vee x = c_n$ resulting from the construction principles of ADTs. This allows us to make a case distinction about the various constructors. Note, the constructor parameters are need to existential bounded.

$$ \frac{ \begin{matrix} x = c_1 \Longrightarrow \ \ldots \Longrightarrow \ x = c_n \Longrightarrow \end{matrix} }{ x : ADT ~ \text{(anywhere)} } $$

Example

Input \datatypes { MyList = MNil | MCons(any head, MyList tail); }

Generated Taclets

``` MyList_Axiom { \schemaVar \formula phi; \schemaVar \variables MyList x;

\find(\forall x; phi)
\varcond(\notFreeIn(x, phi))
\add(
         \forall x; phi
     <->   {\subst x;MNil}phi
         & \forall tail; \forall head; ({\subst x;tail}phi -> {\subst x;MCons(head, tail)}phi)
    ==>
  )
\displayname "Axiom for MyList"

}

MyList_Ind { \schemaVar \formula phi;

   "MNil":
       \add(==> {\subst x;MNil}phi);
   "MCons(anyhead,MyListtail)":
       \add(
           ==>
            \forall tail; \forall head; ({\subst x;tail}phi -> {\subst x;MCons(head, tail)}phi)
         );
   "Use case of MyList":
       \add(\forall x; phi ==>)
   \displayname "Induction for MyList"
 }

MyList_ctor_split { \schemaVar \term MyList var; \schemaVar \skolemTerm any head; \schemaVar \skolemTerm MyList tail;

      \find(var)
      \sameUpdateLevel
      "#var = MNil":
          \add(var = MNil ==>);
      "#var = MCons":
          \add(var = MCons(head, tail) ==>)
      \displayname "case distinction of MyList"
    }

```

Current Problems / TODO

• [x] Matching/Application of taclets not working
• [ ] Test cases