[Imprint][Data Privacy Statement][E-Mail]
Back to main index.
View the specification.
View theorem base summary,
View theorem base listing,
the used properties by spec,
the dependency list,
the symbol table,
enrich
heap-fun
with
functions
mk : Set[Ref[(A, B)]] × (Ref[(A, B)] → A) × (Ref[(A, B)] → B) → Heap[(A, B)];
comment: construct a heap with pairs from domain + two functions giving the components;
. [ . ] : Heap[(A, B)] × Ref[(A, B)] × A × B → Heap[(A, B)];
. [ . ]o : Heap[(A, B)] × Ref[(A, B)] → A;
. [ . ]a : Heap[(A, B)] × Ref[(A, B)] → B;
. ==> ( . ) : Ref[(A, B)] × A × B → Heap[(A, B)] → Bool;
predicates
. [ . ] : (Heap[(A, B)] → Bool) × Set[Ref[(A, B)]] × (Ref[(A, B)] → A) × (Ref[(A, B)] → B);
variables
f : Ref[(A, B)] → A;
g : Ref[(A, B)] → B;
rR : Ref[(A, B)] → Heap[(A, B)] → Bool;
oaR : A × B → Heap[(A, B)] → Bool;
rrR : (Ref[(A, B)], Ref[(A, B)]) → Heap[(A, B)] → Bool;
hR : Heap[(A, B)] → Bool;
hP : Heap[(A, B)] → Bool;
h : Heap[(A, B)];
ha : Heap[(A, B)];
oa : (A, B);
r : Ref[(A, B)];
o : A;
a : B;
rs : Set[Ref[(A, B)]];
bv : Bool;
axioms
selo-def: h[r]o = (h(r))._1;
used for: ls;
sela-def: h[r]a = (h(r))._2;
used for: ls;
mod-def: h[r, o, a] = h(r := (o, a));
used for: ls;
modifysep-def: hP[rs, f, g] ↔ hP[rs, λ r. (f(r), g(r))];
used for: ls;
maplet-def: r.==>(o, a) = r => (o, a);
used for: ls;
mk-def: mk(rs, f, g) = mk(rs, λ r. (f(r), g(r)));
used for: ls;
theorems
at-mk-M01: r ∈ rs → mk(rs, f, g)[r]o = f(r);
used for: s;
at-mk-M02: r ∈ rs → mk(rs, f, g)[r]a = g(r);
used for: s;
in-mk: r ∈ mk(rs, f, g) ↔ r ∈ rs;
used for: s;
apply: hR[rs, f, g] ↔ hR(mk(rs, f, g));
at-rw: (r.==>(o, a) * hR)[rs, f, g] → (f(r) = o ∧ g(r) = a ↔ true);
at-rw0: r.==>(o, a)[rs, f, g] → (f(r) = o ∧ g(r) = a ↔ true);
at-unil-M01: disjoint(rs0, rs1) ∧ r ∈ rs0 → (mk(rs0, f, g) ∪ mk(rs1, f0, g0))[r]o = f(r);
used for: s;
at-unil-M02: disjoint(rs0, rs1) ∧ r ∈ rs0 → (mk(rs0, f, g) ∪ mk(rs1, f0, g0))[r]a = g(r);
used for: s;
at-unir-M01: disjoint(rs0, rs1) ∧ r ∈ rs1 → (mk(rs0, f, g) ∪ mk(rs1, f0, g0))[r]o = f0(r);
used for: s;
at-unir-M02: disjoint(rs0, rs1) ∧ r ∈ rs1 → (mk(rs0, f, g) ∪ mk(rs1, f0, g0))[r]a = g0(r);
used for: s;
del: mk(rs -- r, f, g) = mk(rs, f, g) -- r;
disj: mk(rs0, f, g) ⊥ mk(rs1, f0, g0) ↔ rs0 ∩ rs1 = ∅;
used for: s;
emp: mk(∅, f, g) = ∅;
used for: s;
ex1-shift: (_∃ rR * hR)[rs, f, g] ↔ (∃ r. (rR(r) * hR)[rs, f, g]);
ex2-shift: (_∃ rrR * hR)[rs, f, g] ↔ (∃ r0, r1. (rrR((r0, r1)) * hR)[rs, f, g]);
ex3-shift-01: (_∃ oaR * hR)[rs, f, g] ↔ (∃ o, a. (oaR(o, a) * hR)[rs, f, g]);
in-uni: disjoint(rs0, rs1) → (r ∈ mk(rs0, f, g) ∪ mk(rs1, f0, g0) ↔ r ∈ rs0 ∨ r ∈ rs1);
map-del: (r.==>(o, a) * hR)[rs, f, g] ↔ hR[rs -- r, f, g] ∧ r ∈ rs ∧ f(r) = o ∧ g(r) = a;
map-in: (r.==>(o, a) * hR)[rs, f, g] → r ∈ rs;
map-in0: r.==>(o, a)[rs, f, g] → r ∈ rs;
map-put: (r.=>_ * hR)[rs, f, g] ↔ (r.==>(o1, a1) * hR)[rs, f(r := o1), g(r := a1)] ∧ r ∈ rs;
map-putrev: r ∈ rs ⊦ (r.==>(o0, a0) * hR)[rs, f(r := o1), g(r := a1)] ↔ (o0 = o1 ∧ a0 = a1) ∧ (r.=>_ * hR)[rs, f, g];
mapex-del: (r.=>_ * hR)[rs, f, g] → hR[rs -- r, f, g];
mapex-elim: (r.==>(o, a) * hR)[rs, f, g] → (r.=>_ * hR)[rs, f, g];
mapex-in: (r.=>_ * hR)[rs, f, g] → r ∈ rs;
mapex-in0: r.=>_[rs, f, g] → r ∈ rs;
mapex-new: ¬ r ∈ rs, r ≠ null ⊦ hR[rs, f, g] ↔ (r.=>_ * hR)[rs ++ r, f, g];
mapex-put: r ∈ rs ⊦ (r.=>_ * hR)[rs, f(r := o), g(r := a)] ↔ (r.==>(o, a) * hR)[rs, f(r := o), g(r := a)];
mk-exists: ∃ rs, f, g. ha = mk(rs, f, g);
mk-ext: hR0 = hR1 ↔ (∀ rs, f, g. hR0[rs, f, g] ↔ hR1[rs, f, g]);
prop: ⌜bv⌝ [rs, f, g] ↔ bv;
prop-emp: ((⌜bv⌝ ∧ emp) * hR)[rs, f, g] ↔ bv ∧ hR[rs, f, g];
prop-false: ¬ false[rs, f, g];
prop-sep: ((⌜bv⌝ ∧ hR0) * hR1)[rs, f, g] ↔ bv ∧ (hR0 * hR1)[rs, f, g];
prop-true: true[rs, f, g];
sep: (hR0 * hR1)[rs, f, g] ↔ (∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ disjoint(rs0, rs1) ∧ hR0[rs0, f, g] ∧ hR1[rs1, f, g]);
split-uni: hR0[rs0, f, g] ∧ hR1[rs1, f, g] ∧ disjoint(rs0, rs1) → (hR0 * hR1)[rs0 ∪ rs1, f, g];
true-elim: (hR0 * hR)[rs, f, g] → (true * hR)[rs, f, g];
true-emp: hR[rs, f, g] → (true * hR)[rs, f, g];
uni: disjoint(rs0, rs1) → mk(rs0 ∪ rs1, f, g) = mk(rs0, f, g) ∪ mk(rs1, f, g);
write: r ∈ rs → mk(rs, f(r := o), g(r := a)) = mk(rs, f, g)[r, o, a];
maplet: r.==>(o, a)(ha) ↔ ha = (∅ ++ r)[r, o, a] ∧ r ≠ null;
mapex: r.=>_ = _∃(λ o, a. r.==>(o, a));
ex3-03: (_∃ oaR)(ha) ↔ (∃ o, a. oaR(o, a)(ha));
at-eq: (r.==>(o0, a0) * hR)(ha) → (ha[r]o = o1 ∧ ha[r]a = a1 ↔ o0 = o1 ∧ a0 = a1);
at-rw-M01: (r.==>(o0, a0) * hR)(ha) → ha[r]o = o0;
used for: s;
at-rw-M02: (r.==>(o0, a0) * hR)(ha) → ha[r]a = a0;
used for: s;
eq-objs-M01: (r.==>(o0, a0) * hR0)(ha) ∧ (r.==>(o1, a1) * hR1)(ha) → o0 = o1;
eq-objs-M02: (r.==>(o0, a0) * hR0)(ha) ∧ (r.==>(o1, a1) * hR1)(ha) → a0 = a1;
ex3-shift: (_∃ oaR * hR)(ha) ↔ (∃ o, a. (oaR(o, a) * hR)(ha));
used for: s;
ex3-shiftw: (_∃ oaR -* hR)(ha) ↔ (∀ o, a. (oaR(o, a) -* hR)(ha));
ex3-shiftw-inst: ((_∃ oaR -* hR) * hR0)(ha) ↔ ((_∃ oaR -* hR) * hR0)(ha) ∧ ((oaR(o, a) -* hR) * hR0)(ha);
map-del-01: (r.==>(o, a) * hR)(ha) ↔ hR(ha -- r) ∧ r ∈ ha ∧ ha[r]o = o ∧ ha[r]a = a;
map-in-01: (r.==>(o, a) * hR)(ha) → r ∈ ha;
map-in0-02: r.==>(o, a)(ha) → r ∈ ha;
map-null: null.==>(o, a) = ⌜false⌝ ;
map-put-01: (r.=>_ * hR)(ha) ↔ (r.==>(o1, a1) * hR)(ha[r, o1, a1]) ∧ r ∈ ha;
map-put-rw: r ∈ ha ⊦ (r.==>(o, a) * hR)(ha) → ((r.==>(o0, a0) * hR)(ha[r, o1, a1]) ↔ o0 = o1 ∧ a0 = a1);
map-putex: r ∈ ha ⊦ (r.==>(o0, a0) * hR)(ha[r, o1, a1]) ↔ (o0 = o1 ∧ a0 = a1) ∧ (r.=>_ * hR)(ha);
map-same: r.==>(o0, a0) * r.==>(o1, a1) = false;
map-write-M01: r ∈ ha ⊦ (r.==>(o0, a0) * hR)(ha[r, o1, a1]) → o0 = o1;
map-write-M02: r ∈ ha ⊦ (r.==>(o0, a0) * hR)(ha[r, o1, a1]) → a0 = a1;
mapex-and: (r.=>_ ∧ r.==>(o, a)) = r.==>(o, a);
mapex-elim-01: (r.==>(o, a) * hR)(ha) → (r.=>_ * hR)(ha);
mapex-put-01: r ∈ ha ⊦ (r.=>_ * hR)(ha[r, o, a]) ↔ (r.==>(o, a) * hR)(ha[r, o, a]);
mapex-put-rw: r ∈ ha ⊦ (r.=>_ * hR)(ha) → ((r.==>(o0, a0) * hR)(ha[r, o1, a1]) ↔ o0 = o1 ∧ a0 = a1);
maplet-singleton-heap: r.==>(o, a)(ha) ↔ r ≠ null ∧ ha = (∅ ++ r)[r, o, a];
precise-map: precise(r.==>(o, a));
end enrich