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 = xsi"
  apply (induct xs arbitrary: i)
  apply simp
  apply (case_tac i)
  apply simp_all
  done

lemma [simp]: "xs  i  (xs @ ys)i = ysi - 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 xsa?)"

primrec unique :: "('a × 'b) list  bool"
where
  "unique [] = True"
| "unique (x # xs) = (xsfst x? =   unique xs)"

lemma assoc_set: "psx? = y  (x, y)  set ps"
  by (induct ps) (auto split: if_split_asm)

lemma map_assoc_None [simp]:
  "psx? =   map (λ(x, y). (x, f x y)) psx? = "
  by (induct ps) auto

no_syntax
  "_Map" :: "maplets => 'a  'b"  ("(1[_])")


end