lemma list_map_eq_imp_rel: shows "map f xs = map g ys ⟷ list_all2 (λx y. f x = g y) xs ys" proof assume assms: "map f xs = map g ys" hence "length xs = length ys" by (metis length_map) thus "list_all2 (λx y. f x = g y) xs ys" unfolding list_all2_conv_all_nth using assms by (auto intro: map_eq_imp_length_eq simp: nth_map[of _ xs f, symmetric]) next assume "list_all2 (λx y. f x = g y) xs ys" thus "map f xs = map g ys" by (induction xs ys rule: list.rel_induct; simp) qed
locale A = fixes foo :: "'a => 'b => nat" locale B = A1: A[where 'a = 'aa and 'b = 'bb] foo1 + A2: A[where 'a = 'cc and 'b = 'bb] foo2 for foo1 and foo2The alternative is to write type annotations on the constants in the
for
clause, which gets very verbose for big locales.
locale A = fixes foo :: "'a => 'b => nat" locale B = namespace: A concretefoo + assumes somelemma: "... namespace.foo ... concretefoo ..."
datatype ('a, 'b, 'c) sometype = MkSomeType 'a 'b 'c context fixes foo :: "'a => 'b => 'c => bool" begin type_synonym mytype = "('a, 'b, 'c) sometype" end
-v
option, print the verification time of the individual theories, and not just of the session.-v
option, the theories should be only displayed when their verification successfully completed, and not when it starts as is now the case.