Re: [isabelle] Exception Chr raised while processing "fun" (Isabelle 2016)



Hi Eugene,

The problem seems to be with lexicographic_order (it probably tries to generate some error or info message in which a conversion to characters fails). If you use size_change in the termination proof, it works:

    function (sequential) F :: "'a term â int"
    where "F (T (T (U, b), c)) = 1 + F (T (U, T (b, c)))"
        | "F (T (T (a, b), c)) = 1 + F a + F (T (b, c))"
        | "F (T (U, b)) = 1 + F b"
        | "F (T (a, U)) = 1 + F a"
        | "F (T (a, b)) = (F a) + (F b)"
        | "F a = undefined"
      by pat_completeness auto
    termination by size_change

Best,
Andreas

On 17/10/16 12:17, Eugene W. Stark wrote:
Any ideas about the following?

theory Barf
imports Main
begin

    datatype 't "term" =
      Const 't
    | U
    | T "'t term * 't term"
    | C "'t term * 't term"
    | L "'t term"
    | L' "'t term"
    | R "'t term"
    | R' "'t term"
    | A "'t term * 't term * 't term"
    | A' "'t term * 't term * 't term"

    fun F :: "'a term â int"
    where "F (T (T (U, b), c)) = 1 + F (T (U, T (b, c)))"
        | "F (T (T (a, b), c)) = 1 + F a + F (T (b, c))"
        | "F (T (U, b)) = 1 + F b"
        | "F (T (a, U)) = 1 + F a"
        | "F (T (a, b)) = (F a) + (F b)"
        | "F a = undefined"

    (* exception Chr raised (line 268 of "./basis/String.sml") *)
end





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