*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Simplifying split lambda terms and (maybe) a bug in the "subst" method*From*: Rafal Kolanski <rafalk at cse.unsw.edu.au>*Date*: Wed, 23 Apr 2008 03:03:27 +1000*User-agent*: Thunderbird 2.0.0.12 (X11/20080227)

Dear Isabelle Wizards,

((\<lambda>(h, r). (ass1 (v r) (p r)) (h, r)) &&& (\<lambda>(h, r). (ass2 (p r)) (h, r)) &&& P) (h, r)

*** exception TYPE raised: Variable "?Q" has two distinct types *** At command "apply"

Sincerely, Rafal Kolanski.

theory Temp imports WordMain begin text {* As our state, we essentially work on a "(pptr \<times> vptr) \<rightharpoonup> val" heap but have an extra pptr parameter *} types vptr = "32 word" pptr = "32 word" val = "32 word" ('p,'v,'val) map_assert = "((('p \<times> 'v) \<rightharpoonup> 'val) \<times> 'p) \<Rightarrow> bool" heap_assert = "(pptr, vptr, val) map_assert" text {* Our assertion combining operator, sep_conj only plays around with the heap, passing on the extra pptr unchanged. *} constdefs sep_conj :: "('a,'b,'c) map_assert \<Rightarrow> ('a,'b,'c) map_assert \<Rightarrow> ('a,'b,'c) map_assert" (infixr "&&&" 35) "P &&& Q \<equiv> \<lambda>(h,r). \<exists>h0 h1. dom h0 \<inter> dom h1 = {} \<and> h = h0 ++ h1 \<and> P (h0,r) \<and> Q (h1,r)" text {* We can have assertions like "something maps to something", "something maps to anything", etc *} consts ass1 :: "vptr \<Rightarrow> pptr \<Rightarrow> heap_assert" ass2 :: "pptr \<Rightarrow> heap_assert" ass3 :: "vptr \<Rightarrow> heap_assert" text {* Where it becomes annoying is in a larger lemma, sometimes the arguments to ass1/2/3 may depend on the extra pptr parameter, giving us interesting lambda mangling (see example_problem). Since the root is always the same within a larger assertion, I want to dig it out of the lambda construction. For example_problem, it would be like so: *} lemma example_problem_descramble: "((\<lambda>(h, r). (ass1 (v r) (p r)) (h, r)) &&& (\<lambda>(h, r). (ass2 (p r)) (h, r)) &&& P) (h, r) = (ass1 (v r) (p r) &&& ass2 (p r) &&& P) (h, r)" by (clarsimp simp: sep_conj_def) text {* This is specific to example_problem though and won't work as part of a larger assertion anyway (depends on the external (h,r)). Here are what I believe to be more general cases: *} lemma sep_conj_pop_r_left: "((\<lambda>(h,r). (P r) (h,r)) &&& Q) = (\<lambda>(h,r). (P r &&& Q) (h,r))" by (clarsimp simp: sep_conj_def) lemma sep_conj_pop_r_left': "((\<lambda>(h,r). (P r) (h,r)) &&& (\<lambda>(h,r). (Q r) (h,r))) = (\<lambda>(h,r). (P r &&& Q r) (h,r))" by (clarsimp simp: sep_conj_def) lemma sep_conj_pop_r_right: "(P &&& (\<lambda>(h,r). (Q r) (h,r))) = (\<lambda>(h,r). (P &&& Q r) (h,r))" by (clarsimp simp: sep_conj_def) text {* Unfortunately, I cannot get these cases to substitute properly, and below I manage to get: *** exception TYPE raised: Variable "?Q" has two distinct types *** At command "apply" Which I believe should not happen. *} lemma example_problem: " \<And>h r. \<lbrakk>((\<lambda>(h, r). (ass1 (v r) (p r)) (h, r)) &&& (\<lambda>(h, r). (ass2 (p r)) (h, r)) &&& P) (h, r) ; (ass3 (v r)) (h, r)\<rbrakk> \<Longrightarrow> BLAH" apply (subst (asm) sep_conj_pop_r_left)

**Follow-Ups**:**Re: [isabelle] Simplifying split lambda terms and (maybe) a bug in the "subst" method***From:*Lawrence Paulson

- Previous by Date: [isabelle] 2nd CFP: Proof-Carrying Code workshop PCC 2008 (Extended deadline)
- Next by Date: [isabelle] TPHOLs'2009 Host Selection
- Previous by Thread: [isabelle] 2nd CFP: Proof-Carrying Code workshop PCC 2008 (Extended deadline)
- Next by Thread: Re: [isabelle] Simplifying split lambda terms and (maybe) a bug in the "subst" method
- Cl-isabelle-users April 2008 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