Theory Design_generated_generated

theory Design_generated_generated imports "../Toy_Library"   "../Toy_Library_Static" begin

(* 1 ************************************ 0 + 1 *)
text ‹
  For certain concepts like classes and class-types, only a generic
  definition for its resulting semantics can be given. Generic means,
  there is a function outside HOL that ``compiles'' a concrete,
  closed-world class diagram into a ``theory'' of this data model,
  consisting of a bunch of definitions for classes, accessors, method,
  casts, and tests for actual types, as well as proofs for the
  fundamental properties of these operations in this concrete data
  model. ›

(* 2 ************************************ 1 + 1 *)
text ‹
   Our data universe  consists in the concrete class diagram just of node's,
and implicitly of the class object. Each class implies the existence of a class
type defined for the corresponding object representations as follows: ›

(* 3 ************************************ 2 + 10 *)
datatype tyℰ𝒳𝒯⇩A⇩t⇩o⇩m = mkℰ𝒳𝒯⇩A⇩t⇩o⇩m "oid" "oid list option" "int option" "bool option" "nat option" "unit option"
datatype ty⇩A⇩t⇩o⇩m = mk⇩A⇩t⇩o⇩m "tyℰ𝒳𝒯⇩A⇩t⇩o⇩m" "int option"
datatype tyℰ𝒳𝒯⇩M⇩o⇩l⇩e⇩c⇩u⇩l⇩e = mkℰ𝒳𝒯⇩M⇩o⇩l⇩e⇩c⇩u⇩l⇩e_⇩A⇩t⇩o⇩m "ty⇩A⇩t⇩o⇩m"
                        | mkℰ𝒳𝒯⇩M⇩o⇩l⇩e⇩c⇩u⇩l⇩e "oid" "oid list option" "int option" "bool option" "nat option" "unit option"
datatype ty⇩M⇩o⇩l⇩e⇩c⇩u⇩l⇩e = mk⇩M⇩o⇩l⇩e⇩c⇩u⇩l⇩e "tyℰ𝒳𝒯⇩M⇩o⇩l⇩e⇩c⇩u⇩l⇩e"
datatype tyℰ𝒳𝒯⇩P⇩e⇩r⇩s⇩o⇩n = mkℰ𝒳𝒯⇩P⇩e⇩r⇩s⇩o⇩n_⇩M⇩o⇩l⇩e⇩c⇩u⇩l⇩e "ty⇩M⇩o⇩l⇩e⇩c⇩u⇩l⇩e"
                        | mkℰ𝒳𝒯⇩P⇩e⇩r⇩s⇩o⇩n_⇩A⇩t⇩o⇩m "ty⇩A⇩t⇩o⇩m"
                        | mkℰ𝒳𝒯⇩P⇩e⇩r⇩s⇩o⇩n "oid" "nat option" "unit option"
datatype ty⇩P⇩e⇩r⇩s⇩o⇩n = mk⇩P⇩e⇩r⇩s⇩o⇩n "tyℰ𝒳𝒯⇩P⇩e⇩r⇩s⇩o⇩n" "oid list option" "int option" "bool option"
datatype tyℰ𝒳𝒯⇩G⇩a⇩l⇩a⇩x⇩y = mkℰ𝒳𝒯⇩G⇩a⇩l⇩a⇩x⇩y_⇩P⇩e⇩r⇩s⇩o⇩n "ty⇩P⇩e⇩r⇩s⇩o⇩n"
                        | mkℰ𝒳𝒯⇩G⇩a⇩l⇩a⇩x⇩y_⇩M⇩o⇩l⇩e⇩c⇩u⇩l⇩e "ty⇩M⇩o⇩l⇩e⇩c⇩u⇩l⇩e"
                        | mkℰ𝒳𝒯⇩G⇩a⇩l⇩a⇩x⇩y_⇩A⇩t⇩o⇩m "ty⇩A⇩t⇩o⇩m"
                        | mkℰ𝒳𝒯⇩G⇩a⇩l⇩a⇩x⇩y "oid"
