:: Towards the construction of a model of Mizar concepts
:: by Grzegorz Bancerek
::
:: Received April 21, 2008
:: Copyright (c) 2008 Association of Mizar Users
theorem ThF0: :: ABCMIZ_1:1
theorem :: ABCMIZ_1:2
theorem Th89: :: ABCMIZ_1:3
theorem Lem'id: :: ABCMIZ_1:4
theorem Th90: :: ABCMIZ_1:5
theorem Th1A: :: ABCMIZ_1:6
theorem LemExp: :: ABCMIZ_1:7
definition
let A be
set ;
func varcl A -> set means :
VARCL:
:: 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 VARCL 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 Th11: :: ABCMIZ_1:8
theorem Th13: :: ABCMIZ_1:9
theorem Th14: :: ABCMIZ_1:10
theorem Th10: :: ABCMIZ_1:11
theorem Th8: :: ABCMIZ_1:12
theorem Th9: :: 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 :
VARSdef:
:: ABCMIZ_1:def 2
ex
V being
ManySortedSet of
NAT 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 NAT 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 NAT 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 NAT 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 VARSdef defines Vars ABCMIZ_1:def 2 :
theorem Lem1: :: ABCMIZ_1:14
theorem Lem2: :: ABCMIZ_1:15
theorem Th15: :: ABCMIZ_1:16
theorem Lem3: :: ABCMIZ_1:17
theorem Th16: :: ABCMIZ_1:18
theorem Th17: :: ABCMIZ_1:19
theorem Lem4: :: ABCMIZ_1:20
theorem Lem5: :: ABCMIZ_1:21
theorem Lem6: :: ABCMIZ_1:22
theorem Lem7: :: ABCMIZ_1:23
theorem Th18: :: ABCMIZ_1:24
theorem :: ABCMIZ_1:25
theorem Lem8: :: ABCMIZ_1:26
theorem Th82: :: ABCMIZ_1:27
theorem :: ABCMIZ_1:28
:: deftheorem QuasiLociDef defines QuasiLoci ABCMIZ_1:def 3 :
theorem Th31: :: ABCMIZ_1:29
theorem Th32: :: ABCMIZ_1:30
theorem Th7: :: ABCMIZ_1:31
theorem Th6: :: ABCMIZ_1:32
theorem :: ABCMIZ_1:33
theorem Th33: :: ABCMIZ_1:34
theorem Th34: :: 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 CONSTRSIGN defines constructor ABCMIZ_1:def 9 :
:: deftheorem MINdef defines MinConstrSign ABCMIZ_1:def 10 :
:: deftheorem CNSTR2 defines constructor ABCMIZ_1:def 11 :
theorem :: ABCMIZ_1:37
:: deftheorem INITIALIZED defines initialized ABCMIZ_1:def 12 :
definition
let C be
ConstructorSignature;
A1:
the
carrier of
C = {a_Type ,an_Adj ,a_Term }
by CONSTRSIGN;
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 CONSTRSIGN;
A3:
(
* in {* ,non_op } &
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, A3;
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 MAXdef defines MaxConstrSign ABCMIZ_1:def 24 :
:: deftheorem MSVARS defines MSVars ABCMIZ_1:def 25 :
:: deftheorem defines ground ABCMIZ_1:def 26 :
:: deftheorem COMP defines compound ABCMIZ_1:def 27 :
:: deftheorem ELEMENT defines expression ABCMIZ_1:def 28 :
theorem Th42: :: ABCMIZ_1:41
:: deftheorem defines term ABCMIZ_1:def 29 :
theorem Th43a: :: ABCMIZ_1:42
:: deftheorem TERM1 defines term ABCMIZ_1:def 30 :
theorem ThNon: :: ABCMIZ_1:43
theorem ThNon': :: ABCMIZ_1:44
theorem Th43b: :: ABCMIZ_1:45
definition
let C be
initialized ConstructorSignature;
let o be
OperSymbol of
C;
assume A:
len (the_arity_of o) = 2
;
let e1,
e2 be
expression of
C;
assume B:
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 :
TERM2:
:: 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 A, B, Th43b;
end;
:: deftheorem TERM2 defines term ABCMIZ_1:def 31 :
theorem ThAst: :: ABCMIZ_1:46
theorem :: ABCMIZ_1:47
:: deftheorem defines OperSymbol ABCMIZ_1:def 32 :
theorem Th90A: :: ABCMIZ_1:48
:: deftheorem defines QuasiTerms ABCMIZ_1:def 33 :
theorem :: ABCMIZ_1:49
:: deftheorem defines -term ABCMIZ_1:def 34 :
theorem ThT0: :: ABCMIZ_1:50
theorem Th83: :: ABCMIZ_1:51
:: deftheorem TERM defines -trm ABCMIZ_1:def 35 :
theorem Th43c: :: ABCMIZ_1:52
theorem Th100: :: ABCMIZ_1:53
theorem ThDiff01: :: ABCMIZ_1:54
theorem ThDiff02: :: ABCMIZ_1:55
theorem :: ABCMIZ_1:56
theorem ThNon2: :: ABCMIZ_1:57
theorem ThAst2: :: ABCMIZ_1:58
:: deftheorem NON'OPA defines Non ABCMIZ_1:def 36 :
:: deftheorem POSITIVE defines positive ABCMIZ_1:def 37 :
theorem Th44: :: ABCMIZ_1:59
:: deftheorem NEGATIVE defines negative ABCMIZ_1:def 38 :
theorem Th45g: :: ABCMIZ_1:60
theorem Th45: :: ABCMIZ_1:61
theorem Th44b: :: ABCMIZ_1:62
:: deftheorem REG defines regular ABCMIZ_1:def 39 :
:: deftheorem defines QuasiAdjs ABCMIZ_1:def 40 :
theorem Th52: :: ABCMIZ_1:63
theorem :: ABCMIZ_1:64
theorem ThPos: :: ABCMIZ_1:65
theorem ThPos2: :: ABCMIZ_1:66
theorem Th46: :: ABCMIZ_1:67
theorem :: ABCMIZ_1:68
theorem :: ABCMIZ_1:69
:: deftheorem PURE defines pure ABCMIZ_1:def 41 :
theorem ThP: :: ABCMIZ_1:70
theorem ThP2: :: ABCMIZ_1:71
:: deftheorem defines QuasiTypes ABCMIZ_1:def 42 :
:: deftheorem QUASITYPE defines quasi-type ABCMIZ_1:def 43 :
theorem Th54: :: ABCMIZ_1:72
theorem Th55: :: ABCMIZ_1:73
theorem ThPure: :: ABCMIZ_1:74
theorem ThPure2: :: ABCMIZ_1:75
theorem :: ABCMIZ_1:76
theorem :: ABCMIZ_1:77
theorem :: ABCMIZ_1:78
theorem :: ABCMIZ_1:79
theorem Th59: :: 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 the
carrier of
S;
let s be
SortSymbol of
S;
func X,
s variables_in -> Function of
Union the
Sorts of
(Free S,X),
bool (X . s) means :
VARS'INF:
:: 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 VARS'INF 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 Th84: :: ABCMIZ_1:88
theorem Th84': :: ABCMIZ_1:89
theorem :: ABCMIZ_1:90
theorem :: ABCMIZ_1:91
theorem :: ABCMIZ_1:92
theorem Aux1: :: ABCMIZ_1:93
theorem Aux1': :: ABCMIZ_1:94
theorem :: ABCMIZ_1:95
theorem Aux2: :: ABCMIZ_1:96
theorem Aux2': :: ABCMIZ_1:97
theorem :: ABCMIZ_1:98
theorem Th71: :: 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 Th72: :: ABCMIZ_1:102
theorem :: ABCMIZ_1:103
theorem ThAA: :: ABCMIZ_1:104
theorem :: ABCMIZ_1:105
theorem ThAAe: :: ABCMIZ_1:106
theorem ThG: :: ABCMIZ_1:107
:: deftheorem GROUND2 defines ground ABCMIZ_1:def 50 :
theorem ThG2: :: ABCMIZ_1:108
:: deftheorem defines VarPoset ABCMIZ_1:def 51 :
theorem Th22: :: ABCMIZ_1:109
theorem Th21: :: ABCMIZ_1:110
theorem Th23: :: ABCMIZ_1:111
theorem Th24: :: ABCMIZ_1:112
theorem :: ABCMIZ_1:113
:: deftheorem defines vars-function ABCMIZ_1:def 52 :
:: deftheorem defines smooth ABCMIZ_1:def 53 :
:: deftheorem WOFES defines with_an_operation_for_each_sort ABCMIZ_1:def 54 :
:: deftheorem WMV defines with_missing_variables ABCMIZ_1:def 55 :
theorem LemMV: :: ABCMIZ_1:114
theorem LemTerm0: :: ABCMIZ_1:115
theorem LemTS0: :: ABCMIZ_1:116
theorem LemX: :: ABCMIZ_1:117
theorem LemY0: :: ABCMIZ_1:118
theorem :: ABCMIZ_1:119
theorem ThTNT: :: ABCMIZ_1:120
theorem :: ABCMIZ_1:121
theorem LemTerm: :: ABCMIZ_1:122
theorem LemNTerm: :: ABCMIZ_1:123
theorem LemFT: :: ABCMIZ_1:124
theorem :: ABCMIZ_1:125
theorem :: ABCMIZ_1:126
theorem LemArr: :: ABCMIZ_1:127
theorem LemTS: :: ABCMIZ_1:128
:: deftheorem TT defines term-transformation ABCMIZ_1:def 56 :
theorem ThTr: :: ABCMIZ_1:129
theorem ThTr2: :: ABCMIZ_1:130
:: deftheorem defines substitution ABCMIZ_1:def 57 :
:: deftheorem IRR defines irrelevant ABCMIZ_1:def 58 :
:: deftheorem defines idval ABCMIZ_1:def 59 :
theorem ThIV: :: ABCMIZ_1:131
definition
let C be
initialized ConstructorSignature;
let f be
valuation of
C;
func f # -> term-transformation of
C,
MSVars C means :
SUBST:
:: 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 SUBST defines # ABCMIZ_1:def 60 :
:: deftheorem defines at ABCMIZ_1:def 61 :
:: deftheorem PF defines at ABCMIZ_1:def 62 :
:: deftheorem defines at ABCMIZ_1:def 63 :
theorem :: ABCMIZ_1:132
theorem :: ABCMIZ_1:133
theorem ThS1: :: ABCMIZ_1:134
theorem :: ABCMIZ_1:135
theorem :: ABCMIZ_1:136
theorem ThS2': :: ABCMIZ_1:137
theorem :: ABCMIZ_1:138
theorem ThS2: :: 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 ThZ0: :: ABCMIZ_1:144
theorem ThZ1: :: ABCMIZ_1:145
theorem :: ABCMIZ_1:146
:: deftheorem defines at ABCMIZ_1:def 65 :
theorem :: ABCMIZ_1:147
theorem :: ABCMIZ_1:148
:: deftheorem SUBST2 defines at ABCMIZ_1:def 66 :
theorem ThS3: :: ABCMIZ_1:149
theorem ThZ3: :: ABCMIZ_1:150
theorem :: ABCMIZ_1:151