Theory MiscTools

(*
Auction Theory Toolbox (http://formare.github.io/auctions/)

Authors:
* Marco B. Caminati http://caminati.co.nr
* Manfred Kerber <mnfrd.krbr@gmail.com>
* Christoph Lange <math.semantic.web@gmail.com>
* Colin Rowat <c.rowat@bham.ac.uk>

Dually licenced under
* Creative Commons Attribution (CC-BY) 3.0
* ISC License (1-clause BSD License)
See LICENSE file for details
(Rationale for this dual licence: http://arxiv.org/abs/1107.3212)
*)


section ‹Toolbox of various definitions and theorems about sets, relations and lists›

theory MiscTools 

imports 
"HOL-Library.Discrete"
"HOL-Library.Code_Target_Nat"
"HOL-Library.Indicator_Function"
Argmax
RelationProperties

begin

lemmas restrict_def = RelationOperators.restrict_def

subsection ‹Facts and notations about relations, sets and functions.›

(* We use as alternative notation for paste instead of +* also +< and overload this with the next definition *)
notation paste (infix "+<" 75)

text ‹‹+<› abbreviation permits to shorten the notation for altering a function f in a single point by giving a pair (a, b) so that the new function has value b with argument a.›

abbreviation singlepaste
  where "singlepaste f pair == f +* {(fst pair, snd pair)}"
  notation singlepaste (infix "+<" 75)
(* Type of g in f +< g should avoid ambiguities *)

text ‹‹--› abbreviation permits to shorten the notation for considering a function outside a single point.›

abbreviation singleoutside (infix "--" 75)
  where "f -- x ≡ f outside {x}"

text ‹Turns a HOL function into a set-theoretical function›

definition (*Graph :: "('a => 'b) => ('a × 'b) set" where *) 
  "Graph f = {(x, f x) | x . True}"

text ‹Inverts @{term Graph} (which is equivalently done by @{term eval_rel}).›
(* Assume (x, y) is in R. Apply R to x, i.e., R ,, x,  will result in y assumed y is unique. *)  

definition
  "toFunction R = (λ x . (R ,, x))"

(* toFunction = eval_rel *)
lemma 
  "toFunction = eval_rel" 
  using toFunction_def by blast

lemma lm001: 
  "((P ∪ Q) || X) = ((P || X) ∪ (Q||X))" 
  unfolding restrict_def by blast

text ‹update behaves like P +* Q (paste), but without enlarging P's Domain. update is the set theoretic equivalent of the lambda function update @{term fun_upd}›

definition update 
  where "update P Q = P +* (Q || (Domain P))"
  notation update (infix "+^" 75)

(* The operator runiqer will make out of an arbitrary relation a function by making a choice to all those elements in the domain for which the value is not unique by applying the axiom of choice. *)
definition runiqer  :: "('a × 'b) set => ('a × 'b) set"
  where "runiqer R = { (x, THE y. y ∈ R `` {x})| x. x ∈ Domain R }"

text ‹@{term graph} is like @{term Graph}, but with a built-in restriction to a given set @{term X}.
This makes it computable for finite X, whereas @{term "Graph f || X"} is not computable. 
Duplicates the eponymous definition found in ‹Function_Order›, which is otherwise not needed.›

definition graph 
  where "graph X f = {(x, f x) | x. x ∈ X}" 

lemma lm002: 
  assumes "runiq R" 
  shows "R ⊇ graph (Domain R) (toFunction R)" 
  unfolding graph_def toFunction_def
  using assms graph_def toFunction_def eval_runiq_rel by fastforce

lemma lm003: 
  assumes "runiq R" 
  shows "R ⊆ graph (Domain R) (toFunction R)" 
  unfolding graph_def toFunction_def
  using assms eval_runiq_rel runiq_basic Domain.DomainI mem_Collect_eq subrelI by fastforce

lemma lm004: 
  assumes "runiq R" 
  shows "R = graph (Domain R) (toFunction R)"
  using assms lm002 lm003 by fast

lemma domainOfGraph: 
  "runiq(graph X f) & Domain(graph X f)=X" 
  unfolding graph_def 
  using rightUniqueRestrictedGraph by fast

(* The following definition gives the image of a relation R for a fixed element x. It is equivalent to eval_rel for right unique R, but more general since it determines values even when R is not right unique. *)
abbreviation "eval_rel2 (R::('a × ('b set)) set) (x::'a) == ⋃ (R``{x})"
  notation eval_rel2 (infix ",,," 75)

lemma imageEquivalence: 
  assumes "runiq (f::(('a × ('b set)) set))" "x ∈ Domain f" 
  shows "f,,x = f,,,x"
  using assms Image_runiq_eq_eval cSup_singleton by metis

(* UNIV is the universal set containing everything of the given type. It is defined in Set.thy.*)
lemma lm005: 
  "Graph f=graph UNIV f" 
  unfolding Graph_def graph_def by simp

lemma graphIntersection: 
  "graph (X ∩ Y) f ⊆ ((graph X f) || Y)" 
  unfolding graph_def 
  using Int_iff mem_Collect_eq RelationOperators.restrict_ext subrelI by auto

definition runiqs 
  where "runiqs={f. runiq f}"

lemma outsideOutside: 
  "((P outside X) outside Y) = P outside (X∪Y)" 
  unfolding Outside_def by blast

corollary lm006: 
  "((P outside X) outside X) = P outside X" 
  using outsideOutside by force 

lemma lm007: 
  assumes "(X ∩ Domain P) ⊆ Domain Q" 
  shows "P +* Q = (P outside X) +* Q" 
  unfolding paste_def Outside_def using assms by blast

corollary lm008: 
  "P +* Q = (P outside (Domain Q)) +* Q" 
  using lm007 by fast

corollary outsideUnion: 
  "R = (R outside {x}) ∪ ({x} × (R `` {x}))" 
  using restrict_to_singleton outside_union_restrict by metis

lemma lm009: 
  "P = P ∪ {x}×P``{x}" 
  by (metis outsideUnion sup.right_idem)

corollary lm010: 
  "R = (R outside {x}) +* ({x} × (R `` {x}))" 
  by (metis paste_outside_restrict restrict_to_singleton)

lemma lm011: 
  "R ⊆ R +* ({x} × (R``{x}))" 
  using lm010 lm008 paste_def Outside_def by fast

lemma lm012: 
  "R ⊇ R+*({x} × (R``{x}))" 
  by (metis Un_least Un_upper1 outside_union_restrict paste_def 
            restrict_to_singleton restriction_is_subrel)

lemma lm013: 
  "R = R +* ({x} × (R``{x}))" 
  using lm011 lm012 by force

lemma rightUniqueTrivialCartes: 
  assumes "trivial Y" 
  shows "runiq (X × Y)" 
  using assms runiq_def Image_subset lm013 trivial_subset lm011 by (metis(no_types))

(* Two constant functions can be combined to a function *)
lemma lm014: 
  "runiq ((X × {x}) +* (Y × {y}))" 
  using rightUniqueTrivialCartes trivial_singleton runiq_paste2 by metis

lemma lm015: 
  "(P || (X ∩ Y)) ⊆ (P||X)    &    P outside (X ∪ Y) ⊆ P outside X"
  by (metis doubleRestriction le_sup_iff outsideOutside outside_union_restrict subset_refl) 

lemma lm016: 
  "P || X ⊆ (P||(X ∪ Y))       &    P outside X ⊆ P outside (X ∩ Y)" 
  using lm015 distrib_sup_le sup_idem le_inf_iff subset_antisym sup_commute
  by (metis sup_ge1)

lemma lm017: 
  "P``(X ∩ Domain P) = P``X" 
  by blast

lemma cardinalityOneSubset: 
  assumes "card X=1" and "X ⊆ Y" 
  shows "Union X ∈ Y" 
  using assms cardinalityOneTheElemIdentity by (metis cSup_singleton insert_subset)

lemma cardinalityOneTheElem: 
  assumes "card X=1" "X ⊆ Y" 
  shows "the_elem X ∈ Y" 
  using assms by (metis (full_types) insert_subset cardinalityOneTheElemIdentity)

lemma lm018: 
  "(R outside X1) outside X2 = (R outside X2) outside X1" 
  by (metis outsideOutside sup_commute)




subsection ‹Ordered relations›

(* note that card ❙X≥1 means in Isabelle that X is finite and not empty *)
lemma lm019: 
  assumes "card X≥1" "∀x∈X. y > x" 
  shows "y > Max X" 
  using assms by (metis (poly_guards_query) Max_in One_nat_def card_eq_0_iff lessI not_le)

(* assume the function f has a maximum in mx *)
lemma lm020: 
  assumes "finite X" "mx ∈ X" "f x < f mx" 
  shows"x ∉ argmax f X" 
  using assms not_less by fastforce

lemma lm021: 
  assumes "finite X" "mx ∈ X" "∀x ∈ X-{mx}. f x < f mx" 
  shows "argmax f X ⊆ {mx}"
  using assms mk_disjoint_insert by force

lemma lm022: 
  assumes "finite X" "mx ∈ X" "∀x ∈ X-{mx}. f x < f mx" 
  shows "argmax f X = {mx}" 
  using assms lm021 by (metis argmax_non_empty_iff equals0D subset_singletonD)

(* The following corollary is essentially the same as lm022, however, is simplifies a proof in UniformTieBreaking.thy *)
corollary argmaxProperty: 
  "(finite X & mx ∈ X & (∀aa ∈ X-{mx}. f aa < f mx)) ⟶ argmax f X = {mx}"
  using lm022 by metis

corollary lm023: 
  assumes "finite X" "mx ∈ X" "∀x ∈ X. x ≠ mx ⟶ f x < f mx" 
  shows "argmax f X = {mx}"
  using assms lm022 by (metis Diff_iff insertI1)

lemma lm024: 
  assumes "f ∘ g = id" 
  shows "inj_on g UNIV" using assms 
  by (metis inj_on_id inj_on_imageI2)

(* Note that Pow X is the powerset of X *)
lemma lm025: 
  assumes "inj_on f X" 
  shows "inj_on (image f) (Pow X)"
  using assms inj_on_image_eq_iff inj_onI PowD by (metis (mono_tags, lifting))

lemma injectionPowerset: 
  assumes "inj_on f Y" "X ⊆ Y" 
  shows "inj_on (image f) (Pow X)"
  using assms lm025 by (metis subset_inj_on)

(* the finest possible partition of X, e.g., X = {1, 2, 3} goes to {{1}, {2}, {3}}. *)
definition finestpart 
  where "finestpart X = (%x. {x}) ` X"

lemma finestPart: 
  "finestpart X = {{x}|x . x∈X}" 
  unfolding finestpart_def by blast

lemma finestPartUnion: 
  "X=⋃ (finestpart X)" 
  using finestPart by auto

lemma lm026: 
  "Union ∘ finestpart = id" 
  using finestpart_def finestPartUnion by fastforce

lemma lm027: 
  "inj_on Union (finestpart ` UNIV)" 
  using lm026 by (metis inj_on_id inj_on_imageI)

lemma nonEqualitySetOfSets: 
  assumes "X ≠ Y" 
  shows "{{x}| x. x ∈ X} ≠ {{x}| x. x ∈ Y}" 
  using assms by auto

corollary lm028: 
  "inj_on finestpart UNIV" 
  using nonEqualitySetOfSets finestPart by (metis (lifting, no_types) injI)

(* E.g. in the following example, with X = {{1}, {1,2}}, x can be {1} and {1,2} and Y is {{1}} and {{1},{2}}, that is, the lefthand and righthand sides evaluate to {{1},{2}} *)
lemma unionFinestPart: 
  "{Y | Y. ∃x.((Y ∈ finestpart x) ∧ (x ∈ X))} = ⋃(finestpart`X)" 
  by auto

(* Now we specialize the previous lemma to the situation where X consists of a relation (that is is a set of pairs) *)
lemma rangeSetOfPairs: 
  "Range {(fst pair, Y)| Y pair. Y ∈ finestpart (snd pair) & pair ∈ X} = 
   {Y. ∃x. ((Y ∈ finestpart x) ∧ (x ∈ Range X))}" 
  by auto

(* Further specialization to a singleton for Y *)
lemma setOfPairsEquality: 
  "{(fst pair, {y})| y pair. y ∈ snd pair & pair ∈ X} = 
   {(fst pair, Y)| Y pair. Y ∈ finestpart (snd pair) & pair ∈ X}"
  using finestpart_def by fastforce

lemma setOfPairs: 
  "{(fst pair, {y})| y. y ∈  snd pair} = 
   {fst pair} × {{y}| y. y ∈ snd pair}" 
  by fastforce

lemma lm029: 
  "x ∈ X = ({x} ∈ finestpart X)" 
  using finestpart_def by force

lemma pairDifference: 
  "{(x,X)}-{(x,Y)} = {x}×({X}-{Y})" 
  by blast

lemma lm030: 
  assumes "⋃ P = X" 
  shows "P ⊆ Pow X" 
  using assms by blast

lemma lm031: 
  "argmax f {x} = {x}" 
  by auto

lemma sortingSameSet: 
  assumes "finite X" 
  shows "set (sorted_list_of_set X) = X" 
  using assms by simp

(* We assume for the next lemma that f has value in numbers, and sum f A is
   sum f(x) for x in A. *)
lemma lm032: 
  assumes "finite A" 
  shows "sum f A = sum f (A ∩ B) + sum f (A - B)" 
  using assms by (metis DiffD2 Int_iff Un_Diff_Int Un_commute finite_Un sum.union_inter_neutral)

corollary sumOutside: 
  assumes "finite g" 
  shows "sum f g = sum f (g outside X) + (sum f (g||X))" 
  unfolding Outside_def restrict_def using assms add.commute inf_commute lm032 by (metis)

lemma lm033: 
  assumes "(Domain P ⊆ Domain Q)" 
  shows "(P +* Q) = Q"
  unfolding paste_def Outside_def using assms by fast

lemma lm034: 
  assumes "(P +* Q=Q)" 
  shows "(Domain P ⊆ Domain Q)"
  using assms paste_def Outside_def by blast

lemma lm035: 
  "(Domain P ⊆ Domain Q) = (P +* Q=Q)" 
  using lm033 lm034 by metis

lemma 
  "(P||(Domain Q)) +* Q = Q" 
  by (metis Int_lower2 restrictedDomain lm035)

lemma lm036: 
  "P||X   =   P outside (Domain P - X)" 
  using Outside_def restrict_def by fastforce

lemma lm037: 
  "(P outside X) ⊆    P || ((Domain P)-X)" 
  using lm036 lm016 by (metis Int_commute restrictedDomain outside_reduces_domain)

lemma lm038: 
  "Domain (P outside X) ∩ Domain (Q || X) = {}" 
  using lm036
  by (metis Diff_disjoint Domain_empty_iff Int_Diff inf_commute restrictedDomain     
            outside_reduces_domain restrict_empty)

lemma lm039: 
  "(P outside X) ∩ (Q || X) = {}" 
  using lm038 by fast

lemma lm040: 
  "(P outside (X ∪ Y)) ∩ (Q || X) = {}   &   (P outside X) ∩ (Q || (X ∩ Z)) = {}" 
  using Outside_def restrict_def lm039 lm015 by fast

lemma lm041: 
  "P outside X    =    P || ((Domain P) - X)" 
  using Outside_def restrict_def lm037 by fast

lemma lm042: 
  "R``(X-Y) = (R||X)``(X-Y)" 
  using restrict_def by blast

(* x is a (non-empty) element of the family XX whose union is a subset of X *)
lemma lm043: 
  assumes "⋃ XX ⊆ X" "x ∈ XX" "x ≠ {}" 
  shows "x ∩ X ≠ {}" 
  using assms by blast

(* Note that set converts lists such as L1 into sets. L1 is here a list of lists and l an element, that is, a list. We assume furthermore that f2 is constant function with the fixed 2nd argument N. Then we can convert lists to sets in a canonical way. *)
lemma lm044: 
  assumes "∀l ∈ set L1. set L2 = f2 (set l) N" 
  shows "set [set L2. l <- L1]  =  {f2 P N| P. P ∈ set (map set L1)}" 
  using assms by auto

(* Two Variants of the previous lemma *)
lemma setVsList: 
  assumes "∀l ∈ set (g1 G). set (g2 l N) = f2 (set l) N" 
  shows "set [set (g2 l N). l <- (g1 G)]  =  {f2 P N| P. P ∈ set (map set (g1 G))}" 
  using assms by auto

lemma lm045: 
  "(∀l ∈ set (g1 G). set (g2 l N) = f2 (set l) N) -->  
     {f2 P N| P. P ∈ set (map set (g1 G))} = set [set (g2 l N). l <- g1 G]" 
  by auto

lemma lm046: 
  assumes "X ∩ Y  =  {}" 
  shows "R``X = (R outside Y)``X"
  using assms Outside_def Image_def by blast

lemma lm047: 
  assumes "(Range P) ∩ (Range Q) = {}" "runiq (P^-1)" "runiq (Q^-1)" 
  shows "runiq ((P ∪ Q)^-1)"
  using assms by (metis Domain_converse converse_Un disj_Un_runiq)

lemma lm048: 
  assumes "(Range P) ∩ (Range Q) = {}" "runiq (P^-1)" "runiq (Q^-1)" 
  shows "runiq ((P +* Q)^-1)"
  using lm047 assms subrel_runiq by (metis converse_converse converse_subset_swap paste_sub_Un)

lemma lm049: 
  assumes "runiq R" 
  shows "card (R `` {a}) = 1 ⟷ a ∈ Domain R"
  using assms card_Suc_eq One_nat_def  
  by (metis Image_within_domain' Suc_neq_Zero assms rightUniqueSetCardinality)

(* triples a can be bracket in any way, i.e., (1st, (2nd, 3rd)) → ((1st, 2nd), 3rd).*)
lemma lm050: 
  "inj (λa. ((fst a, fst (snd a)), snd (snd a)))"
  by (auto intro: injI)

lemma lm051: 
  assumes "finite X" "x > Max X" 
  shows "x ∉ X" 
  using assms Max.coboundedI by (metis leD)

lemma lm052: 
  assumes "finite A" "A ≠ {}" 
  shows "Max (f`A) ∈ f`A" 
  using assms by (metis Max_in finite_imageI image_is_empty)

(* Note that in the following -` means the inverse image of the following set. *)
lemma lm053: 
  "argmax f A ⊆ f -` {Max (f ` A)}" 
  by force

lemma lm054: 
  "argmax f A = A ∩ { x . f x = Max (f ` A) }" 
  by auto

lemma lm055: 
  "(x ∈ argmax f X) = (x ∈ X & f x = Max (f ` X))" 
  using argmax.simps mem_Collect_eq by (metis (mono_tags, lifting))

lemma rangeEmpty: 
  "Range -` {{}} = {{}}" 
  by auto

lemma finitePairSecondRange: 
  "(∀ pair ∈ R. finite (snd pair)) = (∀ y ∈ Range R. finite y)" 
  by fastforce

lemma lm056: 
  "fst ` P = snd ` (P^-1)" 
  by force

lemma lm057: 
  "fst pair = snd (flip pair) & snd pair = fst (flip pair)" 
  unfolding flip_def by simp

lemma flip_flip2: 
  "flip ∘ flip   =   id" 
  using flip_flip by fastforce

lemma lm058: 
  "fst = (snd∘flip)" 
  using lm057 by fastforce

lemma lm059: 
  "snd = (fst∘flip)" 
  using lm057 by fastforce

lemma lm060: 
  "inj_on fst P = inj_on (snd∘flip) P" 
  using lm058 by metis

lemma lm062: 
  "inj_on fst P = inj_on snd (P^-1)" 
  using lm060 flip_conv by (metis converse_converse inj_on_imageI lm059)

lemma sumPairsInverse: 
  assumes "runiq (P^-1)" 
  shows "sum (f ∘ snd) P = sum f (Range P)" 
  using assms lm062 converse_converse rightUniqueInjectiveOnFirst rightUniqueInjectiveOnFirst
        sum.reindex snd_eq_Range 
  by metis

lemma notEmptyFinestpart: 
  assumes "X ≠ {}" 
  shows "finestpart X ≠ {}" 
  using assms finestpart_def by blast

lemma lm063: 
  assumes "inj_on g X" 
  shows "sum f (g`X) = sum (f ∘ g) X" 
  using assms by (metis sum.reindex)

lemma functionOnFirstEqualsSecond: 
  assumes "runiq R" "z ∈ R" 
  shows "R,,(fst z) = snd z" 
  using assms by (metis rightUniquePair surjective_pairing)

lemma lm064: 
  assumes "runiq R" 
  shows "sum (toFunction R) (Domain R) = sum snd R" 
  using assms toFunction_def sum.reindex_cong functionOnFirstEqualsSecond
        rightUniqueInjectiveOnFirst 
  by (metis (no_types) fst_eq_Domain)

corollary lm065: 
  assumes "runiq (f||X)" 
  shows "sum (toFunction (f||X)) (X ∩ Domain f) = sum snd (f||X)" 
  using assms lm064 by (metis Int_commute restrictedDomain)

lemma lm066: 
  "Range (R outside X) = R``((Domain R) - X)"
  by (metis Diff_idemp ImageE Range.intros Range_outside_sub_Image_Domain lm041
            lm042 order_class.order.antisym subsetI)

lemma lm067: 
  "(R||X) `` X = R``X" 
  using Int_absorb doubleRestriction restrictedRange by metis

lemma lm068: 
  assumes "x ∈ Domain (f||X)" 
  shows "(f||X)``{x} = f``{x}" 
  using assms doubleRestriction restrictedRange Int_empty_right Int_iff 
        Int_insert_right_if1 restrictedDomain 
  by metis

lemma lm069: 
  assumes "x ∈ X ∩ Domain f" "runiq (f||X)" 
  shows "(f||X),,x = f,,x" 
  using assms doubleRestriction restrictedRange Int_empty_right Int_iff Int_insert_right_if1
        eval_rel.simps 
  by metis

lemma lm070: 
  assumes "runiq (f||X)" 
  shows "sum (toFunction (f||X)) (X ∩ Domain f) = sum (toFunction f) (X ∩ Domain f)" 
  using assms sum.cong lm069 toFunction_def by metis

corollary sumRestrictedToDomainInvariant: 
  assumes "runiq (f||X)" 
  shows "sum (toFunction f) (X ∩ Domain f) = sum snd (f||X)" 
  using assms lm065 lm070 by fastforce

corollary sumRestrictedOnFunction: 
  assumes "runiq (f||X)" 
  shows "sum (toFunction (f||X)) (X ∩ Domain f) = sum snd (f||X)" 
  using assms lm064 restrictedDomain Int_commute by metis

lemma cardFinestpart: 
  "card (finestpart X) = card X" 
  using finestpart_def by (metis (lifting) card_image inj_on_inverseI the_elem_eq)

corollary lm071: 
  "finestpart {} = {}    &    card ∘ finestpart = card" 
  using cardFinestpart finestpart_def by fastforce

lemma finiteFinestpart: 
  "finite (finestpart X) = finite X" 
  using finestpart_def lm071 
  by (metis card_eq_0_iff empty_is_image finite.simps cardFinestpart)

lemma lm072: 
  "finite ∘ finestpart = finite" 
  using finiteFinestpart by fastforce

lemma finestpartSubset: 
  assumes "X ⊆ Y" 
  shows "finestpart X ⊆ finestpart Y" 
  using assms finestpart_def by (metis image_mono)

corollary lm073: 
  assumes "x ∈ X" 
  shows "finestpart x ⊆ finestpart (⋃ X)" 
  using assms finestpartSubset by (metis Union_upper)

lemma lm074: 
  "⋃ (finestpart ` XX) ⊆ finestpart (⋃ XX)" 
  using finestpart_def lm073 by force

lemma lm075: 
  "⋃ (finestpart ` XX) ⊇ finestpart (⋃ XX)" 
  (is "?L ⊇ ?R") 
  unfolding finestpart_def using finestpart_def by auto

corollary commuteUnionFinestpart: 
  "⋃ (finestpart ` XX) = finestpart (⋃ XX)"
  using lm074 lm075 by fast

lemma unionImage: 
  assumes "runiq a" 
  shows "{(x, {y})| x y. y ∈ ⋃ (a``{x}) & x ∈ Domain a} = 
         {(x, {y})| x y. y ∈ a,,x & x ∈ Domain a}" 
  using assms Image_runiq_eq_eval 
  by (metis (lifting, no_types) cSup_singleton)

lemma lm076: 
  assumes "runiq P" 
  shows "card (Domain P) = card P" 
  using assms rightUniqueInjectiveOnFirst card_image by (metis Domain_fst)

lemma finiteDomainImpliesFinite: 
  assumes "runiq f" 
  shows "finite (Domain f) = finite f" 
  using assms Domain_empty_iff card_eq_0_iff finite.emptyI lm076 by metis

(* A relation for the sum of all y∈Y of f(x,y) for a fixed x. *)
lemma sumCurry: 
  "sum ((curry f) x) Y = sum f ({x} × Y)"
proof -
  let ?f="% y. (x, y)" let ?g="(curry f) x" let ?h=f
  have "inj_on ?f Y" by (metis(no_types) Pair_inject inj_onI) 
  moreover have "{x} × Y = ?f ` Y" by fast
  moreover have "∀ y. y ∈ Y ⟶ ?g y = ?h (?f y)" by simp
  ultimately show ?thesis using sum.reindex_cong by metis
qed

lemma lm077: 
  "sum (%y. f (x,y)) Y = sum f ({x}×Y)" 
  using sumCurry Sigma_cong curry_def sum.cong by fastforce

corollary lm078: 
  assumes "finite X" 
  shows "sum f X = sum f (X-Y) + (sum f (X ∩ Y))" 
  using assms Diff_iff IntD2 Un_Diff_Int finite_Un inf_commute sum.union_inter_neutral 
  by metis

lemma lm079: 
  "(P +* Q)``(Domain Q∩X)  =  Q``(Domain Q∩X)" 
  unfolding paste_def Outside_def Image_def Domain_def by blast

corollary lm080: 
  "(P +* Q)``(X∩(Domain Q))  =  Q``X"
  using Int_commute lm079 by (metis lm017)

corollary lm081: 
  assumes "X ∩ (Domain Q) = {}"
  shows "(P +* Q) `` X = (P outside (Domain Q))`` X" 
  using assms paste_def by fast

lemma lm082: 
  assumes "X∩Y = {}" 
  shows "(P outside Y)``X=P``X" 
  using assms Outside_def by blast

corollary lm083: 
  assumes "X∩ (Domain Q) = {}" 
  shows "(P +* Q)``X=P``X" 
  using assms lm081 lm082 by metis

lemma lm084: 
  assumes "finite X" "finite Y" "card(X∩Y) = card X" 
  shows "X ⊆ Y" 
  using assms by (metis Int_lower1 Int_lower2 card_seteq order_refl)

lemma cardinalityIntersectionEquality: 
  assumes "finite X" "finite Y" "card X = card Y" 
  shows "(card (X∩Y) = card X)     =    (X = Y)"
  using assms lm084 by (metis card_seteq le_iff_inf order_refl)

lemma lm085: (*fixes f::"'a => 'b" fixes P::"'a => bool" fixes xx::"'a"*) 
  assumes "P xx" 
  shows "{(x,f x)| x. P x},,xx   =   f xx"
proof -
  let ?F="{(x,f x)| x. P x}" let ?X="?F``{xx}"
  have "?X={f xx}" using Image_def assms by blast thus ?thesis by fastforce 
qed

lemma graphEqImage: 
  assumes "x ∈ X" 
  shows "graph X f,,x   =   f x" 
  unfolding graph_def using assms lm085 by (metis (mono_tags) Gr_def)

lemma lm086: 
  "Graph f,,x    =    f x" 
  using UNIV_I graphEqImage lm005 by (metis(no_types))

lemma lm087: 
  "toFunction (Graph f)    =    f"    (is "?L=_") 
proof -
  {fix x have "?L x=f x" unfolding toFunction_def lm086 by metis} 
  thus ?thesis by blast 
qed

lemma lm088: 
  "R outside X ⊆ R" 
  by (metis outside_union_restrict subset_Un_eq sup_left_idem)

lemma lm089: 
  "Range(f outside X) ⊇ (Range f)-(f``X)" 
  using Outside_def by blast

lemma lm090: 
  assumes "runiq P" 
  shows "(P¯``((Range P)-Y)) ∩ ((P¯)``Y)   =   {}"
  using assms rightUniqueFunctionAfterInverse by blast

lemma lm091: 
  assumes "runiq (P¯)"
  shows "(P``((Domain P) - X)) ∩ (P``X)  =  {}"
  using assms rightUniqueFunctionAfterInverse by fast

lemma lm092: 
  assumes "runiq f" "runiq (f^-1)" 
  shows "Range(f outside X) ⊆ (Range f)-(f``X)" 
  using assms Diff_triv lm091 lm066 Diff_iff ImageE Range_iff subsetI by metis 

lemma rangeOutside: 
  assumes "runiq f" "runiq (f^-1)" 
  shows "Range(f outside X) = (Range f)-(f``X)" 
  using assms lm089 lm092 by (metis order_class.order.antisym)

(* X and Y are family of sets such that any x and y in X and Y resp. are disjoint. *)
lemma unionIntersectionEmpty: 
  "(∀x∈X. ∀y∈Y. x∩y = {}) = ((⋃X)∩(⋃ Y)={})"
  by blast

lemma setEqualityAsDifference: 
  "{x}-{y} = {}  =  (x = y)" 
  by auto

lemma lm093: 
  assumes "R ≠ {}" "Domain R ∩ X ≠ {}" 
  shows "R``X ≠ {}" 
  using assms by blast

lemma lm095: 
  "R ⊆ (Domain R) × (Range R)" 
  by auto

lemma finiteRelationCharacterization: 
  "(finite (Domain Q) & finite (Range Q)) = finite Q"
  using rev_finite_subset finite_SigmaI lm095 finite_Domain finite_Range by metis

lemma familyUnionFiniteEverySetFinite: 
  assumes "finite (⋃ XX)" 
  shows "∀X ∈ XX. finite X" 
  using assms by (metis Union_upper finite_subset)

lemma lm096: 
  assumes "runiq f" "X ⊆ (f^-1)``Y" 
  shows "f``X ⊆ Y" 
  using assms rightUniqueFunctionAfterInverse by (metis Image_mono order_refl subset_trans)

lemma lm097: 
  assumes "y ∈ f``{x}" "runiq f" 
  shows "f,,x = y" 
  using assms by (metis Image_singleton_iff rightUniquePair)




subsection ‹Indicator function in set-theoretical form.›

abbreviation 
  "Outside' X f == f outside X"

abbreviation 
  "Chi X Y == (Y × {0::nat}) +* (X × {1})"
  notation Chi (infix "<||" 80)

abbreviation 
  "chii X Y == toFunction (X <|| Y)"
  notation chii (infix "<|" 80)

(* X is a set and chi X is a function that returns 1 for elements X and 0 else. *)
abbreviation 
  "chi X == indicator X"

lemma lm098: 
  "runiq (X <|| Y)" 
  by (rule lm014)

lemma lm099: 
  assumes "x ∈ X" 
  shows "1 ∈ (X <|| Y) `` {x}" 
  using assms toFunction_def paste_def Outside_def runiq_def lm014 by blast

lemma lm100: 
  assumes "x ∈ Y-X" 
  shows "0 ∈ (X <|| Y) `` {x}" 
  using assms toFunction_def paste_def Outside_def runiq_def lm014 by blast

lemma lm101: 
  assumes "x ∈ X ∪ Y" 
  shows "(X <|| Y),,x = chi X x" (is "?L=?R") 
  using assms lm014 lm099 lm100 lm097 
  by (metis DiffI Un_iff indicator_simps(1) indicator_simps(2))

lemma lm102: 
  assumes "x ∈ X ∪ Y" 
  shows "(X <| Y) x = chi X x" 
  using assms toFunction_def lm101 by metis

corollary lm103: 
  "sum (X <| Y) (X∪Y) = sum (chi X) (X∪Y)"
  using lm102 sum.cong by metis

corollary lm104: 
  assumes "∀x∈X. f x = g x" 
  shows "sum f X = sum g X" 
  using assms by (metis (poly_guards_query) sum.cong)

corollary lm105: 
  assumes "∀x∈X. f x = g x" "Y⊆X" 
  shows "sum f Y = sum g Y" 
  using assms lm104 by (metis contra_subsetD)

corollary lm106: 
  assumes "Z ⊆ X ∪ Y" 
  shows "sum (X <| Y) Z = sum (chi X) Z"  
proof - 
  have "∀x∈Z.(X<|Y) x=(chi X) x" using assms lm102 in_mono by metis 
  thus ?thesis using lm104 by blast 
qed

corollary lm107: 
  "sum (chi X) (Z - X) = 0" 
  by simp

corollary lm108: 
  assumes "Z ⊆ X ∪ Y" 
  shows "sum (X <| Y) (Z - X) = 0" 
  using assms lm107 lm106 Diff_iff in_mono subsetI by metis

corollary lm109: 
  assumes "finite Z" 
  shows "sum (X <| Y) Z    =    sum (X <| Y) (Z - X)   +  (sum (X <| Y) (Z ∩ X))" 
  using lm078 assms by blast

corollary lm110: 
  assumes "Z ⊆ X ∪ Y" "finite Z" 
  shows "sum (X <| Y) Z = sum (X <| Y) (Z ∩ X)" 
  using assms lm078 lm108 comm_monoid_add_class.add_0 by metis

corollary lm111: 
  assumes "finite Z" 
  shows "sum (chi X) Z = card (X ∩ Z)" 
  using assms sum_indicator_eq_card by (metis Int_commute)

corollary lm112: 
  assumes "Z ⊆ X ∪ Y" "finite Z" 
  shows "sum (X <| Y) Z = card (Z ∩ X)"
  using assms lm111 by (metis lm106 sum_indicator_eq_card)

corollary subsetCardinality: 
  assumes "Z ⊆ X ∪ Y" "finite Z" 
  shows "(sum (X <| Y) X) - (sum (X <| Y) Z) = card X - card (Z ∩ X)" 
  using assms lm112 by (metis Int_absorb2 Un_upper1 card.infinite equalityE sum.infinite)

corollary differenceSumVsCardinality: 
  assumes "Z ⊆ X ∪ Y" "finite Z" 
  shows "int (sum (X <| Y) X) - int (sum (X <| Y) Z) =  int (card X) - int (card (Z ∩ X))" 
  using assms lm112 by (metis Int_absorb2 Un_upper1 card.infinite equalityE sum.infinite)

(* type conversion in Isabelle *)
lemma lm113: 
  "int (n::nat) = real n" 
  by simp

(* same as differenceSumVsCardinality but for type real *)
corollary differenceSumVsCardinalityReal: 
  assumes "Z⊆X∪Y" "finite Z" 
  shows "real (sum (X <| Y) X) - real (sum (X <| Y) Z) = 
         real (card X) - real (card (Z ∩ X))" 
  using assms lm112 by (metis Int_absorb2 Un_upper1 card.infinite equalityE sum.infinite)


subsection ‹Lists›
(* If there is an element in a list satisfying P, then the list of all elements satisfying P is not the empty list *)
lemma lm114: 
  assumes "∃ n ∈ {0..<size l}. P (l!n)" 
  shows "[n. n ← [0..<size l], P (l!n)] ≠ []"
  using assms by auto

(* Assume ll is an element of list l, then there is an index n such that the n-th entry of l is ll. *)
lemma lm115: 
  assumes "ll ∈ set (l::'a list)" 
  shows "∃ n∈ (nth l) -` (set l). ll=l!n"
  using assms(1) by (metis in_set_conv_nth vimageI2)

(* variant of the above *)
lemma lm116: 
  assumes "ll ∈ set (l::'a list)" 
  shows "∃ n. ll=l!n & n < size l & n >= 0"
  using assms in_set_conv_nth by (metis le0)

(* another variant of the above *)
lemma lm117: 
  assumes "P -` {True} ∩ set l ≠ {}" 
  shows "∃ n ∈ {0..<size l}. P (l!n)" 
  using assms lm116 by fastforce

(* variant of lm114 *)
lemma nonEmptyListFiltered: 
  assumes "P -` {True} ∩ set l ≠ {}" 
  shows "[n. n ← [0..<size l], P (l!n)] ≠ []" 
  using assms filterpositions2_def lm117 lm114 by metis

(* take the elements of a list l which are also in a set X then this forms a subset of X intersection with the elements of the list *)
lemma lm118: 
  "(nth l) ` set ([n. n ← [0..<size l], (%x. x∈X) (l!n)]) ⊆ X∩set l" 
  by force

(* variant of the above *)
corollary lm119: 
  "(nth l)` set (filterpositions2 (%x.(x∈X)) l) ⊆ X ∩  set l" 
  unfolding filterpositions2_def using lm118 by fast

lemma lm120: 
  "(n∈{0..<N}) = ((n::nat) < N)" 
  using atLeast0LessThan lessThan_iff by metis

(* If X is a set of indices then the corresponding elements combined are a subset of all the elements of the list. *)
lemma lm121: 
  assumes "X ⊆ {0..<size list}" 
  shows "(nth list)`X ⊆ set list" 
  using assms atLeastLessThan_def atLeast0LessThan lessThan_iff by auto

(* The indices of the elements of a list satisfying a predicate P are a subset of all the indices. *)
lemma lm122: 
  "set ([n. n ← [0..<size l], P (l!n)]) ⊆ {0..<size l}" 
  by force

(* variant of the above *)
lemma lm123: 
  "set (filterpositions2 pre list) ⊆ {0..<size list}" 
  using filterpositions2_def lm122 by metis



subsection ‹Computing all the permutations of a list›
abbreviation 
  "rotateLeft == rotate"
abbreviation 
  "rotateRight n l == rotateLeft (size l - (n mod (size l))) l"

(* for n in {0, ..., size l} inserts x in l so that it will have index n in the output*)
(* note that for other n, the behaviour is not guaranteed to be consistent with that *)
abbreviation 
  "insertAt x l n == rotateRight n (x#(rotateLeft n l))"

(* for n in {0,..., fact(size l) - 1 }, 
   perm2 l n gives all and only the possible permutations of l *)
fun perm2 where
  "perm2 [] = (%n. [])" | 
  "perm2 (x#l) = (%n. insertAt x ((perm2 l) (n div (1+size l)))
                      (n mod (1+size l)))"

abbreviation 
  "takeAll P list == map (nth list) (filterpositions2 P list)"

lemma permutationNotEmpty: 
  assumes "l ≠ []" 
  shows "perm2 l n ≠ []" 
  using assms perm2.simps(2) rotate_is_Nil_conv by (metis neq_Nil_conv)

lemma lm124: 
  "set (takeAll P list) = ((nth list) ` set (filterpositions2 P list))" 
  by simp

corollary listIntersectionWithSet: 
  "set (takeAll (%x.(x∈X)) l) ⊆  (X ∩ set l)" 
  using lm119 lm124 by metis

corollary lm125: 
  "set (takeAll P list) ⊆ set list" 
  using lm123 lm124 lm121 by metis

lemma takeAllSubset:
  "set (takeAll (%x. x∈ P) list) ⊆ P"
  by (metis Int_subset_iff listIntersectionWithSet) 

lemma lm126: 
  "set (insertAt x l n) = {x} ∪ set l" 
  by simp

lemma lm127: 
  "∀n. set (perm2 [] n) = set []" 
  by simp

lemma lm128: 
  assumes "∀n. (set (perm2 l n) = set l)" 
  shows "set (perm2 (x#l) n) = {x} ∪ set l" 
  using assms lm126 by force

(* Combining the previous two lemmas we get inductively that the set of elements in a permuted list are the same as the elements in the original list. This is weaker than saying (perm2 l n) is a permutation of l, but suffices for our purposes. *) 
corollary permutationInvariance: 
   "∀n. set (perm2 (l::'a list) n) = set l" 
proof (induct l)
   let ?P = "%l::('a list). (∀n. set (perm2 l n)  =  set l)"
   show "?P []" using lm127 by force 
   fix x fix l 
   assume "?P l" then 
   show "?P (x#l)" by force
qed

(* variant of listIntersectionWithSet with permutation added *)
corollary takeAllPermutation: 
  "set (perm2 (takeAll (%x.(x∈X)) l) n)  ⊆  X ∩ set l" 
  using listIntersectionWithSet permutationInvariance by metis

(* "subList list1 list2" extracts the components of list1 according to the indices given in list2, e.g.,  "subList [1::nat,2,3,4] [0,2]" gives [1,3] *)
abbreviation "subList l xl == map (nth l) (takeAll (%x. x ≤ size l) xl)"


subsection ‹A more computable version of @{term toFunction}.›

(* If R is a relation and the image of x is unique then take that, else take the fallback *)
abbreviation "toFunctionWithFallback R fallback == 
              (% x. if (R``{x} = {R,,x}) then (R,,x) else fallback)"
notation 
  toFunctionWithFallback (infix "Else" 75)

abbreviation sum' where
  "sum' R X == sum (R Else 0) X"

lemma lm129: 
  assumes "runiq f" "x ∈ Domain f" 
  shows "(f Else 0) x = (toFunction f) x" 
  using assms by (metis Image_runiq_eq_eval toFunction_def)

lemma lm130: 
  assumes "runiq f" 
  shows "sum (f Else 0) (X∩(Domain f))  =  sum (toFunction f) (X∩(Domain f))" 
  using assms sum.cong lm129 by fastforce

lemma lm131: 
  assumes "Y ⊆ f-`{0}" 
  shows "sum f Y  =  0" 
  using assms by (metis rev_subsetD sum.neutral vimage_singleton_eq)

lemma lm132: 
  assumes "Y ⊆ f-`{0}" "finite X" 
  shows "sum f X = sum f (X-Y)"
  using Int_lower2 add.comm_neutral assms(1) assms(2) lm078 lm131 order_trans
  by (metis (no_types))

(* - means the complement of a set. *)
lemma lm133: 
  "-(Domain f) ⊆ (f Else 0)-`{0}" 
  by fastforce

corollary lm134: 
  assumes "finite X" 
  shows "sum (f Else 0) X    =   sum (f Else 0) (X∩Domain f)" 
proof - 
  have "X∩Domain f=X-(-Domain f)" by simp 
  thus ?thesis using assms lm133 lm132 by fastforce
qed

corollary lm135: 
  assumes "finite X" 
  shows "sum (f Else 0) (X∩Domain f)   =   sum (f Else 0) X"
  (is "?L=?R") 
proof - 
  have "?R=?L" using assms by (rule lm134) 
  thus ?thesis by simp 
qed

corollary lm136: 
  assumes "finite X" "runiq f" 
  shows "sum (f Else 0) X = sum (toFunction f) (X∩Domain f)" 
  (is "?L=?R") 
proof -
  have "?R = sum (f Else 0) (X∩Domain f) " using assms(2) lm130 by fastforce
  moreover have "... = ?L" using assms(1) by (rule lm135) 
  ultimately show ?thesis by presburger
qed

lemma lm137: 
  "sum (f Else 0) X = sum' f X" 
  by fast

corollary lm138: 
  assumes "finite X" "runiq f" 
  shows "sum (toFunction f) (X∩Domain f)   =   sum' f X"
  using assms lm137 lm136 by fastforce

lemma lm139: 
  "argmax (sum' b) = (argmax ∘ sum') b" 
  by simp

lemma domainConstant: 
  "Domain (Y × {0::nat}) = Y & Domain (X × {1}) = X" 
  by blast

lemma domainCharacteristicFunction: 
  "Domain (X <|| Y) = X ∪ Y" 
  using domainConstant paste_Domain sup_commute by metis

lemma functionEquivalenceOnSets: 
  assumes "∀x ∈ X. f x = g x" 
  shows "f`X = g`X" 
  using assms by (metis image_cong)


subsection ‹Cardinalities of sets.›
lemma lm140: 
  assumes "runiq R" "runiq (R^-1)" 
  shows "(R``A) ∩ (R``B) = R``(A∩B)" 
  using assms rightUniqueInjectiveOnFirst converse_Image by force

lemma intersectionEmptyRelationIntersectionEmpty: 
  assumes "runiq (R^-1)" "runiq R" "X1 ∩ X2 = {}" 
  shows "(R``X1) ∩ (R``X2) = {}"
  using assms by (metis disj_Domain_imp_disj_Image inf_assoc inf_bot_right)

lemma lm141: 
  assumes "runiq f" "trivial Y" 
  shows "trivial (f `` (f^-1 `` Y))"
  using assms by (metis rightUniqueFunctionAfterInverse trivial_subset)

lemma lm142: 
  assumes "trivial X" 
  shows "card (Pow X)∈{1,2}" 
  using trivial_empty_or_singleton card_Pow Pow_empty assms trivial_implies_finite
        cardinalityOneTheElemIdentity power_one_right the_elem_eq 
  by (metis insert_iff)

lemma lm143: 
  assumes "card (Pow A) = 1" 
  shows "A = {}" 
  using assms by (metis Pow_bottom Pow_top cardinalityOneTheElemIdentity singletonD)

(* Note that in Isabelle infinite sets have cardinality 0 *) 
lemma lm144: 
  "(¬ (finite A)) = (card (Pow A) = 0)" 
  by auto

corollary lm145: 
  "(finite A) = (card (Pow A) ≠ 0)" 
  using lm144 by metis

lemma lm146: 
  assumes "card (Pow A) ≠ 0" 
  shows "card A=Discrete.log (card (Pow A))" 
  using assms log_exp card_Pow by (metis card.infinite finite_Pow_iff)

lemma log_2 [simp]:
  "Discrete.log 2 = 1"
  using log_exp [of 1] by simp

lemma lm147: 
  assumes "card (Pow A) = 2" 
  shows "card A = 1" 
  using assms lm146 [of A] by simp

lemma lm148: 
  assumes "card (Pow X) = 1 ∨ card (Pow X) = 2" 
  shows "trivial X" 
  using assms trivial_empty_or_singleton lm143 lm147 cardinalityOneTheElemIdentity by metis

lemma lm149: 
  "trivial A = (card (Pow A) ∈ {1,2})" 
  using lm148 lm142 by blast

lemma lm150: 
  assumes "R ⊆ f" "runiq f" "Domain f = Domain R" 
  shows "runiq R"
  using assms by (metis subrel_runiq)

lemma lm151: 
  assumes "f ⊆ g" "runiq g" "Domain f = Domain g" 
  shows "g ⊆ f"
  using assms Domain_iff contra_subsetD runiq_wrt_ex1 subrelI
  by (metis (full_types,opaque_lifting))

lemma lm152: 
  assumes "R ⊆ f" "runiq f" "Domain f ⊆ Domain R" 
  shows "f = R" 
  using assms lm151 by (metis Domain_mono dual_order.antisym)

lemma lm153: 
  "graph X f = (Graph f) || X" 
  using inf_top.left_neutral lm005 domainOfGraph restrictedDomain lm152 graphIntersection
        restriction_is_subrel subrel_runiq subset_iff 
  by (metis (erased, lifting))

lemma lm154: 
  "graph (X ∩ Y) f = (graph X f) || Y" 
  using doubleRestriction lm153 by metis

lemma restrictionVsIntersection:
  "{(x, f x)| x. x ∈ X2} || X1 = {(x, f x)| x. x ∈ X2 ∩ X1}" 
  using graph_def lm154 by metis

lemma lm155: 
  assumes "runiq f" "X ⊆ Domain f" 
  shows "graph X (toFunction f) = (f||X)" 
proof -
  have "⋀v w. (v::'a set) ⊆ w ⟶ w ∩ v = v" by (simp add: Int_commute inf.absorb1)
  thus "graph X (toFunction f) = f || X" by (metis assms(1) assms(2) doubleRestriction lm004 lm153)
qed

lemma lm156: 
  "(Graph f) `` X = f ` X" 
  unfolding Graph_def image_def by auto

lemma lm157: 
  assumes "X ⊆ Domain f" "runiq f" 
  shows "f``X = (eval_rel f)`X"
  using assms lm156 by (metis restrictedRange lm153 lm155 toFunction_def)

lemma cardOneImageCardOne: 
  assumes "card A = 1" 
  shows "card (f`A) = 1" 
  using assms card_image card_image_le 
proof -
  have "finite (f`A)" using assms One_nat_def Suc_not_Zero card.infinite finite_imageI 
       by (metis(no_types)) 
  moreover have "f`A ≠ {}" using assms by fastforce
  moreover have "card (f`A) ≤ 1" using assms card_image_le One_nat_def Suc_not_Zero card.infinite
       by (metis)
  ultimately show ?thesis by (metis assms image_empty image_insert 
                                    cardinalityOneTheElemIdentity the_elem_eq)
qed

lemma cardOneTheElem: 
  assumes "card A = 1" 
  shows "the_elem (f`A) = f (the_elem A)" 
  using assms image_empty image_insert the_elem_eq by (metis cardinalityOneTheElemIdentity)

(* With split being the inverse of curry we have with g as swap f,  (g x y) = (f y x) *)
abbreviation 
  "swap f == curry ((case_prod f) ∘ flip)" (*swaps the two arguments of a function*)

(* X is finite if and only if X is the set of elements of some list. *)
lemma lm158: 
  "finite X   =  (X ∈ range set)" 
  by (metis List.finite_set finite_list image_iff rangeI)

(* as above, just as lambda expression *)
lemma lm159: 
  "finite = (%X. X∈range set)" 
  using lm158 by metis

lemma lm160: 
  "swap f = (%x. %y. f y x)" 
  by (metis comp_eq_dest_lhs curry_def flip_def fst_conv old.prod.case snd_conv)



subsection ‹Some easy properties on real numbers›
lemma lm161: 
  fixes a::real 
  fixes b c 
  shows "a*b - a*c=a*(b-c)"
  by (metis real_scaleR_def real_vector.scale_right_diff_distrib)

lemma lm162: 
  fixes a::real 
  fixes b c 
  shows "a*b - c*b=(a-c)*b"
  using lm161 by (metis mult.commute)

end