datatype ty⇩G⇩a⇩l⇩a⇩x⇩y = mk⇩G⇩a⇩l⇩a⇩x⇩y "tyℰ𝒳𝒯⇩G⇩a⇩l⇩a⇩x⇩y" "nat option" "unit option"
datatype tyℰ𝒳𝒯⇩T⇩o⇩y⇩A⇩n⇩y = mkℰ𝒳𝒯⇩T⇩o⇩y⇩A⇩n⇩y_⇩G⇩a⇩l⇩a⇩x⇩y "ty⇩G⇩a⇩l⇩a⇩x⇩y"
                        | mkℰ𝒳𝒯⇩T⇩o⇩y⇩A⇩n⇩y_⇩P⇩e⇩r⇩s⇩o⇩n "ty⇩P⇩e⇩r⇩s⇩o⇩n"
                        | mkℰ𝒳𝒯⇩T⇩o⇩y⇩A⇩n⇩y_⇩M⇩o⇩l⇩e⇩c⇩u⇩l⇩e "ty⇩M⇩o⇩l⇩e⇩c⇩u⇩l⇩e"
                        | mkℰ𝒳𝒯⇩T⇩o⇩y⇩A⇩n⇩y_⇩A⇩t⇩o⇩m "ty⇩A⇩t⇩o⇩m"
                        | mkℰ𝒳𝒯⇩T⇩o⇩y⇩A⇩n⇩y "oid"
datatype ty⇩T⇩o⇩y⇩A⇩n⇩y = mk⇩T⇩o⇩y⇩A⇩n⇩y "tyℰ𝒳𝒯⇩T⇩o⇩y⇩A⇩n⇩y"

(* 4 ************************************ 12 + 1 *)
text ‹
   Now, we construct a concrete ``universe of ToyAny types'' by injection into a
sum type containing the class types. This type of ToyAny will be used as instance
for all respective type-variables. ›

(* 5 ************************************ 13 + 1 *)
datatype 𝔄 = in⇩A⇩t⇩o⇩m "ty⇩A⇩t⇩o⇩m"
                        | in⇩M⇩o⇩l⇩e⇩c⇩u⇩l⇩e "ty⇩M⇩o⇩l⇩e⇩c⇩u⇩l⇩e"
                        | in⇩P⇩e⇩r⇩s⇩o⇩n "ty⇩P⇩e⇩r⇩s⇩o⇩n"
                        | in⇩G⇩a⇩l⇩a⇩x⇩y "ty⇩G⇩a⇩l⇩a⇩x⇩y"
                        | in⇩T⇩o⇩y⇩A⇩n⇩y "ty⇩T⇩o⇩y⇩A⇩n⇩y"

(* 6 ************************************ 14 + 1 *)
text ‹
   Having fixed the object universe, we can introduce type synonyms that exactly correspond
to Toy types. Again, we exploit that our representation of Toy is a ``shallow embedding'' with a
one-to-one correspondance of Toy-types to types of the meta-language HOL. ›

(* 7 ************************************ 15 + 5 *)
type_synonym Atom = "⟨⟨ty⇩A⇩t⇩o⇩m⟩⇩⊥⟩⇩⊥"
type_synonym Molecule = "⟨⟨ty⇩M⇩o⇩l⇩e⇩c⇩u⇩l⇩e⟩⇩⊥⟩⇩⊥"
type_synonym Person = "⟨⟨ty⇩P⇩e⇩r⇩s⇩o⇩n⟩⇩⊥⟩⇩⊥"
type_synonym Galaxy = "⟨⟨ty⇩G⇩a⇩l⇩a⇩x⇩y⟩⇩⊥⟩⇩⊥"
type_synonym ToyAny = "⟨⟨ty⇩T⇩o⇩y⇩A⇩n⇩y⟩⇩⊥⟩⇩⊥"

(* 8 ************************************ 20 + 3 *)
definition "oid⇩A⇩t⇩o⇩m_0___boss = 0"
definition "oid⇩M⇩o⇩l⇩e⇩c⇩u⇩l⇩e_0___boss = 0"
definition "oid⇩P⇩e⇩r⇩s⇩o⇩n_0___boss = 0"

(* 9 ************************************ 23 + 2 *)
definition "switch⇩2_01 = (λ [x0 , x1] ⇒ (x0 , x1))"
definition "switch⇩2_10 = (λ [x0 , x1] ⇒ (x1 , x0))"

