Theory FMap

(*  Title:      FMap.thy
    Author:     Ludovic Henrio and Florian Kammuller, 2006

Finite maps for Sigma-calculus
Idea use axiomatic type classes to preserve
usability of datatype afterwards, i.e. definition
of an object as a finite map of labels to fields in
a datatype.
*)

section ‹Finite maps with axclasses›

theory FMap imports ListPre begin

type_synonym ('a, 'b) fmap = "('a :: finite) ⇀ 'b" (infixl ‹-~>› 50)

class inftype =
assumes infinite: "¬finite UNIV"

theorem fset_induct:
  "P {} ⟹ (⋀x (F::('a::finite)set). x ∉ F ⟹ P F ⟹ P (insert x F)) ⟹ P F"
proof (rule_tac P=P and F=F in finite_induct)
  from finite_subset[OF subset_UNIV] show "finite F" by auto
next
  assume "P {}" thus "P {}" by simp
next
  fix x F 
  assume "⋀x F. ⟦ x ∉ F; P F ⟧ ⟹ P (insert x F)" and "x ∉ F" and "P F"
  thus "P (insert x F)" by simp
qed

theorem fmap_unique: "x = y ⟹ (f::('a,'b)fmap) x = f y"
  by (erule ssubst, rule refl)

theorem fmap_case:
  "(F::('a -~> 'b)) = Map.empty ∨ (∃x y (F'::('a -~> 'b)). F = F'(x ↦ y))"
proof (cases "F = Map.empty")
  case True thus ?thesis by (rule disjI1)
next
  case False thus ?thesis
  proof (simp)
    from ‹F ≠ Map.empty› have "∃x. F x ≠ None"
    proof (rule contrapos_np)
      assume "¬ (∃x. F x ≠ None)"
      hence "∀x. F x = None" by simp
      hence "⋀x. F x = None" by simp
      thus "F = Map.empty" by (rule ext)
    qed
    thus "∃x y F'. F = F'(x ↦ y)"
    proof
      fix x assume "F x ≠ None"
      hence "⋀y. F y = (F(x ↦ the (F x))) y" by auto
      hence "F = F(x ↦ the (F x))" by (rule ext)
      thus ?thesis by auto
    qed
  qed
qed

(* define the witness as a constant function so it may be used in the proof of
the induction scheme below *)
definition  
  set_fmap :: "'a -~> 'b ⇒ ('a * 'b)set" where
  "set_fmap F = {(x, y). x ∈ dom F ∧ F x = Some y}"

definition
  pred_set_fmap :: "(('a -~> 'b) ⇒ bool) ⇒ (('a * 'b)set) ⇒ bool" where
  "pred_set_fmap P = (λS. P (λx. if x ∈ fst ` S 
                                  then (THE y. (∃z. y = Some z ∧ (x, z) ∈ S)) 
                                  else None))" 

definition
  fmap_minus_direct :: "[('a -~> 'b), ('a * 'b)] ⇒ ('a -~> 'b)" (infixl ‹--› 50) where
  "F -- x = (λz. if (fst x = z ∧ ((F (fst x)) = Some (snd x))) 
                   then None 
                   else (F z))"

lemma insert_lem : "insert x A = B ⟹ x ∈ B"
  by auto

lemma fmap_minus_fmap: 
  fixes F x a b
  assumes "(F -- x) a = Some b"
  shows "F a = Some b"
proof (rule ccontr, cases "F a")
  case None hence "a ∉ dom F" by auto
  hence "(F -- x) a = None" 
    unfolding fmap_minus_direct_def by auto
  with ‹(F -- x) a = Some b› show False by simp
next
  assume "F a ≠ Some b"
  case (Some y) thus False
  proof (cases "fst x = a")
    case True thus False
    proof (cases "snd x = y")
      case True with ‹F a = Some y› ‹fst x = a› 
      have "(F -- x) a = None" unfolding fmap_minus_direct_def by auto
      with ‹(F -- x) a = Some b› show False by simp
    next
      case False with ‹F a = Some y› ‹fst x = a› 
      have "F (fst x) ≠ Some (snd x)" by auto
      with ‹(F -- x) a = Some b› have "F a = Some b" 
        unfolding fmap_minus_direct_def by auto
      with ‹F a ≠ Some b› show False by simp
    qed
  next
    case False with ‹(F -- x) a = Some b› 
    have "F a = Some b" unfolding fmap_minus_direct_def by auto
    with ‹F a ≠ Some b› show False by simp
  qed
