*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Transitivity reasoning and eta-expansion*From*: Peter Lammich <peter.lammich at uni-muenster.de>*Date*: Wed, 14 Nov 2007 14:20:58 +0100*User-agent*: Thunderbird 1.5.0.9 (X11/20060911)

I have the following problem with the transitivity reasoning setup: given some partial order [<\le>] on a function datatype, I want to do transitivity reasoning. So I declare the transitivity lemma as [trans]. The problem is now, that everything works until I have a reflexivity step. In this case, the goal gets eta-expanded at the next 'also', causing the transitivity reasoner to fail. My question is: Is there a workaround, and if the workaround is to add some extra transitivity rules, how do they have to look like ? I added a rule "(%u. a u) = (%u. b u) ==> P b ==> P a", with this rule, the reasoning worked sometimes (of the =-step is the first one in the reasoning chain), but the also command takes some time and produces some very strange output, repeatedly meantioning "unification bound exceeded". Here the example: constdefs ah_leq :: "('m \<Rightarrow> 'm set) \<Rightarrow> ('m \<Rightarrow> 'm set) \<Rightarrow> bool" (infix "[\<le>]" 50) "h1 [\<le>] h2 == \<forall>m. h1 m \<subseteq> h2 m" interpretation ah_leq: partial_order["op [\<le>]"] apply (rule partial_order.intro) apply (unfold ah_leq_def) apply (auto intro!: ext) done declare ah_leq.below.trans[trans] lemma fixes h :: "'m \<Rightarrow> 'm set" shows "False" proof - have "h[\<le>]h" sorry also have "h = h'" sorry also (* Here we have calculation: (\<lambda>u. h' u) [\<le>] (\<lambda>u. h' u)*) have "h' [\<le>] h''" sorry also <- This fails My current workaround is to avoid =-steps, and only use [\<le>] in the reasoning chain. Regards and thanks for any hints, Peter -- Peter Lammich, Institut für Informatik Raum 715, Einsteinstrasse 62, 48149 Münster Mail: peter.lammich at uni-muenster.de Tel: 0251-83-32749 Mobil: 0163-5310380

**Follow-Ups**:**Re: [isabelle] Transitivity reasoning and eta-expansion***From:*Makarius

- Previous by Date: Re: [isabelle] Problems installing Isabelle
- Next by Date: Re: [isabelle] Transitivity reasoning and eta-expansion
- Previous by Thread: [isabelle] TPHOLs 2008 (call for papers)
- Next by Thread: Re: [isabelle] Transitivity reasoning and eta-expansion
- Cl-isabelle-users November 2007 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