# Theory FMap

Up to index of Isabelle/HOL/Locally-Nameless-Sigma

theory FMap
imports ListPre
`(*  Title:      FMap.thy    Author:     Ludovic Henrio and Florian Kammuller, 2006Finite maps for Sigma-calculusIdea use axiomatic type classes to preserveusability of datatype afterwards, i.e. definitionof an object as a finite map of labels to fields ina datatype.*)header {* Finite maps with axclasses *}theory FMap imports ListPre begintype_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 autonext  assume "P {}" thus "P {}" by simpnext  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 simpqedtheorem fmap_unique: "x = y ==> (f::('a,'b)fmap) x = f y"  by (erule ssubst, rule refl)theorem fmap_case:  "(F::('a -~> 'b)) = empty ∨ (∃x y (F'::('a -~> 'b)). F = F'(x \<mapsto> y))"proof (cases "F = empty")  case True thus ?thesis by (rule disjI1)next  case False thus ?thesis  proof (simp)    from `F ≠ 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 = empty" by (rule ext)    qed    thus "∃x y F'. F = F'(x \<mapsto> y)"    proof      fix x assume "F x ≠ None"      hence "!!y. F y = (F(x \<mapsto> the (F x))) y" by auto      hence "F = F(x \<mapsto> the (F x))" by (rule ext)      thus ?thesis by auto    qed  qedqed(* define the witness as a constant function so it may be used in the proof ofthe 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 autolemma 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 simpnext  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  qedqedlemma 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 blastnext  fix a b assume "(F -- x) a = Some b" from fmap_minus_fmap[OF this]  show "F a = Some b" by assumptionnext  fix a b assume "(F -- (a, b)) a = Some b"   with fmap_minus_fmap[OF this] show False     unfolding fmap_minus_direct_def by autonext  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  qedlemma 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 simpqedlemma 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 simpqedlemma  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 \<mapsto> 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 \<mapsto> snd x)) xa = F xa"    unfolding fmap_minus_direct_def    by (case_tac "xa = fst x", auto)qedlemma set_fmap_inv2:   "fst x ∉ dom F ==> insert x (set_fmap F) = set_fmap (F(fst x \<mapsto> snd x))"  unfolding set_fmap_defproof  assume "fst x ∉ dom F"  thus    "insert x {(x, y). x ∈ dom F ∧ F x = Some y} ⊆     {(xa, y). xa ∈ dom (F(fst x \<mapsto> snd x)) ∧ (F(fst x \<mapsto> snd x)) xa = Some y}"    by forcenext  have    "!!z. z ∈ {(xa, y). xa ∈ dom (F(fst x \<mapsto> snd x))                      ∧ (F(fst x \<mapsto> 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 \<mapsto> snd x))                      ∧ (F(fst x \<mapsto> 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 \<mapsto> snd x)) ∧ (F(fst x \<mapsto> snd x)) xa = Some y} ⊆     insert x {(x, y). x ∈ dom F ∧ F x = Some y}" by autoqedlemma rep_fmap_base: "P (F::('a  -~> 'b)) = (pred_set_fmap P)(set_fmap F)"  unfolding pred_set_fmap_def set_fmap_defproof (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)qedlemma 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 blastqedtheorem finite_fsets: "finite (F::('a::finite)set)"proof -  from finite_subset[OF subset_UNIV] show "finite F" by autoqedlemma 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_defproof -  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 simpqedlemma 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 autoqedlemma rep_fmap_imp:   "∀F x z. x ∉ dom (F::('a -~> 'b)) --> P F --> P (F(x \<mapsto> 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 \<mapsto> 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 \<mapsto> z))" using `∀F x z. x ∉ dom F --> P F --> P (F(x \<mapsto> z))`     by blast  hence "(pred_set_fmap P) (set_fmap (F(x \<mapsto> z)))"    by (simp add: rep_fmap_base)  moreover  from notin   have "(insert (x,z) (set_fmap F)) = (set_fmap (F(fst (x,z) \<mapsto> snd (x,z))))"    by (simp add: set_fmap_inv2)  ultimately  show "(pred_set_fmap P) (insert (x,z) (set_fmap F))" by simpqedlemma empty_dom:   fixes g  assumes "{} = dom g"  shows "g = empty"proof   fix x from assms show "g x = None" by autoqedtheorem fmap_induct[rule_format, case_names empty insert]:  fixes  P  :: "(('a :: finite) -~> 'b) => bool" and  F' :: "('a  -~> 'b)"  assumes   "P empty" and  "∀(F::('a -~> 'b)) x z. x ∉ dom F --> P F --> P (F(x \<mapsto> 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' = empty" by (rule ext)        with `P empty` rep_fmap_base[of P 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 \<mapsto> z))`           fst_notin_fmap_minus_dom[OF `insert x Fa = set_fmap Fb`]        have "P ((Fb -- x)(fst x \<mapsto> 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 \<mapsto> snd x))"          by simp        ultimately        show "pred_set_fmap P (set_fmap Fb)"           using rep_fmap_base[of P "(Fb -- x)(fst x \<mapsto> snd x)"]          by simp      qed    qed  }   from this[OF finite_fset_map[of F']]       rep_fmap_base[of P F']  show "P F'" by blastqedlemma 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 empty empty 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 \<mapsto> a)) (F2(x \<mapsto> b)) (F3(x \<mapsto> c)) |]  ==> P F1 F2 F3"proof (induct F1 rule: fmap_induct)  case empty  from `dom empty = dom F2` have "F2 = empty" by (simp add: empty_dom)  moreover  from `dom F3 = dom empty` have "F3 = empty" by (simp add: empty_dom)  ultimately  show ?case using `P empty empty empty` by simpnext  case (insert F x y) thus ?case  proof (cases "F2 = empty")    case True with `dom (F(x \<mapsto> y)) = dom F2`     have "dom (F(x \<mapsto> y)) = {}" by auto    thus ?thesis by auto  next    case False thus ?thesis    proof (cases "F3 = empty")      case True with `dom F3 = dom (F(x \<mapsto> y))`       have "dom (F(x \<mapsto> 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 \<mapsto> the (F2 l)) ∧ l ∉ dom f'"          by (simp add: one_more_dom)        moreover        from `dom (F(x \<mapsto> y)) = dom F2` have "x ∈ dom F2" by force        ultimately have "∃f'. F2 = f'(x \<mapsto> the (F2 x)) ∧ x ∉ dom f'" by blast        then obtain F2' where "F2 = F2'(x \<mapsto> the (F2 x))" and "x ∉ dom F2'"           by auto        from `F3 ≠ Map.empty`         have "∀l∈dom F3. ∃f'. F3 = f'(l \<mapsto> the (F3 l)) ∧ l ∉ dom f'"          by (simp add: one_more_dom)        moreover from `dom F3 = dom (F(x \<mapsto> y))` have "x ∈ dom F3" by force        ultimately have "∃f'. F3 = f'(x \<mapsto> the (F3 x)) ∧ x ∉ dom f'" by blast        then obtain F3' where "F3 = F3'(x \<mapsto> the (F3 x))" and "x ∉ dom F3'"           by auto        show ?thesis        proof -          from `dom (F(x \<mapsto> y)) = dom F2` `F2 = F2'(x \<mapsto> the (F2 x))`          have "dom (F(x \<mapsto> y)) = dom (F2'(x \<mapsto> 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 \<mapsto> y))` `F3 = F3'(x \<mapsto> the (F3 x))`          have "dom (F(x \<mapsto> y)) = dom (F3'(x \<mapsto> 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 \<mapsto> a)) (F2(x \<mapsto> b)) (F3(x \<mapsto> c))`            `dom F = dom F2'`            `dom F3' = dom F`            `x ∉ dom F`          have "P (F(x \<mapsto> y)) (F2'(x \<mapsto> the (F2 x))) (F3'(x \<mapsto> the (F3 x)))"             by simp          with `F2 = F2'(x \<mapsto> the (F2 x))` `F3 = F3'(x \<mapsto> the (F3 x))`          show "P (F(x \<mapsto> y)) F2 F3" by simp        qed      qed    qed  qedqedlemma 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 blastnext  case (insert f l t P f') note imp = this(2) and pred = this(4)  def pred_cof ≡ "λL b b' l. ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p --> P s p b b' l"  from     map_upd_nonempty[of f l t] `dom f' = dom (f(l \<mapsto> t))`    one_more_dom[of l f']  obtain f'a where     "f' = f'a(l \<mapsto> the(f' l))" and "l ∉ dom f'a" and    "dom (f'a(l \<mapsto> the(f' l))) = dom (f(l \<mapsto> t))"    by auto  from `l ∉ dom f`  have    fla: "∀la∈dom f. f la = (f(l \<mapsto> t)) la" and    "∀la∈dom f. f'a la = (f'a(l \<mapsto> the(f' l))) la"    by auto  with `f' = f'a(l \<mapsto> 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 \<mapsto> the(f' l))) = dom (f(l \<mapsto> t))`]],      intro strip)    fix la assume "la ∈ dom f"    with fla f'ala     have       "la ∈ dom (f(l \<mapsto> t))" and       "f la = (f(l \<mapsto> 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 \<mapsto> t)) la) (f' la) la"    by auto  moreover  have "l ∈ dom (f(l \<mapsto> t))" by simp  with pred obtain L' where    "finite L'" and predfl: "pred_cof L' ((f(l \<mapsto> 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 \<mapsto> t))"    show "P s p ((f(l \<mapsto> 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  qedqedlemma 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 autolemma 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 blastqedlemma 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 blastqedlemma 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 blastqedlemma 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 blastqedend`