(* 10 ************************************ 25 + 3 *)
definition "oid1 = 1"
definition "oid2 = 2"
definition "inst_assoc1 = (λoid_class to_from oid. ((case (deref_assocs_list ((to_from::oid list list ⇒ oid list × oid list)) ((oid::oid)) ((drop ((((map_of_list ([(oid⇩P⇩e⇩r⇩s⇩o⇩n_0___boss , (List.map ((λ(x , y). [x , y]) o switch⇩2_01) ([[[oid1] , [oid2]]])))]))) ((oid_class::oid))))))) of Nil ⇒ None
    | l ⇒ (Some (l)))::oid list option))"

(* 11 ************************************ 28 + 0 *)

(* 12 ************************************ 28 + 2 *)
definition "oid3 = 3"
definition "inst_assoc3 = (λoid_class to_from oid. ((case (deref_assocs_list ((to_from::oid list list ⇒ oid list × oid list)) ((oid::oid)) ((drop ((((map_of_list ([]))) ((oid_class::oid))))))) of Nil ⇒ None
    | l ⇒ (Some (l)))::oid list option))"

(* 13 ************************************ 30 + 0 *)

(* 14 ************************************ 30 + 5 *)
definition "oid4 = 4"
definition "oid5 = 5"
definition "oid6 = 6"
definition "oid7 = 7"
definition "inst_assoc4 = (λoid_class to_from oid. ((case (deref_assocs_list ((to_from::oid list list ⇒ oid list × oid list)) ((oid::oid)) ((drop ((((map_of_list ([(oid⇩P⇩e⇩r⇩s⇩o⇩n_0___boss , (List.map ((λ(x , y). [x , y]) o switch⇩2_01) ([[[oid7] , [oid6]] , [[oid6] , [oid1]] , [[oid4] , [oid5]]])))]))) ((oid_class::oid))))))) of Nil ⇒ None
    | l ⇒ (Some (l)))::oid list option))"

(* 15 ************************************ 35 + 0 *)

