Theory Utils

Up to index of Isabelle/HOL/Tables

header {* Utilities *}

theory Utils = Main:

text {* The following variant of modus ponens is useful as erule,
for example for preparing local inductions. *}

lemma mp1: "\<lbrakk> P; P \<longrightarrow> Q \<rbrakk> \<Longrightarrow> Q"
by simp

subsection {* Functions *}

subsubsection {* Combinators *}

consts const :: "'a \<Rightarrow> 'b \<Rightarrow> 'a"
defs const_def: "const == % x y . x"

lemma const[simp]: "const x y = x"
by (simp add: const_def)

lemma const_expand: "const c = (% x . c)"
by (rule ext, simp)

consts flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'c)"
defs flip_def[simp]: "flip f x y == f y x"

subsubsection {* Currying *}

constdefs
  curry :: "(('a * 'b) \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c"
  "curry f == % a b . f (a,b)"
  uncurry :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a * 'b) \<Rightarrow> 'c"
  "uncurry g == % p . g (fst p) (snd p)"

lemma curry[simp]: "curry f a b = f (a,b)"
by (simp add: curry_def)

lemma uncurry[simp]: "uncurry g (a,b) = g a b"
by (simp add: uncurry_def)

lemma uncurry_lambda2[simp]: "uncurry (\<lambda>h t. F h t) = (\<lambda>p . F (fst p) (snd p))"
by (simp add: uncurry_def)

lemma uncurry_K2[simp]: "uncurry (\<lambda>h t. F h) = (\<lambda>p . F (fst p))"
by simp

lemma uncurry_K[simp]: "uncurry (\<lambda>h. F) = (\<lambda>p . F (snd p))"
by simp

subsubsection {* Pair Manipulation *}

constdefs
  pupd1 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a * 'c) \<Rightarrow> ('b * 'c)"
  "pupd1 f p == (f (fst p), snd p)"
  pupd2 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('c * 'a) \<Rightarrow> ('c * 'b)"
  "pupd2 g p == (fst p, g (snd p))"

lemma pupd1[simp]: "pupd1 f (x,y) = (f x, y)"
by (simp add: pupd1_def)

lemma pupd2[simp]: "pupd2 g (x,y) = (x, g y)"
by (simp add: pupd2_def)

subsubsection {* Extensionality *}

text {* I had some problems applying @{text "HOL.ext"} directly.*}

lemma f_ext:
 assumes eq: "\<And> x . f x = g x"
 shows "f = g"
by (rule HOL.ext)

subsection {* Function Properties *}

subsubsection {* Associativity *}

constdefs
  assoc :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
  "assoc f == (ALL x y z . f (f x y) z = f x (f y z))"

lemma assoc[simp]:
  "assoc f \<Longrightarrow> f (f x y) z = f x (f y z)"
by (unfold assoc_def, auto)

lemma assoc_intro[intro?]:
  "\<lbrakk> \<And> x y z . f (f x y) z = f x (f y z) \<rbrakk> \<Longrightarrow> assoc f"
by (unfold assoc_def, auto)

(*
lemma assoc_const[simp]: "assoc (% x y . x)"
by (rule assoc_intro, simp)
*)

lemma const_assoc[simp]: "assoc const"
by (rule assoc_intro, simp)

subsubsection {* Idempotence *}

constdefs
  idempotent :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
  "idempotent f == (ALL x . f x x = x)"

lemma idempotent[simp]:
  "idempotent f \<Longrightarrow> f x x = x"
by (unfold idempotent_def, auto)

lemma idempotent_intro[intro?]:
  "\<lbrakk> \<And> x . f x x = x \<rbrakk> \<Longrightarrow> idempotent f"
by (unfold idempotent_def, auto)

subsubsection {* Commutativity *}

constdefs
  commutative :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
  "commutative f == (ALL x y . f x y = f y x)"

lemma commutative:
  "commutative f \<Longrightarrow> f x y = f y x"
by (unfold commutative_def, auto)

lemma commutative_intro[intro?]:
  "\<lbrakk> \<And> x y . f x y = f y x \<rbrakk> \<Longrightarrow> commutative f"
by (unfold commutative_def, auto)

subsubsection {* Units *}

consts LRunit :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'bool"

defs LRunit_def: "LRunit f u == ALL y . f u y = y & f y u = y"

lemma LRunit_left: "LRunit f u \<Longrightarrow> f u x = x"
by (unfold LRunit_def, simp)

lemma LRunit_right: "LRunit f u \<Longrightarrow> f x u = x"
by (unfold LRunit_def, simp)

lemma LRunit_equal:
  assumes u[intro,simp]: "LRunit f u"
  assumes v[intro,simp]: "LRunit f v"
  shows "u = v"
proof -
  have "u = f u v" by (rule sym, rule LRunit_right, simp)
  also have "f u v = v" by (rule LRunit_left, simp)
  finally show ?thesis .
qed

lemma LRunit_const:
 "ALL x . LRunit c (F x) \<Longrightarrow> F x = F arbitrary"
