theory Scratch
  imports Main
begin

datatype 'a match_expr = Match 'a

datatype action = Pass | Match | Block

type_synonym ('a, 'p) matcher = "'a \<Rightarrow> 'p \<Rightarrow> bool"

record 'a pf_rule2 =
  get_action :: action

record anchor_rule =
  Direction :: unit

record 'a anchor_rule2 =
  get_match :: "'a match_expr"

datatype 'a line =
  Option
  | PfRule "'a pf_rule2"

type_synonym 'a ruleset = "'a line list"

datatype decision =
  Accept
  | Reject
  | Undecided

fun filter :: "'a ruleset \<Rightarrow> ('a, 'p) matcher \<Rightarrow> 'p \<Rightarrow> _ \<Rightarrow> _" where
 "filter [] _ _ d = d"

lemma "filter rules m packet Undecided = filter rules m packet Undecided"
  quickcheck
  sorry

end