[isabelle-dev] recursive datatype measure

[Chris Capel]

OK, here it is:

datatype prod =
    PTrm nat --{*token*}
  | Prod "prod list list"

primrec powerlist :: "'a list => 'a list list" where
  "powerlist [] = []" |
  "powerlist (x # xs) = (x # xs) # powerlist xs"

lemma [simp]: "length (powerlist x) = length x"
by (induct x) auto

function
    parse_len :: "prod => nat list => int" where

   "parse_len (PTrm tok) toks = (if ((hd toks) = tok) then 1 else -1)"
 | "parse_len (Prod pl) toks =
      last (sort (map (%p. foldl (% (len::int) (p, l).
                                    if len = -1 then -1
                                    else len + parse_len p l)
                                 0 (zip p (powerlist toks)))
                  pl))"
by pat_completeness auto
termination
apply (relation "measure (%(p, l). size p)", auto)
apply (rename_tac pll toks pl len p l)
--{*apply (rule local.termination, auto)*}



Thanks,

Chris

On Mon, Feb 16, 2009 at 14:44, Alexander Krauss <krauss at in.tum.de> wrote:
> Dear Chris,
>
> At first glance, this looks provable to me...
>
> Can you give us the concrete function definition?
>
> Note that for "xs :: T list" there is a difference between "size xs" (length
> of the list) and "list_size size xs" (sum of sizes of elements).
>
> Chris Capel wrote:
>>
>> I have a recursive datatype,
>>
>> datatype prod =
>>    PTrm nat
>>  | Prod "prod list list"
>>
>> and I've defined a recursive function in it using foldl. I'm trying to
>> prove termination, but I'm not sure how. I think my key difficulty
>> might be that I need to prove that p :: prod : set (pl :: prod) ==>
>> size p < size pl. (This is also where the automatic termination proof
>> fails.) Can this be done? I think this is equivalent to the question
>> of whether circular structures can be created out of datatypes in
>> Isabelle.
>
> This has nothing to do with circular structures, which are not possible with
> inductive datatypes.
>
>> More details: after I apply
>>
>> termination
>> apply (rule local.termination, auto)
>>
>> I get the following subgoal:
>>
>> goal (1 subgoal):
>>  1. !!(pll::prod list list) (toks::nat list) (pl::prod list) (len::int)
>>       (p::prod) l::nat list.
>>       [| pl : set pll; (p, l) : set (zip pl toks); len ~= (-1::int) |]
>>       ==> ?f7 (p, l) < ?f7 (prod.Prod pll, toks)
>> variables:
>>  ?f7 :: prod * nat list => nat
>>
>> Applying instead relation "measure (%(p, l). size p)" yields the
>> conclusion (with the same assumptions), "size p < Suc (list_size
>> (list_size size) pll)".
>>
>> Chris Capel
>
> Alex
>



-- 
"What is it like to be a bat? What is it like to bat a bee? What is it
like to be a bee being batted? What is it like to be a batted bee?"
-- The Mind's I (Hofstadter, Dennet)