Theory Lib
chapter "Library"
theory Lib
imports Main
begin
lemma hd_map_simp:
"b ≠ [] ⟹ hd (map a b) = a (hd b)"
by (rule hd_map)
lemma tl_map_simp:
"tl (map a b) = map a (tl b)"
by (induct b,auto)
lemma Collect_eq:
"{x. P x} = {x. Q x} ⟷ (∀x. P x = Q x)"
by (rule iffI) auto
lemma iff_impI: "⟦P ⟹ Q = R⟧ ⟹ (P ⟶ Q) = (P ⟶ R)" by blast
definition
fun_app :: "('a ⇒ 'b) ⇒ 'a ⇒ 'b" (infixr ‹$› 10) where
"f $ x ≡ f x"
declare fun_app_def [iff]
lemma fun_app_cong[fundef_cong]:
"⟦ f x = f' x' ⟧ ⟹ (f $ x) = (f' $ x')"
by simp
lemma fun_app_apply_cong[fundef_cong]:
"f x y = f' x' y' ⟹ (f $ x) y = (f' $ x') y'"
by simp
lemma if_apply_cong[fundef_cong]:
"⟦ P = P'; x = x'; P' ⟹ f x' = f' x'; ¬ P' ⟹ g x' = g' x' ⟧
⟹ (if P then f else g) x = (if P' then f' else g') x'"
by simp
lemma case_prod_apply_cong[fundef_cong]:
"⟦ f (fst p) (snd p) s = f' (fst p') (snd p') s' ⟧ ⟹ case_prod f p s = case_prod f' p' s'"
by (simp add: split_def)
definition
pred_conj :: "('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ ('a ⇒ bool)" (infixl ‹and› 35)
where
"pred_conj P Q ≡ λx. P x ∧ Q x"
definition
pred_disj :: "('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ ('a ⇒ bool)" (infixl ‹or› 30)
where
"pred_disj P Q ≡ λx. P x ∨ Q x"
definition
pred_neg :: "('a ⇒ bool) ⇒ ('a ⇒ bool)" (‹not _› [40] 40)
where
"pred_neg P ≡ λx. ¬ P x"
definition "K ≡ λx y. x"
definition
zipWith :: "('a ⇒ 'b ⇒ 'c) ⇒ 'a list ⇒ 'b list ⇒ 'c list" where
"zipWith f xs ys ≡ map (case_prod f) (zip xs ys)"
primrec
delete :: "'a ⇒ 'a list ⇒ 'a list"
where
"delete y [] = []"
| "delete y (x#xs) = (if y=x then xs else x # delete y xs)"
primrec
find :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a option"
where
"find f [] = None"
| "find f (x # xs) = (if f x then Some x else find f xs)"
definition
"swp f ≡ λx y. f y x"
primrec (nonexhaustive)
theRight :: "'a + 'b ⇒ 'b" where
"theRight (Inr x) = x"
primrec (nonexhaustive)
theLeft :: "'a + 'b ⇒ 'a" where
"theLeft (Inl x) = x"
definition
"isLeft x ≡ (∃y. x = Inl y)"
definition
"isRight x ≡ (∃y. x = Inr y)"
definition
"const x ≡ λy. x"
lemma tranclD2:
"(x, y) ∈ R⇧+ ⟹ ∃z. (x, z) ∈ R⇧* ∧ (z, y) ∈ R"
by (erule tranclE) auto
lemma linorder_min_same1 [simp]:
"(min y x = y) = (y ≤ (x::'a::linorder))"
by (auto simp: min_def linorder_not_less)
lemma linorder_min_same2 [simp]:
"(min x y = y) = (y ≤ (x::'a::linorder))"
by (auto simp: min_def linorder_not_le)
text ‹A combinator for pairing up well-formed relations.
The divisor function splits the population in halves,
with the True half greater than the False half, and
the supplied relations control the order within the halves.›
definition
wf_sum :: "('a ⇒ bool) ⇒ ('a × 'a) set ⇒ ('a × 'a) set ⇒ ('a × 'a) set"
where
"wf_sum divisor r r' ≡
({(x, y). ¬ divisor x ∧ ¬ divisor y} ∩ r')
∪ {(x, y). ¬ divisor x ∧ divisor y}
∪ ({(x, y). divisor x ∧ divisor y} ∩ r)"
lemma wf_sum_wf:
"⟦ wf r; wf r' ⟧ ⟹ wf (wf_sum divisor r r')"
apply (simp add: wf_sum_def)
apply (rule wf_Un)+
apply (erule wf_Int2)
apply (rule wf_subset
[where r="measure (λx. If (divisor x) 1 0)"])
apply simp
apply clarsimp
apply blast
apply (erule wf_Int2)
apply blast
done
abbreviation(input)
"option_map == map_option"
lemmas option_map_def = map_option_case
lemma False_implies_equals [simp]:
"((False ⟹ P) ⟹ PROP Q) ≡ PROP Q"
apply (rule equal_intr_rule)
apply (erule meta_mp)
apply simp
apply simp
done
lemma split_paired_Ball:
"(∀x ∈ A. P x) = (∀x y. (x,y) ∈ A ⟶ P (x,y))"
by auto
lemma split_paired_Bex:
"(∃x ∈ A. P x) = (∃x y. (x,y) ∈ A ∧ P (x,y))"
by auto
end