:: Towards the construction of a model of Mizar concepts
:: by Grzegorz Bancerek
::
:: Received April 21, 2008
:: Copyright (c) 2008 Association of Mizar Users
theorem Th1: :: ABCMIZ_1:1
theorem :: ABCMIZ_1:2
theorem Th3: :: ABCMIZ_1:3
theorem Th4: :: ABCMIZ_1:4
theorem Th5: :: ABCMIZ_1:5
theorem Th6: :: ABCMIZ_1:6
theorem Th7: :: ABCMIZ_1:7
definition
let A be
set ;
func varcl A -> set means :
Def1:
:: ABCMIZ_1:def 1
(
A c= it & ( for
x,
y being
set st
[x,y] in it holds
x c= it ) & ( for
B being
set st
A c= B & ( for
x,
y being
set st
[x,y] in B holds
x c= B ) holds
it c= B ) );
uniqueness
for b1, b2 being set st A c= b1 & ( for x, y being set st [x,y] in b1 holds
x c= b1 ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
b1 c= B ) & A c= b2 & ( for x, y being set st [x,y] in b2 holds
x c= b2 ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
b2 c= B ) holds
b1 = b2
existence
ex b1 being set st
( A c= b1 & ( for x, y being set st [x,y] in b1 holds
x c= b1 ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
b1 c= B ) )
projectivity
for b1, b2 being set st b2 c= b1 & ( for x, y being set st [x,y] in b1 holds
x c= b1 ) & ( for B being set st b2 c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
b1 c= B ) holds
( b1 c= b1 & ( for x, y being set st [x,y] in b1 holds
x c= b1 ) & ( for B being set st b1 c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
b1 c= B ) )
;
end;
:: deftheorem Def1 defines varcl ABCMIZ_1:def 1 :
for
A being
set for
b2 being
set holds
(
b2 = varcl A iff (
A c= b2 & ( for
x,
y being
set st
[x,y] in b2 holds
x c= b2 ) & ( for
B being
set st
A c= B & ( for
x,
y being
set st
[x,y] in B holds
x c= B ) holds
b2 c= B ) ) );
theorem Th8: :: ABCMIZ_1:8
theorem Th9: :: ABCMIZ_1:9
theorem Th10: :: ABCMIZ_1:10
theorem Th11: :: ABCMIZ_1:11
theorem Th12: :: ABCMIZ_1:12
theorem Th13: :: ABCMIZ_1:13
deffunc H1( set , set ) -> set = { [(varcl A),j] where A is Subset of $2, j is Element of NAT : A is finite } ;
definition
func Vars -> set means :
Def2:
:: ABCMIZ_1:def 2
ex
V being
ManySortedSet of st
(
it = Union V &
V . 0 = { [{} ,i] where i is Element of NAT : verum } & ( for
n being
Nat holds
V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) );
existence
ex b1 being set ex V being ManySortedSet of st
( b1 = Union V & V . 0 = { [{} ,i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) )
uniqueness
for b1, b2 being set st ex V being ManySortedSet of st
( b1 = Union V & V . 0 = { [{} ,i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) ) & ex V being ManySortedSet of st
( b2 = Union V & V . 0 = { [{} ,i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) ) holds
b1 = b2
end;
:: deftheorem Def2 defines Vars ABCMIZ_1:def 2 :
theorem Th14: :: ABCMIZ_1:14
theorem Th15: :: ABCMIZ_1:15
theorem Th16: :: ABCMIZ_1:16
theorem Th17: :: ABCMIZ_1:17
theorem Th18: :: ABCMIZ_1:18
theorem Th19: :: ABCMIZ_1:19
theorem Th20: :: ABCMIZ_1:20
theorem Th21: :: ABCMIZ_1:21
theorem Th22: :: ABCMIZ_1:22
theorem Th23: :: ABCMIZ_1:23
theorem Th24: :: ABCMIZ_1:24
theorem :: ABCMIZ_1:25
theorem Th26: :: ABCMIZ_1:26
theorem Th27: :: ABCMIZ_1:27
theorem :: ABCMIZ_1:28
:: deftheorem Def3 defines QuasiLoci ABCMIZ_1:def 3 :
theorem Th29: :: ABCMIZ_1:29
theorem Th30: :: ABCMIZ_1:30
theorem Th31: :: ABCMIZ_1:31
theorem Th32: :: ABCMIZ_1:32
theorem :: ABCMIZ_1:33
theorem Th34: :: ABCMIZ_1:34
theorem Th35: :: ABCMIZ_1:35
theorem :: ABCMIZ_1:36
:: deftheorem defines a_Type ABCMIZ_1:def 4 :
:: deftheorem defines an_Adj ABCMIZ_1:def 5 :
:: deftheorem defines a_Term ABCMIZ_1:def 6 :
:: deftheorem defines * ABCMIZ_1:def 7 :
:: deftheorem defines non_op ABCMIZ_1:def 8 :
:: deftheorem Def9 defines constructor ABCMIZ_1:def 9 :
:: deftheorem Def10 defines MinConstrSign ABCMIZ_1:def 10 :
:: deftheorem Def11 defines constructor ABCMIZ_1:def 11 :
theorem :: ABCMIZ_1:37
:: deftheorem Def12 defines initialized ABCMIZ_1:def 12 :
definition
let C be
ConstructorSignature;
A1:
the
carrier of
C = {a_Type ,an_Adj ,a_Term }
by Def9;
func a_Type C -> SortSymbol of
C equals :: ABCMIZ_1:def 13
a_Type ;
coherence
a_Type is SortSymbol of C
by A1, ENUMSET1:def 1;
func an_Adj C -> SortSymbol of
C equals :: ABCMIZ_1:def 14
an_Adj ;
coherence
an_Adj is SortSymbol of C
by A1, ENUMSET1:def 1;
func a_Term C -> SortSymbol of
C equals :: ABCMIZ_1:def 15
a_Term ;
coherence
a_Term is SortSymbol of C
by A1, ENUMSET1:def 1;
A2:
{* ,non_op } c= the
carrier' of
C
by Def9;
A3:
* in {* ,non_op }
by TARSKI:def 2;
A4:
non_op in {* ,non_op }
by TARSKI:def 2;
func non_op C -> OperSymbol of
C equals :: ABCMIZ_1:def 16
non_op ;
coherence
non_op is OperSymbol of C
by A2, A4;
func ast C -> OperSymbol of
C equals :: ABCMIZ_1:def 17
* ;
coherence
* is OperSymbol of C
by A2, A3;
end;
:: deftheorem defines a_Type ABCMIZ_1:def 13 :
:: deftheorem defines an_Adj ABCMIZ_1:def 14 :
:: deftheorem defines a_Term ABCMIZ_1:def 15 :
:: deftheorem defines non_op ABCMIZ_1:def 16 :
:: deftheorem defines ast ABCMIZ_1:def 17 :
theorem :: ABCMIZ_1:38
definition
func Modes -> set equals :: ABCMIZ_1:def 18
[:{a_Type },[:QuasiLoci ,NAT :]:];
correctness
coherence
[:{a_Type },[:QuasiLoci ,NAT :]:] is set ;
;
func Attrs -> set equals :: ABCMIZ_1:def 19
[:{an_Adj },[:QuasiLoci ,NAT :]:];
correctness
coherence
[:{an_Adj },[:QuasiLoci ,NAT :]:] is set ;
;
func Funcs -> set equals :: ABCMIZ_1:def 20
[:{a_Term },[:QuasiLoci ,NAT :]:];
correctness
coherence
[:{a_Term },[:QuasiLoci ,NAT :]:] is set ;
;
end;
:: deftheorem defines Modes ABCMIZ_1:def 18 :
:: deftheorem defines Attrs ABCMIZ_1:def 19 :
:: deftheorem defines Funcs ABCMIZ_1:def 20 :
:: deftheorem defines Constructors ABCMIZ_1:def 21 :
theorem :: ABCMIZ_1:39
:: deftheorem defines loci_of ABCMIZ_1:def 22 :
:: deftheorem defines index_of ABCMIZ_1:def 23 :
theorem :: ABCMIZ_1:40
:: deftheorem Def24 defines MaxConstrSign ABCMIZ_1:def 24 :
:: deftheorem Def25 defines MSVars ABCMIZ_1:def 25 :
:: deftheorem defines ground ABCMIZ_1:def 26 :
:: deftheorem Def27 defines compound ABCMIZ_1:def 27 :
:: deftheorem Def28 defines expression ABCMIZ_1:def 28 :
theorem Th41: :: ABCMIZ_1:41
:: deftheorem defines term ABCMIZ_1:def 29 :
theorem Th42: :: ABCMIZ_1:42
:: deftheorem Def30 defines term ABCMIZ_1:def 30 :
theorem Th43: :: ABCMIZ_1:43
theorem Th44: :: ABCMIZ_1:44
theorem Th45: :: ABCMIZ_1:45
definition
let C be
initialized ConstructorSignature;
let o be
OperSymbol of
C;
assume A1:
len (the_arity_of o) = 2
;
let e1,
e2 be
expression of
C;
assume A2:
ex
s1,
s2 being
SortSymbol of
C st
(
s1 = (the_arity_of o) . 1 &
s2 = (the_arity_of o) . 2 &
e1 is
expression of
C,
s1 &
e2 is
expression of
C,
s2 )
;
func o term e1,
e2 -> expression of
C equals :
Def31:
:: ABCMIZ_1:def 31
[o,the carrier of C] -tree <*e1,e2*>;
coherence
[o,the carrier of C] -tree <*e1,e2*> is expression of C
by A1, A2, Th45;
end;
:: deftheorem Def31 defines term ABCMIZ_1:def 31 :
theorem Th46: :: ABCMIZ_1:46
theorem :: ABCMIZ_1:47
:: deftheorem defines OperSymbol ABCMIZ_1:def 32 :
theorem Th48: :: ABCMIZ_1:48
:: deftheorem defines QuasiTerms ABCMIZ_1:def 33 :
theorem :: ABCMIZ_1:49
:: deftheorem defines -term ABCMIZ_1:def 34 :
theorem Th50: :: ABCMIZ_1:50
theorem Th51: :: ABCMIZ_1:51
:: deftheorem Def35 defines -trm ABCMIZ_1:def 35 :
theorem Th52: :: ABCMIZ_1:52
theorem Th53: :: ABCMIZ_1:53
theorem Th54: :: ABCMIZ_1:54
theorem Th55: :: ABCMIZ_1:55
theorem :: ABCMIZ_1:56
theorem Th57: :: ABCMIZ_1:57
theorem Th58: :: ABCMIZ_1:58
:: deftheorem Def36 defines Non ABCMIZ_1:def 36 :
:: deftheorem Def37 defines positive ABCMIZ_1:def 37 :
theorem Th59: :: ABCMIZ_1:59
:: deftheorem Def38 defines negative ABCMIZ_1:def 38 :
theorem Th60: :: ABCMIZ_1:60
theorem Th61: :: ABCMIZ_1:61
theorem Th62: :: ABCMIZ_1:62
:: deftheorem Def39 defines regular ABCMIZ_1:def 39 :
:: deftheorem defines QuasiAdjs ABCMIZ_1:def 40 :
theorem Th63: :: ABCMIZ_1:63
theorem :: ABCMIZ_1:64
theorem Th65: :: ABCMIZ_1:65
theorem Th66: :: ABCMIZ_1:66
theorem Th67: :: ABCMIZ_1:67
theorem :: ABCMIZ_1:68
theorem :: ABCMIZ_1:69
:: deftheorem Def41 defines pure ABCMIZ_1:def 41 :
theorem Th70: :: ABCMIZ_1:70
theorem Th71: :: ABCMIZ_1:71
:: deftheorem defines QuasiTypes ABCMIZ_1:def 42 :
:: deftheorem Def43 defines quasi-type ABCMIZ_1:def 43 :
theorem Th72: :: ABCMIZ_1:72
theorem Th73: :: ABCMIZ_1:73
theorem Th74: :: ABCMIZ_1:74
theorem Th75: :: ABCMIZ_1:75
theorem :: ABCMIZ_1:76
theorem :: ABCMIZ_1:77
theorem :: ABCMIZ_1:78
theorem :: ABCMIZ_1:79
theorem Th80: :: ABCMIZ_1:80
theorem :: ABCMIZ_1:81
:: deftheorem defines ast ABCMIZ_1:def 44 :
theorem :: ABCMIZ_1:82
theorem :: ABCMIZ_1:83
theorem :: ABCMIZ_1:84
definition
let S be non
void Signature;
let X be
V6()
ManySortedSet of ;
let s be
SortSymbol of
S;
func X,
s variables_in -> Function of
(Union the Sorts of (Free S,X)),
(bool (X . s)) means :
Def45:
:: ABCMIZ_1:def 45
for
t being
Element of
(Free S,X) holds
it . t = (S variables_in t) . s;
uniqueness
for b1, b2 being Function of (Union the Sorts of (Free S,X)),(bool (X . s)) st ( for t being Element of (Free S,X) holds b1 . t = (S variables_in t) . s ) & ( for t being Element of (Free S,X) holds b2 . t = (S variables_in t) . s ) holds
b1 = b2
existence
ex b1 being Function of (Union the Sorts of (Free S,X)),(bool (X . s)) st
for t being Element of (Free S,X) holds b1 . t = (S variables_in t) . s
end;
:: deftheorem Def45 defines variables_in ABCMIZ_1:def 45 :
:: deftheorem defines variables_in ABCMIZ_1:def 46 :
:: deftheorem defines vars ABCMIZ_1:def 47 :
theorem :: ABCMIZ_1:85
theorem :: ABCMIZ_1:86
theorem :: ABCMIZ_1:87
theorem Th88: :: ABCMIZ_1:88
theorem Th89: :: ABCMIZ_1:89
theorem :: ABCMIZ_1:90
theorem :: ABCMIZ_1:91
theorem :: ABCMIZ_1:92
theorem Th93: :: ABCMIZ_1:93
theorem Th94: :: ABCMIZ_1:94
theorem :: ABCMIZ_1:95
theorem Th96: :: ABCMIZ_1:96
theorem Th97: :: ABCMIZ_1:97
theorem :: ABCMIZ_1:98
theorem Th99: :: ABCMIZ_1:99
theorem :: ABCMIZ_1:100
:: deftheorem defines variables_in ABCMIZ_1:def 48 :
:: deftheorem defines vars ABCMIZ_1:def 49 :
theorem :: ABCMIZ_1:101
theorem Th102: :: ABCMIZ_1:102
theorem :: ABCMIZ_1:103
theorem Th104: :: ABCMIZ_1:104
theorem :: ABCMIZ_1:105
theorem Th106: :: ABCMIZ_1:106
theorem Th107: :: ABCMIZ_1:107
:: deftheorem Def50 defines ground ABCMIZ_1:def 50 :
theorem Th108: :: ABCMIZ_1:108
:: deftheorem defines VarPoset ABCMIZ_1:def 51 :
theorem Th109: :: ABCMIZ_1:109
theorem Th110: :: ABCMIZ_1:110
theorem Th111: :: ABCMIZ_1:111
theorem Th112: :: ABCMIZ_1:112
theorem :: ABCMIZ_1:113
:: deftheorem defines vars-function ABCMIZ_1:def 52 :
:: deftheorem defines smooth ABCMIZ_1:def 53 :
:: deftheorem Def54 defines with_an_operation_for_each_sort ABCMIZ_1:def 54 :
:: deftheorem Def55 defines with_missing_variables ABCMIZ_1:def 55 :
theorem Th114: :: ABCMIZ_1:114
theorem Th115: :: ABCMIZ_1:115
theorem Th116: :: ABCMIZ_1:116
theorem Th117: :: ABCMIZ_1:117
theorem Th118: :: ABCMIZ_1:118
theorem :: ABCMIZ_1:119
theorem Th120: :: ABCMIZ_1:120
theorem :: ABCMIZ_1:121
theorem Th122: :: ABCMIZ_1:122
theorem Th123: :: ABCMIZ_1:123
theorem Th124: :: ABCMIZ_1:124
theorem :: ABCMIZ_1:125
theorem :: ABCMIZ_1:126
theorem Th127: :: ABCMIZ_1:127
theorem Th128: :: ABCMIZ_1:128
:: deftheorem Def56 defines term-transformation ABCMIZ_1:def 56 :
theorem Th129: :: ABCMIZ_1:129
theorem Th130: :: ABCMIZ_1:130
:: deftheorem defines substitution ABCMIZ_1:def 57 :
:: deftheorem Def58 defines irrelevant ABCMIZ_1:def 58 :
:: deftheorem defines idval ABCMIZ_1:def 59 :
theorem Th131: :: ABCMIZ_1:131
definition
let C be
initialized ConstructorSignature;
let f be
valuation of
C;
func f # -> term-transformation of
C,
MSVars C means :
Def60:
:: ABCMIZ_1:def 60
( ( for
x being
variable holds
( (
x in dom f implies
it . (x -term C) = f . x ) & ( not
x in dom f implies
it . (x -term C) = x -term C ) ) ) & ( for
c being
constructor OperSymbol of
C for
p,
q being
FinSequence of
QuasiTerms C st
len p = len (the_arity_of c) &
q = it * p holds
it . (c -trm p) = c -trm q ) & ( for
a being
expression of
C,
an_Adj C holds
it . ((non_op C) term a) = (non_op C) term (it . a) ) & ( for
a being
expression of
C,
an_Adj C for
t being
expression of
C,
a_Type C holds
it . ((ast C) term a,t) = (ast C) term (it . a),
(it . t) ) );
existence
ex b1 being term-transformation of C, MSVars C st
( ( for x being variable holds
( ( x in dom f implies b1 . (x -term C) = f . x ) & ( not x in dom f implies b1 . (x -term C) = x -term C ) ) ) & ( for c being constructor OperSymbol of C
for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = b1 * p holds
b1 . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds b1 . ((non_op C) term a) = (non_op C) term (b1 . a) ) & ( for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds b1 . ((ast C) term a,t) = (ast C) term (b1 . a),(b1 . t) ) )
correctness
uniqueness
for b1, b2 being term-transformation of C, MSVars C st ( for x being variable holds
( ( x in dom f implies b1 . (x -term C) = f . x ) & ( not x in dom f implies b1 . (x -term C) = x -term C ) ) ) & ( for c being constructor OperSymbol of C
for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = b1 * p holds
b1 . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds b1 . ((non_op C) term a) = (non_op C) term (b1 . a) ) & ( for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds b1 . ((ast C) term a,t) = (ast C) term (b1 . a),(b1 . t) ) & ( for x being variable holds
( ( x in dom f implies b2 . (x -term C) = f . x ) & ( not x in dom f implies b2 . (x -term C) = x -term C ) ) ) & ( for c being constructor OperSymbol of C
for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = b2 * p holds
b2 . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds b2 . ((non_op C) term a) = (non_op C) term (b2 . a) ) & ( for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds b2 . ((ast C) term a,t) = (ast C) term (b2 . a),(b2 . t) ) holds
b1 = b2;
end;
:: deftheorem Def60 defines # ABCMIZ_1:def 60 :
:: deftheorem defines at ABCMIZ_1:def 61 :
:: deftheorem Def62 defines at ABCMIZ_1:def 62 :
:: deftheorem defines at ABCMIZ_1:def 63 :
theorem :: ABCMIZ_1:132
theorem :: ABCMIZ_1:133
theorem :: ABCMIZ_1:134
theorem :: ABCMIZ_1:135
theorem :: ABCMIZ_1:136
theorem Th137: :: ABCMIZ_1:137
theorem :: ABCMIZ_1:138
theorem Th139: :: ABCMIZ_1:139
theorem :: ABCMIZ_1:140
theorem :: ABCMIZ_1:141
theorem :: ABCMIZ_1:142
theorem :: ABCMIZ_1:143
:: deftheorem defines at ABCMIZ_1:def 64 :
theorem Th144: :: ABCMIZ_1:144
theorem Th145: :: ABCMIZ_1:145
theorem :: ABCMIZ_1:146
:: deftheorem defines at ABCMIZ_1:def 65 :
theorem :: ABCMIZ_1:147
theorem :: ABCMIZ_1:148
:: deftheorem Def66 defines at ABCMIZ_1:def 66 :
theorem Th149: :: ABCMIZ_1:149
theorem Th150: :: ABCMIZ_1:150
theorem :: ABCMIZ_1:151