Trinh Le Khanh (Oct 22 2020 at 09:35): Trinh Le Khanh (Oct 22 2020 at 09:35):Hi everyone, I want to define and use a set of functions to map elements from set X to set Y but I got trouble about using it.
For example, we have two sets as follows:
definition X :: "nat set"
where "X = {1, 2}"
definition Y :: "nat set"
where "Y = {3, 4}"
alpha is the function map an element of X to an element of Y and alphaSet is the set of alpha. For instance,
alphaSet = {(1,3), (2,4)} or {(1,4), (2,3)} or ...
If alphaSet = {(1,3), (2,4)} then
alpha 1 = 3
alpha 2 = 4
Thus, I defined alpha and alphaSet as follows:
definition alpha :: "nat ⇒ nat" where
"alpha x = (if x ∈ X then (SOME y. y ∈ Y) else 0)"
definition alphaSet :: "(nat ⇒ nat) set " where
"alphaSet = {f. (∀x ∈ X.(f x) ∈ Y)}"
My problem is that how can I generate the values of alphaSet (i.e. how to get the set of function)? I tried
value "∀x ∈ X. alpha x". ------- error
lemma test1: "(x ∈ X) ∧ (alpha ∈ alphaSet) ⟹ ((alpha x) ∈ Y)"
but the result is Failed to finish proof. Could anyone help me, please? Thank you very much.
Mathias Fleury (Oct 22 2020 at 09:48):value does not work for an obvious reason: It does not type. You are probably looking for value "alpha ` X", which does not work either, because of the SOME. There is no way Isabelle can evaluate this expression, it is not constructive.
Mathias Fleury (Oct 22 2020 at 09:49):About test1: I don't believe that it is out of the reach of someone who has done the Isabelle part of the Concrete Semantics.
Mathias Fleury (Oct 22 2020 at 09:49):(and the lemma is correct)
Mathias Fleury (Oct 22 2020 at 09:52):A constructive way for alpha can involve sorted_list_of_set to convert a set to a list and build the mapping explicitly.
Trinh Le Khanh (Oct 22 2020 at 10:01):About test1: I don't believe that it is out of the reach of someone who has done the Isabelle part of the Concrete Semantics.
Yes, I've just done it. I forgot to unfold the definitions of X, Y, alpha, and alphaSet.
A constructive way for alpha can involve
sorted_list_of_setto convert a set to a list and build the mapping explicitly.
Thank you for your suggestion. I'll try it.
Mathias Fleury (Oct 22 2020 at 10:09):The question is probably if you really need to have an explicit mapping. There should be a theorem somewhere that states that there is an injection between two sets of the same cardinality.
Trinh Le Khanh (Oct 22 2020 at 22:33):Mathias Fleury said:
The question is probably if you really need to have an explicit mapping. There should be a theorem somewhere that states that there is an injection between two sets of the same cardinality.
Yes, actually, I need that: for each x ∈ X, create a set Y_x. For example,
X = {0, 1}
x ∈ X
x = 0: create Y_0 = {3,4,5}
x = 1: create Y_1 = {6,7}
Mathias Fleury said:
The question is probably if you really need to have an explicit mapping. There should be a theorem somewhere that states that there is an injection between two sets of the same cardinality.
Hi Mathias, I got a problem defining a set of functions. I defined alphaSet (a set of alpha function) as follows:
definition SyncExport :: "nat set" (* Export*)
where "SyncExport = {1, 2}"
definition SyncElemExport :: "nat set" (*element Export*)
where "SyncElemExport = {1, 2}"
definition TypeSync :: "nat set" (*port types*)
where "TypeSync = {1, 2}"
definition IncSync :: "nat set set" (*port instances of each port type TypeSync*)
where "IncSync = {{5,6}, {7,8,9}}"
definition mapin :: "nat ⇒ nat set" where (*mapin 1 = {5,6}; mapin 2 = {7,8,9}*)
"mapin pt = (if pt ∈ TypeSync then (SOME pIn. pIn ∈ IncSync) else {})"
definition alphaSet :: "(nat ⇒ nat) set " where (*set of functions alpha*)
"alphaSet = {f. ∀x∈TypeSync. (f x) ∈ (mapin x)}"
definition alpha :: "nat ⇒ nat" where (*alpha 1= 5 or alpha 1 = 6*)
"alpha pt = (if pt ∈ TypeSync then (SOME y. y ∈ (mapin pt)) else 0)"
Then, I test the cardinality of TypeSync and IncSync. They are equal.
value "card TypeSync"
value "card IncSync"
But when I want to show the value of the below predicate:
value "(∀t∈TypeSync.∀alp∈alphaSet.(P t (alp t)))"
It caused the error:
Wellsortedness error
(in code equation alphaSet ≡ {f. ∀x∈TypeSync. f x ∈ mapin x},
with dependency "Pure.dummy_pattern" -> "alphaSet"):
Type nat ⇒ nat not of sort enum
No type arity nat :: enum
As I understand, this error is from the infinite set but I defined TypeSync and IncSync are finite sets. Do you have any suggestions?
Mathias Fleury (Nov 01 2020 at 20:13):mapin cannot be calculatedalphaSet cannot be calculated. Without code setup, it requires enumerating constructing all functions f and then filtering them. Trinh Le Khanh (Nov 01 2020 at 21:55):In the mapin, I want that from the i element of set A, we take the corresponding element in the set B.
I read the set library in Isabelle but they just provide operators insert or empty. Is there any chance to make an explicit mapping between two sets' elements?
Mathias Fleury (Nov 02 2020 at 05:28):By definition there is no order of elements of sets, but:
Mathias Fleury said:
A constructive way for alpha can involve
sorted_list_of_setto convert a set to a list and build the mapping explicitly.
allows you to build a list containing the same elements (if the set is finite). Then there is an order on the elements.
Mathias Fleury (Nov 02 2020 at 05:40):Along that line (don't name the function t in your development!):
fun t where
‹t (x # xs) (y # ys) = (t xs ys) (x := y)› |
‹t _ _ = (λx. 0)›
definition explicit_mapping :: ‹nat set ⇒ nat set ⇒ (nat ⇒ nat)› where
‹explicit_mapping xs ys = t (sorted_list_of_set xs) (sorted_list_of_set ys)›
value ‹explicit_mapping {1, 2, 3} {4, 5, 6}›
And here a completely random lemma:
lemma t_maps_to_existing:
‹length xs = length ys ⟹ x ∈ set xs ⟹ (t xs ys) x ∈ set ys›
by (induction xs ys rule: list_induct2) auto
(*why is that not in the library?*)
lemma length_sorted_list_of_set[simp]:
‹finite xs ⟹ length (sorted_list_of_set xs) = card xs›
by (metis distinct_card distinct_sorted_list_of_set set_sorted_list_of_set)
lemma
‹finite xs ⟹ finite ys ⟹ card xs = card ys ⟹ x ∈ xs ⟹ explicit_mapping xs ys x ∈ ys›
using t_maps_to_existing[of ‹sorted_list_of_set xs› ‹sorted_list_of_set ys› x]
by (auto simp: explicit_mapping_def)
But again: do you need to build the mapping explicitly or is it sufficient for you to show that one exists?
Mathias Fleury (Nov 02 2020 at 05:44):In the latter case, you can use the function finite_same_card_bij.
Trinh Le Khanh (Nov 02 2020 at 09:36):Mathias Fleury said:
In the latter case, you can use the function
finite_same_card_bij.
Thank you for your comment. This command
value ‹explicit_mapping {1, 2, 3} {4, 5, 6}›
returns
"_"
:: "nat ⇒ nat"
not
(1=>4), (2=>5), (3=>6)
I think the result should be the latter right?
In the latter case, you can use the function
finite_same_card_bij.
You mean that I can use it when proving lemmas and theorems not defining the mapping, right? Besides, defining the mapping using SOME is incorrect. I should change the definition, right?
Mathias Fleury (Nov 02 2020 at 10:32):I am convinced you can change the definitions to change explicit_mapping from a function (like it is now) to whatever you want.
Mathias Fleury (Nov 02 2020 at 10:33):You mean that I can use it when proving lemmas and theorems not defining the mapping, right? Besides, defining the mapping using SOME is incorrect. I should change the definition, right?
No, using SOME means you cannot compute it, so value cannot work. If you don't need the concrete mapping and don't need value, you can use some.
Trinh Le Khanh (Nov 02 2020 at 14:02):So, I keep my definition as follows:
definition PType :: "nat set" (*port types*)
where "PType = {1, 2}"
definition PIns :: "nat set set" (*port instances of each port type PType*)
where "PIns = {{5,6}, {7,8,9}}"
definition mapin :: "nat ⇒ nat set" where (*mapin 1 = {5,6}; mapin 2 = {7,8,9}*)
"mapin pt = (if pt ∈ PType then (SOME pIn. pIn ∈ PIns) else {})"
definition alphaSet :: "(nat ⇒ nat) set " where (*set of functions alpha*)
"alphaSet = {f. ∀x∈PType. (f x) ∈ (mapin x)}"
Then, I create a lemma using finite_same_card_bij but it unprovable (it stayed in proving forever)
lemma test31: "(∀t∈PType.(∀alp∈alphaSet.(P t (alp t) ⟶ (∀l1∈(mapin t)-{alp t}.¬P t l1))))
⟹ (∀t∈PType.(∃alp∈alphaSet.∀l1∈(mapin t)-{alp t}. ¬P t l1))"
unfolding PType_def mapin_def PIns_def alpha_def alphaSet_def
using finite_same_card_bij
apply blast
done
In Math, it should be equal because
(P 2 7 ⟶ ¬P 2 8 ∧ ¬P 2 9) ∧ (P 2 8 ⟶ ¬P 2 7 ∧ ¬P 2 9) ∧ (P 2 9 ⟶ ¬P 2 8 ∧ ¬P 2 7)
⟷ (¬P 2 8 ∧ ¬P 2 9)∨(¬P 2 7 ∧ ¬P 2 9)∨(¬P 2 8 ∧ ¬P 2 7)
You misunderstand what SOME means. It is an arbitrary choice. Unless that choice is unique, you _cannot say anything_ about its value. In particular mapin 1 = {5, 6} might be true but might also be false.
You are in exactly one of those cases:
mapin 1 = {5, 6} and mapin 2 = {7, 8, 9}
or mapin 1 = {5, 6} and mapin 2 = {5, 6}
or mapin 1 = {7, 8, 9} and mapin 2 = {5, 6}
or mapin 1 = {7, 8, 9} and mapin 2 = {7, 8, 9}
YOU HAVE NO WAY TO KNOW WHICH OF THOSE CASES IS TRUE.
Last updated: Apr 25 2024 at 01:08 UTC