# Theory Basis

```(*  Author:     Stefan Berghofer, TU Muenchen, 2005
*)

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
```