Theory Relation_Lib

section ‹ Meta-theory for Relation Library ›

theory Relation_Lib
  imports
    Countable_Set_Extra Positive Infinity Enum_Type Record_Default_Instance Def_Const
    Relation_Extra Partial_Fun Partial_Inj Finite_Fun Finite_Inj Total_Fun List_Extra
    Bounded_List Tabulate_Command
begin 

text ‹ This theory marks the boundary between reusable library utilities and the creation of the
  Z notation. We avoid overriding any HOL syntax up until this point, but we do supply some optional 
  bundles. ›

lemma if_eqE [elim!]: "⟦ (if b then e else f) = v; ⟦ b; e = v ⟧ ⟹ P; ⟦ ¬ b; f = v ⟧ ⟹ P ⟧ ⟹ P"
  by (cases b, auto)

bundle Z_Type_Syntax
begin

type_notation bool ("𝔹")
type_notation nat ("ℕ")
type_notation int ("ℤ")
type_notation rat ("ℚ")
type_notation real ("ℝ")

type_notation set ("ℙ _" [999] 999)

type_notation tfun (infixr "→" 0)

notation Pow ("ℙ")
notation Fpow ("𝔽")

end

class refine =
  fixes ref_by :: "'a ⇒ 'a ⇒ bool" (infix "⊑" 50)
  and sref_by :: "'a ⇒ 'a ⇒ bool"  (infix "⊏" 50)
  assumes ref_by_order: "class.preorder (⊑) (⊏)"

interpretation ref_preorder: preorder "(⊑)" "(⊏)"
  by (fact ref_by_order)

lemma ref_by_trans [trans]: "⟦ P ⊑ Q; Q ⊑ R ⟧ ⟹ P ⊑ R"
  using ref_preorder.dual_order.trans by auto

abbreviation (input) refines (infix "⊒" 50) where "Q ⊒ P ≡ P ⊑ Q"
abbreviation (input) srefines (infix "⊐" 50) where "Q ⊐ P ≡ P ⊏ Q"

instantiation "bool" :: refine
begin

definition "ref_by_bool P Q = (Q ⟶ P)"
definition "sref_by_bool P Q = (¬ Q ∧ P)"

instance by (intro_classes, unfold_locales, auto simp add: ref_by_bool_def sref_by_bool_def)

end

instantiation "fun" :: (type, refine) refine
begin

definition ref_by_fun :: "('a ⇒ 'b) ⇒ ('a ⇒ 'b) ⇒ bool" where "ref_by_fun f g = (∀ x. f(x) ⊑ g(x))"
definition sref_by_fun :: "('a ⇒ 'b) ⇒ ('a ⇒ 'b) ⇒ bool" where "sref_by_fun f g = (f ⊑ g ∧ ¬ (g ⊑ f))"

instance 
  by (intro_classes, unfold_locales)
     (auto simp add: ref_by_fun_def sref_by_fun_def ref_preorder.less_le_not_le intro: ref_preorder.order.trans)
end

end