Theory IRGraphSort

section ‹Graph Type Class Instantiations›

theory
  IRGraphSort
imports
  Graph.IRGraph
begin

text ‹
An @{typ IRGraph} can be treated as an instantiation of
various type classes such as the equal type class.

Here we define the instantiations for all type classes
of which @{typ IRGraph} belongs.
›


subsection ‹Equal Instance›
text ‹
The following is an incorrect definition of equality
which is used to allow code generation of the Canonicalization
phase. Without this we have to use the values command to generate
all possible results of the canonicalization phase.

Note that we should be able to find a correct equality definition
in terms of the ids, kind, and stamp function. However, we are
yet to find a satisfactory definition as yet.
›
(* Code generation issues
definition IRGraph_equal :: "IRGraph ⇒ IRGraph ⇒ bool" where
  "IRGraph_equal g1 g2 = (as_list g1 = as_list g2)"
*)
definition IRGraph_equal :: "IRGraph ⇒ IRGraph ⇒ bool" where
  "IRGraph_equal g1 g2 = True"

(*lemma graph_eq:
  fixes g1 g2 :: IRGraph
  shows "g1 = g2 ⟷ IRGraph_equal g1 g2"
  sorry*)

instantiation IRGraph :: equal
begin

definition equal_IRGraph :: "IRGraph ⇒ IRGraph ⇒ bool" where
  "equal_IRGraph = IRGraph_equal"

instance proof
  fix g1 g2 :: IRGraph
  show "equal_class.equal g1 g2 ⟷ (g1 = g2)"
    apply standard
    unfolding equal_IRGraph_def IRGraph_equal_def
    unfolding as_list_def
    apply transfer
    sorry
qed
end

end