(* 16 ************************************ 35 + 1 *)
locale state_σ⇩1 =
fixes "oid4" :: "nat"
fixes "oid5" :: "nat"
fixes "oid6" :: "nat"
fixes "oid1" :: "nat"
fixes "oid7" :: "nat"
fixes "oid2" :: "nat"
assumes distinct_oid: "(distinct ([oid4 , oid5 , oid6 , oid1 , oid7 , oid2]))"
fixes "σ⇩1_object0⇩P⇩e⇩r⇩s⇩o⇩n" :: "ty⇩P⇩e⇩r⇩s⇩o⇩n"
fixes "σ⇩1_object0" :: "⋅Person"
assumes σ⇩1_object0_def: "σ⇩1_object0 = (λ_. ⌊⌊σ⇩1_object0⇩P⇩e⇩r⇩s⇩o⇩n⌋⌋)"
fixes "σ⇩1_object1⇩P⇩e⇩r⇩s⇩o⇩n" :: "ty⇩P⇩e⇩r⇩s⇩o⇩n"
fixes "σ⇩1_object1" :: "⋅Person"
assumes σ⇩1_object1_def: "σ⇩1_object1 = (λ_. ⌊⌊σ⇩1_object1⇩P⇩e⇩r⇩s⇩o⇩n⌋⌋)"
fixes "σ⇩1_object2⇩P⇩e⇩r⇩s⇩o⇩n" :: "ty⇩P⇩e⇩r⇩s⇩o⇩n"
fixes "σ⇩1_object2" :: "⋅Person"
assumes σ⇩1_object2_def: "σ⇩1_object2 = (λ_. ⌊⌊σ⇩1_object2⇩P⇩e⇩r⇩s⇩o⇩n⌋⌋)"
fixes "X⇩P⇩e⇩r⇩s⇩o⇩n1⇩P⇩e⇩r⇩s⇩o⇩n" :: "ty⇩P⇩e⇩r⇩s⇩o⇩n"
fixes "X⇩P⇩e⇩r⇩s⇩o⇩n1" :: "⋅Person"
assumes X⇩P⇩e⇩r⇩s⇩o⇩n1_def: "X⇩P⇩e⇩r⇩s⇩o⇩n1 = (λ_. ⌊⌊X⇩P⇩e⇩r⇩s⇩o⇩n1⇩P⇩e⇩r⇩s⇩o⇩n⌋⌋)"
fixes "σ⇩1_object4⇩P⇩e⇩r⇩s⇩o⇩n" :: "ty⇩P⇩e⇩r⇩s⇩o⇩n"
fixes "σ⇩1_object4" :: "⋅Person"
assumes σ⇩1_object4_def: "σ⇩1_object4 = (λ_. ⌊⌊σ⇩1_object4⇩P⇩e⇩r⇩s⇩o⇩n⌋⌋)"
fixes "X⇩P⇩e⇩r⇩s⇩o⇩n2⇩P⇩e⇩r⇩s⇩o⇩n" :: "ty⇩P⇩e⇩r⇩s⇩o⇩n"
fixes "X⇩P⇩e⇩r⇩s⇩o⇩n2" :: "⋅Person"
assumes X⇩P⇩e⇩r⇩s⇩o⇩n2_def: "X⇩P⇩e⇩r⇩s⇩o⇩n2 = (λ_. ⌊⌊X⇩P⇩e⇩r⇩s⇩o⇩n2⇩P⇩e⇩r⇩s⇩o⇩n⌋⌋)"
begin
definition "σ⇩1 = (state.make ((Map.empty (oid4 ↦ (in⇩P⇩e⇩r⇩s⇩o⇩n (σ⇩1_object0⇩P⇩e⇩r⇩s⇩o⇩n)), oid5 ↦ (in⇩P⇩e⇩r⇩s⇩o⇩n (σ⇩1_object1⇩P⇩e⇩r⇩s⇩o⇩n)), oid6 ↦ (in⇩P⇩e⇩r⇩s⇩o⇩n (σ⇩1_object2⇩P⇩e⇩r⇩s⇩o⇩n)), oid1 ↦ (in⇩P⇩e⇩r⇩s⇩o⇩n (X⇩P⇩e⇩r⇩s⇩o⇩n1⇩P⇩e⇩r⇩s⇩o⇩n)), oid7 ↦ (in⇩P⇩e⇩r⇩s⇩o⇩n (σ⇩1_object4⇩P⇩e⇩r⇩s⇩o⇩n)), oid2 ↦ (in⇩P⇩e⇩r⇩s⇩o⇩n (X⇩P⇩e⇩r⇩s⇩o⇩n2⇩P⇩e⇩r⇩s⇩o⇩n))))) ((map_of_list ([(oid⇩P⇩e⇩r⇩s⇩o⇩n_0___boss , (List.map ((λ(x , y). [x , y]) o switch⇩2_01) ([[[oid4] , [oid2]] , [[oid6] , [oid4]] , [[oid1] , [oid6]] , [[oid7] , [oid3]]])))]))))"

