# Theory PBIJ

```(*File: PBIJ.thy*)
(*Authors: Lennart Beringer and Martin Hofmann, LMU Munich 2008*)
theory PBIJ imports OBJ begin

subsection‹Partial bijections›

text‹Partial bijections between locations will be used in the next
section to define indistinguishability of objects and heaps. We define
such bijections as sets of pairs which satisfy the obvious
condition.›

type_synonym PBij = "(Location × Location) set"
definition Pbij :: "PBij set"
where "Pbij = { β . ∀ l1 l2 l3 l4. (l1,l2):β ⟶ (l3,l4):β ⟶
((l1 = l3) = (l2 = l4))}"

text‹Domain and codomain are defined as expected.›

definition Pbij_Dom::"PBij ⇒ (Location set)"
where "Pbij_Dom β = {l . ∃ ll .(l,ll):β}"

definition Pbij_Rng::"PBij ⇒ (Location set)"
where "Pbij_Rng β = {ll . ∃ l .(l,ll):β}"

text‹We also define the inverse operation, the composition, and a
test deciding when one bijection extends another.›

definition Pbij_inverse::"PBij ⇒ PBij"
where "Pbij_inverse β = {(l,ll) . (ll,l):β}"
(*<*)
lemma Pbij_inverseI:"(l1,l2):β ⟹ (l2,l1):Pbij_inverse β"
lemma Pbij_inverseD:"(l1,l2):Pbij_inverse β ⟹ (l2,l1):β"
(*>*)

definition Pbij_compose::"PBij ⇒ PBij ⇒ PBij"
where "Pbij_compose β γ = {(l,ll) . ∃ l1 . (l,l1):β ∧ (l1,ll):γ}"
(*<*)
lemma Pbij_composeI: "⟦(l1, l2) ∈ β; (l2, l3) ∈ γ⟧ ⟹ (l1, l3) ∈ Pbij_compose β γ"
by (simp add: Pbij_compose_def, rule_tac x=l2 in exI, simp)
lemma Pbij_composeD: "(l1, l3) ∈ Pbij_compose β γ ⟹ ∃ l2 . (l1, l2) ∈ β ∧ (l2, l3) ∈ γ"
(*>*)

definition Pbij_extends ::"PBij ⇒ PBij ⇒ bool"
where "Pbij_extends γ β = (β ⊆ γ)"

text‹These definitions satisfy the following properties.›

lemma Pbij_insert:
"⟦β ∈ Pbij;l ∉ Pbij_Rng β; ll ∉ Pbij_Dom β⟧
⟹ insert (ll, l) β ∈ Pbij"
(*<*)
apply clarsimp
apply rule
apply clarsimp apply (simp add: Pbij_Dom_def Pbij_Rng_def) apply fast
apply clarsimp apply (simp add: Pbij_Dom_def Pbij_Rng_def) apply fast
done
(*>*)

lemma Pbij_injective:
"β:Pbij ⟹ (∀ l l1 l2 . (l1,l):β ⟶ (l2,l):β ⟶ l1=l2)"
(*<*)
(*>*)

lemma Pbij_inverse_DomRng[rule_format]:
"γ = Pbij_inverse β ⟹
(Pbij_Dom β = Pbij_Rng γ ∧ Pbij_Dom γ = Pbij_Rng β)"
(*<*)
by (simp add: Pbij_inverse_def Pbij_Dom_def Pbij_Rng_def)
(*>*)

lemma Pbij_inverse_Dom: "Pbij_Dom β = Pbij_Rng (Pbij_inverse β)"
(*<*)
by (simp add: Pbij_inverse_def Pbij_Dom_def Pbij_Rng_def)
(*>*)

lemma Pbij_inverse_Rng: "Pbij_Dom (Pbij_inverse β) = Pbij_Rng β"
(*<*)
by (simp add: Pbij_inverse_def Pbij_Dom_def Pbij_Rng_def)
(*>*)

lemma Pbij_inverse_Pbij: "β:Pbij ⟹ (Pbij_inverse β) : Pbij"
(*<*)
(*>*)

lemma Pbij_inverse_Inverse[rule_format]:
"γ = Pbij_inverse β ⟹ (∀ l ll . ((l,ll):β) = ((ll,l):γ))"
(*<*)
(*>*)

lemma Pbij_compose_Dom:
"Pbij_Dom (Pbij_compose β γ) ⊆ Pbij_Dom β"
(*<*)
by (simp add: Pbij_compose_def Pbij_Dom_def, fast)
(*>*)

lemma Pbij_compose_Rng:
"Pbij_Rng (Pbij_compose β γ) ⊆ Pbij_Rng γ"
(*<*)
by (simp add: Pbij_compose_def Pbij_Rng_def, fast)
(*>*)

lemma Pbij_compose_Pbij:
"⟦β : Pbij; γ : Pbij⟧ ⟹ Pbij_compose β γ : Pbij"
(*<*)
by (simp add: Pbij_compose_def Pbij_def, clarsimp)
(*>*)

lemma Pbij_extends_inverse:
"Pbij_extends γ (Pbij_inverse β) = Pbij_extends (Pbij_inverse γ) β"
(*<*)
by (simp add: Pbij_extends_def Pbij_inverse_def, fast)
(*>*)

lemma Pbij_extends_reflexive:"Pbij_extends β β"
(*<*)
(*>*)

lemma Pbij_extends_transitive:
"⟦Pbij_extends β γ; Pbij_extends γ δ⟧ ⟹ Pbij_extends β δ"
(*<*)
(*>*)

(*<*)
lemma Pbij_inverse_extends_twice_Aux:
"⟦ δ = Pbij_inverse ε; Pbij_extends ε γ; γ = Pbij_inverse  β⟧
⟹ Pbij_extends δ β"
by (simp add: Pbij_extends_def Pbij_inverse_def, fastforce)
(*>*)

lemma Pbij_inverse_extends_twice:
" Pbij_extends (Pbij_inverse (Pbij_inverse β)) β"
(*<*)
(*>*)

text‹The identity bijection on a heap associates each element of the
heap's domain with itself.›

definition mkId::"Heap ⇒ (Location × Location) set"
where "mkId h = {(l1,l2) . l1 = l2 ∧ l1 : Dom h}"

lemma mkId1: "(mkId h):Pbij"
(*<*)
(*>*)

lemma mkId2: "Pbij_Dom (mkId h) = Dom h"
(*<*)
by (simp add: Dom_def Pbij_Dom_def mkId_def)
(*>*)

lemma mkId2b: "Pbij_Rng (mkId h) = Dom h"
(*<*)
by (simp add: Dom_def Pbij_Rng_def mkId_def)
(*>*)

lemma mkId4: "l:Dom h ⟹ (l,l):(mkId h)"
(*<*)