[isabelle] Problems with cong-rules for parser



Dear all,

we currently have problems setting up the right cong-rules for our
parser such termination is provable.

Here, the major problems are parsers which call themselves twice in a row.

Consider the following theory:

theory Test imports Main
begin

types
  ('t, 'a) parser = "'t list => string + ('a x 't list)"

take a token list and produce a string error-message or a pair of result and remaining token list

(state-monad with errors)

now we can define the standard return and bind operations

abbreviation
  return :: "'a => ('t, 'a)parser"
where
  "return x = (%ts. Inr (x, ts))"

definition
bind :: "('t, 'a) parser => ('a => ('t, 'b) parser) => ('t, 'b) parser"
where
  "bind m f ts = (case m ts of
      Inl e => Inl e
    | Inr (x,ts') => f x ts')"

consuming one character

fun consume :: "('t,'t)parser"
where "consume [] = Inl ''error''"
   |  "consume (t # ts) = Inr (t, ts)"

now, here is the difficult function:

function foo :: "('t, 't list)parser"
where "foo ts = (bind consume
                   (% t. bind foo
                   (% us. bind foo
                   (% vs. return (t # us @ vs))))) ts"
by pat_completeness auto
termination
proof
(*  impossible, since there is no link between input ts and the list
    of tokens that is used for recursive foo-calls *)
oops

so, let us add some congruence rule:

lemma bind_cong[fundef_cong]:
  fixes m1 :: "('t,'a)parser"
assumes "m1 ts1 = m2 ts1" and "!! y ts. m1 ts1 = Inr (y,ts) ==> f1 y ts = f2 y ts" and "ts1 = ts2"
  shows "((bind m1 f1) ts1) = ((bind m2 f2) ts2)"
using assms unfolding bind_def by (cases "m1 ts1", auto)

now, indeed a simplied version of foo can be proven to be terminating (if there is only one recursive call)

function foo' :: "('t, 't list)parser"
where "foo' ts = (bind consume
                   (% t. bind foo'
                   (% vs. return (t # vs)))) ts"
by pat_completeness auto
termination by ... tedious reasoning

but, if we want to have the full version which two recursive calls, then not even the function
definition is accepted:

function foo'' :: "('t, 't list)parser"
where "foo'' ts = (bind consume
                   (% t. bind foo''
                   (% us. bind foo''
                   (% vs. return (t # us @ vs))))) ts"
(*
exception THM 0 raised (line 709 of "thm.ML"): implies_elim: major premise
*)

Does someone have an idea, what went wrong in this case?

Best regards,
René

PS: The small theory file is attached.

Attachment: Test.thy
Description: Binary data




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.