Theory Partial_Order_Reduction.Basic_Extensions

section ‹Basics›

theory Basic_Extensions
imports "HOL-Library.Infinite_Set"
begin

  subsection ‹Types›

    type_synonym 'a step = "'a  'a"

  subsection ‹Rules›

    declare less_imp_le[dest, simp]
  
    declare le_funI[intro]
    declare le_funE[elim]
    declare le_funD[dest]
  
    lemma IdI'[intro]:
      assumes "x = y"
      shows "(x, y)  Id"
      using assms by auto

    lemma (in order) order_le_cases:
      assumes "x  y"
      obtains (eq) "x = y" | (lt) "x < y"
      using assms le_less by auto  

    lemma (in linorder) linorder_cases':
      obtains (le) "x  y" | (gt) "x > y"
      by force
  
    lemma monoI_comp[intro]:
      assumes "mono f" "mono g"
      shows "mono (f  g)"
      using assms by (intro monoI, auto dest: monoD)
    lemma strict_monoI_comp[intro]:
      assumes "strict_mono f" "strict_mono g"
      shows "strict_mono (f  g)"
      using assms by (intro strict_monoI, auto dest: strict_monoD)

    lemma eq_le_absorb[simp]:
      fixes x y :: "'a :: order"
      shows "x = y  x  y  x = y" "x  y  x = y  x = y"
      by auto

    lemma INFM_Suc[simp]: "( i. P (Suc i))  ( i. P i)"
      unfolding INFM_nat using Suc_lessE less_Suc_eq by metis
    lemma INFM_plus[simp]: "( i. P (i + n :: nat))  ( i. P i)"
    proof (induct n)
      case 0
      show ?case by simp
    next
      case (Suc n)
      have "( i. P (i + Suc n))  ( i. P (Suc i + n))" by simp
      also have "  ( i. P (i + n))" using INFM_Suc by this
      also have "  ( i. P i)" using Suc by this
      finally show ?case by this
    qed
    lemma INFM_minus[simp]: "( i. P (i - n :: nat))  ( i. P i)"
    proof (induct n)
      case 0
      show ?case by simp
    next
      case (Suc n)
      have "( i. P (i - Suc n))  ( i. P (Suc i - Suc n))" using INFM_Suc by meson
      also have "  ( i. P (i - n))" by simp
      also have "  ( i. P i)" using Suc by this
      finally show ?case by this
    qed

  subsection ‹Constants›

    definition const :: "'a  'b  'a"
      where "const x  λ _. x"
    definition const2 :: "'a  'b  'c  'a"
      where "const2 x  λ _ _. x"
    definition const3 :: "'a  'b  'c  'd  'a"
      where "const3 x  λ _ _ _. x"
    definition const4 :: "'a  'b  'c  'd  'e  'a"
      where "const4 x  λ _ _ _ _. x"
    definition const5 :: "'a  'b  'c  'd  'e  'f  'a"
      where "const5 x  λ _ _ _ _ _. x"
  
    lemma const_apply[simp]: "const x y = x" unfolding const_def by rule
    lemma const2_apply[simp]: "const2 x y z = x" unfolding const2_def by rule
    lemma const3_apply[simp]: "const3 x y z u = x" unfolding const3_def by rule
    lemma const4_apply[simp]: "const4 x y z u v = x" unfolding const4_def by rule
    lemma const5_apply[simp]: "const5 x y z u v w = x" unfolding const5_def by rule

    definition zip_fun :: "('a  'b)  ('a  'c)  'a  'b × 'c" (infixr  51)
      where "f  g  λ x. (f x, g x)"
  
    lemma zip_fun_simps[simp]:
      "(f  g) x = (f x, g x)"
      "fst  (f  g) = f"
      "snd  (f  g) = g"
      "fst  h  snd  h = h"
      "fst ` range (f  g) = range f"
      "snd ` range (f  g) = range g"
      unfolding zip_fun_def by force+
  
    lemma zip_fun_eq[dest]:
      assumes "f  g = h  i"
      shows "f = h" "g = i"
      using assms unfolding zip_fun_def by (auto dest: fun_cong)
  
    lemma zip_fun_range_subset[intro, simp]: "range (f  g)  range f × range g"
      unfolding zip_fun_def by blast
    lemma zip_fun_range_finite[elim]:
      assumes "finite (range (f  g))"
      obtains "finite (range f)" "finite (range g)"
    proof
      show "finite (range f)" using finite_imageI [OF assms(1), of fst]
        by (simp add: image_image)
      show "finite (range g)" using finite_imageI [OF assms(1), of snd]
        by (simp add: image_image)
    qed
  
    lemma zip_fun_split:
      obtains f g
      where "h = f  g"
    proof
      show "h = fst  h  snd  h" by simp
    qed
  
    abbreviation "None_None  (None, None)"
    abbreviation "None_Some  λ (y). (None, Some y)"
    abbreviation "Some_None  λ (x). (Some x, None)"
    abbreviation "Some_Some  λ (x, y). (Some x, Some y)"
  
    abbreviation "None_None_None  (None, None, None)"
    abbreviation "None_None_Some  λ (z). (None, None, Some z)"
    abbreviation "None_Some_None  λ (y). (None, Some y, None)"
    abbreviation "None_Some_Some  λ (y, z). (None, Some y, Some z)"
    abbreviation "Some_None_None  λ (x). (Some x, None, None)"
    abbreviation "Some_None_Some  λ (x, z). (Some x, None, Some z)"
    abbreviation "Some_Some_None  λ (x, y). (Some x, Some y, None)"
    abbreviation "Some_Some_Some  λ (x, y, z). (Some x, Some y, Some z)"

    lemma inj_Some2[simp, intro]:
      "inj None_Some"
      "inj Some_None"
      "inj Some_Some"
      by (rule injI, force)+
  
    lemma inj_Some3[simp, intro]:
      "inj None_None_Some"
      "inj None_Some_None"
      "inj None_Some_Some"
      "inj Some_None_None"
      "inj Some_None_Some"
      "inj Some_Some_None"
      "inj Some_Some_Some"
      by (rule injI, force)+
  
    definition swap :: "'a × 'b  'b × 'a"
      where "swap x  (snd x, fst x)"
  
    lemma swap_simps[simp]: "swap (a, b) = (b, a)" unfolding swap_def by simp
    lemma swap_inj[intro, simp]: "inj swap" by (rule injI, auto)
    lemma swap_surj[intro, simp]: "surj swap" by (rule surjI[where ?f = swap], auto)
    lemma swap_bij[intro, simp]: "bij swap" by (rule bijI, auto)
  
    definition push :: "('a × 'b) × 'c  'a × 'b × 'c"
      where "push x  (fst (fst x), snd (fst x), snd x)"
    definition pull :: "'a × 'b × 'c  ('a × 'b) × 'c"
      where "pull x  ((fst x, fst (snd x)), snd (snd x))"
  
    lemma push_simps[simp]: "push ((x, y), z) = (x, y, z)" unfolding push_def by simp
    lemma pull_simps[simp]: "pull (x, y, z) = ((x, y), z)" unfolding pull_def by simp

    definition label :: "'vertex × 'label × 'vertex  'label"
      where "label  fst  snd"
  
    lemma label_select[simp]: "label (p, a, q) = a" unfolding label_def by simp

  subsection ‹Theorems for @term{curry} and @term{split}›

    lemma curry_split[simp]: "curry  case_prod = id" by auto
    lemma split_curry[simp]: "case_prod  curry = id" by auto
  
    lemma curry_le[simp]: "curry f  curry g  f  g" unfolding le_fun_def by force
    lemma split_le[simp]: "case_prod f  case_prod g  f  g" unfolding le_fun_def by force
  
    lemma mono_curry_left[simp]: "mono (curry  h)  mono h"
      unfolding mono_def by fastforce
    lemma mono_split_left[simp]: "mono (case_prod  h)  mono h"
      unfolding mono_def by fastforce
    lemma mono_curry_right[simp]: "mono (h  curry)  mono h"
      unfolding mono_def split_le[symmetric] by bestsimp
    lemma mono_split_right[simp]: "mono (h  case_prod)  mono h"
      unfolding mono_def curry_le[symmetric] by bestsimp
  
    lemma Collect_curry[simp]: "{x. P (curry x)} = case_prod ` {x. P x}" using image_Collect by fastforce
    lemma Collect_split[simp]: "{x. P (case_prod x)} = curry ` {x. P x}" using image_Collect by force
  
    lemma gfp_split_curry[simp]: "gfp (case_prod  f  curry) = case_prod (gfp f)"
    proof -
      have "gfp (case_prod  f  curry) = Sup {u. u  case_prod (f (curry u))}" unfolding gfp_def by simp
      also have " = Sup {u. curry u  curry (case_prod (f (curry u)))}" unfolding curry_le by simp
      also have " = Sup {u. curry u  f (curry u)}" by simp
      also have " = Sup (case_prod ` {u. u  f u})" unfolding Collect_curry[of "λ u. u  f u"] by simp
      also have " = case_prod (Sup {u. u  f u})" by (force simp add: image_comp)
      also have " = case_prod (gfp f)" unfolding gfp_def by simp
      finally show ?thesis by this
    qed
    lemma gfp_curry_split[simp]: "gfp (curry  f  case_prod) = curry (gfp f)"
    proof -
      have "gfp (curry  f  case_prod) = Sup {u. u  curry (f (case_prod u))}" unfolding gfp_def by simp
      also have " = Sup {u. case_prod u  case_prod (curry (f (case_prod u)))}" unfolding split_le by simp
      also have " = Sup {u. case_prod u  f (case_prod u)}" by simp
      also have " = Sup (curry ` {u. u  f u})" unfolding Collect_split[of "λ u. u  f u"] by simp
      also have " = curry (Sup {u. u  f u})" by (force simp add: image_comp)
      also have " = curry (gfp f)" unfolding gfp_def by simp
      finally show ?thesis by this
    qed

    lemma not_someI:
      assumes " x. P x  False"
      shows "¬ P (SOME x. P x)"
      using assms by blast
    lemma some_ccontr:
      assumes "( x. ¬ P x)  False"
      shows "P (SOME x. P x)"
      using assms someI_ex ccontr by metis

end