Theory ResNormCompare

theory ResNormCompare
  imports
    ResNormDirect
    ResNormRewrite
begin

section‹Comparison of Resource Term Normalisation›

text‹The two normalisation procedures have the same outcome, because they both normalise the term›
lemma normal_rewr_is_normal_dir:
  "normal_rewr = normal_dir"
proof
  fix x :: "('a, 'b) res_term"
  show "normal_rewr x = normal_dir x"
    using normal_dir_normalised res_term_equiv_normal_dir
          normal_rewr_normalised res_term_equiv_normal_rewr
    by metis
qed

text‹
  With resource term normalisation to decide the equvialence, we can prove that the resource term
  mapping may render terms equivalent.
›
lemma
  fixes a b :: 'a and c :: 'b
  assumes "a ≠ b"
  obtains f :: "'a ⇒ 'b" and x y where "map_res_term f g x ∼ map_res_term f g y" and "¬ x ∼ y"
proof
  show "map_res_term (λx. c) g (Res a) ∼ map_res_term (λx. c) g (Res b)"
    by simp
  show "¬ Res a ∼ Res b"
    using assms by (simp add: res_term_equiv_is_normal_rewr)
qed

end