[isabelle-dev] functions over abstract data

[Christian Sternagel]

Dear Alex and all,

once again I started to transform a rather adhoc parser datatype (in 
IsaFoR) into some (I think) nicer variant using abstract datatypes with 
invariants. After tinkering around for several days (where everything 
worked out nicely) I hit a wall, and also remembered that I already did 
so some years ago, when I wanted to do the same thing. Only this time, 
instead of giving up, I started to think about destructing the wall (not 
with my head though ... well ... in a way ;)).

Let me first state my "problem" (parsers are only a special instance). 
Suppose you have an abstract datatype with invariant like

   typedef T = "{x. Inv x}"

with an "Abs"/"Rep" pair and the invariant "Inv".

---------------------------------------------------------
*Example:* Parsers:

   ('a, 'b) raw_parser = 'a list => string + ('b * 'a list)

   leq p <-> (ALL ts x ts'.
     p ts = Inr (x, ts') --> length ts' <= length ts)

   typedef ('a, 'b) parser = "{p::('a, 'b) raw_parser. leq p}"
     morphisms run Parser
---------------------------------------------------------

When defining a function "f", whose result type is "T", it might be 
necessary to "peek under the hood" in order to show termination. When 
doing this manually, we destroy the abstraction and always have to 
reason about the raw-level and even worse, also all the existing 
constants with result type T have to be deconstructed in the definition.

---------------------------------------------------------
*Example:* Suppose we already have do-notation for parsers
(i.e., bind), monadic return, op <|> (for alternatives),
and a parser "just" that parses just the given string. One
simple parser that could be constructed is:

   par =
     (do { just "(", par; just ")"; return () }) <|>
     return ()

However, without lifting the abstraction, we have no handle
on termination. Resulting in something like

   par_aux ts = run
     ((do { just "(", Parser par_aux; just ")"; return () }) <|>
       return ())
     ts

   par = Parser par_aux

where I have to unfold all the abstract definitions in the
body of "par_aux" in order to prove termination and the
termination proof gets really messy (in fact I did not
succeed at all.)
---------------------------------------------------------

Here comes my suggestion (until now I only did a manual --
i.e., all proofs and auxiliary definitions by hand --
case-study for the "par" parser, to check feasibility).

(This only makes sense when "Rep" returns something
of function type.)

Function specifications may be given parameters "Abs", "Rep",
"Inv" (most likely corresponding to some abstract datatype
with invariant) with lemmas:

   Abs_inverse: "Inv x ==> Rep (Abs x) = x"
   Rep_eqI: "(!!x. Rep f x = Rep g x) ==> f = g"

Then when the user writes something like

   function (abstract Abs Rep Inv)
     f :: "T"
   where
     "f = F f"

this is internally replaced by

   "Rep f x = Rep (F f) x"

for the inductive definition of the function graph G_f, we replace the 
existing (see Alex' thesis, page 17) introduction rules (for simplicity 
just using a single recursive call):

   (Gamma ==> (r[h/f], h(r[h/f]) : G_f) ==> (x, F h x) : G_f

by

   (Gamma ==> (r[h/f], Rep h (r[h/f])) : G_f ==> (x, Rep (F h) x) : G_f

(So we more or less consider "Rep f" instead of just "f" to be the newly
defined function for the purpose of internal constructions.)

The introduction rules for the domain are modified similarly. The 
internal definition of the function is now two-fold:

   "f' = (%x. THE y. par_graph x y)"
   "f = Abs f'"

Furthermore, an additional lemma (besides the usual "x : dom_f ==> EX!y. 
(x, y) : G_f") is needed:

   "Inv f' ==> x : dom_f ==> (x, Rep (F f) x) : G_f"

(which is proved similarly to the existence part of the standard lemma 
and where "Inv f'" is needed to obtain, together with "Abs_inverse", 
"Rep f = f'".) Furthermore the usual psimps get an additional assumption:

   psimps: "Inv f' ==> x : dom_f ==> Rep f x = Rep (F f) x"

Then the termination proof involves two steps:
   - show "!!x. x : dom_f", and
   - show "(!!x. x : dom_f) ==> inv f'"
(which is both trivial for the "par" parser). Then we can derive "Rep f 
x = Rep (F f) x", which together with "Rep_eqI" yields the desired "f = 
F f".

Remark: ideally this should also handle additional parameters of "f" 
(which are outside of the abstraction). Maybe something like:

   "f x = F f x"

turned into

   "Rep (f x) y = Rep (F f x) y"

with

   "f' = (%x y. THE z. ((x, y), z) : G_f"
   "f = (%x. Abs (f' x))

Any comments? Would anybody else find this useful?

cheers

chris

PS: I started to dive into the function package. My first hurdle is that 
for "f" not of function type (as in "par"), no recursive calls are 
generated, since "Function_Ctx_Tree.mk_tree" says that "No cong rules 
could be found".