qed

lemma set_fmap_minus_iff: 
  "set_fmap ((F::(('a::finite) -~> 'b)) -- x) = set_fmap F - {x}"
  unfolding set_fmap_def 
proof (auto)
  fix a b assume "(F -- x) a = Some b" from fmap_minus_fmap[OF this]
  show "∃y. F a = Some y" by blast
next
  fix a b assume "(F -- x) a = Some b" from fmap_minus_fmap[OF this]
  show "F a = Some b" by assumption
next
  fix a b assume "(F -- (a, b)) a = Some b" 
  with fmap_minus_fmap[OF this] show False 
    unfolding fmap_minus_direct_def by auto
next
  fix a b assume "(a,b) ≠ x" and "F a = Some b"
  hence "fst x ≠ a ∨ F (fst x) ≠ Some (snd x)" by auto
  with ‹F a = Some b› show "∃y. (F -- x) a = Some y" 
    unfolding fmap_minus_direct_def by (rule_tac x = b in exI, simp)
next
  fix a b assume "(a,b) ≠ x" and "F a = Some b"
  hence "fst x ≠ a ∨ F (fst x) ≠ Some (snd x)" by auto
  with ‹F a = Some b› show "(F -- x) a = Some b" 
    unfolding fmap_minus_direct_def by simp  
qed

lemma set_fmap_minus_insert:
  fixes F :: "('a::finite * 'b)set" and  F':: "('a::finite) -~> 'b" and x
  assumes "x ∉ F" and "insert x F = set_fmap F'"
  shows "F = set_fmap (F' -- x)"
proof -
  from ‹x ∉ F› sym[OF ‹insert x F = set_fmap F'›] set_fmap_minus_iff[of F' x] 
  show ?thesis by simp
qed

lemma notin_fmap_minus: "x ∉ set_fmap ((F::(('a::finite) -~> 'b)) -- x)"
  by (auto simp: set_fmap_minus_iff)

lemma fst_notin_fmap_minus_dom:
  fixes F x and F' :: "('a::finite) -~> 'b"
  assumes "insert x F = set_fmap F'"
  shows "fst x ∉ dom (F' -- x)"
