:: Semantic of MML Query
:: by Grzegorz Bancerek
::
:: Received December 18, 2011
:: Copyright (c) 2011-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies MMLQUERY, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
FUNCOP_1, ZFMISC_1, AOFA_000, CARD_1, FINSEQ_1, NAT_1, NUMBERS, XXREAL_0,
CARD_3, ORDINAL1, FINSET_1, STRUCT_0, QC_LANG1, ARYTM_3;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
RELSET_1, FUNCOP_1, ORDINAL1, FINSET_1, CARD_1, CARD_3, STRUCT_0,
XCMPLX_0, XXREAL_0, NUMBERS, NAT_1, FINSEQ_1, AOFA_000, FINSEQ_4, PROB_3;
constructors TARSKI, SUBSET_1, SETFAM_1, RELSET_1, FUNCT_1, FUNCOP_1,
FINSEQ_1, CARD_1, XXREAL_0, CARD_3, FINSET_1, STRUCT_0, WELLORD2,
FINSEQ_4, XCMPLX_0, NAT_1, PROB_3;
registrations SUBSET_1, RELSET_1, ORDINAL1, FINSET_1, XXREAL_0, FINSEQ_1,
CARD_1, NAT_1, XCMPLX_0;
requirements BOOLE, SUBSET, NUMERALS, ARITHM;
begin :: Elementary queries
definition
let X be set;
mode List of X is Subset of X;
mode Operation of X is Relation of X;
end;
definition
let x,y,R be set;
pred x,y in R means
:: MMLQUERY:def 1
[x,y] in R;
end;
notation
let x,y,R be set;
antonym x,y nin R for x,y in R;
end;
reserve X,Y,z,s for set, L,L1,L2,A,B for List of X, x for Element of X,
O,O1,O2,O3 for Operation of X, a,b,y for Element of X, n,m for Nat;
theorem :: MMLQUERY:1
for R1,R2 be Relation holds R1 c= R2 iff
for z being object holds Im(R1,z) c= Im(R2,z);
notation
let X,O,x;
synonym x.O for Im(O,x);
end;
definition
let X,O,x;
redefine func x.O -> List of X;
end;
theorem :: MMLQUERY:2
x,y in O iff y in x.O;
notation
let X,O,L;
synonym L | O for O.:L;
end;
definition
let X,O,L;
redefine func L | O -> List of X equals
:: MMLQUERY:def 2
union {x.O: x in L};
func L \& O -> List of X equals
:: MMLQUERY:def 3
meet {x.O: x in L};
func L WHERE O -> List of X equals
:: MMLQUERY:def 4
{x: ex y st x,y in O & x in L};
let O2 be Operation of X;
func L WHEREeq(O,O2) -> List of X equals
:: MMLQUERY:def 5
{x: card(x.O) = card(x.O2) & x in L};
func L WHEREle(O,O2) -> List of X equals
:: MMLQUERY:def 6
{x: card(x.O) c= card(x.O2) & x in L};
func L WHEREge(O,O2) -> List of X equals
:: MMLQUERY:def 7
{x: card(x.O2) c= card(x.O) & x in L};
func L WHERElt(O,O2) -> List of X equals
:: MMLQUERY:def 8
{x: card(x.O) in card(x.O2) & x in L};
func L WHEREgt(O,O2) -> List of X equals
:: MMLQUERY:def 9
{x: card(x.O2) in card(x.O) & x in L};
end;
definition
let X,L,O,n;
func L WHEREeq(O,n) -> List of X equals
:: MMLQUERY:def 10
{x: card(x.O) = n & x in L};
func L WHEREle(O,n) -> List of X equals
:: MMLQUERY:def 11
{x: card(x.O) c= n & x in L};
func L WHEREge(O,n) -> List of X equals
:: MMLQUERY:def 12
{x: n c= card(x.O) & x in L};
func L WHERElt(O,n) -> List of X equals
:: MMLQUERY:def 13
{x: card(x.O) in n & x in L};
func L WHEREgt(O,n) -> List of X equals
:: MMLQUERY:def 14
{x: n in card(x.O) & x in L};
end;
theorem :: MMLQUERY:3
x in L WHERE O iff x in L & x.O <> {};
theorem :: MMLQUERY:4
L WHERE O c= L;
theorem :: MMLQUERY:5
L c= dom O implies L WHERE O = L;
theorem :: MMLQUERY:6
n <> 0 & L1 c= L2 implies L1 WHEREge(O,n) c= L2 WHERE O;
theorem :: MMLQUERY:7
L WHEREge(O,1) = L WHERE O;
theorem :: MMLQUERY:8
L1 c= L2 implies L1 WHEREgt(O,n) c= L2 WHERE O;
theorem :: MMLQUERY:9
L WHEREgt(O,0) = L WHERE O;
theorem :: MMLQUERY:10
n <> 0 & L1 c= L2 implies L1 WHEREeq(O,n) c= L2 WHERE O;
theorem :: MMLQUERY:11
L WHEREge(O,n+1) = L WHEREgt(O,n);
theorem :: MMLQUERY:12
L WHEREle(O,n) = L WHERElt(O,n+1);
theorem :: MMLQUERY:13
n <= m & L1 c= L2 & O1 c= O2 implies L1 WHEREge(O1,m) c= L2 WHEREge(O2,n);
theorem :: MMLQUERY:14
n <= m & L1 c= L2 & O1 c= O2 implies L1 WHEREgt(O1,m) c= L2 WHEREgt(O2,n);
theorem :: MMLQUERY:15
n <= m & L1 c= L2 & O1 c= O2 implies L1 WHEREle(O2,n) c= L2 WHEREle(O1,m);
theorem :: MMLQUERY:16
n <= m & L1 c= L2 & O1 c= O2 implies L1 WHERElt(O2,n) c= L2 WHERElt(O1,m);
theorem :: MMLQUERY:17
O1 c= O2 & L1 c= L2 & O c= O3 implies L1 WHEREge(O,O2) c= L2 WHEREge(O3,O1);
theorem :: MMLQUERY:18
O1 c= O2 & L1 c= L2 & O c= O3 implies L1 WHEREgt(O,O2) c= L2 WHEREgt(O3,O1);
theorem :: MMLQUERY:19
O1 c= O2 & L1 c= L2 & O c= O3 implies L1 WHEREle(O3,O1) c= L2 WHEREle(O,O2);
theorem :: MMLQUERY:20
O1 c= O2 & L1 c= L2 & O c= O3 implies L1 WHERElt(O3,O1) c= L2 WHERElt(O,O2);
theorem :: MMLQUERY:21
L WHEREgt(O,O1) c= L WHERE O;
theorem :: MMLQUERY:22
O1 c= O2 & L1 c= L2 implies L1 WHERE O1 c= L2 WHERE O2;
theorem :: MMLQUERY:23
a in L|O iff ex b st a in b.O & b in L;
notation
let X,A,B;
synonym A AND B for A /\ B;
synonym A OR B for A \/ B;
synonym A BUTNOT B for A \ B;
end;
definition
let X,A,B;
redefine func A AND B -> List of X;
redefine func A OR B -> List of X;
redefine func A BUTNOT B -> List of X;
end;
theorem :: MMLQUERY:24
L1 <> {} & L2 <> {} implies (L1 OR L2)\& O = (L1 \& O)AND(L2 \& O);
theorem :: MMLQUERY:25
L1 c= L2 & O1 c= O2 implies L1|O1 c= L2|O2;
theorem :: MMLQUERY:26
O1 c= O2 implies L\&O1 c= L\&O2;
theorem :: MMLQUERY:27
L\&(O1 AND O2) = (L \& O1)AND(L \& O2);
theorem :: MMLQUERY:28
L1 <> {} & L1 c= L2 implies L2 \& O c= L1 \& O;
begin :: Operations
theorem :: MMLQUERY:29
for O1,O2 being Operation of X st for x holds x.O1 = x.O2 holds O1 = O2;
theorem :: MMLQUERY:30
for O1,O2 being Operation of X st for L holds L|O1 = L|O2 holds O1 = O2;
definition
let X,O;
func NOT O -> Operation of X means
:: MMLQUERY:def 15
for L holds L|it = union {IFEQ(x.O, {}, {x}, {}): x in L};
end;
notation
let X;
let O1,O2 be Operation of X;
synonym O1 AND O2 for O1 /\ O2;
synonym O1 OR O2 for O1 \/ O2;
synonym O1 BUTNOT O2 for O1 \ O2;
synonym O1 | O2 for O1 * O2;
end;
definition
let X;
let O1,O2 be Operation of X;
redefine func O1 AND O2 -> Operation of X means
:: MMLQUERY:def 16
for L holds L|it = union {x.O1 AND x.O2: x in L};
redefine func O1 OR O2 -> Operation of X means
:: MMLQUERY:def 17
for L holds L|it = union {x.O1 OR x.O2: x in L};
redefine func O1 BUTNOT O2 -> Operation of X means
:: MMLQUERY:def 18
for L holds L|it = union {x.O1 BUTNOT x.O2: x in L};
redefine func O1 | O2 -> Operation of X means
:: MMLQUERY:def 19
for L holds L|it = L|O1|O2;
func O1 \& O2 -> Operation of X means
:: MMLQUERY:def 20
for L holds L|it = union {x.O1\&O2: x in L};
end;
theorem :: MMLQUERY:31
x.(O1 AND O2) = (x.O1)AND(x.O2);
theorem :: MMLQUERY:32
x.(O1 OR O2) = (x.O1)OR(x.O2);
theorem :: MMLQUERY:33
x.(O1 BUTNOT O2) = (x.O1)BUTNOT(x.O2);
theorem :: MMLQUERY:34
x.(O1|O2) = (x.O1)|O2;
theorem :: MMLQUERY:35
x.(O1\&O2) = (x.O1)\&O2;
theorem :: MMLQUERY:36
for z,s being object holds [z,s] in NOT O iff z = s & z in X & z nin dom O;
theorem :: MMLQUERY:37
NOT O = id(X\dom O);
theorem :: MMLQUERY:38
dom NOT NOT O = dom O;
theorem :: MMLQUERY:39
L WHERE NOT NOT O = L WHERE O;
theorem :: MMLQUERY:40
L WHEREeq(O,0) = L WHERE NOT O;
theorem :: MMLQUERY:41
NOT NOT NOT O = NOT O;
theorem :: MMLQUERY:42
(NOT O1) OR NOT O2 c= NOT (O1 AND O2);
theorem :: MMLQUERY:43
NOT (O1 OR O2) = (NOT O1) AND NOT O2;
theorem :: MMLQUERY:44
dom O1 = X & dom O2 = X implies (O1 OR O2)\& O = (O1 \& O) AND (O2 \& O);
definition
let X,O;
attr O is filtering means
:: MMLQUERY:def 21
O c= id X;
end;
theorem :: MMLQUERY:45
O is filtering iff O = id dom O;
registration
let X,O;
cluster NOT O -> filtering;
end;
registration
let X;
cluster filtering for Operation of X;
end;
reserve F,F1,F2 for filtering Operation of X;
registration
let X,F,O;
cluster F AND O -> filtering for Operation of X;
cluster O AND F -> filtering for Operation of X;
cluster F BUTNOT O -> filtering for Operation of X;
end;
registration
let X,F1,F2;
cluster F1 OR F2 -> filtering for Operation of X;
end;
theorem :: MMLQUERY:46
z in x.F implies z = x;
theorem :: MMLQUERY:47
L|F = L WHERE F;
theorem :: MMLQUERY:48
NOT NOT F = F;
theorem :: MMLQUERY:49
NOT (F1 AND F2) = (NOT F1) OR (NOT F2);
theorem :: MMLQUERY:50
dom(O OR NOT O) = X;
theorem :: MMLQUERY:51
F OR NOT F = id X;
theorem :: MMLQUERY:52
O AND NOT O = {};
theorem :: MMLQUERY:53
(O1 OR O2) AND NOT O1 c= O2;
begin :: Rough queries
reserve i for Element of NAT;
definition
let A be FinSequence;
let a be object;
func #occurrences(a,A) -> Nat equals
:: MMLQUERY:def 22
card {i: i in dom A & a in A.i};
end;
theorem :: MMLQUERY:54
for A being FinSequence, a being set holds #occurrences(a,A) <= len A;
theorem :: MMLQUERY:55
for A being FinSequence, a being set holds
A <> {} & #occurrences(a,A) = len A iff a in meet rng A;
definition
let A be FinSequence;
func max# A -> Nat means
:: MMLQUERY:def 23
(for a being set holds #occurrences(a,A) <= it) &
(for n st for a being set holds #occurrences(a,A) <= n holds it <= n);
end;
theorem :: MMLQUERY:56
for A being FinSequence holds max# A <= len A;
theorem :: MMLQUERY:57
for A being FinSequence, a being set st #occurrences(a,A) = len A holds
max# A = len A;
definition
let X;
let A be FinSequence of bool X;
let n be Nat;
func ROUGH(A,n) -> List of X equals
:: MMLQUERY:def 24
{x: n <= #occurrences(x,A)} if X <> {};
let m be Nat;
func ROUGH(A,n,m) -> List of X equals
:: MMLQUERY:def 25
{x: n <= #occurrences(x,A) & #occurrences(x,A) <= m} if X <> {};
end;
definition
let X;
let A be FinSequence of bool X;
func ROUGH(A) -> List of X equals
:: MMLQUERY:def 26
ROUGH(A, max# A);
end;
theorem :: MMLQUERY:58
for A being FinSequence of bool X holds
ROUGH(A, n, len A) = ROUGH(A, n);
theorem :: MMLQUERY:59
for A being FinSequence of bool X holds
n <= m implies ROUGH(A,m) c= ROUGH(A,n);
theorem :: MMLQUERY:60
for A being FinSequence of bool X holds
for n1,n2,m1,m2 being Nat st n1 <= m1 & n2 <= m2 holds
ROUGH(A,m1,n2) c= ROUGH(A,n1,m2);
theorem :: MMLQUERY:61
for A being FinSequence of bool X holds
ROUGH(A,n,m) c= ROUGH(A,n);
theorem :: MMLQUERY:62
for A being FinSequence of bool X st A <> {} holds
ROUGH(A, len A) = meet rng A;
theorem :: MMLQUERY:63
for A being FinSequence of bool X holds
ROUGH(A, 1) = Union A;
theorem :: MMLQUERY:64
for L1,L2 being List of X holds
ROUGH(<*L1,L2*>,2) = L1 AND L2;
theorem :: MMLQUERY:65
for L1,L2 being List of X holds
ROUGH(<*L1,L2*>,1) = L1 OR L2;
begin :: Constructor Database
definition
struct(1-sorted) ConstructorDB(#
carrier -> set,
Constrs -> List of the carrier,
ref-operation -> Relation of the carrier, the Constrs
#);
end;
definition
let X be 1-sorted;
mode List of X is List of the carrier of X;
mode Operation of X is Operation of the carrier of X;
end;
definition
let X;
let S be Subset of X;
let R be Relation of X,S;
func @R -> Relation of X equals
:: MMLQUERY:def 27
R;
end;
definition
let X be ConstructorDB;
let a be Element of X;
func a ref -> List of X equals
:: MMLQUERY:def 28
a.@the ref-operation of X;
func a occur -> List of X equals
:: MMLQUERY:def 29
a.((@the ref-operation of X)~);
end;
theorem :: MMLQUERY:66
for X being ConstructorDB
for x,y being Element of X holds x in y ref iff y in x occur;
definition
let X be ConstructorDB;
attr X is ref-finite means
:: MMLQUERY:def 30
for x being Element of X holds x ref is finite;
end;
registration
cluster finite -> ref-finite for ConstructorDB;
end;
registration
cluster finite non empty for ConstructorDB;
end;
registration
let X be ref-finite ConstructorDB;
let x be Element of X;
cluster x ref -> finite;
end;
definition
let X be ConstructorDB;
let A be FinSequence of the Constrs of X;
func ATLEAST(A) -> List of X equals
:: MMLQUERY:def 31
{x where x is Element of X: rng A c= x ref}
if the carrier of X <> {};
func ATMOST(A) -> List of X equals
:: MMLQUERY:def 32
{x where x is Element of X: x ref c= rng A}
if the carrier of X <> {};
func EXACTLY(A) -> List of X equals
:: MMLQUERY:def 33
{x where x is Element of X: x ref = rng A}
if the carrier of X <> {};
let n be Nat;
func ATLEAST-(A,n) -> List of X equals
:: MMLQUERY:def 34
{x where x is Element of X: card((rng A) \ x ref) <= n}
if the carrier of X <> {};
end;
definition
let X be ref-finite ConstructorDB;
let A be FinSequence of the Constrs of X;
let n be Nat;
func ATMOST+(A,n) -> List of X equals
:: MMLQUERY:def 35
{x where x is Element of X: card((x ref) \ rng A) <= n}
if the carrier of X <> {};
let m be Nat;
func EXACTLY+-(A,n,m) -> List of X equals
:: MMLQUERY:def 36
{x where x is Element of X: card((x ref) \ rng A) <= n &
card((rng A) \ x ref) <= m}
if the carrier of X <> {};
end;
reserve X for ConstructorDB, A for FinSequence of the Constrs of X,
x for Element of X;
reserve Y for ref-finite ConstructorDB,
B for FinSequence of the Constrs of Y,
y for Element of Y;
theorem :: MMLQUERY:67
ATLEAST-(A,0) = ATLEAST(A);
theorem :: MMLQUERY:68
ATMOST+(B,0) = ATMOST(B);
theorem :: MMLQUERY:69
EXACTLY+-(B,0,0) = EXACTLY(B);
theorem :: MMLQUERY:70
n <= m implies ATLEAST-(A,n) c= ATLEAST-(A,m);
theorem :: MMLQUERY:71
n <= m implies ATMOST+(B,n) c= ATMOST+(B,m);
theorem :: MMLQUERY:72
for n1,n2,m1,m2 being Nat st n1 <= m1 & n2 <= m2 holds
EXACTLY+-(B,n1,n2) c= EXACTLY+-(B,m1,m2);
theorem :: MMLQUERY:73
ATLEAST(A) c= ATLEAST-(A,n);
theorem :: MMLQUERY:74
ATMOST(B) c= ATMOST+(B,n);
theorem :: MMLQUERY:75
EXACTLY(B) c= EXACTLY+-(B,n,m);
theorem :: MMLQUERY:76
EXACTLY A = ATLEAST A AND ATMOST A;
theorem :: MMLQUERY:77
EXACTLY+-(B,n,m) = ATLEAST-(B,m) AND ATMOST+(B,n);
theorem :: MMLQUERY:78
A <> {} implies ATLEAST A = meet {x occur: x in rng A};
theorem :: MMLQUERY:79
for c1,c2 being Element of X holds
A = <*c1,c2*> implies ATLEAST A = (c1 occur) AND (c2 occur);