theory Scratch imports Main begin

lemma Option_map_mono [partial_function_mono]:
  assumes "mono_option F"
  shows "mono_option (%f. Option.map g (F f))"
by(rule monotoneI)(auto simp add: flat_ord_def dest!: monotoneD[OF assms])

type_synonym ('mdigraph, 'node, 'edge, 's) mdigraph_iter =
  "'mdigraph => ('s => bool) => ('edge => 's => 's) => 'node => 's => 's"

locale test = 
  fixes target :: "'mdigraph => 'edge => 'node"
begin

definition succs :: "('mdigraph, 'node, 'edge, 'edge list) mdigraph_iter => 'mdigraph => 'node => 'edge list"
where "succs = undefined"

partial_function (option) foo ::
  "('mdigraph, 'node, 'edge, 'edge list) mdigraph_iter 
   => 'mdigraph => 'node => ('edge * 'node) list => 'edge list option"
where
  "fooo iter G n queue =
   (case queue of [] => None
    | ((e', n') # queue') => 
      if n = n' then Some [e']
      else Option.map (Cons e') (fooo iter G n (queue @ map (\<lambda>e. (e, target G e)) (succs iter G n'))))"

end


notepad begin
  fix xs ys :: "'a list"
  have "xs = ys"
  proof(induction xs\<equiv>"xs" rule: list.induct)
    print_cases
    oops
end



end