:: A Model of Mizar Concepts -- Unification
:: by Grzegorz Bancerek
::
:: Received November 20, 2009
:: Copyright (c) 2009-2021 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 TARSKI, QC_LANG3, PBOOLE, MSUALG_1, CATALG_1, FINSEQ_1, XBOOLE_0,
ZFMISC_1, ARYTM_3, CARD_1, NAT_1, NUMBERS, XXREAL_0, ZF_LANG1, ORDINAL1,
TREES_A, ABIAN, CARD_3, MEMBER_1, FINSET_1, FUNCOP_1, FUNCT_1, TREES_4,
TREES_2, MSATERM, RELAT_1, MCART_1, MSAFREE, ZF_MODEL, AOFA_000,
FINSEQ_2, PARTFUN1, QC_LANG1, FUNCT_2, ORDINAL4, CAT_3, TREES_3,
ABCMIZ_0, ABCMIZ_1, ABCMIZ_A, STRUCT_0, FACIRC_1, INSTALG1, MSUALG_2,
COMPUT_1, BINTREE1, TREES_9, ARYTM_1, FUNCT_6, SUBSET_1, MARGREL1,
SETLIM_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, DOMAIN_1,
RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FACIRC_1, ENUMSET1, FUNCOP_1,
XCMPLX_0, XXREAL_0, ORDINAL1, NAT_D, MCART_1, FINSET_1, CARD_1, NUMBERS,
CARD_3, FINSEQ_1, FINSEQ_2, FINSEQ_4, FUNCT_6, TREES_1, TREES_2, TREES_3,
TREES_4, TREES_9, PBOOLE, STRUCT_0, MSUALG_1, MSUALG_2, MSAFREE,
EQUATION, MSATERM, INSTALG1, CATALG_1, MSAFREE3, AOFA_000, ABCMIZ_1;
constructors RELSET_1, DOMAIN_1, WELLORD2, TREES_9, EQUATION, NAT_D, FINSEQ_4,
CATALG_1, FACIRC_1, ABCMIZ_1, PRE_POLY, XTUPLE_0, XFAMILY;
registrations XBOOLE_0, SUBSET_1, XREAL_0, ORDINAL1, FUNCT_1, FINSET_1,
STRUCT_0, PBOOLE, MSUALG_2, FINSEQ_1, NAT_1, CARD_1, TREES_3, TREES_2,
FUNCOP_1, RELAT_1, INDEX_1, INSTALG1, MSAFREE3, WAYBEL26, FACIRC_1,
ABCMIZ_1, MSATERM, RELSET_1, XTUPLE_0;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
begin :: Preliminary
reserve i,j for Nat;
::$CT
scheme :: ABCMIZ_A:sch 1
MinimalElement{X() -> finite non empty set, R[set,set]}:
ex x being set st x in X() &
for y being set st y in X() holds not R[y,x]
provided
for x,y being set st x in X() & y in X() & R[x,y] holds not R[y,x] and
for x,y,z being set st x in X() & y in X() & z in X() & R[x,y] & R[y,z]
holds R[x,z];
scheme :: ABCMIZ_A:sch 2
FiniteC{X() -> finite set, P[set]}:
P[X()]
provided
for A being Subset of X() st for B being set st B c< A holds P[B] holds P[A];
scheme :: ABCMIZ_A:sch 3
Numeration{X() -> finite set, R[set, set]}:
ex s being one-to-one FinSequence st rng s = X() &
for i,j st i in dom s & j in dom s & R[s.i, s.j] holds i < j
provided
for x,y being set st x in X() & y in X() & R[x,y] holds not R[y,x] and
for x,y,z being set st x in X() & y in X() & z in X() & R[x,y] & R[y,z]
holds R[x,z];
theorem :: ABCMIZ_A:2
for x being variable holds varcl vars x = vars x;
theorem :: ABCMIZ_A:3
for C being initialized ConstructorSignature for e being expression of C holds
e is compound iff not ex x being Element of Vars st e = x-term C;
begin :: Standardized Constructor Signature
registration
cluster empty for quasi-loci;
end;
definition
let C be ConstructorSignature;
attr C is standardized means
:: ABCMIZ_A:def 1
for o being OperSymbol of C st o is constructor holds o in Constructors &
o`1 = the_result_sort_of o &
card o`2`1 = len the_arity_of o;
end;
theorem :: ABCMIZ_A:4
for C being ConstructorSignature st C is standardized
for o being OperSymbol of C
holds o is constructor iff o in Constructors;
registration
cluster MaxConstrSign -> standardized;
end;
registration
cluster initialized standardized strict for ConstructorSignature;
end;
definition
let C be initialized standardized ConstructorSignature;
let c be constructor OperSymbol of C;
func loci_of c -> quasi-loci equals
:: ABCMIZ_A:def 2
c`2`1;
end;
registration
let C be ConstructorSignature;
cluster constructor for Subsignature of C;
end;
registration
let C be initialized ConstructorSignature;
cluster initialized for constructor Subsignature of C;
end;
registration
let C be standardized ConstructorSignature;
cluster -> standardized for constructor Subsignature of C;
end;
theorem :: ABCMIZ_A:5
for S1,S2 being standardized ConstructorSignature
st the carrier' of S1 = the carrier' of S2
holds the ManySortedSign of S1 = the ManySortedSign of S2;
theorem :: ABCMIZ_A:6
for C being ConstructorSignature holds
C is standardized iff C is Subsignature of MaxConstrSign;
registration
let C be initialized ConstructorSignature;
cluster non compound for quasi-term of C;
end;
registration
cluster -> pair for Element of Vars;
end;
theorem :: ABCMIZ_A:7
for x being Element of Vars st vars x is natural holds vars x = 0;
theorem :: ABCMIZ_A:8
Vars misses Constructors;
theorem :: ABCMIZ_A:9
for x being Element of Vars holds x <> * & x <> non_op;
theorem :: ABCMIZ_A:10
for C being standardized ConstructorSignature holds
Vars misses the carrier' of C;
theorem :: ABCMIZ_A:11 :: see ABCMIZ_1:51
for C being initialized standardized ConstructorSignature
for e being expression of C
holds
(ex x being Element of Vars st e = x-term C & e.{} = [x, a_Term]) or
(ex o being OperSymbol of C st e.{} = [o, the carrier of C] &
( o in Constructors or o = * or o = non_op ));
registration
let C be initialized standardized ConstructorSignature;
let e be expression of C;
cluster e.{} -> pair;
end;
theorem :: ABCMIZ_A:12
for C being initialized ConstructorSignature for e being expression of C
for o being OperSymbol of C st e.{} = [o, the carrier of C]
holds
e is expression of C, the_result_sort_of o;
theorem :: ABCMIZ_A:13
for C being initialized standardized ConstructorSignature
for e being expression of C
holds
( (e.{})`1 = * implies e is expression of C, a_Type C ) &
( (e.{})`1 = non_op implies e is expression of C, an_Adj C );
theorem :: ABCMIZ_A:14
for C being initialized standardized ConstructorSignature
for e being expression of C
holds
(e.{})`1 in Vars & (e.{})`2 = a_Term & e is quasi-term of C or
(e.{})`2 = the carrier of C &
( (e.{})`1 in Constructors & (e.{})`1 in the carrier' of C or
(e.{})`1 = * or (e.{})`1 = non_op );
theorem :: ABCMIZ_A:15
for C being initialized standardized ConstructorSignature
for e being expression of C
st (e.{})`1 in Constructors
holds e in (the Sorts of Free(C, MSVars C)).(e.{})`1`1;
theorem :: ABCMIZ_A:16
for C being initialized standardized ConstructorSignature
for e being expression of C
holds not (e.{})`1 in Vars iff (e.{})`1 is OperSymbol of C;
theorem :: ABCMIZ_A:17
for C being initialized standardized ConstructorSignature
for e being expression of C
st (e.{})`1 in Vars
ex x being Element of Vars st x = (e.{})`1 & e = x-term C;
theorem :: ABCMIZ_A:18
for C being initialized standardized ConstructorSignature
for e being expression of C
st (e.{})`1 = *
ex a being expression of C, an_Adj C, q being expression of C, a_Type C st
e = [*,3]-tree(a,q);
theorem :: ABCMIZ_A:19
for C being initialized standardized ConstructorSignature
for e being expression of C
st (e.{})`1 = non_op
ex a being expression of C, an_Adj C st e = [non_op,3]-tree a;
theorem :: ABCMIZ_A:20
for C being initialized standardized ConstructorSignature
for e being expression of C
st (e.{})`1 in Constructors
ex o being OperSymbol of C st o = (e.{})`1 & the_result_sort_of o = o`1 &
e is expression of C, the_result_sort_of o;
theorem :: ABCMIZ_A:21
for C being initialized standardized ConstructorSignature
for t being quasi-term of C holds
t is compound iff (t.{})`1 in Constructors & (t.{})`1`1 = a_Term;
theorem :: ABCMIZ_A:22
for C being initialized standardized ConstructorSignature
for t being expression of C holds
t is non compound quasi-term of C iff (t.{})`1 in Vars;
theorem :: ABCMIZ_A:23
for C being initialized standardized ConstructorSignature
for t being expression of C holds
t is quasi-term of C iff
(t.{})`1 in Constructors & (t.{})`1`1 = a_Term or (t.{})`1 in Vars;
theorem :: ABCMIZ_A:24
for C being initialized standardized ConstructorSignature
for a being expression of C holds
a is positive quasi-adjective of C iff
(a .{})`1 in Constructors & (a .{})`1`1 = an_Adj;
theorem :: ABCMIZ_A:25
for C being initialized standardized ConstructorSignature
for a being quasi-adjective of C holds
a is negative iff (a .{})`1 = non_op;
theorem :: ABCMIZ_A:26
for C being initialized standardized ConstructorSignature
for t being expression of C holds
t is pure expression of C, a_Type C iff
(t.{})`1 in Constructors & (t.{})`1`1 = a_Type;
begin :: Expressions
reserve i,j for Nat,
x for variable,
l for quasi-loci;
definition
mode expression is expression of MaxConstrSign;
mode valuation is valuation of MaxConstrSign;
mode quasi-adjective is quasi-adjective of MaxConstrSign;
func QuasiAdjs -> Subset of Free(MaxConstrSign, MSVars MaxConstrSign) equals
:: ABCMIZ_A:def 3
QuasiAdjs MaxConstrSign;
mode quasi-term is quasi-term of MaxConstrSign;
func QuasiTerms -> Subset of Free(MaxConstrSign, MSVars MaxConstrSign) equals
:: ABCMIZ_A:def 4
QuasiTerms MaxConstrSign;
mode quasi-type is quasi-type of MaxConstrSign;
func QuasiTypes -> set equals
:: ABCMIZ_A:def 5
QuasiTypes MaxConstrSign;
end;
registration
cluster QuasiAdjs -> non empty;
cluster QuasiTerms -> non empty;
cluster QuasiTypes -> non empty;
end;
definition
redefine func Modes -> non empty Subset of Constructors;
redefine func Attrs -> non empty Subset of Constructors;
redefine func Funcs -> non empty Subset of Constructors;
end;
reserve C for initialized ConstructorSignature,
c for constructor OperSymbol of C;
definition
func set-constr -> Element of Modes equals
:: ABCMIZ_A:def 6
[a_Type,[{},0]];
end;
theorem :: ABCMIZ_A:27
kind_of set-constr = a_Type & loci_of set-constr = {} &
index_of set-constr = 0;
theorem :: ABCMIZ_A:28
Constructors = [:{a_Type, an_Adj, a_Term}, [:QuasiLoci, NAT:]:];
theorem :: ABCMIZ_A:29
[rng l, i] in Vars & l^<*[rng l,i]*> is quasi-loci;
theorem :: ABCMIZ_A:30
ex l st len l = i;
theorem :: ABCMIZ_A:31
for X being finite Subset of Vars ex l st rng l = varcl X;
theorem :: ABCMIZ_A:32 :: to mozna uogolnic na X zamkniety na poddrzewa
:: (troche dodatkowych pojec i twierdzen)
for S being non empty non void ManySortedSign
for Y being non empty-yielding ManySortedSet of the carrier of S
for X,o being set, p being DTree-yielding FinSequence
st ex C st X = Union the Sorts of Free(S, Y)
holds o-tree p in X implies p is FinSequence of X;
definition
let C;
let e be expression of C;
mode subexpression of e -> expression of C means
:: ABCMIZ_A:def 7
it in Subtrees e;
func constrs e -> set equals
:: ABCMIZ_A:def 8
(proj1 rng e)/\the set of all o where o is constructor OperSymbol of C;
end;
definition
let S be non empty non void ManySortedSign;
let X be non empty-yielding ManySortedSet of the carrier of S;
let e be Element of Free(S,X);
func main-constr e -> set
equals
:: ABCMIZ_A:def 9 :: dobre dla zestandaryzowanych (nie ma def)
(e.{})`1 if e is compound otherwise {};
func args e -> DTree-yielding FinSequence means
:: ABCMIZ_A:def 10
e = (e.{})-tree it;
end;
definition
let S be non empty non void ManySortedSign;
let X be non empty-yielding ManySortedSet of the carrier of S;
let e be Element of Free(S,X);
redefine func args e -> FinSequence of Free(S, X);
end;
theorem :: ABCMIZ_A:33
for C for e being expression of C holds e is subexpression of e;
theorem :: ABCMIZ_A:34
main-constr (x -term C) = {};
theorem :: ABCMIZ_A:35
for c being constructor OperSymbol of C
for p being FinSequence of QuasiTerms C st len p = len the_arity_of c
holds main-constr (c-trm p) = c;
definition
let C;
let e be expression of C;
attr e is constructor means
:: ABCMIZ_A:def 11
e is compound & main-constr e is constructor OperSymbol of C;
end;
registration
let C;
cluster constructor -> compound for expression of C;
end;
registration
let C;
cluster constructor for expression of C;
end;
registration
let C;
let e be constructor expression of C;
cluster constructor for subexpression of e;
end;
registration
let S be non void Signature;
let X be non empty-yielding ManySortedSet of S;
let t be Element of Free(S,X);
cluster rng t -> Relation-like;
end;
theorem :: ABCMIZ_A:36
for e being constructor expression of C holds main-constr e in constrs e;
begin :: Arity
reserve a,a9 for quasi-adjective,
t,t1,t2 for quasi-term,
T for quasi-type,
c for Element of Constructors;
definition
let C be non void Signature;
attr C is arity-rich means
:: ABCMIZ_A:def 12
for n being Nat, s being SortSymbol of C holds
{o where o is OperSymbol of C: the_result_sort_of o = s &
len the_arity_of o = n} is infinite;
let o be OperSymbol of C;
attr o is nullary means
:: ABCMIZ_A:def 13
the_arity_of o = {};
attr o is unary means
:: ABCMIZ_A:def 14
len the_arity_of o = 1;
attr o is binary means
:: ABCMIZ_A:def 15
len the_arity_of o = 2;
end;
theorem :: ABCMIZ_A:37
for C being non void Signature for o being OperSymbol of C holds
(o is nullary implies o is not unary) &
(o is nullary implies o is not binary) &
(o is unary implies o is not binary);
registration
let C be ConstructorSignature;
cluster non_op C -> unary;
cluster ast C -> binary;
end;
registration
let C be ConstructorSignature;
cluster nullary -> constructor for OperSymbol of C;
end;
theorem :: ABCMIZ_A:38
for C being ConstructorSignature holds C is initialized iff
ex m being OperSymbol of a_Type C, a being OperSymbol of an_Adj C st
m is nullary & a is nullary;
registration
let C be initialized ConstructorSignature;
cluster nullary constructor for OperSymbol of a_Type C;
cluster nullary constructor for OperSymbol of an_Adj C;
end;
registration
let C be initialized ConstructorSignature;
cluster nullary constructor for OperSymbol of C;
end;
registration
cluster arity-rich -> with_an_operation_for_each_sort for
non void Signature;
cluster arity-rich -> initialized for ConstructorSignature;
end;
registration
cluster MaxConstrSign -> arity-rich;
end;
registration
cluster arity-rich initialized for ConstructorSignature;
end;
registration
let C be arity-rich ConstructorSignature;
let s be SortSymbol of C;
cluster nullary constructor for OperSymbol of s;
cluster unary constructor for OperSymbol of s;
cluster binary constructor for OperSymbol of s;
end;
registration
let C be arity-rich ConstructorSignature;
cluster unary constructor for OperSymbol of C;
cluster binary constructor for OperSymbol of C;
end;
theorem :: ABCMIZ_A:39
for o being nullary OperSymbol of C holds
[o, the carrier of C]-tree {} is expression of C, the_result_sort_of o;
definition
let C be initialized ConstructorSignature;
let m be nullary constructor OperSymbol of a_Type C;
redefine func m term -> pure expression of C, a_Type C;
end;
definition
let c be Element of Constructors;
func @c -> constructor OperSymbol of MaxConstrSign equals
:: ABCMIZ_A:def 16
c;
end;
definition
let m be Element of Modes;
redefine func @m -> constructor OperSymbol of a_Type MaxConstrSign;
end;
registration
cluster @set-constr -> nullary;
end;
theorem :: ABCMIZ_A:40
the_arity_of @set-constr = {};
definition
func set-type -> quasi-type equals
:: ABCMIZ_A:def 17
({}QuasiAdjs MaxConstrSign) ast ((@set-constr) term);
end;
theorem :: ABCMIZ_A:41
adjs set-type = {} & the_base_of set-type = (@set-constr) term;
definition
let l be FinSequence of Vars;
func args l -> FinSequence of QuasiTerms MaxConstrSign means
:: ABCMIZ_A:def 18
len it = len l & for i st i in dom l holds it.i = (l/.i)-term MaxConstrSign;
end;
definition
let c;
func base_exp_of c -> expression equals
:: ABCMIZ_A:def 19
(@c)-trm args loci_of c;
end;
theorem :: ABCMIZ_A:42
for o being OperSymbol of MaxConstrSign holds
o is constructor iff o in Constructors;
theorem :: ABCMIZ_A:43
for m being nullary OperSymbol of MaxConstrSign holds
main-constr (m term) = m;
theorem :: ABCMIZ_A:44
for m being unary constructor OperSymbol of MaxConstrSign
for t holds main-constr (m term t) = m;
theorem :: ABCMIZ_A:45
for a holds main-constr ((non_op MaxConstrSign)term a) = non_op;
theorem :: ABCMIZ_A:46
for m being binary constructor OperSymbol of MaxConstrSign
for t1,t2 holds main-constr (m term(t1,t2)) = m;
theorem :: ABCMIZ_A:47
for q being expression of MaxConstrSign, a_Type MaxConstrSign
for a holds main-constr ((ast MaxConstrSign)term(a,q)) = *;
definition
let T be quasi-type;
func constrs T -> set equals
:: ABCMIZ_A:def 20
(constrs the_base_of T) \/ union {constrs a: a in adjs T};
end;
theorem :: ABCMIZ_A:48
for q being pure expression of MaxConstrSign, a_Type MaxConstrSign
for A being finite Subset of QuasiAdjs MaxConstrSign holds
constrs(A ast q) = (constrs q) \/ union {constrs a: a in A};
theorem :: ABCMIZ_A:49
constrs(a ast T) = (constrs a) \/ (constrs T);
begin :: Unification
definition
let C be initialized ConstructorSignature;
let t,p be expression of C;
pred t matches_with p means
:: ABCMIZ_A:def 21
ex f being valuation of C st t = p at f;
reflexivity;
end;
theorem :: ABCMIZ_A:50
for t1,t2,t3 being expression of C st t1 matches_with t2 & t2 matches_with t3
holds t1 matches_with t3;
definition
let C be initialized ConstructorSignature;
let A,B be Subset of QuasiAdjs C;
pred A matches_with B means
:: ABCMIZ_A:def 22
ex f being valuation of C st B at f c= A;
reflexivity;
end;
theorem :: ABCMIZ_A:51
for A1,A2,A3 being Subset of QuasiAdjs C
st A1 matches_with A2 & A2 matches_with A3
holds A1 matches_with A3;
definition
let C be initialized ConstructorSignature;
let T,P be quasi-type of C;
pred T matches_with P means
:: ABCMIZ_A:def 23
ex f being valuation of C st
(adjs P) at f c= adjs T & (the_base_of P) at f = the_base_of T;
reflexivity;
end;
theorem :: ABCMIZ_A:52
for T1,T2,T3 being quasi-type of C st T1 matches_with T2 & T2 matches_with T3
holds T1 matches_with T3;
definition
let C be initialized ConstructorSignature;
let t1,t2 be expression of C;
let f be valuation of C;
::$N Unification of Mizar terms
pred f unifies t1,t2 means
:: ABCMIZ_A:def 24
t1 at f = t2 at f;
end;
theorem :: ABCMIZ_A:53
for t1,t2 being expression of C for f being valuation of C st f unifies t1,t2
holds f unifies t2,t1;
definition
let C be initialized ConstructorSignature;
let t1,t2 be expression of C;
pred t1,t2 are_unifiable means
:: ABCMIZ_A:def 25
ex f being valuation of C st f unifies t1,t2;
reflexivity;
symmetry;
end;
definition
let C be initialized ConstructorSignature;
let t1,t2 be expression of C;
pred t1,t2 are_weakly-unifiable means
:: ABCMIZ_A:def 26
ex g being irrelevant one-to-one valuation of C
st variables_in t2 c= dom g & t1,t2 at g are_unifiable;
reflexivity;
:: symmetry;
end;
:: theorem
:: for t1,t2 being expression of C st t1 matches_with t2
:: holds t1,t2 are_weakly-unifiable;
theorem :: ABCMIZ_A:54
for t1,t2 being expression of C st t1,t2 are_unifiable
holds t1,t2 are_weakly-unifiable;
definition
let C be initialized ConstructorSignature;
let t,t1,t2 be expression of C;
pred t is_a_unification_of t1,t2 means
:: ABCMIZ_A:def 27
ex f being valuation of C st f unifies t1,t2 & t = t1 at f;
end;
theorem :: ABCMIZ_A:55
for t1,t2,t being expression of C st t is_a_unification_of t1,t2
holds t is_a_unification_of t2,t1;
theorem :: ABCMIZ_A:56
for t1,t2,t being expression of C st t is_a_unification_of t1,t2
holds t matches_with t1 & t matches_with t2;
definition
let C be initialized ConstructorSignature;
let t,t1,t2 be expression of C;
pred t is_a_general-unification_of t1,t2 means
:: ABCMIZ_A:def 28
t is_a_unification_of t1,t2 &
for u being expression of C st u is_a_unification_of t1,t2
holds u matches_with t;
end;
:: theorem
:: for t1,t2 being expression of C st t1,t2 are_unifiable
:: ex t being expression of C st t is_a_general-unification_of t1,t2;
begin :: Type distribution
theorem :: ABCMIZ_A:57
for n being Nat for s being SortSymbol of MaxConstrSign
ex m being constructor OperSymbol of s
st len the_arity_of m = n;
theorem :: ABCMIZ_A:58
for l for s being SortSymbol of MaxConstrSign
for m being constructor OperSymbol of s st len the_arity_of m = len l
holds variables_in (m-trm args l) = rng l;
theorem :: ABCMIZ_A:59
for X being finite Subset of Vars st varcl X = X
for s being SortSymbol of MaxConstrSign
ex m being constructor OperSymbol of s st ::a_Type MaxConstrSign
ex p being FinSequence of QuasiTerms MaxConstrSign
st len p = len the_arity_of m & vars (m-trm p) = X;
definition
let d be PartFunc of Vars, QuasiTypes;
attr d is even means
:: ABCMIZ_A:def 29
for x,T st x in dom d & T = d.x holds vars T = vars x;
end;
definition
let l be quasi-loci;
mode type-distribution of l -> PartFunc of Vars, QuasiTypes means
:: ABCMIZ_A:def 30
dom it = rng l & it is even;
end;
theorem :: ABCMIZ_A:60
for l being empty quasi-loci holds {} is type-distribution of l;