Theory Derive

chapter ‹Derive›
text ‹
This theory includes the Isabelle/ML code needed for the derivation and exports the two keywords
\texttt{derive\_generic} and \texttt{derive\_generic\_setup}.
›

theory Derive
  imports Main Tagged_Prod_Sum
  keywords "derive_generic" "derive_generic_setup" :: thy_goal
begin

context begin

qualified definition iso :: "('a ⇒ 'b) ⇒ ('b ⇒ 'a) ⇒ bool" where
"iso from to = ((∀ a. to (from a) = a) ∧ (∀ b . from (to b) = b))"

lemma iso_intro: "(⋀a. to (from a) = a) ⟹ (⋀b. from (to b) = b) ⟹ iso from to"
  unfolding iso_def by simp

end

ML_file ‹derive_util.ML›
ML_file ‹derive_laws.ML›
ML_file ‹derive_setup.ML›
ML_file ‹derive.ML›

end