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)