Theory Infra
chapter ‹Protocol Modeling and Refinement Infrastructure›
text ‹This chapter sets up our theory of refinement and the protocol
modeling infrastructure.›
section ‹Proving infrastructure›
theory Infra imports Main
begin
subsection ‹Prover configuration›
declare if_split_asm [split]
subsection ‹Forward reasoning ("attributes")›
text ‹The following lemmas are used to produce intro/elim rules from
set definitions and relation definitions.›
lemmas set_def_to_intro = meta_eq_to_obj_eq [THEN eqset_imp_iff, THEN iffD2]
lemmas set_def_to_dest = meta_eq_to_obj_eq [THEN eqset_imp_iff, THEN iffD1]
lemmas set_def_to_elim = set_def_to_dest [elim_format]
lemmas setc_def_to_intro =
set_def_to_intro [where B="{x. P x}" for P, to_pred]
lemmas setc_def_to_dest =
set_def_to_dest [where B="{x. P x}" for P, to_pred]
lemmas setc_def_to_elim = setc_def_to_dest [elim_format]
lemmas rel_def_to_intro = setc_def_to_intro [where x="(s, t)" for s t]
lemmas rel_def_to_dest = setc_def_to_dest [where x="(s, t)" for s t]
lemmas rel_def_to_elim = rel_def_to_dest [elim_format]
subsection ‹General results›
subsubsection ‹Maps›
text ‹We usually remove @{term"domIff"} from the simpset and clasets due
to annoying behavior. Sometimes the lemmas below are more well-behaved than
@{term "domIff"}. Usually to be used as "dest: dom\_lemmas". However, adding
them as permanent dest rules slows down proofs too much, so we refrain from
doing this.›
lemma map_definedness:
"f x = Some y ⟹ x ∈ dom f"
by (simp add: domIff)
lemma map_definedness_contra:
"⟦ f x = Some y; z ∉ dom f ⟧ ⟹ x ≠ z"
by (auto simp add: domIff)
lemmas dom_lemmas = map_definedness map_definedness_contra
subsubsection ‹Set›
lemma vimage_image_subset: "A ⊆ f-`(f`A)"
by (auto simp add: image_def vimage_def)
subsubsection ‹Relations›
lemma Image_compose [simp]:
"(R1 O R2)``A = R2``(R1``A)"
by (auto)
subsubsection ‹Lists›
lemma map_id: "map id = id"
by (simp)
lemma map_comp: "map (g o f) = map g o map f"
by (simp)
declare map_comp_map [simp del]
lemma take_prefix: "⟦ take n l = xs ⟧ ⟹ ∃xs'. l = xs @ xs'"
by (induct l arbitrary: n xs, auto)
(case_tac n, auto)
subsubsection ‹Finite sets›
text ‹Cardinality.›
declare arg_cong [where f=card, intro]
lemma finite_positive_cardI [intro!]:
"⟦ A ≠ {}; finite A ⟧ ⟹ 0 < card A"
by (auto)
lemma finite_positive_cardD [dest!]:
"⟦ 0 < card A; finite A ⟧ ⟹ A ≠ {}"
by (auto)
lemma finite_zero_cardI [intro!]:
"⟦ A = {}; finite A ⟧ ⟹ card A = 0"
by (auto)
lemma finite_zero_cardD [dest!]:
"⟦ card A = 0; finite A ⟧ ⟹ A = {}"
by (auto)
end