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"
  by auto

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 nth_el_append1 [simp]: "i < ∥xs∥ ⟹ (xs @ ys)⟨i⟩ = xs⟨i⟩"
proof (induct xs arbitrary: i)
  case Nil
  then show ?case
    by simp
next
  case (Cons a xs i)
  then show ?case by (cases i) auto
qed

lemma nth_el_append2 [simp]: "∥xs∥ ≤ i ⟹ (xs @ ys)⟨i⟩ = ys⟨i - ∥xs∥⟩"
proof (induct xs arbitrary: i)
  case Nil
  then show ?case
    by simp
next
  case (Cons a xs i)
  then show ?case by (cases i) auto
qed

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"  (‹(‹indent=1 notation=‹mixfix map››[_])›)

end