Theory Empty_Convergence_Graph

section ‹An Always-Empty Convergence Graph›

text ‹This theory implements a convergence graph that always returns an empty list for any lookup.
      By using this graph it is possible to represent methods via the SPY and H-Frameworks
      that do not distribute distinguishing traces over converging traces.›

theory Empty_Convergence_Graph
imports Convergence_Graph

type_synonym empty_cg = unit

definition empty_cg_empty :: "empty_cg" where
  "empty_cg_empty = ()"

definition empty_cg_initial :: "(('a,'b,'c) fsm  ('b×'c) prefix_tree  empty_cg)" where
  "empty_cg_initial M T = empty_cg_empty"

definition empty_cg_insert :: "(empty_cg  ('b×'c) list  empty_cg)" where
  "empty_cg_insert G v = empty_cg_empty"

definition empty_cg_lookup :: "(empty_cg  ('b×'c) list  ('b×'c) list list)" where
  "empty_cg_lookup G v = [v]"

definition empty_cg_merge :: "(empty_cg  ('b×'c) list  ('b×'c) list  empty_cg)" where
  "empty_cg_merge G u v = empty_cg_empty"

lemma empty_graph_initial_invar: "convergence_graph_initial_invar M1 M2 empty_cg_lookup empty_cg_initial"
  unfolding convergence_graph_initial_invar_def convergence_graph_lookup_invar_def empty_cg_lookup_def empty_cg_initial_def
  by auto

lemma empty_graph_insert_invar: "convergence_graph_insert_invar M1 M2 empty_cg_lookup empty_cg_insert"
  unfolding convergence_graph_insert_invar_def convergence_graph_lookup_invar_def empty_cg_lookup_def empty_cg_insert_def
  by auto

lemma empty_graph_merge_invar: "convergence_graph_merge_invar M1 M2 empty_cg_lookup empty_cg_merge"
  unfolding convergence_graph_merge_invar_def convergence_graph_lookup_invar_def empty_cg_lookup_def empty_cg_merge_def
  by auto