# 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
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