theory Exercise12 imports "HOL-IMP.Complete_Lattice" begin section "Complete Lattice over Lists" (* Fill in the gaps! *) instantiation list :: (order) order begin definition less_eq_list :: "('a::order)list \ 'a list \ bool" where "xs \ ys \ length xs = length ys \ (\p ys ! p)" definition less_list :: "'a list \ 'a list \ bool" where "less_list x y = (x \ y \ \ y \ x)" instance sorry end definition Inf_list :: "nat \ ('a::complete_lattice) list set \ 'a list" where "Inf_list n M = undefined" interpretation Complete_Lattice "{xs. length xs = n}" "Inf_list n" for n sorry end