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 β"
by (simp add: Pbij_inverse_def)
lemma Pbij_inverseD:"(l1,l2):Pbij_inverse β ⟹ (l2,l1):β"
by (simp add: Pbij_inverse_def) 
(*>*)

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) ∈ γ"
by (simp add: Pbij_compose_def)
(*>*)

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 (simp add: Pbij_def)
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)"
(*<*)
by (simp add: Pbij_def)
(*>*)

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"
(*<*)
by (simp add: Pbij_def Pbij_inverse_def)
(*>*)

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

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 β β"
(*<*)
by (simp add: Pbij_extends_def)
(*>*)

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

(*<*)
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 β)) β"
(*<*)
by (simp add: Pbij_extends_def Pbij_inverse_def)
(*>*)

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"
(*<*)
by (simp add: mkId_def Pbij_def)
(*>*)

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)"
(*<*)
by (simp add: mkId_def)
(*>*)

lemma mkId4b: "(l,ll):(mkId h) ⟹ l:Dom h ∧ l = ll"
(*<*)
by (simp add: mkId_def, clarsimp)
(*>*)

text‹End of theory PBIJ›
end