Skip to content
Permalink
Browse files

fixed wrong axiom in SMT backend and updated library proofs

  • Loading branch information
muenchnerkindl committed Jan 4, 2020
1 parent 199cb92 commit 0bd5cb3dcb9c31ad036c5e7e877779bf2465b4fd
@@ -45,21 +45,21 @@ SeqToBag(seq) == [ x \in Range(seq) |-> Cardinality({i \in DOMAIN seq: seq[i]=x}
THEOREM Bags_SqsubsetPO_Reflexivity ==
ASSUME NEW B, IsABag(B)
PROVE B \sqsubseteq B
BY DEF \sqsubseteq, IsABag
BY DEF \sqsubseteq, IsABag

(*Antisymmetry*)
THEOREM Bags_SqsubseteqPO_AntiSymmetry ==
ASSUME NEW A, NEW B, IsABag(A), IsABag(B),
A \sqsubseteq B, B \sqsubseteq A
PROVE A = B
BY Z3 DEF IsABag, \sqsubseteq
BY DEF IsABag, \sqsubseteq

(*Transitivity*)
THEOREM Bags_SqsubseteqPO_Transitivity ==
ASSUME NEW A, NEW B, NEW C, IsABag(A), IsABag(B), IsABag(C),
A \sqsubseteq B, B \sqsubseteq C
PROVE A \sqsubseteq C
BY Z3 DEF IsABag, \sqsubseteq
BY DEF IsABag, \sqsubseteq

(***************************************************************************)
(* Lemmas on EmptyBags *)
@@ -96,7 +96,7 @@ THEOREM Bags_Scaling ==
BY DEF Scaling, IsABag
<1>5. Scaling(n*m, B) = Scaling(n, Scaling(m, B))
<2>1. CASE m>0 /\ n>0
BY <2>1 DEF Scaling, IsABag
BY <2>1, n*m > 0 DEF Scaling, IsABag
<2>2. CASE m=0
BY <2>2, <1>2, <1>3 DEF Scaling
<2>3. CASE n=0
@@ -113,7 +113,7 @@ THEOREM Bags_Scaling ==
THEOREM Bags_Inverse ==
ASSUME NEW S
PROVE BagToSet(SetToBag(S))=S
BY DEF SetToBag, BagToSet
BY DEF SetToBag, BagToSet

THEOREM Bags_Inverse1 ==
ASSUME NEW B, IsABag(B)
@@ -188,7 +188,7 @@ BY DEF IsABag, (+), \sqsubseteq
THEOREM Bags_ScalingMonotonic ==
ASSUME NEW B, IsABag(B), NEW n \in Nat, NEW m \in Nat, m <= n
PROVE Scaling(m, B) \sqsubseteq Scaling(n, B)
BY DEF IsABag, Scaling, EmptyBag, SetToBag, \sqsubseteq
BY CVC4 DEF IsABag, Scaling, EmptyBag, SetToBag, \sqsubseteq

(***************************************************************************)
(* Given Bags A and B, A(-)B \sqsubseteq A *)
@@ -207,7 +207,7 @@ THEOREM Bags_EmptyBagOperations ==
ASSUME NEW B, IsABag(B)
PROVE /\ B (+) EmptyBag = B
/\ B (-) EmptyBag = B
BY Z3 DEF IsABag, (+), (-), EmptyBag, SetToBag
BY DEF IsABag, (+), (-), EmptyBag, SetToBag

(***************************************************************************)
(* SetToBag of a set is a bag. *)
@@ -340,7 +340,7 @@ THEOREM FS_AddElement ==
IF x \in S THEN Cardinality(S) ELSE Cardinality(S)+1
<1>1. CASE x \notin S
BY <1>1, FS_CardinalityType, Fun_NatBijAddElem, FS_NatBijection,
FS_CountingElements, Z3
FS_CountingElements
<1>. QED BY <1>1, Zenon \* the case "x \in S" is trivial


@@ -351,7 +351,7 @@ THEOREM FS_RemoveElement ==
IF x \in S THEN Cardinality(S)-1 ELSE Cardinality(S)
<1>1. CASE x \in S
BY <1>1, FS_CardinalityType, Fun_NatBijSubElem, FS_NatBijection,
FS_CountingElements, FS_EmptySet, Z3
FS_CountingElements, FS_EmptySet
<1>. QED BY <1>1, Zenon \* the case "x \notin S" is trivial


@@ -455,7 +455,12 @@ THEOREM FS_Injection ==
/\ Cardinality(S) <= Cardinality(T)
/\ Cardinality(S) = Cardinality(T) <=> f \in Surjection(S,T)
<1>1. CASE S = {}
BY <1>1, FS_CardinalityType, FS_EmptySet, Fun_IsSurj, Fun_SurjectionProperties, Z3
<2>1. IsFiniteSet(S) /\ Cardinality(S) <= Cardinality(T)
BY <1>1, FS_CardinalityType, FS_EmptySet
<2>2. Cardinality(S) = Cardinality(T) <=> f \in Surjection(S,T)
BY <1>1, FS_CardinalityType, FS_EmptySet, Fun_IsSurj, Fun_SurjectionProperties, Zenon
DEF Injection
<2>. QED BY <2>1, <2>2
<1>2. CASE S # {}
<2>1. Inverse(f,S,T) \in Surjection(T,S)
BY <1>2, Fun_InjInverse
@@ -807,7 +812,7 @@ THEOREM FS_Product ==
<2>. DEFINE SX == { <<s,x>> : s \in S }
<2>1. /\ IsFiniteSet(A \cup {x})
/\ Cardinality(A \cup {x}) = Cardinality(A) + 1
BY <1>2, FS_AddElement
BY <1>2, FS_AddElement, Zenon
<2>2. S \X (A \cup {x}) = (S \X A) \cup SX
BY <1>2, Isa
<2>3. ExistsBijection(S, SX)
@@ -854,7 +859,7 @@ THEOREM FS_SUBSET ==
<1>2. ASSUME NEW A, NEW x, IsFiniteSet(A), x \notin A, P(A)
PROVE P(A \cup {x})
<2>. DEFINE Ax == {B \cup {x} : B \in SUBSET A}
<2>1. Cardinality(A \cup {x}) = Cardinality(A) + 1 BY <1>2, FS_AddElement
<2>1. Cardinality(A \cup {x}) = Cardinality(A) + 1 BY <1>2, FS_AddElement, Zenon
<2>2. 2^Cardinality(A \cup {x}) = 2^Cardinality(A) + 2^Cardinality(A)
BY <2>1, <1>2, FS_CardinalityType, TwoExpLemma, Zenon
<2>3. SUBSET (A \cup {x}) = (SUBSET A) \cup Ax BY <1>2, Isa
@@ -888,7 +893,7 @@ THEOREM FS_SUBSET ==

=============================================================================
\* Modification History
\* Last modified Fri Oct 18 14:20:59 CEST 2019 by merz
\* Last modified Fri Dec 20 15:02:18 CET 2019 by merz
\* Last modified Thu Jul 04 15:15:07 CEST 2013 by bhargav
\* Last modified Tue Jun 04 11:44:51 CEST 2013 by bhargav
\* Last modified Fri May 03 12:02:51 PDT 2013 by tomr

0 comments on commit 0bd5cb3

Please sign in to comment.
You can’t perform that action at this time.