Theory Degeneralization_Refine

theory Degeneralization_Refine
imports Degeneralization Refine
begin

  lemma degen_param[param]: "(degen, degen) ∈ ⟨S → bool_rel⟩ list_rel → S ×⇩r nat_rel → bool_rel"
  proof (intro fun_relI)
    fix cs ds ak bl
    assume "(cs, ds) ∈ ⟨S → bool_rel⟩ list_rel" "(ak, bl) ∈  S ×⇩r nat_rel"
    then show "(degen cs ak, degen ds bl) ∈ bool_rel"
      unfolding degen_def list_rel_def fun_rel_def list_all2_conv_all_nth
      by (cases "snd ak < length cs") (auto 0 3)
  qed

  lemma count_param[param]: "(Degeneralization.count, Degeneralization.count) ∈
    ⟨A → bool_rel⟩ list_rel → A → nat_rel → nat_rel"
    unfolding count_def null_def[symmetric] by parametricity

end