Theory Refine_Imperative_HOL.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 ⟷ x∉set 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_rel→A)" 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