apply (subgoal_tac "ALL x y . F x = F y", simp)
  apply (intro strip)
  apply (rule LRunit_equal [of c])
apply simp_all
done

subsection {* Additional Material for Lists *}

lemma foldr_append:
 "foldr f (xs @ ys) z = foldr f xs (foldr f ys z)"
by (induct_tac xs, auto)

consts
 foldr_1 :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) * 'a list \<Rightarrow> 'a"

recdef foldr_1 "measure (% (f,xs) . length xs)"
 foldr_1_sing[simp]: "foldr_1 (f, x # []) = x"
 foldr_1_cons0[simp]: "foldr_1 (f, x # y # ys) = f x (foldr_1 (f, y # ys))"

lemma foldr_1_cons[simp]:
   "\<lbrakk> xs ~= [] \<rbrakk> \<Longrightarrow> foldr_1 (f, x # xs) = f x (foldr_1 (f, xs))"
by (cases xs, auto)

lemma foldr_1_append_distr_0:
 "assoc f \<Longrightarrow>
  (ALL x ys . ys ~= [] \<longrightarrow> foldr_1 (f, x # xs @ ys) = f (foldr_1 (f, x # xs)) (foldr_1 (f, ys)))"
by (induct_tac xs, auto)

lemma foldr_1_append_distr:
 assumes xs[simp]: "xs ~= []"
 assumes ys[simp]: " ys ~= []"
 assumes f[simp]: "assoc f"
 shows "foldr_1 (f, xs @ ys) = f (foldr_1 (f, xs)) (foldr_1 (f, ys))"
proof (cases xs)
 case Nil
   thus ?thesis by simp
next
 case Cons
   thus ?thesis by (insert foldr_1_append_distr_0 [of f "tl xs"], simp)
qed

lemma mem_append[simp]:
 "x mem (xs @ ys) = (x mem xs | x mem ys)"
by (induct_tac xs, simp_all)

constdefs
 zipWith :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
 "zipWith f xs ys == map (uncurry f) (zip xs ys)"

lemma zipWith_Cons[simp]:
 "zipWith f (x#xs) (y#ys) = f x y # zipWith f xs ys"
by (simp add: zipWith_def)

lemma zipWith_Nil_1[simp]:
 "zipWith f [] ys = []"
by (simp add: zipWith_def)

lemma zipWith_Nil_2[simp]:
 "zipWith f xs [] = []"
by (simp add: zipWith_def)

lemma zipWith_assoc_0:
  "assoc f \<Longrightarrow> ALL ys zs . zipWith f (zipWith f xs ys) zs = zipWith f xs (zipWith f ys zs)"
apply (induct_tac xs, simp)
apply (intro strip)
apply (induct_tac ys, simp)
apply (induct_tac zs, simp)
apply simp
done

lemma zipWith_assoc[simp]:
  "assoc f \<Longrightarrow> zipWith f (zipWith f xs ys) zs = zipWith f xs (zipWith f ys zs)"
by (insert zipWith_assoc_0, auto)

lemma assoc_zipWith[simp]: "assoc f \<Longrightarrow> assoc (zipWith f)"
by (rule assoc_intro, simp)

subsection {* Option Utilities *}

consts
 option :: "'b \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b"

primrec
 option_N: "option r f None = r"
 option_S: "option r f (Some a) = f a"

subsubsection {* The Option Monad *}

consts
 optThen :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option"

primrec
 optThen_N: "optThen None = (% f . None)"
 optThen_S: "optThen (Some x) = (% f . f x)"

declare optThen_N[simp del]
declare optThen_S[simp del]

lemma optThen_N_f[simp]: "optThen None f = None"
by (simp add: optThen_N)

lemma optThen_S_f[simp]: "optThen (Some x) f = f x"
by (simp add: optThen_S)

lemma optThen_result_Some[simp]:
  "optThen m f = Some x \<Longrightarrow> EX y . m = Some y & f y = Some x"
by (cases m, simp_all)

lemma optThen_option_map[simp]:
 "optThen (option_map f x) g = optThen x (g o f)"
by (cases x, simp_all)

lemma optThen_assoc[simp]:
 "optThen (optThen x f) g = optThen x (% x . optThen (f x) g)"
by (cases x, simp_all)

subsubsection {* Equality Option Collapse *}

consts
 optEq :: "'a option \<Rightarrow> 'a option \<Rightarrow> 'a option"

primrec
 optEq_N: "optEq None = (% my . None)"
 optEq_S: "optEq (Some x) = option None (% y . if (x=y) then Some x else None)"

declare optEq_N[simp del]
declare optEq_S[simp del]

lemma optEq_S_S[simp]:
 "optEq (Some x) (Some y) = (if (x=y) then Some x else None)"
by (simp add: optEq_S)

lemma optEq_S_N[simp]: "optEq (Some x) None = None"
by (simp add: optEq_S)

lemma optEq_N_S[simp]: "optEq None (Some x) = None"
by (simp add: optEq_N)

lemma optEq_N_N[simp]: "optEq None None = None"
by (simp add: optEq_N)

lemma optEq_assoc[simp]: "optEq (optEq a b) c = optEq a (optEq b c)"
apply (cases a, simp add: optEq_N)
apply (cases b, simp add: optEq_N)
apply (cases c, simp add: optEq_N)
apply simp
done

lemma assoc_optEq[simp]: "assoc optEq"
by (rule assoc_intro, simp)

lemma optEq_idempotent[simp]: "idempotent optEq"
by (rule idempotent_intro, case_tac x, simp_all)

(* premise x=0 not available to simp --- why???
lemma optEq_commutative_0: "optEq x y = optEq y x"
proof (cases x)
 case None thus ?thesis proof (cases y)
   case None thus ?thesis apply simp
*)

lemma optEq_commutative[simp]: "commutative optEq"
apply (rule commutative_intro)
apply (case_tac x, case_tac y, simp_all add: optEq_N optEq_S)
apply (case_tac y, simp_all add: optEq_N optEq_S)
done

end

lemma mp1:

  [| P; P --> Q |] ==> Q

Functions

Combinators

lemma const:

  const x y = x

lemma const_expand:

  const c = (%x. c)

Currying

lemma curry:

  curry f a b = f (a, b)

lemma uncurry:

  uncurry g (a, b) = g a b

lemma uncurry_lambda2:

  uncurry F = (%p. F (fst p) (snd p))

lemma uncurry_K2:

  uncurry (%h t. F h) = (%p. F (fst p))

lemma uncurry_K:

  uncurry (%h. F) = (%p. F (snd p))

Pair Manipulation

lemma pupd1:

  pupd1 f (x, y) = (f x, y)

lemma pupd2:

  pupd2 g (x, y) = (x, g y)

Extensionality

lemma

  (!!x. f x = g x) ==> f = g

Function Properties

Associativity

lemma assoc:

  assoc f ==> f (f x y) z = f x (f y z)

lemma assoc_intro:

  (!!x y z. f (f x y) z = f x (f y z)) ==> assoc f

lemma const_assoc:

  assoc const

Idempotence

lemma idempotent:

  idempotent f ==> f x x = x

lemma idempotent_intro:

  (!!x. f x x = x) ==> idempotent f

Commutativity

lemma commutative:

  commutative f ==> f x y = f y x

lemma commutative_intro:

  (!!x y. f x y = f y x) ==> commutative f

Units

lemma LRunit_left:

  LRunit f u ==> f u x = x

lemma LRunit_right:

  LRunit f u ==> f x u = x

lemma

  [| LRunit f u; LRunit f v |] ==> u = v

lemma LRunit_const:

  ALL x. LRunit c (F x) ==> F x = F arbitrary

Additional Material for Lists

lemma foldr_append:

  foldr f (xs @ ys) z = foldr f xs (foldr f ys z)

lemma foldr_1_cons:

  xs ~= [] ==> foldr_1 (f, x # xs) = f x (foldr_1 (f, xs))

lemma foldr_1_append_distr_0:

  assoc f
  ==> ALL x ys.
         ys ~= [] -->
         foldr_1 (f, x # xs @ ys) = f (foldr_1 (f, x # xs)) (foldr_1 (f, ys))

lemma

  [| xs ~= []; ys ~= []; assoc f |]
  ==> foldr_1 (f, xs @ ys) = f (foldr_1 (f, xs)) (foldr_1 (f, ys))

lemma mem_append:

  x mem xs @ ys = (x mem xs | x mem ys)

lemma zipWith_Cons:

  zipWith f (x # xs) (y # ys) = f x y # zipWith f xs ys

lemma zipWith_Nil_1:

  zipWith f [] ys = []

lemma zipWith_Nil_2:

  zipWith f xs [] = []

lemma zipWith_assoc_0:

  assoc f
  ==> ALL ys zs. zipWith f (zipWith f xs ys) zs = zipWith f xs (zipWith f ys zs)

lemma zipWith_assoc:

  assoc f ==> zipWith f (zipWith f xs ys) zs = zipWith f xs (zipWith f ys zs)

lemma assoc_zipWith:

  assoc f ==> assoc (zipWith f)

Option Utilities

The Option Monad

lemma optThen_N_f:

  optThen None f = None

lemma optThen_S_f:

  optThen (Some x) f = f x

lemma optThen_result_Some:

  optThen m f = Some x ==> EX y. m = Some y & f y = Some x

lemma optThen_option_map:

  optThen (option_map f x) g = optThen x (g o f)

lemma optThen_assoc:

  optThen (optThen x f) g = optThen x (%x. optThen (f x) g)

Equality Option Collapse

lemma optEq_S_S:

  optEq (Some x) (Some y) = (if x = y then Some x else None)

lemma optEq_S_N:

  optEq (Some x) None = None

lemma optEq_N_S:

  optEq None (Some x) = None

lemma optEq_N_N:

  optEq None None = None

lemma optEq_assoc:

  optEq (optEq a b) c = optEq a (optEq b c)

lemma assoc_optEq:

  assoc optEq

lemma optEq_idempotent:

  idempotent optEq

lemma optEq_commutative:

  commutative optEq