Theory Sepref_Misc
theory Sepref_Misc
imports
"../Refine_Monadic_Add"
PO_Normalizer
"List-Index.List_Index"
"Refine_Imperative_HOL.Named_Theorems_Rev"
"HOL-Eisbach.Eisbach"
begin
hide_const (open) CONSTRAINT
ML ‹
fun SIMPLE_METHOD_NOPARAM' tac = Scan.succeed (fn ctxt => SIMPLE_METHOD' (IF_EXGOAL (tac ctxt)))
fun SIMPLE_METHOD_NOPARAM tac = Scan.succeed (fn ctxt => SIMPLE_METHOD (tac ctxt))
›
lemma not_None_eq2[simp]: "None ≠ x ⟷ (∃y. x = Some y)"
by (cases x) auto
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)"
abbreviation "uncurry10 f ≡ uncurry (uncurry9 f)"
abbreviation "curry10 f ≡ curry (curry9 f)"
abbreviation "uncurry11 f ≡ uncurry (uncurry10 f)"
abbreviation "curry11 f ≡ curry (curry10 f)"
abbreviation "uncurry12 f ≡ uncurry (uncurry11 f)"
abbreviation "curry12 f ≡ curry (curry11 f)"
abbreviation "uncurry13 f ≡ uncurry (uncurry12 f)"
abbreviation "curry13 f ≡ curry (curry12 f)"
abbreviation "uncurry14 f ≡ uncurry (uncurry13 f)"
abbreviation "curry14 f ≡ curry (curry13 f)"
abbreviation "uncurry15 f ≡ uncurry (uncurry14 f)"
abbreviation "curry15 f ≡ curry (curry14 f)"
abbreviation "uncurry16 f ≡ uncurry (uncurry15 f)"
abbreviation "curry16 f ≡ curry (curry15 f)"
abbreviation "uncurry17 f ≡ uncurry (uncurry16 f)"
abbreviation "curry17 f ≡ curry (curry16 f)"
abbreviation "uncurry18 f ≡ uncurry (uncurry17 f)"
abbreviation "curry18 f ≡ curry (curry17 f)"
abbreviation "uncurry19 f ≡ uncurry (uncurry18 f)"
abbreviation "curry19 f ≡ curry (curry18 f)"
abbreviation "uncurry20 f ≡ uncurry (uncurry19 f)"
abbreviation "curry20 f ≡ curry (curry19 f)"
abbreviation comp4 (infixl "oooo" 55) where "f oooo g ≡ λx. f ooo (g x)"
abbreviation comp5 (infixl "ooooo" 55) where "f ooooo g ≡ λx. f oooo (g x)"
abbreviation comp6 (infixl "oooooo" 55) where "f oooooo g ≡ λx. f ooooo (g x)"
abbreviation comp7 (infixl "ooooooo" 55) where "f ooooooo g ≡ λx. f oooooo (g x)"
abbreviation comp8 (infixl "oooooooo" 55) where "f oooooooo g ≡ λx. f ooooooo (g x)"
abbreviation comp9 (infixl "ooooooooo" 55) where "f ooooooooo g ≡ λx. f oooooooo (g x)"
abbreviation comp10 (infixl "oooooooooo" 55) where "f oooooooooo g ≡ λx. f ooooooooo (g x)"
abbreviation comp11 (infixl "o⇩1⇩1" 55) where "f o⇩1⇩1 g ≡ λx. f oooooooooo (g x)"
abbreviation comp12 (infixl "o⇩1⇩2" 55) where "f o⇩1⇩2 g ≡ λx. f o⇩1⇩1 (g x)"
abbreviation comp13 (infixl "o⇩1⇩3" 55) where "f o⇩1⇩3 g ≡ λx. f o⇩1⇩2 (g x)"
abbreviation comp14 (infixl "o⇩1⇩4" 55) where "f o⇩1⇩4 g ≡ λx. f o⇩1⇩3 (g x)"
abbreviation comp15 (infixl "o⇩1⇩5" 55) where "f o⇩1⇩5 g ≡ λx. f o⇩1⇩4 (g x)"
abbreviation comp16 (infixl "o⇩1⇩6" 55) where "f o⇩1⇩6 g ≡ λx. f o⇩1⇩5 (g x)"
abbreviation comp17 (infixl "o⇩1⇩7" 55) where "f o⇩1⇩7 g ≡ λx. f o⇩1⇩6 (g x)"
abbreviation comp18 (infixl "o⇩1⇩8" 55) where "f o⇩1⇩8 g ≡ λx. f o⇩1⇩7 (g x)"
abbreviation comp19 (infixl "o⇩1⇩9" 55) where "f o⇩1⇩9 g ≡ λx. f o⇩1⇩8 (g x)"
abbreviation comp20 (infixl "o⇩2⇩0" 55) where "f o⇩2⇩0 g ≡ λx. f o⇩1⇩9 (g x)"
notation
comp4 (infixl "∘∘∘" 55) and
comp5 (infixl "∘∘∘∘" 55) and
comp6 (infixl "∘∘∘∘∘" 55) and
comp7 (infixl "∘∘∘∘∘∘" 55) and
comp8 (infixl "∘∘∘∘∘∘∘" 55) and
comp9 (infixl "∘∘∘∘∘∘∘∘" 55) and
comp10 (infixl "∘∘∘∘∘∘∘∘∘" 55) and
comp11 (infixl "∘⇩1⇩1" 55) and
comp12 (infixl "∘⇩1⇩2" 55) and
comp13 (infixl "∘⇩1⇩3" 55) and
comp14 (infixl "∘⇩1⇩4" 55) and
comp15 (infixl "∘⇩1⇩5" 55) and
comp16 (infixl "∘⇩1⇩6" 55) and
comp17 (infixl "∘⇩1⇩7" 55) and
comp18 (infixl "∘⇩1⇩8" 55) and
comp19 (infixl "∘⇩1⇩9" 55) and
comp20 (infixl "∘⇩2⇩0" 55)
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