proof (rule ccontr, auto)
  fix y assume "(F' -- x) (fst x) = Some y"
  with notin_fmap_minus[of x F'] 
  have "y ≠ snd x"
    unfolding set_fmap_def by auto
  moreover
  from insert_lem[OF ‹insert x F = set_fmap F'›] 
  have "F' (fst x) = Some (snd x)"
    unfolding set_fmap_def by auto
  ultimately show False 
    using fmap_minus_fmap[OF ‹(F' -- x) (fst x) = Some y›]
    by simp
qed

lemma  set_fmap_pair: 
  "x ∈ set_fmap F ⟹ (fst x ∈ dom F ∧ snd x = the (F (fst x)))"
  by (simp add: set_fmap_def, auto)

lemma  set_fmap_inv1: 
  "⟦ fst x ∈ dom F; snd x = the (F (fst x)) ⟧ ⟹ (F -- x)(fst x ↦ snd x) = F"
proof (rule ext)
  fix xa assume "fst x ∈ dom F" and "snd x = the (F (fst x))"
  thus "((F -- x)(fst x ↦ snd x)) xa = F xa"
    unfolding fmap_minus_direct_def
    by (case_tac "xa = fst x", auto)
qed

lemma set_fmap_inv2: 
  "fst x ∉ dom F ⟹ insert x (set_fmap F) = set_fmap (F(fst x ↦ snd x))"
  unfolding set_fmap_def
proof
  assume "fst x ∉ dom F"
  thus
    "insert x {(x, y). x ∈ dom F ∧ F x = Some y} ⊆ 
    {(xa, y). xa ∈ dom (F(fst x ↦ snd x)) ∧ (F(fst x ↦ snd x)) xa = Some y}"
    by force
next
  have
    "⋀z. z ∈ {(xa, y). xa ∈ dom (F(fst x ↦ snd x)) 
                     ∧ (F(fst x ↦ snd x)) xa = Some y}
    ⟹ z ∈ insert x {(x, y). x ∈ dom F ∧ F x = Some y}"
    proof -
      fix z
      assume 
        z: "z ∈ {(xa, y). xa ∈ dom (F(fst x ↦ snd x)) 
                     ∧ (F(fst x ↦ snd x)) xa = Some y}"
      hence "z = x ∨ ((fst z) ∈ dom F ∧ F (fst z) = Some (snd z))"
      proof (cases "fst x = fst z")
        case True thus ?thesis using z by auto
      next
        case False thus ?thesis using z by auto
      qed
      thus "z ∈ insert x {(x, y). x ∈ dom F ∧ F x = Some y}" by fastforce
    qed
  thus 
    "{(xa, y). xa ∈ dom (F(fst x ↦ snd x)) ∧ (F(fst x ↦ snd x)) xa = Some y} ⊆ 
    insert x {(x, y). x ∈ dom F ∧ F x = Some y}" by auto
qed

lemma rep_fmap_base: "P (F::('a  -~> 'b)) = (pred_set_fmap P)(set_fmap F)"
  unfolding pred_set_fmap_def set_fmap_def
proof (rule_tac f = P in arg_cong)
  have 
    "⋀x. F x = 
         (λx. if x ∈ fst ` {(x, y). x ∈ dom F ∧ F x = Some y}
               then THE y. ∃z. y = Some z 
                             ∧ (x, z) ∈ {(x, y). x ∈ dom F ∧ F x = Some y}
               else None) x"
  proof auto
    fix a b
    assume "F a = Some b"
    hence "∃!x. x = Some b ∧ a ∈ dom F"
    proof (rule_tac a = "F a" in ex1I)
      assume "F a = Some b"
      thus "F a = Some b ∧ a ∈ dom F" 
        by (simp add: dom_def)
    next
      fix x assume "F a = Some b" and "x = Some b ∧ a ∈ dom F"
      thus "x = F a" by simp
    qed
    hence "(THE y. y = Some b ∧ a ∈ dom F) = Some b ∧ a ∈ dom F" 
      by (rule theI')
    thus "Some b = (THE y. y = Some b ∧ a ∈ dom F)" 
      by simp
  next
    fix x assume nin_x: "x ∉ fst ` {(x, y). x ∈ dom F ∧ F x = Some y}"
    thus "F x = None"
    proof (cases "F x")
      case None thus ?thesis by assumption
    next
      case (Some a)
      hence "x ∈ fst ` {(x, y). x ∈ dom F ∧ F x = Some y}"
        by (simp add: image_def dom_def)
      with nin_x show ?thesis by simp
    qed
  qed
  thus 
    "F = (λx. if x ∈ fst ` {(x, y). x ∈ dom F ∧ F x = Some y}
               then THE y. ∃z. y = Some z 
                             ∧ (x, z) ∈ {(x, y). x ∈ dom F ∧ F x = Some y}
               else None)"
    by (rule ext)
qed

lemma rep_fmap: 
  "∃(Fp ::('a * 'b)set) (P'::('a * 'b)set ⇒ bool). P (F::('a -~> 'b)) = P' Fp"
proof -
  from rep_fmap_base show ?thesis by blast
qed

theorem finite_fsets: "finite (F::('a::finite)set)"
proof -
  from finite_subset[OF subset_UNIV] show "finite F" by auto
qed

lemma finite_dom_fmap: "finite (dom (F::('a -~> 'b))::('a::finite)set)"
  by (rule finite_fsets)

lemma finite_fmap_ran: "finite (ran (F::(('a::finite) -~> 'b)))"
  unfolding ran_def
proof -
  from finite_dom_fmap finite_imageI 
  have "finite ((λx. the (F x)) ` (dom F))" 
    by blast
  moreover
  have "{b. ∃a. F a = Some b} = (λx. the (F x)) ` (dom F)"
    unfolding image_def dom_def by force
  ultimately
  show "finite {b. ∃a. F a = Some b}"  by simp
qed

lemma finite_fset_map: "finite (set_fmap (F::(('a::finite) -~> 'b)))"
proof -
  from finite_cartesian_product[OF finite_dom_fmap finite_fmap_ran]
  have "finite (dom F × ran F)" .
  moreover
  have "set_fmap F ⊆ dom F × ran F"
    unfolding set_fmap_def dom_def ran_def by fastforce
  ultimately
  show ?thesis using finite_subset by auto
qed

lemma rep_fmap_imp: 
  "∀F x z. x ∉ dom (F::('a -~> 'b)) ⟶ P F ⟶ P (F(x ↦ z))
  ⟹ (∀F x z. x ∉ fst ` (set_fmap F) ⟶ (pred_set_fmap P)(set_fmap F) 
        ⟶ (pred_set_fmap P) (insert (x,z) (set_fmap F)))"
proof (clarify)
  fix P F x z
  assume 
    "∀F x z. x ∉ dom (F::('a -~> 'b)) ⟶ P F ⟶ P (F(x ↦ z))" and
    "x ∉ fst ` set_fmap F" and "(pred_set_fmap P)(set_fmap F)"
  hence notin: "x ∉ dom F"
    unfolding set_fmap_def image_def dom_def by simp
  moreover
  from ‹pred_set_fmap P (set_fmap F)› have "P F" by (simp add: rep_fmap_base)
  ultimately
  have "P (F(x ↦ z))" using ‹∀F x z. x ∉ dom F ⟶ P F ⟶ P (F(x ↦ z))› 
    by blast
  hence "(pred_set_fmap P) (set_fmap (F(x ↦ z)))"
    by (simp add: rep_fmap_base)
  moreover
  from notin 
  have "(insert (x,z) (set_fmap F)) = (set_fmap (F(fst (x,z) ↦ snd (x,z))))"
    by (simp add: set_fmap_inv2)
  ultimately
  show "(pred_set_fmap P) (insert (x,z) (set_fmap F))" by simp
qed

lemma empty_dom: 
  fixes g
  assumes "{} = dom g"
  shows "g = Map.empty"
proof 
  fix x from assms show "g x = None" by auto
qed

theorem fmap_induct[rule_format, case_names empty insert]:
  fixes  P  :: "(('a :: finite) -~> 'b) ⇒ bool" and  F' :: "('a  -~> 'b)"
  assumes 
  "P Map.empty" and
  "∀(F::('a -~> 'b)) x z. x ∉ dom F ⟶ P F ⟶ P (F(x ↦ z))"
  shows "P F'"
proof -
  {
    fix F :: "('a × 'b) set" assume "finite F"
    hence "∀F'. F = set_fmap F' ⟶ pred_set_fmap P (set_fmap F')"
    proof (induct F)
      case empty thus ?case
      proof (intro strip)
        fix F' :: "'a -~> 'b" assume "{} = set_fmap F'"
        hence "⋀a. F' a = None" unfolding set_fmap_def by auto
        hence "F' = Map.empty" by (rule ext)
        with ‹P Map.empty› rep_fmap_base[of P Map.empty] 
        show "pred_set_fmap P (set_fmap F')" by simp
      qed
    next
      case (insert x Fa) thus ?case
      proof (intro strip)
        fix Fb :: "'a -~> 'b"
        assume "insert x Fa = set_fmap Fb"
        from 
          set_fmap_minus_insert[OF ‹x ∉ Fa› this]
          ‹∀F'. Fa = set_fmap F' ⟶ pred_set_fmap P (set_fmap F')› 
          rep_fmap_base[of P "Fb -- x"]
        have "P (Fb -- x)" by blast
        with 
          ‹∀F x z. x ∉ dom F ⟶ P F ⟶ P (F(x ↦ z))› 
          fst_notin_fmap_minus_dom[OF ‹insert x Fa = set_fmap Fb›]
        have "P ((Fb -- x)(fst x ↦ snd x))" by blast
        moreover
        from 
          insert_absorb[OF insert_lem[OF ‹insert x Fa = set_fmap Fb›]]
          set_fmap_minus_iff[of Fb x]
          set_fmap_inv2[OF 
           fst_notin_fmap_minus_dom[OF ‹insert x Fa = set_fmap Fb›]] 
        have "set_fmap Fb = set_fmap ((Fb -- x)(fst x ↦ snd x))"
          by simp
        ultimately
        show "pred_set_fmap P (set_fmap Fb)" 
          using rep_fmap_base[of P "(Fb -- x)(fst x ↦ snd x)"]
          by simp
      qed
    qed
  } 
  from this[OF finite_fset_map[of F']]
       rep_fmap_base[of P F']
  show "P F'" by blast
qed

lemma fmap_induct3[consumes 2, case_names empty insert]:
  "⋀(F2::('a::finite) -~> 'b) (F3::('a -~> 'b)).
   ⟦ dom (F1::('a -~> 'b)) = dom F2; dom F3 = dom F1; 
     P Map.empty Map.empty Map.empty;
     ⋀x a b c (F1::('a -~> 'b)) (F2::('a -~> 'b)) (F3::('a -~> 'b)).
     ⟦ P F1 F2 F3; dom F1 = dom F2; dom F3 = dom F1; x ∉ dom F1 ⟧
     ⟹ P (F1(x ↦ a)) (F2(x ↦ b)) (F3(x ↦ c)) ⟧
  ⟹ P F1 F2 F3"
proof (induct F1 rule: fmap_induct)
  case empty
  from ‹dom Map.empty = dom F2› have "F2 = Map.empty" by (simp add: empty_dom)
  moreover
  from ‹dom F3 = dom Map.empty› have "F3 = Map.empty" by (simp add: empty_dom)
  ultimately
  show ?case using ‹P Map.empty Map.empty Map.empty› by simp
next
  case (insert F x y) thus ?case
  proof (cases "F2 = Map.empty")
    case True with ‹dom (F(x ↦ y)) = dom F2› 
    have "dom (F(x ↦ y)) = {}" by auto
    thus ?thesis by auto
  next
    case False thus ?thesis
    proof (cases "F3 = Map.empty")
      case True with ‹dom F3 = dom (F(x ↦ y))› 
      have "dom (F(x ↦ y)) = {}" by simp
      thus ?thesis by simp
    next
      case False thus ?thesis
      proof -
        from ‹F2 ≠ Map.empty› 
        have "∀l∈dom F2. ∃f'. F2 = f'(l ↦ the (F2 l)) ∧ l ∉ dom f'"
          by (simp add: one_more_dom)
        moreover
        from ‹dom (F(x ↦ y)) = dom F2› have "x ∈ dom F2" by force
        ultimately have "∃f'. F2 = f'(x ↦ the (F2 x)) ∧ x ∉ dom f'" by blast
        then obtain F2' where "F2 = F2'(x ↦ the (F2 x))" and "x ∉ dom F2'" 
          by auto

        from ‹F3 ≠ Map.empty› 
        have "∀l∈dom F3. ∃f'. F3 = f'(l ↦ the (F3 l)) ∧ l ∉ dom f'"
          by (simp add: one_more_dom)
        moreover from ‹dom F3 = dom (F(x ↦ y))› have "x ∈ dom F3" by force
        ultimately have "∃f'. F3 = f'(x ↦ the (F3 x)) ∧ x ∉ dom f'" by blast
        then obtain F3' where "F3 = F3'(x ↦ the (F3 x))" and "x ∉ dom F3'" 
          by auto

        show ?thesis
        proof -
          from ‹dom (F(x ↦ y)) = dom F2› ‹F2 = F2'(x ↦ the (F2 x))›
          have "dom (F(x ↦ y)) = dom (F2'(x ↦ the (F2 x)))" by simp
          with ‹x ∉ dom F› ‹x ∉ dom F2'› have "dom F = dom F2'" by auto
          
          moreover
          from ‹dom F3 = dom (F(x ↦ y))› ‹F3 = F3'(x ↦ the (F3 x))›
          have "dom (F(x ↦ y)) = dom (F3'(x ↦ the (F3 x)))" by simp
          with ‹x ∉ dom F› ‹x ∉ dom F3'› have "dom F3' = dom F" by auto

          ultimately have "P F F2' F3'" using insert by simp

          with 
            ‹⋀F1 F2 F3 x a b c.
              ⟦ P F1 F2 F3; dom F1 = dom F2; dom F3 = dom F1; x ∉ dom F1 ⟧
              ⟹ P (F1(x ↦ a)) (F2(x ↦ b)) (F3(x ↦ c))›
            ‹dom F = dom F2'›
            ‹dom F3' = dom F›
            ‹x ∉ dom F›
          have "P (F(x ↦ y)) (F2'(x ↦ the (F2 x))) (F3'(x ↦ the (F3 x)))" 
            by simp
          with ‹F2 = F2'(x ↦ the (F2 x))› ‹F3 = F3'(x ↦ the (F3 x))›
          show "P (F(x ↦ y)) F2 F3" by simp
        qed
      qed
    qed
  qed
qed

lemma fmap_ex_cof2:
  "⋀(P::'c ⇒ 'c ⇒ 'b option ⇒ 'b option ⇒ 'a ⇒ bool)
     (f'::('a::finite) -~> 'b).
  ⟦ dom f' = dom (f::('a -~> 'b)); 
    ∀l∈dom f. (∃L. finite L 
                  ∧ (∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
                      ⟶ P s p (f l) (f' l) l)) ⟧
  ⟹ ∃L. finite L ∧ (∀l∈dom f. (∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p 
                                   ⟶ P s p (f l) (f' l) l))"
proof (induct f rule: fmap_induct)
  case empty thus ?case by blast
next
  case (insert f l t P f') note imp = this(2) and pred = this(4)
  define pred_cof where "pred_cof L b b' l ⟷ (∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p ⟶ P s p b b' l)"
    for L b b' l
  from 
    map_upd_nonempty[of f l t] ‹dom f' = dom (f(l ↦ t))›
    one_more_dom[of l f']
  obtain f'a where 
    "f' = f'a(l ↦ the(f' l))" and "l ∉ dom f'a" and
    "dom (f'a(l ↦ the(f' l))) = dom (f(l ↦ t))"
    by auto
  from ‹l ∉ dom f›
  have
    fla: "∀la∈dom f. f la = (f(l ↦ t)) la" and
    "∀la∈dom f. f'a la = (f'a(l ↦ the(f' l))) la"
    by auto
  with ‹f' = f'a(l ↦ the(f' l))› 
  have f'ala: "∀la∈dom f. f'a la = f' la" by simp
  have "∃L. finite L ∧ (∀la∈dom f. pred_cof L (f la) (f'a la) la)"
    unfolding pred_cof_def
  proof 
    (intro imp[OF insert_dom_less_eq[OF ‹l ∉ dom f'a› ‹l ∉ dom f› 
                                        ‹dom (f'a(l ↦ the(f' l))) = dom (f(l ↦ t))›]],
      intro strip)
    fix la assume "la ∈ dom f"
    with fla f'ala 
    have 
      "la ∈ dom (f(l ↦ t))" and 
      "f la = (f(l ↦ t)) la" and "f'a la = f' la"
      by auto
    with pred
    show "∃L. finite L ∧ (∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p ⟶ P s p (f la) (f'a la) la)"
      by (elim ssubst, blast)
  qed
  with fla f'ala obtain L where 
    "finite L" and predf: "∀la∈dom f. pred_cof L ((f(l ↦ t)) la) (f' la) la"
    by auto
  moreover
  have "l ∈ dom (f(l ↦ t))" by simp
  with pred obtain L' where
    "finite L'" and predfl: "pred_cof L' ((f(l ↦ t)) l) (f' l) l"
    unfolding pred_cof_def
    by blast
  ultimately show ?case
  proof (rule_tac x = "L ∪ L'" in exI, 
      intro conjI, simp, intro strip)
    fix s p la assume 
      sp: "s ∉ L ∪ L' ∧ p ∉ L ∪ L' ∧ s ≠ p" and indom: "la ∈ dom (f(l ↦ t))"
    show "P s p ((f(l ↦ t)) la) (f' la) la"
    proof (cases "la = l")
      case True with sp predfl show ?thesis 
        unfolding pred_cof_def
        by simp
    next
      case False with indom sp predf show ?thesis 
        unfolding pred_cof_def
        by force
    qed
  qed
qed

lemma fmap_ex_cof:
  fixes
  P :: "'c ⇒ 'c ⇒ 'b option ⇒ ('a::finite) ⇒ bool"
  assumes
  "∀l∈dom (f::('a -~> 'b)).
  (∃L. finite L ∧ (∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p ⟶ P s p (f l) l))"
  shows
  "∃L. finite L ∧ (∀l∈dom f. (∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p ⟶ P s p (f l) l))"
  using assms fmap_ex_cof2[of f f  "λs p b b' l. P s p b l"] by auto

lemma fmap_ball_all2:
  fixes 
  Px :: "'c ⇒ 'd ⇒ bool" and 
  P :: "'c ⇒ 'd ⇒ 'b option ⇒ bool"
  assumes
  "∀l∈dom (f::('a::finite) -~> 'b). ∀(x::'c) (y::'d). Px x y ⟶ P x y (f l)"
  shows
  "∀x y. Px x y ⟶ (∀l∈dom f. P x y (f l))"
proof (intro strip)
  fix x y l assume "Px x y" and "l ∈ dom f"
  with assms show "P x y (f l)" by blast
qed

lemma fmap_ball_all2':
  fixes 
  Px :: "'c ⇒ 'd ⇒ bool" and 
  P :: "'c ⇒ 'd ⇒ 'b option ⇒ ('a::finite) ⇒ bool"
  assumes
  "∀l∈dom (f::('a -~> 'b)). ∀(x::'c) (y::'d). Px x y ⟶ P x y (f l) l"
  shows
  "∀x y. Px x y ⟶ (∀l∈dom f. P x y (f l) l)"
proof (intro strip)
  fix x y l assume "Px x y" and "l ∈ dom f"
  with assms show "P x y (f l) l" by blast
qed

lemma fmap_ball_all3:
  fixes 
  Px :: "'c ⇒ 'd ⇒ 'e ⇒ bool" and 
  P :: "'c ⇒ 'd ⇒ 'e ⇒ 'b option ⇒ 'b option ⇒ bool" and
  f :: "('a::finite) -~> 'b" and f' :: "'a -~> 'b"
  assumes
  "dom f' = dom f" and
  "∀l∈dom f.
     ∀(x::'c) (y::'d) (z::'e). Px x y z ⟶ P x y z (f l) (f' l)"
  shows
  "∀x y z. Px x y z ⟶ (∀l∈dom f. P x y z (f l) (f' l))"
proof (intro strip)
  fix x y z l assume "Px x y z" and "l ∈ dom f"
  with assms show "P x y z (f l) (f' l)" by blast
qed

lemma fmap_ball_all4':
  fixes 
  Px :: "'c ⇒ 'd ⇒ 'e ⇒ 'f ⇒ bool" and 
  P :: "'c ⇒ 'd ⇒ 'e ⇒ 'f ⇒ 'b option ⇒ ('a::finite) ⇒ bool"
  assumes
  "∀l∈dom (f::('a -~> 'b)). 
    ∀(x::'c) (y::'d) (z::'e) (a::'f). Px x y z a ⟶ P x y z a (f l) l"
  shows
  "∀x y z a. Px x y z a ⟶ (∀l∈dom f. P x y z a (f l) l)"
proof (intro strip)
  fix x y z a l assume "Px x y z a" and "l ∈ dom f"
  with assms show "P x y z a (f l) l" by blast
qed

end