[isabelle] domintros generated by Function too weak



Hi,

I have some more issues with the Function package, this time with the
domintros option. Consider this (not very useful) example:

______________________________________
function (sequential,domintros) f where
   "f v b = (if v = 1 then f 0 b else f (Suc v) b)"
apply pat_completeness
apply auto
done
______________________________________

The generated domintros rule is too weak:
______________________________________
thm f.domintros(1)[no_vars]
⟦f_dom (0, b); v ≠ Suc 0 ⟹ f_dom (Suc v, b)⟧ ⟹ f_dom (v, b)
______________________________________


Note that the f_rel intros are correct:
thm f_rel.intros[no_vars]
______________________________________
v = 1 ⟹ f_rel (0, b) (v, b)
v ≠ 1 ⟹ f_rel (Suc v, b) (v, b)
______________________________________

I can work around the issue by wrapping the condition of the if
statement in the identity function and removing it temporarily from the
simpset:
______________________________________
declare id_apply[simp del]
function (sequential,domintros) f' where
   "f' v b = (if id (v = 0) then f' 0 b else f' (Suc v) b)"
apply pat_completeness
apply auto
done
declare id_apply[simp]
______________________________________

yields
______________________________________
thm f'.domintros(1)[no_vars]
⟦id (v = 0) ⟹ f'_dom (0, b); ¬ id (v = 0) ⟹ f'_dom (Suc v, b)⟧
⟹ f'_dom (v, b)
______________________________________


A probably related problem is that
______________________________________
function (sequential,domintros) f where
   "f l = (case l of [a,b,0] ⇒ f [a+b])"
apply pat_completeness
apply auto
done
______________________________________

gives the domintro rule
______________________________________
thm f.domintros(1)[no_vars]
(⋀a aa. f_dom [a + aa]) ⟹ f_dom l  [?]
______________________________________

where I am missing the connection between l and a,aa.


I’m not sure if this is a bug in in the Function package, or an
unavoidable limitation.

Thanks,
Joachim

-- 
Joachim Breitner
  e-Mail: mail at joachim-breitner.de
  Homepage: http://www.joachim-breitner.de
  ICQ#: 74513189
  Jabber-ID: nomeata at joachim-breitner.de

Attachment: signature.asc
Description: This is a digitally signed message part



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