Theory Basis
theory Basis
imports Main
begin
section ‹General Utilities›
text ‹
This section introduces some general utilities that will be useful later on in
the formalization of System \fsub{}.
The following rewrite rules are useful for simplifying mutual induction rules.
›
lemma True_simps:
"(True ⟹ PROP P) ≡ PROP P"
"(PROP P ⟹ True) ≡ PROP Trueprop True"
"(⋀x. True) ≡ PROP Trueprop True"
apply -
apply rule
apply (erule meta_mp)
apply (rule TrueI)
apply assumption
apply rule
apply (rule TrueI)
apply assumption
apply rule
apply (rule TrueI)+
done
text ‹
Unfortunately, the standard introduction and elimination rules for bounded
universal and existential quantifier do not work properly for sets of pairs.
›
lemma ballpI: "(⋀x y. (x, y) ∈ A ⟹ P x y) ⟹ ∀(x, y) ∈ A. P x y"
by blast
lemma bpspec: "∀(x, y) ∈ A. P x y ⟹ (x, y) ∈ A ⟹ P x y"
by blast
lemma ballpE: "∀(x, y) ∈ A. P x y ⟹ (P x y ⟹ Q) ⟹
((x, y) ∉ A ⟹ Q) ⟹ Q"
by blast
lemma bexpI: "P x y ⟹ (x, y) ∈ A ⟹ ∃(x, y) ∈ A. P x y"
by blast
lemma bexpE: "∃(x, y) ∈ A. P x y ⟹
(⋀x y. (x, y) ∈ A ⟹ P x y ⟹ Q) ⟹ Q"
by blast
lemma ball_eq_sym: "∀(x, y) ∈ S. f x y = g x y ⟹ ∀(x, y) ∈ S. g x y = f x y"
by auto
lemma wf_measure_size: "wf (measure size)" by simp
notation
Some ("⌊_⌋")
notation
None ("⊥")
notation
length ("∥_∥")
notation
Cons ("_ ∷/ _" [66, 65] 65)
text ‹
The following variant of the standard ‹nth› function returns
‹⊥› if the index is out of range.
›
primrec
nth_el :: "'a list ⇒ nat ⇒ 'a option" ("_⟨_⟩" [90, 0] 91)
where
"[]⟨i⟩ = ⊥"
| "(x # xs)⟨i⟩ = (case i of 0 ⇒ ⌊x⌋ | Suc j ⇒ xs ⟨j⟩)"
lemma [simp]: "i < ∥xs∥ ⟹ (xs @ ys)⟨i⟩ = xs⟨i⟩"
apply (induct xs arbitrary: i)
apply simp
apply (case_tac i)
apply simp_all
done
lemma [simp]: "∥xs∥ ≤ i ⟹ (xs @ ys)⟨i⟩ = ys⟨i - ∥xs∥⟩"
apply (induct xs arbitrary: i)
apply simp
apply (case_tac i)
apply simp_all
done
text ‹Association lists›
primrec assoc :: "('a × 'b) list ⇒ 'a ⇒ 'b option" ("_⟨_⟩⇩?" [90, 0] 91)
where
"[]⟨a⟩⇩? = ⊥"
| "(x # xs)⟨a⟩⇩? = (if fst x = a then ⌊snd x⌋ else xs⟨a⟩⇩?)"
primrec unique :: "('a × 'b) list ⇒ bool"
where
"unique [] = True"
| "unique (x # xs) = (xs⟨fst x⟩⇩? = ⊥ ∧ unique xs)"
lemma assoc_set: "ps⟨x⟩⇩? = ⌊y⌋ ⟹ (x, y) ∈ set ps"
by (induct ps) (auto split: if_split_asm)
lemma map_assoc_None [simp]:
"ps⟨x⟩⇩? = ⊥ ⟹ map (λ(x, y). (x, f x y)) ps⟨x⟩⇩? = ⊥"
by (induct ps) auto
no_syntax
"_Map" :: "maplets => 'a ⇀ 'b" ("(1[_])")
end