Theory Impossibility

subsection ‹Impossibility of hiding sort constraints›
text_raw ‹\label{sec:impossibility}›

text ‹Coauthor of this section: Florian Haftmann›

theory Impossibility
imports Main
begin

axiomatization of_prop :: "prop ⇒ bool" where
of_prop_Trueprop [simp]: "of_prop (Trueprop P) ⟷ P" and
Trueprop_of_prop [simp]: "Trueprop (of_prop Q) ≡ PROP Q"

text ‹A type satisfies the certificate if there is an instance of the class.›

definition is_sg :: "'a itself ⇒ bool" where
"is_sg TYPE('a) = of_prop OFCLASS('a, semigroup_add_class)"

text ‹We trick the parser into ignoring the sort constraint of @{const plus}.›

setup ‹Sign.add_const_constraint (@{const_name plus}, SOME @{typ "'a::{} => 'a ⇒ 'a"})›

definition sg :: "('a ⇒ 'a ⇒ 'a) ⇒ bool" where
"sg plus ⟷ plus = Groups.plus ∧ is_sg TYPE('a)" for plus

text ‹Attempt: Define a type that contains all legal @{const plus} functions.›

typedef (overloaded) 'a Sg = "Collect sg :: ('a ⇒ 'a ⇒ 'a) set"
  morphisms the_plus Sg
  unfolding sg_def[abs_def]
  apply (simp add: is_sg_def)

text ‹We need to prove @{term "OFCLASS('a, semigroup_add_class)"} for arbitrary @{typ 'a}, which is
impossible.›

oops

end