*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] partial functions: is f_rel too weak too?*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Mon, 29 Feb 2016 07:56:52 +0100*In-reply-to*: <F68606B8-9EA6-4947-AC0C-F38CF60807EF@gmail.com>*References*: <F68606B8-9EA6-4947-AC0C-F38CF60807EF@gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:38.0) Gecko/20100101 Thunderbird/38.6.0

Tobias On 29/02/2016 07:33, Peter Gammie wrote:

Hi, Consider this function and proof attempt: function f :: "'a::finite set \<Rightarrow> 'a set \<Rightarrow> 'a list set" where "f C B = (if B = {} then {[]} else if B \<subseteq> C then {c # cs |c cs. c \<in> B \<and> cs \<in> f {} (B - {c})} else {})" by pat_completeness auto lemma f_termination: shows "f_dom (C, B)" proof(induct t \<equiv> "card B" arbitrary: B C) case (Suc i B C) then show ?case apply - apply (rule accpI) apply (erule f_rel.cases) Intuitively this function terminates because we keep removing elements of B from B. However f_rel does not seem to note that c is drawn from B in the recursion. (domintros is too weak, as is apparently well-known.) Any tips? In my use case f is actually only partially defined. cheers, peter

**Attachment:
smime.p7s**

**Follow-Ups**:**Re: [isabelle] partial functions: is f_rel too weak too?***From:*Andreas Lochbihler

**References**:**[isabelle] partial functions: is f_rel too weak too?***From:*Peter Gammie

- Previous by Date: [isabelle] partial functions: is f_rel too weak too?
- Next by Date: Re: [isabelle] partial functions: is f_rel too weak too?
- Previous by Thread: [isabelle] partial functions: is f_rel too weak too?
- Next by Thread: Re: [isabelle] partial functions: is f_rel too weak too?
- Cl-isabelle-users February 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list