lemma perm_σ⇩1 : "σ⇩1 = (state.make ((Map.empty (oid2 ↦ (in⇩P⇩e⇩r⇩s⇩o⇩n (X⇩P⇩e⇩r⇩s⇩o⇩n2⇩P⇩e⇩r⇩s⇩o⇩n)), oid7 ↦ (in⇩P⇩e⇩r⇩s⇩o⇩n (σ⇩1_object4⇩P⇩e⇩r⇩s⇩o⇩n)), oid1 ↦ (in⇩P⇩e⇩r⇩s⇩o⇩n (X⇩P⇩e⇩r⇩s⇩o⇩n1⇩P⇩e⇩r⇩s⇩o⇩n)), oid6 ↦ (in⇩P⇩e⇩r⇩s⇩o⇩n (σ⇩1_object2⇩P⇩e⇩r⇩s⇩o⇩n)), oid5 ↦ (in⇩P⇩e⇩r⇩s⇩o⇩n (σ⇩1_object1⇩P⇩e⇩r⇩s⇩o⇩n)), oid4 ↦ (in⇩P⇩e⇩r⇩s⇩o⇩n (σ⇩1_object0⇩P⇩e⇩r⇩s⇩o⇩n))))) ((assocs (σ⇩1))))"
  apply(simp add: σ⇩1_def)
  apply(subst (1) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
  apply(subst (2) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
  apply(subst (1) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
  apply(subst (3) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
  apply(subst (2) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
  apply(subst (1) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
  apply(subst (4) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
  apply(subst (3) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
  apply(subst (2) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
  apply(subst (1) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
  apply(subst (5) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
  apply(subst (4) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
  apply(subst (3) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
  apply(subst (2) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
  apply(subst (1) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
by(simp)
end

(* 17 ************************************ 36 + 1 *)
locale state_σ⇩1' =
fixes "oid1" :: "nat"
fixes "oid2" :: "nat"
fixes "oid3" :: "nat"
assumes distinct_oid: "(distinct ([oid1 , oid2 , oid3]))"
fixes "X⇩P⇩e⇩r⇩s⇩o⇩n1⇩P⇩e⇩r⇩s⇩o⇩n" :: "ty⇩P⇩e⇩r⇩s⇩o⇩n"
fixes "X⇩P⇩e⇩r⇩s⇩o⇩n1" :: "⋅Person"
assumes X⇩P⇩e⇩r⇩s⇩o⇩n1_def: "X⇩P⇩e⇩r⇩s⇩o⇩n1 = (λ_. ⌊⌊X⇩P⇩e⇩r⇩s⇩o⇩n1⇩P⇩e⇩r⇩s⇩o⇩n⌋⌋)"
fixes "X⇩P⇩e⇩r⇩s⇩o⇩n2⇩P⇩e⇩r⇩s⇩o⇩n" :: "ty⇩P⇩e⇩r⇩s⇩o⇩n"
fixes "X⇩P⇩e⇩r⇩s⇩o⇩n2" :: "⋅Person"
assumes X⇩P⇩e⇩r⇩s⇩o⇩n2_def: "X⇩P⇩e⇩r⇩s⇩o⇩n2 = (λ_. ⌊⌊X⇩P⇩e⇩r⇩s⇩o⇩n2⇩P⇩e⇩r⇩s⇩o⇩n⌋⌋)"
fixes "X⇩P⇩e⇩r⇩s⇩o⇩n3⇩P⇩e⇩r⇩s⇩o⇩n" :: "ty⇩P⇩e⇩r⇩s⇩o⇩n"
fixes "X⇩P⇩e⇩r⇩s⇩o⇩n3" :: "⋅Person"
assumes X⇩P⇩e⇩r⇩s⇩o⇩n3_def: "X⇩P⇩e⇩r⇩s⇩o⇩n3 = (λ_. ⌊⌊X⇩P⇩e⇩r⇩s⇩o⇩n3⇩P⇩e⇩r⇩s⇩o⇩n⌋⌋)"
begin
definition "σ⇩1' = (state.make ((Map.empty (oid1 ↦ (in⇩P⇩e⇩r⇩s⇩o⇩n (X⇩P⇩e⇩r⇩s⇩o⇩n1⇩P⇩e⇩r⇩s⇩o⇩n)), oid2 ↦ (in⇩P⇩e⇩r⇩s⇩o⇩n (X⇩P⇩e⇩r⇩s⇩o⇩n2⇩P⇩e⇩r⇩s⇩o⇩n)), oid3 ↦ (in⇩P⇩e⇩r⇩s⇩o⇩n (X⇩P⇩e⇩r⇩s⇩o⇩n3⇩P⇩e⇩r⇩s⇩o⇩n))))) ((map_of_list ([(oid⇩P⇩e⇩r⇩s⇩o⇩n_0___boss , (List.map ((λ(x , y). [x , y]) o switch⇩2_01) ([[[oid1] , [oid2]]])))]))))"

lemma perm_σ⇩1' : "σ⇩1' = (state.make ((Map.empty (oid3 ↦ (in⇩P⇩e⇩r⇩s⇩o⇩n (X⇩P⇩e⇩r⇩s⇩o⇩n3⇩P⇩e⇩r⇩s⇩o⇩n)), oid2 ↦ (in⇩P⇩e⇩r⇩s⇩o⇩n (X⇩P⇩e⇩r⇩s⇩o⇩n2⇩P⇩e⇩r⇩s⇩o⇩n)), oid1 ↦ (in⇩P⇩e⇩r⇩s⇩o⇩n (X⇩P⇩e⇩r⇩s⇩o⇩n1⇩P⇩e⇩r⇩s⇩o⇩n))))) ((assocs (σ⇩1'))))"
  apply(simp add: σ⇩1'_def)
  apply(subst (1) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
  apply(subst (2) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
  apply(subst (1) fun_upd_twist, metis distinct_oid distinct_length_2_or_more)
by(simp)
end

(* 18 ************************************ 37 + 1 *)
locale pre_post_σ⇩1_σ⇩1' =
fixes "oid1" :: "nat"
fixes "oid2" :: "nat"
fixes "oid3" :: "nat"
fixes "oid4" :: "nat"
fixes "oid5" :: "nat"
fixes "oid6" :: "nat"
fixes "oid7" :: "nat"
assumes distinct_oid: "(distinct ([oid1 , oid2 , oid3 , oid4 , oid5 , oid6 , oid7]))"
fixes "X⇩P⇩e⇩r⇩s⇩o⇩n1⇩P⇩e⇩r⇩s⇩o⇩n" :: "ty⇩P⇩e⇩r⇩s⇩o⇩n"
fixes "X⇩P⇩e⇩r⇩s⇩o⇩n1" :: "⋅Person"
assumes X⇩P⇩e⇩r⇩s⇩o⇩n1_def: "X⇩P⇩e⇩r⇩s⇩o⇩n1 = (λ_. ⌊⌊X⇩P⇩e⇩r⇩s⇩o⇩n1⇩P⇩e⇩r⇩s⇩o⇩n⌋⌋)"
fixes "X⇩P⇩e⇩r⇩s⇩o⇩n2⇩P⇩e⇩r⇩s⇩o⇩n" :: "ty⇩P⇩e⇩r⇩s⇩o⇩n"
fixes "X⇩P⇩e⇩r⇩s⇩o⇩n2" :: "⋅Person"
assumes X⇩P⇩e⇩r⇩s⇩o⇩n2_def: "X⇩P⇩e⇩r⇩s⇩o⇩n2 = (λ_. ⌊⌊X⇩P⇩e⇩r⇩s⇩o⇩n2⇩P⇩e⇩r⇩s⇩o⇩n⌋⌋)"
fixes "X⇩P⇩e⇩r⇩s⇩o⇩n3⇩P⇩e⇩r⇩s⇩o⇩n" :: "ty⇩P⇩e⇩r⇩s⇩o⇩n"
fixes "X⇩P⇩e⇩r⇩s⇩o⇩n3" :: "⋅Person"
assumes X⇩P⇩e⇩r⇩s⇩o⇩n3_def: "X⇩P⇩e⇩r⇩s⇩o⇩n3 = (λ_. ⌊⌊X⇩P⇩e⇩r⇩s⇩o⇩n3⇩P⇩e⇩r⇩s⇩o⇩n⌋⌋)"
fixes "σ⇩1_object0⇩P⇩e⇩r⇩s⇩o⇩n" :: "ty⇩P⇩e⇩r⇩s⇩o⇩n"
fixes "σ⇩1_object0" :: "⋅Person"
assumes σ⇩1_object0_def: "σ⇩1_object0 = (λ_. ⌊⌊σ⇩1_object0⇩P⇩e⇩r⇩s⇩o⇩n⌋⌋)"
fixes "σ⇩1_object1⇩P⇩e⇩r⇩s⇩o⇩n" :: "ty⇩P⇩e⇩r⇩s⇩o⇩n"
fixes "σ⇩1_object1" :: "⋅Person"
assumes σ⇩1_object1_def: "σ⇩1_object1 = (λ_. ⌊⌊σ⇩1_object1⇩P⇩e⇩r⇩s⇩o⇩n⌋⌋)"
fixes "σ⇩1_object2⇩P⇩e⇩r⇩s⇩o⇩n" :: "ty⇩P⇩e⇩r⇩s⇩o⇩n"
fixes "σ⇩1_object2" :: "⋅Person"
assumes σ⇩1_object2_def: "σ⇩1_object2 = (λ_. ⌊⌊σ⇩1_object2⇩P⇩e⇩r⇩s⇩o⇩n⌋⌋)"
fixes "σ⇩1_object4⇩P⇩e⇩r⇩s⇩o⇩n" :: "ty⇩P⇩e⇩r⇩s⇩o⇩n"
fixes "σ⇩1_object4" :: "⋅Person"
assumes σ⇩1_object4_def: "σ⇩1_object4 = (λ_. ⌊⌊σ⇩1_object4⇩P⇩e⇩r⇩s⇩o⇩n⌋⌋)"

assumes σ⇩1: "(state_σ⇩1 (oid4) (oid5) (oid6) (oid1) (oid7) (oid2) (σ⇩1_object0⇩P⇩e⇩r⇩s⇩o⇩n) (σ⇩1_object0) (σ⇩1_object1⇩P⇩e⇩r⇩s⇩o⇩n) (σ⇩1_object1) (σ⇩1_object2⇩P⇩e⇩r⇩s⇩o⇩n) (σ⇩1_object2) (X⇩P⇩e⇩r⇩s⇩o⇩n1⇩P⇩e⇩r⇩s⇩o⇩n) (X⇩P⇩e⇩r⇩s⇩o⇩n1) (σ⇩1_object4⇩P⇩e⇩r⇩s⇩o⇩n) (σ⇩1_object4) (X⇩P⇩e⇩r⇩s⇩o⇩n2⇩P⇩e⇩r⇩s⇩o⇩n) (X⇩P⇩e⇩r⇩s⇩o⇩n2))"

assumes σ⇩1': "(state_σ⇩1' (oid1) (oid2) (oid3) (X⇩P⇩e⇩r⇩s⇩o⇩n1⇩P⇩e⇩r⇩s⇩o⇩n) (X⇩P⇩e⇩r⇩s⇩o⇩n1) (X⇩P⇩e⇩r⇩s⇩o⇩n2⇩P⇩e⇩r⇩s⇩o⇩n) (X⇩P⇩e⇩r⇩s⇩o⇩n2) (X⇩P⇩e⇩r⇩s⇩o⇩n3⇩P⇩e⇩r⇩s⇩o⇩n) (X⇩P⇩e⇩r⇩s⇩o⇩n3))"
begin
interpretation state_σ⇩1: state_σ⇩1 "oid4" "oid5" "oid6" "oid1" "oid7" "oid2" "σ⇩1_object0⇩P⇩e⇩r⇩s⇩o⇩n" "σ⇩1_object0" "σ⇩1_object1⇩P⇩e⇩r⇩s⇩o⇩n" "σ⇩1_object1" "σ⇩1_object2⇩P⇩e⇩r⇩s⇩o⇩n" "σ⇩1_object2" "X⇩P⇩e⇩r⇩s⇩o⇩n1⇩P⇩e⇩r⇩s⇩o⇩n" "X⇩P⇩e⇩r⇩s⇩o⇩n1" "σ⇩1_object4⇩P⇩e⇩r⇩s⇩o⇩n" "σ⇩1_object4" "X⇩P⇩e⇩r⇩s⇩o⇩n2⇩P⇩e⇩r⇩s⇩o⇩n" "X⇩P⇩e⇩r⇩s⇩o⇩n2"
by(rule σ⇩1)

interpretation state_σ⇩1': state_σ⇩1' "oid1" "oid2" "oid3" "X⇩P⇩e⇩r⇩s⇩o⇩n1⇩P⇩e⇩r⇩s⇩o⇩n" "X⇩P⇩e⇩r⇩s⇩o⇩n1" "X⇩P⇩e⇩r⇩s⇩o⇩n2⇩P⇩e⇩r⇩s⇩o⇩n" "X⇩P⇩e⇩r⇩s⇩o⇩n2" "X⇩P⇩e⇩r⇩s⇩o⇩n3⇩P⇩e⇩r⇩s⇩o⇩n" "X⇩P⇩e⇩r⇩s⇩o⇩n3"
by(rule σ⇩1')

definition "heap_σ⇩1 = (heap (state_σ⇩1.σ⇩1))"

definition "heap_σ⇩1' = (heap (state_σ⇩1'.σ⇩1'))"
end

end