[isabelle] size_changes raises Option and Bind



In Isabelle 2011-1, size_change raises the exception Option (line 81 in general/basics.ML) and Bind (line 277 of termination.ML) for the following function definitions. The NOT operator seems to cause the trouble, because size_change (and lexicographic_order) work perfectly well when I unfold NOT i = -i - 1.

This either seems like a bug in termination or some bad setup for NOT.

theory Scratch imports "~~/src/HOL/Word/Bit_Int" begin

function bits :: "int => nat"
where
  "bits i =
  (if i < 0 then bits (NOT i)
   else if i = 0 then 0
   else bits (i div 2) + 1)"
by(pat_completeness) auto
termination apply(size_change) (* raises Option *)

function bits :: "int => nat"
where
  "bits i = (if i < 0 then bits (NOT i) else 0)"
by(pat_completeness) auto
termination apply(size_change) (* raises Bind *)

Andreas

--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft





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