Theory Sepref_Misc

theory Sepref_Misc
imports 
  Refine_Monadic.Refine_Monadic
  PO_Normalizer
  "List-Index.List_Index"
  Separation_Logic_Imperative_HOL.Sep_Main
  Named_Theorems_Rev
  "HOL-Eisbach.Eisbach"
  Separation_Logic_Imperative_HOL.Array_Blit
begin

  hide_const (open) CONSTRAINT

  (* Additions for List_Index *)  
  lemma index_of_last_distinct[simp]: 
    "distinct l  index l (last l) = length l - 1"  
    apply (cases l rule: rev_cases)
    apply (auto simp: index_append)
    done

  lemma index_eqlen_conv[simp]: "index l x = length l  xset l"
    by (auto simp: index_size_conv)


  subsection ‹Iterated Curry and Uncurry›    


  text ‹Uncurry0›  
  definition "uncurry0 c  λ_::unit. c"
  definition curry0 :: "(unit  'a)  'a" where "curry0 f = f ()"
  lemma uncurry0_apply[simp]: "uncurry0 c x = c" by (simp add: uncurry0_def)

  lemma curry_uncurry0_id[simp]: "curry0 (uncurry0 f) = f" by (simp add: curry0_def)
  lemma uncurry_curry0_id[simp]: "uncurry0 (curry0 g) = g" by (auto simp: curry0_def)
  lemma param_uncurry0[param]: "(uncurry0,uncurry0)  A  (unit_relA)" by auto
    
  text ‹Abbreviations for higher-order uncurries›    
  abbreviation "uncurry2 f  uncurry (uncurry f)"
  abbreviation "curry2 f  curry (curry f)"
  abbreviation "uncurry3 f  uncurry (uncurry2 f)"
  abbreviation "curry3 f  curry (curry2 f)"
  abbreviation "uncurry4 f  uncurry (uncurry3 f)"
  abbreviation "curry4 f  curry (curry3 f)"
  abbreviation "uncurry5 f  uncurry (uncurry4 f)"
  abbreviation "curry5 f  curry (curry4 f)"
  abbreviation "uncurry6 f  uncurry (uncurry5 f)"
  abbreviation "curry6 f  curry (curry5 f)"
  abbreviation "uncurry7 f  uncurry (uncurry6 f)"
  abbreviation "curry7 f  curry (curry6 f)"
  abbreviation "uncurry8 f  uncurry (uncurry7 f)"
  abbreviation "curry8 f  curry (curry7 f)"
  abbreviation "uncurry9 f  uncurry (uncurry8 f)"
  abbreviation "curry9 f  curry (curry8 f)"

    
    
  lemma fold_partial_uncurry: "uncurry (λ(ps, cf). f ps cf) = uncurry2 f" by auto

  lemma curry_shl: 
    "g f. (g  curry f)  (uncurry g  f)"
    "g f. (g  curry0 f)  (uncurry0 g  f)"
    by (atomize (full); auto)+
  
  lemma curry_shr: 
    "f g. (curry f  g)  (f  uncurry g)"
    "f g. (curry0 f  g)  (f  uncurry0 g)"
    by (atomize (full); auto)+
  
  lemmas uncurry_shl = curry_shr[symmetric]  
  lemmas uncurry_shr = curry_shl[symmetric]  
  
end