[isabelle] Transitivity reasoning and eta-expansion



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







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